Stream: math-comp analysis

Topic: Next project to work on

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

• is there something regarding hierarchy builder where I could contribute?
• I have this coquelicot proof of holomorphic implies analytic I never fully ported. The big pieces of it were: contour integration, compact convergence, homotopies, and geometric series. Perhaps paths and homotopies is a good thing to do?
• Integration in general vector spaces is pretty important. The "Bochner" and "Pettis" integrals will let us extend Lebesgue integrals without too much extra machinery.

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.

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.

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).

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.

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.

• A generalization issue: How much do we care that X : topologialType rather than X : uniformType? We already have the uniform topology stuff done for for uniformType. Otherwise we'll need to define the compact-open topology and prove stuff stuff about it.
• How should I equip Path.type and Loop.type with a topology? Is it better to treat these as subspaces of {uniform, [0,1] -> T} or use the weak topology construction directly?
• Is this gonna be one of those things where waiting for Topology and Uniform to enter HB will be easier? There's plenty to prove about paths in the meanwhile, so I'm definitely not blocked.

Last updated: Oct 13 2024 at 01:02 UTC