Bernstein functions are the exponents of completely monotone semigroups

TauCeti.IsBernsteinFunction.isContinuousCompletelyMonotoneOnIoi_exp_neg_mul produces, from a Bernstein function f, the completely monotone functions t ↦ e^{-x f(t)} for every x ≥ 0 — the Laplace transforms of the subprobability convolution semigroup subordinate to f. This file proves the converse, so that the two classes determine each other:

f is a Bernstein function if and only if f is nonnegative on [0, ∞) and, for every x > 0, e^{-x f} is continuous on [0, ∞) and completely monotone on (0, ∞).

This is the standard correspondence between the two classes, and the form in which Bernstein functions enter probability theory: e^{-x f} completely monotone for all x > 0 says exactly that f is the Laplace exponent of a possibly killed subordinator, the killing rate being f 0, which this library allows to be positive.

Quantifying over all x > 0 is essential, and the proof shows why: differentiating t ↦ e^{-x f(t)} gives the exact identity

- x⁻¹ · (e^{-x f})'(t) = f'(t) · e^{-x f(t)},

so the left-hand side is completely monotone by TauCeti.IsCompletelyMonotoneOnIoi.neg_deriv, and letting x ↓ 0 along x = 1 / (n + 1) makes the right-hand side converge pointwise to f'. Complete monotonicity survives that limit by TauCeti.isCompletelyMonotoneOnIoi_of_tendsto, which is the whole content: a single x says far less, since it constrains only one member of the family.

The remaining hypotheses of TauCeti.IsBernsteinFunction are recovered from the exponentials rather than assumed, through TauCeti.contDiffOn_of_contDiffOn_exp_const_mul: smoothness of f on (0, ∞) comes from that of e^{-x f}, and only right-continuity of f at 0 is left to hypothesize, the rest of its continuity on [0, ∞) following from the smoothness. Nonnegativity of f is genuinely independent — the constant -1 has e^{x} for its exponentials, and constants are completely monotone.

Main declarations

• TauCeti.isCompletelyMonotoneOnIoi_deriv_mul_exp_neg_mul: for x > 0, the function t ↦ f'(t) · e^{-x f(t)} is completely monotone on (0, ∞) whenever e^{-x f} is.
• TauCeti.isBernsteinFunction_of_forall_isCompletelyMonotoneOnIoi_exp_neg_mul: the converse direction, that the family of exponentials forces f to be a Bernstein function.
• isBernsteinFunction_iff_nonneg_and_forall_isContinuousCompletelyMonotoneOnIoi_exp_neg_mul: the resulting characterization of Bernstein functions.

References

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

theorem TauCeti.isCompletelyMonotoneOnIoi_deriv_mul_exp_neg_mul {f : ℝ → ℝ} {x : ℝ} (hx : 0 < x) (h : IsCompletelyMonotoneOnIoi fun (t : ℝ) => Real.exp (-x * f t)) : IsCompletelyMonotoneOnIoi fun (t : ℝ) => deriv f t * Real.exp (-x * f t)

The derivative of f weighted by an exponential. If e^{-x f} is completely monotone on (0, ∞) for some x > 0, then so is t ↦ f'(t) · e^{-x f(t)}, because that function is -x⁻¹ times the derivative of e^{-x f}.

theorem TauCeti.isBernsteinFunction_of_forall_isCompletelyMonotoneOnIoi_exp_neg_mul {f : ℝ → ℝ} (hzero : ContinuousWithinAt f (Set.Ici 0) 0) (hnonneg : ∀ (t : ℝ), 0 ≤ t → 0 ≤ f t) (h : ∀ (x : ℝ), 0 < x → IsCompletelyMonotoneOnIoi fun (t : ℝ) => Real.exp (-x * f t)) : IsBernsteinFunction f

The exponentials of a Bernstein function determine it. If f is nonnegative on [0, ∞), right-continuous at 0, and e^{-x f} is completely monotone on (0, ∞) for every x > 0, then f is a Bernstein function.

This is the converse of TauCeti.IsBernsteinFunction.isContinuousCompletelyMonotoneOnIoi_exp_neg_mul; smoothness of f on (0, ∞) is not assumed, but deduced from the exponential at x = 1, and with it continuity of f away from the endpoint.

theorem TauCeti.isBernsteinFunction_iff_nonneg_and_forall_isContinuousCompletelyMonotoneOnIoi_exp_neg_mul {f : ℝ → ℝ} : IsBernsteinFunction f ↔ (∀ (t : ℝ), 0 ≤ t → 0 ≤ f t) ∧ ∀ (x : ℝ), 0 < x → IsContinuousCompletelyMonotoneOnIoi fun (t : ℝ) => Real.exp (-x * f t)

The characterization of Bernstein functions by complete monotonicity of their exponentials. A function is a Bernstein function exactly when it is nonnegative on [0, ∞) and each e^{-x f}, x > 0, is completely monotone on (0, ∞) and continuous on [0, ∞).

Continuity of f itself is not part of the right-hand side: it is recovered from continuity of one exponential. Nonnegativity is not: the constant -1 satisfies every other clause.