Documentation

Mathlib.Analysis.Complex.CauchyIntegral

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.

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

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

theorem Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : E) (f' : →L[] E) (z : ) (w : ) (s : Set ) (hs : s.Countable) (Hc : ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)) (Hd : xSet.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x) (Hi : MeasureTheory.IntegrableOn (fun (z : ) => Complex.I (f' z) 1 - (f' z) Complex.I) (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) MeasureTheory.volume) :
(((∫ (x : ) in z.re..w.re, f (x + z.im * Complex.I)) - ∫ (x : ) in z.re..w.re, f (x + w.im * Complex.I)) + Complex.I ∫ (y : ) in z.im..w.im, f (w.re + y * Complex.I)) - Complex.I ∫ (y : ) in z.im..w.im, f (z.re + y * Complex.I) = ∫ (x : ) in z.re..w.re, ∫ (y : ) in z.im..w.im, Complex.I (f' (x + y * Complex.I)) 1 - (f' (x + y * Complex.I)) Complex.I

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.

theorem Complex.integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : E) (f' : →L[] E) (z : ) (w : ) (Hc : ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)) (Hd : xSet.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im), HasFDerivAt f (f' x) x) (Hi : MeasureTheory.IntegrableOn (fun (z : ) => Complex.I (f' z) 1 - (f' z) Complex.I) (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) MeasureTheory.volume) :
(((∫ (x : ) in z.re..w.re, f (x + z.im * Complex.I)) - ∫ (x : ) in z.re..w.re, f (x + w.im * Complex.I)) + Complex.I ∫ (y : ) in z.im..w.im, f (w.re + y * Complex.I)) - Complex.I ∫ (y : ) in z.im..w.im, f (z.re + y * Complex.I) = ∫ (x : ) in z.re..w.re, ∫ (y : ) in z.im..w.im, Complex.I (f' (x + y * Complex.I)) 1 - (f' (x + y * Complex.I)) Complex.I

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.

theorem Complex.integral_boundary_rect_of_differentiableOn_real {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : E) (z : ) (w : ) (Hd : DifferentiableOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)) (Hi : MeasureTheory.IntegrableOn (fun (z : ) => Complex.I (fderiv f z) 1 - (fderiv f z) Complex.I) (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) MeasureTheory.volume) :
(((∫ (x : ) in z.re..w.re, f (x + z.im * Complex.I)) - ∫ (x : ) in z.re..w.re, f (x + w.im * Complex.I)) + Complex.I ∫ (y : ) in z.im..w.im, f (w.re + y * Complex.I)) - Complex.I ∫ (y : ) in z.im..w.im, f (z.re + y * Complex.I) = ∫ (x : ) in z.re..w.re, ∫ (y : ) in z.im..w.im, Complex.I (fderiv f (x + y * Complex.I)) 1 - (fderiv f (x + y * Complex.I)) Complex.I

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.

theorem Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : E) (z : ) (w : ) (s : Set ) (hs : s.Countable) (Hc : ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)) (Hd : xSet.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im) \ s, DifferentiableAt f x) :
(((∫ (x : ) in z.re..w.re, f (x + z.im * Complex.I)) - ∫ (x : ) in z.re..w.re, f (x + w.im * Complex.I)) + Complex.I ∫ (y : ) in z.im..w.im, f (w.re + y * Complex.I)) - Complex.I ∫ (y : ) in z.im..w.im, f (z.re + y * Complex.I) = 0

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.

theorem Complex.integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : E) (z : ) (w : ) (Hc : ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)) (Hd : DifferentiableOn f (Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im))) :
(((∫ (x : ) in z.re..w.re, f (x + z.im * Complex.I)) - ∫ (x : ) in z.re..w.re, f (x + w.im * Complex.I)) + Complex.I ∫ (y : ) in z.im..w.im, f (w.re + y * Complex.I)) - Complex.I ∫ (y : ) in z.im..w.im, f (z.re + y * Complex.I) = 0

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.

theorem Complex.integral_boundary_rect_eq_zero_of_differentiableOn {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : E) (z : ) (w : ) (H : DifferentiableOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)) :
(((∫ (x : ) in z.re..w.re, f (x + z.im * Complex.I)) - ∫ (x : ) in z.re..w.re, f (x + w.im * Complex.I)) + Complex.I ∫ (y : ) in z.im..w.im, f (w.re + y * Complex.I)) - Complex.I ∫ (y : ) in z.im..w.im, f (z.re + y * Complex.I) = 0

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.

theorem Complex.circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {c : } {r : } {R : } (h0 : 0 < r) (hle : r R) {f : E} {s : Set } (hs : s.Countable) (hc : ContinuousOn f (Metric.closedBall c R \ Metric.ball c r)) (hd : z(Metric.ball c R \ Metric.closedBall c r) \ s, DifferentiableAt f z) :
(∮ (z : ) in C(c, R), (z - c)⁻¹ f z) = ∮ (z : ) in C(c, r), (z - c)⁻¹ f z

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.

theorem Complex.circleIntegral_eq_of_differentiable_on_annulus_off_countable {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {c : } {r : } {R : } (h0 : 0 < r) (hle : r R) {f : E} {s : Set } (hs : s.Countable) (hc : ContinuousOn f (Metric.closedBall c R \ Metric.ball c r)) (hd : z(Metric.ball c R \ Metric.closedBall c r) \ s, DifferentiableAt f z) :
(∮ (z : ) in C(c, R), f z) = ∮ (z : ) in C(c, r), f z

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.

theorem Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {c : } {R : } (h0 : 0 < R) {f : E} {y : E} {s : Set } (hs : s.Countable) (hc : ContinuousOn f (Metric.closedBall c R \ {c})) (hd : z(Metric.ball c R \ {c}) \ s, DifferentiableAt f z) (hy : Filter.Tendsto f (nhdsWithin c {c}) (nhds y)) :
(∮ (z : ) in C(c, R), (z - c)⁻¹ f z) = (2 * Real.pi * Complex.I) y

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.

theorem Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {R : } (h0 : 0 < R) {f : E} {c : } {s : Set } (hs : s.Countable) (hc : ContinuousOn f (Metric.closedBall c R)) (hd : zMetric.ball c R \ s, DifferentiableAt f z) :
(∮ (z : ) in C(c, R), (z - c)⁻¹ f z) = (2 * Real.pi * Complex.I) f c

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.

theorem Complex.circleIntegral_eq_zero_of_differentiable_on_off_countable {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {R : } (h0 : 0 R) {f : E} {c : } {s : Set } (hs : s.Countable) (hc : ContinuousOn f (Metric.closedBall c R)) (hd : zMetric.ball c R \ s, DifferentiableAt f z) :
(∮ (z : ) in C(c, R), f z) = 0

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.

theorem Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {R : } {c : } {w : } {f : E} {s : Set } (hs : s.Countable) (hw : w Metric.ball c R \ s) (hc : ContinuousOn f (Metric.closedBall c R)) (hd : xMetric.ball c R \ s, DifferentiableAt f x) :
(∮ (z : ) in C(c, R), (z - w)⁻¹ f z) = (2 * Real.pi * Complex.I) f w

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.

theorem Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {R : } {c : } {w : } {f : E} {s : Set } (hs : s.Countable) (hw : w Metric.ball c R) (hc : ContinuousOn f (Metric.closedBall c R)) (hd : xMetric.ball c R \ s, DifferentiableAt f x) :
((2 * Real.pi * Complex.I)⁻¹ ∮ (z : ) in C(c, R), (z - w)⁻¹ f z) = 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 $\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)$.

theorem Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {R : } {c : } {w : } {f : E} {s : Set } (hs : s.Countable) (hw : w Metric.ball c R) (hc : ContinuousOn f (Metric.closedBall c R)) (hd : xMetric.ball c R \ s, DifferentiableAt f x) :
(∮ (z : ) in C(c, R), (z - w)⁻¹ f z) = (2 * Real.pi * Complex.I) 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)$.

theorem DiffContOnCl.circleIntegral_sub_inv_smul {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {R : } {c : } {w : } {f : E} (h : DiffContOnCl f (Metric.ball c R)) (hw : w Metric.ball c R) :
(∮ (z : ) in C(c, R), (z - w)⁻¹ f z) = (2 * Real.pi * Complex.I) f 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)$.

theorem DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {R : } {c : } {w : } {f : E} (hf : DiffContOnCl f (Metric.ball c R)) (hw : w Metric.ball c R) :
((2 * Real.pi * Complex.I)⁻¹ ∮ (z : ) in C(c, R), (z - w)⁻¹ f z) = f 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)$.

theorem DifferentiableOn.circleIntegral_sub_inv_smul {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {R : } {c : } {w : } {f : E} (hd : DifferentiableOn f (Metric.closedBall c R)) (hw : w Metric.ball c R) :
(∮ (z : ) in C(c, R), (z - w)⁻¹ f z) = (2 * Real.pi * Complex.I) 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)$.

theorem Complex.circleIntegral_div_sub_of_differentiable_on_off_countable {R : } {c : } {w : } {s : Set } (hs : s.Countable) (hw : w Metric.ball c R) {f : } (hc : ContinuousOn f (Metric.closedBall c R)) (hd : zMetric.ball c R \ s, DifferentiableAt f z) :
(∮ (z : ) in C(c, R), f z / (z - w)) = 2 * Real.pi * Complex.I * f 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)$.

theorem Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {R : NNReal} {c : } {f : E} {s : Set } (hs : s.Countable) (hc : ContinuousOn f (Metric.closedBall c R)) (hd : zMetric.ball c R \ s, DifferentiableAt f z) (hR : 0 < R) :

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.

theorem DiffContOnCl.hasFPowerSeriesOnBall {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {R : NNReal} {c : } {f : E} (hf : DiffContOnCl f (Metric.ball c R)) (hR : 0 < R) :

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.

theorem DifferentiableOn.hasFPowerSeriesOnBall {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {R : NNReal} {c : } {f : E} (hd : DifferentiableOn f (Metric.closedBall c R)) (hR : 0 < R) :

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.

theorem DifferentiableOn.analyticAt {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {s : Set } {f : E} {z : } (hd : DifferentiableOn f s) (hz : s nhds z) :

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).

theorem DifferentiableOn.contDiffOn {E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {s : Set } {f : E} {n : } (hd : DifferentiableOn f s) (hs : IsOpen s) :
ContDiffOn (↑n) f 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