Documentation

TauCeti.Analysis.PositiveDefinite.SemigroupGroup.FourierLaplace.Kernel

Berg--Christensen--Ressel representing measures as time kernels #

Let V be a finite-dimensional real inner-product space. A measure μ on V together with a kernel κ from V to ℝ≥0 assembles into a measure TauCeti.swapCompProd μ κ on ℝ≥0 × V, and conversely every finite measure on ℝ≥0 × V admits such a disintegration over its spatial marginal, the Markov kernel being unique only up to equality almost everywhere for that marginal. That assembly is general measure theory and lives in TauCeti.Probability.Kernel.Composition.Swap; this file reads the Berg--Christensen--Ressel representation through it.

The point is that the spatial slice of swapCompProd μ κ at time t is computed by a fibrewise Laplace transform: it is μ weighted by the density q ↦ ∫⁻ p, exp (-t p) ∂(κ q) (TauCeti.spatialSlice_swapCompProd). Since a finite measure on ℝ≥0 × V represents a function F exactly when its spatial slices are the Bochner measures of the time slices of F (TauCeti.representsLaplaceFourier_iff_forall_spatialSlice_eq), and since those Bochner measures decrease in time and are therefore all absolutely continuous with respect to the one at time 0 (TauCeti.bochnerMeasure_timeSlice_absolutelyContinuous), the existence half of the representation theorem becomes a fibrewise Bernstein problem: find a Markov kernel whose fibrewise Laplace transforms are the Radon--Nikodym densities d(bochnerMeasure (F (t, ·))) / d(bochnerMeasure (F (0, ·))) (TauCeti.representsLaplaceFourier_swapCompProd_of_ae_rnDeriv). The reduction is exact: TauCeti.exists_representsLaplaceFourier_iff_exists_timeKernel states it as an equivalence, so nothing is lost in passing from the measure to the kernel.

The time-regularity input that a fibrewise Bernstein argument consumes — antitonicity, the resulting absolute continuity, continuity and alternating finite differences of the slab masses — is in TauCeti.Analysis.PositiveDefinite.SemigroupGroup.Time.Slice.Measure.

Main declarations #

References #

The spatial slices of a measure assembled from a spatial measure and a time kernel #

source
@[simp]
theorem TauCeti.spatialSlice_swapCompProd {V : Type u_1} [MeasurableSpace V] (μ : MeasureTheory.Measure V) [MeasureTheory.SFinite μ] (κ : ProbabilityTheory.Kernel V NNReal) [ProbabilityTheory.IsSFiniteKernel κ] (t : NNReal) :
spatialSlice (swapCompProd μ κ) t = μ.withDensity (κ.laplaceTransform t)

The spatial slices of an assembled measure are its fibrewise Laplace transforms. Weighting by exp (-t p) and integrating out the time coordinate leaves the spatial measure weighted by the fibrewise Laplace transform of the kernel.

The reduction of the representation problem to a kernel problem #

source
theorem TauCeti.representsLaplaceFourier_swapCompProd {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : NNReal × V → ℂ} (hFpd : ∀ (t : NNReal), IsPositiveDefiniteSub fun (a : V) => F (t, a)) (hFcont : ∀ (t : NNReal), Continuous fun (a : V) => F (t, a)) (κ : ProbabilityTheory.Kernel V NNReal) [ProbabilityTheory.IsSFiniteKernel κ] (hκ : ∀ (t : NNReal), (bochnerMeasure fun (a : V) => F (0, a)).withDensity (κ.laplaceTransform t) = bochnerMeasure fun (a : V) => F (t, a)) :
RepresentsLaplaceFourier (swapCompProd (bochnerMeasure fun (a : V) => F (0, a)) κ) F

A time kernel with the prescribed fibrewise Laplace transforms represents F. If the fibrewise Laplace transform of κ at every time t is a density of the spatial Bochner measure at t against the one at time 0, then assembling κ over that time-0 measure produces a Berg--Christensen--Ressel representing measure for F. Only the time slices of F are constrained: positive definiteness and continuity are what make the spatial Bochner measures represent them.

source
theorem TauCeti.representsLaplaceFourier_swapCompProd_of_ae_rnDeriv {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)) (κ : ProbabilityTheory.Kernel V NNReal) [ProbabilityTheory.IsSFiniteKernel κ] (hκ : ∀ (t : NNReal), κ.laplaceTransform t =ᵐ[bochnerMeasure fun (a : V) => F (0, a)] (bochnerMeasure fun (a : V) => F (t, a)).rnDeriv (bochnerMeasure fun (a : V) => F (0, a))) :
RepresentsLaplaceFourier (swapCompProd (bochnerMeasure fun (a : V) => F (0, a)) κ) F

The same criterion, phrased with Radon--Nikodym derivatives. A bounded continuous positive-definite F is represented as soon as some s-finite kernel has, at every time, a fibrewise Laplace transform equal almost everywhere to the Radon--Nikodym derivative of the spatial Bochner measure at that time against the one at time 0. This is the exact form in which a fibrewise Bernstein argument closes the existence half.

source
theorem TauCeti.exists_representsLaplaceFourier_iff_exists_timeKernel {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : NNReal × V → ℂ} (hFpd : ∀ (t : NNReal), IsPositiveDefiniteSub fun (a : V) => F (t, a)) (hFcont : ∀ (t : NNReal), Continuous fun (a : V) => F (t, a)) :
(∃ (μ : MeasureTheory.Measure (NNReal × V)), RepresentsLaplaceFourier μ F) ↔ ∃ (κ : ProbabilityTheory.Kernel V NNReal), ProbabilityTheory.IsMarkovKernel κ ∧ ∀ (t : NNReal), (bochnerMeasure fun (a : V) => F (0, a)).withDensity (κ.laplaceTransform t) = bochnerMeasure fun (a : V) => F (t, a)

The existence half of the Berg--Christensen--Ressel representation is a kernel problem. A function on ℝ≥0 × V whose time slices are continuous and positive-definite has a representing finite measure if and only if there is a Markov kernel from V to ℝ≥0 whose fibrewise Laplace transform at each time t is a density of the spatial Bochner measure at time t against the one at time 0.

The forward direction disintegrates a representing measure over its spatial marginal, which is the time-0 Bochner measure; the backward direction assembles the kernel into a measure and checks its spatial slices.