FKS2.Floor.linear_le_curve

theorem linear_le_curve {x : ℝ} (hx2 : 2 ≤ x) (hxe : x ≤ exp 10) :    4/5 + (5/3) * log x ≤ admissible_bound 9.2211 (3 / 2) 0.8476 1 x := by  have hlogx_nn : 0 ≤ log x := log_nonneg (by linarith)  have hlogx_lo : log 2 ≤ log x := log_le_log (by norm_num) hx2  have hlogx_hi : log x ≤ 10 := by    rw [show (10:ℝ) = log (exp 10) by rw [log_exp]]; exact log_le_log (by positivity) hxe  set s := Real.sqrt (log x) with hs_def  have hs2 : s ^ 2 = log x := Real.sq_sqrt hlogx_nn  have hgl : cbps.getLast (by decide) = (323/100 : ℚ) := by native_decide  have hs_mem : s ∈ Set.Icc ((83/100 : ℚ) : ℝ) ((cbps.getLast (by decide) : ℚ) : ℝ) := by    rw [hgl]    refine ⟨?_, ?_⟩    · have h1 : ((83/100 : ℚ):ℝ) ^ 2 ≤ log x := by        have he : ((83/100 : ℚ):ℝ) ^ 2 = 6889/10000 := by norm_num        rw [he]; nlinarith [hlogx_lo, Real.log_two_gt_d9]      calc ((83/100 : ℚ):ℝ) = Real.sqrt (((83/100 : ℚ):ℝ) ^ 2) :=            (Real.sqrt_sq (by norm_num)).symm        _ ≤ Real.sqrt (log x) := Real.sqrt_le_sqrt h1        _ = s := hs_def.symm    · have h2 : log x ≤ ((323/100 : ℚ):ℝ) ^ 2 := by        have he : ((323/100 : ℚ):ℝ) ^ 2 = 104329/10000 := by norm_num        rw [he]; linarith [hlogx_hi]      calc s = Real.sqrt (log x) := hs_def        _ ≤ Real.sqrt (((323/100 : ℚ):ℝ) ^ 2) := Real.sqrt_le_sqrt h2        _ = ((323/100 : ℚ):ℝ) := Real.sqrt_sq (by norm_num)  have hcov := cover_cmp s hs_mem  simp only [fExpr, gExpr, Expr.eval_add, Expr.eval_mul, Expr.eval_const, Expr.eval_var,    Expr.eval_exp] at hcov  -- LHS: 4/5 + 5/3 * (s*s) = 4/5 + 5/3 * log x  rw [show s * s = log x by rw [← sq]; exact hs2] at hcov  have hlogx_pos : (0:ℝ) < log x := lt_of_lt_of_le (log_pos (by norm_num)) hlogx_lo  unfold admissible_bound  simp only [div_one]  have e1 : (log x) ^ ((3:ℝ)/2) = log x * s := by    rw [show log x * s = s ^ 3 by rw [← hs2]; ring, hs_def, Real.sqrt_eq_rpow,      ← Real.rpow_natCast ((log x) ^ ((1:ℝ)/2)) 3, ← Real.rpow_mul hlogx_nn]    norm_num  have e2 : (log x) ^ ((1:ℝ)/2) = s := by rw [hs_def, Real.sqrt_eq_rpow]  rw [e1, e2]  convert hcov using 2 <;> norm_num