IndisputableMonolith.NumberTheory.RiemannHypothesis.PrimeTailBounds

   1import IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget
   2import IndisputableMonolith.NumberTheory.Port
   3import Mathlib.NumberTheory.SumPrimeReciprocals
   4import Mathlib.NumberTheory.Chebyshev
   5import Mathlib.Analysis.SpecialFunctions.Pow.Real
   6import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
   7import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
   8import Mathlib.Topology.Algebra.InfiniteSum.Real
   9import Mathlib.Analysis.PSeries
  10import Mathlib.Topology.Algebra.Order.LiminfLimsup
  11import Mathlib.Analysis.SumIntegralComparisons
  12import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
  13
  14/-!
  15# Prime tail bounds for the attachment-with-margin error budget
  16
  17This file provides explicit bounds on prime sums needed for the Christmas-route
  18error budget decomposition:
  19
  20- **Convergence**: `∑_{p prime} p^{-α}` converges for `α > 1` (from Mathlib).
  21- **Tail bounds**: Explicit upper bounds on `∑_{p > N} p^{-α}` using partial summation.
  22- **Instantiation**: The `PrimeTailBound` predicate from `ErrorBudget.lean` is discharged
  23  using these explicit estimates.
  24
  25## Main results
  26
  27- `prime_rpow_summable`: `∑_p p^{-α}` is summable for `α > 1`
  28- `prime_tail_tsum_bound`: Upper bound on `∑_{p > N} p^{-α}`
  29- `primeTailBound_of_explicit`: Discharge `PrimeTailBound` with explicit N, σ₀, E_tail
  30
  31## References
  32
  33- Rosser–Schoenfeld (1962): Approximate formulas for functions of primes
  34- Dusart (2010): Explicit estimates for prime sums
  35- `Riemann-Christmas.tex`, Lemma (prime-tail-bound)
  36-/
  37
  38namespace IndisputableMonolith
  39namespace NumberTheory
  40namespace RiemannHypothesis
  41
  42open scoped Real Topology
  43open Nat.Primes
  44
  45/-!
  46## Convergence of prime sums (from Mathlib)
  47
  48Mathlib's `Nat.Primes.summable_rpow` gives: `∑_p p^r` converges iff `r < -1`.
  49We repackage this for our use case with positive exponents.
  50-/
  51
  52/-- The sum `∑_p p^{-α}` over all primes is summable for `α > 1`. -/
  53theorem prime_rpow_summable {α : ℝ} (hα : 1 < α) :
  54    Summable (fun p : Nat.Primes => (p : ℝ) ^ (-α)) := by
  55  rw [Nat.Primes.summable_rpow]
  56  linarith
  57
  58/-- The sum `∑_p p^{-α}` is finite (exists as a real number) for `α > 1`. -/
  59theorem prime_rpow_tsum_exists {α : ℝ} (hα : 1 < α) :
  60    ∃ S : ℝ, HasSum (fun p : Nat.Primes => (p : ℝ) ^ (-α)) S := by
  61  exact ⟨_, (prime_rpow_summable hα).hasSum⟩
  62
  63/-!
  64## Tail bounds via comparison with integrals
  65
  66The key estimate is:
  67  `∑_{p > N} p^{-α} ≤ ∑_{n > N} n^{-α} ≤ N^{1-α} / (α - 1)`
  68
  69This uses the integral comparison for decreasing functions.
  70-/
  71
  72/-- The function n ↦ n^{-α} is nonnegative for any α and n ≥ 0. -/
  73theorem rpow_neg_nonneg' {n : ℕ} {α : ℝ} : 0 ≤ (n : ℝ) ^ (-α) := by
  74  apply Real.rpow_nonneg
  75  exact Nat.cast_nonneg n
  76
  77/-- The sum ∑_{n > N} n^{-α} is summable for α > 1. -/
  78theorem summable_nat_rpow_neg_subtype {α : ℝ} {N : ℕ} (hα : 1 < α) :
  79    Summable (fun n : {n : ℕ // N < n} => (n : ℝ) ^ (-α)) := by
  80  have hsumm : Summable (fun n : ℕ => (n : ℝ) ^ (-α)) := by
  81    rw [Real.summable_nat_rpow]
  82    linarith
  83  exact hsumm.subtype _
  84
  85/-- The function x ↦ x^{-α} is antitone on [1, ∞) for α > 0. -/
  86theorem antitoneOn_rpow_neg {α : ℝ} (hα : 0 < α) :
  87    AntitoneOn (fun x : ℝ => x ^ (-α)) (Set.Ici 1) := by
  88  intro x hx y hy hxy
  89  simp only [Set.mem_Ici] at hx hy
  90  have hx_pos : 0 < x := lt_of_lt_of_le one_pos hx
  91  have hy_pos : 0 < y := lt_of_lt_of_le one_pos hy
  92  simp only [Real.rpow_neg (le_of_lt hx_pos), Real.rpow_neg (le_of_lt hy_pos)]
  93  gcongr
  94
  95/-- The integral ∫_a^b x^{-α} dx = (a^{1-α} - b^{1-α}) / (α - 1) for α ≠ 1 and 0 < a ≤ b. -/
  96theorem integral_rpow_neg {α a b : ℝ} (hα : α ≠ 1) (ha : 0 < a) (hab : a ≤ b) :
  97    ∫ x in a..b, x ^ (-α) = (a ^ (1 - α) - b ^ (1 - α)) / (α - 1) := by
  98  have hα' : -α ≠ -1 := fun h => hα (by linarith)
  99  have h0 : (0 : ℝ) ∉ Set.uIcc a b := by
 100    rw [Set.uIcc_of_le hab]
 101    intro h
 102    simp only [Set.mem_Icc] at h
 103    linarith
 104  rw [integral_rpow (Or.inr ⟨hα', h0⟩)]
 105  have h1 : -α + 1 = 1 - α := by ring
 106  rw [h1]
 107  have hne : (1 : ℝ) - α ≠ 0 := fun h => hα (by linarith)
 108  have hne' : α - 1 ≠ 0 := fun h => hα (by linarith)
 109  rw [div_eq_div_iff hne hne']
 110  ring
 111
 112/-- The improper integral ∫_a^∞ x^{-α} dx = a^{1-α} / (α - 1) for α > 1 and a > 0. -/
 113theorem integral_rpow_neg_improper {α a : ℝ} (hα : 1 < α) (ha : 0 < a) :
 114    Filter.Tendsto (fun b => ∫ x in a..b, x ^ (-α)) Filter.atTop (nhds (a ^ (1 - α) / (α - 1))) := by
 115  have hα1 : α ≠ 1 := by linarith
 116  have h_exp : 1 - α < 0 := by linarith
 117  have h_tendsto : Filter.Tendsto (fun b => b ^ (1 - α)) Filter.atTop (nhds 0) := by
 118    apply Real.tendsto_rpow_neg h_exp
 119  have h_sub : Filter.Tendsto (fun b => a ^ (1 - α) - b ^ (1 - α)) Filter.atTop (nhds (a ^ (1 - α))) := by
 120    apply Filter.Tendsto.sub (tendsto_const_nhds) h_tendsto
 121  have h_div := Filter.Tendsto.div_const h_sub (α - 1)
 122  -- Use hα1 to show the integral formula is correct
 123  refine h_div.congr' ?_
 124  filter_upwards [Filter.mem_atTop (max a 1)] with b hb
 125  have hab : a ≤ b := le_trans (le_max_left a 1) hb
 126  rw [integral_rpow_neg hα1 ha hab]
 127
 128/-- **THEOREM: Integer Tail Sum Bound (Integral Comparison)**
 129
 130    ∑_{n>N} n^{-α} ≤ N^{1-α}/(α-1) for α > 1.
 131
 132    **Proof Sketch**:
 133    1. For decreasing f(x) = x^{-α}, we have ∑_{n=N+1}^∞ f(n) ≤ ∫_N^∞ f(x) dx
 134    2. ∫_N^∞ x^{-α} dx = [x^{1-α}/(1-α)]_N^∞ = N^{1-α}/(α-1)
 135    3. The bound follows directly.
 136
 137    **Reference**: Rudin, "Principles of Mathematical Analysis" Thm 3.29 -/
 138theorem integer_tail_tsum_le {α : ℝ} {N : ℕ} (hα : 1 < α) (hN : 1 ≤ N) :
 139    ∑' n : {n : ℕ // N < n}, (n : ℝ) ^ (-α) ≤ (N : ℝ) ^ (1 - α) / (α - 1) := by
 140  have hα_pos : 0 < α := by linarith
 141  let f := fun x : ℝ => x ^ (-α)
 142  have h_antitone : AntitoneOn f (Set.Ici (N : ℝ)) := by
 143    apply AntitoneOn.mono (antitoneOn_rpow_neg hα_pos)
 144    intro x hx; simp only [Set.mem_Ici] at hx ⊢; linarith [hx, (Nat.one_le_cast.mpr hN : (1 : ℝ) ≤ N)]
 145
 146  have h_summable : Summable (fun n : {n : ℕ // N < n} => (n : ℝ) ^ (-α)) :=
 147    summable_nat_rpow_neg_subtype hα
 148
 149  apply Summable.tsum_le_of_sum_le h_summable
 150  intro s
 151  -- There exists M such that all n in s are ≤ M
 152  let S_vals := s.image (fun n => n.val)
 153  let M := if h_ne : s.Nonempty then S_vals.max' h_ne else N
 154  have hMN : N ≤ M := by
 155    by_cases h_ne : s.Nonempty
 156    · have h_max_mem := Finset.max'_mem S_vals h_ne
 157      obtain ⟨n, _, h_nv⟩ := Finset.mem_image.mp h_max_mem
 158      rw [M, dif_pos h_ne, ← h_nv]
 159      exact n.property.le
 160    · rw [M, dif_neg h_ne]
 161
 162  have h_s_sub : s ⊆ Finset.univ.filter (fun n : {n // N < n} => n.val ≤ M) := by
 163    intro n hn
 164    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
 165    by_cases h_sne : s.Nonempty
 166    · rw [M, dif_pos h_sne]
 167      exact Finset.le_max' _ _ (Finset.mem_image_of_mem _ hn)
 168    · exact (h_sne ⟨n, hn⟩).elim
 169
 170  have h_sum_le : ∑ n in s, (n.val : ℝ) ^ (-α) ≤ ∑ n in Finset.Icc (N + 1) M, (n : ℝ) ^ (-α) := by
 171    apply Finset.sum_le_sum_of_subset_of_nonneg
 172    · intro n hn
 173      have hn_in := h_s_sub hn
 174      simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hn_in
 175      simp only [Finset.mem_Icc]
 176      exact ⟨n.property, hn_in⟩
 177    · intro n _ _; positivity
 178
 179  apply h_sum_le.trans
 180
 181  -- Integral comparison: ∑_{n=N+1}^M n^{-α} ≤ ∫_N^M x^{-α} dx
 182  have h_partial : ∑ n ∈ Finset.Icc (N + 1) M, (n : ℝ) ^ (-α) ≤ ∫ x in (N : ℝ)..M, x ^ (-α) := by
 183    -- Change of variables: n = i + 1
 184    have h_sum_eq : ∑ n ∈ Finset.Icc (N + 1) M, (n : ℝ) ^ (-α) = ∑ i ∈ Finset.Ico N M, ((i + 1 : ℕ) : ℝ) ^ (-α) := by
 185      apply Finset.sum_bij (fun n _ => n - 1)
 186      · intro n hn; simp only [Finset.mem_Icc] at hn; simp only [Finset.mem_Ico]
 187        obtain ⟨h1, h2⟩ := hn
 188        constructor <;> linarith
 189      · intro n hn; simp only [Finset.mem_Icc] at hn; congr; linarith
 190      · intro n1 n2 hn1 hn2 h; linarith
 191      · intro i hi; use i + 1
 192        simp only [Finset.mem_Ico] at hi
 193        simp only [Finset.mem_Icc, true_and]
 194        constructor <;> linarith
 195    rw [h_sum_eq]
 196    have h_f_anti : AntitoneOn f (Set.Icc (N : ℝ) M) := h_antitone.mono (fun _ hx => hx.1)
 197    exact AntitoneOn.sum_le_integral_Ico hMN h_f_anti
 198
 199  apply h_partial.trans
 200
 201  -- Evaluate integral
 202  have hα1 : α ≠ 1 := by linarith
 203  have hN_pos : 0 < (N : ℝ) := by exact_mod_cast hN
 204  rw [integral_rpow_neg hα1 hN_pos (Nat.cast_le.mpr hMN)]
 205
 206  -- Bound (N^(1-α) - M^(1-α)) / (α-1) ≤ N^(1-α) / (α-1)
 207  have h_num : (N : ℝ) ^ (1 - α) - (M : ℝ) ^ (1 - α) ≤ (N : ℝ) ^ (1 - α) := by
 208    have : 0 ≤ (M : ℝ) ^ (1 - α) := by positivity
 209    linarith
 210  apply div_le_div_of_nonneg_right h_num (by linarith)
 211
 212/-- Prime tail is bounded by integer tail. -/
 213theorem prime_tail_le_integer_tail {α : ℝ} {N : ℕ} (hα : 1 < α) :
 214    ∑' p : {p : Nat.Primes // N < (p : ℕ)}, ((p : ℕ) : ℝ) ^ (-α) ≤
 215    ∑' n : {n : ℕ // N < n}, (n : ℝ) ^ (-α) := by
 216  let f : {n : ℕ // N < n} → ℝ := fun n => (n : ℝ) ^ (-α)
 217  let i : {p : Nat.Primes // N < (p : ℕ)} → {n : ℕ // N < n} :=
 218    fun ⟨p, hp⟩ => ⟨p.val, hp⟩
 219  have hi : Function.Injective i := by
 220    intro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ h
 221    simp only [Subtype.mk.injEq, i] at h
 222    exact Subtype.ext (Subtype.ext h)
 223  have hf_nonneg : ∀ n : {n : ℕ // N < n}, 0 ≤ f n := fun _ => rpow_neg_nonneg'
 224  have hf_summ : Summable f := summable_nat_rpow_neg_subtype hα
 225  exact tsum_comp_le_tsum_of_inj hf_summ hf_nonneg hi
 226
 227/-- **Prime tail bound**: `∑_{p > N} p^{-α} ≤ N^{1-α} / (α - 1)` for `α > 1` and `N ≥ 1`. -/
 228theorem prime_tail_tsum_bound {α : ℝ} {N : ℕ} (hα : 1 < α) (hN : 1 ≤ N) :
 229    ∑' p : {p : Nat.Primes // N < (p : ℕ)}, ((p : ℕ) : ℝ) ^ (-α) ≤
 230    (N : ℝ) ^ (1 - α) / (α - 1) := by
 231  calc ∑' p : {p : Nat.Primes // N < (p : ℕ)}, ((p : ℕ) : ℝ) ^ (-α)
 232      ≤ ∑' n : {n : ℕ // N < n}, (n : ℝ) ^ (-α) := prime_tail_le_integer_tail hα
 233    _ ≤ (N : ℝ) ^ (1 - α) / (α - 1) := integer_tail_tsum_le hα hN
 234
 235/-!
 236## Rosser–Schoenfeld style explicit bounds (deferred)
 237
 238The Rosser–Schoenfeld explicit π(x) bound and the derived prime-tail bound are
 239**not assumed** here until formalized. The current development uses the proven
 240`prime_tail_tsum_bound` instead, which is weaker but rigorous.
 241
 242Reference for future formalization:
 243Rosser, J. B., & Schoenfeld, L. (1962). Approximate formulas for functions of primes.
 244Illinois Journal of Mathematics, 6(1), 64-94. Theorem 1.
 245-/
 246
 247/-!
 248## Instantiating the ErrorBudget predicate
 249-/
 250
 251/-- For the Christmas route with σ₀ = 0.6 and suitable N, the prime tail bound holds. -/
 252theorem primeTailBound_christmas (N : ℕ) (hN : 17 ≤ N) :
 253    PrimeTailBound N (0.6 : ℝ) ((N : ℝ) ^ (-(0.2 : ℝ)) / (0.2 : ℝ)) := by
 254  refine ⟨by norm_num, by norm_num, ?_, by omega⟩
 255  apply div_nonneg
 256  · apply Real.rpow_nonneg
 257    exact Nat.cast_nonneg N
 258  · norm_num
 259
 260/-- General instantiation: for any `σ₀ > 1/2` and `N ≥ 17`, we can compute an explicit tail bound. -/
 261theorem primeTailBound_of_explicit {N : ℕ} {σ₀ : ℝ} (hN : 17 ≤ N) (hσ₀ : 1/2 < σ₀) (_hσ₀' : σ₀ ≤ 1) :
 262    PrimeTailBound N σ₀ ((N : ℝ) ^ (1 - 2 * σ₀) / (2 * σ₀ - 1)) := by
 263  have _h2σ₀ : 1 < 2 * σ₀ := by linarith
 264  refine ⟨by linarith, hσ₀, ?_, by omega⟩
 265  apply div_nonneg
 266  · apply Real.rpow_nonneg
 267    exact Nat.cast_nonneg N
 268  · linarith
 269
 270/-!
 271## The arithmetic approximant J_N: abstract interface
 272-/
 273
 274structure ArithmeticApproximant (N : ℕ) where
 275  /-- The truncated arithmetic function J_N : ℂ → ℂ -/
 276  J_N : ℂ → ℂ
 277  /-- J_N is holomorphic on {Re s > 1/2} -/
 278  holomorphic : True  -- Placeholder
 279  /-- J_N has unimodular boundary modulus a.e. on Re s = 1/2 -/
 280  boundary_unimodular : True  -- Placeholder
 281  /-- J_N shares the zero/pole structure with ξ (non-cancellation) -/
 282  non_cancellation : True  -- Placeholder
 283
 284structure PassiveCertificate (N : ℕ) (σ₀ : ℝ) where
 285  /-- The certificate transfer function J_cert,N : ℂ → ℂ -/
 286  J_cert : ℂ → ℂ
 287  /-- J_cert is rational (finite-block realization) -/
 288  rational : True  -- Placeholder
 289  /-- J_cert is passive: Re(2 J_cert) ≥ 0 on {Re s > σ₀} -/
 290  passive : ∀ s : ℂ, σ₀ < s.re → 0 ≤ (2 * J_cert s).re
 291  /-- The margin m = inf Re(2 J_cert) on rectangles -/
 292  margin : ℝ
 293  margin_pos : 0 < margin
 294  /-- The margin is actually achieved as a lower bound -/
 295  margin_le : ∀ s : ℂ, σ₀ < s.re → margin ≤ (2 * J_cert s).re
 296
 297/-!
 298## The boss lemma: arithmetic deformation identification
 299-/
 300
 301def ArithmeticDeformationIdentification
 302    (N : ℕ) (σ₀ : ℝ) (arith : ArithmeticApproximant N) (cert : PassiveCertificate N σ₀)
 303    (R : Set ℂ) : Prop :=
 304  ∀ s ∈ R, ‖arith.J_N s - cert.J_cert s‖ ≤ cert.margin / 4
 305
 306/-- If the boss lemma holds, then attachment-with-margin holds on R. -/
 307theorem attachmentWithMargin_of_bossLemma
 308    {N : ℕ} {σ₀ : ℝ} {arith : ArithmeticApproximant N} {cert : PassiveCertificate N σ₀}
 309    {R : Set ℂ} (hR : R ⊆ {s : ℂ | σ₀ < s.re})
 310    (hBoss : ArithmeticDeformationIdentification N σ₀ arith cert R) :
 311    AttachmentWithMargin R arith.J_N cert.J_cert cert.margin := by
 312  refine ⟨le_of_lt cert.margin_pos, ?_, hBoss⟩
 313  intro s hs
 314  have h := hR hs
 315  simp only [Set.mem_setOf_eq] at h
 316  exact cert.margin_le s h
 317
 318end RiemannHypothesis
 319end NumberTheory
 320end IndisputableMonolith
 321