FKS2.corollary_24_row2

theorem corollary_24_row2 :    ∀ x, Real.log x ∈ Set.Icc (1:ℝ) 65.65 →      Eπ x ≤ (Real.log x) ^ (3/2 : ℝ) * x ^ (-(1:ℝ) / 2) := by  intro x hlog  obtain ⟨hlo, hhi⟩ := hlog  rcases lt_trichotomy x 0 with hxneg | hx0 | hxpos  · -- x < 0: `x^{-1/2} = exp(...)·cos(-π/2) = 0`, so RHS = 0; and `Eπ x ≤ 0`    have hLpos : (0:ℝ) < Real.log x := by linarith    have hEle0 : Eπ x ≤ 0 := by      unfold Eπ      apply div_nonpos_of_nonneg_of_nonpos (abs_nonneg _)      exact le_of_lt (div_neg_of_neg_of_pos hxneg hLpos)    have hxhalf0 : x ^ (-(1:ℝ) / 2) = 0 := by      rw [Real.rpow_def_of_neg hxneg,        show (-(1:ℝ) / 2) * π = -(π / 2) by ring, Real.cos_neg, Real.cos_pi_div_two, mul_zero]    rw [hxhalf0, mul_zero]    exact hEle0  · -- x = 0: `log 0 = 0` contradicts `1 ≤ log x`    exfalso; rw [hx0, Real.log_zero] at hlo; linarith  · -- x > 0: dispatch to the three segments split at `log x = 8, 43`    have cvt : ∀ a b : ℝ, a ≤ Real.log x → Real.log x ≤ b →        x ∈ Set.Icc (Real.exp a) (Real.exp b) := by      intro a b ha hb      exact ⟨by rw [← Real.exp_log hxpos]; exact Real.exp_le_exp.mpr ha,             by rw [← Real.exp_log hxpos]; exact Real.exp_le_exp.mpr hb⟩    rcases le_total (Real.log x) 8 with h1 | h1    · exact floor_trusted_row2 x (cvt 1 8 hlo h1)    · rcases le_total (Real.log x) 43 with h2 | h2      · exact floor_row2 x (cvt 8 43 h1 h2)      · exact band_row2 x (cvt 43 65.65 h2 hhi)