Regrouping an ideal-indexed Dirichlet series by absolute norm

An TauCeti.IdealArithmeticFunction K has two Dirichlet series attached to it: the series indexed by the nonzero integral ideals of 𝓞 K, whose terms are TauCeti.idealTerm, and the Mathlib LSeries of the regrouped coefficients TauCeti.normCoeff. This file proves that the second is obtained from the first by summing over the finite absolute-norm fibres, so that absolute convergence of the ideal-indexed series transfers to the LSeries together with the value of the sum.

Main definitions

• TauCeti.idealTerm f s I is the term f I / N(I) ^ s of the ideal-indexed Dirichlet series.
• TauCeti.idealAbscissaOfAbsConv f is the abscissa of absolute convergence of that series, the ideal-indexed analogue of Mathlib's LSeries.abscissaOfAbsConv.

Main results

• TauCeti.regroupByNorm: if the ideal-indexed series has sum L at s, then so does the LSeries of TauCeti.normCoeff f; TauCeti.LSeriesSummable_normCoeff and TauCeti.LSeries_normCoeff are the summability and value statements it packages.
• TauCeti.summable_log_absNorm_mul_norm_idealTerm_of_re_lt_re: weighting the ideal terms by log N(I) keeps them summable strictly to the right of a point of absolute convergence.
• TauCeti.abscissaOfAbsConv_normCoeff_le: consequently the grouped abscissa of absolute convergence is at most the ideal-indexed one.
• TauCeti.summable_idealTerm_of_norm_normCoeff_eq_sum_norm: the converse holds whenever no cancellation occurs inside a norm fibre. TauCeti.summable_idealTerm_of_nonneg and TauCeti.idealAbscissaOfAbsConv_eq_abscissaOfAbsConv specialize it to the case where every individual ideal summand is nonnegative, where moreover the two abscissae agree.

Implementation notes

The regrouping is an instance of Mathlib's HasSum.tsum_fiberwise along the absolute norm fun I ↦ Ideal.absNorm (I : Ideal (𝓞 K)), whose fibres are the finite sets TauCeti.normFiber K n. Absolute convergence of the ideal-indexed series is expressed as plain Summable, which for a complex-valued family is unconditional convergence and hence absolute convergence; no rearrangement hypothesis is therefore needed for the transfer.

The converse is proved through summable_partition applied to the norms of the terms. All it needs about f is that the norm of each grouped coefficient is the sum of the norms over its fibre — the absence of cancellation inside the fibre. Nonnegativity of every ideal summand is one way to secure that, through TauCeti.norm_normCoeff_eq_sum_norm_of_nonneg; it is the step that fails under cancellation, as the rejection test TauCeti.exists_forall_normCoeff_nonneg_not_forall_nonneg records. That test is a statement about TauCeti.normCoeff alone, so it lives with that definition rather than here.

Roadmap role

This is Layer 1.2 of TauCetiRoadmap/ArithmeticDirichletSeries/README.md; the required worked example 9 accompanies it in TauCeti/NumberTheory/ArithmeticDirichletSeries/NormCoeff.lean. The exact value of the abscissa for the trivial weight is deliberately not proved here: its divergence input is the Layer 5 ideal count of TauCeti/NumberTheory/ArithmeticDirichletSeries/Estimates.lean.

References

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

The ideal-indexed term

