ExponentialZetaComparison.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroZetaConvergence
6 import Mathlib.Analysis.SpecialFunctions.Log.Deriv
7 import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
8 import Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
9 
10 namespace Komorebi.PaperIV
11 noncomputable section
12 open Set Filter Metric
13 open scoped Topology
14 
15 def positiveZetaTerm (r : ℝ) (s : ℂ) : ℂ := Complex.exp (-s * (Real.log r : ℂ))
16 
17 def exponentialZetaDifference (x y : ℕ → ℝ) (m : ℕ) (s : ℂ) : ℂ :=
18   positiveZetaTerm (x m) s - positiveZetaTerm (y m) s
19 
20 theorem positiveZetaTerm_entire (r : ℝ) : Differentiable ℂ (positiveZetaTerm r) := by
21   unfold positiveZetaTerm
22   fun_prop
23 
24 theorem exponentialZetaDifference_entire (x y : ℕ → ℝ) (m : ℕ) :
25     Differentiable ℂ (exponentialZetaDifference x y m) :=
26   (positiveZetaTerm_entire _).sub (positiveZetaTerm_entire _)
27 
28 theorem real_log_lipschitz_one {x y : ℝ} (hx : 1 ≤ x) (hy : 1 ≤ y) :
29     |Real.log x - Real.log y| ≤ |x - y| := by
30   have h := (convex_Ici (1 : ℝ)).norm_image_sub_le_of_norm_deriv_le
31     (f := Real.log) (C := 1)
32     (fun u hu => Real.differentiableAt_log (by change 1 ≤ u at hu; linarith))
33     (fun u hu => by
34       rw [Real.deriv_log, Real.norm_eq_abs, abs_of_pos (inv_pos.mpr (by change 1 ≤ u at hu; linarith))]
35       exact inv_le_one_of_one_le₀ hu) hy hx
36   simpa only [one_mul, Real.norm_eq_abs] using h
37 
38 theorem positiveZetaTerm_norm_le_rpow {y K : ℝ} (hy : 1 ≤ y) {s : ℂ} (hs : ‖s‖ ≤ K) :
39     ‖positiveZetaTerm y s‖ ≤ y ^ K := by
40   rw [positiveZetaTerm, Complex.norm_exp]
41   simp only [Complex.mul_re, Complex.neg_re, Complex.neg_im, Complex.ofReal_re,
42     Complex.ofReal_im, mul_zero, sub_zero]
43   rw [Real.rpow_def_of_pos (by linarith : 0 < y)]
44   apply Real.exp_le_exp.mpr
45   have hre : -s.re ≤ K := (neg_le_abs _).trans ((Complex.abs_re_le_norm s).trans hs)
46   have hl : 0 ≤ Real.log y := Real.log_nonneg hy
47   nlinarith
48 
49 theorem exponentialZetaDifference_factor (x y : ℝ) (s : ℂ) :
50     positiveZetaTerm x s - positiveZetaTerm y s = positiveZetaTerm y s *
51       (Complex.exp (-s * ((Real.log x - Real.log y : ℝ) : ℂ)) - 1) := by
52   unfold positiveZetaTerm
53   rw [mul_sub, ← Complex.exp_add, mul_one]
54   congr 2
55   push_cast
56   ring
57 
58 theorem summable_polynomial_exponential {y : ℕ → ℝ} (hy : ∀ m, 0 < y m)
59     (ht : Tendsto y atTop atTop) (hs : Summable (fun m => 1 / y m ^ (2 : ℝ)))
60     (K : ℝ) {γ : ℝ} (hγ : 0 < γ) :
61     Summable (fun m => y m ^ K * Real.exp (-γ * y m)) := by
62   have h := (tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (K + 2) γ hγ).comp ht
63   have hb := h.eventually (eventually_le_nhds (by norm_num : (0 : ℝ) < 1))
64   apply hs.of_norm_bounded_eventually_nat
65   filter_upwards [hb] with m hm
66   rw [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg (Real.rpow_nonneg (hy m).le _) (Real.exp_pos _).le)]
67   apply (le_div_iff₀ (Real.rpow_pos_of_pos (hy m) 2)).mpr
68   rw [Function.comp_apply, Real.rpow_add (hy m)] at hm
69   nlinarith
70 
71 /-- A summable majorant uniform on each bounded set of complex parameters.
72 The finitely many early indices are handled by the cofinite Weierstrass test. -/
73 theorem exponentialZetaDifference_majorant {x y : ℕ → ℝ}
74     (hy : ∀ m, 0 < y m) (hxT : Tendsto x atTop atTop) (hyT : Tendsto y atTop atTop)
75     (hs : Summable (fun m => 1 / y m ^ (2 : ℝ)))
76     {C γ : ℝ} (_hC : 0 < C) (hγ : 0 < γ)
77     (hclose : ∀ᶠ m in atTop, |x m - y m| ≤ C * Real.exp (-γ * y m))
78     {K : ℝ} (hK : 0 < K) :
79     ∃ u : ℕ → ℝ, Summable u ∧ ∀ᶠ m in atTop, ∀ s : ℂ, ‖s‖ ≤ K →
80       ‖exponentialZetaDifference x y m s‖ ≤ u m := by
81   let u := fun m => (2 * K * C) * (y m ^ K * Real.exp (-γ * y m))
82   have hu : Summable u := (summable_polynomial_exponential hy hyT hs K hγ).mul_left _
83   have ht := hyT.const_mul_atTop_of_neg (neg_lt_zero.mpr hγ)
84   have he := (Real.tendsto_exp_atBot.comp ht).const_mul (K * C)
85   simp only [mul_zero] at he
86   have hsmall := he.eventually (eventually_le_nhds (by norm_num : (0 : ℝ) < 1))
87   refine ⟨u, hu, ?_⟩
88   filter_upwards [hxT.eventually_ge_atTop 1, hyT.eventually_ge_atTop 1, hclose, hsmall]
89     with m hxm hym hcm hsm
90   intro s hsmK
91   have hl : |Real.log (x m) - Real.log (y m)| ≤ C * Real.exp (-γ * y m) :=
92     (real_log_lipschitz_one hxm hym).trans hcm
93   have hz : ‖-s * ((Real.log (x m) - Real.log (y m) : ℝ) : ℂ)‖ ≤
94       K * (C * Real.exp (-γ * y m)) := by
95     rw [norm_mul, norm_neg, Complex.norm_real, Real.norm_eq_abs]
96     exact mul_le_mul hsmK hl (abs_nonneg _) hK.le
97   have hz1 : ‖-s * ((Real.log (x m) - Real.log (y m) : ℝ) : ℂ)‖ ≤ 1 := by
98     apply hz.trans
99     simpa only [Function.comp_apply, mul_assoc] using hsm
100   have hb := (Complex.norm_exp_sub_one_le hz1).trans (mul_le_mul_of_nonneg_left hz (by norm_num))
101   rw [exponentialZetaDifference, exponentialZetaDifference_factor, norm_mul]
102   calc
103     _ ≤ y m ^ K * (2 * (K * (C * Real.exp (-γ * y m)))) :=
104       mul_le_mul (positiveZetaTerm_norm_le_rpow hym hsmK) hb (norm_nonneg _)
105         (Real.rpow_nonneg (hy m).le _)
106     _ = u m := by dsimp [u]; ring
107 
108 theorem exponentialZetaDifference_locally_uniform {x y : ℕ → ℝ}
109     (hy : ∀ m, 0 < y m) (hxT : Tendsto x atTop atTop) (hyT : Tendsto y atTop atTop)
110     (hs : Summable (fun m => 1 / y m ^ (2 : ℝ)))
111     {C γ : ℝ} (hC : 0 < C) (hγ : 0 < γ)
112     (hclose : ∀ᶠ m in atTop, |x m - y m| ≤ C * Real.exp (-γ * y m)) :
113     HasSumLocallyUniformlyOn (exponentialZetaDifference x y)
114       (fun s => ∑' m, exponentialZetaDifference x y m s) univ := by
115   apply hasSumLocallyUniformlyOn_of_of_forall_exists_nhds
116   intro s _
117   obtain ⟨u, hu, hbound⟩ := exponentialZetaDifference_majorant hy hxT hyT hs hC hγ hclose
118     (show 0 < ‖s‖ + 1 by positivity)
119   refine ⟨ball 0 (‖s‖ + 1), mem_nhdsWithin_of_mem_nhds
120     (isOpen_ball.mem_nhds (by simp only [mem_ball, dist_zero_right]; linarith)), ?_⟩
121   apply HasSumUniformlyOn.of_norm_le_summable_eventually hu
122   rw [Nat.cofinite_eq_atTop]
123   filter_upwards [hbound] with m hm
124   intro z hz
125   exact hm z (le_of_lt (by simpa only [mem_ball, dist_zero_right] using hz))
126 
127 theorem exponentialZetaDifference_sum_entire {x y : ℕ → ℝ}
128     (hy : ∀ m, 0 < y m) (hxT : Tendsto x atTop atTop) (hyT : Tendsto y atTop atTop)
129     (hs : Summable (fun m => 1 / y m ^ (2 : ℝ)))
130     {C γ : ℝ} (hC : 0 < C) (hγ : 0 < γ)
131     (hclose : ∀ᶠ m in atTop, |x m - y m| ≤ C * Real.exp (-γ * y m)) :
132     Differentiable ℂ (fun s => ∑' m, exponentialZetaDifference x y m s) := by
133   apply differentiableOn_univ.mp
134   exact (exponentialZetaDifference_locally_uniform hy hxT hyT hs hC hγ hclose).summableLocallyUniformlyOn.differentiableOn isOpen_univ
135     (fun m s _ => exponentialZetaDifference_entire x y m s)
136 
137 end
138 end Komorebi.PaperIV

Back to source controls