Theorems · Theorem · measure theory

MeasureTheory.intervalIntegral_integral_swap

∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] {a b : ℝ} {f : ℝ → α → E},
  MeasureTheory.Integrable (Function.uncurry f) ((MeasureTheory.volume.restrict (Set.uIoc a b)).prod μ) →
    ∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ = ∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ

Change the order of integration, when one of the integrals is an interval integral.

Defined in

Mathlib.MeasureTheory.Integral.Prod

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupNormedSpaceMeasureTheory.SFinite