Bombieri–Vaaler's theorem over ℤ

For an M × N integer matrix A whose rows are linearly independent, the integral solutions of A x = 0 contain N - M linearly independent vectors x₁, …, x_{N-M} with

∏ l, max n, |x l n|  ≤  D⁻¹ √(det (A Aᵀ)),

D the greatest common divisor of the maximal minors of A, and in particular a nonzero integral solution with max n, |x n| ≤ (D⁻¹ √(det (A Aᵀ)))^{1/(N-M)}. These are Theorems 2 and 1 of Bombieri–Vaaler 1983, and the right-hand side is an absolute height on the Grassmannian, so — unlike the bound of Layer 5.1 — it does not move under A ↦ U A for U ∈ GL_M(ℤ).

The proof is the assembly the roadmap prices it at: the covolume identity of Layer 4.3 over ℚ identifies the covolume of the solution lattice with the Arakelov height of the solution space, Layer 3.5 identifies that with the Arakelov height of the row space and Layer 3.4 computes the latter as D⁻¹ √(det (A Aᵀ)), while Minkowski's second theorem (Layer 4.2) against the central slice of the unit cube, whose volume Layer 4.5 bounds below by 2^{N-M}, bounds the product of the successive minima by that covolume. Layer 4.1 then supplies vectors realizing the minima.

Main definitions

• Submodule.cubeSlice: the central slice {y ∈ V | ∀ i, |y i| ≤ 1} of the unit cube of EuclideanSpace ℝ ι by a subspace V. This is the convex body Minkowski's second theorem is applied to, and the body Layer 4.5 measures.
• Int.Matrix.minorGcd: the greatest common divisor of the maximal minors of an integer matrix, the D of Bombieri–Vaaler. The minors are Layer 3.1's Plücker coordinates of the rows.

Main results

• Int.Matrix.exists_linearIndependent_mulVec_eq_zero_prod_iSup_abs_le: Bombieri–Vaaler's Theorem 2, a small basis of the integral solutions.
• Int.Matrix.exists_linearIndependent_mulVec_eq_zero_prod_mulHeight_le: the same, with the multiplicative height of Layer 1 on the left — the K = ℚ case of the statement Layer 5.4 makes over a number field.
• Int.Matrix.exists_ne_zero_mulVec_eq_zero_iSup_abs_le_det_rpow: Bombieri–Vaaler's Theorem 1, a single small nonzero integral solution.
• Int.Matrix.sqrt_det_div_minorGcd_unit_mul: the invariance of the bound under A ↦ U A for U ∈ GL_M(ℤ), which is what Theorem 1 has over Layer 5.1's Siegel lemma.
• Int.Matrix.minorGcd_mul_arakelovMulHeight_ker: the identity the bound is, D · H_Ar(ker A) = √(det (A Aᵀ)).
• ZLattice.prod_successiveMinimum_cubeSlice_le_covolume: Minkowski's second theorem against the cube slice, with the factor 2^n cancelled by Vaaler's bound. This is the geometric half of the theorem, and it knows no arithmetic.
• NumberField.gcd_mul_arakelovMulHeight_intCast: the Arakelov analogue of Layer 5.1's Rat.gcd_mul_mulHeight_intCast, the translation the arithmetic half is read through.
• Int.Matrix.linearIndependent_row_map_rat_iff, Int.Matrix.det_pos, Int.Matrix.one_le_minorGcd: the hypothesis and the two positivity facts that make the bound meaningful.

Implementation notes

⚠ The absolute value in Bombieri–Vaaler's √|det (A Aᵀ)| is redundant. The Gram determinant of the rows is a sum of squares of minors — this is Layer 3.4's Matrix.det_mul_transpose_self_nonneg — and under the rank hypothesis it is positive, Int.Matrix.det_pos. The statements here carry no absolute value, and the hypothesis is stated as Int.Matrix.linearIndependent_row_map_rat_iff makes available: linear independence of the rows over ℚ is exactly (A * Aᵀ).det ≠ 0, a condition on the integer matrix alone.

⚠ The milestone needs Layer 3.5, which its pricing does not mention. The roadmap prices 5.2 at "3.4, 4.2, 4.5 and the ℚ-case of 4.3", and Layer 4.3 delivers the covolume of the solution lattice as the Arakelov height of the solution space. Turning that into the minors of A is the duality theorem Matrix.arakelovMulHeight_ker_mulVecLin of Layer 3.5, and nothing else will do: the Plücker coordinates of the kernel are the complementary minors, which is what duality says. So the ℚ spine is 3.1 → 3.2 → 3.3 → 3.4, 3.5 → 4.1 → 4.2 → 4.3(ℚ) → 4.5 → 5.2, one rung longer than advertised, and every rung of it is landed.

⚠ The 2^n of Minkowski's second theorem and the 2^n of Vaaler's cube-slicing theorem cancel exactly, and that is the whole of why the constant is 1. Layer 4.2 bounds (∏ λ i) · vol B by 2^n · covol L, and Layer 4.5 bounds vol B below by 2^n for B the cube slice; the product of the minima is therefore at most the covolume, with no constant at all. Any body with a worse slice bound would leave a constant behind, which is precisely what happens over a number field with a complex place — Layer 5.4's (2/π)^{k r₂ / d}.

⚠ The basis form needs no hypothesis M < N. Int.Matrix.exists_linearIndependent_mulVec_eq_zero_prod_iSup_abs_le is stated for Fin (N - M) solutions and is sharp at N = M, where both sides are 1: the empty product on the left, and on the right the Arakelov height of the zero subspace. Only the one-vector form needs M < N, and there it is not removable — the exponent 1/(N - M) requires it.

⚠ The proof passes from sup norms to heights pointwise. By Layer 5.1's Rat.gcd_mul_mulHeight_intCast the height of a nonzero integer tuple is its sup norm divided by its content. Applying the resulting height-at-most-sup-norm inequality to each solution gives Int.Matrix.exists_linearIndependent_mulVec_eq_zero_prod_mulHeight_le, the height form that Layer 5.4 generalizes.

References

E. Bombieri and J. Vaaler, "On Siegel's lemma", Inventiones Mathematicae 73 (1983), 11–32, Theorems 1 and 2, and equation (2.5) for the invariance.

I. Aliev and M. Henk, "Minkowski's successive minima in convex and discrete geometry", Communications in Mathematics 31(2) (2023), 35–59, §6, Theorems 6.2–6.3 (arXiv:2304.00120; doi:10.46298/cm.11155). This section gives an adele-free proof using the rational covolume identity stated before Theorem 6.3.

E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Theorem 2.9.4 and Remark 2.9.5 for the number-field statement this is the K = ℚ case of.

This is Layer 5.2 of the ArithmeticHeights roadmap.

The central slice of the unit cube

The convex body Minkowski's second theorem is applied to. Everything in this section is elementary; the one statement with content about it is Layer 4.5's two_pow_finrank_le_volume_inter_cube, which bounds its volume below by 2 ^ dim V.

def Submodule.cubeSlice {ι : Type u_1} (V : Submodule ℝ (EuclideanSpace ℝ ι)) : Set ↥V

The central slice of the unit cube [-1, 1]^ι by a subspace V of EuclideanSpace ℝ ι, as a subset of V.

Equations

• V.cubeSlice = {y : ↥V | ∀ (i : ι), |(↑y).ofLp i| ≤ 1}

theorem Submodule.mem_cubeSlice {ι : Type u_1} (V : Submodule ℝ (EuclideanSpace ℝ ι)) {y : ↥V} : y ∈ V.cubeSlice ↔ ∀ (i : ι), |(↑y).ofLp i| ≤ 1

theorem Submodule.mem_smul_cubeSlice {ι : Type u_1} (V : Submodule ℝ (EuclideanSpace ℝ ι)) {r : ℝ} (hr : 0 < r) {y : ↥V} : y ∈ r • V.cubeSlice ↔ ∀ (i : ι), |(↑y).ofLp i| ≤ r

A dilation of the cube slice is the slice of the corresponding cube, which is how a bound by a successive minimum is read off.

theorem Submodule.convex_cubeSlice {ι : Type u_1} (V : Submodule ℝ (EuclideanSpace ℝ ι)) : Convex ℝ V.cubeSlice

theorem Submodule.neg_mem_cubeSlice {ι : Type u_1} (V : Submodule ℝ (EuclideanSpace ℝ ι)) {x : ↥V} (hx : x ∈ V.cubeSlice) : -x ∈ V.cubeSlice

theorem Submodule.isClosed_cubeSlice {ι : Type u_1} (V : Submodule ℝ (EuclideanSpace ℝ ι)) : IsClosed V.cubeSlice

theorem Submodule.isBounded_cubeSlice {ι : Type u_1} (V : Submodule ℝ (EuclideanSpace ℝ ι)) [Finite ι] : Bornology.IsBounded V.cubeSlice

theorem Submodule.interior_cubeSlice_nonempty {ι : Type u_1} (V : Submodule ℝ (EuclideanSpace ℝ ι)) [Finite ι] : (interior V.cubeSlice).Nonempty

Minkowski's second theorem against the cube slice

Layers 4.2 and 4.5, combined: the two factors 2 ^ n cancel and the product of the successive minima is bounded by the covolume with no constant.

