English
For measurable s ⊆ α×β with finite measure, the function x ↦ ν.real( Prod.mk x⁻¹' s ) is integrable with respect to μ.
Русский
Для измеримого множества s ⊆ α×β с конечной мерой функция x ↦ ν.real(Prod.mk x⁻¹' s) интегрируема по μ.
LaTeX
$$$$\\operatorname{Integrable}\\left( x \\mapsto \\nu.real\\left(\\operatorname{Prod.mk} x^{-1} s\\right)\\right)\\mu$$$$
Lean4
theorem integrable_measure_prodMk_left {s : Set (α × β)} (hs : MeasurableSet s) (h2s : (μ.prod ν) s ≠ ∞) :
Integrable (fun x => ν.real (Prod.mk x ⁻¹' s)) μ :=
by
refine ⟨(measurable_measure_prodMk_left hs).ennreal_toReal.aemeasurable.aestronglyMeasurable, ?_⟩
simp_rw [hasFiniteIntegral_iff_enorm, measureReal_def, enorm_eq_ofReal toReal_nonneg]
convert h2s.lt_top using 1
rw [prod_apply hs]
apply lintegral_congr_ae
filter_upwards [ae_measure_lt_top hs h2s] with x hx
rw [lt_top_iff_ne_top] at hx
simp [ofReal_toReal, hx]
