Motivation

Robust optimization replaces an uncertain constraint $f(\tilde{\mathbf u},\mathbf x)\le 0$ by the requirement that it hold for every $\mathbf u$ in an uncertainty set $\mathcal U\subseteq\mathbb R^d$. The resulting problems are tractable for many sets, but the choice of $\mathcal U$ decides whether the solution means anything probabilistically. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167:235–292, 2018) propose to build $\mathcal U$ from data so that, with high probability over the sample, every robust-feasible decision is also feasible with probability at least $1-\epsilon$ under the unknown distribution $\mathbb P^*$.

This mission covers §6 of that paper, the case where the data are samples of the marginals of $\mathbb P^*$, observed separately, with no assumption that the marginals are independent. This is the situation of asynchronous measurements or records with many missing entries: the joint law cannot be learned, yet a valid uncertainty set can still be built. The set is a box whose sides are order statistics, and its guarantee rests on an elementary binomial test (David and Nagaraja, Order Statistics, §7.1) and a Value-at-Risk bound of Embrechts, Höing and Juri (Finance Stoch. 7, 2003).

Setting

Let $\mathbb P^*$ be a probability measure on $\mathbb R^d$ whose support lies in a known box $[\hat{\mathbf u}^{(0)},\hat{\mathbf u}^{(N+1)}]=\{\mathbf u:\hat u^{(0)}_i\le u_i\le\hat u^{(N+1)}_i\}$. Fix a violation level $0<\epsilon<1$ and a significance level $0<\alpha<1$.

The Value at Risk of $\tilde{\mathbf u}^T\mathbf v$ under a probability measure $\mathbb P$ is

$$\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^T\mathbf v\le t)\ge1-\epsilon\},$$

and the support function of a set $\mathcal U$ is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^T\mathbf u$. A set $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P^*$ if for every $f(\mathbf u,\mathbf x)$ concave in $\mathbf u$ and every $\mathbf x^*$, $f(\mathbf u,\mathbf x^*)\le0$ for all $\mathbf u\in\mathcal U$ implies $\mathbb P^*(f(\tilde{\mathbf u},\mathbf x^*)\le0)\ge1-\epsilon$.

From a sample $\hat{\mathbf u}^1,\dots,\hat{\mathbf u}^N$ let $\hat u^{(j)}_i$, $1\le j\le N$, be the $j$-th order statistic (the $j$-th smallest value) of coordinate $i$, and let $\hat u^{(0)}_i,\hat u^{(N+1)}_i$ be the box ends. The index $s$ is

$$s=\min\Big\{k\in\mathbb N:\sum_{j=k}^N\binom Nj(\epsilon/d)^{N-j}(1-\epsilon/d)^j\le\frac{\alpha}{2d}\Big\},\qquad s=N+1\text{ if the set is empty}, \tag{26}$$

and the uncertainty set is the box

$$\mathcal U^M_\epsilon=\{\mathbf u\in\mathbb R^d:\hat u^{(N-s+1)}_i\le u_i\le\hat u^{(s)}_i,\ i=1,\dots,d\}. \tag{28}$$

The confidence region $\mathcal P^M$ is the set of probability measures on the box with $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(\mathbf e_i)\le\hat u^{(s)}_i$ and $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ for every $i$.

Formalization targets

Goal: Theorem 7

If $N-s+1<s$, then with probability at least $1-\alpha$ over the sample ($N$ samples of each marginal of $\mathbb P^*$, each marginal's samples i.i.d., arbitrary dependence across marginals),

$$\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)\qquad\text{for all }\mathbf v\in\mathbb R^d,$$

and, for every sample, $\mathcal U^M_\epsilon$ is nonempty, convex and compact with

$$\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)=\sum_{i=1}^d\max\big(v_i\hat u^{(N-s+1)}_i,\,v_i\hat u^{(s)}_i\big). \tag{29}$$

Milestones

1. Positive homogeneity: $\mathrm{VaR}^{\mathbb P}_\delta(c\mathbf w)=c\,\mathrm{VaR}^{\mathbb P}_\delta(\mathbf w)$ for $c>0$ (p. 10).
2. Each one-sided order-statistic test is valid at level $\alpha/(2d)$: $\mathbb P^*_{\mathcal S}(\hat u^{(s)}_i<\mathrm{VaR}^{\mathbb P^*}_{\epsilon/d}(\mathbf e_i))\le\alpha/(2d)$, and the mirror bound for $-\mathbf e_i$ with $\hat u^{(N-s+1)}_i$ (pp. 20–21).
3. Union bound: $\mathbb P^*_{\mathcal S}(\mathbb P^*\in\mathcal P^M)\ge1-\alpha$ (p. 21).
4. The weak Embrechts bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_i\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(v_i\mathbf e_i)$ for every probability measure $\mathbb P$ (p. 21).
5. If $N-s+1<s$ then $\hat u^{(N-s+1)}_i\le\hat u^{(s)}_i$ (p. 21).
6. (EC.8): for $\mathbb P\in\mathcal P^M$, $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_{v_i>0}v_i\hat u^{(s)}_i+\sum_{v_i\le0}v_i\hat u^{(N-s+1)}_i$ (p. ec5).
7. (29) as a standalone statement (p. 21).

Significance

Theorem 7 gives an uncertainty set with a finite-sample guarantee from data that carry no information on the dependence between coordinates. The set is a box, so the robust counterpart of a linear constraint is again linear, and Remark 12 of the paper notes that separation over $\{(\mathbf v,t):\delta^*(\mathbf v\mid\mathcal U^M)\le t\}$ is in closed form. Unlike the other confidence regions of the paper (χ², G-test, Kolmogorov–Smirnov, bootstrap), whose coverage is asymptotic, tabulated or approximate, the test here is exact and distribution-free, so the probability statement itself is in scope.

The result is proved in the paper; to our knowledge none of it has a machine-checked proof. The mission produces a complete formal statement of Theorem 7 including the sampling probability, the binomial order-statistic test for a quantile, and the marginal Value-at-Risk bound, all of which are standard tools in nonparametric statistics and risk management that are absent from Mathlib.

Difficulty

The deterministic half, (EC.8) and (29), is short once the weak Embrechts bound is available. The work is in the probabilistic half, which the paper delegates to a textbook citation. Validity of the order-statistic test ties together facts that no library currently connects: the combinatorics of sorted tuples, the binomial law of the number of i.i.d. sample points below a threshold, the behaviour of a quantile at its left limit (the distribution function at the quantile can exceed $1-\epsilon/d$, so the obvious bound uses the wrong probability), and the comparison of binomial tails across success probabilities. The lower-tail test must be handled with the index $N-s+1$ and the quantile of $-\tilde u_i$, where a sign or off-by-one slip produces a false statement that still looks plausible. The boundary regime $s=N+1$, where $\mathcal U^M_\epsilon$ is the a priori box, is valid only because $\mathbb P^*$ lives in that box and needs separate treatment.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ with 0-based coordinates; vectors pair by ⬝ᵥ. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$ applied to $\mathbf u\mapsto\mathbf u^T\mathbf v$, and the support function is the published RobustMDP.Shared.supportFunction; both are real infima/suprema, genuine under $0<\epsilon<1$, a probability measure, and a nonempty bounded set (the goal proves the latter). The order statistics use Mathlib's Tuple.sort; the index $N-s+1$ is N + 1 - s in natural numbers, which is the paper's value since $1\le s\le N+1$.

