trans — Mathlib

English

Equivalence between ergodicity and membership in extremePoints for invariant measures.

Русский

Эквивалентность эргодичности и принадлежности к экстремальным точкам инвариантных мер.

LaTeX

$$$[IsProbabilityMeasure μ] \\\\Rightarrow Ergodic f μ \\\\Leftrightarrow μ \\\\in extremePoints \\\\{ν \\\\mid MeasurePreserving f ν ν \\\\wedge IsProbabilityMeasure ν\\\\}$$$

Lean4

/-- An alias of `MeasureTheory.MeasurePreserving.comp` with a convenient defeq and argument order
for `MeasurableEquiv` -/
protected theorem trans {e : α ≃ᵐ β} {e' : β ≃ᵐ γ} {μa : Measure α} {μb : Measure β} {μc : Measure γ}
    (h : MeasurePreserving e μa μb) (h' : MeasurePreserving e' μb μc) : MeasurePreserving (e.trans e') μa μc :=
  h'.comp h

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