Levy--Khintchine representation of Bernstein functions

This file proves the existence part of the converse Levy--Khintchine representation: every Bernstein function is the sum of a nonnegative killing term, a nonnegative linear drift, and the jump exponent of a Bernstein Levy measure. Uniqueness of the three parameters is proved in TauCeti.Analysis.CompletelyMonotone.Bernstein.LevyKhintchine.Uniqueness.

The proof represents the completely monotone derivative by a measure sigma. The atom of sigma at zero is the drift coefficient, while weighting sigma by x⁻¹ away from zero gives the Levy measure. Continuity of the Bernstein function at zero is exactly what makes the truncated coordinate integrable against this weighted measure.

Main declaration

• TauCeti.IsBernsteinFunction.exists_eqOn_bernsteinLevyKhintchineExponent: existence of a Levy--Khintchine triplet for a Bernstein function.
• TauCeti.isBernsteinFunction_iff_exists_bernsteinLevyKhintchineExponent: the resulting characterization of Bernstein functions.

References

• R. Schilling, R. Song, Z. Vondracek, Bernstein Functions: Theory and Applications (de Gruyter, 2nd ed. 2012), Theorem 3.2.
• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part B (Levy--Khintchine representation of Bernstein functions).

theorem TauCeti.IsBernsteinFunction.exists_eqOn_bernsteinLevyKhintchineExponent {f : ℝ → ℝ} (hf : IsBernsteinFunction f) : ∃ (a : ℝ) (b : ℝ) (μ : MeasureTheory.Measure NNReal), 0 ≤ a ∧ 0 ≤ b ∧ IsBernsteinLevyMeasure μ ∧ Set.EqOn f (bernsteinLevyKhintchineExponent a b μ) (Set.Ici 0)

Every Bernstein function admits a Levy--Khintchine representation on the nonnegative half-line. The witnesses are a killing coefficient, a drift coefficient, and a Levy measure; this theorem asserts existence only.

theorem TauCeti.isBernsteinFunction_iff_exists_bernsteinLevyKhintchineExponent {f : ℝ → ℝ} : IsBernsteinFunction f ↔ ∃ (a : ℝ) (b : ℝ) (μ : MeasureTheory.Measure NNReal), 0 ≤ a ∧ 0 ≤ b ∧ IsBernsteinLevyMeasure μ ∧ Set.EqOn f (bernsteinLevyKhintchineExponent a b μ) (Set.Ici 0)

A function is Bernstein exactly when it has a Levy--Khintchine representation on the nonnegative half-line.