Angles and incenters and excenters.

This file proves lemmas relating incenters and excenters of a simplex to angle bisection.

theorem Affine.Simplex.ExcenterExists.angle_excenter_touchpoint_eq {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) {p : P} {i₁ i₂ : Fin (n + 1)} (hp₁ : p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) (hp₂ : p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) : EuclideanGeometry.angle (s.excenter signs) p (s.touchpoint signs i₁) = EuclideanGeometry.angle (s.excenter signs) p (s.touchpoint signs i₂)

An excenter of a simplex bisects the angle at a point shared between two faces, as measured between that excenter and its touchpoints on those faces.

theorem Affine.Simplex.angle_incenter_touchpoint_eq {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} {i₁ i₂ : Fin (n + 1)} (hp₁ : p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) (hp₂ : p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) : EuclideanGeometry.angle s.incenter p (s.touchpoint ∅ i₁) = EuclideanGeometry.angle s.incenter p (s.touchpoint ∅ i₂)

The incenter of a simplex bisects the angle at a point shared between two faces, as measured between the incenter and its touchpoints on those faces.

theorem Affine.Simplex.exists_excenterExists_and_eq_excenter_of_forall_angle_orthogonalProjectionSpan_eq {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)) {i₁ : Fin (n + 1)} (h : ∀ (i₂ : Fin (n + 1)), i₂ ≠ i₁ → ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points), p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧ EuclideanGeometry.angle p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) = EuclideanGeometry.angle p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)) : ∃ (signs : Finset (Fin (n + 1))), s.ExcenterExists signs ∧ p = s.excenter signs

Given a face of a simplex, if a point bisects the angle between that face and each other face, as measured at points shared between those faces between that point and its projections onto the faces, that point is an excenter of the simplex.

theorem Affine.Triangle.dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {p : P} : dist p ↑((Simplex.faceOpposite t i₃).orthogonalProjectionSpan p) = dist p ↑((Simplex.faceOpposite t i₂).orthogonalProjectionSpan p) ↔ 2 • EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p = 2 • EuclideanGeometry.oangle p (t.points i₁) (t.points i₃)

A point p is equidistant to two sides of a triangle if and only if the oriented angles at their common vertex are equal modulo π.

theorem Affine.Triangle.two_zsmul_oangle_excenter_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) (signs : Finset (Fin 3)) : 2 • EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Simplex.excenter t signs) = 2 • EuclideanGeometry.oangle (Simplex.excenter t signs) (t.points i₁) (t.points i₃)

An excenter of a triangle bisects the angle at a vertex modulo π.

theorem Affine.Triangle.oangle_incenter_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Simplex.incenter t) = EuclideanGeometry.oangle (Simplex.incenter t) (t.points i₁) (t.points i₃)

The incenter of a triangle bisects the angle at a vertex.

theorem Affine.Triangle.oangle_excenter_singleton_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Simplex.excenter t {i₁}) = EuclideanGeometry.oangle (Simplex.excenter t {i₁}) (t.points i₁) (t.points i₃)

The excenter of a triangle opposite a vertex bisects the angle at that vertex.

theorem Affine.Triangle.oangle_excenter_singleton_eq_add_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (Simplex.excenter t {i₁}) = EuclideanGeometry.oangle (Simplex.excenter t {i₁}) (t.points i₂) (t.points i₃) + ↑Real.pi

The excenter of a triangle opposite a vertex bisects the exterior angle at another vertex (that is, the interior angles between vertices and the excenter differ by π).

theorem Affine.Triangle.eq_excenter_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {p : P} (h₁ : 2 • EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p = 2 • EuclideanGeometry.oangle p (t.points i₁) (t.points i₃)) (h₂ : 2 • EuclideanGeometry.oangle (t.points i₃) (t.points i₂) p = 2 • EuclideanGeometry.oangle p (t.points i₂) (t.points i₁)) : ∃ (signs : Finset (Fin 3)), p = Simplex.excenter t signs

A point lying on angle bisectors from two vertices is an excenter.

theorem Affine.Triangle.eq_incenter_or_eq_excenter_singleton_of_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {signs : Finset (Fin 3)} (h : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Simplex.excenter t signs) = EuclideanGeometry.oangle (Simplex.excenter t signs) (t.points i₁) (t.points i₃)) : Simplex.excenter t signs = Simplex.incenter t ∨ Simplex.excenter t signs = Simplex.excenter t {i₁}

An excenter lying on the internal angle bisector from a vertex is either the incenter or the excenter opposite that vertex.

theorem Affine.Triangle.eq_excenter_singleton_of_oangle_eq_add_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {signs : Finset (Fin 3)} (h : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Simplex.excenter t signs) = EuclideanGeometry.oangle (Simplex.excenter t signs) (t.points i₁) (t.points i₃) + ↑Real.pi) : Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}

An excenter lying on the external angle bisector from a vertex is the excenter opposite another vertex.

theorem Affine.Triangle.eq_incenter_of_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {p : P} (h₁ : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p = EuclideanGeometry.oangle p (t.points i₁) (t.points i₃)) (h₂ : EuclideanGeometry.oangle (t.points i₃) (t.points i₂) p = EuclideanGeometry.oangle p (t.points i₂) (t.points i₁)) : p = Simplex.incenter t

A point lying on two internal angle bisectors is the incenter.

theorem Affine.Triangle.eq_excenter_singleton_of_oangle_eq_of_oangle_eq_add_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {p : P} (h₁ : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p = EuclideanGeometry.oangle p (t.points i₁) (t.points i₃)) (h₂ : EuclideanGeometry.oangle (t.points i₃) (t.points i₂) p = EuclideanGeometry.oangle p (t.points i₂) (t.points i₁) + ↑Real.pi) : p = Simplex.excenter t {i₁}

A point lying on the internal angle bisector from vertex i₁ and the external angle bisector from another vertex is the excenter opposite vertex i₁.

theorem Affine.Triangle.eq_excenter_singleton_of_oangle_eq_add_pi_of_oangle_eq_add_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {p : P} (h₁ : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p = EuclideanGeometry.oangle p (t.points i₁) (t.points i₃) + ↑Real.pi) (h₂ : EuclideanGeometry.oangle (t.points i₃) (t.points i₂) p = EuclideanGeometry.oangle p (t.points i₂) (t.points i₁) + ↑Real.pi) : p = Simplex.excenter t {i₃}

A point lying on two external angle bisectors is the excenter opposite the third vertex.