Ramanujan.log_2_IBP_t

lemma log_2_IBP_t (x : ℝ) (hx : 2 ≤ x) :    ∫ t in Set.Icc 2 x, 1 / log t ^ 2 =      x / log x ^ 2 - 2 / log 2 ^ 2 +        2 * ∫ t in Set.Icc 2 x, 1 / log t ^ 3 := by  suffices h_ibp : ∀ a b : ℝ, 2 ≤ a → a ≤ b →      ∫ t in a..b, (1 / (log t) ^ 2) = (b / (log b) ^ 2) - (a / (log a) ^ 2) +        2 * ∫ t in a..b, (1 / (log t) ^ 3) by    simpa only [MeasureTheory.integral_Icc_eq_integral_Ioc,      intervalIntegral.integral_of_le hx] using h_ibp 2 x (by norm_num) hx  intro a b ha hab  have h_deriv : ∀ t ∈ Set.Icc a b,      deriv (fun t ↦ t / (log t) ^ 2) t =        1 / (log t) ^ 2 - 2 * (1 / (log t) ^ 3) := by    intro t ht    norm_num [differentiableAt_log, ne_of_gt (show 0 < log t from log_pos <| by linarith [ht.1]),      ne_of_gt (show 0 < t from by linarith [ht.1])]    ring_nf    grind  have h_ftc : ∫ t in a..b, deriv (fun t ↦ t / (log t) ^ 2) t =      (b / (log b) ^ 2) - (a / (log a) ^ 2) := by    rw [intervalIntegral.integral_deriv_eq_sub']    · rfl    · exact fun x hx ↦ DifferentiableAt.div differentiableAt_id        (DifferentiableAt.pow (differentiableAt_log          (by cases Set.mem_uIcc.mp hx <;> linarith)) _)        (pow_ne_zero _ <| ne_of_gt <| log_pos <|          by cases Set.mem_uIcc.mp hx <;> linarith)    · rw [Set.uIcc_of_le hab]      have hlog_cont := continuousOn_log.mono fun y (hy : y ∈ Set.Icc a b) ↦        ne_of_gt <| by linarith [hy.1]      have hpow_ne : ∀ (n : ℕ), ∀ y ∈ Set.Icc a b, log y ^ n ≠ 0 :=        fun n y hy ↦ pow_ne_zero n <| ne_of_gt <| log_pos <| by linarith [hy.1]      exact ContinuousOn.congr (ContinuousOn.sub        (continuousOn_const.div (hlog_cont.pow _) (hpow_ne _))        (continuousOn_const.mul <| continuousOn_const.div (hlog_cont.pow _) (hpow_ne _))) h_deriv  rw [← h_ftc, intervalIntegral.integral_congr fun t ht =>    h_deriv t <| by simpa [hab] using ht]  rw [intervalIntegral.integral_sub]  · norm_num  · exact ContinuousOn.intervalIntegrable (continuousOn_of_forall_continuousAt fun x hx ↦      ContinuousAt.div continuousAt_const        (ContinuousAt.pow (continuousAt_log          (by linarith [Set.mem_Icc.mp (by simpa [hab] using hx)])) _)        (ne_of_gt (pow_pos (log_pos (by linarith [Set.mem_Icc.mp (by simpa [hab] using hx)])) _)))  · exact ContinuousOn.intervalIntegrable ((continuousOn_const.mul      (continuousOn_of_forall_continuousAt fun x hx ↦        ContinuousAt.div continuousAt_const          (ContinuousAt.pow (continuousAt_log            (by linarith [Set.mem_Icc.mp (by simpa [hab] using hx)])) _)          (ne_of_gt (pow_pos (log_pos (by linarith [Set.mem_Icc.mp (by simpa [hab] using hx)])) _)))))