Elementary prime estimates from Chebyshev bounds

The lower theta bound and prime interval estimates use Mathlib without the entropy upper bound.

theorem RunsOfMultiples.primesUpTo_eq (m : ℕ) : primesUpTo m = m.primesLE

theorem RunsOfMultiples.sum_primesUpTo_eq_theta (m : ℕ) : ∑ p ∈ primesUpTo m, Real.log ↑p = Chebyshev.theta ↑m

theorem RunsOfMultiples.log_le_mul_rpow {x ε : ℝ} (hx : 0 ≤ x) (hε : 0 < ε) : Real.log x ≤ ε⁻¹ * x ^ ε

log x ≤ k x^(1/k) for x ≥ 0, in the form we use.

theorem RunsOfMultiples.log_two_le_one : Real.log 2 ≤ 1

theorem RunsOfMultiples.theta_lower : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m : ℕ), Real.log 2 / 2 * ↑m - C ≤ Chebyshev.theta ↑m

Chebyshev lower bound in the form θ(m) ≥ (log 2 / 2) m - C.

theorem RunsOfMultiples.many_primes : ∃ (q₀ : ℕ), ∀ (q : ℕ), q₀ ≤ q → ↑q ^ (3 / 4) ≤ ↑(Finset.filter Nat.Prime (Finset.Ioc q (4 * q))).card

At least q^(3/4) primes in (q, 4q] for large q.