Commit 2026-05-30 22:11 b8219087

View on Github →

refactor(Analysis/ODE): move public-facing existence and uniqueness theorems to dedicated file (#35043)

Create Mathlib/Analysis/ODE/ExistUnique.lean to collect existence and uniqueness results for ODEs.
Move the Picard-Lindelöf existence theorems from PicardLindelof.lean.
Move the Grönwall-based uniqueness theorems from Gronwall.lean. A future PR will restate these results using the IsIntegralCurve API.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/ODE/ExistUnique.lean

added theorem ContDiffAt.exists_eventually_eq_hasDerivAt

added theorem ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt

added theorem ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀

added theorem IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt

added theorem IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt₀

added theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt

added theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn

added theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith

added theorem ODE_solution_unique

added theorem ODE_solution_unique_of_eventually

added theorem ODE_solution_unique_of_mem_Icc

added theorem ODE_solution_unique_of_mem_Icc_left

added theorem ODE_solution_unique_of_mem_Icc_right

added theorem ODE_solution_unique_of_mem_Ioo

added theorem ODE_solution_unique_univ

Modified Mathlib/Analysis/ODE/Gronwall.lean

deleted theorem ODE_solution_unique

deleted theorem ODE_solution_unique_of_eventually

deleted theorem ODE_solution_unique_of_mem_Icc

deleted theorem ODE_solution_unique_of_mem_Icc_left

deleted theorem ODE_solution_unique_of_mem_Icc_right

deleted theorem ODE_solution_unique_of_mem_Ioo

deleted theorem ODE_solution_unique_univ

Modified Mathlib/Analysis/ODE/PicardLindelof.lean

deleted theorem ContDiffAt.exists_eventually_eq_hasDerivAt

deleted theorem ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt

deleted theorem ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀

deleted theorem IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt

deleted theorem IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt₀

deleted theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt

deleted theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn

deleted theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith

Modified Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean