Exponential integrals on the real line and radial exponentials

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 and the integral of the two-sided exponential; and, on a finite-dimensional real normed space, integrability of the radial exponential exp (-a ‖x‖) for every additive Haar measure, by integrating in polar coordinates.

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.
• TauCeti.integral_exp_neg_mul_abs: its integral is 2 / a.
• TauCeti.lintegral_ofReal_mul_exp_neg_mul_abs: the same evaluation as a lower Lebesgue integral of c * exp (-(a * |·|)).
• TauCeti.integrable_exp_mul_I_mul_exp_neg_mul_abs: the same times the oscillation exp (b * x * I).
• TauCeti.integrable_exp_neg_mul_norm: exp (-(a * ‖·‖)) is integrable on a finite-dimensional space 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_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {a : ℝ} (ha : 0 < a) : MeasureTheory.Integrable (fun (x : E) => Real.exp (-(a * ‖x‖))) μ

The radial exponential exp (-(a * ‖x‖)) is integrable for every additive Haar measure on a finite-dimensional real normed space, when 0 < a.

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.

theorem TauCeti.integral_exp_neg_mul_abs {a : ℝ} (ha : 0 < a) : ∫ (x : ℝ), Real.exp (-(a * |x|)) = 2 / a

The two-sided exponential exp (-(a * |x|)) has integral 2 / a when 0 < a.

theorem TauCeti.lintegral_ofReal_mul_exp_neg_mul_abs {a : ℝ} (ha : 0 < a) (c : ℝ) : ∫⁻ (x : ℝ), ENNReal.ofReal (c * Real.exp (-(a * |x|))) = ENNReal.ofReal (2 * c / a)

The lower Lebesgue integral of a constant multiple of the two-sided exponential: ∫⁻ x, ofReal (c * exp (-(a * |x|))) = ofReal (2 * c / a) when 0 < a. For c ≤ 0 both sides vanish.

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

The two-sided exponential times a unimodular oscillation exp (b * x * I) 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.