Optimization

Motivation

Matroids and their integral generalizations, integral base polytopes, are the combinatorial structures on which the greedy algorithm is exact. Edmonds' theory relates them to submodular and supermodular set functions: a polytope is a base polytope exactly when its support function, restricted to $0/1$ vectors, is supermodular and the greedy formula evaluates it everywhere. Dress and Wenzel's valuated matroids (1990) and Murota's M-concave functions carry the exchange axiom from sets to functions on sets. This paper (Adv. Math. 124, 1996) sets up the resulting theory of discrete concave functions on base sets, later developed into discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003).

The question behind this mission is how the set-level correspondence between exchange and supermodularity extends to functions. Section 5 of the paper answers it with the Local Supermodularity Theorem: the exchange property of a function is a supermodularity property of its concave conjugate, holding locally at every point.

Setting

Let $V$ be a finite nonempty set, $n=|V|$. For $u\in V$ let $\chi_u\in\mathbb Z^V$ be the unit vector, for $X\subseteq V$ let $\chi_X$ be its characteristic vector, $x(X)=\sum_{v\in X}x(v)$, and $\langle p,x\rangle=\sum_v p(v)x(v)$. For a finite $B\subseteq\mathbb Z^V$, $\overline B$ is its convex hull.

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that

$$\text{(B1)}\quad x,y\in B,\ u\in\operatorname{supp}^+(x-y)\ \Rightarrow\ \exists v\in\operatorname{supp}^-(x-y):\ x-\chi_u+\chi_v\in B.$$

A function $\omega:B\to\mathbb R$ satisfies the exchange property (EXC) (is M-concave) if for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ there is $v\in\operatorname{supp}^-(x-y)$ with $x-\chi_u+\chi_v,\ y+\chi_u-\chi_v\in B$ and $\omega(x)+\omega(y)\le\omega(x-\chi_u+\chi_v)+\omega(y+\chi_u-\chi_v)$. Write $\omega[p](x)=\omega(x)+\langle p,x\rangle$ and $\operatorname{argmax}(g)$ for the maximizers of $g$ on $B$.

The support function of $B$ is $\psi^\circ(p)=\min\{\langle p,x\rangle\mid x\in B\}$. A positively homogeneous $h:\mathbb R^V\to\mathbb R$ is "matroidal" if

• (C1) $X\mapsto h(\chi_X)$ is supermodular, and
• (C2) $h(p)=\sum_{j=1}^n(p_j-p_{j+1})\,h(\chi_{V_j})$ whenever $V=\{v_1,\dots,v_n\}$ with $p(v_1)\ge\dots\ge p(v_n)$, $p_j=p(v_j)$, $V_j=\{v_1,\dots,v_j\}$, $p_{n+1}=0$.

The concave conjugate is $\omega^\circ(p)=\min\{\langle p,x\rangle-\omega(x)\mid x\in B\}$, the concave closure is $\hat\omega(b)=\inf_p\{\langle p,b\rangle-\omega^\circ(p)\}$, the subdifferential is $\partial\omega^\circ(p_0)=\{b\mid\omega^\circ(p)-\omega^\circ(p_0)\le\langle p-p_0,b\rangle\ \forall p\}$, and the localization of $\omega^\circ$ at $p_0$ is $\hat L(\omega^\circ,p_0)(p)=\inf\{\langle p,b\rangle\mid b\in\partial\omega^\circ(p_0)\}$.

Formalization targets

Goal: the Local Supermodularity Theorem (Theorem 5.3, corrected)

For $\omega$ on a finite integral base set $B$,

$$\omega\ \text{satisfies (EXC)}\iff\Big(\omega=\hat\omega\ \text{on}\ B\Big)\ \text{and}\ \Big(\hat L(\omega^\circ,p_0)\ \text{is "matroidal" for every}\ p_0\in\mathbb R^V\Big).$$

The printed Theorem 5.3 has only the second condition on the right. Its "only if" direction holds as printed; its "if" direction is false without the first condition, and a separate item of the mission states the counterexample: $B=\{(2,0),(1,1),(0,2)\}$, $\omega=(0,-10,0)$.

Milestones

1. Theorem 2.1: (B1) is equivalent to $B$ being the integer points of an integral submodular (equivalently, supermodular) system, whose defining function is determined by $B$.
2. Theorem 5.1: if $B=\mathbb Z^V\cap\overline B$, then $B$ satisfies (B1) iff $\psi^\circ$ is "matroidal".
3. Lemma 5.2: sums of "matroidal" functions are "matroidal".
4. Theorem 4.4: (EXC) holds iff every $\operatorname{argmax}(\omega[p])$ satisfies (B1).
5. Eq. (5.12): $\hat L(\omega^\circ,p_0)(p)=\min\{\langle p,x\rangle\mid x\in\operatorname{argmax}(\omega[-p_0])\}$.

Significance

The result. Theorem 5.3 is the function-level version of Theorem 5.1. Condition (C1) is a supermodularity condition, so the theorem expresses (EXC) as "a collection of local supermodularity" properties of $\omega^\circ$, in the same way that (B1) corresponds to supermodularity of a support function. In the paper this characterization of the conjugate side underlies the Fenchel-type duality of Section 6, and more generally the conjugacy between M-concave and L-convex functions in discrete convex analysis.

The formalization. No part of this theory is formalized in Lean or on this platform: base sets, (EXC), "matroidal" functions and concave conjugates of functions on base sets are all new. The mission also corrects the published statement: the reduction from localizations to base sets needs every integer point of $\operatorname{conv}(\operatorname{argmax}\,\omega[-p_0])$ to be a maximizer, and the concave-closure condition supplies this. A machine-checked proof would settle both the corrected theorem and the counterexample. Theorem 2.1 and Lemma 5.2 are classical but have no formal proof either.

Difficulty

$\omega^\circ$ depends only on the concave closure $\hat\omega$, so any characterization of (EXC) through $\omega^\circ$ alone cannot see values of $\omega$ below $\hat\omega$. That is why the goal needs the extra clause. The "only if" direction needs the full theory of Section 4: M-concave functions coincide with their concave closure, and all their maximizer sets are base sets. Theorem 5.1 needs the greedy algorithm on integral base polytopes, together with the fact that the base polytope of an integral supermodular function has integral vertices. Theorem 2.1 is the folklore statement that polyhedral and exchange descriptions agree, and the paper does not prove it. Eq. (5.12) needs the subdifferential of a finite minimum of affine functions to be the convex hull of the active gradients, stated globally rather than only near $p_0$.

Formalization scope

Integer vectors are V → ℤ, real vectors V → ℝ, with [Fintype V] [DecidableEq V] [Nonempty V]. A finite subset of $\mathbb Z^V$ is a Finset (V → ℤ). A function on $B$ is a total function (V → ℤ) → ℝ whose values off $B$ are never used. The mission commits to the following readings:

