weightedSumSquares_apply — Mathlib

English

If a basis is orthogonal for the associated quadratic form, then the basis representation equals a weighted sum of squares.

Русский

Если базис ортогонален относительно ассоциированной квадратичной формы, то представление базиса выражается как взвешенная сумма квадратов.

LaTeX

$$basisRepr(Q, v) = weightedSumSquares R (λ i, Q(v_i))$$

Lean4

@[simp]
theorem weightedSumSquares_apply [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (w : ι → S) (v : ι → R) :
    weightedSumSquares R w v = ∑ i : ι, w i • (v i * v i) :=
  QuadraticMap.sum_apply _ _ _

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