barbalat_lemma

Barbalat’s Lemma and the Lyapunov-Like Corollary

The convergence tool for non-autonomous stability, where LaSalle’s invariance principle does not apply. Formalized in Lean 4 for the ctrllib library — machine-checked, #print axioms clean. Proof page: Barbalat (lean module).

Statement

Lemma (Barbalat, derivative form). Let $f:\mathbb{R}\to \mathbb{R}$ be differentiable. If $f$ has a finite limit as $t\to \infty$ and its derivative $\dot{f}$ is uniformly continuous, then

$$\dot{f}(t)⟶0(t\to \infty ).$$

Corollary (Lyapunov-like lemma). Let $V:\mathbb{R}\to \mathbb{R}$ be lower bounded, non-increasing ($\dot{V}\le 0$), with $\dot{V}$ uniformly continuous. Then

$$\dot{V}(t)⟶0(t\to \infty ).$$

(Slotine & Li Lemmas 4.2 and 4.3.)

The corollary is the form used in practice: a Lyapunov (or Lyapunov-like) function gives $\dot{V}\le 0$, so a lower-bounded $V$ converges — but convergence of $V$ alone says nothing about its slope. Barbalat supplies the extra smoothness hypothesis (uniform continuity of $\dot{V}$) that turns “the energy settles” into “the rate $\dot{V}\to 0$” — the step that upgrades a bounded Lyapunov argument to an actual convergence conclusion.

Assumptions

• Uniform continuity of the derivative is essential and is where the hypothesis is spent. Plain continuity is not enough. The standard counterexample is $f(t)=e^{-t}\sin \left(e^{2t}\right)$: it has the finite limit $0$, yet $\dot{f}$ is unbounded and does not tend to $0$ (Slotine §4.5.1).
• Finite limit of $f$ (for the corollary, supplied for free: $\dot{V}\le 0$ plus lower-boundedness gives convergence of $V$ to its infimum by monotone convergence — no uniform continuity needed for this half, matching Slotine’s own remark).
• No autonomy / precompactness assumption. This is exactly why Barbalat is reached for on non-autonomous systems, where LaSalle’s invariance principle — which needs a time-invariant field and a precompact orbit — does not apply.

Proof sketch

Full machine-checked derivation: Barbalat (lean module) (Lean 4 + Mathlib; theorem barbalat / theorem barbalat_lyapunov, #print axioms $\subseteq \{$propext, Classical.choice, Quot.sound$\}$, no sorryAx).

The Lean proof is direct (no contradiction), using Lagrange’s Mean Value Theorem in place of the textbook integration argument. Fix $\epsilon >0$:

1. Uniform continuity of $\dot{f}$ gives a window width $\delta >0$ with $|a-b|<\delta \Rightarrow |\dot{f}(a)-\dot{f}(b)|<\epsilon /2$.
2. Since $f\to L$, the increment over a fixed window vanishes: $f(t+\delta )-f(t)\to 0$, so eventually $|f(t+\delta )-f(t)|<\frac{\epsilon }{2}\delta$. (This step uses only convergence of $f$.)
3. The Mean Value Theorem on $[t,t+\delta ]$ gives $c\in (t,t+\delta )$ with $\dot{f}(c)=\frac{f(t+\delta )-f(t)}{\delta }$, hence $|\dot{f}(c)|<\epsilon /2$.
4. $|t-c|<\delta$, so step 1 gives $|\dot{f}(t)-\dot{f}(c)|<\epsilon /2$; the triangle inequality closes it: $|\dot{f}(t)|\le |\dot{f}(t)-\dot{f}(c)|+|\dot{f}(c)|<\epsilon$.

The two hypotheses appear as the two uses of the window $\delta$: step 1 spends uniform continuity, step 2 spends the finite limit — drop either and the counterexample $e^{-t}\sin (e^{2t})$ walks through. Barbalat’s lemma is confirmed absent from Mathlib v4.31.0 (no barbalat identifier, no UniformContinuous … → Tendsto … 0 lemma), so it is proved from the Mean Value Theorem substrate — an upstream candidate.

Source / provenance

• Literature: slotine1991applied §4.5.2, Lemmas 4.2 (Barbalat) and 4.3 (Lyapunov-like). The verbatim statements were read off the corpus OCR, not reconstructed from memory. Khalil states Barbalat only in §8.3 (outside the currently OCR’d block); Slotine gives it a dedicated section with the clean statement and the practically-used corollary, so it is the canonical cite here. Original result: I. Barbălat (1959).
• Ours: the Lean 4 formalization (Barbalat lean module) and the direct Mean-Value-Theorem proof route.

Caveats

• $\dot{V}\to 0$, not $V\to 0$ and not asymptotic stability of the state. As Slotine’s Example 4.13 stresses, one may conclude a tracking error $\to 0$ while a parameter error stays merely bounded. The consumer must supply the extra structure (e.g. $\dot{V}=-2e^2$) that converts $\dot{V}\to 0$ into a statement about a specific coordinate.
• The Lyapunov-like corollary needs a genuinely uniformly-continuous $\dot{V}$. In applications this is typically established by proving $\ddot{V}$ bounded — an extra bound the analyst must furnish; it is not automatic from $\dot{V}\le 0$.
• Relation to the cascade route. For the proportional form $\dot{V}\le -aV+c\Vert x_2\Vert$ used in the cascade stability arguments, the raw energy does not suffice — a reshaped Lyapunov function is required. See the reshaped-$V_n$ construction in 7-DOF Passivity Extension, where Barbalat’s family of tools and the Panteley–Loría cascade meet.