Arithmetic Dirichlet series and Tauberian methods

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe prime ideal theorem#

For a number field K, Chebyshev's functions satisfy ψ_K(x) ~ x and ϑ_K(x) ~ x, and the number π_K(x) of prime ideals of norm at most x satisfies π_K(x) ~ Li(x).

TauCeti.primeIdealTheorem.{u_1} (K : Type u_1) [Field K] [NumberField K] :
  (Asymptotics.IsEquivalent Filter.atTop (TauCeti.primePsi K Set.univ) fun x => x) ∧
    (Asymptotics.IsEquivalent Filter.atTop (TauCeti.primeTheta K Set.univ) fun x => x) ∧
      Asymptotics.IsEquivalent Filter.atTop (TauCeti.primeCount K Set.univ) TauCeti.Real.logIntegral
Lean

Formalized in Tau Ceti as TauCeti.primeIdealTheorem.

Other forms

The prime ideal theorem, in the form π_K(x) ~ x / log x. Formalized in Tau Ceti as TauCeti.primeCount_univ_isEquivalent_div_log.

TauCeti.primeCount_univ_isEquivalent_div_log.{u_1} (K : Type u_1) [Field K] [NumberField K] :
  Asymptotics.IsEquivalent Filter.atTop (TauCeti.primeCount K Set.univ) fun x => x / Real.log x
Sources
LeanTauCeti.primeIdealTheorem · TauCeti.primeCount_univ_isEquivalent_div_log
Uses 2 · Used by 2
Proof usesBoundary data for all primes of a number field · The conditional prime ideal theorem
Used byDirichlet's theorem on primes in arithmetic progressions, with Dirichlet density · Mertens' first theorem for a number field

TheoremThe Wiener--Ikehara theorem#

Let a n ≥ 0 have Dirichlet series with sum F s on Re s > 1, and let G be continuous on Re s ≥ 1 with G s = F s - κ / (s - 1) on Re s > 1. Then x⁻¹ ∑_{1 ≤ n ≤ x} a n → κ as x → ∞.

TauCeti.LSeries.wienerIkehara {a : ℕ → ℝ} {F G : ℂ → ℂ} {κ : ℝ} (ha : 0 ≤ a)
  (hF : ∀ (s : ℂ), 1 < s.re → LSeriesHasSum (fun n => ↑(a n)) s (F s))
  (hG : ContinuousOn G {s | 1 ≤ s.re}) (hGF : ∀ (s : ℂ), 1 < s.re → G s = F s - ↑κ / (s - 1)) :
  Filter.Tendsto (fun x => x⁻¹ * ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, a n) Filter.atTop (nhds κ)
Lean

Formalized in Tau Ceti as TauCeti.LSeries.wienerIkehara.

Other forms

The Wiener--Ikehara theorem at natural cutoffs. Formalized in Tau Ceti as TauCeti.LSeries.wienerIkehara_nat.

TauCeti.LSeries.wienerIkehara_nat {a : ℕ → ℝ} {F G : ℂ → ℂ} {κ : ℝ}
  (ha : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ a n)
  (hF : ∀ (s : ℂ), 1 < s.re → LSeriesHasSum (fun n => ↑(a n)) s (F s))
  (hG : ContinuousOn G {s | 1 ≤ s.re}) (hGF : ∀ (s : ℂ), 1 < s.re → G s = F s - ↑κ / (s - 1)) :
  Filter.Tendsto (fun N => (↑N)⁻¹ * ∑ n ∈ Finset.Icc 1 N, a n) Filter.atTop (nhds κ)

The Wiener--Ikehara theorem for a pole at a positive abscissa. Formalized in Tau Ceti as TauCeti.LSeries.wienerIkehara_rpow.

TauCeti.LSeries.wienerIkehara_rpow {a : ℕ → ℝ} {F G : ℂ → ℂ} {κ σ : ℝ} (hσ : 0 < σ)
  (ha : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ a n)
  (hF : ∀ (s : ℂ), σ < s.re → LSeriesHasSum (fun n => ↑(a n)) s (F s))
  (hG : ContinuousOn G {s | σ ≤ s.re}) (hGF : ∀ (s : ℂ), σ < s.re → G s = F s - ↑κ / (s - ↑σ)) :
  Filter.Tendsto (fun x => (x ^ σ)⁻¹ * ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, a n) Filter.atTop (nhds (κ / σ))

The Wiener--Ikehara theorem for coefficients in an ordered vector space. Formalized in Tau Ceti as TauCeti.LSeries.wienerIkehara_of_forall_monotone_dual.

TauCeti.LSeries.wienerIkehara_of_forall_monotone_dual.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [PartialOrder E]
  [IsOrderedAddMonoid E] [PosSMulMono ℝ E] [OrderClosedTopology E] {ι : Type u_2}
  {φ : ι → StrongDual ℝ E} (hφ : ∀ (i : ι), Monotone ⇑(φ i))
  (hspan : ∀ (ψ : StrongDual ℝ E), Monotone ⇑ψ → ψ ∈ Submodule.span ℝ (Set.range φ)) {a : ℕ → E}
  {κ : E} (ha : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ a n)
  (hFG :
    ∀ (i : ι),
      ∃ F G,
        (∀ (s : ℂ), 1 < s.re → LSeriesHasSum (fun n => ↑((φ i) (a n))) s (F s)) ∧
          ContinuousOn G {s | 1 ≤ s.re} ∧ ∀ (s : ℂ), 1 < s.re → G s = F s - ↑((φ i) κ) / (s - 1)) :
  Filter.Tendsto (fun x => x⁻¹ • ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, a n) Filter.atTop (nhds κ)

The Wiener--Ikehara theorem for eventually nonnegative coefficients. Formalized in Tau Ceti as TauCeti.LSeries.wienerIkehara_of_eventually_nonneg.

TauCeti.LSeries.wienerIkehara_of_eventually_nonneg {a : ℕ → ℝ} {F G : ℂ → ℂ} {κ : ℝ}
  (ha : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ a n)
  (hF : ∀ (s : ℂ), 1 < s.re → LSeriesHasSum (fun n => ↑(a n)) s (F s))
  (hG : ContinuousOn G {s | 1 ≤ s.re}) (hGF : ∀ (s : ℂ), 1 < s.re → G s = F s - ↑κ / (s - 1)) :
  Filter.Tendsto (fun x => x⁻¹ * ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, a n) Filter.atTop (nhds κ)

The Wiener--Ikehara theorem with zero residue. Formalized in Tau Ceti as TauCeti.LSeries.wienerIkehara_zero.

TauCeti.LSeries.wienerIkehara_zero {a : ℕ → ℝ} {F G : ℂ → ℂ} (ha : 0 ≤ a)
  (hF : ∀ (s : ℂ), 1 < s.re → LSeriesHasSum (fun n => ↑(a n)) s (F s))
  (hG : ContinuousOn G {s | 1 ≤ s.re}) (hGF : ∀ (s : ℂ), 1 < s.re → G s = F s) :
  Filter.Tendsto (fun x => x⁻¹ * ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, a n) Filter.atTop (nhds 0)
Sources
LeanTauCeti.LSeries.wienerIkehara · TauCeti.LSeries.wienerIkehara_nat · TauCeti.LSeries.wienerIkehara_rpow · TauCeti.LSeries.wienerIkehara_of_forall_monotone_dual · TauCeti.LSeries.wienerIkehara_of_eventually_nonneg · TauCeti.LSeries.wienerIkehara_zero
Uses 3 · Used by 2
Proof usesAbel's inequality, comparison form · The Chebyshev bound · Riemann--Lebesgue on a vertical line
Used byPrime-number-theorem transfer from exact boundary data · Weighted Chebotarev for abelian extensions

TheoremPrime-number-theorem transfer from exact boundary data#

