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 #

Push-forward of measures along a kernel #

@[deprecated ProbabilityTheory.Kernel.comp_const (since := "2025-08-06")]
theorem ProbabilityTheory.Kernel.const_bind_eq_comp_const {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} (κ : Kernel α β) (μ : MeasureTheory.Measure α) :
const α (μ.bind κ) = κ.comp (const α μ)
@[deprecated ProbabilityTheory.Kernel.comp_const (since := "2025-08-06")]
theorem ProbabilityTheory.Kernel.comp_const_apply_eq_bind {α : Type u_1} {β : Type u_2} { : MeasurableSpace α} { : MeasurableSpace β} (κ : Kernel α β) (μ : MeasureTheory.Measure α) (a : α) :
(κ.comp (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
Instances For
    theorem ProbabilityTheory.Kernel.Invariant.def {α : Type u_1} { : MeasurableSpace α} {κ : Kernel α α} {μ : MeasureTheory.Measure α} ( : κ.Invariant μ) :
    μ.bind κ = μ
    theorem ProbabilityTheory.Kernel.Invariant.comp_const {α : Type u_1} { : MeasurableSpace α} {κ : Kernel α α} {μ : MeasureTheory.Measure α} ( : κ.Invariant μ) :
    κ.comp (const α μ) = const α μ
    theorem ProbabilityTheory.Kernel.Invariant.comp {α : Type u_1} { : MeasurableSpace α} {κ η : Kernel α α} {μ : MeasureTheory.Measure α} ( : κ.Invariant μ) ( : η.Invariant μ) :
    (κ.comp η).Invariant μ

    Reversibility of kernels #

    Reversibility (detailed balance) of a Markov kernel κ w.r.t. a measure π: for all measurable sets A B, the mass flowing from A to B equals that from B to A.

    Equations
    Instances For
      theorem ProbabilityTheory.Kernel.IsReversible.invariant {α : Type u_1} { : MeasurableSpace α} {κ : Kernel α α} [IsMarkovKernel κ] {π : MeasureTheory.Measure α} (h_rev : κ.IsReversible π) :
      κ.Invariant π

      A reversible Markov kernel leaves the measure π invariant.