Optimization

Motivation

Online convex optimization is the standard model for learning from a stream of data: in round $t$ a learner commits to a point $x_t$ in a convex set $\mathcal X\subseteq\mathbb R^d$, a convex loss $f_t$ is revealed, and the learner pays $f_t(x_t)+\varphi(x_t)$, where $\varphi$ is a fixed regularizer. Subgradient methods for this model use one fixed geometry (usually the Euclidean one) for every coordinate and every direction, regardless of the data. Duchi, Hazan and Singer (JMLR 12 (2011) 2121–2159) introduced ADAGRAD, which adapts the geometry to the observed subgradients. The diagonal version is one of the most widely used optimizers in machine learning and the ancestor of RMSProp and Adam. This mission formalizes the paper's full-matrix version: the proximal term is built from the matrix square root of the accumulated outer products of the subgradients, so the method adapts to correlated directions, not only to individual coordinates.

The analysis extends the regret bounds of primal-dual subgradient methods and regularized dual averaging (Nesterov 2009; Xiao 2010) and of composite mirror descent to proximal functions that change over time, and combines them with trace inequalities for the matrix square root. Concurrent work by McMahan and Streeter (COLT 2010) studied closely related adaptive proximal methods.

Setting

Vectors live in $\mathbb R^d$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|_2$. In round $t=1,2,\dots$ the learner plays $x_t\in\mathcal X$ and observes a subgradient $g_t\in\partial f_t(x_t)$, that is, $f_t(y)\ge f_t(x_t)+\langle g_t,y-x_t\rangle$ for all $y$. The regret against a comparator $x^*\in\mathcal X$ is

$$R_\phi(T)=\sum_{t=1}^T\big[f_t(x_t)+\varphi(x_t)-f_t(x^*)-\varphi(x^*)\big].$$

The outer product matrix is $G_t=\sum_{\tau=1}^t g_\tau g_\tau^\top$, a symmetric positive semidefinite $d\times d$ matrix, and $S_t=G_t^{1/2}$ is its positive semidefinite square root. With parameters $\eta>0$ and $\delta\ge0$, ADAGRAD with full matrices (Figure 2 of the paper) sets

$$H_t=\delta I+S_t,\qquad \psi_t(x)=\tfrac12\langle x,H_tx\rangle,\qquad B_{\psi_t}(x,y)=\tfrac12\langle x-y,H_t(x-y)\rangle,$$

starts at $x_1=0$, and computes $x_{t+1}$ by one of two updates:

• the primal-dual subgradient update (3): $x_{t+1}\in\operatorname{argmin}_{x\in\mathcal X}\{\eta\langle\tfrac1t\sum_{\tau\le t}g_\tau,x\rangle+\eta\varphi(x)+\tfrac1t\psi_t(x)\}$;
• the composite mirror descent update (4): $x_{t+1}\in\operatorname{argmin}_{x\in\mathcal X}\{\eta\langle g_t,x\rangle+\eta\varphi(x)+B_{\psi_t}(x,x_t)\}$.

The dual (semi)norm of $\psi_t$ is $\|v\|_{\psi_t^*}^2=\langle v,H_t^\dagger v\rangle$, where $A^\dagger$ is the pseudo-inverse.

Formalization targets

Goal: Theorem 7

Assume $\mathcal X$ closed and convex, $f_t$ and $\varphi$ convex, and $\varphi$ minimized over $\mathcal X$ at $x_1=0$. For the primal-dual update with $\delta\ge\max_{t\le T}\|g_t\|_2$, every $x^*\in\mathcal X$ satisfies

$$R_\phi(T)\le\frac\delta\eta\|x^*\|_2^2+\frac1\eta\|x^*\|_2^2\operatorname{tr}(G_T^{1/2})+\eta\operatorname{tr}(G_T^{1/2}),$$

and for the composite mirror descent update with any $\delta\ge0$,

$$R_\phi(T)\le\frac\delta\eta\|x^*\|_2^2+\frac1{2\eta}\max_{t\le T}\|x^*-x_t\|_2^2\operatorname{tr}(G_T^{1/2})+\eta\operatorname{tr}(G_T^{1/2}).$$

Milestones

In the order the proof uses them:

1. Lemma 16 and Propositions 3 and 2: regret bounds for mirror descent and dual averaging with time-varying quadratic proximal functions $\psi_t(x)=\tfrac12\langle x,H_tx\rangle$ ((11) and (10)).
2. Lemma 13: $A\succeq B\succeq0$ implies $A^{1/2}\succeq B^{1/2}$.
3. The first display of the proof of Theorem 7 and inequality (16): the growth of the Bregman terms is controlled by $\operatorname{tr}(G_t^{1/2})$.
4. Lemma 14 ($\nabla_X\operatorname{tr}(X^p)=pX^{p-1}$), Lemma 8 (a first-order concavity inequality for $\operatorname{tr}(B^{1/2})$ at singular $B$), Lemma 9, and Lemma 10, the doubling lemma

$$\sum_{t=1}^T\langle g_t,S_t^\dagger g_t\rangle\le2\sum_{t=1}^T\langle g_t,S_T^\dagger g_t\rangle=2\operatorname{tr}(G_T^{1/2}).$$

5. (17): the dual-norm sums of both updates are at most $2\operatorname{tr}(G_T^{1/2})$.

Significance

The quantity $\operatorname{tr}(G_T^{1/2})$ can be much smaller than the $\sqrt{T}\max_t\|g_t\|_2$ factor in the regret of non-adaptive online gradient descent with a tuned step size: it is small when the subgradients concentrate in a few directions, possibly not aligned with the coordinate axes. The paper's Corollary 11 rewrites it as $\sqrt d$ times the square root of $\inf\{\sum_t g_t^\top S^{-1}g_t: S\succeq0,\operatorname{tr}(S)\le d\}$, the gradient term of the best fixed full-matrix proximal function chosen in hindsight. The supporting results have their own uses. Propositions 2 and 3 are the generic regret bounds for adaptive proximal methods. Lemmas 8–10 are trace inequalities for the matrix square root that appear throughout the analysis of second-order online methods.

The results are proved in the paper. To our knowledge none of them has a machine-checked proof. Formalizing them requires the matrix functional calculus (square roots, pseudo-inverses, real powers) in a form usable for inequalities, which Mathlib has only partly: for instance, monotonicity of the square root is in Mathlib for C*-algebras, which covers complex but not real matrices. A complete development gives a verified regret bound for an adaptive full-matrix method together with these matrix inequalities.

Difficulty

The online-learning half (Lemma 16, Propositions 2 and 3) is a convex-analysis argument once the proximal functions are quadratic. The obstacle is the matrix half. The natural approach to Lemma 10 is induction with a scalar inequality $\sqrt{b-a}\le\sqrt b-a/(2\sqrt b)$ applied eigenvalue by eigenvalue. This fails because $G_{T-1}$ and $G_T$ do not commute, so their eigenvectors differ. One needs the concavity of $A\mapsto\operatorname{tr}(A^{1/2})$ on positive semidefinite matrices and its gradient, at points where $A$ may be singular. That is where Lemma 8 and the pseudo-inverse enter: the inverse root does not exist, and a limit $\delta\downarrow0$ is needed. The same issue arises in Lemma 9 and in the dual norm when $\delta=0$.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), so ‖·‖ is the Euclidean norm. Matrices are Matrix (Fin d) (Fin d) ℝ, acting on vectors through Matrix.toEuclideanLin. The square root is Mathlib's CFC.sqrt under the Loewner order (MatrixOrder). The pseudo-inverse is the functional calculus of $\lambda\mapsto\lambda^{-1}$ with $0^{-1}=0$, and $B^{-1/2}$ is written as $(B^\dagger)^{1/2}$. Mathlib's matrix inverse is used only where the matrix is invertible or the vector is zero. Rounds are 1-based and $G_0=0$. The losses and $\varphi$ are real-valued convex functions, and the constraint is carried by $\mathcal X$. Each update's argmin is a predicate (the next iterate lies in $\mathcal X$ and minimizes the objective there), which does not assert existence or uniqueness. A run consists of the $T$ rounds of Figure 2, with the subgradient relation imposed in every round. The subgradient relation is the platform's published ShorNonsmooth.AlmostDiff.IsSubgradient.

Restrictions and conventions, each stated in the item that needs it:

• $\varphi$ is minimized over $\mathcal X$ at $x_1=0$. This is the paper's $x_1=\arg\min_{\mathcal X}\varphi$. Without it both parts of Theorem 7 are false.
• Lemma 8 assumes $\nu\ge0$. The page says "for any $\nu$", but the inequality fails for $\nu<0$ (for $B=0$, $\nu=-1$ it reads $2\|g\|_2\le0$). The paper only applies the lemma with $\nu=1$.
• Lemma 16 and Propositions 2, 3 are specialised to quadratic proximal functions. In Lemma 16 and Proposition 3, $H_t$ is positive semidefinite and $g_t$ lies in its range, so the dual norm is finite. In Proposition 2, $H_t$ is positive definite, the $H_t$ increase, and $x_1=0$. Lemma 16 asks for $x^*\in\mathcal X$. Proposition 3 is stated for $T\ge1$ rounds.
• $H_0=\delta I$ in the dual norm $\|\cdot\|_{\psi_0^*}$ of (17) and Theorem 7. Figure 2's $H_0=0$ is never used by the updates.
• Lemma 14's gradient is stated as a directional derivative along every symmetric direction.

A formalization in which the next iterate need not lie in $\mathcal X$, the comparator ranges outside $\mathcal X$, $S_t$ is $G_t$ itself or its entrywise square root, or $S_t^\dagger$ is Mathlib's matrix inverse (which vanishes on singular matrices), states a different theorem and is excluded.

Proofs need the convex-analysis optimality conditions for the two updates, the Loewner-order calculus of CFC.sqrt on real matrices (Lemma 13), concavity and differentiability of $\operatorname{tr}(A^{1/2})$, and limits $\delta\downarrow0$ in the functional calculus. The matrix lemmas (13, 14, 8, 9, 10) are reusable outside this paper. Alternative proofs, for instance of Lemma 10 through operator concavity, are welcome.

Selected references

• J. Duchi, E. Hazan, Y. Singer, Adaptive Subgradient Methods for Online Learning and Stochastic Optimization, Journal of Machine Learning Research 12 (2011) 2121–2159. https://jmlr.org/papers/v12/duchi11a.html
• H. B. McMahan, M. Streeter, Adaptive Bound Optimization for Online Convex Optimization, COLT 2010. https://arxiv.org/abs/1002.4908
• L. Xiao, Dual Averaging Methods for Regularized Stochastic Learning and Online Optimization, Journal of Machine Learning Research 11 (2010) 2543–2596. https://jmlr.org/papers/v11/xiao10a.html
• Y. Nesterov, Primal-dual subgradient methods for convex problems, Mathematical Programming 120 (2009) 221–259. https://doi.org/10.1007/s10107-007-0149-x
• T. Ando, Concavity of certain maps on positive definite matrices and applications to Hadamard products, Linear Algebra and its Applications 26 (1979) 203–241. https://doi.org/10.1016/0024-3795(79)90179-4

Motivation

Policy gradient methods optimize a decision rule by changing the parameters that determine its action probabilities. In reinforcement learning, the objective is the expected total reward collected over time. Once a policy is restricted to a feature-based class, the best policy may be less effective than the unrestricted optimum. A useful guarantee must therefore compare the computed policy with a chosen comparator and account for both the limits of the features and the error in estimating an update direction. Agarwal, Kakade, Lee and Mahajan give such a guarantee for a version of the natural policy gradient method that fits action values with linear features, called Q-NPG (Agarwal et al., §6.2).

The result matters when a policy has far fewer parameters than there are state-action pairs. A bound phrased only for exact action values or an unrestricted policy class would leave out the errors introduced by fitting from samples and by moving the fitting distribution from the states of a comparator to the states visited by the current policy. Theorem 6.1 keeps those effects visible as separate terms. It also avoids assuming that the comparator is an optimal policy; the comparator can be a policy selected for an application or a benchmark within a restricted class.

Setting

A discounted Markov decision process has a finite state set S, a finite nonempty action set A, transition probabilities P(s'|s,a), immediate rewards r(s,a) in [0,1], and a discount factor γ in [0,1). A policy π assigns a probability distribution over A to every state. The value V^π(s) is the expected sum of discounted rewards from s, and V^π(ρ) averages this value over an initial state distribution ρ. The action value Q^π(s,a) starts by choosing a in s and then follows π. Its advantage is A^π(s,a)=Q^π(s,a)−V^π(s). These are the unnormalized value conventions of §3, pp. 9–12.

For each state-action pair, fix a feature vector φ(s,a) in Euclidean d-space. The log-linear policy with parameter θ assigns probability proportional to exp(θ·φ(s,a)):

$$\pi_\theta(a\mid s)= \frac{\exp(\theta\cdot\phi(s,a))} {\sum_{a'\in A}\exp(\theta\cdot\phi(s,a'))}.$$

The Q-NPG fitting loss $L(w;\theta,\upsilon)$ is the mean squared error of predicting $Q^{\pi_\theta}(s,a)$ by $w\cdot\phi(s,a)$ under a state-action distribution $\upsilon$. Q-NPG uses an approximate minimizer w of this loss under its current on-policy measure and updates θ by ηw. The distribution ν specifies the initial state-action pair for that measure. At time zero, the pair is drawn directly from ν; the given initial action is executed before later actions follow the current policy. These definitions are (19)–(20) of §6.2, pp. 27–28.

The comparison policy π⋆ has discounted state visitation distribution $d^{\pi^\star}_\rho$. The paper's transfer measure $d^\star$ pairs those states with a uniform action from A. The excess risk measures how much worse an approximate fitting direction is than an exact constrained minimizer under the current on-policy measure. The transfer error measures the exact minimizer's loss under $d^\star$. A relative condition number κ bounds, in every feature direction, the covariance quadratic form under $d^\star$ by κ times that under ν (Assumptions 6.1–6.2, pp. 28–29).

Formalization targets

Agnostic Q-NPG guarantee

The goal is Theorem 6.1, p. 29. Starting with θ⁽⁰⁾=0, taking T positive updates with step size $\eta=\sqrt{2\log|A|/(B^2W^2T)}$, bounding feature norms by B and update norms by W, and assuming the expected excess and transfer errors are at most $\varepsilon_{\rm stat}$ and $\varepsilon_{\rm bias}$, respectively, it asserts

$$\mathbb E\!\left[ \min_{t<T}\{V^{\pi^\star}(\rho)-V^{\pi_{\theta^{(t)}}}(\rho)\} \right] \le \frac{BW}{1-\gamma}\sqrt{\frac{2\log|A|}{T}} + \sqrt{\frac{4|A|\kappa\varepsilon_{\rm stat}}{(1-\gamma)^3}} + \frac{\sqrt{4|A|\varepsilon_{\rm bias}}}{1-\gamma}.$$

The expectation encloses the minimum: each random run may have a different best iterate. The claim gives a finite-horizon comparison with π⋆ even when π⋆ is not globally optimal.

Supporting targets

The milestones are the paper's performance-difference identity (Lemma 3.2), smoothness of bounded-feature log-linear policies (Remark 6.7), the deterministic NPG regret lemma (Lemma 6.2), and the two displayed bounds that control transfer and estimation terms ((25) and (26)). Together they connect the MDP's value comparison with the two statistical errors in the goal. Each milestone states a source result rather than a weakened surrogate.

Significance

The theorem separates three quantities that can vary independently in an application: the number of iterations, the statistical quality of the update direction, and the mismatch between the comparator's visited states and the fitting distribution. If both errors vanish, the displayed bound decreases with T at a square-root rate. With imperfect features, the transfer term shows the remaining performance limit. With finite-sample fitting, the excess-risk term shows how estimation quality affects the policy value. This is an agnostic statement because the comparator need not belong to a globally complete policy class (Agarwal et al., Theorem 6.1 and discussion, pp. 29–30).

The paper proves these claims mathematically. This mission asks for machine-checked proofs of the same statements in Lean, including the probabilistic expectation and the exact constants. The reusable parts are the state-action visitation distribution with a prescribed initial action, the log-linear policy and its smoothness property, the least-squares loss, and the deterministic regret lemma. Those objects can support other policy-gradient analyses with different fitting guarantees.

Difficulty

The update direction minimizes a loss under the distribution generated by the current policy, while the value comparison uses states visited by a different policy. The two distributions need not agree, and prediction error under one cannot simply be substituted for error under the other. The relative condition number controls the feature geometry of this shift, while the transfer error separately measures how well an exact on-policy fit predicts under the comparator's measure. Random approximate minimizers add a further layer: the bound concerns the expectation of the best iterate in each run, rather than a deterministic iterate chosen in advance. These are the obstacles identified around Assumptions 6.1–6.2 and the proof of Theorem 6.1.

Formalization scope

The Lean development uses finite state and action types, as in the paper's §3 standing setting. It imports published definitions of transition kernels, policies, occupation probabilities, value and Q-functions, and defines this paper's advantage, discounted visitation, log-linear class and fitting loss on top of them. Parameters and features lie in EuclideanSpace ℝ (Fin d), so the norm is the Euclidean norm used by the paper. A general probability space carries the random update directions and exact constrained minimizers; their measurability and boundedness make the displayed loss expectations integrable.

The action type is nonempty so that the uniform action distribution exists. B and W are positive and T is positive, because the prescribed step size divides by $B^2W^2T$ and the result minimizes over $t<T$. The comparator is assumed to be a policy, with no optimality hypothesis. The nonnegative condition number is represented by its quadratic-form upper-bound property for every direction. This avoids undefined real ratios when a covariance form vanishes and includes the finite coefficient in Assumption 6.2. The value and loss expressions are calculated from P, r, π and φ; they are not free variables. The Q-NPG parameter sequence is defined by the update rule from θ⁽⁰⁾=0. In particular, the goal does not assume the regret lemma or either of the two statistical inequalities that the proof must establish.

The paper notes that some §6 results extend beyond finite state or action spaces. This mission fixes the finite case inherited from §3. Contributions that prove the source milestones, establish the required summability and integrability facts, or generalize the development to larger measurable spaces are useful; a generalization must keep the same statistical and comparator conventions.

Selected references

• Alekh Agarwal, Sham M. Kakade, Jason D. Lee and Gaurav Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. arXiv:1908.00261v5
• Sham M. Kakade and John Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning, 2002. PDF

Motivation

Policy gradient methods adjust a policy by following derivatives of its expected reward. A common expectation is that a small gradient indicates a policy close to optimal. For discounted Markov decision processes, that interpretation can fail when a policy rarely reaches the states where reward is available. Agarwal, Kakade, Lee, and Mahajan study this obstruction as part of their analysis of optimality and distribution shift in policy gradient methods. Their chain example makes the obstruction quantitative: even derivatives of several orders can be exponentially small while the value gap grows with the chain length. Agarwal et al., §4.3 and Proposition 4.1.

The example isolates a specific issue for local optimization. A parameter change at an early state affects reward only after the agent has passed through many intermediate decisions. A local derivative therefore measures the behavior of a policy under its own visitation pattern, which can be very different from the visitation pattern of an optimal policy. This mission states the resulting separation with explicit constants rather than treating “vanishing gradients” as a qualitative description.

Setting

A discounted Markov decision process has a finite set of states, a finite set of actions, a transition probability for each state and action, a reward in $[0,1]$, and a discount $0\le\gamma<1$. The value $V^\pi(s)$ of a policy $\pi$ is the expected sum of discounted rewards when the process starts in state $s$ and follows $\pi$. An optimal policy $\pi^\star$ has value at least as large as every other policy at every state. These conventions are those of §3 of the paper and its unnormalized infinite-horizon value definition. Agarwal et al., §3, pp. 9–12.

The central model is a deterministic chain with states $s_0,s_1,\ldots,s_{H+1}$ and four actions. At $s_0$ the process moves to $s_1$. At each interior state $s_i$, action $a_1$ moves forward to $s_{i+1}$, while $a_2,a_3,a_4$ move backward to $s_{i-1}$. State $s_{H+1}$ is absorbing. The only positive reward is $r(s_{H+1},a_1)=1$, and $\gamma=H/(H+1)$. This is Figure 2 and the transition matrix in equation (27). Agarwal et al., Figure 2, p. 11, and (27), p. 50.

The direct policy parameter $\theta$ has three free coordinates at each interior state: the probabilities assigned to $a_1,a_2,a_3$. The probability of $a_4$ is their complement. Write $\pi_\theta$ for this policy expression and $F_H(\theta)=V^{\pi_\theta}(s_0)$ for its value from the starting state. The paper studies parameters whose free coordinates lie strictly between zero and one and whose forward-action coordinates satisfy $\theta_{i,a_1}<1/4$.

Formalization targets

The goal is Proposition 4.1. For $H\ge1$, every such $\theta$, and every nonnegative integer $k$ satisfying $k\le H/(40\log(2H))-1$, it asserts the multilinear operator-norm bound

$$\|\nabla^k F_H(\theta)\|_{\mathrm{op}}\le (1/3)^{H/4}.$$

The same statement compares this policy with an optimal policy:

$$V^{\pi^\star}(s_0)-F_H(\theta) \ge \frac{H+1}{8}-\frac{(H+1)^2}{3^H}.$$

Both clauses and their constants are part of the target. The derivative order includes $k=0$ whenever the displayed threshold admits it. Agarwal et al., Proposition 4.1, p. 16.

Three supporting targets follow the appendix's attack path. First, $F_H(\theta)$ equals the $(0,H+1)$ entry of the resolvent $M^p=(I-\gamma P^p)^{-1}$, where $p_i=\theta_{i,a_1}$. Second, equation (32) gives the derivative of any entry of $M^p$ in one forward probability. Third, the appendix separately bounds the optimal value below by $(H+1)/8$ and $F_H(\theta)$ above by $(H+1)^2/3^H$. A companion theorem records Lemma 3.1: a five-state deterministic example has a value function that is nonconcave in both the direct and softmax parameterizations. Agarwal et al., Appendix B.2, pp. 51, 54, 59; Lemma 3.1, p. 11.

Significance

The proposition supplies an explicit family in which local derivative information, even at orders growing with $H/\log H$, is small at policies with a large value gap. It limits what a guarantee based only on finding a point with small low-order derivatives can imply about global policy quality. The paper uses this example to motivate attention to state visitation and distribution mismatch in its positive results. Agarwal et al., §4.3, pp. 16–17.

The mathematical result is proved in the cited paper. The remaining work is a machine-checked development of the chain model, its value and resolvent identities, the higher derivative estimates, and the value-gap inequality. The reusable parts include finite-state discounted value calculations, differentiation of a matrix inverse, and operator-norm estimates for multilinear derivatives. The statements in this proposal are proof targets; they do not themselves claim that those proofs have been formalized.

Difficulty

A policy can have a small gradient simply because it almost never reaches the rewarding state. The obvious inference from a near-zero gradient to near-optimal value therefore fails in this model. The technical difficulty is quantitative: each differentiation of a resolvent entry produces terms involving several entries, and the operator norm combines all mixed partial derivatives. The bound must remain exponentially small after that combination, uniformly over every derivative order allowed by the threshold. The second clause must simultaneously show that a policy taking the forward action reaches the reward often enough to create a large value gap. Agarwal et al., Appendix B.2, pp. 54–59.

Formalization scope

States are Fin (H + 2) and actions are Fin 4; the parameter space is EuclideanSpace ℝ (Fin H × Fin 3). Its norm is the Euclidean norm, so the norm of the iterated Fréchet derivative is the paper's multilinear operator norm. The first and last states have no free policy parameters. All four actions at $s_0$ induce the same transition to $s_1$, and the parameterized policy chooses $a_1$ at both boundary states. The resolvent is the matrix inverse of $I-\gamma P^p$; its milestone statements are restricted to interior probabilities $0<p_i<1$, where that inverse is nonsingular.

The displayed coordinate assumptions of Proposition 4.1 do not require the three free probabilities at a state to sum to at most one. The Lean goal retains exactly those assumptions. Its value expression is still determined by the forward probabilities, because every other action has the same backward transition and only the absorbing state yields reward. This prevents an added simplex constraint from silently narrowing the proposition. A constant function or a free value variable cannot replace the chain value: $F_H$ is computed from the concrete transition and reward arrays.

The development uses the published finite-state transition-kernel, policy, occupation, value, and optimal-policy definitions. Contributions needed for a proof include stochasticity of the chain, geometric-series evaluation of its absorbing reward, nonsingularity and differentiation of its resolvent, and estimates that pass from mixed partial derivatives to the Euclidean operator norm. For the companion example, direct parameters lie in the product of action simplices, with positive discount; at zero discount its value is constant and the nonconcavity claim would be false.

Selected references

• Alekh Agarwal, Sham M. Kakade, Jason D. Lee, Gaurav Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. arXiv:1908.00261v5.

Dual decomposition of dominance constraints

A stochastic dominance constraint asks a random outcome $X$ of a decision to be at least as good as a benchmark outcome $Y$ for every risk-averse decision maker: in the second-order version, $\mathbb E[u(X)] \ge \mathbb E[u(Y)]$ for every concave nondecreasing utility $u$. Dentcheva and Ruszczyński introduced optimization problems with such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim. 2003), where the outcome itself is the decision variable, and extended the theory in the paper this mission formalizes, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program. 2004, DOI 10.1007/s10107-003-0453-z), to outcomes $X_i = G_i(z)$ that depend nonlinearly on a decision $z$.

The paper's §4 builds a Lagrangian dual of these problems. The multipliers of the $i$-th dominance constraint are a utility function $u_i$ and an almost-sure multiplier $\theta_i$ for the coupling $X_i = G_i(z)$. The dual functional splits into a part $D_0$ that involves only the decision $z$ and one part $D_i$ per dominance constraint. This mission is about the second kind of part: Theorem 4 computes $D_i$ in closed form as a concave conjugate, and Theorem 5 gives its subgradients. Those two facts are what make the dual problem amenable to nonsmooth optimization and decomposition methods, which is the purpose the paper states for them.

The underlying shortfall function $F_2(X;\eta)=\int_{-\infty}^{\eta}P[X\le\alpha]\,d\alpha$ and its dual characterization are due to Ogryczak and Ruszczyński (Dual stochastic dominance and related mean–risk models, SIAM J. Optim. 2002). The pure-dominance case of the optimality theory is the 2003 paper above.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space, $\mathcal L_1$ the integrable and $\mathcal L_\infty$ the essentially bounded random variables. Fix a bounded interval $[a,b]$ ($a\le b$) and a reference outcome $Y\in\mathcal L_1$.

The utility class $\mathcal U_1([a,b])$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave and nondecreasing, vanish on $[b,\infty)$, and are affine on $(-\infty,a]$: $u(t)=u(a)+c(t-a)$ for $t\le a$, with a constant $c\ge 0$. For such $u$, the left derivative $u'_-(a)$ at $a$ is that slope $c$.

The concave conjugate of $v:\mathbb R\to\mathbb R$ is

$$v^*(\xi)=\inf_{t\in\mathbb R}\,[\xi t-v(t)]\in[-\infty,+\infty).$$

For a random variable $\zeta$, $v^*(\zeta)$ is the extended-real random variable $\omega\mapsto v^*(\zeta(\omega))$.

The dual functional of one dominance constraint, eq. (34), is

$$D(w,\zeta)=\sup_{X\in\mathcal L_1}\mathbb E\big[w(X)-w(Y)-\zeta X\big]\in\overline{\mathbb R},\qquad w\in\mathcal U_1([a,b]),\ \zeta\in\mathcal L_\infty .$$

The functional of eq. (35) is $f(v,\zeta)=-\mathbb E\,v^*(\zeta)$, considered on $\mathrm{Lip}(\mathbb R)\times\mathcal L_1$, where $\mathrm{Lip}(\mathbb R)$ is the space of Lipschitz functions with norm $\|v\|_{\mathrm{Lip}}=|v(0)|+\sup_{t\ne s}|v(t)-v(s)|/|t-s|$.

Formalization targets

Goal: Theorem 4

For every $v\in\mathcal U_1([a,b])$ and every $\zeta\in\mathcal L_\infty$,

$$D(v,\zeta)=-\mathbb E\big[v^*(\zeta)+v(Y)\big].$$

The formal statement has two cases. If $0\le\zeta\le v'_-(a)$ almost surely, then $v^*(\zeta)$ is a.s. finite and integrable and the identity holds between real numbers. Otherwise $D(v,\zeta)=+\infty$.

Milestones

1. Unbounded cases (proof of Theorem 4, p. 13): $P[\zeta<0]>0 \Rightarrow D(v,\zeta)=+\infty$; and $P[\zeta>v'_-(a)]>0 \Rightarrow D(v,\zeta)=+\infty$.
2. Pointwise maximizer (p. 13): for $0\le\xi\le v'_-(a)$, the function $t\mapsto v(t)-\xi t$ attains its maximum at some $t_0\in[a,b]$, so $v^*(\xi)=\xi t_0-v(t_0)$ is finite.
3. Measurable selection (p. 13): if $0\le\zeta\le v'_-(a)$ a.s., there is a measurable $X\in[a,b]$ a.s. with $X(\omega)\in\operatorname{argmax}_t[v(t)-\zeta(\omega)t]$ a.s.
4. Effective domain (p. 13): $D(v,\zeta)<+\infty \iff 0\le\zeta\le v'_-(a)$ a.s.
5. Theorem 5 (p. 14): for $\bar v\in\mathcal U_1([a,b])$, $\bar\zeta\in\mathcal L_1$ with $0\le\bar\zeta\le\bar v'_-(a)$ a.s., and a measurable maximizer selection $X$ with values in $[a,b]$, the pair $(P_X,-X)$ is a subgradient of $f$ at $(\bar v,\bar\zeta)$:

$$f(v,\zeta)\ge f(\bar v,\bar\zeta)+\int\big(v-\bar v\big)\,dP_X-\mathbb E\big[X(\zeta-\bar\zeta)\big]\quad\text{for all }(v,\zeta)\in\mathrm{Lip}(\mathbb R)\times\mathcal L_1.$$

Significance

Theorem 4 reduces an optimization over the infinite-dimensional space $\mathcal L_1$ to one scalar maximization per scenario: the dual functional is an expected conjugate. It identifies the effective domain of the dual in the multiplier $\zeta$ (bounded between $0$ and the slope of the utility at the left end of the interval), and it makes evaluating $D$ as cheap as evaluating $v^*$. Theorem 5 supplies explicit subgradients, the law of a maximizer and the maximizer itself, which is what bundle and cutting-plane methods for the dual problem (31) consume. The paper's §5–§6 build their finite-scenario theory and numerical method on this decomposition.

Both theorems are proved in the paper. Neither has a machine-checked proof; no concave conjugate on $\mathbb R$ with values in $[-\infty,+\infty)$, no dual functional of this kind, and no measurable-selection theorem for argmax correspondences of this shape exist on the platform. A complete formalization would provide reusable infrastructure: an extended-real concave conjugate, interchange of supremum and expectation for a scalar integrand with a bounded maximizer, and a concrete measurable-selection argument.

Difficulty

The hard step is the interchange $\sup_{X\in\mathcal L_1}\mathbb E[\,\cdot\,]=\mathbb E\sup_t[\,\cdot\,]$. The inequality "$\le$" is pointwise, but "$\ge$" needs a random variable that attains the pointwise maximum, is measurable, and is integrable. The paper cites Rockafellar–Wets for both the interchange and the selection. The maximizers are not unique: where $\zeta(\omega)=0$ or $\zeta(\omega)=v'_-(a)$ the argmax is an unbounded half-line, so an arbitrary measurable selection need not be integrable, and the bounded one must be constructed. The unbounded cases need care because $\zeta$ is only essentially bounded and the test outcomes $M\mathbb 1_{\{\zeta<0\}}$ must be shown integrable.

Formalization scope

This chunk's objects are in NonlinSSD.DualFunctional; it imports the already moderated utility class NonlinSSD.Optimality.U1. Random variables are functions $\Omega\to\mathbb R$ on a probability space with IsProbabilityMeasure P; $\mathcal L_1$ is Integrable, $\mathcal L_\infty$ is MemLp ζ ⊤ P. The conventions and explicit readings:

• $c\ge 0$ in $\mathcal U_1([a,b])$. The paper prints $c>0$. The page calls $\mathcal U_1([a,b])$ a convex cone, which must contain $0$, and the companion optimality theorem fails with $c>0$; the formalization uses $c\ge0$.
• Left derivative $v'_-(a)$ is derivWithin v (Set.Iic a) a, never deriv v a, which is $0$ at a kink.
• Extended values. $v^*$, $D$ and $f$ are EReal-valued, so an infimum equal to $-\infty$ and a supremum equal to $+\infty$ are represented, not replaced by $0$. The supremum in $D$ is over integrable $X$ only.
• Theorem 4 in two cases. The paper's right side is an expectation of an extended-real random variable, read as $+\infty$ off the domain. The statement separates the finite case (Bochner integral of the real part, with a.s. finiteness and integrability asserted) from the infinite case, which avoids extended-real subtraction.
• $f$ equals the Bochner integral of $-v^*(\zeta)$ when $v^*(\zeta)$ is a.s. finite with integrable real part, and $+\infty$ otherwise. This is exact because $-v^*(\zeta)\ge v(0)$.
• Theorem 5 adds the hypothesis that the selection lies in $[a,b]$ a.s. As printed ("for every measurable selection") it is false: with $a=-1$, $b=0$, $\bar v(t)=\min(t,0)$, $\bar\zeta=0$ on $[0,1]$ with Lebesgue measure, the selection $X(\omega)=1/\omega$ is not integrable. The continuity of $(P_X,-X)$ as a functional is stated as $X\in\mathcal L_\infty$ and the bound $\int|v|\,dP_X\le(|v(0)|+K)(1+\mathbb E|X|)$ for $K$-Lipschitz $v$.
• The paper's index $i$ and the standing data of §4 ($Y\in\mathcal L_1$, $a\le b$) are explicit binders.

A trivializing formalization is ruled out: a real-valued conjugate or dual functional (junk $0$ at $\mp\infty$), a supremum over all measurable $X$ (junk integrals), or a one-sided case split would each make the goal easier than the paper's theorem, and a sorry-free check confirms that both cases of Theorem 4 are inhabited ($v=\min(t,0)$, $\zeta=1/2$ and $\zeta=2$).

Contributions are welcome at every level: proofs of the milestones in order, general lemmas on extended-real conjugates on $\mathbb R$, and a measurable argmax selection for continuous integrands over a compact interval, which is reusable well beyond this paper.

Selected references

• D. Dentcheva, A. Ruszczyński, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints, Math. Program. 99 (2004). Author manuscript, rev. April 2003. https://doi.org/10.1007/s10107-003-0453-z
• D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14 (2003). https://doi.org/10.1137/S1052623402420528
• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean–risk models, SIAM J. Optim. 13 (2002). https://doi.org/10.1137/S1052623400375075
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998 (Theorems 14.37, 14.60). https://doi.org/10.1007/978-3-642-02431-3

Motivation

Many feasibility problems ask for a point satisfying several constraints at once. When each constraint set admits a manageable Euclidean projection, a parallel method can project onto all sets independently and combine the results. Chapter 5 of Boyd, Parikh, Chu, Peleato and Eckstein (2011) places this construction inside the alternating direction method of multipliers (ADMM). That connection matters when a single projection onto the intersection is difficult but projections onto its individual factors are available.

The chapter first rewrites constrained convex optimization as a split problem. It then treats feasibility for two sets and finally an arbitrary finite collection of sets. For the latter, the product of the sets captures the separate constraints, while a consensus set forces all copies of the variable to agree. These are ordinary finite dimensional convex sets, so the account applies to geometric feasibility and to constrained optimization subproblems in which projection is the computational primitive. The mission isolates the identities that let the product-space algorithm run through parallel individual projections and one average.

Setting

A Euclidean projection of a vector $v$ onto a set $C$ is a point $p\in C$ closest to $v$ in Euclidean distance. Each set $\mathcal A_i\subseteq\mathbb R^n$, for $i=1,\ldots,N$, is assumed nonempty, closed and convex, and $N\ge1$. These properties give a unique projection for every input. They do not require the common intersection $\bigcap_i\mathcal A_i$ to be nonempty: the iteration and the algebraic identities still make sense when the feasibility problem has no solution.

A block vector $x=(x_1,\ldots,x_N)$ belongs to the product set $\mathcal C=\mathcal A_1\times\cdots\times\mathcal A_N$ exactly when $x_i\in\mathcal A_i$ for all $i$. The consensus set $\mathcal D$ consists of constant block vectors $(z,\ldots,z)$. The block average is $\bar x=N^{-1}\sum_i x_i$. Distances in the stacked space use the ordinary Euclidean metric, whose square is $\sum_i\|x_i-y_i\|_2^2$. A block vector need not carry a function-space norm in the formalization for this metric to be stated precisely.

Starting with arbitrary $z^0\in\mathbb R^n$ and $u^0=(u_i^0)$, the parallel projection ADMM run has three updates: each $x_i^{k+1}$ is the projection of $z^k-u_i^k$ onto $\mathcal A_i$; $z^{k+1}$ is the average of $x_i^{k+1}+u_i^k$; and $u_i^{k+1}=u_i^k+x_i^{k+1}-z^{k+1}$. The $u_i^k$ are scaled dual variables, formed using a penalty parameter $\rho>0$. The source presents these equations as the specialization of scaled ADMM for the indicator functions of $\mathcal C$ and $\mathcal D$ §5.1.2, pp. 35–36.

Formalization targets

The first targets identify the projections that make the iteration parallel:

$$\Pi_{\mathcal C}(x)=(\Pi_{\mathcal A_1}(x_1),\ldots,\Pi_{\mathcal A_N}(x_N)),\qquad \Pi_{\mathcal D}(x)=(\bar x,\ldots,\bar x).$$

The goal is the full reduction of a run. Its dual average is zero after every update, and its common vector equals the primal average from the following update onward:

$$\bar u^{k+1}=0\quad(k\ge0),\qquad z^{k+1}=\bar x^{k+1}\quad(k\ge1).$$

Consequently, for every $k\ge2$ and every $i$, the same iterates obey the simpler two-line algorithm

$$x_i^{k+1}=\Pi_{\mathcal A_i}(\bar x^k-u_i^k),\qquad u_i^{k+1}=u_i^k+x_i^{k+1}-\bar x^{k+1}.$$

If $\bar u^0=0$, those last identities hold already for $k\ge1$. The index qualification is necessary because $z^0$ is arbitrary, and $z^1$ still contains the initial dual average unless that average was zero. This is the precise reading of the source's “after the first step” statement §5.1.2, p. 36. The milestone list also records the indicator-function projection update on p. 33 and the averaged identities on p. 36.

Significance

The result identifies what information must pass between the parallel projection steps: each local step needs the shared average and its own dual displacement. It also fixes the relationship between the displayed three-variable ADMM iteration and the shorter project-and-average rule. Without the dual-average identity, replacing $z^k$ by $\bar x^k$ is not justified at the initial indices. The product and consensus projection identities explain why the update can be decomposed into independent local projections followed by a mean §5.1.2, p. 35.

The chapter's identities are known mathematical results; this mission asks for machine-checked proofs of their stated finite dimensional version. A completed development supplies reusable statements about nearest-point projection onto products and diagonal sets, and a precise run predicate for later analysis of parallel ADMM. The goal is a statement about every valid run rather than a claim of convergence or existence of a feasible common point. Neither convergence nor feasibility of the intersection is concluded on these pages. Those distinctions keep the mission aligned with the actual scope of Chapter 5.

Difficulty

The product projection uses a sum of squared component distances. Treating a block vector as an arbitrary function and applying its default norm would change the metric, so a projection theorem stated that way would describe a different algorithm. The consensus projection likewise depends on the Euclidean sum and the finite average, including the condition $N\ge1$. The run reduction has a separate indexing difficulty: the vanishing average follows after one dual update, but the first simplified projection step can occur later because it uses the previous common vector. An argument that silently assumes $z^0=\bar x^0$ would erase the arbitrary initialization on the source page.

Formalization scope

Lean represents each $\mathbb R^n$ as EuclideanSpace ℝ (Fin n) and the $N$ blocks as a function on Fin N; the latter is the source's $1$-based indexing shifted to $0$-based indices. Squared stacked distance is defined as the sum of squared component norms. The average uses the real factor $1/N$ only under $0<N$. Individual projections reuse the published nearest-point relation RandomGradFree.Nonsmooth.IsMetricProjection. A run records the three updates as conditions on sequences, with arbitrary $z^0,u^0$ and unused $x^0$. The source's scaled dual variable $u$ appears directly; $\rho$ cancels from these projection updates once it is positive.

The source assumes closed convex sets; nonemptiness is stated explicitly here because a projection onto an empty set does not exist. The book prints $-z^k$ in its averaged dual update on p. 36, while its defining update on p. 35 and the next line on p. 36 require $-z^{k+1}$. The formal statement uses the corrected index. The book also calls the individual sets $\mathcal C_i$ in its closing sentence; the sets defined for this subsection are $\mathcal A_i$. The milestone quote preserves the printed intermediate index. The goal includes the simplified primal and dual updates, since asserting only that the dual average vanishes would omit the chapter's advertised reduction.

The development needs finite sums in Euclidean spaces, convex-set projection, and elementary properties of product and diagonal sets. Product and consensus projection results are useful beyond ADMM. Contributions proving the four milestones, the full run theorem, or equivalent projection lemmas at the same generality are within scope.

Selected references

• S. Boyd, N. Parikh, E. Chu, B. Peleato and J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011, pp. 1–122. DOI: 10.1561/2200000016.

Motivation

Alternating direction methods are used when one part of an optimization problem is easy to minimize and another part has a simple projection. Chapter 9 of Boyd, Parikh, Chu, Peleato and Eckstein (2011) examines this idea with nonconvex constraints. Its examples include sparse vectors, Boolean vectors and low-rank matrices. The chapter says explicitly that ADMM can fail to converge in this setting and that a limit need not be globally optimal. The useful claim here is narrower and concrete: several individual updates can still be computed exactly.

The capstone is factor-model fitting. A symmetric data matrix, such as an empirical covariance matrix, is approximated by a positive semidefinite matrix of prescribed rank plus a nonnegative diagonal matrix. This decomposition gives one component that captures shared variation and another that represents coordinate-specific variation. The chapter separates the diagonal fit from the rank constraint and writes the resulting ADMM X-update entry by entry. This mission formalizes that exact update and two other projection rules stated in the same chapter.

Setting

Fix a positive integer $n$. Write $\mathbb S^n$ for the real symmetric $n\times n$ matrices, and let $\Sigma\in\mathbb S^n$ be the matrix to approximate. The Frobenius norm squares and sums every ordered matrix entry: $\|X\|_F^2=\sum_{i,j}X_{ij}^2$. A vector $d\in\mathbb R^n$ is nonnegative when $d_i\ge0$ for every $i$, and $\operatorname{diag}(d)$ places those entries on a diagonal matrix. The book's reduced fitting loss is

$$f_\Sigma(X)=\inf_{d\ge0}\frac12\|X+\operatorname{diag}(d)-\Sigma\|_F^2.$$

In the scaled ADMM iteration, $Z$ carries the positive semidefinite rank constraint and $U$ is the scaled dual matrix. Given the current symmetric matrices $Z,U$ and a penalty $\rho>0$, the X-step minimizes $f_\Sigma(X)+(\rho/2)\|X-Z+U\|_F^2$ over $X\in\mathbb S^n$. The X-step itself has no rank or positive semidefinite restriction. The following Z-step projects onto the chosen rank-constrained positive semidefinite set. The theorem here concerns the X-step, whose definition is independent of the chosen rank.

The other two results concern Euclidean projection of vectors $v\in\mathbb R^n$. The cardinality $\operatorname{card}(x)$ is the number of nonzero coordinates of $x$. The sparse set is $\{x:\operatorname{card}(x)\le c\}$ for a nonnegative integer $c$. The Boolean cube is $\{0,1\}^n$. Projection means a nearest point in squared Euclidean distance; it may have more than one value when coordinates tie.

Formalization targets

Partial minimization of the diagonal

The first milestone identifies the book's infimum as the explicit componentwise loss and states that the optimizing diagonal is attained:

$$f_\Sigma(X)=\frac12\sum_{i\ne j}(X_{ij}-\Sigma_{ij})^2+ \frac12\sum_i(X_{ii}-\Sigma_{ii})_+^2, \qquad d_i=(\Sigma_{ii}-X_{ii})_+.$$

The sum over $i\ne j$ counts both $(i,j)$ and $(j,i)$. The statement preserves that convention instead of treating a symmetric matrix as a list of independent upper-triangular entries.

Exact projections for two nonconvex sets

The page 74 milestones say that retaining the $\min(c,n)$ entries of largest absolute value gives a nearest point in $\{x:\operatorname{card}(x)\le c\}$, and that rounding every coordinate to a nearest element of $\{0,1\}$ gives a nearest Boolean vector. They assert nearest-point status for ties without asserting uniqueness. These are chapter results on the same theme of exact nonconvex updates, although they are independent of the factor-model goal.

Factor-model X-update

The goal identifies the unique symmetric minimizer $X^+$ of the X-subproblem. With $a_{ij}=Z_{ij}-U_{ij}$, its off-diagonal and diagonal entries are

$$X^+_{ij}=\frac{\Sigma_{ij}+\rho a_{ij}}{1+\rho}\quad(i\ne j),\qquad X^+_{ii}=\begin{cases} \dfrac{\Sigma_{ii}+\rho a_{ii}}{1+\rho},&\Sigma_{ii}\le a_{ii},\\ a_{ii},&\Sigma_{ii}>a_{ii}. \end{cases}$$

The target asserts both the formula and global minimality over symmetric matrices. It does not replace minimality with a stationarity condition.

Significance

The exact X-update separates the matrix fit from the nonconvex rank projection. It establishes that the factor-model algorithm's X-step is a well-defined, single-valued minimization for every symmetric current state and every positive penalty. It also makes the one-sided diagonal loss explicit: a nonnegative diagonal can absorb a shortfall below $\Sigma_{ii}$, but cannot absorb an excess. The two vector projections give similarly exact updates for sparse and Boolean constraint sets.

The mathematical claims are given in §9.1–9.1.2 of the published monograph; they are not open conjectures. The formalization work is to check the infimum, projection and unique-minimizer statements with every domain and tie convention explicit. The mission poses theorem statements for proofs; these draft statements themselves do not yet supply machine-checked proofs. A complete development can reuse its finite matrix loss and finite vector projection vocabulary in other splitting algorithms.

Difficulty

The diagonal partial minimization is one-sided, while the proximal penalty is symmetric around $Z-U$. An entrywise formula alone does not show that the assembled matrix minimizes the full objective or that it is the only minimizer. Symmetry also couples the two displayed off-diagonal positions $(i,j)$ and $(j,i)$, so a scalar statement on one entry must agree with its transpose. For sparse projection, ties at the cutoff make a rule phrased as “the projection” ambiguous. For Boolean projection, the midpoint is a tie and requires a declared convention. These issues are part of the theorem statements, not numerical implementation details.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; symmetry is an entrywise equality predicate. The factor-model statements assume $n\ge1$, symmetric $\Sigma,Z,U$, and $\rho>0$. The book uses $Z^k,U^k$ at an iteration; the Lean theorem uses those current matrices as parameters and does not posit convergence of an ADMM sequence. The reduced loss is literally the infimum over all componentwise nonnegative $d$, and the Frobenius square is the finite sum of entry squares. The stated X-minimization ranges over all symmetric matrices, with no positive semidefinite or rank hypothesis on $X$.

For sparse vectors, the index set has size $\min(c,n)$ and its selected magnitudes dominate unselected ones. This covers $c=0$, $c>n$ and cutoff ties. The Boolean rounding function chooses zero when an entry equals $1/2$. The book uses indices $1,\ldots,n$; Fin n uses $0,\ldots,n-1$. On page 75 the printed diagonal branch conditions omit the superscript $k$ on $Z$ and $U$; the formalization uses the current $Z,U$ that appear in the surrounding ADMM update. The theorem requires the candidate to minimize the book's reduced loss, preventing an arbitrary replacement loss from making the statement trivial.

The development needs finite-sum algebra, real infima with an attained lower bound, symmetry of matrices, and nearest-point arguments for finite vectors. The rank-$c$ singular-value projection on page 74 is already an open target elsewhere and is outside this mission. The positive semidefinite rank-$k$ eigenvalue projection on page 76 is also outside this goal; it would require a separate spectral development. Contributions that prove the three milestones or the goal against these definitions are in scope. The page also mentions rounding under integer constraints; this mission selects the preceding Boolean claim as its projection milestone.

Selected references

• Stephen Boyd, Neal Parikh, Eric Chu, Borja Peleato and Jonathan Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011, pp. 73–76, §§9.1–9.1.2. DOI: 10.1561/2200000016.

Motivation

In distributionally robust modelling, a baseline probability model $\mu$ on a space $S$ is distrusted, and the analyst reports the largest expected loss over every model within a budget of $\mu$. Blanchet and Murthy (arXiv:1604.01446; Math. Oper. Res. 44(2), 2019, doi:10.1287/moor.2018.0936) measure the budget with an optimal transport cost and prove strong duality for the resulting worst-case expectation on an arbitrary Polish space, with a lower semicontinuous cost and an upper semicontinuous performance function. Duality computes the worst-case value. A risk manager also wants the worst-case model: a distribution that attains the value, whose structure explains which perturbation of $\mu$ is most harmful.

Such a model need not exist. Unlike the Kantorovich problem, where the set of couplings with two fixed marginals is weakly compact, the feasible set here fixes only one marginal and is not compact in general. Section 5 of the paper gives an example on $\mathbb R$ where the supremum is not attained, then gives abstract conditions under which it is (Proposition 9), and growth conditions on a locally compact normed space that imply them (Corollary 1). Related existence results in $\mathbb R^d$ were obtained by Gao and Kleywegt (arXiv:1604.02199, 2016) and, for empirical baselines and norm costs, by Mohajerin Esfahani and Kuhn (arXiv:1505.05116, 2018).

Setting

Let $S$ be a Polish space with its Borel $\sigma$-algebra, $\mu$ a probability measure on $S$, $\delta>0$ a budget, $c:S\times S\to[0,\infty)$ a cost and $f:S\to\mathbb R$ a performance function. The standing assumptions are:

• (A1) $c$ is lower semicontinuous and $c(x,y)=0$ iff $x=y$;
• (A2) $f$ is upper semicontinuous and $\mu$-integrable.

The primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S\times S$ with first marginal $\mu$ and $\int c\,d\pi\le\delta$ (transport plans out of $\mu$ of cost at most $\delta$). The primal objective is $I(\pi)=\int f(y)\,d\pi(x,y)$ and the primal value is $I=\sup\{I(\pi):\pi\in\Phi_{\mu,\delta}\}$. The dual feasible set $\Lambda_{c,f}$ consists of pairs $(\lambda,\varphi)$ with $\lambda\ge0$, $\varphi:S\to[-\infty,\infty]$ universally measurable and $\varphi(x)+\lambda c(x,y)\ge f(y)$ for all $x,y$. The dual objective is $J(\lambda,\varphi)=\lambda\delta+\int\varphi\,d\mu$ and the dual value is $J=\inf J(\lambda,\varphi)$. For $\lambda\ge0$ put $\varphi_\lambda(x)=\sup_y\{f(y)-\lambda c(x,y)\}$.

Section 5 assumes throughout that $(\lambda^*,\varphi_{\lambda^*})\in\Lambda_{c,f}$ is a dual optimal pair with $I=J=J(\lambda^*,\varphi_{\lambda^*})<\infty$. Write $\Phi'_{\mu,\delta}$ for the plans in $\Phi_{\mu,\delta}$ concentrated on $\{f(x)\le f(y)\}$.

(P-Compactness): for every $\varepsilon>0$ there are a compact $K_\varepsilon$ with $\mu(K_\varepsilon)>1-\varepsilon$ and $\gamma>0$ such that $\{(x,y)\in K_\varepsilon\times S: f(y)-\lambda^*c(x,y)\ge\varphi_{\lambda^*}(x)-\gamma\}$ has compact closure. (P-USC): $\limsup_n I(\pi_n)\le I(\pi^*)$ whenever $\pi_n\in\Phi'_{\mu,\delta}$ converge weakly to $\pi^*\in\Phi_{\mu,\delta}$.

On a normed space $E$: (A3) $c(x,y)\ge g(\|x-y\|)$ for $\|x-y\|>C$, with $g$ nondecreasing and $g(t)\uparrow\infty$. (A4) $(f(y)-f(x))/(1+h(\|x-y\|))\le K$ for an increasing $h$ with $h(t)\uparrow\infty$; and for every $\varepsilon>0$, $f(y)-f(x)\le\varepsilon(1+c(x,y))$ once $\|x-y\|>C_\varepsilon$.

Formalization targets

Goal: Corollary 1 (p. 27)

Let $E$ be a real normed space that is locally compact, and let $c,f$ satisfy (A1)–(A4). Under the standing assumption, if $\lambda^*>0$ there is $\pi^*\in\Phi_{\mu,\delta}$ with

$$I(\pi^*)=I=J=J(\lambda^*,\varphi_{\lambda^*}).$$

Milestones

1. Remark 4, (10)–(11) (p. 8): for $\pi\in\Phi_{\mu,\delta}$, $I-I(\pi)$ is the sum of two nonnegative gaps, $\int(\varphi_{\lambda^*}(x)-f(y)+\lambda^*c(x,y))\,d\pi$ and $\lambda^*(\delta-\int c\,d\pi)$; so an $\varepsilon$-optimal plan has both gaps at most $\varepsilon$.
2. Lemma 17 (p. 43): every plan in $\Phi_{\mu,\delta}$ can be replaced by one in $\Phi'_{\mu,\delta}$ with at least the same value.
3. §5 display (p. 26): $I=\sup\{I(\pi):\pi\in\Phi'_{\mu,\delta}\}$.
4. Proposition 9 (p. 26): on a Polish space, (P-Compactness) and (P-USC) give a primal optimizer.
5. Corollary 1, Step 1 (p. 28): (A1)–(A4) and $\lambda^*>0$ give (P-Compactness).
6. Corollary 1, Step 2 (pp. 28–29): (A1), (A2), (A4) and $I<\infty$ give (P-USC):

$$\limsup_n\int f(y)\,d\pi_n\le\int f(y)\,d\pi^*.$$

Significance

The result. An attained worst case turns duality into a structural statement. By Theorem 1(b) of the paper, an optimizer moves mass from $x$ only to maximizers of $f(y)-\lambda^*c(x,y)$ and, when $\lambda^*>0$, uses the full budget. When those maximizers are unique (Remark 8: $c$ convex in $y$, $f$ concave) the worst-case model is unique and is the image of $\mu$ under a transport map. That map is what stress tests and robust estimators are built from. Without existence, these statements describe an object that may not be there.

Formalizing it. The paper's proofs are complete; nothing here is open. No machine-checked version of this result is known: the worst-case optimal transport literature, including the strong duality of this paper, is unformalized. The mission produces the transport objects of §2 in a form that keeps the paper's generality (Polish space, lower semicontinuous real cost, universally measurable dual variables, the $\infty-\infty$ convention), a tightness argument for nearly optimal one-marginal plans, and an upper semicontinuity argument for unbounded upper semicontinuous integrands under uniform integrability.

Difficulty

The obvious argument takes a maximizing sequence and extracts a weak limit. Both steps fail without more structure. First, $\Phi_{\mu,\delta}$ is not tight: only the first marginal is fixed, and a sequence may push mass to infinity at bounded cost. That is exactly what happens in Example 2 (p. 26), where $\lambda^*=0$ and the value $1$ is approached but never reached. Tightness has to come from the dual: nearly optimal plans concentrate near maximizers of $f(y)-\lambda^*c(x,y)$, and (A3)–(A4) with $\lambda^*>0$ confine those maximizers. Second, $f$ is only upper semicontinuous and unbounded, so weak convergence alone does not give $\limsup\int f\,d\pi_n\le\int f\,d\pi^*$. A uniform integrability bound is needed, and it uses the restriction to $\Phi'_{\mu,\delta}$ in an essential way. A third, Lean-specific difficulty is measure-theoretic: $\varphi_{\lambda^*}$ is only universally measurable, and the gaps of Remark 4 are integrals against completions.

Formalization scope

All declarations sit in the namespace ModelRiskOT.PrimalOpt. Values of $I(\pi)$, $I$, $J(\lambda,\varphi)$, $J$ and $\varphi_\lambda$ are in EReal. $I(\pi)$ is $\int f^+(y)\,d\pi-\int f^-(y)\,d\pi$ with lower integrals, and Mathlib's $\top-\top=\bot$ realises the paper's reading of the supremum (footnote 2, p. 5). Integrals of nonnegative or extended-real functions are lower integrals (lintegral), never Bochner integrals. Universal measurability is the published BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. Weak convergence is the topology of ProbabilityMeasure (S × S). Measures on $S\times S$ use the product $\sigma$-algebra.

The following readings are fixed:

• The standing assumption of §5 ($(\lambda^*,\varphi_{\lambda^*})\in\Lambda_{c,f}$, $I=J$, $J=J(\lambda^*,\varphi_{\lambda^*})$, finiteness) consists of hypotheses of Proposition 9 and Corollary 1. $I=J$ is Theorem 1(a), the goal of the companion mission on strong duality, and is not assumed proved here.
• In (P-Compactness) the constant $\gamma$ may depend on $\varepsilon$.
• "Increasing" in (A4) is strict.
• Remark 4's second conclusion in (11) is also stated as $\lambda^*(\delta-\int c\,d\pi)\le\varepsilon$, which covers $\lambda^*=0$.
• Lemma 17's last inequality is stated for every plan, which is equivalent under the EReal convention.
• Corollary 1's space is a real normed space with LocallyCompactSpace. It also carries PolishSpace, which is redundant, since a locally compact real normed space is finite-dimensional.

The goal cannot be satisfied by a junk value: $I$ and $J$ are EReal suprema and infima, not real sSup, and the hypothesis $\lambda^*>0$ is kept because Example 2 shows the conclusion fails without it. A sorry-free check that $c(x,y)=(x-y)^2$, $f(y)=y$ on $\mathbb R$ satisfy (A1), (A3) and (A4) accompanies the drafts.

A complete development needs Prokhorov's theorem (in Mathlib), a Fatou lemma for weakly converging measures with a lower semicontinuous integrand, an upper semicontinuity theorem for uniformly integrable upper semicontinuous integrands, and the change of variables $\int\varphi(x)\,d\pi=\int\varphi\,d\mu$ for universally measurable $\varphi$. The last three are reusable well beyond this mission. Proofs of any milestone, and these general lemmas as separate contributions, are welcome.

Selected references

• J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2):565–600, 2019. arXiv:1604.01446v2, doi:10.1287/moor.2018.0936
• R. Gao and A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, 2016. arXiv:1604.02199
• P. Mohajerin Esfahani and D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171:115–166, 2018. arXiv:1505.05116
• A. M. Zapała, Unbounded mappings and weak convergence of measures, Statist. Probab. Lett. 78(6):698–706, 2008. doi:10.1016/j.spl.2007.09.033
• C. Villani, Optimal Transport: Old and New, Springer, 2009. doi:10.1007/978-3-540-71050-9

Motivation

A probability model $\mu$ for a risk quantity, such as the reserve process of an insurer or the path of a queue, is usually chosen for tractability or fitted to limited data, and the true law of the system is unknown. Distributional model risk asks how large a probability of interest could be if the true law were any model "close" to $\mu$. When closeness is measured by an optimal transport cost rather than a likelihood ratio, the competing models may put mass where $\mu$ puts none, which is the situation for rare events such as ruin or buffer overflow: the event of interest often lies outside the support of the baseline.

Blanchet and Murthy (arXiv:1604.01446, Mathematics of Operations Research 44(2), 2019) prove strong duality for worst-case expectations over an optimal-transport ball on a general Polish space, with a lower semicontinuous cost. Their §2.4 specializes the duality to worst-case probabilities of a closed set and obtains a closed-form answer: the worst-case probability of $A$ is the baseline probability of an inflated version of $A$. This mission formalizes that result, Theorem 3 of the paper, together with the numbered statements its proof uses.

Setting

Let $S$ be a Polish space with its Borel $\sigma$-algebra, $P(S)$ its probability measures, and $\mu \in P(S)$ the baseline. A cost $c : S \times S \to \mathbb R_+$ satisfies Assumption (A1): it is nonnegative, lower semicontinuous, and $c(x,y) = 0$ if and only if $x = y$.

For $\mu_1, \mu_2 \in P(S)$, a coupling of $\mu_1$ and $\mu_2$ is a probability measure $\pi$ on $S \times S$ with marginals $\mu_1$ and $\mu_2$; $\Pi(\mu_1,\mu_2)$ is the set of couplings, and the optimal transport cost is

$$d_c(\mu_1,\mu_2) = \inf\Big\{\int c\,d\pi : \pi \in \Pi(\mu_1,\mu_2)\Big\}.$$

For a budget $\delta > 0$, the primal feasible set $\Phi_{\mu,\delta}$ consists of the probability measures $\pi$ on $S \times S$ with first marginal $\mu$ and $\int c\,d\pi \le \delta$.

Fix a nonempty closed set $A \subseteq S$ and let $c(x,A) = \inf\{c(x,y) : y \in A\}$ be the cheapest cost of moving unit mass from $x$ into $A$. The worst-case probability is

$$I = \sup\{P(A) : d_c(\mu,P) \le \delta\}. \tag{12}$$

Its dual is the univariate problem

$$\inf_{\lambda \ge 0}\Big\{\lambda\delta + E_\mu\big[(1 - \lambda c(X,A))^+\big]\Big\}, \tag{13}$$

and for a minimizer $\lambda^* \in [0,\infty)$ of (13) the paper defines

$$\underline c = \int_{\{c(x,A) < 1/\lambda^*\}} c(x,A)\,d\mu(x), \qquad \overline c = \int_{\{c(x,A) \le 1/\lambda^*\}} c(x,A)\,d\mu(x). \tag{14}$$

Formalization targets

Goal: Theorem 3 (p. 10)

If $\lambda^* \in [0,\infty)$ attains the infimum in (13) and $\underline c = \overline c$, then

$$\sup\{P(A) : d_c(\mu,P) \le \delta\} = \mu\{x : c(x,A) \le 1/\lambda^*\}. \tag{15}$$

Milestones, in the order the proof uses them

1. Coupling form (§2.2, p. 5, for $f = 1_A$): $I = \sup\{\pi(S \times A) : \pi \in \Phi_{\mu,\delta}\}$.
2. Indicator supremum (pp. 8–9): $\sup_{y}\{1_A(y) - \lambda c(x,y)\} = (1 - \lambda c(x,A))^+$ for $\lambda \ge 0$.
3. (13) (p. 9): $I$ equals the infimum in (13).
4. Remark 4, (11) for $f = 1_A$ (p. 8): an $\varepsilon$-optimal plan $\pi_\varepsilon$ satisfies $\int(\varphi_{\lambda^*}(x) - (1_A(y) - \lambda^* c(x,y)))\,d\pi_\varepsilon \le \varepsilon$ and, for $\lambda^* > 0$, $(\delta - \varepsilon/\lambda^*)^+ \le \int c\,d\pi_\varepsilon \le \delta$.
5. Lemma 4 (p. 11): plans $\pi_n \in \Phi_{\mu,\delta}$, $n > 1$, with $\pi_n(C_n) \ge 1 - 1/n$, no cost outside the set $C_n$ of §2.4.1, and $\pi_n(S \times A) \ge I - 2/n$.
6. Lemma 2 (p. 10): $\underline c \le \delta \le \overline c$ if $\lambda^* > 0$ attains (13); $\delta \ge \overline c = \underline c$ if $\lambda^* = 0$ does.

Significance

Theorem 3 converts a supremum over an infinite-dimensional ball of probability measures into a single probability under the baseline: $\mu$ of the set of points that can reach $A$ at cost at most $1/\lambda^*$, where $1/\lambda^*$ is determined by $\delta$ through the one-dimensional function $u \mapsto \int_{\{c(x,A) \le u\}} c(x,A)\,d\mu$. For the cost $c = d$ of a metric this is the baseline probability of the $1/\lambda^*$-neighbourhood of $A$. The paper uses it to compute worst-case ruin probabilities for the Cramér–Lundberg model around a Brownian approximation (§3, §6.1), where $S$ is a path space; the result applies there because nothing in it uses local compactness of $S$.

The result is proved in the paper. As far as the platform's corpus shows, neither it nor the strong duality behind it has been formalized. A formal development produces, beyond Theorem 3: a reusable definition of optimal transport costs with lower semicontinuous costs on Polish spaces; the coupling reformulation of the transport ball, which rests on the existence of optimal transport plans (Villani, Optimal Transport, Theorem 4.1), not in Mathlib; and an $\varepsilon$-optimal-plan argument that avoids assuming a primal optimizer exists.

Difficulty

The heuristic derivation on pp. 9–10 constructs an optimal transport plan that moves each $x$ with $c(x,A) \le 1/\lambda^*$ to a nearest point of $A$ and leaves the others in place. It needs a nearest point to exist and to be selectable measurably, which fails for general closed $A$ in a non-locally-compact space, and it needs a primal optimizer, which need not exist. Theorem 3 assumes neither, so the construction is not a proof. A second point is the boundary level $c(x,A) = 1/\lambda^*$: when $\mu$ charges it, as for atomic baselines, the identity (15) can fail (for $\mu$ a point mass at distance $1$ from $A$ and $\delta < 1$, the worst case is $\delta$, not $1$), and the hypothesis $\underline c = \overline c$ is exactly what excludes this. Measurability is a second obstacle: $x \mapsto c(x,A)$ is an infimum of a lower semicontinuous function over $A$ and in general only universally measurable, so integrals of it are taken against the completion of $\mu$.

Formalization scope

All objects live in the namespace ModelRiskOT.WorstProb. $S$ carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]; $\mu$ is a Measure S with IsProbabilityMeasure; the cost is a real-valued c : S → S → ℝ with (A1) bundled as a structure (nonnegativity, lower semicontinuity on $S \times S$, and $c(x,y) = 0 \iff x = y$). Committed conventions:

• Values in $[0,\infty]$. $d_c$, $I$, the objective of (13), $\underline c$ and $\overline c$ are ℝ≥0∞; integrals are lower Lebesgue integrals and the positive part $(\cdot)^+$ is ENNReal.ofReal. For the universally measurable functions and sets that occur, lower integrals and outer measures agree with the completion of $\mu$, which is the paper's reading (p. 4). No Bochner integral is used.
• The threshold $1/\lambda^*$ is written in multiplied form: $c(x,A) \le 1/\lambda^*$ is $\lambda^* c(x,A) \le 1$, and likewise for the strict inequality and for the sets $C_n$. For $\lambda^* > 0$ this is the printed condition; at $\lambda^* = 0$ it is the whole space, the paper's convention $1/0 = \infty$.
• $d_c$ fixes both marginals; $\Phi_{\mu,\delta}$ fixes only the first.
• $c(x,A)$ is a real infimum over the subtype $A$; every statement assumes $A$ nonempty.
• "$\lambda^*$ attains the infimum in (13)" is $\lambda^* \ge 0$ and $g(\lambda^*) \le g(\lambda)$ for all $\lambda \ge 0$.
• Inequalities $X \ge I - t$ are written $I \le X + t$ in $[0,\infty]$; sequences "$n > 1$" are indexed by $n \in \mathbb N$ with $1 < n$.

A formalization in which the transport ball fixes only the first marginal would contain every probability measure and give $I = 1$ for every nonempty $A$; the definitions here fix both marginals of the couplings in $d_c$, and the hypothesis $\underline c = \overline c$ is kept as stated rather than replaced by continuity of $u \mapsto \int_{\{c(x,A) \le u\}} c(x,A)\,d\mu$.

A complete development needs the existence of optimal couplings for lower semicontinuous costs (tightness and Prokhorov's theorem, available in Mathlib), the strong duality of the paper's Theorem 1 specialized to indicators (milestone 3; a separate mission in this series formalizes Theorem 1 in general), and universal measurability of $c(\cdot,A)$ through projections of Borel sets. The transport-cost definitions and the coupling reformulation are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs that derive (13) from the general strong duality once that is published.

Selected references

• J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, arXiv:1604.01446v2, 2017; Mathematics of Operations Research 44(2):565–600, 2019. https://arxiv.org/abs/1604.01446, https://doi.org/10.1287/moor.2018.0936
• C. Villani, Optimal Transport: Old and New, Grundlehren der mathematischen Wissenschaften 338, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
• R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, arXiv:1604.02199, 2016. https://arxiv.org/abs/1604.02199
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171:115–166, 2018. https://doi.org/10.1007/s10107-017-1172-1
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (universal measurability, Ch. 7).