Parameterized finite-time kernels

This file constructs the finite-dimensional kernel at a fixed strictly ordered time family for a measurably parameterized sub-Markov semigroup. The construction recursively carries the parameter through the augmented state kernel. Fiberwise conservativity is used only for the Markov-kernel property.

The slice theorem identifies evaluation at a parameter and start with the existing nonparameterized finite-time kernel of the fixed-parameter semigroup. No path-space or stochastic-process existence claim is made here.

noncomputable def MarkovProcess.ParameterizedSubMarkovKernelSemigroup.parameterizedFiniteTimeKernel {Theta : Type u_1} {alpha : Type u_2} [MeasurableSpace Theta] [MeasurableSpace alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) {n : ℕ} : FiniteOrderedTimes n → ProbabilityTheory.Kernel (Theta × alpha) (Fin n → alpha)

The jointly measurable finite-time kernel for a parameterized semigroup.

Equations

• One or more equations did not get rendered due to their size.
• P.parameterizedFiniteTimeKernel x_2 = ProbabilityTheory.Kernel.const (Theta × alpha) (MeasureTheory.Measure.dirac (MarkovProcess.FiniteOrderedTimes.emptyPath alpha))

@[simp]

theorem MarkovProcess.ParameterizedSubMarkovKernelSemigroup.parameterizedFiniteTimeKernel_zero {Theta : Type u_1} {alpha : Type u_2} [MeasurableSpace Theta] [MeasurableSpace alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (times : FiniteOrderedTimes 0) : P.parameterizedFiniteTimeKernel times = ProbabilityTheory.Kernel.const (Theta × alpha) (MeasureTheory.Measure.dirac (FiniteOrderedTimes.emptyPath alpha))

@[simp]

theorem MarkovProcess.ParameterizedSubMarkovKernelSemigroup.parameterizedFiniteTimeKernel_succ {Theta : Type u_1} {alpha : Type u_2} [MeasurableSpace Theta] [MeasurableSpace alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) {n : ℕ} (times : FiniteOrderedTimes (n + 1)) : P.parameterizedFiniteTimeKernel times = ((P.augmentedKernel (times 0)).compProd (ProbabilityTheory.Kernel.prodMkLeft (Theta × alpha) (P.parameterizedFiniteTimeKernel times.relativeTail))).mapOfMeasurable (fun (z : (Theta × alpha) × (Fin n → alpha)) => Fin.cons z.1.2 z.2) ⋯

theorem MarkovProcess.ParameterizedSubMarkovKernelSemigroup.isMarkovKernel_parameterizedFiniteTimeKernel {Theta : Type u_1} {alpha : Type u_2} [MeasurableSpace Theta] [MeasurableSpace alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (hP : ∀ (theta : Theta), (P.toSubMarkovKernelSemigroup theta).IsConservative) {n : ℕ} (times : FiniteOrderedTimes n) : ProbabilityTheory.IsMarkovKernel (P.parameterizedFiniteTimeKernel times)

theorem MarkovProcess.ParameterizedSubMarkovKernelSemigroup.parameterizedFiniteTimeKernel_apply {Theta : Type u_1} {alpha : Type u_2} [MeasurableSpace Theta] [MeasurableSpace alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) {n : ℕ} (times : FiniteOrderedTimes n) (theta : Theta) (x : alpha) : (P.parameterizedFiniteTimeKernel times) (theta, x) = ((P.toSubMarkovKernelSemigroup theta).finiteTimeKernel times) x

A fixed-parameter slice is the ordinary finite-time kernel of that semigroup slice.