FKS2.integral_one_div_log_sq_le_of_ge

lemma integral_one_div_log_sq_le_of_ge {x₁ : ℝ} (hx₁ : 14 ≤ x₁) {y : ℝ} (hy : x₁ ≤ y) :    ∫ s in x₁..y, 1 / (Real.log s) ^ 2 ≤ (Real.log x₁ / (Real.log x₁ - 2)) * (y / (Real.log y) ^ 2) := by  have hx₁_gt : 1 < x₁ := by linarith  have hlogx₁ : 0 < Real.log x₁ := Real.log_pos hx₁_gt  have hlogx₁_gt : 2 < Real.log x₁ := log_gt_two_of_ge_14 hx₁  have hc : 0 < 1 - 2 / Real.log x₁ := by    have : 2 / Real.log x₁ < 1 := (div_lt_iff₀ hlogx₁).mpr (by linarith)    linarith  have hs_gt_of_mem : ∀ s ∈ Set.uIcc x₁ y, 1 < s := fun s hs => by    cases Set.mem_uIcc.mp hs <;> linarith  have h_intble1 : IntervalIntegrable (fun s ↦ (1 - 2 / Real.log x₁) * (1 / (Real.log s) ^ 2)) volume x₁ y :=    ContinuousOn.intervalIntegrable <| continuousOn_of_forall_continuousAt fun s hs ↦ by      have hne : Real.log s ≠ 0 := ne_of_gt (Real.log_pos (hs_gt_of_mem s hs))      exact ContinuousAt.mul continuousAt_const        (ContinuousAt.div continuousAt_const          (ContinuousAt.pow (Real.continuousAt_log (by linarith [hs_gt_of_mem s hs])) 2)          (pow_ne_zero 2 hne))  have h_intble2 : IntervalIntegrable (fun s ↦ 1 / (Real.log s) ^ 2 - 2 / (Real.log s) ^ 3) volume x₁ y :=    ContinuousOn.intervalIntegrable <| continuousOn_of_forall_continuousAt fun s hs ↦ by      have hne : Real.log s ≠ 0 := ne_of_gt (Real.log_pos (hs_gt_of_mem s hs))      have hs0 : s ≠ 0 := by linarith [hs_gt_of_mem s hs]      exact (ContinuousAt.div continuousAt_const          (ContinuousAt.pow (Real.continuousAt_log hs0) 2) (pow_ne_zero 2 hne)).sub        (ContinuousAt.div continuousAt_const          (ContinuousAt.pow (Real.continuousAt_log hs0) 3) (pow_ne_zero 3 hne))  have h_mono : ∫ s in x₁..y, (1 - 2 / Real.log x₁) * (1 / (Real.log s) ^ 2) ≤      ∫ s in x₁..y, (1 / (Real.log s) ^ 2 - 2 / (Real.log s) ^ 3) := by    apply intervalIntegral.integral_mono_on hy h_intble1 h_intble2    intro s hs    have hs_gt : 1 < s := hx₁_gt.trans_le hs.1    have hlogs : 0 < Real.log s := Real.log_pos hs_gt    have hlog_le : Real.log x₁ ≤ Real.log s := Real.log_le_log (by linarith) hs.1    have h_frac : 2 / Real.log s ≤ 2 / Real.log x₁ :=      div_le_div_of_nonneg_left (by norm_num) hlogx₁ hlog_le    rw [show (1 - 2 / Real.log x₁) * (1 / (Real.log s) ^ 2) = (1 - 2 / Real.log x₁) / (Real.log s) ^ 2 by ring,        show 1 / (Real.log s) ^ 2 - 2 / (Real.log s) ^ 3 = (1 - 2 / Real.log s) / (Real.log s) ^ 2 by field_simp]    exact div_le_div_of_nonneg_right (by linarith) (by positivity)  have h_int_eq : ∫ s in x₁..y, (1 / (Real.log s) ^ 2 - 2 / (Real.log s) ^ 3) =      y / (Real.log y) ^ 2 - x₁ / (Real.log x₁) ^ 2 :=    intervalIntegral.integral_eq_sub_of_hasDerivAt      (fun s hs => hasDerivAt_id_div_log_sq (hx₁_gt.trans_le (Set.uIcc_of_le hy ▸ hs).1))      h_intble2  rw [intervalIntegral.integral_const_mul] at h_mono  have h_bound : (1 - 2 / Real.log x₁) * ∫ s in x₁..y, 1 / (Real.log s) ^ 2 ≤ y / (Real.log y) ^ 2 :=    calc (1 - 2 / Real.log x₁) * ∫ s in x₁..y, 1 / (Real.log s) ^ 2        ≤ ∫ s in x₁..y, (1 / (Real.log s) ^ 2 - 2 / (Real.log s) ^ 3) := h_mono      _ = y / (Real.log y) ^ 2 - x₁ / (Real.log x₁) ^ 2 := h_int_eq      _ ≤ y / (Real.log y) ^ 2 := by linarith [div_nonneg (by linarith : 0 ≤ x₁) (by positivity : (0 : ℝ) ≤ (Real.log x₁) ^ 2)]  have h_bound' : ∫ s in x₁..y, 1 / (Real.log s) ^ 2 ≤ (y / (Real.log y) ^ 2) / (1 - 2 / Real.log x₁) := by    rwa [le_div_iff₀ hc, mul_comm]  convert h_bound' using 1  field_simp