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 #
probability_theory.kernel.map_measure: the push-forward of a measure along a kernel.probability_theory.kernel.invariant: invariance of a given measure with respect to a kernel.
Useful lemmas #
probability_theory.kernel.comp_apply_eq_map_measure,probability_theory.kernel.const_map_measure_eq_comp_const, andprobability_theory.kernel.comp_const_apply_eq_map_measureestablished the relationship between the push-forward measure and the composition of kernels.
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
- probability_theory.kernel.map_measure κ μ = measure_theory.measure.of_measurable (λ (s : set β) (hs : measurable_set s), ∫⁻ (x : α), ⇑(⇑κ x) s ∂μ) _ _
@[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) :
@[simp]
theorem
probability_theory.kernel.map_measure_zero
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β)) :
@[simp]
theorem
probability_theory.kernel.map_measure_add
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
(μ ν : measure_theory.measure α) :
@[simp]
theorem
probability_theory.kernel.map_measure_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.comp_apply_eq_map_measure
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : measurable_space α}
{mβ : measurable_space β}
{mγ : measurable_space γ}
(η : ↥(probability_theory.kernel β γ))
[probability_theory.kernel.is_s_finite_kernel η]
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
(a : α) :
⇑(probability_theory.kernel.comp η κ) a = probability_theory.kernel.map_measure η (⇑κ a)
theorem
probability_theory.kernel.const_map_measure_eq_comp_const
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
(μ : measure_theory.measure α)
[measure_theory.is_finite_measure μ] :
theorem
probability_theory.kernel.comp_const_apply_eq_map_measure
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
(μ : measure_theory.measure α)
[measure_theory.is_finite_measure μ]
(a : α) :
theorem
probability_theory.kernel.lintegral_map_measure
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.kernel.is_s_finite_kernel κ]
(μ : measure_theory.measure α)
[measure_theory.is_finite_measure μ]
{f : β → ennreal}
(hf : measurable f) :
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
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 α}
[probability_theory.kernel.is_s_finite_kernel κ]
[measure_theory.is_finite_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.kernel.is_s_finite_kernel κ]
[probability_theory.kernel.is_s_finite_kernel η]
[measure_theory.is_finite_measure μ]
(hκ : probability_theory.kernel.invariant κ μ)
(hη : probability_theory.kernel.invariant η μ) :