indepFun_div_right₀ — Mathlib

English

If the family (f_i) is iIndepFun μ and each f_i is AEMeasurable, then for all distinct i, j, k, f_i is independent of f_j / f_k.

Русский

Если семейство (f_i) является iIndepFun μ и каждый f_i является AEMeasurable, то для любых различных i, j, 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,\\ AEMeasurable(f_i,\\mu)$.$$

Lean4

@[to_additive]
theorem indepFun_div_right₀ (hf_indep : iIndepFun f μ) (hf_meas : ∀ i, AEMeasurable (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 (by simp [hf_meas]) i j k hij hik

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