Control Theory

Motivation

Networks of agents that interact both cooperatively and competitively are modelled by signed graphs: a positive edge weight means that one agent moves towards another, a negative weight means that it moves towards the other's opposite. Since Altafini's work on consensus over antagonistic networks (IEEE TAC 2013), the standard target on such networks has been bipartite consensus or bipartite tracking: the agents split into two camps that converge to values of equal size and opposite sign. With a leader, the camp containing the leader tracks the leader's state and the other camp tracks its negative.

Most analyses assume that all agents update at the same instants. In practice agents sample and communicate on their own clocks. Shi, Zheng, Shao and Cheng (arXiv:2004.01867v2, SIAM J. Control Optim. 2021) handle this asynchronous setting with a matrix tool: products of sub-stochastic matrices (nonnegative, row sums at most one) whose row-sum deficits propagate along the communication graph. This mission formalizes their first application, bipartite tracking of first-order agents with a static leader (§3).

Setting

There is one leader $v_0$ and $n$ followers $v_1,\dots,v_n$. Follower weights form a matrix $\mathcal A=[a_{ij}]\in\mathbb R^{n\times n}$: the edge $(v_j,v_i)$ exists iff $a_{ij}\neq 0$, cooperative if $a_{ij}>0$, competitive if $a_{ij}<0$. The number $a_{i0}$ is the weight of the leader edge $(v_0,v_i)$, which exists iff $a_{i0}\ne 0$. The digraph $\tilde{\mathcal G}$ consists of the followers' digraph, the leader and the leader edges.

• C1 (structural balance). The agents split as $\mathcal V_1\cup\mathcal V_2$ with $v_0\in\mathcal V_1$, every weight inside a set is $\ge 0$ and every weight between the sets is $\le 0$.
• C2 (leader reachability). Every follower is reached from $v_0$ by a directed path in $\tilde{\mathcal G}$.

Time is discrete with step size $\tau>0$. Follower $v_i$ communicates only at its own instants $s^i_0\tau<s^i_1\tau<\cdots$ with $s^i_0=0$ and

$$s^i_{k+1}-s^i_k\le h\qquad(2.10)$$

for a constant $h\in\mathbb Z_+$. Positions $x_i(k)\in\mathbb R^p$ evolve by $x_0(k+1)=x_0(k)$ and $x_i(k+1)=x_i(k)+\tau u_i(k)$, with the asynchronous protocol

$$u_i(k)=\psi\sum_{v_j\in\mathcal N_i}|a_{ij}|\big[\operatorname{sgn}(a_{ij})x_j(k)-x_i(k)\big]+\psi|a_{i0}|\big[\operatorname{sgn}(a_{i0})x_0(k)-x_i(k)\big]$$

at the instants of $v_i$, and $u_i(k)=0$ otherwise. Here $\psi>0$ is a gain. Bipartite tracking (Definition 3.1) means $\|x_i(k)-x_0(k)\|\to 0$ for $v_i\in\mathcal V_1$ and $\|x_i(k)+x_0(k)\|\to 0$ for $v_i\in\mathcal V_2$. With $d_M=\max_i\big(\sum_{v_j\in\mathcal N_i}|a_{ij}|+|a_{i0}|\big)$, the gain condition is

$$\psi<\frac{1}{\tau d_M}.\qquad(3.7)$$

In the error coordinates $e_i=x_i-x_0$ on $\mathcal V_1$ and $e_i=-x_i-x_0$ on $\mathcal V_2$, the closed loop is $e(k+1)=(M(k)\otimes I_p)e(k)$ with $M(k)=I_n-\tau\psi\mathcal D(k)-\tau\psi\mathcal B(k)+\tau\psi|\mathcal A(k)|$, where only the rows of followers active at time $k\tau$ differ from the identity.

Formalization targets

Goal: Theorem 3.3, sufficiency

$$\psi<\frac1{\tau d_M},\ \ \mathrm{C1},\ \ \mathrm{C2}\ \Longrightarrow\ \lim_{k\to\infty}\|x_i(k)-x_0(k)\|=0\ (v_i\in\mathcal V_1),\quad \lim_{k\to\infty}\|x_i(k)+x_0(k)\|=0\ (v_i\in\mathcal V_2),$$

for every choice of instants satisfying (2.10) and every initial state.

Milestones

1. Theorem 2.4 1): a product $F_q\cdots F_1$ of sub-stochastic matrices is sub-stochastic.
2. Theorem 2.4 2): with positive diagonals, if every row $i_2$ is fed through $[F_{s_2}]_{i_2i_1}>0$ by a row $i_1$ with $\Lambda_{i_1}[F_{s_1}]<1$, $s_1<s_2$, then $\|\prod_{s=1}^qF_s\|_\infty<1$ and $\rho(\prod_{s=1}^qF_s)<1$.
3. The matrices $M(k)$ (p. 15): under (3.7) they are sub-stochastic with positive diagonals, and $\Lambda_i[M(k)]<1$ exactly when $v_i$ hears the leader at $k\tau$.
4. Error system (3.6): under C1, $e_i(k+1)=\sum_j[M(k)]_{ij}e_j(k)$.
5. Lemma 3.2: under (3.7), C1 and C2, $\big\|\prod_{s=k}^{k+Ph-1}M(s)\big\|_\infty<1$ for every $k$, where $P=\max_i d(v_0,v_i)$ is the largest directed distance from the leader.

Significance

The theorem says that asynchrony costs nothing qualitatively: as long as every follower communicates at least once every $h$ steps and the gain respects (3.7), the network reaches bipartite tracking under the same topological conditions C1 and C2 as in the synchronous case. No common clock, dwell-time condition or joint connectivity of the switching graphs is required. The same product argument is reused in the rest of the paper for second-order and general linear agents, delays and switching topologies, so the milestones here are the base case of that series.

The result is proved in the paper; it has not been formalized. Formalizing it produces a checked theory of products of sub-stochastic matrices with row-sum deficits (Theorem 2.4), which applies to positive switched systems in general, and a reusable encoding of signed digraphs with a leader, structural balance and asynchronous protocols.

Difficulty

Each single matrix $M(k)$ is only marginally stable: its rows of followers that do not hear the leader at time $k\tau$ sum to exactly one, so no single step contracts, and the spectral radius of an individual $M(k)$ may equal one. Contraction appears only in products, and only once a deficit created at a leader edge has had time to travel along the paths of C2, one edge per window of $h$ steps; this requires that deficits never disappear again, which is where positive diagonals (from (3.7)) enter. The passage from "every window product has $\|\cdot\|_\infty<1$" to convergence also needs a uniform bound below one over all windows; the paper's (3.14) uses it without comment. The bound holds because $M(k)$ depends on $k$ only through the set of active followers, so the window products range over a finite set.

Formalization scope

Followers are Fin n (0-based) and the leader is not an index; $a_{ij}$ is a i j and $a_{i0}$ is b i. Positions lie in EuclideanSpace ℝ (Fin p); the paper's norm is unspecified and all norms on $\mathbb R^p$ give the same limits. Eigenvalues are complex: $\rho(F)<1$ means every element of spectrum ℂ of the complexified matrix has modulus $<1$. $\|F\|_\infty$ is the largest absolute row sum. Products multiply later factors on the left. $\operatorname{sgn}$ is Real.sign. The maxima $d_M$ and $P$ are given as values with IsGreatest hypotheses over exactly the printed sets, and (3.7) is kept as printed. C1 is stated for the partition $\mathcal V_1=\{v_0\}\cup V_1$, $\mathcal V_2=$ the remaining followers; fixing the leader in $\mathcal V_1$ is the paper's "with no loss of generality" convention. Definition 3.1 is stated for that same partition.

Only the "if" half of Theorem 3.3 is a target. Definition 3.1 presupposes the partition of C1, so necessity of C1 has no formal meaning, and the printed necessity argument is an informal case discussion. Theorem 2.4 2) is stated with one $(i_1,s_1,s_2)$ per row $i_2$, as its proof and the example on p. 8 use it; this is implied by the literal reading.

Three formalizations would trivialize the goal and are ruled out: a protocol in which every follower updates at every step (the synchronous special case, which drops the asynchronous instants); dropping the sign conditions of C1, or leaving the leader's side free, under which the followers of $\mathcal V_2$ need not approach $-x_0$; and a goal stated about the error system (3.6) instead of the agents' positions $x_i$.

The development needs finite matrix products, the ∞-norm bound on eigenvalues (Gershgorin), and elementary walk reachability in digraphs. All of these exist in Mathlib in some form. Contributions are welcome on every milestone. The product theorem 2.4 does not depend on the network model and is reusable for positive switched systems.

Selected references

• L. Shi, W. X. Zheng, J. Shao, Y. Cheng, Sub/super-stochastic matrix with applications to bipartite tracking control over signed networks, arXiv:2004.01867v2, 2020; SIAM J. Control Optim. 59 (2021). https://arxiv.org/abs/2004.01867, https://doi.org/10.1137/19M1239982
• C. Altafini, Consensus problems on networks with antagonistic interactions, IEEE Trans. Automat. Control 58(4), 2013. https://doi.org/10.1109/TAC.2012.2224251

Distributed optimization over directed, changing networks

In distributed optimization, $n$ agents cooperatively minimize the average $f(x)=\frac1n\sum_{i=1}^n f_i(x)$ of private cost functions $f_i:\mathbb R^p\to\mathbb R$, exchanging information only with their current neighbours in a communication network. The model covers sensor networks, multi-robot coordination and machine learning with data split across machines, where no node can see the whole objective. In many of these systems communication is one-directional (broadcast radios with unequal ranges, asymmetric links) and the network changes over time.

Directed links raise a specific obstacle: a node cannot in general choose weights that are both row and column stochastic, because it knows its out-degree but not how its messages are combined by others. The push-sum (ratio consensus) protocol of Kempe, Dobra and Gehrke (2003) circumvents this with column stochastic weights and a scalar correction. Nedić and Olshevsky (2015) combined it with diminishing-step subgradient methods over time-varying directed graphs, obtaining sublinear rates. Gradient tracking methods (Xu, Zhu, Soh and Xie, 2015; Qu and Li, 2016) and EXTRA (Shi, Ling, Wu and Yin, 2015) reached linear rates with constant steps on undirected or static graphs. Nedić, Olshevsky and Shi (arXiv 2016, SIAM J. Optim. 2017) proved geometric convergence of gradient tracking over graphs that are both time-varying and directed; this mission formalizes that result.

Setting

The agents are $\{1,\dots,n\}$. At each time $k$ there is a set $\mathcal A(k)$ of arcs; an arc $j\to i$ means agent $j$ can send to agent $i$. The out-degree $d^{\rm out}_j(k)$ counts the agents $i\ne j$ with $j\to i$ in $\mathcal A(k)$.

Assumption 6. There is $\tilde B_\ominus>0$ such that for every $t\ge0$ the union of the arc sets over the window $t\tilde B_\ominus,\dots,(t+1)\tilde B_\ominus-1$ is strongly connected. Put $B_\ominus=2\tilde B_\ominus-1$.

Assumption 7. The mixing matrix $C(k)$ has $C_{ij}(k)=1/(d^{\rm out}_j(k)+1)$ if $i=j$ or $j\to i\in\mathcal A(k)$, and $0$ otherwise; each $C(k)$ is column stochastic.

Each $f_i$ is differentiable with $L_i$-Lipschitz gradient (Assumption 4) and $\mu_i$-strongly convex with $\mu_i\ge0$, some $\mu_i>0$ (Assumption 5). Write $L=\max_iL_i$, $\bar\mu=\frac1n\sum_i\mu_i$, $\bar\kappa=L/\bar\mu$, and $x^*$ for the minimizer of $f$.

Iterates are $n\times p$ matrices whose row $i$ belongs to agent $i$; $\nabla\mathbf f(\mathbf x)$ has rows $\nabla f_i(x_i)$, and $\|\cdot\|_F$ is the Frobenius norm. Push-DIGing starts from $\mathbf x(0)=\mathbf u(0)$, $\mathbf y(0)=\nabla\mathbf f(\mathbf x(0))$, $\mathbf v(0)=\mathbf 1$ and iterates, with step size $\alpha>0$ and $V(k)=\operatorname{diag}\{\mathbf v(k)\}$,

$$\mathbf u(k+1)=C(k)(\mathbf u(k)-\alpha\mathbf y(k)),\quad \mathbf v(k+1)=C(k)\mathbf v(k),\quad \mathbf x(k+1)=V(k+1)^{-1}\mathbf u(k+1),$$ $$\mathbf y(k+1)=C(k)\mathbf y(k)+\nabla\mathbf f(\mathbf x(k+1))-\nabla\mathbf f(\mathbf x(k)).$$

The constants of the rate are $\tilde\tau=n^{-(2+nB_\ominus)}$, $Q_1=2n(1+\tilde\tau^{-nB_\ominus})/(1-\tilde\tau^{nB_\ominus})$, $\|V^{-1}\|^1_{\max}=\sup_{k,i}1/v_i(k)$ and, for an integer $B$,

$$\delta=Q_1\big(1-\tilde\tau^{nB_\ominus}\big)^{\frac{B-1}{nB_\ominus}},\qquad J_2=3Q_1\|V^{-1}\|^1_{\max}\bar\kappa B\big(\delta+Q_1(B-1)\big)(1+\sqrt n)\big(1+4\sqrt n\sqrt{\bar\kappa}\big).$$

Formalization targets

Goal: Theorem 18

For $n\ge2$, $B\ge B_\ominus$ with $\delta<1$, and every step size

$$0<\alpha<\frac{1.5(1-\delta)^2}{\bar\mu J_2},$$

there is $C>0$ with $\|\mathbf x(k)-\mathbf 1(x^*)^\top\|_F\le C\lambda^k$ for all $k$, where $0<\lambda<1$ is

$$\lambda=\sqrt[2B]{1-\alpha\bar\mu/1.5}\ \text{ if }\ \alpha\le\frac{1.5\big(\sqrt{J_2^2+(1-\delta^2)J_2}-\delta J_2\big)^2}{\bar\mu J_2(J_2+1)^2},\qquad \lambda=\sqrt[B]{\sqrt{\alpha\bar\mu J_2/1.5}+\delta}\ \text{ otherwise}.$$

Milestones

The paper's proof runs a small gain argument around the cycle $\mathbf q\to\mathbf z\to\check{\mathbf h}\to\check{\mathbf x}\to\mathbf q$, where $\mathbf q(k)=\mathbf x(k)-\mathbf 1(x^*)^\top$, $\mathbf z$ are gradient increments, $\mathbf h(k)=V(k)^{-1}\mathbf y(k)$ and $\check{\ }$ is the deviation from the row average. The milestones are the paper's own statements: the equivalent recursion (48) in terms of the row stochastic $\tilde R(k)=V(k+1)^{-1}C(k)V(k)$; the bound (49) $\|V^{-1}\|^1_{\max}\le n^{nB_\ominus}$ and row stochasticity of $\tilde R(k)$; Lemma 13 ($B$-step contraction by $\delta$); Lemmas 14–17 (the four arrows); Lemma 8 (an error bound for inexact gradient descent); Theorem 3 (the small gain theorem) and Lemma 4.

Significance

The theorem gives a geometric rate, with explicit constants, for a first-order method that uses only out-degree information, constant step sizes, one gradient per agent per round, and networks that are directed and need only be strongly connected jointly over windows. Before it, linear rates for distributed gradient methods required undirected or static graphs. The explicit $\lambda$ quantifies how the rate degrades with $n$, $B_\ominus$ and the condition number $\bar\kappa$. The result is proved in the paper; to the extent known, no machine-checked proof exists. A formalization yields a checked statement of the rate together with reusable components: the ergodic-norm small gain theorem, the push-sum weight bound, and the inexact gradient lemma, which also serve the companion DIGing mission on undirected graphs.

