Convex Optimization

Discrete Geometry Linear Optimization Operations Research+1·Captain: mikedeng1

On Polyhedral Approximations of the Second-Order Cone II: A Lower Bound on the Size of Polyhedral ApproximationsResearch Paper

Motivation

A conic quadratic program minimizes a linear objective subject to constraints of the form $\|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell$ . Interior-point methods solve such programs in polynomial time, but around 2000 the available solvers handled far smaller instances than linear programming codes did. Ben-Tal and Nemirovski (Math. Oper. Res. 26(2), 2001) asked whether a conic quadratic program can be replaced by a linear program of comparable size, and answered it by approximating each second-order cone by a projection of a polyhedral cone. Their Theorem 1.1 builds such an approximation with accuracy $\varepsilon$ using $O(k\ln(2/\varepsilon))$ variables and inequalities. The present mission is their Proposition 3.1: this size is optimal in order, because every polyhedral $\varepsilon$ -approximation needs $\Omega(k\ln(1/\varepsilon))$ inequalities.

The question of how many linear inequalities are needed to represent or approximate a convex set as a projection (its extension complexity) has since become a subject of its own, and the lower bound of Proposition 3.1 is one of its early explicit instances for a non-polyhedral cone.

Setting

For $y\in\mathbb R^k$ write $\|y\|_2=\sqrt{y_1^2+\dots+y_k^2}$ . The Lorentz cone is

L^k=\{(y,t)\in\mathbb R^k\times\mathbb R\mid t\ge\|y\|_2\}.

Let $\varepsilon>0$ . A polyhedral $\varepsilon$ -approximation of $L^k$ is a linear map $\Pi:\mathbb R^k\times\mathbb R\times\mathbb R^p\to\mathbb R^q$ such that

if $(y,t)\in L^k$ , then $\Pi(y,t,u)\ge0$ for some $u\in\mathbb R^p$ ;
if $\Pi(y,t,u)\ge0$ for some $u$ , then $\|y\|_2\le(1+\varepsilon)t$ .

Here $\ge0$ is componentwise, $p$ is the number of auxiliary variables and $q$ the number of homogeneous linear inequalities. Equivalently, the polyhedral cone $K=\{(y,t,u)\mid\Pi(y,t,u)\ge0\}$ projects onto a cone $\widehat L^k$ of the $(y,t)$ -space with $L^k\subseteq\widehat L^k\subseteq\{(y,t)\mid\|y\|_2\le(1+\varepsilon)t\}$ . The slice of $\widehat L^k$ at height one is $G=\{y\mid(y,1)\in\widehat L^k\}$ , and $B=\{y\mid\|y\|_2\le1\}$ denotes the closed unit ball.

Formalization targets

Goal: Proposition 3.1, Eq. (13)

\exists\,c>0\ \ \forall k\ge2,\ \forall\varepsilon\in(0,\tfrac12],\ \forall p,q,\ \forall\Pi\ \text{polyhedral }\varepsilon\text{-approximation of }L^k:\qquad q\ \ge\ c\,k\ln\tfrac1\varepsilon .

The constant is absolute, as in the paper, and no value is fixed; the goal asserts only the order of growth.

Milestones (claims of the proof, in order)

Reduction. For $\varepsilon>0$ one may replace $\Pi$ by an approximation with the same $q$ , at most $p$ auxiliary variables and the same projection, whose cone $K$ contains no line.
Extreme rays. A line-free cone $\{z\mid Az\ge0\}$ defined by $q$ inequalities is the conic hull of at most $2^q$ extreme rays.
Sandwich. $B\subseteq G\subseteq(1+\varepsilon)B$ .
Vertices. If $K$ has no line, $G$ is the convex hull of $N\le2^q$ points.
Covering. If $\operatorname{conv}\{y_1,\dots,y_N\}\supseteq B$ and all $\|y_i\|_2\le1+\varepsilon$ , the closed balls of radius $\sqrt{2\varepsilon(1+\varepsilon)}$ about the $y_i$ cover the sphere $\{\|y\|_2=1+\varepsilon\}$ .
Counting. For $k\ge2$ and $\varepsilon\le\tfrac12$ such a covering needs $N\ge\exp\{c\,k\ln(1/\varepsilon)\}$ balls.

Significance

The result. Proposition 3.1 shows that the construction of Theorem 1.1 is optimal up to an absolute factor in the number of inequalities: approximating a conic quadratic constraint in dimension $k$ to relative accuracy $\varepsilon$ by linear inequalities costs $\Theta(k\ln(1/\varepsilon))$ inequalities, no more and no less. It separates what lifting (auxiliary variables) buys, a logarithmic dependence on $1/\varepsilon$ , from what it cannot buy, a sub-linear dependence on $k$ or on $\ln(1/\varepsilon)$ . Without auxiliary variables a polytope approximating the ball needs $\varepsilon^{-\Omega(k)}$ facets; the proposition says the logarithm of that count is the true cost even when lifting is allowed.

Formalizing it. The result is proved in the paper, in about fifteen lines that appeal to "elementary geometry" and to an unstated covering estimate. No machine-checked proof is known to exist. The mission produces a checked proof of the lower bound together with reusable facts: the finiteness bound on extreme rays of a pointed polyhedral cone and a lower bound on the number of balls needed to cover a Euclidean sphere, which Mathlib does not contain in this form. A companion mission of this series formalizes the matching upper bound (Theorem 1.1).

Difficulty

The obvious argument counts vertices of $G$ : at most $2^q$ of them, and a polytope between $B$ and $(1+\varepsilon)B$ needs many vertices. The difficulty is in making "many" quantitative with the right exponent. A direct volume comparison of $G$ with $B$ gives nothing, since $G$ may have the volume of $(1+\varepsilon)B$ . The argument needs the transfer from "the convex hull of the points contains $B$ " to "the points are $\sqrt{2\varepsilon(1+\varepsilon)}$ -dense on the outer sphere", and then a lower bound on the size of a covering of a sphere by balls whose centres need not lie on the sphere, uniform down to $k=2$ and up to $\varepsilon=\tfrac12$ , where $\ln(1/\varepsilon)$ is only $\ln2$ and the radius $\sqrt{2\varepsilon(1+\varepsilon)}$ is comparable to the sphere's radius. A second, easily overlooked step is the passage to a line-free cone: $K$ itself may contain lines in the $u$ -directions, in which case it has no extreme rays at all.

Formalization scope

Vectors of $\mathbb R^k$ are Fin k → ℝ, and the Euclidean norm is written out as eucNorm y = √(∑ i, y i ^ 2); the norm Mathlib puts on Fin k → ℝ is the sup norm, under which $L^k$ is polyhedral and the goal is false. A polyhedral approximation is an $\mathbb R$ -linear map (Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ), and $p$ , $q$ are the dimensions of its types; with arbitrary (nonlinear) maps, $\Pi(y,t)=t-\|y\|_2$ would give $q=1$ , so linearity is what makes the statement non-trivial. "Extreme ray" means a ray $\{sr\mid s\ge0\}$ , $r\ne0$ , that is an extreme subset (Mathlib IsExtreme) of the cone, counted once per ray.

Corrections of the printed statement. Proposition 3.1 is printed for every positive integer $k$ . It is false for $k=1$ : $L^1=\{|y|\le t\}$ is polyhedral, and $\Pi(y,t)=(t-y,t+y)$ is a polyhedral $\varepsilon$ -approximation with $q=2$ for every $\varepsilon$ , so $q\ge c\ln(1/\varepsilon)$ fails for small $\varepsilon$ . The goal and the counting milestone are therefore stated for $k\ge2$ , which is the case the proof covers. The phrase "polyhedral $\alpha$ approximation" in the proof is read as $\varepsilon$ . The paper's $O(1)$ constants are existential and quantified before every variable they are uniform over; no numerical value is asserted.

A complete development needs the Minkowski–Weyl representation of pointed polyhedral cones by extreme rays, basic convex-hull and separation arguments in Euclidean space, and a lower bound for covering numbers of spheres (for instance by a cap-measure or volume argument). The extreme-ray and covering lemmas are independent of the Lorentz cone and are welcome as stand-alone contributions.

Selected references

A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM, 2001. https://doi.org/10.1137/1.9780898718829

10 thms2 active usersReviewed

Control Theory Linear algebra Numerical Analysis+2·Captain: mikedeng1

Robust Solutions to Least-Squares Problems with Uncertain Data IV: A Semidefinite Upper Bound on the Linear-Fractional Worst-Case Residual, Exact for Full PerturbationsResearch Paper

Motivation

Least-squares fitting is a standard tool in estimation, identification and data analysis, and its data $A$ , $b$ are rarely known exactly. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to choose $x$ to minimize the worst-case residual over a set of admissible data perturbations. Earlier missions of this series treat unstructured perturbations of $[A\ b]$ and perturbations affine in a parameter vector. §5 of the paper covers a more general model, taken from robust identification (Doyle et al.): the perturbed data depend on an uncertain matrix $\Delta$ through a linear-fractional transformation. This form covers rational dependence of the data on uncertain parameters, max-norm bounds on independent parameters, and data matrices with some columns known exactly (pp. 1046–1047).

In this generality, deciding whether the worst-case residual is finite is NP-complete, and computing it is NP-hard even when the dependence is affine (§5.3, Lemma 5.1). Theorem 5.2 gives the tractable replacement: a semidefinite program whose value bounds the worst-case residual from above, and equals it when the perturbation is unstructured. The main tool is a structured form of the S-procedure. Robust control uses the same tool, with the scalings $S$ and $G$ below, to bound the real structured singular value (Fan, Tits and Doyle, 1991).

Setting

Vectors carry the Euclidean norm $\|v\|$ . For a matrix $X$ , $\|X\|$ is its largest singular value (operator norm between Euclidean spaces). Let $\mathcal D$ be a linear subspace of $\mathbb R^{N\times N}$ (the perturbation structure), and fix $A \in \mathbb R^{n\times m}$ , $b \in \mathbb R^n$ , $L \in \mathbb R^{n\times N}$ , $R_A \in \mathbb R^{N\times m}$ , $R_b \in \mathbb R^N$ , $D \in \mathbb R^{N\times N}$ . For $\Delta \in \mathcal D$ with $\det(I - D\Delta) \ne 0$ the perturbed data are

A(\Delta) = A + L\Delta(I - D\Delta)^{-1}R_A, \qquad b(\Delta) = b + L\Delta(I - D\Delta)^{-1}R_b .

With the normalization $\rho = 1$ (the paper's, with no loss of generality), the worst-case residual of $x \in \mathbb R^m$ is

r_{\mathcal D}(A,b,x) = \max_{\Delta \in \mathcal D,\ \|\Delta\| \le 1} \|A(\Delta)x - b(\Delta)\|

if $\det(I - D\Delta) \ne 0$ for every such $\Delta$ , and $+\infty$ otherwise (35). The commutant scalings are $\mathcal S = \{S = S^T : S\Delta = \Delta S\ \forall \Delta \in \mathcal D\}$ and $\mathcal G = \{G = -G^T : G\Delta = \Delta G\ \forall \Delta \in \mathcal D\}$ (37). The SDP constraint is

\mathcal F(\lambda,S,G,x) = \begin{bmatrix} \Theta & \begin{matrix} Ax - b \\ R_Ax - R_b\end{matrix} \\ \begin{matrix}(Ax-b)^T & (R_Ax - R_b)^T\end{matrix} & \lambda\end{bmatrix} \succ 0, \quad \Theta = \begin{bmatrix} \lambda I - LSL^T & -LSD^T + LG \\ -DSL^T + G^TL^T & S + DG - GD^T - DSD^T\end{bmatrix}. \qquad (38),(39)

Formalization targets

Goal: Theorem 5.2 (corrected)

For all $x$ and $\lambda$ :

\text{(a)}\quad S \in \mathcal S,\ G \in \mathcal G,\ S \succ 0,\ G\Delta \text{ skew } \forall \Delta \in \mathcal D,\ \mathcal F(\lambda,S,G,x) \succ 0 \ \Longrightarrow\ \lambda > r_{\mathcal D}(A,b,x);

\text{(b)}\quad \mathcal D = \mathbb R^{N\times N},\ \lambda > r_{\mathcal D}(A,b,x) \ \Longrightarrow\ \exists s > 0:\ \mathcal F(\lambda, sI, 0, x) \succ 0 .

Part (a) says the value of the SDP $\inf\{\lambda : (\lambda, S, G) \text{ feasible}\}$ (40) is an upper bound on $r_{\mathcal D}$ . Part (b) says this upper bound is exact for full perturbations, including the case $r_{\mathcal D} = \infty$ , where (40) is infeasible.

Milestones

Lemma 2.2, both directions: the full-block S-procedure. $\det(I - T_4\Delta) \ne 0$ and $T(\Delta) \succeq 0$ for all $\|\Delta\| \le 1$ if and only if $\|T_4\| < 1$ and a one-scalar LMI (10) holds (the "only if" under $T_2 \ne 0$ or $T_3 = 0$ ).
Lemma 2.3: sufficiency of the scaled LMI for a structured $\mathcal D$ , and its strict necessity for $\mathcal D = \mathbb R^{N\times N}$ .
§5.4, p. 1047: $\lambda > r_{\mathcal D}(A,b,x)$ if and only if a linear-fractional matrix function of $\Delta$ is positive definite on the structured unit ball.
§5.4, (38)–(39): the certificate (a) in the paper's own words.

Significance

The worst-case residual under linear-fractional uncertainty cannot be computed efficiently unless P = NP. Theorem 5.2 gives an SDP-computable upper bound with an explicit certificate $(S, G)$ . Since $x$ enters (38) linearly, the same constraint can also be optimized over $x$ (Theorem 5.3, not part of this mission). For $\mathcal D = \mathbb R^{N\times N}$ the bound is exact, which covers the model $[A(\Delta)\ b(\Delta)] = [A\ b] + L\Delta[R_A\ R_b]$ and, as a special case, the unstructured problem of §3.

The results are proved in the paper (the proof of Theorem 5.2 is only indicated, through Appendix C). No machine-checked version of these statements, of Lemma 2.2 or of the structured S-procedure with commutant scalings is known. The formalization also fixes the statements. As printed, Lemma 2.2's "only if", Lemma 2.3 and the upper bound of Theorem 5.2 are each false in a boundary or structural case (see Formalization scope). The corrected forms stated here are the ones the paper's proofs support.

Difficulty

Part (a) reduces to robust positivity of a linear-fractional matrix function, and the difficulty is the inverse $(I - D\Delta)^{-1}$ . The certificate is one LMI in which $\Delta$ does not appear, while the conclusion is about a rational function of $\Delta$ over a whole structured ball. The certificate also has to guarantee that $I - D\Delta$ is invertible everywhere on that ball, and not only that the residual is small where it is defined. Evaluating $\mathcal F$ at a single point does not show this. Part (b) needs a lossless S-procedure in its strict form. The standard (non-strict) S-lemma gives only $\succeq$ , and the gap between strict and non-strict inequalities is exactly where the printed statements fail. The degenerate case $T_2 = 0$ is not covered by the S-lemma's regularity condition and has to be handled separately.

Formalization scope

Dimensions are Fin n, Fin m, Fin N; $\mathcal D$ is a Submodule ℝ (Matrix (Fin N) (Fin N) ℝ), with $\mathcal D = \mathbb R^{N\times N}$ as ⊤. The Euclidean norm is written out, because ‖·‖ on Fin n → ℝ is the sup norm. $\|\Delta\|$ is the operator norm of Matrix.toEuclideanLin Δ, the largest singular value.
$\lambda > r_{\mathcal D}(A,b,x)$ is the predicate ResidualBelow: every $\Delta \in \mathcal D$ with $\|\Delta\| \le 1$ has $\det(I - D\Delta) \ne 0$ and residual $< \lambda$ . It is false for every $\lambda$ when $r_{\mathcal D} = \infty$ . No real-valued supremum is used, so the $\infty$ branch of (35) cannot turn into a default $0$ . Matrix inverses are Mathlib's Matrix.inv, and every use carries the determinant condition.
$\rho = 1$ throughout, as in the paper; general $\rho$ follows by scaling $\Delta$ .
Corrections of the printed statements. (i) (40) must require $S \succ 0$ . Without it, $N = n = m = 1$ , $D = 2$ , $L = 1$ , $A = b = R_A = R_b = 0$ , $x = 0$ , $S = -1$ , $G = 0$ satisfy (38) for every $\lambda > 1/3$ , while $r_{\mathcal D} = \infty$ . (ii) $G$ must make $G\Delta$ skew-symmetric for every $\Delta \in \mathcal D$ , which is the identity $p^TGq = 0$ used in the proof of Lemma 2.3. For $\mathcal D = \operatorname{span}\{I, J\}$ , $J = \begin{bmatrix}0&1\\-1&0\end{bmatrix}$ , the printed bound certifies $\lambda = 3/2$ for an instance with worst-case residual $2$ . The added condition holds automatically when every element of $\mathcal D$ is symmetric (e.g. the diagonal structures (36)) and when $G = 0$ (e.g. $\mathcal D = \mathbb R^{N\times N}$ ). (iii) Lemma 2.2's "only if" is stated under $T_2 \ne 0$ or $T_3 = 0$ . (iv) Lemma 2.3's necessity is stated in strict form, and its sufficiency concludes $T(\Delta) \succ 0$ .
Not stated: "If $\Theta > 0$ at the optimum, the upper bound is also exact". The infimum over the strict LMI (38) is not attained, and the paper does not say which limit is meant. Theorem 5.3, Lemma 2.4 and Lemma 5.1 are also not stated.
Trivializing encodings ruled out: the goal is not a statement about the value of an infimum (which a junk value could satisfy), and the added hypotheses are satisfiable (for instance $S = sI$ , $G = 0$ for full $\mathcal D$ , which part (b) produces).
Infrastructure needed: the Schur complement for block matrices (in Mathlib), a lossless S-lemma for two homogeneous quadratic forms in strict and non-strict form (the platform has ConvexOptimization.s_procedure, in a different sign convention), square roots of positive definite matrices that commute with $\mathcal D$ , and compactness of the structured unit ball. The S-procedure lemmas are reusable in robust control and trust-region analysis. Proofs of the milestones in any order are welcome.

Selected references

L. El Ghaoui and H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
S. Boyd, L. El Ghaoui, E. Feron and V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
M. K. H. Fan, A. L. Tits and J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36(1):25–38, 1991. https://doi.org/10.1109/9.62265
I. Pólik and T. Terlaky, A survey of the S-lemma, SIAM Review 49(3):371–418, 2007. https://doi.org/10.1137/S003614450444614X

8 thms2 active usersReviewed

Linear algebra Linear Optimization Operations Research+1·Captain: mikedeng1

Path-Finding Methods for Linear Programming II: Properties of the Regularized D-Optimal-Design Weight FunctionResearch Paper

Motivation

Interior point methods for a linear program $\min\{c^\top x : Ax\ge b\}$ with $A\in\mathbb R^{m\times n}$ follow the central path of the logarithmic barrier $-\sum_i\log s_i$ , where $s=Ax-b$ is the slack vector. Renegar's path-following analysis (1988) gives $O(\sqrt m\,L)$ iterations, and for decades this was the best bound for methods whose iterations cost a linear system solve. Vaidya's volumetric barrier $-\log\det(A^\top S^{-2}A)$ and the hybrid volumetric barriers of Vaidya and of Anstreicher (references [45] and [2] of the paper) reached $O((m\,\mathrm{rank}(A))^{1/4}L)$ iterations at the price of more expensive linear algebra. Nesterov and Nemirovski showed that a universal barrier gives $O(\sqrt n\,L)$ iterations, but that barrier cannot be evaluated efficiently.

Lee and Sidford (FOCS 2014; full version arXiv:1312.6677) obtained $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ iterations, each costing $\tilde O(1)$ linear system solves, by following a weighted central path whose weights are recomputed from the slacks. The weights come from a weight function $g$ , defined as the minimizer of a regularized D-optimal-design problem. This mission is about that weight function and the theorem (Theorem 1 of the paper) certifying its properties. The companion mission, Path-Finding Methods for Linear Programming I, formalizes the path-following framework (Theorem 5 of §IV.C) that consumes these properties.

Setting

Fix $A\in\mathbb R^{m\times n}$ with full column rank, $\mathrm{rank}(A)=n$ , and $1\le n<m$ . For vectors $s,w\in\mathbb R^m_{>0}$ write $S=\mathrm{diag}(s)$ , $W=\mathrm{diag}(w)$ , $W^\alpha=\mathrm{diag}(w_i^\alpha)$ , and $A_s=S^{-1}A$ . For a matrix $M$ let $\|v\|_M=\sqrt{v^\top Mv}$ .

Projection matrix and slack sensitivity (Definition 2, p. 428). The projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A\,(A^\top S^{-1}WS^{-1}A)^{-1}A^\top S^{-1}W^{1/2}$ , and the slack sensitivity is

\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\mathbb 1_i\big\|_{P_{S^{-1}A}(w)} .

Weight function (Definition 4, p. 428). A map $g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ is a weight function with constants $c_1,c_\gamma,c_r$ if it is differentiable and, for every $s>0$ , with $G(s)=\mathrm{diag}(g(s))$ , $G'(s)$ the Jacobian of $g$ at $s$ , and $\|y\|_{G(s)}=\sqrt{\sum_ig_i(s)y_i^2}$ :

Size: $\|g(s)\|_1\le c_1$ ;
Slack sensitivity: $c_\gamma\ge1$ and $\gamma(s,g(s))\le c_\gamma$ ;
Step consistency: $c_r\ge1$ and for all $r\ge c_r$ , $y\in\mathbb R^m$ : $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ and $\|y+r^{-1}G^{-1}G'Sy\|_\infty\le\|y\|_\infty+c_r\|y\|_{G(s)}$ ;
Uniformity: $\|g(s)\|_\infty\le2$ .

The regularized objective (6), p. 429. For $\alpha,\beta\in\mathbb R$ ,

\hat f(s,w)=\mathbb 1^\top w-\frac1\alpha\log\det\big(A_s^\top W^\alpha A_s\big)-\beta\sum_{i\in[m]}\log w_i ,\qquad g(s)=\arg\min_{w\in\mathbb R^m_{>0}}\hat f(s,w).

At $\alpha=1,\beta=0$ this is the D-optimal design problem, dual to computing the John ellipsoid of the polytope $\{y:|[A(y-x)]_i|\le s_i\}$ (§V.B).

Formalization targets

Goal: Theorem 1 (Properties of Weight Function), §V.A, p. 429

With

\alpha=1-\Big(\log_2\frac{2m}{\mathrm{rank}(A)}\Big)^{-1},\qquad \beta=\frac{\mathrm{rank}(A)}{2m},

the objective $\hat f(s,\cdot)$ has a unique minimizer over $\mathbb R^m_{>0}$ for every $s>0$ , and the resulting $g$ is a weight function with

c_1(g)=2\,\mathrm{rank}(A),\qquad c_\gamma(g)=2,\qquad c_r(g)=2\log_2\frac{2m}{\mathrm{rank}(A)} .

Milestones: the three bullets of Theorem 1

Size: every minimizer $w$ of $\hat f(s,\cdot)$ satisfies $\|w\|_1\le2\,\mathrm{rank}(A)$ .
Slack sensitivity: every minimizer $w$ satisfies $\gamma(s,w)\le2$ .
Step consistency: any map $g$ selecting a minimizer at every $s>0$ is differentiable on $\mathbb R^m_{>0}$ and satisfies the two step-consistency inequalities for every $r\ge2\log_2\frac{2m}{\mathrm{rank}(A)}$ .

A supporting (non-milestone) item states the existence and uniqueness of the minimizer on its own.

Significance

The result. Theorem 1 is the input that turns the weighted path-following framework into an $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ -iteration method: the framework needs $O(c_\gamma^{-1}c_r^{-3}c_1^{-1/2})$ -sized steps in $t$ (p. 428), and Theorem 1 makes that $\tilde\Omega(1/\sqrt{\mathrm{rank}(A)})$ . The step consistency bound is what allows the weights to be recomputed after each Newton step without losing centrality. The same construction underlies later work on Lewis-weight barriers and on fast approximate John ellipsoids and maximum flow (§VIII of the paper).

Formalizing it. The theorem is proved in the full version of the paper (arXiv:1312.6677); the FOCS extended abstract contains no proofs. No part of it has a machine-checked proof. A complete formalization would give a verified account of leverage-score calculus (sums of leverage scores equal the rank; derivatives of projection matrices), of the convexity of $w\mapsto-\log\det(A^\top W^\alpha A)$ for $\alpha\in(0,1)$ , and of differentiability of an argmin via the implicit function theorem, none of which is currently packaged in Mathlib in this form.

Difficulty

Size and slack sensitivity are statements about the minimizer, which is only characterized implicitly; they require precise matrix calculus for $\log\det(A_s^\top W^\alpha A_s)$ and a comparison between the matrices $A^\top WA$ (which defines $\gamma$ ) and $A^\top W^\alpha A$ (which defines $g$ ). The specific values of $\alpha$ and $\beta$ matter here: the unregularized choice $\alpha=1$ , $\beta=0$ makes the problem degenerate (p. 429).

The hard part is step consistency. The Jacobian $G'$ of an argmin is available only implicitly, as the solution of a linear system obtained by differentiating the optimality condition. A bound on $\|G'\|$ that depends on $m$ is easy to get and useless: the theorem needs the operator norm of $I+r^{-1}G^{-1}G'S$ in the $G(s)$ -norm to be at most $1$ as soon as $r$ exceeds $2\log_2(2m/\mathrm{rank}(A))$ , and an $\ell_\infty$ bound with only an additive $c_r\|y\|_{G(s)}$ loss.

Existence and differentiability of the minimizer are conclusions, not hypotheses. The minimization is over an open orthant on which the objective is not obviously coercive or strictly convex for $\alpha<1$ , and differentiability of $g$ requires the Hessian of $\hat f$ at the minimizer to be invertible.

Formalization scope

Vectors are Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; inverses are Matrix.inv, $\log\det$ is Real.log (Matrix.det …), $w_i^\alpha$ is Real.rpow, $\log_2$ is Real.logb 2, the Jacobian is fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm on Fin m → ℝ.

Conventions and pinned hypotheses:

Full column rank A.rank = n is assumed in every theorem. The paper never states it, but without it $A_s^\top W^\alpha A_s$ is singular and every formula is undefined (in Lean, Matrix.inv and Real.log would return junk $0$ ).
$1\le n<m$ . $\beta=\mathrm{rank}(A)/(2m)$ and $\log_2(2m/\mathrm{rank}(A))$ need $\mathrm{rank}(A)\ge1$ ; at $m=\mathrm{rank}(A)$ the page's $\alpha$ is $0$ and $1/\alpha$ in (6) is undefined.
Reading of $\alpha$ : the exponent $-1$ is the reciprocal of $\log_2\frac{2m}{\mathrm{rank}(A)}$ , giving $\alpha\in(0,1)$ .
Size is an upper bound $\|g(s)\|_1\le c_1$ (the paper's weight function has $\|g(s)\|_1=\tfrac32\mathrm{rank}(A)$ , while Theorem 1 reports $c_1=2\,\mathrm{rank}(A)$ ).
The first step-consistency bullet (an operator-norm bound) is stated for every vector $y$ .
$g$ is any map $\mathbb R^m\to\mathbb R^m$ whose value at each positive $s$ minimizes $\hat f(s,\cdot)$ over $\mathbb R^m_{>0}$ . Only its values on the open orthant matter. The goal also asserts that such minimizers exist and are unique, so it is not vacuous.

Ruling out trivializations: the goal does not assume $g$ to be a weight function or to be differentiable, and it does not replace $g$ by an arbitrary weight function; differentiability is a conclusion (a predicate using fderiv without it would make step consistency hold vacuously wherever $g$ fails to be differentiable).

Useful infrastructure, reusable beyond this mission: leverage scores and their sum; derivatives of $w\mapsto\log\det(A^\top WA)$ and of projection matrices; convexity of $-\log\det(A^\top W^\alpha A)$ in $w$ (related to the published ConvexOptimization.log_det_concaveOn); differentiability of the argmin of a strictly convex smooth function. Contributions of these as separate theorems are welcome, as is a proof of any single bullet of Theorem 1.

Selected references

Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv, 2013. https://arxiv.org/abs/1312.6677
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40 (1988). https://doi.org/10.1007/BF01580724

7 thms2 active usersReviewed

Machine Learning Probability Random Matrix Theory+1·Captain: mikedeng1

The Power of Convex Relaxation: Near-Optimal Matrix Completion I: Exact Nuclear-Norm Recovery with Quadratic Dependence on the RankResearch Paper

Motivation

Matrix completion asks to recover a low-rank matrix from a small random subset of its entries. It models collaborative filtering (a ratings matrix with most entries missing), sensor-network localization from partial distance matrices, and system identification. The natural estimator, the matrix of least rank that agrees with the observations, is NP-hard to compute in general. Candès and Recht (Found. Comput. Math. 2009) proposed to replace the rank by the nuclear norm (the sum of the singular values), its convex envelope, and proved that this convex program recovers the matrix exactly from $O(n^{6/5} r \log n)$ random entries under incoherence assumptions.

Candès and Tao (IEEE Trans. Inf. Theory 2010) sharpened the sample size to within logarithmic factors of the information-theoretic minimum $n r\log n$ . This mission formalizes their first result, Theorem 1.1, whose proof is a direct moment computation, together with the lemmas on which that proof rests.

Timeline:

2009, Candès–Recht: exact recovery from $m \gtrsim \mu_0 n^{6/5} r \log n$ entries.
2010, Candès–Tao (this paper): $m \gtrsim \mu^4 n r^2 (\log n)^2$ (Theorem 1.1, general-rank form) and $m \gtrsim \mu^2 n r \log^6 n$ (Theorem 1.2), plus a lower bound of order $n r \log n$ for every method (Theorem 1.7).
2011, Gross (IEEE Trans. Inf. Theory) and Recht (JMLR): $m \gtrsim \mu_0 n r \log^2 n$ by the "golfing scheme", with a different proof.

Setting

Let $M \in \mathbb R^{n\times n}$ have rank $r$ and singular value decomposition $M = \sum_{k=1}^r \sigma_k u_k v_k^*$ with $\sigma_k > 0$ and orthonormal $u_k$ , $v_k$ . Write $P_U = \sum_k u_k u_k^*$ , $P_V = \sum_k v_k v_k^*$ and $E = \sum_k u_k v_k^*$ . The matrix obeys the strong incoherence property with parameter $\mu > 0$ if, for all indices $a, a', b, b'$ ,

\Bigl|\langle e_a, P_U e_{a'}\rangle - \tfrac{r}{n}1_{a=a'}\Bigr| \le \mu\tfrac{\sqrt r}{n},\qquad \Bigl|\langle e_b, P_V e_{b'}\rangle - \tfrac{r}{n}1_{b=b'}\Bigr| \le \mu\tfrac{\sqrt r}{n},\qquad |E_{ab}| \le \mu\tfrac{\sqrt r}{n}.

For a set $\Omega \subset [n]\times[n]$ of observed positions, the nuclear-norm program is

\text{minimize } \|X\|_* \quad \text{subject to } X_{ab} = M_{ab}\ \ ((a,b)\in\Omega). \qquad \text{(I.3)}

In the uniform model $\Omega$ is a uniformly random $m$ -subset of $[n]\times[n]$ ; in the Bernoulli model each entry is included independently with probability $p = m/n^2$ .

The proof works with the tangent space $T$ at $M$ and its projection $\mathcal P_T(X) = P_UX + XP_V - P_UXP_V$ , the sampling projection $\mathcal P_\Omega$ , and the centered operators $\mathcal Q_\Omega = p^{-1}\mathcal P_\Omega - \mathcal I$ and $\mathcal Q_T = \mathcal P_T - \rho'\mathcal I$ , where $\rho = r/n$ and $\rho' = 2\rho - \rho^2$ . The candidate certificate $Y$ of (III.10) is the matrix of least Frobenius norm with $\mathcal P_\Omega(Y) = Y$ and $\mathcal P_T(Y) = E$ .

Formalization targets

Goal: Theorem 1.1, general-rank form (I.11)

There is an absolute constant $C$ such that, for every strongly incoherent $M$ of rank $r$ and every $m \le n^2$ ,

m \ge C\mu^4 n r^2(\log n)^2 \implies \Pr_{\text{uniform}}\bigl[M \text{ is the unique solution of (I.3)}\bigr] \ge 1 - n^{-3}.

Milestones

Lemma 3.1: a matrix $Y$ supported on $\Omega$ with $\mathcal P_T(Y) = E$ and $\|\mathcal P_{T^\perp}(Y)\| < 1$ , together with injectivity of $\mathcal P_\Omega$ on $T$ , certifies that $M$ is the unique solution (already proved on the platform).
Lemma 5.1 (exponent bound): $|J|+|K|-|Q|-|\Omega| \le -|Q'|+1$ for every admissible pair.
Lemma 5.2 (pair counting): at most $(Cj(k+1))^{2j(k+1)+q}$ strongly admissible pairs have $|Q'| = q$ .
Theorem 3.4 (moment bound I): with $A = (\mathcal Q_\Omega\mathcal Q_T)^k\mathcal Q_\Omega(E)$ and $r_\mu = \mu^2 r$ ,

\mathbb E\operatorname{trace}(A^*A)^j \le (Cj(k+1))^{2j(k+1)}\, n\,(n r_\mu^2/m)^{j(k+1)}.

Corollary 3.5: under the goal's sampling condition and the Bernoulli model, with probability at least $1-n^{-3}$ , $\mathcal P_\Omega$ is injective on $T$ and $\|\mathcal P_{T^\perp}(Y)\| \le 1/2$ .

The Bernoulli-to-uniform transfer (at most doubling the failure probability) is already on the platform and is included as a supporting item.

Significance

Theorem 1.1 shows that a tractable convex program recovers every strongly incoherent matrix of bounded rank from $O(n(\log n)^2)$ random entries, while Theorem 1.7 of the same paper shows that no method can succeed with fewer than order $n\log n$ . The gap is a single logarithmic factor. The result also requires nothing of the singular values, only of the singular vectors.

The theorem is proved in the literature, and later work improved the rank dependence (Theorem 1.2 of the same paper, and the golfing-scheme results of Gross and Recht). As far as is known, none of these results has a machine-checked proof. The mission produces a formal version of the full moment-method argument. Its combinatorial core, the admissible-pair calculus of Sections IV–V, is a self-contained counting problem for closed paths in a grid and is reusable for other trace-moment bounds of random operators. The Candès–Recht mission on the platform already supplies the deterministic duality step (Lemma 3.1) and the model transfer.

Difficulty

The obvious route bounds the Neumann series $\sum_k \|(\mathcal Q_\Omega\mathcal P_T)^k\mathcal Q_\Omega(E)\|$ term by term with noncommutative Khintchine inequalities and decoupling. That is how the earlier $n^{6/5}$ bound was obtained, and it degrades as $k$ grows because the indicator variables in the higher terms are strongly coupled. The moment method replaces these tools by an exact expansion of $\mathbb E\operatorname{trace}(A^*A)^j$ as a sum over "spider" configurations of paths in $[n]\times[n]$ . The difficulty moves into combinatorics. Configurations have to be grouped by admissible pairs, the exponent of $n$ has to be matched against the powers of $1/p$ (Lemma 5.1), and the configurations have to be counted with enough precision that the sum over $q$ converges (Lemma 5.2). A naive count of pairs gives $(2j(k+1))^{4j(k+1)}$ , which is too large by a square.

Formalization scope

Square case. Theorem 1.1 is printed for $n_1\times n_2$ matrices, but the paper proves only the square case (Section I-H: "we shall work exclusively with square matrices"). Every statement is for Matrix (Fin n) (Fin n) ℝ.
General rank. The goal and Corollary 3.5 are stated in the general-rank form (I.11), $m \ge C\mu^4 n r^2(\log n)^2$ . The paper states this form explicitly on p. 2055, and the proof of Corollary 3.5 derives it as (III.26). For $r = O(1)$ it is the printed Theorem 1.1 and the printed Corollary 3.5.
Constants. Every constant ("numerical constant $C$ ", $c_0$ , and $O(M)^M := (CM)^M$ ) is an existential absolute constant quantified before $n$ , $r$ , $m$ , $M$ , $\mu$ , $j$ , $k$ and $q$ . A constant allowed to depend on $n$ or $M$ would make (I.11) unsatisfiable for large $C$ and the goal vacuous; that formalization is ruled out.
Standing assumptions. The paper assumes $n \ge C'$ and $m \ge 2nr$ (I.22) throughout. In the goal and in Corollary 3.5 they are absorbed by $C$ , since strong incoherence forces $\mu \ge 1$ . Theorem 3.4 carries $2nr \le m$ explicitly. Theorem 3.4 omits $r = O(1)$ and (I.10), since Section V uses only its own proviso $m \ge n r_\mu^2$ . Every statement also carries $m \le n^2$ , without which the uniform model is empty.
Probability. The uniform model is the platform's successProb (a ratio of finite counts). The Bernoulli model uses bernoulliEventProb and bernoulliExpectation with $p = m/n^2$ . The logarithm is natural, and the failure probability is written 1 / n^3.
Recovery. "Unique solution of (I.3)" is IsUniqueMinimizer: every other matrix that agrees with $M$ on $\Omega$ has strictly larger nuclear norm. Stating recovery conditionally on the existence of a certificate would reduce the goal to Lemma 3.1; the goal instead bounds the probability of recovery itself.
Admissible pairs. The index $i \in [j]$ is 0-based, the cyclic successor is finRotate, and the lexicographic order is compared through positions. Pair values are counted in Fin (2j(k+1)+1), which contains every admissible value, so the count is exact and finite.
New definitions. centeredTangentProjection ( $\mathcal Q_T$ ), momentMatrix ( $A$ ), and the admissible-pair calculus. Strong incoherence (A1–A2) is the shared definition CandesTao.Shared.StrongIncoherence, used by this mission and by the companion mission II. The $\mathcal Q_T$ definition is drafted independently in mission II.

Contributions are welcome on any milestone. Lemmas 5.1 and 5.2 are finite combinatorics and need no analysis. Theorem 3.4 additionally needs the expansion (IV.4) of the trace moment and the moment bounds for centered Bernoulli variables of Section IV-C. Corollary 3.5 also uses Theorem 3.2 (Rudelson selection estimate) and Lemma 3.3 (replacing $\mathcal P_T$ by $\mathcal Q_T$ ), which are milestones of the companion mission The Power of Convex Relaxation: Near-Optimal Matrix Completion II.

Selected references

E. J. Candès and T. Tao, The Power of Convex Relaxation: Near-Optimal Matrix Completion, IEEE Trans. Inf. Theory 56(5):2053–2080, 2010. https://doi.org/10.1109/TIT.2010.2044061
E. J. Candès and B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9(6):717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
D. Gross, Recovering Low-Rank Matrices From Few Coefficients in Any Basis, IEEE Trans. Inf. Theory 57(3):1548–1566, 2011. https://doi.org/10.1109/TIT.2011.2104999
B. Recht, A Simpler Approach to Matrix Completion, J. Mach. Learn. Res. 12:3413–3430, 2011. https://jmlr.org/papers/v12/recht11a.html

14 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Robust Solutions of Optimization Problems Affected by Uncertain Probabilities II: A Self-Concordant Barrier for the Perspective ConstraintResearch Paper

Motivation

Robust optimization protects a decision against every scenario in an uncertainty set. When the uncertain data are probabilities, a natural uncertainty set is a ball around a nominal distribution measured by a φ-divergence (Kullback–Leibler, Burg entropy, χ², Hellinger and others). Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) show that the robust counterpart of a linear constraint over such a set is a finite convex system, and then ask whether that system is computationally tractable: can an interior-point method solve it in polynomial time?

For the Burg and Kullback–Leibler divergences the reformulated constraints (Eqs. (29) and (32) of the paper) have the shape $\lambda f(s_i/\lambda)\le\dots$ , a perspective constraint. Polynomial-time solvability by interior-point methods follows once the constraint set carries a self-concordant barrier in the sense of Nesterov and Nemirovski (Interior-Point Polynomial Algorithms in Convex Programming, SIAM 1994). Theorem 2 of the paper supplies such a barrier for every perspective constraint whose generating function satisfies a one-dimensional differential inequality. The same question arises for perspective and relative-entropy cones in conic optimization generally, so the criterion is of interest beyond φ-divergences.

Setting

A function $\varphi:F\to\mathbb R$ on an open convex set $F\subseteq\mathbb R^n$ is $\kappa$ -self-concordant ( $\kappa\ge0$ ) if it is three times continuously differentiable on $F$ and for every $y\in F$ and every direction $h\in\mathbb R^n$

\bigl|\nabla^3\varphi(y)[h,h,h]\bigr|\le 2\kappa\,\bigl(h^{\mathsf T}\nabla^2\varphi(y)h\bigr)^{3/2},

where $\nabla^k\varphi(y)[h,\dots,h]$ is the $k$ -th differential of $\varphi$ at $y$ in direction $h$ (Definition 1, p. 350). In Lean this is PhiDivRobust.Barrier.IsSelfConcordant κ F φ.

Let $f$ be a real function on $(0,\infty)$ . Its perspective is $g(s,y)=y\,f(s/y)$ for $s,y>0$ (perspective f). The constraint set (34) is

\{(s,y,z):\ y f(s/y)\le z,\ s\ge0,\ y\ge0\},

and its logarithmic barrier (35) is

\varphi_B(s,y,z)=-\ln\bigl(z-yf(s/y)\bigr)-\ln s-\ln y

(logBarrier f), finite on the open set $F_f=\{(s,y,z): s>0,\ y>0,\ yf(s/y)<z\}$ (barrierDomain f). Directions are $h=(h_1,h_2)$ for $g$ , with $h_1$ along $s$ and $h_2$ along $y$ , and $h\in\mathbb R^3$ for $\varphi_B$ .

Formalization targets

Goal: Theorem 2 (p. 350)

If $f$ is convex on $(0,\infty)$ and, for some $\kappa>0$ ,

|f'''(s)|\le\kappa\,\frac{f''(s)}{s}\qquad(s>0),\tag{33}

then $\varphi_B$ is $\bigl(2+\tfrac{\sqrt2}{3}\kappa\bigr)$ -self-concordant on $F_f$ .

Milestones (the displayed steps of the proof)

Eq. (37): $\nabla^2 g(s,y)[h,h]=f''(s/y)\bigl(h_1^2/y-2sh_1h_2/y^2+s^2h_2^2/y^3\bigr)$ .
The third differential of $g$ in terms of $f''(s/y)$ and $f'''(s/y)$ .
Under (33), inequality (36) with $\beta=3+\kappa\sqrt2$ :

\bigl|\nabla^3 g(s,y)[h,h,h]\bigr|\le\beta\,h^{\mathsf T}\nabla^2 g(s,y)h\,\sqrt{h_1^2/s^2+h_2^2/y^2}.

Lemma A.2 of den Hertog (1994), as quoted in the proof: if (36) holds with $\beta\ge0$ , then $\varphi_B$ is $(1+\beta/3)$ -self-concordant on $F_f$ .

Milestones 3 and 4 give the goal, since $1+\tfrac13(3+\kappa\sqrt2)=2+\tfrac{\sqrt2}{3}\kappa$ . A further item records the paper's application: $f(s)=-\log s$ (the Burg case) satisfies (33) with $\kappa=2$ .

Significance

The result. Theorem 2 turns a two-line calculus check on a scalar function into a certificate of polynomial-time solvability for a three-dimensional convex constraint. The paper uses it to conclude that the robust counterparts for the Burg entropy and Kullback–Leibler uncertainty sets are tractable, and the criterion applies to any other convex $f$ satisfying (33); for example $f(s)=s\log s$ satisfies it with $\kappa=1$ , which covers the relative-entropy cone. The constant $2+\tfrac{\sqrt2}{3}\kappa$ enters the complexity bound of any path-following method through the barrier parameter.

Formalizing it. The theorem is proved in the paper, but the decisive step is delegated to Lemma A.2 of den Hertog's monograph, which in turn belongs to the compatibility theory of Nesterov and Nemirovski. As far as is known none of these statements has a machine-checked proof. The mission produces a checked version of the compatibility lemma for perspective constraints, which is reusable for any barrier of the form $-\ln(z-g)-\ln s-\ln y$ , together with explicit second- and third-differential formulas for perspectives in Mathlib's iteratedFDeriv language. The printed third-differential display contains a typo (see below); the formal statements fix it.

Difficulty

The differential identities (milestones 1 and 2) are routine but heavy: they require computing iterated Fréchet derivatives of a composition with a quotient in two variables and matching them with one-variable iterated derivatives of $f$ . The inequality (milestone 3) is elementary real-variable algebra once the differentials are available.

The central difficulty is den Hertog's lemma. The obvious approach, bounding the three terms of $\nabla^3\varphi_B$ separately against $(\nabla^2\varphi_B)^{3/2}$ , fails: the cross term $-3\,(\nabla\omega\cdot h)\,\nabla^2 g[h,h]/\omega^2$ with $\omega=z-g$ couples the first and second differentials, and bounding it separately loses the constant $1+\beta/3$ . A further practical difficulty is that $F_f$ is open and convex only because the perspective of a convex function is jointly convex and continuous, which must itself be established.

Formalization scope

Points are $(s,y,z)\in\mathbb R\times\mathbb R\times\mathbb R$ and directions for $g$ are in $\mathbb R\times\mathbb R$ . Differentials are iteratedFDeriv ℝ k applied to the constant tuple $(h,\dots,h)$ ; $f''$ and $f'''$ are iteratedDeriv 2 f and iteratedDeriv 3 f. The power $x^{3/2}$ is Real.rpow, which is $0$ for $x<0$ ; this makes the Lean definition of self-concordance no weaker than the paper's. Real.log and division have junk values outside $F_f$ , but $F_f$ is open, so no differential at a point of $F_f$ sees them.

Committed conventions and disclosed deviations:

" $f:\mathbb R^+\to\mathbb R$ " is read as $f$ convex on the open half-line $(0,\infty)$ ; the Burg case $f=-\log$ is undefined at $0$ , and $f$ is only evaluated at $s/y$ with $s,y>0$ .
$f$ is assumed $C^3$ on $(0,\infty)$ . The page does not say so, but (33) uses $f'''$ and Definition 1 requires the barrier to be $C^3$ .
The printed third-differential display ends in $s^3h_x^3/y^5$ ; the correct term is $s^3h_2^3/y^5$ , and the Lean statement uses it. The milestone text keeps the printed version.
Lemma A.2 is stated with $\beta\ge0$ added. The quoted text says "if there exists a $\beta$ ", which is false for $\beta<0$ : with $f\equiv0$ , (36) holds for every $\beta$ and $\beta=-3$ would give a $0$ -self-concordant $-\ln z-\ln s-\ln y$ . The goal uses $\beta=3+\kappa\sqrt2>0$ and is unaffected.

A trivializing formalization is excluded. The self-concordance predicate requires $C^3$ regularity and quantifies over all directions $h\in\mathbb R^3$ , the domain is exactly $F_f$ (not a subset such as $\emptyset$ ), and $\kappa>0$ is as printed. The constant of the conclusion is tied to the same $\kappa$ as in (33).

Useful infrastructure, reusable beyond this mission: iterated derivatives of perspectives, joint convexity of perspectives, and the calculus of self-concordance (sums, $-\ln$ of a concave function composed with an affine map). Proofs of the milestones independently of the goal are welcome, as are proofs of the Burg item's consequence and of the analogous statement for $f(s)=s\log s$ .

Selected references

A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
D. den Hertog, Interior Point Approach to Linear, Quadratic and Convex Programming: Algorithms and Complexity, Kluwer Academic Publishers, 1994. https://doi.org/10.1007/978-94-011-1134-8
Yu. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791

8 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Robust Solutions of Optimization Problems Affected by Uncertain Probabilities I: The Robust Counterpart of a Linear Constraint under φ-Divergence UncertaintyResearch Paper

Motivation

Many decision problems contain a constraint whose coefficients are an expectation under a probability vector that is not known exactly: an expected cost under uncertain scenario probabilities, an expected payoff of an asset under an estimated distribution, the expected demand in a newsvendor model. The probabilities are usually estimated from data, and a solution that is feasible for the estimate can be infeasible for the true distribution. Robust optimization protects against this by requiring the constraint to hold for every probability vector in an uncertainty region around the estimate.

A natural region is a ball in a φ-divergence, a family of statistical distances between probability vectors that contains the Kullback–Leibler divergence, the Burg entropy, the χ² distances, the Hellinger distance and the variation distance. Such balls arise as asymptotic confidence sets for the true distribution given observed frequencies (Pardo 2006), so the radius has a statistical meaning. Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen (Management Science 59(2), 2013) showed that the robust version of a linear constraint over such a ball is equivalent to a finite convex system involving the convex conjugate of φ. This reformulation is a standard tool in the later literature on distributionally robust optimization.

Setting

A φ-divergence function is a function $\phi:\mathbb R\to\mathbb R\cup\{+\infty\}$ that is convex on $[0,\infty)$ , finite on $(0,\infty)$ , and satisfies $\phi(1)=0$ ; the value $\phi(0)$ may be $+\infty$ . Examples are $\phi(t)=t\log t-t+1$ (Kullback–Leibler), $\phi(t)=-\log t+t-1$ (Burg), $\phi(t)=(t-1)^2$ (modified χ²) and $\phi(t)=|t-1|$ (variation). For $p,q\in\mathbb R^m$ with $q>0$ the φ-divergence is

I_\phi(p,q)=\sum_{i=1}^m q_i\,\phi\!\left(\frac{p_i}{q_i}\right),

and the conjugate of $\phi$ is $\phi^*(s)=\sup_{t\ge0}\{st-\phi(t)\}$ , a function with values in $\mathbb R\cup\{+\infty\}$ .

Fix $a\in\mathbb R^n$ , $B\in\mathbb R^{n\times m}$ with columns $b_i$ , $\beta\in\mathbb R$ , $C\in\mathbb R^{k\times m}$ with columns $c_i$ , $d\in\mathbb R^k$ , a nominal vector $q\in\mathbb R^m$ and a radius $\rho>0$ . The uncertainty region is

U=\{p\in\mathbb R^m\mid p\ge0,\ Cp\le d,\ I_\phi(p,q)\le\rho\},

where the linear constraints $Cp\le d$ can encode $e^\top p=1$ and any further information on $p$ . A decision $x\in\mathbb R^n$ satisfies the robust linear constraint if

(a+Bp)^\top x\le\beta\qquad\text{for all }p\in U. \tag{11}

Inequalities between vectors are componentwise throughout.

Formalization targets

Goal: Theorem 1

Assume $q>0$ and $q\in U$ . Then $x$ satisfies (11) if and only if there are $\eta\in\mathbb R^k$ and $\lambda\in\mathbb R$ with

a^\top x+d^\top\eta+\rho\lambda+\lambda\sum_{i}q_i\,\phi^*\!\left(\frac{b_i^\top x-c_i^\top\eta}{\lambda}\right)\le\beta,\qquad\eta\ge0,\ \lambda\ge0, \tag{13}

where $0\phi^*(s/0):=0$ for $s\le0$ and $0\phi^*(s/0):=+\infty$ for $s>0$ . The statement fixes no constants and no particular φ; it holds for the whole class.

Milestones

The proof in the paper has three displayed steps, which are the milestones. With the Lagrange function $L(p,\lambda,\eta)=(a+Bp)^\top x+\rho\lambda-\lambda I_\phi(p,q)+\eta^\top(d-Cp)$ and the dual objective $g(\lambda,\eta)=\sup_{p\ge0}L(p,\lambda,\eta)$ :

Closing identity. For $\lambda\ge0$ , $(\lambda\phi)^*(s)=\sup_{t\ge0}\{st-\lambda\phi(t)\}$ equals $\lambda\phi^*(s/\lambda)$ , with the convention above at $\lambda=0$ .
Eq. (15). For $q>0$ and $\lambda\ge0$ ,

g(\lambda,\eta)=a^\top x+d^\top\eta+\rho\lambda+\sum_{i=1}^m q_i(\lambda\phi)^*(b_i^\top x-c_i^\top\eta).

Duality. Under the hypotheses of Theorem 1, $x$ satisfies (11) if and only if $g(\lambda,\eta)\le\beta$ for some $\lambda\ge0$ , $\eta\ge0$ . This is split into the weak-duality direction and the strong-duality direction with attainment.

An additional item states Corollary 1, the specialization to $U=\{p\ge0,\ e^\top p=1,\ I_\phi(p,q)\le\rho\}$ , where the multiplier $\eta\in\mathbb R$ of the normalization is free in sign.

Significance

Theorem 1 turns a semi-infinite constraint, one inequality for each $p$ in a convex set, into a single convex inequality in $(x,\lambda,\eta)$ . The left side of (13) is jointly convex because $\lambda\phi^*(s/\lambda)$ is the perspective of a convex function. For the divergences of Table 4 of the paper the conjugate has a closed form, and the robust constraint becomes a linear, conic quadratic or self-concordant-barrier-representable constraint. The paper's applications (robust asset pricing, a robust newsvendor, and the tractability results of its §5) all start from this theorem, as do its Corollaries 2–5.

The theorem is proved in the paper; no machine-checked proof of it is known. Formalizing it adds a checked robust-counterpart theorem for φ-divergence regions, a reusable encoding of φ-divergences with extended values, and a strong-duality statement with attainment for convex programs whose constraint function takes the value $+\infty$ on the boundary of the orthant. It also records a correction: the paper states the theorem for $q\ge0$ , and that version is false (see Formalization scope).

Difficulty

The separation step (15) and the conjugate identity are elementary manipulations of suprema, but in extended arithmetic: $\phi$ may be $+\infty$ at $0$ , the conjugate may be $+\infty$ , and the case $\lambda=0$ follows its own convention. The central difficulty is the duality step. The worst-case problem is a convex program whose constraint $I_\phi(p,q)\le\rho$ is not a finite convex function on a closed set: for the Burg or χ² divergence it is $+\infty$ on the boundary of the orthant, and $U$ itself need not be closed. Textbook statements of Slater-type strong duality usually assume finite-valued convex functions on a closed domain, so they do not apply as stated. The statement also requires attainment of the dual minimum, not only the absence of a duality gap, and this is the part a naive limiting argument does not give.

Formalization scope

Conventions:

Vectors are Fin n → ℝ with the componentwise order; $B$ and $C$ are Matrix (Fin n) (Fin m) ℝ and Matrix (Fin k) (Fin m) ℝ; $b_i$ and $c_i$ are the columns fun j => B j i and fun j => C j i.
$\phi$ is ℝ → EReal, never $-\infty$ , finite on $(0,\infty)$ , with $\phi(1)=0$ and convexity on $[0,\infty)$ written out in EReal. $\phi(0)=+\infty$ is allowed, so the Burg, χ² and J divergences are covered.
$I_\phi(p,q)$ , $\phi^*$ , $(\lambda\phi)^*$ , $L$ , $g$ and the left side of (13) are EReal-valued. $\lambda\phi(t)$ is the EReal product, in which $0\cdot(+\infty)=0$ . The term $\lambda\phi^*(s/\lambda)$ is defined by an explicit case split at $\lambda=0$ , and $\lambda\sum_i q_i\phi^*(\cdot/\lambda)$ in (13) is read as $\sum_i q_i\,(\lambda\phi^*(\cdot/\lambda))$ with the convention applied term by term.
The paper's $\max_{p\ge0}$ in $g$ is a supremum; $\min_{\lambda,\eta\ge0}g\le\beta$ is stated in its attained form, $\exists\,\lambda\ge0,\eta\ge0$ with $g(\lambda,\eta)\le\beta$ .
$m$ and $k$ may be $0$ .

Corrected slip. The paper's standing assumption is $q\ge0$ . The third equality of (15) substitutes $p_i=q_it$ , which needs $q_i>0$ , and Theorem 1 is false for $q\ge0$ : with $m=k=2$ , $n=1$ , $\phi(t)=|t-1|$ , $q=(1,0)$ , both columns of $C$ equal to $(1,-1)^\top$ , $d=(1,-1)$ , $a=0$ , $B=(0\ \ 1)$ , $x=1$ , $\rho=1$ , $\beta=0$ , the vector $p=(1/2,1/2)$ lies in $U$ and violates (11), while $\eta=0$ , $\lambda=0$ satisfy (13). Every statement of the mission therefore assumes $q_i>0$ for all $i$ . The hypothesis $q\in U$ (the paper's "such that $q\in U$ ") and $\rho>0$ are kept.

Ruled-out trivializations: a conjugate taken as a supremum over all $t\in\mathbb R$ of a real-valued φ with junk values at $t<0$ is a different function; computing the $\lambda=0$ term as $0\cdot\phi^*(s/0)$ with Lean's $s/0=0$ makes it identically $0$ ; a real-valued, everywhere finite φ silently excludes the Burg, χ² and J divergences; dropping $q\in U$ or $\rho>0$ removes the Slater point and changes the theorem. The mission's definitions avoid all four.

Needed infrastructure: suprema of EReal-valued families over half-lines and orthants, the interchange of a supremum over a product with a finite sum, and a Lagrangian strong-duality theorem with attainment for a convex program with finitely many affine inequality constraints and one convex, possibly infinite-valued, inequality constraint with a Slater point in the interior of its domain. That duality theorem, and the φ-divergence definitions, are reusable beyond this mission, in particular for the paper's Corollaries 2–5 and for other distributionally robust formulations. Contributions of any of these pieces as separate theorems are welcome.

Selected references

A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2):341–357, 2013. https://doi.org/10.1287/mnsc.1120.1641
L. Pardo, Statistical Inference Based on Divergence Measures, Chapman & Hall/CRC, 2006. https://doi.org/10.1201/9781420034813
A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

12 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Introduction to Stochastic Programming VIII: Multistage Jensen Bounds and AggregationTextbook

Motivation

A multistage stochastic program's exact deterministic equivalent grows exponentially with the number of periods, even when each period's random data takes only a handful of values (Chapter 9's concern was the growth in the number of realizations; Chapter 10 adds growth in the number of periods). One remedy, generalizing Chapter 8's single-period Jensen bound, is to replace the exact per-period random data by a coarser, aggregated version — conditional expectations over a partition of the history space at each stage — and solve the resulting smaller deterministic equivalent instead. This is only useful if the aggregated problem's optimal value is provably a bound (here, a lower bound) on the exact problem's, and Birge & Louveaux's Chapter 10, §10.1, Theorem 1 is exactly the statement that makes this legitimate, together with a genuinely necessary extra condition the book states explicitly two paragraphs before the theorem: "if not [i.e. if the extra condition fails], then the conditional expectation form ... may not actually achieve a bound." This mission formalizes that theorem.

Setting

The book's exact multistage stochastic linear program (Eq. 1.1, p. 418) is

min c¹x¹ + E_Ω[c²x² + ⋯ + cᴴxᴴ]
s.t. W¹x¹ = h¹,  Tᵗ⁻¹xᵗ⁻¹ + Wᵗxᵗ = hᵗ (t=2,…,H, a.s.),  xᵗ ≥ 0 a.s., xᵗ nonanticipative (Σᵗ-measurable),

over the exact event space Ω = Ω₁ × ⋯ × Ω_H. Given a consistent nested partition of each Ωᵗ = Ω₁ × ⋯ × Ωₜ into finitely many blocks Sᵗ₁, …, Sᵗ_νₜ, and aggregated data (h̄ᵗᵢ, T̄ᵗᵢ) = E^{Sᵗᵢ}[(hᵗ,Tᵗ)] (the conditional expectation of the true random data over block i), the aggregated problem (Eq. 1.2, p. 419) replaces the exact recursion by a finite tree of blocks, one decision per block, linked to its parent block's decision. Both (1.1) and (1.2) are, structurally, the same kind of object — a finite-tree deterministic-equivalent recourse LP — differing only in which tree and which node data they use; this mission formalizes that shared shape once (Tree, Instance, Feasible, obj) and instantiates it twice.

Formalized as: a shared Tree H structure (a finite node type, per-node stage, anc, and a root), the same representation Chunk 06's Multistage.Tree uses for the exact scenario tree of its own (different) chapter, restated here rather than imported (a draft cannot import another chunk's draft). An Instance H n m T bundles a tree's node-varying LP data (c, W, Tmat, h, p); Feasible/obj give its feasible set and objective. The exact problem (1.1) is Instance H n m TFine for a fine/exact tree TFine; the aggregated problem (1.2) is Instance H n m TCoarse for a coarser tree TCoarse, connected to TFine by an aggregation map agg : TFine.Node → TCoarse.Node.

Formalization targets

Goal — Chapter 10, Theorem 1 (p. 419)

agg respects the tree structure (root, stage, ancestor);
W, c agree between the fine and coarse instances (up to agg);
coarse.h, coarse.Tmat are the p-weighted conditional expectations of fine.h, fine.Tmat over
  each aggregation fiber;
∀ coarse nodes i,i' at the same stage sharing a "current-period outcome",
  coarse.h i = coarse.h i' ∧ coarse.Tmat i = coarse.Tmat i'
  ⟹ zCoarse ≤ zFine

