prime_between

formal source

  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. -/