CorollaryStatement: 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.

Variation of constants for $z^{'} = A z + b (t)$ via the matrix exponential

Statement

Let $n \geq 1$ , equip $R^{n}$ with the Euclidean inner product and norm of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , let $A \in M_{n} (R)$ (The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations), let $t_{0} \in R$ and $z_{0} \in R^{n}$ , and let $b : R \to R^{n}$ be continuous (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral). The Euclidean norm is a norm by Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation, and the standard coordinate vectors form an ordered basis by The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ . For $A = (a_{i j})$ and $z \in R^{n}$ , define $(A z)_{i} : = \sum_{j < n} a_{i j} z_{j}$ ; this is a linear map by Linear map between vector spaces over the same field, hence bounded by A linear map from a finite-dimensional normed space is bounded, and $∥ A ∥$ denotes its induced Euclidean operator norm (The operator norm as the least bound and as the unit-sphere or unit-ball supremum). Matrix powers and products use Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes; their action agrees with composition of the corresponding linear maps by distributing the finite sums in the displayed coordinate formula. Define the matrix exponential

$E : R ⟶ M_{n} (R), E (t) : = \sum_{k = 0}^{\infty} \frac{t^{k}}{k!} A^{k} .$

Then:

$E$ is well defined and of class $C^{1}$ , with $E (0) = I_{n}$ , $E (u + v) = E (u) E (v)$ , $\frac{d}{d u} E (u) = A E (u) = E (u) A$ for all $u, v \in R$ , and $∥ E (u) ∥ \leq e^{∥ A ∥ ∣ u ∣}$ for the operator norm (The operator norm as the least bound and as the unit-sphere or unit-ball supremum) subordinate to the Euclidean norm.
The map $z : R ⟶ R^{n}, z (t) : = E (t - t_{0}) z_{0} + \int_{t_{0}}^{t} E (t - s) b (s) d s,$ satisfies $z (t_{0}) = z_{0}$ and $z^{'} (t) = A z (t) + b (t)$ for every $t \in R$ .
Uniqueness: if $J \subseteq R$ is an interval with nonempty interior containing $t_{0}$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) and $w : J \to R^{n}$ is differentiable with $w^{'} = A w + b$ on $J$ and $w (t_{0}) = z_{0}$ , then $w = z ∣_{J}$ .

Facts & Assumptions

Given: $n \geq 1$ , $A \in M_{n} (R)$ identified with a linear endomorphism of $R^{n}$ , $z_{0} \in R^{n}$ , a continuous $b : R \to R^{n}$ , and the matrix exponential $E$ displayed above.

[F1]

The matrix action defined in the Statement is a bounded linear endomorphism $\hat{A}$ of normed Euclidean $R^{n}$ : the Euclidean norm is a norm, and the standard coordinate vectors form a finite ordered basis, so the finite-dimensional boundedness theorem applies (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, The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ , A linear map from a finite-dimensional normed space is bounded). Its induced metric agrees with $d_{2}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ), which is complete ( $R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ ); hence this normed space is Banach. For matrices $B = (b_{i j})$ and $C = (c_{j ℓ})$ , $((B C) z)_{i} = \sum_{ℓ < n} (\sum_{j < n} b_{i j} c_{j ℓ}) z_{ℓ} = (B (C z))_{i}$ , so matrix multiplication represents composition (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes). The exponential series lemma applies to $\hat{A}$ and gives absolute convergence in operator norm, $E \in C^{1}$ with $E^{'} = A E = E A$ , $E (0) = I_{n}$ , $E (u + v) = E (u) E (v)$ and $∥ E (u) ∥ \leq e^{∥ A ∥ ∣ u ∣}$ (The exponential series of a bounded operator).

[F2]

The convolution differentiation lemma (Differentiation of a variable-limit convolution integral with a C-one matrix kernel) applies with interval $I = R$ , open kernel domain $U = R \supseteq I - I$ , $g : = E : U \to M_{n} (R)$ and $f : = b : I \to R^{n}$ : for every $t$ , the map $t \mapsto \int_{t_{0}}^{t} E (t - s) b (s) d s$ is differentiable with derivative $E (0) b (t) + \int_{t_{0}}^{t} E^{'} (t - s) b (s) d s$ .

[F3]

Differentiation rules: the chain rule and the algebra of derivatives differentiate products and compositions; for a differentiable matrix curve $M$ and constant vector $v$ , $t \mapsto M (t) v$ is differentiable with derivative $M^{'} (t) v$ . [thm-chain-rule, thm-algebra-of-derivatives]

[F4]

Fundamental theorem for continuous derivatives: if $u : J \to R^{n}$ is differentiable with continuous derivative on an interval $J$ containing $t_{0}$ , then $\int_{t_{0}}^{t} u^{'} = u (t) - u (t_{0})$ (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); and $∥ \int_{t_{0}}^{t} ϕ ∥_{2} \leq ∣ \int_{t_{0}}^{t} ∥ ϕ ∥_{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, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[F5]

Gronwall: if a continuous real $u \geq 0$ satisfies $u (t) \leq A + \int_{t_{0}}^{t} B u$ for $t \geq t_{0}$ with constants $A, B \geq 0$ , then $u (t) \leq A e^{B (t - t_{0})}$ ; the time-reflected form with the integral from $t$ to $t_{0}$ applies for $t \leq t_{0}$ (Gronwall's integral inequality with variable and constant coefficients).

Proof

technique · direct; verify the explicit solution by the convolution lemma and the exponential identities, then prove uniqueness by Gronwall

1.1F1F3given

By [F1] the exponential $E$ is $C^{1}$ with $E^{'} = A E = E A$ , $E (0) = I_{n}$ , $E (u + v) = E (u) E (v)$ and $∥ E (u) ∥ \leq e^{∥ A ∥ ∣ u ∣}$ for all $u, v$ ; in particular $t \mapsto E (t - t_{0})$ is differentiable with derivative $A E (t - t_{0})$ , by the chain rule for the affine inner map $t \mapsto t - t_{0}$ .

2.1step 1.1F2F3given

By step 1.1 and [F3], $t \mapsto E (t - t_{0}) z_{0}$ has derivative $A E (t - t_{0}) z_{0}$ . By [F2] the integral term has derivative $E (0) b (t) + \int_{t_{0}}^{t} E^{'} (t - s) b (s) d s = b (t) + \int_{t_{0}}^{t} A E (t - s) b (s) d s$ , where the second identity uses $E^{'} = A E$ of step 1.1 and linearity of the integral. Hence $z^{'} (t) = A E (t - t_{0}) z_{0} + b (t) + A \int_{t_{0}}^{t} E (t - s) b (s) d s = A z (t) + b (t),$ by linearity of matrix-vector multiplication. Moreover $z (t_{0}) = E (0) z_{0} + \int_{t_{0}}^{t_{0}} = z_{0}$ , so clause 2 holds.

3.1step 2.1F4F5∎

For clause 3 let $w$ solve $w^{'} = A w + b$ on an interval $J$ containing $t_{0}$ with $w (t_{0}) = z_{0}$ , and put $u : = w - z ∣_{J}$ . By step 2.1, $u^{'} = A u$ and $u (t_{0}) = 0$ , so by [F4] $u (t) = \int_{t_{0}}^{t} A u (s) d s (t \in J),$ and therefore $∥ u (t) ∥_{2} \leq ∣ \int_{t_{0}}^{t} ∥ A ∥ ∥ u (s) ∥_{2} d s ∣ \leq ∥ A ∥ ∣ \int_{t_{0}}^{t} ∥ u (s) ∥_{2} d s ∣$ for $t \geq t_{0}$ and the reflected inequality for $t \leq t_{0}$ . Applying [F5] with $A_{0} = 0$ and $B = ∥ A ∥$ to the nonnegative continuous function $∥ u ∥_{2}$ gives $∥ u (t) ∥_{2} \leq 0$ on both sides of $t_{0}$ , hence $u = 0$ and $w = z ∣_{J}$ .

Variation of constants for $z^{'} = A z + b (t)$ via the matrix exponential

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Variation of constants for z′=Az+b(t)z′=Az+b(t) via the matrix exponential

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Variation of constants for $z^{'} = A z + b (t)$ via the matrix exponential