comparison_functions

The comparison-function library, formalized — TARGET 12 of the LeanPunov stream

Seal

Rung class-k · Status sealed · #print axioms for every public declaration reports exactly [propext, Classical.choice, Quot.sound] — no sorryAx (recorded in Verification; stream note: sealed 2026-07-06 ~06:05, build green 2648 jobs). No interface hypotheses. Public structures: IsClassK, IsClassKInfinity, IsClassKL; definition classKInv. Confirmed absent from Mathlib v4.31.0 — upstream candidate.
Links: module index · interface ledger · related lyapunov_comparison, time_varying_comparison · sources panteley1998global, panteley2001growth, khalil1996nonlinear (no wiki page yet)

Sealed theorems

IsClassK.monotoneOn

Strict monotonicity weakened to monotone on the ray.

IsClassK.le_of_le

$0\le a\le b$ gives $f(a)\le f(b)$ — the sandwich-to-bound step.

IsClassK.lt_of_lt

Strict version.

IsClassK.nonneg

Nonnegativity on the ray is a theorem, not a definition clause.

IsClassK.pos_of_pos

$x>0$ gives $f(x)>0$.

IsClassK.mapsTo

The ray maps into the ray.

IsClassK.eq_zero_iff

$f(x)=0⟺x=0$ on the ray.

isClassK_id

The identity is class $\mathcal{K}$.

IsClassK.const_mul

Positive scalar multiples stay class $\mathcal{K}$.

IsClassK.comp

Composition stays class $\mathcal{K}$.

IsClassK.add

Sums stay class $\mathcal{K}$.

IsClassK.min

Pointwise min stays class $\mathcal{K}$.

IsClassK.max

Pointwise max stays class $\mathcal{K}$.

isClassKInfinity_id

The identity is class ${\mathcal{K}}_{\infty }$.

IsClassKInfinity.const_mul

Positive scalar multiples stay class ${\mathcal{K}}_{\infty }$.

IsClassKInfinity.comp

Composition stays class ${\mathcal{K}}_{\infty }$.

IsClassKInfinity.surjOn

A class-${\mathcal{K}}_{\infty }$ function covers the whole ray (intermediate value theorem).

IsClassKInfinity.bijOn

A genuine bijection of $[0,\infty )$ onto itself.

IsClassKInfinity.classKInv_leftInvOn

${\alpha }^{-1}(\alpha (x))=x$ on the ray.

IsClassKInfinity.classKInv_rightInvOn

$\alpha ({\alpha }^{-1}(y))=y$ on the ray.

IsClassKInfinity.classKInv_isClassKInfinity

The flagship — the inverse of a class-${\mathcal{K}}_{\infty }$ function is class ${\mathcal{K}}_{\infty }$, continuity via StrictMono.orderIsoOfSurjective.

IsClassKL.nonneg

$\beta (r,s)\ge 0$ on the ray.

Why this module, and why now

Every other stone in this stream has been a theorem — a differential inequality, an invariance principle, a passivity identity. This one is different in kind: it is the vocabulary the later stones are written in. The class-$\mathcal{K}$, ${\mathcal{K}}_{\infty }$ and $\mathcal{K}\mathcal{L}$ comparison functions are the alphabet of nonlinear stability. A Lyapunov function is “positive definite and radially unbounded” precisely when it is sandwiched ${\alpha }_1(\Vert x\Vert )\le V(x)\le {\alpha }_2(\Vert x\Vert )$ by two class-${\mathcal{K}}_{\infty }$ functions; a system is input-to-state stable (ISS) precisely when its trajectory obeys $\Vert x(t)\Vert \le \beta (\Vert x_0\Vert ,t)+\gamma (\Vert u{\Vert }_{\infty })$ with $\beta$ of class $\mathcal{K}\mathcal{L}$ and $\gamma$ of class $\mathcal{K}$. The Panteley–Loría cascade theorems that this stream is climbing toward (panteley1998global Assumptions A1–A4, panteley2001growth Assumptions A1.2–A4) state their hypotheses entirely in this language. We cannot formalize those theorems until the alphabet exists.

It does not exist in Mathlib. A search of Mathlib v4.31.0 for any class-$\mathcal{K}$ / comparison-function development returns nothing — the concept is absent. So this module is, like the house LaSalle layer ((~/Code/vault/lean/lasalle_invariance.md)), a candidate for upstream contribution: a self-contained, axiom-clean development of the comparison-function classes on the reals. The scope here is deliberately broad, not deep — definitions plus a wide base of small structural lemmas — because the substrate’s job is to be reused, not to prove a headline result of its own.

Sources and provenance

The definitions are read verbatim off the rendered sources on disk, not reconstructed from memory.

• panteley1998global (Panteley & Loría, Syst. Control Lett. 33, 1998), Notation paragraph (p.1): “A continuous function $\alpha :{\mathbb{R}}_{\ge 0}\to {\mathbb{R}}_{\ge 0}$ is said to be of class $\mathcal{K}$ if $\alpha (x)$ is strictly increasing and $\alpha (0)=0$; $\alpha \in {\mathcal{K}}_{\infty }$ if in addition $\alpha (x)\to \infty$ as $x\to \infty$. A continuous function $\beta (t,x):{\mathbb{R}}_{\ge 0}\times {\mathbb{R}}_{\ge 0}\to {\mathbb{R}}_{\ge 0}$ is of class $\mathcal{K}\mathcal{L}$ if $\beta (t,\cdot )\in \mathcal{K}$ for each fixed $t$ and $\beta (t,x)\to 0$ as $t\to \infty$ for each $x$.” Note the argument order is $\beta (t,x)$ with $\mathcal{K}$ in the second slot.

• panteley2001growth (Panteley & Loría, Automatica 37, 2001), Notation paragraph (p.3): the identical $\mathcal{K}$, ${\mathcal{K}}_{\infty }$; adds class $\mathcal{L}$ — “continuous, strictly decreasing, ${\lim }_{s\to \infty }\alpha (s)=0$” — and states $\mathcal{K}\mathcal{L}$ in the Khalil argument order $\beta (s,t)$: ”$\beta (\cdot ,t)\in \mathcal{K}$ for each fixed $t\ge 0$ and $\beta (s,\cdot )\in \mathcal{L}$ for each $s\ge 0$.” This is the ordering we formalize, because it is the one the ISS bound $\beta (\Vert x_0\Vert ,t)$ uses.

• Khalil, Nonlinear Systems 3rd ed., §4.4 Definitions 4.2–4.3 — the canonical textbook statement of these classes. Cited by name; the precise section is to be verified when the Khalil OCR lands (the ingest workstation is currently down). Flagged, not fabricated: the two Panteley sources above already pin every clause we formalize, so the definitions stand on rendered provenance regardless.

The two Panteley statements agree on $\mathcal{K}$ and ${\mathcal{K}}_{\infty }$ to the letter and differ only in the cosmetic argument order of $\mathcal{K}\mathcal{L}$. We take the 2001 (Khalil) ordering.

The carrier: ℝ → ℝ with properties on [0,∞)

The paper’s functions live on ${\mathbb{R}}_{\ge 0}$. There are two honest ways to render "${\mathbb{R}}_{\ge 0}$" in Lean: the subtype NNReal, or plain ℝ → ℝ with the defining properties asserted only on the ray Set.Ici 0. We take the second, for three reasons.

1. It composes with the consumers without friction. The quantities the cascade/ISS rungs feed to a comparison function are $\Vert x\Vert :\mathbb{R}$ and a Lyapunov value $V:\mathbb{R}$ — both plain reals. With the ℝ → ℝ carrier, $\alpha (\Vert x\Vert )$ is a bare application; with NNReal it would need a coercion $\alpha (\Vert x{\Vert }_{+})$ at every use site.
2. It matches the house idiom. TimeVaryingComparison.lean ((~/Code/vault/lean/time_varying_comparison.md)) already carries its hypotheses as ContinuousOn v (Ici 0). Reusing Ici 0 keeps the stream’s modules speaking one dialect.
3. Nonnegativity becomes a theorem, not a hypothesis. The paper writes the codomain as ${\mathbb{R}}_{\ge 0}$, but for a class-$\mathcal{K}$ function that is derived: $f(0)=0$ and strict monotonicity give $f(x)\ge f(0)=0$ for $x\ge 0$. We prove this as IsClassK.nonneg rather than bolting it onto the definition — one fewer thing to check when building a class-$\mathcal{K}$ function, and a faithful statement of what the class actually constrains.

Concretely:

structure IsClassK (f : ℝ → ℝ) : Prop where
  continuousOn : ContinuousOn f (Ici 0)
  strictMonoOn : StrictMonoOn f (Ici 0)
  map_zero     : f 0 = 0

structure IsClassKInfinity (f : ℝ → ℝ) : Prop extends IsClassK f where
  tendsto_atTop : Tendsto f atTop atTop

${\mathcal{K}}_{\infty }$ extends $\mathcal{K}$, so every $\mathcal{K}$ lemma applies to a ${\mathcal{K}}_{\infty }$ function through the toIsClassK projection, and unboundedness is the single added field. Encoding ”$f(x)\to \infty$ as $x\to \infty$” as Tendsto f atTop atTop is exact: the filter atTop on ℝ concerns $x\to +\infty$, all of which lie in the ray, so no domain bookkeeping is needed.

The 𝒦ℒ encoding and the r > 0 subtlety

structure IsClassKL (β : ℝ → ℝ → ℝ) : Prop where
  isClassK_fst     : ∀ s, 0 ≤ s → IsClassK (fun r => β r s)
  strictAntiOn_snd : ∀ r, 0 < r → StrictAntiOn (fun s => β r s) (Ici 0)
  tendsto_snd      : ∀ r, 0 < r → Tendsto (fun s => β r s) atTop (𝓝 0)

$\beta (r,s)$ is class $\mathcal{K}$ in its first argument $r$ (for each fixed $s\ge 0$) and class $\mathcal{L}$ in its second argument $s$ (strictly decreasing, tending to $0$). Class $\mathcal{L}$ is unbundled into its two defining clauses strictAntiOn_snd and tendsto_snd rather than given its own structure — it never appears on its own in the cascade hypotheses, so a named IsClassL would be an abstraction with one use site.

The one place we depart from the literal text of panteley2001growth is deliberate and is the sort of thing a reviewer must see. The paper writes ”$\beta (s,\cdot )\in \mathcal{L}$ for each $s\ge 0$”. But class $\mathcal{K}$ in the first argument forces $\beta (0,s)=0$ for all $s$ (that is exactly map_zero of fun r => β r s). So the slice $\beta (0,\cdot )$ is identically zero — and the zero function is not strictly decreasing. The literal “for each $s\ge 0$” is thus vacuously inconsistent at the single point $s=0$; the literature glosses this degenerate slice. We pin it honestly by asserting the decreasing clauses for $r>0$ only. This loses nothing a consumer needs — a $\mathcal{K}\mathcal{L}$ bound $\beta (\Vert x_0\Vert ,t)$ with $\Vert x_0\Vert =0$ means the trajectory started at the origin, where the bound $0$ is already trivial — and it is the same restriction Khalil’s “for each fixed $r$, $\beta (r,s)$ is decreasing” is read with in practice.

The lemma base

Twenty small results, each one a manipulation the cascade/ISS proofs will reach for.

Sign and monotonicity of $\mathcal{K}$. monotoneOn, le_of_le ($0\le a\le b\Rightarrow f(a)\le f(b)$), lt_of_lt, nonneg, pos_of_pos, mapsTo (the ray into the ray), eq_zero_iff ($f(x)=0⟺x=0$ on the ray). The le_of_le shape is exactly the step that turns the sandwich ${\alpha }_1(\Vert x\Vert )\le V$ into a bound on $\Vert x\Vert$ once composed with the inverse.

Constructions of $\mathcal{K}$. The identity isClassK_id; positive scalar multiples const_mul; composition comp (the MapsTo-guarded StrictMonoOn.comp and ContinuousOn.comp); sums add; and pointwise min / max. Closure under min and max is what lets a proof replace two comparison functions by a single dominating (or dominated) one — the standard “take $\alpha =\min ({\alpha }_1,{\alpha }_2)$” move.

Constructions of ${\mathcal{K}}_{\infty }$. isClassKInfinity_id, const_mul, comp (unboundedness composes via Tendsto.comp).

Bijectivity of the carrier. surjOn shows a ${\mathcal{K}}_{\infty }$ function covers the whole ray: continuity plus $f(0)=0$ plus $f\to \infty$ hand the intermediate value theorem (intermediate_value_Ici) every value in $[0,\infty )$. bijOn packages this with injectivity (from StrictMonoOn.injOn) and mapsTo into a genuine bijection of $[0,\infty )$ onto itself. This is the ”${\mathcal{K}}_{\infty }$ is invertible” fact in its cleanest form.

Sign of $\mathcal{K}\mathcal{L}$. IsClassKL.nonneg — $\beta (r,s)\ge 0$ on the ray, immediate from the $\mathcal{K}$-slice.

The inverse is class ${\mathcal{K}}_{\infty }$

The flagship. For $\alpha \in {\mathcal{K}}_{\infty }$ the inverse ${\alpha }^{-1}$ is again class ${\mathcal{K}}_{\infty }$ — this is what makes the ISS manipulation $\alpha (\Vert x\Vert )\le V⟺\Vert x\Vert \le {\alpha }^{-1}(V)$ legitimate. We realize the inverse as classKInv f := Function.invFunOn f (Ici 0), the canonical partial inverse restricted to the ray, and prove:

• classKInv_leftInvOn / classKInv_rightInvOn — the genuine two-sided inverse relations ${\alpha }^{-1}(\alpha (x))=x$ and $\alpha ({\alpha }^{-1}(y))=y$ on the ray, straight from BijOn.invOn_invFunOn.
• classKInv_isClassKInfinity — the inverse is class ${\mathcal{K}}_{\infty }$.

The four pieces of the last result:

• ${\alpha }^{-1}(0)=0$: apply the left-inverse at $\alpha (0)=0$.
• strictly increasing: order-reverse. If ${\alpha }^{-1}(b)\le {\alpha }^{-1}(a)$ then applying the monotone $\alpha$ and the right-inverse gives $b\le a$, contradicting $a<b$.
• unbounded: ${\alpha }^{-1}(x)\ge M$ as soon as $x\ge \alpha (\max (M,0))$, since ${\alpha }^{-1}$ is monotone and ${\alpha }^{-1}(\alpha (\max (M,0)))=\max (M,0)\ge M$.
• continuity — the one genuinely analytic step. Rather than fight a hand-rolled $\epsilon$–$\delta$ inverse-continuity argument, we borrow Mathlib’s order machinery. The restriction of $\alpha$ to the subtype $[0,\infty )$ is a strictly monotone surjection of $[0,\infty )$ onto itself, hence an OrderIso (StrictMono.orderIsoOfSurjective). The subtype $[0,\infty )$ is order-connected, so it carries the order topology (orderTopology_of_ordConnected), and an order isomorphism between order-topology spaces is a homeomorphism — its inverse is continuous for free (OrderIso.continuous). A short bridge identifies invFunOn f (Ici 0) on the ray with the underlying map of that homeomorphism’s inverse (both are the $\alpha$-preimage, equal by injectivity of $\alpha$), and continuousOn_iff_continuous_restrict transports subtype-continuity back to ContinuousOn _ (Ici 0).

That the continuity of the inverse falls out of a Mathlib homeomorphism, with no bespoke analysis, is the payoff of choosing the order-connected ray as the carrier.

What was deliberately left out

• No stability theorems. This module is pure definitional substrate, by scope. The Lyapunov sandwich, ISS estimate, and the Panteley cascade lemmas that consume these classes are separate targets.
• No standalone IsClassL structure — unbundled into the two $\mathcal{K}\mathcal{L}$ clauses, as it has no independent consumer.
• No $\mathcal{K}\mathcal{L}$ construction lemmas (e.g. the canonical $\beta (r,s)=\alpha (r)e^{-s}$). $\mathcal{K}\mathcal{L}$ is carried as a definition with only the nonneg sanity lemma; its builders can be added the turn an ISS proof first needs one, rather than speculatively now.
• No abstract-order generalization. Everything is stated on ℝ. A general-ordered-field version would be the shape of an actual Mathlib PR; for the stream, ℝ is the only carrier the dynamics use.

What the later rungs will consume

• The Lyapunov sandwich rung will use le_of_le / lt_of_lt and IsClassKInfinity.bijOn + classKInv_rightInvOn to move between ${\alpha }_1(\Vert x\Vert )\le V$ and $\Vert x\Vert \le {\alpha }_1^{-1}(V)$.
• The ISS rung will use IsClassKL for the transient term and IsClassK.comp / add / max to assemble the gain composition ${\gamma }_1\circ {\gamma }_2$ and the $\max$ of a state and an input gain.
• The Panteley cascade rung will use IsClassKInfinity for the assumption-${\mathcal{K}}_{\infty }$ bounds ${\alpha }_1,{\alpha }_2,{\alpha }_3$ (panteley2001growth A1.2) and IsClassK for the interconnection coefficient ${\alpha }_4$.

Mathlib substrate used

ContinuousOn.comp, StrictMonoOn.comp (both MapsTo-guarded), StrictMonoOn.monotoneOn, StrictMonoOn.injOn; continuous_min / continuous_max with Continuous.comp_continuousOn and ContinuousOn.prodMk; isPreconnected_Ici with IsPreconnected.intermediate_value_Ici and Ici_mem_atTop for surjectivity; Function.invFunOn with Set.BijOn.invOn_invFunOn and Set.SurjOn.mapsTo_invFunOn; StrictMono.orderIsoOfSurjective with OrderIso.continuous, orderTopology_of_ordConnected, and continuousOn_iff_continuous_restrict for the inverse’s continuity; Filter.Tendsto.const_mul_atTop and tendsto_atTop_atTop.

Verification

Full lake build green. #print axioms for every one of the module’s public declarations (7 $\mathcal{K}$ lemmas, 6 $\mathcal{K}$ constructions, 5 ${\mathcal{K}}_{\infty }$ results, the classKInv definition, 3 inverse results, IsClassKL.nonneg) reports exactly [propext, Classical.choice, Quot.sound] — no sorryAx, no extra axioms. The Classical.choice dependence enters honestly through invFunOn (a choice-based partial inverse) and the order-topology instances; it is the same trio the rest of the stream stands on.

Lean source beside this document: (~/Code/vault/lean/ComparisonFunctions.lean).