English
Let (f i)_{i∈I} be a family of random variables on Ω with joint independence, and assume each f i is measurable. Then for all i, j, k with i ≠ j and i ≠ k, the variable f i is independent of the quotient f j / f k.
Русский
Пусть (f_i) — семейство случайных величин на Ω с попарной независимостью и предположено, что каждая f_i измерима. Тогда для любых i, j, k c i ≠ j и i ≠ k, случайная величина f_i независима от отношения f_j / f_k.
LaTeX
$$$\\forall i,j,k,\\ i \\neq j \\land i \\neq k \\;\\Rightarrow\\; IndepFun(f_i, f_j / f_k)\\,\\mu,$\n при условии $iIndepFun(f,\\mu)$ и $\\forall i,\\ Measurable(f_i)$.$$
Lean4
@[to_additive]
theorem indepFun_div_right (hf_indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i)) (i j k : ι) (hij : i ≠ j)
(hik : i ≠ k) : IndepFun (f i) (f j / f k) μ :=
Kernel.iIndepFun.indepFun_div_right hf_indep hf_meas i j k hij hik
