Fundamental domains

Stream: FLT

[Kevin Buzzard]

So we're close to a sorry-free TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.finiteDimensional and I hope to get this over the line before Christmas (I have plenty of time to work on this myself).

Annoyingly, my vision for how one proof would go has been punctured slightly. We need this basic fact that if $X$ is a locally compact additive abelian group (think $\mathbb{R}^n$) and $\Gamma$ is a countable discrete group of $X$ (think $\mathbb{Z}^n$) such that $X/\Gamma$ is compact, then for $U\subseteq X$ of sufficiently large (Haar) measure, the composite $U\to X\to X/\Gamma$ can't be injective. I had assumed that this would be somewhere in mathlib (and I don't even know a precise statement; maybe what I'm claiming is too general), but the best I can find is docs#MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd which, instead of using quotients, is using docs#IsAddFundamentalDomain and I can't find any magic way of constructing fundamental domains for discrete actions so I'm wondering if the easiest thing is simply to construct the fundamental domain in our situation. This will involve doing measure theory, which is definitely not my strong point. We actually need an adelic version, but only over $\mathbb{Q}$. Here is an example of what would be helpful to us (if we do everything for the adeles of $\mathbb{Q}$ then we can deduce everything in general, because $\mathbb{A}_K=\mathbb{A}_{\mathbb{Q}}\otimes_{\mathbb{Q}}K$).

import Mathlib

open NumberField Metric Measure MeasureTheory IsDedekindDomain

notation:101 "𝔸" K => AdeleRing (𝓞 K) K

instance : MeasurableSpace (𝔸 ℚ) := borel _
instance : BorelSpace (𝔸 ℚ) := ⟨rfl⟩

instance : LocallyCompactSpace (𝔸 ℚ) := sorry

-- is this how you make a VAdd from an Algebra?
noncomputable instance : VAdd ℚ (AdeleRing (𝓞 ℚ) ℚ) where
  vadd q a := algebraMap ℚ (𝔸 ℚ) q + a

def F : Set (𝔸 ℚ) := (Set.univ.pi fun _ => closedBall 0 0.5).prod
      (Set.range <| RestrictedProduct.structureMap _ _ _)

example : IsAddFundamentalDomain ℚ F Measure.addHaar := by
  sorry

I can't find any magic constructors for docs#IsAddFundamentalDomain so I think we might simply have to check the axioms. nullMeasurableSet and ae_covers shouldn't be too bad but I am a bit nervous about aedisjoint : Pairwise <| (AEDisjoint μ on fun g : G => g +ᵥ s). Another approach would be to use $[0,1)$ at infinity rather than $[-0.5,0.5]$ and then one can really prove disjointness; the measure-theory issues go away because this really would be a fundamental domain in the strict sense (it meets every orbit once, rather than up to a measure zero error); maybe this is a better idea (but then we'd have to figure out how to say $[0,1)$ in Set v.Completion where v : InfinitePlace ℚ, which is probably something we should be able to do anyway...

We need this for NumberField.AdeleRing.DivisionAlgebra.Aux.existsE in FLT/DivisionAlgebra/Finiteness.lean.

[Kevin Buzzard]

Actually, typing this message has made me realise that the most sensible approach is simply to use $[0,1)$ which makes all measure-theoretic issues go away. I'm now working on a variant of the above sorry which will suffice.

[Kevin Buzzard]

A couple of random things I've skipped:

import Mathlib

lemma Int.eq_floor {a : ℝ} {b : ℤ} (h1 : 0 ≤ a - b) (h2 : a - b < 1) : b = ⌊a⌋ := by
  sorry

example (t : ℝ) (ht : t ∈ Set.Ico 0 1) : ‖t‖ ≤ 1 := by
  sorry

but things are going well. I have a set and have reduced the proof that it's a fundamental domain to statements which are not measure-theoretic but are completely algebraic, which means that I should be able to use Salvatore's work on the way K sits in A_K.

[Sébastien Gouëzel]

Didn't we already have this kind of discussion some time ago, e.g. in #Is there code for X? > descending measures to compact quotients @ 💬 ?

[Kevin Buzzard]

Yes! And you told me that I had to make a fundamental domain and that's what I've been doing all afternoon.

[Kevin Buzzard]

In particular you pointed out docs#MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd but this needs a fundamental domain. What I want is: "U in X with measure > Bound => map U -> X -> X/Gamma not injective" and I had assumed that compactness of X/Gamma would be enough but my understanding of the discussion you linked to was that we didn't have a way of magically constructing a fundamental domain by abstract nonsense (and the key lemma needs a fundamental domain) so I am just writing one down explicitly.

[Kevin Buzzard]

Oh sorry, let me be more precise: you did give me a method for constructing a fundamental domain by mostly pure thought but then Antoine said this #Is there code for X? > descending measures to compact quotients @ 💬 so I figured I would follow his idea instead.

[Kevin Buzzard]

(The point is that we did all the algebraic work already when proving compactness)

[Michael Stoll]

Kevin Buzzard said:

example (t : ℝ) (ht : t ∈ Set.Ico 0 1) : ‖t‖ ≤ 1 := by
  sorry

import Mathlib

example (t : ℝ) (ht : t ∈ Set.Ico 0 1) : ‖t‖ ≤ 1 := by
  grind [Real.norm_eq_abs]

[Thomas Browning]

The abstract way of doing this is to take the Haar measures on $\Gamma$ and $X/\Gamma$, show that they define a Haar measure on $X$ satisfying $\int_X=\int_{X/\Gamma}\int_\Gamma$ (or rather, $\int_X=\int_{X/\Gamma}\sum_\Gamma$ since $\Gamma$ is discrete). Then $U\to X\to X/\Gamma$ being injective implies that the inner sum is $\leq1$, so $\mu(U)\leq\mu(X/\Gamma$.

[Thomas Browning]

I can play around with this today and see if it's workable if you want (I'm not sure how easy this Haar measures on short exact sequences thing is).

[Kevin Buzzard]

Right -- this was the proof which I had expected to be formalising, but my impression was that the other thread was guiding me towards using fundamental domains instead.

[Michael Stoll]

import Mathlib

lemma Int.eq_floor {a : ℝ} {b : ℤ} (h1 : 0 ≤ a - b) (h2 : a - b < 1) : b = ⌊a⌋ := by
  rw [eq_comm, Int.floor_eq_iff]
  grind

just in case...

[Thomas Browning]

Thomas Browning said:

The abstract way of doing this is to take the Haar measures on $\Gamma$ and $X/\Gamma$, show that they define a Haar measure on $X$ satisfying $\int_X=\int_{X/\Gamma}\int_\Gamma$ (or rather, $\int_X=\int_{X/\Gamma}\sum_\Gamma$ since $\Gamma$ is discrete). Then $U\to X\to X/\Gamma$ being injective implies that the inner sum is $\leq1$, so $\mu(U)\leq\mu(X/\Gamma$.

I've got a proof here: #32672. It's not super pretty yet, but I'll work on cleaning it up over the next few days. Is there a specific sorry in the FLT repo that we're looking to close?

[Kevin Buzzard]

There's something called existsE but that's several things rolled into one. I have a draft PR which contains something closer but it contains a bunch of other stuff too. Today quite busy though

[Kevin Buzzard]

OK on branch kbuzzard-existsE-workingtowards there's not_injective_of_large_measure in FLT/DivisionAlgebra/Finiteness.lean which should be enough for the application. You can assume that $D\subset D_{\mathbb{A}}$ is countable, discrete and cocompact, and that $D_{\mathbb{A}}$ is locally compact; we either have these already or they're easy from what we have.

[Thomas Browning]

Looks like I don't even need cocompactness, just discreteness (although they are equivalent, I think).

[Kevin Buzzard]

You mean for your integral formula? I can believe it. I just need compactness to guarantee finite measure in the application. I checked today that the statement on the FLT branch is enough for me.

[Thomas Browning]

Ok, I'll clean up the PR a bit more and then look into hooking it up to not_injective_of_large_measure.

[Thomas Browning]

So looks like I will need compactness of the quotient after all. Is this known, or will I need to use an explicit compact set (e.g., a fundamental domain or something larger)?

[Thomas Browning]

Or maybe it follows from cocompactness of the adeles?

[Kevin Buzzard]

We already have compactness of the quotient. What we didn't have was the fundamental domain.

[Thomas Browning]

Yes, it's looking like this will go through just fine, I think.

[Thomas Browning]

A bit hacky, but FLT#798 now closes the sorry in not_injective_of_large_measure

[Kevin Buzzard]

It's ready for merge as far as I'm concerned, but it's failing CI because the mathlib PR part of it doesn't lint:

  /- The `defLemma` linter reports:
  INCORRECT DEF/LEMMA: -/
  -- FLT.Mathlib.MeasureTheory.Haar.Extension
  /home/runner/work/FLT/FLT/FLT/Mathlib/MeasureTheory/Haar/Extension.lean:56:1: error: @TopologicalGroup.IsSES.ofClosedSubgroup is a def, should be lemma/theorem
  /home/runner/work/FLT/FLT/FLT/Mathlib/MeasureTheory/Haar/Extension.lean:57:3: error: @TopologicalAddGroup.IsSES.ofClosedAddSubgroup is a def, should be lemma/theorem

  /- The `docBlame` linter reports:
  DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
  -- FLT.Mathlib.MeasureTheory.Haar.Extension
  /home/runner/work/FLT/FLT/FLT/Mathlib/MeasureTheory/Haar/Extension.lean:79:3: error: @TopologicalAddGroup.IsSES.pullback definition missing documentation string
  /home/runner/work/FLT/FLT/FLT/Mathlib/MeasureTheory/Haar/Extension.lean:113:3: error: @TopologicalAddGroup.IsSES.pushforward definition missing documentation string
  /home/runner/work/FLT/FLT/FLT/Mathlib/MeasureTheory/Haar/Extension.lean:224:3: error: @TopologicalAddGroup.IsSES.integrate definition missing documentation string
  /home/runner/work/FLT/FLT/FLT/Mathlib/MeasureTheory/Haar/Extension.lean:248:3: error: @TopologicalAddGroup.IsSES.inducedMeasure definition missing documentation string

and I didn't want to start fixing it because I didn't want it to diverge too much from the mathlib PR, however the mathlib PR seems shorter than the version in FLT so I didn't quite know what to do.

[Thomas Browning]

Ah, these were linting errors in the mathlib PR as well. I'll copy it over.

[Thomas Browning]

It's only longer because it has one extra theorem at the end, I think.

[Thomas Browning]

It should lint now, I think

[Kevin Buzzard]

Thanks! It's merged.

[Alex Kontorovich]

Just seeing this thread. Long ago, Heather and I constructed the classical fundamental domain for $SL(2,\Z)\backslash SL(2,\R)$, in case that API may be useful here...

[Kevin Buzzard]

That sounds much harder than what I did! It's a nonabelian setting. I was lucky enough to be in a situation where I could write down a set-theoretic fundamental domain so all the measure theory could be avoided.

[Alex Kontorovich]

Won't you eventually need $GL(2,{\mathbb Q})\backslash GL(2,{\mathbb A})$...?

[Kevin Buzzard]

One day I will, but this is certainly not a priority; we've just got compactness of $D^\times\backslash (D\otimes_F\mathbb{A}_F)^\times$ for a totally definite quaternion algebra over a totally real field (I literally hit merge under an hour ago) and this will do for now; Jacquet--Langlands is going to be assumed...

[David Loeffler]

Sorry to hijack this thread yet further, but:

@Alex Kontorovich : did you ever prove that the fundamental domain is a fundamental domain?

Despite appearances, this is a genuine question: I'm asking whether it's a theorem that the set ModularGroup.fd satisfies the predicate MeasureTheory.IsFundamentalDomain. I'm hoping to use this to set up a MeasureSpace structure on $SL(2, \mathbb{Z}) \backslash \mathcal{H}$.

[Alex Kontorovich]

We proved two theorems:

• 1) ModularGroup.exists_smul_mem_fd: any point can be moved into the (closed) domain by an element of $SL(2,\Z)$, and
• 2) ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo: if both $z$ and $\gamma\cdot z$ are in the open domain, then they're equal.
  So I think the answer to your question is Yes, but maybe not in the form you want for your application?...

