affineCombination_eq_linear_combination

English

If s is a finite set, p: s → V, w: s → k and the sum of weights ∑_{i∈s} w(i) equals 1, then the affine combination s.affineCombination k p w equals the linear combination ∑_{i∈s} w(i) p(i).

Русский

Пусть s — конечное множество; p: s → V; w: s → k; и сумма весов равна 1. Тогда аффинная комбинация над s равна линейной комбинации тех же точек.

LaTeX

$$$$s.\text{affineCombination}_k(p,w) = \sum_{i\in s} w(i)\, p(i)\quad\text{whenever}\quad \sum_{i\in s} w(i)=1.$$$$

Lean4

/-- Viewing a module as an affine space modelled on itself, affine combinations are just linear
combinations. -/
@[simp]
theorem affineCombination_eq_linear_combination (s : Finset ι) (p : ι → V) (w : ι → k) (hw : ∑ i ∈ s, w i = 1) :
    s.affineCombination k p w = ∑ i ∈ s, w i • p i := by
  simp [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw 0]

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