Theorems · Theorem · probability

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},
  ProbabilityTheory.IdentDistrib X Z μ ν →
    ProbabilityTheory.IdentDistrib Y W μ ν →
      ProbabilityTheory.IndepFun X Y μ →
        ProbabilityTheory.IndepFun Z W ν →
          ProbabilityTheory.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.

Defined in

Mathlib.Probability.IdentDistribIndep

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasure