All missions

Motivation

Data-dependent risk bounds in statistical learning replace combinatorial quantities such as the VC dimension with averages of how well a function class can fit random noise on the observed sample. Bartlett and Mendelson's article (JMLR 3, 2002) established these averages, the Rademacher and Gaussian complexities, as a general tool: a risk bound (their Theorem 8) holds with a complexity penalty, and the complexity of a complicated class can be bounded through structural results that relate it to the complexities of simpler classes.

This mission formalizes two of those structural results, both stated for Gaussian complexities. The first (Theorem 14) controls a Lipschitz function of several real-valued classes at once, the vector-valued analogue of the classical contraction principle. The second (Theorem 16) controls an arbitrary fixed boolean combination of classes of classifiers, such as intersections, unions or majority votes of a fixed number of base classifiers, by the sum of the complexities of the components. Such combinations arise whenever a classifier is assembled from simpler ones, for instance in decision lists, small decision trees over a base class, or voting schemes.

Setting

Let $\mathcal X$ be a set, $\mu$ a probability measure on it, and $n \ge 1$ a sample size. For a class $F$ of functions $\mathcal X \to \mathbb R$ and a sample $x = (x_1, \dots, x_n)$, the empirical Gaussian complexity is

$$\hat G_n(F)(x) = \mathbb E\left[\sup_{f\in F}\left|\frac2n\sum_{i=1}^n g_i f(x_i)\right|\right],$$

with $g_1, \dots, g_n$ independent standard Gaussian $N(0,1)$ variables, and the Gaussian complexity is $G_n(F) = \mathbb E\, \hat G_n(F)(X_1, \dots, X_n)$ for $X_1, \dots, X_n$ i.i.d. with law $\mu$ (Definition 2, p. 464). In Lean these are empiricalGaussian n F x and gaussianComplexity μ n F.

Three constructions of classes appear.

• Direct sum. With $\mathcal A = \mathbb R^m$ carrying the Euclidean distance, a class $F$ of maps $\mathcal X \to \mathcal A$ is a subset of the direct sum of real classes $F_1, \dots, F_m$ when each $f \in F$ is $x \mapsto (f_1(x), \dots, f_m(x))$ with $f_i \in F_i$ (SubsetDirectSum F Fi).
• Composition. For $\phi : \mathcal Y \times \mathcal A \to \mathbb R$, $\phi \circ f$ is $(x, y) \mapsto \phi(y, f(x))$ and $\phi\circ F$ collects these (compClass φ F).
• Boolean combination. For $g : \{\pm1\}^k \to \{\pm1\}$ and classes $F_1, \dots, F_k$ of $\{\pm1\}$-valued functions, $g(F_1, \dots, F_k) = \{x \mapsto g(f_1(x), \dots, f_k(x)) : f_j \in F_j\}$ (boolComb g F).

A centred Gaussian process indexed by a finite set $I$ is a family $(X_i)_{i \in I}$ of real random variables whose finite-dimensional laws are jointly Gaussian with mean zero; $\|X_i - X_j\|_2 = (\mathbb E(X_i - X_j)^2)^{1/2}$.

Formalization targets

Goal: Theorem 16 (p. 472)

For a fixed boolean function $g : \{\pm1\}^k \to \{\pm1\}$ with $k \ge 1$ and classes $F_1, \dots, F_k$ of $\{\pm1\}$-valued functions,

$$G_n\bigl(g(F_1, \dots, F_k)\bigr) \le 2 \sum_{j=1}^k G_n(F_j).$$

Milestones

1. Lemma 13 (p. 471), the comparison of Gaussian processes as printed: if $\|X_i - X_j\|_2 \le \|Y_i - Y_j\|_2$ for all $i, j$, then $\mathbb E\sup_i X_i \le 2\,\mathbb E\sup_i Y_i$.
2. Theorem 14 (p. 471): if each $\phi(y, \cdot)$ is $L$-Lipschitz for the Euclidean distance, passes through the origin, and $\phi$ is uniformly bounded, then for every sample $(x_k, y_k)_{k \le n}$,

$$\hat G_n(\phi \circ F) \le 2L \sum_{i=1}^m \hat G_n(F_i).$$

3. The extension of $g$ (proof of Theorem 16, p. 472): $g(x) = (1 - \|x - a\|)g(a)$ when $\|x - a\| < 1$ for a cube vertex $a$, and $0$ otherwise, is well defined, extends $g$, maps into $[-1,1]$, vanishes at $0$ and is $1$-Lipschitz.

Significance

Theorem 16 turns any bound on the Gaussian complexity of base classes into a bound for a fixed boolean combination of them, at the cost of a factor $2$ on the sum of their complexities, whatever $g$ and $k$ are. Together with the comparison between Gaussian and Rademacher complexities (Lemma 4 of the paper) and the risk bound of Theorem 8, it yields generalization bounds for classifiers built as combinations of base classifiers. Theorem 14 is the general tool: it handles any Lipschitz loss of a vector-valued predictor, such as multiclass margins, through the complexities of its coordinate classes.

All three results are proved in the paper (Lemma 13 is classical and cited from Pisier). None of them is formalized on Prove2Me; the finite-dimensional Sudakov–Fernique inequality, with constant $1$, is (HighDimProb.RandomProcesses.sudakov_fernique_finite_dim). This mission produces machine-checked versions of the vector contraction for Gaussian averages and of the boolean-combination bound, and records the corrections the printed statements need.

Difficulty

The obvious approach to Theorem 14 compares two Gaussian processes indexed by the class, but Definition 2 takes the supremum of an absolute value scaled by $2/n$, while Gaussian comparison inequalities bound the expected supremum of the process itself. The printed proof equates the two; done carefully, the comparison with the printed constant $2$ of Lemma 13 gives only $4L$. Reaching the printed $2L$ requires a comparison with constant $1$ and an argument that handles the absolute value. A second difficulty is that the classes may be infinite and unbounded, so expected suprema must be handled as extended-valued quantities, and the reduction to finite classes ("without loss of generality") must be justified. For Theorem 16 the extension of $g$ must be checked to be Lipschitz across the boundaries of the tents in the Euclidean, not the sup, norm.

Formalization scope

The source is the published JMLR article (vol. 3, 2002, pp. 463–482), not the COLT 2001 version, whose numbering differs.

