FKS2.Floor.integral_etheta_bound

theorem integral_etheta_bound {x : ℝ} (hx2 : 2 ≤ x) (hxe : x ≤ exp 10) :    ∫ t in (2:ℝ)..x, Eθ t / log t ^ 2 ≤ (4/5) / (log 2) ^ 2 * (x - 2) := by  have hlog2 : (0:ℝ) < log 2 := log_pos (by norm_num)  calc ∫ t in (2:ℝ)..x, Eθ t / log t ^ 2      ≤ ∫ _t in (2:ℝ)..x, (4/5) / (log 2) ^ 2 := by        apply intervalIntegral.integral_mono_on hx2 (etheta_integrand_intble hx2)          intervalIntegrable_const        intro t ⟨ht2, htx⟩        have hEθt : Eθ t ≤ 4/5 := etheta_le_floor t ⟨ht2, le_trans htx hxe⟩        have hEθnn : 0 ≤ Eθ t := by unfold Eθ; positivity        have hlogt : log 2 ≤ log t := log_le_log (by norm_num) ht2        have hlogt_pos : (0:ℝ) < log t := lt_of_lt_of_le hlog2 hlogt        have hsq : (log 2)^2 ≤ (log t)^2 := by nlinarith [hlogt, hlog2.le]        calc Eθ t / log t ^ 2 ≤ (4/5) / log t ^ 2 := by gcongr          _ ≤ (4/5) / (log 2) ^ 2 := by gcongr    _ = (4/5) / (log 2) ^ 2 * (x - 2) := by        rw [intervalIntegral.integral_const]; ring