Cauchy integral formula #
In this file we prove the Cauchy-Goursat theorem and the Cauchy integral formula for integrals over
circles. Most results are formulated for a function f : ℂ → E that takes values in a complex
Banach space with second countable topology.
Main statements #
In the following theorems, if the name ends with off_countable, then the actual theorem assumes
differentiability at all but countably many points of the set mentioned below.
Rectangle integrals #
Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable: If a functionf : ℂ → Eis continuous on a closed rectangle and real differentiable on its interior, then its integral over the boundary of this rectangle is equal to the integral ofI • f' (x + y * I) 1 - f' (x + y * I) Iover the rectangle, wheref' z w : Eis the derivative offatzin the directionwandI = Complex.Iis the imaginary unit.Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable: If a functionf : ℂ → Eis continuous on a closed rectangle and is complex differentiable on its interior, then its integral over the boundary of this rectangle is equal to zero.
Unbounded rectangle integrals #
Complex.integral_boundary_unbounded_rect_eq_zero_of_differentiable_on_off_countable: If a functionf : ℂ → Eis continuous on an unbounded rectangle[[x₁, x₂]] ×ℂ Ici y, is complex differentiable on its interior, tends to zero as the imaginary part of its argument tends to infinity inside the strip[[x₁, x₂]] ×ℂ Ici y, and its integrals along the two vertical sides converge, then its integral over the boundary of this rectangle is equal to zero.Complex.tendsto_integral_boundary_unbounded_rect_one_side_atTop_nhds_sum_other_two_sides: In the same setting, the integrals along one vertical side tend to the sum of the integral along the horizontal side and the limit of the integrals along the other vertical side.
Annuli and circles #
Complex.circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable: If a functionf : ℂ → Eis continuous on a closed annulus{z | r ≤ |z - c| ≤ R}and is complex differentiable on its interior{z | r < |z - c| < R}, then the integrals of(z - c)⁻¹ • f zover the outer boundary and over the inner boundary are equal.Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto,Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable: If a functionf : ℂ → Eis continuous on a punctured closed disc{z | |z - c| ≤ R ∧ z ≠ c}, is complex differentiable on the corresponding punctured open disc, and tends toyasz → c,z ≠ c, then the integral of(z - c)⁻¹ • f zover the circle|z - c| = Ris equal to2πiy. In particular, iffis continuous on the whole closed disc and is complex differentiable on the corresponding open disc, then this integral is equal to2πif(c).Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable,Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countableCauchy integral formula: iff : ℂ → Eis continuous on a closed disc of radiusRand is complex differentiable on the corresponding open disc, then for anywin the corresponding open disc the integral of(z - w)⁻¹ • f zover the boundary of the disc is equal to2πif(w). Two versions of the lemma put the multiplier2πiat the different sides of the equality.
Analyticity #
Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable: Iff : ℂ → Eis continuous on a closed disc of positive radius and is complex differentiable on the corresponding open disc, then it is analytic on the corresponding open disc, and the coefficients of the power series are given by Cauchy integral formulas.DifferentiableOn.hasFPowerSeriesOnBall: Iff : ℂ → Eis complex differentiable on a closed disc of positive radius, then it is analytic on the corresponding open disc, and the coefficients of the power series are given by Cauchy integral formulas.DifferentiableOn.analyticAt,Differentiable.analyticAt: Iff : ℂ → Eis differentiable on a neighborhood of a point, then it is analytic at this point. In particular, iff : ℂ → Eis differentiable on the wholeℂ, then it is analytic at every pointz : ℂ.Differentiable.hasFPowerSeriesOnBall: Iff : ℂ → Eis differentiable everywhere then thecauchyPowerSeries f z Ris a formal power series representingfatzwith infinite radius of convergence (this holds for any choice of0 < R).
Higher derivatives #
Complex.circleIntegral_one_div_sub_pow_smul_of_differentiable_on_off_countable,Complex.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countableCauchy integral formula for derivatives: formula for the higher derivatives offat a point in a disc in terms of circle integrals off z / (z - w) ^ (n + 1)around the boundary circle, together with the specialization to the centre of the disc.
Implementation details #
The proof of the Cauchy integral formula in this file is based on a very general version of the
divergence theorem, see MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable
(a version for functions defined on Fin (n + 1) → ℝ),
MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivWithinAt_off_countable_of_le, and
MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countable (versions for
functions defined on ℝ × ℝ).
Usually, the divergence theorem is formulated for a $C^1$ smooth function. The theorems formulated above deal with a function that is
- continuous on a closed box/rectangle;
- differentiable at all but countably many points of its interior;
- have divergence integrable over the closed box/rectangle.
First, we reformulate the theorem for a real-differentiable map ℂ → E, and relate the integral
of f over the boundary of a rectangle in ℂ to the integral of the derivative
$\frac{\partial f}{\partial \bar z}$ over the interior of this box. In particular, for a complex
differentiable function, the latter derivative is zero, hence the integral over the boundary of a
rectangle is zero. Thus we get the Cauchy-Goursat theorem for a rectangle in ℂ.
Next, we apply this theorem to the function $F(z)=f(c+e^{z})$ on the rectangle
$[\ln r, \ln R]\times [0, 2\pi]$ to prove that
$$ \oint_{|z-c|=r}\frac{f(z)\,dz}{z-c}=\oint_{|z-c|=R}\frac{f(z)\,dz}{z-c} $$
provided that f is continuous on the closed annulus r ≤ |z - c| ≤ R and is complex
differentiable on its interior r < |z - c| < R (possibly, at all but countably many points).
Here and below, we write $\frac{f(z)}{z-c}$ in the documentation while the actual lemmas use
(z - c)⁻¹ • f z because f z belongs to some Banach space over ℂ and f z / (z - c) is
undefined.
Taking the limit of this equality as r tends to 𝓝[>] 0, we prove
$$ \oint_{|z-c|=R}\frac{f(z)\,dz}{z-c}=2\pi if(c) $$
provided that f is continuous on the closed disc |z - c| ≤ R and is differentiable at all but
countably many points of its interior. This is the Cauchy integral formula for the center of a
circle. In particular, if we apply this function to F z = (z - c) • f z, then we get
$$ \oint_{|z-c|=R} f(z)\,dz=0. $$
In order to deduce the Cauchy integral formula for any point w, |w - c| < R, we consider the
slope function g : ℂ → E given by g z = (z - w)⁻¹ • (f z - f w) if z ≠ w and g w = f' w.
This function satisfies assumptions of the previous theorem, so we have
$$ \oint_{|z-c|=R} \frac{f(z)\,dz}{z-w}=\oint_{|z-c|=R} \frac{f(w)\,dz}{z-w}= \left(\oint_{|z-c|=R} \frac{dz}{z-w}\right)f(w). $$
The latter integral was computed in circleIntegral.integral_sub_inv_of_mem_ball and is equal to
2 * π * Complex.I.
There is one more step in the actual proof. Since we allow f to be non-differentiable on a
countable set s, we cannot immediately claim that g is continuous at w if w ∈ s. So, we use
the proof outlined in the previous paragraph for w ∉ s (see
Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux), then use continuity
of both sides of the formula and density of sᶜ to prove the formula for all points of the open
ball, see Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable.
Finally, we use the properties of the Cauchy integrals established elsewhere (see
hasFPowerSeriesOn_cauchy_integral) and Cauchy integral formula to prove that the original
function is analytic on the open ball.
TODO #
- The results on unbounded rectangles only cover rectangles that are unbounded above. Add versions for rectangles that are unbounded below, to the left and to the right, together with lemmas transferring statements between the four cases, so that these follow readily from the results already formalised in this file.
Tags #
Cauchy-Goursat theorem, Cauchy integral formula
Functions on rectangles #
Suppose that a function f : ℂ → E is continuous on a closed rectangle with opposite corners at
z w : ℂ, is real differentiable at all but countably many points of the corresponding open
rectangle, and $\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then the
integral of f over the boundary of the rectangle is equal to the integral of
$2i\frac{\partial f}{\partial \bar z}=i\frac{\partial f}{\partial x}-\frac{\partial f}{\partial y}$
over the rectangle.
Suppose that a function f : ℂ → E is continuous on a closed rectangle with opposite corners at
z w : ℂ, is real differentiable on the corresponding open rectangle, and
$\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then the integral of f over
the boundary of the rectangle is equal to the integral of
$2i\frac{\partial f}{\partial \bar z}=i\frac{\partial f}{\partial x}-\frac{\partial f}{\partial y}$
over the rectangle.
Suppose that a function f : ℂ → E is real differentiable on a closed rectangle with opposite
corners at z w : ℂ and $\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then
the integral of f over the boundary of the rectangle is equal to the integral of
$2i\frac{\partial f}{\partial \bar z}=i\frac{\partial f}{\partial x}-\frac{\partial f}{\partial y}$
over the rectangle.
Cauchy-Goursat theorem for a rectangle: the integral of a complex differentiable function
over the boundary of a rectangle equals zero. More precisely, if f is continuous on a closed
rectangle and is complex differentiable at all but countably many points of the corresponding open
rectangle, then its integral over the boundary of the rectangle equals zero.
Cauchy-Goursat theorem for a rectangle: the integral of a complex differentiable function
over the boundary of a rectangle equals zero. More precisely, if f is continuous on a closed
rectangle and is complex differentiable on the corresponding open rectangle, then its integral over
the boundary of the rectangle equals zero.
Cauchy-Goursat theorem for a rectangle: the integral of a complex differentiable function
over the boundary of a rectangle equals zero. More precisely, if f is complex differentiable on a
closed rectangle, then its integral over the boundary of the rectangle equals zero.
Functions on annuli #
If f : ℂ → E is continuous on the closed annulus r ≤ ‖z - c‖ ≤ R, 0 < r ≤ R,
and is complex differentiable at all but countably many points of its interior,
then the integrals of f z / (z - c) (formally, (z - c)⁻¹ • f z)
over the circles ‖z - c‖ = r and ‖z - c‖ = R are equal to each other.
Cauchy-Goursat theorem for an annulus. If f : ℂ → E is continuous on the closed annulus
r ≤ ‖z - c‖ ≤ R, 0 < r ≤ R, and is complex differentiable at all but countably many points of
its interior, then the integrals of f over the circles ‖z - c‖ = r and ‖z - c‖ = R are equal
to each other.
Circle integrals #
Cauchy integral formula for the value at the center of a disc. If f is continuous on a
punctured closed disc of radius R, is differentiable at all but countably many points of the
interior of this disc, and has a limit y at the center of the disc, then the integral
$\oint_{‖z-c‖=R} \frac{f(z)}{z-c}\,dz$ is equal to 2πiy.
Cauchy integral formula for the value at the center of a disc. If f : ℂ → E is continuous on a
closed disc of radius R and center c, and is complex differentiable at all but countably many
points of its interior, then the integral $\oint_{|z-c|=R} \frac{f(z)}{z-c}\,dz$ is equal to
2πi • f c.
Cauchy-Goursat theorem for a disk: if f : ℂ → E is continuous on a closed disk
{z | ‖z - c‖ ≤ R} and is complex differentiable at all but countably many points of its interior,
then the integral $\oint_{|z-c|=R}f(z)\,dz$ equals zero.
Cauchy-Goursat theorem for a disk: if f : ℂ → E is continuous on a closed disk
{z | ‖z - c‖ ≤ R} and is complex differentiable on the open disk,
then the integral $\oint_{|z-c|=R}f(z)\,dz$ equals zero.
An auxiliary lemma for
Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable. This lemma assumes
w ∉ s while the main lemma drops this assumption.
Cauchy integral formula: if f : ℂ → E is continuous on a closed disc of radius R and is
complex differentiable at all but countably many points of its interior, then for any w in this
interior we have $\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$.
Cauchy integral formula: if f : ℂ → E is continuous on a closed disc of radius R and is
complex differentiable at all but countably many points of its interior, then for any w in this
interior we have $\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$.
Cauchy integral formula: if f : ℂ → E is complex differentiable on an open disc and is
continuous on its closure, then for any w in this open ball we have
$\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$.
Cauchy integral formula: if f : ℂ → E is complex differentiable on an open disc and is
continuous on its closure, then for any w in this open ball we have
$\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$.
Cauchy integral formula: if f : ℂ → E is complex differentiable on a closed disc of radius
R, then for any w in its interior we have $\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$.
Cauchy integral formula: if f : ℂ → ℂ is continuous on a closed disc of radius R and is
complex differentiable at all but countably many points of its interior, then for any w in this
interior we have $\oint_{|z-c|=R}\frac{f(z)}{z-w}dz=2\pi i\,f(w)$.
Derivative of Cauchy-type integrals: if f is circle integrable and w does not lie on the
circle, then for every n : ℤ the Cauchy-type integral
fun w ↦ ∮ z in C(c, R), (z - w) ^ n • f z has derivative
-n • ∮ z in C(c, R), (z - w) ^ (n - 1) • f z at w.
Derivative of the Cauchy integral: if f is circle integrable and w does not lie on the
circle, then the Cauchy-type integral fun w ↦ ∮ z in C(c, R), (z - w)⁻¹ • f z has derivative
∮ z in C(c, R), (z - w) ^ (-2) • f z at w.
Applications to analyticity #
If f : ℂ → E is continuous on a closed ball of positive radius and is differentiable at all
but countably many points of the corresponding open ball, then it is analytic on the open ball with
coefficients of the power series given by Cauchy integral formulas.
If f : ℂ → E is complex differentiable on an open disc of positive radius and is continuous
on its closure, then it is analytic on the open disc with coefficients of the power series given by
Cauchy integral formulas.
If f : ℂ → E is complex differentiable on a closed disc of positive radius, then it is
analytic on the corresponding open disc, and the coefficients of the power series are given by
Cauchy integral formulas. See also
Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable for a version of this lemma with
weaker assumptions.
If f : ℂ → E is complex differentiable on some set s, then it is analytic at any point z
such that s ∈ 𝓝 z (equivalently, z ∈ interior s).
If f : ℂ → E is complex differentiable on some open set s, then it is continuously
differentiable on s.
A complex differentiable function f : ℂ → E is analytic at every point.
A complex differentiable function f : ℂ → E is continuously differentiable at every point.
When f : ℂ → E is differentiable, the cauchyPowerSeries f z R represents f as a power
series centered at z in the entirety of ℂ, regardless of R : ℝ≥0, with 0 < R.
On an open set, f : ℂ → E is analytic iff it is differentiable
On an open set, f : ℂ → E is analytic iff it is differentiable
f : ℂ → E is entire iff it's differentiable
f : ℂ → E is analytic at z iff it's differentiable near z
Integrals over unbounded rectangular contours #
If a family of functions g m tends to zero uniformly along the product filter
atTop ×ˢ (comap im atTop ⊓ 𝓟 ([[x₁, x₂]] ×ℂ Ici y)) (i.e., as m → ∞ and the imaginary part of
the input → ∞ jointly, within [[x₁, x₂]] ×ℂ Ici y), then
$\lim_{m \to \infty} \int_{x_1}^{x_2} g(m, x + m I) \, dx = 0$. This generalises
tendsto_integral_atTop_nhds_zero_of_tendsto_im_atTop_nhds_zero.
If $f(z) \to 0$ as $\Im(z) \to \infty$ within [[x₁, x₂]] ×ℂ univ, then
$\lim_{m \to \infty} \int_{x_1}^{x_2} f(x + mI) dx = 0$.
Deformation of unbounded 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. ("Unbounded rectangular contours" refers to contours that look like the disjoint union symbol "⨆")
Deformation of unbounded 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 unbounded 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_unbounded_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 unbounded 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_unbounded_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.
Circle integrals for higher derivatives #
Cauchy integral formula for derivatives at any point w in an open ball, assuming f is
continuous on the corresponding closed ball and differentiable on its interior away from a
countable set.
Cauchy integral formula for derivatives, assuming f is continuous on a closed ball and
differentiable on its interior away from a countable set.
Cauchy integral formula for the first order derivative, assuming f is continuous on a
closed ball and differentiable on its interior away from a countable set.
Cauchy integral formula for derivatives at any point w in an open ball, assuming f is
continuous on the closure of the ball and differentiable on the open ball.
Cauchy integral formula for derivatives, assuming f is continuous on a closed ball and
differentiable on its interior.
Cauchy integral formula for the first order derivative, assuming f is continuous on a
closed ball and differentiable on its interior.
Cauchy integral formula for derivatives at any point w in an open ball, assuming f is
differentiable on the corresponding closed ball.
Cauchy integral formula for derivatives, assuming f is differentiable on a closed ball.
Cauchy integral formula for the first order derivative, assuming f is differentiable on
a closed ball.