English
If hX is a.a. measurable, and s is a measurable set, then the real-valued integral over condDistrib of s is integrable with respect to μ.
Русский
Если hX а.е. измеримо и s измеримо, то интеграл по condDistrib в области s по реальному значению интегрируем относительно μ.
LaTeX
$$$$ \\text{If } hX \\text{ is a.e. measurable and } s \\text{ is measurable, then } \\int (\\cdot) \\mathrm{real}(condDistrib(Y,X,μ)(X(\\cdot))\\, s) \\in L^1(μ). $$$$
Lean4
theorem integrable_toReal_condDistrib (hX : AEMeasurable X μ) (hs : MeasurableSet s) :
Integrable (fun a => (condDistrib Y X μ (X a)).real s) μ :=
by
refine integrable_toReal_of_lintegral_ne_top ?_ ?_
· exact Measurable.comp_aemeasurable (Kernel.measurable_coe _ hs) hX
· refine ne_of_lt ?_
calc
∫⁻ a, condDistrib Y X μ (X a) s ∂μ ≤ ∫⁻ _, 1 ∂μ := lintegral_mono fun a => prob_le_one
_ = μ univ := lintegral_one
_ < ∞ := measure_lt_top _ _
