How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Smooth dependence of ODE solutions on parameters
Statement
Let be jointly in on an open time-state-parameter domain. Near any base data there are a compact time interval and a neighbourhood of such that, for every , the solution of
is defined on , and the resulting solution map is smooth in the pair .
Facts & Assumptions
Given: An open domain , a jointly smooth field , and . Put , , and .
For a smooth system on an established common compact local interval, its solutions depend smoothly on the initial state (Smooth dependence of solutions on initial data). We use this only for a jointly smooth field, so all derivatives entering its variational proof are jointly continuous.
A bounded total derivative on a convex open set gives a Lipschitz bound; closed bounded Euclidean cylinders are compact, and continuous norms on them are bounded (On a convex open set, a uniform bound implies , Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).
Picard–Lindelof gives existence and uniqueness on a cylinder with field bound , state-Lipschitz bound , and ; nearby initial states share one such time interval and compact graph cylinder (Picard-Lindelöf local existence and uniqueness for first-order systems, Nearby initial values share one Picard–Lindelöf time interval and one state cylinder).
A classical solution is equivalent to its Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).
On a common compact interval the initial-state derivative exists, is continuous in that state, and solves the variational equation; the proof's difference-quotient and derivative-continuity estimates are uniform in time ( dependence of solutions on initial data). With jointly continuous state derivatives, those estimates and the variational equation also give joint continuity in time and initial state.
A linear matrix ODE with continuous coefficients has a unique solution on its given compact interval (Linear matrix ODEs have unique global solutions on a fixed interval). An affine linear equation is included by adjoining a constant component ; finite-dimensional multilinear-map spaces are represented by their coordinate arrays.
Proof
The field is jointly smooth on the open time-state domain . Its last equations are , so the parameter is constant along each augmented solution. Thus projection to the first coordinates identifies augmented solutions through with solutions of the displayed original IVP, in both directions.
Choose so . By [F1], and have bounds and on this cylinder, and the mean-value inequality on each open state ball gives the same state-Lipschitz bound . Choose with , and . For every initial state , the radius- cylinder centred at lies in the larger cylinder. Hence [F2] gives a unique augmented solution on , all of whose graphs lie in that one compact cylinder. This establishes the common interval needed below.
Now [L1] applies to the jointly smooth field on the common interval of step 2.1, and gives smooth dependence of on near . We record why this dependence has the joint regularity needed for time derivatives. At first order, [F4] gives and , . The coefficient is jointly continuous; the uniform-in-time estimates in [F4], combined with continuity of the solution of this linear equation in time, make jointly continuous. The solution itself is jointly continuous by the same initial-data estimates and its continuity in time.
The higher-order argument does not require a new existence assumption. For , use the finite-dimensional jet variables , where is a -linear map and . Repeated chain rules in [F3] give and for , with . Here is the finite sum over partitions of the differentiation directions into at least two nonempty blocks, applying the corresponding higher derivative of to the lower jets indexed by those blocks. Initial values are , and for . This jet field is jointly smooth. For nearby full jet initial values, exists on by step 2.1; successively each higher component is affine linear with bounded continuous coefficients and forcing on , so [F5] gives its evolution there. The same linear integral estimates bound each component uniformly for nearby initial values, giving a common compact jet cylinder for each finite order. Thus [F4] legitimately applies to this enlarged system on . Starting with its first-order variational equation, differentiation of the Volterra identities and uniqueness in [F5] identify the prescribed jet with . Its highest component is in the initial state, so these identities upgrade to ; this uses the highest component, not merely the first one. Induction, with the uniform estimates of [F4], gives joint continuity of all state derivatives.
The equation now supplies all mixed derivatives: differentiating it in state variables gives the chain-rule expressions in the jointly continuous state jets, and their displayed jet equations permit subsequent time differentiation. Induction on the time order, using joint smoothness of , proves joint smoothness on the open time interval and the initial-state neighbourhood. Put ; the solution map on therefore extends smoothly to an open time neighbourhood. Projection as in step 1.1 gives the claimed common local solutions and smooth dependence on , including the endpoints of . All solutions and all jet evolutions are uniquely determined by their IVPs; the Picard sequences use prescribed iteration and the argument makes no family selection or additional Choice assumption.
Depends on
- Smooth dependence of solutions on initial data
- Picard-Lindelöf local existence and uniqueness for first-order systems
- Nearby initial values share one Picard–Lindelöf time interval and one state cylinder
- On a convex open set, a uniform bound $\|Df(z)v\|_2\le M\|v\|_2$ implies $\|f(y)-f(x)\|_2\le M\|y-x\|_2$
- A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
- $C^1$ dependence of solutions on initial data
- Linear matrix ODEs have unique global solutions on a fixed interval
- A first-order initial value problem is equivalent to its Volterra integral equation
Used by
- A nontrivial Whitney circle in the fundamental group blocks cancellation Counterexample
- Smooth dependence in an ODE with a parameter Example
- A compact holonomy-free codimension-one foliation is fibered over its leaf space Lemma
- A normal summand of rank at least two realizes every framing-loop obstruction Lemma
- Embedded bands joining two framed spheres exist Lemma
- Frame fields with prescribed boundary conditions along a clean Whitney disk Lemma
- Local solvability and C1 parameter dependence for the augmented characteristic ODE Lemma
- Opposite local signs give the compatible Whitney-circle framing Lemma
- Real Stiefel spaces with complement rank at least two are simply connected Lemma
- The basepoint evaluation of the Stiefel section space is a fibration Lemma
- The surgery gluing has a canonical smooth structure up to diffeomorphism Lemma
- Flat connections have locally path-independent parallel transport on a coordinate ball Proposition
- A flat connection admits local parallel frames Theorem
- Stable normal bundle is independent of the embedding Theorem
- The double has a well-defined smooth structure Theorem
- The fundamental theorem for nonautonomous smooth ODEs Theorem
- The Whitney trick in the codimension-two borderline case Theorem
Dependency tree · two levels
68 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Nigel Hitchin, Differentiable Manifolds, Appendix §10.3, Theorem 10.7 (standard reference, not scraped)
- Chin-Lung Wang, Banach Calculus, §§4.2–4.4 (standard reference, not scraped)