Theorems · Theorem · probability

ProbabilityTheory.iCondIndepSets_iff

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

2 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure