Theorems · Theorem · probability

ProbabilityTheory.condIndep_iff

∀ {Ω : Type u_1} (m' m₁ m₂ : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ),
  m₁ ≤ mΩ →
    m₂ ≤ mΩ →
      ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
        ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ ↔
          ∀ (t1 t2 : Set Ω),
            MeasurableSet t1 →
              MeasurableSet t2 →
                μ[(t1 ∩ t2).indicator fun ω => 1 | m'] =ᵐ[μ]
                  μ[t1.indicator fun ω => 1 | m'] * μ[t2.indicator fun ω => 1 | m']

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

1 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure