PrincipalPartUniqueness.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SimplePoleParts
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter
10 open scoped Topology Classical
11 
12 theorem polePrincipalPart_scaled_general (a : ℂ → ℕ → ℂ) (r : ℕ) {ρ z : ℂ} (hz : 1-z/ρ ≠ 0) :
13     (1-z/ρ) ^ r * polePrincipalPart a r ρ z =
14       ∑ k ∈ Finset.range r, a ρ (k+1) * (1-z/ρ) ^ (r-1-k) := by
15   unfold polePrincipalPart poleTerm
16   rw [Finset.mul_sum]
17   apply Finset.sum_congr rfl
18   intro k hk
19   have hk' : k+1 ≤ r := Finset.mem_range.mp hk
20   have hpow : (1-z/ρ) ^ r = (1-z/ρ) ^ (r-(k+1)) * (1-z/ρ) ^ (k+1) := by
21     rw [← pow_add, Nat.sub_add_cancel hk']
22   rw [hpow, show r-1-k = r-(k+1) by omega]
23   field_simp
24 
25 theorem polePrincipalPart_scaled_limit (a : ℂ → ℕ → ℂ) {r : ℕ} (hr : 0 < r)
26     {ρ : ℂ} (hρ : ρ ≠ 0) :
27     Tendsto (fun z => (1-z/ρ) ^ r * polePrincipalPart a r ρ z) (𝓝[≠] ρ) (𝓝 (a ρ r)) := by
28   let P : ℂ → ℂ := fun z => ∑ k ∈ Finset.range r, a ρ (k+1) * (1-z/ρ) ^ (r-1-k)
29   have hc : ContinuousAt P ρ := by dsimp [P]; fun_prop
30   have heval : P ρ = a ρ r := by
31     simp only [P, div_self hρ, sub_self]
32     rw [Finset.sum_eq_single (r-1)]
33     · simp [show r-1+1 = r by omega]
34     · intro k hk hkne
35       have hpow : r-1-k ≠ 0 := by have := Finset.mem_range.mp hk; omega
36       simp [hpow]
37     · intro hn
38       exact (hn (Finset.mem_range.mpr (by omega))).elim
39   have hlim : Tendsto P (𝓝[≠] ρ) (𝓝 (P ρ)) := hc.tendsto.mono_left nhdsWithin_le_nhds
40   rw [heval] at hlim
41   apply hlim.congr'
42   filter_upwards [self_mem_nhdsWithin] with z hz
43   have ht : 1-z/ρ ≠ 0 := by
44     intro h
45     exact hz ((div_eq_one_iff_eq hρ).mp (sub_eq_zero.mp h).symm)
46   exact (polePrincipalPart_scaled_general a r ht).symm
47 
48 /-- Any principal part satisfying the manuscript's O(1) condition has the
49 same leading Laurent coefficient as the constructed analytic principal part. -/
50 theorem principalPart_leading_coefficient {f : ℂ → ℂ} (hf : Differentiable ℂ f)
51     {ρ : ℂ} (hρ : ρ ≠ 0) (hfρ : f ρ = 0) (hd : deriv f ρ ≠ 0)
52     {r : ℕ} (hr : 0 < r) (a : ℂ → ℕ → ℂ)
53     (hb : ∃ C : ℝ, ∀ᶠ z in 𝓝[≠] ρ, ‖(f z ^ r)⁻¹ - polePrincipalPart a r ρ z‖ ≤ C) :
54     a ρ r = ((-ρ * deriv f ρ) ^ r)⁻¹ := by
55   have ht : Tendsto (fun z : ℂ => 1-z/ρ) (𝓝[≠] ρ) (𝓝 0) := by
56     have hc : ContinuousAt (fun z : ℂ => 1-z/ρ) ρ := by fun_prop
57     simpa [hρ] using hc.tendsto.mono_left nhdsWithin_le_nhds
58   have hn := (poleNumerator_analyticAt hf hρ hd r).continuousAt.tendsto.comp ht
59   have hnum : Tendsto (fun z : ℂ => (1-z/ρ)^r * (f z ^ r)⁻¹) (𝓝[≠] ρ)
60       (𝓝 (((-ρ * deriv f ρ) ^ r)⁻¹)) := by
61     simp only [poleNumerator, sub_zero, mul_one, dslope_same] at hn
62     apply hn.congr'
63     filter_upwards [self_mem_nhdsWithin] with z hz
64     have htz : 1-z/ρ ≠ 0 := by
65       intro h
66       exact hz ((div_eq_one_iff_eq hρ).mp (sub_eq_zero.mp h).symm)
67     rw [poleNumerator_identity hfρ hρ hz r]
68     rw [← mul_assoc, mul_inv_cancel₀ (pow_ne_zero r htz), one_mul]
69     rfl
70   have hzero : Tendsto (fun z : ℂ => (1-z/ρ)^r) (𝓝[≠] ρ) (𝓝 0) := by simpa [hr.ne'] using ht.pow r
71   have hrem := hzero.zero_mul_isBoundedUnder_le hb
72   have hdiff := hnum.sub (polePrincipalPart_scaled_limit a hr hρ)
73   have hEq : ((-ρ * deriv f ρ) ^ r)⁻¹ - a ρ r = 0 :=
74     tendsto_nhds_unique hdiff (by simpa only [mul_sub] using hrem)
75   exact (sub_eq_zero.mp hEq).symm
76 
77 end
78 end Komorebi.PaperIV

Back to source controls