English
If the family (f_i) is iIndepFun μ and each f_i is measurable, then for any i, j, k, l with i ≠ k, i ≠ l, j ≠ k, j ≠ l, the two quotients f_i / f_j and f_k / f_l are independent.
Русский
Если семейство (f_i) является iIndepFun μ и каждая f_i измерима, то для любых i, j, k, l с условиями i ≠ k, i ≠ l, j ≠ k, j ≠ l, независимы дроби f_i / f_j и f_k / f_l.
LaTeX
$$$\\forall i,j,k,l,\\ (i \\neq k) \\land (i \\neq l) \\land (j \\neq k) \\land (j \\neq l) \\Rightarrow IndepFun\\Big(\\frac{f_i}{f_j}, \\frac{f_k}{f_l}\\Big)\\,\\mu$$$
Lean4
@[to_additive]
theorem indepFun_div_div (hf_indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i)) (i j k l : ι) (hik : i ≠ k)
(hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : IndepFun (f i / f j) (f k / f l) μ :=
Kernel.iIndepFun.indepFun_div_div hf_indep hf_meas i j k l hik hil hjk hjl
