NormalizedZeroBell.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.NormalizedProduct
6 import KomorebiPaperIV.AnalyticTaylorDifferential
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 
11 theorem normalized_zeroMomentSeries {N : ℕ} (hN : 2 ≤ N) (j : ℕ) :
12     zeroMomentSeries (entireNormalizedSection N j) =
13       PowerSeries.derivative ℂ (normalizedResidueNegativeLog N j) := by
14   have hN0 : 0 < N := by omega
15   have hs := entireNormalizedSection_zeroPowerSummable hN0 j
16     ((div_lt_one (by positivity : (0 : ℝ) < N)).mpr (by exact_mod_cast (show 1 < N by omega)))
17   have h := hadamard_taylor_zeroMoment_identity
18     (fun z => (analyticAt_entireNormalizedSection hN0 j z).differentiableAt) hs
19     (by rw [entireNormalizedSection_zero]; exact one_ne_zero)
20     (entireNormalizedSection_hadamard hN j)
21   rw [analyticTaylorSeries_entireNormalizedSection hN0,
22     ← normalizedResidueSectionAlg_eq_normalizedResidueSection] at h
23   have hunit : IsUnit (normalizedResidueSectionAlg (R := ℂ) N j) :=
24     PowerSeries.isUnit_iff_constantCoeff.mpr (by simp)
25   apply hunit.mul_left_cancel
26   rw [h, normalizedResidueNegativeLog, map_neg, mul_neg,
27     mul_derivative_logOf (constantCoeff_normalizedResidueSectionAlg N j)]
28 
29 theorem normalized_zeroPowerSum {N : ℕ} (hN : 2 ≤ N) (j n : ℕ) :
30     zeroPowerSum (entireNormalizedSection N j) (n + 1) =
31       PowerSeries.coeff (n + 1) (normalizedResidueNegativeLog (R := ℂ) N j) * (n + 1 : ℂ) := by
32   have h := congrArg (PowerSeries.coeff n) (normalized_zeroMomentSeries hN j)
33   simpa [zeroMomentSeries, PowerSeries.coeff_derivative] using h
34 
35 theorem bellInput_normalized_zeros {N : ℕ} (hN : 2 ≤ N) (j : ℕ) (r : ℂ) :
36     bellInput (fun m => r * ((m - 1).factorial : ℂ) * zeroPowerSum (entireNormalizedSection N j) m) =
37       PowerSeries.C r * normalizedResidueNegativeLog N j := by
38   ext m
39   cases m with
40   | zero => simp [bellInput, PowerSeries.coeff_zero_eq_constantCoeff]
41   | succ m =>
42     simp only [bellInput, PowerSeries.coeff_mk, Nat.succ_ne_zero, ↓reduceIte,
43       Nat.succ_sub_one, normalized_zeroPowerSum hN, PowerSeries.coeff_C_mul]
44     rw [Nat.factorial_succ, Nat.cast_mul]
45     have hm : (m.factorial : ℂ) ≠ 0 := by exact_mod_cast m.factorial_ne_zero
46     have hs : (m.succ : ℂ) ≠ 0 := by exact_mod_cast Nat.succ_ne_zero m
47     field_simp
48     simp
49 
50 /-- The exact coefficient normalization in Proposition 12.4, in terms of
51 the actual nonzero zeros with their analytic multiplicities. -/
52 theorem residuePowerCoeff_zero_sum_bell {N : ℕ} (hN : 2 ≤ N) (j n : ℕ) (r : ℂ) :
53     residuePowerCoeff N j n r = ((N * n).factorial : ℂ) / (n.factorial : ℂ) *
54       completeExponentialBell n (fun m => r * ((m - 1).factorial : ℂ) *
55         zeroPowerSum (entireNormalizedSection N j) m) := by
56   rw [completeExponentialBell, bellInput_normalized_zeros hN, residuePowerCoeff, blockCoeff,
57     residuePowerSeries, formalExpFamily_eq_exp_subst (constantCoeff_normalizedResidueNegativeLog N j)]
58   have hn : (n.factorial : ℂ) ≠ 0 := by exact_mod_cast n.factorial_ne_zero
59   field_simp
60 
61 end
62 end Komorebi.PaperIV

Back to source controls