Theorems · Theorem · probability

MeasureTheory.pdf.integral_mul_eq_integral

∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsFiniteMeasure ℙ]
  [MeasureTheory.HasPDF X ℙ MeasureTheory.volume],
  ∫ (x : ℝ), x * (MeasureTheory.pdf X ℙ MeasureTheory.volume x).toReal = ∫ (x : Ω), X x ∂ℙ

If X is a real-valued random variable that has pdf f, then the expectation of X equals ∫ x, x * f x ∂λ where λ is the Lebesgue measure.

Defined in

Mathlib.Probability.Density

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.HasPDF