iff_mem_extremePoints_measure_univ_eq

English

An ergodic map f with finite μ is equivalent (under the given framework) to μ being an extreme point of invariant measures; i.e., ergodicity characterizes extreme behavior.

Русский

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

LaTeX

$$$[IsFiniteMeasure(\\\\mu)] \\\\Leftrightarrow \\\\mu \\\\text{ is an extreme point of } \{\\\\nu \\\\mid MeasurePreserving(f, \\\\nu, \\\\nu) \\\\wedge \\\\nu.univ = \\\\mu.univ\\\\}$$$

Lean4

theorem iff_mem_extremePoints_measure_univ_eq [IsFiniteMeasure μ] :
    Ergodic f μ ↔ μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = μ univ} :=
  ⟨mem_extremePoints_measure_univ_eq, of_mem_extremePoints_measure_univ_eq (measure_ne_top _ _)⟩

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