khalil_comparison

Three Classical Lemmas in Khalil’s Own Forms: Comparison, the Class-K Sandwich, and Integral Barbalat

At a glance

This page collects three classical results of nonlinear stability theory, each stated in the exact form Khalil’s Nonlinear Systems gives it, and each obtained by casting an already machine-checked building block of this library into that form: the comparison lemma for a linear majorant (Khalil’s Lemma 3.4), the class-$\mathcal{K}$ sandwich estimate behind uniform stability (Khalil’s Theorem 4.8), and the integral form of Barbalat’s lemma (Khalil’s Lemma 8.2). All three are fully machine-checked — Lean’s kernel has verified each one end-to-end, depending on nothing beyond the three standard foundational axioms (propext, Classical.choice, Quot.sound). Nothing is taken on trust: every hypothesis is an ordinary, visible premise of its statement, and the module rests on no open assumption. Links: module index · assumptions ledger · builds on the time-varying comparison bound, the class-K function library, Barbalat’s lemma · sources khalil2002nonlinear, slotine1991applied.

Motivation

The formal library these three results draw on was built from the inside out. Comparison bounds, class-$\mathcal{K}$ comparison functions, an invariance principle, Barbalat’s lemma — each was proved in whatever shape was most convenient to formalize, and that shape does not always match the one a reader carries in from a graduate course. In the standard text, Khalil’s Nonlinear Systems, these same results wear a fixed and familiar dress: they are Lemma 3.4, Theorem 4.8, Lemma 8.2, quoted the same way in a hundred later papers. This page is the dictionary between the two vocabularies. It states three of Khalil’s own lemmas in his own form and proves each one by pointing at the building block already established elsewhere in the library. No new mathematics is introduced; the entire value is the correspondence — that one may open Khalil at a numbered lemma and find the machine-checked statement matching it, hypothesis for hypothesis.

Why these three? Each is a workhorse the thesis reaches for repeatedly. The comparison lemma turns a differential inequality — the kind a Lyapunov argument produces — into an explicit envelope, by bounding the solution of $\dot{v}\le f(t,v)$ with the solution of the associated equality $\dot{u}=f(t,u)$. The class-$\mathcal{K}$ sandwich is the arithmetic core of the Lyapunov uniform-stability theorem: it is the single chain of inequalities that converts a sandwiched, non-increasing energy into a bound on the state. And the integral form of Barbalat’s lemma is the bridge from a convergent integral to a vanishing integrand — the step that concludes an adaptive or time-varying controller drives its error to zero when the invariance principle does not apply.

The objects

Throughout, $E$ is a real normed vector space (in Lean, [NormedAddCommGroup E]), and $\Vert z\Vert$ is the norm of a state $z\in E$. Three families of object recur.

The scalar comparison ODE and its Grönwall envelope. For a scalar continuous function $v:\mathbb{R}\to \mathbb{R}$, a linear majorant is the affine field $f(t,u)=-au+c$ with real constants $a,c$. Its ordinary differential equation $\dot{u}=-au+c$, $u(t_0)=\delta$, has the closed-form integrating-factor solution $\delta e^{-a(t-t_0)}+\frac{c}{a}(1-e^{-a(t-t_0)})$: a decaying transient plus the floor $c/a$. Mathlib packages this solution as gronwallBound, with

$\text{gronwallBound}\delta Kcx=\delta e^{Kx}+\frac{c}{K}(e^{Kx}-1)$

so that the envelope above is exactly gronwallBound $(v{t}_0)(-a)c(t-t_0)$. This is the same object the time-varying comparison bound rides.

The right-hand Dini derivative. For $v$ continuous, the classical comparison lemma is stated not on an ordinary derivative but on the upper right Dini derivative $D^{+}v(t)$, so that it applies to functions that are merely one-sidedly differentiable — precisely the regularity a Lyapunov value along a trajectory carries. In Lean this is expressed through the forward difference quotient slope v t z $=(vz-vt)/(z-t)$ and the “frequently below” relation on the right-neighbourhood filter $\mathcal{N}[>]t$, which is the reading Mathlib’s Grönwall primitive consumes.

Class-$\mathcal{K}$ functions and their inverse. A class-$\mathcal{K}$ function is continuous, zero at zero, and strictly increasing on the ray $[0,\infty )$; a class-${\mathcal{K}}_{\infty }$ function is additionally radially unbounded. The library establishes, in the class-K function library, that a class-${\mathcal{K}}_{\infty }$ function $\alpha$ has a genuine functional inverse classKInv $\alpha$, itself class-${\mathcal{K}}_{\infty }$, satisfying ${\alpha }^{-1}(\alpha (x))=x$ for every $x\ge 0$. That inverse is the one moving part of the sandwich estimate below. It must not be confused with the Gaussian quantile ${\Phi }^{-1}$, a different object entirely (absent from Mathlib, and a documented boundary of the risk layer).

The interval integral. For the integral form of Barbalat, the accumulated integral $F(t)={\int }_0^t\phi (\tau )\mathrm{d}\tau$ is Mathlib’s intervalIntegral, and the fundamental theorem of calculus supplies its derivative.

The comparison lemma for a linear majorant (comparison_lemma_dini)

Khalil (2002), Lemma 3.4 (Comparison Lemma). Consider the scalar equation $\dot{u}=f(t,u)$, $u(t_0)=u_0$. Let $v(t)$ be continuous with upper right Dini derivative $D^{+}v(t)\le f(t,v(t))$ and $v(t_0)\le u_0$. Then $v(t)\le u(t)$ for all $t$ in the interval.

Strategy

The general lemma quantifies over an arbitrary field $f(t,u)$, and its proof needs the maximal interval of existence of the comparison ODE — the full ODE existence-and-uniqueness theory. We deliberately take only the case that needs none of that: the linear majorant $f(t,u)=-au+c$, whose comparison ODE is solved in closed form by the Grönwall envelope. With the solution handed to us as a formula, there is nothing to exist; the lemma becomes a statement about that formula.

The library already proved this envelope bound once, as comparison_shift in the time-varying comparison bound — but from an explicit right-derivative witness (HasDerivWithinAt). Khalil instead states the hypothesis directly on the Dini derivative, $D^{+}v\le f(t,v)$. Since Mathlib’s underlying primitive, le_gronwallBound_of_liminf_deriv_right_le, already accepts the Dini (forward-difference) form, the whole task is to pass that hypothesis through unchanged, one step closer to Khalil’s literal statement than the derivative-witness route.

Proof

We prove: if $v$ is continuous on $[t_0,T]$ and, on $[t_0,T)$, its right-hand Dini derivative is dominated by the linear majorant, then $v(t)\le$ gronwallBound $(v{t}_0)(-a)c(t-t_0)$ throughout $[t_0,T]$.

theorem comparison_lemma_dini {v : ℝ → ℝ} {a c t₀ T : ℝ}
    (hvc : ContinuousOn v (Icc t₀ T))
    (hDini : ∀ t ∈ Ico t₀ T, ∀ r, -a * v t + c < r →
      ∃ᶠ z in 𝓝[>] t, slope v t z < r) :
    ∀ t ∈ Icc t₀ T, v t ≤ gronwallBound (v t₀) (-a) c (t - t₀)

Take as given the continuity of $v$ on $[t_0,T]$ (hvc). The differential-inequality hypothesis hDini is Khalil’s $D^{+}v(t)\le f(t,v(t))$ rendered in the form the Grönwall engine reads: for every level $r$ strictly above the majorant value $-av(t)+c$, the forward difference quotient $\text{slope}(v,t,z)$ is frequently below $r$ as $z\to t^{+}$. This “frequently below every strict upper bound” statement is exactly the assertion that the liminf of the forward slopes does not exceed $-av(t)+c$, which is the differential inequality.

With these two facts the proof is a single application of the Mathlib primitive le_gronwallBound_of_liminf_deriv_right_le. That lemma is fed hvc for continuity and hDini for the slope bound; the initial condition $v(t_0)\le v(t_0)$ holds by reflexivity (so Khalil’s $v(t_0)\le u_0$ is taken here with equality, $u_0=v(t_0)$); and the majorant’s coefficients $-a$ and $c$ are supplied as the constant bounds. It returns, for each $t\in [t_0,T]$, the envelope inequality $v(t)\le$ gronwallBound $(v{t}_0)(-a)c(t-t_0)$, which is the claim. $■$

What this shows

The moral is quantitative. A scalar quantity whose right-hand growth never exceeds a linear majorant $-av+c$ can never rise above the exponential envelope

$v(t)\le v(t_0)e^{-a(t-t_0)}+\frac{c}{a}(1-e^{-a(t-t_0)})$

— a transient that decays at rate $a$ toward the standing floor $c/a$. This is Khalil’s Lemma 3.4 for the one field, the linear majorant, that lets the comparison solution be written down rather than proved to exist; the ODE existence theory the general lemma needs is exactly what this restriction spends nothing on.

The class-K sandwich estimate (classK_sandwich_stability)

Khalil (2002), Theorem 4.8 and the estimate its proof extracts: with ${\alpha }_1\in {\mathcal{K}}_{\infty }$ and ${\alpha }_2\in \mathcal{K}$ sandwiching the Lyapunov function, ${\alpha }_1(\Vert x\Vert )\le V\le {\alpha }_2(\Vert x\Vert )$, and $V$ non-increasing along the motion, $\Vert x(t)\Vert \le {\alpha }_1^{-1}(V(x(t)))\le {\alpha }_1^{-1}(V(x(t_0)))\le {\alpha }_1^{-1}({\alpha }_2(\Vert x(t_0)\Vert ))$, which shows the origin is uniformly stable.

Strategy

Read Khalil’s own chain from left to right and the strategy writes itself. Three facts compose in a row: the lower sandwich ${\alpha }_1\Vert x(t)\Vert \le V(x(t))$; the non-increase $V(x(t))\le V(x(t_0))$ along the trajectory; and the upper sandwich $V(x(t_0))\le {\alpha }_2\Vert x(t_0)\Vert$. Together they give ${\alpha }_1\Vert x(t)\Vert \le {\alpha }_2\Vert x(t_0)\Vert$. To solve this for $\Vert x(t)\Vert$ we must undo ${\alpha }_1$ — and this is where the class-$\mathcal{K}$ library earns its place: the inverse of a class-${\mathcal{K}}_{\infty }$ function is again class-${\mathcal{K}}_{\infty }$ (hence monotone) and is a genuine left inverse on the nonnegative ray. Apply that inverse to both sides and the left one cancels.

A caution the design record insists on: the inverse ${\alpha }_1^{-1}$ here is classKInv ${\alpha }_1$, the class-$\mathcal{K}$ functional inverse proved in the class-K function library. It is not the Gaussian quantile ${\Phi }^{-1}$, which is a separate object the risk layer treats as an open boundary. The two share a superscript and nothing else.

Proof

We prove: given ${\alpha }_1\in {\mathcal{K}}_{\infty }$, ${\alpha }_2\in \mathcal{K}$, the two sandwich bounds, and $V(x(t))\le V(x(t_0))$ for all $t\ge t_0$, the state obeys $\Vert x(t)\Vert \le$ classKInv ${\alpha }_1({\alpha }_2\Vert x(t_0)\Vert )$.

theorem classK_sandwich_stability {α₁ α₂ : ℝ → ℝ}
    (hα₁ : IsClassKInfinity α₁) (_hα₂ : IsClassK α₂)
    {V : E → ℝ} {x : ℝ → E} {t₀ : ℝ}
    (hlo : ∀ z, α₁ ‖z‖ ≤ V z) (hhi : ∀ z, V z ≤ α₂ ‖z‖)
    (hmono : ∀ t, t₀ ≤ t → V (x t) ≤ V (x t₀)) :
    ∀ t, t₀ ≤ t → ‖x t‖ ≤ classKInv α₁ (α₂ ‖x t₀‖)

Fix a time $t\ge t_0$. First assemble Khalil’s chain. Applying the lower sandwich hlo at the point $x(t)$, the non-increase hmono at $t$, and the upper sandwich hhi at $x(t_0)$ in succession,

${\alpha }_1\Vert x(t)\Vert \le V(x(t))\le V(x(t_0))\le {\alpha }_2\Vert x(t_0)\Vert$

so that ${\alpha }_1\Vert x(t)\Vert \le {\alpha }_2\Vert x(t_0)\Vert$.

Now undo ${\alpha }_1$. Because ${\alpha }_1$ is class-${\mathcal{K}}_{\infty }$, its inverse classKInv ${\alpha }_1$ is class-${\mathcal{K}}_{\infty }$ too, and in particular class-$\mathcal{K}$ (this is classKInv_isClassKInfinity from the class-$\mathcal{K}$ library), hence monotone on the ray. Moreover ${\alpha }_1\Vert x(t)\Vert \ge 0$, since a class-$\mathcal{K}$ function is nonnegative on the ray and $\Vert x(t)\Vert \ge 0$. Applying the monotone inverse to both ends of the chain,

$\text{classKInv}{\alpha }_1({\alpha }_1\Vert x(t)\Vert )\le \text{classKInv}{\alpha }_1({\alpha }_2\Vert x(t_0)\Vert )$

Finally cancel on the left. Since classKInv ${\alpha }_1$ is a left inverse of ${\alpha }_1$ on the nonnegative ray (classKInv_leftInvOn), and $\Vert x(t)\Vert \ge 0$, the left-hand side is exactly $\Vert x(t)\Vert$. Substituting gives $\Vert x(t)\Vert \le$ classKInv ${\alpha }_1({\alpha }_2\Vert x(t_0)\Vert )$, as desired. $■$

What this shows

The moral: the Lyapunov uniform-stability theorem, stripped to its arithmetic skeleton, is nothing more than invert the lower comparison function and read off the bound. Every genuinely analytic difficulty — that the inverse of a class-${\mathcal{K}}_{\infty }$ function is again class-${\mathcal{K}}_{\infty }$, continuity and all — was discharged once and for all in the class-$\mathcal{K}$ library; here it is spent in three lines. The estimate this produces, $\Vert x(t)\Vert \le {\alpha }_1^{-1}({\alpha }_2(\Vert x(t_0)\Vert ))$, is the load-bearing bound shared across Khalil’s Theorems 4.1, 4.8, and 4.9: a bound on the current state in terms of the initial state alone, with the class-$\mathcal{K}$ function ${\alpha }_1^{-1}\circ {\alpha }_2$ playing the role of the stability modulus.

The integral form of Barbalat’s lemma (barbalat_integral)

Khalil (2002), Lemma 8.2. Let $\phi :\mathbb{R}\to \mathbb{R}$ be uniformly continuous on $[0,\infty )$. Suppose ${\lim }_{t\to \infty }{\int }_0^t\phi (\tau )\mathrm{d}\tau$ exists and is finite. Then $\phi (t)\to 0$ as $t\to \infty$.

Strategy

Barbalat’s lemma comes in two textbook dresses. The derivative form (Slotine & Li, Lemma 4.2, already machine-checked in Barbalat’s lemma) says a function with a finite limit and a uniformly continuous derivative has that derivative tending to zero. The integral form above is Khalil’s, and it is the one adaptive-control arguments quote directly. The insight is that the two are a single theorem seen through the fundamental theorem of calculus: set $F(t)={\int }_0^t\phi$, and the integral form’s hypotheses become the derivative form’s hypotheses for $F$. Indeed $F$ converges (that is precisely the finite-limit assumption), and by the fundamental theorem $F$ has derivative $\phi$, which is uniformly continuous by assumption. So the entire task is to produce the derivative relation HasDerivAt $F(\phi t)t$ from continuity of $\phi$, and then hand $F$ to the derivative-form lemma.

Proof

We prove: if $\phi$ is uniformly continuous and ${\int }_0^t\phi$ converges to some finite $L$ as $t\to \infty$, then $\phi (t)\to 0$.

theorem barbalat_integral {φ : ℝ → ℝ} (huc : UniformContinuous φ)
    (hconv : ∃ L, Tendsto (fun t => ∫ τ in (0 : ℝ)..t, φ τ) atTop (𝓝 L)) :
    Tendsto φ atTop (𝓝 0)

Uniform continuity of $\phi$ implies, in particular, that $\phi$ is continuous. A continuous integrand is locally integrable, strongly measurable near each point, and continuous at each point — exactly the three inputs the first fundamental theorem of calculus needs. Feeding them to Mathlib’s intervalIntegral.integral_hasDerivAt_right yields, for every $x\in \mathbb{R}$, the derivative relation

$\text{HasDerivAt}(t\mapsto {\int }_0^t\phi (\tau )\mathrm{d}\tau )(\phi (x))x$

that is, the accumulated integral $F$ is everywhere differentiable with $F^{\prime }=\phi$. This is the one place measure theory enters (see the scope note below).

The three ingredients of the derivative-form lemma are now in hand: the derivative witness just produced, the finite-limit hypothesis hconv for $F$, and the uniform continuity huc of $F^{\prime }=\phi$. Applying barbalat (Barbalat’s lemma) to them delivers $\phi (t)\to 0$ as $t\to \infty$. $■$

What this shows

The moral: the integral and derivative forms of Barbalat’s lemma are not two theorems but one, joined by the fundamental theorem of calculus. A convergent integral ${\int }_0^{\infty }\phi$ forces its integrand $\phi$ to die out — provided $\phi$ is uniformly continuous, the smoothness hypothesis that rules out the classic escape $\phi (t)=e^{-t}\sin (e^{2t})$, whose integral converges while the function itself does not decay. In practice this is the step that turns “the accumulated tracking cost is finite” into “the tracking error goes to zero.”

Scope and limitations

• No new mathematics. Each result re-fronts a building block already established and machine-checked elsewhere in the library; the contribution is the faithful correspondence to Khalil’s numbered statements, not a new proof.
• The comparison lemma is only the linear-majorant instance. Khalil’s Lemma 3.4 in full generality, for an arbitrary field $\dot{u}=f(t,u)$, needs the maximal interval of existence — the ODE existence-and-uniqueness theory — which is left out. The linear majorant is exactly the case whose comparison solution is a closed-form envelope.
• The sandwich estimate is autonomous. It captures the class-$\mathcal{K}$ sandwich core of Khalil’s Theorems 4.8 and 4.9. The genuinely time-dependent Lyapunov function $V(t,x)$ and the class-$\mathcal{K}\mathcal{L}$ bound $\Vert x(t)\Vert \le \beta (\Vert x(t_0)\Vert ,t-t_0)$ of Theorem 4.9 stay out, since the library’s flows are autonomous and constructing $\beta$ needs the nonlinear comparison solution.
• The inverse is classKInv, not ${\Phi }^{-1}$. The ${\alpha }_1^{-1}$ of the sandwich estimate is the class-$\mathcal{K}$ functional inverse, fully established. It is unrelated to the Gaussian quantile ${\Phi }^{-1}$, which the risk layer records as an open boundary.
• Integral Barbalat consumes measure theory; it does not develop it. The fundamental-theorem step routes through Mathlib’s measure-theoretic interval integral. It uses that machinery as a finished, axiom-clean fact and builds no measure theory of its own.
• No assumptions taken as given. Unlike the interfaced modules recorded in the assumptions ledger, every hypothesis here is an ordinary, visible premise of its statement — the Dini bound hDini, the sandwich bounds and non-increase hmono, the uniform continuity and convergence of the integral. The module declares no open named hypothesis.

Provenance

• Khalil, Nonlinear Systems, 3rd ed. (2002) — the source of all three statements: Lemma 3.4 (the Comparison Lemma), Theorem 4.8 (uniform stability, and the class-$\mathcal{K}$ estimate its proof extracts), and Lemma 8.2 (the integral form of Barbalat’s lemma). Corpus bibkey khalil2002nonlinear.
• Slotine & Li, Applied Nonlinear Control (1991), Lemma 4.2 — the derivative form of Barbalat’s lemma that barbalat_integral bridges to. Corpus bibkey slotine1991applied.
• Building blocks reused. The Grönwall-envelope comparison bound comparison_shift (the time-varying comparison bound); the class-$\mathcal{K}$ functional inverse classKInv and its properties (the class-K function library); the derivative form barbalat (Barbalat’s lemma).

Machine verification (#print axioms)

Lean’s kernel checked all three theorems end-to-end in the full-library build; the #print axioms report for each, reproduced verbatim, shows dependence on nothing beyond the three standard foundational axioms, with no sorryAx:

Ctrllib/KhalilComparison.lean:123:0: 'Ctrllib.comparison_lemma_dini' depends on axioms: [propext, Classical.choice, Quot.sound]
Ctrllib/KhalilComparison.lean:124:0: 'Ctrllib.classK_sandwich_stability' depends on axioms: [propext, Classical.choice, Quot.sound]
Ctrllib/KhalilComparison.lean:125:0: 'Ctrllib.barbalat_integral' depends on axioms: [propext, Classical.choice, Quot.sound]

The Classical.choice dependence enters honestly through the Mathlib order, metric, and measure-theoretic machinery the three results consume — the same three axioms the rest of the stream stands on. Lean source beside this document: (~/Code/vault/lean/KhalilComparison.lean).