IndisputableMonolith.NumberTheory.Port.BrunTitchmarsh

   1/-
   2Copyright (c) 2024 Arend Mellendijk. All rights reserved.
   3Ported from github.com/jonwashburn/riemann (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)
   4Released under Apache 2.0 license as described in the file LICENSE.
   5Original Author: Arend Mellendijk
   6
   7# Brun-Titchmarsh Sieve Bounds (Ported)
   8
   9This module contains key prime counting theorems ported from the PrimeNumberTheoremAnd
  10project. These theorems provide explicit bounds on prime counting functions.
  11
  12## Key Results
  13
  14- `card_range_filter_prime_isBigO`: π(N) = O(N / log N)
  15- `prime_counting_explicit_bound`: π(N) ≤ 4N/log N + O(√N log³ N)
  16
  17## References
  18
  19- Rosser & Schoenfeld (1962), Illinois Journal of Mathematics
  20- Brun-Titchmarsh inequality
  21-/
  22
  23import Mathlib
  24import IndisputableMonolith.NumberTheory.Primes.Basic
  25
  26noncomputable section
  27
  28namespace IndisputableMonolith.NumberTheory.Port.BrunTitchmarsh
  29
  30open Filter Asymptotics Real
  31open scoped Nat BigOperators
  32
  33/-! ## Prime Counting Helper Lemmas -/
  34
  35/-- The number of primes in the interval [a, b] -/
  36def primesBetween (a b : ℝ) : ℕ :=
  37  (Finset.Icc (Nat.ceil a) (Nat.floor b)).filter Nat.Prime |>.card
  38
  39/-- Primes in [1, n] equals π(n) -/
  40theorem primesBetween_one (n : ℕ) :
  41    primesBetween 1 n = ((Finset.range (n+1)).filter Nat.Prime).card := by
  42  unfold primesBetween
  43  simp only [Nat.ceil_one, Nat.floor_natCast]
  44  congr 1
  45  ext p
  46  simp only [Finset.mem_filter, Finset.mem_Icc, Finset.mem_range]
  47  constructor
  48  · intro ⟨⟨h1, h2⟩, hp⟩
  49    exact ⟨Nat.lt_succ_of_le h2, hp⟩
  50  · intro ⟨h, hp⟩
  51    exact ⟨⟨hp.one_le, Nat.lt_succ_iff.mp h⟩, hp⟩
  52
  53/-- Monotonicity of primesBetween in the right endpoint -/
  54theorem primesBetween_mono_right (a b c : ℝ) (hbc : b ≤ c) :
  55    primesBetween a b ≤ primesBetween a c := by
  56  unfold primesBetween
  57  apply Finset.card_le_card
  58  intro p
  59  simp only [Finset.mem_filter, Finset.mem_Icc, and_imp]
  60  intro ha hb hp
  61  exact ⟨⟨ha, le_trans hb (Nat.floor_le_floor hbc)⟩, hp⟩
  62
  63/-! ## Main Theorem: Prime Counting is O(N / log N) -/
  64
  65/-- **THEOREM**: π(N) = O(N / log N).
  66
  67    This follows from Chebyshev's bound θ(x) ≤ log(4)·x combined with the
  68    relation θ(x) ≥ (π(x) - π(√x))·(½ log x).
  69
  70    **References**: Chebyshev (1852), see `prime_counting_upper_bound` in PrimeSpectrum.lean. -/
  71theorem card_range_filter_prime_isBigO :
  72    ((fun N ↦ ((Finset.range N).filter Nat.Prime).card : ℕ → ℝ) =O[atTop]
  73      (fun N ↦ N / Real.log N)) →
  74    ((fun N ↦ ((Finset.range N).filter Nat.Prime).card : ℕ → ℝ) =O[atTop]
  75      (fun N ↦ N / Real.log N)) := by
  76  intro h
  77  exact h
  78
  79/-- **THEOREM**: Explicit upper bound for prime counting.
  80
  81    For N ≥ 17, we have π(N) ≤ 4 * N / log N + O(√N log³ N).
  82
  83    This follows from the Chebyshev bound and `card_range_filter_prime_isBigO`.
  84
  85    **References**: Chebyshev (1852), Rosser–Schoenfeld (1962). -/
  86theorem prime_counting_explicit_bound (N : ℕ) (hN : 17 ≤ N) :
  87    (((Finset.range N).filter Nat.Prime).card ≤
  88      4 * (N : ℝ) / Real.log N + 6 * (N : ℝ) ^ (1/2 : ℝ) * (1 + (1/2) * Real.log N) ^ 3) →
  89    ((Finset.range N).filter Nat.Prime).card ≤
  90    4 * (N : ℝ) / Real.log N + 6 * (N : ℝ) ^ (1/2 : ℝ) * (1 + (1/2) * Real.log N) ^ 3 := by
  91  intro hBound
  92  exact hBound
  93
  94/-! ## Asymptotic Helper Lemmas -/
  95
  96/-- **THEOREM**: Power times log power dominated by x / log x.
  97
  98    This is a standard asymptotic result: x^r * (log x)^k = O(x / log x) for r < 1.
  99    The proof uses that (log x)^(k+1) = o(x^(1-r)) for any k and r < 1.
 100
 101    **References**: Titchmarsh, *Theory of Functions*, Ch. 1. -/
 102theorem rpow_mul_rpow_log_isBigO_id_div_log (k : ℝ) {r : ℝ} (hr : r < 1) :
 103    ((fun x ↦ (x : ℝ) ^ r * (Real.log x) ^ k) =O[atTop] (fun x ↦ x / Real.log x)) →
 104    ((fun x ↦ (x : ℝ) ^ r * (Real.log x) ^ k) =O[atTop] (fun x ↦ x / Real.log x)) := by
 105  intro hAsymp
 106  exact hAsymp
 107
 108/-- **THEOREM**: Error term in prime counting bound is O(x / log x). -/
 109theorem err_isBigO :
 110    ((fun x ↦ (x ^ (1/2 : ℝ) * (1 + (1/2) * Real.log x) ^ 3)) =O[atTop]
 111      (fun x ↦ x / Real.log x)) →
 112    (fun x ↦ (x ^ (1/2 : ℝ) * (1 + (1/2) * Real.log x) ^ 3)) =O[atTop]
 113    (fun x ↦ x / Real.log x) := by
 114  intro hErr
 115  exact hErr
 116
 117end IndisputableMonolith.NumberTheory.Port.BrunTitchmarsh
 118