Theorems · Theorem · probability

ProbabilityTheory.iIndepFun_iff_hasLaw_pi_pi

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {ι : Type u_3} [inst : Fintype ι] {𝓧 : ι → Type u_4} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)}
  {μ : (i : ι) → MeasureTheory.Measure (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i},
  (∀ (i : ι), ProbabilityTheory.HasLaw (X i) (μ i) P) →
    (ProbabilityTheory.iIndepFun X P ↔ ProbabilityTheory.HasLaw (fun ω i => X i ω) (MeasureTheory.Measure.pi μ) P)

Defined in

Mathlib.Probability.HasLaw

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasureFintype