English
If two finite weighted sums have zero total weights, their inner product equals a certain negative- half double-weight combination of pairwise differences.
Русский
Если два конечных взвешенных сумм имеют нулевые суммы весов, их внутреннее произведение равно некотариальной комбинации парных разностей.
LaTeX
$$$$ \\langle \\sum_{i\\in s_1} w_1(i) v_1(i), \\sum_{j\\in s_2} w_2(j) v_2(j) \\rangle = -\\frac{1}{2} \\sum_{i,j} w_1(i) w_2(j) \\|v_1(i) - v_2(j)\\|^2.$$$$
Lean4
/-- The inner product of two weighted sums, where the weights in each
sum add to 0, in terms of the norms of pairwise differences. -/
theorem inner_sum_smul_sum_smul_of_sum_eq_zero {ι₁ : Type*} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ} (v₁ : ι₁ → F)
(h₁ : ∑ i ∈ s₁, w₁ i = 0) {ι₂ : Type*} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (v₂ : ι₂ → F) (h₂ : ∑ i ∈ s₂, w₂ i = 0) :
⟪∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ =
(-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2 :=
by
simp_rw [sum_inner, inner_sum, real_inner_smul_left, real_inner_smul_right,
real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, ← div_sub_div_same, add_div,
mul_sub_left_distrib, left_distrib, Finset.sum_sub_distrib, Finset.sum_add_distrib, ← Finset.mul_sum, ←
Finset.sum_mul, h₁, h₂, zero_mul, mul_zero, Finset.sum_const_zero, zero_add, zero_sub, Finset.mul_sum, neg_div,
Finset.sum_div, mul_div_assoc, mul_assoc]
