Theorems · Theorem · probability

MeasureTheory.pdf.quasiMeasurePreserving_hasPDF

∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {F : Type u_3} [inst_1 : MeasurableSpace F] {ν : MeasureTheory.Measure F} (X : Ω → E)
  [MeasureTheory.HasPDF X ℙ μ] {g : E → F},
  MeasureTheory.Measure.QuasiMeasurePreserving g μ ν →
    (MeasureTheory.Measure.map g (MeasureTheory.Measure.map X ℙ)).HaveLebesgueDecomposition ν →
      MeasureTheory.HasPDF (g ∘ X) ℙ ν

A random variable that HasPDF transformed under a QuasiMeasurePreserving map also HasPDF if (map g (map X ℙ)).HaveLebesgueDecomposition μ. quasiMeasurePreserving_hasPDF is more useful in the case we are working with a probability measure and a real-valued random variable.

Defined in

Mathlib.Probability.Density

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceMeasureTheory.HasPDF