Deforming Paths of Integration for Open Contours #
In this file, we prove that if a function tends to zero as the imaginary part of its input tends to infinity and satisfies Cauchy-Goursat-type conditions, then we can deform paths of integration along rectangular contours that extend infinitely in the vertical direction.
NOTE: Use atImInfty for vanishing as imaginary part tends to i infinity!
If $f(z) \to 0$ as $\Im(z) \to \infty$, then $\lim_{m \to \infty} \int_{x_1}^{x_2} f(x + mI) dx = 0$.
A direct consequence of the Cauchy-Goursat Theorem for rectangles: given the conditions of
the Cauchy-Goursat Theorem between two vertical lines in the Complex plane, fixing some y, the
integral around rectangles bounded by these vertical lines, the horizontal line with imaginary
part y, and a horizontal line with imaginary part m is eventually equal to 0.
By Cauchy-Goursat, it is immediate that this is true when m ≥ y. Indeed, the contents of this
lemma are not particularly nontrivial. The point is to state this fact using eventually result so
it will be compatible with tendsto_congr', which is useful for applications.
Deformation of open rectangular contours: Given two infinite vertical contours such that a function satisfies Cauchy-Goursat conditions between them, interval integrals of increasing interval length along the first contour tend to the sum of a translation integral and the limit of interval integrals along the second integral.
We call this a deformation of open rectangular contours because it allows us to change contours when working with contours that look like "infinite boxes without lids"---that is, rectangular contours that are "open" at the top (we do not mean open in a topological sense).
Deformation of open rectangular contours: Given two infinite vertical contours such that a function satisfies Cauchy-Goursat conditions between them, the limit of interval integrals along the first contour equals the sum of a translation integral and the limit of interval integrals along the second integral.
Deformation of open rectangular contours: Given two infinite vertical contours such that a function satisfies Cauchy-Goursat conditions between them, the limit of interval integrals along the first contour equals the sum of a translation integral and the limit of interval integrals along the second integral.
This is a variant of integral_boundary_open_rect_eq_zero_of_differentiable_on_off_countable. The
sole difference is that the assumptions in this lemma do not include the factor of I that comes
from contour parametrisation. The reason we state this version is that it might be more convenient
to use in certain cases.
Deformation of open rectangular contours: Given two infinite vertical contours such that a function satisfies Cauchy-Goursat conditions between them and is integrable along both vertical contours, the improper integral along the first contour equals the sum of a translation integral and the improper integrals along the second integral.
This is a variant of integral_boundary_open_rect_eq_zero_of_differentiable_on_off_countable' that
requires the much stronger assumption of integrability. The reason integrability is stronger is that
it requires the integral of the norm of the function to be finite rather than just that of the
function. We nevertheless include this version of the theorem because it is likely that in
applications involving specific functions, there will already be proofs of integrability.