# 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` #

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

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

source
theorem hasDerivAt_circleMap (c : ℂ) (R θ : ℝ) :
HasDerivAt (circleMap c R) (circleMap 0 R θ * Complex.I) θ
source
theorem differentiable_circleMap (c : ℂ) (R : ℝ) :
Differentiable ℝ (circleMap c R)
source
theorem analyticOnNhd_circleMap (c : ℂ) (R : ℝ) :
AnalyticOnNhd ℝ (circleMap c R) Set.univ

The circleMap is real analytic.

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

The circleMap is continuously differentiable.

source
theorem continuous_circleMap (c : ℂ) (R : ℝ) :
Continuous (circleMap c R)
source
theorem measurable_circleMap (c : ℂ) (R : ℝ) :
Measurable (circleMap c R)
source
@[simp]
theorem deriv_circleMap (c : ℂ) (R θ : ℝ) :
deriv (circleMap c R) θ = circleMap 0 R θ * Complex.I
source
theorem deriv_circleMap_eq_zero_iff {c : ℂ} {R θ : ℝ} :
deriv (circleMap c R) θ = 0 ↔ R = 0
source
theorem deriv_circleMap_ne_zero {c : ℂ} {R θ : ℝ} (hR : R ≠ 0) :
deriv (circleMap c R) θ ≠ 0
source
theorem lipschitzWith_circleMap (c : ℂ) (R : ℝ) :
LipschitzWith (Real.nnabs R) (circleMap c R)
source
theorem continuous_circleMap_inv {R : ℝ} {z w : ℂ} (hw : w ∈ Metric.ball z R) :
Continuous fun (θ : ℝ) => (circleMap z R θ - w)⁻¹
source
theorem circleMap_preimage_codiscrete {c : ℂ} {R : ℝ} (hR : R ≠ 0) :
Filter.map (circleMap c R) (Filter.codiscrete ℝ) ≤ Filter.codiscreteWithin (Metric.sphere c |R|)
source
theorem circleMap_neg_radius {r x : ℝ} {c : ℂ} :
circleMap c (-r) x = circleMap c r (x + Real.pi)

### Integrability of a function on a circle #

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

Instances For

source
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)
source
@[simp]
theorem circleIntegrable_const {E : Type u_1} [NormedAddCommGroup E] (a : E) (c : ℂ) (R : ℝ) :
CircleIntegrable (fun (x : ℂ) => a) c R
source
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|`.

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

source
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

`finsum`s of circle integrable functions are circle integrable.

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

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

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

source
@[simp]
theorem circleIntegrable_zero_radius {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} :
CircleIntegrable f c 0
source
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.

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

source
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)
source
theorem ContinuousOn.circleIntegrable' {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hf : ContinuousOn f (Metric.sphere c |R|)) :
CircleIntegrable f c R
source
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
source
@[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.

source
@[simp]
theorem circleIntegrable_sub_inv_iff {c w : ℂ} {R : ℝ} :
CircleIntegrable (fun (z : ℂ) => (z - w)⁻¹) c R ↔ R = 0 ∨ w ∉ Metric.sphere c |R|
source
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 θ)

Instances For

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

Instances For

source
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 θ)
source
@[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
source
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
source
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.

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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`.

source
@[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
source
@[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
source
@[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
source
@[simp]
theorem circleIntegral.integral_sub_center_inv (c : ℂ) {R : ℝ} (hR : R ≠ 0) :
∮ (z : ℂ) in C(c, R), (z - c)⁻¹ = 2 * ↑Real.pi * Complex.I
source
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`.

source
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`.

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

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

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

Instances For

source
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
source
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
source
theorem le_radius_cauchyPowerSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : NNReal) :
↑R ≤ (cauchyPowerSeries f c ↑R).radius
source
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`.

source
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`.

source
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`.

source
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`.

source
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$.