Siegel's lemma in the sup norm, after Bombieri and Vaaler

A nonzero subspace V of ℚ^ι of dimension k contains a nonzero integral vector z with ‖z‖ ≤ H(V) ^ (1 / k), 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 > p unknowns, this is Bombieri and Vaaler's sup-norm form of Siegel's lemma: there is a nonzero integral solution with ‖x‖ ≤ (√det (A Aᵀ) / g) ^ (1 / (n - p)), where g is the greatest common divisor of the maximal minors of A. The classical bound of Siegel, in Mathlib as Int.Matrix.exists_ne_zero_int_vec_norm_le, is ‖x‖ ≤ (n · max 1 (max |A i j|)) ^ (p / (n - p)). By Hadamard's inequality, √det (A Aᵀ) is at most the product of the Euclidean norms of the rows of A, so the bound here is at most (√n · max |A i j|) ^ (p / (n - p)); and unlike the classical bound, it depends on A only through its rational row space, since it is the height of the solution space.

The independent primitive vectors of Submodule.exists_linearIndependent_intPoints_prod_norm_le have product of sup norms at most H(V). At least one has norm at most the kth root of that bound. Thus this theorem is the smallest-vector corollary of the existing product theorem and uses the same cube-slicing and Minkowski second-theorem implementation.

Main results

• Submodule.exists_ne_zero_mem_intPoints_norm_le: a nonzero integral point of V of sup norm at most H(V) ^ (1 / k).
• Matrix.exists_ne_zero_mulVec_eq_zero_norm_le: Bombieri and Vaaler's Theorem 1 over ℤ.

References

• E. Bombieri and J. Vaaler, On Siegel's lemma, Invent. Math. 73 (1983), 11–32, Theorem 1.
• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), §2.9.

theorem Submodule.exists_ne_zero_mem_intPoints_norm_le {ι : Type u_1} [Fintype ι] [LinearOrder ι] {V : Submodule ℚ (ι → ℚ)} (hV : V ≠ ⊥) : ∃ z ∈ V.intPoints, z ≠ 0 ∧ ‖z‖ ≤ V.subspaceHeight ^ (↑(Module.finrank ℚ ↥V))⁻¹

Siegel's lemma for a rational subspace, in the sup norm. A nonzero subspace V of ℚ^ι contains a nonzero integral point z whose sup norm is at most H(V) ^ (1 / k), where H(V) is the absolute Euclidean height of V and k its dimension.

theorem Matrix.exists_ne_zero_mulVec_eq_zero_norm_le {ι : Type u_1} [Fintype ι] {p : ℕ} {A : Matrix (Fin p) ι ℤ} (hA : LinearIndependent ℚ (A.map Int.cast).row) (hp : p < Fintype.card ι) : ∃ (x : ι → ℤ), x ≠ 0 ∧ A.mulVec x = 0 ∧ ‖x‖ ≤ (√↑(A * A.transpose).det / ↑A.minorGcd) ^ (↑(Fintype.card ι) - ↑p)⁻¹

Bombieri and Vaaler's Siegel lemma over ℤ, in the sup norm. Let A be a p × n integer matrix with linearly independent rows and p < n, and let g be the greatest common divisor of its maximal minors. Then A x = 0 has a nonzero integral solution x with ‖x‖ ≤ (√det (A Aᵀ) / g) ^ (1 / (n - p)), where ‖x‖ = max_i |x i|.