Hausdorff--Bernstein--Widder theorem

This file proves the finite-measure form of the Hausdorff--Bernstein--Widder theorem for completely monotone functions on the closed half-line: a function is continuous on [0, ∞) and completely monotone on (0, ∞) if and only if it is the Laplace transform of a (unique) finite positive measure on ℝ≥0.

The hard direction is a direct application of the finite-difference representation theorem in FiniteDifference/Laplace.lean: derivative complete monotonicity implies the mixed-difference condition, and continuity on [0, ∞) supplies right-continuity at zero. The easy direction and uniqueness live in Laplace/Representation.lean.

Main declarations

• TauCeti.exists_representsLaplace_of_isContinuousCompletelyMonotoneOnIoi
• TauCeti.hausdorff_bernstein_widder, TauCeti.hausdorff_bernstein_widder_existsUnique
• TauCeti.bernsteinMeasure: the canonical representing measure, with its uniqueness, total-mass, and algebraic API.

References

The finite-measure representation is the Hausdorff--Bernstein--Widder theorem, after S. Bernstein (1928) and D. V. Widder, The Laplace Transform, Chapter IV.

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

theorem TauCeti.exists_representsLaplace_of_isContinuousCompletelyMonotoneOnIoi {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) : ∃ (μ : MeasureTheory.Measure NNReal), RepresentsLaplace μ f

Existence half of the Hausdorff--Bernstein--Widder theorem: a function continuous on [0, ∞) and completely monotone on (0, ∞) is the Laplace transform of a finite positive measure on ℝ≥0.

Headline theorem

theorem TauCeti.hausdorff_bernstein_widder (f : ℝ → ℝ) : IsContinuousCompletelyMonotoneOnIoi f ↔ ∃ (μ : MeasureTheory.Measure NNReal), RepresentsLaplace μ f

Hausdorff--Bernstein--Widder theorem, finite-measure version on ℝ≥0.

A function is continuous on [0, ∞) and completely monotone on (0, ∞) if and only if it is the Laplace transform of a finite positive measure on ℝ≥0.

theorem TauCeti.hausdorff_bernstein_widder_existsUnique (f : ℝ → ℝ) : IsContinuousCompletelyMonotoneOnIoi f ↔ ∃! μ : MeasureTheory.Measure NNReal, RepresentsLaplace μ f

Unique-existence form of the Hausdorff--Bernstein--Widder theorem.

The canonical representing measure

noncomputable def TauCeti.bernsteinMeasure (f : ℝ → ℝ) : MeasureTheory.Measure NNReal

The Bernstein representing measure of f: the unique finite measure on ℝ≥0 whose Laplace transform is f on [0, ∞), when f has one, and the zero measure otherwise.

By TauCeti.hausdorff_bernstein_widder a representing measure exists exactly when f is continuous on [0, ∞) and completely monotone on (0, ∞).

Equations

• TauCeti.bernsteinMeasure f = if h : ∃ (μ : MeasureTheory.Measure NNReal), TauCeti.RepresentsLaplace μ f then h.choose else 0

theorem TauCeti.bernsteinMeasure_eq_zero_of_not {f : ℝ → ℝ} (h : ¬∃ (μ : MeasureTheory.Measure NNReal), RepresentsLaplace μ f) : bernsteinMeasure f = 0

Outside the hypotheses of the Hausdorff--Bernstein--Widder theorem the Bernstein measure is 0.

theorem TauCeti.representsLaplace_bernsteinMeasure {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) : RepresentsLaplace (bernsteinMeasure f) f

The Bernstein measure represents its function.

instance TauCeti.isFiniteMeasure_bernsteinMeasure (f : ℝ → ℝ) : MeasureTheory.IsFiniteMeasure (bernsteinMeasure f)

The Bernstein measure of any function is finite: for a represented function this is the finiteness of its representing measure, and otherwise the measure is 0.

theorem TauCeti.eq_bernsteinMeasure {f : ℝ → ℝ} (μ : MeasureTheory.Measure NNReal) (hμ : RepresentsLaplace μ f) : μ = bernsteinMeasure f

Uniqueness of the Bernstein measure. Any finite measure representing f by its Laplace transform is the Bernstein measure of f. No hypothesis on f is needed: a represented function is automatically continuous and completely monotone.

theorem TauCeti.laplaceTransform_bernsteinMeasure {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) {t : ℝ} (ht : 0 ≤ t) : laplaceTransform (bernsteinMeasure f) t = f t

The Laplace transform of the Bernstein measure recovers the function on [0, ∞).

@[simp]

theorem TauCeti.bernsteinMeasure_real_univ {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) : (bernsteinMeasure f).real Set.univ = f 0

The total mass of the Bernstein measure is the value of the function at 0.

@[simp]

theorem TauCeti.bernsteinMeasure_univ {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) : (bernsteinMeasure f) Set.univ = ENNReal.ofReal (f 0)

The total mass of the Bernstein measure, as an extended nonnegative real.

theorem TauCeti.isProbabilityMeasure_bernsteinMeasure {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) (hf0 : f 0 = 1) : MeasureTheory.IsProbabilityMeasure (bernsteinMeasure f)

A function with total mass 1 has a probability measure for its Bernstein measure.

@[simp]

theorem TauCeti.bernsteinMeasure_zero : (bernsteinMeasure fun (x : ℝ) => 0) = 0

The Bernstein measure of the zero function is the zero measure.

theorem TauCeti.bernsteinMeasure_add {f g : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) (hg : IsContinuousCompletelyMonotoneOnIoi g) : bernsteinMeasure (f + g) = bernsteinMeasure f + bernsteinMeasure g

The Bernstein measure turns sums of functions into sums of measures.

theorem TauCeti.bernsteinMeasure_const_mul {f : ℝ → ℝ} (hf : IsContinuousCompletelyMonotoneOnIoi f) (c : NNReal) : (bernsteinMeasure fun (t : ℝ) => ↑c * f t) = ↑c • bernsteinMeasure f

The Bernstein measure turns nonnegative scalar multiples of functions into scalar multiples of measures.