SecantAsymptotic.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.LeadingPoleBounds
6 import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter Asymptotics
11 open scoped Topology Classical
12 
13 def cosineNearestZeros : Finset ℂ := {(Real.pi : ℂ)/2, -(Real.pi : ℂ)/2}
14 
15 theorem canonicalSignedDenominator_two_cos : canonicalSignedDenominator 2 = Complex.cos :=
16   funext (entireSigned_two_eq_cos (canonicalPrimitiveRoot_isPrimitive (by norm_num))
17     (canonicalSignedRoot_pow (by norm_num)))
18 
19 theorem cosineNearestZeros_norm {z : ℂ} (hz : z ∈ cosineNearestZeros) : ‖z‖ = Real.pi/2 := by
20   simp only [cosineNearestZeros, Finset.mem_insert, Finset.mem_singleton] at hz
21   rcases hz with rfl | rfl <;> simp [Complex.norm_real, Real.norm_eq_abs, Real.pi_pos.le]
22 
23 theorem cosineNearestZeros_root {z : ℂ} (hz : z ∈ cosineNearestZeros) : canonicalSignedDenominator 2 z = 0 := by
24   rw [canonicalSignedDenominator_two_cos]
25   simp only [cosineNearestZeros, Finset.mem_insert, Finset.mem_singleton] at hz
26   rcases hz with rfl | rfl <;> simp [neg_div, Complex.cos_neg, Complex.cos_pi_div_two]
27 
28 theorem cosineNearestZeros_simple {z : ℂ} (hz : z ∈ cosineNearestZeros) :
29     deriv (canonicalSignedDenominator 2) z ≠ 0 :=
30   entireSigned_two_zero_derivative_ne_zero (canonicalPrimitiveRoot_isPrimitive (by norm_num))
31     (canonicalSignedRoot_pow (by norm_num)) (cosineNearestZeros_root hz)
32 
33 theorem cosine_nearest_zero_exhaustion {z : ℂ} (hnorm : ‖z‖ < 3*Real.pi/2)
34     (hz : canonicalSignedDenominator 2 z = 0) : z ∈ cosineNearestZeros := by
35   obtain ⟨m, hm⟩ := (entireSigned_two_zero_iff_nat (canonicalPrimitiveRoot_isPrimitive (by norm_num))
36     (canonicalSignedRoot_pow (by norm_num))).mp hz
37   have hmod : ‖(((m : ℂ)+1/2)*(Real.pi : ℂ))‖ = ((m : ℝ)+1/2)*Real.pi := by
38     have he : (((m : ℂ)+1/2)*(Real.pi : ℂ)) = ((((m : ℝ)+1/2)*Real.pi : ℝ) : ℂ) := by push_cast; rfl
39     rw [he, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg (by positivity)]
40   have hle : ((m : ℝ)+1/2)*Real.pi < 3*Real.pi/2 := by
41     rcases hm with hm | hm <;> simpa only [hm, norm_neg, hmod] using hnorm
42   have hm0 : m = 0 := by
43     by_contra h
44     have hm1 : (1 : ℝ) ≤ m := by exact_mod_cast Nat.one_le_iff_ne_zero.mpr h
45     nlinarith [Real.pi_pos]
46   subst m
47   rcases hm with rfl | rfl <;> simp [cosineNearestZeros, div_eq_mul_inv, mul_comm]
48 
49 theorem secant_leading_coefficient (n : ℕ) :
50     leadingPoleCoefficient cosineNearestZeros
51       (canonicalPoleCoefficient (canonicalSignedDenominator 2) 1) 1 (2*n) =
52       2 * (2/(Real.pi : ℂ)) ^ (2*n+1) := by
53   have hp : (Real.pi : ℂ) ≠ 0 := by exact_mod_cast Real.pi_ne_zero
54   have hne : (Real.pi : ℂ)/2 ≠ -(Real.pi : ℂ)/2 := by
55     intro he
56     have hh := congrArg Complex.re he
57     simp at hh
58     linarith [Real.pi_pos]
59   simp only [leadingPoleCoefficient, Nat.add_sub_cancel, Nat.sub_self, Nat.choose_zero_right,
60     Nat.cast_one, one_mul, cosineNearestZeros, Finset.sum_pair hne,
61     canonicalPoleCoefficient_leading, canonicalSignedDenominator_two_cos, Complex.deriv_cos,
62     pow_one, Complex.sin_pi_div_two]
63   rw [show -(Real.pi : ℂ)/2 = -((Real.pi : ℂ)/2) by ring,
64     Complex.sin_neg, Complex.sin_pi_div_two]
65   simp only [neg_neg, mul_neg, mul_one, inv_neg, (even_two_mul n).neg_pow]
66   rw [pow_succ]
67   field_simp
68   ring
69 
70 /-- A quantitative version of the secant asymptotic, with an explicit
71 exponentially smaller Cauchy remainder. -/
72 theorem secant_coefficient_error : ∃ C : ℝ, ∀ n : ℕ, 1 ≤ n →
73     ‖reciprocalCoeff 2 n (1 : ℂ) - 2 * ((2*n).factorial : ℂ) * (2/(Real.pi : ℂ)) ^ (2*n+1)‖ ≤
74       C * ((2*n).factorial : ℝ) * Real.pi⁻¹ ^ (2*n) := by
75   obtain ⟨C, hC⟩ := reciprocalCoeff_leading_bound (by norm_num : 0 < 2)
76     (show 0 < Real.pi/2 by positivity) (show Real.pi/2 < Real.pi by linarith [Real.pi_pos])
77     (show Real.pi < 3*Real.pi/2 by linarith [Real.pi_pos])
78     (fun _ hz => cosineNearestZeros_norm hz) (fun _ hz => cosineNearestZeros_root hz)
79     (fun _ hz => cosineNearestZeros_simple hz) (fun _ hz => cosine_nearest_zero_exhaustion hz)
80     (by norm_num : 0 < 1)
81   refine ⟨C, fun n hn => ?_⟩
82   have h := hC n hn
83   rw [secant_leading_coefficient] at h
84   simpa only [lowerPrincipalConstant_one, zero_mul, mul_zero, zero_add, Nat.cast_one,
85     mul_assoc, mul_comm, mul_left_comm] using h
86 
87 def secantMainTerm (n : ℕ) : ℂ :=
88   2 * ((2*n).factorial : ℂ) * (2/(Real.pi : ℂ)) ^ (2*n+1)
89 
90 theorem secantMainTerm_norm (n : ℕ) :
91     ‖secantMainTerm n‖ = 2 * ((2*n).factorial : ℝ) * (2/Real.pi) ^ (2*n+1) := by
92   simp [secantMainTerm, norm_pow, Complex.norm_real,
93     Real.norm_eq_abs, abs_of_pos Real.pi_pos]
94 
95 theorem secantMainTerm_ne_zero (n : ℕ) : secantMainTerm n ≠ 0 := by
96   apply norm_ne_zero_iff.mp
97   rw [secantMainTerm_norm]
98   positivity
99 
100 theorem secant_relative_error : ∃ C : ℝ, ∀ n : ℕ, 1 ≤ n →
101     ‖reciprocalCoeff 2 n (1 : ℂ) / secantMainTerm n - 1‖ ≤
102       (C * Real.pi / 4) * (1/4 : ℝ) ^ n := by
103   obtain ⟨C, hC⟩ := secant_coefficient_error
104   refine ⟨C, fun n hn => ?_⟩
105   rw [div_sub_one (secantMainTerm_ne_zero n), norm_div]
106   have hp : (0 : ℝ) < 2 * ((2*n).factorial : ℝ) * (2/Real.pi) ^ (2*n+1) := by positivity
107   rw [secantMainTerm_norm]
108   have hb := div_le_div_of_nonneg_right (hC n hn) hp.le
109   apply hb.trans_eq
110   rw [pow_succ, pow_mul, pow_mul, div_pow, inv_pow, div_pow]
111   have hfac : ((2*n).factorial : ℝ) ≠ 0 := by positivity
112   have hpi : Real.pi ^ (n*2) * Real.pi⁻¹ ^ (n*2) = 1 := by
113     rw [← mul_pow, mul_inv_cancel₀ Real.pi_ne_zero, one_pow]
114   have hfour : (1/4 : ℝ)^n * 4^n = 1 := by rw [← mul_pow]; norm_num
115   field_simp
116   ring_nf
117   linear_combination 4*C*hpi - 4*C*hfour
118 
119 /-- Corollary 13.4 as a genuine ratio limit for the named reciprocal coefficients. -/
120 theorem secant_coefficient_ratio_limit :
121     Tendsto (fun n : ℕ => reciprocalCoeff 2 n (1 : ℂ) / secantMainTerm n) atTop (𝓝 1) := by
122   obtain ⟨C, hC⟩ := secant_relative_error
123   have hg : Tendsto (fun n : ℕ => (C*Real.pi/4) * (1/4 : ℝ)^n) atTop (𝓝 0) := by
124     simpa using (tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num : (0:ℝ) ≤ 1/4)
125       (by norm_num : (1/4:ℝ) < 1)).const_mul (C*Real.pi/4)
126   have hh : Tendsto (fun n : ℕ => ‖reciprocalCoeff 2 n (1 : ℂ) / secantMainTerm n - 1‖) atTop (𝓝 0) :=
127     squeeze_zero' (Eventually.of_forall (fun n => norm_nonneg _))
128       ((eventually_ge_atTop (1:ℕ)).mono (fun n hn => hC n hn)) hg
129   exact tendsto_iff_norm_sub_tendsto_zero.mpr hh
130 
131 theorem secant_coefficient_asymptotic :
132     (fun n : ℕ => reciprocalCoeff 2 n (1 : ℂ)) ~[atTop] secantMainTerm :=
133   (isEquivalent_iff_tendsto_one (Eventually.of_forall secantMainTerm_ne_zero)).mpr secant_coefficient_ratio_limit
134 
135 end
136 end Komorebi.PaperIV

Back to source controls