noncomputable def TauCeti.idealTerm (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (s : ℂ) (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : ℂ

The term of the ideal-indexed Dirichlet series of f at the nonzero integral ideal I: the value f I divided by the s-th complex power of the absolute norm of I. The zero ideal is absent from the carrier (Ideal (𝓞 K))⁰, so no n = 0 convention is needed here, in contrast with Mathlib's LSeries.term.

Equations

• TauCeti.idealTerm K f s I = f I / ↑(Ideal.absNorm ↑I) ^ s

theorem TauCeti.idealTerm_def (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (s : ℂ) (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : idealTerm K f s I = f I / ↑(Ideal.absNorm ↑I) ^ s

Defining equation of TauCeti.idealTerm.

@[simp]

theorem TauCeti.norm_idealTerm (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (s : ℂ) (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : ‖idealTerm K f s I‖ = ‖f I‖ / ↑(Ideal.absNorm ↑I) ^ s.re

The absolute value of an ideal term depends on s only through its real part.

theorem TauCeti.norm_idealTerm_le_of_re_le_re (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) {s s' : ℂ} (h : s.re ≤ s'.re) (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : ‖idealTerm K f s' I‖ ≤ ‖idealTerm K f s I‖

Ideal terms decrease in absolute value as the real part of s grows, because every nonzero integral ideal has absolute norm at least one.

theorem TauCeti.summable_idealTerm_of_re_le_re (K : Type u_1) [Field K] [NumberField K] {f : IdealArithmeticFunction K} {s s' : ℂ} (h : s.re ≤ s'.re) (hf : Summable (idealTerm K f s)) : Summable (idealTerm K f s')

Absolute convergence of the ideal-indexed series propagates to the right.

theorem TauCeti.summable_idealTerm_iff_of_re_eq_re (K : Type u_1) [Field K] [NumberField K] {f : IdealArithmeticFunction K} {s s' : ℂ} (h : s.re = s'.re) : Summable (idealTerm K f s) ↔ Summable (idealTerm K f s')

Absolute convergence of the ideal-indexed series depends on s only through its real part.

theorem TauCeti.summable_log_absNorm_mul_norm_idealTerm_of_re_lt_re (K : Type u_1) [Field K] [NumberField K] {f : IdealArithmeticFunction K} {s s' : ℂ} (h : s.re < s'.re) (hs : Summable (idealTerm K f s)) : Summable fun (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => Real.log ↑(Ideal.absNorm ↑I) * ‖idealTerm K f s' I‖

Log-weighted ideal terms stay summable strictly to the right. If the ideal-indexed Dirichlet series of f converges absolutely at s, then weighting each term by log N(I) leaves it summable at every s' with Re s < Re s'.

The strict inequality is what separates this from summable_idealTerm_of_re_le_re, which propagates unweighted convergence along Re s ≤ Re s': the logarithmic weight can destroy summability at Re s' = Re s. This is the ideal-indexed counterpart of Mathlib's LSeriesSummable_logMul_of_lt_re, and the logarithmic weight is what appears when the terms are differentiated in s.

Regrouping

theorem TauCeti.term_normCoeff_eq_sum_normFiber (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (s : ℂ) (n : ℕ) : LSeries.term (⇑((normCoeff K) f)) s n = ∑ I ∈ normFiber K n, idealTerm K f s I

The n-th term of the regrouped LSeries is the finite sum of the ideal terms over the absolute-norm fibre of n.

theorem TauCeti.regroupByNorm (K : Type u_1) [Field K] [NumberField K] {f : IdealArithmeticFunction K} {s L : ℂ} (h : HasSum (idealTerm K f s) L) : LSeriesHasSum (⇑((normCoeff K) f)) s L

Regrouping by absolute norm. If the Dirichlet series indexed by the nonzero integral ideals converges absolutely at s with sum L, then the Mathlib LSeries of the regrouped coefficients TauCeti.normCoeff f converges absolutely at s with the same sum.

Absolute convergence of the ideal-indexed series is the hypothesis HasSum, which for a complex-valued family is unconditional. No hypothesis on the individual ideal summands is needed; compare TauCeti.summable_idealTerm_of_nonneg for the converse, which does need one.

theorem TauCeti.LSeriesSummable_normCoeff (K : Type u_1) [Field K] [NumberField K] {f : IdealArithmeticFunction K} {s : ℂ} (h : Summable (idealTerm K f s)) : LSeriesSummable (⇑((normCoeff K) f)) s

Absolute convergence of the ideal-indexed Dirichlet series implies that of the regrouped LSeries.

theorem TauCeti.LSeries_normCoeff (K : Type u_1) [Field K] [NumberField K] {f : IdealArithmeticFunction K} {s : ℂ} (h : Summable (idealTerm K f s)) : LSeries (⇑((normCoeff K) f)) s = ∑' (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), idealTerm K f s I

Where the ideal-indexed Dirichlet series converges absolutely, the regrouped LSeries has the same value.

The ideal-indexed abscissa of absolute convergence

noncomputable def TauCeti.idealAbscissaOfAbsConv (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) : EReal

The abscissa of absolute convergence of the Dirichlet series indexed by the nonzero integral ideals: the ideal-indexed analogue of Mathlib's LSeries.abscissaOfAbsConv.

Equations

• TauCeti.idealAbscissaOfAbsConv K f = sInf (Real.toEReal '' {x : ℝ | Summable (TauCeti.idealTerm K f ↑x)})

theorem TauCeti.idealAbscissaOfAbsConv_def (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) : idealAbscissaOfAbsConv K f = sInf (Real.toEReal '' {x : ℝ | Summable (idealTerm K f ↑x)})

Defining equation of TauCeti.idealAbscissaOfAbsConv.

theorem TauCeti.exists_summable_idealTerm_of_idealAbscissaOfAbsConv_lt_re (K : Type u_1) [Field K] [NumberField K] {f : IdealArithmeticFunction K} {s : ℂ} (hs : idealAbscissaOfAbsConv K f < ↑s.re) : ∃ (y : ℝ), Summable (idealTerm K f ↑y) ∧ y < s.re

A point of absolute convergence strictly to the left. Strictly to the right of the ideal-indexed abscissa of absolute convergence there is a real point, still strictly to the left, at which the ideal-indexed series converges absolutely.

This is the form in which the abscissa is consumed by estimates that need room to the left, such as the logarithmic weights produced by differentiation.

theorem TauCeti.summable_idealTerm_of_idealAbscissaOfAbsConv_lt_re (K : Type u_1) [Field K] [NumberField K] {f : IdealArithmeticFunction K} {s : ℂ} (hs : idealAbscissaOfAbsConv K f < ↑s.re) : Summable (idealTerm K f s)

The ideal-indexed series converges absolutely strictly to the right of its abscissa.

theorem TauCeti.idealAbscissaOfAbsConv_le (K : Type u_1) [Field K] [NumberField K] {f : IdealArithmeticFunction K} {s : ℂ} (h : Summable (idealTerm K f s)) : idealAbscissaOfAbsConv K f ≤ ↑s.re

A point of absolute convergence bounds the ideal-indexed abscissa.

theorem TauCeti.abscissaOfAbsConv_normCoeff_le (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) : LSeries.abscissaOfAbsConv ⇑((normCoeff K) f) ≤ idealAbscissaOfAbsConv K f

The grouped abscissa is at most the ideal-indexed one. Regrouping can only improve convergence, since cancellation inside a norm fibre is never undone.

The converse, in the absence of cancellation inside norm fibres

theorem TauCeti.idealTerm_nonneg (K : Type u_1) [Field K] [NumberField K] {f : IdealArithmeticFunction K} {I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (h : 0 ≤ f I) (x : ℝ) : 0 ≤ idealTerm K f (↑x) I

At a real point, an ideal term of a nonnegative ideal arithmetic function is nonnegative.

theorem TauCeti.summable_idealTerm_of_norm_normCoeff_eq_sum_norm (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (hf : ∀ (n : ℕ), ‖((normCoeff K) f) n‖ = ∑ I ∈ normFiber K n, ‖f I‖) {s : ℂ} (h : LSeriesSummable (⇑((normCoeff K) f)) s) : Summable (idealTerm K f s)

The converse regrouping, in the absence of cancellation inside norm fibres. If the absolute value of every grouped coefficient is the sum of the absolute values of f over the corresponding fibre — that is, if adding up a fibre loses no absolute value — then absolute convergence of the regrouped LSeries implies absolute convergence of the ideal-indexed series.

This is the hypothesis the proof actually uses: it holds for a nonnegative f, by TauCeti.norm_normCoeff_eq_sum_norm_of_nonneg, but equally for a uniformly negative one or, more generally, whenever the values of f over each fibre share a common phase. Nonnegativity of the grouped coefficients TauCeti.normCoeff f does not suffice; see TauCeti.exists_forall_normCoeff_nonneg_not_forall_nonneg.

theorem TauCeti.summable_idealTerm_of_nonneg (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (hf : ∀ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), 0 ≤ f I) {s : ℂ} (h : LSeriesSummable (⇑((normCoeff K) f)) s) : Summable (idealTerm K f s)

The converse regrouping, under nonnegativity of every ideal summand. If every value of f is a nonnegative real number, then absolute convergence of the regrouped LSeries implies absolute convergence of the ideal-indexed series.

This is the special case of TauCeti.summable_idealTerm_of_norm_normCoeff_eq_sum_norm in which nonnegativity rules out cancellation. Nonnegativity of the grouped coefficients TauCeti.normCoeff f does not suffice; see TauCeti.exists_forall_normCoeff_nonneg_not_forall_nonneg.

theorem TauCeti.idealAbscissaOfAbsConv_eq_abscissaOfAbsConv (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (hf : ∀ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), 0 ≤ f I) : idealAbscissaOfAbsConv K f = LSeries.abscissaOfAbsConv ⇑((normCoeff K) f)

For a nonnegative ideal arithmetic function the two abscissae of absolute convergence agree: there is no cancellation inside a norm fibre to exploit.