Theorems · Definition · probability

ProbabilityTheory.CondIndepSet

{Ω : Type u_1} →
  (m' : MeasurableSpace Ω) →
    {mΩ : MeasurableSpace Ω} →
      [StandardBorelSpace Ω] →
        m' ≤ mΩ →
          Set Ω →
            Set Ω →
              (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.CondIndepSet._auto_1) →
                [MeasureTheory.IsFiniteMeasure μ] → Prop

Two sets are conditionally independent if the two measurable space structures they generate are conditionally independent. For a set s, the generated measurable space structure has measurable sets ∅, s, sᶜ, univ. See ProbabilityTheory.condIndepSet_iff.

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

11 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure