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:

[David Ledvinka]

Trying to impliment Sébastien's proof we have ran into two issues. Firstly the compact sets may not be measurable (since without Hausdorff assumption compacts are not necessarily Borel). But this was fixable by using the interiors instead. Secondly though the calculation at the end (at least according to the lemmas we have in the project) require the measure to be regular as well, and without second-countable we dont automatically have that a Haar measure is regular. Is it possible to prove that $\nu$ defined in this way is regular? (its not clear to me that it is)

An alternative idea I had would be to use MeasureTheory.Content and define the content in the same way as $\nu$ but only on compacts. This would automatically give regularity and I haven't checked any of the details but I assume this would be a Haar measure. Unfortunately I think this construction would definitely require compacts to be measurable (so assume Hausdorff).

Is it possible to complete the proof without either of these two assumptions?

[Kevin Buzzard]

Oh all my Haar measures are assumed regular. I always want to be in the situation that Haar measures are unique up to scaling. All my applications have a second countability assumption but I've tried to be as general as possible when sketching the theory

[Sébastien Gouëzel]

I think $\nu$ above should be regular, as $\rho$ is (maybe you need to pick $s_0$ and $t_0$ to be nice enough for this, i.e., compact, closed, and $G_\delta$). I can try to write down the details if you're stuck.

Another way is to use integrals of continuous compactly supported functions instead of measures of sets, to avoid all the regularity issues.

[David Ledvinka]

Kevin Buzzard said:

Oh all my Haar measures are assumed regular. I always want to be in the situation that Haar measures are unique up to scaling. All my applications have a second countability assumption but I've tried to be as general as possible when sketching the theory

Yes I am aware. But I have thought enough about this generalization that I wanted to see it through if reasonable lol. (Note the point I am making is that its not immediately clear that without second countability the constructed Haar measure on the components of the product is regular even though the one on the product is, although according to Sébastien it should be).

[David Ledvinka]

Sébastien Gouëzel said:

I think $\nu$ above should be regular, as $\rho$ is (maybe you need to pick $s_0$ and $t_0$ to be nice enough for this, i.e., compact, closed, and $G_\delta$). I can try to write down the details if you're stuck.

Another way is to use integrals of continuous compactly supported functions instead of measures of sets, to avoid all the regularity issues.

If your intuition says its true I can try to think about it more. I thought about it a little bit and became skeptical.

For your second point are you saying that a version of the following (proved) theorem should be true

lemma mulEquivHaarChar_smul_integral_map (μ : Measure G)
    [IsHaarMeasure μ] [Regular μ] {f : G → ℝ} (φ : G ≃ₜ* G) :
    ∫ (a : G), f a ∂μ = (mulEquivHaarChar φ) • ∫ a, f a ∂(map φ μ)

where we replace [Regular μ] with f continuously compactly supported or something like that?

[Sébastien Gouëzel]

Yes. That's essentially the way haarScalarFactor is defined, so it should come essentially for free from the definitions.

[Kevin Buzzard]

I think I muddied the water by pushing this "let's use a set of nonzero positive measure to calculate everything" idea; this was before I had been taught that using continuous functions with compact support was a better idea. My intuition is so poor that whilst I can immediately solve "if X is a set of reals with measure 1, what is the measure of 2X?" I don't have a clue about "if f is a function whose integral is 1 wrt mu, what is the integral of f wrt (x mapsto 2x)_* mu or (x mapsto 2x)^* mu" instinctively so my instinct was just to avoid them.

[James Sundstrom]

Eliminating the need for regularity turned out to be somewhat easier than expected. Regularity was being used to prove statements of the form mulEquivHaarChar φ • map φ μ = μ, but we only needed those measures to agree on open sets, which holds without regularity. If anyone's interested, the proof is here.

[Kevin Buzzard]

Thanks a lot!