English
If the vertices of a simplex lie in a convex region, any two points p1 and p2 in the affine span of that region that are at the same distance to all vertices are either equal or symmetric with respect to the affine span (reflection).
Русский
Если вершины симплекса лежат в выпуклой области, любые два пункта p1, p2 в аффинном замкнутом span такие, что их расстояния до всех вершин одинаковы, либо равны, либо являются отражением относительно аффинного пространства.
LaTeX
$$$(p_1 = p_2) \lor (p_1 = \text{reflection}_{\text{affineSpan}}(p_2))$$$
Lean4
/-- Suppose all distances from `p₁` and `p₂` to the points of a
simplex are equal, and that `p₁` and `p₂` lie in the affine span of
`p` with the vertices of that simplex. Then `p₁` and `p₂` are equal
or reflections of each other in the affine span of the vertices of the
simplex. -/
theorem eq_or_eq_reflection_of_dist_eq {n : ℕ} {s : Simplex ℝ P n} {p p₁ p₂ : P} {r : ℝ}
(hp₁ : p₁ ∈ affineSpan ℝ (insert p (Set.range s.points))) (hp₂ : p₂ ∈ affineSpan ℝ (insert p (Set.range s.points)))
(h₁ : ∀ i, dist (s.points i) p₁ = r) (h₂ : ∀ i, dist (s.points i) p₂ = r) :
p₁ = p₂ ∨ p₁ = reflection (affineSpan ℝ (Set.range s.points)) p₂ :=
by
set span_s := affineSpan ℝ (Set.range s.points)
have h₁' := s.orthogonalProjection_eq_circumcenter_of_dist_eq h₁
have h₂' := s.orthogonalProjection_eq_circumcenter_of_dist_eq h₂
rw [← affineSpan_insert_affineSpan, mem_affineSpan_insert_iff (orthogonalProjection_mem p)] at hp₁ hp₂
obtain ⟨r₁, p₁o, hp₁o, hp₁⟩ := hp₁
obtain ⟨r₂, p₂o, hp₂o, hp₂⟩ := hp₂
obtain rfl : ↑(s.orthogonalProjectionSpan p₁) = p₁o :=
by
subst hp₁
exact s.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection hp₁o
rw [h₁'] at hp₁
obtain rfl : ↑(s.orthogonalProjectionSpan p₂) = p₂o :=
by
subst hp₂
exact s.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection hp₂o
rw [h₂'] at hp₂
have h : s.points 0 ∈ span_s := mem_affineSpan ℝ (Set.mem_range_self _)
have hd₁ : dist p₁ s.circumcenter * dist p₁ s.circumcenter = r * r - s.circumradius * s.circumradius :=
s.dist_circumcenter_sq_eq_sq_sub_circumradius h₁ h₁' h
have hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius :=
s.dist_circumcenter_sq_eq_sq_sub_circumradius h₂ h₂' h
rw [← hd₂, hp₁, hp₂, dist_eq_norm_vsub V _ s.circumcenter, dist_eq_norm_vsub V _ s.circumcenter, vadd_vsub, vadd_vsub,
← real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, real_inner_smul_left, real_inner_smul_left,
real_inner_smul_right, real_inner_smul_right, ← mul_assoc, ← mul_assoc] at hd₁
by_cases hp : p = s.orthogonalProjectionSpan p
· rw [Simplex.orthogonalProjectionSpan] at hp
rw [hp₁, hp₂, ← hp]
simp only [true_or, smul_zero, vsub_self]
· have hz : ⟪p -ᵥ orthogonalProjection span_s p, p -ᵥ orthogonalProjection span_s p⟫ ≠ 0 := by
simpa only [Ne, vsub_eq_zero_iff_eq, inner_self_eq_zero] using hp
rw [mul_left_inj' hz, mul_self_eq_mul_self_iff] at hd₁
rw [hp₁, hp₂]
rcases hd₁ with hd₁ | hd₁
· left
rw [hd₁]
· right
rw [hd₁, reflection_vadd_smul_vsub_orthogonalProjection p r₂ s.circumcenter_mem_affineSpan, neg_smul]
