Theorems · Theorem · probability

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},
  (∀ (i : ι), Measurable (X i)) →
    ProbabilityTheory.iIndepFun (fun 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.

Defined in: Mathlib.Probability.Independence.InfinitePi
Cited by: 3 results in Mathlib
Foundations: Depth 285 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasureTheory.IsProbabilityMeasure

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
Measurablestatement and proof · cited by 1,499
MeasureTheory.Measure.mapproof · cited by 858
MeasureTheory.IsProbabilityMeasurestatement and proof · cited by 392
ProbabilityTheory.iIndepFunstatement · cited by 138
Measurable.fun_compproof · cited by 95
measurable_pi_applyproof · cited by 77
MeasureTheory.Measure.map_mapproof · cited by 67
MeasureTheory.Measure.infinitePistatement and proof · cited by 48
ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_mapproof · cited by 5
MeasureTheory.Measure.infinitePi_map_evalproof · cited by 4

Cited by3

Results whose statement or proof uses this declaration.

ProbabilityTheory.iIndepFun_uncurry_infinitePiproof · cited by 1
MeasureTheory.Measure.map_infinitePi_infinitePi_of_injproof · cited by 0
MeasureTheory.Measure.infinitePi_map_eval_prodproof · cited by 0