WeakPNT

formal source

  48
  49    **Note**: Exposed as an explicit hypothesis until a full Lean derivation
  50    is landed (Wiener-Ikehara Tauberian infrastructure). -/
  51theorem WeakPNT
  52    (hWeak :
  53      Tendsto (fun N ↦ (∑ n ∈ Finset.Iic N, ArithmeticFunction.vonMangoldt n) / N)
  54        atTop (nhds 1)) :
  55    Tendsto (fun N ↦ (∑ n ∈ Finset.Iic N, ArithmeticFunction.vonMangoldt n) / N)
  56    atTop (nhds 1) := hWeak
  57
  58/-- **TECHNICAL SCAFFOLD**: Chebyshev ψ is asymptotic to x. -/
  59theorem ChebyshevPsi_asymptotic
  60    (hPsi :
  61      (fun x ↦ ∑ n ∈ Finset.Iic ⌊x⌋₊, ArithmeticFunction.vonMangoldt n) ~[atTop] id) :
  62    (fun x ↦ ∑ n ∈ Finset.Iic ⌊x⌋₊, ArithmeticFunction.vonMangoldt n) ~[atTop] id
  63  := hPsi
  64
  65/-! ## Medium Prime Number Theorem -/
  66
  67/-- **TECHNICAL SCAFFOLD**: Medium Prime Number Theorem.
  68
  69    There exists c > 0 such that:
  70    ψ(x) - x = O(x · exp(-c · (log x)^{1/10}))
  71
  72    **Note**: Exposed as an explicit hypothesis until the full complex-analytic
  73    derivation is imported. -/
  74theorem MediumPNT
  75    (hMedium : ∃ c > 0,
  76      (ψ - id) =O[atTop]
  77      fun (x : ℝ) ↦ x * Real.exp (-c * (Real.log x) ^ ((1 : ℝ) / 10))) :
  78    ∃ c > 0,
  79    (ψ - id) =O[atTop]
  80    fun (x : ℝ) ↦ x * Real.exp (-c * (Real.log x) ^ ((1 : ℝ) / 10))
  81  := hMedium