Pick's Theorem

Stream: Is there code for X?

[A. M. Berns]

I've recently finished working through most of Mathematics in Lean as fun personal study, and I'd like to begin contributing to mathlib. Like many others, I am drawn to the 100 theorems list, so I'd like my contributions to be oriented towards formalizing one of the remaining ones. From a relatively cursory search, I see little discussion of Pick's Theorem in the Zulip and few of the relevant objects defined in mathlib. Is anyone working on Pick's Theorem? If so, what would be the most valuable way for me to start helping to formalize it? If not, would it be appropriate for me to just start defining relevant objects and building up lemmas to try to eventually PR to mathlib?

[Joseph Myers]

There may not be much discussion of Pick's theorem, but there is various past discussion of how to define polygons (one of those informal concepts that can end up meaning many different formal things). Once you have a good definition of polygons, you can then link it to measure theory for the area.

[Joseph Myers]

#Proofs from the book > Amsterdam @ 💬 has my suggestions for how API for polygons should be set up.

[Joseph Myers]

As for areas, there are various past discussions of how it would make sense in general to use 2-dimensional Hausdorff measure for areas (so you can talk about areas of surfaces, or relate the volume of a tetrahedron to the area of a face without needing to move back and forth between spaces and subspaces). And, consequently, of Hausdorff measure normalization since the definition we have doesn't match Lebesgue measure when using the Euclidean metric (it does when using the sup metric). But for an intrinsically two-dimensional leaf result such as Pick's theorem, it's probably reasonable enough to use Lebesgue measure directly rather than getting into the Hausdorff measure issues. And since Pick is explicitly about lattice polygons, it's probably also reasonable to do it directly in EuclideanSpace rather than an arbitrary affine space for a real inner product space, in which case you don't run into the issue of not having the appropriate instances for volume on an affine space.

[Joseph Myers]

Though for defining a general concept of "area of a polygon", the Hausdorff measure definition would be the desirable one to be meaningful for a polygon whose vertices are coplanar but where the ambient space is of more than two dimensions.

[A. M. Berns]

Thank you for the replies! To confirm I'm reading you right, it would be at least a productive start to define polygons very minimally, but then work essentially exclusively in EuclideanSpace and with the simpler Lebesgue version of area and start defining basic properties and building up basic theorems about specifically polygons in $\R^2$?

[Joseph Myers]

Yes. I think using EuclideanSpace makes sense for those geometry results that explicitly refer to coordinates, which includes Pick's theorem since it's about polygons with integer vertex coordinates (whereas geometry results not involving coordinates belong in a more general affine space context). And I expect the main results needed about areas to be (a) the area of a triangle with integer vertices not containing any integer points except for its vertices is always 1/2 and (b) that joining two polygons with disjoint interiors along their shared edges adds their areas - which should be straightforward to transfer from one measure to another once you have a lemma that the two measures agree. (Probably plus lots of small API lemmas I haven't thought of.)

[Joseph Myers]

When building up basic lemmas / definitions about polygons (you probably need a lot that don't mention area at all), at least consider what the actual requirements for each result are - don't restrict the ambient space to the Euclidean plane for lemmas that don't need it.

[Violeta Hernández]

I feel like it's going to be really painful to try and deal with areas of polygons without having the Jordan curve theorem.

[Violeta Hernández]

It is possible to define the area of a polygon independently of any topological constraints, via the shoelace formula. This also gives semi-sensible results for non-simple polygons. But of course, proving that this matches the Lebesgue measure of the interior of a simple polygon is another thing entirely.

[Violeta Hernández]

(In fact, it's even possible to define the volume of a general polytope without regards for topology. I did that in this random blog post two years ago.)

[Joseph Myers]

Map the polygon to the affine subspace spanned by the vertices (in the general case where the vertices are coplanar but the ambient space is possibly of higher dimension), take the union of the bounded connected components of the complement of the boundary of the polygon, and take the area of that. That's a mathematically at least somewhat reasonable definition, and it doesn't depend on the Jordan curve theorem to write down the definition, just to turn "union of the bounded connected components" into "the single bounded connected component (whose boundary is the boundary of the polygon)".

[Joseph Myers]

Of course then you need to figure out how to go between such a definition based on Lebesgue measure and whatever is most convenient for proving Pick's theorem (or any other result about areas you want to prove).

[Violeta Hernández]

Do note that the shoelace formula doesn't match the "union of bounded connected components" formula in the case of most non-simple polygons. Shoelace counts the area of each region depending on its winding number.

[Violeta Hernández]

For a non-planar polygon, the shoelace formula can be used to give you a multivector-valued result, though that's probably nothing more than a mathematical curiosity.

[Violeta Hernández]

Joseph Myers said:

Map the polygon to the affine subspace spanned by the vertices (in the general case where the vertices are coplanar but the ambient space is possibly of higher dimension), take the union of the bounded connected components of the complement of the boundary of the polygon, and take the area of that. That's a mathematically at least somewhat reasonable definition, and it doesn't depend on the Jordan curve theorem to write down the definition, just to turn "union of the bounded connected components" into "the single bounded connected component (whose boundary is the boundary of the polygon)".

This won't match the shoelace formula, to be clear. Shoelace is the same as the integral of the winding number of the curve with respect to P, over all points P in the plane. That is to say, some regions will be counted more than once, or zero times, or a negative amount of times. Meanwhile your approach just counts every point once or zero times.

[James E Hanson]

Pick's theorem was recently formalized in Isabelle/HOL. You could try looking at how they approached it.

[Joseph Myers]

Shoelace gives signed area, and requires a choice of orientation (of a two-dimensional space containing the vertices) to determine the sign. The topological approach gives unsigned area (and Pick definitely seems to be about unsigned area). Proving that, for a simple polygon, unsigned area is the absolute value of signed area probably has a lot of overlap with proving the polygonal Jordan curve theorem.