Stream: Is there code for X?
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.
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.
Yury G. Kudryashov (Oct 17 2020 at 01:51):
I think that you may take over this PR if you want.
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