Commit 2020-08-15 22:09 8f75f963View on Github →
feat(geometry/euclidean): circumcenter and circumradius (#3693)
Show that every simplex in a Euclidean affine space has a unique
circumcenter (in the affine subspace spanned by that simplex) and
circumradius. There are four main pieces, which all seem closely
enough related to put them all together in the same PR. Both (b) and
(c) have quite long proofs, but I don't see obvious pieces to extract
(a) Various lemmas about
orthogonal_projection in relation to points
equidistant from families of points.
(b) The induction step for the existence and uniqueness of the
(circumcenter, circumradius) pair,
(this is actually slightly more general than is needed for the
induction; it includes going from a set of points that has a unique
circumcenter and circumradius despite being infinite or not affine
independent, to such a unique circumcenter and circumradius when
another point is added outside their affine subspace). This is
essentially just a calculation using an explicit expression for the
distance of the circumcenter of the new set of points from its
orthogonal projection, but still involves quite a lot of manipulation
to get things down to a form
field_simp, ring can handle.
(c) The actual induction
exists_unique_dist_eq_of_affine_independent, giving a unique
(circumcenter, circumradius) pair for for any affine independent
family indexed by a
fintype, by induction on the cardinality of that
fintype and using the result from (b). Given (b), this is
essentially a lot of manipulation of trivialities.
(d) Extracting definitions and basic properties of
circumradius from the previous result.