[Alex Kontorovich]

@Heather Macbeth and I also had a bunch of work in progress about fundamental domains, but it never made it to Mathlib, I think?

[Kevin Buzzard]

So I was going to do this for $\mathbb{Q}\backslash\mathbb{A}_{\mathbb{Q}}$ and then I realised that to actually prove that the thing was a fundamental domain I had to check that all the overlaps/missing pieces had measure zero, and I didn't fancy that, so I changed my fundamental domain to be $\prod_p\Z_p\times[0,1)$ so that the overlaps/missing pieces were literally empty (this really is a set-theoretic fundamental domain) which was why I could prove that this thing really was an IsFundamentalDomain. I would imagine that basically what is left in the upper half plane case is to show that the closure minus the interior has measure zero but I wouldn't know how to start doing that myself (although I'm sure the experts won't have much trouble).

[Alex Kontorovich]

Of course we could do the same thing, choose boundary representatives. Though we have elliptic fixed points, so there's always a problem there... Maybe we already have that that the measure of finitely (countably) many points of a measure absolutely continuous wrt Lebesgue is zero?...

[David Loeffler]

I would imagine that basically what is left in the upper half plane case is to show that the closure minus the interior has measure zero

Indeed! I didn't realize Alex and Heather had proved the uniqueness result for mem_fdo, and with that in hand, to show that the (closed) fundamental domain $\mathcal{D}$ is a fundamental domain in the measure-theoretic sense, it would suffice to show that $\mathcal{D} \setminus \mathcal{D}^\circ$ has measure zero. I guess it's true more generally that for any open set $X$ in the plane, $\overline{X} \setminus X$ has measure zero, but I don't know if this is in mathlib.

[Riccardo Brasca]

Isn't this false? Taking the union of balls around the rationals (with radius 1/2^r around the r-th rational) gives a dense open set, so the closure minus itself has infinite measure.

[David Loeffler]

Well, that'll be why it isn't in mathlib then :man_facepalming:

[Yaël Dillies]

It is true for a convex set, however. Is your fundamental domain convex?

[David Loeffler]

No, at least not with the restriction of the Euclidean metric. (It's convex wrt the intrinsic metric of the upper half-plane, the one for which segments of circles centred on the real line are geodesics – in this metric it's a triangle – but that probably isn't useful here.)

[David Loeffler]

(this is the metric defined in Mathlib.Analysis.Complex.UpperHalfPlane.Metric)

[David Loeffler]

In the Euclidean metric it's star-convex for some choices of centre point (but not for all)

[Yaël Dillies]

Star-convex from two base points might already be enough?

[David Loeffler]

Any point that's high up enough on the imaginary axis works as a base point (trying to do a trigonometry exercise in my head I think higher than sqrt(3) is probably enough)

[Yaël Dillies]

Alternatively, can you make it convex by inverting around some circle? Inversion preserves zero measure sets

[David Loeffler]

Not as far as I am aware. Going back to your earlier claim "star-convex from two base points might already be enough", can you say more about why you expect that?

[Yaël Dillies]

Star convex from a single base point isn't enough since you could have very thin rays emanating from that single base point. Star convex from two base points however means that you get a whole triangle for every third point in your set (and it's crucial you're in 2D for that to be useful, in 3D you'd instead need three non-collinear base points)

[Alex Kontorovich]

Very interesting, thanks! Can you please point me to the API on "star convex from two base points"?

[Yaël Dillies]

There's none so far. The past few days I've been trying to come up with an (informal) formalisation of my intuition above.

[Stepan Nesterov]

Isn’t this a massive overkill for showing that a half-line and a portion of a circle have measure zero?
Unless I’m misunderstanding the current goal

[Yaël Dillies]

Oh are we talking about (half of) this shape? https://ahilado.wordpress.com/wp-content/uploads/2017/02/modulargroup-fundamentaldomain-01.png

[Yaël Dillies]

Having negligible frontier is preserved under intersection, union, complement, etc... Therefore it should be easy to do what Stepan said if this really is the shape you are interested in

[Yaël Dillies]

Alternatively, you could use the Lebesgue density theorem

[Stepan Nesterov]

Yaël Dillies said:

Oh are we talking about (half of) this shape? https://ahilado.wordpress.com/wp-content/uploads/2017/02/modulargroup-fundamentaldomain-01.png

Even if you take a congruence subgroup of $SL(2, \mathbb{Z})$ then its fundamental domain could be taken to be a finite union of translates of this shape, hence its boundary will be a finite union of half-lines and circular segments

[Stepan Nesterov]

I would hope that we don't need anything more general than that for FLT