# Documentation

Sylvester's law of inertia equivalent_one_neg_one_weighted_sum_squared: A real quadratic form is equivalent to a weighted sum of squares with the weights being ±1 or 0.

When the real quadratic form is nondegenerate we can take the weights to be ±1, as in equivalent_one_zero_neg_one_weighted_sum_squared.

noncomputable def QuadraticForm.isometryEquivSignWeightedSumSquares {ι : Type u_1} [] (w : ι) :
.IsometryEquiv (QuadraticForm.weightedSumSquares fun (i : ι) => (SignType.sign (w i)))

The isometry between a weighted sum of squares with weights u on the (non-zero) real numbers and the weighted sum of squares with weights sign ∘ u.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem QuadraticForm.equivalent_sign_ne_zero_weighted_sum_squared {M : Type u_2} [] [] [] (Q : ) (hQ : LinearMap.SeparatingLeft (QuadraticForm.associated Q)) :
∃ (w : ), (∀ (i : ), w i 0) Q.Equivalent (QuadraticForm.weightedSumSquares fun (i : ) => (w i))

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 QuadraticForm.equivalent_one_neg_one_weighted_sum_squared {M : Type u_2} [] [] [] (Q : ) (hQ : LinearMap.SeparatingLeft (QuadraticForm.associated Q)) :
∃ (w : ), (∀ (i : ), w i = -1 w i = 1) Q.Equivalent

Sylvester's law of inertia: A nondegenerate real quadratic form is equivalent to a weighted sum of squares with the weights being ±1.

theorem QuadraticForm.equivalent_signType_weighted_sum_squared {M : Type u_2} [] [] [] (Q : ) :
∃ (w : ), Q.Equivalent (QuadraticForm.weightedSumSquares fun (i : ) => (w i))

Sylvester's law of inertia: A real quadratic form is equivalent to a weighted sum of squares with the weights being ±1 or 0, SignType version.

theorem QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared {M : Type u_2} [] [] [] (Q : ) :
∃ (w : ), (∀ (i : ), w i = -1 w i = 0 w i = 1) Q.Equivalent

Sylvester's law of inertia: A real quadratic form is equivalent to a weighted sum of squares with the weights being ±1 or 0.