Theorems · Theorem · probability

ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map

∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : Fintype ι]
  {β : ι → Type u_11} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i}
  [MeasureTheory.IsProbabilityMeasure μ],
  (∀ (i : ι), AEMeasurable (f i) μ) →
    (ProbabilityTheory.iIndepFun f μ ↔
      MeasureTheory.Measure.map (fun ω i => f i ω) μ =
        MeasureTheory.Measure.pi fun i => MeasureTheory.Measure.map (f i) μ)

Defined in

Mathlib.Probability.Independence.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

FintypeMeasureTheory.IsProbabilityMeasure