iCondIndepFun_indicator — Mathlib

English

If a family of sets is conditionally independent, then the corresponding indicator-valued random variables are also conditionally independent.

Русский

Если множество семейство условно независимо, то соответствующие индикаторные случайные величины также условно независимы.

LaTeX

$$$\text{hs : iCondIndepSet } m' hm' s μ \Rightarrow\; \text{ICondIndepFun indicator of } s μ.$$$

Lean4

theorem iCondIndepFun_indicator [Zero β] [One β] {m : MeasurableSpace β} {s : ι → Set Ω}
    (hs : iCondIndepSet m' hm' s μ) : iCondIndepFun m' hm' (fun n => (s n).indicator fun _ω => (1 : β)) μ :=
  Kernel.iIndepSet.iIndepFun_indicator hs

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