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	30 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.hasFiniteIntegral_mul, 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 ENNReal 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 ENNReal 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 Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace Real.instMul ENNReal.toReal MeasureTheory.pdf MeasureTheory.MeasureSpace.volume	—	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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 ENNReal 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 Real measurableSpace MeasureTheory.MeasureSpace.volume measureSpace MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Measure.map	—	hasPDF_iff

---

← Back to Index