Siegel's Lemma

In this file we introduce and prove Siegel's Lemma in its most basic version. This is a fundamental tool in diophantine approximation and transcendency and says that there exists a "small" integral non-zero solution of a non-trivial underdetermined system of linear equations with integer coefficients.

Main results

• exists_ne_zero_int_vec_norm_le: Given a non-zero m × n matrix A with m < n the linear system it determines has a non-zero integer solution t with ‖t‖ ≤ ((n * ‖A‖) ^ ((m : ℝ) / (n - m)))

Notation

• ‖_‖ : Matrix.seminormedAddCommGroup is the sup norm, the maximum of the absolute values of the entries of the matrix

References

See [M. Hindry and J. Silverman, Diophantine Geometry: an Introduction][hindrysilverman00].

theorem Int.Matrix.one_le_norm_A_of_ne_zero (m : ℕ) (n : ℕ) (A : Matrix (Fin m) (Fin n) ℤ) (hA : A ≠ 0) : 1 ≤ ‖A‖

The sup norm of a non-zero integer matrix is at lest one

theorem Int.Matrix.exists_ne_zero_int_vec_norm_le (m : ℕ) (n : ℕ) (A : Matrix (Fin m) (Fin n) ℤ) (hn : m < n) (hm : 0 < m) (hA_nezero : A ≠ 0) : ∃ (t : Fin n → ℤ), t ≠ 0 ∧ A.mulVec t = 0 ∧ ‖t‖ ≤ (↑n * ‖A‖) ^ (↑m / (↑n - ↑m))