mathlib documentation

geometry.euclidean.monge_point

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_point is 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_plane is 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).
altitude is the line that passes through a vertex of a simplex and is orthogonal to the opposite face.
orthocenter is 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

def affine.simplex.monge_point {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P n) :

P

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

theorem affine.simplex.monge_point_eq_smul_vsub_vadd_circumcenter {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P n) :

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.

theorem affine.simplex.monge_point_mem_affine_span {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P n) :

s.monge_point ∈ affine_span ℝ (set.range s.points)

The Monge point lies in the affine span.

theorem affine.simplex.monge_point_eq_of_range_eq {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} {s₁ s₂ : affine.simplex ℝ P n} (h : set.range s₁.points = set.range s₂.points) :

s₁.monge_point = s₂.monge_point

Two simplices with the same points have the same Monge point.

def affine.simplex.monge_point_weights_with_circumcenter (n : ℕ) (a : affine.simplex.points_with_circumcenter_index (n + 2)) :

The weights for the Monge point of an (n+2)-simplex, in terms of points_with_circumcenter.

Equations

@[simp]

theorem affine.simplex.sum_monge_point_weights_with_circumcenter (n : ℕ) :

∑ (i : affine.simplex.points_with_circumcenter_index (n + 2)), affine.simplex.monge_point_weights_with_circumcenter n i = 1

monge_point_weights_with_circumcenter sums to 1.

theorem affine.simplex.monge_point_eq_affine_combination_of_points_with_circumcenter {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) :

s.monge_point = ⇑(finset.univ.affine_combination s.points_with_circumcenter) (affine.simplex.monge_point_weights_with_circumcenter n)

The Monge point of an (n+2)-simplex, in terms of points_with_circumcenter.

def affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter {n : ℕ} (i₁ i₂ : fin (n + 3)) (a : affine.simplex.points_with_circumcenter_index (n + 2)) :

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

theorem affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter_eq_sub {n : ℕ} {i₁ i₂ : fin (n + 3)} (h : i₁ ≠ i₂) :

affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter i₁ i₂ = affine.simplex.monge_point_weights_with_circumcenter n - affine.simplex.centroid_weights_with_circumcenter {i₁, i₂}ᶜ

monge_point_vsub_face_centroid_weights_with_circumcenter is the result of subtracting centroid_weights_with_circumcenter from monge_point_weights_with_circumcenter.

@[simp]

theorem affine.simplex.sum_monge_point_vsub_face_centroid_weights_with_circumcenter {n : ℕ} {i₁ i₂ : fin (n + 3)} (h : i₁ ≠ i₂) :

∑ (i : affine.simplex.points_with_circumcenter_index (n + 2)), affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter i₁ i₂ i = 0

monge_point_vsub_face_centroid_weights_with_circumcenter sums to 0.

theorem affine.simplex.monge_point_vsub_face_centroid_eq_weighted_vsub_of_points_with_circumcenter {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) {i₁ i₂ : fin (n + 3)} (h : i₁ ≠ i₂) :

s.monge_point -ᵥ finset.centroid ℝ {i₁, i₂}ᶜ s.points = ⇑(finset.univ.weighted_vsub s.points_with_circumcenter) (affine.simplex.monge_point_vsub_face_centroid_weights_with_circumcenter i₁ i₂)

The Monge point of an (n+2)-simplex, minus the centroid of an n-dimensional face, in terms of points_with_circumcenter.

theorem affine.simplex.inner_monge_point_vsub_face_centroid_vsub {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) {i₁ i₂ : fin (n + 3)} (h : i₁ ≠ i₂) :

inner (s.monge_point -ᵥ finset.centroid ℝ {i₁, i₂}ᶜ s.points) (s.points i₁ -ᵥ s.points i₂) = 0

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.

def affine.simplex.monge_plane {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) (i₁ i₂ : fin (n + 3)) :

affine_subspace ℝ P

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)

theorem affine.simplex.monge_plane_def {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) (i₁ i₂ : fin (n + 3)) :

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.

theorem affine.simplex.monge_plane_comm {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) (i₁ i₂ : fin (n + 3)) :

s.monge_plane i₁ i₂ = s.monge_plane i₂ i₁

The Monge plane associated with vertices i₁ and i₂ equals that associated with i₂ and i₁.

theorem affine.simplex.monge_point_mem_monge_plane {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) {i₁ i₂ : fin (n + 3)} (h : i₁ ≠ i₂) :

s.monge_point ∈ s.monge_plane i₁ i₂

The Monge point lies in the Monge planes.

theorem affine.simplex.direction_monge_plane {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 2)) {i₁ i₂ : fin (n + 3)} (h : i₁ ≠ i₂) :

(s.monge_plane i₁ i₂).direction = (submodule.span ℝ {s.points i₁ -ᵥ s.points i₂}).orthogonal ⊓ vector_span ℝ (set.range s.points)

The direction of a Monge plane.

theorem affine.simplex.eq_monge_point_of_forall_mem_monge_plane {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} {s : affine.simplex ℝ P (n + 2)} {i₁ : fin (n + 3)} {p : P} (h : ∀ (i₂ : fin (n + 3)), i₁ ≠ i₂ → p ∈ s.monge_plane i₁ i₂) :

p = s.monge_point

The Monge point is the only point in all the Monge planes from any one vertex.

def affine.simplex.altitude {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

affine_subspace ℝ P

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)

