Robust Optimization

Motivation

A robust counterpart draws a hard line. Inside the uncertainty set the constraint must hold; outside it, nothing is promised — and in a real problem the perturbation does sometimes land outside. Chapter 3 answered this for linear problems with the globalized robust counterpart: keep the constraint exactly on the normal range $\mathcal{Z}$, and let it degrade at a controlled rate outside, proportionally to the distance from $\mathcal{Z}$. That mission published Proposition 3.2.1, which says the GRC of an uncertain linear inequality is equivalent to two ordinary robust counterparts.

Chapter 11 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (Princeton, 2009) does the same for conic constraints, and the move is not routine. The left hand side of a conic constraint is a vector, not a scalar, so "the constraint is violated by at most $\alpha \,\mathrm{dist}(\zeta, \mathcal{Z})$" has no direct meaning. What replaces it is the observation that a scalar inequality $a^Ty - b \le 0$ is the inclusion $a^Ty - b \in \mathbf{Q} \equiv \mathcal{R}_-$, and that the violation is the distance from the left hand side to $\mathbf{Q}$. In that form the notion lifts verbatim, and the whole chapter follows.

Setting

Definition 11.1.2. Consider an uncertain convex constraint

$$\Bigl[P^0 + \sum_{\ell=1}^L \zeta_\ell P^\ell\Bigr]y - \Bigl[p^0 + \sum_{\ell=1}^L \zeta_\ell p^\ell\Bigr] \ \in\ \mathbf{Q}, \tag{11.1.4}$$

with $\mathbf{Q} \subseteq \mathcal{R}^k$ nonempty, closed and convex. Let the perturbation space split as $\mathcal{R}^L = \mathcal{R}^{L_1}\times\cdots\times\mathcal{R}^{L_S}$, each factor carrying a normal range $\mathcal{Z}^s$, a closed convex cone $\mathcal{L}^s$ and a norm $\|\cdot\|_s$, and let $\|\cdot\|_{\mathbf{Q}}$ be a norm on $\mathcal{R}^k$. A candidate $y$ is robust feasible with global sensitivities $\alpha_s$ if

$$\mathrm{dist}\bigl(P(y,\zeta), \mathbf{Q}\bigr) \ \le\ \sum_{s=1}^S \alpha_s\, \mathrm{dist}(\zeta^s, \mathcal{Z}^s|\mathcal{L}^s) \qquad \forall\, \zeta \in \mathcal{Z} + \mathcal{L}, \tag{11.1.6}$$

where $\mathrm{dist}(u,\mathbf{Q}) = \min_{v\in\mathbf{Q}}\|u - v\|_{\mathbf{Q}}$ and $\mathrm{dist}(\zeta^s,\mathcal{Z}^s|\mathcal{L}^s) = \min\{\|\zeta^s - v\|_s : v \in \mathcal{Z}^s,\ \zeta^s - v \in \mathcal{L}^s\}$.

The object that makes the analysis work is the recessive cone of $\mathbf{Q}$ (Definition 11.3.1): for any $\bar x \in \mathbf{Q}$,

$$\mathrm{Rec}(\mathbf{Q}) = \{h : \bar x + th \in \mathbf{Q}\ \ \forall t \ge 0\},$$

which does not depend on $\bar x$ and is a nonempty closed convex cone.

Formalization targets

Goal — Proposition 11.3.3, the decomposition of the conic GRC

A candidate $y$ is feasible for the GRC (11.1.6) if and only if it satisfies the system

$$\text{(a)}\quad \Bigl[P^0 + \sum_\ell \zeta_\ell P^\ell\Bigr]y - \Bigl[p^0 + \sum_\ell \zeta_\ell p^\ell\Bigr] \in \mathbf{Q} \qquad \forall \zeta \in \mathcal{Z} = \mathcal{Z}^1\times \cdots\times\mathcal{Z}^S,$$ $$\text{(b}_s)\quad \mathrm{dist}\Bigl(\sum_{\ell} [P^\ell y - p^\ell](E_s\zeta^s)_\ell,\ \mathrm{Rec}(\mathbf{Q})\Bigr) \ \le\ \alpha_s \qquad \forall \zeta^s \in \mathcal{L}^s \text{ with } \|\zeta^s\|_s \le 1, \quad s = 1,\ldots,S .$$

Line (a) is the ordinary robust counterpart over the normal range. Each line (b$_s$) is a bounded semi-infinite constraint — the perturbation ranges over the unit ball of a cone, not over an unbounded set — measuring the distance to the recessive cone rather than to $\mathbf{Q}$ itself.

Supporting targets

$$\text{(Def 11.3.1)}\quad \mathrm{Rec}(\mathbf{Q}) \text{ is independent of the base point and is a nonempty closed convex cone},$$ $$\text{(Ex 11.3.2)}\quad \mathbf{Q} \text{ bounded} \Rightarrow \mathrm{Rec}(\mathbf{Q}) = \{0\}; \quad \mathbf{Q} \text{ a cone} \Rightarrow \mathrm{Rec}(\mathbf{Q}) = \mathbf{Q}; \quad \mathrm{Rec}\{u : Au - b \in \mathbf{K}\} = \{h : Ah \in \mathbf{K}\},$$ $$\text{(Prop 11.4.1)}\quad \Psi_\Xi(\mathcal{M}) = \Psi_{\Xi_*}(\mathcal{M}^*), \qquad \Psi(\mathcal{M}) = \max\{\mathrm{dist}_{\|\cdot\|_F}(\mathcal{M}e, \mathbf{K}^F) : e \in \mathbf{K}^E,\ \|e\|_E \le 1\} .$$

Significance

The goal is the chapter's structural result and it does exactly what Proposition 3.2.1 did one level down: it converts a single semi-infinite constraint over an unbounded perturbation set into a robust counterpart over the bounded normal range plus finitely many constraints over unit balls. That matters because every tractability result of Chapters 6 to 9 is about bounded uncertainty sets; without the decomposition none of them applies to a GRC.

The two halves of the decomposition are genuinely different objects. Line (a) is familiar. Lines (b$_s$) are not: they measure the distance from a linear image of a ball to the recessive cone, and that is the function

