Commit 2020-08-15 22:09 8f75f963

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 from them. (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, exists_unique_dist_eq_of_insert (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 circumcenter and circumradius from the previous result.