Commit 2026-03-20 20:42 ec6dab02

View on Github →

feat: IsIntegralCurve for solutions to ODEs (#29186) I define IsIntegralCurve etc. for solutions to ODEs on vector spaces. The translation and scaling lemmas are also included. This parallels IsMIntegralCurve etc. for manifolds. Moved from #26534.

depends on: #26563

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/ODE/Basic.lean

added theorem IsIntegralCurve.continuous

added theorem IsIntegralCurve.isIntegralCurveAt

added theorem IsIntegralCurve.isIntegralCurveOn

added def IsIntegralCurve

added theorem IsIntegralCurveAt.continuousAt

added theorem IsIntegralCurveAt.hasDerivAt

added theorem IsIntegralCurveAt.isIntegralCurveOn

added def IsIntegralCurveAt

added theorem IsIntegralCurveOn.continuousOn

added theorem IsIntegralCurveOn.continuousWithinAt

added theorem IsIntegralCurveOn.isIntegralCurveAt

added theorem IsIntegralCurveOn.mono

added def IsIntegralCurveOn

added theorem isIntegralCurveAt_iff_exists_mem_nhds

added theorem isIntegralCurveAt_iff_exists_pos

added theorem isIntegralCurveOn_iff_isIntegralCurveAt

added theorem isIntegralCurveOn_univ

added theorem isIntegralCurve_iff_isIntegralCurveAt

Created Mathlib/Analysis/ODE/Transform.lean

added theorem IsIntegralCurve.comp_add

added theorem IsIntegralCurve.comp_mul

added theorem IsIntegralCurve.comp_sub

added theorem IsIntegralCurveAt.comp_add

added theorem IsIntegralCurveAt.comp_mul_ne_zero

added theorem IsIntegralCurveAt.comp_sub

added theorem IsIntegralCurveOn.comp_add

added theorem IsIntegralCurveOn.comp_mul

added theorem IsIntegralCurveOn.comp_sub

added theorem isIntegralCurveAt_comp_add

added theorem isIntegralCurveAt_comp_mul_ne_zero

added theorem isIntegralCurveAt_comp_sub

added theorem isIntegralCurveOn_comp_add

added theorem isIntegralCurveOn_comp_mul_ne_zero

added theorem isIntegralCurveOn_comp_sub

added theorem isIntegralCurve_comp_add

added theorem isIntegralCurve_comp_mul_ne_zero

added theorem isIntegralCurve_comp_sub

added theorem isIntegralCurve_const

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

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