Exponential integrals on the real line

This file records integrability and evaluation of exponential integrands on a half-line or the whole real line: natural powers multiplied by an exponentially decaying factor, the exact rate at which a bare exponential is integrable on a right half-line, and integrability of the two-sided exponential.

Mathlib supplies the sufficient direction of the right-half-line integrability criterion, integrableOn_exp_mul_Ioi, for a negative rate. integrableOn_exp_mul_Ioi_iff adds the converse, which is what lets a caller describe an exponential-moment domain as an exact set rather than an inclusion.

Main results

• TauCeti.integrableOn_pow_mul_exp_neg_mul_Ioi: integrability on (0, ∞).
• TauCeti.integral_pow_mul_exp_neg_mul_Ioi: evaluation in terms of a factorial.
• TauCeti.lintegral_ofReal_exp_neg_mul_mul_lintegral: an iterated exponential integral is a Stieltjes-kernel integral.
• TauCeti.integrableOn_exp_mul_Ioi_iff: exp (a * ·) is integrable on (c, ∞) exactly when a < 0.
• TauCeti.integrableOn_exp_mul_Iic_iff: exp (a * ·) is integrable on (-∞, c] exactly when 0 < a.
• TauCeti.integrable_exp_neg_mul_abs: exp (-(a * |·|)) is integrable when 0 < a.

theorem TauCeti.integrableOn_pow_mul_exp_neg_mul_Ioi (n : ℕ) {b : ℝ} (hb : 0 < b) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ n * Real.exp (-(b * t))) (Set.Ioi 0) MeasureTheory.volume

Natural powers times an exponentially decaying factor are integrable on (0, ∞).

theorem TauCeti.integral_pow_mul_exp_neg_mul_Ioi (n : ℕ) {a : ℝ} (ha : 0 < a) : ∫ (t : ℝ) in Set.Ioi 0, t ^ n * Real.exp (-(a * t)) = ↑n.factorial / a ^ (n + 1)

The integral of a natural power times an exponentially decaying factor on (0, ∞).

theorem TauCeti.lintegral_ofReal_exp_neg_mul_mul_lintegral (ν : MeasureTheory.Measure NNReal) [MeasureTheory.SFinite ν] {t : ℝ} (ht : 0 < t) : ∫⁻ (s : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-(t * s))) * ∫⁻ (x : NNReal), ENNReal.ofReal (Real.exp (-(s * ↑x))) ∂ν = ∫⁻ (x : NNReal), ENNReal.ofReal (t + ↑x)⁻¹ ∂ν

The Stieltjes kernel is an iterated exponential integral. Swapping the two integrations turns the outer Laplace integral of the inner one into the Stieltjes integral of ν.

theorem TauCeti.integrable_exp_neg_mul_abs {a : ℝ} (ha : 0 < a) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-(a * |x|))) MeasureTheory.volume

The two-sided exponential is integrable on the line.

@[simp]

theorem TauCeti.integrableOn_exp_mul_Ioi_iff {a c : ℝ} : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (a * x)) (Set.Ioi c) MeasureTheory.volume ↔ a < 0

The exact integrability rate. fun x => exp (a * x) is integrable on (c, ∞) precisely when the rate is negative. Mathlib's integrableOn_exp_mul_Ioi is the ← direction.

@[simp]

theorem TauCeti.integrableOn_exp_mul_Iic_iff {a c : ℝ} : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (a * x)) (Set.Iic c) MeasureTheory.volume ↔ 0 < a

The exact integrability rate on a left half-line. fun x => exp (a * x) is integrable on (-∞, c] precisely when the rate is positive.