The product measure is characterized by continuous functions

Stream: maths

[Etienne Marion]

Given two finite measure spaces $(X, \mu)$ and $(Y, \nu)$, the product measure $\mu \otimes \nu$ is the only measure $\xi$ such that for any bounded continuous functions $f : X \to \mathbb{R}$ and $g : Y \to \mathbb{R}$, $\int f(z.1) * g(z.2) \xi(\mathrm dz) = \int f(x) \mu(\mathrm dx) \times \int g(y) \nu(\mathrm dy)$. Using HasOuterApproxClosed I managed to formalize this in the case where $X$ and $Y$ are Borel spaces and one of them is second-countable (so that $X \times Y$ is also a Borel space), but I am wondering if this is true under more general assumptions. I would guess not because this would require a stronger approximation property and thus lose generality, but I was not able to find a reference for the result (I was not even able to find the statement online or in the different books I looked at).

[Sébastien Gouëzel]

I'm not sure you need second countability of a factor: using your condition and approximation, you should be able to prove that $\xi (A \times B) = \mu(A) \nu(B)$ for closed sets, so two candidates measures $\xi$ and $\xi'$ would coincide on such product sets, and these generate the product sigma-algebra (which is not the Borel sigma algebra in general), so $\xi$ and $\xi'$ should coincide on the product sigma-algebra. Well, you didn't specify in your statement on which sigma-algebra $\xi$ is supposed to be defined, but I guessed the product one. If you're talking about the Borel one, then yes you definitely need second countability somewhere.

[Etienne Marion]

Indeed $\xi$ is defined over the product $\sigma$-algebra. At first I had assumed second countability to make sure products of closed sets generated the $\sigma$-algebra but as you rightfully pointed out this is not needed at all. I had used another result to get convergence of the integral more easily at then end but this required OpensMeasurableSpace because it deduced measurability in dominated convergence from continuity, but as my function is just a product of continuous functions composed with the projections I don't need that, so I applied dominated convergence directly and it worked. So indeed no need for second countability :tada: Thanks for your help!

[Etienne Marion]

I opened #31021 for this.

[Etienne Marion]

I realized I needed something stronger. Indeed if X is a product space Π i, X i where each X i is assumed to be Borel, then applying this result would require Π i, X i to be Borel and thus second countability of each X i. So in #31131 I reworked the file to first prove the case over (Π i, X i) × (Π j, Y j) by using a product of products of bounded continuous functions, and then deduced other cases from there.