Optimization

Motivation

Training a model by stochastic gradients on a constrained or regularized loss is a stochastic composite problem: a smooth expected loss, observed only through noisy gradients, plus a simple non-smooth term such as a constraint set or an $\ell_1$ penalty. For convex losses, accelerated stochastic approximation methods attain the optimal rates (Lan 2012; Ghadimi & Lan 2012). For nonconvex losses, the available guarantees came from randomized stochastic gradient methods (Ghadimi & Lan 2013) and their mini-batch proximal versions (Ghadimi, Lan & Zhang 2016), which are not optimal when the problem happens to be convex.

Ghadimi and Lan (arXiv:1310.3787v1, 2013; Math. Program. 156, 2016) gave one accelerated scheme covering both cases. This mission formalizes its most general result, Theorem 4 (§3.2): the randomized stochastic accelerated gradient (RSAG) method with mini-batches, on a composite objective whose smooth part may be nonconvex and whose gradients are noisy.

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$ is differentiable with $L_f$-Lipschitz gradient and may be nonconvex, $h$ is convex and differentiable with $L_h$-Lipschitz gradient, $L_\Psi=L_f+L_h$, and $\mathcal X$ is a convex, possibly non-smooth function with bounded domain $K$ (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\{\langle y,u\rangle+\frac1{2c}\|u-x\|^2+\mathcal X(u)\}$ for $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)$, a small $\|\mathcal G\|$ certifies approximate stationarity. Assumption 2 asks for $M$ with $\|\mathcal P(x,y,c)\|\le M$ for all $x,y$ and $c>0$.

Gradients come from a stochastic oracle: queried at $x$, it returns $G(x,\xi)$ for a random sample $\xi$. Assumption 1 asks that the output be unbiased, $\mathbb E[G(x,\xi)]=\nabla\Psi(x)$, with variance at most $\sigma^2$.

Algorithm 4 takes $\alpha_1=1$, $\alpha_k\in(0,1)$ for $k\ge2$, $\beta_k,\lambda_k>0$, batch sizes $m_k\ge1$, 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},\qquad\bar G_k=\frac1{m_k}\sum_{i=1}^{m_k}G(x^{md}_k,\xi_{k,i}),$$ $$x_k=\mathcal P(x_{k-1},\bar G_k,\lambda_k),\qquad x^{ag}_k=\mathcal P(x^{md}_k,\bar G_k,\beta_k).$$

With $\Gamma_1=1$ and $\Gamma_k=(1-\alpha_k)\Gamma_{k-1}$ (2.6), the output is $(x^{md}_R,x^{ag}_R)$, where $R\in\{1,\dots,N\}$ is drawn independently of the oracle with

$$\mathrm{Prob}\{R=k\}=\frac{\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)}{\sum_{j=1}^N\Gamma_j^{-1}\beta_j(1-L_\Psi\beta_j)}.\tag{3.7}$$

Formalization targets

Goal: Theorem 4 (pp. 21–22)

Fix $N\ge1$, 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 and $S=\sum_{k=1}^N\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)$. Then

$$\mathbb E\big[\|\mathcal G(x^{md}_R,\nabla\Psi(x^{md}_R),\beta_R)\|^2\big]\le\frac8S\Big[\frac{\|x_0-x^*\|^2}{2\lambda_1}+\frac{L_f}{\Gamma_N}(\|x^*\|^2+2M^2)+\sigma^2\sum_{k=1}^N\frac{\beta_k(4+(1-L_\Psi\beta_k)^2)}{4\Gamma_k(1-L_\Psi\beta_k)m_k}\Big],\tag{3.30}$$

and, if $L_f=0$,

$$\mathbb E\big[\Phi(x^{ag}_R)-\Phi(x^*)\big]\le\frac1S\sum_{k=1}^N\beta_k(1-L_\Psi\beta_k)\Big(\frac{\|x_0-x^*\|^2}{2\lambda_1}+\sigma^2\sum_{j=1}^k\frac{\beta_j(4+(1-L_\Psi\beta_j)^2)}{4\Gamma_j(1-L_\Psi\beta_j)m_j}\Big).\tag{3.31}$$

The expectations are over $R$ and all samples. The goal keeps general step sizes and batch sizes; Corollaries 4 and 5 (explicit policies) are left for follow-up work.

Milestones

In the order of the proof: Lemma 4 ($\mathcal G(x,\cdot,c)$ is 1-Lipschitz); the mini-batch variance bound (3.28) and its consequence (3.29) for the gradient mapping; Lemma 1, (2.16) and 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 three-point inequalities (3.32)–(3.33) and their combination (3.34); the descent bound (2.46) (already proved on the platform) and (2.47); the one-step and summed inequalities of p. 22; the iterate bound (2.52); the summed inequality at $x=x^*$; and the expected bound (3.35).

Significance

The result. Theorem 4 covers stochastic composite problems whether or not $\Psi$ is convex, with one step-size policy. Under Corollary 4's policy and batch sizes it gives a sample complexity for $\mathbb E\|\mathcal G\|^2\le\epsilon$ that improves the dependence on $L_h$ over mini-batch proximal stochastic gradient [Ghadimi, Lan & Zhang 2016], and when $L_f=0$ it recovers the optimal rate for convex stochastic composite optimization. Its proof is a template for later variance-controlled accelerated methods: a weighted Lyapunov argument in which nonconvexity enters only through $L_f$ and noise only through the martingale and variance terms.

Formalizing it. The result has been proved and refereed since 2016. As far as is known, no proof assistant has a formalization of it, and the platform has no accelerated stochastic method with a nonconvex guarantee. A complete development gives machine-checked versions of the mini-batch variance bound for martingale-difference noise, the Lipschitz property of the gradient mapping, the proximal three-point inequality on a convex domain, and the composite accelerated analysis with noise. Each of these can be reused in other stochastic proximal methods.

Difficulty

Copying the deterministic composite proof (Theorem 2) fails in two places. First, the deterministic step bounds $\min_k\|\mathcal G_k\|$ through the decrease $\|x^{ag}_k-x^{md}_k\|^2$, but here $x^{ag}_k$ is computed from $\bar G_k$, so this decrease measures the stochastic gradient mapping. Passing back to the exact one costs an extra variance term, which is why the constant is 8 rather than 2. Second, the noise $\bar\delta_k$ appears in two ways. The linear term $\langle\bar\delta_k,x^*-x_{k-1}\rangle$ vanishes only in expectation, and only because $x_{k-1}$ is fixed before the batch is drawn. The quadratic terms need the variance of an average of dependent samples, which is $\sigma^2/m_k$ only when the samples within a batch are conditionally unbiased given the earlier ones. A pathwise argument cannot remove either term, and an unconditional reading of Assumption 1 does not give the second.

Formalization scope

• Space and smoothness. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) (the published GhadimiLan.RSG.E). Smoothness of $f$ and $h$ is the platform's ConvexOptAlg.SmoothGD.IsBetaSmooth. $\Psi$, $\nabla\Psi$ and $L_\Psi$ are given with the identities $\Psi=f+h$, $\nabla\Psi=\nabla f+\nabla h$, $L_\Psi=L_f+L_h$.
• The convex term is its domain K with finite values X and ConvexOn ℝ K X; the prox map is a function P with the minimizer hypothesis IsProxMap K X P. A real-valued $\mathcal X$ on all of $\mathbb R^n$ is excluded: it makes Assumption 2 unsatisfiable and the goal vacuous. So is a free P with no minimizer property.
• The noise. Oracle calls are numbered consecutively; iteration $k$ makes calls $S_{k-1}+1,\dots,S_{k-1}+m_k$ with $S_k=m_1+\dots+m_k$, all at $x^{md}_k$. Assumption 1 is the published GhadimiLan.RSG.AssumptionA1 along these query points: conditional unbiasedness given a filtration of the earlier calls, and conditional variance bound $\sigma^2$. This conditional form is what the paper's proof uses, and the i.i.d. setting satisfies it. The oracle is jointly measurable. The variance bound (3.28) is a milestone and is never assumed.
• The output index $R$ is measurable, takes values in $\{1,\dots,N\}$ with mass function (3.7), and is independent of the whole sample sequence. Algorithm 4 runs pathwise, for every $k$, and is evaluated at $R$, which is the paper's "run $N$ steps, output the $R$-th iterate". Integrability of every expected quantity is part of each conclusion.
• Excluded trivializations: batch size fixed to 1 (general $m_k$ is kept), $\sigma=0$, a fixed $R$, and (3.28) taken as a hypothesis.
• Conventions. Indexing is 1-based, and $\Gamma_k=\prod_{i=2}^k(1-\alpha_i)$, so $\Gamma_1=1$. (2.9) and (2.10) are imposed for $k=1,\dots,N$, and $\beta_k<1/L_\Psi$ is written $L_\Psi\beta_k<1$. Two hypotheses are added: an optimal $x^*$ exists (the statement uses it), and $\|x_0\|\le M$ (used silently in (2.52) at $k=1$). The page prints $\Phi(x)$ on the left of (3.35) where $\Phi(x^*)$ is meant; the Lean states $\Phi(x^*)$.

