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.

source

noncomputable def quadratic_form.isometry_sign_weighted_sum_squares {ι : Type u_1} [fintype ι] [decidable_eq ι] (w : ι → ℝ) :

(quadratic_form.weighted_sum_squares ℝ w).isometry (quadratic_form.weighted_sum_squares ℝ (real.sign ∘ 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)))

source

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.

source

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.