Theorems · Theorem · probability

ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight

∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'} {γ : Type u_5}
  {mγ : MeasurableSpace γ} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [inst_2 : StandardBorelSpace β]
  [inst_3 : Nonempty β] [StandardBorelSpace β'] [Nonempty β'],
  Measurable f →
    Measurable g →
      ∀ {k : Ω → γ} (hk : Measurable k),
        ProbabilityTheory.CondIndepFun (MeasurableSpace.comap k inferInstance) ⋯ g f μ ↔
          ⇑(ProbabilityTheory.condDistrib f (fun ω => (k ω, g ω))
                μ) =ᵐ[MeasureTheory.Measure.map (fun ω => (k ω, g ω)) μ]
            ⇑(ProbabilityTheory.Kernel.prodMkRight β' (ProbabilityTheory.condDistrib f k μ))

Two random variables f, g are conditionally independent given a third k iff the conditional distribution of f given k and g is equal to the conditional distribution of f given k.

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

0 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasureStandardBorelSpaceNonemptyStandardBorelSpaceNonempty