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.

Equations

• s.ninePointCircle = { center := ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter, radius := s.circumradius / ↑n }

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_eq_lineMap_circumcenter_centroid {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 = (AffineMap.lineMap s.circumcenter s.centroid) ((↑n + 1) / ↑n)

theorem Affine.Simplex.ninePointCircle_center_eq_point {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Simplex ℝ P 0) (i : Fin 1) : s.ninePointCircle.center = s.points i

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

theorem Affine.Simplex.dist_ninePointCircle_center_sq {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)) : dist (s.points i) s.ninePointCircle.center ^ 2 = (s.circumradius ^ 2 + (↑n - 1) * ∑ j ∈ {i}ᶜ, dist (s.points i) (s.points j) ^ 2 - (∑ j ∈ {i}ᶜ, ∑ k ∈ {i}ᶜ, dist (s.points j) (s.points k) ^ 2) / 2) / ↑n ^ 2

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).

Equations

• s.eulerPoint i = (↑n)⁻¹ • (s.points i -ᵥ s.mongePoint) +ᵥ s.mongePoint

@[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

theorem Affine.Triangle.dist_ninePointCircle_center_sq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : dist (s.points i₁) (Simplex.ninePointCircle s).center ^ 2 = (Simplex.circumradius s ^ 2 + dist (s.points i₁) (s.points i₂) ^ 2 + dist (s.points i₁) (s.points i₃) ^ 2 - dist (s.points i₂) (s.points i₃) ^ 2) / 4

In triangle $ABC$ with side length $a$, $b$, and $c$, nine-point circle center $N$ and circumradius $R$, we have $‖AN‖^2 = (R^2 + b^2 + c^2 - a^2) / 4$.