The three conclusions are, respectively, the von Mangoldt-weighted prime-power asymptotic, the logarithmically weighted prime asymptotic after removing higher powers, and the unweighted prime-counting asymptotic after Abel summation. The error-term formulation includes residue zero.

TauCeti.primeNumberTheoremTransfer.{u_1} {K : Type u_1} [Field K] [NumberField K]
  {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {δ : ℝ}
  (B : TauCeti.PrimeBoundaryRemainder K S δ) :
  ((fun x => TauCeti.primePsi K S x - δ * x) =o[Filter.atTop] fun x => x) ∧
    ((fun x => TauCeti.primeTheta K S x - δ * x) =o[Filter.atTop] fun x => x) ∧
      (fun x => TauCeti.primeCount K S x - δ * TauCeti.Real.logIntegral x) =o[Filter.atTop] fun x =>
        x / Real.log x
Lean

Formalized in Tau Ceti as TauCeti.primeNumberTheoremTransfer.

Sources
LeanTauCeti.primeNumberTheoremTransfer
Uses 2 · Used by 3
Statement usesBoundary data for the prime Dirichlet series of S
Proof usesThe Wiener--Ikehara theorem
Used byThe conditional prime ideal theorem · Dirichlet's theorem on primes in arithmetic progressions, with Dirichlet density · The prime number theorem for arithmetic progressions

TheoremThe Dedekind zeta function has no zeros on the line Re s = 1 away from its pole#

If f agrees with ζ_K on Re s > 1 and is complex differentiable at a point s ≠ 1 with Re s = 1, then f s ≠ 0. By exists_differentiableOn_eq_dedekindZeta_sub, such an f exists: the meromorphic continuation of ζ_K.

TauCeti.ne_zero_of_eqOn_dedekindZeta.{u_1} {K : Type u_1} [Field K] [NumberField K] {f : ℂ → ℂ}
  {s : ℂ} (hs : s.re = 1) (hs1 : s ≠ 1) (hf : DifferentiableAt ℂ f s)
  (hfζ : Set.EqOn f (NumberField.dedekindZeta K) {z | 1 < z.re}) : f s ≠ 0
Lean

Formalized in Tau Ceti as TauCeti.ne_zero_of_eqOn_dedekindZeta.

Sources
LeanTauCeti.ne_zero_of_eqOn_dedekindZeta
Uses 1 · Used by 2
Proof usesThe analytic Euler product
Used byBoundary data for all primes of a number field · Weighted Chebotarev for abelian extensions

TheoremNonvanishing when the square also cancels#

If a unitary weight χ and its pointwise square χ ^ 2 both have cancellation, the continued L-function of χ has no zeros on the closed half-plane Re s ≥ 1.

TauCeti.continuedLFunctionOfWeight_ne_zero_of_hasCancellation_sq.{u_1} {K : Type u_1} [Field K]
  [NumberField K] {χ : TauCeti.UnitaryIdealWeight K} (hχ : TauCeti.HasCancellation χ)
  (hχ₂ : TauCeti.HasCancellation (χ ^ 2)) {s : ℂ} (hs : 1 ≤ s.re) :
  TauCeti.continuedLFunctionOfWeight χ s ≠ 0
Lean

Formalized in Tau Ceti as TauCeti.continuedLFunctionOfWeight_ne_zero_of_hasCancellation_sq.

Sources
LeanTauCeti.continuedLFunctionOfWeight_ne_zero_of_hasCancellation_sq
Uses 2
Statement usesThe continued L-function of a unitary weight, defined by partial summation
Proof usesThe analytic Euler product

TheoremThe analytic Euler product#

If the ideal-indexed Dirichlet series of D converges absolutely at s, then its local Euler factors have an unrestricted infinite product over the height-one primes, and that product is the LSeries of the norm coefficients of D.

The hypothesis is absolute convergence of the ideal-indexed series, not of the regrouped one: regrouping can only improve convergence, and the finite partial products of the local factors are sums over ideals, not over norms.

TauCeti.EulerProductData.hasProd_eulerFactor.{u_1} {K : Type u_1} [Field K] [NumberField K]
  (D : TauCeti.EulerProductData K) {s : ℂ}
  (hs : Summable (TauCeti.idealTerm K D.toIdealArithmeticFunction s)) :
  HasProd (fun P => D.eulerFactor P s)
    (LSeries (⇑((TauCeti.normCoeff K) D.toIdealArithmeticFunction)) s)
Lean

Formalized in Tau Ceti as TauCeti.EulerProductData.hasProd_eulerFactor.

Sources
LeanTauCeti.EulerProductData.hasProd_eulerFactor
Used by 9
Used byBoundary data for all primes of a number field · Nonvanishing when the square also cancels · TauCeti.EulerProductData.hasProd_eulerFactor_convolution · The Dedekind zeta function has no zeros on the line Re s = 1 away from its pole · Dirichlet's theorem on primes in arithmetic progressions, with Dirichlet density · Non-Galois Chebotarev for splitting types · The Chebotarev density theorem · Weighted Chebotarev for abelian extensions · Chebyshev's identity for a number field

TheoremTauCeti.EulerProductData.hasProd_eulerFactor_convolution#

The Euler factors of a convolution have an unrestricted product equal to the product of the original norm-regrouped Dirichlet series, whenever both ideal-indexed series converge absolutely.

TauCeti.EulerProductData.hasProd_eulerFactor_convolution.{u_1} {K : Type u_1} [Field K]
  [NumberField K] (D E : TauCeti.EulerProductData K) {s : ℂ}
  (hD : Summable (TauCeti.idealTerm K D.toIdealArithmeticFunction s))
  (hE : Summable (TauCeti.idealTerm K E.toIdealArithmeticFunction s)) :
  HasProd (fun P => (D.convolution E).eulerFactor P s)
    (LSeries (⇑((TauCeti.normCoeff K) D.toIdealArithmeticFunction)) s *
      LSeries (⇑((TauCeti.normCoeff K) E.toIdealArithmeticFunction)) s)
Lean

Formalized in Tau Ceti as TauCeti.EulerProductData.hasProd_eulerFactor_convolution.

Sources
LeanTauCeti.EulerProductData.hasProd_eulerFactor_convolution
Uses 2
Statement usesTauCeti.EulerProductData.convolution
Proof usesThe analytic Euler product

StructureBoundary data for the prime Dirichlet series of S#

The function series is the sum of the Dirichlet series of primeVonMangoldtCoeff K S on Re s > 1. The function remainder is continuous on Re s ≥ 1 and agrees on the open half-plane with series s - δ / (s - 1).

The functions have precisely their mathematically relevant domains, so the structure carries no arbitrary values elsewhere.

TauCeti.PrimeBoundaryRemainder.{u_2} (K : Type u_2) [Field K] [NumberField K]
  (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (δ : ℝ) : Type
Lean

Formalized in Tau Ceti as TauCeti.PrimeBoundaryRemainder.

Sources
LeanTauCeti.PrimeBoundaryRemainder
Used by 5
Used byBoundary data for all primes of a number field · Prime-number-theorem transfer from exact boundary data · The conditional prime ideal theorem · Dirichlet's theorem on primes in arithmetic progressions, with Dirichlet density · The prime number theorem for arithmetic progressions

DefinitionBoundary data for all primes of a number field#

The von Mangoldt series of all primes of K sums to -ζ_K'(s)/ζ_K(s) on Re s > 1, and -ζ_K'(s)/ζ_K(s) - 1/(s - 1) extends continuously to Re s ≥ 1 (TauCeti.exists_continuousOn_eq_neg_deriv_dedekindZeta_div_sub).

TauCeti.LFunctions.primeIdealVonMangoldtBoundary.{u_1} (K : Type u_1) [Field K] [NumberField K] :
  TauCeti.PrimeBoundaryRemainder K Set.univ 1
Lean

Formalized in Tau Ceti as TauCeti.LFunctions.primeIdealVonMangoldtBoundary.

Sources
LeanTauCeti.LFunctions.primeIdealVonMangoldtBoundary
Uses 3 · Used by 1
Statement usesBoundary data for the prime Dirichlet series of S
Proof usesThe analytic Euler product · The Dedekind zeta function has no zeros on the line Re s = 1 away from its pole
Used byThe prime ideal theorem

DefinitionThe continued L-function of a unitary weight, defined by partial summation#

s * ∫_{1}^{∞} (∑_{N(I) ≤ t} χ(I)) t ^ (-(s + 1)) dt.

On Re s > 1 it is the norm-regrouped L-series of χ (TauCeti.continuedLFunctionOfWeight_eq_LSeries); under TauCeti.HasCancellation χ it is holomorphic on Re s > 1 - 1 / [K : ℚ] (TauCeti.differentiableOn_continuedLFunctionOfWeight). Where the integral does not converge it takes the junk value of Mathlib's Bochner integral.

TauCeti.continuedLFunctionOfWeight.{u_1} {K : Type u_1} [Field K] [NumberField K]
  (χ : TauCeti.UnitaryIdealWeight K) (s : ℂ) : ℂ
Lean

Formalized in Tau Ceti as TauCeti.continuedLFunctionOfWeight.

Sources
LeanTauCeti.continuedLFunctionOfWeight
Used by 3
Used byNonvanishing when the square also cancels · The Chebotarev density theorem · Weighted Chebotarev for abelian extensions

DefinitionTauCeti.EulerProductData.convolution#

Convolve two ideal coefficient systems. This operation multiplies local series and is distinct from the pointwise multiplication instance on EulerProductData.

TauCeti.EulerProductData.convolution.{u_1} {K : Type u_1} [Field K] [NumberField K]
  (D E : TauCeti.EulerProductData K) : TauCeti.EulerProductData K
Lean

Formalized in Tau Ceti as TauCeti.EulerProductData.convolution.

Sources
LeanTauCeti.EulerProductData.convolution
Used by 1
Used byTauCeti.EulerProductData.hasProd_eulerFactor_convolution

InstanceTauCeti.MultiplicativeIdealWeight.instStarMul#

Conjugation is the star of the weights, as for MulChar, TauCeti.IdealArithmeticFunction and TauCeti.EulerProductData: an involution which is multiplicative, the product being commutative.

TauCeti.MultiplicativeIdealWeight.instStarMul.{u_1} {K : Type u_1} [Field K] [NumberField K] :
  StarMul (TauCeti.MultiplicativeIdealWeight K)
Lean

Formalized in Tau Ceti as TauCeti.MultiplicativeIdealWeight.instStarMul.

Sources
LeanTauCeti.MultiplicativeIdealWeight.instStarMul

TheoremThe conditional prime ideal theorem#

Boundary data for all prime ideals with residue one give the standard asymptotic equivalences for ψ, ϑ, and π.

TauCeti.primeIdealTheorem_of_boundary.{u_1} {K : Type u_1} [Field K] [NumberField K]
  (B : TauCeti.PrimeBoundaryRemainder K Set.univ 1) :
  (Asymptotics.IsEquivalent Filter.atTop (TauCeti.primePsi K Set.univ) fun x => x) ∧
    (Asymptotics.IsEquivalent Filter.atTop (TauCeti.primeTheta K Set.univ) fun x => x) ∧
      Asymptotics.IsEquivalent Filter.atTop (TauCeti.primeCount K Set.univ) TauCeti.Real.logIntegral
Lean

Formalized in Tau Ceti as TauCeti.primeIdealTheorem_of_boundary.

Sources
LeanTauCeti.primeIdealTheorem_of_boundary
Uses 2 · Used by 1
Statement usesBoundary data for the prime Dirichlet series of S
Proof usesPrime-number-theorem transfer from exact boundary data
Used byThe prime ideal theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.