sum_smul_vsub_eq_weightedVSubOfPoint_sub

English

A weighted sum of pairwise subtractions equals the difference of two weightedVSubOfPoint expressions.

Русский

Взвешенная сумма попаренных вычитаний равна разности двух выражений weightedVSubOfPoint.

LaTeX

$$$ \\sum_{i \\in s} w_i \\,(p_1 i - p_2 i) = s.weightedVSubOfPoint p_1 b w - s.weightedVSubOfPoint p_2 b w $$$

Lean4

/-- A weighted sum of pairwise subtractions, expressed as a subtraction of two
`weightedVSubOfPoint` expressions. -/
theorem sum_smul_vsub_eq_weightedVSubOfPoint_sub (w : ι → k) (p₁ p₂ : ι → P) (b : P) :
    (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) = s.weightedVSubOfPoint p₁ b w - s.weightedVSubOfPoint p₂ b w := by
  simp_rw [weightedVSubOfPoint_apply, ← sum_sub_distrib, ← smul_sub, vsub_sub_vsub_cancel_right]

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