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
μ.bind κ is the same measure.
Main definitions #
Useful lemmas #
Push-forward of measures along a kernel #
Invariant measures of kernels #
μ is invariant with respect to the kernel
κ if the push-forward measure of