English
Adding a vector v to every point in the index set corresponds to subtracting v from the base point in the other slot of the subtraction, preserving the weighted sum: s.weightedVSubOfPoint (v + p) b w = s.weightedVSubOfPoint p (-v + b) w.
Русский
Добавление вектора v ко всем точкам индекса эквивалентно вычитанию v из базовой точки в другой позиции; взвешенная сумма сохраняется.
LaTeX
$$$ s.weightedVSubOfPoint (v + p) b w = s.weightedVSubOfPoint p (-v + b) w $$$
Lean4
/-- The weighted sum, added to the base point, is independent of the
base point when the sum of the weights is 1. -/
theorem weightedVSubOfPoint_vadd_eq_of_sum_eq_one (w : ι → k) (p : ι → P) (h : ∑ i ∈ s, w i = 1) (b₁ b₂ : P) :
s.weightedVSubOfPoint p b₁ w +ᵥ b₁ = s.weightedVSubOfPoint p b₂ w +ᵥ b₂ :=
by
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← @vsub_eq_zero_iff_eq V, vadd_vsub_assoc,
vsub_vadd_eq_vsub_sub, ← add_sub_assoc, add_comm, add_sub_assoc, ← sum_sub_distrib]
conv_lhs =>
congr
· skip
· congr
· skip
· ext
rw [← smul_sub, vsub_sub_vsub_cancel_left]
rw [← sum_smul, h, one_smul, vsub_add_vsub_cancel, vsub_self]
