A Bernstein function divided by its parameter is completely monotone

If f is a Bernstein function, then t ↦ f(t) / t is completely monotone on (0, ∞). This is one of the standard correspondences between Bernstein and completely monotone functions, next to t ↦ e^{-x f(t)} (TauCeti.IsBernsteinFunction.isContinuousCompletelyMonotoneOnIoi_exp_neg_mul) and the primitive of a completely monotone function (TauCeti.IsCompletelyMonotoneOnIoi.isBernsteinFunction_integral). For a complete Bernstein function the quotient is even a Stieltjes function (TauCeti.IsCompleteBernsteinFunction.isStieltjesFunction_div); for a general Bernstein function complete monotonicity is the most one can say.

For a Bernstein function with f(0) > 0, continuity at zero makes the quotient unbounded near the origin. Continuity of f at 0 is not needed for the general theorem, only its nonnegativity and differentiability on (0, ∞) and the complete monotonicity of f' there, so the theorem is stated under exactly those hypotheses and specialized to Bernstein functions afterwards.

The sign of dⁿ/dtⁿ (f(t) / t) is that of (-1)ⁿ T(0), where T is the Taylor polynomial of order n of f expanded at t (TauCeti.iteratedDeriv_div_id). Since (-1)ⁿ f⁽ⁿ⁺¹⁾ ≥ 0, the Taylor remainder has a sign on every [ε, t] with ε > 0, giving T(ε) ≥ f(ε) ≥ 0 (TauCeti.le_taylorWithinEval_of_neg_one_pow_mul_iteratedDerivWithin_nonneg), and T(0) ≥ 0 follows by letting ε → 0.

Main declarations

• TauCeti.isCompletelyMonotoneOnIoi_div_of_isCompletelyMonotoneOnIoi_deriv: if f is differentiable and nonnegative on (0, ∞) with completely monotone derivative there, then t ↦ f(t) / t is completely monotone on (0, ∞).
• TauCeti.IsBernsteinFunction.isCompletelyMonotoneOnIoi_div: a Bernstein function divided by its parameter is completely monotone on (0, ∞).

References

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

theorem TauCeti.isCompletelyMonotoneOnIoi_div_of_isCompletelyMonotoneOnIoi_deriv {f : ℝ → ℝ} (hf : DifferentiableOn ℝ f (Set.Ioi 0)) (hnonneg : ∀ (t : ℝ), 0 < t → 0 ≤ f t) (hf' : IsCompletelyMonotoneOnIoi (deriv f)) : IsCompletelyMonotoneOnIoi fun (t : ℝ) => f t / t

If f is differentiable and nonnegative on (0, ∞) and its derivative is completely monotone there, then t ↦ f(t) / t is completely monotone on (0, ∞).

theorem TauCeti.IsBernsteinFunction.isCompletelyMonotoneOnIoi_div {f : ℝ → ℝ} (hf : IsBernsteinFunction f) : IsCompletelyMonotoneOnIoi fun (t : ℝ) => f t / t

A Bernstein function divided by its parameter is completely monotone on (0, ∞).