LiSeries.FubiniLogExpNeg.integrableOn_exp_neg_div_Ioi_one

lemma integrableOn_exp_neg_div_Ioi_one :    IntegrableOn (fun t => exp (-t) / t) (Set.Ioi 1) := by  have hg : IntegrableOn (fun t => exp (-t)) (Set.Ioi 1) := by    have := (GammaIntegral_convergent (s := 1) (by norm_num : (0 : ℝ) < 1)).mono_set      (Set.Ioi_subset_Ioi zero_le_one)    apply this.congr    filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with t ht    simp only [Set.mem_Ioi] at ht    rw [show (1 : ℝ) - 1 = 0 from by norm_num, rpow_zero, mul_one]  rw [IntegrableOn] at hg ⊢  exact hg.mono    ((continuous_exp.comp continuous_neg).measurable.div measurable_id).aestronglyMeasurable.restrict    (by filter_upwards [self_mem_ae_restrict measurableSet_Ioi] with t ht        simp only [Set.mem_Ioi] at ht        have ht0 : (0 : ℝ) < t := lt_trans zero_lt_one ht        rw [norm_div, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (exp_pos _), abs_of_pos ht0]        exact div_le_self (le_of_lt (exp_pos _)) (le_of_lt ht))