Elementary theory of the exponential distribution

This file completes the elementary moment, transform, and tail API for Mathlib's exponential measure, parametrized by its rate. For a positive rate r, it evaluates all moments, identifies the exact exponential-moment domain, computes the moment- and cumulant-generating functions and the characteristic function, and deduces the mean and variance. It also establishes the memoryless property and computes the law of the minimum of independent exponentials.

Moments come from one formula. integral_pow_expMeasure computes every moment, ∫ x ^ n ∂(expMeasure r) = n ! / r ^ n, and the mean and second moment are its n = 1 and n = 2 specializations.

The exponential law is the shape-one Gamma law. Mathlib defines expMeasure r as gammaMeasure 1 r, so the moments, the exponential-integrability domain, and the transforms are the a = 1 cases of the Gamma results in TauCeti.Probability.Distributions.Gamma.Basic and TauCeti.Probability.Distributions.Gamma.CharFun, rewritten into their exponential closed forms.

Main results

• integrable_expMeasure_iff, integral_expMeasure_eq — integrability and integration against the exponential law, transferred to the real density;
• integrable_pow_expMeasure — every moment is integrable, for 0 < r;
• integral_pow_expMeasure — the n-th moment, n ! / r ^ n, for 0 < r;
• integral_id_expMeasure, integral_sq_expMeasure — the mean and the second moment;
• variance_id_expMeasure — the variance (r ^ 2)⁻¹;
• integrable_exp_mul_expMeasure_iff — exact exponential integrability threshold t < r;
• integrableExpSet_id_expMeasure — exact domain (-∞, r);
• mgf_id_expMeasure — moment-generating function r / (r - t);
• cgf_id_expMeasure — cumulant-generating function log (r / (r - t));
• charFun_expMeasure — characteristic function (r : ℂ) / (r - I * t);
• measureReal_Ioi_expMeasure, measure_Ioi_expMeasure — tail probabilities;
• memoryless_expMeasure — the conditional tail is unchanged by elapsed time;
• map_min_expMeasure — the minimum map sends a product of exponential laws to the exponential law whose rate is the sum of the rates;
• hasLaw_min_expMeasure_of_indepFun — minimum of independent exponentials;
• hasLaw_min_iid_expMeasure — minimum of d i.i.d. exponentials of rate r is exponential of rate d * r.
• nnrealExpMeasure — the exponential measure transported to ℝ≥0.

References

• mathlib4#35504 by Joakim Björnander (Apache 2.0): the names and theorem shapes of the mgf, moment and memorylessness results below, and the proof of memorylessness, are adapted from it.

theorem TauCeti.Probability.expMeasure_eq_withDensity (r : ℝ) : ProbabilityTheory.expMeasure r = MeasureTheory.volume.withDensity (ProbabilityTheory.exponentialPDF r)

expMeasure r is the Lebesgue measure weighted by its exponential density.

theorem TauCeti.Probability.ae_pos_expMeasure (r : ℝ) : ∀ᵐ (x : ℝ) ∂ProbabilityTheory.expMeasure r, 0 < x

The measure expMeasure r is concentrated on the positive reals, for every r. For 0 < r this says an exponential random variable is almost surely positive; for r ≤ 0 the measure is zero and the statement holds trivially.

theorem TauCeti.Probability.integrable_expMeasure_iff {r : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (hr : 0 < r) {g : ℝ → E} : MeasureTheory.Integrable g (ProbabilityTheory.expMeasure r) ↔ MeasureTheory.Integrable (fun (x : ℝ) => ProbabilityTheory.exponentialPDFReal r x • g x) MeasureTheory.volume

Integrability transfer. A function is integrable against an exponential law with positive rate exactly when its density-weighted version is Lebesgue integrable.

theorem TauCeti.Probability.integral_expMeasure_eq {r : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (hr : 0 < r) (g : ℝ → E) : ∫ (x : ℝ), g x ∂ProbabilityTheory.expMeasure r = ∫ (x : ℝ), ProbabilityTheory.exponentialPDFReal r x • g x

Integral transfer. An integral against an exponential law with positive rate is the density-weighted Lebesgue integral.

@[simp]

theorem TauCeti.Probability.integrable_pow_expMeasure {r : ℝ} (hr : 0 < r) (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ n) (ProbabilityTheory.expMeasure r)

Every moment of the exponential law is integrable. This is not implied by the moment formula below: Lean's integral is defined for non-integrable functions too, so an integral equality alone says nothing about finiteness.

@[simp]

theorem TauCeti.Probability.integral_pow_expMeasure {r : ℝ} (hr : 0 < r) (n : ℕ) : ∫ (x : ℝ), x ^ n ∂ProbabilityTheory.expMeasure r = ↑n.factorial / r ^ n

The moments of the exponential law. ∫ x ^ n ∂(expMeasure r) = n ! / r ^ n, for every n.

No nondegeneracy hypothesis on n is needed: at n = 0 both sides are 1. The mean and the second moment below are the n = 1 and n = 2 cases.

@[simp]

theorem TauCeti.Probability.integral_id_expMeasure {r : ℝ} (hr : 0 < r) : ∫ (x : ℝ), x ∂ProbabilityTheory.expMeasure r = r⁻¹

The mean of the exponential law with rate r is r⁻¹.

theorem TauCeti.Probability.integral_sq_expMeasure {r : ℝ} (hr : 0 < r) : ∫ (x : ℝ), x ^ 2 ∂ProbabilityTheory.expMeasure r = 2 / r ^ 2

The second moment of the exponential law with rate r is 2 / r ^ 2.

@[simp]

theorem TauCeti.Probability.variance_id_expMeasure {r : ℝ} (hr : 0 < r) : ProbabilityTheory.variance id (ProbabilityTheory.expMeasure r) = (r ^ 2)⁻¹

The variance of the exponential law with rate r is (r ^ 2)⁻¹.

@[simp]

theorem TauCeti.Probability.integrable_exp_mul_expMeasure_iff {r t : ℝ} (hr : 0 < r) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (ProbabilityTheory.expMeasure r) ↔ t < r

The exact exponential-integrability threshold. The integrand exp (t * x) is integrable against an exponential law with positive rate r exactly when t < r.

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_expMeasure {r : ℝ} (hr : 0 < r) : ProbabilityTheory.integrableExpSet id (ProbabilityTheory.expMeasure r) = Set.Iio r

The exact exponential-integrability domain of an exponential law with positive rate is (-∞, r).

@[simp]

theorem TauCeti.Probability.mgf_id_expMeasure {r t : ℝ} (hr : 0 < r) (ht : t < r) : ProbabilityTheory.mgf id (ProbabilityTheory.expMeasure r) t = r / (r - t)

The moment-generating function of an exponential law with positive rate, on its finiteness domain t < r.

@[simp]

theorem TauCeti.Probability.cgf_id_expMeasure {r t : ℝ} (hr : 0 < r) (ht : t < r) : ProbabilityTheory.cgf id (ProbabilityTheory.expMeasure r) t = Real.log (r / (r - t))

The cumulant-generating function of an exponential law with positive rate.

@[simp]

theorem TauCeti.Probability.charFun_expMeasure {r : ℝ} (hr : 0 < r) (t : ℝ) : MeasureTheory.charFun (ProbabilityTheory.expMeasure r) t = ↑r / (↑r - Complex.I * ↑t)

The characteristic function of an exponential law with positive rate.

@[simp]

theorem TauCeti.Probability.measureReal_Ioi_expMeasure {r : ℝ} (hr : 0 < r) (x : ℝ) : (ProbabilityTheory.expMeasure r).real (Set.Ioi x) = if 0 ≤ x then Real.exp (-(r * x)) else 1

The real-valued tail probability of a positive-rate exponential law.

@[simp]

theorem TauCeti.Probability.measure_Ioi_expMeasure {r : ℝ} (hr : 0 < r) (x : ℝ) : (ProbabilityTheory.expMeasure r) (Set.Ioi x) = ENNReal.ofReal (if 0 ≤ x then Real.exp (-(r * x)) else 1)

The tail probability of a positive-rate exponential law.

theorem TauCeti.Probability.memoryless_expMeasure {r s t : ℝ} (hr : 0 < r) (hs : 0 ≤ s) (ht : 0 ≤ t) : (ProbabilityTheory.expMeasure r)[Set.Ioi (s + t) | Set.Ioi s] = (ProbabilityTheory.expMeasure r) (Set.Ioi t)

The memoryless property of a positive-rate exponential law, stated with conditional probability: after surviving for time s, the chance of surviving a further time t is the original tail probability at t.

theorem TauCeti.Probability.map_min_expMeasure {r s : ℝ} (hr : 0 < r) (hs : 0 < s) : MeasureTheory.Measure.map (fun (z : ℝ × ℝ) => min z.1 z.2) ((ProbabilityTheory.expMeasure r).prod (ProbabilityTheory.expMeasure s)) = ProbabilityTheory.expMeasure (r + s)

The minimum of independent exponential laws is exponential. Mapping the product of positive-rate exponential laws under the pointwise minimum gives the exponential law whose rate is the sum of the input rates.

theorem TauCeti.Probability.hasLaw_min_expMeasure_of_indepFun {r s : ℝ} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} (hr : 0 < r) (hs : 0 < s) (hXY : ProbabilityTheory.IndepFun X Y P) (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.expMeasure r) P) (hY : ProbabilityTheory.HasLaw Y (ProbabilityTheory.expMeasure s) P) : ProbabilityTheory.HasLaw (fun (ω : Ω) => min (X ω) (Y ω)) (ProbabilityTheory.expMeasure (r + s)) P

