Documentation Verification Report

Density

πŸ“ Source: Mathlib/Probability/Density.lean

Statistics

MetricCount
DefinitionsHasPDF, pdf
2
TheoremsabsolutelyContinuous, 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
Total46

MeasureTheory

Definitions

NameCategoryTheorems
HasPDF πŸ“–CompData
15 mathmath: 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 mathmath: 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

NameKindAssumesProvesValidatesDepends On
aemeasurable_of_pdf_ne_zero πŸ“–mathematicalFilter.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 πŸ“–mathematicalAEMeasurableHasPDF
Measure.HaveLebesgueDecomposition
Measure.map
Measure.AbsolutelyContinuous
β€”hasPDF_iff
hasPDF_of_map_eq_withDensity πŸ“–mathematicalAEMeasurable
ENNReal
ENNReal.measurableSpace
Measure.map
Measure.withDensity
HasPDFβ€”withDensity_congr_ae
Measure.haveLebesgueDecomposition_withDensity
withDensity_absolutelyContinuous
hasPDF_of_pdf_ne_zero πŸ“–mathematicalMeasure.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 πŸ“–mathematicalMeasurableSetDFunLike.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 πŸ“–mathematicalAEMeasurableFilter.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 πŸ“–mathematicalMeasure.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

NameKindAssumesProvesValidatesDepends 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 πŸ“–mathematicalFilter.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 πŸ“–mathematicalMeasurableMeasureTheory.Measure.QuasiMeasurePreservingβ€”absolutelyContinuous

MeasureTheory.pdf

Theorems

NameKindAssumesProvesValidatesDepends 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 πŸ“–mathematicalAEMeasurable
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' πŸ“–mathematicalAEMeasurable
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 πŸ“–mathematicalFilter.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 πŸ“–mathematicalMeasureTheory.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 πŸ“–mathematicalMeasureTheory.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 πŸ“–mathematicalAEMeasurable
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 πŸ“–mathematicalMeasureTheory.Measure.QuasiMeasurePreservingMeasureTheory.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' πŸ“–mathematicalMeasureTheory.Measure.QuasiMeasurePreservingMeasureTheory.HasPDFβ€”quasiMeasurePreserving_hasPDF
MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite
MeasureTheory.Measure.instSFiniteMap

ProbabilityTheory.IndepFun

Theorems

NameKindAssumesProvesValidatesDepends On
add_hasPDF πŸ“–mathematicalProbabilityTheory.IndepFunMeasureTheory.HasPDF
Pi.instAdd
AddZero.toAdd
AddZeroClass.toAddZero
AddMonoid.toAddZeroClass
SubNegMonoid.toAddMonoid
AddGroup.toSubNegMonoid
β€”add_hasPDF'
MeasureTheory.IsFiniteMeasure.toSigmaFinite
MeasureTheory.Measure.isFiniteMeasure_map
add_hasPDF' πŸ“–mathematicalProbabilityTheory.IndepFunMeasureTheory.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 πŸ“–mathematicalProbabilityTheory.IndepFunMeasureTheory.HasPDF
Pi.instMul
MulOne.toMul
MulOneClass.toMulOne
Monoid.toMulOneClass
DivInvMonoid.toMonoid
Group.toDivInvMonoid
β€”mul_hasPDF'
MeasureTheory.IsFiniteMeasure.toSigmaFinite
MeasureTheory.Measure.isFiniteMeasure_map
mul_hasPDF' πŸ“–mathematicalProbabilityTheory.IndepFunMeasureTheory.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 πŸ“–mathematicalProbabilityTheory.IndepFunFilter.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' πŸ“–mathematicalProbabilityTheory.IndepFunFilter.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 πŸ“–mathematicalProbabilityTheory.IndepFunFilter.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' πŸ“–mathematicalProbabilityTheory.IndepFunFilter.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

NameKindAssumesProvesValidatesDepends 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 πŸ“–mathematicalAEMeasurable
Real
measurableSpace
MeasureTheory.HasPDF
MeasureTheory.MeasureSpace.volume
measureSpace
MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.map
β€”hasPDF_iff

---

← Back to Index