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.

The terms "exsphere", "excenter" and "exradius" are used in this file in a general sense where a Finset signs of indices is given 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. This includes the cases of the insphere, incenter and inradius, when signs is ∅ (or univ); the insphere always exists. It also includes the case of an exsphere opposite a vertex, when signs is a singleton (or its complement), which always exists in two or more dimensions. In three or more dimensions, there are further possibilities for signs, and the corresponding excenters may or may not exist, depending on the choice of simplex. For convenience, the most common definitions exsphere, excenter and exradius have corresponding insphere, incenter and inradius definitions, and various lemmas are duplicated for the case of the insphere to avoid needing to pass an ExcenterExists hypothesis in that case. However, other definitions such as excenterWeights, touchpoint and touchpointWeights are not duplicated.

Main definitions

• Affine.Simplex.ExcenterExists says whether an excenter exists with a given set of indices.
• 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
• Affine.Simplex.touchpoint for the point where an exsphere of a simplex is tangent to one of the faces.
• Affine.Simplex.touchpointWeights for the weights of a touchpoint as an affine combination of the vertices.

References

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

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

theorem Affine.Simplex.excenterWeightsUnnorm_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))) : (s.reindex e).excenterWeightsUnnorm signs = s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ ⇑e.symm

@[simp]

theorem Affine.Simplex.excenterWeightsUnnorm_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 : ℕ} [NeZero n] (s : Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) : (s.map f.toAffineMap ⋯).excenterWeightsUnnorm = s.excenterWeightsUnnorm

@[simp]

theorem Affine.Simplex.excenterWeightsUnnorm_restrict {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 : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) : (s.restrict S hS).excenterWeightsUnnorm = s.excenterWeightsUnnorm

@[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)⁻¹

theorem Affine.Simplex.excenterWeightsUnnorm_ne_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) (signs : Finset (Fin (n + 1))) (i : Fin (n + 1)) : s.excenterWeightsUnnorm signs i ≠ 0

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.

theorem Affine.Simplex.excenterExists_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex ℝ P n) {e : Fin (n + 1) ≃ Fin (m + 1)} {signs : Finset (Fin (m + 1))} : (s.reindex e).ExcenterExists signs ↔ s.ExcenterExists (Finset.map e.symm.toEmbedding signs)

@[simp]

theorem Affine.Simplex.excenterExists_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 : ℕ} [NeZero n] (s : Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) : (s.map f.toAffineMap ⋯).ExcenterExists = s.ExcenterExists

@[simp]

theorem Affine.Simplex.excenterExists_restrict {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 : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) : (s.restrict S hS).ExcenterExists = s.ExcenterExists

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

theorem Affine.Simplex.excenterWeights_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))) : (s.reindex e).excenterWeights signs = s.excenterWeights (Finset.map e.symm.toEmbedding signs) ∘ ⇑e.symm

@[simp]

theorem Affine.Simplex.excenterWeights_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 : ℕ} [NeZero n] (s : Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) : (s.map f.toAffineMap ⋯).excenterWeights = s.excenterWeights

@[simp]

theorem Affine.Simplex.excenterWeights_restrict {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 : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) : (s.restrict S hS).excenterWeights = s.excenterWeights

theorem Affine.Simplex.ExcenterExists.excenterWeights_ne_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} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (i : Fin (n + 1)) : s.excenterWeights signs i ≠ 0

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

theorem Affine.Simplex.excenterWeights_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) (i : Fin (n + 1)) : 0 < s.excenterWeights ∅ i

@[simp]

theorem Affine.Simplex.sign_excenterWeights_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) (i : Fin (n + 1)) : SignType.sign (s.excenterWeights ∅ i) = 1

@[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) [n.AtLeastTwo] (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 gives information about the location of the incenter (see excenterWeights_empty_lt_inv_two).

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) [n.AtLeastTwo] (i : Fin (n + 1)) : 0 < ∑ j : Fin (n + 1), s.excenterWeightsUnnorm {i} j

theorem Affine.Simplex.sign_excenterWeights_singleton_neg {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) [n.AtLeastTwo] (i : Fin (n + 1)) : SignType.sign (s.excenterWeights {i} i) = -1

