Source indexedtheorem · leanprover/lean4:v4.32.0

Rosser1941.p_n_lower

PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1047 to 1058

Source documentation

Some results from \cite{rosser1941}

Exact Lean statement

@[blueprint
  "thm:rosser1941-pn-lower"
  (title := "Rosser 1941, lower bound on $p_n$")
  (statement := /-- For $n \geq 55$, we have $p_n > n(\log n + \log\log n - 4)$. -/)
  (latexEnv := "theorem")]
theorem p_n_lower (n : ℕ) (hn : n ≥ 55) :
    nth_prime' n > n * (log n + log (log n) - 4)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "thm:rosser1941-pn-lower"  (title := "Rosser 1941, lower bound on $p_n$")  (statement := /-- For $n \geq 55$, we have $p_n > n(\log n + \log\log n - 4)$. -/)  (latexEnv := "theorem")]theorem p_n_lower (n : ℕ) (hn : n ≥ 55) :    nth_prime' n > n * (log n + log (log n) - 4) := 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 (by omega) h    · exact RS_prime_helper.p_n_lower_large n (by omega)  nlinarith [show (n : ℝ) > 0 from by positivity]