indepFun_div_left₀ — Mathlib

English

If iIndepFun f μ and AE-measurability holds for all f i, then for i ≠ k and j, the independence holds for f_i / f_j with f_k in AE sense.

Русский

Если iIndepFun f μ и AE-измеримость для всех f_i, то независимость f_i / f_j от f_k сохраняется в AE-смысле при i ≠ k.

LaTeX

$$$ \\operatorname{iIndepFun} f μ \\rightarrow \\forall i, AEMeasurable (f i) μ \\rightarrow \\forall i j k, i \\neq k \\rightarrow j \\neq k \\rightarrow \\operatorname{IndepFun} (instHDiv.hDiv (f i) (f j)) (f k) μ$$$

Lean4

@[to_additive]
theorem indepFun_div_left₀ (hf_indep : iIndepFun f μ) (hf_meas : ∀ i, AEMeasurable (f i) μ) (i j k : ι) (hik : i ≠ k)
    (hjk : j ≠ k) : IndepFun (f i / f j) (f k) μ :=
  Kernel.iIndepFun.indepFun_div_left₀ hf_indep (by simp [hf_meas]) i j k hik hjk

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