Machine Learning

Motivation

In high-dimensional regression the number of candidate predictors $M$ can far exceed the number of observations $n$. A regression function can then be estimated only if it is well approximated by a combination of a few elements of a large dictionary. The Lasso is the most widely used estimator in this regime. The question this mission formalizes is how well the Lasso predicts when the truth is not assumed to be sparse, or even to lie in the span of the dictionary.

A sparsity oracle inequality answers it. It bounds the prediction error of the estimator by the error of the best sparse approximation of the truth, which only an oracle knowing the truth could compute, plus a remainder proportional to the sparsity of that approximation times $\log M/n$. Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 37(4), 2009) proved such an inequality for the Lasso under their restricted eigenvalue (RE) condition. Earlier oracle inequalities for Lasso-type estimators in fixed design (Bunea, Tsybakov and Wegkamp, 2006–2007) required the Gram matrix to be positive definite or to satisfy a mutual-coherence condition. The RE condition is weaker and allows $M\gg n$, and it is now the standard hypothesis in this literature.

Setting

A dictionary $f_1,\dots,f_M$ is evaluated at fixed points $Z_1,\dots,Z_n$. This gives the design matrix $X=(f_j(Z_i))\in\mathbb R^{n\times M}$ and, for an unknown regression function $f$, the vector $f=(f(Z_1),\dots,f(Z_n))^\top$. The observations are

$$y=f+W,\qquad W_1,\dots,W_n\ \text{independent}\ \mathcal N(0,\sigma^2),\ \sigma>0 .$$

Nothing is assumed about $f$. For $v\in\mathbb R^n$ the empirical norm is $\|v\|_n=(\frac1n\sum_iv_i^2)^{1/2}$, and for $\beta\in\mathbb R^M$ we write $f_\beta=X\beta$. The column norms $\|f_j\|_n$ are assumed nonzero, with $f_{\max}=\max_j\|f_j\|_n$ and $f_{\min}=\min_j\|f_j\|_n$. The support of $\beta$ is $J(\beta)=\{j:\beta_j\neq0\}$ and its sparsity is $\mathcal M(\beta)=|J(\beta)|$.

The Lasso $\hat\beta_L$ is any minimiser of

$$\frac1n\sum_{i=1}^n\big(y_i-(X\beta)_i\big)^2+2r\sum_{j=1}^M\|f_j\|_n|\beta_j|,\qquad r=A\sigma\sqrt{\frac{\log M}{n}},\ A>2\sqrt2,$$

and $\hat f_L=X\hat\beta_L$.

Assumption RE$(s,c_0)$ holds with constant $\kappa>0$ if, for every $J_0\subseteq\{1,\dots,M\}$ with $|J_0|\le s$ and every $\delta\neq0$ with $|\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1$,

$$\kappa\sqrt n\,|\delta_{J_0}|_2\le|X\delta|_2 .$$

The paper's $\kappa(s,c_0)$ is the largest such constant.

Formalization targets

Goal: Theorem 6.1

Fix $\varepsilon>0$, $n\ge1$, $M\ge2$, $1\le s\le M$, and let RE$(s,(3+4/\varepsilon)f_{\max}/f_{\min})$ hold with constant $\kappa$. With probability at least $1-M^{1-A^2/8}$, every Lasso solution satisfies, simultaneously for all $\beta$ with $\mathcal M(\beta)\le s$,

$$\|\hat f_L-f\|_n^2\le(1+\varepsilon)\Big\{\|f_\beta-f\|_n^2+C(\varepsilon)\frac{f_{\max}^2A^2\sigma^2}{\kappa^2}\,\frac{\mathcal M(\beta)\log M}{n}\Big\},\qquad C(\varepsilon)=\frac{4(2+\varepsilon)^2}{\varepsilon(1+\varepsilon)} .$$

Milestones

1. (B.4): the noise event $\mathcal A=\bigcap_j\{2|V_j|\le r\|f_j\|_n\}$, with $V_j=n^{-1}\sum_iX_{ij}W_i$, satisfies $P(\mathcal A^c)\le M^{1-A^2/8}$.
2. (B.1) on $\mathcal A$: for every Lasso solution and every $\beta$,

$$\|\hat f_L-f\|_n^2+r\sum_j\|f_j\|_n|\hat\beta_j-\beta_j|\le\|f_\beta-f\|_n^2+4r\sum_{j\in J(\beta)}\|f_j\|_n|\hat\beta_j-\beta_j| .$$

3. Lemma B.1: the same inequality with probability at least $1-M^{1-A^2/8}$.
4. Cone step: in the case $\varepsilon\|f_\beta-f\|_n^2<4r\sum_{J(\beta)}\|f_j\|_n|\hat\beta_j-\beta_j|$, the difference $\hat\beta_L-\beta$ lies in the cone with constant $(3+4/\varepsilon)f_{\max}/f_{\min}$ at $J(\beta)$.
5. Inequality before decoupling: $\|\hat f_L-f\|_n^2\le\|f_\beta-f\|_n^2+4rf_{\max}\kappa^{-1}\sqrt{\mathcal M(\beta)}\,(\|\hat f_L-f\|_n+\|f_\beta-f\|_n)$.
6. Decoupled bound: $\|\hat f_L-f\|_n^2\le\frac{b+1}{b-1}\|f_\beta-f\|_n^2+\frac{8b^2f_{\max}^2}{(b-1)\kappa^2}r^2\mathcal M(\beta)$ for all $b>1$.
7. Corollary 6.2: the same oracle inequality with $\gamma$ in place of $\kappa$ and no global RE assumption. The infimum runs over those $\beta$ with $\mathcal M(\beta)\le s$ whose support alone satisfies the restricted eigenvalue inequality with constant $\gamma$.

Significance

The theorem says that, up to the factor $1+\varepsilon$ and a remainder of order $\mathcal M(\beta)\log M/n$, the Lasso predicts as well as the best $s$-sparse linear combination of the dictionary. This is the case even when $f$ is not sparse and not in the span of the dictionary. The remainder is the parametric rate for $\mathcal M(\beta)$ parameters, inflated by $\log M$ and by the ill-posedness factor $f_{\max}^2/\kappa^2$. Together with Theorem 5.1 of the same paper (mission II of this series), it shows that the Lasso and the Dantzig selector are within the same distance of the sparse oracle. The oracle inequality is used in aggregation, in model selection, and as a black box in later sparse-estimation papers.

