Theorems · Theorem · probability

MeasureTheory.pdf.lintegral_pdf_mul

∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {X : Ω → E} [MeasureTheory.HasPDF X ℙ μ] {f : E → ENNReal},
  AEMeasurable f μ → ∫⁻ (x : E), MeasureTheory.pdf X ℙ μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ

The Law of the Unconscious Statistician for nonnegative random variables.

Defined in

Mathlib.Probability.Density

Cited by

0 results in Mathlib

Foundations

Depth 216 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceMeasureTheory.HasPDF