Exponential measures as Bernstein representing measures

The exponential probability measure with rate r > 0, transported from ℝ to ℝ≥0, has Laplace transform

t ↦ r / (r + t).

This gives a continuous, non-atomic example of Bernstein's theorem: at unit rate the function t ↦ 1 / (1 + t) is represented by the measure with density e⁻ˣ on [0, ∞). Unlike the Dirac examples, this exercises a genuinely continuous representing measure.

The measure is defined in TauCeti.Probability.Distributions.Exponential.Basic by pushing Mathlib's ProbabilityTheory.expMeasure forward along Real.toNNReal. A positive-rate exponential random variable is nonnegative almost surely, so this transport retains the law and turns its moment-generating-function formula into the required Laplace-transform formula.

Main declarations

• TauCeti.laplaceTransform_nnrealExpMeasure: its Laplace transform is r / (r + t).
• TauCeti.representsLaplace_nnrealExpMeasure: the resulting Bernstein representation.
• TauCeti.bernsteinMeasure_one_div_one_add: the canonical Bernstein measure of t ↦ 1 / (1 + t) is the unit-rate exponential measure.

References

• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications, 2nd ed., Example 1.4 and Theorem 1.4.

theorem TauCeti.laplaceTransform_nnrealExpMeasure {r t : ℝ} (hr : 0 < r) (ht : -r < t) : laplaceTransform (Probability.nnrealExpMeasure r) t = r / (r + t)

The Laplace transform of the exponential measure of rate r > 0 is r / (r + t) throughout its maximal finiteness domain -r < t.

theorem TauCeti.representsLaplace_nnrealExpMeasure {r : ℝ} (hr : 0 < r) : RepresentsLaplace (Probability.nnrealExpMeasure r) fun (t : ℝ) => r / (r + t)

The positive-rate exponential measure represents t ↦ r / (r + t) in Bernstein's theorem.

theorem TauCeti.bernsteinMeasure_div_add {r : ℝ} (hr : 0 < r) : (bernsteinMeasure fun (t : ℝ) => r / (r + t)) = Probability.nnrealExpMeasure r

The canonical Bernstein representing measure of t ↦ r / (r + t), for positive r, is the exponential measure of rate r on ℝ≥0.

theorem TauCeti.representsLaplace_nnrealExpMeasure_one : RepresentsLaplace (Probability.nnrealExpMeasure 1) fun (t : ℝ) => 1 / (1 + t)

At unit rate, the exponential measure on ℝ≥0 represents t ↦ 1 / (1 + t).

theorem TauCeti.bernsteinMeasure_one_div_one_add : (bernsteinMeasure fun (t : ℝ) => 1 / (1 + t)) = Probability.nnrealExpMeasure 1

The canonical Bernstein representing measure of t ↦ 1 / (1 + t) is the unit-rate exponential measure on ℝ≥0.