Ported for Lean Pool from PrimeNumberTheoremAnd commit 0c7abf7be7765dc5ffd21afc1c37b018199ec3c9, via wewantmoore commit d59bd80ea93fabb9faf769e790ab47692645e022 (both Apache-2.0). The port adds the MooreBound namespace and updates Mathlib APIs and proof style. Wiener and Consequences retain the PNT and prime-interval dependency closure; unrelated later developments and LeanArchitect annotations are omitted.

theorem MooreBound.th43_b (x : ℝ) (hx : 2 ≤ x) : ↑⌊x⌋₊.primeCounting = Chebyshev.theta x / Real.log x + ∫ (t : ℝ) in Set.Icc 2 x, Chebyshev.theta t / (t * Real.log t ^ 2)

theorem Asymptotics.IsEquivalent.mooreBoundSubLittleO {α : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {u v w : α → β} {l : Filter α} (huv : IsEquivalent l u v) (hwu : (u - w) =o[l] v) : IsEquivalent l w v

theorem MooreBound.WeakPNT' : Filter.Tendsto (fun (N : ℕ) => (∑ n ≤ N, ArithmeticFunction.vonMangoldt n) / ↑N) Filter.atTop (nhds 1)

theorem MooreBound.WeakPNT'' : Asymptotics.IsEquivalent Filter.atTop Chebyshev.psi fun (x : ℝ) => x

An alternate form of the Weak PNT.

theorem MooreBound.isLittleO_sqrt_mul_log : (fun (x : ℝ) => √x * Real.log x) =o[Filter.atTop] id

√x · log x = o(x) as x → ∞.

theorem MooreBound.chebyshev_asymptotic : Asymptotics.IsEquivalent Filter.atTop Chebyshev.theta id

theorem MooreBound.chebyshev_asymptotic' : ∃ (f : ℝ → ℝ), (∀ ε > 0, f =o[Filter.atTop] fun (t : ℝ) => ε * t) ∧ (∀ (x : ℝ), 2 ≤ x → MeasureTheory.IntegrableOn f (Set.Icc 2 x) MeasureTheory.volume) ∧ ∀ (x : ℝ), Chebyshev.theta x = x + f x

theorem MooreBound.chebyshev_asymptotic'' : ∃ (f : ℝ → ℝ), (∀ ε > 0, f =o[Filter.atTop] fun (x : ℝ) => ε) ∧ (∀ (x : ℝ), 2 ≤ x → MeasureTheory.IntegrableOn f (Set.Icc 2 x) MeasureTheory.volume) ∧ ∀ x > 0, Chebyshev.theta x = x + x * f x

theorem MooreBound.continuousOn_log0 : ContinuousOn (fun (x : ℝ) => -1 / (x * Real.log x ^ 2)) {0, 1, -1}ᶜ

theorem MooreBound.continuousOn_log1 : ContinuousOn (fun (x : ℝ) => (Real.log x ^ 2)⁻¹ * x⁻¹) {0, 1, -1}ᶜ

theorem MooreBound.integral_log_inv (a b : ℝ) (ha : 2 ≤ a) (hb : a ≤ b) : ∫ (t : ℝ) in a..b, (Real.log t)⁻¹ = (Real.log b)⁻¹ * b - (Real.log a)⁻¹ * a + ∫ (t : ℝ) in a..b, (Real.log t ^ 2)⁻¹

theorem MooreBound.integral_log_inv' (a b : ℝ) (ha : 2 ≤ a) (hb : a ≤ b) : ∫ (t : ℝ) in Set.Icc a b, (Real.log t)⁻¹ = (Real.log b)⁻¹ * b - (Real.log a)⁻¹ * a + ∫ (t : ℝ) in Set.Icc a b, (Real.log t ^ 2)⁻¹

theorem MooreBound.integral_log_inv'' (a b : ℝ) (ha : 2 ≤ a) (hb : a ≤ b) : (Real.log a)⁻¹ * a + ∫ (t : ℝ) in Set.Icc a b, (Real.log t)⁻¹ = (Real.log b)⁻¹ * b + ∫ (t : ℝ) in Set.Icc a b, (Real.log t ^ 2)⁻¹

theorem MooreBound.integral_log_inv_pos (x : ℝ) (hx : 2 < x) : 0 < ∫ (t : ℝ) in Set.Icc 2 x, (Real.log t)⁻¹

theorem MooreBound.integral_log_inv_ne_zero (x : ℝ) (hx : 2 < x) : ∫ (t : ℝ) in Set.Icc 2 x, (Real.log t)⁻¹ ≠ 0

theorem MooreBound.pi_asymp_aux (x : ℝ) (hx : 2 ≤ x) : ↑⌊x⌋₊.primeCounting = (Real.log x)⁻¹ * Chebyshev.theta x + ∫ (t : ℝ) in Set.Icc 2 x, Chebyshev.theta t * (t * Real.log t ^ 2)⁻¹

theorem MooreBound.pi_asymp'' : (fun (x : ℝ) => (↑⌊x⌋₊.primeCounting / ∫ (t : ℝ) in Set.Icc 2 x, 1 / Real.log t) - 1) =o[Filter.atTop] fun (x : ℝ) => 1

theorem MooreBound.pi_asymp : ∃ (c : ℝ → ℝ), (c =o[Filter.atTop] fun (x : ℝ) => 1) ∧ ∀ᶠ (x : ℝ) in Filter.atTop, ↑⌊x⌋₊.primeCounting = (1 + c x) * ∫ (t : ℝ) in 2..x, 1 / Real.log t

theorem MooreBound.inv_div_log_asy : ∃ (c : ℝ), ∀ᶠ (x : ℝ) in Filter.atTop, ∫ (t : ℝ) in Set.Icc 2 x, 1 / Real.log t ^ 2 ≤ c * (x / Real.log x ^ 2)

theorem MooreBound.integral_log_inv_pialt (x : ℝ) (hx : 4 ≤ x) : ∫ (t : ℝ) in Set.Icc 2 x, 1 / Real.log t = x / Real.log x - 2 / Real.log 2 + ∫ (t : ℝ) in Set.Icc 2 x, 1 / Real.log t ^ 2

theorem MooreBound.integral_div_log_asymptotic : ∃ (c : ℝ → ℝ), (c =o[Filter.atTop] fun (x : ℝ) => 1) ∧ ∀ᶠ (x : ℝ) in Filter.atTop, ∫ (t : ℝ) in Set.Icc 2 x, 1 / Real.log t = (1 + c x) * x / Real.log x

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

theorem MooreBound.prime_in_gap' (a b : ℕ) (h : a.primeCounting < b.primeCounting) : ∃ (p : ℕ), Nat.Prime p ∧ a + 1 ≤ p ∧ p < b + 1

theorem MooreBound.prime_in_gap (a b : ℝ) (ha : 0 < a) (h : ⌊a⌋₊.primeCounting < ⌊b⌋₊.primeCounting) : ∃ (p : ℕ), Nat.Prime p ∧ a < ↑p ∧ ↑p ≤ b

theorem MooreBound.bound_f_second_term (f : ℝ → ℝ) (hf : Filter.Tendsto f Filter.atTop (nhds 0)) (δ : ℝ) (hδ : δ > 0) : ∀ᶠ (x : ℝ) in Filter.atTop, 1 + f x < 1 + δ

theorem MooreBound.bound_f_first_term {ε : ℝ} (hε : 0 < ε) (f : ℝ → ℝ) (hf : Filter.Tendsto f Filter.atTop (nhds 0)) (δ : ℝ) (hδ : δ > 0) : ∀ᶠ (x : ℝ) in Filter.atTop, 1 + f ((1 + ε) * x) > 1 - δ

theorem MooreBound.smaller_terms {ε : ℝ} (hε : 0 < ε) (f : ℝ → ℝ) (hf : Filter.Tendsto f Filter.atTop (nhds 0)) (δ : ℝ) (hδ : δ > 0) : ∀ᶠ (x : ℝ) in Filter.atTop, (1 - δ) * ((1 + ε) * x / Real.log ((1 + ε) * x)) < (1 + f ((1 + ε) * x)) * ((1 + ε) * x / Real.log ((1 + ε) * x))

theorem MooreBound.second_smaller_terms (f : ℝ → ℝ) (hf : Filter.Tendsto f Filter.atTop (nhds 0)) (δ : ℝ) (hδ : δ > 0) : ∀ᶠ (x : ℝ) in Filter.atTop, (1 + δ) * (x / Real.log x) > (1 + f x) * (x / Real.log x)

theorem MooreBound.x_log_x_atTop : Filter.Tendsto (fun (x : ℝ) => x / Real.log x) Filter.atTop Filter.atTop

theorem MooreBound.tendsto_by_squeeze (ε : ℝ) (hε : ε > 0) : Filter.Tendsto (fun (x : ℝ) => ↑⌊(1 + ε) * x⌋₊.primeCounting - ↑⌊x⌋₊.primeCounting) Filter.atTop Filter.atTop

theorem MooreBound.prime_between {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∃ (p : ℕ), Nat.Prime p ∧ x < ↑p ∧ ↑p < (1 + ε) * x