Integral solutions and kernel bases of bounded sup norm

A subspace V of ℚ^ι of dimension k contains k linearly independent integral points z 0, …, z (k - 1), each primitive (the gcd of its coordinates is 1), with

‖z 0‖ ⋯ ‖z (k - 1)‖ ≤ H(V),

where ‖z‖ = max_i |z i| is the sup norm and H(V) is the absolute Euclidean height Submodule.subspaceHeight V. For the space of solutions of a system A x = 0 of p independent linear equations with integer coefficients in n unknowns, this is the sup-norm form of Bombieri and Vaaler's Theorem 2: there are n - p linearly independent primitive integral solutions x l with

‖x 0‖ ⋯ ‖x (n - p - 1)‖ ≤ √det (A Aᵀ) / g,

where g is the greatest common divisor of the maximal minors of A. The bound depends on A only through its rational row space. The solutions need not form a ℤ-basis of the lattice of all integral solutions: for A = (0 0 1), the solutions (1, 1, 0) and (1, -1, 0) meet the bound 1 and span a sublattice of index 2.

The lattice of integral points of V has covolume H(V) in the real span of V (Submodule.covolume_intLattice), so the statement is the case of integral lattices of ZLattice.exists_linearIndependent_prod_norm_ofLp_le_covolume, which combines Minkowski's second theorem with Vaaler's cube-slicing theorem.

The integral points of V also have a ℤ-basis whose product of sup norms is at most k! / 2 ^ (k - 1) * H(V). This combines Cassels' basis from the successive minima (Submodule.exists_basis_intPoints_prod_norm_le_prod_successiveMin) with the cube-slice bound (Submodule.prod_successiveMin_intLattice_le_subspaceHeight). For the kernel of A, the arithmetic constant comes from Matrix.covolume_intLattice_ker_mulVecLin. The resulting basis generates the entire integral kernel. The bound includes k = 0, when both sides are one.

Main results

• Submodule.exists_linearIndependent_intPoints_prod_norm_le: independent primitive integral points of V whose sup norms have product at most H(V).
• Matrix.exists_linearIndependent_mulVec_eq_zero_prod_norm_le: Bombieri and Vaaler's Theorem 2 over ℤ, in the sup norm.
• Submodule.exists_basis_intPoints_prod_norm_le_subspaceHeight: a ℤ-basis of the integral points of V whose sup norms have product at most k! / 2 ^ (k - 1) * H(V).
• Matrix.exists_basis_ker_mulVecLin_prod_norm_le: a basis of the entire integral kernel with product bound k! / 2 ^ (k - 1) * √det (A Aᵀ) / g.

References

• J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer, 1959, Chapter V, Lemma 8.
• I. Aliev and M. Henk, Minkowski's successive minima in convex and discrete geometry, Commun. Math. 31 (2023), 35–59, §6.
• E. Bombieri and J. Vaaler, On Siegel's lemma, Invent. Math. 73 (1983), 11–32, Theorem 2.
• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), §2.9.

theorem Submodule.exists_linearIndependent_intPoints_prod_norm_le {ι : Type u_1} [Fintype ι] [LinearOrder ι] (V : Submodule ℚ (ι → ℚ)) : ∃ (z : Fin (Module.finrank ℚ ↥V) → ι → ℤ), LinearIndependent ℤ z ∧ (∀ (l : Fin (Module.finrank ℚ ↥V)), z l ∈ V.intPoints) ∧ (∀ (l : Fin (Module.finrank ℚ ↥V)), Finset.univ.gcd (z l) = 1) ∧ ∏ l : Fin (Module.finrank ℚ ↥V), ‖z l‖ ≤ V.subspaceHeight

Independent integral points of small sup norm (Bombieri–Vaaler). A subspace V of ℚ^ι of dimension k contains k linearly independent integral points z l, each with coprime coordinates, the product of whose sup norms is at most the absolute Euclidean height of V.

theorem Submodule.exists_basis_intPoints_prod_norm_le_subspaceHeight {ι : Type u_1} [Fintype ι] [LinearOrder ι] (V : Submodule ℚ (ι → ℚ)) : ∃ (b : Module.Basis (Fin (Module.finrank ℚ ↥V)) ℤ ↥V.intPoints), ∏ l : Fin (Module.finrank ℚ ↥V), ‖↑(b l)‖ ≤ ↑(Module.finrank ℚ ↥V).factorial / 2 ^ (Module.finrank ℚ ↥V - 1) * V.subspaceHeight

A basis of the integral points of small sup norm. For a subspace V of ℚ^ι of dimension k, the integral points V ∩ ℤ^ι have a ℤ-basis b with ∏ l, ‖b l‖ ≤ k! / 2 ^ (k - 1) * H(V), where ‖b l‖ = max_i |b l i| is the sup norm and H(V) is the absolute Euclidean height of V. Unlike the independent points of Submodule.exists_linearIndependent_intPoints_prod_norm_le, these vectors span the whole of V ∩ ℤ^ι, not only a sublattice of finite index.

theorem Matrix.exists_linearIndependent_mulVec_eq_zero_prod_norm_le {ι : Type u_1} [Fintype ι] {p : ℕ} {A : Matrix (Fin p) ι ℤ} (hA : LinearIndependent ℚ (A.map Int.cast).row) : ∃ (x : Fin (Fintype.card ι - p) → ι → ℤ), LinearIndependent ℤ x ∧ (∀ (l : Fin (Fintype.card ι - p)), A.mulVec (x l) = 0) ∧ (∀ (l : Fin (Fintype.card ι - p)), Finset.univ.gcd (x l) = 1) ∧ ∏ l : Fin (Fintype.card ι - p), ‖x l‖ ≤ √↑(A * A.transpose).det / ↑A.minorGcd

Bombieri and Vaaler's Theorem 2 over ℤ, in the sup norm. Let A be a p × n integer matrix with linearly independent rows, and let g be the greatest common divisor of its maximal minors. Then A x = 0 has n - p linearly independent integral solutions x l, each with coprime coordinates, whose sup norms ‖x l‖ = max_i |x l i| satisfy ∏ l, ‖x l‖ ≤ √det (A Aᵀ) / g.

theorem Matrix.exists_basis_ker_mulVecLin_prod_norm_le {ι : Type u_1} [Fintype ι] {p : ℕ} {A : Matrix (Fin p) ι ℤ} (hA : LinearIndependent ℚ (A.map Int.cast).row) : ∃ (b : Module.Basis (Fin (Fintype.card ι - p)) ℤ ↥A.mulVecLin.ker), ∏ l : Fin (Fintype.card ι - p), ‖↑(b l)‖ ≤ ↑(Fintype.card ι - p).factorial / 2 ^ (Fintype.card ι - p - 1) * √↑(A * A.transpose).det / ↑A.minorGcd

An integer matrix with independent rows has a basis of its entire integral kernel whose product of sup norms is at most k! / 2 ^ (k - 1) * √det (A Aᵀ) / minorGcd A, where k is the number of columns minus the number of rows. The conclusion also includes k = 0.