PoleRemoval.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.AnalyticTaylorDifferential
6 import KomorebiPaperIV.PrincipalPartCoefficients
7 import Mathlib.Analysis.Meromorphic.NormalForm
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Filter Metric
12 open scoped Topology Classical
13 
14 def poleTerm (ρ : ℂ) (ℓ : ℕ) (z : ℂ) : ℂ := ((1 - z / ρ) ^ ℓ)⁻¹
15 
16 def polePrincipalPart (a : ℂ → ℕ → ℂ) (r : ℕ) (ρ z : ℂ) : ℂ :=
17   ∑ k ∈ Finset.range r, a ρ (k + 1) * poleTerm ρ (k + 1) z
18 
19 def rawPoleRemainder (f : ℂ → ℂ) (S : Finset ℂ) (a : ℂ → ℕ → ℂ) (r : ℕ) (z : ℂ) : ℂ :=
20   (f z ^ r)⁻¹ - ∑ ρ ∈ S, polePrincipalPart a r ρ z
21 
22 theorem poleTerm_analyticAt {ρ z : ℂ} (hρ : ρ ≠ 0) (hz : z ≠ ρ) (ℓ : ℕ) :
23     AnalyticAt ℂ (poleTerm ρ ℓ) z := by
24   have h : 1 - z / ρ ≠ 0 := by
25     intro he
26     apply hz
27     exact (div_eq_one_iff_eq hρ).mp (sub_eq_zero.mp he).symm
28   unfold poleTerm
29   exact ((analyticAt_const.sub (analyticAt_id.div_const)).pow ℓ).inv (pow_ne_zero ℓ h)
30 
31 theorem poleTerm_meromorphicAt (ρ z : ℂ) (ℓ : ℕ) : MeromorphicAt (poleTerm ρ ℓ) z := by
32   unfold poleTerm
33   exact (((analyticAt_const.sub (analyticAt_id.div_const)).pow ℓ).meromorphicAt).inv
34 
35 theorem polePrincipalPart_analyticAt {ρ z : ℂ} (hρ : ρ ≠ 0) (hz : z ≠ ρ)
36     (a : ℂ → ℕ → ℂ) (r : ℕ) : AnalyticAt ℂ (polePrincipalPart a r ρ) z := by
37   exact Finset.analyticAt_fun_sum _ (fun k _ => analyticAt_const.mul (poleTerm_analyticAt hρ hz (k+1)))
38 
39 theorem rawPoleRemainder_meromorphic {f : ℂ → ℂ} (hf : Differentiable ℂ f)
40     (S : Finset ℂ) (a : ℂ → ℕ → ℂ) (r : ℕ) :
41     MeromorphicOn (rawPoleRemainder f S a r) univ := by
42   intro z _
43   apply (((hf.analyticAt z).pow r).meromorphicAt.inv).sub
44   exact MeromorphicAt.fun_sum (fun ρ _ => MeromorphicAt.fun_sum
45     (fun k _ => (MeromorphicAt.const _ _).mul (poleTerm_meromorphicAt ρ z (k+1))))
46 
47 theorem rawPoleRemainder_analyticAt {f : ℂ → ℂ} {z : ℂ} (hf : AnalyticAt ℂ f z)
48     (hfz : f z ≠ 0) {S : Finset ℂ} (hS : ∀ ρ ∈ S, ρ ≠ 0) (hz : z ∉ S)
49     (a : ℂ → ℕ → ℂ) (r : ℕ) : AnalyticAt ℂ (rawPoleRemainder f S a r) z := by
50   apply ((hf.pow r).inv (pow_ne_zero r hfz)).sub
51   exact Finset.analyticAt_fun_sum _ (fun ρ hρ => polePrincipalPart_analyticAt (hS ρ hρ)
52     (fun (he : z = ρ) => hz (he.symm ▸ hρ)) a r)
53 
54 /-- A locally bounded meromorphic germ has no negative order. This proves
55 removability without assuming a holomorphic remainder. -/
56 theorem meromorphicOrderAt_nonneg_of_bounded {f : ℂ → ℂ} {z : ℂ}
57     (hb : ∃ C : ℝ, ∀ᶠ w in 𝓝[≠] z, ‖f w‖ ≤ C) : 0 ≤ meromorphicOrderAt f z := by
58   by_contra hn
59   have ht := tendsto_norm_atTop_iff_cobounded.mpr (tendsto_cobounded_of_meromorphicOrderAt_neg (lt_of_not_ge hn))
60   obtain ⟨C, hC⟩ := hb
61   obtain ⟨w, hw, hw'⟩ := (hC.and (ht.eventually_gt_atTop C)).exists
62   exact (not_lt_of_ge hw) hw'
63 
64 /-- The manuscript's local O(1) principal-part condition implies boundedness
65 of the remainder after all finitely many principal parts are subtracted. -/
66 theorem rawPoleRemainder_bounded_at_pole {f : ℂ → ℂ} {S : Finset ℂ}
67     (hS : ∀ ρ ∈ S, ρ ≠ 0) (a : ℂ → ℕ → ℂ) (r : ℕ) {ρ : ℂ} (hρ : ρ ∈ S)
68     (hb : ∃ C : ℝ, ∀ᶠ z in 𝓝[≠] ρ, ‖(f z ^ r)⁻¹ - polePrincipalPart a r ρ z‖ ≤ C) :
69     ∃ C : ℝ, ∀ᶠ z in 𝓝[≠] ρ, ‖rawPoleRemainder f S a r z‖ ≤ C := by
70   let Q : ℂ → ℂ := fun z => ∑ τ ∈ S.erase ρ, polePrincipalPart a r τ z
71   have hQ : AnalyticAt ℂ Q ρ := Finset.analyticAt_fun_sum _ (fun τ hτ =>
72     polePrincipalPart_analyticAt (hS τ (Finset.mem_erase.mp hτ).2)
73       (Ne.symm (Finset.mem_erase.mp hτ).1) a r)
74   have he : ∀ᶠ z in 𝓝[≠] ρ, ‖Q z‖ ≤ ‖Q ρ‖ + 1 :=
75     (hQ.continuousAt.norm.eventually (eventually_le_nhds (by linarith : ‖Q ρ‖ < ‖Q ρ‖ + 1))).filter_mono nhdsWithin_le_nhds
76   obtain ⟨C, hC⟩ := hb
77   refine ⟨C + (‖Q ρ‖ + 1), ?_⟩
78   filter_upwards [hC, he] with z hz hq
79   have hsum := Finset.sum_erase_add S (fun τ => polePrincipalPart a r τ z) hρ
80   have heq : rawPoleRemainder f S a r z = ((f z ^ r)⁻¹ - polePrincipalPart a r ρ z) - Q z := by
81     unfold rawPoleRemainder Q
82     rw [← hsum]
83     ring
84   rw [heq]
85   exact (norm_sub_le _ _).trans (add_le_add hz hq)
86 
87 def removedPoleRemainder (f : ℂ → ℂ) (S : Finset ℂ) (a : ℂ → ℕ → ℂ) (r : ℕ) : ℂ → ℂ :=
88   toMeromorphicNFOn (rawPoleRemainder f S a r) univ
89 
90 theorem removedPoleRemainder_analyticOnNhd {f : ℂ → ℂ} (hf : Differentiable ℂ f)
91     {S : Finset ℂ} (hS : ∀ ρ ∈ S, ρ ≠ 0) (a : ℂ → ℕ → ℂ) (r : ℕ) {U : Set ℂ}
92     (hzeros : ∀ z ∈ U, f z = 0 → z ∈ S)
93     (hlocal : ∀ ρ ∈ S, ∃ C : ℝ, ∀ᶠ z in 𝓝[≠] ρ,
94       ‖(f z ^ r)⁻¹ - polePrincipalPart a r ρ z‖ ≤ C) :
95     AnalyticOnNhd ℂ (removedPoleRemainder f S a r) U := by
96   intro z hz
97   have hn := meromorphicNFOn_toMeromorphicNFOn (rawPoleRemainder f S a r) univ (mem_univ z)
98   apply hn.meromorphicOrderAt_nonneg_iff_analyticAt.mp
99   rw [meromorphicOrderAt_toMeromorphicNFOn (rawPoleRemainder_meromorphic hf S a r) (mem_univ z)]
100   by_cases hsz : z ∈ S
101   · exact meromorphicOrderAt_nonneg_of_bounded (rawPoleRemainder_bounded_at_pole hS a r hsz (hlocal z hsz))
102   · have ha := rawPoleRemainder_analyticAt (hf.analyticAt z) (fun he => hsz (hzeros z hz he)) hS hsz a r
103     exact ha.meromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt.mpr ha
104 
105 theorem removedPoleRemainder_eq_raw {f : ℂ → ℂ} (hf : Differentiable ℂ f)
106     {S : Finset ℂ} (hS : ∀ ρ ∈ S, ρ ≠ 0) (a : ℂ → ℕ → ℂ) (r : ℕ) {z : ℂ}
107     (hfz : f z ≠ 0) (hz : z ∉ S) :
108     removedPoleRemainder f S a r z = rawPoleRemainder f S a r z := by
109   unfold removedPoleRemainder
110   rw [toMeromorphicNFOn_eq_toMeromorphicNFAt (rawPoleRemainder_meromorphic hf S a r) (mem_univ z),
111     toMeromorphicNFAt_eq_self.mpr (rawPoleRemainder_analyticAt (hf.analyticAt z) hfz hS hz a r).meromorphicNFAt]
112 
113 end
114 end Komorebi.PaperIV

Back to source controls