English
If μ is finite and f is ergodic with respect to μ, then μ is an extreme point of the convex set of measures ν that are invariant under f and have the same total mass as μ.
Русский
Пусть μ конечна по мере, и f эргодичен относительно μ; тогда μ является экстремальной точкой выпуклого множества мер ν, удовлетворяющих инвариантности по f и имеющих ту же суммарную массу, что и μ.
LaTeX
$$$[IsFiniteMeasure(\\\\mu)] \\\\wedge Ergodic(f, \\\\mu) \\\\Rightarrow \\\\mu \\\\in extremePoints(\\\\mathbb{R}_{\\\\ge 0}^{\\\\infty})\\\\{\\\\nu \\\\mid MeasurePreserving(f, \\\\nu, \\\\nu) \\\\wedge \\\\nu(.univ) = \\\\mu.univ\\\\}$$$
Lean4
theorem mem_extremePoints_measure_univ_eq [IsFiniteMeasure μ] (hμ : Ergodic f μ) :
μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = μ univ} :=
by
rw [mem_extremePoints_iff_left]
refine ⟨⟨hμ.toMeasurePreserving, rfl⟩, ?_⟩
rintro ν₁ ⟨hfν₁, hν₁μ⟩ ν₂ ⟨hfν₂, hν₂μ⟩ ⟨a, b, ha, hb, hab, rfl⟩
have : IsFiniteMeasure ν₁ := ⟨by rw [hν₁μ]; apply measure_lt_top⟩
apply hμ.eq_of_absolutelyContinuous_measure_univ_eq hfν₁ (.add_right _ _) hν₁μ
apply absolutelyContinuous_smul ha.ne'
