Dirichlet domain

Stream: Is there code for X?

[Alex Kontorovich]

I'd like to prove the following. Given a metric space X with a discrete action by a group G, and a base point x : X, one can form the "Dirichlet polyhedron"
D := {y : α | ∀ g : G, dist x y < dist (g • x) y}. Theorem: D is a fundamental domain for the action of G. This needs a measure μ for which sets like {y : α | dist x y = dist (g • x) y} have measure zero (when g doesn't fix x). How do I make the MeasureSpace structure on X compatible with the topology generated by dist?

[Anatole Dedecker]

Compatible in what sense? docs#MeasureTheory.Measure.Regular ?

[Kevin Buzzard]

Is X locally isometric to R^n in your example Alex? I suspect it is. Does this answer the question Anatole, or is there more information needed?

[Alex Kontorovich]

Here's a mwe:

import Mathlib.MeasureTheory.Group.Action

example {X G : Type _} [MetricSpace X] [Group G] [MulAction G X] [MeasurableSpace X] (x : X) (g : G) : MeasurableSet {y : X | dist x y < dist (g • x) y} := sorry

What I'm worried about is declaring both MetricSpace X and MeasurableSpace X. The latter gives me some sigma-algebra, but I want it to be that generated by the topology induced from the metric space structure... (Does that make sense?...)

[Alex Kontorovich]

The opens should be generated from dist balls.

[Anatole Dedecker]

Ah right, you meant that the MeasurableSpace should be compatible with the topology. I thought you meant that the measure had to be compatible (because MeasureSpace contains a measure), and I wasn't sure what that would mean. Is docs#BorelSpace what you want?

[Alex Kontorovich]

Yes that's what I want, thanks! Except I think (?) I first need to generate the topology from the metric space?

[Anatole Dedecker]

No, any docs#MetricSpace comes with a topology (which is provably equal to the one you'd expect)

[Alex Kontorovich]

Here's a better mwe:

import Mathlib.MeasureTheory.Group.Action

example {X : Type _} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] (x : X) (r : ℝ) :
  MeasurableSet {y : X | dist x y < r} := sorry

[Anatole Dedecker]

That should be exactly docs#measurableSet_ball

[Anatole Dedecker]

Notice that if you only want the open sets to be measurable you don't need the full strength of docs#BorelSpace, docs#OpensMeasurableSpace is enough.

[Alex Kontorovich]

Ok thanks; now I need to know that a set of this kind is open. What kinds of techniques are available?

import Mathlib.MeasureTheory.Group.Action

example {X G : Type _} [MetricSpace X] [Group G] [MulAction G X] [MeasurableSpace X]
    [OpensMeasurableSpace X] (x : X) (g : G) :
    IsOpen {y | dist x y < dist (g • x) y} := by
  sorry

[Anatole Dedecker]

I would say docs#isOpen_lt together with docs#Continuous.dist should get you there?

[Alex Kontorovich]

Ah, perfect thanks! Just what I was looking for...

[Michael Stoll]

Just a remark on the mathematics...

Alex Kontorovich said:

D := {y : α | ∀ g : G, dist x y < dist (g • x) y}

This set is empty. I think you have to restrict to g such that g • x ≠ x (in particular, g ≠ 1).

[Alex Kontorovich]

Yes of course, thanks (I'm actually finding it easier to work with ≤ for a variety of reasons, including this one...)

[Alex Kontorovich]

Here's another question: do we have a notion of MetricPreserving (?) for a group action on a metric space, that is, that d(g • x, g • y)=d(x,y) for all g, x, y?

[Alex Kontorovich]

Namely:

class MetricPreserving (α G : Type _) [MetricSpace α] [SMul G α] :
    Prop where
  metric_preserving :
    ∀ x y : α, ∀ g : G, dist (g • x) (g • y) = dist x y

doesn't seem to exist?

[Anatole Dedecker]

docs#IsometricSMul ?

[Alex Kontorovich]

Ah, that's the one. Thanks!

[Alex Kontorovich]

Is there a better way of searching for such things (than asking on here)?

[Alex Kontorovich]

Actually, why does the class require PseudoEMetricSpace? Couldn't it be stated in the greater generality?

[Anatole Dedecker]

Well to find the class in itself I don't think there is any tool (other than guessing the name or having encountered it already), in particular I'm pretty sure exact? can't help here. But you can also search for related lemmas (here docs#dist_smul would be one example) and see the typeclasses there.

[Alex Kontorovich]

I see. edist is extended (to possibly infinite values) dist, not some euclidean thing...

[Anatole Dedecker]

Yes, PseudoEMetricSpace is the most general of the metric space variants: both non-separated (Pseudo) and with possibly infinite (E for extended) distances

[Alex Kontorovich]

I now have an actual mathematical question, perhaps for @Yury G. Kudryashov, who wrote the FundamentalDomain file: I see why you bring a measure in, to be able to say things about ae-covers, pairwise ae-disjoint, etc. But could you not also do it purely topologically, as is done, say, in Misha Kapovich's response here: https://mathoverflow.net/questions/251627/proper-discontinuity-and-existence-of-a-fundamental-domain ? Replacing the ae-conditions could be (1) D is open, or perhaps as stated there, the interior of the closure of D is D itself, (2) the G-orbit of the closure(D) is all of X, and (3) g(D) is disjoint from D for g≠1. (And perhaps local finiteness.) Is there a good reason to bring a measure into it if one doesn't have to? Thanks!

[Yury G. Kudryashov]

I don't remember why I did it this way. Feel free to rewrite. Can you prove μ (frontier U) = 0 for an open set U? Or do you need extra assumptions like convexity?

[Yury G. Kudryashov]

As a backup plan, we can have two notions of a fundamental domain: topological and measure theoretic + theorem(s) like FundamentalDomain.AEFundamentalDomain.

[Alex J. Best]

At least some of the motivation for that definition came from the Minkowski convex body proof. If you can get a purely topological version that would be nice, but I think the definition as it is right now allows both open and closed fundamental domains which is handy. I guess this could be worked in to your definition, e.g. 3) could be g(D) \cap D \subseteq frontier(D) or something like that

[Alex Kontorovich]

Yury G. Kudryashov said:

I don't remember why I did it this way. Feel free to rewrite. Can you prove μ (frontier U) = 0 for an open set U? Or do you need extra assumptions like convexity?

Yes, this is exactly the point that I'd like to avoid (in constructing Dirichlet domains); I tried poking around to find conditions on X, μ that would naturally lead to this, and realized that maybe I shouldn't be talking about μ at all...?

[Anatole Dedecker]

It indeed seems like you want two different things, then main point being that you require true set-theoretic disjointness, not ae-disjointness

[Alex Kontorovich]

Indeed. I could keep trying with the existing definition, but then I'd need to know under what general conditions does something like μ (frontier U) = 0 hold?... (I'm pretty sure doing it purely topologically would allow more general settings...?)

[Anatole Dedecker]

I think both are definitely useful, because enforcing actual disjointness is also a very strong requirement that we don't want to make all the time. And I don't really see a good generalization here.

[Anatole Dedecker]

Well actually we could have a version where "disjoint" is taken modulo docs#EventuallyEq for some filter, and then specialize it to either $\top$ or docs#MeasureTheory.Measure.ae but that doesn't unify the rest of the definition

[Yury G. Kudryashov]

Indeed, my goal was to accomodate for the Minkowskii theorem. BTW, I think that you don't need some of the constructions in the original mathlib 3 PR (didn't check - they may be gone) if you use docs#Convex.addHaar_frontier and/or docs#Convex.nullMeasurableSet