Control Theory

Motivation

In many dynamic decision problems the criterion an agent uses today is not the one it will use tomorrow. The standard example is non-exponential discounting: if a payoff received $t$ periods from now is weighted by $\delta(t)$ and $\delta$ is not geometric, then the plan that is optimal from today's point of view will be abandoned by the agent's future selves. Such problems are called time-inconsistent, and since Strotz (1955) the usual response is to look not for an optimal plan but for an equilibrium: a plan that no future self wants to deviate from, given that all later selves follow it.

Huang and Zhou (arXiv:1809.09243v3, Math. Oper. Res. 2021) study this for finite-state Markov chains, mainly in continuous time. Section 5 of their paper turns to discrete time. On a finite horizon a discrete-time equilibrium is built by backward induction; on an infinite horizon there is no last period to start from, and, as the authors note, "little is known about the existence and characterization of equilibria, even in discrete time" (p. 15). Their Theorem 5.1 gives a general existence result for this case. This mission formalizes it.

Setting

Let $S=\{1,\dots,N\}$ and $\bar{\mathbb N}=\{0,1,2,\dots\}$. A time-homogeneous Markov chain $X=(X_t)_{t\in\bar{\mathbb N}}$ on $S$ is controlled by choosing its transition matrix $u=(u_{ij})$; the $i$-th row $u_i$ is the distribution of $X_{t+1}$ given $X_t=i$. Rows live in the probability simplex

$$\mathfrak P=\Big\{\alpha\in\mathbb R^N_+:\ \sum_i\alpha_i=1\Big\}. \qquad (5.1)$$

For each state $i$ a set $\mathcal A_i\subseteq\mathfrak P$ of admissible rows is given, and $\mathcal A=\{u\in\mathbb R^{N\times N}: u_i\in\mathcal A_i\ \forall i\}$.

A payoff $\kappa:\bar{\mathbb N}\times S\times\mathfrak P\to\mathbb R$ is continuous, and $\kappa(t,i,\alpha)$ is the reward $t$ periods from now when the chain is at $i$ and uses row $\alpha$. The dependence on $t$, the time difference from the present, is what makes the problem time-inconsistent. It is assumed that

$$\sum_{t=0}^\infty\ \sup_{(i,\alpha)\in S\times\mathfrak P}|\kappa(t,i,\alpha)|<\infty. \qquad (5.2)$$

The value of $u$ from state $i$ is $V(i,u)=\mathbb E_{i,u}\big[\sum_{t\ge0}\kappa(t,X_t,u_{X_t})\big]$, and $H_j(u)=\mathbb E_{j,u}\big[\sum_{t\ge0}\kappa(t+1,X_t,u_{X_t})\big]$ is the same with the clock shifted by one.

For $u,u^*\in\mathcal A$ the concatenation $u\otimes_1u^*$ uses $u$ for the step at time $0$ and $u^*$ for every later step. A matrix $u^*\in\mathcal A$ is an equilibrium (Definition 5.1) if

$$V(i,u^*)\ \ge\ V(i,u\otimes_1u^*)\qquad\text{for all }(i,u)\in S\times\mathcal A:$$

the self at time $0$ cannot gain by a one-step deviation, given that all later selves use $u^*$.

Formalization targets

Goal: Theorem 5.1 (p. 16)

If every $\mathcal A_i$ is nonempty, convex and closed and every $\kappa(0,i,\cdot)$ is concave on $\mathfrak P$, then

$$\exists\,u^*\in\mathcal A\quad\text{with}\quad V(i,u^*)\ge V(i,u\otimes_1u^*)\ \ \forall(i,u)\in S\times\mathcal A.$$

Milestones (proof of Theorem 5.1, Appendix B.1)

1. (5.4), p. 15: the one-step decomposition

$$V(i,u\otimes_1u^*)=\kappa(0,i,u_i)+\sum_{j=1}^N H_j(u^*)\,u_{ij}.$$

2. Continuity of $h$, p. 27: for each $j$, $u\mapsto H_j(u)$ is continuous on $\mathcal A$.
3. Best response, p. 27: the correspondence $\Phi(u)=\{w\in\mathcal A: w\in\arg\max_{u'\in\mathcal A}V(i,u'\otimes_1u)\ \forall i\}$ has nonempty, closed, convex values and is upper semicontinuous on $\mathcal A$.
4. Kakutani's fixed-point theorem (already proved on the platform, referenced).

Significance

The result. Theorem 5.1 says that infinite-horizon, discrete-time, finite-state time-inconsistent control always admits an equilibrium under convexity and concavity alone: no discounting structure, no stationarity of $\kappa$ in $t$, and no compactness beyond what $\mathfrak P$ provides. Remark 5.2 of the paper shows that concavity of $\kappa(0,i,\cdot)$ cannot simply be dropped: with strictly convex time-$0$ payoffs, a two-state example has no equilibrium. The discrete-time model is also the bridge to the continuous-time theory: Theorem 5.2 of the same paper (a companion mission) shows that limits of equilibria of time-discretizations are weak equilibria in continuous time.

Formalizing it. The result is proved on paper in one page. The formalization produces a machine-checked existence theorem whose definitions make the probabilistic content explicit (the value is written through the marginals $(u^t)_{ij}$ of the chain), together with a reusable decomposition (5.4) and continuity of the shifted value $H$ in the transition matrix. None of this is formalized elsewhere on the platform; Kakutani's theorem, the one external ingredient, is.

Difficulty

Backward induction, the standard construction of discrete-time equilibria, has no starting point on an infinite horizon, so existence cannot be obtained by a recursion. The value $H_j(u)$ is an infinite sum of products of matrix powers $(u^t)_{jk}$ with $\kappa(t+1,k,u_k)$, and its regularity in the transition matrix $u$ is not automatic: each term is continuous, but passing limits through the sum, and exchanging it with the finite sum over states in (5.4), needs the uniform tail control of (5.2) combined with the stochasticity of every power $u^t$. Without concavity of $\kappa(0,i,\cdot)$ the statement fails (Remark 5.2, p. 16, gives a two-state counterexample), so any argument must use it. Finally, the referenced fixed-point theorem is stated on Euclidean space, while the controls are $N\times N$ matrices.

Formalization scope

• States are Fin N (state $k$ of the paper is index $k-1$); rows are Fin N → ℝ; transition matrices are Matrix (Fin N) (Fin N) ℝ with the product topology.
• Expectations are written through the one-dimensional marginals of the chain: $V(i,u)=\sum_t\sum_j(u^t)_{ij}\kappa(t,j,u_j)$, $H_i(u)=\sum_t\sum_j(u^t)_{ij}\kappa(t+1,j,u_j)$, and $V(i,u\otimes_1u^*)=\kappa(0,i,u_i)+\sum_t\sum_j(u(u^*)^t)_{ij}\kappa(t+1,j,u^*_j)$. This is Fubini plus the marginal laws of a finite chain; no Markov process is constructed. The concatenated value is defined from the process, not by (5.4), so (5.4) is a genuine statement.
• The infinite sums are tsums. A tsum of a non-summable family is $0$ in Lean; here (5.2) and the stochasticity of $u^t$ make every sum absolutely convergent, and no summability hypothesis appears in any statement.
• The standing assumptions of §5 are one structure: $\mathcal A_i\subseteq\mathfrak P$; $\kappa(t,i,\cdot)$ continuous on $\mathfrak P$ for all $t,i$ (continuity on $\bar{\mathbb N}\times S\times\mathfrak P$, both first factors being discrete); (5.2) as a summable majorant $b_t\ge|\kappa(t,i,\alpha)|$ on $\mathfrak P$.
• Added hypothesis: every $\mathcal A_i$ is nonempty. The page's "convex and closed" allows $\mathcal A_i=\emptyset$, in which case $\mathcal A=\emptyset$ and no equilibrium exists.
• Concavity of $\kappa(0,i,\cdot)$ is assumed on all of $\mathfrak P$, as on the page; closedness of $\mathcal A_i$ gives compactness because $\mathfrak P$ is compact, and no compactness is assumed.
• Upper semicontinuity of $\Phi$ is stated with sequences, as on the page.
• A trivializing formalization would define $V(i,u\otimes_1u^*)$ by formula (5.4), or add summability or equilibrium-shaped hypotheses to the goal; none of these is done.
• Infrastructure a complete development needs: bounds on entries of products of stochastic matrices, dominated (Weierstrass M-test) continuity of tsums, a linear homeomorphism between Matrix (Fin N) (Fin N) ℝ and EuclideanSpace ℝ (Fin (N*N)) to apply the referenced Kakutani theorem. The first two are reusable for any finite-state Markov reward model. Proofs of the milestones in any order are welcome.

Selected references

• Y.-J. Huang and Z. Zhou, Strong and Weak Equilibria for Time-Inconsistent Stochastic Control in Continuous Time, Math. Oper. Res. 46(2), 2021; read as arXiv:1809.09243v3. https://arxiv.org/abs/1809.09243 , https://doi.org/10.1287/moor.2020.1066
• S. Kakutani, A generalization of Brouwer's fixed point theorem, Duke Math. J. 8(3), 457–459, 1941. https://doi.org/10.1215/S0012-7094-41-00838-4
• R. H. Strotz, Myopia and inconsistency in dynamic utility maximization, Rev. Econ. Stud. 23(3), 165–180, 1955. https://doi.org/10.2307/2295722

Motivation

Data-driven control asks for a controller computed directly from measured trajectories of an unknown system, without first identifying a model. When the measurements are corrupted by noise, many systems explain the same data, and a controller is acceptable only if it works for all of them. Van Waarde, Camlibel, Eising and Trentelman (arXiv:2203.12959) model the noise by a quadratic matrix inequality (QMI). The set of systems consistent with the data is then itself the solution set of a QMI, and the design question becomes whether one QMI implies another. Their Theorem 5.1 gives a necessary and sufficient linear matrix inequality (LMI) for the existence of a common stabilizing controller, with no rank or Slater-type assumption on the data. It improves van Waarde, Camlibel, Mesbahi, IEEE TAC 2022, Thm. 14, which needed a generalized Slater condition.

The LMI of Theorem 5.1 has size $4n+m+1$ and $\tfrac{n(n+1)}{2}+nm+1$ unknowns. Section 5.2 of the paper removes the controller variable: Theorem 5.3 gives an LMI of size $4n+1$ in the Lyapunov matrix $P$ and one scalar $\beta$, and then writes a stabilizing controller as a closed-form expression in $P$ and the data. This mission formalizes that reduction and the Section 3 results on QMI solution sets that it rests on.

Setting

All matrices are real. $\mathbb S^k$ is the set of symmetric $k\times k$ matrices, $A\ge 0$ ($A>0$) means symmetric positive semidefinite (definite), and $A^\dagger$ is the Moore–Penrose pseudo-inverse. For $\Pi\in\mathbb S^{q+r}$, partitioned with $\Pi_{11}$ of size $q\times q$ and $\Pi_{22}$ of size $r\times r$,

$$\mathcal Z_r(\Pi) = \Big\{Z\in\mathbb R^{r\times q} : \begin{bmatrix} I_q\\ Z\end{bmatrix}^\top\Pi\begin{bmatrix} I_q\\ Z\end{bmatrix}\ge 0\Big\},$$

and $\mathcal Z_r^+(\Pi)$ is the same set with $>0$. The generalized Schur complement is $\Pi\,|\,\Pi_{22} = \Pi_{11}-\Pi_{12}\Pi_{22}^\dagger\Pi_{21}$, and $\boldsymbol\Pi_{q,r}$ is the class of $\Pi\in\mathbb S^{q+r}$ with $\Pi_{22}\le 0$, $\Pi\,|\,\Pi_{22}\ge 0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$. For $W\in\mathbb R^{q\times p}$, $\mathcal Z_r(\Pi)W = \{ZW : Z\in\mathcal Z_r(\Pi)\}$ and $\Pi_W = \mathrm{diag}(W,I_r)^\top\,\Pi\,\mathrm{diag}(W,I_r)$.

Data. An unknown system $x(t+1) = A_sx(t)+B_su(t)+w(t)$ produces $X = [x(0)\cdots x(T)]$ and $U_- = [u(0)\cdots u(T-1)]$; $X_-$ and $X_+$ are the first and last $T$ columns of $X$. The noise matrix $W_- = [w(0)\cdots w(T-1)]$ is unknown but satisfies $W_-^\top\in\mathcal Z_T(\Phi)$ for a given $\Phi\in\boldsymbol\Pi_{n,T}$. The consistent systems are

$$\Sigma = \{(A,B) : X_+ = AX_-+BU_-+W_-\ \text{for some}\ W_-^\top\in\mathcal Z_T(\Phi)\}.$$

The data are informative for quadratic stabilization if there are $K$ and $P>0$ with $P-(A+BK)P(A+BK)^\top>0$ for all $(A,B)\in\Sigma$.

Formalization targets

Goal: Theorem 5.3

With $\Theta = \Phi_{12}+X_+\Phi_{22}$ and $V = [X_-;\,U_-]$: the data are informative if and only if some $P>0$, $\beta>0$ satisfy

$$P-\beta I-[I\ X_+]\Phi[I\ X_+]^\top+\Theta V^\top(V\Phi_{22}V^\top)^\dagger V\Theta^\top\ge 0,\qquad \begin{bmatrix}P-\beta I&0\\0&-P\end{bmatrix}-\begin{bmatrix}I&X_+\\0&-X_-\end{bmatrix}\Phi\begin{bmatrix}I&X_+\\0&-X_-\end{bmatrix}^\top\ge 0,$$

and then

$$K = \big(U_-(\Phi_{22}+\Theta^\top\Gamma^\dagger\Theta)X_-^\top\big)\big(X_-(\Phi_{22}+\Theta^\top\Gamma^\dagger\Theta)X_-^\top\big)^\dagger,\qquad \Gamma = P-\beta I-[I\ X_+]\Phi[I\ X_+]^\top,$$

stabilizes every $(A,B)\in\Sigma$. Under $\Phi_{22}<0$ and $\operatorname{rank}V = n+m$ the same holds with strict inequalities, $\beta = 0$, and $(V\Phi_{22}V^\top)^{-1}$. The goal states all four parts.

Milestones

1. Lemma A.1: $A^\top A\le B^\top B$ iff $A = SB$ with $S^\top S\le I$ (and the strict version), with $S = AB^\dagger$.
2. Lemma A.2: the solutions of $AM = B$.
3. Theorem 3.3: all solutions of a QMI, $Z = -\Pi_{22}^\dagger\Pi_{21}+((-\Pi_{22})^\dagger)^{1/2}S(\Pi|\Pi_{22})^{1/2}+(I-\Pi_{22}^\dagger\Pi_{22})T$.
4. Theorems 3.4 and 3.5: $\mathcal Z_r(\Pi)W = \mathcal Z_r(\Pi_W)$ and its strict analogue.
5. Corollaries 3.6 and 3.7: a QMI solution with $ZW = Y$ exists iff $Y\in\mathcal Z_r(\Pi_W)$.
6. Theorem 5.1: informativity iff the LMI in $(P,L,\beta)$ is feasible, with $K = LP^{-1}$.

Significance

Theorem 5.3 separates the computation of a Lyapunov matrix from the computation of the controller. The LMI drops from size $4n+m+1$ to $4n+1$ and loses the $nm$ entries of $L$. A controller then follows from $P$ by one explicit formula, with no second optimization. The noise class $\boldsymbol\Pi_{n,T}$ covers energy bounds, bounds on individual samples, noise confined to a known subspace, and exact data, so the result applies where earlier conditions requiring $\Phi_{22}<0$ or a Slater point fail.

The Section 3 results are general facts about QMIs: an explicit parameterization of all solutions, also when the solution set is unbounded, and the identification of the image of a solution set under a linear map. They are reusable wherever QMIs appear in robust control: Petersen's lemma, the elimination lemma, dissipativity analysis.

All results are proved in the paper, with the exception of the proof of Theorem 3.5, which is only described as similar to that of Theorem 3.4. None is formalized. The work here is the formal development: a pseudo-inverse calculus for real matrices, generalized Schur complements, matrix square roots in the Loewner order, and the block-matrix identities of Section 5.

Difficulty

The QMI reformulation of the stabilization problem is short. The difficulty lies in degenerate matrices. $\Pi_{22}$ is typically singular, so every step works with pseudo-inverses, kernel inclusions and generalized Schur complements, and identities that are routine for invertible blocks need range conditions. The closed-form gain (5.10) comes from a block pseudo-inverse formula for a positive semidefinite matrix whose blocks may all be singular, and checking it requires tracking which ranges contain which. The strict statements need a separate argument: a strict inequality $A^\top A<B^\top B$ does not pass to $W^\top A^\top AW<W^\top B^\top BW$ without full column rank of $W$, which is why Theorem 3.5 and Corollary 3.7 assume it.

The first idea, to eliminate $L$ from (5.5) by completing the square, runs into the same singular blocks: the minimizing $L$ involves pseudo-inverses of data-dependent matrices whose ranges are not controlled by the LMI alone.

Formalization scope

Lean conventions:

• Index sets are arbitrary finite types, so $q$, $r$, $p$ are cardinalities. The data dimensions $n$, $m$, $T$ are natural numbers, with $X$ an $n\times(T+1)$ matrix.
• $A\ge 0$ is Mathlib's PosSemidef (which includes symmetry); $A>0$ is PosDef.
• $A^\dagger$ is defined as the matrix satisfying the four Penrose conditions, which exists and is unique. Mathlib's A⁻¹, which returns $0$ on singular matrices, appears only in (5.11a) and in $K = LP^{-1}$, where the matrices are invertible.
• Square roots are CFC.sqrt in the Loewner order. Kernel inclusions are stated on vectors. Full column rank of $W\in\mathbb R^{q\times p}$ is rank W = p.

The statements of Theorems 5.1 and 5.3 carry the hypothesis that the data were generated by some $(A_s,B_s)$, i.e. $\Sigma\neq\emptyset$; the paper assumes this when it says the data are generated by (2.1) with noise model (2.3). Without it, informativity holds vacuously and the equivalences fail. "Stabilizing gain" is asserted with the $P$ of the LMI: the Lyapunov inequality $P-(A+BK)P(A+BK)^\top>0$ and $(A+BK)^k\to 0$ for every $(A,B)\in\Sigma$. Corollaries 3.6 and 3.7 print the hypothesis $\ker\Pi_{22}\subseteq\ker\Pi_{21}$, which is dimensionally impossible; it is read as $\ker\Pi_{22}\subseteq\ker\Pi_{12}$. The printed dimensions in Lemma A.2 are corrected to those its formula requires.

A formalization in which Σ may be empty, or in which $A^\dagger$ is replaced by the total inverse, would make the goal vacuous or false. Both are ruled out above.

Theorem 5.1 is restated here as a milestone. It is also the goal of the companion mission IV, and solvers may prove it there.

Reusable infrastructure is welcome as separate contributions: uniqueness and the basic identities of the matrix pseudo-inverse; the generalized Schur complement criterion for positive semidefiniteness of a block matrix; Douglas-type factorization (Lemma A.1); square roots of positive semidefinite matrices commuting with pseudo-inverses.

Selected references

• H. J. van Waarde, M. K. Camlibel, J. Eising, H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023; preprint arXiv:2203.12959v3 (the version cited here). https://arxiv.org/abs/2203.12959
• H. J. van Waarde, M. K. Camlibel, M. Mesbahi, From noisy data to feedback controllers: nonconservative design via a matrix S-lemma, IEEE Trans. Automat. Control, 67 (2022), pp. 162–175. https://doi.org/10.1109/TAC.2020.3047577
• H. J. van Waarde, J. Eising, H. L. Trentelman, M. K. Camlibel, Data informativity: a new perspective on data-driven analysis and control, IEEE Trans. Automat. Control, 65 (2020), pp. 4753–4768. https://doi.org/10.1109/TAC.2020.2966717
• D. S. Bernstein, Matrix Mathematics, 2nd ed., Princeton University Press, 2009. https://doi.org/10.1515/9781400833344

Motivation

Data-driven control asks for a controller computed directly from measured trajectories of an unknown system, without first identifying a model. When the measurements are corrupted by unknown process noise, many systems explain the same data, and a controller designed from the data alone is only trustworthy if it stabilizes every one of them. Van Waarde, Camlibel, Eising and Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) show that this robust design problem is an implication between two quadratic matrix inequalities (QMIs), and they develop matrix versions of Yakubovich's S-lemma and of Finsler's lemma to decide such implications by a linear matrix inequality (LMI).

Timeline:

• 1971: Yakubovich proves the S-lemma for one quadratic constraint under a Slater condition (English translation 1977; see the Pólik–Terlaky survey).
• 2022: van Waarde, Camlibel and Mesbahi (IEEE Trans. Automat. Control 67, pp. 162–175, Thms. 13–14) give an LMI condition for informativity for quadratic stabilization from noisy data, assuming $\Phi_{22}<0$ and a generalized Slater condition.
• 2023: the present paper removes the Slater condition and the definiteness of $\Phi_{22}$: Theorem 5.1 holds for every noise model in the class $\boldsymbol\Pi_{n,T}$, including exact measurements and noise confined to a subspace.

Setting

All matrices are real. $\mathbb{S}^k$ is the set of symmetric $k\times k$ matrices; $A\geqslant 0$ ($A>0$) means $A$ is symmetric positive semidefinite (definite), and $A\leqslant 0$ means $-A\geqslant 0$.

QMI solution sets. For $\Pi\in\mathbb{S}^{q+r}$ partitioned with $\Pi_{11}\in\mathbb{S}^q$, $\Pi_{22}\in\mathbb{S}^r$,

$$\mathcal Z_r(\Pi)=\Big\{Z\in\mathbb{R}^{r\times q}:\begin{bmatrix}I_q\\Z\end{bmatrix}^{\!\top}\Pi\begin{bmatrix}I_q\\Z\end{bmatrix}\geqslant 0\Big\},$$

with $\mathcal Z_r^+(\Pi)$ and $\mathcal Z_r^0(\Pi)$ defined by "$>0$" and "$=0$". The generalized Schur complement is $\Pi\,|\,\Pi_{22}=\Pi_{11}-\Pi_{12}\Pi_{22}^\dagger\Pi_{21}$, with $\dagger$ the Moore–Penrose pseudo-inverse, and $\boldsymbol\Pi_{q,r}$ is the class of $\Pi\in\mathbb{S}^{q+r}$ with $\Pi_{22}\leqslant 0$, $\Pi\,|\,\Pi_{22}\geqslant 0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$.

Data. The unknown system is $x(t+1)=A_sx(t)+B_su(t)+w(t)$ with $x,w\in\mathbb{R}^n$, $u\in\mathbb{R}^m$. The measured data are $X=[x(0)\ \cdots\ x(T)]$ and $U_-=[u(0)\ \cdots\ u(T-1)]$; $X_-$ and $X_+$ are the first and last $T$ columns of $X$. The unknown noise $W_-=[w(0)\ \cdots\ w(T-1)]$ satisfies $W_-^\top\in\mathcal Z_T(\Phi)$ for a given $\Phi\in\boldsymbol\Pi_{n,T}$. The systems compatible with the data form

$$\Sigma=\{(A,B): X_+=AX_-+BU_-+W_- \text{ for some } W_- \text{ with } W_-^\top\in\mathcal Z_T(\Phi)\},$$

and $(A_s,B_s)\in\Sigma$. The data are informative for quadratic stabilization (Definition 2.1) if some $K$ and $P>0$ satisfy $P-(A+BK)P(A+BK)^\top>0$ for all $(A,B)\in\Sigma$.

Formalization targets

Goal: Theorem 5.1

Let $\mathcal L_\beta(P,L)$ be the $(n+n+m+n)$-square matrix

$$\begin{bmatrix}P-\beta I&0&0&0\\0&-P&-L^\top&0\\0&-L&0&L\\0&0&L^\top&P\end{bmatrix}-\begin{bmatrix}I&X_+\\0&-X_-\\0&-U_-\\0&0\end{bmatrix}\Phi\begin{bmatrix}I&X_+\\0&-X_-\\0&-U_-\\0&0\end{bmatrix}^{\!\top}.$$

For $\Phi\in\boldsymbol\Pi_{n,T}$ and data generated by the system:

(a) the data are informative if and only if $\exists\,P>0,\ L,\ \beta>0$ with $\mathcal L_\beta(P,L)\geqslant 0$ (5.5);

(b) if moreover $\Phi_{22}<0$ and $\operatorname{rank}[X_-;U_-]=n+m$, the data are informative if and only if $\exists\,P>0,\ L$ with $\mathcal L_0(P,L)>0$ (5.6);

(c) whenever (5.5) or (5.6) holds, $K=LP^{-1}$ satisfies the Lyapunov inequality with that $P$ and makes $A+BK$ Schur stable for every $(A,B)\in\Sigma$.

Milestones

The vector S-lemma, strict S-lemma and Finsler's lemma (Lemmas 4.1–4.3); the completion and lifting lemmas 4.4–4.5; the reduction of matrix inclusions to vector implications (Theorem 4.6); the matrix S-lemmas

$$\mathcal Z_r(N)\subseteq\mathcal Z_r(M)\iff\exists\,\alpha\geqslant 0:\ M-\alpha N\geqslant 0,\qquad \mathcal Z_r(N)\subseteq\mathcal Z_r^+(M)\iff\exists\,\alpha\geqslant 0,\ \beta>0:\ M-\alpha N\geqslant\begin{bmatrix}\beta I&0\\0&0\end{bmatrix}$$

(Theorems 4.7, 4.10–4.12, Corollary 4.13); and the three claims of §5.1 that put Theorem 5.1 in the form of Corollary 4.13: $\Sigma=\mathcal Z_{n+m}(N)$, the Lyapunov inequality is $[A\ B]^\top\in\mathcal Z^+_{n+m}(M)$, and $N\in\boldsymbol\Pi_{n,n+m}$, $M_{22}\leqslant 0$.

Significance

Theorem 5.1(a) is an exact test, with no rank condition on the data and no Slater condition on the noise model, for the existence of one state-feedback gain with a common quadratic Lyapunov function that stabilizes every system consistent with noisy data. The test is a semidefinite feasibility problem in $(P,L,\beta)$ and returns the controller $K=LP^{-1}$. It covers energy bounds, per-sample bounds, sample-covariance bounds, noise in a known subspace and exact data within one statement, and its matrix S-lemmas are the tools reused in the paper's further results (the reduced LMI and explicit gain of §5.2, Petersen's lemma in §4.5).

None of these results has a machine-checked proof. Mathlib has the Loewner order, positive (semi)definiteness and spectral theory of symmetric matrices, but no S-lemma, no Finsler lemma, no Moore–Penrose pseudo-inverse for matrices and no theory of QMI solution sets. A formalization would supply these as reusable linear-algebra results and would certify the design rule $K=LP^{-1}$.

Difficulty

The "if" directions are direct computations: multiply out a Schur complement. The difficulty is in the "only if" directions. The S-lemma's converse relies on the hidden convexity of the joint range of two quadratic forms (Dines' theorem), which is not a consequence of finite-dimensional convex duality alone. Passing from matrices $Z$ to vectors requires Lemma 4.5, which builds a full matrix solution of the QMI from one vector; it uses the pseudo-inverse factorization of $N$ and fails without $\ker N_{22}\subseteq\ker N_{12}$. In Theorem 4.11 the existence of the margin $\beta>0$ comes from a compactness argument on an unbounded solution set, after splitting off the kernel of $N_{22}$. The obvious approach, applying the strict matrix S-lemma (Theorem 4.10) directly, does not work because $N_{22}$ is only semidefinite in the noise models of interest.

Formalization scope

Matrices are Matrix ι ι ℝ over finite index types; a matrix in $\mathbb{S}^{q+r}$ is indexed by ι ⊕ κ, and block matrices are Matrix.fromBlocks / Matrix.fromRows. $\geqslant 0$ and $>0$ are Mathlib's PosSemidef and PosDef, which include symmetry, as the paper's §1.1 convention does. The pseudo-inverse is defined as the unique matrix satisfying the four Penrose conditions, not Matrix.inv, which returns $0$ on singular matrices. "Stabilizing gain for all of $\Sigma$" is stated as the Lyapunov inequality with the LMI's $P$ together with $(A+BK)^k\to 0$.

The following are added or made explicit:

• the hypothesis that the data are generated by the system ($\Sigma\neq\emptyset$). Without it informativity holds vacuously and the goal is false;
• $q\geqslant 1$ in the "only if" parts of Theorem 4.12 and Corollary 4.13. These parts fail at $q=0$, e.g. for $N=[0]$, $M=[-1]$, and the paper's proofs choose a nonzero vector of $\mathbb{R}^q$;
• $n=k+1$ in Lemma 4.4, to avoid natural-number subtraction.

The goal adds no hypothesis $n\geqslant 1$. A formalization in which $\Sigma$ may be empty, or in which the pseudo-inverse is a junk value, would be trivial or false, and the definitions rule both out.

Contributions are welcome for the pseudo-inverse API (existence, uniqueness, $\ker$ identities), the S-lemma and Finsler's lemma (reusable beyond this mission), and the Schur-complement factorizations (3.2)–(3.4). Platform items ConvexOptimization.s_procedure (inhomogeneous S-procedure) and ConvexOptimization.field_of_values_psd_witness (Dines) are natural proof tools for Lemma 4.1.

Selected references

• H. J. van Waarde, M. K. Camlibel, J. Eising, H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023. arXiv:2203.12959v3. https://arxiv.org/abs/2203.12959
• H. J. van Waarde, M. K. Camlibel, M. Mesbahi, From noisy data to feedback controllers: nonconservative design via a matrix S-lemma, IEEE Trans. Automat. Control 67 (2022), pp. 162–175.
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007). https://doi.org/10.1137/S003614450444614X
• V. A. Yakubovich, S-procedure in nonlinear control theory, Vestnik Leningrad Univ. Math. 4 (1977), pp. 73–93 (English translation).
• S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777

Motivation

Quadratic matrix inequalities (QMIs) describe sets of matrices rather than sets of vectors. They appear whenever an unknown matrix is constrained by a quadratic bound: in robust control, where an uncertain block of a system is only known to lie in a norm ball or a sector, and in data-driven control, where the system matrices $(A, B)$ of a linear system $x(t+1) = Ax(t) + Bu(t) + w(t)$ are unknown and the measured data, corrupted by noise satisfying a quadratic bound, only pin them down to a set defined by a QMI.

H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) develop a systematic theory of such sets, culminating in matrix versions of the S-lemma and of Finsler's lemma and in data-based stabilization tests. Before any of that can be used, one has to know when the set of matrices satisfying a QMI is nonempty, convex, bounded, has interior points, or contains strict and boundary solutions. Section 3.1 of the paper answers these questions in terms of the blocks of the matrix defining the QMI. This mission formalizes that section, Theorem 3.2, together with the Schur complement identities (3.2)–(3.4) on which it rests.

Setting

All matrices are real. Fix integers $q, r \ge 0$. For a matrix $A$, the Moore–Penrose pseudo-inverse $A^\dagger$ is the unique matrix $X$ with

$$AXA = A,\quad XAX = X,\quad (AX)^\top = AX,\quad (XA)^\top = XA.$$

$\mathbb S^n$ is the set of symmetric $n\times n$ matrices; for $A \in \mathbb S^n$, $A \ge 0$ and $A > 0$ mean positive semidefinite and positive definite, $A \le 0$, $A < 0$ the negative versions, and $A \ge B$ means $A - B \ge 0$ (the Loewner order).

A matrix $\Pi \in \mathbb S^{q+r}$ is always partitioned as

$$\Pi = \begin{bmatrix}\Pi_{11} & \Pi_{12}\\ \Pi_{21} & \Pi_{22}\end{bmatrix},\qquad \Pi_{11}\in\mathbb R^{q\times q},\ \Pi_{22}\in\mathbb R^{r\times r},\ \Pi_{21} = \Pi_{12}^\top .$$

For $Z \in \mathbb R^{r\times q}$ the QMI is

$$\begin{bmatrix} I_q\\ Z\end{bmatrix}^\top \Pi \begin{bmatrix} I_q\\ Z\end{bmatrix} \ge 0,$$

with solution set $\mathcal Z_r(\Pi)$. Replacing $\ge 0$ by $> 0$ or $= 0$ gives the sets $\mathcal Z_r^+(\Pi)$ of strict solutions and $\mathcal Z_r^0(\Pi)$ of solutions of the quadratic matrix equation. The generalized Schur complement is

$$\Pi\,|\,\Pi_{22} := \Pi_{11} - \Pi_{12}\Pi_{22}^\dagger\Pi_{21},$$

and the class $\boldsymbol\Pi_{q,r}$ (equation (3.5) of the paper) consists of the $\Pi \in \mathbb S^{q+r}$ with

$$\Pi_{22} \le 0,\qquad \Pi\,|\,\Pi_{22} \ge 0,\qquad \ker\Pi_{22} \subseteq \ker\Pi_{12}.$$

In Lean these are pinv, qmiForm, ZSet, ZPlus, ZZero, schur and InPi in the namespace QuadMatIneq.Basic.

Formalization targets

Goal: Theorem 3.2

For $\Pi \in \boldsymbol\Pi_{q,r}$:

• (a) $\mathcal Z_r(\Pi)$ is nonempty and convex;
• (b) for $q \ge 1$, $\mathcal Z_r(\Pi)$ is bounded if and only if $\Pi_{22} < 0$;
• (c) $\mathcal Z_r(\Pi)$ has nonempty interior if and only if $\Pi_{22} = 0$ or $\Pi\,|\,\Pi_{22} > 0$;
• (d) $\mathcal Z_r^+(\Pi) \ne \varnothing$ if and only if $\Pi\,|\,\Pi_{22} > 0$;
• (e) $\mathcal Z_r^0(\Pi) \ne \varnothing$ if and only if $\operatorname{rank}\Pi_{22} \ge \operatorname{rank}(\Pi\,|\,\Pi_{22})$.

Milestones

For $\Pi \in \mathbb S^{q+r}$ with $\Pi_{22} \le 0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$:

• (3.2): $\ker\Pi_{22}\subseteq\ker\Pi_{12} \iff \Pi_{12}\Pi_{22}\Pi_{22}^\dagger = \Pi_{12}$, and

$$\Pi = \begin{bmatrix} I_q & \Pi_{12}\Pi_{22}^\dagger\\ 0 & I_r\end{bmatrix}\begin{bmatrix}\Pi\,|\,\Pi_{22} & 0\\ 0 & \Pi_{22}\end{bmatrix}\begin{bmatrix} I_q & 0\\ \Pi_{22}^\dagger\Pi_{21} & I_r\end{bmatrix};$$

• (3.3): $\begin{bmatrix} I_q\\ Z\end{bmatrix}^\top \Pi \begin{bmatrix} I_q\\ Z\end{bmatrix} = \Pi\,|\,\Pi_{22} + (Z + \Pi_{22}^\dagger\Pi_{21})^\top\Pi_{22}(Z + \Pi_{22}^\dagger\Pi_{21})$;
• (3.4): $\Pi\,|\,\Pi_{22}$ is the value at $Z = -\Pi_{22}^\dagger\Pi_{21}$ and dominates the value at every $Z$ in the Loewner order;
• the claim after (3.4): $\mathcal Z_r(\Pi) \ne\varnothing$ if and only if $\Pi\,|\,\Pi_{22}\ge 0$;
• Theorem 3.2(b), (c), (e) as separate items.

Significance

Theorem 3.2 turns geometric questions about a set of matrices into finite checks on the blocks of $\Pi$: semidefiniteness, definiteness, vanishing and a rank comparison. In the data-driven setting of the paper, $\mathcal Z_r(\Pi)$ (after transposition) is the set of noise samples, and hence of systems, consistent with the data; part (b) decides when that set is compact, part (c) when it has interior, and (a) guarantees convexity, which is what allows linear matrix inequalities to be used over it. The identities (3.2)–(3.4) are used throughout the rest of the paper, in the matrix S-lemma, the matrix Finsler lemma and the parametrization of solution sets.

The result and its proof appear in the paper; this mission produces machine-checked versions. Mathlib has the Schur complement for invertible blocks and positive semidefiniteness, but no Moore–Penrose pseudo-inverse for matrices and nothing on QMI solution sets. To the knowledge of this mission no formalization of these statements exists.

Difficulty

The obvious argument is the classical Schur complement, which requires $\Pi_{22}$ to be invertible. Here $\Pi_{22}$ is only negative semidefinite, and the singular case is exactly where the interesting behaviour lives: the solution set is unbounded precisely when $\Pi_{22}$ has a kernel, and $\Pi_{22} = 0$ gives the whole space. Working with the pseudo-inverse requires the range and kernel identities of $\Pi_{22}^\dagger$ for a symmetric matrix and the kernel inclusion $\ker\Pi_{22}\subseteq\ker\Pi_{12}$ at every step. Part (c) needs a topological argument about the interior in $\mathbb R^{r\times q}$, and part (e) needs a factorization of one positive semidefinite matrix through another of possibly different size, which is a rank argument rather than an identity.

Formalization scope

• Matrices are indexed by arbitrary finite types: $\iota$ with $|\iota| = q$ and $\kappa$ with $|\kappa| = r$, so $\Pi$ is a matrix over $\iota \oplus \kappa$ and its blocks are Mathlib's toBlocks₁₁, …, toBlocks₂₂. Nothing assumes $q, r \ge 1$ except part (b).
• $A^\dagger$ is defined by Classical.epsilon over the four Penrose conditions. Since a solution exists and is unique, this is the pseudo-inverse and not a default value; the total inverse A⁻¹, which is $0$ on singular matrices, is not used anywhere.
• $\ge 0$ and $> 0$ are Mathlib's PosSemidef and PosDef, which include symmetry, matching the paper's convention that definiteness is only asserted for symmetric matrices. $\Pi\in\mathbb S^{q+r}$ is IsHermitian.
• Kernel inclusions are written $\forall v,\ \Pi_{22}v = 0 \Rightarrow \Pi_{12}v = 0$.
• "Bounded" means entrywise bounded, which is equivalent to boundedness in any norm on $\mathbb R^{r\times q}$. The interior is taken in $\mathbb R^{r\times q}$ with its Euclidean topology, not relative to an affine hull.
• Part (b) carries the hypothesis $q \ge 1$. For $q = 0$ the space $\mathbb R^{r\times 0}$ is a single point, so the solution set is bounded for every $\Pi$, including those with singular $\Pi_{22}$, and (b) as printed fails. The other parts are stated without it and hold for $q = 0$ and for $r = 0$.
• The trivializing formalizations are excluded: the pseudo-inverse is not a junk inverse, the class $\boldsymbol\Pi_{q,r}$ is inhabited (e.g. $\Pi = \operatorname{diag}(1, -1)$ and $\Pi = \operatorname{diag}(1, 0)$ for $q = r = 1$), and the identities (3.2)–(3.4) are stated with the paper's exact block layouts.

Infrastructure needed and reusable beyond this mission: the existence and uniqueness of the matrix pseudo-inverse with its basic identities ($(A^\dagger)^\top = (A^\top)^\dagger$, $AA^\dagger$ is the orthogonal projector onto the range), and the generalized Schur complement identities. Contributions of these as separate lemmas are welcome.

Selected references

• H. J. van Waarde, M. K. Camlibel, J. Eising, H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023; preprint arXiv:2203.12959v3. https://arxiv.org/abs/2203.12959
• D. S. Bernstein, Matrix Mathematics: Theory, Facts, and Formulas, 2nd ed., Princeton University Press, 2009 (reference [4] of the paper, for eigenvalue and pseudo-inverse facts). https://doi.org/10.1515/9781400833344
• F. Zhang (ed.), The Schur Complement and Its Applications, Springer, 2005. https://doi.org/10.1007/b105056

Motivation

Networks of identical dynamical systems coupled along a directed graph model power grids, sensor and robot swarms, neural populations and coupled oscillators. A basic control question is how to steer every node of such a network onto a prescribed reference trajectory by acting directly on only a few nodes. This is pinning control: feedback is injected at a small set of pinned vertices, and the coupling has to carry the reference signal to the rest of the network.

For undirected or strongly connected networks, criteria for pinning synchronization go back to Wang and Chen (2002) and Chen, Liu and Lu (2007), and the first mission of this series treats the strongly connected case of Yu, Chen, Lü and Kurths (2013). Many networks of interest are not strongly connected: information flows down a hierarchy of groups, and the minimal requirement for the reference to reach every node is that the network, with the reference added as a virtual leader, contains a directed spanning tree rooted at the leader. Section 4 of that paper gives a criterion for this general case that splits into one condition per strongly connected component. This mission formalizes that criterion, Theorem 4.5, with the lemmas its proof uses and three corollaries.

Setting

There are $N$ vertices with states $x_i(t)\in\mathbb R^n$. The coupling configuration matrix $G\in\mathbb R^{N\times N}$ has $G_{ij}\ge0$ for $i\ne j$, where $G_{ij}>0$ records a connection from vertex $j$ to vertex $i$, and zero row sums, $G_{ii}=-\sum_{j\ne i}G_{ij}$. Given a function $f:\mathbb R^n\times\mathbb R_+\to\mathbb R^n$, a coupling strength $c$, an inner coupling matrix $\Gamma\in\mathbb R^{n\times n}$ and pinning gains $d_i\ge0$ (vertex $i$ is pinned when $d_i>0$), the controlled network is

$$\dot x_i=f(x_i,t)+c\sum_{j=1}^N G_{ij}\Gamma x_j-c\,d_i\,\Gamma(x_i-s),\qquad i=1,\dots,N,$$

where the reference $s$ solves $\dot s=f(s,t)$. The network is globally synchronized when $x_i(t)-s(t)\to0$ for every vertex and every pair of solutions.

The nonlinearity is controlled by Assumption 1: there is a matrix $K$ with $(x-y)^{\mathsf T}(f(x,t)-f(y,t))\le(x-y)^{\mathsf T}K\Gamma(x-y)$ for all $x,y$ and $t\ge0$. Throughout §4 the paper also assumes that $K$ and $\Gamma$ commute, that $\Gamma$ is positive definite, and puts $\theta=\lambda_{\max}((K+K^{\mathsf T})/2)\ge0$.

The vertices split into strongly connected components $V_1,\dots,V_M$. In the Frobenius normal form the components are ordered so that no edge goes from a later component to an earlier one, which makes $G$ block lower triangular. For each component $j$ the mission uses three matrices:

• $\widetilde G_j$, the diagonal block of $G-\mathrm{diag}(d)$ on $V_j$;
• $A_j$, the within-component part of $G$ with zero row sums;
• $\widetilde\Pi_j=\mathrm{diag}(\Pi_j)$, where $\Pi_j$ is a positive vector with $\Pi_j^{\mathsf T}A_j=0$.

In Lean, component membership is a map blk : Fin N → Fin M, and Fin M carries the Frobenius order.

Formalization targets

Goal: Theorem 4.5

If, for every component $j$,

$$2\theta\widetilde\Pi_j+c\bigl(\widetilde\Pi_j\widetilde G_j+\widetilde G_j^{\mathsf T}\widetilde\Pi_j\bigr)<0, \tag{4.8}$$

then the controlled network with a directed spanning tree is globally synchronized.

Milestones

1. The θ bound (p. 1402). Commutation and $\Gamma>0$ turn Assumption 1 into $(x-y)^{\mathsf T}(f(x,t)-f(y,t))\le\theta(x-y)^{\mathsf T}\Gamma(x-y)$.
2. Lemma 2.13. The strict Schur complement test for a symmetric block matrix.
3. Lemma 4.4. If $\widetilde\Pi_j\widetilde G_j+\widetilde G_j^{\mathsf T}\widetilde\Pi_j<0$ on every diagonal block of a block lower-triangular $\overline G$, then positive block weights $\Delta_j$ exist with $\Delta\widetilde\Pi\overline G+\overline G^{\mathsf T}\widetilde\Pi\Delta<0$.
4. (4.10). Along solutions, $V=\sum_j\Delta_j\widetilde e_j^{\mathsf T}\widetilde\Pi_j\widetilde e_j$ satisfies $\dot V\le e^{\mathsf T}\{[\Delta\widetilde\Pi(c\overline G+\theta I_N)+(c\overline G+\theta I_N)^{\mathsf T}\widetilde\Pi\Delta]\otimes\Gamma\}e$.

Companions

• Corollary 4.7: the same conclusion under $\theta\widetilde\Pi_j+c(\overline A_j-\widetilde\Pi_jC_j-\widetilde\Pi_j\overline D_j)<0$, which separates the outer in-degrees $C_j$ from the pinning gains $\overline D_j$.
• Corollary 4.8 (i): an explicit coupling-strength threshold under Assumption 2.
• Corollary 4.9: partial synchronization of the first components.

Significance

Theorem 4.5 replaces a single $Nn\times Nn$ matrix inequality for the whole network with $M$ inequalities, one of the size of each component. In practice the test runs component by component down the Frobenius order: decide which components need pinning, choose gains for each one separately, and get synchronization of the whole network. Corollary 4.7 makes this explicit in terms of the outer in-degrees: a component with no incoming edges from earlier components has to be pinned (Remark 4), while a component that receives enough weight from upstream needs no control. These conditions underlie the pinning scheme algorithm of §5 of the paper.

On the formal side, as far as a search of the platform and of Mathlib shows, none of these results is machine-checked. Mathlib has the positive semidefinite Schur complement and irreducible nonnegative matrices, but not the strict Schur complement, block-diagonal Lyapunov scaling, or Lyapunov arguments for networked ODEs with Kronecker-structured couplings. The mission produces, beyond the paper's theorem:

• a reusable strict Schur complement lemma;
• a block-triangular diagonal-stability lemma;
• a template for Lyapunov estimates on coupled networks in Lean.

Difficulty

The obvious argument is to take one Lyapunov function weighted by a positive left null vector of the whole coupling matrix, as in the strongly connected case. Here it fails: the coupling matrix of a network that is not strongly connected has no positive left null vector, and condition (4.8) is local to each component. The central step is the passage from blockwise to global negative definiteness (Lemma 4.4). Condition (4.8) says nothing about the off-diagonal blocks that couple a component to earlier ones, and a block lower-triangular matrix whose symmetrized diagonal blocks are negative definite need not have a negative definite symmetric part; the component weights $\Delta_j$ have to be found so that those couplings are dominated, which is a quantitative statement about Schur complements. Turning the resulting matrix inequality into convergence of the trajectories then needs a differential inequality on $[0,\infty)$, a Kronecker-product definiteness argument with $\Gamma$, and the commutation of $K$ and $\Gamma$ to reach the θ bound.

Formalization scope

States are Fin n → ℝ and matrices are indexed by Fin N, Fin n, or the subtype of one component's vertices. Solutions are functions on ℝ that satisfy their ODE on $[0,\infty)$ through HasDerivWithinAt … (Set.Ici 0). "For any initial conditions" means for every pair of solutions $(s,x)$; existence of solutions is not claimed. Convergence is componentwise, which agrees with every norm on $\mathbb R^n$. "Positive definite" is Mathlib's Matrix.PosDef, which includes symmetry, and $X<0$ is (-X).PosDef. $\lambda_{\max}$ is the least Rayleigh bound, IsLamMax, never a supremum of a possibly empty set.

The vertices are not permuted into Frobenius form. The hypotheses say instead that:

• every component is nonempty;
• every component is strongly connected inside itself;
• every edge between components points forward in the order;
• every vertex is reachable from a pinned vertex.

The weights $\Pi_j$ are tied to the paper's object by $\Pi_j^{\mathsf T}A_j=0$. The standing assumptions of p. 1402 (Assumption 1, $K\Gamma=\Gamma K$, $\theta=\lambda_{\max}((K+K^{\mathsf T})/2)\ge0$, $\Gamma>0$) are hypotheses of every goal-level statement. The goal does not assume the weights $\Delta_j$, the bound (4.10), or definiteness of a whole-network matrix; it assumes only (4.8) on each component, so it cannot be trivialized by assuming its own conclusion. For $n=0$ the $\lambda_{\max}$ hypothesis cannot be met, so that degenerate dimension is excluded.

The pages contain three misprints. (4.10) has "$-c$" in its third line and "$++$" in its last; the last line, with a single $+$, is formalized. Corollary 4.9 ranges "$i=1,\dots,N$" where the component range is meant.

A complete development needs a Gronwall-type decay lemma on $[0,\infty)$, the strict Schur complement, definiteness of Kronecker products, and the square root of a positive definite matrix commuting with matrices that commute with it. Each of these is reusable well beyond this mission, and contributions to any of them are welcome, as are proofs of the milestones in any order.

Selected references

• W. Yu, G. Chen, J. Lü, J. Kurths, Synchronization via pinning control on general complex networks, SIAM J. Control Optim. 51(2) (2013), 1395–1416. https://doi.org/10.1137/100781699
• X. F. Wang, G. Chen, Pinning control of scale-free dynamical networks, Physica A 310 (2002), 521–531. https://doi.org/10.1016/S0378-4371(02)00772-0
• T. Chen, X. Liu, W. Lu, Pinning complex networks by a single controller, IEEE Trans. Circuits Syst. I 54(6) (2007), 1317–1326. https://doi.org/10.1109/TCSI.2007.895383
• S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
• R. A. Brualdi, H. J. Ryser, Combinatorial Matrix Theory, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9781107325708