Effective Chebyshev theta estimate

This is the quantitative bridge from the PNTAnd estimate for psi to the prime-only Chebyshev function theta. It is the analytic input used by the Mertens partial-summation development.

theorem AnalyticNumberTheory.PrimeDistribution.chebyshevTheta_medium_error : ∃ c > 0, (Chebyshev.theta - id) =O[Filter.atTop] fun (x : ℝ) => √x + x * Real.exp (-c * Real.log x ^ (1 / 10))

The medium PNT error for psi transfers to theta, with the standard sqrt x prime-power correction retained explicitly.

theorem AnalyticNumberTheory.PrimeDistribution.chebyshevTheta_error : (Chebyshev.theta - id) =O[Filter.atTop] fun (x : ℝ) => x / Real.log x

A coarser theta estimate in the form used by partial summation.

theorem AnalyticNumberTheory.PrimeDistribution.chebyshevTheta_endpoint_error : (fun (x : ℝ) => (Chebyshev.theta x - x) / (x * Real.log x)) =O[Filter.atTop] fun (x : ℝ) => 1 / Real.log x ^ 2

The endpoint error in the Abel formula for reciprocal-prime sums.