English
If (f_i) is iIndepFun μ and each f_i is AEMeasurable, then for i,j,k,l with i ≠ k, i ≠ l, j ≠ k, j ≠ l, the independence relation holds for f_i / f_j and f_k / f_l.
Русский
Если (f_i) является iIndepFun μ и каждая f_i - AEMeasurable, тогда для i,j,k,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, AEMeasurable (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 (by simp [hf_meas]) i j k l hik hil hjk hjl
