Theorems · Theorem · probability

ProbabilityTheory.iIndepFun.hasLaw_infinitePi

∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : ι → Type u_3}
  {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} {μ : (i : ι) → MeasureTheory.Measure (𝓧 i)},
  (∀ (i : ι), ProbabilityTheory.HasLaw (X i) (μ i) P) →
    ProbabilityTheory.iIndepFun X P →
      AEMeasurable (fun ω i => X i ω) P →
        ProbabilityTheory.HasLaw (fun ω i => X i ω) (MeasureTheory.Measure.infinitePi μ) P

Defined in

Mathlib.Probability.Independence.InfinitePi

Cited by

1 results in Mathlib

Foundations

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