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
MulAction.aestabilizer
(G : Type u_1)
{α : Type u_2}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SMulInvariantMeasure G α μ]
(s : 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' := ⋯ }
Instances For
def
AddAction.aestabilizer
(G : Type u_1)
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[MeasureTheory.VAddInvariantMeasure G α μ]
(s : Set α)
:
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' := ⋯ }
Instances For
@[simp]
theorem
AddAction.coe_aestabilizer
(G : Type u_1)
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[MeasureTheory.VAddInvariantMeasure G α μ]
(s : Set α)
:
↑(AddAction.aestabilizer G μ s) = {g : G | g +ᵥ s =ᵐ[μ] s}
@[simp]
theorem
MulAction.coe_aestabilizer
(G : Type u_1)
{α : Type u_2}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SMulInvariantMeasure G α μ]
(s : Set α)
:
↑(MulAction.aestabilizer G μ s) = {g : G | g • s =ᵐ[μ] s}
@[simp]
theorem
MulAction.mem_aestabilizer
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SMulInvariantMeasure G α μ]
{g : G}
{s : Set α}
:
@[simp]
theorem
AddAction.mem_aestabilizer
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.VAddInvariantMeasure G α μ]
{g : G}
{s : Set α}
:
theorem
MulAction.stabilizer_le_aestabilizer
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SMulInvariantMeasure G α μ]
(s : Set α)
:
MulAction.stabilizer G s ≤ MulAction.aestabilizer G μ s
theorem
AddAction.stabilizer_le_aestabilizer
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.VAddInvariantMeasure G α μ]
(s : Set α)
:
AddAction.stabilizer G s ≤ AddAction.aestabilizer G μ s
@[simp]
theorem
MulAction.aestabilizer_empty
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SMulInvariantMeasure G α μ]
:
MulAction.aestabilizer G μ ∅ = ⊤
@[simp]
theorem
AddAction.aestabilizer_empty
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.VAddInvariantMeasure G α μ]
:
AddAction.aestabilizer G μ ∅ = ⊤
@[simp]
theorem
MulAction.aestabilizer_univ
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SMulInvariantMeasure G α μ]
:
MulAction.aestabilizer G μ Set.univ = ⊤
@[simp]
theorem
AddAction.aestabilizer_univ
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.VAddInvariantMeasure G α μ]
:
AddAction.aestabilizer G μ Set.univ = ⊤
theorem
MulAction.aestabilizer_congr
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SMulInvariantMeasure G α μ]
{s t : Set α}
(h : s =ᵐ[μ] t)
:
MulAction.aestabilizer G μ s = MulAction.aestabilizer G μ t
theorem
AddAction.aestabilizer_congr
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.VAddInvariantMeasure G α μ]
{s t : Set α}
(h : s =ᵐ[μ] t)
:
AddAction.aestabilizer G μ s = AddAction.aestabilizer G μ t
theorem
MulAction.aestabilizer_of_aeconst
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SMulInvariantMeasure G α μ]
{s : Set α}
(hs : Filter.EventuallyConst s (MeasureTheory.ae μ))
:
MulAction.aestabilizer G μ 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 α}
[MeasureTheory.SMulInvariantMeasure G α μ]
{x y : G}
{s : Set α}
(hs : x • s =ᵐ[μ] s)
(hy : y ∈ Subgroup.zpowers x)
:
theorem
MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.VAddInvariantMeasure G α μ]
{x y : G}
{s : Set α}
(hs : x +ᵥ s =ᵐ[μ] s)
(hy : y ∈ AddSubgroup.zmultiples x)
:
theorem
MeasureTheory.inv_smul_ae_eq_self
{G : Type u_1}
{α : Type u_2}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SMulInvariantMeasure G α μ]
{x : G}
{s : Set α}
(hs : x • s =ᵐ[μ] s)
:
theorem
MeasureTheory.neg_vadd_ae_eq_self
{G : Type u_1}
{α : Type u_2}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.VAddInvariantMeasure G α μ]
{x : G}
{s : Set α}
(hs : x +ᵥ s =ᵐ[μ] s)
: