AnalyticTaylorDifferential.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.AnalyticTaylorAlgebra
6 import KomorebiPaperIV.ThetaZeroBell
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 theorem analyticTaylorSeries_neg (f : ℂ → ℂ) :
14     analyticTaylorSeries (fun z => -f z) = -analyticTaylorSeries f := by
15   ext n
16   simp [analyticTaylorCoefficient, iteratedDeriv_fun_neg, neg_div]
17 
18 theorem analyticTaylorSeries_deriv (f : ℂ → ℂ) :
19     analyticTaylorSeries (deriv f) = PowerSeries.derivative ℂ (analyticTaylorSeries f) := by
20   ext n
21   rw [analyticTaylorSeries_coeff, analyticTaylorCoefficient, ← iteratedDeriv_succ',
22     PowerSeries.coeff_derivative, analyticTaylorSeries_coeff, analyticTaylorCoefficient]
23   rw [Nat.factorial_succ, Nat.cast_mul]
24   have hn : (n.factorial : ℂ) ≠ 0 := by exact_mod_cast n.factorial_ne_zero
25   have hn1 : (n.succ : ℂ) ≠ 0 := by exact_mod_cast n.succ_ne_zero
26   field_simp
27   simp
28 
29 theorem analyticTaylorSeries_zeroResolvent {f : ℂ → ℂ} (hf : Differentiable ℂ f)
30     (hs : ZeroPowerSummable f 1) (h0 : f 0 ≠ 0) :
31     analyticTaylorSeries (fun w => ∑' i, zeroPartialFraction f i w) = zeroMomentSeries f := by
32   ext n
33   rw [analyticTaylorSeries_coeff, analyticTaylorCoefficient, zeroPowerSum_resolvent_derivative hf hs h0]
34   simp [zeroMomentSeries, Nat.factorial_ne_zero]
35 
36 /-- Formal logarithmic differentiation of a proved analytic product, with
37 Taylor coefficients derived from the actual function. -/
38 theorem hadamard_taylor_zeroMoment_identity {f : ℂ → ℂ} (hf : Differentiable ℂ f)
39     (hs : ZeroPowerSummable f 1) (h0 : f 0 ≠ 0) (hP : f = fullCanonicalProduct f) :
40     analyticTaylorSeries f * zeroMomentSeries f = -PowerSeries.derivative ℂ (analyticTaylorSeries f) := by
41   let G : ℂ → ℂ := fun w => ∑' i, zeroPartialFraction f i w
42   have hG : AnalyticAt ℂ G 0 := zeroResolvent_analyticAt_zero hf hs h0
43   have hnear : (fun w => f w * G w) =ᶠ[𝓝 0] (fun w => -deriv f w) := by
44     filter_upwards [hf.continuous.continuousAt.eventually_ne h0] with w hw
45     have h := fullCanonicalProduct_logDeriv hs h0 (w := w) (fun i he => hw (he ▸ i.1.property))
46     have he : logDeriv f w = logDeriv (fullCanonicalProduct f) w := congrArg (fun F => logDeriv F w) hP
47     rw [← he] at h
48     change -logDeriv f w = G w at h
49     rw [← h, logDeriv_apply]
50     field_simp
51   calc
52     _ = analyticTaylorSeries f * analyticTaylorSeries G := by rw [analyticTaylorSeries_zeroResolvent hf hs h0]
53     _ = analyticTaylorSeries (fun w => f w * G w) := (analyticTaylorSeries_mul (hf.analyticAt 0) hG).symm
54     _ = analyticTaylorSeries (fun w => -deriv f w) := analyticTaylorSeries_congr hnear
55     _ = _ := by rw [analyticTaylorSeries_neg, analyticTaylorSeries_deriv]
56 
57 end
58 end Komorebi.PaperIV

Back to source controls