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

• 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π}(c + Re^{θ i})' f(c+Re^{θ i})\,dθ$;

• cauchyPowerSeries f c R: the power series that is equal to $\sum_{n=0}^{\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 https://github.com/leanprover-community/mathlib4/pull/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π}(c + Re^{θ i})' f(c+Re^{θ i})\,dθ$.

Tags

integral, circle, Cauchy integral

Facts about circleMap

@[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|.

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

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

theorem analyticOnNhd_circleMap (c : ℂ) (R : ℝ) : AnalyticOnNhd ℝ (circleMap c R) Set.univ

The circleMap is real analytic.

theorem contDiff_circleMap (c : ℂ) (R : ℝ) {n : WithTop ℕ∞} : ContDiff ℝ n (circleMap c R)

The circleMap is continuously differentiable.

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)⁻¹

theorem circleMap_preimage_codiscrete {c : ℂ} {R : ℝ} (hR : R ≠ 0) : Filter.map (circleMap c R) (Filter.codiscrete ℝ) ≤ Filter.codiscreteWithin (Metric.sphere c |R|)

theorem circleMap_neg_radius {r x : ℝ} {c : ℂ} : circleMap c (-r) x = circleMap c r (x + Real.pi)

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)

theorem circleIntegrable_def {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (c : ℂ) (R : ℝ) : 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.abs {c : ℂ} {R : ℝ} {f : ℂ → ℝ} (hf : CircleIntegrable f c R) : CircleIntegrable |f| c R

Analogue of IntervalIntegrable.abs: If a real-valued function f is circle integrable, then so is |f|.

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

theorem CircleIntegrable.sum {E : Type u_1} [NormedAddCommGroup E] {c : ℂ} {R : ℝ} {ι : Type u_3} (s : Finset ι) {f : ι → ℂ → E} (h : ∀ i ∈ s, CircleIntegrable (f i) c R) : CircleIntegrable (∑ i ∈ s, f i) c R

Sums of circle integrable functions are circle integrable.

theorem CircleIntegrable.fun_sum {E : Type u_1} [NormedAddCommGroup E] {c : ℂ} {R : ℝ} {ι : Type u_3} (s : Finset ι) {f : ι → ℂ → E} (h : ∀ i ∈ s, CircleIntegrable (f i) c R) : CircleIntegrable (fun (z : ℂ) => ∑ i ∈ s, f i z) c R

Sums of circle integrable functions are circle integrable.

theorem CircleIntegrable.finsum {E : Type u_1} [NormedAddCommGroup E] {c : ℂ} {R : ℝ} {ι : Type u_3} {f : ι → ℂ → E} (h : ∀ (i : ι), CircleIntegrable (f i) c R) : CircleIntegrable (∑ᶠ (i : ι), f i) c R

finsums of circle integrable functions are circle integrable.

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

theorem CircleIntegrable.const_smul {c : ℂ} {R : ℝ} {A : Type u_2} [NormedRing A] {a : A} {f : ℂ → A} (h : CircleIntegrable f c R) : CircleIntegrable (a • f) c R

If f is circle integrable, then so are its scalar multiples.

theorem CircleIntegrable.const_fun_smul {c : ℂ} {R : ℝ} {A : Type u_2} [NormedRing A] {a : A} {f : ℂ → A} (h : CircleIntegrable f c R) : CircleIntegrable (fun (z : ℂ) => a • f z) c R

If f is circle integrable, then so are its scalar multiples.

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.congr_codiscreteWithin {E : Type u_1} [NormedAddCommGroup E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E} (hf : f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂) (hf₁ : CircleIntegrable f₁ c R) : CircleIntegrable f₂ c R

Circle integrability is invariant when functions change along discrete sets.

theorem circleIntegrable_congr_codiscreteWithin {E : Type u_1} [NormedAddCommGroup E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E} (hf : f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂) : CircleIntegrable f₁ c R ↔ CircleIntegrable f₂ c R

Circle integrability is invariant when functions change along discrete sets.

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(_,_),_» : Lean.ParserDescr

∮ z in C(c, R), f z is the circle integral $\oint_{|z-c|=R} f(z)\,dz$.

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 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.circleIntegral_congr_codiscreteWithin {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → ℂ} (hf : f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂) (hR : R ≠ 0) : ∮ (z : ℂ) in C(c, R), f₁ z = ∮ (z : ℂ) in C(c, R), f₂ z

Circle integrals are invariant when functions change along discrete sets.

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_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f 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.integral_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f 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.integral_fun_sum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ι : Type u_2} {s : Finset ι} {f : ι → ℂ → E} {c : ℂ} {R : ℝ} (h : ∀ i ∈ s, CircleIntegrable (f i) c R) : ∮ (z : ℂ) in C(c, R), ∑ i ∈ s, f i z = ∑ i ∈ s, ∮ (z : ℂ) in C(c, R), f i 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 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 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πi}\sum_{n=0}^{\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 ≤ (cauchyPowerSeries f c ↑R).radius

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 : ‖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 : ‖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 : ‖w‖ < R) : (cauchyPowerSeries f c R).sum 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πi$ whenever $|w-c| < R$.