barbalat

Barbalat’s lemma and the Lyapunov-like corollary — rung R3

Seal

Rung rung-3 · Status sealed · #print axioms for both public declarations reports exactly [propext, Classical.choice, Quot.sound] — no sorryAx (recorded in Verification; full-library build green, 2655 jobs). No interface hypotheses — both theorems are standalone and fully discharged from the Mean Value Theorem. Confirmed absent from Mathlib v4.31.0 (no barbalat identifier; no UniformContinuous … → Tendsto … 0 lemma) — upstream candidate.
Links: module index · interface ledger · related comparison_functions, time_varying_comparison, lyapunov_comparison · source Slotine & Li, Applied Nonlinear Control (1991), §4.5 (corpus bibkey slotine1991applied).

Sealed theorems

barbalat

Barbalat’s lemma, derivative form (Slotine & Li Lemma 4.2). A differentiable $f:\mathbb{R}\to \mathbb{R}$ with a finite limit as $t\to \infty$ and a uniformly continuous derivative $\dot{f}$ has $\dot{f}(t)\to 0$ as $t\to \infty$.

barbalat_lyapunov

The Lyapunov-like lemma (Slotine & Li Lemma 4.3), the form actually used in stability analysis. A scalar $V$ that is lower bounded, non-increasing ($\dot{V}\le 0$), and has a uniformly continuous derivative satisfies $\dot{V}(t)\to 0$ as $t\to \infty$.

Why this module, and why now

Every Lyapunov argument in this library stops at the same wall. A Lyapunov (or Lyapunov-like) function $V$ gives $\dot{V}\le 0$, so $V$ is non-increasing; if it is also bounded below, $V$ converges. But convergence of $V$ says nothing about its slope — the classic counterexample is $f(t)=e^{-t}\sin (e^{2t})$, which tends to a limit while $\dot{f}$ stays unbounded (Slotine, §4.5.1). To conclude that the rate $\dot{V}$ dies out — the step that turns “energy settles” into “the tracking error goes to zero” — one needs an extra smoothness hypothesis on $\dot{V}$. Barbalat’s lemma supplies exactly that hypothesis (uniform continuity), and its Lyapunov-like corollary is the workhorse behind non-autonomous convergence proofs where LaSalle’s invariance principle does not apply.

This is the tool the adaptive-control and time-varying rungs of the thesis reach for. LaSalle (lasalle_invariance) needs an autonomous (time-invariant) field and a precompact orbit; when the closed loop is non-autonomous — as the free-flying manipulator’s tracking error dynamics are — Barbalat is the correct substitute. It stands beside the comparison-function substrate (comparison_functions) and the time-varying comparison bound (time_varying_comparison) as core nonlinear-stability vocabulary that Mathlib does not yet carry.

Sources and provenance

Read verbatim off the rendered OCR on disk (Docs/ocr_out/slotine_li_lightonocr.md, L3547 and L3578–3585), not reconstructed from memory.

• Lemma 4.2 (Barbalat) — “If the differentiable function $f(t)$ has a finite limit as $t\to \infty$, and if $\dot{f}$ is uniformly continuous, then $\dot{f}(t)\to 0$ as $t\to \infty$.”

• Lemma 4.3 (“Lyapunov-Like Lemma”) — “If a scalar function $V(x,t)$ satisfies the following conditions: $V(x,t)$ is lower bounded; $\dot{V}(x,t)$ is negative semi-definite; $\dot{V}(x,t)$ is uniformly continuous in time, then $\dot{V}(x,t)\to 0$ as $t\to \infty$.” Slotine’s own justification: ”$V$ then approaches a finite limiting value $V_{\infty }$ … (this does not require uniform continuity). The above lemma then follows from Barbalat’s lemma.”

Source: Slotine & Li, Applied Nonlinear Control, Prentice Hall 1991, §4.5.2 — filed in the corpus as bibkey slotine1991applied (Docs/raw/references.bib; full-book OCR at Docs/raw/md/slotine1991applied/). Khalil states Barbalat only in §8.3, which is outside the OCR’d block, so Slotine is the canonical cite here. The verbatim quotes above stand on the rendered OCR.

The statement in Lean

theorem barbalat {f f' : ℝ → ℝ} (hderiv : ∀ x, HasDerivAt f (f' x) x)
    (hlim : ∃ L, Tendsto f atTop (𝓝 L)) (huc : UniformContinuous f') :
    Tendsto f' atTop (𝓝 0)

Three encoding choices, each faithful to the paper:

1. Explicit derivative witness. The derivative is carried as a separate function f' with ∀ x, HasDerivAt f (f' x) x, not as deriv f. This sidesteps Mathlib’s total-deriv junk-value trap (the same reasoning time_varying_comparison gives for its explicit HasDerivWithinAt witness) and lets a consumer feed the physical rate $\dot{V}$ directly, without discharging a deriv-vs-witness identity at the use site.

2. Finite limit as an existential. ”$f$ has a finite limit as $t\to \infty$” is ∃ L, Tendsto f atTop (𝓝 L). The atTop filter on $\mathbb{R}$ is exactly $t\to +\infty$.

3. Uniform continuity globally on $\mathbb{R}$. Slotine states the hypotheses on $[0,\infty )$; we state UniformContinuous f' on all of $\mathbb{R}$. The conclusion Tendsto f' atTop (𝓝 0) is a statement about $t\to +\infty$ only, which the atTop filter never lets see any $t$ below any given bound, so demanding the hypotheses on all of $\mathbb{R}$ costs a consumer nothing it cannot arrange by extension — and it removes half-line domain bookkeeping that contributes nothing to the mathematics. This is the single modelling simplification, and it strengthens (never weakens) the hypothesis.

The proof, on paper

The textbook (Slotine) proof argues by contradiction and integration: assume
$\dot{f}\nrightarrow 0$, extract a sequence $t_n\to \infty$ with $|\dot{f}(t_n)|\ge \epsilon$; uniform continuity pins $|\dot{f}|\ge \epsilon /2$ across a fixed
window $[t_n,t_n+\delta ]$; integrating, $f$ accumulates a fixed change $\ge \epsilon \delta /2$ over each window, contradicting the Cauchy criterion of a convergent $f$. We formalize the same idea directly, with Lagrange’s Mean Value Theorem replacing the integral — no contradiction, no sequence extraction, which is markedly cleaner in Lean.

Fix $\epsilon >0$.

1. Uniform continuity gives a window. There is $\delta >0$ such that for all
   $a,b$, $|a-b|<\delta ⟹|\dot{f}(a)-\dot{f}(b)|<\epsilon /2$.

2. The increment over the window vanishes. Because $f(t)\to L$, also $f(t+\delta )\to L$ (shift the $t\to \infty$ filter by the constant $\delta$), so the increment $f(t+\delta )-f(t)\to L-L=0$. Hence there is $N$ with
   $\forall t\ge N,|f(t+\delta )-f(t)|<\frac{\epsilon }{2}\delta .$
   This step uses only convergence of $f$ — not uniform continuity — mirroring Slotine’s parenthetical.

3. Mean Value Theorem. Fix $t\ge N$. On $[t,t+\delta ]$ Lagrange gives $c\in (t,t+\delta )$ with

   = \frac{f(t + \delta) - f(t)}{\delta}. $$

Therefore, by step 2,

< \frac{(\varepsilon/2)\,\delta}{\delta} = \frac{\varepsilon}{2}. $$ 4. **Transfer the bound from $c$ back to $t$.** Since $c \in (t, t + \delta)$ we have $|t - c| < \delta$, so step 1 gives $|\dot f(t) - \dot f(c)| < \varepsilon/2$. The triangle inequality closes it: $$ |\dot f(t)| \le |\dot f(t) - \dot f(c)| + |\dot f(c)| < \tfrac{\varepsilon}{2} + \tfrac{\varepsilon}{2} = \varepsilon. $$ As $\varepsilon > 0$ was arbitrary and the bound holds for every $t \ge N$, $\dot f(t) \to 0$. $\qquad\blacksquare$ The two loads the argument carries are visible in the two uses of the window $\delta$: step 1 (uniform continuity) is where the smoothness hypothesis is spent, and step 2 (a convergent function's increment over a *fixed* window dies) is where the finite-limit hypothesis is spent. Drop either and the counterexample $e^{-t}\sin(e^{2t})$ walks through the gap. ## The corollary, on paper ``` theorem barbalat_lyapunov {V V' : ℝ → ℝ} (hderiv : ∀ x, HasDerivAt V (V' x) x) (hlb : ∃ m, ∀ t, m ≤ V t) (hnonpos : ∀ t, V' t ≤ 0) (huc : UniformContinuous V') : Tendsto V' atTop (𝓝 0) ``` $\dot V \le 0$ everywhere makes $V$ **antitone**; being bounded below, $V$ converges to its infimum $\inf_t V(t)$ by the monotone-convergence theorem. That supplies the finite limit `∃ L, Tendsto V atTop (𝓝 L)` — with **no** appeal to uniform continuity, exactly Slotine's "$V$ then approaches a finite limiting value $V_\infty$ … (this does not require uniform continuity)". Barbalat's lemma applied to $f = V$, $f' = \dot V$ then delivers $\dot V(t) \to 0$. $\qquad\blacksquare$ "Negative semi-definite $\dot V$" in Slotine's scalar setting is precisely $\dot V(t) \le 0$ for all $t$, which is how `hnonpos` reads. ## No SymPy pin Barbalat is a pure analysis limit result — a statement about a filter limit, with no algebraic identity to certify. The house SymPy-pin pattern exists to freeze an *algebraic* claim (a determinant, a congruence transport, a controller rate) as a symbolic ground truth before the Lean is written; there is no such computation here. `sympy_pin` is deliberately empty, and this is the correct call, not an omission. ## Mathlib substrate used `exists_hasDerivAt_eq_slope` (Lagrange's MVT, `HasDerivAt` form) is the analytic core. Around it: `Metric.uniformContinuous_iff` (the $\varepsilon$–$\delta$ form of `UniformContinuous`), `Metric.tendsto_atTop` and `NormedAddGroup.tendsto_nhds_zero` (the $\varepsilon$–$N$ readings of the two limits), `tendsto_atTop_add_const_right` with `Tendsto.comp` (to shift $f$ by $\delta$), `continuous_iff_continuousAt` with `HasDerivAt.continuousAt` (the `ContinuousOn` premise of the MVT), `abs_add_le`, `abs_div`, `abs_of_pos`, `div_lt_iff₀`. The corollary adds `antitone_of_deriv_nonpos` (with `HasDerivAt.deriv` and `HasDerivAt.differentiableAt` to feed it) and `tendsto_atTop_ciInf` (monotone convergence to the infimum). ## Honest scope - **No interface hypotheses.** Both theorems are `sealed`: everything they need is either a stated hypothesis in the natural mathematical shape (differentiability, the finite limit, uniform continuity, lower-boundedness, $\dot V \le 0$) or a kernel-checked Mathlib fact. Nothing enters on trust. - **The one modelling choice** is the global-$\mathbb{R}$ domain of the hypotheses (see the statement section) — a strengthening that costs the $t \to \infty$ conclusion nothing. - **What is *not* claimed.** Barbalat gives $\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 the tracking error $\to 0$ while a parameter error stays merely bounded. The consumer supplies the extra structure (e.g. $\dot V = -2e^2$) that turns $\dot V \to 0$ into a statement about a specific coordinate. ## Verification Full `lake build` green (2655 jobs; module built in isolation as `Ctrllib.Barbalat`, 2039 jobs). `#print axioms` for both public declarations: ``` 'Ctrllib.barbalat' depends on axioms: [propext, Classical.choice, Quot.sound] 'Ctrllib.barbalat_lyapunov' depends on axioms: [propext, Classical.choice, Quot.sound] ``` No `sorryAx`, no extra axioms. The `Classical.choice` dependence enters honestly through Mathlib's metric/order machinery (the same trio the rest of the stream stands on). Lean source beside this document: (~/Code/vault/lean/Barbalat.lean).