of_mem_extremePoints — Mathlib

English

If an invariant measure is an extreme point of the set of invariant measures, it is ergodic.

Русский

Если инвариантная мера является экстремальной точкой множества инвариантных мер, она эргодична.

LaTeX

$$$\mu \in \mathrm{extremePoints}\; \mathcal{M}_{f} \Rightarrow \mathrm{Ergodic}(f, \mu)$$$

Lean4

/-- An extreme point of the set of invariant probability measures is an ergodic measure. -/
theorem of_mem_extremePoints (h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ IsProbabilityMeasure ν}) :
    Ergodic f μ :=
  .of_mem_extremePoints_measure_univ_eq ENNReal.one_ne_top <| by simpa only [isProbabilityMeasure_iff] using h

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