indepFun_div_right — Mathlib

English

If {f_i} is CondIndepFun and each f_i is measurable, then for i, j, k with i ≠ j and i ≠ k, the pair f_i and (f_j / f_k) are independent.

Русский

Если {f_i} образуют CondIndepFun и каждая f_i измерима, то для i, j, k с i ≠ j и i ≠ k пары f_i и (f_j / f_k) независимы.

LaTeX

$$$\forall i,j,k,\; i \neq j \land i \neq k \Rightarrow\; \text{CondIndepFun } m' hm' (f_i) \; (f_j / f_k) \; μ.$$$

Lean4

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

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