The Berg--Christensen--Ressel representation theorem

A bounded continuous positive-definite function on the involutive semigroup ℝ≥0 × V, with V a finite-dimensional real inner-product space, is the Laplace--Fourier transform of a unique finite measure on ℝ≥0 × V. This file proves the existence half and packages it with the uniqueness half of TauCeti.Analysis.PositiveDefinite.SemigroupGroup.FourierLaplace.Uniqueness into the equivalence TauCeti.bcr_semigroup_bochner.

Every ingredient is already in place, and the proof here is the assembly.

• Freezing the time variable and applying Bochner's theorem on V turns F into a family of finite spatial measures, and the representation holds exactly when that family is the family of Laplace-weighted spatial slices of a single measure (TauCeti.representsLaplaceFourier_iff_forall_spatialSlice_eq). Disintegrating over the spatial marginal reduces this to producing a kernel from V to ℝ≥0 whose fibrewise Laplace transforms are the densities of the spatial measures against the one at time 0 (TauCeti.exists_representsLaplaceFourier_iff_exists_timeKernel).
• Almost every fibre of TauCeti.timeSliceDensity, the right-continuous version of that family of densities, is a completely monotone function of time (TauCeti.ae_isContinuousCompletelyMonotoneOnIoi_timeSliceDensity), normalized at time 0.
• The Hausdorff--Bernstein--Widder theorem therefore represents each such fibre by a finite measure on ℝ≥0, and those measures depend measurably on the fibre, so they assemble into TauCeti.bernsteinMeasureKernel.

The only step needing care is that "almost every fibre" is not "every fibre", while a kernel must be defined at every point: the density is corrected to 0 on a measurable null set containing the exceptional fibres, which changes neither the Bernstein measures elsewhere nor the resulting representation.

Main declarations

• TauCeti.exists_representsLaplaceFourier: the existence half of the Berg--Christensen--Ressel representation.
• TauCeti.bcr_semigroup_bochner: the representation theorem as an equivalence, with uniqueness.

References

• C. Berg, J. P. R. Christensen, P. Ressel, Harmonic Analysis on Semigroups (GTM 100, 1984), Theorem 4.1.13.

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

theorem TauCeti.exists_representsLaplaceFourier {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : NNReal × V → ℂ} (hFpd : IsSemigroupGroupPD F) (hFcont : Continuous F) (hFbdd : Bornology.IsBounded (Set.range F)) : ∃ (μ : MeasureTheory.Measure (NNReal × V)), RepresentsLaplaceFourier μ F

The existence half of the Berg--Christensen--Ressel representation theorem. A bounded continuous positive-definite function on the involutive semigroup ℝ≥0 × V is the Laplace--Fourier transform of a finite measure on ℝ≥0 × V.

The representing measure is assembled from the spatial Bochner measure at time 0 and the Bernstein measures of the fibres of TauCeti.timeSliceDensity.

theorem TauCeti.bcr_semigroup_bochner {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (F : NNReal × V → ℂ) : IsSemigroupGroupPD F ∧ Continuous F ∧ Bornology.IsBounded (Set.range F) ↔ ∃! μ : MeasureTheory.Measure (NNReal × V), RepresentsLaplaceFourier μ F

The Berg--Christensen--Ressel representation theorem (Berg--Christensen--Ressel 4.1.13). A function on the involutive semigroup ℝ≥0 × V, for V a finite-dimensional real inner-product space, is positive definite, continuous and bounded if and only if it is the Laplace--Fourier transform of a unique finite measure on ℝ≥0 × V:

F (t, a) = ∫ (p, q), exp (-t p) * exp (-2πi⟪a, q⟫) dμ (p, q).

The forward direction is TauCeti.exists_representsLaplaceFourier together with the transform injectivity of TauCeti.RepresentsLaplaceFourier.unique; the converse direction is the elementary fact that such a transform is positive definite, continuous, and bounded by the total mass.