sum_smul_const_vsub_eq_sub_weightedVSubOfPoint

English

A weighted sum of left-constant subtractions equals a subtraction involving a weightedVSubOfPoint.

Русский

Взвешенная сумма левосторонних константных вычитаний равна вычитанию, включающему weightedVSubOfPoint.

LaTeX

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

Lean4

/-- A weighted sum of pairwise subtractions, where the point on the left is constant,
expressed as a subtraction involving a `weightedVSubOfPoint` expression. -/
theorem sum_smul_const_vsub_eq_sub_weightedVSubOfPoint (w : ι → k) (p₂ : ι → P) (p₁ b : P) :
    (∑ i ∈ s, w i • (p₁ -ᵥ p₂ i)) = (∑ i ∈ s, w i) • (p₁ -ᵥ b) - s.weightedVSubOfPoint p₂ b w := by
  rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]

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