Operations Research

Learning with anomalies

In the on-line prediction model studied by Littlestone and Warmuth (Inform. and Comput. 108, 1994), a learner receives instances one at a time, predicts a binary label for each, and is then told the correct label. No probabilistic assumption is made: performance is measured by the number of mistakes on a worst-case sequence. When every label is given by some function of a known target class $F$, the best attainable worst-case number of mistakes is a combinatorial invariant of $F$, characterized by Littlestone (Mach. Learn. 2, 1988) through mistake trees, now called the Littlestone dimension.

Real data are rarely labelled exactly by a member of the class. Littlestone and Warmuth measure the departure by the number of anomalies: the number of trials inconsistent with the best function in the class. Their Weighted Majority algorithm makes a number of mistakes that grows linearly in the number of anomalies, and the rate of growth can be pushed towards $2$ mistakes per anomaly by the choice of the update factor $\beta$. Theorem 8.1 of the paper shows that no deterministic learner does better: rate $2$ is forced for every class with at least two members. This mission formalizes that lower bound.

Setting

Let $X$ be an arbitrary set (the domain) and $F$ a set of functions $X \to \{0,1\}$, possibly infinite. A trial is a pair $(x,y) \in X \times \{0,1\}$, and a sequence of trials $\mathcal S = ((x_1,y_1),\dots,(x_T,y_T))$ is finite; an instance may occur several times with different labels.

• The number of anomalies of $\mathcal S$ with respect to $f : X \to \{0,1\}$ is $\mathrm{anom}_f(\mathcal S) = \#\{t \le T : f(x_t) \ne y_t\}$.
• $S_\eta$ is the collection of sequences with at most $\eta$ anomalies with respect to $F$: those $\mathcal S$ with $\min_{f\in F} \mathrm{anom}_f(\mathcal S) \le \eta$.
• A deterministic on-line algorithm $A$ maps the list of earlier trials and the current instance to a predicted label. $M_A(\mathcal S)$ is the number of trials $t$ at which $A$'s prediction, computed from $(x_1,y_1),\dots,(x_{t-1},y_{t-1})$ and $x_t$, differs from $y_t$.
• $\mathrm{opt}(F,\eta) = \min_A \sup_{\mathcal S \in S_\eta} M_A(\mathcal S) \in \{0,1,\dots\} \cup \{\infty\}$.

A complete $k$-mistake tree for $F$ is a complete binary tree of height $k$ whose internal nodes carry instances of $X$ such that every labelling of a root-to-leaf path is realized by some $f \in F$; in Lean this is the predicate ShattersTree F k v.

Formalization targets

Goal: Theorem 8.1 (p. 250)

For every class $F$ with $|F| > 1$ and every $\eta \ge 0$,

$$\mathrm{opt}(F,\eta) \ \ge\ \mathrm{opt}(F,0) + 2\eta .$$

The constant $2$ is the paper's, and the statement holds for infinite classes, including those with $\mathrm{opt}(F,0) = \infty$.

Milestones

1. The [Lit88, Lit89b] mistake tree (§8, p. 251): for any pool $F$ there is a complete $\mathrm{opt}(F,0)$-mistake tree. This is published and proved on the platform as UnderstandingML.soa_mistake_bound ($M_{\mathrm{SOA}}(F) \le \mathrm{Ldim}(F)$), referenced together with UnderstandingML.ldim_le_mistake_bound; together they identify $\mathrm{opt}(F,0)$ with the Littlestone dimension.
2. The first stage of the adversary (§8, p. 251): if $F$ has a complete $k$-mistake tree with $k \ge 1$, then against any deterministic algorithm there are $k-1$ trials on which it errs every time, an instance $x$, and two functions $f_1, f_2 \in F$ consistent with all these trials with $f_1(x) \ne f_2(x)$.

Significance

The theorem settles the optimal rate at which mistakes must grow with the number of anomalies for deterministic learners: $2$ per anomaly, uniformly over all non-trivial classes. Together with the upper bounds of §2 of the paper, it shows that the deterministic Weighted Majority algorithm is within an arbitrarily small factor of optimal in its dependence on the anomalies, and it explains the factor of $2$ that separates deterministic from randomized prediction (Theorem 8.2, a separate mission of this series, gives rate $1$ for randomized learners).

The result is proved in the paper; to the best of a search of the platform it has not been formalized. The mission produces a machine-checked lower bound in a general setting: arbitrary domain, arbitrary (possibly infinite) class, extended-natural-valued optimal bounds. The noise-free side, the Littlestone dimension and the Standard Optimal Algorithm, is already published on the platform from Shalev-Shwartz and Ben-David's textbook, and this mission connects it to the noisy setting.

Difficulty

The obvious argument forces one mistake per trial and stops: an adversary that always contradicts the learner leaves no function of $F$ with few anomalies once the trials outnumber the mistake tree. The difficulty is to spend the anomaly budget so that each anomaly buys two mistakes while the sequence stays in $S_\eta$, and to do so against an arbitrary algorithm, which may behave adversarially itself. The definition of $S_\eta$ through a minimum over the class (not a fixed target) and the possibility that $\mathrm{opt}(F,0)$ is infinite both have to be handled.

Formalization scope

• The domain is any type X; the class is F : Set (X → Bool); the hypothesis $|F| > 1$ is F.Nontrivial, which is meaningful for infinite classes (a cardinality ncard would be $0$ there).
• Algorithms, histories and mistake counts are those of the published module UnderstandingML_Online (OnlineAlg X Bool, history, mistakes, ShattersTree); an algorithm is an arbitrary function of the history and the current instance, so every deterministic learner is covered.
• Sequences are Fin T → X × Bool for every finite length T, with repeated instances and conflicting labels allowed.
• opt F η : ℕ∞ is an infimum over algorithms of a supremum over sequences in $S_\eta$; $\eta$ is a natural number. Membership in $S_\eta$ is "some $f \in F$ has at most $\eta$ anomalies", which is the paper's minimum over $F$.
• Swapping the quantifiers (one sequence hard for all algorithms) or replacing $\mathrm{opt}$ by a finite toNat truncation would give a different statement; neither is used.

Needed infrastructure: the identification $\mathrm{opt}(F,0) = \min_A M_A(F)$ (sequences with no anomaly are exactly the realizable ones), the existence of a shattered tree of depth $\mathrm{opt}(F,0)$ from the published Littlestone-dimension results, and the two-stage adversary. Contributions of general lemmas about ShattersTree (subtrees, truncation to smaller depth) are reusable for the randomized mission and beyond.

Selected references

• N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. https://doi.org/10.1006/inco.1994.1009
• N. Littlestone, Learning quickly when irrelevant attributes abound: a new linear-threshold algorithm, Machine Learning 2, 285–318, 1988. https://doi.org/10.1007/BF00116827
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 21. https://doi.org/10.1017/CBO9781107298019

Motivation

Airline and hotel revenue-management systems have traditionally been built around nesting by fare order: classes are ranked by price, and as capacity runs short the cheapest open class is closed first, so that the set of open fares is always a top segment $\{1, \dots, k\}$ of the fare ladder. This structure is what makes booking limits, protection levels and bid-price controls work, and it is optimal in the classical independent-demand model of Lee and Hersh (1993), where each customer wants one specific class.

When customers instead choose among the classes on offer (buying down to a cheaper fare, or not buying at all when their preferred fare is closed), the optimal policy need not be nested by fare order. Talluri and van Ryzin (2001 working paper; Management Science 2004) formulate single-resource capacity control under a general discrete choice model and ask which choice models still have optimal policies nested by fare order. Their Theorem 2 answers this with a characterization in terms of the choice probabilities alone. The paper's later sections use it to show that the independent-demand and multinomial-logit models have the property; the mission on the multinomial-logit model in this series builds on that.

Setting

There are $n$ fare products $N = \{1, \dots, n\}$, indexed so that $r_1 \ge r_2 \ge \dots \ge r_n \ge 0$. A choice model assigns to every offer set $S \subseteq N$ and product $j$ a probability $P_j(S) \ge 0$ that an arriving customer buys $j$ when $S$ is offered, with $P_j(S) = 0$ for $j \notin S$ and purchase probability $Q(S) = \sum_{j \in S} P_j(S) \le 1$; the remainder $P_0(S) = 1 - Q(S)$ is the probability of no purchase.

A set is complete if it has the form $A_k = \{1, \dots, k\}$, $k = 0, 1, \dots, n$ (with $A_0 = \emptyset$), and incomplete otherwise. For values $x_1 \ge x_2 \ge \dots \ge x_n$ (in the dynamic program, $x_j = r_j - v$ for a marginal value of capacity $v$), consider the static problem

$$\max_{S \subseteq N} \sum_{j=1}^n x_j P_j(S). \tag{9}$$

The choice model has the nesting-by-fare-order property (Definition 4) if (i) $Q$ is increasing, $Q(S) \le Q(T)$ for $S \subseteq T$, and (ii) for every $x_1 \ge \dots \ge x_n$, problem (9) has an optimal solution that is complete. For convex weights $\alpha_0, \dots, \alpha_n$ write $\bar P_j(\alpha) = \sum_{k=0}^n \alpha_k P_j(A_k)$ for the purchase probabilities of the corresponding randomized mixture of complete sets.

Formalization targets

Goal: Theorem 2 (p. 19)

The choice model has the nesting-by-fare-order property if and only if $Q$ is increasing and, for every incomplete set $T$, there are convex weights $\alpha$ such that

$$\sum_{j=1}^i \bar P_j(\alpha) \ge \sum_{j=1}^i P_j(T) \quad (i = 1, \dots, n-1), \qquad \sum_{j=1}^n \bar P_j(\alpha) = \sum_{j=1}^n P_j(T).$$

That is, some mixture of complete sets majorizes $(P_1(T), \dots, P_n(T))$ in fare order. Both directions are part of the goal, and the right-hand side contains no optimization over $x$.

