mathlib documentation

probability.kernel.invariance

Invariance of measures along a kernel #

We define the push-forward of a measure along a kernel which results in another measure. In the case that the push-forward measure is the same as the original measure, we say that the measure is invariant with respect to the kernel.

Main definitions #

Useful lemmas #

Push-forward of measures along a kernel #

noncomputable def probability_theory.kernel.map_measure {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : (probability_theory.kernel α β)) (μ : measure_theory.measure α) :

The push-forward of a measure along a kernel.

Equations
@[simp]
theorem probability_theory.kernel.map_measure_apply {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : (probability_theory.kernel α β)) (μ : measure_theory.measure α) {s : set β} (hs : measurable_set s) :

Invariant measures of kernels #

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

Equations