Probability

Why shrink an uncertainty set

Robust optimization (RO) protects a decision against every parameter value in an uncertainty set. For a decision $v$ and a parameter $x \in \mathbb{R}^m$ with objective $f(v, x)$ to be maximized, the robust problem around a nominal parameter $x_0$ with a deviation set $\Delta$ is

$$\max_{v} \min_{x_\delta \in \Delta} f(v, x_0 + x_\delta).$$

When deviations are not adversarial, this formulation is known to be conservative (Delage and Mannor, 2010; Xu and Mannor, NIPS 2006). A common remedy in practice is uncertainty set shrinkage: fix $\alpha \in (0,1)$ and solve the same problem over the shrunken set $\alpha\Delta = \{\alpha x : x \in \Delta\}$. The heuristic is easy to implement, but the meaning of the set $\alpha\Delta$ is unclear, and it has lacked a justification.

Section 4.2 of Xu, Caramanis and Mannor (2012) supplies one, using the paper's distributional interpretation of RO: the shrunken problem approximately solves a distributionally robust stochastic program (DRSP) with two scenarios. This mission formalizes that result, Theorem 4.1, and its two corollaries.

Setting

Let $\mathbb{R}^m$ carry the Euclidean norm $\|\cdot\|_2$ and its Borel $\sigma$-algebra, and let $\mathcal P$ be the set of Borel probability measures on $\mathbb{R}^m$. Let $V$ be any set of decisions and $f : V \times \mathbb{R}^m \to \mathbb{R}$. Fix $x_0 \in \mathbb{R}^m$, a deviation set $\Delta \subseteq \mathbb{R}^m$, and $\alpha \in (0,1)$. Write $x_0 + \Delta = \{x_0 + x : x \in \Delta\}$.

The two-scenario set is

$$\hat{\mathcal P}' = \{\mu \in \mathcal P \mid \mu(\{x_0\}) \ge 1-\alpha,\ \mu(x_0 + \Delta) = 1\}.$$

A distribution in $\hat{\mathcal P}'$ describes a system that is, with probability at least $1-\alpha$, in a normal state where the parameter equals $x_0$, and otherwise in an abnormal state where the parameter deviates by an element of $\Delta$. The DRSP value of a decision $v$ is $\inf_{\mu \in \hat{\mathcal P}'} \int f(v, x)\, d\mu(x)$.

Two further quantities enter. The radius of the deviation set is $D = \max_{x \in \Delta} \|x\|_2$. The curvature bound is a constant $h \ge 0$ with

$$-hI \preceq H_v(x) \preceq hI \quad \text{for all } v, x,$$

where $H_v(x)$ is the Hessian of $f(v, \cdot)$ at $x$ and $\preceq$ is the positive-semidefinite order. In the Lean development these are scenarioSet x₀ Δ (1 - α), drspValue, devRadius Δ and HasBoundedHessian (f v) h, all in the namespace DistInterpRO.Shrinkage.

Formalization targets

Goal: Theorem 4.1 (p. 104)

If $f(v,\cdot)$ is twice differentiable with $-hI \preceq H_v(x) \preceq hI$ for all $v, x$, then for all $v$

$$\inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x) - \alpha D^2 h \;\le\; \min_{x_\delta \in \alpha\Delta} f(v, x_0 + x_\delta) \;\le\; \inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x) + \alpha D^2 h.$$

Milestones (the displays of the proof on p. 105)

1. The mean-value step $f(v, x_0 + x_1) = f(v, x_0) + g_v(x_0 + \beta x_1)x_1$ for some $\beta \in [0,1]$, where $g_v$ is the gradient of $f(v,\cdot)$.
2. The gradient bound $\|g_v(x_0 + \beta x_1) - g_v(x_0 + \alpha\beta' x_1)\| \le h\|\beta x_1 - \alpha\beta' x_1\| \le h\|x_1\| \le hD$, stated together with the general fact that the Hessian bound makes $g_v$ $h$-Lipschitz.
3. The pointwise sandwich: for $x_1 \in \Delta$, $f(v, x_0 + \alpha x_1)$ lies within $\alpha D^2 h$ of $(1-\alpha) f(v, x_0) + \alpha f(v, x_0 + x_1)$.
4. The min sandwich: $\min_{\alpha\Delta} f(v, x_0 + \cdot)$ lies within $\alpha D^2 h$ of $(1-\alpha) f(v, x_0) + \alpha \min_{\Delta} f(v, x_0 + \cdot)$.
5. The two-scenario value: $(1-\alpha) f(v, x_0) + \alpha \min_{x_\delta\in\Delta} f(v, x_0 + x_\delta) = \inf_{\mu \in \hat{\mathcal P}'} \int f(v,x)\,d\mu(x)$, which the paper derives from its Corollary 5.2 (p. 107).

Further results

Corollary 4.2 (p. 104): if every $f(v,\cdot)$ is linear, the shrunken value equals the DRSP value exactly. Corollary 4.3 (p. 105): if $\Delta$ is star shaped, every $f(v,\cdot)$ is convex with $f(v, x_0) - \min_{\Delta} f(v, x_0 + \cdot) \ge 1$ and has Hessian bounded by $h$, then the shrunken value lies between the DRSP values over $\hat{\mathcal P}''$ and $\hat{\mathcal P}'$, where $\hat{\mathcal P}''$ requires only $\mu(\{x_0\}) \ge \max(0, 1-\alpha-\alpha D^2 h)$.

Significance

The result gives a physical meaning to the parameter $\alpha$ of the shrinkage heuristic: $1-\alpha$ is a lower bound on the probability that the system is in its nominal state. The error $\alpha D^2 h$ vanishes when the objective is linear in the parameter (Corollary 4.2), which covers linear programs with uncertain costs and Markov decision processes with uncertain rewards; in that case shrinkage is exactly a two-scenario DRSP. The paper also shows by example (p. 104) that without a curvature condition the two problems can differ, so the Hessian bound is the operative hypothesis.

The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it adds a checked link between the discrete two-point structure of the DRSP value and the smooth analysis of the shrunken minimum, with every standing hypothesis written out (see below). The mean-value and gradient-Lipschitz steps are general facts about functions on Euclidean space with bounded Hessian and are reusable elsewhere.

Difficulty

Two points need care. First, the step from the Hessian bound $-hI \preceq H_v \preceq hI$, a bound on a quadratic form, to the Lipschitz bound on the gradient requires the operator norm of the Hessian, which equals the largest absolute value of its quadratic form only because the Hessian is symmetric; symmetry of second derivatives must be invoked for a function that is merely twice (Fréchet) differentiable, not twice continuously differentiable. Second, the DRSP value is an infimum over an infinite-dimensional set of measures; identifying it with the two-point value requires both a construction of a near-optimal measure and a lower bound valid for every admissible measure, including measures that spread their abnormal mass over all of $x_0 + \Delta$.

Formalization scope

$\mathbb{R}^m$ is EuclideanSpace ℝ (Fin m) with its Borel $\sigma$-algebra. Measures are Measures, and membership in $\hat{\mathcal P}'$ includes IsProbabilityMeasure. Infima are real infima over subtypes; integrals are Bochner integrals.

The formalization makes the following readings explicit:

1. $\Delta$ is compact. The page writes min over $\alpha\Delta$ and max over $\Delta$, which presuppose attainment. Compactness together with continuity of $f(v,\cdot)$ gives attainment, a finite $D$, finite integrals and measurability of $x_0 + \Delta$. The goal additionally states that the minimum over $\alpha\Delta$ is attained.
2. $0 \in \Delta$. Without it $\hat{\mathcal P}'$ is empty, since $\mu(\{x_0\}) \ge 1-\alpha > 0$ and $\mu(x_0+\Delta)=1$ force $x_0 \in x_0 + \Delta$. The page's two-scenario reading presupposes it. In Corollary 4.3 it follows from star-shapedness once $\Delta$ is nonempty, and nonemptiness is added there.
3. Twice differentiable with bounded Hessian means that $f(v,\cdot)$ and its derivative are differentiable everywhere and $|D^2 f(v,\cdot)(x)[y,y]| \le h\|y\|_2^2$ for all $x, y$. The constant $h$ is one constant for all $v$.
4. The minima over $\Delta$ and $\alpha\Delta$ are written as infima, which equal the minima under the hypotheses above.

The Lean functions drspValue and devRadius return $0$ on an empty or unbounded input; the hypotheses above exclude those inputs, so no statement holds through a junk value. A formalization that dropped $0 \in \Delta$ would make the inequalities hold or fail for the wrong reason and is ruled out.

Contributions welcome: the Lipschitz-gradient lemma for bounded Hessians in Euclidean space, the evaluation of the two-scenario DRSP value, and the combination into Theorem 4.1 and its corollaries.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• E. Delage, S. Mannor, Percentile Optimization for Markov Decision Processes with Parameter Uncertainty, Operations Research 58(1):203–213, 2010. https://doi.org/10.1287/opre.1080.0685
• E. Delage, Y. Ye, Distributionally Robust Optimization under Moment Uncertainty with Applications to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• D. Bertsimas, D. B. Brown, C. Caramanis, Theory and Applications of Robust Optimization, SIAM Review 53(3):464–501, 2011. https://doi.org/10.1137/080734510

Motivation

Robust optimization (RO) protects a decision against every realisation of an uncertain parameter in a prescribed uncertainty set; distributionally robust stochastic programming (DRSP) protects it against every probability distribution in a prescribed distribution set. The two paradigms are usually treated separately. When the n uncertain parameters live in different spaces, it is folklore that RO over a product of sets is DRSP over the distributions supported on that product (Delage and Ye, Operations Research 2010).

In data-driven problems the situation is different: the parameters $x_1,\dots,x_n$ are samples, and all of them lie in the same space $\mathbb R^m$. Robustifying each sample by its own uncertainty set $\mathcal Z_i$ gives the objective $\sum_i c_i\inf_{x_i\in\mathcal Z_i}f(x_i)$, and the sets $\mathcal Z_i$ typically overlap. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that this objective is again a worst-case expectation, now over distributions on $\mathbb R^m$ itself rather than on $\mathbb R^{m\times n}$. This equivalence is what the same paper uses to prove that box-robust sample average optimisation is statistically consistent, and to explain the shrinkage heuristic of RO.

Setting

Let $m,n\ge1$ and write $[1:n]=\{1,\dots,n\}$. Let $\mathcal P$ be the set of Borel probability measures on $\mathbb R^m$. The data are:

• a measurable utility $f:\mathbb R^m\to\mathbb R$ (the decision variable is suppressed);
• weights $c_1,\dots,c_n>0$ with $\sum_{i=1}^n c_i=1$;
• nonempty Borel uncertainty sets $\mathcal Z_1,\dots,\mathcal Z_n\subseteq\mathbb R^m$, which may intersect or coincide.

For $S\subseteq[1:n]$ write $\mathcal Z_S=\bigcup_{i\in S}\mathcal Z_i$ and $N=[1:n]$. The distribution set is

$$\mathcal P_n=\Big\{\mu\in\mathcal P\ \Big|\ \forall S\subseteq[1:n]:\ \mu(\mathcal Z_S)\ge\sum_{i\in S}c_i\Big\}.$$

Each $\mu\in\mathcal P_n$ must give every union of uncertainty sets at least the total weight of its indices. For $\mu\in\mathcal P$ the expectation $\int f\,d\mu$ is the extended integral $\int f^+d\mu-\int f^-d\mu\in[-\infty,+\infty]$.

Formalization targets

Goal: Theorem 2.1 (Eq. (4), pp. 96–97)

$$\sum_{i=1}^n\Big[c_i\inf_{x_i\in\mathcal Z_i}f(x_i)\Big]=\inf_{\mu\in\mathcal P_n}\int_{\mathbb R^m}f(x)\,d\mu(x),$$

as an identity in $[-\infty,+\infty]$, with no boundedness assumption on $f$ and no disjointness assumption on the $\mathcal Z_i$.

Milestones (proof of Theorem 2.1, p. 97)

1. Every $\mu\in\mathcal P_n$ satisfies $\mu(\mathbb R^m\setminus\mathcal Z_N)=0$, hence $\int_{\mathbb R^m}f\,d\mu=\int_{\mathcal Z_N}f\,d\mu$.
2. Weak duality. With $f_i=\inf_{\mathcal Z_i}f$ finite, every $\alpha\in\mathbb R^{2^n}$ satisfying $\sum_S\alpha_S\mathbf 1(x\in\mathcal Z_S)\le f(x)$ on $\mathcal Z_N$ and $\alpha_S\ge0$ for $S\ne N$ obeys $\sum_i c_i\sum_S\alpha_S\mathbf 1(i\in S)\le\sum_i c_if_i$.
3. The nested dual solution. If $f_1\ge\dots\ge f_n$, the vector with $\alpha_{\{1,\dots,i\}}=f_i-f_{i+1}$, $\alpha_N=f_n$ and all other coordinates $0$ is feasible and has objective $\sum_i c_if_i$.

Further statements

• For pairwise disjoint $\mathcal Z_i$: $\mathcal P_n=\{\mu\in\mathcal P\mid\mu(\mathcal Z_i)=c_i,\ i=1,\dots,n\}$ (p. 97).
• Corollary 2.1 (Eq. (5)): $\inf_{x'\in\mathcal Z}f(x')=\inf_{\mu\in\mathcal P,\ \mu(\mathcal Z)=1}\int f\,d\mu$.
• Corollary 5.2 (nested distributions, p. 107): for $\mathcal Z_1\subseteq\dots\subseteq\mathcal Z_n$ and $0=p_0<p_1<\dots<p_n=1$,

$$\inf_{\mu\in\mathcal P,\ \mu(\mathcal Z_i)\ge p_i\ \forall i}\int f\,d\mu=\sum_{i=1}^n(p_i-p_{i-1})\inf_{x_i\in\mathcal Z_i}f(x_i).$$

Significance

The result. Theorem 2.1 turns a robust problem with overlapping uncertainty sets into a distributionally robust one on the original space $\mathbb R^m$. This is what allows distributions in $\mathcal P_n$ to be compared with the true data-generating distribution as $n$ grows: in §3 of the paper a kernel density estimator is shown to lie in $\mathcal P_n$ for box uncertainty sets, which yields consistency of box-robust sample average optimisation (Theorem 3.1); in §4.2 the nested-distribution form (Corollary 5.2) explains why shrinking an uncertainty set approximates a two-scenario DRSP (Theorem 4.1). The disjoint case recovers the classical product-space equivalence.

Formalizing it. The result is proved in the paper, through the strong duality of a semi-infinite linear program (Isii 1962). It has no machine-checked proof. The mission produces the equivalence as an identity of extended reals, together with a reusable definition of the union-mass distribution set. A proof need not follow the paper's duality route; any correct argument is welcome.

Difficulty

The inequality $\ge$ from the left side is the easy half: point masses $\sum_ic_i\delta_{x_i}$ with $x_i\in\mathcal Z_i$ belong to $\mathcal P_n$. The substance is the reverse bound, that no $\mu\in\mathcal P_n$ can do better than $\sum_ic_if_i$. For disjoint sets this is immediate, since $\mu(\mathcal Z_i)=c_i$. For overlapping sets a measure may place mass in intersections, and a single point of $\mathcal Z_i\cap\mathcal Z_j$ can serve several indices at once; the constraint family over all $2^n$ subsets is what prevents this, and the bound has to exploit the whole family, not the singleton constraints. The paper does this by appeal to semi-infinite LP duality, a theorem that Mathlib does not contain. Measure-theoretic side conditions (unbounded $\mathcal Z_i$, infinite integrals, infima equal to $-\infty$) must also be handled rather than assumed away.

Formalization scope

• $\mathbb R^m$ is Fin m → ℝ with its Borel $\sigma$-algebra; no norm is used. Indices $1,\dots,n$ are Fin n, subsets are Finset (Fin n), and $\{1,\dots,i\}$ is Finset.Iic i.
• $\mathcal P_n$ is a Set (Measure (Fin m → ℝ)) whose membership includes IsProbabilityMeasure; the constraint is imposed for every subset, $\emptyset$ and $[1:n]$ included.
• $\int f\,d\mu$ is expect μ f, defined in EReal as the difference of two lower Lebesgue integrals, $\int f^+-\int f^-$. The Bochner integral is not used, because its value $0$ on non-integrable functions would falsify Eq. (4). Both sides of Eq. (4) are EReal infima; the left infimum ranges over the nonempty set $\mathcal Z_i$.
• Readings of the printed statements. (i) The paper allows $f$ to take the value $-\infty$; here $f$ is real-valued. The excluded case is the one the proof disposes of in its first sentence, where both sides are $-\infty$. (ii) No boundedness hypothesis is added: when some $\inf_{\mathcal Z_i}f=-\infty$ both sides are $-\infty$, and otherwise every $\mu\in\mathcal P_n$ has a finite negative part. (iii) Corollary 2.1 prints "$f:\mathbb R\cup\{-\infty\}$" without a domain; it is read as $f:\mathbb R^m\to\mathbb R$. (iv) Corollary 5.2 is corrected: the paper prints the coefficient $(p_n-p_{n-1})$, while its proof sets $c_i=p_i-p_{i-1}$; the printed version is false (for $\mathcal Z_1=\{a\}\subseteq\mathcal Z_2=\{a,b\}$, $f(a)=1$, $f(b)=0$, $p_1=1/4$, the left side is $1/4$ and the printed right side $3/4$). The mission states $(p_i-p_{i-1})$. (v) The standing hypotheses of Theorem 2.1 ($f$ measurable, $\mathcal Z_i$ nonempty Borel) are made explicit in Corollary 5.2.
• The ordering $f_1\ge\dots\ge f_n$ is a hypothesis of the nested-dual milestone only, as the proof's "without loss of generality"; the goal does not assume it. Milestones 2 and 3 assume $f$ bounded below on each $\mathcal Z_i$ (the proof's first reduction), so that $f_i$ is a real number.
• Ruled out. A Bochner-integral formulation, a restriction to disjoint sets, a distribution set containing non-probability measures, or a set $\mathcal P_n$ defined by the singleton constraints $\mu(\mathcal Z_i)\ge c_i$ alone would each change or trivialise the theorem; none is used.
• Definitions (file Model): the set $\mathcal P_n$, the extended expectation, dual feasibility, and the nested dual vector. The extended expectation and the union-mass distribution set are reusable beyond this mission. Welcome contributions: a proof through semi-infinite LP duality, a direct measure-theoretic proof (for instance a layer-cake argument for the lower bound), and proofs of the corollaries from the goal.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14:185–197, 1962. https://doi.org/10.1007/BF02868641
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050

Motivation

Mission V supplied the general Lyapunov machinery — the extinction criteria of Lemmas 8.5, 8.6 and 8.11 — but a Lyapunov function does not construct itself. For a specific network structure and control policy, one must exhibit a concrete function and verify the drift condition. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the second half of Chapter 8 to two such constructions, chosen to illustrate the two basic templates every later stability chapter follows: a piecewise-linear Lyapunov function tailored to a structural network property (feedforward routing), and a linear one that works for an unrestricted network but is tailored to a specific control policy (head-of-line proportional service, HLSPS). Together they cover, as a corollary, the generalized Jackson network — the classical multiclass queueing network with one server per class — under ordinary non-idling FCFS.

Setting

A queueing network (Section 2.6, restated from mission IV) is feedforward (Definition 8.13) if its stations admit a numbering under which no station routes work to a lower-numbered one (feedback to the same station is still allowed). The workload operator $W(z) := AM(I-P')^{-1}z$ (Eq. 8.24) gives, for any buffer-contents vector $z$, the total service effort each pool would need to drain $z$ to emptiness with no further arrivals; the load vector of the standard load condition is $\rho = W(\lambda)$ (Eq. 8.25), and the total arrival rate vector $\alpha$ (including internally routed traffic) is the unique solution of the traffic equations $\alpha = \lambda + P'\alpha$. A queueing network under HLSPS control (Definition 8.17) splits each pool's capacity among its classes in fixed proportions $\gamma_i := \alpha_i m_i/\rho_{p(i)}$ (Eq. 8.30) — a policy general enough to reduce, for a generalized Jackson network (one class per pool), to ordinary non-idling FCFS.

Formalization targets

Goal: Theorem 8.18 — HLSPS control is stable under the standard load condition

For any queueing network under HLSPS control with proportion vector $\gamma$, if

$$\rho < b \qquad (\text{the standard load condition, Eq. 5.1}),$$

the corresponding fluid model is stable, and hence (Theorem 6.2) the network itself is stable under HLSPS control. This is the weaker of the two possible capstones only in the sense that it fixes one specific policy; it is chosen over Theorem 8.14 as the goal because it needs the full generality of the workload-based linear Lyapunov argument (Lemma 8.20) with no structural restriction on the network's routing, whereas Theorem 8.14 trades policy generality for a feedforward restriction.

Supporting milestones

Lemma 8.15 isolates the workload derivative identity $\dot W_k(Z(t)) = \rho_k - b_k$ at a busy station under any non-idling policy — the calculational engine both Theorem 8.14 and (via Lemma 8.20's analogous linear-potential argument) Theorem 8.18 rely on. Theorem 8.14 shows a feedforward network is stable under any non-idling policy, via a piecewise-linear Lyapunov function built from the routing matrix's block-triangular structure. Lemma 8.20 (numbered in the book but omitted from this mission's planning brief — added here, see STATUS.md) is the direct structural engine behind the goal theorem: a uniform excess departure rate over the total arrival rate at every non-empty class forces extinction. Corollary 8.19 specializes Theorem 8.18 to generalized Jackson networks, where HLSPS provably reduces to non-idling FCFS.

Significance

The result itself. Theorem 8.18 is the book's demonstration that dropping a structural network restriction (feedforward) is possible at the cost of committing to one specific, practically implementable control policy — and Corollary 8.19 shows this specific policy's stability theorem recovers, as a special case, the folklore stability result for the classical multiclass Jackson network under FCFS, arguably the single most studied queueing model in the field. Theorem 8.14, in turn, is the sharpest possible policy-agnostic statement: for feedforward networks, subcriticality alone (with no assumption at all beyond non-idling) suffices.

Formalizing it. Searches for "Jackson network" and "workload" (q=Jackson%20network, q=workload) return no relevant results (per triage.json); this mission is a from-scratch formalization of feedforward networks, the workload operator, HLSPS control, and their stability theorems, building directly on mission III's Theorem 6.2 and mission V's Lyapunov criteria.

Difficulty

Theorem 8.14's proof needs a genuinely delicate construction: a sequence of positive weights $\delta_k$, chosen via the routing matrix's block-triangular structure (guaranteed by feedforwardness) so that the piecewise-linear function $H(z) = \max_k \delta_k W_k(z)$ is positive-definite and has the right drift everywhere — an inductive argument over stations that does not generalize to non-feedforward networks, which is exactly why Theorem 8.18 needs an entirely different (linear, policy-specific) argument rather than a direct strengthening of 8.14's. A second, more subtle difficulty is that Theorem 8.14 and Theorem 8.18 are not related as special case and generalization in the book's own proof structure, despite their overlapping conclusions on feedforward networks under FCFS-like policies: 8.14 is agnostic to policy but needs feedforward structure, while 8.18 is agnostic to structure but needs the specific HLSPS policy — formalizing one as a corollary of the other would misrepresent the book's actual logical dependencies.

Formalization scope

Mission IV's queueing-network model data and fluid-equation specialization are restated locally (drafts in this series do not import one another). The workload operator's matrix inverse $(I-P')^{-1}$ is supplied as external data with its defining two-sided-inverse property, rather than derived from substochasticity/transience hypotheses on $P$ (Chapter 2 material, out of series scope) — the same convention mission III used for its process-family apparatus. The non-idling and HLSPS fluid models are each packaged as their own predicate plus a Definition-6.3-style stability specialization, and Corollary 8.19 deliberately reuses the non-idling stability object (not a separately restated "FCFS fluid model") since the book's own remark identifies the two exactly for generalized Jackson networks. A formalization that stated Theorem 8.14 as a corollary of Theorem 8.18, or vice versa, would misrepresent the chapter's actual proof architecture (see Difficulty); this mission keeps them as independent milestones/ goal, per BRIEF.md's own instruction. Lemma 8.20, numbered and within this chunk's page range but absent from the planning brief's disposition table, is added as a milestone rather than silently dropped, since it is the structural step the goal theorem's own proof cites by name. QueueingNetworkData, workloadOperator, IsFeedforward, and the non-idling/HLSPS fluid-model predicates are the primary reusable contributions; contributions completing the five by sorry proofs are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.
• M. Bramson, "Convergence to equilibria for fluid models of FIFO queueing networks," Queueing Systems 22 (1996), 5–45.

Motivation

Comparing uncertain outcomes is the basic problem of decision making under risk. Second-degree stochastic dominance (SSD) is the comparison that every risk-averse decision maker who prefers larger outcomes agrees with: $X$ dominates $Y$ in this sense exactly when $\mathbb E\,U(X)\ge\mathbb E\,U(Y)$ for every nondecreasing concave utility $U$ for which the expectations are finite. The relation grew out of majorization theory for finite distributions (Hardy, Littlewood and Pólya) and was extended to general distributions by Rothschild and Stiglitz and by Hadar and Russell around 1970; it is the standard consistency requirement for portfolio models and for risk measures in operations research and finance.

SSD is defined through the distribution function, which is awkward in optimization: portfolio returns are linear in the decision variables, but their distribution functions are not. Ogryczak and Ruszczyński (SIAM J. Optim. 13 (2002) 60–78) showed that SSD has an equivalent dual description through the integrated quantile function, the absolute Lorenz curve, and that the two descriptions are related by Fenchel conjugation. That dual description underlies the later theory of SSD-constrained optimization (Dentcheva and Ruszczyński, SIAM J. Optim. 14 (2003)) and the use of conditional value-at-risk as an SSD-consistent risk measure.

Setting

Fix a probability space $(\Omega,\mathcal B,\mathbb P)$ and real random variables $X,Y:\Omega\to\mathbb R$ with $\mathbb E|X|<\infty$, $\mathbb E|Y|<\infty$.

• The distribution function is $F_X(\eta)=\mathbb P\{X\le\eta\}$ (Lean: distFun P X).
• The second performance function is the area below it, $F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}F_X(\xi)\,d\xi$ (secondPerformance P X, eq. (2.1)).
• SSD: $X\succeq_{SSD}Y$ iff $F_X^{(2)}(\eta)\le F_Y^{(2)}(\eta)$ for every $\eta\in\mathbb R$ (SSD P X Y, eq. (2.2)). The dominating variable has the smaller curve.
• The first quantile function is the left-continuous inverse $F_X^{(-1)}(p)=\inf\{\eta:F_X(\eta)\ge p\}$, $0<p\le1$ (leftQuantile P X). A number $q$ is a $p$-quantile if $\mathbb P\{X<q\}\le p\le\mathbb P\{X\le q\}$ (IsPQuantile P X p q).
• The second quantile function (absolute Lorenz curve) $F_X^{(-2)}:\mathbb R\to\overline{\mathbb R}$ is $F_X^{(-2)}(p)=\int_0^pF_X^{(-1)}(\alpha)\,d\alpha$ for $0\le p\le1$ and $+\infty$ otherwise (secondQuantile P X, eq. (3.2)).
• The convex conjugate of $F:\mathbb R\to\overline{\mathbb R}$ is $F^*(p)=\sup_\xi\{p\xi-F(\xi)\}$ (conj F), and $\partial f(\eta)$ is the subdifferential of a real function $f$ at $\eta$ (subdiff f η).

Formalization targets

Goal: Theorem 3.2

$$X\succeq_{SSD}Y\iff F_X^{(-2)}(p)\ge F_Y^{(-2)}(p)\quad\text{for all }0\le p\le1.$$

Both directions are required, and the range of $p$ includes both endpoints (at $p=1$ the right-hand side contains $\mathbb EX\ge\mathbb EY$).

Milestones, in the order the argument uses them

1. (2.4): $F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}(\eta-\xi)\,P_X(d\xi)=\mathbb E\max(\eta-X,0)$.
2. §2, p. 62: $F_X^{(2)}$ is continuous, convex, nonnegative and nondecreasing.
3. §3, p. 64: for $p\in(0,1)$ the $p$-quantiles form a closed interval with left end $F_X^{(-1)}(p)$.
4. (3.3): $\partial F_X^{(2)}(\eta)=[\mathbb P\{X<\eta\},\mathbb P\{X\le\eta\}]$ for every $\eta$.
5. Theorem 3.1(i): $F_X^{(-2)}=[F_X^{(2)}]^*$ on all of $\mathbb R$.
6. Theorem 3.1(ii): $F_X^{(2)}=[F_X^{(-2)}]^*$ on all of $\mathbb R$.

A companion item, Corollary 3.3, states the four equivalent characterizations of a $p$-quantile (quantile condition, attainment in either conjugate, and the Fenchel–Young equality $F_X^{(-2)}(p)+F_X^{(2)}(\eta)=p\eta$).

Significance

Theorem 3.2 converts a condition on distribution functions into a condition on integrated quantiles. Its consequences in the paper include the SSD consistency of the mean–risk models built on tail means (conditional value-at-risk), on the Gini mean difference and on the mean absolute deviation from a quantile, and the linear-programming representations of those models for finitely many scenarios; the companion mission Dual Stochastic Dominance and Related Mean-Risk Models 2 builds on the same objects. Theorem 3.1 is the precise statement that $F_X^{(2)}$ and $F_X^{(-2)}$ form a conjugate pair; Corollary 3.3 identifies the subgradients of each with the quantiles of $X$.

All results here are proved in the paper, and the quantile characterization of the increasing concave order also appears in the stochastic-orders literature. None of them is formalized: Mathlib at the pinned revision has ProbabilityTheory.cdf but no convex conjugate on the extended reals, no subdifferential of a real function, no quantile function and no stochastic dominance. The mission produces a machine-checked account of the quantile side of SSD, with the conjugacy stated exactly, including the value $+\infty$ off $[0,1]$.

Difficulty

The naive route to Theorem 3.2 compares $F_X^{(2)}$ and $F_Y^{(2)}$ through the quantile functions directly, but the first quantiles $F^{(-1)}$ need not be ordered when $X\succeq_{SSD}Y$ (the paper notes this on p. 65), so no pointwise argument on quantiles works. The equivalence rests on Theorem 3.1, and there the hard part is computing the conjugate of $F_X^{(2)}$ for a general distribution: atoms of $X$ make $F_X^{(2)}$ nondifferentiable and flat pieces of $F_X$ make the maximizer non-unique, so the subdifferential (3.3) and the interval of $p$-quantiles must be handled as sets, and the endpoints $p=0,1$ (where the supremum need not be attained) and $p\notin[0,1]$ (where it is $+\infty$) must be treated separately. Part (ii) is a biconjugation statement for a closed convex function, whose general form is not in Mathlib.

Formalization scope

• One probability space (Ω, P) with [IsProbabilityMeasure P] carries both $X$ and $Y$; nothing depends on anything but the laws, and no independence is assumed.
• $F_X(\eta)$ is P.real {ω | X ω ≤ η}; $F_X^{(2)}$ is a Bochner integral over Set.Iic η; $F_X^{(-2)}$ is an interval integral over $(0,p]$, placed in EReal, with ⊤ off $[0,1]$.
• The conjugate is ⨆ ξ, ((p * ξ : ℝ) : EReal) - F ξ in the complete lattice EReal, so terms where $F=+\infty$ contribute $-\infty$, exactly the paper's convention.
• Standing assumption. Every item using $F^{(2)}$ or $F^{(-2)}$ assumes Integrable X P (and Integrable Y P in the goal). This is the paper's own hypothesis $\mathbb E|X|<\infty$ (p. 65, and the hypothesis of Theorem 3.1), not a repair. The $p$-quantile milestone assumes only AEMeasurable X P.
• Quantile at $p=1$. $F_X^{(-1)}$ is a real sInf. It is the true infimum for $0<p<1$; at $p=1$ the paper's value can be $+\infty$ while sInf ∅ = 0. This one point does not affect (3.2), and no item states anything about $F_X^{(-1)}(1)$.
• Omitted. The conditional-expectation form $\mathbb P\{X\le\eta\}\,\mathbb E\{\eta-X\mid X\le\eta\}$ in (2.4) is not stated, since it is undefined when $\mathbb P\{X\le\eta\}=0$.
• Trivializing encodings are ruled out. $F^{(2)}$ is defined by (2.1), not as $\mathbb E\max(\eta-X,0)$, and $F^{(-2)}$ by (3.2), not as a conjugate; either shortcut would make a milestone or Theorem 3.1 true by definition.
• Infrastructure and reuse. Welcome contributions: the extended-real conjugate and Fenchel–Young inequality on $\mathbb R$, biconjugation of closed convex functions of one variable, subdifferentials of integrals of monotone functions, and the basic theory of left quantiles (the quantile transform $F_X^{(-1)}(U)\sim X$). These are reusable beyond this mission, in particular by mission 2 of this series and by any formalization of conditional value-at-risk. The platform's VectorSpaceOpt.fenchel_biconjugate_on and ConvexOptimization.fenchelConjugate concern real-valued conjugates on other spaces and are related but not reused.

Selected references

• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13(1) (2002) 60–78. https://doi.org/10.1137/S1052623400375075
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Theorems 12.2 and 23.5 are used in the paper's proofs). https://doi.org/10.1515/9781400873173
• M. Rothschild, J. E. Stiglitz, Increasing risk: I. A definition, J. Econom. Theory 2 (1970) 225–243. https://doi.org/10.1016/0022-0531(70)90038-4
• J. Hadar, W. R. Russell, Rules for ordering uncertain prospects, Amer. Econom. Rev. 59 (1969) 25–34. https://www.jstor.org/stable/1811090
• D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM J. Optim. 14(2) (2003) 548–566. https://doi.org/10.1137/S1052623402420528
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

A logistic regression model is fitted on finitely many samples, and the quantity a practitioner cares about is the misclassification risk of the fitted classifier on new data. Its empirical counterpart, the training error, is biased downwards, and classical generalization bounds give it an additive margin that depends on a complexity measure of the model class rather than on the data at hand.

Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) take a distributionally robust route. They surround the empirical distribution of the training data by a ball of distributions in the Wasserstein metric and, for a given weight vector, compute the largest and the smallest misclassification probability over that ball. Their Theorem 3 shows that both extremes are optimal values of explicit linear programs. Combined with a measure-concentration result for the empirical distribution in the Wasserstein metric (Fournier and Guillin, PTRF 2015), the two values bracket the true risk with a prescribed confidence. The same Wasserstein-ball construction underlies the data-driven optimization framework of Mohajerin Esfahani and Kuhn (Math. Program. 2018).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and let labels take the values $y\in\{-1,+1\}$. The feature-label space is $\Xi = V\times\{-1,+1\}$ with points $\xi=(x,y)$. A weight vector $\beta$ acts on features by $x\mapsto\langle\beta,x\rangle$; its dual norm is $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$.

Metric (Definition 2). For a weight $\kappa>0$,

$$d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 .$$

Changing a label costs $\kappa$; moving a feature costs its norm distance.

Wasserstein distance (Definition 1). For distributions $\mathbb Q,\mathbb P$ on $\Xi$, $W(\mathbb Q,\mathbb P)$ is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$. The Wasserstein ball of radius $\varepsilon\ge0$ is $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$.

Data. Training samples $(\hat x_i,\hat y_i)$, $i=1,\dots,N$, define the empirical distribution $\hat{\mathbb P}_N = \frac1N\sum_{i=1}^N\delta_{(\hat x_i,\hat y_i)}$.

Classifier and risk. Logistic regression models $\operatorname{Prob}(y\mid x) = [1+\exp(-y\langle\beta,x\rangle)]^{-1}$ (eq. (1)). The classifier is $f_\beta(x)=+1$ if $\operatorname{Prob}(+1\mid x)>0.5$ and $-1$ otherwise, and its risk under the data-generating distribution $\mathbb P$ is $\mathfrak R(\beta) = \mathbb P[y\ne f_\beta(x)]$.

Worst- and best-case risks.

$$\mathfrak R_{\max}(\beta) = \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}\big],\qquad \mathfrak R_{\min}(\beta) = \inf_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}\big].$$

