sum_smul_vsub_const_eq_affineCombination_vsub

English

A weighted sum with the left point fixed equals the left-point affine subtraction: ∑_{i∈s} w_i · (p1 -_V p2(i)) = p1 -_V s.affineCombination k p2 w, given ∑ w_i = 1.

Русский

Взвешенная сумма с фиксированной левой точкой равна вычитанию левой точки и аффинной комбинации правой части.

LaTeX

$$$$ \sum_{i\in s} w(i) \cdot (p_1 -_V p_2(i)) = p_1 -_V s.affineCombination_k(p_2, w). $$$$

Lean4

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

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