theorem Affine.Simplex.sign_excenterWeights_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) [n.AtLeastTwo] {i j : Fin (n + 1)} (h : i ≠ j) : SignType.sign (s.excenterWeights {i} j) = 1

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) [n.AtLeastTwo] (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.

theorem Affine.Simplex.excenterWeights_empty_lt_inv_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) [n.AtLeastTwo] (i : Fin (n + 1)) : s.excenterWeights ∅ i < 2⁻¹

The barycentric coordinates of the incenter are less than 2⁻¹ (thus, it lies closer on an angle bisector to the opposite side than to the vertex, or equivalently the image of the incenter under a homothety with scale factor 2 about a vertex lies outside the simplex).

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

theorem Affine.Simplex.exsphere_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))) : (s.reindex e).exsphere signs = s.exsphere (Finset.map e.symm.toEmbedding signs)

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

@[simp]

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

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

theorem Affine.Simplex.excenter_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))) : (s.reindex e).excenter signs = s.excenter (Finset.map e.symm.toEmbedding signs)

@[simp]

theorem Affine.Simplex.ExcenterExists.excenter_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 : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (f : P →ᵃⁱ[ℝ] P₂) : (s.map f.toAffineMap ⋯).excenter signs = f (s.excenter signs)

@[simp]

theorem Affine.Simplex.ExcenterExists.excenter_restrict {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 : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) : ↑((s.restrict S hS).excenter signs) = s.excenter signs

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

@[simp]

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

@[simp]

theorem Affine.Simplex.incenter_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 : ℕ} [NeZero n] (s : Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) : (s.map f.toAffineMap ⋯).incenter = f s.incenter

@[simp]

theorem Affine.Simplex.incenter_restrict {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 : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) : ↑(s.restrict S hS).incenter = s.incenter

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

theorem Affine.Simplex.exradius_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))) : (s.reindex e).exradius signs = s.exradius (Finset.map e.symm.toEmbedding signs)

@[simp]

theorem Affine.Simplex.exradius_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 : ℕ} [NeZero n] (s : Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) : (s.map f.toAffineMap ⋯).exradius = s.exradius

@[simp]

theorem Affine.Simplex.exradius_restrict {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 : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) : (s.restrict S hS).exradius = s.exradius

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

@[simp]

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

@[simp]

theorem Affine.Simplex.inradius_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 : ℕ} [NeZero n] (s : Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) : (s.map f.toAffineMap ⋯).inradius = s.inradius

@[simp]

theorem Affine.Simplex.inradius_restrict {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 : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) : (s.restrict S hS).inradius = s.inradius

@[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_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.exsphere signsᶜ = s.exsphere signs

@[simp]

theorem Affine.Simplex.excenter_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.excenter signsᶜ = s.excenter signs

@[simp]

theorem Affine.Simplex.exradius_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.exradius signsᶜ = s.exradius signs

@[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) [n.AtLeastTwo] (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.incenter_mem_interior {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 ∈ s.interior

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) [n.AtLeastTwo] (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.sign_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)) : SignType.sign ((s.signedInfDist i) (s.excenter signs)) = SignType.sign (s.excenterWeights signs i)

theorem Affine.Simplex.sign_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)) : SignType.sign ((s.signedInfDist i) s.incenter) = 1

theorem Affine.Simplex.ExcenterExists.affineCombination_eq_excenter_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))} (h : s.ExcenterExists signs) {w : Fin (n + 1) → ℝ} (hw : ∑ j : Fin (n + 1), w j = 1) : (Finset.affineCombination ℝ Finset.univ s.points) w = s.excenter signs ↔ w = s.excenterWeights signs

theorem Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_face {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) {fs : Finset (Fin (n + 1))} {m : ℕ} (hfs : fs.card = m + 1) (hne : m ≠ n) : s.excenter signs ∉ affineSpan ℝ (Set.range (s.face hfs).points)

