Perron's formula

DefinitionTruncated Perron kernel#✓fully proved

For real numbers \(y\), \(c\) and \(T\), the truncated Perron kernel is the complex number

\[K(y, c, T) = \frac{1}{2\pi}\int_{-T}^{T} \frac{y^{c+it}}{c+it}\,dt,\]

where \(y^s\) is the principal complex power of \(y\) viewed as a complex number.

Writing \(s = c + it\), this is \(\frac{1}{2\pi i}\int_{c-iT}^{c+iT} \frac{y^s}{s}\,ds\) along the vertical segment.

noncomputable def perronKernel (y c T : ℝ) : ℂ :=
  (1 / (2 * Real.pi)) * ∫ t : ℝ in (-T)..T,
    (y : ℂ) ^ ((c : ℂ) + t * Complex.I) / ((c : ℂ) + t * Complex.I)
Used by 3
Used byTruncated Perron formula · Truncated Perron bound for \(y > 1\) · Truncated Perron bound for \(0 < y < 1\)

TheoremContinuity of the Perron kernel integrand#✓fully proved

Let \(y > 0\) and \(c \ne 0\) be real numbers. Then the function from \(\mathbb{R}\) to \(\mathbb{C}\) sending \(t\) to \(y^{c+it}/(c+it)\), where \(y^{c+it}\) is the complex power, is continuous.

theorem continuous_perronKernel_integrand {y c : ℝ} (hy : 0 < y) (hc : c ≠ 0) :
    Continuous (fun t : ℝ => (y : ℂ) ^ ((c : ℂ) + t * Complex.I) / ((c : ℂ) + t * Complex.I))

TheoremIntegral formula for \(e^w - 1\)#✓fully proved

For every complex number \(w\),

\[e^w - 1 = w \int_0^1 e^{tw}\,dt,\]

where \(t\) ranges over the real interval \([0, 1]\).

theorem exp_sub_one_eq (w : ℂ) :
    Complex.exp w - 1 = w * ∫ t : ℝ in (0:ℝ)..1, Complex.exp (t * w)
Used by 1
Used byThe averaging operator as a difference quotient

DefinitionThe averaging operator \(E_1\)#✓fully proved

For a complex number \(u\), define \(E_1(u) = \int_0^1 e^{tu}\,dt\), the integral being over real \(t\) from \(0\) to \(1\).

noncomputable def E1 (u : ℂ) : ℂ := ∫ t : ℝ in (0:ℝ)..1, Complex.exp (t * u)
Used by 11
Used byContinuity of the averaging operator · Continuity of the averaging operator at zero · The averaging operator is entire · The averaging operator as a difference quotient · Derivative of the averaging operator · Linear bound for the averaging operator near zero · Value of the averaging operator at zero · Perron remainder · The Perron remainder is entire · The Perron remainder as a difference quotient · Slope of the Perron remainder at the origin

TheoremValue of the averaging operator at zero#✓fully proved

Let \(E_1(u) = \int_0^1 e^{tu}\,dt\) for \(u \in \mathbb{C}\). Then \(E_1(0) = 1\).

theorem E1_zero : E1 0 = 1
Uses 1 · Used by 3
Statement usesThe averaging operator \(E_1\)
Used byContinuity of the averaging operator at zero · Linear bound for the averaging operator near zero · Slope of the Perron remainder at the origin

TheoremThe averaging operator as a difference quotient#✓fully proved

Let \(E_1(u) = \int_0^1 e^{tu}\,dt\) for \(u \in \mathbb{C}\). Then \(E_1(u) = (e^u - 1)/u\) for every nonzero complex number \(u\).

theorem E1_eq_div (u : ℂ) (hu : u ≠ 0) : E1 u = (Complex.exp u - 1) / u
Uses 2 · Used by 4
Statement usesThe averaging operator \(E_1\)
Proof usesIntegral formula for \(e^w - 1\)
Used byContinuity of the averaging operator · Linear bound for the averaging operator near zero · The Perron remainder as a difference quotient · Slope of the Perron remainder at the origin

TheoremLinear bound for the averaging operator near zero#✓fully proved

Let \(E_1(u) = \int_0^1 e^{tu}\,dt\) for \(u \in \mathbb{C}\). For every complex number \(v\) with \(|v| \le 1\), we have \(|E_1(v) - 1| \le |v|\).

