Source indexedtheorem · leanprover/lean4:v4.32.0

LiSeries.fubini_log_exp_neg

PrimeNumberTheoremAnd.IEANTN.LiSeries · PrimeNumberTheoremAnd/IEANTN/LiSeries.lean:378 to 386

Mathematical statement

Exact Lean statement

theorem fubini_log_exp_neg :
    ∫ t in Ioi (0 : ℝ), log t * exp (-t) =
      (∫ t in (0 : ℝ)..1, (exp (-t) - 1) / t) + ∫ t in Ioi (1 : ℝ), exp (-t) / t

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem fubini_log_exp_neg :    ∫ t in Ioi (0 : ℝ), log t * exp (-t) =      (∫ t in (0 : ℝ)..1, (exp (-t) - 1) / t) + ∫ t in Ioi (1 : ℝ), exp (-t) / t := by  -- Split ∫_{Ioi 0} = ∫_{Ioc 0 1} + ∫_{Ioi 1}  have hsplit : Set.Ioi (0 : ℝ) = Set.Ioc 0 1 ∪ Set.Ioi 1 :=    (Set.Ioc_union_Ioi_eq_Ioi zero_le_one).symm  rw [hsplit, setIntegral_union Set.Ioc_disjoint_Ioi_same measurableSet_Ioi      integrableOn_log_mul_exp_neg_Ioc integrableOn_log_mul_exp_neg_Ioi_one]  rw [ibp_Ioc_zero_one, ibp_Ioi_one]