The data are an array S : Fin N → Fin d → ℝ, S k i the $k$-th sample of marginal $i$, under any probability law Q such that, for each $i$, the samples S 0 i, …, S (N-1) i are i.i.d. from the $i$-th marginal of $\mathbb P^*$ (IsMarginalSampleLaw). The dependence between samples of different marginals is left arbitrary, as the paper's asynchronous setting requires; i.i.d. draws of whole vectors are one admissible law. Probabilities of possibly non-measurable events are outer measures. The level $\epsilon$ is fixed: by Remark 11 the family $\{\mathcal U^M_\epsilon\}$ need not work for all $\epsilon$ simultaneously.

The guarantee is stated in the criterion form of Theorem 1(a) of the paper: $\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)$ for all $\mathbf v$, together with nonemptiness, convexity and compactness of $\mathcal U^M_\epsilon$. Theorem 1 (mission I of this series) shows that for such sets this criterion is equivalent to implying a probabilistic guarantee. The coverage of the test is proved, not assumed: there is no hypothesis that $\mathbb P^*\in\mathcal P^M$. A formalization in which the support function is evaluated on an empty or unbounded set, where the library value is 0, would make the criterion trivial; the nonemptiness and compactness conjunct of the goal rules it out.

Standing assumptions: $d\ge1$, $0<\epsilon<1$, $0<\alpha<1$, $\hat{\mathbf u}^{(0)}\le\hat{\mathbf u}^{(N+1)}$, $\mathbb P^*$ a probability measure with $\mathbb P^*$-null complement of the box, and Theorem 7's hypothesis $N-s+1<s$. The page prints the second condition of $\mathcal P^M$ as "$\mathrm{VaR}^{\mathbb P_i}_{\epsilon/d}\ge\hat u^{(N-s+1)}_i$"; the formal region uses the lower-tail condition $\mathrm{VaR}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ that the hypothesis, its rejection rule and the proof use. (EC.8) is stated with "$\le$" for each $\mathbb P\in\mathcal P^M$; the page's middle equality is not claimed.

Reusable infrastructure welcome beyond this mission: order statistics of tuples and the binomial law of threshold counts for i.i.d. samples; monotonicity of binomial tails in the success probability; the left-limit property of quantiles; the Embrechts-type subadditivity bound for Value at Risk.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
• H. A. David, H. N. Nagaraja, Order Statistics, Wiley (cited by the paper as 1970; third edition 2003), §7.1, distribution-free confidence intervals for quantiles. https://doi.org/10.1002/0471722162
• P. Embrechts, A. Höing, A. Juri, Using copulae to bound the Value-at-Risk for functions of dependent risks, Finance and Stochastics 7:145–167, 2003. https://doi.org/10.1007/s007800200085

Motivation

A robust linear constraint $u^\top v \le t$ with $u$ ranging over an uncertainty set $\mathcal U\subseteq\mathbb R^d$ is tractable whenever the support function $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$ is. Robust optimization gains a probabilistic meaning when $\mathcal U$ is chosen so that every robustly feasible decision also satisfies the constraint with probability at least $1-\varepsilon$ under the true distribution $\mathbb P^*$ of the uncertain parameter $\tilde u$. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets from data: a statistical hypothesis test yields a confidence region $\mathcal P$ of distributions, and the uncertainty set is any convex set whose support function dominates the worst-case Value at Risk over $\mathcal P$.

Section 5.2 of the paper applies this schema to the forward and backward deviations of Chen, Sim and Sun (Oper. Res. 55, 2007), one-sided measures of spread that capture skewness. Chen, Sim and Sun assume the mean and deviations are known; the data-driven version replaces them by confidence intervals and must work out the worst case over those intervals. The result is the set $\mathcal U^{FB}_\varepsilon$ of Theorem 6, whose support function has a closed form.

Setting

The uncertain parameter $\tilde u$ takes values in $\mathbb R^d$ and $\mathbb P$ is its law. For $\varepsilon\in(0,1)$ and $v\in\mathbb R^d$, the Value at Risk is

$$\mathrm{VaR}^{\mathbb P}_\varepsilon(v)=\inf\{t:\mathbb P(\tilde u^\top v\le t)\ge1-\varepsilon\}.$$

For a probability measure $\mathbb P_i$ on $\mathbb R$ with mean $\mu_i$, the forward deviation and the backward deviation are

$$\sigma_f(\mathbb P_i)=\sup_{x>0}\sqrt{-\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{x\tilde u_i}]},\qquad\sigma_b(\mathbb P_i)=\sup_{x>0}\sqrt{\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{-x\tilde u_i}]}.$$

From a sample, a bootstrap produces thresholds $t_i$, $\bar\sigma_{fi}$, $\bar\sigma_{bi}$. With the sample mean $\hat\mu_i$ put $m_{bi}=\hat\mu_i-t_i$ and $m_{fi}=\hat\mu_i+t_i$. The confidence region $\mathcal P^{FB}$ consists of the distributions of vectors with independent components $\tilde u_i\sim\mathbb P_i$, each $\mathbb P_i$ having bounded support, mean in $[m_{bi},m_{fi}]$, $\sigma_f(\mathbb P_i)\le\bar\sigma_{fi}$ and $\sigma_b(\mathbb P_i)\le\bar\sigma_{bi}$.

The uncertainty set is

$$\mathcal U^{FB}_\varepsilon=\Big\{y_1+y_2-y_3:\ y_2,y_3\in\mathbb R^d_+,\ \sum_{i=1}^d\Big(\frac{y_{2i}^2}{2\bar\sigma_{fi}^2}+\frac{y_{3i}^2}{2\bar\sigma_{bi}^2}\Big)\le\log(1/\varepsilon),\ m_{bi}\le y_{1i}\le m_{fi}\Big\}.$$

Formalization targets

Goal: Theorem 6

For $m_b\le m_f$, $\bar\sigma_f,\bar\sigma_b>0$ and $\varepsilon\in(0,1)$, the set $\mathcal U^{FB}_\varepsilon$ is nonempty, convex and compact,

$$\delta^*(v\mid\mathcal U^{FB}_\varepsilon)=\sum_{i:v_i\ge0}m_{fi}v_i+\sum_{i:v_i<0}m_{bi}v_i+\sqrt{2\log(1/\varepsilon)\Big(\sum_{i:v_i\ge0}\bar\sigma_{fi}^2v_i^2+\sum_{i:v_i<0}\bar\sigma_{bi}^2v_i^2\Big)}\qquad(24)$$

for every $v$, and $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)$ is at most the right-hand side of (24) for every $\mathbb P\in\mathcal P^{FB}$ and every $v$.

Milestones

1. The Chen–Sim–Sun bound (22): for independent components with known means $\mu_i$ and deviations, $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\sum_i\mu_iv_i+\sqrt{2\log(1/\varepsilon)(\sum_{v_i<0}\sigma_{bi}^2v_i^2+\sum_{v_i\ge0}\sigma_{fi}^2v_i^2)}$.
2. The right-hand side of (24) is the worst case of (22) over the parameters allowed by $\mathcal P^{FB}$.
3. Lagrangian strong duality for $\max_{u\in\mathcal U^{FB}_\varepsilon}u^\top v$.
4. The three one-dimensional sub-subproblems and their optimal values.
5. The combined formula: $\delta^*$ equals a linear term plus $\inf_{\lambda>0}\{\lambda\log(1/\varepsilon)+S/(2\lambda)\}$.
6. $\inf_{\lambda>0}\{\lambda L+S/(2\lambda)\}=\sqrt{2LS}$, attained at $\lambda^*=\sqrt{S/(2L)}$ when $S>0$.

Companions

• Remark 9: when (24) exceeds $t$, an explicit point of $\mathcal U^{FB}_\varepsilon$ gives a violated cut $u^\top v\le t$.
• Theorem 13(b): the constraint $\delta^*(v\mid\mathcal U^{FB}_\varepsilon)\le t$ is convex in $(v,t)$ and convex in $\varepsilon$ for $0<\varepsilon<1/\sqrt e$.

Significance

Theorem 6 gives a data-driven uncertainty set for which a robust linear constraint is a second-order cone constraint, (24) being an explicit norm expression. By Theorem 1 of the paper, the domination of the worst-case Value at Risk over the region by the support function means that every robustly feasible solution satisfies a chance constraint at level $\varepsilon$ for every distribution in the region. Unlike the Chen–Sim–Sun set, which requires the true mean and deviations, $\mathcal U^{FB}_\varepsilon$ needs only data and allows the mean and the support to be unknown. Theorem 13(b) supports the alternating heuristic of §9 for choosing the levels $\varepsilon_j$ across several constraints.

The paper's proof is short and leans on "by inspection" and "by Lagrangian strong duality". A formal development makes each of these steps explicit, including the case where the multiplier is not attained, and corrects two printed slips (the optimal values $v_i\bar\sigma^2/(2\lambda)$, which should be $v_i^2\bar\sigma^2/(2\lambda)$, and the bound $m_b\le y_1\le m_b$). The Chen–Sim–Sun bound itself, a Chernoff-type tail bound under one-sided moment-generating conditions, is cited by the paper without proof. None of these results has a machine-checked proof that this mission is aware of.

Difficulty

The support function of (23) is a maximisation over a set defined by a box, two nonnegative orthants and one coupled quadratic constraint. A coordinate-wise argument does not apply directly because the quadratic budget is shared. The worst case over $\mathcal P^{FB}$ is not a single distribution: the extreme mean and the extreme deviations are chosen coordinate by coordinate according to the sign of $v_i$. The Value at Risk bound needs independence of the components; without it (22) fails. When $v=0$ or the sign pattern makes the quadratic term vanish, the dual multiplier escapes to zero and the dual minimum is only an infimum.

Formalization scope

Vectors are Fin d → ℝ, with 0-based coordinates; $\tilde u^\top v$ is u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\varepsilon$, and the support function is the published RobustMDP.Shared.supportFunction, a real supremum; the goal includes nonemptiness and compactness of $\mathcal U^{FB}_\varepsilon$, so the supremum is a true maximum and cannot hold through the value $0$ of an empty or unbounded set.

The statement is formalized in the criterion form: $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\delta^*(v\mid\mathcal U^{FB}_\varepsilon)$ for all $v$ and every $\mathbb P$ in the region. By Theorem 1 (mission I of this series), for a nonempty convex compact set this criterion is equivalent to the probabilistic guarantee. The page's "with probability $1-\alpha$ with respect to the sample" is the coverage of the bootstrap confidence region, which the paper itself treats as approximate; it is not formalized.

Conventions and added hypotheses:

• $\bar\sigma_{fi},\bar\sigma_{bi}>0$, so that the denominators of (23) are genuine; with $\bar\sigma=0$ Lean's $x/0=0$ would leave $y_2$ unconstrained instead of forcing $y_2=0$.
• $m_b\le m_f$, which holds because $t_i\ge0$.
• The region is built from a product measure (independence) of probability measures with bounded support. These are the hypotheses of Theorem 6 on $\mathbb P^*$ and the section's standing assumption; the page's set-builder for $\mathcal P^{FB}$ omits independence. Without bounded support, the Bochner integral of a non-integrable exponential is $0$ in Lean and the deviation conditions would lose their meaning.
• "$\sigma_f(\mathbb P_i)\le\bar\sigma$" is the predicate "the expression under the root is at most $\bar\sigma^2$ for every $x>0$", which is equivalent and avoids an unbounded supremum.
• Dual minimisations over $\lambda\ge0$ are infima over $\lambda>0$, stated with IsGLB.

A trivializing formalization is ruled out: a region without independence would make the goal false, a region without the probability and bounded-support conditions would let junk integrals satisfy the deviation predicates, and a support function of an empty set would make (24) a statement about $0$.

The development needs a Chernoff argument for products of measures, finite-dimensional Lagrangian duality for one convex quadratic constraint (or a direct Cauchy–Schwarz argument), and compactness of the set (23). The definitions file is self-contained and reusable for other forward/backward-deviation sets. Proofs of any milestone, and of the Chen–Sim–Sun bound as a standalone tail inequality, are welcome.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
• X. Chen, M. Sim, P. Sun, A Robust Optimization Perspective on Stochastic Programming, Operations Research 55(6):1058–1071, 2007. https://doi.org/10.1287/opre.1070.0441

Motivation

A robust linear constraint $f(\mathbf u,\mathbf x)\le 0$ for all $\mathbf u\in\mathcal U$ replaces an uncertain parameter $\tilde{\mathbf u}$ by a deterministic uncertainty set $\mathcal U\subseteq\mathbb R^d$. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets directly from data. Their requirement is a probabilistic guarantee: every robust-feasible decision should satisfy the constraint with probability at least $1-\epsilon$ under the true distribution $\mathbb P^*$, and this should hold with probability at least $1-\alpha$ over the sample. The construction runs a statistical hypothesis test, takes its confidence region of distributions, and turns the worst-case Value at Risk over that region into a set.

This mission covers the case where $\mathbb P^*$ may be continuous but its $d$ coordinates are known to be independent and supported in a known box (§5.1 of the paper). The test is the classical Kolmogorov–Smirnov (KS) goodness-of-fit test, applied separately to each marginal. The result is a convex set $\mathcal U^I_\epsilon$ whose support function has a one-dimensional closed form, (19). The set is representable with exponential cones, and a line search over a single multiplier separates over it (Remarks 6–7).

Setting

Let $d\ge 0$ and $N\ge 1$ (the sample size). For each coordinate $i$ we are given points $\hat u^{(0)}_i<\hat u^{(1)}_i<\cdots<\hat u^{(N)}_i<\hat u^{(N+1)}_i$. The interval $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ is the known box containing the support, and $\hat u^{(1)}_i,\dots,\hat u^{(N)}_i$ are the order statistics of the $i$-th coordinates of the data. Let $\Gamma=\Gamma^{KS}\in(0,1)$ be the KS threshold and $0<\epsilon<1$.

• The Value at Risk of $\mathbb P$ in direction $\mathbf v$ is $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^{\mathsf T}\mathbf v\le t)\ge 1-\epsilon\}$.
• The support function of a set is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^{\mathsf T}\mathbf u$.
• The KS region $\mathcal P^{KS}_i$ is the set of Borel probability measures $\mathbb P_i$ on $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ with $\mathbb P_i(\tilde u_i\le\hat u^{(j)}_i)\ge j/N-\Gamma$ and $\mathbb P_i(\tilde u_i<\hat u^{(j)}_i)\le (j-1)/N+\Gamma$ for $j=1,\dots,N$.
• The independent region $\mathcal P^I$ is the set of product measures $\prod_i\mathbb P_i$ with $\mathbb P_i\in\mathcal P^{KS}_i$.
• The vectors $q^L(\Gamma),q^R(\Gamma)\in\Delta_{N+2}$ of (17) are the two boundary distributions of the KS band. With $k=\lfloor N(1-\Gamma)\rfloor$, $q^L$ puts mass $\Gamma$ at $j=0$, mass $1/N$ at $j=1,\dots,k$, and mass $1-\Gamma-k/N$ at $j=k+1$. Its mirror image is $q^R_j=q^L_{N+1-j}$.
• The relative entropy is $D(\mathbf q,\mathbf p)=\sum_jq_j\log(q_j/p_j)$.
• The uncertainty set (18) is

