Primitives of completely monotone functions are Bernstein functions

This file establishes one direction of the standard correspondence between completely monotone and Bernstein functions. If f is completely monotone on (0, ∞) and continuous on [0, ∞), then

t ↦ ∫ x in 0..t, f x for t ≥ 0

is a Bernstein function. Its derivative on (0, ∞) is f, so complete monotonicity of the derivative is inherited directly from f.

The primitive is packaged as TauCeti.halfLinePrimitive (in TauCeti.Analysis.Calculus.HalfLinePrimitive), which integrates f (max x 0) so that the function is defined on all of ℝ; on [0, ∞) this agrees with ∫₀ᵗ f by TauCeti.halfLinePrimitive_eq_integral_of_nonneg.

Main declarations

• TauCeti.IsCompletelyMonotoneOnIoi.isBernsteinFunction_halfLinePrimitive: the primitive of a function that is completely monotone on (0, ∞) and continuous on [0, ∞) is Bernstein.
• TauCeti.IsCompletelyMonotoneOnIoi.isBernsteinFunction_integral: the same statement written directly in terms of ∫ x in 0..t, f x.
• TauCeti.IsCompletelyMonotone.isBernsteinFunction_halfLinePrimitive, TauCeti.IsCompletelyMonotone.isBernsteinFunction_integral: the corresponding statements for the closed-half-line predicate IsCompletelyMonotone.

References

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

theorem TauCeti.IsCompletelyMonotoneOnIoi.isBernsteinFunction_halfLinePrimitive {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) (hcont : ContinuousOn f (Set.Ici 0)) : IsBernsteinFunction (halfLinePrimitive f)

The primitive on [0, ∞) of a function that is completely monotone on (0, ∞) and continuous on [0, ∞) is a Bernstein function.

theorem TauCeti.IsCompletelyMonotoneOnIoi.isBernsteinFunction_integral {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) (hcont : ContinuousOn f (Set.Ici 0)) : IsBernsteinFunction fun (t : ℝ) => ∫ (x : ℝ) in 0..t, f x

The primitive t ↦ ∫₀ᵗ f of a function that is completely monotone on (0, ∞) and continuous on [0, ∞) is a Bernstein function.

theorem TauCeti.IsCompletelyMonotone.isBernsteinFunction_halfLinePrimitive {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) : IsBernsteinFunction (halfLinePrimitive f)

The primitive on [0, ∞) of a completely monotone function is a Bernstein function.

theorem TauCeti.IsCompletelyMonotone.isBernsteinFunction_integral {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) : IsBernsteinFunction fun (t : ℝ) => ∫ (x : ℝ) in 0..t, f x

The primitive t ↦ ∫₀ᵗ f of a completely monotone function is a Bernstein function.