This is the mission's only formalization target: BRIEF.md records that no separately numbered lemma precedes Theorem 1's proof in this section to serve as an independent milestone (the proof is a direct LP-duality argument against the theorem's own hypotheses), and that Chapter 8's Theorem 1 — the two-period case this theorem generalizes — is a cross-chapter dependency belonging to Chunk 08's own mission, not a milestone here. milestones.yaml is accordingly empty; see STATUS.md for the explicit accounting of what else in this chapter was considered and left out (Theorem 3, the aggregation error bound of §10.2, an unrelated and substantially heavier result).

Significance

Theorem 1 is what licenses every aggregation-based approximation scheme the rest of the book's multistage material builds on: it says precisely when replacing a multistage recourse problem's random data by within-period conditional expectations preserves a valid lower bound, and precisely identifies the condition (aggregated nodes sharing a current-period outcome must carry identical aggregated data) whose failure breaks the bound — a condition the book states is not decorative ("if not, then the conditional expectation form ... may not actually achieve a bound," p. 418). Formalizing it gives Prove2Me a first structural result connecting Chapter 8's single-period Jensen bound (Chunk 08) to genuinely multistage approximation, using the same finite-scenario-tree deterministic-equivalent representation Chunk 06 uses for the exact nested Benders decomposition — the two missions' shared representation choice (documented in both STATUS.md files) means a future mission relating them formally (e.g. instantiating Chunk 06's exact tree as this mission's TFine) has a compatible object to work with, even though neither imports the other's draft.

Difficulty

The theorem's proof (p. 419-420) is a direct LP weak-duality argument: given an optimal dual solution to the aggregated problem, the book constructs a dual-feasible solution to the exact problem attaining the same value, using precisely the "common outcome ⟹ equal aggregated data" hypothesis to make the constructed dual solution well-defined across the exact tree's finer structure. This is a real argument, not a citation, but it is left as sorry: formalizing the proof would need the multistage LP duality machinery (the "multistage version of Theorem 3.13" the book's own proof invokes, itself left as Exercise 1) that no chunk of this series has built. The value of this mission is the faithful statement of the bound and its exact hypotheses.

Formalization scope

The book's own printed typo, resolved and documented. Theorem 1's hypothesis clause reads, as printed, "such that (ωt−1,ωt) ∈ Stj if and only if there exist some (ω̂t−1,ωt) ∈ Stj" — S^t_j appears on both sides of the "if and only if," where the sentence's own subject ("S^t_i and S^t_j that have a common outcome") requires the left side to range over S^t_i. Confirmed against a direct render of PDF page 436 (uv run --with pymupdf python), not assumed from OCR: the PDF's own typesetting has this repetition, not an artefact of text extraction. This formalization reads the corrected clause as "S^t_i and S^t_j project onto the same set of period-t outcomes" and states it via an explicit label type Θ and curOutcome : TCoarse.Node → Θ, since the aggregated tree alone does not carry a literal per-period outcome space to project onto (see Setting above — Tree records only history-node structure, not the underlying product space Ω = Ω₁ × ⋯ × Ω_H).
W, c shared exactly, not aggregated, matching the book's explicit assumption that the recourse matrix and per-stage cost are deterministic and identical across (1.1) and (1.2) ("Wt known and not random," "ct = ct," p. 418) — formalized as direct equality hypotheses (hW_agree, hc_agree) rather than folding W/c into the conditional-expectation machinery that h/Tmat go through.
zFine/zCoarse are hypothesis-characterized, not sInf-defined, avoiding the real infimum's junk value 0 on an unbounded-below or empty feasible set (reference/FAITHFULNESS_TRAPS.md trap 5) — neither tree-LP's feasible set is shown bounded or nonempty by the hypotheses alone.
The conditional-expectation defining equations are weighted, p·h/p·Tmat, not h/Tmat alone, matching the book's own E^{Sti}[·] = (h̄ti,T̄ti) read as "the fiber-sum of p·(h,T) equals p_i·(h̄ti,T̄ti)" — the standard definition of a conditional expectation against counting measure on a finite partition. Instance's own hp_pos (every node's probability is strictly positive) rules out the degenerate case a bare unweighted equation would need to guard separately (a coarse node of probability 0, which cannot occur, is what the read-back of this theorem flags as the one case where the weighted equation would not pin down h_coarse/ Tmat_coarse themselves — moot here since hp_pos excludes it).
Trivialization risk (this chapter's own). A formalization that let coarse.h/coarse.Tmat be arbitrary constants unrelated to fine.h/fine.Tmat (dropping the conditional-expectation defining equations) would still typecheck a "lower bound" conclusion but assert nothing about aggregation — exactly the risk BRIEF.md flags: "a formalization that treats (h̄ti,T̄ti) as arbitrary constants rather than as conditional expectations over a partition of the scenario space at time t loses the theorem's actual content." Both hCoarse_h/hCoarse_T (the defining equations) and hCommonOutcome (the theorem's own extra hypothesis) are load-bearing and present.

Selected references

Birge, J.R., Louveaux, F. Introduction to Stochastic Programming, 2nd ed., Springer 2011, Chapter 10, §10.1 (pp. 417-420), Theorem 1 (p. 419).
Birge, J.R. "Decomposition and partitioning methods for multistage stochastic linear programs." Operations Research 33 (1985), 989-1007 — the source Chapter 10's aggregation bounds draw on (cited in §10.2, the neighboring section this mission does not formalize).

4 thms2 active users

Operations Research Optimization·Captain: mikedeng1

The Relaxation Method of Finding the Common Point of Convex Sets and Its Application to the Solution of Problems in Convex Programming 3: A Convergent Relaxation from Z Solves the Equality ProgramResearch Paper

Motivation

Many large convex programs have the form "minimize a strictly convex function $f$ subject to linear equations $Ax=b$ ". Examples are entropy maximization under moment constraints, the estimation of a matrix with prescribed row and column sums (the matrix-scaling or RAS problem of transportation and input–output analysis), and least-norm solutions of linear systems. When $A$ is large and sparse, methods that touch one equation at a time are attractive: each step needs only one row of $A$ .

L. M. Bregman's 1967 paper (doi:10.1016/0041-5553(67)90040-7) introduced such a method. §1 defines a "relaxation" for finding a common point of closed convex sets $A_i$ , in which each step replaces the current point by its $D$ -projection onto one set: the minimizer of a distance-like function $D(\cdot,y)$ over that set. §2 chooses $D$ from the objective $f$ itself, $D(x,y)=f(x)-f(y)-(g(y),x-y)$ with $g$ the gradient of $f$ ; this function is now called the Bregman divergence. Theorem 3 of the paper, the target of this mission, shows that with this choice the relaxation does more than find a feasible point: started at a suitable point, its limit minimizes $f$ over the feasible set. The resulting row-action methods underlie later work on entropy optimization and matrix balancing (Censor and Zenios, Parallel Optimization, 1997) and the Bregman-projection techniques of modern optimization.

Setting

Work in the Euclidean space $E^p$ with inner product $(\cdot,\cdot)$ . Let $S\subset E^p$ be a convex set with closure $\bar S$ and interior $\operatorname{int}S$ . Let $f$ be strictly convex and continuously differentiable over $S$ , with gradient $g(x)$ at $x\in S$ , and continuous over $\bar S$ . Let $A$ be an $m\times p$ matrix with nonzero rows $A_1,\dots,A_m$ and $b\in E^m$ . The problem (2.1)–(2.3) is

\text{minimize } f(x)\quad\text{subject to}\quad Ax=b,\ x\in\bar S,

with feasible set $R=\{x\in E^p\mid Ax=b,\ x\in\bar S\}$ , assumed nonempty. A point of $R$ minimizing $f$ over $R$ is a solution.

The function (1.4) is

D(x,y)=f(x)-f(y)-\bigl(g(y),x-y\bigr),

and $A_i$ also denotes the hyperplane $\{x\mid (A_i,x)=b_i\}$ . The paper assumes that $D$ satisfies its conditions I–VI of §1 with respect to these hyperplanes; among them, condition II provides, for every $y\in S$ , a $D$ -projection $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$ . It also assumes condition (2): if $y^n\in S$ and $y^n\to y^*\in\bar S$ , then $D(y^*,y^n)\to 0$ .

A relaxation sequence with control $(i_n)_{n\ge0}$ starts at $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$ . The control is any sequence of row indices. Finally,

Z=\{x\in S\mid g(x)=uA=\textstyle\sum_i u_iA_i\ \text{for some } u\in E^m\}

is the set of points of $S$ at which the gradient lies in the row space of $A$ .

Formalization targets

Goal: Theorem 3

Assume that the $D$ -projection of every point of $\operatorname{int}S$ onto every $A_i$ lies in $\operatorname{int}S$ . For every control and every relaxation sequence with $x^0\in Z\cap\operatorname{int}S$ that converges to a point $x^*\in R$ ,

f(x^*)\le f(y)\qquad\text{for every } y\in R .

Convergence of the sequence is a hypothesis; the theorem says what the limit is, whichever control produced it.

Milestones

Lemma 3. If $y^*\in R\cap\bar Z$ , then $y^*$ is a solution of (2.1)–(2.3).
(2.7)–(2.8). For $x\in\operatorname{int}S$ there is $\lambda\in\mathbb R$ with $g(P_ix)=g(x)+\lambda A_i$ and $(A_i,P_ix)=b_i$ .
Invariance of $Z$ . $P_i$ maps $Z\cap\operatorname{int}S$ into $Z\cap\operatorname{int}S$ .

An additional item states Note 2: the point and the multiplier in (2.7)–(2.8) are unique.

Significance

Theorem 3 converts a feasibility algorithm into an optimization algorithm for equality-constrained convex programs. Each step solves a one-dimensional problem (the multiplier $\lambda$ of a single equation), so the method scales to systems with very many equations, and with the controls of Theorems 1–2 of the same paper it gives a complete algorithm. Specializations include iterative proportional fitting for entropy objectives and Kaczmarz-type projections for $f(x)=\tfrac12\|x\|^2$ .

The theorem and its proof are classical and have been reproved many times, but no machine-checked proof is known to exist. A formalization produces a verified bridge between three standard pieces of convex analysis: first-order optimality on an affine set, the supporting-hyperplane inequality for a differentiable convex function extended to the closure of its domain, and the passage of a Lagrange condition to a limit. Each is reusable in other row-action and mirror-descent developments.

Difficulty

The obvious argument says: the limit is feasible, and the gradient at every iterate lies in the row space of $A$ , so the limit satisfies the Karush–Kuhn–Tucker conditions. Two steps of this argument fail as stated. First, the gradient is only known on $S$ , the limit may lie on the boundary of $S$ (or outside $S$ , in $\bar S$ ), and $g$ need not extend continuously there, so the multipliers $u^n$ need not converge and no Lagrange condition holds at the limit. Lemma 3 must therefore reach optimality without a gradient at $y^*$ . Second, the Lagrange condition (2.7) at an iterate requires the projection to be an interior minimizer, which is why the theorem carries the hypothesis that $P_i$ preserves $\operatorname{int}S$ ; on the boundary of $S$ a minimizer over $A_i\cap S$ need not satisfy (2.7).

Formalization scope

The space is EuclideanSpace ℝ (Fin p), rows are vectors a i, and $(A_i,x)$ is the real inner product. The gradient $g$ is explicit data tied to $f$ by HasGradientWithinAt f (g x) S x for $x\in S$ and continuous on $S$ ; $S$ is not assumed open, and Mathlib's gradient is not used. The relevant explicit choices are:

The $D$ -projection is a fixed map $P$ ; condition II says $P_iy$ minimizes $D(\cdot,y)$ over $A_i\cap S$ , and condition III is stated for that map.
Condition IV is assumed in its one-sided directional form (implied by the paper's), so theorems under it are at least as strong as the paper's.
"Compact" in conditions V and VI is sequential compactness. Condition V is assumed for the points of $R\cap S$ .
Condition (2) is assumed for limits $y^*\in\bar S$ ; the page prints $y^*\in S$ , but its use at a feasible point needs $\bar S$ .
Translation slips are corrected in the statements and recorded: condition II's " $D(z,x)$ " and " $i\in T$ ", (2.7)'s " $g(x^{n-1})$ " (read $g(x^{n+1})$ ), and "Theorems 1 − 3" (read Theorems 1–2).
The control is an arbitrary sequence of indices in $\{0,\dots,m-1\}$ ; λ is named lam.
Note 2 is stated for candidate points $y,z\in S$ , where $g$ is meaningful.

The goal does not conclude that the relaxation converges; a statement asserting convergence is a different, unproved theorem. Equally, it must not be weakened to a fixed control, to an open $S$ , or to a limit assumed to lie in $Z$ : any of these would trivialize the passage to the limit that the theorem is about.

A complete development needs the first-order condition for a local minimum on an affine hyperplane, the gradient inequality $f(x)\ge f(y)+(g(y),x-y)$ for $x\in\bar S$ , $y\in S$ , and an induction along the relaxation sequence. Proofs of the milestones and of Note 2 are welcome independently.

Selected references

L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Comput. Math. Math. Phys. 7(3) (1967) 200–217. doi:10.1016/0041-5553(67)90040-7
Y. Censor, S. A. Zenios, Parallel Optimization: Theory, Algorithms, and Applications, Oxford University Press, 1997. doi:10.1093/oso/9780195100624.001.0001
Y. Censor, A. Lent, An iterative row-action method for interval convex programming, J. Optim. Theory Appl. 34 (1981) 321–353. doi:10.1007/BF00934676

6 thms1 active userReviewed

Numerical Analysis Partial Differential Equations·Captain: mikedeng1

Mean Field Games: Numerical Methods for the Planning Problem I: The Discrete Planning Scheme Has a Solution, Given by a Fenchel–Rockafellar Saddle PointResearch Paper

Motivation

Mean field games (Lasry and Lions, 2006–2007; Huang, Malhamé and Caines, 2006) model the limit of a large population of identical rational agents. Each agent solves an optimal control problem whose cost depends on the distribution $m$ of all agents, and the distribution is in turn transported by the agents' optimal feedback. In the continuous setting this gives a coupled system: a backward Hamilton–Jacobi equation for the value function $u$ and a forward Fokker–Planck equation for the density $m$ .

In the usual formulation, $m$ is prescribed at the initial time and $u$ at the final time. The planning problem, introduced by P.-L. Lions in his Collège de France lectures, prescribes instead both the initial density $m_0$ and the final density $m_T$ , and asks for a cost (through $u$ ) that steers the population from one to the other. According to the paper (§1, pp. 2–3), Lions proved existence for the continuous planning problem in mainly two cases: $\nu = 0$ with a smooth, strictly convex, superlinear Hamiltonian; and $\nu > 0$ with $H(p) = c|p|^2$ or close to it. In both cases the coupling is local and the densities are smooth and bounded away from $0$ . Existence for $\nu > 0$ and more general Hamiltonians was then open, and for sublinear $H$ , $m_0\ne m_T$ and short horizons there is no solution.

Achdou, Camilli and Capuzzo-Dolcetta (hal-00465404, 2010; SIAM J. Control Optim. 2012) introduced a finite-difference scheme for the planning problem and proved that the discrete system has a solution. The proof writes the scheme as the optimality system of a discrete optimal control problem, a Fokker–Planck equation driven by a control, and obtains a solution from a saddle point given by the Fenchel–Rockafellar duality theorem. This mission formalizes that existence result: Theorem 1 of §3.1 together with the lemmas on which its proof rests.

Setting

Fix integers $N_h, N_T \ge 1$ , a horizon $T > 0$ and a viscosity $\nu \ge 0$ ; let $h = 1/N_h$ and $\Delta t = T/N_T$ . The grid $\mathbb T^2_h$ is the periodic $N_h\times N_h$ grid on the two-dimensional torus, with points $x_{i,j}$ , $(i,j)\in(\mathbb Z/N_h)^2$ . On grid functions $U$ the scheme uses the forward differences $D_1^+$ , $D_2^+$ , the four-component discrete gradient $[D_hU]_{i,j} = ((D_1^+U)_{i,j}, (D_1^+U)_{i-1,j}, (D_2^+U)_{i,j}, (D_2^+U)_{i,j-1})$ , the five-point Laplacian $\Delta_h$ , a discrete divergence $\mathrm{div}_h$ of four-component fields, and the transport operator $\mathcal B(U, M) = \mathrm{div}_h(M\,\nabla_q g(\cdot, [D_hU]))$ .

A numerical Hamiltonian $g(x_{i,j}, q_1,q_2,q_3,q_4)$ is monotone (nonincreasing in $q_1, q_3$ , nondecreasing in $q_2, q_4$ ), $C^1$ , convex, and superlinearly coercive in the directions where monotonicity does not bound it. The coupling is local: $V = W'$ , with $W$ strictly convex, superlinear and $C^2$ . The set $\mathcal K$ consists of the discrete probability densities, $h^2\sum_{i,j}M_{i,j} = 1$ , $M\ge 0$ . The discrete planning scheme (18) asks for $(U^n, M^n)_{0\le n\le N_T}$ with

\frac{U^{n+1}-U^n}{\Delta t} - \nu\Delta_hU^{n+1} + g(x,[D_hU^{n+1}]) = V(M^n),\qquad \frac{M^{n+1}-M^n}{\Delta t} + \nu\Delta_hM^n + \mathcal B(U^{n+1},M^n) = 0,

for $0\le n<N_T$ , with $M^n\in\mathcal K$ , $M^0 = m_0$ and $M^{N_T} = m_T$ .

The duality is set up as follows. With $\chi$ the indicator of $\{m\ge0\}$ , let $\Theta(\alpha,\beta) = \sum_{n,i,j}(W+\chi)^*(\alpha^n_{i,j} + g(x_{i,j},[\beta^n]_{i,j}))$ on dual variables $(\alpha^n,\beta^n)_{1\le n\le N_T}$ . Let $\Lambda(\Psi)$ be the linear map sending $\Psi = (\Psi^n)_{0\le n\le N_T}$ to the discrete Hamilton–Jacobi operator and the discrete gradient of $\Psi^{n+1}$ . Let $\Sigma(\alpha,\beta) = \mathcal F(\Psi)$ if $(\alpha,\beta) = \Lambda(\Psi)$ with $\sum\Psi^0 = 0$ , and $+\infty$ otherwise, where $\mathcal F(\Psi) = \frac1{\Delta t}(\sum m_0\Psi^0 - \sum m_T\Psi^{N_T})$ . The Legendre–Fenchel transforms $\Theta^*$ , $\Sigma^*$ act on primal variables $(M^n, Z^n)_{0\le n<N_T}$ , where $M^n$ is paired with $\alpha^{n+1}$ (Remark 2).

Formalization targets

Goal: Theorem 1

Under (G1), (G3)–(G5), (24), $m_0, m_T\in\mathcal K$ , $m_0 > 0$ , and either $\nu > 0$ or ( $\nu = 0$ and $m_T > 0$ ):

\min_{M,Z}\ \Theta^*(M,Z) + \Sigma^*(-M,-Z) = -\min_{\alpha,\beta}\big(\Theta(\alpha,\beta) + \Sigma(\alpha,\beta)\big)

has a solution $(M,Z)$ , $(\alpha,\beta)$ with a finite common value. Moreover $(\alpha,\beta) = \Lambda(U)$ for some $U$ , and $(U, M)$ , with $M^{N_T} = m_T$ appended, solves the scheme (18), with $Z^{k,n} = M^n\,\partial_{q_k}g(x,[D_hU^{n+1}])$ .

Milestones, in attack order

§3.1, p. 7. $V$ maps $(0,\infty)$ onto $(\lambda,\infty)$ ; $(W+\chi)^*$ is finite, convex, continuous and nondecreasing, with explicit values on and off $\mathcal J_V$ .
Lemma 1. $\Theta$ is convex and continuous, $\Sigma$ is convex and l.s.c., and $\Sigma$ and $\Theta$ are both finite at some point.
Lemma 2. $\Theta^*$ and $\Sigma^*$ are convex and l.s.c., with explicit formulas.
(30). $\Sigma^*(-M,-Z)$ is $0$ on the constraint set of the control problem (26) and $+\infty$ off it.
Lemma 3. If $m_0 > 0$ , some $(M,Z)$ has $\Theta^*$ , $\Sigma^*(-M,-Z)$ finite and $\Theta^*$ finite and continuous near it.
Positivity. A discrete strong maximum principle from the proof of Theorem 1: densities in $\mathcal K$ that solve the discrete Fokker–Planck equation (42) are strictly positive before the final time.

Significance

Theorem 1 is the existence result for the finite-difference planning problem. It is used in the paper's second part (§3.2), where solutions of a penalized scheme, in which the final condition is relaxed into a penalty, are shown to converge to a solution of (18) as the penalty parameter vanishes. The penalized scheme is what is solved numerically. The discrete existence result covers general convex, monotone, coercive numerical Hamiltonians and every $\nu\ge0$ , which includes discretizations of the continuous cases that were still open when the paper was written.

The result has a published proof. What this mission adds is a machine-checked version of it: a complete discrete model of the planning problem (grid, operators, scheme, duality functionals) and the convex-analytic chain that connects it to the Fenchel–Rockafellar theorem. As far as a search of the platform shows, no part of this has been formalized; the series' second mission formalizes the convergence of the penalized scheme on the same model.

Difficulty

Existence for a coupled forward–backward nonlinear system with conditions at both ends of the time interval is not reachable by a fixed-point or time-marching argument: the Hamilton–Jacobi equation runs backward and the Fokker–Planck equation forward, and the final density is imposed rather than computed. The approach goes through duality, and three points are delicate.

All the functionals in the duality take the value $+\infty$ , and Fenchel–Rockafellar needs a qualification condition on each side. Lemma 1 gives it for the dual problem; Lemma 3 gives it for the primal one, and needs $m_0 > 0$ and the coercivity (G5).
The optimality conditions only give a complementarity system: the Hamilton–Jacobi equation holds where $M^n > 0$ and becomes an inequality where $M^n = 0$ . Recovering the scheme (18) needs the strict positivity of $M^n$ , a discrete strong maximum principle. That principle uses the monotonicity (G1) and either diffusion or a positive final density.
The bookkeeping of the time lag between primal and dual variables and of the discrete integration by parts in $\Sigma^*$ must be exact.

Formalization scope

The Lean development lives in the namespace MFGPlanning.Existence. A structure Data carries $N_h, N_T \ge 1$ , $T > 0$ , $\nu\ge0$ , $g$ at the grid points, $W$ , $m_0$ and $m_T$ . Committed conventions:

grid indices are ZMod Nh × ZMod Nh (periodic), and $d = 2$ as in the paper;
the components $q_1,\dots,q_4$ and $Z^1,\dots,Z^4$ are the Fin 4 indices 0..3;
time levels are Fin (NT+1) for $U$ and the scheme, and Fin NT for the duality variables. M k is $M^k$ and α k is $\alpha^{k+1}$ (Remark 2), and Fin.snoc M mT appends $M^{N_T} = m_T$ ;
$(W+\chi)^*$ , $\Theta$ , $\Theta^*$ , $\Sigma$ , $\Sigma^*$ are EReal-valued lattice suprema and infima, so unbounded suprema are $+\infty$ and not a junk value. Convexity of an extended-valued functional is convexity of its epigraph.

Disclosed encodings:

(G2) is not encoded, since it only defines the continuous Hamiltonian;
"coercive" in (24) is read as superlinear growth $W(m)/|m|\to\infty$ , which the paper's own consequence $V((0,\infty)) = (\lambda,\infty)$ requires;
$g$ is given only at grid points;
the optimality conditions (32)–(33) are stated through what Theorem 1 says they are equivalent to: the scheme (18) and the relation (39).

Theorem 1 is not reducible to "the scheme (18) has a solution". The goal also asserts that the primal and dual problems attain their minima, that there is no duality gap with a finite value, and that $(\alpha,\beta) = \Lambda(U)$ . The duality functionals are never real-valued suprema, which would make (30) and (31) hold or fail for junk reasons. A complete development needs finite-dimensional convex analysis on extended-valued functions: conjugates, the Fenchel–Rockafellar theorem with attainment, and subdifferential optimality conditions. These parts are reusable well beyond this mission, and proofs of them as separate theorems are welcome.

Selected references

Y. Achdou, F. Camilli, I. Capuzzo-Dolcetta, Mean field games: numerical methods for the planning problem, preprint hal-00465404v1, 2010. https://hal.science/hal-00465404 ; published in SIAM J. Control Optim. 50(1), 2012. https://doi.org/10.1137/100790069
Y. Achdou, I. Capuzzo-Dolcetta, Mean field games: numerical methods, SIAM J. Numer. Anal. 48(3), 2010. https://doi.org/10.1137/090758477
J.-M. Lasry, P.-L. Lions, Mean field games, Japanese Journal of Mathematics 2(1), 2007. https://doi.org/10.1007/s11537-007-0657-8
I. Ekeland, R. Temam, Convex Analysis and Variational Problems, North-Holland, 1976 (SIAM Classics reprint 1999). https://doi.org/10.1137/1.9781611971088

11 thms1 active userReviewed

Analysis Operations Research Optimization·Captain: mikedeng1

The Łojasiewicz Inequality for Nonsmooth Subanalytic Functions with Applications to Subgradient Dynamical Systems II: The Łojasiewicz Inequality for Convex Subanalytic Functions on Bounded SetsResearch Paper

Motivation

The Łojasiewicz inequality states that near a critical point $a$ of a real-analytic function $f$ there are $\theta\in[0,1)$ and $C$ with $|f(x)-f(a)|^{\theta}\le C\,\|\nabla f(x)\|$ . Łojasiewicz used it in the 1960s to prove that every bounded trajectory of the gradient flow $\dot x=-\nabla f(x)$ has finite length and converges to a single critical point, a conclusion that fails for general $C^\infty$ functions. The inequality has since become the standard tool for convergence analysis of descent methods on nonconvex problems.

Optimization problems are, however, rarely smooth: constraints enter through indicator functions, and objectives contain norms, maxima and penalties. Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the inequality to nonsmooth subanalytic functions, replacing $\|\nabla f\|$ by a slope built from the limiting subdifferential. Their Section 3.1 treats functions continuous on a closed domain; Section 3.2, the subject of this mission, treats lower semicontinuous convex functions, which may jump to $+\infty$ and whose domain need not be closed. The Kurdyka–Łojasiewicz framework built on this paper (Attouch–Bolte–Svaiter 2013; Bolte–Sabach–Teboulle 2014) underlies the convergence theory of proximal and splitting algorithms used throughout operations research.

Setting

Work in $\mathbb R^n$ with the Euclidean norm, and let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ with domain $\operatorname{dom} f=\{x: f(x)<+\infty\}$ .

A set $A\subseteq\mathbb R^n$ is semianalytic if near every point it is a finite union of finite intersections of sets $\{f_{ij}=0,\ g_{ij}>0\}$ with $f_{ij},g_{ij}$ real-analytic. It is subanalytic if near every point it is the projection of a bounded semianalytic subset of $\mathbb R^n\times\mathbb R^m$ . A function is subanalytic when its graph $\{(x,\lambda): f(x)=\lambda\}$ is. Semialgebraic functions (norms, polynomials, indicators of polyhedra) are subanalytic.

The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y\to x,\,y\ne x}\big(f(y)-f(x)-\langle x^*,y-x\rangle\big)/\|y-x\|\ge 0$ , for $x\in\operatorname{dom} f$ , and is empty otherwise. The limiting subdifferential $\partial f(x)$ is the set of limits of $x_k^*\in\hat\partial f(x_k)$ with $(x_k,f(x_k))\to(x,f(x))$ . The nonsmooth slope is $m_f(x)=\inf\{\|x^*\|:x^*\in\partial f(x)\}$ , equal to $+\infty$ when $\partial f(x)=\emptyset$ , and $\operatorname{crit} f=\{x: 0\in\partial f(x)\}$ is the set of critical points. For lower semicontinuous convex $f$ , $\partial f$ is the subdifferential of convex analysis and $\operatorname{crit} f$ is the set of minimizers. Write $\min f$ for the minimum value and $d_S(x)$ for the distance from $x$ to $S=\operatorname{crit} f$ . The epigraphical sum $g(x)=\inf_u\{f(u)+\tfrac12\|x-u\|^2\}$ is the Moreau envelope of $f$ .

Ratios follow the paper's conventions $0^0=1$ and $\infty/\infty=0/0=0$ .

Formalization targets

Goal: Theorem 3.3

Let $f$ be lower semicontinuous, convex and subanalytic with $\operatorname{crit} f\ne\emptyset$ . For every bounded set $K$ there is $\theta\in[0,1)$ such that

\frac{|f-\min f|^{\theta}}{m_f}\quad\text{is bounded on }K.

The exponent may depend on $K$ ; neither $\theta$ nor the bound is fixed.

Milestones

Eq. (5): $\partial f=\hat\partial f=$ the convex subdifferential, for lsc convex $f$ .
Section 3.2: $\operatorname{crit} f$ is closed, convex and equal to the set of minimizers.
Inequality (16): $|f(x)-\min f|\le\|x^*\|\,d_S(x)$ for all $x^*\in\partial f(x)$ .
Remark 3.6: $|f-\min f|/m_f$ is bounded around every critical point, without subanalyticity.
Proposition 2.9: the epigraphical sum $g$ is $C^1$ and subanalytic when $\inf f\in\mathbb R$ .
Properties (a)–(c): $g$ is finite and $C^1$ , $g\le f$ , $\operatorname{crit} g=\operatorname{crit} f$ , $\inf g=\inf f$ .
Proposition 2.13(ii): $\operatorname{crit} f$ is subanalytic for subanalytic $f$ that is relatively bounded on its domain.
Section 2.1: the distance to a subanalytic set is subanalytic.
The Łojasiewicz factorization lemma on compact sets (recalled from Bierstone–Milman).
Inequality (15): $d_S(x)\le c^{-1/r}|f(x)-\min f|^{1/r}$ on $K$ , with $r>1$ , $c>0$ .
Remark 3.5: the growth condition $|f-\min f|\ge c\,d_S^{\,r}$ on a compact $K$ alone yields a Łojasiewicz inequality at critical points interior to $K$ .

Significance

Theorem 3.3 gives, for convex subanalytic functions, a Łojasiewicz inequality that is uniform on bounded sets rather than local at one critical point, and it needs neither continuity of $f$ on its domain nor a closed domain. Remark 3.4 of the paper exhibits a convex function covered by Theorem 3.3 but not by the continuous-case Theorem 3.1. Through inequality (20) of Section 4, it yields finite length and convergence rates for the subgradient flow $\dot x\in-\partial f(x)$ of such functions. The intermediate inequality (15) is a Hölderian error bound, $d_S\le C|f-\min f|^{1/r}$ , of the kind that drives linear and sublinear rate analyses of first-order methods.

The result is proved in the paper; no machine-checked version of it, or of the nonsmooth Łojasiewicz inequality in any form, is known. Formalizing it would add to the library: subanalytic sets and functions, the limiting subdifferential of convex functions and its agreement with the classical one, the Moreau envelope with its critical points and infimum, and the passage from a growth condition to a Łojasiewicz inequality. Remarks 3.5 and 3.6 isolate parts that need no subanalytic geometry at all.

Difficulty

The convex-analysis steps (inequality (16), properties of the Moreau envelope) are classical. The obstacle is subanalytic geometry. The natural first idea, applying the Łojasiewicz factorization lemma directly to $f-\min f$ and $d_S$ , fails: $f$ is neither continuous nor finite, and its domain need not be subanalytic even when $f$ is convex and subanalytic (Example 2.5 of the paper). The milestones route through the Moreau envelope, which is continuous and finite, but subanalyticity is not preserved by infima over unbounded sets, so the subanalyticity of the envelope (Proposition 2.9) needs a localization argument. The subanalyticity of $\operatorname{crit} g$ and of $d_S$ rests on the stability theory of subanalytic sets (Gabrielov's complement theorem, the projection theorem for globally subanalytic sets), none of which exists in Mathlib.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "lower semicontinuous, convex, somewhere finite and never $-\infty$ " is the published definition MoreauProx.Characterization.GammaZero, whose convexity is convexity of the epigraph. The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff; the convex subdifferential subgrad appears only in Eq. (5), which proves the agreement and is never assumed. Semianalytic and subanalytic sets are defined from scratch for any finite-dimensional real normed space, so that one definition serves $\mathbb R^n$ and its products; global subanalyticity is not defined. $\min f$ is written $\inf_y f(y)$ in EReal and converted to a real number only where it is finite. The bounded ratio (14) is encoded as " $|f(x)-\min f|^{\theta}\le C\|x^*\|$ for every $x\in K$ and every $x^*\in\partial f(x)$ ", with real powers (Real.rpow, $0^0=1$ ). Inequalities (15) and (17) are imposed only where $f(x)<+\infty$ , since Lean sends $+\infty$ to $0$ under toReal.

Trivializing encodings are ruled out: the goal is stated with the limiting subdifferential rather than an assumed convex subdifferential, the slope is never computed in ℝ≥0∞ where $0\cdot\infty=0$ would make the ratio vacuous, and $\theta$ remains existential in $[0,1)$ with the quantifier order "for every $K$ there is $\theta$ ", so that $\theta=0$ is excluded at critical points in $K$ by $0^0=1$ .

A complete development needs a working theory of subanalytic sets (stability under finite unions, complements, closure, projections of bounded sets, the factorization lemma), the Moreau envelope of a convex function on $\mathbb R^n$ and its $C^1$ property, and the convex-analytic description of the limiting subdifferential. The subanalytic-geometry layer and the Moreau-envelope facts are reusable well beyond this mission; contributions to either, or proofs of the convex-only milestones (Eq. (5), (16), Remarks 3.5–3.6), are welcome independently.

Selected references

J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4) (2007) 1205–1223. https://doi.org/10.1137/050644641
E. Bierstone, P. D. Milman, Semianalytic and subanalytic sets, Publ. Math. IHÉS 67 (1988) 5–42. https://doi.org/10.1007/BF02699126
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, Les Équations aux Dérivées Partielles, Éditions du CNRS, Paris, 1963, 87–89.
H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137 (2013) 91–129. https://doi.org/10.1007/s10107-011-0484-9
J. Bolte, S. Sabach, M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Math. Program. 146 (2014) 459–494. https://doi.org/10.1007/s10107-013-0701-9

18 thms1 active userReviewed

Linear Optimization Statistics·Captain: mikedeng1

Conditional Logit Analysis of Qualitative Choice Behavior 4: Existence of the Maximum Likelihood Estimate Is Decided by a Quadratic ProgramResearch Paper

Why a likelihood maximum needs a diagnostic

The conditional logit model assigns probabilities to choices among alternatives whose observable attributes differ from trial to trial. A fitted parameter vector is usually obtained by maximizing a log-likelihood. For a finite data set, however, maximization need not produce a finite vector: some directions in parameter space can keep improving the likelihood while their length grows without bound. McFadden identifies a condition that rules out these directions and then gives a quadratic program that can test the condition. This mission formalizes that test, Lemma 4 of the published 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior.

The chapter develops a statistical model from observable choice data and addresses the existence of a maximum likelihood estimate in Lemma 3. Lemma 4 turns its existence condition into a finite optimization problem. The diagnostic matters because an optimization routine returning increasingly large parameter estimates is not, by itself, evidence that a finite maximizer exists. The result specifies a mathematical test tied to the observed choice counts and the attributes of the alternatives.

Choice experiments and weighted differences

There are $N\geq1$ trials. Trial $n$ offers $J_n$ alternatives, indexed by $i$ and $j$ . Alternative $i$ has an attribute vector $z_{in}\in\mathbb R^K$ , and $S_{in}$ counts how many times it was selected in that trial. Each trial has at least two alternatives and $R_n=\sum_iS_{in}>0$ observations. The vector $\theta\in\mathbb R^K$ is the unknown parameter of the underlying conditional logit model. Equation (16) assigns alternative $i$ a probability proportional to $\exp(z_{in}\cdot\theta)$ , with the probabilities normalized over the alternatives in the same trial McFadden, pp. 113–114, equation (16).

For the test, define the weighted difference

w_{nij}=S_{in}(z_{jn}-z_{in})\in\mathbb R^K.

It is indexed by every trial and every ordered pair of alternatives, including $i=j$ and alternatives whose observed count is zero. Such terms simply produce zero vectors. Keeping them in the index set makes the formal statement agree with the chapter's quantifiers and its quadratic program.

Axiom 5, called full rank in the chapter, says that the rows obtained by subtracting each trial's probability weighted mean attribute vector from its alternative attributes have rank $K$ . Equivalently, the vectors $z_{jn}-z_{in}$ span $\mathbb R^K$ ; the probability weights in that mean are strictly positive and sum to one. Axiom 6 says that no nonzero direction $\gamma\in\mathbb R^K$ satisfies $w_{nij}\cdot\gamma\leq0$ for every ordered index triple. These are conditions on the same observed experiment, but they serve different roles: full rank concerns the attribute geometry, while Axiom 6 also uses the choice counts McFadden, p. 116, Axioms 5–6.

Formalization targets

Lemma 4: a quadratic-programming test

Let $Q$ be the set of feasible vectors

Q=\left\{y=\sum_{n=1}^{N}\sum_{i,j=1}^{J_n}\alpha_{ijn}w_{nij}: \alpha_{ijn}\geq1\text{ for all }n,i,j\right\}.

The mission's goal is the equivalence in Lemma 4:

\text{Axiom 6 holds} \quad\Longleftrightarrow\quad \min_{y\in Q}y\cdot y=0.

The right side means that the program attains a value of zero. An infimum of zero without an attained feasible point would be a weaker statement and would not express the lemma. The three milestones follow the three assertions in the printed proof: a zero minimum implies Axiom 6; an interior origin in the cone generated by the $w_{nij}$ gives positive coefficients and a zero minimum; and a noninterior origin gives a separating direction that violates Axiom 6 McFadden, p. 117, Lemma 4 and equation (22).

What the result provides

Lemma 3 of the chapter states that Axiom 6 characterizes the existence of a vector maximizing the conditional-logit log-likelihood under the preceding axioms. Lemma 4 gives a finite quadratic-programming criterion for that same condition. It therefore allows the model's existence question to be checked from data before treating a numerical optimizer's output as an estimate McFadden, pp. 116–117, Lemmas 3–4.

The paper proves these results. The work here is to produce machine-checkable statements for the finite-dimensional data, the two axioms, the feasible set, and the equivalence, followed by proofs in the solver stage. The cone and separation milestones can support later formalizations of existence conditions in other finite exponential-family models, provided their hypotheses and signs are checked anew. This mission does not claim a general theorem for all such models.

Why the equivalence is delicate

The tempting diagnostic is to ask whether a numerical solve returns a small objective value. That does not settle the mathematical question: the objective's infimum could approach zero without the feasible set containing a zero vector. The paper's conclusion is about a minimum, so attainment must remain visible in the formal statement. There is also a distinction between positive coefficients in a cone representation and the printed constraints $\alpha_{ijn}\geq1$ in equation (22). Both conditions must appear in their proper places.

The full-rank condition alone does not ensure that the vectors $w_{nij}$ span the attribute space if a trial has no observed choices. The section describes $R_n$ repetitions of each trial, and the formal data require $R_n>0$ . This convention is needed for the strict-inequality claim in the first paragraph of Lemma 4's proof. The geometry also has to account for every ordered pair, even when its vector is zero; dropping these indices would alter the program stated in the chapter.

Formalization scope

Lean represents a nonempty set of trials by Fin N, alternatives in trial $n$ by Fin (J n), counts by natural numbers, and attributes by EuclideanSpace ℝ (Fin K). The count $R_n$ is the sum of observed choice counts. The model requires $J_n\geq2$ and $R_n>0$ for each trial. There is no extra assumption that $K>0$ : the zero-dimensional case is included and the equivalence has its ordinary degenerate meaning there.

Axiom 5 is encoded through the equivalent span of within-trial attribute differences. This removes the parameter dependent logit probabilities from a theorem that only uses rank. Axiom 6 retains exactly the nonpositive sign and every $n,i,j$ from the page. The feasible set uses coefficients at least one, while the auxiliary generated cone uses nonnegative coefficients. The quadratic objective is the square of the Euclidean norm. IsLeast on its image over the feasible set expresses an attained minimum, so the statement cannot be satisfied by a vacuous or unattained infimum.

The definition bundle and the three proof-step theorems are the mission's direct scope. A complete development needs finite-dimensional inner-product geometry, finite sums, a cone interior argument, and separation. The definitions of weighted differences and the feasible set are reusable for studying nearby existence tests. Contributions that prove the stated milestones or supply faithful finite-dimensional geometry for them are welcome; substitutions that weaken the coefficient constraint or the attainment claim do not establish Lemma 4.

Selected references

Daniel McFadden, “Conditional Logit Analysis of Qualitative Choice Behavior,” in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, 1974, pp. 105–142; especially pp. 113–117, Axioms 5–6, Lemmas 3–4, and equation (22). Book catalog search.

5 thms1 active userReviewed

Algorithmic Game Theory Machine Learning Optimization·Captain: mikedeng1

Blackwell Approachability and No-Regret Learning are Equivalent 2: A No-Regret Algorithm and a Valid Halfspace Oracle Approach a Compact Convex Set at Rate 2·Regret_T/TResearch Paper

Motivation

Blackwell approachability is the vector-payoff analogue of von Neumann's minimax theorem. In a repeated game where each round's outcome is a vector $u(x_t, y_t) \in \mathbb R^d$ , a player wants the running average of these vectors to converge to a target set $S$ , whatever the opponent does. Blackwell (1956) showed when this is possible, and approachability has since become a standard tool for calibrated forecasting, regret minimization with respect to general benchmarks, and learning in games.

Online linear optimization (OLO) is the problem of choosing points $\theta_t$ in a fixed decision set $\mathcal K$ against a sequence of linear losses $\langle f_t, \cdot\rangle$ , with performance measured by regret against the best fixed point in hindsight. Algorithms with regret $o(T)$ — "no-regret" algorithms such as online gradient descent (Zinkevich, 2003) — are among the most studied objects of machine learning.

Abernethy, Bartlett and Hazan (COLT 2011) showed that the two problems are algorithmically equivalent: each can be converted into the other with explicit control of the rates. This mission covers the direction from OLO to approachability.

Timeline:

1956: Blackwell proves the approachability theorem for convex sets, via a geometric projection strategy.
2003: Zinkevich introduces online gradient descent, a no-regret algorithm for any bounded convex decision set.
2009: Even-Dar, Kleinberg, Mannor and Mansour state approachability in the response-satisfiability form (as cited on p. 32 of the 2011 paper).
2011: Abernethy, Bartlett and Hazan give the two reductions, with explicit rates, and apply them to efficient calibration.

Setting

A Blackwell instance $(\mathcal X, \mathcal Y, u, S)$ consists of compact convex sets $\mathcal X \subseteq \mathbb R^n$ , $\mathcal Y \subseteq \mathbb R^m$ , a payoff $u : \mathcal X \times \mathcal Y \to \mathbb R^d$ that is affine in each argument (biaffine), and a closed convex target set $S \subseteq \mathbb R^d$ . Write $\mathtt{dist}(z, U) = \inf_{w \in U}\|z - w\|$ for the Euclidean distance to a set, and $B_2(r)$ for the closed Euclidean ball of radius $r$ .

A halfspace oracle takes a halfspace $H = \{z : \langle a, z\rangle \le c\}$ and returns a point $\mathcal O(H) \in \mathcal X$ ; it is valid if for every halfspace $H \supseteq S$ , $u(\mathcal O(H), y) \in H$ for all $y \in \mathcal Y$ .

A set $X \subseteq \mathbb R^d$ is a cone if $\alpha z \in X$ for all $z \in X$ , $\alpha \ge 0$ . For $K \subseteq \mathbb R^d$ , $\mathtt{cone}(K) = \{\alpha x : \alpha \ge 0, x \in K\}$ , and the polar cone of $C$ is $C^0 = \{\theta : \langle \theta, x\rangle \le 0 \ \forall x \in C\}$ .

An OLO algorithm $\mathcal L$ maps past loss vectors $(f_1, \dots, f_{t-1})$ to a point $\theta_t \in \mathcal K$ , and its regret is

\mathrm{Regret}_T = \sum_{t=1}^T \langle f_t, \theta_t\rangle - \min_{\theta \in \mathcal K} \sum_{t=1}^T \langle f_t, \theta\rangle .

Algorithm 2 runs $\mathcal L$ on $\mathcal K = S^0 \cap B_2(1)$ when $S$ is a cone: at round $t$ it sets $\theta_t = \mathcal L(f_1, \dots, f_{t-1})$ , plays $x_t = \mathcal O(\{z : \langle \theta_t, z\rangle \le 0\})$ , observes $y_t \in \mathcal Y$ , and feeds $f_t = -u(x_t, y_t)$ back to $\mathcal L$ .

When $S$ is compact but not a cone, it is lifted: with $\kappa = \max_{s\in S}\|s\|$ and $\kappa \oplus z \in \mathbb R^{d+1}$ the concatenation, put $u'(x, y) = \kappa \oplus u(x, y)$ and $S' = \mathtt{cone}(\{\kappa\} \times S)$ , and run Algorithm 2 on $(\mathcal X, \mathcal Y, u', S')$ .

Formalization targets

Goal: Corollary 18 (p. 39)

For a Blackwell instance with $S$ nonempty and compact, any valid halfspace oracle for the lifted instance, any OLO algorithm with values in $\mathcal K' = (S')^0 \cap B_2(1)$ , any $T \ge 1$ and any $y_1, \dots, y_T \in \mathcal Y$ , the run of Algorithm 2 on the lifted instance satisfies

\mathtt{dist}\Big(\frac1T\sum_{t=1}^T u(x_t,y_t), S\Big) \le 2\,\mathtt{dist}\Big(\frac1T\sum_{t=1}^T u'(x_t,y_t), S'\Big) \le \frac2T\,\mathrm{Regret}_T .

The bound holds for every $T$ and every adversary, with no rate assumed for $\mathcal L$ ; a no-regret $\mathcal L$ then gives approachability.

Milestones

Lemma 13 (p. 35): for a nonempty convex cone $C$ , $\mathtt{dist}(x, C) = \max_{\theta \in C^0 \cap B_2(1)} \langle \theta, x\rangle$ .
Theorem 17 (p. 38): if $S$ is a cone, Algorithm 2 achieves $\mathtt{dist}\big(\frac1T\sum_t u(x_t,y_t), S\big) \le \mathrm{Regret}(\mathcal L_{\mathcal K}; f_{1:T})/T$ .
Lemma 14 (p. 35): for nonempty compact convex $\mathcal K$ , $\kappa = \max_{\mathcal K}\|\cdot\|$ and $x \notin \mathcal K$ , $\mathtt{dist}(\kappa\oplus x, \mathtt{cone}(\{\kappa\}\times\mathcal K)) \le \mathtt{dist}(x, \mathcal K) \le 2\,\mathtt{dist}(\kappa\oplus x, \mathtt{cone}(\{\kappa\}\times\mathcal K))$ .

Significance

The result. Corollary 18 turns any no-regret algorithm into an approachability strategy for a compact convex target, provided a valid halfspace oracle is available, with rate $2\,\mathrm{Regret}_T/T$ . Combined with online gradient descent it gives an $O(1/\sqrt T)$ approachability rate, and through the choice of OLO algorithm it lets approachability inherit the computational efficiency of online learning. The paper uses this route to build an efficient calibrated forecaster (Section 5). Together with the converse reduction (Theorem 16), it shows that the two problems are equivalent.

Formalizing it. The results are proved in the paper; none of them has been machine-checked. Formalizing them requires the conic duality formula for distances (Lemma 13), a quantitative lifting lemma (Lemma 14) and the bookkeeping of an interactive protocol. The proof of Lemma 14 on the page is a sketch: it refers to an undefined point and uses a triangle-similarity argument, so a complete proof is new work.

Difficulty

The reduction's core is Lemma 13: the distance to a cone is a maximum of a linear function over the polar cone's unit ball. Lemma 13 needs projection onto a cone in Euclidean space; for a non-closed cone the projection may not exist, and the argument must go through the closure. The lifting Lemma 14 is a geometric statement whose page proof relies on a picture and an undefined point, so the factor 2 has no complete written argument. Finally, connecting the average lifted payoff to the lift of the average payoff, and the halfspace guarantee $\langle\theta_t, f_t\rangle \ge 0$ to the regret, requires keeping the round indexing and the oracle's validity domain exactly aligned.

Formalization scope

All spaces are EuclideanSpace ℝ (Fin d). The concatenation $\kappa\oplus z$ lives in EuclideanSpace ℝ (Fin (d+1)) with coordinate 0 equal to $\kappa$ , so $\|\kappa\oplus z\|^2 = \kappa^2 + \|z\|^2$ ; a product type with the sup norm would change every distance and is ruled out. Distances are Metric.infDist. The polar cone uses the paper's sign ( $\le 0$ ), the negative of Mathlib's innerDual. A halfspace is the pair $(a, c)$ ; a valid oracle must answer every halfspace containing $S$ , including $a = 0$ , not only the halfspaces the algorithm happens to query. The OLO algorithm is a map from histories Fin t → ℝᴰ with values in $S^0 \cap B_2(1)$ at every history. Rounds are $t = 1, \dots, T$ , and the run of Algorithm 2 is given as hypotheses on sequences $\theta, x, f$ , which exist and are unique by recursion. The minimum in the regret and $\kappa$ are written as sInf/sSup of images over nonempty compact sets, where they are attained.

Hypotheses added relative to the page: $S \neq \emptyset$ and $T \ge 1$ in the goal; $C \ne \emptyset$ in Lemma 13 (the empty set is a cone under Definition 11 and the identity fails for it); $\mathcal K \ne \emptyset$ in Lemma 14. Corrected misprints, each disclosed in the item's note: " $\mathrm{Regret}_T(\mathcal A)$ " in Corollary 18 and (9) denotes the regret of the OLO algorithm $\mathcal L$ on the lifted losses; Lemma 14's " $\mathcal K \subseteq \mathcal H$ " has a stray $\mathcal H$ ; $\kappa$ is the maximal norm of the set, not its diameter. The oracle in the goal is a valid oracle for the lifted instance, which is what applying Algorithm 2 to $(\mathcal X, \mathcal Y, u', S')$ requires.

A formalization in which the oracle is valid only at the run's own queries, the OLO algorithm is unconstrained, the regret's minimum ranges over all of $\mathbb R^{d+1}$ , or the middle term of the goal is dropped, is a different statement and is ruled out.

The development needs: the dual formula for the distance to a convex cone, nearest-point projection onto closed convex sets (in Mathlib), compactness of polar-cone slices, and finite sums of biaffine payoffs. The cone layer (Lemma 13) is reusable for the converse direction of the paper and for conic duality generally. Proofs of any milestone, and of the bridge from an oracle for the original instance to one for the lifted instance, are welcome.

Selected references

J. Abernethy, P. L. Bartlett, E. Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, JMLR W&CP 19 (COLT 2011), pp. 27–46. https://proceedings.mlr.press/v19/abernethy11b.html
D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6(1), 1956, pp. 1–8. https://doi.org/10.2140/pjm.1956.6.1
M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf

6 thms1 active userReviewed

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems IV: Online Stochastic Mirror Descent for Combinatorial Semi-BanditsTextbook

Motivation

Many sequential decision problems ask a learner to choose, round after round, a combination of items: a set of $m$ ads out of $d$ , a path in a network, a matching. After each choice the learner sees the loss of the items it used, not of those it did not. This is online combinatorial optimization with semi-bandit feedback. It contains the classical adversarial multi-armed bandit (choose one of $d$ arms) and is a standard model in online advertising, routing and ranking.

Chapter 5 of Bubeck and Cesa-Bianchi's monograph arXiv:1204.5721v2 treats this problem with one algorithm, Online Stochastic Mirror Descent (OSMD). Every regret bound in the chapter comes from a single mirror-descent inequality, specialized through the choice of a convex "regularizer". The chapter's capstone, Theorem 5.7, shows that a polynomial regularizer gives pseudo-regret $O(\sqrt{mdn})$ with no logarithmic factor. For $m=1$ this is the minimax-optimal rate of the adversarial bandit, first attained by the INF strategy of Audibert and Bubeck (2009). The semi-bandit version is due to Audibert, Bubeck and Lugosi (2014).

Setting

Vectors live in $\mathbb R^d$ . The arm set is a nonempty $\mathcal C\subseteq\{0,1\}^d$ with $\|v\|_1=m$ for every $v\in\mathcal C$ , and $\mathcal K=\mathrm{Conv}(\mathcal C)$ . An oblivious adversary fixes loss vectors $\ell_1,\dots,\ell_n\in[0,1]^d$ . In round $t$ the learner plays a random arm $v_t\in\mathcal C$ , pays $\ell_t^\top v_t$ , and observes $(\ell_t(1)v_t(1),\dots,\ell_t(d)v_t(d))$ . The pseudo-regret is

\bar R_n=\mathbb E\sum_{t=1}^n\ell_t^\top v_t-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t^\top x .

A Legendre function on $\bar D$ , for a nonempty open convex $D$ , is a continuous $F:\bar D\to\mathbb R$ that is strictly convex and $C^1$ on $D$ and whose gradient norm tends to $+\infty$ at $\bar D\setminus D$ . Its Bregman divergence is $D_F(x,y)=F(x)-F(y)-(x-y)^\top\nabla F(y)$ , and its Legendre–Fenchel transform is $F^*(u)=\sup_{x\in\bar D}(x^\top u-F(x))$ .

Online Mirror Descent with learning rate $\eta>0$ and vectors $g_t$ starts at $x_1\in\arg\min_{\mathcal K}F$ . It then sets $\nabla F(w_{t+1})=\nabla F(x_t)-\eta g_t$ and $x_{t+1}=\arg\min_{y\in\mathcal K}D_F(y,w_{t+1})$ . OSMD uses a random estimate $g_t=\tilde\ell_t$ of the loss. In the semi-bandit case it plays $v_t$ with $\mathbb E[v_t\mid x_t]=x_t$ and uses

\tilde\ell_t(i)=\frac{\ell_t(i)\,v_t(i)}{x_t(i)}. \tag{5.5}

A $0$ -potential is a convex, $C^1$ , increasing $\psi:(-\infty,a)\to(0,\infty)$ with $\psi(-\infty)=0$ , $\psi(a^-)=+\infty$ and $\int_0^1|\psi^{-1}|<\infty$ . It defines the Legendre function $F_\psi(x)=\sum_i\int_0^{x_i}\psi^{-1}(s)\,ds$ on $[0,\infty)^d$ . With $\psi=\exp$ this is the negative entropy.

Formalization targets

Goal: Theorem 5.7 (p. 80)

For every $0$ -potential $\psi$ and non-negative unbiased estimates,

\bar R_n\le\frac{\sup_{\mathcal K}F_\psi-F_\psi(x_1)}{\eta}+\frac\eta2\sum_{t=1}^n\sum_{i=1}^d\mathbb E\left[\frac{\tilde\ell_t(i)^2}{(\psi^{-1})'(x_t(i))}\right].

For $\psi(x)=(-x)^{-q}$ with $q>1$ , the estimate (5.5) and $\eta=\sqrt{\tfrac{2}{q-1}\,m^{1-2/q}/(n\,d^{1-2/q})}$ ,

\bar R_n\le q\sqrt{\tfrac{2}{q-1}\,mdn},\qquad\text{and }\ \bar R_n\le2\sqrt{2mdn}\ \text{ at }q=2.

Milestones

Lemma 5.1: $F^{**}=F$ , $\nabla F^*=(\nabla F)^{-1}$ on $D^*$ , and $D_F(x,y)=D_{F^*}(\nabla F(y),\nabla F(x))$ .
Lemma 5.2: existence, uniqueness and the Pythagorean inequality of Bregman projections.
Theorem 5.3: $\sum_t\ell_t(x_t)-\sum_t\ell_t(x)\le\frac{F(x)-F(x_1)}\eta+\frac1\eta\sum_tD_{F^*}(\nabla F(x_t)-\eta\nabla\ell_t(x_t),\nabla F(x_t))$ .
Theorem 5.5, linear losses, and its corrected general form.
Lemma 5.3: $F_\psi$ is Legendre and $D_{F_\psi^*}(u,v)\le\frac12\sum_i\psi'(v_i)(u_i-v_i)^2$ for $u\le v$ .
Theorem 5.6: with the negative entropy, $\bar R_n\le\sqrt{2mdn\ln(d/m)}$ .

Significance

Theorem 5.7 is the sharpest semi-bandit bound in the monograph. It shows that removing the $\sqrt{\ln(d/m)}$ factor of the exponential-weights analysis (Theorem 5.6) is a matter of the regularizer, not of a new algorithm. The same OSMD template gives the Euclidean-ball bound of Theorem 5.8 and is reused for bandit convex optimization in Chapter 6. Lemma 5.1, Lemma 5.2 and Theorem 5.3 are the standard mirror-descent toolkit, used throughout online learning and optimization.

All results of the chapter are proved in the book. Lemmas 5.1 and 5.2 are cited from Cesa-Bianchi and Lugosi (2006). None of them is formalized on Prove2Me. The published mirror-descent bound of Bandit Algorithms XII treats linear losses with a comparator inside $D$ and Euclidean-space vectors; it is not Theorem 5.3. The mission adds a machine-checked version of the whole chain, from Legendre duality to the explicit constant $q\sqrt{2mdn/(q-1)}$ , with two of the printed statements corrected (below).

Difficulty

The pathwise mirror-descent inequality is a telescoping argument, but several of its steps rest on convex analysis that Mathlib does not package. One is the existence and interior location of Bregman projections onto a set that touches the boundary of $D$ . Another is the differentiability of $F^*$ on the open dual space and the identity $\nabla F^*=(\nabla F)^{-1}$ . A third is the closed form of $F_\psi^*$ for a potential defined through an improper integral of $\psi^{-1}$ .

The probabilistic step is not a martingale argument. Only conditioning on the current iterate $x_t$ is available. The estimate (5.5) divides by $x_t(i)$ , so its integrability and unbiasedness have to be derived from the fact that the iterates stay in the open orthant. Finally, the explicit constant requires a Hölder step, $\sum_ix_1(i)^{1-1/q}\le m^{(q-1)/q}d^{1/q}$ , and the matching bound $\sum_ix_t(i)^{1/q}\le m^{1/q}d^{1-1/q}$ .

Formalization scope

Vectors are Fin d → ℝ. The arm set is a Set of $0/1$ vectors with coordinate sum $m$ , and $\mathcal K$ is convexHull ℝ C. Rounds are $t=1,\dots,n$ , sums run over Finset.Icc 1 n, and index $0$ is unused. A randomized run is a family of measurable processes $x_t, v_t, \tilde\ell_t, w_t$ on a probability space, with the deterministic OMD recursion holding on every sample path. $\mathbb E[\cdot\mid x_t]$ is the coordinatewise conditional expectation given $\sigma(x_t)$ , which is exactly what the book's proofs use. Losses are oblivious, so $\bar R_n\le B$ is stated as "for every $x\in\mathcal K$ , $\mathbb E\sum_t\ell_t^\top v_t-\sum_t\ell_t^\top x\le B$ ". $F^*$ is valued in EReal, and $D_{F^*}$ is evaluated only on the open dual space, where $F^*$ is finite. Wherever an expectation of a possibly non-integrable quantity appears on a right-hand side, its integrability is assumed: the book's bound is then $+\infty$ and trivial, while Lean's integral would be $0$ .

Corrections and instantiations, each labelled in the item's Formalization Note:

Theorem 5.7, corrected misprint. The book prints $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{d^{1-2/q}}}$ . The proof (p. 81) gives the stated bound only for $\eta=\sqrt{\frac2{q-1}\frac{m^{1-2/q}}{n\,d^{1-2/q}}}$ , which is stated. At $q=2$ this is $\eta=\sqrt{2/n}$ .
Theorem 5.5, corrected misprint. In the first bound the book prints $\mathbb E[\|x_t-\tilde x_t\|\,\|\tilde g_t\|_*]$ . That statement fails for $\ell_t(x)=x^2$ on $[-1,1]$ with $F=x^2/2$ and $\tilde x_t=\pm1$ . The version stated uses $\|\nabla\ell_t(\tilde x_t)\|_*$ , as the proof's first inequality does. The linear-loss bound is stated as printed.
Lemma 5.2. "For all $z\in K\cap D$ " is read as "for the projection $z$ ", which lies in $K\cap D$ .
Hypotheses made explicit: $q>1$ ; non-negativity of the estimates in Theorem 5.6 (used in its proof); unbiasedness $\mathbb E[\tilde\ell_t\mid x_t]=\ell_t$ in the general parts of Theorems 5.6 and 5.7; $\mathcal K\cap(0,\infty)^d\ne\emptyset$ (OMD's requirement $K\cap D\ne\emptyset$ ); a subgradient selection as an explicit input.
Theorem 5.6's particular bound uses the book's $\eta=\sqrt{\frac{2m}{nd}\ln\frac dm}$ as printed. There are no O(·) constants in the chapter's statements.

A trivializing formalization would let $\eta$ , $x_t$ or the estimate be junk values: an OSMD step at $\eta=0$ , a Lean division $x/0=0$ , or a regret written as a real infimum over an unbounded set. Here every run is the book's algorithm on the open orthant, and each bound is stated against every comparator in $\mathcal K$ .

Reusable beyond this mission: the Legendre/Bregman layer, the OMD run predicate and the $\omega$ -potential layer. Proofs of Lemmas 5.1 and 5.2 in this generality would be welcome additions to the library.

Selected references

S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012; arXiv:1204.5721v2. https://arxiv.org/abs/1204.5721
N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921
J.-Y. Audibert, S. Bubeck, Regret bounds and minimax policies under partial monitoring, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/audibert10a.html
J.-Y. Audibert, S. Bubeck, G. Lugosi, Regret in online combinatorial optimization, Mathematics of Operations Research 39(1), 2014. https://doi.org/10.1287/moor.2013.0598

12 thms1 active userReviewed

Algorithmic Game Theory Machine Learning Optimization·Captain: mikedeng1

Blackwell Approachability and No-Regret Learning are Equivalent 1: Any Approachability Algorithm Yields Online Linear Optimization with Regret/T at Most 2κ Times Its Approachability RateResearch Paper

Motivation

Online decision makers often have to choose an action before seeing the cost assigned to it. A no-regret algorithm performs almost as well, in total, as the best single action that could have been chosen after the costs were known. In a related repeated-game problem, Blackwell approachability asks a player to keep the average of vector payoffs close to a desired set despite an adversary's choices. These two performance criteria look different: one compares scalar costs to a fixed benchmark, while the other measures a geometric distance. Abernethy, Bartlett, and Hazan establish algorithmic reductions between them, with explicit finite-horizon bounds in their COLT 2011 paper. This mission isolates the direction that turns an approachability algorithm into an online linear optimization algorithm.

The bound matters even when the input algorithm has no known rate. It relates the regret of the resulting online algorithm to the actual distance attained on the corresponding sequence. Any subsequent guarantee on that distance then yields a regret guarantee through the same reduction. The paper also gives the reverse reduction and an application to calibrated forecasting; those are separate missions in this series.

Setting

Fix a dimension $d$ and a nonempty compact convex decision set $K\subseteq\mathbb R^d$ . On round $t$ , an algorithm selects $x_t\in K$ using only the preceding cost vectors $f_1,\ldots,f_{t-1}$ . The adversary then reveals $f_t$ in the Euclidean unit ball $B_2(1)$ . The incurred linear cost is $\langle f_t,x_t\rangle$ . For a horizon $T$ , regret compares these costs with the cost of the best single point of $K$ evaluated on all $T$ rounds:

\operatorname{Regret}_T = \sum_{t=1}^T\langle f_t,x_t\rangle - \min_{x\in K}\sum_{t=1}^T\langle f_t,x\rangle.

The minimum exists because $K$ is nonempty and compact. No probabilistic model for the cost sequence is assumed. The round index begins at one, and $x_t$ cannot depend on $f_t$ .

The reduction uses $\kappa=\max_{x\in K}\|x\|$ , the maximum norm of a decision. Write $a\oplus x$ for Euclidean concatenation of a scalar and a vector, an element of $\mathbb R^{d+1}$ . The generated cone of a set $M$ consists of its nonnegative scalar multiples, $\operatorname{cone}(M)=\{\alpha m:\alpha\ge0,\ m\in M\}$ . For a set $C$ , its polar cone is $C^0=\{\theta:\langle\theta,z\rangle\le0\text{ for every }z\in C\}$ . This negative-sign convention is fixed throughout the mission.

Algorithm 1 of the paper constructs a vector-payoff game. Its player actions are $K$ , its adversary actions are $B_2(1)$ , its payoff and target are

u(x,f)=\bigl(\langle f,x\rangle/\kappa\bigr)\oplus(-f), \qquad S=\operatorname{cone}(\{\kappa\}\times K)^0.

A Blackwell approachability algorithm for this game chooses each $x_t$ from the preceding adversary moves. Its finite-horizon approachability rate on a given sequence is $D_T(A)=\operatorname{dist}(T^{-1}\sum_{t=1}^T u(x_t,f_t),S)$ , where distance means the Euclidean distance from a point to a set. The online algorithm created by Algorithm 1 uses precisely the same choices $x_t$ .

Formalization targets

The goal is Theorem 16 of the paper. For every admissible history-based algorithm, every sequence of unit-ball costs, and every $T\ge1$ , it asserts

\frac{\operatorname{Regret}_T}{T}\le 2\kappa D_T(A).

This is a statement about the rate actually obtained on the chosen cost sequence. It assumes no upper bound on $D_T(A)$ and does not require an oracle call in the statement. Thus it also covers algorithms whose behavior is specified directly rather than through an implementation of the oracle.

The milestone targets are the distance formula of Lemma 13, the conic distance identity in display (8) of Theorem 16's proof, and the existence of a valid halfspace oracle in Lemma 15. Lemma 13 says distance to a nonempty convex cone equals the attained maximum of a linear functional over the polar cone's unit ball. Display (8) specializes this geometry to Algorithm 1's lifted target. Lemma 15 says that every halfspace containing that target admits a player action whose payoff remains in the halfspace against every permitted adversary move. Together these statements specify the geometry and the oracle needed by the reduction.

Significance

Theorem 16 gives a numerical transfer rule: a bound on approachability distance for Algorithm 1's game immediately bounds average regret for the same sequence. Its factor depends only on the size $\kappa$ of the decision set. This permits comparison of algorithms in a common finite-horizon language, without replacing the online cost sequence by a distribution or an asymptotic limit. The source paper uses this direction as one half of its equivalence between approachability and no-regret learning Abernethy, Bartlett, and Hazan, 2011.

The mathematical results are established in that paper; the goal here is a machine-checked Lean development of their statements and eventually their proofs. The mission also supplies reusable definitions of generated and polar cones, a Euclidean lift, a finite-history online algorithm, and regret over a compact decision set. Lemma 13 is useful outside this reduction whenever distance to a cone is compared with linear functionals on its polar. The proposed theorem items currently carry open proofs, while their statements and definition files are checked for elaboration in the pinned Lean environment.

Difficulty

The main obstacle is the change of viewpoint from a scalar regret comparison to distance from a set of lifted vector payoffs. A direct comparison of individual round costs does not describe that distance. The target is a polar cone in one additional Euclidean dimension, so a faithful account must keep the lift's geometry, the cone's sign convention, and the normalization by $\kappa$ aligned. The distance formula also asserts that its maximum is attained. An encoding that merely writes an infimum or supremum with default values can silently make an edge case look valid without representing the paper's claim.

The oracle milestone has a separate quantifier demand. One selected action must work against every adversary move for each halfspace containing the target. It cannot be replaced by a possibly different action for each move, or by a claim only about tangent halfspaces. The theorem includes halfspaces with arbitrary offsets and zero normals because the source oracle accepts any containing halfspace.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d), and $a\oplus x$ lives in EuclideanSpace ℝ (Fin (d+1)) with the Euclidean norm. The generated cone uses exactly one nonnegative multiple of a point of the generating set, as in Definition 11. The polar uses $\langle\theta,z\rangle\le0$ , the opposite sign from a positive dual-cone convention. Distances are Euclidean point-to-set distances. All arithmetic is over exact real numbers, and the regret minimum ranges over the image of the nonempty compact set $K$ .

The statements require $\kappa>0$ because the source payoff divides by $\kappa$ . This excludes the degenerate case $K=\{0\}$ , in which the source instance is undefined. They require $T\ge1$ wherever an average is formed. Admissible histories consist of unit-ball adversary moves, and each round's decision belongs to $K$ . The dimension may be zero syntactically, but the positive- $\kappa$ hypothesis excludes that case in results using Algorithm 1. These conditions keep the bound from being satisfied through Lean's default values for division by zero, distance to an empty set, or infima over empty sets.

The paper's display (8) writes $\operatorname{cone}(\kappa\oplus K)$ and labels its unit ball with dimension $d$ ; the formalization uses the cone of $\{\kappa\}\times K$ in $\mathbb R^{d+1}$ , matching Algorithm 1. Lemma 12's printed bipolar claim omits closedness; this mission does not use that uncorrected sentence as a milestone. The oracle statement covers all containing halfspaces. Contributions are welcome for the distance identity, the oracle existence result, and the final regret inequality, as well as geometric lemmas supporting those proofs.

Selected references

Jacob Abernethy, Peter L. Bartlett, and Elad Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, Proceedings of the 24th Annual Conference on Learning Theory, JMLR Workshop and Conference Proceedings 19, 2011, pp. 27–46. Published paper.

6 thms1 active userReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Introduction to the Scenario Approach III: The Risks of the Empirical Costs Follow an Ordered Dirichlet DistributionTextbook

Motivation

A scenario program replaces an uncertain optimization problem by its worst case over finitely many sampled instances. In its simplest form it reads

\min_{\nu\in\mathbb R^{d-1}}\Big[\max_{i=1,\dots,N}\ell(\nu,\delta_i)\Big],

where $\ell(\nu,\delta)$ is the cost of a decision $\nu$ when the uncertain parameter takes the value $\delta$ , and $\delta_1,\dots,\delta_N$ are independent draws from an unknown probability $\mathbb P$ . The classical guarantee of the scenario approach (Campi and Garatti, 2008) bounds the probability that a new instance produces a cost above the optimal value $\ell^*$ , and it does so without any knowledge of $\mathbb P$ .

That guarantee concerns a single number, $\ell^*$ . Two scenario programs with the same $N$ and the same optimal value can look very different at the solution: in one, most sampled costs lie just below $\ell^*$ ; in the other, they are widely scattered. The costs that do not determine the solution still carry information about how the cost of the chosen decision is distributed on future instances. Carè, Garatti and Campi (2015) showed that this information can be extracted with the same distribution-free character as the classical result, which is the subject of this mission. It is Chapter 8, §8.1 ("Probability box") of Campi and Garatti, Introduction to the Scenario Approach (SIAM/MOS 2018), the third mission of the series formalizing that book.

Timeline:

2008: Campi and Garatti prove that the violation of the scenario solution is dominated by a beta distribution $B(d,N-d+1)$ , with equality for fully supported problems (doi:10.1137/07069821X).
2015: Carè, Garatti and Campi prove that the risks of all empirical costs from index $d$ on have a joint ordered Dirichlet law (doi:10.1137/130928546).
2018: the book states the result as Theorem 8.4 and draws the probability box from it.

Setting

Let $\Delta$ be a measurable space with a probability $\mathbb P$ , and $\ell:\mathbb R^{d-1}\times\Delta\to\mathbb R$ a cost that is convex in $\nu$ for every $\delta$ (a standing assumption of the book). For a sample $(\delta_1,\dots,\delta_N)$ of independent draws from $\mathbb P$ , let $\nu^*$ be the solution of the program above and $\ell^*=\max_i\ell(\nu^*,\delta_i)$ its optimal value.

Empirical costs (Definition 8.1). Sort the costs of the solution on the sampled scenarios in decreasing order, $\ell^*_1\ge\ell^*_2\ge\dots\ge\ell^*_N$ ; so $\ell^*_1=\ell^*$ .

Risk (Definition 8.2). For a decision $\nu$ and a level $\ell$ , $R(\nu,\ell)=\mathbb P\{\delta:\ell(\nu,\delta)>\ell\}$ . The risk of the $k$ -th empirical cost is $R_k=R(\nu^*,\ell^*_k)$ , and $R_1\le R_2\le\dots\le R_N$ .

Nondegeneracy (Definition 8.3). For every $N\ge d$ , with probability $1$ , $\ell^*_d\ne\ell^*_{d+1}\ne\dots\ne\ell^*_N$ . Costs with index below $d$ are excluded because several scenarios typically attain the maximum at $\nu^*$ .

Support constraints and full support (Definitions 5.1 and 5.4). In epigraph form, $\min t$ subject to $t\ge\ell(\nu,\delta_i)$ , the constraint of scenario $i$ is a support constraint if removing it lowers the optimal value; the problem is fully supported if for every $m\ge d$ the program with $m$ scenarios has exactly $d$ support constraints with probability $1$ .

The ordered Dirichlet distribution with parameters $(d,1,\dots,1)$ is the law on $\{0\le\alpha_d\le\dots\le\alpha_N\le1\}$ with density $\frac{N!}{(d-1)!}\alpha_d^{d-1}$ .

Formalization targets

Goal: Theorem 8.4

Under nondegeneracy, for $N\ge d$ and all $\varepsilon_d,\dots,\varepsilon_N$ ,

\mathbb P^N\{R_d\le\varepsilon_d,\dots,R_N\le\varepsilon_N\}=\frac{N!}{(d-1)!}\int_0^{\varepsilon_d}\alpha_d^{d-1}\int_0^{\varepsilon_{d+1}}\!\!\cdots\int_0^{\varepsilon_N}\mathbf 1_{\{0\le\alpha_d\le\dots\le\alpha_N\le1\}}\,\mathrm d\alpha_N\cdots\mathrm d\alpha_d .

This is an identity of joint distribution functions, not a bound, and it does not depend on $\ell$ or $\mathbb P$ .

Milestones

Theorem 3.7 for the min-max program: $\mathbb P^N\{R(\nu^*,\ell^*)>\varepsilon\}\le\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ for $\varepsilon\in[0,1]$ .
Fully supported problems: $\ell^*=\ell^*_d$ with probability $1$ .
Marginal of $R_d$ (a corollary of the goal): $\mathbb P^N\{R_d\le\varepsilon\}=1-\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}$ , the beta law $B(d,N-d+1)$ .

Significance

The result. The theorem controls the whole distribution function of the cost $\ell(\nu^*,\delta)$ of the scenario solution on a new instance, not just one quantile of it. Discarding the extreme tails of the laws of $R_d,\dots,R_N$ yields, with a prescribed confidence $1-\beta$ , a region (the book's "probability box", Figure 8.2) that contains the entire cumulative distribution function of $\ell(\nu^*,\delta)$ , computed from the sample alone. The first marginal recovers the classical Theorem 3.7, since $\ell^*\ge\ell^*_d$ makes the risk of $\ell^*$ at most $R_d$ .

Formalizing it. The theorem is proved in Carè, Garatti and Campi (2015); the book states it and gives no proof. No machine-checked version of the scenario approach, of its generalization theorem, or of ordered Dirichlet laws of risks is known to exist. A formalization would produce a checked proof of the distribution-free identity together with the combinatorial and measure-theoretic infrastructure (order statistics of sampled costs, laws of random risks) that the rest of scenario theory reuses. The milestones separate the classical beta bound, which is also the goal of the first mission of this series, from the new exact joint law.

Difficulty

The obvious attempt treats $R_d,\dots,R_N$ as the order statistics of the uniform variables $1-F(\ell(\nu^*,\delta_i))$ . That works only for $d=1$ , when the decision space is a point and the costs are independent. For $d\ge2$ the decision $\nu^*$ is itself a function of the whole sample, so the sampled costs at $\nu^*$ are neither independent nor identically distributed, and the $d$ -th cost is tied to the scenarios that determine the solution. The factor $\alpha_d^{d-1}$ and the constant $N!/(d-1)!$ encode exactly this dependence. Any argument must account for which scenarios are active at $\nu^*$ without assuming full support, since the theorem holds whether or not $\ell^*=\ell^*_d$ .

Formalization scope

The decision space is EuclideanSpace ℝ (Fin n) and the book's $d$ is $n+1$ ; the sample is ω : Fin N → Δ with law Measure.pi (fun _ => P). Empirical costs are read from Tuple.sort with $k$ counted from $1$ ; risks are real numbers (P {δ | c < ℓ ν δ}).toReal. The right-hand side of the goal is a Lebesgue integral over the box $\prod_k[0,\varepsilon_k]$ intersected with the ordered simplex, stated for all real $\varepsilon_k$ . The solution map $\omega\mapsto\nu^*$ is a hypothesis-constrained function, never an arbitrary map.

Implicit hypotheses of the book pinned down in the binders:

$\ell(\cdot,\delta)$ is convex for every $\delta$ (p. 6).
Existence and uniqueness of the solution of the program for every sample size $m\ge1$ and every sample; the book's Assumption 3.6 says "every $m$ ", but the program with no scenario has no solution.
Nondegeneracy for every sample size $m\ge d$ , not only for the $N$ of the theorem, as Definition 8.3 is written.
Joint measurability of $(\nu,\delta)\mapsto\ell(\nu,\delta)$ and measurability of the solution map (measurability is glossed over in the book, p. 6 footnote 1 and p. 33).
$N\ge d$ , and $\varepsilon\in[0,1]$ in the binomial-form statements.

A statement in which the solution is an arbitrary measurable map, or in which the nondegeneracy or existence hypothesis is unsatisfiable, would make the goal vacuous; the hypotheses here are met, for example, by $\ell(\nu,\delta)=\|\nu-\delta\|^2$ with a continuous law on $\mathbb R^{n}$ , and for $d=1$ by any cost independent of $\nu$ with an atomless law.

A complete development needs: the scenario approach generalization theorem (reusable across this series), laws of order statistics of i.i.d. uniform variables, and the combinatorics of support sets of convex min-max programs. Proofs of the milestones, of the $d=1$ case of the goal, and of auxiliary facts about kthLargest are all welcome.

Selected references

M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM, 2018. doi:10.1137/1.9781611975444
A. Carè, S. Garatti, M. C. Campi, Scenario min-max optimization and the risk of empirical costs, SIAM J. Optim. 25(4):2061–2080, 2015. doi:10.1137/130928546
M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM J. Optim. 19:1211–1230, 2008. doi:10.1137/07069821X

10 thms1 active userReviewed

Machine Learning Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity III: Projected Subgradient Descent with η = R/(L√t) Satisfies f(average) − f(x*) ≤ RL/√tTextbook

Motivation

Many convex optimization problems in machine learning and statistics have objectives that are convex but not differentiable: hinge losses, $\ell_1$ penalties, maxima of finitely many affine functions, and the dual functions of Lagrangian relaxations. Methods that rely on gradients do not apply to them directly, while cutting-plane methods such as the ellipsoid method pay a price that grows with the dimension. The projected subgradient method replaces the gradient by an arbitrary subgradient and restores feasibility by a Euclidean projection. Its guarantee depends on the dimension only through two constants, a radius $R$ and a Lipschitz constant $L$ . This is the reason it, and its descendants (mirror descent, stochastic gradient descent, online gradient descent), are the standard tools for large-scale nonsmooth problems.

The rate analysed here goes back to the subgradient methods of Shor and Polyak in the 1960s and 1970s and to the lower bounds of Nemirovski and Yudin (1983). The book follows the presentation of Nesterov, Introductory Lectures on Convex Optimization (2004). The strongly convex variant with weights proportional to $s$ is from Lacoste-Julien, Schmidt and Bach (2012).

This mission is the third of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015), and covers the preamble of Chapter 3, Section 3.1 and Section 3.4.1.

Setting

Let $\mathbb R^n$ carry the Euclidean inner product $x^\top y$ and norm $\|\cdot\|$ . Let $\mathcal X\subseteq\mathbb R^n$ be compact and convex, and let $f$ be a convex function on $\mathcal X$ with a minimizer $x^*\in\mathcal X$ .

A vector $g$ is a subgradient of $f$ at $x\in\mathcal X$ if $f(x)-f(y)\le g^\top(x-y)$ for every $y\in\mathcal X$ . The set of subgradients at $x$ is written $\partial f(x)$ . The projection $\Pi_{\mathcal X}(y)$ of a point $y\in\mathbb R^n$ is the point of $\mathcal X$ nearest to $y$ .

Fix step sizes $\eta_s>0$ . Projected subgradient descent starts at some $x_1\in\mathcal X$ and iterates, for $s\ge1$ ,

y_{s+1}=x_s-\eta_s g_s,\quad g_s\in\partial f(x_s),\qquad x_{s+1}=\Pi_{\mathcal X}(y_{s+1}).

Any subgradient may be chosen at each step. In Section 3.1 the step is constant, $\eta_s=\eta$ . The set $\mathcal X$ lies in the Euclidean ball of radius $R$ centred at $x_1$ , and the subgradients have norm at most $L$ .

A function $f$ is $\alpha$ -strongly convex on $\mathcal X$ if $f(x)-f(y)\le g^\top(x-y)-\frac{\alpha}{2}\|x-y\|^2$ for all $x,y\in\mathcal X$ and $g\in\partial f(x)$ .

Formalization targets

Goal: Theorem 3.2

For every horizon $t\ge1$ , projected subgradient descent with the constant step $\eta=R/(L\sqrt t)$ satisfies

f\Big(\frac1t\sum_{s=1}^{t}x_s\Big)-f(x^*)\le\frac{RL}{\sqrt t}.

Milestones

Lemma 3.1. For $x\in\mathcal X$ and $y\in\mathbb R^n$ : $(\Pi_{\mathcal X}(y)-x)^\top(\Pi_{\mathcal X}(y)-y)\le0$ , already on the platform as a published theorem. The mission also states its consequence

\|\Pi_{\mathcal X}(y)-x\|^2+\|y-\Pi_{\mathcal X}(y)\|^2\le\|y-x\|^2 .

The per-step inequality in the proof of Theorem 3.2:

f(x_s)-f(x^*)\le\frac1{2\eta}\big(\|x_s-x^*\|^2-\|y_{s+1}-x^*\|^2\big)+\frac\eta2\|g_s\|^2 .

The summed inequality for any constant step $\eta>0$ :

\sum_{s=1}^{t}\big(f(x_s)-f(x^*)\big)\le\frac{R^2}{2\eta}+\frac{\eta L^2t}{2}.

Companion: Theorem 3.9

If $f$ is $\alpha$ -strongly convex and its subgradients are bounded by $L$ , then with $\eta_s=2/(\alpha(s+1))$ ,

f\Big(\sum_{s=1}^{t}\frac{2s}{t(t+1)}x_s\Big)-f(x^*)\le\frac{2L^2}{\alpha(t+1)}.

Significance

Theorem 3.2 gives an oracle complexity of $O(R^2L^2/\varepsilon^2)$ for reaching an $\varepsilon$ -optimal point, independent of the ambient dimension. Section 3.5 of the book shows this rate is unimprovable for black-box first-order methods once the dimension is large. Theorem 3.9 shows how strong convexity improves the rate to $O(1/t)$ , with the averaging weights changed from uniform to linear. These two bounds are the reference points against which the rest of Chapter 3 and Chapters 4 to 6 (smooth, accelerated, mirror, stochastic methods) are measured.

The results are classical and their proofs are short. Formalizing them produces a reusable, machine-checked account of the basic projected first-order step: the projection inequality, the one-step distance recursion, and the telescoping argument with Jensen's inequality for averaged iterates. To our knowledge, no machine-checked proof of the averaged-iterate bound for the projected subgradient method exists in Mathlib. Related platform items cover other algorithms or other averaging schemes.

Difficulty

The arithmetic is elementary, and the obvious argument works. The care is in the bookkeeping. The projection must be shown not to increase the distance to $x^*$ , which needs convexity of $\mathcal X$ and the variational characterization of the nearest point. The sum must telescope with a horizon-dependent constant step. Jensen's inequality must be applied to a finite convex combination of points of $\mathcal X$ , which requires showing that the average lies in $\mathcal X$ . In Theorem 3.9 the step sizes and the averaging weights are coupled, so neither can be changed independently. In Lean, the iterates are indexed from $1$ with natural-number horizons, and the bounds involve $\sqrt t$ , so these casts need care.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The iterates are sequences ℕ → EuclideanSpace ℝ (Fin n) with the first iterate at index $1$ . The projection is the published relation OnlineConvexOpt.FirstOrder.IsMetricProjection ( $x_{s+1}\in\mathcal X$ is a nearest point to $y_{s+1}$ ). Subgradients are taken relative to $\mathcal X$ (Definition 1.2). A run is a predicate on the steps $s=1,\dots,t$ , and every theorem holds for all runs, that is, for every choice of subgradients. Compactness and convexity of $\mathcal X$ , convexity of $f$ on $\mathcal X$ and the existence of the minimizer $x^*$ are the book's standing assumptions and appear as hypotheses. $R>0$ , $L>0$ and $\alpha>0$ are explicit, because Lean's division by zero would otherwise turn the step size into a junk value.

The book assumes $\|g\|\le L$ for every subgradient at every point of $\mathcal X$ . With subgradients relative to a compact $\mathcal X$ , that assumption can never hold at a boundary point, since every outward normal can be added to a subgradient. Stated that way the theorems would be vacuous. The mission therefore assumes the bound only for the subgradients $g_1,\dots,g_t$ that the run uses. This is a weaker hypothesis and gives a stronger, non-vacuous statement. Bounding only these subgradients is a deliberate choice, not a trivialization: the bound still constrains every quantity the conclusion depends on.

Contributions welcome: proofs of the four inequalities and of the two rates, and a reusable lemma that the convex combination of finitely many points of a convex set lies in the set, together with Jensen's inequality in the form used here.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. https://arxiv.org/abs/1405.4980
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
S. Lacoste-Julien, M. Schmidt and F. Bach, A simpler approach to obtaining an O(1/t) convergence rate for the projected stochastic subgradient method, 2012. https://arxiv.org/abs/1212.2002
N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer, 1985. https://doi.org/10.1007/978-3-642-82118-9

7 thms0 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity II: For t ≥ 2n² log(R/r) the Ellipsoid Method Satisfies f(x_t) − min f ≤ (2BR/r)·exp(−t/(2n²))Textbook

Motivation

The ellipsoid method is the cutting-plane algorithm that settled the polynomial-time solvability of linear programming and, more generally, of convex optimization over any set that comes with an efficient separation oracle. It was introduced for convex minimization by Shor and by Yudin and Nemirovski in the 1970s, and Khachiyan used it in 1979 to give the first polynomial-time algorithm for linear programming. Grötschel, Lovász and Schrijver later turned it into the general equivalence between separation and optimization that underlies much of combinatorial optimization.

This mission is the second of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980v2). Its goal is the convergence guarantee of the ellipsoid method, Theorem 2.4 (p. 250), together with the geometric lemma and the steps of the proof on which it rests.

Timeline:

1976–1977: Yudin–Nemirovski and Shor introduce the method for convex minimization.
1979: Khachiyan applies it to linear programming and obtains polynomial time.
1981: Grötschel, Lovász and Schrijver derive the equivalence of separation and optimization.

Setting

Write $\mathbb R^n$ for the space of real $n$ -vectors, with the dot product $x^\top y$ . An ellipsoid is a set

\mathcal E=\{x\in\mathbb R^n:(x-c)^\top H^{-1}(x-c)\le 1\},

where $c\in\mathbb R^n$ is its center and $H$ is a symmetric positive definite matrix.

A convex body $\mathcal X\subset\mathbb R^n$ is a compact convex set with non-empty interior. The objective $f$ is continuous and convex on $\mathcal X$ with values in $[-B,B]$ , and $r,R>0$ are such that $\mathcal X$ lies in the Euclidean ball $\mathcal E_0$ of center $c_0$ and radius $R$ and contains some Euclidean ball of radius $r$ . A subgradient of $f$ at $x\in\mathcal X$ is a vector $g$ with $f(x)+g^\top(y-x)\le f(y)$ for all $y\in\mathcal X$ .

The method starts from $\mathcal E_0$ , $H_0=R^2\mathrm I_n$ . At step $t\ge0$ it asks for a vector $w_t$ :

if $c_t\notin\mathcal X$ , a separating vector, with $\mathcal X\subset\{x:(x-c_t)^\top w_t\le0\}$ ;
otherwise a subgradient of $f$ at $c_t$ .

It then replaces $\mathcal E_t$ by the ellipsoid $\mathcal E_{t+1}$ given by

c_{t+1}=c_t-\frac1{n+1}\frac{H_tw_t}{\sqrt{w_t^\top H_tw_t}},\qquad H_{t+1}=\frac{n^2}{n^2-1}\Big(H_t-\frac2{n+1}\frac{H_tw_tw_t^\top H_t}{w_t^\top H_tw_t}\Big).

After $t$ iterations the output $x_t$ is the best of the queried centers that lie in $\mathcal X$ .

Formalization targets

Goal: Theorem 2.4

For $n\ge2$ and every $t\ge 2n^2\log(R/r)$ , $t\ge1$ , some queried center lies in $\mathcal X$ , and every output satisfies

f(x_t)-\min_{x\in\mathcal X}f(x)\le\frac{2BR}{r}\exp\Big(-\frac{t}{2n^2}\Big).

Milestones

The scalar inequality $(1+1/n)^2(1-1/n^2)^{n-1}\ge\exp(1/n)$ for $n\ge2$ (proof of Lemma 2.3, pp. 248–249).
Lemma 2.3 (p. 247): for $w\ne0$ the half-ellipsoid $\{x\in\mathcal E_0:w^\top(x-c_0)\le0\}$ lies in an ellipsoid $\mathcal E$ with

\mathrm{vol}(\mathcal E)\le\exp\Big(-\frac1{2n}\Big)\mathrm{vol}(\mathcal E_0),

and for $n\ge2$ the explicit ellipsoid (2.5)–(2.6) works. 3. The remark before Theorem 2.4 (p. 250): a point of $\mathcal X$ can leave the current ellipsoid only at a step with $c_t\in\mathcal X$ , and then its value exceeds $f(c_t)$ . 4. Two steps reused from Theorem 2.1 (pp. 246–247): $\mathrm{vol}(\mathcal X_\varepsilon)=\varepsilon^n\mathrm{vol}(\mathcal X)$ for $\mathcal X_\varepsilon=(1-\varepsilon)x^*+\varepsilon\mathcal X$ , and $f\le f(x^*)+2\varepsilon B$ on $\mathcal X_\varepsilon$ .

Significance

Theorem 2.4 bounds the oracle complexity of the ellipsoid method: accuracy $\varepsilon$ needs $O(n^2\log(1/\varepsilon))$ oracle calls. Each step costs $O(n^2)$ arithmetic operations plus one oracle call. With the separation oracles of linear and semidefinite programs this gives polynomial overall complexity (p. 250). The rate depends on the instance only through $\log(R/r)$ and $B$ , so the method needs no smoothness and no strong convexity. Lemma 2.3 is also the geometric step of the ellipsoid method for linear feasibility.

The result has a textbook proof. The work of this mission is to formalize it. The same update is published on the platform from Bertsimas and Tsitsiklis's Introduction to Linear Optimization (Theorem 8.1), with a proved volume factor of $\exp(-1/(2(n+1)))$ . That factor is weaker than (2.4)'s $\exp(-1/(2n))$ and does not give Theorem 2.4's constant. The sharper factor and the optimization version of the method (subgradient cuts, the output rule and the value bound) are not formalized on the platform.

Difficulty

There are two difficulties: Lemma 2.3 with the sharp constant, and the bookkeeping that turns per-step volume decrease into a value bound.

For the lemma, the volume of the explicit ellipsoid is $\big(n/\sqrt{n^2-1}\big)^n\sqrt{(n-1)/(n+1)}$ times that of $\mathcal E_0$ . Bounding it by $\exp(-1/(2n))$ rather than by the cruder $\exp(-1/(2(n+1)))$ needs the scalar inequality of milestone 1 for every $n\ge2$ . The reduction from a general ellipsoid to the unit ball also needs determinants under an affine map.

For the theorem, the obvious argument compares $\mathrm{vol}(\mathcal X_\varepsilon)$ with $\mathrm{vol}(\mathcal E_t)$ . This only works if no cut removes an optimal point and if every removed point of $\mathcal X$ is worse than a queried center. At the threshold $t=2n^2\log(R/r)$ the admissible $\varepsilon$ is exactly $1$ , so a non-strict volume bound alone does not close the argument there.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ with Lebesgue measure, as in the reused Bertsimas–Tsitsiklis ellipsoid definitions (LinearOptimization.ellipsoid, ellipsoidUpdateCenter, ellipsoidUpdateMatrix, IsSubgradientOn).
Euclidean balls are written with the dot product, because Mathlib's norm on Fin n → ℝ is the sup norm.
The method is a run predicate, IsEllipsoidRun. Every theorem holds for every admissible oracle answer. The update is the published one with $a=-w_t$ .
If an oracle answer is $w_t=0$ (possible only at a minimizer $c_t\in\mathcal X$ ), the run stops. The page's update would divide by zero there.

Conventions and hypotheses added to the page:

$n\ge2$ , because the update (2.6) is defined only for $n\ge2$ .
A minimizer $x^*$ exists (the book's standing assumption, p. 242).
The output ranges over the queried centers $c_0,\dots,c_{t-1}$ . The page writes $\{c_1,\dots,c_t\}$ , but $c_t$ has not been cut yet and $c_0$ has.
$t\ge1$ , because at $R=r$ and $t=0$ no center has been queried.

A run predicate whose separation branch does not require $\mathcal X\subset\{x:(x-c_t)^\top w_t\le0\}$ , or that accepts $w_t=0$ with an update, would make the statements false or vacuous. Both are excluded.

Lemma 2.3's volume factor is $\exp(-1/(2n))$ . The weaker published factor does not prove that milestone. The published theorem LinearOptimization.ellipsoid_update_halfspace_volume is included as a reference: it supplies the containment (2.3) and positive definiteness. Contributions are welcome on every milestone. A determinant formula for the volume of an ellipsoid would be reusable well beyond this mission.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2
N. Z. Shor, Cut-off method with space extension in convex programming problems, Cybernetics 13:94–96, 1977. doi:10.1007/BF01071394
D. B. Yudin and A. S. Nemirovski, Informational complexity and efficient methods for the solution of convex extremal problems, Matekon 13(2):22–45, 1976.
L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Mathematics Doklady 20:191–194, 1979.
M. Grötschel, L. Lovász and A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1:169–197, 1981. doi:10.1007/BF02579273
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 8.1).

11 thms0 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity I: The Center of Gravity Method Satisfies f(x_t) − min f ≤ 2B(1 − 1/e)^{t/n}Textbook

Motivation

Black-box convex optimization asks how many queries to an oracle are needed to minimize a convex function to accuracy $\varepsilon$ . In fixed dimension $n$ the answer is of order $n\log(1/\varepsilon)$ , and the first algorithm to attain it is the center of gravity method, discovered independently by Levin (1965) and Newman (1965). It is the opening example of cutting plane methods: algorithms that keep a set known to contain a minimizer and shrink it with one half-space per oracle call. The ellipsoid method and Vaidya's method, which underlie the polynomial-time solvability of linear programming and convex feasibility problems, follow the same template with cheaper sets. This mission is the first of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (2015), and covers its §2.1.

Timeline:

1960: B. Grünbaum proves that every half-space whose boundary passes through the centroid of a convex body in $\mathbb R^n$ contains at least a fraction $(n/(n+1))^n \ge 1/e$ of its volume.
1965: A. Levin and D. J. Newman independently introduce the center of gravity method and prove its linear rate.
1983: A. Nemirovski and D. Yudin show that $\Omega(n\log(1/\varepsilon))$ oracle calls are necessary for small $\varepsilon$ , so the method's oracle complexity is optimal.

Setting

Let $\mathcal X\subset\mathbb R^n$ be a convex body: a compact convex set with non-empty interior. Let $f:\mathcal X\to[-B,B]$ be continuous and convex, and let $x^*\in\mathcal X$ be a minimizer of $f$ on $\mathcal X$ . A vector $w$ is a subgradient of $f$ at $x\in\mathcal X$ if $f(x)-f(y)\le w^\top(x-y)$ for every $y\in\mathcal X$ . The first order oracle returns, at a query point, some subgradient there; the zeroth order oracle returns the value of $f$ .

For a set $\mathcal S$ of finite positive volume, its center of gravity is

c(\mathcal S)=\frac{1}{\mathrm{vol}(\mathcal S)}\int_{x\in\mathcal S}x\,dx .

The center of gravity method sets $\mathcal S_1=\mathcal X$ and, for $t\ge1$ , computes $c_t=c(\mathcal S_t)$ , queries the first order oracle at $c_t$ to obtain a subgradient $w_t$ , and sets

\mathcal S_{t+1}=\mathcal S_t\cap\{x\in\mathbb R^n:(x-c_t)^\top w_t\le0\}.

After $t$ steps it outputs $x_t\in\operatorname{argmin}_{1\le r\le t}f(c_r)$ , found with $t$ calls to the zeroth order oracle.

The Lean development names these objects IsConvexBody, IsSubgradientOn, centroid and IsCenterOfGravityRun in the namespace ConvexOptAlg.CenterGravity.

Formalization targets

Goal: Theorem 2.1 (p. 245)

For every run of the method and every $t\ge1$ ,

f(x_t)-\min_{x\in\mathcal X}f(x)\le 2B\Big(1-\frac1e\Big)^{t/n}.

Milestones (proof of Theorem 2.1, pp. 246–247)

Lemma 2.2 (Grünbaum). If $\mathcal K$ is centered, $\int_{\mathcal K}x\,dx=0$ , then for every $w\ne0$ ,

\mathrm{Vol}\big(\mathcal K\cap\{x:x^\top w\ge0\}\big)\ge\tfrac1e\,\mathrm{Vol}(\mathcal K).

(2.2). $\mathcal S_t\setminus\mathcal S_{t+1}\subset\{x\in\mathcal X:(x-c_t)^\top w_t>0\}\subset\{x\in\mathcal X:f(x)>f(c_t)\}$ , hence $x^*\in\mathcal S_t$ for every $t$ .
Volume decay. If $w_s\ne0$ for $s\le t$ , then $\mathrm{vol}(\mathcal S_{t+1})\le(1-1/e)^t\,\mathrm{vol}(\mathcal X)$ .
Shrunk copies. For $\varepsilon\in[0,1]$ and $\mathcal X_\varepsilon=\{(1-\varepsilon)x^*+\varepsilon x: x\in\mathcal X\}$ , $\mathrm{vol}(\mathcal X_\varepsilon)=\varepsilon^n\,\mathrm{vol}(\mathcal X)$ .
Values on shrunk copies. Every $x_\varepsilon\in\mathcal X_\varepsilon$ satisfies $f(x_\varepsilon)\le f(x^*)+2\varepsilon B$ .

Significance

Theorem 2.1 is a linear rate whose number of queries to reach accuracy $\varepsilon$ , $O(n\log(2B/\varepsilon))$ , depends on the dimension only linearly and on the accuracy only logarithmically, and matches the Nemirovski–Yudin lower bound. It is the reference point against which the ellipsoid method ( $O(n^2\log(1/\varepsilon))$ queries) and Vaidya's method are measured, and the randomized center of gravity method of §6.7 of the book rests on the same analysis. Grünbaum's inequality is a basic fact of convex geometry with uses well beyond optimization, for instance in the analysis of query complexity and of approximate centroid computations by random walks.

On the formal side, the theorem has been proved since 1965 and the lemma since 1960; neither is known to have a machine-checked proof. A complete development adds to Mathlib-based libraries the center of gravity of a set, the volume of homothetic images in the form used here, Grünbaum's inequality, and a reusable predicate for cutting plane runs. The later missions of this series (the ellipsoid method in particular) reuse the shrunk-copy argument of milestones 4 and 5.

Difficulty

The steps (2.2), the shrunk-copy volume and the value bound are short. The volume decay and the final comparison are bookkeeping once one knows that each cut keeps the method's sets convex bodies with positive volume. The difficulty is Lemma 2.2. A half-space through the centroid need not split the volume evenly: for a cone the smaller side tends to $1/e$ of the volume as $n\to\infty$ , so no symmetry argument works, and the bound must hold uniformly in the dimension. The classical proofs rely on tools of convex geometry, such as volume comparisons between a body and a symmetrized body, that are not available in Lean in the needed form. A second source of work is that the method's sets are defined through centroids: it has to be shown that they remain convex bodies of positive volume, so that each centroid is the genuine center of gravity, and this fact is not available before the volume estimates are.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; volumes are kept in $[0,\infty]$ in every statement. The function is a total map f : EuclideanSpace ℝ (Fin n) → ℝ with $|f|\le B$ , continuity and convexity required on $\mathcal X$ only; its values off $\mathcal X$ are irrelevant. Subgradients are relative to $\mathcal X$ (Definition 1.2). A run is a predicate on sequences indexed from $1$ ; the oracle's choice of subgradient is free, and every theorem holds for all runs. The minimizer $x^*$ is a hypothesis, as in the book's standing notation; it exists here by compactness. The output $x_t$ is any argmin, so the goal bounds the minimum $\min_{1\le r\le t}f(c_r)$ .

Added hypotheses, all disclosed in the statements: $n\ge1$ in the goal, because the exponent $t/n$ is undefined for $n=0$ ; and in Lemma 2.2, that the centered set is a convex body, because in Lean the integral of a non-integrable function is $0$ , which would make every unbounded convex set "centered". The milestone on volume decay assumes $w_s\ne0$ , which is the book's own reduction.

The center of gravity is defined with the real volume $\mathrm{vol}(\mathcal S)$ and is meaningless when that volume is $0$ or infinite. The run predicate does not assume the volumes are positive; that every set of a run is a convex body of positive volume is part of what has to be proved, and a formalization in which runs could degenerate to sets of zero volume, or in which the centroid is an arbitrary point, is not the book's method.

Contributions welcome: proofs of any item; a general Grünbaum inequality for convex sets of finite positive volume; lemmas on centroids (membership in the closed convex hull, translation behaviour) that later missions can reuse.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §2.1. https://arxiv.org/abs/1405.4980
B. Grünbaum, Partitions of mass-distributions and of convex bodies by hyperplanes, Pacific Journal of Mathematics 10(4):1257–1261, 1960. https://doi.org/10.2140/pjm.1960.10.1257
A. Yu. Levin, On an algorithm for the minimization of convex functions, Soviet Mathematics Doklady 6:286–290, 1965.
D. J. Newman, Location of the maximum on unimodal surfaces, Journal of the ACM 12(3):395–398, 1965. https://doi.org/10.1145/321281.321291
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

7 thms0 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization VI: The Moment Set U^CS Has Support Function μ̂ᵀv + Γ₁‖v‖ + √(1/ε − 1)‖Cv‖, an Upper Bound on the Worst-Case Value at RiskResearch Paper

Motivation

In robust optimization, a constraint is checked against every parameter value in an uncertainty set. This turns uncertainty into a deterministic optimization problem, but the set must be chosen carefully: a large set can make decisions unnecessarily conservative, while a small one can miss likely outcomes. Bertsimas, Gupta and Kallus use data to calibrate sets through statistical confidence regions. Their question is whether feasibility for every parameter in the set protects a decision against a fresh uncertain outcome with a specified probability. This mission treats the part of their construction based on estimated first and second moments. Bertsimas, Gupta and Kallus, §8.1.

The moment region originates in a concentration result attributed in the paper to Shawe-Taylor and Cristianini. That result bounds the distance between sample and population means and covariances when the uncertain vector is supported in a Euclidean ball. Bertsimas, Gupta and Kallus also discuss replacing those analytic thresholds with bootstrap thresholds; they describe the resulting coverage as approximate. The present target concerns the mathematical relation between a fixed moment region and its uncertainty set, leaving the statistical calibration of the thresholds to its cited source. Shawe-Taylor and Cristianini, 2003; Bertsimas, Gupta and Kallus, pp. 24–25.

Setting

Let the uncertain vector $\tilde u$ take values in $\mathbb R^d$ . A probability law $P$ belongs to the moment confidence region $\mathcal P^{CS}$ when it is supported in the Euclidean ball of radius $R$ , its mean $m_P$ is within $\Gamma_1$ of an estimate $\hat\mu$ , and its covariance $S_P$ is within $\Gamma_2$ of an estimate $\hat\Sigma$ in Frobenius norm. The covariance is $S_P=\mathbb E_P[\tilde u\tilde u^\top]-m_Pm_P^\top$ . The thresholds $\Gamma_1,\Gamma_2$ are nonnegative and can be chosen by either calibration procedure discussed in the paper. Bertsimas, Gupta and Kallus, Theorem 9 and (33).

For a vector $v$ , Value at Risk $\operatorname{VaR}^{P}_{\varepsilon}(v)$ is the smallest threshold $t$ for which $P(\tilde u^\top v\le t)\ge1-\varepsilon$ . The support function of a set $\mathcal U$ is $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$ . The authors construct the set

\mathcal U^{CS}_{\varepsilon} =\{\hat\mu+y+C^\top w:\|y\|_2\le\Gamma_1,\ \|w\|_2\le\sqrt{1/\varepsilon-1}\}, \qquad C^\top C=\hat\Sigma+\Gamma_2 I.

Here $0<\varepsilon<1$ is the allowed violation probability, $I$ is the identity matrix, and $C$ is a matrix factor of the adjusted covariance. The estimates and $C$ stay fixed while $\varepsilon$ varies. Bertsimas, Gupta and Kallus, (34)–(35).

Formalization targets

The first milestone bounds the quantile for every law in the moment region:

\operatorname{VaR}^{P}_{\varepsilon}(v)\le \hat\mu^\top v+\Gamma_1\|v\|_2+ \sqrt{\frac{1-\varepsilon}{\varepsilon}} \sqrt{v^\top(\hat\Sigma+\Gamma_2I)v} \quad(P\in\mathcal P^{CS}).

The second milestone evaluates the two linear maxima over the Euclidean balls in $\mathcal U^{CS}_{\varepsilon}$ and identifies $\|Cv\|_2$ with the quadratic form above. The goal, the deterministic part of Theorem 10, says the displayed bound equals $\delta^*(v\mid\mathcal U^{CS}_{\varepsilon})$ for every $v$ , while the set is nonempty, convex and compact. This gives the support-function criterion of Theorem 1 for each law in the region. A companion formalizes Theorem 13(a): the resulting support constraint is separately convex in $(v,t)$ and in $\varepsilon$ for $0<\varepsilon<3/4$ . Bertsimas, Gupta and Kallus, Theorems 10 and 13(a).

Significance

The support formula turns a distributional statement about an entire region of probability laws into a deterministic bound on a linear projection. It gives the robust model an explicit quantity to compare with a constraint threshold. The companion convexity result describes which risk levels allow separate convex optimization in the decision variables and the violation probability. Together they explain why the particular set in (35) is useful beyond the fact that it contains plausible uncertain vectors. Bertsimas, Gupta and Kallus, §§8.1 and 9.

The paper proves the mathematical construction and cites statistical results for the region's coverage. In Lean, the published Value-at-Risk and support-function definitions are already available, while this paper's moment region and set (35) need their own definitions. Formalizing the result therefore establishes a reusable interface between moment bounds, quantiles and set support. The theorem statements in this proposal are open proof targets; compiling them checks their types, not their proofs.

Difficulty

A bound on the mean and covariance does not directly bound a high quantile of every projection. The bound must work simultaneously for every probability law in the moment region, including discrete laws and singular covariances. The factor $\sqrt{(1-\varepsilon)/\varepsilon}$ is essential: replacing it by a standard deviation or a Gaussian quantile would change the claim. On the set side, the ordinary norm of a Lean function vector is a sup norm, whereas both balls in (35) are Euclidean. Getting the norm wrong changes the support function. Bertsimas, Gupta and Kallus, (34)–(35).

Formalization scope

Vectors are functions on Fin d, whose coordinates start at zero. enorm and frob explicitly compute the Euclidean and Frobenius norms. The ball-support condition in $\mathcal P^{CS}$ secures finite first and second moments; no density is assumed. The goal fixes $R\ge0$ , $\Gamma_1,\Gamma_2\ge0$ , $0<\varepsilon<1$ , and $C^\top C=\hat\Sigma+\Gamma_2I$ . This factor relation makes the quadratic form nonnegative; a separate positive-semidefinite assumption on $\hat\Sigma$ is unnecessary. The matrix need not be triangular because (35) and its support depend on $C^\top C$ . The uncertainty set's nonemptiness and compactness appear in the goal so the real support-function supremum cannot take Lean's default value for an empty or unbounded set.

Theorem 10's sampling claim is represented by its deterministic criterion for each $P\in\mathcal P^{CS}$ . The confidence-region coverage of Theorem 9 is cited, and the bootstrap coverage discussed on p. 25 is approximate; neither is asserted as an exact probability theorem here. Equation (34) prints an equality for a supremum over $\mathcal P^{CS}$ , yet that region restricts support to a ball, and the page does not establish attainment under that restriction. This mission uses the upper-bound direction needed for Theorem 10 and does not assert the equality or Remark 16's exact equivalence. The scope includes a sharp quantile bound, the exact support formula and the $3/4$ convexity range; a definition that merely makes the claim true by construction would miss these targets. Bertsimas, Gupta and Kallus, pp. 24–25 and 29.

Selected references

D. Bertsimas, V. Gupta and N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; revised in Mathematical Programming 167 (2018), 235–292. arXiv preprint.
J. Shawe-Taylor and N. Cristianini, Estimating the Moments of a Random Vector with Applications, 2003. University of Southampton ePrint.
G. C. Calafiore and L. El Ghaoui, On Distributionally Robust Chance-Constrained Linear Programs, Journal of Optimization Theory and Applications 130 (2006), 1–22. DOI.

6 thms0 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization V: The Order-Statistic Box U^M Built from Marginal Samples Dominates Value at Risk with Probability at Least 1 − αResearch Paper

Motivation

Robust optimization replaces an uncertain constraint $f(\tilde{\mathbf u},\mathbf x)\le 0$ by the requirement that it hold for every $\mathbf u$ in an uncertainty set $\mathcal U\subseteq\mathbb R^d$ . The resulting problems are tractable for many sets, but the choice of $\mathcal U$ decides whether the solution means anything probabilistically. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167:235–292, 2018) propose to build $\mathcal U$ from data so that, with high probability over the sample, every robust-feasible decision is also feasible with probability at least $1-\epsilon$ under the unknown distribution $\mathbb P^*$ .

This mission covers §6 of that paper, the case where the data are samples of the marginals of $\mathbb P^*$ , observed separately, with no assumption that the marginals are independent. This is the situation of asynchronous measurements or records with many missing entries: the joint law cannot be learned, yet a valid uncertainty set can still be built. The set is a box whose sides are order statistics, and its guarantee rests on an elementary binomial test (David and Nagaraja, Order Statistics, §7.1) and a Value-at-Risk bound of Embrechts, Höing and Juri (Finance Stoch. 7, 2003).

Setting

Let $\mathbb P^*$ be a probability measure on $\mathbb R^d$ whose support lies in a known box $[\hat{\mathbf u}^{(0)},\hat{\mathbf u}^{(N+1)}]=\{\mathbf u:\hat u^{(0)}_i\le u_i\le\hat u^{(N+1)}_i\}$ . Fix a violation level $0<\epsilon<1$ and a significance level $0<\alpha<1$ .

The Value at Risk of $\tilde{\mathbf u}^T\mathbf v$ under a probability measure $\mathbb P$ is

\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^T\mathbf v\le t)\ge1-\epsilon\},

and the support function of a set $\mathcal U$ is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^T\mathbf u$ . A set $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P^*$ if for every $f(\mathbf u,\mathbf x)$ concave in $\mathbf u$ and every $\mathbf x^*$ , $f(\mathbf u,\mathbf x^*)\le0$ for all $\mathbf u\in\mathcal U$ implies $\mathbb P^*(f(\tilde{\mathbf u},\mathbf x^*)\le0)\ge1-\epsilon$ .

From a sample $\hat{\mathbf u}^1,\dots,\hat{\mathbf u}^N$ let $\hat u^{(j)}_i$ , $1\le j\le N$ , be the $j$ -th order statistic (the $j$ -th smallest value) of coordinate $i$ , and let $\hat u^{(0)}_i,\hat u^{(N+1)}_i$ be the box ends. The index $s$ is

s=\min\Big\{k\in\mathbb N:\sum_{j=k}^N\binom Nj(\epsilon/d)^{N-j}(1-\epsilon/d)^j\le\frac{\alpha}{2d}\Big\},\qquad s=N+1\text{ if the set is empty}, \tag{26}

and the uncertainty set is the box

\mathcal U^M_\epsilon=\{\mathbf u\in\mathbb R^d:\hat u^{(N-s+1)}_i\le u_i\le\hat u^{(s)}_i,\ i=1,\dots,d\}. \tag{28}

The confidence region $\mathcal P^M$ is the set of probability measures on the box with $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(\mathbf e_i)\le\hat u^{(s)}_i$ and $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ for every $i$ .

Formalization targets

Goal: Theorem 7

If $N-s+1<s$ , then with probability at least $1-\alpha$ over the sample ( $N$ samples of each marginal of $\mathbb P^*$ , each marginal's samples i.i.d., arbitrary dependence across marginals),

\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)\qquad\text{for all }\mathbf v\in\mathbb R^d,

and, for every sample, $\mathcal U^M_\epsilon$ is nonempty, convex and compact with

\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)=\sum_{i=1}^d\max\big(v_i\hat u^{(N-s+1)}_i,\,v_i\hat u^{(s)}_i\big). \tag{29}

Milestones

Positive homogeneity: $\mathrm{VaR}^{\mathbb P}_\delta(c\mathbf w)=c\,\mathrm{VaR}^{\mathbb P}_\delta(\mathbf w)$ for $c>0$ (p. 10).
Each one-sided order-statistic test is valid at level $\alpha/(2d)$ : $\mathbb P^*_{\mathcal S}(\hat u^{(s)}_i<\mathrm{VaR}^{\mathbb P^*}_{\epsilon/d}(\mathbf e_i))\le\alpha/(2d)$ , and the mirror bound for $-\mathbf e_i$ with $\hat u^{(N-s+1)}_i$ (pp. 20–21).
Union bound: $\mathbb P^*_{\mathcal S}(\mathbb P^*\in\mathcal P^M)\ge1-\alpha$ (p. 21).
The weak Embrechts bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_i\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(v_i\mathbf e_i)$ for every probability measure $\mathbb P$ (p. 21).
If $N-s+1<s$ then $\hat u^{(N-s+1)}_i\le\hat u^{(s)}_i$ (p. 21).
(EC.8): for $\mathbb P\in\mathcal P^M$ , $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_{v_i>0}v_i\hat u^{(s)}_i+\sum_{v_i\le0}v_i\hat u^{(N-s+1)}_i$ (p. ec5).
(29) as a standalone statement (p. 21).

