Area of a triangle (was: Help with beginning to contribute to set.mm)

[Benoit]

Following Thierry's last post on the thread "Help with beginning to contribute to set.mm".

There are many ways to characterize the set of points in a triangle. I think the simplest to state is by using barycentric coordinates:

(triangle with vertices A, B, C \in \C) = \{ X \in \C | \exists a, b, c \in \R_{\geq 0}, a + b + c = 1 and X = a A + b B + c C \}

This generalizes to all simplices in any dimension (starting with dimension 0).

By the way, I think that in your (Thierry) description, you got the opposite sign for F and your S is actually a parallelogram.

Benoit

[Jon P]

Hi Benoit, nice idea to start a new thread to talk about this stuff. This is an answer to you too Theirry :)

The goals I have been working towards with this area of a triangle stuff are 1. supporting Heron's theorem and 2. working towards Pick's theorem from the 100 list, however that is supposedly very hard so it's a long way off. 

So far I have done areaquad, to explain how it works look at the left image here. It says given a quadrilateral with sides parallel to the y-axis the area is 1/2 x. (F + E - (D + C)) x. (B - A), where those are all just single real numbers, for example the top left vertex is at (A,F) e. RR^2. If you have the situation where one side is 0 length, for example E = C, then this reduces to area = 1/2 x. (F - D) x. (B - A), which is 1/2 x. base x. height as expected. 

If you look at the right diagram you can see how any triangle can be expressed as two of these quads connected together. For this shape we get, I think, 1/2 x. (W - Y) x. (R - P). This is a slightly odd result and not how areas of triangles are usually expressed. My guess would be it would be good to take this result and then change it into a more familiar form.

I think the way area is expressed in Heron is quite natural, where the area of triangle is basically the cross product, |A||B|sin theta where A and B are two of the sides as vectors and theta is the angle between them.

Benoit I like your way of using barycentric coordinates to express the interior of the triangle, that is quite elegant. I am not sure how to fit it into this scheme though, if you look at U and V in areaquad those are the upper and lower lines of the quad and defining things parallel to the y axis makes the area calculation much easier. I was imagining continuing to use that definition but with more pieces, having the left part and the right part of the triangle defined separately, however I am aware of how inelegant that is.

Thierry I hope I have answered some questions about what the final formula would look like. I am sorry I don't understand your triangle formulation here, I think maybe you are using cross product somewhere? I like the idea of starting with just 3 complex numbers, that has a nice feel to it, and is the same as Heron.

In general I really like working collaboratively so I am grateful for all the help so far and if anyone wants to collaborate on moving these things forward I would like that, I am not so strong in metamath in general. :)

[Thierry Arnoux]

Hi Jon and Benoit,

My formula can be seen as either a change of coordinates (into a system with CA, CB as the unit vectors), or as barycentric coordinates: this shall be the same if I’m not mistaken.
The class variables E/D and F/D shall represent these coordinates and vary between 0 and 1 inside of the unit parallelogram. I just found it more elegant to have E and F vary between 0 and D, this avoids a division (and its corner cases), and results in a shorter formula.
E and F are indeed built using cross products (or matrix determinents, again, this shall be the same).

Of course Benoit is right, my formula would match the full parallelogram, it misses something like ( E + F ) e. ( 0 [,] D ) to cut it in half.

I chose this representation because, as Benoit says, I suspect it is rather compact.
Another way may be to see the triangle as the intersection of 3 half planes and write S = { <. x , y >. | ( ph /\ ps /\ ch ) } where ph, ps and ch are the formula for each half plane.

Jon, do you plan your final statement formula to still require to have the three points ordered with abscisses in ascending order? I’m still interested to see it. In full, like my attempt.

BR,
_
Thierry

[Benoit]

On Tuesday, June 4, 2019 at 11:15:03 AM UTC+2, Jon P wrote:

Benoit I like your way of using barycentric coordinates to express the interior of the triangle, that is quite elegant. I am not sure how to fit it into this scheme though,

The points "inside" the triangle with vertices A, B, C are also characterized as follows: the points A, B define a line, and I want the point X to be in the half-plane with boundary the line (AB) and containing C (this is easily expressed algebraically, see below); similarly for the other two half-planes. This characterization is likely easier to compute areas.  Therefore, as a first step, and before computing areas, I would formalize this equivalence of the two characterizations in metamath, using the representation of the plane as the set of complex numbers.

For instance, in "pseudo-metamath":

df-triangle $a |- triangle = ( <. x, y, z >. e. ( C. X. C. X. C. ) |-> { u e. C. | E. a e. R. E. b e. R. E. c e. R. ( 0 =< a /\ 0 =< b /\ 0 =< c /\ a + b + c = 1 /\ u = a x + b y + c z } )

Then I would prove the permutation formulas (easy):
A, B, C e. C => triangle (A, B, C) = triangle (B, C, A) = triangle (C, A , B) = triangle (A, C, B) =...

Finally, I would prove the above equivalence.  First, define the vector product vec : C. X. C. --> R. Then, prove:

triangle-charac $p |- ( X e. triangle (A, B, C) <->
( 0 <= ( ((B-A) vec (C-A)) x. ((B-A) vec (X-A)) ) /\
  0 <= ( ((C-B) vec (A-B)) x. ((C-B) vec (X-B)) ) /\
  0 <= ( ((A-C) vec (B-C)) x. ((A-C) vec (X-C)) ) ) $= ? $.

Of course, this necessitates several lemmas and will be long. You first prove the implication to the right by proving
trianglelem $p |- ( X e. triangle (A, B, C) -> 0 <= ( ((B-A) vec (C-A)) x. ((B-A) vec (X-A)) ) ) $= ? $.
which should be long but straightforward algebraic manipulation.  The ohter two are then obtained thanks to triangle(A, B, C) = triangle (C, A, B) etc.
The converse implication might be harder: every point in the plane can be written using barycentric coordinates summing up to 1; then the three half-plane conditions will impose that the coefficients are nonnegative.

Note: informally, the implication to the right is easy: changing notation, let a x + b y + c = 0 be the equation of the line (AB).  If you plug in for (x, y) the coordinates of a point expressed as a barycentric mean of A, B, C (say, with coefficients s, t, u >= 0), then, using the fact that A and B are indeed on the line (AB) so satisfy the equation, one has:
a (s xA + t xB + u xC) + b (s yA + t yB + u yC) + c (s + t + u) = a u xC + b u yC + c u = u (a xC + b yC + c) has the same sign as a xC + b yC + c.

Benoit

[Jon P]

Looks like some nice ideas here. Thierry I will try to write out what I had thought in full, some detail may be missing I think.

Take 3 points in CC (though RR^2 could work too), say A, B, C. I was thinking the first step is to relabel them X,Y,Z such that Re(X) <_ Re(Y) <_ Re(Z), I am not sure if this is possible in metamath, so yes getting the abscisses in ascending order. This diagram on the right might help. I

Then when they are in ascending order define three interpolation functions as before

I(x) = ( x - Re(Z) ) / ( Re(Z) - Re(X) )      [whole interval]

J(x) = ( x - Re(Y) ) / ( Re(Y) - Re(X) )     [left section]

K(x) = ( x - Re(Z) ) / ( Re(Z) - Re(Y) )     [right section]

Lets assume that Y is below the line X -> Z. Define the midpoint on the longer side

W = X + ( I(Re(Y)) x. Z )

Define the 4 bounding lines:

U1 = X + J(x) x. ( W - X )

V1 = X + J(x) x. ( Y - X )

U2 = W + K(x) x. ( Z - W )

V2 = Y + K(x) x. ( Z - Y )

Then define the interior of the triangle as

triangle(X,Y,Z) = { t e. CC | ( Re(X) <_Re(t) <_ Re(Y) /\  t e. ( V1 [,] U1) ) \/ ( Re(Y) <_Re(t) <_ Re(Z) /\  t e. ( V2 [,] U2) ) }

so basically you define the interior piecewise in the same way as area quad, just setting the left section and right section separately. This would mean it would be not so hard to then use area quad on both pieces to get the area of the triangle. However I think there may be some problems with defining each of the 5 cases.

I think it might be possible to prove the equivalence of this definition with Benoit's or yours (they are the same set), and then we could use both, this one for ease of proving the area and a nice one for more public consumption.

I am very happy to change direction if there is a better one, I know this is a bit scrappy, I hope it is helpful.

[Thierry Arnoux]

Hi Jon,

Yes, I think that’s the right approach.

I believe once you have the full statement, you start from your triangle, rewrite it as a union, and then apply “itgsplit”.

In order to handle the “without loss of generality” (like in “without loss of generality, we can assume that the abscisses are in ascending order”), in set.mm, one could first prove the specific theorem in the case X <_ Y <_ Z, as a lemma, and then in the main proof, use mpjaodan type of theorem to produce the 6 different cases, whereas each case can be proved with the lemma.

BR,

_

Thierry

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/026a3372-99f9-4a8b-960f-1cb9d67e5adb%40googlegroups.com.

[Jon P]

Thanks Theirry, sounds like a good plan.

I proved this today as a first step towards itgsplit, does anyone have suggestions for a better name for it than splitrr, or should it be rrsplit? Also does this result already exist and I couldn't find it? 

splitrr.1 $e |- Q e. RR $.

splitrr.2 $e |- R = ( -oo (,] Q ) $.

splitrr.3 $e |- S = ( Q [,) +oo ) $.

splitrr $p |- RR = ( R u. S ) $=

Full text here if interested.

[Thierry Arnoux]

Hi Jon,

Looks good, though it probably would have been shorter with ~ ioojoin or some similar theorem.

_

Thierry

--

You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e19fae0b-6fc3-481f-bce0-4cf22be6e4ad%40googlegroups.com.

[Thierry Arnoux]

I was thinking about something like this:

https://pastebin.com/SFyGskvW

But then I found that this misses the ~ ioounsn. ;-)

I'd suggest to make your theorem slightly more generic, like

|- ( ( ( A e. RR* /\ B e. RR /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) u. ( B [,) C ) ) = ( A (,) C ) )

Then it is in the form of the other theorems and could be named e.g. ~ iocunico.

Sorry for the short post answering to my own post!

[Jon P]

Ok yeah I did iocunico, as you say up to the fact that ioounsn is missing, so I might try that tomorrow. I think maybe this is all a bit convoluted as I think ixxun maybe has this in greater generality, however it is not so simple to understand and use I think.   

[Jon P]

I proved iocunico today so that is a nice step forwards :) I'm hopeful using itgsplit to prove the following is now possible. Not sure if I should prove R i^i S = { Q } seperately.

50:: |- A e. dom area

51:: |- Q e. RR

52:: |- R = ( -oo (,] Q )

53:: |- S = ( Q [,) +oo )

54:: |- B = { <. x , y >. | ( <. x , y >. e. A /\ x e. R ) }

55:: |- C = { <. x , y >. | ( <. x , y >. e. A /\ x e. S ) }

QED:: ( area ` A ) = ( area ` B ) + ( area ` C )

[Jon P]

Hey I think I made some progress on linking Benoit's definition of a triangle with the "vertical slices" one which I posted on Jun 5. Here is a diagram of a point in a triangle. Assume A,B,C are vectors in RR^2 or in CC, I think it works the same. This is the case where the right side of the triangle is vertical, the case where the left side is vertical is basically the same, any triangle is the union of two triangles, one which a straight right side and another with a straight left side.

If we start with the vertical slices approach we know that P = (xA + yC) + zy (B - C) where x + y = 1 and z <_ 1. That is you start at the point xA + yC and go up some amount vertically, which is (B-C), but sufficiently little that you don't leave the top of the triangle. 

We can rearrange this to P = xA + zy B + ( y - zy) C and this satisfies Benoit's defintion, that a point is in the triangle if P = alpha A + beta B + gamma C and alpha + beta + gamma <_ 1 because x + zy + y -zy = x + y = 1. We know x >_ 0 and y >_ 0 by definition and with z <_ 1 we know y - zy >_ 0 so alpha, beta, gamma >_0.

Likewise given a point P = alpha X + beta y + gamma Z where alpha + beta + gamma <_ 1 we can rewrite this as P = xA + zy B + (y - zy) C, where x = alpha, zy = beta and y - zy = gamma. Then rearrange so that P = xA + yC + zy (B - C). We know that x + y = alpha + beta + gamma <_ 1 and we know that zy = beta <_1 so this point is in the triangle by the vertical slices definition.

How do we know z,y > 0? We are just solving zy = beta simultaneously with y - zy = gamma. If you sum these you get y = beta + gamma > 0 and then z = beta / y > 0.

Apologies this is all quite loose and wordy as usual, I'd appreciate any feedback from anyone who is interested, do you agree this could be formalised to show the equivalence of the two definitions? I haven't thought about your definition Thierry and I think a similar proof would be possible.

[Benoit]

Jon, you're on the right track but this looks overly difficult.  The key property is "associativity of convex combinations", which means that if a point P is a convex combination of B and C, and Q is a convex combination of A and P, then Q is a convex combination of A, B, C (and you can easily compute the coefficients), and conversely, if a point Q is a convex combination of A, B, C, then there exists a point P which is a convex combination of B and C such that Q is convex combination of A and Q (again, easily computable coefficients).

The thing is that these easy algebraic computations are cumbersome in metamath.  I just proved bj-bary1: it shows that given two distinct points A, B in an affine line (here, the complex line), any point X has unique normalized barycentric coordinates ("normalized" in the sense of "summing to 1"), with the given expressions.  One could do the same in two dimensions (starting with three non-collinear points A, B, C); it would be a bit easier (and sufficient for our purpose) to restrict to real coefficients: the expression of the coefficients is then a bit easier, and their positivity is seen to be equivalent to the positivity of the vector products I mentioned above (e.g. AB vec AX).

As a warmup for the equivalence of positivity, you could prove in metamath the following: if A < B are real numbers, then
  [A, B] = { x | E. s e. RR E. t e. RR ( s >= 0 /\ t >= 0 /\ s + t = 1 /\ x = sA + tB ) }
From the expressions in bj-bary1, you see that t >= 0 if and only if x >= A and s >= 0 if and only if x <= B.  In two dimensions, it will be the same: one of the three barycentric coordinates will be positive if and only if the corresponding vector product is positive (this corresponds to the point X being in a half-plane).

Honestly, I think that the approach you are following is not the best since it's too coordinate-dependent.  The correct way to prove these areas would be to first prove that area is invariant under displacements (rotations, translations, reflections), so that you can then suppose that your triangle has one vertex at (0, 0), one at (a, 0) with a > 0, and the third at (b, c) with c > 0, and then its area is ac/2.  Obviously, the invariance under displacements is much harder to prove, but this is the correct way to go.

Benoit

[Thierry Arnoux]

Here what could be a "grand plan for the area of the triangle":

• progress in the "Geometry" part of set.mm until triangles are defined. There is already a definition of congruence for triangles ( ~ trgcgr)
• progress in the "Geometry" part of set.mm until a distance/metric is defined, for segment lengths. This is further away, down the path.
• define a function for rectangles, to be the product (in RR) of their length and width.
• construct an outer measure based on that function (Method I, Monroe), and derive a measure: that's the generic ` area ` measure of surfaces!
  
• prove that triangles are area-measurable (e.g. first prove that half-planes are measurable, then any intersections of them)
• prove the formula for the area of a rectangle triangle, then of any triangle (as half of base times height)
  

Anything less generic than this is too specific! ;-)

Once we have proven that ` CC ` can be seen as a specific Euclidean planar geometry, we can prove that the current definition of ` area ` and the very general one match on their common domain of definition.

But of course all of this is quite far away. In the mean time, it's pretty fine to work with coordinates!

[Thierry Arnoux]

On 09/06/2019 22:03, Jon P wrote:

> This is the case where the right side of the triangle is vertical

Actually what you describe works fine even if the "right" side of the
triangle is not vertical!

[David A. Wheeler]

On Mon, 10 Jun 2019 09:02:00 +0800, Thierry Arnoux <thierry...@gmx.net> wrote:
> Here what could be a "grand plan for the area of the triangle":

Cool!

> Once we have proven that ` CC ` can be seen as a specific Euclidean
> planar geometry, we can prove that the current definition of ` area `
> and the very general one match on their common domain of definition.

I'm hoping we can create a proof that ` CC ` can be seen as a specific
Euclidean planar geometry so that all our CC-related proofs can be
immediately show to apply to any plane & vice versa.
I suspect that's a while yet :-).

--- David A. Wheeler

[Jon P]

Hi Thierry, that grand plan sounds cool. Is what I'm doing helpful towards it? I hope it is something to build on. 

Benoit, thanks for your thoughtful response. It sounds like some general result for "associativity of convex combinations" would be pretty useful for proving the equivalence of these two triangle definitions, I'm glad it's something that might be possible.

Proving "that area is invariant under displacements (rotations, translations, reflections)" sounds like a very nice program. Looking at areaval I think maybe translations will be relatively straightforward, as it's just shifting the integral along the x and y directions. However I am not sure how to begin on rotations or (arbitrary) reflections. 

I am not sure that it will simplify things particularly though. For example " suppose that your triangle has one vertex at (0, 0), one at (a, 0) with a > 0, and the third at (b, c) with c > 0, and then its area is ac/2". The issue here is that computing the area of such a triangle is still non-trivial. It could be done using this triangle splitting method I am working on, however this method can compute the area for any triangle (I think). If you transform a triangle such that one side is vertical then areaquad will work however proving that was not easy. So I am not sure, considering the work which is already done, that this method would be easier. 

Maybe there is some much superior method for computing areas however I am not sure what it is. Thanks :)

[Junyan Xu]

The set of convex combinations of a set of points (i.e. the convex hull of the set of points) is characterized by the followings:
(1) it is convex and contains the set of points.
(2) it is contained in any convex set (subset of the underlying space) that contains the set of points.

[Benoit]

I added a github issue at https://github.com/metamath/set.mm/issues/3747 related to parts of this thread.

Benoît