Amenable group actions

Stream: mathlib4

[Anatole Dedecker]

@Matthias U Which definition of amenable groups are you going for? In particular does it assume the group to be locally compact? In any case this is great, please ping me once you have an open PR!

[Yaël Dillies]

Anatole, if you want to have a sneak peak, there were 7 open PRs about amenability in mathlib: https://github.com/leanprover-community/mathlib/pulls?q=is%3Apr+amenable+is%3Aopen

[Anatole Dedecker]

Oooooh I missed that! (Probably because I didn’t know anything about amenable groups in 2022…)

[Matthias U]

Anatole Dedecker said:

Matthias U Which definition of amenable groups are you going for? In particular does it assume the group to be locally compact? In any case this is great, please ping me once you have an open PR!

Sure, I'll let you know. I'm mostly considering finitely generated (discrete) groups, so yes. But I'm happy to discuss possible generalisations, if applicable

[Sebastien Gouezel]

It's really important for nonamenability to go beyond discrete groups: essentially all the theory works for locally compact groups (although it is slightly more painful to set up), and this is needed for many applications.

[Patrick Massot]

I think Anatole meant that locally compact groups are not enough.

[Sebastien Gouezel]

Yes, I got that. My comment was to say that, for sure, discrete groups are not enough.

[Notification Bot]

6 messages were moved here from #mathlib4 > github permission by Oliver Nash.

[Notification Bot]

A message was moved here from #mathlib4 > github permission by Oliver Nash.

[Junyan Xu]

Should this combine with #new-members > Amenable Groups?

[Matthias U]

I just created a pull request: https://github.com/leanprover-community/mathlib4/pull/7395 . Looking forward to your comments!

[Henrik Böving]

Matthias U said:

I just created a pull request: https://github.com/leanprover-community/mathlib4/pull/7395 . Looking forward to your comments!

you forgot to run

find Mathlib -name "*.lean" | env LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

slash update Mathlib.lean with your new file

[Matthias U]

Btw, I'm following Bartholdi's survey article: https://arxiv.org/pdf/1705.04091.pdf (see Definitions 2.1 and 2.2 so far).

[Anatole Dedecker]

Reposting some comments I wrote on the PR because I think the discussion deserves to happen here:

I don't really know what the right definition of an amenable action is, but I'm worried that this definition won't give the correct definition for amenable (even locally compact) groups. The reason is that you definitely want your mean to be absolutely continuous with respect to any Haar measure on the group (otherwise there's no hope of viewing the mean as a functional on $L^\infty$).

Furthermore, it would be nice to have a definition of amenability that works for any topological group, the usual one being the existence of a left invariant mean on right uniformly continuous function. The significant disadvantage of that is that linking this with the usual definition requires a bit more work. This is all explained in the book Sébastien mentioned, and I've written a slightly more precise exposition of it with formalization at the back of my mind, so I'd be happy to help anyone working on that, but I'm not sure we have all the prerequisites for it...

In the meantime, I think I'm okay with writing up the theory in the setting of locally compact groups, but we should keep in mind this future generalization. In particular, I'm against Yaël's proposal to link this with probability measures, because that won't be true in a general setting I think. But I'm not sure what to do regarding amenable actions, I'll try to read about it.

By the way, another painful revelation I had when writing about amenable locally compact groups is that we don't have the right $L^\infty$ for it: in this context you really want $L^\infty$ to be the dual of $L^1$, even for non sigma-compact groups, which means that the right thing to quotient by is not equality almost everywhere, but equality locally almost everywhere...

[Sebastien Gouezel]

I had never noticed the subtlety between almost everywhere and locally almost everywhere, thanks for pointing it out. For those who are curious, this is the following phenomenon. Consider a measure space with a single point of infinite mass. Then L^1 is trivial, so you expect its dual L^∞ to be also trivial. However, with the usual definition of L^∞ this is a line in this case (you can prescribe the value at the point). But if you mod out by all functions that are zero on finite measure sets (i.e., all functions, since there are no finite measure sets), then you kill everything and you are left with a trivial space, which is good. So one may argue that, when defining L^∞, instead of identifying functions that coincide ae, one should rather identify functions that coincide locally ae, i.e., are ae equal on each set of finite measure.

So what should we do? (1) Redefine L^p (and ae equal functions) to work with functions that coincide locally ae? Or (2) ignore the issue and add sigma-finiteness assumptions when needed (this implies that ae and locally ae coincide)? I'd rather go for (2) since I've never met interesting non-sigma-finite measures, but I would be ready to change my mind if anyone shows a convincing example where the added generality is important.

[Sebastien Gouezel]

(With (1), the L^∞ norm of the constant function equal to 1 on a single atom of infinite mass is equal to 0, which feels pretty unusual, to say the least).

[Rémy Degenne]

Can you get the same Lp as in (1) by replacing AEStronglyMeasurable by AEFinStronglyMeasurable in the definition of AEEqFun?

[Sebastien Gouezel]

I don't think so. On an uncountable space with the counting measure, the constant function 1 is in L^∞ (in the (1) or (2) sense, they coincide here), but it is not AEFinStronglyMeasurable.

[Anatole Dedecker]

Well the typical case where you want non sigma-finite measures are Haar measure on non sigma-compact groups. I don't know how much care about it in the general case, but I'm pretty sure that people care about uncountable discrete group at least. Of course the problem doesn't arise in this case, but I'm not sure we want a SecondCountableOrDiscrete typeclass just to go around this problem.

[Anatole Dedecker]

