Stream: math-comp analysis

Topic: topological structures on complex numbers


view this post on Zulip Yves Bertot (Jul 05 2021 at 07:26):

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?

view this post on Zulip Cyril Cohen (Jul 05 2021 at 08:01):

This might be a question for @Marie Kerjean

view this post on Zulip Marie Kerjean (Jul 05 2021 at 08:57):

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.

view this post on Zulip Marie Kerjean (Jul 05 2021 at 08:58):

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

view this post on Zulip Marie Kerjean (Jul 05 2021 at 09:00):

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

view this post on Zulip Mohit Tekriwal (Jul 06 2021 at 04:27):

@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 ?

view this post on Zulip Yves Bertot (Jul 06 2021 at 11:10):

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.

view this post on Zulip Mohit Tekriwal (Jul 06 2021 at 13:00):

Thanks Yves for the suggestion

view this post on Zulip Barry Trager (Jun 21 2023 at 18:10):

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

view this post on Zulip Cyril Cohen (Jun 21 2023 at 20:37):

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: Mar 29 2024 at 10:01 UTC