English
Two random variables f and g are conditionally independent given k if the joint distribution of (f,g) given k equals the product of their conditional distributions given k.
Русский
Две случайные величины f и g условно независимы при условии k, если совокупное распределение (f,g) при условии k равно произведению их условных распределений при k.
LaTeX
$$$\\mathrm{CondIndepFun}(m',hm',f,g,\\mu) \\iff \\exists\\ k:\\; \\text{joint condDistrib factorization given } k$$$
Lean4
/-- Two random variables are conditionally independent with respect to `m'` iff the law of
`(id, f, g)` under `μ`, in which the identity is to the space with σ-algebra `m'`, can be written
as a product involving the conditional expectations of `f` and `g` given `m'`.
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_comp_trim {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
(hf : Measurable f) (hg : Measurable g) :
CondIndepFun m' hm' f g μ ↔
@Measure.map _ _ _ (m'.prod _) (fun ω ↦ (ω, f ω, g ω)) μ =
(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ∘ₘ μ.trim hm' :=
by
rw [condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg]
congr!
· rw [Measure.compProd_map (by fun_prop), compProd_trim_condExpKernel,
Measure.map_map (by fun_prop) ((measurable_id.mono le_rfl hm').prodMk measurable_id)]
rfl
· rw [Measure.compProd_eq_comp_prod]
