Heights, units and S-units of number fields
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremA reduced fundamental system (Bugeaud–Győry, Lemma 1)#
Some fundamental system ε of
units has ∏ i, absLogHeight₁ (ε i) ≤ (r!) ^ 2 / (2 ^ (r - 1) * [K : ℚ] ^ r) * regulator K, where
r = rank K. The constant is attained for ℚ(√2). By Hadamard's bound
regulator_le_prod_absLogHeight₁, every fundamental system also has
regulator K ≤ (2 * [K : ℚ]) ^ r * ∏ i, absLogHeight₁ (ε i).
TauCeti.NumberField.Units.exists_fundSystem_prod_absLogHeight₁_le.{u_1} {K : Type u_1} [Field K]
[NumberField K] :
∃ ε,
Subgroup.closure (Set.range ε) ⊔ NumberField.Units.torsion K = ⊤ ∧
∏ i, NumberField.absLogHeight₁ ((algebraMap (NumberField.RingOfIntegers K) K) ↑(ε i)) ≤
↑(NumberField.Units.rank K).factorial ^ 2 /
(2 ^ (NumberField.Units.rank K - 1) *
↑(Module.finrank ℚ K) ^ NumberField.Units.rank K) *
NumberField.Units.regulator K
Lean
Formalized in Tau Ceti as TauCeti.NumberField.Units.exists_fundSystem_prod_absLogHeight₁_le.
Sources
Uses 1
TheoremTauCeti.NumberField.Units.regulator_le_prod_absLogHeight₁#
Every fundamental system bounds the field regulator by (2d) ^ r times the product
of its absolute logarithmic heights, where d is the degree and r the unit rank.
TauCeti.NumberField.Units.regulator_le_prod_absLogHeight₁.{u_1} {K : Type u_1} [Field K]
[NumberField K] {ε : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ}
(hε : Subgroup.closure (Set.range ε) ⊔ NumberField.Units.torsion K = ⊤) :
NumberField.Units.regulator K ≤
(2 * ↑(Module.finrank ℚ K)) ^ NumberField.Units.rank K *
∏ i, NumberField.absLogHeight₁ ((algebraMap (NumberField.RingOfIntegers K) K) ↑(ε i))
Lean
Formalized in Tau Ceti as TauCeti.NumberField.Units.regulator_le_prod_absLogHeight₁.
Sources
Uses 1
ℚ(√2)TheoremMinkowski's second theorem, upper bound, in terms of the successive minima#
For a full
lattice L in a real normed space E of dimension n, a Haar measure μ on E, and a convex
body K symmetric about 0, the successive minima λ i = successiveMin L K i satisfy
λ₀ ⋯ λₙ₋₁ · μ K ≤ 2ⁿ · covolume L μ. If K has empty interior, its measure is zero.
ZLattice.prod_successiveMin_mul_measure_le_two_pow_mul_covolume.{u_1} {E : Type u_1}
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
[BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L]
(μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : ConvexBody E}
(hKs : ∀ x ∈ K, -x ∈ K) :
ENNReal.ofReal (∏ i, ZLattice.successiveMin L K i) * μ ↑K ≤
2 ^ Module.finrank ℝ E * ENNReal.ofReal (ZLattice.covolume L μ)
Lean
Formalized in Tau Ceti as ZLattice.prod_successiveMin_mul_measure_le_two_pow_mul_covolume.
Other forms
Minkowski's second theorem. Formalized in Tau Ceti as Convex.prod_mul_volume_real_le_two_pow.
Convex.prod_mul_volume_real_le_two_pow {n : ℕ} {K : Set (Fin n → ℝ)} (hK : Convex ℝ K)
(hKs : ∀ x ∈ K, -x ∈ K) {a : Fin n → ℝ} (ha : ∀ (i : Fin n), 0 ≤ a i)
(hgap :
∀ (i : Fin n) (z : Fin n → ℤ),
(gauge K fun j => ↑(z j)) < a i → ∀ (j : Fin n), i ≤ j → z j = 0) :
(∏ i, a i) * MeasureTheory.volume.real K ≤ 2 ^ n
Minkowski's second theorem, upper bound. Formalized in Tau Ceti as ZLattice.prod_mul_measure_le_two_pow_mul_covolume.
ZLattice.prod_mul_measure_le_two_pow_mul_covolume.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E)
[DiscreteTopology ↥L] (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure]
{K : Set E} (hK : Convex ℝ K) (hKs : ∀ x ∈ K, -x ∈ K) {n : ℕ} (hn : n = Module.finrank ℝ E)
{a : Fin n → E} (haL : ∀ (i : Fin n), a i ∈ L) (ha : LinearIndependent ℝ a) {g : Fin n → ℝ}
(hg0 : ∀ (i : Fin n), 0 ≤ g i)
(hgap : ∀ (j : Fin n), ∀ v ∈ L, gauge K v < g j → v ∈ Submodule.span ℝ (a '' Set.Iio j)) :
ENNReal.ofReal (∏ i, g i) * μ K ≤ 2 ^ n * ENNReal.ofReal (ZLattice.covolume L μ)
Minkowski's second theorem. Formalized in Tau Ceti as ZLattice.prod_successiveMin_mul_measureReal_le_two_pow_mul_covolume.
ZLattice.prod_successiveMin_mul_measureReal_le_two_pow_mul_covolume.{u_1} {E : Type u_1}
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
[BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L]
(μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : ConvexBody E}
(hKs : ∀ x ∈ K, -x ∈ K) :
(∏ i, ZLattice.successiveMin L K i) * μ.real ↑K ≤ 2 ^ Module.finrank ℝ E * ZLattice.covolume L μ
Minkowski's second theorem, lower bound, general form. Formalized in Tau Ceti as ZLattice.two_pow_div_factorial_mul_covolume_le_prod_mul_measure.
ZLattice.two_pow_div_factorial_mul_covolume_le_prod_mul_measure.{u_1, u_2} {E : Type u_1}
[NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E)
[DiscreteTopology ↥L] (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure]
{K : Set E} (hK : Convex ℝ K) (h0 : 0 ∈ K) (hKs : ∀ x ∈ K, -x ∈ K) {ι : Type u_2} [Fintype ι]
(b : Module.Basis ι ℝ E) (hbL : ∀ (i : ι), b i ∈ L) {a : ι → ℝ} (ha : ∀ (i : ι), 0 ≤ a i)
(hbK : ∀ (i : ι), b i ∈ a i • K) :
ENNReal.ofReal
(2 ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E).factorial * ZLattice.covolume L μ) ≤
ENNReal.ofReal (∏ i, a i) * μ K
Minkowski's second theorem, lower bound, in terms of the successive minima. Formalized in Tau Ceti as ZLattice.two_pow_div_factorial_mul_covolume_le_prod_successiveMin_mul_measure.
ZLattice.two_pow_div_factorial_mul_covolume_le_prod_successiveMin_mul_measure.{u_1} {E : Type u_1}
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
[BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L]
(μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : ConvexBody E}
(hK : 0 ∈ interior ↑K) (hKs : ∀ x ∈ K, -x ∈ K) :
ENNReal.ofReal
(2 ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E).factorial * ZLattice.covolume L μ) ≤
ENNReal.ofReal (∏ i, ZLattice.successiveMin L K i) * μ ↑K
Minkowski's second theorem. Formalized in Tau Ceti as ZLattice.two_pow_div_factorial_mul_covolume_le_prod_successiveMin_mul_measureReal.
ZLattice.two_pow_div_factorial_mul_covolume_le_prod_successiveMin_mul_measureReal.{u_1}
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
[MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L]
(μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : ConvexBody E}
(hK : 0 ∈ interior ↑K) (hKs : ∀ x ∈ K, -x ∈ K) :
2 ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E).factorial * ZLattice.covolume L μ ≤
(∏ i, ZLattice.successiveMin L K i) * μ.real ↑K
Minkowski's second theorem for bodies of measure at least 2ⁿ. Formalized in Tau Ceti as ZLattice.prod_successiveMin_le_covolume_of_two_pow_finrank_le.
ZLattice.prod_successiveMin_le_covolume_of_two_pow_finrank_le.{u_1} {E : Type u_1}
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
[BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L]
(μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : ConvexBody E}
(hKs : ∀ x ∈ K, -x ∈ K) (hμK : 2 ^ Module.finrank ℝ E ≤ μ ↑K) :
∏ i, ZLattice.successiveMin L K i ≤ ZLattice.covolume L μ
Sources
TheoremBombieri and Vaaler's Theorem 2 over ℤ, in the sup norm#
Let A be a p × n integer
matrix with linearly independent rows, and let g be the greatest common divisor of its maximal
minors. Then A x = 0 has n - p linearly independent integral solutions x l, each with
coprime coordinates, whose sup norms ‖x l‖ = max_i |x l i| satisfy
∏ l, ‖x l‖ ≤ √det (A Aᵀ) / g.
Matrix.exists_linearIndependent_mulVec_eq_zero_prod_norm_le.{u_1} {ι : Type u_1} [Fintype ι] {p : ℕ}
{A : Matrix (Fin p) ι ℤ} (hA : LinearIndependent ℚ (A.map Int.cast).row) :
∃ x,
LinearIndependent ℤ x ∧
(∀ (l : Fin (Fintype.card ι - p)), A.mulVec (x l) = 0) ∧
(∀ (l : Fin (Fintype.card ι - p)), Finset.univ.gcd (x l) = 1) ∧
∏ l, ‖x l‖ ≤ √↑(A * A.transpose).det / ↑A.minorGcd
Lean
Formalized in Tau Ceti as Matrix.exists_linearIndependent_mulVec_eq_zero_prod_norm_le.
Sources
Uses 6 · Used by 1
TheoremVaaler's cube-slicing theorem#
Every central slice of the cube [-1, 1] ^ ι by a
subspace V of EuclideanSpace ℝ ι has volume at least 2 ^ finrank ℝ V, computed in V.
Submodule.two_pow_finrank_le_volume_setOf_forall_abs_le_one.{u_1} {ι : Type u_1} [Fintype ι]
(V : Submodule ℝ (EuclideanSpace ℝ ι)) :
2 ^ Module.finrank ℝ ↥V ≤ MeasureTheory.volume {x | ∀ (i : ι), |(↑x).ofLp i| ≤ 1}
Lean
Formalized in Tau Ceti as Submodule.two_pow_finrank_le_volume_setOf_forall_abs_le_one.
Sources
TheoremThe determinant formula for the S-regulator#
For a family ε of S-units that, together
with the torsion subgroup, generates the S-units, an infinite place w' and any identification
e of ι with the places of S and the infinite places other than w', the S-regulator is the
absolute value of the determinant of the matrix whose i-th row lists mult w * log (w (ε i)) at
the infinite places w ≠ w' and log ‖ε i‖_v at the places v ∈ S, in the order given by e.
The family ε is then a fundamental system, its cardinality being forced by e. This is the
S-analogue of Mathlib's NumberField.Units.regulator_eq_det.
TauCeti.NumberField.SUnit.regulator_eq_abs_det.{u_1, u_2} {K : Type u_1} [Field K] [NumberField K]
{S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {ι : Type u_2}
[Fintype ι] [DecidableEq ι] {ε : ι → ↥((↑S).unit K)}
(hε : Subgroup.closure (Set.range ε) ⊔ CommGroup.torsion ↥((↑S).unit K) = ⊤)
(w' : NumberField.InfinitePlace K) (e : ι ≃ { w // w ≠ w' } ⊕ ↥S) :
TauCeti.NumberField.SUnit.regulator S =
|(Matrix.of fun i k =>
Sum.elim (fun w => ↑(↑w).mult * Real.log (↑w ↑↑(ε i)))
(fun v => Real.log ((NumberField.FinitePlace.mk ↑v) ↑↑(ε i))) (e k)).det|
Uses 1
TheoremKronecker's theorem for projective tuples#
A tuple with algebraic coordinates has absolute
projective height one if and only if, for every nonzero coordinate x j, each ratio x i / x j
is zero or of finite multiplicative order. This includes the zero tuple.
TauCeti.absoluteProjectiveTupleHeight_eq_one_iff.{u_1, u_2} {F : Type u_1} [Field F] [CharZero F]
{ι : Type u_2} [Finite ι] {x : ι → F} (hx : ∀ (i : ι), IsAlgebraic ℚ (x i)) :
TauCeti.absoluteProjectiveTupleHeight x = 1 ↔
∀ (i j : ι), x j ≠ 0 → x i = 0 ∨ IsOfFinOrder (x i / x j)
Lean
Formalized in Tau Ceti as TauCeti.absoluteProjectiveTupleHeight_eq_one_iff.
Other forms
Kronecker's theorem. Formalized in Tau Ceti as TauCeti.house_eq_one_iff.
TauCeti.house_eq_one_iff.{u_1} {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : IsIntegral ℤ x) :
TauCeti.house x = 1 ↔ ∃ n, 0 < n ∧ x ^ n = 1
Kronecker's theorem. Formalized in Tau Ceti as TauCeti.mahlerMeasure_eq_one_iff.
TauCeti.mahlerMeasure_eq_one_iff.{u_1} {F : Type u_1} [Field F] [CharZero F] {x : F}
(hx : IsAlgebraic ℚ x) : TauCeti.mahlerMeasure x = 1 ↔ x = 0 ∨ ∃ n, 0 < n ∧ x ^ n = 1
Sources
Uses 1
DefinitionZLattice.successiveMin#
The successive minima of a ℤ-submodule L of E with respect to a convex body K, indexed
from zero: successiveMin L K i is the infimum of the dilation factors t ≥ 0 for which t • K
contains i + 1 vectors of L that are linearly independent over ℝ.
When no dilate of K contains i + 1 independent vectors of L (for instance when L has rank
at most i, or when K is a segment containing 0 and 1 ≤ i), the infimum is over the empty
set and successiveMin L K i takes the junk value sInf ∅ = 0; the minima then need not be
positive or monotone. For a discrete spanning lattice L and 0 in the interior of K, the
hypotheses of the main results, the set is nonempty and the infimum is attained
(ZLattice.successiveMin_isLeast).
ZLattice.successiveMin.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
(L : Submodule ℤ E) (K : ConvexBody E) (i : Fin (Module.finrank ℝ E)) : ℝ
Used by 6
ℤ, in the sup norm · Minkowski's first theorem on the successive minima · Minkowski's second theorem for the unit lattice · Minkowski's second theorem, upper bound, in terms of the successive minima · Siegel's lemma for a rational subspace, in the sup normTheoremA basis from the successive minima (Cassels, Chapter V, Lemma 8)#
For a discrete spanning
lattice L and a symmetric convex body K with 0 in its interior, some ℤ-basis b of L has
b i ∈ (max 1 ((i + 1) / 2) * successiveMin L K i) • K for every i. The factor is 1 for
i ≤ 1, and the product of the factors is n! / 2 ^ (n - 1)
(TauCeti.prod_max_one_add_one_div_two).
ZLattice.exists_basis_mem_smul_successiveMin.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℝ E] {K : ConvexBody E} [FiniteDimensional ℝ E] (L : Submodule ℤ E)
[DiscreteTopology ↥L] [IsZLattice ℝ L] (hK : 0 ∈ interior ↑K) (hsymm : ∀ x ∈ K, -x ∈ K) :
∃ b,
∀ (i : Fin (Module.finrank ℝ E)),
↑(b i) ∈ (max 1 ((↑↑i + 1) / 2) * ZLattice.successiveMin L K i) • ↑K
Uses 1
DefinitionMatrix.minorGcd#
The gcd of the maximal minors of A: the normalized gcd of the determinants
det (A.submatrix id e) over all embeddings e : m ↪ n. It is 0 exactly when every maximal
minor vanishes, in particular when n has fewer elements than m.
Matrix.minorGcd.{u_1, u_2, u_3} {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m]
[DecidableEq m] [Fintype n] [CommRing R] [NormalizedGCDMonoid R] (A : Matrix m n R) : R
TheoremThe height of the kernel of an integer matrix#
The greatest common divisor of the maximal
minors of an integer matrix A, times the absolute Euclidean height of the space of rational
solutions of A y = 0, is √det (A Aᵀ). If the rows are linearly dependent, both sides
vanish.
Matrix.minorGcd_mul_subspaceHeight_ker_mulVecLin.{u_1} {ι : Type u_1} [Fintype ι] [LinearOrder ι]
{p : ℕ} (A : Matrix (Fin p) ι ℤ) :
↑A.minorGcd * (A.map Int.cast).mulVecLin.ker.subspaceHeight = √↑(A * A.transpose).det
Lean
Formalized in Tau Ceti as Matrix.minorGcd_mul_subspaceHeight_ker_mulVecLin.
Sources
Uses 2 · Used by 1
DefinitionTauCeti.NumberField.SUnit.logEmbeddingEquiv#
The S-logarithmic embedding induces a ℤ-linear equivalence from the S-units modulo
torsion onto the S-unit lattice. This is the S-analogue of Mathlib's
NumberField.Units.logEmbeddingEquiv.
TauCeti.NumberField.SUnit.logEmbeddingEquiv.{u_1} {K : Type u_1} [Field K] [NumberField K]
(S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) :
(Additive ↥((↑S).unit K) ⧸ Submodule.torsion ℤ (Additive ↥((↑S).unit K))) ≃ₗ[ℤ]
↥(TauCeti.NumberField.SUnit.unitLattice S)
Used by 1
TheoremBombieri and Vaaler's Siegel lemma over ℤ, in the sup norm#
Let A be a p × n integer
matrix with linearly independent rows and p < n, and let g be the greatest common divisor of
its maximal minors. Then A x = 0 has a nonzero integral solution x with
‖x‖ ≤ (√det (A Aᵀ) / g) ^ (1 / (n - p)), where ‖x‖ = max_i |x i|.
Matrix.exists_ne_zero_mulVec_eq_zero_norm_le.{u_1} {ι : Type u_1} [Fintype ι] {p : ℕ}
{A : Matrix (Fin p) ι ℤ} (hA : LinearIndependent ℚ (A.map Int.cast).row)
(hp : p < Fintype.card ι) :
∃ x,
x ≠ 0 ∧
A.mulVec x = 0 ∧ ‖x‖ ≤ (√↑(A * A.transpose).det / ↑A.minorGcd) ^ (↑(Fintype.card ι) - ↑p)⁻¹
Uses 2
TheoremMinkowski's first theorem on the successive minima#
For a full lattice L in a real normed
space E of positive dimension n, a Haar measure μ on E, and a convex body K symmetric
about 0, the first successive minimum λ₀ of L with respect to K satisfies
λ₀ⁿ · μ.real K ≤ 2ⁿ · covolume L μ. It follows from the upper bound of Minkowski's second
theorem, since λ₀ ≤ λᵢ for every i.
ZLattice.successiveMin_pow_mul_measureReal_le_two_pow_mul_covolume.{u_1} {E : Type u_1}
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
[BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L]
(μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : ConvexBody E}
(hKs : ∀ x ∈ K, -x ∈ K) (hE : 0 < Module.finrank ℝ E) :
ZLattice.successiveMin L K ⟨0, hE⟩ ^ Module.finrank ℝ E * μ.real ↑K ≤
2 ^ Module.finrank ℝ E * ZLattice.covolume L μ
Lean
Formalized in Tau Ceti as ZLattice.successiveMin_pow_mul_measureReal_le_two_pow_mul_covolume.
Sources
Uses 2
TheoremMinkowski's second theorem for the unit lattice#
There are units u 0, …, u (r - 1), where
r = rank K, with linearly independent logarithmic embeddings and
∏ i, ‖log u i‖₁ ≤ r! * regulator K, where ‖log x‖₁ is the ℓ¹ norm of the logarithmic
embedding of x. This is Minkowski's second theorem for the unit lattice and the ℓ¹ unit ball
logBall K, whose volume is 2 ^ r / r!.
TauCeti.NumberField.Units.exists_isMaxRank_prod_sum_abs_logEmbedding_le.{u_1} {K : Type u_1}
[Field K] [NumberField K] :
∃ u,
NumberField.Units.IsMaxRank u ∧
∏ i, ∑ w, |(NumberField.Units.logEmbedding K) (Additive.ofMul (u i)) w| ≤
↑(NumberField.Units.rank K).factorial * NumberField.Units.regulator K
Lean
Formalized in Tau Ceti as TauCeti.NumberField.Units.exists_isMaxRank_prod_sum_abs_logEmbedding_le.
Sources
Uses 2 · Used by 1
TheoremSiegel's lemma for a rational subspace, in the sup norm#
A nonzero subspace V of ℚ^ι
contains a nonzero integral point z whose sup norm is at most H(V) ^ (1 / k), where H(V) is
the absolute Euclidean height of V and k its dimension.
Submodule.exists_ne_zero_mem_intPoints_norm_le.{u_1} {ι : Type u_1} [Fintype ι] [LinearOrder ι]
{V : Submodule ℚ (ι → ℚ)} (hV : V ≠ ⊥) :
∃ z ∈ V.intPoints, z ≠ 0 ∧ ‖z‖ ≤ V.subspaceHeight ^ (↑(Module.finrank ℚ ↥V))⁻¹
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.