Zeta32 — Arith — Sum — PNT — PrimeWeightedAbel.

theorem Zeta32.ArithSum.PrimeSums.theta_eq_sum_Icc_cPrime (t : ℝ) : Chebyshev.theta t = ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, cPrime k

theorem Zeta32.ArithSum.PrimeSums.integral_theta_bounds {a b ε : ℝ} (hab : a ≤ b) (h : ∀ y ∈ Set.Icc a b, |Chebyshev.theta y - y| ≤ ε * y) : |(∫ (t : ℝ) in Set.Ioc a b, Chebyshev.theta t) - (b ^ 2 - a ^ 2) / 2| ≤ ε * (b ^ 2 - a ^ 2) / 2

theorem Zeta32.ArithSum.PrimeSums.wsum_close {a b η : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hη : 0 ≤ η) (h : ∀ y ∈ Set.Icc a b, |Chebyshev.theta y - y| ≤ η * y) : |wsum a b - (b ^ 2 - a ^ 2) / 2| ≤ 2 * η * b ^ 2