Contributions welcome: proofs of any milestone. Lemma 4, (3.28) and the three-point inequality are self-contained and reusable. Also welcome: the measurability of the iterates, and Corollaries 4–5 as follow-up statements.

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
• 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 mini-batch variance bound and Proposition 1, the Lipschitz property of $\mathcal G$). https://doi.org/10.1007/s10107-014-0846-1
• S. Ghadimi, G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23 (2013) 2341–2368 (the randomized stochastic gradient method). https://doi.org/10.1137/120880811
• 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). https://doi.org/10.1137/110848864
• G. Lan, An optimal method for stochastic composite optimization, Math. Program. 133 (2012) 365–397. https://doi.org/10.1007/s10107-010-0434-y

Motivation

In stochastic programming the objective $\Psi(x)=\mathbb E_\xi[F(x,\xi)]$ is an expectation that cannot be evaluated, and an algorithm sees only noisy gradients $G(x,\xi)$ drawn from a stochastic first-order oracle. Stochastic gradient descent and its relatives are the standard methods. For convex $\Psi$ the optimal rate is known: Lan's accelerated stochastic approximation method (Lan, Math. Program. 2012) reaches an expected optimality gap of order $L\|x_0-x^*\|^2/N^2+\sigma\|x_0-x^*\|/\sqrt N$ after $N$ oracle calls. For smooth nonconvex $\Psi$, Ghadimi and Lan's randomized stochastic gradient (RSG) method (arXiv:1309.5549, SIAM J. Optim. 2013) bounds the expected squared gradient norm at a randomly chosen iterate, but it is only nearly optimal when $\Psi$ happens to be convex.

Saeed Ghadimi and Guanghui Lan (arXiv:1310.3787v1, 2013; Mathematical Programming 156, 2016) combined the two lines: the randomized stochastic accelerated gradient (RSAG) method has a guarantee for nonconvex problems, and with suitable step sizes it attains the optimal rate on convex ones. This mission formalizes that result, Theorem 3 of the paper, together with the steps of its proof in §3.1.

Setting

Let $\Psi:\mathbb R^n\to\mathbb R$ be differentiable with Lipschitz gradient: $\|\nabla\Psi(y)-\nabla\Psi(x)\|\le L_\Psi\|y-x\|$ for all $x,y$, with $L_\Psi>0$. Gradients are available only through a stochastic oracle: at its $k$-th call, with input $x$, it returns $G(x,\xi_k)$, where $\xi_1,\xi_2,\dots$ are random variables on a probability space and $G$ is jointly measurable.

Algorithm 3 (RSAG). The inputs are $x_0\in\mathbb R^n$, step sizes $\alpha_1=1$, $\alpha_k\in(0,1)$ for $k\ge2$, $\beta_k>0$, $\lambda_k>0$, an iteration limit $N\ge1$, and a probability mass function $p_1,\dots,p_N$. A termination index $R$ with $\Pr\{R=k\}=p_k$ is drawn first, independently of the noise. With $x^{ag}_0=x_0$, for $k=1,2,\dots$,

$$x^{md}_k=(1-\alpha_k)x^{ag}_{k-1}+\alpha_kx_{k-1},\qquad x_k=x_{k-1}-\lambda_kG(x^{md}_k,\xi_k),\qquad x^{ag}_k=x^{md}_k-\beta_kG(x^{md}_k,\xi_k),$$

and the method stops at $k=R$ and outputs $(x^{md}_R,x^{ag}_R)$. The oracle error is $\delta_k=G(x^{md}_k,\xi_k)-\nabla\Psi(x^{md}_k)$.

Assumption 1 asks that the oracle be unbiased, $\mathbb E[\delta_k]=0$, with variance $\mathbb E\|\delta_k\|^2\le\sigma^2$. The paper does not require the $\xi_k$ to be independent.

The weights are $\Gamma_1=1$, $\Gamma_k=(1-\alpha_k)\Gamma_{k-1}$, and for a horizon $N$

$$C_k=1-L_\Psi\lambda_k-\frac{L_\Psi(\lambda_k-\beta_k)^2}{2\alpha_k\Gamma_k\lambda_k}\Big(\sum_{\tau=k}^N\Gamma_\tau\Big).$$

Formalization targets

Goal: Theorem 3 (pp. 15–16)

Fix $N\ge1$. The expectations are taken over $R$ and $\xi_{[N]}=(\xi_1,\dots,\xi_N)$.

a) If $\Psi$ is bounded below with $\Psi^*=\inf\Psi$, $C_k>0$ for $k\le N$, and $p_k=\lambda_kC_k/\sum_{j}\lambda_jC_j$ (3.4), then

$$\mathbb E\|\nabla\Psi(x^{md}_R)\|^2\le\frac{1}{\sum_{k=1}^N\lambda_kC_k}\Big[\Psi(x_0)-\Psi^*+\frac{L_\Psi\sigma^2}{2}\sum_{k=1}^N\lambda_k^2\Big(1+\frac{(\lambda_k-\beta_k)^2}{\alpha_k\Gamma_k\lambda_k^2}\sum_{\tau=k}^N\Gamma_\tau\Big)\Big].\tag{3.5}$$

b) If $\Psi$ is convex with a minimizer $x^*$, $\alpha_k/(\lambda_k\Gamma_k)$ is nonincreasing (2.10), $\alpha_k\lambda_k\le L_\Psi\beta_k^2$ and $\beta_k<1/L_\Psi$ (3.6), and $p_k\propto\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)$ (3.7), then

$$\mathbb E\|\nabla\Psi(x^{md}_R)\|^2\le\frac{(2\lambda_1)^{-1}\|x_0-x^*\|^2+L_\Psi\sigma^2\sum_{k}\Gamma_k^{-1}\beta_k^2}{\sum_{k}\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)},\tag{3.8}$$ $$\mathbb E[\Psi(x^{ag}_R)-\Psi(x^*)]\le\frac{\sum_{k}\beta_k(1-L_\Psi\beta_k)\big[(2\lambda_1)^{-1}\|x_0-x^*\|^2+L_\Psi\sigma^2\sum_{j\le k}\Gamma_j^{-1}\beta_j^2\big]}{\sum_{k}\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)}.\tag{3.9}$$

The goal keeps every printed constant and leaves the step sizes free. Corollary 3 specializes them; it is not part of this mission.

Milestones

Part a): the quadratic bound (2.1) (already proved on the platform); a pathwise one-step inequality for $\Psi(x_k)$ (p. 16); a stochastic version of (2.17) bounding $\|x^{ag}_{k-1}-x_{k-1}\|^2$; the summed inequality with martingale terms $b_k$ (pp. 16–17); its expectation (p. 17); the identity expressing $\mathbb E\|\nabla\Psi(x^{md}_R)\|^2$ as a $p$-weighted average (p. 17); Theorem 3 a). Part b): Lemma 1 (p. 4); the convexity bound (2.21); (3.10) with a sign corrected; the stochastic version of (2.22); (3.11); its two consequences at $x=x^*$ (p. 18); the weighting identity for $\Psi(x^{ag}_R)$ (p. 18); Theorem 3 b).

Significance

The result. Theorem 3 gives one stochastic first-order method with two guarantees. On a nonconvex problem it finds an approximate stationary point with an explicit bound on $\mathbb E\|\nabla\Psi\|^2$. On a convex problem its optimality gap matches the lower bound for stochastic convex optimization, which the RSG method does not. The method does not need to know which case it is in; only the step-size policy changes. Later work on accelerated and variance-reduced methods for nonconvex stochastic problems builds on the same analysis, and Theorem 4 of the paper extends it to composite problems with mini-batches.

Formalizing it. The result is proved in the paper and, as far as we know, has not been machine-checked. A formal proof would check the bookkeeping that a reader usually takes on trust: the nested sums in $C_k$ and $b_k$, the conditional-expectation arguments that make $\{b_k\}$ a martingale difference sequence, and the passage from fixed horizons to the random output $R$. The printed proof has small errors (see Formalization scope), so the formal statements record the corrected forms.

Difficulty

The deterministic analysis of the AG method (Theorem 1) bounds $\Psi(x_N)$ along a single trajectory. In the stochastic case the same chain produces cross terms $\langle\nabla\Psi(x_{k-1}),\delta_k\rangle$ and $\langle\nabla\Psi(x^{md}_k),\delta_k\rangle$. These cross terms do not vanish pathwise, and the variance terms come with coefficients involving $\sum_{\tau\ge k}\Gamma_\tau$ that grow backwards in time. The obvious argument would take expectations termwise. It fails unless one shows that each cross-term coefficient is measurable with respect to the past, so that its product with $\delta_k$ has zero mean under conditional unbiasedness. This also requires square-integrability of every iterate, which the hypotheses do not state and which has to be established by induction. A second difficulty is the random output: the bound is on $\mathbb E\|\nabla\Psi(x^{md}_R)\|^2$, an integral over $R$ and the noise jointly, so the independence of $R$ from the noise has to be used explicitly.

Formalization scope

• Space and smoothness. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) (the published GhadimiLan.RSG.E n). $\Psi\in\mathcal C^{1,1}_{L_\Psi}$ is the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth Ψ g LΨ, with $g=\nabla\Psi$, and $L_\Psi>0$.
• The run. It is defined along each noise realization by recursion and evaluated pointwise on $\Omega$. Indices are 1-based. $\Gamma_k=\prod_{i=2}^k(1-\alpha_i)$, so $\Gamma_1=1$. The run is recorded for every $k$; the paper itself notes that stopping at $R$ is the same as running $N$ steps and outputting the $R$-th pair.
• Assumption 1 is the published GhadimiLan.RSG.AssumptionA1 applied to the middle points: for a filtration to which the noise is adapted, $\mathbb E[G(x^{md}_k,\xi_k)\mid\mathcal F_{k-1}]=\nabla\Psi(x^{md}_k)$ a.s. and $\mathbb E\|\delta_k\|^2\le\sigma^2$. This conditional form is what the paper's martingale-difference step uses. It holds when the $\xi_k$ are independent, and it allows dependent noise, as the paper does.
• The termination index. $R$ is measurable, takes values in $\{1,\dots,N\}$, has the mass function (3.4) or (3.7), and is independent of the whole noise sequence. Each part of the goal quantifies over its own $R$.
• Conditions on step sizes. (2.7), (2.10) and (3.6) are required for $k=1,\dots,N$.
• Expectations. Every expectation is a Lebesgue integral, and its integrability is part of the conclusion, since Lean assigns $0$ to the integral of a non-integrable function.
• Corrected typos. On p. 16, $\delta_k$ is read as $\delta_\tau$ in the stochastic (2.17), and the middle line of the summed chain has a wrong sign. In (3.10) the term $\beta_k\langle\nabla\Psi(x^{md}_k),\delta_k\rangle$ should carry a minus sign, which this mission states as "(3.10), sign corrected". On p. 18, $\|x_0-x\|$ means $\|x_0-x^*\|$. None of these affects the theorem.

The following versions would make the goal trivial and are excluded: a deterministic oracle ($\sigma=0$ hard-wired), $R$ fixed to $N$, an oracle $G$ not tied to $\nabla\Psi$, and an unconditional unbiasedness hypothesis too weak to support the martingale step.

A complete development needs conditional expectations of vector-valued random variables, square-integrability of the iterates, and the independence calculus for the random index. These parts are reusable for the companion RSG and mini-batch RSAG missions. Contributions are welcome on any milestone. The pathwise milestones (one-step bound, (2.17), (2.21), (2.22), (3.10)) need no probability theory.

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.3787
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM J. Optim. 23 (2013) 2341–2368. https://arxiv.org/abs/1309.5549
• G. Lan, An optimal method for stochastic composite optimization, Math. Program. 133 (2012) 365–397. https://doi.org/10.1007/s10107-010-0434-y
• Y. Nesterov, A method for unconstrained convex minimization problem with the rate of convergence O(1/k²), Doklady AN SSSR 269 (1983) 543–547.

Motivation

In a congestion game, each player chooses resources and pays a cost that depends on how many players use each chosen resource. Such games model shared facilities and network use, where independently chosen strategies can cost more in total than a coordinated choice. The price of anarchy measures this inefficiency by comparing the social cost of an equilibrium with the minimum social cost. A familiar way to bound it is to prove a smoothness inequality that applies to every pair of strategy profiles. That inequality has a useful reach: once established, it bounds not only pure Nash equilibria but also broader equilibrium notions. The question in this mission is how much that reach costs in sharpness. Roughgarden (2015) proves that for congestion games it costs nothing at the level of the worst case over any fixed collection of allowed resource cost functions.

For affine resource costs, earlier analyses had already identified a worst-case value of $5/2$, attained by a finite congestion game and matched by a smoothness bound. The 2015 paper asks whether this agreement reflects affine costs or a general property of congestion games. Its Theorem 5.8 gives the latter answer, even when the collection of allowed functions is infinite and has no prescribed formula. The mission treats the theorem at that generality, while giving the finite positive case and the boundary case their own supporting targets. Roughgarden (2015), §§2.3 and 5.

Setting

A finite congestion game has a finite player set, a finite resource set $E$, and for each player $i$ a nonempty set $S_i$ of subsets of $E$ called strategies. Each resource $e$ has a cost function $c_e:\mathbb N\to\mathbb R$. For a strategy profile $A=(A_i)_i$, its load $x_e(A)$ is the number of players whose selected strategy contains $e$. Player $i$ pays $C_i(A)=\sum_{e\in A_i}c_e(x_e(A))$, and the social cost is $C(A)=\sum_i C_i(A)$. A profile is a pure Nash equilibrium when no player can lower its own cost by changing its strategy alone. These are the objects of Example 2.5 in Roughgarden (2015).

Fix a nonempty set $\mathcal C$ of resource cost functions, each nonnegative, nondecreasing, and not identically zero on positive loads. The class $\mathcal G(\mathcal C)$ contains every finite congestion game whose resource functions belong to $\mathcal C$. It permits any finite number of players and resources and any nonempty strategy families. The pure price of anarchy $\rho_{\mathrm{pure}}(G)$ is the largest equilibrium-to-optimum cost ratio in one game, allowing $+\infty$ when an equilibrium costs more than zero but the optimum costs zero.

A game is $(\lambda,\mu)$-smooth if, for every two feasible profiles $A,A^*$, the sum of the player costs after each player individually switches from $A_i$ to $A_i^*$ is at most $\lambda C(A^*)+\mu C(A)$. The set $\mathcal A(\mathcal G(\mathcal C))$ consists of pairs with $\mu<1$ that satisfy this inequality for every game in the class. A related resourcewise set $\mathcal A(\mathcal C)$ asks, for every $c\in\mathcal C$, current load $x\ge0$, and comparison load $x^*\ge1$, that

