English
Two random variables f and g are conditionally independent with respect to m' iff the joint distribution of f and g given m' factors as the product of their conditionals.
Русский
Две величины f и g условно независимы относительно m', если совместное распределение f и g при условии m' разлагается на произведение их условных распределений.
LaTeX
$$$\\mathrm{CondIndepFun}(m',hm',f,g,\\mu) \\iff \\text{joint condDistrib} = \\text{prod of conditionals}$$$
Lean4
/-- Two random variables `f, g` are conditionally independent given a third `k` iff the
joint distribution of `k, f, g` factors into a product of their conditional distributions
given `k`. -/
theorem condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib {γ : Type*} {mγ : MeasurableSpace γ}
{mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [StandardBorelSpace β] [Nonempty β] [StandardBorelSpace β']
[Nonempty β'] (hf : Measurable f) (hg : Measurable g) {k : Ω → γ} (hk : Measurable k) :
CondIndepFun _ hk.comap_le f g μ ↔
μ.map (fun ω ↦ (k ω, f ω, g ω)) = (Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ μ.map k :=
by
rw [condIndepFun_iff_map_prod_eq_prod_comp_trim hf hg]
simp_rw [Measure.ext_prod₃_iff]
have hk_meas {s : Set γ} (hs : MeasurableSet s) : MeasurableSet[mγ.comap k] (k ⁻¹' s) := ⟨s, hs, rfl⟩
have h_left {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t)
(hu : MeasurableSet u) :
(μ.map (fun ω ↦ (k ω, f ω, g ω))) (s ×ˢ t ×ˢ u) =
(@Measure.map _ _ _ ((mγ.comap k).prod inferInstance) (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u) :=
by
rw [Measure.map_apply (by fun_prop) (hs.prod (ht.prod hu)), Measure.map_apply _ ((hk_meas hs).prod (ht.prod hu))]
· simp [Set.mk_preimage_prod]
· exact (measurable_id.mono le_rfl hk.comap_le).prodMk (by fun_prop)
have h_right {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t)
(hu : MeasurableSet u) :
((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ μ.map k) (s ×ˢ t ×ˢ u) =
((Kernel.id ×ₖ ((condExpKernel μ (mγ.comap k)).map f ×ₖ (condExpKernel μ (mγ.comap k)).map g)) ∘ₘ
μ.trim hk.comap_le)
((k ⁻¹' s) ×ˢ t ×ˢ u) :=
by
rw [Measure.bind_apply ((hk_meas hs).prod (ht.prod hu)) (by fun_prop),
Measure.bind_apply (hs.prod (ht.prod hu)) (by fun_prop), lintegral_map ?_ (by fun_prop), lintegral_trim]
rotate_left
· exact Kernel.measurable_coe _ ((hk_meas hs).prod (ht.prod hu))
· exact Kernel.measurable_coe _ (hs.prod (ht.prod hu))
refine lintegral_congr_ae ?_
filter_upwards [condDistrib_apply_ae_eq_condExpKernel_map hf hk ht,
condDistrib_apply_ae_eq_condExpKernel_map hg hk hu] with a haX haT
simp only [Kernel.prod_apply_prod, Kernel.id_apply, Measure.dirac_apply' _ hs]
rw [@Measure.dirac_apply' _ (mγ.comap k) _ _ (hk_meas hs)]
congr
refine ⟨fun h s t u hs ht hu ↦ ?_, fun h ↦ ?_⟩
· convert h (hk_meas hs) ht hu
· exact h_left hs ht hu
· exact h_right hs ht hu
· rintro - t u ⟨s, hs, rfl⟩ ht hu
convert h hs ht hu
· exact (h_left hs ht hu).symm
· exact (h_right hs ht hu).symm
