Extremal completely monotone functions are exponentials

The functions that are continuous on [0, ∞) and completely monotone on (0, ∞) form a convex cone. A nonzero function f in this cone spans an extreme ray exactly when it satisfies the decomposition condition: every decomposition f = g + h inside the cone, compared on [0, ∞), has g a scalar multiple of f. This file shows that any f in the cone satisfying the decomposition condition (including f = 0) is t ↦ f 0 * exp (-(t * p)) on [0, ∞) for some rate p ≥ 0: the exponentials are the only possible extreme rays.

Main declarations

• TauCeti.IsContinuousCompletelyMonotoneOnIoi.exists_eq_mul_exp_neg_mul_of_extreme_ray: a completely monotone function satisfying the decomposition condition (in particular, one spanning an extreme ray) is a nonnegative multiple of an exponential.

References

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

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.exists_eq_mul_exp_neg_mul_of_extreme_ray {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) (hext : ∀ (g h : ℝ → ℝ), IsContinuousCompletelyMonotoneOnIoi g → IsContinuousCompletelyMonotoneOnIoi h → (∀ (t : ℝ), 0 ≤ t → g t + h t = f t) → ∃ (a : ℝ), ∀ (t : ℝ), 0 ≤ t → g t = a * f t) : ∃ (p : NNReal), ∀ (t : ℝ), 0 ≤ t → f t = f 0 * Real.exp (-(t * ↑p))

Extreme rays of the completely monotone cone are exponential. Let f be continuous on [0, ∞) and completely monotone on (0, ∞), and suppose that whenever f = g + h on [0, ∞) with g and h of the same kind, g is a scalar multiple of f on [0, ∞). Then f t = f 0 * exp (-(t * p)) for all t ≥ 0, for some rate p ≥ 0.