Theorems · Theorem · probability

ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib

∀ {Ω : 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 β] [inst_4 : StandardBorelSpace β'] [inst_5 : Nonempty β'],
  Measurable f →
    Measurable g →
      ∀ {k : Ω → γ} (hk : Measurable k),
        ProbabilityTheory.CondIndepFun (MeasurableSpace.comap k inferInstance) ⋯ f g μ ↔
          MeasureTheory.Measure.map (fun ω => (k ω, f ω, g ω)) μ =
            (MeasureTheory.Measure.map k μ).bind
              ⇑(ProbabilityTheory.Kernel.id.prod
                  ((ProbabilityTheory.condDistrib f k μ).prod (ProbabilityTheory.condDistrib g k μ)))

Two random variables f, g are conditionally independent given a third k iff the joint distribution of k, f, g factors into a product of their conditional distributions given k.

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

1 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasureTheory.IsFiniteMeasureStandardBorelSpaceNonemptyStandardBorelSpaceNonempty