indepFun_prod_range_succ — Mathlib

English

Let f: ℕ → Ω → β be a family satisfying the iIndepFun condition with κ and μ, and each f_i is measurable. Then for every n ∈ ℕ, the finite product over j = 0,1,...,n−1 of f_j is independent of f_n with respect to κ and μ.

Русский

Пусть f: ℕ → Ω → β удовлетворяет условию независимости iIndepFun, и каждый f_i измерим. Тогда для каждого n ∈ ℕ произведение по j = 0,...,n−1 функций f_j независимо от f_n относительно κ μ.

LaTeX

$$$\\text{IndepFun}\\left(\\prod_{j\\in \\text{range}(n)} f_j\\right)\\left(f_n\\right)\\kappa\\mu$$$

Lean4

@[to_additive]
theorem indepFun_prod_range_succ {f : ℕ → Ω → β} (hf_Indep : iIndepFun f κ μ) (hf_meas : ∀ i, Measurable (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

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