Power-saving lattice count in the number-field fundamental cone

A norm cutoff x is a dilation of the norm-one region by x^(1/degree). The boundary count therefore has exponent (degree-1)/degree.

theorem NairTenenbaum.smul_normLeOne (K : Type u_1) [Field K] [NumberField K] {t : ℝ} (ht : 0 < t) : t • NumberField.mixedEmbedding.fundamentalCone.normLeOne K = {x : NumberField.mixedEmbedding.mixedSpace K | x ∈ NumberField.mixedEmbedding.fundamentalCone K ∧ NumberField.mixedEmbedding.norm x ≤ t ^ Module.finrank ℚ K}

theorem NairTenenbaum.exists_normCone_lattice_power_error (K : Type u_1) [Field K] [NumberField K] {L : Submodule ℤ (NumberField.mixedEmbedding.mixedSpace K)} [DiscreteTopology ↥L] [IsZLattice ℝ L] {ι : Type u_2} [Finite ι] (b : Module.Basis ι ℤ ↥L) : ∃ (V : ℝ) (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), 1 ≤ x → |↑(Nat.card { a : ↥L // ↑a ∈ NumberField.mixedEmbedding.fundamentalCone K ∧ NumberField.mixedEmbedding.norm ↑a ≤ x }) - V * x| ≤ C * x ^ (↑(Module.finrank ℚ K - 1) / ↑(Module.finrank ℚ K))