English
condIndepFun_iff_condIndep: with measurable f,g, CondIndepFun is equivalent to CondIndep after applying comaps to codomains.
Русский
при измеримых f,g условная независимость эквивалентна независимости после применения компаков к кодомонам.
LaTeX
$$$CondIndepFun(m', hm', f, g, μ) \\iff CondIndep(m', MeasurableSpace.comap f mβ, MeasurableSpace.comap g mγ, hm', μ)$$$
Lean4
theorem condIndepFun_iff {β γ : Type*} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ)
(hf : Measurable f) (hg : Measurable g) (μ : Measure Ω) [IsFiniteMeasure μ] :
CondIndepFun m' hm' f g μ ↔
∀ t1 t2,
MeasurableSet[MeasurableSpace.comap f mβ] t1 →
MeasurableSet[MeasurableSpace.comap g mγ] t2 → (μ⟦t1 ∩ t2|m'⟧) =ᵐ[μ] (μ⟦t1|m'⟧) * (μ⟦t2|m'⟧) :=
by rw [condIndepFun_iff_condIndep, condIndep_iff _ _ _ _ hf.comap_le hg.comap_le]
