zeroTendstoDiff to residueAtZero

LemmazeroTendstoDiff#

If the limit of \(0\) is \(L_1 - L_2\), then \(L_1 = L_2\).

Proof

Obvious.

Lean

Formalized as zeroTendstoDiff.

Sources
LeanzeroTendstoDiff
Used by 2
Used byformulaLtOne · contourPull3

LemmaRectangleIntegral-tendsTo-VerticalIntegral#

Let \(\sigma,\sigma' \in \mathbb{R}\), and \(f : \mathbb{C} \to \mathbb{C}\) such that the vertical integrals \(\int_{(\sigma)}f(s)ds\) and \(\int_{(\sigma')}f(s)ds\) exist and the horizontal integral \(\int_{(\sigma)}^{\sigma'}f(x + yi)dx\) vanishes as \(y \to \pm \infty\). Then the limit of rectangle integrals

\[ \lim_{T\to\infty}\int_{\sigma-iT}^{\sigma'+iT}f(s)ds = \int_{(\sigma')}f(s)ds - \int_{(\sigma)}f(s)ds. \]
Proof

Almost by definition.

Lean

Formalized as RectangleIntegral_tendsTo_VerticalIntegral.

Sources
LeanRectangleIntegral_tendsTo_VerticalIntegral
Uses 2 · Used by 4
Statement usesRectangleIntegral · VerticalIntegral
Used byformulaLtOne · contourPull3 · residuePull1 · residuePull2

LemmaRectangleIntegral-tendsTo-UpperU#

Let \(\sigma,\sigma' \in \mathbb{R}\), and \(f : \mathbb{C} \to \mathbb{C}\) such that the vertical integrals \(\int_{(\sigma)}f(s)ds\) and \(\int_{(\sigma')}f(s)ds\) exist and the horizontal integral \(\int_{(\sigma)}^{\sigma'}f(x + yi)dx\) vanishes as \(y \to \pm \infty\). Then the limit of rectangle integrals

\[ \int_{\sigma+iT}^{\sigma'+iU}f(s)ds \]

as \(U\to\infty\) is the “UpperUIntegral” of \(f\).

Proof

Almost by definition.

Lean

Formalized as RectangleIntegral_tendsTo_UpperU.

Sources
LeanRectangleIntegral_tendsTo_UpperU
Uses 2
Statement usesUpperUIntegral · RectangleIntegral

LemmaRectangleIntegral-tendsTo-LowerU#

Let \(\sigma,\sigma' \in \mathbb{R}\), and \(f : \mathbb{C} \to \mathbb{C}\) such that the vertical integrals \(\int_{(\sigma)}f(s)ds\) and \(\int_{(\sigma')}f(s)ds\) exist and the horizontal integral \(\int_{(\sigma)}^{\sigma'}f(x + yi)dx\) vanishes as \(y \to -\infty\). Then the limit of rectangle integrals

\[ \int_{\sigma-iU}^{\sigma'-iT}f(s)ds \]

as \(U\to\infty\) is the “LowerUIntegral” of \(f\).

Proof

Almost by definition.

Lean

Formalized as RectangleIntegral_tendsTo_LowerU.

Sources
LeanRectangleIntegral_tendsTo_LowerU
Uses 2
Statement usesLowerUIntegral · RectangleIntegral

TODO : Move to general section

LemmalimitOfConstant#

Let \(a:\mathbb{R}\to\mathbb{C}\) be a function, and let \(\sigma>0\) be a real number. Suppose that, for all \(\sigma, \sigma'>0\), we have \(a(\sigma')=a(\sigma)\), and that \(\lim_{\sigma\to\infty}a(\sigma)=0\). Then \(a(\sigma)=0\).

Proof
\[ \begin{aligned} \lim_{\sigma'\to\infty}a(\sigma) &= \lim_{\sigma'\to\infty}a(\sigma') \\ &= 0 \end{aligned} \]
Lean

Formalized as limitOfConstant.

Sources
LeanlimitOfConstant
Used by 1
Used byformulaLtOne

LemmalimitOfConstantLeft#

Let \(a:\mathbb{R}\to\mathbb{C}\) be a function, and let \(\sigma<-3/2\) be a real number. Suppose that, for all \(\sigma, \sigma'>0\), we have \(a(\sigma')=a(\sigma)\), and that \(\lim_{\sigma\to-\infty}a(\sigma)=0\). Then \(a(\sigma)=0\).

Proof
\[ \begin{aligned} \lim_{\sigma'\to-\infty}a(\sigma) &= \lim_{\sigma'\to-\infty}a(\sigma') \\ &= 0 \end{aligned} \]
Lean

Formalized as limitOfConstantLeft.

Sources
LeanlimitOfConstantLeft
Used by 1
Used byformulaGtOne

Lemmatendsto-rpow-atTop-nhds-zero-of-norm-lt-one#

Let \(x>0\) and \(x<1\). Then

\[ \lim_{\sigma\to\infty}x^\sigma=0. \]
Proof

Standard.

Lean

Formalized as tendsto_rpow_atTop_nhds_zero_of_norm_lt_one.

Sources
Leantendsto_rpow_atTop_nhds_zero_of_norm_lt_one
Used by 2
Used byformulaLtOne · tendsto-rpow-atTop-nhds-zero-of-norm-gt-one

Lemmatendsto-rpow-atTop-nhds-zero-of-norm-gt-one#

Let \(x>1\). Then

\[ \lim_{\sigma\to-\infty}x^\sigma=0. \]
Proof

Standard.

Lean

Formalized as tendsto_rpow_atTop_nhds_zero_of_norm_gt_one.

Sources
Leantendsto_rpow_atTop_nhds_zero_of_norm_gt_one
Uses 1 · Used by 1
Proof usestendsto-rpow-atTop-nhds-zero-of-norm-lt-one
Used byformulaGtOne

LemmaisHolomorphicOn#

Let \(x>0\). Then the function \(f(s) = x^s/(s(s+1))\) is holomorphic on the half-plane \(\{s\in\mathbb{C}:\Re(s)>0\}\).

Proof

Composition of differentiabilities.

Lean

Formalized as Perron.isHolomorphicOn.

Sources
LeanPerron.isHolomorphicOn
Used by 7
Used byformulaLtOne · isIntegrable · residueAtZero · contourPull3 · residueAtNegOne · residuePull1 · residuePull2

LemmaintegralPosAux#

The integral

\[ \int_\mathbb{R}\frac{1}{|(1+t^2)(2+t^2)|^{1/2}}dt \]

is positive (and hence convergent - since a divergent integral is zero in Lean, by definition).

Proof

This integral is between \(\frac{1}{2}\) and \(1\) of the integral of \(\frac{1}{1+t^2}\), which is \(\pi\).

Lean

Formalized as Perron.integralPosAux.

Sources
LeanPerron.integralPosAux
Used by 2
Used byformulaLtOne · vertIntBound

LemmavertIntBound#

Let \(x>0\) and \(\sigma>1\). Then

\[ \left| \int_{(\sigma)}\frac{x^s}{s(s+1)}ds\right| \leq x^\sigma \int_\mathbb{R}\frac{1}{|(1+t ^ 2)(2+t ^ 2)|^{1/2}}dt. \]
Proof

Triangle inequality and pointwise estimate.

Lean

Formalized as Perron.vertIntBound.

Sources
LeanPerron.vertIntBound
Uses 2 · Used by 1
Statement usesVerticalIntegral
Proof usesintegralPosAux
Used byformulaLtOne

LemmavertIntBoundLeft#

Let \(x>1\) and \(\sigma<-3/2\). Then

\[ \left| \int_{(\sigma)}\frac{x^s}{s(s+1)}ds\right| \leq x^\sigma \int_\mathbb{R}\frac{1}{|(1/4+t ^ 2)(2+t ^ 2)|^{1/2}}dt. \]
Proof

Triangle inequality and pointwise estimate.

Lean

Formalized as Perron.vertIntBoundLeft.

Sources
LeanPerron.vertIntBoundLeft
Uses 1 · Used by 1
Statement usesVerticalIntegral
Used byformulaGtOne

LemmaisIntegrable#

Let \(x>0\) and \(\sigma\in\mathbb{R}\). Then

\[ \int_{\mathbb{R}}\frac{x^{\sigma+it}}{(\sigma+it)(1+\sigma + it)}dt \]

is integrable.

Proof

By isHolomorphicOn, \(f\) is continuous, so it is integrable on any interval.

Also, \(|f(x)| = \Theta(x^{-2})\) as \(x\to\infty\),

and \(|f(-x)| = \Theta(x^{-2})\) as \(x\to\infty\).

Since \(g(x) = x^{-2}\) is integrable on \([a,\infty)\) for any \(a>0\), we conclude.

Lean

Formalized as Perron.isIntegrable.

Sources
LeanPerron.isIntegrable
Uses 1 · Used by 4
Proof usesisHolomorphicOn
Used byformulaLtOne · contourPull3 · residuePull1 · residuePull2

Lemmatendsto-zero-Lower#

Let \(x>0\) and \(\sigma',\sigma''\in\mathbb{R}\). Then

\[ \int_{\sigma'}^{\sigma''}\frac{x^{\sigma+it}}{(\sigma+it)(1+\sigma + it)}d\sigma \]

goes to \(0\) as \(t\to-\infty\).

Proof

The numerator is bounded and the denominator tends to infinity.

Lean

Formalized as Perron.tendsto_zero_Lower.

Sources
LeanPerron.tendsto_zero_Lower
Used by 4
Used byformulaLtOne · contourPull3 · residuePull1 · residuePull2

Lemmatendsto-zero-Upper#

Let \(x>0\) and \(\sigma',\sigma''\in\mathbb{R}\). Then

\[ \int_{\sigma'}^{\sigma''}\frac{x^{\sigma+it}}{(\sigma+it)(1+\sigma + it)}d\sigma \]

goes to \(0\) as \(t\to\infty\).

Proof

The numerator is bounded and the denominator tends to infinity.

Lean

Formalized as Perron.tendsto_zero_Upper.

Sources
LeanPerron.tendsto_zero_Upper
Used by 4
Used byformulaLtOne · contourPull3 · residuePull1 · residuePull2

We are ready for the first case of the Perron formula, namely when \(x<1\):

LemmaformulaLtOne#

For \(x>0\), \(\sigma>0\), and \(x<1\), we have

\[ \frac1{2\pi i} \int_{(\sigma)}\frac{x^s}{s(s+1)}ds =0. \]
Proof

Let \(f(s) = x^s/(s(s+1))\). Then \(f\) is holomorphic on the half-plane \(\{s\in\mathbb{C}:\Re(s)>0\}\). The rectangle integral of \(f\) with corners \(\sigma-iT\) and \(\sigma+iT\) is zero. The limit of this rectangle integral as \(T\to\infty\) is \(\int_{(\sigma')}-\int_{(\sigma)}\). Therefore, \(\int_{(\sigma')}=\int_{(\sigma)}\).

But we also have the bound \(\int_{(\sigma')} \leq x^{\sigma'} * C\), where \(C=\int_\mathbb{R}\frac{1}{|(1+t)(1+t+1)|}dt\).

Therefore \(\int_{(\sigma')}\to 0\) as \(\sigma'\to\infty\).

So pulling contours gives \(\int_{(\sigma)}=0\).

Lean

Formalized as Perron.formulaLtOne.

Sources
LeanPerron.formulaLtOne
Uses 12
Statement usesVerticalIntegral
Proof usesvertIntBound · limitOfConstant · zeroTendstoDiff · tendsto-zero-Lower · isIntegrable · tendsto-zero-Upper · RectangleIntegral-tendsTo-VerticalIntegral · tendsto-rpow-atTop-nhds-zero-of-norm-lt-one · integralPosAux · RectangleIntegral · isHolomorphicOn

The second case is when \(x>1\). Here are some auxiliary lemmata for the second case. TODO: Move to more general section

LemmakeyIdentity#

Let \(x\in \mathbb{R}\) and \(s \ne 0, -1\). Then

\[ \frac{x^\sigma}{s(1+s)} = \frac{x^\sigma}{s} - \frac{x^\sigma}{1+s} \]
Proof

By ring.

Lean

Formalized as Perron.keyIdentity.

Sources
LeanPerron.keyIdentity
Used by 2
Used bydiffBddAtNegOne · diffBddAtZero

LemmadiffBddAtZero#

Let \(x>0\). Then for \(0 < c < 1 /2\), we have that the function

\[ s ↦ \frac{x^s}{s(s+1)} - \frac1s \]

is bounded above on the rectangle with corners at \(-c-i*c\) and \(c+i*c\) (except at \(s=0\)).

Proof

Applying Lemma keyIdentity, the function \(s ↦ x^s/s(s+1) - 1/s = x^s/s - x^0/s - x^s/(1+s)\). The last term is bounded for \(s\) away from \(-1\). The first two terms are the difference quotient of the function \(s ↦ x^s\) at \(0\); since it's differentiable, the difference remains bounded as \(s\to 0\).

Lean

Formalized as Perron.diffBddAtZero.

Sources
LeanPerron.diffBddAtZero
Uses 1 · Used by 1
Proof useskeyIdentity
Used byresidueAtZero

LemmadiffBddAtNegOne#

Let \(x>0\). Then for \(0 < c < 1 /2\), we have that the function

\[ s ↦ \frac{x^s}{s(s+1)} - \frac{-x^{-1}}{s+1} \]

is bounded above on the rectangle with corners at \(-1-c-i*c\) and \(-1+c+i*c\) (except at \(s=-1\)).

Proof

Applying Lemma keyIdentity, the function \(s ↦ x^s/s(s+1) - x^{-1}/(s+1) = x^s/s - x^s/(s+1) - (-x^{-1})/(s+1)\). The first term is bounded for \(s\) away from \(0\). The last two terms are the difference quotient of the function \(s ↦ x^s\) at \(-1\); since it's differentiable, the difference remains bounded as \(s\to -1\).

Lean

Formalized as Perron.diffBddAtNegOne.

Sources
LeanPerron.diffBddAtNegOne
Uses 1 · Used by 1
Proof useskeyIdentity
Used byresidueAtNegOne

LemmaresidueAtZero#

Let \(x>0\). Then for all sufficiently small \(c>0\), we have that

\[ \frac1{2\pi i} \int_{-c-i*c}^{c+ i*c}\frac{x^s}{s(s+1)}ds = 1. \]
Proof

For \(c>0\) sufficiently small,

\(x^s/(s(s+1))\) is equal to \(1/s\) plus a function, \(g\), say, holomorphic in the whole rectangle (by Lemma diffBddAtZero).

Now apply Lemma ResidueTheoremOnRectangleWithSimplePole.

Lean

Formalized as Perron.residueAtZero.

Sources
LeanPerron.residueAtZero
Uses 5 · Used by 1
Statement usesRectangleIntegral
Proof usesdiffBddAtZero · ResidueTheoremOnRectangleWithSimplePole · existsDifferentiableOn-of-bddAbove · isHolomorphicOn
Used byresiduePull1

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.