indepFun_mul_left₀ — Mathlib

English

Under AE-measurability, independence of two variables lifts to independence of their product with two other variables.

Русский

При AE-измеримости независимость пары переменных сохраняется при умножении на две другие переменные.

LaTeX

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

Lean4

@[to_additive]
theorem indepFun_mul_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) κ μ :=
  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

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