Documentation

Mathlib.LinearAlgebra.QuadraticForm.Real

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 nondegenerate we can take the weights to be ±1, as in equivalent_one_zero_neg_one_weighted_sum_squared.

source
noncomputable def QuadraticForm.isometryEquivSignWeightedSumSquares {ι : Type u_1} [Fintype ι] (w : ι → ℝ) :
(QuadraticMap.weightedSumSquares ℝ w).IsometryEquiv (QuadraticMap.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
    source
    theorem QuadraticForm.equivalent_sign_ne_zero_weighted_sum_squared {M : Type u_2} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) (hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q)) :
    ∃ (w : Fin (Module.finrank ℝ M) → SignType), (∀ (i : Fin (Module.finrank ℝ M)), w i ≠ 0) ∧ QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ fun (i : Fin (Module.finrank ℝ M)) => ↑(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.

    source
    theorem QuadraticForm.equivalent_one_neg_one_weighted_sum_squared {M : Type u_2} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) (hQ : LinearMap.SeparatingLeft (QuadraticMap.associated Q)) :
    ∃ (w : Fin (Module.finrank ℝ M) → ℝ), (∀ (i : Fin (Module.finrank ℝ M)), w i = -1 ∨ w i = 1) ∧ QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ 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 QuadraticForm.equivalent_signType_weighted_sum_squared {M : Type u_2} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) :
    ∃ (w : Fin (Module.finrank ℝ M) → SignType), QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ fun (i : Fin (Module.finrank ℝ M)) => ↑(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.

    source
    theorem QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared {M : Type u_2} [AddCommGroup M] [Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M) :
    ∃ (w : Fin (Module.finrank ℝ M) → ℝ), (∀ (i : Fin (Module.finrank ℝ M)), w i = -1 ∨ w i = 0 ∨ w i = 1) ∧ QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ 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.