SimplePoleParts.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.PoleRemoval
6 import Mathlib.Analysis.Complex.RemovableSingularity
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology Classical
12 
13 def poleNumerator (f : ℂ → ℂ) (ρ : ℂ) (r : ℕ) (t : ℂ) : ℂ :=
14   (((-ρ) * dslope f ρ (ρ * (1-t))) ^ r)⁻¹
15 
16 def canonicalPoleCoefficient (f : ℂ → ℂ) (r : ℕ) (ρ : ℂ) (ℓ : ℕ) : ℂ :=
17   analyticTaylorCoefficient (poleNumerator f ρ r) (r-ℓ)
18 
19 theorem poleNumerator_analyticAt {f : ℂ → ℂ} (hf : Differentiable ℂ f)
20     {ρ : ℂ} (hρ : ρ ≠ 0) (hd : deriv f ρ ≠ 0) (r : ℕ) : AnalyticAt ℂ (poleNumerator f ρ r) 0 := by
21   have hg : Differentiable ℂ (dslope f ρ) := differentiableOn_univ.mp
22     ((Complex.differentiableOn_dslope (s := univ) (by simp)).mpr hf.differentiableOn)
23   have ha : AnalyticAt ℂ (fun t : ℂ => (-ρ) * dslope f ρ (ρ * (1-t))) 0 := by
24     apply analyticAt_const.fun_mul
25     exact (hg.analyticAt _).comp (by fun_prop)
26   apply (ha.pow r).inv
27   change (((-ρ) * dslope f ρ (ρ * (1-(0:ℂ)))) ^ r) ≠ 0
28   simp only [sub_zero, mul_one, dslope_same]
29   exact pow_ne_zero r (mul_ne_zero (neg_ne_zero.mpr hρ) hd)
30 
31 theorem canonicalPoleCoefficient_leading (f : ℂ → ℂ) (ρ : ℂ) (r : ℕ) :
32     canonicalPoleCoefficient f r ρ r = ((-ρ * deriv f ρ) ^ r)⁻¹ := by
33   simp [canonicalPoleCoefficient, analyticTaylorCoefficient, poleNumerator, dslope_same]
34 
35 theorem poleNumerator_identity {f : ℂ → ℂ} {ρ z : ℂ} (hfρ : f ρ = 0) (hρ : ρ ≠ 0)
36     (hz : z ≠ ρ) (r : ℕ) :
37     (f z ^ r)⁻¹ = ((1-z/ρ) ^ r)⁻¹ * poleNumerator f ρ r (1-z/ρ) := by
38   have ht : 1-z/ρ ≠ 0 := by
39     intro h
40     exact hz ((div_eq_one_iff_eq hρ).mp (sub_eq_zero.mp h).symm)
41   have harg : ρ * (1 - (1-z/ρ)) = z := by field_simp; ring
42   have he : f z = (1-z/ρ) * ((-ρ) * dslope f ρ z) := by
43     have h := sub_smul_dslope_of_zero hfρ z
44     simp only [smul_eq_mul] at h
45     rw [← h]
46     field_simp
47     ring
48   rw [poleNumerator, harg, he, mul_pow, mul_inv]
49 
50 theorem polePrincipalPart_scaled (h : ℂ → ℂ) (r : ℕ) {ρ z : ℂ} (hz : 1-z/ρ ≠ 0) :
51     (1-z/ρ) ^ r * polePrincipalPart (fun _ ℓ => analyticTaylorCoefficient h (r-ℓ)) r ρ z =
52       ∑ i ∈ Finset.range r, analyticTaylorCoefficient h i * (1-z/ρ) ^ i := by
53   classical
54   unfold polePrincipalPart poleTerm
55   rw [Finset.mul_sum]
56   have he : (∑ k ∈ Finset.range r, (1-z/ρ) ^ r *
57       (analyticTaylorCoefficient h (r-(k+1)) * ((1-z/ρ) ^ (k+1))⁻¹)) =
58       ∑ k ∈ Finset.range r, analyticTaylorCoefficient h (r-1-k) * (1-z/ρ) ^ (r-1-k) := by
59     apply Finset.sum_congr rfl
60     intro k hk
61     have hk' : k+1 ≤ r := Finset.mem_range.mp hk
62     have hpow : (1-z/ρ) ^ r = (1-z/ρ) ^ (r-(k+1)) * (1-z/ρ) ^ (k+1) := by
63       rw [← pow_add, Nat.sub_add_cancel hk']
64     have hidx : r-(k+1) = r-1-k := by omega
65     rw [hpow]
66     rw [← hidx]
67     field_simp
68   rw [he]
69   exact Finset.sum_range_reflect (fun i => analyticTaylorCoefficient h i * (1-z/ρ) ^ i) r
70 
71 /-- Simple zeros produce the complete principal parts and the exact leading
72 coefficient; the local boundedness is proved from analytic Taylor division. -/
73 theorem canonicalPoleCoefficient_local_bound {f : ℂ → ℂ} (hf : Differentiable ℂ f)
74     {ρ : ℂ} (hρ : ρ ≠ 0) (hfρ : f ρ = 0) (hd : deriv f ρ ≠ 0) (r : ℕ) :
75     ∃ C : ℝ, ∀ᶠ z in 𝓝[≠] ρ,
76       ‖(f z ^ r)⁻¹ - polePrincipalPart (canonicalPoleCoefficient f r) r ρ z‖ ≤ C := by
77   let h := poleNumerator f ρ r
78   obtain ⟨F, hF, he⟩ := (poleNumerator_analyticAt hf hρ hd r).exists_eventuallyEq_sum_add_pow_mul r
79   have ht : Tendsto (fun z : ℂ => 1-z/ρ) (𝓝[≠] ρ) (𝓝 0) := by
80     have hc : ContinuousAt (fun z : ℂ => 1-z/ρ) ρ := by fun_prop
81     simpa [hρ] using hc.tendsto.mono_left nhdsWithin_le_nhds
82   have hbound : ∀ᶠ z in 𝓝[≠] ρ, ‖F (1-z/ρ)‖ ≤ ‖F 0‖ + 1 :=
83     (hF.continuousAt.norm.tendsto.comp ht).eventually (eventually_le_nhds (by linarith))
84   refine ⟨‖F 0‖+1, ?_⟩
85   filter_upwards [ht.eventually he, hbound, self_mem_nhdsWithin] with z hz hb hzρ
86   have hzne : z ≠ ρ := hzρ
87   have htz : 1-z/ρ ≠ 0 := by
88     intro hh
89     exact hzne ((div_eq_one_iff_eq hρ).mp (sub_eq_zero.mp hh).symm)
90   have hp := polePrincipalPart_scaled h r htz
91   have hpc : (1-z/ρ) ^ r * polePrincipalPart (canonicalPoleCoefficient f r) r ρ z =
92       ∑ i ∈ Finset.range r, analyticTaylorCoefficient h i * (1-z/ρ) ^ i := by
93     simpa only [polePrincipalPart, canonicalPoleCoefficient, h] using hp
94   have hh : (f z ^ r)⁻¹ - polePrincipalPart (canonicalPoleCoefficient f r) r ρ z = F (1-z/ρ) := by
95     rw [poleNumerator_identity hfρ hρ hzne r, hz]
96     simp only [smul_eq_mul]
97     have hsum : (∑ i ∈ Finset.range r, ((1-z/ρ) ^ i / (i.factorial : ℂ)) * iteratedDeriv i (poleNumerator f ρ r) 0) =
98         (1-z/ρ) ^ r * polePrincipalPart (canonicalPoleCoefficient f r) r ρ z := by
99       rw [hpc]
100       apply Finset.sum_congr rfl
101       intro i _
102       dsimp [analyticTaylorCoefficient, h]
103       ring
104     rw [hsum]
105     field_simp
106     ring
107   rw [hh]
108   exact hb
109 
110 end
111 end Komorebi.PaperIV

Back to source controls