Analytic estimates for multiplicative block constructions

Elementary logarithm and prime-count bounds used by both lower-bound constructions.

theorem RunsOfMultiples.log_le_two_sqrt {x : ℝ} (hx : 1 ≤ x) : Real.log x ≤ 2 * √x

theorem RunsOfMultiples.log_sq_le {x : ℝ} (hx : 1 ≤ x) : Real.log x ^ 2 ≤ 16 * √x

theorem RunsOfMultiples.sqrt_le_div_log {x : ℝ} (hx : 1 < x) : √x ≤ 2 * (x / Real.log x)

theorem RunsOfMultiples.sqrt_mul_log_le {x : ℝ} (hx : 1 < x) : √x * Real.log x ≤ 16 * (x / Real.log x)

theorem RunsOfMultiples.card_primesBelow_le (y : ℕ) (hy : 2 ≤ y) : ↑(y + 1).primesBelow.card ≤ (2 * Real.log 4 + 2) * (↑y / Real.log ↑y)

Chebyshev: π(y) ≤ (2 log 4 + 2) y / log y.