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.

Finite-time linearization error bound: quadratic remainder, exponential growth bound and the variation-of-constants estimate

Statement

Let $n \geq 1$ , let $U \subseteq R^{n}$ be open with $0 \in U$ , let $F : U \to R^{n}$ be continuous and locally Lipschitz in the state variable, and let $r > 0$ , $C \geq 0$ , $L \geq 0$ and $A \in M_{n} (R)$ satisfy $\overline{B} (0, r) \subseteq U$ (Open ball, closed ball and sphere in a metric space) and

$∥ F (z) - A z ∥_{2} \leq C ∥ z ∥_{2}^{2}, ∥ F (z) ∥_{2} \leq L ∥ z ∥_{2} (∥ z ∥_{2} \leq r),$ where $A z$ and $∥ A ∥$ use the matrix-action and induced Euclidean operator-norm convention of Variation of constants for $z^{'} = A z + b (t)$ via the matrix exponential.

Let $z_{0} \in R^{n}$ with $δ : = ∥ z_{0} ∥_{2} > 0$ , let $T > 0$ with $δ e^{L T} < r$ , and let $y : R \to R^{n}$ be the solution of the linear system $y^{'} = A y$ , $y (0) = z_{0}$ (Variation of constants for $z^{'} = A z + b (t)$ via the matrix exponential). Then:

