Theorems · Theorem · probability

ProbabilityTheory.condIndepSets_iff

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

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

2 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure