indepFun_mul_right — Mathlib

English

If f is iIndepFun and all f i are measurable, then for i ≠ j and i ≠ k, f_i is independent of f_j · f_k.

Русский

Если iIndepFun f μ и все f_i измеримы, то f_i независим от f_j · f_k при i ≠ j и i ≠ k.

LaTeX

$$$ \\operatorname{iIndepFun} f μ \\rightarrow (\\forall i, Measurable (f i)) \\rightarrow \\forall i j k, i \\neq j \\rightarrow i \\neq k \\rightarrow \\operatorname{IndepFun} (f i) (f j * f k) μ$$$

Lean4

@[to_additive]
theorem indepFun_mul_right (hf_indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (f i)) (i j k : ι) (hij : i ≠ j)
    (hik : i ≠ k) : IndepFun (f i) (f j * f k) μ :=
  Kernel.iIndepFun.indepFun_mul_right hf_indep hf_meas i j k hij hik

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