mathlib3 documentation

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 #

Useful lemmas #

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

Invariant measures of kernels #

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

Equations