# mathlib3documentation

measure_theory.constructions.prod.basic

# The product measure #

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

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 ×ˢ 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.

## Main results #

• measure_theory.measure.prod_apply states μ.prod ν s = ∫⁻ x, ν {y | (x, y) ∈ s} ∂μ for measurable s. measure_theory.measure.prod_apply_symm is the reversed version.
• measure_theory.measure.prod_prod states μ.prod ν (s ×ˢ t) = μ s * ν t for measurable sets s and t.
• 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 called lintegral_lintegral. Both versions have a variant with _symm appended, where the order of integration is reversed. The lemma measurable.lintegral_prod_right' states that the inner integral of the right-hand side is measurable.

## 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 has a different naming scheme, since the version for the uncurried version is reversed.

## Tags #

product measure, 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) :

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} {C : set (set α)} {D : set (set β)} (hC : = _inst_1) (hD : = _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}  :

The product σ-algebra is generated from boxes, i.e. s ×ˢ t for sets s : set α and t : set β.

theorem is_pi_system_prod {α : Type u_1} {β : Type u_3}  :
is_pi_system {s : set α | {t : set β |

Rectangles form a π-system.

theorem measurable_measure_prod_mk_left_finite {α : Type u_1} {β : Type u_3} {ν : measure_theory.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} {ν : measure_theory.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.

theorem measurable_measure_prod_mk_right {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {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} {ν : measure_theory.measure β}  :
measurable (λ (x : α),
theorem measurable.map_prod_mk_right {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α}  :
measurable (λ (y : β), measure_theory.measure.map (λ (x : α), (x, y)) μ)
theorem measurable_embedding.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : measurable_space α} {mβ : measurable_space β} {mγ : measurable_space γ} {mδ : measurable_space δ} {f : α β} {g : γ δ} (hg : measurable_embedding g) (hf : measurable_embedding f) :
measurable_embedding (λ (x : γ × α), (g x.fst, f x.snd))
theorem measurable.lintegral_prod_right' {α : Type u_1} {β : Type u_3} {ν : measure_theory.measure β} {f : α × β ennreal} (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} {ν : measure_theory.measure β} {f : α } (hf : measurable ) :
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} {μ : measure_theory.measure α} {f : α × β ennreal} (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} {μ : measure_theory.measure α} {f : α } (hf : measurable ) :
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.

### The product measure #

@[protected, irreducible]
noncomputable def measure_theory.measure.prod {α : Type u_1} {β : Type u_3} (μ : 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.

Equations
Instances for measure_theory.measure.prod
@[protected, instance]
noncomputable def measure_theory.measure.prod.measure_space {α : Type u_1} {β : Type u_2}  :
Equations
theorem measure_theory.measure.prod_apply {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {s : set × β)} (hs : measurable_set s) :
(μ.prod ν) s = ∫⁻ (x : α), ν (prod.mk x ⁻¹' s) μ
@[simp]
theorem measure_theory.measure.prod_prod {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (s : set α) (t : set β) :
(μ.prod ν) (s ×ˢ t) = μ s * ν t

The product measure of the product of two sets is the product of their measures. Note that we do not need the sets to be measurable.

@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem measure_theory.measure.ae_measure_lt_top {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {s : set × β)} (hs : measurable_set s) (h2s : (μ.prod ν) s ) :
∀ᵐ (x : α) μ, ν (prod.mk x ⁻¹' s) <
theorem measure_theory.measure.measure_prod_null {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {s : set × β)} (hs : measurable_set s) :
(μ.prod ν) s = 0 (λ (x : α), ν (prod.mk x ⁻¹' s)) =ᵐ[μ] 0

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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {s : set × β)} (h : (μ.prod ν) s = 0) :
(λ (x : α), ν (prod.mk x ⁻¹' 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.absolutely_continuous.prod {α : Type u_1} {β : Type u_3} {μ μ' : measure_theory.measure α} {ν ν' : measure_theory.measure β} (h1 : μ.absolutely_continuous μ') (h2 : ν.absolutely_continuous ν') :
(μ.prod ν).absolutely_continuous (μ'.prod ν')
theorem measure_theory.measure.ae_ae_of_ae_prod {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {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.

μ.prod ν has finite spanning sets in rectangles of finite spanning sets.

Equations
@[protected, instance]
theorem measure_theory.measure.prod_eq_generate_from {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {C : set (set α)} {D : set (set β)} (hC : = _inst_1) (hD : = _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 ×ˢ t) = μ s * ν t) :
μ.prod ν = μν

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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {μν : measure_theory.measure × β)} (h : (s : set α) (t : set β), μν (s ×ˢ t) = μ s * ν t) :
μ.prod ν = μν

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} {μ : measure_theory.measure α} {ν : measure_theory.measure β}  :
= ν.prod μ
theorem measure_theory.measure.prod_apply_symm {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {s : set × β)} (hs : measurable_set s) :
(μ.prod ν) s = ∫⁻ (y : β), μ ((λ (x : α), (x, y)) ⁻¹' s) ν
theorem measure_theory.measure.prod_assoc_prod {α : Type u_1} {β : Type u_3} {γ : Type u_5} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {τ : measure_theory.measure γ}  :
= μ.prod (ν.prod τ)

### The product of specific measures #

theorem measure_theory.measure.prod_restrict {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (s : set α) (t : set β) :
(μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)
theorem measure_theory.measure.restrict_prod_eq_prod_univ {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (s : set α) :
(μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ set.univ)
theorem measure_theory.measure.prod_dirac {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} (y : β) :
= measure_theory.measure.map (λ (x : α), (x, y)) μ
theorem measure_theory.measure.dirac_prod {α : Type u_1} {β : Type u_3} {ν : measure_theory.measure β} (x : α) :
theorem measure_theory.measure.dirac_prod_dirac {α : Type u_1} {β : Type u_3} {x : α} {y : β} :
theorem measure_theory.measure.prod_sum {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ι : Type u_2} [finite ι] (ν : ι ) [ (i : ι), ] :
= measure_theory.measure.sum (λ (i : ι), μ.prod (ν i))
theorem measure_theory.measure.sum_prod {α : Type u_1} {β : Type u_3} {ν : measure_theory.measure β} {ι : Type u_2} [finite ι] (μ : ι ) [ (i : ι), ] :
= measure_theory.measure.sum (λ (i : ι), (μ i).prod ν)
theorem measure_theory.measure.prod_add {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (ν' : measure_theory.measure β)  :
μ.prod + ν') = μ.prod ν + μ.prod ν'
theorem measure_theory.measure.add_prod {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (μ' : measure_theory.measure α)  :
+ μ').prod ν = μ.prod ν + μ'.prod ν
@[simp]
theorem measure_theory.measure.zero_prod {α : Type u_1} {β : Type u_3} (ν : measure_theory.measure β) :
0.prod ν = 0
@[simp]
theorem measure_theory.measure.prod_zero {α : Type u_1} {β : Type u_3} (μ : measure_theory.measure α) :
μ.prod 0 = 0
theorem measure_theory.measure.map_prod_map {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_2} {f : α β} {g : γ δ} {μa : measure_theory.measure α} {μc : measure_theory.measure γ} (hfa : measure_theory.sigma_finite ) (hgc : measure_theory.sigma_finite ) (hf : measurable f) (hg : measurable g) :
.prod = (μa.prod μc)
theorem measure_theory.measure_preserving.skew_product {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {μc : measure_theory.measure γ} {μd : measure_theory.measure δ} {f : α β} (hf : μb) {g : α γ δ} (hgm : measurable ) (hg : ∀ᵐ (x : α) μa, μc = μd) :
measure_theory.measure_preserving (λ (p : α × γ), (f p.fst, g p.fst p.snd)) (μa.prod μc) (μb.prod μd)
@[protected]
theorem measure_theory.measure_preserving.prod {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {μc : measure_theory.measure γ} {μd : measure_theory.measure δ} {f : α β} {g : γ δ} (hf : μb) (hg : μd) :
(μa.prod μc) (μb.prod μd)

If f : α → β sends the measure μa to μb and g : γ → δ sends the measure μc to μd, then prod.map f g sends μa.prod μc to μb.prod μd.

theorem measure_theory.quasi_measure_preserving.prod_of_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α × β γ} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {τ : measure_theory.measure γ} (hf : measurable f) (h2f : ∀ᵐ (x : α) μ, measure_theory.measure.quasi_measure_preserving (λ (y : β), f (x, y)) ν τ) :
theorem measure_theory.quasi_measure_preserving.prod_of_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β γ} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {τ : measure_theory.measure γ} (hf : measurable f) (h2f : ∀ᵐ (y : β) ν, measure_theory.measure.quasi_measure_preserving (λ (x : α), f (x, y)) μ τ) :
theorem ae_measurable.prod_swap {α : Type u_1} {β : Type u_3} {γ : Type u_5} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : β × α γ} (hf : (ν.prod μ)) :
ae_measurable (λ (z : α × β), f z.swap) (μ.prod ν)
theorem ae_measurable.fst {α : Type u_1} {β : Type u_3} {γ : Type u_5} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α γ} (hf : μ) :
ae_measurable (λ (z : α × β), f z.fst) (μ.prod ν)
theorem ae_measurable.snd {α : Type u_1} {β : Type u_3} {γ : Type u_5} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : β γ} (hf : ν) :
ae_measurable (λ (z : α × β), f z.snd) (μ.prod ν)

### The Lebesgue integral on a product #

theorem measure_theory.lintegral_prod_swap {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (f : α × β ennreal) (hf : (μ.prod ν)) :
∫⁻ (z : β × α), f z.swap ν.prod μ = ∫⁻ (z : α × β), f z μ.prod ν
theorem measure_theory.lintegral_prod_of_measurable {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (f : α × β ennreal) (hf : measurable f) :
∫⁻ (z : α × β), f z μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ν μ

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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (f : α × β ennreal) (hf : (μ.prod ν)) :
∫⁻ (z : α × β), f z μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ν μ

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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (f : α × β ennreal) (hf : (μ.prod ν)) :
∫⁻ (z : α × β), f z μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) μ ν

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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (f : α × β ennreal) (hf : measurable f) :
∫⁻ (z : α × β), f z μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) μ ν

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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α (hf : (μ.prod ν)) :
∫⁻ (x : α), ∫⁻ (y : β), f x y ν μ = ∫⁻ (z : α × β), f z.fst z.snd μ.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α (hf : (μ.prod ν)) :
∫⁻ (x : α), ∫⁻ (y : β), f x y ν μ = ∫⁻ (z : β × α), f z.snd z.fst ν.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} {μ : measure_theory.measure α} {ν : measure_theory.measure β} ⦃f : α (hf : (μ.prod ν)) :
∫⁻ (x : α), ∫⁻ (y : β), f x y ν μ = ∫⁻ (y : β), ∫⁻ (x : α), f x y μ ν

Change the order of Lebesgue integration.

theorem measure_theory.lintegral_prod_mul {α : Type u_1} {β : Type u_3} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α ennreal} {g : β ennreal} (hf : μ) (hg : ν) :
∫⁻ (z : α × β), f z.fst * g z.snd μ.prod ν = ∫⁻ (x : α), f x μ * ∫⁻ (y : β), g y ν

### Marginals of a measure defined on a product #

noncomputable def measure_theory.measure.fst {α : Type u_1} {β : Type u_3} (ρ : measure_theory.measure × β)) :

Marginal measure on α obtained from a measure ρ on α × β, defined by ρ.map prod.fst.

Equations
Instances for measure_theory.measure.fst
theorem measure_theory.measure.fst_apply {α : Type u_1} {β : Type u_3} {ρ : measure_theory.measure × β)} {s : set α} (hs : measurable_set s) :
(ρ.fst) s = ρ (prod.fst ⁻¹' s)
theorem measure_theory.measure.fst_univ {α : Type u_1} {β : Type u_3} {ρ : measure_theory.measure × β)} :
@[protected, instance]
@[protected, instance]
theorem measure_theory.measure.fst_map_prod_mk₀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {X : α β} {Y : α γ} {μ : measure_theory.measure α} (hX : μ) (hY : μ) :
(measure_theory.measure.map (λ (a : α), (X a, Y a)) μ).fst =
theorem measure_theory.measure.fst_map_prod_mk {α : Type u_1} {β : Type u_3} {γ : Type u_5} {X : α β} {Y : α γ} {μ : measure_theory.measure α} (hX : measurable X) (hY : measurable Y) :
(measure_theory.measure.map (λ (a : α), (X a, Y a)) μ).fst =
noncomputable def measure_theory.measure.snd {α : Type u_1} {β : Type u_3} (ρ : measure_theory.measure × β)) :

Marginal measure on β obtained from a measure on ρ α × β, defined by ρ.map prod.snd.

Equations
Instances for measure_theory.measure.snd
theorem measure_theory.measure.snd_apply {α : Type u_1} {β : Type u_3} {ρ : measure_theory.measure × β)} {s : set β} (hs : measurable_set s) :
(ρ.snd) s = ρ (prod.snd ⁻¹' s)
theorem measure_theory.measure.snd_univ {α : Type u_1} {β : Type u_3} {ρ : measure_theory.measure × β)} :
@[protected, instance]
@[protected, instance]
theorem measure_theory.measure.snd_map_prod_mk₀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {X : α β} {Y : α γ} {μ : measure_theory.measure α} (hX : μ) (hY : μ) :
(measure_theory.measure.map (λ (a : α), (X a, Y a)) μ).snd =
theorem measure_theory.measure.snd_map_prod_mk {α : Type u_1} {β : Type u_3} {γ : Type u_5} {X : α β} {Y : α γ} {μ : measure_theory.measure α} (hX : measurable X) (hY : measurable Y) :
(measure_theory.measure.map (λ (a : α), (X a, Y a)) μ).snd =