The Hausdorff--Bernstein--Widder theorem on the open half-line

A function completely monotone on the open half-line (0, ∞) is the Laplace transform of a unique positive measure on ℝ≥0, and that measure need not be finite: the reciprocal t ↦ 1 / t is completely monotone on (0, ∞) and is represented by Lebesgue measure. The finite-measure statement, TauCeti.hausdorff_bernstein_widder, is the strictly stronger conclusion drawn from the strictly stronger hypothesis of continuity up to the boundary point 0; this file records what survives when that boundary hypothesis is dropped.

The representation predicate is TauCeti.RepresentsLaplaceOnIoi, which replaces the finiteness clause of TauCeti.RepresentsLaplace by integrability of the exponential kernel at every positive parameter -- exactly what makes the transform a genuine Bochner integral rather than the junk value of a non-integrable one.

The proof is an exponential-tilt bookkeeping argument on top of Bernstein's theorem. For each a > 0 the shift t ↦ f (t + a) is completely monotone on the closed half-line, so it has a finite representing measure σ a; the tilted measures e^{a p} · σ a are then all equal, and their common value is the representing measure of f itself. Uniqueness runs the tilt backwards: tilting by e^{-p} turns any representing measure into a finite one, where the Laplace transform is already known to determine the measure.

Main declarations

• TauCeti.RepresentsLaplaceOnIoi.unique: at most one measure represents a given function.
• TauCeti.exists_representsLaplaceOnIoi_of_isCompletelyMonotoneOnIoi: the existence half.
• TauCeti.hausdorff_bernstein_widder_onIoi, TauCeti.hausdorff_bernstein_widder_onIoi_existsUnique: the headline equivalence.
• TauCeti.representsLaplaceOnIoi_one_div, TauCeti.isCompletelyMonotoneOnIoi_one_div, and TauCeti.measure_univ_map_toNNReal_volume_restrict_Ioi: the reciprocal t ↦ 1 / t, its representing measure, and the fact that this measure is infinite.

References

D. V. Widder, The Laplace Transform (Princeton, 1941), Chapter IV, Theorem 12a; see also R. Schilling, R. Song, Z. Vondraček, Bernstein Functions (de Gruyter, 2nd ed. 2012), Theorem 1.4 and its remark on the open half-line.

• Roadmap: TauCetiRoadmap/OneParameterSemigroups/README.md, Part B: the warning attached to the Bernstein milestone asks for the open-half-line representation by a possibly infinite measure, with 1 / t = ∫₀^∞ e^{-tx} dx as its example.

Exponential tilts of measures on ℝ≥0

Tilting a measure by the density p ↦ e^{a p} shifts its Laplace transform by a. This is the only device the proofs below need, so it stays private to this file.

Uniqueness

theorem TauCeti.RepresentsLaplaceOnIoi.unique {f : ℝ → ℝ} {μ ν : MeasureTheory.Measure NNReal} (hμ : RepresentsLaplaceOnIoi μ f) (hν : RepresentsLaplaceOnIoi ν f) : μ = ν

A function has at most one open-half-line representing measure. Tilting by e^{-p} reduces the statement to the finite-measure uniqueness theorem TauCeti.Measure.ext_of_forall_laplaceTransform_natCast_eq.

Existence

theorem TauCeti.exists_representsLaplaceOnIoi_of_isCompletelyMonotoneOnIoi {f : ℝ → ℝ} (hf : IsCompletelyMonotoneOnIoi f) : ∃ (μ : MeasureTheory.Measure NNReal), RepresentsLaplaceOnIoi μ f

Existence half of the open-half-line Hausdorff--Bernstein--Widder theorem. A function completely monotone on (0, ∞) is the Laplace transform of a positive -- possibly infinite -- measure on ℝ≥0.

The positive shifts t ↦ f (t + a) are completely monotone on the closed half-line, so Bernstein's theorem gives them finite representing measures σ a; tilting σ a by e^{a p} undoes the shift, and the resulting measure does not depend on a.

The headline equivalence

theorem TauCeti.hausdorff_bernstein_widder_onIoi (f : ℝ → ℝ) : IsCompletelyMonotoneOnIoi f ↔ ∃ (μ : MeasureTheory.Measure NNReal), RepresentsLaplaceOnIoi μ f

The Hausdorff--Bernstein--Widder theorem on the open half-line. A function is completely monotone on (0, ∞) if and only if it is the Laplace transform of a positive measure on ℝ≥0, integrable against the exponential kernel at every positive parameter.

Compare TauCeti.hausdorff_bernstein_widder, which adds continuity at 0 to the hypotheses and gets a finite measure in return.

theorem TauCeti.hausdorff_bernstein_widder_onIoi_existsUnique (f : ℝ → ℝ) : IsCompletelyMonotoneOnIoi f ↔ ∃! μ : MeasureTheory.Measure NNReal, RepresentsLaplaceOnIoi μ f

Unique-existence form of the open-half-line Hausdorff--Bernstein--Widder theorem.

The reciprocal, and an infinite representing measure

t ↦ 1 / t is the standard witness that the open-half-line theorem cannot return a finite measure: its representing measure is Lebesgue measure on (0, ∞), pushed to ℝ≥0.

theorem TauCeti.measure_univ_map_toNNReal_volume_restrict_Ioi : (MeasureTheory.Measure.map Real.toNNReal (MeasureTheory.volume.restrict (Set.Ioi 0))) Set.univ = ⊤

Lebesgue measure on (0, ∞), pushed forward to ℝ≥0, is infinite.

theorem TauCeti.representsLaplaceOnIoi_one_div : RepresentsLaplaceOnIoi (MeasureTheory.Measure.map Real.toNNReal (MeasureTheory.volume.restrict (Set.Ioi 0))) fun (t : ℝ) => 1 / t

The reciprocal is the Laplace transform of Lebesgue measure: 1 / t = ∫₀^∞ e^{-tx} dx for t > 0. By TauCeti.measure_univ_map_toNNReal_volume_restrict_Ioi the representing measure is infinite, so this is genuinely outside the reach of the finite-measure theorem.

theorem TauCeti.isCompletelyMonotoneOnIoi_one_div : IsCompletelyMonotoneOnIoi fun (t : ℝ) => 1 / t

The reciprocal is completely monotone on (0, ∞), read off from its Laplace representation.