Monge point and orthocenter
This file defines the orthocenter of a triangle, via its n-dimensional generalization, the Monge point of a simplex.
Main definitions
monge_pointis the Monge point of a simplex, defined in terms of its position on the Euler line and then shown to be the point of concurrence of the Monge planes.monge_planeis a Monge plane of an (n+2)-simplex, which is the (n+1)-dimensional affine subspace of the subspace spanned by the simplex that passes through the centroid of an n-dimensional face and is orthogonal to the opposite edge (in 2 dimensions, this is the same as an altitude).altitudeis the line that passes through a vertex of a simplex and is orthogonal to the opposite face.orthocenteris defined, for the case of a triangle, to be the same as its Monge point, then shown to be the point of concurrence of the altitudes.
References
- https://en.wikipedia.org/wiki/Altitude_(triangle)
- https://en.wikipedia.org/wiki/Monge_point
- Małgorzata Buba-Brzozowa, The Monge Point and the 3(n+1) Point Sphere of an n-Simplex
The Monge point of a simplex (in 2 or more dimensions) is a generalization of the orthocenter of a triangle. It is defined to be the intersection of the Monge planes, where a Monge plane is the (n-1)-dimensional affine subspace of the subspace spanned by the simplex that passes through the centroid of an (n-2)-dimensional face and is orthogonal to the opposite edge (in 2 dimensions, this is the same as an altitude). 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 to define the Monge point (so resulting in a point that equals the centroid in 0 or 1 dimensions), and then show in subsequent lemmas that the point so defined lies in the Monge planes and is their unique point of intersection.
Equations
- s.monge_point = (↑(n + 1) / ↑(n - 1)) • (finset.centroid ℝ finset.univ s.points -ᵥ s.circumcenter) +ᵥ s.circumcenter
The position of the Monge point in relation to the circumcenter and centroid.
The Monge point lies in the affine span.
The weights for the Monge point of an (n+2)-simplex, in terms of
points_with_circumcenter.
monge_point_weights_with_circumcenter sums to 1.
The Monge point of an (n+2)-simplex, in terms of
points_with_circumcenter.
The weights for the Monge point of an (n+2)-simplex, minus the
centroid of an n-dimensional face, in terms of
points_with_circumcenter. This definition is only valid when i₁ ≠ i₂.
Equations
- affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter i₁ i₂ affine.simplex.points_with_circumcenter_index.circumcenter_index = (-2) / ↑(n + 1)
- affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter i₁ i₂ (affine.simplex.points_with_circumcenter_index.point_index i) = ite (i = i₁ ∨ i = i₂) (↑(n + 1))⁻¹ 0
monge_point_vsub_face_centroid_weights_with_circumcenter is the
result of subtracting centroid_weights_with_circumcenter from
monge_point_weights_with_circumcenter.
monge_point_vsub_face_centroid_weights_with_circumcenter sums to 0.
The Monge point of an (n+2)-simplex, minus the centroid of an
n-dimensional face, in terms of points_with_circumcenter.
The Monge point of an (n+2)-simplex, minus the centroid of an n-dimensional face, is orthogonal to the difference of the two vertices not in that face.
A Monge plane of an (n+2)-simplex is the (n+1)-dimensional affine
subspace of the subspace spanned by the simplex that passes through
the centroid of an n-dimensional face and is orthogonal to the
opposite edge (in 2 dimensions, this is the same as an altitude).
This definition is only intended to be used when i₁ ≠ i₂.
Equations
- s.monge_plane i₁ i₂ = affine_subspace.mk' (finset.centroid ℝ {i₁, i₂}ᶜ s.points) (submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}).orthogonal ⊓ affine_span ℝ (set.range s.points)
The definition of a Monge plane.
The Monge plane associated with vertices i₁ and i₂ equals that
associated with i₂ and i₁.
The Monge point lies in the Monge planes.
The direction of a Monge plane.
The Monge point is the only point in all the Monge planes from any one vertex.
An altitude of a simplex is the line that passes through a vertex and is orthogonal to the opposite face.
Equations
- s.altitude i = affine_subspace.mk' (s.points i) (affine_span ℝ (s.points '' ↑(finset.univ.erase i))).direction.orthogonal ⊓ affine_span ℝ (set.range s.points)
The definition of an altitude.
The orthocenter of a triangle is the intersection of its altitudes. It is defined here as the 2-dimensional case of the Monge point.
Equations
The orthocenter equals the Monge point.
The position of the orthocenter in relation to the circumcenter and centroid.
The orthocenter lies in the affine span.
In the case of a triangle, altitudes are the same thing as Monge planes.
The orthocenter lies in the altitudes.
The orthocenter is the only point lying in any two of the altitudes.