Has anyone made any work to have topological structures on top of complex numbers, to be able to use both the work of Guillaume Cano on matrix jordan forms (and the like) and continuity results (possibly coming from Coquelicot).

Sophie Bernard had a Cstruct file (still available on github here and this suggests that one should use the complexfield construction from real-closed, but this was before the advent of math-comp analysis. Does anybody have something more up-to-date?

This might be a question for @Marie Kerjean

In the branch holomorphy I have defined topological structures on the top of real-closed' complex numbers. It is straightforward if one only chooses to deal with a single vector space structure on complexes, but this development aimed at dealing with C as a vector space over itself and also over R, and fails to do so efficiently.

This section defines a topology on Rcomplex, an alias fo C as an Rmodule.

This section straighforwarldy defines the topology of C as a field.

@Yves Bertot @Cyril Cohen @Marie Kerjean Thanks for the pointers. I was looking at the existing mathcomp-analysis package available for installation via opam and I could not locate the holomorphy file for use. Is this file available as part of the new development ? When would this be available for use ?

I think the right way to access the information is the holomorphy branch on github.

https://github.com/math-comp/analysis/tree/holomorphy

This is work in progress. If I were to attempt using it,

The first solution is that I would clone the github repository, type `git checkout holomorphy`

, and then use some `opam pin`

command to install that version of analysis instead of the one you are using now.

The second solution is that I would only copy-paste the parts of the development that Marie has been pointing to in a file of my own, and work with this on a temporary basis.

Maybe we should include the relevant parts in the main branch of math-comp analysis, so that they will be in the next release.

Thanks Yves for the suggestion

is there a def of complex numbers as an extension of the reals in math-comp analysis? (or math-comp for that matter)?

Barry Trager said:

is there a def of complex numbers as an extension of the reals in math-comp analysis? (or math-comp for that matter)?

Yes, you can use import `complex`

and use the notation `R[i]`

https://github.com/math-comp/real-closed/blob/master/theories/complex.v

Last updated: Jun 25 2024 at 19:01 UTC