English
If κ and η are invariant with respect to μ, then their composition is invariant with respect to μ.
Русский
Если ядра κ и η инвариантны относительно μ, то их композиция κ ∘ η инвариантна относительно μ.
LaTeX
$$$\\kappa.Invariant\\; μ \\rightarrow \\eta.Invariant\\; μ \\\\Rightarrow (κ \\circ η).Invariant μ$$$
Lean4
/-- A reversible Markov kernel leaves the measure `π` invariant. -/
theorem invariant {κ : Kernel α α} [IsMarkovKernel κ] {π : Measure α} (h_rev : IsReversible κ π) : Invariant κ π :=
by
ext s hs
calc
(κ ∘ₘ π) s = ∫⁻ x, κ x s ∂π := by rw [Measure.bind_apply hs (Kernel.aemeasurable _)]
_ = ∫⁻ x in s, κ x Set.univ ∂π := by simpa [restrict_univ] using (h_rev hs .univ).symm
_ = π s := by simp