Theorems · Theorem · probability

MeasureTheory.pdf.integral_pdf_smul

∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {F : Type u_3} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [MeasureTheory.IsFiniteMeasure ℙ] {X : Ω → E} [MeasureTheory.HasPDF X ℙ μ] {f : E → F},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∫ (x : E), (MeasureTheory.pdf X ℙ μ x).toReal • f x ∂μ = ∫ (x : Ω), f (X x) ∂ℙ

The Law of the Unconscious Statistician: Given a random variable X and a measurable function f, f ∘ X is a random variable with expectation ∫ x, pdf X x • f x ∂μ where μ is a measure on the codomain of X.

Defined in

Mathlib.Probability.Density

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupNormedSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.HasPDF