Theorems · Theorem · measure theory

MeasureTheory.integral_integral_swap_of_hasCompactSupport

∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {X : Type u_5} {Y : Type u_6}
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [inst_4 : MeasurableSpace X] [inst_5 : MeasurableSpace Y]
  [OpensMeasurableSpace X] [OpensMeasurableSpace Y] {f : X → Y → E},
  Continuous (Function.uncurry f) →
    HasCompactSupport (Function.uncurry f) →
      ∀ {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasureOnCompacts μ]
        [MeasureTheory.IsFiniteMeasureOnCompacts ν],
        ∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν

A version of Fubini theorem for continuous functions with compact support: one may swap the order of integration with respect to locally finite measures. One does not assume that the measures are σ-finite, contrary to the usual Fubini theorem.

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

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceMeasurableSpaceMeasurableSpaceOpensMeasurableSpaceOpensMeasurableSpaceMeasureTheory.IsFiniteMeasureOnCompactsMeasureTheory.IsFiniteMeasureOnCompacts