Barycentric coordinates

[benjub]

A family of results I would like to see in set.mm are basic results on barycentric coordinates (to be added by me or others). This would allow to prove some theorems around convex combinations and convex hulls, and do affine geometry.

As a first step, we can restrict attention to the case of real or complex scalars, since we have more utility lemmas for them.

The first nontrivial case is dimension 1, where I added a few years ago the computation of barycentric coordinates (see https://us.metamath.org/mpeuni/bj-bary1.html). It would be nice to have the analogue in dimension 2 (as I wrote there, I don't know if for dimension 2, it's still faster to use a "manual" approach, or if we should begin to use Cramer formulas, which are already in set.mm thanks to @avekens).

Already in dimension 2, we can prove interesting results. I think that "solid" triangles should be defined that way, that is,

(triangle with vertices $A, B, C \in \mathbb{C}=\mathbb{R}^2) =$ { $X \in \mathbb{R}^2 | \exists a, b, c \in \mathbb{R}_{\geq 0}, a + b + c = 1 \text{ and } X = a A + b B + c C$ }

as I wrote in https://groups.google.com/g/metamath/c/cqK5W6vA36Q/m/Oe03ytmQBwAJ, in view of proving the formula for the area of a triangle (a task undertaken by @tirix and Dr Jon P... ---sorry, I'm guessing the name from the email address).

The analogous result in dimension 1 is within reach thanks to https://us.metamath.org/mpeuni/bj-bary1.html. It might not be too hard to prove

${
  baryray.a $e |- ( ph -> A e. RR ) $.
  baryray.b $e |- ( ph -> B e. RR ) $.
  baryray.ab $e |- ( ph -> A < B ) $.
  $( Barycentric characterization of rays in ` RR ` (right-infinite case). $)
  baryrayr $p |- ( ph ->
                 ( A [,) +oo ) = { x e. RR | E. s e. RR E. t e. ( 0 [,) +oo )
                    ( ( s + t ) = 1 /\ x = ( ( s x. A ) + ( t x. B ) ) ) } ) $=
    ? $.
$}

Indeed, from https://us.metamath.org/mpeuni/bj-bary1.html, the condition in the class abstraction is

E. s e. RR E. t e. ( 0 [,) +oo ) ( ( s + t ) = 1 /\ x = ( ( s x. A ) + ( t x. B ) ) )
<=>
E. s e. RR E. t e. ( 0 [,) +oo ) ( s = ( ( B - x ) / ( B - A ) ) /\ t = ( ( x - A ) / ( B - A ) ) )
<=>
E. t e. ( 0 [,) +oo ) t = ( ( x - A ) / ( B - A ) )   [since we simply take s to be ( ( B - x ) / ( B - A ) ) ]
<=>
A <= x

Then, since ( -oo (,] B ) = "-" ( -u B [,) +oo ) we can use the above result with -A for B and -B for A to obtain

  $( Barycentric characterization of rays in ` RR ` (left-infinite case). $)
  baryrayl $p |- ( ph ->
                 ( -oo (,] B ) = { x e. RR | E. s e. ( 0 [,) +oo ) E. t e. RR
                    ( ( s + t ) = 1 /\ x = ( ( s x. A ) + ( t x. B ) ) ) } ) $=
    ? $.

and finally, by using the above two results and taking intersections, we obtain

  $( Barycentric characterization of segments in ` RR ` . $)
  baryseg $p |- ( ph ->
          ( A [,] B ) = { x e. RR | E. s e. ( 0 [,) +oo ) E. t e. ( 0 [,) +oo )
                    ( ( s + t ) = 1 /\ x = ( ( s x. A ) + ( t x. B ) ) ) } ) $=
    ? $.

The barycentric characterization of triangles is explained in some detail in the later message in the same thread https://groups.google.com/g/metamath/c/cqK5W6vA36Q/m/Tun_YclfBgAJ. On the way of proving it, we also get another characterization of "solid" triangles as the intersection of three half-planes.

Any takers for some/any of that ? Please share in comments what part you begin working on, in order to avoid double work.

[tirix]

Maybe another approach could be to provide proofs in a sufficient generic setting we have (like a generic left module LMod instance if it is the right setting). This was we would hit all the stones at once, and the theorems apply (almost) immediately to $\mathbb{R}$ and $\mathbb{C}$.

[benjub]

Maybe another approach could be to provide proofs in a sufficient generic setting we have (like a generic left module LMod instance if it is the right setting). This was we would hit all the stones at once, and the theorems apply (almost) immediately to R and C.

Indeed, the algebraic part is exactly the same in any vector space or even module, but I don't know if there are as many convenience lemmas already in set.mm as in the case of $\mathbb{C}$. Note that most applications of barycentric coordinates use notions of positivity and convexity, where we generally restrict to $\mathbb{R}$ (it's possible to do some stuff for ordered fields, and then there may be interesting results in non-Archimedean geometry, but I don't konw if it's worth the extra generality).