• Complexities in $[0, \infty]$. $\hat G_n$ and $G_n$ are lower Lebesgue integrals of an ENNReal supremum against $N(0,1)^{\otimes n}$ and $\mu^{\otimes n}$. An unbounded class has complexity $+\infty$; a real-valued supremum or Bochner integral would silently return $0$ there and make the upper bounds false, so that encoding is ruled out. No finiteness or boundedness of any class is assumed.
• $\mathcal A = \mathbb R^m$ is EuclideanSpace ℝ (Fin m), so "Lipschitz" refers to the Euclidean distance as printed. Using Fin m → ℝ (the sup distance) would change the theorem.
• $\{\pm1\}$ is encoded as $\mathbb Z^\times$ coerced to $\mathbb R$.
• Lemma 13: centred processes added. As printed the lemma is false: $X_i \equiv 5$, $Y_i \equiv 0$ satisfy the hypothesis. Both processes are assumed mean zero, as in Slepian's lemma. The two processes may live on different probability spaces; the index set is any finite nonempty type. The constant $2$ is kept as printed.
• Theorem 14: printed proof loose, statement kept. The constant $2L$ is kept as printed; the statement is true via the constant-$1$ comparison. The uniform-boundedness hypothesis on $\phi$ is kept as printed although the extended-valued formulation does not need it.
• Theorem 16 and the extension: $k \ge 1$ added. For $k = 0$ the boolean function is a constant $\pm1$, the right side is $0$, and the left side is $\mathbb E\frac2n|\sum_i g_i| > 0$; also the extension would have $g(0) = \pm1$.
• Theorem 16: measurability guard. Each $\hat G_n(F_j)$ is assumed almost-everywhere measurable as a function of the sample, so that the expectation of $\sum_j \hat G_n(F_j)$ is the sum of the expectations. The paper does not discuss measurability.

A complete development needs Gaussian comparison for finite index sets (available on the platform), the reduction from infinite to finite classes for extended-valued suprema, and elementary Euclidean geometry of the cube. The first two are reusable for every Gaussian-average argument in learning theory. Proofs of any milestone, and of the constant-$1$ variant of Lemma 13 transported between probability spaces, are welcome.

Selected references

• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002), 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
• G. Pisier, The Volume of Convex Bodies and Banach Space Geometry, Cambridge University Press, 1989. https://doi.org/10.1017/CBO9780511662454
• M. Ledoux, M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4

Motivation

The multi-secretary problem is the basic model of selecting under a budget from a stream of offers. Hiring a fixed number of candidates, accepting a fixed number of requests for a perishable resource, and admitting customers into a capacity-limited service all have this structure. Each item must be accepted or rejected on arrival, and the comparison point is the offline decision maker, who sees the whole sequence and keeps the best $k$ items. The gap between the two expected values is the regret.

A common class of heuristics in revenue management and online resource allocation does not react to the realised history. These policies fix in advance, period by period, a probability of accepting each type of item, and then follow it until the budget runs out; static bid-price and randomised-acceptance rules are of this kind (Talluri and van Ryzin 2004). Arlotto and Gurvich (arXiv:1710.07719v2, Theorem 1) show that when abilities take finitely many values, an adaptive policy has regret bounded uniformly in the horizon $n$ and the budget $k$. Their Theorem 3 shows that the restriction to non-adaptive policies costs order $\sqrt n$ over a wide range of budgets. Read together, these two results separate adaptive from non-adaptive control by an unbounded factor. This mission formalizes the non-adaptive half.

Setting

There are $n$ candidates with abilities $X_1,\dots,X_n$, independent and identically distributed on $m$ values $0<a_m<a_{m-1}<\dots<a_1$, with masses $f_j=\mathbb P(X_1=a_j)>0$ and $\sum_jf_j=1$. Write $\epsilon=\tfrac12\min_jf_j$ and $\bar F(a_j)=f_1+\dots+f_{j-1}$. The budget is $k$, with $0\le k\le n$.

The offline value is

$$V^*_{\mathrm{off}}(n,k)=\mathbb E\Big[\max\Big\{\textstyle\sum_tX_t\sigma_t:\sigma\in\{0,1\}^n,\ \sum_t\sigma_t\le k\Big\}\Big].$$

A non-adaptive policy is a matrix $\pi=\{p_{j,t}\in[0,1]\}$. At time $t$, if budget remains and $X_t=a_j$, the candidate is selected with probability $p_{j,t}$, independently of everything else. The selection coins $B_t$ are then independent Bernoulli variables with $q_t=\mathbb E[B_t]=\sum_jp_{j,t}f_j$. The policy selects until $k$ coins have come up. Its value $V^\pi_{\mathrm{on}}(n,k)$ is the expected total ability selected, and

$$V^*_{\mathrm{na}}(n,k)=\sup_{\pi}V^\pi_{\mathrm{on}}(n,k).$$

The deterministic relaxation replaces the random counts $Z^n_j=\#\{t:X_t=a_j\}$ by their means. Its value is

$$DR(n,k)=\max\Big\{\textstyle\sum_ja_js_j:0\le s_j\le nf_j,\ \sum_js_j\le k\Big\},$$

with solution $s^*_j=\min\{nf_j,(k-n\bar F(a_j))_+\}$. The index policy takes its probabilities from $s^*$: $p_{j,t}=s^*_j/(nf_j)$.

Formalization targets

Goal: Theorem 3 (p. 25)

For every $\epsilon>0$, $m$ and $a$ there is $M=M(\epsilon,m,a)>0$ such that, for all masses with $\tfrac12\min_jf_j=\epsilon$ and all $(n,k)$ with $(f_1+\epsilon)n\le k\le(1-f_m-\epsilon)n$,

$$M\sqrt n\le V^*_{\mathrm{off}}(n,k)-V^*_{\mathrm{na}}(n,k).$$

The constant does not depend on the masses beyond $\epsilon$, nor on $n$ or $k$.

Milestones