$$\Psi(\mathcal{M}) = \max\bigl\{\mathrm{dist}(\mathcal{M}e, \mathbf{K}^F) : e \in \mathbf{K}^E,\ \|e\|_E \le 1\bigr\}$$

of §11.4, which is almost a norm on linear maps — nonnegative, positively homogeneous, subadditive, but neither symmetric nor strictly positive. Proposition 11.4.1 says this function is self-dual in the precise sense that $\Psi$ of a map with respect to a setup equals $\Psi$ of the adjoint map with respect to the dual setup: dual norms, dual cones, source and destination exchanged. That single identity is what lets every bound on $\Psi$ be computed on whichever side of the duality is tractable, and it is the engine of §11.4's tractability results.

The recessive cone results are the vocabulary. The one that earns its place is $\mathrm{Rec}\{u : Au - b \in \mathbf{K}\} = \{h : Ah \in \mathbf{K}\}$: the conic sets of this book are all of that form, so it says the recessive cone of every constraint in sight is computed by deleting the constant term.

Difficulty

The goal is an equivalence and the two directions are asymmetric.

Forward — GRC implies the system — is where the recessive cone is discovered rather than used. Fix $\bar\zeta \in \mathcal{Z}$ and $\zeta^s$ in the unit ball of $\mathcal{L}^s$, and run $\zeta_i = \bar\zeta + i\,\zeta^s$ out along the cone. The GRC bounds the distance to $\mathbf{Q}$ by $\alpha_s i$, so there are $q_i \in \mathbf{Q}$ with $\|P(y,\bar\zeta) + i\Phi(y)E_s\zeta^s - q_i\|_{\mathbf{Q}} \le \alpha_s i$; the rescaled points $q_i/i$ stay bounded, and a limit point of them lies in $\mathrm{Rec}(\mathbf{Q})$ by the limit characterization of the recessive cone. This is a genuine compactness argument, and it is why the recessive cone — not $\mathbf{Q}$ — is what appears in lines (b$_s$).

Backward is a decomposition-and-assemble: split each $\zeta^s = \bar\zeta^s + \delta^s$ with $\bar\zeta^s \in \mathcal{Z}^s$, $\delta^s \in \mathcal{L}^s$ realizing the distance, get a point of $\mathbf{Q}$ from line (a) and a recession direction from each line (b$_s$), and add them — using that $\mathbf{Q} + \mathrm{Rec}(\mathbf{Q}) \subseteq \mathbf{Q}$.

Proposition 11.4.1 is a chain of polarity identities: the polar of $X + K$ is $X^o \cap (-K_*)$ for compact convex $X$ containing the origin, the polar of a norm ball of radius $\alpha$ is the dual-norm ball of radius $1/\alpha$, and bipolarity. Each step is standard and the composition is not.

Formalization scope

Built on the module published by the third mission of this series, which carries the linear-case globalized robust counterpart and the dual cone. New here: norms as functions with their defining properties, dual norms, the two distances, the recessive cone, the conic GRC, and the function $\Psi$.

Conventions committed to:

• Norms are functions carrying an explicit predicate, not typeclass instances. Chapter 11 quantifies over arbitrary norms $\|\cdot\|_{\mathbf{Q}}$ and $\|\cdot\|_s$ on fixed coordinate spaces, and a statement must be able to range over them; a typeclass instance would fix one norm per type. IsNormOn bundles definiteness, absolute homogeneity and the triangle inequality, and nonnegativity follows from them.
• The dual norm is a predicate, not a construction. $\|f\|^* = \sup\{f^Te : \|e\| \le 1\}$ is asserted as a least upper bound of the set of values, so no supremum is taken on faith.
• Distances are infima, not minima. The source writes $\min$, which is correct because the sets are closed; writing $\inf$ avoids carrying an attainment proof into every statement, and agrees with the minimum whenever the source's own hypotheses hold.
• The recessive cone is indexed by a base point. Definition 11.3.1 defines it at an arbitrary $\bar x \in \mathbf{Q}$ and then asserts independence of the choice; that assertion is one of the published items, so the definition cannot presuppose it.
• The perturbation is carried as a family of blocks, $\zeta = (\zeta^1,\ldots,\zeta^S)$ with $\zeta^s \in \mathcal{R}^{L_s}$, rather than as a single vector in $\mathcal{R}^L$ together with the embeddings $E_s$. This is the same data and removes the index bookkeeping of $E_s$ from every statement.
• $\Psi$ is a predicate on a real number, as for the dual norm and for the same reason.
• §11.2 and §11.5 are out of scope: the definition of a tight safe approximation of a GRC and the worked analysis of nonexpansive dynamical systems. The first is a definition the chapter uses only to phrase §11.4's programme, the second an application.

Selected references

• A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. Chapter 11, §§11.1, 11.3-11.4, pp. 281-294; Chapter 3 for the linear case. https://doi.org/10.1515/9781400831050
• A. Ben-Tal, S. Boyd and A. Nemirovski, Extending scope of robust optimization: comprehensive robust counterparts of uncertain problems, Mathematical Programming 107 (2006), 63-89. https://doi.org/10.1007/s10107-005-0679-z
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Least-squares fitting is a standard tool in estimation, identification and data analysis, and its data $A$, $b$ are rarely known exactly. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to choose $x$ to minimize the worst-case residual over a set of admissible data perturbations. Earlier missions of this series treat unstructured perturbations of $[A\ b]$ and perturbations affine in a parameter vector. §5 of the paper covers a more general model, taken from robust identification (Doyle et al.): the perturbed data depend on an uncertain matrix $\Delta$ through a linear-fractional transformation. This form covers rational dependence of the data on uncertain parameters, max-norm bounds on independent parameters, and data matrices with some columns known exactly (pp. 1046–1047).

In this generality, deciding whether the worst-case residual is finite is NP-complete, and computing it is NP-hard even when the dependence is affine (§5.3, Lemma 5.1). Theorem 5.2 gives the tractable replacement: a semidefinite program whose value bounds the worst-case residual from above, and equals it when the perturbation is unstructured. The main tool is a structured form of the S-procedure. Robust control uses the same tool, with the scalings $S$ and $G$ below, to bound the real structured singular value (Fan, Tits and Doyle, 1991).

Setting

Vectors carry the Euclidean norm $\|v\|$. For a matrix $X$, $\|X\|$ is its largest singular value (operator norm between Euclidean spaces). Let $\mathcal D$ be a linear subspace of $\mathbb R^{N\times N}$ (the perturbation structure), and fix $A \in \mathbb R^{n\times m}$, $b \in \mathbb R^n$, $L \in \mathbb R^{n\times N}$, $R_A \in \mathbb R^{N\times m}$, $R_b \in \mathbb R^N$, $D \in \mathbb R^{N\times N}$. For $\Delta \in \mathcal D$ with $\det(I - D\Delta) \ne 0$ the perturbed data are

$$A(\Delta) = A + L\Delta(I - D\Delta)^{-1}R_A, \qquad b(\Delta) = b + L\Delta(I - D\Delta)^{-1}R_b .$$