theorem Affine.Simplex.incenter_notMem_affineSpan_face {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (hfs : fs.card = m + 1) (hne : m ≠ n) : s.incenter ∉ affineSpan ℝ (Set.range (s.face hfs).points)

theorem Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_faceOpposite {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.excenter signs ∉ affineSpan ℝ (Set.range (s.faceOpposite i).points)

theorem Affine.Simplex.incenter_notMem_affineSpan_faceOpposite {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.incenter ∉ affineSpan ℝ (Set.range (s.faceOpposite i).points)

theorem Affine.Simplex.ExcenterExists.excenter_ne_point {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.excenter signs ≠ s.points i

theorem Affine.Simplex.incenter_ne_point {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.incenter ≠ s.points i

theorem Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_pair {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} [n.AtLeastTwo] {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (i j : Fin (n + 1)) : s.excenter signs ∉ affineSpan ℝ {s.points i, s.points j}

theorem Affine.Simplex.incenter_notMem_affineSpan_pair {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) [n.AtLeastTwo] (i j : Fin (n + 1)) : s.incenter ∉ affineSpan ℝ {s.points i, s.points j}

theorem Affine.Simplex.ExcenterExists.excenterWeights_eq_excenterWeights_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₁ signs₂ : Finset (Fin (n + 1))} (h₁ : s.ExcenterExists signs₁) (h₂ : s.ExcenterExists signs₂) : s.excenterWeights signs₁ = s.excenterWeights signs₂ ↔ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ

theorem Affine.Simplex.ExcenterExists.excenter_eq_excenter_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₁ signs₂ : Finset (Fin (n + 1))} (h₁ : s.ExcenterExists signs₁) (h₂ : s.ExcenterExists signs₂) : s.excenter signs₁ = s.excenter signs₂ ↔ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ

theorem Affine.Simplex.ExcenterExists.excenter_eq_incenter_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))} (h : s.ExcenterExists signs) : s.excenter signs = s.incenter ↔ signs = ∅ ∨ signs = Finset.univ

theorem Affine.Simplex.excenter_singleton_ne_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) [n.AtLeastTwo] (i : Fin (n + 1)) : s.excenter {i} ≠ s.incenter

theorem Affine.Simplex.excenter_singleton_injective {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) [n.AtLeastTwo] : Function.Injective fun (i : Fin (n + 1)) => s.excenter {i}

theorem Affine.Simplex.ExcenterExists.sSameSide_excenter_point_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))} (h : s.ExcenterExists signs) {i : Fin (n + 1)} : (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide (s.excenter signs) (s.points i) ↔ 0 < s.excenterWeights signs i

theorem Affine.Simplex.ExcenterExists.sSameSide_point_excenter_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))} (h : s.ExcenterExists signs) {i : Fin (n + 1)} : (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide (s.points i) (s.excenter signs) ↔ 0 < s.excenterWeights signs i

theorem Affine.Simplex.ExcenterExists.sOppSide_excenter_point_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))} (h : s.ExcenterExists signs) {i : Fin (n + 1)} : (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SOppSide (s.excenter signs) (s.points i) ↔ s.excenterWeights signs i < 0

theorem Affine.Simplex.ExcenterExists.sOppSide_point_excenter_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))} (h : s.ExcenterExists signs) {i : Fin (n + 1)} : (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SOppSide (s.points i) (s.excenter signs) ↔ s.excenterWeights signs i < 0

theorem Affine.Simplex.sSameSide_incenter_point {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)) : (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide s.incenter (s.points i)

theorem Affine.Simplex.sSameSide_point_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)) : (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide (s.points i) s.incenter

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

theorem Affine.Simplex.sOppSide_point_excenter_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) [n.AtLeastTwo] (i : Fin (n + 1)) : (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SOppSide (s.points i) (s.excenter {i})

theorem Affine.Simplex.sSameSide_excenter_singleton_point {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) [n.AtLeastTwo] {i j : Fin (n + 1)} (h : i ≠ j) : (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide (s.excenter {j}) (s.points i)

theorem Affine.Simplex.sSameSide_point_excenter_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) [n.AtLeastTwo] {i j : Fin (n + 1)} (h : i ≠ j) : (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide (s.points i) (s.excenter {j})

noncomputable def Affine.Simplex.touchpoint {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)) : P

A touchpoint is where an exsphere of a simplex is tangent to one of the faces.

theorem Affine.Simplex.touchpoint_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))) (i : Fin (m + 1)) : (s.reindex e).touchpoint signs i = s.touchpoint (Finset.map e.symm.toEmbedding signs) (e.symm i)

@[simp]

theorem Affine.Simplex.ExcenterExists.touchpoint_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 : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (f : P →ᵃⁱ[ℝ] P₂) (i : Fin (n + 1)) : (s.map f.toAffineMap ⋯).touchpoint signs i = f (s.touchpoint signs i)

@[simp]

theorem Affine.Simplex.ExcenterExists.touchpoint_restrict {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 : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)) : ↑((s.restrict S hS).touchpoint signs i) = s.touchpoint signs i

theorem Affine.Simplex.touchpoint_mem_affineSpan {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.touchpoint signs i ∈ affineSpan ℝ (Set.range (s.faceOpposite i).points)

theorem Affine.Simplex.touchpoint_mem_affineSpan_simplex {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.touchpoint signs i ∈ affineSpan ℝ (Set.range s.points)

A weaker version of touchpoint_mem_affineSpan.

theorem Affine.Simplex.touchpoint_eq_point_rev {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (s : Simplex ℝ P 1) (signs : Finset (Fin 2)) (i : Fin 2) : s.touchpoint signs i = s.points i.rev

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.touchpoint signs i) = s.exradius signs

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

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.touchpoint ∅ i) = s.inradius

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

theorem Affine.Simplex.ExcenterExists.dist_excenter_eq_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₁ i₂ : Fin (n + 1)) : dist (s.excenter signs) (s.touchpoint signs i₁) = dist (s.excenter signs) (s.touchpoint signs i₂)

An excenter is equidistant to any two of its touchpoints.

theorem Affine.Simplex.dist_incenter_eq_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₁ i₂ : Fin (n + 1)) : dist s.incenter (s.touchpoint ∅ i₁) = dist s.incenter (s.touchpoint ∅ i₂)

The incenter is equidistant to any two of its touchpoints.

theorem Affine.Simplex.ExcenterExists.touchpoint_mem_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))} (h : s.ExcenterExists signs) (i : Fin (n + 1)) : s.touchpoint signs i ∈ s.exsphere signs

theorem Affine.Simplex.touchpoint_mem_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) (i : Fin (n + 1)) : s.touchpoint ∅ i ∈ s.insphere

theorem Affine.Simplex.ExcenterExists.isTangentAt_touchpoint {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.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))

theorem Affine.Simplex.isTangentAt_insphere_touchpoint {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.insphere.IsTangentAt (s.touchpoint ∅ i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))

theorem Affine.Simplex.eq_touchpoint_of_isTangentAt_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))} {i : Fin (n + 1)} {p : P} (ht : (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points))) : p = s.touchpoint signs i

theorem Affine.Simplex.ExcenterExists.isTangentAt_exsphere_iff_eq_touchpoint {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)} {p : P} : (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points)) ↔ p = s.touchpoint signs i

theorem Affine.Simplex.isTangentAt_insphere_iff_eq_touchpoint {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)} {p : P} : s.insphere.IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points)) ↔ p = s.touchpoint ∅ i

theorem Affine.Simplex.ExcenterExists.affineSpan_faceOpposite_eq_orthRadius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} [hf : Fact (Module.finrank ℝ V = n)] {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (i : Fin (n + 1)) : affineSpan ℝ (Set.range (s.faceOpposite i).points) = (s.exsphere signs).orthRadius (s.touchpoint signs i)

theorem Affine.Simplex.affineSpan_faceOpposite_eq_orthRadius_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) [Fact (Module.finrank ℝ V = n)] (i : Fin (n + 1)) : affineSpan ℝ (Set.range (s.faceOpposite i).points) = s.insphere.orthRadius (s.touchpoint ∅ i)

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

theorem Affine.Simplex.ExcenterExists.touchpoint_injective {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) : Function.Injective (s.touchpoint signs)

theorem Affine.Simplex.touchpoint_empty_injective {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) : Function.Injective (s.touchpoint ∅)

theorem Affine.Simplex.ExcenterExists.touchpoint_notMem_affineSpan_of_ne {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 j : Fin (n + 1)} (hne : i ≠ j) : s.touchpoint signs i ∉ affineSpan ℝ (Set.range (s.faceOpposite j).points)

theorem Affine.Simplex.touchpoint_empty_notMem_affineSpan_of_ne {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 j : Fin (n + 1)} (hne : i ≠ j) : s.touchpoint ∅ i ∉ affineSpan ℝ (Set.range (s.faceOpposite j).points)

theorem Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint {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 j : Fin (n + 1)} (hne : i ≠ j) {r : ℝ} (hr : r ∈ Set.Icc 0 1) : SignType.sign ((s.signedInfDist j) ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) r)) = SignType.sign ((s.signedInfDist j) (s.excenter signs))

theorem Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint {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 j : Fin (n + 1)} (hne : i ≠ j) {r : ℝ} (hr : r ∈ Set.Icc 0 1) : SignType.sign ((s.signedInfDist j) ((AffineMap.lineMap s.incenter (s.touchpoint ∅ i)) r)) = SignType.sign ((s.signedInfDist j) s.incenter)

theorem Affine.Simplex.ExcenterExists.sign_signedInfDist_touchpoint {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 j : Fin (n + 1)} (hne : i ≠ j) : SignType.sign ((s.signedInfDist j) (s.touchpoint signs i)) = SignType.sign ((s.signedInfDist j) (s.excenter signs))

theorem Affine.Simplex.sign_signedInfDist_touchpoint_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) {i j : Fin (n + 1)} (hne : i ≠ j) : SignType.sign ((s.signedInfDist j) (s.touchpoint ∅ i)) = SignType.sign ((s.signedInfDist j) s.incenter)

noncomputable def Affine.Simplex.touchpointWeights {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)) : Fin (n + 1) → ℝ

The unique weights of the vertices in an affine combination equal to the given touchpoint.

@[simp]

theorem Affine.Simplex.sum_touchpointWeights {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)) : ∑ j : Fin (n + 1), s.touchpointWeights signs i j = 1

@[simp]

theorem Affine.Simplex.affineCombination_touchpointWeights {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)) : (Finset.affineCombination ℝ Finset.univ s.points) (s.touchpointWeights signs i) = s.touchpoint signs i

@[simp]

theorem Affine.Simplex.affineCombination_eq_touchpoint_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)} {w : Fin (n + 1) → ℝ} (hw : ∑ j : Fin (n + 1), w j = 1) : (Finset.affineCombination ℝ Finset.univ s.points) w = s.touchpoint signs i ↔ w = s.touchpointWeights signs i

theorem Affine.Simplex.touchpointWeights_reindex {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))) (i : Fin (m + 1)) : (s.reindex e).touchpointWeights signs i = s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm

@[simp]

theorem Affine.Simplex.ExcenterExists.touchpointWeights_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 : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (f : P →ᵃⁱ[ℝ] P₂) : (s.map f.toAffineMap ⋯).touchpointWeights signs = s.touchpointWeights signs

@[simp]

theorem Affine.Simplex.ExcenterExists.touchpointWeights_restrict {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 : AffineSubspace ℝ P) (hS : affineSpan ℝ (Set.range s.points) ≤ S) : (s.restrict S hS).touchpointWeights signs = s.touchpointWeights signs

theorem Affine.Simplex.ExcenterExists.sign_touchpointWeights {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 j : Fin (n + 1)} (hne : i ≠ j) : SignType.sign (s.touchpointWeights signs i j) = SignType.sign (s.excenterWeights signs j)

theorem Affine.Simplex.sign_touchpointWeights_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) {i j : Fin (n + 1)} (hne : i ≠ j) : SignType.sign (s.touchpointWeights ∅ i j) = 1

@[simp]

theorem Affine.Simplex.touchpointWeights_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} {signs : Finset (Fin (n + 1))} (i : Fin (n + 1)) : s.touchpointWeights signs i i = 0

theorem Affine.Simplex.touchpointWeights_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) {i j : Fin (n + 1)} (hne : i ≠ j) : 0 < s.touchpointWeights ∅ i j

theorem Affine.Simplex.touchpoint_empty_mem_interior_faceOpposite {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) [n.AtLeastTwo] (i : Fin (n + 1)) : s.touchpoint ∅ i ∈ (s.faceOpposite i).interior

theorem Affine.Simplex.sign_touchpointWeights_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) [n.AtLeastTwo] {i j : Fin (n + 1)} (hne : i ≠ j) : SignType.sign (s.touchpointWeights {i} i j) = 1

theorem Affine.Simplex.touchpointWeights_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) [n.AtLeastTwo] {i j : Fin (n + 1)} (hne : i ≠ j) : 0 < s.touchpointWeights {i} i j

theorem Affine.Simplex.touchpoint_singleton_mem_interior_faceOpposite {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) [n.AtLeastTwo] (i : Fin (n + 1)) : s.touchpoint {i} i ∈ (s.faceOpposite i).interior

