WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Quadratic form

Revision #1509 → #2184 · back to history

modifiedQuadratic form4b80324cdb84
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—Mathlib defines `QuadraticForm R M := QuadraticMap R M R`, which generalizes the polynomial definition to any commutative semiring and module.
status—formalized
modifiedDefinite vs isotropic (real)32f213363fc8
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.Anisotropic
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`QuadraticMap.Anisotropic Q := ∀ x, Q x = 0 → x = 0` is exactly the property described (an anisotropic / 'definite-in-this-sense' form).
status—formalized
modifiedUnary, binary, ternary forms38a8fe43fa74
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This is purely terminological vocabulary about the number of variables and has no dedicated Mathlib declaration.
status—not_formalized
modifiedQuadric from a quadratic forme1a673f15ea3
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `Quadric` type or projective vanishing-locus construction tied to quadratic forms is present in Mathlib.
status—not_formalized
modifiedSquare of Euclidean norma5d3ea93aaa4
FieldFrom #1509To #2184
mathlib.decl—EuclideanSpace.norm_eq
mathlib.match_kind——
mathlib.module—Mathlib.Analysis.InnerProductSpace.PiL2
note—The squared Euclidean norm is computable via `EuclideanSpace.norm_eq` (norm = sqrt of sum of squared coordinates), but it is not explicitly identified as a `QuadraticForm` instance.
status—partial
modifiedQuadratic space (preview)876650a46782
FieldFrom #1509To #2184
mathlib.decl—QuadraticModuleCat
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
note—`QuadraticModuleCat` bundles a module with a `QuadraticForm`; Mathlib treats 'quadratic space' as the pair (M, Q : QuadraticForm R M) rather than a stand-alone abbrev.
status—partial
modifiedFermat's theorem on sums of two squares465858f50db0
FieldFrom #1509To #2184
mathlib.decl—Nat.Prime.sq_add_sq
mathlib.match_kind—exact
mathlib.module—Mathlib.NumberTheory.SumTwoSquares
note—`Nat.Prime.sq_add_sq` gives the prime case (`p % 4 ≠ 3 ⇒ ∃ a b, p = a^2 + b^2`); `Nat.eq_sq_add_sq_iff` extends to all integers.
status—formalized
addedPell's equation3b446ef303fd
modifiedQuadratic form from a matrix13e9b3b28fd9
FieldFrom #1509To #2184
mathlib.decl—Matrix.toQuadraticForm'
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`Matrix.toQuadraticForm' M : QuadraticForm R (n → R)` sends `x ↦ row x * M * col x`, exactly the matrix-defined quadratic form.
status—formalized
modifiedThree-variable matrix formd03751ea3a8b
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This is a worked example in three variables and is not formalized as a distinct theorem.
status—not_formalized
modifiedSame form iff matching diagonal and symmetric sums873d74e8531d
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No declaration explicitly characterizes equality of `Matrix.toQuadraticForm'` in terms of diagonal entries and symmetric off-diagonal sums.
status—not_formalized
modifiedUnique symmetric matrix for a quadratic forma2b95ea87237
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm.toMatrix'
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`QuadraticForm.toMatrix'` gives the symmetric matrix (with `isSymm_toMatrix'`) recovering Q via `associated`, but uniqueness as a stand-alone statement is not isolated.
status—partial
modifiedBijection between quadratic forms and symmetric matrices7312d0a1643f
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.associated_left_inverse
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`associated_left_inverse` and `toQuadraticMap_associated` together establish the bijection between quadratic forms and symmetric bilinear forms (assuming `Invertible (2 : R)`), not stated as a single equiv with matrices.
status—partial
modifiedJacobi's orthogonal diagonalization047f307ffd85
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm.equivalent_weightedSumSquares
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
note—`QuadraticForm.equivalent_weightedSumSquares` shows every quadratic form over a field with `Invertible (2:K)` is equivalent to a weighted sum of squares, which generalizes Jacobi's orthogonal diagonalization.
status—formalized
modifiedSylvester's law of inertiad26712d7ef71
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm.sigPos_of_equiv_weightedSumSquares
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Signature
note—`sigPos_of_equiv_weightedSumSquares` + `sigNeg_of_equiv_weightedSumSquares` (uniqueness) together with `equivalent_one_zero_neg_one_weighted_sum_squared` (existence) state Sylvester's law of inertia.
status—formalized
modifiedSignature of a quadratic form738105bd352b
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm.sigPos
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Signature
note—`sigPos` and `sigNeg` define the positive/negative parts of the signature; there is no bundled triple `(n₊, n₋, n₀)` invariant declaration.
status—partial
modifiedPositive/negative definite, nondegenerate, isotropic3aea9a568981
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.PosDef
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`QuadraticMap.PosDef`, `QuadraticMap.Anisotropic`, and `QuadraticMap.Nondegenerate` exist; negative-definite is expressed as `PosDef (-Q)` rather than as a distinct definition.
status—partial
modifiedDiscriminant of a quadratic form3b6219e5d22b
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm.discr
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`QuadraticForm.discr b Q := (Q.toMatrix b).det` is the discriminant defined as the determinant of the matrix representation in a basis.
status—formalized
modifiedChange of basis for matrix of a quadratic formcbe6f82ef8e0
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm.toMatrix_comp
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`toMatrix_comp` (and `toMatrix'_comp`) shows the matrix of Q ∘ f equals fᵀ * (Q.toMatrix) * f, the standard change-of-basis transformation.
status—formalized
modifiedJacobi's theorem (orthogonal diagonalization of symmetric matrix)792de675dac8
FieldFrom #1509To #2184
mathlib.decl—LinearMap.BilinForm.exists_orthogonal_basis
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`exists_orthogonal_basis` produces an orthogonal basis for any symmetric bilinear form over a field with `Invertible 2`, generalizing diagonalization of symmetric matrices.
status—formalized
modifiedPositive/negative indices of inertia5937e44a7b8e
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm.sigPos
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Signature
note—`sigPos` and `sigNeg` are the positive and negative indices of inertia, defined as the maximal finrank of a positive- (resp. negative-)definite subspace.
status—formalized
modifiedPositive definite, negative definite, isotropic (via values)254cdc7cf9d9
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.PosDef
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`QuadraticMap.PosDef Q := ∀ x, x ≠ 0 → 0 < Q x` exactly captures positive-definiteness via values; negative-definite is `PosDef (-Q)`.
status—formalized
modifiedUniqueness of positive definite real form up to isometry469954ada9cc
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm.equivalent_one_neg_one_weighted_sum_squared
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Real
note—`equivalent_one_neg_one_weighted_sum_squared` shows nondegenerate real forms are equivalent to a ±1-weighted sum of squares; the pure positive-definite-→-sum-of-squares specialization is not isolated.
status—partial
modifiedQuadratic form over a field (coordinate-free)80e66a9f7652
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`QuadraticForm R M` is the coordinate-free map `M → R` definition (over any commutative semiring), encompassing the field case.
status—formalized
modifiedn-ary quadratic form (polynomial)f6e046a8b9e3
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib's `QuadraticForm`/`QuadraticMap` is map-based; it is not defined as `MvPolynomial.IsHomogeneous n=2`, and no equivalence between the polynomial and map definitions is registered.
status—not_formalized
modifiedNull vector2e709b164c65
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.Anisotropic
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—The predicate `Q v = 0` appears via `Anisotropic` ('no nonzero null vector') but there is no standalone `IsNullVector`-style definition.
status—partial
modifiedEquivalent quadratic formsf1f8fa1c0e35
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.Equivalent
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
note—`QuadraticMap.Equivalent Q₁ Q₂ := Nonempty (Q₁.IsometryEquiv Q₂)` is the existence of a linear equivalence intertwining the two forms.
status—formalized
modifiedSymmetrization of coefficient matrixc7d38202df54
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm.isSymm_toMatrix'
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`Matrix.toQuadraticForm'` plus `isSymm_toMatrix'` express that one can pass to a symmetric representing matrix; the explicit `(A+Aᵀ)/2` formula is not packaged as a lemma.
status—partial
modifiedAssociated bilinear formfe6b031957d2
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.associated
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`QuadraticMap.associated` (via `associatedHom`) sends Q to the symmetric bilinear form `B(x,y) = (1/2)(Q(x+y) − Q(x) − Q(y))` when 2 is invertible.
status—formalized
modifiedEquivalence of symmetric bilinear forms and quadratic forms826a6f719c0b
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.associated_left_inverse
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`associated_left_inverse` and `toQuadraticMap_associated` give the two-sided inverse between symmetric bilinear maps and quadratic maps when 2 is invertible.
status—formalized
modifiedQuadratic form on a vector space601ac2923c93
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—The `QuadraticMap` (and abbreviated `QuadraticForm`) structure axiomatizes precisely `Q(a • x) = a² • Q x` together with a companion bilinear map.
status—formalized
modifiedQuadratic space7a381caa7179
FieldFrom #1509To #2184
mathlib.decl—QuadraticModuleCat
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
note—`QuadraticModuleCat` bundles a module with a quadratic form, the closest thing to a 'quadratic space' object; no standalone abbreviation requiring finite-dimensionality exists.
status—partial
modifiedQ is homogeneous of degree 2339b7bf6c6b2
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.map_smul
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`QuadraticMap.map_smul : Q (a • x) = (a * a) • Q x` is the homogeneity-of-degree-2 axiom built into the structure.
status—formalized
modifiedPolar bilinear form (char ≠ 2)4b970aee54bc
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.associated
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`QuadraticMap.associated`, which requires `Invertible (2 : R)`, is exactly the polar bilinear form `B(x,y) = (1/2)(Q(x+y) − Q(x) − Q(y))`.
status—formalized
modifiedCharacteristic 2 polar form is alternating86f07b79de97
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.polar_self
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`polar_self : polar Q x x = 2 • Q x` becomes 0 in characteristic 2, implying the alternating property; the char-2 specialization itself is not stated as a separate lemma.
status—partial
addedExistence of (non-symmetric) bilinear B″ with B″(x,x)=Q(x) in char 28d46bb752b1b
modifiedIsometric quadratic spaces6033eb14760b
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.IsometryEquiv
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
note—`QuadraticMap.IsometryEquiv Q₁ Q₂` is a linear equivalence with `Q₂ (f m) = Q₁ m`, exactly the notion of isometric quadratic spaces.
status—formalized
modifiedIsometry classes correspond to equivalence classesb820ec721d9b
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.Equivalent
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
note—`Equivalent` is defined as `Nonempty (Q₁.IsometryEquiv Q₂)`, so isometry classes and equivalence classes literally coincide by definition.
status—formalized
modifiedAssociated quadratic form and polar form (over a ring)e123d4d72803
FieldFrom #1509To #2184
mathlib.decl—LinearMap.BilinMap.toQuadraticMap
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`BilinMap.toQuadraticMap B := fun x ↦ B x x` is the associated quadratic map of a bilinear form, paired with `QuadraticMap.polarBilin` in the other direction.
status—formalized
modifiedEquivalent characterizations of quadratic form over a ring4da6a581e9fc
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—Mathlib's `QuadraticMap` adopts the `map_smul + exists_companion` characterization; equivalences with other ring-level characterizations of quadratic forms are not all packaged into lemmas.
status—partial
modifiedOrthogonal vectors and kerneld4b2a8ca35d4
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.IsOrtho
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`QuadraticMap.IsOrtho Q x y := Q (x + y) = Q x + Q y` defines orthogonality with respect to Q; the radical/kernel notion is `QuadraticMap.radical`.
status—formalized
modifiedNon-singular, isotropic, definite, totally singularf2c06dd1aa59
FieldFrom #1509To #2184
mathlib.decl—QuadraticMap.Nondegenerate
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Radical
note—`Nondegenerate`, `Anisotropic`, and `PosDef` cover non-singular/isotropic/definite, but 'totally singular' (Q vanishing on a subspace) is not given a dedicated definition.
status—partial
modifiedOrthogonal group of a quadratic form078d7b0fc38c
FieldFrom #1509To #2184
mathlib.decl—Matrix.orthogonalGroup
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.UnitaryGroup
note—Mathlib has `Matrix.orthogonalGroup` for the standard quadratic form on `n → R`, but no general group `O(Q)` of isometries `QuadraticMap.IsometryEquiv Q Q` is bundled.
status—partial
modifiedComposition algebra461f8e6f4ef2
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `CompositionAlgebra` definition (algebra with a multiplicative quadratic form) is present in Mathlib.
status—not_formalized
modifiedDiagonalization of quadratic forms (char ≠ 2)a016868b9dc6
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm.equivalent_weightedSumSquares
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
note—`equivalent_weightedSumSquares` exhibits every QuadraticForm over a field with `Invertible 2` as equivalent to a weighted sum of squares (a diagonal form).
status—formalized
modifiedGeometric nature via eigenvalues (ellipsoid/hyperboloid)0724aebe0e78
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not classify level sets of quadratic forms as ellipsoids or hyperboloids based on eigenvalue signs.
status—not_formalized
modifiedGeometric nature with zero eigenvalues (paraboloid)bd4edeb4ca52
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—There is no Mathlib classification of degenerate quadratic level sets as paraboloids or cylinders.
status—not_formalized
modifiedIntegral quadratic formae0154ba2baa
FieldFrom #1509To #2184
mathlib.decl—QuadraticForm
mathlib.match_kind——
mathlib.module—Mathlib.LinearAlgebra.QuadraticForm.Basic
note—`QuadraticForm ℤ M` is well-typed (since `QuadraticMap` works over any `CommSemiring`), but no dedicated `IntegralQuadraticForm` abbrev or theory is registered.
status—partial
modifiedIntegral with respect to a lattice307a94f38fd8
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No definition of a real quadratic form being integral with respect to a lattice (taking integer values on lattice points) is present in Mathlib.
status—not_formalized
modifiedUniversal integral quadratic form470c2c6afa56
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No notion of 'universal' integral quadratic form (image = all positive integers) appears in Mathlib.
status—not_formalized
modifiedLagrange's four-square theorem0f5aae04cd24
FieldFrom #1509To #2184
mathlib.decl—Nat.sum_four_squares
mathlib.match_kind—exact
mathlib.module—Mathlib.NumberTheory.SumFourSquares
note—`Nat.sum_four_squares : ∀ n, ∃ a b c d, a^2 + b^2 + c^2 + d^2 = n` is Lagrange's four-square theorem.
status—formalized
modifiedRamanujan's 54 quaternary formsc61ea2df4ce4
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Ramanujan's classification of 54 universal diagonal quaternary forms is not present in Mathlib.
status—not_formalized
modified{1,2,5,5} missing 15bf9050cb4a00
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—This specific counterexample about the form {1,2,5,5} not representing 15 is not formalized in Mathlib.
status—not_formalized
modified15 and 290 theorems6e72008737e2
FieldFrom #1509To #2184
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Conway–Schneeberger 15 theorem and the Bhargava–Hanke 290 theorem are not present in Mathlib.
status—not_formalized