English
For a simplex s and any p1 in its affine span, the squared distance from p1 to p2 equals the sum of the squared distance from p1 to the projection of p2 onto s and the squared distance from p2 to that projection.
Русский
Для симплекса s и любой точки p1 в аффинном пространства s справедливо равенство квадратов расстояний: dist(p1,p2)^2 = dist(p1,Proj_s(p2))^2 + dist(p2,Proj_s(p2))^2.
LaTeX
$$$$\operatorname{dist}(p_1, p_2)^2 = \operatorname{dist}(p_1, \mathrm{Proj}_s(p_2))^2 + \operatorname{dist}(p_2, \mathrm{Proj}_s(p_2))^2.$$$$
Lean4
theorem dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq {n : ℕ} (s : Simplex ℝ P n) {p₁ : P}
(p₂ : P) (hp₁ : p₁ ∈ affineSpan ℝ (Set.range s.points)) :
dist p₁ p₂ * dist p₁ p₂ =
dist p₁ (s.orthogonalProjectionSpan p₂) * dist p₁ (s.orthogonalProjectionSpan p₂) +
dist p₂ (s.orthogonalProjectionSpan p₂) * dist p₂ (s.orthogonalProjectionSpan p₂) :=
by
rw [PseudoMetricSpace.dist_comm p₂ _, dist_eq_norm_vsub V p₁ _, dist_eq_norm_vsub V p₁ _, dist_eq_norm_vsub V _ p₂, ←
vsub_add_vsub_cancel p₁ (s.orthogonalProjectionSpan p₂) p₂,
norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]
exact
Submodule.inner_right_of_mem_orthogonal (vsub_orthogonalProjection_mem_direction p₂ hp₁)
(orthogonalProjection_vsub_mem_direction_orthogonal _ p₂)
