English
Given a finite family of points p_i in an affine space P, a base point b ∈ P, and weights w_i in a ring k, the map that sends w to the vector sum ∑ w_i (p_i − b) is a linear map from the weight space to the direction space V.
Русский
Даны конечная семейство точек p_i в аффинном пространстве P, базовая точка b ∈ P и веса w_i в кольце k. Отображение w ↦ ∑ w_i (p_i − b) является линейным отображением из пространства весов в направление V.
LaTeX
$$$s.weightedVSubOfPoint(p,b) : (ι \\to k) \\to V$; $ (s.weightedVSubOfPoint p b)(w) = \\sum_{i \\in s} w_i (p_i - b)$$$
Lean4
/-- A weighted sum of the results of subtracting a base point from the
given points, as a linear map on the weights. The main cases of
interest are where the sum of the weights is 0, in which case the sum
is independent of the choice of base point, and where the sum of the
weights is 1, in which case the sum added to the base point is
independent of the choice of base point. -/
def weightedVSubOfPoint (p : ι → P) (b : P) : (ι → k) →ₗ[k] V :=
∑ i ∈ s, (LinearMap.proj i : (ι → k) →ₗ[k] k).smulRight (p i -ᵥ b)
