LeanPool.RlTheoryInLean.Probability.MarkovChain.Trajectory

noncomputable def ProbabilityTheory.MarkovChain.kernelComapTrivial {S : Type u} [MeasurableSpace S] (κ : Kernel S S) (n : ℕ) : Kernel (↥(Finset.Iic n) → S) S

Comap a homogeneous kernel along the latest state in a finite history.

Equations

• ProbabilityTheory.MarkovChain.kernelComapTrivial κ n = κ.comap (fun (history : ↥(Finset.Iic n) → S) => history ⟨n, ⋯⟩) ⋯

noncomputable def ProbabilityTheory.MarkovChain.expandKernel {S : Type u} [MeasurableSpace S] (M : HomMarkovChainSpec S) (n : ℕ) : Kernel (↥(Finset.Iic n) → S) S

Expand a homogeneous Markov-chain kernel to act on finite trajectory prefixes.

Equations

• ProbabilityTheory.MarkovChain.expandKernel M n = M.kernel.comap (fun (history : ↥(Finset.Iic n) → S) => history ⟨n, ⋯⟩) ⋯

instance ProbabilityTheory.MarkovChain.instIsMarkovKernelForallSubtypeNatMemFinsetIicExpandKernel {S : Type u} [MeasurableSpace S] (M : HomMarkovChainSpec S) (n : ℕ) : IsMarkovKernel (expandKernel M n)

noncomputable def ProbabilityTheory.MarkovChain.trajProb₀ {S : Type u} [MeasurableSpace S] (M : HomMarkovChainSpec S) (x₀ : ↥(Finset.Iic 0) → S) : MeasureTheory.ProbabilityMeasure (ℕ → S)

The trajectory law started from a fixed length-zero prefix.

Equations

• ProbabilityTheory.MarkovChain.trajProb₀ M x₀ = ⟨(ProbabilityTheory.Kernel.traj (ProbabilityTheory.MarkovChain.expandKernel M) 0) x₀, ⋯⟩

noncomputable def ProbabilityTheory.MarkovChain.trajProb {S : Type u} [MeasurableSpace S] (M : HomMarkovChainSpec S) : MeasureTheory.ProbabilityMeasure (ℕ → S)

The trajectory law obtained by first sampling the initial state.

Equations

• ProbabilityTheory.MarkovChain.trajProb M = ⟨(↑(M.init.map ⋯)).bind ⇑(ProbabilityTheory.Kernel.traj (ProbabilityTheory.MarkovChain.expandKernel M) 0), ⋯⟩