khalil_stability

Lyapunov’s Direct Method for Autonomous Flows

At a glance

This module states and proves, in Lean, the classical theorem that an energy-like function certifies stability without ever solving the equations of motion: if a smooth function $V$ is positive away from the origin, vanishes at it, and never increases along the motion, then the origin is Lyapunov stable — orbits that start near it stay near it. Strengthening “never increases” to “strictly decreases off the origin” upgrades this to asymptotic stability (orbits actually return to the origin), and adding radial unboundedness of $V$ makes the attraction global. All four results are checked end to end by Lean’s kernel on the three standard foundational axioms (propext, Classical.choice, Quot.sound) — no sorry anywhere. The one standing modeling premise, shared with every dynamical module in this library, is that the flow is given and solves the field (IsSolutionTo); no existence-and-uniqueness theory for the differential equation is developed here.
Links: module index · assumptions ledger · attraction engine LaSalle’s invariance principle · sibling wiring page the Khalil comparison layer · source khalil2002nonlinear

Motivation

Suppose you are handed a nonlinear control system — say the closed loop of a free-flying manipulator — and asked a deceptively simple question: will small disturbances stay small? The honest but useless answer is “solve the equations and look.” For anything nonlinear the closed-form solution does not exist, and numerical integration only ever tells you about the finitely many initial conditions you happened to try.

Lyapunov’s insight, from his 1892 thesis, was to sidestep the solution entirely. Find a scalar “energy” $V$ that is positive everywhere except at the equilibrium, where it bottoms out at zero, and check a single inequality: that $V$ never grows as the state evolves. If you can do that, the equilibrium is stable — and you never integrated a single trajectory. This is the direct method, and it is the workhorse of nonlinear control. Every controller in this project’s guidance stack is ultimately certified by exhibiting such a $V$.

The purpose of this module is to make that certificate machine-checkable. Mathlib — Lean’s mathematics library — has an extensive theory of ordinary differential equations and dynamical systems, but as of this writing it has no Lyapunov-stability layer at all: the classical $\epsilon$–$\delta$ theorem simply is not there. So this module builds it, stating the theorem in Khalil’s own form and proving it against the flow-and-energy primitives the library already owns.

The objects

We work over a real normed vector space $E$, which the theorems specialize to a finite-dimensional space when the argument needs compactness. The dynamics are carried by a flow $\phi$ — a Mathlib Flow ℝ E, meaning a jointly continuous map $\phi :\mathbb{R}\times E\to E$ with ${\phi }_0=\mathrm{id}$ and the group law ${\phi }_{s+t}={\phi }_s\circ {\phi }_t$. We write ${\phi }_{t}x$ for the state reached at time $t$ from the start $x$. The link to a vector field $f:E\to E$ is the standing hypothesis IsSolutionTo ϕ f: for every start $x$ and time $t$, the orbit $t\mapsto {\phi }_{t}x$ has derivative $f({\phi }_{t}x)$. The flow is given to satisfy the differential equation $\dot{x}=f(x)$; we do not construct it.

The energy is a function $V:E\to \mathbb{R}$, assumed differentiable (hVdiff). Two conditions make it a candidate Lyapunov function. It is positive definite: it vanishes at the origin, $V(0)=0$ (hV0), and is strictly positive everywhere else, $V(x)>0$ for $x\ne 0$ (hVpos). And it does not increase along the motion. The rate of change of $V$ along the flow is, by the chain rule, the directional derivative of $V$ in the direction of the field — written in Lean as fderiv ℝ V y (f y), the Fréchet derivative of $V$ at $y$ applied to the field vector $f(y)$, and in Khalil’s notation as $\dot{V}$. The non-increase hypothesis is

$\dot{V}(y)=DV(y)[f(y)]\le 0\text{for every }y\in E(\text{hdec}).$

Now, what does “stable” mean precisely? The intuition is that staying near the origin is a promise you can keep to any tolerance if you are allowed to start close enough. The formal predicate (LyapStable) makes the two quantifiers explicit: for every tolerance $\epsilon$ there is a starting radius $\delta$ such that no orbit begun inside the $\delta$-ball ever leaves the $\epsilon$-ball in forward time,

$\text{LyapStable}\phi :=\forall \epsilon >0,\exists \delta >0,\forall x,\Vert x\Vert <\delta \Rightarrow \forall t\ge 0,\Vert {\phi }_{t}x\Vert <\epsilon .$

Asymptotic stability (AsympStable) asks for more than confinement — it asks that nearby orbits actually converge to the origin, on top of being stable:

$\text{AsympStable}\phi :=\text{LyapStable}\phi \wedge \exists \delta >0,\forall x,\Vert x\Vert <\delta \Rightarrow {\phi }_{t}x\to 0(t\to \infty ).$

These predicates are new to the library. The only stability notion present before was the set-relative StableSet of the reduction campaign (the Theorem-6 finish), which certifies stability of an entire invariant set and carries the heavier machinery that generality demands. The point-stability predicates here are the lighter, more Khalil-faithful objects, and they do not collide with the set-relative ones.

The origin is Lyapunov stable (lyapunov_stable)

This is Khalil’s Theorem 4.1, stability half — and the analytically hardest result in the module. It says exactly: a positive-definite $V$ with $\dot{V}\le 0$ forces the origin to be Lyapunov stable.

Strategy

Work backward from the goal. We are handed a tolerance $\epsilon$ and must manufacture a starting radius $\delta$. The obstruction to overcome is that an orbit might drift outward to the sphere of radius $\epsilon$. We have one lever against drift: $V$ never increases along the motion. The plan, then, is to trap the orbit inside a sublevel set of $V$ that sits strictly inside the $\epsilon$-ball — because an orbit that starts in $\{V<\beta \}$ can never reach a place where $V\ge \beta$, the value $V$ being non-increasing.

The technical question is how to choose the threshold $\beta$. The sphere $\Vert \cdot \Vert =\epsilon$ is where we must not let the orbit go. On that sphere $V$ is strictly positive (it is off the origin), and — this is where finite-dimensionality enters — the sphere is compact, so $V$ attains a genuine minimum $\alpha >0$ there. Any threshold $\beta \in (0,\alpha )$ then does the job: the sublevel set $\{V<\beta \}$ cannot touch the sphere, where $V\ge \alpha >\beta$. Take $\beta =\alpha /2$. Finally, because $V$ is continuous and $V(0)=0<\beta$, a whole ball around the origin lies inside $\{V<\beta \}$ — that ball’s radius is our $\delta$.

The technique is direct construction of $\delta$, with the confinement itself proved by contradiction: assume the orbit does reach the sphere and derive an impossibility via the intermediate value theorem.

Proof

Assume $E$ is finite-dimensional, that $\phi$ solves $f$ (hϕ), and that $V$ is differentiable, positive definite, and non-increasing along $f$ as above. We must show LyapStable ϕ.

First dispose of a degenerate case. If the state space $E$ is a single point, then every point equals $0$, so ${\phi }_{t}x=0$ always, its norm is $0<\epsilon$ for any $\epsilon >0$, and any $\delta$ (the proof takes $\delta =1$) witnesses stability. This is not a mathematical subtlety — it is Lean insisting we handle the trivial vector space, where “the sphere” would be empty and the minimum argument would have nothing to attain. Assume henceforth that $E$ is nontrivial.

Fix a tolerance $\epsilon >0$. The sphere $S:=\{y:\Vert y\Vert =\epsilon \}$ is compact, because a closed and bounded set in a finite-dimensional normed space is compact (isCompact_sphere), and it is nonempty precisely because $E$ is nontrivial and $\epsilon >0$ (NormedSpace.sphere_nonempty). Since $V$ is continuous and $S$ is compact and nonempty, $V$ attains a minimum on $S$ at some point $x_m$ (IsCompact.exists_isMinOn). Because $x_m$ lies on the sphere its norm is $\epsilon >0$, so $x_m\ne 0$, and positive definiteness gives

$\alpha :=V(x_m)>0.$

Set the threshold at half the sphere-minimum,

$\beta :=\frac{\alpha }{2},\text{so that}0<\beta <\alpha .$

Now consider the open set $U:=\{y:V(y)<\beta \}\cap B_{\epsilon }(0)$, the intersection of the preimage of $(-\infty ,\beta )$ under the continuous $V$ with the open $\epsilon$-ball. The origin belongs to $U$: on the one hand $V(0)=0<\beta$, and on the other $\Vert 0\Vert =0<\epsilon$. Since $U$ is open and contains $0$, it contains an entire ball around $0$; let $\delta >0$ be its radius, so that $B_{\delta }(0)\subseteq U$ (Metric.isOpen_iff). This $\delta$ is our witness.

It remains to verify confinement. Let $x$ satisfy $\Vert x\Vert <\delta$ and let $t\ge 0$ be any forward time. Membership $x\in B_{\delta }(0)\subseteq U$ gives us two facts to carry forward: $V(x)<\beta$ and $\Vert x\Vert <\epsilon$. Along the orbit, define $g(s):=V({\phi }_{s}x)$. By the chain rule for the composition of $V$ with the orbit map — which is exactly the derivative bookkeeping the LaSalle engine already packages as IsSolutionTo.hasDerivAt_comp — the function $g$ is differentiable with $g^{\prime }(s)=\dot{V}({\phi }_{s}x)\le 0$ by the non-increase hypothesis. A function with non-positive derivative is non-increasing (antitone_of_deriv_nonpos), so $g$ is antitone: $V({\phi }_{s}x)\le V(x)$ for all $s\ge 0$.

Suppose, for contradiction, that the orbit does escape — that $\Vert {\phi }_{t}x\Vert \ge \epsilon$. The map $s\mapsto \Vert {\phi }_{s}x\Vert$ is continuous on $[0,t]$ (the orbit is continuous, and so is the norm). At the left endpoint its value is $\Vert {\phi }_{0}x\Vert =\Vert x\Vert <\epsilon$, and at the right endpoint it is $\ge \epsilon$. By the intermediate value theorem (intermediate_value_Icc) there is a time $s\in [0,t]$ at which the orbit lands exactly on the sphere, $\Vert {\phi }_{s}x\Vert =\epsilon$, so ${\phi }_{s}x\in S$. Two estimates now collide:

$\alpha =V(x_m)\le V({\phi }_{s}x)\le V(x)<\beta =\frac{\alpha }{2}.$

The left inequality holds because $x_m$ minimizes $V$ over the sphere and ${\phi }_{s}x$ lies on it; the middle inequality is antitonicity of $g$ from time $0$ to time $s$; the last is the fact $V(x)<\beta$ we carried from membership in $U$. But $\alpha <\alpha /2$ is impossible for $\alpha >0$. Hence the orbit never reaches the sphere: $\Vert {\phi }_{t}x\Vert <\epsilon$ for every $t\ge 0$, which is what stability demands. $■$

What this shows

The moral is the whole point of the direct method, made concrete: a single pointwise inequality on $V$ replaces knowledge of every trajectory. We never solved $\dot{x}=f(x)$; we only ever used that $V$ decreases along it, together with two facts about the geometry of $V$ (it is positive on the sphere and continuous at the origin). Notice which hypothesis did which job — compactness of the sphere bought the strictly positive minimum $\alpha$, continuity of $V$ bought the ball $B_{\delta }$, and the non-increase of $V$ bought the confinement. Remove any one and the argument collapses, which is exactly why each appears in the statement.

Strict decrease gives asymptotic stability (lyapunov_asymptotically_stable)

Khalil’s Theorem 4.1 continues: “Moreover, if $\dot{V}(x)<0$ in $D-\{0\}$, then the origin is asymptotically stable.” Confinement is no longer the whole story — we now want nearby orbits to return to the origin.

Strategy

Stability itself is free: strict decrease off the origin certainly implies the non-strict decrease everywhere that the previous theorem needs (at the origin, $f(0)=0$ makes $\dot{V}(0)=0$). So the real work is attraction, and here the tool is not a new hand-built argument but LaSalle’s invariance principle, already proved in this library.

The idea: near the origin, stability traps the forward orbit inside a bounded ball, and in finite dimensions a bounded forward orbit has compact closure — it is forward-precompact. LaSalle’s principle then says the orbit converges to the largest invariant set on which $\dot{V}=0$; more precisely, its $\omega$-limit set is nonempty, invariant, and sits inside $\{\dot{V}=0\}$. But strict decrease means $\dot{V}$ is zero only at the origin. So the $\omega$-limit set can only be $\{0\}$, and an orbit whose $\omega$-limit set is $\{0\}$ converges to $0$.

The technique is construction (produce the attraction radius $\delta$) resting on LaSalle as a black box.

Proof

Add to the previous hypotheses that $f(0)=0$ (hf0) and that the decrease is strict off the origin, $\dot{V}(y)<0$ for $y\ne 0$ (hdecStrict).

We first recover the non-strict decrease needed to invoke the stability theorem. For $y\ne 0$ strict decrease gives $\dot{V}(y)<0$, hence $\le 0$; and at $y=0$, since $f(0)=0$, the directional derivative $\dot{V}(0)=DV(0)[0]=0\le 0$. So $\dot{V}(y)\le 0$ for every $y$ (hdec), and lyapunov_stable delivers Lyapunov stability. It remains to produce a radius of attraction.

Apply stability at tolerance $\epsilon =1$ to obtain a radius $\delta >0$ such that every orbit starting inside $B_{\delta }(0)$ stays inside the unit ball $B_1(0)$ for all forward time. We claim this same $\delta$ is a radius of attraction. Fix $x$ with $\Vert x\Vert <\delta$. The forward orbit $\{{\phi }_{t}x:t\ge 0\}$ lies inside $B_1(0)$, hence is bounded (Metric.isBounded_ball), and a bounded set in a finite-dimensional space has compact closure, so the orbit is forward-precompact (forwardPrecompact_of_isBounded).

Now feed this to LaSalle (lasalle): with $\phi$ solving $f$, $V$ differentiable and non-increasing, and the forward orbit of $x$ precompact, the principle returns an $\omega$-limit set ${\omega }^{+}(x)$ that is nonempty and invariant, on which $V$ is constant, and — the piece we use — on which the derivative vanishes, $\dot{V}(y)=0$ for every $y\in {\omega }^{+}(x)$. We show ${\omega }^{+}(x)\subseteq \{0\}$. Let $y\in {\omega }^{+}(x)$ and suppose $y\ne 0$. Then LaSalle gives $\dot{V}(y)=0$, while strict decrease gives $\dot{V}(y)<0$ — a contradiction. So every point of ${\omega }^{+}(x)$ is the origin.

Finally, an orbit whose $\omega$-limit set is contained in $\{0\}$ converges to $0$. Concretely, fix $\epsilon >0$; since ${\omega }^{+}(x)\subseteq \{0\}\subseteq B_{\epsilon }(0)$ and the ball is open, the library lemma eventually_mem_of_omegaLimit_subset says the orbit is eventually inside $B_{\epsilon }(0)$ — there is a time $N$ beyond which $\Vert {\phi }_{t}x\Vert <\epsilon$. As $\epsilon$ was arbitrary, ${\phi }_{t}x\to 0$ as $t\to \infty$. Together with the stability already established, this is AsympStable ϕ. $■$

What this shows

Strict decrease converts a confinement certificate into a convergence one, and it does so through a clean division of labor: the stability half traps the orbit so that compactness is available, and LaSalle then squeezes the trapped orbit onto the zero-set of $\dot{V}$, which strictness has pinched down to the origin alone. This is also the first place the module reuses rather than builds — the entire attraction argument is LaSalle plus one contradiction, a reminder that the invariance principle is precisely the machine for turning ”$\dot{V}\le 0$ with equality only at the target” into asymptotic convergence.

Radial unboundedness makes every sublevel set bounded (sublevel_isBounded_of_tendsto_cobounded)

Before the global theorem we isolate one small, purely topological fact — the technical heart of what “radially unbounded” buys. It is stated for a general normed space (finite-dimensionality is not needed here).

Statement. If $V\to \infty$ as $\Vert x\Vert \to \infty$, then for every level $c$ the sublevel set $\{y:V(y)\le c\}$ is bounded.

The phrase ”$V\to \infty$ as $\Vert x\Vert \to \infty$” is rendered in Mathlib’s filter language as Tendsto V (Bornology.cobounded E) atTop: along the cobounded filter — the filter of complements of bounded sets, i.e. “as $x$ escapes to infinity” — the value $V(x)$ tends to $+\infty$.