The result is proved in the paper. It has not been formalized: at the time of writing, no Lasso oracle inequality and no probabilistic Lasso bound exist on Prove2Me or in Mathlib. What this mission contributes is a machine-checked proof of the paper's Theorem 6.1 with an explicit constant $C(\varepsilon)$. The paper leaves $C(\varepsilon)$ unspecified, and its proof fixes the value used here. The mission also formalizes the Gaussian-tail step (B.4) and the deterministic basic inequality (B.1), both of which are shared with the paper's other Lasso results.

Difficulty

There is no sparse truth, so the usual argument does not apply. That argument places the error $\hat\beta_L-\beta^*$ in the RE cone and reads off a rate. Here the competitor $\beta$ is arbitrary, and the approximation error $\|f_\beta-f\|_n$ can dominate the penalty terms, in which case the error is not in the cone. The RE assumption can be used only where the error does lie in a cone, and the cone constant available there depends on $\varepsilon$ and on the column-norm ratio $f_{\max}/f_{\min}$, because the penalty is weighted while RE is stated for unweighted vectors. What RE then yields is an inequality quadratic in $\|\hat f_L-f\|_n$ with a cross term, not the $(1+\varepsilon)$ form directly, and the constant $C(\varepsilon)$ is determined by how that cross term is absorbed. On the probabilistic side, the whole argument must run on one event of probability at least $1-M^{1-A^2/8}$. That event may depend neither on $\beta$ nor on the choice of minimiser. The Lasso need not have a unique solution.

Formalization scope

• The dictionary enters only through $X\in\mathbb R^{n\times M}$ (Matrix (Fin n) (Fin M) ℝ) and the target only through $f\in\mathbb R^n$, which is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, independent random variables, each with law gaussianReal 0 σ², and $\sigma>0$.
• The Lasso is an argmin predicate, and every statement is made for every minimiser. "With probability at least $p$" means a measurable event $E$ with $P(E)\ge p$, chosen before the competitor $\beta$ and the minimiser.
• RE is stated through a witness $\kappa>0$. Since $\kappa(s,c_0)$ is attained and every bound decreases in $\kappa$, this is equivalent to the paper's form, and it avoids a real infimum over an empty set.
• The infimum over $\{\beta:\mathcal M(\beta)\le s\}$ is written as "for every such $\beta$". This is equivalent, because the set contains $\beta=0$ and the bracket is nonnegative.
• Correction/strengthening. The printed theorem has an unspecified $C(\varepsilon)>0$. The goal instead uses the value $C(\varepsilon)=4(2+\varepsilon)^2/(\varepsilon(1+\varepsilon))$ that the proof yields with $b=1+2/\varepsilon$, and this implies the printed statement. Corollary 6.2 uses the same explicit constant.
• The standing assumptions of Section 2 ($M\ge2$ and every $\|f_j\|_n\neq0$) are hypotheses of every theorem.
• Some formalizations would make the result trivial, and they are excluded here. The noise must be exactly i.i.d. $\mathcal N(0,\sigma^2)$ with $\sigma>0$ and must enter only through $y=f+W$. The target $f$ must not be restricted to $X\beta^*$. The event must be measurable. The constant must depend on $\varepsilon$ alone.
• A single definition file provides the empirical norms, $f_{\max}$, $f_{\min}$, support and sparsity, the weighted Lasso, RE and its single-set version (the family $\Lambda_{s,\gamma,c_0}$ of Corollary 6.2), the Gaussian noise model and the event $\mathcal A$. The same objects appear in the other missions of this series. Gaussian-tail and union-bound lemmas proved along the way are reusable, and contributions of such lemmas are welcome.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. Cited version: arXiv:0801.1095v3; DOI 10.1214/08-AOS620.
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Statist. 1, 169–194, 2007. DOI 10.1214/07-EJS008.
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Aggregation for Gaussian regression, Ann. Statist. 35(4), 1674–1697, 2007. DOI 10.1214/009053606000001587.
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1), 267–288, 1996. DOI 10.1111/j.2517-6161.1996.tb02080.x.

Motivation

In high-dimensional linear regression one observes $y = X\beta^* + w \in \mathbb R^n$ with a design matrix $X\in\mathbb R^{n\times M}$ whose number of columns $M$ may far exceed the sample size $n$. The two standard estimators of a sparse $\beta^*$, the Lasso (Tibshirani, 1996) and the Dantzig selector (Candès and Tao, 2007), both come with error bounds of order $s\log M/n$ for an $s$-sparse $\beta^*$, but only under a condition on $X$: since $X$ has a non-trivial kernel when $M>n$, some form of restricted invertibility is unavoidable.

Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 2009) introduced the restricted eigenvalue (RE) condition, which asks for invertibility of $X$ only on a cone of approximately sparse vectors. It is weaker than the conditions used before it and has since become the default assumption in the sparse-estimation literature. Section 4 of the paper relates RE to the earlier conditions:

• 2005–2007: Candès and Tao (arXiv:math/0506081) analyse the Dantzig selector under a uniform uncertainty principle involving restricted eigenvalues and restricted correlations of $X$; the condition $\phi_{\min}(2s)>\theta_{s,2s}$ is Assumption 1 below with $c_0=1$.
• 2006–2009: Meinshausen and Yu (arXiv:math/0605584) analyse the Lasso under a lower bound on sparse eigenvalues of order $s\log n$.
• 2006: Donoho, Elad and Temlyakov (doi:10.1109/TIT.2005.860430) use mutual coherence for sparse recovery; 2007: Bunea, Tsybakov and Wegkamp (doi:10.1214/07-EJS008) use coherence-type conditions for the Lasso.
• 2009: Bickel, Ritov and Tsybakov show (Lemma 4.1 and Section 4) that each of these conditions implies RE.

This mission formalizes those implications.

Setting

Fix integers $n\ge1$ and $M\ge2$ and a matrix $X\in\mathbb R^{n\times M}$ with columns $x_1,\dots,x_M$. The Gram matrix is $\Psi_n = X^TX/n$. For $\delta\in\mathbb R^M$ and $J\subseteq\{1,\dots,M\}$, $\delta_J$ is the vector equal to $\delta$ on $J$ and $0$ off $J$; $|\cdot|_1$, $|\cdot|_2$ are the $\ell_1$ and Euclidean norms; $\mathcal M(\delta)$ is the number of non-zero coordinates of $\delta$; $J_0^c$ is the complement of $J_0$.

The cone condition for $J_0$ and $c_0>0$ is

$$|\delta_{J_0^c}|_1\le c_0\,|\delta_{J_0}|_1. \tag{4.1}$$

