sum_smul_vsub_const_eq_weightedVSub

English

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

Русский

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

LaTeX

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

Lean4

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

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