PoleTaylor.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.PoleRemoval
6 import KomorebiPaperIV.CompanionCompletion
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology Classical
12 
13 theorem analyticTaylorSeries_sub {f g : ℂ → ℂ} (hf : AnalyticAt ℂ f 0) (hg : AnalyticAt ℂ g 0) :
14     analyticTaylorSeries (fun z => f z - g z) = analyticTaylorSeries f - analyticTaylorSeries g := by
15   simp only [sub_eq_add_neg]
16   rw [analyticTaylorSeries_add (g := fun z => -g z) hf (by fun_prop), analyticTaylorSeries_neg]
17 
18 theorem analyticTaylorSeries_finsetSum {ι : Type*} (S : Finset ι) {f : ι → ℂ → ℂ}
19     (hf : ∀ i ∈ S, AnalyticAt ℂ (f i) 0) :
20     analyticTaylorSeries (fun z => ∑ i ∈ S, f i z) = ∑ i ∈ S, analyticTaylorSeries (f i) := by
21   induction S using Finset.induction_on with
22   | empty => simp
23   | @insert i S hi ih =>
24     simp only [Finset.sum_insert hi]
25     rw [analyticTaylorSeries_add (hf i (Finset.mem_insert_self i S))
26       (Finset.analyticAt_fun_sum _ (fun k hk => hf k (Finset.mem_insert_of_mem hk))),
27       ih (fun k hk => hf k (Finset.mem_insert_of_mem hk))]
28 
29 theorem analyticTaylorSeries_id : analyticTaylorSeries (fun z : ℂ => z) = PowerSeries.X := by
30   ext n
31   cases n with
32   | zero => simp [analyticTaylorCoefficient]
33   | succ n =>
34     simp [analyticTaylorCoefficient, iteratedDeriv_fun_id, PowerSeries.coeff_X]
35     split_ifs <;> simp_all
36 
37 theorem analyticTaylorSeries_poleTerm (ρ : ℂ) (ℓ : ℕ) :
38     analyticTaylorSeries (poleTerm ρ ℓ) = principalPartSeries ρ ℓ := by
39   have hb : AnalyticAt ℂ (fun z : ℂ => 1 - z / ρ) 0 := by fun_prop
40   have he : analyticTaylorSeries (fun z : ℂ => 1 - z / ρ) = 1 - PowerSeries.C ρ⁻¹ * PowerSeries.X := by
41     simp_rw [div_eq_mul_inv, mul_comm _ ρ⁻¹]
42     rw [analyticTaylorSeries_sub (g := fun z => ρ⁻¹ * z) analyticAt_const (by fun_prop),
43       analyticTaylorSeries_mul (f := fun _ => ρ⁻¹) (g := fun z => z) analyticAt_const analyticAt_id, analyticTaylorSeries_const,
44       analyticTaylorSeries_const, analyticTaylorSeries_id]
45     simp
46   have hi := analyticTaylorSeries_inverse_product (f := fun z => (1 - z / ρ) ^ ℓ)
47     (hb.pow ℓ) (by simp)
48   rw [analyticTaylorSeries_pow hb, he] at hi
49   have hu : IsUnit ((1 - PowerSeries.C ρ⁻¹ * PowerSeries.X) ^ ℓ) :=
50     PowerSeries.isUnit_iff_constantCoeff.mpr (by simp)
51   apply hu.mul_left_cancel
52   exact hi.trans (by rw [mul_comm]; exact (principalPartSeries_inverse ρ ℓ).symm)
53 
54 theorem analyticTaylorCoefficient_principalPart {ρ : ℂ} (hρ : ρ ≠ 0)
55     (a : ℂ → ℕ → ℂ) (r m : ℕ) :
56     analyticTaylorCoefficient (polePrincipalPart a r ρ) m =
57       ∑ k ∈ Finset.range r, a ρ (k + 1) * ((m + k).choose k : ℂ) * ρ⁻¹ ^ m := by
58   have ha (k : ℕ) : AnalyticAt ℂ (poleTerm ρ (k+1)) 0 := poleTerm_analyticAt hρ hρ.symm (k+1)
59   rw [← analyticTaylorSeries_coeff (polePrincipalPart a r ρ) m]
60   change PowerSeries.coeff m (analyticTaylorSeries (fun z => ∑ k ∈ Finset.range r,
61     a ρ (k+1) * poleTerm ρ (k+1) z)) = _
62   rw [analyticTaylorSeries_finsetSum _ (fun k _ => analyticAt_const.fun_mul (ha k)), map_sum]
63   apply Finset.sum_congr rfl
64   intro k _
65   rw [analyticTaylorSeries_mul analyticAt_const (ha k), analyticTaylorSeries_const,
66     analyticTaylorSeries_poleTerm, PowerSeries.coeff_C_mul,
67     principalPartSeries_coefficient ρ (Nat.succ_pos k)]
68   simp only [Nat.succ_sub_one, Nat.add_succ_sub_one, mul_assoc]
69 
70 theorem analyticTaylorSeries_canonicalSignedDenominator {N : ℕ} (hN : 0 < N) :
71     analyticTaylorSeries (canonicalSignedDenominator N) = signedSection (R := ℂ) N 0 := by
72   ext n
73   rw [analyticTaylorSeries_coeff, analyticTaylorCoefficient]
74   rw [iteratedDeriv_eq_iterate]
75   unfold canonicalSignedDenominator
76   rw [entireSigned_derivative_at_zero hN hN (canonicalPrimitiveRoot_isPrimitive hN) (canonicalSignedRoot_pow hN)]
77   simp [Nat.factorial_ne_zero]
78 
79 theorem reciprocalSeries_nat (N r : ℕ) : reciprocalSeries (R := ℂ) N (r : ℂ) = reciprocalSeries N 1 ^ r := by
80   induction r with
81   | zero => simp [reciprocalSeries_zero]
82   | succ r ih => rw [Nat.cast_add, Nat.cast_one, ← reciprocalSeries_add, ih, pow_succ]
83 
84 theorem analyticTaylorSeries_reciprocal_signed {N : ℕ} (hN : 0 < N) (r : ℕ) :
85     analyticTaylorSeries (fun z => (canonicalSignedDenominator N z ^ r)⁻¹) =
86       PowerSeries.expand N hN.ne' (reciprocalSeries N (r : ℂ)) := by
87   have hf : AnalyticAt ℂ (canonicalSignedDenominator N) 0 := analyticAt_entireSigned ..
88   have hi := analyticTaylorSeries_inverse_product (f := fun z => canonicalSignedDenominator N z ^ r)
89     (hf.pow r) (by rw [canonicalSignedDenominator_zero hN]; simp)
90   rw [analyticTaylorSeries_pow hf, analyticTaylorSeries_canonicalSignedDenominator hN,
91     signedSection_zero_eq_expand_reducedDenominator hN] at hi
92   have he : PowerSeries.expand N hN.ne' (reciprocalSeries N (r : ℂ)) *
93       (PowerSeries.expand N hN.ne' (reducedDenominator N)) ^ r = 1 := by
94     rw [reciprocalSeries_nat, ← map_pow, ← map_mul, ← mul_pow,
95       ← reciprocalSeries_neg_one (R := ℂ) N, reciprocalSeries_add]
96     simp [reciprocalSeries_zero]
97   have hu : IsUnit ((PowerSeries.expand N hN.ne' (reducedDenominator (R := ℂ) N)) ^ r) :=
98     PowerSeries.isUnit_iff_constantCoeff.mpr (by simp)
99   exact hu.mul_left_cancel (hi.trans (by rw [mul_comm]; exact he.symm))
100 
101 /-- The actual analytic reciprocal has the manuscript's exact factorial-scaled coefficients. -/
102 theorem reciprocalCoeff_analyticTaylor {N : ℕ} (hN : 0 < N) (n r : ℕ) :
103     reciprocalCoeff N n (r : ℂ) = ((N*n).factorial : ℂ) *
104       analyticTaylorCoefficient (fun z => (canonicalSignedDenominator N z ^ r)⁻¹) (N*n) := by
105   rw [← analyticTaylorSeries_coeff]
106   rw [analyticTaylorSeries_reciprocal_signed hN, PowerSeries.coeff_expand_mul]
107   rfl
108 
109 end
110 end Komorebi.PaperIV

Back to source controls