Machine Learning

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3 (p. 7)

For every $\epsilon$-approximate oracle,

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Explicit instantiations and corrections:

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

Three constructions of classes appear.

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

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

Formalization targets

Goal: Theorem 16 (p. 472)

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

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

A robust Markov decision process (robust MDP) evaluates a policy against the worst transition kernel and reward in an uncertainty set around a nominal model $(P_0, r_0)$. It is the standard model for planning when the dynamics are estimated from data (Iyengar 2005; Nilim and El Ghaoui 2005; Wiesemann, Kuhn and Rustem 2013). Its Bellman update contains an inner optimization over the uncertainty set at every state, which makes robust planning costly when the sets are not $(s,a)$-rectangular.

Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) show that, for $s$-rectangular ball uncertainty sets, this inner optimization can be replaced by an explicit penalty that depends both on the policy and on the value function. The resulting twice regularized (R²) MDPs have Bellman operators with no inner optimization over models. The first mission of this series formalizes the robust–regularized equivalence (Theorem 4.1 of the paper). This mission formalizes Section 5: the R² Bellman operators are monotone and contracting under a bound on the transition radius, and the greedy policy of the R² optimal value is optimal.

Setting

Let $\mathcal S$ and $\mathcal A$ be finite nonempty sets of states and actions, $\gamma\in(0,1)$ a discount factor, $P_0(s'\mid s,a)$ a transition kernel and $r_0(s,a)$ a reward. A policy $\pi\in\Delta_{\mathcal A}^{\mathcal S}$ assigns to each state a probability distribution $\pi_s$ on $\mathcal A$. For $v\in\mathbb R^{\mathcal S}$ write $q_s(a)=r_0(s,a)+\gamma\sum_{s'}P_0(s'\mid s,a)v(s')$ and

$$[T^\pi_{(P_0,r_0)}v](s)=\sum_a\pi_s(a)\,q_s(a).$$

All norms $\|\cdot\|$ below are $\ell_2$-norms, $\|a\|=\big(\sum_z a(z)^2\big)^{1/2}$; $\|\cdot\|_\infty$ is the sup norm.

Fix nonnegative radii $\alpha^r_s,\alpha^P_s$ for each state. The R² regularizer is $\Omega_{v,\mathrm R^2}(\pi_s)=\|\pi_s\|\,(\alpha^r_s+\alpha^P_s\gamma\|v\|)$, and the R² Bellman operators are

$$[T^{\pi,\mathrm R^2}v](s)=[T^\pi_{(P_0,r_0)}v](s)-\Omega_{v,\mathrm R^2}(\pi_s),\qquad [T^{*,\mathrm R^2}v](s)=\max_{\pi\in\Delta^{\mathcal S}_{\mathcal A}}[T^{\pi,\mathrm R^2}v](s).$$

A policy $\pi$ is greedy for $v$ when $T^{\pi,\mathrm R^2}v=T^{*,\mathrm R^2}v$.

Assumption 5.1 (bounded radius). For each $s$ there is $\epsilon_s>0$ with

