Documentation

Mathlib.Probability.Kernel.Invariance

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 #

Useful lemmas #

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 α β) :
(μ + ν).bind κ = μ.bind κ + ν.bind κ
@[simp]
theorem ProbabilityTheory.Kernel.bind_smul {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) (μ : MeasureTheory.Measure α) (r : ENNReal) :
(r μ).bind κ = r μ.bind κ
theorem ProbabilityTheory.Kernel.comp_const_apply_eq_bind {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) (μ : MeasureTheory.Measure α) (a : α) :
(κ.comp (ProbabilityTheory.Kernel.const α μ)) a = μ.bind κ

Invariant measures of kernels #

A measure μ is invariant with respect to the kernel κ if the push-forward measure of μ along κ equals μ.

Equations
  • κ.Invariant μ = (μ.bind κ = μ)
Instances For
    theorem ProbabilityTheory.Kernel.Invariant.def {α : Type u_1} {mα : MeasurableSpace α} {κ : ProbabilityTheory.Kernel α α} {μ : MeasureTheory.Measure α} (hκ : κ.Invariant μ) :
    μ.bind κ = μ
    theorem ProbabilityTheory.Kernel.Invariant.comp {α : Type u_1} {mα : MeasurableSpace α} {κ : ProbabilityTheory.Kernel α α} {η : ProbabilityTheory.Kernel α α} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsSFiniteKernel κ] (hκ : κ.Invariant μ) (hη : η.Invariant μ) :
    (κ.comp η).Invariant μ