# mathlib3documentation

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 #

• measure_theory.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.
• measure_theory.integral_prod: Fubini's theorem. It states that for a 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 measure_theory.lintegral_prod). The lemma measure_theory.integrable.integral_prod_right states that the inner integral of the right-hand side is integrable.

## 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 measurable_set_integrable {α : Type u_1} {β : Type u_3} {E : Type u_6} {ν : measure_theory.measure β} ⦃f : α β E  :
measurable_set {x : α | ν}
theorem measure_theory.strongly_measurable.integral_prod_right {α : Type u_1} {β : Type u_3} {E : Type u_6} {ν : measure_theory.measure β} [ E] ⦃f : α β E  :
measure_theory.strongly_measurable (λ (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 measure_theory.strongly_measurable.integral_prod_right' {α : Type u_1} {β : Type u_3} {E : Type u_6} {ν : measure_theory.measure β} [ E] ⦃f : α × β E⦄  :
measure_theory.strongly_measurable (λ (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 measure_theory.strongly_measurable.integral_prod_left {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} [ E] ⦃f : α β E  :
measure_theory.strongly_measurable (λ (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 measure_theory.strongly_measurable.integral_prod_left' {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} [ E] ⦃f : α × β E⦄  :
measure_theory.strongly_measurable (λ (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 measure_theory.measure.integrable_measure_prod_mk_left {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {s : set × β)} (hs : measurable_set s) (h2s : (μ.prod ν) s ) :
measure_theory.integrable (λ (x : α), (ν (prod.mk x ⁻¹' s)).to_real) μ
theorem measure_theory.ae_strongly_measurable.prod_swap {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {γ : Type u_2} {f : β × α γ} (hf : (ν.prod μ)) :
measure_theory.ae_strongly_measurable (λ (z : α × β), f z.swap) (μ.prod ν)
theorem measure_theory.ae_strongly_measurable.fst {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {γ : Type u_2} {f : α γ}  :
measure_theory.ae_strongly_measurable (λ (z : α × β), f z.fst) (μ.prod ν)
theorem measure_theory.ae_strongly_measurable.snd {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {γ : Type u_2} {f : β γ}  :
measure_theory.ae_strongly_measurable (λ (z : α × β), f z.snd) (μ.prod ν)
theorem measure_theory.ae_strongly_measurable.integral_prod_right' {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] ⦃f : α × β E⦄ (hf : (μ.prod ν)) :
measure_theory.ae_strongly_measurable (λ (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 measure_theory.ae_strongly_measurable.prod_mk_left {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {γ : Type u_2} {f : α × β γ} (hf : (μ.prod ν)) :
∀ᵐ (x : α) μ, measure_theory.ae_strongly_measurable (λ (y : β), f (x, y)) ν

### Integrability on a product #

theorem measure_theory.integrable.swap {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α × β E⦄ (hf : (μ.prod ν)) :
(ν.prod μ)
theorem measure_theory.integrable_swap_iff {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α × β E⦄ :
(ν.prod μ) (μ.prod ν)
theorem measure_theory.has_finite_integral_prod_iff {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α × β E⦄  :
(∀ᵐ (x : α) μ, measure_theory.has_finite_integral (λ (y : β), f (x, y)) ν) measure_theory.has_finite_integral (λ (x : α), (y : β), f (x, y) ν) μ
theorem measure_theory.has_finite_integral_prod_iff' {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α × β E⦄ (h1f : (μ.prod ν)) :
(∀ᵐ (x : α) μ, measure_theory.has_finite_integral (λ (y : β), f (x, y)) ν) measure_theory.has_finite_integral (λ (x : α), (y : β), f (x, y) ν) μ
theorem measure_theory.integrable_prod_iff {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α × β E⦄ (h1f : (μ.prod ν)) :
(μ.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α × β E⦄ (h1f : (μ.prod ν)) :
(μ.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_left_ae {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α × β E⦄ (hf : (μ.prod ν)) :
∀ᵐ (y : β) ν, measure_theory.integrable (λ (x : α), f (x, y)) μ
theorem measure_theory.integrable.prod_right_ae {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α × β E⦄ (hf : (μ.prod ν)) :
∀ᵐ (x : α) μ, measure_theory.integrable (λ (y : β), f (x, y)) ν
theorem measure_theory.integrable.integral_norm_prod_left {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α × β E⦄ (hf : (μ.prod ν)) :
measure_theory.integrable (λ (x : α), (y : β), f (x, y) ν) μ
theorem measure_theory.integrable.integral_norm_prod_right {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α × β E⦄ (hf : (μ.prod ν)) :
measure_theory.integrable (λ (y : β), (x : α), f (x, y) μ) ν
theorem measure_theory.integrable_prod_mul {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {L : Type u_2} [is_R_or_C L] {f : α L} {g : β L} (hf : μ) (hg : ν) :
measure_theory.integrable (λ (z : α × β), f z.fst * g z.snd) (μ.prod ν)
theorem measure_theory.integrable.integral_prod_left {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] ⦃f : α × β E⦄ (hf : (μ.prod ν)) :
measure_theory.integrable (λ (x : α), (y : β), f (x, y) ν) μ
theorem measure_theory.integrable.integral_prod_right {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] ⦃f : α × β E⦄ (hf : (μ.prod ν)) :
measure_theory.integrable (λ (y : β), (x : α), f (x, y) μ) ν

### The Bochner integral on a product #

theorem measure_theory.integral_prod_swap {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] (f : α × β E) (hf : (μ.prod ν)) :
(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 measure_theory.integral_fn_integral_add {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] {E' : Type u_7} [complete_space E'] [ E'] ⦃f g : α × β E⦄ (F : E E') (hf : (μ.prod ν)) (hg : (μ.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] {E' : Type u_7} [complete_space E'] [ E'] ⦃f g : α × β E⦄ (F : E E') (hf : (μ.prod ν)) (hg : (μ.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] ⦃f g : α × β E⦄ (F : E ennreal) (hf : (μ.prod ν)) (hg : (μ.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] ⦃f g : α × β E⦄ (hf : (μ.prod ν)) (hg : (μ.prod ν)) :
(x : α), (y : β), f (x, y) + g (x, y) ν μ = (x : α), (y : β), f (x, y) ν μ + (x : α), (y : β), g (x, y) ν μ

theorem measure_theory.integral_integral_add' {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] ⦃f g : α × β E⦄ (hf : (μ.prod ν)) (hg : (μ.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] ⦃f g : α × β E⦄ (hf : (μ.prod ν)) (hg : (μ.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] ⦃f g : α × β E⦄ (hf : (μ.prod ν)) (hg : (μ.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 measure_theory.continuous_integral_integral {α : Type u_1} {β : Type u_3} {E : Type u_6} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E]  :
continuous (λ (f : (μ.prod ν))), (x : α), (y : β), f (x, y) ν μ)

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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] (f : α × β E) (hf : (μ.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] (f : α × β E) (hf : (μ.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] {f : α β E} (hf : (μ.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] {f : α β E} (hf : (μ.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] ⦃f : α β E (hf : (μ.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} [ E] (f : α × β E) {s : set α} {t : set β} (hf : (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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {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 ν