Documentation

LeanPool.MarkovProcess.MarkovProcess.Parameterized.FiniteTimeProjectiveFamily

Parameterized finite-set finite-time kernels #

This file reindexes parameterized finite-time kernels by finite sets of times. It proves exact agreement with the ordinary finite-set kernel at every fixed parameter and starting state, and derives projectivity under fiberwise conservativity. It does not construct a projective-limit measure or a stochastic process.

source
noncomputable def MarkovProcess.ParameterizedSubMarkovKernelSemigroup.parameterizedFiniteSetKernel {Theta : Type u_1} {alpha : Type u_2} [MeasurableSpace Theta] [MeasurableSpace alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (I : Finset NNReal) :
ProbabilityTheory.Kernel (Theta × alpha) (↥I → alpha)

The jointly measurable finite-time kernel indexed by a finite set of times.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MarkovProcess.ParameterizedSubMarkovKernelSemigroup.parameterizedFiniteSetKernel_eq_map {Theta : Type u_1} {alpha : Type u_2} [MeasurableSpace Theta] [MeasurableSpace alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (I : Finset NNReal) :
    P.parameterizedFiniteSetKernel I = (P.parameterizedFiniteTimeKernel (SubMarkovKernelSemigroup.finiteSetTimes I)).map (SubMarkovKernelSemigroup.orderedPathToFiniteSet I)

    The parameterized finite-set kernel agrees with the ordinary kernel map.

    source
    theorem MarkovProcess.ParameterizedSubMarkovKernelSemigroup.parameterizedFiniteSetKernel_apply {Theta : Type u_1} {alpha : Type u_2} [MeasurableSpace Theta] [MeasurableSpace alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (I : Finset NNReal) (theta : Theta) (x : alpha) :
    (P.parameterizedFiniteSetKernel I) (theta, x) = ((P.toSubMarkovKernelSemigroup theta).finiteSetKernel I) x

    At a fixed parameter and start, the parameterized finite-set kernel is the ordinary one.

    source
    theorem MarkovProcess.ParameterizedSubMarkovKernelSemigroup.isMarkovKernel_parameterizedFiniteSetKernel {Theta : Type u_1} {alpha : Type u_2} [MeasurableSpace Theta] [MeasurableSpace alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (hP : ∀ (theta : Theta), (P.toSubMarkovKernelSemigroup theta).IsConservative) (I : Finset NNReal) :
    ProbabilityTheory.IsMarkovKernel (P.parameterizedFiniteSetKernel I)

    Fiberwise conservativity makes every parameterized finite-set kernel Markov.

    source
    theorem MarkovProcess.ParameterizedSubMarkovKernelSemigroup.parameterizedFiniteSetKernel_map_restrict₂ {Theta : Type u_1} {alpha : Type u_2} [MeasurableSpace Theta] [MeasurableSpace alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (hP : ∀ (theta : Theta), (P.toSubMarkovKernelSemigroup theta).IsConservative) {I J : Finset NNReal} (hJI : J ⊆ I) :
    P.parameterizedFiniteSetKernel J = (P.parameterizedFiniteSetKernel I).map (Finset.restrict₂ hJI)

    Restriction along an inclusion gives the kernel on the smaller finite time set.

    source
    theorem MarkovProcess.ParameterizedSubMarkovKernelSemigroup.isProjectiveMeasureFamily_parameterizedFiniteSetKernel_apply {Theta : Type u_1} {alpha : Type u_2} [MeasurableSpace Theta] [MeasurableSpace alpha] (P : ParameterizedSubMarkovKernelSemigroup Theta alpha) (hP : ∀ (theta : Theta), (P.toSubMarkovKernelSemigroup theta).IsConservative) (theta : Theta) (x : alpha) :
    MeasureTheory.IsProjectiveMeasureFamily fun (I : Finset NNReal) => (P.parameterizedFiniteSetKernel I) (theta, x)

    At every parameter and start, the finite-set laws form a projective measure family.