$$\alpha^P_s\le\min\Big(\frac{1-\gamma-\epsilon_s}{\gamma\sqrt{|\mathcal S|}}\ ;\ \min_{u\in\mathbb R^{\mathcal A}_+,\|u\|=1,\ w\in\mathbb R^{\mathcal S}_+,\|w\|=1}\ \sum_{a,s'}u(a)P_0(s'\mid s,a)w(s')\Big),$$

and $\epsilon_*=\min_s\epsilon_s$. The R² value function $v^{\pi,\mathrm R^2}$ of a policy and the R² optimal value $v^{*,\mathrm R^2}$ are the fixed points of $T^{\pi,\mathrm R^2}$ and $T^{*,\mathrm R^2}$.

Formalization targets

Goal: Theorem 5.1 (p. 8)

Under Assumption 5.1, $T^{*,\mathrm R^2}$ and every $T^{\pi,\mathrm R^2}$ have unique fixed points; a greedy policy $\pi^{*,\mathrm R^2}$ for $v^{*,\mathrm R^2}$ exists, and every such policy satisfies

$$v^{\pi^{*,\mathrm R^2},\mathrm R^2}=v^{*,\mathrm R^2}\ \ge\ v^{\pi,\mathrm R^2}\qquad\text{for all }\pi\in\Delta^{\mathcal S}_{\mathcal A};$$

every optimal policy is greedy; and when $\alpha^r_s>0$ for all $s$ the greedy policy is unique, hence the unique optimal R² policy.

Milestones

1. Proposition 2.1 (p. 3): for $\Omega$ strongly convex on the simplex, $\Omega^*(y)=\max_{a\in\Delta}\langle a,y\rangle-\Omega(a)$ is differentiable with Lipschitz gradient equal to the unique maximizer, satisfies $\Omega^*(y+c\mathbb 1)=\Omega^*(y)+c$, and is non-decreasing.
2. Proposition 5.1 (i) (p. 8): $v_1\le v_2$ implies $T^{\pi,\mathrm R^2}v_1\le T^{\pi,\mathrm R^2}v_2$ and $T^{*,\mathrm R^2}v_1\le T^{*,\mathrm R^2}v_2$.
3. Proposition 5.1 (iii) (p. 8):

$$\|T^{\pi,\mathrm R^2}v_1-T^{\pi,\mathrm R^2}v_2\|_\infty\le(1-\epsilon_*)\|v_1-v_2\|_\infty,\qquad \|T^{*,\mathrm R^2}v_1-T^{*,\mathrm R^2}v_2\|_\infty\le(1-\epsilon_*)\|v_1-v_2\|_\infty.$$

Significance

Theorem 5.1 is the R² counterpart of the fundamental theorem of discounted dynamic programming: optimal R² values are achieved by stationary policies obtained by a single greedy step. Together with the contraction of Proposition 5.1 (iii) it justifies the R² modified policy iteration algorithm of the paper, whose greedy step is a projection onto the simplex rather than a robust max–min problem. Combined with the first mission of the series, which identifies the robust value of an $s$-rectangular ball-constrained MDP with the optimum of an R²-regularized program, it gives a route to robust planning at the cost of regularized planning.

The results are proved in the paper (App. C), partly by reference to Geist, Scherrer and Pietquin (2019) for the optimality operator. No machine-checked proof of any of them exists; this mission produces the first. Prop. 2.1 is a general fact of convex analysis (Danskin-type smoothness of a conjugate on the simplex) that is reusable for any regularized MDP or entropy-regularized game.

Difficulty

The R² evaluation operator is not affine: the value regularizer $-\alpha^P_s\gamma\|\pi_s\|\,\|v\|$ is concave in $v$ and decreases as $\|v\|$ grows. Monotonicity therefore does not follow from the positivity of $P_0$ as in the standard case; it requires the second bound of Assumption 5.1, which compares the $\ell_2$ variation of $\|v\|$ with the minimal nonnegative bilinear form of $P_0(\cdot\mid s,\cdot)$. Likewise the contraction modulus is not $\gamma$ but $1-\epsilon_*$, because the regularizer is $\sqrt{|\mathcal S|}$-Lipschitz between the $\ell_2$ and sup norms. The optimality step of the classical proof uses linearity of $T^\pi$ when comparing values of policies; here only monotonicity and contraction are available. Uniqueness of the greedy policy rests on strict concavity on the simplex, which holds only when the regularization weight is positive.

Formalization scope

States and actions are finite nonempty types; transitions are arrays P₀ : S → A → S → ℝ with the published predicate IsTransitionKernel; value functions are S → ℝ with the pointwise order. The $\ell_2$-norm is an explicit l2norm (Mathlib's norm on S → ℝ is the sup norm, used only for $\|\cdot\|_\infty$). $T^{*,\mathrm R^2}v(s)$ is the real supremum over the simplex $\Delta_{\mathcal A}$ (attained), and the inner minimum of Assumption 5.1 is the real infimum over nonnegative $\ell_2$-unit vectors; the witnesses $\epsilon_s$ are explicit. Greedy policies are a predicate, never a function, and the R² value functions are not defined by choice: the goal asserts their existence and uniqueness and speaks about the fixed points.

Disclosed deviations from the page. Assumption 5.1 is a hypothesis of Theorem 5.1 (its proof assumes it). The uniqueness clause of Theorem 5.1 additionally assumes $\alpha^r_s>0$ for all $s$: with one state, two actions, zero reward and zero radii every policy is greedy and optimal. Proposition 2.1 assumes $\Omega$ continuous on the simplex, without which the maximum need not be attained, and strong convexity is Mathlib's StrongConvexOn for some modulus (norm-independent in finite dimension). Proposition 5.1 (ii) is false as printed and is not drafted: with one state, one action, $P_0=1$, $r_0=0$, $\gamma=1/2$, $\alpha^r=0$, $\alpha^P=1/2$, $\epsilon=1/4$, one has $Tv=v/2-|v|/4$, and $v_1=-1$, $c=1$ give $T(v_1+c)=0>-1/4=Tv_1+\gamma c$. Remark 5.1, Algorithm 1 and the $\ell_p$ variant of App. C.1 are out of scope. The inner minimum of Assumption 5.1 is $0$ whenever some $P_0(s'\mid s,a)=0$, forcing $\alpha^P_s=0$; this is the assumption as printed.

A formalization in which $\|\cdot\|$ is the sup norm, the inner minimum ranges over all unit vectors (making the assumption unsatisfiable), or the value functions are postulated rather than shown to exist would be trivial or wrong; the drafted statements avoid all three. Contributions welcome: Prop. 2.1 as a general convex-analysis lemma, Banach fixed-point plumbing for S → ℝ with the sup norm, and the strict concavity of $p\mapsto\langle p,q\rangle-c\|p\|$ on the simplex.

Selected references

• E. Derman, M. Geist, S. Mannor, Twice regularized MDPs and the equivalence between robustness and regularization, NeurIPS 2021. arXiv:2110.06267v1
• M. Geist, B. Scherrer, O. Pietquin, A theory of regularized Markov decision processes, ICML 2019. arXiv:1901.11275
• A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. doi:10.1287/opre.1050.0216
• G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. doi:10.1287/moor.1040.0129
• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov decision processes, Mathematics of Operations Research 38(1), 2013. doi:10.1287/moor.1120.0566
• A. Mensch, M. Blondel, Differentiable dynamic programming for structured prediction and attention, ICML 2018. arXiv:1802.03676

Motivation

The stochastic multi-armed bandit is the basic model of sequential decisions under uncertainty with partial feedback: a forecaster repeatedly picks one of $K$ options and observes only the reward of the option it picked. It models clinical trials, ad placement, routing and dynamic pricing, and is the building block of many reinforcement-learning algorithms. The question is how much reward is lost, compared with always playing the best option, through having to learn which option is best.

Chapter 2 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2) answers this for upper confidence bound (UCB) strategies.

• Lai and Robbins (1985) introduced upper confidence bounds and proved that the number of pulls of a suboptimal arm must grow at least logarithmically, with an explicit constant, for consistent strategies (doi:10.1016/0196-8858(85)90002-8).
• Agrawal (1995) gave simpler sample-mean-based index policies with logarithmic regret (doi:10.2307/1427934).
• Auer, Cesa-Bianchi and Fischer (2002) gave the finite-time analysis of UCB1 for bounded rewards (doi:10.1023/A:1013689704352).
• Bubeck and Cesa-Bianchi (2012) present the $(\alpha,\psi)$-UCB family, whose analysis needs only a bound $\psi$ on the cumulant generating function of the rewards, and the Lai–Robbins lower bound for Bernoulli rewards.

Setting

There are $K\ge2$ arms. Arm $i$ has an unknown reward distribution $\nu_i$ with mean $\mu_i$. At each round $t=1,2,\dots$ the forecaster selects an arm $I_t$ based on the past and receives a reward drawn from $\nu_{I_t}$, independently of the past. Write $\mu^*=\max_i\mu_i$, $\Delta_i=\mu^*-\mu_i$ for the gap of arm $i$, and $T_i(n)$ for the number of times arm $i$ is selected in rounds $1,\dots,n$. The pseudo-regret is

$$\overline R_n=n\mu^*-\mathbb E\sum_{t=1}^n\mu_{I_t}=\sum_{i=1}^K\Delta_i\,\mathbb E\,T_i(n).$$

Moment condition (2.2). There is a convex $\psi:\mathbb R\to\mathbb R$ with $\ln\mathbb E\,e^{\lambda(X-\mathbb EX)}\le\psi(\lambda)$ and $\ln\mathbb E\,e^{\lambda(\mathbb EX-X)}\le\psi(\lambda)$ for all $\lambda\ge0$ and every arm's reward $X$. Its Legendre–Fenchel transform is $\psi^*(\varepsilon)=\sup_{\lambda\in\mathbb R}(\lambda\varepsilon-\psi(\lambda))$. For $[0,1]$ rewards one may take $\psi(\lambda)=\lambda^2/8$, for which $\psi^*(\varepsilon)=2\varepsilon^2$.

$(\alpha,\psi)$-UCB. With $\hat\mu_{i,s}$ the mean of the first $s$ rewards of arm $i$, at round $t$ select

$$I_t\in\operatorname*{argmax}_{i}\Big[\hat\mu_{i,T_i(t-1)}+(\psi^*)^{-1}\Big(\frac{\alpha\ln t}{T_i(t-1)}\Big)\Big].$$

Formalization targets

Goal: Theorem 2.1 (p. 11)

If the rewards satisfy (2.2), then $(\alpha,\psi)$-UCB with $\alpha>2$ satisfies, for every $n$,

$$\overline R_n\le\sum_{i:\Delta_i>0}\Delta_i\Big(\frac{\alpha\ln n}{\psi^*(\Delta_i/2)}+\frac{\alpha}{\alpha-2}\Big).$$

This is the bound the book's proof establishes. The printed statement has $\alpha/(\alpha-2)$ in place of $\Delta_i\,\alpha/(\alpha-2)$; see Formalization scope.

Milestones

• The decomposition $\overline R_n=\sum_i\Delta_i\,\mathbb E\,T_i(n)$ (p. 9).
• The Cramér–Chernoff bound (2.3): $\mathbb P(\mu_i-\hat\mu_{i,s}>\varepsilon)\le e^{-s\psi^*(\varepsilon)}$.
• The three-event lemma (2.5)–(2.7) from the proof of Theorem 2.1.
• The bounded-reward bound (2.4): $\overline R_n\le\sum_{i:\Delta_i>0}\big(\frac{2\alpha}{\Delta_i}\ln n+\frac{\alpha}{\alpha-2}\big)$.
• The comparison (2.8): $2(p-q)^2\le\mathrm{kl}(p,q)\le(p-q)^2/(q(1-q))$.
• Theorem 2.2: for every strategy with $\mathbb E\,T_i(n)=o(n^a)$ on all Bernoulli instances, $\liminf_n\overline R_n/\ln n\ge\sum_{i:\Delta_i>0}\Delta_i/\mathrm{kl}(\mu_i,\mu^*)$.

Significance

Theorem 2.1 says that the cost of learning grows only logarithmically in the horizon, with a constant set by how well each suboptimal arm can be told apart from the best one. Theorem 2.2 shows that, up to constants, this cannot be improved: for Bernoulli rewards any strategy that is good on every instance must pay $\ln n$ per suboptimal arm, with constant $\Delta_i/\mathrm{kl}(\mu_i,\mu^*)$. By (2.8) this constant is at least of order $1/\Delta_i$, matching (2.4). Together they are the template for the analysis of most optimistic algorithms: KL-UCB, linear and contextual UCB, and UCB-style reinforcement learning.

All results of the chapter are classical and proved on paper. This mission makes them machine-checked in a common model. That model has an explicit pseudo-regret, an explicit (generalized) inverse of $\psi^*$, an explicit initialization rule for the algorithm, and a randomized-strategy model for the lower bound. Later chapters of the series and later papers on optimistic algorithms can build on it.

Difficulty

The deterministic part of the upper bound is short, so the main difficulty is probabilistic. The sample mean $\hat\mu_{i,T_i(t-1)}$ is taken over a random number of samples that depends on the algorithm's past. A Chernoff bound for a fixed sample size does not apply to it directly. The proof needs a union bound over all possible sample sizes, together with the representation in which the $s$-th reward of each arm is a fixed random variable. Summing the resulting tail $t^{1-\alpha}$ over rounds is where $\alpha>2$ enters.

The lower bound needs a change-of-measure argument between two Bernoulli instances, applied to a forecaster that may be randomized and never knows the horizon. Expressing "the forecaster cannot distinguish the instances" requires the law of the whole interaction under two environments.

Formalization scope

Model. Arms are Fin K with $2\le K$, rounds are $1,2,\dots$, and the natural logarithm is used. Rewards are a stack: $X_{i,k}$ is the reward of the $(k+1)$-st pull of arm $i$, all mutually independent, identically distributed per arm. For every strategy this gives the same law of arms and rewards as the book's protocol. $\mu^*$, $\Delta_i$ and $T_i(t)$ are the published definitions of ImprovedLinBandits.UCBDelta.armModel. The pseudo-regret is (2.1), $n\mu^*-\mathbb E\sum_t\mu_{I_t}$, not the expected regret. The arms played are measurable random variables, so that every expectation is genuine.

$\psi^*$ and its inverse. $\psi^*$ takes values in the extended reals. $(\psi^*)^{-1}(y)=\inf\{\varepsilon\ge0:\psi^*(\varepsilon)\ge y\}$.

Algorithm. The index is undefined while $T_i(t-1)=0$. Unplayed arms are therefore played first, so each arm is played once in rounds $1,\dots,K$. Ties are broken arbitrarily.

Corrected misprint. The book prints Theorem 2.1 with constant term $\alpha/(\alpha-2)$. Its proof yields $\Delta_i\,\alpha/(\alpha-2)$ (bound on $\mathbb E\,T_i(n)$ times $\Delta_i$). The printed form is false for Gaussian rewards with large gaps. The goal states the proof's version. (2.4) is correct as printed because $\Delta_i\le1$.

Constants. No O(·) appears in the chapter's statements. The constants are the book's: $\alpha/(\alpha-2)$ in Theorem 2.1 and (2.4), and the factor $2$ in (2.4) and (2.8).

Conventions made explicit.

1. $\psi(\lambda)\ge\psi(0)$ for $\lambda\le0$. Condition (2.2) constrains $\psi$ only on $\lambda\ge0$, while $\psi^*$ takes the supremum over all of $\mathbb R$. Without this convention, (2.3) and Theorem 2.1 are false (for example $\psi(\lambda)=c\lambda+\lambda^2/8$ with large $c$).
2. $\psi^*$ is finite on $[0,\infty)$.
3. $\psi^*(\Delta_i/2)>0$ for suboptimal arms.
4. $\varepsilon\ge0$ in (2.3).
5. $q\in(0,1)$ in (2.8).

Conventions 1–3 hold for every $\psi$ the book uses.

Theorem 2.2. The forecaster is a measurable rule from the history and a fresh uniform seed to an arm. It does not depend on the horizon. Consistency is required on every Bernoulli instance, every suboptimal arm and every $a>0$. A term with $\mu^*=1$ ($\mathrm{kl}=+\infty$) is $0$, and the $\liminf$ is taken in the extended reals. The book proves only $K=2$.

Ruled out. The algorithm cannot see unplayed rewards (its index uses only the sample means of rewards already received). Non-measurable arm choices, which would make the expectations vanish in Lean, are excluded. Consistency cannot be assumed only on the instance of the conclusion.

Needed infrastructure. Cramér–Chernoff bounds for sums of i.i.d. variables, Hoeffding's lemma, the stack representation of bandit interactions, and the divergence decomposition for randomized strategies. All are reusable beyond this mission, and contributions of any of them are welcome.

Selected references

• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2, doi:10.1561/2200000024
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. doi:10.1016/0196-8858(85)90002-8
• R. Agrawal, Sample mean based index policies with O(log n) regret for the multi-armed bandit problem, Advances in Applied Probability 27, 1995. doi:10.2307/1427934
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47, 2002. doi:10.1023/A:1013689704352

Motivation

In stochastic optimization and statistical learning one chooses a parameter $\theta$ from a set $\Theta\subseteq\mathbb R^d$ to make the risk $R(\theta)=\mathbb E_P[\ell(\theta;X)]$ small, having seen only a sample $X_1,\dots,X_n$ from $P$. Generalization bounds suggest trading empirical risk against its standard deviation, but the variance-penalized objective is non-convex even for convex losses. Duchi and Namkoong (arXiv:1610.02581v3) replace it by the robustly regularized risk, the worst-case expected loss over a $\chi^2$-divergence ball around the empirical distribution. This objective is convex whenever $\ell$ is, and it agrees with the variance-penalized objective up to a small error.

When the risk has curvature near its minimizers, empirical risk minimization attains rates faster than $1/\sqrt n$ (Bartlett, Bousquet and Mendelson 2005; Shapiro, Dentcheva and Ruszczyński 2009). Section 4.1 of the paper asks whether minimizers of the robust risk, which carry an extra variance-dependent penalty of order $\sqrt{\rho/n}$, keep these fast rates. Its Theorem 5 answers yes, and does so for approximate minimizers, which is what iterative solvers return.

Setting

A loss $\ell:\mathbb R^d\times\mathcal X\to\mathbb R$ is fixed, with $\ell(\cdot;x)$ convex and $L$-Lipschitz on a convex set $\Theta$ for every $x$, and $\ell(\theta;\cdot)$ integrable. The risk is $R(\theta)=\mathbb E_P[\ell(\theta;X)]$.

For a radius $\rho\ge0$, the $\chi^2$ ball around the empirical distribution $\widehat P_n$ is the set of weight vectors

$$\mathcal P_n=\Big\{p\in\mathbb R^n_+:\tfrac12\|np-\mathbf 1\|_2^2\le\rho,\ \langle\mathbf 1,p\rangle=1\Big\},$$

and the robust risk is $R_n(\theta,\mathcal P_n)=\sup_{p\in\mathcal P_n}\sum_i p_i\,\ell(\theta;X_i)$.

For $\epsilon\ge0$ the $\epsilon$-suboptimal sets of the risk and of the robust risk are

$$S_\star^\epsilon=\{\theta\in\Theta:R(\theta)\le\inf_\Theta R+\epsilon\},\qquad\widehat S_\star^\epsilon=\{\theta\in\Theta:R_n(\theta,\mathcal P_n)\le\inf_\Theta R_n(\cdot,\mathcal P_n)+\epsilon\},$$

with $S_\star=S_\star^0$ the solution set and $\pi_{S_\star}$ the Euclidean projection onto it. The risk satisfies a growth condition of order $\gamma>1$ if, for some $\lambda>0$ and $r>0$,

$$R(\theta)-\inf_\Theta R\ \ge\ \lambda\,\mathrm{dist}(\theta,S_\star)^\gamma\quad\text{whenever }\mathrm{dist}(\theta,S_\star)\le r.\tag{26}$$

The complexity of the problem enters through the localized class $\{x\mapsto\ell(\theta;x)-\ell(\pi_{S_\star}(\theta);x):\theta\in A\}$ and its empirical Rademacher complexity $\mathfrak R_n(A)=\mathbb E_\varepsilon\big[\sup_{\theta\in A}\frac1n\sum_i\varepsilon_i(\ell(\theta;X_i)-\ell(\pi_{S_\star}(\theta);X_i))\big]$, with independent uniform signs $\varepsilon_i\in\{\pm1\}$.

Formalization targets

Goal: Theorem 5 (p. 19)

For $t>0$, $\rho\ge0$, and $0<\epsilon\le\frac12\lambda r^\gamma$ satisfying

$$\epsilon\ge\Big(2\frac{8^\gamma L^\gamma}{\lambda}\Big)^{\frac1{\gamma-1}}\Big(\frac\rho n\Big)^{\frac\gamma{2(\gamma-1)}}\quad\text{and}\quad\frac\epsilon2\ge2\,\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+L\Big(\frac{2\epsilon}\lambda\Big)^{\frac1\gamma}\sqrt{\frac{2t}n},\tag{27}$$ $$\mathbb P\big(\widehat S_\star^\epsilon\subset S_\star^{2\epsilon}\big)\ \ge\ 1-e^{-t}.$$

Milestones, in attack order

1. Localization (p. 44). Under (26), $S_\star^{2\epsilon}$ lies in $\{\theta\in\Theta:\mathrm{dist}(\theta,S_\star)\le(2\epsilon/\lambda)^{1/\gamma}\}$.
2. Theorem 1, upper half of (10) (p. 7). $\sup_{p\in\mathcal P_n}\langle p,z\rangle-\bar z\le\sqrt{2\rho s_n^2/n}$ for every $z\in\mathbb R^n$.
3. Claim E.1 (p. 44). If $\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon}$, the localized deviation $\Delta_n$ plus a variance term reaches $\epsilon$ somewhere on $S_\star^{2\epsilon}$.
4. Display (43) (p. 45). $\mathbb P(\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon})\le\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge\epsilon/2)$.
5. Concentration (p. 45). $\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge2\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+u)\le\exp(-\frac{nu^2}{2L^2}(\frac\lambda{2\epsilon})^{2/\gamma})$.

Significance

The theorem says that the variance penalty implicit in the robust objective does not cost the fast rates available under curvature. The $\rho$-dependent condition in (27) is of order $(\rho/n)^{\gamma/(2(\gamma-1))}$, which for quadratic growth ($\gamma=2$) is $\rho/n$, the same order as the localized complexity term in typical parametric problems. Corollary 4.1 of the paper derives explicit rates of order $\frac dn\log\frac nd+\frac tn+\frac\rho n$ from it for a unique minimizer. The result applies to $\epsilon$-approximate minimizers, so it covers the output of the stochastic-gradient methods used to solve the robust problem.

The result is proved in the paper (Appendix E). None of it is formalized: no statement about growth conditions, localized deviations of a robust objective, or fast rates for robust minimizers is on Prove2Me. A formal proof would check the printed constants, settle the boundary case $\epsilon=0$ (see below), and produce a localization lemma and a reduction from approximate robust minimizers to empirical processes that apply to other estimators.

Difficulty

The obvious argument fails at two points. First, a uniform deviation bound over all of $\Theta$ gives only the $1/\sqrt n$ rate: the speed-up comes from localizing to $S_\star^{2\epsilon}$, which requires transferring the growth condition, assumed only within distance $r$ of $S_\star$, to every $2\epsilon$-suboptimal point by convexity. Second, the robust risk is not an empirical average, so standard comparisons between empirical and population minimizers do not apply. Claim E.1 handles this by moving along the segment from a bad approximate minimizer to its projection, which needs the projection to be preserved along that segment (a normal-cone property of $\pi_{S_\star}$) and the risk to be continuous there. The robust–empirical gap is then controlled by the variance expansion of Theorem 1. The concentration step needs a bounded-differences inequality for a supremum over an uncountable class, together with symmetrization; neither is in Mathlib in this form.

Formalization scope

Parameters live in EuclideanSpace ℝ (Fin d), so norms, distances and projections are Euclidean. The sample is the coordinate process of the product measure $P^{\otimes n}$ on Fin n → X, $n\ge1$, and probabilities are measures of sample sets (the outer measure for a set that is not measurable). The $\chi^2$ ball is the weight-vector form (8). The suboptimal sets are written without infima ($R(\theta)\le R(\theta')+\epsilon$ for all $\theta'\in\Theta$). Each supremum "$\sup\ge c$" is written as "for every $\delta>0$ some $\theta$ reaches $c-\delta$", so no statement relies on the default value of a real supremum. The Rademacher complexity is the published UnderstandingML.rademacher, and its expectation over the sample is assumed integrable, so that it is the true expectation and not the default value $0$ of a Bochner integral. Lipschitz continuity is required on $\Theta$, as printed.

Corrections and presuppositions:

• $\epsilon>0$. The paper prints $0\le\epsilon$. At $\epsilon=0$, $\rho=0$, both conditions of (27) hold, yet for $\ell(\theta;x)=\frac12(\theta-x)^2$ on $\Theta=[-1,1]$ with $X$ uniform on $[-\frac12,\frac12]$ the robust minimizer is the sample mean, which is almost surely not in $S_\star=\{0\}$. The proof divides by $\epsilon$ (p. 45). The goal is stated for $\epsilon>0$.
• $S_\star$ nonempty and closed are assumed. The projection $\pi_{S_\star}$ presupposes them, and Appendix E calls $S_\star$ closed.
• Only the upper half of Theorem 1's (10) is stated; it needs no boundedness of the values.

The constant $\big(2\cdot8^\gamma L^\gamma/\lambda\big)^{1/(\gamma-1)}$ is the printed one; the proof uses a smaller one, which the printed condition implies. The hypotheses $\epsilon>0$, $\gamma>1$ and $\lambda>0$ make every power well defined. A formalization that assumed (26) vacuously, took $\epsilon=0$, or let the Rademacher term be a non-integrable Bochner integral would trivialize the goal; the statements rule these out.

Infrastructure: Euclidean projection onto closed convex sets and its normal-cone characterization (partly in Mathlib), convexity of integral functionals, McDiarmid's bounded-differences inequality, and symmetrization for suprema of empirical processes. The concentration tools and the localization lemma can be reused beyond this mission. Contributions toward McDiarmid's inequality and symmetrization are especially welcome.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
• P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
• S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT, 2009. https://arxiv.org/abs/0907.3740

Motivation

Many regression problems have far more unknown coefficients $p$ than observations $n$: gene expression studies with tens of samples and thousands of genes, imaging from few measurements, nonparametric curve recovery from a finite number of noisy samples. Estimation is hopeless in general, but becomes possible when the parameter is sparse, that is, has few nonzero entries. Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) proposed the Dantzig selector, an estimator computed by a single linear program, and showed that its squared error is within a logarithmic factor of what an oracle that knew which coefficients matter could achieve.

The estimator became one of the two standard $\ell_1$ methods for high-dimensional regression, alongside the Lasso; the comparison of the two by Bickel, Ritov and Tsybakov (arXiv:0801.1095, 2009) is built on it. This mission targets the paper's main result, the oracle inequality (Theorem 1.2). A companion mission covers the simpler $\ell_2$ bound for sparse parameters (Theorem 1.1).

Setting

Observations follow the linear model

$$y = X\beta + z,$$

where $X\in\mathbb R^{n\times p}$ is a deterministic design matrix with columns $X_1,\dots,X_p$, each of Euclidean norm $\|X_j\|_{\ell_2}=1$; $\beta\in\mathbb R^p$ is an unknown deterministic parameter; and $z=(z_1,\dots,z_n)$ has independent $N(0,\sigma^2)$ coordinates, $\sigma>0$. The vector $\beta$ is $S$-sparse if at most $S$ of its entries are nonzero.

Two constants of $X$ measure how close sparse sets of columns are to being orthonormal. The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ such that $(1-\delta)\|c\|_{\ell_2}^2\le\|Xc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2$ for every $c$ supported on at most $S$ indices. The restricted orthogonality constant $\theta_{S,S'}$ (defined for $S+S'\le p$) is the smallest $\theta\ge0$ with $|\langle Xc,Xc'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ whenever $c,c'$ are supported on disjoint sets of sizes at most $S$ and $S'$. Below $\delta:=\delta_{2S}$ and $\theta:=\theta_{S,2S}$.

For a tuning level $\lambda_p>0$, a Dantzig selector $\hat\beta$ is any solution of

$$\min_{\tilde\beta\in\mathbb R^p}\|\tilde\beta\|_{\ell_1}\quad\text{subject to}\quad\|X^*(y-X\tilde\beta)\|_{\ell_\infty}=\sup_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\sigma .$$

The ideal mean squared error is $\sum_{i=1}^p\min(\beta_i^2,\sigma^2)$: the risk of an oracle that keeps exactly the coordinates above the noise level.

Formalization targets

Goal: Theorem 1.2 (pp. 8–9)

Let $t>0$, $a\ge0$, and $\lambda_p:=(\sqrt{1+a}+t^{-1})\sqrt{2\log p}$. If $\beta$ is $S$-sparse and $\delta_{2S}+\theta_{S,2S}<1-t$, then with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ every Dantzig selector obeys

$$\|\hat\beta-\beta\|_{\ell_2}^2\le C_2^2\cdot\lambda_p^2\cdot\Big(\sigma^2+\sum_{i=1}^p\min(\beta_i^2,\sigma^2)\Big),$$

with the explicit constant (1.14)

$$C_2=\frac{2C_0}{1-\delta-\theta}+\frac{2\theta(1+\delta)}{(1-\delta-\theta)^2}+\frac{1+\delta}{1-\delta-\theta},\qquad C_0=2\sqrt2\Big(1+\frac{1-\delta^2}{1-\delta-\theta}\Big)+\Big(1+\frac1{\sqrt2}\Big)\frac{(1+\delta)^2}{1-\delta-\theta}.$$

