All missions

Motivation

In a repeated game, players who do not know the payoff structure can still learn by reinforcement: each player keeps a running score for every action, the cumulative payoff that action would have earned, and plays a mixed strategy that favours actions with high scores. Turning scores into mixed strategies through a regularized best response (maximize score minus a convex penalty) gives a family of dynamics that includes exponential weights and the replicator dynamics (entropic penalty), and also the projection dynamics (quadratic penalty). The same scheme is the continuous-time counterpart of online mirror descent and dual averaging in online optimization.

For the replicator dynamics, the standard folk results of evolutionary game theory say that Nash equilibria are stationary, that limits of interior orbits are Nash equilibria, that Lyapunov stable states are Nash equilibria, and that strict equilibria are asymptotically stable (Weibull 1995; Hofbauer–Sigmund 1998). Mertikopoulos and Sandholm (arXiv:1407.6267v2, Math. Oper. Res. 41(4), 2016) show that all four results survive for the whole family. For steep, decomposable penalties several of them were known (Coucheney–Gaujal–Mertikopoulos 2015). The new part is the nonsteep case, where mixed strategies can hit the boundary of the simplex and the induced dynamics on strategies are no longer well defined.

Setting

A finite game $\mathcal G$ has a finite set $\mathcal N$ of players. Player $k$ has a finite nonempty set $\mathcal A_k$ of pure strategies and a payoff function $u_k:\prod_\ell\mathcal A_\ell\to\mathbb R$. A mixed profile is $x=(x_k)_k\in\mathcal X=\prod_k\Delta(\mathcal A_k)$, and $u_k(x)$ is player $k$'s expected payoff when the players randomize independently. The payoff vector is $v_{k\alpha}(x)=u_k(\alpha;x_{-k})$, the payoff of pure strategy $\alpha$ against $x_{-k}$.

A penalty function on a simplex $\Delta$ (Definition 2.1) is a function $h:\Delta\to\mathbb R$ that is continuous, smooth on the relative interior of every face, and $K$-strongly convex:

$$h(tx_1+(1-t)x_2)\le t\,h(x_1)+(1-t)\,h(x_2)-\tfrac12Kt(1-t)\|x_1-x_2\|_2^2 .$$

Steepness (gradients blowing up at the boundary) is not required. Its choice map is $Q(y)=\arg\max_{x\in\Delta}\{\langle y|x\rangle-h(x)\}$. Every player $k$ has a penalty function $h_k$ with constant $K_k$.

The reinforcement learning dynamics (RL) are

$$\dot y_{k\alpha}=v_{k\alpha}(x),\qquad x_k=Q_k(y_k),$$

and an orbit is a pair $(y(t),x(t))$, $t\ge0$, satisfying them. A Nash equilibrium is a profile $x^*$ with $u_k(x^*)\ge u_k(x_k;x^*_{-k})$ for every $k$ and every mixed $x_k$. It is strict if the inequality is strict for every $x_k\neq x^*_k$.

Because (RL) lives in the space of scores and $Q$ is neither injective nor surjective, stability is defined on the trajectories of play (Definition 5.1):

• $x^*$ is Lyapunov stable if for every $\varepsilon>0$ there is $\delta>0$ such that every orbit with $\|x(0)-x^*\|<\delta$ stays within $\varepsilon$ of $x^*$ forever;
• it is attracting if every orbit started close enough to $x^*$ converges to $x^*$;
• it is asymptotically stable if it is both;
• it is stationary if $x^*\in\operatorname{im}Q$ and every orbit with $x(0)=x^*$ stays at $x^*$.

Formalization targets

Goal: Theorem 5.2, Part IV

$$x^*\ \text{strict Nash equilibrium of }\mathcal G\ \Longrightarrow\ x^*\ \text{asymptotically stable under (RL)},$$

for every finite game and every choice of penalty functions $h_k$, steep or not.

Milestones (the steps of the proof, pp. 23–24, and the Appendix results it uses)

• A strict equilibrium is a pure profile $x^*=(\alpha^*_1,\dots,\alpha^*_N)$, and $\delta_k=\min_{\mu\neq\alpha^*_k}\{v_{k\alpha^*_k}(x^*)-v_{k\mu}(x^*)\}>0$.
• Proposition A.1(iii): $Q_\alpha(y)\to0$ whenever $y_\alpha-y_\beta\to-\infty$.
• Proposition C.3: the Fenchel coupling $F_h(p,y)=h(p)+h^*(y)-\langle y|p\rangle$ satisfies $F_h(p,y)\ge\tfrac12K\|Q(y)-p\|^2$.
• Proposition C.2(i)–(iii): the Bregman divergence $D_h(p,x)=h(p)-h(x)-h'(x;p-x)$, built from the one-sided derivative, is finite, nonnegative with (C.6), and continuous on $\Delta_p=\{x:\operatorname{supp}x\supseteq\operatorname{supp}p\}$.
• (C.11): $F_h(p,y)=D_h(p,Q(y))$ whenever $Q(y)\in\Delta_p$.
• The monotonicity step: $h^*(y)-y_{\alpha^*}=\max_{x}\{\sum_{\mu\ne\alpha^*}x_\mu z_\mu-h(x)\}$ is nondecreasing in the relative scores $z_\mu=y_\mu-y_{\alpha^*}$.

Companions

Theorem 5.2, Parts I–III (stationary $\iff$ Nash and in $\operatorname{im}Q$; limits of orbits and Lyapunov stable states are Nash), Proposition 5.3, Proposition 3.1 (global existence and uniqueness of orbits) and Proposition A.1(i)–(ii).

Significance

Theorem 5.2 says that, as far as the qualitative long-run behaviour is concerned, the whole class of regularized reinforcement dynamics behaves like the replicator dynamics. Part IV is the positive half: strict equilibria are robust attractors of learning. This is used to justify equilibrium selection by learning, and Proposition 5.4 (not part of this mission) builds the rates of convergence, including convergence in finite time for nonsteep penalties, on top of it.

The result is proved in the paper; none of it is formalized. A Lean development would provide a reusable layer of game-theoretic learning dynamics: penalty functions without steepness, choice maps as regularized argmax, the Fenchel coupling and the one-sided Bregman divergence on the simplex. Two companion missions on the same paper use the same layer, for the extinction of dominated strategies and for time averages in zero-sum games. As far as is known, the stability theory of Section 5 has no machine-checked proof even for the replicator dynamics.

Difficulty

The obvious argument would be a Lyapunov argument for the induced dynamics on $\mathcal X$, as for the replicator equation. For nonsteep penalties these dynamics are not well defined: orbits reach the boundary and $Q$ is not invertible there. The proof works in the dual space instead, where the natural Lyapunov candidate is the Fenchel coupling $F_h(x^*,y)$. The coupling is not differentiable along the orbit in the usual sense, and its sublevel sets in score space must be related to genuine neighbourhoods of $x^*$ in $\mathcal X$. That needs the Bregman divergence with one-sided derivatives at boundary points and its continuity across faces of different dimension (Proposition C.2(iii)). A second obstacle is that the coupling does not strictly decrease when the maximizer sits at the vertex. The page states a strict inequality there, which fails for nonsteep penalties, so the argument has to be run with the weak inequality and a first-exit-time argument.

Formalization scope

• The game uses the published agt_games vocabulary: AGT.IsLottery, AGT.IsMixedProfile, AGT.expectedPayoff, and AGT.IsMixedNash for (5.1). Players form a Fintype ι, and actions are A k with Fintype and DecidableEq.
• Penalty functions are IsPenalty h K, Definition 2.1 with the Euclidean norm in (2.5) and $C^\infty$ smoothness along curves inside the relative interiors of faces. There is no steepness.
• The choice map is the predicate IsChoice h y x, never a chosen argmax.
• Orbits are IsRLOrbit u h y x, the differential form (3.1) with one-sided derivatives at $t=0$. Statements quantify over orbits and never construct one.
• Neighbourhoods of $x^*$ in $\mathcal X$ are balls of the sup metric on $\prod_k\mathbb R^{\mathcal A_k}$, and Definition 5.1 is stated in $\varepsilon$–$\delta$ form.
• Strict equilibria are not assumed pure; purity is a milestone.
• The one-sided derivative (C.3) is a limit predicate with a real value, so the Bregman divergence's value $+\infty$ is never represented by a junk number.
• Proposition 3.1 adds that every $\mathcal A_k$ is nonempty. This is implicit in "finite game", and without it no orbit exists.
• The monotonicity step is stated with $\le$, not the printed $<$.

Trivializing encodings are excluded. Q is not a chosen maximizer that could be chosen badly. Orbit hypotheses are not vacuous: a verification file exhibits an orbit and a strict equilibrium together with a penalty function. Steepness is not added to the hypotheses. The conclusion is genuine convergence $x(t)\to x^*$ together with Lyapunov stability, not a $\liminf$ or a stability-only statement. Proofs of any milestone are welcome. The conjugate and Bregman layer (Appendix C), the regularized-argmax lemmas (Appendix A) and the well-posedness of (RL) (Proposition 3.1) are reusable beyond this mission.

Selected references

• P. Mertikopoulos and W. H. Sandholm, Learning in games via reinforcement and regularization, Math. Oper. Res. 41(4), 2016. Cited as arXiv:1407.6267v2. https://arxiv.org/abs/1407.6267v2
• P. Coucheney, B. Gaujal and P. Mertikopoulos, Penalty-regulated dynamics and robust learning procedures in games, Math. Oper. Res. 40(3), 2015. https://doi.org/10.1287/moor.2014.0687
• J. W. Weibull, Evolutionary Game Theory, MIT Press, 1995. https://mitpress.mit.edu/9780262731218/
• J. Hofbauer and K. Sigmund, Evolutionary Games and Population Dynamics, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9781139173179
• K. C. Kiwiel, Free-steering relaxation methods for problems with strictly convex costs and linear constraints, Math. Oper. Res. 22(2), 1997. https://doi.org/10.1287/moor.22.2.326

Motivation

Learning dynamics in games describe how players who repeatedly interact adjust their strategies from observed payoffs. A central question is whether such dynamics lead to Nash equilibrium. For the replicator dynamics, the canonical model of evolutionary game theory, the answer is negative in general: in Matching Pennies and in generic zero-sum games with a unique interior equilibrium, replicator trajectories cycle forever. A classical positive result survives: if a replicator trajectory of a 2-player game stays a bounded distance away from the boundary of the strategy space, its time average converges to the Nash set (Hofbauer and Sigmund, 1998, Ch. 7).

Mertikopoulos and Sandholm (arXiv:1407.6267v2; Math. Oper. Res. 41(4), 2016) study a broad family of continuous-time learning dynamics, regularized reinforcement learning: each player aggregates payoffs into scores and plays the mixed strategy that maximizes score minus a strongly convex penalty function. The family contains the replicator dynamics (entropic penalty) and the projection dynamics (quadratic penalty). For non-steep penalties, trajectories can enter and leave the boundary of the strategy space infinitely often, so the classical "stay away from the boundary" criterion is no longer natural. Section 6 of the paper replaces it with a condition on scores and derives convergence of time averages in zero-sum games with an interior equilibrium.

Setting

A 2-player finite game $\mathcal G$ has players $k = 1, 2$, finite pure strategy sets $\mathcal A_k$, and payoff functions $u_k$ on pure profiles. A mixed strategy $x_k$ is a probability vector on $\mathcal A_k$; $\mathcal X$ is the set of mixed profiles $x = (x_1, x_2)$ and $u_k(x)$ the expected payoff (2.1). The payoff vector of player $k$ is $v_{k\alpha}(x) = u_k(\alpha; x_{-k})$, the payoff of the pure strategy $\alpha$ against the opponent's mixed strategy (2.2). A profile $x^*$ is a Nash equilibrium if no player gains by a unilateral deviation to another mixed strategy; it is interior if $x^*_{k\alpha} > 0$ for every $k$ and $\alpha$. The game is zero-sum if $u_1 = -u_2$.

On the simplex $\Delta$ of a finite set, a penalty function $h$ (Definition 2.1) is continuous on $\Delta$, smooth on the relative interior of every face, and $K$-strongly convex for some $K > 0$:

$$h(tx_1 + (1-t)x_2) \le t h(x_1) + (1-t) h(x_2) - \tfrac12 K t(1-t)\|x_1 - x_2\|^2 .$$

No steepness is required. The choice map is $Q(y) = \arg\max_{x\in\Delta}\{\langle y|x\rangle - h(x)\}$ (Definition 2.2), the convex conjugate is $h^*(y) = \max_{x\in\Delta}\{\langle y|x\rangle - h(x)\}$ (C.1), and the Fenchel coupling is $F_h(p, y) = h(p) + h^*(y) - \langle y|p\rangle$ (C.10).

Each player $k$ has its own penalty function $h_k$. An orbit of (RL) is a pair of trajectories $(y(t), x(t))$, $t \ge 0$, of score vectors and mixed profiles with

$$\dot y_k(t) = v_k(x(t)), \qquad x_k(t) = Q_k(y_k(t)) .$$

The time average of the orbit is $\bar x(t) = t^{-1}\int_0^t x(s)\,ds$.

Formalization targets

Goal: Proposition 6.2 (p. 26)

If $\mathcal G$ is a 2-player zero-sum game with an interior Nash equilibrium, then for every orbit of (RL),

$$\operatorname{dist}\big(\bar x(t), \mathrm{NE}(\mathcal G)\big) \xrightarrow[t\to\infty]{} 0 .$$

The statement fixes no rate and no particular penalty function: it holds for every choice of $h_1, h_2$.

Milestones

1. Proposition C.1 (p. 33): $Q$ is Lipschitz and $Q = dh^*$.
2. Lemma C.6 (p. 36): along (RL), $\frac{d}{dt}F_{h_k}(p_k, y_k(t)) = \langle v_k(x(t)) | x_k(t) - p_k\rangle$.
3. (6.5) (p. 26): in the goal's setting, $F_h(x^*, y(t)) = \sum_k F_{h_k}(x_k^*, y_k(t))$ is constant.
4. Proposition A.1(iii) (p. 31): $Q_\alpha(y) \to 0$ when $y_\alpha - y_\beta \to -\infty$.
5. Proposition C.5 (pp. 35–36): for interior $p$, bounded $F_h(p, y_j)$ forces bounded score differences.
6. Theorem 6.1 (p. 25): in any 2-player game, bounded score differences imply convergence of $\bar x(t)$ to the Nash set.

Significance

The result. Proposition 6.2 shows that the time-average convergence known for the replicator dynamics in zero-sum games is a property of the whole class of regularized reinforcement learning schemes, including those whose trajectories hit the boundary of the strategy space infinitely often, such as the projection dynamics. Time-averaged play of no-regret-type dynamics in zero-sum games is the continuous-time counterpart of the standard argument that averaged learning computes minimax strategies. Theorem 6.1 isolates the mechanism for general 2-player games: bounded score differences suffice, with no zero-sum assumption.

Formalizing it. The results are proved in the paper; none has a machine-checked proof. A complete formalization produces reusable components: differentiability of the conjugate of a strongly convex function on the simplex (a Danskin-type statement), the Fenchel-coupling identity along the dynamics, and a conservation law for zero-sum games. These are the building blocks of many analyses of mirror-descent and follow-the-regularized-leader dynamics.

Difficulty

The first idea, comparing $x(t)$ itself with the equilibrium, fails: $x(t)$ need not converge, and for non-steep penalties it does not stay in the interior, so the Kullback–Leibler argument used for the replicator dynamics is unavailable. The conserved quantity is a function of the scores $y(t)$, not of $x(t)$, and turning its boundedness into control of score differences requires the asymptotic behaviour of the choice map when some scores diverge. The second difficulty is analytic: $h$ is not differentiable at the boundary of $\Delta$, yet $h^*$ must be differentiable everywhere on the score space, with derivative $Q$, for the chain rule along (RL) to apply. Finally, the passage from score differences to the time average uses that $v_k$ is linear in the single opponent's strategy, which is specific to two players.

Formalization scope

• Game. Players are Fin 2, strategy types A k are finite, payoffs are real functions on pure profiles; mixed profiles, expected payoffs and mixed Nash equilibria come from the published agt_games vocabulary (AGT.IsMixedNash). Zero-sum is $u_0(s) + u_1(s) = 0$ for every pure profile; interiority is $x^*_{k\alpha} > 0$.
• Penalty functions. IsPenalty h K is Definition 2.1 with strong convexity in the Euclidean norm; since $K$ is existential the class does not depend on the norm. Steepness is not assumed. Each player has its own $h_k$.
• Choice map and orbits. $x = Q(y)$ is the predicate IsChoice h y x (maximizer of $\langle y|x\rangle - h(x)$ over $\Delta$), never a chosen argmax. An orbit is IsRLOrbit u h y x: for $t \ge 0$, $x_k(t) = Q_k(y_k(t))$ and $\dot y_{k\alpha}(t) = v_{k\alpha}(x(t))$, a right derivative at $t = 0$. This differential form is equivalent to the integral form (RL) because $x$ is continuous along an orbit.
• Time average and convergence. $\bar x(t)$ is defined coordinatewise with the interval integral; only $t \to \infty$ is used. Convergence to the Nash set is Metric.infDist $\to 0$ in the sup metric on profiles. For Theorem 6.1, which has no equilibrium among its hypotheses, the conclusion also asserts that the Nash set is nonempty, because the distance to the empty set is $0$ in Lean.
• Ruled out. A chosen argmax for $Q$, orbits that are vacuous, steepness added to the penalty, convergence of a subsequence or a liminf in place of the limit, and a Nash set that may be empty are all excluded by the encoding. A sorry-free check exhibits a game, penalty functions and an orbit satisfying all hypotheses of the goal, and verifies that Matching Pennies has the interior equilibrium $((\tfrac12,\tfrac12),(\tfrac12,\tfrac12))$.
• Not included. Theorem 6.3 (chain transitivity under the best-response dynamics) depends on the theory of perturbed solutions of differential inclusions, which is not available. Proposition 6.4 is omitted (see the mission notes).

Contributions are welcome on any milestone; Proposition C.1 and Proposition A.1(iii) are self-contained convex-analysis statements about a single penalty function.

Selected references

• P. Mertikopoulos and W. H. Sandholm, Learning in games via reinforcement and regularization, Mathematics of Operations Research 41(4), 2016. Preprint arXiv:1407.6267v2 (cited version). https://arxiv.org/abs/1407.6267
• J. Hofbauer and K. Sigmund, Evolutionary Games and Population Dynamics, Cambridge University Press, 1998. https://doi.org/10.1017/CBO9781139173179
• J. Hofbauer, S. Sorin and Y. Viossat, Time average replicator and best-reply dynamics, Mathematics of Operations Research 34(2), 2009. https://doi.org/10.1287/moor.1080.0359
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Why projection methods for variational inequalities

A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. It is the common form of convex minimization (with $F$ a gradient), of saddle-point problems (with $F$ the monotone operator of a convex–concave function), of Nash equilibria of convex games, of complementarity problems and of traffic and economic equilibria. Iterative methods that use only evaluations of $F$ and projections onto the feasible set are the methods of choice when the problem is large, because each step is cheap.

The classical such method, the projected gradient iteration $x_{n+1}=P_C(x_n-\lambda F(x_n))$, does not converge for merely monotone $F$. Korpelevich's extragradient method (1976) does, at the price of two projections and two evaluations of $F$ per step, and it is known to converge R-linearly under strong monotonicity (Tseng 1995, reference [19] of the paper). Popov (1980), Tseng (2000) and Censor–Gibali–Reich (2011) reduced the number of projections or evaluations. Yu. Malitsky's projected reflected gradient method (arXiv:1502.04968, SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) uses one projection and one evaluation of $F$ per step, evaluating $F$ at the reflected point $2x_n-x_{n-1}$ instead of at $x_n$. This mission formalizes the paper's second main result: under strong monotonicity the method keeps the R-linear rate of the extragradient method.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, let $C\subseteq H$ be closed and convex, and let $F:H\to H$. The metric projection $P_C(z)$ is the unique point of $C$ nearest to $z$. The variational inequality (1.1) is

$$\text{find } x^*\in C\ \text{ such that }\ \langle F(x^*),\,x-x^*\rangle\ \ge\ 0\quad\text{for all } x\in C,$$

with solution set $S$. The paper's standing assumptions for this result are

• (C1) $S\neq\emptyset$;
• (C2*) $F$ is strongly monotone with modulus $m>0$: $\langle F(x)-F(y),x-y\rangle\ge m\|x-y\|^2$ for all $x,y\in H$;
• (C3) $F$ is Lipschitz with constant $L>0$: $\|F(x)-F(y)\|\le L\|x-y\|$ for all $x,y\in H$.

Algorithm 3.1 chooses $x_0=y_0\in H$ and a step $\lambda\in\big(0,(\sqrt2-1)/L\big)$ and iterates

$$x_{n+1}=P_C\big(x_n-\lambda F(y_n)\big),\qquad y_{n+1}=2x_{n+1}-x_n .$$

The Lean development names these objects proj, solSet, IsStronglyMonotoneMap, IsLipschitzMap and IsPRGRun in the namespace ProjReflGrad.Linear.

Formalization targets

Goal: Theorem 3.3 (p. 6)

Under (C1), (C2*), (C3) and $0<\lambda<(\sqrt2-1)/L$, every run of Algorithm 3.1 converges to the solution $z$ of (1.1) at least R-linearly:

$$\exists\,\gamma\in(0,1),\ M>0:\qquad \|x_n-z\|\ \le\ M\gamma^n\quad\text{for all } n\ge0 .$$

The goal fixes neither $\gamma$ nor $M$; the proof produces them from $\lambda$, $L$ and $m$, but the theorem asserts only the shape of the rate.

Milestones

In attack order:

1. Uniqueness (p. 6): under (C2*) the solution set has at most one point.
2. The identity for $\|y_n-z\|^2$ (p. 6, via Lemma 2.5): $\|y_n-z\|^2=2\|x_n-z\|^2-\|x_{n-1}-z\|^2+2\|x_n-x_{n-1}\|^2\ge2\|x_n-z\|^2-\|x_{n-1}-z\|^2$.
3. (3.8) (p. 7): the strong-monotonicity estimate at $y_n$ with a free modulus $m_1\in(0,m]$.
4. (3.2) (p. 4): $\|x_{n+1}-z\|^2\le\|x_n-z\|^2-\|x_{n+1}-x_n\|^2-2\lambda\langle F(y_n),x_{n+1}-z\rangle$.
5. (3.4) (p. 5): $2\lambda\langle F(y_{n-1}),y_n-x_{n+1}\rangle\le\|x_{n+1}-x_n\|^2-\|x_n-y_n\|^2-\|x_{n+1}-y_n\|^2$, $n\ge2$.
6. (3.5) (p. 5): the Lipschitz estimate of $2\lambda\langle F(y_n)-F(y_{n-1}),y_n-x_{n+1}\rangle$.
7. (3.9) (p. 7): the two-step recursion $a_{n+1}+b_{n+1}\le(1-2\alpha)a_n+\alpha a_{n-1}+\beta b_n$ in the iterates, with $\beta=\max\{\lambda L/(1-\sqrt2\lambda L),\tfrac12\}$.
8. Lemma 2.8 (p. 3): a nonnegative pair of sequences satisfying that recursion for all $\alpha\in(0,\alpha_0)$ has $a_n\le\gamma^nM$.

Significance

The result. Theorem 3.3 shows that halving the per-step cost of the extragradient method does not cost the linear rate under strong monotonicity. For strongly monotone problems (strongly convex minimization, strongly convex–strongly concave saddle points, strictly monotone games with a quadratic margin) the method therefore reaches accuracy $\varepsilon$ in $O(\log(1/\varepsilon))$ iterations with one projection each, which matters when projecting onto $C$ dominates the cost. The two-step recursion (3.9) and Lemma 2.8 are also a reusable template: the same mechanism gives linear rates for other methods with a memory of one past iterate.

Formalizing it. The theorem is proved in the paper; nothing here is open. No machine-checked proof of it, or of its lemmas, is on the platform. A formal proof needs the projection inequality in a general real Hilbert space, a careful account of the reflected iterate, and a rigorous version of Lemma 2.8, whose printed proof leaves the range of $n$ and the positivity of $M$ implicit. The deliverable is a checked R-linear rate for a one-projection method in infinite dimension.

Difficulty

The natural first attempt, a contraction $\|x_{n+1}-z\|\le q\|x_n-z\|$ (Q-linear convergence), is not what the paper proves and is not available: the reflected point $y_n$ depends on $x_{n-1}$, so the error at step $n+1$ is controlled only by the errors at steps $n$ and $n-1$, together with auxiliary terms $\|x_n-y_{n-1}\|^2$ and $\langle F(z),x_{n-1}-z\rangle$. Strong monotonicity is applied at $y_n$, not at $x_n$, and $\|y_n-z\|^2$ can be smaller than $\|x_n-z\|^2$; the lower bound $2\|x_n-z\|^2-\|x_{n-1}-z\|^2$ may even be negative. The step range $\lambda<(\sqrt2-1)/L$ is exactly what keeps the coefficients of the Lipschitz error terms below the gain from the projection inequality, and the resulting two-step recursion needs Lemma 2.8, with its choice of $\gamma$ and $\delta$, to yield a geometric bound.

Formalization scope

• $H$ is a general real inner product space, complete where a projection is used ([CompleteSpace H]); it is never specialized to $\mathbb R^n$.
• $P_C$ is defined by choice as a nearest point, returning its argument when none exists; every statement using it assumes $C$ closed, convex and nonempty (through $z\in C$, $C\neq\emptyset$, or (C1)), so the junk value is never reached.
• Runs of Algorithm 3.1 are infinite sequences without the stopping rule; a stopped run continues as a constant sequence. $x_0$ is any point of $H$, as in the paper, so statements that need $x_{n-1}\in C$ are stated for $n\ge2$.
• (C2*) and (C3) are required on all of $H$ with real constants $m>0$, $L>0$ (not LipschitzWith, whose $\mathbb R_{\ge0}$ constant admits $L=0$). (C1) stays in the goal: it is the paper's assumption and its only source of $C\neq\emptyset$.
• R-linear convergence means domination by $M\gamma^n$ with $0<\gamma<1$ and $M>0$; a goal allowing $\gamma=1$, $\gamma=0$ or only an $O(\cdot)$ bound would be a different and weaker (or trivially false) statement and is ruled out. The goal does not mention the auxiliary sequences $a_n,b_n$, the constants $\beta,m_1,\alpha_0$, or Lemma 2.8.
• Departures from the page are recorded in each item's Formalization Note: the ranges $n\ge1$/$n\ge2$, the range $n\ge1$ of (2.1) in Lemma 2.8, the proof's "Lemma 2.1" that means Lemma 2.8, and "$m_1$ arbitrary in $(0,m)$" where the argument uses $(0,m]$.
• The projection theorem (existence and characterization of the nearest point) is the published Proved theorem VectorSpaceOpt.min_distance_convex_set, included as a reference. Contributions welcome: proofs of the milestones in any order; Lemma 2.8 and the identity of milestone 2 are self-contained.

Selected references

• Yu. Malitsky, Projected Reflected Gradient Methods for Monotone Variational Inequalities, SIAM J. Optim. 25(1), 2015. arXiv:1502.04968v1. https://arxiv.org/abs/1502.04968 , https://doi.org/10.1137/14097238X
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12, 747–756, 1976.
• P. Tseng, On linear convergence of iterative methods for the variational inequality problem, J. Comput. Appl. Math. 60, 237–252, 1995.
• L. D. Popov, A modification of the Arrow–Hurwicz method for finding saddle points, Math. Notes 28, 845–848, 1980.
• Y. Censor, A. Gibali, S. Reich, The subgradient extragradient method for solving variational inequalities in Hilbert space, J. Optim. Theory Appl. 148, 318–335, 2011.

Motivation

Many problems in optimization, game theory and mechanics come down to a variational inequality: find a point of a convex set at which a given vector field points "inward" against every feasible direction. Constrained convex minimization (where the field is a gradient), saddle-point problems (where it is the gradient of a convex–concave function with one sign flipped), Nash equilibria of convex games and complementarity problems are all of this form. In large-scale and infinite-dimensional settings the methods of choice are projection methods, which use only evaluations of the field and projections onto the feasible set.

The plain projected gradient iteration $x_{n+1}=P_C(x_n-\lambda F(x_n))$ does not converge for merely monotone fields: on a rotation field in the plane it spirals outward for every step size. Korpelevich's extragradient method (1976) repairs this with two field evaluations and two projections per iteration. Later methods (Tseng's forward–backward–forward method, 2000; the subgradient extragradient method of Censor, Gibali and Reich, 2011) reduce the number of projections to one, but still need two evaluations of the field.

Yu. Malitsky's paper (arXiv:1502.04968, SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) introduces the projected reflected gradient method, which uses one projection and one field evaluation per iteration, evaluated at a "reflected" point, and proves that it converges weakly under the same assumptions as the extragradient method. This mission formalizes that convergence theorem, Theorem 3.2 of the paper.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $C\subseteq H$ be closed and convex, and let $F:H\to H$ be a mapping. For $z\in H$, the metric projection $P_C(z)$ is the unique point of $C$ nearest to $z$ (it exists when $C$ is nonempty). The variational inequality (1.1) asks for $x^*\in C$ with

$$\langle F(x^*),\,x-x^*\rangle\ \ge\ 0\qquad\text{for all }x\in C,$$

and $S$ denotes its solution set. The standing assumptions are:

• (C1) $S$ is nonempty;
• (C2) $F$ is monotone: $\langle F(x)-F(y),x-y\rangle\ge0$ for all $x,y\in H$;
• (C3) $F$ is Lipschitz continuous with a constant $L>0$: $\|F(x)-F(y)\|\le L\|x-y\|$ for all $x,y\in H$.

Algorithm 3.1 (projected reflected gradient method). Fix a step size $\lambda\in\big(0,(\sqrt2-1)/L\big)$ and a starting point $x_0=y_0\in H$, and iterate

$$x_{n+1}=P_C\big(x_n-\lambda F(y_n)\big),\qquad y_{n+1}=2x_{n+1}-x_n .$$

The point $y_{n+1}$ is the reflection of $x_n$ through $x_{n+1}$. A sequence $(x_n)$ converges weakly to $x^*$, written $x_n\rightharpoonup x^*$, if $\langle x_n,v\rangle\to\langle x^*,v\rangle$ for every $v\in H$.

Formalization targets

Goal: Theorem 3.2 (p. 5)

Under (C1)–(C3), for $0<\lambda<(\sqrt2-1)/L$ and every run of Algorithm 3.1 there is $x^*\in S$ with

$$x_n\rightharpoonup x^* .$$

Milestones

In the order the proof uses them:

1. Lemma 2.1 (i), p. 3: $\langle P_Mx-x,\,y-P_Mx\rangle\ge0$ for $y\in M$ (already proved on the platform, referenced).
2. Lemma 2.1 (ii), p. 3: $\|P_Mx-y\|^2\le\|x-y\|^2-\|x-P_Mx\|^2$ for $y\in M$.
3. Lemma 3.1, p. 4: for $z\in S$ and $n\ge2$,

$$\|x_{n+1}-z\|^2\le\|x_n-z\|^2-\big(1-\lambda L(1+\sqrt2)\big)\|x_n-x_{n-1}\|^2+\lambda L\|x_n-y_{n-1}\|^2-\big(1-\sqrt2\lambda L\big)\|x_{n+1}-y_n\|^2-2\lambda\langle F(z),y_n-z\rangle .$$

4. (3.6), p. 5: the descent inequality $a_{n+1}\le a_n-b_n$ with $a_n=\|x_n-z\|^2+\lambda L\|x_n-y_{n-1}\|^2+2\lambda\langle F(z),x_{n-1}-z\rangle$ and $b_n=(1-\lambda L(1+\sqrt2))\|x_n-x_{n-1}\|^2$.
5. Lemma 2.7, p. 3: nonnegative sequences with $a_{n+1}\le a_n-b_n$ have $(a_n)$ bounded and $b_n\to0$.
6. Proof of Theorem 3.2, pp. 5–6: $(x_n)$ is bounded, $\|x_{n+1}-x_n\|\to0$ and $\|x_{n+1}-y_n\|\to0$.
7. Lemma 2.2 (Minty), p. 3: for continuous monotone $F$, $x^*\in S$ iff $x^*\in C$ and $\langle F(y),y-x^*\rangle\ge0$ for all $y\in C$.
8. (3.7), p. 6: every weak cluster point of $(x_n)$ lies in $S$.
9. Proof of Theorem 3.2, p. 6: for each $z\in S$, $\|x_n-z\|^2+2\lambda\langle F(z),x_{n-1}-z\rangle$ converges.
10. Lemma 2.3 (Opial), p. 3: if $x_n\rightharpoonup x$ and $y\ne x$, then $\liminf\|x_n-x\|<\liminf\|x_n-y\|$.

Companion items, not milestones: the defined projection is the metric projection (so runs of Algorithm 3.1 exist from every starting point), Remark 2.1 ($S$ is closed and convex), and the characterization of $S$ as the zeros of the projected residual $r(x,y)=\|y-P_C(x-\lambda F(y))\|+\|x-y\|$ (§3, p. 4).

Significance

The result. Theorem 3.2 shows that a monotone Lipschitz variational inequality in Hilbert space can be solved by an iteration costing one projection and one evaluation of $F$ per step, the minimum for a projection method, with no knowledge beyond the Lipschitz constant. This halves the cost of each iteration relative to the extragradient method when evaluating $F$ is expensive, and keeps the cost of projections at one when projecting onto $C$ is expensive. The method and its analysis became the basis for several later algorithms, including the adaptive variant in §4 of the same paper and the golden ratio algorithm of Malitsky (2020).

Formalizing it. The theorem is proved in the paper; no machine-checked proof is known to exist. The formal development needs, beyond the main argument, a usable library of facts about projections onto closed convex sets in Hilbert space, weak convergence of sequences (boundedness of weakly convergent sequences, weak sequential compactness of bounded sets) and Opial's property. These are reused by every weak-convergence proof for splitting and projection methods, and several companion missions of this series and of related papers rely on the same facts.

Difficulty

The naive Lyapunov function $\|x_n-z\|^2$ is not monotone along the iteration: because $F$ is evaluated at the reflected point $y_n$ rather than at $x_n$, the cross terms do not cancel as they do for the extragradient method. The quantity that does decrease (milestones 3–4) carries extra terms, and the step bound $(\sqrt2-1)/L$ is what the decrease requires. As a consequence, $\|x_n-z\|$ itself is not known to converge, so the standard Opial lemma ("if $\|x_n-z\|$ converges for every $z\in S$ and all weak cluster points lie in $S$, then $x_n$ converges weakly") does not apply directly; the uniqueness of the weak cluster point has to be argued with the perturbed quantity and Opial's inequality. In infinite dimension, the weak cluster point step also needs weak sequential compactness of bounded sets, which is not norm compactness.

Formalization scope

