integral curves on manifold

Stream: maths

[Winston Yin]

I've been working on proving the existence of integral curves for smooth vector fields on manifolds. So far I've shown that the integral curve exists in an open interval around t = 0 whenever the initial point x : M is not on the boundary. Would anyone like to take a look?

Next steps would be the fundamental theorem of flows and maybe exponential maps of Lie algebra being integral curves of left-invariant vector fields on the Lie group.

[Winston Yin]

I've made this PR: #17140. I'm not totally satisfied with the way I've split the theorem up into lemmas, and I feel that some generalisation or further splitting can be useful. I'd love to hear any suggestions in this regard! It's probably not quite ready for stylistic comments yet.