condIndepFun_prodMk — Mathlib

English

If a family {f_i} of random variables is conditionally independent in i, then the pair (f_i, f_j) is independent of f_k as a product-maker selection.

Русский

Если семейство случайных величин {f_i} условно независимо по индексам, то пара (f_i, f_j) независимо от f_k рассматривая их как произведение функций.

LaTeX

$$$\operatorname{CondIndepFun}(m', hm', f, g, μ) \Rightarrow \operatorname{CondIndepFun} \; m' \; hm' \; (f_i)_{i} \; (f_j)_{j} \; μ$$$

Lean4

theorem condIndepFun_prodMk {β : ι → Type*} {m : ∀ i, MeasurableSpace (β i)} {f : ∀ i, Ω → β i}
    (hf_Indep : iCondIndepFun m' hm' f μ) (hf_meas : ∀ i, Measurable (f i)) (i j k : ι) (hik : i ≠ k) (hjk : j ≠ k) :
    CondIndepFun m' hm' (fun a => (f i a, f j a)) (f k) μ :=
  Kernel.iIndepFun.indepFun_prodMk hf_Indep hf_meas i j k hik hjk

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