Theorems · Definition · probability

ProbabilityTheory.IndepSets

{Ω : Type u_1} →
  {_mΩ : MeasurableSpace Ω} →
    Set (Set Ω) → Set (Set Ω) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IndepSets._auto_1 → Prop

Two sets of sets s₁, s₂ are independent with respect to a measure μ if for any sets t₁ ∈ p₁, t₂ ∈ s₂, then μ (t₁ ∩ t₂) = μ (t₁) * μ (t₂)

Defined in

Mathlib.Probability.Independence.Basic

Cited by

29 results in Mathlib

Foundations

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