Documentation

TauCeti.Analysis.CompletelyMonotone.Composition

Composing completely monotone and Bernstein functions #

This file proves the composition closure property called for by the OneParameterSemigroups roadmap, Part B: if g is completely monotone and f is a Bernstein function, then g ∘ f is again completely monotone. Two companions come out of the same argument: Bernstein functions are closed under composition, and the prototype t ↦ e^{-x f(t)} is completely monotone for every x ≥ 0 and every Bernstein f.

The induction #

Writing F = g ∘ f, the chain and product rules give F' = -\,[(-g') ∘ f] \cdot f', in which both -g' and f' are completely monotone. Iterating this substitution never returns to a composition alone, but always to a product of a composition with a completely monotone factor. The workhorse TauCeti.IsCompletelyMonotoneOnIoi.comp_isBernsteinFunction_mul therefore carries that product along: for completely monotone g and h, t ↦ g (f t) · h t is completely monotone, that is, 0 ≤ (-1)ⁿ dⁿ/dtⁿ [g(f t) · h t] on (0, ∞), proved by induction on n from the identity

d/dt [g(f t) · h t] = -\,[(-g')(f t) · (f' t · h t)] - [g(f t) · (-h' t)],

whose two bracketed terms are again of the same shape, with (-g', f' · h) and (g, -h') in place of (g, h). Taking h = 1 gives the composition theorem.

The argument runs on the open half-line, where a Bernstein function is smooth and where its values are positive, so that the derivatives of g at f t are honest two-sided derivatives. That positivity is not automatic — a Bernstein function may vanish — but the failure is total: TauCeti.IsBernsteinFunction.eq_zero_of_eq_zero shows that a Bernstein function vanishing at one positive point vanishes on all of [0, ∞), because it is nonnegative, nondecreasing and concave. In that degenerate case the composition is the constant g 0, and the theorems are immediate.

Main declarations #

References #

Bernstein functions with a zero #

source
theorem TauCeti.IsBernsteinFunction.eq_zero_of_eq_zero {f : ℝ → ℝ} (hf : IsBernsteinFunction f) {t₀ : ℝ} (ht₀ : 0 < t₀) (h₀ : f t₀ = 0) {t : ℝ} (ht : 0 ≤ t) :
f t = 0

A Bernstein function that vanishes at one positive point vanishes on the whole closed half-line. Monotonicity pushes the value at the origin down to 0, and concavity then traps the graph between the chord through the two zeros and the horizontal axis.

source
theorem TauCeti.IsBernsteinFunction.pos_of_forall_ne_zero {f : ℝ → ℝ} (hf : IsBernsteinFunction f) (hne : ¬∃ (t₀ : ℝ), 0 < t₀ ∧ f t₀ = 0) {t : ℝ} (ht : 0 < t) :
0 < f t

A Bernstein function with no zero on the open half-line is positive there: this is the dichotomy that lets the composition theorems split into a degenerate constant case and the main case, where the inner function stays inside (0, ∞).

The composition induction #

Composition theorems #

source
theorem TauCeti.IsCompletelyMonotoneOnIoi.comp_isBernsteinFunction_mul {f g h : ℝ → ℝ} (hg : IsCompletelyMonotoneOnIoi g) (hh : IsCompletelyMonotoneOnIoi h) (hf : IsBernsteinFunction f) (hpos : ∀ (t : ℝ), 0 < t → 0 < f t) :
IsCompletelyMonotoneOnIoi fun (u : ℝ) => g (f u) * h u

The product form of the open-half-line composition theorem. For completely monotone g and h and a Bernstein function f that is positive on (0, ∞), the product t ↦ g (f t) · h t is completely monotone on (0, ∞).

The extra factor h is what makes the induction close: differentiating once turns the pair (g, h) into the two pairs (-g', f' · h) and (g, -h'), both again completely monotone.

source
theorem TauCeti.IsCompletelyMonotoneOnIoi.comp_isBernsteinFunction {f g : ℝ → ℝ} (hg : IsCompletelyMonotoneOnIoi g) (hf : IsBernsteinFunction f) (hpos : ∀ (t : ℝ), 0 < t → 0 < f t) :
IsCompletelyMonotoneOnIoi (g ∘ f)

Composition on the open half-line. If g is completely monotone on (0, ∞) and f is a Bernstein function that is positive on (0, ∞), then g ∘ f is completely monotone on (0, ∞). The positivity hypothesis is what keeps f t inside the open half-line, where g is smooth; it is removed in TauCeti.IsContinuousCompletelyMonotoneOnIoi.comp_isBernsteinFunction.

source
theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.comp_isBernsteinFunction {f g : ℝ → ℝ} (hg : IsContinuousCompletelyMonotoneOnIoi g) (hf : IsBernsteinFunction f) :
IsContinuousCompletelyMonotoneOnIoi (g ∘ f)

A completely monotone function composed with a Bernstein function is completely monotone. This is the closure property the OneParameterSemigroups roadmap asks for in Part B.

The conclusion is the closed-half-line predicate IsContinuousCompletelyMonotoneOnIoi, not the stronger IsCompletelyMonotone: a Bernstein function such as t ↦ √t has no finite right derivative at the origin, so the composition need not have one.

source
theorem TauCeti.IsBernsteinFunction.comp {f g : ℝ → ℝ} (hg : IsBernsteinFunction g) (hf : IsBernsteinFunction f) :
IsBernsteinFunction (g ∘ f)

Bernstein functions are closed under composition. The derivative of g ∘ f is (g' ∘ f) · f', a product of the composition theorem's output with a completely monotone factor.

source
theorem TauCeti.IsBernsteinFunction.isContinuousCompletelyMonotoneOnIoi_exp_neg_mul {f : ℝ → ℝ} (hf : IsBernsteinFunction f) {x : ℝ} (hx : 0 ≤ x) :
IsContinuousCompletelyMonotoneOnIoi fun (t : ℝ) => Real.exp (-x * f t)

The prototype completely monotone functions attached to a Bernstein function: for x ≥ 0, the composition t ↦ e^{-x f(t)} is completely monotone on the closed half-line. These are the Laplace transforms of the one-parameter convolution semigroup subordinate to f.