The maximal solution $z$ of $z^{'} = F (z)$ , $z (0) = z_{0}$ is defined on $[0, T]$ and satisfies $∥ z (t) ∥_{2} \leq δ e^{L t}$ for $t \in [0, T]$ (Extensions, maximal solutions, maximal intervals, and global solutions).
For every $t \in [0, T]$ , $∥ z (t) - y (t) ∥_{2} \leq C δ^{2} \int_{0}^{t} e^{∥ A ∥ (t - s)} e^{2 L s} d s \leq C δ^{2} t e^{(∥ A ∥ + 2 L) t},$ where $∥ A ∥$ is the operator norm of $A$ for the Euclidean norm (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

Remarks

Where the quadratic remainder comes from. If $D F$ is Lipschitz on $\overline{B} (0, r)$ with constant $Λ$ — equivalently, by the mean value inequality, if $∥ D F (u) - D F (v) ∥ \leq Λ ∥ u - v ∥_{2}$ there — then for $F (0) = 0$ and $A = D F (0)$ the identity $F (z) - A z = \int_{0}^{1} (D F (t z) - D F (0)) z d t$ (fundamental theorem for the vector-valued curve $t \mapsto F (t z)$ , If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz) gives $∥ F (z) - A z ∥_{2} \leq \frac{Λ}{2} ∥ z ∥_{2}^{2}$ , so the hypothesis holds with $C = Λ / 2$ (The mean value inequality: if $f : [a, b] \to R^{m}$ is continuous and differentiable on $(a, b)$ with $∥ f^{'} ∥_{2} \leq M$ , then $∥ f (b) - f (a) ∥_{2} \leq M (b - a)$ , Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction). For $C^{2}$ fields with $∥ D^{2} F ∥ \leq Λ$ on the ball this is the case.
Scope. The bound is a finite-time statement on $[0, T]$ under the explicit smallness condition $δ e^{L T} < r$ ; it asserts neither global validity of the linear approximation nor stability of the equilibrium, and it does not identify the nonlinear solution with the linear one beyond the displayed order- $δ^{2}$ estimate.

Facts & Assumptions

Given: The field $F$ and constants $A, r, C, L$ as in the statement, the datum $z_{0}$ with $δ = ∥ z_{0} ∥_{2} > 0$ , the time $T > 0$ with $δ e^{L T} < r$ , and the linear solution $y (t) = E (t) z_{0}$ with $E (t)$ the matrix exponential of $A$ .

[F1]

$F$ is continuous and locally Lipschitz in the state variable (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction for the Lipschitz terminology); on the compact ball $\overline{B} (0, r)$ the field $F$ is bounded by $L r$ and Lipschitz with some finite constant (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, Open ball, closed ball and sphere in a metric space). [given]

[F2]

Local existence on a Picard-Lindelof cylinder and the a priori Lipschitz estimate are provided by Continuous and Lipschitz dependence on the initial condition on a Picard-Lindelof cylinder; every initial value problem has a unique maximal solution, and any solution is a restriction of it (Every Picard–Lindelöf initial value problem has one maximal solution on an open interval, Extensions, maximal solutions, maximal intervals, and global solutions). [given]

[F3]

Compact continuation: a solution whose graph stays in a compact subset of $U$ near a finite endpoint extends past that 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). [given]

[F4]

A curve $z$ solves $z^{'} = F (z)$ through $z_{0}$ exactly when $z (t) = z_{0} + \int_{0}^{t} F (z (s)) d s$ for $t$ in its interval of definition, and moreover $∥ \int_{a}^{b} ϕ ∥_{2} \leq ∣ \int_{a}^{b} ∥ ϕ ∥_{2} ∣$ (A first-order initial value problem is equivalent to its Volterra integral equation, 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)$ , The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral). [given]

[F5]

Gronwall: if continuous $u \geq 0$ satisfies $u (t) \leq A_{0} + K \int_{0}^{t} u$ on $[0, T]$ , then $u (t) \leq A_{0} e^{K t}$ there (Gronwall's integral inequality with variable and constant coefficients). [given]

[F6]

Matrix exponential data (Variation of constants for $z^{'} = A z + b (t)$ via the matrix exponential, The operator norm as the least bound and as the unit-sphere or unit-ball supremum): $E$ is $C^{1}$ , $E^{'} (t) = A E (t) = E (t) A$ , $E (t) E (s) = E (t + s)$ , and $∥ E (u) ∥ \leq e^{∥ A ∥ ∣ u ∣}$ ; in particular $y (t) = E (t) z_{0}$ is the global solution of $y^{'} = A y$ , $y (0) = z_{0}$ , obtained by taking the globally continuous forcing $b \equiv 0$ .

Proof

technique · direct; bound the maximal solution by Gronwall while it stays in the ball, extend it to $[0,T]$ by compact continuation, and derive the finite-interval comparison identity with an integrating factor

1.1F1F4F5given

Let $z$ be the maximal solution through $z_{0}$ and let $J \subseteq [0, \infty)$ be that part of its interval on which $∥ z (t) ∥_{2} \leq r$ ; while $t \in J$ , [F4] and the bound $∥ F (z (s)) ∥_{2} \leq L ∥ z (s) ∥_{2}$ give $∥ z (t) ∥_{2} \leq δ + \int_{0}^{t} L ∥ z (s) ∥_{2} d s,$ so [F5] yields $∥ z (t) ∥_{2} \leq δ e^{L t}$ for all $t \in J$ . In particular, if $t \in J$ and $t \leq T$ then $∥ z (t) ∥_{2} \leq δ e^{L T} < r$ .

2.1step 1.1F2F3given

The maximal solution is defined on all of $[0, T]$ . Indeed, if its forward interval ended at some $τ \leq T$ , then the graph of $z$ on $[0, τ)$ would lie in the compact set $[0, T] \times \overline{B} (0, r)$ by step 1.1 applied on $J \cap [0, τ)$ — more precisely, should $z$ reach $∥ z ∥_{2} = r$ at some first time $τ_{0}$ , step 1.1 would give $∥ z (τ_{0}) ∥_{2} \leq δ e^{L τ_{0}} \leq δ e^{L T} < r$ at that time, a contradiction; so $∥ z (t) ∥_{2} < r$ for all $t$ in the maximal forward interval that are $\leq T$ , and the graph stays in the compact subset $[0, T] \times \overline{B} (0, r) \subseteq [0, T] \times U$ . By [F3] the solution extends past every finite endpoint below or at $T$ , so it is defined on $[0, T]$ and step 1.1 gives $∥ z (t) ∥_{2} \leq δ e^{L t}$ there; this is clause 1.

3.1step 2.1F6given

Finite-interval comparison identity: on $[0, T]$ put $q : = z - y$ and $b (t) : = F (z (t)) - A z (t)$ . The curve $b$ is continuous on $[0, T]$ , and $q^{'} = A q + b$ , $q (0) = 0$ . Define $r (t) : = E (- t) q (t)$ . By [F6], the chain rule and product rule, $r^{'} (t) = - A E (- t) q (t) + E (- t) (A q (t) + b (t)) = E (- t) b (t),$ since $A E (- t) = E (- t) A$ . The vector-valued fundamental theorem of calculus, applied on the actual interval $[0, T]$ , gives $r (t) = \int_{0}^{t} E (- s) b (s) d s$ ; multiplying by $E (t)$ and using [F6]'s group law yields $q (t) = \int_{0}^{t} E (t - s) b (s) d s .$ This derivation uses only the continuous values of $b$ on $[0, T]$ . Consequently, using $∥ E (t - s) ∥ \leq e^{∥ A ∥ (t - s)}$ for $0 \leq s \leq t$ , the quadratic remainder hypothesis and clause 1, $∥ z (t) - y (t) ∥_{2} \leq \int_{0}^{t} e^{∥ A ∥ (t - s)} ∥ F (z (s)) - A z (s) ∥_{2} d s \leq C δ^{2} \int_{0}^{t} e^{∥ A ∥ (t - s)} e^{2 L s} d s,$ for every $t \in [0, T]$ .

4.1step 3.1algebra∎

For the final estimate, $e^{∥ A ∥ (t - s)} \leq e^{∥ A ∥ t}$ and $e^{2 L s} \leq e^{2 L t}$ on $0 \leq s \leq t$ , so $\int_{0}^{t} e^{∥ A ∥ (t - s)} e^{2 L s} d s \leq t e^{(∥ A ∥ + 2 L) t}$ ; substituting into step 3.1 gives the displayed product bound. This proves clause 2.

Finite-time linearization error bound: quadratic remainder, exponential growth bound and the variation-of-constants estimate

Statement

Remarks

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources