All missions

Motivation

Many problems in machine learning and statistics have the composite form $\min_x F(x)=f(x)+g(x)$, where $f$ is a smooth loss and $g$ is a non-smooth regularizer such as $\lambda\|x\|_1$. When $g$ is separable, $g(x)=\sum_i g_i(x_i)$, the method of choice at scale is often randomized proximal coordinate descent: at each step one coordinate is drawn at random and a one-dimensional proximal problem is solved in that coordinate only. Each step is cheap, and the method underlies standard solvers for $\ell_1$-regularized regression and for the dual of support vector machines.

Classical linear-convergence guarantees for this method assume strong convexity of $f$ or of $F$ (Richtárik and Takáč, 2014), or rely on the Kurdyka–Łojasiewicz property with constants that are hard to make explicit. Karimi, Nutini and Schmidt (arXiv:1608.04636, ECML PKDD 2016) introduced the proximal-PL inequality, a generalization of the Polyak–Łojasiewicz condition to composite problems, and showed that it alone yields linear rates for proximal-gradient methods. Theorem 6 of that paper, the subject of this mission, extends the analysis to randomized proximal coordinate descent.

Timeline. Polyak (1963) and Łojasiewicz (1963) introduced the gradient-domination inequality for smooth problems. Nesterov (2012) analysed randomized coordinate descent for smooth convex problems; Richtárik and Takáč (2014) extended it to composite separable problems under strong convexity. Karimi, Nutini and Schmidt (2016) obtained the rate $(1-\mu/(dL))^k$ for the proximal coordinate method under proximal-PL alone (Theorem 6, p. 10, proof in Appendix H, p. 23).

Setting

Write $\mathbb R^d$ for the Euclidean space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$; $x_i$ is the $i$-th coordinate of $x$, $e_i$ the $i$-th basis vector, and $\nabla_i f(x)$ the $i$-th coordinate of the gradient. The data are:

• a differentiable $f:\mathbb R^d\to\mathbb R$ whose gradient is $L$-Lipschitz, $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$, with $L>0$;
• convex univariate functions $g_1,\dots,g_d:\mathbb R\to\mathbb R$ and the separable $g(x)=\sum_i g_i(x_i)$;
• $F=f+g$, which has a minimizer $x^*$; write $F^*=F(x^*)$.

For $\alpha>0$ the quantity

$$\mathcal D_g(x,\alpha)=-2\alpha\min_y\Big[\langle\nabla f(x),y-x\rangle+\frac\alpha2\|y-x\|^2+g(y)-g(x)\Big]$$

measures the best decrease of a quadratic upper model of $F$ at $x$. $F$ satisfies the proximal-PL inequality with constant $\mu>0$ if

$$\tfrac12\,\mathcal D_g(x,L)\ \ge\ \mu\,\big(F(x)-F^*\big)\qquad\text{for all }x.$$

The coordinate-wise proximal-gradient method starts at $x_0$. At step $k$ it draws $i_k$ uniformly from $\{1,\dots,d\}$, independently of the past, and sets $x_{k+1}=x_k+\alpha^\star e_{i_k}$, where $\alpha^\star$ minimizes

$$\alpha\,\nabla_{i_k}f(x_k)+\frac L2\alpha^2+g_{i_k}(x_{k,i_k}+\alpha)-g_{i_k}(x_{k,i_k}).\tag{16}$$

Formalization targets

Goal: Theorem 6 (p. 10)

For every $k\ge0$,

$$\mathbb E\big[F(x_k)-F^*\big]\ \le\ \Big(1-\frac{\mu}{dL}\Big)^k\big[F(x_0)-F^*\big].\tag{17}$$

The constant $\mu/(dL)$ is the paper's; no further constant is fixed.

Milestones (Appendix H, p. 23)

1. (62), the coordinate upper model: $F(x+te_i)-F(x)\le t\nabla_i f(x)+\frac L2t^2+g_i(x_i+t)-g_i(x_i)$.
2. The expected-improvement identity: $\frac1d\sum_i\min_{t}\big[t\nabla_i f(x)+\frac L2t^2+g_i(x_i+t)-g_i(x_i)\big]=-\frac1{2Ld}\mathcal D_g(x,L)$.
3. (63), the expected descent: $\mathbb E[F(x_{k+1})\mid x_k=x]\le F(x)-\frac1{2Ld}\mathcal D_g(x,L)$.

A companion statement (not a milestone, not in the paper) asserts that the one-dimensional step (16) exists for convex $g_i$ and $L>0$.

Significance

The result. Theorem 6 gives a linear rate for proximal coordinate descent on every composite problem satisfying proximal-PL, a class that contains $\ell_1$-regularized least squares and other problems that are not strongly convex. The rate matches that of plain randomized coordinate descent under PL (Theorem 3 of the paper) with the composite term added, and the factor $d$ is the usual price of updating one coordinate per step.

Formalizing it. The result is proved on paper; no machine-checked proof is known. A formal proof requires the coordinate descent lemma, the exchange of a separable minimum with a sum, and an exact accounting of the expectation over random index sequences. The definitions of $\mathcal D_g$, proximal-PL and the random-coordinate run built here are reusable for other proximal and coordinate methods.

Difficulty

The one-step argument is short once the expected-improvement identity is available; the difficulty is in that identity. Its left side averages over coordinates the minima of one-dimensional models, while $\mathcal D_g$ is a minimum over the whole space. Equating them requires that the full-space minimum split across coordinates, which is where separability of $g$ is used, and that each minimum be attained, which requires convexity of the $g_i$ and $L>0$. A second point is the expectation: the iterate after $k$ steps is a function of the whole index word $(i_0,\dots,i_{k-1})$, and the one-step expected descent must be propagated through the tower of conditional expectations to the $k$-step bound.

Formalization scope

• The space is EuclideanSpace ℝ (Fin d) with $d\ge1$ (0 < d); the gradient is Mathlib's gradient f, and $\nabla_i f(x)$ is gradient f x i.
• The Lipschitz gradient is the literal hypothesis $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ with $L>0$ and Differentiable ℝ f, as in the setup of Theorem 5. Appendix H uses only coordinate-wise Lipschitz continuity, which follows.
• $X^*\neq\emptyset$ is a point $x^*$ minimizing $F$; $F^*$ is $F(x^*)$, never a free real.
• The $g_i$ are real-valued convex functions. Extended-valued $g_i$ (box indicators, used for the SVM dual in §4.4) are outside this formalization.
• The minimum in $\mathcal D_g$ is a real infimum; it is attained, hence equal to the paper's minimum, for convex $g_i$ and $L>0$, and every statement using it carries these hypotheses.
• The update is any step selection $\mathrm{sel}(x,i)=x+t^\star e_i$ with $t^\star$ a minimizer of (16); the selection is a hypothesis-constrained parameter, never an arbitrary map. Equation (16) as printed assigns the minimizing step to $x_{k+1}$; the iterate $x_k+\alpha^\star e_{i_k}$ of Appendix H is what is encoded.
• $\mathbb E[F(x_k)-F^*]$ is the exact average over all $d^k$ index words, each of probability $d^{-k}$, which is the law of i.i.d. uniform coordinates.
• A formalization that leaves the update unconstrained, takes $F^*$ as a free constant, or computes $\mathcal D_g$ as a junk infimum would make the goal false or vacuous; these are ruled out by the conventions above.

Contributions welcome: proofs of the three milestones and the goal, the existence of the coordinate step, and a version with extended-valued $g_i$.

Selected references

• H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition, ECML PKDD 2016; arXiv:1608.04636v4, 2020. https://arxiv.org/abs/1608.04636
• P. Richtárik, M. Takáč, Iteration complexity of randomized block-coordinate descent methods for minimizing a composite function, Mathematical Programming 144, 2014. https://doi.org/10.1007/s10107-012-0614-z
• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM J. Optim. 22(2), 2012. https://doi.org/10.1137/100802001
• B. T. Polyak, Gradient methods for minimizing functionals, USSR Comput. Math. Math. Phys. 3(4), 1963. https://doi.org/10.1016/0041-5553(63)90382-3

Why lower bounds matter

Online learning studies decisions made before their costs are known. An algorithm selects a point, observes a loss, and repeats. Regret compares its accumulated loss with the loss of one fixed point chosen after the sequence is known. Upper bounds show what a particular algorithm can guarantee; a lower bound shows what every algorithm must sometimes suffer. The distinction matters when deciding whether a rate such as $\sqrt T$ can be improved by changing the update rule. Chapter 5 of Orabona's Online Learning: A Modern Introduction Using Convex Optimization addresses this question for online linear optimization.

The chapter begins with bounded decision sets and then examines unbounded decision spaces. On bounded sets, the main result gives a quantitative obstruction with an explicit constant for every deterministic algorithm. The book compares that order with the regret upper bound for online subgradient descent: the square-root dependence on the number of rounds is optimal up to a constant factor under the same loss-scale and diameter parameters (Orabona, Theorem 5.1 and discussion, pp. 50–51). The same chapter shows a different phenomenon for unprojected subgradient descent with steps that decay too slowly: its regret can have order $T^{2-\alpha}$ for $0<\alpha<1$ (Orabona, Theorem 5.4, p. 52).

The online linear optimization setting

Let $V$ be a nonempty subset of Euclidean space $\mathbb R^d$. On round $t$, a deterministic online algorithm selects $x_t\in V$ using only the loss vectors from rounds $1,\ldots,t-1$. It then observes $g_t\in\mathbb R^d$ and pays the linear loss $\langle g_t,x_t\rangle$. The adversary may select any loss vectors satisfying $\|g_t\|_2\le L$. This is the online linear optimization protocol used in the chapter; it also supplies lower bounds for online convex optimization because linear functions are convex (Orabona, §5.1, p. 50).

For a fixed competitor $u\in V$, define

$$\operatorname{Regret}_T(u) =\sum_{t=1}^{T}\langle g_t,x_t\rangle -\sum_{t=1}^{T}\langle g_t,u\rangle.$$

The competitor is fixed across all $T$ rounds, although it may be selected after the loss sequence. The algorithm must make its own choices causally. These two quantifier positions are part of the mathematical claim. In particular, the hard sequence and competitor can depend on the algorithm, while the algorithm cannot use a future loss vector to choose its current prediction.

The bounded setting also uses the diameter $D=\max_{v,w\in V}\|v-w\|_2$. The theorem assumes $V$ is closed, bounded, and convex, and that $D>0$. In finite-dimensional Euclidean space, closedness and boundedness make $V$ compact, so this maximum exists. The positive diameter excludes a singleton feasible set, where the algorithm and the only comparator coincide. These hypotheses and the diameter convention are stated in Theorem 5.1, pp. 50–51.

Formalization targets

Worst-case regret on every bounded convex set

The goal is the chapter's Theorem 5.1. For every deterministic algorithm on such a set $V$, every positive integer $T$, and every nonnegative loss scale $L$, there are bounded loss vectors and a competitor $u\in V$ for which

$$\operatorname{Regret}_T(u)\ge \frac{\sqrt2}{4}LD\sqrt T.$$

The book prints the exact factor $\sqrt2/4$. The scale $L$ appears in its conclusion and in the restriction $\|g_t\|_2\le L$ but is not introduced before that sentence, so the formal statement quantifies it explicitly. At $L=0$, the bound reads zero; for $L>0$ it gives a positive lower bound when $D>0$ and $T\ge1$ (Orabona, Theorem 5.1, pp. 50–51).

Supporting targets

Three milestones support and contextualize the goal. The first is the real-coefficient, $p=1$ lower-bound case of Khintchine's inequality, which controls the mean absolute value of a weighted sum of independent random signs (Orabona, Theorem A.14, p. 296). The second is the finite first-moment principle: a random sequence whose expected loss is at least $K$ has an outcome with loss at least $K$ (Orabona, §5.1, p. 50). The third records the lower-bound example for unprojected online subgradient descent with step size $t^{-\alpha}$:

$$\operatorname{Regret}_T(0)\ge\frac12\phi(\alpha)T^{2-\alpha}, \qquad \phi(\alpha)=\frac1{2-\alpha}+\frac{(1/2)^{1-\alpha}-1}{1-\alpha}.$$

This last target uses the book's threshold $T\ge2/((1-\alpha)\phi(\alpha))$ and $0<\alpha<1$ (Orabona, Theorem 5.4, p. 52).

What the results establish

The goal rules out an $o(\sqrt T)$ worst-case regret guarantee for deterministic online linear optimization under a fixed positive loss scale and positive diameter. Because the result applies to every nonempty bounded closed convex $V$ with $D>0$, it does not rely on a symmetric feasible set or a chosen cube. The explicit constant permits direct comparison with concrete algorithmic guarantees. Theorem 5.4 separately identifies a failure mode for unprojected online subgradient descent on an unbounded domain. Both conclusions are proved in the book; the remaining task here is to give their statements and supporting objects machine-checkable Lean meanings, then prove them in Lean. Hazan's related lower bound uses a hypercube instance and an unspecified absolute constant, so it is related context rather than the same formal target.

The mathematical difficulty

A hard sequence must be chosen after the algorithm is fixed and must respect the algorithm's information at every round. A sequence selected independently of that quantifier order need not be hard: an algorithm tailored to a known sequence can choose its best fixed point on every round. The bound must also hold on any convex body with positive diameter, including sets whose geometry is asymmetric. The proof therefore needs a way to extract a uniform numerical lower bound from only the diameter and the loss norm bound, while retaining the algorithm's causal dependence on earlier losses (Orabona, §5.1, pp. 50–51).

Formalization scope

Lean represents $\mathbb R^d$ by EuclideanSpace ℝ (Fin d), with vectors $g_t$ and decisions $x_t$ indexed from round one; index zero is unused. A deterministic algorithm is a function of a full loss sequence together with an explicit non-anticipation condition. Its outputs are required to lie in $V$. Regret is a finite sum against one fixed competitor. The positive horizon, positive diameter, closedness, boundedness, convexity, and nonemptiness are explicit. This rules out trivializing the goal by using a singleton domain, an anticipatory algorithm, or a fixed hard sequence that precedes the algorithm's quantifier.

The Khintchine milestone uses the uniform distribution on a finite Boolean cube; each Boolean coordinate represents an independent Rademacher sign. Its expectation is an ordinary finite average and is always defined. The finite first-moment milestone uses arbitrary nonnegative weights summing to one. Theorem 5.4 uses linear losses of norm at most one in arbitrary positive Euclidean dimension, which are convex and $1$-Lipschitz. Its auxiliary function $\phi$ is used only for $0<\alpha<1$, where the printed formula's denominators are nonzero. The separate limiting claim about $\phi$ and the later coin-betting lower bounds are outside this mission's current milestones. Contributions establishing the Rademacher inequality, the geometric lower bound, the causal regret argument, and the unprojected descent example all fit this scope.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026. arXiv.
• Elad Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization, 2016; arXiv:1909.05207. arXiv.

Motivation

In online convex optimization, a learner chooses a point before seeing the loss assigned to that round. Its performance is measured against a fixed point that could have been chosen after the full sequence became known. A learner that merely minimizes accumulated past losses can react sharply when successive losses favor different points. Follow-the-Regularized-Leader (FTRL) changes that decision by adding a regularizer to the past losses. Chapter 7 of Orabona's Online Learning: A Modern Introduction Using Convex Optimization develops the resulting regret guarantees for a general norm, time-varying regularizers, and convex losses. This mission targets its first explicit square-root regret bound, Corollary 7.6, together with the equality and stability statements used to analyze the algorithm.

The general-norm formulation matters because different feasible sets make different norms natural. A Euclidean constraint set and a simplex, for example, need not give useful bounds under the same geometry. The chapter states the central inequality using the norm of the learner's decisions and the corresponding dual norm of loss subgradients. Its regularizer may vary with time, which lets the same result describe a learning-rate schedule chosen before each loss is observed.

Setting

Let $V$ be a nonempty, closed, convex subset of a finite-dimensional real normed space $E$. In round $t=1,\ldots,T$, the learner outputs $x_t\in V$, then receives a loss function $\ell_t$ and incurs $\ell_t(x_t)$. For a fixed comparator $u\in V$, regret is $\sum_{t=1}^T(\ell_t(x_t)-\ell_t(u))$. The comparison point stays the same across all rounds; it is not a round-by-round optimum.

FTRL supplies a sequence of regularizers $\psi_t$. At the start of round $t$, it selects any minimizer of the regularized cumulative loss

$$F_t(z)=\psi_t(z)+\sum_{i=1}^{t-1}\ell_i(z),\qquad x_t\in\operatorname*{argmin}_{z\in V}F_t(z).$$

The sum contains only past losses. Its empty value at $t=1$ means $x_1$ minimizes $\psi_1$. The analysis also names $x_{T+1}$ and $\psi_{T+1}$; that extra iterate occurs after the last charged round. A loss subgradient $g_t$ at $x_t$ is a continuous linear functional with $\ell_t(y)\ge\ell_t(x_t)+g_t(y-x_t)$ for every $y\in E$. Its operator norm is the dual norm $\|g_t\|_*$. The norm in the strong-convexity and stability statements is the norm on $E$.

Formalization targets

The goal is Corollary 7.6 on printed page 102. Let $\psi$ be closed and $\mu$-strongly convex on $V$, with $\mu>0$, and let $m=\min_{z\in V}\psi(z)$. The round-$t$ regularizer is $\psi_t(z)=(\psi(z)-m)/\eta_{t-1}$, with $\psi_{T+1}=\psi_T$. If the losses are subdifferentiable on $V$, the first target is the bound, for every $u\in V$ and every choice of subgradients $g_t\in\partial\ell_t(x_t)$,

$$\sum_{t=1}^T\bigl(\ell_t(x_t)-\ell_t(u)\bigr) \le \frac{\psi(u)-m}{\eta_{T-1}} +\sum_{t=1}^T\frac{\eta_{t-1}}{2\mu}\|g_t\|_*^2 +\sum_{t=1}^{T-1}\left(\frac1{\eta_{t-1}}-\frac1{\eta_t}\right) \bigl(\psi(x_{t+1})-m\bigr).$$

The last sum records the change in the regularizer; it is part of the stated result. The second target uses losses that are $L$-Lipschitz on an open neighborhood of $V$ and the specified schedule $\eta_{t-1}=\alpha\sqrt\mu/(L\sqrt t)$, for $\alpha,L>0$:

$$\sum_{t=1}^T\ell_t(x_t)-\sum_{t=1}^T\ell_t(u) \le\left(\frac{\psi(u)-m}{\alpha}+\alpha\right) \frac{L\sqrt T}{\sqrt\mu}.$$

The goal records both conclusions. Its milestones are the exact regret identity of Lemma 7.1, the stability inequality and minimizer assertion of Lemma 7.5, the proximal-regularizer variant of Lemma 7.7, and the linear-perturbation stability result of Lemma 7.49. The last result extends the chapter's stability theme beyond the immediate proof of Corollary 7.6.

Significance

The second inequality gives an explicit $\sqrt T$ bound with a comparator-dependent regularization term, without imposing a finite diameter on $V$. The first inequality retains the complete dependence on the chosen step sizes and on changes in the regularizer. A reader can therefore see what a schedule must control before specializing to the square-root choice. These are results already proved in the cited textbook; the open work in this mission is their Lean formalization, along with proofs of the stated milestones.

Formalizing the chapter would provide reusable statements about minimizers of strongly convex functions, subgradients in a dual normed space, and the stability of regularized minimization. The identities and stability bounds also connect FTRL's update rule to regret estimates without tying the interface to a single Euclidean norm or a single learning-rate choice. The definitions are intended to be usable by later chapters that employ linearized or optimistic FTRL, although those later results are outside this mission's goal.

Difficulty

The algebraic regret identity is exact, but it still contains the losses on both sides of the comparison. It does not by itself provide an explicit upper bound. The challenge is to control the change between successive minimizers while the objective and regularizer both change, then retain the correct index shift in the regularizer terms. In the general-norm setting, a subgradient is a dual vector; treating it as a primal vector would change the inequality's meaning. The corollary also has two quantifier patterns: its first bound covers every admissible subgradient sequence, while its second uses a particular learning-rate schedule and a Lipschitz condition.

Formalization scope

The Lean development uses a finite-dimensional real normed space. Losses and regularizers are real-valued functions on that space, and minimization is restricted to $V$. This is the chapter's finite-valued regime of its broader extended-real notation. A closed function on $V$ is represented by the closed epigraph of its restriction. Strong convexity is Mathlib's StrongConvexOn; a subgradient is a continuous linear functional and its operator norm is the book's dual norm. Subdifferentiability is required at every feasible point. The Lipschitz condition is stated on an open set containing $V$, as on the page.

Indices start at $1$ for rounds and at $0$ for step sizes. The theorem requires $T\ge1$, positive step sizes, and positive values for every quantity used as a denominator. The minimum $m$ is supplied by a point attaining it, and an FTRL run is a sequence of actual minimizers through round $T+1$. This rules out a sequence of arbitrary feasible decisions or a regularizer schedule unrelated to $\eta$. The first inequality retains the regularizer-change sum even when step sizes are not monotone. The book's one-line proof remarks that this change is nonpositive under an unstated monotonicity condition; the printed statement itself does not impose that condition.

The definition layer and all four milestone statements are in scope. Contributions proving any of them, or developing general lemmas about closed strongly convex objectives and dual-space subgradients that they need, fit this mission. The only simplification is replacing extended-real losses by real-valued losses on the feasible region, so no infinite value or undefined extended-real subtraction enters a displayed bound.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 7, pp. 99–140. arXiv

Motivation

An online learning algorithm chooses a decision before seeing each round's data and is judged by regret: how much more loss it incurs than a fixed decision chosen in hindsight. Statistical learning asks a different question. After seeing data drawn from a distribution, how small is the decision's expected loss on another draw? Chapter 3 of Orabona's textbook connects these settings. It shows that a deterministic online rule with a pathwise regret guarantee also controls expected loss when its input data are independent samples. The chapter's high-probability result is the target here.

The distinction matters when an online guarantee is already available. A regret theorem holds for every loss sequence, including adversarial sequences, yet it does not by itself state what a learner achieves on future data from a distribution. The conversion supplies that statistical reading. It applies to the sequence of predictions produced along one sample path, with no need to select an empirical-risk minimizer from the full decision set. Chapter 3 also studies finite-set validation, in which a separate sample selects one candidate from a fixed collection Orabona, Chapter 3.

Setting

The decision set $V$ is a subset of Euclidean space $\mathbb R^d$. A data point $z$ belongs to a measurable space $D$ and is drawn according to a probability distribution $\rho$. The loss $f(x,z)$ lies in $[0,1]$ for every $x\in V$ and $z\in D$, and is measurable as a function of $z$ when $x$ is fixed. Its true risk is $F(x)=\mathbb E_{z\sim\rho}[f(x,z)]$. For a sample $\xi_1,\ldots,\xi_T$ drawn independently from $\rho$, round $t$ presents the loss function $\ell_t(x)=f(x,\xi_t)$.

A deterministic online algorithm produces predictions $x_1,\ldots,x_{T+1}$ in $V$. Its prediction $x_t$ uses only $\xi_1,\ldots,\xi_{t-1}$. For a fixed competitor $u\in V$, its regret is $\operatorname{Regret}_T(u)=\sum_{t=1}^T\ell_t(x_t)-\sum_{t=1}^T\ell_t(u)$. A proposed regret bound $R(u,T)$ is required to hold on every sample path and for every competitor $u$. The risk comparison uses a minimizer of the full expression $F(u)+R(u,T)/T$, whose existence the theorem assumes.

Formalization targets

The goal is Theorem 3.10, with $T\ge1$ and $0<\delta<1$:

$$\mathbb P\!\left\{\frac1T\sum_{t=1}^T F(x_t) \le \min_{u\in V}\left(F(u)+\frac{R(u,T)}{T}\right) +2\sqrt{\frac{2\ln(2/\delta)}{T}}\right\}\ge1-\delta.$$

The minimum includes both risk and normalized regret. The theorem controls the average risk of the produced predictions; it does not require $F$ to be convex or claim the risk of their average decision. This makes the result applicable to decision sets and losses beyond the convex setting of the chapter's expectation result.

The first milestone is the two-sided bounded-martingale inequality of Theorem 3.9. A second milestone is the displayed concentration estimate in the proof of Theorem 3.10, which compares average true risk with average observed loss for the adaptive predictions. The final milestone is Theorem 3.17: if a fixed nonempty finite set $S\subseteq V$ is evaluated on fresh data and $\widehat x$ minimizes its empirical risk, then

$$F(\widehat x)\le\min_{x\in S}F(x) +2\sqrt{\frac{2\ln(2|S|/\delta)}{T}}$$

with probability at least $1-\delta$ Orabona, pp. 27–32.

Significance

The goal gives a direct way to read an online regret certificate as a distributional risk certificate. The bound retains the competitor-dependent function $R(u,T)$ inside the minimization: a decision with slightly larger risk but substantially smaller regret bound may give the better guarantee. Its deviation term has the exact constant and confidence dependence stated in the textbook. The finite-set theorem supplies a distinct validation guarantee for choosing one candidate from a fixed collection; it applies even when the risk is not convex.

Formalizing these results adds the probability layer absent from a deterministic regret statement: independent samples, a prediction rule constrained by past observations, true risk as an integral, and probability events for the adaptive sequence. Related online-to-batch statements already exist in the platform's developments of Hazan's online convex optimization text and Mohri, Rostamizadeh and Talwalkar's Foundations of Machine Learning. They use different algorithm and loss models and do not state this competitor-dependent bound. The present mission records the precise Chapter 3 formulation as an open formal proof target; the local Lean statements compile, but their proofs are not supplied.

Difficulty

The observed loss $f(x_t,\xi_t)$ uses a prediction chosen from earlier observations, while the event in the goal concerns its expected loss $F(x_t)$. Treating the predictions as fixed would ignore their dependence on the sample history. Allowing a prediction to inspect the current sample would break the comparison. The required concentration statement therefore has to retain the exact information available at each round. The comparator in the final bound is fixed before the samples are observed, while the online predictions remain sample dependent Orabona, proof of Theorem 3.10.

For the finite-set result, the selected predictor depends on the validation sample. A concentration estimate for a single fixed predictor does not immediately give the asserted guarantee for that selected predictor. The finite set must remain fixed before sampling, and the statement must account for every possible selected member.

Formalization scope

The Lean decision space is EuclideanSpace ℝ (Fin d). Samples are functions $\mathbb N\to D$ under the infinite product measure of $\rho$; their values at index zero are unused. The algorithm is a function of the full sample path constrained by a non-anticipation predicate: changing samples from round $t$ onward cannot change $x_t$. Regret is against a fixed $u$, with sums over rounds $1,\ldots,T$. The pathwise regret guarantee quantifies over every sample path, so it cannot be replaced by an expected-regret assumption.

The integral defining $F$ is used with the book's measurable $[0,1]$ losses on $V$, avoiding an undefined-integral convention. Measurability of each prediction, realized loss, and realized risk is stated explicitly where a probability event uses them. These regularity conditions make the probability statements meaningful and are the only extra conditions beyond the textbook's mathematical setup. A minimizer $u_\star\in V$ represents the assumed minimum in Theorem 3.10. The finite-set minimum is a real infimum whose input is nonempty, finite, and bounded. The positive horizon guards division by $T$; $0<\delta<1$ guards the logarithms. In Theorem 3.9, $B>0$ and $\varepsilon\ge0$ make its printed tail formula valid, including at the threshold boundary.

A complete development needs Mathlib's infinite product measure, filtration and martingale interfaces, conditional expectation or conditional moment bounds, and the sub-Gaussian concentration library. The risk, regret, non-anticipation, and empirical-risk definitions can be reused for later stochastic learning results. Contributions that establish the concentration milestone, connect it to the regret identity, or prove the finite-set validation statement all fit this scope.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026. arXiv
• Elad Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization, 2016; revised arXiv version, 2019. arXiv

Motivation

Coordinate descent changes one component of a parameter vector at a time. This matters when evaluating or updating a single component is cheaper than handling the full vector, for example in problems with sparse features. The coordinate chosen at each step can be random or selected from the current gradient. Karimi, Nutini, and Schmidt study these choices for objectives that satisfy a Polyak–Łojasiewicz (PL) inequality, a condition that controls objective error by the size of the gradient without assuming convexity. Their Theorem 3 gives an explicit expected rate for uniform random coordinates, while §3.2 gives a rate for the greedy Gauss–Southwell choice. Karimi, Nutini, and Schmidt (2016), §3

The question is how much of the familiar full-gradient linear rate survives when an update sees only one coordinate. The theorem answers this with a dimension factor: each uniform draw accesses one of $d$ coordinates, and the rate depends on $\mu/(dL)$. The same paper relates the greedy rule to earlier work on coordinate descent and boosting; this mission treats its stated greedy rate as a companion result, using the same coordinate update. Karimi, Nutini, and Schmidt (2016), §§3.1–3.2

Setting

Let $d\ge1$, and let $f:\mathbb R^d\to\mathbb R$ be differentiable. Write $\nabla_i f(x)$ for coordinate $i$ of its gradient and $e_i$ for the corresponding standard basis vector. The paper's coordinate-wise upper bound (5), with $L>0$, is

$$f(x+\alpha e_i)\le f(x)+\alpha\nabla_i f(x)+\frac L2\alpha^2 \quad\text{for every }x\in\mathbb R^d,\ i\in\{1,\ldots,d\},\ \alpha\in\mathbb R.$$

Here $i$ ranges over the $d$ coordinates. The bound concerns motion along one coordinate. It is the exact smoothness condition used in Theorem 3. Let $x^*$ be a global minimizer and put $f^*=f(x^*)$; thus the solution set is nonempty and $f^*$ is an attained optimal value. The PL inequality (3) with $\mu>0$ says

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

The randomized coordinate-descent step (6) draws $i_k$ uniformly from the $d$ coordinates, independently at each time, and sets $x_{k+1}=x_k-L^{-1}\nabla_{i_k}f(x_k)e_{i_k}$. The initial point $x_0$ is arbitrary. For $k$ draws, expectation means the average over all $d^k$ words $(i_0,\ldots,i_{k-1})$, each assigned weight $d^{-k}$. In particular, at $k=0$ the empty word has weight one and the iterate is $x_0$.

The Gauss–Southwell rule instead chooses a coordinate with the largest $|\nabla_i f(x_k)|$; ties may be resolved in any way. Its rate uses a PL inequality in the maximum-coordinate norm, $\|\nabla f(x)\|_\infty=\max_i|\nabla_i f(x)|$, with constant $\mu_1>0$. Karimi, Nutini, and Schmidt (2016), pp. 5–6

Formalization targets

Theorem 3: uniform random coordinates

For every $k\ge0$, the goal is the paper's expected suboptimality bound

$$\mathbb E[f(x_k)-f^*] \le\left(1-\frac{\mu}{dL}\right)^k\bigl(f(x_0)-f^*\bigr).$$

The target includes the specific update (6), the coordinate condition (5), and the PL inequality (3). The three milestones are the paper's displayed one-coordinate decrease, its uniform expected decrease involving $\|\nabla f(x)\|^2$, and the resulting conditional expected gap contraction. They are indexed to the proof of Theorem 3 on page 5. Karimi, Nutini, and Schmidt (2016), Theorem 3 and proof

Greedy coordinate choice

The companion target is the rate stated in §3.2 when the maximum-norm PL inequality holds:

$$f(x_k)-f^* \le\left(1-\frac{\mu_1}{L}\right)^k\bigl(f(x_0)-f^*\bigr).$$

This bound applies to any run that chooses a maximizing coordinate at every step. The different PL modulus is part of the statement; it need not equal the modulus $\mu$ in Theorem 3. Karimi, Nutini, and Schmidt (2016), §3.2

Significance

Theorem 3 gives a quantitative guarantee for a method that reads one gradient component per update. The guarantee depends on the attained optimum, the coordinate smoothness constant, the PL modulus, and the number of coordinates. It applies to objectives satisfying PL even when convexity is unavailable. The companion result records how the stated rate changes when the coordinate is selected by the largest gradient component and the PL condition is measured in the corresponding dual norm. Karimi, Nutini, and Schmidt (2016), §3

The paper proves these claims, but this mission asks for machine-checked proofs of their exact hypotheses and constants. A complete development will make the finite random experiment explicit and give reusable definitions for coordinate updates and expectations of finite coordinate-choice histories. The PL predicate is already published in the theorem library; the coordinate model and the results here remain to be formalized.

Difficulty

A bound for a single coordinate update depends on one component of the gradient. An arbitrary coordinate can have a zero component even when the full gradient is large, so a pointwise decrease with the full gradient norm cannot be asserted for every choice. The theorem instead concerns the expectation over a uniform choice and then over the complete history of choices. The main formal difficulty is keeping those two levels of expectation aligned with a state $x_k$ that itself depends on earlier draws. For the greedy companion, the selected coordinate may not be unique; the statement must cover every maximizing choice without assuming a fixed tie-breaking rule.

Formalization scope

The vector space is EuclideanSpace ℝ (Fin d). The shared definitions give (5), the step (6), the iterate produced by a word Fin k → Fin d, and the expected gap as a real finite sum. The published ShiOptRates.PolyakLojasiewicz predicate represents (3) after multiplying both sides by two. Every theorem using uniform draws assumes $d>0$; every step with $1/L$ assumes $L>0$. The goal also states differentiability, an explicit global minimizer, and $\mu>0$. No convexity is assumed. A free real number called $f^*$ would change the PL condition and could invalidate the rate, so the formal statement uses $f(x^*)$ throughout.

The index-word average is an exact finite representation of independent uniform sampling, including $k=0$. It does not sample coordinates without replacement. The companion theorem represents the maximum-norm PL condition by requiring its inequality at every maximizing coordinate, which is equivalent for $d>0$, and quantifies over every run satisfying the Gauss–Southwell update relation. Useful contributions include proofs of the three displayed milestones, the passage from one draw to the word average, and the greedy companion. The paper's optional remark on sampling proportional to coordinate-specific constants $L_i$ and its exact-coordinate-minimization remark are outside this proposal.

Selected references

• H. Karimi, J. Nutini, and M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD, 2016; arXiv:1608.04636v4.

Motivation

An assortment decision determines which products a seller makes available to a customer. When customers differ, the seller may first choose a limited collection of products and then decide which of those products to display to each arriving customer. This is a concrete way to represent personalized product pages or offers with a common inventory or display budget. The benefit of that second decision is not immediate from a single-customer model: personalization can remove products that dilute one type's purchases while retaining them for another type. El Housni and Topaloglu quantify this benefit for a mixture of multinomial logit choice models.

Their Theorem 3.1 compares optimal expected revenue with and without customer-type customization. It gives a universal factor depending only on the number of types and an explicit family showing that this order can occur. The result is already proved in the authors' SSRN version of December 7, 2021. This mission concerns the statements and proof in that version; the published Operations Research article appeared in 2023 and may use different numbering.

Setting

There are $n$ products $N=\{1,\ldots,n\}$ and $m$ customer types $M=\{1,\ldots,m\}$. Product $i$ earns revenue $r_i>0$ when purchased. Customer type $j$ arrives with probability $\theta_j\ge0$, with $\sum_{j\in M}\theta_j=1$. Its preference weight for product $i$ is $v_{ij}\ge0$; the no-purchase alternative has weight one. An assortment $S\subseteq N$ offered to type $j$ yields MNL expected revenue

$$\operatorname{Rev}_j(S)=\frac{\sum_{i\in S}r_i v_{ij}}{1+\sum_{i\in S}v_{ij}}.$$

The seller may initially carry at most $K$ products. In the customized assortment problem (CAP), it chooses $S$ and, after seeing the type, offers a subset $S_j\subseteq S$. For a fixed carried set, write $f_j(S)=\max_{T\subseteq S}\operatorname{Rev}_j(T)$ and $f^C(S)=\sum_{j\in C}\theta_j f_j(S)$ for any collection $C$ of types. Thus $f^M(S)$ is the expected personalized revenue. In the mixed multinomial logit problem (MMNL), the same carried assortment $S$ is offered to every type. Both models obey the same first-stage cardinality limit:

$$z_{\rm CAP}=\max_{S\subseteq N,\ |S|\le K}f^M(S),\qquad z_{\rm MMNL}=\max_{S\subseteq N,\ |S|\le K}\sum_{j\in M}\theta_j\operatorname{Rev}_j(S).$$

This formulation follows §2 and §3 of the December 2021 SSRN version, pp. 5–7. A zero preference weight is allowed: the authors' tightness instance assigns zero to products a type does not consider.

Formalization targets

Theorem 3.1: universal comparison

For every valid model and every first-stage budget $K$, the target is

$$z_{\rm MMNL}\le z_{\rm CAP}\le m\,z_{\rm MMNL}.$$

The factor counts customer types, not products. The result covers $K=0$ as well: both values are zero. It does not assume the products are sorted by revenue, since the numerical indexing convention in §2 is unnecessary for this comparison and is incompatible with the paper's tightness family.

Theorem 3.1: order-tight family

The same theorem says that there are instances for which the CAP value is $\Omega(m)$ times the MMNL value. The formal target uses the instance constructed in its proof, pp. 8–9 and records the explicit bound implied there:

$$z_{\rm MMNL}>0,\qquad z_{\rm CAP}\ge\frac{m}{6}\,z_{\rm MMNL}\qquad(m\ge2).$$

In this family $n=K=m$. With $\alpha=(\sum_{j=1}^m a^{-j})^{-1}$, the parameters are $\theta_j=\alpha/a^j$, $r_i=a^i$, and $v_{ij}=b^{m-i+1}$ when $i\le j$ and zero otherwise. The proof chooses $b=m-1$ and $a=2m(m-1)^m$. The goal also asserts that this family satisfies the model assumptions. The accompanying milestones are the paper's typewise comparison, the CAP lower bound, equation (3.1), its two term bounds, and the MMNL upper bound.

Significance

The universal inequality limits the improvement that type-specific displays can offer in this model using only the number of types. The family in the second part shows that no bound independent of $m$ can replace it across all valid instances. Thus the comparison locates the possible value of customization even when the seller may carry every product. It also distinguishes the effect of a shared display from the effect of the common product budget, since the example has $K=n$.

The paper already proves both claims. A complete formal development would check the exact MNL revenue formula, the two finite optimization problems, and the asymptotic example within one Lean environment. It would leave reusable definitions for personalized and common assortments under a mixture of choice models. The statements in this draft compile with proof placeholders; this mission does not claim that the theorem has a machine-checked proof yet. It welcomes proofs of the listed milestones, lemmas about finite maxima and nonnegative MNL revenue, and a proof of the combined goal.

Difficulty

For each type, personalization maximizes revenue over its own subset of $S$; MMNL must use one subset for all types. Exchanging the sum over types with a maximum over assortments would erase that distinction and is generally invalid. A simple comparison of the two optima gives the first inequality but cannot explain the precise factor $m$ or why it can be approached in order. The tightness family also balances rapidly changing revenues and arrival probabilities against preference weights. Its boundary case $m=2$ has $b=1$, so a claim needing $b>1$ would miss a valid member of the family.

Formalization scope

Lean represents products by Fin n, customer types by Fin m, and assortments by Finset (Fin n). The paper's one-based product $i$ is Lean's index i.val + 1: $a^i$ becomes a ^ (i.val + 1), and $b^{m-i+1}$ becomes b ^ (m - i.val). The preference function takes product first and type second, matching $v_{ij}$. The common revenue calculation imports the published ChoiceCDLP.MNL.mnlObjective with no-purchase weight one.

All maxima are Finset.sup' over nonempty finite families. The feasible family contains the empty assortment for every natural-number budget; the personal subassortment family contains the empty set as well. This makes the values genuine finite maxima, including at zero budget. No real sSup fallback value is used. The standing assumptions are positive revenues, nonnegative preference weights, nonnegative arrival probabilities, and a probability sum of one. The explicit instance is restricted to $m\ge2$, has positive MMNL value, and satisfies each standing assumption. These conditions exclude a vacuous $\Omega(m)$ ratio based on zero MMNL value or an instance outside the model.

The complete development needs elementary facts about finite sums, powers, ordered Finsets, finite maxima, and nonnegative rational functions. The MNL objective is already a separate published definition; the paper-specific CAP, MMNL, and instance definitions are local. The proof targets are the claims printed in the December 2021 SSRN version, with the constant $1/6$ disclosed as an explicit pin from its proof.

Selected references

• O. El Housni and H. Topaloglu, Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models: Value of Personalized Assortments, SSRN 3830082, version of December 7, 2021, §§2–3, pp. 5–9; published in Operations Research, 2023. SSRN

Motivation

Gradient descent on a smooth function $f:\mathbb R^d\to\mathbb R$ converges at a linear rate (the optimality gap shrinks by a constant factor each step) under strong convexity. Many problems in machine learning and statistics are not strongly convex: least squares with a rank-deficient design, logistic regression on separable or degenerate data, and some non-convex objectives. Over roughly 25 years several weaker conditions were proposed that still give linear convergence. Examples are the error bound of Luo and Tseng, restricted strong convexity, essential strong convexity, weak strong convexity, and quadratic growth (also called optimal or semi-strong convexity). Each came with its own proof, usually assuming convexity. How these conditions relate to one another was rarely made explicit.

Karimi, Nutini and Schmidt (arXiv:1608.04636, ECML PKDD 2016) put the Polyak–Łojasiewicz (PL) inequality (Polyak, 1963) at the centre. Their Theorem 2 orders seven conditions by strength for functions with a Lipschitz gradient, without convexity. It shows that PL is equivalent to the error bound and implies quadratic growth. For convex functions it shows that the four weakest conditions coincide. The equivalence of EB and PL is a special case of a result of Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234, Theorem 5). Zhang (arXiv:1606.00269) independently related RSI, EB, PL and QG.

Setting

Let $f:\mathbb R^d\to\mathbb R$ be differentiable with gradient $\nabla f$. The paper's standing assumptions (§2, p. 2) are:

1. $\nabla f$ is $L$-Lipschitz: $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$, with $L>0$;
2. the solution set $\mathcal X^*=\{x:\ f(x)\le f(y)\ \forall y\}$ is non-empty. Write $f^*$ for the optimal value.

For every $x$, $x_p$ denotes a projection of $x$ onto $\mathcal X^*$: a point of $\mathcal X^*$ at distance $\operatorname{dist}(x,\mathcal X^*)$ from $x$. Each of the following conditions involves a constant $\mu>0$, which may differ between conditions (Appendix A, pp. 11–12):

• SC (strong convexity): $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac\mu2\|y-x\|^2$ for all $x,y$.
• ESC (essential strong convexity): the same inequality for all $x,y$ with $x_p=y_p$.
• WSC (weak strong convexity): $f^*\ge f(x)+\langle\nabla f(x),x_p-x\rangle+\frac\mu2\|x_p-x\|^2$ for all $x$.
• RSI (restricted secant inequality): $\langle\nabla f(x),x-x_p\rangle\ge\mu\|x_p-x\|^2$ for all $x$.
• EB (error bound): $\|\nabla f(x)\|\ge\mu\|x_p-x\|$ for all $x$.
• PL (Polyak–Łojasiewicz): $\frac12\|\nabla f(x)\|^2\ge\mu(f(x)-f^*)$ for all $x$.
• QG (quadratic growth): $f(x)-f^*\ge\frac\mu2\|x_p-x\|^2$ for all $x$.

Formalization targets

Goal: Theorem 2 (p. 3)

Read each condition as "it holds for some $\mu>0$". For $f$ with a Lipschitz-continuous gradient,

$$(SC)\to(ESC)\to(WSC)\to(RSI)\to(EB)\equiv(PL)\to(QG),$$

and if $f$ is also convex,

$$(RSI)\equiv(EB)\equiv(PL)\equiv(QG).$$

The goal states no constants, because the constant may change along the chain.

Milestones: the implications of Appendix A, with their constants

The appendix proves a subset of the arrows, each with an explicit constant. The rest follow by transitivity.

$$\text{SC}(\mu)\Rightarrow\text{ESC}(\mu),\quad \text{ESC}(\mu)\Rightarrow\text{WSC}(\mu),\quad \text{WSC}(\mu)\Rightarrow\text{RSI}(\mu/2),\quad \text{RSI}(\mu)\Rightarrow\text{EB}(\mu),$$ $$\text{EB}(\mu)\Rightarrow\text{PL}(\mu^2/L),\quad \text{PL}(\mu)\Rightarrow\text{QG}(\mu),\quad \text{PL}(\mu)\Rightarrow\text{EB}(\mu),\quad \text{QG}(\mu)+\text{convex}\Rightarrow\text{RSI}(\mu/2).$$

One further milestone is display (20). Under PL, $g=\sqrt{f-f^*}$ satisfies $\|\nabla g(x)\|\ge\sqrt{\mu/2}$ at every $x\notin\mathcal X^*$.

Significance

The result. Theorem 2 shows that QG is the weakest of the seven conditions. QG alone does not rule out non-global local minima, so it cannot guarantee that gradient descent reaches a global minimizer. Among the conditions considered, PL and the equivalent EB are therefore the most general that still give linear convergence to a global minimum. The paper's Theorem 1 gives that rate under PL with a one-paragraph proof. For convex $f$, RSI (there called restricted strong convexity), EB, PL and QG are one condition. A rate proved under any of them transfers to the others, up to the constants of the milestones.

Formalizing it. The result is proved on paper, and the arrows of Appendix A are short, except PL → QG. A machine-checked version adds three things. It fixes a precise meaning for $x_p$ when $\mathcal X^*$ is not convex and a nearest point is not unique. It records the correct constant in EB → PL: the printed text says $\mu/L$, while the displayed argument yields $\mu^2/L$. It puts PL → QG for non-convex $f$ on a checked footing; the acknowledgments note an earlier error in this proof. No formalization of these implications is known to be on the platform or in Mathlib.

Difficulty

Most arrows are one-line rearrangements or the Cauchy–Schwarz inequality. EB → PL also needs the quadratic upper bound implied by the Lipschitz gradient, and $\nabla f(x_p)=0$ at a global minimizer.

The obstacle is PL → QG without convexity. The natural first idea fails. Integrating along the segment from $x$ to $x_p$ uses no information from PL, because the gradient along that segment is unrelated to the gap $f-f^*$. The implication is global: it converts a pointwise bound on the gradient into a lower bound on $f$ in terms of the distance to a possibly non-convex set $\mathcal X^*$. Any proof has to bound the distance to $\mathcal X^*$ by the length of some path into it that is controlled by $f$. Building such a path in Lean, with its existence, its arrival at $\mathcal X^*$ in finite time and a bound on its length, needs analysis that is not yet assembled in Mathlib for this purpose.

Formalization scope

• Space. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d), abbreviated E d. Gradients are Mathlib's gradient. The Lipschitz gradient is the literal hypothesis ∀ x y, ‖gradient f x - gradient f y‖ ≤ L * ‖x - y‖ with 0 < L, together with Differentiable ℝ f.
• Solution set. Non-emptiness is carried by a global minimizer xstar with ∀ y, f xstar ≤ f y, and $f^*$ is f xstar. In WSC, $f^*$ is written $f(x_p)$.
• Projection. $x_p$ is an explicit map p with IsProjSel f p: p x lies in $\mathcal X^*$ and ‖x - p x‖ = Metric.infDist x X*. Every condition, and Theorem 2, refers to an arbitrary such selection. ESC's "$x_p=y_p$" is p x = p y for that same selection. No Classical.choose is used.
• PL is the published predicate ShiOptRates.PolyakLojasiewicz f (gradient f) μ fstar (definition ShiOptrates_FunctionClass), i.e. $2\mu(f(x)-f^*)\le\|\nabla f(x)\|^2$. This is the paper's (3) multiplied by 2.
• Constants. Each milestone carries the constant of its appendix bullet and the hypothesis $\mu>0$. The goal uses Holds C := ∃ μ, 0 < μ ∧ C μ independently on each side of every arrow. Convexity is ConvexOn ℝ Set.univ f.
• Dropped standing hypotheses. Milestones whose argument does not use the Lipschitz gradient omit it: SC → ESC, ESC → WSC, WSC → RSI, RSI → EB, QG + convex → RSI, and (20). Each is then a slightly stronger statement.
• Corrected constant. EB → PL is stated with $\mu^2/L$, which is what the paper's displayed argument proves. The quoted milestone text keeps the printed "$\mu/L$".
• No trivialization. Every condition is quantified over all $x$ (and $y$). The selection p is constrained by IsProjSel, not free, and the goal's hypotheses are satisfiable: $f(x)=\frac12\|x\|^2$ with $p\equiv0$, $L=1$ satisfies all of them and SC with $\mu=1$. A formalization that fixed one $\mu$ for the whole chain, or replaced $x_p$ by an unconstrained map, would be a different theorem.
• Reuse. The condition predicates and the projection selection are reusable by any development on linear convergence without strong convexity. A general "PL implies QG" lemma via gradient flow is reusable beyond this mission. Contributions toward the ODE and arc-length infrastructure are welcome.

Selected references

• H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition, ECML PKDD 2016; arXiv:1608.04636v4 (2020). https://arxiv.org/abs/1608.04636
• B. T. Polyak, Gradient methods for minimizing functionals, Zh. Vychisl. Mat. Mat. Fiz. 3(4):643–653, 1963 (English translation: USSR Comput. Math. Math. Phys. 3(4):864–878). https://doi.org/10.1016/0041-5553(63)90382-3
• J. Bolte, T. P. Nguyen, J. Peypouquet, B. W. Suter, From error bounds to the complexity of first-order descent methods for convex functions, Math. Program. 165, 2017. https://arxiv.org/abs/1510.08234
• H. Zhang, The restricted strong convexity revisited: analysis of equivalence to error bound and quadratic growth, Optim. Lett. 11, 2017. https://arxiv.org/abs/1511.01635
• H. Zhang, New analysis of linear convergence of gradient-type methods via unifying error bound conditions, Math. Program. 180, 2020. https://arxiv.org/abs/1606.00269
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46, 1993. https://doi.org/10.1007/BF02096261

Motivation

A high dimensional expander is a simplicial complex whose local structure forces global expansion. The high order random walks on such a complex move from a $k$-face to a $k$-face through a common $(k+1)$-face. They were studied for their connection to agreement tests in probabilistically checkable proofs (Dinur–Kaufman 2017; Kaufman–Mass 2017), and they later became a tool for sampling. Anari, Liu, Oveis Gharan and Vinzant (arXiv:1811.01816) used the mixing bound of this mission to prove the Mihail–Vazirani conjecture: the bases-exchange walk of every matroid mixes rapidly.

Timeline:

• 1973. Garland (Ann. of Math. 97) shows that spectral gaps in the links of a complex control its cohomology. Inner products are localized to links; this is now called Garland's method.
• 2017. Kaufman and Mass (arXiv:1604.02947) bound the second eigenvalue of the high order walks on complexes with well-expanding links. Dinur and Kaufman obtain the optimal bound under a two-sided spectral gap in the links, as Kaufman–Oppenheim explain.
• 2018. Oppenheim (Discrete Comput. Geom. 59) shows how spectral gaps descend from top-dimensional links to lower ones ("trickling down").
• 2017–2021. Kaufman and Oppenheim (arXiv:1707.02799v3) obtain the optimal mixing bound under a one-sided gap only: negative eigenvalues of the links do not matter. This is the target of this mission.

Setting

Let $V$ be a type of vertices. A pure $n$-dimensional finite simplicial complex $X$ is a finite family of finite subsets of $V$ that is closed under subsets, has faces of at most $n+1$ elements, and has every face contained in a face of exactly $n+1$ elements. A face with $k+1$ elements is a $k$-face; $X(k)$ is the set of $k$-faces, and $X(-1)=\{\emptyset\}$.

A weight function is a map $m$ from the faces of $X$ to $(0,\infty)$ that is balanced: for $-1\le k\le n-1$ and $\tau\in X(k)$,

$$m(\tau)=\sum_{\sigma\in X(k+1),\ \tau\subseteq\sigma}m(\sigma).$$

A $k$-cochain is a function $\phi:X(k)\to\mathbb R$. The cochains carry the inner product $\langle\phi,\psi\rangle=\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)\psi(\sigma)$ and the norm $\|\cdot\|$. The cochains orthogonal to the constants form $C^k_0(X,\mathbb R)=\{\phi:\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)=0\}$.

The upper random walk $M^+_k$ acts on $k$-cochains by

$$M^+_k\phi(\tau)=\frac{1}{k+2}\,\phi(\tau)+\sum_{\tau'\in X(k),\ \tau\cup\tau'\in X(k+1)}\frac{m(\tau\cup\tau')}{(k+2)\,m(\tau)}\,\phi(\tau').$$

It stays put with probability $1/(k+2)$, and otherwise moves to a neighbouring $k$-face with probability proportional to the weight of their union.

The link of a face $\tau$ is $X_\tau=\{\eta\in X:\eta\cap\tau=\emptyset,\ \tau\cup\eta\in X\}$, weighted by $m_\tau(\eta)=m(\tau\cup\eta)$. On the vertices of $X_\tau$, the non-lazy upper walk $(M')^+_{\tau,0}=2M^+_{\tau,0}-I$ is the weighted random walk on the 1-skeleton of the link. Let $\mu_\tau$ be its second largest eigenvalue. $X$ is a one-sided $\lambda$-local spectral expander if $\mu_\tau\le\lambda$ for every face $\tau$ of dimension $-1,\dots,n-2$. The empty face is included, and its link is $X$ itself.

Formalization targets

Goal: Theorem 5.4 (p. 17)

Let $0\le\lambda\le1$ and let $X$ be a one-sided $\lambda$-local spectral expander. Then for every $0\le k\le n-1$ and every $\phi\in C^k_0(X,\mathbb R)$,

$$\|M^+_k\phi\|\le\Big(\frac{k+1}{k+2}+\frac{k+1}{2}\,\lambda\Big)\|\phi\|.$$

Milestones

They follow the paper's proof order:

• Lemma 3.6 and Corollary 3.7: the adjoint $d^*$ of the signless differential $d$, and the factorizations $d^*d=(k+2)M^+_k$, $dd^*=(k+1)M^-_k$.
• Proposition 4.1 (1)–(3), Garland's localization identities, and Proposition 4.2:

$$\|d\phi\|^2=\|d^*\phi\|^2+\|\phi\|^2+\sum_{\tau\in X(k-1)}\langle (M')^+_{\tau,0}(I-M^-_{\tau,0})\phi_\tau,\phi_\tau\rangle .$$

• Lemma 4.3, which bounds the link terms by $(k+1)\mu\|\phi\|^2$.
• Lemma 5.1.
• Theorem 5.2 (the Decomposition Theorem).
• Corollary 5.3, in its general and its one-sided form:

$$\|d\phi\|^2\le\sum_{j=0}^{k}\Big(k+1-j+\frac{(k+j+2)(k+1-j)}{2}\lambda\Big)\|\phi^j\|^2,\qquad \|\phi\|^2=\sum_{j=0}^k\|\phi^j\|^2.$$

Significance

The result. The coefficient $\frac{k+1}{k+2}$ is the baseline in the paper's mixing bound, and the bound is optimal up to the $O(\lambda)$ term. It needs a gap on one side only: links may have eigenvalues near $-1$. This matters in two places. The links of a matroid's independence complex are only one-sided expanders, so the matroid application needs exactly this case. And the links of Ramanujan complexes are one-sided expanders, so this bound gives optimal mixing on them; the two-sided bound of Dinur–Kaufman does not apply to them.

Formalizing it. The theorem is proved on paper; the Lean statements in this mission are proof targets. Completing the mission would give machine-checked proofs of the mixing bound, Garland's localization identities, and the Decomposition Theorem, built on definitions of weighted simplicial complexes, links, and their random walks. Lemma 4.3 and Corollary 5.3 are stated with a correction: as printed they are false when a link eigenvalue bound is negative (see Formalization scope).

Difficulty

The obvious argument fails. The tempting route bounds the second eigenvalue of $M^+_k$ directly from the link spectra, by induction on $k$. But $M^+_k$ has large eigenvalues near $\frac{k+1-j}{k+2}$ for every $j$, coming from cochains of the form $d\psi$ with $\psi$ of lower degree. A single spectral-gap estimate cannot separate these levels from one another. The paper instead splits $\phi$ into contributions from every degree $j\le k$; this is the Decomposition Theorem, and each piece is controlled separately. Formally, the main costs are:

• the double-counting behind Proposition 4.1 (Appendix A, pp. 28–29);
• a square root of a positive self-adjoint operator on a weighted finite-dimensional space (Theorem 5.2);
• the bookkeeping of degrees and links.

Formalization scope

Faces are Finset V. $X$ is a Finset (Finset V), and $X(k)$ is cells X (k + 1): faces are indexed by their number of vertices. Cochains are functions Finset V → ℝ that are read only on the relevant faces. Every operator is zero off $X$. The weight is positive on faces; the paper writes $\mathbb R^+$, and $m$ appears in denominators. Every goal-level statement carries the standing assumption of §2: $X$ is pure $n$-dimensional and $m$ is a weight. Orthogonality to the constants is always weighted by $m$ (or by $m_\tau$ in a link).

The adjoint $d^*$ is defined by its explicit formula; that it is the adjoint is Lemma 3.6. The eigenvalue condition $\mu_\tau\le\lambda$ is stated in Rayleigh form: $\langle (M')^+_{\tau,0}g,g\rangle\le\lambda\|g\|^2$ for every $g$ on the vertices of $X_\tau$ that is $m_\tau$-orthogonal to the constants. It is equivalent to the eigenvalue form even for disconnected links. A Rayleigh bound over all $g$, constants included, would be unsatisfiable for $\lambda<1$ and would make the goal vacuous; it is ruled out. The predicate quantifies over every face of dimension $-1$ to $n-2$, including $\emptyset$.

Corrections, all disclosed in the items:

• Lemma 4.3 is stated with a bound $\mu\ge\max(\mu_k,0)$. The printed version with $\mu_k<0$ fails already for the complete graph on three vertices.
• Corollary 5.3 accordingly takes $\mu_i\ge0$ and $\lambda\ge0$. Its two formal statements retain the page's assumption that every link of dimension at least one is connected, including $X$ itself.
• The proof of Theorem 5.4 ends with $(k+1)\lambda$; the statement's $\frac{k+1}{2}\lambda$ is formalized.

Welcome contributions: proofs of any milestone. Reusable lemmas on finite weighted inner products, on double counting over faces of a Finset (Finset V), and on links are useful beyond this mission; the companion mission on two-sided expanders uses the same objects.

Selected references

• T. Kaufman, I. Oppenheim, High Order Random Walks: Beyond Spectral Gap, arXiv:1707.02799v3, 2021. https://arxiv.org/abs/1707.02799
• N. Anari, K. Liu, S. Oveis Gharan, C. Vinzant, Log-concave polynomials II: High-dimensional walks and an FPRAS for counting bases of a matroid, STOC 2019. https://arxiv.org/abs/1811.01816
• H. Garland, p-adic curvature and the cohomology of discrete subgroups of p-adic groups, Ann. of Math. 97:375–423, 1973. https://doi.org/10.2307/1970781
• T. Kaufman, D. Mass, High dimensional random walks and colorful expansion, ITCS 2017. https://arxiv.org/abs/1604.02947
• I. Oppenheim, Local spectral expansion approach to high dimensional expanders Part I: Descent of spectral gaps, Discrete Comput. Geom. 59(2):293–330, 2018. https://arxiv.org/abs/1709.04431

Multiscale reaction networks and the balance condition

Stochastic models of chemical reaction networks in cell biology routinely combine species present in a handful of copies with species present in thousands, and rate constants that differ by orders of magnitude. Simulating such a system exactly is expensive, and model reduction replaces it with a lower-dimensional limit. A systematic approach, developed by Ball, Kurtz, Popovic and Rempala (2006) and by Kang and Kurtz (arXiv:1011.1672), normalizes species numbers and rate constants by powers of a large parameter $N$ and derives limits as $N\to\infty$ on several time-scales.

For such limits to exist, the normalized species numbers must stay of order one. For a single species this is the species balance condition: either the fastest reaction producing it is as fast as the fastest reaction consuming it, or the time-scale considered is short enough that the imbalance does not show. Kang and Kurtz observed (arXiv:1011.1672v1, §3.2, p. 9) that this is not enough: a collection of species can be produced collectively at a different order of magnitude from the rate at which it is consumed, even when every member is balanced. They therefore impose a balance condition on every nonnegative linear combination of species, which is infinitely many conditions. Section 3.4 of their paper proves combinatorial lemmas that reduce the work of checking them. This mission formalizes the lemmas on positive combinations of two weight vectors.

Setting

A reaction network has $s_0$ species $S_1,\dots,S_{s_0}$ and $r_0$ reactions. Reaction $k$ consumes $\nu_{ik}\in\mathbb N$ molecules of $S_i$ and produces $\nu'_{ik}\in\mathbb N$; its net change is the vector $\zeta_k=\nu'_k-\nu_k$. Each species carries a scaling exponent $\alpha_i\ge0$ and each reaction an exponent $\beta_k\in\mathbb R$; put

$$\rho_k=\beta_k+\nu_k\cdot\alpha=\beta_k+\sum_i\nu_{ik}\alpha_i,$$

the order of magnitude (as a power of $N$) of the rate of reaction $k$.

A weight vector $\theta\in[0,\infty)^{s_0}$ describes the linear combination $\theta\cdot X=\sum_i\theta_iX_i$. Its sign sets (Definition 3.1) are

$$\Gamma^+_\theta=\{k:\theta\cdot\zeta_k>0\},\qquad\Gamma^-_\theta=\{k:\theta\cdot\zeta_k<0\},$$

the reactions that increase and decrease $\theta\cdot X$. Maxima $\max_{k\in S}\rho_k$ are taken in $\mathbb R\cup\{-\infty\}$, with $\max_{k\in\emptyset}\rho_k=-\infty$, and $a\vee b$ is the maximum.

Fix a time-scale exponent $\gamma\in\mathbb R$. Condition 3.2 holds for $\theta$ if either the balance equation

$$\max_{k\in\Gamma^-_\theta}\rho_k=\max_{k\in\Gamma^+_\theta}\rho_k\tag{3.7}$$

or the time-scale constraint

$$\gamma\le\gamma_\theta\equiv\max_{i:\theta_i>0}\alpha_i-\max_{k\in\Gamma^+_\theta\cup\Gamma^-_\theta}\rho_k\tag{3.8}$$

holds, with $\gamma_\theta=+\infty$ when $\Gamma^+_\theta\cup\Gamma^-_\theta=\emptyset$.

Formalization targets

Goal: Lemma 3.8 (p. 18)

Let $\theta^1,\theta^2\in[0,\infty)^{s_0}$, $c_1,c_2>0$, and suppose

$$\Gamma^+_{\theta^1}\cap\Gamma^-_{\theta^2}=\emptyset\quad\text{or}\quad\Gamma^-_{\theta^1}\cap\Gamma^+_{\theta^2}=\emptyset.$$

Then (i) if Condition 3.2 holds for $\theta^1$ and $\theta^2$, it holds for $c_1\theta^1+c_2\theta^2$; and (ii) if (3.7) holds for $\theta^1$ and $\theta^2$, it holds for $c_1\theta^1+c_2\theta^2$.

Milestones, in the order the paper uses them

1. (3.16)–(3.17) (p. 15): $\Gamma^\pm_{c_1\theta^1+c_2\theta^2}\subseteq\Gamma^\pm_{\theta^1}\cup\Gamma^\pm_{\theta^2}$, hence

$$\max_{k\in\Gamma^\pm_{c_1\theta^1+c_2\theta^2}}\rho_k\le\max_{k\in\Gamma^\pm_{\theta^1}}\rho_k\vee\max_{k\in\Gamma^\pm_{\theta^2}}\rho_k.$$

2. Lemma 3.5 (p. 17): (3.8) for $\theta^1,\dots,\theta^m$ implies (3.8) for $\sum_jc_j\theta^j$, $c_j>0$.
3. Lemma 3.6 (p. 17): if $\max_{\Gamma^-_{\theta^1}}\rho=\max_{\Gamma^+_{\theta^1}}\rho>\max_{\Gamma^+_{\theta^2}\cup\Gamma^-_{\theta^2}}\rho$, then (3.7) holds for $c_1\theta^1+c_2\theta^2$.
4. Lemma 3.7 (p. 18): (3.7) for $\theta^1$ and (3.8) for $\theta^2$ give Condition 3.2 for $c_1\theta^1+c_2\theta^2$.
5. (3.35)–(3.36) (p. 19): if $\Gamma^-_{\theta^1}\cap\Gamma^+_{\theta^2}=\emptyset$, then

$$\max_{\Gamma^-_{\theta^1}}\rho\le\max_{\Gamma^-_{c_1\theta^1+c_2\theta^2}}\rho\le\max_{\Gamma^-_{\theta^1}}\rho\vee\max_{\Gamma^-_{\theta^2}}\rho,\quad\max_{\Gamma^+_{\theta^2}}\rho\le\max_{\Gamma^+_{c_1\theta^1+c_2\theta^2}}\rho\le\max_{\Gamma^+_{\theta^1}}\rho\vee\max_{\Gamma^+_{\theta^2}}\rho.$$

Companion results

• Remark 3.9 (p. 18): if no reaction that consumes a species in the support of $\theta^1$ produces a species in the support of $\theta^2$, then $\Gamma^-_{\theta^1}\cap\Gamma^+_{\theta^2}=\emptyset$.
• Lemma 3.10 (p. 19): if (3.7) holds for $\theta^1$, $\theta^2$ and for $\theta^1-\frac{\theta^1\cdot\zeta_k}{\theta^2\cdot\zeta_k}\theta^2$ for every $k\in(\Gamma^+_{\theta^1}\cap\Gamma^-_{\theta^2})\cup(\Gamma^-_{\theta^1}\cap\Gamma^+_{\theta^2})$, then (3.7) holds for $c_1\theta^1+c_2\theta^2$ for all $c_1,c_2>0$.

Significance

Condition 3.2 must hold for every $\theta\in[0,\infty)^{s_0}$ before the limit theorems of the paper's Sections 4–5 apply. Lemma 3.8, together with the decomposition over strongly connected components (Lemma 3.4, the subject of the first mission of this series), turns that infinite family into finitely many checks for many networks: once the condition is known for some generating vectors, it propagates to their positive combinations whenever the sign sets do not conflict. Remark 3.9 gives a condition on the stoichiometry alone under which they do not conflict, and Lemma 3.10 reduces checking balance along a ray of combinations to finitely many breakpoints.

The results are proved in the paper (arXiv:1011.1672v1, pp. 15–19; published in Ann. Appl. Probab. 23(2), 2013), but none is formalized anywhere to our knowledge. The printed proof of Lemma 3.10 is a sketch that treats only the first breakpoint of the ray $\theta^1+c\theta^2$; a machine-checked proof would settle it in full. The definitions of the sign sets, the balance equation and the time-scale constraint are reusable for the other missions of this series.

Difficulty

The proofs are elementary, and the work lies in the bookkeeping. Every statement mixes three conventions: maxima over sets that can be empty (value $-\infty$), a time-scale constant that can be $+\infty$, and strict versus weak sign conditions on $\theta\cdot\zeta_k$. Lemma 3.8 is a case analysis on which disjunct of Condition 3.2 holds for each of $\theta^1$ and $\theta^2$; the obvious idea of applying (3.16)–(3.17) alone fails in the case where both vectors are balanced at the same level ((3.34) in the paper), where only upper bounds are available. That case needs the disjointness hypothesis to get the matching lower bounds (3.35)–(3.36). Lemma 3.10 needs an argument along the whole ray $\theta^1+c\theta^2$, $c>0$: the sign pattern of $(\theta^1+c\theta^2)\cdot\zeta_k$ changes at finitely many values of $c$, and balance has to be tracked through each change, not only the first.

Formalization scope

Species are Fin s and reactions Fin r (0-based indices; $s_0,r_0$ are arbitrary naturals). ν k i is $\nu_{ik}$; $\zeta_{ik}$, $\rho_k$ and $\theta\cdot\zeta_k$ are real numbers, and $\rho$ is defined from $\nu,\alpha,\beta$ rather than taken as a free parameter. A combination $c_1\theta^1+c_2\theta^2$ is c₁ • θ₁ + c₂ • θ₂ on Fin s → ℝ. Maxima are Finset.sup into WithBot ℝ, so the maximum over the empty set is $\bot=-\infty$ and $\vee$ is ⊔. $\gamma_\theta$ is an EReal defined by cases: $+\infty$ if $\Gamma^+_\theta\cup\Gamma^-_\theta=\emptyset$, otherwise the difference of the two maxima computed in $\mathbb R$ (or $-\infty$ if no $\theta_i$ is positive). Every statement carries the paper's standing assumptions $\alpha\ge0$, $\theta^1,\theta^2\ge0$ and $c_1,c_2>0$.

These choices rule out the trivializing encodings: a real-valued maximum with a default value of $0$ on the empty set would make the balance equation hold spuriously; a subtraction in EReal would turn $-\infty-(-\infty)$ into $-\infty$; and dropping $\theta\ge0$ or $c_1,c_2>0$ would change which reactions lie in the sign sets of the combination. In Lemma 3.8 the disjointness of the sign sets is a disjunction, as printed, and the second paragraph's "Condition 3.7" is read as the balance equation (3.7).

The development needs only finite sets, finite sums and order on $\mathbb R\cup\{\pm\infty\}$; no probability theory is involved. Lemmas about Finset.sup into WithBot ℝ over unions and subsets are reusable. Proofs of the milestones, of the goal, and of Lemma 3.10 are all welcome.

Selected references

• H.-W. Kang and T. G. Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, arXiv:1011.1672v1, 2010; Ann. Appl. Probab. 23(2), 2013. https://arxiv.org/abs/1011.1672, https://doi.org/10.1214/12-AAP841
• K. Ball, T. G. Kurtz, L. Popovic and G. Rempala, Asymptotic analysis of multiscale approximations to reaction networks, Ann. Appl. Probab. 16(4):1925–1961, 2006. https://doi.org/10.1214/105051606000000420
• Y. Cao, D. T. Gillespie and L. R. Petzold, The slow-scale stochastic simulation algorithm, J. Chem. Phys. 122(1):014116, 2005. https://doi.org/10.1063/1.1824902