Bernstein's theorem: existence of a representing measure

A completely monotone function on [0, ∞) is the Laplace transform of a finite positive measure on ℝ≥0.

Main results

• TauCeti.exists_representsLaplace_of_isCompletelyMonotone

Scope

This is the existence half of the Bernstein milestone in TauCetiRoadmap/OneParameterSemigroups/README.md, Part B. Uniqueness of the representing measure is TauCeti.RepresentsLaplace.unique, the converse direction is TauCeti.isContinuousCompletelyMonotoneOnIoi_laplaceTransform, and all three combine in Bernstein/HausdorffBernsteinWidder.lean as TauCeti.hausdorff_bernstein_widder and TauCeti.hausdorff_bernstein_widder_existsUnique.

Finiteness of the representing measure is not an extra hypothesis but a consequence of complete monotonicity on the closed half-line: IsCompletelyMonotone builds in Set.Ici 0, so f takes a real value at 0, and the representing measure has total mass f 0. On the open half-line alone the value at 0 need not exist and the representing measure can be infinite — 1/t is completely monotone on (0, ∞) with representing measure Lebesgue.

Implementation

Bernstein/Measures.lean supplies the Chafaï approximating measures chafaiRescaled f n on ℝ≥0 and the reconstruction identity f x - L = ∫ bernsteinKernel n x ∂(chafaiRescaled f n), where L = lim_{t→∞} f t. Those measures are uniformly mass-bounded and, by Bernstein/Tightness.lean, tight. The three remaining steps are:

1. extract a weak limit μ₀ from tightness;
2. pass the reconstruction identity to that limit, replacing the Bernstein kernel by e^{-xp}, which represents the non-constant part f - L;
3. add the atom L • δ₀, whose Laplace transform is the constant L, to represent f itself.

Step 1 uses finite_measure_cluster_limit rather than its subsequence form finite_measure_subseq_limit: the latter needs FirstCountableTopology (FiniteMeasure ℝ≥0), and Mathlib's metrizability instances for spaces of measures are stated for ProbabilityMeasure, not FiniteMeasure. No subsequence is actually required — every ingredient is a filter limit, so an ultrafilter below atTop suffices, and being NeBot it still gives uniqueness of limits.

References

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

• D. Chafaï, Aspects of the Bernstein theorem (2013) — the approximating measures this proof passes to the limit.

• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions (de Gruyter, 2nd ed. 2012), Ch. 1.

theorem TauCeti.exists_representsLaplace_of_isCompletelyMonotone {f : ℝ → ℝ} (hcm : IsCompletelyMonotone f) : ∃ (μ : MeasureTheory.Measure NNReal), RepresentsLaplace μ f

Bernstein's theorem, existence half. A completely monotone function on [0, ∞) is the Laplace transform of a finite positive measure on ℝ≥0.

Uniqueness of that measure is not asserted here; it is TauCeti.RepresentsLaplace.unique, and the two combine in the Hausdorff--Bernstein--Widder theorem.