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.

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.SigmaFinite ν] ⦃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.

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.SigmaFinite μ] ⦃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.SigmaFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) (h2s : (MeasureTheory.Measure.prod μ ν) s ) :
MeasureTheory.Integrable (fun (x : α) => (ν (Prod.mk x ⁻¹' s)).toReal) μ

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.SigmaFinite ν] [TopologicalSpace γ] {f : α × βγ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.prod μ ν)) :
∀ᵐ (x : α) ∂μ, MeasureTheory.AEStronglyMeasurable (fun (y : β) => f (x, y)) ν

Integrability on a product #

theorem MeasureTheory.hasFiniteIntegral_prod_iff {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SigmaFinite ν] ⦃f : α × βE (h1f : MeasureTheory.StronglyMeasurable f) :
MeasureTheory.HasFiniteIntegral f (MeasureTheory.Measure.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.SigmaFinite ν] ⦃f : α × βE (h1f : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.prod μ ν)) :
MeasureTheory.HasFiniteIntegral f (MeasureTheory.Measure.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.SigmaFinite ν] ⦃f : α × βE (h1f : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.prod μ ν)) :
MeasureTheory.Integrable f (MeasureTheory.Measure.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.SigmaFinite ν] [MeasureTheory.SigmaFinite μ] ⦃f : α × βE (h1f : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.prod μ ν)) :
MeasureTheory.Integrable f (MeasureTheory.Measure.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.SigmaFinite ν] [MeasureTheory.SigmaFinite μ] ⦃f : α × βE (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.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.SigmaFinite ν] [MeasureTheory.SigmaFinite μ] ⦃f : α × βE (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.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.SigmaFinite ν] ⦃f : α × βE (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν)) :
MeasureTheory.Integrable (fun (x : α) => ∫ (y : β), 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.SigmaFinite ν] {𝕜 : 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) (MeasureTheory.Measure.prod μ ν)
theorem MeasureTheory.Integrable.prod_mul {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite ν] {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) (MeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] ⦃f : α × βE (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν)) :
MeasureTheory.Integrable (fun (x : α) => ∫ (y : β), 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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] (f : α × βE) :
∫ (z : β × α), f (Prod.swap z)MeasureTheory.Measure.prod ν μ = ∫ (z : α × β), f zMeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace E'] ⦃f : α × βE ⦃g : α × βE (F : EE') (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν)) (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] {E' : Type u_7} [NormedAddCommGroup E'] [NormedSpace E'] ⦃f : α × βE ⦃g : α × βE (F : EE') (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν)) (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] ⦃f : α × βE ⦃g : α × βE (F : EENNReal) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν)) (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] ⦃f : α × βE ⦃g : α × βE (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν)) (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] ⦃f : α × βE ⦃g : α × βE (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν)) (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] ⦃f : α × βE ⦃g : α × βE (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν)) (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] ⦃f : α × βE ⦃g : α × βE (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν)) (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] :
Continuous fun (f : (MeasureTheory.Lp E 1 (MeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] (f : α × βE) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν)) :
∫ (z : α × β), f zMeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] (f : α × βE) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν)) :
∫ (z : α × β), f zMeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] {f : αβE} (hf : MeasureTheory.Integrable (Function.uncurry f) (MeasureTheory.Measure.prod μ ν)) :
∫ (x : α), ∫ (y : β), f x yνμ = ∫ (z : α × β), f z.1 z.2MeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] {f : αβE} (hf : MeasureTheory.Integrable (Function.uncurry f) (MeasureTheory.Measure.prod μ ν)) :
∫ (x : α), ∫ (y : β), f x yνμ = ∫ (z : β × α), f z.2 z.1MeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] ⦃f : αβE (hf : MeasureTheory.Integrable (Function.uncurry f) (MeasureTheory.Measure.prod μ ν)) :
∫ (x : α), ∫ (y : β), f x yνμ = ∫ (y : β), ∫ (x : α), f x yμν

Change the order of Bochner integration.

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

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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] {𝕜 : Type u_8} [RCLike 𝕜] [NormedSpace 𝕜 E] (f : α𝕜) (g : βE) :
∫ (z : α × β), f z.1 g z.2MeasureTheory.Measure.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.SigmaFinite ν] [MeasureTheory.SigmaFinite μ] {L : Type u_8} [RCLike L] (f : αL) (g : βL) :
∫ (z : α × β), f z.1 * g z.2MeasureTheory.Measure.prod μ ν = (∫ (x : α), f xμ) * ∫ (y : β), g yν
theorem MeasureTheory.set_integral_prod_mul {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite μ] {L : Type u_8} [RCLike L] (f : αL) (g : βL) (s : Set α) (t : Set β) :
∫ (z : α × β) in s ×ˢ t, f z.1 * g z.2MeasureTheory.Measure.prod μ ν = (∫ (x : α) in s, f xμ) * ∫ (y : β) in t, g yν
theorem MeasureTheory.integral_fun_snd {α : Type u_1} {β : Type u_3} {E : Type u_6} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [MeasureTheory.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] (f : βE) :
∫ (z : α × β), f z.2MeasureTheory.Measure.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.SigmaFinite ν] [NormedSpace E] [MeasureTheory.SigmaFinite μ] (f : αE) :
∫ (z : α × β), f z.1MeasureTheory.Measure.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.