Theorems · Theorem · probability

MeasureTheory.pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdf

∀ {Ω : 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}
  {Y : Ω → F} [MeasureTheory.IsFiniteMeasure ℙ] [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν]
  [MeasureTheory.HasPDF (fun ω => (X ω, Y ω)) ℙ (μ.prod ν)],
  ProbabilityTheory.IndepFun X Y ℙ ↔
    MeasureTheory.pdf (fun ω => (X ω, Y ω)) ℙ (μ.prod ν) =ᵐ[μ.prod ν] fun z =>
      MeasureTheory.pdf X ℙ μ z.1 * MeasureTheory.pdf Y ℙ ν z.2

Random variables are independent iff their joint density is a product of marginal densities.

Defined in

Mathlib.Probability.Density

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.SigmaFiniteMeasureTheory.SigmaFiniteMeasureTheory.HasPDF