Completely monotone functions

A function f : ℝ → ℝ is completely monotone on a set if its reflection u ↦ f (-u) is absolutely monotone on the reflected set. Mathlib formulates absolute monotonicity through a Taylor-series witness, so this remains meaningful on sets that are not uniquely differentiable. On a UniqueDiffOn set it is equivalent to smoothness together with alternating signs for the iterated derivatives within the set. The principal specialization in this development uses the closed half-line [0, ∞): (-1)ⁿ f⁽ⁿ⁾(t) ≥ 0 for every n and every t ≥ 0. Equivalently f is nonnegative, nonincreasing, convex, and so on through every order. Bernstein's theorem identifies the completely monotone functions on the open half-line (0, ∞) with the Laplace transforms of positive measures on [0, ∞). Demanding smoothness up to the boundary point 0, as we do here, is a genuine strengthening: it carves out the subclass whose representing measure has every moment finite. (It thereby excludes some Laplace transforms of finite measures, such as t ↦ ∫₀^∞ e^{-x t} (1 + x)⁻² dx, which is finite at 0 yet has f'(0⁺) = -∞.) The prototypes t ↦ e^{-x t} (x ≥ 0) are the extreme rays out of which Bernstein's theorem builds the general member.

The smoothness clause is essential and is not folded into the sign condition: an iterated derivative defaults to a junk value where the function fails to be differentiable, so without it a badly behaved f could satisfy 0 ≤ 0 vacuously. We phrase the sign condition through iteratedDerivWithin _ (Set.Ici 0), the derivative within the closed half-line, which is the object that pairs cleanly with ContDiffOn (in particular at the boundary point 0); on the open half-line it agrees with the ordinary iterated derivative.

Main declarations

• TauCeti.CompletelyMonotoneOn: complete monotonicity on an arbitrary set, defined by reflecting Mathlib's AbsolutelyMonotoneOn predicate.
• TauCeti.CompletelyMonotoneOn.iff_neg_one_pow_mul_iteratedDerivWithin_nonneg: on a UniqueDiffOn set, equivalence with smoothness and alternating signs.
• TauCeti.CompletelyMonotoneOn.of_contDiff: a globally smooth function whose ordinary iterated derivatives have alternating signs on a set is completely monotone there.
• TauCeti.CompletelyMonotoneOn.add, TauCeti.CompletelyMonotoneOn.smul: closure under addition and nonnegative scalar multiplication.
• TauCeti.IsCompletelyMonotone: the predicate that f is smooth and sign-alternating on [0, ∞).
• TauCeti.isCompletelyMonotone_iff_completelyMonotoneOn: IsCompletelyMonotone is the Ici 0 specialization of CompletelyMonotoneOn.
• TauCeti.IsCompletelyMonotone.congr: complete monotonicity only depends on the values of the function on [0, ∞).
• TauCeti.IsCompletelyMonotone.nonneg, TauCeti.IsCompletelyMonotone.derivWithin_nonpos, TauCeti.IsCompletelyMonotone.antitoneOn: a completely monotone function is nonnegative and nonincreasing on [0, ∞).
• TauCeti.IsContinuousCompletelyMonotoneOnIoi.exists_nonneg_tendsto_atTop, TauCeti.IsContinuousCompletelyMonotoneOnIoi.le_of_tendsto_atTop: order-limit consequences of nonnegativity and monotonicity on [0, ∞).
• TauCeti.IsCompletelyMonotone.neg_one_pow_mul_iteratedDeriv_nonneg: on the open half-line, the sign condition also holds for ordinary iterated derivatives.
• TauCeti.IsCompletelyMonotone.add, TauCeti.IsCompletelyMonotone.sum, TauCeti.IsCompletelyMonotone.smul: closure under addition, finite sums, and nonnegative scalar multiples.
• TauCeti.IsCompletelyMonotoneOnIoi: the open-half-line analogue, using ordinary iterated derivatives on (0, ∞).
• TauCeti.IsCompletelyMonotoneOnIoi.convexOn: a completely monotone function on (0, ∞) is convex there.
• TauCeti.isCompletelyMonotoneOnIoi_of_forall_comp_add_const: complete monotonicity on (0, ∞) can be checked on the positive translates of a function, the converse of TauCeti.IsCompletelyMonotoneOnIoi.isCompletelyMonotone_comp_add_const.
• TauCeti.IsContinuousCompletelyMonotoneOnIoi: the closed-half-line predicate used by the finite-measure Hausdorff--Bernstein--Widder theorem: continuity on [0, ∞) plus complete monotonicity on (0, ∞).
• TauCeti.isCompletelyMonotone_const: a nonnegative constant is completely monotone.
• TauCeti.isCompletelyMonotone_exp_neg_mul: the building block t ↦ e^{-x t} for x ≥ 0.

