LeadingPoleBounds.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.NearestPoleExpansion
6 import KomorebiPaperIV.SimplePoleParts
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology Classical
12 
13 def principalCoefficientSum (S : Finset ℂ) (a : ℂ → ℕ → ℂ) (r m : ℕ) : ℂ :=
14   ∑ ρ ∈ S, ∑ k ∈ Finset.range r, a ρ (k+1) * ((m+k).choose k : ℂ) * ρ⁻¹ ^ m
15 
16 def leadingPoleCoefficient (S : Finset ℂ) (a : ℂ → ℕ → ℂ) (r m : ℕ) : ℂ :=
17   ((m+r-1).choose (r-1) : ℂ) * ∑ ρ ∈ S, a ρ r * ρ⁻¹ ^ m
18 
19 def lowerPrincipalConstant (S : Finset ℂ) (a : ℂ → ℕ → ℂ) (r : ℕ) : ℝ :=
20   ∑ ρ ∈ S, ∑ k ∈ Finset.range (r-1), ‖a ρ (k+1)‖ * (k+1 : ℝ) ^ k
21 
22 theorem lowerPrincipalConstant_nonneg (S : Finset ℂ) (a : ℂ → ℕ → ℂ) (r : ℕ) :
23     0 ≤ lowerPrincipalConstant S a r := by unfold lowerPrincipalConstant; positivity
24 
25 @[simp] theorem lowerPrincipalConstant_one (S : Finset ℂ) (a : ℂ → ℕ → ℂ) :
26     lowerPrincipalConstant S a 1 = 0 := by simp [lowerPrincipalConstant]
27 
28 theorem principalCoefficientSum_split (S : Finset ℂ) (a : ℂ → ℕ → ℂ) {r : ℕ} (hr : 0 < r) (m : ℕ) :
29     principalCoefficientSum S a r m - leadingPoleCoefficient S a r m =
30       ∑ ρ ∈ S, ∑ k ∈ Finset.range (r-1), a ρ (k+1) * ((m+k).choose k : ℂ) * ρ⁻¹ ^ m := by
31   obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hr.ne'
32   simp only [principalCoefficientSum, leadingPoleCoefficient, Nat.succ_sub_one,
33     Nat.add_succ_sub_one, Finset.sum_range_succ, Finset.sum_add_distrib, Finset.mul_sum]
34   have he : (∑ ρ ∈ S, a ρ (s+1) * ((m+s).choose s : ℂ) * ρ⁻¹ ^ m) =
35       ∑ ρ ∈ S, ((m+s).choose s : ℂ) * (a ρ (s+1) * ρ⁻¹ ^ m) := by
36     apply Finset.sum_congr rfl
37     intro ρ _
38     ring
39   rw [he, add_sub_cancel_right]
40 
41 theorem principalCoefficientSum_leading_error {S : Finset ℂ} {R : ℝ}
42     (hR : 0 < R) (hS : ∀ ρ ∈ S, ‖ρ‖ = R) (a : ℂ → ℕ → ℂ)
43     {r : ℕ} (hr : 0 < r) {m : ℕ} (hm : 1 ≤ m) :
44     ‖principalCoefficientSum S a r m - leadingPoleCoefficient S a r m‖ ≤
45       lowerPrincipalConstant S a r * (m : ℝ) ^ (r-2) * R⁻¹ ^ m := by
46   rw [principalCoefficientSum_split S a hr m]
47   calc
48     _ ≤ ∑ ρ ∈ S, ‖∑ k ∈ Finset.range (r-1), a ρ (k+1) * ((m+k).choose k : ℂ) * ρ⁻¹ ^ m‖ := norm_sum_le _ _
49     _ ≤ ∑ ρ ∈ S, ∑ k ∈ Finset.range (r-1), ‖a ρ (k+1) * ((m+k).choose k : ℂ) * ρ⁻¹ ^ m‖ :=
50       Finset.sum_le_sum (fun ρ _ => norm_sum_le _ _)
51     _ ≤ ∑ ρ ∈ S, ∑ k ∈ Finset.range (r-1),
52         (‖a ρ (k+1)‖ * (k+1 : ℝ) ^ k) * (m : ℝ) ^ (r-2) * R⁻¹ ^ m := by
53       apply Finset.sum_le_sum
54       intro ρ hρ
55       apply Finset.sum_le_sum
56       intro k hk
57       have hk' : k+1 < r := by have := Finset.mem_range.mp hk; omega
58       have hn : ((m+k).choose k : ℝ) ≤ (k+1 : ℝ) ^ k * (m : ℝ) ^ (r-2) := by
59         exact_mod_cast (by simpa using lower_principal_part_choose_bound hm (by omega : 1 ≤ k+1) hk')
60       simp only [norm_mul, Complex.norm_natCast, norm_pow, norm_inv, hS ρ hρ]
61       have hh := mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hn (norm_nonneg (a ρ (k+1))))
62         (pow_nonneg (inv_nonneg.mpr hR.le) m)
63       simpa only [mul_assoc] using hh
64     _ = _ := by simp only [lowerPrincipalConstant, Finset.sum_mul]
65 
66 /-- The lower-order error vanishes identically for simple reciprocal poles. -/
67 theorem principalCoefficientSum_one (S : Finset ℂ) (a : ℂ → ℕ → ℂ) (m : ℕ) :
68     principalCoefficientSum S a 1 m = leadingPoleCoefficient S a 1 m := by
69   simpa using (sub_eq_zero.mp (by simpa using principalCoefficientSum_split S a (by norm_num : 0 < 1) m))
70 
71 /-- Leading-pole expansion, with both error bounds and the r=1 boundary explicit. -/
72 theorem reciprocalCoeff_leading_bound {N : ℕ} (hN : 0 < N)
73     {S : Finset ℂ} {R Rstar R₂ : ℝ} (hR : 0 < R) (hRR : R < Rstar) (hR₂ : Rstar < R₂)
74     (hS : ∀ ρ ∈ S, ‖ρ‖ = R) (hroot : ∀ ρ ∈ S, canonicalSignedDenominator N ρ = 0)
75     (hsimple : ∀ ρ ∈ S, deriv (canonicalSignedDenominator N) ρ ≠ 0)
76     (hzeros : ∀ z : ℂ, ‖z‖ < R₂ → canonicalSignedDenominator N z = 0 → z ∈ S)
77     {r : ℕ} (hr : 0 < r) :
78     ∃ C : ℝ, ∀ n : ℕ, 1 ≤ n →
79       ‖reciprocalCoeff N n (r : ℂ) - ((N*n).factorial : ℂ) *
80         leadingPoleCoefficient S (canonicalPoleCoefficient (canonicalSignedDenominator N) r) r (N*n)‖ ≤
81       lowerPrincipalConstant S (canonicalPoleCoefficient (canonicalSignedDenominator N) r) r *
82         ((N*n).factorial : ℝ) * (N*n : ℝ) ^ (r-2) * R⁻¹ ^ (N*n) +
83       C * ((N*n).factorial : ℝ) * Rstar⁻¹ ^ (N*n) := by
84   have hf : Differentiable ℂ (canonicalSignedDenominator N) := fun z => (analyticAt_entireSigned ..).differentiableAt
85   have hS0 (ρ : ℂ) (hρ : ρ ∈ S) : ρ ≠ 0 := by
86     intro he
87     have := hS ρ hρ
88     rw [he, norm_zero] at this
89     linarith
90   let a := canonicalPoleCoefficient (canonicalSignedDenominator N) r
91   obtain ⟨C, hC⟩ := reciprocalCoeff_nearest_pole_bound hN hS0 a r (hR.trans hRR) hR₂ hzeros
92     (fun ρ hρ => canonicalPoleCoefficient_local_bound hf (hS0 ρ hρ) (hroot ρ hρ) (hsimple ρ hρ) r)
93   refine ⟨C, fun n hn => ?_⟩
94   have hm : 1 ≤ N*n := Nat.mul_pos hN (by omega)
95   have he := principalCoefficientSum_leading_error hR hS a hr hm
96   have hsplit : reciprocalCoeff N n (r : ℂ) - ((N*n).factorial : ℂ) * leadingPoleCoefficient S a r (N*n) =
97       ((N*n).factorial : ℂ) * (principalCoefficientSum S a r (N*n) - leadingPoleCoefficient S a r (N*n)) +
98       (reciprocalCoeff N n (r : ℂ) - ((N*n).factorial : ℂ) * principalCoefficientSum S a r (N*n)) := by ring
99   rw [hsplit]
100   apply (norm_add_le _ _).trans
101   rw [norm_mul, Complex.norm_natCast]
102   have hh := add_le_add (mul_le_mul_of_nonneg_left he (show (0 : ℝ) ≤ (N*n).factorial by positivity)) (hC n)
103   simpa only [principalCoefficientSum, Nat.cast_mul, mul_assoc, mul_comm, mul_left_comm] using hh
104 
105 end
106 end Komorebi.PaperIV

Back to source controls