English
Let f: Ω→β and g: Ω→β' be random variables with measurable f and g. Then CondIndepFun m' hm' f g μ is equivalent to: for all measurable sets s⊆β and t⊆β', the preimages f⁻¹(s) and g⁻¹(t) are conditionally independent given m' with respect to μ.
Русский
Пусть f: Ω→β и g: Ω→β' — случайные величины, удовлетворяющие условию измеримости. Тогда CondIndepFun m' hm' f g μ эквивалентно тому, что для всех измеримых множеств s⊆β и t⊆β' предобраза f⁻¹(s) и g⁻¹(t) условно независимы относительно m' по отношению к μ.
LaTeX
$$$\operatorname{CondIndepFun}(m', hm', f, g; \mu) \iff \forall s,t,\ \operatorname{MeasurableSet}_m(s) \land \operatorname{MeasurableSet}_{m'}(t) \Rightarrow \operatorname{CondIndepSet}(m' hm' (f^{-1}(s)) (g^{-1}(t)) \mu$$
Lean4
theorem condIndepFun_iff_condExp_inter_preimage_eq_mul {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
(hf : Measurable f) (hg : Measurable g) :
CondIndepFun m' hm' f g μ ↔
∀ s t,
MeasurableSet s →
MeasurableSet t → (μ⟦f ⁻¹' s ∩ g ⁻¹' t|m'⟧) =ᵐ[μ] fun ω ↦ (μ⟦f ⁻¹' s|m'⟧) ω * (μ⟦g ⁻¹' t|m'⟧) ω :=
by
rw [condIndepFun_iff _ _ _ _ hf hg]
refine ⟨fun h s t hs ht ↦ ?_, fun h s t ↦ ?_⟩
· exact h (f ⁻¹' s) (g ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩
· rintro ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩
exact h s t hs ht
