English
The conditional expectation of f on the product (X, Y) equals almost surely the integral over y of f(X, y) with respect to condDistrib Y X μ at X a.
Русский
Условное ожидание от f на произведении (X, Y) равно почти наверное интегралу по y от f(X, y) against condDistrib Y X μ в X a.
LaTeX
$$$$ \\mu[ f(X a, Y a) \\mid X] =^{{a.e.}} \\int_y f(X a, y) \\; d(\\operatorname{condDistrib} Y X μ)(y). $$$$
Lean4
/-- The conditional expectation of a function `f` of the product `(X, Y)` is almost everywhere equal
to the integral of `y ↦ f(X, y)` against the `condDistrib` kernel. -/
theorem condExp_prod_ae_eq_integral_condDistrib₀ [NormedSpace ℝ F] [CompleteSpace F] (hX : Measurable X)
(hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a)))
(hf_int : Integrable (fun a => f (X a, Y a)) μ) :
μ[fun a => f (X a, Y a)|mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a) :=
haveI hf_int' : Integrable f (μ.map fun a => (X a, Y a)) := by
rwa [integrable_map_measure hf (hX.aemeasurable.prodMk hY)]
condExp_prod_ae_eq_integral_condDistrib' hX hY hf_int'
