Commit 2024-01-23 11:19 4bde8367

View on Github →

feat: uniqueness of integral curves of a vector field on a manifold (#8886) We prove the uniqueness of integral curves of a vector field on a manifold using the uniqueness theorem for solutions to ODEs.

Estimated changes

Modified Mathlib/Algebra/Order/Ring/Abs.lean

added theorem exists_abs_lt

Modified Mathlib/Analysis/ODE/Gronwall.lean

modified 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

deleted theorem ODE_solution_unique_of_mem_set

modified theorem dist_le_of_approx_trajectories_ODE

added theorem dist_le_of_approx_trajectories_ODE_of_mem

deleted theorem dist_le_of_approx_trajectories_ODE_of_mem_set

modified theorem dist_le_of_trajectories_ODE

added theorem dist_le_of_trajectories_ODE_of_mem

deleted theorem dist_le_of_trajectories_ODE_of_mem_set

Modified Mathlib/Geometry/Manifold/IntegralCurve.lean

added theorem IsIntegralCurve.continuous

added theorem IsIntegralCurveAt.continuousAt

added theorem IsIntegralCurveAt.eventually_hasDerivAt

added theorem IsIntegralCurveOn.continuousAt

added theorem IsIntegralCurveOn.continuousOn

added theorem IsIntegralCurveOn.hasDerivAt

deleted theorem isIntegralCurvOn_comp_mul_ne_zero

added theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt

added theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless

added theorem isIntegralCurveOn_Ioo_eqOn_of_contMDiff

added theorem isIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless

added theorem isIntegralCurveOn_comp_mul_ne_zero

added theorem isIntegralCurve_Ioo_eq_of_contMDiff_boundaryless

added theorem isIntegralCurve_eq_of_contMDiff

Modified Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean

added theorem mfderiv_chartAt_eq_tangentCoordChange