$$\mathcal U^I_\epsilon=\Big\{\mathbf u:\exists\,\theta_i\in[0,1],\ \mathbf q^i\in\Delta_{N+2},\ \sum_{j=0}^{N+1}\hat u^{(j)}_iq^i_j=u_i,\ \sum_{i=1}^dD\big(\mathbf q^i,\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R\big)\le\log(1/\epsilon)\Big\}.$$

Formalization targets

Goal: Theorem 5 (deterministic content)

For every $\mathbf v\in\mathbb R^d$:

$$\mathcal U^I_\epsilon\ \text{is nonempty, convex and compact},\qquad \mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)\ \ \forall\,\mathbb P\in\mathcal P^I,$$ $$\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)=\inf_{\lambda>0}\Big\{\lambda\log(1/\epsilon)+\lambda\sum_{i=1}^d\log\Big[\max\Big(\sum_{j}q^L_je^{v_i\hat u^{(j)}_i/\lambda},\sum_jq^R_je^{v_i\hat u^{(j)}_i/\lambda}\Big)\Big]\Big\}.\tag{19}$$

Milestones, in attack order

1. The Nemirovski–Shapiro bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\lambda\log(1/\epsilon)+\lambda\sum_i\log\mathbb E^{\mathbb P_i}[e^{v_i\tilde u_i/\lambda}]$ for independent, compactly supported marginals.
2. The boundary laws $q^L$, $q^R$ belong to $\mathcal P^{KS}_i$.
3. Theorem EC.2: for monotone $g$, $\sup_{\mathcal P^{KS}_i}\mathbb E[g(\tilde u_i)]=\max(\sum_jq^L_jg(\hat u^{(j)}_i),\sum_jq^R_jg(\hat u^{(j)}_i))$.
4. (16) combined with EC.2: the Value at Risk over $\mathcal P^I$ is at most the expression in (19), for every $\lambda>0$.
5. The Lagrangian dual of $\max\{\mathbf v^{\mathsf T}\mathbf u:\mathbf u\in\mathcal U^I_\epsilon\}$.
6. (EC.6): $\max_{\mathbf q\in\Delta}\{\mathbf c^{\mathsf T}\mathbf q-D(\mathbf q,\mathbf p)\}=\log\sum_jp_je^{c_j}$.
7. (EC.7): the linear optimization over $\theta_i\in[0,1]$ is solved at an endpoint.

Significance

Theorem 5 gives a data-driven uncertainty set for continuous distributions with independent components. Its guarantee is finite-sample, not asymptotic, and its support function costs one line search over $\lambda$ to evaluate. Theorem 1 of the paper shows that $\mathrm{VaR}\le\delta^*$ for all $\mathbf v$ is equivalent to the probabilistic guarantee for nonempty convex compact sets. So the goal certifies that every robust-feasible solution of a constraint concave in $\mathbf u$ satisfies the chance constraint for every distribution the KS tests cannot reject. Theorem EC.2 is a reusable fact about KS bands: monotone expectations are extremized at the band's two boundary distributions.

The result is proved in the paper, but none of it has been formalized. A formal development would supply:

• worst-case expectations over a KS confidence band;
• the finite Gibbs variational identity with possibly vanishing reference masses;
• a Chernoff-type Value-at-Risk bound for product measures;
• a strong-duality statement for an entropy-constrained convex program.

Difficulty

The obvious route to the VaR bound is a union bound over coordinates. It loses a factor of $d$ in $\epsilon$, which is why the paper uses exponential moments and independence instead. The KS region is infinite dimensional, so the inner supremum of (16) is not a finite linear program. Reducing it to the boundary distributions needs the monotonicity of $u\mapsto e^{v_iu/\lambda}$, and a measure-level comparison of distribution functions against the band. The support-function identity needs strong duality for a jointly convex divergence constraint. The duality holds because $\theta_i\mapsto\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R$ is affine and $D$ is jointly convex. The reference vector can have zero entries (when $N(1-\Gamma)$ is an integer, or in the middle of the band), so the Gibbs step must handle vanishing masses.

Formalization scope

• Data and conventions. Coordinates are Fin d. The points are uhat : Fin d → Fin (N + 2) → ℝ with the page's indices $j=0,\dots,N+1$, and the KS constraints run over j : Fin N, which is the page's $j-1$. The order statistics are data. They are ordered, $\hat u^{(0)}_i\le\hat u^{(1)}_i\le\dots\le\hat u^{(N+1)}_i$ (Monotone (uhat i)), as order statistics of a sample in the box are; ties are allowed.
• Standing assumptions. $N\ge1$, $0<\Gamma<1$ and $0<\epsilon<1$.
• Regions. Measures in $\mathcal P^{KS}_i$ are probability measures on $\mathbb R$ carried by the box, and $\mathcal P^I$ consists of the Measure.pi products of such measures, so independence is built in.
• Relative entropy. $D$ carries an explicit finiteness predicate ($q_j>0\Rightarrow p_j>0$), so Lean's log 0 = 0 cannot make an infinite divergence finite.
• Published definitions. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$, and $\delta^*$ is the published RobustMDP.Shared.supportFunction, a real sSup. The goal proves $\mathcal U^I_\epsilon$ nonempty and compact, so $\delta^*$ is never the junk value $0$ of an empty or unbounded set.
• Infima and the multiplier. Infima over $\lambda$ are over $\lambda>0$ and stated with IsGLB. The page's $\lambda\ge0$ gives the same value.
• Criterion form of the guarantee. The guarantee is stated as $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)$ for all $\mathbb P\in\mathcal P^I$. By Theorem 1 (mission I of this series), this criterion is equivalent to the probabilistic guarantee for nonempty convex compact sets.
• Coverage of the test. The statement "with probability at least $1-\alpha$ over the sample" is the coverage of $\mathcal P^I$. It rests on the distribution-free law of the KS statistic (tables) and on combining $d$ tests at level $1-\sqrt[d]{1-\alpha}$. This part is cited, not formalized.
• Ruled out. The VaR inequality is never checked against a $\delta^*$ that sSup collapses to $0$, and the divergence budget is never relaxed by unguarded logarithms.

Contributions are welcome on any milestone. Milestones 1, 3 and 6 are independent of each other and of the rest; the goal follows from milestones 1–7 together with the convex-analytic facts about $\mathcal U^I_\epsilon$.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
• A. Nemirovski, A. Shapiro, Convex approximations of chance constrained programs, SIAM J. Optim. 17(4):969–996, 2006. https://doi.org/10.1137/050622328
• M. A. Stephens, EDF statistics for goodness of fit and some comparisons, J. Amer. Statist. Assoc. 69(347):730–737, 1974. https://doi.org/10.1080/01621459.1974.10480196
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/

Motivation