theorem affine.simplex.altitude_def {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

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.

theorem affine.simplex.mem_altitude {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

s.points i ∈ s.altitude i

A vertex lies in the corresponding altitude.

theorem affine.simplex.direction_altitude {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

(s.altitude i).direction = (vector_span ℝ (s.points '' ↑(finset.univ.erase i))).orthogonal ⊓ vector_span ℝ (set.range s.points)

The direction of an altitude.

theorem affine.simplex.vector_span_le_altitude_direction_orthogonal {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

vector_span ℝ (s.points '' ↑(finset.univ.erase i)) ≤ (s.altitude i).direction.orthogonal

The vector span of the opposite face lies in the direction orthogonal to an altitude.

@[instance]

def affine.simplex.finite_dimensional_direction_altitude {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

finite_dimensional ℝ ↥((s.altitude i).direction)

An altitude is finite-dimensional.

@[simp]

theorem affine.simplex.findim_direction_altitude {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) :

finite_dimensional.findim ℝ ↥((s.altitude i).direction) = 1

An altitude is one-dimensional (i.e., a line).

theorem affine.simplex.affine_span_insert_singleton_eq_altitude_iff {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {n : ℕ} (s : affine.simplex ℝ P (n + 1)) (i : fin (n + 2)) (p : P) :

affine_span ℝ {p, s.points i} = s.altitude i ↔ p ≠ s.points i ∧ p ∈ affine_span ℝ (set.range s.points) ∧ p -ᵥ s.points i ∈ (affine_span ℝ (s.points '' ↑(finset.univ.erase i))).direction.orthogonal

A line through a vertex is the altitude through that vertex if and only if it is orthogonal to the opposite face.

def affine.triangle.orthocenter {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) :

P

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

t.orthocenter = affine.simplex.monge_point t

theorem affine.triangle.orthocenter_eq_monge_point {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) :

t.orthocenter = affine.simplex.monge_point t

The orthocenter equals the Monge point.

theorem affine.triangle.orthocenter_eq_smul_vsub_vadd_circumcenter {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) :

t.orthocenter = 3 • (finset.centroid ℝ finset.univ t.points -ᵥ affine.simplex.circumcenter t) +ᵥ affine.simplex.circumcenter t

The position of the orthocenter in relation to the circumcenter and centroid.

theorem affine.triangle.orthocenter_mem_affine_span {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) :

t.orthocenter ∈ affine_span ℝ (set.range t.points)

The orthocenter lies in the affine span.

theorem affine.triangle.orthocenter_eq_of_range_eq {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {t₁ t₂ : affine.triangle ℝ P} (h : set.range t₁.points = set.range t₂.points) :

t₁.orthocenter = t₂.orthocenter

Two triangles with the same points have the same orthocenter.

theorem affine.triangle.altitude_eq_monge_plane {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) {i₁ i₂ i₃ : fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :

affine.simplex.altitude t i₁ = affine.simplex.monge_plane t i₂ i₃

In the case of a triangle, altitudes are the same thing as Monge planes.

theorem affine.triangle.orthocenter_mem_altitude {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) {i₁ : fin 3} :

t.orthocenter ∈ affine.simplex.altitude t i₁

The orthocenter lies in the altitudes.

theorem affine.triangle.eq_orthocenter_of_forall_mem_altitude {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {t : affine.triangle ℝ P} {i₁ i₂ : fin 3} {p : P} (h₁₂ : i₁ ≠ i₂) (h₁ : p ∈ affine.simplex.altitude t i₁) (h₂ : p ∈ affine.simplex.altitude t i₂) :

p = t.orthocenter

The orthocenter is the only point lying in any two of the altitudes.

theorem affine.triangle.dist_orthocenter_reflection_circumcenter {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) {i₁ i₂ : fin 3} (h : i₁ ≠ i₂) :

dist t.orthocenter (⇑(euclidean_geometry.reflection (affine_span ℝ (t.points '' {i₁, i₂}))) (affine.simplex.circumcenter t)) = affine.simplex.circumradius t

The distance from the orthocenter to the reflection of the circumcenter in a side equals the circumradius.

theorem affine.triangle.dist_orthocenter_reflection_circumcenter_finset {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) {i₁ i₂ : fin 3} (h : i₁ ≠ i₂) :

dist t.orthocenter (⇑(euclidean_geometry.reflection (affine_span ℝ (t.points '' ↑{i₁, i₂}))) (affine.simplex.circumcenter t)) = affine.simplex.circumradius t

The distance from the orthocenter to the reflection of the circumcenter in a side equals the circumradius, variant using a finset.

theorem affine.triangle.affine_span_orthocenter_point_le_altitude {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] (t : affine.triangle ℝ P) (i : fin 3) :

affine_span ℝ {t.orthocenter, t.points i} ≤ affine.simplex.altitude t i

The affine span of the orthocenter and a vertex is contained in the altitude.

theorem affine.triangle.altitude_replace_orthocenter_eq_affine_span {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {t₁ t₂ : affine.triangle ℝ P} {i₁ i₂ i₃ j₁ j₂ j₃ : fin 3} (hi₁₂ : i₁ ≠ i₂) (hi₁₃ : i₁ ≠ i₃) (hi₂₃ : i₂ ≠ i₃) (hj₁₂ : j₁ ≠ j₂) (hj₁₃ : j₁ ≠ j₃) (hj₂₃ : j₂ ≠ j₃) (h₁ : t₂.points j₁ = t₁.orthocenter) (h₂ : t₂.points j₂ = t₁.points i₂) (h₃ : t₂.points j₃ = t₁.points i₃) :

affine.simplex.altitude t₂ j₂ = affine_span ℝ {t₁.points i₁, t₁.points i₂}

Suppose we are given a triangle t₁, and replace one of its vertices by its orthocenter, yielding triangle t₂ (with vertices not necessarily listed in the same order). Then an altitude of t₂ from a vertex that was not replaced is the corresponding side of t₁.

theorem affine.triangle.orthocenter_replace_orthocenter_eq_point {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {t₁ t₂ : affine.triangle ℝ P} {i₁ i₂ i₃ j₁ j₂ j₃ : fin 3} (hi₁₂ : i₁ ≠ i₂) (hi₁₃ : i₁ ≠ i₃) (hi₂₃ : i₂ ≠ i₃) (hj₁₂ : j₁ ≠ j₂) (hj₁₃ : j₁ ≠ j₃) (hj₂₃ : j₂ ≠ j₃) (h₁ : t₂.points j₁ = t₁.orthocenter) (h₂ : t₂.points j₂ = t₁.points i₂) (h₃ : t₂.points j₃ = t₁.points i₃) :

t₂.orthocenter = t₁.points i₁

Suppose we are given a triangle t₁, and replace one of its vertices by its orthocenter, yielding triangle t₂ (with vertices not necessarily listed in the same order). Then the orthocenter of t₂ is the vertex of t₁ that was replaced.