Countable group actions: almost invariant events versus invariant events

Mathlib's ErgodicSMul is phrased with almost invariant events: an action is ergodic when every measurable s with (g • ·) ⁻¹' s =ᵐ[μ] s for all g is null or conull. Concrete σ-algebras of invariant events — the invariant σ-algebra of a map, or the exchangeable σ-algebra of path space — instead collect the exactly invariant events, those with (g • ·) ⁻¹' s = s.

For a countable group the two formulations agree up to null sets: the saturation ⋃ g, g • s is exactly invariant and, being a countable union of sets each almost equal to s, almost equal to s. This file records that saturation (exists_smul_invariant_ae_eq) and the resulting criterion (ergodicSMul_of_forall_smul_invariant): to prove a countable action ergodic it suffices to handle exactly invariant events.

Countability is essential and is not a technical convenience: the saturation of an almost invariant set by an uncountable group need not be measurable, let alone almost equal to the original set.

No measure invariance is needed for the saturation itself; SMulInvariantMeasure enters only because ErgodicSMul extends it.

theorem TauCeti.MeasureTheory.exists_smul_invariant_ae_eq {G : Type u_1} {X : Type u_2} [Group G] [Countable G] [MeasurableSpace X] [MulAction G X] [MeasurableConstSMul G X] {μ : MeasureTheory.Measure X} {s : Set X} (hs : MeasurableSet s) (hinv : ∀ (g : G), (fun (x : X) => g • x) ⁻¹' s =ᵐ[μ] s) : ∃ (t : Set X), MeasurableSet t ∧ (∀ (g : G), (fun (x : X) => g • x) ⁻¹' t = t) ∧ t =ᵐ[μ] s

An almost invariant event of a countable group action is almost equal to an exactly invariant one. The witness is the saturation ⋃ g, g • s.

This needs no invariance hypothesis on μ: each g • s is already almost equal to s, because g • s is the preimage of s under (g⁻¹ • ·).

theorem TauCeti.MeasureTheory.ergodicSMul_of_forall_smul_invariant {G : Type u_1} {X : Type u_2} [Group G] [Countable G] [MeasurableSpace X] [MulAction G X] [MeasurableConstSMul G X] {μ : MeasureTheory.Measure X} [MeasureTheory.SMulInvariantMeasure G X μ] (h : ∀ (t : Set X), MeasurableSet t → (∀ (g : G), (fun (x : X) => g • x) ⁻¹' t = t) → Filter.EventuallyEmptyOrUniv t (MeasureTheory.ae μ)) : ErgodicSMul G X μ

Ergodicity of a countable group action can be tested on exactly invariant events.

Together with MeasureTheory.aeconst_of_forall_preimage_smul_ae_eq this reduces ergodicity of a countable action to a zero-one law for the σ-algebra of exactly invariant events.