Open MathsAll courses

Flow inverses and continuation on their actual domains

The following arguments are §§17.6–17.7 of the AN-03 programme reading Geometric and microlocal calculus. Its local flow and every parameter derivative, NF1–NF15, are supplied separately. The smooth inverse and implicit maps, §§16.4–16.5, supply the inverse construction used below. The finite algebra, §10, and scalar calculus, §§12–13, supply determinant differentiation, compactness, finite integration and the scalar exponential equation.

In the notation below is the finite-dimensional state space, the parameter space, and the smooth vector field on an actual open subset of . The local solution satisfies and its given initial value.

Programme proof: AN-03 course contributors, OpenAI Codex; CC0 1.0. Programme credits and rights notice accompany the text.

17.6. Variable initial times without replacing the original time coordinate

Use the proved solution with the fixed original . Write for it. Near , the actual finite map

is . At its state derivative is the original identity because , its state derivative in is zero, and its time derivative is . Its full derivative is block triangular with diagonal identities; its inverse keeps the lower state/time block . The proved finite inverse/implicit theorem therefore constructs its actual local inverse, with second component . The unchanged original-time solution is

It is jointly , solves the original differential equation in the original , and has the original datum at the original time . Uniqueness was proved in Section17.1. Both maps in NF17 are explicit; no translated time equation or changed vector field is substituted for NF1.

Let . Differentiating the already proved equation gives , . NF8 proves that it is invertible with the constructed opposite-order inverse. Differentiate the second identity of NF17 and then its first identity to obtain the full initial-time derivative

The last equality follows by differentiating NF17 in : . All original inverse factors and endpoint evaluations appear before the comparison. Higher initial-time derivatives are the full finite composition and inverse partition formulas applied to NF16--NF17; they keep the entire time/state/parameter blocks.

17.7. Continuation, the exact composition law and coordinate transport

At every point of a solution, the local construction above applies with that original point and its original time as datum. Its local continuations agree by uniqueness. The union of all continuation intervals is an interval: each contains the original datum time, so two such intervals overlap; their agreeing solutions glue. This gives the unique maximal solution on that interval. If two overlapping continuations are first described through different chains of local rectangles, the same uniqueness argument on the connected time overlap makes them equal. No choice of a chart or of a time subdivision changes the solution.

The full admissible domain of is open and the solution is jointly there. For an actual trajectory segment from to , its compact graph is covered by finitely many construction rectangles with smaller time intervals. Subdivide that original time segment finely enough that each successive piece lies in one such rectangle: a Lebesgue number follows from compactness by taking finitely many smaller neighborhoods whose closures remain in the covering neighborhoods, or by the elementary compact interval subdivision argument. Each local solution map is defined on an open neighborhood of its intermediate datum. Continuity of the finite preceding composition lets one shrink the original data neighborhood so that all intermediate data stay in these open neighborhoods. The finite composition then exists near the given endpoint and is , and uniqueness identifies it with the maximal solution. Slightly moving both endpoint times uses the first and last rectangles. This proves openness and full local regularity throughout the actual domain.

Whenever all displayed solutions are defined along their connected common intervals,

Both sides of the first identity solve NF1 with the same datum at ; uniqueness proves it, and the second is its endpoint case. For an autonomous field write . NF19 gives the local flow law , with their actual domains, and inverse . This is a local diffeomorphism, since both maps are the constructed smooth inverse maps on open sets. It is not an assertion that every field has a globally defined flow.

Under an original smooth coordinate diffeomorphism , retain the transformed field . The chain rule proves that solves its equation with datum . Applying uniqueness gives

This is the exact map between coordinate presentations. For a smooth vector field on the given manifold, these transformations glue local chart solutions and all their parameter derivatives. Their domains are open by the finite-chain proof. For a manifold with boundary, the same assertion in boundary charts needs an actual smooth extension of the coefficients to an open coordinate neighborhood; no extension theorem is hidden in NF20. The collar lesson's stated coefficient extension or an explicitly given extension supplies that separate condition.

The determinant of the original state variation has all of its factors:

Its derivative follows from the full cofactor determinant derivative and the two actual inverse products of NF8: for , . The trace equality is the finite sum . The scalar integrating-factor proof and the initial determinant one give NF21. The original determinant, oriented time integral and original trace are all retained. Positivity of this determinant is the local orientation statement; no state norm or coordinate volume has been silently changed.

If the original state dimension is zero, the unique state is its zero vector, is zero and the solution is constant. Every state inverse is the unique , every empty matrix determinant is one, and NF21 is . No positive state comparison constant or division by a zero operator norm is needed. A zero-dimensional parameter space has no parameter directions; its derivative terms in the original formulas are zero. If is empty there is no datum and no local assertion.