English
The touchpoint weights are governed by the excenter and the affine structure of the simplex.
Русский
Веса точек касания удовлетворяют линейному равенству, связывающему эксцентр и радиус.
LaTeX
$$$ s.touchpointWeights(\text{signs}, i, j) \text{ satisfy affine relations with } s.excenter(\text{signs}) $$$
Lean4
theorem touchpoint_injective {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) :
Function.Injective (s.touchpoint signs) := by
intro i j hij
by_contra hne
by_cases hn1 : n = 1
· subst hn1
rw [s.touchpoint_eq_point_rev signs i, s.touchpoint_eq_point_rev signs j] at hij
apply s.independent.injective.ne hne
convert hij.symm <;> clear hij <;> decide +revert
· suffices s.excenter signs -ᵥ s.touchpoint signs i ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
by
have h' : s.excenter signs -ᵥ s.touchpoint signs i ∈ (vectorSpan ℝ (Set.range s.points)) :=
by
rw [← direction_affineSpan]
exact
AffineSubspace.vsub_mem_direction h.excenter_mem_affineSpan_range (s.touchpoint_mem_affineSpan_simplex _ _)
have h0 : s.excenter signs -ᵥ s.touchpoint signs i = 0 :=
by
rw [← Submodule.mem_bot ℝ, ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]
exact ⟨h', this⟩
rw [← norm_eq_zero, ← dist_eq_norm_vsub, h.dist_excenter] at h0
exact h.exradius_pos.ne' h0
obtain ⟨k, hki, hkj⟩ : ∃ k, k ≠ i ∧ k ≠ j := Fin.exists_ne_and_ne_of_two_lt i j (by cutsat)
have hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points :=
by
simp only [range_faceOpposite_points, ← Set.image_union, ← Set.compl_inter]
convert Set.image_univ.symm
simp [Ne.symm hne]
rw [hu, range_faceOpposite_points, range_faceOpposite_points,
AffineSubspace.vectorSpan_union_of_mem_of_mem ℝ (p := s.points k) (Set.mem_image_of_mem _ (by simp [hki]))
(Set.mem_image_of_mem _ (by simp [hkj])),
← Submodule.inf_orthogonal]
refine ⟨?_, ?_⟩
· rw [← direction_affineSpan, ← range_faceOpposite_points]
exact vsub_orthogonalProjection_mem_direction_orthogonal _ _
· rw [hij, ← direction_affineSpan, ← range_faceOpposite_points]
exact vsub_orthogonalProjection_mem_direction_orthogonal _ _
