Is there a formula for the Haar measure on a product of groups? Let $ (G_{n})_{n \in \mathbb{N}} $ be a sequence of locally compact topological groups with a corresponding sequence $ (\mu_{n})_{n \in \mathbb{N}} $ of Haar measures. Is there a way to construct a Haar measure on the product group $ \displaystyle \prod_{n \in \mathbb{N}} G_{n} $ using $ (\mu_{n})_{n \in \mathbb{N}} $? Is the task easier if the product is finite, or if all of the $ G_{n} $’s are compact?
 A: I only have the answer for the case of finite products, and I am definitely looking forward to seeing a proof of the general case by anyone from the MSE community.
In what follows, all topological groups are assumed to be $ T_{1} $-spaces, which automatically makes them Hausdorff spaces. (In general, $ T_{1} $-spaces are not Hausdorff.)
Recall that a Haar measure on a locally compact topological group $ G $ is defined as a regular Borel measure on $ G $ that is left-invariant and that is finite on compact subsets of $ G $.
Note: A Borel measure on a topological space $ X $ is said to be regular if and only if each Borel-measurable subset of $ X $ is outer open-regular (i.e., it can be approximated in measure arbitrarily closely by its open supersets) and each open subset of $ X $ is inner compact-regular (i.e., it can be approximated in measure arbitrarily closely by its compact subsets).
Let $ G_{1},\ldots,G_{n} $ be locally compact topological groups with respective Haar measures $ \mu_{1},\ldots,\mu_{n} $. Observe that $ G := G_{1} \times \cdots \times G_{n} $ is indeed locally compact (if this were not so, then it would be pointless to continue this discussion).
Define a non-negative linear functional $ \Phi $ on $ {C_{c}}(G) $ as an iterated integral in the following manner:
$$
\forall F \in {C_{c}}(G): \quad
\Phi(F)
\stackrel{\text{def}}{=}
\int_{G_{1}} \cdots \int_{G_{n}} F ~ \mathrm{d}{\mu_{1}} \cdots \mathrm{d}{\mu_{n}}.
$$
One can show, using a simple approximation argument and without invoking Fubini’s Theorem, that permuting the order of appearance of the $ G_{i} $’s in the definition of $ \Phi $ does not result in any changes. More precisely, for any permutation $ \sigma: [n] \to [n] $, we have
$$
\forall F \in {C_{c}}(G): \quad
  \Phi(F)
= \int_{G_{\sigma(1)}} \cdots \int_{G_{\sigma(n)}}
  F ~ \mathrm{d}{\mu_{\sigma(1)}} \cdots \mathrm{d}{\mu_{\sigma(n)}}.
$$
By the Riesz Representation Theorem (as presented in Walter Rudin’s Real and Complex Analysis), there exists a regular Borel measure $ \mu $ on $ G $ that is finite on compact subsets of $ G $ and satisfies
$$
\forall F \in {C_{c}}(G): \quad
\Phi(F) = \int_{G} F ~ \mathrm{d}{\mu}.
$$
As $ \Phi $ is left-invariant, it follows that $ \mu $ is also left-invariant. Hence, $ \mu $ qualifies as a Haar measure on $ G $. To prove that
$$
(\spadesuit) \quad
\forall F \in {L^{1}}(G,\mu): \quad
  \int_{G} F ~ \mathrm{d}{\mu}
= \int_{G_{\sigma(1)}} \cdots \int_{G_{\sigma(n)}}
  F ~ \mathrm{d}{\mu_{\sigma(1)}} \cdots \mathrm{d}{\mu_{\sigma(n)}}
$$
for any permutation $ \sigma: [n] \to [n] $, we have to invoke Fubini’s Theorem (presented in the form of Theorem 13.8 of Edwin Hewitt’s and Kenneth A. Ross’ Abstract Harmonic Analysis. Volume 1 - Structure of Topological Groups. Integration Theory. Group Representations. Second Edition) this time.
Conclusion: As a Haar measure is unique up to scaling by a positive factor, it follows that $ \mu $ is the unique Haar measure on $ G $ that satisfies $ (\spadesuit) $.
