Zulip Chat Archive

Stream: Is there code for X?

Topic: Locally convex spaces and convinient vector spaces


view this post on Zulip Tomas Skrivan (Oct 16 2020 at 22:01):

Looking at the mathlib documentation, there is not a library for locally convex spaces. Is someone working on it?

Also, I would be really interested in having formalization of convinient vector spaces. I'm interested in doing differentiable programming and since convinient vector spaces form a closed cartesion category they should be the ideal setting for formalizing this.

view this post on Zulip Yury G. Kudryashov (Oct 17 2020 at 01:50):

There is a PR #1926 with local convexity but it seems that the author is not interested in getting it merged.

view this post on Zulip Yury G. Kudryashov (Oct 17 2020 at 01:51):

I think that you may take over this PR if you want.

view this post on Zulip Tomas Skrivan (Oct 17 2020 at 11:17):

Nice, I will look into it but I'm not sure if I have the time to take over this.


Last updated: May 16 2021 at 05:21 UTC