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.

Useful lemmas

• ProbabilityTheory.Kernel.const_bind_eq_comp_const, and ProbabilityTheory.Kernel.comp_const_apply_eq_bind established the relationship between the push-forward measure and the composition of kernels.

Push-forward of measures along a kernel

@[deprecated "Use comp_add in Composition/MeasureComp" (since := "2025-02-28")]

theorem ProbabilityTheory.Kernel.bind_add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ ν : MeasureTheory.Measure α) (κ : Kernel α β) : (μ + ν).bind ⇑κ = μ.bind ⇑κ + ν.bind ⇑κ

@[deprecated "Use comp_smul in Composition/MeasureComp" (since := "2025-02-28")]

theorem ProbabilityTheory.Kernel.bind_smul {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (μ : MeasureTheory.Measure α) (r : ENNReal) : (r • μ).bind ⇑κ = r • μ.bind ⇑κ

theorem ProbabilityTheory.Kernel.const_bind_eq_comp_const {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (μ : MeasureTheory.Measure α) : const α (μ.bind ⇑κ) = κ.comp (const α μ)

theorem ProbabilityTheory.Kernel.comp_const_apply_eq_bind {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : Kernel α β) (μ : MeasureTheory.Measure α) (a : α) : (κ.comp (const α μ)) a = μ.bind ⇑κ

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 μ.

Equations

• κ.Invariant μ = (μ.bind ⇑κ = μ)

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 μ