Structures · Analysis
MeasureTheory.HasPDF
A random variable X : Ω → E is said to have a probability density function (HasPDF)
with respect to the measure ℙ on Ω and μ on E
if the push-forward measure of ℙ along X is absolutely continuous with respect to μ
and they have a Lebesgue decomposition (HaveLebesgueDecomposition).
- Defined in
- Mathlib.Probability.Density
- Shape
- 3 explicit arguments · adds aemeasurable', haveLebesgueDecomposition', absolutelyContinuous'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by29
- MeasureTheory.HasPDF.absolutelyContinuous
- MeasureTheory.HasPDF.aemeasurable
- MeasureTheory.HasPDF.aemeasurable'
- MeasureTheory.map_eq_withDensity_pdf
- MeasureTheory.map_eq_setLIntegral_pdf
- MeasureTheory.pdf.eq_of_map_eq_withDensity
- MeasureTheory.pdf.quasiMeasurePreserving_hasPDF
- MeasureTheory.HasPDF.absolutelyContinuous'
- ProbabilityTheory.IndepFun.add_hasPDF'
- MeasureTheory.HasPDF.congr
- MeasureTheory.pdf.integral_pdf_smul
- MeasureTheory.pdf.quasiMeasurePreserving_hasPDF'
- MeasureTheory.pdf.lintegral_eq_measure_univ
- ProbabilityTheory.IndepFun.mul_hasPDF'
- MeasureTheory.pdf.integral_mul_eq_integral
- ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf'
- MeasureTheory.pdf.eq_of_map_eq_withDensity'
- ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf
- MeasureTheory.pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdf
- MeasureTheory.HasPDF.quasiMeasurePreserving_of_measurable
- MeasureTheory.HasPDF.haveLebesgueDecomposition'
- MeasureTheory.HasPDF.haveLebesgueDecomposition
- MeasureTheory.pdf.lintegral_pdf_mul
- ProbabilityTheory.IndepFun.add_hasPDF
- ProbabilityTheory.HasPDF.hasLaw
- ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf
- MeasureTheory.pdf.integrable_pdf_smul_iff
- ProbabilityTheory.IndepFun.mul_hasPDF
- ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf'
Ancestors0
No ancestors.