The exponent in Siegel's lemma is optimal

Siegel's lemma (Mathlib's Int.Matrix.exists_ne_zero_int_vec_norm_le) gives a nonzero integer solution x of an m × n integer system A x = 0, m < n, with ‖x‖ ≤ (n · max 1 ‖A‖) ^ (m / (n - m)) in the sup norms. This file shows that for n = m + 1 the exponent m / (n - m) = m cannot be lowered, whatever the constant.

The witness is the system b xᵢ = xᵢ₊₁, 0 ≤ i < m, whose coefficient matrix TauCeti.Matrix.geomRecurrence b m has entries b, -1 and 0. Its solutions are the geometric progressions xᵢ = bⁱ x₀, so its kernel is spanned by (1, b, …, bᵐ) and every nonzero integer solution has sup norm at least |b| ^ m, against Siegel's bound ((m + 1) |b|) ^ m for |b| ≥ 1.

Main definitions

• TauCeti.Matrix.geomRecurrence b m: the m × (m + 1) matrix of the recurrence b xᵢ - xᵢ₊₁ = 0.

Main results

• TauCeti.Matrix.mulVec_geomRecurrence_eq_zero_iff: the solutions are the geometric progressions of ratio b.
• TauCeti.Matrix.ker_mulVecLin_geomRecurrence: over a commutative ring the kernel is the span of (1, b, …, bᵐ).
• TauCeti.Matrix.norm_geomRecurrence: for 0 < m, the sup norm of the matrix is max ‖b‖ 1.
• TauCeti.Matrix.pow_le_iSup_abs_of_mulVec_geomRecurrence_eq_zero: over ℤ, every nonzero solution has sup norm at least |b| ^ m.
• TauCeti.Int.Matrix.not_forall_exists_ne_zero_int_vec_norm_le: for 0 < m and any exponent e < m and constant C, not every m × (m + 1) integer system has a nonzero solution of sup norm at most C · max 1 ‖A‖ ^ e.

References

• C. L. Siegel, Über einige Anwendungen diophantischer Approximationen, Abh. Preuss. Akad. Wiss. (1929).
• E. Bombieri and J. Vaaler, On Siegel's lemma, Invent. Math. 73 (1983), 11–32.
• M. Hindry and J. H. Silverman, Diophantine Geometry: An Introduction, GTM 201, Springer, 2000, §D.4.

def TauCeti.Matrix.geomRecurrence {R : Type u_1} [Ring R] (b : R) (m : ℕ) : Matrix (Fin m) (Fin (m + 1)) R

The m × (m + 1) coefficient matrix of the linear recurrence b xᵢ - xᵢ₊₁ = 0 for 0 ≤ i < m: row i has b in column i, -1 in column i + 1 and 0 elsewhere. Its solutions are the geometric progressions of ratio b.

theorem TauCeti.Matrix.geomRecurrence_apply {R : Type u_1} [Ring R] (b : R) {m : ℕ} (i : Fin m) (j : Fin (m + 1)) : geomRecurrence b m i j = (if j = i.castSucc then b else 0) - if j = i.succ then 1 else 0

@[simp]

theorem TauCeti.Matrix.mulVec_geomRecurrence {R : Type u_1} [Ring R] (b : R) {m : ℕ} (x : Fin (m + 1) → R) (i : Fin m) : (geomRecurrence b m).mulVec x i = b * x i.castSucc - x i.succ

theorem TauCeti.Matrix.mulVec_geomRecurrence_eq_zero_iff {R : Type u_1} [Ring R] {b : R} {m : ℕ} {x : Fin (m + 1) → R} : (geomRecurrence b m).mulVec x = 0 ↔ ∀ (i : Fin (m + 1)), x i = b ^ ↑i * x 0

The solutions of b xᵢ = xᵢ₊₁ are the geometric progressions xᵢ = bⁱ x₀.

theorem TauCeti.Matrix.eq_zero_of_mulVec_geomRecurrence_eq_zero {R : Type u_1} [Ring R] {b : R} {m : ℕ} {x : Fin (m + 1) → R} (h : (geomRecurrence b m).mulVec x = 0) (h₀ : x 0 = 0) : x = 0

A solution of b xᵢ = xᵢ₊₁ vanishes as soon as its first coordinate does.

theorem TauCeti.Matrix.ker_mulVecLin_geomRecurrence {R : Type u_1} [CommRing R] (b : R) (m : ℕ) : (geomRecurrence b m).mulVecLin.ker = R ∙ fun (i : Fin (m + 1)) => b ^ ↑i

Over a commutative ring the kernel of b xᵢ = xᵢ₊₁ is free of rank one, spanned by the geometric progression (1, b, …, bᵐ).

theorem TauCeti.Matrix.norm_geomRecurrence {R : Type u_1} [NormedRing R] [NormOneClass R] (b : R) {m : ℕ} (hm : 0 < m) : ‖geomRecurrence b m‖ = max ‖b‖ 1

The sup norm of the matrix of b xᵢ = xᵢ₊₁ is max ‖b‖ 1, as soon as there is an equation.

theorem TauCeti.Matrix.pow_le_iSup_abs_of_mulVec_geomRecurrence_eq_zero {b : ℤ} {m : ℕ} {x : Fin (m + 1) → ℤ} (hx : x ≠ 0) (h : (geomRecurrence b m).mulVec x = 0) : |b| ^ m ≤ ⨆ (i : Fin (m + 1)), |x i|

The lower bound in the system b xᵢ = xᵢ₊₁. Every nonzero integer solution has sup norm at least |b| ^ m.

theorem TauCeti.Matrix.pow_le_norm_of_mulVec_geomRecurrence_eq_zero {b : ℤ} {m : ℕ} {x : Fin (m + 1) → ℤ} (hx : x ≠ 0) (h : (geomRecurrence b m).mulVec x = 0) : |↑b| ^ m ≤ ‖x‖

The lower bound pow_le_iSup_abs_of_mulVec_geomRecurrence_eq_zero in the norm of ℤ^(m+1), which is the sup norm in which Siegel's lemma is stated.

theorem TauCeti.Int.Matrix.not_forall_exists_ne_zero_int_vec_norm_le {m : ℕ} (hm : 0 < m) {e : ℝ} (he : e < ↑m) (C : ℝ) : ¬∀ (A : Matrix (Fin m) (Fin (m + 1)) ℤ), ∃ (x : Fin (m + 1) → ℤ), x ≠ 0 ∧ A.mulVec x = 0 ∧ ‖x‖ ≤ C * max 1 ‖A‖ ^ e

The exponent in Siegel's lemma is optimal. For an m × (m + 1) integer system, Siegel's lemma Int.Matrix.exists_ne_zero_int_vec_norm_le gives a nonzero integer solution of sup norm at most ((m + 1) · max 1 ‖A‖) ^ m. For 0 < m no exponent e < m works, with any constant C: the system b xᵢ = xᵢ₊₁ with b large has no nonzero integer solution of sup norm at most C · max 1 ‖A‖ ^ e.