Tightness of the Chafaï approximating measures

This file proves the tightness input for the Prokhorov extraction step in Bernstein's theorem. For a completely monotone function f, the rescaled Chafaï measures have uniformly bounded first moment:

∫⁻ p, p ∂(chafaiRescaled f n) ≤ -f'(0).

Markov's inequality therefore bounds their mass outside [0, R] by -f'(0) / R, uniformly in n. Since the intervals [0, R] are compact in ℝ≥0, this proves that the whole family is tight.

Main declarations

• TauCeti.chafaiRescaled_measure_Ioi_le: the uniform first-moment tail bound.
• TauCeti.isTightMeasureSet_range_chafaiRescaled: the rescaled Chafaï measures form a tight family.

References

• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part B, Bernstein's theorem milestone (“measure extraction via Prokhorov tightness”).
• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications (de Gruyter, 2nd ed. 2012), Ch. 1.
• D. Chafaï, Aspects of the Bernstein theorem (2013).

theorem TauCeti.chafaiRescaled_measure_Ioi_le {f : ℝ → ℝ} (hcm : IsCompletelyMonotone f) (n : ℕ) {R : NNReal} (hR : R ≠ 0) : (chafaiRescaled f n) (Set.Ioi R) ≤ ENNReal.ofReal (-derivWithin f (Set.Ici 0) 0) / ↑R

The rescaled Chafaï measures satisfy the uniform Markov tail estimate

chafaiRescaled f n (R, ∞) ≤ ofReal (-f'(0)) / R

for every positive R. The derivative is taken within [0, ∞), as in the definition of complete monotonicity.

theorem TauCeti.isTightMeasureSet_range_chafaiRescaled {f : ℝ → ℝ} (hcm : IsCompletelyMonotone f) : MeasureTheory.IsTightMeasureSet (Set.range (chafaiRescaled f))

The family of all rescaled Chafaï approximating measures of a completely monotone function is tight. Equivalently, for every positive error tolerance there is a compact interval [0, R] ⊆ ℝ≥0 whose complement has at most that much mass for every approximation order.