My instinct would be to go for (1) (note that this wouldn't actually change the definition for finite p I believe), but I definitely understand that it's a bit of a hassle for a situation which doesn't arise that often. I think we wouldn't lose anything by changing the definition (does anyone know of an example in non-sigma-finite measure where you'd want the current definition), but the risk is making the basic API heavier...

[Sebastien Gouezel]

To get an example where the notions differ, it's not really sigma-finiteness that matters. For instance, for the counting measure on an uncountable space, (1) and (2) coincide. The problem is when you have an infinite measure subset that does not contain a subset of finite positive measure. It's not clear to me if this is possible for a Haar measure on a locally compact group?

[Kevin Buzzard]

For Haar measure on a locally compact group, if you choose an open neighbourhood of a point within a compact neighbourhood then I think necessarily the open and compact neighbourhoods have nonzero finite measure (because every nonempty open has positive measure and every compact has finite measure; these are general properties of Haar measure).

[Sebastien Gouezel]

Here is an example. Consider $\mathbb{R} \times \mathbb{R}$ where the first line has the discrete topology, and the second one the usual topology. Then the Haar measure is a sum of uncountably many Lebesgue measures, one on each vertical line. And this is a locally compact group.

For any countable set $s$, then $s\times \{0\}$ has zero measure: cover each point in $s$ by a vertical open interval with measure $\epsilon * 2^{-n}$, this gives an open set containing $s$ with measure at most $\epsilon$. On the other hand, for any uncountable set $s$ then $s\times \{0\}$ has infinite measure: given an open set which contains it, it contains $t \times (-\epsilon, \epsilon)$ for some uncountable $t$ and some positive $\epsilon$, so it has infinite measure. By outer regularity, this shows the claim. It follows that the horizontal line is an infinite measure set which contains only infinite measure sets and zero measure sets.

[Kevin Buzzard]

So necessarily the infinite measure set must have empty interior, which is indeed what is happening in your example.

[Matthias U]

Anatole Dedecker said:

I don't really know what the right definition of an amenable action is, but I'm worried that this definition won't give the correct definition for amenable (even locally compact) groups. The reason is that you definitely want your mean to be absolutely continuous with respect to any Haar measure on the group (otherwise there's no hope of viewing the mean as a functional on $L^\infty$).

I tried to read a few things about the general situation: If I understand correctely, the following is true: A (topological) group G (with Haar measure $\mu$) is amenable if and only the left translation action $G \curvearrowright G$ admits an invariant mean $m$, where as $\sigma$-algebra, we take the Borel $\sigma$-algebra (i.e. the $\sigma$-algebra generated by the open sets of the topology on $G$); Here, additionally, we need to demand that the mean $m$ is absolutely continuous wrt $\mu$ (i.e. if $A\subset G$ is measurable with $\mu(A) = 0$, then we have $m(A) = 0$).

Reference for this fact: Remark G.1.3 in the appendix of "Kazhdan's Property (T)" by Bekka, de la Harpe, Valette

[Sebastien Gouezel]

I have just asked Bachir Bekka about that remark (he happens to have his office next to mine), and he told me to be careful about this remark, because

• maybe the $L^\infty(X, \mu)$ in the remark is the usual $L^\infty$, contrary to what they use in the rest of the book for $L^\infty$ on groups.
• maybe the reference they give for the details (Hewitt-Stromberg) only deals with the sigma-finite case.

I'll have a look at Hewitt-Stromberg.

[Sebastien Gouezel]

(And note that the remark will only apply to locally compact groups, as you want to use the characterization in Theorem G.3.1 (v) which holds only for locally compact groups. Bachir argued convincingly that the main property of amenability should be the fixed point property for affine actions on compact convex sets, so the general definition should be the one they give in Definition G.1.4.

[Sebastien Gouezel]

Coming back to the distinction between the usual $L^\infty(\mu)$ (bounded measurable functions up to ae equivalence) and the more unusual $L_l^\infty(\mu)$ (bounded measurable functions up to local ae equivalence, i.e., two functions are equivalent iff, for every finite measure set, they coincide ae in this set). I am not sure this distinction is really relevant in the context of amenability of locally compact groups. Indeed, I claim it is equivalent to have an invariant mean on $L^\infty(\mu)$ or $L^\infty_l(\mu)$.

Proof: since there is a map from $L^\infty(\mu)$ to $L^\infty_l(\mu)$, an invariant mean on $L^\infty_l(\mu)$ gives one on $L^\infty(\mu)$. Conversely, assume you have an invariant mean on $L^\infty(\mu)$. As uniformly continuous bounded functions embed into $L^\infty(\mu)$, this gives an invariant mean on uniformly continuous bounded functions. By (i)=>(v) in Theorem G.3.1 in Bekka-de la Harpe-Valette, this gives an invariant mean on $L^\infty_l(\mu)$.

@Anatole Dedecker , does it make sense or am I confused somewhere?

[Sebastien Gouezel]

(It looks like this line of thought also says that it is equivalent to have an invariant mean on all measurable subsets, or an invariant mean on all measurable subsets which vanishes on all sets of Haar measure 0, or an invariant mean on all measurable subsets which vanishes on all sets of Haar measure locally 0).

[Sebastien Gouezel]

To support this, Fremlin (vol 4, Chapter 44) discusses amenable topological groups and amenable locally compact groups at length, without ever using $L^\infty_l$.

[Antoine Chambert-Loir]

I support the idea of having more general measure theory than what is usually done in basic treaties. For my own work, for example, where measures live on naturally huge spaces, it was absolutely fundamental to forget about exterior regularity and focus on interior regularity.

[Antoine Chambert-Loir]

Fremlin's book (I should say, books) is remarkable. If we manage to formalize it, it would be absolutely great.

[Anatole Dedecker]

Sebastien Gouezel said:

Coming back to the distinction between the usual $L^\infty(\mu)$ (bounded measurable functions up to ae equivalence) and the more unusual $L_l^\infty(\mu)$ (bounded measurable functions up to local ae equivalence, i.e., two functions are equivalent iff, for every finite measure set, they coincide ae in this set). I am not sure this distinction is really relevant in the context of amenability of locally compact groups. Indeed, I claim it is equivalent to have an invariant mean on $L^\infty(\mu)$ or $L^\infty_l(\mu)$.

Proof: since there is a map from $L^\infty(\mu)$ to $L^\infty_l(\mu)$, an invariant mean on $L^\infty_l(\mu)$ gives one on $L^\infty(\mu)$. Conversely, assume you have an invariant mean on $L^\infty(\mu)$. As uniformly continuous bounded functions embed into $L^\infty(\mu)$, this gives an invariant mean on uniformly continuous bounded functions. By (i)=>(v) in Theorem G.3.1 in Bekka-de la Harpe-Valette, this gives an invariant mean on $L^\infty_l(\mu)$.

Anatole Dedecker , does it make sense or am I confused somewhere?

I'm convinced by the argument, but I think that this could bite us later because existence of a mean on $L^\infty_l(\mu)$ is really a stronger statement: not only is the map $L^\infty(\mu) \to L^\infty_l(\mu)$ not injective (i.e "we can assume the mean is zero on locally null sets", which is easy to state), it's also not surjective (i.e "we can assume the mean extends to this whole space", which is rather annoying to state without making reference to that bigger state). But I think it should be easy enough to just use the dual of $L^1$ each time we want to refer to $L^\infty_l(\mu)$, so at least it's not a strict requirement.

[Anatole Dedecker]

The situation in Fremlin is confusing to me (somehow I'm always lost when looking up something in Fremlin), because in the proof of theorem 449J (which is his version of G.3.1) he does say "recall that L1 is a Banach algebra under convolution (444Sb), and that L∞ can be
identified with its normed space dual, because μ is a quasi-Radon measure, therefore localizable (415A)". To me that must means that he's assuming something extra on his Haar measures, but I can't find what exactly...

[Anatole Dedecker]

The Haar measure in your counterexample above is outer regular wrt open sets and inner regular for open sets wrt compact sets, right?

[Sebastien Gouezel]

Anatole Dedecker said:

The Haar measure in your counterexample above is outer regular wrt open sets and inner regular for open sets wrt compact sets, right?

Yes. That's the standard definition of the Haar measure, if I am not mistaken.

[Anatole Dedecker]

I agree that it's the standard definition (although regularity is not required in Mathlib, right?)

[Anatole Dedecker]

Ah, Fremlin does assume his quasi-Radon measures to be semi-finite, which means exactly that you can't have infinite measure sets containing no nonzero finite measure sets.

[Sebastien Gouezel]

But then does it mean he can't construct a Haar measure on every locally compact group?

[Anatole Dedecker]

I'm surprised by this too, because he does prove an existence theorem...

[Sebastien Gouezel]

It seems Fremlin's definition of Radon measure is not the standard one (he requires inner regularity wrt compact sets for any measurable set, and he doesn't require outer regularity with respect to open sets). So probably his Haar measure is not the usual one...

[Anatole Dedecker]

I think the same kind of things happens for the Riesz representation theorem: the french wikipedia page gives two different notions of Radon measure that satisfy the Riesz reprensentation theorem (and there's even a claim that the one we have is not the "right" one)

[Anatole Dedecker]

@Antoine Chambert-Loir This is precisely what you claim, right? That inner regularity for all borel sets is more useful than docs#MeasureTheory.Measure.Regular

[Anatole Dedecker]

Matthias U said:

Anatole Dedecker said:

I don't really know what the right definition of an amenable action is, but I'm worried that this definition won't give the correct definition for amenable (even locally compact) groups. The reason is that you definitely want your mean to be absolutely continuous with respect to any Haar measure on the group (otherwise there's no hope of viewing the mean as a functional on $L^\infty$).

I tried to read a few things about the general situation: If I understand correctely, the following is true: A (topological) group G (with Haar measure $\mu$) is amenable if and only the left translation action $G \curvearrowright G$ admits an invariant mean $m$, where as $\sigma$-algebra, we take the Borel $\sigma$-algebra (i.e. the $\sigma$-algebra generated by the open sets of the topology on $G$); Here, additionally, we need to demand that the mean $m$ is absolutely continuous wrt $\mu$ (i.e. if $A\subset G$ is measurable with $\mu(A) = 0$, then we have $m(A) = 0$).

Reference for this fact: Remark G.1.3 in the appendix of "Kazhdan's Property (T)" by Bekka, de la Harpe, Valette

Going back to amenability, yes indeed I think you recover the right notion if you add the absolute continuity, and this is exactly what I claim is the problem with your current definition: there's no absolute continuity. Furthermore, I think it will be nicer to work with means defined on all of $L^\infty$ instead of indicators to begin with, and prove later than you only care about indicators really.

[Anatole Dedecker]

Of course this is assuming we want to use the mean definition at all, instead of going straight to the general case.

[Antoine Chambert-Loir]

Anatole Dedecker said:

Antoine Chambert-Loir This is precisely what you claim, right? That inner regularity for all borel sets is more useful than docs#MeasureTheory.Measure.Regular

I just claim that exterior regularity is a good thing when you have it, but not something to expect in general (beyond the world of Polish spaces).

[Anatole Dedecker]

(Still about amenability)

Like Sébastien I am convinced that we need to consider the general case at some point and the fixed point characterization is really the right one. But, at least if we follow Bekka, de la Harpe and Valette (let's call it BHV), I think we need to do a few things before being able to prove their theorem G.3.1:

• define type aliases to equip a group with left or right uniformity. This is not strictly a requirement, but I expect it will be nicer to work with right-uniformly-continuous function if we can spell them with type aliases (and I have fun versions of some proofs that require playing with these). Note that "left-uniformly-continuous" in BHV means uniformly continuous for the right uniformity for Bourbaki.
• define convolution in multiplicative non-abelian groups, and prove the basic properties (notably that $\ast:L^1\times L^\infty \to L^\infty$ actually takes values in right-uniformly-continuous function) without sigma-finiteness. This might require showing uniqueness of regular haar measures (note docs#MeasureTheory.Measure.haarMeasure_unique assumes sigma-finiteness).
• we also need some facts about the $(L^1, (L^1)^*)$ duality, namely that positive integrable functions of norm 1 map to a dense subset of means on $(L^1)^*$ or $L^\infty_l$. This is left as an exercise in BHV if I remember correctly, but it's not entirely trivial because you need to be careful about positivity
• we need to prove the complex version on a few results on real locally convex spaces (Hahn-Banach separation and some of its consequences mostly).

[Anatole Dedecker]

Antoine Chambert-Loir said:

Anatole Dedecker said:

Antoine Chambert-Loir This is precisely what you claim, right? That inner regularity for all borel sets is more useful than docs#MeasureTheory.Measure.Regular

I just claim that exterior regularity is a good thing when you have it, but not something to expect in general (beyond the world of Polish spaces).

And is it because you trade it for stronger inner regularity? Or just that the measures you care about are not meant to represent linear functionals on $C_c(X)$ at all?

[Antoine Chambert-Loir]

Fremlin has a good discussion of Haar measures and their “uniqueness” (spoiler: as a function on sets, there is no uniqueness in general).

[Antoine Chambert-Loir]

Also, recently, model theory made new concepts emerge, such as Roelcke compactness, which has some interest for large spaces, such as function spaces.

[Sebastien Gouezel]

Anatole Dedecker said:

not only is the map $L^\infty(\mu) \to L^\infty_l(\mu)$ not injective (i.e "we can assume the mean is zero on locally null sets", which is easy to state), it's also not surjective (i.e "we can assume the mean extends to this whole space", which is rather annoying to state without making reference to that bigger state).

I don't understand why it is not surjective. Let me try to prove instead it is surjective. Take an element of $L^\infty_l(\mu)$, and then a measurable representative f. It is bounded by some constant M on a set which is locally almost everything. Let F be the truncation mapping points larger than M to M, and points smaller than -M to -M, and the identity inbetween. Then F o f coincides locally almost everywhere with f, and it is bounded and measurable. It defines an element of $L^\infty(\mu)$, which maps to f in $L^\infty_l(\mu)$. Did I overlook something?

[Anatole Dedecker]

/me should think twice before making "obvious" claims...

More seriously, I'm confused. Your argument looks right, but one of the reasons I made that claim is that I remember that one of the issue that arises when you try to show $L^\infty \simeq (L^1)'$ is that to build an element of $L^\infty$ from a linear form on $L^1$ you need to "glue" elements of $L^\infty(B)$ where $B$ has finite measure, which may prevent surjectivity. And indeed, both https://math.stackexchange.com/a/405587/828303 and Fremlin 243G claim that, even in the semi-finite case, you need something more to get that $L^\infty \to (L^1)'$ is surjective...

[Sebastien Gouezel]

Note that the fact that $L^\infty_l$ is the dual of $L^1$ is not true in general...

[Anatole Dedecker]

Oh. That explains it indeed...

[Anatole Dedecker]

I've found an even better result: theorem 9.4.8 of Measure Theory by Cohn states that, although we do not have $L^\infty \simeq (L^1)'$ for general regular measures on locally compact spaces, we do have an isomorphism as long as we are on a locally compact group.

[Sebastien Gouezel]

Yes, that's what is behind Fremlin's argument also.

[Sebastien Gouezel]

But this is only true for inner regular measures. I think I'll refactor our Haar measure to use the inner regular one instead of the outer regular one, as it is definitely better behaved from a functional analysis point of view.

[Anatole Dedecker]

I think Cohn's definition of regularity is exactly docs#MeasureTheory.Measure.regular though.

[Anatole Dedecker]

Ultimately there is a bijection between outer regular and inner regular measures right? Maybe the safest thing to do is to add this translation explicitly so that we're not blocked in the future (we still have to choose which one we base the theory onto, but even if we choose the "wrong" one it wouldn't cause that much trouble).

[Sebastien Gouezel]

Then his statement is not correct: for the regular Haar measure on $\mathbb{R} \times \mathbb{R}$ where the first copy is discrete, the set $\mathbb{R} \times \{0\}$ only contains zero and infinite measure subsets, so its characteristic function is nonzero in $L^\infty$ but still it is orthogonal to all $L^1$ functions.

[Anatole Dedecker]

Ah yes that's the same example of course... Sorry for getting confused

[Sebastien Gouezel]

My plan is to have a notion of preHaarMeasure where one would just require invariance, finiteness on compacts and positivity on opens (what is now called HaarMeasure). And then prove as many things as possible just assuming this. Additionally, have HaarMeasure require inner regularity. And prove existence and uniqueness of a preHaarMeasure which is regular, and also existence and uniqueness of a preHaarMeasure which is inner regular (i.e., of a HaarMeasure).

[Anatole Dedecker]

That sounds good!

[Cameron Zwarich]

Anatole Dedecker said:

I've found an even better result: theorem 9.4.8 of Measure Theory by Cohn states that, although we do not have $L^\infty \simeq (L^1)'$ for general regular measures on locally compact spaces, we do have an isomorphism as long as we are on a locally compact group.

Cohn proves earlier (in 7.5.4 in the 2nd edition) that this duality holds for the completion of regular Borel measures (for the same definition currently used by Lean) on LCH spaces. However, for Haar measures he proves in 9.4.8 that this holds even for the measure space given by the restriction of Haar measure to Borel sets. His definition of $L^\infty$ is what was previously called $L_l^\infty$ in this thread.

While inner-regular measures seem like a more sensible choice for more general topological measure theory, for harmonic analysis on LCGs the definition in terms of mixed outer/inner regularity has been standard, and I think you will find some subtle reliance on this. One example is the Vitali-Carathéodory theorem that $L^1$ functions can be approximated by lower/upper-semicontinuous functions from above/below.

[Sebastien Gouezel]

Recent textbooks I've looked at (Bogachev, Fremlin) all emphasize that the inner regular version is better, especially for Haar measure on locally compact groups. For L^1 functions, both measures will gives the same result (they only disagree in non sigma-finite situations, and the set of nonzero points of an L^1 function is sigma-finite), so Vitali-Caratheodory will hold whatever the choice of the Haar measure.

[Sebastien Gouezel]

Sebastien Gouezel said:

Vitali-Caratheodory will hold whatever the choice of the Haar measure.

Scratch that, it's just wrong. The two Haar measures agree on what the L^1 space is (i.e., there is a canonical isometry between the two of them), but only as a space of equivalence classes of functions (and the equivalence relation is not the same on the left and on the right, although the quotients are canonically isomorphic). They disagree on what an integrable function is, and indeed for the inner regular measure some integrable functions will not satisfy Vitali-Caratheodory (the characteristic function of $\mathbb{R} \times \{0\}$ is an example: it is almost everywhere zero for the inner Haar measure, so integrable, but still it can not be approximated from above by an integrable lower semicontinuous function).

[Antoine Chambert-Loir]

what do you mean by : “the equivalence relation is not the same although the quotients are canonically isomorphic”?

[Sebastien Gouezel]

When you build equivalence classes of functions, you identify two functions if they coincide almost everywhere. As you have two measures, you have two notions of "coinciding almost everywhere", which are genuinely different. But since the spaces of integrable functions you start from are also different, the quotients you get happen to be the same (well, canonically isomorphic to be precise).

[Kevin Buzzard]

Any sentence containing the word canonical is by definition not precise, the word is used precisely to remove precision

[Ruben Van de Velde]

It is used canonically to remove precision?

[Sebastien Gouezel]

ok, let me be precise :-)
Let $\mu$ be the inner regular Haar measure, and $\nu$ the outer regular one. Let $\mathcal{L}^1(\mu)$ be the space of integrable functions for $\mu$ (genuine functions, not equivalence classes), and $L^1(\mu)$ the space of equivalence classes of integrable functions for $\mu$. There are more zero measure sets for $\mu$ than for $\nu$, and more integrable functions for $\mu$ than for $\nu$ (the characteristic function of $\mathbb{R} \times \{0\}$ is integrable for $\mu$ but not for $\nu$). The composition of the inclusion $\mathcal{L}^1(\nu) \to \mathcal{L}^1(\mu)$ and the quotient map $\mathcal{L}^1(\mu) \to L^1(\mu)$ gives a natural map $\mathcal{L}^1(\nu) \to L^1(\mu)$. It descends to the quotient, giving a map $L^1(\nu) \to L^1(\mu)$, which happens to be a bijective isometry.

[Kevin Buzzard]

This is an extraordinary subtlety in the theory

[Antoine Chambert-Loir]

OK, thanks! In the above discussion, I had not been able to note the inclusion $\mathcal L^1(\nu) \to \mathcal L^1(\mu)$.

[Antoine Chambert-Loir]

Kevin Buzzard said:

This is an extraordinary subtlety in the theory

That's amazing, and also frightening, to realize how much detail is overlooked or forgotten in our standard (and nevertheless quite good) early math education.

[Sebastien Gouezel]

Most authors don't need to care, because they choose once and for all the inner regular Haar measure, or the outer regular Haar measure. Note that this identification is true for all $L^p$ spaces but for $L^\infty$, where the space for the inner one is nicer than the space for the outer one (it is smaller, and coincides with the dual of $L^1$).

[Sebastien Gouezel]

(And in reality all this doesn't matter, because all locally compact groups of interest happen to also be sigma-compact, and then the two Haar measures coincide).

[Anatole Dedecker]

I think the most surprising part is not that there are two standards, it’s that modern measure theorists seem to have a definite answer to "which one is more useful" yet (in my experience) most people teach the other one

[Kevin Buzzard]

What I was surprised by was that I am using Haar measure everywhere when I'm doing representation theory of p-adic groups but never encountered this subtlety -- but now I understand it's because it's not there in the cases which come up in my work (they're all sigma compact)

[Sebastien Gouezel]

I have to say I was completely unaware of this 10 days ago. And I'm glad I read enough measure theory since then to fill the gaps. That's one of the reasons I like so much formalizing -- you have to really understand what is going on, even the gory details noone ever mentions.

[Antoine Chambert-Loir]

Also : when you view measures as linear forms on continuous functions with compact support, this subtleties are totally absent (in that framework, the Haar measure is unique).

[Antoine Chambert-Loir]

If you allow a bit of provocation (those, who know, know) : while people claim the σ-algebra point of view is the only one that is valid to develop integration, it's only true for probability theory, and a lot of analysis (PDEs in particular) is perfectly happy with the point of view of Radon measures, to the point that distribution theory is a kind of generalization of it.