Measurable Bernstein measures and their kernel form

The Hausdorff--Bernstein--Widder theorem and its basic representing-measure API live in TauCeti.Analysis.CompletelyMonotone.Bernstein.HausdorffBernsteinWidder. This file shows that the Bernstein measure depends measurably on a parameter: a family a ↦ f a of completely monotone functions whose values at the natural numbers are measurable in a has Bernstein measures forming a ProbabilityTheory.Kernel.

Measurability is not a selection statement. The representing measure is unique, so the family a ↦ bernsteinMeasure (f a) is already determined; what has to be proved is that this particular family is measurable, and that is TauCeti.measurable_of_measurable_laplaceTransform_natCast, applied to the identity laplaceTransform (bernsteinMeasure (f a)) n = f a n.

Main declarations

• TauCeti.measurable_bernsteinMeasure: measurable dependence on a parameter.
• TauCeti.bernsteinMeasureKernel: the resulting kernel, with its finiteness criterion.

References

The finite-measure representation is the Hausdorff--Bernstein--Widder theorem, after S. Bernstein (1928) and D. V. Widder, The Laplace Transform, Chapter IV; see also R. Schilling, R. Song, Z. Vondraček, Bernstein Functions (de Gruyter, 2nd ed. 2012), Theorem 1.4.

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

theorem TauCeti.measurable_bernsteinMeasure {α : Type u_1} [MeasurableSpace α] {F : α → ℝ → ℝ} (hcm : ∀ (a : α), IsContinuousCompletelyMonotoneOnIoi (F a)) (hmeas : ∀ (n : ℕ), Measurable fun (a : α) => F a ↑n) : Measurable fun (a : α) => bernsteinMeasure (F a)

The Bernstein measure depends measurably on a parameter. If every member of a family of functions is continuous on [0, ∞) and completely monotone on (0, ∞), and if the family is measurable in the parameter at each natural number, then the family of Bernstein measures is measurable for the Giry σ-algebra.

Only the values at natural numbers enter, because a finite measure on ℝ≥0 is already determined by its Laplace transform there.

noncomputable def TauCeti.bernsteinMeasureKernel {α : Type u_1} [MeasurableSpace α] (F : α → ℝ → ℝ) (hcm : ∀ (a : α), IsContinuousCompletelyMonotoneOnIoi (F a)) (hmeas : ∀ (n : ℕ), Measurable fun (a : α) => F a ↑n) : ProbabilityTheory.Kernel α NNReal

The Bernstein kernel of a measurable family. The Bernstein representing measures of a measurable family of completely monotone functions assemble into a kernel from the parameter space to ℝ≥0.

Equations

• TauCeti.bernsteinMeasureKernel F hcm hmeas = { toFun := fun (a : α) => TauCeti.bernsteinMeasure (F a), measurable' := ⋯ }

@[simp]

theorem TauCeti.bernsteinMeasureKernel_apply {α : Type u_1} [MeasurableSpace α] {F : α → ℝ → ℝ} (hcm : ∀ (a : α), IsContinuousCompletelyMonotoneOnIoi (F a)) (hmeas : ∀ (n : ℕ), Measurable fun (a : α) => F a ↑n) (a : α) : (bernsteinMeasureKernel F hcm hmeas) a = bernsteinMeasure (F a)

theorem TauCeti.representsLaplace_bernsteinMeasureKernel {α : Type u_1} [MeasurableSpace α] {F : α → ℝ → ℝ} (hcm : ∀ (a : α), IsContinuousCompletelyMonotoneOnIoi (F a)) (hmeas : ∀ (n : ℕ), Measurable fun (a : α) => F a ↑n) (a : α) : RepresentsLaplace ((bernsteinMeasureKernel F hcm hmeas) a) (F a)

Every fibre of the Bernstein kernel represents the corresponding member of the family.

theorem TauCeti.isFiniteKernel_bernsteinMeasureKernel {α : Type u_1} [MeasurableSpace α] {F : α → ℝ → ℝ} (hcm : ∀ (a : α), IsContinuousCompletelyMonotoneOnIoi (F a)) (hmeas : ∀ (n : ℕ), Measurable fun (a : α) => F a ↑n) {C : ℝ} (hC : ∀ (a : α), F a 0 ≤ C) : ProbabilityTheory.IsFiniteKernel (bernsteinMeasureKernel F hcm hmeas)

The Bernstein kernel is finite as soon as the values of the family at 0 are bounded; those values are exactly the fibre masses.

theorem TauCeti.isMarkovKernel_bernsteinMeasureKernel {α : Type u_1} [MeasurableSpace α] {F : α → ℝ → ℝ} (hcm : ∀ (a : α), IsContinuousCompletelyMonotoneOnIoi (F a)) (hmeas : ∀ (n : ℕ), Measurable fun (a : α) => F a ↑n) (hone : ∀ (a : α), F a 0 = 1) : ProbabilityTheory.IsMarkovKernel (bernsteinMeasureKernel F hcm hmeas)

A family of normalized functions gives a Markov kernel.