FKS2.floor_row3

theorem floor_row3 : ∀ x ∈ Set.Icc (Real.exp (9:ℝ)) (Real.exp (43:ℝ)),    Eπ x ≤ (1 / (8 * π)) * (Real.log x) ^ 2 * x ^ (-(1:ℝ) / 2) := by  have hcurve : ∀ y, Real.exp (9:ℝ) ≤ y →      Expr.eval (fun _ => Real.sqrt (Real.log y)) (xhalfCurveE (79/2000) 4)        ≤ (1 / (8 * π)) * (Real.log y) ^ 2 * 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 h9 : (9:ℝ) ≤ Real.log y := by        rw [← Real.log_exp (9:ℝ)]; exact Real.log_le_log (Real.exp_pos _) hy      linarith    have hsq : (Real.sqrt (Real.log y)) ^ 4 = (Real.log y) ^ 2 := by      rw [show (4:ℕ) = 2 * 2 from rfl, pow_mul, Real.sq_sqrt hyL]    rw [eval_xhalfCurveE (79/2000) 4 y hypos hyL, hsq]    push_cast    have hc_le : (79/2000:ℝ) ≤ 1 / (8 * π) := by      rw [le_div_iff₀ (by positivity : (0:ℝ) < 8 * π)]      nlinarith [Real.pi_lt_d2]    have hnn : (0:ℝ) ≤ (Real.log y) ^ 2 * y ^ (-(1:ℝ) / 2) := by positivity    calc (79/2000:ℝ) * (Real.log y) ^ 2 * y ^ (-(1:ℝ) / 2)        = (79/2000:ℝ) * ((Real.log y) ^ 2 * y ^ (-(1:ℝ) / 2)) := by ring      _ ≤ (1 / (8 * π)) * ((Real.log y) ^ 2 * y ^ (-(1:ℝ) / 2)) :=          mul_le_mul_of_nonneg_right hc_le hnn      _ = (1 / (8 * π)) * (Real.log y) ^ 2 * y ^ (-(1:ℝ) / 2) := by ring  exact floor_xhalf_of_check (xhalfCurveE (79/2000) 4)    (fun x => (1 / (8 * π)) * (Real.log x) ^ 2 * x ^ (-(1:ℝ) / 2)) 9 3 74 (by norm_num)    (by rw [show ((3:ℚ):ℝ) = 3 by norm_num,          show (3:ℝ) = Real.sqrt (3 ^ 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 (79/2000) 4) floor_slab_check_row3 hcurve