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	Set.preimage	—	MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null

MeasureTheory.Measure

Definitions

Name	Category	Theorems
QuasiMeasurePreserving 📖	CompData	37 math math: MeasureTheory.quasiMeasurePreserving_add, MeasureTheory.quasiMeasurePreserving_add_swap, MeasureTheory.quasiMeasurePreserving_inv_mul, MeasureTheory.quasiMeasurePreserving_div_of_right_invariant, quasiMeasurePreserving_smul, MeasureTheory.quasiMeasurePreserving_add_right, QuasiErgodic.toQuasiMeasurePreserving, MeasurableEquiv.quasiMeasurePreserving_symm, MeasureTheory.quasiMeasurePreserving_neg_add_swap, MeasureTheory.Conservative.toQuasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_add_left, MeasureTheory.quasiMeasurePreserving_neg_add, 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, MeasureTheory.quasiMeasurePreserving_mul_swap, quasiMeasurePreserving_eval, MeasureTheory.quasiMeasurePreserving_inv_of_right_invariant, MeasureTheory.quasiMeasurePreserving_sub, MeasureTheory.MeasurePreserving.quasiMeasurePreserving, Measurable.quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_div_left_of_right_invariant, MeasureTheory.quasiMeasurePreserving_inv, QuasiMeasurePreserving.id, LinearMap.quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_neg_of_right_invariant, MeasureTheory.quasiMeasurePreserving_neg, MeasureTheory.quasiMeasurePreserving_mul, 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	—	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	—	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 📖	—	MeasureTheory.Measure.QuasiMeasurePreserving Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass tendsto_ae
ae_eq 📖	—	MeasureTheory.Measure.QuasiMeasurePreserving 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 📖	—	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	MeasurableSet	—	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	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	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.liminf Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Nat.iterate 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.limsup Set CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Nat.iterate 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 📖	—	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure.QuasiMeasurePreserving	—	—	mono_right mono_left
mono_left 📖	—	MeasureTheory.Measure.QuasiMeasurePreserving MeasureTheory.Measure.AbsolutelyContinuous	—	—	measurable MeasureTheory.Measure.AbsolutelyContinuous.trans MeasureTheory.Measure.AbsolutelyContinuous.map absolutelyContinuous
mono_right 📖	—	MeasureTheory.Measure.QuasiMeasurePreserving MeasureTheory.Measure.AbsolutelyContinuous	—	—	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	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	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	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	Set.preimage	—	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	Set Set.smulSet	—	MeasureTheory.Measure.instOuterMeasureClass ae_eq
smul_measure 📖	mathematical	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	Set Set.vaddSet	—	MeasureTheory.Measure.instOuterMeasureClass Set.preimage_vadd_neg ae_eq

MeasureTheory.NullMeasurable

Theorems

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

MeasureTheory.NullMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	MeasureTheory.NullMeasurableSet MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder MeasureTheory.Measure.instPartialOrder	—	—	mono_ac LE.le.absolutelyContinuous
mono_ac 📖	—	MeasureTheory.NullMeasurableSet MeasureTheory.Measure.AbsolutelyContinuous	—	—	preimage MeasureTheory.Measure.QuasiMeasurePreserving.mono_left MeasureTheory.Measure.QuasiMeasurePreserving.id
preimage 📖	mathematical	MeasureTheory.NullMeasurableSet MeasureTheory.Measure.QuasiMeasurePreserving	Set.preimage	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.QuasiMeasurePreserving.measurable MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq
smul_measure 📖	mathematical	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