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-zerom × n
matrixA
withm < n
the linear system it determines has a non-zero integer solutiont
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.
theorem
Int.Matrix.exists_ne_zero_int_vec_norm_le
{α : Type u_1}
{β : Type u_2}
[Fintype α]
[Fintype β]
(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 β]
(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 α)))