condIndepFun_iff_condIndep — Mathlib

English

condIndepFun_iff_condIndep: independence of random variables is equivalent to independence of their comap sigma-algebras.

Русский

независимость случайных величин эквивалентна независимости их сигма-алгебр, порождённых ими.

LaTeX

$$$CondIndepFun(m', hm', f, g, μ) \\iff CondIndep(m', MeasurableSpace.comap f mβ, MeasurableSpace.comap g mγ, hm', μ)$$$

Lean4

theorem condIndepFun_iff_condIndep {β γ : Type*} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ω → β)
    (g : Ω → γ) (μ : Measure Ω) [IsFiniteMeasure μ] :
    CondIndepFun m' hm' f g μ ↔ CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ := by
  simp only [CondIndepFun, CondIndep, Kernel.IndepFun]

Похожие утверждения