# mathlib3documentation

probability.kernel.invariance

# Invariance of measures along a kernel #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• probability_theory.kernel.invariant: invariance of a given measure with respect to a kernel.

## Useful lemmas #

• probability_theory.kernel.const_bind_eq_comp_const, and probability_theory.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 probability_theory.kernel.bind_add {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (μ ν : measure_theory.measure α) (κ : ) :
+ ν).bind κ = μ.bind κ + ν.bind κ
@[simp]
theorem probability_theory.kernel.bind_smul {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) (μ : measure_theory.measure α) (r : ennreal) :
(r μ).bind κ = r μ.bind κ
theorem probability_theory.kernel.const_bind_eq_comp_const {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) (μ : measure_theory.measure α) :
theorem probability_theory.kernel.comp_const_apply_eq_bind {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) (μ : measure_theory.measure α) (a : α) :
= μ.bind κ

### Invariant measures of kernels #

def probability_theory.kernel.invariant {α : Type u_1} {mα : measurable_space α} (κ : ) (μ : measure_theory.measure α) :
Prop

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

Equations
theorem probability_theory.kernel.invariant.def {α : Type u_1} {mα : measurable_space α} {κ : } {μ : measure_theory.measure α} (hκ : μ) :
μ.bind κ = μ
theorem probability_theory.kernel.invariant.comp_const {α : Type u_1} {mα : measurable_space α} {κ : } {μ : measure_theory.measure α} (hκ : μ) :
theorem probability_theory.kernel.invariant.comp {α : Type u_1} {mα : measurable_space α} {κ η : } {μ : measure_theory.measure α} (hκ : μ) (hη : μ) :