WithDensity

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

Statistics

Metric	Count
Definitions withDensity	1
Theorems withDensity_coe, withDensity_ofReal, withDensity, conv_smul_right, mconv_smul_right, prod_smul_right, instSFinite, withDensity, withDensity_ofReal, withDensity_of_ne_top, withDensity_of_ne_top', ae_withDensity_iff, ae_withDensity_iff', ae_withDensity_iff_ae_restrict, ae_withDensity_iff_ae_restrict', aemeasurable_withDensity_ennreal_iff, aemeasurable_withDensity_ennreal_iff', conv_withDensity_eq_lconvolution, conv_withDensity_eq_mlconvolution₀, count_withDensity, count_withDensity', dirac_withDensity, dirac_withDensity', exists_measurable_le_withDensity_eq, instSFiniteHSMulENNRealMeasure, instSFiniteOfCountable, isFiniteMeasure_withDensity, lintegral_withDensity_eq_lintegral_mul, lintegral_withDensity_eq_lintegral_mul_non_measurable, lintegral_withDensity_eq_lintegral_mul_non_measurable₀, lintegral_withDensity_eq_lintegral_mul₀, lintegral_withDensity_eq_lintegral_mul₀', lintegral_withDensity_le_lintegral_mul, mconv_withDensity_eq_mlconvolution, mconv_withDensity_eq_mlconvolution₀, noAtoms_withDensity, prod_withDensity, prod_withDensity_left, prod_withDensity_left₀, prod_withDensity_right, prod_withDensity_right₀, prod_withDensity₀, restrict_withDensity, restrict_withDensity', sFinite_of_absolutelyContinuous, setLIntegral_withDensity_eq_lintegral_mul₀, setLIntegral_withDensity_eq_lintegral_mul₀', setLIntegral_withDensity_eq_setLIntegral_mul, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀', trim_withDensity, withDensity_absolutelyContinuous, withDensity_absolutelyContinuous', withDensity_add_left, withDensity_add_measure, withDensity_add_right, withDensity_ae_eq, withDensity_apply, withDensity_apply', withDensity_apply_eq_zero, withDensity_apply_eq_zero', withDensity_apply_le, withDensity_apply₀, withDensity_congr_ae, withDensity_const, withDensity_eq_zero, withDensity_eq_zero_iff, withDensity_indicator, withDensity_indicator_one, withDensity_inv_same, withDensity_inv_same_le, withDensity_inv_same₀, withDensity_mono, withDensity_mul, withDensity_mul₀, withDensity_ofReal_mutuallySingular, withDensity_one, withDensity_smul, withDensity_smul', withDensity_smul_measure, withDensity_sum, withDensity_tsum, withDensity_zero, withDensity_zero_left	85
Total	86

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_withDensity_iff 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.withDensity	—	ae_withDensity_iff' Measurable.aemeasurable
ae_withDensity_iff' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.withDensity	—	Measure.instOuterMeasureClass ae_iff withDensity_apply_eq_zero' Set.ext
ae_withDensity_iff_ae_restrict 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.withDensity Measure.restrict setOf instZeroENNReal	—	ae_withDensity_iff_ae_restrict' Measurable.aemeasurable
ae_withDensity_iff_ae_restrict' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.withDensity Measure.restrict setOf instZeroENNReal	—	Measure.instOuterMeasureClass ae_withDensity_iff' ae_restrict_iff'₀ Filter.mp_mem Filter.univ_mem' NullMeasurableSet.congr NullMeasurableSet.compl MeasurableSet.nullMeasurableSet MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space
aemeasurable_withDensity_ennreal_iff 📖	mathematical	Measurable NNReal NNReal.measurableSpace	AEMeasurable ENNReal ENNReal.measurableSpace Measure.withDensity ENNReal.ofNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	aemeasurable_withDensity_ennreal_iff' Measurable.aemeasurable
aemeasurable_withDensity_ennreal_iff' 📖	mathematical	AEMeasurable NNReal NNReal.measurableSpace	ENNReal ENNReal.measurableSpace Measure.withDensity ENNReal.ofNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Measure.instOuterMeasureClass MeasurableSet.compl MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable NNReal.borelSpace NNReal.instSecondCountableTopology TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Measurable.smul measurableSMul₂_of_mul ENNReal.instMeasurableMul₂ Measurable.coe_nnreal_ennreal ae_of_ae_restrict_of_ae_restrict_compl ae_restrict_iff' Filter.mp_mem ae_withDensity_iff' AEMeasurable.coe_nnreal_ennreal Filter.EventuallyEq.eq_1 Filter.univ_mem' Function.notMem_support MulZeroClass.zero_mul Measurable.inv ENNReal.instMeasurableInv mul_assoc ENNReal.inv_mul_cancel ENNReal.coe_ne_top one_mul
conv_withDensity_eq_lconvolution 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Measure.conv SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Measure.withDensity lconvolution AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	conv_withDensity_eq_mlconvolution₀ Measurable.aemeasurable
conv_withDensity_eq_mlconvolution₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Measure.conv SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Measure.withDensity lconvolution AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Measure.ext_of_lintegral Measure.lintegral_conv_eq_lintegral_sum prod_withDensity₀ lintegral_withDensity_eq_lintegral_mul₀ AEMeasurable.mul ENNReal.instMeasurableMul₂ AEMeasurable.comp_quasiMeasurePreserving QuasiMeasurePreserving.fst Measure.QuasiMeasurePreserving.id QuasiMeasurePreserving.snd Measurable.comp_aemeasurable' AEMeasurable.add AEMeasurable.fst aemeasurable_id AEMeasurable.snd aemeasurable_lconvolution Measurable.aemeasurable lintegral_prod AEMeasurable.mul' lintegral_congr lintegral_add_left_eq_self MeasurableAdd₂.toMeasurableAdd lintegral_lintegral_swap quasiMeasurePreserving_neg_add AEMeasurable.neg add_neg_cancel_left lintegral_mul_const'' Measure.QuasiMeasurePreserving.comp quasiMeasurePreserving_add_right quasiMeasurePreserving_neg
count_withDensity 📖	mathematical	—	Measure.withDensity Measure.count Measure.sum ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Measure.dirac	—	IsScalarTower.right withDensity_sum dirac_withDensity
count_withDensity' 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Measure.withDensity Measure.count Measure.sum Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Measure.dirac	—	IsScalarTower.right withDensity_sum dirac_withDensity'
dirac_withDensity 📖	mathematical	—	Measure.withDensity Measure.dirac ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	Measure.ext IsScalarTower.right withDensity_apply setLIntegral_dirac Measure.dirac_apply mul_ite mul_one MulZeroClass.mul_zero
dirac_withDensity' 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Measure.withDensity Measure.dirac Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	Measure.ext IsScalarTower.right withDensity_apply setLIntegral_dirac' Measure.dirac_apply' mul_ite mul_one MulZeroClass.mul_zero
exists_measurable_le_withDensity_eq 📖	mathematical	—	Measurable ENNReal ENNReal.measurableSpace Pi.hasLe Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Measure.withDensity	—	exists_measurable_le_forall_setLIntegral_eq Measure.ext withDensity_apply
instSFiniteHSMulENNRealMeasure 📖	mathematical	—	SFinite ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right withDensity_const Measure.withDensity.instSFinite
instSFiniteOfCountable 📖	mathematical	—	SFinite	—	IsScalarTower.right Measure.exists_sum_smul_dirac instSFiniteSumOfCountable SetCoe.countable instSFiniteHSMulENNRealMeasure instSFiniteOfSigmaFinite Measure.dirac.instSigmaFinite
isFiniteMeasure_withDensity 📖	mathematical	—	IsFiniteMeasure Measure.withDensity	—	withDensity_apply MeasurableSet.univ Measure.restrict_univ lt_top_iff_ne_top
lintegral_withDensity_eq_lintegral_mul 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	lintegral Measure.withDensity Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Measurable.ennreal_induction lintegral_indicator lintegral_const Measure.restrict_apply Set.univ_inter withDensity_apply mul_comm lintegral_const_mul lintegral_add_left mul_add Distrib.leftDistribClass ENNReal.instMeasurableMul₂ le_imp_le_of_le_of_le mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid le_refl lintegral_iSup ENNReal.mul_iSup Measurable.mul
lintegral_withDensity_eq_lintegral_mul_non_measurable 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Filter.Eventually Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder Top.top instTopENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral Measure.withDensity Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Measure.instOuterMeasureClass le_antisymm lintegral_withDensity_le_lintegral_mul iSup_lintegral_measurable_le_eq_lintegral iSup₂_le iSup_le mul_comm div_eq_mul_inv ENNReal.div_le_of_le_mul' le_iSup_of_le Measurable.mul ENNReal.instMeasurableMul₂ Measurable.inv ENNReal.instMeasurableInv lintegral_withDensity_eq_lintegral_mul lintegral_mono_ae Filter.mp_mem Filter.univ_mem' eq_or_ne MulZeroClass.zero_mul ENNReal.instCanonicallyOrderedAdd MulZeroClass.mul_zero le_of_eq mul_assoc ENNReal.mul_inv_cancel LT.lt.ne one_mul
lintegral_withDensity_eq_lintegral_mul_non_measurable₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Eventually Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder Top.top instTopENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral Measure.withDensity Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Measure.instOuterMeasureClass withDensity_congr_ae lintegral_withDensity_eq_lintegral_mul_non_measurable Filter.mp_mem Filter.univ_mem' lintegral_congr_ae
lintegral_withDensity_eq_lintegral_mul₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	lintegral Measure.withDensity Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	lintegral_withDensity_eq_lintegral_mul₀' AEMeasurable.mono' withDensity_absolutelyContinuous
lintegral_withDensity_eq_lintegral_mul₀' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Measure.withDensity	lintegral Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	withDensity_congr_ae lintegral_congr_ae lintegral_withDensity_eq_lintegral_mul ae_of_ae_restrict_of_ae_restrict_compl Measure.instOuterMeasureClass Filter.mp_mem ae_withDensity_iff_ae_restrict Filter.EventuallyEq.eq_1 Filter.univ_mem' MeasurableSet.compl MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space ae_restrict_mem MulZeroClass.zero_mul
lintegral_withDensity_le_lintegral_mul 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.withDensity Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	iSup_lintegral_measurable_le_eq_lintegral iSup₂_le iSup_le lintegral_withDensity_eq_lintegral_mul le_iSup₂_of_le Measurable.mul ENNReal.instMeasurableMul₂ le_iSup_of_le le_imp_le_of_le_of_le mul_le_mul_right IsOrderedMonoid.toMulLeftMono Pi.isOrderedMonoid ENNReal.instIsOrderedMonoid le_refl le_rfl
mconv_withDensity_eq_mlconvolution 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Measure.mconv DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.withDensity mlconvolution MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	mconv_withDensity_eq_mlconvolution₀ Measurable.aemeasurable
mconv_withDensity_eq_mlconvolution₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Measure.mconv DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.withDensity mlconvolution MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Measure.ext_of_lintegral Measure.lintegral_mconv_eq_lintegral_prod prod_withDensity₀ lintegral_withDensity_eq_lintegral_mul₀ AEMeasurable.mul ENNReal.instMeasurableMul₂ AEMeasurable.comp_quasiMeasurePreserving QuasiMeasurePreserving.fst Measure.QuasiMeasurePreserving.id QuasiMeasurePreserving.snd Measurable.comp_aemeasurable' AEMeasurable.fst aemeasurable_id AEMeasurable.snd aemeasurable_mlconvolution Measurable.aemeasurable lintegral_prod AEMeasurable.mul' lintegral_congr lintegral_mul_left_eq_self MeasurableMul₂.toMeasurableMul lintegral_lintegral_swap quasiMeasurePreserving_inv_mul AEMeasurable.inv mul_inv_cancel_left lintegral_mul_const'' Measure.QuasiMeasurePreserving.comp quasiMeasurePreserving_mul_right quasiMeasurePreserving_inv
noAtoms_withDensity 📖	mathematical	—	NoAtoms Measure.withDensity	—	withDensity_absolutelyContinuous NoAtoms.measure_singleton
prod_withDensity 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Measure.prod Measure.withDensity Prod.instMeasurableSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	prod_withDensity₀ Measurable.aemeasurable
prod_withDensity_left 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Measure.prod Measure.withDensity Prod.instMeasurableSpace	—	prod_withDensity_left₀ Measurable.aemeasurable
prod_withDensity_left₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Measure.prod Measure.withDensity Prod.instMeasurableSpace	—	Measure.ext_of_lintegral lintegral_prod Measurable.aemeasurable lintegral_withDensity_eq_lintegral_mul₀ AEMeasurable.lintegral_prod_right' AEMeasurable.comp_aemeasurable' AEMeasurable.mono' IsScalarTower.right Measure.map_fst_prod MulZeroClass.mul_zero AEMeasurable.fst aemeasurable_id AEMeasurable.mul' ENNReal.instMeasurableMul₂ lintegral_congr Pi.mul_apply lintegral_const_mul'' Measurable.comp_aemeasurable' AEMeasurable.prodMk aemeasurable_const
prod_withDensity_right 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Measure.prod Measure.withDensity Prod.instMeasurableSpace	—	prod_withDensity_right₀ Measurable.aemeasurable
prod_withDensity_right₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Measure.prod Measure.withDensity Prod.instMeasurableSpace	—	Measure.ext_of_lintegral lintegral_prod Measure.withDensity.instSFinite Measurable.aemeasurable lintegral_withDensity_eq_lintegral_mul₀ AEMeasurable.comp_aemeasurable' AEMeasurable.mono' IsScalarTower.right Measure.map_snd_prod MulZeroClass.mul_zero AEMeasurable.snd aemeasurable_id AEMeasurable.mul' ENNReal.instMeasurableMul₂ lintegral_congr Measurable.comp_aemeasurable' AEMeasurable.prodMk aemeasurable_const
prod_withDensity₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Measure.prod Measure.withDensity Prod.instMeasurableSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	prod_withDensity_left₀ Measure.withDensity.instSFinite prod_withDensity_right₀ withDensity_mul₀ AEMeasurable.comp_aemeasurable' AEMeasurable.mono' IsScalarTower.right Measure.map_snd_prod MulZeroClass.mul_zero AEMeasurable.snd aemeasurable_id Measure.map_fst_prod AEMeasurable.fst mul_comm
restrict_withDensity 📖	mathematical	MeasurableSet	Measure.restrict Measure.withDensity	—	Measure.ext Measure.restrict_apply withDensity_apply MeasurableSet.inter Measure.restrict_restrict
restrict_withDensity' 📖	mathematical	—	Measure.restrict Measure.withDensity	—	Measure.ext Measure.restrict_apply withDensity_apply withDensity_apply' Measure.restrict_restrict
sFinite_of_absolutelyContinuous 📖	mathematical	Measure.AbsolutelyContinuous	SFinite	—	Measure.restrict_add_restrict_compl measurableSet_sigmaFiniteSetWRT IsScalarTower.right restrict_compl_sigmaFiniteSetWRT instSFiniteHAddMeasure instSFiniteOfSigmaFinite instSigmaFiniteRestrictSigmaFiniteSetWRT instSFiniteHSMulENNRealMeasure instSFiniteRestrict
setLIntegral_withDensity_eq_lintegral_mul₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace MeasurableSet	lintegral Measure.restrict Measure.withDensity Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	setLIntegral_withDensity_eq_lintegral_mul₀' AEMeasurable.mono' withDensity_absolutelyContinuous
setLIntegral_withDensity_eq_lintegral_mul₀' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Measure.withDensity MeasurableSet	lintegral Measure.restrict Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	restrict_withDensity lintegral_withDensity_eq_lintegral_mul₀' AEMeasurable.restrict
setLIntegral_withDensity_eq_setLIntegral_mul 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace MeasurableSet	lintegral Measure.restrict Measure.withDensity Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	restrict_withDensity lintegral_withDensity_eq_lintegral_mul
setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace MeasurableSet Filter.Eventually Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder Top.top instTopENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict	lintegral Measure.withDensity Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Measure.instOuterMeasureClass restrict_withDensity lintegral_withDensity_eq_lintegral_mul_non_measurable
setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Measure.restrict MeasurableSet Filter.Eventually Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder Top.top instTopENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral Measure.withDensity Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Measure.instOuterMeasureClass restrict_withDensity lintegral_withDensity_eq_lintegral_mul_non_measurable₀
setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Measure.restrict Filter.Eventually Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder Top.top instTopENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral Measure.withDensity Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Measure.instOuterMeasureClass restrict_withDensity' lintegral_withDensity_eq_lintegral_mul_non_measurable₀
trim_withDensity 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable ENNReal ENNReal.measurableSpace	Measure.trim Measure.withDensity	—	Measure.ext withDensity_apply restrict_trim lintegral_trim trim_measurableSet_eq
withDensity_absolutelyContinuous 📖	mathematical	—	Measure.AbsolutelyContinuous Measure.withDensity	—	withDensity_apply setLIntegral_measure_zero
withDensity_absolutelyContinuous' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Eventually instZeroENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Measure.AbsolutelyContinuous Measure.withDensity	—	Measure.instOuterMeasureClass measure_mono_null nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd le_trans measure_union_le Eq.le zero_add ae_iff Filter.EventuallyEq.eq_1 Set.indicator_zero' ae_eq_restrict_iff_indicator_ae_eq lintegral_eq_zero_iff' AEMeasurable.restrict withDensity_apply
withDensity_add_left 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Measure.withDensity Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Measure Measure.instAdd	—	Measure.ext withDensity_apply Measure.add_apply lintegral_add_left
withDensity_add_measure 📖	mathematical	—	Measure.withDensity Measure Measure.instAdd	—	Measure.ext withDensity_apply Measure.restrict_add lintegral_add_measure
withDensity_add_right 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Measure.withDensity Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Measure Measure.instAdd	—	add_comm withDensity_add_left
withDensity_ae_eq 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Eventually instZeroENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Filter.EventuallyEq Measure.withDensity	—	Measure.instOuterMeasureClass Measure.AbsolutelyContinuous.ae_eq withDensity_absolutelyContinuous' withDensity_absolutelyContinuous
withDensity_apply 📖	mathematical	MeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.withDensity lintegral Measure.restrict	—	Measure.ofMeasurable_apply lintegral_iUnion instCountableNat
withDensity_apply' 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.withDensity lintegral Measure.restrict	—	le_antisymm measure_mono Measure.instOuterMeasureClass subset_toMeasurable withDensity_apply measurableSet_toMeasurable Measure.restrict_toMeasurable_of_sFinite withDensity_apply_le
withDensity_apply_eq_zero 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	DFunLike.coe Measure Set Measure.instFunLike Measure.withDensity instZeroENNReal Set.instInter setOf	—	withDensity_apply_eq_zero' Measurable.aemeasurable
withDensity_apply_eq_zero' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	DFunLike.coe Measure Set Measure.instFunLike Measure.withDensity instZeroENNReal Set.instInter setOf	—	measure_mono_null Measure.instOuterMeasureClass Set.inter_subset_inter_right subset_toMeasurable measure_toMeasurable Set.ext ae_iff ae_restrict_iff'₀ Filter.EventuallyEq.eq_1 lintegral_eq_zero_iff' AEMeasurable.restrict withDensity_apply measurableSet_toMeasurable eq_or_ne measure_union_null withDensity_absolutelyContinuous Filter.mp_mem Filter.univ_mem' measure_congr withDensity_congr_ae MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space lintegral_eq_zero_iff ae_restrict_mem
withDensity_apply_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.restrict DFunLike.coe Measure Set Measure.instFunLike Measure.withDensity	—	lintegral_mono_set subset_toMeasurable withDensity_apply measurableSet_toMeasurable measure_toMeasurable
withDensity_apply₀ 📖	mathematical	NullMeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.withDensity lintegral Measure.restrict	—	setLIntegral_congr NullMeasurableSet.toMeasurable_ae_eq measure_congr Measure.instOuterMeasureClass withDensity_absolutelyContinuous withDensity_apply measurableSet_toMeasurable
withDensity_congr_ae 📖	mathematical	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Measure.withDensity	—	Measure.instOuterMeasureClass Measure.ext withDensity_apply lintegral_congr_ae ae_restrict_of_ae
withDensity_const 📖	mathematical	—	Measure.withDensity ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	Measure.ext IsScalarTower.right withDensity_apply lintegral_const Measure.restrict_apply Set.univ_inter
withDensity_eq_zero 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Measure.withDensity Measure Measure.instZero	Filter.EventuallyEq ae Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero instZeroENNReal	—	Measure.instOuterMeasureClass withDensity_eq_zero_iff
withDensity_eq_zero_iff 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Measure.withDensity Measure Measure.instZero Filter.EventuallyEq ae Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero instZeroENNReal	—	Measure.instOuterMeasureClass Measure.measure_univ_eq_zero withDensity_apply MeasurableSet.univ Measure.restrict_univ lintegral_eq_zero_iff'
withDensity_indicator 📖	mathematical	MeasurableSet	Measure.withDensity Set.indicator ENNReal instZeroENNReal Measure.restrict	—	Measure.ext withDensity_apply lintegral_indicator Measure.restrict_comm
withDensity_indicator_one 📖	mathematical	MeasurableSet	Measure.withDensity Set.indicator ENNReal instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Measure.restrict	—	withDensity_indicator withDensity_one
withDensity_inv_same 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Filter.Eventually instZeroENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass Top.top instTopENNReal	Measure.withDensity ENNReal.instInv	—	Measure.instOuterMeasureClass withDensity_inv_same₀ Measurable.aemeasurable
withDensity_inv_same_le 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Measure Preorder.toLE PartialOrder.toPreorder Measure.instPartialOrder Measure.withDensity Pi.instInv ENNReal.instInv	—	withDensity_mul₀ AEMeasurable.inv ENNReal.instMeasurableInv Measure.instOuterMeasureClass Filter.univ_mem' LE.le.trans withDensity_mono withDensity_one le_refl
withDensity_inv_same₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Eventually instZeroENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass Top.top instTopENNReal	Measure.withDensity ENNReal.instInv	—	Measure.instOuterMeasureClass withDensity_mul₀ AEMeasurable.inv ENNReal.instMeasurableInv Filter.mp_mem Filter.univ_mem' ENNReal.mul_inv_cancel Pi.one_apply withDensity_congr_ae withDensity_one
withDensity_mono 📖	mathematical	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	Measure.instPartialOrder Measure.withDensity	—	Measure.instOuterMeasureClass Measure.le_iff withDensity_apply setLIntegral_mono_ae' Filter.mp_mem Filter.univ_mem'
withDensity_mul 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Measure.withDensity Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	withDensity_mul₀ Measurable.aemeasurable
withDensity_mul₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Measure.withDensity Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Measure.ext withDensity_apply restrict_withDensity lintegral_withDensity_eq_lintegral_mul₀ AEMeasurable.restrict
withDensity_ofReal_mutuallySingular 📖	mathematical	Measurable Real Real.measurableSpace	Measure.MutuallySingular Measure.withDensity ENNReal.ofReal Real.instNeg	—	measurableSet_lt BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal OrderTopology.to_orderClosedTopology instOrderTopologyReal measurable_const withDensity_apply Measure.instOuterMeasureClass lintegral_eq_zero_iff Measurable.ennreal_ofReal Filter.EventuallyEq.eq_1 Filter.Eventually.mono ae_restrict_mem ENNReal.ofReal_eq_zero le_of_lt MeasurableSet.compl Measurable.neg ContinuousNeg.measurableNeg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal not_lt neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
withDensity_one 📖	mathematical	—	Measure.withDensity Pi.instOne ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Measure.ext withDensity_apply lintegral_const Measure.restrict_apply Set.univ_inter one_mul
withDensity_smul 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Measure.withDensity Function.hasSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id Measure Measure.instSMul IsScalarTower.right	—	Measure.ext IsScalarTower.right withDensity_apply Measure.coe_smul Pi.smul_apply smul_eq_mul lintegral_const_mul
withDensity_smul' 📖	mathematical	—	Measure.withDensity ENNReal Function.hasSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id Measure Measure.instSMul IsScalarTower.right	—	Measure.ext IsScalarTower.right withDensity_apply Measure.coe_smul Pi.smul_apply smul_eq_mul lintegral_const_mul'
withDensity_smul_measure 📖	mathematical	—	Measure.withDensity ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	Measure.ext IsScalarTower.right withDensity_apply Measure.restrict_smul lintegral_smul_measure
withDensity_sum 📖	mathematical	—	Measure.withDensity Measure.sum	—	Measure.ext Measure.sum_apply withDensity_apply Measure.restrict_sum lintegral_sum_measure
withDensity_tsum 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Measure.withDensity tsum Pi.addCommMonoid ENNReal.instAddCommMonoid Pi.topologicalSpace ENNReal.instTopologicalSpace SummationFilter.unconditional Measure.sum	—	Measure.ext Measure.sum_apply withDensity_apply lintegral_tsum Measurable.aemeasurable lintegral_congr tsum_apply SummationFilter.instNeBotUnconditional ENNReal.instT2Space Pi.summable ENNReal.summable
withDensity_zero 📖	mathematical	—	Measure.withDensity Pi.instZero ENNReal instZeroENNReal Measure Measure.instZero	—	Measure.ext withDensity_apply lintegral_const Measure.restrict_apply Set.univ_inter MulZeroClass.zero_mul
withDensity_zero_left 📖	mathematical	—	Measure.withDensity Measure Measure.instZero	—	Measure.ext withDensity_apply Measure.restrict_zero lintegral_zero_measure

MeasureTheory.IsLocallyFiniteMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withDensity_coe 📖	mathematical	Continuous NNReal NNReal.instTopologicalSpace	MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.Measure.withDensity ENNReal.ofNNReal	—	MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis MeasureTheory.Measure.finiteAt_nhds Filter.HasBasis.restrict_subset nhds_basis_opens' Filter.Tendsto.eventually_le_const instClosedIciTopology OrderTopology.to_orderClosedTopology NNReal.instOrderTopology lt_add_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd NNReal.addLeftMono Continuous.tendsto MeasureTheory.withDensity_apply IsOpen.measurableSet MeasureTheory.setLIntegral_lt_top_of_bddAbove LT.lt.ne Set.forall_mem_image
withDensity_ofReal 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.Measure.withDensity ENNReal.ofReal	—	withDensity_coe Continuous.comp continuous_real_toNNReal

MeasureTheory.Measure

Definitions

Name	Category	Theorems
withDensity 📖	CompOp	173 math math: MeasureTheory.ae_withDensity_iff_ae_restrict, MeasureTheory.withDensity_apply_le, ProbabilityTheory.posterior_eq_withDensity, MeasureTheory.integrable_withDensity_iff_integrable_coe_smul, MeasureTheory.aemeasurable_withDensity_ennreal_iff', VitaliFamily.withDensity_limRatioMeas_eq, VitaliFamily.withDensity_le_mul, VitaliFamily.le_mul_withDensity, setIntegral_withDensity_eq_setIntegral_smul₀, setIntegral_withDensity_eq_setIntegral_toReal_smul, MeasureTheory.withDensity_absolutelyContinuous', Probability.cauchyMeasure_of_scale_ne_zero, MeasureTheory.withDensity_one, MeasureTheory.isFiniteMeasure_withDensity_ofReal, rnDeriv_withDensity_right, MeasureTheory.pdf.eq_of_map_eq_withDensity, haveLebesgueDecomposition_withDensity, MeasureTheory.lintegral_withDensity_eq_lintegral_mul, MeasureTheory.withDensity_apply_eq_zero, setIntegral_withDensity_eq_setIntegral_toReal_smul', MeasureTheory.withDensity_eq_zero_iff, MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part, MeasureTheory.withDensity_zero, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul, MeasureTheory.withDensity_indicator, setIntegral_withDensity_eq_setIntegral_toReal_smul₀, MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity, MeasureTheory.isFiniteMeasure_withDensity, MeasureTheory.SigmaFinite.withDensity_ofReal, haveLebesgueDecomposition_add, measure_sub_singularPart, MeasureTheory.prod_withDensity₀, integral_withDensity_eq_integral_smul, singularPart_def, rnDeriv_add_singularPart, ProbabilityTheory.gaussianReal_of_var_ne_zero, MeasureTheory.prod_withDensity_left, MeasureTheory.IsLocallyFiniteMeasure.withDensity_coe, MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable, MeasureTheory.withDensity_sum, MeasureTheory.withDensity_mul₀, MeasureTheory.integrable_withDensity_iff_integrable_smul', MeasureTheory.ae_withDensity_iff_ae_restrict', MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable, MeasureTheory.mconv_withDensity_eq_mlconvolution, MeasureTheory.ae_withDensity_iff, setIntegral_withDensity_eq_setIntegral_smul₀', withDensity_rnDeriv_le, MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul, MeasureTheory.integrable_withDensity_iff_integrable_smul₀', MeasureTheory.withDensity_apply_eq_zero', MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀, MeasureTheory.MeasurePreserving.withDensity_rnDeriv, MeasureTheory.integrable_withDensity_iff_integrable_smul₀, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul', MeasureTheory.withDensity_tsum, MeasureTheory.map_eq_withDensity_pdf, MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable₀, MeasureTheory.mconv_eq_withDensity_mlconvolution_rnDeriv, MeasureTheory.withDensity_add_left, MeasureTheory.restrict_withDensity, withDensity_rnDeriv_eq_zero, setIntegral_withDensity_eq_setIntegral_toReal_smul₀', compProd_withDensity, withDensity_sub_of_le, MeasureTheory.withDensity_inv_same, MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity', MeasureTheory.SigmaFinite.withDensity, MeasureTheory.withDensity_eq_iff, singularPart_withDensity, withDensity.instIsLocallyFiniteMeasure, HaveLebesgueDecomposition.lebesgue_decomposition, withDensity.instSigmaFinite, MeasureTheory.memL1_smul_of_L1_withDensity, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul, ProbabilityTheory.withDensity_preCDF, MeasureTheory.prod_withDensity_left₀, MeasureTheory.withDensity_inv_same₀, MeasureTheory.prod_withDensity_right₀, rnDeriv_withDensity_right_of_absolutelyContinuous, MeasureTheory.count_withDensity, MeasureTheory.withDensity_apply₀, MeasureTheory.integrable_withDensity_iff_integrable_smul, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul, absolutelyContinuous_withDensity_rnDeriv_swap, MeasureTheory.withDensity_mul, MeasureTheory.withDensity_ae_eq, rnDeriv_def, MeasureTheory.count_withDensity', MeasureTheory.withDensity_ofReal_mutuallySingular, MeasureTheory.withDensity_inv_same_le, MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀', haveLebesgueDecompositionRnDeriv, integral_withDensity_eq_integral_toReal_smul, MeasureTheory.lintegral_withDensity_le_lintegral_mul, setIntegral_withDensity_eq_setIntegral_smul, ProbabilityTheory.Kernel.withDensity_apply, rnDeriv_withDensity, MeasureTheory.conv_withDensity_eq_lconvolution, setIntegral_toReal_rnDeriv_eq_withDensity', aemeasurable_withDensity_iff, MeasureTheory.withDensityᵥ_toReal, MeasureTheory.SignedMeasure.jordanDecomposition_add_withDensity_mutuallySingular, MeasureTheory.withDensity_pdf_le_map, MeasureTheory.withDensity_add_measure, MeasureTheory.aemeasurable_withDensity_ennreal_iff, AbsolutelyContinuous.withDensity_rnDeriv, MeasureTheory.withDensitySMulLI_apply, MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar, AEMeasurable.withDensity_rnDeriv, MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.trim_withDensity, MeasureTheory.integrable_withDensity_iff_integrable_coe_smul₀, MeasureTheory.pdf.eq_of_map_eq_withDensity', rnDeriv_withDensity₀, MeasureTheory.ae_withDensity_iff', MeasureTheory.IsLocallyFiniteMeasure.withDensity_ofReal, MeasureTheory.withDensity_add_right, MeasureTheory.dirac_withDensity', MeasureTheory.withDensityᵥ_smul_eq_withDensityᵥ_withDensity, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul', MeasureTheory.prod_withDensity, MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀, rnDeriv_withDensity_left_of_absolutelyContinuous, singularPart_add_rnDeriv, MeasureTheory.SigmaFinite.withDensity_of_ne_top, MeasureTheory.conv_eq_withDensity_lconvolution_rnDeriv, MeasureTheory.condLExp_def, MeasureTheory.withDensity_smul_measure, MeasureTheory.withDensity_apply', ProbabilityTheory.posterior_eq_withDensity_of_countable, MeasureTheory.withDensity_congr_ae, MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀, MeasureTheory.withDensity_eq_iff_of_sigmaFinite, MeasureTheory.SigmaFinite.withDensity_of_ne_top', MeasureTheory.prod_withDensity_right, integral_withDensity_eq_integral_toReal_smul₀, MeasureTheory.withDensity_smul, measure_sub_rnDeriv, setIntegral_toReal_rnDeriv_eq_withDensity, MeasureTheory.tilted_eq_withDensity_nnreal, rnDeriv_withDensity_rnDeriv, MeasureTheory.noAtoms_withDensity, MeasureTheory.integrable_withDensity_iff, MeasureTheory.withDensity_indicator_one, MeasureTheory.withDensity_mono, absolutelyContinuous_iff_withDensity_rnDeriv_eq, integral_withDensity_eq_integral_smul₀, MeasureTheory.mconv_withDensity_eq_mlconvolution₀, absolutelyContinuous_withDensity_rnDeriv, MeasureTheory.withDensity_const, rnDeriv_withDensity_withDensity_rnDeriv_left, ProbabilityTheory.HasPDF.hasLaw, MeasurableEmbedding.map_withDensity_rnDeriv, MutuallySingular.withDensity, MeasureTheory.exists_measurable_le_withDensity_eq, rnDeriv_withDensity_withDensity_rnDeriv_right, MeasureTheory.restrict_withDensity', withDensity.instIsFiniteMeasure, MeasureTheory.condLExp_of_not_sub_sigma_measurable, MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar, haveLebesgueDecomposition_spec, MeasureTheory.withDensity_smul', withDensity_sub, withDensity.instSFinite, rnDeriv_withDensity_left, aestronglyMeasurable_withDensity_iff, MeasureTheory.withDensity_apply, MeasureTheory.conv_withDensity_eq_mlconvolution₀, withDensity_rnDeriv_eq, MeasureTheory.withDensity_zero_left, MeasureTheory.dirac_withDensity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conv_smul_right 📖	mathematical	—	conv ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right prod_smul_right map_smul
mconv_smul_right 📖	mathematical	—	mconv ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right prod_smul_right map_smul
prod_smul_right 📖	mathematical	—	prod ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Prod.instMeasurableSpace	—	ext IsScalarTower.right prod_apply MeasureTheory.instSFiniteHSMulENNRealMeasure MeasureTheory.lintegral_const_mul measurable_measure_prodMk_left

MeasureTheory.Measure.MutuallySingular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withDensity 📖	mathematical	MeasureTheory.Measure.MutuallySingular	MeasureTheory.Measure.withDensity	—	mono_ac MeasureTheory.withDensity_absolutelyContinuous MeasureTheory.Measure.AbsolutelyContinuous.rfl

MeasureTheory.Measure.withDensity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSFinite 📖	mathematical	—	MeasureTheory.SFinite MeasureTheory.Measure.withDensity	—	MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space MeasureTheory.withDensity_indicator MeasureTheory.Measure.restrict_compl_add_restrict MeasureTheory.withDensity_tsum instCountableNat Measurable.indicator measurable_one ENNReal.tsum_apply Set.indicator_of_mem ENNReal.tsum_one ENat.card_eq_top_of_infinite instInfiniteNat Set.indicator_of_notMem tsum_zero MeasureTheory.SigmaFinite.withDensity_of_ne_top MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass Set.indicator_apply MeasureTheory.SigmaFinite.withDensity MeasureTheory.Restrict.sigmaFinite MeasureTheory.instSFiniteHAddMeasure MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.instSFiniteSumOfCountable MeasureTheory.sum_sfiniteSeq MeasureTheory.withDensity_sum MeasureTheory.isFiniteMeasure_sfiniteSeq MeasureTheory.exists_measurable_le_withDensity_eq

MeasureTheory.SigmaFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withDensity 📖	mathematical	—	MeasureTheory.SigmaFinite MeasureTheory.Measure.withDensity ENNReal.ofNNReal	—	MeasureTheory.withDensity_apply' MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.setLIntegral_lt_top_of_bddAbove LT.lt.ne LE.le.trans_lt MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.inter_subset_left MeasureTheory.measure_spanningSets_lt_top Set.forall_mem_image Set.iUnion_eq_univ_iff MeasureTheory.mem_spanningSets_of_index_le le_max_left Nat.cast_max NNReal.instIsStrictOrderedRing
withDensity_ofReal 📖	mathematical	—	MeasureTheory.SigmaFinite MeasureTheory.Measure.withDensity ENNReal.ofReal	—	withDensity
withDensity_of_ne_top 📖	mathematical	Filter.Eventually ENNReal Top.top instTopENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.SigmaFinite MeasureTheory.Measure.withDensity	—	MeasureTheory.Measure.instOuterMeasureClass Filter.Eventually.mono ENNReal.coe_toNNReal MeasureTheory.withDensity_congr_ae withDensity
withDensity_of_ne_top' 📖	mathematical	—	MeasureTheory.SigmaFinite MeasureTheory.Measure.withDensity	—	withDensity_of_ne_top MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass

---

← Back to Index