English
Conditional independence of f and g is equivalent to a product form of their conditional distributions as above, expressed via kernels and trimmed measures.
Русский
Условная независимость f и g эквивалентна произведению условных распределений через ядра и усечённые меры, как выше.
LaTeX
$$$\\mathrm{CondIndepFun}(m',hm',f,g,\\mu) \\iff (\\text{kernel equality as above})$$$
Lean4
/-- Two random variables are conditionally independent iff they satisfy the almost sure equality
of conditional expectations `μ⟦f ⁻¹' s ∩ g ⁻¹' t | m'⟧ =ᵐ[μ] μ⟦f ⁻¹' s | m'⟧ * μ⟦g ⁻¹' t | m'⟧`
for all measurable sets `s` and `t` (see `condIndepFun_iff_condExp_inter_preimage_eq_mul`).
Here, this is phrased with Markov kernels associated to the conditional expectations.
For a random variable `f`, `(condExpKernel μ m').map f` is the law of the conditional expectation
of `f` given `m'`: almost surely, `(condExpKernel μ m').map f ω s = μ⟦f ⁻¹' s | m'⟧ ω`. -/
theorem condIndepFun_iff_map_prod_eq_prod_map_map {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
[CountableOrCountablyGenerated Ω (β × β')] (hf : Measurable f) (hg : Measurable g) :
CondIndepFun m' hm' f g μ ↔
(condExpKernel μ m').map (fun ω ↦ (f ω, g ω)) =ᵐ[μ.trim hm']
(condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g :=
by rw [condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg, ← Kernel.compProd_eq_iff]
