indepFun_prodMk — Mathlib

English

If f is iIndepFun and each f i is measurable, then for indices i,j,k with i ≠ k and j ≠ k, the independence holds between the pair (f i, f j) and f k.

Русский

Если f образует i-независимую совокупность и каждый f_i измерим, то для i,j,k с i≠k, j≠k независимость между парой (f_i,f_j) и f_k.

LaTeX

$$$ \\operatorname{iIndepFun} f μ \\rightarrow \\bigl(\\forall i, \\Measurable (f i)\\bigr) \\rightarrow \\forall i j k, i \\neq k \\rightarrow j \\neq k \\rightarrow \\operatorname{IndepFun} (\\lambda a \\mapsto (f i a, f j a)) (f k) μ$$$

Lean4

theorem indepFun_prodMk (hf_Indep : iIndepFun f μ) (hf_meas : ∀ i, Measurable (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 hf_meas i j k hik hjk

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