MeasurePreserving

📁 Source: Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

Statistics

Metric	Count
Definitions `MeasurePreserving`	1
Theorems `measurePreserving`, `measurePreserving_symm`, `add_measure`, `aeconst_comp`, `aeconst_preimage`, `aemeasurable`, `aemeasurable_comp_iff`, `comp`, `comp_left_iff`, `comp_right_iff`, `exists_mem_iterate_mem`, `exists_mem_iterate_mem_of_measure_univ_lt_mul_measure`, `id`, `iterate`, `map_eq`, `map_of_comp`, `measurable`, `measureReal_preimage`, `measure_preimage`, `measure_preimage_emb`, `measure_preimage_equiv`, `measure_preimage_le`, `measure_symmDiff_preimage_iterate_le`, `of_isEmpty`, `of_semiconj`, `preimage_null`, `quasiMeasurePreserving`, `restrict_image_emb`, `restrict_preimage`, `restrict_preimage_emb`, `sfinite`, `sigmaFinite`, `smul_measure`, `trans`, `measurePreserving_subtype_coe`	35
Total	36

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurePreserving` 📖	mathematical	`Measurable`	`MeasureTheory.MeasurePreserving` `MeasureTheory.Measure.map`	—	—

MeasureTheory

Definitions

Name	Category	Theorems
`MeasurePreserving` 📖	CompData	116 math math: `Measure.measurePreserving_sub_left`, `smulInvariantMeasure_iterateMulAct`, `measurePreserving_prod_mul_swap`, `Measure.measurePreserving_neg`, `measurePreserving_prod_neg_add`, `measurePreserving_funUnique`, `unitInterval.measurePreserving_coe`, `volume_measurePreserving_piCongrLeft`, `measurePreserving_div_right`, `measurePreserving_prod_mul_swap_right`, `measurePreserving_prod_div_swap`, `measurePreserving_prod_inv_mul_swap`, `OrthonormalBasis.measurePreserving_repr`, `measurePreserving_mul_left`, `volume_preserving_piFinsetUnion`, `measurePreserving_finTwoArrow_vec`, `measurePreserving_mul_prod_inv_right`, `LinearIsometryEquiv.measurePreserving`, `hausdorffMeasure_measurePreserving_piFinTwo`, `volume_preserving_prodAssoc`, `unitInterval.measurePreserving_symm`, `measurePreserving_sub_right`, `measurePreserving_vadd`, `IsAddFundamentalDomain.measurePreserving_add_quotient_mk`, `PiLp.volume_preserving_toLp`, `Measure.measurePreserving_zsmul`, `Measurable.measurePreserving`, `Ergodic.iff_mem_extremePoints_measure_univ_eq`, `measurePreserving_prod_add_right`, `volume_preserving_piFinSuccAbove`, `measurePreserving_eval`, `measurePreserving_piCongrLeft`, `measurePreserving_add_prod_neg_right`, `measurePreserving_arrowProdEquivProdArrow`, `Ergodic.toMeasurePreserving`, `volume_preserving_pi_empty`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed`, `measurePreserving_prod_sub_swap`, `NumberField.mixedEmbedding.volume_preserving_negAt`, `measurePreserving_piFinTwo`, `Measure.measurePreserving_div_left`, `measurePreserving_prod_div`, `PiLp.volume_preserving_ofLp`, `measurePreserving_prodAssoc`, `NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm`, `ProbabilityTheory.HasLaw.measurePreserving`, `measurePreserving_piFinSuccAbove`, `measurePreserving_eval_infinitePi`, `IsometryEquiv.measurePreserving_hausdorffMeasure`, `Complex.volume_preserving_equiv_real_prod`, `Measure.measurePreserving_homeomorphUnitSphereProd`, `AddCircle.measurePreserving_equivIoc`, `measurePreserving_piUnique`, `hausdorffMeasure_measurePreserving_funUnique`, `OrthonormalBasis.measurePreserving_repr_symm`, `UnitAddCircle.measurePreserving_mk`, `Measure.measurePreserving_add_right_neg`, `volume_preserving_piFinTwo`, `measurePreserving_subtype_coe`, `measurePreserving_prod_sub`, `vaddInvariantMeasure_iterateAddAct`, `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`, `measurePreserving_smul`, `measurePreserving_prod_add`, `measurePreserving_mul_prod`, `Complex.volume_preserving_equiv_pi`, `NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace`, `measurePreserving_prod_add_swap_right`, `Ergodic.iff_mem_extremePoints`, `measurePreserving_add_prod`, `measurePreserving_piFinsetUnion`, `volume_measurePreserving_arrowProdEquivProdArrow`, `AddCircle.measurePreserving_mk`, `Ergodic.mem_extremePoints_measure_univ_eq`, `volume_preserving_piUnique`, `Measure.measurePreserving_inv`, `measurePreserving_add_left`, `measurePreserving_add_right`, `measurePreserving_mul_right`, `measurePreserving_quotientAddGroup_mk_of_AddQuotientMeasureEqMeasurePreimage`, `measurePreserving_prod_add_swap`, `measurePreserving_prod_mul`, `Lp.compMeasurePreserving_continuous`, `measurePreserving_prod_inv_mul`, `measurePreserving_sumPiEquivProdPi_symm`, `MeasurePreserving.id`, `measurePreserving_snd`, `measurePreserving_mul_prod_inv`, `AddMonoidHom.measurePreserving`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm`, `measurePreserving_piEquivPiSubtypeProd`, `Measure.measurePreserving_swap`, `volume_preserving_finTwoArrow`, `Measure.measurePreserving_mul_right_inv`, `measurePreserving_quotientGroup_mk_of_QuotientMeasureEqMeasurePreimage`, `measurePreserving_pi_empty`, `MeasurePreserving.of_isEmpty`, `MonoidHom.measurePreserving`, `measurePreserving_finTwoArrow`, `Measure.measurePreserving_zpow`, `OrthonormalBasis.measurePreserving_measurableEquiv`, `volume_measurePreserving_sumPiEquivProdPi`, `volume_preserving_piEquivPiSubtypeProd`, `Ergodic.mem_extremePoints`, `Real.volume_preserving_transvectionStruct`, `volume_measurePreserving_sumPiEquivProdPi_symm`, `measurePreserving_div_prod`, `volume_preserving_funUnique`, `IsFundamentalDomain.measurePreserving_quotient_mk`, `measurePreserving_prod_neg_add_swap`, `measurePreserving_add_prod_neg`, `measurePreserving_sumPiEquivProdPi`, `MeasurableEquiv.measurePreserving_symm`, `measurePreserving_sub_prod`, `measurePreserving_prod_mul_right`, `measurePreserving_fst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurePreserving_subtype_coe` 📖	mathematical	`MeasurableSet`	`MeasurePreserving` `Set` `Set.instMembership` `Subtype.instMeasurableSpace` `Measure.comap` `Measure.restrict`	—	`measurable_subtype_coe` `map_comap_subtype_coe`

MeasureTheory.MeasurableEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurePreserving_symm` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `MeasureTheory.Measure.map`	—	`MeasureTheory.MeasurePreserving.symm` `Measurable.measurePreserving` `MeasurableEquiv.measurable`

MeasureTheory.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_measure` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`MeasureTheory.Measure` `MeasureTheory.Measure.instAdd`	—	`measurable` `MeasureTheory.Measure.map_add` `map_eq`
`aeconst_comp` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasureTheory.NullMeasurable`	`Filter.EventuallyConst` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `measure_preimage` `MeasureTheory.NullMeasurableSet.compl` `Set.Subsingleton.measurableSet`
`aeconst_preimage` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasureTheory.NullMeasurableSet`	`Filter.EventuallyConst` `Set.preimage` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`aeconst_comp` `Prop.instMeasurableSingletonClass` `MeasurableSet.mem`
`aemeasurable` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`AEMeasurable`	—	`Measurable.aemeasurable` `measurable`
`aemeasurable_comp_iff` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasurableEmbedding`	`AEMeasurable`	—	`map_eq` `MeasurableEmbedding.aemeasurable_map_iff`
`comp` 📖	—	`MeasureTheory.MeasurePreserving`	—	—	`Measurable.comp` `measurable` `MeasureTheory.Measure.map_map` `map_eq`
`comp_left_iff` 📖	—	`MeasureTheory.MeasurePreserving` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike`	—	—	`MeasurableEquiv.symm_comp_self` `CompTriple.comp_eq` `CompTriple.instId_comp` `CompTriple.instIsIdId` `comp` `symm`
`comp_right_iff` 📖	—	`MeasureTheory.MeasurePreserving` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike`	—	—	`MeasurableEquiv.self_comp_symm` `CompTriple.comp_eq` `CompTriple.instComp_id` `CompTriple.instIsIdId` `comp` `symm`
`exists_mem_iterate_mem` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasureTheory.NullMeasurableSet`	`Set` `Set.instMembership` `Nat.iterate`	—	`ENNReal.exists_nat_mul_gt` `MeasureTheory.measure_ne_top` `exists_mem_iterate_mem_of_measure_univ_lt_mul_measure` `LT.lt.ne'`
`exists_mem_iterate_mem_of_measure_univ_lt_mul_measure` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasureTheory.NullMeasurableSet` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Set.instMembership` `Set.Ioo` `Nat.instPreorder` `Nat.iterate`	—	`MeasureTheory.NullMeasurableSet.preimage` `quasiMeasurePreserving` `iterate` `measure_preimage` `Finset.sum_congr` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul` `MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_sum_measure` `tsub_pos_of_lt` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `lt_of_le_of_lt` `Function.iterate_add_apply` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `LT.lt.le` `Ne.lt_or_gt`
`id` 📖	mathematical	—	`MeasureTheory.MeasurePreserving`	—	`measurable_id` `MeasureTheory.Measure.map_id`
`iterate` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`Nat.iterate`	—	`id` `comp`
`map_eq` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`MeasureTheory.Measure.map`	—	—
`map_of_comp` 📖	mathematical	`MeasureTheory.MeasurePreserving` `Measurable`	`MeasureTheory.Measure.map`	—	`MeasureTheory.Measure.map_map` `map_eq`
`measurable` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`Measurable`	—	—
`measureReal_preimage` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasureTheory.NullMeasurableSet`	`MeasureTheory.Measure.real` `Set.preimage`	—	`measure_preimage`
`measure_preimage` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasureTheory.NullMeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.preimage`	—	`map_eq` `MeasureTheory.Measure.map_apply₀` `Measurable.aemeasurable` `measurable`
`measure_preimage_emb` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasurableEmbedding`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.preimage`	—	`map_eq` `MeasurableEmbedding.map_apply`
`measure_preimage_equiv` 📖	mathematical	`MeasureTheory.MeasurePreserving` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike`	`MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.preimage`	—	`measure_preimage_emb` `MeasurableEquiv.measurableEmbedding`
`measure_preimage_le` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage`	—	`map_eq` `MeasureTheory.Measure.le_map_apply` `aemeasurable`
`measure_symmDiff_preimage_iterate_le` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasureTheory.NullMeasurableSet`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instSDiff` `Set.preimage` `Nat.iterate` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`symmDiff_self` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `zero_nsmul` `add_smul` `one_smul` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `MeasureTheory.measure_symmDiff_le` `MeasureTheory.NullMeasurableSet.symmDiff` `MeasureTheory.NullMeasurableSet.preimage` `quasiMeasurePreserving` `Function.iterate_succ'` `Set.preimage_comp` `Set.preimage_symmDiff` `measure_preimage` `iterate`
`of_isEmpty` 📖	mathematical	—	`MeasureTheory.MeasurePreserving`	—	`measurable_of_subsingleton_codomain` `IsEmpty.instSubsingleton` `MeasureTheory.Measure.instSubsingleton`
`of_semiconj` 📖	—	`MeasureTheory.MeasurePreserving` `Function.Semiconj` `Measurable`	—	—	`map_of_comp` `comp` `Function.Semiconj.comp_eq` `measurable` `map_eq`
`preimage_null` 📖	mathematical	`MeasureTheory.MeasurePreserving` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal`	`Set.preimage`	—	`MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null` `quasiMeasurePreserving`
`quasiMeasurePreserving` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`MeasureTheory.Measure.QuasiMeasurePreserving`	—	`measurable` `Eq.absolutelyContinuous` `map_eq`
`restrict_image_emb` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasurableEmbedding`	`MeasureTheory.Measure.restrict` `Set.image`	—	`Set.preimage_image_eq` `MeasurableEmbedding.injective` `restrict_preimage_emb`
`restrict_preimage` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasurableSet`	`MeasureTheory.Measure.restrict` `Set.preimage`	—	`measurable` `map_eq` `MeasureTheory.Measure.restrict_map`
`restrict_preimage_emb` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasurableEmbedding`	`MeasureTheory.Measure.restrict` `Set.preimage`	—	`measurable` `map_eq` `MeasurableEmbedding.restrict_map`
`sfinite` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`MeasureTheory.SFinite`	—	`map_eq` `MeasureTheory.Measure.instSFiniteMap`
`sigmaFinite` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`MeasureTheory.SigmaFinite`	—	`MeasureTheory.SigmaFinite.of_map` `aemeasurable` `map_eq`
`smul_measure` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`MeasureTheory.Measure` `MeasureTheory.Measure.instSMul`	—	`measurable` `MeasureTheory.Measure.map_smul` `map_eq`
`trans` 📖	mathematical	`MeasureTheory.MeasurePreserving` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike`	`MeasurableEquiv.trans`	—	`comp`

---

← Back to Index