Documentation

Mathlib.Dynamics.Ergodic.Action.Basic

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 :

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.

Instances
    theorem ErgodicVAdd.aeconst_of_forall_preimage_vadd_ae_eq {G : Type u_1} {α : Type u_2} :
    ∀ {inst : 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 :

    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.

    Instances
      theorem ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq {G : Type u_1} {α : Type u_2} :
      ∀ {inst : 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 MeasureTheory.ergodicSMul_iterateMulAct {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αα} (hf : Measurable f) :