Theorems · Theorem · probability

MeasureTheory.pdf.hasFiniteIntegral_mul

∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsFiniteMeasure ℙ]
  {f : ℝ → ℝ} {g : ℝ → ENNReal},
  MeasureTheory.pdf X ℙ MeasureTheory.volume =ᵐ[MeasureTheory.volume] g →
    ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ⊤ →
      MeasureTheory.HasFiniteIntegral (fun x => f x * (MeasureTheory.pdf X ℙ MeasureTheory.volume x).toReal)
        MeasureTheory.volume

Defined in

Mathlib.Probability.Density

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasure