Residue calculus on rectangles

This files gathers definitions and basic properties about rectangles.

The border of a rectangle is the union of its four sides.

DefinitionRectangleBorder#

A Rectangle's border, given corners \(z\) and \(w\) is the union of the four sides.

Lean

Formalized as RectangleBorder.

Sources
LeanRectangleBorder
Used by 4
Used byresiduePull1 · residuePull2 · RectanglePullToNhdOfPole · ResidueTheoremOnRectangleWithSimplePole

DefinitionRectangleIntegral#

A RectangleIntegral of a function \(f\) is one over a rectangle determined by \(z\) and \(w\) in \(\mathbb{C}\). We will sometimes denote it by \(\int_{z}^{w} f\). (There is also a primed version, which is \(1/(2\pi i)\) times the original.)

Lean

Formalized as RectangleIntegral.

Sources
LeanRectangleIntegral
Used by 16
Used byformulaLtOne · RectangleIntegral-tendsTo-LowerU · RectangleIntegral-tendsTo-UpperU · RectangleIntegral-tendsTo-VerticalIntegral · residueAtZero · contourPull3 · residueAtNegOne · residuePull1 · residuePull2 · SmoothedChebyshevPull1 · SmoothedChebyshevPull2 · DiffVertRect-eq-UpperLowerUs · HolomorphicOn.vanishesOnRectangle · RectanglePullToNhdOfPole · ResidueTheoremAtOrigin · ResidueTheoremOnRectangleWithSimplePole

DefinitionUpperUIntegral#

An UpperUIntegral of a function \(f\) comes from \(\sigma+i\infty\) down to \(\sigma+iT\), over to \(\sigma'+iT\), and back up to \(\sigma'+i\infty\).

Lean

Formalized as UpperUIntegral.

Sources
LeanUpperUIntegral
Used by 2
Used byRectangleIntegral-tendsTo-UpperU · DiffVertRect-eq-UpperLowerUs

DefinitionLowerUIntegral#

A LowerUIntegral of a function \(f\) comes from \(\sigma-i\infty\) up to \(\sigma-iT\), over to \(\sigma'-iT\), and back down to \(\sigma'-i\infty\).

Lean

Formalized as LowerUIntegral.

Sources
LeanLowerUIntegral
Used by 2
Used byRectangleIntegral-tendsTo-LowerU · DiffVertRect-eq-UpperLowerUs

It is very convenient to define integrals along vertical lines in the complex plane, as follows.

DefinitionVerticalIntegral#

Let \(f\) be a function from \(\mathbb{C}\) to \(\mathbb{C}\), and let \(\sigma\) be a real number. Then we define

\[ \int_{(\sigma)}f(s)ds = \int_{\sigma-i\infty}^{\sigma+i\infty}f(s)ds. \]
Lean

Formalized as VerticalIntegral.

Sources
LeanVerticalIntegral
Used by 11
Used byformulaLtOne · RectangleIntegral-tendsTo-VerticalIntegral · vertIntBound · vertIntBoundLeft · contourPull3 · formulaGtOne · residuePull1 · residuePull2 · SmoothedChebyshev · SmoothedChebyshevPull1 · DiffVertRect-eq-UpperLowerUs

We also have a version with a factor of \(1/(2\pi i)\).

LemmaDiffVertRect-eq-UpperLowerUs#

The difference of two vertical integrals and a rectangle is the difference of an upper and a lower U integrals.

Proof

Follows directly from the definitions.

Lean

Formalized as DiffVertRect_eq_UpperLowerUs.

Sources
LeanDiffVertRect_eq_UpperLowerUs
Uses 4
Statement usesLowerUIntegral · UpperUIntegral · RectangleIntegral · VerticalIntegral

TheoremexistsDifferentiableOn-of-bddAbove#

If \(f\) is differentiable on a set \(s\) except at \(c\in s\), and \(f\) is bounded above on \(s\setminus\{c\}\), then there exists a differentiable function \(g\) on \(s\) such that \(f\) and \(g\) agree on \(s\setminus\{c\}\).

Proof

This is the Riemann Removable Singularity Theorem, slightly rephrased from what's in Mathlib. (We don't care what the function \(g\) is, just that it's holomorphic.)

Lean

Formalized as existsDifferentiableOn_of_bddAbove.

Sources
LeanexistsDifferentiableOn_of_bddAbove
Used by 5
Used byresidueAtZero · residueAtNegOne · SmoothedChebyshevPull1 · logDerivResidue · ResidueOfTendsTo

TheoremHolomorphicOn.vanishesOnRectangle#

If \(f\) is holomorphic on a rectangle \(z\) and \(w\), then the integral of \(f\) over the rectangle with corners \(z\) and \(w\) is \(0\).

Proof

This is in a Mathlib PR.

Lean

Formalized as HolomorphicOn.vanishesOnRectangle.

Sources
LeanHolomorphicOn.vanishesOnRectangle
Uses 1 · Used by 5
Statement usesRectangleIntegral
Used byresiduePull1 · residuePull2 · SmoothedChebyshevPull2 · RectanglePullToNhdOfPole · ResidueTheoremOnRectangleWithSimplePole

The next lemma allows to zoom a big rectangle down to a small square, centered at a pole.

LemmaRectanglePullToNhdOfPole#

If \(f\) is holomorphic on a rectangle \(z\) and \(w\) except at a point \(p\), then the integral of \(f\) over the rectangle with corners \(z\) and \(w\) is the same as the integral of \(f\) over a small square centered at \(p\).

Proof

Chop the big rectangle with two vertical cuts and two horizontal cuts into smaller rectangles, the middle one being the desired square. The integral over each of the outer rectangles vanishes, since \(f\) is holomorphic there. (The constant \(c\) being “small enough” here just means that the inner square is strictly contained in the big rectangle.)

Lean

Formalized as RectanglePullToNhdOfPole.

Sources
LeanRectanglePullToNhdOfPole
Uses 3
Statement usesRectangleIntegral
Proof usesHolomorphicOn.vanishesOnRectangle · RectangleBorder

LemmaResidueTheoremAtOrigin#

The rectangle (square) integral of \(f(s) = 1/s\) with corners \(-1-i\) and \(1+i\) is equal to \(2\pi i\).

Proof

This is a special case of the more general result above.

Lean

Formalized as ResidueTheoremAtOrigin.

Sources
LeanResidueTheoremAtOrigin
Uses 1
Statement usesRectangleIntegral

LemmaResidueTheoremOnRectangleWithSimplePole#

Suppose that \(f\) is a holomorphic function on a rectangle, except for a simple pole at \(p\). By the latter, we mean that there is a function \(g\) holomorphic on the rectangle such that, \(f = g + A/(s-p)\) for some \(A\in\mathbb{C}\). Then the integral of \(f\) over the rectangle is \(A\).

Proof

Replace \(f\) with \(g + A/(s-p)\) in the integral. The integral of \(g\) vanishes by Lemma HolomorphicOn.vanishesOnRectangle. To evaluate the integral of \(1/(s-p)\), pull everything to a square about the origin using Lemma RectanglePullToNhdOfPole, and rescale by \(c\); what remains is handled by Lemma ResidueTheoremAtOrigin.

Lean

Formalized as ResidueTheoremOnRectangleWithSimplePole.

Sources
LeanResidueTheoremOnRectangleWithSimplePole
Uses 3 · Used by 3
Statement usesRectangleIntegral
Proof usesHolomorphicOn.vanishesOnRectangle · RectangleBorder
Used byresidueAtZero · residueAtNegOne · SmoothedChebyshevPull1

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.