English
Given a measurable X: Ω → β and integrable f: Ω → F, the function (x, ω) ↦ f(ω) composed with the map (X ω, ω) is integrable with respect to μ.map ω ↦ (X ω, ω).
Русский
Для измеримой X: Ω → β и интегрируемого f: Ω → F функция (x, ω) ↦ f(ω) по отображению (X ω, ω) интегрируема по μ.map ω ↦ (X ω, ω).
LaTeX
$$$$ \\operatorname{Integrable} (f\\circ \\text{snd}) (\\mu\\mapsto (\\omega \\mapsto (X\\omega,\\omega))). $$$$
Lean4
/-- The conditional expectation of `Y` given `X` is almost everywhere equal to the integral
`∫ y, y ∂(condDistrib Y X μ (X a))`. -/
theorem condExp_ae_eq_integral_condDistrib' {Ω} [NormedAddCommGroup Ω] [NormedSpace ℝ Ω] [CompleteSpace Ω]
[MeasurableSpace Ω] [BorelSpace Ω] [SecondCountableTopology Ω] {Y : α → Ω} (hX : Measurable X)
(hY_int : Integrable Y μ) : μ[Y|mβ.comap X] =ᵐ[μ] fun a => ∫ y, y ∂condDistrib Y X μ (X a) :=
condExp_ae_eq_integral_condDistrib hX hY_int.1.aemeasurable stronglyMeasurable_id hY_int
