RealAxisPoleRigidity.lean

1 import Mathlib.Analysis.Asymptotics.Lemmas
2 import Mathlib.Analysis.Asymptotics.Ring
3 import Mathlib.Analysis.SpecialFunctions.Complex.Analytic
4 import Mathlib.Tactic
5 
6 /-! A pole product argument using only limits and first-order endpoint bounds.
7 No meromorphic or analytic regularity is assumed. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperX.RealAxisPoleRigidity
11 open Filter Asymptotics
12 open scoped Topology
13 
14 /-- A first-order error against a vanishing scale supplies the endpoint limit. -/
15 theorem tendsto_of_error_isBigO {α : Type*} {l : Filter α}
16     {x a : α → ℂ} {A : ℂ} (hx : Tendsto x l (𝓝 0))
17     (ha : (fun t => a t - A) =O[l] x) : Tendsto a l (𝓝 A) := by
18   have h := (ha.trans_tendsto hx).add_const A
19   simpa using h
20 
21 /-- A bounded function cannot have a nonzero simple-pole residue. -/
22 theorem residue_eq_zero_of_bounded {α : Type*} {l : Filter α} [NeBot l]
23     {x Z : α → ℂ} {Q : ℂ} (hx : Tendsto x l (𝓝 0))
24     (hZ : Z =O[l] fun _ => (1 : ℂ))
25     (hQ : Tendsto (fun t => x t * Z t) l (𝓝 Q)) : Q = 0 := by
26   have hb : (fun t => x t * Z t) =O[l] x := by
27     simpa using (isBigO_refl x l).mul hZ
28   exact tendsto_nhds_unique hQ (hb.trans_tendsto hx)
29 
30 /-- Once every endpoint factor is nonzero, a product identity between two
31 simple poles forces the natural exponent to be one. -/
32 theorem exponent_one_of_nonzero_limits {α ι : Type*} [Fintype ι]
33     {l : Filter α} [NeBot l] (x p Z : α → ℂ) (a : ι → α → ℂ)
34     (A : ι → ℂ) (P Q : ℂ) (d : ℕ)
35     (hx : Tendsto x l (𝓝 0))
36     (hp : Tendsto (fun t => x t * p t) l (𝓝 P)) (hP : P ≠ 0)
37     (hZ : Tendsto (fun t => x t * Z t) l (𝓝 Q)) (hQ : Q ≠ 0)
38     (ha : ∀ i, Tendsto (a i) l (𝓝 (A i))) (hA : ∀ i, A i ≠ 0)
39     (hid : Z =ᶠ[l] fun t => (p t * ∏ i, a i t) ^ d) : d = 1 := by
40   classical
41   have hprod : Tendsto (fun t => ∏ i, a i t) l (𝓝 (∏ i, A i)) :=
42     tendsto_finsetProd _ (fun i _ => ha i)
43   have hB : Tendsto (fun t => x t * (p t * ∏ i, a i t)) l
44       (𝓝 (P * ∏ i, A i)) := by
45     simpa only [mul_assoc] using hp.mul hprod
46   have hB0 : P * ∏ i, A i ≠ 0 := mul_ne_zero hP
47     (Finset.prod_ne_zero_iff.mpr (fun i _ => hA i))
48   have hd0 : d ≠ 0 := by
49     intro hd
50     have he : Z =ᶠ[l] fun _ => (1 : ℂ) := by simpa [hd] using hid
51     exact hQ (residue_eq_zero_of_bounded hx
52       ((isBigO_refl (fun _ : α => (1 : ℂ)) l).congr' he.symm Filter.EventuallyEq.rfl) hZ)
53   by_contra hd
54   have hd1 : 0 < d - 1 := by omega
55   have hleft : Tendsto (fun t => x t ^ (d - 1) * (x t * Z t)) l (𝓝 0) := by
56     simpa [zero_pow (Nat.ne_of_gt hd1)] using (hx.pow (d - 1)).mul hZ
57   have hright : Tendsto (fun t => (x t * (p t * ∏ i, a i t)) ^ d) l
58       (𝓝 ((P * ∏ i, A i) ^ d)) := hB.pow d
59   have he : (fun t => x t ^ (d - 1) * (x t * Z t)) =ᶠ[l]
60       fun t => (x t * (p t * ∏ i, a i t)) ^ d := by
61     filter_upwards [hid] with t ht
62     rw [ht, mul_pow]
63     rw [← mul_assoc, ← pow_succ, Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr hd0)]
64     simp only [mul_pow]
65   have hz := tendsto_nhds_unique (hleft.congr' he) hright
66   exact (pow_ne_zero d hB0) hz.symm
67 
68 /-- A finite family with first-order endpoint errors cannot cancel a supplied
69 simple pole inside a natural power which again has a nonzero simple-pole residue.
70 The exponent and nonvanishing conclusions are derived together. -/
71 theorem index_one_and_factors_nonzero {α ι : Type*} [Fintype ι]
72     {l : Filter α} [NeBot l] (x p Z : α → ℂ) (a : ι → α → ℂ)
73     (A : ι → ℂ) (P Q : ℂ) (d : ℕ)
74     (hx : Tendsto x l (𝓝 0))
75     (hp : Tendsto (fun t => x t * p t) l (𝓝 P)) (hP : P ≠ 0)
76     (hZ : Tendsto (fun t => x t * Z t) l (𝓝 Q)) (hQ : Q ≠ 0)
77     (ha : ∀ i, (fun t => a i t - A i) =O[l] x)
78     (hid : Z =ᶠ[l] fun t => (p t * ∏ i, a i t) ^ d) :
79     d = 1 ∧ ∀ i, A i ≠ 0 := by
80   classical
81   have hal : ∀ i, Tendsto (a i) l (𝓝 (A i)) :=
82     fun i => tendsto_of_error_isBigO hx (ha i)
83   have hA : ∀ i, A i ≠ 0 := by
84     intro i hi
85     have hai : a i =O[l] x := by simpa [hi] using ha i
86     have hpa : (fun t => p t * a i t) =O[l] fun _ => (1 : ℂ) := by
87       have hh : (fun t => p t * a i t) =O[l] fun t => x t * p t := by
88         simpa only [mul_comm] using hai.mul (isBigO_refl p l)
89       exact hh.trans (hp.isBigO_one ℂ)
90     have hrest : Tendsto (fun t => ∏ j ∈ Finset.univ.erase i, a j t) l
91         (𝓝 (∏ j ∈ Finset.univ.erase i, A j)) :=
92       tendsto_finsetProd _ (fun j _ => hal j)
93     have hb : (fun t => p t * ∏ j, a j t) =O[l] fun _ => (1 : ℂ) := by
94       have hh := hpa.mul (hrest.isBigO_one ℂ)
95       have he : (fun t => p t * a i t * ∏ j ∈ Finset.univ.erase i, a j t) =
96           fun t => p t * ∏ j, a j t := by
97         funext t
98         rw [mul_assoc, Finset.mul_prod_erase Finset.univ (fun j => a j t)
99           (Finset.mem_univ i)]
100       simpa only [he, one_mul] using hh
101     have hbZ : Z =O[l] fun _ => (1 : ℂ) := by
102       have hh : (fun t => (p t * ∏ j, a j t) ^ d) =O[l] fun _ => (1 : ℂ) := by
103         simpa using hb.pow d
104       exact hh.congr' hid.symm Filter.EventuallyEq.rfl
105     exact hQ (residue_eq_zero_of_bounded hx hbZ hZ)
106   exact ⟨exponent_one_of_nonzero_limits x p Z a A P Q d hx hp hP hZ hQ hal hA hid, hA⟩
107 
108 /-- Specialization to the right-hand real endpoint, with scale `h`. -/
109 theorem right_endpoint_index_one_and_factors_nonzero {ι : Type*} [Fintype ι]
110     (p Z : ℝ → ℂ) (a : ι → ℝ → ℂ) (P Q : ℂ) (d : ℕ)
111     (hp : Tendsto (fun h : ℝ => (h : ℂ) * p h) (𝓝[>] 0) (𝓝 P)) (hP : P ≠ 0)
112     (hZ : Tendsto (fun h : ℝ => (h : ℂ) * Z h) (𝓝[>] 0) (𝓝 Q)) (hQ : Q ≠ 0)
113     (ha : ∀ i, (fun h => a i h - a i 0) =O[𝓝[>] 0] fun h => (h : ℂ))
114     (hid : Z =ᶠ[𝓝[>] 0] fun h => (p h * ∏ i, a i h) ^ d) :
115     d = 1 ∧ ∀ i, a i 0 ≠ 0 := by
116   apply index_one_and_factors_nonzero (fun h : ℝ => (h : ℂ)) p Z a (fun i => a i 0)
117     P Q d _ hp hP hZ hQ ha hid
118   exact Complex.continuous_ofReal.continuousAt.tendsto.mono_left nhdsWithin_le_nhds
119 
120 end PaperX.RealAxisPoleRigidity

Back to source controls