Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.FloorButhe7.rhsE7_le_rowcurve

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23Row7 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row7.lean:82 to 93

Mathematical statement

Exact Lean statement

theorem rhsE7_le_rowcurve (x : ℝ) (hL : (5 : ℝ) ≤ Real.log x) :
    Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE7
      ≤ admissible_bound 38.8 1.5 1.95 5.5666305 x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem rhsE7_le_rowcurve (x : ℝ) (hL : (5 : ℝ) ≤ Real.log x) :    Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE7      ≤ admissible_bound 38.8 1.5 1.95 5.5666305 x := by  have hLnn : (0:ℝ) ≤ Real.log x := le_trans (by norm_num) hL  rw [eval_rhsE7]  exact rowcurve_dom_three_halves 38.8 1.95 (2954/1000) (8266/10000) x hLnn    (by have h2 := R5_rpow_three_halves_le; have h3 := R5_rpow_three_halves_pos        have h1 : (2954/1000:ℝ) ≤ 38.8 / 13.1338 := by norm_num        have h4 : (38.8:ℝ) / 13.1338 ≤ 38.8 / (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)