Prime-distribution API

This module is the stable facade over the ported PNTAnd implementation.

theorem AnalyticNumberTheory.PrimeDistribution.chebyshevPsi_medium_error : ∃ c > 0, (Chebyshev.psi - id) =O[Filter.atTop] fun (x : ℝ) => x * Real.exp (-c * Real.log x ^ (1 / 10))

A medium-strength prime number theorem for Chebyshev's psi function.

theorem AnalyticNumberTheory.PrimeDistribution.primeCounting_asymptotic_real : ∃ (c : ℝ → ℝ), (c =o[Filter.atTop] fun (x : ℝ) => 1) ∧ ∀ (x : ℝ), ↑⌊x⌋₊.primeCounting = (1 + c x) * x / Real.log x

The prime-counting PNT in the real-variable normal form proved by PNTAnd.

def AnalyticNumberTheory.PrimeDistribution.NatPrimeCountingPNT : Prop

A natural-number interface for the prime-counting PNT.

Equations

• AnalyticNumberTheory.PrimeDistribution.NatPrimeCountingPNT = ∃ (c : ℕ → ℝ), (c =o[Filter.atTop] fun (x : ℕ) => 1) ∧ ∀ (x : ℕ), ↑x.primeCounting = (1 + c x) * ↑x / Real.log ↑x

theorem AnalyticNumberTheory.PrimeDistribution.natPrimeCountingPNT : NatPrimeCountingPNT

Restrict the real-variable prime-counting PNT to natural arguments.

theorem AnalyticNumberTheory.PrimeDistribution.primeCounting_upper_bound : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℕ), 2 ≤ x → ↑x.primeCounting ≤ C * ↑x / Real.log ↑x

Upper bound for π: the PNT supplies a constant such that π(x) ≤ C·x/log x uniformly for x ≥ 2. This gives the analytic bound ≤ C·N/(a·log(N/a)) for switchingCount ≤ π(N/a) in the three-factor main-term estimate.