QuasiMeasurePreserving

📁 Source: Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean

Statistics

Metric	Count
Definitions QuasiMeasurePreserving	1
Theorems quasiMeasurePreserving, quasiMeasurePreserving_symm, preimage, absolutelyContinuous, ae, ae_eq, ae_map_le, aemeasurable, comp, exists_preimage_eq_of_preimage_ae, id, image_zpow_ae_eq, iterate, liminf_preimage_iterate_ae_eq, limsup_preimage_iterate_ae_eq, measurable, mono, mono_left, mono_right, preimage_ae_eq, preimage_iterate_ae_eq, preimage_mono_ae, preimage_null, smul_ae_eq_of_ae_eq, smul_measure, tendsto_ae, vadd_ae_eq_of_ae_eq, pairwise_aedisjoint_of_aedisjoint_forall_ne_one, pairwise_aedisjoint_of_aedisjoint_forall_ne_zero, comp_quasiMeasurePreserving, mono, mono_ac, preimage, smul_measure, nullMeasurableSet_smul_measure_iff	35
Total	36

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiMeasurePreserving 📖	mathematical	Measurable	MeasureTheory.Measure.QuasiMeasurePreserving MeasureTheory.Measure.map	—	MeasureTheory.Measure.AbsolutelyContinuous.rfl

MeasurableEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiMeasurePreserving_symm 📖	mathematical	—	MeasureTheory.Measure.QuasiMeasurePreserving DFunLike.coe MeasurableEquiv EquivLike.toFunLike instEquivLike symm MeasureTheory.Measure.map	—	measurable MeasureTheory.Measure.map_map symm_comp_self MeasureTheory.Measure.map_id MeasureTheory.Measure.AbsolutelyContinuous.refl

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nullMeasurableSet_smul_measure_iff 📖	mathematical	—	NullMeasurableSet ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right NullMeasurableSet.mono_ac Measure.absolutelyContinuous_smul NullMeasurableSet.smul_measure

MeasureTheory.AEDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preimage 📖	mathematical	MeasureTheory.AEDisjoint MeasureTheory.Measure.QuasiMeasurePreserving	MeasureTheory.AEDisjoint Set.preimage	—	MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null

MeasureTheory.Measure

Definitions

Name	Category	Theorems
QuasiMeasurePreserving 📖	CompData	50 math math: MeasureTheory.quasiMeasurePreserving_add, MeasureTheory.quasiMeasurePreserving_add_swap, MeasureTheory.QuasiMeasurePreserving.snd, QuasiMeasurePreserving.restrict, MeasureTheory.quasiMeasurePreserving_inv_mul, MeasureTheory.quasiMeasurePreserving_div_of_right_invariant, QuasiMeasurePreserving.mono_right, quasiMeasurePreserving_smul, MeasureTheory.quasiMeasurePreserving_add_right, MeasureTheory.QuasiMeasurePreserving.prod_of_left, QuasiErgodic.toQuasiMeasurePreserving, MeasureTheory.QuasiMeasurePreserving.fst, MeasurableEquiv.quasiMeasurePreserving_symm, MeasureTheory.quasiMeasurePreserving_neg_add_swap, MeasureTheory.Conservative.toQuasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_add_left, QuasiMeasurePreserving.smul_measure, QuasiMeasurePreserving.iterate, MeasureTheory.quasiMeasurePreserving_neg_add, MeasureTheory.QuasiMeasurePreserving.prod_of_right, MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant, quasiMeasurePreserving_fst, MeasureTheory.quasiMeasurePreserving_sub_of_right_invariant, MeasureTheory.quasiMeasurePreserving_mul_left, MeasureTheory.quasiMeasurePreserving_div_left, quasiMeasurePreserving_snd, MeasureTheory.HasPDF.quasiMeasurePreserving_of_measurable, QuasiMeasurePreserving.comp, MeasureTheory.quasiMeasurePreserving_mul_swap, quasiMeasurePreserving_eval, MeasureTheory.quasiMeasurePreserving_inv_of_right_invariant, MeasureTheory.quasiMeasurePreserving_sub, MeasureTheory.MeasurePreserving.quasiMeasurePreserving, Measurable.quasiMeasurePreserving, QuasiMeasurePreserving.congr, MeasureTheory.quasiMeasurePreserving_div_left_of_right_invariant, MeasureTheory.quasiMeasurePreserving_inv, QuasiMeasurePreserving.id, MeasureTheory.QuasiMeasurePreserving.prodMap, LinearMap.quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_neg_of_right_invariant, QuasiMeasurePreserving.mono_left, MeasureTheory.quasiMeasurePreserving_neg, MeasureTheory.quasiMeasurePreserving_mul, QuasiMeasurePreserving.mono, MeasureTheory.quasiMeasurePreserving_sub_left, ContinuousLinearMap.quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_mul_right, MeasureTheory.quasiMeasurePreserving_div, MeasureTheory.quasiMeasurePreserving_inv_mul_swap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pairwise_aedisjoint_of_aedisjoint_forall_ne_one 📖	mathematical	MeasureTheory.AEDisjoint Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction QuasiMeasurePreserving	Pairwise Function.onFun Set MeasureTheory.AEDisjoint Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	inv_mul_eq_one Set.preimage_eq_iff_eq_image MulAction.bijective Set.image_smul Set.smul_set_inter smul_smul inv_mul_cancel one_smul QuasiMeasurePreserving.preimage_null
pairwise_aedisjoint_of_aedisjoint_forall_ne_zero 📖	mathematical	MeasureTheory.AEDisjoint HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction QuasiMeasurePreserving	Pairwise Function.onFun Set MeasureTheory.AEDisjoint HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction	—	neg_add_eq_zero Set.preimage_eq_iff_eq_image AddAction.bijective Set.image_vadd Set.vadd_set_inter vadd_vadd neg_add_cancel zero_vadd QuasiMeasurePreserving.preimage_null

MeasureTheory.Measure.QuasiMeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure.map	—	—
ae 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass tendsto_ae
ae_eq 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass ae
ae_map_le 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map	—	MeasureTheory.Measure.AbsolutelyContinuous.ae_le absolutelyContinuous
aemeasurable 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving	AEMeasurable	—	Measurable.aemeasurable measurable
comp 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving	MeasureTheory.Measure.QuasiMeasurePreserving	—	Measurable.comp measurable MeasureTheory.Measure.map_map MeasureTheory.Measure.AbsolutelyContinuous.trans MeasureTheory.Measure.AbsolutelyContinuous.map absolutelyContinuous
exists_preimage_eq_of_preimage_ae 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving MeasureTheory.NullMeasurableSet Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	Set MeasurableSet Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	—	MeasureTheory.Measure.instOuterMeasureClass MeasurableSet.measurableSet_limsup Measurable.iterate measurable Filter.EventuallyEq.trans preimage_ae_eq Filter.EventuallyEq.symm MeasureTheory.limsup_ae_eq_of_forall_ae_eq preimage_iterate_ae_eq Set.preimage_iterate_eq CompleteLatticeHom.apply_limsup_iterate
id 📖	mathematical	—	MeasureTheory.Measure.QuasiMeasurePreserving	—	measurable_id Eq.absolutelyContinuous MeasureTheory.Measure.map_id
image_zpow_ae_eq 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.image	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike DivInvMonoid.toZPow Group.toDivInvMonoid Equiv.Perm.permGroup	—	MeasureTheory.Measure.instOuterMeasureClass Equiv.image_eq_preimage_symm preimage_iterate_ae_eq inv_pow Equiv.Perm.iterate_eq_pow zpow_neg zpow_natCast Equiv.preimage_image preimage_ae_eq Filter.EventuallyEq.symm
iterate 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving	MeasureTheory.Measure.QuasiMeasurePreserving Nat.iterate	—	id comp
liminf_preimage_iterate_ae_eq 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Filter.liminf Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Nat.iterate Set.preimage Filter.atTop Nat.instPreorder	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.liminf_ae_eq_of_forall_ae_eq Set.preimage_iterate_eq preimage_iterate_ae_eq
limsup_preimage_iterate_ae_eq 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Filter.limsup Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Nat.iterate Set.preimage Filter.atTop Nat.instPreorder	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.limsup_ae_eq_of_forall_ae_eq Set.preimage_iterate_eq preimage_iterate_ae_eq
measurable 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving	Measurable	—	—
mono 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure.QuasiMeasurePreserving	MeasureTheory.Measure.QuasiMeasurePreserving	—	mono_right mono_left
mono_left 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Measure.QuasiMeasurePreserving	—	measurable MeasureTheory.Measure.AbsolutelyContinuous.trans MeasureTheory.Measure.AbsolutelyContinuous.map absolutelyContinuous
mono_right 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Measure.QuasiMeasurePreserving	—	measurable MeasureTheory.Measure.AbsolutelyContinuous.trans absolutelyContinuous
preimage_ae_eq 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	—	MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyLE.antisymm preimage_mono_ae Filter.EventuallyEq.le Filter.EventuallyEq.symm
preimage_iterate_ae_eq 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage Nat.iterate	—	MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.refl Function.iterate_succ Set.preimage_comp Filter.EventuallyEq.trans preimage_ae_eq
preimage_mono_ae 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set.preimage	—	MeasureTheory.Measure.instOuterMeasureClass Filter.eventually_map Filter.Eventually.filter_mono MeasureTheory.Measure.tendsto_ae_map aemeasurable ae_map_le
preimage_null 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike instZeroENNReal	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.preimage instZeroENNReal	—	MeasureTheory.Measure.preimage_null_of_map_null aemeasurable absolutelyContinuous
smul_ae_eq_of_ae_eq 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	MeasureTheory.Measure.instOuterMeasureClass ae_eq
smul_measure 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving	MeasureTheory.Measure.QuasiMeasurePreserving MeasureTheory.Measure MeasureTheory.Measure.instSMul	—	measurable MeasureTheory.Measure.map_smul MeasureTheory.Measure.AbsolutelyContinuous.smul absolutelyContinuous
tendsto_ae 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving	Filter.Tendsto MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Filter.Tendsto.mono_right MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.tendsto_ae_map aemeasurable ae_map_le
vadd_ae_eq_of_ae_eq 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddAction.toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	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 AddAction.toAddSemigroupAction	—	MeasureTheory.Measure.instOuterMeasureClass Set.preimage_vadd_neg ae_eq

MeasureTheory.NullMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_quasiMeasurePreserving 📖	mathematical	MeasureTheory.NullMeasurable MeasureTheory.Measure.QuasiMeasurePreserving	MeasureTheory.NullMeasurable	—	MeasureTheory.NullMeasurableSet.preimage

MeasureTheory.NullMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	mathematical	MeasureTheory.NullMeasurableSet MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder MeasureTheory.Measure.instPartialOrder	MeasureTheory.NullMeasurableSet	—	mono_ac LE.le.absolutelyContinuous
mono_ac 📖	mathematical	MeasureTheory.NullMeasurableSet MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.NullMeasurableSet	—	preimage MeasureTheory.Measure.QuasiMeasurePreserving.mono_left MeasureTheory.Measure.QuasiMeasurePreserving.id
preimage 📖	mathematical	MeasureTheory.NullMeasurableSet MeasureTheory.Measure.QuasiMeasurePreserving	MeasureTheory.NullMeasurableSet Set.preimage	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.QuasiMeasurePreserving.measurable MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq
smul_measure 📖	mathematical	MeasureTheory.NullMeasurableSet	MeasureTheory.NullMeasurableSet ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	mono_ac IsScalarTower.right MeasureTheory.Measure.AbsolutelyContinuous.smul_left MeasureTheory.Measure.AbsolutelyContinuous.rfl

---

← Back to Index