prime_number_theorem_gap
Provedanalytic-number-theorynumber-theoryproved
Prime number theorem: π(x) ~ x/log x. Proved by Hadamard and de la Vallée Poussin (1896). Li(x) approximation is much better. Error term O(x exp(-c√log x)) is known; RH implies O(x^{1/2} log x).
Preamble
import Mathlib
Formal statement
import Mathlib
theorem prime_number_theorem_gap :
Filter.Tendsto (fun x : ℝ =>
(∑ p ∈ (Finset.range (Nat.floor x)).filter Nat.Prime, (1 : ℝ)) /
(x / Real.log x))
Filter.atTop (nhds 1) := by
sorrySource