Optimization

Motivation

Least-squares regression fitted by stochastic gradient descent — the least-mean-square (LMS) algorithm — is the basic large-scale learning procedure: each observation is touched once, at a cost linear in the dimension. Classical analyses of stochastic approximation give the rate $O(1/\sqrt n)$ for non-strongly-convex objectives, and $O(1/(\mu n))$ when the objective is $\mu$-strongly convex. For least squares, $\mu$ is the smallest eigenvalue of the input covariance, which in high-dimensional problems is close to zero, so the strongly convex rate is often worse than the non-strongly-convex one.

F. Bach and E. Moulines (arXiv:1306.2119, NeurIPS 2013) showed that for the square loss this dichotomy disappears: averaged LMS with a constant step size reaches the rate $O(1/n)$ with no strong-convexity assumption, and with a constant that does not involve the smallest eigenvalue. Averaging of stochastic approximation iterates goes back to Polyak and Juditsky (SIAM J. Control Optim. 1992), whose guarantees are asymptotic and use decreasing step sizes. The proof technique for the expansion of the noise process is adapted from Aguech, Moulines and Priouret (SIAM J. Control Optim. 2000). This mission formalizes the non-asymptotic bound in expectation (Theorem 1 of the paper) and the chain of lemmas of its Appendix A.

Setting

Let $\mathcal H=\mathbb R^d$ with $d\ge1$, inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. For $a\in\mathcal H$, $a\otimes a$ is the operator $b\mapsto\langle a,b\rangle a$. For self-adjoint operators, $A\preccurlyeq B$ means that $B-A$ is positive semi-definite.

The data are independent and identically distributed pairs $(x_n,z_n)\in\mathcal H\times\mathcal H$, $n\ge1$, with finite second moments. The covariance operator is $H=\mathbb E[x_n\otimes x_n]$, assumed invertible (its eigenvalues may be arbitrarily small). The least-squares objective

$$f(\theta)=\tfrac12\,\mathbb E\big[\langle\theta,x_n\rangle^2-2\langle\theta,z_n\rangle\big]$$

attains its global minimum at $\theta^*$, and $\xi_n=z_n-\langle\theta^*,x_n\rangle x_n$ is the residual. The model need not be well specified: $\mathbb E[\xi_n\mid x_n]$ need not vanish. Two constants $R,\sigma>0$ satisfy

$$\mathbb E[\xi_n\otimes\xi_n]\preccurlyeq\sigma^2H,\qquad \mathbb E\big[\|x_n\|^2x_n\otimes x_n\big]\preccurlyeq R^2H .$$

These are assumptions (A1)–(A6) of §2.1. The LMS recursion with constant step size $\gamma$, started at $\theta_0\in\mathcal H$, is

$$\theta_n=\theta_{n-1}-\gamma\big(\langle\theta_{n-1},x_n\rangle x_n-z_n\big)=(I-\gamma x_n\otimes x_n)\theta_{n-1}+\gamma z_n ,$$

and its average is $\bar\theta_{n-1}=n^{-1}\sum_{k=0}^{n-1}\theta_k$.

Formalization targets

Goal: Theorem 1, Eq. (2)

For every step size $0<\gamma<1/R^2$ and every $n\ge1$,

$$\mathbb E\big[f(\bar\theta_{n-1})-f(\theta^*)\big]\le\frac{1}{2n}\left[\frac{\sigma\sqrt d}{1-\sqrt{\gamma R^2}}+R\|\theta_0-\theta^*\|\frac{1}{\sqrt{\gamma R^2}}\right]^2 .$$

The constants are the paper's. A companion item states the case $\gamma=1/(4R^2)$, where the bound reads $\frac2n\big[\sigma\sqrt d+R\|\theta_0-\theta^*\|\big]^2$.

Milestones (Appendix A)

1. The excess risk is a quadratic form: $f(\theta)-f(\theta^*)=\tfrac12\langle\theta-\theta^*,H(\theta-\theta^*)\rangle$.
2. Consequences of (A6): $\mathbb E\|x_n\|^2\le R^2$, $\operatorname{tr}H\le R^2$, $H\preccurlyeq R^2I$, and $\gamma H\preccurlyeq I$ for $\gamma\le1/R^2$.
3. Lemma 1: for a recursion $\alpha_n=(I-\gamma x_n\otimes x_n)\alpha_{n-1}+\gamma\xi_n$ with martingale-difference noise and $\gamma R^2\le1$,

$$(1-\gamma R^2)\,\mathbb E\langle\bar\alpha_{n-1},H\bar\alpha_{n-1}\rangle+\tfrac{1}{2n\gamma}\mathbb E\|\alpha_n\|^2\le\tfrac{1}{2n\gamma}\|\alpha_0\|^2+\tfrac{\gamma}{n}\textstyle\sum_{k=1}^{n}\mathbb E\|\xi_k\|^2 .$$

4. Lemma 3: $(1-(1-u)^n)^2\le nu$ for $u\in[0,1]$ and $n>0$.
5. Lemma 2: for $\alpha_n=(I-\gamma H)\alpha_{n-1}+\gamma\xi_n$ with $\mathbb E[\xi_n\otimes\xi_n]\preccurlyeq C$, the second-moment bound (13) and

$$\mathbb E\langle\bar\alpha_{n-1},H\bar\alpha_{n-1}\rangle\le\tfrac{1}{n\gamma}\|\alpha_0\|^2+\tfrac1n\operatorname{tr}(CH^{-1}).$$

6. The pathwise decomposition $\theta_n-\theta^*=M^n_1(\theta_0-\theta^*)+\gamma\sum_{k=1}^nM^n_{k+1}\xi_k$ (A.2).
7. The initial-condition bound $\mathbb E\langle\bar\eta_{n-1},H\bar\eta_{n-1}\rangle\le\|\eta_0\|^2/(n\gamma)$ for the noise-free process (A.3).
8. The expansion of the noise process (A.4): the remainder recursion (16), the covariance bound (17) $\mathbb E[\eta^r_{n-1}\otimes\eta^r_{n-1}]\preccurlyeq\gamma^{r+1}R^{2r}\sigma^2I$, the order-$r$ bound $\frac1n\gamma^rR^{2r}d\sigma^2$, the remainder bound $\frac{\gamma^{r+2}\sigma^2R^{2r+4}}{1-\gamma R^2}$, and the noise bound

$$\big(\mathbb E\langle\bar\eta_{n-1},H\bar\eta_{n-1}\rangle\big)^{1/2}\le\frac{\sigma\sqrt d}{\sqrt n}\cdot\frac{1}{1-\sqrt{\gamma R^2}}\quad(\eta_0=0,\ \gamma R^2<1).$$

Significance

The result. Theorem 1 gives a finite-sample, dimension-explicit bound with two terms: a variance term $\sigma^2d/n$, which matches the minimax rate for least-squares regression, and a bias term $R^2\|\theta_0-\theta^*\|^2/(\gamma n)$. Neither involves the smallest eigenvalue of $H$, so the guarantee survives ill-conditioning, which is the regime of high-dimensional learning. The bound is the basis for the paper's later results: the high-probability bound (Theorem 2) and the constant-step algorithm for logistic regression (Theorem 3), whose analysis invokes Theorem 1 for the quadratic approximations.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no part of it has been machine-checked. A formalization yields a reusable layer for linear stochastic approximation in finite dimension: martingale-difference noise in $\mathbb R^d$, second-moment bounds for linear recursions driven by random operators, Loewner-order arguments, and averaging. The lemmas are stated for an abstract filtration and an abstract operator $H$, so they apply beyond this model. The mission also records the corrections the appendix needs (an "$=$" that should be "$\preccurlyeq$" in (13), an index in (16), and the exponent of $\|\eta_0\|$ in A.5).

Difficulty

Two steps resist the naive approach. First, the obvious one-step analysis — expand $\|\theta_n-\theta^*\|^2$ and take expectations — yields the bias part and Lemma 1, but on the noise it gives only $\gamma\sum_k\mathbb E\|\xi_k\|^2/n$, which does not decrease with $n$. The $\sigma^2d/n$ rate requires averaging to cancel the noise, and this cancellation is visible only for the recursion with $x_n\otimes x_n$ replaced by its mean $H$. The random recursion is therefore expanded in powers of $\gamma$ around the mean recursion, and each term $\eta^r$ needs its own covariance bound, by induction on $r$, using the independence of $x_n$ from $\eta^{r}_{n-1}$. Second, the induction relies on Loewner-order bookkeeping: sums of $(I-\gamma H)^{2k}H$ must be bounded uniformly in $n$ without dividing by small eigenvalues.

Formalization scope

The space $\mathcal H$ is EuclideanSpace ℝ (Fin d). Operators are continuous linear maps, and $H^{-1}$ is an explicit two-sided inverse. Observations are indexed from $1$. Averages are $\bar p_{n-1}=n^{-1}\sum_{k=0}^{n-1}p_k$, with $n\ge1$ in every statement that uses them. The covariance operator is defined by its bilinear form, $\langle v,Hw\rangle=\mathbb E[\langle x_1,v\rangle\langle x_1,w\rangle]$. Every Loewner inequality whose sides are expectations is an inequality of quadratic forms (for example $\mathbb E\langle\xi_1,v\rangle^2\le\sigma^2\langle v,Hv\rangle$ for all $v$), which is the same order for self-adjoint operators.

Lean's Bochner integral is $0$ on non-integrable functions, so every moment assumption carries the integrability of its integrand, and every bounded expectation in a conclusion is paired with an integrability conjunct. Without these, a heavy-tailed $x_n$ would satisfy (A6) vacuously and a conclusion could hold through the value $0$; neither formalization is acceptable. Independence is of the pairs $(x_n,z_n)$, not of $x_n$ and $z_n$ separately. (A4) is attainment of the minimum, not a gradient condition.

The following hypotheses are added to the page and disclosed in each item:

• $\gamma>0$ (a step size, and $\sqrt{\gamma R^2}$ is a denominator);
• $n\ge1$;
• the positivity and self-adjointness of $H$ in Lemma 2;
• $\gamma R^2<1$ instead of $\le1$ in the remainder bound, which divides by $1-\gamma R^2$.

A complete development needs:

• conditional expectations of $\mathbb R^d$-valued martingale differences, and the orthogonality of their sums;
• independence of a fresh observation from the past iterates;
• spectral calculus for $(I-\gamma H)^k$;
• Minkowski's inequality in $L^2$.

All of these are reusable for other stochastic-approximation missions. Proofs of any milestone are welcome, as are alternative arguments for the noise bound that avoid the expansion.

Selected references

• F. Bach and E. Moulines, Non-strongly-convex smooth stochastic approximation with convergence rate O(1/n), Advances in Neural Information Processing Systems 26, 2013. https://arxiv.org/abs/1306.2119
• B. T. Polyak and A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM Journal on Control and Optimization 30(4), 1992. https://doi.org/10.1137/0330046
• R. Aguech, E. Moulines and P. Priouret, On a perturbation approach for the analysis of stochastic tracking algorithms, SIAM Journal on Control and Optimization 39(3), 2000. https://doi.org/10.1137/S0363012997331639
• F. Bach and E. Moulines, Non-asymptotic analysis of stochastic approximation algorithms for machine learning, Advances in Neural Information Processing Systems 24, 2011. https://hal.science/hal-00608041

Motivation

Many large convex programs have far more constraints than can be handled at once, but each constraint on its own is simple: a single linear equation or inequality. Row-action methods exploit this by touching one constraint per iteration. L. M. Bregman's 1967 paper (DOI 10.1016/0041-5553(67)90040-7) introduced the general framework behind most of them. A strictly convex function $f$ induces the "distance" $D(x,y)=f(x)-f(y)-(g(y),x-y)$, now called the Bregman distance, and the method moves from point to point by $D$-projections onto one constraint at a time. For $f(x)=\|x\|^2/2$ this reduces to Hildreth's method for quadratic programming; for entropy-type $f$ it gives the balancing (matrix scaling) methods used for transportation and traffic problems. The later literature on Bregman projections, mirror descent and entropic regularisation starts from this paper.

This mission formalizes the last main result of the paper, Theorem 4 (p. 212), which treats linear inequality constraints. Here a plain projection cycle does not minimize $f$. Bregman's fix carries a vector of nonnegative multipliers $u^n$ along with the primal point $x^n$ and lets each step either move towards a violated constraint or relax a multiplier. The result is a primal–dual method.

Timeline. Hildreth (1957) gave the quadratic case. Bregman (1967) proved the general theorem stated here. Censor and Lent (1981) revisited the method for interval constraints under explicit assumptions on Bregman functions (DOI 10.1007/BF00934676).

Setting

Let $E^p$ be $p$-dimensional Euclidean space and $S\subset E^p$ a convex set. Let $f$ be strictly convex on $S$, continuously differentiable over $S$ with gradient $g(x)$, and continuous over the closure $\bar S$. Let $A$ be an $m\times p$ matrix ($m\ge1$) with nonzero rows $A_1,\dots,A_m$, and $b\in E^m$. The inequality program (2.11)–(2.13) is

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

with feasible set $R=\{x \mid Ax\ge b,\ x\in\bar S\}$, assumed nonempty. The Bregman function is $D(x,y)=f(x)-f(y)-(g(y),x-y)$ (1.4). The $D$-projection $P_iy$ of $y\in S$ onto the hyperplane $A_i=\{x \mid (A_i,x)=b_i\}$ minimizes $D(\cdot,y)$ over $A_i\cap S$. The standing hypotheses ("the conditions of Theorem 3") are that $D$ satisfies the abstract conditions I–VI of §1 for these hyperplanes, together with condition (2) of Note 1: $y^n\to y^*\in\bar S$ implies $D(y^*,y^n)\to0$. In addition, $D$-projections of interior points of $S$ stay in the interior. Condition V (compact sublevel sets of $D(z,\cdot)$) is used for $z\in R$.

Write $Z_0=\{x\in S \mid g(x)=uA \text{ for some } u\ge0\}$, where $uA=\sum_iu_iA_i$, and $\varphi(x,u)=f(x)-(u,Ax-b)$. A run of the method is a sequence of pairs $(x^n,u^n)$ with $x^0\in\operatorname{int}S$, $u^0\ge0$, $g(x^0)=u^0A$, and cyclic indices $i_n$. Each step with $i=i_n$ is one of the following:

• (a) if $(A_i,x^n)<b_i$: $g(x^{n+1})=g(x^n)+\lambda_nA_i$, $(A_i,x^{n+1})=b_i$, and $u_i$ increases by $\lambda_n$;
• (b) if $(A_i,x^n)=b_i$, or $(A_i,x^n)>b_i$ with $u_i=0$: nothing changes;
• (c) if $(A_i,x^n)>b_i$ and $u_i>0$: $g(x^{n+1})=g(x^n)-\mu_nA_i$ with $\mu_n=\min(\mu_n',u_i)$, where $\mu_n'$ is the step that would reach the hyperplane, and $u_i$ decreases by $\mu_n$.

Formalization targets

Goal: Theorem 4

For every run of the method,

$$x^n\to x^*,\qquad x^*\in R,\qquad f(x^*)=\min_{y\in R}f(y).$$

Milestones (steps 1–4 of the proof)

1. $u^n\ge0$ and $g(x^n)=u^nA$ for all $n$ (step 1, (2.20)–(2.21)).
2. $\varphi(x^{n+1},u^{n+1})-\varphi(x^n,u^n)\ge D(x^{n+1},x^n)$ (step 2, (2.22)–(2.24)).
3. For $z\in R$: $D(z,x^n)\le f(z)-\varphi(x^0,u^0)$ and $\varphi(x^n,u^n)\le f(z)$ (step 3, (2.25)–(2.26)).
4. $\{x^n\}$ lies in a compact set, and $\lim\varphi(x^n,u^n)$ exists and is at most $f(z)$ for every $z\in R$ (step 3, (2.27)).
5. $D(x^{n+1},x^n)\to0$, and every limiting point of $\{x^n\}$ lies in $R$ (step 4).

Significance

Theorem 4 says that a method using one constraint per step and only $f$'s gradient converges to the minimizer of a strictly convex function over a polyhedron intersected with $\bar S$. Its multipliers $u^n$ form a dual sequence. Note 4 of the paper deduces from the theorem that the optimal value equals $\sup\varphi(x,u)$ over dual-feasible pairs ($g(x)=uA$, $u\ge0$). The theorem is the convergence statement behind Hildreth's algorithm, behind entropy-based balancing for linear inequality systems, and behind the later "interval convex programming" methods.

The theorem is proved on paper, but no machine-checked proof of it, or of any Bregman-projection row-action method, is known to exist. The formalization adds two things. It makes the paper's standing hypotheses explicit, since several are stated once or left implicit. It also forces a complete argument for the convergence of the whole sequence: the printed proof gets this from condition (2) by an argument that assumes a monotonicity property established in §1 for the pure projection method but not for the primal–dual one. A Lean proof of the goal therefore also supplies a complete proof of the paper's claim.

Difficulty

The standard argument for projection methods uses a Fejér-type property: $D(z,x^n)$ decreases for every feasible $z$. That fails here. In case (c) the point moves away from the hyperplane of a satisfied constraint, and $D(z,x^n)$ can increase. So any argument has to control primal and dual quantities together. To pass from "every limiting point is feasible" to "the whole sequence converges to an optimal point", complementary slackness has to hold in the limit, and this depends on the cyclic order and on the cap $\mu_n\le u_i$. The naive route, applying the §1 convergence theorems to the hyperplanes $A_i$, does not apply, because the iterates are not $D$-projections onto fixed sets in case (c).

Formalization scope

• $E^p$ is EuclideanSpace ℝ (Fin p); the rows are vectors $a_i$, and $uA$ is $\sum_iu_ia_i$. The gradient $g$ is explicit data tied to $f$ by HasGradientWithinAt on $S$. $S$ is not assumed open, and $f$ is continuous on $\bar S$.
• The $D$-projections form a fixed map $P$. Condition IV is assumed in the one-sided form the proofs use, which the paper's two-sided IV implies. "Compact" means sequentially compact, which agrees with compact in $E^p$. Condition (2) is read with $y^*\in\bar S$.
• Condition V is assumed for $z\in R$, the inequality-feasible set, where the proof applies it. The §1 form (for $z$ in the intersection of the hyperplanes) could hold vacuously for an inequality system.
• Step (a) is encoded by its defining conditions (2.14)–(2.15). Every new point, and the auxiliary point of case (c), lies in $S$. The run starts with $u^0\ge0$, and the cyclic control is $i_n=n\bmod m$ over indices $0,\dots,m-1$.
• Translation slips are corrected: the $Z_0$ set-builder, which breaks off, is completed; "$\mu_n'=u_{i_n}^n$" is read as $\mu_n''=u_{i_n}^n$; "Theorems 1–3" in Theorem 3 means Theorems 1–2.
• The goal quantifies over every run from every admissible start and asserts convergence of the whole sequence together with optimality of the limit. Neither "some limiting point is optimal" nor a single constructed run is an acceptable substitute. The hypotheses are jointly satisfiable, for example by Hildreth's case $f=\|x\|^2/2$, $S=E^p$ with a run that takes a case (a) step, so the goal is not vacuous.
• Needed infrastructure: Bregman distances of differentiable strictly convex functions on non-open convex sets, the strict monotonicity of the gradient, and subsequence and compactness arguments in $E^p$. These are reusable for the companion missions on Theorems 1–3 of the same paper. Contributions are welcome: proofs of the milestones, the full-convergence argument, and the duality statement of Note 4.

Selected references

• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Comput. Math. Math. Phys. 7(3) (1967) 200–217. https://doi.org/10.1016/0041-5553(67)90040-7
• C. Hildreth, A quadratic programming procedure, Naval Res. Logist. Quart. 4 (1957) 79–85. https://doi.org/10.1002/nav.3800040113
• Y. Censor, A. Lent, An iterative row-action method for interval convex programming, J. Optim. Theory Appl. 34 (1981) 321–353. https://doi.org/10.1007/BF00934676

Motivation

Many decision problems are solved repeatedly against data that arrive over time: routing traffic, allocating budgets, choosing portfolios or combinatorial structures. Online linear optimization models this. At each round $t = 1, \ldots, T$ a learner picks a decision $x_t$ from a fixed domain $\mathcal K\subseteq\mathbb R^n$, then a reward vector $f_t$ is revealed and the learner earns $f_t\cdot x_t$. Performance is measured by regret, the gap to the best fixed decision in hindsight. When $\mathcal K$ is combinatorial (paths, spanning trees, assignments), the only computationally reasonable access to $\mathcal K$ is a procedure that optimizes a linear function over it, and in practice such procedures are often only approximate.

Follow the Perturbed Leader (FPL), introduced by Hannan (1957) and analysed for linear optimization by Kalai and Vempala (JCSS 2005), uses exactly one call to an exact linear optimizer per round and achieves regret $O(\sqrt T)$ over arbitrary, not necessarily convex, domains. Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) needed a version of FPL that works with an additively approximate linear optimizer, as a building block for oracle-based robust optimization with linearly parametrized uncertainty sets. Their §3.3 analyses this variant and proves Theorem 6, the goal of this mission.

