Theorem: Existence of Product Measures

Let $\struct {X, \Sigma_X, \mu}$ and $\struct {Y, \Sigma_Y, \nu}$ be $\sigma$-finite measure spaces.
Then there exists a measure $\rho$ on the product space $\paren {X \times Y, \Sigma_1 \otimes \Sigma_2}$ such that:
:$\forall E_1 \in \Sigma_X, E_2 \in \Sigma_Y: \map \rho {E_1 \times E_2} = \map \mu {E_1} \map \nu {E_2}$
and all such measures are $\sigma$-finite. 
Further, two such measures are given by: 
:$\ds \map {\rho_1} E = \int_X \map \nu {E_x} \rd \mu$
and:
:$\ds \map {\rho_2} E = \int_Y \map \mu {E^y} \rd \nu$
for each $E \in \Sigma_1 \otimes \Sigma_2$.

Proof:
For each $E \in \Sigma_1 \otimes \Sigma_2$ define the function $f_E : X \to \overline \R$ by: 
:$\map {f_E} x = \map \nu {E_x}$
for each $x \in X$. 
Define the function $g_E : Y \to \overline \R$ by: 
:$\map {g_E} y = \map \mu {E^y}$
for each $y \in Y$. 
From Measure of Vertical Section of Measurable Set gives Measurable Function, we have that: 
:$f_E$ is $\Sigma_X$-measurable.
From Measure of Horizontal Section of Measurable Set gives Measurable Function, we have that: 
:$g_E$ is $\Sigma_Y$-measurable.
Note that $f_E \ge 0$ and $g_E \ge 0$ since $\mu \ge 0$ and $\nu \ge 0$. 
We can therefore define the function $\rho_1 : \Sigma_X \otimes \Sigma_Y \to \overline \R$ by: 
:$\ds \map {\rho_1} E = \int_X \map \nu {E_x} \rd \mu$
and the function $\rho_2 : \Sigma_X \otimes \Sigma_Y \to \overline \R$ by: 
:$\ds \map {\rho_2} E = \int_Y \map \mu {E^y} \rd \nu$
for each $E \in \Sigma_X \otimes \Sigma_Y$.
We show that $\rho_1$ and $\rho_2$ are measures. 
We verify each of the conditions $(1)$, $(2)$ and $(3)$ for $\rho_1$ and $\rho_2$.
From the definition of the integral of a positive measurable function, we have that: 
:$\map {\rho_1} E \ge 0$
and:
:$\map {\rho_2} E \ge 0$
for each $E \in \Sigma_X \otimes \Sigma_Y$. 
This verifies $(1)$ for $\rho_1$ and $\rho_2$. 
Let $\sequence {E_n}_{n \mathop \in \N}$ be a sequence of pairwise disjoint $\Sigma_X \otimes \Sigma_Y$-measurable sets.
From Intersection of Vertical Sections is Vertical Section of Intersection and Vertical Section of Measurable Set is Measurable, we have that: 
:$\sequence {\paren {E_n}_x}_{n \mathop \in \N}$ is a sequence of pairwise disjoint $\Sigma_Y$-measurable sets.
From Intersection of Horizontal Sections is Horizontal Section of Intersection and Horizontal Section of Measurable Set is Measurable, we have that: 
:$\sequence {\paren {E_n}^y}_{n \mathop \in \N}$ is a sequence of pairwise disjoint $\Sigma_X$-measurable sets.
We have: 
{{begin-eqn}}
{{eqn	| l = \map {\rho_1} {\bigcup_{n \mathop = 1}^\infty E_n}
		| r = \int_X \map \nu {\paren {\bigcup_{n \mathop = 1}^\infty E_n}_x} \rd \mu
}}
{{eqn	| r = \int_X \map \nu {\bigcup_{n \mathop = 1}^\infty \paren {E_n}_x} \rd \mu
		| c = Union of Vertical Sections is Vertical Section of Union
}}
{{eqn	| r = \int_X \paren {\sum_{n \mathop = 1}^\infty \map \nu {\paren {E_n}_x} } \rd \mu
		| c = since $\nu$ is countably additive
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \paren {\int_X \map \nu {\paren {E_n}_x} \rd \mu}
		| c = Integral of Series of Positive Measurable Functions
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \map {\rho_1} {E_n}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn	| l = \map {\rho_2} {\bigcup_{n \mathop = 1}^\infty E_n}
		| r = \int_Y \map \mu {\paren {\bigcup_{n \mathop = 1}^\infty E_n}^y} \rd \nu
}}
{{eqn	| r = \int_Y \map \mu {\bigcup_{n \mathop = 1}^\infty \paren {E_n}^y} \rd \nu
		| c = Union of Horizontal Sections is Horizontal Section of Union
}}
{{eqn	| r = \int_Y \paren {\sum_{n \mathop = 1}^\infty \map \mu {\paren {E_n}^y} } \rd \nu
		| c = since $\mu$ is countably additive
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \paren {\int_Y \map \mu {\paren {E_n}^y} \rd \nu}
		| c = Integral of Series of Positive Measurable Functions
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \map {\rho_2} {E_n}
}}
{{end-eqn}}
So $\rho_1$ and $\rho_2$ are countably additive.
This verifies $(2)$ for $\rho_1$ and $\rho_2$.
We finally verify $(3)$. 
We have: 
{{begin-eqn}}
{{eqn	| l = \map {\rho_1} \O
		| r = \int_X \map \nu {\O_x} \rd \mu
}}
{{eqn	| r = \int_X \map \nu \O \rd \mu
		| c = Vertical Section of Empty Set
}}
{{eqn	| r = \int_X 0 \rd \mu
		| c = Empty Set is Null Set
}}
{{eqn	| r = 0
		| c = Measurable Function Zero A.E. iff Absolute Value has Zero Integral
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn	| l = \map {\rho_2} \O
		| r = \int_Y \map \mu {\O^y} \rd \nu
}}
{{eqn	| r = \int_Y \map \mu \O \rd \nu
		| c = Horizontal Section of Empty Set
}}
{{eqn	| r = \int_Y 0 \rd \nu
		| c = Empty Set is Null Set
}}
{{eqn	| r = 0
		| c = Measurable Function Zero A.E. iff Absolute Value has Zero Integral
}}
{{end-eqn}}
verifying $(3)$ for $\rho_1$ and $\rho_2$. 
So $\rho_1$ and $\rho_2$ are both measures.
We now show that:
:$\forall E_1 \in \Sigma_X, E_2 \in \Sigma_Y: \map {\rho_1} {E_1 \times E_2} = \map \mu {E_1} \map \nu {E_2}$
and:
:$\forall E_1 \in \Sigma_X, E_2 \in \Sigma_Y: \map {\rho_2} {E_1 \times E_2} = \map \mu {E_1} \map \nu {E_2}$
Let $E_1 \in \Sigma_X$ and $E_2 \in \Sigma_Y$.
We have: 
{{begin-eqn}}
{{eqn	| l = \map {\rho_1} {E_1 \times E_2}
		| r = \int_X \map \nu {\paren {E_1 \times E_2}_x} \rd \mu
}}
{{eqn	| r = \int_X \map \nu {E_2} \chi_{E_1} \rd \mu
		| c = Measure of Vertical Section of Cartesian Product
}}
{{eqn	| r = \map \nu {E_2} \int_X \chi_{E_1} \rd \mu
		| c = Integral of Positive Measurable Function is Positive Homogeneous
}}
{{eqn	| r = \map \mu {E_1} \map \nu {E_2}
		| c = Integral of Characteristic Function: Corollary
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn	| l = \map {\rho_2} {E_1 \times E_2}
		| r = \int_Y \map \mu {\paren {E_1 \times E_2}^y} \rd \nu
}}
{{eqn	| r = \int_Y \map \mu {E_1} \chi_{E_2} \rd \nu
		| c = Measure of Horizontal Section of Cartesian Product
}}
{{eqn	| r = \map \mu {E_1} \int_Y \chi_{E_2} \rd \nu
		| c = Integral of Positive Measurable Function is Positive Homogeneous
}}
{{eqn	| r = \map \mu {E_1} \map \nu {E_2}
		| c = Integral of Characteristic Function: Corollary
}}
{{end-eqn}}
giving the demand for both $\rho_1$ and $\rho_2$. 
Finally, we show that any measure $\rho$ satsfiying:
:$\forall E_1 \in \Sigma_X, E_2 \in \Sigma_Y: \map \rho {E_1 \times E_2} = \map \mu {E_1} \map \nu {E_2}$
is $\sigma$-finite.
Since $\struct {X, \Sigma_X, \mu}$ and $\struct {Y, \Sigma_Y, \nu}$ are $\sigma$-finite measure spaces, we have: 
:$\mu$ and $\nu$ are $\sigma$-finite measures on $X$ and $Y$ respectively. 
Since $\mu$ is $\sigma$-finite, there exists a sequence of $\Sigma_X$-measurable sets $\sequence {E_n}_{n \mathop \in \N}$ such that: 
:$\ds X = \bigcup_{n \mathop = 1}^\infty E_n$
with: 
:$\map \mu {E_n} < \infty$ for each $n$.
Since $\nu$ is $\sigma$-finite, there exists a sequence of $\Sigma_Y$-measurable sets $\sequence {F_n}_{n \mathop \in \N}$ such that: 
:$\ds Y = \bigcup_{n \mathop = 1}^\infty F_n$
with: 
:$\map \mu {F_n} < \infty$ for each $n$.
We then have: 
{{begin-eqn}}
{{eqn	| l = X \times Y
		| r = \paren {\bigcup_{n \mathop = 1}^\infty E_n} \times \paren {\bigcup_{n \mathop = 1}^\infty F_n}
}}
{{eqn	| r = \bigcup_{\tuple {n, m} \in \N \times \N} \paren {E_n \times F_m}
		| c = Cartesian Product of Unions: General Result
}}
{{end-eqn}}
Since $E_n \in \Sigma_X$ and $F_m \in \Sigma_Y$, we have: 
:$E_n \times F_m \in \Sigma_X \otimes \Sigma_Y$
for each $n, m$. 
For each $n, m$, we also have: 
:$\map {\rho} {E_n \times F_m} = \map {\mu_X} {E_n} \map {\mu_Y} {F_m} < \infty$
From Cartesian Product of Countable Sets is Countable, we have that: 
:$\N \times \N$ is countable.
So:
:$\ds \bigcup_{\tuple {n, m} \in \N \times \N} \paren {E_n \times F_m}$ is the countable union of $\Sigma_X \otimes \Sigma_Y$-measurable sets with $\map {\rho} {E_n \times F_m} < \infty$ for each $n, m$. 
Hence: 
:$\rho$ is $\sigma$-finite
completing the proof.
{{qed}}