Theorems · Definition · probability

ProbabilityTheory.CondIndepFun

{Ω : Type u_1} →
  (m' : MeasurableSpace Ω) →
    {mΩ : MeasurableSpace Ω} →
      [StandardBorelSpace Ω] →
        m' ≤ mΩ →
          {β : Type u_3} →
            {γ : Type u_4} →
              [MeasurableSpace β] →
                [MeasurableSpace γ] →
                  (Ω → β) →
                    (Ω → γ) →
                      (μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.CondIndepFun._auto_1) →
                        [MeasureTheory.IsFiniteMeasure μ] → Prop

Two functions are conditionally independent if the two measurable space structures they generate are conditionally independent. For a function f with codomain having measurable space structure m, the generated measurable space structure is m.comap f. See ProbabilityTheory.condIndepFun_iff. We use the notation X ⟂ᵢ[Z, hZ; μ] Y to write that X and Y are conditionally independent given (the σ-algebra generated by) Z (scoped in ProbabilityTheory).

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

41 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasurableSpaceMeasurableSpaceMeasureTheory.IsFiniteMeasure