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 μ)
:
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 μ)
:
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 μ]
: