ZeroSequenceAsymptotics.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedZeroSequence
6 import Mathlib.Analysis.PSeries
7 import Mathlib.Analysis.Asymptotics.SpecificAsymptotics
8 import Mathlib.Analysis.Normed.Module.FiniteDimension
9 
10 namespace Komorebi.PaperIV
11 noncomputable section
12 open Filter Asymptotics Metric
13 
14 theorem signedZeroCenter_tendsto_atTop {N : ℕ} (hN : 2 ≤ N) :
15     Tendsto (signedZeroCenter N) atTop atTop := by
16   exact (tendsto_atTop_add_const_right atTop (1 / 2 : ℝ) tendsto_natCast_atTop_atTop).const_mul_atTop
17     (div_pos Real.pi_pos (signed_sine_pos hN))
18 
19 theorem signedPositiveZero_sub_center_isBigO_one {N : ℕ} (hN : 3 ≤ N) :
20     (fun m => signedPositiveZero N m - signedZeroCenter N m) =O[atTop] (fun _ => (1 : ℝ)) := by
21   obtain ⟨C, _, m0, hm0⟩ := signedPositiveZero_local_strings hN
22   apply isBigO_iff.mpr
23   refine ⟨1 / ‖signedZeroFrequency N‖, ?_⟩
24   filter_upwards [eventually_ge_atTop m0] with m hm
25   have hb := (hm0 m hm).1.2.2
26   simpa only [mem_closedBall, dist_eq_norm, ← Complex.ofReal_sub, Complex.norm_real,
27     Real.norm_eq_abs, norm_one, mul_one] using hb
28 
29 theorem signedPositiveZero_equivalent_center {N : ℕ} (hN : 3 ≤ N) :
30     signedPositiveZero N ~[atTop] signedZeroCenter N := by
31   have ht : Tendsto (fun m => ‖signedZeroCenter N m‖) atTop atTop := by
32     apply (signedZeroCenter_tendsto_atTop (by omega : 2 ≤ N)).congr'
33     filter_upwards [] with m
34     rw [Real.norm_eq_abs, abs_of_nonneg]
35     exact (le_of_lt (one_div_pos.mpr (norm_pos_iff.mpr (signedZeroFrequency_ne_zero (by omega))))).trans
36       (signedZeroCenter_ge_radius (by omega) m)
37   exact (signedPositiveZero_sub_center_isBigO_one hN).trans_isLittleO
38     (isLittleO_const_left.mpr (Or.inr ht))
39 
40 theorem signedPositiveZero_tendsto_atTop {N : ℕ} (hN : 3 ≤ N) :
41     Tendsto (signedPositiveZero N) atTop atTop := by
42   have he := signedPositiveZero_equivalent_center hN
43   exact he.symm.tendsto_atTop (signedZeroCenter_tendsto_atTop (by omega))
44 
45 theorem reducedPositiveZero_equivalent_center_power {N : ℕ} (hN : 3 ≤ N) :
46     reducedPositiveZero N ~[atTop] (fun m => signedZeroCenter N m ^ N) :=
47   (signedPositiveZero_equivalent_center hN).pow N
48 
49 /-- The reciprocal powers of the actual positive zero sequence have the sharp threshold `s > 1`. -/
50 theorem signedPositiveZero_reciprocal_rpow_summable_iff {N : ℕ} (hN : 3 ≤ N) (s : ℝ) :
51     Summable (fun m => 1 / signedPositiveZero N m ^ s) ↔ 1 < s := by
52   have hA : 0 < Real.pi / Real.sin (Real.pi / N) := div_pos Real.pi_pos (signed_sine_pos (by omega))
53   have ht : 0 ≤ signedZeroCenter N := fun m => by unfold signedZeroCenter; positivity
54   have he := (IsEquivalent.rpow ht (signedPositiveZero_equivalent_center hN) (r := s)).inv
55   have heq : (fun m => 1 / signedPositiveZero N m ^ s) ~[atTop]
56       (fun m => 1 / signedZeroCenter N m ^ s) := by simpa only [one_div] using! he
57   rw [heq.summable_iff_nat]
58   have hf : (fun m => 1 / signedZeroCenter N m ^ s) =
59       (fun m : ℕ => (1 / (Real.pi / Real.sin (Real.pi / N)) ^ s) * (1 / |(m : ℝ) + 1 / 2| ^ s)) := by
60     funext m
61     rw [signedZeroCenter, Real.mul_rpow hA.le (by positivity), abs_of_pos (by positivity : 0 < (m : ℝ) + 1 / 2)]
62     ring
63   rw [hf, summable_mul_left_iff (one_div_ne_zero (ne_of_gt (Real.rpow_pos_of_pos hA s)))]
64   exact Real.summable_one_div_nat_add_rpow (1 / 2) s
65 
66 /-- The reduced positive zeros have reciprocal-power threshold `N s > 1`. -/
67 theorem reducedPositiveZero_reciprocal_rpow_summable_iff {N : ℕ} (hN : 3 ≤ N) (s : ℝ) :
68     Summable (fun m => 1 / reducedPositiveZero N m ^ s) ↔ 1 < (N : ℝ) * s := by
69   have he : (fun m => 1 / reducedPositiveZero N m ^ s) =
70       (fun m => 1 / signedPositiveZero N m ^ ((N : ℝ) * s)) := by
71     funext m
72     rw [reducedPositiveZero, ← Real.rpow_natCast, ← Real.rpow_mul (le_of_lt (signedPositiveZero_pos (by omega) m))]
73   rw [he]
74   exact signedPositiveZero_reciprocal_rpow_summable_iff hN _
75 
76 theorem reducedPositiveZero_reciprocal_summable {N : ℕ} (hN : 3 ≤ N) :
77     Summable (fun m => 1 / reducedPositiveZero N m) := by
78   simpa using (reducedPositiveZero_reciprocal_rpow_summable_iff hN 1).mpr (by exact_mod_cast (show 1 < N * 1 by omega))
79 
80 end
81 end Komorebi.PaperIV

Back to source controls