indep_generateFrom_le_nat — Mathlib

English

For every natural number n, the sigma-algebra generated by s_{n+1} is independent of the sigma-algebra generated by all s_k with k ≤ n, under the same independence assumptions as above.

Русский

Для каждого натурального числа n алгебра сигм, порожденная s_{n+1}, независима от алгебры сигм, порожденной всеми s_k, с k ≤ n, при тех же предположениях независимости.

LaTeX

$$$Indep\left(\sigma(\{s_{n+1}\}), \sigma\left(\{t \mid \exists k \le n,\ s_k = t\}\right)\right)\ κ\ μ$$$

Lean4

theorem indep_generateFrom_le_nat {s : ℕ → Set Ω} (hsm : ∀ n, MeasurableSet (s n)) (hs : iIndepSet s κ μ) (n : ℕ) :
    Indep (generateFrom {s (n + 1)}) (generateFrom {t | ∃ k ≤ n, s k = t}) κ μ :=
  iIndepSet.indep_generateFrom_le hsm hs _ n.lt_succ_self

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