theorem Affine.Simplex.sign_touchpointWeights_singleton_neg {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) [n.AtLeastTwo] {i j : Fin (n + 1)} (hne : i ≠ j) : SignType.sign (s.touchpointWeights {i} j i) = -1

theorem Affine.Simplex.touchpointWeights_singleton_neg {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) [n.AtLeastTwo] {i j : Fin (n + 1)} (hne : i ≠ j) : s.touchpointWeights {i} j i < 0

theorem Affine.Simplex.ExcenterExists.touchpoint_ne_point {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} [n.AtLeastTwo] {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) (i j : Fin (n + 1)) : s.touchpoint signs i ≠ s.points j

theorem Affine.Simplex.touchpoint_empty_ne_point {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex ℝ P n) [n.AtLeastTwo] (i j : Fin (n + 1)) : s.touchpoint ∅ i ≠ s.points j

theorem Affine.Triangle.excenterExists {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) (signs : Finset (Fin 3)) : Simplex.ExcenterExists t signs

All excenters exist for a triangle.

theorem Affine.Triangle.excenter_eq_incenter_or_excenter_singleton {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) (signs : Finset (Fin 3)) : Simplex.excenter t signs = Simplex.incenter t ∨ ∃ (i : Fin (2 + 1)), Simplex.excenter t signs = Simplex.excenter t {i}

An excenter of a triangle is either the incenter or the excenter opposite a vertex.

theorem Affine.Triangle.excenter_eq_incenter_or_excenter_singleton_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) (signs : Finset (Fin 3)) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Simplex.excenter t signs = Simplex.incenter t ∨ Simplex.excenter t signs = Simplex.excenter t {i₁} ∨ Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}

An excenter of a triangle is either the incenter or the excenter opposite one of three enumerated different vertices. This is intended for when it is known a point is an excenter and it is to be proved which excenter it is by elimination of the other cases.

theorem Affine.Triangle.sSameSide_affineSpan_pair_incenter_point {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : (affineSpan ℝ {t.points i₂, t.points i₃}).SSameSide (Simplex.incenter t) (t.points i₁)

theorem Affine.Triangle.sSameSide_affineSpan_pair_point_incenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : (affineSpan ℝ {t.points i₂, t.points i₃}).SSameSide (t.points i₁) (Simplex.incenter t)

theorem Affine.Triangle.sOppSide_affineSpan_pair_excenter_singleton_point {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : (affineSpan ℝ {t.points i₂, t.points i₃}).SOppSide (Simplex.excenter t {i₁}) (t.points i₁)

theorem Affine.Triangle.sOppSide_affineSpan_pair_point_excenter_singleton {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : (affineSpan ℝ {t.points i₂, t.points i₃}).SOppSide (t.points i₁) (Simplex.excenter t {i₁})

theorem Affine.Triangle.sSameSide_affineSpan_pair_excenter_singleton_point {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : (affineSpan ℝ {t.points i₂, t.points i₃}).SSameSide (Simplex.excenter t {i₂}) (t.points i₁)

theorem Affine.Triangle.sSameSide_affineSpan_pair_point_excenter_singleton {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : (affineSpan ℝ {t.points i₂, t.points i₃}).SSameSide (t.points i₁) (Simplex.excenter t {i₂})

theorem Affine.Triangle.affineSpan_pair_eq_orthRadius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) [Fact (Module.finrank ℝ V = 2)] (signs : Finset (Fin 3)) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : affineSpan ℝ {t.points i₂, t.points i₃} = (Simplex.exsphere t signs).orthRadius (Simplex.touchpoint t signs i₁)

theorem Affine.Triangle.affineSpan_pair_eq_orthRadius_insphere {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) [Fact (Module.finrank ℝ V = 2)] {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : affineSpan ℝ {t.points i₂, t.points i₃} = (Simplex.insphere t).orthRadius (Simplex.touchpoint t ∅ i₁)

theorem Affine.Triangle.sbtw_touchpoint_empty {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Sbtw ℝ (t.points i₁) (Simplex.touchpoint t ∅ i₂) (t.points i₃)

theorem Affine.Triangle.sbtw_touchpoint_singleton {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Sbtw ℝ (t.points i₁) (Simplex.touchpoint t {i₂} i₂) (t.points i₃)

theorem Affine.Triangle.touchpoint_singleton_sbtw {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Sbtw ℝ (Simplex.touchpoint t {i₁} i₂) (t.points i₃) (t.points i₁)