All missions

Motivation

Phase recovery (also called phase retrieval) asks to reconstruct a complex signal from the magnitudes of linear measurements of it, the phases being lost. It arises wherever detectors record intensities only: X-ray crystallography, diffraction imaging, astronomy and optics, where a sensor measures $|\langle a_i, x\rangle|^2$ and not $\langle a_i, x\rangle$. The classical algorithms are alternating projections of Gerchberg–Saxton type (Gerchberg and Saxton, 1972; Fienup, 1982), which are fast but non-convex and can stall at stationary points that are not solutions.

Two convex relaxations change this picture. PhaseLift (Chai, Moscoso and Papanicolaou, 2011; Candès, Strohmer and Voroninski, 2013) lifts the signal $x$ to the rank-one matrix $xx^*$ and relaxes the rank constraint to a trace minimization; for random Gaussian measurements it provably recovers $x$ with high probability (Candès and Li, 2014). Waldspurger, d'Aspremont and Mallat (arXiv:1206.0102v3, Math. Programming 2015) instead separate amplitude and phase and obtain PhaseCut, a semidefinite program with the structure of the Goemans–Williamson MaxCut relaxation, for which MaxCut algorithms (block coordinate descent, rounding) apply. The question this mission formalizes is how the two relaxations compare in the noiseless case.

Timeline. An earlier version of the paper showed that PhaseLift tightness implies PhaseCut tightness; Voroninski (2012, working paper, cited in arXiv:1206.0102v3, §4.3) reversed the argument under additional assumptions. Version 3 of the paper (2013) introduces the refined program PhaseCutMod and proves that, for injective $A$, PhaseCutMod is tight whenever PhaseLift is (Corollary 4.3).

Setting

Fix a measurement matrix $A\in\mathbb C^{n\times p}$ with rows $a_1^*,\dots,a_n^*$, and a vector of amplitudes $b\in\mathbb R^n$. The phase recovery problem (1) is

$$\text{find } x\in\mathbb C^p \text{ such that } |Ax| = b,$$

i.e. $|a_i^*x| = b_i$ for every $i$. Write $\mathbf H_m$ for the $m\times m$ Hermitian matrices and $X\succeq 0$ for positive semidefiniteness. When $A$ is injective, $A^*A$ is invertible and the pseudoinverse is $A^\dagger = (A^*A)^{-1}A^*$; $AA^\dagger$ is the orthogonal projector onto the range of $A$. With $\operatorname{diag}(b)$ the diagonal matrix of the $b_i$, set

$$M = \operatorname{diag}(b)(\mathbf I - AA^\dagger)\operatorname{diag}(b),\qquad B = \operatorname{diag}(b)A^{\dagger *}A^\dagger\operatorname{diag}(b).$$

The three programs are

$$\text{(PhaseLift)}\quad \min_{X\in\mathbf H_p} \operatorname{Tr}(X)\ \ \text{s.t.}\ \operatorname{Tr}(a_ia_i^*X) = b_i^2,\ i=1,\dots,n,\ X\succeq 0;$$ $$\text{(PhaseCut)}\quad \min_{U\in\mathbf H_n} \operatorname{Tr}(UM)\ \ \text{s.t.}\ \operatorname{diag}(U) = 1,\ U\succeq 0;$$ $$\text{(PhaseCutMod)}\quad \min_{U\in\mathbf H_n} \operatorname{Tr}(BU)\ \ \text{s.t.}\ \operatorname{Tr}(MU) = 0,\ \operatorname{diag}(U) = 1,\ U\succeq 0.$$

PhaseCutMod selects, among the optimal points of PhaseCut (which in the noiseless case are exactly its points with $\operatorname{Tr}(MU)=0$), one of minimal $\operatorname{Tr}(BU)$. A relaxation is tight when it has a unique optimal solution and that solution has rank one. The two lifted programs are linked by the map

$$\Phi(X) = \operatorname{diag}(b)^{-1}AXA^*\operatorname{diag}(b)^{-1}.$$

In Lean these objects are PhaseCut.Tight.pinv, Mmat, Bmat, Phi, IsSolvable, phaseLiftFeasible/phaseLiftOptimal, phaseCutFeasible/phaseCutOptimal, phaseCutModFeasible/phaseCutModOptimal and IsTight.

Formalization targets

Goal: Corollary 4.3 (p. 13)

If $A$ is injective, $b_i\neq 0$ for all $i$, and (1) has an exact solution, then

$$\text{PhaseLift is tight}\ \Longrightarrow\ \text{PhaseCutMod is tight}.$$

The statement fixes no constants and no probabilistic model: it is a deterministic comparison of two programs, valid for every $A$ and $b$ meeting the three hypotheses.

Milestones

1. $M\succeq 0$ (§2.2, p. 4).
2. For $U, M\succeq 0$, $\operatorname{Tr}(UM)=0$ implies $UM=0$ (proof of Proposition 4.2, p. 12).
3. $\operatorname{Tr}(MU)=0,\ U\succeq 0$ (15) holds iff $U=\Phi(X)$ for some $X\succeq 0$ (16) (proof of Proposition 4.2, p. 12).
4. Proposition 4.2 (p. 12): $\Phi$ is a bijection from the feasible set of PhaseLift onto the feasible set of PhaseCutMod.
5. $\operatorname{Tr}(X) = \operatorname{Tr}(B\Phi(X))$ (proof of Corollary 4.3, p. 13).
6. $\operatorname{Rank}(X) = \operatorname{Rank}(\Phi(X))$ (proof of Corollary 4.3, p. 13).
7. Companion: when (1) is solvable, every optimal solution of PhaseCut is feasible for PhaseCutMod (§4.3, p. 12).

Significance

The result. Corollary 4.3 says that the MaxCut-type relaxation, once refined to PhaseCutMod, is never worse than PhaseLift at exact recovery: every recovery guarantee proved for PhaseLift (for instance the Gaussian-measurement results of Candès–Strohmer–Voroninski and Candès–Li) transfers to PhaseCutMod. Since PhaseCutMod can be approached by solving PhaseCut with $M$ replaced by $M+\gamma B$ for small $\gamma>0$, the algorithms designed for PhaseCut (greedy and block-coordinate SDP solvers) inherit those guarantees. The bijection of Proposition 4.2 also gives a precise dictionary between the lifted signal space $\mathbf H_p$ and the phase space $\mathbf H_n$.

Formalizing it. The result is proved in the paper; to the best of current knowledge none of it has a machine-checked proof. The mission produces a formal statement of the three programs over complex Hermitian matrices, of the pseudoinverse identities for injective matrices, and of the trace and rank transport under the congruence $\Phi$, which are reusable for other lifting arguments in phase retrieval and low-rank SDP.

Difficulty

The corollary itself is short once Proposition 4.2 and the two transport identities are available; the substance lies in Proposition 4.2. The natural first attempt is to check that $\Phi$ maps feasible points to feasible points, which is direct. Surjectivity is the step that requires an argument: a PhaseCutMod-feasible $U$ satisfies only the scalar constraint $\operatorname{Tr}(MU)=0$, and one must first upgrade it to the matrix equation $MU=0$ (using positive semidefiniteness of both factors) and then to a range condition on $\operatorname{diag}(b)U\operatorname{diag}(b)$ before a preimage can be written down. In Lean, an additional cost is the absence of a pseudoinverse and of trace-zero-product lemmas for complex Hermitian matrices in the form needed, and the bookkeeping between complex traces and real objectives.

Formalization scope

Matrices are Matrix (Fin n) (Fin p) ℂ and Matrix (Fin m) (Fin m) ℂ; $X\succeq 0$ is Mathlib's Matrix.PosSemidef (Hermitian included); rank is Matrix.rank. Conventions committed to:

• Injectivity is Function.Injective A.mulVec. $A^\dagger$ is encoded as (Aᴴ * A)⁻¹ * Aᴴ, Mathlib's inverse returning $0$ on singular matrices; it is the pseudoinverse only for injective $A$, so every statement mentioning $M$, $B$ or $\Phi$ assumes injectivity. This adds injectivity, not present on the page, to the claim $M\succeq 0$ (p. 4) and to the companion claim on p. 12.
• $\operatorname{diag}(b)^{-1}$ has entries $b_i^{-1}$ and is used only under $b_i\neq 0$.
• $\operatorname{Tr}(a_ia_i^*X) = a_i^*Xa_i$ is the diagonal entry $(AXA^*)_{ii}$.
• Objectives are real parts of complex traces (the traces are real on the feasible sets); the PhaseCutMod constraint $\operatorname{Tr}(MU)=0$ is an equation in $\mathbb C$.
• Optimal sets are sets of minimizers over the feasible set; tight means the optimal set equals $\{X\}$ for some $X$ of rank one. Weakening this to "some optimal solution has rank one" would be a different, weaker statement and is excluded, as is applying tightness to the feasible set instead of the optimal set.
• Proposition 4.2's "bijection" is Set.BijOn Φ (PhaseLift feasible) (PhaseCutMod feasible).
• The hypotheses of Proposition 4.2 and Corollary 4.3 are the page's, including the solvability of (1).

Infrastructure that a complete development needs, and that is reusable beyond this mission: the pseudoinverse identities $A^\dagger A = \mathbf I$ and $AA^\dagger A = A$ for injective complex $A$, the fact that $\mathbf I - AA^\dagger$ is a Hermitian idempotent, the lemma $\operatorname{Tr}(UM)=0\Rightarrow UM=0$ for complex positive semidefinite matrices, and rank invariance under congruence by injective matrices. Proofs of any milestone are welcome, as are general Mathlib-style lemmas on these points.

Selected references

• I. Waldspurger, A. d'Aspremont, S. Mallat, Phase recovery, MaxCut and complex semidefinite programming, Mathematical Programming 149 (2015); preprint arXiv:1206.0102v3 (2013). https://arxiv.org/abs/1206.0102
• E. J. Candès, T. Strohmer, V. Voroninski, PhaseLift: Exact and stable signal recovery from magnitude measurements via convex programming, Comm. Pure Appl. Math. 66 (2013). https://arxiv.org/abs/1109.4499
• E. J. Candès, X. Li, Solving quadratic equations via PhaseLift when there are about as many equations as unknowns, Found. Comput. Math. 14 (2014). https://arxiv.org/abs/1208.6247
• A. Chai, M. Moscoso, G. Papanicolaou, Array imaging using intensity-only measurements, Inverse Problems 27 (2011). https://doi.org/10.1088/0266-5611/27/1/015005
• V. Voroninski, A comparison between the PhaseLift and PhaseCut algorithms, working paper, 2012 (as cited in arXiv:1206.0102v3, p. 28). https://arxiv.org/abs/1206.0102
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995). https://doi.org/10.1145/227683.227684
• J. R. Fienup, Phase retrieval algorithms: a comparison, Applied Optics 21 (1982). https://doi.org/10.1364/AO.21.002758

Why D-optimal design needs a rate guarantee

In D-optimal design, a statistician chooses weights for a collection of candidate observations. The weights determine an information matrix, and maximizing its determinant favors a design that estimates several parameters jointly with a small confidence region. The same determinant objective appears in the minimum-volume enclosing ellipsoid problem. These links, and the earlier methods developed specifically for this objective, are described by Lu, Freund and Nesterov (2018), §2.2. A convergence theorem matters because a numerical design is useful only when its objective value can be related to the best possible value.

The paper applies a general relative smoothness framework to this problem. The usual first-order analysis asks for a uniform Lipschitz bound on the gradient of the objective. The logarithmic determinant has curvature that grows near singular information matrices, so a Euclidean smoothness constant on the whole design region is unsuitable. A logarithmic reference function gives a scale adapted to the coordinate boundary. The mission isolates the matrix result that provides this scale and the resulting explicit iteration bound for the primal gradient scheme. Both results are proved in the paper; their Lean statements are targets for formal proof.

Design weights, objective and algorithm

Fix an $m\times n$ real matrix $H$ with row rank $m$ and $n\ge m+1$. A design weight is a vector $x\in\mathbb R^n$ with nonnegative coordinates and $\sum_j x_j=1$. This set is the simplex $\Delta_n$. Write $X=\operatorname{Diag}(x)$ and $M(x)=HXH^\top$. On the points where $M(x)$ is positive definite, the optimization problem is

$$f^*=\min_{x\in\Delta_n} f(x), \qquad f(x)=-\log\det M(x).$$

The optimum may occur on the boundary of $\Delta_n$. At a singular point $f$ has no finite real value in the paper's model. Accordingly, the formal optimum is an attained point $x^*\in\Delta_n$ for which $M$x^*$\succ0$, minimal among all such points.

For the algorithm, the positive simplex is $\Delta_n^\circ=\{x\in\Delta_n:x_j>0\text{ for every }j\}$. The reference function and its Bregman distance are

h(x)=-\sum_{j=1}^n\log x_j, \qquad D_h(y,x)=h(y)-h(x)-\nabla h(x)\cdot$y-x$.

A primal gradient run starts at $x^0=e/n$. At each iteration $i\ge0$, it chooses $x^{i+1}\in\Delta_n^\circ$ to minimize

$$u\longmapsto f(x^i)+\nabla f(x^i)\cdot(u-x^i)+D_h(u,x^i) \quad\text{over }u\in\Delta_n^\circ.$$

The coefficient of $D_h$ is exactly one. Proposition 2.2 of Lu, Freund and Nesterov (2018) establishes this relative smoothness constant on the positive orthant. The displayed update represents the minimization condition; no tie-breaking rule is fixed.

Formalization targets

Relative smoothness of the determinant objective

For all positive vectors $x,y$, Proposition 2.2 asserts

f(y)\le f(x)+\nabla f(x)\cdot$y-x$+D_h(y,x).

Its source-stated matrix claims form the first part of the milestone list. If $C=H^\top(HXH^\top)^{-1}H$, the paper identifies $\nabla f(x)=\operatorname{diag}(-C)$, $\nabla^2 f(x)=C\circ C$, and $C\preceq X^{-1}$. Equation (17) then records the full comparison with $\nabla^2h(x)=X^{-2}$. Proposition 1.1 connects this Hessian comparison to relative smoothness. These statements fix the constant used by the algorithm.

Accuracy after a specified number of iterations

The mission goal is Theorem 4.1 of Lu, Freund and Nesterov (2018). For $0<\varepsilon\le f(x^0)-f^*$, it states

$$k\ge \frac{2n\log\!\bigl(2(f(x^0)-f^*)/\varepsilon\bigr)}{\varepsilon} \quad\Longrightarrow\quad f(x^k)-f^*\le\varepsilon.$$

The remaining milestones are the instance of the paper's primal gradient rate used here, the interior comparison point bound (40), and the logarithmic Bregman estimate (41)–(42). They follow the objects and constants named in the proof of Theorem 4.1.

What the result provides

The theorem gives a concrete stopping threshold expressed in the number of design weights, the requested objective gap, and the gap at the uniform start. It applies the same primal gradient method analyzed for general relatively smooth functions to a determinant objective whose gradient becomes steep near the boundary. The rate is an iteration count; it does not claim a superior arithmetic-operation count to specialized Frank–Wolfe methods. The paper compares those costs in its Table 1, noting that dense primal gradient iterations require a matrix inverse computation Lu, Freund and Nesterov (2018), §4.

A machine-checked development would connect finite-dimensional matrix inequalities, determinant derivatives, relative smoothness, and the algorithmic rate in one formal model. The matrix and logarithmic derivative results can be reused for other determinant objectives and barrier-based methods. The article proves Theorem 4.1; the mission asks solvers to formalize that known proof or another proof of the same precise statement. None of the draft theorem items is represented as already machine-checked.

Where the mathematical work lies

The determinant objective is well behaved on positive definite information matrices but is undefined at a singular design. A first attempt to apply a smoothness bound over the entire closed simplex encounters unbounded curvature near that boundary. A second issue is that an optimal design can have zero weights, while the logarithmic reference function and the algorithm use positive weights. The rate statement must therefore compare an interior run with an optimum that may lie on the boundary. The milestone list exposes the matrix curvature estimate and the boundary comparison as separate claims rather than hiding either in the goal's assumptions.

Formalization scope and conventions

Vectors are functions $\operatorname{Fin}(n)\to\mathbb R$, with explicit finite sums; matrices have the corresponding finite index types. The Bregman pairing $\nabla h(x)\cdot$y-x$$ is Lean's real Fréchet derivative applied to $y-x$. Iterates are zero-based. A Loewner inequality $A\preceq B$ means that $B-A$ is positive semidefinite. Rank $m$ and $n\ge m+1$ are the standing data of problem (16). The reference function is used on the positive orthant, and Algorithm 1 minimizes over $\Delta_n^\circ$, matching the positive subproblem minimizer described on p. 341.

The paper treats $f$ as infinite when the information matrix is singular and $h$ as infinite at a zero coordinate. Lean's real logarithm has a total value there, so every theorem restricts its meaningful objective evaluations to positive vectors or positive definite information matrices. The goal represents $f^*$ by an attained $x^*$ on that domain. It states $\varepsilon>0$ because the source's iteration formula divides by $\varepsilon$ and takes a logarithm of a ratio involving it. The interior point in (40) is constructed from $x^*,x^0,\varepsilon$; it is not an unconstrained input. These conditions rule out a vacuous interior, a junk logarithm, or division by zero as a formalization of the paper's conclusion.

The development needs matrix rank and positive definiteness, determinant and logarithm differentiation, positive semidefinite matrix order and the Schur product property, finite-sum calculus, and convex analysis of the positive simplex. The finite-dimensional matrix estimates and the relative smoothness criterion are natural reusable contributions. A proof may establish the listed milestones in another order, provided it keeps the same statements and constants.

Selected references

• H. Lu, R. M. Freund and Yu. Nesterov, Relatively smooth convex optimization by first-order methods, and applications, SIAM Journal on Optimization 28(1), 333–354 (2018). DOI: 10.1137/16M1099546.

Motivation

Online learning studies repeated decisions made before their losses are known. A learner chooses a point, observes a loss function, and then uses that observation to choose the next point. The natural performance measure is regret: the learner's cumulative loss minus the cumulative loss of one fixed competitor chosen after the sequence is known. A regret bound makes a claim for every loss sequence, including a sequence adapted to the learner's earlier decisions. Orabona's Chapter 6 develops online mirror descent as a way to obtain such bounds in geometries other than Euclidean distance Orabona, Chapter 6.

The geometry matters because the decision set and its loss gradients can have very different scales under different norms. On a simplex, for example, a Euclidean description treats coordinate changes differently from an entropy-based description. Theorem 6.11 expresses the guarantee in a primal norm chosen for the regularizer and the corresponding dual norm for the observed subgradients. It is the chapter's general regret statement for the basic mirror-descent algorithm Orabona, Theorem 6.11, p. 67.

Setting

Let $E$ be a finite-dimensional real normed space, representing the book's $\mathbb R^d$ with a chosen norm $\|\cdot\|$. The learner chooses from a nonempty closed convex set $V\subseteq E$. A regularizer $\psi$ has domain $X\supseteq V$; it is strictly convex on $X$ and differentiable on the interior of $X$. Its Bregman divergence is

$$B_\psi(y;x)=\psi(y)-\psi(x)-\langle\nabla\psi(x),y-x\rangle,$$

defined when $y\in X$ and $x\in\operatorname{int}X$. It need not be symmetric or satisfy the triangle inequality. The regularizer is $\lambda$-strongly convex on $V$ with respect to the chosen norm, where $\lambda>0$. The norm of a gradient $g$, written $\|g\|_*$, is the norm dual to $\|\cdot\|$. These are the conventions of Definition 6.4 and Lemma 6.10 Orabona, pp. 63–67.

At round $t$, beginning with $t=1$, the learner has $x_t\in V$, then observes a loss $\ell_t$ and a selected subgradient $g_t$ at $x_t$. With step size $\eta_t>0$, Algorithm 6.1 chooses any minimizer

$$x_{t+1}\in\arg\min_{y\in V}\left\{\langle g_t,y\rangle+\frac{1}{\eta_t}B_\psi(y;x_t)\right\}.$$

The book gives two ways to keep each update in the interior of $X$. The statements assume either of them, (6.5) or (6.6), $V\subseteq\operatorname{int}X$, so every iterate is a valid reference point for the next Bregman divergence Orabona, Algorithm 6.1 and (6.6), p. 65. Regret is measured against one fixed $u\in V$:

$$R_T(u)=\sum_{t=1}^{T}\bigl(\ell_t(x_t)-\ell_t(u)\bigr).$$

Formalization targets

For $T\ge1$ and nonincreasing positive step sizes, Theorem 6.11 gives the chapter's general bound

$$R_T(u)\le\frac{\max_{1\le t\le T}B_\psi(u;x_t)}{\eta_T} +\frac{1}{2\lambda}\sum_{t=1}^{T}\eta_t\|g_t\|_*^2\qquad(u\in V).$$

When every step equals the same $\eta>0$, it also gives the more specific bound

$$R_T(u)\le\frac{B_\psi(u;x_1)}{\eta} +\frac{\eta}{2\lambda}\sum_{t=1}^{T}\|g_t\|_*^2.$$

The decreasing-step bound is the goal; the constant-step conclusion is a companion theorem. The milestone list records the book's three-point identity (Lemma 6.7), the unique-minimizer theorem for a closed strongly convex function (Theorem 6.9), and the existence and full three-part inequality of the one-step mirror-descent lemma (Lemma 6.10). Theorem 6.11 follows these results in the source Orabona, pp. 64–67.

Significance

The first bound makes the cost of the update explicit: one term measures the divergence from the competitor to the iterates, and the other accumulates squared dual norms of the selected subgradients. The constant-step form depends only on the initial divergence, which can be substantially easier to estimate. These forms let a later analysis choose a regularizer and norm pair suited to its feasible set and gradients, as the chapter does in its subsequent examples Orabona, §§6.6–6.7.

The theorem and its proof are known mathematically from the textbook. The work here is to express the algorithm, its admissible oracle choices, and the exact bounds as Lean statements and then prove them. A formal proof of the one-step inequality would also be reusable for later dynamic-regret and optimistic mirror-descent results. The published Bregman-divergence definition is reused, but the statements in this mission remain proof targets; a related published three-point identity assumes continuous differentiability, stronger than the book's hypothesis.

Difficulty

The usual squared Euclidean distance has a symmetric algebraic expansion. Bregman divergence is asymmetric and its second argument must lie where the regularizer is differentiable. Thus a direct replacement of squared distance by $B_\psi$ does not by itself establish that every update is defined or that the terms in a regret sum have the right orientation. Theorem 6.11 also allows changing step sizes, so the divergence terms carry different denominators from one round to the next. The one-step lemma packages the exact inequality needed to make those issues precise Orabona, Lemma 6.10 and Theorem 6.11, p. 67.

Formalization scope

The Lean development uses an arbitrary finite-dimensional real normed space; continuous linear functionals represent subgradients, and their operator norm is $\|\cdot\|_*$. The regularizer is a total real-valued Lean function, but only its values on $X$ represent the book's function. Closedness is expressed by the closed epigraph of the extension equal to $+\infty$ outside $X$. Bregman divergence uses the published definition with the derivative at the second argument. The run predicate records the initial point, a selected subgradient, and a minimizer over $V$ on each round; it imposes no tie-breaking rule. The loss functions are real valued on $V$, and subgradient inequalities are stated relative to $V$, the only points compared in the regret result.

All sums use rounds $1,\ldots,T$; index zero carries no data. The maximum is a finite maximum with the explicit condition $T\ge1$. Positive $\eta_t$ and $\lambda$ protect every division in the displayed bounds. Every drafted statement assumes the book's "(6.5) or (6.6)", with (6.5) read as a one-sided limit $r\to0^+$. The update is required to minimize over $V$ itself, and $u$ ranges over $V$; allowing points outside that set would change the theorem. The minimizer result, the full one-step chain, and both regret bounds are welcome proof targets. The domain-restricted closed-function representation and the finite-round run predicate can be reused in related online convex optimization developments.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv preprint arXiv:1912.13213v10, 2026. arXiv

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

Motivation

A constraint $\mathbb E[v(x,\tilde z)] \le w$ on a decision $x$ needs the distribution of the random vector $\tilde z$, which in practice is known only through partial information: a support, some moments, the probability mass of a few regions. Distributionally robust optimization requires the constraint for every distribution consistent with that information. Wiesemann, Kuhn and Sim (Optimization Online 3757, 2013; Oper. Res. 62(6), 2014) introduced a standardized ambiguity set built from expectation conditions and probability bounds on confidence sets. Their Theorem 1 shows that the worst-case constraint over such a set is equivalent to a finite conic system, provided the confidence sets satisfy a nesting condition: any two are strictly nested or disjoint.

Many natural ambiguity sets violate nesting, for instance two overlapping confidence ellipsoids. For these the paper (§2.2) proposes two conservative approximations, the naïve approximation and the infimal convolution bound, and Theorem 3 orders them: the naïve approximation implies the infimal convolution bound, which implies the robust constraint. Infimal convolution bounds of this type had been used in classical and distributionally robust optimization before, e.g. in Goh and Sim (2010), Theorem 4. This mission formalizes Theorem 3, the steps of its proof, and Proposition 1, which compares partitions.

Setting

The random vector is $\tilde z \in \mathbb R^P$, with an auxiliary $\tilde u \in \mathbb R^Q$. A proper cone $\mathcal K$ is a closed convex cone with $\mathcal K\cap(-\mathcal K)=\{0\}$ and nonempty interior, and $x \preccurlyeq_{\mathcal K} y$ means $y - x\in\mathcal K$. For $i \in \mathcal I = \{1,\dots,I\}$ the confidence sets are $\mathcal C_i = \{(z,u) : C_iz + D_iu \preccurlyeq_{\mathcal K_i} c_i\}$, and the ambiguity set is

$$\mathcal P = \Big\{\mathbb P : \mathbb E_{\mathbb P}[A\tilde z + B\tilde u] = b,\ \ \mathbb P[(\tilde z,\tilde u)\in\mathcal C_i]\in[\underline p_i,\overline p_i]\ \ \forall i\in\mathcal I\Big\}.$$

The standing conditions are: (C1) $\mathcal C_I$ is bounded with $\underline p_I = \overline p_I = 1$ (it is the support); (C2) some $\mathbb P\in\mathcal P$ meets every non-degenerate probability bound strictly; (C3) $v(x,z) = \max_{l}\,[(S_lz+s_l)^\top x + \mathbf t_l^\top z + t_l]$, a maximum of finitely many bi-affine pieces, so $v$ is convex in $x$. The distributionally robust constraint (3) is $\mathbb E_{\mathbb P}[v(x,\tilde z)]\le w$ for all $\mathbb P\in\mathcal P$.

Write $A \Subset B$ when $A$ lies in the interior of $B$. A partition $\{\mathcal I_j\}_{j\in\mathcal J}$ of $\mathcal I$, with $J = |\mathcal J|$ blocks, satisfies the weak nesting condition (N′) if within each block any two distinct confidence sets are strictly nested or disjoint. The outer approximation $\mathcal P^j$ keeps the expectation condition and only the probability bounds of block $j$:

$$\mathcal P^j = \Big\{\mathbb P : \mathbb E_{\mathbb P}[A\tilde z + B\tilde u] = b,\ \ \mathbb P[(\tilde z,\tilde u)\in\mathcal C_i]\in[\underline p_i,\overline p_i]\ \ \forall i\in\mathcal I_j\Big\}.$$

With $\Gamma(x) = \{(y,\delta) : \sum_j y_j = x,\ \sum_j\delta_j = 1,\ \delta > 0\}$, the naïve approximation (6) and the infimal convolution bound (7) are

$$\min_{j\in\mathcal J}\sup_{\mathbb P\in\mathcal P^j}\mathbb E_{\mathbb P}[v(x,\tilde z)]\le w,\qquad \inf_{(y,\delta)\in\Gamma(x)}\sum_{j\in\mathcal J}\delta_j\sup_{\mathbb P\in\mathcal P^j}\mathbb E_{\mathbb P}[v(y_j/\delta_j,\tilde z)]\le w.$$

Formalization targets

Goal: Theorem 3 (p. 13)

$$\text{(6)}\ \Longrightarrow\ \text{(7)}\ \Longrightarrow\ \text{(3)},\qquad\text{and (3)} \Longrightarrow \text{(7)},\ \text{(3)}\Longrightarrow\text{(6)}\ \text{ if } J = 1,$$

under (C1)–(C3), (N′) and one disclosed added hypothesis, the uniform first-moment bound (see Formalization scope).

Milestones (proof of Theorem 3, p. 37; Proposition 1, p. 14)

1. $\mathcal P\subseteq\mathcal P^j$ for every $j$ (p. 12).
2. The chain: for $(y,\delta)\in\Gamma(x)$, $\sum_j\delta_j\sup_{\mathcal P^j}\mathbb E[v(y_j/\delta_j,\tilde z)] \ge \sum_j\delta_j\sup_{\mathcal P}\mathbb E[v(y_j/\delta_j,\tilde z)] \ge \sup_{\mathcal P}\mathbb E[v(x,\tilde z)]$.
3. (7) $\Rightarrow$ (3).
4. The limiting display: with $\delta_{j^\star}(k) = 1-1/k$, $y_{j^\star} = x$ and $\delta_j(k) = 1/(k(J-1))$, $y_j = 0$ otherwise,

$$\sum_j\delta_j(k)\sup_{\mathbb P\in\mathcal P^j}\mathbb E_{\mathbb P}[v(y_j/\delta_j(k),\tilde z)]\ \xrightarrow[k\to\infty]{}\ \sup_{\mathbb P\in\mathcal P^{j^\star}}\mathbb E_{\mathbb P}[v(x,\tilde z)].$$

5. (6) $\Rightarrow$ (7).
6. If $J = 1$ then $\mathcal P = \mathcal P^1$.
7. Proposition 1: if one partition refines another, both satisfying (N′), then (7) for the finer partition implies (7) for the coarser one.

Significance

The result. Theorem 1 of the paper needs nesting; Theorem 3 is what remains when nesting fails. It certifies that both surrogates are safe (a decision satisfying either satisfies the robust constraint) and that the infimal convolution bound is never looser than the naïve one. The paper also shows that (7), with $\Gamma(x)$ replaced by a closed approximation, has a conic reformulation (Observation 1), while optimizing over (6) with several constraints is strongly NP-hard (Theorem 4). Proposition 1 then says coarser partitions give tighter bounds, which guides the choice of partition.

Formalizing it. The result is proved in the paper; no machine-checked version is known. Formalizing it produces a reusable layer of extended-real worst-case expectations over sets of probability measures, with the infimal convolution and the perspective $\delta\,v(y/\delta,\cdot)$, and it corrects a gap in the printed proof of (6) $\Rightarrow$ (7) (see below).

Difficulty

The implications (7) $\Rightarrow$ (3) and Proposition 1 are short on paper; in Lean the work lies in extended-real arithmetic, where $-\infty+\infty=-\infty$, and in the integrability of $v(x,\tilde z)$. The step (6) $\Rightarrow$ (7) is the delicate one. The constraint $\delta>0$ forbids putting all weight on the minimizing block, so the bound is reached only in a limit, and the limit requires every block's worst-case expectation of $v(0,\tilde z)$, and of $\delta\,v(x/\delta,\tilde z)$ uniformly in $\delta$, to be controlled. The outer approximations drop the support condition (C1) for blocks that do not contain $I$, so these worst-case values can be $+\infty$, and the printed justification fails.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ; the outcome space is $(\texttt{Fin nP → ℝ})\times(\texttt{Fin nQ → ℝ})$ with its Borel σ-algebra. Indices are 0-based: $\mathcal I$ is Fin (nI + 1) (so $I\ge1$), $\mathcal C_I$ is index Fin.last nI, and $\mathcal J$ is Fin nJ. A partition is a surjective block map blk : Fin (nI + 1) → Fin nJ, so every block is nonempty; "$J=1$" is nJ = 1. Distributions in $\mathcal P$ and in every $\mathcal P^j$ are probability measures with a finite first moment, since a Lean integral of a non-integrable function is $0$. Worst-case expectations, (6) and (7) take values in EReal, with $\sup\emptyset=-\infty$; the minimum in (6) is a finite infimum, and $y_j/\delta_j$ is used only on $\Gamma(x)$, where $\delta>0$. Constraint (3) is in its $\forall$-form.

Added hypothesis. The goal, milestone 4 and milestone 5 assume a uniform first-moment bound: for every $j$, $\sup_{\mathbb P\in\mathcal P^j}\mathbb E_{\mathbb P}\|\tilde z\| < \infty$. Without it (6) $\Rightarrow$ (7) is false: with $P=1$, $\mathcal C_1=[0,\tfrac12]$ of probability at least $\tfrac12$, $\mathcal C_2=[0,1]$ of probability $1$, the singleton partition, $v(x,z)=z$ and $w=1$, (6) holds through $\mathcal P^2$, while $\mathcal P^1$ contains $\tfrac12\delta_0+\tfrac12\delta_M$ for every $M$, so (7) fails. The bound holds whenever every block contains a bounded confidence set with $\underline p_i=1$. No other hypothesis is added; (N′), (C1) and the cone conditions are kept as on the page although the proofs do not use them.

The definitions rule out the trivializing formalizations: no expectation is a junk integral, empty blocks are excluded by surjectivity, the ambiguity set is nonempty under (C2), and no real-valued supremum or division by a zero weight appears. Contributions welcome: proofs of the milestones, and reusable lemmas on EReal suprema of integrals and on perspectives of piecewise-affine functions.

Selected references

• W. Wiesemann, D. Kuhn, M. Sim, Distributionally Robust Convex Optimization, Optimization Online preprint 3757, version of September 22, 2013. https://optimization-online.org/wp-content/uploads/2013/02/3757.pdf
• W. Wiesemann, D. Kuhn, M. Sim, Distributionally Robust Convex Optimization, Operations Research 62(6):1358–1376, 2014. https://doi.org/10.1287/opre.2014.1314
• J. Goh, M. Sim, Distributionally Robust Optimization and Its Tractable Approximations, Operations Research 58(4):902–917, 2010. https://doi.org/10.1287/opre.1090.0712

Motivation

Classifiers trained to be robust against small, adversarially chosen input perturbations routinely lose standard accuracy. Adversarial training (Madry et al., 2018) improves worst-case accuracy under an $\ell_p$-bounded attack, but on MNIST, CIFAR-10 and ImageNet the resulting models are measurably less accurate on unperturbed inputs, and the loss grows with the attack radius. A natural reading is that this is an artefact of training procedures or of finite data.

Tsipras, Santurkar, Engstrom, Turner and Mądry (ICLR 2019) argue otherwise: they exhibit a simple distribution on which every classifier faces the trade-off, so that the tension is a property of the data distribution itself and survives infinite data, including for the Bayes-optimal classifier. The argument isolates a distinction that has since been influential: robust features, moderately correlated with the label and stable under small perturbations, versus non-robust features, individually weak but jointly highly predictive and easily flipped. This mission formalizes the paper's first theorem, Theorem 2.1, and its proof in Appendix C.

Setting

Fix $d \in \mathbb N$, a probability $p$ with $\tfrac12 \le p < 1$, and $\eta \ge 0$. The distribution $\mathcal D$ of an input-label pair $(x, y)$, $x = (x_1, x_2, \dots, x_{d+1}) \in \mathbb R^{d+1}$, is the data model (3):

$$y \sim \mathrm{Unif}\{-1,+1\}, \qquad x_1 = \begin{cases} +y & \text{w.p. } p\\ -y & \text{w.p. } 1-p\end{cases}, \qquad x_2, \dots, x_{d+1} \overset{\text{i.i.d.}}{\sim} \mathcal N(\eta y, 1),$$

with $x_1$ and $(x_2, \dots, x_{d+1})$ independent given $y$. Write $G_+$ and $G_-$ for the law $\mathcal N(\pm\eta, 1)^{\otimes d}$ of the weak features given $y = +1$ and $y = -1$.

A classifier is a measurable map $f : \mathbb R^{d+1} \to \{-1, +1\}$. Its standard accuracy is $\Pr_{(x,y)\sim\mathcal D}[f(x) = y]$, the objective (1) of the paper with the 0–1 loss. Its $\ell_\infty$ robust accuracy at radius $\varepsilon$ is

$$\mathrm{acc}_\varepsilon(f) = \Pr_{(x,y)\sim\mathcal D}\big[f(x + \delta) = y \text{ for every } \delta \in \mathbb R^{d+1} \text{ with } \|\delta\|_\infty \le \varepsilon\big],$$

the objective (2) with the 0–1 loss and perturbation set $\Delta = \{\|\delta\|_\infty \le \varepsilon\}$. In Lean these are stdAcc d p η f and robustAcc d p η f ε, each an average with weight $\tfrac12$ of the two class-conditional probabilities. The proof also uses $p_{ij}$, the probability that $f$ predicts $+1$ when $x_1 = i$ and the weak features follow $G_j$ (pij), and the shift adversary $x_i \mapsto x_i - 2\eta y$ for $i \ge 2$ (shiftAdv, accuracy shiftAcc).

Formalization targets

Goal: Theorem 2.1 (p. 5)

For every measurable classifier $f$ and every $\delta \in \mathbb R$,

$$\Pr[f(x) = y] \ge 1 - \delta \ \Longrightarrow\ \mathrm{acc}_\varepsilon(f) \le \frac{p}{1-p}\,\delta \qquad \text{for every } \varepsilon \ge 2\eta.$$

The statement quantifies over all classifiers, not a parametric family, and over every radius $\varepsilon \ge 2\eta$.

Milestones (App. C, pp. 14–16)

1. The shift $z_i \mapsto z_i - 2\eta y$ pushes $\mathcal N(\eta y, 1)^{\otimes d}$ forward to $\mathcal N(-\eta y, 1)^{\otimes d}$: it changes $G_+$ to $G_-$ and vice versa.
2. For $\varepsilon \ge 2\eta \ge 0$, robust accuracy is at most the accuracy against the shift adversary.
3. $\Pr[f(x) = y] = \tfrac12\big(p(1 + p_{++} - p_{--}) + (1-p)(1 + p_{-+} - p_{+-})\big)$.
4. $\Pr[f(x_{\mathrm{adv}}) = y] = \tfrac12\big(p(1 + p_{+-} - p_{-+}) + (1-p)(1 + p_{--} - p_{++})\big)$.
5. With $a = 1 - p_{++} + p_{--} \ge 0$ and $b = 1 - p_{-+} + p_{+-}$: $1 - \tfrac12(pa + (1-p)b) \ge 1 - \delta$ implies $\tfrac12((1-p)a + pb) \le \tfrac{p}{1-p}\delta$.

Companion statements (§2.1, pp. 4–5)

• Tightness. $\mathrm{sign}(x_1)$ has standard accuracy $p$ and robust accuracy $p$ for $0 \le \varepsilon < 1$; at $\delta = 1-p$ the bound of Theorem 2.1 is attained.
• Standard classification is easy. For $f_{\mathrm{avg}}(x) = \mathrm{sign}(\tfrac1d\sum_{i\ge2} x_i)$, $\Pr[f_{\mathrm{avg}}(x) = y] = \Pr[\mathcal N(\eta, 1/d) > 0]$, which exceeds $99\%$ when $\eta \ge 3/\sqrt d$.

Significance

Theorem 2.1 converts the empirical observation into a statement about a distribution: on $\mathcal D$, standard accuracy $1 - \delta$ caps robust accuracy at $\frac{p}{1-p}\delta$, so as $\delta \to 0$ robust accuracy falls to $0$, while the adversary's budget $\varepsilon = 2\eta = \Theta(1/\sqrt d)$ is small compared with the feature scale $\pm 1$. Together with the companion statements it shows that the model admits a classifier with accuracy above $99\%$ and a classifier with robust accuracy $p$, but no classifier with both. It underlies the paper's conclusion that robust training must give up non-robust features, and the later line of work on robust versus non-robust features.

The result is proved in the paper, with an elementary argument. As far as the platform record and a search of the literature show, it has not been machine-checked. The formalization adds an exact, convention-explicit version of the model and of robust accuracy (worst case over a closed $\ell_\infty$ ball, outer measure of a possibly non-measurable event), a Lean statement of the shift-invariance property of Gaussian products that the argument rests on, and a reusable template for 0–1-loss adversarial objectives that later missions on robustness in Gaussian models can follow.

Difficulty

The obvious attempt is to bound robust accuracy for a specific classifier, or for linear classifiers, where the adversary's best response is explicit. That does not reach the theorem: the claim is about every measurable $f$, for which no best response is computable and the robust event need not even be measurable. On the formal side, the statements involve the pushforward of a product of Gaussians under a coordinatewise shift, the decomposition of the class-conditional law into the two-point law of $x_1$ and the product $G_\pm$, and a measure applied to a possibly non-measurable robust event; none of these is available as a ready-made lemma for this model.

Formalization scope

Inputs live in Fin (d + 1) → ℝ; coordinate 0 is $x_1$ and coordinate i.succ is $x_{i+2}$. The Mathlib norm on this type is the sup norm, so ‖δ‖ ≤ ε is exactly the $\ell_\infty$ ball. Labels and predictions are the reals $\pm1$. The class-conditional law is ((x1Law p y).prod (weakLaw d η y)).map (Matrix.vecCons ·.1 ·.2) with weakLaw d η y = Measure.pi (fun _ => gaussianReal (y * η) 1). Accuracies are real numbers in $[0,1]$ computed with toReal. The robust event is measured by its outer measure, i.e. under the completion of $\mathcal D$; no measurability of that event is assumed.

The standing assumption $p \ge \tfrac12$ of model (3) is a hypothesis of every statement. Four hypotheses implicit on the page are explicit: $p < 1$ in the goal (the bound divides by $1-p$, and Lean's $p/0 = 0$ would make the statement false at $p = 1$); $\eta \ge 0$ (the page takes $\eta$ large, $\Theta(1/\sqrt d)$; with $\eta < 0$ the case $\varepsilon = 0$ has no adversary and the statement fails); measurability of $f$; and $f(x) \in \{\pm1\}$ for every $x$.

A trivializing formalization is ruled out: the goal is stated for every measurable $\{\pm1\}$-valued classifier and for the worst case over the full $\ell_\infty$ ball of every radius $\varepsilon \ge 2\eta$, not for linear classifiers, not for the fixed shift adversary, and not with the $p_{ij}$ among its hypotheses; those appear only in milestones.

The development needs Mathlib's gaussianReal, Measure.pi, product measures and pushforwards. Welcome contributions: the Gaussian shift identity (reusable for any Gaussian location model), the disintegration of condLaw along $x_1$, and the two accuracy formulas.

Selected references

• D. Tsipras, S. Santurkar, L. Engstrom, A. Turner, A. Mądry, Robustness May Be at Odds with Accuracy, ICLR 2019; arXiv:1805.12152v5 (2019). https://arxiv.org/abs/1805.12152
• A. Madry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
• L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, NeurIPS 2018. https://arxiv.org/abs/1804.11285

Motivation and context

Large matrices are often reduced by retaining only some rows or columns. The reduced matrix is cheaper to store and apply, but its spectral norm can be distorted by a single unusually large row, column, or entry. A useful estimate must show both the average effect of sampling and the cost of these local concentrations. In §5.2 of Tropp's monograph, matrix Chernoff inequalities give numerical estimates for independently sampled columns and for independently sampled rows and columns. The latter is the capstone of this mission.

The general matrix Chernoff inequality, Theorem 5.1.1, is already an Open goal in tc's Chapter 5 mission on Prove2Me. The intrinsic-dimension Chernoff inequality, Theorem 7.2.1, is likewise Open in tc's Chapter 7 mission. This mission concerns the application statements that those chapter missions have not posed: the numerical bound (5.2.2), its three displayed intermediate estimates, and companion consequences in §§5.1.1, 5.2.1 and 7.2.2. The motivation for choosing this target is that it connects a general concentration result to a concrete random matrix model; its terms can be read directly from a deterministic input matrix.

Setting

Fix a complex matrix $B\in\mathbb C^{d\times n}$ with $d,n\ge1$. For each row $j$, let $\delta_j$ equal one when that row is retained and zero otherwise. For each column $k$, let $\xi_k$ have the analogous meaning. The whole family is independent, with $\delta_j\sim\operatorname{Bernoulli}(p/d)$ and $\xi_k\sim\operatorname{Bernoulli}(r/n)$, where $0\le p\le d$ and $0\le r\le n$. Thus $p$ and $r$ are the expected numbers of retained rows and columns. Put

$$P=\operatorname{diag}(\delta_1,\ldots,\delta_d),\qquad R=\operatorname{diag}(\xi_1,\ldots,\xi_n),\qquad Z=PBR.$$

The zeros remain in the matrix: $Z$ has the same dimensions as $B$, but entries in discarded rows or columns vanish. Write $b_{j:}$ for row $j$, $b_{:k}$ for column $k$, and $b_{jk}$ for an entry. Their vector norms are Euclidean, while $\|B\|$ and $\|Z\|$ denote the spectral operator norm. The source uses $\mathbb E$ for expectation over the selections. Its maxima range over all rows, columns or entries of $B$, so a highly uneven matrix is distinguished from one whose mass is spread evenly.

The first milestone is the streamlined upper matrix Chernoff expectation bound. For a finite independent family of positive semidefinite Hermitian matrices $X_k$ with eigenvalues at most $L$, let $Y=\sum_kX_k$ and $\mu_{\max}=\lambda_{\max}(\mathbb EY)$. The bound uses the book's numerical constant $1.72$. The subsequent milestones specialize this setting to the row and column selectors above. A separate companion states the lower bound with $0.63$ and the two weakened tail inequalities of §5.1.1.

Formalization targets

The goal is the exact displayed estimate (5.2.2), with the book's rounded constants:

$$\begin{aligned} \mathbb E\|PBR\|^2\le{}&3\frac pd\frac rn\|B\|^2 +2\frac{p\log d}{d}\max_k\|b_{:k}\|^2\\ &+2\frac{r\log n}{n}\max_j\|b_{j:}\|^2 +(\log d)(\log n)\max_{j,k}|b_{jk}|^2. \end{aligned}$$

Its milestone chain is (5.1.8), followed by (5.2.3), (5.2.4), and (5.2.5). These are the claims the text places immediately before the final estimate. They bound, respectively, the first column-selection stage, the norm of the row-selected matrix, and the largest column norm after row selection. The companion (5.2.1) gives both the top and least squared singular-value bounds for column selection alone. The companion from §7.2.2 replaces $\log d$ by $\log(2\operatorname{srank}(B))$, where $\operatorname{srank}(B)=\|B\|_F^2/\|B\|^2$ is stable rank.

Significance

The goal separates four sources of size in a sampled matrix. The first term scales the squared spectral norm by the expected row and column retention fractions. The remaining terms record concentrations in a column, a row, and an individual entry. Consequently, the estimate can be evaluated from $B$ and the two sampling rates without specifying a distribution for $B$ itself. It is an expectation bound, not a claim that every realized submatrix is close to $B$.

The formal development would make the application layer of Tropp's Chapter 5 available alongside tc's general, currently Open matrix Chernoff theorem. A proof of that general theorem does not itself identify the random projectors, their joint independence, or the deterministic quantities on the right side of (5.2.2). The stable-rank companion also links the Chapter 7 notion of intrinsic dimension to a concrete rectangular matrix statistic. Both the chapter's general theorems and this mission's statements remain Open on the platform; none is being presented as already machine proved. Tropp, §§5.2 and 7.2.2 gives the mathematical results.

Difficulty

Sampling both rows and columns introduces two interacting random projectors. Merely applying a one-stage column estimate to $B$ leaves the row selection uncontrolled; merely applying a one-stage row estimate leaves the sampled column norms random. The two families must be independent of each other as well as independent internally. That distinction is substantial: separate independence claims for the row family and the column family do not imply independence between $P$ and $R$. The final estimate must also retain the book's exact $3$ and $2$ coefficients rather than replacing the right side by an unspecified constant times a simpler expression.

Formalization scope

Matrices are Matrix (Fin d) (Fin n) ℂ, matching the book's general complex-matrix convention. The spectral norm, extreme eigenvalues, Borel measurable matrix space, and intrinsic dimension come from tc's published definitions, which this mission references. Random selectors are measurable real-valued functions on a probability space; their Bernoulli law specifies almost-sure values zero or one and the probability of one. The row and column selectors form one jointly independent family. Products with diagonal selector matrices define $PB$, $BR$ and $PBR$; a deterministic diagonal or an unconstrained zero-one function would not be the sampled model.

Every sampling rate is within its Bernoulli domain. Nonzero dimensions keep the maxima over finite, inhabited sets and give the logarithms their intended arguments. Lean's Bochner integral otherwise returns zero on a nonintegrable function; each expectation inequality records integrability in its conclusion, which follows from measurable, bounded Bernoulli selectors and Tropp's standing regularity convention in §2.2.1. The maxima of column, row, and entry magnitudes are real finite suprema, equal to maxima for these finite nonempty index sets. The intrinsic-dimension identity assumes $p>0$ and $B\ne0$ for scale invariance; the final stable-rank bound itself includes zero sampling and the zero matrix.

The definitions of Bernoulli selection, random diagonal projections, sampled matrices, finite norm maxima and stable rank are reusable outside this mission. Contributions can address their structural identities, integrability, the four milestones, the goal, or the independent column-selection companions. The book's constants $1.72$ and $0.63$ are retained as decimals; $3$ and $2$ are the rounded coefficients printed in (5.2.2), as the text explains on p. 66.

Selected references

• Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, arXiv:1501.01571v1, §§2.1, 2.2, 5.1, 5.2, 7.2.
• Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, DOI:10.1561/2200000048. The formalization cites the pinned arXiv version above for page and equation indices.

Motivation

In a game, each participant chooses a strategy while the cost of that choice depends on what everyone else does. A network user may choose a route, for example, but its travel time depends on the routes chosen by other users. The price of anarchy compares the cost of self-interested outcomes with the best joint outcome. A guarantee restricted to a Nash equilibrium leaves open what happens when players repeatedly adapt their choices without settling on any equilibrium. Roughgarden's extension theorem addresses sequences produced by players whose accumulated costs are asymptotically competitive with fixed alternatives. Its bound depends on a property of the game, rather than on a particular learning algorithm or on convergence of play. Roughgarden, §§1 and 3.2.

Setting

There is a finite set of players $i$, and player $i$ has a strategy set $S_i$. These sets may be infinite. An outcome $s$ specifies one strategy $s_i\in S_i$ for every player. The real number $C_i(s)$ is player $i$'s cost, and the joint cost is $C(s)=\sum_i C_i(s)$. The paper treats this objective as nonnegative. If player $i$ alone changes to the strategy $s'_i$ of another outcome $s'$, its cost is written $C_i(s'_i,s_{-i})$; every other player's strategy stays as in $s$. Roughgarden, §2.1.

A game is $(\lambda,\mu)$-smooth if every pair $s,s'$ satisfies $\sum_i C_i(s'_i,s_{-i})\leq\lambda C(s')+\mu C(s)$. The robust price of anarchy $\rho(G)$ is the infimum of $\lambda/(1-\mu)$ over all such smoothness pairs with $\mu<1$. This number packages every bound obtainable from the same smoothness condition. It is taken in the extended reals, with value $+\infty$ when no pair exists; the mission assumes an admissible pair exists, so it is below $+\infty$. Roughgarden, Definitions 2.1–2.2.

For a played outcome $s^t$ at time $t$ and a comparison outcome $s'$, define the hypothetical improvement $\delta_i(s^t;s')=C_i(s^t)-C_i(s'_i,s^t_{-i})$. A player has vanishing average external regret when its average cost, up to an error tending to zero, is no greater than the average cost it would have paid by using any one fixed strategy throughout the first $T$ rounds. The comparison strategy is held fixed across time, while the other players' strategies may change on every round. Each player may have its own error function. Roughgarden, (22), (24).

Formalization targets

Additive bound

The paragraph following equation (25) asserts a bound with a vanishing additive error. For any comparison outcome $s'$ and every horizon $T\geq1$, there is a function $\eta(T)\to0$ with

$$\frac1T\sum_{t=1}^{T}C(s^t)\leq\rho(G)C(s')+\eta(T).$$

This target includes the case $C(s')=0$. The paper states the conclusion for an optimal outcome; the same displayed relations also apply to any comparison outcome. Relations (23) and (25) are separate milestones: the former bounds one outcome using the players' hypothetical improvements, and the latter averages that bound over time. Roughgarden, §3.2, pp. 13–14.

Multiplicative repeated-play bound

The mission goal is Theorem 3.3's multiplicative presentation. For a comparison outcome with $C(s')>0$, there is a function $\eta(T)\to0$ such that

$$\frac1T\sum_{t=1}^{T}C(s^t)\leq\bigl(\rho(G)+\eta(T)\bigr)C(s')\qquad(T\geq1).$$

The positive-cost condition is needed to make the printed statement true. Consider one player with strategies of costs $1$ and $0$, playing the costly strategy once and the zero-cost strategy thereafter. Its average regret tends to zero, but its average cost is $1/T>0$ at every finite horizon. Taking the zero-cost strategy as $s'$ makes the right-hand side of the printed multiplicative bound zero for any $\eta$. The additive milestone preserves the valid zero-cost case. Roughgarden, Theorem 3.3 and the paragraph preceding it.

Significance

The result transfers a bound defined by the game's smoothness condition to repeated play even when the sequence does not converge. It therefore gives a welfare guarantee for the behavior captured by vanishing external regret without identifying which learning rule generated the sequence. The additive statement also records exactly what remains true when an optimal outcome has zero cost. Roughgarden, §3.2.

Formalizing the result makes the quantifiers behind $o(1)$ explicit: for each fixed game, sequence, and comparison outcome, one error sequence works across all positive horizons and tends to zero. The development also distinguishes the paper's valid additive consequence from its multiplicative display at zero cost. The paper proves the result mathematically; the Lean files in this mission are theorem statements for solvers and do not yet contain machine-checked proofs.

Difficulty

For a fixed smoothness pair, a finite-time inequality controls average joint cost by the comparison cost and players' average hypothetical improvements. Regret controls those improvements asymptotically, but the robust price of anarchy takes an infimum over all admissible pairs. Passing from bounds for individual pairs to that infimum requires the sign and boundedness conditions on the joint cost to be tracked correctly. A direct replacement of the fixed pair's ratio by $\rho(G)$ does not itself justify the limit. The zero-cost example also shows why an additive error cannot simply be displayed as a multiplicative $o(1)$ term in every case. Roughgarden, (23)–(25) and Theorem 3.3.

Formalization scope

Lean uses a finite type of players, arbitrary strategy types, and real-valued player costs. It defines the joint objective by the finite sum $\sum_i C_i(s)$; it does not assume that each individual cost is nonnegative. The goal and additive milestone assume that the joint objective is nonnegative at every outcome, matching the paper's standing convention. They also assume at least one smoothness pair with $\mu<1$, the case in which $\rho(G)=+\infty$ and the page's bound is vacuous. $\rho(G)$ is an extended-real infimum and the inequalities are compared in the extended reals. For a nonnegative game with an admissible pair, $\rho(G)$ is a real number at least 1 when some outcome has positive cost; if all outcomes cost zero, the target cost bounds are zero. Roughgarden, §§1, 2.1, 3.2.

Time indices are $1,\ldots,T$, with $T\geq1$. The Lean sequence is infinite so that the asymptotic assertion concerns prefixes of one sequence; its value at index zero is unused. The regret definition quantifies over every fixed alternative strategy rather than assuming a minimum is attained when a strategy set is infinite. A separate vanishing error sequence may be chosen for each player. The conclusion chooses one vanishing error sequence after the game, play sequence, and comparison outcome, and uses it at every horizon. These choices make the $o(1)$ terms genuine limits, rather than unconstrained values chosen separately for each $T$. Roughgarden, (24), Theorem 3.3.

The game objective, smoothness predicate, robust price of anarchy, deviation improvement, and regret predicate are the reusable definitions. Solvers can contribute proofs of the one-step bound, its averaged form, the additive conclusion, and the main theorem. Mixed-outcome sequences from Remark 3.4 are outside this mission's core; their probability and integrability conventions would require another definition layer.

Selected references

• Tim Roughgarden, Intrinsic Robustness of the Price of Anarchy, Journal of the ACM 62(5), Article 32, 2015. DOI: 10.1145/2806883. Statements and page numbers follow the author's final version dated July 14, 2015.