Setting

Fix a dimension $n$, a domain $\mathcal K\subseteq\mathbb R^n$ (arbitrary: not necessarily convex, closed or bounded) and $\epsilon > 0$. An $\epsilon$-approximate linear optimization procedure over $\mathcal K$ is a map $M_\epsilon:\mathbb R^n\to\mathbb R^n$ such that, for every $g\in\mathbb R^n$,

$$M_\epsilon(g)\in\mathcal K \qquad\text{and}\qquad g\cdot M_\epsilon(g)\;\ge\; g\cdot x-\epsilon\quad\text{for all }x\in\mathcal K .$$

Reward vectors $f_1,\ldots,f_T\in\mathbb R^n$ are fixed in advance (an oblivious adversary). Write $f_{1:t}=\sum_{\tau=1}^t f_\tau$, with $f_{1:0}=0$, and $\|v\|_1=\sum_i|v_i|$.

Follow the Approximate Perturbed Leader with parameter $\eta>0$ plays at round $t$

$$x_t = M_\epsilon\big(f_{1:t-1}+p_t\big),\qquad p_t \text{ uniform on the cube } [0,1/\eta]^n .$$

Three scale parameters enter the bound: $D$ bounds the $\ell_1$ diameter of $\mathcal K$, $\|x-y\|_1\le D$ for $x,y\in\mathcal K$; $A$ bounds $\|f_t\|_1$; and $R$ bounds how much each reward varies over the domain, $|f_t\cdot x-f_t\cdot y|\le R$ for $x,y\in\mathcal K$.

Formalization targets

Goal: Theorem 6 (p. 11)

With $\eta=\sqrt{D/(RAT)}$, for every $x^*\in\mathcal K$,

$$\sum_{t=1}^T f_t\cdot x^* - \mathbf E\Big[\sum_{t=1}^T f_t\cdot x_t\Big]\;\le\;2\sqrt{DRAT}+2\epsilon T .$$

The bound for every $\eta$ (proof of Theorem 6, p. 13)

For every $\eta>0$ and $x\in\mathcal K$,

$$\mathbf E\Big[\sum_{t=1}^T f_t\cdot x_t\Big]\;\ge\; f_{1:T}\cdot x-\frac D\eta-\eta RAT-2\epsilon T .$$

Supporting lemmas (pp. 12–13)

• Lemma 7 (approximate be-the-leader): $\sum_{t=1}^T M_\epsilon(f_{1:t})\cdot f_t\ge M_\epsilon(f_{1:T})\cdot f_{1:T}-\epsilon T$.
• Lemma 8 (be the approximate perturbed leader): for $T\ge2$, $p\in[0,1/\eta]^n$ and $x\in\mathcal K$, $\sum_{t=1}^T M_\epsilon(f_{1:t}+p)\cdot f_t\ge f_{1:T}\cdot x-D/\eta-2\epsilon T$.
• Lemma 9 (stability): for $p$ uniform on $[0,1/\eta]^n$, $\mathbf E[M_\epsilon(f_{1:t-1}+p)\cdot f_t]-\mathbf E[M_\epsilon(f_{1:t}+p)\cdot f_t]\ge-\eta RA$.

Significance

Theorem 6 shows that perturbed-leader online linear optimization is robust to additive error in its optimization subroutine: an $\epsilon$-approximate oracle costs only $2\epsilon T$ extra regret, so the average regret is $2\sqrt{DRA/T}+2\epsilon$. This allows the algorithm to be run over domains where exact linear optimization is intractable but a good additive approximation is available, and the paper invokes it as the online-learning primitive of its oracle-based scheme for linearly parametrized uncertainty in §3.2 (that application is not part of this mission). Unlike online gradient methods, it requires no convexity of $\mathcal K$ and no projection.

On the formal side, no regret bound for Follow the Perturbed Leader, exact or approximate, is currently formalized on the platform, and the Kalai–Vempala stability argument (comparing a uniform distribution on a cube with its translate) is a reusable piece of measure theory. The mission's statements are proved on paper; the work here is to formalize those proofs, with one correction to a hypothesis, explained under Formalization scope.

Difficulty

Lemmas 7 and 8 are deterministic and combinatorial. The substance is Lemma 9. It compares the expectations of one bounded function of $M_\epsilon(\cdot)$ under the uniform law on a cube and under its translate by $f_t$. The natural first attempt, a pointwise comparison of $M_\epsilon(f_{1:t-1}+p)$ and $M_\epsilon(f_{1:t}+p)$, fails: an approximate (even an exact) maximizer can jump arbitrarily under an arbitrarily small change of its input, and $M_\epsilon$ is not assumed continuous or even consistent between nearby inputs. Any valid argument must therefore control the two distributions as a whole rather than the decisions point by point, which in the formal development involves Lebesgue measure on $\mathbb R^n$, conditioning on a box and translation invariance.

A second subtlety is that the stability bound depends on how $R$ is read, which is the reason for the correction below.

Formalization scope

Vectors are Fin n → ℝ with dotProduct. All $\ell_1$ quantities are written as $\sum_i|v_i|$, never with the default norm (the sup norm). Rewards are a function f : ℕ → Fin n → ℝ read at $t=1,\ldots,T$, and $f_{1:t}$ is prefixSum f t. The perturbation law is Lebesgue measure conditioned on the cube $[0,1/\eta]^n$ (ProbabilityTheory.cond volume), a probability measure for $\eta>0$. Maxima over $\mathcal K$ are expressed as "for every $x\in\mathcal K$", so neither attainment nor boundedness of $\mathcal K$ is presupposed.

Conventions and deviations, each also stated in the affected item:

1. $R$ is an oscillation bound. The paper takes $R\ge\max_{t,x}|f_t\cdot x|$. With that reading Lemma 9 is false (for $\mathcal K=\{-1,1\}$, the exact maximizer, $f_{1:t-1}=-A$, $f_t=A=R$, $\eta A\le1$, the left side is $-2\eta RA$), and the printed constant in Theorem 6 does not follow. The proof's step "they can differ by at most $R$" is correct when $R\ge|f_t\cdot x-f_t\cdot y|$ for $x,y\in\mathcal K$; Lemma 9, the display and Theorem 6 are stated with that hypothesis. The printed hypothesis implies it with $2R$; for non-negative rewards the two coincide.
2. Expected reward. $\mathbf E[\sum_t f_t\cdot x_t]$ is written as $\sum_t\int f_t\cdot M_\epsilon(f_{1:t-1}+p)\,d\mu_\eta(p)$, which by linearity of expectation is the same for independent or shared perturbations (the paper makes the same observation).
3. Printed typos. In (13) the summand $f_t$ is $f_\tau$ and round $t$ uses $f_{1:t-1}$; in Lemma 8 and the display, $\max_{x}f_{1:t}\cdot x$ means $f_{1:T}$.
4. Added hypotheses. $M_\epsilon$ is measurable (otherwise every expectation would be a Bochner integral of a non-measurable function and equal $0$); an approximate maximizer can always be chosen measurable. $D,R,A>0$ and $T\ge1$ make $\eta=\sqrt{D/(RAT)}$ a positive real. The display is stated for $T\ge1$ (Lemma 8 needs $T\ge2$ as printed; the case $T=1$ also holds).
5. No $O(\cdot)$ appears: all constants are the paper's explicit ones.

A trivializing formalization is ruled out: $M_\epsilon$ must return points of $\mathcal K$ (otherwise $D$ would not bound $\|M_\epsilon(\cdot)-M_\epsilon(\cdot)\|_1$), it must be measurable, and the perturbation law is the normalized uniform distribution, not Lebesgue measure restricted to the cube (which is not a probability measure for $\eta\neq1$).

Needed infrastructure: the overlap estimate for a cube and its translate, $\mathrm{vol}([0,1/\eta]^n\cap(v+[0,1/\eta]^n))\ge(1-\eta\|v\|_1)\,\eta^{-n}$, and the integrability of bounded measurable functions of $M_\epsilon$. Both are reusable for any perturbation-based online-learning analysis; contributions of these as standalone lemmas are welcome.

Selected references

• A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-Based Robust Optimization via Online Learning, Operations Research 63(3), 2015; preprint arXiv:1402.6361v1, 2014. https://arxiv.org/abs/1402.6361
• A. Kalai, S. Vempala, Efficient algorithms for online decision problems, Journal of Computer and System Sciences 71(3), 291–307, 2005. https://doi.org/10.1016/j.jcss.2004.10.016
• J. Hannan, Approximation to Bayes risk in repeated play, Contributions to the Theory of Games III, Annals of Mathematics Studies 39, 97–139, 1957.

Motivation

In robust optimization, a decision must satisfy a constraint for every parameter value in a prescribed uncertainty set. A nonlinear uncertain constraint can be difficult to use directly because it contains a universal condition over a continuum of parameters. Ben-Tal, den Hertog, and Vial study constraints whose value is concave in the uncertain parameter. Their Theorem 2 replaces the universal condition by one inequality involving a new vector and two conjugate functions. The replacement is the general framework used for the paper's later examples, including uncertainty regions assembled from simpler sets and nonlinear functions whose conjugates have explicit forms. The discussion paper, §§2–4 is the source for this mission; theorem and page numbers refer to that 2012 version.

The paper's result extends a more specialized counterpart for a linear uncertain constraint under a φ-divergence uncertainty region. That 2013 result has a proved formalization on Prove2Me, but its divergence-specific conjugate and uncertainty set are different objects. The same earlier formalization also supplies a proved version of the self-concordant-barrier statement that this paper quotes as Lemma 33, with a differently printed constant. Neither earlier theorem supplies the general concave-constraint result here.

Setting

Fix dimensions $m,n,L$. The nominal vector is $a^0\in\mathbb R^m$, and $A\in\mathbb R^{m\times L}$ maps a primitive uncertainty $\zeta\in Z\subseteq\mathbb R^L$ to an uncertain parameter $a=a^0+A\zeta$. Thus the uncertainty set is $U=\{a^0+A\zeta:\zeta\in Z\}$. The paper assumes that $Z$ is nonempty, convex, and compact, with $0$ in its relative interior $\operatorname{ri}Z$. Relative interior is taken inside the affine hull of a set, so $Z$ may lie in a lower-dimensional plane.

A decision is $x\in\mathbb R^n$. For each decision, $D(x)$ is the effective domain of the uncertain constraint $f(\cdot,x)$: $f(a,x)$ is real on $D(x)$ and is interpreted as $-\infty$ outside it. The function is concave in $a$ on $D(x)$ for every $x$; the paper imposes no convexity assumption in the decision $x$. The robust constraint (RC) is $f(a,x)\le0$ for every $a\in U$. In the domain representation used here, this means every $a\in U\cap D(x)$. The nominal vector is regular when $a^0\in\operatorname{ri}D(x)$ for every decision $x$, as in Definition 1.

The support function of $S$ is $\delta^*(y\mid S)=\sup_{a\in S}y^Ta$. The partial concave conjugate is $f_*(v,x)=\inf_{a\in D(x)}(a^Tv-f(a,x))$. Both have extended-real values: an empty support set has support value $-\infty$, and the conjugate can be $-\infty$ when its infimum is unbounded below. These values matter in the equivalence; replacing them by a default real number changes the constraint.

Formalization targets

The goal is the paper's Theorem 2. Under the standing assumptions and regularity, for every decision $x$,

$$\left[\forall a\in U\cap D(x),\ f(a,x)\le0\right] \quad\Longleftrightarrow\quad \left[\exists v\in\mathbb R^m:\ (a^0)^Tv+\delta^*(A^Tv\mid Z)-f_*(v,x)\le0\right].$$

The right-hand inequality is the Fenchel robust counterpart (FRC). Its existence claim is essential: equality of primal and dual infima alone would not show that an auxiliary vector satisfying FRC exists.

Four source statements form the milestone path. Remark 5 gives the weak-duality inequality and the FRC-to-RC implication without concavity. Equations (16)–(18) calculate the support function of $U$. Equation (7) states the relative-interior qualification. Equations (13)–(15) state the worst-case/dual-value identity and, through the printed minimum, attainment of the dual infimum. The milestone list quotes those source passages and identifies their printed pages. Theorem 2 and its proof appear on pp. 4–5.

Significance

The equivalence gives an exact way to replace an infinite family of uncertain inequalities by an existential constraint. In examples where the support function and concave conjugate can be evaluated or represented with standard optimization constraints, it yields a finite robust counterpart. The conclusion remains a mathematical equivalence even when such an explicit representation has not been found. It is also independent of any convexity of $f$ in the decision variable, a point the paper makes after Corollary 3.

This mission supplies reusable, domain-aware support and conjugate definitions and formal statements for the duality path in the paper's central result. The new goal and milestones are open proof obligations: their Lean declarations compile, but they do not yet have machine-checked proofs. The proved 2013 φ-divergence case is narrower and does not close them. A completed development would make the general relative-interior and attained-duality steps reusable for other robust optimization models.

Difficulty

The delicate point is the direction from RC to the existence of an FRC vector. Weak duality gives only a one-sided bound. Identifying the two optimal values still leaves an existence question when an infimum is not attained. The paper invokes Fenchel duality under a relative-interior intersection condition; replacing relative interior by ordinary interior would exclude lower-dimensional uncertainty sets and effective domains that the source permits. A second difficulty is keeping finite and infinite conjugate values distinct while subtracting them in the counterpart inequality. An unbounded-below conjugate must make a finite-support FRC value $+\infty$, not a plausible finite number.

Formalization scope

Vectors are functions on Fin m, Fin n, and Fin L; $A$ is a real matrix, and dot products use the finite-vector dot product. Mathlib's intrinsicInterior ℝ represents relative interior. The domain map $D(x)$ is explicit, with the concavity hypothesis imposed on that domain. The real representative of $f$ outside $D(x)$ is ignored everywhere. The paper's Notation paragraph calls its generic concave functions closed, but the statements here omit closedness: the finite-dimensional duality qualification used for Theorem 2 needs relative-interior overlap, not that extra regularity. This is a stated strengthening of the source theorem, not a change of its feasible points.

Support functions, conjugates, worst-case values, and dual values use EReal. The paper's “max” in (8), (13), and Remark 5 is read as an extended-real supremum; its “min” in (15) is an infimum accompanied by an attaining vector. The support identity includes $Z=\varnothing$, where both sides are $-\infty$, although Theorem 2 keeps the paper's nonempty, convex, compact $Z$. On the theorem's hypotheses the support value is finite and $D(x)$ is nonempty, so the undefined-looking combinations $+\infty-(+\infty)$ and $-\infty+(+\infty)$ cannot occur in FRC. No all-space real-valued substitute for $f_*$ is used, and the theorem still quantifies over every decision and every allowed uncertainty vector.

The proof development needs finite-dimensional relative-interior behavior under affine maps and Fenchel duality with attainment. General convex conjugates and support functions can serve later missions. Corollary 3 and the paper's complexity discussion are outside this mission. Theorem A.1 is not separately made a milestone here: as printed, its domain-restricted dual maximum has a problematic $-\infty$ case; the directly used, attained identity (13)–(15) is the target under the main theorem's standing assumptions.

Selected references

• A. Ben-Tal, D. den Hertog, J.-P. Vial, Deriving robust counterparts of nonlinear uncertain inequalities, CentER Discussion Paper 2012-053, Tilburg University, 2012. Discussion-paper PDF; journal version, Mathematical Programming, 2015, DOI 10.1007/s10107-014-0750-8.
• A. Ben-Tal et al., Robust solutions of optimization problems affected by uncertain probabilities, Management Science, 2013. Prove2Me formalization of its φ-divergence case.

Motivation

Robust optimization protects a decision against every realization of uncertain data in a prescribed uncertainty set. The standard approach replaces the uncertain constraints by a deterministic robust counterpart and solves that counterpart directly (Ben-Tal, El Ghaoui, Nemirovski, Robust Optimization, 2009). The counterpart is often a harder problem than the original: a robust linear program with ellipsoidal uncertainty becomes a second-order cone program, and a robust quadratic program can become a semidefinite program. A practitioner who has an efficient, specialised solver for the nominal problem may therefore have no efficient solver for its robust version.

Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) ask whether the robust problem can be solved by repeatedly calling a solver of the nominal problem, with the number of calls independent of the dimension. Their first answer, the dual-subgradient meta-algorithm of §3.1, does so whenever the constraints are concave in the noise and the uncertainty set is convex. It is a primal–dual scheme: an online-learning algorithm picks the noise, and the nominal solver answers. This mission formalizes that result, Theorem 3.

Setting

Let $\mathcal D\subseteq\mathbb R^n$ be a convex domain, $\mathcal U\subseteq\mathbb R^d$ a convex uncertainty set, and $f_1,\dots,f_m:\mathbb R^n\times\mathbb R^d\to\mathbb R$ constraint functions. The robust feasibility problem (3) is

$$\exists\,x\in\mathcal D:\qquad f_i(x,u_i)\le 0\quad\forall u_i\in\mathcal U,\ i=1,\dots,m .$$

(An objective is handled by binary search on its value, so feasibility is the core question.) A point $x\in\mathcal D$ is an $\epsilon$-approximate solution if $f_i(x,u)\le\epsilon$ for all $u\in\mathcal U$ and all $i$.

An $\epsilon$-approximate oracle $\mathcal O_\epsilon$ (Figure 1) takes a noise vector $u=(u_1,\dots,u_m)\in\mathcal U^m$ and either returns some $x\in\mathcal D$ with $f_i(x,u_i)\le\epsilon$ for all $i$, or answers "infeasible", which it may do only if no $x\in\mathcal D$ has $f_i(x,u_i)\le 0$ for all $i$.

The standing assumptions of §3.1 are: each $f_i(\cdot,u)$ is convex on $\mathcal D$; each $f_i(x,\cdot)$ is concave on $\mathcal U$ for $x\in\mathcal D$; $D\ge\|u-v\|_2$ for all $u,v\in\mathcal U$; and $\|\nabla_u f_i(x,u)\|_2\le G$ for $x\in\mathcal D$, $u\in\mathcal U$. Write $P$ for the Euclidean projection onto $\mathcal U$.

Algorithm 1 sets $T=\lceil G^2D^2/\epsilon^2\rceil$ and $\eta=D/(G\sqrt T)$, starts from $u^0_1,\dots,u^0_m\in\mathcal U$, and for $t=1,\dots,T$ updates

$$u^t_i=P\bigl(u^{t-1}_i+\eta\,\nabla_u f_i(x^{t-1},u^{t-1}_i)\bigr),\qquad x^t=\mathcal O_\epsilon(u^t_1,\dots,u^t_m),$$

stopping with "infeasible" as soon as the oracle says so, and otherwise returning $\bar x=\frac1T\sum_{t=1}^T x^t$. In Lean these are alg1T, alg1Eta, alg1U, alg1X, alg1Output and alg1Calls in the namespace OracleRO.DualSubgrad.

Formalization targets

Goal: Theorem 3 (p. 7)

For every $\epsilon$-approximate oracle,

$$\text{output}=\text{"infeasible"}\ \Longrightarrow\ \neg\,\exists x\in\mathcal D\ \forall i\ \forall u\in\mathcal U:\ f_i(x,u)\le 0,$$ $$\text{output}=\bar x\ \Longrightarrow\ \bar x\in\mathcal D\ \text{ and }\ f_i(\bar x,u)\le 2\epsilon\ \ \forall i,\ \forall u\in\mathcal U,$$

