IndisputableMonolith.NumberTheory.Port.PNT

   1/-
   2Copyright (c) 2024 Various Authors. All rights reserved.
   3Ported from github.com/jonwashburn/riemann (PrimeNumberTheoremAnd/)
   4Released under Apache 2.0 license.
   5
   6# Prime Number Theorem (Ported)
   7
   8This module contains key Prime Number Theorem results ported from the
   9PrimeNumberTheoremAnd project.
  10
  11## Key Results
  12
  13- `MediumPNT`: ψ(x) = x + O(x exp(-c (log x)^{1/10}))
  14- `WeakPNT`: ∑_{n≤N} Λ(n) / N → 1
  15- `prime_between`: For any ε > 0, there exist arbitrarily large primes in [x, x(1+ε)]
  16
  17## References
  18
  19- Prime Number Theorem (Hadamard, de la Vallée-Poussin, 1896)
  20- Zero-free region approach to PNT
  21-/
  22
  23import Mathlib
  24import IndisputableMonolith.NumberTheory.Primes.Basic
  25
  26noncomputable section
  27
  28namespace IndisputableMonolith.NumberTheory.Port.PNT
  29
  30open Filter Asymptotics Real Nat
  31open scoped BigOperators ArithmeticFunction
  32
  33/-! ## Chebyshev Functions -/
  34
  35/-- The Chebyshev ψ function: ψ(x) = ∑_{n≤x} Λ(n) -/
  36def ChebyshevPsi (x : ℝ) : ℝ :=
  37  ∑ n ∈ Finset.Iic ⌊x⌋₊, ArithmeticFunction.vonMangoldt n
  38
  39/-- Local notation for Chebyshev ψ -/
  40local notation "ψ" => ChebyshevPsi
  41
  42/-! ## Weak Prime Number Theorem -/
  43
  44/-- **TECHNICAL SCAFFOLD**: Weak Prime Number Theorem.
  45
  46    The average of the von Mangoldt function tends to 1:
  47    ∑_{n≤N} Λ(n) / N → 1 as N → ∞
  48
  49    **Note**: Exposed as an explicit hypothesis until a full Lean derivation
  50    is landed (Wiener-Ikehara Tauberian infrastructure). -/
  51theorem WeakPNT
  52    (hWeak :
  53      Tendsto (fun N ↦ (∑ n ∈ Finset.Iic N, ArithmeticFunction.vonMangoldt n) / N)
  54        atTop (nhds 1)) :
  55    Tendsto (fun N ↦ (∑ n ∈ Finset.Iic N, ArithmeticFunction.vonMangoldt n) / N)
  56    atTop (nhds 1) := hWeak
  57
  58/-- **TECHNICAL SCAFFOLD**: Chebyshev ψ is asymptotic to x. -/
  59theorem ChebyshevPsi_asymptotic
  60    (hPsi :
  61      (fun x ↦ ∑ n ∈ Finset.Iic ⌊x⌋₊, ArithmeticFunction.vonMangoldt n) ~[atTop] id) :
  62    (fun x ↦ ∑ n ∈ Finset.Iic ⌊x⌋₊, ArithmeticFunction.vonMangoldt n) ~[atTop] id
  63  := hPsi
  64
  65/-! ## Medium Prime Number Theorem -/
  66
  67/-- **TECHNICAL SCAFFOLD**: Medium Prime Number Theorem.
  68
  69    There exists c > 0 such that:
  70    ψ(x) - x = O(x · exp(-c · (log x)^{1/10}))
  71
  72    **Note**: Exposed as an explicit hypothesis until the full complex-analytic
  73    derivation is imported. -/
  74theorem MediumPNT
  75    (hMedium : ∃ c > 0,
  76      (ψ - id) =O[atTop]
  77      fun (x : ℝ) ↦ x * Real.exp (-c * (Real.log x) ^ ((1 : ℝ) / 10))) :
  78    ∃ c > 0,
  79    (ψ - id) =O[atTop]
  80    fun (x : ℝ) ↦ x * Real.exp (-c * (Real.log x) ^ ((1 : ℝ) / 10))
  81  := hMedium
  82
  83/-! ## Strong PNT (Partial) -/
  84
  85/-- **TECHNICAL SCAFFOLD**: Strong Prime Number Theorem (Partial).
  86
  87    Under the Riemann Hypothesis:
  88    ψ(x) - x = O(√x · log² x). -/
  89theorem StrongPNT_conditional (hRH : True) -- RH placeholder
  90    (hStrong : ∃ C > 0, (ψ - id) =O[atTop] fun x ↦ Real.sqrt x * (Real.log x) ^ 2) :
  91    ∃ C > 0, (ψ - id) =O[atTop] fun x ↦ Real.sqrt x * (Real.log x) ^ 2
  92  := hStrong
  93
  94/-! ## Consequences for Prime Counting -/
  95
  96/-- **TECHNICAL SCAFFOLD**: Prime between consecutive integers for large N. -/
  97theorem prime_between {ε : ℝ} (hε : 0 < ε)
  98    (hPrimeBetween :
  99      ∃ N₀ : ℕ, ∀ x : ℝ, N₀ ≤ x → ∃ p : ℕ, Nat.Prime p ∧ x < p ∧ (p : ℝ) ≤ x * (1 + ε)) :
 100    ∃ N₀ : ℕ, ∀ x : ℝ, N₀ ≤ x → ∃ p : ℕ, Nat.Prime p ∧ x < p ∧ (p : ℝ) ≤ x * (1 + ε)
 101  := hPrimeBetween
 102
 103/-- **TECHNICAL SCAFFOLD**: Prime counting function asymptotic (π(x) ~ x / log x). -/
 104theorem prime_counting_asymptotic_pnt
 105    (hPNT :
 106      (fun x ↦ (Nat.primeCounting ⌊x⌋₊ : ℝ)) ~[atTop] (fun x ↦ x / Real.log x)) :
 107    (fun x ↦ (Nat.primeCounting ⌊x⌋₊ : ℝ)) ~[atTop] (fun x ↦ x / Real.log x)
 108  := hPNT
 109
 110/-!
 111Verification roadmap for PNT scaffolds:
 1121. **WeakPNT / ChebyshevPsi_asymptotic**: Replace with Mathlib theorems if available;
 113   otherwise cite classical PNT (Hadamard, de la Vallée-Poussin, 1896) and
 114   Tauberian arguments (Wiener–Ikehara).
 1152. **MediumPNT**: Cite de la Vallée-Poussin zero-free region bounds and
 116   standard explicit error term derivations.
 1173. **StrongPNT_conditional**: Use RH-conditional explicit bounds (e.g., Schoenfeld).
 1184. **prime_between / prime_counting_asymptotic_pnt**: Use PNT consequences or
 119   existing Mathlib results if present.
 120
 121Status note:
 122- Mathlib search for PNT/primeCounting asymptotics returned no direct theorems.
 123-/
 124
 125/-- **THEOREM**: Prime counting function asymptotic (π(x) ~ x / log x).
 126
 127    This is the classical form of the Prime Number Theorem. -/
 128theorem prime_counting_asymptotic :
 129    ((fun x ↦ (Nat.primeCounting ⌊x⌋₊ : ℝ)) ~[atTop] (fun x ↦ x / Real.log x)) →
 130    ((fun x ↦ (Nat.primeCounting ⌊x⌋₊ : ℝ)) ~[atTop] (fun x ↦ x / Real.log x)) := by
 131  intro hPNT
 132  exact prime_counting_asymptotic_pnt hPNT
 133
 134end IndisputableMonolith.NumberTheory.Port.PNT
 135