integral_prod_left' — Mathlib

English

A variant ensuring measurability of left-hand integrals in the Fubini setup.

Русский

Вариант левой части доказательства Фубини по мере.

LaTeX

$$$$\\text{StronglyMeasurable}\\left( x \\mapsto \\int_y f(x,y)\\,d\\nu\\right)$$$$

Lean4

/-- The Bochner integral is measurable. This shows that the integrand of (the right-hand-side of)
  the symmetric version of Fubini's theorem is measurable. -/
theorem integral_prod_left' [SFinite μ] ⦃f : α × β → E⦄ (hf : StronglyMeasurable f) :
    StronglyMeasurable fun y => ∫ x, f (x, y) ∂μ :=
  (hf.comp_measurable measurable_swap).integral_prod_right'

Похожие утверждения