Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.FloorButhe6.rhsE6_le_rowcurve

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23Row6 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row6.lean:86 to 97

Mathematical statement

Exact Lean statement

theorem rhsE6_le_rowcurve (x : ℝ) (hL : (5 : ℝ) ≤ Real.log x) :
    Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE6
      ≤ admissible_bound 12.4 1.5 1.9 5.5666305 x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem rhsE6_le_rowcurve (x : ℝ) (hL : (5 : ℝ) ≤ Real.log x) :    Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE6      ≤ admissible_bound 12.4 1.5 1.9 5.5666305 x := by  have hLnn : (0:ℝ) ≤ Real.log x := le_trans (by norm_num) hL  rw [eval_rhsE6]  exact rowcurve_dom_three_halves 12.4 1.9 (944/1000) (8054/10000) x hLnn    (by have h2 := R5_rpow_three_halves_le; have h3 := R5_rpow_three_halves_pos        have h1 : (944/1000:ℝ) ≤ 12.4 / 13.1338 := by norm_num        have h4 : (12.4:ℝ) / 13.1338 ≤ 12.4 / (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)