LinearSystems.Stability.Continuous.LyapunovLTV

Hespanha's Lyapunov-stability definition for a continuous-time linear time-varying system, read as theorems about the stability predicates of Stability/Continuous/Defs.lean, applied to the unforced system s.toContinuousSystem.zeroInput.

The textbook states four conditions on the homogeneous state response x(t) = Φ(t, t₀) x₀ of ẋ = A(t) x and calls them stability, asymptotic stability, exponential stability and instability. Nothing here re-defines any of those: each of the four is proved equivalent to the predicate the nonlinear track already has, so a result proved on either side is available on the other.

Contents

Each result is stated about a ContinuousLTV, since these are properties of a system, and needs only Continuous s.A — the input and output matrices play no part in Lyapunov stability.

• Definition 8.1(1) — stable_iff_boundedHomogeneousResponse: stability is boundedness of every homogeneous response. Its workhorse stable_iff_boundedStateTransition gives the equivalent bound on Φ(t, t₀) itself, and uniformlyStable_iff_uniformlyBoundedStateTransition makes that bound independent of t₀.
• Definition 8.1(2) — locallyAsymptoticallyStable_iff_decayingHomogeneousResponse.
• Definition 8.1(3) — locallyExponentiallyStable_iff_decayingStateTransition and its global twin globallyExponentiallyStable_iff_decayingStateTransition, with locallyExponentiallyStable_iff_globallyExponentiallyStable recording that for a linear system the two coincide.
• Definition 8.1(4) — unstable_iff_unboundedHomogeneousResponse.

Every one of them is the trajectory characterization plus homogeneity. The trajectory characterization itself is solution theory and lives in Solutions/CtsLTV.lean: ContinuousLTV.isTrajectory_homogeneousResponse for existence and eq_homogeneousResponse_of_isIntegralCurveOn for uniqueness.

One state space, one set of stability predicates

Everything here lives in X → ℝ under the L∞ norm — the space Solutions/ works in, because that is where matrix multiplication is submultiplicative and the Peano–Baker series converges. Stability/Continuous/Defs.lean is stated over an arbitrary real normed space, so its predicates apply here directly: there is no second notion of stability for linear systems and no transport between state spaces.

The unforced system is s.toContinuousSystem.zeroInput, whose trajectories are those of s under the zero input, and ContinuousLTV.vectorField_zero_input reduces its vector field to fun t z => s.A t *ᵥ z. That reduction is what lets the left-hand sides speak about the system while the proofs work with the state matrix.

The predicates quantify over trajectory segments [t₀, t₁], so no solution is assumed to exist for all time; local asymptotic stability also asks for forward completeness, which a linear system has (ContinuousLTV.isForwardComplete_zeroInput).

Why the equivalences are not definitional

Two things separate the textbook statements from the predicates:

• The textbook quantifies over initial conditions, the predicates over trajectories. The gap closes in both directions only because Φ both solves the equation (ContinuousLTV.isTrajectory_homogeneousResponse) and is the unique solution (eq_homogeneousResponse_of_isIntegralCurveOn) — the second is where Grönwall enters, through stateTransitionMatrix_mulVec_unique.
• The textbook's bounds are on the response from every initial state; the predicates' bounds are on the response from a ball. Linearity is what makes these the same: the response from r x₀ is r times the response from x₀, so a bound on any ball scales to a bound everywhere. This is why a linear system has no nontrivial region of attraction, and the reason locallyExponentiallyStable_iff_globallyExponentiallyStable holds.

The sign in Real.exp (-γ * (t - t₀)) is the decaying one; the estimate as printed in some editions of Hespanha carries e^{λ(t-t₀)} with λ > 0, which is a typo for e^{-λ(t-t₀)}.

Reference: Hespanha, Linear Systems Theory (2nd ed.), Chapter 8, Definition 8.1; Khalil, Nonlinear Systems (3rd ed.), Definitions 4.4 and 4.5.

Trajectories of a linear system

"The solutions of ẋ = A(t) x from t₀ are exactly the homogeneous responses Φ(·, t₀) x₀" is solution theory and lives in Solutions/CtsLTV.lean, stated on the system: ContinuousLTV.isTrajectoryOn_homogeneousResponse for existence and ContinuousLTV.eq_homogeneousResponse_of_isTrajectoryOn for uniqueness, on a segment. No bridging is needed here, because a trajectory of s.toContinuousSystem.zeroInput on I is a trajectory of s under the zero input on I — both unfold to IsIntegralCurveOn φ (s.vectorField 0) I.

