Analytic continuation of Dirichlet series

DefinitionPartial sums of a coefficient sequence#✓fully proved

For \(f : \mathbb{N} \to \mathbb{C}\) and \(n \in \mathbb{N}\), the one-based partial sum is \(A(n) = \sum_{k=1}^{n} f(k)\); in particular \(A(0) = 0\) and the value \(f(0)\) is never used.

def abelPartialSum (f : ℕ → ℂ) (n : ℕ) : ℂ :=
  ∑ k ∈ Finset.Icc 1 n, f k

Used by 16

Used byA cosine series for \(\varphi_r(x-1) + \varphi_r(-x)\) · Abel continuation agrees with the Dirichlet series · The Abel continuation as a Mellin transform · Partial sums after subtracting a constant · Summatory step function · Analyticity of the linear asymptotic continuation away from \(1\) · Analyticity of the Abel continuation · Complex differentiability of the Abel continuation · Growth bound for the partial sums of a shifted sequence · Growth of the summatory step function · Meromorphy of the linear asymptotic continuation at \(1\) · Meromorphy of the linear asymptotic continuation on a half-plane · The linear asymptotic continuation has a simple pole at \(1\) · Abel continuation as the limit of Dirichlet partial sums · Convergence of the Dirichlet series to the linear asymptotic continuation · Limit of the linear asymptotic continuation times \(s - 1\) at \(1\)

DefinitionSummatory step function#✓fully proved

For \(f : \mathbb{N} \to \mathbb{C}\) with partial sums \(A(n) = \sum_{k=1}^{n} f(k)\), the summatory step function of \(f\) is the function \(S : \mathbb{R} \to \mathbb{C}\) with \(S(t) = A(\lfloor t \rfloor)\) for \(t \ge 0\) and \(S(t) = 0\) for \(t < 0\). Equivalently, \(S(t) = \sum_{1 \le k \le t} f(k)\) for every real \(t\).

def abelSummatory (f : ℕ → ℂ) (t : ℝ) : ℂ :=
  abelPartialSum f ⌊t⌋₊

Uses 1 · Used by 8

Statement usesPartial sums of a coefficient sequence

Used byAbel continuation of a Dirichlet series · The Abel continuation as a Mellin transform · The summatory step function vanishes below one · Complex differentiability of the Abel continuation · Growth of the summatory step function · The summatory step function is negligible near zero · Local integrability of the summatory function · Abel continuation as the limit of Dirichlet partial sums

DefinitionAbel continuation of a Dirichlet series#✓fully proved

For \(f : \mathbb{N} \to \mathbb{C}\) with partial sums \(A(n) = \sum_{k=1}^{n} f(k)\), the Abel continuation of \(f\) is the function \(F_f : \mathbb{C} \to \mathbb{C}\) given by

\[F_f(s) = s \int_1^\infty A(\lfloor t \rfloor)\, t^{-s-1}\, dt,\]

where the integral is taken to be \(0\) when the integrand is not integrable on \((1, \infty)\).

def abelContinuation (f : ℕ → ℂ) (s : ℂ) : ℂ :=
  s * ∫ t : ℝ in Set.Ioi (1 : ℝ), abelSummatory f t * (t : ℂ) ^ (-(s + 1))

Uses 1 · Used by 13

Statement usesSummatory step function

Used byA cosine series for \(\varphi_r(x-1) + \varphi_r(-x)\) · Abel continuation agrees with the Dirichlet series · The Abel continuation as a Mellin transform · Analyticity of the linear asymptotic continuation away from \(1\) · Analyticity of the Abel continuation · Complex differentiability of the Abel continuation · Linear asymptotic Dirichlet continuation · Cleared-denominator form of the linear asymptotic continuation · Meromorphy of the linear asymptotic continuation at \(1\) · The linear asymptotic continuation has a simple pole at \(1\) · Abel continuation as the limit of Dirichlet partial sums · Convergence of the Dirichlet series to the linear asymptotic continuation · Limit of the linear asymptotic continuation times \(s - 1\) at \(1\)

TheoremThe summatory step function vanishes below one#✓fully proved

For \(f : \mathbb{N} \to \mathbb{C}\), the summatory step function \(S(t) = \sum_{1 \le k \le t} f(k)\) satisfies \(S(t) = 0\) for every real \(t < 1\).

theorem abelSummatory_eq_zero_of_lt_one (f : ℕ → ℂ) {t : ℝ} (ht : t < 1) :
    abelSummatory f t = 0

Uses 1 · Used by 2

Statement usesSummatory step function

Used byThe Abel continuation as a Mellin transform · The summatory step function is negligible near zero

TheoremLocal integrability of the summatory function#✓fully proved

For every \(f : \mathbb{N} \to \mathbb{C}\), the summatory step function \(t \mapsto \sum_{k=1}^{\lfloor t \rfloor} f(k)\) on \(\mathbb{R}\) is locally integrable on the open half-line \((0, \infty)\): every \(t > 0\) has a neighbourhood within \((0, \infty)\) on which this function is Lebesgue integrable.

theorem locallyIntegrableOn_abelSummatory (f : ℕ → ℂ) :
    LocallyIntegrableOn (abelSummatory f) (Set.Ioi (0 : ℝ))

Uses 1 · Used by 2

Statement usesSummatory step function

Used byThe Abel continuation as a Mellin transform · Complex differentiability of the Abel continuation

TheoremGrowth of the summatory step function#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{C}\) have partial sums \(A(n) = \sum_{k=1}^{n} f(k)\) and summatory step function \(S(t) = \sum_{1 \le k \le t} f(k)\), and let \(\sigma\) be any real number with \(A(n) = O(n^\sigma)\) as \(n \to \infty\). Then \(S(t) = O(t^\sigma)\) as \(t \to \infty\) through the reals.

No sign condition on \(\sigma\) is needed.

theorem isBigO_abelSummatory_atTop (f : ℕ → ℂ) {σ : ℝ}
    (hO : (fun n => abelPartialSum f n) =O[atTop]
      fun n => ((n : ℝ) ^ σ : ℝ)) :
    (abelSummatory f) =O[atTop] fun t : ℝ => (t ^ σ : ℝ)

Uses 2 · Used by 2

Statement usesPartial sums of a coefficient sequence · Summatory step function

Used byThe Abel continuation as a Mellin transform · Complex differentiability of the Abel continuation

TheoremThe summatory step function is negligible near zero#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{C}\) have summatory step function \(S(t) = \sum_{1 \le k \le t} f(k)\). For every real \(b\), \(S(t) = O(t^{-b})\) as \(t \to 0^+\).

This holds because \(S\) vanishes on \((0, 1)\).

theorem isBigO_abelSummatory_nhdsGT_zero (f : ℕ → ℂ) (b : ℝ) :
    (abelSummatory f) =O[𝓝[>] (0 : ℝ)] fun t : ℝ => (t ^ (-b) : ℝ)

Uses 2 · Used by 2

Statement usesSummatory step function

Proof usesThe summatory step function vanishes below one

Used byThe Abel continuation as a Mellin transform · Complex differentiability of the Abel continuation

TheoremThe Abel continuation as a Mellin transform#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{C}\) have partial sums \(A(n) = \sum_{k=1}^{n} f(k)\) and summatory step function \(S(t) = \sum_{1 \le k \le t} f(k)\) for real \(t\), and let \(\sigma\) be a real number with \(A(n) = O(n^\sigma)\) as \(n \to \infty\). Then for every \(s \in \mathbb{C}\) with \(\operatorname{Re} s > \sigma\), the Abel continuation satisfies \(F_f(s) = s\,\mathcal{M}S(-s)\), where \(\mathcal{M}S(z) = \int_0^\infty t^{z-1} S(t)\,dt\) is the Mellin transform of \(S\).

This identity transfers holomorphy of the Mellin transform to the continuation.

theorem abelContinuation_eq_mul_mellin (f : ℕ → ℂ) {σ : ℝ} {s : ℂ}
    (hs : σ < s.re)
    (hO : (fun n => abelPartialSum f n) =O[atTop] fun n => ((n : ℝ) ^ σ : ℝ)) :
    abelContinuation f s = s * mellin (abelSummatory f) (-s)

Uses 7 · Used by 1

Statement usesAbel continuation of a Dirichlet series · Partial sums of a coefficient sequence · Summatory step function

Proof usesThe summatory step function vanishes below one · Growth of the summatory step function · The summatory step function is negligible near zero · Local integrability of the summatory function

Used byComplex differentiability of the Abel continuation

TheoremComplex differentiability of the Abel continuation#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{C}\) have partial sums \(A(n) = \sum_{k=1}^{n} f(k)\), and let \(\sigma\) be a real number with \(A(n) = O(n^\sigma)\) as \(n \to \infty\). Then the Abel continuation \(F_f\) of \(f\) is complex differentiable at every \(s \in \mathbb{C}\) with \(\operatorname{Re} s > \sigma\).

The proof uses holomorphy of the Mellin transform of the summatory step function at \(-s\).

theorem differentiableAt_abelContinuation (f : ℕ → ℂ) {σ : ℝ}
    {s : ℂ} (hs : σ < s.re)
    (hO : (fun n => abelPartialSum f n) =O[atTop] fun n => ((n : ℝ) ^ σ : ℝ)) :
    DifferentiableAt ℂ (abelContinuation f) s

Uses 7 · Used by 1

Statement usesAbel continuation of a Dirichlet series · Partial sums of a coefficient sequence

Proof usesThe Abel continuation as a Mellin transform · Summatory step function · Growth of the summatory step function · The summatory step function is negligible near zero · Local integrability of the summatory function

Used byAnalyticity of the Abel continuation

TheoremAnalyticity of the Abel continuation#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{C}\) have partial sums \(A(n) = \sum_{k=1}^{n} f(k)\), and let \(\sigma\) be a real number with \(A(n) = O(n^\sigma)\) as \(n \to \infty\). Then the Abel continuation \(F_f\) of \(f\) is analytic on the half-plane \(\{s \in \mathbb{C} : \operatorname{Re} s > \sigma\}\).

theorem analyticOn_abelContinuation (f : ℕ → ℂ) {σ : ℝ}
    (hO : (fun n => abelPartialSum f n) =O[atTop] fun n => ((n : ℝ) ^ σ : ℝ)) :
    AnalyticOn ℂ (abelContinuation f) {s | σ < s.re}

Uses 3 · Used by 5

Statement usesAbel continuation of a Dirichlet series · Partial sums of a coefficient sequence

Proof usesComplex differentiability of the Abel continuation

Used byA cosine series for \(\varphi_r(x-1) + \varphi_r(-x)\) · Analyticity of the linear asymptotic continuation away from \(1\) · Meromorphy of the linear asymptotic continuation at \(1\) · The linear asymptotic continuation has a simple pole at \(1\) · Limit of the linear asymptotic continuation times \(s - 1\) at \(1\)

TheoremAbel continuation agrees with the Dirichlet series#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{C}\) have partial sums \(A(n) = \sum_{k=1}^{n} f(k)\), let \(\sigma \ge 0\) be a real number with \(A(n) = O(n^\sigma)\) as \(n \to \infty\), and let \(s\) be a complex number with \(\operatorname{Re} s > \sigma\) at which the Dirichlet series \(\sum_{n \ge 1} f(n) n^{-s}\) converges absolutely. Then the Abel continuation \(F_f\) of \(f\) satisfies \(F_f(s) = \sum_{n=1}^{\infty} f(n) n^{-s}\).

The hypothesis \(\sigma \ge 0\) is inherited from the integral representation of the Dirichlet series used in the proof.

theorem abelContinuation_eq_LSeries (f : ℕ → ℂ) {σ : ℝ} (hσ : 0 ≤ σ) {s : ℂ}
    (hs : σ < s.re) (hS : LSeriesSummable f s)
    (hO : (fun n => abelPartialSum f n) =O[atTop] fun n => ((n : ℝ) ^ σ : ℝ)) :
    abelContinuation f s = LSeries f s

Uses 2 · Used by 1

Statement usesAbel continuation of a Dirichlet series · Partial sums of a coefficient sequence

