indepFun_mul_mul₀ — Mathlib

English

Independence is preserved under division on the left: if f_i and f_j are independent of f_k, then f_i / f_j is independent of f_k.

Русский

Независимость сохраняется при делении слева: если f_i и f_j независимы от f_k, то f_i / f_j независимы от f_k.

LaTeX

$$$\IndepFun (f_i / f_j) (f_k) κ μ$$$

Lean4

@[to_additive]
theorem indepFun_mul_mul₀ (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) κ μ :=
  (hf_indep.indepFun_prodMk_prodMk₀ hf_meas i j k l hik hil hjk hjl).comp measurable_mul measurable_mul

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