The product measure #
In this file we define and prove properties about the binary product measure. If α and β have
σ-finite measures μ resp. ν then α × β can be equipped with a σ-finite measure μ.prod ν that
satisfies (μ.prod ν) s = ∫⁻ x, ν {y | (x, y) ∈ s} ∂μ.
We also have (μ.prod ν) (s.prod t) = μ s * ν t, i.e. the measure of a rectangle is the product of
the measures of the sides.
We also prove Tonelli's theorem and Fubini's theorem.
Main definition #
measure_theory.measure.prod: The product of two measures.
Main results #
measure_theory.measure.prod_applystatesμ.prod ν s = ∫⁻ x, ν {y | (x, y) ∈ s} ∂μfor measurables.measure_theory.measure.prod_apply_symmis the reversed version.measure_theory.measure.prod_prodstatesμ.prod ν (s.prod t) = μ s * ν tfor measurable setssandt.measure_theory.lintegral_prod: Tonelli's theorem. It states that for a measurable functionα × β → ℝ≥0∞we have∫⁻ z, f z ∂(μ.prod ν) = ∫⁻ x, ∫⁻ y, f (x, y) ∂ν ∂μ. The version for functionsα → β → ℝ≥0∞is reversed, and calledlintegral_lintegral. Both versions have a variant with_symmappended, where the order of integration is reversed. The lemmameasurable.lintegral_prod_right'states that the inner integral of the right-hand side is measurable.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. The lemmameasure_theory.integrable.integral_prod_rightstates that the inner integral of the right-hand side is integrable.
Implementation Notes #
Many results are proven twice, once for functions in curried form (α → β → γ) and one for
functions in uncurried form (α × β → γ). The former often has an assumption
measurable (uncurry f), which could be inconvenient to discharge, but for the latter it is more
common that the function has to be given explicitly, since Lean cannot synthesize the function by
itself. We name the lemmas about the uncurried form with a prime.
Tonelli's theorem and Fubini's theorem have a different naming scheme, since the version for the
uncurried version is reversed.
Tags #
product measure, Fubini's theorem, Tonelli's theorem, Fubini-Tonelli theorem
theorem
is_pi_system.prod
{α : Type u_1}
{β : Type u_3}
{C : set (set α)}
{D : set (set β)}
(hC : is_pi_system C)
(hD : is_pi_system D) :
is_pi_system (set.image2 set.prod C D)
Rectangles formed by π-systems form a π-system.
theorem
is_countably_spanning.prod
{α : Type u_1}
{β : Type u_3}
{C : set (set α)}
{D : set (set β)}
(hC : is_countably_spanning C)
(hD : is_countably_spanning D) :
Rectangles of countably spanning sets are countably spanning.
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
generate_from_prod_eq
{α : Type u_1}
{β : Type u_2}
{C : set (set α)}
{D : set (set β)}
(hC : is_countably_spanning C)
(hD : is_countably_spanning D) :
The product of generated σ-algebras is the one generated by rectangles, if both generating sets are countably spanning.
theorem
generate_from_eq_prod
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{C : set (set α)}
{D : set (set β)}
(hC : measurable_space.generate_from C = _inst_1)
(hD : measurable_space.generate_from D = _inst_3)
(h2C : is_countably_spanning C)
(h2D : is_countably_spanning D) :
If C and D generate the σ-algebras on α resp. β, then rectangles formed by C and D
generate the σ-algebra on α × β.
theorem
generate_from_prod
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β] :
measurable_space.generate_from (set.image2 set.prod {s : set α | measurable_set s} {t : set β | measurable_set t}) = prod.measurable_space
The product σ-algebra is generated from boxes, i.e. s.prod t for sets s : set α and
t : set β.
theorem
is_pi_system_prod
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β] :
is_pi_system (set.image2 set.prod {s : set α | measurable_set s} {t : set β | measurable_set t})
Rectangles form a π-system.
theorem
measurable_measure_prod_mk_left_finite
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[measure_theory.finite_measure ν]
{s : set (α × β)}
(hs : measurable_set s) :
measurable (λ (x : α), ⇑ν (prod.mk x ⁻¹' s))
If ν is a finite measure, and s ⊆ α × β is measurable, then x ↦ ν { y | (x, y) ∈ s } is
a measurable function. measurable_measure_prod_mk_left is strictly more general.
theorem
measurable_measure_prod_mk_left
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
{s : set (α × β)}
(hs : measurable_set s) :
measurable (λ (x : α), ⇑ν (prod.mk x ⁻¹' s))
If ν is a σ-finite measure, and s ⊆ α × β is measurable, then x ↦ ν { y | (x, y) ∈ s } is
a measurable function.
theorem
measurable_measure_prod_mk_right
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[measure_theory.sigma_finite μ]
{s : set (α × β)}
(hs : measurable_set s) :
measurable (λ (y : β), ⇑μ ((λ (x : α), (x, y)) ⁻¹' s))
If μ is a σ-finite measure, and s ⊆ α × β is measurable, then y ↦ μ { x | (x, y) ∈ s } is
a measurable function.
theorem
measurable.map_prod_mk_left
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν] :
measurable (λ (x : α), ⇑(measure_theory.measure.map (prod.mk x)) ν)
theorem
measurable.map_prod_mk_right
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[measure_theory.sigma_finite μ] :
measurable (λ (y : β), ⇑(measure_theory.measure.map (λ (x : α), (x, y))) μ)
theorem
measurable.lintegral_prod_right'
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
{f : α × β → ℝ≥0∞}
(hf : measurable f) :
measurable (λ (x : α), ∫⁻ (y : β), f (x, y) ∂ν)
The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of) Tonelli's theorem is measurable.
theorem
measurable.lintegral_prod_right
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
{f : α → β → ℝ≥0∞}
(hf : measurable (function.uncurry f)) :
measurable (λ (x : α), ∫⁻ (y : β), f x y ∂ν)
The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of)
Tonelli's theorem is measurable.
This version has the argument f in curried form.
theorem
measurable.lintegral_prod_left'
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[measure_theory.sigma_finite μ]
{f : α × β → ℝ≥0∞}
(hf : measurable f) :
measurable (λ (y : β), ∫⁻ (x : α), f (x, y) ∂μ)
The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of) the symmetric version of Tonelli's theorem is measurable.
theorem
measurable.lintegral_prod_left
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[measure_theory.sigma_finite μ]
{f : α → β → ℝ≥0∞}
(hf : measurable (function.uncurry f)) :
measurable (λ (y : β), ∫⁻ (x : α), f x y ∂μ)
The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of)
the symmetric version of Tonelli's theorem is measurable.
This version has the argument f in curried form.
theorem
measurable_set_integrable
{α : Type u_1}
{β : Type u_3}
{E : Type u_6}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[normed_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[opens_measurable_space E]
⦃f : α → β → E⦄
(hf : measurable (function.uncurry f)) :
measurable_set {x : α | measure_theory.integrable (f x) ν}
theorem
measurable.integral_prod_right
{α : Type u_1}
{β : Type u_3}
{E : Type u_6}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[normed_group E]
[measurable_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_space E]
[measure_theory.sigma_finite ν]
⦃f : α → β → E⦄
(hf : measurable (function.uncurry f)) :
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
measurable.integral_prod_right'
{α : Type u_1}
{β : Type u_3}
{E : Type u_6}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[normed_group E]
[measurable_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_space E]
[measure_theory.sigma_finite ν]
⦃f : α × β → E⦄
(hf : measurable f) :
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
measurable.integral_prod_left
{α : Type u_1}
{β : Type u_3}
{E : Type u_6}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[normed_group E]
[measurable_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_space E]
[measure_theory.sigma_finite μ]
⦃f : α → β → E⦄
(hf : measurable (function.uncurry f)) :
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
measurable.integral_prod_left'
{α : Type u_1}
{β : Type u_3}
{E : Type u_6}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[normed_group E]
[measurable_space E]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_space E]
[measure_theory.sigma_finite μ]
⦃f : α × β → E⦄
(hf : measurable f) :
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 #
@[protected]
def
measure_theory.measure.prod
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
(μ : measure_theory.measure α)
(ν : measure_theory.measure β) :
measure_theory.measure (α × β)
The binary product of measures. They are defined for arbitrary measures, but we basically prove all properties under the assumption that at least one of them is σ-finite.
@[protected, instance]
def
measure_theory.measure.prod.measure_space
{α : Type u_1}
{β : Type u_2}
[measure_theory.measure_space α]
[measure_theory.measure_space β] :
theorem
measure_theory.measure.prod_apply
{α : 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) :
@[simp]
theorem
measure_theory.measure.prod_prod
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
{s : set α}
{t : set β}
(hs : measurable_set s)
(ht : measurable_set t) :
theorem
measure_theory.measure.prod_prod_le
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
(s : set α)
(t : set β) :
If we don't assume measurability of s and t, we can bound the measure of their product.
theorem
measure_theory.measure.ae_measure_lt_top
{α : 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 < ⊤) :
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.measure.measure_prod_null
{α : 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) :
Note: the assumption hs cannot be dropped. For a counterexample, see
Walter Rudin Real and Complex Analysis, example (c) in section 8.9.
theorem
measure_theory.measure.measure_ae_null_of_prod_null
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
{s : set (α × β)}
(h : ⇑(μ.prod ν) s = 0) :
Note: the converse is not true without assuming that s is measurable. For a counterexample,
see Walter Rudin Real and Complex Analysis, example (c) in section 8.9.
theorem
measure_theory.measure.ae_ae_of_ae_prod
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
{p : α × β → Prop}
(h : ∀ᵐ (z : α × β) ∂μ.prod ν, p z) :
∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, p (x, y)
Note: the converse is not true. For a counterexample, see Walter Rudin Real and Complex Analysis, example (c) in section 8.9.
def
measure_theory.measure.finite_spanning_sets_in.prod
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
{C : set (set α)}
{D : set (set β)}
(hμ : μ.finite_spanning_sets_in C)
(hν : ν.finite_spanning_sets_in D)
(hC : ∀ (s : set α), s ∈ C → measurable_set s)
(hD : ∀ (t : set β), t ∈ D → measurable_set t) :
(μ.prod ν).finite_spanning_sets_in (set.image2 set.prod C D)
μ.prod ν has finite spanning sets in rectangles of finite spanning sets.
theorem
measure_theory.measure.prod_fst_absolutely_continuous
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν] :
⇑(measure_theory.measure.map prod.fst) (μ.prod ν) ≪ μ
theorem
measure_theory.measure.prod_snd_absolutely_continuous
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν] :
⇑(measure_theory.measure.map prod.snd) (μ.prod ν) ≪ ν
@[protected, instance]
def
measure_theory.measure.prod.sigma_finite
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ] :
theorem
measure_theory.measure.prod_eq_generate_from
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
{C : set (set α)}
{D : set (set β)}
(hC : measurable_space.generate_from C = _inst_1)
(hD : measurable_space.generate_from D = _inst_3)
(h2C : is_pi_system C)
(h2D : is_pi_system D)
(h3C : μ.finite_spanning_sets_in C)
(h3D : ν.finite_spanning_sets_in D)
{μν : measure_theory.measure (α × β)}
(h₁ : ∀ (s : set α), s ∈ C → ∀ (t : set β), t ∈ D → ⇑μν (s.prod t) = (⇑μ s) * ⇑ν t) :
A measure on a product space equals the product measure if they are equal on rectangles with as sides sets that generate the corresponding σ-algebras.
theorem
measure_theory.measure.prod_eq
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ]
{μν : measure_theory.measure (α × β)}
(h : ∀ (s : set α) (t : set β), measurable_set s → measurable_set t → ⇑μν (s.prod t) = (⇑μ s) * ⇑ν t) :
A measure on a product space equals the product measure if they are equal on rectangles.
theorem
measure_theory.measure.prod_swap
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ] :
theorem
measure_theory.measure.prod_apply_symm
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ]
{s : set (α × β)}
(hs : measurable_set s) :
theorem
measure_theory.measure.prod_assoc_prod
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
{τ : measure_theory.measure γ}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ]
[measure_theory.sigma_finite τ] :
⇑(measure_theory.measure.map ⇑measurable_equiv.prod_assoc) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ)
The product of specific measures #
theorem
measure_theory.measure.prod_restrict
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ]
{s : set α}
{t : set β}
(hs : measurable_set s)
(ht : measurable_set t) :
theorem
measure_theory.measure.restrict_prod_eq_prod_univ
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ]
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.measure.prod_dirac
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[measure_theory.sigma_finite μ]
(y : β) :
μ.prod (measure_theory.measure.dirac y) = ⇑(measure_theory.measure.map (λ (x : α), (x, y))) μ
theorem
measure_theory.measure.dirac_prod
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
(x : α) :
(measure_theory.measure.dirac x).prod ν = ⇑(measure_theory.measure.map (prod.mk x)) ν
theorem
measure_theory.measure.dirac_prod_dirac
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{x : α}
{y : β} :
theorem
measure_theory.measure.prod_sum
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
[measure_theory.sigma_finite μ]
{ι : Type u_2}
[fintype ι]
(ν : ι → measure_theory.measure β)
[∀ (i : ι), measure_theory.sigma_finite (ν i)] :
μ.prod (measure_theory.measure.sum ν) = measure_theory.measure.sum (λ (i : ι), μ.prod (ν i))
theorem
measure_theory.measure.sum_prod
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
{ι : Type u_2}
[fintype ι]
(μ : ι → measure_theory.measure α)
[∀ (i : ι), measure_theory.sigma_finite (μ i)] :
(measure_theory.measure.sum μ).prod ν = measure_theory.measure.sum (λ (i : ι), (μ i).prod ν)
theorem
measure_theory.measure.prod_add
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ]
(ν' : measure_theory.measure β)
[measure_theory.sigma_finite ν'] :
theorem
measure_theory.measure.add_prod
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ]
(μ' : measure_theory.measure α)
[measure_theory.sigma_finite μ'] :
@[simp]
theorem
measure_theory.measure.zero_prod
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
(ν : measure_theory.measure β) :
@[simp]
theorem
measure_theory.measure.prod_zero
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
(μ : measure_theory.measure α) :
theorem
measure_theory.measure.map_prod_map
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{δ : Type u_2}
[measurable_space δ]
{f : α → β}
{g : γ → δ}
{μa : measure_theory.measure α}
{μc : measure_theory.measure γ}
(hfa : measure_theory.sigma_finite (⇑(measure_theory.measure.map f) μa))
(hgc : measure_theory.sigma_finite (⇑(measure_theory.measure.map g) μc))
(hf : measurable f)
(hg : measurable g) :
(⇑(measure_theory.measure.map f) μa).prod (⇑(measure_theory.measure.map g) μc) = ⇑(measure_theory.measure.map (prod.map f g)) (μa.prod μc)
theorem
ae_measurable.prod_swap
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite μ]
[measure_theory.sigma_finite ν]
{f : β × α → γ}
(hf : ae_measurable f (ν.prod μ)) :
ae_measurable (λ (z : α × β), f z.swap) (μ.prod ν)
theorem
ae_measurable.fst
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
{f : α → γ}
(hf : ae_measurable f μ) :
ae_measurable (λ (z : α × β), f z.fst) (μ.prod ν)
theorem
ae_measurable.snd
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
{f : β → γ}
(hf : ae_measurable f ν) :
ae_measurable (λ (z : α × β), f z.snd) (μ.prod ν)
theorem
ae_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[borel_space E]
[complete_space E]
⦃f : α × β → E⦄
(hf : ae_measurable f (μ.prod ν)) :
ae_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
ae_measurable.prod_mk_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
{f : α × β → γ}
(hf : ae_measurable f (μ.prod ν)) :
∀ᵐ (x : α) ∂μ, ae_measurable (λ (y : β), f (x, y)) ν
The Lebesgue integral on a product #
theorem
measure_theory.lintegral_prod_swap
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ]
(f : α × β → ℝ≥0∞)
(hf : ae_measurable f (μ.prod ν)) :
theorem
measure_theory.lintegral_prod_of_measurable
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
(f : α × β → ℝ≥0∞)
(hf : measurable f) :
Tonelli's Theorem: For ℝ≥0∞-valued measurable functions on α × β,
the integral of f is equal to the iterated integral.
theorem
measure_theory.lintegral_prod
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
(f : α × β → ℝ≥0∞)
(hf : ae_measurable f (μ.prod ν)) :
Tonelli's Theorem: For ℝ≥0∞-valued almost everywhere measurable functions on α × β,
the integral of f is equal to the iterated integral.
theorem
measure_theory.lintegral_prod_symm'
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ]
(f : α × β → ℝ≥0∞)
(hf : ae_measurable f (μ.prod ν)) :
The symmetric verion of Tonelli's Theorem: For ℝ≥0∞-valued almost everywhere measurable
functions on α × β, the integral of f is equal to the iterated integral, in reverse order.
theorem
measure_theory.lintegral_prod_symm
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ]
(f : α × β → ℝ≥0∞)
(hf : ae_measurable f (μ.prod ν)) :
The symmetric verion of Tonelli's Theorem: For ℝ≥0∞-valued measurable
functions on α × β, the integral of f is equal to the iterated integral, in reverse order.
theorem
measure_theory.lintegral_lintegral
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
⦃f : α → β → ℝ≥0∞⦄
(hf : ae_measurable (function.uncurry f) (μ.prod ν)) :
The reversed version of Tonelli's Theorem. In this version f is in curried form, which makes
it easier for the elaborator to figure out f automatically.
theorem
measure_theory.lintegral_lintegral_symm
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ]
⦃f : α → β → ℝ≥0∞⦄
(hf : ae_measurable (function.uncurry f) (μ.prod ν)) :
The reversed version of Tonelli's Theorem (symmetric version). In this version f is in curried
form, which makes it easier for the elaborator to figure out f automatically.
theorem
measure_theory.lintegral_lintegral_swap
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
[measure_theory.sigma_finite μ]
⦃f : α → β → ℝ≥0∞⦄
(hf : ae_measurable (function.uncurry f) (μ.prod ν)) :
Change the order of Lebesgue integration.
theorem
measure_theory.lintegral_prod_mul
{α : Type u_1}
{β : Type u_3}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
[measure_theory.sigma_finite ν]
{f : α → ℝ≥0∞}
{g : β → ℝ≥0∞}
(hf : ae_measurable f μ)
(hg : ae_measurable g ν) :
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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[opens_measurable_space E]
[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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[opens_measurable_space E]
[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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[opens_measurable_space E]
⦃f : α × β → E⦄
(h1f : 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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[opens_measurable_space E]
⦃f : α × β → E⦄
(h1f : ae_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[opens_measurable_space E]
⦃f : α × β → E⦄
(h1f : ae_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[opens_measurable_space E]
[measure_theory.sigma_finite μ]
⦃f : α × β → E⦄
(h1f : ae_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[opens_measurable_space E]
[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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[opens_measurable_space E]
[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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[opens_measurable_space E]
⦃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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[opens_measurable_space E]
[measure_theory.sigma_finite μ]
⦃f : α × β → E⦄
(hf : measure_theory.integrable f (μ.prod ν)) :
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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_space E]
[measure_theory.sigma_finite μ]
(f : α × β → E)
(hf : ae_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_space E]
[measure_theory.sigma_finite μ]
{E' : Type u_7}
[measurable_space E']
[normed_group E']
[borel_space E']
[complete_space E']
[normed_space ℝ E']
[topological_space.second_countable_topology 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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_space E]
[measure_theory.sigma_finite μ]
{E' : Type u_7}
[measurable_space E']
[normed_group E']
[borel_space E']
[complete_space E']
[normed_space ℝ E']
[topological_space.second_countable_topology 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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_space E]
[measure_theory.sigma_finite μ]
⦃f g : α × β → E⦄
(F : E → ℝ≥0∞)
(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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_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_group E]
[measurable_space E]
[measure_theory.sigma_finite ν]
[topological_space.second_countable_topology E]
[normed_space ℝ E]
[complete_space E]
[borel_space E]
[measure_theory.sigma_finite μ]
⦃f : α → β → E⦄
(hf : measure_theory.integrable (function.uncurry f) (μ.prod ν)) :
Change the order of Bochner integration.