integral_prod_left — Mathlib

English

Similarly, the map y ↦ ∫ f(x, y) dν is measurable in y when f is measurable in the second argument.

Русский

Аналогично, отображение y ↦ ∫ f(x,y) dν измеримо в y при измеримости по второй переменной.

LaTeX

$$$$\\text{StronglyMeasurable}\\left( y \\mapsto \\int_x f(x,y)\\,d\\mu\\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.
  This version has `f` in curried form. -/
theorem integral_prod_left [SFinite μ] ⦃f : α → β → E⦄ (hf : StronglyMeasurable (uncurry f)) :
    StronglyMeasurable fun y => ∫ x, f x y ∂μ :=
  (hf.comp_measurable measurable_swap).integral_prod_right'

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