• $H$ is an arbitrary real inner product space with [CompleteSpace H] in every statement that needs completeness; it is never specialised to $\mathbb R^n$, where weak and norm convergence coincide.
• Weak convergence is stated elementarily: $\langle x_n,v\rangle\to\langle x^*,v\rangle$ for every $v\in H$. Subsequences are $x\circ\varphi$ with $\varphi$ strictly increasing.
• The projection $P_C(z)$ is defined by choice as a nearest point, with the junk value $z$ when none exists. Every statement that uses it assumes $C$ closed, convex and nonempty (directly or through $S\ne\emptyset$ or $z\in S$), and a companion item certifies that it is then the metric projection.
• (C2) and (C3) are imposed on all of $H$, as in the paper; $L$ is a real number with $L>0$, and the step range $0<\lambda<(\sqrt2-1)/L$ is strict on both sides.
• Runs of Algorithm 3.1 carry no stopping rule: a run reaching a solution $x_n=y_n\in S$ stays constant, so infinite runs subsume stopped ones. The starting point $x_0$ is any point of $H$, not necessarily in $C$; for this reason Lemma 3.1 and (3.6) are stated for $n\ge2$, which is the range the proof of Theorem 3.2 uses.
• Opial's inequality is stated with liminfs in $[0,\infty]$, where they are always defined.
• A trivializing formalization is ruled out: the goal assumes exactly (C1)–(C3), closedness and convexity of $C$ and the step range, and concludes weak convergence to a point of $S$; it does not assume boundedness of the iterates, a starting point in $C$, finite dimension, or any of the intermediate estimates.

Contributions welcome: proofs of the milestones in any order; general Hilbert-space lemmas (boundedness of weakly convergent sequences via the uniform boundedness principle, weak sequential compactness of bounded sets, Opial's inequality) are useful well beyond this mission.

Selected references

• Yu. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM J. Optim. 25(1) (2015), 502–520. arXiv:1502.04968, doi:10.1137/14097238X
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12 (1976), 747–756.
• P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38(2) (2000), 431–446. doi:10.1137/S0363012998338806
• Y. Censor, A. Gibali, S. Reich, The subgradient extragradient method for solving variational inequalities in Hilbert space, J. Optim. Theory Appl. 148 (2011), 318–335. doi:10.1007/s10957-010-9757-3
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73 (1967), 591–597. doi:10.1090/S0002-9904-1967-11761-0
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. doi:10.1007/978-3-319-48311-5

Motivation

Many engineered and natural systems are networks of identical dynamical units coupled through a directed interaction graph: arrays of oscillators, power grids, sensor and multi-agent networks, gene regulatory circuits. A basic control question for such a network is how to force every unit onto a prescribed reference trajectory (an equilibrium, a periodic orbit or a chaotic solution of a single unit) by acting on only a few of them. Applying a feedback controller to a small fraction of the vertices and letting the coupling spread its effect is called pinning control. It was introduced for scale-free networks by Wang and Chen (2002), shown to work with a single controller on undirected networks by Chen, Liu and Lu (2007), and turned into checkable criteria for undirected networks by Yu, Chen and Lü (2009).

Directed networks are harder. Earlier criteria for directed networks (Zhou, Lu and Lü 2008; Song and Cao 2010) were stated through the symmetric part $G+G^T$ of the coupling matrix, which may have eigenvalues with positive real part even when the network synchronizes, so they lose the structural information of the graph. Yu, Chen, Lü and Kurths (SIAM J. Control Optim., 2013) replaced the standard quadratic Lyapunov function by one weighted with the positive left null vector of the coupling matrix. This mission formalizes their main criterion for strongly connected networks (§3 of the paper) together with the matrix-theoretic lemmas it rests on (§2).

Setting

The network has $N$ vertices with states $x_i(t)\in\mathbb R^n$. A coupling matrix $G=(G_{ij})\in\mathbb R^{N\times N}$ has $G_{ij}\ge 0$ for $i\ne j$ ($G_{ij}>0$ means a connection from vertex $j$ to vertex $i$) and zero row sums, $G_{ii}=-\sum_{j\ne i}G_{ij}$. The network is strongly connected if any vertex can be reached from any other by a directed path; $G$ is irreducible if no simultaneous permutation of rows and columns brings it to block lower-triangular form $\begin{pmatrix}\tilde G_{11}&0\\\tilde G_{21}&\tilde G_{22}\end{pmatrix}$ with square diagonal blocks of sizes $m$ and $N-m$, $1\le m\le N-1$. The in-degree of vertex $i$ is $k_i^{\mathrm{in}}=\sum_{j\ne i}G_{ij}$.

Each vertex runs the dynamics $\dot x=f(x,t)$ for a continuously differentiable $f:\mathbb R^n\times\mathbb R_+\to\mathbb R^n$. A reference trajectory $s$ solves $\dot s=f(s,t)$. With coupling strength $c$, inner coupling matrix $\Gamma\in\mathbb R^{n\times n}$ and control 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.$$

It is globally synchronized if $x_i(t)-s(t)\to0$ for every $i$, every reference trajectory and every solution. The vector field satisfies Assumption 1 if, for a constant matrix $K$,

$$(x-y)^T\bigl(f(x,t)-f(y,t)\bigr)\le(x-y)^TK\Gamma(x-y)\qquad\forall x,y\in\mathbb R^n,\ t\ge0 .$$

For positive weights $\xi_1,\dots,\xi_N$ put $\Xi=\operatorname{diag}(\xi)$, $D=\operatorname{diag}(d)$ and $\widehat G=\tfrac12(\Xi G+G^T\Xi)$.

Formalization targets

Goal: Theorem 3.1 (p. 1402)

Let $f$ satisfy Assumption 1 with $\Gamma$ symmetric, let $G$ be a strongly connected coupling matrix, and let $\xi$ be positive with $\widehat G$ having zero row sums (the weights of Lemma 2.12). If

$$\Xi\otimes\frac{K\Gamma+\Gamma^TK^T}{2}+c\,\widehat G\otimes\frac{\Gamma+\Gamma^T}{2}-c\,(\Xi D)\otimes\frac{\Gamma+\Gamma^T}{2}<0,$$

then the controlled network is globally synchronized.

Milestones

The path to the goal follows the paper: Lemma 2.5 (irreducible $\iff$ strongly connected), Lemma 2.9 ($\rho(A)=\|A\|_\infty$ for nonnegative $A$ with constant row sums), Lemma 2.8 (Perron–Frobenius, already on the platform), Lemma 2.11 (a positive vector $x$ with $G^Tx=0$), Lemma 2.12 (the weights $\Xi$), and the derivative estimate (3.4) for $V=\tfrac12\sum_i\xi_ie_i^Te_i$, $e_i=x_i-s$:

$$\dot V\le e^T\bigl[\Xi\otimes(K\Gamma)+c(\widehat G-\Xi D)\otimes\Gamma\bigr]e .$$

Companion results

Lemma 2.7, Lemma 2.10, and, under the paper's standing assumptions ($K\Gamma=\Gamma K$, $\theta=\lambda_{\max}(\tfrac{K+K^T}{2})\ge0$) with $\Gamma$ positive definite: Corollary 3.2 (the $N\times N$ condition $\theta\Xi+c(\widehat G-\Xi D)<0$ suffices), Corollary 3.3 (i) (an explicit coupling threshold $c>\lambda_{\max}(\theta\Xi)/|\lambda_{\max}(\widehat G-\Xi D)|$), and Corollary 3.4 (the necessary conditions $d_i>\theta/c-k_i^{\mathrm{in}}$ at pinned and $k_i^{\mathrm{in}}>\theta/c$ at unpinned vertices).

Significance

The criterion reduces global synchronization of an $nN$-dimensional nonlinear system to one linear matrix inequality in the data $(G,\Gamma,K,c,D)$, and the corollaries reduce it further to an $N\times N$ inequality and to explicit bounds. Corollary 3.4 turns this into a pinning rule: vertices whose in-degree is below $\theta/c$ must be controlled. Weighting by the left null vector of $G$ is the device that later work on directed consensus and pinning reuses; Lemmas 2.11 and 2.12 isolate it as a statement about Metzler matrices.

The paper's results are proved on paper; none of them has a machine-checked proof that this mission is aware of. A formalization adds three things: a corrected statement of Theorem 3.1 (see the scope section), a Lean library of directed-network matrix facts (irreducibility in the permutation form, its equivalence with strong connectivity, positive left null vectors, the weighted symmetrization $\widehat G$), and a reusable Lyapunov argument for linearly coupled networks with Kronecker-structured quadratic forms.

Difficulty

The obvious first idea, the unweighted Lyapunov function $\tfrac12\sum_ie_i^Te_i$, produces the symmetric part of $G$, which for a directed network need not be negative semidefinite; this is exactly the defect of earlier criteria. The weights must come from a positive left null vector of $G$, whose existence is a Perron–Frobenius statement that needs irreducibility, hence the graph–matrix equivalence of Lemma 2.5. The analytic part needs a derivative of $V$ along solutions on $[0,\infty)$, the conversion of a sum over vertices into a Kronecker quadratic form, and the passage from a negative definite form to convergence of every error component. On the Mathlib side, irreducibility in the paper's permutation sense, spectral radius through characteristic roots, and largest eigenvalues of symmetric matrices all have to be connected to existing API.

Formalization scope

States are Fin n → ℝ and matrices are indexed by Fin N, Fin n and, for Kronecker products, by pairs (i, a) with $(A\otimes B)_{(i,a),(j,b)}=A_{ij}B_{ab}$; the stacked error uses the same order. Convergence (2.7) is stated with the neighbourhood filter of $0$ in $\mathbb R^n$, which does not depend on the norm. Derivatives are taken within $[0,\infty)$. Pinning is encoded by $d_i>0$ instead of the paper's reordering of the first $l$ vertices. "$M<0$" is positive definiteness of $-M$ (Mathlib PosDef, which includes symmetry); every matrix compared with $0$ is symmetric by construction. $\lambda_{\max}(A)$ of a symmetric matrix is the least $r$ with $v^TAv\le r\,v^Tv$ for all $v$; $\rho(A)$ is the largest modulus of a complex characteristic root. Global synchronization quantifies over every reference solution and every network solution; existence of solutions is not asserted.

Added hypotheses, each disclosed in the item: $\Gamma^T=\Gamma$ in Theorem 3.1 and (3.4), because the printed theorem allows any $\Gamma$ and is then false (a directed 3-cycle with $\Gamma=\begin{pmatrix}1&3\\-3&1\end{pmatrix}$ satisfies (3.2) but its error grows); $c>0$ in Corollary 3.4; at least one pinned vertex in Corollary 3.3 (i); $N\ge1$ in Lemma 2.10. The weights $\Xi$ are not arbitrary: Theorem 3.1 and the corollaries require $\widehat G$ to have zero row sums, which for a coupling matrix is equivalent to $G^T\xi=0$. Assuming the derivative bound (3.4), negative definiteness of $\widehat G-\Xi D$ or decay of $V$ in the goal would trivialize it and is excluded.

The mission needs: graph reachability for matrices with nonnegative off-diagonal entries; Perron–Frobenius for irreducible nonnegative matrices (referenced from the platform); Gershgorin-type bounds; Kronecker products and positive definiteness; and calculus of quadratic forms along solutions. The matrix lemmas (2.5, 2.7, 2.9–2.12) are reusable beyond this mission. Proofs of any item, and alternative proofs of the milestones, are welcome. Corollary 3.3 (ii) is not posed.

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 (2007), 1317–1326. https://doi.org/10.1109/TCSI.2007.895383
• J. Zhou, J. Lu, J. Lü, Pinning adaptive synchronization of a general complex dynamical network, Automatica 44 (2008), 996–1003. https://doi.org/10.1016/j.automatica.2007.08.016
• W. Yu, G. Chen, J. Lü, On pinning synchronization of complex dynamical networks, Automatica 45 (2009), 429–435. https://doi.org/10.1016/j.automatica.2008.07.016
• Q. Song, J. Cao, On pinning synchronization of directed and undirected complex dynamical networks, IEEE Trans. Circuits Syst. I 57 (2010), 672–680. https://doi.org/10.1109/TCSI.2009.2024971
• R. Olfati-Saber, R. M. Murray, Consensus problems in networks of agents with switching topology and time-delays, IEEE Trans. Automat. Control 49 (2004), 1520–1533. https://doi.org/10.1109/TAC.2004.834113
• R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985. https://doi.org/10.1017/CBO9780511810817
• R. A. Brualdi, H. J. Ryser, Combinatorial Matrix Theory, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9781107325708