Theorems · Theorem · measure theory

Measurable.lintegral_prod_right

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {f : α → β → ENNReal},
  Measurable (Function.uncurry f) → Measurable fun x => ∫⁻ (y : β), f x y ∂ν

The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of) Tonelli's theorem is measurable. This version has the argument f in curried form.

Defined in

Mathlib.MeasureTheory.Measure.Prod

Cited by

10 results in Mathlib

Foundations

Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceMeasurableSpaceMeasureTheory.SFinite