[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*}[/step]

[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: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]