That the origin is an equilibrium is likewise a property of the system, ContinuousLTV.vectorField_apply_zero. Everything below is those facts plus homogeneity.

Homogeneity

A bound on the response from a ball is a bound from every state, because the response is linear in the initial state: Mathlib's ContinuousLinearMap.opNorm_le_of_ball and ContinuousLinearMap.opNorm_le_of_shell, applied to x ↦ Φ(t, t₀) x. This is the only place linearity is used beyond the trajectory characterization above.

Stability at a single initial time

Lyapunov stability and uniform Lyapunov stability differ only in where the quantifier on the initial time sits — Khalil's whole distinction is the order of ∃ δ and ∀ t₀. The two lemmas below are the content at a fixed t₀, with the margin δ and the bound C explicit, so that each of the two theorems is nothing but quantifier placement on top of them.

Definition 8.1(1): Lyapunov stability

theorem LinearSystems.stable_iff_boundedStateTransition {X : Type u_1} {U : Type u_2} {Y : Type u_3} [Fintype X] [DecidableEq X] [Fintype U] (s : ContinuousLTV X U Y ℝ) (hA : Continuous s.A) : s.toContinuousSystem.zeroInput.Stable 0 ↔ ∀ (t₀ : ℝ), 0 ≤ t₀ → ∃ C ≥ 0, ∀ t ≥ t₀, ∀ (x : X → ℝ), ‖(stateTransitionMatrix s.A t t₀).mulVec x‖ ≤ C * ‖x‖

The state-transition form of Definition 8.1(1): stability of ẋ = A(t) x is a bound ‖Φ(t, t₀) x‖ ≤ C ‖x‖, uniform in t but allowed to depend on t₀.

This is the workhorse behind stable_iff_boundedHomogeneousResponse; it is stated separately because the bound on every state, not the per-initial-condition one, is what later results consume.

theorem LinearSystems.stable_iff_boundedHomogeneousResponse {X : Type u_1} {U : Type u_2} {Y : Type u_3} [Fintype X] [DecidableEq X] [Fintype U] (s : ContinuousLTV X U Y ℝ) (hA : Continuous s.A) : s.toContinuousSystem.zeroInput.Stable 0 ↔ ∀ (t₀ : ℝ), 0 ≤ t₀ → ∀ (x₀ : X → ℝ), ∃ (C : ℝ), ∀ t ≥ t₀, ‖homogeneousResponse s.A t₀ x₀ t‖ ≤ C

The system ẋ = A(t) x is (marginally) stable in the sense of Lyapunov — for every initial condition x(t₀) = x₀ the homogeneous state response x(t) = Φ(t, t₀) x₀ is bounded on [t₀, ∞) — exactly when the origin is a stable equilibrium in the sense of ContinuousSystem.Stable.

The textbook's per-initial-condition form and the state-transition form are equivalent by Banach–Steinhaus: a pointwise-bounded family of operators on a Banach space is norm-bounded.

theorem LinearSystems.uniformlyStable_iff_uniformlyBoundedStateTransition {X : Type u_1} {U : Type u_2} {Y : Type u_3} [Fintype X] [DecidableEq X] [Fintype U] (s : ContinuousLTV X U Y ℝ) (hA : Continuous s.A) : s.toContinuousSystem.zeroInput.UniformlyStable 0 ↔ ∃ C ≥ 0, ∀ (t₀ : ℝ), 0 ≤ t₀ → ∀ t ≥ t₀, ∀ (x : X → ℝ), ‖(stateTransitionMatrix s.A t t₀).mulVec x‖ ≤ C * ‖x‖

Uniform stability is the same bound made independent of the initial time.

Khalil separates uniform stability from stability by the order of the quantifiers on δ and t₀; on the linear side that separation is visible as whether the constant C bounding the response may depend on t₀.

Definition 8.1(2): asymptotic stability

