Source indexedtheorem · leanprover/lean4:v4.32.0

li.two_approx

PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions · PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean:202 to 217

Mathematical statement

Exact Lean statement

@[blueprint
  "Ramanujan-Soldner-constant"
  (title := "Ramanujan-Soldner constant")
  (statement := /-- $\li(2) = 1.0451\dots$. -/)
  (proof := /--
    Symmetrize the integral and use and some
    numerical integration. -/)
  (latexEnv := "lemma")
  (discussion := 759)]

theorem li.two_approx : li 2 ∈ Set.Icc 1.0451 1.0452

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "Ramanujan-Soldner-constant"  (title := "Ramanujan-Soldner constant")  (statement := /-- $\li(2) = 1.0451\dots$. -/)  (proof := /--    Symmetrize the integral and use and some    numerical integration. -/)  (latexEnv := "lemma")  (discussion := 759)] theorem li.two_approx : li 2 ∈ Set.Icc 1.0451 1.0452 := by  rw [li_eq_eulerMascheroni_add_log_log_add_tsum (show (1 : ℝ) < 2 by norm_num)]  have hll_lo : (-0.366513 : ℝ) ≤ Real.log (Real.log 2) := LogTables.log_log_2_gt  have hll_hi : Real.log (Real.log 2) ≤ -0.366512 := LogTables.log_log_2_lt   constructor <;> linarith [hs_lo, hs_hi, hγ_lo, hγ_hi]