[Merged by Bors] - feat(Geometry/Euclidean/Incenter): incenters and excenters#23752
[Merged by Bors] - feat(Geometry/Euclidean/Incenter): incenters and excenters#23752
Conversation
… of simplex
Add two simple lemmas about the projection of a vertex of a simplex
onto the opposite face (that arise while setting up the theory of
`incenter` and `excenter`).
```lean
@[simp] lemma ne_orthogonalProjection_faceOpposite (i : Fin (n + 1)) : s.points i ≠
orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) := by
```
```lean
lemma dist_orthogonalProjection_faceOpposite_pos (i : Fin (n + 1)) :
0 < dist (s.points i)
(orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i)) := by
```
Add the trivial lemmas `abs_ite`, `abs_dite`, `mabs_ite` and `mabs_dite`.
PR summary 0665576140Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
Co-authored-by: Eric Wieser <efw@google.com>
Co-authored-by: Eric Wieser <efw@google.com>
Co-authored-by: Eric Wieser <efw@google.com>
…pposite' into jsm28/incenter
mathlib4-dependent-issues-bot
removed
the
blocked-by-other-PR
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This reduces the number of cases where rewriting on the definition of `orthogonalProjectionSpan` is needed.
|
Whether |
|
(With the added complication that the space of n-simplices in an ambient space of n dimensions isn't actually connected, it has two connected components corresponding to orientations of the ambient space.) |
|
Just to be clear I understand what you wrote above; you have no examples of extreme simplices in mind that permit more than the single-face excenters, but you believe they could exist? |
|
A general simplex will have all 2^n possible excenters. It's equality (and thus fewer excenters) that's the exceptional case; the extreme simplices are in order to show that equality is possible (via showing that both signs of the inequality are possible). Simply taking a regular simplex gives all possible excenters except for those given by a set of exactly half the vertices (in an odd dimension). |
|
But to construct the extreme simplices: we want to construct an n-simplex (thus n+1 vertices), with n at least 3, where three heights are equal and much smaller than the rest (reciprocals much larger than the rest) so the sign of the inequality is determined by which set contains two of the three. When giving explicit coordinates for an n-simplex it's often convenient to work in more than n dimensions; we'll work in n+2 dimensions.. n-2 of the vertices are of the form (1, 0, 0, ...), (0, 1, 0, 0, ...), using the first n-2 coordinates. The remaining three vertices are (0, ..., 0, 1-epsilon, epsilon, 0, 0), (0, ..., 0, 1-epsilon, 0, epsilon, 0) and (0, ..., 0, 1-epsilon, 0, 0, epsilon). The final three vertices are close to each other, so have small heights, and symmetry says their heights are equal. To bound the height of the first vertex (which equals the height of any other of the first n-2), note that all the others lie in the affine subspace where the sum of all but the first coordinate is 1, and the first coordinate is 0, so the distance to that subspace (which is at least 1) is a lower bound on that height. |
|
(There may well be simpler constructions, or indeed explicit constructions to give equality directly for any desired set of between 2 and n-1 vertices.) |
mathlib4-dependent-issues-bot
added
blocked-by-other-PR
|
I think this definition gives an arbitrary point for degenerate triangles. But I think for triangles you can still define the incenter to be the middle one of the three points if they are collinear, and I think this gives a continuous, total definition of incenter of a triangle. Is this something we want? And does this have a natural definition other than a case split? |
|
Everything here is for a |
|
The case giving an arbitrary point with these definitions is rather where the signed sum of weights is 0. You can interpret such a sum of points with weights summing to 0 as giving a vector via |
|
I guess you could make the same argument that |
|
You could apply the definitions of |
|
I think I said the wrong thing above, that actually sounds correct to me. |
ghost
added
the
Define the exspheres and insphere of a simplex (in dimension 1 and greater), and corresponding definitions for their center and radius. Give necessary and sufficient conditions for them to exist (in terms of the barycentric coordinates, being signed versions of the inverses of the distances between vertices and opposite faces, having a nonzero sum) and show that they do always exist in the case of the incenter and of the excenter opposite a single vertex (the latter in dimensions 2 and greater), and that any point lying in the span of the vertices and equidistant from the faces opposite the vertices is an excenter (and, when signs of the equal distances are given, is the excenter with corresponding signs). Some major pieces are deferred to followups, in particular definitions of touchpoints, tangency of exspheres and insphere to faces, and the relation to angle bisectors in various forms. But since the file is already over 600 lines, I think this is a reasonable starting point (and since the lemmas do show that the definitions have their characteristic properties of points being equidistant from the faces on the desired sides, I think it sufficiently justifies that the definitions are correct and usable as-is). Feel free to golf; the calculations involved in showing that the excenter opposite a vertex always exists (in dimensions 2 and greater) are rather long. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
…r-community#23752) Define the exspheres and insphere of a simplex (in dimension 1 and greater), and corresponding definitions for their center and radius. Give necessary and sufficient conditions for them to exist (in terms of the barycentric coordinates, being signed versions of the inverses of the distances between vertices and opposite faces, having a nonzero sum) and show that they do always exist in the case of the incenter and of the excenter opposite a single vertex (the latter in dimensions 2 and greater), and that any point lying in the span of the vertices and equidistant from the faces opposite the vertices is an excenter (and, when signs of the equal distances are given, is the excenter with corresponding signs). Some major pieces are deferred to followups, in particular definitions of touchpoints, tangency of exspheres and insphere to faces, and the relation to angle bisectors in various forms. But since the file is already over 600 lines, I think this is a reasonable starting point (and since the lemmas do show that the definitions have their characteristic properties of points being equidistant from the faces on the desired sides, I think it sufficiently justifies that the definitions are correct and usable as-is). Feel free to golf; the calculations involved in showing that the excenter opposite a vertex always exists (in dimensions 2 and greater) are rather long. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…r-community#23752) Define the exspheres and insphere of a simplex (in dimension 1 and greater), and corresponding definitions for their center and radius. Give necessary and sufficient conditions for them to exist (in terms of the barycentric coordinates, being signed versions of the inverses of the distances between vertices and opposite faces, having a nonzero sum) and show that they do always exist in the case of the incenter and of the excenter opposite a single vertex (the latter in dimensions 2 and greater), and that any point lying in the span of the vertices and equidistant from the faces opposite the vertices is an excenter (and, when signs of the equal distances are given, is the excenter with corresponding signs). Some major pieces are deferred to followups, in particular definitions of touchpoints, tangency of exspheres and insphere to faces, and the relation to angle bisectors in various forms. But since the file is already over 600 lines, I think this is a reasonable starting point (and since the lemmas do show that the definitions have their characteristic properties of points being equidistant from the faces on the desired sides, I think it sufficiently justifies that the definitions are correct and usable as-is). Feel free to golf; the calculations involved in showing that the excenter opposite a vertex always exists (in dimensions 2 and greater) are rather long. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…r-community#23752) Define the exspheres and insphere of a simplex (in dimension 1 and greater), and corresponding definitions for their center and radius. Give necessary and sufficient conditions for them to exist (in terms of the barycentric coordinates, being signed versions of the inverses of the distances between vertices and opposite faces, having a nonzero sum) and show that they do always exist in the case of the incenter and of the excenter opposite a single vertex (the latter in dimensions 2 and greater), and that any point lying in the span of the vertices and equidistant from the faces opposite the vertices is an excenter (and, when signs of the equal distances are given, is the excenter with corresponding signs). Some major pieces are deferred to followups, in particular definitions of touchpoints, tangency of exspheres and insphere to faces, and the relation to angle bisectors in various forms. But since the file is already over 600 lines, I think this is a reasonable starting point (and since the lemmas do show that the definitions have their characteristic properties of points being equidistant from the faces on the desired sides, I think it sufficiently justifies that the definitions are correct and usable as-is). Feel free to golf; the calculations involved in showing that the excenter opposite a vertex always exists (in dimensions 2 and greater) are rather long. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
6 participants
Define the exspheres and insphere of a simplex (in dimension 1 and greater), and corresponding definitions for their center and radius. Give necessary and sufficient conditions for them to exist (in terms of the barycentric coordinates, being signed versions of the inverses of the distances between vertices and opposite faces, having a nonzero sum) and show that they do always exist in the case of the incenter and of the excenter opposite a single vertex (the latter in dimensions 2 and greater), and that any point lying in the span of the vertices and equidistant from the faces opposite the vertices is an excenter (and, when signs of the equal distances are given, is the excenter with corresponding signs).
Some major pieces are deferred to followups, in particular definitions of touchpoints, tangency of exspheres and insphere to faces, and the relation to angle bisectors in various forms. But since the file is already over 600 lines, I think this is a reasonable starting point (and since the lemmas do show that the definitions have their characteristic properties of points being equidistant from the faces on the desired sides, I think it sufficiently justifies that the definitions are correct and usable as-is).
Feel free to golf; the calculations involved in showing that the excenter opposite a vertex always exists (in dimensions 2 and greater) are rather long.
abs_ite#23751orthogonalProjectionSpanmore #24503⟪_ -ᵥ _, _ -ᵥ _⟫ = dist _ _ ^ 2#24968Simplex.height#25029