English
A weighted sum over the difference of two Finsets equals the difference of affine combinations adjusted by the subtracted weights: (s \ s₂).affineCombination k p w -ᵥ s₂.affineCombination k p (-w) = s.weightedVSub p w.
Русский
Взвешенная сумма по разности двух Finset равна разности соответствующих аффинных комбинаций с учётом двойной смены знака весов.
LaTeX
$$$$ (s \ s_2).affineCombination_k(p,w) -_V s_2.affineCombination_k(p,-w) = s.weightedVSub p w. $$$$
Lean4
/-- A weighted sum may be split into a subtraction of affine combinations over two subsets. -/
theorem affineCombination_sdiff_sub [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k) (p : ι → P) :
(s \ s₂).affineCombination k p w -ᵥ s₂.affineCombination k p (-w) = s.weightedVSub p w :=
by
simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]
exact s.weightedVSub_sdiff_sub h _ _
