condIndep_iSup_of_monotone — Mathlib

English

For s: Nat → Set Ω with measurable s_n, and iCondIndepSet m' hm' s μ, we have CondIndep m' (generateFrom {s (n+1)}) (generateFrom {t | ∃ k ≤ n, s k = t}) hm' μ for every n.

Русский

Для последовательности s_n измеримых, если iCondIndepSet выполняется, то CondIndep между generateFrom {s_{n+1}} и generateFrom {t | ∃ k ≤ n, s_k = t} держится.

LaTeX

$$$\mathrm{CondIndep}\bigl(m', \operatorname{generateFrom}\{s(n+1)\}, \operatorname{generateFrom}\{t \mid \exists k \le n, s_k = t\}, hm', \mu\bigr)$$$

Lean4

theorem condIndep_iSup_of_monotone [SemilatticeSup ι] {m : ι → MeasurableSpace Ω}
    (h_indep : ∀ i, CondIndep m' (m i) m₁ hm' μ) (h_le : ∀ i, m i ≤ mΩ) (h_le' : m₁ ≤ mΩ) (hm : Monotone m) :
    CondIndep m' (⨆ i, m i) m₁ hm' μ :=
  Kernel.indep_iSup_of_monotone h_indep h_le h_le' hm

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