Power-saving counts in an ideal class

The fundamental-cone lattice count counts principal ideals with a prescribed ideal divisor, up to the finite torsion-unit multiplicity. Multiplication by a representative of the inverse class converts this to each ideal class.

noncomputable def NairTenenbaum.numberFieldCountingExponent (K : Type u_1) [Field K] [NumberField K] : ℝ

The power-saving exponent in the number-field ideal-counting estimate.

Equations

• NairTenenbaum.numberFieldCountingExponent K = ↑(Module.finrank ℚ K - 1) / ↑(Module.finrank ℚ K)

theorem NairTenenbaum.numberFieldCountingExponent_nonneg (K : Type u_1) [Field K] [NumberField K] : 0 ≤ numberFieldCountingExponent K

theorem NairTenenbaum.numberFieldCountingExponent_lt_one (K : Type u_1) [Field K] [NumberField K] : numberFieldCountingExponent K < 1

noncomputable def NairTenenbaum.principalDivisorIdealCount (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (x : ℝ) : ℕ

The count of principal divisor ideals below the norm cutoff.

Equations

• NairTenenbaum.principalDivisorIdealCount K J x = Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑J ∣ ↑I ∧ Submodule.IsPrincipal ↑I ∧ ↑(Ideal.absNorm ↑I) ≤ x }

noncomputable def NairTenenbaum.idealClassNormCount (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (NumberField.RingOfIntegers K)) (x : ℝ) : ℕ

The count of ideals in a fixed class below the norm cutoff.

Equations

• NairTenenbaum.idealClassNormCount K C x = Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑(Ideal.absNorm ↑I) ≤ x ∧ ClassGroup.mk0 I = C }

theorem NairTenenbaum.idealSet_normCount_eq_lattice (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (x : ℝ) : Nat.card { a : ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J) // NumberField.mixedEmbedding.norm ↑a ≤ x } = Nat.card { a : ↥(NumberField.mixedEmbedding.idealLattice K ((FractionalIdeal.mk0 K) J)) // ↑a ∈ NumberField.mixedEmbedding.fundamentalCone K ∧ NumberField.mixedEmbedding.norm ↑a ≤ x }

theorem NairTenenbaum.exists_idealSet_normCount_power_error (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : ∃ (V : ℝ) (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), 1 ≤ x → |↑(Nat.card { a : ↑(NumberField.mixedEmbedding.fundamentalCone.idealSet K J) // NumberField.mixedEmbedding.norm ↑a ≤ x }) - V * x| ≤ C * x ^ numberFieldCountingExponent K

theorem NairTenenbaum.exists_principalDivisorIdealCount_power_error (K : Type u_1) [Field K] [NumberField K] (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : ∃ (V : ℝ) (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), 1 ≤ x → |↑(principalDivisorIdealCount K J x) - V * x| ≤ C * x ^ numberFieldCountingExponent K

theorem NairTenenbaum.idealClassNormCount_eq_principalDivisor (K : Type u_1) [Field K] [NumberField K] {C : ClassGroup (NumberField.RingOfIntegers K)} {J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hJ : ClassGroup.mk0 J = C⁻¹) (x : ℝ) : idealClassNormCount K C x = principalDivisorIdealCount K J (x * ↑(Ideal.absNorm ↑J))

theorem NairTenenbaum.exists_idealClassNormCount_power_error (K : Type u_1) [Field K] [NumberField K] (A : ClassGroup (NumberField.RingOfIntegers K)) : ∃ (V : ℝ) (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), 1 ≤ x → |↑(idealClassNormCount K A x) - V * x| ≤ C * x ^ numberFieldCountingExponent K