Abel summation for norm-indexed summatory functions

Mathlib's sum_mul_eq_sub_sub_integral_mul is Abel summation for a sequence indexed by the natural numbers. Every counting argument of the arithmetic-Dirichlet-series roadmap instead sums a weight over a carrier indexed by ideals or by height-one primes, cut off inclusively by the absolute norm. This file supplies the bridge: the weight is regrouped into its norm fibres, Mathlib's identity is applied to the resulting sequence, and the answer is read back as an equation between TauCeti.summatory functions.

The bridge is stated for a general Northcott index N : ι → ℕ, because Layer 6 uses it for both the ideal carrier and the prime carrier. The integral runs over the half-open interval Set.Ioc, so each boundary term is counted exactly once, as the roadmap's conventions table demands.

Main results

• TauCeti.summatory_mul_eq_sub_sub_integral_mul: Abel summation between two nonnegative real cutoffs for a weight of the form i ↦ w i * g (N i).
• TauCeti.summatory_mul_eq_sub_integral_mul_of_le: Abel summation from a real lower bound.
• TauCeti.idealSummatory_mul_eq_sub_integral_mul: the cutoff-1 form for nonzero ideals.
• TauCeti.primeSummatory_mul_eq_sub_integral_mul: the cutoff-2 form for the height-one primes of a number field.
• TauCeti.norm_summatory_mul_cpow_le_of_summatory_le: an imaginary-power twist preserves a positive power bound for partial sums, with an explicit constant.
• TauCeti.integrableOn_mul_summatory: a summatory function times an integrable factor is integrable on a compact interval, so the integrals above are genuine.
• TauCeti.summatory_mul_le_of_summatory_le and TauCeti.tsum_mul_le_of_summatory_le: for a nonnegative nonincreasing g and a carrier whose indices all have N-value at least a ≥ 0, an upper bound C on the partial sums of w gives the upper bound C * g a for the twisted partial sums and series. This is how an eventual comparison of counting functions becomes a comparison of Dirichlet series uniform in s.
• TauCeti.primeTheta_eq_log_mul_primeCount_sub_integral and TauCeti.primeCount_eq_primeTheta_div_log_add_integral: the two exact Abel identities relating the roadmap's weighted prime counts, ϑ(x) = π(x) log x - ∫_2^x π(t)/t dt and π(x) = ϑ(x)/log x + ∫_2^x ϑ(t)/(t log²t) dt. Both hold for every real cutoff; below 2 all three terms vanish.

Roadmap role

This is Layer 6.1 of TauCetiRoadmap/ArithmeticDirichletSeries/README.md: Mathlib's exact finite identity is consumed, not restated, and only the norm-indexed bridges are added. The two prime identities are the finite input to Layer 6.2, which turns ϑ(x) ∼ δx into π(x) ∼ δ Li(x) by estimating the integrals appearing here.

References

• H. Davenport, Multiplicative Number Theory, Chapter 1.
• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter I.2.

Regrouping a weight into its norm fibres

Abel summation over a Northcott carrier

theorem TauCeti.summatory_mul_eq_sub_sub_integral_mul {ι : Type u_1} (N : ι → ℕ) [Northcott N] {𝕜 : Type u_2} [RCLike 𝕜] (w : ι → 𝕜) {g : ℝ → 𝕜} {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hg_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ g t) (hg_int : MeasureTheory.IntegrableOn (deriv g) (Set.Icc a b) MeasureTheory.volume) : summatory N (fun (i : ι) => w i * g ↑(N i)) b - summatory N (fun (i : ι) => w i * g ↑(N i)) a = g b * summatory N w b - g a * summatory N w a - ∫ (t : ℝ) in Set.Ioc a b, deriv g t * summatory N w t

Abel summation for a norm-indexed summatory function. For a weight w on the index type and a function g differentiable on [a, b], the summatory function of the twisted weight i ↦ w i * g (N i) between the inclusive cutoffs a and b is the boundary term g b · A(b) - g a · A(a) minus the integral of g' · A, where A = summatory N w.

This is Mathlib's sum_mul_eq_sub_sub_integral_mul read through the norm fibres of N.

theorem TauCeti.summatory_mul_eq_sub_integral_mul_of_le {ι : Type u_1} (N : ι → ℕ) [Northcott N] {𝕜 : Type u_2} [RCLike 𝕜] {a : ℝ} (ha : 0 ≤ a) (hN : ∀ (i : ι), a ≤ ↑(N i)) (w : ι → 𝕜) {g : ℝ → 𝕜} (b : ℝ) (hg_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ g t) (hg_int : MeasureTheory.IntegrableOn (deriv g) (Set.Icc a b) MeasureTheory.volume) : summatory N (fun (i : ι) => w i * g ↑(N i)) b = g b * summatory N w b - ∫ (t : ℝ) in Set.Ioc a b, deriv g t * summatory N w t

Abel summation from a real cutoff a for a carrier all of whose indices have N-value at least a. The boundary term at a cancels, because there the twisted weight is g a times the untwisted one.

The identity holds for every cutoff b: below a all three terms vanish.

theorem TauCeti.integrableOn_mul_summatory {ι : Type u_1} (N : ι → ℕ) [Northcott N] {𝕜 : Type u_2} [RCLike 𝕜] (w : ι → 𝕜) {f : ℝ → 𝕜} {a b : ℝ} (ha : 0 ≤ a) (hf : MeasureTheory.IntegrableOn f (Set.Icc a b) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (t : ℝ) => f t * summatory N w t) (Set.Icc a b) MeasureTheory.volume

A summatory function, multiplied by a factor integrable on a compact interval of nonnegative cutoffs, is integrable there.

Imaginary-power twists

theorem TauCeti.norm_summatory_mul_cpow_le_of_summatory_le {ι : Type u_1} (N : ι → ℕ) [Northcott N] (hN : ∀ (i : ι), 1 ≤ ↑(N i)) (w : ι → ℂ) {C θ x : ℝ} (hx : 1 ≤ x) (hθ : 0 < θ) (z : ℂ) (hz : z.re = 0) (hC : ∀ t ∈ Set.Icc 1 x, ‖summatory N w t‖ ≤ C * t ^ θ) : ‖summatory N (fun (i : ι) => w i * ↑(N i) ^ (-z)) x‖ ≤ C * (1 + ‖z‖ / θ) * x ^ θ

An imaginary-power Abel bound. Suppose every index has N-value at least 1, and the partial sums of w are bounded by C * t ^ θ on [1, x] for a positive exponent θ. Twisting the weight by (N i) ^ (-z) with Re z = 0 preserves that exponent, at the cost of the explicit factor 1 + ‖z‖ / θ.

One-sided bounds for twisted sums

theorem TauCeti.summatory_mul_le_of_summatory_le {ι : Type u_1} (N : ι → ℕ) [Northcott N] {a : ℝ} (ha : 0 ≤ a) (hN : ∀ (i : ι), a ≤ ↑(N i)) (w : ι → ℝ) {g : ℝ → ℝ} {C x : ℝ} (hx : a ≤ x) (hC : ∀ t ∈ Set.Icc a x, summatory N w t ≤ C) (hg_diff : ∀ t ∈ Set.Icc a x, DifferentiableAt ℝ g t) (hg_int : MeasureTheory.IntegrableOn (deriv g) (Set.Icc a x) MeasureTheory.volume) (hg_deriv : ∀ t ∈ Set.Icc a x, deriv g t ≤ 0) (hg_nonneg : 0 ≤ g x) : summatory N (fun (i : ι) => w i * g ↑(N i)) x ≤ C * g a

A one-sided Abel bound. Let every index have N-value at least the cutoff a ≥ 0, and let g be nonincreasing on [a, x] with 0 ≤ g x. If the summatory function of a real weight w is at most C at every cutoff in [a, x], then the summatory function at x of the twisted weight i ↦ w i * g (N i) is at most C * g a.

No sign condition is imposed on w or on C: only the partial sums of w are controlled.

theorem TauCeti.tsum_mul_le_of_summatory_le {ι : Type u_1} (N : ι → ℕ) [Northcott N] {a : ℝ} (ha : 0 ≤ a) (hN : ∀ (i : ι), a ≤ ↑(N i)) (w : ι → ℝ) {g : ℝ → ℝ} {C : ℝ} (hC : ∀ (t : ℝ), a ≤ t → summatory N w t ≤ C) (hg_diff : ∀ (t : ℝ), a ≤ t → DifferentiableAt ℝ g t) (hg_int : ∀ (x : ℝ), a ≤ x → MeasureTheory.IntegrableOn (deriv g) (Set.Icc a x) MeasureTheory.volume) (hg_deriv : ∀ (t : ℝ), a ≤ t → deriv g t ≤ 0) (hg_nonneg : ∀ (t : ℝ), a ≤ t → 0 ≤ g t) (hsum : Summable fun (i : ι) => w i * g ↑(N i)) : ∑' (i : ι), w i * g ↑(N i) ≤ C * g a

A one-sided Abel bound for the full series. Let every index have N-value at least the cutoff a ≥ 0. If the summatory function of a real weight w is at most C at every cutoff t ≥ a, and g is nonnegative and nonincreasing on [a, ∞), then the sum of the summable twisted family i ↦ w i * g (N i) is at most C * g a.

The ideal and prime carriers of a number field

theorem TauCeti.idealSummatory_mul_eq_sub_integral_mul {𝕜 : Type u_2} [RCLike 𝕜] (K : Type u_3) [Field K] [NumberField K] (w : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) → 𝕜) {g : ℝ → 𝕜} (x : ℝ) (hg_diff : ∀ t ∈ Set.Icc 1 x, DifferentiableAt ℝ g t) (hg_int : MeasureTheory.IntegrableOn (deriv g) (Set.Icc 1 x) MeasureTheory.volume) : idealSummatory K (fun (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => w I * g ↑(Ideal.absNorm ↑I)) x = g x * idealSummatory K w x - ∫ (t : ℝ) in Set.Ioc 1 x, deriv g t * idealSummatory K w t

Abel summation over the nonzero ideals of 𝓞 K, from the cutoff 1.

theorem TauCeti.norm_idealSummatory_mul_cpow_le_of_summatory_le (K : Type u_3) [Field K] [NumberField K] (w : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) → ℂ) {C θ x : ℝ} (hx : 1 ≤ x) (hθ : 0 < θ) (z : ℂ) (hz : z.re = 0) (hC : ∀ t ∈ Set.Icc 1 x, ‖idealSummatory K w t‖ ≤ C * t ^ θ) : ‖idealSummatory K (fun (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => w I * ↑(Ideal.absNorm ↑I) ^ (-z)) x‖ ≤ C * (1 + ‖z‖ / θ) * x ^ θ

An imaginary norm-power twist preserves a positive power bound for partial sums over the nonzero ideals of a number field.

theorem TauCeti.primeSummatory_mul_eq_sub_integral_mul (K : Type u_3) [Field K] [NumberField K] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) → ℝ) {g : ℝ → ℝ} (x : ℝ) (hg_diff : ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ g t) (hg_int : MeasureTheory.IntegrableOn (deriv g) (Set.Icc 2 x) MeasureTheory.volume) : primeSummatory K (fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => w v * g ↑(Ideal.absNorm v.asIdeal)) x = g x * primeSummatory K w x - ∫ (t : ℝ) in Set.Ioc 2 x, deriv g t * primeSummatory K w t

Abel summation over the height-one primes of 𝓞 K, from the cutoff 2.

theorem TauCeti.primeTheta_eq_log_mul_primeCount_sub_integral {K : Type u_3} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ℝ) : primeTheta K S x = Real.log x * primeCount K S x - ∫ (t : ℝ) in Set.Ioc 2 x, primeCount K S t / t

Chebyshev's ϑ from π. The logarithmically weighted prime count is recovered from the unweighted one by Abel summation, with the inclusive cutoff and the half-open integration range fixed by the roadmap's conventions.

theorem TauCeti.primeCount_eq_primeTheta_div_log_add_integral {K : Type u_3} [Field K] [NumberField K] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (x : ℝ) : primeCount K S x = primeTheta K S x / Real.log x + ∫ (t : ℝ) in Set.Ioc 2 x, primeTheta K S t / (t * Real.log t ^ 2)

Chebyshev's π from ϑ. The unweighted prime count is recovered from the logarithmically weighted one by Abel summation. This is the finite identity whose two terms Layer 6.2 estimates in order to turn ϑ(x) ∼ δx into π(x) ∼ δ Li(x).