theorem ZLattice.prod_successiveMinimum_cubeSlice_le_covolume {ι : Type u_1} [Fintype ι] (V : Submodule ℝ (EuclideanSpace ℝ ι)) (L : Submodule ℤ ↥V) [DiscreteTopology ↥L] [IsZLattice ℝ L] : ∏ i ∈ Finset.range (Module.finrank ℝ ↥V), successiveMinimum L V.cubeSlice i ≤ covolume L MeasureTheory.volume

The geometric half of Bombieri–Vaaler's theorem. For the central slice of the unit cube as the convex body, the product of the successive minima of a lattice in a subspace of EuclideanSpace ℝ ι is at most the covolume of the lattice. The 2 ^ n of Minkowski's second theorem (Layer 4.2) is cancelled exactly by Vaaler's slice bound (Layer 4.5).

The Arakelov height of an integer tuple

The Arakelov analogue of Layer 5.1's Rat.gcd_mul_mulHeight_intCast, which is what turns the Plücker point of the row space into a euclidean norm of minors.

theorem NumberField.gcd_mul_arakelovMulHeight_intCast {κ : Type u_1} [Fintype κ] {x : κ → ℤ} (hx : x ≠ 0) : ↑(Finset.univ.gcd x) * arakelovMulHeight (Int.cast ∘ x) = √(∑ i : κ, ↑(x i) ^ 2)

The Arakelov sup-norm-to-height translation. The Arakelov height of a nonzero tuple of integers, read as a tuple of rationals, is its euclidean norm divided by the greatest common divisor of its entries. Layer 4.3's NumberField.arakelovMulHeight_intCast_of_gcd_eq_one is the primitive case, and Layer 5.1's Rat.gcd_mul_mulHeight_intCast is the same statement for the sup norm.

The greatest common divisor of the maximal minors

noncomputable def Int.Matrix.minorGcd {ι : Type u_1} [Fintype ι] [LinearOrder ι] {m : ℕ} (A : Matrix (Fin m) ι ℤ) : ℤ

The greatest common divisor of the maximal minors of an integer matrix — the D of Bombieri–Vaaler. The minors are Layer 3.1's Plücker coordinates of the rows, indexed by the sets of m columns.

Equations

• Int.Matrix.minorGcd A = Finset.univ.gcd (exteriorPower.plucker m A.row)

theorem Int.Matrix.linearIndependent_row_map_rat_iff {ι : Type u_1} [Fintype ι] [LinearOrder ι] {m : ℕ} (A : Matrix (Fin m) ι ℤ) : LinearIndependent ℚ (A.map Int.cast).row ↔ (A * A.transpose).det ≠ 0

The rank hypothesis is a condition on the integer matrix alone: the rows are linearly independent over ℚ exactly when the Gram determinant of the rows is nonzero. This is Layer 3.4's Gram criterion, read over ℤ.

theorem Int.Matrix.det_pos {ι : Type u_1} [Fintype ι] [LinearOrder ι] {m : ℕ} {A : Matrix (Fin m) ι ℤ} (hA : LinearIndependent ℚ (A.map Int.cast).row) : 0 < (A * A.transpose).det

The Gram determinant is positive under the rank hypothesis, so the Bombieri–Vaaler bound is a positive real and the absolute value the literature writes around det (A Aᵀ) is redundant.

theorem Int.Matrix.one_le_minorGcd {ι : Type u_1} [Fintype ι] [LinearOrder ι] {m : ℕ} {A : Matrix (Fin m) ι ℤ} (hA : LinearIndependent ℚ (A.map Int.cast).row) : 1 ≤ minorGcd A

The divisor D is at least 1 under the rank hypothesis: it is a normalized greatest common divisor of integers not all zero.

theorem Int.Matrix.minorGcd_mul_arakelovMulHeight_ker {ι : Type u_1} [Fintype ι] [LinearOrder ι] {m : ℕ} (A : Matrix (Fin m) ι ℤ) (hA : LinearIndependent ℚ (A.map Int.cast).row) : ↑(minorGcd A) * (A.map Int.cast).mulVecLin.ker.arakelovMulHeight = √↑(A * A.transpose).det

The identity the Bombieri–Vaaler bound is: D times the Arakelov height of the solution space of A x = 0 is √(det (A Aᵀ)). Layer 3.5 identifies the height of the solution space with that of the row space, Layer 3.3 computes the latter as the height of the tuple of maximal minors, and NumberField.gcd_mul_arakelovMulHeight_intCast divides out its content; the sum of squares of minors is Layer 3.4's Cauchy–Binet identity.

