Independence of an infinite family of random variables

In this file we provide several results about independence of arbitrary families of random variables, relying on Measure.infinitePi.

Implementation note

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.

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

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 Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {𝓧 : ι → Type u_3} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} [Countable ι] (mX : ∀ (i : ι), AEMeasurable (X i) P) : iIndepFun X P ↔ MeasureTheory.Measure.map (fun (ω : Ω) (i : ι) => X i ω) P = MeasureTheory.Measure.infinitePi fun (i : ι) => MeasureTheory.Measure.map (X i) P

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 Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {𝓧 : ι → Type u_3} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} (mX : ∀ (i : ι), Measurable (X i)) : iIndepFun X P ↔ MeasureTheory.Measure.map (fun (ω : Ω) (i : ι) => X i ω) P = MeasureTheory.Measure.infinitePi fun (i : ι) => MeasureTheory.Measure.map (X i) P

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)} {P : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)] {X : (i : ι) → Ω i → 𝓧 i} (mX : ∀ (i : ι), Measurable (X i)) : iIndepFun (fun (i : ι) (ω : (i : ι) → Ω i) => X i (ω i)) (MeasureTheory.Measure.infinitePi P)

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

theorem 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} (mX : ∀ (i : ι) (j : κ i), Measurable (X i j)) (h1 : iIndepFun (fun (i : ι) (ω : Ω) (x : κ i) => X i x ω) P) (h2 : ∀ (i : ι), iIndepFun (X i) P) : iIndepFun (fun (p : (i : ι) × κ i) (ω : Ω) => 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'.

theorem ProbabilityTheory.iIndepFun_uncurry_infinitePi {ι : Type u_1} {κ : ι → Type u_4} {𝓧 : (i : ι) → κ i → Type u_5} {m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)} {Ω : (i : ι) → κ i → Type u_6} {mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)} {X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j} (μ : (i : ι) → (j : κ i) → MeasureTheory.Measure (Ω i j)) [∀ (i : ι) (j : κ i), MeasureTheory.IsProbabilityMeasure (μ i j)] (mX : ∀ (i : ι) (j : κ i), Measurable (X i j)) : iIndepFun (fun (p : (i : ι) × κ i) (ω : (i : ι) → (j : κ i) → Ω i j) => X p.fst p.snd (ω p.fst p.snd)) (MeasureTheory.Measure.infinitePi fun (i : ι) => MeasureTheory.Measure.infinitePi (μ i))

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

theorem ProbabilityTheory.iIndepFun_uncurry' {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {κ : Type u_4} {𝓧 : ι → κ → Type u_5} {m𝓧 : (i : ι) → (j : κ) → MeasurableSpace (𝓧 i j)} {X : (i : ι) → (j : κ) → Ω → 𝓧 i j} (mX : ∀ (i : ι) (j : κ), Measurable (X i j)) (h1 : iIndepFun (fun (i : ι) (ω : Ω) (x : κ) => X i x ω) P) (h2 : ∀ (i : ι), iIndepFun (X i) P) : iIndepFun (fun (p : ι × κ) (ω : Ω) => X p.1 p.2 ω) 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 non-dependent version of iIndepFun_uncurry.

theorem ProbabilityTheory.iIndepFun_uncurry_infinitePi' {ι : Type u_1} {κ : Type u_4} {𝓧 : ι → κ → Type u_5} {m𝓧 : (i : ι) → (j : κ) → MeasurableSpace (𝓧 i j)} {Ω : ι → κ → Type u_6} {mΩ : (i : ι) → (j : κ) → MeasurableSpace (Ω i j)} {X : (i : ι) → (j : κ) → Ω i j → 𝓧 i j} (μ : (i : ι) → (j : κ) → MeasureTheory.Measure (Ω i j)) [∀ (i : ι) (j : κ), MeasureTheory.IsProbabilityMeasure (μ i j)] (mX : ∀ (i : ι) (j : κ), Measurable (X i j)) : iIndepFun (fun (p : ι × κ) (ω : (i : ι) → (j : κ) → Ω i j) => X p.1 p.2 (ω p.1 p.2)) (MeasureTheory.Measure.infinitePi fun (i : ι) => MeasureTheory.Measure.infinitePi (μ i))

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