iCondIndepFun_iff — Mathlib

English

iCondIndepFun_iff_iCondIndep: equivalence of independence for functions f,g via comaps of measure spaces.

Русский

Эквивалентость независимости при функциях f,g через компаки сигма-алгебр.

LaTeX

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

Lean4

theorem iCondIndepFun_iff {β : ι → Type*} (m : ∀ x : ι, MeasurableSpace (β x)) (f : ∀ x : ι, Ω → β x)
    (hf : ∀ i, Measurable (f i)) (μ : Measure Ω) [IsFiniteMeasure μ] :
    iCondIndepFun m' hm' f μ ↔
      ∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i, i ∈ s → MeasurableSet[(m i).comap (f i)] (g i)),
        μ⟦⋂ i ∈ s, g i|m'⟧ =ᵐ[μ] ∏ i ∈ s, (μ⟦g i|m'⟧) :=
  by
  simp only [iCondIndepFun_iff_iCondIndep]
  rw [iCondIndep_iff]
  exact fun i ↦ (hf i).comap_le

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