Theorems · Theorem · probability

ProbabilityTheory.iIndepFun_pi

∀ {ι : Type u_11} [inst : Fintype ι] {Ω : ι → Type u_12} {mΩ : (i : ι) → MeasurableSpace (Ω i)}
  {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {𝓧 : ι → Type u_13}
  [inst_2 : (i : ι) → MeasurableSpace (𝓧 i)] {X : (i : ι) → Ω i → 𝓧 i},
  (∀ (i : ι), AEMeasurable (X i) (μ i)) →
    ProbabilityTheory.iIndepFun (fun i ω => X i (ω i)) (MeasureTheory.Measure.pi μ)

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

Defined in

Mathlib.Probability.Independence.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeMeasureTheory.IsProbabilityMeasureMeasurableSpace