Bernstein functions

A Bernstein function is a nonnegative continuous function f : ℝ → ℝ on the closed half-line [0, ∞), smooth on the open half-line (0, ∞), whose ordinary derivative is completely monotone on (0, ∞). Equivalently f ≥ 0 and f' alternates in sign through every order: 0 ≤ f', 0 ≥ f'', 0 ≤ f''', and so on. These are exactly the functions f for which t ↦ e^{-s f(t)} is completely monotone for every s ≥ 0; in probability they are the Laplace exponents of subordinators, and the completely-monotone ↔ Bernstein correspondence (a Bernstein function has completely monotone derivative, and a completely monotone function composed with a Bernstein function stays completely monotone) is the backbone of the Lévy–Khinchine theory.

The open-half-line smoothness clause is essential: an iterated derivative defaults to a junk value where the function fails to be differentiable, so without smoothness on (0, ∞) a badly behaved f could be declared "Bernstein" because its junk derivative 0 is (vacuously) completely monotone. Continuity at the boundary is kept separate, so the definition includes standard examples whose right derivative blows up at 0.

A Bernstein function is nondecreasing (its derivative is nonnegative) and concave (its derivative is nonincreasing) on [0, ∞); both are recorded below. The class is closed under sums and nonnegative scalar multiples, and the basic catalogue — constants, the identity, affine functions t ↦ c + d t with c, d ≥ 0, and the prototype t ↦ 1 - e^{-x t} — is built from these.

Main declarations

• TauCeti.IsBernsteinFunction: the predicate that f is continuous and nonnegative on [0, ∞), smooth on (0, ∞), and has completely monotone ordinary derivative on (0, ∞).
• TauCeti.IsBernsteinFunction.nonneg, TauCeti.IsBernsteinFunction.deriv_nonneg, TauCeti.IsBernsteinFunction.monotoneOn, TauCeti.IsBernsteinFunction.concaveOn: a Bernstein function is nonnegative, has nonnegative derivative, is nondecreasing, and is concave on [0, ∞).
• TauCeti.IsBernsteinFunction.congr: the property depends only on the values on [0, ∞).
• TauCeti.IsBernsteinFunction.add, TauCeti.IsBernsteinFunction.smul, TauCeti.IsBernsteinFunction.const_add, TauCeti.IsBernsteinFunction.sum: closure under sums, nonnegative scalar multiples, adding a nonnegative constant, and finite sums.
• TauCeti.isBernsteinFunction_const, TauCeti.isBernsteinFunction_id, TauCeti.isBernsteinFunction_affine, TauCeti.isBernsteinFunction_one_sub_exp_neg_mul: the basic examples.

References

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

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

A function f : ℝ → ℝ is a Bernstein function if it is continuous and nonnegative on [0, ∞), C^∞ on (0, ∞), and its ordinary derivative is completely monotone on (0, ∞). The open-half-line derivative condition is the standard one and permits boundary singularities such as the right derivative of sqrt at 0.

Equations

• TauCeti.IsBernsteinFunction f = (ContinuousOn f (Set.Ici 0) ∧ ContDiffOn ℝ (↑⊤) f (Set.Ioi 0) ∧ (∀ (t : ℝ), 0 ≤ t → 0 ≤ f t) ∧ TauCeti.IsCompletelyMonotoneOnIoi (deriv f))

theorem TauCeti.isBernsteinFunction_iff {f : ℝ → ℝ} : IsBernsteinFunction f ↔ ContinuousOn f (Set.Ici 0) ∧ ContDiffOn ℝ (↑⊤) f (Set.Ioi 0) ∧ (∀ (t : ℝ), 0 ≤ t → 0 ≤ f t) ∧ IsCompletelyMonotoneOnIoi (deriv f)

A function is Bernstein exactly when it is continuous and nonnegative on [0, ∞), smooth on (0, ∞), and has completely monotone derivative there. The body of IsBernsteinFunction is not @[expose]d, so this is how downstream files build the predicate from its four clauses.

theorem TauCeti.IsBernsteinFunction.continuousOn {f : ℝ → ℝ} (hf : IsBernsteinFunction f) : ContinuousOn f (Set.Ici 0)

A Bernstein function is continuous on [0, ∞).

theorem TauCeti.IsBernsteinFunction.contDiffOn {f : ℝ → ℝ} (hf : IsBernsteinFunction f) : ContDiffOn ℝ (↑⊤) f (Set.Ioi 0)

A Bernstein function is C^∞ on (0, ∞).

theorem TauCeti.IsBernsteinFunction.nonneg {f : ℝ → ℝ} (hf : IsBernsteinFunction f) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ f t

A Bernstein function is nonnegative on [0, ∞).

theorem TauCeti.IsBernsteinFunction.deriv_isCompletelyMonotoneOnIoi {f : ℝ → ℝ} (hf : IsBernsteinFunction f) : IsCompletelyMonotoneOnIoi (deriv f)

The ordinary derivative of a Bernstein function is completely monotone on (0, ∞).

theorem TauCeti.IsBernsteinFunction.differentiableOn {f : ℝ → ℝ} (hf : IsBernsteinFunction f) : DifferentiableOn ℝ f (Set.Ioi 0)

A Bernstein function is differentiable on (0, ∞).

theorem TauCeti.IsBernsteinFunction.deriv_nonneg {f : ℝ → ℝ} (hf : IsBernsteinFunction f) {t : ℝ} (ht : 0 < t) : 0 ≤ deriv f t

The derivative of a Bernstein function is nonnegative on (0, ∞): a Bernstein function is nondecreasing.

theorem TauCeti.IsBernsteinFunction.monotoneOn {f : ℝ → ℝ} (hf : IsBernsteinFunction f) : MonotoneOn f (Set.Ici 0)

A Bernstein function is nondecreasing on [0, ∞).

theorem TauCeti.IsBernsteinFunction.concaveOn {f : ℝ → ℝ} (hf : IsBernsteinFunction f) : ConcaveOn ℝ (Set.Ici 0) f

A Bernstein function is concave on [0, ∞): its derivative is nonincreasing.

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

Being a Bernstein function depends only on the values on [0, ∞).

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

Bernstein functions are closed under addition.

theorem TauCeti.IsBernsteinFunction.smul {f : ℝ → ℝ} (hf : IsBernsteinFunction f) {c : ℝ} (hc : 0 ≤ c) : IsBernsteinFunction (c • f)

Bernstein functions are closed under multiplication by a nonnegative constant.

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

A nonnegative constant function is a Bernstein function.

theorem TauCeti.isBernsteinFunction_zero : IsBernsteinFunction fun (x : ℝ) => 0

The zero function is a Bernstein function.

theorem TauCeti.IsBernsteinFunction.const_add {f : ℝ → ℝ} (hf : IsBernsteinFunction f) {c : ℝ} (hc : 0 ≤ c) : IsBernsteinFunction fun (t : ℝ) => c + f t

Adding a nonnegative constant to a Bernstein function again gives a Bernstein function.

theorem TauCeti.IsBernsteinFunction.sum {ι : Type u_1} {s : Finset ι} {f : ι → ℝ → ℝ} (hf : ∀ i ∈ s, IsBernsteinFunction (f i)) : IsBernsteinFunction fun (t : ℝ) => ∑ i ∈ s, f i t

Bernstein functions are closed under finite sums.

theorem TauCeti.isBernsteinFunction_id : IsBernsteinFunction fun (t : ℝ) => t

The identity function is a Bernstein function: it is nonnegative on [0, ∞) with constant derivative 1.

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

An affine function t ↦ c + d t with nonnegative coefficients is a Bernstein function.

theorem TauCeti.isBernsteinFunction_one_sub_exp_neg_mul {x : ℝ} (hx : 0 ≤ x) : IsBernsteinFunction fun (t : ℝ) => 1 - Real.exp (-x * t)

The prototype Bernstein function t ↦ 1 - e^{-x t} for x ≥ 0: it is nonnegative on [0, ∞) and its derivative t ↦ x e^{-x t} is completely monotone.