feat(analysis/analytic/isolated_zeros): Principle of isolated zeros

[vbeffara]

Local version: an analytic function is either locally zero, or nonzero in a punctured neighborhood.

---

Second take on #14382 but starting from scratch.

[b-mehta]

I don't have anything to add to Anatole's comments, but just to say it would be great to have this in mathlib!

[ADedecker]

With Vincent's agreement, I pushed some changes directly on the branch because it was the occasion to add quite a bunch of API and that was easier to do than to explain. I didn't touch any mathematically interesting part. Unfortunately this made the PR more spread out and quite longer, so if you have time to spend splitting it would be nice for the next reviewer. Also, I won't approve the PR since I made significant changes, but I think this is a really good PR, the proofs using dslope are really nice!

[vbeffara]

Thanks for all the comments and changes! I will need some time to process all the mk_pi stuff, but just to answer 2 questions that came up related to a previous version of the PR:

• having order live in with_top nat was indeed my first intuition, but it made using it slightly annoying because of all the coercions between nat and with_top nat, and besides many lemmas were true when order was either 0 or top. The value of order 0 should probably be considered a junk value anyway.
• the definition of p.coef n instead of using p n 1 was a basic definition that removed some mental overhead, plus it allows for a few nice simp lemmas, so I believe it can be useful. Anything to make formal_multilinear_series more approachable, this part of the library is quite nice to use but the learning curve is rather steep...

[ADedecker]

I will need some time to process all the mk_pi stuff

Yeah don't worry about that, I see a lot of people struggling with this and the multiple variations on it, and I definitely did too. I think part of the problem is the name here, but basically I'm just using the fact that for a k-multilinear map f from k^n to E, you don't have any other choice than sending (x_i) to (∏i, x_i) • f (1, 1, ..., 1).

[vbeffara]

In filter.tendsto.eventually_ne as it is now, the linter says that α does not have to be a topological_space, which makes sense. I just added a microscopic commit to appease the linter.

[jcommelin]

Thanks :tada:

bors merge

[bors[bot]]

Build failed (retrying...):

• Lint mathlib

[bors[bot]]

Build failed:

• Lint mathlib

[vbeffara]

The PR has gone a little stale, I just merged master and it doesn't build anymore (same issue as in #16074), let's fix it

[jcommelin]

bors d+

[bors[bot]]

:v: vbeffara can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[vbeffara]

bors r+

[bors[bot]]

Build failed (retrying...):

• Run tests

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests