English
A variant with a stronger assumption on measurability showing that condExpProd equals integral against condDistrib.
Русский
Вариант с более сильным предположением измеримости: condExpProd равен интегралу против condDistrib.
LaTeX
$$$$ \\text{CondExpProd}'(hX,hY,hf,hf\\_int) $$$$
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 : StronglyMeasurable f) (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.aestronglyMeasurable (hX.aemeasurable.prodMk hY)]
condExp_prod_ae_eq_integral_condDistrib' hX hY hf_int'
