The r-th prime is O(r log r)

From θ(x) ≥ x / 2 for large x (a consequence of theta_asymp) and θ(x) ≤ π(x) log x.

theorem IwaniecLinearSieve.log_le_div_eight {K : ℝ} (hK : 256 ≤ K) : Real.log K ≤ K / 8

theorem IwaniecLinearSieve.nth_prime_le : ∃ (C : ℝ), ∀ (r : ℕ), 2 ≤ r → ↑(Nat.nth Nat.Prime (r - 1)) ≤ C * ↑r * Real.log ↑r

The r-th prime p_r = Nat.nth Nat.Prime (r - 1) satisfies p_r ≤ C r log r.