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.
-
complex.integral_boundary_rect_of_has_fderiv_within_at_real_off_countable
: If a functionf : ℂ → E
is 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) I
over the rectangle, wheref' z w : E
is the derivative off
atz
in the directionw
andI = complex.I
is the imaginary unit. -
complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable
: If a functionf : ℂ → E
is 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. -
complex.circle_integral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable
: If a functionf : ℂ → E
is 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 z
over the outer boundary and over the inner boundary are equal. -
complex.circle_integral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto
,complex.circle_integral_sub_center_inv_smul_of_differentiable_on_off_countable
: If a functionf : ℂ → E
is continuous on a punctured closed disc{z | |z - c| ≤ R ∧ z ≠ c}
, is complex differentiable on the corresponding punctured open disc, and tends toy
asz → c
,z ≠ c
, then the integral of(z - c)⁻¹ • f z
over the circle|z - c| = R
is equal to2πiy
. In particular, iff
is continuous on the whole closed disc and is complex differentiable on the corresponding open disc, then this integral is equal to2πif(c)
. -
complex.circle_integral_sub_inv_smul_of_differentiable_on_off_countable
,complex.two_pi_I_inv_smul_circle_integral_sub_inv_smul_of_differentiable_on_off_countable
Cauchy integral formula: iff : ℂ → E
is continuous on a closed disc of radiusR
and is complex differentiable on the corresponding open disc, then for anyw
in the corresponding open disc the integral of(z - w)⁻¹ • f z
over the boundary of the disc is equal to2πif(w)
. Two versions of the lemma put the multiplier2πi
at the different sides of the equality. -
complex.has_fpower_series_on_ball_of_differentiable_off_countable
: Iff : ℂ → E
is 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. -
differentiable_on.has_fpower_series_on_ball
: Iff : ℂ → 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. -
differentiable_on.analytic_at
,differentiable.analytic_at
: Iff : ℂ → E
is differentiable on a neighborhood of a point, then it is analytic at this point. In particular, iff : ℂ → E
is differentiable on the wholeℂ
, then it is analytic at every pointz : ℂ
. -
differentiable.has_power_series_on_ball
: Iff : ℂ → E
is differentiable everywhere then thecauchy_power_series f z R
is a formal power series representingf
atz
with infinite radius of convergence (this holds for any choice of0 < R
).
Implementation details #
The proof of the Cauchy integral formula in this file is based on a very general version of the
divergence theorem, see measure_theory.integral_divergence_of_has_fderiv_within_at_off_countable
(a version for functions defined on fin (n + 1) → ℝ
),
measure_theory.integral_divergence_prod_Icc_of_has_fderiv_within_at_off_countable_of_le
, and
measure_theory.integral2_divergence_prod_of_has_fderiv_within_at_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 the 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 circle_integral.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.circle_integral_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.circle_integral_sub_inv_smul_of_differentiable_on_off_countable
.
Finally, we use the properties of the Cauchy integrals established elsewhere (see
has_fpower_series_on_cauchy_integral
) and Cauchy integral formula to prove that the original
function is analytic on the open ball.
Tags #
Cauchy-Goursat theorem, Cauchy integral formula
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.
If f : ℂ → E
is continuous 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.
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 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πiy`.
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.
An auxiliary lemma for
complex.circle_integral_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 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)$.
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.has_fpower_series_on_ball_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
).
A complex differentiable function f : ℂ → E
is analytic at every point.
When f : ℂ → E
is differentiable, the cauchy_power_series f z R
represents f
as a power
series centered at z
in the entirety of ℂ
, regardless of R : ℝ≥0
, with 0 < R
.