Measurable families of finite measures on ℝ≥0

A finite measure on ℝ≥0 is determined by its Laplace transform at the natural numbers (TauCeti.Measure.ext_of_forall_laplaceTransform_natCast_eq). This file upgrades that determinacy statement to a measurable one: a family a ↦ μ a of finite measures on ℝ≥0 is measurable for the Giry σ-algebra as soon as each of the scalar functions a ↦ laplaceTransform (μ a) n, n : ℕ, is measurable.

The proof uses the exponential change of variables p ↦ e^{-p}, which carries ℝ≥0 into the unit interval and turns the Laplace transform at n into the n-th moment. Weierstrass approximation then makes a ↦ ∫ g dμ a measurable for every continuous g on the interval, the outer approximation of a closed set by bounded continuous functions transfers this to a ↦ μ a F for closed F, and the closed sets are a π-system generating the Borel σ-algebra.

Because a unique finite measure is attached to each parameter value, no measurable-selection theorem is involved: the family is whatever it is, and the theorem merely certifies it measurable. This is what turns a fibrewise Bernstein representation into a kernel, in TauCeti/Analysis/CompletelyMonotone/Bernstein/Kernel.lean.

Main declarations

• TauCeti.measurable_of_measurable_laplaceTransform_natCast: a family of finite measures on ℝ≥0 is measurable when its Laplace transforms at the natural numbers are.

References

• R. Schilling, R. Song, Z. Vondraček, Bernstein Functions: Theory and Applications (de Gruyter, 2nd ed. 2012), Chapter 1.

• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part C, Milestone 2 (BCR semigroup--Bochner).

The exponential change of variables

Measurability of a family from its Laplace transforms

theorem TauCeti.measurable_of_measurable_laplaceTransform_natCast {α : Type u_1} [MeasurableSpace α] {μ : α → MeasureTheory.Measure NNReal} [∀ (a : α), MeasureTheory.IsFiniteMeasure (μ a)] (h : ∀ (n : ℕ), Measurable fun (a : α) => laplaceTransform (μ a) ↑n) : Measurable μ

Measurability from Laplace transforms. A family of finite measures on ℝ≥0 indexed by a measurable space is measurable for the Giry σ-algebra as soon as each of the functions a ↦ laplaceTransform (μ a) n, for n : ℕ, is measurable.

Only the natural-number values of the transforms are used, matching the determinacy statement TauCeti.Measure.ext_of_forall_laplaceTransform_natCast_eq.