Linear Optimization

Motivation

Network revenue management decides which products to make available to arriving customers when products share scarce resources: an airline sells itineraries (products) that consume seats on flight legs (resources), and each itinerary has a fare. When customers choose among the offered products, rather than asking for one fixed product, the standard planning tool is a deterministic linear program that replaces random choices by their expected values. Gallego, Iyengar, Phillips and Dubey (2004, Columbia CORC technical report TR-2004-01) and Liu and van Ryzin (2008) formulated this choice-based linear program; its solution drives bid-price and offer-set policies used in practice.

The difficulty is size. The choice-based program has one variable for each subset of products, $2^n$ in all, and is solved by column generation, whose pricing subproblem is itself an assortment problem. Feldman and Topaloglu (Oper. Res. 65(5), 2017) show that when customers choose under the Markov chain choice model of Blanchet, Gallego and Goyal (2016), the choice-based program is equivalent to a linear program with only $2n$ variables and $m+n$ constraints. This mission formalizes that equivalence, Theorem 7 of the paper.

Setting

There are $n$ products, $N=\{1,\dots,n\}$. Under the Markov chain choice model a customer first visits product $j$ with probability $\lambda_j$. If the product she visits is offered, she buys it. Otherwise she moves from product $j$ to product $i$ with probability $\rho_{j,i}$, or leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$. The paper assumes throughout that

$$\lambda_j>0\quad\text{and}\quad\sum_{i\in N}\rho_{j,i}<1\qquad\text{for all } j\in N.$$

For an offer set $S\subseteq N$, $P_{j,S}$ is the expected number of visits to product $j$ while it is offered, which is its purchase probability, and $R_{j,S}$ is the expected number of visits to $j$ while it is not offered. The pair $(P_S,R_S)$ is the solution of the (Balance) equations

$$P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S .$$

Dropping the constraints tied to $S$ gives the polyhedron

$$\mathcal H=\Big\{(x,z)\in\mathbb R^{2n}_+ : x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \ \forall j\in N\Big\}.$$

The network has $m$ resources, $M=\{1,\dots,m\}$, with capacities $c_q$; the selling horizon has $T$ periods; product $j$ earns $r_j$ and consumes $a_{q,j}$ units of resource $q$. With $u_S$ the probability of offering $S$ in a period, the (Choice Based) linear program is

$$\max_{u\in\mathbb R^{2^n}_+}\Big\{\sum_{S\subseteq N}\sum_{j\in N}T r_jP_{j,S}u_S:\ \sum_{S\subseteq N}\sum_{j\in N}Ta_{q,j}P_{j,S}u_S\le c_q\ \forall q\in M,\ \sum_{S\subseteq N}u_S=1\Big\},$$

and the (Reduced) linear program is

$$\max_{(x,z)\in\mathbb R^{2n}_+}\Big\{\sum_{j\in N}T r_jx_j:\ \sum_{j\in N}Ta_{q,j}x_j\le c_q\ \forall q\in M,\ x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \forall j\in N\Big\}.$$

In (Reduced), $x_j$ is the expected number of visits to product $j$ while it is available and $z_j$ the expected number of visits while it is not.

Formalization targets

Goal: Theorem 7

Let $(\hat x,\hat z)$ be an optimal solution of (Reduced). Then there are subsets $S^1,\dots,S^K\subseteq N$ and positive scalars $\gamma^1,\dots,\gamma^K$ with $\sum_k\gamma^k=1$ such that

$$\hat x=\sum_{k=1}^K\gamma^kP_{S^k},\qquad \hat z=\sum_{k=1}^K\gamma^kR_{S^k},$$

and for any such subsets and scalars the vector $\hat u$ with $\hat u_{S^k}=\gamma^k$ and $\hat u_S=0$ for $S\notin\{S^1,\dots,S^K\}$ is optimal for (Choice Based), with objective value equal to that of $(\hat x,\hat z)$ in (Reduced). In particular the two programs have the same optimal value.

Milestones

1. (Balance) has a unique and nonnegative solution for every offer set (§2, p. 1325).
2. Lemma 1: an extreme point $(\hat x,\hat z)$ of $\mathcal H$ equals $(P_{S},R_{S})$ for $S=\{j:\hat x_j>0\}$ (p. 1326).
3. Lemma 10: $\mathcal H$ is bounded (quoted on p. 1331; proved in the online appendix).
4. Every point of $\mathcal H$ is a positive convex combination of finitely many extreme points of $\mathcal H$ (proof of Theorem 7, p. 1331).
5. Every feasible $u$ of (Choice Based) yields the feasible point $\tilde x_j=\sum_S P_{j,S}u_S$, $\tilde z_j=\sum_S R_{j,S}u_S$ of (Reduced), with the same objective value (proof of Theorem 7, p. 1332).

Significance

The result. Theorem 7 replaces a program with $2^n$ columns by one with $2n$ variables and $m+n$ constraints, solvable directly by any LP solver, and it returns an optimal solution of the original program, not only its value. The optimal value is the standard upper bound on the optimal expected revenue of a network revenue management policy, and the dual variables of the capacity constraints are the bid prices used to control sales. The decomposition of part 1 is what turns the small program's solution back into offer-set frequencies that a policy can implement; Section 7 of the paper makes that decomposition algorithmic (a separate mission of this series).

Formalizing it. The theorem is proved in the paper; to the best of available knowledge no machine-checked version exists. A formal proof checks the link between polyhedral geometry (extreme points of $\mathcal H$ and the solutions of (Balance)) and linear-programming optimality, and records exactly which properties of the Markov chain choice model are used: the standing assumptions enter through uniqueness and nonnegativity of $(P_S,R_S)$ and through boundedness of $\mathcal H$.

Difficulty

The inequality "(Reduced) $\ge$ (Choice Based)" is a direct computation: averaging the (Balance) equations with weights $u_S$ lands in $\mathcal H$. The reverse direction is where the obvious argument fails. A point of $\mathcal H$ has no offer set attached to it, and a general polyhedron need not be the convex hull of its extreme points: it can contain lines or rays. The argument requires that $\mathcal H$ is bounded, which depends on the substochasticity $\sum_i\rho_{j,i}<1$, and that each extreme point is exactly some $(P_S,R_S)$, which uses the structure of the balance equations and the uniqueness of their solution. Neither follows from general linear-programming facts. In Lean, the finite vertex representation of a bounded polyhedron is also not a one-line consequence of Mathlib's Krein–Milman theorem, which gives only the closure of the convex hull.

Formalization scope

Products are Fin n, offer sets Finset (Fin n), resources Fin m. The model is a structure Model n holding $\lambda$, $\rho$ (rho j i $=\rho_{j,i}$, the transition from $j$ to $i$) and the standing assumptions $\lambda_j>0$ and $\sum_i\rho_{j,i}<1$; the nonnegativity $\rho_{j,i}\ge0$, implicit in the paper because the $\rho_{j,i}$ are probabilities, is an added field. $(P_S,R_S)$ is a solution of (Balance) chosen by Classical.epsilon, and milestone 1 is what identifies it with the paper's unique solution. $\mathcal H$ is a subset of (Fin n → ℝ) × (Fin n → ℝ), extreme points are Mathlib's Set.extremePoints ℝ, and boundedness is Bornology.IsBounded. $T$ is a natural number entering as a real factor exactly where the paper writes it; $c$, $a$, $r$ carry no sign conditions, as in the paper. "Optimal solution" means feasible and at least as good as every feasible point; no supremum is used.

Two conventions are disclosed. The paper defines $\hat u$ by $\hat u_{S^k}=\gamma^k$; the formalization sets $\hat u_S=\sum_{k:S^k=S}\gamma^k$, which agrees when the $S^k$ are distinct and is the only consistent reading otherwise. Milestone 5 is stated for every feasible $u$ of (Choice Based), while the paper applies it to an optimal one; its argument uses only feasibility. No printed statement needed correction.

The goal is not only the decomposition of part 1, which is milestones 2 and 4 combined: it also asserts optimality of $\hat u$ and equality of the optimal values, and a formalization that drops part 2 does not state Theorem 7. Part 2 is required for every decomposition, and part 1 guarantees one exists, so part 2 is not vacuous.

A complete development needs the vertex representation of polytopes (reusable beyond this mission; LinearOptimization.polyhedron_resolution on the platform proves the resolution theorem in another encoding), the theory of substochastic matrices behind (Balance) (invertibility of $I-\bar Q$ with a nonnegative inverse), and finite-sum manipulations over Finset (Fin n). Contributions to any milestone, and bridges to existing polyhedral results, are welcome.

Selected references

• J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
• J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
• Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0172
• G. Gallego, G. Iyengar, R. Phillips, A. Dubey, Managing Flexible Products on a Network, Computational Optimization Research Center Technical Report TR-2004-01, Columbia University, 2004 (technical report; no DOI).
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

A retailer or an airline decides which products to make available, and customers choose among what is offered. When a preferred product is missing, many customers substitute to another product instead of leaving. Assortment optimization asks which subset of products to offer so that the expected revenue from a customer is as large as possible, and its answer depends entirely on the choice model used to describe substitution.

The Markov chain choice model was introduced by Blanchet, Gallego and Goyal (EC 2013; Oper. Res. 64(4), 2016), who showed that it contains the multinomial logit model as a special case and proposed it as an approximation of general random-utility choice models. Feldman and Topaloglu (Oper. Res. 65(5), 2017) study revenue management under this model. Their first result, the subject of this mission, is that the assortment problem, a search over all $2^n$ offer sets, is solved by one linear program with $n$ variables. The same paper uses this result for its dynamic single-resource and network results, which are the subjects of the companion missions II–IV of this series.

Timeline:

• 2013/2016: Blanchet, Gallego and Goyal introduce the model and give a polynomial-time assortment algorithm.
• 2017: Feldman and Topaloglu show that the optimal assortment is read off an optimal solution of a dual linear program (their Theorem 2), and derive structural and capacity-control consequences.

Setting

There are $n$ products $N=\{1,\dots,n\}$. A customer arrives to purchase product $j$ with probability $\lambda_j$. If the product she visits is offered, she buys it. Otherwise she transitions to product $i$ with probability $\rho_{j,i}$ and checks whether $i$ is offered, or leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$. Throughout, $\lambda_j>0$, $\rho_{j,i}\ge0$ and $\sum_{i\in N}\rho_{j,i}<1$ for all $j$.

For an offer set $S\subseteq N$, let $P_{j,S}$ be the expected number of visits to product $j$ while it is offered (the probability that $j$ is purchased) and $R_{j,S}$ the expected number of visits to $j$ while it is not offered. The pair $(P_S,R_S)$ is the unique solution of the (Balance) equations

$$P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S .$$

With revenue $r_j\in\mathbb R$ for product $j$, the (Assortment) problem is $\max_{S\subseteq N}\sum_{j\in N}P_{j,S}r_j$. Two linear programs enter: the maximization of $\sum_j r_jx_j$ over the polyhedron

$$\mathcal H=\Big\{(x,z)\in\mathbb R^{2n}_+:\ x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \ \forall j\in N\Big\},$$

and its dual

$$\min_{v\in\mathbb R^n}\Big\{\sum_{j\in N}\lambda_jv_j:\ v_j\ge r_j\ \ \forall j\in N,\ \ v_j\ge\sum_{i\in N}\rho_{j,i}v_i\ \ \forall j\in N\Big\}.\qquad\text{(Dual)}$$

Formalization targets

Goal: Theorem 2 (p. 1326)

For every optimal solution $\hat v$ of (Dual), the set $\hat S=\{j\in N:\hat v_j=r_j\}$ is an optimal assortment:

$$\sum_{j\in N}P_{j,S}\,r_j\ \le\ \sum_{j\in N}P_{j,\hat S}\,r_j\qquad\text{for all } S\subseteq N .$$

Milestones, in the order the paper uses them

1. (p. 1325) The (Balance) equations have a unique nonnegative solution for every $S$.
2. Lemma 1 (p. 1326): for an extreme point $(\hat x,\hat z)$ of $\mathcal H$ and $S_{\hat x}=\{j:\hat x_j>0\}$, $P_{j,S_{\hat x}}=\hat x_j$ and $R_{j,S_{\hat x}}=\hat z_j$ for all $j$.
3. (p. 1326) The linear program over $\mathcal H$ has an optimal solution, and its optimal value equals the optimal value of (Assortment).
4. (p. 1326) (Dual) has an optimal solution, and its optimal value equals that of the linear program over $\mathcal H$.
5. (p. 1326, proof of Theorem 2) An optimal $\hat v$ satisfies $\hat v_j=r_j$ or $\hat v_j=\sum_i\rho_{j,i}\hat v_i$ for each $j$.