• Minima. $\psi^\circ$, $\omega^\circ$ are real infima over the finite set $B$, hence minima for nonempty $B$ (every statement has $B$ nonempty). $\hat\omega$ is a real infimum used only at points of $B$, where it is bounded below.
• Localization. $\hat L$ is a real sInf over the subdifferential, defined by (5.8)–(5.9) exactly, not by the formula (5.12). Eq. (5.12) is stated with IsLeast, so it asserts attainment, not just the value.
• (C2). It is required for every bijection Fin n ≃ V along which $p$ is non-increasing. This is equivalent to "for some" such indexing. "Matroidal" includes positive homogeneity but not concavity.
• Theorem 2.1. The page's "$\forall X\subset V$" is read as all $X\subseteq V$. The set functions are integer-valued, and "Moreover" is read strongly: every $f$ (resp. $g$) as in (b) (resp. (c)) equals the displayed max (resp. min).
• Theorem 4.4. "$\overline{\operatorname{argmax}(\omega[p])}$ is an integral base polytope" is read as "$\operatorname{argmax}(\omega[p])$ satisfies (B1)", following Lemma 4.3 and the proof of Theorem 5.3. The literal convex-hull reading makes the "if" direction false (same counterexample).
• Theorem 5.1 keeps the page's hypothesis $B=\mathbb Z^V\cap\overline B$.

Trivializing formalizations are ruled out. Defining $\hat L$ by (5.12) would reduce the goal to Theorems 4.4 and 5.1. A "matroidal" without (C2) would be satisfied by support functions of non-base sets. An $\omega^\circ$ taken as a supremum would reverse the sign conventions.

The development needs: the greedy algorithm and integrality for integral base polytopes, supergradients of polyhedral concave functions, and the Section 4 results of the paper (concave closure of M-concave functions, Lemma 4.3). The base-set and "matroidal" layers can be reused beyond this mission. Proofs of any milestone, of the counterexample, and a proof of the "only if" direction on its own are all welcome.

Selected references

• K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996), 272–311. https://doi.org/10.1006/aima.1996.0084
• A. W. M. Dress, W. Wenzel, Valuated matroids: a new look at the greedy algorithm, Applied Mathematics Letters 3 (1990), 33–35.
• S. Fujishige, Submodular Functions and Optimization, 2nd ed., Annals of Discrete Mathematics 58, Elsevier, 2005.
• L. Lovász, Submodular functions and convexity, in Mathematical Programming: The State of the Art, Springer, 1983, 235–257. https://doi.org/10.1007/978-3-642-68874-4_10
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

The problem of solving linear inequalities

The linear feasibility problem takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns

$$\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset$$

has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.

What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$. In the real-number model the input is a list of $mn + m$ exact real numbers, each arithmetic operation ($+, -, \times, \div$), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$. An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every $m$, $n$, and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.

Why it matters

For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$, covering network flows and all $\{0,\pm1\}$-constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).

For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.

The question and what is known

$$\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}$$

The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).

Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.

Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of $A$ alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.

The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).

A hierarchy of formalization targets

The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.

Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:

$$\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.$$

It fixes nothing about $n \ge 2$; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.

Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of

$$2^n - 1 \text{ pivots}$$

from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.

Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$, every admissible ellipsoid run decides feasibility within

$$t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.$$

The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$.

Level 3 — the goal (open). A uniform program with data-independent polynomial cost:

$$\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.$$

The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.

Formalization scope

Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with $\{x \mid Ax \ge b\}$ as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$; both are benign for the class of programs quantified over.

The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.

Selected references

• L. Blum, M. Shub, S. Smale, On a theory of computation and complexity over the real numbers, Bull. AMS 21(1):1–46, 1989. DOI
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2):7–15, 1998. DOI
• V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, pp. 159–175.
• L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20:53–72, 1980. DOI
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4:373–395, 1984. DOI
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40:59–93, 1988. DOI
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Oper. Res. 34(2):250–256, 1986. DOI
• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. DOI
• G. Kalai, A subexponential randomized simplex algorithm, STOC 1992. DOI
• O. Friedmann, T. D. Hansen, U. Zwick, Subexponential lower bounds for randomized pivoting rules for the simplex algorithm, STOC 2011. DOI
• D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. DOI
• S. A. Vavasis, Y. Ye, A primal-dual interior point method whose running time depends only on the constraint matrix, Math. Programming 74:79–120, 1996. DOI
• Y. Ye, The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate, Math. Oper. Res. 36(4):593–603, 2011. DOI
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. DOI
• X. Allamigeon, S. Gaubert, N. Vandame, No self-concordant barrier interior point method is strongly polynomial, STOC 2022. arXiv
• D. Dadush, S. Huiberts, B. Natura, L. A. Végh, A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix, STOC 2020. arXiv
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the Introduction to Linear Optimization mission series).
• B. Korte, J. Vygen, Combinatorial Optimization: Theory and Algorithms, 6th ed., Springer, 2018, §4.1–4.5.

Why variance-regularized risk bounds

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

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

Setting

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

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

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

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

Formalization targets

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

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

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

Milestones

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
• P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
• O. Bousquet, A Bennett concentration inequality and its application to suprema of empirical processes, Comptes Rendus Mathématique 334(6), 2002. https://doi.org/10.1016/S1631-073X(02)02292-6
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT 2009. https://arxiv.org/abs/0907.3740
• M. Ledoux and M. Talagrand, Probability in Banach Spaces, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4

Motivation

Many engineering and economic planning problems must meet random requirements with a prescribed reliability: a reservoir must satisfy demand with probability at least $0.95$, a power system must cover load except on rare days, an inventory must avoid shortage with high probability. Probabilistic constrained programming (also called chance-constrained programming) models this by requiring that a system of random inequalities hold jointly with probability at least $p$.

The first obstacle to solving such problems is structural. The probability that random constraints are satisfied is, in general, neither concave nor convex in the decision, so the feasible set need not be convex and local search can stall. Prékopa's theory of logarithmically concave measures (1971–1973) removed that obstacle for a large class of distributions, and it is the basis of the numerical methods of Chapter 5 of Ermoliev and Wets, Numerical Techniques for Stochastic Optimization (Springer 1988). This mission formalizes the structural theorems of that chapter.

Timeline:

• 1959: Charnes and Cooper, individual chance constraints.
• 1971: Prékopa, logarithmic concave measures with application to stochastic programming (Acta Sci. Math. Szeged 32).
• 1973: Prékopa, logarithmic concave measures and functions (Acta Sci. Math. Szeged 34), containing the marginal theorem: marginals of log-concave functions are log-concave.
• 1970s–1980s: nonlinear programming methods for (5.1) (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) combined with Monte Carlo evaluation of $h_0$; the chapter surveys them.

Setting

Let $\xi$ be a random vector in $\mathbb R^q$ on a probability space $(\Omega, \mathcal F, P)$ and let $g_1, \dots, g_r : \mathbb R^n \times \mathbb R^q \to \mathbb R$. The chapter studies problem (5.1):

$$\min h(x) \quad \text{s.t.} \quad h_0(x) = P\bigl(g_1(x,\xi) \ge 0, \dots, g_r(x,\xi) \ge 0\bigr) \ge p, \quad h_1(x) \ge p_1, \dots, h_m(x) \ge p_m .$$

The function $h_0$ is the probability function (chanceProb in Lean). In the special case $g_i(x,y) = T_i x - y_i$ it equals $F(Tx)$, where $F$ is the joint distribution function of $\xi$.

A function $f \ge 0$ is logarithmically concave on a convex set $S$ if

$$f(\lambda u + (1-\lambda) v) \ge f(u)^{\lambda} f(v)^{1-\lambda}, \qquad u, v \in S,\ 0 < \lambda < 1 .$$

Where $f > 0$ this is concavity of $\log f$; the power form also makes sense where $f = 0$. Nondegenerate normal densities, uniform densities on convex bodies and exponential densities are log-concave.

Section 5.7 introduces the polynomial distribution (5.19) on the cube $0 < z_j \le 1$:

$$F(z_1, \dots, z_n) = \frac{1}{\sum_{i=1}^{N} c_i z_1^{\alpha_{i1}} \cdots z_n^{\alpha_{in}}}, \qquad c_i > 0,\ \alpha_{ij} \le 0,\ \textstyle\sum_j \alpha_{ij} < 0$$

(polyDistF in Lean).

Formalization targets

Goal: Theorem 5.1

If $g_1, \dots, g_r$ are jointly concave on $\mathbb R^{n+q}$ and $\xi$ has a log-concave density $f$ on $\mathbb R^q$, then

$$h_0 \text{ is logarithmically concave on } \mathbb R^n .$$

Its immediate consequence is that the feasible set $\{x : h_0(x) \ge p\}$ is convex for every $p$.

Milestones

1. Theorem 5.2.1: if $h$ is log-concave on the convex set $H = \{h \ge p\}$, $0 < p < 1$, then $h - p$ is log-concave on $H$. This makes the logarithmic penalty function (5.5) of the SUMT method convex.
2. Theorem 5.2.2: under the standing assumptions of §5.2, every interior point $z$ of the feasible set of (5.1) satisfies $h_i(z) > p_i$, $i = 0, \dots, m$.
3. Theorem 5.7.1 (proved content, (5.21)): for $n = 2$ and oppositely ordered exponents, $\partial^2 F / \partial z_1 \partial z_2 \ge 0$ on $(0,1)^2$.
4. Theorem 5.7.2: the polynomial distribution function is log-concave on $(0,1]^n$.

The platform theorem ConvexOptimization.prekopa_marginal_log_concave (Prékopa's marginal theorem, proved) is included as a reference item.

Significance

Theorem 5.1 turns a probabilistic constraint into a convex constraint after taking logarithms. This is what makes convergence proofs for nonlinear programming methods (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) applicable to (5.1) and to the reliability maximization problem (5.4); without it, those methods have no guarantee of finding a global optimum. Theorems 5.2.1 and 5.2.2 are the two facts that make the SUMT method of §5.2 well defined and convex on the interior of the feasible set. Theorem 5.7.2 shows that probabilistic constraints under the polynomial distribution define convex sets, so they can be added to geometric programmes.

On status: Theorem 5.1 is a classical result, proved in Prékopa's papers (the chapter itself refers to Prékopa's survey for the proof). Prékopa's marginal theorem and the Prékopa–Leindler inequality are already machine-checked on this platform; Theorem 5.1 and the §5.2 and §5.7 theorems are, as far as a search of the platform shows, not formalized. The work is formalizing known proofs, in the log-concavity predicate the platform already uses.

Difficulty

The obvious argument for Theorem 5.1, "the constraint set is convex and the density is log-concave, so the probability is log-concave", hides the real content: log-concavity of a probability as a function of a parameter is a statement about integrals, and it does not follow from pointwise properties of the integrand without a Prékopa–Leindler-type inequality. Concavity of each $g_i$ separately in $x$ and in $y$ is not enough; joint concavity in $(x, y)$ is used essentially. The probability function vanishes on large regions in typical examples, so any argument that takes logarithms pointwise fails at the boundary of its support.

For Theorem 5.2.2 the naive argument fails at the index $i = 0$: nothing about $h_0$ is assumed directly, and log-concavity of $h_0$ is exactly Theorem 5.1. For Theorem 5.7.1 the difficulty is a sign condition on a covariance; without the ordering hypothesis the mixed derivative can be negative.

Formalization scope

$\mathbb R^n$ and $\mathbb R^q$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin q); the constraint functions take pairs $(x, y)$ in the product, and concavity is ConcaveOn ℝ Set.univ on that product (joint concavity). A "continuous probability distribution with density $f$" is stated as P.map ξ = volume.withDensity (ENNReal.ofReal ∘ f) with $\xi$ and $f$ measurable and $P$ a probability measure. Log-concavity is the platform definition ConvexOptimization.LogConcaveOn (nonnegativity plus the power inequality), imported as a reference item; concavity of Real.log ∘ h₀ would be a different, wrong property because Lean's Real.log 0 = 0. Indices are 0-based (Fin r, Fin m, Fin N, Fin n); the probabilistic constraint $i = 0$ of Theorem 5.2.2 is stated separately from $h_1, \dots, h_m$. The polynomial distribution is a formula on Fin n → ℝ with real powers, used only on the cube.

No constant of the book is replaced by an explicit value: every result of this chapter is qualitative.

Corrections of the printed text, recorded in each item's Formalization Note:

• Theorem 5.1 states the density condition "for every $x_1, x_2 \in \mathbb R^n$"; the density lives on $\mathbb R^q$ and the condition is imposed there.
• (5.19) prints the first factor as $z_i^{\alpha_{i1}}$ and the domain index as $i = 1, \dots, N$; they are read as $z_1^{\alpha_{i1}}$ and $j = 1, \dots, n$.
• Theorem 5.7.1 prints its ordering hypothesis with transposed indices ($\alpha_{11} \le \alpha_{12} \le \dots \le \alpha_{1n}$); following the proof, it is read as: across the $N$ terms the $z_1$-exponents increase and the $z_2$-exponents decrease.
• Theorem 5.7.1 claims "is a probability distribution function"; the book proves only (5.21), and normalization would need $\sum_i c_i = 1$, which is not assumed. The formal statement is (5.21), the mixed derivative as an iterated deriv.

Theorem 5.2.2 carries all six assumptions of §5.2, including compactness of the feasible set and the Slater point; it does not assume log-concavity of $h_0$, which must be derived from the density and concavity hypotheses. A trivializing formalization, such as one with a density hypothesis that no probability law satisfies or a log-concavity predicate that holds for every function vanishing somewhere, is ruled out: the density hypotheses are satisfiable (checked locally) and LogConcaveOn is the multiplicative inequality at every pair of points.

Needed infrastructure: Prékopa's marginal theorem (available), log-concavity of indicators of convex sets and of products, measurability of the constraint set, and Artin's theorem that a sum of log-convex functions is log-convex (for Theorem 5.7.2). Artin's theorem and closure properties of LogConcaveOn are reusable beyond this mission, and contributions of them are welcome.

Selected references

• A. Prékopa, "Numerical Solution of Probabilistic Constrained Programming Problems", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 5, pp. 123–139. https://doi.org/10.1007/978-3-642-61370-8
• A. Prékopa, "Logarithmic concave measures with application to stochastic programming", Acta Sci. Math. (Szeged) 32 (1971), 301–316.
• A. Prékopa, "On logarithmic concave measures and functions", Acta Sci. Math. (Szeged) 34 (1973), 335–343.
• A. Charnes and W. W. Cooper, "Chance-constrained programming", Management Science 6 (1959), 73–79. https://doi.org/10.1287/mnsc.6.1.73
• B. L. Miller and H. M. Wagner, "Chance constrained programming with joint constraints", Operations Research 13 (1965), 930–945. https://doi.org/10.1287/opre.13.6.930
• A. Prékopa, Stochastic Programming, Kluwer 1995. https://doi.org/10.1007/978-94-017-3087-7

Motivation

Many design problems in control, finance and operations research are convex programs with uncertain constraints: a decision $\theta$ must satisfy $\theta\in\Theta_\delta$ for a parameter $\delta$ that is not known in advance. Enforcing the constraint for every possible $\delta$ (robust optimization) is often intractable or too conservative, and a chance-constrained formulation needs the distribution of $\delta$, which in practice is rarely known. The scenario approach replaces the uncertain constraint by the constraints of $N$ observed samples $\delta_1,\dots,\delta_N$ and solves the resulting ordinary convex program. The question it answers is how much of the unseen uncertainty the resulting decision still violates.

The answer, the generalization theorem of the scenario approach, is distribution-free: the probability that the scenario solution violates more than a fraction $\varepsilon$ of the uncertainty is bounded by a binomial tail that depends only on $N$ and on the number $d$ of decision variables. This mission formalizes that theorem as it is presented in Chapters 3 and 5 of Campi and Garatti's textbook Introduction to the Scenario Approach (SIAM/MOS 2018), the first mission of a series on the book.

Timeline. Calafiore and Campi introduced scenario programs and bounded the violation of their solutions through the count of support constraints (Math. Program. 2005; IEEE TAC 2006). Campi and Garatti proved in 2008 that the binomial-tail bound of Theorem 3.7 holds for every convex scenario program under existence and uniqueness of the solution, and that it is attained with equality by fully supported problems (SIAM J. Optim. 2008), which settled the tightness question. The textbook (DOI 10.1137/1.9781611975444) presents the theorem with a complete proof for fully supported problems in the plane.

Setting

Fix a cost vector $c\in\mathbb R^d$, a domain $\Theta\subseteq\mathbb R^d$, a measurable space $\Delta$ of uncertainty instances with a probability $\mathbb P$, and a constraint set $\Theta_\delta\subseteq\mathbb R^d$ for each $\delta\in\Delta$.

• The violation of a decision $\theta$ (Definition 3.1) is $V(\theta)=\mathbb P\{\delta\in\Delta:\theta\notin\Theta_\delta\}$, the probability that $\theta$ fails the constraint of a fresh instance.
• For a sample $(\delta_1,\dots,\delta_m)$, the scenario program is

$$\min_{\theta\in\Theta}c^T\theta\quad\text{subject to}\quad\theta\in\bigcap_{i=1}^{m}\Theta_{\delta_i}.$$

A solution is a feasible point of least cost. With $m=N$ i.i.d. samples its solution is denoted $\theta^*$; it is a random vector, a function of the sample, and $V(\theta^*)$ is a random variable in $[0,1]$.

• Assumption 3.4 (convexity): $\Theta$ and every $\Theta_\delta$ are convex and closed. Assumption 3.6 (existence and uniqueness): for every $m$ and every sample, the program with $m$ constraints has exactly one solution.
• A constraint is a support constraint (Definition 5.1) if its removal improves the solution. A problem is fully supported (Definition 5.4) if for every $m\ge d$ the program with $m$ constraints has, with probability 1, exactly $d$ support constraints.

Formalization targets

Goal: Theorem 3.7

For $1\le d\le N$ and every $\varepsilon\in[0,1]$, under Assumptions 3.4 and 3.6,

$$\mathbb P^N\{V(\theta^*)>\varepsilon\}\le\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}.$$

The right-hand side is the upper tail of a Beta$(d,N-d+1)$ distribution. The statement leaves $\mathbb P$, $\Theta$ and the constraint family completely unspecified beyond the two assumptions.

Milestones

1. Helly's lemma (Lemma 5.3), referenced from the platform in its $d$-dimensional form.
2. Theorem 5.2: for every $m$ and every sample, a convex scenario program has at most $d$ support constraints.
3. Eq. (5.3): for a fully supported problem with $d=N=2$, $\mathbb P^2\{V(\theta^*)>\varepsilon\}=1-\varepsilon^2$.
4. Eq. (5.2): for fully supported problems, Theorem 3.7 holds with equality.
5. Eqs. (3.5)–(3.6): the bound is the Beta$(d,N-d+1)$ distribution function (a published incomplete-beta identity).
6. Eq. (3.9): $\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}\le 2^{d-1}(1-\varepsilon/2)^N\le2^{d-1}e^{-\varepsilon N/2}$.
7. Theorem 3.8: $\mathbb E[V(\theta^*)]\le d/(N+1)$.
8. Theorem 1.3: if $N\ge\frac2\varepsilon(\ln\frac1\beta+d-1)$, then $V(\theta^*)\le\varepsilon$ with probability at least $1-\beta$.

Significance

Theorem 3.7 is what makes the scenario approach usable as a design method: it certifies the reliability of a decision computed from data without any knowledge of the data-generating distribution, requiring only independence of the samples. Theorems 3.8 and 1.3 are its two most used consequences, an expected-violation bound and an explicit sample size, and later chapters of the book (constraint removal, the FAST algorithm, empirical-cost results) build on the same statement. Equality for fully supported problems shows that the bound cannot be improved for any $d$ and $N$.

The theorem is proved in the literature; it has no machine-checked proof. A formalization produces, beyond the result itself, a reusable library of scenario programs, violation probabilities and support constraints on which the rest of the series (constraint removal, nonconvex support sets) can be stated, and it checks the measure-theoretic content that the book deliberately leaves aside ("measurability issues are glossed over throughout", p. 33).

Difficulty

The deterministic part, at most $d$ support constraints, is a short consequence of Helly's theorem. The probabilistic part is where the obvious approach fails. A uniform-convergence argument over all $\theta$ (Vapnik–Chervonenkis theory, footnote 11 of the book) gives bounds of the wrong order and can be vacuous, because it ignores that only the solution matters. The sharp bound is an exact statement about the law of $V(\theta^*)$, not a union bound, and problems with fewer than $d$ support constraints, or with degenerate configurations of constraints, must be shown to be no worse than fully supported ones; the book treats the general case only in the plane and refers to Campi & Garatti 2008 for general $d$. Handling the null sets and the exchangeability of the samples under the product measure is a substantial part of the work.

Formalization scope

• Decisions live in EuclideanSpace ℝ (Fin d); the cost is inner ℝ c θ. A sample of size $m$ is ω : Fin m → Δ with law Measure.pi (fun _ : Fin m => P), and P is a probability measure.
• The violation is the real number (P {δ | θ ∉ Θδ δ}).toReal; probabilities of events over the sample are compared in $[0,\infty]$ through ENNReal.ofReal.
• The solution $\theta^*$ is a function θstar : (Fin N → Δ) → EuclideanSpace ℝ (Fin d) together with the hypothesis that θstar ω solves the program for every sample; it is never an arbitrary map.
• Assumption 3.6 is stated for every $m$ including $m=0$ (a unique minimizer on $\Theta$ itself) and for every sample, as on the page.
• Hypotheses the page leaves implicit are explicit: the constraint relation $\{(\theta,\delta):\theta\in\Theta_\delta\}$ is jointly measurable and θstar is measurable (the book's p. 33 convention); $\varepsilon\in[0,1]$; $d\ge1$.
• A support constraint is one whose removal leaves a feasible point of strictly smaller cost than the solution; the count is a Finset.card over Fin m.
• Theorem 3.8 asserts integrability of $V(\theta^*)$ together with the bound, so it cannot hold through the convention that a non-integrable function integrates to $0$. Theorem 1.3's own sentence omits the assumptions; they are added as in §3.2.1, where it is derived from Theorem 3.7.

A statement in which $\theta^*$ is any feasible point of the program, or merely a measurable function of the sample, is false and does not count as a formalization of Theorem 3.7; nor does one in which Assumption 3.6 is weakened to almost every sample. Contributions of general infrastructure are welcome: exchangeability arguments for product measures, the binomial–beta identity, and Helly-type counting lemmas are reusable well beyond this mission.

Selected references

• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018. https://doi.org/10.1137/1.9781611975444
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3), 2008. https://doi.org/10.1137/07069821X
• G. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102, 2005. https://doi.org/10.1007/s10107-003-0499-y
• G. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5), 2006. https://doi.org/10.1109/TAC.2006.875041
• E. Helly, Über Mengen konvexer Körper mit gemeinschaftlichen Punkten, Jahresbericht der DMV 32, 1923.

Motivation

A discrete function defined only on the integer lattice cannot, by itself, be minimized by the tools of continuous optimization — gradients and convexity in the classical sense simply do not apply. Murota's theory of M-convex functions closes this gap by showing that the exchange axiom alone, a purely combinatorial condition, is enough to guarantee that a discrete function behaves exactly like a convex one: its minimizers form a well-structured (M-convex) set, it can be extended to a genuine convex function on real space without gaining any new local minima, and its behavior under a change of price vector (in the economic interpretation where the function is a cost and its argument a bundle of goods) satisfies the same gross substitutes law economists have studied since Kelso and Crawford's matching-market models. This mission develops the second half of that connection: from local optimality (established in the companion mission) to the full structural picture — minimizer sets, price-substitution laws, and the extension of M-convex functions to genuine convex functions in real variables.

Companion mission 06-mconvex-functions-i (Discrete Convex Analysis V) and sibling mission 22-ch06b-mconvexfunctions (Discrete Convex Analysis XXI) cover this chapter's optimality theory (the M-optimality criterion, the exchange axiom as sequential improvement) and its algebraic toolkit (domain operations, worked examples). This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the results on minimizer structure, gross substitutability, and convex extension that this chapter's remaining sections develop: the M-convexity of minimizer sets, the gross substitutes and stepwise gross substitutes properties and their characterizing role, a minimizer-cut theorem with scaling, integral convexity of M♮-convex functions, and — this mission's goal — the theorem characterizing M-convexity entirely through the polyhedral structure of a function's convex extension.

Setting

Fix a finite ground set $V$. For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain, write $f[p](x) = f(x) - \langle p,x \rangle$ for the linear reweighting by $p \in \mathbb R^V$, and $\arg\min g = \{x : g(x) \le g(y)\ \forall y\}$ for the minimizer set of any function $g$. The convex closure $\bar f(x)$ of $f$ at a real point $x$ is the infimum, over finite convex combinations of points of $\operatorname{dom} f$ representing $x$, of the corresponding combination of function values; $f$ is convex extensible if $\bar f$ agrees with $f$ on $\mathbb Z^V$, and integrally convex if $\bar f(x)$ can always be computed using only points from $x$'s own integral neighborhood $N(x)$ (the integer vectors within one unit of $x$ in every coordinate). A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (polyhedral) M-convex if it satisfies the real-variable exchange axiom (M-EXC[R]): for $x,y \in \operatorname{dom}_{\mathbb R} g$ and $u \in \operatorname{supp}^+(x-y)$, some $v \in \operatorname{supp}^-(x-y)$ and $\alpha_0 > 0$ make the exchange inequality hold for every $\alpha \in [0,\alpha_0]$.

Formalization targets

Goal: convex extensibility characterizes M-convexity

For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain,

$$f \text{ is M-convex} \iff \bigl(f \text{ is convex extensible}\bigr) \wedge \bigl(\forall p \in \mathbb R^V,\ \arg\min \bar f[-p] \text{ is an M-convex polyhedron, if nonempty}\bigr),$$

with the M♮-analogue using M♮-convex polyhedra (Theorem 6.43). This is the weakest stable form: it characterizes M-convexity purely by properties of the (unique) convex closure, without reference to any specific algorithm for computing it or any bound on the polyhedron's complexity.

Supporting structural targets

Ten further results build the toolkit this goal draws on and the picture it completes: the M-convexity of minimizer sets (Proposition 6.29), the gross substitutes and stepwise gross substitutes properties and the theorems showing they characterize M-convexity and M♮-convexity among convex-extensible functions (Propositions 6.32-6.33, 6.35, Theorems 6.34, 6.36), a minimizer-cut theorem with scaling used algorithmically in Chapter 10 (Theorem 6.39), integral convexity of M♮-convex functions (Theorem 6.42), a shared-coefficient convex-combination theorem for pairs of M♮-convex functions used in Chapter 8's separation theorem (Theorem 6.44), and the polyhedral-M-convexity of an M-convex function's convex extension together with the correspondence between polyhedral M♮-convexity and the real exchange axiom (Theorems 6.45, 6.47).

Significance

Theorem 6.43 is what makes the whole edifice of M-convex function theory a genuine extension of M-convex set theory (chapters 4-5) rather than a separate parallel development: it says that knowing a function's convex extension is polyhedral, with every price-weighted minimizer set an M-convex polyhedron, is not merely a consequence of M-convexity but an exact characterization of it. This is the theorem that lets later results (the discrete conjugacy theorem of Chapter 8, the separation theorems for M♮-convex functions) move freely between the discrete and continuous pictures. The gross substitutes property (Propositions 6.32-6.36) is independently significant outside this book: it is the exact condition, discovered independently in mathematical economics (Kelso-Crawford, Gul-Stacchetti), under which competitive equilibria with indivisible goods are guaranteed to exist — Murota's theorem that gross substitutability characterizes M-convexity (among convex-extensible functions) is what unifies the economic and combinatorial literatures on this question, taken up again in Chapter 11.

None of these results are open — they are Murota's systematic account of a theory with roots in matroid theory, submodular optimization, and mathematical economics. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (MExchangeAxiom, ConvexClosureVal, ArgMinOn) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The forward direction of Theorem 6.43 (M-convex $\implies$ convex extensible with polyhedral minimizers) is comparatively direct given Theorem 6.42 and Proposition 6.29. The converse is substantial: it must show that a function whose weighted minimizer sets are all M-convex polyhedra — a purely global, polyhedral condition — satisfies the local exchange axiom (M-EXCloc[Z]), and the book's proof does this by an edge-direction argument on the polyhedron $B = \arg\min f$: every edge of an M-convex polyhedron must be parallel to some $\chi_u - \chi_v$, a fact borrowed from the combinatorial structure of chapter 4's base polyhedra applied to a carefully perturbed weight vector. No shortcut through convex analysis alone succeeds, because ordinary polyhedral theory says nothing about which combinatorial directions a polyhedron's edges must follow — that content comes entirely from the M-convexity of the minimizer sets, not from convexity of the closure by itself.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; functions are (V→ℤ)→WithTop ℝ (integer domain) or (V→ℝ)→WithTop ℝ (real domain, for the polyhedral theorems). The convex closure is built directly from finite convex-combination representations rather than an abstract closure operator, and integral convexity compares it against the same construction restricted to each point's integral neighborhood (Fintype.piFinset of per-coordinate Finset.Icc). Real M-convex/M♮-convex polyhedra are defined as convex hulls of M-convex/M♮-convex integer sets, reusing chapters 4-5's own characterization. The real-variable exchange axioms (Theorems 6.45, 6.47) are formalized from the book's primal (interval-of-$\alpha$) definition, not the directional-derivative reformulation (M-EXC'[R]); Theorem 6.47's own three-way equivalence is correspondingly stated with only its first two legs (see Difficulty and MODERATION_NOTES.md/HARD.md — this is a documented scope choice, not a trivializing omission, since the six results using the primal axiom already exercise the chapter's real- variable machinery in full). No numeric constants are hard-coded anywhere in this mission beyond the book's own literal coefficients in Theorem 6.39's cut bound ((n-1)(α-1)). This mission's definitions are redeclared from chunks 06-mconvex-functions-i and 22-ch06b-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the twelve sorrys are welcome; the goal's converse direction and Theorem 6.44's shared-coefficient construction carry the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• A. S. Kelso Jr. and V. P. Crawford, "Job matching, coalition formation, and gross substitutes," Econometrica, 50 (1982), pp. 1483-1504.
• F. Gul and E. Stacchetti, "Walrasian equilibrium with gross substitutes," Journal of Economic Theory, 87 (1999), pp. 95-124.

Motivation

The continuous-review $(Q, r)$ policy — order a fixed quantity $Q$ whenever the inventory position falls to the reorder point $r$ — is the textbook policy for a single item with random demand and a positive replenishment leadtime (Hadley and Whitin 1963). Its optimal parameters have no closed form, so practice routinely falls back on the deterministic economic order quantity (EOQ) model with backorders, whose optimum is explicit. How much the deterministic model misjudges the stochastic system's cost is therefore a practical question, and before Zheng (1992) it had been studied only numerically (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978).

Zheng's paper answers it analytically. This mission targets its Theorem 3, which brackets the optimal cost of the stochastic model by the optimal cost of the EOQ model with the same parameters.

Setting

Demands arrive at rate $\lambda>0$ and orders arrive after a fixed leadtime $L>0$. Each order costs $K>0$; holding and backorder costs accrue at rates $h>0$ and $p>0$ per unit per unit time. The leadtime demand $D$ is a nonnegative random variable with $E(D)=\lambda L$. The inventory cost rate at inventory position $y$ is the newsvendor cost

$$G(y)=E\big[h(y-D)^+ + p(D-y)^+\big],$$

assumed to attain its minimum at a unique point $y^0$.

For order quantity $Q>0$ and reorder point $r$, the long-run average cost is

$$c(Q,r)=\frac{\lambda K+\int_r^{r+Q}G(y)\,dy}{Q}.$$

Let $r(Q)$ be a reorder point minimizing $c(Q,\cdot)$, and define $H(Q)=G(r(Q))$ for $Q>0$, $H(0)=G(y^0)$, and $C(Q)=c(Q,r(Q))$. The optimal order quantity $Q^*$ minimizes $C$ over $Q>0$, and $C^*=C(Q^*)$. Write $H_0(Q)=H(Q)-G(y^0)$ and

$$C_0(Q)=\frac{\lambda K+\int_0^Q H_0(y)\,dy}{Q},$$

the controllable cost, so that $C(Q)=G(y^0)+C_0(Q)$; $C^*_0=C_0(Q^*)$. The constant $G(y^0)$ is the newsboy cost.

The EOQ model is the same construction with demand constant at $\lambda L$: $G_d(y)=h(y-\lambda L)^+ + p(\lambda L-y)^+$, with functions $H_d$, $C_d$, optimal quantity $Q^*_d=\sqrt{2\lambda K(h+p)/(hp)}$ and optimal cost $C^*_d=C_d(Q^*_d)$.

Formalization targets

Goal: Theorem 3 (p. 97)

$$C^*_0\le\frac{Q^*_d}{Q^*}\,C^*_d,\qquad C^*_d\le C^*\le G(y^0)+\frac{Q^*_d}{Q^*}\,C^*_d.$$

All three inequalities are part of the goal. The weaker remark after the proof, $C^*_d\le C^*\le C^*_d+G(y^0)$, drops the factor $Q^*_d/Q^*$ and is not the goal.

Milestones

1. Eq. (7): $C(Q)=\big(\lambda K+\int_0^Q H(y)\,dy\big)/Q$ for $Q>0$.
2. Eq. (8): $Q>0$ is optimal iff $H(Q)=C(Q)$.
3. Eqs. (13)–(15): $C(Q)=G(y^0)+C_0(Q)$, and $H_0(Q^*)=C_0(Q^*)$.
4. Lemma 6: $A(Q)=QH(Q)-\int_0^QH$ is increasing and convex; $Q=Q^*$ iff $A(Q)=\lambda K$; $Q^*$ increases and $r^*$ decreases in $K$.
5. Eqs. (18), (20): $H_d(Q)=\frac{hp}{h+p}Q$, and $Q^*_d$ is the EOQ optimum.
6. Lemma 8: $\int_0^QH\ge\tfrac12QH(Q)\ge A(Q)\ge\tfrac12QH_0(Q)\ge\int_0^QH_0$, with equalities for deterministic demand.
7. Eq. (22): $G_d(y)\le G(y)$ for all $y$.

Significance

Theorem 3 says that randomness of leadtime demand raises the total optimal cost above the EOQ's, yet the controllable part of that cost — the part the order quantity actually trades off — is smaller than the EOQ's cost, scaled by $Q^*_d/Q^*$. Combined with $Q^*_d\le Q^*$ (Theorem 2 of the paper), the gap $C^*-C^*_d$ is at most the newsboy cost $G(y^0)$, independent of $K$, so the EOQ cost is a good proxy when $K$ is large relative to $G(y^0)$. The same machinery yields the paper's Theorem 5, that using $Q^*_d$ in the stochastic model costs at most $1/8$ more than the optimum.

The result was proved in 1992; no machine-checked proof is known to exist. Formalizing it requires the continuous $(Q,r)$ model as a whole — optimal reorder points, the one-variable reduction through $H$, and the area function $A$ — none of which is in Mathlib. The companion missions of this series formalize Theorems 2, 4 and 5 of the same paper on the same model.

Difficulty

The middle inequality compares minima of two different functions: $C_d\le C$ pointwise follows from Jensen's inequality, but only after the reorder point of each model is chosen optimally, so the comparison has to pass through the definition of $C$ as a minimum over $r$. The outer inequalities depend on Lemma 8, whose proof uses convexity of $H$ and a slope comparison $H'\le H_d'$ (Lemmas 4 and 7). The paper argues these through first and second derivatives of $r(Q)$ and $G$, which exist only when the leadtime demand has a smooth distribution; the formal statements assume no density, so a proof must either avoid derivatives or handle one-sided ones. Existence of optimal reorder points and of $Q^*$ is asserted in the paper without a separate argument.

