LeanPool.RlTheoryInLean.Probability.MarkovChain.Defs

structure ProbabilityTheory.MarkovChain.HomMarkovChainSpec (S : Type u) [MeasurableSpace S] : Type u

A homogeneous Markov chain specified by its transition kernel and initial law.

• kernel : Kernel S S

  The one-step transition kernel.

• markov_kernel : IsMarkovKernel self.kernel

  The transition kernel is Markov.

• init : MeasureTheory.ProbabilityMeasure S

  The initial distribution.

noncomputable def ProbabilityTheory.MarkovChain.Kernel.iter (S : Type u) [MeasurableSpace S] (κ : Kernel S S) : ℕ → Kernel S S

Iterates of the transition kernel of a Markov chain.

Equations

• ProbabilityTheory.MarkovChain.Kernel.iter S κ 0 = ProbabilityTheory.Kernel.id
• ProbabilityTheory.MarkovChain.Kernel.iter S κ n.succ = (ProbabilityTheory.MarkovChain.Kernel.iter S κ n).comp κ