Revision #1439 → #3487 · back to history
modifiedPicard–Lindelöf theorem0b75d13c1b1e
| Field | From #1439 | To #3487 |
|---|
| mathlib.module | Mathlib.Analysis.ODE.PicardLindelof | Mathlib.Analysis.ODE.ExistUnique |
| note | Local existence is given by `exists_eq_forall_mem_Icc_hasDerivWithinAt` and uniqueness by `ODE_solution_unique` in `Mathlib.Analysis.ODE.Gronwall`. | Local existence is given by `IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt` and uniqueness by `ODE_solution_unique`, both in `Mathlib.Analysis.ODE.ExistUnique`. |
addedBoundary value problemfa0000df2cb3
addedLinear multistep method (classification)ccdbb984386e
addedStiff differential equation (rule of thumb)c9340f7e827b
addedSymplectic integratorff18098871cb
modifiedGlobal error of one-step method implies convergence38120a2eb193
| Field | From #1439 | To #3487 |
|---|
| note | This convergence result for one-step methods is not formalized in Mathlib, though `discrete_gronwall` provides related discrete error-bound infrastructure. | This convergence result for one-step methods is not formalized in Mathlib, though `discrete_gronwall` in `Mathlib.Analysis.ODE.DiscreteGronwall` provides related discrete error-bound infrastructure. |
addedDifferential inclusion3f8f2fccea4d
addedA-stability3938291f0c67