comp — Mathlib

English

For finite μ, f-ergodicity is equivalent to μ being an extreme point of the set of invariant measures.

Русский

Для конечной μ эргодичность по f эквивалентна тому, что μ — экстремальная точка множества инвариантных мер.

LaTeX

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

Lean4

protected theorem comp {g : β → γ} {f : α → β} (hg : MeasurePreserving g μb μc) (hf : MeasurePreserving f μa μb) :
    MeasurePreserving (g ∘ f) μa μc :=
  ⟨hg.1.comp hf.1, by rw [← map_map hg.1 hf.1, hf.2, hg.2]⟩

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