Theorems · Theorem · probability

ProbabilityTheory.iIndepFun_uncurry_infinitePi

∀ {ι : Type u_1} {κ : ι → Type u_4} {𝓧 : (i : ι) → κ i → Type u_5} {m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)}
  {Ω : (i : ι) → κ i → Type u_6} {mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)}
  {X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j} (μ : (i : ι) → (j : κ i) → MeasureTheory.Measure (Ω i j))
  [∀ (i : ι) (j : κ i), MeasureTheory.IsProbabilityMeasure (μ i j)],
  (∀ (i : ι) (j : κ i), Measurable (X i j)) →
    ProbabilityTheory.iIndepFun (fun p ω => X p.fst p.snd (ω p.fst p.snd))
      (MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.infinitePi (μ i))

Given random variables X i j : Ω i j → 𝓧 i j, they are independent when viewed as random variables defined on the product space Π i, Π j, Ω i j.

Defined in

Mathlib.Probability.Independence.InfinitePi

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure