LiSeries.FubiniLogExpNeg.integrableOn_log_mul_exp_neg_Ioi_one

lemma integrableOn_log_mul_exp_neg_Ioi_one :    IntegrableOn (fun t => log t * exp (-t)) (Set.Ioi 1) := by  have hg : IntegrableOn (fun t => t * exp (-t)) (Set.Ioi 1) := by    have := (GammaIntegral_convergent (s := 2) (by norm_num : (0 : ℝ) < 2)).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 (2 : ℝ) - 1 = 1 from by norm_num, rpow_one t, mul_comm]  rw [IntegrableOn] at hg ⊢  exact hg.mono    ((measurable_log.mul        (continuous_exp.comp continuous_neg).measurable).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_mul, norm_mul, Real.norm_eq_abs (log t), Real.norm_eq_abs t,            abs_of_nonneg (log_nonneg ht.le), abs_of_pos ht0]        exact mul_le_mul_of_nonneg_right (log_le_self ht0.le) (norm_nonneg _))