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.

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

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

• AddAction.aestabilizer G μ s = { carrier := {g : G | g +ᵥ s =ᵐ[μ] s}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

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

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

@[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}

@[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}

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

• MulAction.aestabilizer G μ s = { carrier := {g : G | g • s =ᵐ[μ] s}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[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

theorem AddAction.stabilizer_le_aestabilizer {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ] (s : Set α), AddAction.stabilizer G s ≤ AddAction.aestabilizer G μ s

theorem MulAction.stabilizer_le_aestabilizer {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ] (s : Set α), MulAction.stabilizer G s ≤ MulAction.aestabilizer G μ s

@[simp]

theorem AddAction.aestabilizer_empty {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ], AddAction.aestabilizer G μ ∅ = ⊤

@[simp]

theorem MulAction.aestabilizer_empty {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ], MulAction.aestabilizer G μ ∅ = ⊤

@[simp]

theorem AddAction.aestabilizer_univ {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.VAddInvariantMeasure G α μ], AddAction.aestabilizer G μ Set.univ = ⊤

@[simp]

theorem MulAction.aestabilizer_univ {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ], MulAction.aestabilizer G μ Set.univ = ⊤

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 =ᵐ[μ] t → AddAction.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 =ᵐ[μ] t → MulAction.aestabilizer G μ s = MulAction.aestabilizer G μ t

theorem MulAction.aestabilizer_of_aeconst {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] : ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α}, Filter.EventuallyConst s (MeasureTheory.ae μ) → MulAction.aestabilizer G μ s = ⊤

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 =ᵐ[μ] s → y ∈ AddSubgroup.zmultiples x_1 → y +ᵥ 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 =ᵐ[μ] s → y ∈ Subgroup.zpowers x_1 → y • 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 =ᵐ[μ] s → x_1⁻¹ • s =ᵐ[μ] s