TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

C¹ dependence of an autonomous flow on the initial condition, and the variational equation

Statement

Let $n \geq 1$ , let $U \subseteq R^{n}$ be open, let $F : U \to R^{n}$ be of class $C^{1}$ ( $C^{k}$ Euclidean maps and diffeomorphisms), let $a_{0} \in U$ , and let $T > 0$ , $R > 0$ with $\overline{B} (a_{0}, R) \subseteq U$ (Open ball, closed ball and sphere in a metric space). Put $M : = \sup_{\overline{B} (a_{0}, R)} ∥ F ∥_{2}$ and $L : = \sup_{\overline{B} (a_{0}, R)} ∥ D F ∥$ , where $D F (x)$ is the total derivative of $F$ at $x$ with its operator norm (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, The operator norm as the least bound and as the unit-sphere or unit-ball supremum); both are finite. Let $0 < ρ < R - M T$ , so that in particular $M T < R$ . Let $Φ$ be the local flow of $x^{'} = F (x)$ (The local flow of an autonomous first-order system).

Then:

For every $a \in \overline{B} (a_{0}, ρ)$ the maximal solution $x (\cdot; a)$ is defined on $[0, T]$ and satisfies $∥ x (t; a) - a_{0} ∥_{2} \leq ρ + M t < R$ for $t \in [0, T]$ ; moreover

$∥ x (t; a) - x (t; b) ∥_{2} \leq e^{L t} ∥ a - b ∥_{2} (a, b \in \overline{B} (a_{0}, ρ), t \in [0, T]),$

and $(t, a) \mapsto x (t; a)$ is continuous on the compact set $[0, T] \times \overline{B} (a_{0}, ρ)$ .

For every $a \in B (a_{0}, ρ)$ the variational equation along $x (\cdot; a)$ ,

$Y^{'} (t) = D F (x (t; a)) Y (t), Y (0) = I_{n},$

has a unique solution $Y_{a} : [0, T] \to M_{n} (R)$ (The variational equation along an ODE solution), and for every $t \in [0, T]$ the map $a \mapsto x (t; a)$ is differentiable on the open ball $B (a_{0}, ρ)$ , with

$D_{a} x (t; a) h = Y_{a} (t) h (h \in R^{n}) .$

The map $(t, a) \mapsto Y_{a} (t)$ is continuous on $[0, T] \times B (a_{0}, ρ)$ , and consequently $(t, a) \mapsto x (t; a)$ is $C^{1}$ there with

$\partial_{t} x (t; a) = F (x (t; a)), D_{a} x (t; a) = Y_{a} (t) .$

Facts & Assumptions

Given: The open set $U$ , the $C^{1}$ field $F$ , the point $a_{0} \in U$ , the numbers $T, R > 0$ with $\overline{B} (a_{0}, R) \subseteq U$ , the finite constants $M, L$ , and $0 < ρ < R - M T$ .

[F10]

Matrix and norm convention (The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation, A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum): a matrix $A \in M_{n} (R)$ acts on Euclidean $R^{n}$ by $(A v)_{i} = \sum_{j < n} A_{i j} v_{j}$ , and every matrix norm in this item is the subordinate Euclidean norm $∥ A ∥_{o p} : = \sup_{∥ v ∥_{2} \leq 1} ∥ A v ∥_{2}$ ; the undecorated $∥ D F ∥$ in the Statement means this norm. Rowwise Cauchy-Schwarz gives $∥ A v ∥_{2} \leq (\sum_{i, j < n} A_{i j}^{2})^{1 / 2} ∥ v ∥_{2}$ , so the linear map is bounded and its operator norm is finite. Rescaling gives $∥ A v ∥_{2} \leq ∥ A ∥_{o p} ∥ v ∥_{2}$ ; the triangle inequality on vectors gives the triangle inequality on these operator norms. Matrix multiplication represents composition, hence $∥ A B ∥_{o p} \leq ∥ A ∥_{o p} ∥ B ∥_{o p}$ , and $∥ I_{n} ∥_{o p} = 1$ since $n \geq 1$ . Moreover $∣ ∥ A ∥_{o p} - ∥ B ∥_{o p} ∣ \leq ∥ A - B ∥_{o p} \leq (\sum_{i, j < n} (A_{i j} - B_{i j})^{2})^{1 / 2}$ , so entrywise continuity implies continuity in this norm. For a continuous matrix curve $C$ on $[r, s]$ , its integral is entrywise; applying the vector integral estimate to $C (t) v$ for each $∥ v ∥_{2} \leq 1$ and taking the supremum gives $∥ \int_{r}^{s} C (t) d t ∥_{o p} \leq \int_{r}^{s} ∥ C (t) ∥_{o p} d t$ when $r \leq s$ (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable).

[F1]

$F$ is continuous (differentiability implies continuity) and locally Lipschitz in the state variable: on the compact convex cylinder $[0, T] \times \overline{B} (a_{0}, R)$ the derivative bound $L$ gives $∥ F (x) - F (y) ∥_{2} \leq L ∥ x - y ∥_{2}$ , since $F$ is $C^{1}$ and the segment between two points of the ball lies in the ball; and $∥ F ∥ \leq M$ there. The same segment argument on a closed ball contained in $U$ about any point proves the local Lipschitz hypothesis throughout $U$ . Also $\overline{B} (a_{0}, R)$ is compact, and [F10] makes $∥ D F ∥_{o p}$ continuous, so both suprema are attained and finite (Local Lipschitz continuity in the state variable, locally uniform in time and parameters, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $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).

[F2]

Picard-Lindelöf and maximal solutions: local solutions exist uniquely through every initial point, and every initial value problem has a unique maximal solution, of which every other solution through the same data is a restriction (Picard-Lindelöf local existence and uniqueness for first-order systems, Every Picard–Lindelöf initial value problem has one maximal solution on an open interval, Extensions, maximal solutions, maximal intervals, and global solutions, The local flow of an autonomous first-order system).

[F3]

Compact continuation: a solution of $x^{'} = F (x)$ whose graph approaches a compact subset of $R \times U$ at a finite endpoint extends past that endpoint; in the autonomous case it suffices that the solution values stay in a compact subset of $U$ near the endpoint (Compact continuation for locally Lipschitz ODEs: a solution whose graph stays in a compact subset of the domain near a finite endpoint extends past it).

[F4]

Solutions are equivalent to solutions of the Volterra equation $x (t) = a + \int_{0}^{t} F (x (r)) d r$ , and the integral is additive over subintervals (A first-order initial value problem is equivalent to its Volterra integral equation, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[F5]

Norm and integral estimates: $∥ \int_{r}^{s} g ∥_{2} \leq ∣ \int_{r}^{s} ∥ g ∥_{2} ∣$ , and if $∥ g ∥_{2} \leq c$ on an interval then the norm of the integral is at most $c$ times the length; the Euclidean norm satisfies the triangle inequality, and for $u \neq 0$ the supremum $\sup_{∥ v ∥_{2} = 1} ∣ ⟨ u, v ⟩_{2} ∣$ equals $∥ u ∥_{2}$ (the value $v = u / ∥ u ∥_{2}$ gives $∥ u ∥_{2}$ , and Cauchy-Schwarz bounds every value by $∥ u ∥_{2}$ ) (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable, If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F6]

Gronwall: if continuous $u : [0, T] \to R$ , $u \geq 0$ , satisfies $u (t) \leq a (t) + \int_{0}^{t} L u$ with $L \geq 0$ and nondecreasing continuous $a \geq 0$ , then $u (t) \leq a (t) e^{L t}$ ; with a constant $A$ this reads $u (t) \leq A e^{L t}$ (Gronwall's integral inequality with variable and constant coefficients).

[F7]

$F$ is $C^{1}$ , so for $x, y$ with the segment $[x, y] \subseteq U$ one has $F (y) - F (x) = \int_{0}^{1} D F (x + τ (y - x)) (y - x) d τ$ , by the chain rule for $τ \mapsto F (x + τ (y - x))$ and the fundamental theorem; on the compact ball this gives the uniform remainder bound $∥ F (y) - F (x) - D F (x) (y - x) ∥_{2} \leq ω (∥ y - x ∥_{2}) ∥ y - x ∥_{2}$ , where $ω (s) : = \sup {∥ D F (u) - D F (w) ∥ : u, w \in \overline{B} (a_{0}, R), ∥ u - w ∥_{2} \leq s}$ and $ω (s) \to 0$ as $s ↓ 0$ by [F10] and Heine-Cantor uniform continuity of $D F$ on the compact ball (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[F8]

The linear matrix initial value problem $Y^{'} = C (t) Y$ , $Y (0) = I_{n}$ , with $C : [0, T] \to M_{n} (R)$ continuous, has a unique solution on all of $[0, T]$ (Linear matrix ODEs have unique global solutions on a fixed interval).

[F9]

If the partial derivatives of a map exist on a neighbourhood of a point and are continuous there, the map is totally differentiable at that point (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

Proof

technique · direct; first trap the solutions in a compact ball and extend them by continuation, then estimate differences with Gronwall, then compare solutions with the variational equation

1.1givenF1F2F4F5choosealgebra

Fix $a \in \overline{B} (a_{0}, ρ)$ and let $x = x (\cdot; a) : [0, β) \to U$ be the maximal forward solution, with $β \leq \infty$ . Choose a fixed radius $r$ with $ρ + M T < r < R$ . The curve cannot reach the sphere of radius $r$ about $a_{0}$ at a time $t_{*} < β$ with $t_{*} \leq T$ : at the first such time it has stayed in $\overline{B} (a_{0}, r) \subseteq \overline{B} (a_{0}, R)$ , so [F4] and [F5] give $∥ x (t_{*}) - a_{0} ∥_{2} \leq ρ + M t_{*} \leq ρ + M T < r$ , a contradiction. Thus for every $0 \leq t < β$ with $t \leq T$ the whole curve on $[0, t]$ stays in this fixed ball, and the same integral estimate gives $∥ x (t) - a_{0} ∥_{2} \leq ρ + M t < R$ .

2.1step 1.1F3

Consequently, if $β \leq T$ the graph of $x$ stays in the compact set $[0, T] \times \overline{B} (a_{0}, ρ + M T) \subseteq R \times U$ ; by [F3] $x$ extends past $β$ , contradicting maximality of the maximal solution (Extensions, maximal solutions, maximal intervals, and global solutions). Hence $β > T$ , so $x (\cdot; a)$ is defined on $[0, T]$ , and step 1.1 gives $∥ x (t; a) - a_{0} ∥_{2} \leq ρ + M t \leq ρ + M T < R$ there.

3.1step 1.12.1F1F4F5F6algebra

For $a, b \in \overline{B} (a_{0}, ρ)$ put $e (t) : = x (t; a) - x (t; b)$ . By [F4] and [F5], $∥ e (t) ∥_{2} \leq ∥ a - b ∥_{2} + L \int_{0}^{t} ∥ e (r) ∥_{2} d r$ for $t \in [0, T]$ , because both graphs lie in $\overline{B} (a_{0}, R)$ by step 2.1 and $∥ F (x) - F (y) ∥ \leq L ∥ x - y ∥$ there. By [F6] with $A = ∥ a - b ∥_{2}$ , $∥ e (t) ∥_{2} \leq e^{L t} ∥ a - b ∥_{2}$ . Adding the uniform bound $∥ x (t; a) - x (s; a) ∥_{2} \leq M ∣ t - s ∣$ obtained from [F4] and [F5] gives continuity of $(t, a) \mapsto x (t; a)$ on $[0, T] \times \overline{B} (a_{0}, ρ)$ . This is clause 1.

4.1step 3.1F7F8algebra

Fix $a \in B (a_{0}, ρ)$ and let $Y_{a}$ be the unique solution of the variational equation on $[0, T]$ , which exists by [F8] since $t \mapsto D F (x (t; a))$ is continuous (composition of the continuous map $D F$ with the continuous curve $x (\cdot; a)$ ). For $h \in R^{n}$ with $a + h \in \overline{B} (a_{0}, ρ)$ put $e_{h} : = x (\cdot; a + h) - x (\cdot; a)$ and $R_{h} (t) : = F (x (t; a + h)) - F (x (t; a)) - D F (x (t; a)) e_{h} (t) .$ By [F7] applied to the pair $(x (t; a + h), x (t; a))$ , whose segment lies in $\overline{B} (a_{0}, R)$ by convexity, $∥ R_{h} (t) ∥_{2} \leq ω (∥ e_{h} (t) ∥_{2}) ∥ e_{h} (t) ∥_{2}$ , and by step 3.1 $∥ e_{h} (t) ∥_{2} \leq e^{L T} ∥ h ∥_{2}$ .

4.2step 3.1F4F5F6F7F10algebra

The map $(t, a) \mapsto Y_{a} (t)$ is continuous on $[0, T] \times B (a_{0}, ρ)$ . First, $∥ Y_{a} (t) ∥_{o p} \leq e^{L t} \leq e^{L T}$ by the entrywise Volterra equation, the matrix integral and product estimates of [F10], $∥ I_{n} ∥_{o p} = 1$ and [F6]. Second, for $a, b$ the difference $Δ : = Y_{a} - Y_{b}$ satisfies $Δ^{'} = D F (x (t; a)) Δ + (D F (x (t; a)) - D F (x (t; b))) Y_{b}$ with $Δ (0) = 0$ , so [F4], [F5], [F6] and [F10] with $∥ Y_{b} ∥_{o p} \leq e^{L T}$ give $∥ Δ (t) ∥_{o p} \leq e^{L T} \cdot T \cdot \sup_{r \in [0, T]} ∥ D F (x (r; a)) - D F (x (r; b)) ∥_{o p} \cdot e^{L T},$ which tends to $0$ as $b \to a$ because $x (r; b) \to x (r; a)$ uniformly in $r$ by step 3.1 and $∥ D F (u) - D F (w) ∥ \leq ω (∥ u - w ∥_{2})$ with $ω (s) \to 0$ . Finally, $∥ Y_{a} (t) - Y_{a} (s) ∥_{o p} \leq L e^{L T} ∣ t - s ∣$ by $Y_{a} (t) - Y_{a} (s) = \int_{s}^{t} D F (x (r; a)) Y_{a} (r) d r$ and [F10]. Combining these three estimates proves continuity.

5.1step 4.1F4F5F6F7algebra

Define $δ_{h} (t) : = e_{h} (t) - Y_{a} (t) h$ . Differentiating and using the definitions of $e_{h}$ , $R_{h}$ and $Y_{a}$ gives $δ_{h}^{'} (t) = D F (x (t; a)) δ_{h} (t) + R_{h} (t)$ with $δ_{h} (0) = 0$ ; hence, by [F4] applied to the curve $δ_{h}$ and [F5], $∥ δ_{h} (t) ∥_{2} \leq \int_{0}^{t} ∥ R_{h} (r) ∥_{2} d r + L \int_{0}^{t} ∥ δ_{h} (r) ∥_{2} d r .$ Since $r \mapsto \int_{0}^{r} ∥ R_{h} ∥_{2}$ is nondecreasing, [F6] gives $∥ δ_{h} (t) ∥_{2} \leq e^{L t} \int_{0}^{t} ∥ R_{h} (r) ∥_{2} d r \leq e^{2 L T} T ω (e^{L T} ∥ h ∥_{2}) ∥ h ∥_{2}$ for $∥ h ∥_{2} \leq e^{- L T}$ ; dividing by $∥ h ∥_{2}$ and letting $h \to 0$ yields $∥ x (t; a + h) - x (t; a) - Y_{a} (t) h ∥_{2} / ∥ h ∥_{2} \to 0$ uniformly in $t \in [0, T]$ . Hence $a \mapsto x (t; a)$ is differentiable on $B (a_{0}, ρ)$ with $D_{a} x (t; a) h = Y_{a} (t) h$ for every $t$ . This is clause 2.

6.1step 1.13.14.25.1F2F8F9choose∎

Choose $ϵ > 0$ so small that $ρ + M (T + ϵ) < R$ (if $M = 0$ , any sufficiently small positive $ϵ$ works). Steps 1.1-5.1, which did not use [F9], apply with $T + ϵ$ in place of $T$ and show that the positive-time flow has continuous state derivative on $[0, T + ϵ] \times B (a_{0}, ρ)$ . Apply those same steps to the $C^{1}$ field $- F$ for time length $ϵ$ , with the same ball and bounds $M, L$ . Its solution $Ψ (s, a)$ gives $Φ (t, a) = Ψ (- t, a)$ for $- ϵ \leq t \leq 0$ : time reversal solves the original equation and agrees with its maximal solution by [F2]. Hence the state derivative exists and is continuous also on this negative-time slab; at $t = 0$ both state derivatives are $I_{n}$ , and their joint continuity on the two slabs makes the state derivative continuous across $0$ . The time derivative exists throughout the open set $(- ϵ, T + ϵ) \times B (a_{0}, ρ)$ and equals $F (Φ (t, a))$ , including at $0$ because the maximal solution solves the equation on its open interval. Joint continuity follows from step 3.1 on each slab and their common value $Φ (0, a) = a$ . Thus all partial derivatives are continuous on this open set, and [F9] makes the flow $C^{1}$ there. Its restriction proves clause 3 on $[0, T] \times B (a_{0}, ρ)$ , with $D_{a} Φ (t, a) = Y_{a} (t)$ by step 5.1; the variational solution on the longer interval restricts to $Y_{a}$ by uniqueness [F8].

Remarks

The hypothesis $ρ + M T < R$ is a genuine trapping condition: it keeps the whole graph of every considered solution in a compact subset of the domain, which is what lets Compact continuation for locally Lipschitz ODEs: a solution whose graph stays in a compact subset of the domain near a finite endpoint extends past it extend the maximal solution to the full interval $[0, T]$ . The conclusion is local in the initial condition and in time, and no claim is made that $D_{a} x (t; a)$ is defined at the boundary of the ball or for $t$ outside $[0, T]$ .
The proof actually shows more than stated: $∥ x (t; a + h) - x (t; a) - Y_{a} (t) h ∥_{2} \leq e^{2 L T} T ω (e^{L T} ∥ h ∥_{2}) ∥ h ∥_{2}$ , an explicit first-order error bound. The nonautonomous analogue (with $F = F (t, x)$ and the variational equation along a solution on a compact interval) is the same computation with the time variable kept, and is not needed in this batch.

C¹ dependence of an autonomous flow on the initial condition, and the variational equation

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources