FKS2.floor_row11

theorem floor_row11 : ∀ x ∈ Set.Icc (Real.exp (3.5:ℝ)) (Real.exp (10:ℝ)),    Eπ x ≤ x ^ (-(1:ℝ)/100) := by  intro x hx  have hcurve : ∀ y, Real.exp (3.5:ℝ) ≤ y →      Expr.eval (fun _ => Real.sqrt (Real.log y)) (expSplitNegXpow 100)        ≤ y ^ (-(1:ℝ)/(100:ℕ)) := 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 h35 : (3.5:ℝ) ≤ Real.log y := by        rw [← Real.log_exp (3.5:ℝ)]; exact Real.log_le_log (Real.exp_pos _) hy      linarith    exact le_of_eq (eval_expSplitNegXpow_eq_xpow 100 (by norm_num) y hypos hyL)  have h := floor_xpow_of_check (expSplitNegXpow 100) 100 (3.5:ℝ) (187/100) 26 (by norm_num)    (by rw [show ((187/100:ℚ):ℝ) = 1.87 by norm_num,          show (1.87:ℝ) = Real.sqrt (1.87^2) from (Real.sqrt_sq (by norm_num)).symm]        exact Real.sqrt_le_sqrt (by norm_num))    (by have h316 : Real.sqrt 10 ≤ 3.163 := by          rw [show (3.163:ℝ) = Real.sqrt (3.163^2) from (Real.sqrt_sq (by norm_num)).symm]          exact Real.sqrt_le_sqrt (by norm_num)        push_cast; linarith [h316])    (lhsE_sub_negxpow_supported 100) floor_slab_check hcurve x hx  simpa using h