Ergodic group actions #
A group action of G on a space α with measure μ is called ergodic,
if for any (null) measurable set s,
if it is a.e.-invariant under each scalar multiplication (g • ·), g : G,
then it is either null or conull.
class
ErgodicVAdd
(G : Type u_1)
(α : Type u_2)
[VAdd G α]
{x✝ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
extends MeasureTheory.VAddInvariantMeasure G α μ :
An additive group action of G on a space α with measure μ is called ergodic,
if for any (null) measurable set s,
if it is a.e.-invariant under each scalar addition (g +ᵥ ·), g : G,
then it is either null or conull.
- measure_preimage_vadd (c : G) ⦃s : Set α⦄ : MeasurableSet s → μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s
- aeconst_of_forall_preimage_vadd_ae_eq {s : Set α} : MeasurableSet s → (∀ (g : G), (fun (x : α) => g +ᵥ x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
Instances
class
ErgodicSMul
(G : Type u_1)
(α : Type u_2)
[SMul G α]
{x✝ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
extends MeasureTheory.SMulInvariantMeasure G α μ :
A group action of G on a space α with measure μ is called ergodic,
if for any (null) measurable set s,
if it is a.e.-invariant under each scalar multiplication (g • ·), g : G,
then it is either null or conull.
- measure_preimage_smul (c : G) ⦃s : Set α⦄ : MeasurableSet s → μ ((fun (x : α) => c • x) ⁻¹' s) = μ s
- aeconst_of_forall_preimage_smul_ae_eq {s : Set α} : MeasurableSet s → (∀ (g : G), (fun (x : α) => g • x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
Instances
theorem
ergodicSMul_iff
(G : Type u_1)
(α : Type u_2)
[SMul G α]
{x✝ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
:
ErgodicSMul G α μ ↔ MeasureTheory.SMulInvariantMeasure G α μ ∧ ∀ {s : Set α},
MeasurableSet s →
(∀ (g : G), (fun (x : α) => g • x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
theorem
ergodicVAdd_iff
(G : Type u_1)
(α : Type u_2)
[VAdd G α]
{x✝ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
:
ErgodicVAdd G α μ ↔ MeasureTheory.VAddInvariantMeasure G α μ ∧ ∀ {s : Set α},
MeasurableSet s →
(∀ (g : G), (fun (x : α) => g +ᵥ x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
theorem
MeasureTheory.aeconst_of_forall_preimage_smul_ae_eq
(G : Type u_1)
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[SMul G α]
[ErgodicSMul G α μ]
{s : Set α}
(hm : MeasureTheory.NullMeasurableSet s μ)
(h : ∀ (g : G), (fun (x : α) => g • x) ⁻¹' s =ᵐ[μ] s)
:
theorem
MeasureTheory.aeconst_of_forall_preimage_vadd_ae_eq
(G : Type u_1)
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[VAdd G α]
[ErgodicVAdd G α μ]
{s : Set α}
(hm : MeasureTheory.NullMeasurableSet s μ)
(h : ∀ (g : G), (fun (x : α) => g +ᵥ x) ⁻¹' s =ᵐ[μ] s)
:
theorem
MeasureTheory.aeconst_of_forall_smul_ae_eq
(G : Type u_1)
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Group G]
[MulAction G α]
[ErgodicSMul G α μ]
{s : Set α}
(hm : MeasureTheory.NullMeasurableSet s μ)
(h : ∀ (g : G), g • s =ᵐ[μ] s)
:
theorem
MeasureTheory.aeconst_of_forall_vadd_ae_eq
(G : Type u_1)
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[AddGroup G]
[AddAction G α]
[ErgodicVAdd G α μ]
{s : Set α}
(hm : MeasureTheory.NullMeasurableSet s μ)
(h : ∀ (g : G), g +ᵥ s =ᵐ[μ] s)
:
theorem
MulAction.aeconst_of_aestabilizer_eq_top
(G : Type u_1)
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Group G]
[MulAction G α]
[ErgodicSMul G α μ]
{s : Set α}
(hm : MeasureTheory.NullMeasurableSet s μ)
(h : MulAction.aestabilizer G μ s = ⊤)
:
theorem
AddAction.aeconst_of_aestabilizer_eq_top
(G : Type u_1)
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[AddGroup G]
[AddAction G α]
[ErgodicVAdd G α μ]
{s : Set α}
(hm : MeasureTheory.NullMeasurableSet s μ)
(h : AddAction.aestabilizer G μ s = ⊤)
:
theorem
ErgodicSMul.of_aestabilizer
(G : Type u_1)
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Group G]
[MulAction G α]
[MeasureTheory.SMulInvariantMeasure G α μ]
(h : ∀ (s : Set α), MeasurableSet s → MulAction.aestabilizer G μ s = ⊤ → Filter.EventuallyConst s (MeasureTheory.ae μ))
:
ErgodicSMul G α μ
theorem
MeasureTheory.ergodicSMul_iterateMulAct
{α : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → α}
(hf : Measurable f)
:
ErgodicSMul (IterateMulAct f) α μ ↔ Ergodic f μ