The minimum of two independent random variables with exponential laws has an exponential law whose rate is the sum of their rates.

theorem TauCeti.Probability.hasLaw_min_iid_expMeasure {r : ℝ} {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Fintype ι] [Nonempty ι] {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} (hr : 0 < r) (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : ι), ProbabilityTheory.HasLaw (X i) (ProbabilityTheory.expMeasure r) P) : ProbabilityTheory.HasLaw (fun (ω : Ω) => Finset.univ.inf' ⋯ fun (i : ι) => X i ω) (ProbabilityTheory.expMeasure (↑(Fintype.card ι) * r)) P

The minimum of d independent exponential variables of a common positive rate r is exponential of rate d * r. This is the d-fold form of TauCeti.Probability.hasLaw_min_expMeasure_of_indepFun, which allows two different rates.

noncomputable def TauCeti.Probability.nnrealExpMeasure (r : ℝ) : MeasureTheory.Measure NNReal

The exponential measure of rate r on ℝ≥0, obtained by transporting the usual exponential law on ℝ along Real.toNNReal.

For r > 0 this transport loses no information because the exponential law is supported on the nonnegative half-line.

Equations

• TauCeti.Probability.nnrealExpMeasure r = MeasureTheory.Measure.map Real.toNNReal (ProbabilityTheory.expMeasure r)

theorem TauCeti.Probability.nnrealExpMeasure_def (r : ℝ) : nnrealExpMeasure r = MeasureTheory.Measure.map Real.toNNReal (ProbabilityTheory.expMeasure r)

The exponential measure on ℝ≥0 is the pushforward of Mathlib's exponential measure along Real.toNNReal.

theorem TauCeti.Probability.nnrealExpMeasure_one_eq_map_withDensity : nnrealExpMeasure 1 = MeasureTheory.Measure.map Real.toNNReal (MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (if 0 ≤ x then Real.exp (-x) else 0))

At unit rate, nnrealExpMeasure is the measure with density e⁻ˣ on the nonnegative real half-line, transported to ℝ≥0. The displayed if makes the zero density on negative reals explicit before the transport.

theorem TauCeti.Probability.isProbabilityMeasure_nnrealExpMeasure {r : ℝ} (hr : 0 < r) : MeasureTheory.IsProbabilityMeasure (nnrealExpMeasure r)

The positive-rate exponential measure on ℝ≥0 is a probability measure.