NormalizedAnalyticPowers.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.NormalizedZeroBell
6 import Mathlib.Analysis.SpecialFunctions.Complex.Analytic
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 theorem powerSeries_eq_of_derivative_constant {F G : PowerSeries ℂ}
14     (h0 : F.constantCoeff = G.constantCoeff) (hd : PowerSeries.derivative ℂ F = PowerSeries.derivative ℂ G) : F = G := by
15   ext n
16   cases n with
17   | zero => simpa only [PowerSeries.coeff_zero_eq_constantCoeff] using h0
18   | succ n =>
19     have h := congrArg (PowerSeries.coeff n) hd
20     simp only [PowerSeries.coeff_derivative] at h
21     exact mul_right_cancel₀ (by exact_mod_cast Nat.succ_ne_zero n : (n+1 : ℂ) ≠ 0) h
22 
23 theorem analyticTaylorSeries_log {f : ℂ → ℂ} (hf : Differentiable ℂ f) (h0 : f 0 = 1) :
24     analyticTaylorSeries (fun z => Complex.log (f z)) = PowerSeries.logOf (analyticTaylorSeries f) := by
25   let L : ℂ → ℂ := fun z => Complex.log (f z)
26   have hslit : f 0 ∈ Complex.slitPlane := by rw [h0]; simp
27   have hL : AnalyticAt ℂ L 0 := (analyticAt_clog hslit).comp (hf.analyticAt 0)
28   have he : (fun z => f z * deriv L z) =ᶠ[𝓝 0] deriv f := by
29     filter_upwards [hf.continuous.continuousAt.preimage_mem_nhds (Complex.isOpen_slitPlane.mem_nhds hslit)] with z hz
30     have hd := ((hf z).hasDerivAt.clog hz).deriv
31     change deriv L z = deriv f z / f z at hd
32     rw [hd]
33     field_simp [Complex.slitPlane_ne_zero hz]
34   have hprod : analyticTaylorSeries f * PowerSeries.derivative ℂ (analyticTaylorSeries L) =
35       PowerSeries.derivative ℂ (analyticTaylorSeries f) := by
36     rw [← analyticTaylorSeries_deriv,
37       ← analyticTaylorSeries_mul (g := deriv L) (hf.analyticAt 0) hL.deriv,
38       analyticTaylorSeries_congr he, analyticTaylorSeries_deriv]
39   have hunit : IsUnit (analyticTaylorSeries f) := PowerSeries.isUnit_iff_constantCoeff.mpr (by simp [h0])
40   have hc1 : (analyticTaylorSeries f).constantCoeff = 1 := by simp [h0]
41   apply powerSeries_eq_of_derivative_constant
42   · simp only [analyticTaylorSeries_constantCoeff, h0, Complex.log_one, PowerSeries.constantCoeff_logOf hc1]
43   · exact hunit.mul_left_cancel (hprod.trans
44       (mul_derivative_logOf (by simpa using h0)).symm)
45 
46 theorem analyticTaylorSeries_exp {g : ℂ → ℂ} (hg : AnalyticAt ℂ g 0) (h0 : g 0 = 0) :
47     analyticTaylorSeries (fun z => Complex.exp (g z)) =
48       formalExpFamily (analyticTaylorSeries g) 1 := by
49   let E : ℂ → ℂ := fun z => Complex.exp (g z)
50   have hE : AnalyticAt ℂ E 0 := hg.cexp
51   have he : deriv E =ᶠ[𝓝 0] (fun z => E z * deriv g z) := by
52     filter_upwards [hg.eventually_analyticAt] with z hz
53     exact hz.differentiableAt.hasDerivAt.cexp.deriv
54   have hS0 : (analyticTaylorSeries g).constantCoeff = 0 := by simp [h0]
55   apply powerSeries_linear_ode_unique (H := PowerSeries.derivative ℂ (analyticTaylorSeries g))
56   · simp [h0, constantCoeff_formalExpFamily_of_zero hS0]
57   · rw [← analyticTaylorSeries_deriv, analyticTaylorSeries_congr he,
58       analyticTaylorSeries_mul hE hg.deriv, analyticTaylorSeries_deriv]
59   · simpa using derivative_formalExpFamily hS0 (1 : ℂ)
60 
61 /-- Principal logarithm gives the normalized analytic germ at zero. The
62 Taylor identity proves the full complex-parameter coefficient normalization. -/
63 def normalizedAnalyticPower (N j : ℕ) (r : ℂ) (w : ℂ) : ℂ :=
64   Complex.exp (-r * Complex.log (entireNormalizedSection N j w))
65 
66 theorem normalizedAnalyticPower_taylor {N : ℕ} (hN : 0 < N) (j : ℕ) (r : ℂ) :
67     analyticTaylorSeries (normalizedAnalyticPower N j r) = residuePowerSeries N j r := by
68   have hf : Differentiable ℂ (entireNormalizedSection N j) := fun z => (analyticAt_entireNormalizedSection hN j z).differentiableAt
69   have hL : AnalyticAt ℂ (fun z => Complex.log (entireNormalizedSection N j z)) 0 :=
70     (analyticAt_clog (by rw [entireNormalizedSection_zero]; simp)).comp (hf.analyticAt 0)
71   have hG : AnalyticAt ℂ (fun z => -r * Complex.log (entireNormalizedSection N j z)) 0 := analyticAt_const.fun_mul hL
72   change analyticTaylorSeries (fun w => Complex.exp (-r * Complex.log (entireNormalizedSection N j w))) = _
73   rw [analyticTaylorSeries_exp hG (by simp [entireNormalizedSection_zero]),
74     analyticTaylorSeries_mul analyticAt_const hL, analyticTaylorSeries_const,
75     analyticTaylorSeries_log hf (entireNormalizedSection_zero N j),
76     analyticTaylorSeries_entireNormalizedSection hN, ← normalizedResidueSectionAlg_eq_normalizedResidueSection]
77   rw [residuePowerSeries, formalExpFamily_eq_exp_subst
78       (by simp [PowerSeries.constantCoeff_logOf (constantCoeff_normalizedResidueSectionAlg (R := ℂ) N j)]),
79     formalExpFamily_eq_exp_subst (constantCoeff_normalizedResidueNegativeLog N j)]
80   simp [normalizedResidueNegativeLog]
81 
82 theorem normalizedAnalyticPower_zero_sum_bell {N : ℕ} (hN : 2 ≤ N) (j n : ℕ) (r : ℂ) :
83     analyticTaylorCoefficient (normalizedAnalyticPower N j r) n =
84       completeExponentialBell n (fun m => r * ((m-1).factorial : ℂ) *
85         zeroPowerSum (entireNormalizedSection N j) m) / (n.factorial : ℂ) := by
86   have h := residuePowerCoeff_zero_sum_bell hN j n r
87   rw [residuePowerCoeff, blockCoeff, ← normalizedAnalyticPower_taylor (by omega), analyticTaylorSeries_coeff] at h
88   have hn : ((N*n).factorial : ℂ) ≠ 0 := by exact_mod_cast (N*n).factorial_ne_zero
89   apply mul_left_cancel₀ hn
90   convert h using 1
91   ring
92 
93 end
94 end Komorebi.PaperIV

Back to source controls