Powers of s-finite, finite and Markov kernels

Iterating an s-finite kernel remains s-finite; iterating a uniformly finite kernel remains uniformly finite. The latter permits taking finite transition masses, and thus nonnegative real transition matrices, for every iterate. Iterating a Markov kernel also preserves the probability normalization of every row. Every power of a kernel preserves each of its invariant measures.

The powers of a deterministic kernel are the deterministic kernels of the iterates. Restricting the Chapman–Kolmogorov integral to one intermediate state bounds (κ ^ (m + n)) x s below by (κ ^ m) x {y} * (κ ^ n) y s; this is how positivity of multi-step transition masses propagates along paths of states.

instance ProbabilityTheory.IsSFiniteKernel.pow {α : Type u_1} [MeasurableSpace α] (κ : Kernel α α) [IsSFiniteKernel κ] (n : ℕ) : IsSFiniteKernel (κ ^ n)

Every natural power of an s-finite kernel is s-finite.

instance ProbabilityTheory.IsFiniteKernel.pow {α : Type u_1} [MeasurableSpace α] (κ : Kernel α α) [IsFiniteKernel κ] (n : ℕ) : IsFiniteKernel (κ ^ n)

Every natural power of a finite kernel is finite.

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

Every natural power of a Markov kernel is a Markov kernel.

theorem ProbabilityTheory.Kernel.one_def {α : Type u_1} [MeasurableSpace α] : 1 = Kernel.id

The unit of the monoid of kernels Kernel α α is the identity kernel.

@[simp]

theorem ProbabilityTheory.Kernel.Invariant.pow_comp {α : Type u_1} [MeasurableSpace α] {κ : Kernel α α} {ν : MeasureTheory.Measure α} (hν : κ.Invariant ν) (n : ℕ) : ν.bind ⇑(κ ^ n) = ν

Every power of a kernel preserves each of its invariant measures.

theorem ProbabilityTheory.Kernel.comp_pow_eq_pow_comp_of_comp_eq {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] {e : Kernel β α} {η : Kernel β β} {κ : Kernel α α} (h : e.comp η = κ.comp e) (n : ℕ) : e.comp (η ^ n) = (κ ^ n).comp e

A kernel intertwining two one-step kernels also intertwines all their powers.

theorem ProbabilityTheory.Kernel.Invariant.pow {α : Type u_1} [MeasurableSpace α] {κ : Kernel α α} {μ : MeasureTheory.Measure α} (hκ : κ.Invariant μ) (n : ℕ) : (κ ^ n).Invariant μ

A measure invariant under a kernel is invariant under every natural power of it.

@[simp]

theorem ProbabilityTheory.Kernel.deterministic_pow {α : Type u_1} [MeasurableSpace α] {f : α → α} (hf : Measurable f) (n : ℕ) : deterministic f hf ^ n = deterministic f^[n] ⋯

The n-th power of the deterministic kernel of f is the deterministic kernel of the n-th iterate of f.

theorem ProbabilityTheory.Kernel.pow_apply_singleton_mul_le_pow_add_apply {α : Type u_1} [MeasurableSpace α] (κ : Kernel α α) (m n : ℕ) (x y : α) {s : Set α} : ((κ ^ m) x) {y} * ((κ ^ n) y) s ≤ ((κ ^ (m + n)) x) s

Chapman–Kolmogorov lower bound. The m + n-step mass of a set s is at least the mass of the paths that sit at the intermediate state y at time m.

theorem ProbabilityTheory.Kernel.pow_add_apply_pos {α : Type u_1} [MeasurableSpace α] {κ : Kernel α α} {m n : ℕ} {x y : α} {s : Set α} (hxy : 0 < ((κ ^ m) x) {y}) (hy : 0 < ((κ ^ n) y) s) : 0 < ((κ ^ (m + n)) x) s

Positive multi-step masses compose: if x reaches y with positive probability in m steps and y reaches s with positive probability in n steps, then x reaches s with positive probability in m + n steps.