Integration with respect to the product measure #
In this file we prove Fubini's theorem.
Main results #
MeasureTheory.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.
MeasureTheory.integral_prod: Fubini's theorem. It states that for an 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 (seeMeasureTheory.lintegral_prod). The lemmaMeasureTheory.Integrable.integral_prod_rightstates that the inner integral of the right-hand side is integrable.MeasureTheory.integral_integral_swap_of_hasCompactSupport: a version of Fubini theorem for continuous functions with compact support, which does not assume that the measures are σ-finite contrary to all the usual versions of Fubini.
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
measurableSet_integrable
{α : Type u_1}
{β : Type u_3}
{E : Type u_6}
[MeasurableSpace α]
[MeasurableSpace β]
{ν : MeasureTheory.Measure β}
[NormedAddCommGroup E]
[MeasureTheory.SigmaFinite ν]
⦃f : α → β → E⦄
(hf : MeasureTheory.StronglyMeasurable (Function.uncurry f))
:
MeasurableSet {x : α | MeasureTheory.Integrable (f x) ν}
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 (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.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.
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 (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.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) μ
theorem
MeasureTheory.AEStronglyMeasurable.prod_swap
{α : Type u_1}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{γ : Type u_7}
[TopologicalSpace γ]
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
{f : β × α → γ}
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.prod ν μ))
:
MeasureTheory.AEStronglyMeasurable (fun (z : α × β) => f (Prod.swap z)) (MeasureTheory.Measure.prod μ ν)
theorem
MeasureTheory.AEStronglyMeasurable.fst
{α : Type u_1}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{γ : Type u_7}
[TopologicalSpace γ]
[MeasureTheory.SigmaFinite ν]
{f : α → γ}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.AEStronglyMeasurable (fun (z : α × β) => f z.1) (MeasureTheory.Measure.prod μ ν)
theorem
MeasureTheory.AEStronglyMeasurable.snd
{α : Type u_1}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{γ : Type u_7}
[TopologicalSpace γ]
[MeasureTheory.SigmaFinite ν]
{f : β → γ}
(hf : MeasureTheory.AEStronglyMeasurable f ν)
:
MeasureTheory.AEStronglyMeasurable (fun (z : α × β) => f z.2) (MeasureTheory.Measure.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.SigmaFinite ν]
[NormedSpace ℝ E]
⦃f : α × β → E⦄
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.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.SigmaFinite ν]
[TopologicalSpace γ]
{f : α × β → γ}
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.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.SigmaFinite ν]
[MeasureTheory.SigmaFinite μ]
{f : α × β → E}
:
MeasureTheory.Integrable (f ∘ Prod.swap) (MeasureTheory.Measure.prod ν μ) ↔ MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν)
theorem
MeasureTheory.Integrable.swap
{α : 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 μ ν))
:
MeasureTheory.Integrable (f ∘ Prod.swap) (MeasureTheory.Measure.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.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.integral_norm_prod_right
{α : 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 μ ν))
:
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.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) ∂ν) μ
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.SigmaFinite ν]
[NormedSpace ℝ E]
[MeasureTheory.SigmaFinite μ]
⦃f : α × β → E⦄
(hf : MeasureTheory.Integrable f (MeasureTheory.Measure.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.SigmaFinite ν]
[NormedSpace ℝ E]
[MeasureTheory.SigmaFinite μ]
(f : α × β → E)
:
∫ (z : β × α), f (Prod.swap z) ∂MeasureTheory.Measure.prod ν μ = ∫ (z : α × β), f z ∂MeasureTheory.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 : E → E')
(hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν))
(hg : MeasureTheory.Integrable g (MeasureTheory.Measure.prod μ ν))
:
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 : E → E')
(hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν))
(hg : MeasureTheory.Integrable g (MeasureTheory.Measure.prod μ ν))
:
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 : E → ENNReal)
(hf : MeasureTheory.Integrable f (MeasureTheory.Measure.prod μ ν))
(hg : MeasureTheory.Integrable g (MeasureTheory.Measure.prod μ ν))
:
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 μ ν))
:
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 μ ν))
:
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 μ ν))
:
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 μ ν))
:
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 z ∂MeasureTheory.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 z ∂MeasureTheory.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.2 ∂MeasureTheory.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.1 ∂MeasureTheory.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 z ∂MeasureTheory.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.2 ∂MeasureTheory.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.2 ∂MeasureTheory.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 β)
:
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.2 ∂MeasureTheory.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.1 ∂MeasureTheory.Measure.prod μ ν = (↑↑ν Set.univ).toReal • ∫ (x : α), f x ∂μ
theorem
MeasureTheory.integral_integral_swap_of_hasCompactSupport
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{X : Type u_8}
{Y : Type u_9}
[TopologicalSpace X]
[TopologicalSpace Y]
[MeasurableSpace X]
[MeasurableSpace Y]
[OpensMeasurableSpace X]
[OpensMeasurableSpace Y]
{f : X → Y → E}
(hf : Continuous (Function.uncurry f))
(h'f : HasCompactSupport (Function.uncurry f))
{μ : MeasureTheory.Measure X}
{ν : MeasureTheory.Measure Y}
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
[MeasureTheory.IsFiniteMeasureOnCompacts ν]
:
∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν
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.