Documentation

TauCeti.Analysis.CompletelyMonotone.Reparametrization

Complete monotonicity is closed under nonnegative affine reparametrization #

This file extends the closure API of TauCeti.IsCompletelyMonotone (sums, nonnegative scalar multiples, products and differentiation, in TauCeti.Analysis.CompletelyMonotone.Basic and TauCeti.Analysis.CompletelyMonotone.Closure) with closure under reparametrizing the argument by a nonnegative affine map t ↦ c · t + a (c, a ≥ 0), as called for by the OneParameterSemigroups roadmap's completely-monotone closure programme.

Both nonnegativity conditions are essential and are exactly what keeps the reparametrized argument inside [0, ∞), where the sign-alternation of f lives: scaling t ↦ c · t needs c ≥ 0 so that c · t ≥ 0, and it multiplies the n-th alternating derivative by the nonnegative factor cⁿ; shifting t ↦ t + a needs a ≥ 0 so that t + a ≥ 0, and it leaves the alternating derivative unchanged, only evaluated further to the right. A negative scaling c < 0 reflects the half-line and turns complete monotonicity into absolute monotonicity, so the sign condition genuinely fails; a negative shift a < 0 samples f to the left of 0, where nothing is assumed.

The scaling step is a direct consequence of Mathlib's iteratedDerivWithin_comp_const_smul; the shift step uses iteratedDerivWithin_comp_add_const, whose reparametrized set a +ᵥ [0, ∞) is [a, ∞), and there the alternating derivative of f agrees with its value within [0, ∞) because f is smooth across the interior of the half-line. Combining the two gives the general nonnegative affine reparametrization.

These closure lemmas manufacture new completely monotone functions from old: for instance t ↦ e^{-x (c t + a)} is completely monotone whenever x, c, a ≥ 0, and every resolvent kernel t ↦ (λ + t)⁻¹ reparametrized by a nonnegative affine map stays completely monotone.

Main declarations #

References #

source
theorem TauCeti.IsCompletelyMonotone.comp_const_mul {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) {c : ℝ} (hc : 0 ≤ c) :
IsCompletelyMonotone fun (t : ℝ) => f (c * t)

Completely monotone functions are closed under scaling the argument by a nonnegative constant: if f is completely monotone and 0 ≤ c, then t ↦ f (c · t) is completely monotone. The n-th alternating derivative is multiplied by the nonnegative factor cⁿ.

source
theorem TauCeti.IsCompletelyMonotone.comp_add_const {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) {a : ℝ} (ha : 0 ≤ a) :
IsCompletelyMonotone fun (t : ℝ) => f (t + a)

Completely monotone functions are closed under shifting the argument by a nonnegative constant: if f is completely monotone and 0 ≤ a, then t ↦ f (t + a) is completely monotone. The alternating derivative is unchanged, evaluated at the shifted point.

source
theorem TauCeti.IsCompletelyMonotone.iteratedDerivWithin_Ici_comp_add_const {f : ℝ → ℝ} (n : ℕ) (hs : ContDiffOn ℝ (↑n) f (Set.Ici 0)) {a t : ℝ} (ha : 0 ≤ a) (ht : 0 ≤ t) :
iteratedDerivWithin n (fun (s : ℝ) => f (s + a)) (Set.Ici 0) t = iteratedDerivWithin n f (Set.Ici 0) (t + a)

Iterated derivatives within [0, ∞) are compatible with a nonnegative shift of the argument.

source
theorem TauCeti.IsCompletelyMonotone.sub_comp_add_const {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) {a : ℝ} (ha : 0 ≤ a) :
IsCompletelyMonotone fun (t : ℝ) => f t - f (t + a)

The forward difference of a completely monotone function, with the sign reversed, is again completely monotone: every alternating derivative (-1)ⁿ f⁽ⁿ⁾ is itself completely monotone, hence nonincreasing, which is exactly the sign condition for t ↦ f t - f (t + a).

source
theorem TauCeti.IsCompletelyMonotone.comp_affine {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) {c a : ℝ} (hc : 0 ≤ c) (ha : 0 ≤ a) :
IsCompletelyMonotone fun (t : ℝ) => f (c * t + a)

Completely monotone functions are closed under nonnegative affine reparametrization of the argument: if f is completely monotone and 0 ≤ c, 0 ≤ a, then t ↦ f (c · t + a) is completely monotone.