NearestPoleExpansion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.PoleTaylor
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter Metric
10 open scoped Topology Classical
11 
12 theorem removedPoleRemainder_taylor {f : ℂ → ℂ} (hf : Differentiable ℂ f) (hf0 : f 0 ≠ 0)
13     {S : Finset ℂ} (hS : ∀ ρ ∈ S, ρ ≠ 0) (a : ℂ → ℕ → ℂ) (r m : ℕ) :
14     analyticTaylorCoefficient (removedPoleRemainder f S a r) m =
15       analyticTaylorCoefficient (fun z => (f z ^ r)⁻¹) m -
16         ∑ ρ ∈ S, ∑ k ∈ Finset.range r, a ρ (k+1) * ((m+k).choose k : ℂ) * ρ⁻¹ ^ m := by
17   have h0 : (0 : ℂ) ∉ S := fun h => hS 0 h rfl
18   have hnear : removedPoleRemainder f S a r =ᶠ[𝓝 0] rawPoleRemainder f S a r := by
19     filter_upwards [hf.continuous.continuousAt.eventually_ne hf0,
20       S.finite_toSet.isClosed.isOpen_compl.mem_nhds h0] with z hz hzs
21     exact removedPoleRemainder_eq_raw hf hS a r hz hzs
22   have hp (ρ : ℂ) (hρ : ρ ∈ S) : AnalyticAt ℂ (polePrincipalPart a r ρ) 0 :=
23     polePrincipalPart_analyticAt (hS ρ hρ) (hS ρ hρ).symm a r
24   rw [← analyticTaylorSeries_coeff]
25   rw [analyticTaylorSeries_congr hnear]
26   change PowerSeries.coeff m (analyticTaylorSeries (fun z => (f z ^ r)⁻¹ -
27     ∑ ρ ∈ S, polePrincipalPart a r ρ z)) = _
28   rw [
29     analyticTaylorSeries_sub (f := fun z => (f z ^ r)⁻¹)
30       (by simpa only using! (((hf.analyticAt 0).pow r).inv (pow_ne_zero r hf0)))
31       (Finset.analyticAt_fun_sum _ hp),
32     analyticTaylorSeries_finsetSum S hp, map_sub, map_sum, analyticTaylorSeries_coeff]
33   congr 1
34   apply Finset.sum_congr rfl
35   intro ρ hρ
36   simpa only [analyticTaylorSeries_coeff] using analyticTaylorCoefficient_principalPart (hS ρ hρ) a r m
37 
38 /-- The complete finite principal-part expansion with an explicit Cauchy
39 constant, valid for every coefficient. The local O(1) assumptions are exactly
40 the meaning of the principal parts specified in Theorem 13.1. -/
41 theorem nearest_pole_taylor_bound {f : ℂ → ℂ} (hf : Differentiable ℂ f) (hf0 : f 0 ≠ 0)
42     {S : Finset ℂ} (hS : ∀ ρ ∈ S, ρ ≠ 0) (a : ℂ → ℕ → ℂ) (r : ℕ)
43     {R R₂ : ℝ} (hR : 0 < R) (hR₂ : R < R₂)
44     (hzeros : ∀ z : ℂ, ‖z‖ < R₂ → f z = 0 → z ∈ S)
45     (hlocal : ∀ ρ ∈ S, ∃ C : ℝ, ∀ᶠ z in 𝓝[≠] ρ,
46       ‖(f z ^ r)⁻¹ - polePrincipalPart a r ρ z‖ ≤ C) :
47     ∃ C : ℝ, ∀ m : ℕ,
48       ‖analyticTaylorCoefficient (fun z => (f z ^ r)⁻¹) m -
49         ∑ ρ ∈ S, ∑ k ∈ Finset.range r, a ρ (k+1) * ((m+k).choose k : ℂ) * ρ⁻¹ ^ m‖ ≤ C / R ^ m := by
50   let H := removedPoleRemainder f S a r
51   have hH : AnalyticOnNhd ℂ H (ball 0 R₂) := removedPoleRemainder_analyticOnNhd hf hS a r
52     (fun z hz => hzeros z (mem_ball_zero_iff.mp hz)) hlocal
53   have hdiff : DiffContOnCl ℂ H (ball 0 R) := hH.differentiableOn.diffContOnCl_ball
54     (fun z hz => mem_ball_zero_iff.mpr ((mem_closedBall_zero_iff.mp hz).trans_lt hR₂))
55   have hc : ContinuousOn H (sphere 0 R) := hH.continuousOn.mono
56     (fun z hz => mem_ball_zero_iff.mpr ((by simpa only [mem_sphere, dist_zero_right] using hz : ‖z‖ = R).trans_lt hR₂))
57   obtain ⟨C, hC⟩ := (isCompact_sphere (0 : ℂ) R).bddAbove_image hc.norm
58   refine ⟨C, fun m => ?_⟩
59   rw [← removedPoleRemainder_taylor hf hf0 hS a r m]
60   exact analyticTaylorCoefficient_norm_le hR hdiff (fun z hz => hC (mem_image_of_mem _ hz)) m
61 
62 theorem reciprocalCoeff_nearest_pole_bound {N : ℕ} (hN : 0 < N)
63     {S : Finset ℂ} (hS : ∀ ρ ∈ S, ρ ≠ 0) (a : ℂ → ℕ → ℂ) (r : ℕ)
64     {R R₂ : ℝ} (hR : 0 < R) (hR₂ : R < R₂)
65     (hzeros : ∀ z : ℂ, ‖z‖ < R₂ → canonicalSignedDenominator N z = 0 → z ∈ S)
66     (hlocal : ∀ ρ ∈ S, ∃ C : ℝ, ∀ᶠ z in 𝓝[≠] ρ,
67       ‖(canonicalSignedDenominator N z ^ r)⁻¹ - polePrincipalPart a r ρ z‖ ≤ C) :
68     ∃ C : ℝ, ∀ n : ℕ,
69       ‖reciprocalCoeff N n (r : ℂ) - ((N*n).factorial : ℂ) *
70         ∑ ρ ∈ S, ∑ k ∈ Finset.range r, a ρ (k+1) * ((N*n+k).choose k : ℂ) * ρ⁻¹ ^ (N*n)‖ ≤
71       C * ((N*n).factorial : ℝ) * R⁻¹ ^ (N*n) := by
72   have hf : Differentiable ℂ (canonicalSignedDenominator N) := fun z => (analyticAt_entireSigned ..).differentiableAt
73   obtain ⟨C, hC⟩ := nearest_pole_taylor_bound hf (by rw [canonicalSignedDenominator_zero hN]; exact one_ne_zero)
74     hS a r hR hR₂ hzeros hlocal
75   refine ⟨C, fun n => ?_⟩
76   rw [reciprocalCoeff_analyticTaylor hN, ← mul_sub, norm_mul, Complex.norm_natCast]
77   have h := mul_le_mul_of_nonneg_left (hC (N*n)) (show (0 : ℝ) ≤ (N*n).factorial by positivity)
78   simpa only [div_eq_mul_inv, inv_pow, mul_assoc, mul_comm, mul_left_comm] using h
79 
80 end
81 end Komorebi.PaperIV

Back to source controls