Linear ideal counts and the exact abscissa of the trivial ideal weight

Mathlib's NumberField.Ideal.tendsto_norm_le_div_atTop₀ says that the number of nonzero integral ideals of 𝓞 K of absolute norm at most x is asymptotic to ρ x, with ρ the positive residue of the Dedekind zeta function. This file turns that single asymptotic into the two-sided linear bounds that every later estimate of the roadmap counts against, and then spends them on the exact abscissa of absolute convergence of the trivial ideal weight.

Both directions are needed. Convergence uses the upper bound alone: it makes the partial sums of the norm coefficients O(n), so Mathlib's LSeriesSummable_of_sum_norm_bigO gives absolute convergence on Re s > 1. Divergence at s = 1 uses both bounds together, to estimate the mass of a block N < n ≤ m N of fixed ratio m as a difference of endpoint counts: the lower bound at the right endpoint m N and the upper bound at the left endpoint N leave the block at least lower * m N - upper * N of coefficient mass, so the terms ‖a n‖ / n add up to at least lower - upper / m, which is at least lower / 2 once m ≥ 2 * upper / lower, while the blocks of a convergent series of nonnegative terms must become arbitrarily small.

Main definitions

• TauCeti.IdealCountingLinearBounds K packages positive constants lower and upper with the two-sided bound lower * x ≤ #{I ≠ 0 | N(I) ≤ x} ≤ upper * x, valid from cutoff 1 on.
• TauCeti.card_primePowersLE_isBigO transfers the upper ideal-count bound to the number of prime-power ideals at most x.

Main results

• TauCeti.idealCount_linearBounds: such a package exists for every number field.
• TauCeti.abscissaOfAbsConv_normCoeff_one: the abscissa of absolute convergence of the trivial ideal weight is exactly 1; TauCeti.LSeriesSummable_normCoeff_one_iff is the sharp convergence criterion.
• TauCeti.abscissaOfAbsConv_dedekindZetaCoeff and TauCeti.LSeriesSummable_dedekindZetaCoeff_iff are the same two statements for TauCeti.dedekindZetaCoeff, the coefficient system Mathlib's NumberField.dedekindZeta is the LSeries of. That system counts all integral ideals, so it differs from the trivial norm coefficients at n = 0 and the two statements are related only through the n ≠ 0 congruence LSeries.abscissaOfAbsConv_congr.
• TauCeti.summable_idealTerm_of_bounded_of_one_lt_re: a uniformly bounded weight has an absolutely convergent ideal-indexed Dirichlet series on Re s > 1, and TauCeti.summable_idealTerm_of_unitary_of_one_lt_re is its unitary specialization.
• TauCeti.idealAbscissaOfAbsConv_lt_re_of_bounded: the same hypothesis places the ideal-indexed abscissa of absolute convergence strictly below every Re s > 1.

Implementation notes

The counting function is Mathlib's own Nat.card {I : (Ideal (𝓞 K))⁰ // (Ideal.absNorm (I : Ideal (𝓞 K)) : ℝ) ≤ x}, written out rather than abbreviated, so that the bounds apply to NumberField.Ideal.tendsto_norm_le_div_atTop₀ without a translation lemma. The inclusive real cutoff is the one fixed by the conventions table of the roadmap.

TauCeti.NumberTheory.EffectiveBounds.IdealCount proves the effective bound #{I ≠ 0 | N(I) ≤ x} ≤ x² 2^[K:ℚ], with an explicit constant but the wrong exponent; it cannot prove convergence at Re s > 1, and it has no lower bound at all.

Relationship to other estimates

The unweighted prime-power cardinality estimate is separate from the weighted higher-prime-power estimates in HigherPrimePowers.lean. The abscissa results above depend only on the two-sided linear ideal counts, not on the analytic continuation of the Dedekind zeta function or its pole at s = 1.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII.
• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapters II--III.

Finiteness and monotonicity of the ideal count

theorem TauCeti.finite_setOf_absNorm_real_le (K : Type u_1) [Field K] [NumberField K] (x : ℝ) : {I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) | ↑(Ideal.absNorm ↑I) ≤ x}.Finite

The nonzero integral ideals of absolute norm at most a real cutoff form a finite set.

theorem TauCeti.card_absNorm_real_le_mono (K : Type u_1) [Field K] [NumberField K] {x y : ℝ} (h : x ≤ y) : Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑(Ideal.absNorm ↑I) ≤ x } ≤ Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑(Ideal.absNorm ↑I) ≤ y }

The number of nonzero integral ideals of bounded absolute norm is monotone in the cutoff.

theorem TauCeti.one_le_card_absNorm_real_le (K : Type u_1) [Field K] [NumberField K] {x : ℝ} (hx : 1 ≤ x) : 1 ≤ Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑(Ideal.absNorm ↑I) ≤ x }

From cutoff 1 on there is at least one nonzero integral ideal of bounded absolute norm, namely the unit ideal.

Two-sided linear bounds

structure TauCeti.IdealCountingLinearBounds (K : Type u_1) [Field K] [NumberField K] : Type

Two-sided positive linear bounds for the ideal-counting function of a number field K: constants lower and upper, both positive, with lower * x ≤ #{I ≠ 0 | N(I) ≤ x} ≤ upper * x for every cutoff x ≥ 1.

Only the existence of such a package matters; TauCeti.idealCount_linearBounds provides it from Mathlib's asymptotic NumberField.Ideal.tendsto_norm_le_div_atTop₀. Both inequalities are used: the upper one alone gives absolute convergence to the right of 1, and the two together give divergence at 1.

• lower : ℝ

  The constant in the lower bound.

• upper : ℝ

  The constant in the upper bound.

• lower_pos : 0 < self.lower

  The constant in the lower bound is positive.

• upper_pos : 0 < self.upper

  The constant in the upper bound is positive.

• le_card (x : ℝ) (hx : 1 ≤ x) : self.lower * x ≤ ↑(Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑(Ideal.absNorm ↑I) ≤ x })

  The lower bound, valid from cutoff 1 on.

• card_le (x : ℝ) (hx : 1 ≤ x) : ↑(Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑(Ideal.absNorm ↑I) ≤ x }) ≤ self.upper * x

  The upper bound, valid from cutoff 1 on.

theorem TauCeti.idealCount_linearBounds (K : Type u_1) [Field K] [NumberField K] : Nonempty (IdealCountingLinearBounds K)

Two-sided linear ideal counts. The number of nonzero integral ideals of absolute norm at most x is bounded above and below by positive multiples of x, for every cutoff x ≥ 1.

Both constants come from Mathlib's asymptotic NumberField.Ideal.tendsto_norm_le_div_atTop₀, whose limit is positive by NumberField.dedekindZeta_residue_pos; below the threshold produced by that limit the bounds are secured by the unit ideal and by monotonicity of the count.

theorem TauCeti.card_primePowersLE_isBigO (K : Type u_2) [Field K] [NumberField K] : (fun (x : ℝ) => ↑(primePowersLE K x).card) =O[Filter.atTop] fun (x : ℝ) => x

The number of prime-power ideals with absolute norm at most x is O(x).

Partial sums of the trivial norm coefficients

theorem TauCeti.norm_normCoeff_one (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : ‖((normCoeff K) 1) n‖ = ↑(normFiber K n).card

The trivial ideal weight has norm coefficient the number of nonzero integral ideals of the given absolute norm, so its absolute value is that count.

theorem TauCeti.UnitaryIdealWeight.norm_normCoeff_le_norm_normCoeff_one (K : Type u_1) [Field K] [NumberField K] (χ : UnitaryIdealWeight K) (n : ℕ) : ‖((normCoeff K) χ.toIdealArithmeticFunction) n‖ ≤ ‖((normCoeff K) 1) n‖

The norm coefficients of a unitary weight are bounded in modulus by those of the trivial weight, which count the ideals of each norm.

theorem TauCeti.sum_norm_normCoeff_one (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : ∑ k ∈ Finset.Icc 1 n, ‖((normCoeff K) 1) k‖ = ↑(Nat.card { I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) // ↑(Ideal.absNorm ↑I) ≤ ↑n })

The partial sums of the trivial norm coefficients are the ideal counts. Summing the norm coefficients of the trivial ideal weight over 1 ≤ k ≤ n counts the nonzero integral ideals of absolute norm at most n, because the absolute-norm fibres partition them.

The exact abscissa of the trivial ideal weight

theorem TauCeti.isBigO_sum_norm_normCoeff_one (K : Type u_1) [Field K] [NumberField K] : (fun (n : ℕ) => ∑ k ∈ Finset.Icc 1 n, ‖((normCoeff K) 1) k‖) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ 1

The upper linear ideal count makes the partial sums of the trivial norm coefficients O(n).

theorem TauCeti.abscissaOfAbsConv_normCoeff_one_le (K : Type u_1) [Field K] [NumberField K] : LSeries.abscissaOfAbsConv ⇑((normCoeff K) 1) ≤ 1

The Dirichlet series of the trivial ideal weight converges absolutely on Re s > 1.

theorem TauCeti.not_LSeriesSummable_normCoeff_one (K : Type u_1) [Field K] [NumberField K] : ¬LSeriesSummable (⇑((normCoeff K) 1)) 1

Divergence at s = 1. The Dirichlet series of the trivial ideal weight does not converge at s = 1.

The two-sided linear ideal counts are what force this: by TauCeti.lower_div_two_le_sum_Ioc_norm_term every block N < n ≤ m N of fixed ratio m ≥ 2 * upper / lower carries mass at least lower / 2, whereas the blocks of a convergent series of nonnegative terms become arbitrarily small.

The exact abscissa, and its Dedekind zeta form

@[simp]

theorem TauCeti.abscissaOfAbsConv_normCoeff_one (K : Type u_1) [Field K] [NumberField K] : LSeries.abscissaOfAbsConv ⇑((normCoeff K) 1) = 1

The exact abscissa of absolute convergence of the trivial ideal weight is 1.

The upper linear ideal count on its own supplies convergence on Re s > 1, and the two counts together supply divergence at s = 1; no analytic continuation of the Dedekind zeta function, and no knowledge of its pole, is involved.

@[simp]

theorem TauCeti.LSeriesSummable_normCoeff_one_iff (K : Type u_1) [Field K] [NumberField K] {s : ℂ} : LSeriesSummable (⇑((normCoeff K) 1)) s ↔ 1 < s.re

The Dirichlet series of the trivial ideal weight converges exactly on the open half-plane Re s > 1; on the line Re s = 1 it diverges.

theorem TauCeti.summable_idealTerm_one_iff {K : Type u_2} [Field K] [NumberField K] {s : ℂ} : Summable (idealTerm K 1 s) ↔ 1 < s.re

The ideal-indexed Dirichlet series of the trivial ideal weight converges absolutely exactly on Re s > 1.

theorem TauCeti.summable_idealTerm_of_bounded_of_one_lt_re {K : Type u_2} [Field K] [NumberField K] {f : IdealArithmeticFunction K} {C : ℝ} (hf : ∀ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), ‖f I‖ ≤ C) {s : ℂ} (hs : 1 < s.re) : Summable (idealTerm K f s)

A uniformly bounded weight converges wherever the trivial weight does. If every value of f on a nonzero integral ideal has modulus at most C, its ideal-indexed Dirichlet series converges absolutely on Re s > 1.

The bound may be any nonnegative real — a negative C makes the hypothesis unsatisfiable, since ‖f I‖ is a norm — and no C = 1 normalisation is wanted, since a weight is often bounded by something other than 1 without being rescaled. The unitary case — a Dirichlet or Galois character, of modulus 1 at the good primes and 0 at the bad ones — is C = 1, and is packaged as summable_idealTerm_of_unitary_of_one_lt_re. Stating the hypothesis here as a bound rather than as unitarity is what lets the vanishing at the bad primes pass without a special case.

Only one direction holds, unlike summable_idealTerm_one_iff: a weight that vanishes identically is bounded by every nonnegative C and converges everywhere.

theorem TauCeti.summable_idealTerm_of_unitary_of_one_lt_re {K : Type u_2} [Field K] [NumberField K] (χ : UnitaryIdealWeight K) {s : ℂ} (hs : 1 < s.re) : Summable (idealTerm K χ.toIdealArithmeticFunction s)

A unitary weight converges on Re s > 1. The specialization of summable_idealTerm_of_bounded_of_one_lt_re at C = 1, through TauCeti.UnitaryIdealWeight.norm_le_one: a unitary weight has modulus 1 on the good ideals and vanishes on the rest, so it is bounded by 1 on all of them and the caller is left no case split.

This is the form the Euler-product code consumes, its hasProd_eulerFactor asking for exactly a Summable (idealTerm K · s) hypothesis on the weight's passage to IdealArithmeticFunction.

theorem TauCeti.idealAbscissaOfAbsConv_lt_re_of_bounded {K : Type u_2} [Field K] [NumberField K] {f : IdealArithmeticFunction K} {C : ℝ} (hf : ∀ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), ‖f I‖ ≤ C) {s : ℂ} (hs : 1 < s.re) : idealAbscissaOfAbsConv K f < ↑s.re

A uniformly bounded weight has ideal-indexed abscissa below every Re s > 1. This is the form in which summable_idealTerm_of_bounded_of_one_lt_re feeds results stated strictly to the right of TauCeti.idealAbscissaOfAbsConv, such as the termwise differentiation of the Euler logarithm: absolute convergence at a point between 1 and Re s bounds the abscissa.

@[simp]

theorem TauCeti.abscissaOfAbsConv_dedekindZetaCoeff (K : Type u_1) [Field K] [NumberField K] : (LSeries.abscissaOfAbsConv fun (n : ℕ) => ↑(dedekindZetaCoeff K n)) = 1

The Dedekind zeta series has abscissa of absolute convergence 1.

@[simp]

theorem TauCeti.LSeriesSummable_dedekindZetaCoeff_iff (K : Type u_1) [Field K] [NumberField K] {s : ℂ} : LSeriesSummable (fun (n : ℕ) => ↑(dedekindZetaCoeff K n)) s ↔ 1 < s.re

The Dedekind zeta series converges exactly on the open half-plane Re s > 1.