References

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

def TauCeti.CompletelyMonotoneOn (f : ℝ → ℝ) (s : Set ℝ) : Prop

A function f : ℝ → ℝ is completely monotone on a set s if its reflection u ↦ f (-u) is absolutely monotone on the reflected set -s. Mathlib's AbsolutelyMonotoneOn uses a Taylor-series witness, so this definition remains meaningful even when s is not uniquely differentiable. Under UniqueDiffOn ℝ s, it is equivalent to smoothness on s together with the alternating-sign condition on iteratedDerivWithin; see CompletelyMonotoneOn.iff_neg_one_pow_mul_iteratedDerivWithin_nonneg.

Equations

• TauCeti.CompletelyMonotoneOn f s = AbsolutelyMonotoneOn (fun (u : ℝ) => f (-u)) (-s)

theorem TauCeti.completelyMonotoneOn_iff_absolutelyMonotoneOn_comp_neg {f : ℝ → ℝ} {s : Set ℝ} : CompletelyMonotoneOn f s ↔ AbsolutelyMonotoneOn (fun (u : ℝ) => f (-u)) (-s)

Complete monotonicity on s unfolds to absolute monotonicity of the reflected function on the reflected set.

theorem TauCeti.CompletelyMonotoneOn.contDiffOn {f : ℝ → ℝ} {s : Set ℝ} (hf : CompletelyMonotoneOn f s) : ContDiffOn ℝ (↑⊤) f s

A completely monotone function on s is smooth on s.

theorem TauCeti.CompletelyMonotoneOn.of_contDiff {f : ℝ → ℝ} {s : Set ℝ} (hf : ContDiff ℝ (↑⊤) f) (h : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ (-1) ^ n * iteratedDeriv n f x) : CompletelyMonotoneOn f s

A globally C^∞ function whose iterated derivatives have alternating signs on s is completely monotone on s. The set s need not satisfy UniqueDiffOn.

theorem TauCeti.CompletelyMonotoneOn.neg_one_pow_mul_iteratedDerivWithin_nonneg {f : ℝ → ℝ} {s : Set ℝ} (hf : CompletelyMonotoneOn f s) (hs : UniqueDiffOn ℝ s) (n : ℕ) {x : ℝ} (hx : x ∈ s) : 0 ≤ (-1) ^ n * iteratedDerivWithin n f s x

On a uniquely differentiable set, the iterated derivatives of a completely monotone function have the expected alternating signs.

theorem TauCeti.CompletelyMonotoneOn.iff_neg_one_pow_mul_iteratedDerivWithin_nonneg {f : ℝ → ℝ} {s : Set ℝ} (hs : UniqueDiffOn ℝ s) : CompletelyMonotoneOn f s ↔ ContDiffOn ℝ (↑⊤) f s ∧ ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ (-1) ^ n * iteratedDerivWithin n f s x

On a uniquely differentiable set, complete monotonicity is equivalent to smoothness together with the usual alternating-sign condition on iterated derivatives within the set.

Closure properties

theorem TauCeti.CompletelyMonotoneOn.add {f : ℝ → ℝ} {s : Set ℝ} {g : ℝ → ℝ} (hf : CompletelyMonotoneOn f s) (hg : CompletelyMonotoneOn g s) : CompletelyMonotoneOn (f + g) s

The sum of two completely monotone functions is completely monotone.

theorem TauCeti.CompletelyMonotoneOn.smul {f : ℝ → ℝ} {s : Set ℝ} {c : ℝ} (hf : CompletelyMonotoneOn f s) (hc : 0 ≤ c) : CompletelyMonotoneOn (c • f) s

A nonnegative scalar multiple of a completely monotone function is completely monotone.

def TauCeti.IsCompletelyMonotone (f : ℝ → ℝ) : Prop

A function f : ℝ → ℝ is completely monotone if it is C^∞ on the closed half-line [0, ∞) and its iterated derivatives within [0, ∞) alternate in sign: 0 ≤ (-1)ⁿ f⁽ⁿ⁾(t) for every n and every t ≥ 0. The smoothness clause prevents the sign condition from being satisfied vacuously by a junk iterated derivative.

Equations

• TauCeti.IsCompletelyMonotone f = (ContDiffOn ℝ (↑⊤) f (Set.Ici 0) ∧ ∀ (n : ℕ) (t : ℝ), 0 ≤ t → 0 ≤ (-1) ^ n * iteratedDerivWithin n f (Set.Ici 0) t)

theorem TauCeti.isCompletelyMonotone_iff {f : ℝ → ℝ} : IsCompletelyMonotone f ↔ ContDiffOn ℝ (↑⊤) f (Set.Ici 0) ∧ ∀ (n : ℕ) (t : ℝ), 0 ≤ t → 0 ≤ (-1) ^ n * iteratedDerivWithin n f (Set.Ici 0) t

IsCompletelyMonotone f unfolds to its defining conjunction: f is C^∞ on [0, ∞) and its iterated derivatives within [0, ∞) alternate in sign.

theorem TauCeti.isCompletelyMonotone_iff_completelyMonotoneOn {f : ℝ → ℝ} : IsCompletelyMonotone f ↔ CompletelyMonotoneOn f (Set.Ici 0)

The closed-half-line predicate is the specialization of complete monotonicity on a set.

theorem TauCeti.IsCompletelyMonotone.contDiffOn {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) : ContDiffOn ℝ (↑⊤) f (Set.Ici 0)

A completely monotone function is C^∞ on [0, ∞).

theorem TauCeti.IsCompletelyMonotone.neg_one_pow_mul_iteratedDerivWithin_nonneg {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) (n : ℕ) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ (-1) ^ n * iteratedDerivWithin n f (Set.Ici 0) t

The sign-alternation property of the iterated derivatives of a completely monotone function: 0 ≤ (-1)ⁿ f⁽ⁿ⁾(t) for every n and every t ≥ 0.

theorem TauCeti.IsCompletelyMonotone.neg_one_pow_mul_iteratedDeriv_nonneg {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) (n : ℕ) {t : ℝ} (ht : 0 < t) : 0 ≤ (-1) ^ n * iteratedDeriv n f t

On the open half-line, the completely monotone sign condition can be read using ordinary iterated derivatives instead of derivatives within [0, ∞).

