Incenters and excenters of simplices.

This file defines the insphere and exspheres of a simplex (tangent to the faces of the simplex), and the center and radius of such spheres.

Main definitions

• Affine.Simplex.ExcenterExists says whether an excenter exists with a given set of indices (that determine, up to negating all the signs, which vertices of the simplex lie on the same side of the opposite face as the excenter and which lie on the opposite side of that face).
• Affine.Simplex.excenterWeights are the weights of the excenter with the given set of indices, if it exists, as an affine combination of the vertices.
• Affine.Simplex.exsphere is the exsphere with the given set of indices, if it exists, with shorthands:
  • Affine.Simplex.excenter for the center of this sphere
  • Affine.Simplex.exradius for the radius of this sphere
• Affine.Simplex.insphere is the insphere, with shorthands:
  • Affine.Simplex.incenter for the center of this sphere
  • Affine.Simplex.inradius for the radius of this sphere

References

• https://en.wikipedia.org/wiki/Incircle_and_excircles
• https://en.wikipedia.org/wiki/Incenter

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

The unnormalized weights of the vertices in an affine combination that gives an excenter with signs determined by the given set of indices (for the empty set, this is the incenter; for a singleton set, this is the excenter opposite a vertex). An excenter with those signs exists if and only if the sum of these weights is nonzero (so the normalized weights sum to 1).

Equations

• s.excenterWeightsUnnorm signs i = (if i ∈ signs then -1 else 1) * (s.height i)⁻¹

@[simp]

theorem Affine.Simplex.excenterWeightsUnnorm_empty_apply {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.excenterWeightsUnnorm ∅ i = (s.height i)⁻¹

def Affine.Simplex.ExcenterExists {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) : Prop

Whether an excenter exists with a given choice of signs.

Equations

• s.ExcenterExists signs = (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i ≠ 0)

def Affine.Simplex.excenterWeights {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) : Fin (n + 1) → ℝ

The normalized weights of the vertices in an affine combination that gives an excenter with signs determined by the given set of indices. An excenter with those signs exists if and only if the sum of these weights is 1.

Equations

• s.excenterWeights signs = (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ • s.excenterWeightsUnnorm signs

@[simp]

theorem Affine.Simplex.excenterWeightsUnnorm_compl {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) : s.excenterWeightsUnnorm signsᶜ = -s.excenterWeightsUnnorm signs

@[simp]

theorem Affine.Simplex.excenterWeights_compl {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) : s.excenterWeights signsᶜ = s.excenterWeights signs

@[simp]

theorem Affine.Simplex.excenterExists_compl {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) {signs : Finset (Fin (n + 1))} : s.ExcenterExists signsᶜ ↔ s.ExcenterExists signs

theorem Affine.Simplex.sum_excenterWeights {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) [Decidable (s.ExcenterExists signs)] : ∑ i : Fin (n + 1), s.excenterWeights signs i = if s.ExcenterExists signs then 1 else 0

@[simp]

theorem Affine.Simplex.sum_excenterWeights_eq_one_iff {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) {signs : Finset (Fin (n + 1))} : ∑ i : Fin (n + 1), s.excenterWeights signs i = 1 ↔ s.ExcenterExists signs

theorem Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) {signs : Finset (Fin (n + 1))} : s.ExcenterExists signs → ∑ i : Fin (n + 1), s.excenterWeights signs i = 1

Alias of the reverse direction of Affine.Simplex.sum_excenterWeights_eq_one_iff.

theorem Affine.Simplex.sum_excenterWeightsUnnorm_empty_pos {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) : 0 < ∑ i : Fin (n + 1), s.excenterWeightsUnnorm ∅ i

@[simp]

theorem Affine.Simplex.excenterExists_empty {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.ExcenterExists ∅

The existence of the incenter, expressed in terms of ExcenterExists.

theorem Affine.Simplex.sum_inv_height_sq_smul_vsub_eq_zero {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.height i)⁻¹ ^ 2 • (s.points i -ᵥ s.altitudeFoot i) = 0

theorem Affine.Simplex.inv_height_eq_sum_mul_inv_dist {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.height i)⁻¹ = ∑ j : Fin (n + 1)with j ≠ i, -(inner ℝ (s.points i -ᵥ s.altitudeFoot i) (s.points j -ᵥ s.altitudeFoot j) / (s.height i * s.height j)) * (s.height j)⁻¹

The inverse of the distance from one vertex to the opposite face, expressed as a sum of multiples of that quantity for the other vertices. The multipliers, expressed here in terms of inner products, are equal to the cosines of angles between faces (informally, the inverse distances are proportional to the volumes of the faces and this is equivalent to expressing the volume of a face as the sum of the signed volumes of projections of the other faces onto that face).

theorem Affine.Simplex.inv_height_lt_sum_inv_height {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (hn : 1 < n) (i : Fin (n + 1)) : (s.height i)⁻¹ < ∑ j : Fin (n + 1)with j ≠ i, (s.height j)⁻¹

The inverse of the distance from one vertex to the opposite face is less than the sum of that quantity for the other vertices. This implies the existence of the excenter opposite that vertex; it also implies that the image of the incenter under a homothety with scale factor 2 about a vertex lies outside the simplex.

theorem Affine.Simplex.sum_excenterWeightsUnnorm_singleton_pos {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (hn : 1 < n) (i : Fin (n + 1)) : 0 < ∑ j : Fin (n + 1), s.excenterWeightsUnnorm {i} j

theorem Affine.Simplex.excenterExists_singleton {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (hn : 1 < n) (i : Fin (n + 1)) : s.ExcenterExists {i}

The existence of the excenter opposite a vertex (in two or more dimensions), expressed in terms of ExcenterExists.

def Affine.Simplex.exsphere {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) : EuclideanGeometry.Sphere P

The exsphere with signs determined by the given set of indices (for the empty set, this is the insphere; for a singleton set, this is the exsphere opposite a vertex). This is only meaningful if s.ExcenterExists; otherwise, it is a sphere of radius zero at some arbitrary point.

Equations

• s.exsphere signs = { center := (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights signs), radius := |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| }

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

The insphere of a simplex.

Equations

• s.insphere = s.exsphere ∅

def Affine.Simplex.excenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) : P

The excenter with signs determined by the given set of indices (for the empty set, this is the incenter; for a singleton set, this is the excenter opposite a vertex). This is only meaningful if s.ExcenterExists signs; otherwise, it is some arbitrary point.

Equations

• s.excenter signs = (s.exsphere signs).center

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

The incenter of a simplex.

Equations

• s.incenter = (s.exsphere ∅).center

def Affine.Simplex.exradius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) : ℝ

The distance between an excenter and a face of the simplex (zero if no such excenter exists).

Equations

• s.exradius signs = (s.exsphere signs).radius

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

The distance between the incenter and a face of the simplex.

Equations

• s.inradius = (s.exsphere ∅).radius

@[simp]

theorem Affine.Simplex.exsphere_center {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) : (s.exsphere signs).center = s.excenter signs

@[simp]

theorem Affine.Simplex.exsphere_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) : (s.exsphere signs).radius = s.exradius signs

@[simp]

theorem Affine.Simplex.insphere_center {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.insphere.center = s.incenter

@[simp]

theorem Affine.Simplex.insphere_radius {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.insphere.radius = s.inradius

@[simp]

theorem Affine.Simplex.exsphere_empty {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.exsphere ∅ = s.insphere

@[simp]

theorem Affine.Simplex.excenter_empty {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.excenter ∅ = s.incenter

@[simp]

theorem Affine.Simplex.exradius_empty {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.exradius ∅ = s.inradius

@[simp]

theorem Affine.Simplex.exsphere_univ {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.exsphere Finset.univ = s.insphere

@[simp]

theorem Affine.Simplex.excenter_univ {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.excenter Finset.univ = s.incenter

@[simp]

theorem Affine.Simplex.exradius_univ {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.exradius Finset.univ = s.inradius

theorem Affine.Simplex.excenter_eq_affineCombination {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) : s.excenter signs = (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights signs)

theorem Affine.Simplex.exradius_eq_abs_inv_sum {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) : s.exradius signs = |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹|

theorem Affine.Simplex.incenter_eq_affineCombination {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.incenter = (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights ∅)

theorem Affine.Simplex.inradius_eq_abs_inv_sum {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.inradius = |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm ∅ i)⁻¹|

theorem Affine.Simplex.exradius_nonneg {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (signs : Finset (Fin (n + 1))) : 0 ≤ s.exradius signs

theorem Affine.Simplex.ExcenterExists.exradius_pos {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) : 0 < s.exradius signs

theorem Affine.Simplex.inradius_pos {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) : 0 < s.inradius

theorem Affine.Simplex.exradius_singleton_pos {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (hn : 1 < n) (i : Fin (n + 1)) : 0 < s.exradius {i}

theorem Affine.Simplex.ExcenterExists.excenter_mem_affineSpan_range {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) : s.excenter signs ∈ affineSpan ℝ (Set.range s.points)

theorem Affine.Simplex.incenter_mem_affineSpan_range {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.incenter ∈ affineSpan ℝ (Set.range s.points)

theorem Affine.Simplex.excenter_singleton_mem_affineSpan_range {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (hn : 1 < n) (i : Fin (n + 1)) : s.excenter {i} ∈ affineSpan ℝ (Set.range s.points)

theorem Affine.Simplex.ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (i : Fin (n + 1)) : (s.signedInfDist i) (s.excenter signs) = (if i ∈ signs then -1 else 1) * (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)⁻¹

theorem Affine.Simplex.ExcenterExists.signedInfDist_excenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (i : Fin (n + 1)) : (s.signedInfDist i) (s.excenter signs) = (if i ∈ signs then -1 else 1) * ↑(SignType.sign (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) * s.exradius signs

The signed distance between the excenter and its projection in the plane of each face is the exradius.

theorem Affine.Simplex.signedInfDist_incenter {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.signedInfDist i) s.incenter = s.inradius

The signed distance between the incenter and its projection in the plane of each face is the inradius.

In other words, the incenter is internally tangent to the faces.

theorem Affine.Simplex.ExcenterExists.dist_excenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (i : Fin (n + 1)) : dist (s.excenter signs) ↑((s.faceOpposite i).orthogonalProjectionSpan (s.excenter signs)) = s.exradius signs

The distance between the excenter and its projection in the plane of each face is the exradius.

In other words, the exsphere is tangent to the faces.

theorem Affine.Simplex.dist_incenter {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)) : dist s.incenter ↑((s.faceOpposite i).orthogonalProjectionSpan s.incenter) = s.inradius

The distance between the incenter and its projection in the plane of each face is the inradius.

In other words, the incenter is tangent to the faces.

theorem Affine.Simplex.exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) {p : P} (hp : p ∈ affineSpan ℝ (Set.range s.points)) {signs : Finset (Fin (n + 1))} : (∃ (r : ℝ), ∀ (i : Fin (n + 1)), (s.signedInfDist i) p = (if i ∈ signs then -1 else 1) * r) ↔ s.ExcenterExists signs ∧ p = s.excenter signs

theorem Affine.Simplex.exists_forall_signedInfDist_eq_iff_eq_incenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) {p : P} (hp : p ∈ affineSpan ℝ (Set.range s.points)) : (∃ (r : ℝ), ∀ (i : Fin (n + 1)), (s.signedInfDist i) p = r) ↔ p = s.incenter

theorem Affine.Simplex.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) {p : P} (hp : p ∈ affineSpan ℝ (Set.range s.points)) : (∃ (r : ℝ), ∀ (i : Fin (n + 1)), dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p) = r) ↔ ∃ (signs : Finset (Fin (n + 1))), s.ExcenterExists signs ∧ p = s.excenter signs