5. Lyapunov analyses

This page explains how AutoLyap uses the algorithm representation and interpolation assumptions to cast the existence of a Lyapunov analysis as the feasibility of a particular SDP. Moreover, this formulation is constructive, in the sense that any feasible solution directly yields an explicit Lyapunov function and associated convergence certificate.

For later convenience across pages 5.1, 5.2, and 5.3, we introduce the solution variables used in the Lyapunov analyses.

We are interested in analyses that may depend on a solution to the inclusion problem (2.1). Without loss of generality and for computational efficiency, we use

(5.1)\[\begin{split}\begin{aligned} \p{y^{\star}, \hat{\bu}^{\star}, \bFcn^{\star}} \in \Bigset{ \underbracket{\p{y,\hat{\bu}, \bFcn}}_{ \in \calH \times\calH^{m-1} \times \reals^{\NumFunc} } \xmiddle| \begin{aligned} &\p{u_{i}}_{i\in\IndexFunc} \in \prod_{i\in\IndexFunc}\partial f_{i}\p{y}, \\ &\p{u_{i}}_{i\in\IndexOp} \in \prod_{i\in\IndexOp}G_{i}\p{y}, \\ &\sum_{i=1}^{m} u_{i} = 0, \\ &\hat{\bu} = \p{u_{1},\ldots,u_{m-1}}, \\ &\bFcn=\p{\bfcn_{i}\p{y}}_{i\in\IndexFunc} \end{aligned} },\end{aligned}\end{split}\]

where \(\hat{\bu}^{\star}\) is void when \(m=1\). In particular, \(y^{\star}\) in (5.1) is a solution to (2.1).

The three subpages below are organized as follows. Page 5.1 introduces a technical SDP primitive. Pages 5.2 and 5.3 then build on that primitive. The actual Lyapunov analyses, together with their corresponding convergence conclusions, are presented in pages 5.2 and 5.3.