Invariance of measures along a kernel

We say that a measure μ is invariant with respect to a kernel κ if its push-forward along the kernel μ.bind κ is the same measure.

Main definitions

• ProbabilityTheory.Kernel.Invariant: invariance of a given measure with respect to a kernel.

Invariant measures of kernels

def ProbabilityTheory.Kernel.Invariant {α : Type u_1} {mα : MeasurableSpace α} (κ : Kernel α α) (μ : MeasureTheory.Measure α) : Prop

A measure μ is invariant with respect to the kernel κ if the push-forward measure of μ along κ equals μ.

theorem ProbabilityTheory.Kernel.Invariant.def {α : Type u_1} {mα : MeasurableSpace α} {κ : Kernel α α} {μ : MeasureTheory.Measure α} (hκ : κ.Invariant μ) : μ.bind ⇑κ = μ

theorem ProbabilityTheory.Kernel.Invariant.comp_const {α : Type u_1} {mα : MeasurableSpace α} {κ : Kernel α α} {μ : MeasureTheory.Measure α} (hκ : κ.Invariant μ) : κ.comp (const α μ) = const α μ

theorem ProbabilityTheory.Kernel.Invariant.comp {α : Type u_1} {mα : MeasurableSpace α} {κ η : Kernel α α} {μ : MeasureTheory.Measure α} (hκ : κ.Invariant μ) (hη : η.Invariant μ) : (κ.comp η).Invariant μ

Reversibility of kernels

def ProbabilityTheory.Kernel.IsReversible {α : Type u_1} {mα : MeasurableSpace α} (κ : Kernel α α) (π : MeasureTheory.Measure α) : Prop

Reversibility (detailed balance) of a Markov kernel κ w.r.t. a measure π: for all measurable sets A B, the mass flowing from A to B equals that from B to A.

theorem ProbabilityTheory.Kernel.IsReversible.invariant {α : Type u_1} {mα : MeasurableSpace α} {κ : Kernel α α} [IsMarkovKernel κ] {π : MeasureTheory.Measure α} (h_rev : κ.IsReversible π) : κ.Invariant π

A reversible Markov kernel leaves the measure π invariant.