feat: compute the distributive Haar character of ℝ, ℂ, ℤ_[p] and ℚ_[p]

[YaelDillies]

Co-authored-by: Javier López-Contreras [email protected]

---

• depends on: chore: rename modularHaarChar to distribHaarChar #263

[kbuzzard]

Here are two ideas which are (to me) distinct.

1. Given a multiplicative group G acting as a DistribMulAction on an additive group A (e.g. A is a ring and G=A^*) with an additive Haar measure, there's a character G -> R_{>0}. Note that the key axiom is g . (a1 + a2) = g . a1 + g . a2, and G acts on A via additive group isos. Everything can be commutative here and the answer can still be interesting.

2. Given a multiplicative group G acting on a multiplicative group H (e.g. H=G) with [IsScalarTower G H H] i.e. the axiom (g • h1) * h2 = g • (h1 * h2), and a multiplicative Haar measure on H, there's a character G -> R_{>0}. Note that G acts on H via things which aren't group isos, but they are bijections. Note also that nontriviality of this character implies that left and right Haar measures on H are different and in particular that H is not commutative.

"Modular character" is reserved in the literature for (2). I want (1). In this PR right now we have two files FLT/ForMathlib/DomMulActMeasure.lean and FLT/HaarMeasure/ModularCharacter.lean both with docstrings which seem to say basically the same thing (and both of which seem to be (1)), and both of which seem to use the words "modular character" for (1). We need to call it something else. How about distribHaarCharacter?

[YaelDillies]

Here are two ideas which are (to me) distinct. [...]

Yes, Javier and I ended up understanding what you meant by "This is not what the literature calls modular characters". Will update this PR later today

[kbuzzard]

Thanks! This mostly looks fine, but I have an issue with one of the sorrys.

[kbuzzard]

I think we're nearly there. Can you maybe not add any more stuff so we can get this over the line?

[kbuzzard]

Thanks so much for your work on this!