AnalyticTaylorAlgebra.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.PoleCoefficientBounds
6 import Mathlib.RingTheory.PowerSeries.Basic
7 import Mathlib.Analysis.Analytic.IteratedFDeriv
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Filter
12 open scoped Topology
13 
14 def analyticTaylorSeries (f : ℂ → ℂ) : PowerSeries ℂ := PowerSeries.mk (analyticTaylorCoefficient f)
15 
16 @[simp] theorem analyticTaylorSeries_coeff (f : ℂ → ℂ) (n : ℕ) :
17     PowerSeries.coeff n (analyticTaylorSeries f) = analyticTaylorCoefficient f n := by
18   simp [analyticTaylorSeries]
19 
20 @[simp] theorem analyticTaylorSeries_constantCoeff (f : ℂ → ℂ) :
21     (analyticTaylorSeries f).constantCoeff = f 0 := by simp [analyticTaylorSeries, analyticTaylorCoefficient]
22 
23 theorem analyticTaylorSeries_congr {f g : ℂ → ℂ} (h : f =ᶠ[𝓝 0] g) :
24     analyticTaylorSeries f = analyticTaylorSeries g := by
25   ext n
26   simp only [analyticTaylorSeries_coeff, analyticTaylorCoefficient, h.iteratedDeriv_eq n]
27 
28 theorem analyticTaylorSeries_mul {f g : ℂ → ℂ} (hf : AnalyticAt ℂ f 0) (hg : AnalyticAt ℂ g 0) :
29     analyticTaylorSeries (fun z => f z * g z) = analyticTaylorSeries f * analyticTaylorSeries g := by
30   ext n
31   rw [analyticTaylorSeries_coeff, analyticTaylorCoefficient,
32     iteratedDeriv_fun_mul hf.contDiffAt hg.contDiffAt, PowerSeries.coeff_mul,
33     Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Finset.sum_div]
34   apply Finset.sum_congr rfl
35   intro k hk
36   have hkn : k ≤ n := Nat.le_of_lt_succ (Finset.mem_range.mp hk)
37   have hfac : (n.choose k : ℂ) * (k.factorial : ℂ) * ((n - k).factorial : ℂ) = n.factorial := by
38     exact_mod_cast Nat.choose_mul_factorial_mul_factorial hkn
39   simp only [analyticTaylorSeries_coeff, analyticTaylorCoefficient]
40   have hn : (n.factorial : ℂ) ≠ 0 := by exact_mod_cast n.factorial_ne_zero
41   have hk0 : (k.factorial : ℂ) ≠ 0 := by exact_mod_cast k.factorial_ne_zero
42   have hnk : ((n-k).factorial : ℂ) ≠ 0 := by exact_mod_cast (n-k).factorial_ne_zero
43   field_simp
44   linear_combination (iteratedDeriv k f 0 * iteratedDeriv (n-k) g 0) * hfac
45 
46 theorem analyticTaylorSeries_add {f g : ℂ → ℂ} (hf : AnalyticAt ℂ f 0) (hg : AnalyticAt ℂ g 0) :
47     analyticTaylorSeries (fun z => f z + g z) = analyticTaylorSeries f + analyticTaylorSeries g := by
48   ext n
49   simp [analyticTaylorCoefficient, iteratedDeriv_fun_add hf.contDiffAt hg.contDiffAt, add_div]
50 
51 @[simp] theorem analyticTaylorSeries_const (c : ℂ) :
52     analyticTaylorSeries (fun _ => c) = PowerSeries.C c := by
53   ext n
54   cases n with
55   | zero => simp [analyticTaylorCoefficient]
56   | succ n => simp [analyticTaylorCoefficient, iteratedDeriv_const]
57 
58 theorem analyticTaylorSeries_pow {f : ℂ → ℂ} (hf : AnalyticAt ℂ f 0) (r : ℕ) :
59     analyticTaylorSeries (fun z => f z ^ r) = analyticTaylorSeries f ^ r := by
60   induction r with
61   | zero => simp
62   | succ r ih => simp_rw [pow_succ]; rw [analyticTaylorSeries_mul (f := fun z => f z ^ r) (by fun_prop) hf, ih]
63 
64 theorem analyticTaylorSeries_inverse_product {f : ℂ → ℂ} (hf : AnalyticAt ℂ f 0) (h0 : f 0 ≠ 0) :
65     analyticTaylorSeries f * analyticTaylorSeries (fun z => (f z)⁻¹) = 1 := by
66   rw [← analyticTaylorSeries_mul (g := fun z => (f z)⁻¹) hf (by fun_prop)]
67   have h : (fun z => f z * (f z)⁻¹) =ᶠ[𝓝 0] (fun _ => (1 : ℂ)) := by
68     filter_upwards [hf.continuousAt.eventually_ne h0] with z hz
69     exact mul_inv_cancel₀ hz
70   rw [analyticTaylorSeries_congr h]
71   simp
72 
73 end
74 end Komorebi.PaperIV

Back to source controls