English
The inner product of two weighted vector subtractions can be expressed as a double sum of weights times pairwise distances, scaled by 1/2.
Русский
Параметризованное скалярное произведение для взвешенных векторов можно записать как двойную сумму весов и попарных расстояний, умноженную на 1/2.
LaTeX
$$$ \langle s_1.weightedVSub\, p_1\, w_1 , s_2.weightedVSub\, p_2\, w_2 \rangle = -\frac{1}{2} \sum_{i_1 \in s_1} \sum_{i_2 \in s_2} w_1(i_1) w_2(i_2) \big( dist(p_1(i_1), p_2(i_2)) \cdot dist(p_1(i_1), p_2(i_2)) \big) $$$
Lean4
/-- The inner product of two vectors given with `weightedVSub`, in
terms of the pairwise distances. -/
theorem inner_weightedVSub {ι₁ : Type*} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ} (p₁ : ι₁ → P) (h₁ : ∑ i ∈ s₁, w₁ i = 0)
{ι₂ : Type*} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (p₂ : ι₂ → P) (h₂ : ∑ i ∈ s₂, w₂ i = 0) :
⟪s₁.weightedVSub p₁ w₁, s₂.weightedVSub p₂ w₂⟫ =
(-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2 :=
by
rw [Finset.weightedVSub_apply, Finset.weightedVSub_apply, inner_sum_smul_sum_smul_of_sum_eq_zero _ h₁ _ h₂]
simp_rw [vsub_sub_vsub_cancel_right]
rcongr (i₁ i₂) <;> rw [dist_eq_norm_vsub V (p₁ i₁) (p₂ i₂)]
