Effective arithmetic bounds and geometry of numbers
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
TheoremEffective Hermite--Minkowski#
Inside a fixed extension A / ℚ, the number of number fields
K (finite extensions of ℚ) with |discr K| ≤ N is at most
(2 * coeffBoundOfDiscrBdd N + 1) ^ (rankOfDiscrBdd N + 1) * rankOfDiscrBdd N, an explicit function
of N alone. This upgrades Mathlib's NumberField.finite_of_discr_bdd from finiteness to an
explicit count.
NumberField.ncard_setOf_finiteDimensional_abs_discr_le_le.{u_1} (A : Type u_1) [Field A]
[CharZero A] (N : ℕ) :
{K | |NumberField.discr ↥↑K| ≤ ↑N}.ncard ≤
(2 * NumberField.coeffBoundOfDiscrBdd N + 1) ^
(NumberField.hermiteTheorem.rankOfDiscrBdd N + 1) *
NumberField.hermiteTheorem.rankOfDiscrBdd N
Lean
Formalized in Tau Ceti as NumberField.ncard_setOf_finiteDimensional_abs_discr_le_le.
Sources
Uses 2
TheoremNumberField.card_ideal_absNorm_le#
In any number field F, the set of nonzero integral ideals with norm at most X is
finite, and for X ≥ 1 its cardinality is at most X² * 2^[F:ℚ].
NumberField.card_ideal_absNorm_le.{u_1} (F : Type u_1) [Field F] [NumberField F] {X : ℝ}
(hX : 1 ≤ X) :
{I | I ≠ ⊥ ∧ ↑(Ideal.absNorm I) ≤ X}.Finite ∧
↑{I | I ≠ ⊥ ∧ ↑(Ideal.absNorm I) ≤ X}.ncard ≤ X ^ 2 * 2 ^ Module.finrank ℚ F
TheoremTauCeti.Polynomial.ncard_biUnion_roots_natDegree_le_abs_intCoeff_le#
The integer specialisation: the roots in a domain S of all integer polynomials of degree at
most d with every coefficient bounded by B in absolute value number at most
(2 · B + 1) ^ (d + 1) · d. Each of the 2 · B + 1 integers in [-B, B] is an allowed
coefficient, and a degree-≤ d polynomial has at most d roots.
TauCeti.Polynomial.ncard_biUnion_roots_natDegree_le_abs_intCoeff_le.{u_2} {S : Type u_2}
[CommRing S] [IsDomain S] [DecidableEq S] (m : ℤ →+* S) (d B : ℕ) :
(⋃ f,
⋃ (_ : f.natDegree ≤ d ∧ ∀ (i : ℕ), |f.coeff i| ≤ ↑B),
↑(Polynomial.map m f).roots.toFinset).ncard ≤
(2 * B + 1) ^ (d + 1) * d
Lean
Formalized in Tau Ceti as TauCeti.Polynomial.ncard_biUnion_roots_natDegree_le_abs_intCoeff_le.
Sources
TheoremNorthcott's theorem for the naive height, with Evertse's count#
In a field of
characteristic zero, the algebraic elements of degree at most d and naive height at most B
form a finite set with at most d (2⌊B⌋ + 1)^(d + 1) elements.
TauCeti.finite_setOf_naiveHeight_le.{u_1} {F : Type u_1} [Field F] [CharZero F] (d : ℕ) (B : ℝ) :
{z | IsAlgebraic ℚ z ∧ (minpoly ℚ z).natDegree ≤ d ∧ TauCeti.naiveHeight z ≤ B}.Finite ∧
{z | IsAlgebraic ℚ z ∧ (minpoly ℚ z).natDegree ≤ d ∧ TauCeti.naiveHeight z ≤ B}.ncard ≤
d * (2 * ⌊B⌋₊ + 1) ^ (d + 1)
Lean
Formalized in Tau Ceti as TauCeti.finite_setOf_naiveHeight_le.
Other forms
Northcott's theorem for subspaces (Schmidt). Formalized in Tau Ceti as Submodule.finite_subspaceHeight_le.
Submodule.finite_subspaceHeight_le.{u_1, u_2} {ι : Type u_1} {K : Type u_2} [LinearOrder ι]
[Finite ι] [Field K] [NumberField K] (B : ℝ) : {U | U.subspaceHeight ≤ B}.Finite
Northcott's theorem for the absolute height. Formalized in Tau Ceti as TauCeti.finite_setOf_absMulHeight₁_le.
TauCeti.finite_setOf_absMulHeight₁_le.{u_1} {F : Type u_1} [Field F] [CharZero F] (d : ℕ) (B : ℝ) :
{x | IsAlgebraic ℚ x ∧ (minpoly ℚ x).natDegree ≤ d ∧ NumberField.absMulHeight₁ x ≤ B}.Finite
Northcott's theorem for the Mahler measure. Formalized in Tau Ceti as TauCeti.finite_setOf_mahlerMeasure_le.
TauCeti.finite_setOf_mahlerMeasure_le.{u_1} {F : Type u_1} [Field F] [CharZero F] (d : ℕ) (B : ℝ) :
{z | IsAlgebraic ℚ z ∧ (minpoly ℚ z).natDegree ≤ d ∧ TauCeti.mahlerMeasure z ≤ B}.Finite
Sources
Uses 3
TheoremThe regulator of a number field of unit rank zero is 1#
When the unit rank is zero,
the unit lattice sits inside the zero-dimensional log space, and the regulator — its covolume,
computed by NumberField.Units.regulator_eq_det' as a determinant indexed by the infinite
places other than the distinguished one — is the determinant of the empty matrix, 1.
NumberField.Units.regulator_eq_one_of_rank_eq_zero.{u_1} (K : Type u_1) [Field K] [NumberField K]
(h : NumberField.Units.rank K = 0) : NumberField.Units.regulator K = 1
Lean
Formalized in Tau Ceti as NumberField.Units.regulator_eq_one_of_rank_eq_zero.
Sources
DefinitionNumberField.coeffBoundOfDiscrBdd#
An explicit height bound for the integer minimal polynomial of a primitive generator of a number
field of discriminant ≤ N. It is ⌈M ^ D * (D.choose (D / 2))⌉₊ where D = rankOfDiscrBdd N is
Mathlib's degree bound and M = max √(1 + boundOfDiscBdd N ^ 2) 1 dominates the per-conjugate bound
of both the real and complex primitive elements of finite_of_discr_bdd.
NumberField.coeffBoundOfDiscrBdd (N : ℕ) : ℕ
Used by 1
DefinitionNumberField.hermiteCountBound#
The elementary polynomial count appearing in effective Hermite--Minkowski: if every field is
generated by a root of an integer polynomial of degree at most D and coefficient height at most
C, then the number of possible generated fields is bounded by
(2 * C + 1) ^ (D + 1) * D.
NumberField.hermiteCountBound (D C : ℕ) : ℕ
TheoremTauCeti.index_square_le_of_closure_eq_top#
In a commutative group generated by a finite set S, the subgroup of squares has index at
most 2 ^ S.card. The quotient by the squares is an elementary abelian 2-group spanned by
the image of S.
TauCeti.index_square_le_of_closure_eq_top.{u_1} {G : Type u_1} [CommGroup G] {S : Finset G}
(hS : Subgroup.closure ↑S = ⊤) : (Subgroup.square G).index ≤ 2 ^ S.card
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.