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_iffstates that a binary function is integrable iff bothy ↦ f (x, y)is integrable for almost everyx, and- the function
x ↦ ∫ ‖f (x, y)‖ dyis integrable.
measure_theory.integral_prod: Fubini's theorem. It states that for a integrable functionα × β → E(whereEis 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 (seemeasure_theory.lintegral_prod). The lemmameasure_theory.integrable.integral_prod_rightstates 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}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[normed_add_comm_group E]
[measure_theory.sigma_finite ν]
⦃f : α → β → E⦄
(hf : measure_theory.strongly_measurable (function.uncurry f)) :
measurable_set {x : α | measure_theory.integrable (f x) ν}
theorem
measure_theory.strongly_measurable.integral_prod_right
{α : Type u_1}
{β : Type u_3}
{E : Type u_6}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
[measure_theory.sigma_finite ν]
⦃f : α → β → E⦄
(hf : measure_theory.strongly_measurable (function.uncurry f)) :
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}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
[measure_theory.sigma_finite ν]
⦃f : α × β → E⦄
(hf : measure_theory.strongly_measurable f) :
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}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
[measure_theory.sigma_finite μ]
⦃f : α → β → E⦄
(hf : measure_theory.strongly_measurable (function.uncurry f)) :
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}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
[measure_theory.sigma_finite μ]
⦃f : α × β → E⦄
(hf : measure_theory.strongly_measurable f) :
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}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
{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}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
{γ : Type u_2}
[topological_space γ]
[measure_theory.sigma_finite μ]
[measure_theory.sigma_finite ν]
{f : β × α → γ}
(hf : measure_theory.ae_strongly_measurable f (ν.prod μ)) :
measure_theory.ae_strongly_measurable (λ (z : α × β), f z.swap) (μ.prod ν)
theorem
measure_theory.ae_strongly_measurable.fst
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
{γ : Type u_2}
[topological_space γ]
[measure_theory.sigma_finite ν]
{f : α → γ}
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.ae_strongly_measurable (λ (z : α × β), f z.fst) (μ.prod ν)
theorem
measure_theory.ae_strongly_measurable.snd
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
{γ : Type u_2}
[topological_space γ]
[measure_theory.sigma_finite ν]
{f : β → γ}
(hf : measure_theory.ae_strongly_measurable 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}
[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]
⦃f : α × β → E⦄
(hf : measure_theory.ae_strongly_measurable f (μ.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}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
{γ : Type u_2}
[measure_theory.sigma_finite ν]
[topological_space γ]
{f : α × β → γ}
(hf : measure_theory.ae_strongly_measurable f (μ.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}
[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⦄
(hf : measure_theory.integrable f (μ.prod ν)) :
measure_theory.integrable (f ∘ prod.swap) (ν.prod μ)
theorem
measure_theory.integrable_swap_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⦄ :
measure_theory.integrable (f ∘ prod.swap) (ν.prod μ) ↔ measure_theory.integrable f (μ.prod ν)
theorem
measure_theory.has_finite_integral_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.strongly_measurable f) :
measure_theory.has_finite_integral f (μ.prod ν) ↔ (∀ᵐ (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}
[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.has_finite_integral f (μ.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}
[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_left_ae
{α : 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⦄
(hf : measure_theory.integrable f (μ.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}
[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⦄
(hf : measure_theory.integrable f (μ.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}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[normed_add_comm_group E]
[measure_theory.sigma_finite ν]
⦃f : α × β → E⦄
(hf : measure_theory.integrable f (μ.prod ν)) :
theorem
measure_theory.integrable.integral_norm_prod_right
{α : 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⦄
(hf : measure_theory.integrable f (μ.prod ν)) :
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 ν) :
theorem
measure_theory.integrable.integral_prod_left
{α : 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]
⦃f : α × β → E⦄
(hf : measure_theory.integrable f (μ.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}
[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 ν)) :
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}
[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.ae_strongly_measurable f (μ.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}
[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 ν)) :
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 ν)) :
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 ν)) :
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 ν)) :
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 ν)) :
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 ν)) :
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 ν)) :
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}
[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 μ] :
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 ν)) :
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 ν)) :
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 ν)) :
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 ν)) :
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 ν)) :
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 ν)) :
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) :
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 β) :