Voronoi diagrams

Stream: Is there code for X?

[Nicolau Oliver]

Hi, I am an undergrad computer science interested in Voronoi Diagrams. There are a lot of kinds and families of them, some sharing properties. But sometimes things in computational geometry are hard to formalize.

I am following #tpil and playing the natural number game, and really like it. But I really have no clue about how to tackle defining mathematical objects like Voronoi Diagrams, or even simpler things.

Another one I was looking foward to was the unbounded part of the Voronoi Diagrams, usually described as a circular sequence of permutations linked by adjacent transpositions.

Is there any other similar objects already in mathlib or existing lean4 code on similar topics?

[Ruben Van de Velde]

I'm thinking those are not necessarily a great concept to work on when you're just starting out

[Kevin Buzzard]

Yeah I would imagine that even just proving that given a finite set in the plane, the corresponding Voronoi cells are polygonal might be quite scary! Proof is "draw a picture and it's obvious" which will need some thought to formalise. @Joseph Myers is this easier than I think it is?

[Joseph Myers]

I'd tend to say a polygonal set is a polyhedral set in two dimensions and that polyhedral (in a real affine space) means a finite intersection of half-spaces. That "at least as close to point X as to point Y" gives a half-space should be easy to prove. If this is an unsatisfactory answer, maybe the real question is providing some other less abstract description of polygonal sets? Certainly, while such a definition makes it easy that the Voronoi cells are polyhedral, it says very little about any of the combinatorics of the diagram.

We don't have polyhedral sets in mathlib. There's an old PR #13256 that defines half-spaces (only for real inner product spaces, not for affine spaces - much of the convexity library doesn't yet handle affine spaces, but there's a review comment on that PR from July querying the need for an inner product in the definition, and it's been awaiting-author since then). On the other hand, you may not need a half-space type to define polyhedral sets, you could work directly with inequalities on the values of a linear / affine map, like some existing convexity code in mathlib.

(Definitions could be given more generally than for real affine spaces, but it's not clear the concept is useful when working over other fields and it's also less clear what the right definition of a half-space would be in such a more general context.)

[Nicolau Oliver]

Thank you very much for the answers. I would be really exited to eventually help start formalization in this small corner of mathematics/comp sci.

Seeing that some basic elements are missing, I have three follow up questions:

• Is there code formalizing the definition of a Jordan curve? Ive seen messages of people interested in formalizing the JCT in relation to planar graphs. The motivation for me would be to later define "Abstract Voronoi Diagrams" where the bisectors of any two sites are just Jordan curves with some extra axioms on number and kind of intersection.

• Is there any existing project on formalizing other geometric objects like Delaunay triangulations and associated graphs? Or is it better to first formalize planar graphs, and only later look at more complex stuff?

[Nicolau Oliver]

(deleted)

[Yaël Dillies]

Planar graphs are hard :face_with_peeking_eye:

[Vincent Beffara]

Here the embedding comes before the graph so the situation might actually be easier than abstract graphs. I would guess that Jordan curve is fine but JCT would be difficult - maybe JCT for polygonal lines would be a good project? Has it been done in Lean?