Theorems · Definition · probability

ProbabilityTheory.iCondIndepSets

{Ω : Type u_1} →
  {ι : Type u_2} →
    (m' : MeasurableSpace Ω) →
      {mΩ : MeasurableSpace Ω} →
        [StandardBorelSpace Ω] →
          m' ≤ mΩ →
            (ι → Set (Set Ω)) →
              (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.iCondIndepSets._auto_1) →
                [MeasureTheory.IsFiniteMeasure μ] → Prop

A family of sets of sets π : ι → Set (Set Ω) is conditionally independent given m' with respect to a measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ π i_1, ..., f i_n ∈ π i_n, then μ⟦⋂ i in s, f i | m'⟧ =ᵐ[μ] ∏ i ∈ s, μ⟦f i | m'⟧. See ProbabilityTheory.iCondIndepSets_iff. It will be used for families of π-systems.

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

9 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure