Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generated
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 F(t,x,λ) be jointly C∞ in (t,x,λ) on an open time-state-parameter domain. Near any base data (t0,x0,λ0) there are a compact time interval I and a neighbourhood W of (x0,λ0) such that, for every (y,λ)∈W, the solution of

x′(t)=F(t,x(t),λ),x(t0)=y,

is defined on I, and the resulting solution map is smooth in the pair (y,λ).

Facts & Assumptions

Given: An open domain D⊆R×Rn×Rm, a jointly smooth field F:D→Rn, and (t0,x0,λ0)∈D. Put d=n+m, z=(x,λ), z0=(x0,λ0) and G(t,z)=(F(t,x,λ),0)∈Rd.

[L1]

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.

[F2]

Picard–Lindelof gives existence and uniqueness on a cylinder with field bound M, state-Lipschitz bound L, hM≤r and Lh<1; 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).

[F3]

A classical solution is equivalent to its Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).

[F4]

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 (C1 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.

[F5]

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 1; finite-dimensional multilinear-map spaces are represented by their coordinate arrays.

Proof

technique · direct
1.1givenconstructF3

The field G is jointly smooth on the open time-state domain D. Its last m equations are λ′=0, so the parameter is constant along each augmented solution. Thus projection to the first n coordinates identifies augmented solutions through (y,λ) with solutions of the displayed original IVP, in both directions.

2.1F1F2step 1.1choose

Choose a,r>0 so [t0−a,t0+a]×B‾(z0,2r)⊆D. By [F1], G and DzG have bounds M≥1 and L≥1 on this cylinder, and the mean-value inequality on each open state ball gives the same state-Lipschitz bound L. Choose H>0 with H<a, HM<r and HL<1. For every initial state z∈B(z0,r), the radius-r cylinder centred at z lies in the larger cylinder. Hence [F2] gives a unique augmented solution Z(t,z) on J=[t0−H,t0+H], all of whose graphs lie in that one compact cylinder. This establishes the common interval needed below.

3.1L1F4F5step 2.1

Now [L1] applies to the jointly smooth field G on the common interval J of step 2.1, and gives smooth dependence of Z(t,z) on z near z0. We record why this dependence has the joint regularity needed for time derivatives. At first order, [F4] gives X1=DzZ and X1′=DzG(t,Z)X1, X1(t0)=Id. 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 X1 jointly continuous. The solution Z itself is jointly continuous by the same initial-data estimates and its continuity in time.

4.1F3F4F5step 2.1step 3.1algebra

The higher-order argument does not require a new existence assumption. For r≥1, use the finite-dimensional jet variables X0,…,Xr, where Xj is a j-linear map and X0∈Rd. Repeated chain rules in [F3] give X0′=G(t,X0) and Xj′=DzG(t,X0)Xj+Pj(t,X0,…,Xj−1) for j≥1, with P1=0. Here Pj is the finite sum over partitions of the j differentiation directions into at least two nonempty blocks, applying the corresponding higher derivative of G to the lower jets indexed by those blocks. Initial values are X0(t0)=z, X1(t0)=Id and Xj(t0)=0 for j≥2. This jet field is jointly smooth. For nearby full jet initial values, X0 exists on J by step 2.1; successively each higher component is affine linear with bounded continuous coefficients and forcing on J, 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 J. Starting with its first-order variational equation, differentiation of the Volterra identities and uniqueness in [F5] identify the prescribed jet with (Z,DzZ,…,DzrZ). Its highest component is C1 in the initial state, so these identities upgrade Cr to Cr+1; this uses the highest component, not merely the first one. Induction, with the uniform estimates of [F4], gives joint continuity of all state derivatives.

5.1givenstep 1.1step 2.1step 3.1step 4.1∎

The equation ∂tZ=G(t,Z) 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 G, proves joint smoothness on the open time interval (t0−H,t0+H) and the initial-state neighbourhood. Put I=[t0−H/2,t0+H/2]; the solution map on I therefore extends smoothly to an open time neighbourhood. Projection as in step 1.1 gives the claimed common local solutions and smooth dependence on (y,λ), including the endpoints of I. 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

Used by

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