Ramanujan.log_7_IBP

theorem log_7_IBP (x : ℝ) (hx : 2 ≤ x) :    ∫ t in Set.Icc 2 x, 1 / log t ^ 7 =      x / log x ^ 7 - 2 / log 2 ^ 7 +        7 * ∫ t in Set.Icc 2 x, 1 / log t ^ 8 := by  suffices h_ibp : ∀ a b : ℝ, 2 ≤ a → a ≤ b →      ∫ t in a..b, (1 / (log t) ^ 7) = (b / (log b) ^ 7) - (a / (log a) ^ 7) +        7 * ∫ t in a..b, (1 / (log t) ^ 8) 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) ^ 7) t =        1 / (log t) ^ 7 - 7 * (1 / (log t) ^ 8) := 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) ^ 7) t =      (b / (log b) ^ 7) - (a / (log a) ^ 7) := 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  · ring_nf    exact ContinuousOn.intervalIntegrable (      continuousOn_of_forall_continuousAt fun x hx =>        ContinuousAt.pow (ContinuousAt.inv₀          (continuousAt_log (by linarith [Set.mem_Icc.mp (by simpa [hab] using hx)]))          (ne_of_gt (log_pos (by linarith [Set.mem_Icc.mp (by simpa [hab] using hx)])))) _) ..  · apply_rules [ContinuousOn.intervalIntegrable]    exact ContinuousOn.mul continuousOn_const <|      ContinuousOn.inv₀ (ContinuousOn.pow        (continuousOn_log.mono <| by          intro x hx; cases Set.mem_uIcc.mp hx <;> norm_num <;> linarith) _)        fun x hx ↦ ne_of_gt <| pow_pos (log_pos <| by          cases Set.mem_uIcc.mp hx <;> linarith) _