canonical norm coming from Haar measure

Stream: Is there code for X?

[Kevin Buzzard]

If $R$ is a locally compact topological ring, and if we fix an additive Haar measure $\mu$ on $(R,+)$, then for every $r$ in the unit group $R^\times$ we can consider the measure $U\mapsto \mu(rU)$. Distributivity tells us that this is also a Haar measure on $R$ , and thus up to a positive real constant $\Delta(r)$ it's the measure we started with, i.e. $\mu(rU)=\Delta(r)\mu(U)$. This gives us a canonical function $\Delta:R^\times\to\mathbb{R}_{>0}$ which is easily checked to be a group homomorphism. For example, on the reals it's just the absolute value, and on the complexes we have $\Delta(x+iy)=x^2+y^2$. Do we have this group homomorphism? We have all the difficult ingredients needed to define it, for sure, so it would probably be a fun exercise if we don't have it.

[Eric Wieser]

Does this always coincide with the norm when R is a normed ring?

[Kevin Buzzard]

I doubt it because presumably we have endowed $\mathbb{C}$ with its usual norm, and as you can see from the example above (or just by thinking geometrically), multiplication by 2 on the complexes scales area by a factor of $4=\Delta(2)$ which is the square of the usual norm of 2.

[Kevin Buzzard]

This function is completely intrinsic. I didn't mention that in my original post but $\Delta$ is even independent of the choice of Haar measure, it's a canonical function on the units of any locally compact topological ring.

[Kevin Buzzard]

Right now I'm having trouble even stating things in Lean because I've never used Haar measure before and I don't know where to get [MeasurableSpace R] from.

[Anatole Dedecker]

Kevin Buzzard said:

Right now I'm having trouble even stating things in Lean because I've never used Haar measure before and I don't know where to get [MeasurableSpace R] from.

You should assume [MeasurableSpace R] [BorelSpace R]

[Anatole Dedecker]

And for using it in a proof if you don't have a MeasurableSpace available there is the wonderful docs#Mathlib.Tactic.Borelize.borelize tactic

[Anatole Dedecker]

By the way, I remember some work getting done about the modular character, did that ever make it into Mathlib ?

[Kevin Buzzard]

Aah, modular characters! That's the name. Apparently they have them in unreal engine but not in mathlib.

[Kevin Buzzard]

Wait no, that is something else? That's how left haar measure scales under right multiplication :-/ (so it's trivial on $\mathbb{R}$) Looks like I shouldn't have used $\Delta$ for my notation.

[Anatole Dedecker]

Yes it's not quite the same (after all the modular character is trivial for abelian groups) but it's also essentially the same

[Kevin Buzzard]

Yes I agree that if we have one of them, then defining the other one just got even easier!

[Anatole Dedecker]

Maybe there is some general setup: if you have $f : G \to G$ which is $\phi$-equivariant for some map $\phi : G\to G$ (meaning $f(g\cdot x) = \phi(g)\cdot f(x)$) then you can define the modular character of $f$. This takes care of both definitions (and its either a morphism or an antimorphism depending on wether I have chosen the right sides, which I think I haven't but oh well).

[Anatole Dedecker]

I don't know if this has any interest though :upside_down:

[Kevin Buzzard]

Well I need the one I asked about for FLT and this MSE question is complaining about different normalisations in the literature for the one you talked about, so at least people seem to be interested in those two examples!

[Yury G. Kudryashov]

About MeasurableSpace and borelize: have a look at how docs#dimH uses borelize to avoid [MeasurableSpace _] [BorelSpace _] assumptions.

[Kevin Buzzard]

My FLT class will have to figure it out on Monday :-) Thanks for the tips!

[Yaël Dillies]

docs#MeasureTheory.Measure.haarScalarFactor ?

[David Ang]

docs#MeasureTheory.Measure.addHaarScalarFactor !

[Yaël Dillies]

FLT#195