• Lemma 2 (p. 8): binomial overshoot, $\mathbb E[(B-k)_+]\le1/(4\varepsilon)$ when $k$ exceeds the mean by $\varepsilon n$, and the symmetric bound.
• Remark 2 (pp. 10–11): $s^*$ solves the relaxation, and $V^*_{\mathrm{off}}\le DR$.
• Lemma 3 (p. 25): the index policy satisfies $DR-V^{\mathrm{id}}_{\mathrm{na}}\le\varepsilon^{-1}a_1\sqrt n$ when $k/n\ge\varepsilon$, so the order $\sqrt n$ is attained.
• Lemma 5 (p. 26): for a centred Bernoulli sum with variance $\varsigma^2$, $\mathbb E[(\pm N-\Upsilon\varsigma)_+]\ge\beta_1\varsigma-(2+3\sqrt2)$ with $\beta_1(\Upsilon)>0$, and $\mathbb E[(N+\Upsilon\varsigma)_+^2]\le\beta_2\varsigma^2$.
• Lemma 7 (p. 27): an optimal non-adaptive policy exists, and any optimal one has $f_1/2\le q_t\le1-f_m/2$ outside $2M\sqrt n$ periods, so $\sum_tq_t(1-q_t)\ge\tfrac{f_1f_m}4(n-2M\sqrt n)$.
• Lemma 4 (p. 25): for $k\le n(f_1-\epsilon)$ the non-adaptive regret is at most $a_2/(4\epsilon)$.
• Lemma 8 and Proposition 6 (p. 40): $\mathbb E[\mathfrak S^n_j]=s^*_j\pm M\sqrt n$, and $0\le DR-V^*_{\mathrm{off}}\le M\sqrt n$ in general and $\le a_1m/(4\epsilon')$ when $k/n$ is $\epsilon'$ away from the jump points of $\bar F$.

Significance

Theorem 3 is the lower half of the separation in Theorem 1 of the paper. The Budget-Ratio policy and the dynamic-programming policy have regret $O(1)$, uniformly in $(n,k)$, while every non-adaptive policy has regret $\Omega(\sqrt n)$ when $k/n$ lies strictly between $f_1$ and $1-f_m$. The order $\sqrt n$ of fluid and static randomised policies is therefore a property of the whole class, not of a poor choice inside it. Lemma 4 shows that the budget range cannot be removed: with a small budget a non-adaptive policy is as good as any.

The result is proved in the source but has not been machine-checked. A complete development would formalize, inside one finite probabilistic model: the binomial overshoot bound, a uniform anti-concentration estimate for Bernoulli sums, the structure of optimal non-adaptive policies, and the comparison with the offline sort. The source's proof of Theorem 3 also relies on a lemma that fails as printed (see Formalization scope), so a formal proof would close a real gap in the published argument.

Difficulty

The upper bound of order $\sqrt n$ (Lemma 3) follows from a variance computation. The lower bound must hold for every non-adaptive policy, including time-varying ones, and the obvious argument does not cover them. That argument compares a policy with the index policy and shows the index policy loses $\sqrt n$. A policy can, however, differ from the index policy by order $\sqrt n$ in its expected selection counts and still have regret of the same order. The step "small regret forces $s_j(\pi)\approx s^*_j$", which the source uses, is exactly the step that fails.

What has to be shown is that the selection count $\sum_tB_t$ of an optimal policy fluctuates by order $\sqrt n$, uniformly in the policy. A policy that runs out of budget early then misses top-value candidates late in the horizon, and one that keeps budget wastes slots. Both effects must be bounded below by a multiple of $\sqrt n$ that is uniform over all masses with the same $\epsilon$. Lemma 5 needs a normal approximation with an explicit, $q$-independent error. Lemma 7 needs the existence of an optimal policy, which is a maximisation over a continuum of matrices.

Formalization scope

The source is the arXiv preprint arXiv:1710.07719v2 (1 June 2018). Its printed page numbers equal the PDF page numbers.

• Indices. The value and mass vectors are a f : Fin m → ℝ. Lean index $j$ is the paper's index $j+1$, so a 0 $=a_1$ is the largest value and f (Fin.rev 0) $=f_m$ is the mass of the smallest. The standing assumptions of Sec. 2 are IsValues a (strictly decreasing, positive) and IsMasses f (positive, summing to one).
• Expectations. All expectations are finite sums over outcome sequences. For the offline problem these are $x:\mathrm{Fin}\,n\to\mathrm{Fin}\,m$ with weight $\prod_tf_{x_t}$. For a non-adaptive policy they are pairs $(X_t,B_t)$ with weight $\prod_tf_{x_t}\,p_{x_t,t}^{b_t}(1-p_{x_t,t})^{1-b_t}$. No measure theory is used.
• Selection rule. A candidate is selected iff its coin is $1$ and fewer than $k$ earlier coins were $1$. This equals the paper's "up to the stopping time $\nu$" for $k\ge1$. At $k=0$ the printed $\nu=1$ would allow a selection without budget, and the feasible rule is used.
• Suprema. $V^*_{\mathrm{na}}$ is a supremum over all matrices with entries in $[0,1]$, not over $0/1$ matrices or the index policy alone. $DR$ is the supremum of its linear program; it is not defined by the formula $\sum_ja_js^*_j$, which is a milestone.
• Index policy. $j_{\mathrm{id}}$ is the largest index with $\bar F(a_{j_{\mathrm{id}}})\le k/n$. As printed the defining inequality has no solution at $k=n$.
• Constants. Each constant is quantified after $(\epsilon,m,a)$ and before $(f,n,k)$. The goal's $M$ and Lemma 5's $\beta_1$ are strictly positive; with $M=0$ the goal would reduce to $V^*_{\mathrm{na}}\le V^*_{\mathrm{off}}$. Theorem 3 is posed for all $n$ in the range, as printed, without a threshold on $n$. Lemma 2 is stated in the multiplied form $(p+\varepsilon)n\le k$ of its proof. Lemma 4 adds $m\ge2$, so that $a_2$ exists.
• Disclosed gaps in the source. The source's proof of Theorem 3 relies on a lemma that fails as printed (Lemma 6, p. 26), so Lemma 6 is not part of this mission. The statement of Theorem 3 is posed as in the source. The printed argument for the second inequality of Lemma 7's (36) does not go through, and a corrected one also uses $a_{m-1}$. Lemma 7's constant is therefore quantified after all of $a$.

Contributions of any kind are welcome. Reusable pieces include binomial overshoot bounds, anti-concentration for sums of independent Bernoulli variables (for example via a Wasserstein normal approximation, which Mathlib lacks), and compactness arguments for optimal randomised policies.

Selected references

• A. Arlotto, I. Gurvich, Uniformly Bounded Regret in the Multi-Secretary Problem, arXiv:1710.07719v2, 2018; Stochastic Systems 9(3), 2019. https://arxiv.org/abs/1710.07719v2
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000
• N. Ross, Fundamentals of Stein's method, Probability Surveys 8, 2011. https://doi.org/10.1214/11-PS182
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

Motivation

The multi-secretary problem is the simplest model of capacity allocation under uncertainty: a decision maker sees $n$ candidates one at a time and may hire at most $k$ of them, with every decision final. The same structure underlies single-resource revenue management (accepting or rejecting booking requests against a fixed inventory; see Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004), online knapsack and packing problems, and dynamic assortment of limited stock.

The performance of an online policy is measured against the offline benchmark, the value of the best $k$ candidates chosen with full hindsight. The gap between the two is the regret.

• In the version where the values arrive as a uniform random permutation, Kleinberg (2005) proved that the minimal regret is of order $\sqrt k$ and gave an algorithm attaining it (as summarized in Remark 1 of the paper below).
• Arlotto and Gurvich (arXiv:1710.07719, 2017; Stochastic Systems 2019) showed that when the values have a finite support, the optimal online policy, and an explicit simple policy, have regret bounded by a constant that does not depend on $n$ or $k$. The constant depends only on the smallest probability mass.

This mission formalizes that upper bound.

Setting

Abilities take values in a finite set $\mathcal A=\{a_m<a_{m-1}<\dots<a_1\}$ of distinct positive reals, with probabilities $f_j=\mathbb P(X=a_j)>0$, $\sum_j f_j=1$. Write $\bar F(a_j)=f_1+\dots+f_{j-1}$ for the mass strictly above $a_j$, and

$$\epsilon=\tfrac12\min\{f_m,\dots,f_1\}.$$

The abilities $X_1,\dots,X_n$ are independent with this distribution. Budget pairs range over the triangle $\mathcal T=\{(n,k):0\le k\le n\}$.

• Offline value. $V^*_{\mathrm{off}}(n,k)=\mathbb E\big[\max\{\sum_t X_t\sigma_t:\sigma\in\{0,1\}^n,\ \sum_t\sigma_t\le k\}\big]$.
• Online policies. A policy decides $\sigma_t\in\{0,1\}$ using only $X_1,\dots,X_t$ and must select at most $k$ candidates on every realization. $\Pi(n,k)$ is the set of such policies, $V^\pi_{\mathrm{on}}(n,k)=\mathbb E[\sum_t X_t\sigma^\pi_t]$, and $V^*_{\mathrm{on}}(n,k)=\max_{\pi\in\Pi(n,k)}V^\pi_{\mathrm{on}}(n,k)$.
• Counts. $Z^r_j$ is the number of $a_j$-candidates among the first $r$. The offline sort selects $\mathfrak S^r_j=\min\{Z^r_j,(k-\sum_{i<j}Z^r_i)_+\}$ of them. $S^{\pi,r}_j$ counts those selected by $\pi$.
• Action index. $j_0(n,k)$ is the largest $j$ with $\bar F(a_j)+\tfrac12f_j\le k/n$, or $1$ if there is none.
• Thresholds. $T_1=0$, $T_j=\bar F(a_j)+\tfrac12 f_j$ for $2\le j\le m$, and $T_{m+1}=+\infty$.
• Budget-Ratio (BR) policy. With remaining budget $K_t$ ($K_0=k$), at time $t+1$ the policy finds $j$ with $T_j\le K_t/(n-t)<T_{j+1}$. It selects $X_{t+1}$ if and only if $K_t>0$ and $X_{t+1}\ge a_j$.
• Stopping times. For $0<\delta<\epsilon$, $\tau_0$ is the first time the budget ratio comes within $\delta/2$ of a threshold, or the cut-off $n-2\delta^{-1}-1$. The time $\tau$ of (20) is the first later time the ratio leaves the $\delta$-band around that threshold, or the cut-off.

Formalization targets

Goal: Theorem 1 (first display)

For every $\epsilon>0$ there is a constant $M$ such that for every instance with $\tfrac12\min_jf_j=\epsilon$ and all $(n,k)\in\mathcal T$, $\mathrm{br}\in\Pi(n,k)$ and

$$V^*_{\mathrm{off}}(n,k)-V^*_{\mathrm{on}}(n,k)\le V^*_{\mathrm{off}}(n,k)-V^{\mathrm{br}}_{\mathrm{on}}(n,k)\le a_1M.$$

No constant is fixed. Only the shape is asserted: a bound uniform in $n$, $k$, the support size and the distribution, given $\epsilon$.

Milestones, in the order the proof uses them

• The benchmark inequality $V^\pi_{\mathrm{on}}\le V^*_{\mathrm{off}}$ (p. 5).
• The sort identity $V^*_{\mathrm{off}}=\sum_ja_j\mathbb E[\mathfrak S^n_j]$ (4).
• The binomial overshoot bound $\mathbb E[(B-k)_+]\le1/(4\varepsilon)$ (Lemma 2).
• The offline decomposition $V^*_{\mathrm{off}}=\sum_{i<j}a_i\mathbb E[Z^n_i]+a_j\mathbb E[\mathfrak S^n_j]+a_{j+1}\mathbb E[\mathfrak S^n_{j+1}]\pm a_1/(4\epsilon)$ (Proposition 1).
• The sufficient condition: four properties (i)–(iv) of a policy up to a stopping time imply regret at most $3a_1M+a_1/(4\epsilon)$ (Proposition 2).
• The identification $j_0(n,k)=j$ on $k/n\in[T_j,T_{j+1})$ (p. 17).
• The BR selection probability and the jump bound $|K_t/(n-t)-K_{t+1}/(n-t-1)|\le\delta/2$ (p. 13).
• $\mathbb E[\tau]\ge n-M$ (Theorem 2).
• BR and $\tau$ satisfy (i)–(iv) (Corollary 1).
• The state-space reduction $v_\ell(w,\kappa)=w+g_\ell(\kappa)$ of the Bellman recursion (Proposition 5).

Significance

The result. Bounded regret means that the loss from not knowing the future is a fixed number of candidates' worth of value, however long the horizon and however large the budget. The bound holds uniformly over all distributions with the same $\epsilon$. It is attained by an explicit, adaptive, non-randomized rule that compares one ratio with $m$ fixed thresholds. The companion result of the same paper shows that every non-adaptive policy suffers regret of order $\sqrt n$ in the interior regime. Together they quantify the value of adapting to the remaining budget. Lemma 1 of the paper shows the dependence on $\epsilon$ cannot be removed.

Formalizing it. The result is proved in the paper, but no part of it is machine-checked; there is no multi-secretary or bounded-regret development on the platform. The mission produces several pieces of machinery: a reusable finite model of sequential selection with online policies and the offline benchmark; an explicit online policy with its stopping-time analysis; and a binomial overshoot bound usable elsewhere. The constant $M$ is not made explicit in the paper. A formal proof would give one, and sharper constants are welcome.

Difficulty

The offline decomposition and the sufficient condition are bookkeeping with counts and one concentration bound. The hard step is Theorem 2: showing that the budget ratio $K_t/(n-t)$ stays within $\delta$ of its attracting threshold until a bounded expected number of periods before the end. Near the horizon a single selection moves the ratio by about $1/(n-t)$, so the band becomes easy to leave. Equivalently, the target $\delta(n-\tau_0-u)$ that the deviation process must exceed shrinks to zero. A standard martingale or drift argument with a fixed band therefore does not give a bound uniform in $n$. The paper combines the mean-reverting drift of the deviation process with an exponential tail bound (its Proposition 4) and a Lyapunov argument. A second subtlety is uniformity: every constant must depend on $\epsilon$ (and $\delta$) only, never on $m$, the $a_j$, $n$ or $k$.

Formalization scope

The source is arXiv:1710.07719v2; its printed page numbers equal the PDF page numbers.

Representation.

• Ability levels are Fin m, with index 0 the largest value $a_1$; Lean index $i$ is the paper's $i+1$.
• Each instance carries $a$ strictly decreasing and positive, $f$ positive with $\sum f=1$.
• Expectations are finite sums over sequences $x:\mathrm{Fin}\,n\to\mathrm{Fin}\,m$ weighted by $\prod_tf(x_t)$, so no measure theory is needed.
• Policies are deterministic selection rules $\sigma(x,t)$ that are non-anticipating and feasible. $V^*_{\mathrm{on}}$ is a maximum over this finite set. The paper allows randomized policies; for this finite problem the optimal values coincide (p. 39). In any case, restricting to deterministic policies can only lower $V^*_{\mathrm{on}}$ and so does not weaken the goal.
• $V^*_{\mathrm{off}}$ is defined as an expected maximum over selection vectors, not by the sort formula. The sort formula is a milestone.

Quantifiers. The constant $M$ in the goal is chosen after $\epsilon$ and before $m$, the instance, $n$ and $k$. A statement with $M$ chosen after the instance, or after $n$, is trivial (regret $\le a_1n$) and is excluded.

Corrections to the printed text, disclosed in the items.

1. In Theorem 2 and Corollary 1, $M$ depends on the auxiliary $\delta\in(0,\epsilon)$ as well, because $\tau$ does. $\delta$ is quantified before $M$. The goal itself is $\delta$-free.
2. Lemma 2's conditions $p+\varepsilon\le k/n$, $k/n\le p-\varepsilon$ are stated as $(p+\varepsilon)n\le k$, $k\le(p-\varepsilon)n$, the form used in its proof. This avoids a false case at $n=0$.
3. The BR rule is applied at every time $t+1\in\{1,\dots,n\}$; p. 11 writes $\{1,\dots,n-1\}$.
4. $\tau$ is capped at $n$, which matters only when $n=0$.
5. In Proposition 5 the recursions are imposed for $\kappa\ge1$ (boundary conditions at $\kappa=0$), and only identity (49) is stated.

Infrastructure. The model definitions (instance, offline value, online policies, counts, thresholds, action index) and the binomial overshoot lemma are reusable for other finite-support online selection and revenue-management results. All of the following are welcome:

• proofs of individual milestones;
• an explicit constant;
• a formal derivation of $V^*_{\mathrm{on}}(n,k)=v_n(0,k)$ connecting Proposition 5 to $V^*_{\mathrm{on}}$.

Selected references

• A. Arlotto, I. Gurvich, Uniformly Bounded Regret in the Multi-Secretary Problem, arXiv:1710.07719v2, 2018; Stochastic Systems 9(3), 2019. https://arxiv.org/abs/1710.07719
• R. Kleinberg, A multiple-choice secretary algorithm with applications to online auctions, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070519
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

Motivation

Assortment optimization asks which set of products a firm should offer when customers choose among the offered products according to a discrete choice model; it underlies shelf-space planning in retail and fare-class control in airline revenue management (Talluri and van Ryzin, 2004). Under the nested logit model products are grouped into nests, and a customer first picks a nest and then a product inside it. Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) map out how hard this problem is across variants of the model.

When every nest dissimilarity parameter is at most one and a customer who chose a nest always buys there, offering the top-revenue products of each nest is optimal (Theorem 4 of the paper, the subject of an earlier mission of this series). Once a customer may leave a nest without buying — a partially-captured nest — that structure breaks and the problem becomes NP-hard (Theorem 8). This mission targets the paper's response: a small, explicitly constructed family of candidate assortments per nest from which a linear program recovers a solution within a factor of two of optimal.

Setting

There are $m$ nests $M$ and, in each nest, $n$ products $N = \{1, \dots, n\}$. Product $j$ of nest $i$ has a revenue $r_{ij} \ge 0$ and a preference weight $v_{ij} > 0$, with $r_{i1} \ge \dots \ge r_{in}$. Nest $i$ has a dissimilarity parameter $\gamma_i > 0$ and a within-nest no-purchase weight $v_{i0} \ge 0$; $v_0 \ge 0$ is the weight of choosing no nest. For an assortment $S_i \subseteq N$,

$$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,$$

and the expected revenue of $(S_1, \dots, S_m)$ is $\Pi = \sum_i V_i(S_i)^{\gamma_i} R_i(S_i) / (v_0 + \sum_i V_i(S_i)^{\gamma_i})$. The optimal expected revenue $Z^*$ is the optimal value of the linear program

$$\text{(3)}\quad \min\ x \quad\text{s.t.}\quad 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)\ \ \forall S_i \subseteq N,\ i \in M,$$

and problem (4) is the same program with the second family of constraints imposed only for a chosen collection of candidate assortments in each nest.

Throughout, $\gamma_i \le 1$ for every nest and the $v_{i0}$ are arbitrary. For a capacity $\epsilon_i \ge 0$, the knapsack value $K_i(\epsilon_i)$ is the largest $\sum_{j \in S} r_{ij} v_{ij}$ over assortments $S$ with $\sum_{j \in S} v_{ij} \le \epsilon_i$ (display (9)). Its continuous relaxation (11) allows fractional $z_{ij} \in [0, \mathbf 1(v_{ij} \le \epsilon_i)]$ under the same capacity. The greedy solution $\hat z_i(\epsilon_i)$ of (11) fills the capacity with the products of weight at most $\epsilon_i$ in revenue order, each fully while it fits and the next one fractionally, and

$$\hat S_i(\epsilon_i) = \{ j \in N : \hat z_{ij}(\epsilon_i) = 1 \}.$$

Problem (10) replaces the per-assortment constraints of (3) by $y_i \ge \max_{\epsilon_i \ge 0} (v_{i0}+\epsilon_i)^{\gamma_i}[K_i(\epsilon_i)/(v_{i0}+\epsilon_i) - x]$.

Formalization targets

Goal: Theorem 10 (p. 24)

Let $(\hat x, \hat y)$ be an optimal solution of (4) with candidate collections $\{\hat S_i(\epsilon_i) : \epsilon_i \in [0,\infty]\} \cup \{\{j\} : j \in N\}$. Then

$$(2\hat x,\ 2\hat y) \ \text{ is feasible for (3).}$$

Milestones

1. Per-nest identity (proof of Lemma 9, p. 23). For $x \ge 0$, $\max_{S_i} V_i(S_i)^{\gamma_i}(R_i(S_i) - x) = \max_{\epsilon_i \ge 0}(v_{i0}+\epsilon_i)^{\gamma_i}[K_i(\epsilon_i)/(v_{i0}+\epsilon_i) - x]$.
2. Lemma 9 (p. 23). Problems (3) and (10) have the same optimal solutions.
3. Relaxation (p. 23). Every feasible point of (9) is feasible for (11), so $\hat K_i(\epsilon_i) \ge K_i(\epsilon_i)$.
4. Greedy solution (pp. 23–24). $\hat z_i(\epsilon_i)$ is optimal for (11) and has at most one fractional component.
5. Sign (A.3, p. 45). $\hat x \ge 0$.
6. Inequalities (28) and (29) (A.3, pp. 45–46). In both cases — $\hat z_i(\epsilon)$ with and without a fractional component — $2\hat y_i \ge (v_{i0}+\epsilon)^{\gamma_i}[K_i(\epsilon)/(v_{i0}+\epsilon) - 2\hat x]$.

Two further statements accompany the goal: the factor-two revenue guarantee obtained from Theorem 10 and Theorem 1 of the paper, and the fact that every $\hat S_i(\epsilon_i)$ is one of the at most $1 + n^2$ assortments $N^k_{ij}$, the first $j$ products by revenue among the $k$ lightest.

Significance

Theorem 10 turns an NP-hard assortment problem into a linear program with $1 + m$ variables and $1 + m(1 + n + n^2)$ constraints whose solution is within a factor of two of optimal. The construction is explicit: the candidates are defined by a greedy rule, not by an optimization oracle. The same template, a restricted linear program whose doubled optimum is feasible for the full one, is reused in §6 of the paper for the most general instances, and Lemma 9's knapsack reformulation is the link to the classical approximation theory of knapsack problems (Williamson and Shmoys, 2011).

The theorem is proved in the paper. No machine-checked proof of it, of Lemma 9, or of greedy optimality for the continuous knapsack with an eligibility bound exists on the platform. Formalizing it yields a checked factor-two guarantee and a reusable fractional-knapsack development.

Difficulty

The obvious argument would compare the restricted program (4) with (3) constraint by constraint. That fails: (3) has one constraint per subset of products, and most subsets are not candidates. The comparison has to pass through the knapsack reformulation (10), which requires showing that a maximum over all subsets equals a maximum over a one-dimensional capacity parameter, using $\gamma_i \le 1$ and $x \ge 0$ in an essential way. The second obstacle is that the greedy assortment $\hat S_i(\epsilon_i)$ keeps only the fully taken products, so its value can fall short of the continuous knapsack value, and no single candidate assortment need attain the knapsack bound. With dissimilarity parameters above one the monotonicity behind the reformulation is lost, and §6 of the paper needs a different factor.

Formalization scope

Products are Fin n (indices $0, \dots, n-1$), nests a finite type, and every quantity is real. Powers are Real.rpow; $x/0 = 0$, which gives $R_i(\emptyset) = 0$. An optimal solution of a linear program is a feasible pair whose $x$ is minimal among feasible pairs. The constraint "$y_i \ge \max_{\epsilon_i \ge 0}(\dots)$" of (10) is stated in constraint form, for every $\epsilon_i \ge 0$, so no real supremum is taken. $K_i(\epsilon)$ is defined for $\epsilon \ge 0$ only; its placeholder value for $\epsilon < 0$ is never used. Ties in revenue (and, for $N^k_{ij}$, in weight) are broken by index. The candidate collection is taken over real $\epsilon_i \ge 0$; $\epsilon_i = \infty$ adds nothing, since every capacity of at least $\sum_j v_{ij}$ already gives $\hat S_i = N$.

Standing assumptions and added hypotheses: $\gamma_i \le 1$ for every nest (the section's assumption) on the goal and on every model milestone; the pins $v_{ij} > 0$, $r_{ij} \ge 0$, $\gamma_i > 0$ and the revenue ordering, shared by the series; $n \ge 1$ on Lemma 9, on $\hat x \ge 0$ and on (28)/(29), the paper's nonempty $N$; and $v_0 > 0$ on the factor-two revenue guarantee, where Theorem 1 of the paper fails without it.

The greedy assortments $\hat S_i(\epsilon_i)$ are defined explicitly. Quantifying over arbitrary optimal solutions of (11) instead would change the candidate collection and is not the paper's theorem. The goal states feasibility for the full program (3) and does not mention knapsack values, the greedy solution or the case split. A formalization that weakens the conclusion to feasibility for (10), or that drops the singletons from the candidate collection, is not a solution.

Needed infrastructure: fractional knapsack optimality of the greedy rule with an eligibility bound, monotonicity of $t \mapsto t^{\gamma}$ and $t \mapsto t^{\gamma - 1}$ for $\gamma \le 1$, and finite maximization over subsets. The fractional-knapsack lemmas are reusable beyond this mission. Proofs of any milestone, and alternative decompositions of the goal, are welcome.

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). DOI 10.1287/opre.2014.1256
• K. T. Talluri, G. J. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 15–33, 2004. DOI 10.1287/mnsc.1030.0147
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. DOI 10.1017/CBO9780511921735

Motivation

A retailer choosing which products to display, or an airline choosing which fare classes to open, solves an assortment optimization problem: pick the set of offered products that maximizes expected revenue when customers choose among what is offered according to a discrete choice model. Under the multinomial logit model the answer has a simple form: an optimal assortment consists of the few highest-revenue products (Talluri and van Ryzin, 2004). The multinomial logit model, however, forces every pair of products to compete in the same way. The nested logit model relaxes this by grouping products into nests (brands, store sections, departure times) and letting a customer first choose a nest and then a product inside it.

Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) study how much of the multinomial logit structure survives under the nested logit model. Their first answer is the theorem this mission targets: when the nest dissimilarity parameters are at most one and no customer who chose a nest leaves it without buying, offering the top products of each nest is still optimal. The other missions of this series treat the cases where this fails: dissimilarity parameters above one (the problem becomes NP-hard) and nests with their own no-purchase option.

Setting

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

An assortment is a tuple $(S_1, \dots, S_m)$ of subsets $S_i \subseteq N$. 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, inside the nest, product $j$ with probability $v_{ij}/V_i(S_i)$. The expected revenue is

$$\Pi(S_1, \dots, S_m) = \sum_{i \in M} Q_i\, R_i(S_i) = \frac{\sum_{i \in M} V_i(S_i)^{\gamma_i} R_i(S_i)}{v_0 + \sum_{i \in M} V_i(S_i)^{\gamma_i}},$$

and problem (2) asks for $Z^* = \max \Pi(S_1, \dots, S_m)$ over all assortments. The nested-by-revenue assortment $N_{ij} = \{1, \dots, j\}$ collects the $j$ highest-revenue products of nest $i$, with $N_{i0} = \emptyset$ and $N_+ = \{0, 1, \dots, n\}$.

This mission works under the standing assumptions of §3 of the paper: competitive products, $\gamma_i \le 1$, and fully-captured nests, $v_{i0} = 0$, for every nest $i$.

Formalization targets

Goal: Theorem 4 (p. 15)

If $\gamma_i \le 1$ and $v_{i0} = 0$ for all $i \in M$, there exists an optimal solution $(S^*_1, \dots, S^*_m)$ of problem (2) such that

$$S^*_i = N_{ij} \ \text{ for some } j \in N_+, \qquad \text{for all } i \in M.$$

Milestones

1. The case $v_0 = 0$ (p. 14). Offering only the single product with the largest revenue $\max_{i} r_{i1}$ is optimal.
2. Proposition 2 (p. 14). If $S^*$ is optimal and $S^*_i \ne \emptyset$, then $R_i(S^*_i) \ge Z^*$.
3. Lemma 3 (p. 14). If $Z = \Pi(S)$, $R_i(S_i) \ge Z$ and some $j \in S_i$ has $r_{ij} < \gamma_i Z + (1-\gamma_i) R_i(S_i)$, removing $j$ strictly increases the expected revenue.
4. $g(\alpha) \le \gamma$ (p. 15). For $0 < \gamma \le 1$ and $0 < \alpha < 1$: $(1 - \alpha^{\gamma})/(\alpha^{\gamma-1} - \alpha^{\gamma}) \le \gamma$.
5. Revenue threshold (p. 15). Every $j \in S^*_i$ of an optimal $S^*$ has $r_{ij} \ge \gamma_i Z^* + (1-\gamma_i) R_i(S^*_i)$.
6. $h(\alpha) \ge \gamma$ (p. 16). For $0 < \gamma \le 1$ and $0 < \alpha < 1$: $(1 - \alpha^{\gamma})/(1 - \alpha) \ge \gamma$.
7. Exchange step (p. 15). If $S^*$ is optimal, $j \in S^*_i$, $k \notin S^*_i$ and $k < j$, then adding $k$ to $S^*_i$ keeps the assortment optimal.

A companion item (not a milestone) states the algorithmic consequence at the end of §3: solving the linear program (4) over the candidates $\{N_{ij} : j \in N_+\}$ and choosing in each nest a maximizer of problem (5) gives an optimal solution of (2).

Significance

Theorem 4 reduces problem (2), a search over $2^{mn}$ assortments, to $(n+1)^m$ nested-by-revenue combinations, and the paper then finds the best one with a linear program with $1 + m$ variables and $1 + m(1+n)$ constraints. It marks the exact boundary of the classical multinomial logit structure inside the nested logit model: the paper's §4 shows that a single nest with $\gamma_i > 1$ already breaks it, and that the general problem is NP-hard. The structural statement is also the base case for the approximation guarantees of §§5–6, which compare against nested-by-revenue assortments.

The theorem is proved in the paper; to our knowledge it has no machine-checked proof. A formal proof would supply a verified reduction from a combinatorial revenue maximization over the nested logit model to a polynomial-size search, with every boundary case (empty nests, $v_0 = 0$, ties in revenues) handled explicitly.

Difficulty

The obvious argument copies the multinomial logit proof: take an optimal assortment and swap a low-revenue product for a missing higher-revenue one. Under the nested logit model this exchange changes the nest's attraction $V_i(S_i)^{\gamma_i}$ non-linearly, so the revenue of the modified assortment is not an affine function of the change, and a simple swap can lower the expected revenue. The argument must instead control how adding or removing one product moves the nest weight relative to the nest revenue, and this is exactly where $\gamma_i \le 1$ enters, through two scalar inequalities in the ratio $\alpha$ of nest weights. With $\gamma_i > 1$ these inequalities fail and so does the theorem.

A second subtlety is ties: several optimal assortments may exist, and only some of them are nested by revenue. The statement asserts existence, not that every optimum has this form.

Formalization scope

All statements live in the namespace NestedLogitVariants.Competitive and share one definition file. Nests form a finite type ι with decidable equality; products are Fin n, indexed $0, \dots, n-1$, so $N_{ij}$ is nbr n j $= \{k : k < j\}$ with $j \le n$, and $j = 0$ gives $\emptyset$. Powers are Real.rpow, and $x / 0 = 0$, which gives $R_i(\emptyset) = 0$. Optimality of an assortment means its revenue is at least that of every assortment.

Standing assumptions carried as hypotheses: $v_0 \ge 0$, $v_{i0} \ge 0$, revenues ordered within each nest, and §3's $\gamma_i \le 1$ and $v_{i0} = 0$. Three pins are disclosed: $v_{ij} > 0$ (the paper allows zero-weight padding products, under which Proposition 2 fails), $r_{ij} \ge 0$, and $\gamma_i > 0$ (the paper's $\gamma_i \ge 0$; its convention $V_i(\emptyset)^{\gamma_i} = 0$ fails at $\gamma_i = 0$). The section's "without loss of generality $v_0 > 0$" is a hypothesis of Proposition 2, Lemma 3, the threshold, the exchange step and the LP item; the goal itself only assumes $v_0 \ge 0$, and the case $v_0 = 0$ is milestone 1. The two scalar inequalities are stated as inequalities, not as monotonicity claims.

The goal is not trivialized by any hypothesis: it assumes none of the milestones, and stating "some nested-by-revenue assortment exists" (always true) or "every optimal assortment is nested by revenue" (false under ties) would be a different theorem.

Needed infrastructure is light: finite sums, real powers, and concavity of $x \mapsto x^{\gamma}$ for $\gamma \le 1$. The scalar lemmas are reusable for other nested logit results. Proofs of any milestone are welcome independently.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 250–273, 2014. https://doi.org/10.1287/opre.2014.1256 (cited from the authors' revised manuscript of June 18, 2013)
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
• D. McFadden, Modelling the choice of residential location, in A. Karlqvist et al. (eds.), Spatial Interaction Theory and Planning Models, North-Holland, 75–96, 1978.

Motivation

Many problems in machine learning and statistics are regularized empirical risk minimization: minimize an average $f(x)=\frac1n\sum_{i=1}^n f_i(x)$ of $n$ loss terms, one per data point, plus a regularizer $\psi(x)$ such as $\lambda\|x\|_1$. When $n$ is large, a full gradient $\nabla f$ costs $n$ component gradients, so stochastic gradient methods that touch one $f_i$ per step are preferred. Variance-reduced methods (SVRG, SAGA) correct the stochastic gradient with a periodically recomputed full gradient and reach the rates of full-gradient descent at the cost of stochastic steps; accelerated full-gradient methods (Nesterov) improve the rate from $O(1/T)$ to $O(1/T^2)$ on convex problems.

Combining the two directly was open until Allen-Zhu's Katyusha (arXiv:1603.05953, STOC 2017, JMLR 2018). Before it, accelerated stochastic rates were obtained either for special structure (accelerated coordinate and dual methods, which need strong convexity or dual access) or through reductions such as Catalyst and APPA, which wrap a non-accelerated method in an outer proximal-point loop and lose logarithmic factors. Katyusha adds a third momentum term, the Katyusha momentum, that pulls each iterate back to the snapshot point, and obtains the accelerated rate directly. This mission concerns the paper's second main result: the variant Katyusha$^{\mathrm{ns}}$ (Algorithm 2) for objectives that are convex but not strongly convex.

Setting

Problem (1.1) of the paper is

$$\min_{x\in\mathbb R^d} F(x)=f(x)+\psi(x)=\frac1n\sum_{i=1}^n f_i(x)+\psi(x),$$

where $n\ge1$, each component $f_i:\mathbb R^d\to\mathbb R$ is convex and $L$-smooth, $\|\nabla f_i(x)-\nabla f_i(y)\|\le L\|x-y\|$, and the regularizer $\psi$ is convex. A point $x^*$ minimizes $F$.

Katyusha$^{\mathrm{ns}}(x_0,S,L)$ runs $S$ epochs of $m$ iterations each (the paper takes $m=2n$). It keeps three sequences $y_k$, $z_k$ and a snapshot $\widetilde x^s$, all starting at $x_0$, and fixes $\tau_2=\frac12$. Epoch $s$ uses the weight $\tau_{1,s}=\frac{2}{s+4}$ and the step $\alpha_s=\frac{1}{3\tau_{1,s}L}$, computes $\nabla f(\widetilde x^s)$ once, and performs, for $k=sm,\dots,sm+m-1$:

1. the coupling $x_{k+1}=\tau_{1,s}z_k+\tau_2\widetilde x^s+(1-\tau_{1,s}-\tau_2)y_k$;
2. the SVRG estimator $\widetilde\nabla_{k+1}=\nabla f(\widetilde x^s)+\nabla f_i(x_{k+1})-\nabla f_i(\widetilde x^s)$, with $i$ uniform in $\{1,\dots,n\}$, independent across iterations;
3. the mirror step $z_{k+1}=\arg\min_z\{\frac1{2\alpha_s}\|z-z_k\|^2+\langle\widetilde\nabla_{k+1},z\rangle+\psi(z)\}$;
4. the gradient step (Option I) $y_{k+1}=\arg\min_y\{\frac{3L}2\|y-x_{k+1}\|^2+\langle\widetilde\nabla_{k+1},y\rangle+\psi(y)\}$.

At the end of the epoch the new snapshot is the average $\widetilde x^{s+1}=\frac1m\sum_{j=1}^m y_{sm+j}$. The output is $\widetilde x^S$. Throughout, $D_k=F(y_k)-F(x^*)$ and $\widetilde D^s=F(\widetilde x^s)-F(x^*)$.

Formalization targets

Goal: Theorem 4.1 with the constants of its proof

$$\mathbb E\big[F(\widetilde x^S)\big]-F(x^*)\le\frac{16\,\big(F(x_0)-F(x^*)\big)}{(S+3)^2}+\frac{12\,L\,\|x_0-x^*\|^2}{m\,(S+3)^2}\qquad(S\ge0,\ m\ge1).$$

The paper states $O\big(\frac{F(x_0)-F(x^*)}{S^2}+\frac{L\|x_0-x^*\|^2}{mS^2}\big)$; the explicit form above is what its proof in Appendix C.1 establishes.

Milestones, in the order of the proof

1. Lemma 2.7 for $\sigma=0$: the one-iteration inequality coupling $D_k$, $\mathbb E[D_{k+1}]$, $\widetilde D$ and the distances $\|z_k-x^*\|^2$, $\mathbb E\|z_{k+1}-x^*\|^2$.
2. (C.1): Lemma 2.7 summed over one epoch.
3. (C.2): the epoch inequality for $s\ge1$, after inserting the average snapshot and $\alpha_s=1/(3\tau_{1,s}L)$.
4. (C.3): the same for the base epoch $s=0$.
5. The parameter inequalities $\frac1{\tau_{1,s}^2}\ge\frac{1-\tau_{1,s+1}}{\tau_{1,s+1}^2}$ and $\frac{\tau_{1,s}+\tau_2}{\tau_{1,s}^2}\ge\frac{\tau_2}{\tau_{1,s+1}^2}$.
6. (C.4): the bound telescoped over $S$ epochs.

Significance

Theorem 4.1 gives the accelerated $O(1/S^2)$ rate for non-strongly convex composite finite sums with a direct method: $\varepsilon$ error after $O\big(\frac{n\sqrt{F(x_0)-F(x^*)}}{\sqrt\varepsilon}+\frac{\sqrt{nL}\,\|x_0-x^*\|}{\sqrt\varepsilon}\big)$ stochastic gradient evaluations, a factor $S$ better than the $O(1/S)$ of non-accelerated variance-reduced methods such as SAGA (Remark 4.2). The non-strongly convex case covers $\ell_1$-regularized and unregularized convex losses, where no strong-convexity parameter is available to tune a linear-rate method.

The result is proved in the paper; no machine-checked proof of Katyusha or Katyusha$^{\mathrm{ns}}$ is known to exist. The mission produces a formal statement of the algorithm and its rate with explicit constants, and a formal chain of the paper's intermediate inequalities. A SAGA mission on this platform states SAGA's non-accelerated $O(1/k)$ rate for the same problem class, so the two results become directly comparable in Lean.

Difficulty

Each step uses only convexity, smoothness and the optimality of proximal points, but the steps interlock. The variance of $\widetilde\nabla_{k+1}$ cannot be bounded by $F(\widetilde x)-F(x^*)$ as in SVRG's analysis without losing acceleration; the paper's bound (Lemma 2.4) leaves a linear term $\langle\nabla f(x_{k+1}),\widetilde x-x_{k+1}\rangle$ that is cancelled only by the specific weight $\tau_2=\frac12$ of the Katyusha momentum (Lemmas 2.6–2.7). Without strong convexity the per-epoch inequalities do not contract, so the proof must telescope across epochs with epoch-dependent weights $\tau_{1,s}$: the coefficients of $D_{sm+j}$ produced by epoch $s$ must dominate those consumed by epoch $s+1$, and the snapshot term $m\widetilde D^s$ must be charged to the previous epoch's iterates. Getting the boundary epoch $s=0$ (whose snapshot is $x_0$) and the last epoch right is where the constants come from.

Formalization scope

The Lean development works on EuclideanSpace ℝ (Fin d) with components indexed by Fin n ($n\ge1$). Gradients are given functions $\nabla f_i$ tied to $f_i$ by HasGradientAt; $L$-smoothness is the Lipschitz bound on them with $L>0$; convexity is ConvexOn ℝ Set.univ. $f$ and $\nabla f$ are the published SAGA.Convex.fAvg and SAGA.Convex.gradAvg. The regularizer $\psi$ is real-valued and convex, so extended-valued regularizers such as indicator functions of constraint sets are not covered. The two arg-min steps are evaluated through a map $P$ assumed to return a proximal point of $\psi$ (the published SAGA.Convex.IsProxPoint) for every positive step; for real-valued convex $\psi$ such points exist and are unique, so the hypothesis is satisfiable. $x^*$ is assumed to minimize $F$ (without strong convexity a minimizer need not exist). Randomness is modelled by finite sequences of indices: the expectation is the uniform average over all index sequences (SAGA.Convex.expectIdx), with the $Sm$ indices split into epochs by Mathlib's finProdFinEquiv.

Conventions committed to:

• Explicit constants for O(·). The goal's $O(\cdot)$ is instantiated as $16\,(F(x_0)-F(x^*))/(S+3)^2+12L\|x_0-x^*\|^2/(m(S+3)^2)$: the proof bounds $\widetilde D^S$ by $\frac{2\tau_{1,S-1}^2}{m}$ times the right-hand side of (C.4), which equals $2m\,(F(x_0)-F(x^*))+\frac{3L}2\|x_0-x^*\|^2$, with $\tau_{1,S-1}=\frac2{S+3}$. The bound holds trivially at $S=0$, so the goal is stated for all $S$.
• Epoch length. $m\ge1$ is a parameter (the algorithm sets $m=2n$); every statement holds for every $m\ge1$.
• Option I only; the unused input $\sigma$ and Option II are not modelled.
• Lemma 2.7 is stated for $\sigma=0$ with the paper's implicit side conditions $\alpha>0$, $0<\tau_1\le\frac12$.
• (C.2) is stated for an epoch $s\ge1$ whose snapshot is the average of given previous iterates; (C.1) and (C.3) are stated from an arbitrary epoch start state, which is the paper's "the randomness in the first $s-1$ epochs is fixed".
• The typo $\|z_{Sm}-z^*\|^2$ in (C.4) is read as $\|z_{Sm}-x^*\|^2$.

A trivializing formalization is ruled out: the prox map, the gradients and $x^*$ are all tied to $\psi$, $f_i$ and $F$ by hypotheses that a quadratic instance satisfies, and the expectation averages over every index sequence rather than a chosen one. The iteration count stated "in other words" after Theorem 4.1 is not a target.

Contributions welcome: proofs of the milestones in any order; general lemmas about proximal points of convex functions (the three-point inequality behind Lemma 2.5) and the co-coercivity of convex $L$-smooth functions (behind Lemma 2.4) are reusable beyond this mission.

Selected references

• Z. Allen-Zhu, Katyusha: The First Direct Acceleration of Stochastic Gradient Methods, STOC 2017; JMLR 18(221), 2018. arXiv:1603.05953v6. https://arxiv.org/abs/1603.05953
• A. Defazio, F. Bach, S. Lacoste-Julien, SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives, NeurIPS 2014. https://arxiv.org/abs/1407.0202
• R. Johnson, T. Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, NeurIPS 2013. https://papers.nips.cc/paper/4937
• Y. Nesterov, Introductory Lectures on Convex Programming, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9