Complete monotonicity in the finite-difference sense

TauCeti.IsCompletelyMonotone asks for a smooth function whose iterated derivatives alternate in sign. There is a second, purely order-theoretic notion, which mentions no derivatives at all: a function f : ℝ → ℝ is completely monotone in the finite-difference sense when every iterated forward difference taken with an arbitrary list [h₁, …, hₙ] of nonnegative steps has the sign (-1)ⁿ, 0 ≤ (-1)ⁿ (Δ_{h₁} ⋯ Δ_{hₙ} f)(t) for t ≥ 0, where Δ_h g = fun t => g (t + h) - g t is Mathlib's fwdDiff. Low orders read as f ≥ 0, f nonincreasing, f "convex along every pair of steps", and so on.

This file introduces the predicate TauCeti.IsDifferenceCompletelyMonotone and proves that on smooth functions it is exactly complete monotonicity (TauCeti.isCompletelyMonotone_iff_isDifferenceCompletelyMonotone). The two halves are genuinely different in character:

• difference to derivative: fixing a list l, the sign hypothesis for k :: l says that the slope of Δ_l f over [t, t + k] has the sign (-1)^(|l|+1); letting k → 0⁺ turns that into the sign of (Δ_l f)' = Δ_l f', so -f' again satisfies the hypothesis and an induction on the order finishes the argument;
• derivative to difference: if f is completely monotone and a ≥ 0 then so is t ↦ f t - f (t + a), because the n-th alternating derivative of f is itself completely monotone, hence nonincreasing (TauCeti.IsCompletelyMonotone.sub_comp_add_const). Iterating this over the list gives the sign of every mixed difference.

The finite-difference form is the hypothesis that arises in practice: the alternating differences of a positive-definite function on the involutive semigroup [0, ∞) × V are positive definite, so the mass of the associated spatial Bochner measure is a function of time all of whose mixed differences alternate, with no smoothness available a priori. Combining the characterization here with the mollification of TauCeti.Analysis.CompletelyMonotone.FiniteDifference.Mollify converts that hypothesis into the input of the Hausdorff--Bernstein--Widder theorem, up to an arbitrarily small shift of the argument.

Main declarations

• TauCeti.fwdDiffList: the forward difference Δ_{h₁} ⋯ Δ_{hₙ} f along a list of steps.
• TauCeti.fwdDiffList_congr: on [0, ∞) a mixed difference with nonnegative steps only sees the values of the function there, and TauCeti.fwdDiffList_congr_of_add_mem sharpens this to any set of arguments closed under adding the steps.
• TauCeti.IsDifferenceCompletelyMonotone: complete monotonicity in the finite-difference sense.
• TauCeti.isDifferenceCompletelyMonotone_of_tendsto: the predicate is closed under pointwise limits on [0, ∞), unlike its derivative form.
• TauCeti.IsDifferenceCompletelyMonotone.neg_derivWithin: the negated derivative within the half-line of a differentiable finite-difference completely monotone function is again one.
• TauCeti.IsDifferenceCompletelyMonotone.isCompletelyMonotone: a C^∞ function that is completely monotone in the finite-difference sense is completely monotone.
• TauCeti.IsCompletelyMonotone.sub_comp_add_const: if f is completely monotone and 0 ≤ a then so is t ↦ f t - f (t + a).
• TauCeti.isCompletelyMonotone_iff_isDifferenceCompletelyMonotone: the two notions agree on C^∞ functions.

References

• D. V. Widder, The Laplace Transform (Princeton, 1941), Chapter IV.
• C. Berg, J. P. R. Christensen, P. Ressel, Harmonic Analysis on Semigroups (GTM 100, 1984).

Forward differences along a list of steps

def TauCeti.fwdDiffList {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (l : List M) (f : M → G) : M → G

The iterated forward difference of f along a list of steps: fwdDiffList [h₁, …, hₙ] f is Δ_{h₁} (⋯ (Δ_{hₙ} f)), built from Mathlib's fwdDiff. The order of the steps is irrelevant, but keeping them in a list is what makes mixed step sizes available, which is strictly more information than the iterates (Δ_h)^[n] of a single step.

Equations

• TauCeti.fwdDiffList l f = List.foldr fwdDiff f l

@[simp]

theorem TauCeti.fwdDiffList_nil {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (f : M → G) : fwdDiffList [] f = f

The empty list of steps takes no difference at all.

@[simp]

theorem TauCeti.fwdDiffList_cons {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (h : M) (l : List M) (f : M → G) : fwdDiffList (h :: l) f = fwdDiff h (fwdDiffList l f)

Consing a step applies one more forward difference on the outside.

theorem TauCeti.fwdDiffList_append {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (l l' : List M) (f : M → G) : fwdDiffList (l ++ l') f = fwdDiffList l (fwdDiffList l' f)

Concatenating step lists composes the corresponding difference operators.

theorem TauCeti.fwdDiffList_eq_of_perm {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] {l l' : List M} (h : l.Perm l') (f : M → G) : fwdDiffList l f = fwdDiffList l' f

Permuting the step sizes does not change a mixed forward difference.

theorem TauCeti.fwdDiffList_replicate {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (n : ℕ) (h : M) (f : M → G) : fwdDiffList (List.replicate n h) f = (fwdDiff h)^[n] f

Along a constant list the mixed difference is the iterated single-step difference.

theorem TauCeti.fwdDiffList_add {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (l : List M) (f g : M → G) : (fwdDiffList l fun (t : M) => f t + g t) = fun (t : M) => fwdDiffList l f t + fwdDiffList l g t

Mixed differences commute with addition.

theorem TauCeti.fwdDiffList_const_smul {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] {R : Type u_3} [Monoid R] [DistribMulAction R G] (c : R) (l : List M) (f : M → G) : (fwdDiffList l fun (t : M) => c • f t) = fun (t : M) => c • fwdDiffList l f t

Mixed differences commute with scalar multiplication by a constant.

theorem TauCeti.fwdDiffList_neg {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (l : List M) (f : M → G) : (fwdDiffList l fun (t : M) => -f t) = fun (t : M) => -fwdDiffList l f t

Mixed differences are additive-group homomorphisms: they commute with negation.

theorem TauCeti.fwdDiffList_congr_of_add_mem {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] {S : Set M} {l : List M} {f g : M → G} {t : M} (hS : ∀ h ∈ l, ∀ u ∈ S, u + h ∈ S) (ht : t ∈ S) (hfg : ∀ u ∈ S, f u = g u) : fwdDiffList l f t = fwdDiffList l g t

A mixed forward difference only reads the function on a set closed under its steps. If S contains the base point and is closed under adding each step, the difference at that point depends on the function only through its values on S. Compare TauCeti.fwdDiffList_congr, which is the case of nonnegative real steps and S = [0, ∞).

theorem TauCeti.fwdDiffList_congr {f g : ℝ → ℝ} {l : List ℝ} (hl : ∀ h ∈ l, 0 ≤ h) (hfg : ∀ (u : ℝ), 0 ≤ u → g u = f u) {t : ℝ} (ht : 0 ≤ t) : fwdDiffList l g t = fwdDiffList l f t

Only the values of f on [0, ∞) matter for a mixed difference evaluated there, as long as all the steps are nonnegative.

theorem TauCeti.continuous_fwdDiffList {f : ℝ → ℝ} (l : List ℝ) (hf : Continuous f) : Continuous (fwdDiffList l f)

A mixed difference of a continuous function is continuous.

The finite-difference predicate

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

A function f : ℝ → ℝ is completely monotone in the finite-difference sense if every mixed forward difference along a list of nonnegative steps has the alternating sign of its length, at every point of [0, ∞): 0 ≤ (-1)ⁿ (Δ_{h₁} ⋯ Δ_{hₙ} f)(t) for h₁, …, hₙ ≥ 0 and t ≥ 0.

Unlike TauCeti.IsCompletelyMonotone this mentions no derivative, so it makes sense for an arbitrary function; on C^∞ functions the two agree (TauCeti.isCompletelyMonotone_iff_isDifferenceCompletelyMonotone). Mixed steps, rather than the iterates of a single step, are what makes the notion stable under differentiation.

Equations

• TauCeti.IsDifferenceCompletelyMonotone f = ∀ (l : List ℝ), (∀ h ∈ l, 0 ≤ h) → ∀ (t : ℝ), 0 ≤ t → 0 ≤ (-1) ^ l.length * TauCeti.fwdDiffList l f t

theorem TauCeti.isDifferenceCompletelyMonotone_iff {f : ℝ → ℝ} : IsDifferenceCompletelyMonotone f ↔ ∀ (l : List ℝ), (∀ h ∈ l, 0 ≤ h) → ∀ (t : ℝ), 0 ≤ t → 0 ≤ (-1) ^ l.length * fwdDiffList l f t

IsDifferenceCompletelyMonotone f unfolds to the alternating sign condition on every mixed forward difference with nonnegative steps.

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

A function that is completely monotone in the finite-difference sense is nonnegative on [0, ∞): this is the hypothesis for the empty list of steps.

theorem TauCeti.IsDifferenceCompletelyMonotone.apply_add_le {f : ℝ → ℝ} (hf : IsDifferenceCompletelyMonotone f) {t h : ℝ} (ht : 0 ≤ t) (hh : 0 ≤ h) : f (t + h) ≤ f t

A function that is completely monotone in the finite-difference sense is nonincreasing on [0, ∞): this is the hypothesis for a single step.

theorem TauCeti.IsDifferenceCompletelyMonotone.congr {f g : ℝ → ℝ} (hf : IsDifferenceCompletelyMonotone f) (hfg : ∀ (t : ℝ), 0 ≤ t → g t = f t) : IsDifferenceCompletelyMonotone g

The predicate depends only on the values of the function on [0, ∞).

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

A function that is completely monotone in the finite-difference sense is nonincreasing on [0, ∞).

theorem TauCeti.IsDifferenceCompletelyMonotone.neg_fwdDiff {f : ℝ → ℝ} (hf : IsDifferenceCompletelyMonotone f) {h : ℝ} (hh : 0 ≤ h) : IsDifferenceCompletelyMonotone fun (t : ℝ) => -fwdDiff h f t

The finite-difference predicate is stable under taking one more difference: if f qualifies and 0 ≤ h, then so does -Δ_h f.

theorem TauCeti.tendsto_fwdDiffList {f : ℝ → ℝ} {ι : Type u_3} {L : Filter ι} {F : ι → ℝ → ℝ} {l : List ℝ} (hl : ∀ h ∈ l, 0 ≤ h) (hF : ∀ (u : ℝ), 0 ≤ u → Filter.Tendsto (fun (i : ι) => F i u) L (nhds (f u))) {t : ℝ} (ht : 0 ≤ t) : Filter.Tendsto (fun (i : ι) => fwdDiffList l (F i) t) L (nhds (fwdDiffList l f t))

Mixed differences pass to a pointwise limit. As in TauCeti.fwdDiffList_congr, a mixed difference with nonnegative steps evaluated on [0, ∞) only reads the function there, so convergence on [0, ∞) is all that is needed.

theorem TauCeti.isDifferenceCompletelyMonotone_of_tendsto {f : ℝ → ℝ} {ι : Type u_3} {L : Filter ι} [L.NeBot] {F : ι → ℝ → ℝ} (hF : ∀ᶠ (i : ι) in L, IsDifferenceCompletelyMonotone (F i)) (hlim : ∀ (u : ℝ), 0 ≤ u → Filter.Tendsto (fun (i : ι) => F i u) L (nhds (f u))) : IsDifferenceCompletelyMonotone f

Complete monotonicity in the finite-difference sense is closed under pointwise limits on [0, ∞), the half-line the predicate lives on. This is a genuine advantage of the finite-difference formulation: the derivative form is not visibly stable under pointwise convergence.

theorem TauCeti.IsDifferenceCompletelyMonotone.add {f g : ℝ → ℝ} (hf : IsDifferenceCompletelyMonotone f) (hg : IsDifferenceCompletelyMonotone g) : IsDifferenceCompletelyMonotone fun (t : ℝ) => f t + g t

Complete monotonicity in the finite-difference sense is closed under addition.

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

Complete monotonicity in the finite-difference sense is closed under multiplication by a nonnegative constant.

Differences commute with differentiation

theorem TauCeti.differentiable_fwdDiffList {f : ℝ → ℝ} (l : List ℝ) (hf : Differentiable ℝ f) : Differentiable ℝ (fwdDiffList l f)

A mixed difference of a differentiable function is differentiable.

theorem TauCeti.deriv_fwdDiffList {f : ℝ → ℝ} (l : List ℝ) (hf : Differentiable ℝ f) : deriv (fwdDiffList l f) = fwdDiffList l (deriv f)

Forward differences commute with differentiation.

From differences to derivatives

theorem TauCeti.IsDifferenceCompletelyMonotone.neg_derivWithin {f : ℝ → ℝ} (hf : IsDifferenceCompletelyMonotone f) (hd : DifferentiableOn ℝ f (Set.Ici 0)) : IsDifferenceCompletelyMonotone fun (t : ℝ) => -derivWithin f (Set.Ici 0) t

Passing to the negated derivative within [0, ∞) preserves complete monotonicity in the finite-difference sense. The sign of (Δ_l f)' is read off from the sign of the extra difference Δ_k (Δ_l f) by letting the step k tend to 0 from the right.

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

A function that is C^∞ on [0, ∞) and completely monotone in the finite-difference sense has alternating iterated derivatives within that half-line.

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

Finite differences detect complete monotonicity. A C^∞ function all of whose mixed forward differences alternate in sign on [0, ∞) is completely monotone.

From derivatives to differences

theorem TauCeti.IsCompletelyMonotone.isDifferenceCompletelyMonotone {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) : IsDifferenceCompletelyMonotone f

A completely monotone function is completely monotone in the finite-difference sense.

theorem TauCeti.isCompletelyMonotone_iff_isDifferenceCompletelyMonotone {f : ℝ → ℝ} (hs : ContDiffOn ℝ (↑⊤) f (Set.Ici 0)) : IsCompletelyMonotone f ↔ IsDifferenceCompletelyMonotone f

The finite-difference characterization of complete monotonicity. For a C^∞ function, alternating mixed forward differences on [0, ∞) are equivalent to alternating iterated derivatives there.