Revision #3147 → #4104 · back to history
modifiedGlobal solution39e161c77438
| Field | From #3147 | To #4104 |
|---|
| note | `IsIntegralCurve γ v` is precisely an integral curve defined on all of ℝ, matching the notion of a global solution. | `IsIntegralCurve γ v` is precisely an integral curve defined on all of ℝ, matching the notion of a global solution. Status upgraded from partial to formalized to align with the exact match_kind. |
| provenance | ai | ai-moderated |
| status | partial | formalized |
modifiedFinite duration solution example9656b5998754
| Field | From #3147 | To #4104 |
|---|
| anchor.snippet | Admits the finite duration solution | admits the finite duration solution |
| note | This explicit finite-duration example is not formalized in Mathlib. | This explicit finite-duration example is not formalized in Mathlib. Snippet corrected to match article capitalization. |
| provenance | ai | ai-moderated |
modifiedPicard–Lindelöf theorem350f79d68068
| Field | From #3147 | To #4104 |
|---|
| mathlib.module | Mathlib.Analysis.ODE.PicardLindelof | Mathlib.Analysis.ODE.ExistUnique |
| note | The Picard–Lindelöf (Cauchy–Lipschitz) theorem is proved in `IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt`. | The Picard–Lindelöf (Cauchy–Lipschitz) theorem is proved in `IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt` (verified module is `Mathlib.Analysis.ODE.ExistUnique`). |
addedGrönwall's inequality (application to ODEs)b718f36986d1
modifiedLocal existence and uniqueness theorem493fce98cda0
| Field | From #3147 | To #4104 |
|---|
| mathlib.module | Mathlib.Analysis.ODE.PicardLindelof | Mathlib.Analysis.ODE.ExistUnique |
| note | Local existence is given by `IsPicardLindelof.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`. |
modifiedGlobal uniqueness and maximum domainb153af2abce8
| Field | From #3147 | To #4104 |
|---|
| mathlib.module | Mathlib.Analysis.ODE.Gronwall | Mathlib.Analysis.ODE.ExistUnique |
| note | Global uniqueness for Lipschitz vector fields is given by `ODE_solution_unique_univ`, but the existence of a maximal interval of definition is not formalized. | Global uniqueness for Lipschitz vector fields is given by `ODE_solution_unique_univ` (verified module is `Mathlib.Analysis.ODE.ExistUnique`), but the existence of a maximal interval of definition is not formalized. |