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