Commit 2025-06-30 12:51 6a0a7c72

feat: existence of local flows of vector fields (#26382) I formalise the existence theorem for local flows of time-dependent vector fields (IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt). Currently, if we wish to show the existence of a family of integral curves indexed by their initial conditions, it is necessary to prove the hypotheses of the vector field (Lipschitz continuity within a closed ball, etc.), centred around each of these initial conditions. I have refactored the current proof of the Picard-Lindelöf theorem to allow the initial point to be different from the point about which the hypotheses on the vector field are stated. This way, integral curves and flows are treated on equal footing. Credits going to the original author @urkud, I have completely rewritten the file to accommodate different design choices. Many of the proof steps are nevertheless inspired by Yury's formalisation.

• The PicardLindelof data structure is removed entirely. It merely bundles the non-Prop arguments into itself. Although it simplifies the assumptions in subsequent proofs, it obscures the (in)dependence on the relevant constants in the type description of theorems. Since IsPicardLindelof is already a public facing structure, we should also simply use it internally, without any loss.
• In particular, I remove the completely superficial dependence of FunSpace on the PicardLindelof structure.
• FunSpace no longer specifies the initial condition. It only needs the initial point to lie in a closed ball (which will be the domain of the local flow).
• I avoid defining new non-Prop things that are only used in the proof steps, such as the current vComp and tDist. The proofs are a little longer as a result, but they are also more readable.
• I place all private (i.e. only internally used) theorems under the namespace FunSpace, to guide users to the proper theorems in the public API. This is part of my effort to show that the solution to an ODE depends smoothly on the initial condition, or on parameters of the ODE. This is in turn needed for many results about manifolds, such as the fact that $C^1$ vector fields on compact manifolds always have global integral curves (or global flows). I especially welcome any suggestions to rename lemmas or define new structures to simplify the statements. I'm happy to write up the proof in LaTeX as well, if it's going to help reviewers.

• depends on: #20696
• depends on: #20731