Random variables are independent iff their joint distribution is the product measure.

There are several possible measurability assumptions:

• The map ω ↦ (Xᵢ(ω))ᵢ is measurable.
• For all i, the map ω ↦ Xᵢ(ω) is measurable.
• The map ω ↦ (Xᵢ(ω))ᵢ is almost everywhere measurable.
• For all i, the map ω ↦ Xᵢ(ω) is almost everywhere measurable. Although the first two options are equivalent, the last two are not if the index set is not countable. Therefore we first prove the third case iIndepFun_iff_map_fun_eq_infinitePi_map₀, then deduce the fourth case in iIndepFun_iff_map_fun_eq_infinitePi_map₀' (assuming the index type is countable), and we prove the first case in iIndepFun_iff_map_fun_eq_infinitePi_map.

theorem ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {𝓧 : ι → Type u_3} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} (mX : AEMeasurable (fun (ω : Ω) (i : ι) => X i ω) μ) : iIndepFun X μ ↔ MeasureTheory.Measure.map (fun (ω : Ω) (i : ι) => X i ω) μ = MeasureTheory.Measure.infinitePi fun (i : ι) => MeasureTheory.Measure.map (X i) μ

Random variables are independent iff their joint distribution is the product measure. This is a version where the random variable ω ↦ (Xᵢ(ω))ᵢ is almost everywhere measurable. See iIndepFun_iff_map_fun_eq_infinitePi_map₀' for a version which only assumes that each Xᵢ is almost everywhere measurable and that ι is countable.

theorem ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀' {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {𝓧 : ι → Type u_3} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} [Countable ι] (mX : ∀ (i : ι), AEMeasurable (X i) μ) : iIndepFun X μ ↔ MeasureTheory.Measure.map (fun (ω : Ω) (i : ι) => X i ω) μ = MeasureTheory.Measure.infinitePi fun (i : ι) => MeasureTheory.Measure.map (X i) μ

Random variables are independent iff their joint distribution is the product measure. This is an AEMeasurable version of iIndepFun_iff_map_fun_eq_infinitePi_map, which is why it requires ι to be countable.

theorem ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {𝓧 : ι → Type u_3} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} (mX : ∀ (i : ι), Measurable (X i)) : iIndepFun X μ ↔ MeasureTheory.Measure.map (fun (ω : Ω) (i : ι) => X i ω) μ = MeasureTheory.Measure.infinitePi fun (i : ι) => MeasureTheory.Measure.map (X i) μ

Random variables are independent iff their joint distribution is the product measure.

theorem ProbabilityTheory.iIndepFun_infinitePi {ι : Type u_1} {𝓧 : ι → Type u_3} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {Ω : ι → Type u_4} {mΩ : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {X : (i : ι) → Ω i → 𝓧 i} (mX : ∀ (i : ι), Measurable (X i)) : iIndepFun (fun (i : ι) (ω : (i : ι) → Ω i) => X i (ω i)) (MeasureTheory.Measure.infinitePi μ)

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