Theorems · Theorem · probability

MeasureTheory.map_eq_setLIntegral_pdf

∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} (X : Ω → E)
  (ℙ : MeasureTheory.Measure Ω) (μ : autoParam (MeasureTheory.Measure E) MeasureTheory.map_eq_setLIntegral_pdf._auto_1)
  [hX : MeasureTheory.HasPDF X ℙ μ] {s : Set E},
  MeasurableSet s → (MeasureTheory.Measure.map X ℙ) s = ∫⁻ (x : E) in s, MeasureTheory.pdf X ℙ μ x ∂μ

Defined in

Mathlib.Probability.Density

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasureTheory.HasPDF