Defs

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

Statistics

Metric	Count
Definitions IsAddLeftInvariant, IsAddRightInvariant, IsMulLeftInvariant, IsMulRightInvariant, SMulInvariantMeasure, VAddInvariantMeasure	6
Theorems map_add_left_eq_self, vaddInvariantMeasure, map_add_right_eq_self, toVAddInvariantMeasure_op, map_mul_left_eq_self, smulInvariantMeasure, map_mul_right_eq_self, toSMulInvariantMeasure_op, instSMulInvariantMeasureSubtypeMemSubmonoidOfIsMulLeftInvariant, instVAddInvariantMeasureSubtypeMemAddSubmonoidOfIsAddLeftInvariant, measure_preimage_smul, measure_preimage_vadd, smulInvariantMeasure_iff, vaddInvariantMeasure_iff	14
Total	20

MeasureTheory

Definitions

Name	Category	Theorems
SMulInvariantMeasure 📖	CompData	19 math math: SMulInvariantMeasure.smul, smulInvariantMeasure_iterateMulAct, Measure.IsMulRightInvariant.toSMulInvariantMeasure_op, Subgroup.smulInvariantMeasure, UpperHalfPlane.instSMulInvariantMeasureGeneralLinearGroupFinOfNatNatRealVolume, instSMulInvariantMeasureHausdorffMeasureOfIsIsometricSMul, MeasurePreserving.smulInvariantMeasure_iterateMulAct, SMulInvariantMeasure.zero, SMulInvariantMeasure.add, ergodicSMul_iff, smulInvariantMeasure_iff, QuotientMeasureEqMeasurePreimage.smulInvariantMeasure_quotient, smulInvariantMeasure_map, ErgodicSMul.toSMulInvariantMeasure, smulInvariantMeasure_tfae, SMulInvariantMeasure.smul_nnreal, Measure.instSMulInvariantMeasureSubtypeMemSubmonoidOfIsMulLeftInvariant, smulInvariantMeasure_map_smul, Measure.IsMulLeftInvariant.smulInvariantMeasure
VAddInvariantMeasure 📖	CompData	19 math math: vaddInvariantMeasure_iff, Measure.IsAddLeftInvariant.vaddInvariantMeasure, VAddInvariantMeasure.add, vaddInvariantMeasure_map, ErgodicVAdd.toVAddInvariantMeasure, Measure.instVAddInvariantMeasureSubtypeMemAddSubmonoidOfIsAddLeftInvariant, Measure.IsAddRightInvariant.toVAddInvariantMeasure_op, instVAddInvariantMeasureEuclideanHausdorffMeasureOfIsIsometricVAdd, ergodicVAdd_iff, Subgroup.vaddInvariantMeasure, vaddInvariantMeasure_iterateAddAct, VAddInvariantMeasure.vadd_nnreal, VAddInvariantMeasure.zero, instVAddInvariantMeasureHausdorffMeasureOfIsIsometricVAdd, MeasurePreserving.vaddInvariantMeasure_iterateAddAct, VAddInvariantMeasure.vadd, vaddInvariantMeasure_map_vadd, AddQuotientMeasureEqMeasurePreimage.vaddInvariantMeasure_quotient, vaddInvariantMeasure_tfae

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smulInvariantMeasure_iff 📖	mathematical	—	SMulInvariantMeasure DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.preimage	—	—
vaddInvariantMeasure_iff 📖	mathematical	—	VAddInvariantMeasure DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.preimage HVAdd.hVAdd instHVAdd	—	—

MeasureTheory.Measure

Definitions

Name	Category	Theorems
IsAddLeftInvariant 📖	CompData	19 math math: MeasureTheory.isMulLeftInvariant_map_add_right, MeasureTheory.isAddLeftInvariant_map, MeasureTheory.forall_measure_preimage_add_iff, instIsAddLeftInvariantEuclideanHausdorffMeasureOfIsIsometricVAdd, instIsAddLeftInvariantMeasure, instIsAddLeftInvariantForallVolumeOfMeasurableAddOfSigmaFinite, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addInvariantMeasure_quotient, isAddLeftInvariant_addHaarMeasure, prod.instIsAddLeftInvariant, IsAddLeftInvariant.comap, MeasureTheory.isAddLeftInvariant_smul, IsAddHaarMeasure.toIsAddLeftInvariant, instIsAddLeftInvariantCount, neg.instIsAddLeftInvariant, MeasureTheory.isAddLeftInvariant_map_vadd, MeasureTheory.instIsAddLeftInvariantHausdorffMeasureOfIsIsometricVAdd, MeasureTheory.isAddLeftInvariant_smul_nnreal, pi.isAddLeftInvariant, MeasureTheory.Pi.isAddLeftInvariant_volume
IsAddRightInvariant 📖	CompData	14 math math: MeasureTheory.isMulRightInvariant_map_add_left, instIsAddRightInvariantForallVolumeOfMeasurableAddOfSigmaFinite, MeasureTheory.isAddRightInvariant_map_vadd, pi.isAddRightInvariant, MeasureTheory.instIsAddRightInvariantHausdorffMeasureOfIsIsometricVAddAddOpposite, prod.instIsAddRightInvariant, IsAddRightInvariant.comap, neg.instIsAddRightInvariant, MeasureTheory.isAddRightInvariant_smul, instIsAddRightInvariantCount, MeasureTheory.isAddRightInvariant_smul_nnreal, MeasureTheory.IsAddLeftInvariant.isAddRightInvariant, instIsAddRightInvariantEuclideanHausdorffMeasureOfIsIsometricVAddAddOpposite, MeasureTheory.forall_measure_preimage_add_right_iff
IsMulLeftInvariant 📖	CompData	17 math math: MeasureTheory.instIsMulLeftInvariantHausdorffMeasureOfIsIsometricSMul, IsHaarMeasure.toIsMulLeftInvariant, isMulLeftInvariant_haarMeasure, MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient, MeasureTheory.isMulLeftInvariant_map_smul, instIsMulLeftInvariantCount, MeasureTheory.isMulLeftInvariant_smul, instIsMulLeftInvariantForallVolumeOfMeasurableMulOfSigmaFinite, inv.instIsMulLeftInvariant, MeasureTheory.forall_measure_preimage_mul_iff, prod.instIsMulLeftInvariant, pi.isMulLeftInvariant, MeasureTheory.isMulLeftInvariant_smul_nnreal, MeasureTheory.isMulLeftInvariant_map, MeasureTheory.Pi.isMulLeftInvariant_volume, IsMulLeftInvariant.comap, MeasureTheory.isMulLeftInvariant_map_mul_right
IsMulRightInvariant 📖	CompData	13 math math: IsMulRightInvariant.comap, MeasureTheory.isMulRightInvariant_map_mul_left, prod.instIsMulRightInvariant, MeasureTheory.isMulRightInvariant_smul, MeasureTheory.IsMulLeftInvariant.isMulRightInvariant, instIsMulRightInvariantForallVolumeOfMeasurableMulOfSigmaFinite, pi.isMulRightInvariant, MeasureTheory.instIsMulRightInvariantHausdorffMeasureOfIsIsometricSMulMulOpposite, inv.instIsMulRightInvariant, MeasureTheory.isMulRightInvariant_smul_nnreal, instIsMulRightInvariantCount, MeasureTheory.isMulRightInvariant_map_smul, MeasureTheory.forall_measure_preimage_mul_right_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSMulInvariantMeasureSubtypeMemSubmonoidOfIsMulLeftInvariant 📖	mathematical	—	MeasureTheory.SMulInvariantMeasure Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.smul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Monoid.toMulAction	—	MeasureTheory.SMulInvariantMeasure.measure_preimage_smul IsMulLeftInvariant.smulInvariantMeasure
instVAddInvariantMeasureSubtypeMemAddSubmonoidOfIsAddLeftInvariant 📖	mathematical	—	MeasureTheory.VAddInvariantMeasure AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.vadd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction AddMonoid.toAddAction	—	MeasureTheory.VAddInvariantMeasure.measure_preimage_vadd IsAddLeftInvariant.vaddInvariantMeasure

MeasureTheory.Measure.IsAddLeftInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_add_left_eq_self 📖	mathematical	—	MeasureTheory.Measure.map	—	—
vaddInvariantMeasure 📖	mathematical	—	MeasureTheory.VAddInvariantMeasure Add.toVAdd	—	MeasureTheory.Measure.measure_preimage_of_map_eq_self map_add_left_eq_self MeasurableSet.nullMeasurableSet

MeasureTheory.Measure.IsAddRightInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_add_right_eq_self 📖	mathematical	—	MeasureTheory.Measure.map	—	—
toVAddInvariantMeasure_op 📖	mathematical	—	MeasureTheory.VAddInvariantMeasure AddOpposite Add.toVAddAddOpposite	—	MeasureTheory.Measure.measure_preimage_of_map_eq_self map_add_right_eq_self MeasurableSet.nullMeasurableSet

MeasureTheory.Measure.IsMulLeftInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mul_left_eq_self 📖	mathematical	—	MeasureTheory.Measure.map	—	—
smulInvariantMeasure 📖	mathematical	—	MeasureTheory.SMulInvariantMeasure	—	MeasureTheory.Measure.measure_preimage_of_map_eq_self map_mul_left_eq_self MeasurableSet.nullMeasurableSet

MeasureTheory.Measure.IsMulRightInvariant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mul_right_eq_self 📖	mathematical	—	MeasureTheory.Measure.map	—	—
toSMulInvariantMeasure_op 📖	mathematical	—	MeasureTheory.SMulInvariantMeasure MulOpposite Mul.toSMulMulOpposite	—	MeasureTheory.Measure.measure_preimage_of_map_eq_self map_mul_right_eq_self MeasurableSet.nullMeasurableSet

MeasureTheory.SMulInvariantMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measure_preimage_smul 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.preimage	—	—

MeasureTheory.VAddInvariantMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measure_preimage_vadd 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.preimage HVAdd.hVAdd instHVAdd	—	—

---

← Back to Index