Used byA cosine series for \(\varphi_r(x-1) + \varphi_r(-x)\)

TheoremAbel continuation as the limit of Dirichlet partial sums#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{C}\) with partial sums \(A(n) = \sum_{k=1}^{n} f(k)\), let \(\sigma\) be a real number and let \(s\) be a complex number with \(\sigma < \operatorname{Re} s\). If \(A(n) = O(n^\sigma)\) as \(n \to \infty\), then the partial sums \(\sum_{n=1}^{N} f(n) n^{-s}\) converge, as \(N \to \infty\), to the Abel continuation \(F_f(s)\) of \(f\) at \(s\).

No summability of the Dirichlet series is assumed: the convergence may be conditional.

theorem tendsto_abelContinuation_Icc (f : ℕ → ℂ) {σ : ℝ} {s : ℂ}
    (hs : σ < s.re)
    (hO : (fun n => abelPartialSum f n) =O[atTop]
      fun n => ((n : ℝ) ^ σ : ℝ)) :
    Tendsto (fun N => ∑ n ∈ Finset.Icc 1 N, LSeries.term f s n) atTop
      (𝓝 (abelContinuation f s))

Uses 3 · Used by 2

Statement usesAbel continuation of a Dirichlet series · Partial sums of a coefficient sequence

Proof usesSummatory step function

Used byA cosine series for \(\varphi_r(x-1) + \varphi_r(-x)\) · Convergence of the Dirichlet series to the linear asymptotic continuation

DefinitionLinear asymptotic Dirichlet continuation#✓fully proved

For \(a : \mathbb{N} \to \mathbb{C}\) and \(\rho \in \mathbb{C}\), the linear asymptotic Dirichlet continuation of \(a\) with constant \(\rho\) is the function \(L_{a,\rho} : \mathbb{C} \to \mathbb{C}\) given by \(L_{a,\rho}(s) = \rho\,\zeta(s) + F_{a-\rho}(s)\), where \(\zeta\) is the Riemann zeta function and \(F_{a-\rho}\) is the Abel continuation of the sequence \(n \mapsto a(n) - \rho\).

For \(\rho \neq 0\) the term \(\rho\,\zeta(s)\) carries the pole at \(s = 1\), and \(F_{a-\rho}\) continues the remainder. At \(s = 1\) the formula uses the finite value that Mathlib assigns to \(\zeta(1)\).

def linearAsymptoticDirichletContinuation (a : ℕ → ℂ) (ρ s : ℂ) : ℂ :=
  ρ * riemannZeta s + abelContinuation (fun n => a n - ρ) s

Uses 1 · Used by 7

Statement usesAbel continuation of a Dirichlet series

Used byAnalyticity of the linear asymptotic continuation away from \(1\) · Cleared-denominator form of the linear asymptotic continuation · Meromorphy of the linear asymptotic continuation at \(1\) · Meromorphy of the linear asymptotic continuation on a half-plane · The linear asymptotic continuation has a simple pole at \(1\) · Convergence of the Dirichlet series to the linear asymptotic continuation · Limit of the linear asymptotic continuation times \(s - 1\) at \(1\)

TheoremPartial sums after subtracting a constant#✓fully proved

For \(a : \mathbb{N} \to \mathbb{C}\), \(\rho \in \mathbb{C}\) and \(n \in \mathbb{N}\), the one-based partial sum \(\sum_{k=1}^{n} (a(k) - \rho)\) equals \(\sum_{k=1}^{n} a(k) - n\rho\).

theorem abelPartialSum_sub_const (a : ℕ → ℂ) (ρ : ℂ) (n : ℕ) :
    abelPartialSum (fun k => a k - ρ) n = abelPartialSum a n - n • ρ

Uses 1 · Used by 1

Statement usesPartial sums of a coefficient sequence

Used byGrowth bound for the partial sums of a shifted sequence

TheoremGrowth bound for the partial sums of a shifted sequence#✓fully proved

