English
The linear part of the affine combination equals the corresponding weightedVSub.
Русский
Линейная часть аффинного сочетания равна соответствующему weightedVSub.
LaTeX
$$$ (s.affineCombination k p).linear = s.weightedVSub p $$$
Lean4
/-- A weighted sum of the results of subtracting a default base point
from the given points, added to that base point, as an affine map on
the weights. This is intended to be used when the sum of the weights
is 1, in which case it is an affine combination (barycenter) of the
points with the given weights; that condition is specified as a
hypothesis on those lemmas that require it. -/
def affineCombination (p : ι → P) : (ι → k) →ᵃ[k] P
where
toFun w := s.weightedVSubOfPoint p (Classical.choice S.nonempty) w +ᵥ Classical.choice S.nonempty
linear := s.weightedVSub p
map_vadd' w₁ w₂ := by simp_rw [vadd_vadd, weightedVSub, vadd_eq_add, LinearMap.map_add]