theorem TauCeti.IsCompletelyMonotone.nonneg {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ f t

A completely monotone function is nonnegative on [0, ∞).

theorem TauCeti.IsCompletelyMonotone.derivWithin_nonpos {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) {t : ℝ} (ht : 0 ≤ t) : derivWithin f (Set.Ici 0) t ≤ 0

The derivative within [0, ∞) of a completely monotone function is nonpositive: it is nonincreasing.

theorem TauCeti.IsCompletelyMonotone.congr {f g : ℝ → ℝ} (hf : IsCompletelyMonotone f) (h : Set.EqOn g f (Set.Ici 0)) : IsCompletelyMonotone g

Complete monotonicity is determined by the values of the function on [0, ∞): if g agrees with a completely monotone f throughout [0, ∞), then g is completely monotone too. Both the smoothness clause and the sign condition only see the function within [0, ∞).

theorem TauCeti.IsCompletelyMonotone.hasDerivAt_iteratedDerivWithin_succ {f : ℝ → ℝ} (hcm : IsCompletelyMonotone f) (k : ℕ) {t : ℝ} (ht : 0 < t) : HasDerivAt (iteratedDerivWithin k f (Set.Ici 0)) (iteratedDerivWithin (k + 1) f (Set.Ici 0) t) t

For a completely monotone f, the k-th iterated derivative within [0, ∞) is differentiable at any t > 0, with derivative the (k+1)-th iterated derivative.

theorem TauCeti.IsCompletelyMonotone.add {f g : ℝ → ℝ} (hf : IsCompletelyMonotone f) (hg : IsCompletelyMonotone g) : IsCompletelyMonotone (f + g)

Completely monotone functions are closed under addition.

theorem TauCeti.IsCompletelyMonotone.smul {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) {c : ℝ} (hc : 0 ≤ c) : IsCompletelyMonotone (c • f)

Completely monotone functions are closed under multiplication by a nonnegative constant.

theorem TauCeti.isCompletelyMonotone_const {c : ℝ} (hc : 0 ≤ c) : IsCompletelyMonotone fun (x : ℝ) => c

A nonnegative constant function is completely monotone.

theorem TauCeti.IsCompletelyMonotone.sum {ι : Type u_1} {s : Finset ι} {f : ι → ℝ → ℝ} (hf : ∀ i ∈ s, IsCompletelyMonotone (f i)) : IsCompletelyMonotone fun (t : ℝ) => ∑ i ∈ s, f i t

Completely monotone functions are closed under finite sums.

theorem TauCeti.isCompletelyMonotone_exp_neg_mul {x : ℝ} (hx : 0 ≤ x) : IsCompletelyMonotone fun (t : ℝ) => Real.exp (-x * t)

The prototype completely monotone function t ↦ e^{-x t} for x ≥ 0. Its n-th derivative is (-x)ⁿ e^{-x t}, so (-1)ⁿ times it is xⁿ e^{-x t} ≥ 0.

def TauCeti.IsCompletelyMonotoneOnIoi (f : ℝ → ℝ) : Prop

Complete monotonicity on the open half-line (0, ∞): the function is C^∞ there and its ordinary iterated derivatives alternate in sign. This is the version used for derivatives of Bernstein functions, whose right derivatives need not be finite at 0.

Equations

• TauCeti.IsCompletelyMonotoneOnIoi f = (ContDiffOn ℝ (↑⊤) f (Set.Ioi 0) ∧ ∀ (n : ℕ) (t : ℝ), 0 < t → 0 ≤ (-1) ^ n * iteratedDeriv n f t)

theorem TauCeti.isCompletelyMonotoneOnIoi_iff_completelyMonotoneOn {f : ℝ → ℝ} : IsCompletelyMonotoneOnIoi f ↔ CompletelyMonotoneOn f (Set.Ioi 0)

Complete monotonicity on (0, ∞) is the open-half-line specialization of complete monotonicity on a set.

theorem TauCeti.IsCompletelyMonotoneOnIoi.contDiffOn {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) : ContDiffOn ℝ (↑⊤) f (Set.Ioi 0)

A completely monotone function on (0, ∞) is smooth there.

theorem TauCeti.IsCompletelyMonotoneOnIoi.neg_one_pow_mul_iteratedDeriv_nonneg {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) (n : ℕ) {t : ℝ} (ht : 0 < t) : 0 ≤ (-1) ^ n * iteratedDeriv n f t

The sign-alternation property on (0, ∞).

theorem TauCeti.IsCompletelyMonotoneOnIoi.nonneg {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) {t : ℝ} (ht : 0 < t) : 0 ≤ f t

A completely monotone function on (0, ∞) is nonnegative there.

theorem TauCeti.IsCompletelyMonotoneOnIoi.nonneg_of_continuousWithinAt {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) (hcont : ContinuousWithinAt f (Set.Ici 0) 0) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ f t

A function completely monotone on (0, ∞) that is continuous within [0, ∞) at the origin is nonnegative on all of [0, ∞): nonnegativity on (0, ∞) passes to the boundary point 0 in the limit.

theorem TauCeti.IsCompletelyMonotoneOnIoi.deriv_nonpos {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) {t : ℝ} (ht : 0 < t) : deriv f t ≤ 0

The derivative of a completely monotone function on (0, ∞) is nonpositive there.

theorem TauCeti.IsCompletelyMonotoneOnIoi.convexOn {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) : ConvexOn ℝ (Set.Ioi 0) f

A function completely monotone on (0, ∞) is convex there: its second derivative is the alternating derivative of order 2, hence nonnegative.

theorem TauCeti.IsCompletelyMonotoneOnIoi.congr {f g : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) (h : Set.EqOn g f (Set.Ioi 0)) : IsCompletelyMonotoneOnIoi g

Complete monotonicity on (0, ∞) is preserved by pointwise equality there.

theorem TauCeti.IsCompletelyMonotoneOnIoi.add {f g : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) (hg : IsCompletelyMonotoneOnIoi g) : IsCompletelyMonotoneOnIoi (f + g)

Complete monotonicity on (0, ∞) is closed under addition.

theorem TauCeti.IsCompletelyMonotoneOnIoi.smul {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) {c : ℝ} (hc : 0 ≤ c) : IsCompletelyMonotoneOnIoi (c • f)

Complete monotonicity on (0, ∞) is closed under multiplication by a nonnegative constant.

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

The closed-half-line Tau Ceti predicate restricts to complete monotonicity on (0, ∞).

theorem TauCeti.IsCompletelyMonotoneOnIoi.isCompletelyMonotone_comp_add_const {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) {a : ℝ} (ha : 0 < a) : IsCompletelyMonotone fun (t : ℝ) => f (t + a)

Positive right-translates of a function completely monotone on (0, ∞) satisfy the strong closed-half-line predicate: the shift moves the boundary into the open half-line, where all derivatives exist. Compare IsCompletelyMonotone.comp_add_const, which keeps the strong predicate under nonnegative translates.

theorem TauCeti.isCompletelyMonotoneOnIoi_of_forall_comp_add_const {f : ℝ → ℝ} (h : ∀ (a : ℝ), 0 < a → IsCompletelyMonotoneOnIoi fun (s : ℝ) => f (s + a)) : IsCompletelyMonotoneOnIoi f

Complete monotonicity on (0, ∞) is detected by the positive translates of a function: if t ↦ f (t + a) is completely monotone on (0, ∞) for every a > 0, then so is f. This is the converse of TauCeti.IsCompletelyMonotoneOnIoi.isCompletelyMonotone_comp_add_const, and it is how a statement proved after moving the boundary into the open half-line is transported back.

Closed-half-line complete monotonicity

def TauCeti.IsContinuousCompletelyMonotoneOnIoi (f : ℝ → ℝ) : Prop

Roadmap-level complete monotonicity on the closed half-line.

This is the classical finite-measure hypothesis: the function is continuous on [0, ∞) and completely monotone on the open half-line (0, ∞). It is weaker at the endpoint than the existing IsCompletelyMonotone, which requires all derivatives within [0, ∞) to exist at 0.

Equations

• TauCeti.IsContinuousCompletelyMonotoneOnIoi f = (ContinuousOn f (Set.Ici 0) ∧ TauCeti.IsCompletelyMonotoneOnIoi f)

theorem TauCeti.isContinuousCompletelyMonotoneOnIoi_iff {f : ℝ → ℝ} : IsContinuousCompletelyMonotoneOnIoi f ↔ ContinuousOn f (Set.Ici 0) ∧ IsCompletelyMonotoneOnIoi f

IsContinuousCompletelyMonotoneOnIoi f unfolds to continuity on [0, ∞) and complete monotonicity on the open half-line.

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.continuousOn {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) : ContinuousOn f (Set.Ici 0)

A closed-half-line completely monotone function is continuous on [0, ∞).

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

A closed-half-line completely monotone function is completely monotone on (0, ∞).

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.of_isCompletelyMonotone {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) : IsContinuousCompletelyMonotoneOnIoi f

The existing strong Tau Ceti predicate implies the roadmap-level closed-half-line predicate.

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.add {f g : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) (hg : IsContinuousCompletelyMonotoneOnIoi g) : IsContinuousCompletelyMonotoneOnIoi (f + g)

Closed-half-line complete monotonicity is closed under addition.

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.smul {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) {c : ℝ} (hc : 0 ≤ c) : IsContinuousCompletelyMonotoneOnIoi (c • f)

Closed-half-line complete monotonicity is closed under multiplication by a nonnegative constant.

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.antitoneOn {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) : AntitoneOn f (Set.Ici 0)

A closed-half-line completely monotone function is nonincreasing on [0, ∞): the derivative is nonpositive on the interior and continuity extends the monotonicity to the endpoint.

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.nonneg {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ f t

A closed-half-line completely monotone function is nonnegative on [0, ∞): nonnegativity on the open half-line passes to 0 by continuity.

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.nonneg_zero {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) : 0 ≤ f 0

A closed-half-line completely monotone function is nonnegative at 0.

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.le_apply_zero {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) {t : ℝ} (ht : 0 ≤ t) : f t ≤ f 0

A closed-half-line completely monotone function lies below its value at 0 on [0, ∞).

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.congr {f g : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) (h : Set.EqOn g f (Set.Ici 0)) : IsContinuousCompletelyMonotoneOnIoi g

Closed-half-line complete monotonicity is determined by values on [0, ∞).

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.sum {ι : Type u_1} {s : Finset ι} {F : ι → ℝ → ℝ} (hF : ∀ i ∈ s, IsContinuousCompletelyMonotoneOnIoi (F i)) : IsContinuousCompletelyMonotoneOnIoi fun (t : ℝ) => ∑ i ∈ s, F i t

Closed-half-line complete monotonicity is closed under finite sums.

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.exists_nonneg_tendsto_atTop {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) : ∃ (L : ℝ), Filter.Tendsto f Filter.atTop (nhds L) ∧ 0 ≤ L

A closed-half-line completely monotone function has a limit L ≥ 0 at infinity: it is antitone on [0, ∞) and bounded below by 0.

theorem TauCeti.IsContinuousCompletelyMonotoneOnIoi.le_of_tendsto_atTop {f : ℝ → ℝ} (hcm : IsContinuousCompletelyMonotoneOnIoi f) {L : ℝ} (hL : Filter.Tendsto f Filter.atTop (nhds L)) {T : ℝ} (hT : 0 ≤ T) : L ≤ f T

A closed-half-line completely monotone function lies above its limit at infinity on [0, ∞).

theorem TauCeti.IsCompletelyMonotone.antitoneOn {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) : AntitoneOn f (Set.Ici 0)

A completely monotone function is nonincreasing on [0, ∞): the strong predicate implies the closed-half-line one, whose monotonicity applies.