integral_log_inv_pos

lemma integral_log_inv_pos (x : ℝ) (hx : 2 < x) :    0 < ∫ t in Set.Icc 2 x, (log t)⁻¹ := by  classical  rw [MeasureTheory.integral_pos_iff_support_of_nonneg_ae]  · simp only [Function.support_inv, measurableSet_Icc, Measure.restrict_apply']    rw [show Function.support log ∩ Set.Icc 2 x = Set.Icc 2 x by      rw [Set.inter_eq_right]      intro t ht      simp only [Set.mem_Icc, Function.mem_support, ne_eq, log_eq_zero, not_or] at ht ⊢      exact ⟨by linarith, by linarith, by linarith⟩]    simpa  · simp only [measurableSet_Icc, ae_restrict_eq, EventuallyLE, eventually_inf_principal]    refine .of_forall fun t (ht : _ ∧ _) => ?_    simpa only [Pi.zero_apply, inv_nonneg] using log_nonneg (by linarith)  · apply ContinuousOn.integrableOn_Icc    apply ContinuousOn.inv₀    · exact (continuousOn_log).mono <| by aesop     · rintro t ⟨ht, -⟩      simp only [ne_eq, log_eq_zero, not_or]      exact ⟨by linarith, by linarith, by linarith⟩