Optimization

Completed

Convex Optimization·Captain: mikedeng1

Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming 2: One Aggressive Stepsize Policy Drives the AG Gradient Mapping to Zero on Nonconvex Composite ProblemsResearch Paper

Motivation

Many problems in statistics, signal processing and machine learning have the form "smooth loss plus simple non-smooth term": a differentiable data-fit term together with a constraint set or a sparsity-inducing penalty such as the $\ell_1$ norm. When the loss is convex, Nesterov's accelerated gradient (AG) method and its proximal variants are known to be optimal among first-order methods: after $N$ iterations the optimality gap is $O(L/N^2)$ , against $O(L/N)$ for plain proximal gradient (Nesterov 1983, reference [24] of the paper; Beck & Teboulle 2009). When the loss is nonconvex, the classical accelerated schemes come with no convergence guarantee at all, and practitioners must choose between a method that is fast on convex problems and one that is guaranteed to make progress on nonconvex ones.

Ghadimi and Lan (arXiv:1310.3787v1, 2013; Math. Program. 156, 2016) proposed a single AG scheme that does both. This mission formalizes their result for composite problems (§2.2, Theorem 2), where the smooth part is split into a possibly nonconvex piece with Lipschitz constant $L_f$ and a convex piece, and a non-smooth convex term is handled through a proximal step. The theorem shows that one aggressive step-size policy, the one that is optimal in the convex case, still drives a stationarity measure to zero when the smooth part is nonconvex.

Setting

Work in $\mathbb R^n$ with the Euclidean norm. The problem (1.3) is

\min_{x\in\mathbb R^n}\ \Phi(x):=\Psi(x)+\mathcal X(x),\qquad \Psi=f+h,

where:

$f:\mathbb R^n\to\mathbb R$ is differentiable with $L_f$ -Lipschitz gradient and may be nonconvex;
$h:\mathbb R^n\to\mathbb R$ is convex and differentiable with $L_h$ -Lipschitz gradient, so $\Psi$ has $L_\Psi$ -Lipschitz gradient with $L_\Psi=L_f+L_h$ ;
$\mathcal X$ is a convex, possibly non-smooth function with bounded domain $K=\{u:\mathcal X(u)<+\infty\}$ , for instance the indicator of a convex compact set, or that indicator plus $\|\cdot\|_1$ .

The prox map (2.37) is

\mathcal P(x,y,c)=\operatorname*{argmin}_{u\in\mathbb R^n}\Big\{\langle y,u\rangle+\frac1{2c}\|u-x\|^2+\mathcal X(u)\Big\},\qquad c>0,

and the gradient mapping (2.38) is $\mathcal G(x,y,c)=\frac1c[x-\mathcal P(x,y,c)]$ . With $y=\nabla\Psi(x)$ it reduces to $\nabla\Psi(x)$ when $\mathcal X\equiv0$ , and a small $\|\mathcal G\|$ certifies approximate stationarity of (1.3). Assumption 2 asks for a constant $M$ with $\|\mathcal P(x,y,c)\|\le M$ for all $x,y$ and $c>0$ ; it holds whenever $\mathcal X$ is proper, closed, convex with bounded domain (Lemma 2).

Algorithm 2 takes step sizes with $\alpha_1=1$ , $\alpha_k\in(0,1)$ for $k\ge2$ , $\beta_k>0$ , $\lambda_k>0$ , starts from $x_0=x^{ag}_0$ , and for $k\ge1$ sets

x^{md}_k=(1-\alpha_k)x^{ag}_{k-1}+\alpha_kx_{k-1},\quad x_k=\mathcal P\big(x_{k-1},\nabla\Psi(x^{md}_k),\lambda_k\big),\quad x^{ag}_k=\mathcal P\big(x^{md}_k,\nabla\Psi(x^{md}_k),\beta_k\big).

The weights are $\Gamma_1=1$ , $\Gamma_k=(1-\alpha_k)\Gamma_{k-1}$ (2.6).

Formalization targets

Goal: Theorem 2 (p. 11)

Fix $N\ge1$ and assume, for $k=1,\dots,N$ ,

\alpha_k\lambda_k\le\beta_k<\frac1{L_\Psi}\ \ (2.9),\qquad \frac{\alpha_1}{\lambda_1\Gamma_1}\ge\frac{\alpha_2}{\lambda_2\Gamma_2}\ge\cdots\ \ (2.10).

Let $x^*$ be an optimal solution of (1.3). Then

\min_{k=1,\dots,N}\big\|\mathcal G(x^{md}_k,\nabla\Psi(x^{md}_k),\beta_k)\big\|^2\le2\Big[\sum_{k=1}^N\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)\Big]^{-1}\Big[\frac{\|x_0-x^*\|^2}{2\lambda_1}+\frac{L_f}{\Gamma_N}\big(\|x^*\|^2+2M^2\big)\Big],\tag{2.44}

and, if $L_f=0$ ,

\Phi(x^{ag}_N)-\Phi(x^*)\le\frac{\Gamma_N\|x_0-x^*\|^2}{2\lambda_1}.\tag{2.45}

The goal is stated for general step sizes, so it does not hard-code the constants of a particular policy; Corollary 2 (the policy $\alpha_k=2/(k+1)$ , $\beta_k=1/(2L_\Psi)$ , $\lambda_k=k\beta_k/2$ ) is a specialization left for follow-up work.

Milestones

In the order of the proof: Lemma 1 (unrolling a $\Gamma_k$ -weighted recursion) and (2.16); the identity (2.42) linking $\mathcal G$ to $x^{md}_k-x^{ag}_k$ ; Lemma 5, the two-sided bound $-\frac{L_f}2\|y-x\|^2\le\Psi(y)-\Psi(x)-\langle\nabla\Psi(x),y-x\rangle\le\frac{L_\Psi}2\|y-x\|^2$ ; the descent bound (2.46) (already proved on the platform); the one-step inequalities (2.47)–(2.51); the summed inequality after (2.51); and the bounds (2.52)–(2.53).

Significance

The result. Theorem 2 gives a uniform treatment of convex and nonconvex composite problems. The same step sizes yield the optimal $O(L_\Psi\|x_0-x^*\|^2/N^2)$ optimality gap when $f$ is affine, and a bound on the gradient mapping when $f$ is nonconvex. Under Corollary 2's policy that bound gives an iteration count of $O(L_\Psi^{2/3}/\epsilon^{1/3}+L_\Psi L_f/\epsilon)$ for $\|\mathcal G\|^2\le\epsilon$ , which depends on the Lipschitz constant $L_h$ of the convex part more mildly than projected gradient does. The proof template (a weighted Lyapunov argument in which the nonconvexity appears only through $L_f$ ) recurs in later stochastic and variance-reduced accelerated methods, including the paper's own Theorem 4.

Formalizing it. The result has been proved and refereed since 2016. As far as is known it has not been formalized in any proof assistant, and the platform holds no accelerated method with a nonconvex guarantee. A complete development would give a machine-checked proximal three-point inequality for convex functions on a convex domain, a checked composite AG analysis, and a checked version of Lemma 5. These are reusable pieces for any accelerated proximal method.

Difficulty

The obvious route is to copy the convex analysis of accelerated methods. It breaks at the convexity step: the bound $\Psi(x^{md}_k)\le(1-\alpha_k)\Psi(x^{ag}_{k-1})+\alpha_k\Psi(x)+\dots$ needs convexity of $\Psi$ , which is now available only up to $L_f$ -quadratic errors. Those errors involve $\|x^{md}_k-x\|$ and $\|x^{ag}_{k-1}-x_{k-1}\|$ , which do not telescope and are not controlled by the usual potential; without some a priori bound on the iterates they can grow with $N$ . A formal proof also has to track the extended-valued $\mathcal X$ carefully, since its convexity is used only at points of its domain, and the first iteration, where $x^{ag}_0=x_0$ is not a prox output.

Formalization scope

Space. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Smoothness of $f$ and $h$ is the platform's ConvexOptAlg.SmoothGD.IsBetaSmooth (differentiable with an explicit gradient map, Lipschitz gradient, nonnegative constant). $\Psi$ and $\nabla\Psi$ are written as $f+h$ and $\nabla f+\nabla h$ .
The convex term. $\mathcal X$ is represented by its domain K and its finite values X : E n → ℝ on K, with ConvexOn ℝ K X. Points outside K never enter: $\Phi$ is compared only on K, $x^*$ is optimal over K, and (2.48)–(2.51) quantify over $x\in K$ . A real-valued $\mathcal X$ on all of $\mathbb R^n$ is ruled out, because Assumption 2 is then unsatisfiable ( $\mathcal P(x,y,c)\to x$ as $c\to0$ ) and the goal would hold vacuously.
The prox map is a function P x y c with the hypothesis IsProxMap K X P: for every $c>0$ , P x y c ∈ K and it minimizes the prox objective over K. Without this minimizer hypothesis the three-point inequalities and the goal are false, so it cannot be dropped.
Indexing is 1-based as in the paper. $\Gamma_k=\prod_{i=2}^k(1-\alpha_i)$ , so $\Gamma_1=1$ . The minimum in (2.44) is Finset.inf' over $\{1,\dots,N\}$ . Conditions (2.9)–(2.10) are imposed for $k=1,\dots,N$ , and $\beta_k<1/L_\Psi$ is written $L_\Psi\beta_k<1$ .
One added hypothesis, $\|x_0\|\le M$ . The paper uses it silently in (2.52) at $k=1$ ; it holds whenever $x_0\in\operatorname{dom}\mathcal X$ .
A typo is corrected. (2.53) prints $\|x_0-x\|^2$ after substituting $x=x^*$ ; the Lean states $\|x_0-x^*\|^2$ .

Contributions welcome: proofs of any milestone. The three-point inequality (2.48)–(2.49) and Lemma 5 are self-contained and reusable. Also welcome: a proof of Lemma 2 (bounded domain implies Assumption 2), and Corollary 2 as a follow-up statement.

Selected references

S. Ghadimi, G. Lan, Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming, arXiv:1310.3787v1, 2013; Math. Program. 156 (2016) 59–99. https://arxiv.org/abs/1310.3787v1 · https://doi.org/10.1007/s10107-015-0871-8
A. Beck, M. Teboulle, A Fast Iterative Shrinkage-Thresholding Algorithm for Linear Inverse Problems, SIAM J. Imaging Sci. 2 (2009) 183–202. https://doi.org/10.1137/080716542
S. Ghadimi, G. Lan, H. Zhang, Mini-batch stochastic approximation methods for nonconvex stochastic composite optimization, Math. Program. 155 (2016) 267–305 (reference [13] of the paper: the projected-gradient bound compared against). https://doi.org/10.1007/s10107-014-0846-1
S. Ghadimi, G. Lan, Optimal stochastic approximation algorithms for strongly convex stochastic composite optimization, I: a generic algorithmic framework, SIAM J. Optim. 22 (2012) 1469–1492 (reference [11] of the paper; its Lemma 2 is the three-point inequality (2.48)–(2.49)). https://doi.org/10.1137/110848864

17 thms3 active usersReviewed

Completed

Machine Learning·Captain: mikedeng1

Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition I: Gradient Descent with Step 1/L Satisfies f(x_k) − f* ≤ (1 − μ/L)^k (f(x_0) − f*)Research Paper

Motivation

Gradient descent is often introduced with strong convexity as the condition that gives a geometric reduction in objective error. That condition excludes useful smooth objectives whose minimizer is not unique and some nonconvex objectives. Karimi, Nutini, and Schmidt place the Polyak–Łojasiewicz inequality at the center of a more general account: it controls the objective gap using the squared gradient norm without requiring convexity. Their paper uses it to analyze gradient, coordinate, stochastic, and proximal gradient methods, and identifies settings including least squares and logistic regression in which the condition is useful. Karimi, Nutini, and Schmidt, §1–2

This mission isolates the paper's first rate theorem and its immediate analytic setting. The question is whether the ordinary gradient step with length $1/L$ has a global geometric rate when the objective has a Lipschitz gradient, attains its minimum, and satisfies the PL inequality. The claim applies to every initial point, even when the function is nonconvex. It also gives a precise test case for deciding which properties of smoothness and optimality must be represented explicitly in Lean. Karimi, Nutini, and Schmidt, Theorem 1, p. 2

Setting

Let $d$ be a natural number and let $f:\mathbb R^d\to\mathbb R$ be a differentiable objective. Its gradient at $x$ is $\nabla f(x)$ , with the Euclidean norm and inner product denoted by $\|\cdot\|$ and $\langle\cdot,\cdot\rangle$ . An $L$ -Lipschitz gradient means that $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for every $x,y$ , with $L>0$ . The corresponding quadratic upper bound is the paper's inequality (2):

f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac L2\|y-x\|^2.

The optimization problem is unconstrained. It has a nonempty set of solutions: choose a global minimizer $x^*$ , so $f(x^*)\le f(y)$ for every $y$ , and write $f^*=f(x^*)$ . This notation ties the reference value to an attained optimum. The PL inequality with constant $\mu>0$ is

\frac12\|\nabla f(x)\|^2\ge\mu\bigl(f(x)-f^*\bigr) \qquad\text{for every }x\in\mathbb R^d.

Given any starting point $x_0$ , the gradient descent run is the sequence specified by $x_{k+1}=x_k-L^{-1}\nabla f(x_k)$ . The term “linear convergence” here refers to a geometric bound on the difference in objective values, not to a claim that the points $x_k$ approach a particular minimizer. Multiple minimizers are allowed. These conventions are those of §2 and Theorem 1 of the source. Karimi, Nutini, and Schmidt, p. 2

Formalization targets

Gradient descent at step size $1/L$

The mission goal is the paper's Theorem 1. For every starting point and every $k\in\mathbb N$ ,

f(x_k)-f^*\le\left(1-\frac\mu L\right)^k\bigl(f(x_0)-f^*\bigr).

The target includes the gradient update itself. Its three milestones record the source's analytic path: the quadratic upper bound (2) from the Lipschitz gradient assumption, the one-step decrease displayed in the proof, and the one-step PL contraction displayed immediately afterwards. The latter two are linked to proved platform theorems whose exact-gradient specializations give the source's displays. Karimi, Nutini, and Schmidt, Theorem 1 and proof, p. 2

Nearby consequences

The mission also states the paper's observation that an exact line search over all real step sizes has the same function-value rate. Two companion claims record that a stationary point under PL is a global minimizer, and that $\mu$ -strong convexity implies PL with the same $\mu$ . These claims locate the rate theorem among the conditions discussed in §2.2 and Appendix B; they are separate from the goal and its milestone list. Karimi, Nutini, and Schmidt, pp. 3, 14

Significance

The rate bounds the objective error at each finite iteration, with an explicit factor $1-\mu/L$ . It explains why uniqueness of the minimizer and convexity are not prerequisites for this particular function-value guarantee. It does not by itself assert a rate for the distance to the solution set, a rate for individual iterates, or convergence to a uniquely determined point. The strong-convexity companion shows that the classical strongly convex case fits inside the same PL framework. Karimi, Nutini, and Schmidt, §§2–2.2 and Appendix B

For formalization, the mission adds the precise bridge from a literal Lipschitz-gradient hypothesis to the quadratic upper-bound form used by the existing step results. It also states the complete source theorem with an attained optimum, a genuine gradient, and the update rule, rather than treating any reference value or gradient-like map as interchangeable with those objects. The two published one-step theorems are already machine checked on Prove2Me; the five source-specific draft statements in this proposal remain targets until their proofs are supplied and verified. This distinction matters because the previously published geometric-rate theorem assumes $\mu\le L$ , while Theorem 1 does not state that restriction.

Difficulty

Smoothness controls the change in $f$ during a gradient step through the size of the gradient. A geometric rate needs the change to be related to the remaining objective gap. That relation does not follow from smoothness alone; the PL inequality supplies the additional control. Another issue is that the factor $1-\mu/L$ may be negative if $\mu>L$ . The source does not exclude that parameter range, so the formal theorem must handle it without inserting an extra hypothesis. An exact line search raises a distinct issue: its asserted minimum along a line must be attained, and the chosen next iterate must be a point realizing it. Karimi, Nutini, and Schmidt, Theorem 1 and following paragraph, pp. 2–3

Formalization scope

Lean represents $\mathbb R^d$ as EuclideanSpace ℝ (Fin d), so $d=0$ is included and denotes a one-point space. It uses Mathlib's gradient on an explicitly differentiable $f$ , ordinary real scalars and norms, and a sequence indexed by natural numbers. The fixed step is written with $1/L$ and requires $L>0$ . The minimizer witness $x^*$ and its global-minimality property are explicit; the PL predicate uses exactly $f(x^*)$ as its reference value. The PL inequality is represented in the equivalent form $2\mu(f(x)-f(x^*))\le\|\nabla f(x)\|^2$ . The goal assumes the literal Lipschitz bound on gradients; equation (2) is a milestone conclusion. No convexity and no condition $\mu\le L$ are added.

The exact line-search companion quantifies over every real step size and requires an attained minimizing iterate. The stationary-point consequence retains differentiability but does not need the $L$ -Lipschitz gradient bound. The strong-convexity companion uses the first inequality in Appendix A and the implication in Appendix B, with the same $\mu$ on both sides. The shared ShiOptRates predicates for the quadratic upper bound and PL inequality are referenced as published definitions. Useful contributions include proofs of the Lipschitz-to-quadratic-bound bridge and the paper-specific results, as well as reusable facts about gradients on Euclidean spaces. A freely chosen $f^*$ or a default value of gradient at a nondifferentiable point would change the mathematical claim; the goal excludes both.

Selected references

H. Karimi, J. Nutini, and M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD, 2016; arXiv:1608.04636v4. This mission cites the pinned preprint's pp. 2–3, 11, and 14.

5 thms3 active usersReviewed

Completed

Machine Learning Operations Research Probability·Captain: mikedeng1

Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming 1: The Randomized Stochastic Gradient Method Has (1/L)E‖∇f(x_R)‖² ≤ (D_f² + σ²Σγ_k²)/Σ(2γ_k − Lγ_k²)Research Paper

Motivation

Stochastic gradient methods are the standard tool for minimizing an objective that can only be accessed through noisy gradient samples. Training a machine-learning model on sampled data, simulation-based optimization, and stochastic programs with endogenous uncertainty are all of this kind. In many of these applications the objective is nonconvex: the loss or the regularizer of a learning problem may be nonconvex, as may the expected cost of a simulation model.

Before 2013 the complexity theory of stochastic approximation (SA) was essentially a convex theory. Robbins and Monro (1951) introduced the method. Polyak and Juditsky (1992) and Nemirovski, Juditsky, Lan and Shapiro (2009) established optimal rates for convex problems, and Lan (2012) unified the smooth, nonsmooth and stochastic convex cases. None of these results covered nonconvex objectives. Ghadimi and Lan (2013) gave the first non-asymptotic complexity bound for a stochastic gradient method on a smooth nonconvex problem. The bound is stated for the expected squared gradient norm at a randomly chosen iterate, and it is the result this mission formalizes.

Setting

The problem is

f^*=\inf_{x\in\mathbb R^n} f(x),

where $f:\mathbb R^n\to\mathbb R$ is differentiable and bounded below, and its gradient is $L$ -Lipschitz: $\|\nabla f(y)-\nabla f(x)\|\le L\|y-x\|$ for all $x,y$ . This class is written $\mathcal C^{1,1}_L(\mathbb R^n)$ . The function need not be convex.

The gradient is accessible only through a stochastic first-order oracle: at the $k$ -th query point $x_k$ it returns $G(x_k,\xi_k)$ , where $\xi_1,\xi_2,\dots$ are random variables and $G$ is a Borel function. Assumption A1 asks that for every $k\ge1$ , conditionally on the past, $G(x_k,\xi_k)$ is an unbiased estimate of $\nabla f(x_k)$ , and that its error $\delta_k=G(x_k,\xi_k)-\nabla f(x_k)$ has second moment $\mathbb E\|\delta_k\|^2\le\sigma^2$ . The noise variables need not be independent of each other or of the iterates.

The randomized stochastic gradient (RSG) method takes an initial point $x_1$ , an iteration limit $N$ , stepsizes $\gamma_k$ and a probability mass function $P_R$ on $\{1,\dots,N\}$ . It draws a random index $R\sim P_R$ , runs

x_{k+1}=x_k-\gamma_k\,G(x_k,\xi_k),\qquad k=1,\dots,R,

and outputs $x_R$ . The mass function used in the main theorem is

P_R(k)=\frac{2\gamma_k-L\gamma_k^2}{\sum_{j=1}^N(2\gamma_j-L\gamma_j^2)},\qquad k=1,\dots,N.

The constants are $D_f=[2(f(x_1)-f^*)/L]^{1/2}$ and, in the convex case with minimizer $x^*$ , $D_X=\|x_1-x^*\|$ .

Formalization targets

Goal: Theorem 2.1 a)

If $0<\gamma_k<2/L$ for $k=1,\dots,N$ , $N\ge1$ , and $R$ has the mass function above, then under Assumption A1

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

where the expectation is over $R$ and the noise. Any stepsize sequence below $2/L$ is allowed, so the goal does not fix a step rule, and the step rules of the paper's corollaries follow from it.

Milestones

The quadratic bound (1.6): $|f(y)-f(x)-\langle\nabla f(x),y-x\rangle|\le\frac L2\|y-x\|^2$ (already proved on the platform).
The one-step inequality (2.8) and its pathwise sum (2.9).
The conditional mean-zero property (2.10), $\mathbb E[\langle\nabla f(x_k),\delta_k\rangle\mid\xi_{[k-1]}]=0$ .
The averaged bound (2.11), $\sum_k(\gamma_k-\frac L2\gamma_k^2)\,\mathbb E\|\nabla f(x_k)\|^2\le f(x_1)-f^*+\frac{L\sigma^2}{2}\sum_k\gamma_k^2$ .
The weighting identity: $\mathbb E\|\nabla f(x_R)\|^2$ equals the $P_R$ -weighted average of $\mathbb E\|\nabla f(x_k)\|^2$ .
For the convex companion: co-coercivity (1.8) (already proved on the platform) and its consequence (2.12), $\frac1L\|\nabla f(y)\|^2\le\langle\nabla f(y),y-x^*\rangle$ when $\nabla f(x^*)=0$ .

Companion statements

Theorem 2.1 b) bounds $\mathbb E[f(x_R)-f^*]$ by $(D_X^2+\sigma^2\sum\gamma_k^2)/\sum(2\gamma_k-L\gamma_k^2)$ when $f$ is convex with a minimizer. Corollary 2.2 specializes both bounds to the stepsizes $\gamma_k=\min\{1/L,\tilde D/(\sigma\sqrt N)\}$ :

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

and the analogous bound with $D_X$ for $\mathbb E[f(x_R)-f^*]$ in the convex case.

Significance

Theorem 2.1 a) is the basic guarantee for stochastic gradient descent on smooth nonconvex objectives. With the stepsizes of Corollary 2.2 it shows that $O(\sigma^2/\epsilon^2)$ oracle calls suffice to reach $\mathbb E\|\nabla f(x_R)\|^2\le\epsilon$ . The paper builds two further methods on it: a two-phase variant with large-deviation guarantees, and a zeroth-order variant (RSGF) that uses Gaussian smoothing when only function values are available. Later analyses of variance-reduced and adaptive stochastic methods for nonconvex problems measure their improvements against this bound.

The result is proved on paper; no machine-checked proof of it is known. A formalized fixed-step bound of the form "some iterate among the first $K$ has small expected squared gradient" exists, but it is a different statement: it has no randomized output and no general stepsizes. A complete formalization would check the measure-theoretic content that the paper treats informally: integrability of the iterates' gradients, the conditional-expectation step under dependent noise, and the role of the independence of $R$ .

Difficulty

The algebra of (2.8)–(2.9) is routine. The difficulty is in the probability. The noise may depend on the past, so the cross term $\langle\nabla f(x_k),\delta_k\rangle$ vanishes only in conditional expectation, and only once $x_k$ is known to be measurable with respect to the past. Its integrability is not assumed anywhere: $\nabla f(x_k)$ must be shown to have a finite second moment from the recursion, the Lipschitz gradient and Assumption A1. The randomized output adds a second step, where $\mathbb E\|\nabla f(x_R)\|^2$ is rewritten as a weighted average. This needs $R$ independent of the noise, and $\|\nabla f(x_k)\|^2$ has to be exhibited as a measurable function of the noise sequence. A proof that replaces $x_R$ by the deterministic weighted average skips exactly this step.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). $f\in\mathcal C^{1,1}_L$ is the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth f g L, with the gradient given as a map $g$ . $f^*$ is the greatest lower bound of the range of $f$ , not an arbitrary lower bound.
Indices are 1-based. The iterates satisfy $x_1$ given and $x_{k+1}=x_k-\gamma_kG(x_k,\xi_k)$ for $k\ge1$ , pointwise on the sample space. The noise takes values in a general measurable space.
Assumption A1 is stated along the trajectory and in conditional form, with respect to any filtration to which the noise is adapted. The paper's history filtration $\sigma(\xi_1,\dots,\xi_k)$ is one admissible choice. Every conditional expectation and every integral in a hypothesis comes with an integrability clause. Every bounded expectation in a conclusion comes with an integrability conjunct.
The output index $R$ is a measurable random variable with values in $\{1,\dots,N\}$ and law $P_R$ . It is assumed independent of the whole noise sequence; the paper leaves this implicit (Step 0 draws $R$ before any oracle call).
Added hypotheses, all implicit on the page: $L>0$ ; $\gamma_k>0$ ; independence of $R$ . In Corollary 2.2 the stepsize (2.13) is read as $\gamma_k=1/L$ when $\sigma=0$ , the paper's convention $\tilde D/0=+\infty$ , because Lean's $\tilde D/0=0$ would otherwise give $\gamma_k=0$ .
The goal concerns the integral of $\|\nabla f(x_{R(\omega)}(\omega))\|^2$ over the sample space. A statement about the weighted sum of $\mathbb E\|\nabla f(x_k)\|^2$ with $R$ removed, or one that drops the integrability conjunct, would trivialize the randomized output and does not formalize the goal.
Infrastructure: measurability of the iterates as functions of the noise, the pull-out property of conditional expectation for inner products, and a second-moment induction along the recursion. These are reusable for the paper's two-phase and zeroth-order methods and for other stochastic-approximation analyses. Proofs of any milestone, or of the integrability lemmas on their own, are welcome.

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 (cited version). https://arxiv.org/abs/1309.5549
H. Robbins and S. Monro, A stochastic approximation method, Ann. Math. Statist. 22(3), 400–407, 1951. https://doi.org/10.1214/aoms/1177729586
B. T. Polyak and A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM J. Control Optim. 30(4), 838–855, 1992. https://doi.org/10.1137/0330046
A. Nemirovski, A. Juditsky, G. Lan and A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19(4), 1574–1609, 2009. https://doi.org/10.1137/070704277
G. Lan, An optimal method for stochastic composite optimization, Math. Program. 133, 365–397, 2012. https://doi.org/10.1007/s10107-010-0434-y
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

13 thms3 active usersReviewed

Machine Learning Operations Research Probability·Captain: mikedeng1

Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming 2: The Randomized Stochastic Gradient-Free Method with Gaussian Smoothing Bounds (1/L)E‖∇f(x_R)‖² for Nonconvex fResearch Paper

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

18 thms3 active usersReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

A game-theoretic approach to computation offloading in mobile cloud computing I: The Offloading GNEP Has a SolutionResearch Paper

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

$F(x)_u=\nabla_{x_u}\lambda_uR_u(x)$ wherever both denominators are positive (p. 11).
For fixed $x_{-u}$ , user $u$ 's feasible set is convex and its cost is convex on it (p. 11).
Every solution of $\mathrm{VI}(K,F)$ is a solution of the GNEP (proof of Proposition 1).
$F$ is continuous on $K$ , and $K$ is compact and convex (proof of Proposition 1).
$\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

8 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

A game-theoretic approach to computation offloading in mobile cloud computing II: The VI Map of the Offloading GNEP Is Monotone When the Cloudlet Is Not OverloadedResearch Paper

Motivation

Mobile devices run applications whose computational demand often exceeds what a battery-powered processor can serve with acceptable delay. Computation offloading sends part of the work elsewhere: to a cloudlet, a small cluster of servers one wireless hop away, or to a distant cloud reached through the wide-area network. When many users share one cloudlet, each user's response time depends on how much the others offload, and selfish users interact strategically. Cardellini, De Nitto Personé, Di Valerio, Facchinei, Grassi, Lo Presti and Piccialli (Math. Program., 2016) model this interaction as a generalized Nash equilibrium problem (GNEP): every user minimises its own expected cost, and all users share a coupling constraint that caps the cloudlet's utilisation.

The paper computes equilibria through a variational inequality (VI) reformulation and, for distributed computation, through an extended game with a price player. The convergence of the methods it relies on (proximal-point and best-response schemes for monotone VIs, see Facchinei and Pang, 2003) requires the VI map to be monotone. This mission formalizes the paper's Theorem 1, which gives an explicit, checkable condition on the model's parameters under which that map is monotone.

Setting

There are $N$ users $u=1,\dots,N$ . Each user splits its task stream over three tiers $I=\{m,\mathit{clet},\mathit{cloud}\}$ (own device, cloudlet, cloud) and chooses fractions $x_u=(x_{u,m},x_{u,clet},x_{u,cloud})$ ; a strategy profile is $x\in\mathbb R^{3N}$ . The data are positive rates combined into $\alpha_u,\beta_u,\gamma_u,\delta_u$ (the traffic intensities a user generates on its device, the wireless link, the cloud path and the cloudlet), power parameters $P_{u,m},P_{u,t},P_{u,\max}$ , the number $n$ of cloudlet servers, the offloadable fraction $\chi\in(0,1]$ and the utilisation cap $U_{\max}$ .

The cloudlet load is $\frac1n\sum_v\delta_vx_{v,clet}$ and $D(x)=1-\frac1n\sum_t\delta_tx_{t,clet}$ . User $u$ 's private feasible set $\tilde K_u$ consists of the $x_u\ge0$ with $\sum_{i}x_{u,i}=1$ , $x_{u,clet}+x_{u,cloud}\le\chi$ and the power budget $\alpha_uP_{u,m}x_{u,m}+\beta_uP_{u,t}(x_{u,clet}+x_{u,cloud})\le P_{u,\max}$ . The shared constraint is $\Omega=\{x:\frac1n\sum_u\delta_ux_{u,clet}\le U_{\max}\}$ , and the joint feasible set is $K=(\prod_u\tilde K_u)\cap\Omega$ . User $u$ minimises

\lambda_uR_u(x)=\frac{\alpha_ux_{u,m}}{1-\alpha_ux_{u,m}}+\beta_ux_{u,clet}+\gamma_ux_{u,cloud}+\frac{\delta_ux_{u,clet}}{D(x)}.

Assumption A requires $U_{\max}$ and all $\alpha_u,\delta_u$ to lie in $(0,1)$ .

The VI map $F:\mathbb R^{3N}\to\mathbb R^{3N}$ stacks each user's gradient in its own variables:

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,clet}}{D(x)^2},\ \gamma_u\Big).

$F$ is monotone on $K$ if $(F(y)-F(x))^\top(y-x)\ge0$ for all $x,y\in K$ . Finally $\delta_{\max}=\max_u\delta_u$ .

Formalization targets

Goal: Theorem 1

Under Assumption A, if

\delta_{\max}\le\frac{n}{N\chi}(1-U_{\max}),\tag{18}

then $F$ is monotone on $K$ . The condition involves only the data of the game, so the goal is the paper's statement with no constant changed.

Milestones

The milestones follow the paper's argument in order.

A map whose Jacobian is positive semidefinite on a convex set is monotone there (p. 12, citing Facchinei–Pang).
The Jacobian $JF(x)$ has the sparse structure (16), with nonzero entries $A_u$ , $B_u$ , $B_{uv}$ given by (17).
On $K$ , $JF(x)$ is positive semidefinite as soon as the symmetric part $B^s=\frac12(B^\top+B)$ of its clet block is.
The identity (20): $B^s=\frac1{nD^2}\big(\delta\delta^\top\circ(I+E+\frac1{nD}(x^\delta_{clet}e^\top+e(x^\delta_{clet})^\top))\big)$ , with $\circ$ the Hadamard product, $E$ the all-ones matrix and $x^\delta_{clet}=(\delta_ux_{u,clet})_u$ .
The Schur product theorem (a published platform theorem).
The characteristic polynomial (21) of $ve^\top+ev^\top$ , namely $\eta^{N-2}(\eta^2-2(e^\top v)\eta+(e^\top v)^2-N\|v\|^2)$ .
The sufficient condition (22): $\frac1{nD}(\sqrt N\|x^\delta_{clet}\|-e^\top x^\delta_{clet})\le1$ implies $B^s\succeq0$ .
The bound (23) on $K$ : $\frac1{nD}(\sqrt N\|x^\delta_{clet}\|-e^\top x^\delta_{clet})\le\frac1{nD}\delta_{\max}\chi\sqrt N(\sqrt N-1)\le\frac{\delta_{\max}}{1-U_{\max}}\frac{N\chi}{n}$ .

Significance

Theorem 1 is the hypothesis under which the rest of the paper operates. The extended game of §5.2 inherits the monotonicity properties of $F$ (p. 14), and the distributed solution methods of §6 are designed for that monotone setting. Condition (18) translates monotonicity into a statement about the system: the largest per-user cloudlet traffic intensity must stay below a threshold that grows with the number $n$ of servers and shrinks with $N$ , $\chi$ and $U_{\max}$ . Remark 1 (p. 14) stresses that (18) is only sufficient.

The result is proved in the paper; this mission produces a machine-checked proof. On the way it yields statements reusable outside this model: the Jacobian criterion for monotonicity of a differentiable map on a convex set, and the spectrum of the symmetric rank-two matrix $ve^\top+ev^\top$ . None of these statements is on the platform; the Schur product theorem, which the proof also uses, is referenced as a published platform theorem.

Difficulty

The Jacobian $JF(x)$ is not symmetric: $B_{uv}$ carries the row user's own term $\frac2n\delta_ux_{u,clet}$ , so $B_{uv}\ne B_{vu}$ in general, and the eigenvalues of $JF(x)$ say nothing directly about its quadratic form. The quadratic form must be controlled uniformly over the whole feasible set $K$ , whose shape (simplices cut by the cap $\chi$ , the power budgets and the shared constraint) enters the final bound, and the condition must come out in the paper's exact constants. In Lean, the main costs are the coordinatewise Fréchet derivative of $F$ on $\mathbb R^{3N}$ , the characteristic polynomial of a rank-two matrix of arbitrary size, and the passage from a characteristic polynomial to positive semidefiniteness.

Formalization scope

Users are Fin N (0-based); tiers are a three-element type Tier; a profile is Fin N → Tier → ℝ. The inner product on $\mathbb R^{3N}$ is written out as $\sum_u\sum_i a_{u,i}b_{u,i}$ , and the norm on $\mathbb R^N$ in (21)–(23) is the Euclidean norm written as $\sqrt{\sum_uv_u^2}$ , because Mathlib's norm on function types is the sup norm. $F$ is defined by the closed form of p. 11, not as a derivative, so milestone 2 has content. $\delta_{\max}$ is the real supremum of the $\delta_u$ , which is the maximum for $N\ge1$ .

Standing hypotheses carried by every statement: Assumption A, $n\ge1$ and $0<\chi\le1$ . Disclosed choices relative to the page:

(21) is stated for an arbitrary $v\in\mathbb R^N$ and assumes $N\ge2$ , so that $\eta^{N-2}$ is a polynomial;
(22) is stated at any profile with $D>0$ ;
(20) is stated at any profile with $D\ne0$ ;
the derivative (16)–(17) is stated on the open region $\alpha_ux_{u,m}<1$ , $\frac1n\sum_t\delta_tx_{t,clet}<1$ , which contains $K$ ;
in milestone 1, differentiability is required at each point of the convex set (in a full neighbourhood).

The formulas for $F$ , $A_u$ , $B_u$ and $B_{uv}$ divide by $1-\alpha_ux_{u,m}$ and $D$ , and Lean sets $a/0=0$ . Every statement is therefore restricted to $K$ or to a region where these denominators are nonzero; monotonicity on the larger set $\prod_u\tilde K_u$ , where $D$ can vanish, is a different and false-by-junk claim and is not posed. $K$ is nonempty for admissible data (e.g. all users computing locally), so the goal is not vacuous.

