LeanPool.RlTheoryInLean.Probability.Kernel.Basic

noncomputable def ProbabilityTheory.Kernel.iter {α : Type u_1} [MeasurableSpace α] (κ : Kernel α α) : ℕ → Kernel α α

Iterates of a homogeneous transition kernel.

Equations

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

instance ProbabilityTheory.Kernel.instIsMarkovKernelIter {α : Type u_1} [MeasurableSpace α] (n : ℕ) (κ : Kernel α α) [IsMarkovKernel κ] : IsMarkovKernel (κ.iter n)

theorem ProbabilityTheory.Kernel.iter_comm {α : Type u_1} [MeasurableSpace α] (κ : Kernel α α) (n : ℕ) : κ.comp (κ.iter n) = (κ.iter n).comp κ

theorem ProbabilityTheory.Kernel.iter_comp {α : Type u_1} [MeasurableSpace α] (κ : Kernel α α) (m n : ℕ) : (κ.iter m).comp (κ.iter n) = κ.iter (m + n)