Reversibility and the exchange of the current and next states #
A Markov kernel κ is reversible with respect to π, in the sense of Kernel.IsReversible, if
and only if the joint distribution π ⊗ₘ κ of the current and the next states does not change
when the two are exchanged. In the proofs of Propositions 1, S1, and S4 of the paper, the second
form is established.
theorem
CSMC.isReversible_iff_map_swap
{α : Type u_1}
[MeasurableSpace α]
{π : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure π]
{κ : ProbabilityTheory.Kernel α α}
[ProbabilityTheory.IsFiniteKernel κ]
:
For a finite measure π and a finite kernel κ, κ is reversible with respect to π if and
only if π ⊗ₘ κ is invariant under the exchange of the two coordinates.
theorem
CSMC.isReversible_of_map_swap
{α : Type u_1}
[MeasurableSpace α]
{π : MeasureTheory.Measure α}
[MeasureTheory.SFinite π]
{κ : ProbabilityTheory.Kernel α α}
[ProbabilityTheory.IsSFiniteKernel κ]
(h : MeasureTheory.Measure.map Prod.swap (π.compProd κ) = π.compProd κ)
:
κ.IsReversible π
For an s-finite measure π and an s-finite kernel κ, if π ⊗ₘ κ is invariant under the
exchange of the two coordinates, then κ is reversible with respect to π.
theorem
CSMC.invariant_of_map_snd
{α : Type u_1}
[MeasurableSpace α]
{π : MeasureTheory.Measure α}
[MeasureTheory.SFinite π]
{κ : ProbabilityTheory.Kernel α α}
[ProbabilityTheory.IsSFiniteKernel κ]
(h : MeasureTheory.Measure.map Prod.snd (π.compProd κ) = π)
:
κ.Invariant π
For an s-finite measure π and an s-finite kernel κ, if the second marginal of π ⊗ₘ κ is
π, then κ leaves π invariant.