CanonicalPartialFractions.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.HadamardIdentification
6 import Mathlib.Analysis.Calculus.LogDerivUniformlyOn
7 import Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Filter
12 open scoped Topology
13 
14 def zeroPartialFraction (f : ℂ → ℂ) (i : ZeroMultiplicityIndex f) (w : ℂ) : ℂ :=
15   1 / (indexedZero i - w)
16 
17 theorem zeroPartialFraction_uniform_majorant {f : ℂ → ℂ}
18     (hf : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) {B : ℝ} (hB : 0 ≤ B) :
19     ∀ᶠ i : ZeroMultiplicityIndex f in cofinite, ∀ w : ℂ, ‖w‖ ≤ B →
20       ‖zeroPartialFraction f i w‖ ≤ 2 / ‖indexedZero i‖ := by
21   have ht := (zeroMultiplicity_reciprocal_summable hf).tendsto_cofinite_zero
22   have hC : 0 < 2 * (B + 1) := by positivity
23   filter_upwards [ht.eventually (gt_mem_nhds (one_div_pos.mpr hC))] with i hi
24   intro w hw
25   have ha : 0 < ‖indexedZero i‖ := norm_pos_iff.mpr (indexedZero_ne_zero hf0 i)
26   have hlarge : 2 * (B + 1) < ‖indexedZero i‖ := by
27     simpa only [one_mul] using (div_lt_div_iff₀ ha hC).mp hi
28   have htri := norm_sub_norm_le (indexedZero i) w
29   have hd : 0 < ‖indexedZero i - w‖ := by linarith
30   simp only [zeroPartialFraction, norm_div, norm_one]
31   apply (div_le_div_iff₀ hd ha).mpr
32   nlinarith
33 
34 theorem zeroPartialFraction_norm_summable {f : ℂ → ℂ}
35     (hf : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) (w : ℂ) :
36     Summable (fun i : ZeroMultiplicityIndex f => ‖zeroPartialFraction f i w‖) := by
37   have hm := (zeroMultiplicity_reciprocal_summable hf).mul_left 2
38   apply hm.of_norm_bounded_eventually
39   filter_upwards [zeroPartialFraction_uniform_majorant hf hf0 (norm_nonneg w)] with i hi
40   simpa only [norm_norm, mul_one_div] using hi w le_rfl
41 
42 /-- Compact-uniform convergence of the unregularized partial fractions. -/
43 theorem zeroPartialFraction_uniform_on_compact {f : ℂ → ℂ}
44     (hf : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) {K : Set ℂ} (hK : IsCompact K) :
45     HasSumUniformlyOn (zeroPartialFraction f) (fun w => ∑' i, zeroPartialFraction f i w) K := by
46   obtain ⟨B, hB⟩ := hK.isBounded.exists_norm_le
47   have hb : 0 ≤ max 0 B := le_max_left _ _
48   apply HasSumUniformlyOn.of_norm_le_summable_eventually ((zeroMultiplicity_reciprocal_summable hf).mul_left 2)
49   filter_upwards [zeroPartialFraction_uniform_majorant hf hf0 hb] with i hi
50   intro w hw
51   simpa only [mul_one_div] using hi w ((hB w hw).trans (le_max_right _ _))
52 
53 theorem logDeriv_linear_factor {a w : ℂ} (ha : a ≠ 0) (hw : w ≠ a) :
54     logDeriv (fun z : ℂ => 1 - z / a) w = -(1 / (a - w)) := by
55   rw [logDeriv_apply]
56   erw [((hasDerivAt_const w (1 : ℂ)).sub ((hasDerivAt_id w).div_const a)).deriv]
57   have hwa : a - w ≠ 0 := sub_ne_zero.mpr hw.symm
58   field_simp
59   ring
60 
61 theorem fullCanonicalProduct_logDeriv {f : ℂ → ℂ}
62     (hf : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) {w : ℂ}
63     (hw : ∀ i : ZeroMultiplicityIndex f, w ≠ indexedZero i) :
64     -logDeriv (fullCanonicalProduct f) w = ∑' i, zeroPartialFraction f i w := by
65   have hn : ∀ i : ZeroMultiplicityIndex f, 1 - w / indexedZero i ≠ 0 := by
66     intro i
67     rw [sub_ne_zero]
68     intro he
69     exact hw i ((div_eq_one_iff_eq (indexedZero_ne_zero hf0 i)).mp he.symm)
70   have he : (fun i : ZeroMultiplicityIndex f => logDeriv (fun z : ℂ => 1 - z / indexedZero i) w) =
71       (fun i => -zeroPartialFraction f i w) := by
72     funext i
73     exact logDeriv_linear_factor (indexedZero_ne_zero hf0 i) (hw i)
74   have hs : Summable (fun i : ZeroMultiplicityIndex f => logDeriv (fun z : ℂ => 1 - z / indexedZero i) w) := by
75     rw [he]
76     exact (zeroPartialFraction_norm_summable hf hf0 w).of_norm.neg
77   have h := logDeriv_tprod_eq_tsum isOpen_univ (mem_univ w) hn
78     (fun _ => by fun_prop) hs (fullCanonicalProduct_locally_uniform hf).multipliableLocallyUniformlyOn
79     (fullCanonicalProduct_ne_zero hf hf0 hw)
80   change logDeriv (fullCanonicalProduct f) w = _ at h
81   rw [he, tsum_neg] at h
82   linear_combination -h
83 
84 theorem entireReducedDenominator_partialFractions {N : ℕ} (hN : 2 ≤ N)
85     {w : ℂ} (hw : entireReducedDenominator N w ≠ 0) :
86     -logDeriv (entireReducedDenominator N) w =
87       ∑' i : ZeroMultiplicityIndex (entireReducedDenominator N), 1 / (indexedZero i - w) := by
88   have hf0 : entireReducedDenominator N 0 ≠ 0 := by rw [entireReducedDenominator_zero]; exact one_ne_zero
89   have hneq : ∀ i : ZeroMultiplicityIndex (entireReducedDenominator N), w ≠ indexedZero i := by
90     intro i he
91     apply hw
92     rw [he]
93     exact i.1.property
94   have h := fullCanonicalProduct_logDeriv (entireReducedDenominator_reciprocal_zeros_summable hN) hf0 hneq
95   simpa only [← entireReducedDenominator_eq_fullCanonicalProduct hN, zeroPartialFraction] using h
96 
97 theorem zeroPartialFraction_locally_uniform {f : ℂ → ℂ}
98     (hf : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) :
99     HasSumLocallyUniformlyOn (zeroPartialFraction f) (fun w => ∑' i, zeroPartialFraction f i w) univ := by
100   apply hasSumLocallyUniformlyOn_of_forall_compact isOpen_univ
101   intro K _ hK
102   exact zeroPartialFraction_uniform_on_compact hf hf0 hK
103 
104 /-- The manuscript's tangent as an actual meromorphic function. -/
105 def analyticTransferTangent (N : ℕ) (z : ℂ) : ℂ :=
106   -logDeriv (canonicalSignedDenominator N) z
107 
108 theorem analyticTransferTangent_eq_reduced_logDeriv {N : ℕ} (hN : 0 < N) (z : ℂ) :
109     analyticTransferTangent N z =
110       (N : ℂ) * z ^ (N - 1) * (-logDeriv (entireReducedDenominator N) (z ^ N)) := by
111   have he : canonicalSignedDenominator N = entireReducedDenominator N ∘ (fun w : ℂ => w ^ N) :=
112     funext (canonicalSignedDenominator_eq_reduced_power hN)
113   rw [analyticTransferTangent, he, logDeriv_comp
114     (analyticAt_entireReducedDenominator hN _).differentiableAt (by fun_prop)]
115   rw [(hasDerivAt_pow N z).deriv]
116   ring
117 
118 /-- Corollary 12.7: the full, unregularized Mittag-Leffler identity. -/
119 theorem analyticTransferTangent_mittagLeffler {N : ℕ} (hN : 2 ≤ N)
120     {z : ℂ} (hz : canonicalSignedDenominator N z ≠ 0) :
121     analyticTransferTangent N z = (N : ℂ) * z ^ (N - 1) *
122       ∑' i : ZeroMultiplicityIndex (entireReducedDenominator N), 1 / (indexedZero i - z ^ N) := by
123   have hw : entireReducedDenominator N (z ^ N) ≠ 0 := by
124     rwa [← canonicalSignedDenominator_eq_reduced_power (by omega)]
125   rw [analyticTransferTangent_eq_reduced_logDeriv (by omega), entireReducedDenominator_partialFractions hN hw]
126 
127 theorem analyticTransferTangent_mittagLeffler_absolute {N : ℕ} (hN : 2 ≤ N) (z : ℂ) :
128     Summable (fun i : ZeroMultiplicityIndex (entireReducedDenominator N) =>
129       ‖(1 : ℂ) / (indexedZero i - z ^ N)‖) :=
130   zeroPartialFraction_norm_summable (entireReducedDenominator_reciprocal_zeros_summable hN)
131     (by rw [entireReducedDenominator_zero]; exact one_ne_zero) _
132 
133 /-- Uniform convergence is asserted for the summed fractions. The formula for
134 the tangent is restricted to nonpoles in the preceding theorem. -/
135 theorem analyticTransferTangent_mittagLeffler_locally_uniform {N : ℕ} (hN : 2 ≤ N) :
136     HasSumLocallyUniformlyOn
137       (fun (i : ZeroMultiplicityIndex (entireReducedDenominator N)) z => 1 / (indexedZero i - z ^ N))
138       (fun z => ∑' i : ZeroMultiplicityIndex (entireReducedDenominator N), 1 / (indexedZero i - z ^ N))
139       univ := by
140   have h := zeroPartialFraction_locally_uniform (entireReducedDenominator_reciprocal_zeros_summable hN)
141     (by rw [entireReducedDenominator_zero]; exact one_ne_zero)
142   exact h.comp (fun z : ℂ => z ^ N) (mapsTo_univ _ _) (by fun_prop : ContinuousOn (fun z : ℂ => z ^ N) univ)
143 
144 end
145 end Komorebi.PaperIV

Back to source controls