Theorems · Definition · probability

ProbabilityTheory.iCondIndepFun

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

A family of functions defined on the same space Ω and taking values in possibly different spaces, each with a measurable space structure, is conditionally independent if the family of measurable space structures they generate on Ω is conditionally independent. For a function g with codomain having measurable space structure m, the generated measurable space structure is m.comap g. See ProbabilityTheory.iCondIndepFun_iff.

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

28 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasurableSpaceMeasureTheory.IsFiniteMeasure