indepFun_mul_left — Mathlib

English

If a family {f_i} is conditionally independent (iCondIndepFun), then the product f_i * f_j is conditionally independent from f_k for distinct i,j,k.

Русский

Если семейство {f_i} условно независимо, то произведение f_i f_j независимо от f_k при различии индексов.

LaTeX

$$$\operatorname{indepFun}_\text{mul}_\text{left} \; (hf_{Indep}) \Rightarrow \operatorname{CondIndepFun} \; m' \; hm' \; (f_i * f_j) \; f_k \; μ$$$

Lean4

@[to_additive]
theorem indepFun_mul_left (hf_indep : iCondIndepFun m' hm' f μ) (hf_meas : ∀ i, Measurable (f i)) (i j k : ι)
    (hik : i ≠ k) (hjk : j ≠ k) : CondIndepFun m' hm' (f i * f j) (f k) μ :=
  Kernel.iIndepFun.indepFun_mul_left hf_indep hf_meas i j k hik hjk

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