LiSeries.FubiniLogExpNeg.ibp_Ioc_zero_one

lemma ibp_Ioc_zero_one :    ∫ t in Set.Ioc (0 : ℝ) 1, log t * exp (-t) =      ∫ t in (0 : ℝ)..1, (exp (-t) - 1) / t := by  rw [← intervalIntegral.integral_of_le zero_le_one]  have hf_int : IntervalIntegrable (fun t => log t * exp (-t)) volume 0 1 :=    (intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one).mpr      integrableOn_log_mul_exp_neg_Ioc  have hg_int := intervalIntegrable_expm1_div  set F : ℝ → ℝ := fun ε => (∫ t in ε..(1 : ℝ), log t * exp (-t)) -      (∫ t in ε..(1 : ℝ), (exp (-t) - 1) / t)  suffices F 0 = 0 by simp [F] at this; linarith  have hf_intOn : IntegrableOn (fun t => log t * exp (-t)) (Set.uIcc 0 1) :=    (intervalIntegrable_iff').1 hf_int  have hg_intOn : IntegrableOn (fun t => (exp (-t) - 1) / t) (Set.uIcc 0 1) :=    (intervalIntegrable_iff').1 hg_int  have hF_cts : ContinuousOn F (Set.uIcc 0 1) :=    (intervalIntegral.continuousOn_primitive_interval_left hf_intOn).sub      (intervalIntegral.continuousOn_primitive_interval_left hg_intOn)  have hF_tends_F0 : Tendsto F (𝓝[Set.Ioi 0] 0) (𝓝 (F 0)) :=    (hF_cts.continuousWithinAt left_mem_uIcc).mono_left nhdsWithin_Ioi_le_nhdsWithin_uIcc  have h_bdy : Tendsto (fun ε => (exp (-ε) - 1) * log ε) (𝓝[>] (0 : ℝ)) (𝓝 0) := by    have h_mul_log : Tendsto (fun x : ℝ => log x * x) (𝓝[>] 0) (𝓝 0) := by      simpa [rpow_one] using tendsto_log_mul_rpow_nhdsGT_zero zero_lt_one    exact squeeze_zero_norm'      (eventually_nhdsWithin_of_forall fun ε (hε : 0 < ε) => by        simp only [Real.norm_eq_abs, abs_mul]        calc |exp (-ε) - 1| * |log ε| = |log ε| * |exp (-ε) - 1| := mul_comm _ _          _ ≤ |log ε| * |ε| := by              apply mul_le_mul_of_nonneg_left _ (abs_nonneg _)              rw [abs_le, abs_of_pos hε]              exact ⟨by linarith [one_sub_le_exp_neg ε],                     by linarith [exp_le_one_iff.mpr (neg_nonpos.mpr hε.le)]⟩)      (by simpa [norm_zero] using h_mul_log.norm)  have hF_tends_0 : Tendsto F (𝓝[Set.Ioi 0] 0) (𝓝 0) := by    apply Tendsto.congr' _ h_bdy    rw [eventuallyEq_nhdsWithin_iff]    filter_upwards [Iio_mem_nhds (show (0 : ℝ) < 1 from by norm_num)] with ε hε hε0    simp only [F]    linarith [ibp_eps hε0 hε]  exact tendsto_nhds_unique hF_tends_F0 hF_tends_0