Theorems · Theorem · probability

ProbabilityTheory.iCondIndep_iff

∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (m : ι → MeasurableSpace Ω),
  (∀ (i : ι), m i ≤ mΩ) →
    ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
      ProbabilityTheory.iCondIndep m' hm' m μ ↔
        ∀ (s : Finset ι) {f : ι → Set Ω},
          (∀ i ∈ s, MeasurableSet (f i)) →
            μ[(⋂ i ∈ s, f i).indicator fun ω => 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).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