Theorems · Theorem · probability

ProbabilityTheory.condIndepFun_iff_condIndep

∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  {β : Type u_3} {γ : Type u_4} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ)
  (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndepFun m' hm' f g μ ↔
    ProbabilityTheory.CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ

Defined in

Mathlib.Probability.Independence.Conditional

Cited by

1 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceMeasurableSpaceMeasurableSpaceMeasureTheory.IsFiniteMeasure