Pointwise limits of completely monotone functions

Complete monotonicity on (0, ∞) is stable under pointwise convergence: no uniformity, no equicontinuity, and no smoothness of the limit need be assumed. This file proves that closure property, completing the algebraic ones of TauCeti.Analysis.CompletelyMonotone.OpenClosure.

The derivative form of the predicate is not visibly stable under pointwise limits — nothing says that the derivatives converge — so the proof passes through the finite-difference form TauCeti.IsDifferenceCompletelyMonotone, which is manifestly stable (TauCeti.isDifferenceCompletelyMonotone_of_tendsto), and comes back through the representation theorem of TauCeti.Analysis.CompletelyMonotone.FiniteDifference.Laplace. That return trip needs the limit to be right-continuous at the left endpoint of the half-line it is stated on, and this is where the convexity of a completely monotone function is used: a pointwise limit of convex functions is convex, hence continuous on the open half-line, so every positive translate of the limit is right-continuous at 0. That convexity is TauCeti.IsCompletelyMonotoneOnIoi.convexOn.

The open half-line is not a defect of the proof. Complete monotonicity on the closed half-line is genuinely not closed under pointwise limits: the functions t ↦ (1 + n t)⁻¹ are completely monotone on [0, ∞) and converge pointwise to the indicator of {0}, which is not even continuous. What survives at the endpoint is exactly one extra hypothesis, right-continuity at 0, and with it TauCeti.IsContinuousCompletelyMonotoneOnIoi is closed under pointwise limits too.

Main declarations

• TauCeti.isCompletelyMonotoneOnIoi_of_tendsto: complete monotonicity on (0, ∞) is closed under pointwise limits.
• TauCeti.isContinuousCompletelyMonotoneOnIoi_of_tendsto: the closed-half-line predicate is closed under pointwise limits of functions completely monotone on (0, ∞), given right-continuity of the limit at 0.

References

• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications (de Gruyter, 2nd ed. 2012), Corollary 1.7.
• D. V. Widder, The Laplace Transform (Princeton, 1941), Chapter IV.

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

Complete monotonicity on (0, ∞) is closed under pointwise limits. A pointwise limit of functions completely monotone on (0, ∞) is completely monotone on (0, ∞); in particular it is automatically C^∞ there.

Nothing is assumed about the limit, and no uniformity is assumed about the convergence. The closed half-line version is false, see the module docstring, and TauCeti.isContinuousCompletelyMonotoneOnIoi_of_tendsto for what replaces it.

theorem TauCeti.isContinuousCompletelyMonotoneOnIoi_of_tendsto {f : ℝ → ℝ} {ι : Type u_1} {L : Filter ι} [L.NeBot] {F : ι → ℝ → ℝ} (hF : ∀ᶠ (i : ι) in L, IsCompletelyMonotoneOnIoi (F i)) (hlim : ∀ (u : ℝ), 0 < u → Filter.Tendsto (fun (i : ι) => F i u) L (nhds (f u))) (hzero : ContinuousWithinAt f (Set.Ici 0) 0) : IsContinuousCompletelyMonotoneOnIoi f

Complete monotonicity in the closed-half-line sense of TauCeti.IsContinuousCompletelyMonotoneOnIoi is closed under pointwise limits on (0, ∞), once the limit is known to be right-continuous at the endpoint. That extra hypothesis cannot be dropped: see the module docstring.