Real quadratic forms #
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 nondegerate we can take the weights to be ±1,
as in equivalent_one_zero_neg_one_weighted_sum_squared
.
noncomputable
def
quadratic_form.isometry_sign_weighted_sum_squares
{ι : Type u_1}
[fintype ι]
[decidable_eq ι]
(w : ι → ℝ) :
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
- quadratic_form.isometry_sign_weighted_sum_squares w = let u : ι → ℝˣ := λ (i : ι), dite (w i = 0) (λ (h : w i = 0), 1) (λ (h : ¬w i = 0), units.mk0 (w i) h) in _.mpr ((quadratic_form.weighted_sum_squares ℝ w).isometry_basis_repr ((pi.basis_fun ℝ ι).units_smul (λ (i : ι), _.unit)))
theorem
quadratic_form.equivalent_one_neg_one_weighted_sum_squared
{M : Type u_1}
[add_comm_group M]
[module ℝ M]
[finite_dimensional ℝ M]
(Q : quadratic_form ℝ M)
(hQ : (⇑quadratic_form.associated Q).nondegenerate) :
∃ (w : fin (finite_dimensional.finrank ℝ M) → ℝ), (∀ (i : fin (finite_dimensional.finrank ℝ M)), w i = -1 ∨ w i = 1) ∧ Q.equivalent (quadratic_form.weighted_sum_squares ℝ w)
Sylvester's law of inertia: A nondegenerate real quadratic form is equivalent to a weighted sum of squares with the weights being ±1.
theorem
quadratic_form.equivalent_one_zero_neg_one_weighted_sum_squared
{M : Type u_1}
[add_comm_group M]
[module ℝ M]
[finite_dimensional ℝ M]
(Q : quadratic_form ℝ M) :
∃ (w : fin (finite_dimensional.finrank ℝ M) → ℝ), (∀ (i : fin (finite_dimensional.finrank ℝ M)), w i = -1 ∨ w i = 0 ∨ w i = 1) ∧ Q.equivalent (quadratic_form.weighted_sum_squares ℝ w)
Sylvester's law of inertia: A real quadratic form is equivalent to a weighted sum of squares with the weights being ±1 or 0.