lintegral_prod_left' — Mathlib

English

The Lebesgue integral is measurable; the integrand in Tonelli's theorem (right-hand side) is measurable when f is suitably measurable.

Русский

Лебегов интеграл измерим; интегрант правой части теоремы Тонелли измерим при корректной измеримости f.

LaTeX

$$$\\text{Measurable}(f) \\Rightarrow \\text{Measurable}(x \\mapsto \\int f(x,y) \\, dν(y))$$$

Lean4

/-- The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of)
  the symmetric version of Tonelli's theorem is measurable. -/
@[fun_prop, measurability]
theorem lintegral_prod_left' [SFinite μ] {f : α × β → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun y => ∫⁻ x, f (x, y) ∂μ :=
  (measurable_swap_iff.mpr hf).lintegral_prod_right'

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