Theorems · Theorem · probability
MeasureTheory.HasPDF.aemeasurable
∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} (X : Ω → E)
(ℙ : MeasureTheory.Measure Ω) (μ : MeasureTheory.Measure E) [MeasureTheory.HasPDF X ℙ μ], AEMeasurable X ℙ- Defined in
- Mathlib.Probability.Density
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound
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
- AEMeasurablestatement · cited by 840
- MeasureTheory.HasPDFstatement and proof · cited by 37
- MeasureTheory.HasPDF.aemeasurable'proof · cited by 7
Cited by8
Results whose statement or proof uses this declaration.
- MeasureTheory.pdf.quasiMeasurePreserving_hasPDFproof · cited by 1
- MeasureTheory.HasPDF.congrproof · cited by 1
- MeasureTheory.pdf.integral_pdf_smulproof · cited by 1
- MeasureTheory.pdf.lintegral_eq_measure_univproof · cited by 1
- ProbabilityTheory.HasPDF.hasLawproof · cited by 0
- MeasureTheory.pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdfproof · cited by 0
- MeasureTheory.pdf.integrable_pdf_smul_iffproof · cited by 0
- MeasureTheory.pdf.lintegral_pdf_mulproof · cited by 0