indepFun_prod_range_succ₀ — Mathlib

English

Under iIndepFun, if the product over j in a finite set s of f_j is independent of f_i whenever i ∉ s, then IndepFun (∏ j∈s f_j) (f_i) κ μ.

Русский

При условии iIndepFun, если произведение по j в конечном множестве s функций f_j независимо от f_i при i ∉ s, то IndepFun (∏_{j∈s} f_j) (f_i) κ μ.

LaTeX

$$$\\text{IndepFun}\\left(\\prod_{j\\in s} f_j\\right)\\left(f_i\\right)\\kappa\\mu$$$

Lean4

@[to_additive]
theorem indepFun_prod_range_succ₀ {f : ℕ → Ω → β} (hf_Indep : iIndepFun f κ μ)
    (hf_meas : ∀ i, AEMeasurable (f i) (κ ∘ₘ μ)) (n : ℕ) : IndepFun (∏ j ∈ Finset.range n, f j) (f n) κ μ :=
  hf_Indep.indepFun_finset_prod_of_notMem₀ hf_meas Finset.notMem_range_self

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