Operations Research

Completed

Convex Optimization Functional Analysis·Captain: mikedeng1

Optimization of Convex Risk Functions 2: On a Banach Lattice, a Proper Convex Monotone Risk Function Is Continuous and Subdifferentiable on the Interior of Its DomainResearch Paper

Motivation

Risk-averse stochastic optimization replaces the expected cost $\mathbb E[X]$ of an uncertain outcome $X$ by a risk function $\rho(X)$ : conditional value-at-risk, mean–semideviation and mean–upper-semideviation models, and the coherent and convex risk measures of Artzner, Delbaen, Eber and Heath and of Föllmer and Schied. Ruszczyński and Shapiro, Optimization of convex risk functions (Math. Oper. Res. 31, 2006), develop the convex analysis of such functions on general spaces of random variables, so that they can be used inside optimization problems $\min_{z\in S}\rho(F(z))$ .

Optimality conditions, duality and sensitivity analysis for such problems need two regularity properties of $\rho$ : continuity, and the existence of subgradients that are continuous linear functionals. For extended-valued convex functions on infinite-dimensional spaces neither comes for free. The standard sufficient condition, boundedness from above on a neighbourhood of a point (Ioffe and Tikhomirov), often cannot be used: the paper notes (p. 436) that the cone of nonnegative functions in $\mathcal L_p(\mathbb R^m,\mathcal B,\mu)$ , $p\in[1,+\infty)$ , $\mu$ a continuous probability measure, has empty interior. Section 3.1 shows instead that for monotone convex risk functions on a Banach lattice both properties follow from convexity and monotonicity alone. This mission formalizes that result, Proposition 3.1, and its $\mathcal L_p$ instance, Corollary 3.1.

Setting

Let $\mathcal X$ be a real vector space with a partial order $\succeq$ , and $\overline{\mathbb R}=[-\infty,+\infty]$ . Outcomes are costs: smaller is better. A function $\rho:\mathcal X\to\overline{\mathbb R}$ has domain $\operatorname{dom}\rho=\{X:\rho(X)<+\infty\}$ and is proper if $\rho(X)>-\infty$ for all $X$ and $\operatorname{dom}\rho\neq\emptyset$ . The paper's axioms used here are

(A1) convexity: $\rho(\alpha X+(1-\alpha)Y)\le\alpha\rho(X)+(1-\alpha)\rho(Y)$ for all $X,Y\in\mathcal X$ and $\alpha\in[0,1]$ ;
(A2) monotonicity: if $Y\succeq X$ then $\rho(Y)\ge\rho(X)$ .

A linear functional $l:\mathcal X\to\mathbb R$ , not necessarily continuous, is an algebraic subgradient of $\rho$ at $\bar X$ if

\rho(X)\ge\rho(\bar X)+l(X-\bar X)\qquad\forall X\in\mathcal X.\tag{3.1}

When $\mathcal X$ is a Banach space it carries its norm topology and is paired with its dual $\mathcal Y:=\mathcal X^*$ . The subdifferential $\partial\rho(\bar X)$ is the set of continuous $l\in\mathcal X^*$ satisfying (3.1), and $\rho$ is subdifferentiable at $\bar X$ if $\partial\rho(\bar X)\neq\emptyset$ .

A Banach lattice is a real Banach space $\mathcal X$ whose order makes it a lattice, compatible with addition, such that $|X_1|\le|X_2|$ implies $\|X_1\|\le\|X_2\|$ . Every $\mathcal L_p(\Omega,\mathcal F,\bar\mu)$ , $p\in[1,+\infty]$ , with the almost-everywhere order, is one.

In Lean everything lives in the namespace ConvexRiskFn.Cont: dom, IsProper, A1, A2, IsAlgSubgradient and subdiff are defined in the setting file.

Formalization targets

Goal: Proposition 3.1 (p. 437)

Let $\mathcal X$ be a Banach lattice and $\rho:\mathcal X\to\overline{\mathbb R}$ proper, satisfying (A1) and (A2). Then

\rho \text{ is continuous on } \operatorname{int}(\operatorname{dom}\rho), \qquad \partial\rho(\bar X)\neq\emptyset \ \text{ for every } \bar X\in\operatorname{int}(\operatorname{dom}\rho).

Milestones (the steps of the paper's argument, pp. 436–437)

At $\bar X\in\operatorname{int}(\operatorname{dom}\rho)$ the directional derivative $\delta(X)=\rho'(\bar X,X)=\lim_{t\downarrow0}(\rho(\bar X+tX)-\rho(\bar X))/t$ is finite, positively homogeneous and convex, and $\rho(X)\ge\rho(\bar X)+\delta(X-\bar X)$ .
$\rho$ has an algebraic subgradient at every $\bar X\in\operatorname{int}(\operatorname{dom}\rho)$ .
Under (A2) an algebraic subgradient is positive: $l(X)\ge0$ for $X\succeq0$ .
(Levin) Every positive linear functional on a Banach lattice is continuous.
If $l\in\partial\rho(\bar X)$ , then $\rho$ is lower semicontinuous at $\bar X$ .
(Phelps) A proper convex $\rho$ on a Banach space that is lower semicontinuous at every point of $\operatorname{int}(\operatorname{dom}\rho)$ is continuous there.

Companions

Corollary 3.1 (p. 437): for $\mathcal X=\mathcal L_p(\Omega,\mathcal F,\bar\mu)$ , $p\in[1,+\infty)$ , paired with $\mathcal L_q$ , the same conclusion, with subgradients represented by $g\in\mathcal L_q$ through $\int g\,(X-\bar X)\,d\bar\mu$ .
Real-valued case (p. 437): if moreover $\rho(X)<+\infty$ for every $X$ , then $\rho$ is continuous on all of $\mathcal X$ and subdifferentiable everywhere.

Significance

Proposition 3.1 removes lower semicontinuity from the list of assumptions a modeller has to check. In the paper's framework, the dual representation $\rho(X)=\sup_{\mu\in\mathcal A}\{\langle\mu,X\rangle-\rho^*(\mu)\}$ (Theorem 2.2) requires lower semicontinuity. The subdifferential formulas, the Hadamard directional differentiability of composite functions $\rho(F(z))$ and the optimality conditions of §§3.2 and 6 require continuity or subdifferentiability at the point of interest. On $\mathcal L_p$ spaces, Corollary 3.1 gives all of these on the interior of the domain from (A1) and (A2) alone, for example for real-valued convex monotone risk functions such as the mean–upper-semideviation and conditional value-at-risk models of §4.

The result is proved in the paper, so the formalization adds no new mathematics. It does add two classical functional-analytic facts that the paper cites without proof: automatic continuity of positive functionals on Banach lattices, and continuity of lower semicontinuous convex functions on open subsets of Banach spaces, here for extended-real-valued functions. As far as a search of Mathlib and of the platform shows, neither is formalized in this generality. Mathlib's continuity result for convex functions is finite-dimensional. Mathlib has the Hahn–Banach extension theorem but no theory of positive functionals on Banach lattices.

Difficulty

An algebraic subgradient exists at an interior point by Hahn–Banach applied to the directional derivative, and in a general Banach space it may be discontinuous. Continuity cannot come from local boundedness either: the usual criterion (bounded above near a point) is exactly what fails for natural examples, since positive cones in $\mathcal L_p$ , $p<\infty$ , have empty interior. The order structure has to do the work. Monotonicity forces the subgradient to be positive, and positivity forces continuity on a Banach lattice. That last step needs completeness and solidity of the norm. Without them, positive linear functionals need not be continuous, for example on the space of finitely supported sequences.

The second difficulty is passing from lower semicontinuity at each interior point to continuity on the interior. For a convex function this needs a Baire category argument on the Banach space, and completeness cannot be dropped.

Formalization scope

The Banach lattice is abstract: a type E with NormedAddCommGroup, NormedSpace ℝ, CompleteSpace, Lattice, HasSolidNorm (the solidity condition) and IsOrderedAddMonoid. This is the paper's definition, and it contains the paper's function spaces, so the formal goal is a generalization. Compatibility of the order with multiplication by nonnegative scalars is not assumed; it follows from these axioms.
$\overline{\mathbb R}$ is EReal. Convexity (A1) is written with EReal arithmetic, which agrees with the paper's for proper functions. Continuity on the interior is continuity of an EReal-valued function in the order topology. On the interior the function is finite, so this is ordinary continuity.
Subgradients in the goal are continuous linear functionals E →L[ℝ] ℝ, i.e. $\mathcal Y=\mathcal X^*$ . A version stating only an algebraic (possibly discontinuous) subgradient would be the easy half of the result and is not the goal; it is milestone 2.
The interior of the domain may be empty. The goal is then vacuous, as on the page. The domain is never assumed to be all of $\mathcal X$ , except in the real-valued companion, where the page assumes it.
Corollary 3.1 uses Mathlib's Lp ℝ p μbar (a.e. classes) with a finite measure $\bar\mu$ (the paper's measures are finite, p. 434) and $p\neq\infty$ . Its subgradient is a function $g$ with MemLp g q μbar for the Hölder conjugate $q$ , paired by the integral.
Needed infrastructure: one-sided directional derivatives of extended-valued convex functions, Hahn–Banach for sublinear functionals (exists_extension_of_le_sublinear in Mathlib), positive functionals on Banach lattices, and the Baire-category continuity theorem for convex lower semicontinuous functions. The last two are reusable well beyond risk functions. Contributions proving any milestone, or proving the Phelps or Levin step in greater generality, are welcome.

Selected references

A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
V. L. Levin, Convex Analysis in Spaces of Measurable Functions and Its Applications in Economics, Nauka, Moscow, 1985 (cited as [11]: Lemma 1.1, Theorem 0.12).
R. R. Phelps, Convex Functions, Monotone Operators and Differentiability, Lecture Notes in Mathematics 1364, Springer, 1989 (cited as [19]: Theorem 3.3).
A. D. Ioffe, V. M. Tihomirov, Theory of Extremal Problems, North-Holland, 1979 (cited as [9]).
P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072

9 thms2 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Primal and Dual Linear Decision Rules in Stochastic and Robust Optimization 2: With Random Recourse, the SDP (3.14) Conservatively Approximates the Linear Decision Rule Problem, Exactly for l = 1Research Paper

Linear decision rules for stochastic programs with random recourse

In a one-stage stochastic program a decision maker observes a random outcome $\xi$ and then picks a decision $x(\xi)$ , subject to constraints that depend on $\xi$ , so as to minimize expected cost. The optimization variable is a whole function $x$ , and computing the optimal value is #P-hard even for a uniform distribution on the unit cube (Dyer and Stougie, 2006, cited in the paper as [16, Theorem 3.2]). A standard tractable approximation, introduced for robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004) and carried to stochastic programming by Shapiro–Nemirovski and Chen–Sim–Sun, restricts decisions to linear decision rules $x(\xi)=X\xi$ . This restriction gives an upper bound on the optimal value.

Kuhn, Wiesemann and Georghiou (2009/2011) study these approximations systematically. Their §3 treats the case where the constraint matrix itself depends on $\xi$ (random recourse). Linear decisions then produce constraints that are quadratic in $\xi$ , and the paper reformulates the resulting semi-infinite problem as a semidefinite program. This mission formalizes that reformulation, the primal half of the paper's Theorem 2.

Setting

Uncertainty is a probability measure $\mathbb P$ on $\mathbb R^k$ , with outcomes $\xi$ . The support $\Xi$ of $\mathbb P$ is the smallest closed set of probability one. It is assumed to have the form

\Xi=\{\xi\in\mathbb R^k:\ e_1^\top\xi=1,\ \ \xi^\top W_\ell\xi\ge0,\ \ell=1,\dots,l\}\qquad(3.11)

for symmetric matrices $W_1,\dots,W_l$ , where $e_1$ is the first standard basis vector. The first coordinate of every outcome is therefore $1$ , so linear functions of $\xi$ are affine functions of the remaining coordinates. $\Xi$ is assumed nonempty and bounded, and its linear hull is assumed to be $\mathbb R^k$ . Let $\mathbb S$ denote the symmetric $k\times k$ matrices and $M=\mathbb E(\xi\xi^\top)$ the second-moment matrix.

The data are $C\in\mathbb R^{n\times k}$ (cost $c(\xi)=C\xi$ ), $B\in\mathbb R^{m\times k}$ (right-hand side $b(\xi)=B\xi$ , with rows $b_\mu^\top$ ), and $A_1,\dots,A_m\in\mathbb R^{k\times n}$ , where the $\mu$ th row of the recourse matrix $A(\xi)$ is $\xi^\top A_\mu$ . The stochastic program $\mathcal{SP}$ minimizes $\mathbb E(c(\xi)^\top x(\xi))$ over square-integrable $x$ subject to $A(\xi)x(\xi)\le b(\xi)$ almost surely. It is strictly feasible if some square-integrable $\bar x,\bar s$ and some $\varepsilon>0$ satisfy $A(\xi)\bar x(\xi)+\bar s(\xi)=b(\xi)$ and $\bar s(\xi)\ge\varepsilon e$ almost surely.

With linear decisions $X\xi$ and quadratic slacks $\xi^\top S_\mu\xi$ , $S_\mu\in\mathbb S$ , one obtains the primal approximation

\mathcal{SP}^u:\quad \min\ \operatorname{Tr}(MC^\top X)\ \ \text{s.t.}\ \ \xi^\top A_\mu X\xi+\xi^\top S_\mu\xi=b_\mu^\top\xi,\ \ \xi^\top S_\mu\xi\ge0\ \ \mathbb P\text{-a.s.},\ \mu=1,\dots,m,

and the SDP (3.14)

\min\ \operatorname{Tr}(MC^\top X)\ \ \text{s.t.}\ \ \tfrac12(A_\mu X+X^\top A_\mu^\top)+S_\mu=\tfrac12(e_1b_\mu^\top+b_\mu e_1^\top),\ \ S_\mu-\textstyle\sum_\ell\Lambda_{\mu\ell}W_\ell\succeq0,\ \ \Lambda\ge0 .

Formalization targets

Goal: Theorem 2, primal half (p. 17)

\operatorname{Feas}(3.14)\ \text{projects into}\ \operatorname{Feas}\mathcal{SP}^u,\qquad \operatorname{val}\mathcal{SP}^u\le\operatorname{val}(3.14),

l=1\ \text{and}\ \mathcal{SP}\ \text{strictly feasible}\ \Longrightarrow\ \operatorname{val}\mathcal{SP}^u=\operatorname{val}(3.14).

Milestones

§3.2, (3.13), p. 12. The $\mu$ th equality constraint of $\mathcal{SP}^u$ holds almost surely if and only if $H_\mu:=\tfrac12(A_\mu X+X^\top A_\mu^\top-e_1b_\mu^\top-b_\mu e_1^\top)+S_\mu=0$ .
Lemma 1 (S-lemma), p. 12. If $\bar\xi^\top W\bar\xi>0$ for some $\bar\xi$ , then $[\xi^\top W\xi\ge0\Rightarrow\xi^\top S\xi\ge0]\iff\exists\lambda\ge0:\ S\succeq\lambda W$ . This is linked to the platform's proved S-procedure, of which it is the homogeneous case.
Proposition 6, p. 12. For symmetric $S$ : $\exists\lambda\ge0$ with $S-\sum_\ell\lambda_\ell W_\ell\succeq0$ implies $\xi^\top S\xi\ge0$ almost surely, and the converse holds when $l=1$ .

Significance

The theorem replaces a problem with infinitely many constraints, one per outcome, by a semidefinite program with $O(mk^2+ml)$ variables. Its value is always an upper bound on $\mathcal{SP}^u$ , and hence on $\mathcal{SP}$ . When the support is a single ellipsoid in the hyperplane $e_1^\top\xi=1$ ( $l=1$ ), the bound loses nothing beyond the restriction to linear decisions. For $l>1$ the gap is unavoidable in general: an exact tractable reformulation would decide copositivity, which is NP-hard (Remark 7). Random recourse arises whenever technology or yield coefficients are uncertain, for example in production planning and portfolio problems with uncertain returns.

The result is proved in the paper. As far as is known it has no machine-checked proof. A formalization adds a precise statement of the hypotheses. Writing those hypotheses out showed that the unnumbered §3.2 step needs $\Xi$ to have dimension $k-1$ , which spanning alone does not give for nonconvex $\Xi$ (see Formalization scope). The other half of Theorem 2, about the lower-bounding SDP (3.18), is false in this preprint and is not part of the mission.

Difficulty

The semi-infinite constraints hold only $\mathbb P$ -almost surely. The first step is to pass from "almost surely" to "for every $\xi\in\Xi$ ", which uses that $\Xi$ is exactly the support and that the constraint functions are continuous. A bound $\mathbb P(\Xi)=1$ alone is not enough. For the equality constraints, a quadratic form that vanishes on $\Xi$ must vanish identically. This requires $\Xi$ to be large enough, and the obvious argument from " $\Xi$ spans $\mathbb R^k$ " fails when $\Xi$ is a finite set. For the inequality constraints with $l=1$ , the implication $\xi^\top W_1\xi\ge0\Rightarrow\xi^\top S\xi\ge0$ must be established on all of $\mathbb R^k$ and not only on the slice $e_1^\top\xi=1$ . Doing so needs boundedness of $\Xi$ (no recession directions) and a strictly feasible point for the S-lemma. The S-lemma itself is a nonconvex duality statement. It is available on the platform.

Formalization scope

Outcomes live in Fin k → ℝ, with $k\ge1$ carried in the setting. Indices are 0-based: $\xi_1$ is coordinate 0, and $\mu,\ell$ range over Fin m, Fin l. " $\Xi$ is the support of $\mathbb P$ " is stated as: $\Xi$ is closed, $\mathbb P(\Xi^{\mathrm c})=0$ , and every ball centred in $\Xi$ has positive measure. Mathlib has no Measure.support at this revision. The standing assumptions (probability measure, symmetric $W_\ell$ , support, nonempty, bounded, spanning) form one predicate assumed by every theorem. Decision rules are Borel measurable square-integrable functions. Optimal values are infima in EReal, $+\infty$ for an empty feasible set and $-\infty$ for an unbounded one. "Equivalent" means equal optimal values. Each $S_\mu$ is required symmetric in both problems; $\succeq$ is positive semidefiniteness and $\Lambda\ge0$ is componentwise. Strict feasibility of $\mathcal{SP}$ in §3 is the paper's condition (2.9) of §2 with $A$ replaced by $A(\xi)$ . The paper uses the phrase without restating it.

Repairs and narrowings:

Only the clauses of Theorem 2 about (3.14) and $\mathcal{SP}^u$ are stated. The clauses about (3.18) and $\mathcal{SP}^l$ are false in this preprint: a strictly feasible instance with $l=1$ has $\operatorname{val}(3.18)\approx1.170>\ln3=\operatorname{val}\mathcal{SP}$ . Propositions 7–9 serve only that half and are not included. "Polynomial size, efficiently solvable" is informal and omitted.
The §3.2 milestone carries the extra hypothesis that $\Xi$ contains a relatively open piece of the hyperplane $e_1^\top\xi=1$ (the paper's "dimension $k-1$ ", p. 10). Without it the claim is false for $l\ge2$ . For $l=1$ the hypothesis follows from the standing assumptions, so the goal is unaffected.
Strict feasibility is kept in the $l=1$ clause as printed, although the argument does not use it.

The goal cannot be trivialized through its definitions. Feasibility is quantified $\mathbb P$ -almost surely for a measure whose support is $\Xi$ , not over an empty or arbitrary set. Both optimal values are infima of the same real objective over the problems' own feasible sets. The standing assumptions are satisfiable, for instance by $k=2$ , $W_1=\operatorname{diag}(1,-1)$ , and $\mathbb P$ the uniform law on $\{1\}\times[-1,1]$ .

The definitions (support of a measure, $\mathcal L^2$ decision rules, the random-recourse data) are reusable for the other sections of the paper and for related work on decision rules. Proofs of any milestone, Lean lemmas on quadratic forms vanishing on open cones, and an almost-sure-to-support transfer lemma are welcome.

Selected references

D. Kuhn, W. Wiesemann, A. Georghiou, Primal and dual linear decision rules in stochastic and robust optimization, Optimization Online 2009/02/2218 (2009); Math. Program. 130 (2011) 177–209. https://optimization-online.org/wp-content/uploads/2009/02/2218.pdf, https://doi.org/10.1007/s10107-009-0331-4
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM Studies in Applied Mathematics 15, 1994 (the paper's source for Lemma 1). https://doi.org/10.1137/1.9781611970777
S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004, Appendix B (the S-procedure as stated on the platform). https://web.stanford.edu/~boyd/cvxbook/
I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007) 371–418. https://doi.org/10.1137/S003614450444614X
M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Math. Program. 106 (2006) 423–432. https://doi.org/10.1007/s10107-005-0597-0

7 thms2 active usersReviewed

Completed

Convex Optimization Functional Analysis·Captain: mikedeng1

Optimization of Convex Risk Functions 1: Dual Representation of a Lower Semicontinuous Convex Risk Function, with Monotonicity, Translation Equivariance and Homogeneity Read Off Its Dual DomainResearch Paper

Motivation

A risk function assigns to an uncertain cost $X$ (a function of the random state $\omega$ ) a single number $\rho(X)$ that a decision maker can minimize. Artzner, Delbaen, Eber and Heath (Math. Finance 9, 1999) singled out four axioms, convexity, monotonicity, translation equivariance and positive homogeneity, and called real-valued functions satisfying all four coherent. Föllmer and Schied (Finance Stoch. 6, 2002) and Frittelli and Rosazza Gianin dropped homogeneity to obtain convex risk measures. In each of these works, a central result is a dual representation: the risk function is a supremum of expectations under a family of probability measures, possibly with a penalty.

Ruszczyński and Shapiro (Math. Oper. Res. 31, 2006) place these representations inside general conjugate duality. Their Theorem 2.2 shows that, for any proper, lower semicontinuous, convex risk function on a locally convex space of measurable functions paired with a space of signed measures, the representation holds over the domain of the conjugate, and each remaining axiom corresponds exactly to a property of the measures in that domain. The paper then builds its optimization theory (subdifferentials of composite risk functions, optimality conditions, duality for nonanticipativity constraints) on this representation.

Timeline. Artzner et al. (1999): the coherent axioms, with a representation for finite $\Omega$ . Delbaen (2002): coherent measures on $L^\infty$ under the Fatou property. Föllmer–Schied (2002): convex risk measures on bounded functions. Cheridito, Delbaen and Kupper (2004): spaces of processes. Rockafellar, Uryasev and Zabarankin (2002–2006): the risk envelope in $\mathcal L_2$ . Ruszczyński–Shapiro (2006): the general paired-space statement formalized here.

Setting

Outcomes are costs: smaller values of $X$ are better. Let $(\Omega,\mathcal F)$ be a measurable space and $\mathbb Y$ the space of finite signed measures on it. The mission fixes

a real locally convex topological vector space $\mathcal X$ of $\mathcal F$ -measurable functions $X:\Omega\to\mathbb R$ , with its own topology (for instance a norm), not necessarily pointwise convergence;
a linear subspace $\mathcal Y\subseteq\mathbb Y$ with $\int_\Omega|X|\,d|\mu|<\infty$ for all $X\in\mathcal X$ , $\mu\in\mathcal Y$ , where $|\mu|=\mu^++\mu^-$ ;
the pairing $\langle\mu,X\rangle=\int_\Omega X\,d\mu=\int X\,d\mu^+-\int X\,d\mu^-$ , compatible with the topology of $\mathcal X$ : every $\langle\mu,\cdot\rangle$ is continuous, and every continuous linear functional on $\mathcal X$ is some $\langle\mu,\cdot\rangle$ , $\mu\in\mathcal Y$ .

Write $\mathcal X_+$ for the nonnegative functions, $Y\succeq X$ for $Y(\omega)\ge X(\omega)$ for all $\omega$ , $\mathcal Y_+$ for the nonnegative measures in $\mathcal Y$ , and $\mathcal P$ for the probability measures in $\mathcal Y$ . Condition (C) requires that every $\mu\in\mathcal Y\setminus\mathcal Y_+$ have $\langle\mu,X\rangle<0$ for some $X\in\mathcal X_+$ .

A risk function $\rho:\mathcal X\to\overline{\mathbb R}$ is proper if it never equals $-\infty$ and is finite somewhere. The axioms are

(A1) $\rho(\alpha X+(1-\alpha)Y)\le\alpha\rho(X)+(1-\alpha)\rho(Y)$ , $\alpha\in[0,1]$ ;
(A2) $Y\succeq X\Rightarrow\rho(Y)\ge\rho(X)$ ;
(A3) $\rho(X+a)=\rho(X)+a$ , $a\in\mathbb R$ ;
(A4) $\rho(tX)=t\rho(X)$ , $t>0$ .

The conjugate is $\rho^*(\mu)=\sup_{X\in\mathcal X}\{\langle\mu,X\rangle-\rho(X)\}$ , the biconjugate $\rho^{**}(X)=\sup_{\mu\in\mathcal Y}\{\langle\mu,X\rangle-\rho^*(\mu)\}$ , the dual domain $\mathcal A=\operatorname{dom}\rho^*=\{\mu\in\mathcal Y:\rho^*(\mu)<+\infty\}$ , and $\operatorname{lsc}(\rho)(X)=\liminf_{Z\to X}\rho(Z)$ the lower semicontinuous hull. In Lean these are pair, PairedSpaces, CondC, IsProper, A1–A4, conj, biconj, dualDom and lscHull in ConvexRiskFn.Dual.

Formalization targets

Goal: Theorem 2.2 (p. 435)

Under condition (C), for $\rho$ proper, lower semicontinuous and convex,

\rho(X)=\sup_{\mu\in\mathcal A}\{\langle\mu,X\rangle-\rho^*(\mu)\}\quad\forall X,\qquad(2.6)

and (i) (A2) holds iff every $\mu\in\mathcal A$ is nonnegative; (ii) when $\mathcal X$ contains the constant function $1$ , (A3) holds iff $\mu(\Omega)=1$ for all $\mu\in\mathcal A$ ; (iii) (A4) holds iff $\rho(X)=\sup_{\mu\in\mathcal A}\langle\mu,X\rangle$ for all $X$ (2.7).

Milestones

Under (C), $\mathcal Y_+=\{\mu\in\mathcal Y:\langle\mu,X\rangle\ge0\ \forall X\in\mathcal X_+\}$ (p. 434).
Theorem 2.1 (Fenchel–Moreau): $\rho^{**}=\operatorname{lsc}(\rho)$ for convex proper $\rho$ with $\operatorname{lsc}(\rho)>-\infty$ .
The representation (2.6) by itself.
Under (C) and (A2), $\rho^*(\mu)=+\infty$ for $\mu\notin\mathcal Y_+$ .
Under (A3), $\rho^*(\mu)=+\infty$ when $\mu(\Omega)\ne1$ .
Under (A4), $\rho^*$ is the indicator function of $\{\mu\in\mathcal Y:\langle\mu,\cdot\rangle\le\rho\}$ .

Companion: the risk envelope (2.8), p. 436

Under (A1)–(A3), (2.6) holds with $\mathcal A\subseteq\mathcal P$ ; adding (A4), $\rho^*$ is the indicator of $\mathcal A=\{\mu\in\mathcal P:\langle\mu,X\rangle\le\rho(X)\ \forall X\}$ .

Significance

Theorem 2.2 is the unifying statement behind the dual representations of coherent and convex risk measures: one theorem covers bounded measurable functions paired with all finite signed measures, $\mathcal L_p$ paired with $\mathcal L_q$ , and weak topologies. Downstream, the paper uses it to describe subdifferentials of risk functions as subsets of $\mathcal A$ , to derive optimality conditions for $\min_z\rho(F(z))$ , and to obtain the risk envelope (2.8) used in distributionally robust optimization.

The result is proved in the paper, assuming Fenchel–Moreau in locally convex spaces as a cited theorem. As far as is known, neither Theorem 2.2 nor Fenchel–Moreau for extended-real functions on a general locally convex space has a machine-checked proof. At the pinned revision Mathlib has geometric Hahn–Banach separation in locally convex spaces but no Fenchel conjugate at all. A formal proof of the goal would yield, in particular, a reusable Fenchel–Moreau theorem for extended-real convex functions under a measure pairing.

Difficulty

The characterizations (i)–(iii) are short once (2.6) is available; the weight sits in (2.6), that is, in Fenchel–Moreau. Its proof separates a point below the epigraph from the closed convex epigraph in $\mathcal X\times\mathbb R$ , which needs Hahn–Banach in a locally convex space, the identification of the separating functional with a measure in $\mathcal Y$ through the compatibility assumption, and a careful case analysis when the separating hyperplane is vertical, a case that occurs because $\rho$ may take the value $+\infty$ . The extended-real arithmetic ( $r-(+\infty)=-\infty$ , $0\cdot(+\infty)=0$ ) has to be tracked through every supremum. A finite-dimensional argument does not transfer: $\mathcal X$ is an arbitrary locally convex space, and lower semicontinuity is with respect to its own topology.

Formalization scope

$\mathcal X$ is an abstract real vector space with a topology and the instances IsTopologicalAddGroup, ContinuousSMul ℝ, LocallyConvexSpace ℝ (no Hausdorff assumption), mapped injectively and linearly into $\Omega\to\mathbb R$ . $\mathcal Y$ is a Submodule ℝ (SignedMeasure Ω). The pairing is the difference of the Bochner integrals against the Jordan parts; integrability against $|\mu|$ is a field of the structure, so the pairing is never the junk value of a non-integrable integral. The topology of $\mathcal Y$ is not modelled, since no statement uses it. Risk functions take values in EReal, and every supremum is an iSup in EReal. The order $\succeq$ is pointwise, not almost everywhere. The constant $a$ in (A3) is $a\cdot\mathbf 1$ for an element $\mathbf 1\in\mathcal X$ equal to the constant function $1$ . Condition (C) is a separate hypothesis, assumed where it is used.

Two statements depart from the page, and both departures are disclosed in their items. Theorem 2.1 carries the extra hypothesis $\operatorname{lsc}(\rho)>-\infty$ , without which the printed statement is false in infinite dimension; Theorem 2.1 is a cited result, and the goal does not depend on this choice. The indicator-function milestone names the set $\{\mu:\langle\mu,\cdot\rangle\le\rho\}$ explicitly instead of "a closed convex subset of $\mathcal Y$ ".

The goal mentions neither $\rho^{**}$ nor $\operatorname{lsc}(\rho)$ : it is stated about $\rho$ , $\rho^*$ and $\mathcal A$ alone, and a proof must establish (2.6) from the hypotheses, not assume it. The hypotheses are satisfiable: a one-point $\Omega$ with $\mathcal X=\mathbb R^{\{\ast\}}$ , $\mathcal Y=\mathbb Y$ and $\rho(X)=X(\ast)$ meets all of them, including (C) and (A1)–(A4).

Contributions are welcome at every level: Fenchel–Moreau for EReal-valued convex functions on locally convex spaces (reusable well beyond this mission), lemmas about the pairing (linearity, $\langle\mu,1\rangle=\mu(\Omega)$ , positivity), and the milestones in the order listed.

Selected references

A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072
F. Delbaen, Coherent risk measures on general probability spaces, in Advances in Finance and Stochastics, Springer, 2002, 1–37. https://doi.org/10.1007/978-3-662-04790-3_1
P. Cheridito, F. Delbaen, M. Kupper, Coherent and convex monetary risk measures for bounded càdlàg processes, Stochastic Processes and their Applications 112(1):1–22, 2004. https://doi.org/10.1016/j.spa.2004.01.009
R. T. Rockafellar, Conjugate Duality and Optimization, SIAM, 1974. https://doi.org/10.1137/1.9781611970524
R. T. Rockafellar, S. Uryasev, M. Zabarankin, Generalized deviations in risk analysis, Finance and Stochastics 10(1):51–74, 2006. https://doi.org/10.1007/s00780-005-0165-8

8 thms2 active usersReviewed

Algorithmic Game Theory Linear algebra·Captain: mikedeng1

Flows and Decompositions of Games: Harmonic and Potential Games 3: In Every Harmonic Game the Uniformly Mixed Strategy Profile Is a Mixed Nash EquilibriumResearch Paper

Motivation

Finite games in strategic form are the basic model of strategic interaction in economics, engineering and computer science. Potential games (Monderer and Shapley, 1996, DOI 10.1006/game.1996.0044) are the class with the most tractable equilibrium behaviour: every finite potential game has a pure Nash equilibrium, and simple learning dynamics converge to one.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Mathematics of Operations Research 36(3), 2011, DOI 10.1287/moor.1110.0500) decompose every finite game canonically into a potential, a harmonic and a nonstrategic component, by viewing the payoff differences of a game as a flow on a graph and applying the combinatorial Helmholtz decomposition. Harmonic games are the complement of potential games, and their equilibria behave in the opposite way: they generically have no pure Nash equilibrium. This mission formalizes the paper's positive result on the harmonic side. In every harmonic game, whatever the number of players and strategies, the profile in which every player randomizes uniformly over its strategies is a mixed Nash equilibrium. Rock–paper–scissors and matching pennies are the familiar two-player instances.

Setting

A finite game has a finite set of players $\mathcal M$ and, for each player $m$ , a nonempty finite strategy set $E^m$ with $h_m = |E^m|$ elements. A strategy profile is $p = (p^m)_m \in E = \prod_m E^m$ . We write $p^{-m}$ for the strategies of the players other than $m$ , $E^{-m} = \prod_{k\ne m}E^k$ , and $(q^m, p^{-m})$ for $p$ with player $m$ 's strategy replaced by $q^m$ . A game is identified with its utilities $u = (u^m)_m$ , $u^m : E \to \mathbb R$ , which form an element of $C_0^M$ , where $C_0 = \{f : E\to\mathbb R\}$ carries $\langle\varphi_1,\varphi_2\rangle_0 = \sum_p\varphi_1(p)\varphi_2(p)$ .

Two profiles are $m$ -comparable if they are distinct and differ only in player $m$ 's strategy. The game graph has the profiles as nodes and joins every comparable pair. An edge flow is a function $X$ on ordered pairs of profiles with $X(p,q) = -X(q,p)$ on edges and $X = 0$ off edges. The space $C_1$ of edge flows carries $\langle X,Y\rangle_1 = \tfrac12\sum_{(p,q)\in A}X(p,q)Y(p,q)$ . The combinatorial gradient is $(\delta_0\varphi)(p,q) = W(p,q)(\varphi(q)-\varphi(p))$ , with $W$ the edge indicator, and $\delta_0^*$ is its adjoint. Restricting to $m$ -comparable pairs gives $D_m : C_0\to C_1$ , and $Du = \sum_m D_m u^m$ is the flow of payoff differences of $u$ . With $\Pi_m = D_m^\dagger D_m$ (Moore–Penrose pseudoinverse) and $\Pi = \operatorname{diag}(\Pi_1,\dots,\Pi_M)$ , Definition 4.2 of the paper sets

\mathcal H = \{u \mid u = \Pi u,\ Du \in \ker\delta_0^*\},\qquad \mathcal N = \ker D .

A game is a harmonic game if $u\in\mathcal H\oplus\mathcal N$ , and a normalized harmonic game if $u\in\mathcal H$ .

A mixed strategy of player $m$ is a probability vector $x^m\in\Delta E^m$ , and a mixed strategy profile is $x = \{x^m\}_m\in\prod_m\Delta E^m$ . The mixed extension is $u^m(x) = \sum_{p\in E}u^m(p)\prod_k x^k(p^k)$ (34). The payoff of the pure strategy $q^m$ against $x^{-m}$ is $u^m(q^m,x^{-m}) = \sum_{p^{-m}}u^m(q^m,p^{-m})\prod_{k\ne m}x^k(p^k)$ (35). A mixed Nash equilibrium (Definition 5.1.1) is a mixed profile with $u^m(x^m,x^{-m})\ge u^m(p^m,x^{-m})$ for every $m$ and $p^m\in E^m$ . A probability distribution $x\in\Delta E$ on profiles is a correlated equilibrium (Definition 5.1.2) if $\sum_{p^{-m}}(u^m(p^m,p^{-m})-u^m(q^m,p^{-m}))\,x(p^m,p^{-m})\ge 0$ for all $m$ and $p^m,q^m$ . The uniformly mixed strategy profile (Definition 5.2) has $x^m(q^m) = 1/h_m$ for every $m$ and $q^m$ .

Formalization targets

Goal: Theorem 5.4

For every harmonic game $u\in\mathcal H\oplus\mathcal N$ , the uniformly mixed strategy profile $x$ is a mixed Nash equilibrium:

u^m(x^m,x^{-m}) \;\ge\; u^m(p^m,x^{-m})\qquad\text{for all } m\in\mathcal M,\ p^m\in E^m .

Milestones

Lemma A.1: for every edge flow $\hat X$ and every set of profiles $\hat S$ , $\sum_{p\in\hat S}(\delta_0^*\hat X)(p) = -\sum_{p\in\hat S}\sum_{q\in\hat S^c}\hat X(p,q)$ .
Lemma 5.2: in a harmonic game, $\sum_{p^{-m}\in E^{-m}}\big(u^m(r^m,p^{-m}) - u^m(q^m,p^{-m})\big) = 0$ for all $m$ and $q^m, r^m$ .
Proposition 5.2: in a normalized harmonic game, a distribution $x\in\Delta E$ is a correlated equilibrium iff all the inequalities of Definition 5.1.2 hold with equality (36), iff $\sum_{p^{-m}}u^m(q^m,p^{-m})\,x(p^m,p^{-m}) = 0$ for all $m,p^m,q^m$ (37).
Remark after Proposition 5.2: the equivalence of correlated equilibrium with (36) holds for all harmonic games.
Corollary 5.2: in a harmonic game, a mixed profile is a mixed Nash equilibrium iff $u^m(x^m,x^{-m}) = u^m(p^m,x^{-m})$ for all $m$ and $p^m$ (42).

Significance

Theorem 5.4 is the counterpart, for harmonic games, of the existence of pure equilibria in potential games. It exhibits an explicit equilibrium that does not depend on the payoffs at all, only on the strategy counts $h_m$ . Corollary 5.2, a milestone here, adds that at any mixed equilibrium of a harmonic game every player is indifferent among all its pure strategies, including those outside the support. That is much stronger than the usual support condition. Proposition 5.2 shows that the correlated equilibria of a normalized harmonic game are the points of the probability simplex in a linear subspace determined by the utilities. The paper uses that description in its later analysis of two-player harmonic games.

The results are proved in the paper; none of them is machine-checked. The formalization connects the paper's operator layer (flows on the game graph, the gradient and its adjoint with the $\tfrac12$ -weighted inner product, pseudoinverses) with standard equilibrium notions on finite games. It reuses published definitions of lotteries, the mixed extension and correlated equilibria.

Difficulty

The equilibrium statement follows quickly once Lemma 5.2 is available. The difficulty lies in translating the harmonic condition, a statement about the adjoint of an operator on edge flows, into an identity about payoffs. That needs the explicit form of $\delta_0^*$ , which depends on the $\tfrac12$ in the inner product of $C_1$ . It also needs the fact that $D$ kills the nonstrategic component, and a computation of the flow of $Du$ across the boundary of the set of profiles in which player $m$ plays $r^m$ . Corollary 5.2 needs the passage from mixed profiles to product distributions on profiles and a careful accounting of sums over $p^{-m}$ against sums over full profiles.

The first idea, to use the normalization $\sum_{q^m}u^m(q^m,p^{-m}) = 0$ , is not available. The goal concerns all harmonic games, not only normalized ones, and normalization alone does not give indifference against uniform opponents: the harmonic condition is essential.

Formalization scope

Players form a finite type ι with decidable equality, and the strategy sets E m are nonempty finite types, as in the paper ( $E^m = \{1,\dots,h_m\}$ ). The hypothesis [∀ m, Nonempty (E m)] is stated explicitly on the game theorems, because the uniform profile $1/h_m$ is a probability vector only if $h_m\ge1$ . A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)) with the unweighted sum inner product of p. 14. $C_1$ is the subspace of edge flows with the inner product $\tfrac12\sum$ of (7). $\delta_0^*$ is Mathlib's adjoint, and the pseudoinverse is defined directly. $\mathcal H$ and $\mathcal N$ are defined by (28), and harmonic games are the submodule H ⊔ N. Lotteries, mixed profiles and the mixed extension (34) come from the published agt_games definitions; correlated equilibrium is the published HartSchmeidler.Finite.IsCorrelatedEq. The pure-deviation payoff (35), mixed Nash equilibrium with pure deviations (Definition 5.1.1, as printed), and the uniform profile are defined in the mission. Sums over $p^{-m}$ are written as sums over the profiles with player $m$ 's strategy fixed, so each $p^{-m}$ is counted once.

The goal concerns mixed Nash equilibria. Stating it for the uniform product distribution as a correlated equilibrium, or for normalized games only, would be a weaker statement and is not the target. No hypothesis is added beyond the nonemptiness of the strategy sets.

Contributions welcome: proofs of the milestones, and general lemmas on adjoints of graph gradients and on product distributions that are reusable beyond this mission.

Selected references

O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Mathematics of Operations Research 36(3), 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14, 1996. https://doi.org/10.1006/game.1996.0044
S. Hart, D. Schmeidler, Existence of Correlated Equilibria, Mathematics of Operations Research 14(1), 1989. https://doi.org/10.1287/moor.14.1.18

12 thms2 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Optimization of Convex Risk Functions 3: A Distribution-Invariant Risk Function Is Consistent with the Increasing Convex Order Iff It Is Monotone and Risk AverseResearch Paper

Motivation

Risk-averse optimization replaces the expected cost $\mathbb E[X]$ of a random outcome by a risk function $\rho(X)$ that also penalizes dispersion: mean–deviation, mean–semideviation, conditional value-at-risk (CVaR) and their combinations are the standard examples in stochastic programming and portfolio selection. A decision maker who uses $\rho$ should not prefer an outcome that every risk-averse expected-utility maximizer rejects. For costs, the order that expresses this agreement among risk-averse agents is the increasing convex order: $X_2$ is worse than $X_1$ if $\mathbb E[u(X_2)]\ge\mathbb E[u(X_1)]$ for every increasing convex disutility $u$ . It is the counterpart, for costs, of second-order stochastic dominance.

Whether a given mean–risk model is consistent with stochastic dominance was settled model by model: Ogryczak and Ruszczyński for mean–semideviation models (Eur. J. Oper. Res. 1999, Math. Program. 2001, SIAM J. Optim. 2002) and Pflug for CVaR (2000). Ruszczyński and Shapiro (Math. Oper. Res. 31, 2006) gave a single criterion, Theorem 5.1, which contains these results as special cases: among risk functions that depend only on the distribution of the outcome, consistency with the increasing convex order is equivalent to two structural properties, monotonicity and risk aversion.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $p\in[1,\infty)$ . The space of outcomes is $\mathcal X=\mathcal L_p(\Omega,\mathcal F,P)$ , the real random variables with $\mathbb E|X|^p<\infty$ . An outcome is a cost: smaller is better. A risk function is a map $\rho:\mathcal X\to\mathbb R$ .

The cdf of $X$ is $F_X(t)=P(X\le t)$ . $\rho$ is distribution invariant (Definition 5.2) if $F_{X_1}=F_{X_2}$ implies $\rho(X_1)=\rho(X_2)$ .
$\rho$ satisfies (A2) (monotonicity) if $X\le Y$ almost surely implies $\rho(X)\le\rho(Y)$ .
$\rho$ is risk averse (Definition 5.1) if for every $\sigma$ -algebra $\mathcal G\subset\mathcal F$ and every $X\in\mathcal X$ ,

\rho(X)\ \ge\ \rho\big(\mathbb E[X\mid\mathcal G]\big),

for every version of the conditional expectation.

For random variables $X_1,X_2$ , the usual stochastic order $X_2\succeq_{\mathrm{st}}X_1$ holds if $\mathbb E[u(X_2)]\ge\mathbb E[u(X_1)]$ for every nondecreasing $u:\mathbb R\to\mathbb R$ for which both expectations exist; the increasing convex order $X_2\succeq_{\mathrm{icx}}X_1$ is the same with $u$ ranging over the increasing convex functions.
$\rho$ is consistent with an order $\succeq$ if $X_2\succeq X_1$ implies $\rho(X_2)\ge\rho(X_1)$ for all $X_1,X_2\in\mathcal X$ .

The paper places one more standing assumption on §5.2: the space is rich enough to carry a uniform random variable, a measurable $U:\Omega\to\mathbb R$ with $P(U\le t)=t$ for all $t\in[0,1]$ .

In Lean these are IsUniformRV, cdfOf, cdfInv, DistInvariant, A2, RiskAverse, StLE, ConsistentSt and ConsistentIcx in the namespace ConvexRiskFn.Order; the increasing convex order is the published StochasticOrders.MonotoneConvex.IcxOrder P P X₁ X₂, read as $X_1\preceq_{\mathrm{icx}}X_2$ .

Formalization targets

Goal: Theorem 5.1 (p. 446)

Under the standing assumptions, for every distribution-invariant $\rho:\mathcal X\to\mathbb R$ ,

\rho\ \text{consistent with}\ \succeq_{\mathrm{icx}}\quad\Longleftrightarrow\quad \rho\ \text{satisfies (A2) and is risk averse}.

No convexity, translation equivariance or positive homogeneity of $\rho$ is assumed.

Milestones

The usual stochastic order and the cdf (§5.2, p. 445): $X_2\succeq_{\mathrm{st}}X_1$ iff $F_{X_2}(t)\le F_{X_1}(t)$ for all $t$ .
The quantile coupling (proof of Lemma 5.1, p. 446): $F_X^{-1}(U)$ has the law of $X$ , and $F_{X_2}\le F_{X_1}$ gives $F_{X_1}^{-1}(U)\le F_{X_2}^{-1}(U)$ almost surely.
Lemma 5.1 (p. 445): a distribution-invariant $\rho$ is consistent with $\succeq_{\mathrm{st}}$ iff it satisfies (A2).
Conditional expectation is icx-smaller (proof of Theorem 5.1, p. 446): $\mathbb E[X\mid\mathcal G]\in\mathcal X$ and $\mathbb E[X\mid\mathcal G]\preceq_{\mathrm{icx}}X$ .
Strassen's coupling on $\Omega$ (proof of Theorem 5.1, p. 446): if $X_1\preceq_{\mathrm{icx}}X_2$ , there are $\widehat X_1\overset{D}{\sim}X_1$ , $\widehat X_2\overset{D}{\sim}X_2$ on the same $\Omega$ with $\widehat X_1\le\mathbb E[\widehat X_2\mid\widehat X_1]$ a.s.

Significance

Theorem 5.1 reduces a property quantified over all pairs of ordered distributions to two properties that can be checked on the risk function directly. Monotonicity is usually immediate, and risk aversion follows for the main examples from the dual representation of the risk function (the paper verifies it for mean–semideviation and for CVaR-based models in §5.1). The theorem then yields at once the consistency of these models with the increasing convex order, which was previously proved case by case. It also explains the failures: a law-invariant risk function that violates (A2), such as mean–deviation for $p>1$ under the paper's condition $(*)$ , cannot be consistent with any increasing integral stochastic order.

The result has a complete published proof. What the mission adds is a machine-checked version of it on the paper's own space $\mathcal L_p(\Omega,\mathcal F,P)$ , together with reusable pieces of stochastic-order theory: the cdf characterization of the usual stochastic order, the quantile coupling, conditional Jensen in increasing-convex form, and Strassen's martingale coupling realized on a given space carrying a uniform random variable. Mathlib has conditional Jensen for convex functions (ConvexOn.map_condExp_le_univ) but not the stochastic orders, the quantile coupling or Strassen's theorem. Strassen's theorem for laws on $\mathbb R^n$ , with a coupling on some probability space, is posed separately on Prove2Me but not proved.

Difficulty

The forward direction is short given milestone 4. The reverse direction is where the work is. Consistency compares $\rho(X_1)$ and $\rho(X_2)$ for random variables that are related only through their laws: $X_1\preceq_{\mathrm{icx}}X_2$ says nothing about $X_1(\omega)$ versus $X_2(\omega)$ , so neither (A2) nor risk aversion applies to the pair as given. The argument has to replace the pair by another pair, with the same laws, on the same space $\Omega$ , related by a conditional expectation; only then can monotonicity and risk aversion be chained. Producing that pair is Strassen's theorem, a nonconstructive existence result about martingale couplings, and it has to be realized on the given $\Omega$ , not on a product space built for the purpose, because $\rho$ is defined only on $\mathcal L_p(\Omega,\mathcal F,P)$ . That is the role of the uniform random variable, and transporting the coupling onto $\Omega$ through it is a separate measure-theoretic step. The first-order analogue, Lemma 5.1, needs the same kind of transfer, through quantile functions, whose values at $0$ and $1$ must be handled.

Formalization scope

$\mathcal L_p$ is encoded by functions $\Omega\to\mathbb R$ satisfying MemLp X p P with 1 ≤ p and p ≠ ⊤, not by almost-everywhere classes. $\rho$ is a function (Ω → ℝ) → ℝ; every definition quantifies only over MemLp arguments, so its values elsewhere play no role. $\rho$ is real valued, as in Definition 5.2.
The order in (A2) is the almost-sure order, the order of $\mathcal L_p$ (p. 434).
"For which the expectations exist" is integrability of $u\circ X_1$ and $u\circ X_2$ , as in the published increasing convex order.
Risk aversion quantifies over every sub- $\sigma$ -algebra $\mathcal G\subseteq\mathcal F$ and every $\mathcal G$ -measurable version of Mathlib's conditional expectation P[X|m].
The uniform random variable and $p\in[1,\infty)$ appear as hypotheses of the goal, of Lemma 5.1 and of milestone 5, exactly where the paper's standing assumptions of §5.2 apply. Milestones 1 and 4 do not need them.
The quantile $F^{-1}(t)=\inf\{s:F(s)\ge t\}$ is a real infimum, which is $0$ where the paper's value is $\pm\infty$ ( $t\notin(0,1)$ ); milestone 2 is therefore stated almost surely.
The goal mentions neither quantiles, nor $U$ beyond its existence, nor any coupling. A statement that assumed convexity of $\rho$ , dropped distribution invariance, restricted to bounded or pointwise-ordered outcomes, or replaced risk aversion by the single $\sigma$ -algebra $\{\emptyset,\Omega\}$ would be a different and weaker theorem and does not count.

Needed infrastructure: equality in law from equality of cdfs, the quantile transform, conditional Jensen's inequality (in Mathlib) turned into the increasing convex order, and Strassen's theorem in dimension one with the transfer of a coupling to a space carrying a uniform random variable. The last two are reusable well beyond this mission. Proofs of any milestone, and of supporting lemmas such as the cdf characterization of equality in law, are welcome.

Selected references

A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
A. Müller, D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002 (Theorem 1.2.8, Corollary 1.5.21). https://www.wiley.com/en-us/Comparison+Methods+for+Stochastic+Models+and+Risks-p-9780471494461
V. Strassen, The existence of probability measures with given marginals, Annals of Mathematical Statistics 36(2):423–439, 1965. https://doi.org/10.1214/aoms/1177700153
D. Blackwell, Equivalent comparisons of experiments, Annals of Mathematical Statistics 24(2):265–272, 1953. https://doi.org/10.1214/aoms/1177729032
W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean–risk models, SIAM Journal on Optimization 13(1):60–78, 2002. https://doi.org/10.1137/S1052623400375075
M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

8 thms2 active usersReviewed

Algorithmic Game Theory Linear algebra·Captain: mikedeng1

Flows and Decompositions of Games: Harmonic and Potential Games 2: Harmonic Games Generically Have No Pure Nash EquilibriumResearch Paper

Motivation

Finite games in strategic form are the basic model of interaction between self-interested agents in economics, engineering and computer science. Among them, potential games (Monderer and Shapley, 1996) are the class with the most tractable equilibrium behaviour: every finite potential game has a pure Nash equilibrium, and simple learning dynamics such as best response and fictitious play converge to one. A natural question is what lies at the opposite end of the space of games, and how far a general game is from that tractable class.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Mathematics of Operations Research 36(3), 2011, DOI 10.1287/moor.1110.0500) answer this with a canonical decomposition of every finite game into a potential, a harmonic and a nonstrategic component, obtained by viewing the payoff differences of a game as a flow on a graph and applying the combinatorial Helmholtz decomposition. Harmonic games, those whose potential component vanishes, are the complement of potential games, and the paper shows that their equilibrium behaviour is opposite as well. This mission formalizes the first such result: harmonic games generically have no pure Nash equilibrium, so the guaranteed existence of pure equilibria in potential games has no counterpart on the harmonic side. The decomposition has since been used to study near-potential games and the convergence of learning dynamics in them.

Setting

A finite game has a finite set of players $\mathcal M$ with $M = |\mathcal M|$ and, for each player $m$ , a nonempty finite strategy set $E^m$ with $h_m = |E^m|$ elements. A strategy profile is $p = (p^m)_m \in E = \prod_m E^m$ , and $(q^m, p^{-m})$ denotes $p$ with player $m$ 's strategy replaced by $q^m$ . The utilities $u = (u^m)_m$ assign to each player a function $u^m : E \to \mathbb R$ ; for fixed $\mathcal M$ and $E$ a game is identified with its utilities, an element of $C_0^M$ , where $C_0 = \{f : E \to \mathbb R\}$ carries the inner product $\langle \varphi_1,\varphi_2\rangle_0 = \sum_p \varphi_1(p)\varphi_2(p)$ .

A profile $p$ is a pure Nash equilibrium if $u^m(p^m, p^{-m}) \ge u^m(q^m, p^{-m})$ for every player $m$ and every $q^m \in E^m$ .

Two profiles are $m$ -comparable if they are distinct and differ only in player $m$ 's strategy. The game graph has the profiles as nodes and joins every comparable pair. An edge flow is a function $X$ on ordered pairs of profiles with $X(p,q) = -X(q,p)$ on edges and $X = 0$ off edges; the space $C_1$ of edge flows carries $\langle X,Y\rangle_1 = \tfrac12\sum_{(p,q)\in A} X(p,q)Y(p,q)$ . The combinatorial gradient is $(\delta_0\varphi)(p,q) = W(p,q)(\varphi(q)-\varphi(p))$ , with $W$ the edge indicator, and $\delta_0^*$ is its adjoint. Restricting to $m$ -comparable pairs gives $D_m : C_0 \to C_1$ , and $D u = \sum_m D_m u^m$ is the flow of payoff differences of the game $u$ . With $\Pi_m = D_m^\dagger D_m$ (Moore–Penrose pseudoinverse) and $\Pi = \operatorname{diag}(\Pi_1,\dots,\Pi_M)$ , the paper's Definition 4.2 sets

\mathcal P = \{u \mid u = \Pi u,\ Du \in \operatorname{im}\delta_0\},\quad \mathcal H = \{u \mid u = \Pi u,\ Du \in \ker\delta_0^*\},\quad \mathcal N = \ker D .

A game is a harmonic game if $u \in \mathcal H \oplus \mathcal N$ : its payoff differences form a flow with no source or sink at any profile.

Formalization targets

Goal: Proposition 5.1

For finite games in which at least two players have at least two strategies each, and for any additive Haar measure $\mu$ on the finite-dimensional space $\mathcal H \oplus \mathcal N$ ,

\mu\big(\{u \in \mathcal H\oplus\mathcal N : u \text{ has a pure Nash equilibrium}\}\big) = 0 .

This is the paper's "harmonic games generically do not have pure Nash equilibria", with "generically" read as the paper defines it: true except on a set of measure zero within the harmonic games.

Stronger structural form

For each profile $p$ , the harmonic games having $p$ as a pure Nash equilibrium form a proper linear subspace of $\mathcal H \oplus \mathcal N$ . The exceptional set of the goal is then a finite union of lower-dimensional subspaces.

Milestones

Lemma 5.1: at a pure Nash equilibrium of a harmonic game, every player is indifferent among all of their strategies.
Proposition 4.1: $\dim\mathcal P = \prod_m h_m - 1$ , $\dim\mathcal H = (M-1)\prod_m h_m - \sum_m\prod_{k\ne m}h_k + 1$ , $\dim\mathcal N = \sum_m\prod_{k\ne m}h_k$ .

Significance

The result separates harmonic games sharply from potential games. A finite potential game always has a pure equilibrium; a harmonic game almost never has one. Together with the decomposition theorem, it says that the obstruction to pure equilibria in a general game is carried by its harmonic component, and it motivates the paper's later results on mixed equilibria of harmonic games (the uniformly mixed profile is always a mixed equilibrium). Proposition 4.1, a milestone here, also gives the dimension of the harmonic games, $(M-1)\prod_m h_m + 1$ , and so measures how large that class is.

The results are proved in the paper; none of them is machine-checked. Formalizing them requires the paper's operator layer (flows on the game graph, the gradient with its adjoint, pseudoinverses) in Lean for the first time, and pins down two points the paper leaves informal: the measure with respect to which "generically" is meant, and the shape condition on the game under which the statement holds.

Difficulty

Lemma 5.1 is a short counting argument once the divergence-free condition $\delta_0^* D u = 0$ is unpacked, but unpacking it requires knowing that $D$ kills $\mathcal N$ and computing $\delta_0^*$ from the $\tfrac12$ -weighted inner product. The main obstacle of the goal is showing that the exceptional subspaces are proper. The proof needs a harmonic game with nonzero payoff differences, that is $\dim\mathcal H > 0$ , and the only route the paper offers is the dimension count of Proposition 4.1. That count rests on the full decomposition $C_0^M = \mathcal P\oplus\mathcal H\oplus\mathcal N$ , on the kernel of each $D_m$ and on the connectivity of the game graph, all of which must be built in Lean. The measure-theoretic last step, that a finite union of proper subspaces is Haar-null, is in Mathlib.

A tempting shortcut fails: placing Lebesgue measure on all of $C_0^M$ and observing that $\mathcal H \oplus \mathcal N$ is a proper subspace would prove the goal without saying anything about equilibria.

Formalization scope

Players form a finite type ι with decidable equality, and the strategy sets E m are nonempty finite types, as in the paper ( $E^m = \{1,\dots,h_m\}$ ). A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)), with the unweighted sum inner product of p. 14. $C_1$ is the subspace of edge flows with the inner product $\tfrac12\sum$ of (7). $\delta_0^*$ is Mathlib's adjoint, and the pseudoinverse is defined directly as the inverse of $L$ on $(\ker L)^\perp$ composed with the orthogonal projection onto $\operatorname{im} L$ . $\mathcal P,\mathcal H,\mathcal N$ are defined by (28), not by the alternative description (29). Harmonic games are the submodule H ⊔ N, and pure Nash equilibrium is AGT.IsPureNash from the published agt_games definitions.

Added hypothesis. The paper leaves implicit that at least two distinct players have at least two strategies each. Its proof uses this through "dimension of $\mathcal H$ is larger than zero". Without it Proposition 5.1 is false: with two players having $1$ and $h$ strategies, $\dim\mathcal H = (2-1)h - (h+1) + 1 = 0$ , every harmonic game is nonstrategic, and every profile is a pure equilibrium of every harmonic game. The goal and the structural theorem therefore carry this hypothesis explicitly.

The measure. The measure is an arbitrary additive Haar measure on the subspace $\mathcal H\oplus\mathcal N$ itself, with the Borel σ-algebra of its subspace topology. A measure on the ambient $C_0^M$ would make the statement trivial, because the whole subspace is null there. Proposition 4.1 is stated as equalities in $\mathbb Z$ , so that $M-1$ and the subtraction in part 2 are not truncated.

Needed infrastructure: kernels of the $D_m$ (the paper's Lemma 4.2), the projection property of $D^\dagger D$ , the decomposition theorem, and the connectivity of the game graph. The operator layer is shared with the other missions of this series and is reusable for any work on flows on graphs. Proofs of the milestones, and of the structural form independently of the goal, are welcome.

Selected references

O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Mathematics of Operations Research 36(3):474–503, 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044
X. Jiang, L.-H. Lim, Y. Yao, Y. Ye, Statistical ranking and combinatorial Hodge theory, Mathematical Programming 127(1):203–244, 2011. https://doi.org/10.1007/s10107-010-0419-x

9 thms2 active usersReviewed

Convex Optimization Linear Optimization·Captain: mikedeng1

Retailer-Supplier Flexible Commitments Contracts: A Robust Optimization Approach: With Box Demand Uncertainty the Min-Max RSFC Problem Has the Same Optimal Value on the Extreme DemandsResearch Paper

Motivation

In a flexible commitments contract a retailer announces, before a selling horizon starts, a vector of planned orders (commitments) to its supplier, who uses them to plan capacity. During the horizon the retailer may deviate from the commitments, but pays penalties for each deviation and for changes between successive commitments. Such contracts were studied with stochastic demand by Bassok and Anupindi, Tsay and Lovejoy, and others, typically by dynamic programming over a discretized state space.

Ben-Tal, Golany, Nemirovski and Vial (2005) treat the retailer's problem as a robust multiperiod linear program: demand is only known to lie in an uncertainty set, decisions may adapt to observed demand, and the retailer minimizes its worst-case total cost. Most of the paper approximates this problem by affinely adjustable decision rules. For one important case, however, the paper shows that the problem can be solved exactly: when the uncertainty set is a box, nature may be restricted to the finitely many corner trajectories of the box. That reduction, Proposition 1 of the Appendix, is the subject of this mission, together with the general principle behind it (Lemma 2), which applies to any multistage worst-case problem with polyhedral dynamics and convex polyhedral costs.

Setting

Data. There are $T$ periods. Period $t$ carries an ordering cost $c_t$ , a holding cost $h_t$ , a shortage cost $p_t$ , penalties $\alpha_t^{+}, \alpha_t^{-}$ for ordering above or below the commitment, and penalties $\beta_t^{+}, \beta_t^{-}$ for raising or lowering the commitment relative to the previous one. A salvage value $s$ applies to the final inventory; put $\bar h_t = h_t$ for $t < T$ and $\bar h_T = h_T - s$ . The initial inventory $x_1$ and a nominal previous commitment $w_0$ are given, as are order bounds $L_t \le q_t \le U_t$ and cumulative bounds $\widehat L_t \le \sum_{\tau \le t} q_\tau \le \widehat U_t$ , possibly infinite.

Decisions. Before any demand is observed the retailer fixes commitments $w_t \ge 0$ and amounts $z_t$ . Demand $d = (d_1, \dots, d_T)$ lies in a product set $\mathcal U^T = \mathcal U_1 \times \dots \times \mathcal U_T$ . The order $q_t$ and the cost bounds $y_t, u_t$ of period $t$ are decision rules, functions of the past demands $d^{t-1} = (d_1, \dots, d_{t-1})$ ; the inventory $x_{t+1}$ is a function of $d^t$ . This nonanticipativity is required on trajectories of $\mathcal U^T$ .

The min-max RSFC problem (5)–(6). A policy is feasible if for every $d \in \mathcal U^T$ and every $t$ : $x_{t+1} = x_t + q_t - d_t$ ; the order and cumulative-order bounds hold; $y_t \ge \bar h_t x_{t+1}$ and $y_t \ge -p_t x_{t+1}$ ; $u_t \ge \alpha_t^{+}(q_t - w_t)$ and $u_t \ge -\alpha_t^{-}(q_t - w_t)$ ; and $z_t \ge \beta_t^{+}(w_t - w_{t-1})$ , $z_t \ge -\beta_t^{-}(w_t - w_{t-1})$ . The optimal value is

\operatorname{value}(\mathcal U) = \inf_{\text{feasible policies}}\ \sup_{d \in \mathcal U^T}\ \sum_{t=1}^T \big[c_t q_t(d^{t-1}) + y_t(d^{t-1}) + u_t(d^{t-1}) + z_t\big] \in [-\infty, +\infty].

Box uncertainty (9)–(10). $\mathcal U_t = [d_t^{\min}, d_t^{\max}]$ with $d_t^{\min} < d_t^{\max}$ ; its extreme points are $\{d_t^{\min}, d_t^{\max}\}$ .

Convex polyhedral functions. A function $f : \mathbb R^m \to \mathbb R \cup \{+\infty\}$ is a c.p.f. if its domain $\{f < \infty\}$ is the solution set of finitely many linear inequalities and $f$ is convex and lower semicontinuous on it. Lemma 2 concerns the generic problem $(P[F_0, \dots, F_T])$ : minimize, over decision rules $S_t(d^{t-1}) \in \mathbb R^{m_t}$ , the worst case over $d \in F_0 \times \dots \times F_T$ of $\sum_{t=1}^{T+1} f_t(S_t(d^{t-1}))$ , subject to $A_1 S_1 \ge b_1$ , $A_{t+1} S_{t+1} \ge B_{t+1} d_t + C_{t+1} S_t + b_{t+1}$ and $\|S_t\|_\infty \le R$ .

Formalization targets

Goal: Proposition 1 (p. 269)

\operatorname{value}\Big(\prod_{t=1}^T [d_t^{\min}, d_t^{\max}]\Big) = \operatorname{value}\Big(\prod_{t=1}^T \{d_t^{\min}, d_t^{\max}\}\Big).

The data are arbitrary reals (bounds in $[-\infty, +\infty]$ ) and the values are compared in the extended reals, so the statement covers infeasible and unbounded instances.

Milestones

The extreme points of a segment $[a,b]$ , $a<b$ , are $a$ and $b$ .
(38): for a c.p.f. $\operatorname{val}$ and a polytope $D$ , $\sup_{d \in D} \operatorname{val}(Bd + Cs + b) = \sup_{d \in \operatorname{ext} D} \operatorname{val}(Bd + Cs + b)$ .
$\operatorname{val}(b) = \min\{f(s) : As \ge b, \|s\|_\infty \le R\}$ is a c.p.f. when $f$ is.
A c.p.f. composed with an affine map is a c.p.f.
Item (a): $\varphi(s_T) = \max_{d_T \in D_T} \Phi_T(s_T, d_T)$ and $f_T + \varphi$ are c.p.f.s.
The Bellman reduction $\operatorname{opt}(P[F_0, \dots, F_T]) = \operatorname{opt}(P_+[F_0, \dots, F_{T-1}])$ .
(39): replacing the last polytope by its extreme points leaves the optimal value unchanged.
Lemma 2: $\operatorname{opt}(P[D_0, \dots, D_T]) = \operatorname{opt}(P[\operatorname{ext} D_0, \dots, \operatorname{ext} D_T])$ for convex polytopes $D_\tau$ , $D_0$ a singleton, and c.p.f. costs.
For every $R$ , the RSFC problem with every decision bounded by $R$ has the same value on the box and on its corners.
The $R$ -box step, in corrected form: $\operatorname{value}(\text{box}) \le \operatorname{value}_R(\text{box})$ for all $R$ , $\operatorname{value}(\text{corners}) \le \operatorname{value}(\text{box})$ , and $\operatorname{value}(\text{corners}) = \inf_R \operatorname{value}_R(\text{corners})$ .

Significance

Proposition 1 turns a semi-infinite multistage problem into a finite one: with box uncertainty, the min-max RSFC problem is equivalent to a linear program over the scenario tree of the $2^T$ corner trajectories, problem $P_{\text{ext}}$ of §2.3. The paper uses this exact value as a benchmark for its affinely adjustable approximation in the simulation study. Lemma 2 is the transferable statement: in any multistage worst-case problem whose stage costs are convex polyhedral and whose dynamics are linear with a uniform box on the decisions, the adversary may be restricted to the vertices of each period's uncertainty polytope.

The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces a reusable notion of convex polyhedral function in the extended reals, closure properties of that class (partial minimization over a polyhedral box, affine substitution, finite maxima, sums), and a formal worst-case Bellman equation for nonanticipative policies. The corrected form of the $R$ -box step also records precisely when the paper's informal "for $R$ large enough" argument is valid.

Difficulty

The natural argument, "a convex function attains its maximum over a polytope at a vertex", applies to one stage only. In a multistage problem the cost of the last stage depends on the earlier decisions, which depend on earlier demands, so the worst case is not a convex function of the whole trajectory. The proof must therefore pass through a dynamic programming recursion, and the class of stage costs must be closed under the recursion: the optimal last-stage value as a function of the previous decision must again be convex polyhedral. That closure (the value of a parametric problem with a convex polyhedral objective and a box constraint) is where the work is: the domain is a projection of a polyhedron, and attainment and lower semicontinuity have to be shown with infinite values allowed.

A second difficulty is bookkeeping. The RSFC problem must be rewritten as an instance of Lemma 2 with the right stage vectors so that nonanticipativity of $y_t$ in $d^{t-1}$ is preserved, and the bounded problem must be related back to the unbounded one, which can have value $-\infty$ .

Formalization scope

Periods of the RSFC model are Fin T, 0-based. Policies are functions of the whole demand trajectory with nonanticipativity imposed on trajectories of the uncertainty set; a policy that sees future demand is not admissible, which rules out the clairvoyant reading under which the statement changes. Optimal values are EReal infima of suprema: $+\infty$ for infeasible problems and possibly $-\infty$ , never a real sInf that would turn both into $0$ . The c.p.f. definition requires the domain to be exactly a finite system of linear inequalities, so it cannot be satisfied vacuously.

The standing assumptions of §2.2, $s < c_T$ and (1) $h_T - s \ge -p_T$ , are not imposed, and no sign is assumed on any cost or penalty: Proposition 1 holds without them, so the formal statement is a generalization. The norm $\|\cdot\|_\infty$ is Mathlib's default norm on Fin m → ℝ. Lemma 2's families are indexed by $\mathbb N$ with the paper's indices; B t, C t stand for $B_{t+1}$ , $C_{t+1}$ . Two printed slips are corrected in the statements: (38) keeps the $+\,b_{T+1}$ that the page drops, and the $R$ -box step is stated in the corrected sandwich form because the literal claim fails when the value is $-\infty$ .

Useful infrastructure: convex polyhedral functions in EReal, Fourier–Motzkin projection of polyhedra, maximum principle for convex functions on polytopes, extreme points of convex hulls of finite sets. Contributions to any milestone, and to general lemmas on these topics, are welcome.

Selected references

A. Ben-Tal, B. Golany, A. Nemirovski, J.-P. Vial, Retailer-Supplier Flexible Commitments Contracts: A Robust Optimization Approach, Manufacturing & Service Operations Management 7(3):248–271, 2005. https://doi.org/10.1287/msom.1050.0081
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99(2):351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
G. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30:257–280, 2005. https://doi.org/10.1287/moor.1040.0129

13 thms2 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Distributionally Robust Optimization and Its Tractable Approximations 3: The Infimal Convolution of π¹, π², π³ Bounds the Worst Case over the Intersected Families and Improves on EachResearch Paper

Motivation

Two-stage and multistage stochastic programs ask for decisions that react to uncertainty revealed over time. When the distribution of the uncertainty is known only partially, one optimizes against the worst distribution in a family $\mathbb F$ consistent with what is known: a support set, a range for the mean, a covariance matrix, bounds on how fast the tails decay. Goh and Sim (Oper. Res. 58(4), 2010) show that once linear and deflected linear decision rules are imposed, the recourse costs of such models reduce to worst-case expectations of positive parts,

\sup_{\mathbb P\in\mathbb F}E_{\mathbb P}\big((r^0+r'\tilde\zeta)^+\big),

of affine functions of a random vector $\tilde\zeta$ . These quantities are generally intractable, so the paper bounds them by optimization problems that are. Each kind of partial information gives its own bound, and in practice a modeller usually has several kinds at once. Theorem 4 of the paper, the target here, combines the separate bounds into a single one that uses all of the information.

Timeline: Scarf (1958) gave, for a newsvendor problem, the worst-case expected positive part of a scalar with known mean and variance. Chen, Sim and Sun (Oper. Res. 55(6), 2007) introduced the forward and backward deviations used here to describe tails of independent components. Chen and Sim (Oper. Res. 57(2), 2009) introduced the combination of bounds by infimal convolution that Theorem 4 restates in the present setting. Goh and Sim (2010) assemble the three kinds of information into one model and use the combined bound for their bideflected linear decision rules.

Setting

A distribution $\mathbb P$ is a probability measure on $\mathbb R^{N_E}$ , the law of the uncertain vector $\tilde\zeta$ ; its mean is $\hat\zeta=E_{\mathbb P}(\tilde\zeta)$ . Fix data: sets $\mathcal V,\hat{\mathcal V}\subseteq\mathbb R^{N_E}$ , matrices $F\in\mathbb R^{N\times N_E}$ , $\Sigma\in\mathbb R^{N\times N}$ , $F_\sigma\in\mathbb R^{N_\sigma\times N_E}$ , a vector $g_\sigma\in\mathbb R^{N_\sigma}$ , a set $\hat{\mathcal W}_\sigma\subseteq\mathbb R^{N_\sigma}$ and vectors $\sigma_f,\sigma_b\ge0$ in $\mathbb R^{N_\sigma}$ . Three families encode three kinds of information:

Mean and support: $\mathbb F_1=\{\mathbb P:\hat\zeta\in\hat{\mathcal V},\ \mathbb P(\tilde\zeta\in\mathcal V)=1\}$ .
Mean and covariance: $\mathbb F_2=\{\mathbb P:\hat\zeta\in\hat{\mathcal V},\ E_{\mathbb P}(F(\tilde\zeta-\hat\zeta)(\tilde\zeta-\hat\zeta)'F')=\Sigma\}$ .
Mean and directional deviations: $\mathbb F_3$ is the set of $\mathbb P$ with $\hat\zeta\in\hat{\mathcal V}$ such that $\tilde z_\sigma=F_\sigma\tilde\zeta+g_\sigma$ has independent components whose forward and backward deviations

\sigma_{f\mathbb P}(\tilde z_{\sigma,j})=\sup_{\theta>0}\sqrt{\tfrac{2}{\theta^2}\ln E_{\mathbb P}e^{\theta(\tilde z_{\sigma,j}-\hat z_{\sigma,j})}},\qquad \sigma_{b\mathbb P}(\tilde z_{\sigma,j})=\sup_{\theta>0}\sqrt{\tfrac{2}{\theta^2}\ln E_{\mathbb P}e^{-\theta(\tilde z_{\sigma,j}-\hat z_{\sigma,j})}}

are at most $\sigma_{f,j}$ and $\sigma_{b,j}$ .

The bounds are the optimal values $\pi^1,\pi^2,\pi^3$ of (21), (22) and (24) of the paper. For instance

\pi^1(r^0,r)=\inf_{s}\Big(\sup_{\hat\zeta\in\hat{\mathcal V}}s'\hat\zeta+\sup_{\zeta\in\mathcal V}\max\{r^0+r'\zeta-s'\zeta,-s'\zeta\}\Big),

$\pi^2$ is an infimum over $y$ with $F'y=r$ of a supremum over $\hat{\mathcal V}$ of a Scarf-type expression, and $\pi^3$ is an infimum over $(s^0,s,x^0,x)$ with $x^0+x'g_\sigma=r^0$ , $F_\sigma'x=r$ that involves the function

\psi(x^0,x)=\inf_{\lambda>0}\frac{\lambda}{e}\exp\Big(\frac1\lambda\sup_{\hat z_\sigma\in\hat{\mathcal W}_\sigma}\{x^0+x'\hat z_\sigma\}+\frac{\|u\|_2^2}{2\lambda^2}\Big),\qquad u_j=\max\{x_j\sigma_{f,j},-x_j\sigma_{b,j}\}.

For $S\subseteq\{1,2,3\}$ the unified bound is the infimal convolution

\pi(r^0,r)=\min\Big\{\sum_{s\in S}\pi^s(r^{0,s},r^s):\ r^0=\sum_{s\in S}r^{0,s},\ r=\sum_{s\in S}r^s\Big\}.\qquad(25)

All values lie in $[-\infty,+\infty]$ , with the paper's convention that an infeasible minimization has value $+\infty$ and an infeasible maximization $-\infty$ .

Formalization targets

Goal: Theorem 4 (p. 911)

With $\mathbb F=\bigcap_{s\in S}\mathbb F_s$ ,

\sup_{\mathbb P\in\mathbb F}E_{\mathbb P}\big((r^0+r'\tilde\zeta)^+\big)\le\pi(r^0,r)\le\pi^s(r^0,r)\qquad\forall s\in S.\qquad(26)

Milestones

Theorem 1, upper-bound part: $\sup_{\mathbb F_1}E_{\mathbb P}((r^0+r'\tilde\zeta)^+)\le\pi^1(r^0,r)$ .
Theorem 2, upper-bound part: $\sup_{\mathbb F_2}E_{\mathbb P}((r^0+r'\tilde\zeta)^+)\le\pi^2(r^0,r)$ .
Theorem 3: $\sup_{\mathbb F_3}E_{\mathbb P}((r^0+r'\tilde\zeta)^+)\le\pi^3(r^0,r)$ .
The right inequality of (26): $\pi(r^0,r)\le\pi^s(r^0,r)$ for every $s\in S$ .

The tightness halves of Theorems 1 and 2 are the subject of the two companion missions of this series; Theorem 4 does not use them.

Significance

The unified bound turns heterogeneous partial information into one tractable upper bound. When a modeller knows a support set, a covariance and tail information for some independent factors, $\pi$ is valid for the intersected family and is never worse than the best of the separate bounds; it is the bound the paper's deflected and bideflected linear decision rules (§6, (31) onward) use for every recourse term. Theorem 4 is thus the guarantee behind the paper's main approximation scheme, and the same infimal-convolution device applies to any collection of valid bounds on a common convex objective.

The theorems are proved in the paper's electronic companion. To the knowledge of this mission none of them has a machine-checked proof: the Lean library has neither a Scarf-type bound nor a bound on expected positive parts from deviation measures. Formalizing Theorem 3 in particular produces reusable facts about moment generating functions of independent sums under deviation bounds.

Difficulty

The left inequality of (26) looks like bookkeeping, but it rests on three separate bounds, each with its own argument: a weak-duality argument for $\pi^1$ , a Scarf-type mean–variance inequality for $\pi^2$ , and an exponential-moment argument for $\pi^3$ that needs independence of the components of $\tilde z_\sigma$ to factor a moment generating function and the deviation bounds to control each factor. Each piece must be carried out with all values in the extended reals: suprema can be $+\infty$ , families can be empty, and a term equal to $-\infty$ in a sum can absorb a $+\infty$ . The right inequality depends on how each $\pi^s$ behaves at the zero objective, which for $\pi^3$ is an infimum over $\lambda>0$ that is not attained. The naive idea of proving (26) by attainment of the minimum in (25) does not work: the minimum need not be attained, and the statement must hold for every feasible split.

Formalization scope

A distribution is a Measure on Fin N_E → ℝ with IsProbabilityMeasure; $\tilde\zeta$ is the identity map. The mean is the published MomentDRO.Conf.meanVec. $\mathbb F_1$ and $\mathbb F_3$ require integrable coordinates and $\mathbb F_2$ finite second moments, so that means and covariances exist. $\mathbb P(\tilde\zeta\in\mathcal V)=1$ is an almost-everywhere statement. In $\mathbb F_3$ , independence is iIndepFun of the coordinates of $\tilde z_\sigma$ ; every exponential moment $E e^{\theta\tilde z_{\sigma,j}}$ is required finite; and the deviation bounds are the published predicates FwdDevLe, BwdDevLe applied to the law of each coordinate, which state $\frac{2}{\theta^2}\ln E e^{\theta(\tilde z_{\sigma,j}-\hat z_{\sigma,j})}\le\sigma_{f,j}^2$ for all $\theta>0$ , equivalent to the square-root form above for $\sigma_{f,j}\ge0$ .

Worst cases and bounds take values in EReal; the printed "min" of (25) and "inf" of (21), (22), (24) are read as infima, without attainment. In $\psi$ the supremum over $\hat{\mathcal W}_\sigma$ is taken outside the increasing exponential, which gives the same value whenever $\hat{\mathcal W}_\sigma$ is nonempty. The index set $S$ is a nonempty Finset (Fin 3) with index $0,1,2$ for the paper's $1,2,3$ , and vector indices are 0-based.

Two hypotheses come from the paper's model rather than its theorem statements: $\sigma_f,\sigma_b\ge0$ (deviations are square roots), and $F_\sigma\hat\zeta+g_\sigma\in\hat{\mathcal W}_\sigma$ for every $\hat\zeta\in\hat{\mathcal V}$ , which follows from $\hat{\mathcal W}_\sigma=H_\sigma\hat{\mathcal W}$ , $\hat{\mathcal V}=\{\hat\zeta:F\hat\zeta+g\in\hat{\mathcal W}\}$ , $F_\sigma=H_\sigma F$ and $g_\sigma=H_\sigma g$ (pp. 905, 908, 910).

The bounds are defined by (21), (22), (24) and (25) verbatim; a formalization that defines $\pi$ through the worst case itself, sets some $\pi^s$ to $+\infty$ , drops the exponential integrability from $\mathbb F_3$ , or uses real-valued suprema (which return $0$ on unbounded sets) would trivialize or falsify the statement and is ruled out.

Contributions welcome: proofs of the three upper bounds, a Scarf inequality $E X^+\le\frac12(EX+\sqrt{(EX)^2+\operatorname{Var}X})$ as a reusable lemma, and the EReal lemmas about infimal convolutions of extended-real functions.

Selected references

J. Goh, M. Sim, Distributionally Robust Optimization and Its Tractable Approximations, Operations Research 58(4):902–917, 2010. https://doi.org/10.1287/opre.1090.0795
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
W. Chen, M. Sim, Goal-Driven Optimization, Operations Research 57(2):342–357, 2009. https://doi.org/10.1287/opre.1080.0570
H. Scarf, A Min-Max Solution of an Inventory Problem, in Studies in the Mathematical Theory of Inventory and Production, K. Arrow, ed., Stanford University Press, 1958, 201–209.

10 thms2 active usersReviewed

Convex Optimization Optimization·Captain: mikedeng1

Solving Semidefinite-Quadratic-Linear Programs Using SDPT3: The HKM and NT Search Directions of Second-Order Cone Programming Are Invariant Under Automorphic ScalingResearch Paper

Motivation

Second-order cone programming (SOCP) minimizes a linear function over the intersection of an affine subspace with a product of Lorentz cones. It contains convex quadratically constrained programs, robust linear programs with ellipsoidal uncertainty, and many norm-minimization problems, and it is solved in practice by primal–dual interior-point methods. At each iteration such a method computes a search direction from a linearized, symmetrized form of the complementarity conditions; the symmetrization depends on a scaling matrix $G$ , and different choices of $G$ give different directions. The two directions used in practice are the HKM direction (Helmberg–Rendl–Vanderbei–Wolkowicz, Kojima–Shindoh–Hara, Monteiro) and the NT direction (Nesterov–Todd).

A desirable property of a search direction is scale invariance: if the problem is transformed by an automorphism of the cone, the direction computed for the transformed problem is the image of the original direction. A scale-invariant method behaves identically on all problems related by such a change of coordinates, so its behaviour does not depend on an arbitrary choice of coordinates within each cone.

Timeline. Tsuchiya (1999, Optim. Methods Softw. 11 & 12, pp. 141–182; reference [27] of the paper) proved that the HKM and NT directions for SOCP are scale invariant, with a two-page argument for each. Tütüncü, Toh and Todd (2003), in the paper that describes the solver SDPT3 version 3.0, derived closed forms for the blocks $(\mathcal E_i)^{-1}\mathcal F_i$ of the Schur complement matrix ((23) for HKM, (29) for NT) and used them to give a short proof of Tsuchiya's result (their Proposition 1).

Setting

There are $n_q$ second-order cone blocks. Block $i$ has dimension $q_i \ge 1$ , and a vector $x_i \in \mathbb R^{q_i}$ is split into its first coordinate $x_i^0$ and the rest $x_i^1$ . The cone is $K_q^{q_i} = \{x : x^0 \ge \|x^1\|_2\}$ , and with $\bar J = \operatorname{diag}(1, -I)$ and $J = -\bar J$ , the function $\gamma(x) = \sqrt{(x^0)^2 - \langle x^1, x^1 \rangle} = \sqrt{x^\top \bar J x}$ is defined on the cone.

The data are matrices $A_i \in \mathbb R^{q_i \times m}$ , a vector $b \in \mathbb R^m$ and vectors $c_i \in \mathbb R^{q_i}$ . The primal problem minimizes $\sum_i \langle c_i, x_i \rangle$ subject to $\sum_i A_i^\top x_i = b$ and $x_i \in K_q^{q_i}$ ; the dual maximizes $b^\top y$ subject to $A_i y + z_i = c_i$ and $z_i \in K_q^{q_i}$ .

The arrow matrix of $v$ is $\operatorname{Arw}(v) = \begin{pmatrix} v^0 & (v^1)^\top \\ v^1 & v^0 I \end{pmatrix}$ . Given an interior iterate $(x, y, z)$ and a scaling block $G_i$ , set

\mathcal E_i = \operatorname{Arw}(G_i^{-1} z_i)\, G_i, \qquad \mathcal F_i = \operatorname{Arw}(G_i x_i)\, G_i^{-1}, \qquad T_{G_i}(x_i, z_i) = \operatorname{Arw}(G_i x_i)(G_i^{-1} z_i).

With $\mu = \langle x, z \rangle / n_q$ and a centering parameter $\sigma$ , a search direction $(\Delta x, \Delta y, \Delta z)$ solves the Newton system

A_i \Delta y + \Delta z_i = c_i - z_i - A_i y, \qquad \sum_i A_i^\top \Delta x_i = b - \sum_i A_i^\top x_i, \qquad \mathcal E_i \Delta x_i + \mathcal F_i \Delta z_i = \sigma\mu\, e_1 - T_{G_i}(x_i, z_i).

The HKM direction takes $G_i$ from the explicit formula (19) in $z_i$ ; the NT direction takes $G_i$ from (20)–(21) in $x_i$ and $z_i$ .

The automorphism group $\mathcal G_i$ of $K_q^{q_i}$ consists of the invertible linear maps $F$ with $F K_q^{q_i} = K_q^{q_i}$ ; these are exactly the matrices with $F^\top \bar J F = \lambda^2 \bar J$ for some $\lambda > 0$ and $F_{00} > 0$ . Scaling by $F = \operatorname{diag}(F_1, \dots, F_{n_q})$ sends the data and iterate to $\hat A_i = F_i^{-1} A_i$ , $\hat b = b$ , $\hat c_i = F_i^{-1} c_i$ , $\hat x_i = F_i^\top x_i$ , $\hat y = y$ , $\hat z_i = F_i^{-1} z_i$ .

Formalization targets

Goal: Proposition 1 (p. 11)

For either direction (HKM or NT), every interior iterate, every $\sigma$ , and every choice of $F_i \in \mathcal G_i$ ,

(\Delta x, \Delta y, \Delta z) \text{ solves the Newton system for } (A, b, c; x, y, z) \iff (F^\top \Delta x,\ \Delta y,\ F^{-1} \Delta z) \text{ solves it for } (\hat A, \hat b, \hat c; \hat x, \hat y, \hat z).

Milestones

In attack order: the identities (31) for $F$ with $F^\top \bar J F = \bar J$ ; the Schur complement reduction (10)–(15); $\operatorname{Arw}(G_i^{-1} z_i) = I$ for HKM; the HKM closed forms (23) and (24)–(25); the right-hand-side formula (28) for both directions; the HKM invariance step of the proof; the NT identities $G_i x_i = G_i^{-1} z_i$ and (29); the NT block formula (30); and the NT invariance step of the proof.

Significance

The proposition shows that SDPT3's two second-order-cone directions do not depend on how each cone is coordinatized. The closed forms (23), (24), (29) and (30) are what SDPT3 uses to assemble the Schur complement matrix: they show that each block is a diagonal matrix plus a low-rank term, which is the basis for its sparse and Sherman–Morrison–Woodbury handling of large cones.

The result is proved twice in the literature (Tsuchiya 1999 and this paper). As far as is known, neither proof has been machine-checked, and no formal library contains the HKM or NT scalings, the arrow matrix of the Jordan algebra of the Lorentz cone, or its automorphism group. This mission produces those definitions and a checked proof. The printed proof assumes $F_i^\top \bar J F_i = \bar J$ , that is $\lambda = 1$ ; the goal covers the whole group $\mathcal G_i$ , so a complete formalization also closes the case $\lambda \ne 1$ , where (31) and the remark that $\omega_i$ is unchanged no longer hold as printed.

Difficulty

Every step is linear algebra, but none is a one-line rewrite. The inverse of $\mathcal E_i$ appears everywhere, so one first needs invertibility of $G_i$ and $\mathcal E_i$ for interior iterates, and the HKM and NT scalings must be shown to satisfy $G_i e_1 = z_i$ and $G_i x_i = G_i^{-1} z_i$ respectively, which are identities involving $\gamma$ , square roots and the denominators $\gamma(z) + z^0$ and $1 + t^0$ . Transporting the Newton system directly through $F$ fails: $\mathcal E_i$ and $\mathcal F_i$ are built from $G_i$ , which is not equivariant in an obvious way, and the HKM scaling at $\hat z_i$ is not $F_i^{-1} G_i$ . For $\lambda \ne 1$ , the quantities $\gamma$ , $\omega$ and $t$ scale by powers of $\lambda$ , and these factors must be tracked until they cancel.

Formalization scope

A block of dimension $q_i$ is Fin (d i + 1) → ℝ, so $q_i = d_i + 1 \ge 1$ ; $x_i^0$ is index 0 and $x_i^1$ the indices Fin.succ j. Mathlib's norm on this type is the sup norm, so every Euclidean quantity is written through $\bar J$ . Interior points are encoded by $x^0 > 0$ and $(x^0)^2 - \langle x^1, x^1 \rangle > 0$ . Matrix inverses are Matrix.inv, which is $0$ on singular input; the milestones that invert a matrix state its invertibility.

Standing assumptions: the problem is a pure SOCP ( $n_s = n_l = 0$ ); the iterate is interior; $\mu = \langle x, z \rangle / n_q$ . The paper's assumption that $A$ has full row rank is dropped, because the goal is stated for solution sets of the Newton system and needs no uniqueness. $\mathcal G_i$ is encoded algebraically (positive multiples of orthochronous Lorentz transformations) rather than as $\{F : F K = K\}$ , so that the goal does not require the classification of cone automorphisms. The goal assumes nothing about the scaled iterate; its interiority is a consequence.

The Newton system is defined by its raw rows with $\mathcal E_i$ , $\mathcal F_i$ from (8) and $G_i$ from (19)/(21). A formalization that defined the direction through the closed forms (23)/(29), or defined $G_i$ implicitly by $G_i e_1 = z_i$ or $G_i x_i = G_i^{-1} z_i$ , would make the goal nearly definitional and is ruled out.

Reusable infrastructure: the arrow matrix and $\gamma$ of the Lorentz cone, the HKM and NT scalings, and the algebra of Lorentz transformations. Contributions toward any milestone, and alternative proofs of the goal that bypass the milestones, are welcome.

Selected references

R. H. Tütüncü, K. C. Toh, M. J. Todd, Solving semidefinite-quadratic-linear programs using SDPT3, Mathematical Programming 95 (2003) 189–217. https://doi.org/10.1007/s10107-002-0347-5
T. Tsuchiya, A convergence analysis of the scaling-invariant primal-dual path-following algorithms for second-order cone programming, Optimization Methods and Software 11 & 12 (1999) 141–182 (reference [27] of the SDPT3 paper; no stable link recorded).
F. Alizadeh, D. Goldfarb, Second-order cone programming, Mathematical Programming 95 (2003) 3–51. https://doi.org/10.1007/s10107-002-0339-5
Yu. Nesterov, M. J. Todd, Self-scaled barriers and interior-point methods in convex programming, Mathematics of Operations Research 22 (1997) 1–42. https://doi.org/10.1287/moor.22.1.1

12 thms2 active usersReviewed

Linear Optimization Optimization Probability·Captain: mikedeng1

Overbooking with Substitutable Inventory Classes: With Semigroup Survivals the Expected Net Revenue Is Componentwise Concave and Submodular in the Overbooking LevelsResearch Paper

Motivation

Airlines, hotels and car-rental firms sell reservations ahead of service, and a fraction of those reservations cancel or do not show up. Overbooking — accepting more reservations than there is capacity — recovers revenue that cancellations would otherwise destroy, at the risk of denying service to some customers. In practice inventory is often substitutable: a passenger booked in economy can be upgraded to business, a guest booked in a standard room can be given a suite. With substitution, the right overbooking level for one reservation class depends on the levels of all the others.

Karaesmen and van Ryzin (Operations Research 52(1):83–104, 2004) model this as a two-period problem: overbooking decisions in a reservation period, followed by an optimal assignment of the customers who actually show up to inventory classes in a service period. Their structural result, Theorem 2, establishes the shape of the expected net revenue as a function of the overbooking levels. That shape is what justifies critical-level booking policies and the stochastic-gradient method of their §4, and it is the textbook account of joint overbooking with substitution (Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004, Proposition 4.4).

Setting

There are $n$ reservation classes $i = 1, \dots, n$ and $m + 1$ inventory classes $j = 0, 1, \dots, m$ . Class $j = 0$ is virtual: assigning a customer to it means the customer is denied service.

Reservation period. The firm holds $x_i$ reservations of class $i$ and chooses overbooking levels $u_i \ge x_i$ . Accepting a class- $i$ reservation earns $r_i$ ; a cancellation of class $i$ is refunded $q_i$ , with $q_i \le r_i$ . The number of class- $i$ customers who survive to the service period is a random variable $Z_i(u_i)$ with values in $\{0, 1, 2, \dots\}$ . The family $\{Z_i(u_i)\}$ has the semigroup property: if $Y_1$ and $Y_2$ are independent with the laws of $Z_i(u_i)$ and $Z_i(s_i)$ , then $Y_1 + Y_2$ has the law of $Z_i(u_i + s_i)$ . The binomial model ( $Z_i(u_i) \sim \mathrm{Bin}(u_i, p_i)$ for integer $u_i$ ) and the Poisson model ( $Z_i(u_i) \sim \mathrm{Poisson}(u_i p_i)$ ) both have it. The survivals of different classes are independent.

Service period. Given the survivals $z = (z_1, \dots, z_n) \ge 0$ , net benefits $a_{ij}$ (of either sign) and capacities $c_j$ , the firm solves the transportation problem

V_0(z, c) = \max \sum_{i=1}^n \sum_{j=0}^m a_{ij} y_{ij} \quad \text{s.t.} \quad \sum_{j=0}^m y_{ij} = z_i, \ \ \sum_{i=1}^n y_{ij} \le c_j, \ \ y_{ij} \ge 0.

Expected net revenue. The objective of the reservation period is

G(u) = \sum_{i=1}^n r_i (u_i - x_i) - \mathbb E\Big[\sum_{i=1}^n q_i\big(u_i - Z_i(u_i)\big)\Big] + \mathbb E\big[V_0(Z(u), c)\big],

to be maximized over $u \ge x$ .

A function $f$ on $\mathbb R^n$ is submodular on $S$ if $f(s \vee s') + f(s \wedge s') \le f(s) + f(s')$ for $s, s' \in S$ , with $\vee, \wedge$ the componentwise maximum and minimum.

Formalization targets

Goal: Theorem 2

For every $u$ with levels in the parameter set $P$ , every class $i$ and all $\varepsilon, \alpha \in P$ ,

G(u + (\varepsilon + \alpha) e_i) - G(u + \alpha e_i) \le G(u + \varepsilon e_i) - G(u),

and $G$ is submodular on $P^n$ :

G(u \vee u') + G(u \wedge u') \le G(u) + G(u').

The first statement is the paper's componentwise concavity (6); the second is its submodularity, proved in the paper through the pairwise inequality (7) and Theorem 1.

Milestones

LP duality for the transportation problem (§2.2, p. 86): for $z \ge 0$ the primal attains its optimum and equals the dual optimum.
Lemma 1: $V_0(\cdot, c)$ is submodular on $\mathbb R^n_{\ge 0}$ .
Lemma 2: $V_0$ is concave in $(z_1, \dots, z_n)$ and concave in $(c_1, \dots, c_m)$ .
Theorem 1: on a product set, submodularity is equivalent to decreasing differences.
Under the semigroup property, $\mathbb E[Z_i(u_i)]$ is additive in $u_i$ .
The semigroup representation $\mathbb E[V_0(Z(u + \varepsilon e_i))] = \mathbb E[V_0(Z(u) + Y e_i)]$ with $Y$ independent of $Z(u)$ and distributed as $Z_i(\varepsilon)$ .
The sample-path inequalities of the proof: nonincreasing increments of $V_0$ along one coordinate, and the pairwise submodularity inequality for two coordinates.

Significance

Componentwise concavity of $G$ implies that for each reservation class there is a critical booking level beyond which expected revenue does not increase, other levels held fixed. Submodularity implies that these critical levels are nonincreasing in the bookings accepted for any other class: heavier overbooking in one class leaves less spare substitute capacity for the others. These two properties underpin the heuristics and the stochastic-gradient optimization of §4–§5 of the paper.

The result is proved in the paper (for $n = 2$ , with the general case described as straightforward). A machine-checked version would cover the general semigroup case, which includes the binomial model the paper calls realistic, real-valued levels and arbitrary step sizes. The platform already holds a proved special case, RevenueManagement.joint_overbooking_concave_submodular (Talluri–van Ryzin, Proposition 4.4): Poisson survivals, integer levels and unit steps only. This mission generalizes it in all three respects and also formalizes the transportation-problem facts (LP duality, submodularity and concavity of $V_0$ ) as reusable statements.

Difficulty

The obvious route — differentiate $G$ and use concavity of $V_0$ — fails twice. First, $V_0$ is piecewise linear and the survivals are discrete, so there is nothing to differentiate; under the binomial model $G$ is only defined at integer levels. Second, concavity of $V_0$ alone does not survive the expectation: $\mathbb E[V_0(Z(u))]$ is a mixture over laws that change with $u$ , and a concave function of a random vector whose law moves with the parameter need not be concave in the parameter. The semigroup property is what replaces a change of law by the addition of an independent block of survivors, and that coupling must be built for every coordinate and every pair of coordinates at once. On the LP side, submodularity of a transportation-problem value in its demands is a lattice-programming fact (Topkis, Theorem 3.4.1; Shapley 1962), not a consequence of concavity.

Formalization scope

All declarations are in the namespace SubstOverbooking.Structure. Reservation classes are Fin n (0-based), inventory classes Fin (m + 1) with 0 the virtual denied-service class. Conventions committed to:

Uncapacitated virtual class. The paper gives class 0 "finite but very high capacity" and then needs it to absorb every survivor; with Poisson survivals no finite capacity does. Constraint (4) is imposed only for $j \ne 0$ , $c_0$ is unused, and the dual fixes $\lambda_0 = 0$ . Capacities satisfy $c_j \ge 0$ for $j \ne 0$ .
$V_0$ on real demands. $V_0$ is the supremum of the TP objective over feasible assignments, for real $z$ ; every statement assumes $z \ge 0$ , where the supremum is attained and finite.
Survival laws. Each class has a family $u \mapsto L_i(u)$ of probability mass functions on $\mathbb N$ , with finite means. Levels range over a parameter set $P \subseteq [0, \infty)$ that contains $0$ and is closed under addition and under nonnegative differences: $P = \mathbb N$ covers the binomial model, $P = [0, \infty)$ the Poisson model. The semigroup property is the identity of laws $L_i(u + s) = (L_i(u) \otimes L_i(s)) \circ (+)^{-1}$ for $u, s \in P$ , and independence across classes is the product law.
Concavity is stated as the increment inequality (6), which is meaningful on a discrete $P$ ; submodularity of $G$ is lattice submodularity on $P^n$ via the published SupermodularOn applied to $-G$ .
Theorem 1 is stated for product sets $S = T_1 \times \dots \times T_n$ ; as printed for arbitrary $S \subset \mathbb R^n$ it is false, and every set the paper applies it to is a product.
The refund condition $q_i \le r_i$ is kept as a hypothesis of the goal, as on the page.

A formalization that fixes Poisson laws, integer levels or unit steps, or that defines $G$ or $V_0$ through the inequalities to be proved, is the already-proved special case or an empty statement, and is not the goal.

A complete development needs finite LP duality for the transportation problem, the lattice-programming argument for Lemma 1, product measures and image measures on $\mathbb N^n$ , and the coupling of the semigroup property. The LP and lattice parts are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Lemma 1 (for instance via monotonicity of optimal duals, after Erlenkotter 1970).

Selected references

I. Karaesmen and G. van Ryzin, Overbooking with Substitutable Inventory Classes, Operations Research 52(1):83–104, 2004. https://doi.org/10.1287/opre.1030.0079
K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004, §4.4. https://doi.org/10.1007/b139000
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998, Theorem 3.4.1. https://doi.org/10.1515/9781400822539
R. K. Sundaram, A First Course in Optimization Theory, Cambridge University Press, 1996. https://doi.org/10.1017/CBO9780511804526
L. S. Shapley, Complements and substitutes in the optimal assignment problem, Naval Research Logistics Quarterly 9(1):45–48, 1962. https://doi.org/10.1002/nav.3800090106
M. Shaked and J. G. Shanthikumar, Stochastic convexity and its applications, Advances in Applied Probability 20(2):427–446, 1988. https://doi.org/10.2307/1427398

11 thms2 active usersReviewed

Convex Optimization Optimization·Captain: mikedeng1

On Implementing a Primal-Dual Interior-Point Method for Conic Quadratic Optimization IV: The Nesterov–Todd Scaling of a Quadratic or Rotated Quadratic Cone Is W = −Q + (e₁ + w)(e₁ + w)ᵀ/(1 + w₁)Research Paper

Why the Nesterov–Todd scaling of a second-order cone matters

Conic quadratic (second-order cone) programs are solved in practice by primal-dual interior-point methods. Each iteration solves a Newton system for the central-path equations, and for non-polyhedral cones that system is only guaranteed to be well posed after the problem is scaled: the primal point $x$ and the dual slack $s$ are transformed by a matrix $\Theta W$ chosen from the current iterate. Among the scalings analysed by Monteiro and Tsuchiya (2000), the best complexity bounds are obtained with the Nesterov–Todd (NT) scaling of Nesterov and Todd (1997), which maps $x$ and $s$ to the same point.

Andersen, Roos and Terlaky (2003) describe the conic quadratic interior-point solver of MOSEK. Their Lemma 4.2 gives the NT scaling in closed form for each of the three cone types they use. It is what makes the NT direction cheap: each cone block of $W$ is determined by one vector $w$ , and $W$ , $W^2$ and their inverses can be applied in time linear in the dimension. For the quadratic cone the formula goes back to Tsuchiya (1999); the paper re-derives it and extends it to the rotated quadratic cone.

Setting

Fix one cone block of dimension $d$ . Coordinates are $x = (x_1,\dots,x_d)$ , $x_{k:d}$ denotes the subvector of coordinates $k,\dots,d$ , and $\|\cdot\|$ is the Euclidean norm. The block is one of

the positive half-line $\mathbb R_+$ ( $d=1$ ), with $T = Q = 1$ ;
the quadratic cone $K^q = \{x : x_1 \ge \|x_{2:d}\|\}$ ( $d\ge1$ ), with $T = I$ and $Q = \operatorname{diag}(1,-1,\dots,-1)$ ;
the rotated quadratic cone $K^r = \{x : 2x_1x_2 \ge \|x_{3:d}\|^2,\ x_1,x_2\ge0\}$ ( $d\ge2$ ), with $T$ the identity except for the leading block $\tfrac1{\sqrt2}\begin{bmatrix}1&1\\1&-1\end{bmatrix}$ , and $Q$ the matrix with $Q_{12} = Q_{21} = 1$ , $Q_{jj} = -1$ for $j\ge3$ , and zeros elsewhere.

A scaling matrix (Definition 3.3) is a symmetric positive definite $W$ with $WQW = Q$ . For $\theta>0$ the scaled points are $\bar x = \theta W x$ and $\bar s = (\theta W)^{-1}s$ . The pair $(\theta, W)$ is an NT scaling of $(x, s)$ when $\bar x = \bar s$ , equation (28); equivalently $s = \theta^2W^2x$ , equation (29).

Formalization targets

Goal: Lemma 4.2 (p. 15)

For $x, s$ in the interior of the cone:

every NT scaling satisfies

\theta^2 = \sqrt{\frac{s^TQs}{x^TQx}};\qquad(30)

with this $\theta$ and

w = \frac{\theta^{-1}s + \theta Qx}{\sqrt2\sqrt{x^Ts + \sqrt{x^TQx\,s^TQs}}},\qquad(32)

the following matrices $W$ make $(\theta, W)$ an NT scaling: $W = \theta^{-1}(X^{-1}S)^{1/2}$ for $\mathbb R_+$ ;

W = \begin{bmatrix} w_1 & w_{2:d}^T\\ w_{2:d} & I + \frac{w_{2:d}w_{2:d}^T}{1+w_1}\end{bmatrix} = -Q + \frac{(e_1+w)(e_1+w)^T}{1+e_1^Tw}\qquad(31)

for $K^q$ ; and

W = -Q + \frac{(Te_1+w)(Te_1+w)^T}{1+e_1^TTw}\qquad(34)

for $K^r$ . In the last two cases $W^2 = -Q + 2ww^T$ , equations (33) and (35).

Milestones

Lemma 3.3 i)–iii) (scaling preserves $x^Ts$ and rescales $x^TQx$ , $s^TQs$ by $\theta^{\pm2}$ ); (30) on its own; the normalization $w_1^2 - \|w_{2:d}\|^2 = 1$ and the square (62) of the arrow form (31); positivity of the radicand of (32); the identity $2\theta^2(w^Tx)^2 = x^Ts + \sqrt{x^TQx\,s^TQs}$ and the formula (32); for the rotated cone, the transport (63) by $T$ , the identities $\hat\theta = \theta$ and $\hat w = Tw$ , and $TWT = \hat W$ . Two companions: Lemma 4.3, $(\theta W)^{-2} = \theta^{-2}QW^2Q$ , and Lemma 3.3 iv), that a scaling maps the cone and its interior onto themselves.

Significance

The result. Lemma 4.2 turns the NT scaling, defined implicitly by (28), into explicit data: one scalar $\theta$ and one vector $w$ per cone. Combined with Lemma 4.3 it shows that every product with $W$ , $W^2$ or their inverses in the scaled Newton system (27) is a rank-one correction of a signature matrix, which is what the paper's implementation relies on. The rotated-cone formula (34) is the paper's own addition and is what lets rotated cones be handled natively instead of through a change of variables.

Formalizing it. The result is proved on paper; no machine-checked version is known to exist, and the platform has no formalization of second-order-cone scalings. The work is the matrix algebra of the Lorentz group — the signature matrix $Q$ , the matrices with $WQW = Q$ , and their action on $K^q$ and $K^r$ — which is reusable for every second-order-cone algorithm.

Difficulty

Most of the items are finite-dimensional identities, but they are identities between block matrices of arbitrary size with entries that are nested square roots, and they hold only on the interior of the cone, where the radicands are positive. The derivation in the paper runs backwards: it assumes $W$ has the shape (31) and solves for $w$ , taking a square root without fixing its sign. The goal asks for the forward direction — that the displayed $\theta$ , $w$ , $W$ do satisfy (28) and $W\succ0$ — which needs the normalization $w^TQw = 1$ , positive definiteness of $-Q + (e_1+w)(e_1+w)^T/(1+w_1)$ , and, for the rotated cone, the reduction to the quadratic cone through $T$ with $TT = I$ and $TQ^rT = Q^q$ .

Formalization scope

Per block. Every statement is made for one cone block. $\Theta$ and $W$ are block diagonal (pp. 11–12), so this is the paper's statement block by block. The cone type is the parameter kind : ConeKind, and vectors are Fin d → ℝ.
Index base and norms. The paper's $x_1$ is coordinate 0. $\|x_{2:d}\|^2$ is written as a sum of squares (tailSq x 1); Mathlib's norm on Fin d → ℝ, which is the sup norm, is never used.
Interiors. The interiors are given by strict inequalities. The paper never defines $\operatorname{int}(K)$ concretely; these coincide with the topological interiors.
Added hypotheses. All are disclosed in the items:
- the dimension conventions ( $d=1$ for $\mathbb R_+$ , $d\ge1$ for $K^q$ , $d\ge2$ for $K^r$ ), which the paper leaves implicit;
- $\theta>0$ in Definition 3.3, which the paper calls positive definite on p. 24;
- $1+w_1>0$ wherever the page divides by $1+w_1$ ;
- $w^Tx>0$ for the last step of the derivation of (32), where the page silently fixes this sign.
Inverses. The matrix inverse is Mathlib's total inverse. The NT predicate always contains $W\succ0$ , so (28) never reads the junk value of a singular inverse.
Reading of Lemma 4.2. The lemma names $\theta$ and $W$ without quantifying them. The goal states (30) for every NT scaling and asserts that the displayed formulas are an NT scaling. It does not claim that the NT scaling is unique, which the paper does not prove.
Ruling out a trivial formalization. Stating only (30) would allow a version that holds vacuously if no NT scaling existed. Part 2 of the goal is what excludes this, and a sanity check exhibits $\theta = 1$ , $W = I$ at $x = s = e_1$ in $K^q$ for $d=2$ .

A complete development needs:

the cone definitions and the matrices $T$ , $Q$ ;
Mathlib's Matrix.PosDef and Matrix.inv;
elementary real square-root algebra.

Lemmas about $\{W : W\succ0,\ WQW = Q\}$ (closure under products and inverses, invariance of $K^q$ ) are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for positive definiteness of (31).

Selected references

E. D. Andersen, C. Roos, T. Terlaky, On implementing a primal-dual interior-point method for conic quadratic optimization, Mathematical Programming 95 (2003) 249–277; authors' preprint of 18 Dec 2000. https://doi.org/10.1007/s10107-002-0349-3
Yu. E. Nesterov, M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Mathematics of Operations Research 22(1) (1997) 1–42. https://doi.org/10.1287/moor.22.1.1
R. D. C. Monteiro, T. Tsuchiya, Polynomial convergence of primal-dual algorithms for the second-order cone program based on the MZ-family of directions, Mathematical Programming 88(1) (2000) 61–83. https://doi.org/10.1007/PL00011378
T. Tsuchiya, A convergence analysis of the scaling-invariant primal-dual path-following algorithms for second-order cone programming, Optimization Methods and Software 11–12 (1999) 141–182. https://doi.org/10.1080/10556789908805750
F. Alizadeh, D. Goldfarb, Second-order cone programming, Mathematical Programming 95 (2003) 3–51. https://doi.org/10.1007/s10107-002-0339-5

15 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

On Implementing a Primal-Dual Interior-Point Method for Conic Quadratic Optimization III: A Newton Step Scales the Homogeneous Residuals and the Complementarity Gap by 1 − α(1 − γ)Research Paper

Motivation

Conic quadratic optimization — linear optimization over products of quadratic (second-order, Lorentz) cones — covers robust linear programming, portfolio problems with risk constraints, norm minimization and many engineering design problems. Andersen, Roos and Terlaky describe the primal-dual interior-point method implemented in the MOSEK optimizer for this problem class (Math. Program. 95 (2003)). Their algorithm does not solve the primal and dual problems directly. It solves the homogeneous model, an embedding that has a solution whether or not the original problem is feasible, and from which either an optimal pair or a certificate of infeasibility is read off.

The convergence argument of such a method rests on one algebraic property of its search direction: a step along the Newton direction reduces the infeasibility of the homogeneous model and its complementarity gap at the same rate. For linear programming this is classical (Xu, Hung and Ye, 1996; Andersen and Andersen, 2000). This mission formalizes the conic quadratic version, Lemma 4.1 of the paper, in which the diagonal complementarity products of linear programming are replaced by arrow-head matrices.

Setting

The cone is a product $K = K^1\times\cdots\times K^k$ . Each factor $K^i\subseteq\mathbb R^{n^i}$ is one of three kinds:

the half-line $\mathbb R_+ = \{x\in\mathbb R : x\ge0\}$ , with $n^i = 1$ ;
the quadratic cone $K^q = \{x\in\mathbb R^{n} : x_1^2\ge\|x_{2:n}\|^2,\ x_1\ge0\}$ , with $n^i\ge1$ ;
the rotated quadratic cone $K^r = \{x\in\mathbb R^{n} : 2x_1x_2\ge\|x_{3:n}\|^2,\ x_1,x_2\ge0\}$ , with $n^i\ge2$ .

Vectors are partitioned by cones, $x = (x^1;\dots;x^k)$ , and $x^Ts = \sum_i (x^i)^Ts^i$ . To each cone is attached a symmetric orthogonal matrix $T^i$ : the identity for $\mathbb R_+$ and $K^q$ , and for $K^r$ the identity with its leading $2\times2$ block replaced by $\frac{1}{\sqrt2}\begin{bmatrix}1&1\\1&-1\end{bmatrix}$ . For $v\in\mathbb R^d$ the arrow-head matrix is

\operatorname{mat}(v) = \begin{bmatrix} v_1 & v_{2:d}^T\\ v_{2:d} & v_1 I\end{bmatrix}.

At a point $(x,s)$ put $X^i = \operatorname{mat}(T^ix^i)$ , $S^i = \operatorname{mat}(T^is^i)$ , and let $X$ , $S$ , $T$ be block diagonal with blocks $X^i$ , $S^i$ , $T^i$ . Let $e^i$ be the first unit vector of $\mathbb R^{n^i}$ and $e = (e^1;\dots;e^k)$ .

The data are $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ . A current point is $(x^{(0)},\tau^{(0)},y^{(0)},s^{(0)},\kappa^{(0)})$ , with

\mu^{(0)} = \frac{(x^{(0)})^Ts^{(0)} + \tau^{(0)}\kappa^{(0)}}{k+1}.

For a centering parameter $\gamma\in[0,1]$ the Newton direction $(d_x,d_\tau,d_y,d_s,d_\kappa)$ solves the linear system (22):

\begin{aligned} A d_x - b d_\tau &= (\gamma-1)(Ax^{(0)} - b\tau^{(0)}),\\ A^Td_y + d_s - c d_\tau &= (\gamma-1)(A^Ty^{(0)} + s^{(0)} - c\tau^{(0)}),\\ -c^Td_x + b^Td_y - d_\kappa &= (\gamma-1)(-c^Tx^{(0)} + b^Ty^{(0)} - \kappa^{(0)}),\\ X^{(0)}Td_s + S^{(0)}Td_x &= -X^{(0)}S^{(0)}e + \gamma\mu^{(0)}e,\\ \tau^{(0)}d_\kappa + \kappa^{(0)}d_\tau &= -\tau^{(0)}\kappa^{(0)} + \gamma\mu^{(0)}. \end{aligned}

The new point is $(x^{(1)},\tau^{(1)},y^{(1)},s^{(1)},\kappa^{(1)}) = (x^{(0)},\tau^{(0)},y^{(0)},s^{(0)},\kappa^{(0)}) + \alpha(d_x,d_\tau,d_y,d_s,d_\kappa)$ for a step size $\alpha\in[0,1]$ (23).

Formalization targets

Goal: Lemma 4.1 (p. 13)

Under (22) and (23),

\begin{aligned} Ax^{(1)} - b\tau^{(1)} &= (1-\alpha(1-\gamma))(Ax^{(0)} - b\tau^{(0)}),\\ A^Ty^{(1)} + s^{(1)} - c\tau^{(1)} &= (1-\alpha(1-\gamma))(A^Ty^{(0)} + s^{(0)} - c\tau^{(0)}),\\ -c^Tx^{(1)} + b^Ty^{(1)} - \kappa^{(1)} &= (1-\alpha(1-\gamma))(-c^Tx^{(0)} + b^Ty^{(0)} - \kappa^{(0)}),\\ d_x^Td_s + d_\tau d_\kappa &= 0,\\ (x^{(1)})^Ts^{(1)} + \tau^{(1)}\kappa^{(1)} &= (1-\alpha(1-\gamma))\big((x^{(0)})^Ts^{(0)} + \tau^{(0)}\kappa^{(0)}\big). \end{aligned}

Milestones

(25), p. 13: with $\eta = 1-\gamma$ , the shifted point $\eta(x^{(0)},\tau^{(0)},y^{(0)},s^{(0)},\kappa^{(0)}) + d$ satisfies the three linear equations of the homogeneous model.
(26), p. 13: $0 = (\eta x^{(0)}+d_x)^T(\eta s^{(0)}+d_s) + (\eta\tau^{(0)}+d_\tau)(\eta\kappa^{(0)}+d_\kappa)$ , and its expansion in powers of $\eta$ .
(61), p. 36: $e^TXSe = \sum_i (T^ix^i)^TT^is^i = x^Ts$ for all $x$ , $s$ .
p. 14, first equality: $(x^{(0)})^Td_s + (s^{(0)})^Td_x = e^T(X^{(0)}Td_s + S^{(0)}Td_x)$ , for all vectors.
p. 14, the chain's value: $(x^{(0)})^Td_s + (s^{(0)})^Td_x + \tau^{(0)}d_\kappa + \kappa^{(0)}d_\tau = (\gamma-1)\mu^{(0)}(k+1)$ .
p. 14, orthogonality: $d_x^Td_s + d_\tau d_\kappa = 0$ .

Significance

Lemma 4.1 is what makes the homogeneous algorithm analyzable. Because the three residuals and the gap shrink by the same factor $1-\alpha(1-\gamma)$ , their ratios are invariant along the iterates, and a step with $\gamma<1$ and $\alpha>0$ makes measurable progress toward a solution of the homogeneous model. The paper notes (p. 14) that all properties stated in Lemma 4.1 hold for the Nesterov–Todd-scaled direction (27) as well, the direction actually implemented, for which polynomial complexity is shown by Monteiro and Tsuchiya (2000).

The result is proved on the page; it is not open. As far as the platform's catalogue shows, it has not been formalized. Machine-checked versions exist only for linear-programming analogues, with diagonal complementarity products in place of arrow-head matrices. The formalization adds two things. First, it fixes three printed slips: the third line of (22) prints $\kappa$ for $\kappa^{(0)}$ ; the fourth identity of (24) prints $d_x^Td_s^T$ ; and the proof's evaluation on p. 14 ends with $(\gamma-1)\mu^{(0)}k$ where $(\gamma-1)\mu^{(0)}(k+1)$ is correct, since $e^Te = k$ and the $\tau\kappa$ equation contributes the extra $\mu^{(0)}$ . Second, the arrow-head identities (61) and the p. 14 equality are reusable for missions on the complementarity conditions (Lemma 3.1) and the scaled directions of the same paper.

Difficulty

The first three identities of (24) are linear and follow from the first three lines of (22) alone. The content is in the last two. They need an inner-product identity that turns the fourth line of (22), a statement about arrow-head matrix products, into a statement about the scalar quantity $(x^{(0)})^Td_s + (s^{(0)})^Td_x$ . The naive reading treats $X^{(0)}Td_s$ as an abstract linear image of $d_s$ and loses exactly this link. What is needed is that the first row of $\operatorname{mat}(v)$ is $v^T$ , that $\operatorname{mat}(u)\operatorname{mat}(v)e_1$ has first entry $u^Tv$ , and that every $T^i$ is symmetric and orthogonal. The last fails for the rotated cone when $n^i<2$ , so the dimension conventions are not decoration. The bookkeeping constant $e^Te = k$ must also be tracked correctly; the page itself gets it wrong.

Formalization scope

Representation. Blocks are indexed by Fin k; block $i$ is Fin (n i) → ℝ, and indices are 0-based (the paper's $v_1$ is v 0). $A$ is given by its column blocks $A^i$ , so $Ax = \sum_iA^ix^i$ , $(A^Ty)^i = (A^i)^Ty$ and $c^Tx = \sum_i (c^i)^Tx^i$ . The second line of (22) and of (24), and the fourth line of (22), are stated block by block; this is equivalent because $X$ , $S$ , $T$ are block diagonal.
Definitions. The shared module ConicQuadIPM.Complementarity.Setting provides the cone kinds, $T^i$ (Tmat), $\operatorname{mat}(v)$ (arrow), $e^i$ (e1) and the predicate WellFormed; this mission's ConicQuadIPM.NewtonStep.Setting adds $\mu^{(0)}$ (mu0) and the system (22) (NewtonSystem). WellFormed is the paper's implicit dimension convention ( $n^i = 1$ , $\ge1$ , $\ge2$ for the three kinds).
Hypotheses. Every theorem assumes WellFormed. This is a disclosed addition: the paper never states the dimensions, and without them a block of dimension $0$ breaks $e^Te = k$ . The ranges $\alpha\in[0,1]$ and $\gamma\in[0,1]$ are kept as on the page, although the identities hold for all real values. No interiority or cone membership of the current point is assumed, because Lemma 4.1 does not use any. The $\kappa$ of (22)'s third line is $\kappa^{(0)}$ .
No trivialization. The fourth line of (22) must stay in terms of arrow and Tmat. Replacing $X^{(0)}Td_s$ by an abstract linear map, or by $(x^{(0)})^Td_s$ directly, would turn milestone 4 into a definition and empty the goal. Milestone 5 states the corrected constant $k+1$ ; the printed $k$ is false whenever $\gamma\ne1$ and $\mu^{(0)}\ne0$ .
Reusable parts. The arrow-head lemmas (first row of $\operatorname{mat}(v)$ , $e_1^T\operatorname{mat}(u)\operatorname{mat}(v)e_1 = u^Tv$ , symmetry and orthogonality of $T^i$ ) are useful beyond this mission. Contributions of these as separate lemmas are welcome.

Selected references

E. D. Andersen, C. Roos, T. Terlaky, On implementing a primal-dual interior-point method for conic quadratic optimization, Mathematical Programming 95 (2003) 249–277; cited from the authors' preprint of 18 December 2000. https://doi.org/10.1007/s10107-002-0349-3
X. Xu, P.-F. Hung, Y. Ye, A simplified homogeneous and self-dual linear programming algorithm and its implementation, Annals of Operations Research 62 (1996) 151–171. https://doi.org/10.1007/BF02206815
E. D. Andersen, K. D. Andersen, The MOSEK interior point optimizer for linear programming: an implementation of the homogeneous algorithm, in High Performance Optimization, Kluwer (2000) 197–232. https://doi.org/10.1007/978-1-4757-3216-0_8
R. D. C. Monteiro, T. Tsuchiya, Polynomial convergence of primal-dual algorithms for the second-order cone program based on the MZ-family of directions, Mathematical Programming 88 (2000) 61–83. https://doi.org/10.1007/PL00011378

9 thms2 active usersReviewed

Bandit Algorithms Probability·Captain: mikedeng1

Linearly Parameterized Bandits 2: Under Smooth Best Arm Response, the Phased Exploration and Greedy Exploitation Policy Has Regret at Most a₁(‖z‖ + 1/‖z‖)r√TResearch Paper

Motivation

In a linearly parameterized bandit, a decision maker repeatedly chooses an arm from a possibly infinite set of vectors and receives a noisy reward whose mean is linear in an unknown parameter. Classical bandit policies treat arms as independent and must try each arm, so their regret grows with the number of arms (Lai and Robbins 1985); in applications such as marketing, where similar products are expected to have similar sales, the linear structure lets one observation inform many arms, and the regret can be made independent of the number of arms. Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, Mathematics of Operations Research 2010) show that when the arms form the unit sphere of $\mathbb R^r$ , no policy has Bayes risk below order $r\sqrt T$ . This mission concerns their matching upper bound: a simple policy that alternates exploration and greedy exploitation in cycles of growing length attains regret of order $r\sqrt T$ whenever the best arm depends smoothly on the parameter.

The linearly parameterized bandit was studied earlier by Abe and Long (1999), Auer (2002) and, independently of this paper, Dani, Hayes and Kakade (2008), whose policies rely on confidence regions for the parameter. The result here shows that for arm sets with a smooth best arm, such as balls and, by Polovinkin (1996), ellipsoids, a phase-based policy with a single least squares estimate per cycle suffices.

Setting

Let $r \ge 2$ and let $\mathcal U_r \subset \mathbb R^r$ be a compact set of arms. Playing arm $u$ in period $t$ yields the reward

X^u_t = u'Z + W^u_t,

where $Z \in \mathbb R^r$ is an unknown parameter and the errors $W^u_t$ are independent of each other and of $Z$ , identically distributed in $t$ for each arm, with mean zero.

Assumption 1 fixes constants $\sigma_0, \bar u, \lambda_0 > 0$ that do not depend on $r$ : (a) every error satisfies $\mathbb E[e^{xW^u_t}] \le e^{x^2\sigma_0^2/2}$ for all $x \in \mathbb R$ ; (b) every arm has $\|u\| \le \bar u$ , and $\mathcal U_r$ contains linearly independent arms $b_1, \dots, b_r$ with $\lambda_{\min}(\sum_k b_kb_k') \ge \lambda_0$ .

The smooth best arm response condition SBAR( $J$ ) requires that every $z \ne 0$ have a unique best arm $u^*(z)$ , the maximizer of $v'z$ over $\mathcal U_r$ , and that $\|u^*(z) - u^*(y)\| \le J\|z - y\|$ for unit vectors $z, y$ .

The PEGE policy (Phased Exploration and Greedy Exploitation) runs in cycles $c = 1, 2, \dots$ . In cycle $c$ it plays $b_1, \dots, b_r$ once each, computes the ordinary least squares estimate

\widehat Z(c) = \frac1c\Big(\sum_{k=1}^r b_kb_k'\Big)^{-1}\sum_{s=1}^c\sum_{k=1}^r b_k X^{b_k}(s)

from all exploration rewards so far, and then plays a greedy arm $G(c) \in \arg\max_{v \in \mathcal U_r} v'\widehat Z(c)$ for $c$ periods, ties broken arbitrarily.

The regret given $Z = z$ over $T$ periods is $\mathrm{Regret}(z, T, \mathrm{PEGE}) = \sum_{t=1}^T \mathbb E[\max_{v \in \mathcal U_r} v'z - U_t'z \mid Z = z]$ , where $U_t$ is the arm played in period $t$ , and the risk is $\mathrm{Risk}(T, \mathrm{PEGE}) = \mathbb E[\mathrm{Regret}(Z, T, \mathrm{PEGE})]$ for a prior on $Z$ .

Formalization targets

Goal: Theorem 3.1 (p. 15)

Under Assumption 1 and SBAR( $J$ ), there is $a_1 > 0$ depending only on $\sigma_0, \bar u, \lambda_0, J$ such that for every $r \ge 2$ , every $z \ne 0$ and $T \ge r$ ,

\mathrm{Regret}(z, T, \mathrm{PEGE}) \le a_1\Big(\|z\| + \frac1{\|z\|}\Big) r\sqrt T,

and, if $\mathbb E\|Z\| \le M$ and $\mathbb E[1/\|Z\|] \le M$ for every $r$ , there is $a_2$ depending only on $\sigma_0, \bar u, \lambda_0, J, M$ with

\mathrm{Risk}(T, \mathrm{PEGE}) \le a_2\, r\sqrt T.

The constants are unspecified; only the order $r\sqrt T$ and its uniformity in $r$ are asserted.

Milestones on the way

Lemma 3.4 (p. 16): $\mathbb E[\|\widehat Z(c) - z\|^2 \mid Z = z] \le h_1 r/c$ .
Lemma 3.5 (p. 17): $\|w/\|w\| - z/\|z\|\| \le 2\|w - z\|/\max\{\|z\|, \|w\|\}$ .
Lemma 3.6 (p. 17): $\mathbb E[\max_{u} z'(u - G(c)) \mid Z = z] \le r h_2/(c\|z\|)$ .
Sec. 3.1 (p. 18): $\mathrm{Regret}(z, rK + \sum_{c=1}^K c, \mathrm{PEGE}) \le h_3 r\|z\|K + h_4\sum_{c=1}^K r/\|z\|$ .

Further results

Lemma 3.2 (p. 16): a density condition near the origin gives $\mathbb E[1/\|Z\|] \le M$ ; for $Z \sim N(0, I_r/r)$ , $\mathbb E\|Z\| \le 1$ and $\mathbb E[1/\|Z\|] \le \sqrt\pi$ .
The unit ball and the unit sphere satisfy SBAR(1) (pp. 15–16).
Corollary 3.3 (p. 16): on the unit sphere with standard normal errors, $\mathrm{Regret} \le a_3(\|z\| + 1/\|z\|)r\sqrt T$ and, under the prior $N(0, I_r/r)$ , $\mathrm{Risk} \le a_3 r\sqrt T$ .

Significance

Theorem 3.1 with the lower bound of Theorem 2.1 of the same paper identifies $r\sqrt T$ as the optimal order of the regret and the Bayes risk on the unit sphere, and Corollary 3.3 makes this precise. The bound is achieved by a policy with no confidence sets and no per-period optimization beyond one linear maximization per cycle. The factor $\|z\| + 1/\|z\|$ shows how the difficulty depends on the size of the parameter; combined with the trivial bound $2\bar u\|z\|T$ , the regret does not deteriorate as $\|z\| \to 0$ .

The results are proved in the paper; none of them is machine-checked. A formalization yields a verified dimension-explicit regret bound for an explore–exploit policy with a continuum of arms, the least squares error bound under sub-Gaussian noise (Lemma 3.4), and Lipschitz properties of normalization and of the best-arm map on balls, all of which are reusable.

Difficulty

The expected instantaneous regret of a greedy arm computed from a noisy estimate is not obviously small: for a general compact arm set the best arm may jump under a small perturbation of the parameter, and the regret is then of order $\|z\|$ however good the estimate is. The SBAR condition prevents such jumps, but only for unit vectors, so the estimation error must be transferred to the direction of the estimate, which costs a factor $1/\|z\|$ . The estimate may also vanish with positive probability when the errors are discrete, where the greedy arm is arbitrary. Finally, the constants must be uniform in the dimension $r$ : a bound with an $r$ -dependent constant is immediate from $\mathrm{Regret} \le 2\bar u\|z\|T$ , so the content of the theorem lies in keeping every constant independent of $r$ and of the arm set.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin r), so the norm is Euclidean and the inner product is $u'z$ . The model's standing assumptions are encoded as follows: $\mathcal U_r$ is compact; the errors of each arm have mean zero and a law $\nu_u$ ; Assumption 1(a) requires the moment generating function to exist and satisfy the sub-Gaussian bound; Assumption 1(b) writes $\lambda_{\min}(\sum_k b_kb_k') \ge \lambda_0$ as $\lambda_0\|x\|^2 \le \sum_k (b_k'x)^2$ . Every constant is quantified before the dimension $r$ , the arm set, the error laws, the exploration arms, the tie-breaking rule, the prior, $z$ and $T$ ; a version with constants depending on $r$ or on the instance is trivial and is excluded by this quantifier order.

PEGE uses exactly the exploration arms $b_k$ of Assumption 1(b), which are an argument of the policy. The greedy rule is any measurable selection of a maximizer; measurability, implicit on the page, is a hypothesis. Since PEGE uses only exploration rewards, the expectation is over an independent table of exploration errors $W^{b_k}(s)$ with laws $\nu_{b_k}$ , with the parameter fixed to $z$ ("given $Z = z$ "). Regret and risk are lower Lebesgue integrals of nonnegative gaps, valued in $[0, \infty]$ , so an upper bound is never satisfied by a default value of an integral. The moment conditions on the prior are lower Lebesgue integrals, so $\mathbb E[1/\|Z\|] = \infty$ if the prior charges the origin.

Two printed statements are adjusted. Lemma 3.6 is printed "for any $z \in \mathbb R^r$ ", but its bound $r h_2/(c\|z\|)$ is undefined at $z = 0$ ; it is stated for $z \ne 0$ . The p. 18 cycle-sum display is likewise stated for $z \ne 0$ . In Corollary 3.3, the exploration arms are those of Assumption 1(b) with $\bar u = \lambda_0 = 1$ , as in its proof. Measurability of the density in Lemma 3.2(a) is added.

The source is arXiv:0812.3465v2; its printed page numbers equal the PDF page numbers. Contributions welcome: proofs of the milestones, a sub-Gaussian least squares library, and the Lipschitz analysis of best-arm maps.

Selected references

P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, arXiv:0812.3465v2, 2010; Mathematics of Operations Research 35(2), 2010. https://arxiv.org/abs/0812.3465v2
V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT 2008. https://www.learningtheory.org/colt2008/papers/80-Dani.pdf
P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
E. S. Polovinkin, Strongly convex analysis, Sbornik: Mathematics 187(2), 1996. https://doi.org/10.1070/SM1996v187n02ABEH000111

13 thms2 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Distributionally Robust Optimization and Its Tractable Approximations 2: Under a Mean Set and a Known Covariance, the Bound π² Equals the Worst-Case Expected Positive PartResearch Paper

Motivation

Many operations models contain terms of the form $E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big)$ : expected shortfall or overflow of an affine function of an uncertain vector. Inventory and newsvendor costs, penalties for violated soft constraints, and the Conditional Value-at-Risk of a linear decision rule all reduce to it. In practice the distribution $\mathbb P$ of the uncertainty is rarely known; what is known are a few descriptive statistics, such as a range for the mean and an estimate of the covariance. Distributionally robust optimization then replaces the expectation by its supremum over every distribution consistent with that information.

The question goes back to Scarf (1958), who solved a single-product newsvendor problem against the worst distribution with known mean $\mu$ and variance $\sigma^2$ , using the fact that $\sup E(X^+) = \tfrac12\big(\mu + \sqrt{\mu^2 + \sigma^2}\big)$ over such laws; Gallego and Moon (1993) simplified the argument. El Ghaoui, Oks and Oustry (2003) obtained conic representations of worst-case Value-at-Risk under mean and covariance information, and Delage and Ye (2010) studied stochastic programs with uncertain mean and covariance. Goh and Sim (2010) use bounds of this kind inside a general framework for linear optimization under uncertainty with recourse: after a piecewise-linear decision rule is introduced, every expectation in the reformulated problem is of the form above, and the framework needs a tractable, ideally exact, value for its worst case. Section 5.2 of the paper provides it when the information consists of a set containing the mean and the exact covariance.

Setting

A primitive uncertainty $\tilde z \in \mathbb R^{N}$ is represented through a segregated uncertainty $\tilde\zeta \in \mathbb R^{N_E}$ , $N_E \ge N$ , and a fixed matrix $F \in \mathbb R^{N\times N_E}$ and vector $g \in \mathbb R^{N}$ with $\tilde z = F\tilde\zeta + g$ (equation (9) of the paper). The paper notes that $F$ has full row rank. Write $n = N_E$ .

The distributional information is:

a set $\hat{\mathcal V} \subseteq \mathbb R^{n}$ known to contain the mean $\hat\zeta = E_{\mathbb P}(\tilde\zeta)$ (the mean is uncertain, its "support" is $\hat{\mathcal V}$ );
the exact covariance $\Sigma \in \mathbb R^{N \times N}$ of the primitive vector $\tilde z$ .

The family is

\mathbb F_2 = \Big\{\mathbb P :\ \hat\zeta = E_{\mathbb P}(\tilde\zeta) \in \hat{\mathcal V},\ E_{\mathbb P}\big(F(\tilde\zeta - \hat\zeta)(\tilde\zeta - \hat\zeta)'F'\big) = \Sigma\Big\}.

For $r^0 \in \mathbb R$ and $r \in \mathbb R^{n}$ the worst-case expected positive part is $\sup_{\mathbb P \in \mathbb F_2} E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big)$ , and the bound of (22) is

\pi^2(r^0, r) = \inf_{y:\, F'y = r}\ \sup_{\hat\zeta \in \hat{\mathcal V}} \Big\{ \tfrac12 (r^0 + r'\hat\zeta) + \tfrac12 \sqrt{(r^0 + r'\hat\zeta)^2 + y'\Sigma y} \Big\}.

Following the paper (p. 909), an infeasible minimization has value $+\infty$ ; all values are in $[-\infty, +\infty]$ .

Formalization targets

Goal: Theorem 2 (p. 910)

For $F$ of full row rank, $\Sigma$ positive semidefinite and $\hat{\mathcal V}$ nonempty,

\sup_{\mathbb P \in \mathbb F_2} E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big) = \pi^2(r^0, r) \qquad \text{for all } r^0, r.

This is an exact identity; it contains no constants that later work could improve.

Milestones

Upper-bound part of Theorem 2: $\sup_{\mathbb F_2} E_{\mathbb P}((r^0 + r'\tilde\zeta)^+) \le \pi^2(r^0, r)$ , with no hypotheses.
Remark after Theorem 2: for $\Sigma \succeq 0$ , $f(u) = \tfrac12 u + \tfrac12\sqrt{u^2 + y'\Sigma y}$ is nondecreasing in $u$ .
(23): for $\Sigma \succeq 0$ and $\hat{\mathcal V} \neq \emptyset$ ,

\pi^2(r^0, r) = \inf_{u,\, y}\Big\{\tfrac12 u + \tfrac12\sqrt{u^2 + y'\Sigma y} :\ r^0 + \sup_{\hat\zeta \in \hat{\mathcal V}} r'\hat\zeta \le u,\ F'y = r\Big\}.

Tightness part of Theorem 2: $\pi^2(r^0, r) \le \sup_{\mathbb F_2} E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$ under the goal's hypotheses.

Significance

Theorem 2 says that the deterministic problem (22) evaluates the worst case exactly, not merely bounds it. Through (23) it becomes a second-order cone program whenever $\hat{\mathcal V}$ is conic representable, so distributionally robust constraints and objectives with mean–covariance information can be handed to an off-the-shelf conic solver without loss. In the paper, $\pi^2$ is one of three building blocks (with the mean–support bound $\pi^1$ and the directional-deviation bound $\pi^3$ ) that are combined by infimal convolution into the unified bound of Theorem 4, which in turn prices the deflected linear decision rules of §6. Specialized to $N = n$ , $F = I$ and a singleton mean set, it recovers Scarf's mean–variance bound.

The theorem is proved in the paper's online appendix; no machine-checked proof of it, nor of Scarf's bound in this multivariate form, is known to exist. A formalization would certify the exact value, including the cases the printed statement treats only implicitly: $r$ outside the range of $F'$ (both sides $+\infty$ ), a degenerate quadratic form $y'\Sigma y = 0$ , and unbounded mean sets.

Difficulty

The upper bound is a moment inequality and is the easier half. The difficulty is tightness. The supremum over $\mathbb F_2$ is in general not attained, so the proof must exhibit, for every point of $\hat{\mathcal V}$ , distributions on $\mathbb R^{n}$ that meet the full covariance constraint on $F\tilde\zeta$ exactly while driving the expected positive part of the single linear functional $r'\tilde\zeta$ to the bound. The constraint fixes $N(N+1)/2$ second moments, not just the variance of $r'\tilde\zeta$ , so the scalar extremal laws behind Scarf's bound do not directly give members of $\mathbb F_2$ . The case $F'y = r$ infeasible requires showing that the worst case is $+\infty$ , i.e. that $\mathbb F_2$ contains distributions with arbitrarily large expectations; this is where the full-rank assumption on $F$ enters.

Formalization scope

The random vector is the identity on Fin n → ℝ and a distribution is a measure P on it. The mean, the covariance matrix and the finite-second-moment condition come from the published definition MomentDRO_Conf_Setting (meanVec, covMat, HasSecondMoments). The covariance condition is $F\,\mathrm{Cov}_{\mathbb P}(\tilde\zeta)\,F' = \Sigma$ , which equals the paper's $E_{\mathbb P}(F(\tilde\zeta - \hat\zeta)(\tilde\zeta - \hat\zeta)'F')$ by linearity; it constrains the covariance of the primitive vector, an $N \times N$ matrix, not the covariance of $\tilde\zeta$ . The positive part is max · 0. The worst case and $\pi^2$ take values in EReal: an infimum over an empty set is $+\infty$ and a supremum over an empty set is $-\infty$ , matching the paper's convention for infeasible problems. The paper's "inf" and "sup" are not claimed to be attained.

Readings fixed by this mission, each implicit in the paper:

Full row rank of $F$ (p. 906, "F has to be full rank"), stated as surjectivity of $x \mapsto Fx$ ;
$\Sigma$ positive semidefinite, as a covariance matrix must be;
$\hat{\mathcal V}$ nonempty.

Each is needed for the equality: without it $\mathbb F_2$ can be empty (worst case $-\infty$ ) while $\pi^2$ is finite or $+\infty$ . No convexity or closedness of $\hat{\mathcal V}$ is assumed; the theorem does not need it. A formalization that takes the infimum in $\mathbb R$ (where an empty infimum is $0$ ) or states only the inequality $\le$ would trivialize or weaken the theorem and is ruled out.

A complete development needs a Scarf-type mean–variance inequality for $E(X^+)$ , constructions of multivariate distributions with a prescribed mean and covariance (Gaussian or finitely supported laws), and the monotonicity and continuity facts behind (23). The scalar inequality and the constructions of distributions with given first two moments are reusable well beyond this mission. Proofs of any milestone, and supporting lemmas on moment-constrained families, are welcome.

Selected references

J. Goh and M. Sim, Distributionally Robust Optimization and Its Tractable Approximations, Operations Research 58(4), 902–917, 2010. https://doi.org/10.1287/opre.1090.0795
H. Scarf, A min-max solution of an inventory problem, in K. Arrow (ed.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 201–209, 1958.
G. Gallego and I. Moon, The distribution free newsboy problem: Review and extensions, Journal of the Operational Research Society 44(8), 825–834, 1993. https://doi.org/10.1057/jors.1993.141
L. El Ghaoui, M. Oks and F. Oustry, Worst-case value-at-risk and robust portfolio optimization: A conic programming approach, Operations Research 51(4), 543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101
E. Delage and Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3), 595–612, 2010. https://doi.org/10.1287/opre.1090.0741
X. Chen, M. Sim, P. Sun and J. Zhang, A linear decision-based approximation approach to stochastic programming, Operations Research 56(2), 344–357, 2008. https://doi.org/10.1287/opre.1070.0441

8 thms2 active usersReviewed

Optimization Probability·Captain: mikedeng1

Convex Quadratic and Semidefinite Programming Relaxations in Scheduling III: Optimal Nonpreemptive Schedules Are Within 3 of Preemptive Ones for R | rᵢⱼ | Σ wⱼCⱼ, Within 2 Without Release DatesResearch Paper

Motivation

In machine scheduling, preemption means that a job may be interrupted and resumed later, possibly on a different machine. Allowing it can only lower the optimal cost, and a basic question for every scheduling model is how much it can lower it: the ratio between the best nonpreemptive and the best preemptive schedule, often called the power of preemption. For identical parallel machines and the total weighted completion time, McNaughton (1959) showed that preemption does not help at all (doi:10.1287/mnsc.6.1.1). For unrelated machines, where every job has its own processing time on every machine, and with release dates, it does help, and no exact relation is known.

Skutella's paper (J. ACM 48 (2001), doi:10.1145/375827.375840) gives approximation algorithms for unrelated-machine scheduling based on convex quadratic programming relaxations. Its §4 adapts the relaxation of §3 to preemptive schedules and rounds it to a nonpreemptive schedule. A by-product is a constant bound on the power of preemption for $R\mid r_{ij}\mid\sum w_jC_j$ : the factor $3$ , and $2$ without release dates. This mission formalizes that bound together with the steps of §4 that produce it.

Setting

There are $n$ jobs $j$ and $m$ unrelated machines $i$ . Job $j$ has a weight $w_j\ge0$ , and on machine $i$ a processing time $p_{ij}>0$ and a release date $r_{ij}\ge0$ before which it may not be processed there.

A preemptive schedule is a finite list of pieces: job $j$ runs on machine $i$ during $[s,e]$ . Running job $j$ for $\ell$ time units on machine $i$ completes the fraction $\ell/p_{ij}$ of it. A schedule is feasible if every piece of $j$ on $i$ starts no earlier than $r_{ij}$ , two pieces on the same machine never overlap, two pieces of the same job never overlap, and the fractions of every job add up to exactly $1$ . The completion time $C_j$ is the end of the last piece of $j$ , and the objective is $\sum_j w_jC_j$ . A schedule is nonpreemptive if every job consists of a single piece.

Smith's order $\prec_i$ on machine $i$ orders the jobs by nonincreasing ratio $w_j/p_{ij}$ , ties broken by index. On each machine the release dates sorted nondecreasingly are $\rho_{i_1}\le\dots\le\rho_{i_n}$ , with $\rho_{i_{n+1}}:=\infty$ , and the time slot $i_k$ is $[\rho_{i_k},\rho_{i_{k+1}})$ . For a preemptive schedule, $a_{i_kj}$ is the fraction of job $j$ processed on machine $i$ inside slot $i_k$ . The convex quadratic program $(CQP'_p)$ asks for $a\ge0$ and $Z$ with $\sum_{i,k}a_{i_kj}=1$ , slot capacities $\sum_j a_{i_kj}p_{ij}\le\rho_{i_{k+1}}-\rho_{i_k}$ , $a_{i_kj}=0$ when $\rho_{i_k}<r_{ij}$ , and

Z\ \ge\ \sum_j w_j\sum_{i,k}a_{i_kj}\Bigl(\rho_{i_k}+\frac{a_{i_kj}}{2}p_{ij}+\sum_{j'\prec_ij}a_{i_kj'}p_{ij'}\Bigr),\qquad Z\ \ge\ \sum_j w_j\sum_{i,k}a_{i_kj}p_{ij}.

Randomized rounding puts job $j$ into slot $i_k$ with probability $a_{i_kj}$ , pairwise independently over jobs, and schedules each slot's jobs back to back in Smith's order from the slot's start.

Formalization targets

Goal: Corollary 4.6, the power of preemption

For every feasible preemptive schedule $P$ there is a feasible nonpreemptive schedule $S$ with

\sum_j w_jC_j(S)\ \le\ 3\sum_j w_jC_j(P),

and if all $r_{ij}=0$ , one with $\sum_j w_jC_j(S)\le 2\sum_j w_jC_j(P)$ . This is the paper's ratio of optima, stated so that no existence of optimal schedules is needed.

Milestones

(24): $\sum_j w_jC_j\ge\sum_j w_j\sum_{i,k}a_{i_kj}p_{ij}$ for every preemptive schedule.
Exchange inequality (proof of Lemma 4.2): inside one slot, Smith's order minimizes $\sum_j a_jw_j\sum_{j'\text{ before }j}a_{j'}p_{ij'}$ over all orders.
(25): the bound (23) with $\prec_i$ replaced by the order of completion times in the schedule.
Lemma 4.2: every preemptive schedule satisfies (23) and (24).
$(CQP'_p)$ is a relaxation: the fractions of every preemptive schedule, with $Z=\sum_j w_jC_j$ , are feasible.
Lemma 4.3: rounding any feasible $(\bar a,Z)$ yields feasible nonpreemptive schedules with $\mathbb E[\sum_j w_jC_j]\le 3Z$ , and $\le 2Z$ when all release dates are $0$ .

Significance

The result gives a constant bound on how much preemption can help on unrelated machines with release dates, a model in which both the preemptive and the nonpreemptive problems are NP-hard (for the preemptive problem even without weights and release dates, by Sitters, J. Algorithms 57 (2005), doi:10.1016/j.jalgor.2004.06.011). The bound comes from an algorithm: a single relaxation that is valid for preemptive schedules, rounded to a nonpreemptive one. The same rounding is a randomized $3$ -approximation for $R\mid r_{ij},pmtn\mid\sum w_jC_j$ and a $2$ -approximation for $R\mid pmtn\mid\sum w_jC_j$ (Theorem 4.5), and since it never preempts, these bounds hold under any communication delays between machines.

The paper proves all of this on paper. As far as a search of the platform shows, none of it is formalized: the only formal preemption result found is McNaughton's theorem for identical machines. The mission produces a machine-checked model of preemptive schedules on unrelated machines with release dates, a checked lower bound on such schedules by a convex quadratic function of their slot fractions, and a checked analysis of pairwise-independent rounding into nonpreemptive schedules.

Difficulty

The natural first idea is to reuse the nonpreemptive relaxation $(CQP)$ of §3, which already allows fractional assignments. It fails. Example 4.1 of the paper gives two jobs on two machines where an optimal preemptive schedule costs $7$ but the corresponding $(CQP)$ value is $7.25$ , so $(CQP)$ is not a relaxation of the preemptive problem. The relaxation must be weakened: the term $(1+a_{i_kj})/2$ of §3 becomes $a_{i_kj}/2$ , and this weakening is what raises the factor from $2$ to $3$ .

Proving that the weaker program is a relaxation (Lemma 4.2) takes real work. The fractions of a job inside a slot of an arbitrary preemptive schedule are scattered, so the bound needs a rearrangement inside each slot by completion times, then an exchange argument that compares this order with Smith's order slot by slot. On the rounding side, Lemma 4.3 reduces to the analysis of §3 (each job's expected completion time is at most twice its value in the relaxation) and, without release dates, to Theorem 2.1 of §2. Both have to be redone here on the slot model.

Formalization scope

Jobs, machines and slots are Fin n, Fin m, Fin n (0-based). The standing assumptions $p_{ij}>0$ , $w_j\ge0$ , $r_{ij}\ge0$ of p. 2 are hypotheses of every theorem. Smith's order is cross-multiplied ( $w_jp_{ik}>w_kp_{ij}$ ), equivalent to the ratio form because $p>0$ . Sorted release dates come from Tuple.sort. The last slot of each machine has no right end, so $\rho_{i_{n+1}}=\infty$ is never a real number, and the slot capacity constraint is imposed only for slots with a successor. A preemptive schedule is a List of pieces with migration allowed and any number of pieces; nonpreemptive means one piece per job. Completion time is the latest end time among a job's pieces.

Added constraint. The display of $(CQP'_p)$ on p. 22 omits the condition $a_{i_kj}=0$ if $\rho_{i_k}<r_{ij}$ (constraint (18) of §3). Without it the rounding can place a job in a slot that opens before its release date, and "computes a nonpreemptive schedule" in Lemma 4.3 fails. It is included here. The fractions of every feasible preemptive schedule satisfy it, so the program remains a relaxation.

Randomized rounding is a probability weight on the finite set of slot assignments with marginals $\bar a$ and pairwise products $\bar a\bar a'$ . Pairwise independence is required, full independence is not, and the expectation is a finite sum. "Without nontrivial release dates" is read as $r_{ij}=0$ for all $i,j$ . Communication delays are not modelled: without them the preemptive class is the largest, so the goal implies the bound for every delay model.

Not formalized: polynomial running time, solving $(CQP'_p)$ within an additive error $\varepsilon$ , derandomization by conditional probabilities (Theorem 4.5), and Corollary 4.4.

The goal is not trivial. Feasible preemptive schedules exist and are not vacuous, since each job's fractions must sum to $1$ and no machine runs two pieces at once. The nonpreemptive schedule is required to be feasible in the same model, and its value is compared with the given schedule's real objective, not with a relaxation value.

A complete development needs: the slot schedule (15)–(17) and its feasibility, the bound $\mathbb E[C_j]\le2\bar C_j$ of §3 (Lemma 3.5) and Theorem 2.1 of §2, both restated on this slot model, and a product-measure argument showing that pairwise-independent rounding exists. The preemptive-schedule model and the slot machinery are reusable for other unrelated-machine results. Contributions to any milestone are welcome, and so are alternative proofs of Lemma 4.2.

Selected references

M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, J. ACM 48(2) (2001) 206–242. https://doi.org/10.1145/375827.375840
W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106
R. McNaughton, Scheduling with deadlines and loss functions, Management Science 6(1) (1959) 1–12. https://doi.org/10.1287/mnsc.6.1.1
A. S. Schulz and M. Skutella, Scheduling unrelated machines by randomized rounding, SIAM J. Discrete Math. 15(4) (2002) 450–469. https://doi.org/10.1137/S0895480199357078
R. Sitters, Complexity of preemptive minsum scheduling on unrelated parallel machines, J. Algorithms 57(1) (2005) 37–48. https://doi.org/10.1016/j.jalgor.2004.06.011

10 thms2 active usersReviewed

Algorithmic Game Theory Optimization·Captain: mikedeng1

How Bad is Selfish Routing? 3: With Finitely Many Agents Splitting Their Flow and x·ℓₑ(x) Convex, a Nash Flow Costs No More Than Any Flow Feasible for Twice the RatesResearch Paper

Motivation

In a road or communication network, traffic is routed by its users, not by a central planner. Each user picks the route that is cheapest for itself, and the resulting equilibrium can be much more expensive for the network as a whole than the best centrally planned routing. Roughgarden and Tardos, How Bad is Selfish Routing? (J. ACM 2002), quantified this loss. Their basic model is nonatomic: infinitely many users, each controlling a negligible amount of traffic. There, the cost of a Nash flow can exceed the optimum by an unbounded factor, but it never exceeds the cost of an optimal flow that routes twice as much traffic (their Theorem 3.1).

Many networks are not like that. A few large operators (internet service providers, freight companies, a navigation app routing its whole user base) each control a strictly positive share of the traffic and can split it over many paths. Section 5.2 of the paper treats this finite splittable model and proves the analogue of the bicriteria bound, Theorem 5.4. This mission formalizes that theorem and the three steps of its proof.

Setting

A network has a finite set $E$ of edges. Each edge $e$ carries a latency function $\ell_e$ , nonnegative, nondecreasing and continuous on $[0,\infty)$ : the delay on $e$ when $x$ units of flow use it is $\ell_e(x)$ .

There are $k$ agents. Agent $i$ must send $r_i>0$ units of flow from a source $s_i$ to a destination $t_i$ , over its set $\mathcal P_i$ of paths. Distinct agents may have the same source and destination; their path sets are then separate copies. A flow $f$ assigns a nonnegative amount $f_P$ to each path; agent $i$ 's part is $f^{(i)}$ , the restriction of $f$ to $\mathcal P_i$ . The flow is feasible for the rates $r$ if $\sum_{P\in\mathcal P_i} f_P = r_i$ for every $i$ , and feasible for $2r$ if each agent instead sends $2r_i$ .

The edge flow $f_e=\sum_{P\ni e} f_P$ is the flow of all agents through $e$ . The latency of a path is $\ell_P(f)=\sum_{e\in P}\ell_e(f_e)$ , and

C(f)=\sum_P \ell_P(f)\,f_P,\qquad C_i(f)=\sum_{P\in\mathcal P_i}\ell_P(f)\,f^{(i)}_P

are the cost of the flow (its total latency) and the cost of agent $i$ . A feasible flow $f$ is at Nash equilibrium if no agent can lower its own cost by rerouting its own flow: for each $i$ , $f^{(i)}$ minimizes $C_i$ given $f^{(j)}$ for $j\neq i$ .

In Lean, edges, paths and agents are Fin J, Fin R and Fin Sd; a path is a $0/1$ incidence column A j r, s r is the agent owning path r, and rate i is $r_i$ . The edge flow linkFlow and the feasible set wardropFeasible come from the published definition KellyStochasticNetworks_Wardrop; pathLatency, cost and the modified latencies barLatency come from the series' shared model definitions (SelfishRouting.Bicriteria), and agentCost and IsSplittableNash are defined in this mission.

Formalization targets

Goal: Theorem 5.4 (p. 20)

If $x\cdot\ell_e(x)$ is convex on $[0,\infty)$ for every edge, $f$ is at Nash equilibrium for the finite splittable instance $(G,r,\ell)$ , and $f^*$ is feasible for $(G,2r,\ell)$ , then

C(f)\le C(f^*).

The comparison flow $f^*$ is arbitrary, so the statement implies the bound against an optimal flow for $2r$ without naming one.

Milestones (proof of Theorem 5.4, p. 20)

The proof uses the modified latencies $\bar\ell_e(x)=\ell_e(f_e)$ for $x\le f_e$ and $\bar\ell_e(x)=\ell_e(x)$ for $x\ge f_e$ , built from the Nash flow $f$ (p. 12). Writing $\bar C(g)=\sum_P\bar\ell_P(g)g_P$ :

$\bar C(f^*) - C(f^*)\le C(f)$ for any flows with nonnegative path flows;
$f$ is optimal for $(G,r,\bar\ell)$ : $\bar C(f)\le\bar C(g)$ for every $g$ feasible for $r$ ;
every $g$ feasible for $2r$ has $\bar C(g)\ge 2C(f)$ .

Significance

Theorem 5.4 says that in a network shared by finitely many traffic-splitting operators, the inefficiency of selfish routing can always be offset by doubling the network's capacity to carry traffic, whatever the network topology and whatever the (convexity-qualified) delay functions. Theorem 3.1 is its limit as the number of agents grows and each share shrinks to zero. The finite splittable model is the setting of later work on atomic splittable routing games and their price of anarchy, which this mission's definitions can serve.

On the formalization side, the result is proved on paper but, as far as a search of the platform and of Mathlib shows, no part of selfish-routing equilibrium theory with finitely many agents has been formalized. The mission provides a reusable encoding of the finite splittable model (per-agent costs, per-agent best responses with all other agents fixed) on top of the published Wardrop definitions, and the three proof steps as separately provable milestones. Milestone 2 is the one with independent content: it turns a game-theoretic equilibrium into the optimum of a convex program.

Difficulty

The obvious attempt copies the proof of Theorem 3.1. That proof uses the nonatomic equilibrium condition: every used path of a commodity has the same, minimal latency $L_i(f)$ , so $\bar\ell_P(g)\ge L_i(f)$ for every path and the lower bound $\bar C(g)\ge 2C(f)$ follows path by path. In the finite splittable model this fails: an agent at equilibrium balances marginal costs $\ell_P(f)+f^{(i)}_P\cdot(\text{slope})$ , not latencies, and its used paths can have different latencies. The proof must go through the optimality of $f$ for the modified program $(G,r,\bar\ell)$ , and that needs both the convexity of $x\cdot\ell_e(x)$ and a comparison between the change of agent $i$ 's cost and the change of the $\bar\ell$ -cost under the same local move. The paper invokes a first-order optimality lemma (its Lemma 2.4) for $\bar\ell$ , which is not differentiable at $f_e$ ; a formal proof has to handle one-sided derivatives or argue by convexity directly.

Formalization scope

Routes, not graphs. Paths are arbitrary $0/1$ incidence columns with an owner map; the paper's simple-path families are one instance. The proof never uses graph structure. Two agents with the same source and destination have disjoint index sets of routes.
Latency hypotheses on $[0,\infty)$ only: 0 ≤ ℓ j t for 0 ≤ t, MonotoneOn and ContinuousOn on Set.Ici 0, and ConvexOn ℝ (Set.Ici 0) (fun t => t * ℓ j t). Continuity replaces the differentiability of §2.1, as footnote 3 (p. 7) and §5.2 allow; this weakens a hypothesis.
Rates are positive (0 < rate i). The case of zero agents is allowed and trivial, as in the paper.
Nash equilibrium is the precise form printed on p. 19: each agent's part minimizes its cost among feasible flows that agree with $f$ on every other agent's paths. A deviating agent keeps its total at $r_i$ and cannot change others' flows; the agent's cost is evaluated at the total edge flow of all agents.
No ratios. The theorem is the inequality $C(f)\le C(f^*)$ for every $f^*$ feasible for $2r$ ; no division by an optimal cost appears.
Feasible for $2r$ is wardropFeasible s (fun i => 2 * rate i).
The existence of a Nash flow (Rosen) is neither assumed nor claimed. A sorry-free check shows the definition is satisfiable: in the two-link Pigou network with one agent of rate 1 and latencies $1$ and $x$ , the flow $(1/2,1/2)$ is a Nash flow.
A trivializing formalization is excluded: the equilibrium is not the Wardrop condition, deviations are restricted to the deviating agent's own feasible flows, and the theorem quantifies over every feasible comparison flow rather than over an assumed optimum.

Contributions welcome: proofs of the three milestones and the goal; a general lemma that a feasible flow minimizing a convex separable edge cost has no improving two-path move, and its converse; a proof that $x\mapsto\bar\ell_e(x)\,x$ is convex when $x\,\ell_e(x)$ is.

Selected references

T. Roughgarden and É. Tardos, How Bad is Selfish Routing?, Journal of the ACM 49(2):236–259, 2002. https://doi.org/10.1145/506147.506153
J. B. Rosen, Existence and Uniqueness of Equilibrium Points for Concave N-Person Games, Econometrica 33(3):520–534, 1965. https://doi.org/10.2307/1911749
F. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 4. https://doi.org/10.1017/CBO9781139565363

8 thms2 active usersReviewed

Algorithmic Game Theory Convex Optimization Optimization·Captain: mikedeng1

How Bad is Selfish Routing? 4: With Polynomial Latencies of Degree p and Nonnegative Coefficients the Cost of a Nash Flow Is at Most p + 1 Times the Optimal CostResearch Paper

Motivation

In a road or communication network carrying a large population of users, each user picks a route that is fastest for itself given the congestion caused by everyone else. The resulting traffic pattern, a Wardrop or Nash equilibrium, need not minimize the total travel time: Braess's paradox shows that adding a road can make every user slower. Transportation science has modelled such equilibria since Wardrop (1952) and Beckmann, McGuire and Winsten (1956), and the question of how much efficiency selfish behaviour costs was posed in computer science by Koutsoupias and Papadimitriou (1999).

Roughgarden and Tardos, How Bad is Selfish Routing? (J. ACM, 2002) gave the first general answers for networks with many infinitesimal users. This mission formalizes the first of them, from §2.5 of the paper: when every edge latency is a polynomial of degree at most $p$ with nonnegative coefficients, the total latency at equilibrium is at most $p+1$ times the optimum. The argument goes through the convex program of Beckmann et al., whose optimal solutions are exactly the equilibria (Dafermos and Sparrow, 1969).

Timeline. 1952: Wardrop states the equilibrium principle. 1956: Beckmann, McGuire and Winsten characterize equilibria as minimizers of a convex potential and prove existence. 1969: Dafermos and Sparrow reprove existence and essential uniqueness for general networks. 1999: Koutsoupias and Papadimitriou introduce the worst-case ratio between equilibrium and optimum. 2000–2002: Roughgarden and Tardos prove the bounds $p+1$ for polynomials (Corollary 2.8) and $4/3$ for linear latencies. 2002–2003: Roughgarden shows the worst ratio for degree- $p$ polynomials is $\Theta(p/\ln p)$ , attained already on two parallel links.

Setting

An instance consists of finitely many edges $e$ , finitely many commodities $i\in\{1,\dots,k\}$ and finitely many routes $P$ . Each route is a set of edges, recorded by a $0/1$ incidence matrix $A$ ( $A_{eP}=1$ iff $e\in P$ ), and serves exactly one commodity; $\mathcal P_i$ is the set of routes serving commodity $i$ . Commodity $i$ has a rate $r_i>0$ .

A flow assigns a value $f_P$ to each route. It induces the edge flows $f_e=\sum_{P\ni e}f_P$ and is feasible if $f_P\ge0$ for all $P$ and $\sum_{P\in\mathcal P_i}f_P=r_i$ for all $i$ . Each edge has a latency function $\ell_e$ , nonnegative, nondecreasing and continuous on $[0,\infty)$ . The latency of a route is $\ell_P(f)=\sum_{e\in P}\ell_e(f_e)$ and the cost of a flow is

C(f)=\sum_P\ell_P(f)\,f_P=\sum_e\ell_e(f_e)\,f_e .

A feasible flow is at Nash equilibrium (Definition 2.1) if moving any amount $\delta\in[0,f_{P_1}]$ of commodity $i$ from a used route $P_1$ to another route $P_2\in\mathcal P_i$ leaves $P_2$ at least as slow, after the move, as $P_1$ was before. Lemma 2.2 shows that this is the Wardrop condition: every route that carries flow has minimum latency among the routes of its commodity.

The Beckmann potential of a flow is $\Phi(f)=\sum_e\int_0^{f_e}\ell_e(t)\,dt$ , the objective of the program (NLP2) of the paper.

Formalization targets

Goal: Corollary 2.8

For latencies $\ell_e(x)=\sum_{i=0}^{p}a_{e,i}x^i$ with $p\ge1$ an integer and $a_{e,i}\ge0$ , every flow $f$ at Nash equilibrium and every feasible flow $f^*$ satisfy

C(f)\le(p+1)\,C(f^*).

This is the paper's $\rho(G,r,\ell)=C(f)/C(f^*)\le p+1$ written without division.

Milestones

Lemma 2.2: Nash equilibrium (Definition 2.1) $\iff$ the Wardrop condition.
Proof of Lemma 2.6: the flows at Nash equilibrium are exactly the feasible minimizers of $\Phi$ .
Lemma 2.6: a Nash flow exists, and all Nash flows have the same cost.
Corollary 2.7: if $x\,\ell_e(x)\le\alpha\int_0^x\ell_e(t)\,dt$ for every edge and every $x>0$ , with $\alpha\ge1$ , then

C(f)\le\alpha\,C(f^*)\quad\text{for every Nash flow } f \text{ and feasible } f^* .

Significance

The result. Corollary 2.8 was, according to the authors, the first bound of its kind for polynomial latencies (p. 11). It shows that for the latency functions used in practice (the Bureau of Public Roads function $\ell(x)=a+bx^4$ has $p=4$ ) uncoordinated routing loses at most a bounded factor, independent of the network size, the number of commodities and the rates. Corollary 2.7 isolates the mechanism: a single scalar property of each latency function, how far the cost $x\ell(x)$ can exceed the potential $\int_0^x\ell$ , controls the efficiency loss of the whole network.

Formalizing it. The results are proved in the paper (and the bound $p+1$ has since been sharpened); none of them is machine-checked on the platform. The mission produces a reusable Lean development of nonatomic selfish routing: Definition 2.1 in its deviation form, its equivalence with the Wardrop condition, the Beckmann characterization of equilibria with an honest integral potential, existence and cost-uniqueness of equilibria, and the potential-based efficiency bound. The same layer is used by the companion missions on the bicriteria bound and the $4/3$ bound for linear latencies.

Difficulty

The bound itself is a short chain of inequalities once the equilibrium is known to minimize the potential $\Phi$ . That step is the substance: it requires showing that the Wardrop condition is a first-order optimality condition of a convex program over the polytope of feasible flows, with latencies that are only continuous, so $\Phi$ is differentiable but its derivative may have kinks. Passing from Definition 2.1 (finite deviations) to the Wardrop condition needs a limit $\delta\to0$ , which fails without continuity of the latencies. Mathlib has no Karush–Kuhn–Tucker theory for such programs, so the optimality characterization has to be built from first principles.

Formalization scope

Encoding. Edges, routes and commodities are Fin J, Fin R, Fin Sd. Edge flows, feasibility, the Wardrop condition and the potential $\Phi$ are the published KellyStochasticNetworks.linkFlow, wardropFeasible, IsWardropEquilibrium and wardropObjective, reused unchanged.
Routes, not graphs. Routes are arbitrary $0/1$ incidence columns rather than the simple $s_i$ – $t_i$ paths of a graph, a generalization the paper's arguments never use. Two copies of one path serving two commodities are two routes.
Definition 2.1 is read with $P_1\ne P_2$ and $f_{P_1}>0$ . As printed, $P_1=P_2$ makes the condition fail for strictly increasing latencies, and $f_{P_1}=0$ forces unused routes to have the same latency as used ones; either reading would make Nash flows nonexistent in simple instances.
Latencies are nonnegative, nondecreasing and continuous on $[0,\infty)$ only. Continuity replaces the paper's differentiability, as its footnote 3 allows; it also makes $\int_0^x\ell_e$ a genuine integral.
Rates are positive. In Lemma 2.6's existence part every commodity must be served by a route, the route-encoding meaning of "an instance".
No ratios. Every bound $\rho\le c$ is stated as $C(f)\le c\,C(f^*)$ for every feasible $f^*$ , which is what each proof shows and which avoids division by a zero cost.
Polynomials share one degree bound $p\ge1$ ; leading coefficients may vanish; coefficients are required nonnegative for $i\le p$ .

A statement in which Nash flows cannot exist (the literal Definition 2.1), or in which $\int_0^x\ell_e$ is the junk value of a non-integrable function, would make the goal vacuous; the guards above rule both out, and the sorry-free check that two small instances admit Nash flows confirms it.

Contributions welcome: proofs of the milestones, in particular the first-order characterization of minimizers of $\Phi$ over the feasible polytope, which is reusable for every potential game on flows.

Selected references

T. Roughgarden and É. Tardos, How Bad is Selfish Routing?, J. ACM 49(2):236–259, 2002. https://doi.org/10.1145/506147.506153
M. Beckmann, C. B. McGuire and C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956 (RAND RM-1488). https://www.rand.org/pubs/research_memoranda/RM1488.html
S. C. Dafermos and F. T. Sparrow, The traffic assignment problem for a general network, J. Res. Nat. Bur. Standards 73B(2):91–118, 1969. https://doi.org/10.6028/jres.073B.010
J. G. Wardrop, Some theoretical aspects of road traffic research, Proc. Inst. Civil Engineers, Part II, 1:325–378, 1952. https://doi.org/10.1680/ipeds.1952.11259
E. Koutsoupias and C. Papadimitriou, Worst-case equilibria, STACS 1999, LNCS 1563, 404–413. https://doi.org/10.1007/3-540-49116-3_38
T. Roughgarden, The price of anarchy is independent of the network topology, J. Comput. System Sci. 67(2):341–364, 2003. https://doi.org/10.1016/S0022-0000(03)00044-8

10 thms2 active usersReviewed

Convex Optimization Linear algebra Optimization·Captain: mikedeng1

Semidefinite Programming Relaxations for Semialgebraic Problems 2: A Feasible Solution of the SDPs (7.7) Certifies That M Is Copositive, and the Test Is at Least as Strong as M = P + NResearch Paper

Copositive matrices and why they need certificates

A real symmetric matrix is copositive when its quadratic form is nonnegative on the nonnegative orthant. Copositive matrices appear wherever a quadratic objective meets sign constraints: standard quadratic programs over the simplex, linear complementarity problems, and conic reformulations of combinatorial problems such as the stability number of a graph. Parrilo's §7.5 (Math. Program. 96 (2003) 293–320) gives an example: if $C$ is copositive and $Q - A^TCA \succeq \gamma I$ , then $\gamma$ is a lower bound on $\min\{x^TQx : Ax \ge 0,\ x^Tx = 1\}$ .

Deciding copositivity is hard. Murty and Kabadi (Math. Program. 39 (1987) 117–129) showed that checking whether a given integer matrix is not copositive is NP-complete, so the exact tests based on principal minors take an exponential number of operations in the worst case. Efficiently checkable sufficient conditions are therefore what applications use.

Timeline:

1962. Diananda (Proc. Cambridge Philos. Soc. 58) studies the decomposition of a matrix as positive semidefinite plus elementwise nonnegative, condition (7.6) below, which is sufficient for copositivity and also necessary for $n \le 4$ .
1977. Choi and Lam (Math. Ann. 231) relate this decomposition to sums of squares of quartic forms (their Lemma 3.5).
1987. Murty and Kabadi prove the NP-completeness result above.
2000–2003. Parrilo's thesis and the 2003 paper introduce a hierarchy of semidefinite programming tests, one level per degree $r$ , of which (7.6) is level $0$ ; Theorem 7.7 makes level $1$ explicit.
2002. De Klerk and Pasechnik (SIAM J. Optim. 12) use this hierarchy to approximate the stability number of a graph.

Setting

Fix $n \ge 0$ and a real symmetric matrix $M = (m_{ij}) \in \mathbb R^{n\times n}$ . The matrix $M$ is copositive if

x_i \ge 0 \text{ for all } i \;\Longrightarrow\; x^T M x \ge 0 .

For real variables $z = (z_1,\dots,z_n)$ write $\mathbf z = [z_1^2, \dots, z_n^2]^T$ . Three polynomials in $z$ are associated with $M$ :

P(z) := \mathbf z^T M \mathbf z = \sum_{i,j} m_{ij} z_i^2 z_j^2, \qquad P_r(z) = \Bigl(\sum_{i=1}^n z_i^2\Bigr)^r P(z), \qquad P_1(z) := \sum_{i,j,k} m_{ij} z_i^2 z_j^2 z_k^2 .

A form is positive semidefinite if it is nonnegative at every point of $\mathbb R^n$ , and a polynomial is a sum of squares if it is a finite sum of squares of real polynomials. A matrix $A$ satisfies $A \succeq 0$ if it is symmetric and $x^TAx \ge 0$ for all $x \in \mathbb R^n$ .

The SDPs (7.7) ask for $n$ symmetric matrices $\Lambda^1, \dots, \Lambda^n \in \mathcal S^n$ , with entries $\Lambda^i_{jk} = \Lambda^i_{kj}$ , such that

\begin{aligned} M - \Lambda^i &\succeq 0, && i = 1,\dots,n,\\ \Lambda^i_{ii} &= 0, && i = 1,\dots,n,\\ \Lambda^i_{jj} + \Lambda^j_{ji} + \Lambda^j_{ij} &= 0, && i \ne j,\\ \Lambda^i_{jk} + \Lambda^j_{ki} + \Lambda^k_{ij} &\ge 0, && i \ne j \ne k . \end{aligned}

Condition (7.6) asks for a decomposition $M = P + N$ with $P \succeq 0$ and $n_{ij} \ge 0$ for all $i,j$ .

Formalization targets

Goal: Theorem 7.7

For every real symmetric $n\times n$ matrix $M$ ,

\text{(7.7) feasible} \;\Longrightarrow\; \bigl(P_1(z) \ge 0 \ \ \forall z \in \mathbb R^n\bigr) \ \text{and}\ M \text{ copositive}, \qquad\text{and}\qquad \text{(7.6)} \;\Longrightarrow\; \text{(7.7) feasible}.

The second implication is the paper's "this test is at least as powerful as condition (7.6)".

Milestones (all from §7.5, pp. 317–318)

$P_1 = P_r$ at $r = 1$ : $\bigl(\sum_k z_k^2\bigr)P(z) = \sum_{i,j,k} m_{ij} z_i^2z_j^2z_k^2$ .
If $P_r(z) \ge 0$ for all $z$ , then $P(z) \ge 0$ for all $z$ .
$M$ is copositive if and only if $P(z) \ge 0$ for all $z \in \mathbb R^n$ .
$P(z)$ is a sum of squares if and only if condition (7.6) holds.
If $P_i$ is a sum of squares, then so is $P_{i+1}$ .

Significance

Theorem 7.7 turns copositivity at level $r = 1$ into a single semidefinite feasibility problem whose size is polynomial in $n$ : $n$ symmetric $n \times n$ matrices, $n$ semidefinite constraints and $O(n^3)$ linear ones. Its second half says that nothing is lost against the classical test (7.6): every matrix certified by the decomposition $M = P + N$ is also certified by (7.7). The milestones place the result inside the hierarchy: certificates at any level $r$ certify copositivity (milestones 2 and 3), and the sum-of-squares tests become weakly stronger as $r$ grows (milestone 5), with (7.6) equivalent to the test at level $0$ (milestone 4). This hierarchy underlies later SDP approximations of the copositive cone and of the stability number of a graph.

The paper prints no proof of Theorem 7.7. These statements are proved results of the literature; none of them is formalized in Mathlib or, as far as a search of the platform shows, elsewhere in Lean. The mission produces machine-checked statements and proofs of the level- $1$ test and of the structural facts about the hierarchy, built on the platform's published definition of copositivity.

Difficulty

The first half of Theorem 7.7 requires seeing a feasible point of (7.7) as a certificate for the polynomial $P_1$ : the semidefinite constraints control quadratic expressions in $\mathbf z$ , while the linear constraints on the entries of $\Lambda$ must account for every monomial $z_i^2z_j^2z_k^2$ of degree six, grouped by which indices coincide. The bookkeeping over the three index patterns (all equal, two equal, all distinct) and over the superscript/subscript roles of $\Lambda^i_{jk}$ is where a careless argument loses a term. The second half asks, for an arbitrary decomposition $M = P + N$ , for a point satisfying all $n$ semidefinite constraints and all the linear equalities and inequalities of (7.7) at once. The obvious first idea of testing $M \succeq 0$ fails: positive semidefiniteness is sufficient for copositivity but far from necessary, since every elementwise nonnegative matrix is copositive.

Formalization scope

$M$ is Matrix (Fin n) (Fin n) ℝ with a hypothesis M.IsSymm; $n$ is arbitrary, including $n = 0$ .
Copositivity is the published definition MurtyKabadi.Reduction.Copositive (Murty–Kabadi mission), $x^TMx \ge 0$ for every coordinatewise nonnegative $x$ ; it is not replaced by $M \succeq 0$ .
$P$ , $P_r$ and $P_1$ are elements of MvPolynomial (Fin n) ℝ; $P_1$ is defined by its own display, and its equality with $P_r$ at $r = 1$ is a milestone.
"Positive semidefinite form" and "nonnegative" mean nonnegative evaluation at every point of $\mathbb R^n$ ; "sum of squares" is Mathlib's IsSumSq in the polynomial ring.
$\succeq 0$ is Mathlib's Matrix.PosSemidef. $\Lambda$ is a family Fin n → Matrix (Fin n) (Fin n) ℝ, with $\Lambda^i_{jk}$ = Λ i j k; each $\Lambda^i$ is required symmetric as on the page.
" $i \ne j \ne k$ " is read as $i, j, k$ pairwise distinct. Under the symmetry of the $\Lambda^i$ and the third constraint, the extra constraints of the literal reading hold with equality, so both readings give the same feasible set.
"At least as powerful as condition (7.6)" is formalized as the implication (7.6) $\Rightarrow$ (7.7) feasible.
The mission does not trivialize: the hypothesis of the goal is satisfiable (the identity matrix with $\Lambda = 0$ is feasible), the conclusion is copositivity on the orthant rather than a weaker or vacuous property, and the SDP is the paper's finite system with every constraint of (7.7) present.

Contributions welcome: proofs of the milestones, general lemmas on sums of squares in MvPolynomial (closure under multiplication, Gram-matrix representations of a quadratic form in monomials) and Gram-matrix arguments for forms that are even in every variable.

Selected references

P. A. Parrilo, Semidefinite programming relaxations for semialgebraic problems, Math. Program. Ser. B 96 (2003) 293–320. https://doi.org/10.1007/s10107-003-0387-5
K. G. Murty, S. N. Kabadi, Some NP-complete problems in quadratic and nonlinear programming, Math. Program. 39 (1987) 117–129. https://doi.org/10.1007/BF02592948
P. H. Diananda, On non-negative forms in real variables some or all of which are non-negative, Proc. Cambridge Philos. Soc. 58 (1962) 17–25. https://doi.org/10.1017/S0305004100036185
M. D. Choi, T. Y. Lam, Extremal positive semidefinite forms, Math. Ann. 231 (1977) 1–18. https://doi.org/10.1007/BF01360024
E. de Klerk, D. V. Pasechnik, Approximation of the stability number of a graph via copositive programming, SIAM J. Optim. 12 (2002) 875–892. https://doi.org/10.1137/S1052623401383248

9 thms2 active usersReviewed

Optimization Probability·Captain: mikedeng1

Centralized and Competitive Inventory Models with Demand Substitution 3: Under Multivariate Normal Demand the Centralized Expected Profit Decreases in Every Demand CorrelationResearch Paper

Motivation

A retailer that carries several substitutable products (brands of the same good, sizes of the same item) faces demands that are linked in two ways: a customer who finds the first-choice product out of stock may buy another one, and the first-choice demands themselves are statistically dependent. Inventory planners routinely assume multivariate normal demand and need to know how the dependence between demands affects what the assortment earns. In the single-product newsvendor and in classical risk-pooling arguments, positive correlation is known to hurt; with substitution it is not obvious, because substitution is itself a form of pooling whose value depends on whether two products run out together.

Netessine and Rudi (SSRN 303779, 2002; journal version in Operations Research 51(2), 2003) settle the question for the centralized model with an arbitrary number of products: under multivariate normal demand, the retailer's expected profit decreases in every demand correlation. The authors note that this effect had been observed numerically by Rajaram and Tang (working paper, UCLA, 1999) and Ernst and Kouvelis (1999) but not proved. They prove the analogous statement for each firm in the competitive model with stocking quantities held fixed.

Setting

There are $n$ products. Product $i$ is stocked in quantity $Q_i\ge 0$ at unit cost $c_i$ , sold at price $r_i$ , and salvaged at value $s_i$ , with $r_i>c_i>s_i>0$ . Write $u_i=r_i-c_i$ (underage cost) and $o_i=c_i-s_i$ (overage cost). The substitution fraction $a_{ij}\in[0,1]$ is the share of the unmet demand for product $i$ that switches to product $j$ ; $a_{ii}=0$ and $\sum_j a_{ij}<1$ .

The first-choice demand is a random vector $D=(D_1,\dots,D_n)$ . The effective demand of product $i$ , after substitution from the other products, is

D^s_i = D_i + \sum_{j\ne i} a_{ji}\,(D_j-Q_j)^+ ,\qquad x^+=\max(0,x).

For one realization, product $k$ earns

\pi_k(D) = u_kD^s_k - u_k(D^s_k-Q_k)^+ - o_k(Q_k-D^s_k)^+ ,

and a single centralized company owning all products earns $\pi(D)=\sum_k\pi_k(D)$ . The expected profits are $\pi(Q)=\mathbb E\,\pi(D)$ (the paper's equation (1)) and $\pi_k(Q)=\mathbb E\,\pi_k(D)$ (equation (9), the profit of firm $k$ when each product is owned by a separate firm).

In this mission $D\sim N(m,\Sigma)$ is multivariate normal with mean $m\in\mathbb R^n$ and positive semidefinite covariance matrix $\Sigma=(\sigma_{ij})$ . The correlation of products $i\ne j$ is $\rho_{ij}=\sigma_{ij}/\sqrt{\sigma_{ii}\sigma_{jj}}$ . Raising $\rho_{ij}$ means passing from $\Sigma^1$ to $\Sigma^2$ where $\sigma^2_{ij}=\sigma^2_{ji}\ge\sigma^1_{ij}=\sigma^1_{ji}$ and every other entry, in particular every variance, is unchanged.

A function $f:\mathbb R^n\to\mathbb R$ is supermodular if $f(x)+f(y)\le f(x\vee y)+f(x\wedge y)$ for the componentwise maximum and minimum, and submodular if $-f$ is supermodular. A random vector $D^1$ is smaller than $D^2$ in the supermodular order, $D^1\le_{sm}D^2$ , if $\mathbb Ef(D^1)\le\mathbb Ef(D^2)$ for every supermodular $f$ whose expectations exist.

Formalization targets

Goal: Proposition 2 (p. 7)

For $\Sigma^2$ obtained from $\Sigma^1$ by raising one covariance $\sigma_{ij}$ , $i\ne j$ ,

\pi^{\Sigma^2}(Q)\le\pi^{\Sigma^1}(Q)\quad\text{for every } Q\ge 0,

and, for every maximizer $Q^1$ of $\pi^{\Sigma^1}$ and every maximizer $Q^2$ of $\pi^{\Sigma^2}$ over $Q\ge0$ ,

\pi^{\Sigma^2}(Q^2)\le\pi^{\Sigma^1}(Q^1).

These are the two readings of "stocking quantities held fixed or adjusted optimally".

Milestones

The effective demand $h(D)=D_i+\sum_{j\ne i}a_{ji}(D_j-Q_j)^+$ is a valuation (both super- and submodular).
$D\mapsto\min(h(D),Q_i)$ is submodular.
The realized profit $\pi(D)=\sum_i[(u_i+o_i)\min(D^s_i,Q_i)-o_iQ_i]$ , and each $\pi_k(D)$ , is submodular in $D$ .
(Müller and Scarsini, quoted on p. 7) If $\sigma^1_{ii}=\sigma^2_{ii}$ and $\sigma^1_{ij}\le\sigma^2_{ij}$ for all $i,j$ , then

N(m,\Sigma^1)\le_{sm}N(m,\Sigma^2).

(Proposition 5, p. 10) For every firm $k$ and every fixed $Q\ge0$ , $\pi_k^{\Sigma^2}(Q)\le\pi_k^{\Sigma^1}(Q)$ .

Significance

The result. Proposition 2 says that, under normal demand, positive dependence between substitutable products is costly to the retailer whatever the substitution pattern, the number of products, and the cost parameters, and that re-optimizing the stocking levels cannot undo this. It turns an empirical regularity of numerical studies into a structural statement, and it gives a reason to prefer assortments of products whose demands are less correlated. Proposition 5 gives the same conclusion for each competing firm when stocking quantities are fixed; the paper does not claim it when firms re-optimize, since equilibrium quantities move in ways that need not favour every firm.

Formalizing it. The result is proved in the paper, partly by citation: the comparison of normal laws in the supermodular order is a theorem of Müller and Scarsini that is quoted, not proved, there. No machine-checked version of that comparison is known on the platform: the existing Slepian and Sudakov–Fernique comparisons concern expected suprema and tail probabilities, not expectations of arbitrary supermodular functions. A formal proof of milestone 4 would therefore be reusable well beyond inventory theory, wherever supermodular functionals of Gaussian vectors are compared (portfolio risk, dependence orderings, stop-loss premiums).

Difficulty

The deterministic steps (milestones 1–3) are elementary lattice arguments. The difficulty is milestone 4. The natural route is Gaussian interpolation: connect the two laws through $N(m,(1-t)\Sigma^1+t\Sigma^2)$ and differentiate $\mathbb Ef$ in $t$ . That argument needs $f$ twice differentiable with controlled growth, while the statement must hold for every supermodular $f$ that is merely integrable under the two endpoint laws, such as the piecewise-linear profits of this model, and for singular covariance matrices. Passing from smooth to general supermodular functions, without assuming integrability along the interpolation path, is where the work lies. The paper's own route to the "adjusted optimally" clause, a total derivative $d\pi/d\rho_{ij}$ along a differentiable optimal path, presumes a smoothness of the optimizer that is not available, since the expected profit need not be concave in $Q$ ; the goal is stated as a comparison of optimal values, which avoids it.

Formalization scope

All declarations live in DemandSubstitution.Correlation. Products are indexed by Fin n, 0-based. The model data and the standing assumptions $r_i>c_i>s_i>0$ , $a_{ij}\in[0,1]$ , $a_{ii}=0$ , $\sum_ja_{ij}<1$ form a structure Model n; $u_i$ and $o_i$ are definitions. The paper's §2 assumption that demand is continuous with positive support is dropped, as the paper drops it: a normal law charges negative demands. $N(m,\Sigma)$ is Mathlib's multivariateGaussian on EuclideanSpace ℝ (Fin n), pushed forward to Fin n → ℝ; every statement assumes both covariance matrices positive semidefinite, because Mathlib's construction returns a Dirac mass otherwise. Correlations are encoded through covariances with fixed variances, which is equivalent to raising $\rho_{ij}$ . "Decreasing" is weak. Expectations are Bochner integrals; the profit integrands are Lipschitz and integrable under every normal law, and this integrability is to be proved, not assumed. Supermodularity and the supermodular order reuse the platform definitions SupermodularOn and SupermodularOrder.

A trivializing formalization is ruled out: the Müller–Scarsini comparison is a milestone theorem, never a hypothesis of the goal or of Proposition 5, and the "adjusted optimally" clause quantifies over every pair of maximizers, not over one chosen optimizer.

Contributions welcome: integrability of Lipschitz functions under multivariateGaussian; Gaussian interpolation for supermodular functions; the supermodular comparison itself, which would be reusable on its own.

Selected references

S. Netessine and N. Rudi, Centralized and Competitive Inventory Models with Demand Substitution, Simon School Working Paper OP 02-01, 2002, SSRN 303779. https://doi.org/10.2139/ssrn.303779 (published in Operations Research 51(2):329–335, 2003, https://doi.org/10.1287/opre.51.2.329.12788)
A. Müller and M. Scarsini, Some remarks on the supermodular order, Journal of Multivariate Analysis 73(1):107–119, 2000. https://doi.org/10.1006/jmva.1999.1867
D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
K. Rajaram and C. S. Tang, The impact of product substitution on retail merchandising, working paper, University of California, Los Angeles, 1999 (reference [16] of the source; no stable link).
D. M. Topkis, Minimizing a submodular function on a lattice, Operations Research 26(2):305–321, 1978. https://doi.org/10.1287/opre.26.2.305
R. Ernst and P. Kouvelis, The effects of selling packaged goods on inventory decisions, Management Science 45(8):1142–1155, 1999. https://doi.org/10.1287/mnsc.45.8.1142

9 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

On Implementing a Primal-Dual Interior-Point Method for Conic Quadratic Optimization II: Points of a Product of Quadratic and Rotated Cones Are Complementary Iff Their Arrow-Head Products VanishResearch Paper

Motivation

Conic quadratic optimization (also called second-order cone programming) minimizes a linear function over the intersection of an affine subspace with a product of quadratic cones. It contains linear programming, convex quadratically constrained programming, robust linear programming with ellipsoidal uncertainty and many problems from engineering design; see Lobo, Vandenberghe, Boyd and Lebret (1998). Primal–dual interior-point methods solve these problems in practice; E. D. Andersen, C. Roos and T. Terlaky describe one such method, and an implementation of it linked to the MOSEK optimizer, in On implementing a primal-dual interior-point method for conic quadratic optimization (Math. Program., 2003).

A primal–dual method needs the optimality condition "the duality gap is zero" in a form that can be relaxed into a central path and linearized by Newton's method. For linear programming that form is the componentwise product $x_js_j=0$ . For quadratic cones the scalar condition $x^Ts=0$ is not componentwise, and the paper's Lemma 3.1 gives the replacement: a block-wise system built from arrow-head matrices. This mission formalizes that lemma and the facts its proof uses.

Setting

A vector $v\in\mathbb R^n$ is written $v=(v_1,\dots,v_n)$ and $v_{2:n}=(v_2,\dots,v_n)$ ; $\|\cdot\|$ is the Euclidean norm. The paper works with three cones (Definition 3.1):

\mathbb R_+=\{x\ge 0\},\qquad K^q=\{x\in\mathbb R^n: x_1^2\ge\|x_{2:n}\|^2,\ x_1\ge0\},\qquad K^r=\{x\in\mathbb R^n: 2x_1x_2\ge\|x_{3:n}\|^2,\ x_1,x_2\ge0\},

the nonnegative half-line, the quadratic cone and the rotated quadratic cone. The cone of the problem is a product $K=K^1\times\cdots\times K^k$ of such cones, of dimensions $n^1,\dots,n^k$ , and a point is partitioned accordingly, $x=(x^1;\dots;x^k)$ ; $x^Ts=\sum_i(x^i)^Ts^i$ .

To each cone the paper attaches two matrices (Definition 3.2): $T^i=Q^i=1$ for $\mathbb R_+$ ; $T^i=I$ and $Q^i=\operatorname{diag}(1,-1,\dots,-1)$ for $K^q$ ; and for $K^r$ , $T^i$ is the identity except for the leading block $\tfrac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ , while $Q^i$ is $-I$ except for the leading block $\begin{pmatrix}0&1\\1&0\end{pmatrix}$ . The arrow-head matrix of a vector is

\operatorname{mat}(v)=\begin{pmatrix}v_1&v_{2:n}^T\\ v_{2:n}&v_1I\end{pmatrix},

and $X^i=\operatorname{mat}(T^ix^i)$ , $S^i=\operatorname{mat}(T^is^i)$ ; $e^i$ is the first unit vector of $\mathbb R^{n^i}$ .

For the companion statements the paper defines $\mu=(x^Ts+\tau\kappa)/(k+1)$ and the neighbourhood

\mathcal N(\beta)=\Bigl\{(x,\tau,s,\kappa):(x;\tau),(s;\kappa)\in K\times\mathbb R_+,\ \min_i\sqrt{(x^i)^TQ^ix^i\,(s^i)^TQ^is^i}\ge\beta\mu,\ \tau\kappa\ge\beta\mu\Bigr\}.

Formalization targets

Goal: Lemma 3.1 (p. 9)

For $x,s\in K$ ,

x^Ts=0\iff X^iS^ie^i=S^iX^ie^i=0\quad(i=1,\dots,k).

This is the paper's exact statement; it fixes no constants and covers every mixture of the three cone types.

Milestones

$Q^iQ^i=I$ and $T^iT^i=I$ , with $Q^i$ , $T^i$ symmetric (p. 9).
$K^q=\{x:x^TQx\ge0,\ x_1\ge0\}$ and $K^r=\{x:x^TQx\ge0,\ x_1,x_2\ge0\}$ (p. 9).
For the rotated cone's $T$ : $x\in K^q\iff Tx\in K^r$ (p. 9).
$x\in K$ implies $T^ix^i\in K^q$ for every block (Appendix, p. 36).
Identity (61): $(e^i)^TX^iS^ie^i=(T^ix^i)^TT^is^i=(x^i)^Ts^i$ , hence $e^TXSe=x^Ts$ .
The explicit form of (20) for one block: $(x^i)^Ts^i=0$ and $(T^ix^i)_1(T^is^i)_{2:n}+(T^is^i)_1(T^ix^i)_{2:n}=0$ (p. 36).
For $x,s\in K$ : $x^Ts=\sum_i(T^ix^i)^TT^is^i\ge\sum_i\bigl((T^ix^i)_1(T^is^i)_1-\|(T^ix^i)_{2:n}\|\|(T^is^i)_{2:n}\|\bigr)\ge\sum_i\sqrt{(x^i)^TQ^ix^i(s^i)^TQ^is^i}\ge0$ (pp. 36–37).
If $x^Ts=0$ and $(T^ix^i)_1,(T^is^i)_1\ne0$ , then $(x^i)^TQ^ix^i=(s^i)^TQ^is^i=0$ and $(T^ix^i)_1(T^is^i)_1=\|(T^ix^i)_{2:n}\|\|(T^is^i)_{2:n}\|$ (p. 37).
If $(x^i)^Ts^i=0$ and $(T^ix^i)_1,(T^is^i)_1\ne0$ , then $(T^ix^i)_{2:n}=\alpha(T^is^i)_{2:n}$ with $\alpha=-(T^ix^i)_1/(T^is^i)_1$ , and (20) holds for block $i$ (p. 37).
Lemma 3.2 ii) (p. 11): a point of $\mathcal N(1)$ has $X^iS^ie^i=\mu e^i$ and $\tau\kappa=\mu$ .
§6.1 (pp. 28–29): the starting point $x^{i(0)}=s^{i(0)}=T^ie^i_1$ , $\tau^{(0)}=\kappa^{(0)}=1$ lies in $\mathcal N(1)$ .

Significance

Lemma 3.1 is what makes a primal–dual method for conic quadratic problems possible in the familiar form: replacing $X^iS^ie^i=0$ by $X^iS^ie^i=\gamma\mu e^i$ gives the central path (21), and linearizing it gives the Newton system the paper analyses in §4. Lemma 3.2 ii) identifies $\mathcal N(1)$ with that central path, and the §6.1 statement shows the algorithm starts on it. The arrow-head product $X^iS^ie^i$ is the Jordan product of the Lorentz cone's Euclidean Jordan algebra, so the lemma is also the concrete, coordinate form of complementarity in that algebra (Alizadeh and Goldfarb, 2003).

The lemma is proved in the paper's Appendix and is classical; the mission's contribution is a machine-checked version. To our knowledge no proof assistant library contains complementarity for quadratic or rotated quadratic cones, the rotated-cone transformation, or the arrow-head matrix. The statements here are not yet proved anywhere in Lean.

Difficulty

The forward direction is an identity, (61). The converse is where the work is: $x^Ts=0$ is one scalar equation, yet it must force $n^i$ equations per block. The argument needs a reverse Cauchy–Schwarz bound inside each quadratic cone, an equality-case analysis that splits on whether a leading coordinate vanishes, and the reduction of the rotated cone to the quadratic one through $T$ . A block-by-block argument fails without first showing that each $(x^i)^Ts^i$ is nonnegative, since only the sum is known to vanish. In Lean, the arithmetic of $1/\sqrt2$ in $T$ and the index bookkeeping of $v_{2:n}$ inside Fin n add their own friction.

Formalization scope

Vectors are Fin d → ℝ; the paper's $x_1$ is index 0 and $x_2$ is index 1, read through coord v r. The Euclidean tails are written out as sums, tailSq v 1 $=\|v_{2:n}\|^2$ and tailSq v 2 $=\|v_{3:n}\|^2$ ; Mathlib's norm on Fin d → ℝ is the sup norm and is never used. Points of $K$ are stored block by block, x : (i : Fin k) → Fin (n i) → ℝ, with a cone kind kind i ∈ {nonneg, quad, rot} per block; $x^Ts$ is $\sum_i x^i\cdot s^i$ , and the block-diagonal $X$ , $S$ are represented by their blocks. Tmat, Qmat, arrow and e1 are defined entrywise from (16)–(19) and p. 9.

Standing assumptions and additions:

The paper never states block dimensions; every theorem assumes WellFormed: $n^i=1$ for $\mathbb R_+$ , $n^i\ge1$ for $K^q$ , $n^i\ge2$ for $K^r$ (the rotated cone needs $x_1$ and $x_2$ ).
" $x,s\in K$ " is taken literally; $K$ is self-dual, so no separate dual cone is introduced.
The milestones 8 and 9 carry the page's case hypotheses $(T^ix^i)_1\ne0$ , $(T^is^i)_1\ne0$ .
The printed upper limit $n$ in (61) is read as $k$ ; "(x; τ), (s; κ) ∈ N(1)" in Lemma 3.2 ii) is read as $(x,\tau,s,\kappa)\in\mathcal N(1)$ .

The goal is stated with arrow and Tmat, not with the unfolded vector $((T^ix^i)^TT^is^i;\ (T^ix^i)_1(T^is^i)_{2:n}+(T^is^i)_1(T^ix^i)_{2:n})$ : replacing the arrow-head matrices by that vector, or dropping the rotated cone, would remove the content the lemma is about. Contributions welcome: proofs of any milestone, and reusable lemmas on tailSq (Cauchy–Schwarz for tails, its equality case) and on the arrow-head matrix.

Selected references

E. D. Andersen, C. Roos, T. Terlaky, On implementing a primal-dual interior-point method for conic quadratic optimization, Mathematical Programming 95 (2003). https://doi.org/10.1007/s10107-002-0349-3
F. Alizadeh, D. Goldfarb, Second-order cone programming, Mathematical Programming 95 (2003), 3–51. https://doi.org/10.1007/s10107-002-0339-5
M. S. Lobo, L. Vandenberghe, S. Boyd, H. Lebret, Applications of second-order cone programming, Linear Algebra and its Applications 284 (1998), 193–228. https://doi.org/10.1016/S0024-3795(98)10032-0
Yu. E. Nesterov, M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM Journal on Optimization 8 (1998), 324–364. https://doi.org/10.1137/S1052623495290209

13 thms2 active usersReviewed

Convex Optimization Optimization·Captain: mikedeng1

On Implementing a Primal-Dual Interior-Point Method for Conic Quadratic Optimization I: Solutions of the Homogeneous Model Are Complementary and Give an Optimal Pair or an Infeasibility CertificateResearch Paper

Motivation

Conic optimization minimizes a linear function over the intersection of an affine subspace with a closed convex cone. Linear programming (the nonnegative orthant), second-order cone programming (products of quadratic cones) and semidefinite programming (the positive semidefinite cone) are all instances. Primal–dual interior-point methods are the standard algorithms for these problems, and production solvers for conic quadratic optimization, such as the MOSEK solver described by Andersen, Roos and Terlaky (Math. Program. 95 (2003)), are built on them.

The classical primal–dual method assumes that both the primal and the dual problem have strictly feasible points. A practical solver cannot assume this: it must also recognize infeasible problems and return a certificate. The device that handles this is the homogeneous model, introduced by Goldman and Tucker for linear programming (1956) and used in interior-point form by Ye, Todd and Mizuno (Math. Oper. Res. 19 (1994)). The model embeds the primal–dual pair into a larger homogeneous system that always has solutions; a solution with a positive homogenizing variable yields an optimal pair, and one with a positive slack variable yields an infeasibility certificate. Section 2 of Andersen, Roos and Terlaky states this generalization to an arbitrary pointed closed convex cone, and this mission formalizes it.

Setting

Let $A \in \mathbb R^{m\times n}$ , $b \in \mathbb R^m$ , $c \in \mathbb R^n$ , and let $K \subseteq \mathbb R^n$ be a pointed closed convex cone: closed, convex, closed under multiplication by nonnegative scalars, and pointed, $K \cap (-K) = \{0\}$ (it contains $0$ , and $x \in K$ and $-x \in K$ imply $x = 0$ ). Its dual cone is

K_* := \{\, s \in \mathbb R^n : s^Tx \ge 0 \text{ for all } x \in K \,\}.

The primal problem is $(P)$ : minimize $c^Tx$ subject to $Ax = b$ , $x \in K$ . The dual problem is $(D)$ : maximize $b^Ty$ subject to $A^Ty + s = c$ , $s \in K_*$ . A point satisfying the constraints is feasible; a feasible point is optimal if no feasible point has a better objective value; a problem without feasible points is infeasible. $(P)$ is strictly feasible if some $x$ with $Ax = b$ lies in the interior of $K$ , and $(D)$ if some $(y,s)$ with $A^Ty + s = c$ has $s$ in the interior of $K_*$ .

The homogeneous model (7) of the paper asks for $(x, \tau, y, s, \kappa)$ with

Ax - b\tau = 0,\qquad A^Ty + s - c\tau = 0,\qquad -c^Tx + b^Ty - \kappa = 0,

x \in K,\ \tau \ge 0,\qquad s \in K_*,\ \kappa \ge 0.

The quantity $x^Ts + \tau\kappa$ is its complementarity gap. In the Lean development these objects are dualCone, PrimalFeasible, DualFeasible, PrimalOptimal, DualOptimal, PrimalInfeasible, DualInfeasible and HomFeasible, all in the namespace ConicQuadIPM.Homogeneous.

Formalization targets

Goal: Lemma 2.1 (p. 6)

For every solution $(x^*, \tau^*, y^*, s^*, \kappa^*)$ of (7):

\text{(i)}\quad (x^*)^Ts^* + \tau^*\kappa^* = 0;

\text{(ii)}\quad \tau^* > 0 \implies x^*/\tau^* \text{ is optimal for } (P) \text{ and } (y^*, s^*)/\tau^* \text{ is optimal for } (D);

\text{(iii)}\quad \kappa^* > 0 \implies b^Ty^* > 0 \ \text{or}\ c^Tx^* < 0;\ \ b^Ty^* > 0 \Rightarrow (P) \text{ infeasible};\ \ c^Tx^* < 0 \Rightarrow (D) \text{ infeasible}.

Milestones

Theorem 2.1, weak duality (p. 4): for feasible $x$ and $(y,s)$ , $c^Tx - b^Ty = x^Ts \ge 0$ .
Lemma 2.1 i) on its own.
Theorem 2.1, primal infeasibility (5): $s \in K_*$ , $A^Ty + s = 0$ , $b^Ty > 0$ imply that $(P)$ is infeasible.
Theorem 2.1, dual infeasibility (6): $x \in K$ , $Ax = 0$ , $c^Tx < 0$ imply that $(D)$ is infeasible.
From the proof of Lemma 2.1: $\kappa^* > 0$ forces $b^Ty^* > 0$ or $c^Tx^* < 0$ .
(10): if $\kappa^* > 0$ and $b^Ty^* > 0$ , then $b^Ty^* > 0$ , $A^Ty^* + s^* = 0$ , $s^* \in K_*$ .
(11): if $\kappa^* > 0$ and $c^Tx^* < 0$ , then $c^Tx^* < 0$ , $Ax^* = 0$ , $x^* \in K$ .
Theorem 2.1, strong duality (p. 4): if one side is strictly feasible with a bounded objective, then $(x, y, s)$ is optimal if and only if it is feasible with $c^Tx - b^Ty = x^Ts = 0$ .

Significance

Lemma 2.1 is the correctness statement behind every homogeneous-model interior-point solver for conic problems: whatever solution with $\tau^* + \kappa^* > 0$ the algorithm approaches, it is either a scaled optimal primal–dual pair or a certificate of primal or dual infeasibility. Parts (iii) and the certificates (5)–(6) are the conic Farkas-type alternatives on which infeasibility reporting rests. The paper also notes the limit of the statement: for conic problems a solution with $\tau^* + \kappa^* > 0$ need not exist (a feasible conic quadratic pair with a nonzero duality gap is an example), unlike in linear programming.

The results are classical and proved on paper; the strong-duality part is cited from the literature rather than proved in the source. Linear-programming versions of the homogeneous-model properties exist as formal statements on the platform (from Ye–Todd–Mizuno, Vanderbei and Matoušek), but those concern the nonnegative orthant only. This mission states the general conic version over an arbitrary pointed closed convex cone, and the weak-duality and certificate statements it introduces are reusable by any later conic formalization.

Difficulty

Parts (i) and (ii) and the certificates are short arguments from the definitions; the formal work is in handling the cone axioms and the bilinear algebra cleanly. The step that is easy to overlook is in (iii): the identities $A^Ty^* + s^* = 0$ in (10) and $Ax^* = 0$ in (11) do not follow from the equations of (7) alone, because the terms $c\tau^*$ and $b\tau^*$ are present; the paper passes over this point. The strong-duality milestone is of a different order: it is a genuine conic duality theorem, cited rather than proved in the source, and it fails without the Slater-type hypothesis (feasible conic quadratic pairs with a nonzero duality gap exist).

Formalization scope

Vectors are Fin n → ℝ, $u^Tv$ is u ⬝ᵥ v, $Ax$ is A *ᵥ x and $A^Ty$ is Aᵀ *ᵥ y; the paper's first coordinate is index 0. The standing assumption that $K$ is a pointed closed convex cone is the hypothesis IsPointedClosedConvexCone K on every theorem, even where a proof uses less. The paper's further assumption that $A$ has full row rank is stated "for convenience and without loss of generality" and is not used in any of these results; it is dropped, which makes every statement a generalization. A nonempty interior of $K$ is not assumed, and no milestone except strong duality mentions interiors; there, interiors are topological interiors in $\mathbb R^n$ . Optimality is a predicate (feasible, and at least as good as every feasible point), never a value defined through an infimum or supremum, and infeasibility is the non-existence of a feasible point. Division by $\tau^*$ is scalar multiplication by $(\tau^*)^{-1}$ under $\tau^* > 0$ .

A trivializing reading is excluded: part (ii) must conclude optimality of both the primal and the dual point against all feasible points, and part (iii) must conclude that the relevant problem has no feasible point, not merely the sign condition; the milestones (10) and (11) assume only $\kappa^* > 0$ and the respective inequality, never $\tau^* = 0$ .

All definitions live in one module, Definitions.Def_ConicQuadIPM_Homogeneous_Setting. Contributions welcome: proofs of the milestones, a proof of conic strong duality in this standard form (the platform's Lagrangian conic Slater theorem may help), and reuse of weak duality and the certificates in later conic missions.

Selected references

E. D. Andersen, C. Roos, T. Terlaky, On implementing a primal-dual interior-point method for conic quadratic optimization, Mathematical Programming 95 (2003) 249–277. https://doi.org/10.1007/s10107-002-0349-3
A. J. Goldman, A. W. Tucker, Theory of linear programming, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956. https://doi.org/10.1515/9781400881987-005
Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt n L)$ -iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19 (1994) 53–67. https://doi.org/10.1287/moor.19.1.53
Yu. Nesterov, M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM Journal on Optimization 8 (1998) 324–364. https://doi.org/10.1137/S1052623495290209

10 thms2 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion 3: With Random Right-Hand Side and Known Dual Extreme Points, the Problem Equals the Semidefinite Program (14)Research Paper

Motivation

Two-stage stochastic linear programs model a decision $x$ taken before uncertainty is revealed, followed by a corrective recourse action once it is. The classical model needs the full probability distribution of the uncertain data, which in practice is rarely known; often only estimates of the mean and the second moments are available, and the computed plan can be sensitive to the distribution assumed. The minimax (distributionally robust) approach replaces the single distribution by the class of all distributions with given first and second moments and optimizes against the worst member of that class. Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) combine this with risk aversion, through a piecewise-linear disutility of the second-stage cost, and determine which instances can be solved as semidefinite programs.

When the randomness sits in the right-hand side of the second stage, the paper shows that the problem is NP-hard in general (Theorem 3.1). This mission concerns the tractable special case that follows (§3.2): if the extreme points of the dual feasible region of the recourse problem are known, the whole minimax problem is one semidefinite program.

Setting

A first-stage decision $x\in\mathbb R^n$ is feasible if $x\in X=\{x : Ax=b,\ x\ge 0\}$ and costs $c'x$ . Given a recourse matrix $W\in\mathbb R^{r\times d}$ , a technology matrix $T\in\mathbb R^{r\times n}$ , a constant cost vector $q\in\mathbb R^d$ and a realized right-hand side $h\in\mathbb R^r$ , the second-stage cost is written as the optimal value of the dual of the recourse linear program,

\mathcal Q(h,x)=\max_{p}\ (h-Tx)'p\quad\text{s.t.}\quad W'p\le q .

Risk aversion enters through the disutility $\mathbb U(t)=\max_{k=1,\dots,K}(\alpha_k t+\beta_k)$ with $\alpha_k\ge 0$ . The right-hand side $\tilde h$ is random, and its distribution is only known to lie in the moment class

\mathcal P=\{P : \mathbb E_P[\tilde h]=\mu,\ \mathbb E_P[\tilde h\tilde h']=Q\}.

The worst-case expected disutility is $\hat Z(x)=\sup_{P\in\mathcal P}\mathbb E_P[\mathbb U(\mathcal Q(\tilde h,x))]$ , and the problem is

Z=\min_{x\in X}\big(c'x+\hat Z(x)\big).

The moment problem defining $\hat Z(x)$ has the dual (12): minimize $Q\cdot Y+\mu'y+y_0$ over symmetric $Y$ , $y\in\mathbb R^r$ , $y_0\in\mathbb R$ with $h'Yh+y'h+y_0\ge\mathbb U(\mathcal Q(h,x))$ for every $h$ , where $Q\cdot Y=\sum_{i,j}Q_{ij}Y_{ij}$ .

The standing assumptions are: $X$ nonempty and bounded (Assumption 1); complete recourse, $\{Ww : w\ge 0\}=\mathbb R^r$ (Assumption 2); a nonempty dual polyhedron $\{p : W'p\le q\}$ (Assumption 3); $Q\succ\mu\mu'$ (Assumption 4); and the extreme points $p_1,\dots,p_N$ of $\{p : W'p\le q\}$ are known (Assumption 5).

Formalization targets

Goal: Theorem 3.2 (p. 589)

The problem is equivalent to the semidefinite program

\hat Z_{\rm SDP}=\min_{x,Y,y,y_0}\ c'x+Q\cdot Y+\mu'y+y_0\ \ \text{s.t.}\ \begin{pmatrix}Y & \tfrac12(y-\alpha_k p_i)\\ \tfrac12(y-\alpha_k p_i)' & y_0+\alpha_k p_i'Tx-\beta_k\end{pmatrix}\succeq 0\ \ \forall k,i,\quad Ax=b,\ x\ge 0, \tag{14}

in the sense that $\hat Z(x)$ equals the value of the per- $x$ program (15) for every $x\in X$ , and $Z=\hat Z_{\rm SDP}$ , both being genuine finite infima.

Milestones (§3.1 and the proof of Theorem 3.2, pp. 588–590)

Strong duality for (11)/(12): $\hat Z(x)=\hat Z_D(x)$ .
The constraints of (12) are equivalent to $h'Yh+(y-\alpha_kp)'h+y_0+\alpha_kp'Tx-\beta_k\ge 0$ for all $h$ , all $p$ with $W'p\le q$ and all $k$ .
Every feasible $Y$ of (12) is positive semidefinite.
$\mathcal Q(h,x)=\max_{i=1,\dots,N}(h-Tx)'p_i$ .
A quadratic $h'Yh+2v'h+c$ is nonnegative on $\mathbb R^r$ iff the bordered matrix $\begin{pmatrix}Y&v\\v'&c\end{pmatrix}$ is positive semidefinite (already proved on the platform).
The feasible sets of (12) and (15) coincide, so $\hat Z_D(x)$ is the value of (15).

Significance

The result. Theorem 3.2 turns a two-level problem — a minimum over $x$ of a supremum over an infinite-dimensional set of distributions — into one convex program of polynomial size in $n$ , $r$ , $K$ and $N$ , jointly in the first-stage decision and the dual multipliers. The first-stage decision enters the linear matrix inequalities only through the corner entry $y_0+\alpha_kp_i'Tx-\beta_k$ , which is affine in $x$ ; this is what keeps the joint program convex. Together with the NP-hardness of the general case (Theorem 3.1), it locates the source of intractability in the enumeration of dual vertices. The same program (15) is the starting point of the construction of an extremal distribution (Theorem 3.3), which the paper uses to stress-test first-stage solutions.

Formalizing it. The result is proved in the paper, with strong duality for the moment problem cited from the literature. Nothing in this chain is formalized: neither the moment-problem duality under the interior condition $Q\succ\mu\mu'$ , nor the vertex representation of a bounded linear program over a pointed polyhedron given by its extreme points. The lemma that a nonnegative quadratic corresponds to a positive semidefinite bordered matrix is already proved on the platform and is reused.

Difficulty

The reduction from (12) to (15) is elementary once $\mathcal Q(h,x)=\max_i(h-Tx)'p_i$ is available, but that identity is a genuine statement about polyhedra: the dual region $\{p : W'p\le q\}$ is unbounded, so compactness arguments such as Krein–Milman do not apply, and one needs both that the polyhedron is pointed (here a consequence of complete recourse, which forces $W$ to have full row rank) and that a bounded linear objective attains its maximum at a vertex. The other substantial step is strong duality between the moment problem over measures and the semi-infinite dual (12), which requires the moment vector $(\mu,Q)$ to lie in the interior of the moment cone; without $Q\succ\mu\mu'$ a duality gap or an empty class $\mathcal P$ can occur. Finally, the equality $Z=\hat Z_{\rm SDP}$ requires exchanging an infimum over $x$ with the infimum over the dual variables, which needs each per- $x$ program to be feasible and bounded.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin r) (Fin d) ℝ, and pieces and extreme points are indexed by Fin K and Fin N (zero-based). The paper's letter $p$ is both the dimension of $q$ and the dual variable; in Lean the dimension is $d$ and the dual vector is π. The class $\mathcal P$ consists of probability measures on $\mathbb R^r$ with square-integrable coordinates, mean $\mu$ and uncentred second-moment matrix $Q$ , built on the published MomentDRO.Conf.Setting; the paper's densities are replaced by measures. $\mathcal Q(h,x)$ is the real supremum over the dual polyhedron. Every printed min/max is a real infimum/supremum of a set of objective values, and the statements assert with IsLUB/IsGLB that these are genuine finite bounds; attainment of the minima is not claimed. $Y$ is required symmetric throughout. The bordered matrix is the published WorstCaseVaR.KnownMoments.bordered and $\succeq 0$ is Matrix.PosSemidef.

Readings of the source:

As printed, Assumption 2 (complete recourse) and Assumption 3 ("for all $q$ ") contradict each other when $r\ge 1$ . The section-wise reading is used: complete recourse together with dual feasibility at the single constant $q$ of §3.
"Assumption i" in Theorem 3.2 and in its proof is read as Assumption 5.
"The strong duality condition" is read as Assumption 4.
Assumption 5 is the hypothesis that the list $p_1,\dots,p_N$ is exactly the set of extreme points of the dual region; "explicitly known" has no further mathematical content.
(11) integrates over $\mathbb R^p$ where $\mathbb R^r$ is meant.

A formalization in which $\hat Z_{\rm SDP}$ is defined through $\hat Z_D(x)$ , or in which positive semidefiniteness is replaced by a hand-written quadratic condition, would make the goal a restatement of strong duality; (14) is stated as a single program in $(x,Y,y,y_0)$ with Matrix.PosSemidef constraints. The hypotheses of the goal are satisfiable ( $r=1$ , $W=[1,-1]$ , $q=(1,1)$ , $\mu=0$ , $Q=1$ , $X=\{1\}$ ).

Contributions welcome: the vertex representation of bounded linear programs over pointed polyhedra, and duality for moment problems with first and second moments, are both reusable well beyond this mission.

Selected references

D. Bertsimas, X. V. Doan, K. Natarajan, C.-P. Teo, Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion, Mathematics of Operations Research 35(3):580–602, 2010. https://doi.org/10.1287/moor.1100.0445
K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14:185–197, 1962. https://doi.org/10.1007/BF02868641
A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, Kluwer, 2001, pp. 135–165. https://doi.org/10.1007/978-1-4757-3403-4_7
L. El Ghaoui, M. Oks, F. Oustry, Worst-case value-at-risk and robust portfolio optimization: a conic programming approach, Operations Research 51(4):543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101

10 thms2 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Distributionally Robust Optimization and Its Tractable Approximations 1: Under a Support Set and a Mean Set, the Bound π¹ Equals the Worst-Case Expected Positive PartResearch Paper

Motivation

Linear decision rules are a standard device for making multistage optimization under uncertainty computationally tractable: a recourse decision is restricted to be an affine function of the uncertain data observed so far. Their weakness is that a recourse variable that must stay nonnegative forces the rule to be very conservative. Goh and Sim, Distributionally Robust Optimization and Its Tractable Approximations (Operations Research, 2010), repair this with deflected linear decision rules, in which the violated part of an affine rule is corrected and paid for. The cost of the correction is the expected positive part $\mathbb E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$ of an affine function of the uncertainty.

The distribution $\mathbb P$ is not known. The paper assumes only partial distributional information (a support set, a set containing the mean, a covariance, directional deviations) and bounds the worst case of this expectation over every distribution consistent with that information. Such worst-case bounds go back to Scarf's 1958 mean–variance newsvendor bound and form the core of distributionally robust optimization. This mission formalizes the first bound of §5, which uses support and mean information only.

Setting

Let $\tilde\zeta$ be a random vector in $\mathbb R^{n}$ (in the paper, the segregated uncertainty vector of dimension $n = N_E$ ). Two sets describe what is known about it:

a support set $\mathcal V \subseteq \mathbb R^n$ with $\mathbb P(\tilde\zeta \in \mathcal V) = 1$ ;
a mean set $\widehat{\mathcal V} \subseteq \mathbb R^n$ containing the mean $\hat\zeta = \mathbb E_{\mathbb P}(\tilde\zeta)$ . A known mean is the case where $\widehat{\mathcal V}$ is a single point.

The family of distributions consistent with this information is

\mathbb F_1 = \{\mathbb P : \hat\zeta = \mathbb E_{\mathbb P}(\tilde\zeta) \in \widehat{\mathcal V},\ \mathbb P(\tilde\zeta \in \mathcal V) = 1\}.

For data $r^0 \in \mathbb R$ and $r \in \mathbb R^n$ the worst-case value is $\sup_{\mathbb P \in \mathbb F_1} \mathbb E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$ , with $x^+ = \max\{x, 0\}$ . The paper's candidate for this value is the deterministic quantity of (21),

\pi^1(r^0, r) = \inf_{s \in \mathbb R^{n}} \Phi(s), \qquad \Phi(s) = \sup_{\hat\zeta \in \widehat{\mathcal V}} \{s'\hat\zeta\} + \sup_{\zeta \in \mathcal V} \max\{r^0 + r'\zeta - s'\zeta,\ -s'\zeta\}.

Both quantities live in the extended reals: following the paper (p. 909), an infeasible maximization has value $-\infty$ and an infeasible minimization $+\infty$ .

Formalization targets

Goal: Theorem 1 (p. 909)

For closed convex $\mathcal V, \widehat{\mathcal V}$ with $\widehat{\mathcal V} \cap \operatorname{int} \mathcal V \neq \emptyset$ , and all $r^0, r$ ,

\sup_{\mathbb P \in \mathbb F_1} \mathbb E_{\mathbb P}\big((r^0 + r'\tilde\zeta)^+\big) = \pi^1(r^0, r).

Milestones

Upper-bound part of Theorem 1. $\sup_{\mathbb P \in \mathbb F_1} \mathbb E_{\mathbb P}((r^0 + r'\tilde\zeta)^+) \le \pi^1(r^0, r)$ , for arbitrary sets $\mathcal V, \widehat{\mathcal V}$ .
Remark after Theorem 1, first case (p. 910). If $\widehat{\mathcal V} \subseteq \mathcal V$ is nonempty and $r^0 + r'\zeta \ge 0$ on $\mathcal V$ , then the worst-case value equals $r^0 + \sup_{\hat\zeta \in \widehat{\mathcal V}} r'\hat\zeta$ , and $\Phi(r) = \pi^1(r^0, r)$ .
Remark after Theorem 1, second case (p. 910). If $\widehat{\mathcal V} \subseteq \mathcal V$ is nonempty and $r^0 + r'\zeta \le 0$ on $\mathcal V$ , then the worst-case value is $0$ , and $\Phi(0) = \pi^1(r^0, r) = 0$ .
Tightness part of Theorem 1. Under the goal's hypotheses, $\pi^1(r^0, r) \le \sup_{\mathbb P \in \mathbb F_1} \mathbb E_{\mathbb P}((r^0 + r'\tilde\zeta)^+)$ .

Significance

The result itself. Theorem 1 converts an optimization over an infinite-dimensional set of probability measures into a finite-dimensional convex program over the given sets. When $\mathcal V$ and $\widehat{\mathcal V}$ are representable by linear and second-order cone constraints, the epigraph of $\pi^1$ is a pair of robust constraints over those sets and is again tractable (Remark, p. 910). The bound is tight, so no better bound can be built from support and mean information alone. In the paper, $\pi^1$ is one of three building blocks; their infimal convolution (Theorem 4) prices the deflection in the deflected linear decision rules of §6, and the experiments there compare these rules against plain linear decision rules.

Formalizing it. The proof of Theorem 1 is in the paper's online appendix, not in the main text. A search of the Prove2Me library (October 2026) found no formal statement of this or any other mean-and-support bound. A formal proof has to settle the extended-real bookkeeping (empty families, unbounded suprema) and the exact hypotheses under which tightness holds. As printed, the theorem omits a condition: with no constraint qualification it fails when $\mathbb F_1$ is empty, which can happen for disjoint closed convex sets. This mission states the corrected version.

Difficulty

The upper-bound part is weak duality and needs no structure on the sets. The difficulty is tightness. It amounts to a strong-duality statement between the worst case over distributions and the infimum over the multiplier $s$ , and strong duality for convex problems over unbounded sets needs a constraint qualification. Two obvious approaches fail. The first is to search for a single worst-case distribution: for unbounded $\mathcal V$ the supremum over $\mathbb F_1$ is generally not attained, and it may be $+\infty$ . The second is to restrict to compact $\mathcal V$ , which excludes the paper's main use, a segregation of an unbounded support such as $(-\infty, -1] \cup [-1, 1] \cup [1, \infty)$ . Mathlib has separating-hyperplane theorems but no Fenchel duality theorem, so this duality has to be built.

Formalization scope

A distribution is a measure $P$ on Fin n → ℝ with IsProbabilityMeasure P, and the random vector is the identity map. Every coordinate is required to be $P$ -integrable, so the mean is a genuine expectation; the mean is MomentDRO.Conf.meanVec from the published definition MomentDRO_Conf_Setting.
$\mathbb P(\tilde\zeta \in \mathcal V) = 1$ is the almost-everywhere statement ∀ᵐ ζ ∂P, ζ ∈ V, which needs no measurability of $\mathcal V$ .
The positive part is max (r0 + r ⬝ᵥ ζ) 0.
The worst-case value, both suprema and the infimum in (21) are taken in EReal. An empty supremum is $-\infty$ , an empty infimum $+\infty$ , and an unbounded supremum $+\infty$ . The paper's "inf" is ⨅; attainment is claimed only where the Remark claims it, via the objective $\Phi$ (pi1Obj) at $s = r$ and $s = 0$ .
The paper's tractable conic representable sets are modelled as closed and convex sets. The goal and its tightness part also assume $\widehat{\mathcal V} \cap \operatorname{int}\mathcal V \ne \emptyset$ . This condition is not on the page; it is consistent with the paper's full-dimensionality assumptions (pp. 905–906), and it implies $\mathbb F_1 \neq \emptyset$ .
The Remark's two cases assume $\widehat{\mathcal V} \subseteq \mathcal V$ and $\widehat{\mathcal V} \ne \emptyset$ . The paper's construction of $\mathcal V, \widehat{\mathcal V}$ from one set $\mathcal H$ (§4.5) gives the inclusion, and without it the first case is false.
The segregation map, the matrices $F$ , $g$ and the set $\mathcal H$ of §4 are context only and are not formalized: the theorem is stated for an arbitrary random vector with the listed properties.
A real-valued supremum, a family without integrability (for which the mean would be a junk value), or a $\pi^1$ defined through the worst case would each trivialize the statement; the definitions avoid all three, and $\pi^1$ is defined directly from the sets.

Needed infrastructure: finite mixtures of Dirac masses as members of $\mathbb F_1$ , integration of almost-surely bounded functions, separation of convex sets in $\mathbb R^n$ , and a Fenchel-type duality for a concave function over a closed convex set under an interior-point condition. The duality and the concave-envelope facts are reusable well beyond this mission, including for Theorems 2–4 of the same paper. Proofs of any milestone, and reusable lemmas on extended-real suprema of integrals, are welcome.

Selected references

J. Goh and M. Sim, Distributionally Robust Optimization and Its Tractable Approximations, Operations Research 58(4, Part 1 of 2):902–917, 2010. https://doi.org/10.1287/opre.1090.0795
H. Scarf, A Min–Max Solution of an Inventory Problem, in K. Arrow, ed., Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958, 201–209.
W. Chen and M. Sim, Goal-Driven Optimization, Operations Research 57(2):342–357, 2009 (cited by the paper for the infimal convolution of bounds).
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorem 31.1, Fenchel duality). https://doi.org/10.1515/9781400873173

7 thms2 active usersReviewed

Combinatorics Graph Theory Optimization·Captain: mikedeng1

Convex Quadratic and Semidefinite Programming Relaxations in Scheduling IV: A ρ-Approximate Max-m-Cut Gives a (ρ + m(1 − ρ))-Approximate Schedule for Pm | | Σ wⱼCⱼResearch Paper

Motivation

Scheduling jobs on identical parallel machines to minimize the total weighted completion time $\sum_j w_jC_j$ , the problem $P\,|\,|\sum w_jC_j$ , is one of the basic NP-hard problems of machine scheduling. On a single machine it is solved by Smith's ratio rule (Smith 1956); with several machines the only hard decision is which jobs share a machine. Section 6 of M. Skutella's paper Convex quadratic and semidefinite programming relaxations in scheduling (J. ACM 48 (2001)) observes that this decision is a graph partitioning problem: the cost of a schedule is, up to a constant, the weight of the edges that a partition of a weighted complete graph does not cut. Minimizing $\sum_j w_jC_j$ on $m$ machines is therefore equivalent to Max- $m$ -Cut on that graph, and the paper shows that the equivalence preserves approximation in a quantified way.

The reduction explains, from the graph side, why semidefinite rounding works for two machines: with the 0.878-approximation for MaxCut of Goemans and Williamson (1995) it gives a 1.122-approximation for $P2\,|\,|\sum w_jC_j$ (Corollary 6.2 of the paper). For general $m$ , the uniform random partition is both a $(1-1/m)$ -approximation for Max- $m$ -Cut and randomized rounding of the optimum of the convex quadratic relaxation (CQP).

Setting

There are $n$ jobs $J=\{1,\dots,n\}$ and $m\ge 1$ identical machines. Job $j$ has a processing time $p_j>0$ and a weight $w_j\ge 0$ . Smith's order $\prec$ puts $j\prec k$ when $w_j/p_j>w_k/p_k$ , ties broken by index. An assignment $\sigma:J\to\{1,\dots,m\}$ is a partition $J_1,\dots,J_m$ of the jobs; each machine processes its jobs in the order $\prec$ without idle time, so the completion time of $j$ is

C_j(\sigma)=p_j+\sum_{k\prec j,\ \sigma(k)=\sigma(j)}p_k .

The value of $\sigma$ is $\sum_j w_jC_j(\sigma)$ , and $Z^*$ is the minimum value over all assignments.

The graph $G_J$ is the complete graph on $J$ in which the edge $\{j,k\}$ with $k\prec j$ has weight $c(jk)=w_jp_k$ ; $c(E_J)$ is its total weight. A partition induces the $m$ -cut $E_{\mathrm{cut}}$ , the edges whose endpoints lie in different parts, of weight $c(E_{\mathrm{cut}})$ ; $Z^*_{\mathrm{cut}}$ is the maximum weight of an $m$ -cut.

The convex quadratic relaxation (CQP) of §2.2, specialised to identical machines, has variables $a_{ij}\ge 0$ with $\sum_i a_{ij}=1$ and objective $Z_{CQP}(a)=\sum_j w_jC_j$ where

C_j=\sum_{i=1}^m a_{ij}\Big(\frac{1+a_{ij}}{2}\,p_j+\sum_{k\prec j}a_{ik}\,p_k\Big)\qquad(11).

Its optimum value is $Z^*_{CQP}$ .

Formalization targets

Goal: Theorem 6.1

For $\rho\le 1$ , any assignment $\sigma$ whose $m$ -cut weighs at least $\rho\cdot Z^*_{\mathrm{cut}}$ satisfies

\sum_j w_jC_j(\sigma)\le\big(\rho+m(1-\rho)\big)\,Z^* .

That is, a $\rho$ -approximation algorithm for Max- $m$ -Cut translates into a $(\rho+m(1-\rho))$ -approximation algorithm for $Pm\,|\,|\sum w_jC_j$ . The constant $\rho$ is a parameter, so the goal does not depend on the best known cut algorithm.

Milestones

(36): for every partition, $c(E_J)=\sum_j w_jC_j-\sum_j w_jp_j+c(E_{\mathrm{cut}})$ .
Lemma 2.5: $\bar a_{ij}=1/m$ is an optimum of (CQP), unique when the ratios $w_j/p_j$ are pairwise different and positive.
(37): $Z^*\ge Z^*_{CQP}=\frac1m c(E_J)+\big(\frac12+\frac1{2m}\big)\sum_j w_jp_j$ .
(38): $Z^*_{\mathrm{cut}}\le\frac{m-1}{m}c(E_J)+\big(\frac12-\frac1{2m}\big)\sum_j w_jp_j$ .
Theorem 2.6 b) (supplementary): assigning each job independently and uniformly at random has expected value at most $\big(\frac32-\frac1{2m}\big)Z^*$ .

Significance

The result. Theorem 6.1 makes Max- $m$ -Cut algorithms usable for scheduling with an explicit loss: a cut algorithm with ratio $\rho$ close to $1$ yields a schedule within $1+m(1-\rho)$ of optimal. For $m=2$ and the Goemans–Williamson ratio $0.878$ the guarantee is $1.122$ , better than the $5/4$ of Theorem 2.6 b) and the $1.2752$ of the paper's semidefinite rounding in §5. In the other direction, (38) bounds the maximum cut of $G_J$ by the scheduling lower bound $Z^*_{CQP}$ , which is how a relaxation for scheduling becomes a bound for a cut problem. The problem itself is better understood today: $P\,|\,|\sum w_jC_j$ has a polynomial-time approximation scheme (Skutella and Woeginger 2000), and a fully polynomial one for fixed $m$ (Sahni 1976). The reduction remains of interest as a structural identity between the two problems and as the source of the closed-form relaxation bound (37).

Formalizing it. All statements are proved in the paper; none is known to have a machine-checked proof. The mission produces a formal model of identical-machine scheduling under Smith's rule, of the weighted graph $G_J$ and its $m$ -cuts, and of (CQP) for identical machines, together with the closed-form optimum of (CQP) (Lemma 2.5), which is the basis of the $\frac32-\frac1{2m}$ guarantee of Theorem 2.6 b).

Difficulty

The bookkeeping identity (36) and the final chain of inequalities are finite-sum manipulations. The substance is Lemma 2.5: that the uniform vector $\bar a$ minimizes the quadratic objective (11) over the product of simplices. The objective is not separable, since the term $\sum_{k\prec j}a_{ik}p_k$ couples jobs through Smith's order, and its convexity on the feasible region (the positive semidefiniteness established in Lemma 2.4 of the paper) is the fact on which optimality and, with distinct positive ratios, uniqueness rest. The relaxation half of (37), that $Z^*_{CQP}$ is at most the value of every schedule, needs the observation that $Z_{CQP}$ evaluated at the 0/1 vector of an assignment equals the value of that assignment.

Formalization scope

Jobs are Fin n and machines Fin m, 0-based; Smith's order is cross-multiplied ( $w_jp_k>w_kp_j$ , or equality and $j<k$ ), equal to the ratio definition because $p>0$ . Assignments are functions Fin n → Fin m, and every machine is sequenced by $\prec$ ; by Smith's rule (p. 7 of the paper, a classical result it cites) this loses no optimality, so $Z^*$ is the minimum over assignments and is never a primitive: "within factor $\alpha$ of $Z^*$ " is stated against the value of every assignment. Likewise "weight at least $\rho\cdot Z^*_{\mathrm{cut}}$ " is stated as $\rho\,c(E_{\mathrm{cut}}(\tau))\le c(E_{\mathrm{cut}}(\sigma))$ for every assignment $\tau$ , so no supremum of an empty or unbounded set can enter. The edge weight is attached to the ordered pair $(j,k)$ with $k\prec j$ and is zero on the other orientation, so each edge of $G_J$ is counted once. Standing hypotheses on every theorem: $p_j>0$ , $w_j\ge 0$ (p. 2 of the paper) and $m>0$ (needed for $1/m$ ). Theorem 6.1 keeps the page's $\rho\le 1$ .

Not formalized: polynomial running time, the phrase "approximation algorithm" beyond the value bound it asserts, and the semidefinite results of §5 and Corollary 6.2. A trivializing reading, such as stating the cut condition against a junk-valued supremum or replacing $Z^*$ by a free variable, is excluded by the encodings above.

The development needs only finite sums over Fin types and real arithmetic; the model of identical-machine scheduling under Smith's rule and the closed form of (CQP) are reusable for other results on $P\,|\,|\sum w_jC_j$ . Proofs of the milestones, alternative proofs of Lemma 2.5 (the KKT argument the paper mentions, or Goemans' symmetrization argument it gives), and a proof of Theorem 2.6 b) are all welcome.

Selected references

M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, Journal of the ACM 48(2), 2001. https://doi.org/10.1145/375827.375840
W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 1956. https://doi.org/10.1002/nav.3800030106
M. X. Goemans and D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, Journal of the ACM 42(6), 1995. https://doi.org/10.1145/227683.227684
A. Frieze and M. Jerrum, Improved approximation algorithms for MAX k-CUT and MAX BISECTION, Algorithmica 18, 1997. https://doi.org/10.1007/BF02523689
M. Skutella and G. J. Woeginger, A PTAS for minimizing the total weighted completion time on identical parallel machines, Mathematics of Operations Research 25(1), 2000. https://doi.org/10.1287/moor.25.1.63.15212
S. Sahni, Algorithms for scheduling independent tasks, Journal of the ACM 23(1), 1976. https://doi.org/10.1145/321921.321934

8 thms2 active usersReviewed

Optimization Probability·Captain: mikedeng1

On the Rate of Convergence of Optimal Solutions of Monte Carlo Approximations of Stochastic Programs 2: At a Sharp Minimum the SAA Problem Fails to Be Exact with Exponentially Small ProbabilityResearch Paper

Motivation

The sample average approximation (SAA) method replaces an expectation in a stochastic program by the average over a random sample and solves the resulting deterministic problem. It is the standard way to solve two-stage stochastic linear programs with large or continuous scenario sets, and it underlies the stochastic counterpart and sample-path optimization methods of the 1990s. A basic question is how large the sample has to be.

For smooth problems the SAA optimal solution $\hat x_N$ converges to the true one at the rate $N^{-1/2}$ of the central limit theorem. A. Shapiro and T. Homem-de-Mello (SIAM J. Optim. 11(1), 2000) observed that for problems whose optimum is a sharp minimum, as is typical of two-stage linear programs with finitely many scenarios, the picture is different. In §2 of the paper they prove that the SAA problem then returns the exact true solution with probability one for all sufficiently large $N$ . In §3, formalized here, they show that the probability of the complementary event, the SAA solution not being exactly $\bar x$ , decays exponentially in $N$ . One consequence they draw is that a modest sample can find the optimum of a problem with an astronomically large number of scenarios. This mission is the second of three on the paper; the first formalizes the almost sure statement (Theorem 2.1), the third the polyhedral case with multiple optima (Theorem 3.2).

Setting

Let $P$ be a probability measure on a sample space $(\Omega,\mathcal F)$ , $\Theta\subseteq\mathbb R^m$ , and $h:\mathbb R^m\times\Omega\to\mathbb R$ . The true problem (1.1) is

\min_{x\in\Theta}\ f(x):=\mathbb E_P\,h(x,\omega).

Given an i.i.d. sample $\omega^1,\omega^2,\dots$ with law $P$ , the SAA problem (1.2) is

\min_{x\in\Theta}\ \hat f_N(x):=\frac1N\sum_{j=1}^N h(x,\omega^j).

$A$ and $A_N$ denote the sets of optimal solutions of (1.1) and (1.2). For a function $g$ , $g'(x,d)=\lim_{t\downarrow0}(g(x+td)-g(x))/t$ is its directional derivative, and $h'_\omega(x,d)$ is that of $h(\cdot,\omega)$ . $T_\Theta(\bar x)$ is the tangent cone of $\Theta$ at $\bar x$ , and $S^{m-1}=\{d:\|d\|=1\}$ .

The standing hypotheses are those of Theorem 2.1 of the paper: (i) $h(\cdot,\omega)$ is convex for every $\omega$ ; (ii) $f$ is finite valued; (iii) $\Theta$ is closed and convex; (iv) Assumption (A): $A=\{\bar x\}$ and $\bar x$ is a sharp minimum, i.e. there is $c>0$ with

f(x)\ge f(\bar x)+c\|x-\bar x\|\qquad\text{for all }x\in\Theta. \tag{2.2}

Section 3 adds Assumption (B): with $\eta(d,\omega):=h'_\omega(\bar x,d)$ (3.1), there is $\kappa>0$ such that $\sup_{d\in S^{m-1}}|\eta(d,\omega)|\le\kappa$ for $P$ -almost every $\omega$ . It holds whenever $\Omega$ is finite.

The event of interest is

\mathcal E_N:=\{A_N\neq\emptyset\text{ and }A_N=\{\bar x\}\},\tag{3.7}

that the SAA problem has the unique optimal solution $\hat x_N=\bar x$ .

For a direction $d$ , $M_d(t)=\mathbb E_P e^{t\eta(d,\omega)}$ and $I_d(\alpha)=\sup_{t\in\mathbb R}[t\alpha-\log M_d(t)]$ (3.5) is the one-dimensional rate function of $\eta(d,\omega)$ . On the Banach space $Z=C(S^{m-1})$ , $I(z)=\sup_{z^*\in Z^*}\{z^*(z)-\log M(z^*)\}$ (3.4) is the rate function of the random element $\eta(\cdot,\omega)$ .

Formalization targets

Goal: Theorem 3.1 (p. 11)

Under (i)–(iv) and Assumption (B) there is a constant $\beta>0$ with

\limsup_{N\to\infty}\frac1N\log P(\mathcal E_N^c)\le-\beta.\tag{3.8}

The goal asserts the existence of an exponential rate and does not fix its value.

Stronger: the explicit rate (p. 12)

With $c$ from (2.2) and $\kappa$ from (B),

\limsup_{N\to\infty}\frac1N\log P(\mathcal E_N^c)\le-\frac{c^2}{2\kappa^2},

which is (3.8) combined with (3.15).

Milestones

In the order of the proof:

the reduction $P(\mathcal E_N^c)\le P(\zeta_N\in F)$ with $\zeta_N=\hat f'_N(\bar x,\cdot)$ and $F=\{z:\inf_{T_\Theta(\bar x)\cap S^{m-1}}z\le0\}$ (p. 11);
for a random variable $X$ with $|X|\le\kappa$ and $\Lambda(t)=\log\mathbb E e^{tX}$ , the bounds $|\Lambda'|\le\kappa$ , $|\Lambda''|\le\kappa^2$ (3.11) and $|\Lambda'(t)-\Lambda'(s)|\le\kappa^2|t-s|$ (3.12);
the quadratic lower bound $I_d(\alpha)\ge|\alpha-\bar\alpha_d|^2/(2\kappa^2)$ (3.13);
$I_d(0)\ge c^2/(2\kappa^2)$ on $T_\Theta(\bar x)\cap S^{m-1}$ (3.14);
the comparison $I(z)\ge\sup_{d}I_d(z(d))$ (3.6);
$\beta=\inf_{z\in F}I(z)\ge c^2/(2\kappa^2)$ (3.15).

Significance

Theorem 3.1 says that at a sharp minimum the SAA method is exact except on an event of probability $O(e^{-\beta N})$ . The sample size needed for a given confidence therefore grows only logarithmically in the confidence level, and it does not depend on the number of scenarios. This is the basis of the paper's numerical observation that problems with very many scenarios are solved exactly from samples of a few hundred. The explicit constant $c^2/(2\kappa^2)$ relates the rate to two interpretable quantities: the sharpness $c$ of the optimum and the bound $\kappa$ on the subgradients of $h(\cdot,\omega)$ at $\bar x$ .

The result is proved in the paper. As far as is known it has no machine-checked proof. A complete formalization produces three things. First, a Lean proof that the SAA problem recovers a sharp optimum exactly with exponentially small failure probability. Second, the elementary facts about cumulant generating functions of bounded variables, (3.11)–(3.13), which are reusable in any Chernoff-type argument. Third, the link between the rate function of a $C(K)$ -valued random element and its one-dimensional projections, (3.6).

Difficulty

The event $\mathcal E_N^c$ is controlled by the positivity of a whole function, $\zeta_N(d)=\hat f_N'(\bar x,d)$ , on the infinite set $T_\Theta(\bar x)\cap S^{m-1}$ . A Chernoff bound for each fixed direction $d$ is easy, but there are uncountably many directions, so a union bound over $d$ is not available. The paper handles this with Cramér's theorem in the separable Banach space $C(S^{m-1})$ , and that infinite-dimensional large deviations upper bound is not in Mathlib. A proof must either develop that bound or find a finite-dimensional substitute that keeps an exponential rate.

A second difficulty is conversion. Cramér's theorem gives a rate in terms of $\inf_{z\in F}I(z)$ , and that infimum must be shown positive. Positivity comes from the sharpness constant $c$ through the strong convexity of the one-dimensional rate functions, which needs the bounds (3.11)–(3.13) on the cumulant generating function.

Formalization scope

The decision space is EuclideanSpace ℝ (Fin m). The scenario space $(\Omega,\mathcal F,P)$ carries the law of one scenario. The sample is one i.i.d. sequence of $\Omega$ -valued maps on a separate probability space $(S,Q)$ , and $\hat f_N$ uses its first $N$ terms. Optimal sets are written without infima: $A_N=\{\bar x\}$ encodes "nonempty and equal to $\{\bar x\}$ ".
Directional derivatives are the limUnder of the difference quotient as $t\downarrow0$ . Every statement assumes (i), under which the limit exists. The tangent cone is Mathlib's tangentConeAt, which for convex $\Theta$ is the closure of the cone of feasible directions.
Disclosed pins.
- "f finite valued" is $P$ -integrability of every $h(x,\cdot)$ , which includes measurability.
- Assumption (B) is stated pointwise in $d\in S^{m-1}$ under the almost sure quantifier.
- $\mathcal E_N^c$ is not shown measurable, so its probability is an outer measure, and an upper bound on it is the stronger claim.
- The rate (3.8) is stated in the equivalent form: there is $\beta>0$ such that for every $\varepsilon>0$ , eventually $Q(\mathcal E_N^c)\le e^{-(\beta-\varepsilon)N}$ . A logarithm of a real probability is never taken.
- Rate functions $I_d$ and $I$ take values in $(-\infty,+\infty]$ . They use the published extended-real logMGF and legendre, under which $I_d(\alpha)=+\infty$ for $|\alpha|>\kappa$ is a genuine value, not a default.
- The one-dimensional bounds (3.11)–(3.13) are stated for an arbitrary bounded measurable random variable.
Trivializing readings are ruled out. The goal's $\beta$ is fixed before $\varepsilon$ and $N$ , so it cannot depend on them. The event is uniqueness and equality, $A_N=\{\bar x\}$ , not $\bar x\in A_N$ . The standing hypotheses are jointly satisfiable: a sorry-free check exhibits them for $h(x,\omega)=\|x\|$ , $\Theta=\mathbb R^m$ and a product-measure sample.
Infrastructure. A complete development needs: directional derivatives of finite convex functions and their continuity in the direction; interchange of directional derivative and expectation (Proposition 2.2 of the paper, formalized in the first mission of the series); derivatives of the cumulant generating function (Mathlib's ProbabilityTheory.cgf and its analyticity); and an exponential upper bound for empirical means in $C(S^{m-1})$ or a substitute. The cumulant generating function lemmas and any Banach-space Cramér bound are reusable beyond this mission. Contributions are welcome for any milestone, and for alternative proofs of the goal that avoid Cramér's theorem in function space.

Selected references

A. Shapiro and T. Homem-de-Mello, On the rate of convergence of optimal solutions of Monte Carlo approximations of stochastic programs, SIAM J. Optim. 11(1):70–86, 2000. https://doi.org/10.1137/S1052623498349541 (formalized from the authors' preprint, Stochastic Programming E-Print Series)
J.-D. Deuschel and D. W. Stroock, Large Deviations, Academic Press, 1989 (Cramér's theorem in Banach spaces, cited as [8]).
J.-B. Hiriart-Urruty and C. Lemaréchal, Convex Analysis and Minimization Algorithms II, Springer, 1993, Theorem X.4.2.2 (strong convexity of conjugates, cited as [12]). https://doi.org/10.1007/978-3-662-06409-2
A. J. Kleywegt, A. Shapiro and T. Homem-de-Mello, The sample average approximation method for stochastic discrete optimization, SIAM J. Optim. 12(2):479–502, 2002. https://doi.org/10.1137/S1052623499363220

11 thms2 active usersReviewed

Operations Research

Missions

Optimization of Convex Risk Functions 2: On a Banach Lattice, a Proper Convex Monotone Risk Function Is Continuous and Subdifferentiable on the Interior of Its DomainResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.1 (p. 437)

Milestones (the steps of the paper's argument, pp. 436–437)

Companions

Significance

Difficulty

Formalization scope

Selected references

Primal and Dual Linear Decision Rules in Stochastic and Robust Optimization 2: With Random Recourse, the SDP (3.14) Conservatively Approximates the Linear Decision Rule Problem, Exactly for l = 1Research Paper

Linear decision rules for stochastic programs with random recourse

Setting

Formalization targets

Goal: Theorem 2, primal half (p. 17)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimization of Convex Risk Functions 1: Dual Representation of a Lower Semicontinuous Convex Risk Function, with Monotonicity, Translation Equivariance and Homogeneity Read Off Its Dual DomainResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.2 (p. 435)

Milestones

Companion: the risk envelope (2.8), p. 436

Significance

Difficulty

Formalization scope

Selected references

Flows and Decompositions of Games: Harmonic and Potential Games 3: In Every Harmonic Game the Uniformly Mixed Strategy Profile Is a Mixed Nash EquilibriumResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimization of Convex Risk Functions 3: A Distribution-Invariant Risk Function Is Consistent with the Increasing Convex Order Iff It Is Monotone and Risk AverseResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.1 (p. 446)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Flows and Decompositions of Games: Harmonic and Potential Games 2: Harmonic Games Generically Have No Pure Nash EquilibriumResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 5.1

Stronger structural form

Milestones

Significance

Difficulty

Formalization scope

Selected references

Retailer-Supplier Flexible Commitments Contracts: A Robust Optimization Approach: With Box Demand Uncertainty the Min-Max RSFC Problem Has the Same Optimal Value on the Extreme DemandsResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 1 (p. 269)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Distributionally Robust Optimization and Its Tractable Approximations 3: The Infimal Convolution of π¹, π², π³ Bounds the Worst Case over the Intersected Families and Improves on EachResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 (p. 911)