Results about identically distributed random variables and independence

Main statements

• IdentDistrib.prodMk: if X and Y are independent random variables on Ω, Z and W are independent random variables on Ω', such that X and Z are identically distributed and Y and W are identically distributed, then the pairs (X, Y) and (Z, W) are identically distributed.
• IdentDistrib.pi: 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.

theorem ProbabilityTheory.IdentDistrib.prodMk {Ω : Type u_1} {Ω' : Type u_2} {E : Type u_4} {F : Type u_5} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {mE : MeasurableSpace E} {mF : MeasurableSpace F} {μ : MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω'} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → E} {Y : Ω → F} {Z : Ω' → E} {W : Ω' → F} (hXZ : IdentDistrib X Z μ ν) (hYW : IdentDistrib Y W μ ν) (hXY : IndepFun X Y μ) (hZW : IndepFun Z W ν) : IdentDistrib (fun (ω : Ω) => (X ω, Y ω)) (fun (ω' : Ω') => (Z ω', W ω')) μ ν

If X and Y are independent random variables on Ω, Z and W are independent random variables on Ω', such that X and Z are identically distributed and Y and W are identically distributed, then the pairs (X, Y) and (Z, W) are identically distributed.

theorem 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} (h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν) (hX_ind : iIndepFun X μ) (hY_ind : iIndepFun Y ν) : 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.