Difficulty

The natural Lyapunov approach fails: with asymmetric, time-varying weights there is in general no quadratic function that decreases at every step, and the consensus error contracts only over windows of $B$ iterations. The analysis therefore works with ergodic norms $\max_{k\le K}\lambda^{-k}\|\mathbf s(k)\|_F$ and chains four inequalities. Two further inputs come from outside the paper: the lower bound $v_i(k)\ge n^{-nB_\ominus}$ (Corollary 2(b) of Nedić–Olshevsky 2015) and the contraction of products of row stochastic matrices with entries bounded below on arcs (Lemma 5 of Nedić–Ozdaglar 2010), both of which a complete development has to prove.

Formalization scope

Stacked iterates are functions Fin n → EuclideanSpace ℝ (Fin p); agents are indexed from 0 and time from 0. An arc $j\to i$ is a pair (j, i) in a finite set A k. The weights $\mathbf v(k)$ are defined from $C$ alone, so $\|V^{-1}\|^1_{\max}$ is a constant of the graph sequence; it enters statements as a number with the hypothesis that it is the least upper bound of $\{1/v_i(k)\}$, never as a real supremum. Real powers are Real.rpow. The ergodic norm is the truncated maximum; the untruncated supremum is replaced by its pointwise meaning.

Four hypotheses are added to the page, each disclosed in the statements:

1. Assumption 7 includes the self-weight $C_{jj}(k)=1/(d^{\rm out}_j(k)+1)$. The printed rule assigns weights on arcs only, which makes column sums $d/(d+1)$; the paper's agent updates (p. 21) and analysis use the push-sum convention.
2. The step-size interval is open on the right: at $\alpha=1.5(1-\delta)^2/(\bar\mu J_2)$ the printed formula gives $\lambda=1$.
3. $B\ge B_\ominus$, required by Lemma 13, makes "large enough" precise.
4. $n\ge2$: at $n=1$ the constant $Q_1$ has a zero denominator.

The goal states only the hypotheses of Theorem 18 and the rate; it does not assume any of the arrows, gains, auxiliary parameters $\beta,\eta$ or ergodic-norm bounds, so it cannot be discharged by assembling hypotheses.

A complete development needs matrix-product contraction bounds for push-sum, Frobenius-norm calculus on stacked matrices, and strong convexity estimates for inexact gradient steps. The small gain theorem, Lemma 8 and the push-sum lemmas are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• A. Nedić, A. Olshevsky, W. Shi, Achieving geometric convergence for distributed optimization over time-varying graphs, SIAM J. Optim. 27 (2017) 2597–2633; arXiv:1607.03218v3. https://arxiv.org/abs/1607.03218 — https://doi.org/10.1137/16M1084316
• A. Nedić, A. Olshevsky, Distributed optimization over time-varying directed graphs, IEEE Trans. Automat. Control 60 (2015) 601–615. https://arxiv.org/abs/1303.2289
• A. Nedić, A. Olshevsky, Stochastic gradient-push for strongly convex functions on time-varying directed graphs, arXiv:1406.2075, 2014. https://arxiv.org/abs/1406.2075
• D. Kempe, A. Dobra, J. Gehrke, Gossip-based computation of aggregate information, Proc. 44th IEEE FOCS, 2003, 482–491. https://doi.org/10.1109/SFCS.2003.1238221
• W. Shi, Q. Ling, G. Wu, W. Yin, EXTRA: an exact first-order algorithm for decentralized consensus optimization, SIAM J. Optim. 25 (2015) 944–966. https://arxiv.org/abs/1404.6264
• G. Qu, N. Li, Harnessing smoothness to accelerate distributed optimization, arXiv:1605.07112, 2016. https://arxiv.org/abs/1605.07112
• J. Xu, S. Zhu, Y. C. Soh, L. Xie, Augmented distributed gradient methods for multi-agent optimization under uncoordinated constant stepsizes, Proc. 54th IEEE CDC, 2015, 2055–2060.

Motivation

In distributed optimization, $n$ agents each hold a private function $f_i:\mathbb R^p\to\mathbb R$ and must jointly solve

$$\min_{x\in\mathbb R^p}\ f(x)=\frac1n\sum_{i=1}^n f_i(x)$$

by exchanging vectors only with their current neighbours in a communication network. The setting covers distributed estimation and learning in sensor networks, formation control and power-system control, where no agent can see all the data and no central coordinator is available. Often the network changes over time: links appear and fail, and agents move.

The classical method, distributed gradient descent (DGD), mixes neighbours' iterates and takes a local gradient step. With a fixed step size it does not converge to the optimum, because at a consensual optimum the local gradients $\nabla f_i(x^*)$ need not vanish; exact convergence requires diminishing steps and is then sublinear. Nedić, Olshevsky and Shi (arXiv:1607.03218, SIAM J. Optim. 2017) introduced DIGing, which adds a second variable that tracks the network-wide average gradient, and proved that it converges R-linearly (geometrically) to the exact optimum with a fixed step size, over time-varying undirected graphs, with an explicit rate.

Setting

An $n\times p$ matrix $\mathbf x$ is stored by its rows; row $i$ is agent $i$'s copy $x_i\in\mathbb R^p$, and $\|\mathbf x\|_F$ is the Frobenius norm. Write $\bar x=\frac1n\sum_ix_i$ and $\check{\mathbf x}=\mathbf x-\mathbf 1\bar x^\top$ (the consensus violation). The stacked gradient $\nabla\mathbf f(\mathbf x)$ has rows $\nabla f_i(x_i)$.

Objectives. Each $f_i$ is differentiable with $L_i$-Lipschitz gradient, $L_i>0$ (Assumption 4), and satisfies $f_i(x)\ge f_i(y)+\langle\nabla f_i(y),x-y\rangle+\frac{\mu_i}2\|x-y\|^2$ with $\mu_i\ge0$, at least one $\mu_i>0$ (Assumption 5). Put $L=\max_iL_i$, $\bar\mu=\frac1n\sum_i\mu_i$ and $\bar\kappa=L/\bar\mu$. Then $f$ has a unique minimizer $x^*$.

Network. At time $k$ the agents communicate over an undirected graph $E(k)$ and mix with a matrix $W(k)$. Let $W_B(k)=W(k)W(k-1)\cdots W(k-B+1)$ and $\delta(k)=\sigma_{\max}\{W_B(k)-\frac1n\mathbf 1\mathbf 1^\top\}$. Assumption 1 requires: $W_{ij}(k)=0$ when $i\ne j$ and $(j,i)\notin E(k)$; every $W(k)$ is doubly stochastic; and for some positive integer $B$, $\delta=\sup_{k\ge B-1}\delta(k)<1$.

DIGing (Algorithm 1) with step size $\alpha>0$: $\mathbf y(0)=\nabla\mathbf f(\mathbf x(0))$ and

$$\mathbf x(k+1)=W(k)\mathbf x(k)-\alpha\mathbf y(k),\qquad \mathbf y(k+1)=W(k)\mathbf y(k)+\nabla\mathbf f(\mathbf x(k+1))-\nabla\mathbf f(\mathbf x(k)).$$

Formalization targets

Goal: Theorem 10

Let $J_1=3\bar\kappa B^2(1+4\sqrt n\sqrt{\bar\kappa})$. For every step size $0<\alpha<1.5(1-\delta)^2/(\bar\mu J_1)$ there is $C>0$ with

$$\|\mathbf x(k)-\mathbf 1(x^*)^\top\|_F\le C\lambda^k\quad\text{for all }k,$$

where $0<\lambda<1$ is the explicit rate

$$\lambda=\sqrt[2B]{1-\frac{\alpha\bar\mu}{1.5}}\ \text{ if }\ \alpha\le\frac{1.5(\sqrt{J_1^2+(1-\delta^2)J_1}-\delta J_1)^2}{\bar\mu J_1(J_1+1)^2},\qquad \lambda=\sqrt[B]{\sqrt{\frac{\alpha\bar\mu J_1}{1.5}}+\delta}\ \text{ otherwise.}$$

Milestones

The proof runs a small gain argument in the ergodic norm $\|\mathbf s\|_F^{\lambda,K}=\max_{k\le K}\lambda^{-k}\|\mathbf s(k)\|_F$ around the cycle $\mathbf q\to\mathbf z\to\check{\mathbf y}\to\check{\mathbf x}\to\mathbf q$, where $\mathbf q(k)=\mathbf x(k)-\mathbf 1(x^*)^\top$ and $\mathbf z(k)$ are the gradient differences. The milestones are the paper's own lemmas: Lemma 2 (the $B$-step consensus contraction); Lemmas 5, 6, 7 and 9 (the four arrows); Lemma 8 (an error bound for inexact gradient descent, used by Lemma 9); Theorem 3 (the small gain theorem); Lemma 4 (a bounded ergodic norm gives an R-linear rate).

Companions

The existence and uniqueness of $x^*$ (p. 9); Corollary 11, the polynomial-in-$n$ rate $\lambda(\tau)=\sqrt[B]{1-\tau^2/(128B^2n^{4.5}\bar\kappa^{1.5})}$ under the concrete graph and weight Assumptions 2–3; and Proposition 1, the optimality conditions behind the algorithm.

Significance

Theorem 10 gives geometric convergence of a fixed-step method to the exact optimum over networks that may be disconnected at every instant, provided they are jointly well mixed over windows of $B$ steps. Its rate is explicit in $B$, $n$, $\delta$, $\bar\mu$ and $\bar\kappa$, and Corollary 11 turns it into an iteration count polynomial in $n$. Gradient tracking of this kind has since become a standard building block of decentralized optimization and learning algorithms, and the small-gain analysis in the ergodic norm is reused for other methods with time-varying or directed communication; the companion mission in this series treats Push-DIGing over directed graphs with the same machinery.

The result is proved in the paper. As far as is known it has not been machine-checked. A formalization provides checked versions of the paper's reusable components: the small gain theorem in the ergodic norm, the error bound for inexact gradient descent on a sum of strongly convex functions, and the consensus contraction for products of doubly stochastic matrices. It also pins down the conventions the paper leaves implicit, such as the sign of the mixing weights and the endpoint of the step-size interval.

Difficulty

DIGing does not decrease any obvious quantity monotonically: the distance to the optimum can grow while the gradient tracker is still far from consensus, and over a time-varying graph a single mixing step need not contract at all; only products of $B$ matrices do. A one-step Lyapunov argument therefore fails. The paper's way around this is to bound each quantity of the cycle by the previous one in the ergodic norm, with gains that depend on $\lambda$, and to choose $\lambda$ and $\alpha$ so that the product of the four gains is below one. The algebra of that choice, which produces the two-regime formula for $\lambda$, is delicate: the constraints $\delta<\lambda^B<1$, $\sqrt{1-\alpha\bar\mu\beta/(\beta+1)}\le\lambda$ and the gain condition (37) pull in opposite directions. Lemma 8 needs a careful one-step analysis of gradient descent with perturbed gradient evaluations.

Formalization scope

A stacked matrix is Fin n → EuclideanSpace ℝ (Fin p); $\|\cdot\|_F$, $\bar x$, $\check{\mathbf x}$, $\mathbf 1c^\top$ and the ergodic norm (6) are defined in DIGing.Undir.Common; $W_B(k)$, $\sigma_{\max}$ (the operator norm on Euclidean $\mathbb R^n$), $\delta(k)$, Assumptions 1–3, DIGing, $J_1$ and the rate are in DIGing.Undir.Setting. The constants $L_i,\mu_i$ are parameters. $\delta$ is given as the least upper bound of $\{\delta(k):k\ge B-1\}$, and the optimum $x^*$ by its optimality. Agents and iterations are indexed from $0$. Roots are Real.rpow.

Two hypotheses differ from the printed text, both disclosed in the item notes. Doubly stochastic includes nonnegative entries (Mathlib's doublyStochastic); the paper uses the term in this sense, and Lemma 6 is false for signed matrices with unit row and column sums. The right endpoint $\alpha=1.5(1-\delta)^2/(\bar\mu J_1)$, printed as included, is excluded: there the rate formula gives $\lambda=1$. Corollary 11 assumes $p\ge1$, the paper's standing range (p. 4).

The goal assumes nothing about the arrows, the gains, the auxiliary parameters $\beta,\eta$ or the ergodic norm of the iterates; its only rate hypothesis is $0<\alpha<1.5(1-\delta)^2/(\bar\mu J_1)$, and its conclusion includes $\lambda<1$, so a bounded-sequence reading is ruled out.

A complete development needs: products and the spectral norm of doubly stochastic matrices; the ergodic norm and its monotonicity in $K$; basic smooth strongly convex analysis (existence of the minimizer, $\mu_i\le L_i$, co-coercivity); and real-power algebra for the choice of $\lambda$. The small gain theorem, Lemma 8 and Lemma 2 are reusable beyond this mission, and are shared with the Push-DIGing mission of this series. Corollary 11's proof additionally uses a bound $\delta\le1-\tau/(2n^2)$ from the consensus literature; formalizing it is a welcome separate contribution. Proofs of any milestone, and alternative arguments for the arrows, are welcome.

Selected references

• A. Nedić, A. Olshevsky, W. Shi, Achieving geometric convergence for distributed optimization over time-varying graphs, SIAM J. Optim. 27(4), 2017. https://arxiv.org/abs/1607.03218 (v3 is the version formalized)
• A. Nedić, A. Olshevsky, A. Ozdaglar, J. N. Tsitsiklis, On distributed averaging algorithms and quantization effects, IEEE Trans. Automat. Control 54(11), 2009. https://doi.org/10.1109/TAC.2009.2031203
• W. Shi, Q. Ling, G. Wu, W. Yin, EXTRA: An exact first-order algorithm for decentralized consensus optimization, SIAM J. Optim. 25(2), 2015. https://arxiv.org/abs/1404.6264
• A. Nedić, A. Ozdaglar, Distributed subgradient methods for multi-agent optimization, IEEE Trans. Automat. Control 54(1), 2009. https://doi.org/10.1109/TAC.2008.2009515

Motivation

The stochastic linear quadratic (LQ) optimal control problem asks to steer a linear stochastic differential equation by a control so as to minimize a quadratic cost. It is the basic model of stochastic control: Wonham studied it in 1968 (Wonham 1968), and it is the model on which feedback design, mean-field control and LQ differential games are built (Yong–Zhou 1999).

Classically the cost weights are assumed nonnegative and the control weight $R$ uniformly positive definite, the standard conditions (1.4). Under them the Riccati equation has a unique solution and the optimal control is a linear state feedback. A stochastic problem can however be well posed when $R$ is indefinite, because the diffusion term also penalizes the control.

Timeline:

• 1998: Chen, Li and Zhou observe that a stochastic LQ problem can be solvable with an indefinite $R$ (SIAM J. Control Optim. 36).
• 2002: Ait Rami, Moore and Zhou introduce a generalized Riccati equation with a pseudoinverse and algebraic constraints (SIAM J. Control Optim. 40).
• 2014: Sun and Yong prove that closed-loop solvability is equivalent to the existence of a regular solution of that Riccati equation (SIAM J. Control Optim. 52).
• 2016: Sun, Li and Yong characterize strongly regular solvability by the uniform convexity of the cost functional (SIAM J. Control Optim. 54, Theorem 4.5). This mission is that theorem.

Setting

A probability space $(\Omega,\mathcal F,\mathbb P)$ carries a standard one-dimensional Brownian motion $W$. Its natural filtration, augmented by the $\mathbb P$-null sets, is $\mathbb F$. Fix a horizon $T>0$ and deterministic coefficients $A,C\in\mathbb R^{n\times n}$, $B,D\in\mathbb R^{n\times m}$, weights $Q\in\mathbb S^n$, $S\in\mathbb R^{m\times n}$, $R\in\mathbb S^m$ (functions of time) and $G\in\mathbb S^n$. The admissible controls $\mathcal U[t,T]$ are the $\mathbb F$-progressively measurable processes $u$ with $\mathbb E\int_t^T|u|^2ds<\infty$. The state from the initial pair $(t,x)$ solves

$$dX=(AX+Bu+b)\,ds+(CX+Du+\sigma)\,dW,\qquad X(t)=x,$$

and the cost is

$$J(t,x;u)=\mathbb E\Big\{\langle GX(T),X(T)\rangle+2\langle g,X(T)\rangle+\int_t^T\big[\langle QX,X\rangle+2\langle SX,u\rangle+\langle Ru,u\rangle+2\langle q,X\rangle+2\langle\rho,u\rangle\big]ds\Big\}.$$

Standing assumptions (H1)–(H2): $A\in L^1$, $B,C\in L^2$, $D\in L^\infty$, $Q\in L^1$, $S\in L^2$, $R\in L^\infty$ on $(0,T)$, and square-integrability of the random terms $b,\sigma,q,\rho,g$. No sign condition is imposed on $G$, $Q$ or $R$. The homogeneous problem (SLQ)$^0$ sets $b,\sigma,g,q,\rho=0$; its cost is $J^0$.

The map $u\mapsto J^0(0,0;u)$ is uniformly convex if, for some $\lambda>0$,

$$J^0(0,0;u)\ \ge\ \lambda\,\mathbb E\int_0^T|u(s)|^2ds\qquad\forall u\in\mathcal U[0,T].\qquad(4.2)$$

With $\Sigma_P=R+D^\top PD$ and $K_P=B^\top P+D^\top PC+S$, the Riccati equation is

$$\dot P+PA+A^\top P+C^\top PC+Q-K_P^\top\Sigma_P^\dagger K_P=0,\qquad P(T)=G,\qquad(4.6)$$

with $\dagger$ the Moore–Penrose pseudoinverse. A solution $P\in C([0,T];\mathbb S^n)$ is strongly regular if $\Sigma_P\ge\lambda I$ a.e. for some $\lambda>0$ (4.10).

Formalization targets

Goal: Theorem 4.5

$$\exists\lambda>0:\ J^0(0,0;u)\ge\lambda\,\mathbb E\!\int_0^T\!|u|^2ds\ \ \forall u\in\mathcal U[0,T]\iff(4.6)\text{ admits a strongly regular solution.}$$

The goal fixes no constant: the $\lambda$ on each side is existential.

Milestones

1. Lemma 2.2: the cost of a feedback control $\Theta X+u$, written through the solution of a Lyapunov equation.
2. Lemma 2.3: $u\mapsto u-\Theta X^{(u)}$ is bounded below, $\mathbb E\int|u-\Theta X^{(u)}|^2\ge\gamma\,\mathbb E\int|u|^2$.
3. Proposition 4.1: uniform convexity gives unique open-loop solvability and $V^0(t,x)\ge\alpha|x|^2$.
4. Proposition 4.4: every Lyapunov solution satisfies $R+D^\top PD\ge\lambda I$ and $P\ge\alpha I$, with the same $\lambda,\alpha$.
5. (4.20) and the monotonicity $P_1\ge P_i\ge P_{i+1}\ge\alpha I$ of the iteration (4.18)–(4.19).
6. Uniform convergence of the iteration to a strongly regular solution.
7. The completion of squares $J^0(0,0;u)=\mathbb E\int\langle\Sigma_P(u-\Theta X^{(u)}),u-\Theta X^{(u)}\rangle ds$.

Companion items: Remark 4.6 (the same $\lambda$ bounds $\Sigma_P$), the well-posedness of the state equation and the cost (Sun–Yong 2014, Proposition 2.1), and Proposition 3.5 (the standard conditions (1.4) imply uniform convexity).

Significance

Theorem 4.5 gives a checkable sufficient condition for the classical structure of LQ control: under (4.2) the Riccati equation has a solution whose gain matrix $R+D^\top PD$ is uniformly positive definite, so the optimal control is a state feedback with an invertible gain. It covers indefinite weights, and Proposition 3.5 shows that it contains the classical case (1.4). Combined with Sun–Yong's equivalence it yields Corollary 4.7, the feedback representation of the open-loop optimal control, which later missions of this series use.

The results are proved in the paper. As far as is known they have no machine-checked proof. Formalizing them requires stochastic calculus for controlled SDEs (Itô's formula for quadratic forms of a state process) linked to matrix ODE theory. The definitions this mission fixes (the LQ problem, the Riccati and Lyapunov equations with a pseudoinverse) can be reused by the other missions of the series and by any stochastic LQ formalization.

Difficulty

The direction (ii) ⇒ (i) is a completion of squares followed by Lemma 2.3. Lemma 2.3 is not obvious: it asserts a bounded inverse for an operator defined through an SDE.

The direction (i) ⇒ (ii) is the hard one. The obvious approach would solve (4.6) directly, but (4.6) is nonlinear and its coefficient $\Sigma_P^\dagger$ may be singular. No sign condition gives a priori bounds. The paper instead builds a policy-iteration sequence of linear Lyapunov equations. The difficulty is to show that every iterate keeps $R+D^\top P_iD\ge\lambda I$, so that the next gain is defined, and stays bounded below. These bounds come from the cost functional (Proposition 4.4), not from the matrix equation. Uniform convergence of the iterates then needs integrable estimates under the weak integrability of (H1).

Formalization scope

• Basis. The paper's $(\Omega,\mathcal F,\mathbb P,W)$ is a probability measure with a standard Brownian motion IsStdBrownian (Mathlib's IsBrownianReal per coordinate, published module Peng1990.SMP.Stochastic). $\mathbb F$ is augmentedFiltration (published ReflectedBSDE.Existence.Setting).
• State and cost. The state from $(t,x)$ is an Itô solution from time $0$ whose coefficients are switched on at $t$, with continuous paths and $\mathbb E\sup|X|^2<\infty$. $J$ is evaluated along a chosen solution, which is unique; the item state_wellposed poses existence, uniqueness and integrability of the cost. Expectations are Bochner integrals, and $|u|^2$ is the Euclidean $u\cdot u$.
• Integrability and values. $L^p$ conditions on matrix functions are entrywise. The diffusion coefficients $C,D$ are taken Borel measurable on $[0,\infty)$ (a measurable representative of their class), so that the Itô integrand $CX+Du+\sigma$ of (1.1) is progressively measurable. $V$ is an EReal infimum over admissible controls.
• Matrix ODEs. The Riccati and Lyapunov equations are in integral form: continuous symmetric $P$, an integrable right-hand side, and $P(t)=G+\int_t^TF(s,P(s))ds$. The pseudoinverse is the published HarmonicGames.Decomposition.pinv. Where the paper prints $(\cdot)^{-1}$ ((4.19), p. 2290) Lean's matrix inverse is used; it is invertible there by $R+D^\top PD\ge\lambda I$.
• The iteration. The sequence of milestones 5–6 is given by hypotheses: $P_0$ solves (4.18) and $P_{i+1}$ the Lyapunov equation of $\Theta_i$. Lyapunov solutions are unique, so this is the paper's sequence.
• Constants. $\lambda$ and $\alpha$ in Proposition 4.4 and Remark 4.6 are the constants of (4.2) and (4.1), passed as parameters.

Ruling out trivial forms. Uniform convexity is not defined through the operator $M_2(0)$ of (3.8), and strong regularity includes the integral Riccati equation. A formalization that drops the Riccati equation, or reads uniform convexity off a matrix condition, is a different theorem. No positivity of $G$, $Q$ or $R$ is assumed anywhere except in Proposition 3.5, whose hypothesis (1.4) is exactly that.

Contributions welcome: Itô's formula for $\langle P(s)X(s),X(s)\rangle$ with a $C^1$ (or absolutely continuous) matrix $P$; existence and uniqueness for linear SDEs with $L^1/L^2$ coefficients; existence and uniqueness for linear matrix ODEs; the Penrose identities for pinv.

Selected references

• J. Sun, X. Li, J. Yong, Open-Loop and Closed-Loop Solvabilities for Stochastic Linear Quadratic Optimal Control Problems, SIAM J. Control Optim. 54 (2016), 2274–2308. https://doi.org/10.1137/15M103532X
• J. Sun, J. Yong, Linear Quadratic Stochastic Differential Games: Open-Loop and Closed-Loop Saddle Points, SIAM J. Control Optim. 52 (2014), 4082–4121. https://doi.org/10.1137/140953642
• M. Ait Rami, J. B. Moore, X. Y. Zhou, Indefinite Stochastic Linear Quadratic Control and Generalized Differential Riccati Equation, SIAM J. Control Optim. 40 (2002), 1296–1311. https://doi.org/10.1137/S0363012900371083
• S. Chen, X. Li, X. Y. Zhou, Stochastic Linear Quadratic Regulators with Indefinite Control Weight Costs, SIAM J. Control Optim. 36 (1998), 1685–1702. https://doi.org/10.1137/S0363012996310478
• W. M. Wonham, On a Matrix Riccati Equation of Stochastic Control, SIAM J. Control 6 (1968), 681–697. https://doi.org/10.1137/0306044
• J. Yong, X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3

Why open-loop and closed-loop solvability must be told apart

In a stochastic linear–quadratic (LQ) optimal control problem a controller steers a linear stochastic differential equation and pays a quadratic cost. When the cost weights are allowed to be indefinite — as in mean–variance portfolio selection, where the control weight is zero — the problem can still be well posed, and two different notions of solution appear. An open-loop optimal control is a process chosen for one given initial pair $(t,x)$. A closed-loop optimal strategy is a feedback law $u=\Theta X+v$ that is optimal for every initial state at once. A closed-loop optimal strategy yields an open-loop optimal control for each initial state; the converse is the question.

Timeline. Chen, Li and Zhou (1998, doi:10.1137/S0363012996310478) started the theory of indefinite stochastic LQ control. Ait Rami, Moore and Zhou (2002, doi:10.1137/S0363012900371083) introduced the generalized Riccati equation with a Moore–Penrose pseudoinverse and stated that, for Problem (SLQ)$^0$ with continuous coefficients and $S=0$, a continuous open-loop optimal control exists at every initial pair if and only if the Riccati equation has a solution satisfying a range condition and a sign condition. Sun and Yong (2014, doi:10.1137/140953642) characterized closed-loop solvability by regular solutions of that Riccati equation. Sun, Li and Yong (2016, doi:10.1137/15M103532X) showed by two explicit examples that the 2002 equivalence fails in both directions, and that open-loop solvability is strictly weaker than closed-loop solvability. This mission formalizes those examples.

Setting

Let $W$ be a standard one-dimensional Brownian motion on a probability space $(\Omega,\mathcal F,\mathbb P)$ and $\mathbb F$ its augmented natural filtration. For $(t,x)\in[0,T)\times\mathbb R^n$ and a control $u$ in the space $\mathcal U[t,T]$ of $\mathbb F$-progressively measurable $\mathbb R^m$-valued processes with $\mathbb E\int_t^T|u|^2ds<\infty$, the state equation is

$$dX=(AX+Bu+b)\,ds+(CX+Du+\sigma)\,dW,\qquad X(t)=x,$$

and the cost $J(t,x;u)$ is the expectation of $\langle GX(T),X(T)\rangle+2\langle g,X(T)\rangle$ plus the time integral of a quadratic form in $(X,u)$ with weights $Q,S,R$ and linear terms $q,\rho$. Problem (SLQ)$^0$ is the case $b=\sigma=g=q=\rho=0$, with cost $J^0$ and value function $V^0(t,x)=\inf_{u\in\mathcal U[t,T]}J^0(t,x;u)$.

The Riccati equation (4.6) is

$$\dot P+PA+A^\top P+C^\top PC+Q-(PB+C^\top PD+S^\top)(R+D^\top PD)^\dagger(B^\top P+D^\top PC+S)=0,\qquad P(T)=G,$$

where $M^\dagger$ is the Moore–Penrose pseudoinverse. A solution is regular if (4.7) $\mathcal R(B^\top P+D^\top PC+S)\subseteq\mathcal R(R+D^\top PD)$ a.e., (4.8) $(R+D^\top PD)^\dagger(B^\top P+D^\top PC+S)\in L^2$, and (4.9) $R+D^\top PD\ge 0$ a.e.

Example 7.1 is Problem (SLQ)$^0$ with $n=1$, $m=2$, $T=1$:

$$dX=[u_1+u_2]\,ds+[u_1-u_2]\,dW,\qquad J^0(t,x;u)=\mathbb E\,X(1)^2,$$

that is, $A=C=Q=0$, $B=(1,1)$, $D=(1,-1)$, $G=1$, $S=0$, $R=0$.

Formalization targets

Goal: Example 7.1

For every $(t,x)\in[0,1)\times\mathbb R$,

$$u^*_{(t,x)}(s)=-\Big(\frac{x}{2-2t},\frac{x}{2-2t}\Big)^\top\ \text{is open-loop optimal},\qquad V^0(t,x)=0,$$

while $V^0(1,x)=x^2$, and for every $t\in[0,1)$ the problem is not closed-loop solvable on $[t,1]$.

Milestones

1. (7.3): the Riccati equation has the unique solution $P\equiv1$, and it violates (4.7).
2. Theorem 4.3 for (SLQ)$^0$: closed-loop solvability on $[t,T]$ is equivalent to the existence of a regular solution on $[t,T]$.
3. (7.5)–(7.6): with $R$ replaced by $R+\varepsilon I$ the Riccati equation has the strongly regular solution $P_\varepsilon(t)=\varepsilon/(\varepsilon+2-2t)$.
4. (7.7): $P_\varepsilon(t)\to 0$ for $t<1$ and $P_\varepsilon(1)=1$.
5. (7.9)–(7.10): the closed-loop state and control of the regularized problem, $u_\varepsilon=-\big(\frac{x}{\varepsilon+2-2t},\frac{x}{\varepsilon+2-2t}\big)^\top$.
6. $u_\varepsilon\to u^*_{(t,x)}$ in $L^2$ as $\varepsilon\to0$.

Companion: Example 7.2

For $dX=u\,ds$ and $J=X(1)^2+\int_t^1s^2u^2ds$, the Riccati equation (7.12) has the unique solution $P(t)=t$, which satisfies (4.7) and (4.9), yet no open-loop optimal control exists at $(0,x)$, $x\neq0$.

Significance

The result. Example 7.1 refutes the necessity half of the Ait Rami–Moore–Zhou criterion: a continuous open-loop optimal control exists at every initial pair, but the Riccati equation has no regular solution. Example 7.2 refutes the sufficiency half. Together they show that the Riccati equation with conditions (4.7) and (4.9) characterizes neither notion, and that open-loop solvability is strictly weaker than closed-loop solvability; Example 7.1 also exhibits a finite value function that is discontinuous in time. These facts are why the paper develops separate characterizations of open-loop solvability (through the regularized Riccati solutions $P_\varepsilon$) instead of the Riccati equation itself.

Formalizing it. The examples are proved in the paper by appeal to its Theorems 5.3 and 6.2 and to Theorem 4.3 from Sun–Yong (2014). Nothing in this chain is machine-checked anywhere. A formal proof of the goal must verify the explicit optimal control against the canonical stochastic state equation, compute the value function, and rule out every closed-loop strategy; it can use Theorem 4.3 (posed here as a milestone) or a direct argument. The definitions built here (the stochastic LQ problem, the pseudoinverse Riccati equation, regularity) are shared with the other missions of this series.

Difficulty

Open-loop optimality looks immediate because $J^0=\mathbb EX(1)^2\ge0$, but it requires showing that the state driven by $u^*$ hits $0$ at time $1$, which means identifying the solution of the stochastic state equation for this control. The value at $t=1$ requires the degenerate interval $[1,1]$ to be handled inside the same SDE framework. The hard part is the negative claim: it quantifies over all feedback pairs $(\Theta,v)$ with $\Theta\in L^2$, and must show that no such pair drives every initial state to $0$ at time $1$. The paper reduces this to Theorem 4.3, whose proof (in Sun–Yong 2014) is a substantial piece of stochastic LQ theory; checking that $P\equiv 1$ fails the range condition is the easy end of that chain.

Formalization scope

Time is $\mathbb R_{\ge0}$, vectors are Fin k → ℝ, inner products are dot products, and $|u|^2=u\cdot u$. The Brownian motion is the published Peng1990.SMP.IsStdBrownian, the filtration the published augmented filtration, the SDE solution concept the published Peng1990.SMP.SolvesSDE, and the pseudoinverse the published HarmonicGames.Decomposition.pinv.

• The state from $(t,x)$ is an SDE from time $0$ with coefficients switched on at $t$, with a.s. continuous paths and $\mathbb E\sup|X|^2<\infty$; the cost uses a chosen solution, unique by [23, Proposition 2.1].
• Value functions are infima in the extended reals over admissible controls.
• The Riccati equation is in integral form on $[t_0,T]$; regularity is (4.7)–(4.9) on $[t_0,T]$.
• A closed-loop optimal strategy on $[t,T]$ requires $\Theta\in L^2(t,T)$, $v\in\mathcal U[t,T]$, and, for every initial state, a solution of the closed-loop system that is no worse than any admissible control.
• Theorem 4.3 is stated on $[t,T]$ (the paper states it on $[0,T]$ and applies it on $[t,1]$).
• The goal places no hypotheses on the probability space beyond the Brownian motion.

Proving only that $P\equiv1$ violates (4.7) does not settle the goal: the goal is about solvability of the control problem itself, and "not closed-loop solvable on any $[t,1]$" is stated for every $t<1$, not as the failure on some interval.

Contributions are welcome on any milestone, on the well-posedness of linear SDEs in this framework, and on the pseudoinverse identities (Penrose equations, the pseudoinverse of a scaled symmetric matrix) that the Riccati computations need.

Selected references

• J. Sun, X. Li, J. Yong, Open-loop and closed-loop solvabilities for stochastic linear quadratic optimal control problems, SIAM J. Control Optim. 54(5) (2016) 2274–2308. doi:10.1137/15M103532X
• M. Ait Rami, J. B. Moore, X. Y. Zhou, Indefinite stochastic linear quadratic control and generalized differential Riccati equation, SIAM J. Control Optim. 40 (2002) 1296–1311. doi:10.1137/S0363012900371083
• J. Sun, J. Yong, Linear quadratic stochastic differential games: open-loop and closed-loop saddle points, SIAM J. Control Optim. 52 (2014) 4082–4121. doi:10.1137/140953642
• S. Chen, X. Li, X. Y. Zhou, Stochastic linear quadratic regulators with indefinite control weight costs, SIAM J. Control Optim. 36 (1998) 1685–1702. doi:10.1137/S0363012996310478

Motivation

Linear–quadratic (LQ) optimal control is the basic test case of stochastic control: a linear stochastic differential equation, a quadratic cost, and an optimal control that one expects to be a linear feedback of the state computed from a Riccati equation. In the indefinite stochastic case the weighting matrices $G$, $Q$, $R$ carry no sign condition. The cost can then be convex without being uniformly convex, an optimal control may fail to exist although the value is finite, and the Riccati equation may have no solution of the kind the classical theory needs.

Sun, Li and Yong (SIAM J. Control Optim. 54 (2016) 2274–2308) separate finiteness, convexity, open-loop solvability and closed-loop solvability for this problem. This mission covers their Section 6. Under uniform convexity the optimal control is the Riccati feedback of Corollary 4.7. Section 6 removes uniform convexity: it regularizes the control weight $R$ to $R+\varepsilon I$, takes the Riccati feedback control $u_\varepsilon$ of each regularized problem, and shows that open-loop solvability of the original problem is exactly the convergence of $u_\varepsilon$ along some sequence $\varepsilon_k\to0$.

Timeline. Chen, Li and Zhou (SIAM J. Control Optim. 36 (1998)) introduced indefinite stochastic LQ problems. Ait Rami, Moore and Zhou (SIAM J. Control Optim. 40 (2002)) introduced the generalized Riccati equation with a pseudoinverse. Sun and Yong (SIAM J. Control Optim. 52 (2014)) characterized closed-loop solvability by regular solutions of that equation. In 2016 Sun, Li and Yong characterized uniform convexity by strongly regular solutions and open-loop solvability by the regularized feedback sequence treated here.

Setting

Fix a horizon $T>0$ and a probability space carrying a one-dimensional standard Brownian motion $W$, with $\mathbb F$ the augmented natural filtration of $W$. For an initial pair $(t,x)\in[0,T)\times\mathbb R^n$ and an admissible control $u\in\mathcal U[t,T]$, an $\mathbb F$-progressively measurable $\mathbb R^m$-valued process with $\mathbb E\int_t^T|u|^2ds<\infty$, the state solves

$$dX=(AX+Bu+b)\,ds+(CX+Du+\sigma)\,dW,\qquad X(t)=x .$$

The cost is

$$J(t,x;u)=\mathbb E\Big[\langle GX(T),X(T)\rangle+2\langle g,X(T)\rangle+\int_t^T\big(\langle QX,X\rangle+2\langle SX,u\rangle+\langle Ru,u\rangle+2\langle q,X\rangle+2\langle\rho,u\rangle\big)ds\Big].$$

The coefficients $A,B,C,D,Q,S,R$ and $G$ are deterministic, $b,\sigma,q,\rho,g$ are random, and the integrability conditions are (H1)–(H2). The value function is $V(t,x)=\inf_uJ(t,x;u)\in[-\infty,\infty)$. A control $u^*$ is open-loop optimal at $(t,x)$ if $J(t,x;u^*)\le J(t,x;u)$ for every $u\in\mathcal U[t,T]$. Problem (SLQ)$^0$ is the case $b,\sigma,g,q,\rho=0$, with cost $J^0$.

For $\varepsilon>0$ let $P_\varepsilon$ be the strongly regular solution of the Riccati equation (5.7),

$$\dot P_\varepsilon+P_\varepsilon A+A^\top P_\varepsilon+C^\top P_\varepsilon C+Q-K_\varepsilon^\top\Sigma_\varepsilon^{-1}K_\varepsilon=0,\qquad P_\varepsilon(T)=G,$$

where $\Sigma_\varepsilon=R+\varepsilon I+D^\top P_\varepsilon D\ge\lambda I$ for some $\lambda>0$ and $K_\varepsilon=B^\top P_\varepsilon+D^\top P_\varepsilon C+S$. Let $(\eta_\varepsilon,\zeta_\varepsilon)$ be the adapted solution of the linear backward equation (4.11) for these data, and put

$$\Theta_\varepsilon=-\Sigma_\varepsilon^{-1}K_\varepsilon,\qquad v_\varepsilon=-\Sigma_\varepsilon^{-1}\big(B^\top\eta_\varepsilon+D^\top\zeta_\varepsilon+D^\top P_\varepsilon\sigma+\rho\big).$$

With $X_\varepsilon$ the solution of the closed-loop system $dX_\varepsilon=[(A+B\Theta_\varepsilon)X_\varepsilon+Bv_\varepsilon+b]ds+[(C+D\Theta_\varepsilon)X_\varepsilon+Dv_\varepsilon+\sigma]dW$, $X_\varepsilon(t)=x$, the regularized feedback sequence is

$$u_\varepsilon=\Theta_\varepsilon X_\varepsilon+v_\varepsilon,\qquad\varepsilon>0 .$$

$\mathcal U[t,T]=L^2_{\mathbb F}(t,T;\mathbb R^m)$ is a Hilbert space with inner product $\mathbb E\int_t^T\langle u,v\rangle ds$; weak and strong convergence of controls refer to it.

Formalization targets

Goal: Theorem 6.2

Assume (H1)–(H2) and that $u\mapsto J^0(0,0;u)$ is convex. For $(t,x)\in[0,T)\times\mathbb R^n$ the following are equivalent:

$$\text{(SLQ) is open-loop solvable at }(t,x)\iff\exists\,\varepsilon_k\downarrow0:\ u_{\varepsilon_k}\rightharpoonup u^*\iff\exists\,\varepsilon_k\downarrow0:\ u_{\varepsilon_k}\to u^*\text{ in }\mathcal U[t,T],$$

and every weak or strong limit of such a subsequence is an open-loop optimal control at $(t,x)$. The goal assumes convexity, not uniform convexity, and no finiteness.

Milestones

1. Corollary 3.4: convexity of $J(t,x;\cdot)$ or $J^0(t,x;\cdot)$ at one $x$, at every $x$, and $J^0(t,0;u)\ge0$ on $\mathcal U[t,T]$ are equivalent.
2. The zero extension (4.3): $J^0(t,0;u)=J^0(0,0;0I_{[0,t)}\oplus u)$.
3. Corollary 4.7: under uniform convexity, the Riccati feedback control (4.28) is the unique open-loop optimal control.
4. Theorem 6.1: if the problem is finite, $\lim_{\varepsilon\to0^+}J(t,x;u_\varepsilon)=V(t,x)$.
5. Lemma 6.3: in a Hilbert space the norm is weakly lower semicontinuous, and strong convergence is weak convergence plus convergence of norms.
6. (6.7): $\mathbb E\int_t^T|u_\varepsilon|^2ds\le(V_\varepsilon-V)/\varepsilon\le\mathbb E\int_t^T|v^*|^2ds$ for any optimal $v^*$.
7. Weak lower semicontinuity of $u\mapsto J(t,x;u)$.

Two further statements follow the goal: open-loop solvability is equivalent to $\sup_{\varepsilon>0}\mathbb E\int_t^T|u_\varepsilon|^2ds<\infty$ (p. 2303), and Proposition 6.4: if $\sup_{\varepsilon>0}\int_0^T|\Theta_\varepsilon|^2ds<\infty$, the Riccati equation (4.6) has a regular solution and Problem (SLQ)$^0$ is closed-loop solvable.

Significance

Theorem 6.1 gives a minimizing sequence computed from Riccati and backward equations whenever the problem is finite. Theorem 6.2 turns it into a test for open-loop solvability that needs no uniform convexity and no regular solution of the original Riccati equation. When an optimal control exists, it is recovered as the limit of feedback controls. Proposition 6.4 converts a bound on the gains $\Theta_\varepsilon$ into closed-loop solvability of the homogeneous problem. Section 7 of the paper shows that open-loop solvability does not imply closed-loop solvability, so a criterion phrased directly in open-loop terms is needed.

All of these results are proved in the paper. None of them, nor the solution theory of stochastic LQ problems they rest on, had a machine-checked proof on Prove2Me or in Mathlib as of October 2026. A formal development needs the well-posedness of linear SDEs and BSDEs with integrable coefficients, the Riccati theory of Section 4, and the Hilbert-space structure of the space of admissible controls. Those parts are reusable for any stochastic LQ problem.

Difficulty

The obvious approach takes any minimizing sequence and extracts a weakly convergent subsequence. That fails without uniform convexity: a minimizing sequence need not be bounded, and boundedness is exactly what open-loop solvability provides in (6.7). The converse direction needs the limit of the regularized costs to identify the value, which requires both the minimizing property of $u_\varepsilon$ (Theorem 6.1) and weak lower semicontinuity of $J$. That in turn rests on convexity being transported from $J^0(0,0;\cdot)$ to $J(t,x;\cdot)$ through Corollary 3.4 and the zero extension. Upgrading weak to strong convergence uses the norm bound (6.7) with the limit itself as the optimal control. Every step depends on Corollary 4.7, the Riccati representation of the optimal control of the regularized problem, whose proof requires the theory of Section 4.

Formalization scope

The probability basis is a probability space with a one-dimensional standard Brownian motion and its augmented natural filtration. Vectors are Fin k → ℝ and matrices Matrix (Fin k) (Fin l) ℝ. Time is ℝ≥0, and $|u|^2$ is the Euclidean dot product u ⬝ᵥ u. (H1)–(H2) are standing assumptions, with entrywise $L^p$ conditions on the matrix coefficients. The state from $(t,x)$ is a strong solution of the published SDE notion Peng1990.SMP.SolvesSDE whose coefficients are switched on at $t$; it has a.s. continuous paths and $\mathbb E\sup|X|^2<\infty$. The cost is evaluated along a chosen solution, which is unique. $V$ is an infimum in the extended reals. Limits in $\varepsilon$ are taken as $\varepsilon\to0^+$. "A subsequence" is a sequence $\varepsilon_k>0$ with $\varepsilon_k\to0$, and the limit control is required to be admissible. The backward equations use the published Peng1990.SMP.SolvesBSDE, and the pseudoinverse in (4.6) and (4.11) is the published HarmonicGames.Decomposition.pinv.

Theorem 6.1 prints the term $-\Theta_\varepsilon^\top\rho$ in its backward equation. The equation (4.11) that its proof uses through Corollary 4.7 has $+\Theta_\varepsilon^\top\rho$, and the formalization uses (4.11). Corollary 3.4 is stated without its item (vi), which involves an operator $M_2(t)$ that the paper quotes from another source.

The families $P_\varepsilon$, $(\eta_\varepsilon,\zeta_\varepsilon)$ and $X_\varepsilon$ are hypotheses pinned by their equations for every $\varepsilon>0$. The sequence $u_\varepsilon$ is therefore the Riccati feedback sequence (6.2), never an arbitrary minimizing sequence or an arbitrary family of $\varepsilon$-optimal controls; with such a family the implication (ii) ⇒ (i) would be a different theorem.

Contributions are welcome at every level: the solution theory of linear SDEs and BSDEs, Itô's formula for quadratic forms, Riccati and Lyapunov equations in integral form, weak compactness in $L^2_{\mathbb F}$, and the milestones themselves.

Selected references

• J. Sun, X. Li, J. Yong, Open-loop and closed-loop solvabilities for stochastic linear quadratic optimal control problems, SIAM J. Control Optim. 54(5) (2016) 2274–2308. https://doi.org/10.1137/15M103532X
• J. Sun, J. Yong, Linear quadratic stochastic differential games: open-loop and closed-loop saddle points, SIAM J. Control Optim. 52(6) (2014) 4082–4121. https://doi.org/10.1137/140953642
• S. Chen, X. Li, X. Y. Zhou, Stochastic linear quadratic regulators with indefinite control weight costs, SIAM J. Control Optim. 36(5) (1998) 1685–1702. https://doi.org/10.1137/S0363012996310478
• M. Ait Rami, J. B. Moore, X. Y. Zhou, Indefinite stochastic linear quadratic control and generalized differential Riccati equation, SIAM J. Control Optim. 40(4) (2002) 1296–1311. https://doi.org/10.1137/S0363012900371083
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4) (1990) 966–979. https://doi.org/10.1137/0328054