[proofplan]
We estimate the Lyapunov value along a trajectory on an arbitrary finite time interval. The dissipation hypothesis gives scalar decay whenever $V$ lies above an input-dependent threshold, and a scalar comparison argument converts this into a uniform bound by a decaying term plus a disturbance term. The proper bounds $\alpha_1(|x|)\leq V(x)\leq \alpha_2(|x|)$ then translate the Lyapunov estimate into an estimate for $|x(t)|$. Since the estimate is independent of the endpoint of the finite interval, it prevents finite-time blow-up and gives the global ISS bound.
[/proofplan]
[step:Fix a finite time interval and define the input size]
Fix an initial state $x_0 \in \mathbb{R}^n$, a measurable locally essentially bounded input
\begin{align*}
w:[0,\infty)\to \mathbb{R}^m,
\end{align*}
and let
\begin{align*}
x:[0,T_{\max})\to \mathbb{R}^n
\end{align*}
be the maximal solution of $\dot{x}=f(x,w)$ with $x(0)=x_0$. Local Lipschitz continuity of $f$ in $(x,u)$ gives local existence and uniqueness for locally essentially bounded inputs, so $x$ is absolutely continuous on each compact subinterval of $[0,T_{\max})$.
Let $T \in (0,T_{\max})$ be arbitrary. Define the finite-horizon input size
\begin{align*}
M_T:=\|w\|_{L^\infty(0,T)}.
\end{align*}
Since $w$ is locally essentially bounded, $M_T<\infty$. Define the Lyapunov trajectory
\begin{align*}
y:[0,T]\to [0,\infty), \qquad y(t):=V(x(t)).
\end{align*}
Because $V$ is continuously differentiable and $x$ is absolutely continuous, the chain rule for absolutely continuous curves gives, for almost every $t \in [0,T]$,
\begin{align*}
\dot{y}(t)=\nabla V(x(t))\cdot f(x(t),w(t)).
\end{align*}
[/step]
[step:Derive scalar decay above the disturbance threshold]
Define the disturbance threshold in Lyapunov coordinates by
\begin{align*}
c_T:=\alpha_2(\chi(M_T)).
\end{align*}
For almost every $t \in [0,T]$ such that $y(t)>c_T$, the upper Lyapunov bound implies
\begin{align*}
\alpha_2(|x(t)|)\geq V(x(t))=y(t)> \alpha_2(\chi(M_T)).
\end{align*}
Since $\alpha_2 \in \mathcal{K}_\infty$ is strictly increasing, this gives $|x(t)|>\chi(M_T)$. Also $|w(t)|\leq M_T$ for almost every $t \in [0,T]$, and $\chi$ is increasing, so $\chi(|w(t)|)\leq \chi(M_T)$. Hence
\begin{align*}
|x(t)|>\chi(M_T)\geq \chi(|w(t)|).
\end{align*}
The ISS Lyapunov dissipation condition therefore yields
\begin{align*}
\dot{y}(t)\leq -\alpha_3(|x(t)|).
\end{align*}
Using $V(x(t))\leq \alpha_2(|x(t)|)$ and the monotonicity of $\alpha_2^{-1}$, we obtain
\begin{align*}
\alpha_2^{-1}(y(t))\leq |x(t)|.
\end{align*}
Since $\alpha_3$ is increasing,
\begin{align*}
\dot{y}(t)\leq -\alpha_3(\alpha_2^{-1}(y(t))).
\end{align*}
Define the comparison function
\begin{align*}
\rho:[0,\infty)\to [0,\infty), \qquad \rho(s):=\alpha_3(\alpha_2^{-1}(s)).
\end{align*}
Then $\rho \in \mathcal{K}_\infty$, and for almost every $t \in [0,T]$,
\begin{align*}
y(t)>c_T \implies \dot{y}(t)\leq -\rho(y(t)).
\end{align*}
[guided]
The goal of this step is to convert the vector differential inequality for $V$ into a one-dimensional inequality for $y(t)=V(x(t))$. The obstruction is that the Lyapunov dissipation condition is only guaranteed when the state is large compared with the input. We therefore define a threshold depending on the input size over the interval:
\begin{align*}
M_T:=\|w\|_{L^\infty(0,T)}, \qquad c_T:=\alpha_2(\chi(M_T)).
\end{align*}
Suppose that $y(t)>c_T$. Since $y(t)=V(x(t))$ and $V(x)\leq \alpha_2(|x|)$, we get
\begin{align*}
\alpha_2(|x(t)|)\geq y(t)> \alpha_2(\chi(M_T)).
\end{align*}
Because $\alpha_2$ is strictly increasing, this implies $|x(t)|>\chi(M_T)$. On the other hand, by the definition of the essential supremum, $|w(t)|\leq M_T$ for almost every $t\in[0,T]$, and therefore $\chi(|w(t)|)\leq \chi(M_T)$. Thus, for almost every $t$ with $y(t)>c_T$,
\begin{align*}
|x(t)|>\chi(M_T)\geq \chi(|w(t)|).
\end{align*}
This verifies exactly the hypothesis needed to use the ISS Lyapunov dissipation inequality at the point $(x(t),w(t))$. Hence
\begin{align*}
\dot{y}(t)=\nabla V(x(t))\cdot f(x(t),w(t))\leq -\alpha_3(|x(t)|).
\end{align*}
We now want the right-hand side to depend only on $y(t)$, not directly on $x(t)$. The upper Lyapunov estimate gives $y(t)=V(x(t))\leq \alpha_2(|x(t)|)$, so applying the increasing inverse $\alpha_2^{-1}$ gives
\begin{align*}
\alpha_2^{-1}(y(t))\leq |x(t)|.
\end{align*}
Since $\alpha_3$ is increasing,
\begin{align*}
\alpha_3(\alpha_2^{-1}(y(t)))\leq \alpha_3(|x(t)|).
\end{align*}
Therefore
\begin{align*}
\dot{y}(t)\leq -\alpha_3(\alpha_2^{-1}(y(t))).
\end{align*}
Defining
\begin{align*}
\rho:[0,\infty)\to [0,\infty), \qquad \rho(s):=\alpha_3(\alpha_2^{-1}(s)),
\end{align*}
we obtain the scalar implication
\begin{align*}
y(t)>c_T \implies \dot{y}(t)\leq -\rho(y(t)).
\end{align*}
The function $\rho$ belongs to $\mathcal{K}_\infty$ because it is the composition of two $\mathcal{K}_\infty$ functions, namely $\alpha_3$ and $\alpha_2^{-1}$.
[/guided]
[/step]
[step:Apply scalar comparison to bound the Lyapunov value]
By the scalar comparison lemma for differential inequalities with a positive definite right-hand side, applied to the inequality
\begin{align*}
\dot{z}(t)=-\rho(z(t)),
\end{align*}
there exists a function $\sigma\in \mathcal{KL}$ such that every nonnegative absolutely [continuous function](/page/Continuous%20Function) $y$ satisfying
\begin{align*}
y(t)>c_T \implies \dot{y}(t)\leq -\rho(y(t))
\end{align*}
for almost every $t\in[0,T]$ obeys
\begin{align*}
y(t)\leq \max\{\sigma(y(0),t),c_T\}
\end{align*}
for all $t\in[0,T]$. Applying this to the Lyapunov trajectory gives
\begin{align*}
V(x(t))\leq \max\{\sigma(V(x_0),t),\alpha_2(\chi(M_T))\}
\end{align*}
for every $t\in[0,T]$.
Here the scalar comparison lemma is used as an external standard result not yet linked in the wiki: comparison lemma for scalar differential inequalities.
[/step]
[step:Convert the Lyapunov estimate into a state estimate]
Using the lower Lyapunov bound at time $t$ and the upper Lyapunov bound at time $0$, we have
\begin{align*}
\alpha_1(|x(t)|)\leq V(x(t))
\end{align*}
and
\begin{align*}
V(x_0)\leq \alpha_2(|x_0|).
\end{align*}
Therefore, for every $t\in[0,T]$,
\begin{align*}
\alpha_1(|x(t)|)\leq \max\{\sigma(\alpha_2(|x_0|),t),\alpha_2(\chi(M_T))\}.
\end{align*}
Applying the increasing inverse $\alpha_1^{-1}$ gives
\begin{align*}
|x(t)|\leq \max\{\alpha_1^{-1}(\sigma(\alpha_2(|x_0|),t)),\alpha_1^{-1}(\alpha_2(\chi(M_T)))\}.
\end{align*}
Define
\begin{align*}
\beta:[0,\infty)\times[0,\infty)\to[0,\infty), \qquad \beta(r,t):=\alpha_1^{-1}(\sigma(\alpha_2(r),t)),
\end{align*}
and
\begin{align*}
\gamma_0:[0,\infty)\to[0,\infty), \qquad \gamma_0(s):=\alpha_1^{-1}(\alpha_2(\chi(s))).
\end{align*}
Then $\beta\in\mathcal{KL}$ and $\gamma_0\in\mathcal{K}_\infty$, because $\alpha_1^{-1}$, $\alpha_2$, and $\chi$ are $\mathcal{K}_\infty$ functions and $\sigma\in\mathcal{KL}$. Hence
\begin{align*}
|x(t)|\leq \max\{\beta(|x_0|,t),\gamma_0(M_T)\}
\end{align*}
for every $t\in[0,T]$.
[/step]
[step:Remove the finite endpoint and prove forward completeness]
Now fix any $t\in[0,T_{\max})$ and apply the previous estimate with $T=t$ when $t>0$. For $t=0$, the estimate follows directly from $|x(0)|=|x_0|$. Thus, for every $t\in[0,T_{\max})$,
\begin{align*}
|x(t)|\leq \max\left\{\beta(|x_0|,t),\gamma_0\left(\|w\|_{L^\infty(0,t)}\right)\right\}.
\end{align*}
Since $\max\{a,b\}\leq a+b$ for $a,b\geq 0$, this implies
\begin{align*}
|x(t)|\leq \beta(|x_0|,t)+\gamma_0\left(\|w\|_{L^\infty(0,t)}\right).
\end{align*}
It remains to show that $T_{\max}=\infty$. Suppose instead that $T_{\max}<\infty$. Since $w$ is locally essentially bounded, the number
\begin{align*}
M_*:=\|w\|_{L^\infty(0,T_{\max})}
\end{align*}
is finite. Applying the estimate for every $t<T_{\max}$ gives
\begin{align*}
|x(t)|\leq \beta(|x_0|,0)+\gamma_0(M_*),
\end{align*}
because $\beta(|x_0|,t)\leq \beta(|x_0|,0)$ for all $t\geq0$. Thus the trajectory remains in the compact Euclidean ball
\begin{align*}
\overline{B}\left(0,\beta(|x_0|,0)+\gamma_0(M_*)\right)
\end{align*}
on $[0,T_{\max})$. Local Lipschitz continuity of $f$ and essential boundedness of $w$ on $[0,T_{\max})$ imply that a solution whose state remains bounded cannot have a finite maximal existence time. This contradicts the definition of $T_{\max}$. Hence $T_{\max}=\infty$.
Taking $\gamma:=\gamma_0$ gives functions $\beta\in\mathcal{KL}$ and $\gamma\in\mathcal{K}_\infty$ such that
\begin{align*}
|x(t)|\leq \beta(|x_0|,t)+\gamma\left(\|w\|_{L^\infty(0,t)}\right)
\end{align*}
for every $x_0\in\mathbb{R}^n$, every measurable locally essentially bounded input $w$, and every $t\geq0$. This is exactly input-to-state stability.
[/step]
