Vectors of bounded value for a positive definite integral quadratic form

A positive definite quadratic form on a finitely generated free ℤ-module takes each of its values only finitely often: the sets {x | q x ≤ n} and {x | q x = n} are finite. This is the finiteness that makes "the vectors of norm n" of a positive definite lattice a finite list, and the one that turns an orbit lying in a level set into a periodic orbit.

Main results

• QuadraticMap.PosDef.finite_setOf_apply_le: a positive definite quadratic form on a finitely generated free ℤ-module has only finitely many vectors of value at most n.
• QuadraticMap.PosDef.finite_setOf_apply_eq: consequently only finitely many vectors of value exactly n.

These results live in the root QuadraticMap.PosDef namespace so that they are available by dot notation on a QuadraticForm.PosDef hypothesis.

Implementation notes

The argument stays inside ℤ; no rational or real coefficients, no compactness, and no diagonalization enter. Write B for the polar form, which is symmetric with B x x = 2 * q x, hence nonnegative, and let b be a basis. The coordinates of x in the dual-like map T x = fun i ↦ B x (b i) are bounded by Cauchy-Schwarz for a positive semidefinite symmetric form (LinearMap.BilinForm.apply_sq_le_of_symm), since (B x (b i)) ^ 2 ≤ B x x * B (b i) (b i) and the right-hand side is bounded once q x is. The map T is injective: a vector it kills is orthogonal to a basis, hence to itself, hence isotropic, hence zero. So the set in question is the preimage under an injective map of a box of integer vectors.

Note that T is not claimed to be surjective, and need not be: the polar form of a positive definite integral quadratic form is generally not unimodular. Injectivity is all the argument uses.

theorem QuadraticMap.PosDef.finite_setOf_apply_le {M : Type u_1} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] {q : QuadraticForm ℤ M} (hq : PosDef q) (n : ℤ) : {x : M | q x ≤ n}.Finite

A positive definite integral quadratic form has finitely many vectors of bounded value. For a positive definite quadratic form q on a finitely generated free ℤ-module and any integer n, only finitely many vectors satisfy q x ≤ n.

theorem QuadraticMap.PosDef.finite_setOf_apply_eq {M : Type u_1} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] {q : QuadraticForm ℤ M} (hq : PosDef q) (n : ℤ) : {x : M | q x = n}.Finite

A positive definite integral quadratic form takes each value finitely often. For a positive definite quadratic form q on a finitely generated free ℤ-module, only finitely many vectors satisfy q x = n; for a positive definite lattice this is the finiteness of the set of vectors of a given norm.