Let \(a : \mathbb{N} \to \mathbb{C}\), \(\rho \in \mathbb{C}\) and \(\sigma \in \mathbb{R}\). If the one-based partial sums \(A(n) = \sum_{k=1}^{n} a(k)\) satisfy \(A(n) - n\rho = O(n^{\sigma})\) as \(n \to \infty\), then \(\sum_{k=1}^{n} (a(k) - \rho) = O(n^{\sigma})\) as \(n \to \infty\).

theorem isBigO_abelPartialSum_sub_const (a : ℕ → ℂ) (ρ : ℂ) {σ : ℝ}
    (hO : (fun n => abelPartialSum a n - n • ρ) =O[atTop]
      fun n => ((n : ℝ) ^ σ : ℝ)) :
    (fun n => abelPartialSum (fun k => a k - ρ) n) =O[atTop]
      fun n => ((n : ℝ) ^ σ : ℝ)

Uses 2 · Used by 5

Statement usesPartial sums of a coefficient sequence

Proof usesPartial sums after subtracting a constant

Used byAnalyticity of the linear asymptotic continuation away from \(1\) · Meromorphy of the linear asymptotic continuation at \(1\) · The linear asymptotic continuation has a simple pole at \(1\) · Convergence of the Dirichlet series to the linear asymptotic continuation · Limit of the linear asymptotic continuation times \(s - 1\) at \(1\)

TheoremAnalyticity of the linear asymptotic continuation away from \(1\)#✓fully proved

Let \(a : \mathbb{N} \to \mathbb{C}\), \(\rho \in \mathbb{C}\) and \(\sigma \in \mathbb{R}\), and suppose that the one-based partial sums \(A(n) = \sum_{k=1}^{n} a(k)\) satisfy \(A(n) - n\rho = O(n^{\sigma})\) as \(n \to \infty\). Then the linear asymptotic Dirichlet continuation \(L_{a,\rho}\) of \(a\) with constant \(\rho\) is complex analytic at every \(s \in \mathbb{C}\) with \(\operatorname{Re} s > \sigma\) and \(s \neq 1\).

theorem analyticAt_linearAsymptoticDirichletContinuation_of_ne_one
    (a : ℕ → ℂ) (ρ : ℂ) {σ : ℝ}
    (hO : (fun n => abelPartialSum a n - n • ρ) =O[atTop]
      fun n => ((n : ℝ) ^ σ : ℝ))
    {s : ℂ} (hs : σ < s.re) (hs1 : s ≠ 1) :
    AnalyticAt ℂ (linearAsymptoticDirichletContinuation a ρ) s

Uses 5 · Used by 1

Statement usesPartial sums of a coefficient sequence · Linear asymptotic Dirichlet continuation

Proof usesAbel continuation of a Dirichlet series · Analyticity of the Abel continuation · Growth bound for the partial sums of a shifted sequence

Used byMeromorphy of the linear asymptotic continuation on a half-plane

TheoremCleared-denominator form of the linear asymptotic continuation#✓fully proved

Let \(a : \mathbb{N} \to \mathbb{C}\) and \(\rho \in \mathbb{C}\), let \(L_{a,\rho}\) be the linear asymptotic Dirichlet continuation of \(a\) with constant \(\rho\), and let \(F_{a-\rho}\) be the Abel continuation of the sequence \(n \mapsto a(n) - \rho\). Let \(\zeta_1 : \mathbb{C} \to \mathbb{C}\) be the function with \(\zeta_1(s) = (s - 1)\,\zeta(s)\) for \(s \neq 1\) and \(\zeta_1(1) = 1\), where \(\zeta\) is the Riemann zeta function. Then for every \(s \in \mathbb{C}\) with \(s \neq 1\),

\[ L_{a,\rho}(s) = (s - 1)^{-1} \bigl(\rho\,\zeta_1(s) + (s - 1)\,F_{a-\rho}(s)\bigr). \]

theorem linearAsymptoticDirichletContinuation_eq_inv_sub_mul
    (a : ℕ → ℂ) (ρ : ℂ) {s : ℂ} (hs : s ≠ 1) :
    linearAsymptoticDirichletContinuation a ρ s =
      (s - 1)⁻¹ *
        (ρ * riemannZeta₁ s + (s - 1) * abelContinuation (fun n => a n - ρ) s)

Uses 2 · Used by 3

Statement usesAbel continuation of a Dirichlet series · Linear asymptotic Dirichlet continuation

Used byMeromorphy of the linear asymptotic continuation at \(1\) · The linear asymptotic continuation has a simple pole at \(1\) · Limit of the linear asymptotic continuation times \(s - 1\) at \(1\)

TheoremMeromorphy of the linear asymptotic continuation at \(1\)#✓fully proved

Let \(a : \mathbb{N} \to \mathbb{C}\), \(\rho \in \mathbb{C}\) and \(\sigma \in \mathbb{R}\) with \(\sigma < 1\), and suppose that the one-based partial sums \(A(n) = \sum_{k=1}^{n} a(k)\) satisfy \(A(n) - n\rho = O(n^{\sigma})\) as \(n \to \infty\). Then the linear asymptotic Dirichlet continuation \(L_{a,\rho}\) of \(a\) with constant \(\rho\) is meromorphic at \(s = 1\).

theorem meromorphicAt_linearAsymptoticDirichletContinuation_one
    (a : ℕ → ℂ) (ρ : ℂ) {σ : ℝ} (hσ1 : σ < 1)
    (hO : (fun n => abelPartialSum a n - n • ρ) =O[atTop]
      fun n => ((n : ℝ) ^ σ : ℝ)) :
    MeromorphicAt (linearAsymptoticDirichletContinuation a ρ) 1

Uses 6 · Used by 2

Statement usesPartial sums of a coefficient sequence · Linear asymptotic Dirichlet continuation

Proof usesAbel continuation of a Dirichlet series · Analyticity of the Abel continuation · Growth bound for the partial sums of a shifted sequence · Cleared-denominator form of the linear asymptotic continuation

Used byMeromorphy of the linear asymptotic continuation on a half-plane · The linear asymptotic continuation has a simple pole at \(1\)

TheoremThe linear asymptotic continuation has a simple pole at \(1\)#✓fully proved

Let \(a : \mathbb{N} \to \mathbb{C}\), \(\rho \in \mathbb{C}\) with \(\rho \neq 0\) and \(\sigma \in \mathbb{R}\) with \(\sigma < 1\), and suppose that the one-based partial sums \(A(n) = \sum_{k=1}^{n} a(k)\) satisfy \(A(n) - n\rho = O(n^{\sigma})\) as \(n \to \infty\). Then the meromorphic order at \(s = 1\) of the linear asymptotic Dirichlet continuation \(L_{a,\rho}\) of \(a\) with constant \(\rho\) is \(-1\).

theorem meromorphicOrderAt_linearAsymptoticDirichletContinuation_one
    (a : ℕ → ℂ) (ρ : ℂ) {σ : ℝ} (hσ1 : σ < 1)
    (hO : (fun n => abelPartialSum a n - n • ρ) =O[atTop]
      fun n => ((n : ℝ) ^ σ : ℝ)) (hρ : ρ ≠ 0) :
    meromorphicOrderAt (linearAsymptoticDirichletContinuation a ρ) 1 =
      ((-1 : ℤ) : WithTop ℤ)

Uses 7

Statement usesPartial sums of a coefficient sequence · Linear asymptotic Dirichlet continuation

Proof usesAbel continuation of a Dirichlet series · Analyticity of the Abel continuation · Growth bound for the partial sums of a shifted sequence · Cleared-denominator form of the linear asymptotic continuation · Meromorphy of the linear asymptotic continuation at \(1\)

TheoremLimit of the linear asymptotic continuation times \(s - 1\) at \(1\)#✓fully proved

Let \(a : \mathbb{N} \to \mathbb{C}\), \(\rho \in \mathbb{C}\) and \(\sigma \in \mathbb{R}\) with \(\sigma < 1\), and suppose that the one-based partial sums \(A(n) = \sum_{k=1}^{n} a(k)\) satisfy \(A(n) - n\rho = O(n^{\sigma})\) as \(n \to \infty\). Let \(L_{a,\rho}\) be the linear asymptotic Dirichlet continuation of \(a\) with constant \(\rho\). Then \((s - 1)\,L_{a,\rho}(s) \to \rho\) as \(s \to 1\) with \(s \neq 1\).

