Theorems · Definition · probability
MeasureTheory.pdf
{Ω : Type u_1} →
{E : Type u_2} →
[inst : MeasurableSpace E] →
{x : MeasurableSpace Ω} →
(Ω → E) → MeasureTheory.Measure Ω → autoParam (MeasureTheory.Measure E) MeasureTheory.pdf._auto_1 → E → ENNRealIf X is a random variable, then pdf X ℙ μ
is the Radon–Nikodym derivative of the push-forward measure of ℙ along X with respect to μ.
- Defined in
- Mathlib.Probability.Density
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ENNRealstatement · cited by 9,879
- MeasureTheory.Measure.mapproof · cited by 858
- MeasureTheory.Measure.rnDerivproof · cited by 234
Cited by32
Results whose statement or proof uses this declaration.
- MeasureTheory.pdf_defstatement · cited by 6
- MeasureTheory.map_eq_withDensity_pdfstatement · cited by 6
- MeasureTheory.measurable_pdfstatement · cited by 4
- MeasureTheory.pdf.IsUniform.pdf_eqstatement and proof · cited by 3
- MeasureTheory.pdf.IsUniform.pdf_eq_zero_of_measure_eq_zero_or_topstatement · cited by 2
- MeasureTheory.pdf.eq_of_map_eq_withDensitystatement and proof · cited by 2
- MeasureTheory.map_eq_setLIntegral_pdfstatement and proof · cited by 2
- MeasureTheory.pdf_of_not_aemeasurablestatement · cited by 1
- MeasureTheory.pdf_of_not_haveLebesgueDecompositionstatement · cited by 1
- MeasureTheory.aemeasurable_of_pdf_ne_zerostatement and proof · cited by 1
- MeasureTheory.pdf.ae_lt_topstatement · cited by 1
- MeasureTheory.pdf.hasFiniteIntegral_mulstatement and proof · cited by 1