Theorems · Definition · probability

ProbabilityTheory.iIndep

{Ω : Type u_1} →
  {ι : Type u_2} →
    (ι → MeasurableSpace Ω) →
      {_mΩ : MeasurableSpace Ω} → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.iIndep._auto_1 → Prop

A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a measure μ (typically defined on a finer σ-algebra) if the family of sets of measurable sets they define is independent. m : ι → MeasurableSpace Ω is independent with respect to measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ m i_1, ..., f i_n ∈ m i_n, then μ (⋂ i in s, f i) = ∏ i ∈ s, μ (f i).

Defined in

Mathlib.Probability.Independence.Basic

Cited by

30 results in Mathlib

Foundations

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