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

[vbeffara]

This is a first step towards isolated zeros / analytic continuation for analytic functions in one variable. The proof is by induction in the order of the zero, which is perhaps not optimal but necessitated the least amount of additional API for power series in one variable.

---

[vbeffara]

Updated proof, with a more explicit argument (f z can be factored as (z - z0) ^ n * iterated_dslope f n)

[sgouezel]

The linter is not happy. Can you fix it by adding the missing docstring?

[vbeffara]

That should do it. I'm not sure though whether this definition is strictly needed (which is why it did not have a docstring in the first place). I do believe that we need a way to state "this sequence is summable and its sum satisfies this relation" and that was my attempt to do that, but even if it serves the API should be fleshed out.

[urkud]

I think that we should have formal_multilinear_series.order for any multilinear series. Then you can prove that the sum of a series is its first term plus O(...). BTW, you can use supr or infi to define it without dite.

[vbeffara]

Yes, indeed it makes sense to generalize the definition to the general case, although I was a bit afraid of matching p.coef n = 0 with p n = 0.

Saying order := Inf { n | p n = 0 } means that the order of the zero series would be 0 rather than \top, but in retrospect I am leaning more and more towards this option.

[sgouezel]

I agree that it would make sense to have this for a general formal multilinear series. And having order 0 = 0 is probably easier to use, indeed. Would you agree to make this change (and move this definition to another file)?