Contributions welcome: proofs of any milestone, especially the generic ones (1 and 6), which belong in a general library.

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, J.-S. Pang, Finite-Dimensional Variational Inequalities and Complementarity Problems, vols. I–II, Springer, 2003 (the paper's [17]). https://doi.org/10.1007/b97543
F. Facchinei, C. Kanzow, Generalized Nash equilibrium problems, Annals of Operations Research 175 (2010), 177–211 (the paper's [16]). https://doi.org/10.1007/s10479-009-0653-x
R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, 1990 (the paper's [24]; Schur product theorem, Theorem 7.5.3). https://doi.org/10.1017/CBO9780511810817
D. S. Bernstein, Matrix Mathematics: Theory, Facts, and Formulas with Application to Linear Systems Theory, Princeton University Press, 2005 (the paper's [6]; Fact 4.9.16). https://press.princeton.edu/books/hardcover/9780691118024

10 thms3 active usersReviewed

Completed

Algorithmic Game Theory·Captain: mikedeng1

On the Complexity of Nash Equilibria and Other Fixed Points 4: The Fixed Points of the Division-Free Map G_I(x)ij = max(x_ij + u_i((i:j); x−i) − t_i, 0) Are Exactly the Nash EquilibriaResearch Paper

Motivation

Nash's existence theorem for finite games is a fixed-point theorem: one writes down a continuous map from the set of mixed strategy profiles to itself whose fixed points are exactly the Nash equilibria, and applies Brouwer's theorem. Nash's own map (Nash 1951) divides by $1+\sum_j \max(0,\cdot)$ , and the choice of map matters as soon as the question is computational rather than existential.

Etessami and Yannakakis (SIAM J. Comput. 39 (2010)) introduce the class FIXP of fixed-point search problems whose maps are given by algebraic circuits over $\{+,-,*,/,\max,\min\}$ and rational constants, and show that computing a Nash equilibrium of a 3-player game is FIXP-complete. In Section 4 they ask which gates are really needed. Since the Nash problem is complete, it suffices to find, for every game, a map with the same fixed points and a cheaper circuit. They define a division-free map $G_I$ , prove that its fixed points are precisely the Nash equilibria (Lemma 20), show that it is computed by a circuit with gates $\{+,-,*,\max,\min\}$ (Lemma 21), and conclude that FIXP is unchanged if circuits use only $\{+,*,\max\}$ and rational constants (Theorem 22). The same map, defined as a Euclidean projection, appears earlier in Gul, Pearce and Stacchetti (1993).

This mission formalizes the game-theoretic content of that section: the map $G_I$ , its well-definedness, and Lemma 20.

Setting

A finite game $I$ has a finite set of players $i$ ; each player has a finite, nonempty set $S_i$ of pure strategies, and a payoff function $u_i$ assigns a real number to every pure strategy profile. A mixed strategy of player $i$ is a vector $(x_{ij})_{j\in S_i}$ with $x_{ij}\ge0$ and $\sum_{j}x_{ij}=1$ ; a mixed profile $x$ is one mixed strategy per player, and $\Delta$ denotes the set of mixed profiles (the product of the players' unit simplices). The expected payoff $u_i(x)$ is the expectation of $u_i$ when the players draw their strategies independently according to $x$ . For $j\in S_i$ , $u_i((i{:}j);x_{-i})$ is player $i$ 's expected payoff when $i$ plays $j$ and the others play according to $x$ . A Nash equilibrium is a mixed profile $x$ such that no player can raise $u_i(x)$ by switching unilaterally to another mixed strategy.

For a vector $x$ indexed by pairs $(i,j)$ , let $v(x)_{ij}=u_i((i{:}j);x_{-i})$ and $h(x)=x+v(x)$ . For each player $i$ define the function of a real variable

f_{i,x}(t)=\sum_{j\in S_i}\max\bigl(h_{ij}(x)-t,\,0\bigr).

It is continuous, nonincreasing, strictly decreasing below $\max_j h_{ij}(x)$ and zero above it, so there is a unique threshold $t_i$ with $f_{i,x}(t_i)=1$ . The division-free map is

G_I(x)_{ij}=\max\bigl(h_{ij}(x)-t_i,\,0\bigr).

In the Lean development, $v(x)_{ij}$ is DGPNash.NashMap.purePayoff u x i j, $h$ is hVal, $f_{i,x}$ is fSum, $t_i$ is threshold and $G_I$ is G, all in the namespace FixpNash.DivFree.

Formalization targets

Goal: Lemma 20 (p. 47)

For every finite game with nonempty strategy sets and every $x\in\Delta$ ,

G_I(x)=x\iff x\text{ is a Nash equilibrium of }I.

Milestones, in the order the proof uses them

The threshold is well defined (p. 47): for every real $x$ and every player with $S_i\neq\emptyset$ , $f_{i,x}(t)=1$ has exactly one solution, and it is $t_i$ .
$G_I$ maps into $\Delta$ (p. 47): $\sum_{j\in S_i}G_I(x)_{ij}=1$ for every $i$ , so $G_I(x)\in\Delta$ .
Pure deviations suffice (p. 11): $x$ is a Nash equilibrium iff $x\in\Delta$ and $u_i((i{:}j);x_{-i})\le u_i(x)$ for all $i$ and $j\in S_i$ .
Fixed points equalize the support (proof of Lemma 20, p. 47): if $x\in\Delta$ and $G_I(x)=x$ , then $u_i((i{:}j);x_{-i})=t_i$ when $x_{ij}>0$ and $u_i((i{:}j);x_{-i})\le t_i$ when $x_{ij}=0$ .
At an equilibrium the threshold is the payoff (proof of Lemma 20, p. 47): if $x$ is a Nash equilibrium then $t_i=u_i(x)$ for every $i$ .
Closed form of the threshold (proof of Lemma 21, p. 48): if $z_{i1}\ge\dots\ge z_{in_i}$ is $h_i(x)$ sorted in decreasing order, then

t_i=\max\Bigl\{\tfrac1l\Bigl(\sum_{j=1}^{l}z_{ij}-1\Bigr):l=1,\dots,n_i\Bigr\}.

This last milestone is off the goal's path; it is the formula behind the division-free circuit.

Significance

Lemma 20, with Brouwer's theorem and the continuity of $G_I$ , gives an elementary proof of Nash's theorem. With Lemma 21 it shows that the Nash equilibrium problem, and therefore every FIXP problem, is represented by circuits without division; the paper uses this to obtain Theorem 22. The pure-deviation criterion of milestone 3 is the standard test for equilibria and is used throughout equilibrium computation. The closed form of milestone 6 is the threshold of the Euclidean projection onto the simplex, used widely in optimization.

All of these results are proved in the paper. The mission produces machine-checked versions. No platform item states Lemma 20 or the pure-deviation criterion for AGT.IsMixedNash. Related posed items, with other conventions, are credited below rather than reused: the thresholds of the simplex projection in the Condat 2015 series (SimplexProj.Condat.simplex_projection_threshold, threshold_root_bracket, subsequence_mean_le_threshold, stated for the projection on $\mathbb R^N$ with a radius), and the best-response fixed-point characterization in supermodular games (Supermodularity.Games.equilibrium_iff_fixed_point_v2, a different map). The paper also remarks, without proof, that $G_I(x)$ is the point of $\Delta$ closest to $h(x)$ . That remark is not a target here.

Difficulty

The map $G_I$ is defined through an implicitly determined threshold. In the formalization the threshold has to be a definition that does not depend on a proof, and every statement about it rests on the existence and uniqueness of the root of $f_{i,x}(t)=1$ . This is an intermediate-value argument for a piecewise linear function of a finite sum of $\max$ terms. Its strict monotonicity holds only below $\max_j h_{ij}(x)$ , and the argument must use that $S_i$ is nonempty.

The equivalence itself needs the multilinearity of the expected payoff: $u_i(x)=\sum_j x_{ij}\,u_i((i{:}j);x_{-i})$ and, more generally, the payoff of a deviation to a mixed strategy $y_i$ is $\sum_j y_{ij}\,u_i((i{:}j);x_{-i})$ . In the agt_games representation the expected payoff is a sum over all pure profiles of products of probabilities, so this identity must be extracted from the product structure rather than read off.

Formalization scope

The game uses the published agt_games vocabulary: players form a finite type ι with decidable equality, the strategies of player i a finite type S i, payoffs are real (the paper's are rational, so this is a generalization), mixed profiles are real weight functions satisfying AGT.IsMixedProfile, and Nash equilibrium is AGT.IsMixedNash (no profitable deviation to any lottery). The pure-strategy payoff $u_i((i{:}j);x_{-i})$ is the published DGPNash.NashMap.purePayoff.

The following readings are explicit in the Lean and implicit on the page:

every strategy set is nonempty (∀ i, Nonempty (S i)). The paper assumes this tacitly; without it $\Delta$ is empty and $t_i$ does not exist;
the threshold is defined as $t_i=\inf\{t: f_{i,x}(t)\le1\}$ . Milestone 1 proves that this is the paper's "unique value of $t$ where $f_{i,x}(t_i)=1$ ". A formalization in which $t_i$ is a free parameter, or is set to $u_i(x)$ , would make Lemma 20 nearly definitional. That is ruled out: $G_I$ is defined from the game alone, and $t_i$ is the root of $f_{i,x}(t)=1$ ;
$h$ , $f_{i,x}$ , $t_i$ and $G_I$ are given by the same formulas for every real vector $x$ . Milestones 1, 2 and 6 hold in that generality, while the goal and milestones 4–5 are stated on $\Delta$ , as on the page;
"fixed point of $G_I$ " means a point $x\in\Delta$ with $G_I(x)=x$ ;
"it is sufficient to check switches to pure strategies only" becomes an equivalence between AGT.IsMixedNash and the pure-deviation inequalities for a mixed profile;
in milestone 6, the sorted order is a bijection $e$ from $\{0,\dots,n\}$ onto $S_i$ along which $h_{i,e(l)}(x)$ is nonincreasing, so $n_i=n+1$ and the paper's index $l$ is $l+1$ .

Contributions welcome: proofs of any milestone. The multilinearity of AGT.expectedPayoff in one player's strategy, and the existence and uniqueness of the threshold of a finite sum of hinge functions, are reusable beyond this mission.

Selected references

K. Etessami and M. Yannakakis, On the complexity of Nash equilibria and other fixed points, SIAM J. Comput. 39(6) (2010) 2531–2597; author manuscript, Section 4, pp. 47–48. https://doi.org/10.1137/080720826
J. Nash, Non-cooperative games, Annals of Mathematics 54 (1951) 286–295. https://doi.org/10.2307/1969529
F. Gul, D. Pearce and E. Stacchetti, A bound on the proportion of pure strategy equilibria in generic games, Mathematics of Operations Research 18(3) (1993) 548–552. https://doi.org/10.1287/moor.18.3.548
L. Condat, Fast projection onto the simplex and the ℓ1 ball, Mathematical Programming 158 (2016) 575–585. https://doi.org/10.1007/s10107-015-0946-6

10 thms3 active usersReviewed

Completed

Algorithmic Game Theory·Captain: mikedeng1

On the Complexity of Nash Equilibria and Other Fixed Points 1: ε-Nash Equilibria Are Weak (n+1)ε-Fixed Points of Nash's Function, and Weak ε²/(4c²n³)-Fixed Points Are ε-Nash EquilibriaResearch Paper

Motivation

Nash proved that every finite game has an equilibrium by exhibiting a continuous map of the set of mixed profiles into itself whose fixed points are exactly the equilibria, and applying Brouwer's fixed point theorem (Nash, 1951). Computationally, the same map is the bridge between games and fixed-point problems: complexity classes for total search problems such as PPAD (Papadimitriou, 1994) and FIXP (Etessami and Yannakakis, 2010) are defined through fixed points, and a game problem is placed in such a class by passing through Nash's map.

For three or more players, equilibria can be irrational, so algorithms produce approximations. Two different notions compete. An $\varepsilon$ -Nash equilibrium is a profile at which no player can gain more than $\varepsilon$ by deviating unilaterally; a weak $\varepsilon'$ -approximate fixed point of Nash's map is a profile that the map moves by less than $\varepsilon'$ in every coordinate. Proposition 3 of Etessami and Yannakakis shows that the two notions are interchangeable up to polynomially related tolerances. Since weak approximate fixed points of polynomially continuous, polynomially computable maps can be found in PPAD (their Proposition 2), this gives the membership of $\varepsilon$ -Nash equilibria in PPAD, first observed by Daskalakis, Goldberg and Papadimitriou (2009) and by Papadimitriou (1994).

Setting

A finite game $\Gamma$ in normal form has a finite set of players; each player $i$ has a finite nonempty set $S_i$ of pure strategies and a payoff function $u_i$ on the pure strategy profiles $S=\prod_i S_i$ . A mixed profile $x$ assigns to each player $i$ a probability vector $x_i=(x_{i,j})_{j\in S_i}$ ; $D_\Gamma$ is the set of mixed profiles. The expected payoff of player $i$ is $u_i(x)$ , and $u_i((i{:}j);x_{-i})$ is the expected payoff of $i$ when $i$ plays the pure strategy $j$ and every other player keeps its mixed strategy. The gain of switching to $j$ is

g_{i,j}(x)=u_i((i{:}j);x_{-i})-u_i(x).

Nash's function $F_\Gamma:D_\Gamma\to D_\Gamma$ is

F_\Gamma(x)_{(i,j)}=\frac{x_{i,j}+\max\{0,g_{i,j}(x)\}}{1+\sum_{l\in S_i}\max\{0,g_{i,l}(x)\}}.

A profile $x$ is an $\varepsilon$ -NE if $u_i(x)\ge u_i(y_i;x_{-i})-\varepsilon$ for every player $i$ and every mixed strategy $y_i$ of $i$ . A weak $\varepsilon'$ -approximate fixed point is an $x\in D_\Gamma$ with $|F_\Gamma(x)-x|_\infty<\varepsilon'$ .

The proof uses three constants of the game: $n=\max_i|S_i|$ , the maximum number of pure strategies of a player; $M$ , the maximum over players $i$ of $\max_s u_i(s)-\min_s u_i(s)$ ; and $c=1+M$ .

Formalization targets

Goal: Proposition 3 in explicit form

For every $\varepsilon'>0$ , every $\varepsilon'/(n+1)$ -NE $x$ is a weak $\varepsilon'$ -approximate fixed point of $F_\Gamma$ :

|F_\Gamma(x)_{(i,j)}-x_{i,j}|<\varepsilon'\quad\text{for all } i,j.

For every $0<\varepsilon\le1$ , every weak $\varepsilon'$ -approximate fixed point with

\varepsilon'=\frac{\varepsilon^2}{4c^2n^3}

is an $\varepsilon$ -NE.

Milestones

(p. 12) $x$ is an $\varepsilon$ -NE iff $x$ is a mixed profile and $g_{i,j}(x)\le\varepsilon$ for all $i,j$ : pure deviations suffice.
(p. 20) the first direction, as its own statement.
(p. 21) for a mixed profile, $\sum_{j}x_{i,j}g_{i,j}(x)=0$ ; split by sign, $\sum x_{i,j}\varphi_{i,j}(x)=\sum x_{i,j}\psi_{i,j}(x)$ with $\varphi_{i,j}=\max\{0,g_{i,j}\}$ and $\psi_{i,j}=-g_{i,j}$ where $g_{i,j}\le 0$ .
(p. 21) at a weak $\varepsilon'$ -approximate fixed point, $|\varphi_{i,j}(x)-x_{i,j}\sum_l\varphi_{i,l}(x)|<\varepsilon'(1+\sum_l\varphi_{i,l}(x))<\varepsilon^2/(2cn^2)$ .
(p. 21) the first case of the final argument: if some $j$ with $g_{i,j}(x)<0$ has $x_{i,j}\ge\varepsilon/(2cn^2)$ , then $\sum_l\varphi_{i,l}(x)<\varepsilon$ .

Significance

The result says that the "almost at equilibrium" notion of approximation and the "almost fixed" notion attached to Nash's map are the same notion up to polynomial changes of tolerance. It is the reason the weak approximation problem for Nash's function inherits PPAD membership from Proposition 2 and conversely why PPAD-hardness of $\varepsilon$ -NE transfers to weak approximation. The paper contrasts it with strong approximation (being close to an actual equilibrium), which it shows to be much harder; the explicit tolerances make precise which of the two notions a fixed-point algorithm for Nash's map actually delivers.

The result is proved in the paper. To our knowledge neither direction is formalized. On Prove2Me, the Daskalakis–Goldberg–Papadimitriou series contains the analogous Lemma 3.8 (DGPNash.NashMap.approx_fixed_point_is_approx_nash, posed) and its inequality (3) (DGPNash.NashMap.eq_3, posed): they concern the same map, but for games with a common strategy set Fin n, nonnegative payoffs and a different error term, so they are credited rather than reused. This mission states both directions for arbitrary finite strategy families with the paper's own constants.

Difficulty

Neither direction needs advanced mathematics; the difficulty is in the second direction. The obvious reading, that a profile moved little by $F_\Gamma$ has small gains, fails as stated: the approximate fixed-point condition controls $\varphi_{i,j}-x_{i,j}\sum_l\varphi_{i,l}$ , the gain of a strategy relative to the player's total positive gain weighted by $x_{i,j}$ , not the gain $\varphi_{i,j}$ itself. A strategy that carries most of the probability and most of the positive gain can be almost fixed while its gain is large, so the bound on each $\varphi_{i,j}$ has to come from information that the coordinatewise condition alone does not contain, with the exact constants $\varepsilon/(2cn^2)$ and $1/(2n)$ of the paper tracked throughout; the paper's argument is compact and leaves several of these estimates implicit. In Lean, the multilinearity of the expected payoff in a single player's mixed strategy, which underlies both the reduction to pure deviations and the zero-average identity, has to be derived from the product-form definition of the expected payoff.

Formalization scope

Games, mixed profiles and expected payoffs are those of the published agt_games bundle: players form a finite type ι, player i has a finite strategy type S i, payoffs are real (u : ι → (∀ i, S i) → ℝ; the paper's payoffs are rational for computational reasons only). $u_i((i{:}j);x_{-i})$ is the published DGPNash.NashMap.purePayoff, and the $\varepsilon$ -NE is the published DGPNash.WellSupported.IsEpsApproxNash, which includes that $x$ is a mixed profile. New definitions: gain, nashFunction (by the printed formula, the sum over all of $S_i$ ), IsWeakApproxFixedPoint (a mixed profile with every coordinate of $F_\Gamma(x)-x$ of absolute value $<\varepsilon'$ ), and the constants maxNumStrategies ( $n$ ), payoffSpread ( $M$ ) and cConst ( $c$ ), all computed from the game.

Explicit readings of the paper's text:

"P-time equivalent" is formalized by the two explicit implications of the proof; no statement about algorithms or encoding sizes is made.
The first direction concludes, as the page does, that $x$ is a weak $\varepsilon'$ -approximate fixed point (strict, as defined on p. 16). The computation on p. 20 prints the looser bound " $\le(m_i+1)\epsilon\le\epsilon'$ "; the strict bound holds with the same printed $\varepsilon=\varepsilon'/(n+1)$ .
"Assume without loss of generality that $\epsilon\le1$ " becomes the hypothesis $\varepsilon\le1$ of the second direction.
The sums $\sum_{l=1}^{m_i}$ of pp. 12 and 20–21 run over all of $S_i$ ; $m_i$ is the paper's $n_i=|S_i|$ .
$\epsilon^2/2cn^2$ and $\epsilon/2cn^2$ are read as $\varepsilon^2/(2cn^2)$ and $\varepsilon/(2cn^2)$ .
"One of the strategies $j$ on the rhs" is a strategy with $g_{i,j}(x)<0$ .
The goal assumes every $S_i$ nonempty, as every game with a mixed profile has.

The constants $n$ , $M$ , $c$ are definitions computed from the game, not free parameters: a formalization that lets them be chosen (for instance a large $c$ in the second direction, or $n=0$ so that $\varepsilon^2/(4c^2n^3)$ becomes $0$ ) would trivialize the statement and is ruled out. Contributions of reusable lemmas are welcome, in particular the linearity of AGT.expectedPayoff in one player's mixed strategy and the bound $|g_{i,j}(x)|\le M$ , which are useful to every game-theoretic mission built on agt_games.

Selected references

K. Etessami and M. Yannakakis, On the complexity of Nash equilibria and other fixed points, SIAM J. Comput. 39(6) (2010) 2531–2597 (author manuscript used here). https://doi.org/10.1137/080720826
J. Nash, Non-cooperative games, Annals of Mathematics 54(2) (1951) 286–295. https://doi.org/10.2307/1969529
C. Daskalakis, P. W. Goldberg and C. H. Papadimitriou, The complexity of computing a Nash equilibrium, SIAM J. Comput. 39(1) (2009) 195–259. https://doi.org/10.1137/070699652
C. H. Papadimitriou, On the complexity of the parity argument and other inefficient proofs of existence, J. Comput. System Sci. 48(3) (1994) 498–532. https://doi.org/10.1016/S0022-0000(05)80063-7

11 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Statistics·Captain: mikedeng1

Bootstrap Robust Prescriptive Analytics 2: The Entropic Robust Nadaraya-Watson Budget Equals inf{α : ν log Σ D·exp((L−α)w/ν) + rν ≤ 0}Research Paper

Motivation

Data-driven decision making with side information ("prescriptive analytics") chooses a decision $z$ after observing a context $x = x_0$ , using a training set of past pairs $(x, y)$ . A common recipe estimates the conditional expected cost $\mathbb E[L(z, y) \mid x = x_0]$ with a local learning method, such as Nadaraya–Watson kernel regression or nearest neighbours, and then minimizes the estimate over $z$ (Ban and Rudin 2019; Bertsimas and Kallus 2020). Such estimate-then-optimize decisions are known to be optimistically biased: the minimized estimate tends to understate the cost that the decision incurs on new data.

Bertsimas and Van Parys (arXiv:1711.09974v2) robustify these formulations against distributions near the empirical one, measured by a relative-entropy bootstrap distance. They show that this choice protects the decision against disappointment on resampled (bootstrap) data at an exponential rate. A robust formulation is only usable if it can be computed. This mission concerns the paper's computational result for the Nadaraya–Watson case: the robust budget, a supremum over a set of distributions, equals a two-variable convex dual program.

Setting

The training data have finitely many distinct points, the support $\Omega_n$ . A distribution on $\Omega_n$ is a vector $D = (D_i)_{i \in \Omega_n}$ with $D_i \ge 0$ and $\sum_i D_i = 1$ ; their set is $\mathcal D_n$ . Fix a context $x_0$ and a decision $\bar z$ . Each support point $i = (\bar x_i, \bar y_i)$ carries a weight $w_i = w_n(\bar x_i, x_0) > 0$ and a loss $\ell_i = L(\bar z, \bar y_i)$ .

The Nadaraya–Watson estimate at $D$ (equation (19)) is the weighted average

E^n_D[\ell] = \frac{\sum_i w_i\,\ell_i\,D_i}{\sum_i w_i\,D_i}.

The bootstrap distance (Definition 6, equation (27)) is the relative entropy

B(D', D) = \sum_i D'_i \log\frac{D'_i}{D_i},

with $0\log 0 = 0$ and $B(D', D) = +\infty$ when $D'$ puts mass on a point where $D$ vanishes. For a reference distribution $D$ and a radius $r$ , the bootstrap robust Nadaraya–Watson budget (equation (24) with $R = B$ and $k(n) = n$ ) is

c_n(\bar z, D, x_0) = \sup\big\{ E^n_{D'}[\ell] : D' \in \mathcal D_n,\ B(D', D) \le r \big\}.

For the nearest-neighbours variant, nested neighbourhoods $N^0 \subseteq N^1 \subseteq \dots \subseteq N^n = \Omega_n$ define a partial robust budget $c^j_n$ (equation (25)), with two extra linear constraints tying the mass of $N^j$ and $N^{j-1}$ to $k/n$ and $(k-1)/n$ .

Formalization targets

Goal: Lemma 2

For every $D \in \mathcal D_n$ and every radius $r \in \mathbb R$ ,

c_n(\bar z, D, x_0) = \inf\Big\{\alpha \in \mathbb R :\ \exists\,\nu > 0,\ \ \nu\log\Big(\sum_i \exp\Big(\frac{(\ell_i - \alpha)\,w_i}{\nu}\Big) D_i\Big) + r\,\nu \le 0\Big\}.

No hypothesis on $r$ is imposed. For $r < 0$ both sides are $-\infty$ , and for $r = 0$ both equal $E^n_D[\ell]$ .

Milestones

The milestones follow the proof in Appendices B.3 and B.8:

The estimate $E^n_D[\ell]$ is the maximum of a linear program in $(s, P)$ with the single feasible point $P = sD$ (B.3).
Corollary 1: for any distance $R$ , $c_n$ equals the perspective program $\sup_{s > 0, P} \sum_i w_i \ell_i P_i$ subject to $s\,R(P/s, D) \le s\,r$ , $\sum_i P_i = s$ and $\sum_i w_i P_i = 1$ .
The Fenchel step: $\sup_{\lambda \ge 0}(\lambda b - \nu\lambda\log\lambda) = \nu e^{b/\nu - 1}$ .
Strong duality for $r > 0$ : the program of Corollary 1 with $R = B$ equals $\inf\{\alpha : \exists \beta, \nu > 0,\ r\nu + \nu\sum_i D_i e^{((\ell_i - \alpha)w_i + \beta)/\nu - 1} \le \beta\}$ .
Elimination of $\beta$ : such a $\beta$ exists if and only if $\nu \log \sum_i e^{(\ell_i-\alpha)w_i/\nu} D_i + r\nu \le 0$ .
Lemma 1 (companion): the analogous dual (32) of the partial nearest-neighbours budget, assuming Slater's condition $\inf\{B(D', D) : D' \in \mathcal D^j_n\} < r$ .

Significance

The robust budget is a supremum over a $|\Omega_n|$ -dimensional set of distributions, and the decision minimizes it over $\bar z$ , which is a min–max problem. Lemma 2 replaces the inner supremum by an infimum over two scalars $(\alpha, \nu)$ , so the robust prescription becomes a single minimization over $(\bar z, \alpha, \nu)$ . When $L$ is convex in $\bar z$ , that minimization is an exponential-cone program. The paper's numerical section (§5) solves its robust formulations in exactly this form. Lemma 1 plays the same role for the nearest-neighbours formulation, with one dual program per neighbourhood.

The results are proved in the paper (Appendices B.3, B.7, B.8) by a Lagrangian computation. As far as we know, none of them has been machine-checked. A formalization adds three things. It handles reference distributions $D$ with zeros, which the page's computation divides by. It covers the full range of radii, including $r \le 0$ , where Slater's condition fails. And it records the corrected sign of the minimizing multiplier $\beta^\star$ . The linear-objective special case without the ratio and with a strictly positive reference, $\max\{v^\top p : D(p\|q) \le \beta\} = \inf_{\lambda > 0} \lambda \log \sum_j q_j e^{v_j/\lambda} + \beta\lambda$ , is already proved on the platform (Nilim–El Ghaoui, RobustMDP.EntropyInner.kl_ball_inner_problem_dual, with its multiplier elimination RobustMDP.EntropyInner.mu_elimination). Both are included as supporting references.

Difficulty

The obvious route is to apply the known entropic duality formula to the robust budget directly. That route fails because the objective $E^n_{D'}[\ell]$ is a ratio of two linear functions of $D'$ , not a linear function. The ratio is quasi-linear, and Lagrangian duality does not apply to it as it stands. The paper first lifts it to a linear objective over the cone $(s, P) = (s, sD')$ (Corollary 1). The entropy constraint then becomes the perspective $s\,B(P/s, D) \le s\,r$ , and duality is applied to this lifted program. A second difficulty is that the reference $D$ may vanish on part of the support. The ball then lives on a face of the simplex, and every step must respect the convention $B = +\infty$ off the support of $D$ . Finally, strong duality needs a Slater point, which exists only for $r > 0$ . The cases $r \le 0$ of the goal have to be handled separately.

Formalization scope

The support $\Omega_n$ is a finite type ι, and $\mathcal D_n$ is stdSimplex ℝ ι. Covariates, responses and the distance of Definition 2 do not appear: only the weights w : ι → ℝ (positive) and the losses L z : ι → ℝ of a fixed decision enter. Losses are real-valued, a restriction of the paper's $\mathbb R_+ \cup \{+\infty\}$ , while nonnegativity is not required. The conventions are the following.

$B$ is EReal-valued: it is $+\infty$ when the first argument charges a zero of the second, and $0 \log 0 = 0$ .
All suprema and infima are in EReal: the supremum of the empty set is $-\infty$ and the infimum of the empty set is $+\infty$ .
Dual variables satisfy $\nu > 0$ . The page's $\nu \in \mathbb R_+$ admits $\nu = 0$ only as the perspective limit, and the infimum over $\alpha$ is unchanged.
In the perspective programs, $P/s \in \mathcal D_n$ is stated explicitly.
The neighbourhood chain is a monotone family of finite sets with $N^0 = \emptyset$ and $N^n = \Omega_n$ .

Several formalizations would make the statements trivial, and each is ruled out:

a real-valued $B$ , whose finite junk values enlarge the ball when $D$ has zeros;
real sSup/sInf, which return $0$ on empty or unbounded sets;
$\nu \ge 0$ with Lean's $x/0 = 0$ , which makes every $\alpha$ feasible;
a positivity hypothesis on $D$ , which the lemma does not have.

A complete development needs the following:

Gibbs' inequality and continuity of $B$ on the simplex;
Lagrangian (or Fenchel) duality for a convex program with one entropic constraint and linear constraints;
the perspective of relative entropy;
the one-dimensional conjugate of $\lambda \log \lambda$ .

The duality and conjugate lemmas are reusable for any KL-ball robust program. Contributions are welcome on each milestone, on bridges from the published RobustMDP.EntropyInner theorems to the setting here (they agree with $B$ when the reference is positive), and on the $r \le 0$ cases of the goal.

Selected references

D. Bertsimas and B. Van Parys, Bootstrap robust prescriptive analytics, arXiv:1711.09974v2, 2021 (Math. Program., 2021). https://arxiv.org/abs/1711.09974v2
G.-Y. Ban and C. Rudin, The big data newsvendor: practical insights from machine learning, Operations Research 67(1), 2019. https://doi.org/10.1287/opre.2018.1757
D. Bertsimas and N. Kallus, From predictive to prescriptive analytics, Management Science 66(3), 2020. https://doi.org/10.1287/mnsc.2018.3253
A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. https://doi.org/10.1287/opre.1050.0216
A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg and G. Rennen, Robust solutions of optimization problems affected by uncertain probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641

11 thms3 active usersReviewed

Completed

Analysis Operations Research·Captain: mikedeng1

Extrapolated Proximal Subgradient Algorithms for Nonconvex and Nonsmooth Fractional Programs 1: Every Cluster Point of the e-PSG Iterates Is a Lifted Stationary PointResearch Paper

Motivation

A fractional program minimizes a ratio $f(x)/g(x)$ over a set $S$ . Nonconvex, nonsmooth ratios arise in the scale-invariant sparse signal recovery model $\min\|x\|_1/\|x\|_2$ over a polyhedron, in robust Sharpe-ratio optimization in finance, and in the Rayleigh quotient $x^\top Ax/x^\top Bx$ over a sphere; with $g\equiv1$ and $S=H$ the problem reduces to composite optimization $\min f^{\mathsf s}+f^{\mathsf n}$ . The classical method of Dinkelbach (1967) and its proximal-gradient descendants assume a convex numerator and a concave or smooth denominator, which these models do not satisfy.

Boţ, Dao and Li (arXiv:2003.04124, Math. Oper. Res. 2022) propose the extrapolated proximal subgradient algorithm (e-PSG) for problems in which the numerator is the sum of a smooth convex and a nonsmooth nonconvex term and the denominator is only weakly convex, and they prove that its cluster points satisfy a first-order condition. This mission formalizes that subsequential convergence theorem (Theorem 4.5).

Setting

Let $H=\mathbb R^N$ with the Euclidean inner product, and let $S\subseteq H$ be nonempty, closed and convex. The problem is

\min_{x\in S}\ \frac{f(x)}{g(x)}.\qquad(\mathrm P)

Assumption 1. $f=f^{\mathsf s}+f^{\mathsf n}$ , where $f^{\mathsf s}:H\to\mathbb R$ is continuously differentiable and convex with an $\ell$ -Lipschitz gradient, $f^{\mathsf n}:H\to(-\infty,+\infty]$ is proper and lower semicontinuous, $S\cap\operatorname{dom}f\ne\emptyset$ , and $f\ge0$ on $S\cap\operatorname{dom}f$ .

Assumption 2. $g$ is finite and positive on $S$ , continuous on an open set containing $S$ , and either weakly convex with modulus $\beta$ on an open convex set containing $S$ (that is, $g+\frac\beta2\|\cdot\|^2$ is convex there), or regular (Fréchet and limiting subdifferentials coincide) and weakly convex with modulus $\beta$ on $S$ .

The limiting subdifferential $\partial_L h(x)$ collects limits of Fréchet subgradients $u_k\in\widehat\partial h(x_k)$ along $x_k\to x$ with $h(x_k)\to h(x)$ . A point $\bar x\in S$ is a lifted stationary point of (P) if

0\in g(\bar x)\,\partial_L(f+\iota_S)(\bar x)-f(\bar x)\,\partial_L g(\bar x),

where $\iota_S$ is $0$ on $S$ and $+\infty$ off $S$ .

The boundedness condition (BC) asks for $0<m\le g\le M$ on $S\cap\operatorname{dom}f$ . Algorithm 1 (e-PSG) starts from $x_{-1}=x_0\in S\cap\operatorname{dom}f$ with parameters $\delta>0$ , $\zeta>0$ ( $1-\sqrt\beta\zeta>0$ ) and extrapolation bounds $\bar\mu,\bar\kappa$ (in explicit ranges depending on $m,M,\ell$ under (BC), and $\bar\mu=\bar\kappa=0$ otherwise). At step $n$ it sets $\theta_n=f(x_n)/g(x_n)$ , picks $g_n\in\partial_L g(x_n)$ and $0<\tau_n\le1/\max\{\sqrt\beta\theta_n/\zeta,\delta\}$ , forms $u_n=x_n+\kappa_n(x_n-x_{n-1})$ , $v_n=x_n+\mu_n(x_n-x_{n-1})$ with $\kappa_n\in[0,\bar\kappa]$ , $\mu_n\in[0,\bar\mu\tau_n]$ , and takes

x_{n+1}\in\operatorname*{argmin}_{x\in S}\Big(f^{\mathsf n}(x)+f^{\mathsf s}(u_n)+\langle\nabla f^{\mathsf s}(u_n),x-u_n\rangle+\tfrac1{2\tau_n}\|x-v_n-\tau_n\theta_ng_n\|^2+\tfrac\ell2\|x-u_n\|^2\Big).

Finally $S_0=\{x\in S: f(x)/g(x)\le f(x_0)/g(x_0)\}$ .

Formalization targets

Goal: Theorem 4.5(iii)

If $S_0$ is bounded and $\liminf_n\tau_n=\bar\tau>0$ , then every cluster point $\bar x$ of $(x_n)$ satisfies

\bar x\in S\cap\operatorname{dom}f,\qquad \lim_{n\to\infty}\frac{f(x_n)}{g(x_n)}=\frac{f(\bar x)}{g(\bar x)},\qquad \bar x\ \text{is lifted stationary.}

In the formal statement $g$ is in addition Lipschitz around every point of $S$ ; see Formalization scope.

Milestones, in proof order

Lemma 4.3: for $x,y\in S$ and $u\in\partial_L g(x)$ , $\langle u,y-x\rangle\le g(y)-g(x)+\frac\beta2\|y-x\|^2$ .
Lemma 4.4 (descent lemma), already on the platform.
Inequality (16): the one-step inequality from the subproblem.
Inequality (17): the ratio inequality, for every Young parameter $\omega>0$ .
Theorem 4.5(i): $x_n\in S\cap\operatorname{dom}f$ and

\Big(\tfrac{f(x_{n+1})}{g(x_{n+1})}+c\|x_{n+1}-x_n\|^2\Big)+\alpha\|x_{n+1}-x_n\|^2\le\tfrac{f(x_n)}{g(x_n)}+c\|x_n-x_{n-1}\|^2

with the explicit constants (14), and convergence of $f(x_n)/g(x_n)$ . 6. Theorem 4.5(ii): $(x_n)$ is bounded, $\|x_{n+1}-x_n\|\to0$ , and $\sum_n\|x_{n+1}-x_n\|^2<\infty$ . 7. The limit inequality at a cluster point (proof of Theorem 4.5(iii), p. 13).

Significance

Theorem 4.5 is the subsequential convergence result on which the paper's later results rest: with a Kurdyka–Łojasiewicz property of a merit function it upgrades to convergence of the whole sequence and to linear rates (Theorem 5.5), and under strict differentiability of $g$ lifted stationarity becomes ordinary stationarity (Corollary 4.6). The merit function $F_n=f(x_n)/g(x_n)+c\|x_n-x_{n-1}\|^2$ with explicit constants is the template for analyzing extrapolated proximal methods on ratio objectives.

The result is proved on paper; no machine-checked version exists. Formalizing it produces a verified descent analysis of an extrapolated proximal method for a nonconvex ratio, a formal subgradient inequality for weakly convex functions with respect to the limiting subdifferential, and a checked passage to the limit through limiting subdifferentials. It also pins down the hypotheses: the formal statement records a missing assumption of the printed theorem (below).

Difficulty

The ratio is not a sum, so the standard sufficient-decrease argument for proximal gradient methods does not apply directly: the subproblem linearizes $g$ through a limiting subgradient $g_n$ scaled by the current ratio $\theta_n$ , and the descent of $f/g$ comes only after dividing by $g(x_{n+1})$ , which ties the step size to $\theta_n$ and to bounds on $g$ . Extrapolation adds a cross term $\langle x_{n+1}-x_n,x_n-x_{n-1}\rangle$ that the merit function must absorb, which is where the explicit ranges of $\bar\mu,\bar\kappa$ come from. At a cluster point, $f$ is only lower semicontinuous, so convergence of $f(x_{k_n})$ to $f(\bar x)$ must be extracted from the optimality of the subproblems, and the limits of $g_n$ must be shown to lie in $\partial_L g(\bar x)$ . The naive approach of passing to the limit in the subproblem's optimality condition fails because $\partial_L(f^{\mathsf n}+\iota_S)$ has no sum rule in this generality.

Formalization scope

$H$ is EuclideanSpace ℝ (Fin N). Functions into $(-\infty,+\infty]$ are EReal-valued; properness is the published IsProperFn, and $\widehat\partial$ , $\partial_L$ are the published IsRegularSubgrad and LimitingSubdiff. The denominator $g$ is real-valued on all of $H$ : only its values and subgradients near $S$ enter, where the paper's $g$ is finite. Weak convexity "with modulus $\beta$ " means that $\beta\ge0$ is a valid constant, not the smallest one. A run of Algorithm 1 is a predicate on the sequences $(x_n),(g_n),(\tau_n),(\kappa_n),(\mu_n)$ ; the argmin and $g_n$ are selections, never Classical.choose. $x_{-1}=x_0$ . Ratios are real numbers (f x).toReal / g x, meaningful because the iterates stay in $\operatorname{dom}f$ . The $\bar\kappa$ -range of Step 1 is written as $\ell\bar\kappa^2<\frac{m\delta(1-\sqrt\beta\zeta)}M-\frac{2m\bar\mu}{\sqrt{mM}}$ , avoiding division by $\ell$ . $\liminf\tau_n>0$ is an eventual positive lower bound, which is equivalent since $\tau_n\le1/\delta$ . Cluster points are MapClusterPt.

Correction. Under the second alternative of Assumption 2 alone, Theorem 4.5(iii) fails: for $S=[0,1]$ , $g(x)=2-\sqrt x$ on $S$ and $f(x)=1-\sqrt x/4$ , the iterates converge to $0$ , where $\partial_Lg(0)=\emptyset$ , so $0$ is not lifted stationary. The goal and the limit-inequality milestone therefore assume that $g$ is Lipschitz around every point of $S$ , which holds automatically under the first alternative.

The trivializing formalizations are ruled out: the parameter ranges are inhabited (checked in Lean, including $\ell=0$ ), the goal quantifies over every cluster point of every run, and lifted stationarity requires actual limiting subgradients rather than an infDist that would be $0$ on an empty set.

Contributions welcome: the subgradient inequality for weakly convex functions, the descent lemma's use in (16), the limit arguments for limiting subdifferentials (the platform has the robustness property (3) as NonconvexSplitting.ProxGrad.limitingSubdiff_robust), and Fermat's rule for constrained minimizers of $\varphi+\iota_S$ — the last is reusable well beyond this mission.

Selected references

R. I. Boţ, M. N. Dao, G. Li, Extrapolated Proximal Subgradient Algorithms for Nonconvex and Nonsmooth Fractional Programs, Math. Oper. Res. 47 (2022); arXiv:2003.04124v2. https://arxiv.org/abs/2003.04124
W. Dinkelbach, On nonlinear fractional programming, Management Science 13 (1967) 492–498. https://doi.org/10.1287/mnsc.13.7.492
B. S. Mordukhovich, Variational Analysis and Generalized Differentiation I, Springer, 2006. https://doi.org/10.1007/3-540-31247-1
Y. Nesterov, Introductory Lectures on Convex Optimization, Springer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

13 thms3 active usersReviewed

Machine Learning Operations Research Optimal Transport·Captain: mikedeng1

Regularization via Mass Transportation II: Wasserstein-Robust Linear Regression Equals Empirical Loss plus a Dual-Norm PenaltyResearch Paper

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

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$ .
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.
End of the proof of Lemma A.3 (p. 30). $\mathrm{lip}(L)=\sup\{|\theta|:L^*(\theta)<\infty\}$ .
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).

15 thms3 active usersReviewed

Completed

Convex Optimization Operations Research·Captain: mikedeng1

Proximal Algorithms I: A Point Minimizes f + g Exactly When It Is a Fixed Point of the Forward-Backward Operator x ↦ prox_λg(x − λ∇f(x))Research Paper

Motivation

Many convex optimization problems combine a smooth loss with a term that is easy to handle through minimization but awkward to differentiate. A constraint can be represented by an indicator function that is zero on the feasible set and $+\infty$ outside it. A norm penalty can be finite yet nonsmooth. The proximal gradient method handles such objectives by applying a gradient step to the smooth term and a proximal step to the other term. Parikh and Boyd present this method in §4.2 of Proximal Algorithms, after developing the proximal operator, its fixed points, and its connection to the subdifferential.

The mission concerns the method's optimality interpretation. A fixed point of the forward-backward update is a minimizer of the composite objective, for every positive step size. That is a statement about which points solve the problem. The separate claim that repeated updates converge requires further control of the gradient and the step size; the paper discusses that condition after the fixed-point identity on p. 151. This mission captures the fixed-point identity itself and the paper's stated convex-analytic results that support it.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $x^{\mathsf T}y$ and norm $\|x\|_2$ . Let $f:\mathbb R^n\to\mathbb R$ be convex and differentiable everywhere. Let $g:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ be closed, proper and convex: its epigraph is nonempty, closed and convex. The effective domain $\operatorname{dom}g$ consists of the points where $g$ is finite. The composite problem, equation (4.5), is to minimize $f(x)+g(x)$ over all $x\in\mathbb R^n$ . An indicator $g=I_C$ expresses the constraint $x\in C$ within the same notation. These conventions are those of §1.1 and §4.2 of the monograph.

For a closed proper convex function $h$ , the proximal operator sends $v$ to the unique minimizer of $h(u)+\tfrac12\|u-v\|_2^2$ . For $\lambda>0$ , the operator $\operatorname{prox}_{\lambda h}$ equivalently minimizes $h(u)+\tfrac1{2\lambda}\|u-v\|_2^2$ . The paper assumes closed proper convexity whenever it uses a proximal operator, including one applied to $g$ . This assumption gives a unique proximal point at every input, even when $g$ is infinite outside a strict subset of the space.

The subdifferential $\partial g(x)$ is the set of vectors $y$ such that $g(z)\ge g(x)+y^{\mathsf T}(z-x)$ for every $z\in\operatorname{dom}g$ , as in (2.3). Unlike the gradient of $f$ , it can be empty or contain several vectors. The resolvent of the subdifferential with parameter $\lambda$ is the inverse relation $(I+\lambda\partial g)^{-1}$ . Equation (3.4) says that this relation is the everywhere-defined, single-valued map $\operatorname{prox}_{\lambda g}$ . Both descriptions of the proximal point appear in the milestone list.

Formalization targets

Goal: fixed points of the forward-backward operator

For any $\lambda>0$ and $x^\star\in\mathbb R^n$ , the target from §4.2.1, pp. 150–151, is

x^\star\text{ minimizes }f+g \quad\Longleftrightarrow\quad x^\star=\operatorname{prox}_{\lambda g}\bigl(x^\star-\lambda\nabla f(x^\star)\bigr).

The quantifier covers every positive $\lambda$ ; it is independent of any Lipschitz bound. The equation describes a fixed point of the forward-backward operator, which first evaluates $\nabla f$ and then applies the proximal operator of $g$ .

Supporting statements

The milestones follow statements printed in the same monograph: existence and uniqueness of a proximal minimizer from (1.1)–(1.2); the subdifferential optimality condition for a proximal minimizer in §2.3; the fixed-point characterization of minimizers in §2.3; the full-domain, single-valued resolvent identity (3.4); and the condition $0\in\nabla f(x^\star)+\partial g(x^\star)$ for minimizing $f+g$ in §4.2.1. The resolvent milestone includes its domain and uniqueness claims because the paper states both, rather than only an equality of partially defined relations. These targets retain the authors' constants $\tfrac12$ , $\tfrac1{2\lambda}$ and $\lambda$ .

Why the result matters

The equivalence identifies the solutions of a composite convex problem using an update rule that treats the smooth and nonsmooth terms differently. It applies when $g$ encodes constraints or a nonsmooth penalty and still characterizes the exact minimizers. It also says what a converged proximal gradient iteration must solve. The characterization by itself makes no claim that an iteration converges, a distinction made in the paper's discussion on p. 151. Parikh and Boyd, §4.2.1, give the fixed-point view of the algorithm in precisely this setting.

The formalization connects an existing machine-checked proximal-point definition from the Moreau 1965 series to a new Euclidean subdifferential defined by the supporting inequality (2.3). It leaves reusable statements about proximal optimality and resolvents alongside the composite result. A related published theorem, ProxNewton.Inexact.compGradStep_eq_zero_iff, characterizes minimizers through a composite-gradient step at unit step length under stronger smoothness assumptions and a different proximal representation. The present target preserves the monograph's arbitrary positive $\lambda$ , its extended-real $g$ , and its particular proximal operator.

Difficulty

The two sides of the goal compare different minimization problems. The left side minimizes $f+g$ globally; the right side minimizes a quadratic centered at $x^\star-\lambda\nabla f(x^\star)$ plus $\lambda g$ . Merely expanding the definition of the proximal operator does not make these objectives identical. The needed first-order conditions must also remain valid when $g$ is infinite outside its domain and its subdifferential is set-valued. In (3.4), an inverse relation is asserted to have a value at every point and only one value there; an equality that overlooks either property would be weaker than the paper's statement.

Formalization scope

The Lean carrier is EuclideanSpace ℝ (Fin n) for arbitrary $n\in\mathbb N$ . Its norm and inner product are the paper's Euclidean ones. No positive-dimension hypothesis is imposed: the zero-dimensional case is a singleton space and does not invalidate these identities. Values of $g$ are in EReal; the imported MoreauProx.Decomposition.GammaZero records that $g$ never equals $-\infty$ , is finite somewhere, has a convex epigraph, and is lower semicontinuous. For real-valued convex $f$ on all of $\mathbb R^n$ , closedness and properness follow from finiteness and convexity. Differentiability is explicit so Mathlib's gradient f x represents the intended $\nabla f(x)$ .

The imported MoreauProx.Decomposition.IsProx is a predicate saying that a point minimizes $\tfrac12\|u-v\|_2^2+\lambda g(u)$ . Positive $\lambda$ makes its minimizers those of the paper's (1.2), including at points where $g(u)=+\infty$ . Uniqueness is supplied by the referenced Moreau strict-minimum theorem. The local subdifferential follows (2.3): it is empty when its argument lies outside the effective domain, and it tests the supporting inequality over all $z\in\mathbb R^n$ . Outside $\operatorname{dom}g$ the right side is $+\infty$ , so those tests add no restriction. The composite minimization condition ranges over every $y\in\mathbb R^n$ and compares extended-real values.

The goal must relate these two genuinely different minimization problems through the gradient and convexity; defining the forward-backward operator to minimize $f+g$ would empty the theorem of its content. Contributions on extended-real subgradient calculus, the full-domain resolvent relation, and the composite optimality condition are welcome. The imported Moreau definitions and the local supporting-inequality subdifferential are reusable in further convex optimization developments.

This source PDF is the authors' Foundations and Trends formatted copy of the published monograph. Printed page numbers throughout this mission refer to that copy; its body begins on PDF page 5 at printed p. 123.

Selected references

Neal Parikh and Stephen Boyd, Proximal Algorithms, Foundations and Trends in Optimization 1(3), 2014. DOI: 10.1561/2400000003.

8 thms3 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Quantity Flexibility Contracts and Supply Chain Performance 1: Under the Minimum Commitment Policy a Flex Node With At Least Its Customer's Flexibility Keeps Zero InventoryResearch Paper

Motivation

Manufacturers and their suppliers rarely trade on fixed orders. A buyer sends a rolling schedule of intended purchases for the coming periods and revises it every period as its own forecasts change. Left unconstrained, such revisions pass demand volatility up the supply chain and amplify it, the phenomenon studied as the bullwhip effect (Lee, Padmanabhan & Whang 1997). A quantity flexibility (QF) contract limits how far each estimate may move from one period to the next: the buyer commits to a band around its earlier estimate, and the supplier commits to supply anything inside that band. The paper reports QF-type agreements at Sun Microsystems, Solectron, Nippon Otis, Toyota, IBM, Hewlett Packard and Compaq (p. 92).

Tsay & Lovejoy (1999) model a multi-stage chain in which every stage is linked to its neighbours by QF contracts, and ask how the flexibility a node offers its customer, compared with the flexibility it receives from its supplier, determines the inventory the node must carry. This mission formalizes their answer for one node: Proposition 2 (p. 97), which states that a node whose supply side is at least as flexible as its customer side needs no inventory at all.

Setting

Time is discrete, $t = 0, 1, 2, \dots$ . In period $t$ a flex node receives from its customer a release schedule $f(t) = [f_0(t), f_1(t), \dots]$ : $f_0(t)$ is the quantity sold in period $t$ , and $f_j(t)$ is the current estimate of the quantity to be sold in period $t + j$ . The node sends its supplier a replenishment schedule $r(t) = [r_0(t), r_1(t), \dots]$ with the same meaning on the purchase side. Its ending stock evolves as

I(t) = I(t-1) + r_0(t) - f_0(t).

The QF contract on the customer side has output parameters $\alpha^{out}_q \ge 0$ and $0 \le \omega^{out}_q \le 1$ , $q \ge 1$ , and the output IR (Incremental Revision) constraints (6):

(1 - \omega^{out}_j)\, f_j(t) \le f_{j-1}(t+1) \le (1 + \alpha^{out}_j)\, f_j(t), \qquad j \ge 1.

The supplier side has input parameters $(\alpha^{in}_q, \omega^{in}_q)$ and the analogous constraints (7) on $r$ . The cumulative flexibilities (9), (11) are

1 + A_j = \prod_{q=1}^{j}(1 + \alpha_q), \qquad 1 - \Omega_j = \prod_{q=1}^{j}(1 - \omega_q),

on each side, with $A_0 = \Omega_0 = 0$ . The pair of sequences $(A, \Omega)$ is the side's flexibility profile.

The node follows the Minimum Commitment (MC) policy (21)–(23). From $I(t-1)$ , $r(t-1)$ and $f(t)$ it computes, by one recursion on $j \ge 0$ , projected inventories $l_j(t)$ and the new schedule:

l_0(t) = I(t-1),\qquad r_j(t) = \max\Bigl[\frac{(1 + A^{out}_j) f_j(t) - l_j(t)}{1 + A^{in}_j},\ (1 - \omega^{in}_{j+1})\, r_{j+1}(t-1)\Bigr],

l_{j+1}(t) = \bigl[l_j(t) + (1 - \Omega^{in}_j)\, r_j(t) - (1 + A^{out}_j)\, f_j(t)\bigr]^+.

The first term of the maximum is the target $T_j(t)$ of (22): the least supply that covers the largest purchase the customer may still make in period $t + j$ . The second term is the least value the supplier contract allows given last period's schedule.

Formalization targets

Goal: Proposition 2

Under the standing assumptions, if (a) the release schedules are nonnegative and obey (6), (b) the node uses the MC policy, (c) $I(0) = 0$ and the run starts with $r(0) = f(0)$ , and (d) $A^{out}_j \le A^{in}_j$ and $\Omega^{out}_j \le \Omega^{in}_j$ for all $j \ge 1$ , then

I(t) = 0 \quad \text{for all } t.

If moreover $(A^{in}, \Omega^{in}) = (A^{out}, \Omega^{out})$ and $\omega^{in}_q < 1$ for all $q$ , then

r_j(t) = f_j(t) \quad \text{for all } j \ge 0,\ t \ge 1.

Milestones

(8), p. 95: the IR constraints imply the cumulative bounds $(1 - \Omega^{out}_j) f_j(t) \le f_0(t + j) \le (1 + A^{out}_j) f_j(t)$ .
Coverage, p. 108: along the MC run, $r_j(t) \ge T_j(t)$ for every $j$ , hence $I(t) \ge 0$ .
Inventory is non-increasing, p. 108: under (d), $r_0(t) \le f_0(t)$ , hence $I(t) \le I(t-1)$ .
The vanishing step, p. 108: if $l_j(t) = 0$ and $r_j(t) = f_j(t)$ , then $l_{j+1}(t) = 0$ .

Significance

Proposition 2 isolates the source of inventory at an intermediate stage of a QF-linked chain: it is the disparity between the node's input and output flexibility, not the volatility of the forecasts themselves. A node supplied at least as flexibly as it serves can meet every contractual obligation with zero stock, and a node with matched flexibility passes every schedule upstream unchanged, acting as a non-distorting conduit of information and material. The paper uses this to argue that supply flexibility beyond the customer's is wasted at the node unless passed downstream (p. 97). Inventory under a flexibility mismatch, where the node amplifies flexibility, is studied numerically in §5 of the paper.

The result has a short proof in the paper, but that proof routes through formula (33), a closed form of the MC schedule as a maximum over all earlier periods, whose proof is omitted and which needs schedules before any starting period. A machine-checked proof must instead argue directly on a run with a definite start. No part of the paper has been formalized before; this mission also produces a reusable formal model of rolling schedules, QF constraints and the MC policy.

Difficulty

The obvious argument shows $r_0(t) \le f_0(t)$ from the definition of the MC policy at index $0$ alone. That fails: $r_0(t)$ is a maximum that includes the carried-over term $(1 - \omega^{in}_1)\, r_1(t-1)$ , which depends on the whole earlier schedule $r(t-1)$ , and that in turn on $r(t-2)$ , and so on back to the initial schedule. Bounding $r_0(t)$ therefore requires control of every component of every earlier schedule, an invariant over both indices that the paper does not state. The start of the run matters: with an unconstrained initial schedule the claim is false. The equal-flexibility part additionally needs a second induction, on $j$ within each period, interleaved with the recursion that defines $l_j(t)$ and $r_j(t)$ .

Formalization scope

Schedules are functions $\mathbb N \to \mathbb R$ indexed by $j \ge 0$ ; the release schedules are a function $f : \mathbb N \to \mathbb N \to \mathbb R$ with f t j $= f_j(t)$ . The QF parameters are sequences $\mathbb N \to \mathbb R$ whose value at index $0$ is unused. Constraint (6) is stated with the paper's $j$ written $j + 1$ . The MC policy is defined literally by (21)–(23), for every $j \in \mathbb N$ , as one recursion that interleaves $l_j(t)$ and $r_j(t)$ ; the run starts from a given state $(I(0), r(0))$ at period $0$ and applies the policy from period $1$ on. All values are real.

The standing assumptions of p. 95 ( $\alpha \ge 0$ , $0 \le \omega \le 1$ ) are hypotheses. Three hypotheses are added to the page's statement and disclosed in each item:

$f_j(t) \ge 0$ , implicit in the paper ("all quantities are measured in end-item equivalents") and used by its proof;
the start $r(0) = f(0)$ : the paper names no initial schedule, and with a large $r_1(0)$ the conclusion fails at $t = 1$ ;
$\omega^{in}_q < 1$ in the equal-flexibility part only: the paper's proof divides by $1 - \Omega^{in}_j$ , and with $\omega = 1$ allowed the part is false.

A formalization in which the run sets $r(t) := f(t)$ , or in which the MC step drops the carried-over term in (21) or the positive part in (23), would make the goal trivial; the model rules this out by defining the policy exactly as printed. Condition (d) compares the cumulative profiles, not the parameters termwise. Formula (33) and Propositions 1, 3 and 4 are not part of this mission; Proposition 1 (optimality of MC for the open-loop program) is the companion mission.

Contributions welcome: proofs of the milestones, a proof of the goal through an invariant on $(1 - \Omega^{in}_j)\, r_j(t)$ , and lemmas about the MC run reusable for the companion mission.

Selected references

A. A. Tsay and W. S. Lovejoy, Quantity Flexibility Contracts and Supply Chain Performance, Manufacturing & Service Operations Management 1(2):89–111, 1999. https://doi.org/10.1287/msom.1.2.89
A. A. Tsay, The Quantity Flexibility Contract and Supplier–Customer Incentives, Management Science 45(10):1339–1358, 1999. https://doi.org/10.1287/mnsc.45.10.1339
H. L. Lee, V. Padmanabhan and S. Whang, Information Distortion in a Supply Chain: The Bullwhip Effect, Management Science 43(4):546–558, 1997. https://doi.org/10.1287/mnsc.43.4.546

6 thms3 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization Operations Research·Captain: mikedeng1

How Bad is Selfish Routing? 2: With Linear Latency Functions the Cost of a Nash Flow Is at Most 4/3 Times the Optimal CostResearch Paper

Motivation

In a road or communication network, each user picks a route to minimize its own delay, without regard to the delay it imposes on others. The outcome is an equilibrium that is in general not socially optimal: Braess's paradox shows that adding a road can make every user worse off, and Pigou's two-link example shows that selfish users can incur a third more total delay than a central planner would. Transportation science has studied such equilibria since Wardrop (1952) and Beckmann, McGuire and Winsten (1956). The computer-science question of how much is lost, uniformly over all networks, was answered for linear delays by Roughgarden and Tardos in How Bad is Selfish Routing? (FOCS 2000; J. ACM 2002, doi:10.1145/506147.506153). Their bound became the first instance of the price of anarchy for nonatomic routing and the template for a large literature on the inefficiency of equilibria.

Timeline. Wardrop (1952) states the equilibrium principle. Beckmann et al. (1956) and Dafermos–Sparrow (1969) characterize equilibria and optima by convex programs. Koutsoupias and Papadimitriou (1999) introduce the worst-case ratio of equilibrium to optimum. Roughgarden and Tardos (2000/2002) prove the bound $4/3$ for linear latencies, tight by Pigou's example. Roughgarden (2003) and Correa, Schulz and Stier-Moses (2004) extend the analysis to general latency classes.

Setting

A network has finitely many edges $e$ and finitely many routes $P$ ; a route is the set of edges it uses, recorded by a $0/1$ incidence. There are $k$ commodities; each route serves one commodity $i$ , and $\mathcal P_i$ is the set of routes serving $i$ . Commodity $i$ has a positive rate $r_i$ . A flow assigns a nonnegative amount $f_P$ to each route; it is feasible for $r$ if $\sum_{P\in\mathcal P_i}f_P=r_i$ for every $i$ . The edge flow is $f_e=\sum_{P\ni e}f_P$ .

Each edge has a linear latency $\ell_e(x)=a_ex+b_e$ with $a_e,b_e\ge0$ . 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 if no small amount of flow on a route $P_1$ can reduce its latency by moving to another route $P_2$ of the same commodity (Definition 2.1); equivalently (Lemma 2.2), every used route of commodity $i$ has minimum latency among the routes in $\mathcal P_i$ . A flow is optimal if it is feasible and has minimum cost among feasible flows. The marginal cost of edge $e$ is $\ell^*_e(x)=(x\ell_e(x))'=2a_ex+b_e$ , and $L^*_i(f^*)=\min_{P\in\mathcal P_i}\sum_{e\in P}\ell^*_e(f^*_e)$ .

The Lean development uses the names pathLatency, cost, IsNashFlow, IsOptimalFlow, linLatency, marginalLatency and minMarginalPathCost for these objects.

Formalization targets

Goal: Theorem 4.5

For every instance with linear latencies $a_e,b_e\ge0$ , every Nash flow $f$ and every feasible flow $f^*$ ,

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

This is the paper's $\rho(G,r,\ell)=C(f)/C(f^*)\le4/3$ , stated without the ratio.

Milestones

Lemma 2.2: Nash flows are exactly the Wardrop flows (for continuous nondecreasing latencies).
Lemma 2.3: at a Nash flow, $C(f)=\sum_iL_i(f)\,r_i$ , with $L_i(f)$ the common latency of the used routes of commodity $i$ .
Lemma 4.1(a), (b): Nash and optimal flows for linear latencies, characterized by $\sum_{e\in P}(a_ef_e+b_e)$ and $\sum_{e\in P}(2a_ef^*_e+b_e)$ being minimal on used routes.
Corollary 4.2: for $\ell_e(x)=a_ex$ , optimal and Nash flows coincide.
Lemma 4.3: if $f$ is a Nash flow for $r$ then $f/2$ is optimal for $r/2$ , and $\ell^*_P(f/2)=\ell_P(f)$ .
Lemma 4.4: if $f^*$ is optimal for $r$ and $\delta>0$ , every flow feasible for $(1+\delta)r$ costs at least $C(f^*)+\delta\sum_iL^*_i(f^*)\,r_i$ .
$C(f/2)\ge\frac14C(f)$ (proof of Theorem 4.5).
Figure 3: in Pigou's network the Nash flow costs $1$ and the optimal flow $3/4$ , so the constant $4/3$ is attained.

Significance

The bound says that, with linear delays, selfish routing never costs more than $4/3$ times the optimum, independently of the network's size and topology and of the number of commodities. It explains why Braess-type phenomena are bounded in magnitude, and it yields consequences for mechanical networks of strings and springs (Corollary 4.6 of the paper). The inequality $C(f)\le\frac43C(f^*)$ for every feasible $f^*$ is the basic input to later work on bicriteria bounds, Stackelberg routing, tolls and the general price-of-anarchy framework.

The result is proved in the paper and in textbooks (Nisan et al., Algorithmic Game Theory, ch. 18). No machine-checked proof is known to exist on Prove2Me or in Mathlib. A formalization produces a checked model of nonatomic routing (route flows, Nash and optimal flows) together with the first-order characterization of optimal flows for convex quadratic costs, both of which are reusable for the other results of the paper and for later routing papers.

Difficulty

The equilibrium bound is not a pointwise inequality between the two flows: the Nash flow $f$ and an arbitrary feasible flow $f^*$ can use entirely different routes. The step that requires real work is the comparison between an optimal flow for the rates $r/2$ and an arbitrary flow for the rates $r$ (Lemma 4.4), which rests on the characterization of optimal flows of a convex program (Lemma 4.1(b)). That characterization is a Karush–Kuhn–Tucker statement over a polytope of route flows; the paper cites it rather than proving it, and Mathlib has no ready-made version. The naive approach, bounding each edge's cost separately, fails because the two flows load different edges.

Formalization scope

Edges, routes and commodities are Fin J, Fin R, Fin Sd. A route is a $0/1$ column A j r of the incidence; the commodity of route r is s r. The paper's simple paths in a directed graph are one instance, so all statements are a disclosed generalization; copies of one path serving two commodities are two routes.
Edge flows and feasibility are the published KellyStochasticNetworks.linkFlow and KellyStochasticNetworks.wardropFeasible; the Wardrop condition is KellyStochasticNetworks.IsWardropEquilibrium.
All rates are positive (0 < rate i), as on p. 6. Linear latencies have $a_e,b_e\ge0$ , and only their values at nonnegative arguments matter.
Definition 2.1 is formalized for distinct routes $P_1\neq P_2$ and $0<\delta\le f_{P_1}$ . The literal $P_1=P_2$ would make Nash flows nonexistent, and the literal $\delta=0$ on an unused $P_1$ would force equal latencies on unused routes; both readings would make the theorems vacuous or false.
Lemmas 2.2 and 2.3 are stated for arbitrary latencies that are nonnegative, nondecreasing and continuous on $[0,\infty)$ ; continuity replaces differentiability, as the paper's footnote 3 allows.
The ratio $\rho$ is never formed: $C(f^*)$ may be $0$ and Lean's division returns $0$ there. Every bound is stated as an inequality against every feasible flow.
$L^*_i$ is a minimum over the nonempty finite set of routes serving $i$ ; $L_i(f)$ in Lemma 2.3 is stated existentially.
A trivializing formalization (a Nash definition no flow satisfies, a ratio with junk denominator, or a single-commodity or parallel-link special case) is ruled out by the choices above; Pigou's flow $(0,1)$ is checked to satisfy the formal Nash definition.

Needed infrastructure: the edge/route exchange of summation, the first-order optimality conditions for a convex differentiable function on a product of simplices, and the convexity inequality $x\ell_e(x)\ge y\ell_e(y)+(x-y)\ell^*_e(y)$ . Contributions of a general KKT lemma for separable convex costs on flow polytopes are reusable beyond this mission.

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. G. Wardrop, Some theoretical aspects of road traffic research, Proc. Institution of Civil Engineers, Part II, 1, 325–378, 1952. https://doi.org/10.1680/ipeds.1952.11259
M. Beckmann, C. B. McGuire and C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956.
S. C. Dafermos and F. T. Sparrow, The traffic assignment problem for a general network, J. Research of the National Bureau of Standards 73B(2), 91–118, 1969. https://doi.org/10.6028/jres.073B.010
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. Computer and System Sciences 67(2), 341–364, 2003. https://doi.org/10.1016/S0022-0000(03)00044-8

15 thms3 active usersReviewed

Completed

Convex Optimization Linear algebra·Captain: mikedeng1

Guaranteed Minimum-Rank Solutions of Linear Matrix Equations via Nuclear Norm Minimization 1: If δ_5r < 1/10, Nuclear Norm Minimization Recovers Every Matrix of Rank at Most r ExactlyResearch Paper

Motivation

Many problems in system identification, collaborative filtering, low-dimensional embedding and model reduction ask for the simplest matrix consistent with a set of linear observations, where "simplest" means "of least rank". Given a linear map $\mathcal A:\mathbb R^{m\times n}\to\mathbb R^p$ and a vector $b\in\mathbb R^p$ , the affine rank minimization problem is

\min_X\ \operatorname{rank}(X)\quad\text{s.t.}\quad \mathcal A(X)=b .

This problem is NP-hard in general: it contains the problem of finding the sparsest solution of a linear system as the special case of diagonal matrices. A standard heuristic, popularized in control by Fazel, Hindi and Boyd, replaces the rank by the nuclear norm $\|X\|_*$ , the sum of the singular values, which is the convex envelope of the rank on the unit ball of the operator norm. The resulting problem is a semidefinite program and can be solved efficiently.

Recht, Fazel and Parrilo (arXiv:0706.4138, SIAM Review 2010) gave the first general conditions under which this heuristic provably returns the minimum-rank solution. Their argument transfers the compressed sensing theory of Candès and Tao (Decoding by linear programming, 2005) and Candès, Romberg and Tao from sparse vectors and the $\ell_1$ norm to low-rank matrices and the nuclear norm. This mission formalizes the paper's deterministic recovery theorem (Section 3).

Setting

Matrices are real $m\times n$ matrices. For matrices $X,Y$ of the same size, $\langle X,Y\rangle=\operatorname{Tr}(X^{\top}Y)=\sum_{i,j}X_{ij}Y_{ij}$ is the trace inner product. With $\sigma_1(X)\ge\sigma_2(X)\ge\dots\ge0$ the singular values of $X$ , the three norms used are the operator norm $\|X\|=\sigma_1(X)$ , the Frobenius norm $\|X\|_F=\sqrt{\langle X,X\rangle}=(\sum_i\sigma_i(X)^2)^{1/2}$ , and the nuclear norm $\|X\|_*=\sum_i\sigma_i(X)$ .

A linear map $\mathcal A:\mathbb R^{m\times n}\to\mathbb R^p$ is given by $p$ measurement matrices $A_1,\dots,A_p$ through $\mathcal A(X)_i=\langle A_i,X\rangle$ ; $\|\mathcal A(X)\|$ is the Euclidean norm of the vector $\mathcal A(X)\in\mathbb R^p$ .

For an integer $r$ , the $r$ -restricted isometry constant $\delta_r(\mathcal A)$ (Definition 3.1) is the smallest $\delta\ge0$ with

(1-\delta)\,\|X\|_F\le\|\mathcal A(X)\|\le(1+\delta)\,\|X\|_F\qquad\text{for every } X \text{ with } \operatorname{rank}X\le r .

Fix a matrix $X_0$ of rank at most $r$ , put $b=\mathcal A(X_0)$ , and consider the nuclear norm minimization problem

X^*:=\arg\min_X\ \|X\|_*\quad\text{s.t.}\quad\mathcal A(X)=b. \tag{3.1}

Formalization targets

Goal: Theorem 3.3

If $r\ge1$ and $\delta_{5r}(\mathcal A)<\tfrac1{10}$ , then $X^*=X_0$ ; precisely,

\forall X\in\mathbb R^{m\times n}:\quad \mathcal A(X)=\mathcal A(X_0)\ \text{ and }\ \|X\|_*\le\|X_0\|_*\ \Longrightarrow\ X=X_0 .

The statement holds for every linear map, every $m,n,p$ and every $X_0$ of rank at most $r$ . The constant $1/10$ is the paper's; the paper notes (p. 14) that its derivation is chosen for simplicity and is not optimal.

Milestones, in the paper's order

Theorem 3.2 (p. 12): if $\delta_{2r}<1$ , then $X_0$ is the only matrix of rank at most $r$ with $\mathcal A(X)=b$ .
(2.1) (p. 6): $\|X\|\le\|X\|_F\le\|X\|_*\le\sqrt r\,\|X\|_F\le r\,\|X\|$ whenever $\operatorname{rank}X\le r$ .
Lemma 2.3 (p. 9): if $AB^{\top}=0$ and $A^{\top}B=0$ , then $\|A+B\|_*=\|A\|_*+\|B\|_*$ .
Lemma 3.4 (pp. 12–13): every $B$ splits as $B=B_1+B_2$ with $\operatorname{rank}B_1\le2\operatorname{rank}A$ , $AB_2^{\top}=0$ , $A^{\top}B_2=0$ and $\langle B_1,B_2\rangle=0$ .
(3.3)–(3.4) (p. 13): for the error $R=R_0+R_c$ of a minimizer, $\|R_c\|_*\le\|R_0\|_*$ .
(3.5)–(3.6) (p. 13): a matrix splits into pairwise orthogonal pieces of rank at most $3r$ whose Frobenius norms, from the second piece on, sum to at most $\|M\|_*/\sqrt{3r}$ .
Monotonicity (p. 12): $\delta_r\le\delta_{r'}$ for $r\le r'$ .
(3.7) (p. 14): $\|\mathcal A(R)\|\ge\big((1-\delta_{5r})-\tfrac9{11}(1+\delta_{3r})\big)\|R_0\|_F$ , with a positive factor whenever $9\delta_{3r}+11\delta_{5r}<2$ .

Significance

Theorem 3.3 is a deterministic certificate: it separates the question "does nuclear norm minimization recover low-rank matrices?" into a property of the measurement map alone, with an absolute constant independent of $m$ , $n$ , $r$ and $p$ . Section 4 of the same paper then shows that random maps with i.i.d. Gaussian or Bernoulli entries satisfy $\delta_{5r}<1/10$ with high probability once $p$ is of order $r(m+n)\log(mn)$ , so a matrix with $mn$ entries is determined by far fewer measurements than entries and is found by a semidefinite program.

The theorem is proved in the paper, and the sparse-vector analogue has been formalized on this platform (HighDimProb.SparseRecovery.rip_implies_exact_recovery, from Vershynin's textbook; CandesTao.Decoding.decoding_by_lp). The matrix version is not formalized. A machine-checked proof needs the basic theory of singular values for rectangular real matrices (the norm comparisons (2.1), additivity of the nuclear norm, the triangle inequality for the nuclear norm, and block decompositions via the singular value decomposition), most of which Mathlib lacks in this form. That infrastructure is reusable for every nuclear-norm result on the platform.

Difficulty

For sparse vectors the analogous proof splits the error vector by its support, and every step is coordinatewise. For matrices there is no common basis: the error $R$ and the target $X_0$ have different singular vectors, and the restricted isometry inequality controls only matrices of low rank. The first obstacle is therefore to split $R$ into a piece of rank at most $2\operatorname{rank}X_0$ and a piece whose row and column spaces are orthogonal to those of $X_0$ , so that the nuclear norm is additive. The second is that the triangle inequality, additivity and the norm chain (2.1) for the nuclear norm are themselves nontrivial statements about singular values. Applying the restricted isometry inequality directly to $R$ fails, because $R$ need not have low rank.

Formalization scope

Matrices are Matrix (Fin m) (Fin n) ℝ; rank is Matrix.rank; transpose is Xᵀ. The norms and the inner product are opNorm, frobeniusNorm, nuclearNorm and traceInner of the published module HighDimStat_MatrixRank_Core, which defines the nuclear norm as the sum of the square roots of the eigenvalues of $X^{\top}X$ .
The map $\mathcal A$ is given by Xs : Fin p → Matrix (Fin m) (Fin n) ℝ and evaluated by observationOp; measNorm Xs X is $\|\mathcal A(X)\|$ .
ripConst Xs r is the infimum of the admissible $\delta\ge0$ ; the set is nonempty and closed, so the infimum is attained. It is defined for every $r$ , not only $1\le r\le m$ , since the goal uses $\delta_{5r}$ . The paper's normalization $m\le n$ is not assumed.
The goal assumes $\operatorname{rank}X_0\le r$ rather than $=r$ (equivalent by monotonicity of $\delta$ ). Its conclusion quantifies over all feasible $X$ with $\|X\|_*\le\|X_0\|_*$ , so it does not depend on a choice of arg min. A formalization that fixes some minimizer unrelated to $b$ , or only asserts the existence of a minimizer equal to $X_0$ , would be trivial and is excluded.
Milestone (3.5)–(3.6) is stated existentially, listing the properties of the singular value blocks that the proof uses, because Mathlib has no ordered rectangular singular value decomposition. Milestone (3.7) makes explicit the orthogonality $\langle R_0,R_1\rangle=0$ that the paper uses silently.

Welcome contributions: a rectangular SVD with ordered singular values, the triangle inequality and duality for nuclearNorm, and the attainment and monotonicity lemmas for ripConst.

Selected references

B. Recht, M. Fazel, P. A. Parrilo, Guaranteed Minimum-Rank Solutions of Linear Matrix Equations via Nuclear Norm Minimization, SIAM Review 52(3), 471–501, 2010. https://doi.org/10.1137/070697835 ; preprint arXiv:0706.4138v1. https://arxiv.org/abs/0706.4138
E. J. Candès, T. Tao, Decoding by Linear Programming, IEEE Trans. Inform. Theory 51(12), 2005. https://doi.org/10.1109/TIT.2005.858979
E. J. Candès, J. Romberg, T. Tao, Stable Signal Recovery from Incomplete and Inaccurate Measurements, Comm. Pure Appl. Math. 59(8), 2006. https://doi.org/10.1002/cpa.20124
M. Fazel, Matrix Rank Minimization with Applications, PhD thesis, Stanford University, 2002.
R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018, §10.5. https://doi.org/10.1017/9781108231596

11 thms3 active usersReviewed

Convex Optimization Machine Learning·Captain: mikedeng1

Pegasos: Primal Estimated Sub-Gradient Solver for SVM: Mini-Batch Pegasos Has Average Instantaneous Objective Within c(1+ln T)/(2λT) of the SVM Optimum'sResearch Paper

Motivation

The support vector machine (SVM) is a linear classifier trained by minimising a regularised hinge loss. For training sets with millions of examples, solving the SVM problem to high accuracy by interior-point or dual decomposition methods is too slow, and what is needed is an algorithm whose cost per iteration does not grow with the number of examples. Pegasos (Primal Estimated sub-GrAdient SOlver for SVM), introduced by Shalev-Shwartz, Singer and Srebro in 2007 and analysed in its final form by Shalev-Shwartz, Singer, Srebro and Cotter in Mathematical Programming (2011, doi:10.1007/s10107-010-0420-4), is a stochastic sub-gradient method on the primal SVM objective with step size $1/(\lambda t)$ . Its analysis showed that the number of iterations needed for accuracy $\epsilon$ is $\tilde O(1/(\lambda\epsilon))$ , independent of the training-set size, and the method became a standard baseline for large-scale linear SVM training.

The analysis rests on a logarithmic-regret bound for online gradient descent on strongly convex functions, due to Hazan, Agarwal and Kale (Machine Learning 69, 2007), which the paper re-proves for non-smooth functions as its Lemma 1 and then applies to the Pegasos iterates in its Theorem 1.

Setting

A training set consists of $m$ examples $(x_i, y_i)$ , $i\in[m]$ , with $x_i\in\mathbb R^n$ and labels $y_i\in\{+1,-1\}$ . The hinge loss of a weight vector $w$ on $(x,y)$ is $\ell(w;(x,y)) = \max\{0,\,1 - y\langle w, x\rangle\}$ . For a regularisation parameter $\lambda>0$ , the SVM objective (Eq. (1)) is

f(w) = \frac\lambda2\|w\|^2 + \frac1m\sum_{i=1}^m \ell(w;(x_i,y_i)),

and $w^\star$ denotes a minimiser of $f$ (Eq. (9)). For a mini-batch $A$ of $k\ge1$ example indices, the instantaneous objective (Eq. (7)) is

f(w;A) = \frac\lambda2\|w\|^2 + \frac1k\sum_{i\in A}\ell(w;(x_i,y_i)).

Mini-batch Pegasos (Fig. 2 of the paper) starts at $w_1 = 0$ . At each round $t = 1, 2, \dots$ it receives a mini-batch $A_t$ , forms the sub-gradient

\nabla_t = \lambda w_t - \frac1k\sum_{i\in A_t}\mathbb 1\bigl[y_i\langle w_t, x_i\rangle < 1\bigr]\,y_i x_i \qquad (8)

of $f(\cdot;A_t)$ at $w_t$ , and sets $w_{t+1} = w_t - \eta_t\nabla_t$ with $\eta_t = 1/(\lambda t)$ . Optionally it then applies the projection step (6), $w_{t+1}\leftarrow\min\{1,(1/\sqrt\lambda)/\|w_{t+1}\|\}\,w_{t+1}$ , which maps $w_{t+1}$ to the closest point of the Euclidean ball of radius $1/\sqrt\lambda$ . A function $g$ is $\lambda$ -strongly convex if $g(w) - \frac\lambda2\|w\|^2$ is convex, and $v$ is a sub-gradient of a convex $g$ at $w_0$ if $g(w) - g(w_0)\ge\langle v, w - w_0\rangle$ for every $w$ .

In the Lean development these objects are svmObj, instObj, subgrad, projBall and run in the namespace Pegasos.Analysis; the hinge loss is UnderstandingML.hingeLoss, sub-gradients are UnderstandingML.IsSubgradient, and " $z$ is the projection of $v$ onto $B$ " is LogRegretOCO.OGD.IsProj B v z.

Formalization targets

Goal: Theorem 1

Assume $\|x_i\|\le R$ for every $i$ , and set $c = (\sqrt\lambda + R)^2$ when the projection step is performed and $c = 4R^2$ when it is not. Then for every sequence of mini-batches and every $T\ge3$ ,

\frac1T\sum_{t=1}^T f(w_t;A_t) \;\le\; \frac1T\sum_{t=1}^T f(w^\star;A_t) + \frac{c\,(1+\ln T)}{2\lambda T}.

The constants are the paper's and are stated exactly; a version with a single constant for both variants, or with an unspecified constant, is a weaker theorem.

Milestones

Eq. (10): for $\lambda$ -strongly convex $g$ with sub-gradient $v$ at $w$ , $\langle w - u, v\rangle\ge g(w) - g(u) + \frac\lambda2\|w-u\|^2$ .
Eq. (11): one projected step satisfies $\langle w_t - u,\nabla_t\rangle\le\frac{\|w_t-u\|^2 - \|w_{t+1}-u\|^2}{2\eta_t} + \frac{\eta_t}2G^2$ (an already-proved platform theorem, stated with a factor 2).
Lemma 1: projected sub-gradient steps $\eta_t = 1/(\lambda t)$ on $\lambda$ -strongly convex $f_t$ with $\|\nabla_t\|\le G$ satisfy $\frac1T\sum f_t(w_t)\le\frac1T\sum f_t(u) + \frac{G^2(1+\ln T)}{2\lambda T}$ for all $u\in B$ .
The vector (8) is a sub-gradient of $f(\cdot;A)$ ; $f(\cdot;A)$ is $\lambda$ -strongly convex; the projection step (6) is the projection onto the ball of radius $1/\sqrt\lambda$ .
The gradient bounds: $\|\nabla_t\|\le\sqrt\lambda + R$ with projection; Eq. (13), $w_{t+1} = \frac1{\lambda t}\sum_{i\le t}v_i$ , and $\|\nabla_t\|\le 2R$ without.
$\|w^\star\|\le 1/\sqrt\lambda$ .

Significance

Theorem 1 is the deterministic core of every guarantee in the paper. Taking expectations over uniformly random mini-batches turns its left side into the expected objective of the iterates and its right side into $f(w^\star)$ plus the rate, which yields the $\tilde O(1/(\lambda\epsilon))$ iteration bound and, via Markov-type arguments, the high-probability bounds of the later sections. Because the bound holds for every sequence of mini-batches, it is also an online-learning regret bound for the sequence of instantaneous objectives.

The result is proved in the paper and is classical. To our knowledge it has no machine-checked proof. Formalizing it produces a verified logarithmic-regret lemma for non-smooth strongly convex sub-gradient descent with an arbitrary closed convex feasible set (the platform currently has the twice-differentiable version with a bounded feasible set), a verified sub-gradient calculus for the regularised hinge loss, and an exact treatment of the Pegasos iteration including both the projected and unprojected variants.

Difficulty

The obvious argument applies Lemma 1 with $B$ the ball of radius $1/\sqrt\lambda$ in both variants and $G$ the sup of $\|\nabla_t\|$ over that ball. This fails twice. Without the projection step the iterates are not confined to that ball, so a separate argument (the closed form (13)) is needed to bound them, and it gives the different constant $4R^2$ . With projection, Lemma 1 requires the comparator $w^\star$ to lie in the ball, and $\|w^\star\|\le1/\sqrt\lambda$ is not implied by the elementary comparison $f(w^\star)\le f(0)\le1$ , which only gives $\|w^\star\|\le\sqrt{2/\lambda}$ ; the paper obtains the sharp radius through duality. In Lemma 1 itself, the telescoping only closes because the step size $1/(\lambda t)$ is matched exactly to the strong-convexity modulus; any off-by-one in the step indexing breaks the cancellation.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), examples are indexed by Fin m, labels are real numbers with the hypothesis $y_i\in\{+1,-1\}$ , and $\lambda>0$ , $k\ge1$ are hypotheses. A mini-batch is a $k$ -tuple Fin k → Fin m: an injective tuple is a subset of size $k$ as in Fig. 2, a non-injective one is the multi-set with repetitions the paper also allows. The theorem is stated for every sequence of mini-batches A : ℕ → Fin k → Fin m; no probability space appears, because the proof never uses that the batches are random. Iterations are 1-based: run … 1 = 0, the step producing $w_{t+1}$ uses $\eta_t = 1/(\lambda t)$ and the batch $A_t$ only, and index 0 is unused. The variant is selected by a Boolean flag, and $c$ depends on it. $w^\star$ is any $w$ with $f(w^\star)\le f(w)$ for all $w$ , minimising the full objective (1), not the instantaneous ones. Strong convexity is the paper's own definition, convexity of $g - \frac\lambda2\|\cdot\|^2$ . At $w = 0$ the projection formula is evaluated with Lean's $a/0 = 0$ , which gives the intended value $0$ . The paper's display (12) has two printed slips (the sign of the $v_t$ term and $x_t$ for $x_i$ ); the Lean states the correct update, and Eq. (13) is correct as printed.

A trivializing formalization is ruled out: the goal is stated for the concrete iteration run, not for an abstract sequence assumed to be sub-gradient steps or projections, and those facts are separate milestones.

A complete development needs the sub-differential sum rule for a convex function plus a quadratic, convexity of the hinge loss, the variational characterisation of the projection onto a ball, the harmonic-sum bound $\sum_{t\le T}1/t\le1+\ln T$ , and a proof of $\|w^\star\|\le1/\sqrt\lambda$ (through duality or a direct optimality argument). Lemma 1 and the sub-gradient lemmas are reusable for any strongly convex stochastic sub-gradient method. Proofs of any milestone, and alternative proofs of the bound on $\|w^\star\|$ that avoid the dual problem, are welcome.

Selected references

S. Shalev-Shwartz, Y. Singer, N. Srebro, A. Cotter, Pegasos: primal estimated sub-gradient solver for SVM, Mathematical Programming Ser. B 127 (2011) 3–30. https://doi.org/10.1007/s10107-010-0420-4
E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007) 169–192. https://doi.org/10.1007/s10994-007-5016-8
S. Shalev-Shwartz, Y. Singer, N. Srebro, Pegasos: primal estimated sub-gradient solver for SVM, ICML 2007. https://doi.org/10.1145/1273496.1273598

15 thms3 active usersReviewed

Completed

Machine Learning Statistics·Captain: mikedeng1

Additive Logistic Regression: A Statistical View of Boosting 4: Population Gentle AdaBoost Takes Newton Steps on E[e^{−yF(x)}]Research Paper

Motivation

Boosting combines many weak classifiers into a strong one by refitting, again and again, to reweighted data. AdaBoost (Freund and Schapire, 1997) and its confidence-rated variant Real AdaBoost (Schapire and Singer, 1999) were introduced through the theory of online learning. Friedman, Hastie and Tibshirani (2000) recast them as stagewise fitting of an additive model $F(x) = \sum_m f_m(x)$ by minimizing the exponential criterion $J(F) = E\,e^{-yF(x)}$ , where $y\in\{-1,1\}$ is the class label. In that view Real AdaBoost minimizes $J(F+f)$ exactly over the new term $f$ at each stage.

The same paper proposes Gentle AdaBoost (Algorithm 4, §4.4), which replaces the exact minimization by a single Newton step. Its increments are bounded, and the authors report that it often matches or beats Real AdaBoost and LogitBoost, especially when numerical stability is an issue. The paper's stagewise view of boosting led on to gradient boosting (Friedman, 2001). This mission formalizes the paper's justification of the algorithm: its population version takes Newton steps on $E\,e^{-yF(x)}$ .

Setting

A feature $x$ ranges over a measurable space $X$ . The label $y$ takes values in $\{-1,1\}$ , and $(x,y)$ has a joint probability law $\nu$ on $X\times\{-1,1\}$ . Conditional expectations given $x$ , written $E(\cdot\mid x)$ , are integrals against the conditional law $\nu(\cdot\mid x)$ of $y$ given $x$ , and $P = P(y=1\mid x)$ .

The algorithm maintains a current additive fit $F : X\to\mathbb R$ , starting from $F = 0$ . For a new term $f(x)$ , the conditional exponential criterion is

J(F(x)+f(x)) = E\big(e^{-y(F(x)+f(x))}\mid x\big),

a function of the real number $f(x)$ for each fixed $x$ .

The weight attached to an observation is $w(x,y) = e^{-yF(x)}$ . The weighted conditional expectation (p. 347) is

E_w\big[g(x,y)\mid x\big] = \frac{E[w(x,y)\,g(x,y)\mid x]}{E[w(x,y)\mid x]},

and $P_w(y=b\mid x) = E_w[1_{[y=b]}\mid x]$ are the weighted class probabilities.

Gentle AdaBoost (Algorithm 4) repeats three steps: fit $f_m$ by weighted least squares of $y$ on $x$ with weights $w$ , update $F \leftarrow F + f_m$ , and update $w \leftarrow w\,e^{-yf_m(x)}$ with renormalization. In the population version the weighted least-squares fit is the weighted conditional mean, so one step is

F(x) \leftarrow F(x) + E_w(y\mid x),\qquad w(x,y) = e^{-yF(x)}.

For comparison with LogitBoost the paper uses the symmetric logistic $p(x) = e^{F(x)}/(e^{F(x)}+e^{-F(x)})$ and the 0/1 response $y^* = (y+1)/2$ .

Formalization targets

Goal: Result 4

For every $x$ , with $s(x) = -E(e^{-yF(x)}y\mid x)$ and $H(x) = E(e^{-yF(x)}\mid x)$ : $s(x)$ is the first derivative of $J(F(x)+f(x))$ at $f(x)=0$ , $H(x)$ is the second derivative, $H(x)>0$ , and

F(x) + E_w(y\mid x) = F(x) - \frac{s(x)}{H(x)}.

This is the paper's Result 4, "the Gentle AdaBoost algorithm (population version) uses Newton steps for minimizing $Ee^{-yF(x)}$ ", in the precise form its Derivation gives.

Milestones

The Derivation's derivatives:

\frac{\partial J}{\partial f(x)}\Big|_{0} = -E(e^{-yF(x)}y\mid x),\qquad \frac{\partial^2 J}{\partial f(x)^2}\Big|_{0} = E(e^{-yF(x)}\mid x).

The Newton update: $F(x) + E(e^{-yF(x)}y\mid x)/E(e^{-yF(x)}\mid x) = F(x) + E_w(y\mid x)$ .
The update as weighted class probabilities: $E_w(y\mid x) = P_w(y=1\mid x) - P_w(y=-1\mid x)$ .
The range: $E_w(y\mid x) \in [-1,1]$ .
Display (37):

\frac{E(e^{-yF(x)}y\mid x)}{E(e^{-yF(x)}\mid x)} = \frac{e^{-F(x)}P - e^{F(x)}(1-P)}{e^{-F(x)}P + e^{F(x)}(1-P)} = \frac{P-p(x)}{(1-p(x))P + p(x)(1-P)} \in [-1,1].

Display (38): the LogitBoost increment $\tfrac12 E(y^*-p(x)\mid x)/E(p(x)(1-p(x))\mid x)$ equals $\tfrac12 (P-p(x))/(p(x)(1-p(x)))$ .

Significance

The result. Result 4 places Gentle AdaBoost alongside LogitBoost (Result 3) as a Newton method. Real AdaBoost (Result 2) and Gentle AdaBoost minimize the same criterion, but one solves the stagewise problem exactly and the other takes one Newton step. Displays (37) and (38) then put Gentle AdaBoost and LogitBoost in the same coordinates $P$ and $p(x)$ . The two updates are close when $p(x)\approx \tfrac12$ . LogitBoost's update can be unbounded as $p(x)$ approaches $0$ or $1$ , while Gentle AdaBoost's always stays in $[-1,1]$ . This is the paper's explanation for the stability of Gentle AdaBoost.

Formalizing it. The result is proved on the page by direct calculation. No machine-checked version is known to exist. The mission produces a formal account of the population algorithm on an arbitrary joint law, through Mathlib's disintegration of a measure on $X\times\{-1,1\}$ , and of the Newton-step identity. It also gives a reusable treatment of the paper's weighted conditional expectation $E_w$ in the conditional-kernel language. The same objects appear in the other missions of this series (Real AdaBoost, LogitBoost).

Difficulty

The calculus on the page is short. The work is in the setting. "Differentiate the criterion with respect to $f(x)$ " has to mean differentiating an integral against the conditional law of $y$ given $x$ with respect to a parameter, with the derivative established, not read off a formula. A plain derivative equation proves nothing at a point where the function is not differentiable. The second derivative needs the first derivative as a function of $t$ , not only its value at $0$ . The Newton step divides by $H(x)$ , so its positivity must be established before the identity has content. Finally, (37) requires recovering $P(y=-1\mid x) = 1-P$ from the conditional law being a probability measure, and the second equality in (37) holds only for the symmetric logistic.

Formalization scope

Labels are Bool (true for $y=1$ , false for $y=-1$ ); $y$ is sgn b and $y^*$ is ystar b. The joint law is ν : Measure (X × Bool) with [IsProbabilityMeasure ν], and $E(\cdot\mid x)$ is the Bochner integral against ν.condKernel x, a probability measure on the two-point type. Every statement holds for every $x$ . No almost-everywhere qualifier, integrability or measurability hypothesis is needed, and none is added. The kernel is unique only almost everywhere, and the statements hold for the chosen version. They use only the fact that it is a Markov kernel. The definitions file fixes the conditional criterion condCritAt, the weighted conditional expectation wCondExp with weight $e^{-yF(x)}$ , the weighted class probabilities wProb, the population step gentleStep, and the symmetric logistic symLogistic. All of these are written exactly as on the page.

Derivatives are HasDerivAt statements. The second derivative is the derivative at $0$ of an explicit first-derivative function, which is itself shown to be the derivative at every point. $H(x)>0$ is a conclusion of the goal, never a hypothesis. Several formalizations would trivialize the claims and are ruled out. The criterion is the integral against the conditional law, not a closed form $\eta e^{-F-t}+(1-\eta)e^{F+t}$ in a free parameter $\eta$ . No bare deriv equation and no division by an unproved nonzero quantity is used. The logistic is the symmetric $e^{F}/(e^{F}+e^{-F})$ , not $1/(1+e^{-F})$ , which differs by a factor $2$ in $F$ and makes (37) false. The sample version of Algorithm 4 (trees, terminal-node averages) is not formalized.

Welcome contributions: proofs of the milestones, general lemmas on differentiating integrals over finite label spaces with respect to a parameter, and lemmas connecting condKernel on Bool with the closed forms in $P$ .

Selected references

J. Friedman, T. Hastie, R. Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28(2):337–407, 2000. https://doi.org/10.1214/aos/1016218223
Y. Freund, R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, J. Comput. Syst. Sci. 55(1):119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
R. E. Schapire, Y. Singer, Improved boosting algorithms using confidence-rated predictions, Mach. Learn. 37(3):297–336, 1999. https://doi.org/10.1023/A:1007614523901
J. Friedman, Greedy function approximation: a gradient boosting machine, Ann. Statist. 29(5):1189–1232, 2001. https://doi.org/10.1214/aos/1013203451

10 thms3 active usersReviewed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Consumer Returns Policies and Supply Chain Performance 2: Under Consumer Returns, the Differentiated Buy-Back with b − l = s Coordinates the Supply Chain and Gives the Retailer a Share φResearch Paper

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

Under a standard buy-back the retailer's optimal refund is $r^* = b$ (Sec. 5.1, p. 15).
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).
Under (16)–(18), $w - b = \phi(c-s)$ and $E\max(V,b-l) - b = \phi[E\max(V,s)-s]$ ((32)–(33)).
At $(E\max(V,s), q, s)$ the retailer earns $\phi\,\Pi_T$ ((34)–(39)).
Retailer plus manufacturer profit under direct returns is $\Pi_T$ (Sec. 5.3, p. 17).
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$ .
Proposition 5: the sales rebate $u = \frac{E\max(V,s)-s}{c-s}(w-c)$ makes the chain optimum a retailer optimum.
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

12 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Probability·Captain: mikedeng1

Convex Quadratic and Semidefinite Programming Relaxations in Scheduling I: Randomized Rounding of the Convex Quadratic Relaxation (CQP′) Is Within 3/2 for R | | Σ wⱼCⱼResearch Paper

Motivation

Scheduling jobs on unrelated parallel machines to minimize the total weighted completion time, the problem written $R\,|\,|\sum w_jC_j$ in the three-field notation, is one of the basic NP-hard models of machine scheduling. Each job may take a different time on each machine, as when heterogeneous processors, plants or crews serve the same pool of tasks, and the objective rewards finishing important jobs early. For a single machine the problem is solved exactly by Smith's ratio rule (Smith, 1956). With several unrelated machines the problem is strongly NP-hard and the question is how close to the optimum a polynomial-time algorithm can come.

Timeline of the guarantees for $R\,|\,|\sum w_jC_j$ :

Lenstra, Shmoys and Tardos (1990) gave an LP-based 2-approximation for the makespan on unrelated machines; their assignment variables $a_{ij}$ are the ones used here.
Hall, Schulz, Shmoys and Wein (1997) gave constant-factor approximations for $\sum w_jC_j$ on unrelated machines via time-indexed and interval-indexed LP relaxations.
Schulz and Skutella (conference version 1999, journal 2002) obtained $3/2+\varepsilon$ by randomized rounding of a time-indexed LP.
Skutella (J. ACM 2001), the paper of this mission, gave a convex quadratic relaxation in assignment variables alone and a $3/2$ -approximation by randomized rounding, with a short analysis.
Bansal, Srinivasan and Svensson (2016) improved $3/2$ to $3/2-\varepsilon$ for a small constant $\varepsilon>0$ ; later work lowered the constant further.

Setting

There are $n$ jobs $j\in J$ and $m$ machines $i$ . Job $j$ has a weight $w_j\ge 0$ and a processing time $p_{ij}>0$ on machine $i$ . A schedule assigns each job to one machine and orders the jobs on every machine; the completion time $C_j$ of a job is the time at which it finishes when each machine works without idle time.

For a fixed assignment, Smith's ratio rule orders each machine optimally. Fix for each machine $i$ the total order $j\prec_i k$ iff $w_j/p_{ij}>w_k/p_{ik}$ , ties broken by index. Under an assignment $\sigma$ the completion time of $j$ is

C_j(\sigma)=p_{\sigma(j)j}+\sum_{k\prec_{\sigma(j)}j,\ \sigma(k)=\sigma(j)}p_{\sigma(j)k},

and the problem is to minimize $\mathrm{val}(\sigma)=\sum_jw_jC_j(\sigma)$ over all assignments.

With $a_{ij}\in\{0,1\}$ indicating that $j$ runs on $i$ , the problem is the integer quadratic program (IQP) with objective

Z_{QP}(a)=c^Ta+\tfrac12a^TDa,\qquad c_{ij}=w_jp_{ij},

where $D$ is symmetric with entry $w_jp_{ik}$ at $((i,j),(i,k))$ for $k\prec_ij$ and zero across machines and on the diagonal. Relaxing $a_{ij}\in\{0,1\}$ to $a\ge 0$ with $\sum_ia_{ij}=1$ gives (QP). Raising the diagonal gives the convex program (CQP), with objective $Z_{CQP}(a)=\tfrac12c^Ta+\tfrac12a^T(D+\operatorname{diag}(c))a$ . Adding the lower bound $c^Ta$ gives (CQP′):

\min Z\quad\text{s.t.}\quad \textstyle\sum_ia_{ij}=1,\ \ a\ge 0,\ \ Z\ge Z_{CQP}(a),\ \ Z\ge c^Ta .

Randomized rounding of a fractional $\bar a$ sends job $j$ to machine $i$ with probability $\bar a_{ij}$ , the choices being pairwise independent across jobs, and then orders every machine by $\prec_i$ .

Formalization targets

Goal: (CQP′) is a relaxation, and rounding loses at most 3/2

For every instance with $p>0$ , $w\ge 0$ :

\forall\sigma:\ (a^\sigma,\ \mathrm{val}(\sigma))\ \text{is feasible for (CQP′)},

\forall(\bar a,Z)\ \text{feasible for (CQP′)}:\quad \mathbb E\Bigl[\sum_jw_jC_j\Bigr]\le\tfrac32 Z .

The first part makes $Z^*_{CQP'}$ a lower bound on the optimum. The second is Lemma 2.8. Together they are Corollary 2.9 and the value guarantee of the $3/2$ -approximation.

Milestones

In attack order:

Lemma 2.2: $\mathbb E[C_j]=\sum_i(\Pr[j\mapsto i]p_{ij}+\sum_{k\prec_ij}\Pr[j,k\mapsto i]p_{ik})$ for any random assignment.
Theorem 2.1: rounding a feasible $\bar a$ has expected value exactly $Z_{QP}(\bar a)$ .
Corollary 2.3: (IQP) and (QP) have the same optimum.
The positive semidefiniteness of $D+\operatorname{diag}(c)$ and Lemma 2.4: $a\mapsto(1-\gamma)c^Ta+\tfrac12a^T(D+2\gamma\operatorname{diag}(c))a$ is convex for all instances iff $\gamma\ge\tfrac12$ .
The identity $Z_{QP}=Z_{CQP}+\tfrac12(c^Ta-a^T\operatorname{diag}(c)a)$ and Theorem 2.6 a), the factor $2$ for (CQP).
Lemma 2.8, the integrality step of Theorem 2.10, and Corollary 2.11, the bound $(1+c^T\bar a/(2Z))Z$ .

Significance

The result gives a $3/2$ -approximation for $R\,|\,|\sum w_jC_j$ from a relaxation with only $mn$ variables, without time indexing, so its size does not depend on the processing times. The same convexification, adapted to time slots, yields the factor 2 with release dates (§3 of the paper). The equality of Theorem 2.1 makes the analysis exact: the loss of rounding is exactly the gap between $Z_{QP}$ and the convex objective. The relaxation also bounds the power of preemption (§4), and for identical machines it connects scheduling to Max- $k$ -Cut (§6).

All these results are proved in the paper; none is known to be formalized. A formal development adds:

a checked model of Smith-sequenced assignment schedules;
the expectation calculus for pairwise independent rounding;
the positive-semidefiniteness argument of Lemma 2.4;
a precise statement of what the $3/2$ guarantee says when complexity is set aside.

Difficulty

Two steps resist the obvious approach.

Positive semidefiniteness. $D$ alone is indefinite: two jobs with unit data give the block $\left(\begin{smallmatrix}0&1\\1&0\end{smallmatrix}\right)$ . Positive semidefiniteness of $D+\operatorname{diag}(c)$ holds only because the jobs on each machine are ordered by Smith's ratio. A generic matrix argument that ignores this ordering fails, and the "only if" half of Lemma 2.4 needs a specific family of instances.

Exact expectations under pairwise independence. Theorem 2.1 is an equality that uses only the one- and two-job marginals. A proof that silently assumes full independence of the choices proves a different statement. A proof that drops the product condition on pairs is false: with correlated choices the expected value differs from $Z_{QP}$ .

Formalization scope

Jobs and machines are Fin n and Fin m; vectors in $\mathbb R^{mn}$ are functions on Fin m × Fin n and $D$ is a Matrix over that type. The order $\prec_i$ is cross-multiplied ( $w_jp_{ik}>w_kp_{ij}$ , or equality and $j<k$ ), which equals the page's ratio definition because $p>0$ .

Standing assumptions of p. 2 are hypotheses of every theorem: $p_{ij}>0$ and $w_j\ge0$ . Hypotheses added relative to the page:

Corollary 2.11 assumes $Z>0$ , which its fraction presupposes;
the integrality step of Theorem 2.10 assumes integral $p$ and $w$ , as the page's proof does.

Optimum. The scheduling optimum $Z^*$ is the minimum of $\mathrm{val}$ over assignments, by Smith's rule (p. 7, cited by the paper, not reproved). "Within a factor $\alpha$ of the optimum" is stated as a bound against the value of every assignment, so no optimum is presupposed.

Rounding. Randomized rounding is any nonnegative weight $\mu$ of total mass 1 on assignments, with $\Pr_\mu[j\mapsto i]=\bar a_{ij}$ and $\Pr_\mu[j\mapsto i,\,k\mapsto h]=\bar a_{ij}\bar a_{hk}$ for $j\ne k$ . The product weight satisfies this.

Not formalized. Polynomial running time, solvability of (CQP′) within additive error $\varepsilon$ (ellipsoid method), and derandomization by conditional probabilities. Theorem 2.10 is formalized as the existence of an outcome in the support of the rounding with the $3/2$ guarantee.

Trivializing formalization ruled out. A bound $\mathbb E\le\tfrac32Z$ for an arbitrary number $Z$ says nothing about schedules. The goal therefore also states that every schedule is feasible for (CQP′) at its own value, so $Z$ is a genuine lower bound on the optimum.

Contributions welcome. A complete development needs:

linearity of expectation over a finite weight on assignments;
the computation of Lemma 2.2;
a positive-semidefiniteness criterion via principal minors or a direct sum-of-squares decomposition of $a^T(D+\operatorname{diag}(c))a$ ;
convexity of quadratic forms with PSD matrices.

The rounding calculus and the PSD lemma are reusable for §§3–4 of the same paper. Alternative proofs of Lemma 2.4 are 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
J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46, 1990. https://doi.org/10.1007/BF01585745
L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Mathematics of Operations Research 22(3), 1997. https://doi.org/10.1287/moor.22.3.513
A. S. Schulz, M. Skutella, Scheduling unrelated machines by randomized rounding, SIAM Journal on Discrete Mathematics 15(4), 2002. https://doi.org/10.1137/S0895480199357078
N. Bansal, A. Srinivasan, O. Svensson, Lift-and-round to improve weighted completion time on unrelated machines, STOC 2016. https://doi.org/10.1145/2897518.2897572

12 thms3 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

A Combinatorial Algorithm Minimizing Submodular Functions in Strongly Polynomial Time I: Schrijver's Algorithm Returns a Minimizer of f After at Most |V|⁶ IterationsResearch Paper

Motivation

Minimizing a submodular set function is one of the central tractable problems of combinatorial optimization. Minimum cuts in graphs and hypergraphs, matroid intersection and partition, the rank of a matroid union, and many problems in facility location, image segmentation and machine learning are special cases or subroutines of it. The question is algorithmic: given only a value oracle for $f$ , find a set $U$ with $f(U) = \min_W f(W)$ using a number of operations bounded by a polynomial in $|V|$ alone, independent of the size of the values of $f$ (strongly polynomial).

Timeline.

1981. Grötschel, Lovász and Schrijver showed with the ellipsoid method that submodular functions can be minimized in strongly polynomial time (Combinatorica 1, 1981). The method is not combinatorial.
1985. Cunningham gave a combinatorial pseudo-polynomial algorithm for submodular function minimization (Combinatorica 5, 1985).
1999–2000. Two combinatorial strongly polynomial algorithms appeared independently: Iwata, Fleischer and Fujishige (J. ACM 48, 2001), and Schrijver, the paper of this mission (J. Combin. Theory Ser. B 80, 2000).

Schrijver's algorithm is the one usually taught. Its proof uses only the greedy vectors of $f$ , a reachability digraph and a lexicographic potential.

Setting

Let $V = \{1,\dots,n\}$ and let $f$ be a real function on all subsets of $V$ that is submodular:

f(Y) + f(Z) \ge f(Y\cap Z) + f(Y\cup Z) \qquad (Y, Z \subseteq V),

normalized so that $f(\emptyset)=0$ . For $x \in \mathbb R^V$ and $U \subseteq V$ write $x(U) = \sum_{v\in U} x(v)$ . The base polytope is $B_f = \{x \in \mathbb R^V : x(U) \le f(U)\ \forall U,\ x(V) = f(V)\}$ .

For a total order $\prec$ on $V$ let $v_\prec = \{u : u \prec v\}$ . The greedy vector of $\prec$ is $h^\prec(v) = f(v_\prec\cup\{v\}) - f(v_\prec)$ . A lower ideal of $\prec$ is a set closed under taking $\prec$ -smaller elements. The interval $(s,t]_\prec$ is $\{v : s \prec v \preceq t\}$ . For $s \prec u$ , the order $\prec^{s,u}$ is obtained from $\prec$ by moving $u$ to the position just before $s$ . The vector $\chi^u$ is the incidence vector of $u$ .

The algorithm keeps a point $x = \lambda_1 h^{\prec_1} + \dots + \lambda_k h^{\prec_k}$ with $\lambda_i > 0$ and $\sum_i \lambda_i = 1$ ; initially $x = h^\prec$ for an arbitrary order. It forms the digraph $D = (V, A)$ , where $A = \{(u,v) : u \prec_i v \text{ for some } i\}$ , and the sets $P = \{x > 0\}$ and $N = \{x < 0\}$ .

Case 1: $D$ has no path from $P$ to $N$ . The algorithm returns the set $U$ of vertices that can reach $N$ .
Case 2: there is such a path. Let $d(v)$ $d (v)$ be the distance from $P$ $P$ to $v$ $v$ in $D$ $D$ . The algorithm picks $t \in N$ $t \in N$ maximizing $(d(t), t)$ $(d (t), t)$ , then the largest $s$ $s$ with $(s,t)\in A$ $(s, t) \in A$ and $d(s) = d(t)-1$ $d (s) = d (t) - 1$ , then an order $\prec_1$ $≺_{1}$ maximizing $|(s,t]_{\prec_1}|$ $∣ (s, t]_{≺_{1}} ∣$ .
- It finds $\delta \ge 0$ with $h^{\prec_1} + \delta(\chi^t - \chi^s)$ a convex combination of the $h^{\prec_1^{s,u}}$ , $u \in (s,t]_{\prec_1}$ .
- It moves $x$ toward $y = x + \lambda_1\delta(\chi^t-\chi^s)$ as far as $x(t) \le 0$ allows.
- It reduces the new convex decomposition to at most $|V|$ terms, dropping $\prec_1$ if $x'(t) < 0$ .

Formalization targets

Goal: correctness, well-definedness and the iteration bound

For every submodular $f$ with $f(\emptyset)=0$ :

\text{(i) in Case 1, } f(U) \le f(W)\ \forall W \subseteq V;\quad \text{(ii) every Case 2 state has a successor};\quad \text{(iii) every run has } m \le |V|^6 \text{ iterations}.

Part (iii) is the opening claim of §5 (p. 352), and part (i) is display (16) (p. 351). Part (ii) states that the description of §4 can always be carried out, and it keeps (iii) from holding vacuously.

Milestones

In order: the diminishing-returns inequality (9); $h^\prec(U) = f(U)$ on lower ideals and $h^\prec \in B_f$ (§2); the comparison (8) of $h^{\prec^{s,u}}$ with $h^\prec$ ; the subroutine (12); the Case 1 certificate (16); existence of a Case 2 iteration (§4, p. 352); the location (22) of new arcs; monotonicity (20) of distances; and the lexicographic decrease (21) of $(d(t), t, s, \alpha, \beta)$ while $d$ stays fixed.

Significance

The result. The theorem gives a submodular minimizer after a number of iterations bounded by a polynomial in $|V|$ . Each iteration makes polynomially many oracle calls and arithmetic operations, so the algorithm is strongly polynomial. The same exchange-and-potential scheme underlies later improvements (Fleischer–Iwata's push-relabel variant, Iwata–Orlin, Orlin's $O(n^5)$ bound). Section 6 of the paper, the companion mission, transfers the result to submodular functions on ring families.

Formalizing it. The result is proved and has been in textbooks for twenty years. It has no machine-checked proof that we know of, in Lean or elsewhere, and Mathlib has no submodular minimization. A complete development yields a verified correctness and termination proof for a nontrivial combinatorial algorithm on the base polytope. It also yields reusable facts about greedy vectors and lower ideals, and a worked example of a lexicographic-potential termination argument.

Difficulty

Correctness (16) is short once $h^\prec(U) = f(U)$ on lower ideals is available. The difficulty is termination. A single iteration can increase $x$ at $t$ and decrease it at $s$ , and it adds new orders and so new arcs. Neither $|N|$ nor $x(N)$ need improve monotonically, and the obvious potentials fail. The argument needs the precise structure of the new arcs (22): every new arc lies inside the interval $[s,t]$ of $\prec_1$ , and that gives both the monotonicity of distances (20) and the strict lexicographic decrease (21). The choice rule for $t$ and $s$ ("largest") is what makes (21) hold. An arbitrary choice can cycle. Well-definedness also takes work: it combines (12) with a Carathéodory reduction over the hyperplane $x(V) = f(V)$ .

Formalization scope

Ground set and values. $V$ is Fin n and subsets are Finset (Fin n). Values are real; the paper allows any ordered field. "Largest" in the choice of $t$ and $s$ is the order of Fin n.
Orders and states. A total order is a permutation $\sigma$ read as a position map: $u \prec v$ iff $\sigma(u) < \sigma(v)$ . The order $\prec^{s,u}$ is characterized relationally (IsMoved). A state is a list of (order, weight) pairs.
Distances. Distances take values in $\mathbb N \cup \{\infty\}$ , with $\infty$ for unreachable vertices.
Standing assumptions. Submodularity (the platform definition NonmonotoneSubmod.Shared.Submodular) and $f(\emptyset) = 0$ are the paper's standing assumptions of §2 and §4. Milestones that do not need $f(\emptyset)=0$ omit it.
Iterations as a relation. An iteration is a relation Step that admits every choice the paper leaves open: any subroutine output $\delta$ , any maximizing index, and any Carathéodory reduction. The reduced decomposition may only use orders $\prec_i$ ( $i \ne 1$ ), each $\prec_1^{s,u}$ at most once, and $\prec_1$ only when $x'(t) = 0$ .
Not formalized. The value oracle, "strongly polynomial time" and the number of oracle calls are not formalized, because there is no machine model. Only the iteration count is.
No trivial reading. A Step relation that is never satisfiable would make the bound vacuous. Part (ii) of the goal rules this out, and the goal does not mention $d$ , $\alpha$ , $\beta$ or the matrix of §3.
Contributions welcome. Proofs of the milestones, general lemmas on greedy vectors and lower ideals (reusable for any base-polytope development), and a Carathéodory lemma for convex combinations in an affine hyperplane.

Selected references

A. Schrijver, A combinatorial algorithm minimizing submodular functions in strongly polynomial time, J. Combin. Theory Ser. B 80 (2000) 346–355. https://doi.org/10.1006/jctb.2000.1989
S. Iwata, L. Fleischer, S. Fujishige, A combinatorial strongly polynomial algorithm for minimizing submodular functions, J. ACM 48 (2001) 761–777. https://doi.org/10.1145/502090.502096
M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981) 169–197. https://doi.org/10.1007/BF02579273
W. H. Cunningham, On submodular function minimization, Combinatorica 5 (1985) 185–192. https://doi.org/10.1007/BF02579361
J. B. Orlin, A faster strongly polynomial time algorithm for submodular function minimization, Math. Program. 118 (2009) 237–251. https://doi.org/10.1007/s10107-007-0189-2

12 thms3 active usersReviewed

Completed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Convex Quadratic and Semidefinite Programming Relaxations in Scheduling V: 3-Occurrence Max3Sat L-Reduces to R | rⱼ | Σ Cⱼ with Constants 32 and 1Research Paper

Motivation

The scheduling problem $R\,|\,r_j\,|\sum C_j$ asks for a nonpreemptive schedule of jobs on unrelated parallel machines, each job with a machine-dependent processing time and a release date, so that the total completion time is minimal. It is NP-hard, and the question that remains is how well it can be approximated in polynomial time. Positive results include the 2-approximation of Skutella (J. ACM 2001), based on a convex quadratic relaxation. This mission covers the negative side, from §7 of the same paper: the problem has no polynomial-time approximation scheme unless P = NP.

The standard route to such a statement is an L-reduction (Papadimitriou and Yannakakis 1991) from a problem already known to be MaxSNP-hard. MaxSNP-hard problems have no approximation scheme unless P = NP, by the PCP theorem (Arora et al. 1998).

Timeline.

1991: Papadimitriou and Yannakakis define MaxSNP and L-reductions, and show that MAX3SAT with a bounded number of occurrences per variable is MaxSNP-complete.
1998: Hoogeveen, Schuurman and Woeginger prove that $R\,|\,|\sum w_jC_j$ and $R\,|\,r_j\,|\sum C_j$ are MaxSNP-hard, by a reduction from a MaxSNP-hard variant of 3-dimensional matching.
2001: Skutella (§7, pp. 32–33) gives a shorter reduction from 3-OCCURRENCE MAX3SAT, the variant of MAX3SAT in which every variable occurs at most three times (MaxSNP-hard, see Ausiello et al. 1999, Corollary 8.15).

Setting

An instance $I$ of 3-OCCURRENCE MAX3SAT has $n$ variables and $m$ clauses. Each clause is a set of one to three literals (a variable $x$ or its negation $\neg x$ ), and each variable occurs at most three times in total. A truth assignment $t$ gives each variable the value true or false and satisfies a clause when one of the clause's literals is true. $\#(t)$ denotes the number of satisfied clauses, and $\mathrm{OPT}_{\mathrm{SAT}}(I)=\max_t \#(t)$ .

The scheduling instance $R(I)$ has $n+m$ jobs and $2n$ machines.

Every variable $x$ has a true machine and a false machine, and one v-job. The v-job is released at time $0$ , has processing time $4$ on the two machines of $x$ , and cannot run anywhere else.
Every clause $c$ has one c-job, released at time $3$ , with processing time $0$ . It may run on the false machine of $x$ when $x$ occurs in $c$ , on the true machine of $x$ when $\neg x$ occurs in $c$ , and nowhere else.

A schedule $S$ gives every job $j$ a machine and a start time $S_j\ge r_j$ , with no two jobs on one machine overlapping. Its value is the total completion time $\mathrm{VAL}(S)=\sum_j (S_j+p_j)$ . The truth assignment $\mathrm{SAT}(S)$ sets $x$ true exactly when the v-job of $x$ runs on the true machine. $\mathrm{OPT}_{\mathrm{SCH}}(R(I))$ is the minimum of $\mathrm{VAL}$ over feasible schedules.

Formalization targets

Goal: the L-reduction inequalities (Lemma 7.1 b) and the proof of Theorem 7.2, p. 33)

$R(I)$ has an optimal schedule $S_0$ , and

\mathrm{VAL}(S_0)=4n+4m-\mathrm{OPT}_{\mathrm{SAT}}(I)\le 32\,\mathrm{OPT}_{\mathrm{SAT}}(I),\qquad \mathrm{OPT}_{\mathrm{SAT}}(I)-\#(\mathrm{SAT}(S))\le\mathrm{VAL}(S)-\mathrm{VAL}(S_0)

for every feasible schedule $S$ . These are the two conditions of an L-reduction, with constants $\alpha=32$ and $\beta=1$ .

Milestones

Lemma 7.1 a) (p. 32): $\#(\mathrm{SAT}(S))\ge 4n+4m-\mathrm{VAL}(S)$ for every feasible $S$ .
Lemma 7.1 b) (p. 33): $\mathrm{OPT}_{\mathrm{SCH}}(R(I))=4n+4m-\mathrm{OPT}_{\mathrm{SAT}}(I)$ .
The two counting facts of the proof of Theorem 7.2: $\mathrm{OPT}_{\mathrm{SAT}}(I)\ge m/2$ and $n\le 3m$ .
The first L-reduction condition: $\mathrm{OPT}_{\mathrm{SCH}}(R(I))\le 12m+4m\le 32\,\mathrm{OPT}_{\mathrm{SAT}}(I)$ .
The second L-reduction condition: $\mathrm{OPT}_{\mathrm{SAT}}(I)-\#(\mathrm{SAT}(S))\le\mathrm{VAL}(S)-\mathrm{OPT}_{\mathrm{SCH}}(R(I))$ .

Significance

The result. The two inequalities are what an L-reduction requires. Combined with the MaxSNP-hardness of 3-OCCURRENCE MAX3SAT, they show that $R\,|\,r_j\,|\sum C_j$ is MaxSNP-hard (Theorem 7.2, due to Hoogeveen, Schuurman and Woeginger), and therefore has no polynomial-time approximation scheme unless P = NP. Together with the constant-factor algorithms of the earlier sections of the paper, this places the problem in APX but outside PTAS. The identity of Lemma 7.1 b) is exact, so the reduction transfers solutions in both directions with no loss beyond the affine shift $k\mapsto 4n+4m-k$ .

Formalizing it. The result is proved, on paper, by both the 1998 and the 2001 reductions. As far as the platform's corpus shows, neither is machine-checked. This mission produces a checked version of the combinatorial core of Skutella's reduction: the exact relation between optimal schedules of $R(I)$ and optimal truth assignments of $I$ , and the two L-reduction constants. A Lean model of 3-OCCURRENCE MAX3SAT and of nonpreemptive schedules with release dates and machine eligibility is a by-product.

Difficulty

The obvious argument is the paper's intuition: given a truth assignment, a c-job can start at time $3$ without conflicting with a v-job exactly when its clause is satisfied. That is not enough for Lemma 7.1 a), which concerns every feasible schedule. In an arbitrary schedule a v-job may be delayed so that c-jobs of unsatisfied clauses run before it on its machine, and v-jobs and c-jobs may start at arbitrary real times. To compare such a schedule with a normalized one, its total completion time has to be bounded from below by $4n+4m-\#(\mathrm{SAT}(S))$ . The bound depends on the occurrence limit of three, which caps how many c-jobs can share a machine with a given v-job; without that limit Lemma 7.1 a) is false. Lemma 7.1 b) also needs the existence of an optimal schedule, which the paper takes for granted.

Formalization scope

Variables and clauses are Fin n and Fin m; here $n$ and $m$ count variables and clauses, not jobs and machines as in the rest of the paper. A literal is a pair (x, b) with b = true for $x$ and b = false for $\neg x$ , and a clause is a Finset of literals. Jobs are Fin n ⊕ Fin m and machines Fin n × Bool. Infinite processing times are encoded by an eligibility relation. Start times are real numbers, and $\mathrm{VAL}$ is a real number; $\#$ and $\mathrm{OPT}_{\mathrm{SAT}}$ are natural numbers cast to the reals, so no natural-number subtraction occurs. $\mathrm{OPT}_{\mathrm{SCH}}$ is never a primitive: statements assert, or assume, a feasible schedule that is no worse than every feasible schedule.

Two conventions are fixed that the page leaves implicit:

Every clause has between one and three literals. An empty clause would leave its c-job with no machine, so $R(I)$ would have no schedule, and "at least $m/2$ " would fail.
Every variable occurs at least once. The bound $n\le 3m$ , and with it the constant $32$ , needs this: a variable that occurs nowhere adds $4$ to $\mathrm{OPT}_{\mathrm{SCH}}$ and nothing to $\mathrm{OPT}_{\mathrm{SAT}}$ .

Zero-length jobs need a precise non-overlap rule. Two distinct jobs on one machine must satisfy $S_j+p_j\le S_k$ or $S_k+p_k\le S_j$ . Under this rule a c-job at time $3$ conflicts with a v-job running over $[0,4)$ , but several c-jobs may share a start time. Reading jobs as half-open intervals $[S_j,S_j+p_j)$ would let a zero-length c-job sit inside a v-job, so every clause would count as satisfied: that formalization is ruled out.

Not formalized: MaxSNP, MaxSNP-hardness and Theorem 7.2's statement itself; the definition of an L-reduction as a pair of polynomial-time maps; the polynomial running time of $R$ and $\mathrm{SAT}$ ; the weighted variant for $R\,|\,|\sum w_jC_j$ in the last paragraph of §7, which the paper does not prove. Contributions are welcome on the counting facts, on a normal form for schedules of $R(I)$ (v-jobs at time $0$ , c-jobs at time $3$ or $4$ ), and on the existence of optimal schedules.

Selected references

M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, J. ACM 48(2), 206–242, 2001. https://doi.org/10.1145/375827.375840
J. A. Hoogeveen, P. Schuurman, G. J. Woeginger, Non-approximability results for scheduling problems with minsum criteria, IPCO 1998, LNCS 1412, 353–366. https://doi.org/10.1007/3-540-69346-7_27
C. H. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. System Sci. 43(3), 425–440, 1991. https://doi.org/10.1016/0022-0000(91)90023-X
G. Ausiello, P. Crescenzi, G. Gambosi, V. Kann, A. Marchetti-Spaccamela, M. Protasi, Complexity and Approximation, Springer, 1999. https://doi.org/10.1007/978-3-642-58412-1
S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3), 501–555, 1998. https://doi.org/10.1145/278298.278306

7 thms3 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Conditional Value-at-Risk for General Loss Distributions: β-CVaR Is min_α F_β(x, α), Attained on the Interval from β-VaR to Upper β-VaRResearch Paper

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

The note after Definition 3: $\Psi_\beta(x,\cdot)$ is a distribution function, so the $\beta$ -tail distribution exists; its mean is finite.
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.
$F_\beta(x,\cdot)$ is finite and convex.
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)$ .
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.
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

9 thms3 active usersReviewed

Completed

Machine Learning Statistics·Captain: mikedeng1

Additive Logistic Regression: A Statistical View of Boosting 3: Population LogitBoost Takes Newton Steps on the Binomial Log-LikelihoodResearch Paper

Motivation

Boosting combines many weak classifiers into a strong one by refitting, round after round, to a reweighted version of the training data. Freund and Schapire's AdaBoost was introduced as a procedure, with guarantees on the training error, and for several years it was not clear what statistical model it fitted. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) answered this by showing that boosting is stagewise additive modelling: each round adds one term to an additive function $F(x) = \sum_m f_m(x)$ so as to improve a population criterion.

Section 4.3 of that paper takes the step from interpretation to design. If boosting is stagewise fitting of an additive logistic model, one can choose the criterion directly: the Bernoulli log-likelihood. The resulting procedure, LogitBoost (Algorithm 3), fits at each round a weighted least-squares regression to a working response, exactly as iteratively reweighted least squares fits a logistic regression. Result 3 states that this is no accident: in the population, LogitBoost's update is a Newton step on the expected log-likelihood. The same Newton reading reappears in gradient boosting with logistic loss, where each terminal node of a tree takes one Newton step (Friedman 2001).

Timeline:

1997: Freund and Schapire, AdaBoost (J. Comput. Syst. Sci. 55).
1999: Schapire and Singer, Real AdaBoost with confidence-rated predictions (Mach. Learn. 37).
2000: Friedman, Hastie and Tibshirani, the statistical view; LogitBoost and Result 3.
2001: Friedman, gradient boosting machines (Ann. Statist. 29).

Setting

Let $X$ be a measurable space of features and let $\nu$ be a probability measure on $X\times\{0,1\}$ , the joint law of a feature $x$ and a 0/1 response $y^*$ . Write $E(\cdot\mid x)$ for the conditional expectation given $x$ , an integral against the regular conditional distribution of $y^*$ given $x$ .

A current fit is a function $F : X\to\mathbb R$ . The symmetric logistic model (30) represents $P(y^*=1\mid x)$ by

p(x) = \frac{e^{F(x)}}{e^{F(x)}+e^{-F(x)}}.

For an update $f(x)$ , the expected log-likelihood (31) is

E\,l(F+f) = E\Big[2y^*\big(F(x)+f(x)\big) - \log\big(1+e^{2(F(x)+f(x))}\big)\Big],

whose integrand is the Bernoulli log-likelihood $y^*\log p + (1-y^*)\log(1-p)$ of $y^*$ under the model.

For a positive weight $w$ , the weighted conditional expectation is $E_w(g\mid x) = E(wg\mid x)/E(w\mid x)$ . LogitBoost (Algorithm 3), population version, computes the working response and weight

z = \frac{y^*-p(x)}{p(x)(1-p(x))},\qquad w(x) = p(x)(1-p(x)),

fits $f(x) = E_w(z\mid x)$ (the population weighted least-squares regression of $z$ on $x$ ), and updates $F(x)\leftarrow F(x)+\tfrac12 f(x)$ .

Formalization targets

Goal: Result 3

Fix $x$ and let $\ell_x(t) = E[\,2y^*(F(x)+t) - \log(1+e^{2(F(x)+t)})\mid x]$ . Then $\ell_x$ has first derivative $s(x)$ and second derivative $H(x)$ at $t=0$ ,

s(x) = 2E\big(y^*-p(x)\mid x\big),\qquad H(x) = -4E\big(p(x)(1-p(x))\mid x\big),

$H(x)\neq0$ , and the population LogitBoost update equals the Newton update:

F(x) + \tfrac12E_w(z\mid x) = F(x) - H(x)^{-1}s(x).

Milestones

(31): the integrand of $E\,l(F+f)$ is the Bernoulli log-likelihood of the symmetric logistic model.
(32): the first derivative $s(x)$ .
(33): the second derivative $H(x)$ .
(34)–(35): $F(x) - H(x)^{-1}s(x) = F(x) + \frac12 \frac{E(y^*-p(x)\mid x)}{E(p(x)(1-p(x))\mid x)} = F(x)+\frac12E_w\big(\frac{y^*-p(x)}{p(x)(1-p(x))}\,\big|\,x\big)$ .
(36): the Newton update solves $\min_{f(x)} E_{w(x)}\big(F(x)+\frac12 z - (F(x)+f(x))\big)^2$ .

Significance

The result. Result 3 explains what LogitBoost computes: a stagewise Newton–Raphson ascent of the expected Bernoulli log-likelihood, one coordinate $F(x)$ at a time. It makes the working response and the weights of Algorithm 3 the score and curvature of the likelihood, and reduces each round to a weighted least-squares problem (36) that any regression method can solve.

Formalizing it. The result is proved on the page by a short calculation, and no machine-checked version exists. The mission produces a formal account of the population algorithm on an arbitrary joint law, with conditional expectations taken through a regular conditional distribution, the derivatives stated with differentiability, and the Newton step identified exactly, including the constants $2$ , $-4$ and $\tfrac12$ that the symmetric parametrization forces.

Difficulty

The algebra is short; the formal content is in keeping every object honest. The derivatives are of a conditional expectation in a parameter, so differentiation must pass through the integral against the conditional law. The second derivative needs the first derivative as a function of $t$ , not only its value at $0$ . The Newton step divides by $H(x)$ , which must be shown nonzero from $0<p(x)<1$ rather than assumed. A tempting shortcut, replacing the conditional expectation of the log-likelihood by its closed form in a free probability parameter, removes the joint law from the statement and is ruled out.

Formalization scope

Labels are Bool, with $y^*(\texttt{true}) = 1$ and $y^*(\texttt{false})=0$ . The joint law is a probability measure ν on X × Bool; $E(\cdot\mid x)$ is the integral against Mathlib's ν.condKernel x. Every statement is for every $x$ , conditional on $x$ as in the Derivation; because the label space is finite, no integrability or measurability hypotheses are needed.
The symmetric logistic is written exactly as (30), $e^{t}/(e^{t}+e^{-t})$ , not as $1/(1+e^{-t})$ , which differs by a factor $2$ in $t$ and would change every constant.
The conditional log-likelihood is defined as an integral against the conditional law, not by its closed form with a free parameter.
Derivatives are stated with HasDerivAt, never with deriv, which returns $0$ at non-differentiable points; $H(x)\neq0$ is a conclusion, so the division in the Newton step cannot silently return $0$ .
The weighted conditional expectation takes its weight as an explicit argument; here it is $p(x)(1-p(x))$ .
In (36) the page writes $E_{w(x)}$ without " $\mid x$ "; it is read as the conditional weighted expectation, since the Derivation conditions on $x$ throughout.
Out of scope: the data version of Algorithm 3 (regression trees, the $z_{\max}$ threshold and the weight floor of pp. 352–353), which are implementation choices, and the multiclass algorithm (§5).

Contributions welcome: differentiation of finite conditional expectations in a parameter, and derivative facts for the symmetric logistic, both reusable across the other missions of this series.

Selected references

J. Friedman, T. Hastie, R. Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28(2):337–407, 2000. https://doi.org/10.1214/aos/1016218223
Y. Freund, R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, J. Comput. Syst. Sci. 55(1):119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
R. E. Schapire, Y. Singer, Improved boosting algorithms using confidence-rated predictions, Mach. Learn. 37(3):297–336, 1999. https://doi.org/10.1023/A:1007614523901
J. Friedman, Greedy function approximation: a gradient boosting machine, Ann. Statist. 29(5):1189–1232, 2001. https://doi.org/10.1214/aos/1013203451

7 thms3 active usersReviewed

Machine Learning Statistics·Captain: mikedeng1

Additive Logistic Regression: A Statistical View of Boosting 2: Population Discrete AdaBoost Is a Newton-Like Step with Exact Line Search c = ½ log((1−err)/err)Research Paper

Motivation

AdaBoost (Freund and Schapire, 1997) combines many weak classifiers $f_m(x) \in \{-1, 1\}$ into a weighted vote $\operatorname{sign}\big(\sum_m c_m f_m(x)\big)$ . At each round it fits a classifier to a reweighted training sample, sets $c_m = \log((1 - \mathrm{err}_m)/\mathrm{err}_m)$ from the weighted error $\mathrm{err}_m$ , and multiplies the weights of the misclassified points by $e^{c_m}$ . The algorithm was introduced as a procedure for boosting the accuracy of weak learners in the PAC sense, and its good test performance was at first not explained by any statistical model.

Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) recast boosting as stagewise fitting of an additive model by minimizing the exponential criterion $J(F) = E(e^{-yF(x)})$ . Their Lemma 1 shows that $J$ is minimized at half the log-odds, so an additive $F$ fitted this way estimates a logistic regression model. Result 1 of that paper, the subject of this mission, shows that Discrete AdaBoost is exactly such a fitting procedure: in its population version, each round is a Newton-like step on $J$ followed by an exact line search, and the resulting reweighting is AdaBoost's. This view underlies gradient boosting, LogitBoost and the loss-function analysis of boosting in later work.

Setting

Let $X$ be a measurable space of features and let $\nu$ be a probability law of the pair $(x, y)$ on $X \times \{-1, 1\}$ . The conditional law of $y$ given $x$ is the disintegration $\nu(\cdot \mid x)$ , and $E(\cdot \mid x)$ is the integral against it. A current estimate is a measurable $F : X \to \mathbb R$ , and the exponential criterion is

J(F) = E\big(e^{-yF(x)}\big) \in [0, \infty].

With weight $w(x, y) = e^{-yF(x)}$ , the weighted conditional expectation and the weighted expectation are

E_w[g(x, y) \mid x] = \frac{E[w(x, y) g(x, y) \mid x]}{E[w(x, y) \mid x]}, \qquad E_w[g(x, y)] = \frac{E[w(x, y) g(x, y)]}{E[w(x, y)]}.

A classifier is a measurable $f : X \to \{-1, 1\}$ ; its weighted error is $\mathrm{err} = E_w[1_{[y \neq f(x)]}]$ . The paper's candidate update is $F \leftarrow F + cf$ with

f(x) = \begin{cases} 1, & E_w(y \mid x) > 0, \\ -1, & \text{otherwise}, \end{cases} \qquad (18) \qquad\qquad c = \frac12 \log\frac{1 - \mathrm{err}}{\mathrm{err}}. \qquad (20)

Algorithm 1 (p. 338) uses $c_m = \log((1 - \mathrm{err})/\mathrm{err}) = 2c$ and the update $w \leftarrow w \exp(c_m 1_{[y \neq f(x)]})$ followed by renormalization.

Formalization targets

Goal: Result 1 (p. 346)

For $F$ measurable with $J(F) < \infty$ :

for every $c > 0$ and every $x$ , the classifier (18) minimizes the quadratic approximation $E_w(1 - ycs + c^2/2 \mid x)$ over $s \in \{-1, 1\}$ ;
for every classifier $f$ with $0 < \mathrm{err} < 1$ , the coefficient $c$ of (20) satisfies

J(F + cf) \le J(F + c'f) \qquad \text{for all } c' \in \mathbb R;

for every classifier $f$ , every $x$ and $y$ ,

e^{-yF(x)} e^{-cf(x)y} = e^{-c} \cdot e^{-yF(x)} \exp\Big(\log\frac{1 - \mathrm{err}}{\mathrm{err}}\, 1_{[y \neq f(x)]}\Big),

so the population reweighting coincides with Algorithm 1's after renormalization.

Milestones

the second-order expansion of $E_w(e^{-cys} \mid x)$ in $c$ (proof of Result 1, p. 346);
(17)–(18): for $c > 0$ , (16) is maximization of $E_w[yf(x)]$ , solved by (18) (p. 347);
(19): $-E_w[yf(x)] = E_w[(y - f(x))^2]/2 - 1$ (p. 347);
(20): $c = \frac12\log((1-\mathrm{err})/\mathrm{err})$ is the unique minimizer of $E_w e^{-cyf(x)}$ (p. 347);
$-yf(x) = 2 \times 1_{[y \neq f(x)]} - 1$ and the weight identity (p. 347);
Corollary 2 (p. 348), referenced from the platform in its sample form;
(21)–(22): the first-order condition of the line search (p. 348).

Significance

The result. Result 1 turns AdaBoost from a combinatorial reweighting scheme into an optimization method with a known objective. It identifies the population quantity the algorithm estimates (via Lemma 1, half the log-odds), explains the specific constant $\log((1-\mathrm{err})/\mathrm{err})$ as an exact line search, explains why the weights of misclassified points are inflated by $(1-\mathrm{err})/\mathrm{err}$ , and shows that a weak learner worse than chance is used with reversed sign. It is the template for the other population results of the paper (Real AdaBoost, LogitBoost, Gentle AdaBoost) and for later functional-gradient views of boosting.

Formalizing it. The result is proved on paper; it has not been machine-checked. The paper's argument is stated informally ("≈", "arg min", "Newton-like"); this mission fixes each claim as a precise statement about measures on $X \times \{-1, 1\}$ . The sample version of Corollary 2 is already proved on the platform (UnderstandingML.adaboost_reweighted_error) and is reused; everything else is new.

Difficulty

Each step is elementary on its own; the work is in carrying the population statements through measure theory. The weighted expectations are ratios of integrals that are meaningful only under integrability of $e^{-yF(x)}$ , and the line-search claim compares $J(F + c'f)$ for all real $c'$ , all of which must be shown finite before they can be compared as real numbers. The pointwise claim (16)–(18) uses the conditional law of $y$ given $x$ , which exists only as a disintegration kernel; passing from it to the unconditional (17) requires the disintegration identity and measurability of (18) in $x$ . The tempting shortcut of treating $J(F + cf)$ as its quadratic approximation does not prove the line-search claim: (20) is the exact minimizer of $J$ , not of the approximation.

Formalization scope

Labels are Booleans, with $y = 1$ for true and $y = -1$ for false. $J$ is a lower Lebesgue integral in $[0, \infty]$ and is compared there; $E_w$ and $E_w(\cdot \mid x)$ are ratios of Bochner integrals, the conditional one against ν.condKernel x. Disclosed additions, each needed for the page's formulas to be defined: $F$ and $f$ measurable, $J(F) < \infty$ , and $0 < \mathrm{err} < 1$ wherever $\log((1-\mathrm{err})/\mathrm{err})$ is used. No condition $\mathrm{err} < 1/2$ is imposed. Ties $E_w(y \mid x) = 0$ go to $-1$ , as printed. The "≈" of the expansion is read as "second-order Taylor polynomial in $c$ ", and derivatives are stated with HasDerivAt.

Trivializing formalizations are excluded: $J$ is not defined by a conditional formula or as a Bochner integral (which would return $0$ on non-integrable weights and make every step optimal), the logarithm is never applied outside its domain, and the class of $f$ stays $\{-1, 1\}$ -valued (over real-valued $f$ the Newton step is Gentle AdaBoost's, a different result).

Everything is in the namespace AddLogReg.Discrete, with one definitions file (Setting) holding $J$ , $E_w$ , the classifier (18), $\mathrm{err}$ and the coefficient (20). Reusable pieces are lemmas on disintegrations of laws on $X \times \mathrm{Bool}$ and on weighted expectations. Proofs of any milestone are welcome independently.

Selected references

J. Friedman, T. Hastie and R. Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28(2):337–407, 2000. https://doi.org/10.1214/aos/1016218223
Y. Freund and R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, J. Comput. System Sci. 55(1):119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
R. E. Schapire and Y. Singer, Improved boosting algorithms using confidence-rated predictions, Machine Learning 37:297–336, 1999. https://doi.org/10.1023/A:1007614523901

10 thms3 active usersReviewed

Linear Optimization Operations Research·Captain: mikedeng1

An O(√nL)-Iteration Homogeneous and Self-Dual Linear Programming Algorithm 2: τᵏ Stays Bounded Below If (LP) Has an Optimum, and Otherwise κᵏ Stays Bounded Below and τᵏ/θᵏ Is BoundedResearch Paper

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)$ :

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;

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

17 thms3 active usersReviewed

Missions

Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming 2: One Aggressive Stepsize Policy Drives the AG Gradient Mapping to Zero on Nonconvex Composite ProblemsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 11)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition I: Gradient Descent with Step 1/L Satisfies f(x_k) − f* ≤ (1 − μ/L)^k (f(x_0) − f*)Research Paper

Motivation

Setting

Formalization targets

Gradient descent at step size 1/L1/L1/L

Nearby consequences

Significance

Difficulty

Formalization scope

Selected references

Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming 1: The Randomized Stochastic Gradient Method Has (1/L)E‖∇f(x_R)‖² ≤ (D_f² + σ²Σγ_k²)/Σ(2γ_k − Lγ_k²)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2.1 a)

Milestones

Companion statements

Significance

Difficulty

Formalization scope

Selected references

Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming 2: The Randomized Stochastic Gradient-Free Method with Gaussian Smoothing Bounds (1/L)E‖∇f(x_R)‖² for Nonconvex fResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2 a)

Companions

Milestones

Significance

Difficulty

Formalization scope

Selected references

A game-theoretic approach to computation offloading in mobile cloud computing I: The Offloading GNEP Has a SolutionResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 1 (p. 12)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A game-theoretic approach to computation offloading in mobile cloud computing II: The VI Map of the Offloading GNEP Is Monotone When the Cloudlet Is Not OverloadedResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Complexity of Nash Equilibria and Other Fixed Points 4: The Fixed Points of the Division-Free Map G_I(x)ij = max(x_ij + u_i((i:j); x−i) − t_i, 0) Are Exactly the Nash EquilibriaResearch Paper

Motivation

Setting

Formalization targets

Goal: Lemma 20 (p. 47)

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

On the Complexity of Nash Equilibria and Other Fixed Points 1: ε-Nash Equilibria Are Weak (n+1)ε-Fixed Points of Nash's Function, and Weak ε²/(4c²n³)-Fixed Points Are ε-Nash EquilibriaResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3 in explicit form

Milestones

Gradient descent at step size $1/L$