condIndepFun_prod_range_succ — Mathlib

English

For a sequence f_i, the product of the first n terms is CondIndepFun from f_n, i.e., the product over j in {0,...,n-1} is independent of f_n.

Русский

Для последовательности f_i произведение первых n членов независимо от f_n: prod_{j < n} f_j ⟂ f_n.

LaTeX

$$$\forall n\in\mathbb{N}, \; \text{CondIndepFun } m' hm' (\prod_{j=0}^{n-1} f_j) (f_n) μ.$$$

Lean4

@[to_additive]
theorem condIndepFun_prod_range_succ {f : ℕ → Ω → β} (hf_Indep : iCondIndepFun m' hm' f μ)
    (hf_meas : ∀ i, Measurable (f i)) (n : ℕ) : CondIndepFun m' hm' (∏ j ∈ Finset.range n, f j) (f n) μ :=
  Kernel.iIndepFun.indepFun_prod_range_succ hf_Indep hf_meas n

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