Compact-test transport for finite-set kernels

This file identifies the increasing-coordinate representation of a finite set with its ordinary function space by a homeomorphism. It transports compactly supported tests across that homeomorphism and rewrites their finite-set-kernel integrals as finite-time-kernel integrals.

Strong measurability of a compactly supported test follows from the shared uniform coordinate- polynomial approximations. This avoids adding an OpensMeasurableSpace assumption on the finite product. These declarations are finite-dimensional infrastructure; no statement about path space is proved here.

noncomputable def MarkovProcess.SubMarkovKernelSemigroup.orderedPathToFiniteSetHomeomorph {alpha : Type u_1} [TopologicalSpace alpha] (I : Finset NNReal) : (Fin I.card → alpha) ≃ₜ (↥I → alpha)

The increasing-coordinate representation of paths on a finite time set, as a homeomorphism.

Equations

• MarkovProcess.SubMarkovKernelSemigroup.orderedPathToFiniteSetHomeomorph I = Homeomorph.piCongrLeft (I.orderIsoOfFin ⋯).toEquiv

@[simp]

theorem MarkovProcess.SubMarkovKernelSemigroup.orderedPathToFiniteSetHomeomorph_apply {alpha : Type u_1} [TopologicalSpace alpha] (I : Finset NNReal) (path : Fin I.card → alpha) : (orderedPathToFiniteSetHomeomorph I) path = orderedPathToFiniteSet I path

The ordered-coordinate homeomorphism has underlying function orderedPathToFiniteSet.

noncomputable def MarkovProcess.SubMarkovKernelSemigroup.pullbackFiniteSetCompactTest {alpha : Type u_1} [TopologicalSpace alpha] (I : Finset NNReal) (f : CompactlySupportedContinuousMap (↥I → alpha) ℝ) : CompactlySupportedContinuousMap (Fin I.card → alpha) ℝ

Pull a compactly supported test on finite-set coordinates back to increasing coordinates.

Equations

• MarkovProcess.SubMarkovKernelSemigroup.pullbackFiniteSetCompactTest I f = f.comp (MarkovProcess.SubMarkovKernelSemigroup.orderedPathToFiniteSetHomeomorph I).toCocompactMap

@[simp]

theorem MarkovProcess.SubMarkovKernelSemigroup.pullbackFiniteSetCompactTest_apply {alpha : Type u_1} [TopologicalSpace alpha] (I : Finset NNReal) (f : CompactlySupportedContinuousMap (↥I → alpha) ℝ) (path : Fin I.card → alpha) : (pullbackFiniteSetCompactTest I f) path = f (orderedPathToFiniteSet I path)

Evaluation of a compact test pulled back to increasing coordinates.

theorem MarkovProcess.SubMarkovKernelSemigroup.integral_map_orderedPathToFiniteSet {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [LocallyCompactSpace alpha] [T2Space alpha] (I : Finset NNReal) (f : CompactlySupportedContinuousMap (↥I → alpha) ℝ) (mu : MeasureTheory.Measure (Fin I.card → alpha)) : ∫ (y : ↥I → alpha), f y ∂MeasureTheory.Measure.map (orderedPathToFiniteSet I) mu = ∫ (path : Fin I.card → alpha), (pullbackFiniteSetCompactTest I f) path ∂mu

Integration against the mapped ordered-coordinate law equals integration of the pulled-back compact test.

theorem MarkovProcess.SubMarkovKernelSemigroup.integral_finiteSetKernel_eq_integral_pullbackFiniteSetCompactTest {alpha : Type u_1} [TopologicalSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [LocallyCompactSpace alpha] [T2Space alpha] (P : SubMarkovKernelSemigroup alpha) (I : Finset NNReal) (f : CompactlySupportedContinuousMap (↥I → alpha) ℝ) (x : alpha) : ∫ (y : ↥I → alpha), f y ∂(P.finiteSetKernel I) x = ∫ (path : Fin I.card → alpha), (pullbackFiniteSetCompactTest I f) path ∂(P.finiteTimeKernel (finiteSetTimes I)) x

A compact-test integral against finiteSetKernel is the corresponding pulled-back integral against finiteTimeKernel.