Formalization scope

Everything lives in the namespace ZhengQR.CostBounds. The machinery (qrCost, reorderPt, idealPt, Hfun, Cfun, Afun, H0fun, C0fun, IsOptQty) is defined for an arbitrary $G:\mathbb R\to\mathbb R$ and instantiated at the stochastic $G$ and at $G_d$. A structure QRModel holds the parameters, the demand distribution $\mu$ (a probability measure on $\mathbb R$) and the standing assumptions.

Conventions committed to:

• Positivity of $\lambda,L,K,h,p$; $D\ge0$ almost surely; $D$ integrable with $E(D)=\lambda L$; $G$ has a unique minimizer (p. 90). No density is assumed.
• $r(Q)$ is a chosen minimizer of $c(Q,\cdot)$ over $\mathbb R$, not a solution of $G(r)=G(r+Q)$; $y^0$ is a chosen minimizer of $G$. Both use junk value $0$ when no minimizer exists, which never happens under the assumptions.
• $H(0)=G(y^0)$; statements about $H$ and $A$ are on $[0,\infty)$, about $c$, $C$, $C_0$ for $Q>0$.
• "Optimal order quantity" means $Q>0$ and $C(Q)\le C(Q')$ for all $Q'>0$; the goal takes any such $Q^*$ and Lemma 6 states that exactly one exists, so the goal is not vacuous.
• $C^*_d$ is $C_d(Q^*_d)$, with $Q^*_d$ the explicit formula (20); milestone 5 proves it is the EOQ optimum. $C^*_0$ is $C_0(Q^*)$, which equals $\min_{Q>0}C_0$ by (13).
• "Increasing" in Lemma 6 is read strictly, as the proof gives. Lemma 8 is stated for $Q\ge0$; "deterministic" means $\mu$ is the Dirac mass at $\lambda L$.

A formalization in which $C^*_d$ were an arbitrary number, or $Q^*$ an arbitrary positive real, would make the goal false or empty; both are tied to the model above.

Needed infrastructure: existence of minimizers of convex coercive functions on $\mathbb R$, differentiation of parametric integrals $\int_{r(Q)}^{r(Q)+Q}G$, and properties of the newsvendor cost (convexity, coercivity, Jensen). Most of it is reusable for any continuous-review inventory model. Proofs of any milestone, and of lemmas the paper uses but this mission does not list (Lemmas 2–5, 7), are welcome.

Selected references

• Y.-S. Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87
• G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• P. Zipkin, Inventory Service-Level Measures: Convexity and Approximation, Management Science 32(8):975–981, 1986. https://doi.org/10.1287/mnsc.32.8.975
• A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808

Motivation

In many operational problems (shortest paths, assignment, planning) the decision solves a linear program whose cost vector is unknown at decision time and is predicted from contextual features. The predict-then-optimize pipeline fits a model $f$ that maps a feature vector $x$ to a predicted cost vector $\hat c=f(x)$, and then acts on the decision that is optimal for $\hat c$. Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed to measure the quality of such a model not by the prediction error but by the SPO loss (Smart Predict-then-Optimize loss): the excess true cost of the decision induced by the prediction over the best decision in hindsight.

The question is whether a small SPO loss on the training sample implies a small SPO loss on new data, uniformly over the models a training procedure may return. The SPO loss is neither convex nor continuous in the prediction, so the standard Lipschitz-based bounds for regression do not apply. El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3, Mathematics of Operations Research 2023; a preliminary version appeared at NeurIPS 2019) give the first such generalization bounds. This mission formalizes their first one, for polyhedral feasible regions, which treats every vertex of the feasible region as a class label of a multiclass classification problem. The bound has since been used by later work, e.g. Hu, Kallus and Mao (Fast rates for contextual linear optimization, Management Science 2022), who sharpen it by a $\sqrt{\log n}$ factor (as noted on p. 4 of the paper).

Setting

A feasible region $S\subseteq\mathbb R^d$ is nonempty, compact and convex. For a cost vector $c\in\mathbb R^d$ the nominal problem is $\min_{w\in S}c^\top w$. An optimization oracle is a fixed map $w^*:\mathbb R^d\to S$ with $w^*(c)\in\arg\min_{w\in S}c^\top w$ for every $c$; nothing is assumed about how it breaks ties. The SPO loss of a prediction $\hat c$ when the realized cost is $c$ is

$$\ell_{\rm SPO}(\hat c,c)=c^\top w^*(\hat c)-c^\top w^*(c)\ \ge 0 .$$

The linear optimization gap is $\omega_S(c)=\max_{w\in S}c^\top w-\min_{w\in S}c^\top w$, and for a set $\mathcal C$ of cost vectors $\omega_S(\mathcal C)=\sup_{c\in\mathcal C}\omega_S(c)$; the SPO loss of a cost in $\mathcal C$ lies in $[0,\omega_S(\mathcal C)]$.

Data are pairs $(x,c)$ drawn from a distribution $\mathcal D$ on $\mathcal X\times\mathcal C$. A hypothesis class $\mathcal H$ is a family of predictors $f:\mathcal X\to\mathbb R^d$. The SPO risk is $R_{\rm SPO}(f)=\mathbb E_{\mathcal D}[\ell_{\rm SPO}(f(x),c)]$, and on an i.i.d. sample $(x_1,c_1),\dots,(x_n,c_n)$ the empirical SPO risk is $\hat R_{\rm SPO}(f)=\frac1n\sum_i\ell_{\rm SPO}(f(x_i),c_i)$. The empirical Rademacher complexity with respect to the SPO loss is

$$\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)=\mathbb E_\sigma\Big[\sup_{f\in\mathcal H}\frac1n\sum_{i=1}^n\sigma_i\,\ell_{\rm SPO}(f(x_i),c_i)\Big]$$

with independent uniform signs $\sigma_i\in\{\pm1\}$, and $\mathfrak R^n_{\rm SPO}(\mathcal H)$ is its expectation over the sample.

The decisions induced by $\mathcal H$ form the class $w^*(\mathcal H)=\{x\mapsto w^*(f(x)):f\in\mathcal H\}$. A class $\mathcal F$ N-shatters a finite set $\mathbb X\subseteq\mathcal X$ if there are two labelings $g_1,g_2$ that differ at every point of $\mathbb X$ such that every mixture of them (follow $g_1$ on a subset $T$, $g_2$ on the rest) is realized by some member of $\mathcal F$. The Natarajan dimension $d_N(\mathcal F)$ is the largest size of an N-shattered set. When $S$ is a polyhedron, $\mathfrak S$ denotes its finite set of extreme points.

Formalization targets

Goal: Theorem 2, second display (p. 11)

For a polyhedral $S$ and every $\delta>0$, with probability at least $1-\delta$ over an i.i.d. sample of size $n$, every $f\in\mathcal H$ satisfies

