Product integrals over measurable sets by slices

This file provides Tonelli and Fubini formulas for integration over an arbitrary measurable subset of a product, together with their specialization to a region between two measurable real-valued graphs, in the closed-interval convention.

Mathlib's setLIntegral_prod / setIntegral_prod cover only rectangles s ×ˢ t. The inner integral below is over the section {y | (x, y) ∈ T}, written Prod.mk x ⁻¹' T.

The named Mathlib region between graphs is regionBetween (Ioo). The lemmas in this file use the closed companion already recorded as measurableSet_region_between_cc. For Lebesgue measure on the fibre, the graphs are null, so the Ioo and Icc conventions agree.

This is a temporary project home. Intended Mathlib placement:

• setLIntegral_prod_slices, setLIntegral_prod_slices_symm → Mathlib.MeasureTheory.Measure.Prod, next to setLIntegral_prod
• setIntegral_prod_slices, setIntegral_prod_slices_symm → Mathlib.MeasureTheory.Integral.Prod, next to setIntegral_prod
• the Icc graph lemmas → next to regionBetween in Mathlib.MeasureTheory.Measure.Lebesgue.Basic

setIntegral_prod_Icc_slice_volume is a local convenience for the product MeasureSpace instance on α × ℝ and is not intended for Mathlib.

TODO: if those lemmas land in Mathlib, delete this file and switch uses to the upstream names.

Nonnegative integrals

theorem MeasureTheory.setLIntegral_prod_slices {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [SFinite ν] (T : Set (α × β)) (hT : MeasurableSet T) (f : α × β → ENNReal) (hf : AEMeasurable f ((μ.prod ν).restrict T)) : ∫⁻ (p : α × β) in T, f p ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β) in Prod.mk x ⁻¹' T, f (x, y) ∂ν ∂μ

Tonelli's theorem for a nonnegative integral restricted to a measurable subset T of a product. The inner integral is over the section {y | (x, y) ∈ T}. Unlike setIntegral_prod_slices, this result requires no integrability hypothesis.

theorem MeasureTheory.setLIntegral_prod_slices_symm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [SFinite μ] [SFinite ν] (T : Set (α × β)) (hT : MeasurableSet T) (f : α × β → ENNReal) (hf : AEMeasurable f ((μ.prod ν).restrict T)) : ∫⁻ (p : α × β) in T, f p ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α) in Prod.mk y ⁻¹' Prod.swap ⁻¹' T, f (x, y) ∂μ ∂ν

Symmetric Tonelli theorem for a nonnegative integral restricted to a measurable subset T of a product. The inner integral is over the section {x | (x, y) ∈ T}.

Bochner integrals

theorem MeasureTheory.setIntegral_prod_slices {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {ν : Measure β} [SigmaFinite μ] [SigmaFinite ν] (T : Set (α × β)) (hT : MeasurableSet T) (f : α × β → E) (hf : IntegrableOn f T (μ.prod ν)) : ∫ (p : α × β) in T, f p ∂μ.prod ν = ∫ (x : α), ∫ (y : β) in Prod.mk x ⁻¹' T, f (x, y) ∂ν ∂μ

Fubini's theorem for an integrable function restricted to a measurable subset T of a product. The inner integral is over the section {y | (x, y) ∈ T}.

theorem MeasureTheory.setIntegral_prod_slices_symm {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {ν : Measure β} [SigmaFinite μ] [SigmaFinite ν] (T : Set (α × β)) (hT : MeasurableSet T) (f : α × β → E) (hf : IntegrableOn f T (μ.prod ν)) : ∫ (p : α × β) in T, f p ∂μ.prod ν = ∫ (y : β), ∫ (x : α) in Prod.mk y ⁻¹' Prod.swap ⁻¹' T, f (x, y) ∂μ ∂ν

Symmetric Fubini theorem for an integrable function restricted to a measurable subset T of a product. The inner integral is over the section {x | (x, y) ∈ T}.

Regions between graphs of real functions

theorem MeasureTheory.setLIntegral_prod_Icc_slice {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : MeasurableSet s) {lo hi : α → ℝ} (hlo : Measurable lo) (hhi : Measurable hi) (f : α × ℝ → ENNReal) (hf : AEMeasurable f ((μ.prod volume).restrict {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Icc (lo p.1) (hi p.1)})) : ∫⁻ (p : α × ℝ) in {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Icc (lo p.1) (hi p.1)}, f p ∂μ.prod volume = ∫⁻ (x : α) in s, ∫⁻ (t : ℝ) in Set.Icc (lo x) (hi x), f (x, t) ∂μ

Tonelli's theorem for the region between two graphs, in the closed-interval convention. This is the Icc companion of regionBetween; see measurableSet_region_between_cc.

theorem MeasureTheory.setIntegral_prod_Icc_slice {α : Type u_1} [MeasurableSpace α] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} [SigmaFinite μ] {s : Set α} (hs : MeasurableSet s) {lo hi : α → ℝ} (hlo : Measurable lo) (hhi : Measurable hi) (f : α × ℝ → E) (hf : IntegrableOn f {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Icc (lo p.1) (hi p.1)} (μ.prod volume)) : ∫ (p : α × ℝ) in {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Icc (lo p.1) (hi p.1)}, f p ∂μ.prod volume = ∫ (x : α) in s, ∫ (t : ℝ) in Set.Icc (lo x) (hi x), f (x, t) ∂μ

Fubini's theorem for the region between two graphs, in the closed-interval convention. This is the Icc companion of regionBetween; see measurableSet_region_between_cc.

theorem MeasureTheory.setIntegral_prod_Icc_slice_volume {α : Type u_2} [MeasureSpace α] [SigmaFinite volume] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set α} (hs : MeasurableSet s) {lo hi : α → ℝ} (hlo : Measurable lo) (hhi : Measurable hi) (f : α × ℝ → E) (hf : IntegrableOn f {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Icc (lo p.1) (hi p.1)} volume) : ∫ (p : α × ℝ) in {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Icc (lo p.1) (hi p.1)}, f p = ∫ (x : α) in s, ∫ (t : ℝ) in Set.Icc (lo x) (hi x), f (x, t)

Volume form of setIntegral_prod_Icc_slice, matching the product MeasureSpace instance on α × ℝ. Local convenience, not intended for Mathlib.