Integral over a circle in ℂ

In this file we define ∮ z in C(c, R), f z to be the integral ${\oint }_{|z-c|=|R|}f(z),dz$ and prove some properties of this integral. We give definition and prove most lemmas for a function f : ℂ → E, where E is a complex Banach space. For this reason, some lemmas use, e.g., (z - c)⁻¹ • f z instead of f z / (z - c).

Main definitions

• circleMap c R: the exponential map $\theta \mapsto c+R{e}^{\theta i}$;

• CircleIntegrable f c R: a function f : ℂ → E is integrable on the circle with center c and radius R if f ∘ circleMap c R is integrable on [0, 2π];

• circleIntegral f c R: the integral ${\oint }_{|z-c|=|R|}f(z),dz$, defined as ${\int }_0^{2\pi }(c+R{e}^{\theta i}{)}^{\prime }f(c+R{e}^{\theta i}),d\theta$;

• cauchyPowerSeries f c R: the power series that is equal to $\sum _{n=0}^{\mathrm{\infty }}{\oint }_{|z-c|=R}{\left(\frac{w-c}{z-c}\right)}^n\frac{1}{z-c}f(z),dz$ at w - c. The coefficients of this power series depend only on f ∘ circleMap c R, and the power series converges to f w if f is differentiable on the closed ball Metric.closedBall c R and w belongs to the corresponding open ball.

Main statements

