[Merged by Bors] - feat(Geometry/Euclidean/Incenter): incenters and excenters

Mathlib.lean

@@ -1537,6 +1537,7 @@ import Mathlib.Analysis.Fourier.ZMod
 import Mathlib.Analysis.FunctionalSpaces.SobolevInequality
 import Mathlib.Analysis.Hofer
 import Mathlib.Analysis.InnerProductSpace.Adjoint
+import Mathlib.Analysis.InnerProductSpace.Affine
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.InnerProductSpace.Calculus
 import Mathlib.Analysis.InnerProductSpace.CanonicalTensor
@@ -3554,6 +3555,7 @@ import Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct
 import Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
 import Mathlib.Geometry.Euclidean.Basic
 import Mathlib.Geometry.Euclidean.Circumcenter
+import Mathlib.Geometry.Euclidean.Incenter
 import Mathlib.Geometry.Euclidean.Inversion.Basic
 import Mathlib.Geometry.Euclidean.Inversion.Calculus
 import Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane

Mathlib/Analysis/InnerProductSpace/Affine.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2025 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.Analysis.Normed.Group.AddTorsor
+/-!
+# Normed affine spaces over an inner product space
+-/
+
+variable {𝕜 V P : Type*}
+
+section RCLike
+variable [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [MetricSpace P]
+variable [NormedAddTorsor V P]
+
+open scoped InnerProductSpace
+
+theorem inner_vsub_left_eq_zero_symm {a b : P} {v : V} :
+    ⟪a -ᵥ b, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0 := by
+  rw [← neg_vsub_eq_vsub_rev, inner_neg_left, neg_eq_zero]
+
+theorem inner_vsub_right_eq_zero_symm {v : V} {a b : P} :
+    ⟪v, a -ᵥ b⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0 := by
+  rw [← neg_vsub_eq_vsub_rev, inner_neg_right, neg_eq_zero]
+
+end RCLike
+
+section Real
+variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
+variable [NormedAddTorsor V P]
+
+open scoped RealInnerProductSpace
+
+/-!
+In this section, the first `left`/`right` indicates where the common argument to `vsub` is,
+and the section refers to the argument of `inner` that ends up in the `dist`.
+
+The lemma shapes are such that the relevant argument of `inner` remains unchanged,
+and that the other `vsub` preserves the position of the unchanging argument. -/
+
+theorem inner_vsub_vsub_left_eq_dist_sq_left_iff {a b c : P} :
+    ⟪a -ᵥ b, a -ᵥ c⟫ = dist a b ^ 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0 := by
+  rw [dist_eq_norm_vsub V, inner_eq_norm_sq_left_iff, vsub_sub_vsub_cancel_left,
+    inner_vsub_right_eq_zero_symm]
+
+theorem inner_vsub_vsub_left_eq_dist_sq_right_iff {a b c : P} :
+    ⟪a -ᵥ b, a -ᵥ c⟫ = dist a c ^ 2 ↔ ⟪c -ᵥ b, a -ᵥ c⟫ = 0 := by
+  rw [real_inner_comm, inner_vsub_vsub_left_eq_dist_sq_left_iff, real_inner_comm]
+
+theorem inner_vsub_vsub_right_eq_dist_sq_left_iff {a b c : P} :
+    ⟪a -ᵥ c, b -ᵥ c⟫ = dist a c ^ 2 ↔ ⟪a -ᵥ c, b -ᵥ a⟫ = 0 := by
+  rw [dist_eq_norm_vsub V, inner_eq_norm_sq_left_iff, vsub_sub_vsub_cancel_right,
+    inner_vsub_right_eq_zero_symm]
+
+theorem inner_vsub_vsub_right_eq_dist_sq_right_iff {a b c : P} :
+    ⟪a -ᵥ c, b -ᵥ c⟫ = dist b c ^ 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0 := by
+  rw [real_inner_comm, inner_vsub_vsub_right_eq_dist_sq_left_iff, real_inner_comm]
+
+end Real

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -265,6 +265,18 @@ theorem real_inner_mul_inner_self_le (x y : F) : ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ
       exact le_abs_self _
     _ ≤ ⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ := @inner_mul_inner_self_le ℝ _ _ _ _ x y
 
+theorem inner_eq_ofReal_norm_sq_left_iff {v w : E} : ⟪v, w⟫_𝕜 = ‖v‖ ^ 2 ↔ ⟪v, v - w⟫_𝕜 = 0 := by
+  rw [inner_sub_right, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]
+
+theorem inner_eq_norm_sq_left_iff {v w : F} : ⟪v, w⟫_ℝ = ‖v‖ ^ 2 ↔ ⟪v, v - w⟫_ℝ = 0 :=
+  inner_eq_ofReal_norm_sq_left_iff
+
+theorem inner_eq_ofReal_norm_sq_right_iff {v w : E} : ⟪v, w⟫_𝕜 = ‖w‖ ^ 2 ↔ ⟪v - w, w⟫_𝕜 = 0 := by
+  rw [inner_sub_left, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]
+
+theorem inner_eq_norm_sq_right_iff {v w : F} : ⟪v, w⟫_ℝ = ‖w‖ ^ 2 ↔ ⟪v - w, w⟫_ℝ = 0 :=
+  inner_eq_ofReal_norm_sq_right_iff
+
 end BasicProperties_Seminormed
 
 section BasicProperties

Mathlib/Geometry/Euclidean/Altitude.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
 import Mathlib.Geometry.Euclidean.Projection
+import Mathlib.Analysis.InnerProductSpace.Affine
 
 /-!
 # Altitudes of a simplex
@@ -170,6 +171,101 @@ def height {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : ℝ :=
 lemma height_pos {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : 0 < s.height i := by
   simp [height]
 
+open scoped RealInnerProductSpace
+
+-- TODO: move
+private theorem _root_.Fin.exists_ne_of_ne_of_two_lt
+    {n : ℕ} {i j : Fin n} (h : i ≠ j) (h : 2 < n) : ∃ k, k ≠ i ∧ k ≠ j := by
+  have : NeZero n := ⟨by linarith⟩
+  rcases i with ⟨i, hi⟩
+  rcases j with ⟨j, hj⟩
+  simp_rw [← Fin.val_ne_iff]
+  by_cases h0 : 0 ≠ i ∧ 0 ≠ j
+  · exact ⟨0, h0⟩
+  · by_cases h1 : 1 ≠ i ∧ 1 ≠ j
+    · exact ⟨⟨1, by omega⟩, h1⟩
+    · refine ⟨⟨2, by omega⟩, ?_⟩
+      dsimp only
+      omega
+
+/-- The inner product of an edge from `j` to `i` and the vector from the foot of `i` to `i`
+is the square of the height. -/
+lemma inner_vsub_vsub_altitudeFoot_eq_height_sq
+    {n : ℕ} [NeZero n] (s : Simplex ℝ P n) {i j : Fin (n + 1)} (h : i ≠ j)  :
+    ⟪s.points i -ᵥ s.points j, s.points i -ᵥ s.altitudeFoot i⟫ = s.height i ^ 2 := by
+  rw [height, inner_vsub_vsub_left_eq_dist_sq_right_iff, altitudeFoot]
+  refine Submodule.inner_right_of_mem_orthogonal
+        (K := vectorSpan ℝ (Set.range (s.faceOpposite i).points))
+        (vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
+          (SetLike.coe_mem _)
+          (mem_affineSpan ℝ ?_)) ?_
+  · simp only [range_faceOpposite_points, ne_eq, Set.mem_image, Set.mem_setOf_eq]
+    refine ⟨j, h.symm, rfl⟩
+  · rw [← direction_affineSpan]
+    exact vsub_orthogonalProjection_mem_direction_orthogonal _ _
+
+/-- The angle between two distinct faces can never reach 0 or π. -/
+lemma abs_inner_height_vsub_altitudeFoot_div_lt_one
+    {n : ℕ} [NeZero n] (s : Simplex ℝ P n) {i j : Fin (n + 1)} (hij : i ≠ j) (hn : 1 < n) :
+    |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫
+            / (s.height i * s.height j)| < 1 := by
+  rw [abs_div, div_lt_one (by simp [height])]
+  apply LE.le.lt_of_ne
+  · convert abs_real_inner_le_norm _ _ using 1
+    simp only [dist_eq_norm_vsub, abs_eq_self, height]
+    positivity
+  · simp_rw [height, dist_eq_norm_vsub]
+    nth_rw 2 [abs_eq_self.2 (by positivity)]
+    rw [← Real.norm_eq_abs, ne_eq, norm_inner_eq_norm_iff (by simp) (by simp)]
+    rintro ⟨r, hr, h⟩
+    suffices s.points j -ᵥ s.altitudeFoot j = 0 by
+      simp at this
+    rw [← Submodule.mem_bot ℝ,
+      ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]
+    refine ⟨vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
+      (mem_affineSpan _ (Set.mem_range_self _)) ?_, ?_⟩
+    · refine SetLike.le_def.1 (affineSpan_mono _ ?_) (Subtype.property _)
+      simp
+    · rw [SetLike.mem_coe]
+      have hk : ∃ k, k ≠ i ∧ k ≠ j := Fin.exists_ne_of_ne_of_two_lt hij (by linarith only [hn])
+      have hs : vectorSpan ℝ (Set.range s.points) =
+          vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔
+            vectorSpan ℝ (Set.range (s.faceOpposite j).points) := by
+        rcases hk with ⟨k, hki, hkj⟩
+        have hki' : s.points k ∈ Set.range (s.faceOpposite i).points := by
+          rw [range_faceOpposite_points]
+          exact Set.mem_image_of_mem _ hki
+        have hkj' : s.points k ∈ Set.range (s.faceOpposite j).points := by
+          rw [range_faceOpposite_points]
+          exact Set.mem_image_of_mem _ hkj
+        convert AffineSubspace.vectorSpan_union_of_mem_of_mem ℝ hki' hkj'
+        simp only [range_faceOpposite_points, ← Set.image_union]
+        simp_rw [← Set.image_univ, ← Set.compl_setOf, ← Set.compl_inter,
+          Set.setOf_eq_eq_singleton]
+        rw [Set.inter_singleton_eq_empty.mpr ?_, Set.compl_empty]
+        simpa using hij.symm
+      rw [hs, ← Submodule.inf_orthogonal, Submodule.mem_inf]
+      refine ⟨?_, ?_⟩
+      · rw [h, ← direction_affineSpan]
+        exact Submodule.smul_mem _ _
+          (vsub_orthogonalProjection_mem_direction_orthogonal _ _)
+      · rw [← direction_affineSpan]
+        exact vsub_orthogonalProjection_mem_direction_orthogonal _ _
+
+/-- The angle between two faces can never reach π. -/
+lemma neg_one_lt_inner_height_vsub_altitudeFoot_div
+    {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i j : Fin (n + 1)) (hn : 1 < n) :
+    -1 < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫
+            / (s.height i * s.height j) := by
+  obtain rfl | hij := eq_or_ne i j
+  · rw [real_inner_self_eq_norm_sq, height]
+    refine neg_one_lt_zero.trans_le ?_
+    positivity
+  rw [neg_lt]
+  refine lt_of_abs_lt ?_
+  rw [abs_neg]
+  exact abs_inner_height_vsub_altitudeFoot_div_lt_one s hij hn
+
 end Simplex
 
 end Affine