Cauchy's residue theorem on punctured disk

Stream: Is there code for X?

[Daniel Eriksson]

As a project over a few weeks in a Lean PhD course, I am planning to try to formalize the residue theorem for circles on a punctured disk:
If f has a Laurent expansion $f(z)=\sum_{n=-\infty}^{\infty} a_n z^n$ on the punctured disk $B_R(0)-{0}$ then for 0<r<R $\oint_{|z|=r} f(z) dz= 2\pi i a_{-1}$. Is anyone working on something like this? 

I looked at what there is in Mathlib and will try to build on it. There is an issue that I want to have coefficients in Laurent expansion as input but in Mathlib Cauchy series are built from explicitly from f. 

In Mathlib, there is

1. Cauchy theorem for circles: if f is continuous on closed disk and complex differentiable at all but finitely many point in its interior then the integral of any circle in disk is zero, see 

Complex.circleIntegral_eq_zero_of_differentiable_on_off_countable.

2. If f is complex differentiable on a closed disk, it has a power series on the corresponding open disk with coefficients given by Cauchy Integral Formula, see

DifferentiableOn.hasFPowerSeriesOnBall.

3. Integral around C(c,r) of (z-c)^n = 0 if n ≠ -1, 0 otherwise, see

Complex.circleIntegral.integral_sub_zpow_of_ne and Complex.circleIntegral.integral_sub_inv_of_mem_ball

4. cauchyPowerSeries f c R: power series with coefficients given by Cauchy integral formula,

implemented as a formal multilinear series which in turn is implemented as a family of multilinear maps

The main thing task would be to define Laurent series valid on annuli r<|z|<R and show uniform convergence on closed sub annuli. It seems not so obvious how to implement statements like ”f has an expansion”.

I was thinking something like this:

theorem integral_circle_in_punctured_disk__is_mult_residue {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E]

(r R:ℝ)(Rpos:R>0)(hr:0<r∧r<R)(a:ℤ → ℂ)(f:ℂ→E ) (h: hasLaurentSeriesOnAnnulus f a 0 R)

:  (∮ z in C(c, r), f z) = 2 * π * I * (a -1) := by sorry

The steps would be 

1. Define LaurentSeries with input a function f:C->E, coefficients defined by a:Z->C and radii 0<r<R

Idea: Sum of a cauchyPowerSeries f z R in z for |z|<R and a cauchyPowerSeries f z^(-1) r^(-1) in z^(-1) for |z|>r

2. Define a structure hasLaurentSeriesOnAnnulus similar to hasFPowerSeriesOnBall

3. Prove Laurent series converges uniformly on closed sub annuli

4. Use 3 to integrate the integral term by term and use 3 above to evaluate the integral

What do you think?

[Yury G. Kudryashov]

You may want to use (or not) docs#LaurentSeries

[Daniel Eriksson]

Oh didn't find, thanks!