Assumption RE$(s,c_0)$ holds with constant $\kappa>0$ if $|X\delta|_2\ge\kappa\sqrt n\,|\delta_{J_0}|_2$ for every $J_0$ with $|J_0|\le s$ and every $\delta\ne0$ satisfying (4.1). For $m\ge s$, let $J_1$ be a set of $m$ indices outside $J_0$ carrying the $m$ largest $|\delta_j|$, and $J_{01}=J_0\cup J_1$; Assumption RE$(s,m,c_0)$ replaces $|\delta_{J_0}|_2$ by $|\delta_{J_{01}}|_2$.

The restricted eigenvalues are $\phi_{\min}(u)$ and $\phi_{\max}(u)$, the minimum and maximum of $x^T\Psi_nx/|x|_2^2$ over $x$ with $1\le\mathcal M(x)\le u$. The restricted correlations $\theta_{m_1,m_2}$ are the maximum of $c_1^TX_{I_1}^TX_{I_2}c_2/(n|c_1|_2|c_2|_2)$ over disjoint index sets $I_1,I_2$ with $|I_i|\le m_i$ and non-zero $c_i\in\mathbb R^{I_i}$. Two constants are attached to them:

$$\kappa_1(s,c_0)=\sqrt{\phi_{\min}(2s)}\Big(1-\frac{c_0\theta_{s,2s}}{\phi_{\min}(2s)}\Big),\qquad \kappa_2(s,m,c_0)=\sqrt{\phi_{\min}(s+m)}\Big(1-c_0\sqrt{\tfrac{s\,\phi_{\max}(m)}{m\,\phi_{\min}(s+m)}}\Big).$$

$P_{01}$ is the orthogonal projector in $\mathbb R^n$ onto the span of the columns $x_j$, $j\in J_{01}$.

Formalization targets

Goal: Lemma 4.1 (ii)

For integers $1\le s\le M/2$, $m\ge s$, $s+m\le M$ and $c_0>0$, if Assumption 2 $m\,\phi_{\min}(s+m)>c_0^2\,s\,\phi_{\max}(m)$ holds, then $\kappa_2(s,m,c_0)>0$, RE$(s,c_0)$ and RE$(s,m,c_0)$ hold with constant $\kappa_2(s,m,c_0)$, and for every $J_0$ with $|J_0|\le s$ and every $\delta$ satisfying (4.1)

$$\frac1{\sqrt n}|P_{01}X\delta|_2\ \ge\ \kappa_2(s,m,c_0)\,|\delta_{J_{01}}|_2 .$$

Assumption 2 involves no correlations, only extreme eigenvalues of small principal submatrices of $\Psi_n$.

Lemma 4.1 (i)

For $1\le s\le M/2$ and $c_0>0$, Assumption 1 $\phi_{\min}(2s)>c_0\theta_{s,2s}$ implies the same conclusions with $m=s$ and constant $\kappa_1(s,c_0)$.

Coherence-type conditions (Section 4)

For $1\le s\le M$ and $c_0>0$, each of

$$\phi_{\min}(s)>2c_0\theta_{s,1}\sqrt s,\qquad \phi_{\min}(s)>2c_0\theta_{1,1}s,\qquad \operatorname{diag}\Psi_n=1\ \text{and}\ \theta_{1,1}<\frac1{(1+2c_0)s}$$

(Assumptions 3, 4, 5) implies RE$(s,c_0)$, with the constants $\kappa^2=\phi_{\min}(s)-2c_0\theta_{s,1}\sqrt s$, $\phi_{\min}(s)-2c_0\theta_{1,1}s$ and $1-(1+2c_0)\theta_{1,1}s$ respectively.

The milestones are the steps of the proof in Appendix A — the projection inequality (A.1), the block bound (A.2), the shelling bound (A.3), the Candès–Tao correlation bound used for part (i) — followed by part (i) and the three coherence-type implications.

Significance

RE$(s,c_0)$ with $c_0=3$ and $c_0=1$ is the hypothesis of the paper's prediction and $\ell_1$ bounds for the Lasso and the Dantzig selector (Theorems 5.1, 6.1, 7.1, 7.2), and RE$(s,m,c_0)$ is the hypothesis of its $\ell_p$ bounds. Assumptions 1–5 are stated through quantities that are standard in compressed sensing and random matrix theory, so known bounds for $\phi_{\min}$, $\phi_{\max}$ and $\theta$ of random designs transfer, through this mission's theorems, to every result stated under RE. Lemma 4.1 also shows that RE is weaker than the Candès–Tao condition used for the Dantzig selector.

The results are proved in the paper; parts of Lemma 4.1's proof (the correlation bound for part (i)) are cited from Candès and Tao without proof. None of these results is formalized: the platform has pairwise-incoherence and restricted-nullspace statements from Wainwright's textbook (a different conclusion and normalization) and restricted isometry definitions, but neither restricted eigenvalues $\phi_{\min}(u),\phi_{\max}(u)$, restricted correlations $\theta_{m_1,m_2}$, nor the RE condition in this form.

Difficulty

The naive attempt to bound $|X\delta|_2$ from below splits $\delta=\delta_{J_0}+\delta_{J_0^c}$ and applies an eigenvalue bound to each part. This fails: $\delta_{J_0^c}$ can have up to $M-s$ non-zero coordinates, and no condition on $s$- or $2s$-sparse submatrices controls $|X\delta_{J_0^c}|_2$ directly. The cone condition bounds only the $\ell_1$ norm of $\delta_{J_0^c}$, while eigenvalue conditions speak about $\ell_2$ norms of sparse vectors; bridging the two with the right constant $\sqrt{s/m}$, and keeping track of how the leading block $J_{01}$ interacts with the rest through the projector $P_{01}$, is where the work lies. For part (i), the interaction between disjoint sparse blocks has to be controlled by $\theta_{s,2s}$ rather than by $\phi_{\max}$.

Formalization scope

• Representation. $X$ is Matrix (Fin n) (Fin M) ℝ; vectors are Fin M → ℝ and Fin n → ℝ; $|X\delta|_2=(\sum_i (X\delta)_i^2)^{1/2}$. The projector $P_{01}$ is Mathlib's orthogonal projection on EuclideanSpace ℝ (Fin n) onto the span of the columns indexed by $J_{01}$.
• RE through a witness. RE X s c0 κ asserts the RE inequality with constant $\kappa$ for all admissible $J_0$ and $\delta$. The paper's $\kappa(s,c_0)$ is the largest such $\kappa$ (the minimum is attained), so "RE holds with $\kappa(s,c_0)\ge\kappa_2$" is exactly "$\kappa_2>0$ is a witness". This avoids a real infimum over an empty set when $J_0=\emptyset$.
• Ties. Every admissible choice of $J_1$ (the $m$ largest $|\delta_j|$ outside $J_0$) is quantified over.
• Restricted eigenvalues and correlations are sInf/sSup over nonempty bounded sets (a basis vector for $\phi$; two disjoint singletons for $\theta$, since $M\ge2$), so they equal the paper's attained min/max. $u$, $s$, $m$ are natural numbers; $s\le M/2$ is written $2s\le M$.
• Corrections of the printed statement. (1) Lemma 4.1 says the RE assumptions "hold with $\kappa(s,c_0)=\kappa(s,m,c_0)=\kappa_2(s,m,c_0)$" (and likewise with $\kappa_1$); the proof gives only the lower bound, and the lower bound is what is stated. (2) The paper calls $P_{01}$ "the projector in $\mathbb R^M$"; it acts on $\mathbb R^n$. (3) The Section 4 claims "Assumption 3/4/5 implies RE$(s,c_0)$" are stated with the explicit constant produced by the displayed argument, a labelled strengthening. (4) The Candès–Tao bound is stated with the hypotheses the proof uses: the blocks are disjoint, of sizes at most $s$ and $2s$, and $\phi_{\min}(2s)>0$.
• Ruling out trivializations. RE quantifies over all $J_0$ with $|J_0|\le s$ and all non-zero $\delta$ in the cone, and bounds the full $|X\delta|_2$, not $|X\delta_{J_0}|_2$; no hypothesis restricts $X$ beyond the stated assumptions. The hypotheses are satisfiable: for $n=M=4$, $X=2I$ (so $\Psi_n=I$), $s=1$, $m=2$, $c_0=1$, Assumption 2 reads $2>1$.
• Infrastructure. A sparse-vector library (restriction, support, sorting coordinates into blocks) and facts about orthogonal projections onto column spans are needed; both are reusable for the other missions of this series and for compressed-sensing results. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. arXiv:0801.1095v3. https://arxiv.org/abs/0801.1095
• E. Candès, T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6), 2313–2351, 2007. https://arxiv.org/abs/math/0506081
• N. Meinshausen, B. Yu, Lasso-type recovery of sparse representations for high-dimensional data, Ann. Statist. 37(1), 246–270, 2009. https://arxiv.org/abs/math/0605584
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Statist. 1, 169–194, 2007. https://doi.org/10.1214/07-EJS008
• D. L. Donoho, M. Elad, V. N. Temlyakov, Stable recovery of sparse overcomplete representations in the presence of noise, IEEE Trans. Inform. Theory 52(1), 6–18, 2006. https://doi.org/10.1109/TIT.2005.860430

Motivation

In online convex optimization a player repeatedly chooses a point $x_t$ from a convex set $P \subseteq \mathbb{R}^n$, after which an adversary reveals a convex cost function $f_t$ and the player pays $f_t(x_t)$. The player's regret after $T$ rounds is its total cost minus the cost of the best fixed point in hindsight. The model covers online portfolio selection, online regression and prediction with expert advice, and it underlies the analysis of stochastic and adaptive optimization methods (Zinkevich 2003; Cesa-Bianchi and Lugosi 2006).

For general convex costs the best achievable regret is of order $\sqrt{T}$. Hazan, Agarwal and Kale (Mach Learn 69, 2007) showed that a curvature condition, $\alpha$-exp-concavity, brings the regret down to order $\log T$, and gave several algorithms that achieve it. This mission concerns the simplest of them, Exponentially Weighted Online Optimization (EWOO), which needs nothing beyond exp-concavity: no bound on gradients and no bound on the diameter of $P$.

Timeline.

• 1991: Cover's universal portfolio algorithm attains regret $O(n \log T)$ for online portfolio selection, whose log-loss is $1$-exp-concave (Cover 1991).
• 1997: Blum and Kalai give a short analysis of the universal portfolio with transaction costs, using a shrinking argument around the best portfolio (Blum and Kalai 1997/1999).
• 2003: Kalai and Vempala give a polynomial-time randomized implementation of Cover's algorithm via random walks (JMLR 3, 2003).
• 2007: Hazan, Agarwal and Kale state EWOO for general $\alpha$-exp-concave costs and prove the regret bound of Theorem 7, alongside the Online Newton Step and Follow the Approximate Leader.

Setting

Fix $n \ge 0$ and a set $P \subseteq \mathbb{R}^n$ that is nonempty, closed, bounded and convex, with positive Lebesgue volume $\mathrm{vol}(P)$. Fix $\alpha > 0$. The cost functions are $f_1, f_2, \dots : \mathbb{R}^n \to \mathbb{R}$, each continuous on $P$ and $\alpha$-exp-concave on $P$: the function $h_t(x) = e^{-\alpha f_t(x)}$ is concave on $P$ (LogRegretOCO.EWOO.IsExpConcave).

EWOO keeps the weights

$$w_t(x) = \exp\Bigl(-\alpha \sum_{\tau=1}^{t-1} f_\tau(x)\Bigr) = \prod_{\tau=1}^{t-1} h_\tau(x),$$

and on round $t$ plays the $w_t$-weighted mean of $P$,

$$x_t = \frac{\int_P x\, w_t(x)\, dx}{\int_P w_t(x)\, dx}$$

(LogRegretOCO.EWOO.ewooPoint). In particular $x_1$ is the centroid of $P$, and each $x_t$ depends only on $f_1, \dots, f_{t-1}$. The regret against a comparator $u \in P$ is $\sum_{t=1}^T \bigl(f_t(x_t) - f_t(u)\bigr)$.

Formalization targets

Goal: Theorem 7

For every $T \ge 1$ and every $u \in P$,

$$\sum_{t=1}^{T} f_t(x_t) - \sum_{t=1}^{T} f_t(u) \;\le\; \frac{1}{\alpha}\, n\, \bigl(1 + \log(T+1)\bigr).$$

This is the paper's printed constant. The paper's proof yields the slightly sharper $\frac{1}{\alpha}\bigl(1 + n\log(T+1)\bigr)$; the printed form is the goal.

Milestones

The proof in §3.4 (p. 187) passes through five displays, each a milestone:

1. Jensen for the weighted mean (first display on p. 187): $h_t(x_t) \ge \int_P h_t\, w_t \,/ \int_P w_t$.
2. Eq. (18): $\prod_{\tau=1}^t h_\tau(x_\tau) \ge \int_P \prod_{\tau=1}^t h_\tau \,/\, \mathrm{vol}(P)$.
3. The nearby set $S = \{\frac{T}{T+1}x^* + \frac{1}{T+1}y : y \in P\}$: for $x \in S$, $h_t(x) \ge \frac{T}{T+1}h_t(x^*)$ and $\prod_{\tau=1}^T h_\tau(x) \ge \frac1e \prod_{\tau=1}^T h_\tau(x^*)$.
4. Volume of $S$: $\mathrm{vol}(S) = \mathrm{vol}(P)/(T+1)^n$.
5. Multiplicative regret bound (last display on p. 187): $\prod_{\tau=1}^T h_\tau(x_\tau) \ge \frac{1}{e(T+1)^n}\prod_{\tau=1}^T h_\tau(x^*)$.

Significance

The result. Theorem 7 shows that exp-concavity alone suffices for logarithmic regret, with a constant $n/\alpha$ that does not depend on the size of $P$ or on the gradients of the costs. Specialised to the log-loss $f_t(x) = -\log(r_t^\top x)$ on the simplex, where $\alpha = 1$, it recovers the $O(n\log T)$ regret of Cover's universal portfolio. The bound is the benchmark against which the computationally cheaper second-order methods of the same paper (Online Newton Step, Follow the Approximate Leader) are compared: those need a gradient bound $G$ and diameter $D$ and pay a factor $(1/\alpha + GD)$.

Formalizing it. The theorem is proved in the paper, and a textbook version with a different constant, $(n/\alpha)\log T + 2/\alpha$, appears in Hazan's Introduction to Online Convex Optimization (Theorem 4.4). No machine-checked proof of either is known. The work here is to formalize the paper's proof: Jensen's inequality for a weighted Lebesgue average in $\mathbb{R}^n$, the change of volume under homothety, and the elementary inequality $(1 + 1/T)^T \le e$. A companion draft of the textbook version exists on the platform as a private item (OnlineConvexOpt.SecondOrder.ewoo_regret) with another constant; it is not reused.

Difficulty

The pieces are classical, but they have to be assembled in measure-theoretic form. The point $x_t$ is a Bochner integral of a vector-valued function over $P$, and its membership in $P$ and the Jensen inequality both require the normalised weight $w_t\,dx/\int_P w_t$ to be a genuine probability measure on $P$, with every integrand integrable. The obvious one-dimensional intuition — "the weighted mean of a convex set lies in the set" — hides the requirement that $P$ be closed and have positive volume.

The second obstacle is that Eq. (18) compares the algorithm with an average of the product $\prod h_\tau$ over all of $P$, while the regret compares it with a single point. The natural attempt, bounding the average below by the value at the comparator, fails: the average can be far smaller than the maximum, and a lower bound that loses more than a factor polynomial in $T$ destroys the logarithmic rate. Controlling this loss in $n$ dimensions, with a constant independent of the shape and size of $P$, is the heart of the argument.

Formalization scope

Points live in EuclideanSpace ℝ (Fin n) with its Lebesgue (Haar) measure volume. Rounds are numbered from $1$: the weights sum over Finset.Ico 1 t, the regret over Finset.Icc 1 T. Cost functions are defined on all of $\mathbb{R}^n$; only their values on $P$ enter. The algorithm is the total function ewooPoint P α f t, and the goal is stated for $x_t$ equal to it — not for an arbitrary sequence satisfying a Jensen-type inequality.

Conventions and corrections relative to the printed text:

• Regret against every comparator. The regret is stated as $\sum_t (f_t(x_t) - f_t(u)) \le$ bound for every $u \in P$, never through a real-valued ⨅ or sInf over $P$, which in Lean would return a junk value off its intended domain and trivialize the statement.
• Positive volume volume P ≠ 0 is added: the algorithm divides by $\int_P w_t$, which the paper leaves implicit. Without it Lean's convention $0^{-1} = 0$ would set $x_t = 0$.
• Continuity of each $f_t$ on $P$ is the paper's standing assumption (§2.2: costs twice differentiable and convex) weakened to what the argument uses; it makes every integral in the development an integral of an integrable function.
• Typos. Theorem 7's "$f_t : P \to \mathbb{R}^n$" is read as real-valued, and its "$\exp(-\alpha f(x))$" as $\exp(-\alpha f_t(x))$. The set-builder "$S = \{x \in S \mid \dots\}$" defines $S$ in terms of itself and is read as the set of all $\frac{T}{T+1}x^* + \frac{1}{T+1}y$, $y \in P$; the printed "$S = x^* + \frac{1}{T+1}P$" is a translate of that set with the same volume.
• Comparator. The paper's $x^*$ is a minimizer of $\sum_t f_t$; milestones 3 and 5 are stated for every $x^* \in P$, which implies the minimizer case.
• Constant. The printed $\frac{1}{\alpha}n(1+\log(T+1))$ is stated, although the proof gives the sharper $\frac{1}{\alpha}(1 + n\log(T+1))$.
• Not in scope. The randomized variant (sampling $x_t$ with density proportional to $w_t$, "in expectation") and the running-time discussion of §3.4.1 have no separate proof in the paper.

Infrastructure that a complete development needs, and that is reusable beyond this mission: Jensen's inequality for concave functions under a probability measure with a continuous density on a compact convex set (Mathlib has ConcaveOn.le_map_integral and Convex.integral_mem); the scaling identity for Haar measure (MeasureTheory.Measure.addHaar_smul); and the elementary bound $(T/(T+1))^T \ge 1/e$. Proofs of any milestone, and a general weighted-Jensen lemma usable across the milestones, are welcome.

Selected references

• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
• T. M. Cover, Universal portfolios, Mathematical Finance 1 (1991), 1–29. https://doi.org/10.1111/j.1467-9965.1991.tb00002.x
• A. Blum, A. Kalai, Universal portfolios with and without transaction costs, Machine Learning 35 (1999), 193–205 (COLT 1997). https://doi.org/10.1023/A:1007530728748
• A. Kalai, S. Vempala, Efficient algorithms for universal portfolios, Journal of Machine Learning Research 3 (2003), 423–440. https://www.jmlr.org/papers/v3/kalai02a.html
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press 2022; arXiv:1909.05207, Theorem 4.4. https://arxiv.org/abs/1909.05207

Motivation

Online convex optimization models repeated decision making against an adversary: in each round a player chooses a point of a convex set, and only then learns the convex cost of that round. It covers online portfolio selection, online regression and routing, and it is the standard lens for analysing learning algorithms that must commit before seeing data. The figure of merit is regret, the player's total cost minus the cost of the best fixed decision in hindsight. For general convex costs regret $\Theta(\sqrt T)$ over $T$ rounds is optimal; for costs with curvature it can be logarithmic.

