English
The squared distance between two points obtained by orthogonal additions along the same vector is given by a sum of squared terms.
Русский
Квадрат расстояния между двумя точками, полученными ортогональным добавлением одного и того же вектора, равен сумме квадратов членов.
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 between two points constructed by
adding multiples of the same orthogonal vector to points in the same
subspace. -/
theorem dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd {s : AffineSubspace ℝ P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s)
(hp₂ : p₂ ∈ s) (r₁ r₂ : ℝ) {v : V} (hv : v ∈ s.directionᗮ) :
dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
dist p₁ p₂ * dist p₁ p₂ + (r₁ - r₂) * (r₁ - r₂) * (‖v‖ * ‖v‖) :=
calc
dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ :=
by
rw [dist_eq_norm_vsub V (r₁ • v +ᵥ p₁), vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, sub_smul, add_comm, add_sub_assoc]
_ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖(r₁ - r₂) • v‖ * ‖(r₁ - r₂) • v‖ :=
(norm_add_sq_eq_norm_sq_add_norm_sq_real
(Submodule.inner_right_of_mem_orthogonal (vsub_mem_direction hp₁ hp₂) (Submodule.smul_mem _ _ hv)))
_ = ‖(p₁ -ᵥ p₂ : V)‖ * ‖(p₁ -ᵥ p₂ : V)‖ + |r₁ - r₂| * |r₁ - r₂| * ‖v‖ * ‖v‖ :=
by
rw [norm_smul, Real.norm_eq_abs]
ring
_ = dist p₁ p₂ * dist p₁ p₂ + (r₁ - r₂) * (r₁ - r₂) * (‖v‖ * ‖v‖) := by
rw [dist_eq_norm_vsub V p₁, abs_mul_abs_self, mul_assoc]
