Theorems · Theorem · probability

ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map

∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : ι → Type u_3}
  {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} [MeasureTheory.IsProbabilityMeasure P],
  (∀ (i : ι), Measurable (X i)) →
    (ProbabilityTheory.iIndepFun X P ↔
      MeasureTheory.Measure.map (fun ω i => X i ω) P =
        MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.map (X i) P)

Random variables are independent iff their joint distribution is the product measure.

Defined in

Mathlib.Probability.Independence.InfinitePi

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure