Theorems · Theorem · probability

MeasureTheory.pdf.integrable_pdf_smul_iff

∀ {Ω : 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 μ →
    (MeasureTheory.Integrable (fun x => (MeasureTheory.pdf X ℙ μ x).toReal • f x) μ ↔
      MeasureTheory.Integrable (fun x => f (X x)) ℙ)

Defined in

Mathlib.Probability.Density

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupNormedSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.HasPDF