Nine-point circle

This file defines the nine-point circle of a triangle, and its higher dimension analogue, the 3(n+1)-point sphere of a simplex. Specifically for triangles, we show that it passes through nine specific points as desired.

Main definitions

• Affine.Simplex.ninePointCircle: the 3(n+1)-point sphere of a simplex.
• Affine.Simplex.eulerPoint: the $1/n$th of the way from the Monge point to a vertex.
• Affine.Simplex.faceOppositeCentroid_mem_ninePointCircle: the 3(n+1)-point sphere passes through the centroid of each face of the simplex
• Affine.Simplex.eulerPoint_mem_ninePointCircle: the 3(n+1)-point sphere passes through all Euler points.
• Affine.Triangle.altitudeFoot_mem_ninePointCircle: the nine-point circle passes through all three altitude feet of the triangle.

References

• Małgorzata Buba-Brzozowa, The Monge Point and the 3(n+1) Point Sphere of an n-Simplex

noncomputable def Affine.Simplex.ninePointCircle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) : EuclideanGeometry.Sphere P

The 3(n+1)-point sphere of a simplex. Due to the lack of a better name and to avoid numbers in the identifier, we still use the name "nine-point circle" even for higher dimensions. The center $N$ is defined on the Euler line, collinear with circumcenter $O$ and centroid $G$, in the order of $O$, $G$, and $N$, with $OG : GN = n : 1$. The radius is $1/n$ of the circumradius.

theorem Affine.Simplex.ninePointCircle_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) : s.ninePointCircle.center = ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter

theorem Affine.Simplex.ninePointCircle_center_mem_affineSpan {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) : s.ninePointCircle.center ∈ affineSpan ℝ (Set.range s.points)

theorem Affine.Simplex.ninePointCircle_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) : s.ninePointCircle.radius = s.circumradius / ↑n

@[simp]

theorem Affine.Simplex.ninePointCircle_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) : (s.reindex e).ninePointCircle = s.ninePointCircle

theorem Affine.Simplex.ninePointCircle_map {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂] [MetricSpace P₂] [NormedAddTorsor V₂ P₂] {n : ℕ} (s : Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) : (s.map f.toAffineMap ⋯).ninePointCircle = { center := f s.ninePointCircle.center, radius := s.ninePointCircle.radius }

theorem Affine.Simplex.ninePointCircle_restrict {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) (S : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) : (s.restrict S hS).ninePointCircle = { center := ⟨s.ninePointCircle.center, ⋯⟩, radius := s.ninePointCircle.radius }

theorem Affine.Simplex.faceOppositeCentroid_mem_ninePointCircle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.faceOppositeCentroid i ∈ s.ninePointCircle

theorem Affine.Simplex.ninePointCircle_eq_circumsphere_medial {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) : s.ninePointCircle = s.medial.circumsphere

noncomputable def Affine.Simplex.eulerPoint {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) : P

Euler points are a set of points that the ninePointCircle passes through. They are defined as being $1/n$th of the way from the Monge point to a vertex. Specifically for triangles, these are the midpoints between the orthocenter and a given vertex (Affine.Triangle.eulerPoint_eq_midpoint).

@[simp]

theorem Affine.Simplex.eulerPoint_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) : (s.reindex e).eulerPoint = s.eulerPoint ∘ ⇑e.symm

@[simp]

theorem Affine.Simplex.eulerPoint_map {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂] [MetricSpace P₂] [NormedAddTorsor V₂ P₂] {n : ℕ} (s : Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) (i : Fin (n + 1)) : (s.map f.toAffineMap ⋯).eulerPoint i = f (s.eulerPoint i)

@[simp]

theorem Affine.Simplex.eulerPoint_restrict {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) (S : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)) : ↑((s.restrict S hS).eulerPoint i) = s.eulerPoint i

theorem Affine.Simplex.points_vsub_eulerPoint {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.points i -ᵥ s.eulerPoint i = ((↑n - 1) / ↑n) • (s.points i -ᵥ s.mongePoint)

theorem Affine.Simplex.midpoint_faceOppositeCentroid_eulerPoint {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [hn : NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : midpoint ℝ (s.faceOppositeCentroid i) (s.eulerPoint i) = s.ninePointCircle.center

theorem Affine.Simplex.isDiameter_ninePointCircle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.ninePointCircle.IsDiameter (s.faceOppositeCentroid i) (s.eulerPoint i)

theorem Affine.Simplex.eulerPoint_mem_ninePointCircle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.eulerPoint i ∈ s.ninePointCircle

theorem Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : ↑((s.faceOpposite i).orthogonalProjectionSpan (s.eulerPoint i)) ∈ s.ninePointCircle

theorem Affine.Triangle.eulerPoint_eq_midpoint {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Triangle ℝ P) (i : Fin 3) : Simplex.eulerPoint s i = midpoint ℝ s.orthocenter (s.points i)

theorem Affine.Triangle.altitudeFoot_mem_ninePointCircle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Triangle ℝ P) (i : Fin 3) : Simplex.altitudeFoot s i ∈ Simplex.ninePointCircle s