# Integration with respect to the product measure #

In this file we prove Fubini's theorem.

## Main results #

- `MeasureTheory.integrable_prod_iff` states that a binary function is integrable iff both
  - `y ↦ f (x, y)` is integrable for almost every `x`, and
  - the function `x ↦ ∫ ‖f (x, y)‖ dy` is integrable.
- `MeasureTheory.integral_prod`: Fubini's theorem. It states that for an integrable function `α × β → E` (where `E` is a second countable Banach space) we have `∫ z, f z ∂(μ.prod ν) = ∫ x, ∫ y, f (x, y) ∂ν ∂μ`. This theorem has the same variants as Tonelli's theorem (see `MeasureTheory.lintegral_prod`). The lemma `MeasureTheory.Integrable.integral_prod_right` states that the inner integral of the right-hand side is integrable.
- `MeasureTheory.integral_integral_swap_of_hasCompactSupport`: a version of Fubini theorem for continuous functions with compact support, which does not assume that the measures are σ-finite contrary to all the usual versions of Fubini.

## Tags #

product measure, Fubini's theorem, Fubini-Tonelli theorem

### Measurability #

Before we define the product measure, we can talk about the measurability of operations on binary functions. We show that if `f` is a binary measurable function, then the function that integrates along one of the variables (using either the Lebesgue or Bochner integral) is measurable.

source
theorem measurableSet_integrable {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] ⦃f : α → β → E⦄ (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)) :
MeasurableSet {x : α | MeasureTheory.Integrable (f x) ν}
source
theorem MeasureTheory.StronglyMeasurable.integral_prod_right {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ν : Measure β} [NormedAddCommGroup E] [NormedSpace ℝ E] [SFinite ν] ⦃f : α → β → E⦄ (hf : StronglyMeasurable (Function.uncurry f)) :
StronglyMeasurable fun (x : α) => ∫ (y : β), f x y ∂ν

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

source
theorem MeasureTheory.StronglyMeasurable.integral_prod_right' {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ν : Measure β} [NormedAddCommGroup E] [NormedSpace ℝ E] [SFinite ν] ⦃f : α × β → E⦄ (hf : StronglyMeasurable f) :
StronglyMeasurable fun (x : α) => ∫ (y : β), f (x, y) ∂ν

The Bochner integral is measurable. This shows that the integrand of (the right-hand-side of) Fubini's theorem is measurable.

source
theorem MeasureTheory.StronglyMeasurable.integral_prod_left {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] [SFinite μ] ⦃f : α → β → E⦄ (hf : StronglyMeasurable (Function.uncurry f)) :
StronglyMeasurable fun (y : β) => ∫ (x : α), f x y ∂μ

The Bochner integral is measurable. This shows that the integrand of (the right-hand-side of) the symmetric version of Fubini's theorem is measurable. This version has `f` in curried form.

source
theorem MeasureTheory.StronglyMeasurable.integral_prod_left' {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] [SFinite μ] ⦃f : α × β → E⦄ (hf : StronglyMeasurable f) :
StronglyMeasurable fun (y : β) => ∫ (x : α), f (x, y) ∂μ

The Bochner integral is measurable. This shows that the integrand of (the right-hand-side of) the symmetric version of Fubini's theorem is measurable.

### The product measure #

source
theorem MeasureTheory.Measure.integrable_measure_prodMk_left {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) (h2s : (μ.prod ν) s ≠ ⊤) :
Integrable (fun (x : α) => ν.real (Prod.mk x ⁻¹' s)) μ
source
theorem MeasureTheory.AEStronglyMeasurable.prod_swap {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {X : Type u_4} [TopologicalSpace X] [SFinite μ] [SFinite ν] {f : β × α → X} (hf : AEStronglyMeasurable f (ν.prod μ)) :
AEStronglyMeasurable (fun (z : α × β) => f z.swap) (μ.prod ν)
source
theorem MeasureTheory.AEStronglyMeasurable.comp_fst {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {γ : Type u_5} [TopologicalSpace γ] {f : α → γ} (hf : AEStronglyMeasurable f μ) :
AEStronglyMeasurable (fun (z : α × β) => f z.1) (μ.prod ν)
source
theorem MeasureTheory.AEStronglyMeasurable.comp_snd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {γ : Type u_5} [TopologicalSpace γ] {f : β → γ} (hf : AEStronglyMeasurable f ν) :
AEStronglyMeasurable (fun (z : α × β) => f z.2) (μ.prod ν)
source
theorem MeasureTheory.AEStronglyMeasurable.integral_prod_right' {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] ⦃f : α × β → E⦄ (hf : AEStronglyMeasurable f (μ.prod ν)) :
AEStronglyMeasurable (fun (x : α) => ∫ (y : β), f (x, y) ∂ν) μ

The Bochner integral is a.e.-measurable. This shows that the integrand of (the right-hand-side of) Fubini's theorem is a.e.-measurable.

source
theorem MeasureTheory.AEStronglyMeasurable.prodMk_left {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {X : Type u_4} [TopologicalSpace X] [SFinite ν] {f : α × β → X} (hf : AEStronglyMeasurable f (μ.prod ν)) :
∀ᵐ (x : α) ∂μ, AEStronglyMeasurable (fun (y : β) => f (x, y)) ν
source
theorem MeasureTheory.AEStronglyMeasurable.prodMk_right {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {X : Type u_4} [TopologicalSpace X] [SFinite μ] [SFinite ν] {f : α × β → X} (hf : AEStronglyMeasurable f (μ.prod ν)) :
∀ᵐ (y : β) ∂ν, AEStronglyMeasurable (fun (x : α) => f (x, y)) μ
source
theorem MeasureTheory.AEStronglyMeasurable.of_comp_snd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {X : Type u_4} [TopologicalSpace X] {f : β → X} [SFinite ν] (hf : AEStronglyMeasurable (fun (x : α × β) => f x.2) (μ.prod ν)) (hμ : μ ≠ 0) :
AEStronglyMeasurable f ν
source
theorem MeasureTheory.AEStronglyMeasurable.of_comp_fst {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {X : Type u_4} [TopologicalSpace X] {f : α → X} [SFinite μ] [SFinite ν] (hf : AEStronglyMeasurable (fun (x : α × β) => f x.1) (μ.prod ν)) (hν : ν ≠ 0) :
AEStronglyMeasurable f μ
source
theorem MeasureTheory.AEStronglyMeasurable.comp_fst_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {X : Type u_4} [TopologicalSpace X] [SFinite μ] [SFinite ν] {f : α → X} (hν : ν ≠ 0) :
AEStronglyMeasurable (fun (x : α × β) => f x.1) (μ.prod ν) ↔ AEStronglyMeasurable f μ
source
theorem MeasureTheory.AEStronglyMeasurable.comp_snd_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {X : Type u_4} [TopologicalSpace X] [SFinite ν] {f : β → X} (hμ : μ ≠ 0) :
AEStronglyMeasurable (fun (x : α × β) => f x.2) (μ.prod ν) ↔ AEStronglyMeasurable f ν

### Integrability on a product #

source
theorem MeasureTheory.integrable_swap_iff {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [SFinite μ] {f : α × β → E} :
Integrable (f ∘ Prod.swap) (ν.prod μ) ↔ Integrable f (μ.prod ν)
source
theorem MeasureTheory.Integrable.swap {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [SFinite μ] ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) :
Integrable (f ∘ Prod.swap) (ν.prod μ)
source
theorem MeasureTheory.hasFiniteIntegral_prod_iff {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] ⦃f : α × β → E⦄ (h1f : StronglyMeasurable f) :
HasFiniteIntegral f (μ.prod ν) ↔ (∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun (y : β) => f (x, y)) ν) ∧ HasFiniteIntegral (fun (x : α) => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
source
theorem MeasureTheory.hasFiniteIntegral_prod_iff' {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] ⦃f : α × β → E⦄ (h1f : AEStronglyMeasurable f (μ.prod ν)) :
HasFiniteIntegral f (μ.prod ν) ↔ (∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun (y : β) => f (x, y)) ν) ∧ HasFiniteIntegral (fun (x : α) => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
source
theorem MeasureTheory.integrable_prod_iff {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] ⦃f : α × β → E⦄ (h1f : AEStronglyMeasurable f (μ.prod ν)) :
Integrable f (μ.prod ν) ↔ (∀ᵐ (x : α) ∂μ, Integrable (fun (y : β) => f (x, y)) ν) ∧ Integrable (fun (x : α) => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ

A binary function is integrable if the function `y ↦ f (x, y)` is integrable for almost every `x` and the function `x ↦ ∫ ‖f (x, y)‖ dy` is integrable.

source
theorem MeasureTheory.integrable_prod_iff' {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [SFinite μ] ⦃f : α × β → E⦄ (h1f : AEStronglyMeasurable f (μ.prod ν)) :
Integrable f (μ.prod ν) ↔ (∀ᵐ (y : β) ∂ν, Integrable (fun (x : α) => f (x, y)) μ) ∧ Integrable (fun (y : β) => ∫ (x : α), ‖f (x, y)‖ ∂μ) ν

A binary function is integrable if the function `x ↦ f (x, y)` is integrable for almost every `y` and the function `y ↦ ∫ ‖f (x, y)‖ dx` is integrable.

source
theorem MeasureTheory.Integrable.prod_left_ae {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [SFinite μ] ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) :
∀ᵐ (y : β) ∂ν, Integrable (fun (x : α) => f (x, y)) μ
source
theorem MeasureTheory.Integrable.prod_right_ae {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [SFinite μ] ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) :
∀ᵐ (x : α) ∂μ, Integrable (fun (y : β) => f (x, y)) ν
source
theorem MeasureTheory.Integrable.integral_norm_prod_left {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) :
Integrable (fun (x : α) => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
source
theorem MeasureTheory.Integrable.integral_norm_prod_right {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [SFinite μ] ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) :
Integrable (fun (y : β) => ∫ (x : α), ‖f (x, y)‖ ∂μ) ν
source
theorem MeasureTheory.Integrable.op_fst_snd {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] {F : Type u_4} {G : Type u_5} [NormedAddCommGroup F] [NormedAddCommGroup G] {op : E → F → G} (hop : Continuous (Function.uncurry op)) (hop_norm : ∃ (C : ℝ), ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖) {f : α → E} {g : β → F} (hf : Integrable f μ) (hg : Integrable g ν) :
Integrable (fun (z : α × β) => op (f z.1) (g z.2)) (μ.prod ν)
source
theorem MeasureTheory.Integrable.comp_fst {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} [NormedAddCommGroup E] {f : α → E} (hf : Integrable f μ) (ν : Measure β) [IsFiniteMeasure ν] :
Integrable (fun (x : α × β) => f x.1) (μ.prod ν)
source
theorem MeasureTheory.Integrable.comp_snd {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] {f : β → E} (hf : Integrable f ν) (μ : Measure α) [IsFiniteMeasure μ] :
Integrable (fun (x : α × β) => f x.2) (μ.prod ν)
source
theorem MeasureTheory.Integrable.smul_prod {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] {R : Type u_4} [NormedRing R] [Module R E] [IsBoundedSMul R E] {f : α → R} {g : β → E} (hf : Integrable f μ) (hg : Integrable g ν) :
Integrable (fun (z : α × β) => f z.1 • g z.2) (μ.prod ν)
source
theorem MeasureTheory.Integrable.mul_prod {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {L : Type u_4} [NormedRing L] {f : α → L} {g : β → L} (hf : Integrable f μ) (hg : Integrable g ν) :
Integrable (fun (z : α × β) => f z.1 * g z.2) (μ.prod ν)
source
theorem MeasureTheory.IntegrableOn.swap {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [SFinite μ] {f : α × β → E} {s : Set α} {t : Set β} (hf : IntegrableOn f (s ×ˢ t) (μ.prod ν)) :
IntegrableOn (f ∘ Prod.swap) (t ×ˢ s) (ν.prod μ)
source
theorem MeasureTheory.Integrable.of_comp_snd {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] {f : β → E} (hf : Integrable (fun (x : α × β) => f x.2) (μ.prod ν)) (hμ : μ ≠ 0) :
Integrable f ν
source
theorem MeasureTheory.Integrable.of_comp_fst {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [SFinite μ] {f : α → E} (hf : Integrable (fun (x : α × β) => f x.1) (μ.prod ν)) (hν : ν ≠ 0) :
Integrable f μ
source
theorem MeasureTheory.Integrable.comp_snd_iff {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [IsFiniteMeasure μ] {f : β → E} (hμ : μ ≠ 0) :
Integrable (fun (x : α × β) => f x.2) (μ.prod ν) ↔ Integrable f ν
source
theorem MeasureTheory.Integrable.comp_fst_iff {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite μ] [IsFiniteMeasure ν] {f : α → E} (hν : ν ≠ 0) :
Integrable (fun (x : α × β) => f x.1) (μ.prod ν) ↔ Integrable f μ
source
theorem MeasureTheory.Integrable.integral_prod_left {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) :
Integrable (fun (x : α) => ∫ (y : β), f (x, y) ∂ν) μ
source
theorem MeasureTheory.Integrable.integral_prod_right {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) :
Integrable (fun (y : β) => ∫ (x : α), f (x, y) ∂μ) ν

### The Bochner integral on a product #

source
theorem MeasureTheory.integral_prod_swap {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] (f : α × β → E) :
∫ (z : β × α), f z.swap ∂ν.prod μ = ∫ (z : α × β), f z ∂μ.prod ν
source
theorem MeasureTheory.setIntegral_prod_swap {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] (s : Set α) (t : Set β) (f : α × β → E) :
∫ (z : β × α) in t ×ˢ s, f z.swap ∂ν.prod μ = ∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν

Some rules about the sum/difference of double integrals. They follow from `integral_add`, but we separate them out as separate lemmas, because they involve quite some steps.

source
theorem MeasureTheory.integral_fn_integral_add {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] ⦃f g : α × β → E⦄ (F : E → E') (hf : Integrable f (μ.prod ν)) (hg : Integrable g (μ.prod ν)) :
∫ (x : α), F (∫ (y : β), f (x, y) + g (x, y) ∂ν) ∂μ = ∫ (x : α), F (∫ (y : β), f (x, y) ∂ν + ∫ (y : β), g (x, y) ∂ν) ∂μ

Integrals commute with addition inside another integral. `F` can be any function.

source
theorem MeasureTheory.integral_fn_integral_sub {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] ⦃f g : α × β → E⦄ (F : E → E') (hf : Integrable f (μ.prod ν)) (hg : Integrable g (μ.prod ν)) :
∫ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ = ∫ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ

Integrals commute with subtraction inside another integral. `F` can be any measurable function.

source
theorem MeasureTheory.lintegral_fn_integral_sub {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] ⦃f g : α × β → E⦄ (F : E → ENNReal) (hf : Integrable f (μ.prod ν)) (hg : Integrable g (μ.prod ν)) :
∫⁻ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ = ∫⁻ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ

Integrals commute with subtraction inside a lower Lebesgue integral. `F` can be any function.

source
theorem MeasureTheory.integral_integral_add {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] ⦃f g : α × β → E⦄ (hf : Integrable f (μ.prod ν)) (hg : Integrable g (μ.prod ν)) :
∫ (x : α), ∫ (y : β), f (x, y) + g (x, y) ∂ν ∂μ = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ + ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ

Double integrals commute with addition.

source
theorem MeasureTheory.integral_integral_add' {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] ⦃f g : α × β → E⦄ (hf : Integrable f (μ.prod ν)) (hg : Integrable g (μ.prod ν)) :
∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ + ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ

Double integrals commute with addition. This is the version with `(f + g) (x, y)` (instead of `f (x, y) + g (x, y)`) in the LHS.

source
theorem MeasureTheory.integral_integral_sub {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] ⦃f g : α × β → E⦄ (hf : Integrable f (μ.prod ν)) (hg : Integrable g (μ.prod ν)) :
∫ (x : α), ∫ (y : β), f (x, y) - g (x, y) ∂ν ∂μ = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ - ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ

Double integrals commute with subtraction.

source
theorem MeasureTheory.integral_integral_sub' {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] ⦃f g : α × β → E⦄ (hf : Integrable f (μ.prod ν)) (hg : Integrable g (μ.prod ν)) :
∫ (x : α), ∫ (y : β), (f - g) (x, y) ∂ν ∂μ = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ - ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ

Double integrals commute with subtraction. This is the version with `(f - g) (x, y)` (instead of `f (x, y) - g (x, y)`) in the LHS.

source
theorem MeasureTheory.continuous_integral_integral {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] :
Continuous fun (f : ↥(Lp E 1 (μ.prod ν))) => ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ

The map that sends an L¹-function `f : α × β → E` to `∫∫f` is continuous.

source
theorem MeasureTheory.integral_prod {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] (f : α × β → E) (hf : Integrable f (μ.prod ν)) :
∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ

Fubini's Theorem: For integrable functions on `α × β`, the Bochner integral of `f` is equal to the iterated Bochner integral. `integrable_prod_iff` can be useful to show that the function in question in integrable. `MeasureTheory.Integrable.integral_prod_right` is useful to show that the inner integral of the right-hand side is integrable.

source
theorem MeasureTheory.integral_prod_symm {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] (f : α × β → E) (hf : Integrable f (μ.prod ν)) :
∫ (z : α × β), f z ∂μ.prod ν = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν

Symmetric version of Fubini's Theorem: For integrable functions on `α × β`, the Bochner integral of `f` is equal to the iterated Bochner integral. This version has the integrals on the right-hand side in the other order.

source
theorem MeasureTheory.integral_integral {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] {f : α → β → E} (hf : Integrable (Function.uncurry f) (μ.prod ν)) :
∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (z : α × β), f z.1 z.2 ∂μ.prod ν

Reversed version of Fubini's Theorem.

source
theorem MeasureTheory.integral_integral_symm {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] {f : α → β → E} (hf : Integrable (Function.uncurry f) (μ.prod ν)) :
∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (z : β × α), f z.2 z.1 ∂ν.prod μ

Reversed version of Fubini's Theorem (symmetric version).

source
theorem MeasureTheory.integral_integral_swap {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] ⦃f : α → β → E⦄ (hf : Integrable (Function.uncurry f) (μ.prod ν)) :
∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (y : β), ∫ (x : α), f x y ∂μ ∂ν

Change the order of Bochner integration.

source
theorem MeasureTheory.intervalIntegral_integral_swap {α : Type u_1} {E : Type u_3} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] [SFinite μ] {a b : ℝ} {f : ℝ → α → E} (h_int : Integrable (Function.uncurry f) ((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.

source
theorem MeasureTheory.setIntegral_prod {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] (f : α × β → E) {s : Set α} {t : Set β} (hf : IntegrableOn f (s ×ˢ t) (μ.prod ν)) :
∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ

Fubini's Theorem for set integrals.

source
theorem MeasureTheory.integral_prod_smul {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] {𝕜 : Type u_5} [RCLike 𝕜] [NormedSpace 𝕜 E] (f : α → 𝕜) (g : β → E) :
∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν
source
theorem MeasureTheory.integral_prod_mul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [SFinite ν] [SFinite μ] {L : Type u_5} [RCLike L] (f : α → L) (g : β → L) :
∫ (z : α × β), f z.1 * g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) * ∫ (y : β), g y ∂ν
source
theorem MeasureTheory.setIntegral_prod_mul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [SFinite ν] [SFinite μ] {L : Type u_5} [RCLike L] (f : α → L) (g : β → L) (s : Set α) (t : Set β) :
∫ (z : α × β) in s ×ˢ t, f z.1 * g z.2 ∂μ.prod ν = (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν
source
theorem MeasureTheory.integral_fun_snd {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] (f : β → E) :
∫ (z : α × β), f z.2 ∂μ.prod ν = μ.real Set.univ • ∫ (y : β), f y ∂ν
source
theorem MeasureTheory.integral_fun_fst {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} [NormedAddCommGroup E] [SFinite ν] [NormedSpace ℝ E] [SFinite μ] (f : α → E) :
∫ (z : α × β), f z.1 ∂μ.prod ν = ν.real Set.univ • ∫ (x : α), f x ∂μ
source
theorem MeasureTheory.integrable_continuousLinearMap_prod' {E : Type u_5} {F : Type u_6} {G : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : Measure E} [IsProbabilityMeasure μ] {ν : Measure F} [IsProbabilityMeasure ν] {L : E × F →L[ℝ] G} (hLμ : Integrable (⇑(L.comp (ContinuousLinearMap.inl ℝ E F))) μ) (hLν : Integrable (⇑(L.comp (ContinuousLinearMap.inr ℝ E F))) ν) :
Integrable (⇑L) (μ.prod ν)
source
theorem MeasureTheory.integrable_continuousLinearMap_prod {E : Type u_5} {F : Type u_6} {G : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : Measure E} [IsProbabilityMeasure μ] {ν : Measure F} [IsProbabilityMeasure ν] {L : E × F →L[ℝ] G} (hμ : Integrable id μ) (hν : Integrable id ν) :
Integrable (⇑L) (μ.prod ν)
source
theorem MeasureTheory.integral_continuousLinearMap_prod' {E : Type u_5} {F : Type u_6} {G : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : Measure E} [IsProbabilityMeasure μ] {ν : Measure F} [IsProbabilityMeasure ν] {L : E × F →L[ℝ] G} [CompleteSpace G] (hLμ : Integrable (⇑(L.comp (ContinuousLinearMap.inl ℝ E F))) μ) (hLν : Integrable (⇑(L.comp (ContinuousLinearMap.inr ℝ E F))) ν) :
∫ (p : E × F), L p ∂μ.prod ν = ∫ (x : E), (L.comp (ContinuousLinearMap.inl ℝ E F)) x ∂μ + ∫ (y : F), (L.comp (ContinuousLinearMap.inr ℝ E F)) y ∂ν
source
theorem MeasureTheory.integral_continuousLinearMap_prod {E : Type u_5} {F : Type u_6} {G : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] {mE : MeasurableSpace E} [NormedAddCommGroup F] [NormedSpace ℝ F] {mF : MeasurableSpace F} [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : Measure E} [IsProbabilityMeasure μ] {ν : Measure F} [IsProbabilityMeasure ν] {L : E × F →L[ℝ] G} [CompleteSpace G] (hμ : Integrable id μ) (hν : Integrable id ν) :
∫ (p : E × F), L p ∂μ.prod ν = ∫ (x : E), (L.comp (ContinuousLinearMap.inl ℝ E F)) x ∂μ + ∫ (y : F), (L.comp (ContinuousLinearMap.inr ℝ E F)) y ∂ν
source
theorem MeasureTheory.integral_integral_swap_of_hasCompactSupport {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace X] [OpensMeasurableSpace Y] {f : X → Y → E} (hf : Continuous (Function.uncurry f)) (h'f : HasCompactSupport (Function.uncurry f)) {μ : Measure X} {ν : Measure Y} [IsFiniteMeasureOnCompacts μ] [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.