• hasFPowerSeriesOn_cauchy_integral: for any circle integrable function f, the power series cauchyPowerSeries f c R, R > 0, converges to the Cauchy integral (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z on the open disc Metric.ball c R;

• circleIntegral.integral_sub_zpow_of_undef, circleIntegral.integral_sub_zpow_of_ne, and circleIntegral.integral_sub_inv_of_mem_ball: formulas for ∮ z in C(c, R), (z - w) ^ n, n : ℤ. These lemmas cover the following cases:

  • circleIntegral.integral_sub_zpow_of_undef, n < 0 and |w - c| = |R|: in this case the function is not integrable, so the integral is equal to its default value (zero);

  • circleIntegral.integral_sub_zpow_of_ne, n ≠ -1: in the cases not covered by the previous lemma, we have (z - w) ^ n = ((z - w) ^ (n + 1) / (n + 1))', thus the integral equals zero;

  • circleIntegral.integral_sub_inv_of_mem_ball, n = -1, |w - c| < R: in this case the integral is equal to 2πi.

  The case n = -1, |w -c| > R is not covered by these lemmas. While it is possible to construct an explicit primitive, it is easier to apply Cauchy theorem, so we postpone the proof till we have this theorem (see #10000).

Notation

• ∮ z in C(c, R), f z: notation for the integral ${\oint }_{|z-c|=|R|}f(z),dz$, defined as ${\int }_0^{2\pi }(c+R{e}^{\theta i}{)}^{\prime }f(c+R{e}^{\theta i}),d\theta$.

Tags

integral, circle, Cauchy integral

circleMap, a parametrization of a circle

def circleMap (c : ℂ) (R : ℝ) : ℝ → ℂ

The exponential map $\theta \mapsto c+R{e}^{\theta i}$. The range of this map is the circle in ℂ with center c and radius |R|.

Equations

• circleMap c R θ = c + ↑R * Complex.exp (↑θ * Complex.I)

theorem periodic_circleMap (c : ℂ) (R : ℝ) : Function.Periodic (circleMap c R) (2 * Real.pi)

circleMap is 2π-periodic.

theorem Set.Countable.preimage_circleMap {s : Set ℂ} (hs : Set.Countable s) (c : ℂ) {R : ℝ} (hR : R ≠ 0) : Set.Countable (circleMap c R ⁻¹' s)

@[simp]

theorem circleMap_sub_center (c : ℂ) (R : ℝ) (θ : ℝ) : circleMap c R θ - c = circleMap 0 R θ

theorem circleMap_zero (R : ℝ) (θ : ℝ) : circleMap 0 R θ = ↑R * Complex.exp (↑θ * Complex.I)

@[simp]

theorem abs_circleMap_zero (R : ℝ) (θ : ℝ) : Complex.abs (circleMap 0 R θ) = |R|

theorem circleMap_mem_sphere' (c : ℂ) (R : ℝ) (θ : ℝ) : circleMap c R θ ∈ Metric.sphere c |R|

theorem circleMap_mem_sphere (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (θ : ℝ) : circleMap c R θ ∈ Metric.sphere c R

theorem circleMap_mem_closedBall (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (θ : ℝ) : circleMap c R θ ∈ Metric.closedBall c R

theorem circleMap_not_mem_ball (c : ℂ) (R : ℝ) (θ : ℝ) : circleMap c R θ ∉ Metric.ball c R

theorem circleMap_ne_mem_ball {c : ℂ} {R : ℝ} {w : ℂ} (hw : w ∈ Metric.ball c R) (θ : ℝ) : circleMap c R θ ≠ w

@[simp]

theorem range_circleMap (c : ℂ) (R : ℝ) : Set.range (circleMap c R) = Metric.sphere c |R|

The range of circleMap c R is the circle with center c and radius |R|.

@[simp]

theorem image_circleMap_Ioc (c : ℂ) (R : ℝ) : circleMap c R '' Set.Ioc 0 (2 * Real.pi) = Metric.sphere c |R|

The image of (0, 2π] under circleMap c R is the circle with center c and radius |R|.

@[simp]

theorem circleMap_eq_center_iff {c : ℂ} {R : ℝ} {θ : ℝ} : circleMap c R θ = c ↔ R = 0

@[simp]

theorem circleMap_zero_radius (c : ℂ) : circleMap c 0 = Function.const ℝ c

theorem circleMap_ne_center {c : ℂ} {R : ℝ} (hR : R ≠ 0) {θ : ℝ} : circleMap c R θ ≠ c

theorem hasDerivAt_circleMap (c : ℂ) (R : ℝ) (θ : ℝ) : HasDerivAt (circleMap c R) (circleMap 0 R θ * Complex.I) θ

theorem differentiable_circleMap (c : ℂ) (R : ℝ) : Differentiable ℝ (circleMap c R)

theorem continuous_circleMap (c : ℂ) (R : ℝ) : Continuous (circleMap c R)

theorem measurable_circleMap (c : ℂ) (R : ℝ) : Measurable (circleMap c R)

@[simp]

theorem deriv_circleMap (c : ℂ) (R : ℝ) (θ : ℝ) : deriv (circleMap c R) θ = circleMap 0 R θ * Complex.I

theorem deriv_circleMap_eq_zero_iff {c : ℂ} {R : ℝ} {θ : ℝ} : deriv (circleMap c R) θ = 0 ↔ R = 0

theorem deriv_circleMap_ne_zero {c : ℂ} {R : ℝ} {θ : ℝ} (hR : R ≠ 0) : deriv (circleMap c R) θ ≠ 0

theorem lipschitzWith_circleMap (c : ℂ) (R : ℝ) : LipschitzWith (Real.nnabs R) (circleMap c R)

theorem continuous_circleMap_inv {R : ℝ} {z : ℂ} {w : ℂ} (hw : w ∈ Metric.ball z R) : Continuous fun (θ : ℝ) => (circleMap z R θ - w)⁻¹

Integrability of a function on a circle

def CircleIntegrable {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (c : ℂ) (R : ℝ) : Prop

We say that a function f : ℂ → E is integrable on the circle with center c and radius R if the function f ∘ circleMap c R is integrable on [0, 2π].

Note that the actual function used in the definition of circleIntegral is (deriv (circleMap c R) θ) • f (circleMap c R θ). Integrability of this function is equivalent to integrability of f ∘ circleMap c R whenever R ≠ 0.

Equations

• CircleIntegrable f c R = IntervalIntegrable (fun (θ : ℝ) => f (circleMap c R θ)) MeasureTheory.volume 0 (2 * Real.pi)

@[simp]

theorem circleIntegrable_const {E : Type u_1} [NormedAddCommGroup E] (a : E) (c : ℂ) (R : ℝ) : CircleIntegrable (fun (x : ℂ) => a) c R

theorem CircleIntegrable.add {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {g : ℂ → E} {c : ℂ} {R : ℝ} (hf : CircleIntegrable f c R) (hg : CircleIntegrable g c R) : CircleIntegrable (f + g) c R

theorem CircleIntegrable.neg {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hf : CircleIntegrable f c R) : CircleIntegrable (-f) c R

theorem CircleIntegrable.out {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ} [NormedSpace ℂ E] (hf : CircleIntegrable f c R) : IntervalIntegrable (fun (θ : ℝ) => deriv (circleMap c R) θ • f (circleMap c R θ)) MeasureTheory.volume 0 (2 * Real.pi)

The function we actually integrate over [0, 2π] in the definition of circleIntegral is integrable.

@[simp]

theorem circleIntegrable_zero_radius {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} : CircleIntegrable f c 0

theorem circleIntegrable_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} (R : ℝ) : CircleIntegrable f c R ↔ IntervalIntegrable (fun (θ : ℝ) => deriv (circleMap c R) θ • f (circleMap c R θ)) MeasureTheory.volume 0 (2 * Real.pi)

theorem ContinuousOn.circleIntegrable' {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hf : ContinuousOn f (Metric.sphere c |R|)) : CircleIntegrable f c R

theorem ContinuousOn.circleIntegrable {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hf : ContinuousOn f (Metric.sphere c R)) : CircleIntegrable f c R

@[simp]

theorem circleIntegrable_sub_zpow_iff {c : ℂ} {w : ℂ} {R : ℝ} {n : ℤ} : CircleIntegrable (fun (z : ℂ) => (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ Metric.sphere c |R|

The function fun z ↦ (z - w) ^ n, n : ℤ, is circle integrable on the circle with center c and radius |R| if and only if R = 0 or 0 ≤ n, or w does not belong to this circle.

@[simp]

theorem circleIntegrable_sub_inv_iff {c : ℂ} {w : ℂ} {R : ℝ} : CircleIntegrable (fun (z : ℂ) => (z - w)⁻¹) c R ↔ R = 0 ∨ w ∉ Metric.sphere c |R|

def circleIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) : E

Definition for ${\oint }_{|z-c|=R}f(z),dz$.

Equations

• circleIntegral f c R = ∫ (θ : ℝ) in 0 ..2 * Real.pi, deriv (circleMap c R) θ • f (circleMap c R θ)

def «term∮_InC(_,_),_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def «term∮_InC(_,_),_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem circleIntegral_def_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) : (∮ (z : ℂ) in C(c, R), f z) = ∫ (θ : ℝ) in Set.Icc 0 (2 * Real.pi), deriv (circleMap c R) θ • f (circleMap c R θ)

@[simp]

theorem circleIntegral.integral_radius_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) : (∮ (z : ℂ) in C(c, 0), f z) = 0

theorem circleIntegral.integral_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {g : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (h : Set.EqOn f g (Metric.sphere c R)) : (∮ (z : ℂ) in C(c, R), f z) = ∮ (z : ℂ) in C(c, R), g z

theorem circleIntegral.integral_sub_inv_smul_sub_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (w : ℂ) (R : ℝ) : (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z

theorem circleIntegral.integral_undef {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hf : ¬CircleIntegrable f c R) : (∮ (z : ℂ) in C(c, R), f z) = 0

theorem circleIntegral.integral_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {g : ℂ → E} {c : ℂ} {R : ℝ} (hf : CircleIntegrable f c R) (hg : CircleIntegrable g c R) : (∮ (z : ℂ) in C(c, R), f z - g z) = (∮ (z : ℂ) in C(c, R), f z) - ∮ (z : ℂ) in C(c, R), g z

theorem circleIntegral.norm_integral_le_of_norm_le_const' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {C : ℝ} (hf : ∀ z ∈ Metric.sphere c |R|, ‖f z‖ ≤ C) : ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * Real.pi * |R| * C

theorem circleIntegral.norm_integral_le_of_norm_le_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {C : ℝ} (hR : 0 ≤ R) (hf : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) : ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * Real.pi * R * C

theorem circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {C : ℝ} (hR : 0 ≤ R) (hf : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) : ‖(2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C

theorem circleIntegral.norm_integral_lt_of_norm_le_const_of_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {C : ℝ} (hR : 0 < R) (hc : ContinuousOn f (Metric.sphere c R)) (hf : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) (hlt : ∃ z ∈ Metric.sphere c R, ‖f z‖ < C) : ‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * Real.pi * R * C

If f is continuous on the circle |z - c| = R, R > 0, the ‖f z‖ is less than or equal to C : ℝ on this circle, and this norm is strictly less than C at some point z of the circle, then ‖∮ z in C(c, R), f z‖ < 2 * π * R * C.

@[simp]

theorem circleIntegral.integral_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {𝕜 : Type u_2} [RCLike 𝕜] [NormedSpace 𝕜 E] [SMulCommClass 𝕜 ℂ E] (a : 𝕜) (f : ℂ → E) (c : ℂ) (R : ℝ) : (∮ (z : ℂ) in C(c, R), a • f z) = a • ∮ (z : ℂ) in C(c, R), f z

@[simp]

theorem circleIntegral.integral_smul_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (f : ℂ → ℂ) (a : E) (c : ℂ) (R : ℝ) : (∮ (z : ℂ) in C(c, R), f z • a) = (∮ (z : ℂ) in C(c, R), f z) • a

@[simp]

theorem circleIntegral.integral_const_mul (a : ℂ) (f : ℂ → ℂ) (c : ℂ) (R : ℝ) : (∮ (z : ℂ) in C(c, R), a * f z) = a * ∮ (z : ℂ) in C(c, R), f z

@[simp]

theorem circleIntegral.integral_sub_center_inv (c : ℂ) {R : ℝ} (hR : R ≠ 0) : (∮ (z : ℂ) in C(c, R), (z - c)⁻¹) = 2 * ↑Real.pi * Complex.I

theorem circleIntegral.integral_eq_zero_of_hasDerivWithinAt' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {f' : ℂ → E} {c : ℂ} {R : ℝ} (h : ∀ z ∈ Metric.sphere c |R|, HasDerivWithinAt f (f' z) (Metric.sphere c |R|) z) : (∮ (z : ℂ) in C(c, R), f' z) = 0

If f' : ℂ → E is a derivative of a complex differentiable function on the circle Metric.sphere c |R|, then ∮ z in C(c, R), f' z = 0.

theorem circleIntegral.integral_eq_zero_of_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {f' : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (h : ∀ z ∈ Metric.sphere c R, HasDerivWithinAt f (f' z) (Metric.sphere c R) z) : (∮ (z : ℂ) in C(c, R), f' z) = 0

If f' : ℂ → E is a derivative of a complex differentiable function on the circle Metric.sphere c R, then ∮ z in C(c, R), f' z = 0.

theorem circleIntegral.integral_sub_zpow_of_undef {n : ℤ} {c : ℂ} {w : ℂ} {R : ℝ} (hn : n < 0) (hw : w ∈ Metric.sphere c |R|) : (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0

If n < 0 and |w - c| = |R|, then (z - w) ^ n is not circle integrable on the circle with center c and radius |R|, so the integral ∮ z in C(c, R), (z - w) ^ n is equal to zero.

theorem circleIntegral.integral_sub_zpow_of_ne {n : ℤ} (hn : n ≠ -1) (c : ℂ) (w : ℂ) (R : ℝ) : (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0

If n ≠ -1 is an integer number, then the integral of (z - w) ^ n over the circle equals zero.

def cauchyPowerSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) : FormalMultilinearSeries ℂ ℂ E

The power series that is equal to $\frac{1}{2\pi i}\sum _{n=0}^{\mathrm{\infty }}{\oint }_{|z-c|=R}{\left(\frac{w-c}{z-c}\right)}^n\frac{1}{z-c}f(z),dz$ at w - c. The coefficients of this power series depend only on f ∘ circleMap c R, and the power series converges to f w if f is differentiable on the closed ball Metric.closedBall c R and w belongs to the corresponding open ball. For any circle integrable function f, this power series converges to the Cauchy integral for f.

Equations

• cauchyPowerSeries f c R n = ContinuousMultilinearMap.mkPiRing ℂ (Fin n) ((2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)

theorem cauchyPowerSeries_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ) (w : ℂ) : ((cauchyPowerSeries f c R n) fun (x : Fin n) => w) = (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z

theorem norm_cauchyPowerSeries_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ) : ‖cauchyPowerSeries f c R n‖ ≤ ((2 * Real.pi)⁻¹ * ∫ (θ : ℝ) in 0 ..2 * Real.pi, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n

theorem le_radius_cauchyPowerSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : NNReal) : ↑R ≤ FormalMultilinearSeries.radius (cauchyPowerSeries f c ↑R)

theorem hasSum_two_pi_I_cauchyPowerSeries_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ} (hf : CircleIntegrable f c R) (hw : Complex.abs w < R) : HasSum (fun (n : ℕ) => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

For any circle integrable function f, the power series cauchyPowerSeries f c R multiplied by 2πI converges to the integral ∮ z in C(c, R), (z - w)⁻¹ • f z on the open disc Metric.ball c R.

theorem hasSum_cauchyPowerSeries_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ} (hf : CircleIntegrable f c R) (hw : Complex.abs w < R) : HasSum (fun (n : ℕ) => (cauchyPowerSeries f c R n) fun (x : Fin n) => w) ((2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

For any circle integrable function f, the power series cauchyPowerSeries f c R, R > 0, converges to the Cauchy integral (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z on the open disc Metric.ball c R.

theorem sum_cauchyPowerSeries_eq_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ} (hf : CircleIntegrable f c R) (hw : Complex.abs w < R) : FormalMultilinearSeries.sum (cauchyPowerSeries f c R) w = (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z

For any circle integrable function f, the power series cauchyPowerSeries f c R, R > 0, converges to the Cauchy integral (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z on the open disc Metric.ball c R.

theorem hasFPowerSeriesOn_cauchy_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : NNReal} (hf : CircleIntegrable f c ↑R) (hR : 0 < R) : HasFPowerSeriesOnBall (fun (w : ℂ) => (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) (cauchyPowerSeries f c ↑R) c ↑R

For any circle integrable function f, the power series cauchyPowerSeries f c R, R > 0, converges to the Cauchy integral (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z on the open disc Metric.ball c R.

theorem circleIntegral.integral_sub_inv_of_mem_ball {c : ℂ} {w : ℂ} {R : ℝ} (hw : w ∈ Metric.ball c R) : (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑Real.pi * Complex.I

Integral ${\oint }_{|z-c|=R}\frac{dz}{z-w}=2\pi i$ whenever $|w-c|<R$.