Hazan, Agarwal and Kale (Mach Learn 69 (2007) 169–192) gave several algorithms with $O(\log T)$ regret for $\alpha$-exp-concave costs, the class that contains the log-loss of portfolio selection. This mission formalizes one of them, Follow the Approximate Leader (FTAL). It connects to the oldest online algorithm, Follow the Leader (FTL), which plays the minimiser of all past costs: FTAL is FTL run on quadratic lower models of the costs, and the paper's analysis shows that FTL itself has logarithmic regret on a class of curved costs.

Timeline. Zinkevich (2003) proved $O(\sqrt T)$ regret for online gradient descent on convex costs. Cover (1991) gave a universal portfolio with logarithmic regret for the log-loss, at a running time exponential in the dimension. Kalai and Vempala (2005) analysed perturbed Follow the Leader through the "be the leader" argument. Hazan, Agarwal and Kale (2007) gave efficient algorithms (Online Newton Step, FTAL, EWOO) with $O(n \log T)$ regret for exp-concave costs.

Setting

The decision set $P \subseteq \mathbb{R}^n$ is nonempty, convex, closed and bounded, and $D$ bounds its diameter: $\|y - z\|_2 \le D$ for $y, z \in P$. In rounds $t = 1, 2, \dots$ the player picks $x_t \in P$ and then pays $f_t(x_t)$, where $f_t$ is a cost function differentiable at the points of $P$ with gradient norm $\|\nabla f_t(x)\| \le G$ on $P$. The cost $f_t$ is $\alpha$-exp-concave ($\alpha > 0$) if $x \mapsto \exp(-\alpha f_t(x))$ is concave on $P$. The regret over $T$ rounds against a comparator $u \in P$ is $\sum_{t=1}^T \bigl(f_t(x_t) - f_t(u)\bigr)$.

Follow the Leader plays $x_t \in \arg\min_{x \in P} \sum_{\tau=1}^{t-1} f_\tau(x)$ (any point of $P$ in round 1). Follow the Approximate Leader (version 1 of the paper's Fig. 3) with parameter $\beta$ plays FTL on the approximate costs

$$\tilde f_\tau(x) = f_\tau(x_\tau) + \nabla_\tau^\top(x - x_\tau) + \frac{\beta}{2}(x - x_\tau)^\top \nabla_\tau\nabla_\tau^\top (x - x_\tau), \qquad \nabla_\tau = \nabla f_\tau(x_\tau).$$

In the Lean development these are IsFTLRun P f x and IsFTALRun P β f x, predicates on a whole trajectory $x$.

Formalization targets

Goal: Theorem 6

With $\beta = \tfrac12 \min\{1/(4GD), \alpha\}$, every FTAL run on $\alpha$-exp-concave costs satisfies, for every $T \ge 1$ and $u \in P$,

$$\sum_{t=1}^T \bigl(f_t(x_t) - f_t(u)\bigr) \le 64\left(\frac1\alpha + GD\right) n\,(\log T + 1).$$

This is the paper's statement with its constant, stated for the algorithm as defined, and for every adversarial sequence of costs.

Milestones

1. Lemma 3: an $\alpha$-exp-concave cost with gradients bounded by $G$ lies above the paraboloid $f(y) + \nabla f(y)^\top(x-y) + \frac\beta2 (\nabla f(y)^\top (x - y))^2$ on $P$.
2. Lemma 9: regret on lower surrogates that touch the costs at the played points dominates the true regret.
3. Lemma 10: $\sum_t f_t(x_{t+1}) \le \sum_t f_t(u)$ for an FTL run ("be the leader").
4. Lemma 12: $A^{-1} \bullet (A - B) \le \log(|A|/|B|)$ for $A \succeq B \succ 0$.
5. Lemma 11: $\sum_{t=1}^T u_t^\top V_t^{-1} u_t \le n\log(r^2T/\varepsilon + 1)$ with $V_t = \sum_{\tau \le t} u_\tau u_\tau^\top + \varepsilon I$.
6. Theorem 5 (corrected constant): FTL on costs $g_t(v_t^\top x)$ with $\|v_t\| \le R$, $|g_t'| \le b$, $g_t'' \ge a$ has regret at most $\frac{nb^2}{a}\log\bigl(\frac{a^2D^2R^2T^2}{b^2} + 1\bigr) + \frac{b^2}{a}$.

Significance

Theorem 6 shows that a simple rule, re-solving a convex quadratic program over all past linearized costs, achieves $O(n\log T)$ regret on exp-concave costs, matching the Online Newton Step up to constants. Theorem 5 is of independent interest: it shows that unmodified Follow the Leader, which has linear regret on linear costs, has logarithmic regret whenever each cost is a strongly curved function of one linear form. Portfolio selection is such a case. The appendix lemmas (log-determinant potential, elliptical potential) are standard tools reused throughout the bandit and online-learning literature.

On formalization: the results are proved on paper; none is formalized. The Lean development provides a reusable encoding of Follow the Leader as a trajectory predicate, the "be the leader" reduction, the surrogate reduction for regret, and the matrix potential inequalities, which the Online Newton Step analysis also needs. The paper's printed statements of Theorem 5 and Lemma 10 contain errors (see below); this mission states corrected versions that suffice for the goal.

Difficulty

The obvious attempt, bounding each term $f_t(x_t) - f_t(x_{t+1})$ by how far the leader moves, requires knowing how far the minimiser of a constrained problem moves when one cost is added. For unconstrained strongly convex quadratics this is an explicit Newton step, but here the minimiser lies in a general convex set and each cost contributes curvature in only one direction, so the accumulated curvature can be singular for many rounds and no per-round strong convexity is available. Turning the per-round movement into a sum that grows only like $\log T$, with the paper's explicit constant, is the core of the work; the printed Theorem 5 bound is negative for small $T$, so the constants must be tracked exactly rather than asymptotically.

Formalization scope

Points are in EuclideanSpace ℝ (Fin n) so that $\|\cdot\|$ is the Euclidean norm; cost functions are functions on all of $\mathbb{R}^n$, differentiable at the points of $P$, with Mathlib's gradient. Rounds are $1$-based; $x_0$ and $f_0$ are unused. $D$ is any upper bound on pairwise distances in $P$. Exp-concavity is ConcaveOn ℝ P (fun x => Real.exp (-α * f t x)). Algorithms are predicates on the trajectory, required at every round, so every tie-breaking rule is covered and adaptive adversaries are included.

Regret is always stated against every comparator $u \in P$. A formalization with a real-valued ⨅/sInf over $P$, or one that bounds the regret of an arbitrary sequence of points rather than of an FTAL run with the paper's $\beta$, would be trivial or false, and is excluded: the goal carries IsFTALRun with $\beta = \frac12\min\{1/(4GD),\alpha\}$.

Corrections and conventions relative to the printed paper:

• Theorem 5: the printed bound $\frac{2nb^2}{a}[\log(DRaT/b) + 1]$ is false when $DRaT/b < 1/e$. The milestone states the bound the paper's proof gives, $\frac{nb^2}{a}\log(\frac{a^2D^2R^2T^2}{b^2} + 1) + \frac{b^2}{a}$, which implies the printed one when $DRaT \ge b$. Derivatives are deriv with explicit differentiability at the points $v_t^\top x$, $x \in P$.
• Lemma 10: printed with $x_t = \arg\min \sum_{\tau=1}^{t} f_\tau$, under which it is false at $T = 1$; the proof and its use require the FTL index $\sum_{\tau=1}^{t-1}$, which is stated.
• Lemma 11: the typo $\sum_\tau u_t u_t^\top$ is read as $\sum_\tau u_\tau u_\tau^\top$, and $\varepsilon > 0$ is stated.
• Lemma 3: $\beta > 0$ is added (the proof divides by $\beta$), and $G, D > 0$ so that $1/(4GD)$ is meaningful.
• Theorem 6: "$f_t : P \to \mathbb{R}^n$" is read as $\mathbb{R}$-valued; only first-order differentiability is assumed; $G, D > 0$. The theorem is true as printed, although the paper's route through the printed Theorem 5 is invalid for $T < 16$.
• Only version 1 of FTAL is formalized; Lemma 4 (equivalence with the pseudoinverse form) is out of scope.

Needed infrastructure: first-order optimality for convex minimisation over a convex set, a mean-value theorem along segments, determinants and eigenvalues of symmetric positive definite matrices (Mathlib has most of this), and the matrix inequality $|A| \le (\operatorname{tr} A/n)^n$. Contributions welcome: proofs of any milestone, and a proof of the goal from the milestones.

Selected references

• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• T. M. Cover, Universal portfolios, Mathematical Finance 1 (1991), 1–29. https://doi.org/10.1111/j.1467-9965.1991.tb00002.x
• A. Kalai, S. Vempala, Efficient algorithms for online decision problems, J. Comput. System Sci. 71 (2005), 291–307. https://doi.org/10.1016/j.jcss.2004.10.016
• E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization 2 (2016). https://arxiv.org/abs/1909.05207

Motivation

Online convex optimization models repeated decision making against an unknown, possibly adversarial environment: in each round $t=1,\dots,T$ a player picks a point $x_t$ of a convex set $\mathcal P\subseteq\mathbb R^n$, and only then learns a convex cost function $f_t$ and pays $f_t(x_t)$. Performance is measured by regret, the excess of the total cost over that of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that online gradient descent has regret $O(\sqrt T)$ for arbitrary convex costs with bounded gradients, and this rate cannot be improved in general.

Many costs met in practice have more curvature than bare convexity. The log-loss $f(x)=-\log(x^\top a)$ of universal portfolio management (Cover, Math. Finance 1991) is not strongly convex, but it is exp-concave. Hazan, Agarwal and Kale (Mach Learn 69, 2007) gave the first efficient algorithms with regret logarithmic in $T$ for exp-concave costs. This mission formalizes the second of their algorithms, the Online Newton Step (ONS), and its regret bound (Theorem 2 of the paper). ONS is the basis of later second-order online methods and appears as a standard algorithm in textbooks on online learning.

Timeline:

• 2003 — Zinkevich: $O(\sqrt T)$ regret for general convex costs by online gradient descent.
• 2006–2007 — Hazan, Agarwal, Kale (COLT 2006; Mach Learn 2007): $O(\log T)$ regret for strongly convex costs by gradient descent, and $O(n\log T)$ regret for exp-concave costs by ONS, Follow the Approximate Leader, and exponentially weighted online optimization.
• 2016 — Hazan, Introduction to Online Convex Optimization (Found. Trends Optim., arXiv:1909.05207): textbook treatment of ONS with modified parameters.

Setting

The decision set $\mathcal P\subseteq\mathbb R^n$ is nonempty, closed, bounded and convex, and $D$ bounds its diameter: $\|x-y\|\le D$ for all $x,y\in\mathcal P$, with the Euclidean norm. The costs $f_1,f_2,\dots$ are real functions, differentiable at every point of $\mathcal P$, with gradient bound $\|\nabla f_t(x)\|\le G$ on $\mathcal P$. A cost is $\alpha$-exp-concave ($\alpha>0$) if $x\mapsto\exp(-\alpha f_t(x))$ is concave on $\mathcal P$.

For a matrix $A$, the generalized projection $\Pi^A_{\mathcal P}(y)$ is a point of $\mathcal P$ minimising $(y-x)^\top A(y-x)$ over $x\in\mathcal P$.

The Online Newton Step fixes

$$\beta=\tfrac12\min\Big\{\frac1{4GD},\alpha\Big\},\qquad \varepsilon=\frac1{\beta^2D^2},$$

writes $\nabla_t=\nabla f_t(x_t)$ and $A_t=\sum_{i=1}^t\nabla_i\nabla_i^\top+\varepsilon I_n$, plays an arbitrary $x_1\in\mathcal P$, and then

$$x_{t+1}=\Pi^{A_t}_{\mathcal P}\Big(x_t-\frac1\beta A_t^{-1}\nabla_t\Big).$$

The regret after $T$ rounds against a comparator $u\in\mathcal P$ is $\sum_{t=1}^T\big(f_t(x_t)-f_t(u)\big)$; the paper's regret is its maximum over $u\in\mathcal P$.

In Lean the objects are LogRegretOCO.ONS.onsBeta, onsEps, onsMatrix, IsGenProj and IsONSRun, with the regularised Gram matrix regGram and the quadratic form quadForm.

Formalization targets

Goal: Theorem 2 with $n\log T\ge4$

For every run of ONS, every horizon $T$ with $n\log T\ge 4$, and every $u\in\mathcal P$,

$$\sum_{t=1}^T\big(f_t(x_t)-f_t(u)\big)\le 5\Big(\frac1\alpha+GD\Big)\,n\log T.$$

The added condition $n\log T\ge4$ is what makes the printed constant correct (see Formalization scope).

Milestones

1. Lemma 3 (p. 177): for $0<\beta\le\frac12\min\{1/(4GD),\alpha\}$ and $x,y\in\mathcal P$,

$$f(x)\ge f(y)+\nabla f(y)^\top(x-y)+\tfrac\beta2\big(\nabla f(y)^\top(x-y)\big)^2 .$$

2. Lemma 8 (p. 188): for convex $\mathcal P$, $A\succeq0$, $z=\Pi^A_{\mathcal P}(y)$ and $a\in\mathcal P$: $(y-a)^\top A(y-a)\ge(z-a)^\top A(z-a)$.
3. The display on p. 178: for every run of ONS and $u\in\mathcal P$,

$$\sum_{t=1}^T\big(f_t(x_t)-f_t(u)\big)\le\frac1{2\beta}\sum_{t=1}^T\nabla_t^\top A_t^{-1}\nabla_t+\frac1{2\beta}.$$

4. Lemma 12 (p. 191): for $A\succeq B\succ0$, $A^{-1}\bullet(A-B)\le\log(|A|/|B|)$.
5. Lemma 11 (p. 190): if $\|u_t\|\le r$, $\varepsilon>0$ and $V_t=\sum_{\tau\le t}u_\tau u_\tau^\top+\varepsilon I_n$, then $\sum_{t=1}^Tu_t^\top V_t^{-1}u_t\le n\log(r^2T/\varepsilon+1)$.

Significance

Theorem 2 shows that exp-concavity alone, without strong convexity, suffices for regret logarithmic in $T$, at a per-round cost of one rank-one matrix update and one generalized projection. Its consequences include logarithmic regret for universal portfolio selection with a polynomial-time algorithm, and, by online-to-batch conversion, fast rates for stochastic exp-concave optimization. Lemma 11 (the elliptical potential bound) is used well beyond this paper, in linear bandits and online regression.

The result has been proved on paper since 2007. The remaining work is its machine-checked proof: the potential argument, the log-determinant inequality and the generalized-projection inequality for positive semidefinite matrices. As far as is known, none of these results is formalized in Mathlib. Prove2Me holds a related elliptical potential lemma for linear bandits (BanditAlgorithm.elliptical_potential_lemma, with $V_{t-1}$ and a $\min(1,\cdot)$, a different statement) and the Euclidean case $A=I$ of Lemma 8 (UnderstandingML.projection_lemma). The textbook version of ONS (OnlineConvexOpt.SecondOrder.online_newton_step_regret, with $\gamma=\frac12\min\{1/(GD),\alpha\}$ and bound $2(1/\alpha+GD)n\log T$) is an open private draft with different parameters.

Difficulty

The obvious route to logarithmic regret, the gradient-descent argument of Theorem 1 with step sizes $1/(Ht)$, needs a uniform lower bound $H>0$ on the Hessians. Exp-concave costs such as the log-loss have no such bound: their curvature vanishes in directions orthogonal to the gradients seen so far. The analysis therefore has to track curvature only along the observed gradient directions. This requires a matrix-valued potential $\sum_t\nabla_t^\top A_t^{-1}\nabla_t$ and a projection in the norm of $A_t$ rather than the Euclidean norm. The Euclidean projection inequality does not transfer to this norm, which changes from round to round. Bounding the potential requires determinant inequalities for positive definite matrices. The analytic facts are elementary, but their Lean statements involve the interaction of EuclideanSpace, Matrix.mulVec, Matrix.inv and Matrix.det.

Formalization scope

Points live in EuclideanSpace ℝ (Fin n), so all norms are Euclidean; matrices are Matrix (Fin n) (Fin n) ℝ acting on coordinate vectors. Rounds are 1-based: sums run over Finset.Icc 1 T and the index $0$ is unused. Cost functions are ambient functions $\mathbb R^n\to\mathbb R$, differentiable at the points of $\mathcal P$, with $\nabla f_t$ given by Mathlib's gradient. The paper's standing assumptions of convexity and twice differentiability are not needed and are omitted. $D$ enters only as an upper bound on distances in $\mathcal P$. The generalized projection is a predicate that every minimiser satisfies, and ONS is the predicate IsONSRun on the whole trajectory, so the goal covers every tie-break and every adaptive adversary.

Corrections and added hypotheses:

• Theorem 2 is false as printed at $T=1$. Take $n=1$, $\mathcal P=[-1,1]$, $f_1(x)=x^2$, $\alpha=\frac12$, $G=D=2$ and $x_1=1$: the regret is $1$ and the bound is $0$. The paper's proof gives $4(1/\alpha+GD)(n\log T+1)$ for $T\ge2$; the final sentence drops the additive $1/(2\beta)$ of the p. 178 display. The goal adds $n\log T\ge4$, under which the printed constant $5$ follows.
• $G,D,\alpha>0$ are assumed wherever $\beta$ or $\varepsilon$ appear: they are the non-degeneracy the formulas presuppose (in Lean, $1/0=0$).
• Lemma 3 adds $0<\beta$; the proof divides by $\beta$.
• Lemma 11 adds $\varepsilon>0$ and reads the printed $\sum_{\tau=1}^tu_tu_t^\top$ as $\sum_{\tau=1}^tu_\tau u_\tau^\top$.
• Lemma 12's product $\bullet$ is the entrywise inner product $\sum_{i,j}C_{ij}E_{ij}$, written out as a double sum.
• The printed "$f_t:\mathcal P\to\mathbb R^n$" is read as $f_t:\mathcal P\to\mathbb R$, and "$\Pi^{A_t}_{S_n}$" on p. 177 as $\Pi^{A_t}_{\mathcal P}$.

Regret is stated against every comparator $u\in\mathcal P$, never as a real infimum ⨅ over $\mathcal P$, which is junk-valued in Lean on unbounded or empty sets. The goal is a statement about runs of the paper's algorithm with the paper's $\beta$, $\varepsilon$ and $A_t$. A bound for an arbitrary sequence satisfying the p. 178 display would be a milestone, not Theorem 2. The hypotheses are jointly satisfiable: the closed unit ball with $f_t(x)=\|x\|^2/2$, $\alpha=1$, $G=1$, $D=2$ is a model.

A complete development needs: first-order conditions for concave functions on convex sets at boundary points; the optimality condition for minimising a convex quadratic over a convex set; spectral facts about symmetric positive definite matrices (square roots, eigenvalues, $\operatorname{tr}$ and $\det$); and the telescoping of log-determinants. Lemmas 8, 11 and 12 are reusable beyond this mission, in the sibling missions of this series (Follow the Approximate Leader) and in linear-bandit analyses. Proofs of any milestone are welcome, as are alternative proofs of Lemma 12 through concavity of $\log\det$.

Selected references

• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• T. M. Cover, Universal portfolios, Mathematical Finance 1 (1991), 1–29. https://doi.org/10.1111/j.1467-9965.1991.tb00002.x
• E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization 2 (2016); 2nd ed. arXiv:1909.05207. https://arxiv.org/abs/1909.05207