Action

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

Statistics

Metric	Count
Definitions	0
Theorems smulInvariantMeasure_iterateMulAct, vaddInvariantMeasure_iterateAddAct, smul, vadd, add, smul, smul_nnreal, zero, add, vadd, vadd_nnreal, zero, eventuallyConst_smul_set_ae, eventuallyConst_vadd_set_ae, isLocallyFiniteMeasure_of_smulInvariant, isLocallyFiniteMeasure_of_vaddInvariant, map_smul, map_vadd, measurePreserving_smul, measurePreserving_vadd, measure_eq_zero_iff_eq_empty_of_smulInvariant, measure_eq_zero_iff_eq_empty_of_vaddInvariant, measure_inter_inv_smul, measure_inter_neg_vadd, measure_inv_smul_inter, measure_inv_smul_sdiff, measure_inv_smul_symmDiff, measure_inv_smul_union, measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero, measure_isOpen_pos_of_smulInvariant_of_ne_zero, measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero, measure_isOpen_pos_of_vaddInvariant_of_ne_zero, measure_neg_vadd_inter, measure_neg_vadd_sdiff, measure_neg_vadd_symmDiff, measure_neg_vadd_union, measure_pos_iff_nonempty_of_smulInvariant, measure_pos_iff_nonempty_of_vaddInvariant, measure_preimage_smul, measure_preimage_smul_le, measure_preimage_smul_null, measure_preimage_smul_of_nullMeasurableSet, measure_preimage_vadd, measure_preimage_vadd_le, measure_preimage_vadd_null, measure_preimage_vadd_of_nullMeasurableSet, measure_sdiff_inv_smul, measure_sdiff_neg_vadd, measure_smul, measure_smul_eq_zero_iff, measure_smul_null, measure_symmDiff_inv_smul, measure_symmDiff_neg_vadd, measure_union_inv_smul, measure_union_neg_vadd, measure_vadd, measure_vadd_eq_zero_iff, measure_vadd_null, smulInvariantMeasure_iterateMulAct, smulInvariantMeasure_map, smulInvariantMeasure_map_smul, smulInvariantMeasure_tfae, smul_ae, smul_mem_ae, smul_set_ae_eq, smul_set_ae_le, tendsto_smul_ae, tendsto_vadd_ae, vaddInvariantMeasure_iterateAddAct, vaddInvariantMeasure_map, vaddInvariantMeasure_map_vadd, vaddInvariantMeasure_tfae, vadd_ae, vadd_mem_ae, vadd_set_ae_eq, vadd_set_ae_le	76
Total	76

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventuallyConst_smul_set_ae 📖	mathematical	—	Filter.EventuallyConst Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass Set.preimage_smul_inv Filter.eventuallyConst_preimage Filter.map_smul smul_ae
eventuallyConst_vadd_set_ae 📖	mathematical	—	Filter.EventuallyConst HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass Set.preimage_vadd_neg Filter.eventuallyConst_preimage Filter.map_vadd vadd_ae
isLocallyFiniteMeasure_of_smulInvariant 📖	mathematical	IsOpen Set.Nonempty	IsLocallyFiniteMeasure	—	IsOpen.exists_smul_mem IsOpen.mem_nhds IsOpen.preimage Continuous.const_smul continuous_id Ne.lt_top measure_preimage_smul
isLocallyFiniteMeasure_of_vaddInvariant 📖	mathematical	IsOpen Set.Nonempty	IsLocallyFiniteMeasure	—	IsOpen.exists_vadd_mem IsOpen.mem_nhds IsOpen.preimage Continuous.const_vadd continuous_id Ne.lt_top measure_preimage_vadd
map_smul 📖	mathematical	—	Measure.map	—	MeasurePreserving.map_eq measurePreserving_smul
map_vadd 📖	mathematical	—	Measure.map HVAdd.hVAdd instHVAdd	—	MeasurePreserving.map_eq measurePreserving_vadd
measurePreserving_smul 📖	mathematical	—	MeasurePreserving	—	MeasurableConstSMul.measurable_const_smul Measure.ext Measure.map_apply SMulInvariantMeasure.measure_preimage_smul
measurePreserving_vadd 📖	mathematical	—	MeasurePreserving HVAdd.hVAdd instHVAdd	—	MeasurableConstVAdd.measurable_const_vadd Measure.ext Measure.map_apply VAddInvariantMeasure.measure_preimage_vadd
measure_eq_zero_iff_eq_empty_of_smulInvariant 📖	mathematical	IsOpen	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal Set.instEmptyCollection	—	not_iff_not pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd measure_pos_iff_nonempty_of_smulInvariant Set.nonempty_iff_ne_empty
measure_eq_zero_iff_eq_empty_of_vaddInvariant 📖	mathematical	IsOpen	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal Set.instEmptyCollection	—	not_iff_not pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd measure_pos_iff_nonempty_of_vaddInvariant Set.nonempty_iff_ne_empty
measure_inter_inv_smul 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instInter Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	measure_smul Set.smul_set_inter smul_smul mul_inv_cancel one_smul
measure_inter_neg_vadd 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instInter HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	measure_vadd Set.vadd_set_inter vadd_vadd add_neg_cancel zero_vadd
measure_inv_smul_inter 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instInter Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_inv measure_inter_inv_smul
measure_inv_smul_sdiff 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSDiff Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_inv measure_sdiff_inv_smul
measure_inv_smul_symmDiff 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_inv measure_symmDiff_inv_smul
measure_inv_smul_union 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instUnion Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_inv measure_union_inv_smul
measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero 📖	mathematical	IsCompact IsOpen Set.Nonempty	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike	—	IsCompact.exists_finite_cover_smul pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd measure_mono_null Measure.instOuterMeasureClass measure_biUnion_null_iff Finset.countable_toSet measure_smul
measure_isOpen_pos_of_smulInvariant_of_ne_zero 📖	mathematical	IsOpen Set.Nonempty	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike	—	Measure.Regular.exists_isCompact_not_null measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero
measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero 📖	mathematical	IsCompact IsOpen Set.Nonempty	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike	—	IsCompact.exists_finite_cover_vadd pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd measure_mono_null Measure.instOuterMeasureClass measure_biUnion_null_iff Finset.countable_toSet measure_vadd
measure_isOpen_pos_of_vaddInvariant_of_ne_zero 📖	mathematical	IsOpen Set.Nonempty	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike	—	Measure.Regular.exists_isCompact_not_null measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero
measure_neg_vadd_inter 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instInter HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg_neg measure_inter_neg_vadd
measure_neg_vadd_sdiff 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSDiff HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg_neg measure_sdiff_neg_vadd
measure_neg_vadd_symmDiff 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg_neg measure_symmDiff_neg_vadd
measure_neg_vadd_union 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instUnion HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	neg_neg measure_union_neg_vadd
measure_pos_iff_nonempty_of_smulInvariant 📖	mathematical	IsOpen	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike Set.Nonempty	—	nonempty_of_measure_ne_zero LT.lt.ne' measure_isOpen_pos_of_smulInvariant_of_ne_zero
measure_pos_iff_nonempty_of_vaddInvariant 📖	mathematical	IsOpen	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike Set.Nonempty	—	nonempty_of_measure_ne_zero LT.lt.ne' measure_isOpen_pos_of_vaddInvariant_of_ne_zero
measure_preimage_smul 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.preimage SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	LE.le.antisymm measure_preimage_smul_le Set.preimage_preimage smul_inv_smul
measure_preimage_smul_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.preimage	—	IsScalarTower.right Measure.outerMeasure_le_iff Eq.le SMulInvariantMeasure.measure_preimage_smul
measure_preimage_smul_null 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.preimage instZeroENNReal	—	eq_bot_mono measure_preimage_smul_le
measure_preimage_smul_of_nullMeasurableSet 📖	mathematical	NullMeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.preimage	—	measure_toMeasurable SMulInvariantMeasure.measure_preimage_smul measurableSet_toMeasurable measure_congr Measure.instOuterMeasureClass tendsto_smul_ae NullMeasurableSet.toMeasurable_ae_eq
measure_preimage_vadd 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.preimage HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	LE.le.antisymm measure_preimage_vadd_le Set.preimage_preimage vadd_neg_vadd
measure_preimage_vadd_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.preimage HVAdd.hVAdd instHVAdd	—	IsScalarTower.right Measure.outerMeasure_le_iff Eq.le VAddInvariantMeasure.measure_preimage_vadd
measure_preimage_vadd_null 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.preimage HVAdd.hVAdd instHVAdd instZeroENNReal	—	eq_bot_mono measure_preimage_vadd_le
measure_preimage_vadd_of_nullMeasurableSet 📖	mathematical	NullMeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.preimage HVAdd.hVAdd instHVAdd	—	measure_toMeasurable VAddInvariantMeasure.measure_preimage_vadd measurableSet_toMeasurable measure_congr Measure.instOuterMeasureClass tendsto_vadd_ae NullMeasurableSet.toMeasurable_ae_eq
measure_sdiff_inv_smul 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSDiff Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	measure_smul Set.smul_set_sdiff smul_smul mul_inv_cancel one_smul
measure_sdiff_neg_vadd 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSDiff HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	measure_vadd Set.vadd_set_sdiff vadd_vadd add_neg_cancel zero_vadd
measure_smul 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	Set.preimage_smul_inv measure_preimage_smul
measure_smul_eq_zero_iff 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instZeroENNReal	—	measure_smul
measure_smul_null 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction instZeroENNReal	—	measure_smul_eq_zero_iff
measure_symmDiff_inv_smul 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	measure_smul Set.smul_set_symmDiff smul_smul mul_inv_cancel one_smul
measure_symmDiff_neg_vadd 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	measure_vadd Set.vadd_set_symmDiff vadd_vadd add_neg_cancel zero_vadd
measure_union_inv_smul 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instUnion Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	measure_smul Set.smul_set_union smul_smul mul_inv_cancel one_smul
measure_union_neg_vadd 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instUnion HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	measure_vadd Set.vadd_set_union vadd_vadd add_neg_cancel zero_vadd
measure_vadd 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	Set.preimage_vadd_neg measure_preimage_vadd
measure_vadd_eq_zero_iff 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instZeroENNReal	—	measure_vadd
measure_vadd_null 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	DFunLike.coe Measure Set ENNReal Measure.instFunLike HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction instZeroENNReal	—	measure_vadd_eq_zero_iff
smulInvariantMeasure_iterateMulAct 📖	mathematical	Measurable	SMulInvariantMeasure IterateMulAct SemigroupAction.toSMul Monoid.toSemigroup CommMonoid.toMonoid IterateMulAct.instCommMonoid MulAction.toSemigroupAction IterateMulAct.instMulAction MeasurePreserving	—	Measurable.measurableSMul₂_iterateMulAct measurePreserving_smul MeasurableSMul.toMeasurableConstSMul MeasurableSMul₂.toMeasurableSMul MeasurePreserving.smulInvariantMeasure_iterateMulAct
smulInvariantMeasure_map 📖	mathematical	Measurable	SMulInvariantMeasure Measure.map	—	Measure.map_apply MeasurableSet.preimage MeasurableConstSMul.measurable_const_smul Set.preimage_preimage SMulInvariantMeasure.measure_preimage_smul
smulInvariantMeasure_map_smul 📖	mathematical	—	SMulInvariantMeasure Measure.map	—	smulInvariantMeasure_map SMulCommClass.smul_comm MeasurableConstSMul.measurable_const_smul
smulInvariantMeasure_tfae 📖	mathematical	—	List.TFAE SMulInvariantMeasure SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	SMulInvariantMeasure.measure_preimage_smul MeasurePreserving.map_eq measurePreserving_smul MeasurableConstSMul.measurable_const_smul MeasurePreserving.measure_preimage_emb measurableEmbedding_const_smul Set.preimage_smul_inv Set.preimage_smul List.tfae_of_cycle
smul_ae 📖	mathematical	—	Filter Filter.instSMulFilter SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Filter.ext Measure.instOuterMeasureClass Set.preimage_smul
smul_mem_ae 📖	mathematical	—	Set Filter Filter.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	Measure.instOuterMeasureClass
smul_set_ae_eq 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	Measure.instOuterMeasureClass
smul_set_ae_le 📖	mathematical	—	Filter.EventuallyLE Prop.le ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	Measure.instOuterMeasureClass
tendsto_smul_ae 📖	mathematical	—	Filter.Tendsto ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass eq_bot_mono measure_preimage_smul_le
tendsto_vadd_ae 📖	mathematical	—	Filter.Tendsto HVAdd.hVAdd instHVAdd ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass eq_bot_mono measure_preimage_vadd_le
vaddInvariantMeasure_iterateAddAct 📖	mathematical	Measurable	VAddInvariantMeasure IterateAddAct AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid IterateAddAct.instAddCommMonoid AddAction.toAddSemigroupAction IterateAddAct.instAddAction MeasurePreserving	—	Measurable.measurableSMul₂_iterateAddAct measurePreserving_vadd MeasurableVAdd.toMeasurableConstVAdd MeasurableVAdd₂.toMeasurableVAdd MeasurePreserving.vaddInvariantMeasure_iterateAddAct
vaddInvariantMeasure_map 📖	mathematical	HVAdd.hVAdd instHVAdd Measurable	VAddInvariantMeasure Measure.map	—	Measure.map_apply MeasurableSet.preimage MeasurableConstVAdd.measurable_const_vadd Set.preimage_preimage VAddInvariantMeasure.measure_preimage_vadd
vaddInvariantMeasure_map_vadd 📖	mathematical	—	VAddInvariantMeasure Measure.map HVAdd.hVAdd instHVAdd	—	vaddInvariantMeasure_map VAddCommClass.vadd_comm MeasurableConstVAdd.measurable_const_vadd
vaddInvariantMeasure_tfae 📖	mathematical	—	List.TFAE VAddInvariantMeasure AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	VAddInvariantMeasure.measure_preimage_vadd MeasurePreserving.map_eq measurePreserving_vadd MeasurableConstVAdd.measurable_const_vadd MeasurePreserving.measure_preimage_emb measurableEmbedding_const_vadd Set.preimage_vadd_neg Set.preimage_vadd List.tfae_of_cycle
vadd_ae 📖	mathematical	—	HVAdd.hVAdd Filter instHVAdd Filter.instVAddFilter AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Filter.ext Measure.instOuterMeasureClass Filter.mem_vadd_filter Set.preimage_vadd vadd_mem_ae
vadd_mem_ae 📖	mathematical	—	Set Filter Filter.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	Measure.instOuterMeasureClass mem_ae_iff Set.vadd_set_compl measure_vadd_eq_zero_iff
vadd_set_ae_eq 📖	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	—	Measure.instOuterMeasureClass Filter.eventuallyLE_antisymm_iff vadd_set_ae_le
vadd_set_ae_le 📖	mathematical	—	Filter.EventuallyLE Prop.le ae Measure Measure.instFunLike Measure.instOuterMeasureClass HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	Measure.instOuterMeasureClass ae_le_set Set.vadd_set_sdiff measure_vadd_eq_zero_iff

MeasureTheory.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smulInvariantMeasure_iterateMulAct 📖	mathematical	MeasureTheory.MeasurePreserving	MeasureTheory.SMulInvariantMeasure IterateMulAct SemigroupAction.toSMul Monoid.toSemigroup CommMonoid.toMonoid IterateMulAct.instCommMonoid MulAction.toSemigroupAction IterateMulAct.instMulAction	—	measure_preimage iterate MeasurableSet.nullMeasurableSet
vaddInvariantMeasure_iterateAddAct 📖	mathematical	MeasureTheory.MeasurePreserving	MeasureTheory.VAddInvariantMeasure IterateAddAct AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid IterateAddAct.instAddCommMonoid AddAction.toAddSemigroupAction IterateAddAct.instAddAction	—	measure_preimage iterate MeasurableSet.nullMeasurableSet

MeasureTheory.NullMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	mathematical	MeasureTheory.NullMeasurableSet	MeasureTheory.NullMeasurableSet Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	preimage MeasureTheory.MeasurePreserving.quasiMeasurePreserving MeasureTheory.measurePreserving_smul
vadd 📖	mathematical	MeasureTheory.NullMeasurableSet	MeasureTheory.NullMeasurableSet HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	Set.preimage_vadd_neg preimage MeasureTheory.MeasurePreserving.quasiMeasurePreserving MeasureTheory.measurePreserving_vadd

MeasureTheory.SMulInvariantMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	—	MeasureTheory.SMulInvariantMeasure MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	measure_preimage_smul
smul 📖	mathematical	—	MeasureTheory.SMulInvariantMeasure ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right measure_preimage_smul
smul_nnreal 📖	mathematical	—	MeasureTheory.SMulInvariantMeasure NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right	—	smul
zero 📖	mathematical	—	MeasureTheory.SMulInvariantMeasure MeasureTheory.Measure MeasureTheory.Measure.instZero	—	—

MeasureTheory.VAddInvariantMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	—	MeasureTheory.VAddInvariantMeasure MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	measure_preimage_vadd
vadd 📖	mathematical	—	MeasureTheory.VAddInvariantMeasure ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right measure_preimage_vadd
vadd_nnreal 📖	mathematical	—	MeasureTheory.VAddInvariantMeasure NNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right	—	vadd
zero 📖	mathematical	—	MeasureTheory.VAddInvariantMeasure MeasureTheory.Measure MeasureTheory.Measure.instZero	—	—

---

← Back to Index