# 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 #

@[simp]
theorem ProbabilityTheory.kernel.bind_add {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (μ : ) (ν : ) (κ : ()) :
(μ + ν).bind κ = μ.bind κ + ν.bind κ
@[simp]
theorem ProbabilityTheory.kernel.bind_smul {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (μ : ) (r : ENNReal) :
(r μ).bind κ = r μ.bind κ
theorem ProbabilityTheory.kernel.const_bind_eq_comp_const {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (μ : ) :
ProbabilityTheory.kernel.const α (μ.bind κ) =
theorem ProbabilityTheory.kernel.comp_const_apply_eq_bind {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (μ : ) (a : α) :
= μ.bind κ

### Invariant measures of kernels #

def ProbabilityTheory.kernel.Invariant {α : Type u_1} {mα : } (κ : ()) (μ : ) :

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

Equations
• = (μ.bind κ = μ)
Instances For
theorem ProbabilityTheory.kernel.Invariant.def {α : Type u_1} {mα : } {κ : ()} {μ : } (hκ : ) :
μ.bind κ = μ
theorem ProbabilityTheory.kernel.Invariant.comp_const {α : Type u_1} {mα : } {κ : ()} {μ : } (hκ : ) :
theorem ProbabilityTheory.kernel.Invariant.comp {α : Type u_1} {mα : } {κ : ()} {η : ()} {μ : } (hκ : ) (hη : ) :