weightedVSubOfPoint_apply — Mathlib

English

The evaluation of the weighted sum is the explicit finite sum: (s.weightedVSubOfPoint p b w) = ∑ i∈s w_i (p_i − b).

Русский

Оценка взвешенной суммы равна явной конечной сумме: (s.weightedVSubOfPoint p b w) = ∑_{i∈s} w_i (p_i − b).

LaTeX

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

Lean4

@[simp]
theorem weightedVSubOfPoint_apply (w : ι → k) (p : ι → P) (b : P) :
    s.weightedVSubOfPoint p b w = ∑ i ∈ s, w i • (p i -ᵥ b) := by simp [weightedVSubOfPoint, LinearMap.sum_apply]

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