id — Mathlib · SciLib

English

For finite μ, ergodicity of f w.r.t μ is equivalent to μ being an extreme point in the set of ν with measure-preserving f and ν a probability measure.

Русский

Пусть μ конечно по мере; эргодичность f по μ эквивалентна тому, что μ является экстремальной точкой множества ν с MeasurePreserving f и ν вероятностная мера.

LaTeX

$$$[IsFiniteMeasure μ] \\\\Leftrightarrow \\\\big( Ergodic f μ \\\\Leftrightarrow μ \\\\in extremePoints \\\\{ν \\\\mid MeasurePreserving f ν ν \\\\wedge IsProbabilityMeasure ν\\\\}\\big)$$$

Lean4

protected theorem id (μ : Measure α) : MeasurePreserving id μ μ :=
  ⟨measurable_id, map_id⟩

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