$$c(x+1)x^*\le\lambda c(x^*)x^*+\mu c(x)x.$$

Its best ratio is $\gamma(\mathcal C)=\inf_{(\lambda,\mu)\in\mathcal A(\mathcal C)}\lambda/(1-\mu)$, with value $+\infty$ if there is no admissible pair. The bounded-load versions $\mathcal A(\mathcal C,n)$ and $\gamma(\mathcal C,n)$ use $0\le x\le n$ and $1\le x^*\le n$. Roughgarden (2015), equations (34)–(36) and (41).

Formalization targets

Tightness of the congestion-game class

Theorem 5.8, in the form of equation (34), is the goal:

$$\sup_{G\in\mathcal G(\mathcal C)}\rho_{\mathrm{pure}}(G) =\inf_{(\lambda,\mu)\in\mathcal A(\mathcal G(\mathcal C))}\frac{\lambda}{1-\mu}.$$

It applies to every nonempty set $\mathcal C$ satisfying the standing cost-function conditions, whether finite, countable, or uncountable. Neither the number of players nor the number of resources is fixed. The equality is stronger than the routine upper bound from smoothness: it says that the best upper bound available from a uniform smoothness argument matches actual worst-case pure-equilibrium inefficiency. Roughgarden (2015), Theorem 5.8 and (34).

Resourcewise characterization

The paper also identifies the common value with $\gamma(\mathcal C)$:

$$\sup_{G\in\mathcal G(\mathcal C)}\rho_{\mathrm{pure}}(G)=\gamma(\mathcal C).$$

The milestone list follows the paper's statements: the general upper bound; nonnegativity of $\mu$; passage from resource constraints to game smoothness; the bound for one game; the two finite optimization lemmas; the finite lower-bound theorem; the infinite-price boundary case; the countable case; and the characterization by $\gamma(\mathcal C)$. The finite lower-bound target uses the one-sided conclusion established in the proof of Theorem 5.6. Roughgarden (2015), §§5.1–5.5.

Significance

The equality rules out a uniform improvement of the worst-case pure price-of-anarchy bound by using features of pure Nash equilibrium that a smoothness argument ignores. In this domain the broader applicability of smoothness does not force a worse class-wide bound. For a chosen cost-function family, the resourcewise characterization expresses that bound through explicit inequalities rather than a search over every possible finite game. Roughgarden (2015), §§2.4 and 5.5.

The result is proved in the paper. The remaining work here is a machine-checked proof of its formal statement and supporting theorems. The published congestion-game model supplies loads, player costs, feasible profiles, and pure Nash equilibria. The definitions of smoothness parameters and prices of anarchy built for this mission can also support later work on other cost-function classes and equilibrium bounds. The goal statement itself is a proof target, not an already verified result.

Difficulty

The smoothness inequality immediately gives an upper bound on equilibrium costs, but it does not by itself show that a game attains or approaches that bound. The difficult direction relates a small family of resourcewise constraints to actual games with inefficient equilibria. For finite positive cost-function sets, the optimum parameter value may be attained or may be approached only at infinity in parameter space; the two cases have different statements in Lemmas 5.3 and 5.5. The general theorem must also cover functions that vanish at a positive load, unbounded worst-case ratios, and sets of functions of arbitrary cardinality. Simply optimizing a bound for one fixed game would miss the supremum over the entire class. Roughgarden (2015), §§5.2–5.4.

Formalization scope

Lean represents players and resources by Fin k and Fin m and quantifies over every $k,m\in\mathbb N$. A strategy is a finite resource subset, a strategy family is finite and nonempty, and all costs are real-valued at each load. The value $c(0)$ is unrestricted because it is unused in a player's cost and is multiplied by zero in (35). The all-zero function is excluded as in §5.1. Nonemptiness of $\mathcal C$, stated at the start of that section, is carried into the finite optimization lemmas because their conclusions select functions from $\mathcal C$. Zero-player and zero-resource games are allowed and do not raise the worst-case supremum.

Prices of anarchy and the values $\gamma$ are extended nonnegative reals. Thus an empty smoothness-parameter set has infimum $+\infty$; a positive equilibrium cost over zero optimum gives $+\infty$; and a game with no equilibrium contributes zero to the supremum. The paper's finite congestion games with nonempty strategy sets do have pure equilibria. The conversion of a real ratio $\lambda/(1-\mu)$ into this type does not truncate admissible class-wide ratios: if some cost function has $c(1)>0$, a one-resource game forces the ratio to be at least one; if none does, the parameter set is empty. Smoothness and optimum quantify over feasible profiles only. These choices prevent the equality from becoming vacuous through an empty real infimum, total division by zero, or a supremum over a fixed small game size.

The complete development needs finite-set sums, function updates, extended nonnegative infima and suprema, and the published congestion-game definitions. Reusable contributions include lemmas about the resourcewise parameter sets and their relation to game smoothness. The paper's uncountable approximation paragraph has a gap for flat cost functions; the theorem remains the stated target, and a formal proof may use a different argument at that stage. Roughgarden (2015), pp. 31–32.

Selected references

• Tim Roughgarden, Intrinsic Robustness of the Price of Anarchy, Journal of the ACM 62(5), Article 32, 2015. DOI. The source used here is the author's final version dated July 14, 2015; the cited page numbers are its printed pages.

Motivation

Stochastic gradient (SG) methods are the default algorithms for training machine-learning models: when an objective is an average over a very large number of training examples, computing its full gradient even a few times is infeasible, while the gradient of a single randomly chosen example is cheap. The classical convergence theory of SG rates its expected suboptimality under strong convexity — the $O(1/k)$ rate of Nemirovski, Juditsky, Lan and Shapiro (2009) — yet common models such as least squares with a rank-deficient design and logistic regression are convex but not strongly convex.

Karimi, Nutini and Schmidt (2016) observed that the much older Polyak–Łojasiewicz (PL) inequality of Polyak (1963) is enough to recover linear rates for gradient descent and its variants without any convexity. Their Theorem 4 transfers this observation to SG: under PL alone, SG with a decreasing step attains the $O(1/k)$ rate known from the strongly convex case, and SG with a constant step converges linearly to a neighbourhood of the optimum whose size is proportional to the step. This mission formalizes that theorem.

Setting

Let $d\ge0$ and let $\mathbb R^d$ carry the Euclidean norm $\|\cdot\|$. An index $i$ ranges over a measurable space $I$ with a probability measure $\nu$, and each index has a differentiable component function $f_i:\mathbb R^d\to\mathbb R$. The stochastic optimization problem (7) is to minimize

$$f(x) = \mathbb E_{i\sim\nu}[f_i(x)],$$

of which the finite sum $f = \frac1n\sum_{i=1}^n f_i$ (8) is the case of the uniform distribution on $n$ indices. The component gradients are unbiased: $\mathbb E_{i\sim\nu}[\nabla f_i(x)] = \nabla f(x)$ for every $x$.

The SG method (9) starts from a point $x_0$ and, given step sizes $\alpha_k>0$ and indices $i_0,i_1,\dots$ drawn independently from $\nu$, iterates

$$x_{k+1} = x_k - \alpha_k\nabla f_{i_k}(x_k).$$

The iterate $x_k$ is a random vector, a function of $i_0,\dots,i_{k-1}$.

The standing assumptions on $f$ (§2 of the paper) are:

1. $\nabla f$ is $L$-Lipschitz: $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$, with $L>0$;
2. the solution set is non-empty: some $x^*$ minimizes $f$, and $f^* = f(x^*)$;
3. the PL inequality (3) with constant $\mu>0$: $\tfrac12\|\nabla f(x)\|^2\ge\mu\,(f(x)-f^*)$ for all $x$.

Theorem 4 adds a second-moment bound along the iterates: $\mathbb E_{i\sim\nu}\big[\|\nabla f_i(x_k)\|^2\big]\le C^2$ for every iterate $x_k$.

Formalization targets

Goal: Theorem 4 (p. 6)

Under the assumptions above,

1. with the decreasing step $\alpha_k = \dfrac{2k+1}{2\mu(k+1)^2}$,

$$\mathbb E[f(x_k)-f^*]\le\frac{LC^2}{2k\mu^2}\qquad(k\ge1);$$

2. with a constant step $\alpha_k=\alpha$, $0<\alpha<\dfrac1{2\mu}$,

$$\mathbb E[f(x_k)-f^*]\le(1-2\mu\alpha)^k\,[f(x_0)-f^*]+\frac{LC^2\alpha}{4\mu}\qquad(k\ge0).$$

The second-moment bound is assumed separately for the run of each scheme, with the same constant $C$.

Milestones (proof of Theorem 4, p. 7)

1. One-step bound. For any point $x$ with $\mathbb E_i\|\nabla f_i(x)\|^2\le C^2$ and any step $a$,

$$\mathbb E_i[f(x-a\nabla f_i(x))]\le f(x)-a\|\nabla f(x)\|^2+\frac{LC^2a^2}{2}.$$

2. Recursion (10). Along the run, whenever $\alpha_k\ge0$,

$$\mathbb E[f(x_{k+1})-f^*]\le(1-2\alpha_k\mu)\,\mathbb E[f(x_k)-f^*]+\frac{LC^2\alpha_k^2}{2}.$$

3. Decreasing step rate, the first half of the goal.
4. Constant step rate, the second half of the goal.

Significance

The result. Theorem 4 places SG under PL on the same footing as SG under strong convexity: the same $O(1/k)$ rate, with constants depending on $L$, $\mu$ and $C$ only, and no convexity. Since PL holds for least squares with any design matrix and, over any compact set, for logistic regression (§2.3 of the paper), the theorem gives explicit SG rates for these models. The constant-step bound quantifies the practitioners' rule of halving the step when progress stalls: halving $\alpha$ at least halves the noise floor $LC^2\alpha/(4\mu)$.

Formalizing it. The result is proved, in a short argument, in the paper. To our knowledge no machine-checked proof exists: the existing Lean formalizations of SG rates on Prove2Me concern stationarity of non-convex objectives under a variance bound, a different noise model with a different conclusion. The remaining work is to formalize the paper's proof, which requires a usable treatment of expectations over an i.i.d. index sequence (conditioning the step from $x_k$ on the past) — infrastructure that every later analysis of a stochastic first-order method can reuse.

Difficulty

The deterministic content is elementary: the descent lemma, unbiasedness, the PL inequality, a telescoping sum and a geometric series. The difficulty is probabilistic bookkeeping. Recursion (10) takes the expectation of a one-step inequality with respect to $i_k$ alone, holding $x_k$ fixed; this is legitimate because $i_k$ is independent of $i_0,\dots,i_{k-1}$, of which $x_k$ is a function. Making this precise requires measurability of the iterates in the sample path and a Fubini-type decomposition of the product law into the first $k$ coordinates, the $k$-th coordinate and the rest. A second subtlety is that the second-moment bound holds only at the iterates, not at every point, so the one-step bound must be applied pointwise in the path, on a set of full measure, rather than once and for all.

Formalization scope

The space is EuclideanSpace ℝ (Fin d) and $\nabla$ is Mathlib's gradient. The index law is an arbitrary probability measure $\nu$ on a measurable space, and the path law is the infinite product Measure.infinitePi (fun _ => ν); the run is a deterministic function sgRun of the path. The Lipschitz-gradient assumption is stated literally on $\nabla f$; the PL inequality is the published predicate ShiOptRates.PolyakLojasiewicz f (gradient f) μ (f xstar) (inequality (3) multiplied by 2); the solution set is a point xstar with ∀ y, f xstar ≤ f y, and $f^*$ is f xstar, never a free real.

Every expectation of a gap is a lower Lebesgue integral of $\max(f(x_k)-f^*,0)$ with values in $[0,\infty]$, which equals $\mathbb E[f(x_k)-f^*]$ because $f^*$ is the minimum; no integrability side condition can make a bound hold by default. The second-moment bound is the lower Lebesgue integral of $\|\nabla f_i(x_k)\|^2$, required for almost every path and every $k$. Unbiasedness and problem (7) carry explicit integrability, so a non-integrable gradient cannot turn them into trivialities.

The second-moment bound is deliberately not imposed at every point $x$. With the bound at every point, $\|\nabla f\|\le C$ everywhere, so $f-f^*\le C^2/(2\mu)$ by PL, while along the gradient-ascent flow $f-f^*$ grows exponentially unless it vanishes; hence $f$ would be constant and the theorem vacuous. Along the iterates the hypothesis is met by non-constant objectives such as $f(x)=\tfrac12\|x\|^2$.

Additions relative to the page, all disclosed in the statements: each $f_i$ is differentiable; $(i,x)\mapsto\nabla f_i(x)$ is jointly measurable, so that the iterates are random variables; the constant step is positive; the decreasing-step rate is stated for $k\ge1$; and "each $f$ has an $L$-Lipschitz continuous gradient" is read as a condition on $f$, the only one the proof uses. The page's proof of the constant-step bound writes the exponent $k$ where $k+1$ is meant; the statements follow the theorem's (correct) form.

Contributions welcome: the measurability of the run, the conditioning step for infinitePi, the deterministic one-step bound, and the two scalar recursions, each of which is reusable for other SG analyses.

Selected references

• H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition, ECML PKDD 2016; arXiv:1608.04636v4, 2020. https://arxiv.org/abs/1608.04636
• B. T. Polyak, Gradient methods for minimizing functionals, USSR Computational Mathematics and Mathematical Physics 3(4), 1963. https://doi.org/10.1016/0041-5553(63)90382-3
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4), 2009. https://doi.org/10.1137/070704277
• F. Bach, E. Moulines, Non-strongly-convex smooth stochastic approximation with convergence rate O(1/n), NeurIPS 2013. https://arxiv.org/abs/1306.2119

Motivation

Accelerated gradient (AG) methods go back to Nesterov (1983), who showed that a first-order method with a momentum-like extrapolation reaches an $\epsilon$-optimal value of a smooth convex function in $O(1/\sqrt\epsilon)$ iterations, against $O(1/\epsilon)$ for gradient descent, and that this rate is optimal among first-order methods. Many objectives met in practice (training losses, nonconvex penalties, problems with unknown convexity) are smooth but not convex. For those, gradient descent is known to drive the gradient norm to zero, with $\min_{k\le N}\|\nabla\Psi(x_k)\|^2=O(1/N)$, while the classical AG method has no convergence guarantee at all.

Saeed Ghadimi and Guanghui Lan (arXiv:1310.3787v1, 2013; Mathematical Programming 156, 2016) modified the AG method with a third step size and proved that one algorithm handles both cases: on a smooth nonconvex problem it has the gradient-descent rate for $\min_k\|\nabla\Psi\|^2$, and when the problem turns out to be convex it keeps Nesterov's optimal rate for the optimality gap. This mission formalizes that result, Theorem 1 of the paper, and its proof path in §2.1.

Setting

Let $\Psi:\mathbb R^n\to\mathbb R$ be differentiable with Lipschitz gradient: there is $L_\Psi>0$ with

$$\|\nabla\Psi(y)-\nabla\Psi(x)\|\le L_\Psi\|y-x\|\qquad\forall x,y\in\mathbb R^n, \tag{1.2}$$

and bounded from below, with $\Psi^*=\inf_x\Psi(x)$ (problem (1.1)). $\Psi$ need not be convex.

Algorithm 1 (AG). The inputs are a starting point $x_0$ and step sizes $\{\alpha_k\},\{\beta_k\},\{\lambda_k\}$, $k\ge1$, with $\alpha_1=1$, $\alpha_k\in(0,1)$ for $k\ge2$, $\beta_k>0$ and $\lambda_k>0$. Set $x^{ag}_0=x_0$ and, for $k=1,2,\dots$,

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

One gradient is evaluated per iteration, at the middle point $x^{md}_k$; $x_k$ takes a long step $\lambda_k$ and the aggregated point $x^{ag}_k$ a short step $\beta_k$. With $\beta_k=\lambda_k$ the method reduces to gradient descent, with $\beta_k=\alpha_k\lambda_k$ to a variant of Nesterov's method.

The weights are $\Gamma_1=1$, $\Gamma_k=(1-\alpha_k)\Gamma_{k-1}$ ($k\ge2$), and for a horizon $N$ and $1\le k\le N$

$$C_k=1-L_\Psi\lambda_k-\frac{L_\Psi(\lambda_k-\beta_k)^2}{2\alpha_k\Gamma_k\lambda_k}\Big(\sum_{\tau=k}^N\Gamma_\tau\Big).$$

Formalization targets

Goal: Theorem 1 (p. 5)

Fix $N\ge1$.

a) If $C_k>0$ for $k=1,\dots,N$, then

$$\min_{k=1,\dots,N}\|\nabla\Psi(x^{md}_k)\|^2\le\frac{\Psi(x_0)-\Psi^*}{\sum_{k=1}^N\lambda_kC_k}.$$

b) If $\Psi$ is convex with a minimizer $x^*$, and for $k=1,\dots,N$ one has $\alpha_k\lambda_k\le\beta_k<1/L_\Psi$ and $\alpha_1/(\lambda_1\Gamma_1)\ge\alpha_2/(\lambda_2\Gamma_2)\ge\dots$, then

$$\min_{k=1,\dots,N}\|\nabla\Psi(x^{md}_k)\|^2\le\frac{\|x_0-x^*\|^2}{\lambda_1\sum_{k=1}^N\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)},\qquad \Psi(x^{ag}_N)-\Psi(x^*)\le\frac{\Gamma_N\|x_0-x^*\|^2}{2\lambda_1}.$$

The theorem leaves the step-size policy open: any sequences meeting the conditions are covered, and the rates of Corollary 1 ($O(1/N)$ in part a, $O(1/N^2)$ for the gap in part b) follow by substitution.

Milestones

The milestones follow the proof in §2.1: the quadratic bound (2.1); Lemma 1, which unrolls the recursion $\theta_k\le(1-\alpha_k)\theta_{k-1}+\eta_k$; the nonconvex chain (2.13), (2.15), the identity for $x^{ag}_k-x_k$, (2.16), (2.17), (2.18) and (2.19); and the convex chain (2.20)–(2.25).

Significance

The result. Theorem 1 is the first convergence guarantee for an accelerated gradient method on nonconvex smooth problems. It shows that acceleration costs nothing in the nonconvex case (the same $O(1/N)$ rate for the squared gradient norm as gradient descent) while keeping the optimal $O(1/N^2)$ gap when the function is convex, so a user need not know in advance which case holds. The same analysis is the template for the composite and stochastic results of the paper (Theorems 2–4) and for the later literature on accelerated methods for nonconvex optimization.

Formalizing it. The theorem is proved on paper; it is not known to have a machine-checked proof. The mission produces a Lean definition of the AG run with its three step sizes, a formal Lemma 1 (a reusable tool for any Nesterov-type analysis), and the two chains of estimates with all constants explicit. These pieces are reused by the composite and stochastic missions of the same paper.

Difficulty

The standard analysis of Nesterov's method is an estimate-sequence or potential argument that relies on convexity at every step: it bounds $\Psi(x^{md}_k)$ below by a linearization. Without convexity that lower bound fails, and the potential need not decrease. Part a) instead tracks the decrease of $\Psi$ along the $x_k$ sequence, where gradients are evaluated at a different point $x^{md}_k$; the error this creates is governed by the gap $x^{ag}_k-x_k$, which accumulates all past gradients with weights $\Gamma_k/\Gamma_\tau$. Controlling that accumulated term, and showing it is absorbed by the condition $C_k>0$ with $C_k$ depending on the horizon $N$, is the delicate step. Part b) needs the monotonicity (2.10) to turn a weighted telescoping sum into a single initial-distance term.

Formalization scope

• The space is EuclideanSpace ℝ (Fin n). The gradient is an explicit map g, tied to $\Psi$ by the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth Ψ g LΨ (differentiable with gradient $g$, and (1.2)); $L_\Psi>0$ as in (1.2). The quadratic bound (2.1) is the published, proved ConvexOptAlg.SmoothGD.lemma_3_4.
• The run is a definition (agRun, with xSeq, xagSeq, xmdSeq), computed by (2.2)–(2.4) from $x_0$; indices are 1-based as in the paper. $\Gamma_k=\prod_{i=2}^k(1-\alpha_i)$, so $\Gamma_1=1$. $C_k$ is C LΨ α β lam N k and depends on $N$.
• "Bounded from below" is BddBelow (Set.range Ψ) and $\Psi^*$ is ⨅ x, Ψ x. The minimum over $k=1,\dots,N$ is Finset.inf' over Finset.Icc 1 N with $N\ge1$. Convexity is ConvexOn ℝ Set.univ Ψ; $x^*$ is any global minimizer.
• Conditions (2.7), (2.9), (2.10) are imposed for $k=1,\dots,N$ only.
• Trivializing formalizations are excluded: the conclusion is about the AG run itself, not an arbitrary sequence; $g$ is the gradient of $\Psi$; $\Gamma_1=1$, not $0$ (with which every bound would divide by zero); and the minimum ranges over $k\le N$, not over all $k$.

Welcome contributions: proofs of Lemma 1 and of the algebraic milestones (the identity before (2.16), (2.16), (2.17), (2.22), (2.25)), which are independent of $\Psi$; then the descent chains; then Theorem 1.

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.3787
• Y. E. Nesterov, A method for unconstrained convex minimization problem with the rate of convergence O(1/k²), Doklady AN SSSR 269 (1983) 543–547.
• Y. E. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• S. Bubeck, Convex Optimization: Algorithms and Complexity, Found. Trends Mach. Learn. 8 (2015), arXiv:1405.4980. https://arxiv.org/abs/1405.4980

Learning inventory policies from historical demand

An inventory policy chooses how much stock to order before demand is observed. Its quality is assessed by the holding and backlogging costs it incurs on future demand. A policy chosen to perform well on historical demand can overfit those observations. A useful statistical guarantee therefore controls the difference between historical and future costs simultaneously over the policies that the procedure may select. Xie, Ma and Xin establish such guarantees for stationary base-stock, $(s,S)$, and nonstationary base-stock policy classes.

This formalization covers the principal bound families in that paper. Its first goal is the expected generalization and estimation bound for nonstationary base-stock policies with no fixed ordering cost, Corollary 4.10. Its supporting targets include Theorem 4.9 and the constructive product-sample partition in Lemma 4.12. The other principal bounds remain in the explicit scope below and await their own full Lean declarations. The companion inventory-information project needs these results as proved dependencies; merely citing the paper does not close that project's formal proof obligations.

Demand, policy classes and statistical errors

There are $T+L$ periods, a deterministic lead time $L\ge0$, and demand bounded by $U>0$. The first order arrives in period $L+1$. Average loss means the sum of holding and backlogging costs in periods $L+1,\ldots,T+L$, divided by the positive horizon $T$. The initial pipeline is empty, and initial inventory is nonpositive for the base-stock models. Holding and backlogging cost coefficients are $h,b\in[0,1]$. Nonstationary base-stock policies in the first goal have no fixed ordering cost and use levels $S^t\in[0,(L+1)U]$.

The Lean model indexes the first period by zero. It uses the source's explicit finite-maximum formula for post-replenishment inventory, with the demand interval summed up to, but excluding, the observation period. In mathematical notation the inventory in period $L+k+1$ is $\max_{0\le j\le k}(S_j-\sum_{j\le r<k+L}d_r)$. Cost is evaluated after subtracting the current demand $d_{L+k}$. This is a backlog model; applications to lost sales require a separate equivalence argument.

