Ergodic group actions and extreme invariant measures

For a countable group G acting measurably on X, an invariant measure of finite total mass is ergodic if and only if it is an extreme point of the G-invariant measures of that total mass; in particular an invariant probability measure is ergodic if and only if it is an extreme point of the invariant measures of total mass one. This is the group-action form of Mathlib's Ergodic.iff_mem_extremePoints, which concerns a single measure-preserving map.

Two general facts about an ergodic action carry the characterisation and are useful on their own: an almost invariant function is almost everywhere constant (ErgodicSMul.ae_eq_const_of_forall_ae_eq_comp_smul₀), and an invariant measure absolutely continuous with respect to an ergodic one is a multiple of it (ErgodicSMul.eq_smul_of_absolutelyContinuous). These, the invariant-measure set and the forward direction of the characterisation need only an action by a type with a scalar multiplication; the group and its countability enter only in the reverse direction, through the saturation of an almost invariant event in CountableAction.lean.

Extremality also has an integral form: an ergodic probability measure written as a mixture κ ∘ₘ π of almost surely invariant probability measures has almost every component equal to itself (ErgodicSMul.ae_eq_of_comp_eq). This is what removes a global randomization parameter from a functional representation of an ergodic law.

Main results

• TauCeti.MeasureTheory.invariantMeasuresOfMeasureUnivEq, with its membership and convexity lemmas; the invariant probability measures are the case of total mass one
• ErgodicSMul.ae_eq_const_of_forall_ae_eq_comp_smul₀
• ErgodicSMul.eq_smul_of_absolutelyContinuous, ErgodicSMul.eq_of_absolutelyContinuous_measure_univ_eq, ErgodicSMul.eq_of_absolutelyContinuous
• ErgodicSMul.iff_mem_extremePoints_measure_univ_eq, ErgodicSMul.iff_mem_extremePoints
• TauCeti.MeasureTheory.smulInvariantMeasure_comp, ErgodicSMul.ae_eq_of_comp_eq: a mixture of invariant measures is invariant, and an ergodic probability measure written as such a mixture has almost every component equal to itself

References

The proofs of eq_smul_of_absolutelyContinuous, eq_of_absolutelyContinuous_measure_univ_eq, mem_extremePoints_measure_univ_eq and of_mem_extremePoints_measure_univ_eq are adapted from Mathlib's Mathlib/Dynamics/Ergodic/Extreme.lean by Yury Kudryashov, transposed from a single measure-preserving map to an action; ae_eq_const_of_forall_ae_eq_comp_smul₀ follows PreErgodic.ae_eq_const_of_ae_eq_comp in Mathlib/Dynamics/Ergodic/Function.lean. The same argument for the sortwise relabelling action on relational structures appears in Graphon/RelErgodicExtreme.lean of cameronfreer/graphon (Apache 2.0) at commit 18d47ebb4155d32031090ec3412eb71583a94f69.

Invariant measures and ergodic actions of a scalar multiplication

def TauCeti.MeasureTheory.invariantMeasuresOfMeasureUnivEq (G : Type u_3) (X : Type u_4) [SMul G X] [MeasurableSpace X] (c : ENNReal) : Set (MeasureTheory.Measure X)

The G-invariant measures on X of total mass c, a convex set of measures.

Equations

• TauCeti.MeasureTheory.invariantMeasuresOfMeasureUnivEq G X c = {ν : MeasureTheory.Measure X | MeasureTheory.SMulInvariantMeasure G X ν ∧ ν Set.univ = c}

@[simp]

theorem TauCeti.MeasureTheory.mem_invariantMeasuresOfMeasureUnivEq_iff {G : Type u_1} {X : Type u_2} [SMul G X] {m : MeasurableSpace X} {ν : MeasureTheory.Measure X} {c : ENNReal} : ν ∈ invariantMeasuresOfMeasureUnivEq G X c ↔ MeasureTheory.SMulInvariantMeasure G X ν ∧ ν Set.univ = c

