indepFun_prodMk₀ — Mathlib

English

If X_i are independent random variables on Ω_i with product measure, then the combined family (X_i) is independent on the product space.

Русский

Если X_i независимы на пространствах Ω_i с произведением мер, то совокупность (X_i) независима на произведенном пространстве.

LaTeX

$$IndepFun X μ → IndepFun Prod X μ$$

Lean4

theorem indepFun_prodMk₀ (hf_Indep : iIndepFun f μ) (hf_meas : ∀ i, AEMeasurable (f i) μ) (i j k : ι) (hik : i ≠ k)
    (hjk : j ≠ k) : IndepFun (fun a => (f i a, f j a)) (f k) μ :=
  Kernel.iIndepFun.indepFun_prodMk₀ hf_Indep (by simp [hf_meas]) i j k hik hjk

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