Half-line closure for completely monotone functions

This file extends the API for TauCeti.IsCompletelyMonotoneOnIoi, the ordinary-derivative version of complete monotonicity on (0, ∞), with the multiplicative and differential closure properties needed by the Bernstein-function part of the one-parameter-semigroups roadmap, and derives the corresponding multiplicative closure for the closed-half-line predicate TauCeti.IsContinuousCompletelyMonotoneOnIoi.

The closed-half-line predicate TauCeti.IsCompletelyMonotone already has product and negated-derivative closure in TauCeti.Analysis.CompletelyMonotone.Closure. The open version is not just a corollary of that file: Bernstein functions are allowed to have a singular right derivative at 0, so their derivative is naturally completely monotone only on (0, ∞).

Main declarations

• TauCeti.IsCompletelyMonotoneOnIoi.mul: closure under pointwise multiplication.
• TauCeti.IsCompletelyMonotoneOnIoi.prod: closure under finite products.
• TauCeti.IsCompletelyMonotoneOnIoi.pow: closure under natural powers.
• TauCeti.IsCompletelyMonotoneOnIoi.neg_one_pow_mul_iteratedDeriv: every alternating ordinary iterated derivative of a completely monotone function on (0, ∞) is again completely monotone there.
• TauCeti.IsCompletelyMonotoneOnIoi.neg_deriv: the negated ordinary derivative of a completely monotone function on (0, ∞) is completely monotone there.
• TauCeti.IsContinuousCompletelyMonotoneOnIoi.mul, TauCeti.IsContinuousCompletelyMonotoneOnIoi.prod, TauCeti.IsContinuousCompletelyMonotoneOnIoi.pow: the closed-half-line predicate is closed under pointwise multiplication, finite products, and natural powers.

References

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

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

Completely monotone functions on (0, ∞) are closed under pointwise multiplication.

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

Completely monotone functions on (0, ∞) are closed under finite products.

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

Completely monotone functions on (0, ∞) are closed under taking natural powers.

theorem TauCeti.IsCompletelyMonotoneOnIoi.neg_one_pow_mul_iteratedDeriv {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) (k : ℕ) : IsCompletelyMonotoneOnIoi fun (t : ℝ) => (-1) ^ k * iteratedDeriv k f t

Every alternating ordinary iterated derivative of a completely monotone function on (0, ∞) is completely monotone there.

theorem TauCeti.IsCompletelyMonotoneOnIoi.neg_deriv {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) : IsCompletelyMonotoneOnIoi fun (t : ℝ) => -deriv f t

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

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

Closed-half-line complete monotonicity is closed under pointwise multiplication.

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

Closed-half-line complete monotonicity is closed under finite products.

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

Closed-half-line complete monotonicity is closed under natural powers.