Significance

Theorem 2 reduces a combinatorial problem over $2^n$ offer sets to a linear program, so the assortment problem under the Markov chain choice model is solvable in polynomial time. The same structure drives the rest of the paper: the dual variables $\hat v_j$ are used to show that optimal offer sets shrink when all revenues fall by a common amount, to show that the optimal offer sets of the single-resource dynamic program are nested in the remaining capacity and time, and to reduce the choice-based network linear program to a compact one.

The result is proved in the paper. This mission produces a machine-checked version of it and of its supporting lemmas; to the knowledge of the mission author no formalization of the Markov chain choice model exists. The definition layer (the model, the (Balance) solution, $\mathcal H$ and (Dual)) is the first formal encoding of this choice model and is shared, with the same encoding, by missions II–IV.

Difficulty

The obvious route, comparing $\sum_jP_{j,S}r_j$ across offer sets directly, fails because $P_{j,S}$ is defined only implicitly through a linear system whose coefficient matrix changes with $S$; there is no closed-form expression that can be compared across offer sets, and enumerating the $2^n$ sets is exponential. The connection to linear programming needs an exact correspondence between the vertices of $\mathcal H$ and the (Balance) solutions, which is a statement about polyhedra, not about Markov chains. Even well-posedness is not free: existence, uniqueness and nonnegativity of $(P_S,R_S)$ depend on the row sums $\sum_i\rho_{j,i}$ being strictly below one. Mathlib has extreme points of convex sets but no ready-made theory of vertices of polyhedra or of linear programming duality in this form.

Formalization scope

Products are Fin n (0-based), offer sets are Finset (Fin n) (the paper's $S\subset N$ is non-strict inclusion, so every subset including $\emptyset$ and $N$ is an offer set), and rho j i is $\rho_{j,i}$, the transition from $j$ to $i$. The model structure carries the paper's standing assumptions $\lambda_j>0$ and $\sum_i\rho_{j,i}<1$ (p. 1325) and the implicit nonnegativity $\rho_{j,i}\ge0$. Revenues are arbitrary reals with no sign assumption. $\mathbb R^{2n}$ is (Fin n → ℝ) × (Fin n → ℝ), and extreme points are Mathlib's Set.extremePoints ℝ.

The pair $(P_S,R_S)$ is a solution of (Balance) chosen by Classical.epsilon; milestone 1 states that it satisfies (Balance), is nonnegative and equals every solution, so all statements are about the paper's $(P_S,R_S)$ and not about a junk value. Every optimum (of (Assortment), of the linear program over $\mathcal H$, of (Dual)) is stated as "feasible and at least as good as every feasible point", never through sSup or sInf. The goal is stated for every optimal $\hat v$ of (Dual), which is what the proof uses; uniqueness of $\hat v$ is neither assumed nor claimed. Replacing the hypothesis "$\hat v$ optimal for (Dual)" by "$\hat v$ feasible for (Dual)" would make the statement false, and an existential over $\hat v$ would weaken it; neither is the target.

No hypothesis beyond the paper's is added. Two printed index slips on pp. 1325–1326 (a garbled sum in the discussion after (Balance), and $\sum_i\rho_{i,j}\hat z_j$ for $\sum_i\rho_{i,j}\hat z_i$ in the proof of Lemma 1) are not part of any statement here.

Welcome contributions: the existence and uniqueness of (Balance) solutions via Neumann series for substochastic matrices, a characterization of vertices of polyhedra given by equality constraints and nonnegativity, and a strong duality statement usable for this primal–dual pair. These are reusable well beyond this mission.

Selected references

• J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
• J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

For a convex function on $\mathbb R^n$, a point is a global minimizer as soon as it is a local minimizer — this is one of the earliest and most consequential facts of convex analysis, and it underlies why local-search and gradient methods can certify global optimality in convex programs. The discrete analogue is not automatic: a function on the integer lattice $\mathbb Z^n$ can be "locally optimal" with respect to any fixed finite neighborhood system and still fail to be a global minimizer, unless the function's discrete structure is compatible with that neighborhood in the right way. Identifying exactly which classes of lattice functions admit a local-to-global optimality principle, and with respect to which neighborhood, is one of the organizing questions of discrete convex analysis.

Integrally convex functions, introduced by Favati and Tardella (1990) and developed systematically by Murota, are the most general class of $\mathbb Z^n$-valued functions for which such a principle holds. They are defined purely in terms of the classical convex closure of a real relaxation, which lets one import theorems from ordinary convex analysis, but the resulting notion of local optimality — checking only the $3^n - 1$ neighbors obtained by independently nudging each coordinate by $-1$, $0$, or $+1$ (excluding the trivial no-change case) — is a genuinely discrete, dimension-independent statement about functions whose domain can be arbitrarily large. Almost every discrete convex function class studied later in the book, including M-convex and L-convex functions, is a special case of integral convexity, and this mission's goal theorem is the direct ancestor of the optimality criteria (Theorems 6.26 and 7.14) that drive the algorithms in the rest of the book.

Setting

Let $f : \mathbb Z^n \to \mathbb R \cup \{+\infty\}$ be a function with nonempty effective domain $\operatorname{dom}_{\mathbb Z} f = \{x \in \mathbb Z^n : f(x) \ne +\infty\}$. The convex closure of $f$ is

$$\bar f(x) = \sup_{p \in \mathbb R^n,\, \alpha \in \mathbb R} \{\langle p,x\rangle + \alpha : \langle p,y\rangle + \alpha \le f(y)\ \forall y \in \mathbb Z^n\} \qquad (x \in \mathbb R^n),$$

the pointwise supremum of every affine function minorizing $f$ on all of $\mathbb Z^n$. If $\bar f$ agrees with $f$ on integer points, $f$ is convex extensible. The integral neighborhood of $x \in \mathbb R^n$ is

$$N(x) = \{y \in \mathbb Z^n : \lfloor x_i \rfloor \le y_i \le \lceil x_i \rceil,\ 1 \le i \le n\},$$

and the local convex extension $\tilde f$ relaxes $\bar f$'s definition by requiring the affine minorant condition only on $N(x)$ rather than on all of $\mathbb Z^n$. Always $\tilde f \ge \bar f$ pointwise, and the two agree on $\mathbb Z^n$. A function $f$ is integrally convex if $\tilde f = \bar f$ everywhere on $\mathbb R^n$ — equivalently, if $\tilde f$ is a convex function on all of $\mathbb R^n$ (it is automatically convex on every unit cube $[z, z+1]^n$ with $z \in \mathbb Z^n$, but need not be convex globally without this extra condition).

A discrete set $S \subseteq \mathbb Z^n$ is hole free if $S$ equals the set of integer points in its own real convex hull, and $\arg\min f[-p]$ denotes the minimizer set, over $\mathbb Z^n$, of the linearly perturbed function $f[-p](x) = f(x) - \langle p,x\rangle$.

Formalization targets

Goal: Theorem 3.21 (local optimality characterizes global optimality)

For integrally convex $f$ and $x \in \operatorname{dom}_{\mathbb Z} f$:

$$f(x) \le f(y)\ (\forall y \in \mathbb Z^n) \iff f(x) \le f(x + \chi_Y - \chi_Z)\ (\forall\, Y, Z \subseteq \{1,\dots,n\}),$$

where $\chi_Y \in \{0,1\}^n$ is the indicator vector of $Y$. The right-hand side is a check over at most $3^n - 1$ points (each coordinate independently unchanged, incremented, or decremented), regardless of how large $\operatorname{dom}_{\mathbb Z} f$ is; this uniform, dimension-only bound is the entire content of the theorem, and is the weakest correct formulation — restricting to a single $(Y,Z)$ or letting the right-hand side range over all of $\mathbb Z^n$ would trivialize or falsify the equivalence.

Milestones: Propositions 3.18 and 3.19

Proposition 3.18: $f$ convex extensible $\implies$ $\arg\min f[-p]$ hole free for every $p$ (and conversely, when $\operatorname{dom}_{\mathbb Z} f$ is bounded). Proposition 3.19: $f$ is integrally convex if and only if every restriction $f_{[a,b]}$ to a finite integer interval is integrally convex — integral convexity is detectable by looking at bounded pieces of $f$ one at a time.

Significance

The result itself. Theorem 3.21 is what makes integrally convex functions tractable: without it, verifying global optimality on an infinite or exponentially large integer domain would require checking every point. The theorem reduces this to a check whose size depends only on the dimension $n$, not on the size of the domain, and it does so for the widest class of lattice functions for which such a reduction is possible — the class is defined precisely so that this property holds and no wider natural class enjoys it. Every specialized local-optimality theorem later in the book (for M-convex, M$^\natural$-convex, L-convex, and L$^\natural$-convex functions) restricts this same neighborhood-checking principle to a class where the local check can be made even smaller (a single-element exchange rather than a full sign pattern) precisely because those classes are integrally convex plus more.

Formalizing it. No matching item exists on the platform: a direct search for "integrally convex" returns no results, and the theorem's own proof leans on results (Theorem 1.1's local-to-global principle for ordinary convex functions on $\mathbb R^n$, and an LP-duality-based alternate formula for $\tilde f$) that are either classical convex analysis or belong to a different chapter of this same book. The remaining work is therefore to give a complete, correct account of the definitional chain — convex closure, local convex extension, integral convexity — in a form a solver can build a proof from directly, and to state the finite local-check equivalence itself exactly at the strength the book proves it, not a plausible-looking weakening of it.

Difficulty

The natural first attempt is to try to prove the "$\Leftarrow$" direction of Theorem 3.21 by a direct induction on the $\ell^1$-distance to a global minimizer, moving one coordinate at a time. This fails in general lattice functions (a function that is only "coordinatewise convex" can have strict local minima that are not global), and the theorem's actual proof instead routes through the real relaxation: it shows the neighborhood-check hypothesis forces $x$ to be a local minimizer of the local convex extension $\tilde f$ restricted to the unit ball around $x$, then invokes ordinary convex analysis (local minimality implies global minimality for a convex function on $\mathbb R^n$) to conclude $x$ globally minimizes $\bar f$, and finally uses integral convexity ($\tilde f = \bar f$) to transfer this back to $f$ on $\mathbb Z^n$. The identification of $f$'s local behavior with $\tilde f$'s convexity on a single unit cube — rather than any coordinatewise or separable argument — is the step that makes the class of integrally convex functions exactly the right one for this theorem, and is where a naive combinatorial argument breaks down.

Formalization scope

The ground set is $\mathbb Z^n$, represented as Fin n → ℤ; $f$'s codomain is WithTop ℝ (exactly $\mathbb R \cup \{+\infty\}$), while the convex closure $\bar f$ and local convex extension $\tilde f$ take values in EReal (exactly $\mathbb R \cup \{\pm\infty\}$, a complete lattice, so their defining suprema are total functions with no side conditions). A trivializing formalization of the goal would quantify the right-hand side over a single fixed $(Y,Z)$ pair, or over all of $\mathbb Z^n$ instead of the sign-pattern neighbors; both are excluded by keeping $Y, Z$ universally quantified Finset (Fin n) ranging over the full $3^n$ sign-pattern space (minus the trivial case, which the equivalence still holds through vacuously).

Checked against the platform (GET /theorems?q=integrally convex, 0 hits) and against Mathlib's Analysis/Convex/ for the classical facts this chapter's proof would eventually need (ordinary convex-function local-to-global optimality, LP duality): these are broadly available in Mathlib's convex-analysis library in some form, but none of them is imported here, since none appears in the statement of any item this mission drafts — they belong to a proof this pass does not attempt. Contributions to a shared DiscreteConvex.IntegralConvexity definitions layer are welcome from chunks 06–09, which specialize integral convexity to M-convex and L-convex functions and will need the same convex-closure/local-extension vocabulary.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• P. Favati, F. Tardella, "Convexity in nonlinear integer programming," Ricerca Operativa, 53, 1990, pp. 3–44.

Motivation

Many combinatorial optimization problems on graphs are linear programs over a polytope whose inequality description is unknown. The stable set polytope is the standard example: maximizing a linear function over it is the maximum weight stable set problem, which is NP-hard, and no complete inequality description is known for general graphs. A productive line of work, begun in V. Chvátal's 1975 paper On certain polytopes associated with graphs (J. Combin. Theory Ser. B 18 (1975) 138–154), asks instead how such descriptions behave under graph operations: if descriptions are known for small graphs, can one write one down for a graph built from them?

Section 5 of that paper answers this for substitution, the operation that replaces a vertex of one graph by a whole second graph. Substitution contains three familiar constructions as special cases: duplicating a vertex, forming the join of two graphs, and forming the lexicographic product (composition). Duplication is one of the two ingredients of Lovász's proof of the perfect graph theorem (Lovász 1972); substitution in general is the operation under which perfection is preserved, and graphs built from simple pieces by substitution are a recurring source of classes with tractable stable set polytopes.

Setting

All graphs are finite, undirected and loopless. A stable set of a graph $G=(V,E)$ is a set of vertices no two of which are adjacent. Write $S(G)\subseteq\mathbb R^V$ for the set of incidence vectors of stable sets (the zero–one vectors $x$ with $\{u:x_u=1\}$ stable), and

$$P(G)=\operatorname{conv}S(G)$$

for the stable set polytope. A finite system of linear inequalities in the variables $(x_u:u\in V)$ is a defining linear system of $P(G)$ when its set of solutions is exactly $P(G)$.

Let $G_1=(V_1,E_1)$ and $G_2=(V_2,E_2)$ be graphs with $V_1\cap V_2=\emptyset$, and let $v\in V_1$. The graph $G$ obtained from $G_1$ by substituting $G_2$ for $v$ has vertex set $(V_1-\{v\})\cup V_2$. Its edges are the edges of $G_1-v$, the edges of $G_2$, and every edge joining a vertex of $G_2$ to a neighbour of $v$ in $G_1$. In Lean the vertex type is the disjoint sum {u : V₁ // u ≠ v} ⊕ V₂ and the graph is substitute G₁ v G₂.

Formalization targets

Goal: Theorem 5.1

For $k\in\{1,2\}$ let

$$-x_u\le 0\ (u\in V_k),\qquad \sum_{u\in V_k}a_{iu}x_u\le b_i\ (i\in J_k)$$

be a defining linear system of $P(G_k)$, with $J_1,J_2$ finite index sets and real coefficients, and put $a^+_{iv}=\max\{a_{iv},0\}$ for $i\in J_1$. Then

$$-x_u\le 0\ \ (u\in V_2\cup(V_1-\{v\})),\qquad a^+_{iv}\sum_{u\in V_2}a_{ju}x_u+b_j\sum_{u\in V_1-\{v\}}a_{iu}x_u\le b_ib_j\ \ (i\in J_1,\ j\in J_2)\tag{5.1}$$

is a defining linear system of $P(G)$. The statement fixes no particular system for $G_1$ or $G_2$: any defining systems of the two pieces produce one for $G$, with $|J_1|\cdot|J_2|$ rows besides nonnegativity.

Milestones

1. Validity of (5.1) (§5, p. 145): every $x\in S(G)$ satisfies (5.1), hence so does every point of $P(G)$.
2. Proposition 2.1 (pp. 139–140): for a finite nonempty set $S$ of solutions of a system with nonnegativity rows $-x_u\le 0$, the solution set equals $\operatorname{conv}S$ if and only if for every integer vector $c$ the value $\max\{cx:x\in S\}$ equals the minimum of the associated dual linear program, the minimum being attained.
3. Decomposition of the optimum (§5, pp. 145–146): for an integer vector $c$ on $V_2\cup W$, $W=V_1-\{v\}$, with $d_u=\max\{c_u,0\}$,

$$\max\{cx:x\in S(G)\}=\max\{m_0,\ m_1+m_2\},$$

where $m_0$ and $m_1$ are the maxima of $\sum_{u\in W}d_ux_u$ over $x\in S(G_1)$ with $x_v=0$ and $x_v=1$ respectively, and $m_2$ is the maximum of $\sum_{u\in V_2}d_ux_u$ over $S(G_2)$.

Significance

Theorem 5.1 gives an explicit construction: from a polyhedral description of $P(G_1)$ and $P(G_2)$ it writes one of $P(G)$, row by row, with no loss. Specialized to $G_1=K_2$ it gives Corollary 5.2 of the paper, a defining linear system for the join $G_1+G_2$; applied repeatedly it gives defining systems for lexicographic products, and applied with $G_2=\overline{K_2}$ it describes the effect of duplicating a vertex. Applied to clique systems, whose coefficients are 0 and 1, the rows of (5.1) are again clique inequalities of $G$, so the class of graphs whose stable set polytope is described by nonnegativity and clique inequalities is closed under substitution.

The result has been proved in print since 1975. As far as a search of the Prove2Me catalogue shows, none of it, including Proposition 2.1 and the substitution operation itself, has a machine-checked statement or proof. The mission asks for a formal proof of the theorem and of the two combinatorial and polyhedral steps it rests on. The definitions of $S(G)$, $P(G)$ and graph substitution, and the LP characterization of Proposition 2.1, are reusable by every other mission on stable set polytopes and on polyhedral descriptions of 0–1 sets.

Difficulty

That every point of $P(G)$ satisfies (5.1) is a short case check on stable sets of $G$. The difficulty is the reverse inclusion: that no point outside $P(G)$ satisfies (5.1). The first idea, taking a point that satisfies (5.1) and splitting it directly into a point of $P(G_1)$ and a point of $P(G_2)$, fails: (5.1) couples the two input systems through products of their coefficients and right-hand sides, and a fractional solution of (5.1) carries no evident decomposition into the two pieces. Nothing is assumed about the signs of the input coefficients, so the rows of (5.1) can mix positive and negative terms, and the positive part $a^+_{iv}$ in place of $a_{iv}$ is what keeps the system valid when $a_{iv}<0$.

The polyhedral step behind Proposition 2.1, relating a convex hull of finitely many points to an inequality system through linear programming duality, is not available in Mathlib in this form and has to be built.

Formalization scope

• Graphs are SimpleGraph on a Fintype with decidable equality; the substituted graph lives on {u : V₁ // u ≠ v} ⊕ V₂, which builds in $V_1\cap V_2=\emptyset$.
• $S(G)$ is the set of real incidence vectors of finite stable sets (IsIndepSet); $P(G)$ is convexHull ℝ (S G), never the solution set of an inequality system.
• A linear system is a finite index type $J$ with real a : J → V → ℝ, b : J → ℝ. The nonnegativity rows $-x_u\le0$ are kept as a separate conjunct ∀ u, 0 ≤ x u everywhere; Proposition 2.1 is false without them. "Defining linear system" is set equality of the solution set with $P(G)$.
• No sign conditions on the $a_{iu}$ or $b_i$ are assumed; the paper assumes none.
• Implicit hypothesis made explicit: $V_2\ne\emptyset$ ([Nonempty V₂]) in Theorem 5.1. The paper's graphs have nonempty vertex sets and its proof picks a vertex of $G_2$; with $V_2=\emptyset$, $J_2=\emptyset$ and $V_1\ne\{v\}$, (5.1) is just $x\ge0$ and the theorem fails. The validity milestone does not need it.
• In Proposition 2.1 the set $S$ is assumed nonempty, which the paper's $\max\{cx:x\in S\}$ presupposes. "max = min" is stated as a lower bound for every feasible dual vector plus a feasible dual vector attaining the maximum.
• In the decomposition milestone each maximum is a real sSup over a finite set that always contains the zero vector or the incidence vector of $\{v\}$, so no junk value of sSup can occur.
• A trivializing formalization is excluded: $P(G)$ is the convex hull of stable-set vectors rather than a set defined through the same inequalities, and the goal is the full set equality, not the validity inclusion alone.

Contributions welcome: a proof of Proposition 2.1 (the reusable core), the combinatorial decomposition, the validity case check, and the assembly of the goal.

Selected references

• V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
• L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
• F. Harary, Graph Theory, Addison-Wesley, 1969.

Motivation

Many decision problems in operations research are solved in two stages: a model predicts the unknown cost vector of a linear optimization problem from features, and the predicted costs are then passed to a solver. The smart predict-then-optimize (SPO) loss of Elmachtoub and Grigas measures the quality of a prediction by the excess true cost of the decision it induces, rather than by the prediction error itself. El Balghiti, Elmachtoub, Grigas and Tewari study how well the empirical SPO loss generalizes. Their margin-based bounds (Theorems 4 and 5 of the paper) require a geometric condition on the feasible region, the strength property, and a way to compute the distance to degeneracy that enters the margin loss.

Section 5 of the paper verifies this condition in the two cases that matter in practice. For strongly convex regions it is Theorem 7 (mission III of this series). This mission covers the other case, §5.2: feasible regions that are polytopes given by a list of points, which includes the unit simplex of multiclass classification and the feasible regions of shortest-path, assignment and other combinatorial problems written as convex hulls.

Setting

Let $E$ be a finite-dimensional real vector space (the paper's $\mathbb R^d$) with a norm $\|\cdot\|$. A cost vector $\hat c$ is a linear functional on $E$; its value at $w$ is written $\hat c^\top w$, and its dual norm is $\|\hat c\|_*=\max_{\|w\|\le1}\hat c^\top w$.

The feasible region is a polytope with a known convex hull representation: pairwise distinct points $v_1,\dots,v_K\in E$ and

$$S=\mathrm{conv}\{v_1,\dots,v_K\}.$$

Redundant points (points that are convex combinations of the others) are allowed. For a cost vector $\hat c$, $P(\hat c)$ is the problem $\min_{w\in S}\hat c^\top w$, and an optimization oracle $w^*$ is any map with $w^*(\hat c)\in\arg\min_{w\in S}\hat c^\top w$ for every $\hat c$.

• The degenerate set $\mathcal C^\circ$ is the set of cost vectors $\hat c$ for which $P(\hat c)$ has more than one optimal solution.
• The distance to degeneracy is $\nu_S(\hat c)=\inf_{c\in\mathcal C^\circ}\|c-\hat c\|_*$.
• $S$ has the strength property with parameter $\mu>0$ if

$$\hat c^\top\big(w-w^*(\hat c)\big)\ \ge\ \frac{\mu\,\nu_S(\hat c)}{2}\,\|w-w^*(\hat c)\|^2\qquad\text{for all } w\in S\text{ and all }\hat c.$$

• The negative normal cone at $v_j$ is $\mathcal K_j=-N_S(v_j)=\{\hat c:\hat c^\top(w-v_j)\ge0\ \text{for all } w\in S\}$, the cost vectors for which $v_j$ is optimal.
• The diameter is $\Delta(S)=\sup_{w_1,w_2\in S}\|w_1-w_2\|$.

Formalization targets

Goal: Theorem 8, strength claim (p. 25)

If $S=\mathrm{conv}\{v_1,\dots,v_K\}$ is not a singleton, then for every oracle $w^*$, $S$ has the strength property with parameter

$$\mu=\frac{2}{\Delta(S)}>0 .$$

Milestones, in attack order

1. Eq. (9) (p. 24): each cone is described by finitely many inequalities,

$$\mathcal K_j=\{\hat c:\hat c^\top(v_i-v_j)\ge0\ \text{for all } i=1,\dots,K\}.$$

2. Proposition 2 (p. 25): $P(\hat c)$ has a unique optimal solution if and only if $\hat c\in\mathrm{int}(\mathcal K_j)$ for some $j$; hence

$$\mathcal C^\circ=\mathbb R^d\setminus\bigcup_{j=1}^K\mathrm{int}(\mathcal K_j).$$

3. Diameter (p. 25, the sentence before Theorem 8): $\Delta(S)=\max_{i,j}\|v_i-v_j\|$.
4. Theorem 8, eq. (10) (p. 25): for every oracle and every $\hat c$,

$$\nu_S(\hat c)=\min_{j:\,v_j\ne w^*(\hat c)}\frac{\hat c^\top(v_j-w^*(\hat c))}{\|v_j-w^*(\hat c)\|}.$$

Significance

The result. Formula (10) turns the distance to degeneracy, defined as an infimum over an infinite non-convex set, into a minimum of $K$ explicit ratios that needs one oracle call. This makes the margin SPO loss of the paper computable for polytopes. The strength claim, combined with the paper's Theorems 4 and 5, yields margin-based generalization bounds for the SPO loss over any polytope with a known vertex list, with a dependence on the hypothesis class through its multivariate Rademacher complexity rather than through a Natarajan dimension. For the unit simplex it recovers known margin bounds for multiclass classification (Example 8).

Formalizing it. The results are proved in the paper; to our knowledge none of them is machine-checked. A formalization produces, beyond the four statements, a Lean account of the normal fan of a polytope presented by a point list, its interplay with uniqueness of linear-optimization solutions, and distances to its boundary measured in a dual norm. These are standard facts of polyhedral theory that Mathlib does not yet state in this form.

Difficulty

The obstacle is that $\nu_S$ is a distance to the degenerate set, and that set is neither convex nor given by inequalities: it is a union of lower-dimensional pieces of the normal fan, so no projection formula applies, and its description depends on which points of the representation are redundant. Relating a dual-norm ball around $\hat c$ to the finitely many inequalities of eq. (9) is where the argument needs care. A Euclidean shortcut is not available: the norm is arbitrary, and the numerator of (10) and the distance $\nu_S$ are measured in different norms. A second trap is the oracle: at a degenerate $\hat c$ it may return a point that is not among the $v_j$, and (10) must still hold.

Formalization scope

• $E$ is a finite-dimensional real normed space; cost vectors are elements of StrongDual ℝ E, whose operator norm is the dual norm. Interiors and distances in the cost space use that norm.
• The polytope is v : Fin K → E, injective, with $S$ = convexHull ℝ (Set.range v). Nonemptiness, compactness and convexity of $S$ (the paper's §2 standing assumptions) follow from this representation; Proposition 2 and the diameter identity add $K\ge1$, which is that nonemptiness.
• "Not a singleton" is S.Nontrivial. Without it $\mathcal C^\circ=\emptyset$, $\nu_S\equiv0$ and the strength property holds for free; with it, $0\in\mathcal C^\circ$ and $\nu_S$ is a genuine distance. The goal's parameter $2/\Delta(S)$ is stated to be positive, so the Lean conventions $\mathrm{diam}=0$ on unbounded or one-point sets and $2/0=0$ cannot trivialize it.
• The oracle is arbitrary: every theorem quantifies over all maps $w$ with $w(\hat c)\in\arg\min_S\hat c$, never a fixed selection.
• $\nu_S$ is Metric.infDist to $\mathcal C^\circ$; $\Delta(S)$ is Metric.diam, correct here because $S$ is bounded. Minima and maxima over finite index sets are stated with IsLeast/IsGreatest, so no junk value of min' or sInf enters.
• Reusable infrastructure: the negative normal cones and normal fan of a point-list polytope, the characterization of unique optima of linear optimization over a polytope, and the dual-norm distance to the boundary of a polyhedral cone. Contributions of any of these as standalone 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), 2022. https://doi.org/10.1287/mnsc.2020.3922
• G. M. Ziegler, Lectures on Polytopes, Graduate Texts in Mathematics 152, Springer, 1995. https://doi.org/10.1007/978-1-4613-8431-1
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 2009. https://doi.org/10.1007/978-3-642-02431-3

Cutting planes from lattice-free convex sets

Cutting planes for mixed-integer linear programs are often derived from a few rows of an optimal simplex tableau. Keeping $q$ rows for basic integer variables $x_1,\dots,x_q$, dropping the nonnegativity of $x$ (Gomory's corner polyhedron, Gomory 1969) and then the integrality of the nonbasic variables leaves the set of $s\ge0$ with $f+\sum_j r^js_j\in\mathbb Z^q$. Balas observed in 1971 that convex sets with no integral point in their interior give valid inequalities for such sets (Balas 1971). Andersen, Louveaux, Weismantel and Wolsey (2007) for two rows, and Borozan and Cornuéjols (2009) for any number of rows, showed that for rational data the irredundant valid inequalities correspond to maximal lattice-free convex sets. Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543; Math. Oper. Res. 35(3), 2010) removed the rationality assumption. This mission formalizes that result, Theorem 3 of their paper.

Setting

Fix $q\ge0$, a point $f\in\mathbb R^q$ and a linear subspace $W\subseteq\mathbb R^q$, and assume that the affine space $f+W$ contains an integral point. Products such as $ry$ are standard inner products.

• $\mathcal W$ is the space of real functions $s=(s_r)_{r\in W}$ with finite support. The semi-infinite relaxation is

$$R_f(W)=\Big\{s\in\mathcal W \ \Big|\ f+\sum_{r\in W}rs_r\in\mathbb Z^q,\ s_r\ge0\ (r\in W)\Big\}.$$

• A linear inequality is a pair $(\psi,\alpha)$ with $\psi:W\to\mathbb R$ an arbitrary function and $\alpha\in\mathbb R$, read as $\Psi(s)=\sum_{r\in W}\psi(r)s_r\ge\alpha$. It is valid if every $s\in R_f(W)$ satisfies it.
• $V$ is the affine hull of $(f+W)\cap\mathbb Z^q$, and $\mathcal V=\{s\in\mathcal W\mid f+\sum_r rs_r\in V\}$. A linear inequality is trivial if every $s\in\mathcal V$ with $s\ge0$ satisfies it. When $W$ is irrational (not spanned by the integral points it contains, up to translation), $V$ is a proper affine subspace of $f+W$.
• $\sum\psi(r)s_r\ge\alpha$ dominates $\sum\psi'(r)s_r\ge\alpha$ if $\psi\le\psi'$ pointwise. A valid inequality is minimal if no valid inequality with the same $\alpha$ and a different $\psi'\le\psi$ exists.
• Choose $C\in\mathbb R^{\ell\times q}$ and $d\in\mathbb R^\ell$ with $V=\{x\in f+W\mid Cx=d\}$. Two valid inequalities are equivalent if $\psi(r)=\rho\psi'(r)+\lambda^TCr$ for all $r\in W$ and $\alpha=\rho\alpha'+\lambda^T(d-Cf)$, for some $\rho>0$, $\lambda\in\mathbb R^\ell$.
• A maximal lattice-free convex set in $f+W$ is a convex $B\subseteq f+W$ with no integral point in its interior relative to $f+W$, inclusionwise maximal with these properties.
• For $K\subseteq W$ closed, convex, with $0$ in its interior relative to $W$: the polar $K^*=\{y\in W\mid ry\le1\ \forall r\in K\}$, $\hat K=\{y\in K^*\mid\exists x\in K,\ xy=1\}$, and $\rho_K(r)=\sup_{y\in\hat K}ry$. For such a $B$ with $f$ in its interior, $\psi_B=\rho_{B-f}$; for a polyhedral $B=\{x\in f+W\mid a_i(x-f)\le1\}$ with tight rows this is $\psi_B(r)=\max_ia_ir$.

A function $\sigma:W\to\mathbb R$ is sublinear if $\sigma(\lambda r)=\lambda\sigma(r)$ for $\lambda\ge0$ and $\sigma(r+r')\le\sigma(r)+\sigma(r')$.

Formalization targets

Goal: Theorem 3 (p. 6)

1. Every nontrivial valid linear inequality for $R_f(W)$ is dominated by a nontrivial minimal valid linear inequality for $R_f(W)$.
2. Every nontrivial minimal valid linear inequality for $R_f(W)$ is equivalent to one of the form

$$\sum_{r\in W}\psi_B(r)s_r\ \ge\ 1$$

with $\psi_B\ge0$ on $W$ and $B$ a maximal lattice-free convex set in $f+W$ with $f$ in its interior.

The goal is stated as one conjunction. It fixes no constants and makes no rationality assumption on $f$ or $W$.

Milestones

In the order in which the proof on pp. 15–21 uses them:

• Lemma 23 (a sublinear valid inequality below any valid one)
• Lemma 26 (invariance under equivalence)
• Claims 1 and 2 in the proof of Theorem 3
• Theorem 28 (Basu–Cornuéjols–Zambelli: $\rho_K$ is the smallest sublinear function with $1$-sublevel set $K$)
• Remark 30 and Claim 4 (the inequality $\sum\rho_K(r)s_r\ge1$)
• Remark 29 ($\rho_K=\max_ia_ir$ for tight rows)
• Claim 6 (a shift by $\lambda^TC$ making $\psi$ nonnegative)
• Claim 7 ($\psi_B$ below a nonnegative sublinear $\psi''$)
• Lemma 31 (maximal lattice-free sets give minimal inequalities)

Significance

Theorem 3 says that the minimal valid inequalities of $R_f(W)$ are exactly those produced by maximal lattice-free convex sets, up to the equivalence forced by the affine hull $\mathcal V$. It also says that for irrational $W$, where valid inequalities can have negative coefficients, some equivalent form always has nonnegative coefficients. The paper derives two further results from it: a description of the closure of $\operatorname{conv}(R_f(W))$ in a suitable norm (Theorem 4), and a reduction of extreme inequalities of the infinite model to finite ones (Theorem 5). Both results remain unproved without it.

The result has a complete proof in the paper, which relies on the cited Theorem 28 from Basu, Cornuéjols, Zambelli. To our knowledge none of it is machine-checked. A formalization would provide a definitional layer for corner relaxations, lattice-free sets and valid inequalities, which is currently absent from Mathlib. It would also expose where the page is imprecise; see the scope section.

Difficulty

For rational data every valid inequality can be written with right-hand side $1$ and nonnegative coefficients, and $\psi$ is then the gauge of $B_\psi$. For irrational $W$ this fails. Since $R_f(W)\subseteq\mathcal V$, adding $\lambda^TCr$ to $\psi$ changes nothing on $R_f(W)$, so coefficients can be negative, and $B_\psi=\{x\in f+W\mid\psi(x-f)\le\alpha\}$ may have a full-dimensional recession cone. A maximal lattice-free set containing $B_\psi$ then yields a $\psi_B$ that need not lie below $\psi$ (the example on pp. 21–22 shows this). One must first pass to an equivalent inequality whose set has no full-dimensional recession cone within $V$. This step combines the structure theorem for maximal lattice-free sets in irrational subspaces (Theorem 9 of the paper) with a duality argument. A second obstacle is that $\psi$ is an arbitrary function: validity alone gives no convexity or continuity, and Lemma 23 is needed to recover them.

Formalization scope

• Ambient space. $\mathbb R^q$ is EuclideanSpace ℝ (Fin q), $W$ is a Submodule, and $\mathcal W$ is W →₀ ℝ. The printed phrase "the set $\{r\mid s_r>0\}$ has finite cardinality" is read as ordinary finite support.
• Standing hypothesis. Every statement assumes that $f+W$ contains an integral point. Without it $R_f(W)=\emptyset$ and every inequality is valid, so this hypothesis rules out the trivializing formalization. The equivalence predicate carries the hypothesis $V=\{x\in f+W\mid Cx=d\}$ together with validity of both inequalities. With $C,d$ unconstrained, equivalence would be rescaling only, and part 2 of the goal would be false for irrational $W$.
• Interiors. All interiors are relative: to $f+W$ for $B$ and $B_\psi$, to $W$ for $K$.
• $\psi_B$. It is defined as $\rho_{B-f}$, independent of any description of $B$.

The paper is imprecise in three places, and the formalization departs from the page in each:

1. Remark 29 is false without tight rows: for $K=(-\infty,1]\subseteq\mathbb R$ written with $a_1=1$, $a_2=1/2$, $\rho_K(r)=r\ne\max(r,r/2)$ for $r<0$. It is stated with the tightness the paper arranges before using it.
2. The identity $\operatorname{int}(B_\psi)=\{x\mid\psi(x-f)<\alpha\}$ on p. 17 fails at $\alpha=0$, for example for $\psi\equiv0$. Claims 1 and 2 use the strict sublevel set, and Claim 2 is false for the topological interior.
3. Claims 5 and 7 invoke Corollary 20 in $f+W$, although it is proved only for a lattice of a linear space. Corollary 20 and Claim 5 are therefore not milestones.

Two kinds of contributions are especially welcome: reusable infrastructure for polars of convex sets relative to a subspace and for sublinear functions on submodules, and a proof of Theorem 28.

Selected references

• A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543v1
• A. Basu, G. Cornuéjols, G. Zambelli, Convex sets and minimal sublinear functions, J. Convex Anal. 18(2), 2011 (reference [9]).
• V. Borozan, G. Cornuéjols, Minimal valid inequalities for integer constraints, Math. Oper. Res. 34(3), 2009. https://doi.org/10.1287/moor.1090.0400
• K. Andersen, Q. Louveaux, R. Weismantel, L. Wolsey, Inequalities from two rows of a simplex tableau, IPCO 2007. https://doi.org/10.1007/978-3-540-72792-7_1
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra Appl. 2, 1969. https://doi.org/10.1016/0024-3795(69)90017-2

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