The worst case counts a nonpositive margin, the best case a strictly negative one.

The linear programs. For data $(\hat x_i,\hat y_i)$, a weight vector $\hat\beta$ and variables $\lambda\in\mathbb R$, $s,r,t\in\mathbb R^N$, program (10a) minimizes $\lambda\varepsilon + \frac1N\sum_i s_i$ subject to, for every $i$,

$$1 - r_i\hat y_i\langle\hat\beta,\hat x_i\rangle\le s_i,\quad 1 + t_i\hat y_i\langle\hat\beta,\hat x_i\rangle - \lambda\kappa\le s_i,\quad r_i\|\hat\beta\|_*\le\lambda,\quad t_i\|\hat\beta\|_*\le\lambda,\quad r_i,t_i,s_i\ge0 .$$

Program (10b) has the same objective and bounds, with the signs of the two margin terms exchanged.

Formalization targets

Goal: Theorem 3 (i)–(ii)

For every $\kappa>0$, $\varepsilon\ge0$, $N\ge1$, all samples and every weight vector $\hat\beta$, both programs attain their minima $v$ and $w$, and

$$\mathfrak R_{\max}(\hat\beta) = v,\qquad \mathfrak R_{\min}(\hat\beta) = 1-w .$$

The identities hold for each fixed $\hat\beta$, so they apply to any $\hat\beta$ computed from the data.

Milestone: Theorem 3(i) alone

$\mathfrak R_{\max}(\hat\beta)$ equals the minimum of (10a).

Milestones: the confidence clauses

If the training samples are i.i.d. from $\mathbb P$ and the radius is such that $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, then for any sample-dependent $\hat\beta$

$$\mathbb P^N\{\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-\eta,\qquad \mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\}\ge1-\eta,$$ $$\mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-2\eta .$$

Significance

The result. Theorem 3 replaces an optimization over an infinite-dimensional set of distributions by a linear program with $3N+1$ variables and $4N$ constraints plus sign constraints. That makes the worst- and best-case misclassification probabilities computable at the scale of the training set, for any norm on the features whose dual norm can be evaluated. With the confidence clauses, the two values are data-driven upper and lower confidence bounds on the out-of-sample risk of the classifier actually deployed, including one fitted on the same data.

Formalizing it. The paper states Theorem 3 without proof in the main text; the argument is deferred to a technical appendix. No part of it is machine-checked. A formal proof needs the evaluation of a worst-case probability of a closed set over a type-1 Wasserstein ball around a discrete distribution, and the analogous best-case probability of an open set. Both are reusable in any Wasserstein-robust treatment of chance constraints or classification error.

Difficulty

The objective $\mathbf 1_{\{y\langle\beta,x\rangle\le0\}}$ is neither continuous nor concave, so the duality theorems for Wasserstein balls stated for continuous or Lipschitz losses do not apply directly. Upper semicontinuity of the indicator of a closed set is what matters, and the strict inequality in $\mathfrak R_{\min}$ has to be handled as the complement of a closed set. The transport cost couples a norm on the features with a discrete label-flip cost, so a sample can reach the misclassification region either by moving its feature to the hyperplane $\langle\hat\beta,x\rangle=0$ or by flipping its label, and the two options interact through the shared budget $\varepsilon$. Distances to the hyperplane are measured in the given norm and produce the dual norm $\|\hat\beta\|_*$. The degenerate weight $\hat\beta=0$ (every point on the hyperplane) must come out correctly without any division by $\|\hat\beta\|_*$.

Formalization scope

The feature space is a finite-dimensional real normed space V with an arbitrary norm, standing for $(\mathbb R^n,\|\cdot\|)$; the Euclidean norm is not assumed. A weight vector is a continuous linear functional V →L[ℝ] ℝ, and $\|\hat\beta\|_*$ is its operator norm, which is exactly the dual norm. Labels are Bool with an explicit embedding $\text{true}\mapsto+1$, $\text{false}\mapsto-1$; the metric of Definition 2 is written literally. The Wasserstein distance is ℝ≥0∞-valued, probabilities and expectations of indicators are measure values in $[0,\infty]$, and suprema and infima range exactly over the probability measures in the ball. "min" in (10a)/(10b) is formalized as attainment (IsLeast) of the objective over the feasible set. Samples are indexed by Fin N with $N\ge1$.

The following choices differ from a literal reading of the page:

• The paper says the risk "can be expressed as" $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$. This fails on the hyperplane $\langle\beta,x\rangle=0$, where $f_\beta(x)=-1$ is correct for $y=-1$. The mission defines $\mathfrak R(\beta)=\mathbb P[y\ne f_\beta(x)]$ from (1) and includes the true statement $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}]\le\mathfrak R(\beta)\le\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$ as a helper item.
• The choice $\varepsilon=\varepsilon_N(\eta)$ of (8) and the measure-concentration theorem behind it (Theorem 2) are not formalized. The confidence clauses take their conclusion, $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, as a hypothesis, and "with probability $1-\eta$" is read as "with probability at least $1-\eta$". The printed level $1-2\eta$ is kept for the two-sided bound.

Swapping the strict and non-strict inequalities in $\mathfrak R_{\max}$ and $\mathfrak R_{\min}$, restricting the supremum to measures supported on the sample points, or replacing the ball by a set that excludes non-discrete distributions would each change the theorem. None of these is an acceptable reformulation of the goal.

Useful infrastructure: couplings of a discrete measure with an arbitrary one, the distance from a point to a closed half-space in a general norm, and LP-duality arguments for fractional-knapsack-type programs. Proofs of the helper and confidence items, and any reusable lemma about worst-case probabilities of closed sets over Wasserstein balls, are welcome.

Selected references

• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://papers.nips.cc/paper/2015/hash/cc1aa436277138f61cda703991069eaf-Abstract.html
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://doi.org/10.1007/s00440-014-0583-7
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018). https://doi.org/10.1007/s10107-017-1172-1

Motivation

Deciding whether a graph has a perfect matching, and finding one, are basic problems of combinatorial optimization; Edmonds' blossom algorithm solves them sequentially in polynomial time. The question behind this paper is whether they can also be solved in parallel, in polylogarithmic time on polynomially many processors (the class NC, or RNC when random bits are allowed).

The algebraic route to that question goes through the Tutte matrix. Tutte (1947) showed that a graph has a perfect matching if and only if its Tutte matrix, a skew-symmetric matrix of indeterminates, has a nonzero determinant. Substituting random numbers for the indeterminates turns this into a randomized parallel decision procedure, but it does not say which perfect matching exists, and a graph may have exponentially many.

Mulmuley, Vazirani and Vazirani (Combinatorica 7 (1987) 105–113) resolve this with the isolating lemma: random small integer weights make the minimum weight member of an arbitrary set family unique with probability at least one half. Once a single perfect matching is isolated, one determinant and one adjugate of an integer matrix reveal it. The isolating lemma has since become a standard tool in randomized algorithms and complexity theory, well beyond matchings.

Timeline:

• 1947, Tutte: a graph has a perfect matching iff the determinant of its Tutte matrix is a nonzero polynomial (doi:10.1112/jlms/s1-22.2.107).
• 1979, Lovász: random substitution into the Tutte matrix gives a randomized algorithm for deciding whether a perfect matching exists (Fundamentals of Computation Theory, LNCS 1979).
• 1986, Karp, Upfal and Wigderson: the first RNC algorithm that finds a perfect matching, with RNC³ running time (Combinatorica 6 (1986) 35–48).
• 1987, Mulmuley, Vazirani and Vazirani: the isolating lemma and an RNC² algorithm that inverts one integer matrix (this paper).
• 2016–2017, Fenner, Gurjar and Thierauf (arXiv:1601.06319) for bipartite graphs, and Svensson and Tarnawski (arXiv:1704.01929) for general graphs, partially derandomize the isolation step and place perfect matching in quasi-NC. Whether perfect matching is in NC remains open.

Setting

A set system $(S, F)$ is a finite set $S$ of elements together with a family $F$ of subsets of $S$. Given a weight $w_x \in \mathbb{N}$ for each element $x$, the weight of $T \subseteq S$ is $w(T) = \sum_{x \in T} w_x$, and $F$ has a unique minimum weight set if one member of $F$ is strictly lighter than every other member.

A graph $G$ has vertices $v_1, \dots, v_n$ (in Lean, Fin n, in their natural order) and edge set $E$, with $m = |E|$. A perfect matching is a set $M \subseteq E$ such that every vertex lies in exactly one edge of $M$. The edges and the perfect matchings of $G$ form a set system.

Given edge weights $w_{ij} \in \mathbb{N}$, the integer matrix $B$ is obtained from the Tutte matrix by substituting $2^{w_{ij}}$ for its indeterminates:

$$b_{ij} = 2^{w_{ij}} \ \text{if } (v_i, v_j) \in E,\ i < j; \qquad b_{ij} = -2^{w_{ij}} \ \text{if } (v_i, v_j) \in E,\ i > j; \qquad b_{ij} = 0 \ \text{otherwise}.$$

$|B|$ is its determinant, $B_{ij}$ the submatrix with row $i$ and column $j$ removed, and $\operatorname{adj}(B)$ its adjugate, whose $(j, i)$ entry is $\pm|B_{ij}|$.

The algorithm of §4 is:

1. Step 1. Compute $|B|$ and obtain $w$, the exponent for which $2^{2w}$ is the highest power of 2 dividing $|B|$.
2. Step 2. Compute $\operatorname{adj}(B)$.
3. Step 3. Output every edge $(v_i, v_j)$ for which the integer $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.

Formalization targets

Goal: Steps 1–3 find a minimum weight perfect matching with probability at least 1/2

For every graph $G$ that has a perfect matching, with edge weights drawn uniformly and independently from $\{1, \dots, 2m\}$,

$$\Pr\bigl[\text{the output of Steps 1–3 is a perfect matching of } G \text{ of minimum weight}\bigr] \ \ge\ \tfrac12 .$$

This is the correctness half of the paper's Theorem (p. 109). The probability is a fraction of the $(2m)^m$ weight functions.

Milestones

1. Lemma 1 (isolating lemma): for a nonempty family $F$ over an $n$-element set, weights uniform in $[1, 2n]$ give a unique minimum weight set with probability $\ge 1/2$.
2. Isolation for perfect matchings (§4): with edge weights uniform in $[1, 2m]$, the minimum weight perfect matching is unique with probability $\ge 1/2$.
3. Odd-cycle cancellation (proof of Lemma 2): for a skew-symmetric integer matrix, only permutations all of whose cycles have even length contribute to the determinant.
4. Lemma 2: if the minimum weight perfect matching is unique, of weight $w$, then $|B| \neq 0$ and $2^{2w}$ is the highest power of 2 dividing $|B|$.
5. Lemma 3: under the same hypothesis, $(v_i, v_j) \in M$ iff $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.
6. Steps 1–3, deterministic core: under the same hypothesis, Step 1 obtains the weight of $M$ and Steps 2–3 output exactly $M$.

Two companion items are included but are not on the goal's path: the maximum weight version of Lemma 1 (the remark after its proof, p. 107) and Lemma 4 (p. 110): the lexicographically largest matching set, for vertices sorted by decreasing weight, is a heaviest matching set.

Significance

The isolating lemma is a statement about arbitrary set families with no structure assumed, which is why it transfers: it is used for isolating satisfying assignments, for parallel algorithms for exact matching and minimum weight matchings with small weights, and in the derandomization program that led to the quasi-NC matching algorithms cited above. Lemmas 2 and 3 are the bridge from a combinatorial object (a unique minimum weight perfect matching) to arithmetic facts about one integer matrix (2-adic valuations of its determinant and adjugate entries), which is what makes the algorithm reducible to matrix inversion.

All results of this mission are proved in the paper. What the mission adds is machine-checked proofs: Mathlib at the pinned revision contains Tutte's barrier theorem but neither the isolating lemma nor the Tutte-matrix determinant arguments, and a search of Prove2Me (September 2026) found no formalization of them. A complete development yields a reusable isolating lemma for finite set systems and a reusable determinant expansion for skew-symmetric matrices.

Difficulty

The probabilistic step is a union bound over elements, but the event bounded for each element, "the element is ambiguous", is defined through a threshold that depends on all the other weights; the argument needs independence of that threshold from the element's own weight, which is a product-space (Fubini-type) counting statement rather than a one-line estimate. In a counting formalization over $\{1, \dots, 2n\}^S$, each fibre must be handled separately.

The determinant steps require a genuine combinatorial involution on permutations: reversing an odd cycle must be well defined (a canonical choice of cycle) and self-inverse, preserve the sign, negate the value, and in Lemma 3 also preserve the constraint $\sigma(i) = j$, which is where "since $n$ is even, there are at least two odd cycles" enters. Relating a permutation with only even cycles to a pair of perfect matchings whose union is its trail is the second nontrivial bijection. Divisibility must be tracked exactly: $2^{2w}$ divides every term, and every term other than the one of $M$ is divisible by $2^{2w+1}$.

Formalization scope

Vertices are Fin n and the graph is G : SimpleGraph (Fin n) with decidable adjacency. Edge weights are functions G.edgeSet → ℕ; perfect matchings are Finset G.edgeSet in which every vertex lies in exactly one edge. The matrix is weightedTutteMatrix G w : Matrix (Fin n) (Fin n) ℤ, with the positive entry above the diagonal. Probabilities are ratios of counts over Fintype.piFinset (fun _ => Finset.Icc 1 (2m)), stated without division as $(2m)^m \le 2 \cdot \#\{\dots\}$; the weight range is exactly $[1, 2m]$ (resp. $[1, 2n]$ in Lemma 1). "$x/2^k$ is odd" means $2^k \mid x$ and $x/2^k$ is an odd integer. The minor $|B_{ij}|$ is taken as Mathlib's signed cofactor adjugate B j i; parity and divisibility do not see the sign. Step 1's $w$ is $\lfloor \nu_2(|B|)/2\rfloor$.

Added hypotheses: Lemma 1 and its maximum version assume $F$ nonempty (the printed lemma omits it and is false for $F = \emptyset$); the goal and the isolation milestone assume $G$ has a perfect matching, which is the paper's own input assumption. Lemmas 2 and 3 allow arbitrary natural weights, as printed.

The algorithm's output is defined from $B$, $|B|$, $\operatorname{adj}(B)$, the 2-adic valuation and parity only; a definition of the output that refers to perfect matchings or to minimality would trivialize the goal and is ruled out. The complexity half of the Theorem (RNC², $O(n^{3.5}m)$ processors), which rests on Pan's matrix-inversion algorithm, is not formalized, nor are §5a–b and §6.

Contributions welcome: proofs of the milestones in any order, general lemmas about the permutation expansion of skew-symmetric determinants, and a counting form of the union bound over product spaces, all of which are reusable outside this mission.

Selected references

• K. Mulmuley, U. V. Vazirani, V. V. Vazirani, Matching is as easy as matrix inversion, Combinatorica 7(1) (1987) 105–113. https://doi.org/10.1007/BF02579206
• W. T. Tutte, The factorization of linear graphs, J. London Math. Soc. 22 (1947) 107–111. https://doi.org/10.1112/jlms/s1-22.2.107
• R. M. Karp, E. Upfal, A. Wigderson, Constructing a perfect matching is in random NC, Combinatorica 6(1) (1986) 35–48. https://doi.org/10.1007/BF02579407
• L. Lovász, On determinants, matchings, and random algorithms, Fundamentals of Computation Theory (FCT '79), 1979, 565–574.
• S. Fenner, R. Gurjar, T. Thierauf, Bipartite perfect matching is in quasi-NC, STOC 2016. https://arxiv.org/abs/1601.06319
• O. Svensson, J. Tarnawski, The matching problem in general graphs is in quasi-NC, FOCS 2017. https://arxiv.org/abs/1704.01929

Motivation

Classifiers trained by standard methods can be fooled by small, carefully chosen perturbations of their inputs. Adversarial training reduces this vulnerability on the training set, but on image benchmarks such as CIFAR10 the robust accuracy on held-out data remains far below the training accuracy. Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285) asked whether this gap is a failure of current algorithms or an intrinsic statistical phenomenon, and answered it in two simple data models: learning a classifier that is robust to $\ell_\infty$-bounded perturbations can require provably more samples than learning a classifier with small standard error.

The paper's separation has two halves in its Gaussian model. The lower half (every learner needs many samples) is the subject of the companion mission Adversarially Robust Generalization Requires More Data 1. This mission formalizes the upper half: a concrete, simple estimator reaches small robust error once the number of samples is of order $\varepsilon^2\sqrt d$, so the lower bound is tight up to logarithmic factors.

Setting

Write $\langle\cdot,\cdot\rangle$ and $\|\cdot\|_2$ for the Euclidean inner product and norm on $\mathbb R^d$, and $\|v\|_\infty=\max_i|v_i|$. Labels are $y\in\{\pm1\}$.

The $(\theta^\star,\sigma)$-Gaussian model (Definition 1) is the distribution of a pair $(x,y)\in\mathbb R^d\times\{\pm1\}$ obtained by drawing the label $y$ uniformly at random and then the point $x$ from the spherical Gaussian $\mathcal N_d(y\,\theta^\star,\sigma^2I)$, where $\theta^\star\in\mathbb R^d$ is the per-class mean and $\sigma>0$ the standard deviation of each coordinate. The paper works in the regime $\|\theta^\star\|_2=\sqrt d$, which every statement of this mission assumes explicitly.

A classifier is a map $f:\mathbb R^d\to\{\pm1\}$. Its classification error (Definition 2) under a distribution $\mathcal P$ is $\mathbb P_{(x,y)\sim\mathcal P}[f(x)\ne y]$. Given the perturbation set $\mathcal B_\infty^\varepsilon(x)=\{x':\|x'-x\|_\infty\le\varepsilon\}$, its $\ell_\infty^\varepsilon$-robust classification error (Definition 3) is

$$\mathbb P_{(x,y)\sim\mathcal P}\big[\exists\,x'\in\mathcal B_\infty^\varepsilon(x):\ f(x')\ne y\big].$$

The $\ell_p^\varepsilon$-robust error is defined the same way with the $\ell_p$ ball, and $\|w\|_p^*=\sup\{\langle w,v\rangle:\|v\|_p\le1\}$ is the dual norm.

For $w\in\mathbb R^d$ the linear classifier is $f_w(x)=\operatorname{sgn}\langle w,x\rangle$. The estimator studied here is built from $n$ i.i.d. samples $(x_1,y_1),\dots,(x_n,y_n)$ of the model: the class-weighted sample mean

$$\bar z=\frac1n\sum_{i=1}^ny_ix_i,\qquad \widehat w=\frac{\bar z}{\|\bar z\|_2},$$

and the classifier is $f_{\widehat w}$.

Formalization targets

Goal: Corollary 22

If $\|\theta^\star\|_2=\sqrt d$ and $\sigma\le\frac1{32}d^{1/4}$, then with probability at least $1-2\exp\!\big(-\frac{d}{8(\sigma^2+1)}\big)$ over the sample, $f_{\widehat w}$ has $\ell_\infty^\varepsilon$-robust classification error at most $0.01$ provided

$$n\ge\begin{cases}1 & \varepsilon\le\frac14d^{-1/4},\\ 64\,\varepsilon^2\sqrt d & \frac14d^{-1/4}\le\varepsilon\le\frac14.\end{cases}$$

The general bound: Theorem 21

For every $\beta>0$ and every $\varepsilon\le\frac{2\sqrt n-1}{2\sqrt n+4\sigma}-\frac{\sigma\sqrt{2\log(1/\beta)}}{\sqrt d}$, with the same probability the $\ell_\infty^\varepsilon$-robust error of $f_{\widehat w}$ is at most $\beta$.

Milestones on the way

The milestones follow the paper's Appendix A.1: Fact 12 (Gaussian norm tail); Lemmas 13 and 14 (norm of a Gaussian sample mean); Lemma 15 (inner product of the sample mean with the mean); Lemma 16 (alignment $\langle\widehat w,\mu\rangle\ge\frac{2\sqrt n-1}{2\sqrt n+4\sigma}\sqrt d$ with high probability); Lemma 17 (Gaussian margin tail for a fixed unit vector); Lemma 20 (the $\ell_p^\varepsilon$-robust error of a fixed linear classifier, for every $p\in[1,\infty]$); and Theorem 21. The mission also contains Theorem 18, the corresponding standard-generalization bound, as a companion item.

Significance

The result. Corollary 22 shows that the $\ell_\infty$ lower bound of the paper is essentially attained by an elementary estimator: in the regime $\sigma\approx d^{1/4}$ a single sample gives small standard error, while $\ell_\infty$-robustness at level $\varepsilon$ is obtained with $O(\varepsilon^2\sqrt d)$ samples, matching the lower bound $\Omega(\varepsilon^2\sqrt d/\log d)$ up to a logarithm. The separation between standard and robust sample complexity is therefore a property of the data distribution and not of a weak learning procedure. Lemma 20 is of independent use: it gives the exact form of the robust error of any linear classifier in a Gaussian model for every $\ell_p$ adversary.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. A formalization produces a checked instance of a statistical-versus-robust separation, and along the way checked versions of dimension-explicit Gaussian tail bounds (norm and inner-product tails of sample means) that Mathlib states only in partial form.

Difficulty

The estimator is explicit, so the difficulty is analytic and quantitative. Two obstacles stand out. First, the robust error involves a supremum over an uncountable perturbation set for every test point, so it is not a margin probability until the worst case over the $\ell_p$ ball has been identified exactly; any slack there changes the constants. Second, the estimator $\widehat w$ is random, and its alignment with $\theta^\star$ depends on two concentration events at once, a norm upper bound and an inner-product lower bound, with dimension-explicit constants. Generic sub-Gaussian bounds with unspecified constants, the usual first attempt, do not yield the stated $0.01$, $64$ and $1/32$: the constants have to be tracked through the final numerical case analysis. Gaussian norm concentration in the dimension-free form of Fact 12 is not available in Mathlib.

Formalization scope

Everything is stated in the namespace RobustGeneralization.GaussUpper. The data space is EuclideanSpace ℝ (Fin d); labels are Bool with true $=+1$. $\mathcal N_d(m,s^2I)$ is the push-forward of Mathlib's stdGaussian under $v\mapsto m+s\,v$, with $s$ the standard deviation (Definition 1 calls $\sigma$ the "variance parameter" but samples from $\mathcal N(y\theta^\star,\sigma^2I)$). The model is a measure on $\mathbb R^d\times\{\pm1\}$ and the errors are literally the measures of the events of Definitions 2–3; since the robust event need not be Borel, the measure of it is its outer measure, i.e. its probability under the completed measure. The $\ell_\infty$ ball is written coordinatewise. The linear classifier labels the tie $\langle w,x\rangle=0$ as $+1$; no statement depends on this. $\widehat w$ is $\|\bar z\|_2^{-1}\bar z$, equal to $0$ on the null event $\bar z=0$. The $n$ samples are a product measure on Fin n → ℝ^d × Bool.

"With probability at least $1-q$ the error is at most $\beta$" is stated as an upper bound on the probability of the failure set, which is the strong form under outer measures.

Added hypotheses, each disclosed in its item: $t\ge0$ (Fact 12), $n\ge1$ (Lemmas 13, 15 and Theorem 18), $\mu\ne0$ (Lemma 15, false as printed at $\mu=0$), and $\beta>0$ (Theorem 21). The constants $1/32$, $1/4$, $64$, $0.01$, $2$ and $8(\sigma^2+1)$ are kept exactly.

A formalization that states the robust error bound for a fixed unit vector instead of the estimator $\widehat w$, that replaces the robust error by its closed-form margin expression, or that uses the $\ell_2$ ball instead of the $\ell_\infty$ ball, proves a different and weaker statement and is excluded.

A complete development needs: Gaussian concentration for Lipschitz functions (or a direct $\chi$-type tail for $\|z\|_2$), the law of a sample mean of Gaussian vectors and of a one-dimensional projection of a spherical Gaussian, and the dual-norm identity for linear functionals over $\ell_p$ balls. These pieces are reusable beyond this mission. Proofs of any milestone, and reusable lemmas on spherical Gaussians under stdGaussian, are welcome. Related platform work: the other missions of this series, Adversarially Robust Generalization Requires More Data 1, 2 and 4.

Selected references

• L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, arXiv:1804.11285v2, 2018 (NeurIPS 2018). https://arxiv.org/abs/1804.11285
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013 (Example 5.7 is the source of Fact 12). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001