Product of Borel spaces

Stream: maths

[Kevin Buzzard]

Here's a definition which we have in FLT (and we're still developing the API for). Let $R$ be a topological ring which is locally compact as a topological space. Then thanks to Floris we know that there's a Haar measure $\mu$ on the additive abelian group $(R,+)$, unique up to a positive real scaling factor. If $u\in R^\times$ then left multiplication by $u$ is an additive group isomorphism $(R,+)\cong (R,+)$ and so there must be a positive real number $\delta_R(u)$ such that $\mu(uX)=\delta_R(u)\mu(X)$ for all measurable $X\subseteq R$. The map $\delta_R$ is easily checked to be a group homomorphism from $R^\times$ to the positive reals. Examples: $\delta_{\mathbb{R}}(u)=|u|$ for
$0\not=u\in\mathbb{R}$ because multiplication by $u$ scales Lebesgue measure on $\R$ by a factor $|u|$. Another example: $\delta_{\mathbb{C}}(z)=|z|^2$ because, for example, doubling on the complex numbers scales area by a factor of 4.

On Monday I gave a lecture where I (informally) made this definition of $\delta_R$ and then later on I made the remark that it is trivial to check that $\delta_{R\times S}(u,v)=\delta_R(u)\delta_S(v)$, because if you scale the width of a rectangle by a positive real factor $x$ and the height by $y$ then you scale the area by $xy$. Are you all following along so far?

This lecture was part of a series of lectures on FLT, and we need this product result in the proof I'm formalising, in the case where $R$ is the finite adeles of a number field, $S$ is the infinite adeles, and $R\times S$ is the adeles (these definitions have recently landed in mathlib). But of course I wanted to formalise everything in the correct generality as part of the API for $\delta_R$, so in particular I wanted to formalise this trivial result about $\delta_{R\times S}$.

I have very limited experience with the measure theory part of mathlib (and with the area in general), but my understanding is that if $R$ is a topological space and I want to start talking about measures on it then I need to write this:

variable (R : Type*)
  [TopologicalSpace R] [MeasurableSpace R] [BorelSpace R]

(it annoys me that this isn't [IsBorelSpace R], making it clearer what's going on to amateurs like me, but never mind). So I ploughed on with making the formal statement about these characters on products of locally compact rings, and to my mild surprise I got typeclass errors in the statement, which due to the magic of #synth I could easily trace back to the following failure:

import Mathlib

variable (R S : Type*)
  [TopologicalSpace R] [MeasurableSpace R] [BorelSpace R]
  [TopologicalSpace S] [MeasurableSpace S] [BorelSpace S]

#synth BorelSpace (R × S) -- fails

The correct name for this instance would be something like Prod.borelSpace so I #checked this name and it does exist in mathlib, but doesn't quite say what I expected it to say, as there is an unexpected extra hypothesis:

Prod.borelSpace.{u_1, u_2} {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α]
  [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] [SecondCountableTopologyEither α β] : BorelSpace (α × β)

This was the first time I'd encountered the rather novel SecondCountableTopologyEither α β typeclass (which in my opinion should be called IsSecondCountableTopologyEither, but never mind). In my application both R and S are second countable so the proof of FLT is not broken, but is my very convincing-looking (at least to me!) informal mathematical claim about $\delta_{R\times S}$ at the beginning of this message not actually correct? What is the mathematical subtlety here? There seems to be no comments in mathlib about why this extra hypothesis is needed, but perhaps I have fallen into some standard trap.

If my "obvious" lemma turns out to be false, this experience will just add weight to my conviction that humans shouldn't be left alone to do mathematics without the aid of machines like Lean.

[Dagur Asgeirsson]

I'm not familiar with this part of the library, but removing the assumption about second countability leads me to docs#Prod.opensMeasurableSpace, I guess you can find the mathematical subtlety by looking at its proof.

So the second countability assumption is just to ensure that all open sets in $R \times S$ are measurable. Googling a bit, this seems to be well-known. I don't think there is any way for your obvious lemma to be false, just undefined. But I agree with

Kevin Buzzard said:

humans shouldn't be left alone to do mathematics without the aid of machines like Lean.

[Yaël Dillies]

Yes, exactly. The issue is that the open sets in the product are generated by arbitrary unions from boxes, while measurable sets in the product are generated by countable union. They match only if there is a way to consider only countably many sets in one direction or the other

[Kevin Buzzard]

I now understand the mathematical subtlety but I don't see why my lemma is undefined: if R is any locally compact topological ring then as far as I can see $\delta_R$ is well-defined, and a binary product of locally compact rings is locally compact. So the way I see it (at this point) the lemma is either true or false.

[Kevin Buzzard]

Let me talk through the argument a little more. Left multiplication by u is an additive automorphism of (R,+) which is also a homeomorphism. If I then put the Borel sigma-algebra structure on R it's an isomorphism of measurable spaces. So I get my positive real number from general nonsense, right?

[Johan Commelin]

Can't you get your BorelSpace (R \times S) via a different route, if you know that R and S are both loc.cmpt top rings?

[Sébastien Gouëzel]

Your lemma is correct, but your proof is not. Let $\mu$ be a Haar measure on $S$ (more precisely on the Borel sigma algebra of $S$, call it $\mathcal{B}_S$). In the same way, let $\nu$ be a Haar measure on $\mathcal{B}_T$ in $T$. Then the product measure $\mu \otimes \nu$ (in Mathlib sense) is a measure on the product sigma-algebra $\mathcal{B}_S \otimes \mathcal{B}_T$, which is not the Borel sigma-algebra on $S \times T$ when both of these spaces are not second-countable. So, $\mu \otimes \nu$ is not a Haar measure.

[Sébastien Gouëzel]

On the other hand, you can start from a Haar measure $\rho$ on $S \times T$, which exists as this space is locally compact. It is defined on the much bigger sigma-algebra $\mathcal{B}_{S \times T}$, and it is not a product measure a priori. Fix $s_0$ and $t_0$ sets in $S$ and $T$ which are compact with nonempty interior. Then I can define a measure $\nu$ on $\mathcal{B}_S$ by $\nu(s) := \rho(s \times t_0)$. This is a Haar measure on $S$. Then $\delta_{R\times S} (a,1) \nu(s_0) = \delta_{R\times S} (a,1) \rho(s_0\times t_0) =\rho ((a, 1) (s_0 \times t_0)) = \rho(a s_0 \times t_0) = \nu(as_0)=\delta_R(a) \nu(s_0)$, which shows that the Haar expansion factor of $(a, 1)$ in $R\times S$ coincides with the Haar expansion factor of $a$ in $R$. Similarly, $\delta_{R \times S} (1, b) = \delta_S(b)$. Taking the product, $\delta_{R \times S}(a, b) = \delta_R(a) \delta_S(b)$.

[Sébastien Gouëzel]

Note that I specified "in the Mathlib sense" for the product measure above, because there are competing definitions of product measures in the literature. For some authors, you first take the measure on the product of the Borel sigma algebras as above, but then you complete as much as you can. Then the product of Haar measures would be a completion of the Haar measure on the product (but this requires an additional proof, which is essentially the argument I've given above, and starts from the existence of the Haar measure on the whole Borel sigma-algebra of the product).

[Kevin Buzzard]

Wonderful! Many thanks for this. So "product of Haar measures is obviously a Haar measure" is ultimately my error. I am reminded of my "pushforward of product topologies is obviously product of pushforward topologies because what else can it be" error a few months ago, but Patrick saw through that claim immediately. I like that my error here is so subtle -- product of Haar measures isn't even a measure on the correct sigma algebra so it's actually a type error to claim that it's equal to Haar measure on the product. Many thanks all!

[Jireh Loreaux]

I love this thread. It's a perfect example of one of the reasons I've loved formalization so much. In pursuing the appropriate generality, we learn so much more than we would've otherwise, and we end up needing cross-pollination from different sides of the community. :heart: