Closure of completely monotone functions under products and differentiation

This file extends the basic API of TauCeti.IsCompletelyMonotone (sums and nonnegative scalar multiples, in TauCeti.Analysis.CompletelyMonotone.Basic) with two further closure properties called for by the OneParameterSemigroups roadmap:

• the product of two completely monotone functions is completely monotone, hence so is any finite product and any natural power;
• if f is completely monotone then so is t ↦ -f'(t), the negated derivative.

Both are elementary consequences of the sign-alternation definition. For the product, the Leibniz rule expands (-1)ⁿ (fg)⁽ⁿ⁾ as a nonnegative combination ∑ₖ (n choose k) · [(-1)ᵏ f⁽ᵏ⁾] · [(-1)ⁿ⁻ᵏ g⁽ⁿ⁻ᵏ⁾] of products of the (nonnegative) alternating derivatives of f and g. For the negated derivative, the (n+1)-st alternating derivative of f is the n-th alternating derivative of -f'. Mathlib has the analogous closure lemmas for AbsolutelyMonotoneOn only up to sums and scalar multiples (AbsolutelyMonotoneOn.add, AbsolutelyMonotoneOn.smul), so the multiplicative and differential closure built here is new.

These workhorses combine with the prototypes t ↦ e^{-x t} to manufacture completely monotone functions: e.g. any finite sum ∑ⱼ cⱼ e^{-xⱼ t} with cⱼ, xⱼ ≥ 0, or a product like t ↦ e^{-x t} / (1 + t)-style mixtures once their factors are known completely monotone. The negated-derivative closure is the first step towards the completely-monotone ↔ Bernstein-function correspondence (a Bernstein function is a nonnegative function whose derivative is completely monotone).

Main declarations

• TauCeti.IsCompletelyMonotone.mul: completely monotone functions are closed under pointwise multiplication.
• TauCeti.IsCompletelyMonotone.prod: closure under finite products.
• TauCeti.IsCompletelyMonotone.pow: closure under natural powers.
• TauCeti.IsCompletelyMonotone.neg_one_pow_mul_iteratedDerivWithin: every alternating iterated derivative of a completely monotone function is completely monotone.
• TauCeti.IsCompletelyMonotone.neg_derivWithin: the negated derivative within [0, ∞) of a completely monotone function is completely monotone.

References

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

theorem TauCeti.IsCompletelyMonotone.mul {f g : ℝ → ℝ} (hf : IsCompletelyMonotone f) (hg : IsCompletelyMonotone g) : IsCompletelyMonotone (f * g)

Completely monotone functions are closed under pointwise multiplication.

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

Completely monotone functions are closed under finite products.

theorem TauCeti.IsCompletelyMonotone.pow {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) (k : ℕ) : IsCompletelyMonotone (f ^ k)

Completely monotone functions are closed under taking natural powers.

theorem TauCeti.IsCompletelyMonotone.neg_one_pow_mul_iteratedDerivWithin {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) (k : ℕ) : IsCompletelyMonotone fun (t : ℝ) => (-1) ^ k * iteratedDerivWithin k f (Set.Ici 0) t

Every alternating iterated derivative of a completely monotone function is completely monotone.

theorem TauCeti.IsCompletelyMonotone.neg_derivWithin {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) : IsCompletelyMonotone fun (t : ℝ) => -derivWithin f (Set.Ici 0) t

The negated derivative within [0, ∞) of a completely monotone function is completely monotone.