Documentation Verification Report

AEStabilizer

📁 Source: Mathlib/MeasureTheory/Group/AEStabilizer.lean

Statistics

Metric	Count
Definitions `aestabilizer`, `aestabilizer`	2
Theorems `aestabilizer_congr`, `aestabilizer_empty`, `aestabilizer_univ`, `coe_aestabilizer`, `mem_aestabilizer`, `stabilizer_le_aestabilizer`, `inv_smul_ae_eq_self`, `neg_vadd_ae_eq_self`, `smul_ae_eq_self_of_mem_zpowers`, `vadd_ae_eq_self_of_mem_zmultiples`, `aestabilizer_congr`, `aestabilizer_empty`, `aestabilizer_of_aeconst`, `aestabilizer_univ`, `coe_aestabilizer`, `mem_aestabilizer`, `stabilizer_le_aestabilizer`	17
Total	19

AddAction

Definitions

Name	Category	Theorems
`aestabilizer` 📖	CompOp	6 math math: `aestabilizer_congr`, `aestabilizer_empty`, `stabilizer_le_aestabilizer`, `aestabilizer_univ`, `coe_aestabilizer`, `mem_aestabilizer`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aestabilizer_congr` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`aestabilizer`	—	`MeasureTheory.Measure.instOuterMeasureClass` `AddSubgroup.ext` `mem_aestabilizer` `Filter.EventuallyEq.congr_right` `Filter.EventuallyEq.congr_left` `MeasureTheory.vadd_set_ae_eq`
`aestabilizer_empty` 📖	mathematical	—	`aestabilizer` `Set` `Set.instEmptyCollection` `Top.top` `AddSubgroup` `AddSubgroup.instTop`	—	`top_unique` `MeasureTheory.Measure.instOuterMeasureClass` `mem_aestabilizer` `Set.vadd_set_empty` `Filter.EventuallyEq.refl`
`aestabilizer_univ` 📖	mathematical	—	`aestabilizer` `Set.univ` `Top.top` `AddSubgroup` `AddSubgroup.instTop`	—	`top_unique` `MeasureTheory.Measure.instOuterMeasureClass` `mem_aestabilizer` `Set.vadd_set_univ` `MeasureTheory.ae_eq_univ` `Set.compl_univ` `MeasureTheory.measure_empty`
`coe_aestabilizer` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `aestabilizer` `setOf` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	—
`mem_aestabilizer` 📖	mathematical	—	`AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `aestabilizer` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	—
`stabilizer_le_aestabilizer` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `stabilizer` `Set` `Set.addActionSet` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `aestabilizer`	—	`MeasureTheory.Measure.instOuterMeasureClass` `mem_aestabilizer` `mem_stabilizer_iff` `Filter.EventuallyEq.refl`

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_smul_ae_eq_self` 📖	mathematical	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Measure.instOuterMeasureClass` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass`
`neg_vadd_ae_eq_self` 📖	mathematical	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Measure.instOuterMeasureClass` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `AddSubgroup.instAddSubgroupClass`
`smul_ae_eq_self_of_mem_zpowers` 📖	—	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers`	—	—	`Measure.instOuterMeasureClass` `Subgroup.zpowers_le` `MulAction.mem_aestabilizer`
`vadd_ae_eq_self_of_mem_zmultiples` 📖	—	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	—	—	`Measure.instOuterMeasureClass` `AddSubgroup.zmultiples_le` `AddAction.mem_aestabilizer`

MulAction

Definitions

Name	Category	Theorems
`aestabilizer` 📖	CompOp	7 math math: `mem_aestabilizer`, `stabilizer_le_aestabilizer`, `aestabilizer_empty`, `coe_aestabilizer`, `aestabilizer_of_aeconst`, `aestabilizer_congr`, `aestabilizer_univ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aestabilizer_congr` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`aestabilizer`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Subgroup.ext` `mem_aestabilizer` `Filter.EventuallyEq.congr_right` `Filter.EventuallyEq.congr_left` `MeasureTheory.smul_set_ae_eq`
`aestabilizer_empty` 📖	mathematical	—	`aestabilizer` `Set` `Set.instEmptyCollection` `Top.top` `Subgroup` `Subgroup.instTop`	—	`top_unique` `MeasureTheory.Measure.instOuterMeasureClass` `Set.smul_set_empty`
`aestabilizer_of_aeconst` 📖	mathematical	`Filter.EventuallyConst` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`aestabilizer` `Top.top` `Subgroup` `Subgroup.instTop`	—	`MeasureTheory.Measure.instOuterMeasureClass` `top_unique` `Filter.eventuallyConst_set'` `aestabilizer_congr` `aestabilizer_empty` `aestabilizer_univ`
`aestabilizer_univ` 📖	mathematical	—	`aestabilizer` `Set.univ` `Top.top` `Subgroup` `Subgroup.instTop`	—	`top_unique` `MeasureTheory.Measure.instOuterMeasureClass` `Set.smul_set_univ` `Set.compl_univ` `MeasureTheory.measure_empty`
`coe_aestabilizer` 📖	mathematical	—	`SetLike.coe` `Subgroup` `Subgroup.instSetLike` `aestabilizer` `setOf` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	—
`mem_aestabilizer` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `aestabilizer` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	—
`stabilizer_le_aestabilizer` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `stabilizer` `Set` `Set.mulActionSet` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `aestabilizer`	—	`MeasureTheory.Measure.instOuterMeasureClass`

---

← Back to Index