Partitioning the partial Dirichlet series over a set of primes

Let K be a number field. Mathlib's partial Dirichlet series NumberField.Set.primeIdealZetaSum sums 𝔑𝔭 ^ (-s) over a set of nonzero prime ideals of 𝓞 K, and this file cuts that sum along a partition of the primes. The sum is additive along a finite pairwise disjoint union, given summability on each piece, and subadditive along an arbitrary union of two sets. For a finite set S of primes it also compares the sum over the complement Sᶜ with the sum over all primes: deleting S never increases the sum, and for s ≥ 0 it lowers it by at most the number of primes deleted.

Main results

• NumberField.Set.primeIdealZetaSum_biUnion_of_pairwiseDisjoint: given summability on each piece, the sum over a finite pairwise disjoint union is the sum of the sums over the pieces.
• NumberField.Set.primeIdealZetaSum_union_le: given summability on both sets, the sum over a union is at most the sum of the two sums.
• NumberField.Set.primeIdealZetaSum_le_add_symmDiff: given summability over T and over S ∆ T, the sum over S exceeds the sum over T by at most the sum over S ∆ T.
• NumberField.Set.primeIdealZetaSum_compl_le_univ_of_finite: deleting a finite set of primes does not increase the sum.
• NumberField.Set.primeIdealZetaSum_univ_sub_compl_le_ncard_of_finite: for s ≥ 0, deleting a finite set of primes lowers the sum by at most S.ncard.

Implementation notes

primeIdealZetaSum S s is a tsum, so it takes the value 0 on a family that is not summable. That junk value is not additive along a partition, which is why the disjoint-union identity carries a summability hypothesis.

The same junk value, together with Set.ncard being 0 on an infinite set, makes finiteness of S essential to the two complement statements rather than a convenience, and both fail without it. Take S = {𝔭₀}ᶜ, which is itself infinite and whose complement {𝔭₀} is a single prime. At s = 0 every term is 1, so the sum over all primes diverges and is read as 0 while the sum over {𝔭₀} is 1: the first bound reads 1 ≤ 0. At s = 2 both sums converge while S.ncard is read as 0, so the second bound reads (∑' 𝔭, 𝔑𝔭 ^ (-2)) - 𝔑𝔭₀ ^ (-2) ≤ 0, whose left-hand side is the positive sum over the primes other than 𝔭₀.

References

The corresponding statements for a source-local primeIdealZetaSum over Set (Ideal (𝓞 K)) are primeIdealZetaSum_biUnion_of_pairwiseDisjoint, primeIdealZetaSum_union_of_disjoint and primeIdealZetaSum_le_of_subset in CebotarevDensity/Density.lean of CBirkbeck/chebotarev-density (Apache-2.0, Birkbeck--Brasca) at commit 8575c9df1ae0a61120ab5c964c7911414254bec7. Those are gated on 1 < s; the statements here take the weaker hypotheses that each proof actually uses — summability on the participating pieces for the disjoint-union identity, finiteness for the two complement bounds.

theorem NumberField.Set.primeIdealZetaSum_biUnion_of_pairwiseDisjoint {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (t : Finset ι) (g : ι → Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (hg : (↑t).PairwiseDisjoint g) {s : ℝ} (hsum : ∀ i ∈ t, Summable fun (𝔭 : ↑(g i)) => ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) : primeIdealZetaSum (⋃ i ∈ t, g i) s = ∑ i ∈ t, primeIdealZetaSum (g i) s

The sum is additive along a finite disjoint union. The sum over a finite pairwise disjoint union of sets of primes is the sum of the sums over the pieces.

Summability is asked for on each participating piece rather than on all primes at once: a finite union of summable pieces is summable even at an s where the full prime series diverges, and the identity holds there too.

theorem NumberField.Set.primeIdealZetaSum_union_le {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {s : ℝ} (hS : Summable fun (𝔭 : ↑S) => ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) (hT : Summable fun (𝔭 : ↑T) => ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) : primeIdealZetaSum (S ∪ T) s ≤ primeIdealZetaSum S s + primeIdealZetaSum T s

The sum is subadditive along a union. Given summability over S and over T, the sum over S ∪ T is at most the sum over S plus the sum over T.

theorem NumberField.Set.primeIdealZetaSum_le_add_symmDiff {K : Type u_1} [Field K] [NumberField K] {S T : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} {s : ℝ} (hT : Summable fun (𝔭 : ↑T) => ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) (hST : Summable fun (𝔭 : ↑(symmDiff S T)) => ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) : primeIdealZetaSum S s ≤ primeIdealZetaSum T s + primeIdealZetaSum (symmDiff S T) s

Changing a set by a small symmetric difference changes the sum by little. Given summability over T and over S ∆ T, the sum over S is at most the sum over T plus the sum over S ∆ T.

theorem NumberField.Set.primeIdealZetaSum_compl_le_univ_of_finite {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} (hS : S.Finite) (s : ℝ) : primeIdealZetaSum Sᶜ s ≤ primeIdealZetaSum Set.univ s

Deleting a finite set of primes does not increase the sum.

theorem NumberField.Set.primeIdealZetaSum_univ_sub_compl_le_ncard_of_finite {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} (hS : S.Finite) {s : ℝ} (hs : 0 ≤ s) : primeIdealZetaSum Set.univ s - primeIdealZetaSum Sᶜ s ≤ ↑S.ncard

A finite set of primes costs at most its number. Deleting a finite set S of primes from the all-prime sum lowers it by at most S.ncard, uniformly in s ≥ 0.