Theorems · Theorem · probability

ProbabilityTheory.IdentDistrib.pi

∀ {Ω : Type u_1} {Ω' : Type u_2} {ι : Type u_3} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [Countable ι] {E : ι → Type u_6}
  {mE : (i : ι) → MeasurableSpace (E i)} {X : (i : ι) → Ω → E i} {Y : (i : ι) → Ω' → E i},
  (∀ (i : ι), ProbabilityTheory.IdentDistrib (X i) (Y i) μ ν) →
    ProbabilityTheory.iIndepFun X μ →
      ProbabilityTheory.iIndepFun Y ν → ProbabilityTheory.IdentDistrib (fun ω x => X x ω) (fun ω x => Y x ω) μ ν

If (X i) and (Y i) are families of independent random variables indexed by a countable type ι, such that for each i, X i and Y i are identically distributed, then the products X and Y are identically distributed.

Defined in

Mathlib.Probability.IdentDistribIndep

Cited by

0 results in Mathlib

Foundations

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

Assumes

Countable