English
The square distance formula remains stable under orthogonal additions along an orthogonal direction.
Русский
Квадрат расстояния сохраняется при ортогональном сложении вдоль ортогонального направления.
LaTeX
$$$ dist(r_1 v + p_1, r_2 v + p_2)^2 = dist(p_1,p_2)^2 + (r_1 - r_2)^2 \|v\|^2 $$$
Lean4
/-- The square of the distance from a point in `s` to `p₂` equals the
sum of the squares of the distances of the two points to the
`orthogonalProjection`. -/
theorem dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq {s : AffineSubspace ℝ P} [Nonempty s]
[s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (hp₁ : p₁ ∈ s) :
dist p₁ p₂ * dist p₁ p₂ =
dist p₁ (orthogonalProjection s p₂) * dist p₁ (orthogonalProjection s p₂) +
dist p₂ (orthogonalProjection s p₂) * dist p₂ (orthogonalProjection s p₂) :=
by
rw [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₁ (orthogonalProjection s 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 s p₂)
