Documentation

Mathlib.MeasureTheory.Constructions.Prod.Integral

Integration with respect to the product measure #

In this file we prove Fubini's theorem.

Main results #

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.

theorem MeasureTheory.StronglyMeasurable.integral_prod_right {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [NormedSpace E] [MeasureTheory.SFinite ν] ⦃f : αβE (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)) :
MeasureTheory.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.

theorem MeasureTheory.StronglyMeasurable.integral_prod_right' {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [NormedSpace E] [MeasureTheory.SFinite ν] ⦃f : α × βE (hf : MeasureTheory.StronglyMeasurable f) :
MeasureTheory.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.

theorem MeasureTheory.StronglyMeasurable.integral_prod_left {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace E] [MeasureTheory.SFinite μ] ⦃f : αβE (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)) :
MeasureTheory.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.

theorem MeasureTheory.StronglyMeasurable.integral_prod_left' {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace E] [MeasureTheory.SFinite μ] ⦃f : α × βE (hf : MeasureTheory.StronglyMeasurable f) :
MeasureTheory.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 #

theorem MeasureTheory.Measure.integrable_measure_prod_mk_left {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) (h2s : (μ.prod ν) s ) :
MeasureTheory.Integrable (fun (x : α) => (ν (Prod.mk x ⁻¹' s)).toReal) μ
theorem MeasureTheory.AEStronglyMeasurable.prod_swap {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {γ : Type u_7} [TopologicalSpace γ] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {f : β × αγ} (hf : MeasureTheory.AEStronglyMeasurable f (ν.prod μ)) :
MeasureTheory.AEStronglyMeasurable (fun (z : α × β) => f z.swap) (μ.prod ν)
theorem MeasureTheory.AEStronglyMeasurable.fst {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {γ : Type u_7} [TopologicalSpace γ] [MeasureTheory.SFinite ν] {f : αγ} (hf : MeasureTheory.AEStronglyMeasurable f μ) :
MeasureTheory.AEStronglyMeasurable (fun (z : α × β) => f z.1) (μ.prod ν)
theorem MeasureTheory.AEStronglyMeasurable.snd {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {γ : Type u_7} [TopologicalSpace γ] [MeasureTheory.SFinite ν] {f : βγ} (hf : MeasureTheory.AEStronglyMeasurable f ν) :
MeasureTheory.AEStronglyMeasurable (fun (z : α × β) => f z.2) (μ.prod ν)
theorem MeasureTheory.AEStronglyMeasurable.integral_prod_right' {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] ⦃f : α × βE (hf : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)) :
MeasureTheory.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.

theorem MeasureTheory.AEStronglyMeasurable.prod_mk_left {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {γ : Type u_7} [MeasureTheory.SFinite ν] [TopologicalSpace γ] {f : α × βγ} (hf : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)) :
∀ᵐ (x : α) ∂μ, MeasureTheory.AEStronglyMeasurable (fun (y : β) => f (x, y)) ν

Integrability on a product #

theorem MeasureTheory.integrable_swap_iff {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {f : α × βE} :
MeasureTheory.Integrable (f Prod.swap) (ν.prod μ) MeasureTheory.Integrable f (μ.prod ν)
theorem MeasureTheory.Integrable.swap {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] ⦃f : α × βE (hf : MeasureTheory.Integrable f (μ.prod ν)) :
MeasureTheory.Integrable (f Prod.swap) (ν.prod μ)
theorem MeasureTheory.hasFiniteIntegral_prod_iff {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] ⦃f : α × βE (h1f : MeasureTheory.StronglyMeasurable f) :
MeasureTheory.HasFiniteIntegral f (μ.prod ν) (∀ᵐ (x : α) ∂μ, MeasureTheory.HasFiniteIntegral (fun (y : β) => f (x, y)) ν) MeasureTheory.HasFiniteIntegral (fun (x : α) => ∫ (y : β), f (x, y)ν) μ
theorem MeasureTheory.hasFiniteIntegral_prod_iff' {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] ⦃f : α × βE (h1f : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)) :
MeasureTheory.HasFiniteIntegral f (μ.prod ν) (∀ᵐ (x : α) ∂μ, MeasureTheory.HasFiniteIntegral (fun (y : β) => f (x, y)) ν) MeasureTheory.HasFiniteIntegral (fun (x : α) => ∫ (y : β), f (x, y)ν) μ
theorem MeasureTheory.integrable_prod_iff {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] ⦃f : α × βE (h1f : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)) :
MeasureTheory.Integrable f (μ.prod ν) (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (y : β) => f (x, y)) ν) MeasureTheory.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.

theorem MeasureTheory.integrable_prod_iff' {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] ⦃f : α × βE (h1f : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)) :
MeasureTheory.Integrable f (μ.prod ν) (∀ᵐ (y : β) ∂ν, MeasureTheory.Integrable (fun (x : α) => f (x, y)) μ) MeasureTheory.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.

theorem MeasureTheory.Integrable.prod_left_ae {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] ⦃f : α × βE (hf : MeasureTheory.Integrable f (μ.prod ν)) :
∀ᵐ (y : β) ∂ν, MeasureTheory.Integrable (fun (x : α) => f (x, y)) μ
theorem MeasureTheory.Integrable.prod_right_ae {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] ⦃f : α × βE (hf : MeasureTheory.Integrable f (μ.prod ν)) :
∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (y : β) => f (x, y)) ν
theorem MeasureTheory.Integrable.integral_norm_prod_left {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] ⦃f : α × βE (hf : MeasureTheory.Integrable f (μ.prod ν)) :
MeasureTheory.Integrable (fun (x : α) => ∫ (y : β), f (x, y)ν) μ
theorem MeasureTheory.Integrable.integral_norm_prod_right {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] ⦃f : α × βE (hf : MeasureTheory.Integrable f (μ.prod ν)) :
MeasureTheory.Integrable (fun (y : β) => ∫ (x : α), f (x, y)μ) ν
theorem MeasureTheory.Integrable.prod_smul {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] {𝕜 : Type u_7} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {f : α𝕜} {g : βE} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g ν) :
MeasureTheory.Integrable (fun (z : α × β) => f z.1 g z.2) (μ.prod ν)
theorem MeasureTheory.Integrable.prod_mul {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {L : Type u_7} [RCLike L] {f : αL} {g : βL} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g ν) :
MeasureTheory.Integrable (fun (z : α × β) => f z.1 * g z.2) (μ.prod ν)
theorem MeasureTheory.Integrable.integral_prod_left {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] ⦃f : α × βE (hf : MeasureTheory.Integrable f (μ.prod ν)) :
MeasureTheory.Integrable (fun (x : α) => ∫ (y : β), f (x, y)ν) μ
theorem MeasureTheory.Integrable.integral_prod_right {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] ⦃f : α × βE (hf : MeasureTheory.Integrable f (μ.prod ν)) :
MeasureTheory.Integrable (fun (y : β) => ∫ (x : α), f (x, y)μ) ν

The Bochner integral on a product #

theorem MeasureTheory.integral_prod_swap {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] (f : α × βE) :
∫ (z : β × α), f z.swapν.prod μ = ∫ (z : α × β), 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.

theorem MeasureTheory.integral_fn_integral_add {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace E'] ⦃f : α × βE ⦃g : α × βE (F : EE') (hf : MeasureTheory.Integrable f (μ.prod ν)) (hg : MeasureTheory.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.

theorem MeasureTheory.integral_fn_integral_sub {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace E'] ⦃f : α × βE ⦃g : α × βE (F : EE') (hf : MeasureTheory.Integrable f (μ.prod ν)) (hg : MeasureTheory.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.

theorem MeasureTheory.lintegral_fn_integral_sub {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] ⦃f : α × βE ⦃g : α × βE (F : EENNReal) (hf : MeasureTheory.Integrable f (μ.prod ν)) (hg : MeasureTheory.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.

theorem MeasureTheory.integral_integral_add {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] ⦃f : α × βE ⦃g : α × βE (hf : MeasureTheory.Integrable f (μ.prod ν)) (hg : MeasureTheory.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.

theorem MeasureTheory.integral_integral_add' {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] ⦃f : α × βE ⦃g : α × βE (hf : MeasureTheory.Integrable f (μ.prod ν)) (hg : MeasureTheory.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.

theorem MeasureTheory.integral_integral_sub {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] ⦃f : α × βE ⦃g : α × βE (hf : MeasureTheory.Integrable f (μ.prod ν)) (hg : MeasureTheory.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.

theorem MeasureTheory.integral_integral_sub' {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] ⦃f : α × βE ⦃g : α × βE (hf : MeasureTheory.Integrable f (μ.prod ν)) (hg : MeasureTheory.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.

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

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

theorem MeasureTheory.integral_prod {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] (f : α × βE) (hf : MeasureTheory.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.

theorem MeasureTheory.integral_prod_symm {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] (f : α × βE) (hf : MeasureTheory.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.

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

Reversed version of Fubini's Theorem.

theorem MeasureTheory.integral_integral_symm {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] {f : αβE} (hf : MeasureTheory.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).

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

Change the order of Bochner integration.

theorem MeasureTheory.setIntegral_prod {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] (f : α × βE) {s : Set α} {t : Set β} (hf : MeasureTheory.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.

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

Alias of MeasureTheory.setIntegral_prod.


Fubini's Theorem for set integrals.

theorem MeasureTheory.integral_prod_smul {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] {𝕜 : Type u_8} [RCLike 𝕜] [NormedSpace 𝕜 E] (f : α𝕜) (g : βE) :
∫ (z : α × β), f z.1 g z.2μ.prod ν = (∫ (x : α), f xμ) ∫ (y : β), g yν
theorem MeasureTheory.integral_prod_mul {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {L : Type u_8} [RCLike L] (f : αL) (g : βL) :
∫ (z : α × β), f z.1 * g z.2μ.prod ν = (∫ (x : α), f xμ) * ∫ (y : β), g yν
theorem MeasureTheory.setIntegral_prod_mul {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {L : Type u_8} [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ν
@[deprecated MeasureTheory.setIntegral_prod_mul]
theorem MeasureTheory.set_integral_prod_mul {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {L : Type u_8} [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ν

Alias of MeasureTheory.setIntegral_prod_mul.

theorem MeasureTheory.integral_fun_snd {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] (f : βE) :
∫ (z : α × β), f z.2μ.prod ν = (μ Set.univ).toReal ∫ (y : β), f yν
theorem MeasureTheory.integral_fun_fst {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SFinite ν] [NormedSpace E] [MeasureTheory.SFinite μ] (f : αE) :
∫ (z : α × β), f z.1μ.prod ν = (ν Set.univ).toReal ∫ (x : α), f xμ

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.