Operations Research

Motivation

Many optimization problems in simulation-based design, reinforcement learning and machine learning can be evaluated but not differentiated. Their objective is an expectation $f(x) = \mathbb E[F(x,\xi)]$ that can only be sampled through noisy function values $F(x,\xi)$. Gradients may be unavailable because the model is a black box, a simulator, or a legacy code. Methods for this setting are called zeroth-order or derivative-free stochastic methods. The objective $f$ is often nonconvex, so the realistic target is an approximately stationary point, $\|\nabla f(x)\|^2 \le \epsilon$, not a global minimizer.

Ghadimi and Lan (arXiv:1309.5549; SIAM J. Optim. 23(4), 2013) gave the first complexity bounds for stochastic zeroth-order methods on nonconvex problems. Their randomized stochastic gradient free (RSGF) method combines two ingredients. The first is the Gaussian smoothing and random finite-difference estimator of Nesterov and Spokoiny (Found. Comput. Math. 17, 2017; preprint 2011). The second is a randomized stopping rule that outputs an iterate chosen at random along the trajectory. The resulting bound has become the standard reference point for derivative-free nonconvex stochastic optimization.

Timeline:

• 1952: Kiefer and Wolfowitz introduce finite-difference stochastic approximation.
• 2011: Nesterov and Spokoiny analyze Gaussian random gradient-free oracles for convex and deterministic nonconvex problems.
• 2013: Ghadimi and Lan prove the nonconvex stochastic rate of the RSGF method (Theorem 3.2) and its $O(n/\epsilon^2)$ complexity (Corollary 3.3).

Setting

Let $\mathbb R^n$ be Euclidean space and let $\xi$ be a random vector with distribution $P$ on a measurable space $\Xi$. The problem is

$$f^* := \inf_{x\in\mathbb R^n}\Big\{ f(x) := \int_\Xi F(x,\xi)\,dP(\xi) \Big\}. \tag{3.1}$$

The sample functions $F(\cdot,\xi)$ lie in $\mathcal C^{1,1}_L(\mathbb R^n)$ almost surely: they are differentiable, and their gradients are $L$-Lipschitz. Two assumptions describe the noise. Assumption A1 concerns the first-order oracle $G(x,\xi) = \nabla_x F(x,\xi)$: it is unbiased, $\mathbb E[G(x,\xi)] = \nabla f(x)$, and has variance at most $\sigma^2$. Assumption A3 says the zeroth-order oracle is unbiased, $\mathbb E[F(x,\xi)] = f(x)$.

For a smoothing parameter $\mu > 0$ and an $n$-dimensional standard Gaussian vector $u$, the Gaussian smoothing of $f$ is $f_\mu(x) = \mathbb E_u[f(x+\mu u)]$ (3.3). The RSGF method starts from $x_1$ and uses stepsizes $\gamma_k$. At step $k$ it draws a fresh sample $\xi_k$ and a fresh Gaussian direction $u_k$, forms the zeroth-order estimator

$$G_\mu(x_k,\xi_k,u_k) = \frac{F(x_k+\mu u_k,\xi_k) - F(x_k,\xi_k)}{\mu}\,u_k, \tag{3.12}$$

and sets $x_{k+1} = x_k - \gamma_k G_\mu(x_k,\xi_k,u_k)$ (3.13). The output is $x_R$, where the random iteration count $R \in \{1,\dots,N\}$ has the probability mass function

$$P_R(k) = \frac{\gamma_k - 2L(n+4)\gamma_k^2}{\sum_{j=1}^N[\gamma_j - 2L(n+4)\gamma_j^2]}. \tag{3.15}$$

In the Lean development, $f$ is objective P F, $G_\mu$ is szoGrad (the published RandomGradFree.Shared.oracle applied to $F(\cdot,\xi)$), and $f_\mu$ is the published RandomGradFree.Shared.smoothing. The smoothing parameter is μs, because μ names the probability measure.

Formalization targets

Goal: Theorem 3.2 a)

Let $0 < \gamma_k < 1/[2(n+4)L]$ for $k = 1,\dots,N$, with $N \ge 1$, and let $D_f^2 = 2(f(x_1)-f^*)/L$. Then

$$\frac1L\,\mathbb E\|\nabla f(x_R)\|^2 \le \frac{D_f^2 + 2\mu^2(n+4)\big(1 + L(n+4)^2\sum_{k=1}^N(\frac{\gamma_k}{4} + L\gamma_k^2)\big) + 2(n+4)\sigma^2\sum_{k=1}^N\gamma_k^2}{\sum_{k=1}^N[\gamma_k - 2L(n+4)\gamma_k^2]}. \tag{3.16}$$

The stepsizes are left free, so every stepsize policy specializes the goal.

Companions

• Theorem 3.2 b), (3.17): for convex $f$ with a minimizer $x^*$, the bound on $\mathbb E[f(x_R) - f^*]$.
• Corollary 3.3, (3.26): for the constant stepsizes (3.24) and $\mu \le D_f/((n+4)\sqrt{2N})$,

$$\frac1L\,\mathbb E\|\nabla f(x_R)\|^2 \le \frac{12(n+4)LD_f^2}{N} + \frac{4\sigma\sqrt{n+4}}{\sqrt N}\Big(\tilde D + \frac{D_f^2}{\tilde D}\Big).$$

Milestones

The milestones follow the paper's proof.

• Properties of the smoothing. These are Theorem 3.1 a)–c): $f_\mu$ has an $L$-Lipschitz gradient given by (3.4), $|f_\mu - f| \le \frac{\mu^2}{2}Ln$ (3.5), the gradient bound (3.6), and the second-moment bound (3.7). Three of these are already on the platform and are referenced. Two consequences follow, (3.9) and (3.11).
• Unbiasedness, (3.14): the estimator $G_\mu$ is unbiased for $\nabla f_\mu$.
• The proof chain of Theorem 3.2. The pathwise descent inequality (3.19), the martingale identity (3.20) and the conditional second-moment bound (3.21) combine into the weighted bound (3.23). The $R$-weighting identity converts (3.23) into (3.16).

Significance

The theorem shows that function values alone suffice to find approximately stationary points of nonconvex stochastic programs. The price is a factor of the dimension $n$: with constant stepsizes the RSGF method needs $O(n/\epsilon^2)$ iterations, against $O(1/\epsilon^2)$ for the first-order RSG method. The randomized output rule and the analysis through $f_\mu$ are reused in later zeroth-order methods, including two-phase variants, mirror-descent variants and variance-reduced schemes.

The result is proved in the paper. It is not formalized anywhere known to this mission. The platform already holds parts of the Gaussian-smoothing theory from the Nesterov–Spokoiny series, but only for convex problems with exact function values. This mission adds:

• the nonconvex form of the second-moment bound (3.7);
• the gradient-approximation bound (3.6);
• the stochastic sampling model with conditional expectations;
• the first machine-checkable statement of a nonconvex stochastic zeroth-order rate.

Difficulty

The first idea is to treat the RSGF method as the first-order RSG method run on $f_\mu$ with the unbiased estimator $G_\mu$, and to quote the RSG bound. This fails, because the variance $\mathbb E\|G_\mu - \nabla f_\mu\|^2$ has no uniform bound: by (3.7) it grows with $\|\nabla f(x_k)\|^2$ at the random iterate. The analysis has to carry that term along and absorb it into the left side, which is where the weights $\gamma_k - 2L(n+4)\gamma_k^2$ come from. It must also move between $\nabla f_\mu$ and $\nabla f$ through (3.6) at a cost polynomial in $n$.

On the formal side, three obstacles stand out.

• The Gaussian moment estimates behind (3.6) and (3.7) need bounds on $\mathbb E\|u\|^p$ up to $p = 6$ for a standard Gaussian vector.
• Conditional expectations with respect to $\sigma(\zeta_{[k-1]})$ are taken at random iterates that depend on the past, so independence of the fresh samples must be used carefully.
• Integrability must be established for every quantity before expectations can be manipulated.

Formalization scope

• Space. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The constants $(n+3)$, $(n+4)$, $(n+6)$ use the same natural number $n$. The Gaussian is Mathlib's stdGaussian.
• Iterates. They are indexed from $1$, and $R$ takes values in $\{1,\dots,N\}$.
• Optimal values. $f^*$ is the infimum of $f$ (IsGLB), with $f$ bounded below. The paper's $f^*_\mu := \min f_\mu$ (3.10) is read as an infimum, since the minimum need not be attained.
• Smoothness. $F(\cdot,\xi) \in \mathcal C^{1,1}_L$ is required for $P$-almost every $\xi$, as on the page.
• Assumption A1 is stated at every point $x$ for $G = \nabla_x F$.
• Assumption A3 is the definition of $f$, with $F(x,\cdot)$ integrable.

The following are explicit additions; the paper leaves them implicit.

• Sampling. The samples $\xi_k \sim P$ and $u_k \sim \mathcal N(0,I_n)$ are measurable and mutually independent, and $R$ is independent of all of them.
• Measurability and integrability. $F$ is jointly measurable, and $\nabla_x F(x,\cdot)$ is integrable.
• Stepsizes are positive.
• Corollary 3.3 assumes $\sigma > 0$.

Every conclusion about an expectation also asserts the integrability of its integrand. A non-integrable function has Lean integral $0$, so a bound without this conjunct could hold for the wrong reason.

The goal is stated about the objects of the method only: $F$, $P$, $f$, the run (3.12)–(3.13), $R$ and the constants. It does not mention $f_\mu$, $\Delta_k$ or the filtration, so it cannot be discharged by choosing an auxiliary object.

A complete development needs:

• Gaussian moment bounds and differentiation under the Gaussian integral;
• conditional expectation with respect to the natural filtration of an independent sequence;
• the descent lemma for $\mathcal C^{1,1}_L$ functions.

The Gaussian-smoothing lemmas (3.6), (3.7) and (3.9) are reusable by any zeroth-order mission. Contributions of proofs of individual milestones are welcome, as are alternative proofs of (3.7) without Nesterov's bound.

Selected references

• S. Ghadimi and G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23(4):2341–2368, 2013. Preprint arXiv:1309.5549v1, the version cited here. https://arxiv.org/abs/1309.5549
• Y. Nesterov and V. Spokoiny, Random gradient-free minimization of convex functions, Found. Comput. Math. 17:527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
• J. Kiefer and J. Wolfowitz, Stochastic estimation of the maximum of a regression function, Ann. Math. Statist. 23(3):462–466, 1952. https://doi.org/10.1214/aoms/1177729392

Motivation

Mobile devices run applications whose computational load can exceed what the device itself can serve in reasonable time and with reasonable battery drain. Computation offloading sends part of that load elsewhere: to a cloudlet, a small cluster of servers one wireless hop away, or to a distant cloud reached through the wide-area network. The cloudlet is shared, so its response time depends on how much load all users send to it, and each user's best offloading decision depends on everybody else's. Cardellini, De Nitto Personé, Di Valerio, Facchinei, Grassi, Lo Presti and Piccialli (Math. Program., 2016, DOI 10.1007/s10107-015-0881-6) model this as a non-cooperative game between users and study it with the tools of variational inequalities.

The game is a generalized Nash equilibrium problem (GNEP): not only the costs but also the feasible sets of the players depend on the other players' choices, because all users share one capacity constraint on the cloudlet. GNEPs with a shared convex constraint (jointly convex games) can be reduced to a single variational inequality, a reduction the paper takes from Facchinei, Fischer and Piccialli (Oper. Res. Lett. 2007, DOI 10.1016/j.orl.2006.03.004); Facchinei and Kanzow survey the area (Ann. Oper. Res. 2010, DOI 10.1007/s10479-009-0653-x). This mission formalizes the first step of the paper's analysis: the game has an equilibrium.

Setting

There are $N$ users $u=1,\dots,N$ and three tiers $I=\{m,\mathrm{clet},\mathrm{cloud}\}$ (mobile device, cloudlet, cloud). User $u$ chooses the fractions $x_u=(x_{u,m},x_{u,\mathrm{clet}},x_{u,\mathrm{cloud}})$ of its tasks run on each tier. A profile is $x=(x_1,\dots,x_N)\in\mathbb R^{3N}$.

The data are reals $\alpha_u,\beta_u,\gamma_u,\delta_u$ (arrival rates divided by service or transfer rates), powers $P_{u,m},P_{u,t},P_{u,\max}$, the number $n\ge1$ of cloudlet servers, the offloadable fraction $\chi\in(0,1]$ and a utilisation cap $U_{\max}$. Assumption A requires $U_{\max}$ and every $\alpha_u,\delta_u$ to lie in $(0,1)$.

User $u$'s private feasible set is

$$\tilde K_u=\Big\{x_u\in\mathbb R^3_+:\ \textstyle\sum_{i\in I}x_{u,i}=1,\ x_{u,\mathrm{clet}}+x_{u,\mathrm{cloud}}\le\chi,\ \alpha_uP_{u,m}x_{u,m}+\beta_uP_{u,t}(x_{u,\mathrm{clet}}+x_{u,\mathrm{cloud}})\le P_{u,\max}\Big\},$$

the shared constraint is $\Omega=\{x:\frac1n\sum_v\delta_vx_{v,\mathrm{clet}}\le U_{\max}\}$, and the joint feasible set is $K=\big(\prod_u\tilde K_u\big)\cap\Omega$. User $u$ minimises the mean response cost

$$\lambda_uR_u(x_u,x_{-u})=\frac{\alpha_ux_{u,m}}{1-\alpha_ux_{u,m}}+\beta_ux_{u,\mathrm{clet}}+\gamma_ux_{u,\mathrm{cloud}}+\frac{\delta_ux_{u,\mathrm{clet}}}{1-\frac1n\sum_v\delta_vx_{v,\mathrm{clet}}}$$

over $\{y\in\tilde K_u:(y,x_{-u})\in\Omega\}$. A solution of the GNEP is a profile $\bar x\in K$ at which no user can lower its cost by a deviation that keeps the shared constraint satisfied.

The map $F:\mathbb R^{3N}\to\mathbb R^{3N}$ stacks the users' partial gradients,

$$F(x)_u=\Big(\frac{\alpha_u}{(1-\alpha_ux_{u,m})^2},\ \beta_u+\delta_u\frac{1-\frac1n\sum_{v\ne u}\delta_vx_{v,\mathrm{clet}}}{\big(1-\frac1n\sum_v\delta_vx_{v,\mathrm{clet}}\big)^2},\ \gamma_u\Big),$$

and $\bar x$ solves the variational inequality $\mathrm{VI}(K,F)$ if $\bar x\in K$ and $F(\bar x)^\top(x-\bar x)\ge0$ for all $x\in K$. Such solutions are the variational (or normalized) solutions of the game.

Formalization targets

Goal: Proposition 1 (p. 12)

Under Assumption A, and provided every $\tilde K_u$ is nonempty,

$$\exists\,\bar x\in K\ \ \forall u\ \ \forall y\in\tilde K_u\ \text{with}\ (y,\bar x_{-u})\in\Omega:\quad \lambda_uR_u(\bar x_u,\bar x_{-u})\le\lambda_uR_u(y,\bar x_{-u}).$$

Milestones

1. $F(x)_u=\nabla_{x_u}\lambda_uR_u(x)$ wherever both denominators are positive (p. 11).
2. For fixed $x_{-u}$, user $u$'s feasible set is convex and its cost is convex on it (p. 11).
3. Every solution of $\mathrm{VI}(K,F)$ is a solution of the GNEP (proof of Proposition 1).
4. $F$ is continuous on $K$, and $K$ is compact and convex (proof of Proposition 1).
5. $\mathrm{VI}(K,F)$ has a solution (proof of Proposition 1, citing Facchinei–Pang, Corollary 2.2.5).

Milestones 3 and 5 give the goal; milestones 1 and 2 are what milestone 3 rests on, and milestone 4 is what milestone 5 rests on. The platform's Proved statement of Brouwer's fixed-point theorem (AGT.brouwer_fixed_point) is included as a reference item for milestone 5.

Significance

The result. Existence of an equilibrium is the precondition for everything else in the paper: the monotonicity of $F$ (Theorem 1), the reformulation with a cloudlet price as an extended game (Theorem 2), and the distributed algorithm whose convergence is Theorem 3. Proposition 1 also shows that variational solutions exist, which is the specific equilibrium the paper's algorithm computes.

Formalizing it. The result is proved in the paper, in three lines that cite two textbook theorems. The work here is to make those citations machine-checked for this concrete model: that the closed-form $F$ is indeed the stacked partial gradient, that each user's problem is convex despite the rational cost terms, that the VI-to-GNEP reduction holds, and that a VI on a compact convex set with continuous map has a solution. None of these steps is formalized in Mathlib for GNEPs; the last is a finite-dimensional Hartman–Stampacchia theorem, which Mathlib does not contain. No part of this paper has a machine-checked proof.

Difficulty

The obvious argument is to apply Kakutani's theorem to the best-response correspondence. With a shared constraint this needs lower semicontinuity of the feasible-set map $x_{-u}\mapsto\{y\in\tilde K_u:(y,x_{-u})\in\Omega\}$, which is a separate argument, and Kakutani is not in Mathlib either. The VI route avoids it but has its own points. The cost has the rational terms $\alpha_ux_{u,m}/(1-\alpha_ux_{u,m})$ and $\delta_ux_{u,\mathrm{clet}}/D(x)$, and convexity and differentiability must be checked on the region where the denominators are positive; on a user's feasible set this needs Assumption A and the shared constraint, not the private constraints alone. The existence of a VI solution needs a fixed-point theorem on a compact convex set, and Mathlib has no Brouwer theorem. That is why the platform's statement of it is attached to this mission.

Formalization scope

Users are Fin N (0-based) and tiers an inductive type Tier with three constructors; a profile is Fin N → Tier → ℝ. The inner product $a^\top b$ is the coordinatewise double sum (not Mathlib's sup norm on Pi types). The cost and $F$ are the paper's closed forms; $F$ is not defined as a derivative, so milestone 1 has content. Lean's $x/0=0$ makes both formulas junk where a denominator vanishes. Under Assumption A both denominators are positive on $K$ and at every point the GNEP definition compares, and milestone 1 assumes the two positivity conditions explicitly.

Standing hypotheses in every statement: Assumption A, $n\ge1$, $0<\chi\le1$. Nothing is assumed of $\beta_u,\gamma_u$ or the powers, as in the paper. Added hypothesis: every $\tilde K_u$ is nonempty, in the goal and in milestone 5. The printed proposition is false without it: if $0<P_{u,\max}<\min(\alpha_uP_{u,m},\beta_uP_{u,t})$ then $\tilde K_u=\emptyset$, so $K=\emptyset$. The condition is equivalent to $K\ne\emptyset$. Milestone 4 adds convexity of $K$ to the paper's "continuous and compact".

Trivializing formalizations are ruled out: $K$ cannot be empty under the added hypothesis, $F$ is not a derivative by definition, no statement evaluates the cost at a point with a vanishing denominator, and the GNEP keeps the shared constraint in each player's feasible set (dropping it gives a different game, a NEP).

Contributions welcome: a finite-dimensional Hartman–Stampacchia theorem (reusable well beyond this mission), the general VI-implies-GNEP reduction for jointly convex games, and proofs of the model-specific milestones.

Selected references

• V. Cardellini, V. De Nitto Personé, V. Di Valerio, F. Facchinei, V. Grassi, F. Lo Presti, V. Piccialli, A game-theoretic approach to computation offloading in mobile cloud computing, Mathematical Programming (2016). https://doi.org/10.1007/s10107-015-0881-6 (accepted manuscript: IRIS Sapienza, handle 11573/779661)
• F. Facchinei, A. Fischer, V. Piccialli, On generalized Nash games and variational inequalities, Operations Research Letters 35 (2007). https://doi.org/10.1016/j.orl.2006.03.004
• F. Facchinei, C. Kanzow, Generalized Nash equilibrium problems, Annals of Operations Research 175 (2010). https://doi.org/10.1007/s10479-009-0653-x
• F. Facchinei, J.-S. Pang, Finite-Dimensional Variational Inequalities and Complementarity Problems, Springer, 2003. https://doi.org/10.1007/b97543

Motivation

Ordinary least squares and its robust relatives (least absolute deviations, Huber, $\epsilon$-insensitive and quantile regression) fit a linear predictor by minimizing an average loss over the training sample. That average estimates the out-of-sample error poorly when the sample is small, and the usual fix is to add a regularization penalty such as a norm of the weights. Choosing that penalty is often a heuristic. Distributionally robust optimization gives one principled derivation of it: hedge against every data-generating distribution that is close to the empirical one in a Wasserstein distance, and minimize the worst-case expected loss.

S. Shafieezadeh-Abadeh, D. Kuhn and P. Mohajerin Esfahani, Regularization via Mass Transportation (arXiv:1710.10016v3, 2019; JMLR 20, 2019), show that for linear regression with a convex Lipschitz loss this worst-case problem is exactly a regularized empirical risk problem, with an explicit dual-norm penalty. The same identity appears for the logistic loss in Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn, Distributionally Robust Logistic Regression (NeurIPS 2015, arXiv:1509.09259). For a general convex loss it is Theorem 10 of the tutorial by Kuhn, Mohajerin Esfahani, Nguyen and Shafieezadeh-Abadeh (arXiv:1908.08729). Blanchet, Kang and Murthy (arXiv:1610.05627) obtain the square-root Lasso from a type-2 transport cost. This mission formalizes the regression theorem of the first paper, Theorem 3.1(ii) on p. 8. The source PDF is the arXiv preprint v3, and every page and label cited here refers to it.

Setting

Data. Inputs are $x\in\mathbb R^n$ and outputs are $y\in\mathbb R$. A pair is written $\xi=(x,y)\in\mathbb R^{n+1}$. The training samples are $(\hat x_i,\hat y_i)$ for $i=1,\dots,N$, and $\hat{\mathbb P}_N=\frac1N\sum_{i=1}^N\delta_{(\hat x_i,\hat y_i)}$ is their empirical distribution (§2.1, p. 5).

Hypotheses and loss. A weight vector $w\in\mathbb R^n$ defines the linear hypothesis $h(x)=\langle w,x\rangle$. A univariate convex loss $L:\mathbb R\to\mathbb R$ defines the regression loss $\ell(\langle w,x\rangle,y)=L(\langle w,x\rangle-y)$ (§3.1, p. 8). The residual $\langle w,x\rangle-y$ is the pairing of $\xi$ with the vector $(w,-1)$.

Norms. $\mathbb R^{n+1}$ carries an arbitrary norm $\|\cdot\|$ with dual norm $\|z\|_*=\sup\{\langle z,\xi\rangle:\|\xi\|\le1\}$ (§1.1, p. 4). The Lipschitz modulus of $L$ is $\mathrm{lip}(L)=\sup_{z\ne z'}|L(z)-L(z')|/|z-z'|$, and the convex conjugate is $L^*(\theta)=\sup_z\theta z-L(z)$ (§1.1).

Wasserstein ball. With transport cost $d(\xi,\xi')=\|\xi-\xi'\|$, the Wasserstein distance (Definition 2.2, p. 7) is

$$W(\mathbb Q,\mathbb Q')=\inf_\Pi\int d(\xi,\xi')\,\Pi(\mathrm d\xi,\mathrm d\xi'),$$

where the infimum runs over couplings $\Pi$ of $\mathbb Q$ and $\mathbb Q'$. The ball of radius $\rho\ge0$ is $\mathbb B_\rho(\hat{\mathbb P}_N)=\{\mathbb Q:\mathbb Q(\Xi)=1,\ W(\mathbb Q,\hat{\mathbb P}_N)\le\rho\}$ (3). The distributionally robust regression problem is

$$\inf_w\ \sup_{\mathbb Q\in\mathbb B_\rho(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[L(\langle w,x\rangle-y)\big].\qquad(4)$$

Formalization targets

Goal: Theorem 3.1(ii), p. 8

Let $\Xi=\mathbb R^{n+1}$, $\rho\ge0$, $N\ge1$, and let $L$ be nonnegative, convex and Lipschitz continuous. Then for every $w$

$$\sup_{\mathbb Q\in\mathbb B_\rho(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[L(\langle w,x\rangle-y)\big]=\frac1N\sum_{i=1}^NL(\langle w,\hat x_i\rangle-\hat y_i)+\rho\,\mathrm{lip}(L)\,\|(w,-1)\|_*,$$

so (4) and the regularized problem (6) have the same optimal value.

Milestones

1. Lemma A.1 (p. 28). The worst case over the ball equals $\inf_{\lambda\ge0}\lambda\rho+\frac1N\sum_i\sup_\xi[I(\xi)-\lambda d(\xi,\hat\xi_i)]$. This milestone is linked to the published, proved WassersteinDRO.Duality.strong_duality_worst_case_risk_v2, which covers it for $\rho>0$.
2. Lemma A.3 (p. 29). For $\gamma>0$, $\sup_\zeta L(\langle\beta,\zeta\rangle)-\gamma\|\zeta-\hat\zeta\|$ equals $L(\langle\beta,\hat\zeta\rangle)$ if $\mathrm{lip}(L)\|\beta\|_*\le\gamma$, and $+\infty$ otherwise.
3. End of the proof of Lemma A.3 (p. 30). $\mathrm{lip}(L)=\sup\{|\theta|:L^*(\theta)<\infty\}$.
4. The inf-over-$\lambda$ display in the proof of Theorem 3.1(ii) (pp. 30–31). The worst case equals $\inf\{\lambda\rho+\frac1N\sum_iL(\langle w,\hat x_i\rangle-\hat y_i):\lambda\ge0,\ \mathrm{lip}(L)\|(w,-1)\|_*\le\lambda\}$.

Significance

The result. The theorem turns an infinite-dimensional min–max problem over distributions into a finite convex program over $w$: an empirical average plus a norm penalty. The penalty is not $\|w\|_*$ but $\|(w,-1)\|_*$, because the transport cost moves outputs as well as inputs. It scales with the radius $\rho$ and with the Lipschitz modulus of the univariate loss. With the Huber, $\epsilon$-insensitive and pinball losses it gives Corollaries 3.2–3.4 of the paper. It also gives a statistical reading of the regularization weight as a Wasserstein radius, which the paper's §4 turns into generalization bounds.

Formalizing it. The theorem is proved in the paper; none of its items is formalized yet except Lemma A.1. Lemma A.1 is available in a general form (any $p\ge1$, any closed support set, $\rho>0$) as a proved platform theorem from the mission Wasserstein Distributionally Robust Optimization. The per-$w$ identity also follows from the proved WassersteinDRO.Duality.convex_loss_p1_v2 (Theorem 10 of the tutorial, also present as WassersteinDRO.Regularization.convex_loss_p1_v2; the public mission Wasserstein Distributionally Robust Optimization IV has it as goal) once one shows that $\mathrm{lip}(L\circ\langle(w,-1),\cdot\rangle)=\mathrm{lip}(L)\|(w,-1)\|_*$. No platform item states that factorization. What this mission adds is the paper's explicit form of the penalty, Lemma A.3 (the inner supremum for an arbitrary convex Lipschitz loss and an arbitrary norm), and the conjugate description of the Lipschitz modulus. The last two are reusable in classification (mission I of this series states them again in its own namespace) and in every Wasserstein-regularization result with linear hypotheses.

Difficulty

The obvious argument is to write the worst case as a supremum over perturbations of the samples and bound each perturbed loss by its Lipschitz constant. That gives only the inequality "$\le$", and only for one Lipschitz constant. The identity needs two further steps that this bound does not supply. First, the bound must be attained: the supremum over distributions has to be shown to reach $\rho\,\mathrm{lip}(L)\|(w,-1)\|_*$, a matching lower bound that a Lipschitz estimate cannot give. Second, $\mathrm{lip}(L)$ must be the modulus, not any constant: an upper Lipschitz constant $K>\mathrm{lip}(L)$ makes the identity false. In Lemma A.3 the case $\mathrm{lip}(L)\|\beta\|_*=\gamma$ sits exactly on the boundary between a finite and an infinite supremum. A further point is that the duality of Lemma A.1 needs $\rho>0$, while the theorem includes $\rho=0$.

Formalization scope

• Space. $\mathbb R^{n+1}$ with an arbitrary norm is an abstract finite-dimensional real normed space E with its Borel σ-algebra. A continuous linear isomorphism e : E ≃L[ℝ] (Fin n → ℝ) × ℝ reads off inputs and outputs. The theorem therefore covers every norm on $\mathbb R^{n+1}$; fixing a concrete norm would prove it for that norm only. The functional $(w,-1)$ is pairing e w, and $\|(w,-1)\|_*$ is its operator norm.
• Published objects. The ball, the worst case, the empirical distribution and the Lipschitz modulus are the published definitions WassersteinDRO_Duality_ambiguitySet, _worstCaseRisk_v2, _empiricalDistribution and _lipschitzModulus. The worst case is taken in the extended reals, and expectations follow the convention of nominalRisk_v2 (no junk value for non-integrable losses). $\mathrm{lip}(L)$ takes values in $[0,\infty]$.
• Standing assumptions. $L$ is nonnegative, convex on $\mathbb R$ and Lipschitz continuous; $N\ge1$; $\rho\ge0$; $\Xi=\mathbb R^{n+1}$. The paper's $L\ge0$ (§2.1) is imposed as the standing loss-function assumption.
• Reading of "equivalent". The paper does not define the word. The goal states the per-$w$ identity that the proof establishes plus equality of optimal values. Attainment of the infimum is not claimed.
• Corrections. The printed display on p. 30 omits a factor $\frac1N$ and carries a stray $|\theta|$ in the constraint; milestone 4 states the corrected identity. The printed Lemma A.1 omits $\rho>0$, which its proof uses; the linked platform theorem has it.
• Ruled out. The goal is not a restatement of Theorem 10 with $\mathrm{Lip}(\ell_w)$ of the composite loss: its right-hand side is the explicit average of (6) with $\mathrm{lip}$ of the univariate $L$ and the dual norm of $(w,-1)$.
• Welcome contributions. The factorization $\mathrm{lip}(L\circ\beta)=\mathrm{lip}(L)\|\beta\|_*$ for a linear functional $\beta$ on a finite-dimensional normed space, conjugate calculus for univariate convex functions, and the evaluation of the worst case at $\rho=0$.

Selected references

• S. Shafieezadeh-Abadeh, D. Kuhn, P. Mohajerin Esfahani, Regularization via Mass Transportation, arXiv:1710.10016v3, 2019; J. Mach. Learn. Res. 20(103), 2019. https://arxiv.org/abs/1710.10016
• D. Kuhn, P. Mohajerin Esfahani, V. A. Nguyen, S. Shafieezadeh-Abadeh, Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning, INFORMS TutORials, 2019. https://arxiv.org/abs/1908.08729
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171, 2018. https://arxiv.org/abs/1505.05116
• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, NeurIPS, 2015. https://arxiv.org/abs/1509.09259
• J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, J. Appl. Probab. 56(3), 2019. https://arxiv.org/abs/1610.05627
• D. P. Bertsekas, Convex Optimization Theory, Athena Scientific, 2009 (cited as [9] in the paper for Propositions 5.3.1 and 5.5.4).

Motivation

Retailers in many categories accept returns of products that are not defective: a consumer buys, learns whether the product suits them, and may send it back for a refund. Returns of this kind are a large cost item in retailing, and the refund a retailer offers is an operational decision on a par with its price and its stocking quantity. Xuanming Su, Consumer Returns Policies and Supply Chain Performance (SSRN 1020451, version of August 2008; published in Manufacturing & Service Operations Management 11(4), 2009, doi:10.1287/msom.1080.0240), studies this decision first for a single seller and then in a supply chain.

This mission formalizes the supply chain part, Section 5 of the paper. A classical result of supply chain contracting is that a manufacturer can align a retailer's ordering decision with the interest of the whole chain by a buy-back contract, which pays the retailer a credit for unsold units (Cachon, Supply Chain Coordination with Contracts, 2003). Su shows that once the retailer also sets a consumer returns policy, the standard buy-back no longer coordinates, and identifies three contracts that do. The companion mission (mission 1 of this series) formalizes the single-seller results of Sections 3–4, in particular Proposition 2, which gives the supply chain optimum used here.

Setting

A consumer who buys at price $p$ learns a valuation $V$, drawn independently from a law $\nu$ with finite mean $\mu = EV$, and then either keeps the product or returns it for the refund $r$. Keeping is optimal when $V \ge r$. Write

$$\bar G(r) = \mathbb P(V \ge r), \qquad G(r) = \mathbb P(V < r),$$

for the probabilities of keeping and returning. A consumer's expected utility from buying is $E\max(V,r)$, which is therefore the reservation price: all consumers buy if $p \le E\max(V,r)$ and none buys otherwise (the demand rule (6)). Market demand $X \ge 0$ has distribution function $F$ and $\bar F = 1 - F$; a stock $q \ge 0$ sells $E\min(X,q)$ in expectation when consumers buy, and nothing when they do not. Write $S(p,q,r)$ for these expected sales. The production cost is $c$, leftover and returned units are salvaged at $s$, and $0 \le s < c < \mu$.

The total supply chain profit is

$$\Pi_T(p,q,r) = [(p-s)\bar G(r) + (p-r)G(r)]\,S(p,q,r) - (c-s)q. \tag{15}$$

A manufacturer sells to a retailer, who sets $p$, $q$ and (except in Proposition 4) $r$. The contracts are:

• standard buy-back $(w,b)$: wholesale price $w$, credit $b$ per leftover unit; the retailer earns (14);
• differentiated buy-back $(w,b,l)$: credit $b$ per unsold unit and $b-l$ per returned unit; the retailer earns

$$\Pi_R(p,q,r) = [(p-b)\bar G(r) + (p-r-l)G(r)]\,S(p,q,r) - (w-b)q; \tag{31}$$

• direct-to-manufacturer returns with a buy-back $(w,b)$: consumers return to the manufacturer, who sets $r$; the profits are (19) and (21);
• sales rebate $(w,u)$: a rebate $u$ per unit sold, returned or not; the retailer earns (25).

The supply chain optimum, from Proposition 2 of the paper, is

$$p^{SC} = E\max(V,s), \qquad \bar F(q^{SC}) = \frac{c-s}{E\max(V,s)-s}, \qquad r^{SC} = s.$$

Formalization targets

Goal: Proposition 3 (p. 16)

For $\phi \in [0,1]$ and $\bar\phi = 1-\phi$, the differentiated buy-back

$$w = \phi c + \bar\phi\,E\max(V,s), \qquad b = \phi s + \bar\phi\,E\max(V,s), \qquad b - l = s$$

makes the supply chain optimum a retailer optimum and gives the retailer the share $\phi$:

$$\Pi_R(p,q,r) \le \Pi_R(p^{SC},q^{SC},r^{SC}) \ \ \forall p, r,\ q \ge 0, \qquad \Pi_R(p^{SC},q^{SC},r^{SC}) = \phi\,\Pi_T(p^{SC},q^{SC},r^{SC}),$$

and the contract is implementable: $w \ge b$, $l \ge 0$, $b - l \ge s$.

Milestones

1. Under a standard buy-back the retailer's optimal refund is $r^* = b$ (Sec. 5.1, p. 15).
2. Under (31) the retailer's optimum is $p^* = E\max(V,b-l)$, $\bar F(q^*) = (w-b)/(E\max(V,b-l)-b)$, $r^* = b-l$ (proof of Proposition 3, p. 27).
3. Under (16)–(18), $w - b = \phi(c-s)$ and $E\max(V,b-l) - b = \phi[E\max(V,s)-s]$ ((32)–(33)).
4. At $(E\max(V,s), q, s)$ the retailer earns $\phi\,\Pi_T$ ((34)–(39)).
5. Retailer plus manufacturer profit under direct returns is $\Pi_T$ (Sec. 5.3, p. 17).
6. Proposition 4: with direct-to-manufacturer returns and the buy-back (22)–(23), the chain optimum is a Nash equilibrium between retailer and manufacturer, with retailer share $\phi$.
7. Proposition 5: the sales rebate $u = \frac{E\max(V,s)-s}{c-s}(w-c)$ makes the chain optimum a retailer optimum.
8. With a rebate paid on kept units only, the retailer's optimal refund is $r^* = s - u < s$ (Sec. 5.4, p. 19).

Significance

The results separate what a contract must observe in order to coordinate a chain with consumer returns: either the manufacturer distinguishes returned from unsold units (Propositions 3 and 4), or it observes sales (Proposition 5). The negative results (milestones 1 and 8) show why the standard buy-back and a kept-only rebate fail: each distorts the retailer's refund away from the salvage value. These statements are proved in the paper by short arguments; none of them has, to the knowledge of this mission, a machine-checked proof. Formalizing them yields a reusable model of a newsvendor with an endogenous price and refund under valuation uncertainty, and a checked account of the coordination conditions, including the boundary cases ($\phi = 0$, atoms in the valuation law) that the paper does not discuss.

Difficulty

Each result combines two optimizations, and neither is routine at the generality of the formal statements. The first is over price and refund jointly: the demand rule makes every profit discontinuous in $p$ and $r$, and the refund problem must be solved for an arbitrary valuation law, where atoms make the tie rule at $V = r$ matter. The second is a newsvendor problem in $q$ for an arbitrary demand law: the paper writes the optimal stock as $\bar F^{-1}$ of a fractile, which presumes a continuous, strictly increasing $F$, whereas here $F$ may jump or be flat and the optimal stock is any solution of the fractile equation. The obvious reduction, "the retailer's profit is $\phi\,\Pi_T$, so its maximizer is the chain's", is not available: that identity holds only at the chain's price and refund, and away from them the retailer's profit is not proportional to $\Pi_T$. In Proposition 4 the manufacturer's deviation to a refund below $s$ acts on the consumers' purchase decision, and the paper's remark that no one then buys is false when $V \ge s$ almost surely, so that case needs its own argument.

Formalization scope

Prices, refunds, costs, quantities and profits are real numbers. The valuation law $\nu$ is a probability measure on $\mathbb R$ with integrable identity (a strict generalization of the paper's density $g$); $\bar G(r) = \nu([r,\infty))$ and $G(r) = \nu((-\infty,r))$, matching the rule "keep iff $V \ge r$". The demand law $D$ is a probability measure on $\mathbb R$ with $D((-\infty,0)) = 0$, and $E\min(X,q)$ is SupplyChainTheory.expSales from the published module SupplyChainTheory_contracts. Every profit includes the demand rule (6): without it, (15) and (31) are unbounded in $p$. Optimization is over all real $p$ and $r$ and all $q \ge 0$, nonnegative stocks and demand being the paper's setting; with negative stocks the profits are unbounded. Optimality of the paper's closed-form triple is claimed, never uniqueness, and "induces the retailer to maximize supply chain profit" is stated as "the chain-optimal triple is a retailer optimum"; that the triple maximizes $\Pi_T$ is Proposition 2, formalized in mission 1, and not restated. The optimal stock is any solution of the fractile equation, and no continuity of $D$ is assumed. The Nash equilibrium of Proposition 4 is written as the two best-response inequalities. Proposition 5 adds the hypothesis $w \ge s$, implied by the paper's range $w \ge c$ (p. 19) and necessary: for $w < s$ the retailer's profit is unbounded. The kept-only rebate of Sec. 5.4 has no printed formula; its profit is (24) with the rebate removed from the returned-units term. Printed page numbers equal PDF page numbers throughout the source. A formalization in which the retailer's profit is defined as $\phi\,\Pi_T$, or in which the optimization is restricted to $r = s$, would make the goal trivial and is excluded: (31) is stated with free $w$, $b$, $l$, and the contract enters only through hypotheses.

The model module (SuReturns.Coordination.Model) restates the single-seller objects of mission 1 in this sub-namespace. Contributions welcome: proofs of the two optimization steps as reusable lemmas (the refund step for a general valuation law and the newsvendor step for an arbitrary demand law), which serve every milestone here.

Selected references

• X. Su, Consumer Returns Policies and Supply Chain Performance, SSRN working paper 1020451, version of August 2008. https://ssrn.com/abstract=1020451 ; published in Manufacturing & Service Operations Management 11(4), 2009. https://doi.org/10.1287/msom.1080.0240
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in Operations Research and Management Science, vol. 11, 2003. https://doi.org/10.1016/S0927-0507(03)11006-7
• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities (the buy-back contract), Marketing Science 4(2), 1985. https://doi.org/10.1287/mksc.4.2.166

Motivation

Financial institutions, insurers and engineers who manage the risk of a decision describe it by a statistic of the loss distribution that the decision induces. The value-at-risk (VaR) at confidence level $\beta$, the $\beta$-quantile of the loss, became an industry and regulatory standard in the 1990s, but it is not subadditive and behaves erratically as a function of the decision when the loss distribution has atoms, as it always does in scenario-based models. The conditional value-at-risk (CVaR), roughly the average of the losses beyond VaR, was proposed as a replacement that is coherent in the sense of Artzner, Delbaen, Eber and Heath and that can be optimized.

In an earlier paper (Rockafellar and Uryasev, 2000) the same authors showed, for loss distributions with continuous distribution functions, that CVaR is the minimum value of an explicit convex function of one real variable, and that VaR is a minimizer. That formula turned CVaR minimization over a portfolio into a linear program and is the reason CVaR is used in practice. The paper formalized here (Rockafellar and Uryasev, Research Report #2001-5, 2001, published in J. Banking & Finance 2002) defines CVaR for general loss distributions, discrete ones included, and proves that the minimization formula survives.

Timeline.

• 1997–1999: Artzner, Delbaen, Eber and Heath introduce coherent risk measures; VaR fails subadditivity.
• 2000: Rockafellar and Uryasev prove the minimization formula for continuous loss distributions.
• 2001–2002: the present paper, Theorem 10: the formula holds for every integrable loss once CVaR is defined as the mean of the $\beta$-tail distribution. Acerbi and Tasche (2002) give an equivalent "expected shortfall" formulation.

Setting

A decision $x$ lies in a set $X\subseteq\mathbb R^n$; an uncertain outcome $y\in\mathbb R^m$ has a Borel probability law $P$ that does not depend on $x$. The loss is $z=f(x,y)$, where $f$ is continuous in $x$ on $X$, measurable in $y$, and $E\{|f(x,y)|\}<\infty$ for each $x\in X$. A confidence level $\beta\in(0,1)$ is fixed.

• The distribution function of the loss is $\Psi(x,\alpha)=P\{y\mid f(x,y)\le\alpha\}$, with left limit $\Psi(x,\alpha^-)=P\{y\mid f(x,y)<\alpha\}$.
• The $\beta$-VaR is $\alpha_\beta(x)=\min\{\alpha\mid\Psi(x,\alpha)\ge\beta\}$ and the upper $\beta$-VaR is $\alpha^+_\beta(x)=\inf\{\alpha\mid\Psi(x,\alpha)>\beta\}$.
• The $\beta$-tail distribution is the probability measure on $\mathbb R$ with distribution function

$$\Psi_\beta(x,\alpha)=\begin{cases}0,&\alpha<\alpha_\beta(x),\\ \dfrac{\Psi(x,\alpha)-\beta}{1-\beta},&\alpha\ge\alpha_\beta(x).\end{cases}$$

• The $\beta$-CVaR $\phi_\beta(x)$ is the mean of the $\beta$-tail distribution.
• The upper $\beta$-CVaR is $\phi^+_\beta(x)=E\{f(x,y)\mid f(x,y)>\alpha_\beta(x)\}$, defined when $\Psi(x,\alpha_\beta(x))<1$, and $\lambda_\beta(x)=[\Psi(x,\alpha_\beta(x))-\beta]/[1-\beta]$.
• Finally

$$F_\beta(x,\alpha)=\alpha+\frac{1}{1-\beta}\,E\big\{[f(x,y)-\alpha]^+\big\},\qquad[t]^+=\max\{0,t\}.$$

When $\Psi(x,\cdot)$ jumps across $\beta$ at $\alpha_\beta(x)$, the tail distribution keeps only the part $\lambda_\beta(x)$ of that atom needed to give the tail total mass one: the atom is split.

Formalization targets

Goal: Theorem 10 (fundamental minimization formula)

For each $x\in X$: $F_\beta(x,\cdot)$ is finite and convex (hence continuous), and

$$\phi_\beta(x)=\min_{\alpha\in\mathbb R}F_\beta(x,\alpha),\qquad \operatorname{argmin}_\alpha F_\beta(x,\alpha)=[\alpha_\beta(x),\alpha^+_\beta(x)],$$

the minimum being attained and the argmin a nonempty closed bounded interval; in particular $\phi_\beta(x)=F_\beta(x,\alpha_\beta(x))$.

Milestones, in attack order

1. The note after Definition 3: $\Psi_\beta(x,\cdot)$ is a distribution function, so the $\beta$-tail distribution exists; its mean is finite.
2. Proposition 6: $\phi_\beta(x)=\lambda_\beta(x)\alpha_\beta(x)+[1-\lambda_\beta(x)]\phi^+_\beta(x)$ when $\Psi(x,\alpha_\beta(x))<1$, and $\phi_\beta(x)=\alpha_\beta(x)$ otherwise.
3. $F_\beta(x,\cdot)$ is finite and convex.
4. The one-sided derivatives (31): $\partial^+F_\beta/\partial\alpha=[\Psi(x,\alpha)-\beta]/(1-\beta)$ and $\partial^-F_\beta/\partial\alpha=[\Psi(x,\alpha^-)-\beta]/(1-\beta)$.
5. Bounded level sets, and $\operatorname{argmin}_\alpha F_\beta(x,\alpha)=\{\alpha\mid\Psi(x,\alpha^-)\le\beta\le\Psi(x,\alpha)\}$, a nonempty closed bounded interval.
6. The least element of that set is $\alpha_\beta(x)$ and the greatest is $\alpha^+_\beta(x)$.

A companion item states Corollary 7: $\phi_\beta(x)\ge\alpha_\beta(x)$, strictly when $\Psi(x,\alpha_\beta(x))<1$.

Significance

Theorem 10 is what makes CVaR computable and optimizable. Since $\phi_\beta(x)=\min_\alpha F_\beta(x,\alpha)$, minimizing CVaR over $x\in X$ is the joint minimization of $F_\beta(x,\alpha)$ over $(x,\alpha)$; with a finite scenario set and a loss linear in $x$, that is a linear program, and VaR comes out as a by-product. The convexity and sublinearity of CVaR in $x$ (Corollary 11), its coherence (Corollary 12) and the equivalence of CVaR-constrained and CVaR-penalized problems (Theorem 14) are all derived from it. The formula is the basis of CVaR portfolio optimization software and of a large literature on risk-averse stochastic programming.

The result has been proved since 2001 and is not open. To our knowledge it has no machine-checked proof with CVaR defined independently: the CVaR items already on Prove2Me take $\min_\alpha F_\beta$ as the definition of CVaR, which makes (28) true by definition. This mission produces a formal proof that the tail-mean definition, with its atom splitting, agrees with the minimization formula for every integrable loss, together with reusable facts about one-sided derivatives of $\alpha\mapsto E[f-\alpha]^+$ and the argmin of the Rockafellar–Uryasev function.

Difficulty

The minimization side is elementary convex analysis in one variable once the one-sided derivatives are known; computing them requires passing a limit under the expectation, with the jumps of $\Psi(x,\cdot)$ handled separately for right and left limits. The step that does not follow from that analysis is the identification of the minimum value with $\phi_\beta(x)$. When the loss has an atom at $\alpha_\beta(x)$ that straddles level $\beta$, neither $E\{f\mid f\ge\alpha_\beta(x)\}$ nor $E\{f\mid f>\alpha_\beta(x)\}$ equals the minimum value; only the mean of the distribution with the split atom does. The obvious approach, proving the formula for continuous laws and passing to a limit, does not deliver the identity at the level of the defined objects; the identity has to be proved directly from the definition of the tail distribution, through Proposition 6.

Formalization scope

• The outcome space is $\mathbb R^m$ (Fin m → ℝ) with its Borel σ-algebra and a probability measure P. The paper's support set $Y\subseteq\mathbb R^m$ is not modelled: a law on $Y$ is a law on $\mathbb R^m$ concentrated on $Y$, and no statement uses $Y$.
• Probabilities are real numbers (P.real). $\Psi(x,\alpha^-)$ is $P\{f(x,\cdot)<\alpha\}$, as the paper defines it in (2).
• $\alpha_\beta(x)$ is the published MultistageStochastic.valueAtRisk P (f x) β (a real infimum, referenced, not redefined); $\alpha^+_\beta(x)$ is a real infimum. Both are meaningful because $P$ is a probability measure and $0<\beta<1$, and those hypotheses are carried wherever they appear.
• The $\beta$-tail distribution is a probability measure on $\mathbb R$ whose distribution function is $\Psi_\beta(x,\cdot)$, chosen when one exists (it is then unique); $\phi_\beta(x)$ is its mean. Milestone 1 establishes existence and integrability.
• "Minimum" is attainment: $\phi_\beta(x)$ is the least element of the range of $F_\beta(x,\cdot)$. The argmin is the set of global minimizers. "Finite" is integrability of $[f(x,\cdot)-\alpha]^+$ for each $\alpha$.
• One-sided derivatives are derivatives within $[\alpha,\infty)$ and $(-\infty,\alpha]$. The display (31) as printed on p. 14 has $\alpha_\beta(x)$ in place of $\alpha$; the formalization follows the derivation on p. 15.
• The goal and Corollary 7 carry all standing assumptions of §2; milestones assume only what they use (integrability, measurability of the single loss $f(x,\cdot)$), which makes them stronger.

Defining CVaR as $\min_\alpha F_\beta(x,\alpha)$, or as the quantile average, or by formula (21), would make the goal or a milestone true by definition; CVaR is defined here as the mean of the $\beta$-tail distribution, and any such redefinition is ruled out.

A complete development needs: right-continuity and limits of distribution functions, dominated convergence for the difference quotients of $\alpha\mapsto E[f-\alpha]^+$, the uniqueness of a probability measure on $\mathbb R$ with given distribution function, and one-variable convex analysis linking one-sided derivatives to minimizers. The derivative and argmin lemmas are reusable for any Rockafellar–Uryasev-type objective. Proofs of any milestone, and Lean lemmas that bridge valueAtRisk (stated with ENNReal) and P.real, are welcome.

Selected references

• R. T. Rockafellar and S. Uryasev, Conditional value-at-risk for general loss distributions, Research Report #2001-5, ISE Dept., University of Florida, April 2001; published in Journal of Banking & Finance 26 (2002) 1443–1471. https://doi.org/10.1016/S0378-4266(02)00271-6
• R. T. Rockafellar and S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2 (2000) 21–41. https://doi.org/10.21314/JOR.2000.038
• P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9 (1999) 203–228. https://doi.org/10.1111/1467-9965.00068
• C. Acerbi and D. Tasche, On the coherence of expected shortfall, Journal of Banking & Finance 26 (2002) 1487–1503. https://doi.org/10.1016/S0378-4266(02)00283-2
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Interior-point methods for linear programming are usually analysed under two assumptions: a strictly feasible starting point is known, and the problem has an optimal solution. In practice neither is known in advance. The homogeneous self-dual embedding of Ye, Todd and Mizuno (Math. Oper. Res. 19(1), 1994) removes both assumptions. It embeds a standard-form linear program and its dual into one artificial program that always has an obvious interior starting point. A solution of the artificial program either yields optimal solutions of the original pair or certifies that one of them is infeasible. The embedding underlies the infeasibility detection of several interior-point LP and conic solvers.

The paper's main result is an $O(\sqrt n L)$ iteration bound. Section 4, "Analysis of the output", asks a different, practical question: what can be read off the iterates if the algorithm is stopped early, at an approximate solution? Theorem 8 answers it. This mission formalizes Theorem 8 and the results its proof uses.

Setting

Let $A\in\mathbb R^{m\times n}$, $b\in\mathbb R^m$, $c\in\mathbb R^n$. The primal and dual programs are

$$\text{(LP)}\ \min\{c^Tx : Ax=b,\ x\ge0\},\qquad \text{(LD)}\ \max\{b^Ty : A^Ty\le c\},$$

with dual slack $s=c-A^Ty$. An optimal solution pair is an optimal $\bar x$ of (LP) together with an optimal $(\bar y,\bar s)$ of (LD).

Write $e$ for the all-ones vector and set $\bar b=b-Ae$, $\bar c=c-e$, $\bar z=c^Te+1$. The homogeneous self-dual program (HLP), in the paper's normalization $y^0=0$, $x^0=s^0=e$, has variables $(y,x,\tau,\theta,s,\kappa)$ with $y\in\mathbb R^m$, $x,s\in\mathbb R^n$, $\tau,\theta,\kappa\in\mathbb R$:

$$\begin{array}{rl} \min & (n+1)\theta\\ \text{s.t.} & Ax-b\tau+\bar b\theta=0,\\ & s=-A^Ty+c\tau-\bar c\theta\ \ge0,\\ & \kappa=b^Ty-c^Tx+\bar z\theta\ \ge0,\\ & -\bar b^Ty+\bar c^Tx-\bar z\tau=-(n+1),\qquad x\ge0,\ \tau\ge0. \end{array}$$

$\mathcal F_h$ is its feasible set and $\mathcal F_h^0$ the subset with $x,\tau,s,\kappa>0$. A self-complementary solution is an optimal solution of (HLP). A strictly self-complementary one also has $\theta=0$ and $(x+s;\tau+\kappa)>0$. For a point of (HLP) put $\mu=(x^Ts+\tau\kappa)/(n+1)$, and for $\beta\in(0,1)$ let

$$\mathcal N(\beta)=\Bigl\{z\in\mathcal F_h^0 : \Bigl\|\begin{pmatrix}Xs\\ \tau\kappa\end{pmatrix}-\mu e\Bigr\|_2\le\beta\mu\Bigr\}.$$

The predictor–corrector algorithm with $\beta=1/4$ starts at $z^0=(0,e,1,1,e,1)$. At even $k$ (predictor step) it solves the Newton system (11)–(12) with target $\gamma\mu^k=0$ and moves along the direction by the largest step that stays in $\mathcal N(2\beta)$ (13). At odd $k$ (corrector step) it solves the system with target $\mu^k$ and takes a full step.

Formalization targets

Goal: Theorem 8 (p. 63)

For every predictor–corrector sequence $(y^k,x^k,\tau^k,\theta^k,s^k,\kappa^k)$:

1. if (LP) possesses an optimal solution, then for every optimal pair $\bar x,(\bar y,\bar s)$

$$\tau^k\ge\frac{1-2\beta}{e^T\bar x+e^T\bar s+1}\quad\text{for all }k;$$

2. otherwise there is a fixed $\varepsilon>0$, independent of $k$, with

$$\kappa^k\ge\frac{(1-2\beta)\varepsilon}{n+1},\qquad \frac{1-2\beta}{2(n+1)}\le\frac{1-2\beta}{\kappa^k}\le\frac{\tau^k}{\theta^k}\le\frac{1+2\beta}{\kappa^k}\le\frac{(n+1)(1+2\beta)}{(1-2\beta)\varepsilon}$$

for all $k$.

Milestones

In the order the proof uses them:

• the predictor-step and corrector-step claims from the proof of Theorem 6 (p. 62);
• the iterates lie in $\mathcal N(2\beta)$ (p. 63);
• Theorem 2 (iv): the optimal value of (HLP) is $0$ and $(n+1)\theta=x^Ts+\tau\kappa$ on $\mathcal F_h$ (stated for general $x^0,s^0>0$, $y^0$);
• equation (9): $e^Tx+e^Ts+\tau+\kappa-(n+1)\theta=n+1$;
• an optimal pair scaled by $\alpha=(n+1)/(e^T\bar x+e^T\bar s+1)$ is a self-complementary solution;
• the orthogonality identity $(x^k)^Ts^*+(s^k)^Tx^*+\kappa^k\tau^*=(n+1)\theta^k$;
• Theorem 2 (v), existence of a strictly self-complementary solution;
• Theorem 3 (i) and (ii), reading such a solution back into (LP) and (LD);
• the bound $\kappa^k\le(n+1)+(n+1)\theta^k\le2(n+1)$.

Significance

Theorem 8 is a stopping criterion. Either $\tau^k$ stays bounded away from zero, which happens exactly when (LP) has an optimal solution, or $\tau^k$ and $\theta^k$ go to zero at the same rate while $\kappa^k$ stays bounded away from zero. An implementation can therefore watch $\tau^k/\theta^k$ and $\kappa^k$ and decide the status of (LP) from an approximate iterate, without the exact rounding procedure needed for the $O(\sqrt nL)$ bound. The bounds hold for real data, with no integrality and no bit length.

Theorem 8 has a published proof on one page, building on the self-duality facts of §2 and the Mizuno–Todd–Ye step analysis. None of it is machine-checked. A complete development would give a verified account of the homogeneous self-dual embedding, including:

• the skew-symmetric orthogonality argument;
• Goldman–Tucker strict complementarity for (HLP);
• the predictor–corrector neighborhood invariants.

These are the ingredients of every analysis of the embedding. Homogeneous self-dual programs appear on Prove2Me in other conventions (Vanderbei's (22.4) and (22.21), Matoušek's (SD)), but their statements concern different programs: no artificial variable $\theta$, no normalizing row. They do not formalize any statement here.

Difficulty

The two branches of Theorem 8 rest on facts of different depth.

• The first branch needs only an optimal pair of (LP)/(LD), lifted into (HLP), and the identity $(x^k)^Ts^*+(s^k)^Tx^*+\kappa^k\tau^*=(n+1)\theta^k$.
• The "otherwise" branch needs an optimal solution of (HLP) with $\kappa^*>0$. Its existence is not elementary. It comes from strict complementarity (Theorem 2 (v)) together with the characterization of Theorem 3 (i). Strict complementarity for linear programs is the Goldman–Tucker theorem, which Mathlib does not contain.
• The neighborhood invariants behind "the sequence is in $\mathcal N(2\beta)$" are the Mizuno–Todd–Ye estimates. They need the orthogonality $d_x^Td_s+d_\tau d_\kappa=0$ of the Newton directions and a careful quadratic bound on $\|D_xd_s\|$.

The obvious first idea is to treat Theorem 8 as a consequence of Theorem 6. It fails: Theorem 8 is about every iterate of an infinite run and uses no iteration count. The constant $\varepsilon$ depends on the instance and is not explicit.

Formalization scope

• Data. Real data A : Matrix (Fin m) (Fin n) ℝ, b : Fin m → ℝ, c : Fin n → ℝ, with no rank assumption and no integrality. (LP)/(LD) feasibility and optimality are built on the published general-form LP definition LinearOptimization_DualLP. "(LP) has a solution (feasible and bounded)" in Theorem 3 is read as "(LP) has an optimal solution".
• Points. A point of (HLP) is a structure with fields y x τ θ s κ. The slacks $s,\kappa$ are pinned to the constraint expressions. (HLP) is defined for general $(x^0,y^0,s^0)$; the instance (7) is obtained by substitution. Optimality means minimizing the objective over $\mathcal F_h$, not "$\theta=0$", so Theorem 2 (iv) is not built into the definition.
• Norm. The norm in $\mathcal N(\beta)$ is the Euclidean norm on $\mathbb R^{n+1}$, written out explicitly.
• Constants. $\beta=1/4$ is a named constant. The statements show $1-2\beta$ and $1+2\beta$ as printed.
• The iteration. It is a relation IsPCSequence: $z^0=(0,e,1,1,e,1)$, and each step is $z^{k+1}=z^k+\alpha d$ for some solution $d$ of (11)–(12). The relation is needed because $d_y$ is not unique when $A$ is rank-deficient.
• Step size. The predictor step size must be the greatest element of the set in (13), as printed. On an instance where that maximum is not attained, no predictor–corrector sequence exists and Theorem 8 holds vacuously there. A sorry-free check shows that $z^0\in\mathcal N(1/4)$ for all data, so the sequence does start.
• The two branches. They are two implications with complementary hypotheses, "(LP) has an optimal solution" and its negation. The negation covers infeasible and unbounded (LP) alike.
• Quantifiers. The first branch quantifies over all optimal pairs. In the second, $\exists\varepsilon>0$ precedes $\forall k$.
• Divisions. The chain keeps the printed divisions. All denominators ($\kappa^k$, $\theta^k=\mu^k$) are positive on $\mathcal N(2\beta)$, so Lean's $x/0=0$ convention plays no role.
• Ruled out. A formalization in which $\varepsilon$ may depend on $k$, or in which the first branch asserts the bound for only some optimal pair, would make Theorem 8 trivial or weaker. Both are excluded.

Needed infrastructure: LP duality and Goldman–Tucker strict complementarity for real standard-form programs, and the skew-symmetric orthogonality lemma. These are reusable well beyond this mission. Proofs of any milestone, and alternative arguments (e.g. via the central-path limit) for the existence of $\kappa^*>0$, are welcome.

Selected references

• Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt nL)$-Iteration Homogeneous and Self-Dual Linear Programming Algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. https://doi.org/10.1287/moor.19.1.53
• S. Mizuno, M. J. Todd, Y. Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Mathematics of Operations Research 18(4), 964–981, 1993. https://doi.org/10.1287/moor.18.4.964
• O. Güler, Y. Ye, Convergence behavior of interior-point algorithms, Mathematical Programming 60, 215–228, 1993. https://doi.org/10.1007/BF01580610
• A. J. Goldman, A. W. Tucker, Theory of linear programming, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, 53–97, 1956. https://doi.org/10.1515/9781400881987-005