English
For any finite set with weights summing to 1, the distance between the two affine combinations equals a quadratic form in the weight differences and pairwise distances.
Русский
Для конечного множества с весами, сумма которых равна 1, расстояние между аффинными комбинациями равняется квадратичной форме по разности весов и попарных расстояний.
LaTeX
$$$ dist( s.weightedVSub p_1, s.weightedVSub p_2 )^2 = -\dfrac{1}{2} \sum_{i_1\in s} \sum_{i_2\in s} (w_1(i_1)-w_2(i_1))(w_1(i_2)-w_2(i_2)) \\ \times dist(p_1(i_1), p_2(i_2))^2 $$$
Lean4
/-- The distance between two points given with `affineCombination`,
in terms of the pairwise distances between the points in that
combination. -/
theorem dist_affineCombination {ι : Type*} {s : Finset ι} {w₁ w₂ : ι → ℝ} (p : ι → P) (h₁ : ∑ i ∈ s, w₁ i = 1)
(h₂ : ∑ i ∈ s, w₂ i = 1) : by
have a₁ := s.affineCombination ℝ p w₁
have a₂ := s.affineCombination ℝ p w₂
exact
dist a₁ a₂ * dist a₁ a₂ =
(-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2 :=
by
dsimp only
rw [dist_eq_norm_vsub V (s.affineCombination ℝ p w₁) (s.affineCombination ℝ p w₂), ← @inner_self_eq_norm_mul_norm ℝ,
Finset.affineCombination_vsub]
have h : (∑ i ∈ s, (w₁ - w₂) i) = 0 := by simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, h₁, h₂, sub_self]
exact inner_weightedVSub p h p h