theorem Int.Matrix.minorGcd_unit_mul {ι : Type u_1} [Fintype ι] [LinearOrder ι] {m : ℕ} {U : Matrix (Fin m) (Fin m) ℤ} (hU : IsUnit U.det) (A : Matrix (Fin m) ι ℤ) : minorGcd (U * A) = minorGcd A

A row operation of determinant ±1 does not change the divisor D: it scales every maximal minor by that determinant, which a normalized greatest common divisor does not see.

theorem Int.Matrix.det_mul_transpose_self_unit_mul {ι : Type u_1} [Fintype ι] [LinearOrder ι] {m : ℕ} {U : Matrix (Fin m) (Fin m) ℤ} (hU : IsUnit U.det) (A : Matrix (Fin m) ι ℤ) : (U * A * (U * A).transpose).det = (A * A.transpose).det

A row operation of determinant ±1 does not change the Gram determinant of the rows.

theorem Int.Matrix.sqrt_det_div_minorGcd_unit_mul {ι : Type u_1} [Fintype ι] [LinearOrder ι] {m : ℕ} {U : Matrix (Fin m) (Fin m) ℤ} (hU : IsUnit U.det) (A : Matrix (Fin m) ι ℤ) : √↑(U * A * (U * A).transpose).det / ↑(minorGcd (U * A)) = √↑(A * A.transpose).det / ↑(minorGcd A)

The invariance of the Bombieri–Vaaler bound (Bombieri–Vaaler (2.5)): D⁻¹ √(det (A Aᵀ)) is unchanged by A ↦ U A for U ∈ GL_M(ℤ), which fixes the solution space. This is what Theorem 1 has over the classical Siegel lemma of Layer 5.1, whose bound depends on the entries and so moves under a row operation.

Bombieri–Vaaler's theorems

theorem Int.Matrix.exists_linearIndependent_mulVec_eq_zero_prod_iSup_abs_le {ι : Type u_1} [Fintype ι] [LinearOrder ι] {m : ℕ} (A : Matrix (Fin m) ι ℤ) (hA : LinearIndependent ℚ (A.map Int.cast).row) : ∃ (x : Fin (Fintype.card ι - m) → ι → ℤ), LinearIndependent ℤ x ∧ (∀ (l : Fin (Fintype.card ι - m)), A.mulVec (x l) = 0) ∧ ∏ l : Fin (Fintype.card ι - m), ↑(⨆ (i : ι), |x l i|) ≤ √↑(A * A.transpose).det / ↑(minorGcd A)

Bombieri–Vaaler's Theorem 2 (Bombieri–Vaaler 1983, Theorem 2; Aliev–Henk 2023, §6, Theorem 6.2). For an M × N integer matrix with linearly independent rows there are N - M linearly independent integral solutions of A x = 0 whose sup norms have product at most D⁻¹ √(det (A Aᵀ)), D the greatest common divisor of the maximal minors.

No hypothesis M < N is needed: at N = M the conclusion is the empty product 1 on the left and the Arakelov height of the zero subspace, also 1, on the right.

theorem Int.Matrix.exists_linearIndependent_mulVec_eq_zero_prod_mulHeight_le {ι : Type u_1} [Fintype ι] [LinearOrder ι] {m : ℕ} (A : Matrix (Fin m) ι ℤ) (hA : LinearIndependent ℚ (A.map Int.cast).row) : ∃ (x : Fin (Fintype.card ι - m) → ι → ℤ), LinearIndependent ℤ x ∧ (∀ (l : Fin (Fintype.card ι - m)), A.mulVec (x l) = 0) ∧ ∏ l : Fin (Fintype.card ι - m), Height.mulHeight (Int.cast ∘ x l) ≤ √↑(A * A.transpose).det / ↑(minorGcd A)

Bombieri–Vaaler's Theorem 2, in height form — the K = ℚ case of the statement Layer 5.4 makes over a number field, the discriminant being 1. The proof applies the pointwise inequality Rat.mulHeight_intCast_le to the sup-norm form above: the height of a nonzero integer tuple is its sup norm divided by its content, by Rat.gcd_mul_mulHeight_intCast.

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

Bombieri–Vaaler's Theorem 1 (Bombieri–Vaaler 1983, Theorem 1; also a one-vector consequence of the product bound in Aliev–Henk 2023, §6, Theorem 6.2). For an M × N integer matrix with linearly independent rows and M < N there is a nonzero integral solution of A x = 0 with sup norm at most (D⁻¹ √(det (A Aᵀ)))^{1/(N - M)}.

Unlike the bound of Layer 5.1 this one is invariant under A ↦ U A for U ∈ GL_M(ℤ), by Int.Matrix.sqrt_det_div_minorGcd_unit_mul.