English
For μ finite and f ergodic, μ is an extreme point of the set of ν with MeasurePreserving f ν ν and ν univ = μ univ.
Русский
Для μ конечной и f эргодичного, μ является экстремальной точкой множества ν с MeasurePreserving f ν ν и равенством ν(univ) = μ(univ).
LaTeX
$$$[IsFiniteMeasure(\\\\mu)] \\\\Rightarrow \\\\mu \\\\in extremePoints \\\\{\\\\nu \\\\mid MeasurePreserving(f, \\\\nu, \\\\nu) \\\\wedge \\\\nu.univ = \\\\mu.univ\\\\}$$$
Lean4
theorem iff_mem_extremePoints [IsProbabilityMeasure μ] :
Ergodic f μ ↔ μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ IsProbabilityMeasure ν} :=
⟨mem_extremePoints, of_mem_extremePoints⟩