Rough paths & signatures

Stream: Is there code for X?

[Josha Dekker]

Do we have (some of) the theory on rough path theory and/or signatures?

[Kevin Buzzard]

We don't really have anything on differential equations at all

[Josha Dekker]

Okay, I'll postpone working on these then ... I don't think I have the Lean skills nor the time to set that up at this point...

[Kevin Buzzard]

If you know something about differential equations yourself (I don't have the first clue about them) then it might be nice to come up with a challenge problem which you think might be accessible; you could open it as an issue on the mathlib4 repo, for example, or make it into a github project. People are always looking for projects.

[Josha Dekker]

Thank you for the suggestion. I know some differential equations, but I’m not too sure about the level of generality that we should approach this at (over Euclidean spaces or in more generality?). Perhaps a resident expert on the topic can shed some light on this?

[Josha Dekker]

If I'm reading the documentation for Analysis/ODE/PicardLindelof correctly, I don't think this is yet the full strength of the Picard-Lindelöf theorem. Similarly, I think we're missing the Peano existence theorem, so these might be obvious targets?