theorem LinearSystems.locallyAsymptoticallyStable_iff_decayingHomogeneousResponse {X : Type u_1} {U : Type u_2} {Y : Type u_3} [Fintype X] [DecidableEq X] [Fintype U] (s : ContinuousLTV X U Y ℝ) (hA : Continuous s.A) : s.toContinuousSystem.zeroInput.LocallyAsymptoticallyStable 0 ↔ (∀ (t₀ : ℝ), 0 ≤ t₀ → ∀ (x₀ : X → ℝ), ∃ (C : ℝ), ∀ t ≥ t₀, ‖homogeneousResponse s.A t₀ x₀ t‖ ≤ C) ∧ ∀ (t₀ : ℝ), 0 ≤ t₀ → ∀ (x₀ : X → ℝ), Filter.Tendsto (homogeneousResponse s.A t₀ x₀) Filter.atTop (nhds 0)

The system ẋ = A(t) x is asymptotically stable — stable, and x(t) = Φ(t, t₀) x₀ → 0 for every initial condition — exactly when the origin is asymptotically stable in the sense of ContinuousSystem.LocallyAsymptoticallyStable.

The boundedness clause is stated because the textbook states it ("in addition"), not because it is needed: a continuous response that converges is bounded.

Definition 8.1(3): exponential stability

theorem LinearSystems.globallyExponentiallyStable_iff_decayingStateTransition {X : Type u_1} {U : Type u_2} {Y : Type u_3} [Fintype X] [DecidableEq X] [Fintype U] (s : ContinuousLTV X U Y ℝ) (hA : Continuous s.A) : s.toContinuousSystem.zeroInput.GloballyExponentiallyStable 0 ↔ ∃ k > 0, ∃ γ > 0, ∀ (t₀ : ℝ), 0 ≤ t₀ → ∀ t ≥ t₀, ∀ (x : X → ℝ), ‖(stateTransitionMatrix s.A t t₀).mulVec x‖ ≤ k * Real.exp (-γ * (t - t₀)) * ‖x‖

Exponential stability in its global form: the response obeys ‖x(t)‖ ≤ k e^{-γ(t - t₀)} ‖x(t₀)‖ for every initial condition.

theorem LinearSystems.locallyExponentiallyStable_iff_decayingStateTransition {X : Type u_1} {U : Type u_2} {Y : Type u_3} [Fintype X] [DecidableEq X] [Fintype U] (s : ContinuousLTV X U Y ℝ) (hA : Continuous s.A) : s.toContinuousSystem.zeroInput.LocallyExponentiallyStable 0 ↔ ∃ k > 0, ∃ γ > 0, ∀ (t₀ : ℝ), 0 ≤ t₀ → ∀ t ≥ t₀, ∀ (x : X → ℝ), ‖(stateTransitionMatrix s.A t t₀).mulVec x‖ ≤ k * Real.exp (-γ * (t - t₀)) * ‖x‖

Exponential stability in its local form. The right-hand side is the same as in globallyExponentiallyStable_iff_decayingStateTransition: the radius c of the local definition carries no information for a linear system.

theorem LinearSystems.locallyExponentiallyStable_iff_globallyExponentiallyStable {X : Type u_1} {U : Type u_2} {Y : Type u_3} [Fintype X] [Fintype U] (s : ContinuousLTV X U Y ℝ) (hA : Continuous s.A) : s.toContinuousSystem.zeroInput.LocallyExponentiallyStable 0 ↔ s.toContinuousSystem.zeroInput.GloballyExponentiallyStable 0

For a linear system, exponential stability is automatically global.

A linear system has no nontrivial region of attraction: the two definitions differ only by a radius, and the response is homogeneous, so the radius scales away.

Definition 8.1(4): instability

theorem LinearSystems.unstable_iff_unboundedHomogeneousResponse {X : Type u_1} {U : Type u_2} {Y : Type u_3} [Fintype X] [DecidableEq X] [Fintype U] (s : ContinuousLTV X U Y ℝ) (hA : Continuous s.A) : s.toContinuousSystem.zeroInput.Unstable 0 ↔ ∃ (t₀ : ℝ), 0 ≤ t₀ ∧ ∃ (x₀ : X → ℝ), ∀ (C : ℝ), ∃ t ≥ t₀, C < ‖homogeneousResponse s.A t₀ x₀ t‖

The system is unstable when it is not marginally stable: some initial condition has an unbounded homogeneous response.