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 α)
(κ : { x // x ∈ ProbabilityTheory.kernel α β })
:
MeasureTheory.Measure.bind (μ + ν) ↑κ = MeasureTheory.Measure.bind μ ↑κ + MeasureTheory.Measure.bind ν ↑κ
@[simp]
theorem
ProbabilityTheory.kernel.bind_smul
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : { x // x ∈ ProbabilityTheory.kernel α β })
(μ : MeasureTheory.Measure α)
(r : ENNReal)
:
MeasureTheory.Measure.bind (r • μ) ↑κ = r • MeasureTheory.Measure.bind μ ↑κ
theorem
ProbabilityTheory.kernel.const_bind_eq_comp_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : { x // x ∈ ProbabilityTheory.kernel α β })
(μ : MeasureTheory.Measure α)
:
theorem
ProbabilityTheory.kernel.comp_const_apply_eq_bind
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : { x // x ∈ ProbabilityTheory.kernel α β })
(μ : MeasureTheory.Measure α)
(a : α)
:
Invariant measures of kernels #
def
ProbabilityTheory.kernel.Invariant
{α : Type u_1}
{mα : MeasurableSpace α}
(κ : { x // x ∈ ProbabilityTheory.kernel α α })
(μ : MeasureTheory.Measure α)
:
A measure μ
is invariant with respect to the kernel κ
if the push-forward measure of μ
along κ
equals μ
.
Instances For
theorem
ProbabilityTheory.kernel.Invariant.def
{α : Type u_1}
{mα : MeasurableSpace α}
{κ : { x // x ∈ ProbabilityTheory.kernel α α }}
{μ : MeasureTheory.Measure α}
(hκ : ProbabilityTheory.kernel.Invariant κ μ)
:
MeasureTheory.Measure.bind μ ↑κ = μ
theorem
ProbabilityTheory.kernel.Invariant.comp_const
{α : Type u_1}
{mα : MeasurableSpace α}
{κ : { x // x ∈ ProbabilityTheory.kernel α α }}
{μ : MeasureTheory.Measure α}
(hκ : ProbabilityTheory.kernel.Invariant κ μ)
:
theorem
ProbabilityTheory.kernel.Invariant.comp
{α : Type u_1}
{mα : MeasurableSpace α}
{κ : { x // x ∈ ProbabilityTheory.kernel α α }}
{η : { x // x ∈ ProbabilityTheory.kernel α α }}
{μ : MeasureTheory.Measure α}
[ProbabilityTheory.IsSFiniteKernel κ]
(hκ : ProbabilityTheory.kernel.Invariant κ μ)
(hη : ProbabilityTheory.kernel.Invariant η μ)
: