Spatial slices of a measure on ℝ≥0 × V

The Berg--Christensen--Ressel representation writes a bounded continuous positive-definite function on the involutive semigroup ℝ≥0 × V as the Laplace--Fourier transform

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

of a finite measure μ on ℝ≥0 × V. Freezing the time variable at t leaves a spatial representation: weighting μ by the Laplace factor exp (-t p) and forgetting the time coordinate produces a finite measure on V whose Fourier-convention transform is the time slice F (t, ·). This file develops that slicing operation, TauCeti.spatialSlice, and the companion time marginal of a slab ℝ≥0 × B.

The two structural results are the necessary conditions a representing measure satisfies, each phrased against the representation theorem it consumes:

• by Bochner's theorem on V, each spatial slice of a representing measure is the Bochner measure of the corresponding time slice of F, and conversely a finite measure whose spatial slices are those Bochner measures represents F (TauCeti.representsLaplaceFourier_iff_forall_spatialSlice_eq);
• the mass a spatial slice assigns to a fixed measurable set is, as a function of the time, the Laplace transform of a finite measure on ℝ≥0 (TauCeti.representsLaplace_timeMarginal).

Together they say what a representing measure has to look like: its slices are prescribed by Bochner's theorem, and the resulting set functions t ↦ μ_t B are Laplace transforms. The existence half of the Berg--Christensen--Ressel theorem has to reverse both implications, and the criterion above is what it discharges last.

Main declarations

• TauCeti.spatialSlice: the Laplace-weighted spatial marginal of a measure on ℝ≥0 × V.
• TauCeti.spatialSlice_apply, TauCeti.spatialSlice_real_apply: the mass of a measurable set under a spatial slice, as a lower and as a Bochner integral over the corresponding slab.
• TauCeti.integral_fourierAtom_spatialSlice, TauCeti.charFun_spatialSlice: the Fourier-convention transform, and the characteristic function, of a spatial slice are the Laplace--Fourier transform at that time.
• TauCeti.spatialSlice_antitone: spatial slices decrease in time.
• TauCeti.timeMarginal: the time marginal of the slab ℝ≥0 × B.
• TauCeti.RepresentsLaplaceFourier.spatialSlice_eq and TauCeti.representsLaplaceFourier_iff_forall_spatialSlice_eq: the spatial slices of a representing measure are the Bochner measures of the time slices, and this property characterizes the representing measure.
• TauCeti.representsLaplace_timeMarginal: the slab masses of the spatial slices are Laplace transforms.
• TauCeti.Measure.ext_of_forall_spatialSlice_eq: a finite measure on ℝ≥0 × V is determined by its spatial slices.

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"), whose existence half these slices reduce to Bochner's theorem on V.

The spatial slices and the time marginals

