sum_smul_vsub_eq_affineCombination_vsub

English

A weighted sum of pairwise subtractions equals the difference of two affine combinations: ∑_{i∈s} w_i · (p1(i) -_V p2(i)) = s.affineCombination k p1 w -_V s.affineCombination k p2 w.

Русский

Сумма с весами взводит различия между точками: взвешенная сумма попарных разностей равна разности двух аффинных комбинаций.

LaTeX

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

Lean4

/-- A weighted sum of pairwise subtractions, expressed as a subtraction of two `affineCombination`
expressions. -/
theorem sum_smul_vsub_eq_affineCombination_vsub (w : ι → k) (p₁ p₂ : ι → P) :
    (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) = s.affineCombination k p₁ w -ᵥ s.affineCombination k p₂ w :=
  by
  simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]
  exact s.sum_smul_vsub_eq_weightedVSubOfPoint_sub _ _ _ _

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