English
Two random variables f and g are conditionally independent given m' if the joint distribution of (f,g) given m' equals the product of their marginal conditional distributions. This can be characterized via Markov kernels and conditional expectations.
Русский
Две случайные величины f и g условно независимы относительно m', если совместное распределение (f,g) при условии m' равно произведению маргинальных условных распределений. Это выражается через марковские ядра и условные ожидания.
LaTeX
$$$\\mathrm{CondIndepFun}(m',hm',f,g,\\mu)$$$
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, and the
almost sure equality is expressed as equality of the composition-product with the measure, which is
equivalent to a.e. equality. See `condIndepFun_iff_map_prod_eq_prod_map_map` for the a.e. equality
version with kernels.
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_compProd_map_prod_eq_compProd_prod_map_map {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
(hf : Measurable f) (hg : Measurable g) :
CondIndepFun m' hm' f g μ ↔
(μ.trim hm') ⊗ₘ (condExpKernel μ m').map (fun ω ↦ (f ω, g ω)) =
(μ.trim hm') ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g) :=
Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg
