English
A non-infinite extreme point of the invariant measures under f is ergodic.
Русский
Экстремальная точка множества инвариантных мер относительно f является эргодической.
LaTeX
$$$\mathrm{of\_mem\_extremePoints\_measure\_univ\_eq}(f, \mu)$$$
Lean4
/-- Given a constant `c ≠ ∞`, an extreme point of the set of measures that are invariant under `f`
and have total mass `c` is an ergodic measure. -/
theorem of_mem_extremePoints_measure_univ_eq {c : ℝ≥0∞} (hc : c ≠ ∞)
(h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = c}) : Ergodic f μ :=
by
have hf : MeasurePreserving f μ μ := h.1.1
rcases eq_or_ne c 0 with rfl | hc₀
· convert zero_measure hf.measurable
rw [← measure_univ_eq_zero, h.1.2]
· refine ⟨hf, ⟨?_⟩⟩
have : IsFiniteMeasure μ := by
constructor
rwa [h.1.2, lt_top_iff_ne_top]
set S := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
have {s : Set X} (hsm : MeasurableSet s) (hfs : f ⁻¹' s = s) (hμs : μ s ≠ 0) : c • μ[|s] ∈ S :=
by
refine ⟨.smul_measure (.smul_measure ?_ _) c, ?_⟩
· convert hf.restrict_preimage hsm
exact hfs.symm
· rw [Measure.smul_apply, (cond_isProbabilityMeasure hμs).1, smul_eq_mul, mul_one]
intro s hsm hfs
by_contra H
obtain ⟨hs, hs'⟩ : μ s ≠ 0 ∧ μ sᶜ ≠ 0 := by simpa [eventuallyConst_set, ae_iff, and_comm] using H
have hcond : c • μ[|s] = μ :=
by
apply h.2 (this hsm hfs hs) (this hsm.compl (by rw [preimage_compl, hfs]) hs')
refine ⟨μ s / c, μ sᶜ / c, ENNReal.div_pos hs hc, ENNReal.div_pos hs' hc, ?_, ?_⟩
· rw [← ENNReal.add_div, measure_add_measure_compl hsm, h.1.2, ENNReal.div_self hc₀ hc]
· simp [ProbabilityTheory.cond, smul_smul, ← mul_assoc, ENNReal.div_mul_cancel, ENNReal.mul_inv_cancel, *]
rw [← hcond] at hs'
simp [ProbabilityTheory.cond_apply, hsm] at hs'
