indep_iSup_of_antitone — Mathlib

English

If a family of sigma-algebras (m_i) is decreasing (antitone) and each m_i is independent of a fixed m' with respect to κ μ, then the supremum of the m_i is independent of m'.

Русский

Если семейство сигма-алгебр (m_i) убывающее и каждая m_i независима от фиксированной m' относительно κ и μ, то их объединение независимо от m'.

LaTeX

$$$Indep\left(\bigvee_i m_i\right) m'\ κ\ μ$$$

Lean4

theorem indep_iSup_of_antitone [SemilatticeInf ι] {Ω} {m : ι → MeasurableSpace Ω} {m' m0 : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} [IsZeroOrMarkovKernel κ] (h_indep : ∀ i, Indep (m i) m' κ μ) (h_le : ∀ i, m i ≤ m0)
    (h_le' : m' ≤ m0) (hm : Antitone m) : Indep (⨆ i, m i) m' κ μ :=
  indep_iSup_of_directed_le h_indep h_le h_le' hm.directed_le

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