Levy--Khintchine exponents of Bernstein functions

This file develops the forward half of the Levy--Khintchine representation for Bernstein functions. A measure mu on ℝ≥0 is a Bernstein Levy measure when it has no atom at zero and min 1 x is integrable. Its jump exponent is

t ↦ ∫ x, (1 - exp (-t * x)) ∂mu.

The integrability condition ensures that this integral is finite: it controls the kernel linearly near zero and by a constant at infinity. The derivative at every positive time is the Laplace transform of the measure with density x with respect to mu. That transform is completely monotone, so the jump exponent, and hence its sum with nonnegative killing and drift terms, is a Bernstein function.

Main declarations

• TauCeti.IsBernsteinLevyMeasure: the standard integrability and no-atom-at-zero condition.
• TauCeti.bernsteinLevyJumpExponent: the jump part of a Bernstein function's Levy--Khintchine representation.
• TauCeti.bernsteinLevyDerivativeMeasure: coordinate-weighting of a Levy measure, whose Laplace transform is the derivative of the jump exponent; it is inverted by TauCeti.withDensity_inv_bernsteinLevyDerivativeMeasure.
• TauCeti.isBernsteinFunction_bernsteinLevyJumpExponent: an integrable Levy jump exponent is a Bernstein function.
• TauCeti.isBernsteinFunction_bernsteinLevyKhintchineExponent: adding nonnegative killing and drift terms preserves the Bernstein property.

Existence of the converse triplet is proved in TauCeti.Analysis.CompletelyMonotone.Bernstein.LevyKhintchine.Representation, and uniqueness in TauCeti.Analysis.CompletelyMonotone.Bernstein.LevyKhintchine.Uniqueness.

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).

def TauCeti.IsBernsteinLevyMeasure (μ : MeasureTheory.Measure NNReal) : Prop

A measure on ℝ≥0 is a Bernstein Levy measure when it has no atom at zero and x ↦ min 1 x is integrable. This is the standard Levy-measure condition for subordinators.

Equations

• TauCeti.IsBernsteinLevyMeasure μ = (μ {0} = 0 ∧ MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ)

@[simp]

theorem TauCeti.isBernsteinLevyMeasure_iff {μ : MeasureTheory.Measure NNReal} : IsBernsteinLevyMeasure μ ↔ μ {0} = 0 ∧ MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ

Characterization of a Bernstein Levy measure by its two defining conditions.

theorem TauCeti.isBernsteinLevyMeasure_zero : IsBernsteinLevyMeasure 0

The zero measure is a Bernstein Levy measure.

theorem TauCeti.IsBernsteinLevyMeasure.measure_singleton_zero {μ : MeasureTheory.Measure NNReal} (hμ : IsBernsteinLevyMeasure μ) : μ {0} = 0

A Bernstein Levy measure has no atom at zero.

theorem TauCeti.IsBernsteinLevyMeasure.integrable_min_one {μ : MeasureTheory.Measure NNReal} (hμ : IsBernsteinLevyMeasure μ) : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ

The truncated coordinate is integrable against a Bernstein Levy measure.

theorem TauCeti.IsBernsteinLevyMeasure.add {μ ν : MeasureTheory.Measure NNReal} (hμ : IsBernsteinLevyMeasure μ) (hν : IsBernsteinLevyMeasure ν) : IsBernsteinLevyMeasure (μ + ν)

Bernstein Levy measures are closed under addition.

theorem TauCeti.isBernsteinLevyMeasure_dirac {x : NNReal} (hx : x ≠ 0) : IsBernsteinLevyMeasure (MeasureTheory.Measure.dirac x)

A Dirac mass away from zero is a Bernstein Levy measure.

noncomputable def TauCeti.bernsteinLevyJumpExponent (μ : MeasureTheory.Measure NNReal) (t : ℝ) : ℝ

The jump exponent associated to a measure on ℝ≥0. Integrability of the truncated coordinate guarantees integrability of its kernel at nonnegative parameters.

Equations

• TauCeti.bernsteinLevyJumpExponent μ t = ∫ (x : NNReal), 1 - Real.exp (-(t * ↑x)) ∂μ

@[simp]

theorem TauCeti.bernsteinLevyJumpExponent_apply (μ : MeasureTheory.Measure NNReal) (t : ℝ) : bernsteinLevyJumpExponent μ t = ∫ (x : NNReal), 1 - Real.exp (-(t * ↑x)) ∂μ

