Zulip Chat Archive

Stream: Is there code for X?

Topic: measure theory for algebraists


view this post on Zulip Kevin Buzzard (Feb 26 2021 at 17:56):

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

Now assume that MM has a real-valued norm on it. All we have so far is that μ(UV)=μ(U)+μ(V)\mu(U\cup V)=\mu(U)+\mu(V) for UU and VV disjoint clopens, and in particular it can absolutely happen that μ(U)>μ(UV)|\mu(U)|>|\mu(U\cup V)| -- note that MM is not ordered, it just has a norm, so μ(U)>μ(UV)\mu(U)>\mu(U\cup V) doesn't make sense. Here is an example where this weirdness happens. If XX is finite of size pp a prime, and if M is the integers, and if we give each element of XX measure 1, then XX itself has measure pp, and if we now put the pp-adic norm on MM (which is real-valued and satisfies 1=1|1|=1 and p<1|p|<1) then the norm of 11 is greater than the norm of pp 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 XX the pp-adic integers, but give XX size 1, now thought of as an element of M=QM=\mathbb{Q}, and if we use Haar measure, then pnXp^nX has size pnp^{-n} which has very big pp-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 XX to a normed semiring) is said to be a measure if there is some real number KK such that μ(U)K|\mu(U)|\leq K for all clopens UU (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 μ(U)K|\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 MM is multiplicative and nonarchimedean (m1+m2max{m1,m2}|m_1+m_2|\leq \max\{|m_1|,|m_2|\} it's easy to check that XfdμKf|\int_X fd\mu|\leq K|f| and so if furthermore MM is complete with respect to the norm (e.g. MM is the pp-adic numbers) then this integral now extends from the locally constant functions to the space of all continuous functions XMX\to M, where we put the topology on MM 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 MM 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 MM to be the pp-adic numbers.

view this post on Zulip Heather Macbeth (Feb 26 2021 at 18:14):

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 XX to MM) to MM. Then you're trying to prove an extension theorem for this normed group homomorphism, extending from the subgroup (locally constant) to all continuous functions.

view this post on Zulip Heather Macbeth (Feb 26 2021 at 18:14):

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

view this post on Zulip Heather Macbeth (Feb 26 2021 at 18:19):

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.

view this post on Zulip Eric Wieser (Feb 26 2021 at 18:38):

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

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 21:55):

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).

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 21:55):

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

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 21:56):

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


Last updated: May 17 2021 at 15:13 UTC