and the number of oracle calls is at most $\lceil G^2D^2/\epsilon^2\rceil$.

Milestones

1. Lemma 1 (p. 5, Zinkevich 2003): projected online gradient ascent with step $\eta=D/(G\sqrt T)$ on concave rewards has regret $\sum_t f_t(x^*)-\sum_t f_t(x_t)\le GD\sqrt T$ for every $x^*$ in the decision set.
2. (6) (p. 7): if a point is returned, $\frac1T\sum_{t=1}^T f_i(x^t,u^t_i)\le\epsilon$ for every $i$.
3. (7) (p. 8): for every $i$ and $u\in\mathcal U$, $\frac1T\sum_t f_i(x^t,u)-\frac1T\sum_t f_i(x^t,u^t_i)\le GD/\sqrt T\le\epsilon$.
4. Final inequality of the proof (p. 8): $f_i(\bar x,u)\le\frac1T\sum_t f_i(x^t,u)$ for $u\in\mathcal U$.

Significance

The result. Theorem 3 turns any approximate solver of the nominal problem into an approximate solver of its robust counterpart, at a cost of $\lceil G^2D^2/\epsilon^2\rceil$ solver calls, a number that depends on the geometry of $\mathcal U$ and the sensitivity of the constraints to the noise but not on $n$, $d$ or $m$. It is the prototype of the paper's oracle-based reductions: the same primal–dual template, with a different online learner, gives the dual-perturbation algorithm of §3.2–3.3 for non-convex uncertainty sets, and the applications of §4 (robust linear programs, quadratic programs, semidefinite programs) instantiate it.

Formalizing it. The theorem is proved in the paper; none of it is machine-checked. A formal development adds a checked statement of the reduction with an explicit call count in place of the paper's $O(\cdot)$, and a reusable regret bound for projected online gradient ascent on concave rewards (Lemma 1), which the paper quotes from Zinkevich without proof and which many other online-learning results rest on.

Difficulty

The obvious argument for the dual side fails at one point: in round $t$ the primal point $x^t$ is computed from $u^t$, so the reward $f_i(x^t,\cdot)$ that the dual player faces depends on its own current move. A regret bound that assumed rewards fixed in advance, or drawn independently of the learner's play, would not apply. Lemma 1 must be used in its adversarial form, valid for every sequence of reward functions, including adaptively chosen ones. A second point is that the projection step requires the variational characterization of a nearest point in a convex set, which a mere "map into $\mathcal U$" does not provide.

Formalization scope

Points are elements of EuclideanSpace ℝ (Fin k), so every norm is the $\ell_2$ norm. The projection is a predicate IsProjOnto U P (each $P(y)$ is a nearest point of $\mathcal U$ to $y$), not a construction; the oracle is a function (Fin m → E d) → Option (E n) with none for "infeasible", constrained by the predicate IsApproxOracle on inputs in $\mathcal U^m$. The goal is quantified over every oracle meeting that specification. The gradient $\nabla_u f_i(x,u)$ is a given map gradU with HasGradientAt at points of $\mathcal U$; no differentiability in $x$ is assumed. Rounds are indexed by natural numbers with index $0$ for the initialization; the starting primal point $x^0\in\mathcal D$, used by the first update and left undefined by the algorithm, is an input. Hypotheses $D>0$ and $G>0$ are added so that $\eta$ and $T\ge1$ are meaningful. Maxima over $\mathcal U$ are stated as "for every $u\in\mathcal U$".

Explicit instantiations and corrections:

• The paper's "$O(G^2D^2/\epsilon^2)$ calls" is stated as at most $\lceil G^2D^2/\epsilon^2\rceil$ calls (one call per round, $T$ rounds).
• Lemma 1's "$G\ge\max_t\|f_t(x_t)\|$" is read as the gradient bound $\|\nabla f_t(x_t)\|\le G$, as the same sentence describes it.
• The proof's "Combining (10) and (12)" refers to (6) and (7).

Trivializing formalizations are ruled out: an oracle specification under which "infeasible" is never returned, or an output that is not the average of the oracle's answers, would not be Theorem 3. The "infeasible" conclusion is about the robust problem, not the nominal one.

A complete development needs the variational inequality for nearest points in a convex set, the gradient (supergradient) inequality for a concave function differentiable at a point of a convex set, Zinkevich's telescoping argument, and Jensen's inequality for finite averages. The first two and Lemma 1 are reusable beyond this mission. Proofs of the milestones, in any order, are welcome.

Selected references

• A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-Based Robust Optimization via Online Learning, arXiv:1402.6361v1, 2014; Operations Research 63(3), 2015. https://arxiv.org/abs/1402.6361v1
• M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization, 2016. https://arxiv.org/abs/1909.05207

Motivation

A retailer that sells products in several categories, channels or stores has to decide which products to offer in each. Customers substitute: a product left out of the assortment sends some of its demand to other products, and some of it away. The nested logit model (McFadden 1974, 1981) is the standard choice model for this situation. It groups products into nests, so that substitution within a nest differs from substitution across nests. Assortment optimization under this model asks which products to offer in each nest so as to maximize expected revenue.

Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) split the problem into four cases: dissimilarity parameters at most one or unrestricted, and nests that are fully or only partially captured. The problem is polynomially solvable in the first case and NP-hard in the other three. Every approximation guarantee in the paper for the hard cases (Theorems 7, 10, 11, 12) comes from one general framework, set up in §2: a linear program equivalent to the assortment problem, and Theorem 1, which turns a feasibility certificate for that linear program into a performance guarantee. This mission formalizes that framework.

Setting

There are $m$ nests $M$ and $n$ products $N = \{1, \dots, n\}$ in each nest. Product $j$ of nest $i$ has revenue $r_{ij} \ge 0$ and preference weight $v_{ij} > 0$, and the products in each nest are ordered so that $r_{i1} \ge \dots \ge r_{in}$. Nest $i$ has a no-purchase weight $v_{i0} \ge 0$ and a dissimilarity parameter $\gamma_i > 0$. The weight of choosing no nest at all is $v_0 \ge 0$. If the assortment $S_i \subseteq N$ is offered in nest $i$, write

$$V_i(S_i) = v_{i0} + \sum_{j \in S_i} v_{ij}, \qquad R_i(S_i) = \frac{\sum_{j\in S_i} r_{ij} v_{ij}}{V_i(S_i)}, \quad R_i(\emptyset) = 0 .$$

A customer picks nest $i$ with probability $Q_i = V_i(S_i)^{\gamma_i} / (v_0 + \sum_{l\in M} V_l(S_l)^{\gamma_l})$, and then a product of that nest by the multinomial logit model. The expected revenue is

$$\Pi(S_1, \dots, S_m) = \sum_{i \in M} Q_i(S_1, \dots, S_m)\, R_i(S_i),$$

and problem (2) is $Z^* = \max_{S_i \subseteq N} \Pi(S_1, \dots, S_m)$.

The linear program (3) in the variables $(x, y_1, \dots, y_m)$ minimizes $x$ subject to

$$v_0 x \ge \sum_{i\in M} y_i, \qquad y_i \ge V_i(S_i)^{\gamma_i}\big(R_i(S_i) - x\big) \quad \forall S_i \subseteq N,\ i \in M.$$

Given candidate collections $\{A_{it} : t \in \mathcal T_i\}$ of assortments for each nest, the linear program (4) is (3) with the second family of constraints imposed only for $S_i$ in the collection of nest $i$.

Formalization targets

Goal: Theorem 1 (p. 13)

Let $(\hat x, \hat y)$ be an optimal solution of (4), and let $\hat S_i$ solve $\max_{S_i \in \{A_{it}\}} V_i(S_i)^{\gamma_i}(R_i(S_i) - \hat x)$, problem (5), in every nest. If $(\alpha \hat x, \beta \hat y)$ is feasible for (3) for some $\alpha, \beta$, then, with $\hat Z = \Pi(\hat S_1, \dots, \hat S_m)$,

$$\alpha \hat Z \ \ge\ Z^* \ \ge\ \hat Z .$$

The theorem fixes no candidate collection and no value of $\alpha$. Each later section of the paper instantiates it with its own collection and its own factor, so a formal proof applies to all of them.

Milestones (§2, pp. 11–12)

1. Problem (2) is equivalent to (3): $Z^*$ is the least $x$ for which some $y$ makes $(x, y)$ feasible for (3).
2. At an optimal solution of (4), the first constraint binds at the maximizers $\hat S_i$ of (5), and $\hat x = \Pi(\hat S_1, \dots, \hat S_m)$.
3. Problem (4) relaxes (3), so $\hat x \le Z^*$.

Companions (§7, pp. 29–30)

• The tighter program (16), which lets each nest's assortment be a fractional vector $z_i \in [0,1]^n$, has every feasible $x$ above $Z^*$.
• Proposition 13: $\hat F_i(x) = \max_{z_i \in [0,1]^n} F_i(z_i \mid x)$ is convex, with subgradient $-(v_{i0} + \sum_j v_{ij}\hat z_{ij}(x))^{\gamma_i}$ at $x$.

Significance

Theorem 1 is the common step behind the paper's four approximation guarantees: the factor $\rho$ or $2\kappa$ of Theorem 7, the factor 2 of Theorem 10, the factor of Theorem 11, and the $\delta^{2\bar\gamma+1}$ of Theorem 12. Each of these reduces to checking that a scaled optimum of a small linear program is feasible for (3). With Theorem 1 formalized, those guarantees reduce to inequalities about candidate collections, which are the subject of the sister missions of this series. The upper bound (16) and Proposition 13 give the instance-specific bound that the paper uses to assess its assortments numerically.

The results are proved in the paper. To our knowledge none of them has a machine-checked proof. The formal work adds two things: the statements below are made exact at the degenerate inputs the prose passes over (an empty assortment, $v_0 = 0$), and a formal proof certifies the framework once for every later instantiation.

Difficulty

The equivalence of (2) and (3) rests on decomposing a maximum over joint assortments into a sum of per-nest maxima, and on reading the fractional objective $\Pi \le x$ as a linear constraint. Both steps need care where a denominator $v_0 + \sum_i V_i(S_i)^{\gamma_i}$ can vanish. The binding argument for (4) is a perturbation argument: lowering $\hat x$ must keep every constraint satisfiable, which needs a continuity and monotonicity property of the right-hand side in $x$. The obvious one-line reading of Theorem 1, "$\hat x = \hat Z$ and $\alpha\hat x \ge Z^*$", is correct only once both of these facts are established with their hypotheses. In particular, it is false when $v_0 = 0$ (see below). Proposition 13 requires that the supremum over the box be finite, which comes from the boundedness of $F_i$ on $[0,1]^n$.

Formalization scope

Nests are a finite type ι and products are Fin n, indexed $0, \dots, n-1$. An assortment is a finite set of products per nest, and a candidate collection is a set of such finite sets. Powers are real powers, and Lean's $x / 0 = 0$ gives $R_i(\emptyset) = 0$. $Z^*$ is $\Pi(S^*)$ for an arbitrary optimal assortment $S^*$; no supremum over assortments is taken. "Optimal solution of (4)" means feasible with minimal $x$, and "$\hat S_i$ solves (5)" means $\hat S_i$ belongs to the collection of nest $i$ and maximizes the objective of (5) over it at $\hat x$.

Standing assumptions and pins. These are $v_0, v_{i0} \ge 0$ and ordered revenues, together with $v_{ij} > 0$, $r_{ij} \ge 0$ and $\gamma_i > 0$. The paper allows zero-weight padding products and $\gamma_i = 0$, but its own conventions fail there. Theorem 1 and the binding milestone add $v_0 > 0$. The page allows $v_0 = 0$, but then Theorem 1 is false: take one nest with $v_{10} = 0$, $\gamma_1 = 1$, $r_{11} = v_{11} = 1$ and candidates $\{\emptyset, \{1\}\}$. Then $\hat x = 1$ and $\hat S_1 = \emptyset$ meet every hypothesis with $\alpha = \beta = 1$, yet $\hat Z = 0 < Z^* = 1$. The equivalence of (2) and (3) and the bound from (16) keep $v_0 \ge 0$, as the page does, and assume at least one nest and one product: with neither and $v_0 = 0$, every $x$ is feasible for (3).

A formalization that assumes the binding equality, the identity $\hat x = \hat Z$, or the inequality $\hat x \le Z^*$ in the goal would trivialize it. Those facts appear only as milestones. Likewise, reading "optimal solution of (4)" as mere feasibility would make the goal false rather than easier.

The development needs only finite sums, real powers and elementary order reasoning. Proposition 13 also needs the boundedness of a continuous function on a box and the convexity of a pointwise supremum of affine functions. Welcome contributions include proofs of the milestones, the goal from them, and reusable lemmas on the per-nest decomposition of maxima, which the sister missions of this series use as well.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 2014 (revised manuscript of June 18, 2013, cited here). https://doi.org/10.1287/opre.2014.1256
• D. McFadden, Econometric models of probabilistic choice, in C. Manski, D. McFadden (eds.), Structural Analysis of Discrete Data with Econometric Applications, MIT Press, 1981. https://eml.berkeley.edu/~mcfadden/discrete.html
• P. Rusmevichientong, D. Shmoys, H. Topaloglu, Assortment optimization with mixtures of logits, Technical report, Cornell University, 2010. https://people.orie.cornell.edu/huseyin/publications/publications.html
• M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, 2nd ed., Wiley, 1993. https://doi.org/10.1002/0471787779