Area of a polygon

Stream: new members

[Jeremiah Peterson]

I am new to lean and working on implementing the solutions to competition math problems.
Is there a good way to describe and prove the area of a polygon? I haven't been able to think of a pathway to prove something like "the area of the rectangle given by (0,1),(-1,0),(0,-1),(1,0) is equal to 2".
The area could maybe be described with MeasureTheory.volume and convexHull, but I'm not sure where to proceed since I can't find an implementation of the Shoelace formula, or figure out how to convert the area to a bounded integral of 1, split into triangles and compute the area of triangles, etc.

[Jireh Loreaux]

I realized I misread the rectangle.

[Jireh Loreaux]

I'm fairly certain that we don't have the shoelace formula yet. Maybe the right approach here is to consider a LinearIsometryEquiv which performs the rotation by π/4. This will preserve convexHulls because its linear, and volumes (on the EuclideanSpace ℝ 2) via docs#LinearIsometryEquiv.measurePreserving. Then you can show that the (rotated) convex hull is equal to Icc (-√2) √2 ×ˢ Icc (-√2) √2 from which you can easily compute the measure (here docs#PiLp.volume_preserving_equiv will be helpful, along with docs#MeasureTheory.Measure.volume_prod and docs#MeasureTheory.Measure.prod_prod)