theorem E1_sub_one_le (v : ℂ) (hv : ‖v‖ ≤ 1) : ‖E1 v - 1‖ ≤ ‖v‖
Uses 3 · Used by 1
Statement usesThe averaging operator \(E_1\)
Proof usesThe averaging operator as a difference quotient · Value of the averaging operator at zero
Used byContinuity of the averaging operator at zero

TheoremContinuity of the averaging operator at zero#✓fully proved

The function \(E_1 : \mathbb{C} \to \mathbb{C}\) given by \(E_1(u) = \int_0^1 e^{tu}\,dt\) is continuous at \(0\).

theorem E1_continuousAt_zero : ContinuousAt E1 0
Uses 3 · Used by 1
Statement usesThe averaging operator \(E_1\)
Proof usesLinear bound for the averaging operator near zero · Value of the averaging operator at zero
Used byContinuity of the averaging operator

TheoremContinuity of the averaging operator#✓fully proved

The function \(E_1 : \mathbb{C} \to \mathbb{C}\) given by \(E_1(u) = \int_0^1 e^{tu}\,dt\) is continuous.

theorem E1_continuous : Continuous E1
Uses 3
Statement usesThe averaging operator \(E_1\)
Proof usesContinuity of the averaging operator at zero · The averaging operator as a difference quotient

TheoremDerivative of the averaging operator#✓fully proved

Let \(E_1(u) = \int_0^1 e^{tu}\,dt\) for \(u \in \mathbb{C}\). For every \(x_0 \in \mathbb{C}\), the function \(E_1\) has complex derivative \(\int_0^1 t\,e^{t x_0}\,dt\) at \(x_0\).

theorem E1_hasDerivAt (x₀ : ℂ) :
    HasDerivAt E1 (∫ t in (0:ℝ)..1, (t : ℂ) * Complex.exp ((t : ℂ) * x₀)) x₀
Uses 1 · Used by 1
Statement usesThe averaging operator \(E_1\)
Used byThe averaging operator is entire

TheoremThe averaging operator is entire#✓fully proved

The function \(E_1 : \mathbb{C} \to \mathbb{C}\) given by \(E_1(u) = \int_0^1 e^{tu}\,dt\) is complex differentiable at every point of \(\mathbb{C}\).

theorem E1_differentiable : Differentiable ℂ E1
Uses 2 · Used by 1
Statement usesThe averaging operator \(E_1\)
Proof usesDerivative of the averaging operator
Used byThe Perron remainder is entire

DefinitionPerron remainder#✓fully proved

For a real number \(y\) and a complex number \(s\), the Perron remainder is \(R_y(s) = \log y \cdot E_1(s \log y)\), where \(E_1(u) = \int_0^1 e^{tu}\,dt\) is the averaging operator and \(\log\) is the real logarithm (extended by \(\log 0 = 0\) and \(\log y = \log |y|\) for \(y < 0\)).

The function \(R_y\) is entire, and for \(y > 0\) it agrees with \((y^s - 1)/s\) for \(s \neq 0\).

noncomputable def perronRemainder (y : ℝ) (s : ℂ) : ℂ :=
  Real.log y * E1 (s * Real.log y)
Uses 1 · Used by 6
Statement usesThe averaging operator \(E_1\)
Used bySplitting off the pole of the Perron kernel quotient · The Perron remainder is entire · The Perron remainder as a difference quotient · Slope of the Perron remainder at the origin · Rectangle integral of \(y^s/s\) around the origin · Rectangle integral of \(y^s/s\) with the pole outside

TheoremThe Perron remainder is entire#✓fully proved

For a real number \(y\), the Perron remainder is the function \(R_y(s) = \log y \int_0^1 e^{ts\log y}\,dt\) of \(s \in \mathbb{C}\), where \(\log y = \log|y|\) for \(y \ne 0\) and \(\log 0 = 0\). For every real \(y\), the function \(R_y\) is complex differentiable at every point of \(\mathbb{C}\).

theorem perronRemainder_differentiable (y : ℝ) :
    Differentiable ℂ (perronRemainder y)
Uses 3 · Used by 2
Statement usesPerron remainder
Proof usesThe averaging operator \(E_1\) · The averaging operator is entire
Used byRectangle integral of \(y^s/s\) around the origin · Rectangle integral of \(y^s/s\) with the pole outside

TheoremThe Perron remainder as a difference quotient#✓fully proved

For every real \(y > 0\) and every complex \(s \neq 0\), the Perron remainder \(R_y\) satisfies \(R_y(s) = (y^s - 1)/s\), where \(y^s = e^{s \log y}\).

theorem perronRemainder_eq_div {y : ℝ} (hy : 0 < y) {s : ℂ} (hs : s ≠ 0) :
    perronRemainder y s = ((y : ℂ) ^ s - 1) / s
Uses 3 · Used by 1
Statement usesPerron remainder
Proof usesThe averaging operator \(E_1\) · The averaging operator as a difference quotient
Used bySplitting off the pole of the Perron kernel quotient

TheoremSlope of the Perron remainder at the origin#✓fully proved

For every real \(y\) and every complex \(h \neq 0\), the Perron remainder \(R_y\) satisfies

\[\frac{R_y(h) - R_y(0)}{h} = (\log y)^2 \int_0^1 t \, E_1(t h \log y)\,dt,\]

where \(E_1(u) = \int_0^1 e^{\tau u}\,d\tau\) is the averaging operator and \(\log\) is the real logarithm (extended by \(\log 0 = 0\) and \(\log y = \log |y|\) for \(y < 0\)).

theorem perronRemainder_slope {y : ℝ} {h : ℂ} (hh : h ≠ 0) :
    (perronRemainder y h - perronRemainder y 0) / h
      = (Real.log y : ℂ) ^ 2 * ∫ t : ℝ in (0:ℝ)..1, t * E1 (t * h * Real.log y)
Uses 4
Statement usesThe averaging operator \(E_1\) · Perron remainder
Proof usesThe averaging operator as a difference quotient · Value of the averaging operator at zero

TheoremModulus of a complex power of a positive real#✓fully proved

For every real \(y > 0\) and every complex number \(s\), \(|y^s| = \exp(\operatorname{Re}(s) \log y)\), where \(y^s\) is the principal complex power.

theorem norm_cpow_ofReal {y : ℝ} (hy : 0 < y) (s : ℂ) :
    ‖(y : ℂ) ^ s‖ = Real.exp (s.re * Real.log y)
Used by 3
Used byHorizontal side bound for the Perron integrand on \((c, U)\) · Horizontal side bound for the Perron integrand when \(y > 1\) · Bound for the integral of \(y^s/s\) along a vertical segment

TheoremSplitting off the pole of the Perron kernel quotient#✓fully proved

Let \(y > 0\) be real and let \(s \ne 0\) be complex. Then \(y^s/s = R_y(s) + 1/s\), where \(R_y(s) = \log y \cdot E_1(s \log y)\) is the Perron remainder and \(E_1(u) = \int_0^1 e^{tu}\,dt\).

theorem cpow_div_eq_remainder_add {y : ℝ} (hy : 0 < y) {s : ℂ} (hs : s ≠ 0) :
    (y : ℂ) ^ s / s = perronRemainder y s + 1 / s
Uses 2 · Used by 2
Statement usesPerron remainder
Proof usesThe Perron remainder as a difference quotient
Used byRectangle integral of \(y^s/s\) around the origin · Rectangle integral of \(y^s/s\) with the pole outside

TheoremIntegral of \(\exp(Lx)\)#✓fully proved

For real numbers \(L \ne 0\), \(a\) and \(b\),

\[\int_a^b \exp(Lx)\,dx = \frac{\exp(Lb) - \exp(La)}{L},\]

where the integral is oriented: \(\int_a^b = -\int_b^a\) when \(a > b\).

theorem integral_exp_mul {L a b : ℝ} (hL : L ≠ 0) :
    ∫ x : ℝ in a..b, Real.exp (L * x)
      = (Real.exp (L * b) - Real.exp (L * a)) / L
Used by 2
Used byHorizontal side bound for the Perron integrand on \((c, U)\) · Horizontal side bound for the Perron integrand when \(y > 1\)

TheoremHorizontal side bound for the Perron integrand when \(y > 1\)#✓fully proved

Let \(y > 1\), let \(U > 0\), \(c > 0\) and \(T > 0\) be real numbers, and let \(\tau = T\) or \(\tau = -T\). Then

\[\left|\int_{-U}^{c} \frac{y^{x+i\tau}}{x+i\tau}\,dx\right| \le \frac{\exp(c\log y)}{T\log y},\]

where \(y^s = \exp(s \log y)\) is the principal complex power. The bound does not depend on \(U\).

theorem horiz_side_bound_gt_one {y U c T e : ℝ} (hy : 0 < y) (hy1 : 1 < y)
    (hU : 0 < U) (hc : 0 < c) (hT : 0 < T) (he : e = T ∨ e = -T) :
    ‖∫ x : ℝ in (-U)..c, (y : ℂ) ^ ((x : ℂ) + (e : ℂ) * Complex.I)
      / ((x : ℂ) + (e : ℂ) * Complex.I)‖
      ≤ Real.exp (Real.log y * c) / Real.log y / T
Uses 2 · Used by 1
Proof usesIntegral of \(\exp(Lx)\) · Modulus of a complex power of a positive real
Used byTruncated Perron bound for \(y > 1\)

TheoremBound for the integral of \(y^s/s\) along a vertical segment#✓fully proved

Let \(y, d, T\) be real numbers with \(y > 0\), \(d \neq 0\) and \(T > 0\), and write \(y^s = e^{s \log y}\). Then

\[\left| \int_{-T}^{T} \frac{y^{d + it}}{d + it}\,dt \right| \le 2T \cdot \frac{e^{d \log y}}{|d|},\]

that is, at most \(2T y^d/|d|\).

theorem vert_side_bound {y d T : ℝ} (hy : 0 < y) (hd : d ≠ 0) (hT : 0 < T) :
    ‖∫ t : ℝ in (-T)..T, (y : ℂ) ^ ((d : ℂ) + (t : ℂ) * Complex.I)
      / ((d : ℂ) + (t : ℂ) * Complex.I)‖
      ≤ 2 * T * (Real.exp (Real.log y * d) / |d|)
Uses 1 · Used by 2
Proof usesModulus of a complex power of a positive real
Used byBound for the integral of \(y^s/s\) along the left vertical side · Bound for the integral of \(y^s/s\) along the right vertical side

TheoremBound for the integral of \(y^s/s\) along the left vertical side#✓fully proved

Let \(y, U, T\) be real numbers with \(y > 0\), \(U > 0\) and \(T > 0\), and write \(y^s = e^{s \log y}\). Then

\[\left| \int_{-T}^{T} \frac{y^{-U + it}}{-U + it}\,dt \right| \le 2T \cdot \frac{e^{-U \log y}}{U},\]

that is, at most \(2T y^{-U}/U\). This is the vertical segment bound at real part \(-U\).

theorem vert_side_bound_left {y U T : ℝ} (hy : 0 < y) (hU : 0 < U) (hT : 0 < T) :
    ‖∫ t : ℝ in (-T)..T, (y : ℂ) ^ (((-U : ℝ) : ℂ) + (t : ℂ) * Complex.I)
      / (((-U : ℝ) : ℂ) + (t : ℂ) * Complex.I)‖
      ≤ 2 * T * (Real.exp (Real.log y * (-U)) / U)
Uses 1 · Used by 1
Proof usesBound for the integral of \(y^s/s\) along a vertical segment
Used byTruncated Perron bound for \(y > 1\)

TheoremBound for the integral of \(y^s/s\) along the right vertical side#✓fully proved

Let \(y, U, T\) be real numbers with \(y > 0\), \(U > 0\) and \(T > 0\), and write \(y^s = e^{s \log y}\). Then

\[\left| \int_{-T}^{T} \frac{y^{U + it}}{U + it}\,dt \right| \le 2T \cdot \frac{e^{U \log y}}{U},\]

that is, at most \(2T y^{U}/U\). This is the vertical segment bound at real part \(U\).

theorem vert_side_bound_right {y U T : ℝ} (hy : 0 < y) (hU : 0 < U) (hT : 0 < T) :
    ‖∫ t : ℝ in (-T)..T, (y : ℂ) ^ (((U : ℝ) : ℂ) + (t : ℂ) * Complex.I)
      / (((U : ℝ) : ℂ) + (t : ℂ) * Complex.I)‖
      ≤ 2 * T * (Real.exp (Real.log y * U) / U)
Uses 1 · Used by 1
Proof usesBound for the integral of \(y^s/s\) along a vertical segment
Used byTruncated Perron bound for \(0 < y < 1\)

TheoremRectangle integral of \(y^s/s\) around the origin#✓fully proved

Let \(y, U, c, T\) be real numbers with \(y > 0\), \(U > 0\), \(c > 0\) and \(T > 0\), and write \(y^s = e^{s \log y}\). Then

\[\int_{-U}^{c} \frac{y^{x - iT}}{x - iT}\,dx - \int_{-U}^{c} \frac{y^{x + iT}}{x + iT}\,dx + i \left( \int_{-T}^{T} \frac{y^{c + it}}{c + it}\,dt - \int_{-T}^{T} \frac{y^{-U + it}}{-U + it}\,dt \right) = 2\pi i,\]

that is, the integral of \(y^s/s\) over the positively oriented boundary of the rectangle with corners \(-U - iT\) and \(c + iT\) equals \(2\pi i\).

The identity holds for every \(y > 0\); it is used to close the Perron contour to the left when \(y > 1\).

theorem rect_identity_gt_one {y U c T : ℝ} (hy : 0 < y) (hU : 0 < U) (hc : 0 < c)
    (hT : 0 < T) :
    (∫ x : ℝ in (-U)..c, (y : ℂ) ^ ((x : ℂ) + ((-T : ℝ) : ℂ) * Complex.I)
        / ((x : ℂ) + ((-T : ℝ) : ℂ) * Complex.I))
      - (∫ x : ℝ in (-U)..c, (y : ℂ) ^ ((x : ℂ) + ((T : ℝ) : ℂ) * Complex.I)
        / ((x : ℂ) + ((T : ℝ) : ℂ) * Complex.I))
      + Complex.I * ((∫ t : ℝ in (-T)..T, (y : ℂ) ^ ((c : ℂ) + (t : ℂ) * Complex.I)
          / ((c : ℂ) + (t : ℂ) * Complex.I))
        - (∫ t : ℝ in (-T)..T, (y : ℂ) ^ (((-U : ℝ) : ℂ) + (t : ℂ) * Complex.I)
          / (((-U : ℝ) : ℂ) + (t : ℂ) * Complex.I)))
      = 2 * Real.pi * Complex.I
Uses 4 · Used by 1
Proof usesRectangle integral of \(1/s\) around the origin · Splitting off the pole of the Perron kernel quotient · Perron remainder · The Perron remainder is entire
Used byTruncated Perron bound for \(y > 1\)

TheoremHorizontal side bound for the Perron integrand on \((c, U)\)#✓fully proved

Let \(y > 0\) with \(\log y \ne 0\), let \(c \le U\) and \(T > 0\) be real numbers, and let \(\tau = T\) or \(\tau = -T\). Then

\[\left|\int_c^U \frac{y^{x+i\tau}}{x+i\tau}\,dx\right| \le \frac{\exp(U\log y)-\exp(c\log y)}{T\log y},\]

where \(y^s = \exp(s \log y)\) is the principal complex power.

No sign condition on \(\log y\) is assumed.

theorem horiz_side_bound_exact {y U c T e : ℝ} (hy : 0 < y)
    (hcU : c ≤ U) (hT : 0 < T) (he : e = T ∨ e = -T) (hL : Real.log y ≠ 0) :
    ‖∫ x : ℝ in c..U, (y : ℂ) ^ ((x : ℂ) + (e : ℂ) * Complex.I)
      / ((x : ℂ) + (e : ℂ) * Complex.I)‖
      ≤ (Real.exp (Real.log y * U) - Real.exp (Real.log y * c))
        / Real.log y / T
Uses 2 · Used by 1
Proof usesIntegral of \(\exp(Lx)\) · Modulus of a complex power of a positive real
Used byTruncated Perron bound for \(0 < y < 1\)

TheoremRectangle integral of \(y^s/s\) with the pole outside#✓fully proved

Let \(y, U, c, T\) be real numbers with \(y > 0\), \(0 < c < U\) and \(T > 0\), and write \(y^s = e^{s \log y}\). Then

\[\int_{c}^{U} \frac{y^{x - iT}}{x - iT}\,dx - \int_{c}^{U} \frac{y^{x + iT}}{x + iT}\,dx + i \left( \int_{-T}^{T} \frac{y^{U + it}}{U + it}\,dt - \int_{-T}^{T} \frac{y^{c + it}}{c + it}\,dt \right) = 0,\]

that is, the integral of \(y^s/s\) over the positively oriented boundary of the rectangle with corners \(c - iT\) and \(U + iT\) vanishes.

The identity holds for every \(y > 0\); it is used to close the Perron contour to the right when \(y < 1\).

