Documentation

Mathlib.MeasureTheory.Group.AEStabilizer

A.e. stabilizer of a set #

In this file we define the a.e. stabilizer of a set under a measure preserving group action.

The a.e. stabilizer MulAction.aestabilizer G μ s of a set s is the set of the elements g : G such that s is a.e.-invariant under (g • ·).

For a measure preserving group action, this set is a subgroup of G. If the set is null or conull, then this subgroup is the whole group. The converse is true for an ergodic action and a null-measurable set.

Implementation notes #

We define the a.e. stabilizer as a bundled Subgroup, thus we do not deal with monoid actions.

Also, many lemmas in this file are true for a quasi measure-preserving action, but we don't have the corresponding typeclass.

def AddAction.aestabilizer (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] :
{x : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [inst : MeasureTheory.VAddInvariantMeasure G α μ] → Set αAddSubgroup G

A.e. stabilizer of a set under an additive group action.

Equations
Instances For
    theorem AddAction.aestabilizer.proof_1 (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] :
    ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.VAddInvariantMeasure G α μ] (s : Set α) {g₁ g₂ : G}, g₁ {g : G | g +ᵥ s =ᵐ[μ] s}g₂ {g : G | g +ᵥ s =ᵐ[μ] s}g₁ + g₂ +ᵥ s =ᵐ[μ] s
    theorem AddAction.aestabilizer.proof_2 (G : Type u_2) {α : Type u_1} [AddGroup G] [AddAction G α] :
    ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), 0 +ᵥ s =ᵐ[μ] s
    theorem AddAction.aestabilizer.proof_3 (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] :
    ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.VAddInvariantMeasure G α μ] (s : Set α) {g : G}, g { carrier := {g : G | g +ᵥ s =ᵐ[μ] s}, add_mem' := , zero_mem' := }.carrier-g { carrier := {g : G | g +ᵥ s =ᵐ[μ] s}, add_mem' := , zero_mem' := }.carrier
    @[simp]
    theorem MulAction.aestabilizer_coe (G : Type u_1) {α : Type u_2} [Group G] [MulAction G α] :
    ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SMulInvariantMeasure G α μ] (s : Set α), (MulAction.aestabilizer G μ s) = {g : G | g s =ᵐ[μ] s}
    @[simp]
    theorem AddAction.aestabilizer_coe (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] :
    ∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.VAddInvariantMeasure G α μ] (s : Set α), (AddAction.aestabilizer G μ s) = {g : G | g +ᵥ s =ᵐ[μ] s}
    def MulAction.aestabilizer (G : Type u_1) {α : Type u_2} [Group G] [MulAction G α] :
    {x : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [inst : MeasureTheory.SMulInvariantMeasure G α μ] → Set αSubgroup G

    A.e. stabilizer of a set under a group action.

    Equations
    Instances For
      @[simp]
      theorem AddAction.mem_aestabilizer {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] :
      ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ] {g : G} {s : Set α}, g AddAction.aestabilizer G μ s g +ᵥ s =ᵐ[μ] s
      @[simp]
      theorem MulAction.mem_aestabilizer {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] :
      ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ] {g : G} {s : Set α}, g MulAction.aestabilizer G μ s g s =ᵐ[μ] s
      @[simp]
      @[simp]
      @[simp]
      theorem AddAction.aestabilizer_univ {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] :
      @[simp]
      theorem MulAction.aestabilizer_univ {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] :
      theorem AddAction.aestabilizer_congr {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] :
      ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ] {s t : Set α}, s =ᵐ[μ] tAddAction.aestabilizer G μ s = AddAction.aestabilizer G μ t
      theorem MulAction.aestabilizer_congr {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] :
      ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ] {s t : Set α}, s =ᵐ[μ] tMulAction.aestabilizer G μ s = MulAction.aestabilizer G μ t
      theorem MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] :
      ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ] {x_1 y : G} {s : Set α}, x_1 +ᵥ s =ᵐ[μ] sy AddSubgroup.zmultiples x_1y +ᵥ s =ᵐ[μ] s
      theorem MeasureTheory.smul_ae_eq_self_of_mem_zpowers {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] :
      ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ] {x_1 y : G} {s : Set α}, x_1 s =ᵐ[μ] sy Subgroup.zpowers x_1y s =ᵐ[μ] s
      theorem MeasureTheory.neg_vadd_ae_eq_self {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] :
      ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ] {x_1 : G} {s : Set α}, x_1 +ᵥ s =ᵐ[μ] s-x_1 +ᵥ s =ᵐ[μ] s
      theorem MeasureTheory.inv_smul_ae_eq_self {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] :
      ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ] {x_1 : G} {s : Set α}, x_1 s =ᵐ[μ] sx_1⁻¹ s =ᵐ[μ] s