Positive definiteness of Laplace--Fourier transforms

A finite positive measure on ℝ≥0 × V has a bounded, continuous, semigroup-group positive-definite Laplace--Fourier transform. This is the easy direction of the Berg--Christensen--Ressel representation theorem: each point of the measure supplies the positive-definite atom

(t, a) ↦ exp (-t p) * exp (-2πi⟪a, q⟫),

and integration preserves its finite quadratic-form inequalities. Continuity follows from dominated convergence, since every atom has norm at most one.

This advances TauCetiRoadmap/OneParameterSemigroups/README.md, Part C, Milestone 2 ("BCR semigroup--Bochner"). Together with the transform definition and uniqueness theorem, it supplies the complete measure-to-function direction and leaves the representation of an arbitrary bounded continuous positive-definite function as the remaining existence problem.

Main declarations

• TauCeti.norm_laplaceFourierTransform_le: the transform is bounded by the total mass.
• TauCeti.continuous_laplaceFourierTransform: a finite measure's transform is continuous.
• TauCeti.isSemigroupGroupPD_laplaceFourierTransform: a finite measure's transform is semigroup-group positive definite.
• TauCeti.RepresentsLaplaceFourier.isSemigroupGroupPD and TauCeti.RepresentsLaplaceFourier.continuous: every represented function inherits the two structural properties.

References

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

theorem TauCeti.norm_laplaceFourierTransform_le {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) [MeasureTheory.IsFiniteMeasure μ] (x : NNReal × V) : ‖laplaceFourierTransform μ x‖ ≤ μ.real Set.univ

The Laplace--Fourier transform of a finite measure is bounded in norm by the measure's total mass. In particular it is a bounded function, as required in the BCR representation theorem.

theorem TauCeti.continuous_laplaceFourierTransform {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [OpensMeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) [MeasureTheory.IsFiniteMeasure μ] : Continuous (laplaceFourierTransform μ)

The Laplace--Fourier transform of a finite measure is continuous. The integrands are jointly continuous in the evaluation variable and uniformly dominated by the integrable constant one.

theorem TauCeti.isSemigroupGroupPD_laplaceFourierTransform {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [OpensMeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) [MeasureTheory.IsFiniteMeasure μ] : IsSemigroupGroupPD (laplaceFourierTransform μ)

The Laplace--Fourier transform of a finite positive measure is semigroup-group positive definite. This is the positivity half of the measure-to-function direction of BCR.

theorem TauCeti.RepresentsLaplaceFourier.isSemigroupGroupPD {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [OpensMeasurableSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} (h : RepresentsLaplaceFourier μ F) : IsSemigroupGroupPD F

A function represented by a finite measure is semigroup-group positive definite.

theorem TauCeti.RepresentsLaplaceFourier.continuous {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [OpensMeasurableSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} (h : RepresentsLaplaceFourier μ F) : Continuous F

A function represented by a finite measure is continuous.

theorem TauCeti.RepresentsLaplaceFourier.norm_le_mass {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} (h : RepresentsLaplaceFourier μ F) (x : NNReal × V) : ‖F x‖ ≤ μ.real Set.univ

A function represented by μ is uniformly bounded in norm by the total mass of μ.