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.
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}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : Kernel α β)
(μ : MeasureTheory.Measure α)
:
@[deprecated ProbabilityTheory.Kernel.comp_const (since := "2025-08-06")]
theorem
ProbabilityTheory.Kernel.comp_const_apply_eq_bind
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : Kernel α β)
(μ : MeasureTheory.Measure α)
(a : α)
:
Invariant measures of kernels #
def
ProbabilityTheory.Kernel.Invariant
{α : Type u_1}
{mα : MeasurableSpace α}
(κ : 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 α}
{κ : Kernel α α}
{μ : MeasureTheory.Measure α}
(hκ : κ.Invariant μ)
:
theorem
ProbabilityTheory.Kernel.Invariant.comp_const
{α : Type u_1}
{mα : MeasurableSpace α}
{κ : Kernel α α}
{μ : MeasureTheory.Measure α}
(hκ : κ.Invariant μ)
:
theorem
ProbabilityTheory.Kernel.Invariant.comp
{α : Type u_1}
{mα : MeasurableSpace α}
{κ η : Kernel α α}
{μ : MeasureTheory.Measure α}
(hκ : κ.Invariant μ)
(hη : η.Invariant μ)
:
Reversibility of kernels #
def
ProbabilityTheory.Kernel.IsReversible
{α : Type u_1}
{mα : MeasurableSpace α}
(κ : Kernel α α)
(π : MeasureTheory.Measure α)
:
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
- κ.IsReversible π = ∀ ⦃A B : Set α⦄, MeasurableSet A → MeasurableSet B → ∫⁻ (x : α) in A, (κ x) B ∂π = ∫⁻ (x : α) in B, (κ x) A ∂π
Instances For
theorem
ProbabilityTheory.Kernel.IsReversible.invariant
{α : Type u_1}
{mα : MeasurableSpace α}
{κ : Kernel α α}
[IsMarkovKernel κ]
{π : MeasureTheory.Measure α}
(h_rev : κ.IsReversible π)
:
κ.Invariant π
A reversible Markov kernel leaves the measure π
invariant.