invariant — Mathlib

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

Похожие утверждения