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
proof body
Term-mode proof.
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. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.