English
For a nondegenerate real quadratic form Q on a finite-dimensional real vector space, there exists a finite set of signs w taking values in {−1,1} such that Q is equivalent to a weighted sum of squares with coefficients w.
Русский
Для неубывающейся реальной квадратичной формы Q на конечномерном вещественном пространстве существует конечный набор знаков из {−1,1}, таких что Q эквивалентна взвешенной сумме квадратов с весами w.
LaTeX
$$$\\exists w: \\mathrm{Fin}(\\mathrm{finrank}_{\\mathbb{R}} M) \\to \\{-,+\\},\\quad \\forall i, w(i) \\in \\{-1,1\\} \\land \\text{Equivalent}(Q, \\text{weightedSumSquares } \\mathbb{R} w)$$$
Lean4
/-- **Sylvester's law of inertia**: A nondegenerate real quadratic form is equivalent to a weighted
sum of squares with the weights being ±1, `SignType` version. -/
theorem equivalent_sign_ne_zero_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M]
(Q : QuadraticForm ℝ M) (hQ : (associated (R := ℝ) Q).SeparatingLeft) :
∃ w : Fin (Module.finrank ℝ M) → SignType, (∀ i, w i ≠ 0) ∧ Equivalent Q (weightedSumSquares ℝ fun i ↦ (w i : ℝ)) :=
let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares_units_of_nondegenerate' hQ
⟨sign ∘ ((↑) : ℝˣ → ℝ) ∘ w, fun i => sign_ne_zero.2 (w i).ne_zero,
⟨hw₁.trans (isometryEquivSignWeightedSumSquares (((↑) : ℝˣ → ℝ) ∘ w))⟩⟩
