Operations Research

Why streaming revenue is a cooperative-game question

Music streaming platforms collect a subscription fee from each user and have to pass the revenue on to the artists whose content was played. The two rules used in practice are pro-rata (each artist is paid in proportion to their total number of streams, over all users) and user-centric (each user's fee is split among the artists that user played, in proportion to that user's streams). Which rule is fair has been debated by platforms, rights holders and regulators. Bergantiños and Moreno-Ternero (arXiv:2310.11861, Management Science, 2025) study the problem axiomatically, and in their §4 also through cooperative game theory: they associate a transferable-utility game with every streaming problem and ask which revenue allocations no coalition of artists could object to.

This mission formalizes their Theorem 2. It gives an explicit description of the core of that game.

Setting

There are $n$ artists $N=\{1,\dots,n\}$ and a finite set $M$ of users, each of whom pays $1$, so $m=|M|$ is to be shared. A streaming problem records the number $t_{ij}\in\mathbb N$ of times user $j$ played artist $i$. Every user in $M$ is assumed to have played at least one artist.

• The list of user $j$ is $L^j=\{i\in N:t_{ij}>0\}$, the artists that user played.
• The streaming game gives a coalition $S\subseteq N$ of artists the fees of the users who played only artists in $S$:

$$v(S)=\bigl|\{j\in M: L^j\subseteq S\}\bigr|.$$

This is a pessimistic estimate of what a group of artists could earn by leaving to found its own platform. Because every list is nonempty, $v(\emptyset)=0$.

• The core of $v$ is the set of payoff vectors $x\in\mathbb R^N$ that distribute exactly $v(N)=m$ and give every coalition at least its worth:

$$C(N,v)=\Bigl\{x:\ \sum_{i\in N}x_i=v(N),\ \sum_{i\in S}x_i\ge v(S)\ \text{for all } S\subseteq N\Bigr\}.$$

• The allocation set $A(N,M,t)$ consists of the vectors $x=\sum_{j\in M}x^j$, where each $x^j\in\mathbb R^N$ is nonnegative, vanishes outside $L^j$, and sums to $1$. Each user's fee is split in any way among the artists that user played, and the shares are added up.

The proof goes through two classical objects of cooperative game theory. The Harsanyi dividends are $\Delta_v(R)=\sum_{S\subseteq R}(-1)^{|R|-|S|}v(S)$. A sharing system $p=(p^R)_{\emptyset\ne R\subseteq N}$ assigns to each nonempty coalition $R$ a probability vector $p^R$ supported on $R$. The Harsanyi set $H(N,v)$ is the set of allocations $y^p_i=\sum_{R\ni i}\Delta_v(R)\,p^R_i$ that a sharing system induces. The unanimity game $u_R$ has $u_R(S)=1$ if $R\subseteq S$ and $0$ otherwise.

Formalization targets

Goal: Theorem 2 (p. 14)

$$C(N,v)=A(N,M,t)\qquad\text{for every streaming problem }(N,M,t).$$

Milestones (the proof in the paper's appendix, pp. 22–23)

1. Harsanyi (1959). For every TU game, $v=\sum_{\emptyset\ne R\subseteq N}\Delta_v(R)\,u_R$, and these weights are unique.
2. Vasil'ev (1981). If $\Delta_v(R)\ge 0$ for every nonempty $R$, then $C(N,v)=H(N,v)$.
3. The streaming game decomposes as $v=\sum_{\emptyset\ne R\subseteq N}|\{j\in M:L^j=R\}|\,u_R$.
4. Its dividends are $\Delta_v(R)=|\{j\in M:L^j=R\}|\ge 0$.
5. $H(N,v)\subseteq A(N,M,t)$.
6. $A(N,M,t)\subseteq H(N,v)$.
7. Companion (§4, p. 13): $v$ is a convex (supermodular) game.

Significance

Theorem 2 says that the core-stable allocations of streaming revenue are exactly those that split each user's fee among the artists that user played. The user-centric rule is such a split, so its rewards always lie in the core. The pro-rata rule can fall outside the core: in the paper's Example 1 a coalition of one artist receives less than the fee of the user who played only that artist. This observation underlies the paper's Theorem 3, where core selection together with homogeneity and additivity characterizes the user-centric index. Beyond streaming, the theorem gives an explicit core for a class of games built from users' lists. The museum-pass games of Ginsburg and Zang have the same structure.

The paper's proof combines two cited classical theorems (Harsanyi's unanimity decomposition and Vasil'ev's identification of core and Harsanyi set for games with nonnegative dividends) with bookkeeping specific to streaming. None of these is formalized on the platform except the bare existence of a unanimity decomposition (Young 1985's exists_unanimity_expansion, Proved, referenced here). The mission therefore produces reusable statements of Harsanyi dividends, the Harsanyi set and Vasil'ev's theorem for arbitrary finite TU games, as well as the streaming result itself.

Difficulty

Most of the mission is finite bookkeeping: Möbius inversion over the subset lattice and regrouping sums by users' lists. The central difficulty is the inclusion $C(N,v)\subseteq H(N,v)$ in Vasil'ev's theorem. One has to show that every core vector can be generated by splitting each dividend among the members of its coalition. This is a feasibility statement for a transportation problem whose supplies are the dividends and whose demands are the core payoffs, with each coalition allowed to ship only to its own members. The core inequalities have to be turned into such a shipment plan, and neither of the obvious candidates does that. Splitting each dividend equally among a coalition's members gives the Shapley value, a single point. Taking extreme points of the core gives the marginal vectors, and writing an arbitrary core point through them is the same feasibility question again. The paper cites the result without proof.

Formalization scope

• Artists and users. Artists are Fin n, numbered from $0$. Users are named by natural numbers. A problem is a finitely supported map t : ℕ →₀ (Fin n → ℕ) with t j i $=t_{ij}$; the user set $M$ is its support. Every user in $M$ therefore has a nonempty list, which is the paper's standing assumption $L^j\ne\emptyset$ (recalled on p. 19). Streams are natural numbers. The empty problem is allowed; there both sides of Theorem 2 are $\{0\}$.
• Inclusions. The paper's $\subset$ is read as $\subseteq$ throughout: $R=N$ is a coalition, and $S=\emptyset$ and $S=N$ are core constraints.
• Vectors. Payoff vectors are Fin n → ℝ. The core is the published Supermodularity.Cooperative.Core Finset.univ. Convexity is the published Supermodularity.Cooperative.IsConvexGame. The unanimity game is the published MonotonicSolutions.StrongMono.unanimity.
• Dividends. The paper defines the dividends implicitly, as the unique weights of the unanimity decomposition. The formalization uses the explicit formula $\Delta_v(R)=\sum_{S\subseteq R}(-1)^{|R|-|S|}v(S)$, and milestone 1 states that it gives those unique weights. A sharing system is a function on all coalitions whose value at $\emptyset$ is never read.
• No trivialization. The allocation set is the set of sums of user-indexed probability vectors supported on the users' lists. It is not the larger set "$x\ge 0$, $\sum_i x_i=m$", which would make Theorem 2 false. Theorem 2 is stated directly as a set equality between the core and the allocation set, not through the Harsanyi set. Vasil'ev's theorem is stated for every TU game with nonnegative dividends, as cited.
• Reusable parts. The Harsanyi dividend, sharing systems, the Harsanyi set, Harsanyi's uniqueness theorem and Vasil'ev's theorem apply to any finite TU game. Proofs of these, especially of Vasil'ev's inclusion $C\subseteq H$, are the most valuable contributions. The streaming steps (milestones 3 to 6) are welcome as independent footholds.
• The same streaming objects are restated in the sibling missions Revenue Sharing at Music Streaming Platforms I and III.

Selected references

• G. Bergantiños, J. D. Moreno-Ternero, Revenue sharing at music streaming platforms, Management Science, 2025; preprint arXiv:2310.11861v1, 2023. https://arxiv.org/abs/2310.11861
• J. C. Harsanyi, A bargaining model for the cooperative n-person game, in Contributions to the Theory of Games IV, Annals of Mathematics Studies 40, Princeton University Press, 1959.
• V. A. Vasil'ev, On a class of imputations in cooperative games, Soviet Mathematics Doklady 23 (1981), 53–57.
• R. van den Brink, G. van der Laan, V. Vasil'ev, Constrained core solutions for totally positive games with ordered players, International Journal of Game Theory, 2014 (the presentation of the Harsanyi set the paper follows, footnote 22).
• H. P. Young, Monotonic solutions of cooperative games, International Journal of Game Theory 14 (1985), 65–72. https://doi.org/10.1007/BF01769885

Motivation

Quadratically constrained quadratic programs (QCQPs) minimize a quadratic function subject to quadratic inequality and equality constraints. They model trust-region subproblems, robust least squares, max-cut and many problems in signal processing and control. They are NP-hard in general, so practice relies on convex relaxations, and the standard one is the Shor semidefinite (SDP) relaxation. The SDP relaxation lifts $N$ variables to an $(N+1)\times(N+1)$ positive semidefinite matrix, which is expensive for large $N$.

For an important subclass, the simultaneously diagonalizable QCQPs (SD-QCQPs), a much cheaper relaxation is available: after a change of variables all quadratic forms are diagonal, and the products $x_j^2$ can be relaxed by $N$ new variables $y_j \ge x_j^2$. This is a second-order cone (SOCP) relaxation, studied by Ben-Tal and den Hertog (2014) and Locatelli (2016) for the trust-region problem with additional constraints and related problems. Whether one may use the SOCP relaxation in place of the SDP relaxation without losing anything, for the optimal value and for the convex-hull description, is the question settled here.

This mission formalizes Proposition 1 of A. L. Wang and F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs (Math. Program., 2021; arXiv:1911.09195v3), §4.2.1 and App. A, together with Lemma 9 of §4.2.

Setting

A QCQP (1) in $N$ variables has data $A_i \in \mathbb{S}^N$, $b_i \in \mathbb{R}^N$, $c_i \in \mathbb{R}$ for $i \in [\![0,m]\!]$, with $m \ge 1$ constraints of which the first $m_I$ are inequalities. Writing $q_i(x) = x^\top A_i x + 2 b_i^\top x + c_i$,

$$\mathrm{Opt} = \inf_{x\in\mathbb{R}^N} \bigl\{ q_0(x) : q_i(x) \le 0,\ i \in [\![m_I]\!];\ q_i(x) = 0,\ i \in [\![m_I+1,m]\!] \bigr\}.$$

The SDP relaxation (3) uses $Q_i = \begin{pmatrix} c_i & b_i^\top \\ b_i & A_i\end{pmatrix}$ and the lifted variable $Y = \begin{pmatrix} 1 & x^\top \\ x & X\end{pmatrix}$ with $X \in \mathbb{S}^N$:

$$\mathrm{Opt}_{\mathrm{SDP}} = \inf_{x, X} \bigl\{ \langle Q_0, Y\rangle : \langle Q_i, Y\rangle \le 0,\ i \in [\![m_I]\!];\ \langle Q_i, Y\rangle = 0,\ i \in [\![m_I+1,m]\!];\ Y \succeq 0 \bigr\}.$$

Its projected epigraph $\mathcal{D}_{\mathrm{SDP}}$ (4) is the set of $(x,t) \in \mathbb{R}^{N+1}$ for which some $X$ satisfies these constraints together with $\langle Q_0, Y\rangle \le 2t$.

A family $\{A_i\}_{i\in[\![0,m]\!]}$ is simultaneously diagonalizable (SD) if there is an invertible $U$ with every $U^\top A_i U$ diagonal (Definition 4); an SD-QCQP is a QCQP whose matrices are SD (Definition 5). Changing variables by $U$ gives a diagonal QCQP (10): $A_i = \mathrm{Diag}(a_i)$ with $a_i \in \mathbb{R}^N$, so $q_i(x) = \langle a_i, x^2\rangle + 2\langle b_i, x\rangle + c_i$ with $(x^2)_j = x_j^2$. For it, the SOCP relaxation (11) is

$$\mathrm{Opt}_{\mathrm{SOCP}} = \inf_{x, y\in\mathbb{R}^N} \bigl\{ \langle a_0,y\rangle + 2\langle b_0,x\rangle + c_0 : \langle a_i,y\rangle + 2\langle b_i,x\rangle + c_i \le 0 \text{ or } = 0;\ y_j \ge x_j^2\ \forall j \bigr\},$$

and $\mathcal{D}_{\mathrm{SOCP}}$ (12) is the set of $(x,t)$ for which some $y$ satisfies these constraints and $\langle a_0,y\rangle + 2\langle b_0,x\rangle + c_0 \le 2t$.

The dual set is $\Gamma = \{\gamma \in \mathbb{R}^m : A_0 + \sum_i \gamma_i A_i \succeq 0,\ \gamma_i \ge 0\ \forall i \in [\![m_I]\!]\}$.

Formalization targets

Goal: Proposition 1 (p. 21)

For a diagonal QCQP (10),

$$\mathcal{D}_{\mathrm{SOCP}} = \mathcal{D}_{\mathrm{SDP}} \qquad\text{and}\qquad \mathrm{Opt}_{\mathrm{SOCP}} = \mathrm{Opt}_{\mathrm{SDP}}.$$

No regularity assumption is made; both values may be $+\infty$ or $-\infty$.

Milestones (App. A, pp. 34–35)

1. If $\begin{pmatrix} 1 & x^\top \\ x & X\end{pmatrix} \succeq 0$, then $X \succeq xx^\top$ and $X_{jj} \ge x_j^2$.
2. $\mathcal{D}_{\mathrm{SDP}} \subseteq \mathcal{D}_{\mathrm{SOCP}}$.
3. If $y_j \ge x_j^2$ for all $j$, the matrix $X$ with diagonal $y$ and off-diagonal entries $x_jx_k$ satisfies $\begin{pmatrix} 1 & x^\top \\ x & X\end{pmatrix} \succeq 0$.
4. $\mathcal{D}_{\mathrm{SOCP}} \subseteq \mathcal{D}_{\mathrm{SDP}}$.

Companion: Lemma 9 (p. 19)

For any SD-QCQP, $\Gamma$ is polyhedral.

Significance

The result. Proposition 1 transfers every SDP-tightness and convex-hull criterion to the SOCP relaxation of an SD-QCQP. The paper's main theorems give sufficient conditions for $\mathrm{conv}(\mathcal{D}) = \mathcal{D}_{\mathrm{SDP}}$ and for $\mathrm{Opt} = \mathrm{Opt}_{\mathrm{SDP}}$ under the assumption that $\Gamma$ is polyhedral; Lemma 9 shows this assumption holds for every SD-QCQP, and Proposition 1 then gives the same conclusions for an SOCP with only $N$ additional variables and $N$ convex quadratic constraints instead of an $(N+1)\times(N+1)$ semidefinite matrix (Remark 12). The value identity was first recorded by Locatelli (2016); the set identity is, according to the authors, new in the paper.

Formalizing it. The result is proved in the paper; no machine-checked version is known. The mission produces Lean definitions of the QCQP, its Shor relaxation, its projected epigraph and the lifted SOCP relaxation that are shared with the other missions of this series on the same paper, and a checked transfer from SDP to SOCP relaxations that downstream tightness results can use.

Difficulty

The argument is short on paper; the formal work is in the matrix bookkeeping. The inclusion $\mathcal{D}_{\mathrm{SDP}} \subseteq \mathcal{D}_{\mathrm{SOCP}}$ needs a Schur complement for a block matrix whose top-left block is the scalar $1$, in the block indexing $\mathrm{Fin}\,1 \oplus \mathrm{Fin}\,N$, and the identity $\langle \mathrm{Diag}(a), X\rangle = \langle a, \mathrm{diag}(X)\rangle$ inside a trace of block products. The reverse inclusion needs an explicit lifted matrix, and its positive semidefiniteness is a global property of an $(N+1)\times(N+1)$ matrix that the coordinatewise inequalities $y_j \ge x_j^2$ do not give entry by entry. The value identity is an identity of infima in the extended reals, where either side may be $\pm\infty$, so real arithmetic on the values is not available.

Formalization scope

• A QCQP is a structure QCQP N m with symmetric $A_0, A_i$, vectors $b_0, b_i$, scalars $c_0, c_i$ and $m_I \le m$. Constraint $i : \mathrm{Fin}\ m$ is the paper's constraint $i+1$, an inequality iff $i < m_I$.
• $\mathrm{Opt}_{\mathrm{SDP}}$ and $\mathrm{Opt}_{\mathrm{SOCP}}$ are infima in EReal, so infeasibility gives $+\infty$ and unboundedness $-\infty$. $\langle Q, Y\rangle$ is $\operatorname{tr}(QY)$, and $X$ in the SDP is symmetric.
• Diagonal, not SD. The paper states Proposition 1 "for any SD-QCQP", but $\mathcal{D}_{\mathrm{SOCP}}$ and $\mathrm{Opt}_{\mathrm{SOCP}}$ are defined only after the change of variables, which §4.2.1 assumes throughout. The goal and milestones 2 and 4 therefore take vectors $a_0, a_i$ and the hypothesis $A_0 = \mathrm{Diag}(a_0)$, $A_i = \mathrm{Diag}(a_i)$. Lemma 9 is stated for SD-QCQPs, with invertibility of $U$ as IsUnit U.
• The goal keeps the standing assumption $m \ge 1$ (p. 1); the milestones and Lemma 9 drop it, which makes them stronger. No Assumption 1 is made anywhere.
• No trivializing reading: $\mathcal{D}_{\mathrm{SOCP}}$ is defined directly from (12) with a vector $y$, not through matrices or through $\mathcal{D}_{\mathrm{SDP}}$, so the goal is a genuine comparison of two different feasible sets.
• Polyhedral means a finite intersection of closed halfspaces.
• Needed infrastructure: Schur complements of block matrices (Mathlib's Matrix.fromBlocks positive-semidefiniteness results), traces of block products, and EReal infima. A reusable lemma "$\begin{pmatrix} 1 & x^\top \\ x & X\end{pmatrix} \succeq 0 \iff X - xx^\top \succeq 0$" is welcome beyond this mission.

Selected references

• A. L. Wang, F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs, Mathematical Programming, 2021. arXiv:1911.09195v3, doi:10.1007/s10107-020-01589-9
• A. Ben-Tal, D. den Hertog, Hidden conic quadratic representation of some nonconvex quadratic optimization problems, Mathematical Programming 143:1–29, 2014 (reference [8] of the paper).
• M. Locatelli, Exactness conditions for an SDP relaxation of the extended trust region problem, Optimization Letters 10(6):1141–1151, 2016 (reference [37] of the paper).
• N. Z. Shor, Dual quadratic estimates in polynomial and boolean programming, Annals of Operations Research 25:163–168, 1990 (reference [47] of the paper).

Motivation

A chance constraint asks that a decision $x\in\mathbb R^n$ satisfy uncertain inequalities with high probability. In the setting of Zymler, Kuhn and Rustem (Math. Program. 137, 2013), $m$ affine inequalities $y_i^0(x)+y_i(x)^\top\tilde\xi\le0$, whose coefficients depend affinely on $x$, must hold jointly with probability at least $1-\epsilon$. Joint chance constraints appear wherever several safety conditions must hold at once: portfolio and network design, water reservoir operation, production planning under uncertain demand. They are hard for two reasons. Checking feasibility of a fixed $x$ requires a multi-dimensional integral, and the feasible set is typically nonconvex (Prékopa 1995). Moreover the distribution of $\tilde\xi$ is rarely known; often only its mean and covariance can be estimated.

The distributionally robust version requires the constraint for every distribution consistent with the known first and second moments. A standard tractable inner approximation replaces the probability by a worst-case Conditional Value-at-Risk (CVaR) of a single loss. For a joint constraint this needs the $m$ inequalities aggregated into one loss, and the choice of aggregation decides how much is lost.

Timeline. Charnes and Cooper (1959) and Miller and Wagner (1965) introduced chance constraints; Prékopa proved convexity of joint constraints with log-concave right-hand sides. Nemirovski and Shapiro (2006) studied convex (CVaR-type) approximations. El Ghaoui, Oks and Oustry (2003) and Calafiore and El Ghaoui (2006) gave exact SDP and SOCP reformulations of individual robust chance constraints under moment information. Chen, Sim, Sun and Teo (2010) introduced scaling parameters and an SOCP approximation of joint constraints. Zymler, Kuhn and Rustem (2013) showed that the worst-case CVaR of the scaled max-loss admits an exact LMI representation and that, with the scaling parameters free, it is essentially exact.

Setting

Let $\tilde\xi$ be a random vector in $\mathbb R^k$. Fix $\mu\in\mathbb R^k$ and a positive definite $\Sigma\in\mathbb S^k$, and let $\mathcal P$ be the set of all probability measures on $\mathbb R^k$ with finite second moments, mean $\mu$ and covariance $\Sigma$. The second-order moment matrix is

$$\Omega=\begin{bmatrix}\Sigma+\mu\mu^\top&\mu\\ \mu^\top&1\end{bmatrix}.$$

For a measurable loss $L$, a probability measure $\mathbb P$ and $\epsilon\in(0,1)$, the CVaR is

$$\mathbb P\text{-}\mathrm{CVaR}_\epsilon(L(\tilde\xi))=\inf_{\beta\in\mathbb R}\Big\{\beta+\tfrac1\epsilon\,\mathbb E_{\mathbb P}\big((L(\tilde\xi)-\beta)^+\big)\Big\},$$

and the worst-case CVaR is its supremum over $\mathbb P\in\mathcal P$.

The data are vectors $a_i^0,a_i^j\in\mathbb R^n$ and scalars $b_i^0,b_i^j$ for $i=1,\dots,m$, $j=1,\dots,k$, with $y_i^j(x)=(a_i^j)^\top x-b_i^j$ and $y_i(x)=[y_i^1(x),\dots,y_i^k(x)]^\top$. The sets of interest are:

• the robust joint chance constraint set $\mathcal X^{\mathrm{JCC}}=\{x:\inf_{\mathbb P\in\mathcal P}\mathbb P(y_i^0(x)+y_i(x)^\top\tilde\xi\le0\ \forall i)\ge1-\epsilon\}$;
• its strict version $\mathcal X^{\mathrm{JCC}}_\circ$, with every $\le0$ replaced by $<0$;
• for scaling parameters $\alpha\in\mathcal A=\{\alpha\in\mathbb R^m:\alpha_i>0\ \forall i\}$, the worst-case CVaR approximation $\mathcal Z^{\mathrm{JCC}}(\alpha)=\{x:\mathcal J(x,\alpha)\le0\}$ with

$$\mathcal J(x,\alpha)=\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-}\mathrm{CVaR}_\epsilon\Big(\max_{i=1,\dots,m}\alpha_i\big(y_i^0(x)+y_i(x)^\top\tilde\xi\big)\Big);$$

• the union $\mathcal Z^{\mathrm{JCC}}=\bigcup_{\alpha\in\mathcal A}\mathcal Z^{\mathrm{JCC}}(\alpha)$.

Formalization targets

Goal: Theorem 3.6 (p. 20)

$$\mathcal X^{\mathrm{JCC}}_\circ\subseteq\mathcal Z^{\mathrm{JCC}}\subseteq\mathcal X^{\mathrm{JCC}}.$$

The goal makes no regularity assumption on the constraint functions; it holds for all data, all $m\ge1$, all $\mu$, all $\Sigma\succ0$ and all $\epsilon\in(0,1)$.

Milestones

1. (7), p. 6: for every measurable loss $L$, $\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-}\mathrm{CVaR}_\epsilon(L)\le0$ implies $\inf_{\mathbb P\in\mathcal P}\mathbb P(L\le0)\ge1-\epsilon$.
2. p. 17: $\mathcal Z^{\mathrm{JCC}}(\alpha)\subseteq\mathcal X^{\mathrm{JCC}}$ for every $\alpha\in\mathcal A$.
3. Lemma A.1, p. 30: $\sup_{\mathbb P\in\mathcal P}\mathbb E_{\mathbb P}(f^+)=\inf\{\langle\Omega,M\rangle:M\succeq0,\ [\xi^\top\,1]M[\xi^\top\,1]^\top\ge f(\xi)\ \forall\xi\}$ for every measurable $f$.
4. (31), p. 16: $\mathcal J(x,\alpha)=\inf_\beta\{\beta+\frac1\epsilon\sup_{\mathbb P\in\mathcal P}\mathbb E_{\mathbb P}([\max_i\alpha_i(y_i^0(x)+y_i(x)^\top\tilde\xi)-\beta]^+)\}$.
5. Theorem 3.3, p. 16: $\mathcal Z^{\mathrm{JCC}}(\alpha)$ is the set of $x$ for which some $(\beta,M)$ satisfies $\beta+\frac1\epsilon\langle\Omega,M\rangle\le0$, $M\succeq0$ and the $m$ LMIs

$$M-\begin{bmatrix}0&\tfrac12\alpha_iy_i(x)\\ \tfrac12\alpha_iy_i(x)^\top&\alpha_iy_i^0(x)-\beta\end{bmatrix}\succeq0 .$$

6. Lemma A.2, p. 31: for every Borel $\mathcal S$, $\sup_{\mathbb P\in\mathcal P}\mathbb P(\tilde\xi\in\mathcal S)=\inf\{\langle\Omega,M\rangle:M\succeq0,\ [\xi^\top\,1]M[\xi^\top\,1]^\top\ge1\ \forall\xi\in\mathcal S\}$.
7. Lemma 2.2 (S-lemma), p. 8: the lossless S-procedure for one strictly feasible quadratic constraint, already proved on the platform.
8. (40), p. 21: $\mathcal X^{\mathrm{JCC}}_\circ$ is the set of $x$ for which some $M\succeq0$ and $\alpha>0$ satisfy $\langle\Omega,M\rangle\le\epsilon$ and the LMIs of Theorem 3.3 with $\beta=-1$.

Significance

The result. The worst-case CVaR approximation $\mathcal Z^{\mathrm{JCC}}(\alpha)$ is an LMI-representable inner approximation of the robust joint chance constraint for each fixed $\alpha$ (Theorem 3.3). Theorem 3.6 says that optimizing over $\alpha$ loses at most the boundary between the strict and the non-strict constraint: no tractable family based on the scaled max-loss can be uniformly better. Remark 3.2 of the paper observes that, for well-specified constraints, $\mathcal X^{\mathrm{JCC}}$ and $\mathcal X^{\mathrm{JCC}}_\circ$ differ by a Lebesgue-null set. Together with the inclusions of §3.3, it places the approximation at least as tight as the Bonferroni and Chen–Sim–Sun–Teo approximations and as close to $\mathcal X^{\mathrm{JCC}}$ as the strict constraint allows; it is the reason to treat $\alpha$ as a decision variable.

Formalizing it. The theorem is proved in the paper; nothing here is open mathematically. None of it is machine-checked. A formal proof requires moment-problem duality for the full moment set (Lemmas A.1 and A.2, which the paper sketches by citing Isii and Calafiore–El Ghaoui), a minimax interchange over a non-compact set of distributions, and the S-lemma, which is available on the platform. Each milestone is reusable: Lemmas A.1 and A.2 are the generalized Chebyshev bounds behind most of moment-based distributionally robust optimization.

Difficulty

The second inclusion is the conservativeness of CVaR, a Markov-type argument. The first inclusion is where the content lies. It requires the worst-case probability of a union of half-spaces to be an attained semidefinite program value, and an S-lemma certificate for each row. The obvious proof applies the S-lemma to every row, but the S-lemma's converse needs a strictly feasible point, which a row with $y_i(x)=0$ lacks; such rows must be treated separately. Similarly, the SDP representations are stated as existence of a feasible point, so the infima must be shown to be attained. The interchange of the supremum over $\mathcal P$ and the infimum over $\beta$ in (31) cannot cite weak compactness: $\mathcal P$ is not weakly compact, since mass can escape to infinity while the second moments stay fixed.

Formalization scope

• $\mathbb R^k$ is Fin k → ℝ; matrices in $\mathbb S^{k+1}$ are indexed by Fin k ⊕ Unit with the extra coordinate last; $M\succeq0$ is Matrix.PosSemidef (which includes symmetry); $\langle X,Y\rangle=\operatorname{Tr}(XY)$.
• $\mathcal P$ consists of probability measures with every coordinate in $L^2$, mean $\mu$ and covariance $\Sigma$ (the published MomentDRO.Conf definitions), so moments are genuine integrals.
• CVaR, the worst-case CVaR, worst-case expectations and SDP values take values in the extended reals. The expectation of a positive part is a lower Lebesgue integral. A supremum over $\mathcal P$ or an infimum over an infeasible set may be infinite.
• Standing assumptions, carried by every theorem: $\Sigma\succ0$ and $\epsilon\in(0,1)$ (p. 5). The theorems about the max-loss also assume $m\ge1$, implicit in the maximum over $i=1,\dots,m$. Milestone (7) assumes the loss measurable, as on p. 5.
• $\alpha\in\mathcal A$ is componentwise strict positivity, $\alpha_i>0$ for all $i$, not the product-order $\alpha>0$.
• A real-valued supremum would be $0$ on an unbounded set and make "$\mathcal J(x,\alpha)\le0$" true by a junk value. The extended-real encoding rules this out, and the moment set is nonempty under $\Sigma\succ0$, so no statement holds vacuously.
• Printed slips: the lower-left block "$\tfrac12\alpha_iy_i^\top$" of (30) is read as $\tfrac12\alpha_iy_i(x)^\top$; "$\bigcup_{\alpha\in\mathcal S}$" on p. 20 is read as $\bigcup_{\alpha\in\mathcal A}$; the index range "$i=1,\dots,n$" on p. 2 is read as $i=1,\dots,m$. The printed homogeneous S-lemma is replaced by the inhomogeneous one the proofs use.
• Contributions welcome: the moment-duality lemmas, the minimax interchange (31), attainment of the SDP infima, and the degenerate-row case of (40).

Selected references

• S. Zymler, D. Kuhn, B. Rustem, Distributionally robust joint chance constraints with second-order moment information, Math. Program. 137 (2013) 167–198. https://doi.org/10.1007/s10107-011-0494-7
• W. Chen, M. Sim, J. Sun, C.-P. Teo, From CVaR to uncertainty set: implications in joint chance-constrained optimization, Oper. Res. 58 (2010) 470–485. https://doi.org/10.1287/opre.1090.0712
• G. Calafiore, L. El Ghaoui, On distributionally robust chance-constrained linear programs, J. Optim. Theory Appl. 130 (2006) 1–22. https://doi.org/10.1007/s10957-006-9084-x
• L. El Ghaoui, M. Oks, F. Oustry, Worst-case value-at-risk and robust portfolio optimization: a conic programming approach, Oper. Res. 51 (2003) 543–556. https://doi.org/10.1287/opre.51.4.543.16101
• A. Nemirovski, A. Shapiro, Convex approximations of chance constrained programs, SIAM J. Optim. 17 (2006) 969–996. https://doi.org/10.1137/050622328
• R. T. Rockafellar, S. Uryasev, Optimization of conditional value-at-risk, J. Risk 2 (2000) 21–41. https://doi.org/10.21314/JOR.2000.038
• A. Prékopa, Stochastic Programming, Kluwer, 1995. https://doi.org/10.1007/978-94-017-3087-7

Motivation

A chance constraint asks that an uncertain constraint hold with high probability: a decision is acceptable if the loss $L(\tilde\xi)$ it incurs is nonpositive with probability at least $1-\epsilon$. Chance constraints appear in portfolio selection, power-system dispatch, inventory control and engineering design, wherever an occasional violation is tolerable but a frequent one is not. Two obstacles stand in the way of using them. The distribution of $\tilde\xi$ is rarely known exactly, and even when it is, the feasible set of a chance constraint is in general nonconvex and hard to compute.

Distributionally robust chance constraints address the first obstacle by requiring the constraint to hold for every distribution consistent with the available information. Zymler, Kuhn and Rustem (Math. Program. 137, 2013) take that information to be the mean and the covariance of $\tilde\xi$. The standard way around the second obstacle is to replace the probability by the Conditional Value-at-Risk (CVaR) of Rockafellar and Uryasev (J. Risk 2, 2000): a nonpositive CVaR implies the chance constraint, and the worst-case CVaR over a moment set can be computed by semidefinite programming. The approximation is conservative, and the question this mission formalizes is when it loses nothing.

Timeline. Isii (Ann. Inst. Statist. Math. 12, 1960) established strong duality for moment problems, the basis of generalized Chebyshev bounds; Calafiore, Topcu and El Ghaoui (Systems & Control Letters 58, 2009) gave the semidefinite form of the worst-case probability of a set under mean and covariance information that the paper uses as Lemma A.2. El Ghaoui, Oks and Oustry (Oper. Res. 51, 2003) computed the worst-case Value-at-Risk of a portfolio under mean and covariance information. Calafiore and El Ghaoui (J. Optim. Theory Appl. 130, 2006) showed that a distributionally robust individual chance constraint with a loss affine in $\tilde\xi$ is a second-order cone constraint. Zymler, Kuhn and Rustem (2013) showed that the worst-case CVaR approximation is exact for every continuous loss that is concave or quadratic in $\tilde\xi$ (Theorem 2.2), which is the goal of this mission, and extended the approach to joint chance constraints (the companion mission II).

Setting

Let $\tilde\xi$ be a random vector in $\mathbb R^k$. Fix a mean vector $\mu\in\mathbb R^k$ and a covariance matrix $\Sigma\in\mathbb S^k$ with $\Sigma\succ0$ (positive definite). The moment set $\mathcal P$ is the set of all probability distributions $\mathbb P$ on $\mathbb R^k$ with finite second moments, $\mathbb E_{\mathbb P}[\tilde\xi]=\mu$ and $\mathbb E_{\mathbb P}[(\tilde\xi-\mu)(\tilde\xi-\mu)^\top]=\Sigma$. The second-order moment matrix is

$$\Omega=\begin{bmatrix}\Sigma+\mu\mu^\top & \mu\\ \mu^\top & 1\end{bmatrix},$$

and $\langle X,Y\rangle=\operatorname{Tr}(XY)$ is the trace scalar product.

Fix a tolerance $\epsilon\in(0,1)$ and a loss $L:\mathbb R^k\to\mathbb R$. Write $x^+=\max\{x,0\}$. The CVaR of $L(\tilde\xi)$ under $\mathbb P$ is

$$\mathbb P\text{-}\mathrm{CVaR}_\epsilon(L(\tilde\xi))=\inf_{\beta\in\mathbb R}\Big\{\beta+\frac1\epsilon\,\mathbb E_{\mathbb P}\big((L(\tilde\xi)-\beta)^+\big)\Big\},$$

and the worst-case CVaR is its supremum over $\mathbb P\in\mathcal P$. The distributionally robust individual chance constraint is $\inf_{\mathbb P\in\mathcal P}\mathbb P(L(\tilde\xi)\le0)\ge1-\epsilon$. The worst-case Value-at-Risk is

$$\mathrm{WC\text{-}VaR}_\epsilon(L(\tilde\xi))=\inf\Big\{\gamma\in\mathbb R:\ \inf_{\mathbb P\in\mathcal P}\mathbb P\big(L(\tilde\xi)\le\gamma\big)\ge1-\epsilon\Big\}.$$

A loss is quadratic if $L(\xi)=\xi^\top Q\xi+q^\top\xi+q^0$, with no sign condition on $Q$.

Formalization targets

Goal: Theorem 2.2

For a continuous loss $L$ that is either concave or (possibly nonconcave) quadratic in $\xi$,

$$\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-}\mathrm{CVaR}_\epsilon\big(L(\tilde\xi)\big)\le0\iff\inf_{\mathbb P\in\mathcal P}\mathbb P\big(L(\tilde\xi)\le0\big)\ge1-\epsilon .$$

The implication from left to right holds for every loss; the content of the theorem is the converse.

Milestones

1. (15): for every measurable $L$, the chance constraint holds iff $\mathrm{WC\text{-}VaR}_\epsilon(L(\tilde\xi))\le0$.
2. Lemma A.2: for a Borel set $\mathcal S$, $\sup_{\mathbb P\in\mathcal P}\mathbb P(\tilde\xi\in\mathcal S)=\inf\{\langle\Omega,M\rangle: M\succeq0,\ [\xi^\top 1]M[\xi^\top 1]^\top\ge1\ \forall\xi\in\mathcal S\}$.
3. Lemma 2.1 (nonlinear Farkas lemma) for convex functions under a Slater point.
4. Lemma 2.2 (the $\mathcal S$-lemma), through the platform's proved lossless S-procedure.
5. (20): for the losses of Theorem 2.2,

$$\mathrm{WC\text{-}VaR}_\epsilon(L(\tilde\xi))=\inf\Big\{\beta+\tfrac1\epsilon\langle\Omega,M\rangle:\ M\succeq0,\ [\xi^\top\ 1]M[\xi^\top\ 1]^\top+\beta-L(\xi)\ge0\ \forall\xi\Big\}.$$

6. Lemma A.1: $\sup_{\mathbb P\in\mathcal P}\mathbb E_{\mathbb P}((f(\tilde\xi))^+)=\inf\{\langle\Omega,M\rangle: M\succeq0,\ [\xi^\top 1]M[\xi^\top 1]^\top\ge f(\xi)\ \forall\xi\}$ for measurable $f$.
7. The display after (20): for the losses of Theorem 2.2, the worst-case CVaR equals $\inf_\beta\{\beta+\frac1\epsilon\sup_{\mathbb P}\mathbb E_{\mathbb P}((L(\tilde\xi)-\beta)^+)\}$ and the value of the program in (20).
8. The identity of p. 9: for the losses of Theorem 2.2, the worst-case CVaR equals the worst-case VaR.

Significance

The theorem says that for concave and for quadratic losses the worst-case CVaR constraint, which is a linear matrix inequality in the decision through (20), describes exactly the feasible set of the distributionally robust chance constraint. Its affine special case (Corollary 2.1 of the paper) gives an exact semidefinite representation of robust individual chance constraints with affine dependence on the uncertainty, the case most used in robust portfolio and engineering models. The same equality between worst-case CVaR and worst-case VaR is the starting point of the paper's treatment of joint chance constraints, where an exact representation is obtained by optimizing over scaling parameters (mission II). The quadratic case covers losses such as portfolio variance terms or quadratic constraint functions, which are neither convex nor concave in general.

The results are proved in the paper, but parts of the argument are sketches. Lemmas A.1 and A.2 are strong duality theorems for moment problems that the paper cites from Isii and from Calafiore et al. rather than proves, and the interchange of supremum and infimum in the worst-case CVaR is justified by a citation to a stochastic saddle-point theorem. To our knowledge none of these results has a machine-checked proof. A formalization produces a checked moment-duality theorem with given mean and covariance, a nonlinear Farkas lemma, and a complete proof of the exactness theorem.

Difficulty

The direction from the worst-case CVaR constraint to the chance constraint is elementary. The converse cannot be obtained distribution by distribution: for a single distribution the CVaR is strictly larger than the VaR in general, and for a convex piecewise-linear loss the worst-case equivalence fails (Example 2.1 of the paper). The identity therefore depends on the specific moment set and the specific loss classes, and passes through two infinite-dimensional dualities. The moment set $\mathcal P$ is not compact in the weak topology, since mass can escape to infinity while the first two moments stay fixed, so the minimax interchange in the worst-case CVaR does not follow from a standard compact minimax theorem. Lemmas A.1 and A.2 are stated for an arbitrary measurable function and an arbitrary Borel set; their strong duality uses $\Sigma\succ0$ in an essential way. Finally, the semi-infinite constraint "for all $\xi$ with $L(\xi)>\gamma$" involves a strict inequality on a nonconvex set, and turning it into a matrix inequality is where concavity or quadraticity of $L$ enters.

Formalization scope

• $\mathbb R^k$ is Fin k → ℝ; matrices in $\mathbb S^{k+1}$ are indexed by Fin k ⊕ Unit with the extra coordinate last, so that $[\xi^\top 1]M[\xi^\top 1]^\top$ is liftQuad M ξ. $\Omega$ is built from the published ConvexOptimization.symQuadBlock.
• $\mathcal P$ is every probability measure with every coordinate in $L^2$, mean $\mu$ and covariance $\Sigma$ (the published MomentDRO.Conf.HasSecondMoments, meanVec, covMat). It is not restricted to discrete laws, densities or a support set.
• The standing assumptions $\Sigma\succ0$ and $\epsilon\in(0,1)$ are hypotheses of every theorem. Lemma 2.1 involves no distribution and does not carry them. Lemma A.1 needs measurability of $f$ and Lemma A.2 a Borel set, as printed; (15) is stated for every measurable loss.
• CVaR, the worst-case CVaR, the worst-case expectation, the worst-case VaR and the values of the semidefinite programs are extended reals. Expectations of positive parts are lower Lebesgue integrals and may be $+\infty$; an infimum over an empty feasible set is $+\infty$. A formalization with real-valued suprema would assign $0$ to an unbounded worst-case CVaR and make the constraint "worst-case CVaR $\le 0$" hold by a default value; this encoding rules that out.
• A quadratic loss is $\xi^\top Q\xi+q^\top\xi+q^0$ with $Q$ neither symmetric nor definite; concavity is on all of $\mathbb R^k$.
• The printed $\mathcal S$-lemma (homogeneous forms, general $p$) is replaced by the platform's proved lossless S-procedure for two inhomogeneous quadratics under a Slater point, which is the form the proof uses.

A complete development needs moment-problem duality on $\mathbb R^k$, a convex Farkas lemma, and the S-procedure (already proved on the platform). The first two are reusable beyond this mission, in particular by mission II, which uses Lemmas A.1 and A.2 verbatim. Proofs of any milestone are welcome independently.

Selected references

• S. Zymler, D. Kuhn, B. Rustem, Distributionally robust joint chance constraints with second-order moment information, Mathematical Programming 137 (2013) 167–198. https://doi.org/10.1007/s10107-011-0494-7
• R. T. Rockafellar, S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2 (2000) 21–41. https://doi.org/10.21314/JOR.2000.038
• K. Isii, The extrema of probability determined by generalized moments (I) bounded random variables, Annals of the Institute of Statistical Mathematics 12 (1960) 119–134 (reference [14] of the paper).
• G. Calafiore, U. Topcu, L. El Ghaoui, Parameter estimation with expected and residual-at-risk criteria, Systems & Control Letters 58 (2009) 39–46 (reference [7] of the paper).
• L. El Ghaoui, M. Oks, F. Oustry, Worst-case value-at-risk and robust portfolio optimization: a conic programming approach, Operations Research 51 (2003) 543–556. https://doi.org/10.1287/opre.51.4.543.16101
• G. C. Calafiore, L. El Ghaoui, On distributionally robust chance-constrained linear programs, Journal of Optimization Theory and Applications 130 (2006) 1–22. https://doi.org/10.1007/s10957-006-9084-x
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007) 371–418. https://doi.org/10.1137/S003614450444614X

Motivation

When every participant in a repeated game runs a no-regret learning algorithm, the time-averaged play converges to a coarse correlated equilibrium, and in smooth games the average welfare approaches the price-of-anarchy guarantee. These facts are a standard justification for equilibrium predictions in auctions, routing and markets, where agents learn rather than solve for equilibria. Against an adversary, the regret of any learning algorithm can grow like $\sqrt T$, which gives average regret of order $T^{-1/2}$. Syrgkanis, Agarwal, Luo and Schapire (arXiv:1507.00407, NIPS 2015) asked whether learning is faster when the opponents are themselves learning, and so their play changes slowly.

Timeline. Daskalakis, Deckelbaum and Kim (2011) gave a decentralized algorithm with $O(\log T)$ regret in two-player zero-sum games. Rakhlin and Sridharan (2013) obtained the same rate in zero-sum games with optimistic mirror descent, which uses the last observed utility as a prediction of the next one. Syrgkanis et al. (2015) extended recency-biased learning to general multi-player normal-form games. They isolated the RVU property, proved that it gives constant total regret (Theorem 4, Corollary 8), and proved that each individual player's regret is $O(T^{1/4})$ (Theorem 11, Corollary 12). This mission formalizes the second result. Later work by Chen and Peng (2020) and by Daskalakis, Fishelson and Golowich (2021) improved the individual rate to polylogarithmic in $T$.

Setting

A static game has $n$ players. Each player $i$ has a finite strategy set $S_i$ with $|S_i|=d$, and a utility function $u_i:S_1\times\cdots\times S_n\to[0,1]$. A mixed strategy is a point $w_i$ of the probability simplex $\Delta(S_i)\subset\mathbb R^d$, and the players randomize independently. The game is played at times $t=1,\dots,T$. At time $t$ each player picks $w_i^t\in\Delta(S_i)$ and then observes its utility vector

$$u_i^t=\big(\mathbb E_{s_{-i}\sim w_{-i}^t}[u_i(x,s_{-i})]\big)_{x\in S_i},$$

so its expected utility is $\langle w_i^t,u_i^t\rangle$. The regret of player $i$ after $T$ steps is

$$r_i(T)=\sup_{w_i^*\in\Delta(S_i)}\sum_{t=1}^T\langle w_i^*-w_i^t,u_i^t\rangle .$$

Strategies are measured in the norm $\|\cdot\|=\|\cdot\|_1$. Utilities are measured in its dual, $\|v\|_*=\|v\|_\infty$. A regularizer $\mathcal R$ is 1-strongly convex if $\mathcal R(\frac{a+b}2)\le\frac{\mathcal R(a)+\mathcal R(b)}2-\frac{\|a-b\|_1^2}8$. The range $R$ is $\max_i(\sup_{\Delta}\mathcal R_i-\inf_\Delta\mathcal R_i)$.

Optimistic follow the regularized leader (OFTRL) with step size $\eta>0$ and predictor sequence $M_i^t$ plays $w_i^0=\operatorname{argmin}_\Delta\mathcal R$ and

$$w_i^T=\operatorname*{argmax}_{w\in\Delta(S_i)}\Big\langle w,\ \sum_{t=1}^{T-1}u_i^t+M_i^T\Big\rangle-\frac{\mathcal R(w)}{\eta}.$$

With one-step recency bias, $M_i^T=u_i^{T-1}$. An algorithm has the RVU property (Regret bounded by Variation in Utilities) with parameters $\alpha,\beta,\gamma$ if its regret against every $w^*$ is at most $\alpha+\beta\sum_t\|u^t-u^{t-1}\|_*^2-\gamma\sum_t\|w^t-w^{t-1}\|^2$. It has the stability property with constant $\kappa$ if $\|w_i^t-w_i^{t+1}\|\le\kappa$.

Formalization targets

Goal: Corollary 12 (p. 5)

If $n\ge2$, every player runs OFTRL with $M_i^t=u_i^{t-1}$ and $\eta=(n-1)^{-1/2}T^{-1/4}$, then for every player $i$ and every $w_i^*\in\Delta(S_i)$,

$$\sum_{t=1}^T\langle w_i^*-w_i^t,u_i^t\rangle\le(R+4)\sqrt{n-1}\cdot T^{1/4}.$$

Milestones

1. Lemma 20 (supp. p. 4): $\|w^t-g^t\|\le\eta\|M^t-u^t\|_*$ and $\|g^t-w^{t+1}\|\le\eta\|M^{t+1}\|_*$, where $g^T=\operatorname{argmax}_\Delta\langle g,\sum_{t\le T}u^t\rangle-\mathcal R(g)/\eta$ is the leader sequence.
2. Stability with $\kappa=2\eta$ (p. 5, before Corollary 12): OFTRL with $M^t=u^{t-1}$ and utilities in $[0,1]$ moves by at most $2\eta$ per step.
3. Proposition 7 (p. 5): OFTRL with $M^t=u^{t-1}$ has the RVU property with $\alpha=R/\eta$, $\beta=\eta$, $\gamma=1/(4\eta)$.
4. The display in the proof of Theorem 11 (p. 5): $\|u_i^t-u_i^{t-1}\|_*^2\le(n-1)\sum_{j\ne i}\|w_j^t-w_j^{t-1}\|^2\le(n-1)^2\kappa^2$.
5. Theorem 11 (p. 5): RVU with $\alpha>0,\beta>0,\gamma\ge0$ plus stability $\kappa$ give each player regret at most $\alpha+\beta\kappa^2(n-1)^2T$.

Significance

The result. Corollary 12 shows that recency-biased regularized learning in a game guarantees each player average regret $O(T^{-3/4})$. The adversarial optimum is $O(T^{-1/2})$. The bound covers every player separately and needs no coordination beyond a common step size. Corollary 8, by contrast, bounds only the sum of the regrets. Theorem 11 isolates the two algorithmic properties responsible, RVU and stability. Any algorithm with both, including optimistic mirror descent and the other recency biases of the paper, inherits the bound.

Formalizing it. The result is proved in the paper, with the proofs of Proposition 7 and Lemma 20 in its supplementary material. No machine-checked version of optimistic FTRL, of the RVU property or of fast rates in games appears to exist. A formalization makes the following explicit: the strong-convexity form the proofs actually use, the convention for the first utility vector $u^0$, and the exact range of times on which stability is needed. A later mission of this series formalizes the companion bound on total regret (Corollary 8) on the same objects.

Difficulty

The game-theoretic part is short. Once Proposition 7 and the stability bound are available, Theorem 11 is a summation and Corollary 12 is arithmetic with real powers. The weight lies in the single-player analysis of optimistic FTRL. The first idea, to compare consecutive argmax points through first-order optimality conditions, fails because the regularizer need not be differentiable and the maximizers can lie on the boundary of the simplex. The arguments must work with the optimality of argmax points over $\Delta$ and with a quadratic-growth consequence of strong convexity. That consequence is not immediate from the midpoint condition in footnote 3. It needs continuity of the regularizer to pass from midpoints to the whole segment. Bounding the variation of utility vectors by the movement of the other players needs a total-variation estimate for product distributions.

Formalization scope

Players are Fin n and strategies Fin d, both indexed from $0$. Time keeps the paper's indices: $w^0$ is the initial play and sums run over $t\in\{1,\dots,T\}$. The vector $u_i^0$ is the utility vector against $w^0$; the paper never defines it. Mixed profiles and expectations use the published agt_games definitions. $\|\cdot\|$ is $\ell_1$ and $\|\cdot\|_*$ is Mathlib's sup norm. Optimistic FTRL and the leader sequence are predicates on trajectories, so every maximizer is a valid run. The goal quantifies over every run of the dynamics.

Standing assumptions and disclosed additions:

• utilities lie in $[0,1]$ (§2);
• each player may have its own regularizer (footnote 2);
• strong convexity is footnote 3's midpoint condition on $\Delta$ plus continuity on $\Delta$;
• $R$ is any common upper bound on the ranges, which includes the exact range;
• $n\ge2$ and $T\ge1$, since otherwise the step size is undefined;
• the regret's supremum is expressed as a bound for every comparator $w^*\in\Delta$;
• Theorem 11 assumes RVU only on the realized play, which strengthens the theorem, and stability only for the steps $t=0,\dots,T-1$.

Trivializations are ruled out. The regularizer class is nonempty: $(d/2)\sum_x w_x^2$ satisfies it. Removing the $[0,1]$ bound on utilities would make the stability claim false. The goal fixes the paper's step size and constant, so it is not a statement about a chosen run, an unbounded supremum or a vacuous parameter range.

A complete development needs the following:

• quadratic growth of strongly convex functions at constrained maximizers, for $\ell_1$ on the simplex;
• the be-the-leader induction of Theorem 19;
• a total-variation bound for product measures on finite sets.

These are reusable well beyond this mission, for online learning and for learning in games, and contributions of each are welcome.

Selected references

• V. Syrgkanis, A. Agarwal, H. Luo, R. E. Schapire, Fast Convergence of Regularized Learning in Games, NIPS 2015; arXiv:1507.00407v5. https://arxiv.org/abs/1507.00407
• A. Rakhlin, K. Sridharan, Optimization, Learning, and Games with Predictable Sequences, NIPS 2013. https://arxiv.org/abs/1311.1869
• C. Daskalakis, A. Deckelbaum, A. Kim, Near-Optimal No-Regret Algorithms for Zero-Sum Games, SODA 2011. https://arxiv.org/abs/1011.1489
• X. Chen, B. Peng, Hedging in Games: Faster Convergence of External and Swap Regrets, NeurIPS 2020. https://arxiv.org/abs/2006.04953
• C. Daskalakis, M. Fishelson, N. Golowich, Near-Optimal No-Regret Learning in General Games, NeurIPS 2021. https://arxiv.org/abs/2108.06924
• T. Roughgarden, Intrinsic Robustness of the Price of Anarchy, J. ACM 62(5), 2015. https://doi.org/10.1145/2806883

Why evaluate a policy against an ambiguous transition kernel

A Markov decision process (MDP) evaluates a policy by its expected discounted reward, which requires the transition probabilities. In practice these are estimated from data, and the optimal policy of the estimated model can perform badly under the true kernel. Robust MDPs replace the kernel by an ambiguity set of kernels and judge a policy by its worst-case expected reward over that set (Satia–Lave 1973; Nilim–El Ghaoui 2005; Iyengar 2005).

Robust evaluation is tractable when the ambiguity set is rectangular, meaning that the kernels of different states (or state–action pairs) can be chosen independently. Many natural ambiguity sets are not rectangular, for example confidence regions for jointly estimated parameters. Wiesemann, Kuhn and Rustem (Math. Oper. Res. 2013) show that for general sets robust policy evaluation is NP-hard even to approximate (their Theorem 2.6). They then give a lower bound computable by semidefinite programming, which is the subject of this mission.

Timeline:

• 1973: Satia and Lave pose MDPs with uncertain transition probabilities.
• 2005: Nilim–El Ghaoui and Iyengar solve robust dynamic programming over (s, a)-rectangular sets with deterministic policies.
• 2011: Kuhn, Wiesemann and Georghiou develop affine (linear) decision rules with S-lemma reformulations in stochastic and robust optimization.
• 2013: Wiesemann, Kuhn and Rustem treat s-rectangular and non-rectangular ambiguity sets with randomized policies. For the latter they give the affine approximation of their Theorem 3.8.

The robust MDP with an affinely parametrized ambiguity set

There are finitely many states $\mathcal S$ and actions $\mathcal A$. Choosing action $a$ in state $s$ and moving to $s'$ earns a reward $r(s,a,s')\ge 0$. Rewards are discounted by $\lambda\in(0,1)$, and the initial state has distribution $p_0$ in the probability simplex $\mathcal M(\mathcal S)$. An unknown parameter $\xi$ lies in

$$\Xi := \{\xi\in\mathbb R^q : \xi^\top O_l\,\xi + o_l^\top\xi + \omega_l\ge 0,\ l=1,\dots,L\},$$

where each $O_l$ is symmetric with $O_l\preceq 0$. The set $\Xi$ is bounded and has a Slater point $\bar\xi$, at which every constraint is strict. The transition probabilities depend affinely on $\xi$: $p^\xi(\cdot\mid s,a) = k_{sa}+K_{sa}\xi$, and this is a probability vector for every $\xi\in\Xi$.

A stationary randomized policy $\pi\in\Pi$ fixes a distribution $\pi(\cdot\mid s)$ over actions in each state. It induces the transition matrix $\widehat P_{ss'}(\xi)=\sum_a\pi(a\mid s)p^\xi(s'\mid s,a)$ and the expected rewards $\widehat r_s(\xi)=\sum_a\pi(a\mid s)\sum_{s'}p^\xi(s'\mid s,a)r(s,a,s')$. The reward to-go is $v(\xi)=\sum_{t\ge0}[\lambda\widehat P(\xi)]^t\widehat r(\xi)$. Robust policy evaluation asks for $\inf_{\xi\in\Xi}p_0^\top v(\xi)$.

Fix $\pi$. The affine approximate policy evaluation problem restricts reward to-go functions to affine maps $\vartheta(\xi)=w+W\xi$:

$$\sup_{w,W}\Big\{\inf_{\xi\in\Xi}p_0^\top(w+W\xi) : w+W\xi\le\widehat r(\xi)+\lambda\widehat P(\xi)(w+W\xi)\ \ \forall\xi\in\Xi\Big\}. \tag{19}$$

The semidefinite program (20) maximizes $\tau$ over $(\tau,w,W,\gamma,\Gamma)$ with $\gamma\ge0$ and $\Gamma\ge0$, subject to $(1+q)\times(1+q)$ linear matrix inequalities. Constraint (20b) involves $p_0^\top w-\tau$, $W^\top p_0$ and the matrices $Q_l=\big[\begin{smallmatrix}\omega_l & \frac12 o_l^\top\\ \frac12 o_l & O_l\end{smallmatrix}\big]$. Constraints (20c), one per state, involve $k_{sa}$, $K_{sa}$, $r_{sa}=(r(s,a,s'))_{s'}$, $w$, $W$ and $Q_l$.

Formalization targets

Goal: Theorem 3.8

Let $(\tau^*,w^*,W^*,\gamma^*,\Gamma^*)$ be an optimal solution of (20).

• If $L=1$, then $\tau^*$ equals the supremum of (19), and $\vartheta^*(\xi)=w^*+W^*\xi$ is feasible and optimal in (19).
• If $L>1$, then $\vartheta^*$ is feasible in (19), $\tau^*$ is a lower bound on the supremum of (19), and

$$\inf_{\xi\in\Xi}p_0^\top(w^*+W^*\xi)=\tau^*.$$

The theorem takes an optimal solution of (20) as given; it does not assert that (20) has one.

Milestones

1. Proposition 3.1 (c): every sub-solution $w\le\widehat r(\xi)+\lambda\widehat P(\xi)w$ lies below $v(\xi)$.
2. Every feasible $(w,W)$ of (19) satisfies $w+W\xi\le\bar r e/(1-\lambda)$ on $\Xi$, where $\bar r=\max r$.
3. Problem (19) is solvable.
4. Proposition 3.7 (17), the approximate S-lemma: if some $\gamma\ge 0$ makes $\big[\begin{smallmatrix}\sigma & \frac12 s^\top\\ \frac12 s & S\end{smallmatrix}\big]-\sum_l\gamma_lQ_l\succeq0$, then $\xi^\top S\xi+s^\top\xi+\sigma\ge0$ on $\Xi$.
5. The reverse implication of 4 when $S\succeq 0$.
6. The reverse implication of 4 when $L=1$: the published S-procedure, reused here.
7. The constraint $\tau\le p_0^\top(w+W\xi)$ on $\Xi$ is equivalent to (20b).
8. Constraint (20c) at $s$ implies the semi-infinite feasibility constraint of (19) at $s$, with equivalence when $L=1$.

Significance

When the ambiguity set is not rectangular, the robust value of a policy cannot be approximated efficiently in general. Theorem 3.8 gives a certified lower bound $\tau^*$ on it, computable by a semidefinite program of size polynomial in $|\mathcal S|$, $|\mathcal A|$, $q$ and $L$. Proposition 3.1 (c) makes (19) a restriction of the exact evaluation problem. For $L=1$, for example an ellipsoidal confidence region for $\xi$, the bound is the best affine one. The paper uses the theorem to compare policies under non-rectangular ambiguity, and in Proposition 3.10 to show that the bound is tight for s-rectangular sets.

On the formal side, the theorems are proved in the paper, and none of them, nor Proposition 3.7, has been formalized before. The platform has the exact S-procedure for one constraint, reused here, and other S-lemma variants in other settings. It has no approximate S-lemma for several concave quadratic constraints, no convex-Farkas argument for $S\succeq 0$, and no robust MDP with an affine parametrization. A completed mission would give a machine-checked SDP reformulation of a semi-infinite constraint in a dynamic programming setting.

Difficulty

Each direction rests on a different fact. The step from (20) to (19) is the elementary direction of the S-lemma, applied state by state and then combined with the objective's epigraph constraint. Showing that the bound is attained for $L=1$ needs four further facts:

• Problem (19) has an optimal solution. Its feasible region is unbounded (adding a constant $c\le0$ to $w$ preserves feasibility), so attainment needs the uniform bound of milestone 2 and a Slater ball inside $\Xi$.
• The objective's epigraph constraint $\tau\le p_0^\top(w+W\xi)$ on $\Xi$ and (20b) are exactly equivalent for every $L$, by convex Farkas (milestone 5).
• (20c) is exact for $L=1$, by the lossless S-procedure.
• The lower-right block $\lambda K_{sa}^\top W$ of (20c) is not symmetric.

A tempting shortcut is to treat (20c) as an ordinary positive semidefinite constraint on a symmetric matrix. That is wrong here: the matrix is not symmetric, and only its quadratic form carries meaning.

Formalization scope

Everything is finite-dimensional, and no measure theory is used.

• Types. States and actions are nonempty finite types. A policy is $\pi:\mathcal S\to\mathcal A\to\mathbb R$ with each $\pi(s)$ a probability vector (the published IsPolicy). $\widehat P$ and $\widehat r$ are built from the published InducedTransition and InducedReward.
• Reward to-go. $v$ is defined by the matrix-power series (8). The paper defines it as an expectation (5) and cites that (5) equals (8).
• The set $\Xi$. It is the set defined by the data $(O_l,o_l,\omega_l)$, with $\omega_l$ indexed by $l$; the page prints $\omega$ without the index in (3b). Boundedness, the Slater point and $O_l\preceq0$ (as PosSemidef of $-O_l$) are hypotheses.
• Problem (19). Affine $\vartheta$ is encoded as $(w,W)$, the paper's own (21). The objective is an infimum over the subtype $\Xi$, which is attained because $\Xi$ is nonempty and compact. "The supremum of (19)" is the greatest element, or every upper bound, of the set of feasible objective values.
• Block matrices. They have index type Unit ⊕ Fin q, with the scalar entry first. "$A\succeq0$" means $x^\top Ax\ge0$ for all $x$. This agrees with positive semidefiniteness on symmetric matrices and is the only faithful reading for (20c). Encoding (20c) with Mathlib's PosSemidef would make (20) infeasible and the goal vacuous, which is ruled out here. A verification instance with $|\mathcal S|=2$, $q=L=1$ shows that the standing hypotheses hold and that $(0,0,0,0,0)$ is feasible in (20).
• The S-procedure reference. It puts the scalar entry last and uses the opposite sign convention. Applying it to (17) for $L=1$ takes a permutation congruence and negation.

Welcome contributions include:

• the approximate S-lemma and the convex Farkas theorem of the alternative for several quadratic constraints, both reusable well beyond this mission;
• Proposition 3.1 (c) (the comparison principle for discounted Markov reward processes);
• compactness and attainment arguments for semi-infinite linear programs over $\Xi$.

Selected references

• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov Decision Processes, Mathematics of Operations Research 38(1), 2013; preprint Optimization Online 2610, revision of February 9, 2012. https://doi.org/10.1287/moor.1120.0566
• A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. https://doi.org/10.1287/opre.1050.0216
• G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. https://doi.org/10.1287/moor.1040.0129
• D. Kuhn, W. Wiesemann, A. Georghiou, Primal and dual linear decision rules in stochastic and robust optimization, Mathematical Programming 130(1), 2011. https://doi.org/10.1007/s10107-009-0331-4
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49(3), 2007. https://doi.org/10.1137/S003614450444614X
• L. Vandenberghe, S. Boyd, Semidefinite programming, SIAM Review 38(1), 1996. https://doi.org/10.1137/1038003
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887