English
Two random variables f and g are conditionally independent given k iff their joint distribution equals the product of their conditionals given k (involving sums, maps, and kernels).
Русский
Две величины f и g условно независимы при условии k, если их совместное распределение равно произведению их условных распределений, выраженных через ядра.
LaTeX
$$$\\mathrm{CondIndepFun}(m',hm',f,g,\\mu) \\iff \\text{map equality with condExpKernel}$$$
Lean4
/-- Two random variables `f, g` are conditionally independent given a third `k` iff the
conditional distribution of `f` given `k` and `g` is equal to the conditional distribution of `f`
given `k`. -/
theorem condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft {γ : Type*} {mγ : MeasurableSpace γ} {mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'} [StandardBorelSpace β] [Nonempty β] [StandardBorelSpace β'] [Nonempty β']
(hf : Measurable f) (hg : Measurable g) {k : Ω → γ} (hk : Measurable k) :
CondIndepFun (mγ.comap k) hk.comap_le g f μ ↔
condDistrib f (fun ω ↦ (k ω, g ω)) μ =ᵐ[μ.map (fun ω ↦ (k ω, g ω))] (condDistrib f k μ).prodMkRight _ :=
by
rw [condDistrib_ae_eq_iff_measure_eq_compProd (μ := μ) _ hf.aemeasurable,
condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib hg hf hk, Measure.compProd_eq_comp_prod]
let e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
have h_eq :
((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k =
(Kernel.id ×ₖ (condDistrib f k μ).prodMkRight _) ∘ₘ μ.map (fun a ↦ (k a, g a)) :=
by
calc
((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k
_ = (Kernel.id ×ₖ (condDistrib f k μ).prodMkRight _) ∘ₘ (μ.map k ⊗ₘ condDistrib g k μ) :=
by
rw [Measure.compProd_eq_comp_prod, Measure.comp_assoc]
congr 2
have h :=
Kernel.prod_prodMkRight_comp_deterministic_prod (condDistrib g k μ) (condDistrib f k μ) Kernel.id
measurable_id
rw [← Kernel.id] at h
simpa using h.symm
_ = (Kernel.id ×ₖ (condDistrib f k μ).prodMkRight _) ∘ₘ μ.map (fun a ↦ (k a, g a)) := by
rw [compProd_map_condDistrib hg.aemeasurable]
rw [← h_eq]
have h1 : μ.map (fun x ↦ ((k x, g x), f x)) = (μ.map (fun a ↦ (k a, g a, f a))).map e :=
by
rw [Measure.map_map (by fun_prop) (by fun_prop)]
rfl
have h1_symm : μ.map (fun a ↦ (k a, g a, f a)) = (μ.map (fun x ↦ ((k x, g x), f x))).map e.symm := by
rw [h1, Measure.map_map (by fun_prop) (by fun_prop), MeasurableEquiv.symm_comp_self, Measure.map_id]
have h2 :
((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k =
((Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ μ.map k).map e :=
by
rw [← Measure.deterministic_comp_eq_map e.measurable, Measure.comp_assoc]
congr 2
unfold e
rw [Kernel.deterministic_comp_eq_map, Kernel.prodAssoc_symm_prod]
have h2_symm :
(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ μ.map k =
(((Kernel.id ×ₖ condDistrib g k μ) ×ₖ condDistrib f k μ) ∘ₘ μ.map k).map e.symm :=
by rw [h2, Measure.map_map (by fun_prop) (by fun_prop), MeasurableEquiv.symm_comp_self, Measure.map_id]
rw [h1, h2]
exact ⟨fun h ↦ by rw [h], fun h ↦ by rw [h1_symm, h1, h2_symm, h2, h]⟩
