Theorems · Theorem · probability

ProbabilityTheory.iIndepFun_uncurry

∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {κ : ι → Type u_4}
  {𝓧 : (i : ι) → κ i → Type u_5} {m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)}
  {X : (i : ι) → (j : κ i) → Ω → 𝓧 i j},
  (∀ (i : ι) (j : κ i), Measurable (X i j)) →
    ProbabilityTheory.iIndepFun (fun i ω x => X i x ω) P →
      (∀ (i : ι), ProbabilityTheory.iIndepFun (X i) P) → ProbabilityTheory.iIndepFun (fun p ω => X p.fst p.snd ω) P

Consider ((Xᵢⱼ)ⱼ)ᵢ a family of families of random variables. Assume that for any i, the random variables (Xᵢⱼ)ⱼ are independent. Assume furthermore that the random variables ((Xᵢⱼ)ⱼ)ᵢ are independent. Then the random variables (Xᵢⱼ) indexed by pairs (i, j) are independent. This is a dependent version of iIndepFun_uncurry'.

Defined in

Mathlib.Probability.Independence.InfinitePi

Cited by

2 results in Mathlib

Foundations

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