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 α]
extends
MeasureTheory.VAddInvariantMeasure
:
{x : MeasurableSpace α} → MeasureTheory.Measure α → Prop
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
theorem
ErgodicVAdd.aeconst_of_forall_preimage_vadd_ae_eq
{G : Type u_1}
{α : Type u_2}
[VAdd G α]
:
∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : ErgodicVAdd G α μ] {s : Set α},
MeasurableSet s → (∀ (g : G), (fun (x : α) => g +ᵥ x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
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 μ)
class
ErgodicSMul
(G : Type u_1)
(α : Type u_2)
[SMul G α]
extends
MeasureTheory.SMulInvariantMeasure
:
{x : MeasurableSpace α} → MeasureTheory.Measure α → Prop
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.aeconst_of_forall_preimage_smul_ae_eq
{G : Type u_1}
{α : Type u_2}
[SMul G α]
:
∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : ErgodicSMul 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_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_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_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
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
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
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
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 μ