Uniqueness of the Levy--Khintchine representation

This file completes the Levy--Khintchine representation of Bernstein functions by proving that its killing coefficient, drift coefficient, and Levy measure are unique. The killing coefficient is the value of the exponent at zero, which agreement on the positive half-line already fixes because the exponent is continuous at that endpoint. For the other two parameters, differentiating on the positive half-line gives the Laplace transform of

b delta_0 + x mu(dx).

Uniqueness of open-half-line Laplace representations identifies these derivative measures. Their mass at zero recovers the drift b; after cancelling that atom, multiplication by x is invertible away from zero, and the Levy condition mu {0} = 0 recovers mu.

Main declarations

• TauCeti.eq_of_eqOn_bernsteinLevyKhintchineExponent: two Levy--Khintchine triplets defining the same function on (0, infinity) are equal.
• TauCeti.IsBernsteinFunction.existsUnique_eqOn_bernsteinLevyKhintchineExponent: every Bernstein function has a unique Levy--Khintchine triplet.

References

• R. Schilling, R. Song, Z. Vondracek, Bernstein Functions: Theory and Applications (de Gruyter, 2nd ed. 2012), Theorem 3.2.

theorem TauCeti.eq_of_eqOn_bernsteinLevyKhintchineExponent {a b a' b' : ℝ} {μ ν : MeasureTheory.Measure NNReal} (hμ : IsBernsteinLevyMeasure μ) (hν : IsBernsteinLevyMeasure ν) (hb : 0 ≤ b) (hb' : 0 ≤ b') (heq : Set.EqOn (bernsteinLevyKhintchineExponent a b μ) (bernsteinLevyKhintchineExponent a' b' ν) (Set.Ioi 0)) : a = a' ∧ b = b' ∧ μ = ν

Uniqueness of Levy--Khintchine triplets. If two triplets give the same function on the positive half-line, then their killing coefficients, drift coefficients, and Levy measures are respectively equal.

theorem TauCeti.IsBernsteinFunction.existsUnique_eqOn_bernsteinLevyKhintchineExponent {f : ℝ → ℝ} (hf : IsBernsteinFunction f) : ∃! p : ℝ × ℝ × MeasureTheory.Measure NNReal, 0 ≤ p.1 ∧ 0 ≤ p.2.1 ∧ IsBernsteinLevyMeasure p.2.2 ∧ Set.EqOn f (bernsteinLevyKhintchineExponent p.1 p.2.1 p.2.2) (Set.Ici 0)

Every Bernstein function has a unique Levy--Khintchine triplet. The components of the triple are respectively the killing coefficient, drift coefficient, and Levy measure.