Smoothing a finite-difference completely monotone function

TauCeti.IsDifferenceCompletelyMonotone.isCompletelyMonotone upgrades the finite-difference sign condition to genuine complete monotonicity, but only for a function that is already C^∞. This file supplies the missing smoothing step without imposing any regularity beyond the difference condition itself.

Averaging f against a smooth probability density supported in (-ε, 0), g t = ∫ ψ s · f (t - s) ds, only ever evaluates f on [t, t + ε], so on [0, ∞) it never leaves the half-line where the hypothesis lives. The average is C^∞ because it is a convolution with a smooth compactly supported kernel, and every mixed forward difference of g is the same average of the corresponding difference of f, so the sign condition passes to g verbatim. Since f is nonincreasing, g is squeezed between f (· + ε) and f, by the general kernel-average bound TauCeti.MeasureTheory.integral_kernel_mem_Icc_of_antitoneOn.

The outcome, TauCeti.IsDifferenceCompletelyMonotone.exists_isCompletelyMonotone_between_shift, is a completely monotone g with f (t + ε) ≤ g t ≤ f t on [0, ∞).

Main declarations

• TauCeti.IsDifferenceCompletelyMonotone.exists_isCompletelyMonotone_between_shift: a function that is completely monotone in the finite-difference sense is squeezed between the shift f (· + ε) and f by a completely monotone function, for every ε > 0.

References

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

theorem TauCeti.IsDifferenceCompletelyMonotone.exists_isCompletelyMonotone_between_shift {f : ℝ → ℝ} (hf : IsDifferenceCompletelyMonotone f) {ε : ℝ} (hε : 0 < ε) : ∃ (g : ℝ → ℝ), IsCompletelyMonotone g ∧ ∀ (t : ℝ), 0 ≤ t → f (t + ε) ≤ g t ∧ g t ≤ f t

Smoothing a finite-difference completely monotone function. If all mixed forward differences of f with nonnegative steps alternate in sign on [0, ∞), then for every ε > 0 there is a genuinely completely monotone g with f (t + ε) ≤ g t ≤ f t for t ≥ 0.

The function g is the average of f against a smooth probability density supported in (-ε, 0); smoothness comes from the convolution, the sign condition is inherited pointwise, and the two-sided bound is monotonicity of f.