Tail integrals of completely monotone functions

If f is completely monotone on (0, ∞) and its integral over one positive tail is finite, then t ↦ ∫ s in Ioi t, f s is completely monotone on (0, ∞). Its derivative is -f, so integration shifts the alternating derivative signs by one order. This gives an integral closure operation that complements the closure under negated derivatives.

Integrability over (0, ∞) further makes the tail integral continuous on [0, ∞), including when f itself has a singularity at the origin. The open-ray result only needs integrability of one positive tail, so it also applies to functions such as t ↦ t⁻².

Main declarations

• TauCeti.IsCompletelyMonotoneOnIoi.integral_Ioi: complete monotonicity of positive tail integrals.
• TauCeti.IsCompletelyMonotoneOnIoi.isContinuousCompletelyMonotoneOnIoi_integral_Ioi: integrability at the origin gives the closed-half-line continuity clause.

The derivatives are given by MeasureTheory.IntegrableOn.hasDerivAt_integral_Ioi and MeasureTheory.IntegrableOn.iteratedDeriv_integral_Ioi. Continuity at the origin comes from Mathlib's MeasureTheory.IntegrableOn.continuousOn_Ici_primitive_Ioi.

References

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

theorem TauCeti.IsCompletelyMonotoneOnIoi.integral_Ioi {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) (hint : ∃ a > 0, MeasureTheory.IntegrableOn f (Set.Ioi a) MeasureTheory.volume) : IsCompletelyMonotoneOnIoi fun (t : ℝ) => ∫ (s : ℝ) in Set.Ioi t, f s

Positive tail integration preserves complete monotonicity on (0, ∞) whenever one positive tail is integrable. Integrability or continuity at the origin is unnecessary.

theorem TauCeti.IsCompletelyMonotoneOnIoi.isContinuousCompletelyMonotoneOnIoi_integral_Ioi {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) (hint : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume) : IsContinuousCompletelyMonotoneOnIoi fun (t : ℝ) => ∫ (s : ℝ) in Set.Ioi t, f s

If a completely monotone function on (0, ∞) is integrable there, its tail integral is continuous on [0, ∞) and completely monotone on (0, ∞). The integrand need not be continuous or bounded at the origin.