Proof. The claim is the contrapositive of the definition of that limit, unwound. Because $V$ tends to $+\infty$ along the cobounded filter, for the threshold $c$ the value eventually exceeds it: the set $\{y:c<V(y)\}$ belongs to the cobounded filter (hV.eventually applied to eventually_gt_atTop). Now observe that this set is exactly the complement of the sublevel set,

$\{y:V(y)\le c{\}}^{\complement }=\{y:c<V(y)\}.$

A set whose complement is a member of the cobounded filter is, by the very definition of “cobounded,” bounded. Hence $\{V\le c\}$ is bounded. $■$

What this shows. Radial unboundedness is precisely the hypothesis that turns “low energy” into “bounded position.” Its role in the global theorem is to supply, for any start $x$, a bounded region — the sublevel set at level $V(x)$ — that the orbit can never leave, exactly as the unit ball did locally in the previous proof.

Global asymptotic stability — the Barbashin–Krasovskii theorem (lyapunov_globally_asymptotically_stable)

Khalil’s Theorem 4.2 removes the word “near.” With radial unboundedness added, every orbit — no matter how far from the origin it starts — converges to it, and the origin is Lyapunov stable. This is the theorem of Barbashin and Krasovskii.

Strategy

The local proof attracted only orbits starting inside a radius $\delta$, and the reason was purely that we needed a bounded region to get compactness. Radial unboundedness removes that restriction wholesale: the sublevel set $\{V\le V(x)\}$ is bounded for any $x$ (the lemma just proved), and the orbit of $x$ can never leave it because $V$ is non-increasing along the motion. So the same LaSalle endgame that handled near-origin orbits now runs verbatim from an arbitrary start. Stability is unchanged from the local theorem.

Proof

Assume, in addition to positive definiteness and strict decrease off the origin, that $V$ is radially unbounded (hRadUnbdd: $V\to \infty$ along the cobounded filter). As before, strict decrease plus $f(0)=0$ yields the non-strict $\dot{V}\le 0$ everywhere, so lyapunov_stable gives Lyapunov stability. Fix an arbitrary start $x$; we show ${\phi }_{t}x\to 0$.

Along the orbit set $g(s):=V({\phi }_{s}x)$. Exactly as in the first proof, the chain rule and the non-increase hypothesis make $g$ antitone, so $V({\phi }_{t}x)\le V(x)$ for every $t\ge 0$. Therefore the entire forward orbit lies in the sublevel set $\{y:V(y)\le V(x)\}$, which the preceding lemma shows is bounded (radial unboundedness at level $V(x)$). A bounded forward orbit in finite dimensions is forward-precompact (forwardPrecompact_of_isBounded).

From here the argument is identical to the local case. LaSalle (lasalle) returns a nonempty invariant $\omega$-limit set on which $\dot{V}=0$; strict decrease off the origin forces ${\omega }^{+}(x)\subseteq \{0\}$, since a nonzero point of the $\omega$-limit set would have both $\dot{V}=0$ (LaSalle) and $\dot{V}<0$ (strictness). Finally, for each $\epsilon >0$ the containment ${\omega }^{+}(x)\subseteq \{0\}\subseteq B_{\epsilon }(0)$ and eventually_mem_of_omegaLimit_subset place the orbit eventually inside $B_{\epsilon }(0)$, so ${\phi }_{t}x\to 0$. Since $x$ was arbitrary, every orbit converges to the origin. $■$

What this shows

The single hypothesis of radial unboundedness is what separates local from global. Its entire contribution is the bounded sublevel set of the small lemma above — replace the local unit-ball trap with a sublevel-set trap that exists at every energy level, and the local proof becomes global without a new idea. This is the globally asymptotically stable certificate the cascade lemmas downstream ultimately want: a Lyapunov function that is positive definite, radially unbounded, and strictly decreasing pins the whole state space onto the origin.

Assumptions taken as given

Every theorem in this module carries one named hypothesis: IsSolutionTo ϕ f, the statement that the flow $\phi$ exists and solves $\dot{x}=f(x)$ orbitwise. Assuming it is honest for two reasons. First, it is exactly where the direct method’s power lies — Lyapunov’s argument never constructs solutions, it only reasons about whatever solutions there are, so the flow’s existence is genuinely an input, not a gap in the proof. Second, it is the library’s standing modeling premise, shared with the LaSalle module and the entire reduction campaign, recorded once in the assumptions ledger; discharging it (packaging Picard–Lindelöf into a Mathlib flow) is its own open task on that ledger, not a debt of this module.

Scope and limitations

What is proved here is the direct method for an autonomous flow on a finite-dimensional space, with the equilibrium at the origin and the domain global ($D=E$). Several deliberate boundaries are worth stating plainly, so a reader knows exactly what the kernel did and did not verify.

• The flow is taken as given — the named hypothesis above; no existence-and-uniqueness theory (Picard–Lindelöf, completeness of the field, forward versus two-sided time) is developed.
• Autonomous only. The field $f$ and the energy $V$ do not depend on time. Khalil’s time-varying Theorems 4.8–4.9, with a Lyapunov function $V(t,x)$ sandwiched between class-$\mathcal{K}$ bounds, need machinery for time-varying flows that the library does not yet have; the autonomous sandwich core is captured separately in the comparison layer.
• Finite-dimensional. Compactness of spheres and sublevel sets — the source of the attained minimum and of forward-precompactness — is used throughout and holds because closed bounded sets are compact in finite dimensions. The results are stated for that setting.
• No convergence rate. These theorems certify convergence, not its speed. A class-$\mathcal{K}\mathcal{L}$ decay estimate $\Vert x(t)\Vert \le \beta (\Vert x(0)\Vert ,t)$ is a strictly stronger statement, requiring the comparison-function solution and left out here by design.

Provenance

The theorems and their proofs follow Khalil, Nonlinear Systems, 3rd edition (2002), khalil2002nonlinear:

• Theorem 4.1 — Lyapunov stability, with the asymptotic strengthening under strict decrease — is the source of lyapunov_stable and lyapunov_asymptotically_stable. The proof given here is Khalil’s own sublevel-set trapping argument, with the sphere-minimum $\alpha$, the threshold $\beta \in (0,\alpha )$, and the intermediate-value crossing onto the sphere.
• Theorem 4.2 — global asymptotic stability under radial unboundedness — is the source of lyapunov_globally_asymptotically_stable. Khalil attributes this result to Barbashin and Krasovskii; the mechanism is that radial unboundedness makes sublevel sets bounded, which sublevel_isBounded_of_tendsto_cobounded isolates.

The attraction half of both asymptotic theorems is carried by LaSalle’s invariance principle as formalized in this library’s LaSalle module, which supplies the nonempty invariant $\omega$-limit set inside $\{\dot{V}=0\}$ and the “$\omega$-limit in every ball” translation to convergence. Mathlib was verified to contain no Lyapunov-stability layer at the time of writing, which is why the $\epsilon$–$\delta$ theorem is built here rather than imported.

Machine verification (#print axioms)

Lean’s kernel checks each theorem against the standard foundational axioms; the #print axioms command reports the complete list every declaration transitively depends on. For all four public results the list is the standard trio and nothing more — propext (propositional extensionality), Classical.choice (the axiom of choice), and Quot.sound (soundness of quotients) — with no sorryAx, so nothing is left unproved. The output, verbatim from the build:

Ctrllib/KhalilStability.lean:237:0: 'Ctrllib.lyapunov_stable' depends on axioms: [propext, Classical.choice, Quot.sound]
Ctrllib/KhalilStability.lean:238:0: 'Ctrllib.lyapunov_asymptotically_stable' depends on axioms: [propext, Classical.choice, Quot.sound]
Ctrllib/KhalilStability.lean:239:0: 'Ctrllib.sublevel_isBounded_of_tendsto_cobounded' depends on axioms: [propext, Classical.choice, Quot.sound]
Ctrllib/KhalilStability.lean:240:0: 'Ctrllib.lyapunov_globally_asymptotically_stable' depends on axioms: [propext, Classical.choice, Quot.sound]

The tracked source is [(~/Code/vault/lean/KhalilStability.lean)], mirrored byte-for-byte to the lake build copy at ~/lean/ctrllib/Ctrllib/KhalilStability.lean.