Commit 2020-06-14 19:26 797177c3View on Github →
feat(linear_algebra/affine_space): affine combinations of points (#2979)
Some basic definitions and lemmas related to affine combinations of
points, in preparation for defining barycentric coordinates for use in
This version for sums over a
fintype is probably the most convenient
for geometrical uses (where the type will be
fin 3 in the case of a
triangle, or more generally
fin (n + 1) for an n-simplex), but other
use cases may find that
finsupp versions of these
definitions are of use as well.
weighted_vsub is expected to be used with weights
that sum to zero, and the definition
affine_combination is expected
to be used with weights that sum to 1, but such a hypothesis is only
specified for lemmas that need it rather than for those definitions.
I expect that most nontrivial geometric uses of barycentric
coordinates will need to prove such a hypothesis at some point, but
that it will still be more convenient not to need to pass it to all
the definitions and trivial lemmas.