Integral lemmas for completely monotone functions

Taylor-remainder sign bounds and finite- and improper-integral facts about completely monotone functions.

These extend the object API in CompletelyMonotone/Basic.lean with the sign of the Taylor integral remainder, the finite-interval integral-of-(-f') identity, and improper-integral facts for the first derivative within [0, ∞).

Main declarations

• TauCeti.IsCompletelyMonotone.neg_one_pow_mul_taylor_remainder_nonneg: the Taylor integral remainder has sign (-1)ⁿ.
• TauCeti.IsCompletelyMonotone.continuousOn_iteratedDerivWithin_uIcc: every iterated derivative within [0, ∞) is continuous on a compact interval [x, T] ⊆ [0, ∞).
• TauCeti.IsCompletelyMonotone.integral_neg_iteratedDerivWithin_one_Ici_eq_sub: on a compact interval in [0, ∞), the integral of -f' is the endpoint drop f x - f T.
• TauCeti.IsCompletelyMonotone.neg_iteratedDerivWithin_one_integrableOn, TauCeti.IsCompletelyMonotone.integral_Ioi_neg_iteratedDerivWithin_one: integrability and the improper integral of -f' on (0, ∞), represented as iteratedDerivWithin 1.
• TauCeti.IsCompletelyMonotone.integral_Ioi_neg_iteratedDerivWithin_one_of_nonneg: the same improper integral from an arbitrary nonnegative endpoint, ∫ₓ^∞ (-f') = f x - L.

References

• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part B (Bernstein theorem milestone).

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

• D. Chafaï, Aspects of the Bernstein theorem (2013).

theorem TauCeti.IsCompletelyMonotone.neg_one_pow_mul_taylor_remainder_nonneg {f : ℝ → ℝ} (hf : IsCompletelyMonotone f) {x T : ℝ} {n : ℕ} (hx : 0 ≤ x) (hxT : x ≤ T) : 0 ≤ (-1) ^ n * ∫ (t : ℝ) in x..T, (↑(n - 1).factorial)⁻¹ * (T - t) ^ (n - 1) * iteratedDerivWithin n f (Set.Icc x T) t

CM sign of the Taylor remainder. For a completely monotone function the Taylor integral remainder ∫ₓᵀ (T-t)ⁿ⁻¹/(n-1)! · f⁽ⁿ⁾(t) dt has sign (-1)ⁿ: 0 ≤ (-1)ⁿ times it.

Smoothness-index helpers

theorem TauCeti.IsCompletelyMonotone.continuousOn_iteratedDerivWithin_uIcc {f : ℝ → ℝ} (hcm : IsCompletelyMonotone f) (m : ℕ) {x T : ℝ} (hx : 0 ≤ x) (hT : 0 ≤ T) : ContinuousOn (iteratedDerivWithin m f (Set.Ici 0)) (Set.uIcc x T)

Every iterated derivative within [0, ∞) of a completely monotone function is continuous on the interval spanned by any two nonnegative endpoints. The endpoints need no ordering: uIcc is the unordered interval, and [0, ∞) is order-connected.

theorem TauCeti.IsCompletelyMonotone.integral_neg_iteratedDerivWithin_one_Ici_eq_sub {f : ℝ → ℝ} (hcm : IsCompletelyMonotone f) {x T : ℝ} (hx : 0 ≤ x) (hxT : x ≤ T) : ∫ (t : ℝ) in x..T, -iteratedDerivWithin 1 f (Set.Ici 0) t = f x - f T

On a compact interval in [0, ∞), the integral of -f' for a completely monotone function is the endpoint drop, with the derivative taken within [0, ∞).

theorem TauCeti.IsCompletelyMonotone.neg_iteratedDerivWithin_one_integrableOn {f : ℝ → ℝ} (hcm : IsCompletelyMonotone f) : MeasureTheory.IntegrableOn (fun (t : ℝ) => -iteratedDerivWithin 1 f (Set.Ici 0) t) (Set.Ioi 0) MeasureTheory.volume

-f' is integrable on (0, ∞) for a completely monotone function, where the derivative is taken within the closed half-line [0, ∞).

theorem TauCeti.IsCompletelyMonotone.integral_Ioi_neg_iteratedDerivWithin_one_of_nonneg {f : ℝ → ℝ} (hcm : IsCompletelyMonotone f) {x : ℝ} (hx : 0 ≤ x) {L : ℝ} (hL : Filter.Tendsto f Filter.atTop (nhds L)) : ∫ (t : ℝ) in Set.Ioi x, -iteratedDerivWithin 1 f (Set.Ici 0) t = f x - L

The improper integral ∫ₓ^∞ (-f') dt = f x - L from an arbitrary nonnegative endpoint x, for a completely monotone function with limit L at infinity.

theorem TauCeti.IsCompletelyMonotone.integral_Ioi_neg_iteratedDerivWithin_one {f : ℝ → ℝ} (hcm : IsCompletelyMonotone f) {L : ℝ} (hL : Filter.Tendsto f Filter.atTop (nhds L)) : ∫ (t : ℝ) in Set.Ioi 0, -iteratedDerivWithin 1 f (Set.Ici 0) t = f 0 - L

The improper integral ∫₀^∞ (-f') dt = f(0) - L for completely monotone functions.