Polygons PR

Stream: PR reviews

[A. M. Berns]

Hello,
I just submitted this PR defining Polygons. This is my first mathlib PR so some of the stylistic choices might not be ideal, but I wanted to quickly explain them here and invite discussion. Polygons are defined as generally as possible. The type P of the points must an affine space to define the edges in multiple useful ways. The RealModulesection provides some definitions that only work in the common setting where the ambient space is a module over the reals. The EuclideanPolygon extends Polygon for the case when the ambient space is EuclideanSpace ℝ (Fin 2), and EuclideanTriangle extends further to the case n = 3. I chose to require noncollinearity for a EuclideanTriangle to allow for interconversion with Affine.Triangle. Existing results in EuclideanGeometry play well with these definitions, e.g. it is simple to prove the law of cosines for EuclideanTriangles using the existing EuclideanGeometry.law_cos.

After establishing these basic definitions, I have two ideas for rich areas building on this framework. The first is proving more triangle theorems in a separate EuclideanTriangle file, including both conversions of existing proved facts in a general affine context in EuclideanGeometry and a good context for unformalized theorems like Ceva's Theorem. The second is working with the area of polygons. In order to move toward introducing area, I also have a file SimpleEuclideanPolygons about EuclideanPolygons with the additional simplicity properties that no two vertices are adjacent, all non-consecutive edges are disjoint, and any two consecutive edges intersect only at their shared vertex. This file contains a working proof that SimpleEuclideanPolygons have a bounded interior as expected, but it takes the general Jordan Curve Theorem as an axiom, so I don't know how Mathlib would feel about that.

[Kim Morrison]

For now just take the JCT as a hypothesis rather than an axiom!

[Violeta Hernández]

Actually, I don't think we should be talking about interiors of polygons before we have at the very least the polygonal version of the Jordan curve theorem. Otherwise we're going to have to carry that hypothesis around everywhere.

[Violeta Hernández]

Is there any progress on that? I hear that there's elementary-ish proofs in the case of polygons.

[Violeta Hernández]

I'd just like to warn that polygons are a very tricky thing to work with, despite how intuitive they might look. There's a reason we don't yet have them in Mathlib.

[Johan Commelin]

Violeta Hernández said:

Otherwise we're going to have to carry that hypothesis around everywhere.

Can you just variable [JCT] at the top of the file?

Hopefully that makes it almost transparent. And then when JCT is filled in, we can just remove that line (plus epsilon inevitable fixes).

[Snir Broshi]

Violeta Hernández said:

Is there any progress on that? I hear that there's elementary-ish proofs in the case of polygons.

I'd really love to do this (this is the elementary-ish proof I know), but I'm not sure we should. I thought we're waiting for algebraic-geometry to prove the full theorem, and that proving JCT without it (even just for polygons) won't be accepted.

[Snir Broshi]

btw do we have a statement of JCT that was checked by experts?

[A. M. Berns]

Snir Broshi said:

btw do we have a statement of JCT that was checked by experts?

This is what I'd like to know too. I think polygon area depends fundamentally on the JCT, so it's ok to carry that around as a hypothesis and then replace and fix once the JCT is formalized, like @Johan Commelin said. But that requires a good formulation of the JCT that will be the one actually formalized later.

[Violeta Hernández]

You don't need JCT to define polygon areas, though you probably want it anyways. Here's me talking about this three weeks ago: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Pick's.20Theorem/near/566191613

[A. M. Berns]

Personally I think it makes more sense to bake in the JCT than to make area definitionally equal to shoelace

[Violeta Hernández]

Maybe we can have both? Define a signedArea via shoelace, a normal area via JCT, and then prove the shoelace formula |signedArea| = area (for simple polygons)

[A. M. Berns]

Yes that's more what I was thinking. That makes the shoelace theorem an actual theorem. Also, this open PR will definitely be relevant to defining the area of polygons.

[Albert Smith]

Given winding numbers of continuous curves (which I don't think Mathlib has atm?) there is a third definition windingArea where you integrate the function mapping p to the winding number of the polygon about p, which coincides with signedArea for not-necessarily-simple polygons, and this seems like a natural intermediary between the two other definitions since |windingArea| = area is "easy" for Jordan curves

[Snir Broshi]

A. M. Berns said:

Also, this open PR will definitely be relevant to defining the area of polygons.

FYI if you write the PR number explicitly a bot will show the PR's status in an emoji reaction:
#34697
(if you mention multiple PRs it will show the status of the first one I believe)

[Snir Broshi]

First polygons PR: #34393

[Snir Broshi]

Nondegeneracy and triangles: #34598

[Snir Broshi]

Simple polygons and boundary map: #35069

[Snir Broshi]

btw the last PR doesn't have the dependency setup correctly for the dependencies bot to detect (so it would add the label blocked-by-other-PR). Try this format: - [ ] depends on: #34598

[A. M. Berns]

Thanks for the tips!