Reciprocal building blocks are completely monotone

This file adds a second family of concrete completely monotone functions to the OneParameterSemigroups roadmap, alongside the exponentials t ↦ e^{-x t} already in TauCeti.Analysis.CompletelyMonotone.Basic: the reciprocals of affine functions t ↦ (a + t)⁻¹ with a > 0.

These are the resolvent kernels t ↦ (λ + t)⁻¹ that Part A of the roadmap builds a semigroup theory around, and they are among the basic Stieltjes (resolvent) kernels appearing in Stieltjes representations. The acceptance example t ↦ 1/(1 + t) named in Part B of the roadmap is the special case a = 1; its representing measure e^{-x} dx is the exponential distribution.

Main declarations

• TauCeti.isCompletelyMonotone_inv_const_add: for a > 0, the reciprocal t ↦ (a + t)⁻¹ is completely monotone.
• TauCeti.isCompletelyMonotone_one_div_const_add: the t ↦ 1 / (a + t) phrasing of the same resolvent kernel.
• TauCeti.isCompletelyMonotone_one_div_one_add: the roadmap acceptance example t ↦ 1 / (1 + t).

References

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

theorem TauCeti.isCompletelyMonotone_inv_const_add {a : ℝ} (ha : 0 < a) : IsCompletelyMonotone fun (t : ℝ) => (a + t)⁻¹

For a > 0, the reciprocal t ↦ (a + t)⁻¹ is completely monotone. This is the resolvent kernel t ↦ (λ + t)⁻¹ of the roadmap's semigroup theory.

theorem TauCeti.isCompletelyMonotone_one_div_const_add {a : ℝ} (ha : 0 < a) : IsCompletelyMonotone fun (t : ℝ) => 1 / (a + t)

For a > 0, the reciprocal t ↦ 1 / (a + t) is completely monotone. This is the 1 / (a + t) phrasing of the resolvent kernel isCompletelyMonotone_inv_const_add.

theorem TauCeti.isCompletelyMonotone_one_div_one_add : IsCompletelyMonotone fun (t : ℝ) => 1 / (1 + t)

The roadmap acceptance example: t ↦ 1 / (1 + t) is completely monotone. Its representing measure under Bernstein's theorem is the exponential distribution e^{-x} dx.