Robust optimization replaces uncertain data by a set of possible values and requires a decision to work for every value in that set. A central question is how to choose the set from data so that robust feasibility also gives a specified chance of satisfying the original constraint. Bertsimas, Gupta, and Kallus study this question for several sampling models in Data-Driven Robust Optimization. Their finite-support construction addresses a practical case: the uncertain vector can take one of finitely many known outcomes, while their probabilities must be inferred from observations. The resulting sets use classical goodness-of-fit tests to account for uncertainty in those probabilities. Bertsimas, Gupta, and Kallus, §§2–4, pp. 2–13.

In this case the support vectors are known in advance, so the problem is not to discover which outcomes are possible. The question is how much confidence to place in their estimated frequencies and how to turn that confidence region into a set of uncertain vectors suitable for a robust constraint. The paper gives two answers, one based on Pearson's chi-square statistic and one based on the likelihood-ratio, or G, statistic. Both answers are meant to work at every requested risk level $0<\epsilon<1$ for the same observed sample. Bertsimas, Gupta, and Kallus, Theorem 4, p. 13.

Setting

Let $a_0,\ldots,a_{n-1}\in\mathbb R^d$ be the listed possible outcomes. A probability vector $p=(p_j)$ belongs to the simplex $\Delta_n$ when all $p_j$ are nonnegative and $\sum_jp_j=1$. It determines the finite-support law $P_p=\sum_jp_j\delta_{a_j}$. From a sample one obtains the empirical frequencies $\hat p\in\Delta_n$. A nonnegative number $\rho$ records the test threshold; in the paper it is $\chi^2_{n-1,1-\alpha}/(2N)$, where $N$ is sample size and $\alpha$ is the test's significance level. Bertsimas, Gupta, and Kallus, (10), p. 12.

The Pearson confidence region $\mathcal P^{\chi^2}$ contains candidates $p\in\Delta_n$ satisfying $\sum_j(p_j-\hat p_j)^2/(2p_j)\le\rho$. The G confidence region $\mathcal P^G$ instead requires $D(\hat p,p)\le\rho$, with relative entropy $D(r,p)=\sum_jr_j\log(r_j/p_j)$. In either region, a candidate $p_j=0$ is excluded when $\hat p_j>0$: the source's divergence is then infinite. If both entries are zero, that coordinate contributes zero. These conventions matter because ordinary real division and logarithm in Lean have total values at zero. Bertsimas, Gupta, and Kallus, (10), p. 12.

For a direction $v\in\mathbb R^d$, value at risk $\operatorname{VaR}^{P_p}_\epsilon(v)$ is the lower $1-\epsilon$ quantile of the scalar loss $u^{\mathsf T}v$. Conditional value at risk is the minimum over real $t$ of $t+\epsilon^{-1}\sum_jp_j(a_j^{\mathsf T}v-t)^+$. The paper's auxiliary set $U^{\operatorname{CVaR}_{P_p}}_\epsilon$ reweights the outcomes with another probability vector $q$ constrained by $q_j\le p_j/\epsilon$. The two data-driven uncertainty sets $U^{\chi^2}_\epsilon$ and $U^G_\epsilon$ allow such a reweighting for some $p$ in the corresponding confidence region. Their support function $\delta^*(v\mid U)$ is the largest $u^{\mathsf T}v$ over $u\in U$. Bertsimas, Gupta, and Kallus, (11)–(13), pp. 12–13; Theorem EC.1, p. ec2.

Formalization targets

The first target is the paper's finite-support CVaR identity and the comparison between the two risk measures:

$$\operatorname{VaR}^{P_p}_\epsilon(v) \le \operatorname{CVaR}^{P_p}_\epsilon(v) =\delta^*(v\mid U^{\operatorname{CVaR}_{P_p}}_\epsilon).$$

The goal is Theorem 4's deterministic claim, simultaneously for all $0<\epsilon<1$. For each $p$ in the relevant confidence region, it asks for both bounds

$$\operatorname{VaR}^{P_p}_\epsilon(v)\le\delta^*(v\mid U^{\chi^2}_\epsilon), \qquad \operatorname{VaR}^{P_p}_\epsilon(v)\le\delta^*(v\mid U^G_\epsilon)$$

for every $v$, with each uncertainty set nonempty, convex, and compact. A supporting milestone identifies each support function as the supremum of CVaR over its confidence region. The paper also displays conic optimization programs for these support functions in (14) and (15); those programs are outside this mission's drafted statements. Bertsimas, Gupta, and Kallus, Theorem 4, p. 13; proof, p. ec2.

Significance

The bounds give a way to certify the directional risk of every candidate distribution accepted by a goodness-of-fit test. For a nonempty convex compact uncertainty set, the paper's Theorem 1 turns this directional condition into a probabilistic guarantee for every constraint concave in the uncertain vector. Theorem 4 adds the sampling claim through coverage of the confidence region: when the true finite-support distribution belongs to that region, the whole family indexed by $\epsilon$ receives the guarantee. The statistical tests use chi-square approximations, so their advertised coverage is asymptotic rather than an exact finite-sample result. Bertsimas, Gupta, and Kallus, Theorems 1–4, pp. 10–13.

The paper proves the mathematical result. This mission asks for machine-checked proofs of its finite-dimensional definitions, the CVaR identity, the worst-case support identities, and the deterministic risk bounds. The drafted Lean statements are open goals. A completed development would also give reusable facts about finite-support risk measures and support functions under divergence-constrained probabilities. It would leave the test coverage calculation and the explicit programs (14)–(15) for separate work.

Difficulty

The risk comparison alone does not identify a robust uncertainty set: the support function must agree with the worst-case CVaR over an entire region of probability vectors. This brings a finite-dimensional optimization identity into the formal proof, including attainment and the relationship between reweightings and distributions. Boundary coordinates create another difficulty. The Pearson expression divides by $p_j$, and the G expression contains $\log(\hat p_j/p_j)$; silently accepting Lean's values at zero would enlarge the regions and change the theorem. The support function and CVaR are real infima or suprema, so their nonempty, bounded domains must also be established. Bertsimas, Gupta, and Kallus, (10)–(13), pp. 12–13; proof, p. ec2.

Formalization scope

Lean represents outcomes and probability vectors as functions on Fin d and Fin n; indices start at zero. The simplex is Mathlib's stdSimplex. The law is a finite sum of point masses. If two listed vectors coincide, their point masses aggregate; the paper's notation $p_j=P_p(\tilde u=a_j)$ is recovered with the intended distinct listing. Value at risk and the support function reuse published Prove2Me definitions; the finite-vector relative entropy also reuses a published definition, guarded at zero in this mission's G region. CVaR uses a real sInf, equal to the paper's minimum for a simplex law and $0<\epsilon<1$. No statement applies it outside that domain.

The goal assumes $\hat p\in\Delta_n$ and $\rho\ge0$. These express, respectively, that the center is an empirical probability vector and that the chi-square threshold is nonnegative. It quantifies over every $0<\epsilon<1$, with the same confidence regions for all levels. The paper's sample size, chi-square quantile, and significance level are compressed into $\rho$; coverage of the true distribution by the test is a separate statistical premise and is not formalized here. The source's $\mathbb P^*$ is represented by $P_{p^*}$ for a supported probability vector $p^*$. The draft does not treat an arbitrary unsupported law as a member of the confidence region.

The nonempty and compact conclusions rule out a zero returned by a support function on an empty or unbounded set. The zero-denominator guards rule out candidates the paper assigns infinite divergence. Contributions needed to close the mission include finite-simplex geometry, the finite-support CVaR identity, continuity of the divergence regions at boundary coordinates, and the risk-bound theorem. Those facts can be reused in later data-driven robust optimization developments.

Selected references

• Dimitris Bertsimas, Vishal Gupta, and Nathan Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; revised version in Mathematical Programming 167 (2018), 235–292. Preprint.

Motivation

Most stochastic programs of practical size, such as two-stage recourse models in energy, finance or supply-chain planning, cannot be solved exactly: the expectation in the objective is a high-dimensional integral. The standard remedy is sample average approximation (SAA): replace the expectation by an average over a Monte Carlo sample and solve the resulting deterministic problem. This produces a candidate solution $\hat x$ but says nothing about how good it is. A decision maker needs a statistical certificate: an interval that contains the candidate's optimality gap with a prescribed probability.

Mak, Morton and Wood (Oper. Res. Lett. 24, 1999) built such a certificate from $n_g\ge 30$ independent SAA replications, which requires solving at least 30 optimization problems. Bayraksan and Morton (preprint January 2005, published in Math. Program. 108, 2006) showed that a single replication suffices asymptotically, and gave two variants that use two replications. This mission formalizes their validity theorems.

Setting

Let $\tilde\xi$ be a random vector with distribution $\mu$ on a measurable space $\Xi$, let $X\subseteq\mathbb R^d$ be a set of decisions, and let $f:\mathbb R^d\times\Xi\to\mathbb R$ be a cost. The stochastic program is

$$z^*=\min_{x\in X} Ef(x,\tilde\xi). \qquad\text{(SP)}$$

Its optimal set is $X^*$, and the optimality gap of a candidate $\hat x\in X$ is $\mu_{\hat x}=Ef(\hat x,\tilde\xi)-z^*\ge 0$. The paper assumes throughout:

• (A1) $f(\cdot,\tilde\xi)$ is continuous on $X$, with probability one;
• (A2) $E\sup_{x\in X} f^2(x,\tilde\xi)<\infty$;
• (A3) $X$ is nonempty and compact.

Let $\tilde\xi^1,\tilde\xi^2,\dots$ be i.i.d. copies of $\tilde\xi$, and write $\bar f_n(x)=\frac1n\sum_{i=1}^n f(x,\tilde\xi^i)$. The SAA problem is $z_n^*=\min_{x\in X}\bar f_n(x)$ (SP$_n$), with an optimal solution $x_n^*$. The gap estimator is $G_n(\hat x)=\bar f_n(\hat x)-z_n^*$ (display (2)), and the sample variance of the differences $f(\hat x,\tilde\xi^i)-f(x,\tilde\xi^i)$ is

$$s_n^2(x)=\frac1{n-1}\sum_{i=1}^n\Big[\big(f(\hat x,\tilde\xi^i)-f(x,\tilde\xi^i)\big)-\big(\bar f_n(\hat x)-\bar f_n(x)\big)\Big]^2,$$

with population counterpart $\sigma^2_{\hat x}(x)=\operatorname{var}[f(\hat x,\tilde\xi)-f(x,\tilde\xi)]$. Finally $z_\alpha$ is defined by $P(N(0,1)\le z_\alpha)=1-\alpha$.

The single replication procedure (SRP) solves (SP$_n$) once and reports the one-sided interval $\big[0,\ G_n(\hat x)+z_\alpha s_n(x_n^*)/\sqrt n\big]$ (display (5)). The I2RP takes the variance from a second, independent sample $\tilde\xi^{n+1},\dots,\tilde\xi^{2n}$ and its own minimizer $x_n^{2*}$. The A2RP runs the SRP on both halves of a sample of size $2n$, averages the gaps and the variances as in (10), and scales by $\sqrt{2n}$.

Formalization targets

Goal: Theorem 2 (p. 7)

Under (A1)–(A3), for $\hat x\in X$ and $0<\alpha<1$, provided $\alpha\le1/2$ or $\sigma^2_{\hat x}(x^*_{\max})>0$ (see Formalization scope),

$$\liminf_{n\to\infty}P\left(\mu_{\hat x}\le G_n(\hat x)+\frac{z_\alpha s_n(x_n^*)}{\sqrt n}\right)\ge 1-\alpha. \qquad(6)$$

Consistency (Proposition 1, p. 6)

The milestones follow the paper's own proof:

1. the uniform strong law $\sup_{x\in X}|\bar f_n(x)-Ef(x,\tilde\xi)|\to 0$ w.p.1;
2. (i) $z_n^*\to z^*$ w.p.1;
3. (ii) every limit point of $\{x_n^*\}$ lies in $X^*$ w.p.1;
4. the uniform convergence $s_n^2\to\sigma^2_{\hat x}$ on $X$ w.p.1;
5. (iii) $\sigma^2_{\hat x}(x^*_{\min})\le\liminf_n s_n^2(x_n^*)\le\limsup_n s_n^2(x_n^*)\le\sigma^2_{\hat x}(x^*_{\max})$ w.p.1, where $x^*_{\min}$ and $x^*_{\max}$ minimize and maximize $\sigma^2_{\hat x}$ over $X^*$;
6. the $\varepsilon$-bound of the proof of Theorem 2: if $\alpha\le 1/2$ and $\sigma^2_{\hat x}(x^*_{\min})>0$, then for $0<\varepsilon<1$ the liminf in (6) is at least $\Phi((1-\varepsilon)z_\alpha)$.

Companions

Theorem 3 (p. 9) and Theorem 4 (p. 10) are the same coverage statement for the I2RP and the A2RP. Three further statements are included: the negative bias $Ez_n^*\le z^*$ of display (1), the pathwise bound $G_n(\hat x)\ge\bar f_n(\hat x)-\bar f_n(x)$ for $x\in X$, and the consistency $\liminf_n s_n'^2\ge\sigma^2_{\hat x}(x^*_{\min})$ of the pooled variance.

Significance

Theorem 2 makes a single SAA solve enough for an asymptotically valid upper confidence bound on the optimality gap. It cuts the computational cost of the multiple-replication procedure by a factor of about thirty, and it needs no asymptotic normality of $G_n(\hat x)$, which typically fails when (SP) has several optimal solutions. The two-replication variants lessen the small-sample under-coverage of the SRP. The single- and two-replication estimators were later reused in sequential sampling procedures for SAA.

As far as is known, none of these results has been machine-checked. A complete formalization needs a uniform strong law of large numbers over a compact parameter set, which is a reusable result in its own right, together with the SAA consistency theory and a central-limit argument for a statistic that is not itself asymptotically normal.

Difficulty

The obvious route would be to show that $G_n(\hat x)$ is asymptotically normal and apply a standard confidence-interval argument. That fails: $z_n^*$ is a minimum of sample averages, and when $X^*$ is not a singleton its limit law is the law of a minimum of correlated Gaussians, not a Gaussian. The paper's argument has to bound the coverage from below without that limit law. It also needs to control the sample variance at a random, non-convergent minimizer $x_n^*$, which only accumulates on $X^*$. The uniform strong law (Rubinstein–Shapiro, Lemma A1) on which both consistency statements rest is not in Mathlib.

Formalization scope

The Lean development uses these conventions:

