Stream: math-comp analysis

Topic: Next project to work on

view this post on Zulip Zachary Stone (Aug 29 2022 at 20:55):

I'm gonna have a bunch of time to work on math stuff for the next few weeks. Is there something I can focus on that would be useful to other folks? I'm thinking about

view this post on Zulip Cyril Cohen (Aug 30 2022 at 07:11):

@Zachary Stone either of your two last items look very useful! I'm not sure if someone else is working on it (CC @Marie Kerjean @Reynald Affeldt ) but I'm not.

view this post on Zulip Zachary Stone (Aug 30 2022 at 22:22):

I guess I'll work on the homotopy stuff then. The integration stuff relies on dual spaces, which relies on sensible vector subspaces. That seems likely to change with HB improvements. If there are any existing materials on paths/homotopies I should know about, I'd be happy to see them. Otherwise I'll just start with some HB mixins for paths and loops and see how far I get.

view this post on Zulip Marie Kerjean (Aug 31 2022 at 15:06):

I don't plan to work on any of your two items (I would love to see more of holomorphic functions ported though). As soon as the port to HB is successful I would love to start working on duality theory and topological vector spaces. Also, @Cyril Cohen if I can be of any help on HB let me know (it happened while I was away, and as far as I can see there only remains technicalities on which I'm not sure I can help).

view this post on Zulip Zachary Stone (Sep 01 2022 at 18:51):

I've posted a first pass of HB structures for paths. A long way to go to define winding numbers, but it's a start.

view this post on Zulip Zachary Stone (Sep 01 2022 at 21:59):

So I have a crazy idea, but I'm not sure how to do it.

I suspect there's an elegant approach to define path homotopies on X as paths in the "PathSpace" of X. That is, the set of paths on X, equipped with the uniform topology. If we can get this right, then

  1. Chaining homotopies is a trivial application of chaining paths.
  2. Same with reversing paths, constant homotopies, etc
  3. Path-connectedness partitions a topological space -> homotopies are an equivalence relation
  4. We'll be better positioned to work with general homotopies from A -> B as paths in {family compact, A -> B}.
    probably some other major conveniences.

I can figure out the proofs, but I am not sure about some of the other issues.

Last updated: Feb 05 2023 at 13:02 UTC