Completing the square for a weighted sum of squared distances #
In a real inner product space, a weighted sum a ‖y‖² + b ‖x - y‖² of the squared distances from
y to the two points 0 and x is, as a function of y, a multiple of the squared distance
from y to the weighted centre (b / (a + b)) • x, plus a constant:
a ‖y‖² + b ‖x - y‖² = (a + b) ‖y - (b / (a + b)) • x‖² + (a b / (a + b)) ‖x‖²
whenever a + b ≠ 0. This is the identity behind products of Gaussians being Gaussians.
Main declarations #
TauCeti.mul_norm_sq_add_mul_norm_sub_sq: the completed-square identity above.
theorem
TauCeti.mul_norm_sq_add_mul_norm_sub_sq
{F : Type u_1}
[SeminormedAddCommGroup F]
[InnerProductSpace ℝ F]
{a b : ℝ}
(hab : a + b ≠ 0)
(x y : F)
:
Completing the square for a weighted sum of squared distances: if a + b ≠ 0, then
a ‖y‖² + b ‖x - y‖² = (a + b) ‖y - (b / (a + b)) • x‖² + (a b / (a + b)) ‖x‖².