Finite-radius counting for the algebraic integers. The input is a short independent integral basis over the reals; it is not required to generate the ring of integers over ℤ.

noncomputable def CCDN.numberFieldLatticeBoxConstant (n : ℕ) (C : ℝ) : ℝ

A dimension-only coefficient for the box count when the independent integral vectors have norm at most C times the box radius.

Equations

• CCDN.numberFieldLatticeBoxConstant n C = 2 ^ n * 2 ^ n * (2 * √↑n + ↑n * C) ^ n

theorem CCDN.numberFieldLatticeBoxConstant_nonneg (n : ℕ) {C : ℝ} (hC : 0 ≤ C) : 0 ≤ numberFieldLatticeBoxConstant n C

The box-count constant numberFieldLatticeBoxConstant n C is nonnegative for C ≥ 0.

theorem CCDN.boundedSquareNormTranslationClasses_count_of_relative_short_basis (K : Type u_1) [Field K] [NumberField K] {ι : Type u_2} [Finite ι] (b : Module.Basis ι ℝ (NumberField.mixedEmbedding.euclidean.mixedSpace K)) (hb : ∀ (i : ι), b i ∈ NumberField.mixedEmbedding.euclidean.integerLattice K) {B C : ℝ} (hB : 1 ≤ B) (hC : 0 ≤ C) (hnorm : ∀ (i : ι), ‖b i‖ ≤ C * B) : ↑(boundedSquareNormTranslationClasses K B).card * √|↑(NumberField.discr K)| ≤ numberFieldLatticeBoxConstant (Module.finrank ℚ K) C * 2 ^ Module.finrank ℚ K * B ^ (Module.finrank ℚ K - 1)

Dividing by short integer translates gives the expected one-dimensional saving for translation classes.