noncomputable def TauCeti.spatialSlice {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (t : NNReal) : MeasureTheory.Measure V

The spatial slice of a measure on ℝ≥0 × V at time t: weight by the Laplace factor exp (-t p), then forget the time coordinate. Its characteristic function is the Laplace--Fourier transform at time t, up to the -2π Fourier rescaling (TauCeti.charFun_spatialSlice).

Equations

• TauCeti.spatialSlice μ t = (μ.withDensity fun (y : NNReal × V) => ↑(Real.exp (-↑t * ↑y.1)).toNNReal).snd

instance TauCeti.isFiniteMeasure_spatialSlice {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) [MeasureTheory.IsFiniteMeasure μ] (t : NNReal) : MeasureTheory.IsFiniteMeasure (spatialSlice μ t)

A spatial slice of a finite measure is finite: the Laplace weight is at most 1.

theorem TauCeti.spatialSlice_apply {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (t : NNReal) {B : Set V} (hB : MeasurableSet B) : (spatialSlice μ t) B = ∫⁻ (y : NNReal × V) in Prod.snd ⁻¹' B, ↑(Real.exp (-↑t * ↑y.1)).toNNReal ∂μ

The measure a spatial slice assigns to a measurable set is the Laplace-weighted mass of the corresponding slab.

theorem TauCeti.spatialSlice_apply_eq_ofReal_integral {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) [MeasureTheory.IsFiniteMeasure μ] (t : NNReal) {B : Set V} (hB : MeasurableSet B) : (spatialSlice μ t) B = ENNReal.ofReal (∫ (y : NNReal × V) in Prod.snd ⁻¹' B, Real.exp (-↑t * ↑y.1) ∂μ)

The mass of a measurable set under a spatial slice, as a Bochner integral over the slab.

theorem TauCeti.spatialSlice_real_apply {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) [MeasureTheory.IsFiniteMeasure μ] (t : NNReal) {B : Set V} (hB : MeasurableSet B) : (spatialSlice μ t).real B = ∫ (y : NNReal × V) in Prod.snd ⁻¹' B, Real.exp (-↑t * ↑y.1) ∂μ

The real-valued mass of a measurable set under a spatial slice.

@[simp]

theorem TauCeti.spatialSlice_zero {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) : spatialSlice μ 0 = μ.snd

At time 0 the Laplace weight is trivial, so the spatial slice is the spatial marginal.

@[simp]

theorem TauCeti.spatialSlice_zero_measure {V : Type u_1} [MeasurableSpace V] (t : NNReal) : spatialSlice 0 t = 0

Every spatial slice of the zero measure is the zero measure.

theorem TauCeti.spatialSlice_antitone {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) : Antitone (spatialSlice μ)

The spatial slices decrease in time: the Laplace weight exp (-t p) is nonincreasing in t at every frequency p ≥ 0.

theorem TauCeti.spatialSlice_le_snd {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (t : NNReal) : spatialSlice μ t ≤ μ.snd

Every spatial slice is dominated by the spatial marginal.

noncomputable def TauCeti.timeMarginal {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (B : Set V) : MeasureTheory.Measure NNReal

The time marginal of the slab ℝ≥0 × B, as a measure on ℝ≥0. It is the measure whose Laplace transform records the masses t ↦ (spatialSlice μ t).real B (TauCeti.representsLaplace_timeMarginal).

Equations

• TauCeti.timeMarginal μ B = (μ.restrict (Prod.snd ⁻¹' B)).fst

instance TauCeti.isFiniteMeasure_timeMarginal {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) [MeasureTheory.IsFiniteMeasure μ] (B : Set V) : MeasureTheory.IsFiniteMeasure (timeMarginal μ B)

A time marginal of a finite measure is finite.

theorem TauCeti.integral_exp_timeMarginal {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (B : Set V) (t : ℝ) : ∫ (p : NNReal), Real.exp (-t * ↑p) ∂timeMarginal μ B = ∫ (y : NNReal × V) in Prod.snd ⁻¹' B, Real.exp (-t * ↑y.1) ∂μ

Integrating the Laplace kernel against a time marginal integrates it over the slab.

theorem TauCeti.timeMarginal_apply {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) {A : Set NNReal} (hA : MeasurableSet A) (B : Set V) : (timeMarginal μ B) A = μ (A ×ˢ B)

A time marginal evaluates to the mass of the corresponding rectangle.

theorem TauCeti.representsLaplace_timeMarginal {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure (NNReal × V)) [MeasureTheory.IsFiniteMeasure μ] {B : Set V} (hB : MeasurableSet B) : RepresentsLaplace (timeMarginal μ B) fun (t : ℝ) => (spatialSlice μ t.toNNReal).real B

The slab masses of the spatial slices are Laplace transforms. For a measurable B ⊆ V, the function t ↦ (spatialSlice μ t).real B on [0, ∞) is the Laplace transform of the finite measure timeMarginal μ B on ℝ≥0. This is the time-direction necessary condition on a Berg--Christensen--Ressel representing measure.

theorem TauCeti.Measure.ext_of_forall_spatialSlice_eq {V : Type u_1} [MeasurableSpace V] {μ ν : MeasureTheory.Measure (NNReal × V)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hslice : ∀ (t : NNReal), spatialSlice μ t = spatialSlice ν t) : μ = ν

A finite measure on ℝ≥0 × V is determined by its spatial slices. Testing a slice against a measurable set B leaves the Laplace transform of the finite time marginal of the slab ℝ≥0 × B (TauCeti.representsLaplace_timeMarginal), and Laplace determinacy pins that marginal down; measurable rectangles then form a π-system generating the product σ-algebra.

Together with TauCeti.representsLaplaceFourier_iff_forall_spatialSlice_eq, this reduces the Berg--Christensen--Ressel representation to the prescribed-slices problem: the representing measure is the unique finite measure whose spatial slices are the Bochner measures of the time slices.

Integration against a spatial slice

theorem TauCeti.integral_spatialSlice {V : Type u_1} [TopologicalSpace V] [MeasurableSpace V] [BorelSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (t : NNReal) {f : V → ℂ} (hf : Continuous f) : ∫ (q : V), f q ∂spatialSlice μ t = ∫ (y : NNReal × V), ↑(Real.exp (-↑t * ↑y.1)) * f y.2 ∂μ

Integration against a spatial slice reinstates the Laplace weight.

theorem TauCeti.integral_fourierAtom_spatialSlice {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (t : NNReal) (a : V) : ∫ (q : V), fourierAtom a q ∂spatialSlice μ t = laplaceFourierTransform μ (t, a)

The Fourier-convention transform of a spatial slice is the Laplace--Fourier transform. Freezing the time variable at t turns the two-variable transform into the spatial transform of the slice at t.

theorem TauCeti.charFun_spatialSlice {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] (μ : MeasureTheory.Measure (NNReal × V)) (t : NNReal) (a : V) : MeasureTheory.charFun (spatialSlice μ t) ((-2 * Real.pi) • a) = laplaceFourierTransform μ (t, a)

The characteristic function of a spatial slice is the Laplace--Fourier transform, after the -2π rescaling that converts Mathlib's Fourier convention into the characteristic-function convention.

The spatial slices of a representing measure

theorem TauCeti.RepresentsLaplaceFourier.spatialSlice_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} (h : RepresentsLaplaceFourier μ F) (t : NNReal) : spatialSlice μ t = bochnerMeasure fun (a : V) => F (t, a)

The spatial slices of a Berg--Christensen--Ressel representing measure are the Bochner measures of the time slices. Bochner's theorem on V has a unique representing measure, and the spatial slice at t represents the time slice F (t, ·), so the two coincide.

theorem TauCeti.representsLaplaceFourier_of_forall_spatialSlice_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} (hμ : MeasureTheory.IsFiniteMeasure μ) (hFpd : ∀ (t : NNReal), IsPositiveDefiniteSub fun (a : V) => F (t, a)) (hFcont : ∀ (t : NNReal), Continuous fun (a : V) => F (t, a)) (h : ∀ (t : NNReal), spatialSlice μ t = bochnerMeasure fun (a : V) => F (t, a)) : RepresentsLaplaceFourier μ F

The converse. A finite measure whose spatial slices are the Bochner measures of the continuous positive-definite time slices of F represents F. Positive definiteness and continuity enter through Bochner's theorem, which is what makes those Bochner measures represent the slices.

theorem TauCeti.representsLaplaceFourier_iff_forall_spatialSlice_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} (hμ : MeasureTheory.IsFiniteMeasure μ) (hFpd : ∀ (t : NNReal), IsPositiveDefiniteSub fun (a : V) => F (t, a)) (hFcont : ∀ (t : NNReal), Continuous fun (a : V) => F (t, a)) : RepresentsLaplaceFourier μ F ↔ ∀ (t : NNReal), spatialSlice μ t = bochnerMeasure fun (a : V) => F (t, a)

The slice criterion for the Berg--Christensen--Ressel representation. A finite measure on ℝ≥0 × V represents F by its Laplace--Fourier transform if and only if each of its spatial slices is the Bochner measure of the corresponding continuous positive-definite time slice of F. The existence half of the representation theorem is exactly the problem of producing a finite measure with these prescribed slices.

theorem TauCeti.RepresentsLaplaceFourier.spatialSlice_real_univ {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} (h : RepresentsLaplaceFourier μ F) (t : NNReal) : (spatialSlice μ t).real Set.univ = (F (t, 0)).re

The total mass of the spatial slice at t is the value of F on the time axis.

theorem TauCeti.RepresentsLaplaceFourier.representsLaplace_bochnerMeasure {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure (NNReal × V)} {F : NNReal × V → ℂ} (h : RepresentsLaplaceFourier μ F) {B : Set V} (hB : MeasurableSet B) : RepresentsLaplace (timeMarginal μ B) fun (t : ℝ) => (bochnerMeasure fun (a : V) => F (t.toNNReal, a)).real B

The Bochner measures of the time slices have Laplace-transform masses. Reading TauCeti.representsLaplace_timeMarginal through the identification of the spatial slices with the Bochner measures: for a represented F and a measurable B ⊆ V, the mass that the Bochner measure of the time slice F (t, ·) assigns to B is, as a function of t, the Laplace transform of a finite measure on ℝ≥0.