----
> [!definition] Definition. ([[product measure]])
> Suppose $(X, \Sigma, \mu)$ and $(Y, \mathcal{T}, \nu)$ are [[finite measure|σ-finite]] [[measure|measure spaces]]. There exists a unique measure $\mu \times \nu$ on $(X \times Y, \Sigma \otimes \mathcal{T})$ with the property that $(\mu \times \nu)(E \times F)=\mu(E)\nu(F)$. Explicitly, we define [[product of σ-algebras|a]] [[measure]] $\mu \times \nu$ [[σ-algebra|on]] $(X \times Y, \Sigma \otimes \mathcal{T})$ via $E \mapsto \int _{X} \int _{Y} \, \chi_{E} (x, y) \, d\nu (y) \, d\mu(x) .$
> This iterated [[integral]] is well-defined:
> - The inner integral equals $\nu([E]_{x})$, [[integral#^equivalence|which makes sense]] since $[E]_{x}$ is [[σ-algebra|measurable]] as the [[product of σ-algebras|cross section of a measurable set]];
> - The outer integral is of $x \mapsto \nu([E]_{x})$, and this makes sense by [[measure of cross section is a measurable function]].
> [!generalization]
> - [[transition kernel|semidirect product of measures]]
^generalization
> [!justification]
>
> We need to check that the product $\mu \times \nu$ of two measures is indeed a [[measure]]. Clearly $(\mu \times \nu)(\emptyset)=0$. Suppose $E_{1},E_{2},\dots$ is a disjoint [[sequence]] of sets in $\Sigma \otimes \mathcal{T}$. Then countable additivity holds because $\begin{align}
> (\mu \times \nu)(\bigsqcup_{k=1}^{\infty} E_{k}) &= \int _{X} \nu ([\bigsqcup_{k=1}^{\infty} E_{k}]_{x}) \, d\mu (x) \\
> &= \int _{X} \nu ( \bigsqcup_{k=1}^{\infty} [E_{k}]_{x})\, d\mu (x) \\
> &= \int _{X} \sum_{k=1}^{\infty} \nu([E_{k}]_{x}) \, d\mu (x) \\
> &= \sum_{k=1}^{\infty} \int _{X} \nu ([E_{k}]_{x}) \, d\mu (x) \\
> &= \sum_{k=1}^{\infty} (\mu \times \nu) (E_{k})
> \end{align}$
> where the fourth equality follows from the [[monotone convergence theorem for nonnegative measurable functions|monotone convergence theorem]].
----
####
----
#### References
> [!backlink]
> ```dataview
> TABLE rows.file.link as "Further Reading"
> FROM [[]]
> FLATTEN file.tags as Tag
> WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom"
> GROUP BY Tag
> ```
> [!frontlink]
> ```dataview
> TABLE rows.file.link as "Further Reading"
> FROM outgoing([[]])
> FLATTEN file.tags as Tag
> WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom"
> GROUP BY Tag
> ```