Voronoi Domains

Stream: mathlib4

[Newell Jensen]

@Xavier Roblot I am looking to add Voronoi Domians and wanted to get your thoughts on the definition I have ( #10345). This PR would be just to introduce the definition in terms of the $\mathbb{Z}$-lattice (i.e. would still need to most likely do a PR for the togological definition in a future PR).

[Newell Jensen]

I also see that @Alex J. Best was potentially thinking of adding Voronoi Diagrams for the Geometry of Numbers.

[Xavier Roblot]

I am afraid I don't know much about Voronoi domains but looking at the definition on Wikipedia what you write seems reasonable. One thing I can suggest if you plan to develop this topic is to create a new directory Algebra.Module.Zlattice, move Zlattice.lean to Zlattice/Basic.lean and put the stuff about Voronoi domains in a new file in this directory.

[Antoine Chambert-Loir]

I don't really see the relevance of having lattices in the theory of Voronoi domains. The definition makes sense in a metric space: the open cell of a point p is the locus of points which are closer to c than to any other (strictly closer), it is an open set.
There are several possible definitions for closed cells, I believe taking closure of open cells is best, but that won't give a partition in general (take a space with 3 points {0,1,2}).

[Antoine Chambert-Loir]

In a normed vector space, the cells should be convex.
If the norm is euclidean, the cells are open polyhedra. (I don't know whether Hahn-Banach suffices here, actually I don't think so, one needs finiteness of extremal points, etc.)

[Junyan Xu]

The definition currently produces an open set centered at the origin, which is a fundamental domain for translation by the lattice. This won't work in the generality of an arbitrary set. But I agree we should make the general definition, so that you can state, e.g., translating the Voronoi cell at the origin by a lattice point yields the Voronoi cell at that lattice point.

[Newell Jensen]

Junyan Xu said:

The definition currently produces an open set centered at the origin, which is a fundamental domain for translation by the lattice. This won't work in the generality of an arbitrary set. But I agree we should make the general definition, so that you can state, e.g., translating the Voronoi cell at the origin by a lattice point yields the Voronoi cell at that lattice point.

Yes, this would at least show what I was originally tending for.

In regards to fundamental domains, they are defined in regards to a $\mathbb{Z}$-lattice and also as:

"A set s is said to be a fundamental domain of an action of a group G on a measurable space α
with respect to a measure μ if

• s is a measurable set;

• the sets g • s over all g : G cover almost all points of the whole space;

• the sets g • s, are pairwise a.e. disjoint, i.e., μ (g₁ • s ∩ g₂ • s) = 0 whenever g₁ ≠ g₂;
  we require this for g₂ = 1 in the definition, then deduce it for any two g₁ ≠ g₂."

I am not much of an analyst but will take a look at what I can come up with in regards to a general definition based on different metrics/norms when I get some more time.