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.EventuallyEmptyOrUniv 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.EventuallyEmptyOrUniv 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.EventuallyEmptyOrUniv 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.EventuallyEmptyOrUniv s (MeasureTheory.ae μ)
theorem MeasureTheory.aeconst_of_forall_preimage_smul_ae_eq (G : Type u_1) {α : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [SMul G α] [ErgodicSMul G α μ] {s : Set α} (hm : 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 α} {μ : Measure α} [VAdd G α] [ErgodicVAdd G α μ] {s : Set α} (hm : 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 α} {μ : Measure α} [Group G] [MulAction G α] [ErgodicSMul G α μ] {s : Set α} (hm : 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 α} {μ : Measure α} [AddGroup G] [AddAction G α] [ErgodicVAdd G α μ] {s : Set α} (hm : 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 : 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 : 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.EventuallyEmptyOrUniv s (MeasureTheory.ae μ)) :
ErgodicSMul G α μ
theorem MeasureTheory.ergodicSMul_iterateMulAct {α : Type u_2} {m : MeasurableSpace α} {μ : Measure α} {f : α → α} (hf : Measurable f) :