RealAxisPoleBoundary.lean

1 import PaperX.RealAxisPoleRigidity
2 import Mathlib.Analysis.SpecialFunctions.Sqrt
3 
4 /-! Finite endpoint limits do not suffice for the pole argument: a square-root
5 factor cancels half a pole, and taking its square restores a simple pole. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.RealAxisPoleBoundary
9 open Filter Asymptotics
10 open scoped Topology
11 
12 def pole (h : ℝ) : ℂ := (h : ℂ)⁻¹
13 def rootFactor (h : ℝ) : ℂ := (Real.sqrt h : ℂ)
14 
15 theorem rootFactor_zero : rootFactor 0 = 0 := by simp [rootFactor]
16 
17 theorem rootFactor_tendsto : Tendsto rootFactor (𝓝[>] 0) (𝓝 0) := by
18   have h := Complex.continuous_ofReal.comp Real.continuous_sqrt
19   change Tendsto (fun x : ℝ => (Real.sqrt x : ℂ)) (𝓝[>] 0) (𝓝 0)
20   simpa [Function.comp_def] using h.continuousAt.tendsto.mono_left
21     (nhdsWithin_le_nhds : 𝓝[>] (0 : ℝ) ≤ 𝓝 0)
22 
23 theorem pole_residue : Tendsto (fun h : ℝ => (h : ℂ) * pole h) (𝓝[>] 0) (𝓝 1) := by
24   apply tendsto_const_nhds.congr'
25   filter_upwards [self_mem_nhdsWithin] with h hh
26   have hh0 : (h : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (ne_of_gt hh)
27   simp [pole, hh0]
28 
29 /-- The identity holds on the entire positive real axis. -/
30 theorem squared_product (h : ℝ) (hh : 0 < h) :
31     pole h = (pole h * rootFactor h) ^ 2 := by
32   have hs : rootFactor h ^ 2 = (h : ℂ) := by
33     simpa [rootFactor, ← Complex.ofReal_pow] using
34       congrArg (fun x : ℝ => (x : ℂ)) (Real.sq_sqrt (le_of_lt hh))
35   have hh0 : (h : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (ne_of_gt hh)
36   rw [mul_pow, hs]
37   simp only [pole]
38   field_simp
39 
40 theorem eventual_squared_product : pole =ᶠ[𝓝[>] 0]
41     fun h => (pole h * rootFactor h) ^ 2 := by
42   filter_upwards [self_mem_nhdsWithin] with h hh
43   exact squared_product h hh
44 
45 /-- The square-root factor has a finite endpoint limit but lacks the first-order
46 error bound used in the real-axis pole theorem. -/
47 theorem rootFactor_not_isBigO :
48     ¬ ((fun h => rootFactor h - rootFactor 0) =O[𝓝[>] 0] fun h : ℝ => (h : ℂ)) := by
49   intro hb
50   have hid : pole =ᶠ[𝓝[>] 0] fun h =>
51       (pole h * ∏ _ : Unit, rootFactor h) ^ 2 := by
52     simpa using eventual_squared_product
53   have hd := PaperX.RealAxisPoleRigidity.right_endpoint_index_one_and_factors_nonzero
54     pole pole (fun _ : Unit => rootFactor) 1 1 2 pole_residue one_ne_zero
55     pole_residue one_ne_zero (fun _ => hb) hid
56   norm_num at hd
57 
58 /-- An explicit witness refutes replacement of first-order errors by finite
59 limits alone, even when both normalized pole residues equal one. -/
60 theorem finite_limits_do_not_force_index_one :
61     ∃ (p Z a : ℝ → ℂ) (d : ℕ),
62       Tendsto (fun h : ℝ => (h : ℂ) * p h) (𝓝[>] 0) (𝓝 1) ∧
63       Tendsto (fun h : ℝ => (h : ℂ) * Z h) (𝓝[>] 0) (𝓝 1) ∧
64       Tendsto a (𝓝[>] 0) (𝓝 (a 0)) ∧
65       (Z =ᶠ[𝓝[>] 0] fun h => (p h * a h) ^ d) ∧ d ≠ 1 ∧ a 0 = 0 := by
66   exact ⟨pole, pole, rootFactor, 2, pole_residue, pole_residue,
67     by simpa [rootFactor_zero] using rootFactor_tendsto,
68     eventual_squared_product, by decide, rootFactor_zero⟩
69 
70 end PaperX.RealAxisPoleBoundary

Back to source controls