ZeroMomentCoefficients.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroMomentDerivatives
6 import KomorebiPaperIV.BellCompletion
7 import KomorebiPaperIV.ReciprocalCompletion
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Filter FormalMultilinearSeries
12 open scoped Topology
13 
14 theorem entireReducedDenominator_iteratedDeriv_zero {N : ℕ} (hN : 0 < N) (n : ℕ) :
15     iteratedDeriv n (entireReducedDenominator N) 0 =
16       (n.factorial : ℂ) * PowerSeries.coeff n (reducedDenominator (R := ℂ) N) := by
17   let p := ofScalars ℂ (fun n => PowerSeries.coeff n (reducedDenominator (R := ℂ) N))
18   have hp : HasFPowerSeriesAt (entireReducedDenominator N) p 0 :=
19     (p.hasFPowerSeriesOnBall (by dsimp [p]; rw [reducedDenominator_entire_radius hN]; simp)).hasFPowerSeriesAt
20   have he := hp.eq_formalMultilinearSeries (analyticAt_entireReducedDenominator hN 0).hasFPowerSeriesAt
21   have hc := congrArg (fun q : FormalMultilinearSeries ℂ ℂ ℂ => q.coeff n) he
22   simp only [p, coeff_ofScalars] at hc
23   have hn : (n.factorial : ℂ) ≠ 0 := by exact_mod_cast n.factorial_ne_zero
24   exact ((div_eq_iff hn).mp hc.symm).trans (mul_comm _ _)
25 
26 theorem zeroResolvent_analyticAt_zero {f : ℂ → ℂ} (hf : Differentiable ℂ f)
27     (hs : ZeroPowerSummable f 1) (h0 : f 0 ≠ 0) :
28     AnalyticAt ℂ (fun w => ∑' i, zeroPartialFraction f i w) 0 := by
29   have hU : IsOpen {w : ℂ | f w ≠ 0} := isOpen_ne_fun hf.continuous continuous_const
30   have h := (zeroPartialFraction_locally_uniform hs h0).mono (subset_univ {w : ℂ | f w ≠ 0})
31   apply (h.differentiableOn ?_ hU).analyticAt (hU.mem_nhds h0)
32   apply Eventually.of_forall
33   intro S
34   apply DifferentiableOn.fun_sum
35   intro i _ w hw
36   have hn : w ≠ indexedZero i := by intro he; apply hw; rw [he]; exact i.1.property
37   exact ((hasDerivAt_const w (1 : ℂ)).div
38     ((hasDerivAt_const w (indexedZero i)).sub (hasDerivAt_id w))
39     (sub_ne_zero.mpr hn.symm)).differentiableAt.differentiableWithinAt
40 
41 /-- Newton's convolution for the actual complex zero power sums, obtained by
42 differentiating the proved analytic partial-fraction identity at zero. -/
43 theorem reducedZeroPowerSum_convolution {N : ℕ} (hN : 2 ≤ N) (n : ℕ) :
44     (∑ k ∈ Finset.range (n + 1),
45       PowerSeries.coeff k (reducedDenominator (R := ℂ) N) *
46         zeroPowerSum (entireReducedDenominator N) (n - k + 1)) =
47       -(PowerSeries.coeff (n + 1) (reducedDenominator (R := ℂ) N) * (n + 1 : ℂ)) := by
48   let f := entireReducedDenominator N
49   let G : ℂ → ℂ := fun w => ∑' i, zeroPartialFraction f i w
50   have hf : Differentiable ℂ f := fun z => (analyticAt_entireReducedDenominator (by omega) z).differentiableAt
51   have hs := entireReducedDenominator_reciprocal_zeros_summable hN
52   have h0 : f 0 ≠ 0 := by dsimp [f]; rw [entireReducedDenominator_zero]; exact one_ne_zero
53   have hG : AnalyticAt ℂ G 0 := zeroResolvent_analyticAt_zero hf hs h0
54   have hnear : f * G =ᶠ[𝓝 0] -deriv f := by
55     filter_upwards [hf.continuous.continuousAt.eventually_ne h0] with w hw
56     have h := entireReducedDenominator_partialFractions hN hw
57     change -logDeriv f w = G w at h
58     change f w * G w = -deriv f w
59     rw [← h, logDeriv_apply]
60     field_simp
61   have he := hnear.iteratedDeriv_eq n
62   rw [iteratedDeriv_mul (hf.analyticAt 0).contDiffAt hG.contDiffAt,
63     iteratedDeriv_neg, ← iteratedDeriv_succ'] at he
64   simp only [f, entireReducedDenominator_iteratedDeriv_zero (show 0 < N by omega)] at he
65   have hGD (k : ℕ) : iteratedDeriv k G 0 =
66       (k.factorial : ℂ) * zeroPowerSum f (k + 1) := zeroPowerSum_resolvent_derivative hf hs h0 k
67   simp only [hGD] at he
68   have hsimp : (∑ k ∈ Finset.range (n + 1),
69       (n.choose k : ℂ) * ((k.factorial : ℂ) * PowerSeries.coeff k (reducedDenominator (R := ℂ) N)) *
70         ((n - k).factorial : ℂ) * zeroPowerSum f (n - k + 1)) =
71       (n.factorial : ℂ) * ∑ k ∈ Finset.range (n + 1),
72         PowerSeries.coeff k (reducedDenominator (R := ℂ) N) * zeroPowerSum f (n - k + 1) := by
73     rw [Finset.mul_sum]
74     apply Finset.sum_congr rfl
75     intro k hk
76     have hk' : k ≤ n := by simpa only [Finset.mem_range, Nat.lt_succ_iff] using hk
77     have hfac : (n.choose k : ℂ) * (k.factorial : ℂ) * ((n - k).factorial : ℂ) = (n.factorial : ℂ) := by
78       exact_mod_cast Nat.choose_mul_factorial_mul_factorial hk'
79     linear_combination (PowerSeries.coeff k (reducedDenominator (R := ℂ) N) * zeroPowerSum f (n - k + 1)) * hfac
80   have hn : (n.factorial : ℂ) ≠ 0 := by exact_mod_cast n.factorial_ne_zero
81   apply mul_left_cancel₀ hn
82   dsimp [f] at hsimp
83   rw [← hsimp]
84   have hfac : ((n + 1).factorial : ℂ) = (n + 1 : ℂ) * (n.factorial : ℂ) := by
85     simp only [Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one]
86   rw [hfac] at he
87   dsimp [f] at he
88   simpa only [mul_assoc, mul_comm, mul_left_comm, mul_neg] using he
89 
90 def zeroMomentSeries (f : ℂ → ℂ) : PowerSeries ℂ :=
91   PowerSeries.mk (fun n => zeroPowerSum f (n + 1))
92 
93 theorem reducedDenominator_mul_zeroMomentSeries {N : ℕ} (hN : 2 ≤ N) :
94     reducedDenominator (R := ℂ) N * zeroMomentSeries (entireReducedDenominator N) =
95       -PowerSeries.derivative ℂ (reducedDenominator N) := by
96   ext n
97   rw [PowerSeries.coeff_mul, map_neg, PowerSeries.coeff_derivative]
98   simp only [zeroMomentSeries, PowerSeries.coeff_mk]
99   rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
100   exact reducedZeroPowerSum_convolution hN n
101 
102 /-- Every formal logarithmic coefficient equals the actual zero power sum. -/
103 theorem kappaCoeff_eq_zeroPowerSum {N m : ℕ} (hN : 2 ≤ N) (hm : 0 < m) :
104     kappaCoeff (R := ℂ) N m = zeroPowerSum (entireReducedDenominator N) m := by
105   have hu : IsUnit (reducedDenominator (R := ℂ) N) :=
106     PowerSeries.isUnit_iff_constantCoeff.mpr (by rw [constantCoeff_reducedDenominator]; exact isUnit_one)
107   have he : zeroMomentSeries (entireReducedDenominator N) = reducedTangentSeries (R := ℂ) N :=
108     hu.mul_left_cancel ((reducedDenominator_mul_zeroMomentSeries hN).trans
109       (reducedDenominator_mul_reducedTangentSeries (R := ℂ) N).symm)
110   obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm.ne'
111   have hc := congrArg (PowerSeries.coeff n) he
112   simpa only [zeroMomentSeries, PowerSeries.coeff_mk, coeff_reducedTangentSeries] using hc.symm
113 
114 theorem reducedZeroPowerSum_newton {N : ℕ} (hN : 2 ≤ N) (n : ℕ) :
115     zeroPowerSum (entireReducedDenominator N) (n + 1) =
116       -((n + 1 : ℂ) * PowerSeries.coeff (n + 1) (reducedDenominator (R := ℂ) N)) -
117       ∑ k ∈ Finset.range n, PowerSeries.coeff (k + 1) (reducedDenominator (R := ℂ) N) *
118         zeroPowerSum (entireReducedDenominator N) (n - k) := by
119   have h := reducedZeroPowerSum_convolution hN n
120   rw [Finset.sum_range_succ'] at h
121   simp only [Nat.sub_zero, PowerSeries.coeff_zero_eq_constantCoeff, constantCoeff_reducedDenominator, one_mul] at h
122   have he : (∑ k ∈ Finset.range n,
123       PowerSeries.coeff (k + 1) (reducedDenominator (R := ℂ) N) *
124         zeroPowerSum (entireReducedDenominator N) (n - (k + 1) + 1)) =
125       ∑ k ∈ Finset.range n,
126       PowerSeries.coeff (k + 1) (reducedDenominator (R := ℂ) N) *
127         zeroPowerSum (entireReducedDenominator N) (n - k) := by
128     apply Finset.sum_congr rfl
129     intro k hk
130     rw [show n - (k + 1) + 1 = n - k by have := Finset.mem_range.mp hk; omega]
131   rw [he] at h
132   linear_combination h
133 
134 /-- Corollary 12.9 in exactly the manuscript's factorial normalization. -/
135 theorem transferTangentCoeff_zero_sum {N : ℕ} (hN : 2 ≤ N) (n : ℕ) :
136     transferTangentCoeff (R := ℂ) N n =
137       (N : ℂ) * ((N * n + N - 1).factorial : ℂ) * zeroPowerSum (entireReducedDenominator N) (n + 1) := by
138   rw [transferTangentCoeff_eq_kappa, kappaCoeff_eq_zeroPowerSum hN (by omega)]
139 
140 theorem bellInput_zero_sums {N : ℕ} (hN : 2 ≤ N) (r : ℂ) :
141     bellInput (fun m => r * ((m - 1).factorial : ℂ) * kappaCoeff N m) =
142       bellInput (fun m => r * ((m - 1).factorial : ℂ) * zeroPowerSum (entireReducedDenominator N) m) := by
143   ext m
144   simp only [bellInput, PowerSeries.coeff_mk]
145   split_ifs with hm
146   · rfl
147   · rw [kappaCoeff_eq_zeroPowerSum hN (Nat.pos_of_ne_zero hm)]
148 
149 /-- Corollary 12.10: reciprocal coefficients from the genuine zero multiset. -/
150 theorem reciprocalCoeff_zero_sum_bell {N : ℕ} (hN : 2 ≤ N) (n : ℕ) (r : ℂ) :
151     reciprocalCoeff N n r =
152       ((N * n).factorial : ℂ) / (n.factorial : ℂ) * completeExponentialBell n
153         (fun m => r * ((m - 1).factorial : ℂ) * zeroPowerSum (entireReducedDenominator N) m) := by
154   rw [reciprocalCoeff_bell_formula, completeExponentialBell, bellInput_zero_sums hN]
155   rfl
156 
157 end
158 end Komorebi.PaperIV

Back to source controls