indepFun_div_div — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem indepFun_div_div (hf_indep : iCondIndepFun m' hm' f μ) (hf_meas : ∀ i, Measurable (f i)) (i j k l : ι)
    (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : CondIndepFun m' hm' (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

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