[proofplan] We apply the residue theorem to the [meromorphic function](/page/Meromorphic%20Function) \begin{align*} G(s)=F(s)\frac{x^s}{s} \end{align*} on the positively oriented boundary of the rectangle $R_{\alpha,c,T}$. The hypotheses ensure that $G$ is meromorphic on a neighbourhood of the rectangle and has no poles on the boundary. The boundary integral splits into four directed line integrals, and rearranging this identity isolates the right vertical integral while packaging the two horizontal sides into the stated term $E_{\mathrm{hor}}(x,T)$. [/proofplan]

[step:Define the meromorphic integrand on a neighbourhood of the rectangle]Define the function \begin{align*} G: U \setminus P &\to \mathbb{C} \\ s &\mapsto F(s)\frac{x^s}{s}, \end{align*} where $U \subset \mathbb{C}$ is an open neighbourhood of $R_{\alpha,c,T}$ on which $F$ is meromorphic, and $P \subset U$ is the discrete set of poles of $G$. Since $R_{\alpha,c,T}$ is compact and $G$ is meromorphic on $U$, the set $P \cap R_{\alpha,c,T}^{\circ}$ is finite. By hypothesis, $P \cap \partial R_{\alpha,c,T} = \varnothing$, so all boundary line integrals below are well-defined.[/step]

[guided]We first isolate the function to which the residue theorem will be applied. Let $U \subset \mathbb{C}$ be an open neighbourhood of the closed rectangle $R_{\alpha,c,T}$ on which the meromorphic continuation of $F$ is defined. Define \begin{align*} G: U \setminus P &\to \mathbb{C} \\ s &\mapsto F(s)\frac{x^s}{s}, \end{align*} where $P$ denotes the set of poles of $G$. The expression $x^s$ is unambiguous because $x>0$, so we use the real logarithm and write $x^s=\exp(s\log x)$. The set of poles of a meromorphic function is discrete in its domain. Since the closed rectangle $R_{\alpha,c,T}$ is compact and contained in $U$, only finitely many poles of $G$ can lie in $R_{\alpha,c,T}^{\circ}$. The theorem assumes that no pole lies on $\partial R_{\alpha,c,T}$, which is exactly the condition needed for the contour integral over the boundary to be defined.[/guided]

[step:Apply the residue theorem to the positively oriented rectangle]Let $\Gamma$ denote the positively oriented boundary of $R_{\alpha,c,T}$: \begin{align*} \Gamma = [\alpha-iT,c-iT] \cup [c-iT,c+iT] \cup [c+iT,\alpha+iT] \cup [\alpha+iT,\alpha-iT]. \end{align*} By the Residue Theorem, applied to $G$ on the open neighbourhood $U$ of the rectangle with pole set $P \cap R_{\alpha,c,T}^{\circ}$, \begin{align*} \int_{\Gamma} G(s)\,ds = 2\pi i \sum_{\rho \in P \cap R_{\alpha,c,T}^{\circ}} \operatorname{Res}_{s=\rho} G(s). \end{align*} Expanding the boundary integral according to the four directed sides gives \begin{align*} & \int_{\alpha-iT}^{c-iT} G(s)\,ds + \int_{c-iT}^{c+iT} G(s)\,ds + \int_{c+iT}^{\alpha+iT} G(s)\,ds + \int_{\alpha+iT}^{\alpha-iT} G(s)\,ds \\ &\qquad = 2\pi i \sum_{\rho \in P \cap R_{\alpha,c,T}^{\circ}} \operatorname{Res}_{s=\rho} G(s). \end{align*}[/step]

[guided]Let $\Gamma$ be the counterclockwise boundary of the rectangle. Written as directed line segments, this contour is \begin{align*} \Gamma = [\alpha-iT,c-iT] \cup [c-iT,c+iT] \cup [c+iT,\alpha+iT] \cup [\alpha+iT,\alpha-iT]. \end{align*} The residue theorem applies because $G$ is meromorphic on an [open set](/page/Open%20Set) containing the rectangle, has no poles on the boundary, and has finite interior pole set $P \cap R_{\alpha,c,T}^{\circ}$. Therefore \begin{align*} \int_{\Gamma} G(s)\,ds = 2\pi i \sum_{\rho \in P \cap R_{\alpha,c,T}^{\circ}} \operatorname{Res}_{s=\rho} G(s). \end{align*} The orientation matters. Traversing the rectangle counterclockwise means that the bottom edge runs from $\alpha-iT$ to $c-iT$, the right edge runs from $c-iT$ to $c+iT$, the top edge runs from $c+iT$ to $\alpha+iT$, and the left edge runs from $\alpha+iT$ to $\alpha-iT$. Hence \begin{align*} & \int_{\alpha-iT}^{c-iT} G(s)\,ds + \int_{c-iT}^{c+iT} G(s)\,ds + \int_{c+iT}^{\alpha+iT} G(s)\,ds + \int_{\alpha+iT}^{\alpha-iT} G(s)\,ds \\ &\qquad = 2\pi i \sum_{\rho \in P \cap R_{\alpha,c,T}^{\circ}} \operatorname{Res}_{s=\rho} G(s). \end{align*}[/guided]

[step:Isolate the right vertical integral and reverse the remaining orientations]Solving the preceding identity for the right vertical integral yields \begin{align*} \int_{c-iT}^{c+iT} G(s)\,ds &= 2\pi i \sum_{\rho \in R_{\alpha,c,T}^{\circ}} \operatorname{Res}_{s=\rho} G(s) - \int_{\alpha-iT}^{c-iT} G(s)\,ds - \int_{c+iT}^{\alpha+iT} G(s)\,ds - \int_{\alpha+iT}^{\alpha-iT} G(s)\,ds. \end{align*} Reversing the orientation of the left vertical side and both horizontal sides gives \begin{align*} \int_{c-iT}^{c+iT} G(s)\,ds &= 2\pi i \sum_{\rho \in R_{\alpha,c,T}^{\circ}} \operatorname{Res}_{s=\rho} G(s) + \int_{\alpha-iT}^{\alpha+iT} G(s)\,ds \\ &\qquad + \int_{\alpha+iT}^{c+iT} G(s)\,ds + \int_{c-iT}^{\alpha-iT} G(s)\,ds. \end{align*} Dividing by $2\pi i$ and substituting $G(s)=F(s)x^s/s$ gives exactly the asserted identity, with the two horizontal integrals equal to $E_{\mathrm{hor}}(x,T)$. This proves the formula.[/step]

[guided]Starting from the four-side identity, we isolate the right vertical side because this is the integral appearing on the left-hand side of the theorem: \begin{align*} \int_{c-iT}^{c+iT} G(s)\,ds &= 2\pi i \sum_{\rho \in R_{\alpha,c,T}^{\circ}} \operatorname{Res}_{s=\rho} G(s) - \int_{\alpha-iT}^{c-iT} G(s)\,ds - \int_{c+iT}^{\alpha+iT} G(s)\,ds - \int_{\alpha+iT}^{\alpha-iT} G(s)\,ds. \end{align*} Each minus sign is converted into a reversal of orientation. For a directed line segment, reversing the endpoints changes the sign of the line integral. Hence \begin{align*} -\int_{\alpha-iT}^{c-iT} G(s)\,ds &= \int_{c-iT}^{\alpha-iT} G(s)\,ds, \\ -\int_{c+iT}^{\alpha+iT} G(s)\,ds &= \int_{\alpha+iT}^{c+iT} G(s)\,ds, \\ -\int_{\alpha+iT}^{\alpha-iT} G(s)\,ds &= \int_{\alpha-iT}^{\alpha+iT} G(s)\,ds. \end{align*} Substituting these three orientation reversals gives \begin{align*} \int_{c-iT}^{c+iT} G(s)\,ds &= 2\pi i \sum_{\rho \in R_{\alpha,c,T}^{\circ}} \operatorname{Res}_{s=\rho} G(s) + \int_{\alpha-iT}^{\alpha+iT} G(s)\,ds \\ &\qquad + \int_{\alpha+iT}^{c+iT} G(s)\,ds + \int_{c-iT}^{\alpha-iT} G(s)\,ds. \end{align*} Finally divide by $2\pi i$ and use the definition $G(s)=F(s)x^s/s$. The first reversed integral is the left vertical integral, and the two remaining reversed integrals are exactly the horizontal contribution $E_{\mathrm{hor}}(x,T)$ as defined in the theorem statement. This is the claimed identity.[/guided]