$$R_{\rm SPO}(f)\le\hat R_{\rm SPO}(f)+2\,\omega_S(\mathcal C)\sqrt{\frac{2d_N(w^*(\mathcal H))\log(n|\mathfrak S|^2)}{n}}+\omega_S(\mathcal C)\sqrt{\frac{\log(1/\delta)}{2n}} .$$

Milestones, in attack order

1. Theorem 1 (p. 9): with probability $1-\delta$, $R_{\rm SPO}(f)\le\hat R_{\rm SPO}(f)+2\mathfrak R^n_{\rm SPO}(\mathcal H)+\omega_S(\mathcal C)\sqrt{\log(1/\delta)/(2n)}$ for all $f\in\mathcal H$.
2. Massart step (Appendix B.1, p. 31): for a fixed sample with costs in $\mathcal C$, $\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)\le\omega_S(\mathcal C)\sqrt{2\log|\mathfrak F_{|\mathbb X}|/n}$, where $\mathfrak F_{|\mathbb X}$ is the set of decision vectors $(w^*(f(x_1)),\dots,w^*(f(x_n)))$.
3. Natarajan lemma (cited on p. 31; proved on the platform as UnderstandingML.natarajan_lemma): a class from an $m$-point set to $k$ labels with Natarajan dimension $d$ has at most $m^d k^{2d}$ members.
4. Empirical bound (Appendix B.1, p. 31): for a fixed sample, $\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)\le\omega_S(\mathcal C)\sqrt{2d_N(w^*(\mathcal H))\log(n|\mathfrak S|^2)/n}$.
5. Theorem 2, first display (p. 11): the same bound for the expected complexity $\mathfrak R^n_{\rm SPO}(\mathcal H)$.

Significance

The bound controls the out-of-sample decision cost of every predictor in the class, not only of an empirical risk minimizer, so it applies to any training procedure (SPO+ surrogate minimization, decision trees, heuristics) that returns a member of $\mathcal H$. Its dependence on the feasible region is only through $\omega_S(\mathcal C)$ and $\log|\mathfrak S|$: the number of vertices of a combinatorial polytope is typically exponential in $d$, and enters only logarithmically. For linear predictors $x\mapsto Bx$ the paper's Corollary 2 bounds $d_N(w^*(\mathcal H_{\rm lin}))$ by $dp$, giving a rate of order $\sqrt{dp\log(n|\mathfrak S|)/n}$.

The results are proved in the paper; this mission formalizes them. No statement about predict-then-optimize or the SPO loss is known to have a machine-checked proof. The platform already has the Natarajan lemma (proved) and several Massart-type lemmas for generic classes; this mission connects that multiclass machinery to decision losses, and its Theorem 1 is a reusable Rademacher generalization bound for a loss with range $[0,\omega]$.

Difficulty

The obvious route through Lipschitz contraction fails: the SPO loss jumps when the prediction crosses a point where the optimum is not unique, so the Rademacher complexity of the composed class cannot be bounded by that of $\mathcal H$ times a Lipschitz constant. Any argument through the finitely many vertices of $S$ needs the decisions $w^*(f(x_i))$ to take finitely many values on a sample, i.e. the oracle to return vertices; for an oracle that returns a non-vertex optimal point under ties, $w^*(\mathcal H)$ may take infinitely many values on a sample. On the probabilistic side, the passage from the empirical to the expected complexity and the McDiarmid concentration step (Theorem 1) require the suprema over an uncountable class to be measurable, which the paper does not discuss.

Formalization scope

Lean works in $\mathbb R^d$ = EuclideanSpace ℝ (Fin d); cost vectors and decisions live in the same space and $c^\top w$ is the inner product. The standing assumptions of §2 are hypotheses of every theorem: $S$ nonempty, compact and convex; $w^*$ an arbitrary oracle (a hypothesis IsOracle S w, never a specific selection); $\mathcal C$ nonempty and bounded, with the cost component of $\mathcal D$ in $\mathcal C$ almost surely (or, for fixed-sample statements, every $c_i\in\mathcal C$); $n\ge1$. "Polyhedron" means the solution set of finitely many linear inequalities; with compactness it is a polytope, and $|\mathfrak S|$ is the cardinality of Set.extremePoints ℝ S. The expectation over signs is the exact average over the $2^n$ sign vectors; $R_{\rm SPO}$ and $\mathfrak R^n_{\rm SPO}$ are Bochner integrals. "With probability at least $1-\delta$" is stated as: the product measure of the set of samples on which some $f\in\mathcal H$ violates the bound is at most $\delta$.

The formalization commits to the following disclosed additions:

• In the empirical bound, Theorem 2 and its first display, the oracle returns extreme points of $S$. This is the proof's own "w.l.o.g." (p. 31), made explicit because p. 10 allows non-vertex outputs under ties. The hypothesis is needed: on the unit square, an oracle that returns distinct interior points of an edge under ties can have $d_N(w^*(\mathcal H))=1$ and empirical complexity near $\frac12$, which exceeds the printed bound for large $n$.
• The Natarajan dimension is not defined as a number (a supremum in $\mathbb N$ would silently be $0$ for unboundedly large shattered sets). Statements carry a natural number $k$ bounding the size of every N-shattered set, in place of $d_N(w^*(\mathcal H))$. This is equivalent when $d_N$ is finite; the printed bound is vacuous otherwise.
• Theorem 1 and the goal carry three measurability hypotheses: each loss function $z\mapsto\ell_{\rm SPO}(f(z_1),z_2)$ is measurable; the uniform deviation $\sup_f(R_{\rm SPO}(f)-\hat R_{\rm SPO}(f))$ and, for each sign vector, the signed supremum $\sup_f\frac1n\sum_i\sigma_i\ell_{\rm SPO}(f(x_i),c_i)$ are almost-everywhere measurable functions of the sample. Without them the integral defining $\mathfrak R^n_{\rm SPO}$ could default to $0$.
• The Massart step assumes $\mathfrak F_{|\mathbb X}$ finite, the case in which its printed right-hand side is finite.

A formalization that let $d_N$ be an sSup in $\mathbb N$, or chose a specific tie-breaking oracle inside the definitions, would prove a different and in part trivial statement; both are excluded.

Infrastructure needed: McDiarmid's bounded-differences inequality and symmetrization for the product measure; Massart's finite-class lemma (a proved version is on the platform as RademacherMassart.rad_le_massart, with its own normalization); the Natarajan lemma (proved, UnderstandingML.natarajan_lemma, stated with its own but identical notion of N-shattering over finite types); finiteness and nonemptiness of the extreme points of a nonempty polytope. Theorem 1 and the Massart step do not use polyhedrality and are reusable for any bounded decision loss. Contributions of these infrastructure lemmas are welcome.

Selected references

• O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, arXiv:1905.11488v3, 2022; Mathematics of Operations Research, 2023. https://arxiv.org/abs/1905.11488
• A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 9–26, 2022. https://arxiv.org/abs/1710.08005
• 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
• B. K. Natarajan, On learning sets and functions, Machine Learning 4(1), 67–97, 1989. https://doi.org/10.1007/BF00114804
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014 (Lemma 29.4). https://doi.org/10.1017/CBO9781107298019
• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018 (Theorem 3.3, Corollary 3.8). https://cs.nyu.edu/~mohri/mlbook/