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_hasFDerivAt_real_off_countable: If a function f : ℂ → 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 of I • f' (x + y * I) 1 - f' (x + y * I) I over the rectangle, where f' z w : E is the derivative of f at z in the direction w and I = Complex.I is the imaginary unit.
Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable: If a function f : ℂ → 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.circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable: If a function f : ℂ → 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.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 function f : ℂ → 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 to y as z → c, z ≠ c, then the integral of (z - c)⁻¹ • f z over the circle |z - c| = R is equal to 2πiy. In particular, if f is continuous on the whole closed disc and is complex differentiable on the corresponding open disc, then this integral is equal to 2π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_countable Cauchy integral formula: if f : ℂ → E is continuous on a closed disc of radius R and is complex differentiable on the corresponding open disc, then for any w in the corresponding open disc the integral of (z - w)⁻¹ • f z over the boundary of the disc is equal to 2πif(w). Two versions of the lemma put the multiplier 2πi at the different sides of the equality.
Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable: If f : ℂ → 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.
DifferentiableOn.hasFPowerSeriesOnBall: 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.
DifferentiableOn.analyticAt, Differentiable.analyticAt: If f : ℂ → E is differentiable on a neighborhood of a point, then it is analytic at this point. In particular, if f : ℂ → E is differentiable on the whole ℂ, then it is analytic at every point z : ℂ.
Differentiable.hasFPowerSeriesOnBall: If f : ℂ → E is differentiable everywhere then the cauchyPowerSeries f z R is a formal power series representing f at z with infinite radius of convergence (this holds for any choice of 0 < 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 MeasureTheory.integral_divergence_of_hasFDerivWithinAt_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.

Tags #

Cauchy-Goursat theorem, Cauchy integral formula