equivalent_weightedSumSquares — Mathlib

English

There exists a finite weight vector w such that Q is equivalent to the weighted sum of squares with weights w.

Русский

Существуют веса $w$ так, что $Q$ эквивалентна взвешенной сумме квадратов с весами $w$.

LaTeX

$$$\exists w: Fin(\mathrm{finrank}_K V) \to K,\; Q \;\text{Equivalent}\; \operatorname{weightedSumSquares} K w$$$

Lean4

theorem equivalent_weightedSumSquares (Q : QuadraticForm K V) :
    ∃ w : Fin (Module.finrank K V) → K, Equivalent Q (weightedSumSquares K w) :=
  let ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm _ Q)
  ⟨_, ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩

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