Theorems · Theorem · probability

ProbabilityTheory.iCondIndepSets_singleton_iff

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