AnalyticManifold

Stream: mathlib4

[Geoffrey Irving]

I'd be interested in upstreaming AnalyticManifold and holomorphic functions to Mathlib from https://github.com/girving/ray/blob/main/Ray/AnalyticManifold/AnalyticManifold.lean. Would this be appreciated? If so, I can make a PR.

The main flaw is that I currently have AnalyticManifold defined only in the boundaryless case. I can easily fix this for the definition of AnalyticManifold, but it would be a bit more work to map all the holomorphicity lemmas to the boundary case.

[Johan Commelin]

It is good to make definitions as general as possible. For lemmas it is of course also good, but a bit less important. Those can be generalize more gradually.

[Geoffrey Irving]

I'll fix AnalyticManifold. For holomorphicAt, I suppose the correct definition is (1) analytic in charts if we're in the interior, and (2) smooth in charts at boundary points?

Also happy to change names: using holomorphic is a bit overly cute (similar to smooth), mainly because manalytic looked annoying.