← Mathematical handbook

noncomputable def Verification.exponentialIntegralE1 (a : ℝ) : ℝ

The classical real exponential integral in the source's convention.

Equations

• Verification.exponentialIntegralE1 a = ∫ (s : ℝ) in Set.Ioi 1, Real.exp (-a * s) / s

theorem Verification.integral_unit_neg_exp (f : ℝ → ℝ) : ∫ (u : ↑unitInterval), f ↑u = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-t) * f (Real.exp (-t))

theorem Verification.integral_exp_three : ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-3 * t) = 1 / 3

theorem Verification.integral_t_exp_three : ∫ (t : ℝ) in Set.Ioi 0, t * Real.exp (-3 * t) = 1 / 9

theorem Verification.integrable_exp_three : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-3 * t)) (Set.Ioi 0) MeasureTheory.volume

theorem Verification.integrable_t_exp_three : MeasureTheory.IntegrableOn (fun (t : ℝ) => t * Real.exp (-3 * t)) (Set.Ioi 0) MeasureTheory.volume

theorem Verification.integrable_exp_three_div {θ : ℝ} (hθ : 0 ≤ θ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-3 * t) / (1 + 2 * θ * t)) (Set.Ioi 0) MeasureTheory.volume

theorem Verification.integral_exp_three_div {θ : ℝ} (hθ : 0 < θ) : ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-3 * t) / (1 + 2 * θ * t) = Real.exp (3 / (2 * θ)) / (2 * θ) * exponentialIntegralE1 (3 / (2 * θ))

theorem Verification.integral_gb_exponential (θ : ℝ) (hθ : 0 < θ) : ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-3 * t) * (1 + θ * t) ^ 2 / (1 + 2 * θ * t) = θ / 18 + 1 / 4 + Real.exp (3 / (2 * θ)) / (8 * θ) * exponentialIntegralE1 (3 / (2 * θ))