Zeta32 — Arith — Sum — PNT — PrimeThetaInterval.

noncomputable def Zeta32.ArithSum.PrimeSums.logSum (a b : ℝ) : ℝ

Sum of prime logarithms over the integer indices in the interval (a, b].

Equations

• Zeta32.ArithSum.PrimeSums.logSum a b = ∑ k ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊, Zeta5Irrational.cPrime k

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

theorem Zeta32.ArithSum.PrimeSums.logSum_eq_theta_sub {a b : ℝ} (hab : a ≤ b) : logSum a b = Chebyshev.theta b - Chebyshev.theta a

theorem Zeta32.ArithSum.PrimeSums.theta_ratio_tendsto : Filter.Tendsto (fun (x : ℝ) => Chebyshev.theta x / x) Filter.atTop (nhds 1)

theorem Zeta32.ArithSum.PrimeSums.theta_scaled_tendsto {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (x : ℝ) => Chebyshev.theta (c * x) / x) Filter.atTop (nhds c)

theorem Zeta32.ArithSum.PrimeSums.theta_interval_tendsto {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : Filter.Tendsto (fun (x : ℝ) => (Chebyshev.theta (b * x) - Chebyshev.theta (a * x)) / x) Filter.atTop (nhds (b - a))

theorem Zeta32.ArithSum.PrimeSums.logSum_scaled_tendsto {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : Filter.Tendsto (fun (x : ℝ) => logSum (a * x) (b * x) / x) Filter.atTop (nhds (b - a))

theorem Zeta32.ArithSum.PrimeSums.theta_interval_nat_tendsto {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : Filter.Tendsto (fun (n : ℕ) => (Chebyshev.theta (b * ↑n) - Chebyshev.theta (a * ↑n)) / ↑n) Filter.atTop (nhds (b - a))