indepFun_mul_left — Mathlib

English

If f_i and f_j are independent of f_k, then the product f_i * f_j is independent of f_k, provided measurability holds for the factors.

Русский

Если f_i и f_j независимы от f_k, то произведение f_i f_j независимо от f_k при соблюдении измеримости факторов.

LaTeX

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

Lean4

@[to_additive]
theorem indepFun_mul_left (hf_indep : iIndepFun f κ μ) (hf_meas : ∀ i, Measurable (f i)) (i j k : ι) (hik : i ≠ k)
    (hjk : j ≠ k) : IndepFun (f i * f j) (f k) κ μ :=
  by
  have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ := hf_indep.indepFun_prodMk hf_meas i j k hik hjk
  simpa using this.comp (measurable_fst.mul measurable_snd) measurable_id

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