English
If μ is a probability measure and f is ergodic with respect to μ, then μ lies in the set of extreme points of the collection of invariant probability measures for f.
Русский
Если μ — вероятность меры, и f эргодичен относительно μ, то μ принадлежит множеству экстремальных точек множества инвариантных вероятностных мер для f.
LaTeX
$$$[IsProbabilityMeasure(\\\\mu)] \\\\wedge Ergodic(f, \\\\mu) \\\\Rightarrow \\\\mu \\\\in extremePoints(\\\\mathbb{R}_{\\\\ge 0}^{\\\\infty})\\\\{\\\\nu \\\\mid MeasurePreserving(f, \\\\nu, \\\\nu) \\\\wedge IsProbabilityMeasure(\\\\nu)\\\\}$$$
Lean4
theorem mem_extremePoints [IsProbabilityMeasure μ] (hμ : Ergodic f μ) :
μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ IsProbabilityMeasure ν} := by
simpa only [isProbabilityMeasure_iff, measure_univ] using hμ.mem_extremePoints_measure_univ_eq
