Commit 2024-01-09 02:13 7649e802

feat: local existence of integral curves of vector field (#8483) Port of [mathlib#17140](https://github.com/leanprover-community/mathlib/pull/17140) plus much more. Comments therein addressed. For any continuously differentiable vector field (section of tangent bundle) on a manifold M and any chosen interior point x₀ : M, there exists an integral curve γ : ℝ → M such that γ t₀ = x₀ for any real number t₀ and the tangent vector of γ at t coincides with the vector field at γ t for all t within an open interval around t₀. As a corollary, such an integral curve exists for any starting point x₀ if M is a manifold without boundary. We define three Props:

1. IsIntegralCurveOn γ v s means γ t is tangent to v (γ t) for all t within s : Set ℝ.
2. IsIntegralCurveAt γ v t₀ means γ is a local integral curve to v. That is, γ t is tangent to v (γ t) for all t within some open interval of t₀.
3. IsIntegralCurve γ v means γ is a global integral curve to v. That is, γ t is tangent to v (γ t) for all t : ℝ. Lemmas about rescaling and translation of integral curves are proven:

• If γ solves v at t₀, then γ (t + dt) is tangent to v at t₀ - dt.
• If γ solves v at t₀, then γ (a * t) is tangent to a • v at t₀ / a for any non-zero a.
• The constant function at x₀ solves any v with v x₀ = 0. We also shuffle the position of ∃ ε > (0 : ℝ) in PicardLindelof to one that makes more sense, since f t₀ = x₀ does not depend on ε yet.