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 {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (A : Matrix α β ℤ) (hA : A ≠ 0) : 1 ≤ ‖A‖

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

theorem Int.Matrix.exists_ne_zero_int_vec_norm_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] [DecidableEq α] (A : Matrix α β ℤ) (hn : Fintype.card α < Fintype.card β) (hm : 0 < Fintype.card α) : ∃ (t : β → ℤ), t ≠ 0 ∧ A.mulVec t = 0 ∧ ‖t‖ ≤ (↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))

theorem Int.Matrix.exists_ne_zero_int_vec_norm_le' {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] [DecidableEq α] (A : Matrix α β ℤ) (hn : Fintype.card α < Fintype.card β) (hm : 0 < Fintype.card α) (hA : A ≠ 0) : ∃ (t : β → ℤ), t ≠ 0 ∧ A.mulVec t = 0 ∧ ‖t‖ ≤ (↑(Fintype.card β) * ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))