iCondIndepFun_iff_iCondIndep — Mathlib

English

iCondIndepFun_iff_iCondIndep: independence of a family of random mappings f,g is equivalent to independence after applying comaps to their codomains.

Русский

Независимость семейства отображений в условном смысле равна независимости после приложения компаков к их кодомандам.

LaTeX

$$$iCondIndepFun(m', hm', f, g, μ) \\iff iCondIndep(m', hm', (\\lambda x. \\mathrm{MeasurableSpace.comap}(f x) (m x)), μ)$$$

Lean4

theorem iCondIndepFun_iff_iCondIndep {β : ι → Type*} (m : ∀ x : ι, MeasurableSpace (β x)) (f : ∀ x : ι, Ω → β x)
    (μ : Measure Ω) [IsFiniteMeasure μ] :
    iCondIndepFun m' hm' f μ ↔ iCondIndep m' hm' (fun x ↦ MeasurableSpace.comap (f x) (m x)) μ := by
  simp only [iCondIndepFun, iCondIndep, Kernel.iIndepFun]

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