English
The squared distance between points on a line parameterized by r along a fixed vector v from p1 is a quadratic polynomial in r with coefficients given by inner products and distances.
Русский
Квадрат расстояния между точками на прямой, задаваемой параметром r по фиксированному вектору v от p1, есть квадратичная функция по r с коэффициентами из скалярного произведения и расстояний.
LaTeX
$$$ dist(r\cdot v + p_1, p_2)^2 = (v,v) r^2 + 2 \langle v, p_1 - p_2 \rangle r + \langle p_1 - p_2, p_1 - p_2 \rangle $$$
Lean4
/-- The squared distance between points on a line (expressed as a
multiple of a fixed vector added to a point) and another point,
expressed as a quadratic. -/
theorem dist_smul_vadd_sq (r : ℝ) (v : V) (p₁ p₂ : P) :
dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ = ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ :=
by
rw [dist_eq_norm_vsub V _ p₂, ← real_inner_self_eq_norm_mul_norm, vadd_vsub_assoc, real_inner_add_add_self,
real_inner_smul_left, real_inner_smul_left, real_inner_smul_right]
ring
