Theorems · Definition · probability

ProbabilityTheory.Indep

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

Two measurable space structures (or σ-algebras) m₁, m₂ are independent with respect to a measure μ (defined on a third σ-algebra) if for any sets t₁ ∈ m₁, t₂ ∈ m₂, μ (t₁ ∩ t₂) = μ (t₁) * μ (t₂)

Defined in

Mathlib.Probability.Independence.Basic

Cited by

43 results in Mathlib

Foundations

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