Fractional powers are Bernstein functions

The power t ↦ t^s with 0 ≤ s ≤ 1 is a Bernstein function: it is nonnegative and continuous on [0, ∞), smooth on (0, ∞), and its derivative t ↦ s · t^{s-1} is the completely monotone negative power of TauCeti.isCompletelyMonotoneOnIoi_rpow_neg, since s - 1 = -(1 - s) with 1 - s ≥ 0.

Feeding this into TauCeti.IsContinuousCompletelyMonotoneOnIoi.comp_isBernsteinFunction produces the stretched exponentials t ↦ e^{-x t^s}. These are the acceptance example the OneParameterSemigroups roadmap asks the composition closure to deliver. The endpoint s = 1 recovers the exponential t ↦ e^{-x t} and s = 0 the constant t ↦ e^{-x}.

Main declarations

• TauCeti.isBernsteinFunction_rpow: t ↦ t^s is a Bernstein function for 0 ≤ s ≤ 1.
• TauCeti.isContinuousCompletelyMonotoneOnIoi_exp_neg_mul_rpow: the stretched exponential t ↦ e^{-x t^s} is completely monotone.

References

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

theorem TauCeti.isBernsteinFunction_rpow {s : ℝ} (hs : 0 ≤ s) (hs₁ : s ≤ 1) : IsBernsteinFunction fun (t : ℝ) => t ^ s

For 0 ≤ s ≤ 1 the power t ↦ t^s is a Bernstein function: its derivative is the completely monotone negative power t ↦ s · t^{-(1-s)}.

theorem TauCeti.isContinuousCompletelyMonotoneOnIoi_exp_neg_mul_rpow {x s : ℝ} (hx : 0 ≤ x) (hs : 0 ≤ s) (hs₁ : s ≤ 1) : IsContinuousCompletelyMonotoneOnIoi fun (t : ℝ) => Real.exp (-x * t ^ s)

The stretched exponential t ↦ e^{-x t^s} is completely monotone on [0, ∞) for x ≥ 0 and 0 ≤ s ≤ 1: it is the composition of the completely monotone t ↦ e^{-x t} with the Bernstein function t ↦ t^s.