measure theory for algebraists

Stream: Is there code for X?

[Kevin Buzzard]

Here is a situation where algebraic number theorists use the language of measure theory. I spent some time with @Ashvni Narayanan today trying abstract out from some number theory texts what is actually going on, and I'm wondering if there's anything in the measure theory library which we can use or whether we need to build this stuff from scratch.

Let $X$ be a profinite (i.e. compact. Hausdorff, totally disconnected) space (this could work in more generality). Let $M$ be an add_comm_monoid. A distribution $\mu$ on $X$ is a finitely additive function from the clopen subsets of $X$ to $M$ (a finite disjoint union of clopen sets is clopen). [Note that we definitely don't want $M$ to be the nonnegative reals, in the end it will be the p-adic numbers or something like that.]. If $f:X\to M$ is locally constant then it's continuous for the discrete topology on $M$ and hence the image of $f$ is finite, so if $M$ is actually a commutative semiring then one can define $\int_Xf d\mu$ to be the obvious finite sum of products $m\mu(\{x\mid f(x)=m\})$, and this integral is finitely additive too.

Now assume that $M$ has a real-valued norm on it. All we have so far is that $\mu(U\cup V)=\mu(U)+\mu(V)$ for $U$ and $V$ disjoint clopens, and in particular it can absolutely happen that $|\mu(U)|>|\mu(U\cup V)|$ -- note that $M$ is not ordered, it just has a norm, so $\mu(U)>\mu(U\cup V)$ doesn't make sense. Here is an example where this weirdness happens. If $X$ is finite of size $p$ a prime, and if M is the integers, and if we give each element of $X$ measure 1, then $X$ itself has measure $p$, and if we now put the $p$-adic norm on $M$ (which is real-valued and satisfies $|1|=1$ and $|p|<1$) then the norm of $1$ is greater than the norm of $p$ so we have this slightly weird behaviour of subsets having "size" greater than the whole set.

Indeed if we do the same sort of thing with $X$ the $p$-adic integers, but give $X$ size 1, now thought of as an element of $M=\mathbb{Q}$, and if we use Haar measure, then $p^nX$ has size $p^{-n}$ which has very big $p$-adic norm, and we have smaller and smaller clopen sets whose measures have bigger and bigger norm. This is a bit crazy so we rule it out -- a distribution in this general context (mapping clopen subsets of $X$ to a normed semiring) is said to be a measure if there is some real number $K$ such that $|\mu(U)|\leq K$ for all clopens $U$ (we will allow subsets to have bigger measure than the whole set, but we will control how big everything can be globally).

We can integrate locally constant functions with respect to any distribution. If $\mu$ is however a measure with $|\mu(U)|\leq K$, and if we give the space of locally constant functions the sup norm (recall that the image is finite), then under the assumption that the norm on $M$ is multiplicative and nonarchimedean ($|m_1+m_2|\leq \max\{|m_1|,|m_2|\}$ it's easy to check that $|\int_X fd\mu|\leq K|f|$ and so if furthermore $M$ is complete with respect to the norm (e.g. $M$ is the $p$-adic numbers) then this integral now extends from the locally constant functions to the space of all continuous functions $X\to M$, where we put the topology on $M$ coming from the norm.

This is what we need. I don't see any obstructions to doing this in Lean -- but my question is whether there is anything at all in the measure theory repo which bears any resemblence to this or whether we just have to start from scratch. Note that the clopen subsets do not even form a sigma-algebra because a countably infinite union of clopens is not in general clopen. However in the situation where we have a measure and a nonarchimedean norm on a complete $M$ we could probably define the measure of anything in the sigma-algebra generated by the clopens. It is however of course essential that we can allow $M$ to be the $p$-adic numbers.

[Heather Macbeth]

Maybe not in the measure theory repo, but perhaps there are useful tools in the general analysis folder? For example, your integral could be expressed, to start with, as a normed group homomorphism from a certain subgroup of (continuous functions $X$ to $M$) to $M$. Then you're trying to prove an extension theorem for this normed group homomorphism, extending from the subgroup (locally constant) to all continuous functions.

[Heather Macbeth]

Not that there's much content in this, but it might let you at least avoid some boilerplate.

[Heather Macbeth]

Mathlib at least already has the normed group structure on the space of bounded continuous functions,
docs#bounded_continuous_function.normed_group
and things like that.

[Eric Wieser]

By "normed group homomorphism" are you referring to the normed_group_hom in #6375?

[Kevin Buzzard]

Yeah, it's funny how doing some advanced maths means that you need some other stuff which other people doing other advanced maths need too. This has happened several times (see the class groups paper and the synergy with the Berkeley group, or my development of DVRs and Johan/Rob doing Witt vectors).

[Kevin Buzzard]

Or all the topology which Patrick did for the perfectoid project being used in a ton of other places

[Kevin Buzzard]

This is what makes what we're doing so powerful.