ZeroMomentLogarithm.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroMomentCoefficients
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter Metric FormalMultilinearSeries
10 open scoped Topology NNReal
11 
12 /-- Taylor convergence throughout an open complex disk, with the radius
13 proved by Cauchy's formula on each smaller closed disk. -/
14 theorem differentiableOn_ball_taylor_hasSum {f : ℂ → ℂ} {R : ℝ}
15     (hf : DifferentiableOn ℂ f (ball 0 R)) {w : ℂ} (hw : w ∈ ball 0 R) :
16     HasSum (fun n => iteratedDeriv n f 0 / (n.factorial : ℂ) * w ^ n) (f w) := by
17   have hwR : ‖w‖ < R := mem_ball_zero_iff.mp hw
18   obtain ⟨S, hwS, hSR⟩ := exists_between hwR
19   have hS : 0 < S := lt_of_le_of_lt (norm_nonneg w) hwS
20   let s : ℝ≥0 := ⟨S, hS.le⟩
21   have hd : DifferentiableOn ℂ f (closedBall 0 (s : ℝ)) :=
22     hf.mono (fun z hz => mem_ball_zero_iff.mpr ((mem_closedBall_zero_iff.mp hz).trans_lt hSR))
23   have hp := hd.hasFPowerSeriesOnBall (show 0 < s from hS)
24   have he := hp.hasFPowerSeriesAt.eq_formalMultilinearSeries
25     (hf.analyticAt (isOpen_ball.mem_nhds (mem_ball_self (hS.trans hSR)))).hasFPowerSeriesAt
26   rw [he] at hp
27   have h := hp.hasSum_sub (show w ∈ eball (0 : ℂ) (s : ENNReal) by
28     rw [eball_coe]; exact mem_ball_zero_iff.mpr hwS)
29   simpa only [sub_zero, ofScalars_apply_eq', smul_eq_mul, mul_comm] using h
30 
31 /-- On every zero-free disk the normalized negative logarithm has exactly
32 the zero-moment Taylor series. The logarithm is the analytic branch with
33 value zero at the origin, rather than an unrestricted principal logarithm. -/
34 theorem reducedZeroPowerSum_logarithm {N : ℕ} (hN : 2 ≤ N) {R : ℝ} (hR : 0 < R)
35     (hn : ∀ w ∈ ball (0 : ℂ) R, entireReducedDenominator N w ≠ 0) :
36     ∃ L : ℂ → ℂ, DifferentiableOn ℂ L (ball 0 R) ∧ L 0 = 0 ∧
37       (∀ w ∈ ball (0 : ℂ) R, Complex.exp (-L w) = entireReducedDenominator N w) ∧
38       ∀ w ∈ ball (0 : ℂ) R,
39         HasSum (fun m => zeroPowerSum (entireReducedDenominator N) m * w ^ m / (m : ℂ)) (L w) := by
40   let f := entireReducedDenominator N
41   let G : ℂ → ℂ := fun w => ∑' i, zeroPartialFraction f i w
42   have hf : Differentiable ℂ f := fun z => (analyticAt_entireReducedDenominator (by omega) z).differentiableAt
43   have hs := entireReducedDenominator_reciprocal_zeros_summable hN
44   have h0 : f 0 ≠ 0 := by dsimp [f]; rw [entireReducedDenominator_zero]; exact one_ne_zero
45   have hG : DifferentiableOn ℂ G (ball 0 R) := by
46     have he : EqOn G (fun w => -logDeriv f w) (ball 0 R) :=
47       fun w hw => (entireReducedDenominator_partialFractions hN (hn w hw)).symm
48     apply DifferentiableOn.congr _ he
49     intro w hw
50     exact (((hf.analyticAt w).deriv.differentiableAt.div (hf w) (hn w hw)).neg).differentiableWithinAt
51   obtain ⟨L, hL0, hL⟩ := hG.isExactOn_ball.with_val_at 0 0
52   have hLd : DifferentiableOn ℂ L (ball 0 R) := fun w hw => (hL w hw).differentiableAt.differentiableWithinAt
53   have hH : ∀ w ∈ ball (0 : ℂ) R, HasDerivAt (fun z => f z * Complex.exp (L z)) 0 w := by
54     intro w hw
55     have he : G w = -logDeriv f w := (entireReducedDenominator_partialFractions hN (hn w hw)).symm
56     convert! (hf w).hasDerivAt.mul (hL w hw).cexp using 1
57     rw [he, logDeriv_apply]
58     field_simp [show f w ≠ 0 from hn w hw]
59     ring
60   have hExp : ∀ w ∈ ball (0 : ℂ) R, Complex.exp (-L w) = f w := by
61     intro w hw
62     have he := isOpen_ball.is_const_of_deriv_eq_zero (convex_ball (0 : ℂ) R).isPreconnected
63       (fun z hz => (hH z hz).differentiableAt.differentiableWithinAt)
64       (fun z hz => (hH z hz).deriv) hw (mem_ball_self hR)
65     simp only [f, entireReducedDenominator_zero, hL0, Complex.exp_zero, one_mul] at he
66     rw [Complex.exp_neg]
67     exact (eq_inv_of_mul_eq_one_left he).symm
68   have hcoeff (n : ℕ) : iteratedDeriv n L 0 / (n.factorial : ℂ) = zeroPowerSum f n / (n : ℂ) := by
69     cases n with
70     | zero => simp [hL0]
71     | succ n =>
72       have he : deriv L =ᶠ[𝓝 0] G := by
73         filter_upwards [isOpen_ball.mem_nhds (mem_ball_self hR)] with w hw
74         exact (hL w hw).deriv
75       rw [iteratedDeriv_succ', he.iteratedDeriv_eq n,
76         zeroPowerSum_resolvent_derivative hf hs h0 n]
77       have hfac : (n.factorial : ℂ) ≠ 0 := by exact_mod_cast n.factorial_ne_zero
78       simp only [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one]
79       field_simp
80   refine ⟨L, hLd, hL0, hExp, fun w hw => ?_⟩
81   have ht := differentiableOn_ball_taylor_hasSum hLd hw
82   simp only [hcoeff] at ht
83   simpa only [div_mul_eq_mul_div] using ht
84 
85 /-- The analytic resolvent realizes the same coefficients as the formal
86 logarithmic derivative throughout any zero-free disk. -/
87 theorem reducedZeroPowerSum_resolvent_hasSum {N : ℕ} (hN : 2 ≤ N) {R : ℝ}
88     (hn : ∀ w ∈ ball (0 : ℂ) R, entireReducedDenominator N w ≠ 0)
89     {w : ℂ} (hw : w ∈ ball (0 : ℂ) R) :
90     HasSum (fun n => zeroPowerSum (entireReducedDenominator N) (n + 1) * w ^ n)
91       (-logDeriv (entireReducedDenominator N) w) := by
92   let f := entireReducedDenominator N
93   let G : ℂ → ℂ := fun w => ∑' i, zeroPartialFraction f i w
94   have hf : Differentiable ℂ f := fun z => (analyticAt_entireReducedDenominator (by omega) z).differentiableAt
95   have hs := entireReducedDenominator_reciprocal_zeros_summable hN
96   have h0 : f 0 ≠ 0 := by dsimp [f]; rw [entireReducedDenominator_zero]; exact one_ne_zero
97   have hG : DifferentiableOn ℂ G (ball 0 R) := by
98     apply DifferentiableOn.congr _ (fun z hz => (entireReducedDenominator_partialFractions hN (hn z hz)).symm)
99     intro z hz
100     exact (((hf.analyticAt z).deriv.differentiableAt.div (hf z) (hn z hz)).neg).differentiableWithinAt
101   have ht := differentiableOn_ball_taylor_hasSum hG hw
102   have hc (n : ℕ) : iteratedDeriv n G 0 / (n.factorial : ℂ) = zeroPowerSum f (n + 1) := by
103     rw [zeroPowerSum_resolvent_derivative hf hs h0 n]
104     exact mul_div_cancel_left₀ _ (by exact_mod_cast n.factorial_ne_zero)
105   simp only [hc] at ht
106   rwa [entireReducedDenominator_partialFractions hN (hn w hw)]
107 
108 /-- The factorial-normalized tangent coefficients are coefficients of the
109 actual analytic tangent, not merely of an unrelated formal series. -/
110 theorem analyticTransferTangent_coefficient_hasSum {N : ℕ} (hN : 2 ≤ N) {R : ℝ}
111     (hn : ∀ w ∈ ball (0 : ℂ) R, entireReducedDenominator N w ≠ 0)
112     {z : ℂ} (hz : z ^ N ∈ ball (0 : ℂ) R) :
113     HasSum (fun n => transferTangentCoeff (R := ℂ) N n /
114       ((N * n + N - 1).factorial : ℂ) * z ^ (N * n + N - 1))
115       (analyticTransferTangent N z) := by
116   have ht := (reducedZeroPowerSum_resolvent_hasSum hN hn hz).mul_left ((N : ℂ) * z ^ (N - 1))
117   rw [← analyticTransferTangent_eq_reduced_logDeriv (show 0 < N by omega)] at ht
118   convert! ht using 1
119   funext n
120   rw [transferTangentCoeff_zero_sum hN]
121   have hfac : ((N * n + N - 1).factorial : ℂ) ≠ 0 := by exact_mod_cast (N * n + N - 1).factorial_ne_zero
122   field_simp
123   rw [show N * n + N - 1 = N * n + (N - 1) by omega, pow_add, pow_mul]
124   ring
125 
126 end
127 end Komorebi.PaperIV

Back to source controls