Data comprise $N>0$ IID demand trajectories from a probability measure $\mu$ on the bounded trajectory space. Different periods of the same trajectory can be dependent. Generalization error is the one-sided supremum $\mathrm{GE}=\sup_S(R(S)-\widehat R(S))$, where $R$ is expected average loss and $\widehat R$ is empirical average loss. Estimation error is $R(\widehat S)-R(S_*)$, for an empirical minimizer and a best-in-class population policy. It is not the error relative to every history-dependent inventory policy. These conventions follow Sections 3 and 4.

Formalization targets

The first goal, Corollary 4.10, asserts the existence of one absolute constant $C>0$ such that

$$\mathbb E\mathrm{EE}\le\mathbb E\mathrm{GE}\le C(L+1)U/\sqrt N.$$

The constant is quantified before the horizon, lead time, support, costs, demand distribution, sample size, and policy selections. The first inequality explicitly refers to actual minimizers, with an integrable selected risk. The GE conclusion holds independently of whether a particular selector has been supplied.

Its principal complexity target is Theorem 4.9: for each relevant period and $0<\gamma\le1$, the normalized inventory class has fat-shattering dimension at most $2/\gamma+1$. The Lean statement says directly that every $\gamma$-shattered indexed sample has cardinality at most that number. It uses the source convention of a strict upper label and non-strict lower label.

Lemma 4.12 partitions all $N^D$ product indices into $N^{D-1}$ groups of $N$ indices. Every coordinate of every group traverses the original row indices exactly once. The formal statement uses a bijection between anchor-offset pairs and complete index tuples, together with a coordinate-permutation assertion. The dimension $D=d+1$ is positive, and $N=1$ and $D=1$ are included.

The full scope also retains Theorem 4.1 and Corollary 4.2 (stationary policies), Theorem 4.4 and Corollary 4.5 ($(s,S)$ upper bounds), Theorem 4.7 and Corollary 4.8 ($(s,S)$ fat-shattering and GE lower bounds), and the expected Product ERM comparison in equation (4.7). They are catalogued with their assumptions but are not yet all encoded. The GE lower bound is not asserted to be a minimax policy-regret lower bound.

What the formalization supplies

The nonstationary policy vector grows with the horizon, while the expected average-loss bound has no horizon factor. A verified version supplies a reusable statistical ingredient for finite-horizon inventory learning. Total-cost bounds require multiplication by the horizon. Absolute uniform deviation, period-dependent costs, high-probability statements, initial-state reductions, and censoring require further bridge theorems. They are not attributed to Corollary 4.10 without those proofs.

The cyclic partition has a complete locally checked Lean proof with axiom dependencies only propext and Quot.sound. The two statistical targets remain open. Neither a drafted declaration nor a local proof is described as a server-verified contribution.

Mathematical difficulty

Ordinary pseudodimension can grow with the horizon for the nonstationary class, so it does not by itself give the desired horizon-free rate. A full proof needs scale-sensitive complexity, probability, and integration infrastructure. For Product ERM, coordinate independence must be explicit: the groups in the partition need not be independent of each other. The expected comparison transfers upper bounds; it cannot reverse direction to transfer a GE lower bound.

Formalization scope and conventions

The shared environment is Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Demand and policy coordinates are bounded real subtypes with their usual measurable structures. Probability is over IID whole trajectories. Finite maximum indices are nonempty. Positive $T,N,U$ prevent zero denominators in the targets. General definitions remain total, and their behavior outside these hypotheses is exposed in the independent read-backs.

Complete proofs must establish the boundedness and measurability needed for the real suprema and integrals to have their usual meaning. They may not assume the convergence bound, replace arbitrary probability measures by finite-support distributions, or silently restrict the policy class. The $(s,S)$ branch additionally needs explicit unbounded-domain conventions when holding or backlogging costs vanish. Reusable contributions include shattering, symmetrization, entropy bounds, selection and integrability facts, and finite-product sampling.

Selected references

• Yaqi Xie, Will Ma and Linwei Xin, VC Theory for Inventory Policies, arXiv:2404.11509v3, 2026. https://arxiv.org/abs/2404.11509v3
• Hanzhang Qin, David Simchi-Levi and Ruihao Zhu, Information Limits of Multistage Inventory Control: Learning, Valuation, and Censoring, arXiv:2609.37380v1, 2026. https://arxiv.org/abs/2609.37380v1

Motivation

Many problems in quantum information theory ask for the maximum of a linear functional over pairs of quantum states, one on each of two systems, subject to linear constraints on each state. The best success probability of an approximate quantum error-correcting code of given size is of this form: the encoder and the decoder are quantum channels, their Choi matrices are states with fixed marginals, and the objective is bilinear in the two (Berta, Borderi, Fawzi & Scholz, arXiv:1810.12197, §4). Such constrained bilinear programs are nonconvex. Seesaw methods give lower bounds that often converge in practice, but they offer no guarantee of global optimality. What is needed is a hierarchy of efficiently computable outer bounds that converges to the optimum, with an explicit rate.

For the unconstrained problem, the optimisation over separable states, such a hierarchy is classical: the Doherty–Parrilo–Spedalieri hierarchy of $n$-extendible states, whose convergence follows from finite quantum de Finetti theorems (Christandl, König, Mitchison & Renner 2007; Brandão & Harrow 2013). The standard de Finetti approximant is, however, a mixture of product states that need not satisfy the linear constraints, so it says nothing about the constrained problem. The paper proves a de Finetti theorem with linear constraints (Theorem 2.3) and derives from it a semidefinite hierarchy for constrained bilinear programs with a convergence guarantee (Theorem 3.1).

Setting

A $d$-dimensional quantum system has operator space $\mathcal S=\mathbb C^{d\times d}$; a state is a positive semidefinite $W\in\mathcal S$ with $\mathrm{Tr}\,W=1$. Let $A$ and $B$ be systems of dimensions $d_A$ and $d_B$. The data are an objective $G_{AB}\in\mathcal S_A\otimes\mathcal S_B$, arbitrary linear maps $\Lambda_{A\to C_A}:\mathcal S_A\to\mathcal S_{C_A}$ and $\Gamma_{B\to C_B}:\mathcal S_B\to\mathcal S_{C_B}$, and matrices $X_{C_A}$, $Y_{C_B}$. The constrained bilinear program is

$$Q=\max\ \mathrm{Tr}[G_{AB}(W_A\otimes W_B)]\quad\text{s.t. } W_A,W_B\ \text{states},\quad \Lambda_{A\to C_A}(W_A)=X_{C_A},\quad \Gamma_{B\to C_B}(W_B)=Y_{C_B}.$$

For $n\ge1$ let $B_1,\dots,B_n$ be copies of $B$. A state $W_{AB_1^n}$ on $A\otimes B_1\cdots B_n$ is symmetric with respect to $A$ if it is invariant under every permutation $\mathcal U^\pi_{B_1^n}$ of the copies $B_1,\dots,B_n$, $\pi\in\mathfrak S_n$. Write $W_{B_1^n}=\mathrm{Tr}_A W_{AB_1^n}$, $W_{B_1^{n-1}}=\mathrm{Tr}_{B_n}W_{B_1^n}$ and $W_{AB_1}=\mathrm{Tr}_{B_2^n}W_{AB_1^n}$. The level-$n$ program is

$$\mathrm{SDP}_n=\max\ \mathrm{Tr}[G_{AB}W_{AB_1}]\quad\text{s.t. } W_{AB_1^n}\ \text{a state, symmetric with respect to } A,$$ $$(\Lambda_{A\to C_A}\otimes\mathcal I_{B_1^n})(W_{AB_1^n})=X_{C_A}\otimes W_{B_1^n},\qquad (\mathcal I_{B_1^{n-1}}\otimes\Gamma_{B_n\to C_B})(W_{B_1^n})=W_{B_1^{n-1}}\otimes Y_{C_B}.$$

It is a semidefinite program of size polynomial in $d_A$ and $d_B^n$.

The rate involves the trace norm $\|X\|_1=\mathrm{Tr}|X|$, the Schatten $\infty$-norm $\|G\|_\infty$ (largest singular value), and the minimal distortion with side information of $B$,

$$f(B|\cdot)=\inf_{\mathcal M_B}\ \sup_{\substack{\xi_{AB}^\dagger=\xi_{AB}\\ \xi_A=0,\ \xi_B=0}}\frac{\|\xi_{AB}\|_1}{\|(\mathcal I_A\otimes\mathcal M_B)(\xi_{AB})\|_1},$$

the infimum over measurements $\mathcal M_B$ on $B$ and the supremum over all finite-dimensional $A$; $f(A,B)$ is the analogue with product measurements $\mathcal M_A\otimes\mathcal M_B$. Throughout, $\log$ is base 2.

Formalization targets

Goal: Theorem 3.1 with its explicit rate

$$Q\ \le\ \mathrm{SDP}_n\ \le\ Q+\|G_{AB}\|_\infty\,d_B^2(d_B+1)\sqrt{\frac{(2\ln2)\log d_A}{n}}\quad(n\ge1),\qquad Q=\lim_{n\to\infty}\mathrm{SDP}_n.$$

The page states $0\le\mathrm{SDP}_n-Q\le\mathrm{poly}(d)/\sqrt n$ with $d=\max\{d_A,d_B\}$. The goal makes explicit the rate the proof gives.

Milestones, in attack order

1. Lemma 2.1 (p. 6): for a permutation-invariant classical-quantum state $\rho_{AZ_1^n}$ there is $0\le m<n$ with $\mathbf E_{z_1^m}\|\rho_{AZ_{m+1}|z_1^m}-\rho_{A|z_1^m}\otimes\rho_{Z_{m+1}|z_1^m}\|_1^2\le(2\ln2)\log d_A/n$.
2. Lemma D.1 (p. 29): for a state two-design $\{P_z\}$ and $\mathcal M_B$ with effects $\frac{d_B}{t}P_z$, $\|(\mathcal I_A\otimes\mathcal M_B)(\xi_{AB})\|_1\ge\|\xi_{AB}\|_1/(d_B^2(d_B+1))$ for every Hermitian $\xi_{AB}$.
3. Existence of state two-designs in every dimension (p. 29).
4. $f(B|\cdot)\le d_B^2(d_B+1)$ (p. 6).
5. Conditional constraints (p. 8): the states obtained by measuring $B_1,\dots,B_m$ and conditioning satisfy $\Lambda(\rho_{A|z_1^m})=X_{C_A}$ and $\Gamma(\rho_{B_{m+1}|z_1^m})=Y_{C_B}$.
6. Theorem 2.3 (p. 7): under the constraints of $\mathrm{SDP}_n$, $\|\rho_{AB}-\sum_ip_i\sigma^i_A\otimes\omega^i_B\|_1\le\min\{f(A,B),f(B|\cdot)\}\sqrt{(2\ln2)\log d_A/n}$ with states $\Lambda(\sigma^i_A)=X_{C_A}$, $\Gamma(\omega^i_B)=Y_{C_B}$.
7. Eq. (3) (p. 2): $Q$ equals the maximum over mixtures of feasible product states.
8. Hölder step (p. 11): $\mathrm{Tr}[GW]\le\mathrm{Tr}[GV]+\|G\|_\infty\|W-V\|_1$.
9. $0\le\mathrm{SDP}_n-Q$ (p. 11).

Significance

Theorem 3.1 turns a nonconvex problem into a sequence of semidefinite programs whose values decrease to the optimum at rate $O(1/\sqrt n)$, with a constant that depends polynomially on $d_B$ and logarithmically on $d_A$. Every level is a certified upper bound; together with any feasible point it brackets $Q$. The same argument applied to channel fidelities gives converging outer bounds on the success probability of approximate quantum error correction (§4 of the paper), and the constrained de Finetti theorem is the key step there as well. Theorem 2.3 is of independent interest: it is the first finite de Finetti theorem in which the approximating separable state inherits linear constraints of the extension.

The results are proved in the paper; none of them has been machine-checked. A complete formalization requires the quantum relative entropy and mutual information with their chain rule, the quantum Pinsker inequality, state two-designs and their existence, and a weighted Hölder inequality for Schatten norms; most of this is absent from Mathlib, and each piece is reusable beyond this mission.

Difficulty

The obvious route measures every copy $B_i$ with a fixed informationally complete measurement and uses the resulting classical de Finetti statement. This approximates $\rho_{AB}$ by a mixture of product states, but the states in the mixture need not satisfy $\Gamma(\omega^i)=Y$, and projecting them onto the constraint set destroys the error bound. The paper instead conditions on the outcomes of only $m$ copies and keeps $B_{m+1}$ quantum; the constraint on $B_n$ then transfers to the conditional state of $B_{m+1}$ by symmetry. Making this rigorous needs the chain rule of conditional mutual information with classical conditioning, and the distortion of the measurement must be bounded independently of the side system $A$, which is what Lemma D.1 provides. The Schatten-norm estimate there is elementary but requires a weighted Hölder inequality and a careful choice of weight.

Formalization scope

Systems are finite index types: $A\otimes B_1\cdots B_N$ is indexed by Fin dA × (Fin N → Fin dB), $\otimes$ is Mathlib's Kronecker product, and the permutation action permutes the word in Fin N → Fin dB. States, trace norm and partial traces are the published definitions WildeQIT_IsDensityOperator, WildeQIT_traceNorm and WildeQIT_partialTrace. The linear maps $\Lambda$, $\Gamma$ are arbitrary $\mathbb C$-linear maps (not assumed positive or trace preserving), applied blockwise to one tensor factor. The objective is the real part of $\mathrm{Tr}[G\,W]$, equal to $\mathrm{Tr}[G\,W]$ for Hermitian $G$. Each "max" is the supremum of the set of objective values over the feasible set, never over all matrices. Wherever the page has $n\ge1$ copies of $B$, the Lean has n + 1: SDPval … n is the page's $\mathrm{SDP}_{n+1}$, and the bounds have denominator $n+1$. The distortions $f(A,B)$ and $f(B|\cdot)$ take values in $[0,\infty]$; the standalone bound on $f(B|\cdot)$ assumes $d_B\ge1$.

No feasibility hypothesis is added to the goal. The feasible sets of $Q$ and of every level are empty or nonempty together, and the empty case reads $0\le0\le0+\dots$. The goal mentions only $Q$, $\mathrm{SDP}_n$, $G$, $d_A$, $d_B$ and $n$; a formalization in which $Q$ or $\mathrm{SDP}_n$ were free real numbers, or in which the de Finetti mixture was not required to satisfy the constraints, would be a different and much weaker statement.

Contributions are welcome at every milestone, and especially in the reusable infrastructure: quantum relative entropy and mutual information on matrices, the quantum Pinsker inequality, unitary and state designs, and Hölder inequalities for Schatten norms.

Selected references

• M. Berta, F. Borderi, O. Fawzi, V. B. Scholz, Semidefinite programming hierarchies for constrained bilinear optimization, Mathematical Programming, 2021; arXiv:1810.12197v3. https://arxiv.org/abs/1810.12197
• F. G. S. L. Brandão, A. W. Harrow, Quantum de Finetti theorems under local measurements with applications, STOC 2013. https://arxiv.org/abs/1210.6367
• M. Christandl, R. König, G. Mitchison, R. Renner, One-and-a-half quantum de Finetti theorems, Communications in Mathematical Physics 273, 2007. https://arxiv.org/abs/quant-ph/0602130
• A. C. Doherty, P. A. Parrilo, F. M. Spedalieri, Complete family of separability criteria, Physical Review A 69, 2004. https://arxiv.org/abs/quant-ph/0308032