compact limits of holomorphic functions

Stream: PR reviews

[Vincent Beffara]

There are currently two PRs proving some version of the fact that (locally) uniform limits of holomorphic functions are holomorphic:

• #13500 by @Chris Birkbeck which has been sitting in the queue for a while, and
• #17074 which I submitted yesterday (I wasn't aware of the existence of the other one)

Chris and I chatted this morning and reached a conclusion: his PR does not compile anymore, my version uses a different approach and shows the additional fact that derivatives also converge locally uniformly, which is useful. OTOH his PR introduces some API for circle integrals which would be desirable for other things, typically proving Cauchy's formulas for higher derivatives. So we reached a proposal: I leave my PR now in the review process, he keeps the circle integral API from his, and we try to get all that into mathlib.

Does that sound reasonable? @Bhavik Mehta @Anatole Dedecker @Kevin Wilson

[Chris Birkbeck]

I should add that #13500 was too big for one single PR, so I split it into parts, the first two being : #13885 and #15356 the first of which is in mathlib and the second is in the queue (and should now compile!)

[Bhavik Mehta]

This sounds sensible to me, although I haven't looked at the PRs in much detail

[Vincent Beffara]

The locally uniform convergence API part of my PR is now in #17092 for easier review.

[Vincent Beffara]

Just a small ping: #17092 is now merged, so #17074 about locally uniform limits of holomorphic functions being holomorphic has no dependency anymore. It built correctly 3 weeks ago, I will merge master into it to make sure everything works smoothly but I'm not anticipating a lot of change due to the merge.

[Vincent Beffara]

Merged. I only had to replace \|| with \Vert everywhere :-)