residueAtNegOne to formulaGtOne

LemmaresidueAtNegOne#

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

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

Compute the integral.

Lean

Formalized as Perron.residueAtNegOne.

Sources
LeanPerron.residueAtNegOne
Uses 5 · Used by 1
Statement usesRectangleIntegral
Proof usesResidueTheoremOnRectangleWithSimplePole · diffBddAtNegOne · existsDifferentiableOn-of-bddAbove · isHolomorphicOn
Used byresiduePull2

LemmaresiduePull1#

For \(x>1\) (of course \(x>0\) would suffice) and \(\sigma>0\), we have

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

We pull to a square with corners at \(-c-i*c\) and \(c+i*c\) for \(c>0\) sufficiently small. By Lemma residueAtZero, the integral over this square is equal to \(1\).

Lean

Formalized as Perron.residuePull1.

Sources
LeanPerron.residuePull1
Uses 10 · Used by 1
Statement usesVerticalIntegral
Proof usesresidueAtZero · HolomorphicOn.vanishesOnRectangle · tendsto-zero-Lower · isIntegrable · tendsto-zero-Upper · RectangleBorder · RectangleIntegral-tendsTo-VerticalIntegral · RectangleIntegral · isHolomorphicOn
Used byformulaGtOne

LemmaresiduePull2#

For \(x>1\), we have

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

Pull contour from \((-1/2)\) to \((-3/2)\).

Lean

Formalized as Perron.residuePull2.

Sources
LeanPerron.residuePull2
Uses 10 · Used by 1
Statement usesVerticalIntegral
Proof usesHolomorphicOn.vanishesOnRectangle · tendsto-zero-Lower · isIntegrable · tendsto-zero-Upper · RectangleBorder · residueAtNegOne · RectangleIntegral-tendsTo-VerticalIntegral · RectangleIntegral · isHolomorphicOn
Used byformulaGtOne

LemmacontourPull3#

For \(x>1\) and \(\sigma<-3/2\), we have

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

Pull contour from \((-3/2)\) to \((\sigma)\).

Lean

Formalized as Perron.contourPull3.

Sources
LeanPerron.contourPull3
Uses 8 · Used by 1
Statement usesVerticalIntegral
Proof useszeroTendstoDiff · tendsto-zero-Lower · isIntegrable · tendsto-zero-Upper · RectangleIntegral-tendsTo-VerticalIntegral · RectangleIntegral · isHolomorphicOn
Used byformulaGtOne

LemmaformulaGtOne#

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

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

Let \(f(s) = x^s/(s(s+1))\). Then \(f\) is holomorphic on \(\mathbb{C} \setminus {0,-1}\).

First pull the contour from \((\sigma)\) to \((-1/2)\), picking up a residue \(1\) at \(s=0\).

Next pull the contour from \((-1/2)\) to \((-3/2)\), picking up a residue \(-1/x\) at \(s=-1\).

Then pull the contour all the way to \((\sigma')\) with \(\sigma'<-3/2\).

For \(\sigma' < -3/2\), the integral is bounded by \(x^{\sigma'}\int_\mathbb{R}\frac{1}{|(1+t ^ 2)(2+t ^ 2)|^{1/2}}dt\).

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

So pulling contours gives \(\int_{(-3/2)}=0\).

Lean

Formalized as Perron.formulaGtOne.

Sources
LeanPerron.formulaGtOne
Uses 7
Statement usesVerticalIntegral
Proof usesvertIntBoundLeft · residuePull1 · tendsto-rpow-atTop-nhds-zero-of-norm-gt-one · residuePull2 · limitOfConstantLeft · contourPull3

The two together give the Perron formula. (Which doesn't need to be a separate lemma.)

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

\[ \frac1{2\pi i} \int_{(\sigma)}\frac{x^s}{s(s+1)}ds = \begin{cases} 1-\frac1x & \text{ if }x>1\\ 0 & \text{ if } x<1 \end{cases}. \]

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.