Significance

Theorem 7 gives an uncertainty set with a finite-sample guarantee from data that carry no information on the dependence between coordinates. The set is a box, so the robust counterpart of a linear constraint is again linear, and Remark 12 of the paper notes that separation over $\{(\mathbf v,t):\delta^*(\mathbf v\mid\mathcal U^M)\le t\}$ is in closed form. Unlike the other confidence regions of the paper (χ², G-test, Kolmogorov–Smirnov, bootstrap), whose coverage is asymptotic, tabulated or approximate, the test here is exact and distribution-free, so the probability statement itself is in scope.

The result is proved in the paper; to our knowledge none of it has a machine-checked proof. The mission produces a complete formal statement of Theorem 7 including the sampling probability, the binomial order-statistic test for a quantile, and the marginal Value-at-Risk bound, all of which are standard tools in nonparametric statistics and risk management that are absent from Mathlib.

Difficulty

The deterministic half, (EC.8) and (29), is short once the weak Embrechts bound is available. The work is in the probabilistic half, which the paper delegates to a textbook citation. Validity of the order-statistic test ties together facts that no library currently connects: the combinatorics of sorted tuples, the binomial law of the number of i.i.d. sample points below a threshold, the behaviour of a quantile at its left limit (the distribution function at the quantile can exceed $1-\epsilon/d$ , so the obvious bound uses the wrong probability), and the comparison of binomial tails across success probabilities. The lower-tail test must be handled with the index $N-s+1$ and the quantile of $-\tilde u_i$ , where a sign or off-by-one slip produces a false statement that still looks plausible. The boundary regime $s=N+1$ , where $\mathcal U^M_\epsilon$ is the a priori box, is valid only because $\mathbb P^*$ lives in that box and needs separate treatment.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ with 0-based coordinates; vectors pair by ⬝ᵥ. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$ applied to $\mathbf u\mapsto\mathbf u^T\mathbf v$ , and the support function is the published RobustMDP.Shared.supportFunction; both are real infima/suprema, genuine under $0<\epsilon<1$ , a probability measure, and a nonempty bounded set (the goal proves the latter). The order statistics use Mathlib's Tuple.sort; the index $N-s+1$ is N + 1 - s in natural numbers, which is the paper's value since $1\le s\le N+1$ .

The data are an array S : Fin N → Fin d → ℝ, S k i the $k$ -th sample of marginal $i$ , under any probability law Q such that, for each $i$ , the samples S 0 i, …, S (N-1) i are i.i.d. from the $i$ -th marginal of $\mathbb P^*$ (IsMarginalSampleLaw). The dependence between samples of different marginals is left arbitrary, as the paper's asynchronous setting requires; i.i.d. draws of whole vectors are one admissible law. Probabilities of possibly non-measurable events are outer measures. The level $\epsilon$ is fixed: by Remark 11 the family $\{\mathcal U^M_\epsilon\}$ need not work for all $\epsilon$ simultaneously.

The guarantee is stated in the criterion form of Theorem 1(a) of the paper: $\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)$ for all $\mathbf v$ , together with nonemptiness, convexity and compactness of $\mathcal U^M_\epsilon$ . Theorem 1 (mission I of this series) shows that for such sets this criterion is equivalent to implying a probabilistic guarantee. The coverage of the test is proved, not assumed: there is no hypothesis that $\mathbb P^*\in\mathcal P^M$ . A formalization in which the support function is evaluated on an empty or unbounded set, where the library value is 0, would make the criterion trivial; the nonemptiness and compactness conjunct of the goal rules it out.

Standing assumptions: $d\ge1$ , $0<\epsilon<1$ , $0<\alpha<1$ , $\hat{\mathbf u}^{(0)}\le\hat{\mathbf u}^{(N+1)}$ , $\mathbb P^*$ a probability measure with $\mathbb P^*$ -null complement of the box, and Theorem 7's hypothesis $N-s+1<s$ . The page prints the second condition of $\mathcal P^M$ as " $\mathrm{VaR}^{\mathbb P_i}_{\epsilon/d}\ge\hat u^{(N-s+1)}_i$ "; the formal region uses the lower-tail condition $\mathrm{VaR}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ that the hypothesis, its rejection rule and the proof use. (EC.8) is stated with " $\le$ " for each $\mathbb P\in\mathcal P^M$ ; the page's middle equality is not claimed.

Reusable infrastructure welcome beyond this mission: order statistics of tuples and the binomial law of threshold counts for i.i.d. samples; monotonicity of binomial tails in the success probability; the left-limit property of quantiles; the Embrechts-type subadditivity bound for Value at Risk.

Selected references

D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
H. A. David, H. N. Nagaraja, Order Statistics, Wiley (cited by the paper as 1970; third edition 2003), §7.1, distribution-free confidence intervals for quantiles. https://doi.org/10.1002/0471722162
P. Embrechts, A. Höing, A. Juri, Using copulae to bound the Value-at-Risk for functions of dependent risks, Finance and Stochastics 7:145–167, 2003. https://doi.org/10.1007/s007800200085

11 thms0 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization IV: The Forward–Backward Deviation Set U^FB Has a Closed-Form Support Function That Bounds the Worst-Case Value at RiskResearch Paper

Motivation

A robust linear constraint $u^\top v \le t$ with $u$ ranging over an uncertainty set $\mathcal U\subseteq\mathbb R^d$ is tractable whenever the support function $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$ is. Robust optimization gains a probabilistic meaning when $\mathcal U$ is chosen so that every robustly feasible decision also satisfies the constraint with probability at least $1-\varepsilon$ under the true distribution $\mathbb P^*$ of the uncertain parameter $\tilde u$ . Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets from data: a statistical hypothesis test yields a confidence region $\mathcal P$ of distributions, and the uncertainty set is any convex set whose support function dominates the worst-case Value at Risk over $\mathcal P$ .

Section 5.2 of the paper applies this schema to the forward and backward deviations of Chen, Sim and Sun (Oper. Res. 55, 2007), one-sided measures of spread that capture skewness. Chen, Sim and Sun assume the mean and deviations are known; the data-driven version replaces them by confidence intervals and must work out the worst case over those intervals. The result is the set $\mathcal U^{FB}_\varepsilon$ of Theorem 6, whose support function has a closed form.

Setting

The uncertain parameter $\tilde u$ takes values in $\mathbb R^d$ and $\mathbb P$ is its law. For $\varepsilon\in(0,1)$ and $v\in\mathbb R^d$ , the Value at Risk is

\mathrm{VaR}^{\mathbb P}_\varepsilon(v)=\inf\{t:\mathbb P(\tilde u^\top v\le t)\ge1-\varepsilon\}.

For a probability measure $\mathbb P_i$ on $\mathbb R$ with mean $\mu_i$ , the forward deviation and the backward deviation are

\sigma_f(\mathbb P_i)=\sup_{x>0}\sqrt{-\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{x\tilde u_i}]},\qquad\sigma_b(\mathbb P_i)=\sup_{x>0}\sqrt{\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{-x\tilde u_i}]}.

From a sample, a bootstrap produces thresholds $t_i$ , $\bar\sigma_{fi}$ , $\bar\sigma_{bi}$ . With the sample mean $\hat\mu_i$ put $m_{bi}=\hat\mu_i-t_i$ and $m_{fi}=\hat\mu_i+t_i$ . The confidence region $\mathcal P^{FB}$ consists of the distributions of vectors with independent components $\tilde u_i\sim\mathbb P_i$ , each $\mathbb P_i$ having bounded support, mean in $[m_{bi},m_{fi}]$ , $\sigma_f(\mathbb P_i)\le\bar\sigma_{fi}$ and $\sigma_b(\mathbb P_i)\le\bar\sigma_{bi}$ .

The uncertainty set is

\mathcal U^{FB}_\varepsilon=\Big\{y_1+y_2-y_3:\ y_2,y_3\in\mathbb R^d_+,\ \sum_{i=1}^d\Big(\frac{y_{2i}^2}{2\bar\sigma_{fi}^2}+\frac{y_{3i}^2}{2\bar\sigma_{bi}^2}\Big)\le\log(1/\varepsilon),\ m_{bi}\le y_{1i}\le m_{fi}\Big\}.

Formalization targets

Goal: Theorem 6

For $m_b\le m_f$ , $\bar\sigma_f,\bar\sigma_b>0$ and $\varepsilon\in(0,1)$ , the set $\mathcal U^{FB}_\varepsilon$ is nonempty, convex and compact,

\delta^*(v\mid\mathcal U^{FB}_\varepsilon)=\sum_{i:v_i\ge0}m_{fi}v_i+\sum_{i:v_i<0}m_{bi}v_i+\sqrt{2\log(1/\varepsilon)\Big(\sum_{i:v_i\ge0}\bar\sigma_{fi}^2v_i^2+\sum_{i:v_i<0}\bar\sigma_{bi}^2v_i^2\Big)}\qquad(24)

for every $v$ , and $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)$ is at most the right-hand side of (24) for every $\mathbb P\in\mathcal P^{FB}$ and every $v$ .

Milestones

The Chen–Sim–Sun bound (22): for independent components with known means $\mu_i$ and deviations, $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\sum_i\mu_iv_i+\sqrt{2\log(1/\varepsilon)(\sum_{v_i<0}\sigma_{bi}^2v_i^2+\sum_{v_i\ge0}\sigma_{fi}^2v_i^2)}$ .
The right-hand side of (24) is the worst case of (22) over the parameters allowed by $\mathcal P^{FB}$ .
Lagrangian strong duality for $\max_{u\in\mathcal U^{FB}_\varepsilon}u^\top v$ .
The three one-dimensional sub-subproblems and their optimal values.
The combined formula: $\delta^*$ equals a linear term plus $\inf_{\lambda>0}\{\lambda\log(1/\varepsilon)+S/(2\lambda)\}$ .
$\inf_{\lambda>0}\{\lambda L+S/(2\lambda)\}=\sqrt{2LS}$ , attained at $\lambda^*=\sqrt{S/(2L)}$ when $S>0$ .

Companions

Remark 9: when (24) exceeds $t$ , an explicit point of $\mathcal U^{FB}_\varepsilon$ gives a violated cut $u^\top v\le t$ .
Theorem 13(b): the constraint $\delta^*(v\mid\mathcal U^{FB}_\varepsilon)\le t$ is convex in $(v,t)$ and convex in $\varepsilon$ for $0<\varepsilon<1/\sqrt e$ .

Significance

Theorem 6 gives a data-driven uncertainty set for which a robust linear constraint is a second-order cone constraint, (24) being an explicit norm expression. By Theorem 1 of the paper, the domination of the worst-case Value at Risk over the region by the support function means that every robustly feasible solution satisfies a chance constraint at level $\varepsilon$ for every distribution in the region. Unlike the Chen–Sim–Sun set, which requires the true mean and deviations, $\mathcal U^{FB}_\varepsilon$ needs only data and allows the mean and the support to be unknown. Theorem 13(b) supports the alternating heuristic of §9 for choosing the levels $\varepsilon_j$ across several constraints.

The paper's proof is short and leans on "by inspection" and "by Lagrangian strong duality". A formal development makes each of these steps explicit, including the case where the multiplier is not attained, and corrects two printed slips (the optimal values $v_i\bar\sigma^2/(2\lambda)$ , which should be $v_i^2\bar\sigma^2/(2\lambda)$ , and the bound $m_b\le y_1\le m_b$ ). The Chen–Sim–Sun bound itself, a Chernoff-type tail bound under one-sided moment-generating conditions, is cited by the paper without proof. None of these results has a machine-checked proof that this mission is aware of.

Difficulty

The support function of (23) is a maximisation over a set defined by a box, two nonnegative orthants and one coupled quadratic constraint. A coordinate-wise argument does not apply directly because the quadratic budget is shared. The worst case over $\mathcal P^{FB}$ is not a single distribution: the extreme mean and the extreme deviations are chosen coordinate by coordinate according to the sign of $v_i$ . The Value at Risk bound needs independence of the components; without it (22) fails. When $v=0$ or the sign pattern makes the quadratic term vanish, the dual multiplier escapes to zero and the dual minimum is only an infimum.

Formalization scope

Vectors are Fin d → ℝ, with 0-based coordinates; $\tilde u^\top v$ is u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\varepsilon$ , and the support function is the published RobustMDP.Shared.supportFunction, a real supremum; the goal includes nonemptiness and compactness of $\mathcal U^{FB}_\varepsilon$ , so the supremum is a true maximum and cannot hold through the value $0$ of an empty or unbounded set.

The statement is formalized in the criterion form: $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\delta^*(v\mid\mathcal U^{FB}_\varepsilon)$ for all $v$ and every $\mathbb P$ in the region. By Theorem 1 (mission I of this series), for a nonempty convex compact set this criterion is equivalent to the probabilistic guarantee. The page's "with probability $1-\alpha$ with respect to the sample" is the coverage of the bootstrap confidence region, which the paper itself treats as approximate; it is not formalized.

Conventions and added hypotheses:

$\bar\sigma_{fi},\bar\sigma_{bi}>0$ , so that the denominators of (23) are genuine; with $\bar\sigma=0$ Lean's $x/0=0$ would leave $y_2$ unconstrained instead of forcing $y_2=0$ .
$m_b\le m_f$ , which holds because $t_i\ge0$ .
The region is built from a product measure (independence) of probability measures with bounded support. These are the hypotheses of Theorem 6 on $\mathbb P^*$ and the section's standing assumption; the page's set-builder for $\mathcal P^{FB}$ omits independence. Without bounded support, the Bochner integral of a non-integrable exponential is $0$ in Lean and the deviation conditions would lose their meaning.
" $\sigma_f(\mathbb P_i)\le\bar\sigma$ " is the predicate "the expression under the root is at most $\bar\sigma^2$ for every $x>0$ ", which is equivalent and avoids an unbounded supremum.
Dual minimisations over $\lambda\ge0$ are infima over $\lambda>0$ , stated with IsGLB.

A trivializing formalization is ruled out: a region without independence would make the goal false, a region without the probability and bounded-support conditions would let junk integrals satisfy the deviation predicates, and a support function of an empty set would make (24) a statement about $0$ .

The development needs a Chernoff argument for products of measures, finite-dimensional Lagrangian duality for one convex quadratic constraint (or a direct Cauchy–Schwarz argument), and compactness of the set (23). The definitions file is self-contained and reusable for other forward/backward-deviation sets. Proofs of any milestone, and of the Chen–Sim–Sun bound as a standalone tail inequality, are welcome.

Selected references

D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
X. Chen, M. Sim, P. Sun, A Robust Optimization Perspective on Stochastic Programming, Operations Research 55(6):1058–1071, 2007. https://doi.org/10.1287/opre.1070.0441

12 thms0 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization III: For Independent Marginals, the Kolmogorov–Smirnov Set U^I Has Support Function (19) and Bounds the Worst-Case Value at RiskResearch Paper

Motivation

A robust linear constraint $f(\mathbf u,\mathbf x)\le 0$ for all $\mathbf u\in\mathcal U$ replaces an uncertain parameter $\tilde{\mathbf u}$ by a deterministic uncertainty set $\mathcal U\subseteq\mathbb R^d$ . Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets directly from data. Their requirement is a probabilistic guarantee: every robust-feasible decision should satisfy the constraint with probability at least $1-\epsilon$ under the true distribution $\mathbb P^*$ , and this should hold with probability at least $1-\alpha$ over the sample. The construction runs a statistical hypothesis test, takes its confidence region of distributions, and turns the worst-case Value at Risk over that region into a set.

This mission covers the case where $\mathbb P^*$ may be continuous but its $d$ coordinates are known to be independent and supported in a known box (§5.1 of the paper). The test is the classical Kolmogorov–Smirnov (KS) goodness-of-fit test, applied separately to each marginal. The result is a convex set $\mathcal U^I_\epsilon$ whose support function has a one-dimensional closed form, (19). The set is representable with exponential cones, and a line search over a single multiplier separates over it (Remarks 6–7).

Setting

Let $d\ge 0$ and $N\ge 1$ (the sample size). For each coordinate $i$ we are given points $\hat u^{(0)}_i<\hat u^{(1)}_i<\cdots<\hat u^{(N)}_i<\hat u^{(N+1)}_i$ . The interval $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ is the known box containing the support, and $\hat u^{(1)}_i,\dots,\hat u^{(N)}_i$ are the order statistics of the $i$ -th coordinates of the data. Let $\Gamma=\Gamma^{KS}\in(0,1)$ be the KS threshold and $0<\epsilon<1$ .

The Value at Risk of $\mathbb P$ in direction $\mathbf v$ is $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^{\mathsf T}\mathbf v\le t)\ge 1-\epsilon\}$ .
The support function of a set is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^{\mathsf T}\mathbf u$ .
The KS region $\mathcal P^{KS}_i$ is the set of Borel probability measures $\mathbb P_i$ on $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ with $\mathbb P_i(\tilde u_i\le\hat u^{(j)}_i)\ge j/N-\Gamma$ and $\mathbb P_i(\tilde u_i<\hat u^{(j)}_i)\le (j-1)/N+\Gamma$ for $j=1,\dots,N$ .
The independent region $\mathcal P^I$ is the set of product measures $\prod_i\mathbb P_i$ with $\mathbb P_i\in\mathcal P^{KS}_i$ .
The vectors $q^L(\Gamma),q^R(\Gamma)\in\Delta_{N+2}$ of (17) are the two boundary distributions of the KS band. With $k=\lfloor N(1-\Gamma)\rfloor$ , $q^L$ puts mass $\Gamma$ at $j=0$ , mass $1/N$ at $j=1,\dots,k$ , and mass $1-\Gamma-k/N$ at $j=k+1$ . Its mirror image is $q^R_j=q^L_{N+1-j}$ .
The relative entropy is $D(\mathbf q,\mathbf p)=\sum_jq_j\log(q_j/p_j)$ .
The uncertainty set (18) is

\mathcal U^I_\epsilon=\Big\{\mathbf u:\exists\,\theta_i\in[0,1],\ \mathbf q^i\in\Delta_{N+2},\ \sum_{j=0}^{N+1}\hat u^{(j)}_iq^i_j=u_i,\ \sum_{i=1}^dD\big(\mathbf q^i,\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R\big)\le\log(1/\epsilon)\Big\}.

Formalization targets

Goal: Theorem 5 (deterministic content)

For every $\mathbf v\in\mathbb R^d$ :

\mathcal U^I_\epsilon\ \text{is nonempty, convex and compact},\qquad \mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)\ \ \forall\,\mathbb P\in\mathcal P^I,

\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)=\inf_{\lambda>0}\Big\{\lambda\log(1/\epsilon)+\lambda\sum_{i=1}^d\log\Big[\max\Big(\sum_{j}q^L_je^{v_i\hat u^{(j)}_i/\lambda},\sum_jq^R_je^{v_i\hat u^{(j)}_i/\lambda}\Big)\Big]\Big\}.\tag{19}

Milestones, in attack order

The Nemirovski–Shapiro bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\lambda\log(1/\epsilon)+\lambda\sum_i\log\mathbb E^{\mathbb P_i}[e^{v_i\tilde u_i/\lambda}]$ for independent, compactly supported marginals.
The boundary laws $q^L$ , $q^R$ belong to $\mathcal P^{KS}_i$ .
Theorem EC.2: for monotone $g$ , $\sup_{\mathcal P^{KS}_i}\mathbb E[g(\tilde u_i)]=\max(\sum_jq^L_jg(\hat u^{(j)}_i),\sum_jq^R_jg(\hat u^{(j)}_i))$ .
(16) combined with EC.2: the Value at Risk over $\mathcal P^I$ is at most the expression in (19), for every $\lambda>0$ .
The Lagrangian dual of $\max\{\mathbf v^{\mathsf T}\mathbf u:\mathbf u\in\mathcal U^I_\epsilon\}$ .
(EC.6): $\max_{\mathbf q\in\Delta}\{\mathbf c^{\mathsf T}\mathbf q-D(\mathbf q,\mathbf p)\}=\log\sum_jp_je^{c_j}$ .
(EC.7): the linear optimization over $\theta_i\in[0,1]$ is solved at an endpoint.

Significance

Theorem 5 gives a data-driven uncertainty set for continuous distributions with independent components. Its guarantee is finite-sample, not asymptotic, and its support function costs one line search over $\lambda$ to evaluate. Theorem 1 of the paper shows that $\mathrm{VaR}\le\delta^*$ for all $\mathbf v$ is equivalent to the probabilistic guarantee for nonempty convex compact sets. So the goal certifies that every robust-feasible solution of a constraint concave in $\mathbf u$ satisfies the chance constraint for every distribution the KS tests cannot reject. Theorem EC.2 is a reusable fact about KS bands: monotone expectations are extremized at the band's two boundary distributions.

The result is proved in the paper, but none of it has been formalized. A formal development would supply:

worst-case expectations over a KS confidence band;
the finite Gibbs variational identity with possibly vanishing reference masses;
a Chernoff-type Value-at-Risk bound for product measures;
a strong-duality statement for an entropy-constrained convex program.

Difficulty

The obvious route to the VaR bound is a union bound over coordinates. It loses a factor of $d$ in $\epsilon$ , which is why the paper uses exponential moments and independence instead. The KS region is infinite dimensional, so the inner supremum of (16) is not a finite linear program. Reducing it to the boundary distributions needs the monotonicity of $u\mapsto e^{v_iu/\lambda}$ , and a measure-level comparison of distribution functions against the band. The support-function identity needs strong duality for a jointly convex divergence constraint. The duality holds because $\theta_i\mapsto\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R$ is affine and $D$ is jointly convex. The reference vector can have zero entries (when $N(1-\Gamma)$ is an integer, or in the middle of the band), so the Gibbs step must handle vanishing masses.

Formalization scope

Data and conventions. Coordinates are Fin d. The points are uhat : Fin d → Fin (N + 2) → ℝ with the page's indices $j=0,\dots,N+1$ , and the KS constraints run over j : Fin N, which is the page's $j-1$ . The order statistics are data. They are ordered, $\hat u^{(0)}_i\le\hat u^{(1)}_i\le\dots\le\hat u^{(N+1)}_i$ (Monotone (uhat i)), as order statistics of a sample in the box are; ties are allowed.
Standing assumptions. $N\ge1$ , $0<\Gamma<1$ and $0<\epsilon<1$ .
Regions. Measures in $\mathcal P^{KS}_i$ are probability measures on $\mathbb R$ carried by the box, and $\mathcal P^I$ consists of the Measure.pi products of such measures, so independence is built in.
Relative entropy. $D$ carries an explicit finiteness predicate ( $q_j>0\Rightarrow p_j>0$ ), so Lean's log 0 = 0 cannot make an infinite divergence finite.
Published definitions. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$ , and $\delta^*$ is the published RobustMDP.Shared.supportFunction, a real sSup. The goal proves $\mathcal U^I_\epsilon$ nonempty and compact, so $\delta^*$ is never the junk value $0$ of an empty or unbounded set.
Infima and the multiplier. Infima over $\lambda$ are over $\lambda>0$ and stated with IsGLB. The page's $\lambda\ge0$ gives the same value.
Criterion form of the guarantee. The guarantee is stated as $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)$ for all $\mathbb P\in\mathcal P^I$ . By Theorem 1 (mission I of this series), this criterion is equivalent to the probabilistic guarantee for nonempty convex compact sets.
Coverage of the test. The statement "with probability at least $1-\alpha$ over the sample" is the coverage of $\mathcal P^I$ . It rests on the distribution-free law of the KS statistic (tables) and on combining $d$ tests at level $1-\sqrt[d]{1-\alpha}$ . This part is cited, not formalized.
Ruled out. The VaR inequality is never checked against a $\delta^*$ that sSup collapses to $0$ , and the divergence budget is never relaxed by unguarded logarithms.

Contributions are welcome on any milestone. Milestones 1, 3 and 6 are independent of each other and of the rest; the goal follows from milestones 1–7 together with the convex-analytic facts about $\mathcal U^I_\epsilon$ .

Selected references

D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
A. Nemirovski, A. Shapiro, Convex approximations of chance constrained programs, SIAM J. Optim. 17(4):969–996, 2006. https://doi.org/10.1137/050622328
M. A. Stephens, EDF statistics for goodness of fit and some comparisons, J. Amer. Statist. Assoc. 69(347):730–737, 1974. https://doi.org/10.1080/01621459.1974.10480196
S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/

11 thms0 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization II: With Known Finite Support, the χ² and G Uncertainty Sets Bound the Worst-Case Value at Risk over Their Confidence RegionsResearch Paper

Motivation

Robust optimization replaces uncertain data by a set of possible values and requires a decision to work for every value in that set. A central question is how to choose the set from data so that robust feasibility also gives a specified chance of satisfying the original constraint. Bertsimas, Gupta, and Kallus study this question for several sampling models in Data-Driven Robust Optimization. Their finite-support construction addresses a practical case: the uncertain vector can take one of finitely many known outcomes, while their probabilities must be inferred from observations. The resulting sets use classical goodness-of-fit tests to account for uncertainty in those probabilities. Bertsimas, Gupta, and Kallus, §§2–4, pp. 2–13.

In this case the support vectors are known in advance, so the problem is not to discover which outcomes are possible. The question is how much confidence to place in their estimated frequencies and how to turn that confidence region into a set of uncertain vectors suitable for a robust constraint. The paper gives two answers, one based on Pearson's chi-square statistic and one based on the likelihood-ratio, or G, statistic. Both answers are meant to work at every requested risk level $0<\epsilon<1$ for the same observed sample. Bertsimas, Gupta, and Kallus, Theorem 4, p. 13.

Setting

Let $a_0,\ldots,a_{n-1}\in\mathbb R^d$ be the listed possible outcomes. A probability vector $p=(p_j)$ belongs to the simplex $\Delta_n$ when all $p_j$ are nonnegative and $\sum_jp_j=1$ . It determines the finite-support law $P_p=\sum_jp_j\delta_{a_j}$ . From a sample one obtains the empirical frequencies $\hat p\in\Delta_n$ . A nonnegative number $\rho$ records the test threshold; in the paper it is $\chi^2_{n-1,1-\alpha}/(2N)$ , where $N$ is sample size and $\alpha$ is the test's significance level. Bertsimas, Gupta, and Kallus, (10), p. 12.

The Pearson confidence region $\mathcal P^{\chi^2}$ contains candidates $p\in\Delta_n$ satisfying $\sum_j(p_j-\hat p_j)^2/(2p_j)\le\rho$ . The G confidence region $\mathcal P^G$ instead requires $D(\hat p,p)\le\rho$ , with relative entropy $D(r,p)=\sum_jr_j\log(r_j/p_j)$ . In either region, a candidate $p_j=0$ is excluded when $\hat p_j>0$ : the source's divergence is then infinite. If both entries are zero, that coordinate contributes zero. These conventions matter because ordinary real division and logarithm in Lean have total values at zero. Bertsimas, Gupta, and Kallus, (10), p. 12.

For a direction $v\in\mathbb R^d$ , value at risk $\operatorname{VaR}^{P_p}_\epsilon(v)$ is the lower $1-\epsilon$ quantile of the scalar loss $u^{\mathsf T}v$ . Conditional value at risk is the minimum over real $t$ of $t+\epsilon^{-1}\sum_jp_j(a_j^{\mathsf T}v-t)^+$ . The paper's auxiliary set $U^{\operatorname{CVaR}_{P_p}}_\epsilon$ reweights the outcomes with another probability vector $q$ constrained by $q_j\le p_j/\epsilon$ . The two data-driven uncertainty sets $U^{\chi^2}_\epsilon$ and $U^G_\epsilon$ allow such a reweighting for some $p$ in the corresponding confidence region. Their support function $\delta^*(v\mid U)$ is the largest $u^{\mathsf T}v$ over $u\in U$ . Bertsimas, Gupta, and Kallus, (11)–(13), pp. 12–13; Theorem EC.1, p. ec2.

Formalization targets

The first target is the paper's finite-support CVaR identity and the comparison between the two risk measures:

\operatorname{VaR}^{P_p}_\epsilon(v) \le \operatorname{CVaR}^{P_p}_\epsilon(v) =\delta^*(v\mid U^{\operatorname{CVaR}_{P_p}}_\epsilon).

The goal is Theorem 4's deterministic claim, simultaneously for all $0<\epsilon<1$ . For each $p$ in the relevant confidence region, it asks for both bounds

\operatorname{VaR}^{P_p}_\epsilon(v)\le\delta^*(v\mid U^{\chi^2}_\epsilon), \qquad \operatorname{VaR}^{P_p}_\epsilon(v)\le\delta^*(v\mid U^G_\epsilon)

for every $v$ , with each uncertainty set nonempty, convex, and compact. A supporting milestone identifies each support function as the supremum of CVaR over its confidence region. The paper also displays conic optimization programs for these support functions in (14) and (15); those programs are outside this mission's drafted statements. Bertsimas, Gupta, and Kallus, Theorem 4, p. 13; proof, p. ec2.

Significance

The bounds give a way to certify the directional risk of every candidate distribution accepted by a goodness-of-fit test. For a nonempty convex compact uncertainty set, the paper's Theorem 1 turns this directional condition into a probabilistic guarantee for every constraint concave in the uncertain vector. Theorem 4 adds the sampling claim through coverage of the confidence region: when the true finite-support distribution belongs to that region, the whole family indexed by $\epsilon$ receives the guarantee. The statistical tests use chi-square approximations, so their advertised coverage is asymptotic rather than an exact finite-sample result. Bertsimas, Gupta, and Kallus, Theorems 1–4, pp. 10–13.

The paper proves the mathematical result. This mission asks for machine-checked proofs of its finite-dimensional definitions, the CVaR identity, the worst-case support identities, and the deterministic risk bounds. The drafted Lean statements are open goals. A completed development would also give reusable facts about finite-support risk measures and support functions under divergence-constrained probabilities. It would leave the test coverage calculation and the explicit programs (14)–(15) for separate work.

Difficulty

The risk comparison alone does not identify a robust uncertainty set: the support function must agree with the worst-case CVaR over an entire region of probability vectors. This brings a finite-dimensional optimization identity into the formal proof, including attainment and the relationship between reweightings and distributions. Boundary coordinates create another difficulty. The Pearson expression divides by $p_j$ , and the G expression contains $\log(\hat p_j/p_j)$ ; silently accepting Lean's values at zero would enlarge the regions and change the theorem. The support function and CVaR are real infima or suprema, so their nonempty, bounded domains must also be established. Bertsimas, Gupta, and Kallus, (10)–(13), pp. 12–13; proof, p. ec2.

Formalization scope

Lean represents outcomes and probability vectors as functions on Fin d and Fin n; indices start at zero. The simplex is Mathlib's stdSimplex. The law is a finite sum of point masses. If two listed vectors coincide, their point masses aggregate; the paper's notation $p_j=P_p(\tilde u=a_j)$ is recovered with the intended distinct listing. Value at risk and the support function reuse published Prove2Me definitions; the finite-vector relative entropy also reuses a published definition, guarded at zero in this mission's G region. CVaR uses a real sInf, equal to the paper's minimum for a simplex law and $0<\epsilon<1$ . No statement applies it outside that domain.

The goal assumes $\hat p\in\Delta_n$ and $\rho\ge0$ . These express, respectively, that the center is an empirical probability vector and that the chi-square threshold is nonnegative. It quantifies over every $0<\epsilon<1$ , with the same confidence regions for all levels. The paper's sample size, chi-square quantile, and significance level are compressed into $\rho$ ; coverage of the true distribution by the test is a separate statistical premise and is not formalized here. The source's $\mathbb P^*$ is represented by $P_{p^*}$ for a supported probability vector $p^*$ . The draft does not treat an arbitrary unsupported law as a member of the confidence region.

The nonempty and compact conclusions rule out a zero returned by a support function on an empty or unbounded set. The zero-denominator guards rule out candidates the paper assigns infinite divergence. Contributions needed to close the mission include finite-simplex geometry, the finite-support CVaR identity, continuity of the divergence regions at boundary coordinates, and the risk-bound theorem. Those facts can be reused in later data-driven robust optimization developments.

Selected references

Dimitris Bertsimas, Vishal Gupta, and Nathan Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; revised version in Mathematical Programming 167 (2018), 235–292. Preprint.

8 thms0 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Data-Driven Robust Optimization I: An Uncertainty Set Whose Support Function Dominates Value at Risk Implies a Probabilistic Guarantee for Every Concave ConstraintResearch Paper

Motivation

Robust optimization replaces an uncertain constraint $f(\tilde{\mathbf u},\mathbf x)\le 0$ , whose parameter $\tilde{\mathbf u}\in\mathbb R^d$ is random, by the requirement that the constraint hold for every $\mathbf u$ in a chosen uncertainty set $\mathcal U$ :

f(\mathbf u,\mathbf x)\le 0\qquad\forall\,\mathbf u\in\mathcal U .

The resulting problem is deterministic and, for many shapes of $\mathcal U$ , tractable (Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization, 2009). The modelling question it leaves open is how to choose $\mathcal U$ . A set that is too large makes every solution conservative; a set that is too small gives no protection. The practitioner's real requirement is usually probabilistic: a robust feasible $\mathbf x$ should violate the uncertain constraint with probability at most $\epsilon$ .

Bertsimas, Gupta and Kallus (Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167, 2018) build uncertainty sets directly from data so that this requirement holds with high confidence. Their whole construction rests on one characterization, Theorem 1 of the paper, of when a set carries such a guarantee. This mission formalizes that characterization and the two results (Theorems 2 and 3) that turn it into a data-driven recipe.

Earlier work used the "if" direction of the characterization for bi-affine constraints when designing sets for specific distributional assumptions (Ben-Tal et al., 2009; Chen, Sim and Sun, Oper. Res. 55, 2007). The extension to every constraint concave in $\mathbf u$ is due to Bertsimas, Gupta and Kallus.

Setting

Let $\mathbb P$ be a probability measure on $\mathbb R^d$ , the law of $\tilde{\mathbf u}$ , and fix a level $0<\epsilon<1$ . Throughout, $f(\mathbf u,\mathbf x)$ is concave in $\mathbf u$ for every value of the decision variable $\mathbf x\in\mathbb R^k$ .

The support function of a set $\mathcal U\subseteq\mathbb R^d$ is

\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^T\mathbf u,\qquad\mathbf v\in\mathbb R^d .

The Value at Risk of the linear loss $\tilde{\mathbf u}^T\mathbf v$ at level $\epsilon$ is

\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\ \mathbb P(\tilde{\mathbf u}^T\mathbf v\le t)\ge 1-\epsilon\}.

A set $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P$ (property (P2) of the paper) if for every $k$ , every $f(\mathbf u,\mathbf x)$ concave in $\mathbf u$ for each $\mathbf x\in\mathbb R^k$ , and every $\mathbf x^*\in\mathbb R^k$ ,

f(\mathbf u,\mathbf x^*)\le0\ \ \forall\mathbf u\in\mathcal U\quad\Longrightarrow\quad\mathbb P\big(f(\tilde{\mathbf u},\mathbf x^*)\le0\big)\ge1-\epsilon. \tag{2}

A function is bi-affine if it has the form $f(\mathbf u,\mathbf x)=\mathbf u^TF\mathbf x+\mathbf f_u^T\mathbf u+\mathbf f_x^T\mathbf x+f_0$ .

In the data-driven setting, $\mathbb P^*$ is unknown and a sample $\mathcal S=(\hat{\mathbf u}^1,\dots,\hat{\mathbf u}^N)$ is drawn i.i.d. from it. The paper's schema fixes $0<\alpha<1$ , takes the confidence region $\mathcal P(\mathcal S)$ of a hypothesis test at level $\alpha$ , and builds a closed convex set $\mathcal U(\mathcal S)$ whose support function bounds $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)$ for every $\mathbb P\in\mathcal P(\mathcal S)$ and every $\mathbf v$ .

Formalization targets

Goal: Theorem 1

(a) If $\mathcal U$ is nonempty, convex and compact and

\delta^*(\mathbf v\mid\mathcal U)\ge\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\qquad\forall\,\mathbf v\in\mathbb R^d,

then $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P$ .

(b) If $\mathcal U$ is nonempty and $\delta^*(\mathbf v\mid\mathcal U)<\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)$ for some $\mathbf v$ at which $\delta^*(\mathbf v\mid\mathcal U)$ is finite, then some bi-affine $f$ violates (2).

Milestones toward the goal

The proof in the electronic companion (EC.1.1) is a short chain, and its steps are the milestones: the attainment property of VaR, $\mathbb P(\tilde{\mathbf u}^T\mathbf v>\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v))\le\epsilon$ (already proved on the platform); a strict separating hyperplane between $\mathcal U$ and the superlevel set $\{f(\cdot,\mathbf x^*)\ge t\}$ ; the bound $\mathbb P(f(\tilde{\mathbf u},\mathbf x^*)\ge t)\le\epsilon$ for $t>0$ ; its limit $\mathbb P(f(\tilde{\mathbf u},\mathbf x^*)>0)\le\epsilon$ ; and, for part (b), the witness $f(\mathbf u,x)=\mathbf v^T\mathbf u-x$ at $x^*=\delta^*(\mathbf v\mid\mathcal U)$ .

Companions: Theorems 2 and 3

Theorem 2: with probability at least $1-\alpha$ over the sample, $\mathcal U(\mathcal S)$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P^*$ . Theorem 3: if the region does not depend on $\epsilon$ , then with probability at least $1-\alpha$ the whole family $\{\mathcal U(\mathcal S,\epsilon):0<\epsilon<1\}$ implies the guarantee simultaneously (a), and every $\mathbf x$ satisfying the level-optimized constraints (9) satisfies the joint chance constraint

\mathbb P^*\Big(\max_{j=1,\dots,m}f_j(\tilde{\mathbf u},\mathbf x)\le0\Big)\ge1-\bar\epsilon \tag{7}

(b).

Significance

Theorem 1(a) is what certifies every uncertainty set in the paper: the $\chi^2$ and $G$ sets for discrete distributions, the Kolmogorov–Smirnov and forward–backward sets for independent marginals, the marginal-sample box and the moment sets. Each construction reduces to proving one inequality between a support function and a Value at Risk, which is a statement about a single linear functional, and Theorem 1(a) lifts it to every concave constraint at once. Part (b) shows the condition cannot be dropped even for bi-affine constraints. Theorems 2 and 3 separate the statistical input (coverage of a confidence region) from the convex-analytic input (the support-function bound), and Theorem 3(b) is what allows the levels $\epsilon_j$ of a system of constraints to be optimized after seeing the data.

The results are proved in the paper. None of them has a machine-checked proof; the only formalized ingredient is the attainment property of VaR, which is on the platform as a proved theorem. The formalization provides a checked bridge from support-function bounds to probabilistic guarantees that the other missions of this series (II–VI) use to state their own results in the criterion form $\mathrm{VaR}\le\delta^*$ .

Difficulty

The informal argument is short; the difficulty is in the infinite-dimensional bookkeeping that the page leaves implicit. The superlevel set $\{f(\cdot,\mathbf x^*)\ge t\}$ need not be bounded, so the strict separation must use compactness of $\mathcal U$ alone. Closedness of this set and measurability of $\{f(\tilde{\mathbf u},\mathbf x^*)\le0\}$ depend on concave functions on $\mathbb R^d$ being continuous. The passage $t\downarrow0$ is continuity of a measure along an increasing union. The attainment of the infimum in the definition of VaR requires right-continuity of distribution functions. A naive attempt to separate $\mathcal U$ from the zero superlevel set $\{f\ge0\}$ directly fails, because the two sets may touch.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ; $\tilde{\mathbf u}$ is the identity map; $\mathbf v^T\mathbf u$ is the dot product u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$ , and the support function is the published RobustMDP.Shared.supportFunction. Both are real-valued sInf/sSup, which return $0$ on empty or unbounded sets, so every statement assumes $0<\epsilon<1$ , a probability measure, and an uncertainty set that is nonempty and compact (Theorem 1(a), Theorems 2–3) or nonempty with $\{\mathbf v^T\mathbf u:\mathbf u\in\mathcal U\}$ bounded above in the direction considered (Theorem 1(b)). In Theorem 1(b) and its witness this is the paper's own requirement that $\delta^*(\mathbf v\mid\mathcal U)$ be finite, which its strict inequality with a real VaR forces and its proof uses by treating $\delta^*(\mathbf v\mid\mathcal U)$ as a real number. Part (b) is printed with $\mathcal U^*$ , a slip for $\mathcal U$ ; the proof's separation step prints both inequalities in the same direction, a slip corrected in the strict separation milestone.

Property (P2) quantifies over the dimension $k$ of the decision variable, every function concave in $\mathbf u$ for each $\mathbf x$ , and every $\mathbf x^*$ . Restricting it to affine $f$ or to $k=0$ would trivialize part (a) and falsify part (b), and is ruled out by the definition.

In Theorems 2 and 3 the sample is Fin N → (Fin d → ℝ) with the product law Measure.pi; the confidence region and the uncertainty set are arbitrary maps of the sample, and the coverage $\mathbb P^*_{\mathcal S}(\mathbb P^*\in\mathcal P(\mathcal S))\ge1-\alpha$ is a hypothesis, never the conclusion's event. Step 2 of the schema is stated with $g=\delta^*(\cdot\mid\mathcal U(\mathcal S))$ directly. The sets are assumed nonempty and compact (Step 3 says closed and convex; a finite support function that bounds VaR forces nonemptiness and boundedness). Theorem 3(b) reads the levels $\epsilon_j$ in $(0,1)$ , where the family is defined. Probabilities of events in the sample space are outer measures, so no measurability hypotheses are needed.

A complete development needs strict separation of a compact convex set from a closed convex set (Mathlib's geometric_hahn_banach_compact_closed), continuity of concave functions on finite-dimensional spaces, and the attainment property of VaR. Contributions are welcome on all milestones; the separation and limit steps are reusable for any chance-constraint argument based on support functions.

Selected references

D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Mathematical Programming 167:235–292, 2018. https://arxiv.org/abs/1401.0212
A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
X. Chen, M. Sim, P. Sun, A Robust Optimization Perspective on Stochastic Programming, Operations Research 55(6):1058–1071, 2007. https://doi.org/10.1287/opre.1070.0441

12 thms0 active usersReviewed

Linear Optimization Operations Research·Captain: mikedeng1

Constructing Uncertainty Sets for Robust Linear Optimization 3: The Largest Centrally Symmetric Distortion Inner Approximation of a Polytope Solves a Linear ProgramResearch Paper

Motivation

A robust linear constraint $a'x \ge b$ for all $a \in \mathcal U$ protects a decision $x$ against every realization of the data $a$ in an uncertainty set $\mathcal U$ . Robust optimization took this form in the work of Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Oper. Res. Lett. 1999), where $\mathcal U$ is chosen by the modeller. Bertsimas and Brown (Oper. Res. 2009) tie the choice of $\mathcal U$ to the decision maker's attitude towards risk: on a finite sample $\mathcal A = \{a_1,\dots,a_N\}$ , a coherent risk measure constraint $\mu(\tilde a'x - b) \le 0$ is equivalent to a robust constraint over a convex set built from $\mathcal A$ , and for the distortion risk measures (the law-invariant, comonotone coherent measures, which include CVaR) that set is a polytope of a special kind, a permutohull.

An uncertainty set in practice is often an arbitrary polyhedron, given by the modeller or by previous analysis. Section 4.5 of the paper asks which distortion risk measure best approximates such a polyhedron from inside: the largest permutohull of a given shape contained in it. A positive answer quantifies how conservative a given polyhedral uncertainty set is relative to a distortion risk measure, and gives the risk measure that is closest to it. This mission is the third of a series of three on the paper; the first establishes the permutohull representation of distortion risk constraints, the second the generators of the centrally symmetric distortion measures.

Setting

Fix $N \ge 1$ and data $a_1,\dots,a_N \in \mathbb R^n$ , the columns of a matrix $A$ . Let $e_N \in \mathbb R^N$ have $1/N$ at each entry, so the sample mean is $\hat a = Ae_N$ .

The restricted simplex $\hat\Delta^N$ is the set of probability vectors $q \in \mathbb R^N$ with $q_1 \ge \dots \ge q_N$ . Under the uniform probability on $N$ points, the distortion risk measures are exactly the maps $\mu_q(X) = -\sum_i q_i x_{(i)}$ , $q \in \hat\Delta^N$ , with $x_{(1)} \le \dots \le x_{(N)}$ the ordered values of $X$ (Theorem 4.2 of the paper).
For $q \in \mathbb R^N$ , the $q$ -permutohull is $\Pi_q(\mathcal A) = \operatorname{conv}\{\sum_i q_{\sigma(i)} a_i : \sigma \in S_N\}$ . The robust constraint over $\Pi_q(\mathcal A)$ is the risk constraint for $\mu_q$ .
The symmetric restricted simplex $\hat\Delta^N_{\mathrm{sym}}$ is the set of $q \in \hat\Delta^N$ with $q = 2e_N - q_\sigma$ for some permutation $\sigma$ , where $(q_\sigma)_i = q_{\sigma(i)}$ . For these $q$ the permutohull is centrally symmetric about $\hat a$ .
With $\tilde\pi_q(\mathcal A) = \Pi_q(\mathcal A) - \hat a$ , the Minkowski functional

\|w\|_{q,\mathcal A} = \inf\{\alpha > 0 : w/\alpha \in \tilde\pi_q(\mathcal A)\}

measures $w = a - \hat a$ against the shifted permutohull (12).

The polyhedron is $\mathcal U = \{a \in \mathbb R^n : u_k'a \ge v_k,\ k = 1,\dots,m\}$ (14), with $\hat a \in \mathcal U$ .

The family of candidate inner approximations is obtained by mixing a fixed $\hat q \in \hat\Delta^N_{\mathrm{sym}}$ with the uniform generator: $q = \lambda\hat q + (1-\lambda)e_N$ , $\lambda \in \mathbb R$ .

Formalization targets

Goal: Theorem 4.5

Let $\lambda^*$ be the optimal value of the linear program

\max\ \lambda\quad\text{s.t.}\quad q = \lambda\hat q + (1-\lambda)e/N,\quad e'(s_k + t_k) \ge v_k\ \forall k,\quad s_{k,i} + t_{k,j} \le (u_k'a_j)\,q_i\ \forall i,j,k, \tag{15}

in $s_k, t_k, q \in \mathbb R^N$ and $\lambda \in \mathbb R$ , and $q^* = \lambda^*\hat q + (1-\lambda^*)e_N$ . Then

\Pi_{q^*}(\mathcal A) \subseteq \mathcal U,\qquad \Pi_{\lambda\hat q + (1-\lambda)e_N}(\mathcal A) \subseteq \mathcal U \implies \Pi_{\lambda\hat q + (1-\lambda)e_N}(\mathcal A) \subseteq \Pi_{q^*}(\mathcal A),

and, when $\hat q \ne e_N$ , $q^* \in \hat\Delta^N$ if and only if

\lambda^* \le \frac{1}{1 - N\hat q_{\min}}. \tag{16}

Milestones

Proposition 4.2: for $q \in \hat\Delta^N_{\mathrm{sym}}$ with $\Pi_q(\mathcal A)$ of nonempty interior, $\|\cdot\|_{q,\mathcal A}$ is a norm.
Scaling (proof of Lemma 4.2): $\Pi_{\lambda q + (1-\lambda)e_N}(\mathcal A) = \hat a + \lambda\,\tilde\pi_q(\mathcal A)$ for every $q \in \mathbb R^N$ , $\lambda \in \mathbb R$ .
Lemma 4.2: $\|a - \hat a\|_{\lambda q + (1-\lambda)e_N,\mathcal A} = \frac{1}{|\lambda|}\|a - \hat a\|_{q,\mathcal A}$ for $q \in \hat\Delta^N_{\mathrm{sym}}$ , $\lambda \ne 0$ .
Containment as linear constraints (proof of Theorem 4.5): $\Pi_q(\mathcal A) \subseteq \mathcal U$ iff vectors $s_k, t_k$ satisfying the constraints of (15) exist, for every $q \in \mathbb R^N$ .
Nonnegativity (proof of Theorem 4.5): for $\lambda \ge 0$ and $N\hat q_{\min} < 1$ , $\lambda\hat q + (1-\lambda)e_N \in \hat\Delta^N$ iff $\lambda \le 1/(1 - N\hat q_{\min})$ .

Significance

The theorem reduces a geometric question — the largest member of a one-parameter family of centrally symmetric polytopes, each with $N!$ potential vertices, that fits inside an arbitrary polyhedron — to a linear program with $O(mN)$ variables and $O(mN^2)$ constraints. Its solution identifies a distortion risk measure $\mu = \lambda^*\mu_{\hat q} + (1-\lambda^*)\mathbb E[-X]$ , which the paper reads as a mean–deviation measure in the style of a Sharpe ratio, and the bound (16) decides whether the optimal set is itself a distortion set or must be shrunk further.

The results are proved in the paper, with short proofs that pass over several points: the scaling identity is asserted, the duality step leaves the assignment-problem structure implicit, and the norm claim requires a nondegeneracy condition that the page does not state. No machine-checked proof of any of them is known. A formalization fixes the exact hypotheses (nonempty interior for the norm, $\lambda \ne 0$ in (13), $\hat q \ne e_N$ in (16)), and the containment equivalence for arbitrary real weight vectors $q$ is a reusable fact about permutohulls and assignment duality.

Difficulty

The goal combines three ingredients of different nature. The containment equivalence needs that minimizing a linear function over the permutohull is a linear program over the Birkhoff polytope of doubly stochastic matrices, followed by linear programming duality for that program; neither the Birkhoff–von Neumann theorem nor assignment duality is a one-line consequence of what is in Mathlib. The scaling identity is a statement about convex hulls under an affine map and holds for all real $\lambda$ , including the reflected case $\lambda < 0$ ; the maximality claim then needs the central symmetry of $\Pi_{\hat q}(\mathcal A)$ about $\hat a$ , which is a property of $\hat\Delta^N_{\mathrm{sym}}$ (Proposition 4.1 of the paper) and not of a general $q$ . The tempting shortcut — comparing gauges directly — fails at $\lambda = 0$ , where the permutohull is the single point $\hat a$ and the gauge is degenerate.

Formalization scope

Vectors in $\mathbb R^N$ and $\mathbb R^n$ are Fin N → ℝ and Fin n → ℝ, with $0$ -based indices; $a_i$ is a i, $u_k'a$ is a dot product. $\hat\Delta^N$ uses Mathlib's stdSimplex and Antitone. The permutohull is convexHull of the range over Equiv.Perm (Fin N), defined for every real $q$ because (15) evaluates it at mixtures with possibly negative entries. The Minkowski functional is Mathlib's gauge, which takes the value $0$ (not $+\infty$ ) on points no positive multiple of the set reaches; this is why Proposition 4.2 assumes $\Pi_q(\mathcal A)$ has nonempty interior and why the goal states "largest" as set containment. $\hat q_{\min}$ is $\min_i \hat q_i$ . The optimal value $\lambda^*$ is a hypothesis (it is the greatest element of the feasible set of (15)), not a supremum defined by sSup.

Standing assumptions and disclosed additions: $N \ge 1$ ; the polyhedron (14) is not assumed bounded (a generalization); in (13) the right-hand norm is that of $q$ , not $\tilde q$ as printed, and $\lambda \ne 0$ ; in (16), $N\hat q_{\min} < 1$ ; "corresponds to a distortion risk measure" is read, as the proof reads it, as $q^* \in \hat\Delta^N$ . A formalization that assumes $\Pi_{q^*}(\mathcal A) \subseteq \mathcal U$ or the maximality of $\lambda^*$ trivializes the theorem: both are conclusions, and the linear program enters only through its constraints and its optimal value.

A complete development needs: convex hulls under affine maps; the Birkhoff–von Neumann theorem (doubly stochastic matrices are convex combinations of permutation matrices); duality for the assignment linear program; gauge calculus for centrally symmetric convex bodies. The containment equivalence and the scaling identity are reusable beyond this mission. Proofs of any milestone, and of the Birkhoff and assignment-duality infrastructure, are welcome.

Selected references

D. Bertsimas and D. B. Brown, Constructing uncertainty sets for robust linear optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0646
A. Ben-Tal and A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
A. Ben-Tal and A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068

7 thms0 active usersReviewed

Convex Optimization

Missions

On Polyhedral Approximations of the Second-Order Cone II: A Lower Bound on the Size of Polyhedral ApproximationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.1, Eq. (13)

Milestones (claims of the proof, in order)

Significance

Difficulty

Formalization scope

Selected references

Robust Solutions to Least-Squares Problems with Uncertain Data IV: A Semidefinite Upper Bound on the Linear-Fractional Worst-Case Residual, Exact for Full PerturbationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.2 (corrected)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Path-Finding Methods for Linear Programming II: Properties of the Regularized D-Optimal-Design Weight FunctionResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (Properties of Weight Function), §V.A, p. 429

Milestones: the three bullets of Theorem 1

Significance

Difficulty

Formalization scope

Selected references

The Power of Convex Relaxation: Near-Optimal Matrix Completion I: Exact Nuclear-Norm Recovery with Quadratic Dependence on the RankResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.1, general-rank form (I.11)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Robust Solutions of Optimization Problems Affected by Uncertain Probabilities II: A Self-Concordant Barrier for the Perspective ConstraintResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 350)

Milestones (the displayed steps of the proof)

Significance

Difficulty

Formalization scope

Selected references

Robust Solutions of Optimization Problems Affected by Uncertain Probabilities I: The Robust Counterpart of a Linear Constraint under φ-Divergence UncertaintyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Introduction to Stochastic Programming VIII: Multistage Jensen Bounds and AggregationTextbook

Motivation

Setting

Formalization targets

Goal — Chapter 10, Theorem 1 (p. 419)

Significance

Difficulty

Formalization scope

Selected references

The Relaxation Method of Finding the Common Point of Convex Sets and Its Application to the Solution of Problems in Convex Programming 3: A Convergent Relaxation from Z Solves the Equality ProgramResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope