Density

📁 Source: Mathlib/Probability/Density.lean

Statistics

Metric	Count
Definitions HasPDF, pdf	2
Theorems absolutelyContinuous, absolutelyContinuous', aemeasurable, aemeasurable', congr_iff, haveLebesgueDecomposition, haveLebesgueDecomposition', quasiMeasurePreserving_of_measurable, aemeasurable_of_pdf_ne_zero, hasPDF_iff, hasPDF_iff_of_aemeasurable, hasPDF_of_map_eq_withDensity, hasPDF_of_pdf_ne_zero, map_eq_setLIntegral_pdf, map_eq_withDensity_pdf, measurable_pdf, ae_lt_top, eq_of_map_eq_withDensity, eq_of_map_eq_withDensity', hasFiniteIntegral_mul, indepFun_iff_pdf_prod_eq_pdf_mul_pdf, integrable_pdf_smul_iff, integral_mul_eq_integral, integral_pdf_smul, lintegral_eq_measure_univ, lintegral_pdf_mul, ofReal_toReal_ae_eq, quasiMeasurePreserving_hasPDF, quasiMeasurePreserving_hasPDF', pdf_def, pdf_of_not_aemeasurable, pdf_of_not_haveLebesgueDecomposition, setLIntegral_pdf_le_map, withDensity_pdf_le_map, add_hasPDF, add_hasPDF', mul_hasPDF, mul_hasPDF', pdf_add_eq_lconvolution_pdf, pdf_add_eq_lconvolution_pdf', pdf_mul_eq_mlconvolution_pdf, pdf_mul_eq_mlconvolution_pdf', hasPDF_iff, hasPDF_iff_of_aemeasurable	44
Total	46

MeasureTheory

Definitions

Name	Category	Theorems
HasPDF 📖	CompData	15 math math: ProbabilityTheory.IndepFun.mul_hasPDF', pdf.IsUniform.hasPDF, hasPDF_iff, ProbabilityTheory.IndepFun.add_hasPDF', pdf.quasiMeasurePreserving_hasPDF', HasPDF.congr, hasPDF_of_pdf_ne_zero, Real.hasPDF_iff, Real.hasPDF_iff_of_aemeasurable, HasPDF.congr_iff, hasPDF_of_map_eq_withDensity, ProbabilityTheory.IndepFun.add_hasPDF, hasPDF_iff_of_aemeasurable, pdf.quasiMeasurePreserving_hasPDF, ProbabilityTheory.IndepFun.mul_hasPDF
pdf 📖	CompOp	29 math math: pdf.integral_mul_eq_integral, pdf.IsUniform.mul_pdf_integrable, pdf_of_not_haveLebesgueDecomposition, pdf.eq_of_map_eq_withDensity, pdf.integral_pdf_smul, pdf.uniformPDF_eq_pdf, ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf', measurable_pdf, map_eq_withDensity_pdf, ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf, ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf, pdf.lintegral_pdf_mul, pdf.IsUniform.pdf_toReal_ae_eq, pdf.IsUniform.pdf_eq_zero_of_measure_eq_zero_or_top, map_eq_setLIntegral_pdf, pdf.IsUniform.pdf_eq, ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf', pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdf, pdf_of_not_aemeasurable, pdf.congr, withDensity_pdf_le_map, setLIntegral_pdf_le_map, pdf.lintegral_eq_measure_univ, pdf.integrable_pdf_smul_iff, pdf_def, pdf.eq_of_map_eq_withDensity', ProbabilityTheory.HasPDF.hasLaw, pdf.ofReal_toReal_ae_eq, pdf.ae_lt_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_of_pdf_ne_zero 📖	mathematical	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass pdf Pi.instZero instZeroENNReal	AEMeasurable	—	Measure.instOuterMeasureClass Mathlib.Tactic.Contrapose.contrapose₂ pdf_of_not_aemeasurable
hasPDF_iff 📖	mathematical	—	HasPDF AEMeasurable Measure.HaveLebesgueDecomposition Measure.map Measure.AbsolutelyContinuous	—	—
hasPDF_iff_of_aemeasurable 📖	mathematical	AEMeasurable	HasPDF Measure.HaveLebesgueDecomposition Measure.map Measure.AbsolutelyContinuous	—	hasPDF_iff
hasPDF_of_map_eq_withDensity 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Measure.map Measure.withDensity	HasPDF	—	withDensity_congr_ae Measure.haveLebesgueDecomposition_withDensity withDensity_absolutelyContinuous
hasPDF_of_pdf_ne_zero 📖	mathematical	Measure.AbsolutelyContinuous Measure.map Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass pdf Pi.instZero instZeroENNReal	HasPDF	—	Measure.instOuterMeasureClass aemeasurable_of_pdf_ne_zero Mathlib.Tactic.Contrapose.contrapose₂ pdf_of_not_haveLebesgueDecomposition Filter.univ_mem'
map_eq_setLIntegral_pdf 📖	mathematical	MeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.map lintegral Measure.restrict pdf	—	withDensity_apply map_eq_withDensity_pdf
map_eq_withDensity_pdf 📖	mathematical	—	Measure.map Measure.withDensity pdf	—	pdf_def Measure.withDensity_rnDeriv_eq HasPDF.haveLebesgueDecomposition HasPDF.absolutelyContinuous
measurable_pdf 📖	mathematical	—	Measurable ENNReal ENNReal.measurableSpace pdf	—	Measure.measurable_rnDeriv
pdf_def 📖	mathematical	—	pdf Measure.rnDeriv Measure.map	—	—
pdf_of_not_aemeasurable 📖	mathematical	AEMeasurable	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass pdf Pi.instZero instZeroENNReal	—	Measure.instOuterMeasureClass pdf_def Measure.map_of_not_aemeasurable Measure.rnDeriv_zero
pdf_of_not_haveLebesgueDecomposition 📖	mathematical	Measure.HaveLebesgueDecomposition Measure.map	pdf Pi.instZero ENNReal instZeroENNReal	—	Measure.rnDeriv_of_not_haveLebesgueDecomposition
setLIntegral_pdf_le_map 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.restrict pdf DFunLike.coe Measure Set Measure.instFunLike Measure.map	—	LE.le.trans withDensity_apply_le withDensity_pdf_le_map
withDensity_pdf_le_map 📖	mathematical	—	Measure Preorder.toLE PartialOrder.toPreorder Measure.instPartialOrder Measure.withDensity pdf Measure.map	—	Measure.withDensity_rnDeriv_le

MeasureTheory.HasPDF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure.map	—	absolutelyContinuous'
absolutelyContinuous' 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure.map	—	—
aemeasurable 📖	mathematical	—	AEMeasurable	—	aemeasurable'
aemeasurable' 📖	mathematical	—	AEMeasurable	—	—
congr_iff 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	MeasureTheory.HasPDF	—	MeasureTheory.Measure.instOuterMeasureClass congr Filter.EventuallyEq.symm
haveLebesgueDecomposition 📖	mathematical	—	MeasureTheory.Measure.HaveLebesgueDecomposition MeasureTheory.Measure.map	—	haveLebesgueDecomposition'
haveLebesgueDecomposition' 📖	mathematical	—	MeasureTheory.Measure.HaveLebesgueDecomposition MeasureTheory.Measure.map	—	—
quasiMeasurePreserving_of_measurable 📖	mathematical	Measurable	MeasureTheory.Measure.QuasiMeasurePreserving	—	absolutelyContinuous

MeasureTheory.pdf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_lt_top 📖	mathematical	—	Filter.Eventually ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.pdf Top.top instTopENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.rnDeriv_lt_top MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.isFiniteMeasure_map
eq_of_map_eq_withDensity 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	MeasureTheory.Measure.map MeasureTheory.Measure.withDensity Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.pdf	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.map_eq_withDensity_pdf MeasureTheory.withDensity_eq_iff Measurable.aemeasurable MeasureTheory.measurable_pdf lintegral_eq_measure_univ MeasureTheory.measure_ne_top
eq_of_map_eq_withDensity' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	MeasureTheory.Measure.map MeasureTheory.Measure.withDensity Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.pdf	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.withDensity_eq_iff_of_sigmaFinite Measurable.aemeasurable MeasureTheory.measurable_pdf MeasureTheory.map_eq_withDensity_pdf
hasFiniteIntegral_mul 📖	mathematical	Filter.EventuallyEq Real ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume MeasureTheory.pdf Real.measurableSpace	MeasureTheory.HasFiniteIntegral ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.instMul ENNReal.toReal	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.hasFiniteIntegral_iff_enorm MeasureTheory.ae_eq_trans Filter.EventuallyEq.fun_mul MeasureTheory.ae_eq_refl Filter.EventuallyEq.symm ofReal_toReal_ae_eq enorm_smul instENormSMulClass NormedSpace.toNormSMulClass Real.enorm_eq_ofReal ENNReal.toReal_nonneg lt_top_iff_ne_top MeasureTheory.lintegral_congr_ae
indepFun_iff_pdf_prod_eq_pdf_mul_pdf 📖	mathematical	—	ProbabilityTheory.IndepFun Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure Prod.instMeasurableSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.prod MeasureTheory.pdf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	quasiMeasurePreserving_hasPDF' MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.quasiMeasurePreserving_fst MeasureTheory.Measure.quasiMeasurePreserving_snd MeasureTheory.Measure.prod_eq MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.withDensity_apply MeasurableSet.prod MeasureTheory.Measure.prod_restrict MeasureTheory.lintegral_prod_mul MeasureTheory.instSFiniteRestrict Measurable.aemeasurable MeasureTheory.measurable_pdf MeasureTheory.map_eq_setLIntegral_pdf MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map MeasureTheory.HasPDF.aemeasurable eq_of_map_eq_withDensity Measurable.mul ENNReal.instMeasurableMul₂ Measurable.comp measurable_fst measurable_snd
integrable_pdf_smul_iff 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField ENNReal.toReal MeasureTheory.pdf	—	MeasureTheory.integrable_map_measure MeasureTheory.AEStronglyMeasurable.mono_ac MeasureTheory.HasPDF.absolutelyContinuous MeasureTheory.HasPDF.aemeasurable MeasureTheory.map_eq_withDensity_pdf MeasureTheory.pdf_def MeasureTheory.integrable_rnDeriv_smul_iff MeasureTheory.HasPDF.haveLebesgueDecomposition MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.Measure.withDensity_rnDeriv_eq
integral_mul_eq_integral 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume Real.instMul ENNReal.toReal MeasureTheory.pdf	—	mul_comm integral_pdf_smul Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace measurable_id
integral_pdf_smul 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasureTheory.integral Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField ENNReal.toReal MeasureTheory.pdf	—	MeasureTheory.integral_map MeasureTheory.HasPDF.aemeasurable MeasureTheory.AEStronglyMeasurable.mono_ac MeasureTheory.HasPDF.absolutelyContinuous MeasureTheory.map_eq_withDensity_pdf MeasureTheory.pdf_def MeasureTheory.integral_rnDeriv_smul MeasureTheory.HasPDF.haveLebesgueDecomposition MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.Measure.withDensity_rnDeriv_eq
lintegral_eq_measure_univ 📖	mathematical	—	MeasureTheory.lintegral MeasureTheory.pdf DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.univ	—	MeasureTheory.setLIntegral_univ MeasureTheory.map_eq_setLIntegral_pdf MeasurableSet.univ MeasureTheory.Measure.map_apply_of_aemeasurable MeasureTheory.HasPDF.aemeasurable Set.preimage_univ
lintegral_pdf_mul 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring MeasureTheory.pdf	—	MeasureTheory.pdf_def MeasureTheory.lintegral_map' AEMeasurable.mono_ac MeasureTheory.HasPDF.absolutelyContinuous MeasureTheory.HasPDF.aemeasurable MeasureTheory.lintegral_rnDeriv_mul MeasureTheory.HasPDF.haveLebesgueDecomposition
ofReal_toReal_ae_eq 📖	mathematical	—	Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass ENNReal.ofReal ENNReal.toReal MeasureTheory.pdf	—	MeasureTheory.ofReal_toReal_ae_eq ae_lt_top
quasiMeasurePreserving_hasPDF 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving	MeasureTheory.HasPDF	—	AEMeasurable.mono_ac MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable MeasureTheory.HasPDF.absolutelyContinuous MeasureTheory.hasPDF_iff AEMeasurable.map_map_of_aemeasurable MeasureTheory.HasPDF.aemeasurable Measurable.comp_aemeasurable MeasureTheory.Measure.QuasiMeasurePreserving.measurable MeasureTheory.Measure.AbsolutelyContinuous.trans MeasureTheory.Measure.AbsolutelyContinuous.map MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous
quasiMeasurePreserving_hasPDF' 📖	mathematical	MeasureTheory.Measure.QuasiMeasurePreserving	MeasureTheory.HasPDF	—	quasiMeasurePreserving_hasPDF MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.Measure.instSFiniteMap

ProbabilityTheory.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_hasPDF 📖	mathematical	ProbabilityTheory.IndepFun	MeasureTheory.HasPDF Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	add_hasPDF' MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.isFiniteMeasure_map
add_hasPDF' 📖	mathematical	ProbabilityTheory.IndepFun	MeasureTheory.HasPDF Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	MeasureTheory.HasPDF.aemeasurable' MeasureTheory.hasPDF_iff_of_aemeasurable AEMeasurable.add' map_add_eq_map_conv_map₀' MeasureTheory.HaveLebesgueDecomposition.conv MeasureTheory.HasPDF.haveLebesgueDecomposition MeasureTheory.HasPDF.absolutelyContinuous MeasureTheory.Measure.conv_absolutelyContinuous MeasureTheory.instSFiniteOfSigmaFinite
mul_hasPDF 📖	mathematical	ProbabilityTheory.IndepFun	MeasureTheory.HasPDF Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	mul_hasPDF' MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.isFiniteMeasure_map
mul_hasPDF' 📖	mathematical	ProbabilityTheory.IndepFun	MeasureTheory.HasPDF Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	MeasureTheory.HasPDF.aemeasurable' MeasureTheory.hasPDF_iff_of_aemeasurable AEMeasurable.mul' map_mul_eq_map_mconv_map₀' MeasureTheory.HaveLebesgueDecomposition.mconv MeasureTheory.HasPDF.haveLebesgueDecomposition MeasureTheory.HasPDF.absolutelyContinuous MeasureTheory.Measure.mconv_absolutelyContinuous MeasureTheory.instSFiniteOfSigmaFinite
pdf_add_eq_lconvolution_pdf 📖	mathematical	ProbabilityTheory.IndepFun	Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.pdf Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid MeasureTheory.lconvolution NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.pdf.eq_1 map_add_eq_map_conv_map₀ MeasureTheory.HasPDF.aemeasurable' MeasureTheory.rnDeriv_conv MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.HasPDF.haveLebesgueDecomposition MeasureTheory.HasPDF.absolutelyContinuous
pdf_add_eq_lconvolution_pdf' 📖	mathematical	ProbabilityTheory.IndepFun	Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.pdf Pi.instAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid MeasureTheory.lconvolution NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.pdf.eq_1 map_add_eq_map_conv_map₀' MeasureTheory.HasPDF.aemeasurable' MeasureTheory.rnDeriv_conv' MeasureTheory.HasPDF.absolutelyContinuous
pdf_mul_eq_mlconvolution_pdf 📖	mathematical	ProbabilityTheory.IndepFun	Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.pdf Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MeasureTheory.mlconvolution InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.pdf.eq_1 map_mul_eq_map_mconv_map₀ MeasureTheory.HasPDF.aemeasurable' MeasureTheory.rnDeriv_mconv MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.HasPDF.haveLebesgueDecomposition MeasureTheory.HasPDF.absolutelyContinuous
pdf_mul_eq_mlconvolution_pdf' 📖	mathematical	ProbabilityTheory.IndepFun	Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.pdf Pi.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MeasureTheory.mlconvolution InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.pdf.eq_1 map_mul_eq_map_mconv_map₀' MeasureTheory.HasPDF.aemeasurable' MeasureTheory.rnDeriv_mconv' MeasureTheory.HasPDF.absolutelyContinuous

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasPDF_iff 📖	mathematical	—	MeasureTheory.HasPDF Real measurableSpace MeasureTheory.MeasureSpace.volume measureSpace AEMeasurable MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure.map	—	MeasureTheory.hasPDF_iff MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.Measure.instSFiniteMap MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal
hasPDF_iff_of_aemeasurable 📖	mathematical	AEMeasurable Real measurableSpace	MeasureTheory.HasPDF MeasureTheory.MeasureSpace.volume measureSpace MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure.map	—	hasPDF_iff

---

← Back to Index