indep_generateFrom_le_nat — Mathlib

English

As above for singleton case: independence iff product measure equality for the singleton sigma-algebras.

Русский

Как выше в случае с синглтоном: независимость эквивалентна равенству произведения мер для сигма-алгебр-синглтонов.

LaTeX

$$IndepSets({s}, {t}; μ) ↔ μ(s ∩ t) = μ(s) μ(t)$$

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}) μ :=
  Kernel.iIndepSet.indep_generateFrom_le_nat hsm hs n

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