The defining integral of the Bernstein Levy exponent.

noncomputable def TauCeti.bernsteinLevyKhintchineExponent (a b : ℝ) (μ : MeasureTheory.Measure NNReal) (t : ℝ) : ℝ

The Levy--Khintchine function with killing coefficient a, drift coefficient b, and jump measure μ.

Equations

• TauCeti.bernsteinLevyKhintchineExponent a b μ t = a + b * t + TauCeti.bernsteinLevyJumpExponent μ t

@[simp]

theorem TauCeti.bernsteinLevyKhintchineExponent_apply (a b : ℝ) (μ : MeasureTheory.Measure NNReal) (t : ℝ) : bernsteinLevyKhintchineExponent a b μ t = a + b * t + bernsteinLevyJumpExponent μ t

The defining formula for the Bernstein Levy--Khintchine function.

theorem TauCeti.integrable_one_sub_exp_neg_mul_of_integrable_min_one {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ) {t : ℝ} (ht : 0 ≤ t) : MeasureTheory.Integrable (fun (x : NNReal) => 1 - Real.exp (-(t * ↑x))) μ

The Levy jump kernel is integrable at every nonnegative parameter.

theorem TauCeti.integrable_mul_exp_neg_mul_of_integrable_min_one {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ) {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (fun (x : NNReal) => ↑x * Real.exp (-(t * ↑x))) μ

The derivative kernel of the Levy jump exponent is integrable at every positive parameter.

theorem TauCeti.bernsteinLevyJumpExponent_nonneg (μ : MeasureTheory.Measure NNReal) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ bernsteinLevyJumpExponent μ t

The jump exponent is nonnegative at nonnegative parameters.

theorem TauCeti.bernsteinLevyJumpExponent_zero (μ : MeasureTheory.Measure NNReal) : bernsteinLevyJumpExponent μ 0 = 0

Every Levy jump exponent vanishes at zero.

theorem TauCeti.bernsteinLevyJumpExponent_zero_measure (t : ℝ) : bernsteinLevyJumpExponent 0 t = 0

The zero measure has identically zero Levy jump exponent.

noncomputable def TauCeti.bernsteinLevyDerivativeMeasure (μ : MeasureTheory.Measure NNReal) : MeasureTheory.Measure NNReal

Weighting a Bernstein Levy measure by the coordinate gives the measure whose Laplace transform is the derivative of its jump exponent.

Equations

• TauCeti.bernsteinLevyDerivativeMeasure μ = μ.withDensity fun (x : NNReal) => ↑x

@[simp]

theorem TauCeti.bernsteinLevyDerivativeMeasure_apply (μ : MeasureTheory.Measure NNReal) {s : Set NNReal} (hs : MeasurableSet s) : (bernsteinLevyDerivativeMeasure μ) s = ∫⁻ (x : NNReal) in s, ↑x ∂μ

The mass that the coordinate-weighted Levy measure assigns to a measurable set.

theorem TauCeti.withDensity_inv_bernsteinLevyDerivativeMeasure {μ : MeasureTheory.Measure NNReal} (hμ : μ {0} = 0) : ((bernsteinLevyDerivativeMeasure μ).withDensity fun (x : NNReal) => (↑x)⁻¹) = μ

Dividing out the coordinate weight recovers a Levy measure from its coordinate-weighted counterpart, since the weight is invertible away from the zero-mass point 0.

theorem TauCeti.integrable_exp_neg_mul_bernsteinLevyDerivativeMeasure {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ) {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (fun (x : NNReal) => Real.exp (-(t * ↑x))) (bernsteinLevyDerivativeMeasure μ)

The exponential kernel is integrable against a coordinate-weighted Levy measure at every positive parameter.

theorem TauCeti.laplaceTransform_bernsteinLevyDerivativeMeasure (μ : MeasureTheory.Measure NNReal) (t : ℝ) : laplaceTransform (bernsteinLevyDerivativeMeasure μ) t = ∫ (x : NNReal), ↑x * Real.exp (-(t * ↑x)) ∂μ

The Laplace transform of the coordinate-weighted Levy measure is the exponentially damped first moment of the original measure.

theorem TauCeti.representsLaplaceOnIoi_bernsteinLevyDerivativeMeasure {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ) : RepresentsLaplaceOnIoi (bernsteinLevyDerivativeMeasure μ) fun (t : ℝ) => ∫ (x : NNReal), ↑x * Real.exp (-(t * ↑x)) ∂μ

The coordinate-weighted Levy measure represents the exponentially damped first moment of the original measure by its Laplace transform on the positive half-line.

theorem TauCeti.continuousOn_bernsteinLevyJumpExponent {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ) : ContinuousOn (bernsteinLevyJumpExponent μ) (Set.Ici 0)

The Levy jump exponent of a measure with integrable truncated coordinate is continuous on the nonnegative half-line, including at the endpoint 0.

theorem TauCeti.hasDerivAt_bernsteinLevyJumpExponent {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ) {t : ℝ} (ht : 0 < t) : HasDerivAt (bernsteinLevyJumpExponent μ) (∫ (x : NNReal), ↑x * Real.exp (-(t * ↑x)) ∂μ) t

At a positive parameter, a Levy jump exponent has derivative equal to the exponentially damped first moment of its measure.

theorem TauCeti.deriv_bernsteinLevyJumpExponent {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ) {t : ℝ} (ht : 0 < t) : deriv (bernsteinLevyJumpExponent μ) t = ∫ (x : NNReal), ↑x * Real.exp (-(t * ↑x)) ∂μ

At a positive parameter, the derivative of a Levy jump exponent is the exponentially damped first moment of its Levy measure.

theorem TauCeti.isBernsteinFunction_bernsteinLevyJumpExponent_of_integrable_min_one {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ) : IsBernsteinFunction (bernsteinLevyJumpExponent μ)

Integrability of min 1 x suffices for the Levy jump exponent to be a Bernstein function. No condition at the origin is needed, because an atom at zero contributes the identically zero jump kernel.

theorem TauCeti.isBernsteinFunction_bernsteinLevyJumpExponent {μ : MeasureTheory.Measure NNReal} (hμ : IsBernsteinLevyMeasure μ) : IsBernsteinFunction (bernsteinLevyJumpExponent μ)

A Bernstein Levy measure gives a Bernstein function through its jump exponent.

theorem TauCeti.isBernsteinFunction_bernsteinLevyKhintchineExponent_of_integrable_min_one {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : IsBernsteinFunction (bernsteinLevyKhintchineExponent a b μ)

Nonnegative killing and drift coefficients together with an integrable Levy jump measure give a Bernstein function by the Levy--Khintchine formula.

theorem TauCeti.isBernsteinFunction_bernsteinLevyKhintchineExponent {μ : MeasureTheory.Measure NNReal} (hμ : IsBernsteinLevyMeasure μ) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : IsBernsteinFunction (bernsteinLevyKhintchineExponent a b μ)

Nonnegative killing and drift coefficients together with a Bernstein Levy measure give a Bernstein function by the Levy--Khintchine formula.

theorem TauCeti.bernsteinLevyJumpExponent_add_measure {μ ν : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ) (hν : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) ν) {t : ℝ} (ht : 0 ≤ t) : bernsteinLevyJumpExponent (μ + ν) t = bernsteinLevyJumpExponent μ t + bernsteinLevyJumpExponent ν t

At a nonnegative parameter, the Levy jump exponent of a sum of measures with integrable truncated coordinates is the sum of their jump exponents.

theorem TauCeti.deriv_bernsteinLevyKhintchineExponent {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable (fun (x : NNReal) => min 1 ↑x) μ) (a b : ℝ) {t : ℝ} (ht : 0 < t) : deriv (bernsteinLevyKhintchineExponent a b μ) t = b + ∫ (x : NNReal), ↑x * Real.exp (-(t * ↑x)) ∂μ

At a positive parameter, the derivative of a Levy--Khintchine exponent is its drift coefficient plus the exponentially damped first moment of its jump measure.

theorem TauCeti.bernsteinLevyJumpExponent_dirac (x : NNReal) (t : ℝ) : bernsteinLevyJumpExponent (MeasureTheory.Measure.dirac x) t = 1 - Real.exp (-(t * ↑x))

A one-atom Levy measure gives the prototype jump exponent 1 - exp (-t x).

theorem TauCeti.bernsteinLevyKhintchineExponent_zero (a b : ℝ) (μ : MeasureTheory.Measure NNReal) : bernsteinLevyKhintchineExponent a b μ 0 = a

At zero, the Levy--Khintchine function is its killing coefficient.