[proofplan] The proof separates the genuinely deep selection statement from the Lyapunov argument that follows it. The pointwise control Lyapunov inequality says that, away from the origin, the affine input map $u \mapsto a(x)+b(x)u$ admits a strictly negative value; the small-control property is precisely the extra hypothesis that permits a continuous selection with value $0$ at the origin. Once such a feedback is obtained by Artstein's continuous feedback theorem, differentiating $V$ along classical closed-loop solutions gives strict decay. Compactness of sublevels upgrades strict decay to Lyapunov stability and attractivity, and the converse direction follows by evaluating the open-loop infimum at the already stabilizing feedback. [/proofplan]

[step:Use Artstein's continuous selection theorem to choose a stabilizing feedback]For each $x \in \Omega_c$, define the admissible-control set \begin{align*} S(x) := \{u \in \mathbb{R}^m : a(x)+b(x)u<0\}. \end{align*} For $x \in \Omega_c \setminus \{0\}$, the hypothesis \begin{align*} \inf_{u\in\mathbb{R}^m}\bigl(a(x)+b(x)u\bigr)<0 \end{align*} implies $S(x)\ne \varnothing$. More explicitly, if $b(x)=0$, then the displayed infimum equals $a(x)$, so $a(x)<0$ and $S(x)=\mathbb{R}^m$. If $b(x)\ne 0$, the affine map $u\mapsto a(x)+b(x)u$ is nonconstant and admits strictly negative values, so $S(x)$ is nonempty. The set $S(x)$ is open and convex because it is the strict sublevel set of the continuous affine map $u\mapsto a(x)+b(x)u$ on $\mathbb{R}^m$. We invoke Artstein's continuous feedback theorem for control Lyapunov functions with the small-control property, stated here as an external prerequisite not yet resolved to a wiki theorem: if $a:\Omega_c\to\mathbb{R}$ and $b:\Omega_c\to\mathbb{R}^{1\times m}$ are continuous, $a(0)=0$, $b(0)=0$, the affine inequality $a(x)+b(x)u<0$ has nonempty open convex solution sets for every $x\in\Omega_c\setminus\{0\}$, and the small-control property holds at the origin, then there exists a continuous selection $k:\Omega_c\to\mathbb{R}^m$ with $k(0)=0$ and $k(x)\in S(x)$ for every $x\in\Omega_c\setminus\{0\}$. Here $a$ and $b$ are continuous because $V\in C^1(D;\mathbb{R})$ and $f,g$ are continuous; also $a(0)=\nabla V(0)\cdot f(0)=0$ because $f(0)=0$, and $b(0)=0$ because the positive definiteness of the $C^1$ function $V$ at its minimum $0$ gives $\nabla V(0)=0$. The nonempty open convex solution-set condition was verified above, and the small-control property is a stated hypothesis. Applying Artstein's theorem gives a continuous feedback $k:\Omega_c\to\mathbb{R}^m$ such that $k(0)=0$ and \begin{align*} a(x)+b(x)k(x)<0 \end{align*} for every $x\in\Omega_c\setminus\{0\}$.[/step]

[guided]The purpose of the small-control property is to solve a selection problem continuously at the origin. Away from $0$, the control Lyapunov inequality only says that at least one input works at each state. That gives pointwise choices, but pointwise choices need not vary continuously. For each $x\in\Omega_c$, define \begin{align*} S(x) := \{u \in \mathbb{R}^m : a(x)+b(x)u<0\}. \end{align*} This is the set of controls that make the derivative of $V$ strictly negative at $x$. If $x\ne 0$, the hypothesis \begin{align*} \inf_{u\in\mathbb{R}^m}\bigl(a(x)+b(x)u\bigr)<0 \end{align*} means that some $u\in\mathbb{R}^m$ satisfies $a(x)+b(x)u<0$, so $S(x)$ is nonempty. The usual affine structural condition is also encoded in this infimum hypothesis. If $b(x)=0$, then $a(x)+b(x)u=a(x)$ for every $u\in\mathbb{R}^m$, so the infimum condition forces $a(x)<0$ and every input is admissible. If $b(x)\ne 0$, the affine map is nonconstant and the strict infimum condition gives at least one admissible input. The set $S(x)$ is open because the map $u\mapsto a(x)+b(x)u$ is continuous, and it is convex because it is a strict sublevel set of an affine function. The remaining issue is continuity of the choice $x\mapsto u$. We use Artstein's continuous feedback theorem for control Lyapunov functions with the small-control property, stated here as an external prerequisite not yet resolved to a wiki theorem. The theorem requires continuous coefficient maps $a:\Omega_c\to\mathbb{R}$ and $b:\Omega_c\to\mathbb{R}^{1\times m}$, the origin conditions $a(0)=0$ and $b(0)=0$, nonempty open convex admissible sets away from $0$, and the small-control property at $0$. These conditions hold here: $a$ and $b$ are continuous because $V\in C^1(D;\mathbb{R})$ and $f,g$ are continuous; $a(0)=0$ follows from $f(0)=0$; $b(0)=0$ follows because $V$ has a $C^1$ minimum at $0$, hence $\nabla V(0)=0$; the admissible sets were verified above; and the small-control property is a stated hypothesis. The theorem therefore produces a continuous map $k:\Omega_c\to\mathbb{R}^m$ such that $k(0)=0$ and $k(x)\in S(x)$ for every $x\in\Omega_c\setminus\{0\}$. Unpacking the definition of $S(x)$ gives \begin{align*} a(x)+b(x)k(x)<0 \end{align*} for every $x\in\Omega_c\setminus\{0\}$.[/guided]

[step:Compute the closed-loop derivative of the Lyapunov function] Define the closed-loop vector field $F_k:\Omega_c\to\mathbb{R}^n$ by \begin{align*} F_k(x):=f(x)+g(x)k(x). \end{align*} Since $f$, $g$, and $k$ are continuous on $\Omega_c$, the map $F_k$ is continuous. Also $F_k(0)=0$, because $f(0)=0$ and $k(0)=0$. For every $x\in\Omega_c\setminus\{0\}$, the definition of $a$ and $b$ gives \begin{align*} \nabla V(x)\cdot F_k(x)=\nabla V(x)\cdot f(x)+\nabla V(x)g(x)k(x)=a(x)+b(x)k(x). \end{align*} The selection property from the previous step therefore yields \begin{align*} \nabla V(x)\cdot F_k(x)<0 \end{align*} for every $x\in\Omega_c\setminus\{0\}$. [/step]

[step:Show that $V$ strictly decreases along nonzero classical forward solutions] Let $x:[0,\infty)\to\Omega_c$ be a classical solution of the closed-loop equation \begin{align*} \dot{x}(t)=F_k(x(t)). \end{align*} The composition $V\circ x:[0,\infty)\to\mathbb{R}$ is continuously differentiable because $V\in C^1(D;\mathbb{R})$ and $x$ is classical. By the chain rule, for every $t\ge 0$ with $x(t)\ne 0$, \begin{align*} \frac{d}{dt}V(x(t))=\nabla V(x(t))\cdot \dot{x}(t)=\nabla V(x(t))\cdot F_k(x(t))<0. \end{align*} If $x(t)=0$, then $F_k(0)=0$, so the same chain-rule computation gives \begin{align*} \frac{d}{dt}V(x(t))=\nabla V(0)\cdot F_k(0)=0. \end{align*} Thus $t\mapsto V(x(t))$ is nonincreasing on $[0,\infty)$ and is strictly decreasing on every time interval on which $x(t)\ne 0$. [/step]

[step:Use compact sublevels to prove Lyapunov stability] Let $\rho>0$ be such that $B(0,\rho)\subset D$. Fix $\varepsilon>0$ small enough that $B(0,\varepsilon)\subset D$. Since $V$ is continuous and $V(0)=0$, there exists $r_\varepsilon\in(0,c)$ such that \begin{align*} K_{r_\varepsilon}\subset B(0,\varepsilon). \end{align*} Indeed, if no such $r_\varepsilon$ existed, there would be a sequence $(x_j)_{j=1}^{\infty}$ in $\Omega_c\setminus B(0,\varepsilon)$ with $V(x_j)\to 0$. For some $r_0\in(0,c)$, all sufficiently large $x_j$ would lie in the compact set $K_{r_0}$, hence a subsequence would converge to a point $y\in K_{r_0}\setminus B(0,\varepsilon)$ with $V(y)=0$, contradicting positive definiteness of $V$. By continuity of $V$ at $0$, choose $\delta>0$ such that $B(0,\delta)\subset\Omega_c$ and \begin{align*} |x_0|<\delta \implies V(x_0)<r_\varepsilon. \end{align*} If $x:[0,\infty)\to\Omega_c$ is any classical forward solution with $|x(0)|<\delta$, then the preceding step gives \begin{align*} V(x(t))\le V(x(0))<r_\varepsilon \end{align*} for all $t\ge 0$. Hence $x(t)\in K_{r_\varepsilon}\subset B(0,\varepsilon)$ for all $t\ge 0$. This proves Lyapunov stability of the origin relative to classical forward solutions remaining in $\Omega_c$. [/step]

[step:Use strict negativity on compact annuli to prove attractivity] Let $x:[0,\infty)\to\Omega_c$ be a classical forward solution with $V(x(0))<c$. Define \begin{align*} r_0:=V(x(0)). \end{align*} If $r_0=0$, then $x(0)=0$ by positive definiteness. Since the preceding step shows that $t\mapsto V(x(t))$ is nonincreasing and $V(x(t))\ge 0$ for all $t\ge 0$, we have $V(x(t))=0$ for every $t\ge 0$. Positive definiteness then gives $x(t)=0$ for every $t\ge 0$, so $\lim_{t\to\infty}x(t)=0$. Assume $r_0>0$. Since $t\mapsto V(x(t))$ is nonincreasing and bounded below by $0$, the limit \begin{align*} \ell:=\lim_{t\to\infty}V(x(t)) \end{align*} exists in $[0,r_0]$. We prove $\ell=0$. Suppose instead that $\ell>0$. Define the compact annulus \begin{align*} A_{\ell,r_0}:=\{y\in D:\ell\le V(y)\le r_0\}. \end{align*} This set is compact because it is a closed subset of the compact sublevel $K_{r_0}$, and it does not contain $0$ because $V(0)=0<\ell$. Define the [continuous function](/page/Continuous%20Function) $q:A_{\ell,r_0}\to\mathbb{R}$ by \begin{align*} q(y):=\nabla V(y)\cdot F_k(y). \end{align*} From the strict closed-loop Lyapunov inequality, $q(y)<0$ for every $y\in A_{\ell,r_0}$. Since $A_{\ell,r_0}$ is compact, $q$ attains its maximum, and there exists $\eta>0$ such that \begin{align*} q(y)\le -\eta \end{align*} for every $y\in A_{\ell,r_0}$. For every $t\ge 0$, the point $x(t)$ lies in $A_{\ell,r_0}$, because $\ell\le V(x(t))\le r_0$. Therefore \begin{align*} \frac{d}{dt}V(x(t))=q(x(t))\le -\eta \end{align*} for every $t\ge 0$. Integrating this differential inequality over $[0,T]$ with respect to one-dimensional [Lebesgue measure](/page/Lebesgue%20Measure) gives \begin{align*} V(x(T))-V(x(0))=\int_0^T \frac{d}{dt}V(x(t))\, d\mathcal{L}^1(t)\le -\eta T. \end{align*} For $T>r_0/\eta$, the right-hand side gives $V(x(T))<0$, contradicting the positive definiteness of $V$. Hence $\ell=0$. It remains to convert $V(x(t))\to 0$ into $x(t)\to 0$. Let $\varepsilon>0$. As in the stability step, compactness of sublevels and positive definiteness give some $r_\varepsilon\in(0,c)$ such that $K_{r_\varepsilon}\subset B(0,\varepsilon)$. Since $V(x(t))\to 0$, there exists $T_\varepsilon\ge 0$ such that $V(x(t))<r_\varepsilon$ for all $t\ge T_\varepsilon$. Thus $x(t)\in B(0,\varepsilon)$ for all $t\ge T_\varepsilon$. Since $\varepsilon>0$ was arbitrary, \begin{align*} \lim_{t\to\infty}x(t)=0. \end{align*} This proves attractivity relative to classical forward solutions remaining in $\Omega_c$. [/step]

[step:Derive the conditional converse from the stabilizing feedback] Now assume the hypotheses in the converse part. The map $F:U\to\mathbb{R}^n$ is locally Lipschitz by assumption, and the origin is asymptotically stable with basin containing the open neighbourhood $A\subseteq U$. By the assumed converse Lyapunov theorem for locally Lipschitz asymptotically stable systems, applied on $A$, there exists $W\in C^1(A;\mathbb{R})$ that is positive definite, has compact closed sublevels in $A$, and satisfies \begin{align*} \nabla W(x)\cdot F(x)<0 \end{align*} for every $x\in A\setminus\{0\}$. For every $x\in A\setminus\{0\}$, evaluating the open-loop affine expression at the particular input $u=k(x)$ gives \begin{align*} \inf_{u\in\mathbb{R}^m}\nabla W(x)\cdot\bigl(f(x)+g(x)u\bigr)\le \nabla W(x)\cdot\bigl(f(x)+g(x)k(x)\bigr). \end{align*} Since $F(x)=f(x)+g(x)k(x)$, the right-hand side equals \begin{align*} \nabla W(x)\cdot F(x)<0. \end{align*} Therefore \begin{align*} \inf_{u\in\mathbb{R}^m}\nabla W(x)\cdot\bigl(f(x)+g(x)u\bigr)<0 \end{align*} for every $x\in A\setminus\{0\}$. Together with the stated positivity and compact-sublevel properties of $W$, this is exactly the asserted control Lyapunov property for the open-loop system on $A$. [/step]