Quadratic forms over the complex numbers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
equivalent_sum_squares: A nondegenerate quadratic form over the complex numbers is equivalent to
a sum of squares.
noncomputable
def
quadratic_form.isometry_sum_squares
{ι : Type u_1}
[fintype ι]
[decidable_eq ι]
(w' : ι → ℂ) :
(quadratic_form.weighted_sum_squares ℂ w').isometry (quadratic_form.weighted_sum_squares ℂ (λ (i : ι), ite (w' i = 0) 0 1))
The isometry between a weighted sum of squares on the complex numbers and the
sum of squares, i.e. weighted_sum_squares with weights 1 or 0.
Equations
- quadratic_form.isometry_sum_squares w' = let w : ι → ℂˣ := λ (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)))
noncomputable
def
quadratic_form.isometry_sum_squares_units
{ι : Type u_1}
[fintype ι]
[decidable_eq ι]
(w : ι → ℂˣ) :
The isometry between a weighted sum of squares on the complex numbers and the
sum of squares, i.e. weighted_sum_squares with weight λ i : ι, 1.
Equations
theorem
quadratic_form.equivalent_sum_squares
{M : Type u_1}
[add_comm_group M]
[module ℂ M]
[finite_dimensional ℂ M]
(Q : quadratic_form ℂ M)
(hQ : (⇑quadratic_form.associated Q).nondegenerate) :
A nondegenerate quadratic form on the complex numbers is equivalent to
the sum of squares, i.e. weighted_sum_squares with weight λ i : ι, 1.
theorem
quadratic_form.complex_equivalent
{M : Type u_1}
[add_comm_group M]
[module ℂ M]
[finite_dimensional ℂ M]
(Q₁ Q₂ : quadratic_form ℂ M)
(hQ₁ : (⇑quadratic_form.associated Q₁).nondegenerate)
(hQ₂ : (⇑quadratic_form.associated Q₂).nondegenerate) :
Q₁.equivalent Q₂
All nondegenerate quadratic forms on the complex numbers are equivalent.