Membership in the invariant measures of total mass c.

theorem TauCeti.MeasureTheory.convex_invariantMeasuresOfMeasureUnivEq {G : Type u_1} {X : Type u_2} [SMul G X] {m : MeasurableSpace X} {c : ENNReal} : Convex ENNReal (invariantMeasuresOfMeasureUnivEq G X c)

The invariant measures of a fixed total mass form a convex set.

theorem TauCeti.MeasureTheory.smulInvariantMeasure_comp {G : Type u_1} {X : Type u_2} [SMul G X] {m : MeasurableSpace X} [MeasurableConstSMul G X] {Z : Type u_3} {mZ : MeasurableSpace Z} {π : MeasureTheory.Measure Z} {κ : ProbabilityTheory.Kernel Z X} (hκ : ∀ᵐ (z : Z) ∂π, MeasureTheory.SMulInvariantMeasure G X (κ z)) : MeasureTheory.SMulInvariantMeasure G X (π.bind ⇑κ)

A mixture of invariant measures is invariant: if almost every measure of the kernel κ is G-invariant, then so is its mixture κ ∘ₘ π. The integral counterpart of the convexity of invariantMeasuresOfMeasureUnivEq.

theorem ErgodicSMul.ae_eq_const_of_forall_ae_eq_comp_smul₀ {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} (G : Type u_2) [SMul G X] {β : Type u_3} [Nonempty β] [MeasurableSpace β] [MeasurableSpace.CountablySeparated β] [ErgodicSMul G X μ] {g : X → β} (hgm : MeasureTheory.NullMeasurable g μ) (hg : ∀ (c : G), (g ∘ fun (x : X) => c • x) =ᵐ[μ] g) : ∃ (b : β), g =ᵐ[μ] Function.const X b

An almost invariant function under an ergodic action is almost everywhere constant. The target may be any nonempty countably separated measurable space; the action-level analogue of Ergodic.ae_eq_const_of_ae_eq_comp₀.

