Ergodic measures as extreme points

In this file we prove that a finite measure μ is an ergodic measure for a self-map f iff it is an extreme point of the set of invariant measures of f with the same total volume. We also specialize this result to probability measures.

theorem Ergodic.of_mem_extremePoints_measure_univ_eq {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → X} {c : ENNReal} (hc : c ≠ ⊤) (h : μ ∈ Set.extremePoints ENNReal {ν : MeasureTheory.Measure X | MeasureTheory.MeasurePreserving f ν ν ∧ ν Set.univ = c}) : Ergodic f μ

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 Ergodic.of_mem_extremePoints {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → X} (h : μ ∈ Set.extremePoints ENNReal {ν : MeasureTheory.Measure X | MeasureTheory.MeasurePreserving f ν ν ∧ MeasureTheory.IsProbabilityMeasure ν}) : Ergodic f μ

An extreme point of the set of invariant probability measures is an ergodic measure.

theorem Ergodic.eq_smul_of_absolutelyContinuous {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} {f : X → X} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμ : Ergodic f μ) (hfν : MeasureTheory.MeasurePreserving f ν ν) (hνμ : ν.AbsolutelyContinuous μ) : ∃ (c : ENNReal), ν = c • μ

theorem Ergodic.eq_of_absolutelyContinuous_measure_univ_eq {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} {f : X → X} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμ : Ergodic f μ) (hfν : MeasureTheory.MeasurePreserving f ν ν) (hνμ : ν.AbsolutelyContinuous μ) (huniv : ν Set.univ = μ Set.univ) : ν = μ

theorem Ergodic.eq_of_absolutelyContinuous {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} {f : X → X} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hμ : Ergodic f μ) (hfν : MeasureTheory.MeasurePreserving f ν ν) (hνμ : ν.AbsolutelyContinuous μ) : ν = μ

theorem Ergodic.mem_extremePoints_measure_univ_eq {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → X} [MeasureTheory.IsFiniteMeasure μ] (hμ : Ergodic f μ) : μ ∈ Set.extremePoints ENNReal {ν : MeasureTheory.Measure X | MeasureTheory.MeasurePreserving f ν ν ∧ ν Set.univ = μ Set.univ}

theorem Ergodic.mem_extremePoints {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → X} [MeasureTheory.IsProbabilityMeasure μ] (hμ : Ergodic f μ) : μ ∈ Set.extremePoints ENNReal {ν : MeasureTheory.Measure X | MeasureTheory.MeasurePreserving f ν ν ∧ MeasureTheory.IsProbabilityMeasure ν}

theorem Ergodic.iff_mem_extremePoints_measure_univ_eq {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → X} [MeasureTheory.IsFiniteMeasure μ] : Ergodic f μ ↔ μ ∈ Set.extremePoints ENNReal {ν : MeasureTheory.Measure X | MeasureTheory.MeasurePreserving f ν ν ∧ ν Set.univ = μ Set.univ}

theorem Ergodic.iff_mem_extremePoints {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → X} [MeasureTheory.IsProbabilityMeasure μ] : Ergodic f μ ↔ μ ∈ Set.extremePoints ENNReal {ν : MeasureTheory.Measure X | MeasureTheory.MeasurePreserving f ν ν ∧ MeasureTheory.IsProbabilityMeasure ν}