QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared
theorem QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared :
∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module ℝ M] [inst_2 : FiniteDimensional ℝ M]
(Q : QuadraticForm ℝ M),
∃ w,
(∀ (i : Fin (FiniteDimensional.finrank ℝ M)), w i = -1 ∨ w i = 0 ∨ w i = 1) ∧
Q.Equivalent (QuadraticForm.weightedSumSquares ℝ w)
This theorem is a statement of Sylvester's law of inertia in the context of real quadratic forms. It asserts that for any real quadratic form `Q` on a finite-dimensional real vector space `M`, there exists a function `w` such that for each index `i` in the finite dimensional range of `M`, `w i` equals `-1`, `0`, or `1`, and moreover, `Q` is equivalent to a weighted sum of squares, where the weights are provided by `w`. In other words, any real quadratic form can be expressed as a sum of squares, where each square is multiplied by either `-1`, `0`, or `1`.
More concisely: Every real quadratic form on a finite-dimensional real vector space is equivalent to a weighted sum of squares with weights in {-1, 0, 1}.
|
QuadraticForm.equivalent_one_neg_one_weighted_sum_squared
theorem QuadraticForm.equivalent_one_neg_one_weighted_sum_squared :
∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module ℝ M] [inst_2 : FiniteDimensional ℝ M]
(Q : QuadraticForm ℝ M),
LinearMap.SeparatingLeft (QuadraticForm.associated Q) →
∃ w,
(∀ (i : Fin (FiniteDimensional.finrank ℝ M)), w i = -1 ∨ w i = 1) ∧
Q.Equivalent (QuadraticForm.weightedSumSquares ℝ w)
**Sylvester's Law of Inertia**: This theorem states that for any nondegenerate real quadratic form, there exists a weighted sum of squares equivalent to it where the weights are either -1 or 1. Specifically, given a nondegenerate real quadratic form 'Q' and a positive-definite bilinear form associated with 'Q', there exists a function 'w' defined on the finite dimensional real vector space such that each value of 'w' is either -1 or 1 and 'Q' is equivalent to the weighted sum of squares with weights defined by 'w'. The dimension of the vector space is determined by the rank of the module.
More concisely: For any nondegenerate real quadratic form, there exists an equivalent representation as a weighted sum of squares with weights being -1 or 1.
|