• Decisions live in EuclideanSpace ℝ (Fin d). The paper's $\mathbb R^n$ is renamed $\mathbb R^d$ because $n$ is the sample size.
• $\mu$ is a probability measure on $\Xi$ (the law of $\tilde\xi$), and $Ef(x,\tilde\xi)$ is the Bochner integral $\int f(x,\cdot)\,d\mu$.
• The sample is one infinite i.i.d. sequence ξ : ℕ → Ω → Ξ on a probability space $(\Omega,P)$, 0-based: $\tilde\xi^i$ is ξ (i-1). The second sample of Theorems 3–4 is ξ n, …, ξ (2n-1), exactly as printed, and the A2RP's "random" partition is this fixed one, which has the same joint law.
• Estimators are functions of a sample path. $z^*$ and $z_n^*$ are infima of images of $X$, and $X^*$ is an argmin set.
• Probabilities are ℝ≥0∞-valued, so the liminf in (6) is genuine. Proposition 1 (iii) is stated in its equivalent $\varepsilon$-form, which avoids real liminf/limsup junk values.
• $z_\alpha$ is any real with cdf (gaussianReal 0 1) zα = 1 - α.

Standing assumptions and pins. Every goal-level statement carries (A1)–(A3) and the i.i.d. hypothesis. Three hypotheses are made explicit that the paper leaves implicit:

1. $f(x,\cdot)$ is measurable for each $x$ ("$f(x,\tilde\xi)$ is a random variable");
2. $x_n^*$ is a measurable map that, almost surely, lies in $X$ and minimizes $\bar f_n$ over $X$ on the same sample;
3. (A2) is read as "$\sup_{x\in X}f^2(x,\cdot)$ has an integrable majorant", which avoids proving that the supremum is measurable.

At $n\le 1$ the factors $1/n$, $1/(n-1)$ and $1/\sqrt n$ evaluate to Lean's $0$; every coverage statement is a liminf and ignores them.

Several encodings would trivialize the statement, and all are ruled out. The minimizer $x_n^*$ must minimize the SAA problem of its own sample: a free $x_n^*$, or one fitted to the other sample, would change the theorem. The second sample must not be replaced by an independent sequence. The quantile must not be pinned through an sInf. Positivity of $\sigma^2_{\hat x}(x^*_{\min})$ is a hypothesis only of the $\varepsilon$-bound, as on p. 8.

One correction of the paper. Theorems 2 and 4 are stated for every $0<\alpha<1$, but for $\alpha>1/2$ the paper's argument (replace $x^*_{\min}$ by $x^*_{\max}$) needs $\sigma^2_{\hat x}(x^*_{\max})>0$, and without it both statements are false: for $X=[-1,1]$, $f(x,\xi)=x^2-2x\xi$, $\tilde\xi\sim N(0,1)$, $\hat x=0$ and $\alpha=0.9$, the SRP coverage tends to about $0.010$ and the A2RP coverage to $e^{-2z_\alpha^2}\approx0.037$, both below $0.1$. The Lean goal and Theorem 4 therefore carry the hypothesis "$\alpha\le1/2$, or $\sigma^2_{\hat x}(x)>0$ for some $x\in X^*$". Theorem 3 is stated as printed.

Contributions are welcome at every level. The most reusable one is the uniform strong law of large numbers for Carathéodory integrands on a compact set with an integrable envelope, which also serves other SAA consistency results.

Selected references

• G. Bayraksan, D. P. Morton, Assessing Solution Quality in Stochastic Programs, preprint (January 26, 2005); published in Math. Program. 108 (2006). https://doi.org/10.1007/s10107-006-0720-x
• W. K. Mak, D. P. Morton, R. K. Wood, Monte Carlo bounding techniques for determining solution quality in stochastic programs, Oper. Res. Lett. 24 (1999) 47–56. https://doi.org/10.1016/S0167-6377(98)00054-6
• R. Y. Rubinstein, A. Shapiro, Discrete Event Systems: Sensitivity Analysis and Stochastic Optimization by the Score Function Method, Wiley, 1993 (Lemma A1, p. 67; Theorem A1, p. 69).
• A. Shapiro, Monte Carlo sampling methods, in: Handbooks in OR & MS 10, Stochastic Programming, Elsevier, 2003, 353–425. https://doi.org/10.1016/S0927-0507(03)10006-0

Motivation

Local Rademacher averages measure the complexity of a learning problem only near the functions that matter, such as those with small empirical error, rather than over the whole function class. Bartlett, Bousquet and Mendelson (Local Rademacher complexities, Ann. Statist. 33 (2005)) show that error bounds for empirical risk minimization are governed by the fixed point of a sub-root upper bound on such local averages, and that these bounds give fast rates ($1/n$ rather than $1/\sqrt n$) under variance conditions. A bound is only useful in practice if it can be computed from the data. For classification with the discrete loss, the paper's Corollary 6.2 states the bound in terms of a localized empirical Rademacher average $\hat\psi_n(r)$. That average is a supremum over a constrained subclass, and it is not obvious how to evaluate it.

Theorem 6.3 of the paper answers this. An upper bound on $\hat\psi_n(r)$ can be computed by any algorithm that minimizes a weighted empirical classification error. A similar reduction was known for the global Rademacher average of a classification class: Bartlett, Boucheron and Lugosi (Model selection and error estimation, Machine Learning 48 (2002)) observed that the empirical Rademacher average equals one half minus an expected empirical risk minimum with random labels, and Lemma 6.4 of the paper is adapted from their argument. Theorem 6.3 shows that localization and the use of star-hulls keep this reduction intact.

Setting

Fix inputs $X_1,\dots,X_n$ in a set $\mathcal X$ ($n\ge1$) and labels $Y_1,\dots,Y_n\in\{-1,1\}$. Everything below is deterministic given this sample. A classifier is a function $f:\mathcal X\to\{-1,1\}$, and $\mathcal F$ is a class of classifiers. The discrete loss is $\ell(y,y')=\mathbf 1[y\ne y']$. For a vector $z\in\mathbb R^n$ write

$$P_n\ell(f(X),z)=\frac1n\sum_{i=1}^n\ell(f(X_i),z_i),\qquad P_n\ell_f=P_n\ell(f(X),Y),$$

so $P_n\ell_f$ is the empirical risk of $f$.

A sign vector $\sigma\in\{-1,1\}^n$ plays the role of Rademacher signs, and $\mathbb E_\sigma$ is the average over all $2^n$ sign vectors. The empirical Rademacher average of the loss functions of the classifiers with empirical risk at most $b$ is

$$\mathbb E_\sigma R_n\{\ell_f : f\in\mathcal F,\ P_n\ell_f\le b\}=\frac1n\,\mathbb E_\sigma\sup_{f\in\mathcal F,\ P_n\ell_f\le b}\ \sum_{i=1}^n\sigma_i\,\ell(f(X_i),Y_i).$$

For $c\ge0$, $x>0$ and $0<r\le1/2$, the empirical local Rademacher complexity of the classification loss class is

$$\hat\psi_n(r)=c\sup_{\alpha\in[\sqrt{2r},1]}\alpha\,\mathbb E_\sigma R_n\{\ell_f : f\in\mathcal F,\ P_n\ell_f\le 2r/\alpha^2\}+\frac{26x}{n}.$$

In Corollary 6.2, $c=20$. The parameter $\alpha$ comes from the star-hull of the loss class: rescaling a loss function by $\alpha$ turns the constraint $P_n(\alpha\ell_f)^2\le 2r$ into $P_n\ell_f\le 2r/\alpha^2$.

For a sign vector $\sigma$ and a multiplier $\mu\ge0$, the weighted empirical risk minimum is

$$J(\mu)=\min_{f\in\mathcal F}\frac1n\sum_{i=1}^n|\sigma_i+\mu Y_i|\,\ell\big(f(X_i),\operatorname{sign}(\sigma_i+\mu Y_i)\big).$$

It is the smallest weighted training error when the labels are corrupted to $\operatorname{sign}(\sigma_i+\mu Y_i)$ and example $i$ has weight $|\sigma_i+\mu Y_i|$.

Formalization targets

Goal: Theorem 6.3

If some $f\in\mathcal F$ has $P_n\ell_f\le 2r$, then

$$\hat\psi_n(r)\le c\sup_{\alpha\in[\sqrt{2r},1]}\alpha\,\mathbb E_\sigma\min_{\mu\ge0}\Big(\Big(\frac{2r}{\alpha^2}-\frac12\Big)\mu+\frac1{2n}\sum_{i=1}^n|\sigma_i+\mu Y_i|-J(\mu)\Big)+\frac{26x}{n}.$$

The multiplier $c$ is kept general, and the term $26x/n$ appears on both sides as printed.

Milestones

1. Lemma 6.4. For every $b\in[0,1]$ with a feasible classifier,

$$\mathbb E_\sigma R_n\{\ell_f : f\in\mathcal F,\ P_n\ell_f\le b\}=\frac12-\mathbb E_\sigma\min\{P_n\ell(f(X),\sigma) : f\in\mathcal F,\ P_n\ell(f(X),Y)\le b\}.$$

2. Weak duality (proof of Theorem 6.3). With $L(f,\mu)=P_n\ell(f(X),\sigma)+\mu(P_n\ell(f(X),Y)-2r/\alpha^2)$ and $g(\mu)=\min_{f\in\mathcal F}L(f,\mu)$, for every $\mu\ge0$,

$$\min\{P_n\ell(f(X),\sigma) : f\in\mathcal F,\ P_n\ell(f(X),Y)\le 2r/\alpha^2\}\ge g(\mu).$$

3. The identity for $g(\mu)$ (proof of Theorem 6.3, corrected).

$$g(\mu)=J(\mu)-\frac1{2n}\sum_{i=1}^n|\sigma_i+\mu Y_i|+\frac{1+\mu}2-\mu\frac{2r}{\alpha^2}.$$

Significance

The theorem turns a quantity defined by a supremum over a data-dependent subclass into one computable by a standard learning primitive. For each sign vector and each multiplier $\mu$, $J(\mu)$ is the value of a weighted classification problem, which any weighted empirical risk minimizer solves. The expectation over signs can be estimated by repeated sampling. The paper notes that $J$ is Lipschitz in $\mu$, so a finite grid of $\mu$ values suffices, and that a sub-root upper bound on $\hat\psi_n$ can then be read off. Combined with Corollary 6.2, this yields error bounds for empirical risk minimization in classification that are computable from the training data and that localize: they depend only on the classifiers with small empirical error.

The result is proved in the paper. It has not been formalized; as far as a search of the Prove2Me catalog shows, neither the classification loss class nor $J(\mu)$ exists as a formal object. This mission produces machine-checked statements of the theorem and of its three proof steps. These cover the exact identity between Rademacher averages of the discrete loss class and random-label empirical risk minimization, and a Lagrangian duality bound for constrained empirical risk minimization.

Difficulty

The obvious route is to apply Lemma 6.4 and then exchange the constrained minimum for a Lagrangian. Each step has a point where a careless argument fails.

• Lemma 6.4 needs a change of variables on sign vectors ($\sigma_i\mapsto-Y_i\sigma_i$) that preserves the uniform average. It also needs the identity $\ell(y,y')=|y-y'|/2$ on $\{\pm1\}$, which fails off $\{\pm1\}$.
• The Lagrangian step gives only weak duality. The bound is an inequality, and attempts to prove equality in Theorem 6.3 fail in general.
• The identity for $g(\mu)$ rests on $\ell(y,\hat y)=(1-y\hat y)/2$. This holds only for $\pm1$ arguments, while $\operatorname{sign}(\sigma_i+\mu Y_i)$ is $0$ when $\mu=1$ and $\sigma_i=-Y_i$. Those terms carry weight zero, and the bookkeeping has to show this.
• Passing the per-$\alpha$, per-$\sigma$ inequalities through the outer supremum and the average requires every supremum and minimum to be over a nonempty, bounded set. This is where the feasibility hypothesis is used.

Formalization scope

• Representation. Inputs are xs : Fin n → X for an arbitrary type X. Labels and signs are real vectors Fin n → ℝ. Classifiers are functions X → ℝ with values in $\{\pm1\}$, a class is a Set (X → ℝ), and the discrete loss is defined on all real pairs. Sign vectors are indexed by Fin n → Bool through the published UnderstandingML.signVec. Every $\mathbb E_\sigma$, on both sides of every statement, is the finite average over these $2^n$ vectors; no probability measure is used. The empirical Rademacher average is the published UnderstandingML.rademacher applied to the set of loss vectors.
• Suprema and minima. Every supremum and minimum is Lean's real ⨆/⨅ over a subtype. The hypotheses make each index set nonempty and each family bounded, so these are true suprema and minima. The convention Real.sign 0 = 0 is used where the paper's sign is undefined; it affects only weight-zero terms.
• Added hypotheses. Each of these is implicit on the page:
  • $n\ge1$;
  • $c\ge0$ (for $c<0$ the inequality reverses);
  • $0<r\le1/2$ (otherwise the range of $\alpha$ is empty);
  • $x>0$ (Corollary 6.2's "fix $x>0$");
  • a classifier with $P_n\ell_f\le 2r$ in the goal, and a feasible classifier in Lemma 6.4 and in the weak duality step (the page's minima presuppose one);
  • a nonempty $\mathcal F$ in the $g(\mu)$ identity.
• Corrections of the print. The last display of the proof on p. 30 ends each line with $-2r/\alpha^2$. From the page's own definition $g(\mu)=\min_f L(f,\mu)$, the constant is $-\mu\,2r/\alpha^2$, which is the form Theorem 6.3's term $(2r/\alpha^2-1/2)\mu$ requires. The milestone states the corrected identity.
• No trivialization. Without the feasibility hypothesis, Lean would evaluate the empty-class Rademacher average and the unbounded $\mu$-minimum to the junk value $0$, and the goal would compare junk values. The feasibility hypothesis rules this out. The goal is the inequality between the two expressions for $\hat\psi_n$ as printed; it is not restated through $g(\mu)$, $L(f,\mu)$ or Lemma 6.4.
• Contributions welcome. A reusable lemma that the uniform average over $\{\pm1\}^n$ is invariant under coordinatewise sign flips would serve beyond this mission, as would general facts about real infima over finite-valued families. Proofs of the three milestones, and of the goal from them, are the main targets.

Selected references

• P. L. Bartlett, O. Bousquet, S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 1497–1537, 2005. arXiv:math/0508275v1 (cited version): https://arxiv.org/abs/math/0508275, DOI https://doi.org/10.1214/009053605000000282 — §6.2, Corollary 6.2 and Theorem 6.3 (pp. 28–29), Lemma 6.4 (p. 29), proof of Theorem 6.3 (p. 30).
• P. L. Bartlett, S. Boucheron, G. Lugosi, Model selection and error estimation, Machine Learning 48, 85–113, 2002. https://doi.org/10.1023/A:1013999503812
• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian complexities: risk bounds and structural results, Journal of Machine Learning Research 3, 463–482, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 26 (the Rademacher complexity reused here). https://doi.org/10.1017/CBO9781107298019