theorem ErgodicSMul.eq_smul_of_absolutelyContinuous {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} (G : Type u_2) [SMul G X] [MeasurableConstSMul G X] [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [ErgodicSMul G X μ] [MeasureTheory.SMulInvariantMeasure G X ν] (hνμ : ν.AbsolutelyContinuous μ) : ∃ (c : ENNReal), ν = c • μ

An invariant finite measure absolutely continuous with respect to an ergodic one is a multiple of it. The action-level analogue of Ergodic.eq_smul_of_absolutelyContinuous.

theorem ErgodicSMul.eq_of_absolutelyContinuous_measure_univ_eq {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} (G : Type u_2) [SMul G X] [MeasurableConstSMul G X] [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [ErgodicSMul G X μ] [MeasureTheory.SMulInvariantMeasure G X ν] (hνμ : ν.AbsolutelyContinuous μ) (huniv : ν Set.univ = μ Set.univ) : ν = μ

An invariant finite measure absolutely continuous with respect to an ergodic one, of the same total mass, equals it. The action-level analogue of Ergodic.eq_of_absolutelyContinuous_measure_univ_eq.

theorem ErgodicSMul.eq_of_absolutelyContinuous {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} (G : Type u_2) [SMul G X] [MeasurableConstSMul G X] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [ErgodicSMul G X μ] [MeasureTheory.SMulInvariantMeasure G X ν] (hνμ : ν.AbsolutelyContinuous μ) : ν = μ

An invariant probability measure absolutely continuous with respect to an ergodic one equals it.

theorem ErgodicSMul.mem_extremePoints_measure_univ_eq {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {G : Type u_2} [SMul G X] [MeasurableConstSMul G X] [MeasureTheory.IsFiniteMeasure μ] [ErgodicSMul G X μ] : μ ∈ Set.extremePoints ENNReal (TauCeti.MeasureTheory.invariantMeasuresOfMeasureUnivEq G X (μ Set.univ))

An ergodic finite measure is an extreme point of the invariant measures of its total mass.

theorem ErgodicSMul.mem_extremePoints {X : Type u_1} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {G : Type u_2} [SMul G X] [MeasurableConstSMul G X] [MeasureTheory.IsProbabilityMeasure μ] [ErgodicSMul G X μ] : μ ∈ Set.extremePoints ENNReal (TauCeti.MeasureTheory.invariantMeasuresOfMeasureUnivEq G X 1)

An ergodic probability measure is an extreme point of the invariant measures of total mass one, the invariant probability measures.

The reverse direction, for a countable group action

theorem ErgodicSMul.of_mem_extremePoints_measure_univ_eq {G : Type u_1} {X : Type u_2} [Group G] [Countable G] [MulAction G X] {m : MeasurableSpace X} [MeasurableConstSMul G X] {μ : MeasureTheory.Measure X} {c : ENNReal} (hc : c ≠ ⊤) (h : μ ∈ Set.extremePoints ENNReal (TauCeti.MeasureTheory.invariantMeasuresOfMeasureUnivEq G X c)) : ErgodicSMul G X μ

An extreme invariant measure of finite total mass is ergodic.

theorem ErgodicSMul.of_mem_extremePoints {G : Type u_1} {X : Type u_2} [Group G] [Countable G] [MulAction G X] {m : MeasurableSpace X} [MeasurableConstSMul G X] {μ : MeasureTheory.Measure X} (h : μ ∈ Set.extremePoints ENNReal (TauCeti.MeasureTheory.invariantMeasuresOfMeasureUnivEq G X 1)) : ErgodicSMul G X μ

An extreme invariant probability measure is ergodic: an extreme point of the invariant measures of total mass one is ergodic.

theorem ErgodicSMul.iff_mem_extremePoints_measure_univ_eq {G : Type u_1} {X : Type u_2} [Group G] [Countable G] [MulAction G X] {m : MeasurableSpace X} [MeasurableConstSMul G X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] : ErgodicSMul G X μ ↔ μ ∈ Set.extremePoints ENNReal (TauCeti.MeasureTheory.invariantMeasuresOfMeasureUnivEq G X (μ Set.univ))

Ergodicity is extremality for a countable group action, among the invariant measures of the same finite total mass.

theorem ErgodicSMul.iff_mem_extremePoints {G : Type u_1} {X : Type u_2} [Group G] [Countable G] [MulAction G X] {m : MeasurableSpace X} [MeasurableConstSMul G X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] : ErgodicSMul G X μ ↔ μ ∈ Set.extremePoints ENNReal (TauCeti.MeasureTheory.invariantMeasuresOfMeasureUnivEq G X 1)

Ergodicity is extremality for a countable group action: an invariant probability measure is ergodic if and only if it is an extreme point of the invariant measures of total mass one, the invariant probability measures.

Integral decompositions of an ergodic measure

theorem ErgodicSMul.ae_eq_of_comp_eq {G : Type u_1} {X : Type u_2} {Z : Type u_3} [SMul G X] {m : MeasurableSpace X} [MeasurableConstSMul G X] {mZ : MeasurableSpace Z} {μ : MeasureTheory.Measure X} {π : MeasureTheory.Measure Z} {κ : ProbabilityTheory.Kernel Z X} [MeasurableSpace.CountablyGenerated X] [MeasureTheory.IsProbabilityMeasure μ] [ErgodicSMul G X μ] [ProbabilityTheory.IsMarkovKernel κ] (hκ : ∀ᵐ (z : Z) ∂π, MeasureTheory.SMulInvariantMeasure G X (κ z)) (hμ : π.bind ⇑κ = μ) : ∀ᵐ (z : Z) ∂π, κ z = μ

An ergodic probability measure is not a nontrivial mixture of invariant measures. If μ is the mixture κ ∘ₘ π of a Markov kernel whose measures are almost all invariant, then almost every κ z equals μ. This is the integral form of mem_extremePoints: an extreme point of a convex set is not a proper finite convex combination, and an ergodic measure is not even a proper integral one.