Source indexedtheorem · leanprover/lean4:v4.32.0

Rosser1938.p_n_gt_2

PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:997 to 1008

Mathematical statement

Exact Lean statement

@[blueprint
  "thm:rosser1938-pn-lower"
  (title := "Rosser 1938, lower bound on $p_n$")
  (statement := /-- For $n > 1$, we have $p_n > n(\log n + \log\log n - 10)$. -/)
  (latexEnv := "theorem")]
theorem p_n_gt_2 (n : ℕ) (hn : n > 1) :
    nth_prime' n > n * (log n + log (log n) - 10)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "thm:rosser1938-pn-lower"  (title := "Rosser 1938, lower bound on $p_n$")  (statement := /-- For $n > 1$, we have $p_n > n(\log n + \log\log n - 10)$. -/)  (latexEnv := "theorem")]theorem p_n_gt_2 (n : ℕ) (hn : n > 1) :    nth_prime' n > n * (log n + log (log n) - 10) := by  have h_rs : (nth_prime' n : ℝ) > n * (log n + log (log n) - 3 / 2) := by    by_cases h : n ≤ 31    · exact RS_prime_helper.p_n_lower_small n hn h    · exact RS_prime_helper.p_n_lower_large n (by omega)  nlinarith [show (n : ℝ) > 0 from by positivity]