lyapunov_comparison

The Lyapunov comparison lemma, formalized — L2 of the LeanPunov stream

Why this theorem, and why these definitions

The thesis’s stability story is cascade-shaped. The framing paper (giordano2019coordinated) decouples the dynamics into a linear CoM subsystem feeding a coupled attitude-and-end-effector subsystem — its eq 22a/22b triangular structure — and closes the loop with a cascaded-stability argument. The mathematical machinery for such arguments is the Panteley–Loría pair: panteley1998global and panteley2001growth, the two densest Lyapunov sources in our corpus.

Strip those papers to their quantitative core and one scalar object does the heavy lifting: a differential inequality for the Lyapunov function along solutions. Proposition 1 of panteley2001growth shows every uniformly globally asymptotically stable system admits a Lyapunov function $\mathcal{V}$ with (their eq 14)

$$\dot{\mathcal{V}}\le -\mathcal{V}$$

and the boundedness engine inside their Lemma 2 runs on the perturbed version (their eq 35)

$$\dot{v}\le -v+c(r)\Vert x_2(t)\Vert$$

where the driving subsystem’s state $x_2$ injects a disturbance. Everything else in those papers — class-$\mathcal{K}$ bookkeeping, growth conditions, integrability — exists to manufacture or exploit an inequality of this shape. So when Mathlib offers no Lyapunov layer at all (verified absent 2026-07-04: no Lyapunov, no passivity, no LaSalle, no ISS), the first stone to lay is exactly this: the comparison lemma that turns a decrease inequality into an explicit exponential bound. The definitions in the Lean file are the two hypotheses this one theorem consumes — nothing more. We deliberately do not define $\epsilon$–$\delta$ stability yet: no theorem in this file would consume the definition, and a definition without a theorem is dead weight (the design rule for this stream: the theorem drives the definitions).

Sources and provenance

• panteley2001growth (Panteley & Loría, Automatica 37, 2001): cascade setup eqs 1–3, Lyapunov hypotheses eqs 10–12, Proposition 1 (eqs 13–15), Lemma 2 and its eq 35. Verbatim statements extracted from the rendered corpus page 2026-07-05.
• panteley1998global (Panteley & Loría, Syst. Control Lett. 33, 1998): cascade setup eqs 4–5, Theorems 1–3, the class-$\mathcal{K}$/UGAS vocabulary.
• giordano2019coordinated (framing paper): decoupled dynamics eq 22a/22b, passivity property eq 23, Lyapunov function eq 37, derivative eq 38, Proposition IV.1.
• Mathlib substrate: Mathlib.Analysis.ODE.Gronwall — gronwallBound and le_gronwallBound_of_liminf_deriv_right_le (no sign restriction on K; the file’s own header notes the inequality holds “with any sign of K x and f x”).
• The names “comparison lemma” and “ultimate bound(edness)” are Khalil’s (Nonlinear Systems; the book is on the digestion queue, so we cite the concepts by name and defer precise section numbers until the OCR lands — flagged, not fabricated).

The precise statements

Work in a real normed vector space $E$. All four Lean declarations live in Lyapunov.lean beside this document; here is their mathematical content.

Definition (Lyapunov decrease along a field). Let $V:E\to \mathbb{R}$ be differentiable, $f:E\to E$ a vector field, and $a,\epsilon \in \mathbb{R}$. We say $V$ decreases along $f$ at rate $a$ up to $\epsilon$ when for every $y\in E$

$$DV(y)[f(y)]\le -aV(y)+\epsilon$$

where $DV(y)$ is the Fréchet derivative of $V$ at $y$. With $\epsilon =0$ and $a=1$ this is precisely the conclusion of panteley2001growth Proposition 1; with $\epsilon >0$ it majorizes the interconnection term of their Lemma 2 on a horizon where $c(r)\Vert x_2(t)\Vert \le \epsilon$.

Definition (quadratic sandwich). Constants $c_1,c_2$ sandwich $V$ when $c_1\Vert y{\Vert }^2\le V(y)\le c_2\Vert y{\Vert }^2$ for all $y$. This is the quadratic instance of the class-${\mathcal{K}}_{\infty }$ bounds ${\alpha }_1(\Vert x\Vert )\le V\le {\alpha }_2(\Vert x\Vert )$ (panteley2001growth eq 10) — and the framing paper’s Lyapunov function (eq 37)

$$V=\frac{1}{2}{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{M}}\breve{\mathbf{v}}+\frac{1}{2}{\tilde{\mathbf{x}}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}$$

satisfies it with $c_1,c_2$ half the extreme eigenvalues of $\mathrm{diag}(\breve{\mathbf{M}},\breve{\mathbf{K}})$ on any region where the inertia stays bounded.

Theorem (comparison bound). Let $x:[0,T]\to E$ be a solution of $\dot{x}=f(x)$ (continuous on $[0,T]$, right-differentiable with derivative $f(x(t))$ on $[0,T)$), and let $V$ be differentiable with the decrease property above. Then for all $t\in [0,T]$

$$V(x(t))\le V(x(0))e^{-at}+\frac{\epsilon }{a}\left(1-e^{-at}\right)$$

(for $a\ne 0$; the Lean statement covers $a=0$ uniformly via Mathlib’s gronwallBound, which degenerates to $V(x(0))+\epsilon t$ there).

Three corollaries, each one inequality away: with $\epsilon =0$, exponential decay $V(x(t))\le V(x(0))e^{-at}$ (the Proposition-1 shape); with $a>0$, the right side tends to $\epsilon /a$ — the ultimate bound, the cascade’s noise floor; and under the quadratic sandwich, the state-level bound

$$c_1\Vert x(t){\Vert }^2\le c_2\Vert x(0){\Vert }^2{e}^{-at}$$

which after dividing by $c_1>0$ is exponential stability with overshoot constant $\sqrt{c_2/c_1}$ and rate $a/2$ in the norm — the Lyapunov direct method’s exponential conclusion in the quadratic case. (The Lean statement stays division-free and square-level; taking square roots is a paper step.)

Scratch work — where the bound comes from

Pretend for a moment the inequality were an equality: $\dot{w}=-aw+\epsilon$. This linear ODE is solved by the integrating factor $e^{at}$: multiply through and the left side becomes a perfect derivative,

$$\frac{d}{dt}\left(w{e}^{at}\right)=\left(\dot{w}+aw\right)e^{at}=\epsilon e^{at}$$

and integrating from $0$ to $t$ gives $w(t)=w(0)e^{-at}+\frac{\epsilon }{a}(1-e^{-at})$. So the claimed bound is exactly the solution of the comparison system — the equality case. The whole content of the theorem is that solutions of the inequality stay below solutions of the equality. That is the comparison lemma; Grönwall’s inequality is its workhorse.

Proof (paper version, teacher-verifiable)

Assume $v:[0,T]\to \mathbb{R}$ is differentiable with $\dot{v}(t)\le -av(t)+\epsilon$ on $[0,T)$; here $v(t)=V(x(t))$, whose differentiability and derivative value $DV(x(t))[f(x(t))]$ come from the chain rule applied to the differentiable $V$ and the solution $x$. Define, for $a\ne 0$, the deviation from the comparison solution:

$$w(t)=\left(v(t)-\frac{\epsilon }{a}\right)e^{at}$$

Since $w$ is a product of differentiable functions, it is differentiable, and

$$\dot{w}(t)=\left(\dot{v}(t)+av(t)-\epsilon \right)e^{at}$$

By the decrease hypothesis the parenthesis is at most zero, and $e^{at}>0$, so $\dot{w}\le 0$: the function $w$ is nonincreasing. Therefore $w(t)\le w(0)=v(0)-\epsilon /a$, and unwinding the definition of $w$,

$$v(t)\le \frac{\epsilon }{a}+\left(v(0)-\frac{\epsilon }{a}\right)e^{-at}=v(0)e^{-at}+\frac{\epsilon }{a}\left(1-e^{-at}\right)$$

as claimed. For the state-level corollary, chain the sandwich inequalities: $c_1\Vert x(t){\Vert }^2\le V(x(t))\le V(x(0))e^{-at}\le c_2\Vert x(0){\Vert }^2{e}^{-at}$, using $e^{-at}>0$ for the last step. $\square$

How the Lean proof differs — and why it is stronger. The paper proof above assumes $v$ differentiable everywhere on the interval. Mathlib’s le_gronwallBound_of_liminf_deriv_right_le needs only a right lower-slope condition at each interior point (a liminf of forward difference quotients), plus continuity — strictly weaker hypotheses, the textbook-honest setting for Lyapunov derivatives that are only Dini-differentiable along trajectories. The Lean route: chain rule (HasFDerivAt.comp_hasDerivWithinAt) turns the field-level decrease into the trajectory-level slope bound with $K=-a$ (Mathlib’s Grönwall file explicitly permits negative $K$), and gronwallBound evaluates to the display above via $\text{gronwallBound}\delta K\epsilon (t)=\delta e^{Kt}+\frac{\epsilon }{K}(e^{Kt}-1)$ at $K=-a$. Same proof skeleton, weaker hypotheses, machine-checked.

Post-proof analysis

The moral. One scalar inequality carries the entire quantitative content of cascaded-systems stability: the rate $a$ and the disturbance ceiling $\epsilon$ enter once, and the geometry of the state space never appears. This is why Panteley–Loría can run their entire program in class-$\mathcal{K}$ bookkeeping above this engine room — and why it is the right first stone for a Lyapunov layer in Mathlib.

What this does not prove — the honest boundary. The framing paper’s Proposition IV.1 is not an instance of this theorem. Giordano’s Lyapunov derivative (eq 38) is only negative semidefinite — $\dot{V}=-{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{D}}\breve{\mathbf{v}}\le 0$, flat in the $\tilde{\mathbf{x}}$ directions — and the proof closes with LaSalle’s invariance principle plus cascade theorems for compact invariant sets (their ref [13], El-Hawwary & Maggiore 2013). The same relaxation appears as A1.2 (eq 11, $\dot{V}\le -W$ with $W$ positive semidefinite) in panteley2001growth, whose Remark 1 flags it explicitly. Formalizing LaSalle — $\omega$-limit sets, invariance, Barbashin–Krasovskii — is the genuine L3 wall; it exists in no proof assistant’s mainline library that we know of, and this stream’s charter treats it as a phase of its own, not a lemma to rush.

Design note on the definitions. LyapunovDecrease is stated at the field level (a property of $V$ and $f$ alone, quantified over the state space), not along a specific trajectory — so one hypothesis serves every solution, matching how the papers state A1.2/Prop 1. The junk-value trap of Mathlib’s total fderiv (which returns $0$ for non-differentiable $V$, making the decrease predicate vacuously satisfiable) is disarmed by the explicit Differentiable ℝ V hypothesis in every theorem that consumes the definition.

The machine seal

Lyapunov.lean in this directory holds the two definitions, the comparison theorem, and the three corollaries; the #print axioms output for all four theorems is recorded on the stream note (~/Code/tasks/streams/leanpunov.md). The build copy lives at ~/lean/leanpunov/Leanpunov/Lyapunov.lean; this directory’s copy is the tracked source of truth.