English
For measurable X, AEMeasurable Y and measurable sets s, t, the left-hand side lintegral over X⁻¹'t of condDistrib(Y,X,μ)(X a) restricted to s equals the right-hand side measure of t ∩ Y⁻¹' s.
Русский
Для измеримых X, AE-измеримой Y и измеримых множеств s, t выполняется равенство интегралов по preimage и условному распределению condDistrib.
LaTeX
$$$\\int^{-}_{a \\in X^{-1} t} condDistrib(Y,X,μ)(X a)(s) \\, dμ(a) = μ(X^{-1} t \\cap Y^{-1} s).$$$
Lean4
theorem setLIntegral_preimage_condDistrib (hX : Measurable X) (hY : AEMeasurable Y μ) (hs : MeasurableSet s)
(ht : MeasurableSet t) : ∫⁻ a in X ⁻¹' t, condDistrib Y X μ (X a) s ∂μ = μ (X ⁻¹' t ∩ Y ⁻¹' s) := by
rw [← lintegral_map (Kernel.measurable_coe _ hs) hX, condDistrib, ← Measure.restrict_map hX ht, ←
Measure.fst_map_prodMk₀ hY, Measure.setLIntegral_condKernel_eq_measure_prod ht hs,
Measure.map_apply_of_aemeasurable (hX.aemeasurable.prodMk hY) (ht.prod hs), mk_preimage_prod]
