LemmaStatement: AI-adaptedProof: AI-adapted

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.

Linear matrix ODEs have unique global solutions on a fixed interval

Statement

Let $I = [a, b] \subseteq R$ be a nonempty compact interval, let $C : I \to M_{n} (R)$ be continuous, let $t_{0} \in I$ , and let $Y_{0} \in M_{n} (R)$ . For $n = 0$ , there is exactly one map $Y : I \to M_{0} (R)$ , namely the empty-matrix map, and all entrywise differential identities are vacuous. For $n \geq 1$ and $a < b$ , the linear matrix initial value problem

$Y^{'} (t) = C (t) Y (t), Y (t_{0}) = Y_{0},$

has a unique solution on all of $I$ , with domain-relative one-sided derivatives at the endpoints. If $n \geq 1$ and $a = b$ , then $t_{0} = a$ and there is exactly one map $Y : I \to M_{n} (R)$ with $Y (a) = Y_{0}$ . This singleton map extends to a solution of $Z^{'} = C (a) Z$ , $Z (a) = Y_{0}$ , on an open interval around $a$ ; any two such local continuations agree on their common interval containing $a$ . No time derivative or IVP solution on the singleton itself is asserted.

Facts & Assumptions

Given: The compact interval $I = [a, b]$ , the continuous matrix field $C : I \to M_{n} (R)$ , the time $t_{0} \in I$ , and the initial matrix $Y_{0}$ .

[F1]

Picard-Lindelof gives a unique local solution for a continuous state-Lipschitz first-order system on an open domain (Picard-Lindelöf local existence and uniqueness for first-order systems).

[F2]

A solution of a first-order system is equivalent to a solution of the associated Volterra integral equation (A first-order initial value problem is equivalent to its Volterra integral equation).

[F3]

Every Picard-Lindelof IVP has a unique maximal solution on an open interval, and every other solution through the same data is its restriction (Every Picard–Lindelöf initial value problem has one maximal solution on an open interval).

[L1]

A solution whose graph approaches a compact interior region at a finite endpoint extends past that endpoint (A solution whose graph approaches a compact interior region at a finite endpoint extends past that endpoint).

[L2]

A continuous real-valued function on a nonempty compact metric space attains its maximum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[L3]

The norm of a vector-valued integral is at most the integral of the norm (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).

[L4]

Gronwall's integral inequality converts $u (t) \leq A + \int_{t_{0}}^{t} m (s) u (s) d s$ into an exponential bound (Gronwall's integral inequality with variable and constant coefficients).

Proof

technique · direct

1.1F1givenconstruct

If $n = 0$ , every value lies in the singleton $M_{0} (R)$ , so there is exactly one map on $I$ and all entrywise differential identities are vacuous; no positive-dimensional vector IVP theorem is used. For the remainder assume $n \geq 1$ . Extend $C$ continuously to the open interval $(a - 1, b + 1)$ by setting $\tilde{C} (t) : = C (a)$ for $t < a$ , $\tilde{C} (t) : = C (t)$ for $t \in I$ , and $\tilde{C} (t) : = C (b)$ for $t > b$ . Regard $M_{n} (R)$ as $R^{n^{2}}$ . Then the right-hand side $\tilde{F} (t, Y) : = \tilde{C} (t) Y$ is continuous on the open domain $(a - 1, b + 1) \times R^{n^{2}}$ and is globally Lipschitz in $Y$ on every compact time interval, because $∥ \tilde{C} (t) (Y - Z) ∥_{2} \leq ∥ \tilde{C} (t) ∥ ∥ Y - Z ∥_{2}$ . Hence [F1] gives a unique local solution through $(t_{0}, Y_{0})$ .

2.1givenF1step 1.1

If $a = b$ , then $t_{0} = a$ and the prescribed value $Y (a) = Y_{0}$ determines exactly one map on $I$ . The extension in step 1.1 has constant coefficient $C (a)$ near $a$ , so its local solution is a continuation of this map; [F1] gives agreement of any two such continuations on their common interval containing $a$ . This proves the singleton assertions without differentiating a singleton-domain map. For the remainder assume $a < b$ .

2.2F2F3L2L3L4step 1.1

By [F3], let $J = (α, β)$ be the maximal interval of existence of that solution in $(a - 1, b + 1)$ . Since $C$ is continuous on compact $I$ , [L2] supplies a bound $∥ C (t) ∥ \leq M$ on all of $I$ . For $t \in J \cap [t_{0}, b]$ , the Volterra equation from [F2] and the norm estimate [L3] give the forward inequality below. $∥ Y (t) ∥_{2} \leq ∥ Y_{0} ∥_{2} + M \int_{t_{0}}^{t} ∥ Y (s) ∥_{2} d s .$ Therefore [L4] yields $∥ Y (t) ∥_{2} \leq ∥ Y_{0} ∥_{2} e^{M (t - t_{0})}$ on $J \cap [t_{0}, b]$ .

2.3F2L2L3L4step 1.1

For $t \in J \cap [a, t_{0}]$ , the oriented Volterra equation gives $Y (t) = Y_{0} - \int_{t}^{t_{0}} C (s) Y (s) d s$ , so [L3] gives the reflected inequality below. $∥ Y (t) ∥_{2} \leq ∥ Y_{0} ∥_{2} + M \int_{t}^{t_{0}} ∥ Y (s) ∥_{2} d s .$ The time-reflected part of [L4] therefore yields $∥ Y (t) ∥_{2} \leq ∥ Y_{0} ∥_{2} e^{M (t_{0} - t)}$ on $J \cap [a, t_{0}]$ .

3.1L1step 2.2step 2.3

Put $R : = ∥ Y_{0} ∥_{2} e^{M (b - a)}$ . If $β \leq b$ , then a tail of every sequence $t_{j} ↑ β$ in $J$ has graph points in the compact set $[a, b] \times \overline{B} (0, R) \subseteq (a - 1, b + 1) \times M_{n} (R)$ by steps 2.2 and 2.3. So [L1] extends the solution past $β$ , contradicting maximality. The same argument at the left endpoint rules out $α \geq a$ . Therefore $I \subseteq J$ , and the restriction of the maximal solution to $I$ is defined on all of $I$ .

4.1F1step 1.1step 2.1step 3.1∎

For $n \geq 1$ and $a < b$ , step 3.1 gives existence on all of $I$ . Restricting the solution on the open interval $J$ gives the domain-relative one-sided derivatives at both endpoints of $I$ . Uniqueness follows from [F1] for any two solutions through the same data on their common interval $I$ . Step 2.1 supplies the separate singleton case in positive dimension, and step 1.1 supplies the empty-matrix case.

Linear matrix ODEs have unique global solutions on a fixed interval

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources