Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.FloorButhe8.rhsE8_le_rowcurve

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23Row8 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row8.lean:141 to 152

Mathematical statement

Exact Lean statement

theorem rhsE8_le_rowcurve (x : ℝ) (hL : (5 : ℝ) ≤ Real.log x) :
    Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE8
      ≤ admissible_bound 121.107 1.5 2 5.5666305 x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem rhsE8_le_rowcurve (x : ℝ) (hL : (5 : ℝ) ≤ Real.log x) :    Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE8      ≤ admissible_bound 121.107 1.5 2 5.5666305 x := by  have hLnn : (0:ℝ) ≤ Real.log x := le_trans (by norm_num) hL  rw [eval_rhsE8]  exact rowcurve_dom_three_halves 121.107 2 (9220/1000) (8478/10000) x hLnn    (by have h2 := R5_rpow_three_halves_le; have h3 := R5_rpow_three_halves_pos        have h1 : (9220/1000:ℝ) ≤ 121.107 / 13.1338 := by norm_num        have h4 : (121.107:ℝ) / 13.1338 ≤ 121.107 / (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)