Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.FloorButhe.rhsE_le_rowcurve

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean:390 to 401

Mathematical statement

Exact Lean statement

theorem rhsE_le_rowcurve (x : ℝ) (hL : (5 : ℝ) ≤ Real.log x) :
    Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE
      ≤ admissible_bound 2.22 1.5 1.5 5.5666305 x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem rhsE_le_rowcurve (x : ℝ) (hL : (5 : ℝ) ≤ Real.log x) :    Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE      ≤ admissible_bound 2.22 1.5 1.5 5.5666305 x := by  have hLnn : (0:ℝ) ≤ Real.log x := le_trans (by norm_num) hL  rw [eval_rhsE]  exact rowcurve_dom_three_halves 2.22 1.5 (169029/1000000) (63577/100000) x hLnn    (by have h2 := R5_rpow_three_halves_le; have h3 := R5_rpow_three_halves_pos        have h1 : (169029/1000000:ℝ) ≤ 2.22 / 13.1338 := by norm_num        have h4 : (2.22:ℝ) / 13.1338 ≤ 2.22 / (5.5666305:ℝ) ^ (1.5:ℝ) :=          div_le_div_of_nonneg_left (by norm_num) h3 h2        linarith)    (by rw [div_le_iff₀ sqrtR5_pos]; nlinarith [sqrtR5_lb]) (by norm_num)