Finite mixtures of completely monotone exponential functions

The extreme rays of the cone of completely monotone functions are the exponential functions t ↦ exp (-p * t) with p ≥ 0. This file develops their finite positive mixtures. It packages a finite mixture both as an explicit sum and as the Laplace transform of the corresponding finite sum of weighted Dirac measures.

This is the finite-support case of the measure representation in Bernstein's theorem. In particular, a single atom of unit weight at p = 1 represents t ↦ exp (-t), one of the acceptance examples in the one-parameter-semigroups roadmap.

Main declarations

• TauCeti.finiteExponentialMixture: a finite positive mixture of exponential extreme rays.
• TauCeti.finiteExponentialMixtureMeasure: the corresponding finite sum of weighted Dirac measures on ℝ≥0.
• TauCeti.isCompletelyMonotone_finiteExponentialMixture: every finite exponential mixture is completely monotone.
• TauCeti.finiteExponentialMixture_eq_integral: the explicit sum is the Laplace transform of its discrete representing measure.
• TauCeti.integral_exp_neg_mul_dirac_one: the acceptance example exp (-t) ↔ δ₁.

References

• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications (de Gruyter, 2nd ed. 2012), Chapter 1.

noncomputable def TauCeti.finiteExponentialMixture {ι : Type u_1} (s : Finset ι) (w p : ι → NNReal) (t : ℝ) : ℝ

A finite positive mixture of the exponential extreme rays t ↦ exp (-p * t).

The weights and rates are indexed by a finset. Both take values in ℝ≥0, making their nonnegativity intrinsic to the data.

Equations

• TauCeti.finiteExponentialMixture s w p t = ∑ i ∈ s, ↑(w i) * Real.exp (-↑(p i) * t)

@[simp]

theorem TauCeti.finiteExponentialMixture_empty {ι : Type u_1} (w p : ι → NNReal) : finiteExponentialMixture ∅ w p = 0

The empty exponential mixture is the zero function.

@[simp]

theorem TauCeti.finiteExponentialMixture_singleton {ι : Type u_1} (i : ι) (w p : ι → NNReal) (t : ℝ) : finiteExponentialMixture {i} w p t = ↑(w i) * Real.exp (-↑(p i) * t)

A singleton exponential mixture is one weighted exponential extreme ray.

theorem TauCeti.isCompletelyMonotone_finiteExponentialMixture {ι : Type u_1} (s : Finset ι) (w p : ι → NNReal) : IsCompletelyMonotone (finiteExponentialMixture s w p)

Every finite positive mixture of exponential extreme rays is completely monotone.

noncomputable def TauCeti.finiteExponentialMixtureMeasure {ι : Type u_1} (s : Finset ι) (w p : ι → NNReal) : MeasureTheory.Measure NNReal

The finite positive measure that places weight w i at each rate p i.

Repeated rates are intentionally allowed: measure addition combines their weights.

Equations

• TauCeti.finiteExponentialMixtureMeasure s w p = ∑ i ∈ s, ↑(w i) • MeasureTheory.Measure.dirac (p i)

@[simp]

theorem TauCeti.finiteExponentialMixtureMeasure_apply {ι : Type u_1} (s : Finset ι) (w p : ι → NNReal) {A : Set NNReal} (hA : MeasurableSet A) : (finiteExponentialMixtureMeasure s w p) A = ∑ i ∈ s, A.indicator (fun (x : NNReal) => ↑(w i)) (p i)

The representing measure of a measurable set is the sum of the weights at rates in the set.

@[simp]

theorem TauCeti.finiteExponentialMixtureMeasure_empty {ι : Type u_1} (w p : ι → NNReal) : finiteExponentialMixtureMeasure ∅ w p = 0

The empty exponential mixture has the zero representing measure.

@[simp]

theorem TauCeti.finiteExponentialMixtureMeasure_singleton {ι : Type u_1} (i : ι) (w p : ι → NNReal) : finiteExponentialMixtureMeasure {i} w p = ↑(w i) • MeasureTheory.Measure.dirac (p i)

A singleton mixture has the corresponding weighted Dirac representing measure.

theorem TauCeti.finiteExponentialMixture_eq_integral {ι : Type u_1} (s : Finset ι) (w p : ι → NNReal) (t : ℝ) : finiteExponentialMixture s w p t = ∫ (q : NNReal), Real.exp (-t * ↑q) ∂finiteExponentialMixtureMeasure s w p

A finite exponential mixture is the Laplace transform of its discrete representing measure.

theorem TauCeti.integral_exp_neg_mul_dirac_one (t : ℝ) : ∫ (q : NNReal), Real.exp (-t * ↑q) ∂MeasureTheory.Measure.dirac 1 = Real.exp (-t)

The Laplace transform of the unit Dirac mass at 1 is t ↦ exp (-t).

This is the discrete representing-measure acceptance example for Bernstein's theorem.

theorem TauCeti.finiteExponentialMixture_singleton_one (t : ℝ) : finiteExponentialMixture {()} (fun (x : Unit) => 1) (fun (x : Unit) => 1) t = Real.exp (-t)

The exponential t ↦ exp (-t) is the unit-weight, unit-rate finite exponential mixture.