Milestones

1. Lemma 3.2: $\|X\beta\|_{\ell_2}\le\sqrt{1+\delta}\,(\|\beta\|_{\ell_2}+(2S)^{-1/2}\|\beta\|_{\ell_1})$ for every $\beta$.
2. Lemma A.1 (dual sparse reconstruction, $\ell_2$ version): for $c$ supported on $|T|\le2S$, a vector $\beta$ on $T$ whose correlations $\langle X\beta,X_j\rangle$ equal $c_j$ on $T$ and are small off $T$ except on an exceptional set of size at most $S$, with bounds (6.1)–(6.6).
3. Corollary A.2 ($\ell_\infty$ version): the same without exceptional set, constants $1/(1-\delta-\theta)$.
4. Corollary A.3 (constrained thresholding): an $S$-sparse $\beta$ with $\|\beta\|_{\ell_2}<\lambda\sqrt S$ splits as $\beta'+\beta''$ with $\beta'$ small in $\ell_2$ and $\ell_1$ and $\|X^*X\beta''\|_{\ell_\infty}<\frac{1-\delta^2}{1-\delta-\theta}\lambda$.
5. Gaussian tail bound (Section 3, p. 15): $P(\sup_j|\langle z,X_j\rangle|>u)\le2p\,\varphi(u)/u$ for standard Gaussian noise.
6. Lemma 3.1: the $\ell_2$ mass of $h$ on $T_0$ and its top $S$ positions outside $T_0$ is controlled by $\|X^T_{T_{01}}Xh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$.

Significance

The result. Theorem 1.2 says that a single linear program, which knows neither the support of $\beta$ nor which coefficients exceed the noise, matches the oracle risk $\sum_i\min(\beta_i^2,\sigma^2)$ up to a factor $O(\log p)$, uniformly over $S$-sparse parameters and with explicit, nonasymptotic constants. For coefficients well below the noise level it is far sharper than the $\sigma^2 S\log p$ bound of Theorem 1.1. It is the template for later oracle inequalities for $\ell_1$-penalized estimators under restricted isometry or restricted eigenvalue conditions.

Formalizing it. The theorem is proved in the paper, but parts of the argument are only sketched: Corollary A.2 refers to the 2005 Decoding by Linear Programming paper for its convergence argument, and Corollary A.3's $\ell_1$ bound is printed with a constant its own proof does not deliver. A machine-checked proof settles these steps. The restricted isometry and orthogonality constants used here are already published on the platform from the decoding series; the appendix lemmas on dual vectors are reusable for any compressed-sensing result in that framework. No formalization of the Dantzig selector's oracle inequality is known to us.

Difficulty

The natural proof compares $\hat\beta$ with the hard-thresholded parameter $\beta^{(1)}$ that keeps only the large coefficients: if $\beta^{(1)}$ were feasible for the Dantzig constraint, the analysis of Theorem 1.1 would apply directly. It is not feasible in general, because the small coefficients $\beta^{(2)}$, though individually below the noise level, can add up to a large correlation $X^*X\beta^{(2)}$. The central difficulty is to split $\beta^{(2)}$ into a part with controlled $\ell_1$ and $\ell_2$ norm and a part invisible to the constraint; this requires constructing dual vectors with prescribed correlations (Lemma A.1, Corollary A.2), via an iterative, geometrically convergent correction. The probabilistic part is a Gaussian tail estimate plus a union bound, and the bookkeeping of constants must be carried through exactly.

Formalization scope

Vectors are functions Fin p → ℝ, the design is Matrix (Fin n) (Fin p) ℝ, and the noise is a family z : Fin n → Ω → ℝ of mutually independent random variables (iIndepFun) each with law gaussianReal 0 σ². $\delta_{2S}$ and $\theta_{S,2S}$ are the published CandesTao.Decoding.restrictedIsometryConst X (2*S) and restrictedOrthogonalityConst X S (2*S) (infima, absolute value in the orthogonality condition). Domain: $S\ge1$ and $3S\le p$ (the paper defines $\theta_{S,S'}$ for $S+S'\le p$), which forces $p\ge3$ and $\log p>0$. A Dantzig selector is any $\ell_1$ minimizer over the feasible set; the $\ell_\infty$ constraint is a bound on every coordinate.

The goal bounds from above the (outer) probability of the bad event "no Dantzig selector exists, or some Dantzig selector violates (1.13)". Because the event includes non-existence, a definition no vector satisfies cannot make the theorem vacuous; and the constant $C_2$ is the printed (1.14), evaluated at $\delta_{2S}$, $\theta_{S,2S}$ of $X$, not a free constant chosen after the fact.

Corrected constant: Corollary A.3 is stated with $\|\beta'\|_{\ell_1}\le2\frac{1+\delta}{1-\delta-\theta}\|\beta\|_{\ell_2}^2/\lambda$, the bound its proof gives once Corollary A.2 is applied at an integer sparsity level; the printed statement omits the factor $2$. Corollary A.2 carries Lemma A.1's standing hypothesis $\delta+\theta<1$. The deterministic lemmas (3.1, 3.2, A.1–A.3) assume nothing about column norms, since their statements do not need it.

Useful infrastructure: monotonicity of $\delta_S$ and $\theta_{S,S'}$ in their indices (the proof applies the lemmas at a smaller sparsity level), the Gaussian tail bound $1-\Phi(u)<\varphi(u)/u$, existence of minimizers of the Dantzig linear program, and a sorting/blocking toolkit for "the $S$ largest positions". Proofs of individual milestones are welcome independently.

Selected references

• E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6):2313–2351, 2007. arXiv:math/0506081v3, doi:10.1214/009053606000001523
• E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12):4203–4215, 2005. arXiv:math/0502327, doi:10.1109/TIT.2005.858979
• P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4):1705–1732, 2009. arXiv:0801.1095, doi:10.1214/08-AOS620
• D. Donoho and I. Johnstone, Ideal spatial adaptation by wavelet shrinkage, Biometrika 81(3):425–455, 1994. doi:10.1093/biomet/81.3.425