theorem rect_identity_lt_one {y U c T : ℝ} (hy : 0 < y) (hcU : c < U) (hc : 0 < c)
    (hT : 0 < T) :
    (∫ x : ℝ in c..U, (y : ℂ) ^ ((x : ℂ) + ((-T : ℝ) : ℂ) * Complex.I)
        / ((x : ℂ) + ((-T : ℝ) : ℂ) * Complex.I))
      - (∫ x : ℝ in c..U, (y : ℂ) ^ ((x : ℂ) + ((T : ℝ) : ℂ) * Complex.I)
        / ((x : ℂ) + ((T : ℝ) : ℂ) * Complex.I))
      + Complex.I * ((∫ t : ℝ in (-T)..T, (y : ℂ) ^ (((U : ℝ) : ℂ) + (t : ℂ) * Complex.I)
          / (((U : ℝ) : ℂ) + (t : ℂ) * Complex.I))
        - (∫ t : ℝ in (-T)..T, (y : ℂ) ^ ((c : ℂ) + (t : ℂ) * Complex.I)
          / ((c : ℂ) + (t : ℂ) * Complex.I)))
      = 0
Uses 4 · Used by 1
Proof usesRectangle integral of \(1/s\) with the pole outside · Splitting off the pole of the Perron kernel quotient · Perron remainder · The Perron remainder is entire
Used byTruncated Perron bound for \(0 < y < 1\)

TheoremTruncated Perron bound for \(y > 1\)#✓fully proved

Let \(y > 1\), \(c > 0\) and \(T > 0\) be real numbers, and let \(K(y, c, T) = \frac{1}{2\pi}\int_{-T}^{T} \frac{y^{c+it}}{c+it}\,dt\) be the truncated Perron kernel. Then

\[|K(y, c, T) - 1| \le \frac{\exp(c \log y)}{\pi T \log y}.\]

Here \(y^s\) is the principal complex power.

theorem perron_bound_gt_one {y c T : ℝ} (hy : 0 < y) (hy1 : 1 < y)
    (hc : 0 < c) (hT : 0 < T) :
    ‖perronKernel y c T - 1‖ ≤ Real.exp (Real.log y * c) / Real.log y / T / Real.pi
Uses 4 · Used by 1
Statement usesTruncated Perron kernel
Proof usesHorizontal side bound for the Perron integrand when \(y > 1\) · Rectangle integral of \(y^s/s\) around the origin · Bound for the integral of \(y^s/s\) along the left vertical side
Used byTruncated Perron formula

TheoremTruncated Perron bound for \(0 < y < 1\)#✓fully proved

Let \(0 < y < 1\), \(c > 0\) and \(T > 0\) be real numbers, and let \(K(y, c, T) = \frac{1}{2\pi}\int_{-T}^{T} \frac{y^{c+it}}{c+it}\,dt\) be the truncated Perron kernel. Then

\[|K(y, c, T)| \le \frac{\exp(c \log y)}{\pi T |\log y|}.\]

Here \(y^s\) is the principal complex power.

theorem perron_bound_lt_one {y c T : ℝ} (hy : 0 < y) (hylt : y < 1)
    (hc : 0 < c) (hT : 0 < T) :
    ‖perronKernel y c T‖ ≤ Real.exp (Real.log y * c) / |Real.log y| / T / Real.pi
Uses 4 · Used by 1
Statement usesTruncated Perron kernel
Proof usesHorizontal side bound for the Perron integrand on \((c, U)\) · Rectangle integral of \(y^s/s\) with the pole outside · Bound for the integral of \(y^s/s\) along the right vertical side
Used byTruncated Perron formula

TheoremTruncated Perron formula#✓fully proved

Let \(y > 0\) with \(y \ne 1\), and let \(c > 0\) and \(T > 0\) be real numbers. Let \(K(y, c, T) = \frac{1}{2\pi}\int_{-T}^{T} \frac{y^{c+it}}{c+it}\,dt\) be the truncated Perron kernel, and let \(\delta(y) = 1\) if \(y > 1\) and \(\delta(y) = 0\) if \(y < 1\). Then

\[|K(y, c, T) - \delta(y)| \le \frac{\exp(c \log y)}{\pi T |\log y|}.\]

Here \(y^s\) is the principal complex power.

theorem perron_bound {y c T : ℝ} (hy : 0 < y) (hy1 : y ≠ 1)
    (hc : 0 < c) (hT : 0 < T) :
    ‖perronKernel y c T - (if 1 < y then (1:ℂ) else 0)‖
      ≤ Real.exp (Real.log y * c) / |Real.log y| / T / Real.pi
Uses 3
Statement usesTruncated Perron kernel
Proof usesTruncated Perron bound for \(y > 1\) · Truncated Perron bound for \(0 < y < 1\)
28 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.