Invariance of measures along a kernel #
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 #
ProbabilityTheory.kernel.Invariant
: invariance of a given measure with respect to a kernel.
Useful lemmas #
ProbabilityTheory.kernel.const_bind_eq_comp_const
, andProbabilityTheory.kernel.comp_const_apply_eq_bind
established the relationship between the push-forward measure and the composition of kernels.
Push-forward of measures along a kernel #
@[simp]
theorem
ProbabilityTheory.kernel.bind_add
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
(κ : ↥(ProbabilityTheory.kernel α β))
:
@[simp]
theorem
ProbabilityTheory.kernel.bind_smul
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
(μ : MeasureTheory.Measure α)
(r : ENNReal)
:
theorem
ProbabilityTheory.kernel.const_bind_eq_comp_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
(μ : MeasureTheory.Measure α)
:
ProbabilityTheory.kernel.const α (μ.bind ⇑κ) = ProbabilityTheory.kernel.comp κ (ProbabilityTheory.kernel.const α μ)
theorem
ProbabilityTheory.kernel.comp_const_apply_eq_bind
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
(μ : MeasureTheory.Measure α)
(a : α)
:
(ProbabilityTheory.kernel.comp κ (ProbabilityTheory.kernel.const α μ)) a = μ.bind ⇑κ
Invariant measures of kernels #
def
ProbabilityTheory.kernel.Invariant
{α : Type u_1}
{mα : MeasurableSpace α}
(κ : ↥(ProbabilityTheory.kernel α α))
(μ : MeasureTheory.Measure α)
:
A measure μ
is invariant with respect to the kernel κ
if the push-forward measure of μ
along κ
equals μ
.
Equations
- ProbabilityTheory.kernel.Invariant κ μ = (μ.bind ⇑κ = μ)
Instances For
theorem
ProbabilityTheory.kernel.Invariant.def
{α : Type u_1}
{mα : MeasurableSpace α}
{κ : ↥(ProbabilityTheory.kernel α α)}
{μ : MeasureTheory.Measure α}
(hκ : ProbabilityTheory.kernel.Invariant κ μ)
:
μ.bind ⇑κ = μ
theorem
ProbabilityTheory.kernel.Invariant.comp_const
{α : Type u_1}
{mα : MeasurableSpace α}
{κ : ↥(ProbabilityTheory.kernel α α)}
{μ : MeasureTheory.Measure α}
(hκ : ProbabilityTheory.kernel.Invariant κ μ)
:
theorem
ProbabilityTheory.kernel.Invariant.comp
{α : Type u_1}
{mα : MeasurableSpace α}
{κ : ↥(ProbabilityTheory.kernel α α)}
{η : ↥(ProbabilityTheory.kernel α α)}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsSFiniteKernel κ]
(hκ : ProbabilityTheory.kernel.Invariant κ μ)
(hη : ProbabilityTheory.kernel.Invariant η μ)
: