Stieltjes functions are completely monotone

A Stieltjes representation is a nonnegative combination of a reciprocal, a constant, and an integral of shifted reciprocals. This file proves that every such representation is completely monotone on (0, ∞). The open half-line is essential: the singular coefficient a / t, and more generally an infinite representing measure, need not admit a finite value or derivatives at the origin.

The proof differentiates the integral under the integral sign. Its n-th derivative has kernel (-1)ⁿ n! (t + x)⁻ⁿ⁻¹. On a neighborhood of a positive parameter, every such kernel is dominated by a constant multiple of the defining Stieltjes weight (1 + x)⁻¹; thus the sharp integrability hypothesis in RepresentsStieltjes suffices at every derivative order.

Main declarations

• TauCeti.integrable_zpow_neg_one_sub_add: all derivative-order Stieltjes kernels are integrable at positive parameters.
• TauCeti.iteratedDeriv_integral_inv_add: the derivative formula for the integral term.
• TauCeti.isCompletelyMonotoneOnIoi_integral_inv_add: a Stieltjes integral is completely monotone on (0, ∞).
• TauCeti.IsStieltjesFunction.isCompletelyMonotoneOnIoi: every Stieltjes function is completely monotone on (0, ∞).

References

• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications, 2nd ed., Theorem 2.2.
• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part B, the Stieltjes/Bernstein-function relationships target.

Integrability and domination of the derivative kernels

theorem TauCeti.integrable_zpow_neg_one_sub_add {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (n : ℕ) {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (fun (x : NNReal) => (t + ↑x) ^ (-1 - ↑n)) μ

Every integer-power kernel occurring in a derivative of a Stieltjes integral is integrable at a positive parameter.

theorem TauCeti.iteratedDeriv_integral_inv_add {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable stieltjesWeight μ) (n : ℕ) {t : ℝ} (ht : 0 < t) : iteratedDeriv n (fun (u : ℝ) => ∫ (x : NNReal), (u + ↑x)⁻¹ ∂μ) t = (-1) ^ n * ↑n.factorial * ∫ (x : NNReal), (t + ↑x) ^ (-1 - ↑n) ∂μ

The n-th derivative of a Stieltjes integral is the integral of (-1)ⁿ n! (t + x)⁻ⁿ⁻¹ at every positive parameter.

theorem TauCeti.isCompletelyMonotoneOnIoi_integral_inv_add {μ : MeasureTheory.Measure NNReal} (hμ : MeasureTheory.Integrable stieltjesWeight μ) : IsCompletelyMonotoneOnIoi fun (t : ℝ) => ∫ (x : NNReal), (t + ↑x)⁻¹ ∂μ

Integrating the shifted reciprocal kernels against a measure satisfying the Stieltjes weight condition gives a function completely monotone on (0, ∞).

theorem TauCeti.RepresentsStieltjes.isCompletelyMonotoneOnIoi {μ : MeasureTheory.Measure NNReal} {a b : NNReal} {f : ℝ → ℝ} (h : RepresentsStieltjes μ a b f) : IsCompletelyMonotoneOnIoi f

A function with a Stieltjes representation is completely monotone on (0, ∞).

theorem TauCeti.IsStieltjesFunction.isCompletelyMonotoneOnIoi {f : ℝ → ℝ} (hf : IsStieltjesFunction f) : IsCompletelyMonotoneOnIoi f

Every Stieltjes function is completely monotone on (0, ∞).