Read the coefficients off at \(t = 0\); time invariance says every other time agrees with it.

Read the coefficients off at \(k = 0\).

Induction on \(k\): \(P_0\) is constant, and \(P_{k+1}\) is the primitive of a continuous integrand (definition 147), hence continuous by the fundamental theorem of calculus.

Induction on \(k\): bound the integrand \(A(s) P_k(s,t_0)\) pointwise on the segment between \(t_0\) and \(t\), using submultiplicativity of the matrix norm and the induction hypothesis. Split on whether \(t_0 \le t\) or \(t \le t_0\) and integrate the majorant via the power rule, flipping the integral’s orientation (intervalIntegral.integral_symm) in the backward case.

Monotonicity of \(t \mapsto (M|t-t_0|)^k\) on the segment between \(t_0\) and \(t_1\), combined with lemma 150.

Compare against the exponential series \(\sum _k (M|t-t_0|)^k/k!\) via lemma 150 and the comparison test.

Each term \(P_k(\cdot ,t_0)\) is continuous (lemma 149) with a summable, point-independent bound (lemma 151); apply the Weierstrass \(M\)-test for continuity of a series.

Differentiate the Peano–Baker series term by term, using lemma 150 as the uniform bound needed for term-by-term differentiation of a series. The \(k=0\) term is constant, so peel it off and match the shifted series’ derivative against \(A(t)\Phi (t,t_0)\) using linearity of the sum under left multiplication by \(A(t)\).

Every term of the Peano–Baker series beyond \(k=0\) integrates over the degenerate interval \([t_0,t_0]\) and vanishes.

Push theorem 154 through the fixed linear map \(M \mapsto M x_0\) (continuous, since the domain is finite-dimensional).

Right-multiply theorem 154 by the constant \(C\) (HasDerivAt.mul_const), then reassociate.

The fundamental theorem of calculus applied to theorem 156, using \(\Phi (t_0,t_0) = I\) (theorem 155) to fix the initial value.

The fundamental theorem of calculus applied to theorem 157, using \(\Phi (t_0,t_0) = I\) (theorem 155) to fix the initial value.

Apply the continuous-dependence bound of Theorem 3.4 with zero perturbation: since both solutions share the initial value \(x_0\), the resulting bound on \(\| x(t) - z(t)\| \) collapses to \(0\).

Restatement of theorem 160 at \(x_0 := e_i\), using \(\Phi (t,t_0)\, e_i = (\Phi (t,t_0))_{\cdot ,i}\) (Matrix.mulVec_single_one).

Apply the continuous-dependence bound of Theorem 3.4 with zero perturbation: since both solutions share the initial value \(C\), the resulting bound on \(\| Y(t) - Z(t)\| \) collapses to \(0\).

\(\Phi (\cdot ,\tau )\), re-anchored at \(s\), is an integral solution of the matrix ODE on the segment between \(s\) and \(t\) with initial value \(\Phi (s,\tau )\), hence coincides with \(\Phi (\cdot ,s)\, \Phi (s,\tau )\) there by theorem 162.

From theorem 163, generalized to arbitrary order by re-anchoring \(\Phi (\cdot ,\tau )\) at \(t\) and invoking uniqueness there, \(\Phi (\tau ,t)\Phi (t,\tau ) = \Phi (\tau ,\tau ) = I\), so \(\Phi (t,\tau )\) and \(\Phi (\tau ,t)\) are mutual inverses.

\(\Phi (\cdot , a)\), re-anchored at \(b\), is an integral solution of \(\dot Y = A(r)Y\) with value \(\Phi (b,a)\) at \(b\); so is \(\Phi (\cdot , b)\Phi (b,a)\). They agree by theorem 162.

lemma 165 gives \(\Phi (s,\tau ) = \Phi (s,t)\Phi (t,\tau )\); left-multiply by \(\Phi (t,s)\) and cancel using \(\Phi (t,s)\Phi (s,t) = I\) (theorem 164).

theorem 166 with \(\tau \) itself as the middle point gives \(\Phi (t,\tau )\Phi (\tau ,t_0) = \Phi (t,t_0)\); right-multiply by \(\Phi (t_0,\tau )\) and cancel \(\Phi (\tau ,t_0)\Phi (t_0,\tau ) = I\).

By theorem 164, \(\Phi (t,\tau ) = \Phi (\tau ,t)^{-1}\), so the map is \(\tau \mapsto \Phi (\tau ,t)\) — continuous in its first argument — followed by matrix inversion, which is continuous at every unit.

The obstacle is that \(t\) appears in both the upper limit and the integrand. Factor it out: with \(w(t) := x_0 + \int _{t_0}^{t}\Phi (t_0,\tau )B(\tau )u(\tau )\, d\tau \), whose integrand does not depend on \(t\), the fundamental theorem of calculus gives \(w\) directly, and lemma 167 shows \(x(t) = \Phi (t,t_0)w(t)\). Differentiating that product and cancelling \(\Phi (t,t_0)\Phi (t_0,t) = I\) leaves the claim. \(\Phi \) is thus only ever integrated in its second argument, never differentiated there.

For fixed \(t\) the right-hand side \(v \mapsto A(t)v + B(t)u(t)\) is affine in \(v\), hence Lipschitz with constant \(\max (M, 1)\) where \(\| A\| \le M\). Continuous dependence on initial conditions with zero perturbation then bounds \(\| z_1(t) - z_2(t)\| \) by \(0\). The forcing term \(B(t)u(t)\) is common to both solutions and cancels in the difference, so it never enters the Lipschitz estimate.

The integrating-factor identity rewrites the response as \(\Phi (z,t_0)\, w(z)\) with \(w(z) = x_0 + \int _{t_0}^{z}\Phi (t_0,\tau )B(\tau )u(\tau )\, \mathrm{d}\tau \), whose integrand does not depend on \(z\) — only the limit does. Continuity of \(w\) is then the ordinary continuity of a primitive, and \(\Phi (\cdot ,t_0)\) is continuous by lemma 153.

The fundamental theorem of calculus, applied to the derivative on the open interval (theorem 169) together with continuity on the closed one (lemma 175), with lemma 170 fixing the initial value.

For \(t \ne t_0\), apply theorem 169 on a window having \(t\) in its interior; since the window is unordered this covers \(t {\lt} t_0\) as well as \(t {\gt} t_0\), and continuity of \(A\) supplies the bound on the compact segment.

At \(t = t_0\) no such window exists, because the formula is anchored there and \(t_0\) is an endpoint of every window. Instead take the integral form (theorem 176) on \([t_0, t_0+1]\) and on \([t_0-1, t_0]\); each yields a one-sided derivative at \(t_0\) (lemma 35), and the two glue to a two-sided one.

theorem 177 at a system with no inputs, where the forcing integral vanishes (lemma 178). The dummy system is an artefact of the proof: only \(A\) appears in the statement, and no hypothesis on \(B\) is needed.

On \([t_{0}, t]\) the solution satisfies the integral equation (lemma 34), so uniqueness for the Peano–Baker solution (theorem 160) identifies it with \(\Phi (\cdot , t_{0}) x(t_{0})\) there.

theorem 179, restricted to the ray by lemma 86.

theorem 180, after reducing the unforced state equation by lemma 117.

A trajectory on \([t_0, t_1]\) agrees there with the homogeneous response from its initial state (theorem 182), which is a trajectory on \([t_0, \infty )\) (theorem 181).

Induction on \(k\). The \(k = 0\) term is the identity. For the step, \(\Phi _{k+1}(t,t_0) = \int _{t_0}^{t} A\, \Phi _k(s,t_0)\, ds\); substituting the inductive hypothesis pulls \(A^{k+1}\) out of the integral and leaves \(\int _{t_0}^{t}(s-t_0)^k ds = (t-t_0)^{k+1}/(k+1)\), which combines with \(1/k!\) to give \(1/(k+1)!\).

Sum lemma 184 termwise; the Peano–Baker series converges for any continuous state matrix, a constant one included.

Both sides are power series in \(A\): lemma 185 for the left, the defining series of \(\exp \) for the right. Match them termwise.

The time-varying uniqueness theorem applied at the constant state matrix \(A(\cdot ) \equiv A\), whose bound \(\| A(t)\| \le \| A\| \) is immediate, then rewritten through theorem 186. There is no new ODE content: uniqueness for LTI is uniqueness for LTV at a constant matrix.

theorem 187 at \(x_0 = e_i\), in the column form supplied by the time-varying column-uniqueness theorem.

theorem 186 identifies \(\Phi \) with the matrix exponential, applied once to the homogeneous term and once under the integral sign.

theorem 177 at the LTV system of the LTI system (definition 126), whose coefficient maps are constant and so continuous, rewritten by lemma 189.

\(v \mapsto C(t)v\) is a continuous linear map and so commutes with the interval integral; the integrand is continuous by lemma 168.

Write a complex vector as \(v = a + i b\) with \(a, b\) real. Then \(v^{*}P_{\mathbb C}v = a^{\mathsf T}Pa + b^{\mathsf T}Pb\): the imaginary part cancels because \(P\) is symmetric, and the real part is positive because \(v \ne 0\) forces \(a\) or \(b\) to be nonzero.

Entrywise complexification is a continuous ring homomorphism, and \(\exp \) commutes with any such.

Induction gives \(M^{k}v = \mu ^{k}v\) for every \(k\). The map \(N \mapsto Nv\) is linear and continuous, so it commutes with the sum defining \(e^{M} = \sum _{k} (k!)^{-1} M^{k}\), giving \(e^{M}v = \sum _{k} (k!)^{-1}\mu ^{k} v = e^{\mu } v\).

Reverse spectral mapping: every spectral value of \(e^{A_{\mathbb C}}\) is \(e^{\mu }\) for an eigenvalue \(\mu \) of \(A_{\mathbb C}\), and \(|e^{\mu }| = e^{\operatorname {Re}\mu } {\lt} 1\).

\(tA\) and \(\tau A\) commute, being scalar multiples of the same matrix, so the exponential of the sum factors. The general \(e^{X}e^{Y} = e^{X+Y}\) needs commutativity and is false without it; here it is free.

Cayley–Hamilton reduces every power \(A^k\) to a combination of \(A^0, \dots , A^{n-1}\), say with coefficients \(\bar a_i(k)\); substituting into the exponential series and exchanging the finite sum over \(i\) with the infinite sum over \(k\) exhibits \(\alpha _i(t) = \sum _k t^k \bar a_i(k)/k!\) as a witness.

The exchange needs those series to converge, which holds because the reduced coefficients grow at most geometrically, \(|\bar a_i(k)| \le CM^k\), dominating each \(\alpha _i\) by a scalar exponential series. That growth bound is the crux of the proof and is established by iteration, not by spectral theory: “multiply by \(X\), reduce modulo the characteristic polynomial” is a fixed linear operation on the \(n\)-dimensional space of polynomials of degree \({\lt} n\), so one step scales the \(\ell ^1\) size of the coefficient vector by at most a constant factor. No eigenvalues and no Jordan form appear anywhere.

The defining product is over the empty range \([t_0, t_0)\).

Peel the leading factor \(A(t)\) off the defining product.

Induction on \(t\) from \(t_0\): the base case is lemma 205 and the step chains the recursion against lemma 206. No analytic content at all, unlike the continuous-time counterpart — the recursion pins each value outright.

theorem 208 at \(x_0 = e_i\), using \(\Phi (t,t_0)e_i = (\Phi (t,t_0))_{\cdot ,i}\).

Induction on \(t\) from \(s\), chaining lemma 206 at both \(s\) and \(\tau \).

Peel the top term off the sum defining \(x(t+1)\) and fold \(A(t)\Phi (t,\tau +1)\) into \(\Phi (t+1,\tau +1)\) termwise by lemma 206, applied once more to the leading \(\Phi (t,t_0)\) term. The peeled term is exactly \(B(t)u(t)\), since \(\Phi (t+1,t+1) = I\).

Induction on \(t\) from \(t_0\). Unlike theorem 171, no Lipschitz condition or Gronwall estimate is needed: the recursion determines each successive value outright, so uniqueness is immediate.

lemma 211.

theorem 212.

\(\Phi (t_0, t_0) = I\) (lemma 205).

\(\Phi (t+1, t_0) = A(t)\Phi (t, t_0)\) (lemma 206).

\(\Phi (t, t_0)\) is the ordered product of \(t - t_0\) factors, all equal to \(A\).

lemma 217, which is the trajectory condition on the nose.

Both satisfy the forced recursion from the same initial value, so they agree by theorem 213.

lemma 219, after reducing the unforced state equation by lemma 134.

theorem 208, after reducing the unforced state equation by lemma 134.