Complete Bernstein functions and Stieltjes functions

A complete Bernstein function has a representation

g(t) = a + b t + ∫ x, t / (t + x) ∂μ,

where a, b ≥ 0, the positive measure μ has no atom at zero, and ∫ (1 + x)⁻¹ ∂μ < ∞. The normalization μ {0} = 0 stops an atom at zero from making the integral term jump — such an atom contributes 1 at every positive parameter and 0 at zero — so the integral term vanishes at zero and the representation is the intended continuous extension. This file packages that standard representation and proves the first fundamental correspondence: f is Stieltjes exactly when t ↦ t f(t) on (0, ∞) has a complete Bernstein extension to [0, ∞).

The predicate defined here is the integral representation, that is, the representing clause of the cited theorem, and it carries exactly the data μ, a, b of TauCeti.RepresentsStieltjes. The correspondence below is therefore the change of normalization f ↦ t f(t) performed on that shared data. The equivalence of the representation with the analytic characterizations of a complete Bernstein function — extension to a Pick function on ℂ ∖ (-∞, 0], or operator monotonicity — is not formalized here.

The extension is necessary when the Stieltjes representation has a nonzero a / t term: its value at zero must be a, whereas the literal product 0 * f(0) is zero. Values of a Stieltjes function outside (0, ∞) remain irrelevant, and values of a complete Bernstein function outside [0, ∞) remain irrelevant.

Main declarations

• TauCeti.RepresentsCompleteBernstein: complete-Bernstein representing data, with the accessors measure_singleton_zero, integrable_weight, eq_stieltjesBernsteinTransform, apply_zero and congr.
• TauCeti.IsCompleteBernsteinFunction: the representation-based predicate.
• TauCeti.representsCompleteBernstein_stieltjesBernsteinTransform and TauCeti.isCompleteBernsteinFunction_stieltjesBernsteinTransform: the transform of normalized, integrable representing data carries the representation.
• TauCeti.RepresentsCompleteBernstein.add, TauCeti.RepresentsCompleteBernstein.smul, TauCeti.IsCompleteBernsteinFunction.add and TauCeti.IsCompleteBernsteinFunction.smul: complete Bernstein functions are closed under sums and nonnegative scalar multiples.
• TauCeti.IsCompleteBernsteinFunction.isBernsteinFunction: a complete Bernstein function is a Bernstein function.
• TauCeti.RepresentsCompleteBernstein.representsStieltjes_div and TauCeti.IsCompleteBernsteinFunction.isStieltjesFunction_div: dividing a complete Bernstein function by its parameter gives a Stieltjes function.
• TauCeti.isStieltjesFunction_iff_exists_isCompleteBernsteinFunction_eqOn_mul: the Stieltjes--complete-Bernstein correspondence.
• TauCeti.isCompleteBernsteinFunction_affine, TauCeti.isCompleteBernsteinFunction_const, TauCeti.isCompleteBernsteinFunction_id and TauCeti.isCompleteBernsteinFunction_div_add: the affine, constant, identity and point-mass witnesses.

References

• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications, 2nd ed., Theorems 6.2 and 7.3.

def TauCeti.RepresentsCompleteBernstein (μ : MeasureTheory.Measure NNReal) (a b : NNReal) (f : ℝ → ℝ) : Prop

A measure μ and coefficients a, b ≥ 0 represent a complete Bernstein function when μ satisfies the standard Stieltjes integrability condition and the function agrees on [0, ∞) with a + b t + ∫ x, t / (t + x) ∂μ. Requiring μ {0} = 0 stops an atom at zero from making the integral term jump between zero and the positive parameters.

Equations

• TauCeti.RepresentsCompleteBernstein μ a b f = (μ {0} = 0 ∧ MeasureTheory.Integrable TauCeti.stieltjesWeight μ ∧ Set.EqOn f (TauCeti.stieltjesBernsteinTransform μ a b) (Set.Ici 0))

theorem TauCeti.representsCompleteBernstein_iff {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} : RepresentsCompleteBernstein μ a b f ↔ μ {0} = 0 ∧ MeasureTheory.Integrable stieltjesWeight μ ∧ Set.EqOn f (stieltjesBernsteinTransform μ a b) (Set.Ici 0)

Characterization of complete-Bernstein representing data without unfolding the predicate.

theorem TauCeti.RepresentsCompleteBernstein.measure_singleton_zero {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsCompleteBernstein μ a b f) : μ {0} = 0

A complete-Bernstein representing measure has no atom at zero.

theorem TauCeti.RepresentsCompleteBernstein.integrable_weight {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsCompleteBernstein μ a b f) : MeasureTheory.Integrable stieltjesWeight μ

A complete-Bernstein representing measure satisfies the Stieltjes weight condition.

theorem TauCeti.RepresentsCompleteBernstein.eq_stieltjesBernsteinTransform {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsCompleteBernstein μ a b f) {t : ℝ} (ht : 0 ≤ t) : f t = stieltjesBernsteinTransform μ a b t

Evaluation of a complete-Bernstein representation at a nonnegative parameter.

theorem TauCeti.RepresentsCompleteBernstein.apply_zero {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsCompleteBernstein μ a b f) : f 0 = ↑a

A represented complete Bernstein function takes the value a at zero: the boundary value records the coefficient of the a / t term of the associated Stieltjes function.

theorem TauCeti.RepresentsCompleteBernstein.congr {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f g : ℝ → ℝ} (h : RepresentsCompleteBernstein μ a b f) (hgf : Set.EqOn g f (Set.Ici 0)) : RepresentsCompleteBernstein μ a b g

A complete-Bernstein representation depends only on the represented function's values on [0, ∞).

theorem TauCeti.RepresentsCompleteBernstein.representsStieltjes_div {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsCompleteBernstein μ a b f) : RepresentsStieltjes μ a b fun (t : ℝ) => f t / t

Dividing a complete Bernstein function by its parameter on (0, ∞) gives the Stieltjes function with the same representing data.

theorem TauCeti.RepresentsCompleteBernstein.add {μ ν : MeasureTheory.Measure NNReal} {a b c d : NNReal} {f g : ℝ → ℝ} (hf : RepresentsCompleteBernstein μ a b f) (hg : RepresentsCompleteBernstein ν c d g) : RepresentsCompleteBernstein (μ + ν) (a + c) (b + d) (f + g)

The sum of two complete-Bernstein representations is represented by the sum of their coefficients and measures.

theorem TauCeti.RepresentsCompleteBernstein.smul {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsCompleteBernstein μ a b f) {r : ℝ} (hr : 0 ≤ r) : RepresentsCompleteBernstein (ENNReal.ofReal r • μ) (r.toNNReal * a) (r.toNNReal * b) (r • f)

A nonnegative scalar multiple of a complete-Bernstein representation is represented by scaling its coefficients and measure.

theorem TauCeti.RepresentsCompleteBernstein.isBernsteinFunction {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsCompleteBernstein μ a b f) : IsBernsteinFunction f

A function with a complete-Bernstein representation is a Bernstein function.

def TauCeti.IsCompleteBernsteinFunction (f : ℝ → ℝ) : Prop

A real function is a complete Bernstein function if it has the standard Stieltjes-type representation on [0, ∞).

Equations

• TauCeti.IsCompleteBernsteinFunction f = ∃ (a : NNReal) (b : NNReal) (μ : MeasureTheory.Measure NNReal), TauCeti.RepresentsCompleteBernstein μ a b f

theorem TauCeti.isCompleteBernsteinFunction_iff {f : ℝ → ℝ} : IsCompleteBernsteinFunction f ↔ ∃ (a : NNReal) (b : NNReal) (μ : MeasureTheory.Measure NNReal), RepresentsCompleteBernstein μ a b f

Characterization of a complete Bernstein function by its representing data.

theorem TauCeti.IsCompleteBernsteinFunction.isBernsteinFunction {f : ℝ → ℝ} (hf : IsCompleteBernsteinFunction f) : IsBernsteinFunction f

Every complete Bernstein function is a Bernstein function.

theorem TauCeti.IsCompleteBernsteinFunction.congr {f g : ℝ → ℝ} (hf : IsCompleteBernsteinFunction f) (hgf : Set.EqOn g f (Set.Ici 0)) : IsCompleteBernsteinFunction g

The complete Bernstein property depends only on values on [0, ∞).

theorem TauCeti.IsCompleteBernsteinFunction.add {f g : ℝ → ℝ} (hf : IsCompleteBernsteinFunction f) (hg : IsCompleteBernsteinFunction g) : IsCompleteBernsteinFunction (f + g)

Complete Bernstein functions are closed under addition.

theorem TauCeti.IsCompleteBernsteinFunction.smul {f : ℝ → ℝ} (hf : IsCompleteBernsteinFunction f) {r : ℝ} (hr : 0 ≤ r) : IsCompleteBernsteinFunction (r • f)

Complete Bernstein functions are closed under multiplication by a nonnegative scalar.

theorem TauCeti.IsCompleteBernsteinFunction.isStieltjesFunction_div {f : ℝ → ℝ} (hf : IsCompleteBernsteinFunction f) : IsStieltjesFunction fun (t : ℝ) => f t / t

Dividing a complete Bernstein function by its parameter gives a Stieltjes function.

theorem TauCeti.representsCompleteBernstein_stieltjesBernsteinTransform {μ : MeasureTheory.Measure NNReal} {a b : NNReal} (hzero : μ {0} = 0) (hμ : MeasureTheory.Integrable stieltjesWeight μ) : RepresentsCompleteBernstein μ a b (stieltjesBernsteinTransform μ a b)

The Stieltjes--Bernstein transform of normalized, integrable measure data has a complete Bernstein representation with the given measure and coefficients.

theorem TauCeti.isCompleteBernsteinFunction_stieltjesBernsteinTransform {μ : MeasureTheory.Measure NNReal} {a b : NNReal} (hzero : μ {0} = 0) (hμ : MeasureTheory.Integrable stieltjesWeight μ) : IsCompleteBernsteinFunction (stieltjesBernsteinTransform μ a b)

The Stieltjes--Bernstein transform of normalized, integrable measure data is a complete Bernstein function.

theorem TauCeti.isStieltjesFunction_iff_exists_isCompleteBernsteinFunction_eqOn_mul {f : ℝ → ℝ} : IsStieltjesFunction f ↔ ∃ (g : ℝ → ℝ), IsCompleteBernsteinFunction g ∧ Set.EqOn g (fun (t : ℝ) => t * f t) (Set.Ioi 0)

Stieltjes--complete-Bernstein correspondence. A function f is Stieltjes exactly when its product t ↦ t * f t on (0, ∞) extends to a complete Bernstein function on [0, ∞). The extension's value at zero records the coefficient of the possible t⁻¹ singularity. Both sides are the same representing data μ, a, b, so the content is the change of normalization f ↦ t f(t) and the continuous extension of the product across zero.

theorem TauCeti.isCompleteBernsteinFunction_affine {c d : ℝ} (hc : 0 ≤ c) (hd : 0 ≤ d) : IsCompleteBernsteinFunction fun (t : ℝ) => c + d * t

Nonnegative affine functions are complete Bernstein functions.

theorem TauCeti.isCompleteBernsteinFunction_const {c : ℝ} (hc : 0 ≤ c) : IsCompleteBernsteinFunction fun (x : ℝ) => c

Nonnegative constant functions are complete Bernstein functions.

theorem TauCeti.isCompleteBernsteinFunction_id : IsCompleteBernsteinFunction fun (t : ℝ) => t

The identity function is a complete Bernstein function.

theorem TauCeti.isCompleteBernsteinFunction_div_add {x : ℝ} (hx : 0 < x) : IsCompleteBernsteinFunction fun (t : ℝ) => t / (t + x)

For x > 0, the basic function t ↦ t / (t + x) is complete Bernstein, represented by the unit point mass at x.