English
For any vectors x,y, the squared distance between x and y equals the sum of squared norms minus twice the product of norms times cos of the angle between x and y.
Русский
Для любых векторов x,y квадрат расстояния между ними равен сумме квадратов норм минус удвоенное произведение норм на косинус угла между x и y.
LaTeX
$$$\|x-y\|^2 = \|x\|^2 + \|y\|^2 - 2\|x\|\|y\| \cos(\angle x,y)$$$
Lean4
/-- **Law of cosines** (cosine rule), vector angle form. -/
theorem norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle (x y : V) :
‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) := by
rw [show 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖)) by ring,
cos_angle_mul_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, ←
real_inner_self_eq_norm_mul_norm, real_inner_sub_sub_self, sub_add_eq_add_sub]
