mathlib3 documentation

measure_theory.constructions.prod.integral

Integration with respect to the product measure #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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.

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 #

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.

Integrability on a product #

theorem measure_theory.integrable_prod_iff {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] ⦃f : α × β E⦄ (h1f : measure_theory.ae_strongly_measurable f (μ.prod ν)) :
measure_theory.integrable f (μ.prod ν) (∀ᵐ (x : α) μ, measure_theory.integrable (λ (y : β), f (x, y)) ν) measure_theory.integrable (λ (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 measure_theory.integrable_prod_iff' {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [measure_theory.sigma_finite μ] ⦃f : α × β E⦄ (h1f : measure_theory.ae_strongly_measurable f (μ.prod ν)) :
measure_theory.integrable f (μ.prod ν) (∀ᵐ (y : β) ν, measure_theory.integrable (λ (x : α), f (x, y)) μ) measure_theory.integrable (λ (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 measure_theory.integrable_prod_mul {α : Type u_1} {β : Type u_3} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [measure_theory.sigma_finite ν] {L : Type u_2} [is_R_or_C L] {f : α L} {g : β L} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g ν) :
measure_theory.integrable (λ (z : α × β), f z.fst * g z.snd) (μ.prod ν)

The Bochner integral on a product #

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 measure_theory.integral_fn_integral_add {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] {E' : Type u_7} [normed_add_comm_group E'] [complete_space E'] [normed_space E'] ⦃f g : α × β E⦄ (F : E E') (hf : measure_theory.integrable f (μ.prod ν)) (hg : measure_theory.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 measure_theory.integral_fn_integral_sub {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] {E' : Type u_7} [normed_add_comm_group E'] [complete_space E'] [normed_space E'] ⦃f g : α × β E⦄ (F : E E') (hf : measure_theory.integrable f (μ.prod ν)) (hg : measure_theory.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 measure_theory.lintegral_fn_integral_sub {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] ⦃f g : α × β E⦄ (F : E ennreal) (hf : measure_theory.integrable f (μ.prod ν)) (hg : measure_theory.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 measure_theory.integral_integral_add {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] ⦃f g : α × β E⦄ (hf : measure_theory.integrable f (μ.prod ν)) (hg : measure_theory.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 measure_theory.integral_integral_add' {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] ⦃f g : α × β E⦄ (hf : measure_theory.integrable f (μ.prod ν)) (hg : measure_theory.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 measure_theory.integral_integral_sub {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] ⦃f g : α × β E⦄ (hf : measure_theory.integrable f (μ.prod ν)) (hg : measure_theory.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 measure_theory.integral_integral_sub' {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] ⦃f g : α × β E⦄ (hf : measure_theory.integrable f (μ.prod ν)) (hg : measure_theory.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.

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

theorem measure_theory.integral_prod {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] (f : α × β E) (hf : measure_theory.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. measure_theory.integrable.integral_prod_right is useful to show that the inner integral of the right-hand side is integrable.

theorem measure_theory.integral_prod_symm {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] (f : α × β E) (hf : measure_theory.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 measure_theory.integral_integral {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] {f : α β E} (hf : measure_theory.integrable (function.uncurry f) (μ.prod ν)) :
(x : α), (y : β), f x y ν μ = (z : α × β), f z.fst z.snd μ.prod ν

Reversed version of Fubini's Theorem.

theorem measure_theory.integral_integral_symm {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] {f : α β E} (hf : measure_theory.integrable (function.uncurry f) (μ.prod ν)) :
(x : α), (y : β), f x y ν μ = (z : β × α), f z.snd z.fst ν.prod μ

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

theorem measure_theory.integral_integral_swap {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] ⦃f : α β E (hf : measure_theory.integrable (function.uncurry f) (μ.prod ν)) :
(x : α), (y : β), f x y ν μ = (y : β), (x : α), f x y μ ν

Change the order of Bochner integration.

theorem measure_theory.set_integral_prod {α : Type u_1} {β : Type u_3} {E : Type u_6} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [normed_add_comm_group E] [measure_theory.sigma_finite ν] [normed_space E] [complete_space E] [measure_theory.sigma_finite μ] (f : α × β E) {s : set α} {t : set β} (hf : measure_theory.integrable_on 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.

theorem measure_theory.integral_prod_mul {α : Type u_1} {β : Type u_3} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [measure_theory.sigma_finite ν] [measure_theory.sigma_finite μ] {L : Type u_2} [is_R_or_C L] (f : α L) (g : β L) :
(z : α × β), f z.fst * g z.snd μ.prod ν = (x : α), f x μ * (y : β), g y ν
theorem measure_theory.set_integral_prod_mul {α : Type u_1} {β : Type u_3} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} [measure_theory.sigma_finite ν] [measure_theory.sigma_finite μ] {L : Type u_2} [is_R_or_C L] (f : α L) (g : β L) (s : set α) (t : set β) :
(z : α × β) in s ×ˢ t, f z.fst * g z.snd μ.prod ν = (x : α) in s, f x μ * (y : β) in t, g y ν