Milestones (the paper's proof, in order)

1. Condition (ii) of Definition 4 holds iff, for every incomplete $T$, the linear system (10)–(11) — values $x_1 \ge \dots \ge x_n$ and a scalar $u$ with $u < \sum_{j \in T} x_j P_j(T)$ and $\sum_{j \in A_k} x_j P_j(A_k) \le u$ for all $k$ — has no solution (p. 20).
2. For one set $T$: (10)–(11) has no solution iff the dual system in $(\alpha, z)$ is solvable (Farkas' lemma, p. 20).
3. For one set $T$: eliminating $z$, the dual system is solvable iff the prefix-sum conditions above hold (pp. 20–21).
4. A mixture satisfying the prefix-sum conditions earns at least as much as $T$ in (9) for every $x_1 \ge \dots \ge x_n$ (pp. 19–20).

Companions

The paper remarks (p. 21) that the proof never uses completeness: the same characterization holds for any specified family of offer sets $F_1, \dots, F_m$ in place of the complete sets. Example 2 (pp. 18–19) gives a three-product model, arising from a mixture of two customer types, in which the incomplete set $\{1, 3\}$ is the unique maximizer of (9) at $x = (400, 100, 50)$, so the property fails.

Significance

Theorem 2 turns a statement quantified over all value vectors $x$ and all $2^n$ offer sets into a finite collection of linear feasibility problems, one per incomplete set, involving only the choice probabilities. Combined with the paper's Theorem 1 (the optimal policy offers nondominated sets, nested in capacity and time), it gives a checkable criterion for when a nested-by-fare-order booking-limit or bid-price policy is optimal under customer choice. The paper uses it to verify the property for the independent-demand model (Proposition 5) and the multinomial-logit model (Proposition 6), and the p. 21 remark makes it a tool to test conjectures that optimal offer sets come from another structured family.

The result is proved in the paper; the mission's contribution is a machine-checked version of the characterization and of each proof step, which are the reusable pieces for the follow-up mission on the multinomial-logit model. Farkas' lemma in inequality form is already formalized on the platform (LinearOptimization.farkas_inequality_form, referenced here); the theorem of this mission is not.

Difficulty

The argument is short on paper but the bookkeeping is where the content sits. The reduction of Definition 4(ii) to infeasibility of (10)–(11) needs care with ties: (9) only needs some complete optimum, so the system asks that $T$ beat every complete set strictly, not that $T$ be the unique optimum. The dual system must then be matched exactly to the primal: the multiplier of the ordering constraint $x_j \ge x_{j+1}$ enters two adjacent equations, the boundary multipliers $z_0$ and $z_n$ are fixed at zero, and the inhomogeneous constraint on $u$ is what forces $\sum_k \alpha_k = 1$. A naive application of Farkas' lemma to the strict system, without homogenizing in $u$, gives the wrong normalization. The boundary case $j = n$ is what produces the equality of totals rather than a further inequality, and the fare order of $x$ is the only link between the prefix-sum conditions and revenue.

Formalization scope

Products are Fin n (product $j$ is the element $j - 1$), offer sets are Finset (Fin n), probabilities are real. The choice-model axioms are the platform definition RevenueManagement.IsChoiceModel ($P_j(S) \ge 0$ and $Q(S) \le 1$), reused by reference, together with the model's own standing convention $P_j(S) = 0$ for $j \notin S$ (SupportedOn), which is needed because $\bar P_j$ and the totals sum over all products. The order $x_1 \ge \dots \ge x_n$ is Antitone x. The maximum in (9) is over all subsets of $N$.

Complete sets are $A_k$ for $k = 0, \dots, n$, so $A_0 = \emptyset$ is complete and the weights $\alpha$ live on $n + 1$ sets. The page indexes the weights by $k = 1, \dots, n$; with $A_0$ included the property is the one the paper's applications need (for the multinomial-logit model and all $x_j < 0$ the unique optimum of (9) is $\emptyset$), and the family companion contains the page's literal $k = 1, \dots, n$ version as an instance. The prefix conditions are stated for $i = 0, \dots, n - 1$, where $i = 0$ is trivial.

A formalization that put an optimization over $x$ on the right-hand side of the goal, or dropped condition (i) from either side, would be a restatement rather than the characterization; the goal's right-hand side mentions only the choice probabilities.

The development needs finite sums over Fin n, and a Farkas lemma (available on the platform). Proofs of the milestones and of the companions are welcome individually; the family version of the characterization is reusable for any conjectured family of optimal offer sets.

Selected references

• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, working paper, October 21, 2001 (UPF Economics Working Paper 533); published in Management Science 50(1):15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
• T. C. Lee, M. Hersh, A model for dynamic airline seat inventory control with multiple seat bookings, Transportation Science 27(3):252–265, 1993. https://doi.org/10.1287/trsc.27.3.252
• A. W. Marshall, I. Olkin, B. C. Arnold, Inequalities: Theory of Majorization and Its Applications, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-0-387-68276-1
• K. Talluri, G. van Ryzin, The Theory and Practice of Revenue Management, Kluwer, 2004, §2.6.2. https://doi.org/10.1007/b139000

Motivation

A cutting-stock shop receives orders for pieces of several lengths and cuts them from a limited menu of longer stock lengths. Each stock length has a cost. The shop can repeat any cutting pattern, so the central optimization question is which patterns meet the demand at least cost. The direct linear program has a variable for every possible pattern. Even a modest menu of piece lengths can yield too many columns to list before optimization begins. Gilmore and Gomory's 1961 article addresses this large-column obstacle by testing whether an as-yet-unlisted pattern could lower the cost of a current basic solution.

The article studies the linear programming relaxation: cutting activities may have nonnegative real weights rather than integer repetition counts. It does not claim that the resulting fractional optimum is always an integer cutting plan. Its worked example happens to have an integer optimum of cost 170; the authors explicitly note that this integrality is fortuitous (Gilmore and Gomory 1961, p. 858). The target here is the exact stopping condition for the relaxation.

Setting

An instance has $m$ ordered piece lengths $\ell_i$, demand $N_i\in\mathbb N$ for each piece length, and $k$ stock lengths $L_j$ with real costs $c_j$. A cutting pattern for stock $j$ is a vector of nonnegative integer counts $a_i$ with $\sum_i\ell_i a_i\le L_j$. An activity consists of that stock choice and its fitting pattern. Its demand column is $a=(a_i)$ and its cost is $c_j$. A surplus column for demand row $i$ has coefficient $-1$ in that row, zero elsewhere, and zero cost. The paper uses such columns to turn its demand inequalities into equations (Gilmore and Gomory 1961, p. 850, (1)–(3)).

A feasible solution assigns nonnegative real weights to finitely many activities and surplus columns so that activity output minus surplus equals $N_i$ in every row. Its cost is the weighted sum of stock costs. A basis $\beta$ lists $m$ columns with invertible coefficient matrix $A$ and cost row $C$. The associated bordered matrix, demand column, tableau column, and multipliers are

$$B=\begin{pmatrix}1&-C\\0&A\end{pmatrix},\qquad N'=(0,N_1,\ldots,N_m)^T,\qquad \bar N=B^{-1}N',\qquad b_i=(B^{-1})_{0,i+1}.$$

A feasible basis has nonnegative basic values, the last $m$ entries of $\bar N$. Those values on the basic columns, with zero on every other column, form the current basic solution. The first entry of $\bar N$ is its cost. These definitions follow the matrix and tableau of routine steps (2)–(4) (Gilmore and Gomory 1961, pp. 854–855).

Formalization targets

The goal is the stopping statement of step (4). If no nonbasic surplus column has a negative multiplier, and no available stock $j$ has a fitting pattern satisfying $\sum_i b_i a_i>c_j$, then the current solution is feasible and minimizes cost across all feasible activity and surplus assignments:

$$\bigl(\forall i\text{ with surplus }i\notin\beta,\ b_i\ge0\bigr) \quad\land\quad \bigl(\forall j,a,\ \sum_i\ell_i a_i\le L_j\Rightarrow\sum_i b_i a_i\le c_j\bigr) \quad\Longrightarrow\quad \operatorname{cost}(z_\beta)=\bar N_0\le\operatorname{cost}(z) \quad\text{for every feasible }z.$$

The six milestones record the paper's ingredients: the first row of $B^{-1}$ and the meaning of $\bar N$; the entering-column price test (4)–(5); the surplus-column test of step (3); the integer-pattern form (6)–(7); the maximum-pattern test; and the dynamic programming recurrence for $F_s(x)$ (Gilmore and Gomory 1961, pp. 852–855). The paper has no numbered theorems or lemmas; each milestone is drawn from a sentence or display on those pages.

Significance

The result makes a finite tableau a certificate for an optimization problem whose set of potential cutting activities is much larger than the current basis. A failed pricing search is meaningful only when it covers every fitting pattern for every stock length; the goal makes that full scope explicit. In the example, the final multipliers are $(2,3,5)$ and the relevant knapsack maxima for stock lengths $5$, $6$, and $9$ are $5$, $7$, and $10$, matching their stopping prices and the cost 170 (Gilmore and Gomory 1961, p. 858).

The mathematical argument is known from the 1961 article. This mission asks for a machine-checked Lean proof of its particular cutting-stock formulation, including the bounded-pattern search, bordered tableau, surplus columns, and global optimality conclusion. The proposal statements compile with proof placeholders; they are not already proved by those placeholders. Published general LP results are listed as references, but their finite-indexed formulations do not directly state the cutting-stock theorem.

Difficulty

Checking only the columns already in a tableau cannot establish optimality: an unlisted pattern might still fit a stock length and have a price greater than its cost. The article reduces this large search to an integer knapsack maximum for each stock length (Gilmore and Gomory 1961, pp. 852–853). Formalization must retain the distinction between a basis of $m$ columns and the full collection of possible columns. Strict improvement also needs care at a degenerate basic solution. The paper directs zero-ratio pivots to a separate degeneracy procedure (Gilmore and Gomory 1961, p. 855); the sufficient directions of the pricing milestones therefore require positive basic values, while the goal's optimality direction does not.

Formalization scope

Lean indexes piece types from zero and uses a separate initial cost coordinate followed by the $m$ demand coordinates for $B$. Thus the paper's $(i+1)$st bordered row corresponds to Lean demand index $i$. Patterns are vectors in $\mathbb N^m$; the zero pattern is included. A solution is a finitely supported real weighting of all activity and surplus columns. Global minimality quantifies over every such feasible weighting, including activities not in the current basis. No sign condition is imposed on stock costs or stock lengths in the goal; the goal is a conditional optimality statement and remains valid whenever its hypotheses hold.

The knapsack value $F_s(x)$ uses extended real numbers, giving $-\infty$ when no pattern fits, rather than an accidental real value from an empty supremum. The maximum-pattern milestone assumes positive piece lengths and nonnegative stock length, so the feasible set is finite and nonempty. The recursion milestone assumes positive lengths for all types through the newly added one; without the earlier positivity, a negative earlier length could let the new piece count exceed the displayed upper bound. The nondegeneracy hypotheses are confined to the sufficient directions of the three improvement milestones.

Reusable contributions include lemmas connecting the bordered inverse with $C A^{-1}$, finite-support linear program identities, and the integer knapsack recurrence. The source's rounding discussion, heuristic search, and under-specified anti-cycling device are outside this mission. An encoding that compares the current solution only with basis columns or generated columns would miss the paper's stopping claim.

Selected references

• P. C. Gilmore and R. E. Gomory, A linear programming approach to the cutting-stock problem, Operations Research 9(6):849–859, 1961. DOI: 10.1287/opre.9.6.849.

Motivation

A Markov decision process with finitely many states and actions and a discounted cost criterion can be solved in three classical ways: policy iteration, value iteration, and linear programming. The third goes back to F. d'Epenoux's paper A Probabilistic Production and Inventory Problem (Management Science 10(1), 1963, partly redrafted from a translation of d'Epenoux's 1960 article in the Revue Française de Recherche Opérationnelle), which showed that the optimal discounted cost of a stochastic production and inventory model is the solution of a single linear program. Together with Manne's linear program for the average-cost case (1960), it is the origin of the linear programming approach to dynamic programming, which underlies occupation-measure methods, constrained Markov decision processes, and approximate linear programming for large models.

Timeline:

• 1957–1960. Bellman's Dynamic Programming (value iteration, the principle of optimality); Howard's policy iteration for average costs (1960); Manne's linear program for average costs (Linear programming and sequential decisions, Management Sci., 1960).
• 1960/1963. d'Epenoux treats the discounted case: policy iteration and value iteration (Sections 2–4), then the linear program $(P_2)$ and its dual (Sections 5–6). Footnote 2 credits Guilbaud (1957) with an earlier observation of an equivalent linear program in another context.
• 1967. Denardo, Contraction mappings in the theory underlying dynamic programming, places the linear programs in an abstract contraction framework.

Setting

The stock at the beginning of a period is $i \in \{0, 1, \dots, \sigma\}$, where $\sigma$ is the stock capacity. The decision is the potential $j$, the quantity available for the period (output plus initial stock), with $i \le j \le \sigma$. Given the potential $j$, the stock at the end of the period is $s$ with probability $p_{js}$; each row $(p_{js})_s$ is a probability vector. The expected cost of a period with initial stock $i$ and potential $j$ is a real number $d_{ij}$. Costs one period ahead are discounted by $\lambda$, $0 < \lambda < 1$.

A strategy is a map $J$ with $i \le J(i)$ for every $i$: the potential depends only on the current stock. It has the transition matrix $(P_J)_{is} = p_{J(i)s}$ and the cost vector $(d_J)_i = d_{iJ(i)}$. The cost of following $J$ forever is the solution $u$ of (2), $u = d_J + \lambda P_J u$. The optimal cost $u^*$ solves the fundamental equation (7),

$$u^*_i = \min_{j \ge i}\Big( d_{ij} + \lambda \sum_{s=0}^{\sigma} p_{js} u^*_s \Big), \qquad i = 0, \dots, \sigma .$$

For a vector $u$ put $U_{ij} = u_i - \lambda \sum_s p_{js} u_s - d_{ij}$. The set $A$ consists of the vectors satisfying the linear constraints (9), $U_{ij} \le 0$ for all admissible pairs $i \le j$. The set $B$ consists of the vectors with $\prod_{j \ge i} U_{ij} = 0$ for every $i$.

Formalization targets

Goal: $u^* = \max(u \in A)$, and $(P_2)$

The system (7) has a solution, and every solution $u^*$ is the greatest element of $A$:

$$u^* \in A, \qquad u \le u^* \ \text{componentwise for every } u \in A .$$

Moreover, for every weight vector $c$ with all $c_i > 0$ and $\sum_i c_i = 1$, $u^*$ is the unique optimal solution of

$$(P_2) \qquad \text{maximize } (1-\lambda) \sum_i c_i u_i \quad \text{subject to } U_{ij} \le 0 \ \ (i \le j).$$

Milestones

1. Eq. (3). For a stochastic matrix $P$ and $0<\lambda<1$, $I - \lambda P$ is invertible and $(I-\lambda P)^{-1} = \sum_{k \ge 0} \lambda^k P^k$.
2. Eq. (4). $u - \lambda P u \ge 0$ implies $u \ge 0$.
3. Eq. (5). If moreover $u - \lambda P u \ne 0$ and $P$ is indecomposable, then $u_i > 0$ for all $i$.
4. Eq. (7). (7) has a unique solution, the cost of an optimal strategy (referenced, Proved).
5. Section 5. $u$ solves (7) iff $u \in A \cap B$; the points of $B$ are exactly the costs of strategies.
6. Section 5. Every point of $A$ lies below every point of $B$.
7. Section 5. If every $P_J$ is indecomposable, $u^*$ is a strict vectorial maximum of $A$: $u \in A$, $u \ne u^*$ imply $u_i < u^*_i$ for all $i$.

Significance

The result turns a fixed-point equation with a minimum in it into a linear program with $\tfrac12(\sigma+1)(\sigma+2)$ linear constraints. Its consequences are the ones the paper draws in Section 6: the dual of $(P_2)$ has a probabilistic interpretation (discounted state–action frequencies), its optimal basic solutions are optimal strategies, and every linear programming algorithm becomes an algorithm for discounted dynamic programs. The uniqueness clause is what makes the weighted objective recover the whole cost vector; with a single objective $u_e$, as the paper notes, the optimum need not determine the complete optimal strategy when the states decompose into several groups.

The dynamic programming half of the paper (Sections 2–4: policy evaluation, policy iteration, value iteration) is already formalized and proved on the platform for the general finite discounted model, as Bertsekas, Dynamic Programming and Optimal Control, Prop. 7.3.1 (BertsekasDP.discounted_main_theorem); it enters this mission as a reference item, and the mission's model is an instance of the same published structure BertsekasSSPModel. The linear programming half is not formalized. Related items in other models are posed elsewhere: Bäuerle and Rieder's Theorem 7.5.9 (finite-state linear program in a measure-theoretic reward model, open) and Denardo's Programs I–II in an abstract contraction model; neither states the componentwise maximality of $u^*$ in $A$ in this model.

Difficulty

The individual steps are short, but the goal combines several facts that are easy to state wrongly. The paper calls the invertibility of $I-\lambda P$ and the positivity of its inverse "known and obvious"; in Lean they are statements about an arbitrary stochastic matrix over Fin m, for which Mathlib provides no default matrix norm, and the comparison of $A$ with $B$ depends on them. Uniqueness of the optimum of $(P_2)$ needs both strict positivity of the weights and the componentwise maximality; with a zero weight it fails. The obvious first idea for the strict maximum, that indecomposability of the optimal strategy's matrix alone suffices, is not the formalized statement: only the sufficient condition over all strategies is posed.

Formalization scope

Stock levels and potentials are Fin (σ + 1), $0$-based. The kernel $p_{js}$ is an arbitrary stochastic kernel indexed by the potential, and the costs $d_{ij}$ are arbitrary reals; the paper's demand-driven kernel and its cost decomposition $d_{ij} = d'(j-i) + \sum_n p_n d''(i,j,n)$ are an instance and are not built in, because the arguments of Sections 2–5 use only stochasticity (the paper itself remarks on p. 101 that its methods apply far beyond the inventory problem). Only admissible pairs $i \le j$ enter $A$, $B$, the minimum in (7), and strategies. The discount is called lam in Lean. Equation (7) is the fixed-point equation of the Bellman operator BertsekasDiscountedBellmanOp of the model.

Explicit readings of the paper's phrases:

• "$u^* = \max(u \in A)$" is IsGreatest in the componentwise order.
• "the complete solution" of $(P_2)$ is uniqueness of its optimal solution, for every admissible weight vector.
• "$u > 0$" in (5) and "strict vectorial maximum" mean every component strictly positive, respectively strictly smaller.
• "indecomposable" means irreducible: for all $i,k$ some power $P^n$ has $(P^n)_{ik} > 0$. The weaker reading (one closed class plus transient states) makes (5) false.
• "the points of the set $B$ correspond to the costs associated with every possible strategy" is the equivalence between membership in $B$ and solving (2) for some strategy.

Ruled out: defining $u^*$ as the optimum of the linear program, as a supremum of $A$, or as a limit (which would make the goal circular); assuming a solution of (7) without the existence conjunct; constraining also the inadmissible pairs $j < i$ (which can exclude $u^*$ from $A$); and weakening the weights to $c_i \ge 0$.

Not formalized: the demand-driven kernel, the finite-horizon recursion of Section 2, the monotone convergence remark of Section 4 (c), the count of strategies, the reformulations $(P_1)$ and $(P_3)$, and all of Section 6 (duality). Contributions welcome: proofs of the milestones and of the goal, and, as a follow-up mission, the dual programs of Section 6. The matrix facts (3)–(5) are stated for arbitrary stochastic matrices and are reusable beyond this mission.

Selected references

• F. d'Epenoux, A Probabilistic Production and Inventory Problem, Management Science 10(1), 98–108, 1963. https://doi.org/10.1287/mnsc.10.1.98
• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3), 259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press and John Wiley, 1960.
• R. Bellman, Dynamic Programming, Princeton University Press, 1957.
• E. V. Denardo, Contraction Mappings in the Theory Underlying Dynamic Programming, SIAM Review 9(2), 165–177, 1967. https://doi.org/10.1137/1009030
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Prop. 7.3.1.
• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Section 7.5. https://doi.org/10.1007/978-3-642-18324-9

Motivation

The ellipsoid method is the cutting-plane algorithm that settled the polynomial-time solvability of linear programming and, more generally, of convex optimization over any set that comes with an efficient separation oracle. It was introduced for convex minimization by Shor and by Yudin and Nemirovski in the 1970s, and Khachiyan used it in 1979 to give the first polynomial-time algorithm for linear programming. Grötschel, Lovász and Schrijver later turned it into the general equivalence between separation and optimization that underlies much of combinatorial optimization.

This mission is the second of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980v2). Its goal is the convergence guarantee of the ellipsoid method, Theorem 2.4 (p. 250), together with the geometric lemma and the steps of the proof on which it rests.

Timeline:

• 1976–1977: Yudin–Nemirovski and Shor introduce the method for convex minimization.
• 1979: Khachiyan applies it to linear programming and obtains polynomial time.
• 1981: Grötschel, Lovász and Schrijver derive the equivalence of separation and optimization.

Setting

Write $\mathbb R^n$ for the space of real $n$-vectors, with the dot product $x^\top y$. An ellipsoid is a set

$$\mathcal E=\{x\in\mathbb R^n:(x-c)^\top H^{-1}(x-c)\le 1\},$$

where $c\in\mathbb R^n$ is its center and $H$ is a symmetric positive definite matrix.

A convex body $\mathcal X\subset\mathbb R^n$ is a compact convex set with non-empty interior. The objective $f$ is continuous and convex on $\mathcal X$ with values in $[-B,B]$, and $r,R>0$ are such that $\mathcal X$ lies in the Euclidean ball $\mathcal E_0$ of center $c_0$ and radius $R$ and contains some Euclidean ball of radius $r$. A subgradient of $f$ at $x\in\mathcal X$ is a vector $g$ with $f(x)+g^\top(y-x)\le f(y)$ for all $y\in\mathcal X$.

The method starts from $\mathcal E_0$, $H_0=R^2\mathrm I_n$. At step $t\ge0$ it asks for a vector $w_t$:

• if $c_t\notin\mathcal X$, a separating vector, with $\mathcal X\subset\{x:(x-c_t)^\top w_t\le0\}$;
• otherwise a subgradient of $f$ at $c_t$.

It then replaces $\mathcal E_t$ by the ellipsoid $\mathcal E_{t+1}$ given by

$$c_{t+1}=c_t-\frac1{n+1}\frac{H_tw_t}{\sqrt{w_t^\top H_tw_t}},\qquad H_{t+1}=\frac{n^2}{n^2-1}\Big(H_t-\frac2{n+1}\frac{H_tw_tw_t^\top H_t}{w_t^\top H_tw_t}\Big).$$

After $t$ iterations the output $x_t$ is the best of the queried centers that lie in $\mathcal X$.

Formalization targets

Goal: Theorem 2.4

For $n\ge2$ and every $t\ge 2n^2\log(R/r)$, $t\ge1$, some queried center lies in $\mathcal X$, and every output satisfies

$$f(x_t)-\min_{x\in\mathcal X}f(x)\le\frac{2BR}{r}\exp\Big(-\frac{t}{2n^2}\Big).$$

Milestones

1. The scalar inequality $(1+1/n)^2(1-1/n^2)^{n-1}\ge\exp(1/n)$ for $n\ge2$ (proof of Lemma 2.3, pp. 248–249).
2. Lemma 2.3 (p. 247): for $w\ne0$ the half-ellipsoid $\{x\in\mathcal E_0:w^\top(x-c_0)\le0\}$ lies in an ellipsoid $\mathcal E$ with

$$\mathrm{vol}(\mathcal E)\le\exp\Big(-\frac1{2n}\Big)\mathrm{vol}(\mathcal E_0),$$

and for $n\ge2$ the explicit ellipsoid (2.5)–(2.6) works. 3. The remark before Theorem 2.4 (p. 250): a point of $\mathcal X$ can leave the current ellipsoid only at a step with $c_t\in\mathcal X$, and then its value exceeds $f(c_t)$. 4. Two steps reused from Theorem 2.1 (pp. 246–247): $\mathrm{vol}(\mathcal X_\varepsilon)=\varepsilon^n\mathrm{vol}(\mathcal X)$ for $\mathcal X_\varepsilon=(1-\varepsilon)x^*+\varepsilon\mathcal X$, and $f\le f(x^*)+2\varepsilon B$ on $\mathcal X_\varepsilon$.

Significance

Theorem 2.4 bounds the oracle complexity of the ellipsoid method: accuracy $\varepsilon$ needs $O(n^2\log(1/\varepsilon))$ oracle calls. Each step costs $O(n^2)$ arithmetic operations plus one oracle call. With the separation oracles of linear and semidefinite programs this gives polynomial overall complexity (p. 250). The rate depends on the instance only through $\log(R/r)$ and $B$, so the method needs no smoothness and no strong convexity. Lemma 2.3 is also the geometric step of the ellipsoid method for linear feasibility.

The result has a textbook proof. The work of this mission is to formalize it. The same update is published on the platform from Bertsimas and Tsitsiklis's Introduction to Linear Optimization (Theorem 8.1), with a proved volume factor of $\exp(-1/(2(n+1)))$. That factor is weaker than (2.4)'s $\exp(-1/(2n))$ and does not give Theorem 2.4's constant. The sharper factor and the optimization version of the method (subgradient cuts, the output rule and the value bound) are not formalized on the platform.

Difficulty

There are two difficulties: Lemma 2.3 with the sharp constant, and the bookkeeping that turns per-step volume decrease into a value bound.

For the lemma, the volume of the explicit ellipsoid is $\big(n/\sqrt{n^2-1}\big)^n\sqrt{(n-1)/(n+1)}$ times that of $\mathcal E_0$. Bounding it by $\exp(-1/(2n))$ rather than by the cruder $\exp(-1/(2(n+1)))$ needs the scalar inequality of milestone 1 for every $n\ge2$. The reduction from a general ellipsoid to the unit ball also needs determinants under an affine map.

For the theorem, the obvious argument compares $\mathrm{vol}(\mathcal X_\varepsilon)$ with $\mathrm{vol}(\mathcal E_t)$. This only works if no cut removes an optimal point and if every removed point of $\mathcal X$ is worse than a queried center. At the threshold $t=2n^2\log(R/r)$ the admissible $\varepsilon$ is exactly $1$, so a non-strict volume bound alone does not close the argument there.

Formalization scope

• $\mathbb R^n$ is Fin n → ℝ with Lebesgue measure, as in the reused Bertsimas–Tsitsiklis ellipsoid definitions (LinearOptimization.ellipsoid, ellipsoidUpdateCenter, ellipsoidUpdateMatrix, IsSubgradientOn).
• Euclidean balls are written with the dot product, because Mathlib's norm on Fin n → ℝ is the sup norm.
• The method is a run predicate, IsEllipsoidRun. Every theorem holds for every admissible oracle answer. The update is the published one with $a=-w_t$.
• If an oracle answer is $w_t=0$ (possible only at a minimizer $c_t\in\mathcal X$), the run stops. The page's update would divide by zero there.

Conventions and hypotheses added to the page:

1. $n\ge2$, because the update (2.6) is defined only for $n\ge2$.
2. A minimizer $x^*$ exists (the book's standing assumption, p. 242).
3. The output ranges over the queried centers $c_0,\dots,c_{t-1}$. The page writes $\{c_1,\dots,c_t\}$, but $c_t$ has not been cut yet and $c_0$ has.
4. $t\ge1$, because at $R=r$ and $t=0$ no center has been queried.

A run predicate whose separation branch does not require $\mathcal X\subset\{x:(x-c_t)^\top w_t\le0\}$, or that accepts $w_t=0$ with an update, would make the statements false or vacuous. Both are excluded.

Lemma 2.3's volume factor is $\exp(-1/(2n))$. The weaker published factor does not prove that milestone. The published theorem LinearOptimization.ellipsoid_update_halfspace_volume is included as a reference: it supplies the containment (2.3) and positive definiteness. Contributions are welcome on every milestone. A determinant formula for the volume of an ellipsoid would be reusable well beyond this mission.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2
• N. Z. Shor, Cut-off method with space extension in convex programming problems, Cybernetics 13:94–96, 1977. doi:10.1007/BF01071394
• D. B. Yudin and A. S. Nemirovski, Informational complexity and efficient methods for the solution of convex extremal problems, Matekon 13(2):22–45, 1976.
• L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Mathematics Doklady 20:191–194, 1979.
• M. Grötschel, L. Lovász and A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1:169–197, 1981. doi:10.1007/BF02579273
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 8.1).

Motivation

Every linear program comes with a second linear program, its dual, whose feasible solutions certify bounds on the optimum of the first. The duality theorem of linear programming says that these certificates are perfect: when both programs are feasible, the best bound equals the optimum. The theorem underlies the analysis of the simplex method, sensitivity analysis and shadow prices in operations research, the minimax theorem for zero-sum games, max-flow/min-cut and König-type min-max theorems in combinatorial optimization, and the primal–dual design of approximation and online algorithms.

The Farkas lemma, a theorem of the alternative for linear systems, contains the essence of duality: a system of linear equations or inequalities either has a (nonnegative) solution, or a single linear combination of its rows proves that it has none. It goes back to Farkas (1902) and Minkowski's work on finitely generated cones; the duality theorem itself is due to von Neumann (1947) and Gale, Kuhn and Tucker (1951).

This mission formalizes Chapter 6 of Matoušek and Gärtner's textbook Understanding and Using Linear Programming (Springer, 2007): the duality theorem in the book's form, weak duality, the Farkas lemma in its algebraic, geometric and three-variant forms, and the lemmas of two self-contained proofs of the Farkas lemma, one analytic (nearest points in finitely generated cones) and one via minimally infeasible systems.

Setting

Let $A$ be a real matrix with $m$ rows and $n$ columns, $b\in\mathbb{R}^m$, $c\in\mathbb{R}^n$. Vector inequalities are componentwise. The primal and dual linear programs are

$$\text{(P)}\quad\max\ c^{T}x \ \text{ s.t. } Ax\le b,\ x\ge 0, \qquad\qquad \text{(D)}\quad\min\ b^{T}y \ \text{ s.t. } A^{T}y\ge c,\ y\ge 0.$$

A feasible solution of (P) is an $x\in\mathbb{R}^n$ satisfying its constraints; an optimal solution is a feasible $x^*$ with $c^{T}x\le c^{T}x^*$ for every feasible $x$. (P) is unbounded if its objective takes arbitrarily large values on feasible solutions. For the minimization (D) the notions are mirrored: an optimal $y^*$ has $b^{T}y^*\le b^{T}y$ for all feasible $y$, and (D) is unbounded if $b^{T}y$ takes arbitrarily small values.

For $a_1,\dots,a_n\in\mathbb{R}^m$, the convex cone generated by them is $C=\{t_1a_1+\dots+t_na_n : t_i\ge 0\}$; a primitive cone is one generated by $k\le m$ linearly independent vectors. A system $Ax\le b$ of $m$ inequalities is minimally infeasible if it has no solution but dropping any one inequality makes it solvable.

Formalization targets

Goal: the duality theorem (§6.1, p. 83)

For (P) and (D) as above, exactly one of the following occurs:

1. neither (P) nor (D) is feasible;
2. (P) is unbounded and (D) is infeasible;
3. (P) is infeasible and (D) is unbounded;
4. both are feasible; then both have optimal solutions, and every optimal $x^*$ of (P) and optimal $y^*$ of (D) satisfy

$$c^{T}x^*=b^{T}y^*.$$

Milestones

• Proposition 6.1.1 (weak duality). $c^{T}x\le b^{T}y$ for all feasible $x$ of (P) and $y$ of (D); hence (P) unbounded forces (D) infeasible, and (D) unbounded forces (P) infeasible.
• Proposition 6.4.1 (Farkas lemma). Exactly one of: $Ax=b$ has a solution $x\ge 0$; some $y$ has $y^{T}A\ge 0^{T}$ and $y^{T}b<0$. Already on the platform as LinearOptimization.farkas_lemma (Proved) and linked as a reference.
• Proposition 6.4.3 (three variants). Solvability of $Ax=b$, $x\ge0$; of $Ax\le b$, $x\ge 0$; and of $Ax\le b$ with $x$ free, each characterized by a certificate condition on $y$.
• Proposition 6.4.2 (geometric Farkas lemma). $b$ lies in the cone generated by $a_1,\dots,a_n$, or a hyperplane through $0$ separates the cone from $b$ strictly — exactly one.
• Lemmas 6.5.4, 6.5.5, 6.5.3, 6.5.1. Primitive cones are closed; a finitely generated cone is a finite union of primitive cones; hence it is closed (6.5.3, on the platform as Polyhedral.isClosed_conicSpan, Proved); hence it has a point nearest to any $b\notin C$.
• Lemmas 6.6.2 and 6.6.1. $Ax=b$ is solvable iff every $y$ with $y^{T}A=0^{T}$ has $y^{T}b=0$; in a minimally infeasible system, for every $i$ some $\tilde x^{(i)}$ satisfies all inequalities except the $i$th with equality.

Significance

The result. The duality theorem converts optimality into feasibility: a pair $(x,y)$ of primal and dual feasible solutions with $c^{T}x=b^{T}y$ is a short, checkable certificate that both are optimal, and the theorem guarantees such a certificate exists whenever an optimum does. It classifies every primal–dual pair into four behaviours and excludes the other five combinations of feasible-bounded, unbounded and infeasible. Later chapters of the same book rest on it: the minimax theorem for zero-sum games, the integrality of bipartite matching polytopes, the LP rounding for unrelated-machine scheduling, and the Delsarte bound for codes.

Formalizing it. All results here are classical and fully proved in the book; the work is formalization. Mathlib contains a Farkas lemma for proper cones in Hilbert spaces and closedness facts for finitely generated cones, and the platform already has Bertsimas–Tsitsiklis-style duality for a general-form minimization (LinearOptimization.lp_strong_duality) and matrix Farkas lemmas. What is missing is the textbook statement in Matoušek's inequality form (P)/(D), with its four-case exclusive classification, together with the chain of named lemmas that make two different elementary proofs of the Farkas lemma machine-checkable. The analytic chain (6.5.x) and the minimally-infeasible chain (6.6.x) are reusable independently of LP.

Difficulty

Weak duality is a two-line computation. The difficulty is entirely in the reverse direction, that a feasible bounded (P) forces the dual to be feasible with the same value. Any proof must use something beyond linear algebra over $\mathbb{R}$: either the termination of the simplex method with an anticycling rule, a topological fact (a finitely generated cone is closed), or an extremal argument (an optimal solution of an auxiliary LP). The naive geometric argument — take the nearest point of the cone to $b$ — fails without closedness, and closedness of the cone generated by a set is false for infinitely generated cones (the cone over a disc touching the origin is an open half-plane plus a point), so finiteness has to be used, which is the role of the primitive-cone decomposition. In the four-case theorem itself, the remaining obstacle is attainment: "bounded and feasible" must be upgraded to "an optimum exists" for both programs, which is not a consequence of Farkas-type statements alone.

Formalization scope

• Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; the book's indices $1,\dots,n$ become $0,\dots,n-1$. The row vector $y^{T}A$ is Aᵀ *ᵥ y, so $y^{T}A\ge 0^{T}$ is 0 ≤ Aᵀ *ᵥ y; scalar products are ⬝ᵥ.
• Optimal solutions and unboundedness are stated against every feasible point; no sSup/sInf is used, so no junk value of an empty or unbounded supremum enters. "Exactly one of the four cases" is ∃! k : Fin 4, DualityCase A b c k, with the book's case $k$ at index $k-1$; a plain disjunction would be weaker than the book.
• Cone items live in EuclideanSpace ℝ (Fin m), so the nearest point of Lemma 6.5.1 is Euclidean and $y^{T}x$ is the inner product. The convex cone generated by $a_1,\dots,a_n$ is the set of nonnegative combinations (it contains $0$, also for $n=0$).
• A trivializing formalization — case 4 read as "if both have optimal solutions then their values agree", which is weak duality plus nothing — is ruled out: case 4 asserts the existence of both optima from feasibility alone.
• Lemma 6.3.1 (the dual solution read off the final simplex tableau) and Lemma 6.5.2 (nearest point in a nonempty closed set, available in Mathlib as IsClosed.exists_infDist_eq_dist) are not separate targets. The Fourier–Motzkin elimination of §6.7 has no numbered result.
• Contributions welcome: proofs of any milestone, the two Farkas-lemma chains, and bridges to the general-form duality already on the platform.

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, Chapter 6. https://doi.org/10.1007/978-3-540-30717-4
• J. Farkas, Theorie der einfachen Ungleichungen, J. Reine Angew. Math. 124 (1902), 1–27. https://doi.org/10.1515/crll.1902.124.1
• D. Gale, H. W. Kuhn and A. W. Tucker, Linear programming and the theory of games, in Activity Analysis of Production and Allocation, Wiley, 1951, 317–329.
• M. Conforti, M. Di Summa and G. Zambelli, Minimally infeasible set-partitioning problems with balanced constraints, Mathematics of Operations Research (cited in the book as to appear; the source of the proof in §6.6).
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 4.

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.