Continuous-time LTI solutions: the matrix exponential

Theorems specializing the LTV Peano-Baker series (CtsLTV.lean) to a constant state matrix A, building up to Theorem 6.1: for LTI systems ẋ = Ax, the state transition matrix collapses to the classical closed form Φ(t,t₀) = e^{A(t-t₀)} (6.2). This is what lets every LTV property already proved in CtsLTV.lean (existence, uniqueness, semigroup, invertibility, variation of constants) be reused directly for LTI by specialization, rather than re-derived from scratch.

Reference: Hespanha, Linear Systems Theory (2nd ed.), Chapter 6.

theorem LinearSystems.peanoBakerTerm_const {X : Type u_1} [Fintype X] [DecidableEq X] (A : Matrix X X ℝ) (k : ℕ) (t t₀ : ℝ) : peanoBakerTerm (fun (x : ℝ) => A) k t t₀ = ((t - t₀) ^ k / ↑k.factorial) • A ^ k

Peano-Baker term for constant A (Hespanha, equation (6.1)). For a constant state matrix A, the k-th Peano-Baker term collapses to the closed form ((t-t₀)^k / k!) • A^k.

Reference: Hespanha, Linear Systems Theory (2nd ed.), Chapter 6, equation (6.1).

theorem LinearSystems.stateTransitionMatrix_const_eq_tsum {X : Type u_1} [Fintype X] [DecidableEq X] (A : Matrix X X ℝ) (t t₀ : ℝ) : stateTransitionMatrix (fun (x : ℝ) => A) t t₀ = ∑' (k : ℕ), ((t - t₀) ^ k / ↑k.factorial) • A ^ k

Peano-Baker series for constant A (Hespanha, equation (6.1)). For a constant state matrix A, the continuous-time state transition matrix is given by the power series Φ(t,t₀) = Σ_{k=0}^∞ ((t-t₀)^k / k!) A^k — summing peanoBakerTerm_const termwise.

Reference: Hespanha, Linear Systems Theory (2nd ed.), Chapter 6, equation (6.1).

theorem LinearSystems.stateTransitionMatrix_const {X : Type u_1} [Fintype X] [DecidableEq X] (A : Matrix X X ℝ) (t t₀ : ℝ) : stateTransitionMatrix (fun (x : ℝ) => A) t t₀ = NormedSpace.exp ((t - t₀) • A)

The matrix exponential as state transition matrix (Hespanha, equation (6.2)). For a constant state matrix A, the continuous-time state transition matrix collapses to the matrix exponential Φ(t,t₀) = e^{A(t-t₀)}. This is what lets every LTV property already proved for stateTransitionMatrix (existence, uniqueness, semigroup, invertibility, variation of constants) be reused directly for LTI by specialization.

Proof: sum peanoBakerTerm_const termwise and match against Mathlib's own series characterization of exp (NormedSpace.exp_eq_tsum).

Reference: Hespanha, Linear Systems Theory (2nd ed.), Chapter 6, equation (6.2).

theorem LinearSystems.exp_mulVec_unique {X : Type u_1} [Fintype X] [DecidableEq X] (A : Matrix X X ℝ) {t₀ t₁ : ℝ} (x₀ : X → ℝ) {z : ℝ → X → ℝ} (hz : IsIntegralSolution t₀ t₁ z x₀ fun (x : ℝ) (v : X → ℝ) => A.mulVec v) (hz_cont : ContinuousOn z (Set.uIcc t₀ t₁)) (t : ℝ) : t ∈ Set.uIcc t₀ t₁ → z t = (NormedSpace.exp ((t - t₀) • A)).mulVec x₀

LTI uniqueness (Hespanha, P6.1). e^{A(t-t₀)} *ᵥ x₀ is the unique solution of ẋ = Ax, x(t₀) = x₀, for a constant state matrix A — a direct corollary of the LTV uniqueness theorem stateTransitionMatrix_mulVec_unique, specialized at A := fun _ => A and rewritten via the bridge lemma stateTransitionMatrix_const. No new ODE-theoretic content: uniqueness for LTI systems is just uniqueness for LTV systems at a constant state matrix.

Reference: Hespanha, Linear Systems Theory (2nd ed.), Chapter 6, Property P6.1.

theorem LinearSystems.exp_col_unique {X : Type u_1} [Fintype X] [DecidableEq X] (A : Matrix X X ℝ) {t₀ t₁ : ℝ} (i : X) {z : ℝ → X → ℝ} (hz : IsIntegralSolution t₀ t₁ z (Pi.single i 1) fun (x : ℝ) (v : X → ℝ) => A.mulVec v) (hz_cont : ContinuousOn z (Set.uIcc t₀ t₁)) (t : ℝ) : t ∈ Set.uIcc t₀ t₁ → z t = (NormedSpace.exp ((t - t₀) • A)).col i

Columns of the matrix exponential (Hespanha, P6.2). For every fixed t₀, the i-th column of e^{A(t-t₀)} is the unique solution to ẋ = Ax, x(t₀) = eᵢ, where eᵢ is the i-th standard basis vector — the column-restatement of exp_mulVec_unique, a direct corollary of the LTV theorem stateTransitionMatrix_col_unique.

Reference: Hespanha, Linear Systems Theory (2nd ed.), Chapter 6, Property P6.2.

P6.3 and P6.5 are proved elsewhere

MatrixAlgebra/Exponential.lean carries the semigroup property e^{At} e^{Aτ} = e^{A(t+τ)} (P6.3) and the finite-polynomial form e^{At} = Σ αᵢ(t) Aⁱ (P6.5, via Cayley-Hamilton (6.6)). Both are statements about exp and A alone — no trajectory, no initial time, no state transition matrix — so neither needs the LTV solution theory this file is built on.

What stays here is what genuinely specializes LTV to a constant A: the Peano-Baker collapse (6.1), the closed form (6.2), and uniqueness (P6.1, P6.2).

The time-invariant forced response

For a time-invariant system the state transition matrix is the matrix exponential (stateTransitionMatrix_const), so the variation-of-constants formula collapses to the closed form every textbook writes.

theorem LinearSystems.forcedResponse_timeInvariant {X : Type u_1} [Fintype X] [DecidableEq X] (A : Matrix X X ℝ) {U : Type u_2} [Fintype U] (B : Matrix X U ℝ) (u : ℝ → U → ℝ) (t₀ : ℝ) (x₀ : X → ℝ) (t : ℝ) : forcedResponse (fun (x : ℝ) => A) (fun (x : ℝ) => B) u t₀ x₀ t = (NormedSpace.exp ((t - t₀) • A)).mulVec x₀ + ∫ (τ : ℝ) in t₀..t, (NormedSpace.exp ((t - τ) • A)).mulVec (B.mulVec (u τ))

Variation of constants, time-invariant case. For constant A and B the forced response is the closed form

x(t) = e^{A(t-t₀)} x₀ + ∫ τ in t₀..t, e^{A(t-τ)} B u(τ) dτ.

Reference: Hespanha, Linear Systems Theory (2nd ed.), Chapter 6.

theorem LinearSystems.ContinuousLTI.isTrajectory {X : Type u_1} [Fintype X] [DecidableEq X] {U : Type u_2} {Y : Type u_3} [Fintype U] {u : ℝ → U → ℝ} (sys : ContinuousLTI X U Y ℝ) (hu : Continuous u) (t₀ : ℝ) (x₀ : X → ℝ) : sys.IsTrajectory u fun (t : ℝ) => (NormedSpace.exp ((t - t₀) • sys.A)).mulVec x₀ + ∫ (τ : ℝ) in t₀..t, (NormedSpace.exp ((t - τ) • sys.A)).mulVec (sys.B.mulVec (u τ))

The closed-form response of an LTI system is a trajectory of that system.