English
There exists a finite sign function w taking values in {−1,0,1} such that the real quadratic form Q is equivalent to the weighted sum of squares with weights w.
Русский
Существует функция знаков, принимающая значения из {−1,0,1}, такая что Q эквивалентна взвешенной сумме квадратов с весами w.
LaTeX
$$$\\exists w: \\mathrm{Fin}(\\mathrm{finrank}_{\\mathbb{R}} M) \\to \\{ -1,0,1\\}, \\ \\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. -/
theorem equivalent_one_neg_one_weighted_sum_squared {M : Type*} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M]
(Q : QuadraticForm ℝ M) (hQ : (associated (R := ℝ) Q).SeparatingLeft) :
∃ w : Fin (Module.finrank ℝ M) → ℝ, (∀ i, w i = -1 ∨ w i = 1) ∧ Equivalent Q (weightedSumSquares ℝ w) :=
let ⟨w, hw₀, hw⟩ := Q.equivalent_sign_ne_zero_weighted_sum_squared hQ
⟨(w ·), fun i ↦ by cases hi : w i <;> simp_all, hw⟩
