Commit 2020-08-23 14:51 d80f3ef3

feat(geometry/euclidean): Monge point and orthocenter (#3872) The main purpose of this PR is to define the orthocenter of a triangle. Simplices in more than two dimensions do not in general have an orthocenter: the altitudes are not necessarily concurrent. However, there is a n-dimensional generalization of the orthocenter in the form of the Monge point of a simplex. Define a Monge plane to be an (n-1)-dimensional subspace that passes through the centroid of an (n-2)-dimensional face of the simplex and is orthogonal to the opposite edge. Then the Monge planes of a simplex are always concurrent, and their point of concurrence is known as the Monge point of the simplex. Furthermore, the circumcenter O, centroid G and Monge point M are collinear in that order on the Euler line, with OG : GM = (n-1) : 2. Here, we use that ratio as a convenient way to define the Monge point in terms of the existing definitions of the circumcenter and the centroid. First we set up some infrastructure for dealing with affine combinations of the vertices of a simplex together with its circumcenter, which can be convenient for computations rather than dealing with combinations of the vertices alone; the use of an inductive type points_with_circumcenter_index seemed to be more convenient than other options for how to index such combinations. Then, a straightforward calculation using inner_weighted_vsub shows that the point defined in terms of the circumcenter and the centroid does indeed lie in the Monge planes, so justifying the definition as being a definition of the Monge point. It is then shown to be the only point in that intersection (in fact, the only point in the intersection of all the Monge planes where one of the two vertices needed to specify a Monge plane is fixed). The altitudes of a simplex are then defined. In the case of a triangle, the orthocenter is defined to be the Monge point, the altitudes are shown to equal the Monge planes (mathematically trivial, but involves quite a bit of fiddling around with fin 3) and thus the orthocenter is shown to lie in the altitudes and to be the unique point lying in any two of them (again, involves various fiddling around with fin 3 to link up with the previous lemmas). Because of the definition chosen for the Monge point, the position of the orthocenter on the Euler line of the triangle comes for free (not quite rfl, but two rewrites of rfl lemmas plus norm_num).