FKS2.Floor.corollary_22_floor

theorem corollary_22_floor :    ∀ x ∈ Set.Icc (2:ℝ) (exp 10), Eπ x ≤ admissible_bound 9.2211 (3 / 2) 0.8476 1 x := by  intro x hx  obtain ⟨hx2, hxe⟩ := hx  have hxpos : (0:ℝ) < x := by linarith  have hlogx_pos : (0:ℝ) < log x := log_pos (by linarith)  have hℓ : (0:ℝ) < log 2 := log_pos (by norm_num)  have hℓ2 : (0:ℝ) < (log 2) ^ 2 := by positivity  have hℓ_gt : 0.6931471803 < log 2 := Real.log_two_gt_d9  have hlogxx_nn : (0:ℝ) ≤ log x / x := div_nonneg hlogx_pos.le hxpos.le  have h30 := eq_30 (x₀ := 2) hx2 (by norm_num)  rw [delta_two] at h30  have hEθ : Eθ x ≤ 4/5 := etheta_le_floor x ⟨hx2, hxe⟩  have hint : ∫ t in (2:ℝ)..x, Eθ t / log t ^ 2 ≤ (4/5) / (log 2) ^ 2 * (x - 2) :=    integral_etheta_bound hx2 hxe  -- bracket algebra: the two correction terms ≤ (5/3) log x  have hb1 : 2 / log 2 ≤ 2887/1000 := by rw [div_le_iff₀ hℓ]; nlinarith [hℓ_gt]  have hb2 : (4/5) / (log 2) ^ 2 ≤ 1666/1000 := by rw [div_le_iff₀ hℓ2]; nlinarith [hℓ_gt, hℓ]  have hbracket :      (log x / x) * (2 / log 2) * 1 + (log x / x) * ((4/5) / (log 2) ^ 2 * (x - 2))        ≤ (5/3) * log x := by    have hred : 2 / log 2 + (4/5) / (log 2) ^ 2 * (x - 2) ≤ (5/3) * x := by      have hxm2 : (0:ℝ) ≤ x - 2 := by linarith      have hstep : 2 / log 2 + (4/5) / (log 2) ^ 2 * (x - 2)          ≤ 2887/1000 + 1666/1000 * (x - 2) := by gcongr      nlinarith [hstep, hx2]    have h := mul_le_mul_of_nonneg_left hred hlogxx_nn    rw [show (log x / x) * ((5/3) * x) = (5/3) * log x by field_simp] at h    rw [show (log x / x) * (2 / log 2 + (4/5) / (log 2) ^ 2 * (x - 2))        = (log x / x) * (2 / log 2) * 1 + (log x / x) * ((4/5) / (log 2) ^ 2 * (x - 2)) by      ring] at h    exact h  calc Eπ x      ≤ Eθ x + log x / x * (2 / log 2) * 1          + log x / x * ∫ t in (2:ℝ)..x, Eθ t / log t ^ 2 := h30    _ ≤ 4/5 + log x / x * (2 / log 2) * 1          + log x / x * ((4/5) / (log 2) ^ 2 * (x - 2)) := by gcongr    _ ≤ 4/5 + (5/3) * log x := by linarith [hbracket]    _ ≤ admissible_bound 9.2211 (3 / 2) 0.8476 1 x := linear_le_curve hx2 hxe