Geometry Of Numbers

Stream: Is there code for X?

[Sahil Sharma]

What is the status of theorems like, Minkowski's theorem, Pick's Theorem and Blichfeldt's theorem have they been formalised yet?

[Thomas Browning]

#2819

[Sahil Sharma]

Thomas Browning said:

#2819

https://leanprover-community.github.io/100-missing.html

Oh, so I guess this list is no longer reliable?

[Thomas Browning]

Usually we would update the list once the pull request is merged into mathlib, I think.

[Yaël Dillies]

I am still working towards making #2819 hit mathlib but work is happening in the dependent PRs.

[Johan Commelin]

It seems that progress is blocked by #17775 atm

[Yaël Dillies]

Yes indeed. I was away for the past two weeks, so I had very little Lean time. I should be able to make #17775 mergeable tonight.

[Alex J. Best]

I also started work on the minkowski proof of pick for "fundamental triangles" or whatever you call them somewhere. I'm not yet sure what the best way to approach the general Pick's theorem is, i.e. how to describe a simple polygon with lattice vertices in the plane most usefully

[Johan Commelin]

@Yaël Dillies What's the status with #17775?

[Yaël Dillies]

The status is that I have a fix in local.

[Johan Commelin]

Let's apply a local-to-global principle!

[Yaël Dillies]

Update: The Gitpod it was on expired yesterday apparently :rofl:

[Yaël Dillies]

It's fine, I can do it again. Shouldn't take too long.

[Joseph Myers]

Alex J. Best said:

I also started work on the minkowski proof of pick for "fundamental triangles" or whatever you call them somewhere. I'm not yet sure what the best way to approach the general Pick's theorem is, i.e. how to describe a simple polygon with lattice vertices in the plane most usefully

I think polygons are something that will end up needing multiple types, and predicates on them and functions for converting between them, simply because different contexts where polygons are used may have different expectations for the information needed and the well-behavedness conditions involved. For some purposes maybe a cycle of points (in an affine space for a real topological vector space - ignoring for now more general contexts such as polygons in hyperbolic space or on a sphere) is appropriate, for others maybe you want to index the points by fin n. For some purposes self-intersections may be allowed, for others not. For some you may allow a degenerate 0-gon or 1-gon or 2-gon, for others not. For some you may allow the angle at a point to be 0 or pi, for others not. For some it may be OK for consecutive vertices to be equal, for others not. For most purposes you probably want the vertices to be coplanar (but maybe allow an ambient space of more than two dimensions, polygons in three dimensions have plenty of uses e.g. in relation to polyhedra). For any of the above there's then the question of what the right way is to define the interior of the polygon so as to define its area, though once the boundary is required to be a simple closed curve all reasonable definitions should end up equivalent. If you're doing something that generalizes to polyhedra (which Pick doesn't), maybe you don't want anything involving a cyclic order on vertices at all, but just a polyhedral or semipolyhedral set (finite intersection of half-spaces or finite union of such finite intersections), with whatever conditions you need for that to be well-behaved for the purposes of your result - or to start with an abstract polytope.

[Yaël Dillies]

Pushed a fix to #17775

[Johan Commelin]

@Yaël Dillies Thanks! I see that Eric already left a review.