theorem tendsto_sub_one_mul_linearAsymptoticDirichletContinuation
    (a : ℕ → ℂ) (ρ : ℂ) {σ : ℝ} (hσ1 : σ < 1)
    (hO : (fun n => abelPartialSum a n - n • ρ) =O[atTop]
      fun n => ((n : ℝ) ^ σ : ℝ)) :
    Tendsto (fun s : ℂ =>
      (s - 1) * linearAsymptoticDirichletContinuation a ρ s)
      (𝓝[≠] (1 : ℂ)) (𝓝 ρ)

Uses 6

Statement usesPartial sums of a coefficient sequence · Linear asymptotic Dirichlet continuation

Proof usesAbel continuation of a Dirichlet series · Analyticity of the Abel continuation · Growth bound for the partial sums of a shifted sequence · Cleared-denominator form of the linear asymptotic continuation

TheoremMeromorphy of the linear asymptotic continuation on a half-plane#✓fully proved

Let \(a : \mathbb{N} \to \mathbb{C}\), \(\rho \in \mathbb{C}\) and \(\sigma \in \mathbb{R}\) with \(\sigma < 1\), and suppose that the one-based partial sums \(A(n) = \sum_{k=1}^{n} a(k)\) satisfy \(A(n) - n\rho = O(n^{\sigma})\) as \(n \to \infty\). Then the linear asymptotic Dirichlet continuation \(L_{a,\rho}\) of \(a\) with constant \(\rho\) is meromorphic at every point of the half-plane \(\{s \in \mathbb{C} : \operatorname{Re} s > \sigma\}\).

theorem meromorphicOn_linearAsymptoticDirichletContinuation
    (a : ℕ → ℂ) (ρ : ℂ) {σ : ℝ} (hσ1 : σ < 1)
    (hO : (fun n => abelPartialSum a n - n • ρ) =O[atTop]
      fun n => ((n : ℝ) ^ σ : ℝ)) :
    MeromorphicOn (linearAsymptoticDirichletContinuation a ρ)
      {s : ℂ | σ < s.re}

Uses 4

Statement usesPartial sums of a coefficient sequence · Linear asymptotic Dirichlet continuation

Proof usesAnalyticity of the linear asymptotic continuation away from \(1\) · Meromorphy of the linear asymptotic continuation at \(1\)

TheoremConvergence of the Dirichlet series to the linear asymptotic continuation#✓fully proved

Let \(a : \mathbb{N} \to \mathbb{C}\), \(\rho \in \mathbb{C}\) and \(\sigma \in \mathbb{R}\) with \(\sigma < 1\), and suppose that the one-based partial sums \(A(n) = \sum_{k=1}^{n} a(k)\) satisfy \(A(n) - n\rho = O(n^{\sigma})\) as \(n \to \infty\). Then for every \(s \in \mathbb{C}\) with \(\operatorname{Re} s > 1\), the partial sums \(\sum_{n=1}^{N} a(n)\, n^{-s}\) converge, as \(N \to \infty\), to \(L_{a,\rho}(s)\), where \(L_{a,\rho}\) is the linear asymptotic Dirichlet continuation of \(a\) with constant \(\rho\).

theorem tendsto_linearAsymptoticDirichletContinuation_Icc
    (a : ℕ → ℂ) (ρ : ℂ) {σ : ℝ} (hσ1 : σ < 1)
    (hO : (fun n => abelPartialSum a n - n • ρ) =O[atTop]
      fun n => ((n : ℝ) ^ σ : ℝ))
    {s : ℂ} (hs : 1 < s.re) :
    Tendsto (fun N => ∑ n ∈ Finset.Icc 1 N, LSeries.term a s n) atTop
      (𝓝 (linearAsymptoticDirichletContinuation a ρ s))

Uses 5

Statement usesPartial sums of a coefficient sequence · Linear asymptotic Dirichlet continuation

Proof usesAbel continuation of a Dirichlet series · Growth bound for the partial sums of a shifted sequence · Abel continuation as the limit of Dirichlet partial sums

22 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.