Commit 2025-07-15 19:54 5bfba479

View on Github →

feat: solution to ODE is Lipschitz with respect to the initial condition (#26392) This PR continues the work from #20733. Original PR: https://github.com/leanprover-community/mathlib4/pull/20733 I formalise a corollary to the Picard-Lindelöf theorem: the local solution to an ODE is Lipschitz continuous with respect to the initial condition. This in particular means that the local flow to the associated vector field is continuous.

Estimated changes

Modified Mathlib/Analysis/ODE/PicardLindelof.lean

added theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn

added theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith

added theorem ODE.FunSpace.dist_iterate_iterate_next_le_of_lipschitzWith

added theorem ODE.FunSpace.dist_iterate_next_le

added theorem ODE.FunSpace.dist_next_next

added theorem ODE.FunSpace.exists_forall_closedBall_funSpace_dist_le_mul