sum_smul_vsub_const_eq_weightedVSubOfPoint_sub

English

A weighted sum of pairwise subtractions with a constant right-hand point equals a combination of a weightedVSubOfPoint and a constant term.

Русский

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

LaTeX

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

Lean4

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

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