iff_mem_extremePoints — Mathlib

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⟩

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