sum_smul_const_vsub_eq_neg_weightedVSub

English

If the weights sum to 0, then sum_i w_i (p1 −ᵥ p2 i) equals the negative of weightedVSub of p2 with weights w.

Русский

При сумме весов равной нулю сумма w_i (p1 −ᵥ p2 i) равна −WeightedVSub(p2,w).

LaTeX

$$$\\displaystyle \\sum_{i\\in s} w_i\\,(p_1-ᵥ p_2(i)) = -\,s.weightedVSub(p_2,w)$, если $\\sum_{i\\in s} w_i = 0$.$$

Lean4

/-- A weighted sum of pairwise subtractions, where the point on the left is constant and the
sum of the weights is 0. -/
theorem sum_smul_const_vsub_eq_neg_weightedVSub (w : ι → k) (p₂ : ι → P) (p₁ : P) (h : ∑ i ∈ s, w i = 0) :
    (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i)) = -s.weightedVSub p₂ w := by
  rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, zero_sub]

Похожие утверждения