Documentation

Mathlib.NumberTheory.SiegelsLemma

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 #

Notation #

References #

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

theorem Int.Matrix.one_le_norm_A_of_ne_zero {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (A : Matrix α β ) (hA : A 0) :

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 β] (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 α)))