integral_log_inv

lemma integral_log_inv (a b : ℝ) (ha : 2 ≤ a) (hb : a ≤ b) :    ∫ t in a..b, (log t)⁻¹ =    ((log b)⁻¹ * b) - ((log a)⁻¹ * a) +      ∫ t in a..b, ((log t)^2)⁻¹ := by  rw [le_iff_lt_or_eq] at hb  rcases hb with hb | rfl; swap  · simp only [intervalIntegral.integral_same, sub_self, add_zero]  · have := intervalIntegral.integral_mul_deriv_eq_deriv_mul      (u := fun x => (log x)⁻¹)      (u' := fun x => -1 / (x * (log x)^2))      (v := fun x => x)      (v' := fun _ => 1) (a := a) (b := b)      (fun x hx => by        rw [Set.uIcc_eq_union, Set.Icc_eq_empty (lt_iff_not_ge |>.1 hb), Set.union_empty] at hx        obtain ⟨hx1, _⟩ := hx        rw [show (-1 / (x * log x ^ 2)) = (-1 / log x ^ 2) * (x⁻¹) by          rw [mul_comm x]; field_simp]        apply HasDerivAt.comp          (h := fun t => log t) (h₂ := fun t => t⁻¹) (x := x)        · simpa using! HasDerivAt.inv (c := fun t : ℝ => t) (c' := 1) (x := log x)            (hasDerivAt_id' (log x))            (by simp only [ne_eq, log_eq_zero, not_or]; refine ⟨?_, ?_, ?_⟩ <;> linarith)        · apply hasDerivAt_log; linarith)      (fun x _ => hasDerivAt_id' x)      (by        rw [intervalIntegrable_iff_integrableOn_Icc_of_le (le_of_lt hb)]        apply ContinuousOn.integrableOn_Icc        refine continuousOn_log0.mono fun x hx ↦ ?_        simp only [Set.mem_Icc, Set.mem_compl_iff, Set.mem_insert_iff, Set.mem_singleton_iff,          not_or] at hx ⊢        refine ⟨?_, ?_, ?_⟩ <;> linarith)      (by        constructor <;>        apply MeasureTheory.integrable_const)    simp only [mul_one] at this    rw [this]    simp_rw [neg_div, neg_mul]    rw [sub_eq_add_neg]    congr 1    rw [intervalIntegral.integral_of_le (le_of_lt hb),      intervalIntegral.integral_of_le (le_of_lt hb),      ← MeasureTheory.integral_neg]    simp_rw [neg_neg]    refine integral_congr_ae ?_    · rw [ae_restrict_eq, eventuallyEq_inf_principal_iff]      · refine .of_forall fun x hx => ?_        simp only [Set.mem_Ioc, one_div, mul_inv_rev, mul_assoc] at hx ⊢        rw [inv_mul_cancel₀, mul_one]        linarith      exact measurableSet_Ioc