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, andprobability_theory.kernel.comp_const_apply_eq_bindestablished 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 α)
(κ : ↥(probability_theory.kernel α β)) :
@[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) :
theorem
probability_theory.kernel.const_bind_eq_comp_const
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
(μ : measure_theory.measure α) :
theorem
probability_theory.kernel.comp_const_apply_eq_bind
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
(μ : measure_theory.measure α)
(a : α) :
⇑(probability_theory.kernel.comp κ (probability_theory.kernel.const α μ)) a = μ.bind ⇑κ
Invariant measures of kernels #
def
probability_theory.kernel.invariant
{α : Type u_1}
{mα : measurable_space α}
(κ : ↥(probability_theory.kernel α α))
(μ : measure_theory.measure α) :
Prop
A measure μ is invariant with respect to the kernel κ if the push-forward measure of μ
along κ equals μ.
Equations
- probability_theory.kernel.invariant κ μ = (μ.bind ⇑κ = μ)
theorem
probability_theory.kernel.invariant.def
{α : Type u_1}
{mα : measurable_space α}
{κ : ↥(probability_theory.kernel α α)}
{μ : measure_theory.measure α}
(hκ : probability_theory.kernel.invariant κ μ) :
theorem
probability_theory.kernel.invariant.comp_const
{α : Type u_1}
{mα : measurable_space α}
{κ : ↥(probability_theory.kernel α α)}
{μ : measure_theory.measure α}
(hκ : probability_theory.kernel.invariant κ μ) :
theorem
probability_theory.kernel.invariant.comp
{α : Type u_1}
{mα : measurable_space α}
{κ η : ↥(probability_theory.kernel α α)}
{μ : measure_theory.measure α}
[probability_theory.is_s_finite_kernel κ]
(hκ : probability_theory.kernel.invariant κ μ)
(hη : probability_theory.kernel.invariant η μ) :