Disintegration

📁 Source: Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_map_addHaar_eq_smul_addHaar, exists_map_addHaar_eq_smul_addHaar', ae_ae_add_linearMap_mem_iff, ae_comp_linearMap_mem_iff, ae_mem_of_ae_add_linearMap_mem	5
Total	5

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_map_addHaar_eq_smul_addHaar 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal MeasureTheory.Measure.map MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right Submodule.topologicalAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup Subtype.borelSpace locallyCompact_of_proper instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace exists_map_addHaar_eq_smul_addHaar' ENNReal.instCanonicallyOrderedAdd ENNReal.instNoZeroDivisors MeasureTheory.Measure.instNeZeroOfNonempty MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure
exists_map_addHaar_eq_smul_addHaar' 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Top.top instTopENNReal MeasureTheory.Measure.map MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule SetLike.instMembership Submodule.setLike ker Subtype.instMeasurableSpace Set MeasureTheory.Measure.instFunLike MeasureTheory.Measure.addHaar NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Submodule.normedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing instTopologicalSpaceSubtype Submodule.topologicalAddGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup Subtype.borelSpace locallyCompact_of_proper Subtype.pseudoMetricSpace instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace Set.univ	—	FiniteDimensional.of_locallyCompactSpace subsingleton_or_nontrivial Function.Surjective.subsingleton proper_of_compact TopologicalSpace.NoetherianSpace.compactSpace TopologicalSpace.Finite.to_noetherianSpace Finite.of_subsingleton ProperSpace.of_locallyCompact_module Module.Finite.of_surjective RingHomSurjective.ids FiniteDimensional.proper locallyCompact_of_proper IsScalarTower.right Submodule.topologicalAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup Subtype.borelSpace instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace Submodule.exists_isCompl RingHomInvPair.ids continuous_of_finiteDimensional IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Prod.instIsTopologicalAddGroup Prod.continuousSMul SMulMemClass.continuousSMul Submodule.smulMemClass TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Prod.t2Space instT2SpaceSubtype Module.instFiniteDimensionalOfIsReflexive Prod.instModuleIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_submodule Module.Projective.of_free Module.Free.of_divisionRing injective_domRestrict_iff IsCompl.inf_eq_bot IsCompl.symm surjective_domRestrict_iff IsCompl.sup_eq_top RingHomCompTriple.ids ext RingHomSurjective.invPair LinearEquiv.apply_symm_apply map_add SemilinearMapClass.toAddHomClass semilinearMapClass map_coe_ker zero_add comp.congr_simp Submodule.toLinearMap_prodEquivOfIsCompl_symm Submodule.linearProjOfIsCompl_apply_right Submodule.linearProjOfIsCompl_apply_left MeasureTheory.Measure.map_map Continuous.measurable Subtype.opensMeasurableSpace BorelSpace.opensMeasurable Prod.opensMeasurableSpace secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Measurable.comp Prod.borelSpace ContinuousLinearEquiv.isAddHaarMeasure_map MeasureTheory.Measure.prod.instIsAddHaarMeasure MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.sigmaFinite_addHaarMeasure ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant LT.lt.ne' MeasureTheory.Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure ENNReal.coe_ne_top MeasureTheory.Measure.isAddLeftInvariant_eq_smul Prod.locallyCompactSpace TopologicalSpace.instSecondCountableTopologyProd MeasureTheory.Measure.map_snd_prod ENNReal.instCanonicallyOrderedAdd ENNReal.instNoZeroDivisors ENNReal.mul_lt_top Ne.lt_top MeasureTheory.Measure.map_smul smul_smul mul_assoc mul_comm

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_ae_add_linearMap_mem_iff 📖	mathematical	MeasurableSet	Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule LinearMap.instFunLike ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	FiniteDimensional.of_locallyCompactSpace ProperSpace.of_locallyCompactSpace LinearMap.continuous_of_finiteDimensional Prod.instIsTopologicalAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup Prod.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Prod.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Module.instFiniteDimensionalOfIsReflexive Prod.instModuleIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.Projective.of_free Module.Free.of_divisionRing RingHomSurjective.ids LinearMap.range_eq_top LinearMap.range_coprod LinearMap.range_id sup_of_le_left Measure.instOuterMeasureClass ae_comp_linearMap_mem_iff Prod.borelSpace secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Measure.prod.instIsAddHaarMeasure instSFiniteOfSigmaFinite Measure.IsAddHaarMeasure.sigmaFinite SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd Prod.locallyCompactSpace Measure.ae_prod_mem_iff_ae_ae_mem Continuous.measurable Prod.opensMeasurableSpace BorelSpace.opensMeasurable
ae_comp_linearMap_mem_iff 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule LinearMap.instFunLike MeasurableSet	Filter.Eventually Set Set.instMembership ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	FiniteDimensional.of_locallyCompactSpace Continuous.aemeasurable BorelSpace.opensMeasurable LinearMap.continuous_of_finiteDimensional SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Measure.instOuterMeasureClass ae_map_iff IsScalarTower.right LinearMap.exists_map_addHaar_eq_smul_addHaar Measure.ae_ennreal_smul_measure_iff LT.lt.ne'
ae_mem_of_ae_add_linearMap_mem 📖	—	MeasurableSet Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule LinearMap.instFunLike ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	—	Measure.instOuterMeasureClass ae_ae_add_linearMap_mem_iff Filter.Eventually.of_forall

---

← Back to Index