Cauchy integral formula #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 : ℂ → 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. -
complex.circle_integral_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.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 : ℂ → 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.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_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. -
complex.has_fpower_series_on_ball_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. -
differentiable_on.has_fpower_series_on_ball: 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. -
differentiable_on.analytic_at,differentiable.analytic_at: 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.has_power_series_on_ball: Iff : ℂ → Eis differentiable everywhere then thecauchy_power_series f z Ris a formal power series representingfatzwith 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 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)$.
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.