Theorems · Definition · probability

ProbabilityTheory.iCondIndep

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

A family of measurable space structures (i.e. of σ-algebras) is conditionally independent given m' with respect to a measure μ (typically defined on a finer σ-algebra) if the family of sets of measurable sets they define is independent. m : ι → MeasurableSpace Ω is conditionally independent given m' with respect to measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ m i_1, ..., f i_n ∈ m i_n, then μ⟦⋂ i in s, f i | m'⟧ =ᵐ[μ] ∏ i ∈ s, μ⟦f i | m'⟧ . See ProbabilityTheory.iCondIndep_iff.

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

19 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasure