Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.floor_xhalf_row5

PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row5 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row5.lean:42 to 67

Source documentation

Row-5 Buthe floor [e^3, e^43] via floor_xhalf_of_check. (Named floor_xhalf_row5, not floor_row5, since FKS2.floor_row5 is already taken by Corollary 23's row 5 in the imported FKS2Cor23.lean base file - unrelated corollary, same row index.)

Exact Lean statement

theorem floor_xhalf_row5 : ∀ x ∈ Set.Icc (Real.exp (3:ℝ)) (Real.exp (43:ℝ)),
    Eπ x ≤ (Real.log x) ^ 3 * x ^ (-(1:ℝ) / 2)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem floor_xhalf_row5 : ∀ x ∈ Set.Icc (Real.exp (3:ℝ)) (Real.exp (43:ℝ)),    Eπ x ≤ (Real.log x) ^ 3 * x ^ (-(1:ℝ) / 2) := by  have hcurve : ∀ y, Real.exp (3:ℝ) ≤ y →      Expr.eval (fun _ => Real.sqrt (Real.log y)) (xhalfCurveE 1 6)        ≤ (Real.log y) ^ 3 * y ^ (-(1:ℝ) / 2) := by    intro y hy    have hypos : (0:ℝ) < y := lt_of_lt_of_le (Real.exp_pos _) hy    have hyL : (0:ℝ) ≤ Real.log y := by      have h3 : (3:ℝ) ≤ Real.log y := by        rw [← Real.log_exp (3:ℝ)]; exact Real.log_le_log (Real.exp_pos _) hy      linarith    refine le_of_eq ?_    have hsq : (Real.sqrt (Real.log y)) ^ 6 = (Real.log y) ^ 3 := by      rw [show (6:ℕ) = 2 * 3 from rfl, pow_mul, Real.sq_sqrt hyL]    rw [eval_xhalfCurveE 1 6 y hypos hyL, hsq]    push_cast; ring  exact floor_xhalf_of_check (xhalfCurveE 1 6)    (fun x => (Real.log x) ^ 3 * x ^ (-(1:ℝ) / 2)) 3 (173/100) 97 (by norm_num)    (by rw [show ((173/100:ℚ):ℝ) = 1.73 by norm_num,          show (1.73:ℝ) = Real.sqrt (1.73 ^ 2) from (Real.sqrt_sq (by norm_num)).symm]        exact Real.sqrt_le_sqrt (by norm_num))    (by have h656 : Real.sqrt 43 ≤ 6.56 := by          rw [show (6.56:ℝ) = Real.sqrt (6.56 ^ 2) from (Real.sqrt_sq (by norm_num)).symm]          exact Real.sqrt_le_sqrt (by norm_num)        push_cast; linarith [h656])    (xhalfCurve_sub_supported 1 6) floor_slab_check_row5 hcurve