With the normalization $\rho = 1$ (the paper's, with no loss of generality), the worst-case residual of $x \in \mathbb R^m$ is

$$r_{\mathcal D}(A,b,x) = \max_{\Delta \in \mathcal D,\ \|\Delta\| \le 1} \|A(\Delta)x - b(\Delta)\|$$

if $\det(I - D\Delta) \ne 0$ for every such $\Delta$, and $+\infty$ otherwise (35). The commutant scalings are $\mathcal S = \{S = S^T : S\Delta = \Delta S\ \forall \Delta \in \mathcal D\}$ and $\mathcal G = \{G = -G^T : G\Delta = \Delta G\ \forall \Delta \in \mathcal D\}$ (37). The SDP constraint is

$$\mathcal F(\lambda,S,G,x) = \begin{bmatrix} \Theta & \begin{matrix} Ax - b \\ R_Ax - R_b\end{matrix} \\ \begin{matrix}(Ax-b)^T & (R_Ax - R_b)^T\end{matrix} & \lambda\end{bmatrix} \succ 0, \quad \Theta = \begin{bmatrix} \lambda I - LSL^T & -LSD^T + LG \\ -DSL^T + G^TL^T & S + DG - GD^T - DSD^T\end{bmatrix}. \qquad (38),(39)$$

Formalization targets

Goal: Theorem 5.2 (corrected)

For all $x$ and $\lambda$:

$$\text{(a)}\quad S \in \mathcal S,\ G \in \mathcal G,\ S \succ 0,\ G\Delta \text{ skew } \forall \Delta \in \mathcal D,\ \mathcal F(\lambda,S,G,x) \succ 0 \ \Longrightarrow\ \lambda > r_{\mathcal D}(A,b,x);$$ $$\text{(b)}\quad \mathcal D = \mathbb R^{N\times N},\ \lambda > r_{\mathcal D}(A,b,x) \ \Longrightarrow\ \exists s > 0:\ \mathcal F(\lambda, sI, 0, x) \succ 0 .$$

Part (a) says the value of the SDP $\inf\{\lambda : (\lambda, S, G) \text{ feasible}\}$ (40) is an upper bound on $r_{\mathcal D}$. Part (b) says this upper bound is exact for full perturbations, including the case $r_{\mathcal D} = \infty$, where (40) is infeasible.

Milestones

1. Lemma 2.2, both directions: the full-block S-procedure. $\det(I - T_4\Delta) \ne 0$ and $T(\Delta) \succeq 0$ for all $\|\Delta\| \le 1$ if and only if $\|T_4\| < 1$ and a one-scalar LMI (10) holds (the "only if" under $T_2 \ne 0$ or $T_3 = 0$).
2. Lemma 2.3: sufficiency of the scaled LMI for a structured $\mathcal D$, and its strict necessity for $\mathcal D = \mathbb R^{N\times N}$.
3. §5.4, p. 1047: $\lambda > r_{\mathcal D}(A,b,x)$ if and only if a linear-fractional matrix function of $\Delta$ is positive definite on the structured unit ball.
4. §5.4, (38)–(39): the certificate (a) in the paper's own words.

Significance

The worst-case residual under linear-fractional uncertainty cannot be computed efficiently unless P = NP. Theorem 5.2 gives an SDP-computable upper bound with an explicit certificate $(S, G)$. Since $x$ enters (38) linearly, the same constraint can also be optimized over $x$ (Theorem 5.3, not part of this mission). For $\mathcal D = \mathbb R^{N\times N}$ the bound is exact, which covers the model $[A(\Delta)\ b(\Delta)] = [A\ b] + L\Delta[R_A\ R_b]$ and, as a special case, the unstructured problem of §3.

The results are proved in the paper (the proof of Theorem 5.2 is only indicated, through Appendix C). No machine-checked version of these statements, of Lemma 2.2 or of the structured S-procedure with commutant scalings is known. The formalization also fixes the statements. As printed, Lemma 2.2's "only if", Lemma 2.3 and the upper bound of Theorem 5.2 are each false in a boundary or structural case (see Formalization scope). The corrected forms stated here are the ones the paper's proofs support.

Difficulty

Part (a) reduces to robust positivity of a linear-fractional matrix function, and the difficulty is the inverse $(I - D\Delta)^{-1}$. The certificate is one LMI in which $\Delta$ does not appear, while the conclusion is about a rational function of $\Delta$ over a whole structured ball. The certificate also has to guarantee that $I - D\Delta$ is invertible everywhere on that ball, and not only that the residual is small where it is defined. Evaluating $\mathcal F$ at a single point does not show this. Part (b) needs a lossless S-procedure in its strict form. The standard (non-strict) S-lemma gives only $\succeq$, and the gap between strict and non-strict inequalities is exactly where the printed statements fail. The degenerate case $T_2 = 0$ is not covered by the S-lemma's regularity condition and has to be handled separately.

Formalization scope

• Dimensions are Fin n, Fin m, Fin N; $\mathcal D$ is a Submodule ℝ (Matrix (Fin N) (Fin N) ℝ), with $\mathcal D = \mathbb R^{N\times N}$ as ⊤. The Euclidean norm is written out, because ‖·‖ on Fin n → ℝ is the sup norm. $\|\Delta\|$ is the operator norm of Matrix.toEuclideanLin Δ, the largest singular value.
• $\lambda > r_{\mathcal D}(A,b,x)$ is the predicate ResidualBelow: every $\Delta \in \mathcal D$ with $\|\Delta\| \le 1$ has $\det(I - D\Delta) \ne 0$ and residual $< \lambda$. It is false for every $\lambda$ when $r_{\mathcal D} = \infty$. No real-valued supremum is used, so the $\infty$ branch of (35) cannot turn into a default $0$. Matrix inverses are Mathlib's Matrix.inv, and every use carries the determinant condition.
• $\rho = 1$ throughout, as in the paper; general $\rho$ follows by scaling $\Delta$.
• Corrections of the printed statements. (i) (40) must require $S \succ 0$. Without it, $N = n = m = 1$, $D = 2$, $L = 1$, $A = b = R_A = R_b = 0$, $x = 0$, $S = -1$, $G = 0$ satisfy (38) for every $\lambda > 1/3$, while $r_{\mathcal D} = \infty$. (ii) $G$ must make $G\Delta$ skew-symmetric for every $\Delta \in \mathcal D$, which is the identity $p^TGq = 0$ used in the proof of Lemma 2.3. For $\mathcal D = \operatorname{span}\{I, J\}$, $J = \begin{bmatrix}0&1\\-1&0\end{bmatrix}$, the printed bound certifies $\lambda = 3/2$ for an instance with worst-case residual $2$. The added condition holds automatically when every element of $\mathcal D$ is symmetric (e.g. the diagonal structures (36)) and when $G = 0$ (e.g. $\mathcal D = \mathbb R^{N\times N}$). (iii) Lemma 2.2's "only if" is stated under $T_2 \ne 0$ or $T_3 = 0$. (iv) Lemma 2.3's necessity is stated in strict form, and its sufficiency concludes $T(\Delta) \succ 0$.
• Not stated: "If $\Theta > 0$ at the optimum, the upper bound is also exact". The infimum over the strict LMI (38) is not attained, and the paper does not say which limit is meant. Theorem 5.3, Lemma 2.4 and Lemma 5.1 are also not stated.
• Trivializing encodings ruled out: the goal is not a statement about the value of an infimum (which a junk value could satisfy), and the added hypotheses are satisfiable (for instance $S = sI$, $G = 0$ for full $\mathcal D$, which part (b) produces).
• Infrastructure needed: the Schur complement for block matrices (in Mathlib), a lossless S-lemma for two homogeneous quadratic forms in strict and non-strict form (the platform has ConvexOptimization.s_procedure, in a different sign convention), square roots of positive definite matrices that commute with $\mathcal D$, and compactness of the structured unit ball. The S-procedure lemmas are reusable in robust control and trust-region analysis. Proofs of the milestones in any order are welcome.

Selected references

• L. El Ghaoui and H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• S. Boyd, L. El Ghaoui, E. Feron and V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
• M. K. H. Fan, A. L. Tits and J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36(1):25–38, 1991. https://doi.org/10.1109/9.62265
• I. Pólik and T. Terlaky, A survey of the S-lemma, SIAM Review 49(3):371–418, 2007. https://doi.org/10.1137/S003614450444614X

Motivation

Many statistical procedures minimize an average observed loss. This treats two candidates with the same average as equally attractive even when one has much more variable losses across the sample. Adding a multiple of the empirical standard deviation can distinguish them, but the resulting objective need not be convex even when each individual loss is convex. Duchi and Namkoong study a distributionally robust alternative: they maximize expected loss over a small neighborhood of the empirical distribution, then minimize that worst-case value. Their paper identifies when this convex robust value agrees exactly with the mean-plus-standard-deviation expression and how far apart the two can be otherwise. The finite-sample statement is Theorem 1 of the pinned preprint.

The relation matters to someone choosing a loss function for stochastic optimization. The variance expression has a direct statistical interpretation, while the robust expression preserves convexity in a decision parameter when the loss is convex. Theorem 1 makes the relationship quantitative for a single bounded random variable, before the paper turns to uniform guarantees over whole classes of losses. This mission isolates that first step and its finite optimization model.

Setting

Take observed real values $z_1,\ldots,z_n$, with $n\ge1$. Their empirical mean and empirical variance are

$$\bar z=\frac1n\sum_{i=1}^n z_i,\qquad s_n^2=\frac1n\sum_{i=1}^n z_i^2-\bar z^2.$$

The variance uses $1/n$, not the unbiased-estimator factor $1/(n-1)$. A weight vector $p=(p_1,\ldots,p_n)$ is feasible when its entries are nonnegative, sum to one, and satisfy

$$\frac12\sum_{i=1}^n(np_i-1)^2\le\rho,\qquad \rho\ge0.$$

This is the paper's χ² neighborhood $\mathcal P_n(\rho)$ of the uniform empirical weights. Its robust sample expectation is

$$R_n(z,\rho)=\sup_{p\in\mathcal P_n(\rho)}\sum_{i=1}^n p_i z_i.$$

For a random variable $Z$ with law $P$ supported on $[M_0,M_1]$, write $M=M_1-M_0$ and $\sigma^2=\operatorname{Var}_P(Z)$. An independent sample $Z_1,\ldots,Z_n$ supplies the vector $z$. The paper describes $\mathcal P_n$ through a $\phi$-divergence from the empirical distribution, with $\phi(t)=\tfrac12(t-1)^2$; its finite maximization problem (8) is the weight-vector form used here. The preprint, pp. 2 and 5–7 fixes these conventions.

Formalization targets

Deterministic bound

For every sample in $[M_0,M_1]$, the robust value lies between the empirical mean plus a corrected variance penalty and the full penalty:

$$\left(\sqrt{\frac{2\rho s_n^2}{n}}-\frac{2M\rho}{n}\right)_+\le R_n(z,\rho)-\bar z\le\sqrt{\frac{2\rho s_n^2}{n}}.$$

This is inequality (10). The correction is explicit, so this target records more than an asymptotic approximation.

Exact expansion

When $\sigma^2>0$ and the sample size obeys

$$n\ge\max\left\{5,\frac{M^2}{\sigma^2}\max\{8\sigma,44,44\rho\}\right\},$$

the goal is the high-probability equality

$$\Pr\left\{R_n(Z_{1:n},\rho)\ne\bar Z+\sqrt{\frac{2\rho s_n^2}{n}}\right\}\le\exp\left(-\frac{n\sigma^2}{11M^2}\right).$$

This is Theorem 1's equality (11) with the missing $\rho$-dependent sample-size requirement supplied from the proof. The exact expansion is the mission goal; display (30), inequality (10), and Lemma A.2 form the milestone list, and the exact value under condition (9) is a further statement of the mission.

Significance

The deterministic result states how large the discrepancy between a convex robust risk and a variance penalty can be for any bounded sample. The equality says that, with the stated confidence, no discrepancy remains once the population variance and sample size make the penalty compatible with nonnegative probability weights. These are the numerical facts later sections need when they move from one loss variable to families of losses and minimizers. The claims and constants come from Theorem 1 and Section 2.1.

The paper develops arguments for these results, although its printed (11) needs the correction described below; the statements in this mission have no machine-checked proofs yet. The formalization work includes the finite χ² feasible set, its real supremum, exact handling of tied observations, empirical moments with the paper's normalization, and a product-law event for the probability estimate. The Samson concentration milestone is reusable for other bounded independent-coordinate models. Solvers can also contribute a different route to the corrected exact expansion; the goal concerns the statement, not one chosen argument.

Difficulty

Without the nonnegativity requirement on $p$, optimizing a linear function over the centered Euclidean ball gives the mean plus a standard-deviation term. The candidate weights can become negative when a sample coordinate is far below the mean, so that calculation alone cannot certify the robust value. Condition (9) records precisely when the candidate is feasible. The probability target then needs a quantitative guarantee that the sample variance is large enough often enough, with the stated exponential constant. A pointwise inequality for a fixed sample does not by itself yield that probability estimate. These are separate obligations in Section 2.1 and Appendix A.

Formalization scope

The sample is a function Fin n → ℝ; feasible weights have the same type. chiSqBall, robustSup, empMean, and empVar mirror equations (8) and the definitions on p. 6. Every theorem assumes $n>0$ and $\rho\ge0$, so the weight ball is nonempty and its real supremum is bounded. The high-probability theorem uses a probability measure $P$ on the reals, supported on $[M_0,M_1]$, and the independent product measure on Fin n → ℝ. Its conclusion bounds the measure of the event on which equality fails. The positive population variance hypothesis makes division by $\sigma^2$ and $M^2$ meaningful. The deterministic bounds include every sample in the interval and use $x_+=\max\{x,0\}$.

The paper prints the threshold without $44\rho$ in (11), but its Appendix A invokes the corresponding inequality, and the printed claim fails for sufficiently large $\rho$. The goal includes that term. The paper's route through Lemmas A.1 and A.4 contains misprinted lower-tail and moment claims, so those are not milestones. Lemma A.3's displayed (31b) is also omitted because its correction term has the wrong scaling; the corrected goal stands as a target to establish independently. These discrepancies are detailed in the local moderation notes and the pinned source, pp. 7 and 32–35.

No hypothesis may force the bad event to be empty, and the robust value must optimize over all feasible weights, not a selected optimizer. The supporting definitions are intended for reuse in later missions on uniform variance expansions. Contributions to the finite optimization facts, the concentration statement, and the probability goal are welcome.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv preprint arXiv:1610.02581v3, 2017. Pinned preprint.

Motivation

Empirical risk minimization (ERM) chooses, from a class $\mathcal F$ of loss functions, the one with the smallest average loss on a sample $X_1,\dots,X_n$. Its standard guarantees bound the excess population risk by a term of order $1/\sqrt n$, whatever the variance of the losses. When good functions in $\mathcal F$ have small variance, a better trade-off is available in principle: minimize the empirical risk plus a standard-deviation penalty $\sqrt{2\rho\,\mathrm{Var}_{\widehat P_n}(f)/n}$. Maurer and Pontil (COLT 2009) showed that this sample variance penalization enjoys faster rates, but the penalized objective is non-convex even for convex losses, so it cannot be minimized efficiently in general.

Duchi and Namkoong (arXiv:1610.02581v3, 2017; NIPS 2017) replace the variance penalty by a distributionally robust objective: the worst-case average loss over all reweightings of the sample within a $\chi^2$-divergence ball of radius $\rho/n$. This objective is convex whenever the loss is convex, and it equals the empirical risk plus the standard-deviation penalty up to an error of order $1/n$. Theorem 3 of the paper turns this into a guarantee for the minimizer of the robust objective, using covering numbers of the class. This mission formalizes Theorem 3 and the lemmas its proof rests on.

Setting

Let $\mathcal X$ be a measurable space, $P$ a probability measure on it, and $X_1,\dots,X_n$ ($n\ge1$) an i.i.d. sample from $P$ with empirical distribution $\widehat P_n$. Let $\mathcal F$ be a nonempty class of measurable functions $f:\mathcal X\to[M_0,M_1]$, and set $M = M_1-M_0$. Write $\mathbb E[f]=\int f\,dP$, $\mathrm{Var}(f)$ for the variance of $f(X)$, and

$$\mathbb E_{\widehat P_n}[f] = \frac1n\sum_{i=1}^n f(X_i),\qquad \mathrm{Var}_{\widehat P_n}(f) = \frac1n\sum_{i=1}^n f(X_i)^2 - \big(\mathbb E_{\widehat P_n}[f]\big)^2 .$$

For $\rho\ge0$, the $\chi^2$ ball $\mathcal P_n$ is the set of weight vectors $p\in\mathbb R^n$ with $p_i\ge0$, $\sum_i p_i = 1$ and $\frac12\sum_i (np_i-1)^2\le\rho$: the distributions $P$ on the sample with $D_\phi(P\|\widehat P_n)\le\rho/n$ for $\phi(t)=\frac12(t-1)^2$. The robust risk of $f$ is

$$R_n(f) = \sup_{P:\,D_\phi(P\|\widehat P_n)\le \rho/n}\mathbb E_P[f(X)] = \max_{p\in\mathcal P_n}\sum_{i=1}^n p_i f(X_i),$$

and a robust minimizer is any $\widehat f\in\operatorname{argmin}_{f\in\mathcal F} R_n(f)$.

Complexity is measured by empirical $\ell_\infty$ covering numbers. For $V\subset\mathbb R^m$, $N(V,\epsilon,\|\cdot\|_\infty)$ is the least number of points $v_1,\dots,v_N\in V$ such that every $v\in V$ lies within sup-distance $\epsilon$ of some $v_i$. For $x\in\mathcal X^m$ let $\mathcal F(x)=\{(f(x_1),\dots,f(x_m)) : f\in\mathcal F\}$, and

$$N_\infty(\mathcal F,\epsilon,m) = \sup_{x\in\mathcal X^m} N\big(\mathcal F(x),\epsilon,\|\cdot\|_\infty\big)\in\mathbb N\cup\{\infty\}.$$

Formalization targets

Goal: the oracle inequality (16)

Let $n\ge 8M^2/t$, $t\ge\log 12$, $\epsilon>0$ and $\rho\ge 9t$. With probability at least $1-2(3N_\infty(\mathcal F,\epsilon,2n)+1)e^{-t}$, every robust minimizer $\widehat f$ satisfies

$$\mathbb E[\widehat f(X)] \le \inf_{f\in\mathcal F}\left\{\mathbb E[f] + 2\sqrt{\frac{2\rho}{n}\mathrm{Var}(f)}\right\} + \frac{19M\rho}{3n} + \left(2+4\sqrt{\frac{2t}{n}}\right)\epsilon .$$

The certificate (15)

Under the same hypotheses and with the same probability, simultaneously for all $f\in\mathcal F$,

$$\mathbb E[f(X)] \le R_n(f) + \frac{11}{3}\frac{M\rho}{n} + \left(2+4\sqrt{\frac{2t}{n}}\right)\epsilon .$$

Supporting results (milestones)

1. Theorem 1, inequality (10): for every vector $z\in[M_0,M_1]^n$, the robust mean minus the sample mean lies between $\big(\sqrt{2\rho s_n^2/n}-2M\rho/n\big)_+$ and $\sqrt{2\rho s_n^2/n}$.
2. Lemma C.1: a uniform empirical Bernstein bound over $\mathcal F$ with probability $1-6N_\infty(\mathcal F,\epsilon,2n)e^{-t}$.
3. Lemma A.1, first bound: $\mathbb P(s_n\ge\sqrt{\mathbb E s_n^2}+t)\le\exp(-nt^2/(2M^2))$.
4. Bernstein's inequality for one fixed $f$, as displayed in the proof (p. 38).
5. The certificate (15).

Significance

Inequality (15) says the robust risk is a uniform upper confidence bound on the population risk, with an $O(1/n)$ slack instead of the $O(1/\sqrt n)$ slack of the empirical risk. Inequality (16) says the robust minimizer competes with the best variance-penalized population risk in the class. When some $f\in\mathcal F$ has small risk and small variance, the excess risk of $\widehat f$ is of order $1/n$ up to the covering term, a rate ERM does not achieve in general (§3.3 of the paper gives an example). For a parametric class with $N_\infty(\mathcal F,\epsilon,2n)$ polynomial in $1/\epsilon$, choosing $\epsilon=M/n$ gives Corollaries 3.1 and 3.2 of the paper.

The results are proved in the paper; none of them has a machine-checked proof that we know of. The mission's output is a formal proof of Theorem 3 and its ingredients: a deterministic analysis of the $\chi^2$-constrained linear program (Theorem 1 (10)), a covering-number empirical Bernstein inequality (Lemma C.1, from Maurer and Pontil), concentration of the sample standard deviation (Lemma A.1), and the scalar Bernstein inequality in the form used. Each of these is reusable outside distributionally robust optimization.

Difficulty

The deterministic part, (10), is a short analysis of a quadratically constrained linear program. The main obstacle is Lemma C.1. A union bound over a cover of $\mathcal F$ fails directly: the cover depends on the sample, and a population-level cover of $\mathcal F$ need not be finite. The standard route goes through a ghost sample of size $n$ (hence covering at $2n$ points), a symmetrization that must preserve the sample variance rather than only the mean, and a concentration bound for the sample variance itself. Lemma A.1 needs concentration of $s_n$, a non-linear and non-smooth function of the sample, at the sub-Gaussian rate $M/\sqrt n$. Finally, the oracle inequality (16) holds for an infimum over the whole class, while the concentration step for the comparison function is only proved for one fixed $f$ at a time.

Formalization scope

The sample is the coordinate process of the product measure $P^{\otimes n}$ on $\mathcal X^n$ (Measure.pi). Each probability statement bounds the probability of the bad event, the set of samples where the inequality fails for some $f$ (or some minimizer). This set need not be measurable, and its measure is then the outer measure, as is standard in empirical-process theory. Probability bounds are computed in $[0,\infty]$, and the covering number is valued in $\mathbb N\cup\{\infty\}$, so an infinite covering number makes the bound trivial rather than collapsing to zero. Covering numbers are internal (centres in $\mathcal F(x)$) and use closed sup-norm balls, as on p. 9; this is Mathlib's Metric.coveringNumber. The empirical variance is normalized by $1/n$. The $\chi^2$ ball is encoded as weight vectors on the sample points; with tied sample values this gives the same supremum as the paper's distributions on the sample. Statement (16) is formalized for every minimizer of the robust risk, and the event is empty if no minimizer exists. The infimum ranges over the nonempty class $\mathcal F$, on which every term is at least $M_0$. Population moments are those of bounded measurable functions, hence finite.

Deviations from the printed text:

• Lemma A.1 is stated only for its first (upper-tail) bound. The paper derives the second bound from Lemma A.4, which is false as printed; the second bound is not stated. $M>0$ is assumed because $M^2$ is a denominator.
• Lemma C.1 is the paper's restatement of Maurer and Pontil's Theorem 6, with a general radius $\epsilon$. It is formalized as printed, with the implicit assumption $\epsilon>0$ made explicit.
• $n\ge1$ is assumed throughout. The hypothesis $n\ge 8M^2/t$ is kept as printed.

A trivializing formalization is ruled out: the bound is not taken over all functions, a probability bound is not formed from the real part of an infinite covering number, and the minimizer is not a hypothesis that can fail to exist for the given sample.

Needed infrastructure: product-measure concentration (Bernstein, and a bounded-difference or convex-Lipschitz inequality for $s_n$), symmetrization with a ghost sample, and finite union bounds over a cover. Contributions are welcome on any milestone, in particular a general covering-number empirical Bernstein inequality, which is reusable on its own.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017 (NIPS 2017; JMLR 20, 2019). https://arxiv.org/abs/1610.02581
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT 2009. https://arxiv.org/abs/0907.3740
• 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. W. van der Vaart and J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996. https://doi.org/10.1007/978-1-4757-2545-2

Why variance-regularized risk bounds

In statistical learning, one picks a function $f$ from a class $\mathcal F$ to make the population risk $\mathbb E[f]$ small, with access only to an i.i.d. sample $x_1,\dots,x_n$ from an unknown distribution $P$. Empirical risk minimization replaces $\mathbb E[f]$ by the empirical mean $\mathbb E_{\widehat P_n}[f]$, and its classical guarantees decay like $1/\sqrt n$ regardless of how concentrated $f$ is. Bernstein-type inequalities show that the deviation of $\mathbb E_{\widehat P_n}[f]$ from $\mathbb E[f]$ scales with the standard deviation of $f$, so a procedure that minimizes "empirical risk plus a standard-deviation penalty" can, in principle, achieve faster rates when the variance at the optimum is small (Maurer and Pontil, 2009). The penalized objective is non-convex even when every $f$ is convex in its parameters, which makes it hard to optimize.

J. C. Duchi and H. Namkoong (arXiv:1610.02581v3, 2017) replace the penalty by a distributionally robust objective: the worst-case risk over all reweightings of the sample within a $\chi^2$-divergence ball. This objective is convex whenever the losses are, and (Theorem 1 of the paper) it equals the empirical mean plus a standard-deviation penalty up to an error of order $1/n$. This mission formalizes the paper's guarantee for the minimizer of that robust objective in terms of localized Rademacher complexities (Section 3.2, Theorem 4), the sharpest of the paper's three generalization analyses. It is the third of four missions on the paper.

Setting

Let $P$ be a probability measure on a measurable space $\mathcal X$ and $x_1,\dots,x_n$, $n\ge1$, an i.i.d. sample from $P$ with empirical distribution $\widehat P_n$. Let $M\ge1$ and let $\mathcal F$ be a collection of measurable functions $f:\mathcal X\to[0,M]$ (losses).

• The $\chi^2$ ball of radius $\rho\ge0$ is the set $\mathcal P_n$ of weight vectors $p\in\mathbb R^n$ with $p_i\ge0$, $\sum_ip_i=1$ and $\frac12\sum_i(np_i-1)^2\le\rho$; equivalently, the distributions $P$ on the sample with $D_\phi(P\|\widehat P_n)\le\rho/n$ for $\phi(t)=\frac12(t-1)^2$.
• The robust risk of $f$ is $\sup_{P:\,D_\phi(P\|\widehat P_n)\le\rho/n}\mathbb E_P[f]=\sup_{p\in\mathcal P_n}\sum_ip_if(x_i)$, and a robust minimizer $\widehat f$ minimizes it over $\mathcal F$.
• The empirical Rademacher complexity is $\mathfrak R_n(\mathcal F)=\mathbb E_\varepsilon\big[\sup_{f\in\mathcal F}\frac1n\sum_i\varepsilon_if(x_i)\big]$ with i.i.d. uniform signs $\varepsilon_i\in\{-1,1\}$, and $\mathbb E[\mathfrak R_n(\mathcal F)]$ averages it over the sample.
• A function $\psi:\mathbb R_+\to\mathbb R_+$ is sub-root if it is nonnegative, nondecreasing, and $r\mapsto\psi(r)/\sqrt r$ is nonincreasing on $r>0$.
• The localization inequality (20) asks that, for all $r\ge0$,

$$\psi_n(r)\ \ge\ \mathbb E\big[\mathfrak R_n(\{cf : f\in\mathcal F,\ c\in[0,1],\ \mathbb E[c^2f^2]\le r\})\big],$$

with $\psi_n$ sub-root, and $r_n^\star>0$ is a point with $r_n^\star\ge\psi_n(r_n^\star)$.

Formalization targets

Goal: Theorem 4, inequality (23), as its proof establishes it

Let $0<t<n$ and let $\rho$ satisfy (21): $\frac\rho n\ge8\big(\frac{45M}n\big(t+\log\lceil\log\frac nt\rceil\big)+18r_n^\star\big)$. With probability at least $1-4e^{-t}$, every robust minimizer $\widehat f$ satisfies

$$\mathbb E[\widehat f]\ \le\ \Big(1+2\sqrt{\tfrac{2\rho}n}\Big)\inf_{f\in\mathcal F}\Big(\mathbb E[f]+\sqrt{\tfrac{182\rho}{45n}\mathrm{Var}(f)}\Big)+\Big(14+6\sqrt{\tfrac{2\rho}n}\Big)\frac{M(3\rho+t)}n .$$

Milestones

In attack order: Bousquet's form of Talagrand's inequality (Lemma B.2); the elementary root bound (Lemma D.4); the contraction principle (Lemma D.5, a published theorem); the uniform Bernstein inequality with Rademacher complexity (Lemma D.1); its localized version in terms of $r_n^\star$ (Lemma D.2); localized second-moment bounds (Lemma D.3); the deterministic expansion (10) of Theorem 1,

$$\Big(\sqrt{\tfrac{2\rho}n s_n^2}-\tfrac{2M\rho}n\Big)_+\le\sup_{P}\mathbb E_P[Z]-\mathbb E_{\widehat P_n}[Z]\le\sqrt{\tfrac{2\rho}ns_n^2};$$

and the uniform bound (22): with probability at least $1-2e^{-t}$, for all $f\in\mathcal F$,

$$\mathbb E[f]\le\Big(1+2\sqrt{\tfrac{2\rho}n}\Big)\sup_{P:\,D_\phi(P\|\widehat P_n)\le\rho/n}\mathbb E_P[f]+\Big(13+4\sqrt{\tfrac{2\rho}n}\Big)\frac{M\rho}n .$$

Significance

The bound (23) says that the robust minimizer competes with the best trade-off between risk and standard deviation in the class, and that the complexity of the class enters only through the fixed point $r_n^\star$ of a localized complexity bound. For bounded VC classes $r_n^\star$ is of order $\frac{d\log(n/d)}n$ (Bartlett, Bousquet and Mendelson, 2005, Corollary 3.7), so when the optimal function has small variance the excess risk is of order $\rho/n$, faster than the $1/\sqrt n$ of uniform covering arguments; and localized complexities apply to classes, such as balls of reproducing kernel Hilbert spaces, whose covering numbers are too large for the covering-number analysis of the paper's Theorem 3 (mission II of this series).

The paper's result is proved, not open. No part of it, and none of the localized-complexity machinery of Bartlett, Bousquet and Mendelson, is formalized in Lean or Mathlib to our knowledge. The mission produces a checked version of the theorem with every constant explicit and, along the way, the localization lemmas D.1–D.3, which are reusable for any localized-complexity analysis. Reading the proof also exposed three arithmetic slips in the printed statements; the mission states what the proof establishes (see Formalization scope).

Difficulty

The obvious route applies a uniform concentration inequality to $\mathcal F$ and then a Bernstein bound to each $f$. Talagrand's inequality applied to the whole class gives a deviation governed by the largest variance in the class and by the global complexity $\mathbb E[\mathfrak R_n(\mathcal F)]$, which yields only $1/\sqrt n$ rates. Obtaining a deviation that scales with each function's own second moment requires peeling the class into shells of comparable second moment and a fixed-point argument on the sub-root bound, with a union bound whose cost appears as $\log\lceil\log\frac nt\rceil$. The two directions of the localized inequalities (population to sample, and sample to population for second moments) must then be combined with the deterministic expansion (10) while keeping the constants explicit. A further subtlety is the self-normalized rescaling $f\mapsto\sqrt{r/(\mathbb E[f^2]\vee r)}\,f$, which differs from the variance normalization of Bartlett et al. and is what makes the bound compatible with the robust objective.

Formalization scope

Lean conventions. The sample is the coordinate map of the product measure $P^n$ on Fin n → X. Distributions on the sample are weight vectors in the $\chi^2$ ball; the robust risk is the real supremum over that ball (attained, since the ball is nonempty and compact for $n\ge1$, $\rho\ge0$). Population means and variances are ∫ x, f x ∂P and ProbabilityTheory.variance f P for measurable bounded $f$; empirical means and variances are normalized by $1/n$. The empirical Rademacher complexity is the published UnderstandingML_Rademacher definition evaluated on $\{(f(x_1),\dots,f(x_n))\}$. Its expectation is a Bochner integral, and every hypothesis that bounds it also asserts that the integrand is integrable: otherwise the integral is $0$, (20) would hold for free, and the theorem would be false. Probability bounds are stated for the failure event under $P^n$ (an outer measure when the event is not measurable). The goal speaks about every minimizer of the robust risk, so it is not vacuous when the set of minimizers is empty. The condition $r_n^\star>0$ is part of the page's "root" (and the proof divides by $\sqrt{r_n^\star}$); with $r_n^\star=0$ allowed, $\psi(r)=\sqrt r$ would remove the complexity term from (21). The condition $t<n$ makes $\log\lceil\log\frac nt\rceil$ defined.

Corrections of printed statements, each recorded in the item's docstring and Formalization Note (the milestone texts stay verbatim):

• (22) is stated with probability $1-2e^{-t}$; the paper prints $1-e^{-t}$, and its proof (p. 41) concludes $1-2e^{-t}$.
• (23) is stated with probability $1-4e^{-t}$ (printed $1-3e^{-t}$; the proof adds two fixed-$f$ events to the two of (22)) and with $\frac{182\rho}{45n}$ (printed $\frac{91\rho}{45n}$; the proof's step $\sqrt\rho+\sqrt t\le\sqrt{91\rho/45}$ multiplies $\sqrt{2\mathrm{Var}(f)/n}$).
• Lemma D.3 is stated with the additive term $72M^2(1+\eta)r_n^\star+(4(1+\eta)+\frac{14}3)\frac{M^2t}n$ and, in the reversed direction, the coefficient $1+\frac1{1+\eta}$, as its proof yields (printed: $\frac{Mt}n(4+\frac73M)$ and $1+\frac\eta{1+\eta}$), under Theorem 4's standing hypothesis $M\ge1$.
• Lemma D.5 is linked to the published contraction lemma UnderstandingML.contraction_lemma, which states it at a fixed sample for nonempty bounded classes and allows a different Lipschitz map per coordinate.

Contributions welcome: proofs of the milestones in any order; Lemma B.2 (Bousquet's inequality) is the deepest single ingredient and is reusable well beyond this mission, as are the peeling Lemma D.1 and the sub-root fixed-point Lemma D.2.

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
• O. Bousquet, A Bennett concentration inequality and its application to suprema of empirical processes, Comptes Rendus Mathématique 334(6), 2002. https://doi.org/10.1016/S1631-073X(02)02292-6
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT 2009. https://arxiv.org/abs/0907.3740
• M. Ledoux and M. Talagrand, Probability in Banach Spaces, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4

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