Complete monotonicity in the finite-difference sense, from rational data

TauCeti.IsDifferenceCompletelyMonotone quantifies over all lists of nonnegative real steps and all nonnegative real base points. A construction that produces a candidate function as a countable limit — for instance a fibrewise Radon--Nikodym density, which is only defined up to a null set — can verify the sign condition on a countable set of data and no more. This file closes that gap: for a function that is continuous from the right on [0, ∞), the sign condition on rational lists at rational base points already implies the full predicate (TauCeti.isDifferenceCompletelyMonotone_of_forall_rat).

No density argument in several variables is needed. The steps are freed one at a time, each one costing a single one-variable limit: if every mixed difference of f along l ++ m alternates whenever the extra step is rational, then the signed difference along l ++ m is nonincreasing along rational increments, hence — being right-continuous — nonincreasing outright, which is the sign condition for one further real step. The permutation invariance of a mixed difference (TauCeti.fwdDiffList_eq_of_perm) is what lets the new step be peeled off the front.

The right-continuity hypothesis is doing real work: rational data say nothing whatsoever about the value of f at an irrational point, so lowering f there below zero leaves every rational datum untouched while destroying the sign condition for the empty list of steps.

Main declarations

• TauCeti.tendsto_fwdDiffList_nhdsGT: a mixed forward difference of a right-continuous function is right-continuous.
• TauCeti.isDifferenceCompletelyMonotone_of_forall_rat: rational data suffice.

References

• D. V. Widder, The Laplace Transform (Princeton, 1941), Chapter IV.

theorem TauCeti.tendsto_fwdDiffList_nhdsGT {f : ℝ → ℝ} (hf : ∀ (u : ℝ), 0 ≤ u → Filter.Tendsto f (nhdsWithin u (Set.Ioi u)) (nhds (f u))) {l : List ℝ} (hl : ∀ h ∈ l, 0 ≤ h) {u : ℝ} (hu : 0 ≤ u) : Filter.Tendsto (fwdDiffList l f) (nhdsWithin u (Set.Ioi u)) (nhds (fwdDiffList l f u))

A mixed forward difference of a right-continuous function is right-continuous. The steps are assumed nonnegative so that the shifted base points stay in [0, ∞), where the hypothesis lives.

theorem TauCeti.isDifferenceCompletelyMonotone_of_forall_rat {f : ℝ → ℝ} (hcont : ∀ (u : ℝ), 0 ≤ u → Filter.Tendsto f (nhdsWithin u (Set.Ioi u)) (nhds (f u))) (hrat : ∀ (l : List ℚ), (∀ h ∈ l, 0 ≤ h) → ∀ (s : ℚ), 0 ≤ s → 0 ≤ (-1) ^ l.length * fwdDiffList (List.map Rat.cast l) f ↑s) : IsDifferenceCompletelyMonotone f

Rational data suffice for complete monotonicity in the finite-difference sense. A function that is continuous from the right at every point of [0, ∞) and whose mixed forward differences along lists of nonnegative rational steps alternate at every nonnegative rational base point is completely monotone in the finite-difference sense.

This is the form in which a fibrewise construction verifies the hypothesis of the Hausdorff--Bernstein--Widder theorem: countably many almost-everywhere statements can be intersected, whereas the uncountable family of conditions packaged in TauCeti.IsDifferenceCompletelyMonotone cannot.