Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.1308255793978239Formalized record≥ 2.15Open frontier

9 provers on it17 of 18 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.1308255793978239Formalized record≥ 2.15Open frontier

9 provers on it17 of 18 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Robust Mean-Covariance Solutions for Stochastic Optimization III: Concave Utilities with a Monotone Second Derivative Have a Closed-Form Robust ObjectiveResearch Paper

Motivation

A decision maker who chooses a portfolio $x\in\mathbb R^n$ of risky assets with random return vector $R$ receives the scalar return $x'R$ and evaluates it by an expected utility $E[u(x'R)]$ . In practice the law of $R$ is not known; what can be estimated with some confidence are its mean $\mu$ and covariance $\Sigma$ . The robust mean-covariance objective replaces the unknown law by the worst law consistent with these two moments:

U(x)=\inf\{E[u(x'R)] : R \text{ has mean } \mu \text{ and covariance } \Sigma\}.

Ioana Popescu (Operations Research 55(1), 2007) showed that $U(x)$ depends on $x$ only through $\mu_x=x'\mu$ and $\sigma_x^2=x'\Sigma x$ , and that for large classes of utilities it has a closed form or reduces to a one-dimensional search. This turns a robust stochastic program into a parametric mean-variance program, which is the practical point of the paper. This mission formalizes the closed form for concave utilities with a monotone second derivative (Proposition 7), a class that contains the exponential utility $1-e^{-ay}$ and all concave quadratics. The reduction to $(\mu_x,\sigma_x)$ is the subject of the companion mission Robust Mean-Covariance Solutions for Stochastic Optimization I; the two-point case is mission II.

The underlying univariate question is a moment problem in the tradition of Chebyshev-type bounds: the extremal value of $E[u(r)]$ over all laws with prescribed mean and variance. Scarf (1958) solved an instance for a piecewise-linear inventory cost, and Birge and Dulá (1991) treated two-point extremal laws on bounded domains.

Setting

Fix $m\in\mathbb R$ and $s\ge 0$ . The mean-variance class $\mathbb M_{(m,s^2)}$ is the set of Borel probability measures $\nu$ on $\mathbb R$ with $\int r^2\,d\nu<\infty$ , $\int r\,d\nu=m$ and $\int (r-m)^2\,d\nu=s^2$ (Lean: MeanVarClass m (s ^ 2)). For a utility $u:\mathbb R\to\mathbb R$ the robust objective is

U(m,s)=\inf\Big\{\int u\,d\nu : \nu\in\mathbb M_{(m,s^2)}\Big\},

with $\min$ read, as in the paper, "in the wide sense of $\inf$ ", so the value $-\infty$ is allowed. The paper's $U(x)$ is $U(\mu_x,\sigma_x)$ .

For $p\in(0,1)$ the two-point law $r_p$ puts mass $p$ on $b=m+\sqrt{(1-p)/p}\,s$ and mass $1-p$ on $a=m-\sqrt{p/(1-p)}\,s$ ; these are exactly the two-point laws of $\mathbb M_{(m,s^2)}$ . Its expected utility is the two-point objective (8),

U(p)=p\,u(b)+(1-p)\,u(a)\qquad(\texttt{twoPointValue u m s p}).

A supporting quadratic of $u$ is $q(y)=Ay^2+By+C$ with $q\le u$ on $\mathbb R$ ; the set of their coefficients is $\mathcal Q$ . Since every $r\sim(m,s^2)$ has $E[q(r)]=A(m^2+s^2)+Bm+C$ , each element of $\mathcal Q$ gives a lower bound on $U(m,s)$ (Proposition 3). The function $u$ has the one-point support property with respect to $(m,s^2)$ (Definition 3, OnePointSupportWrt u m s) if some supporting quadratic touches $u$ at $m$ and $E[u(r_p)]\to E[q(r_p)]$ as $p\to0^+$ or as $p\to1^-$ ; it has one-point support (OnePointSupport u) if this holds for every $m$ and every $s\ge0$ .

Formalization targets

Goal: Proposition 7

Let $u$ be concave and twice differentiable with monotone $u''$ .

(a) If $u'$ is convex, then

U(m,s)=u(m)+\lim_{y\to-\infty}u''(y)\,\frac{s^2}{2}\qquad\text{for all } m,\ s.

(b) If $u'$ is concave, the same holds with $\lim_{y\to+\infty}u''(y)$ .

In each part the limit $L$ of $u''$ exists in $[-\infty,0]$ . When $L$ is finite the goal asserts that $u$ is integrable under every law of every class, that $u(m)+Ls^2/2$ is the greatest lower bound of the expected utilities, and that $u$ has one-point support. When $L=-\infty$ and $s>0$ it asserts $U(m,s)=-\infty$ .

Milestones

Display (9): $\partial U/\partial p=u(b)-u(a)-(b-a)\,\frac{u'(b)+u'(a)}{2}$ .
For convex $u'$ and $s>0$ , $U(p)$ is nonincreasing on $(0,1)$ .
Appendix (4): $\lim_{p\to1^-}U(p)=u(m)+\frac{s^2}{2}\lim_{y\to-\infty}u''(y)$ , including the value $-\infty$ .
Proposition 3: every $E[u(r)]$ dominates every $A(m^2+s^2)+Bm+C$ with $(A,B,C)\in\mathcal Q$ .
The function $d(y)=\frac{u(y)-u(m)}{(y-m)^2}-\frac{u'(m)}{y-m}$ is nondecreasing on $\{y \neq m\}$ when $u'$ is convex.
Appendix (5): $q(y)=\tfrac12u''(-\infty)(y-m)^2+u'(m)(y-m)+u(m)$ supports $u$ , and $\inf_{y\ne m}d(y)=\lim_{y\to-\infty}d(y)=\tfrac12u''(-\infty)$ .

An additional item states Proposition 8: a monotone convex $u$ has one-point support and $U(m,s)=u(m)$ .

Significance

Proposition 7 turns the worst-case expected utility into a mean-variance criterion with an explicit risk weight: a prudent investor ( $u'$ convex) is penalized by $\tfrac12\lim_{y\to-\infty}u''(y)$ per unit of variance, an imprudent one by the limit at $+\infty$ . With Proposition 1, the robust portfolio problem becomes $\max_x\ u(\mu_x)+\tfrac12 L\,\sigma_x^2$ , a concave mean-variance program. For exponential utility the weight is $-\infty$ (Example 3 of the paper), so the robust investor must eliminate variance entirely; this is a qualitative statement about robustness that follows only from the $-\infty$ case of the theorem.

The result is published with a proof in the appendix of the paper. It has, to the best of our search, no machine-checked version, and the platform currently holds no statement of Propositions 3, 7 or 8 or Definition 3. A formal proof would also check two points where the printed argument is incomplete: the proof's step " $\lim_{y\to-\infty}u'(y)=\infty$ " fails for affine $u$ , where the theorem nevertheless holds, and the claim that $u$ "has one-point support" fails when $\lim u''=-\infty$ (see the scope section). Related platform work on worst-case expectations over ambiguity sets is the mission Wasserstein Distributionally Robust Optimization II, which uses a different ambiguity set.

Difficulty

The infimum ranges over all laws with two prescribed moments, an infinite-dimensional set with no compactness, and in the relevant cases it is not attained. The natural first idea, restricting to two-point laws and minimizing over $p$ , gives only an upper bound (display (7)), and here the minimizing $p$ runs off to the boundary: the extremal law puts vanishing mass on a point escaping to $-\infty$ . Identifying the limiting value requires controlling $u(m-sq)/(1+q^2)$ as $q\to\infty$ , a second-order asymptotic statement about $u$ at $-\infty$ . The matching lower bound requires a supporting quadratic whose curvature is exactly $\tfrac12\lim u''$ ; showing that it lies below $u$ everywhere, not only near $m$ , is a global statement that uses the convexity of $u'$ on the whole line. The finite-limit and infinite-limit cases also behave differently: in the second, no supporting quadratic exists at all.

Formalization scope

Laws are Measure ℝ with IsProbabilityMeasure, finite second moment is MemLp id 2, and the class is parameterized by mean $m$ and variance $s^2$ with $s\ge0$ . The statements are univariate: $U(x)$ of the paper is the univariate objective at $(\mu_x,\sigma_x)$ by Proposition 1 of the paper (mission I). Derivatives are deriv u and deriv (deriv u); "twice differentiable" is differentiability of $u$ and of $u'$ . Limits of $u''$ are explicit hypotheses (Tendsto … atBot (𝓝 L) or Tendsto … atBot atBot), never limUnder. Limits in $p$ are one-sided inside $(0,1)$ . Expectations under two-point laws are written by the explicit formula (8).

"Min" is never a real ⨅, which Lean evaluates to $0$ on sets unbounded below. The finite case uses IsGLB together with integrability of $u$ under every law of the class; the infinite case asserts that integrable laws with arbitrarily small expected utility exist; Proposition 3 is stated as "every value $\ge$ every value". Proposition 3 assumes $u$ integrable under the law; Proposition 8 takes the infimum over laws under which $u$ is integrable, which for convex $u$ loses nothing.

One correction to the printed statement: Proposition 7 opens with "then $u$ has one-point support", which is false when $\lim u''=-\infty$ , since no quadratic lies below $1-e^{-ay}$ on $\mathbb R$ . The formalization asserts one-point support only in the finite-limit case and the value $-\infty$ in the other. A formalization that took $\min$ as a real infimum, dropped the integrability conjunct, or asserted one-point support unconditionally would be either trivially satisfiable or false; none of these is used.

A complete development needs: moments of two-point laws, a second-order l'Hôpital or Taylor argument at $-\infty$ , the trapezoid inequality for convex functions, and Jensen-type integration of quadratic lower bounds. The mean-variance class, the two-point objective and the supporting-quadratic lemmas are reusable for mission II and for other moment-problem bounds. Proofs of any milestone, and of part (b), are welcome.

Selected references

I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
H. Scarf, A min-max solution of an inventory problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
J. R. Birge, J. H. Dulá, Bounding separable recourse functions with limited distribution information, Annals of Operations Research 30, 1991.
S. Karlin, W. J. Studden, Tchebycheff Systems: With Applications in Analysis and Statistics, Interscience, 1966.

11 thms4 active usersReviewed

Completed

Combinatorics Probability·Captain: mikedeng1

Limits of Permutation Sequences II: Convergence Is Equivalent to Being Cauchy in the Rectangular DistanceResearch Paper

Motivation

For dense graphs, convergence of subgraph densities was shown by Lovász and Szegedy (2006) to have graphons as limit objects, and Borgs, Chayes, Lovász, Sós and Vesztergombi (2008) proved that the same convergence is metric: a graph sequence converges exactly when it is Cauchy in the cut distance. The metric view is what makes the space of graphons compact and connects limit theory with regularity lemmas and property testing.

Hoppen, Kohayakawa, Moreira, Ráth and Sampaio (arXiv:1103.5844; J. Combin. Theory Ser. B, 2013) developed the corresponding theory for permutations. Besides the existence of limits (the subject of mission I of this series), they introduced a rectangular distance $d_\square$ between permutations, a normalized version of Cooper's discrepancy (Cooper, J. Combin. Theory Ser. A, 2004; reference [7] of the paper), and proved in Theorem 1.8 that convergence of a permutation sequence is the same as being Cauchy for $d_\square$ . This mission formalizes that theorem.

Timeline:

2004. Cooper introduces the discrepancy of a permutation as a measure of quasirandomness.
2006–2008. Lovász–Szegedy and Borgs et al. establish graph limits and the cut-distance characterization of convergence.
2011–2013. Hoppen et al. prove the permutation analogues, including Theorem 1.8 (this paper).

Setting

For $n \ge 1$ , $S_n$ is the set of permutations of $[n]=\{1,\dots,n\}$ , $|\pi| = n$ for $\pi\in S_n$ , and $\mathcal S=\bigcup_n S_n$ . For $\tau\in S_k$ and $\pi\in S_n$ , $\Lambda(\tau,\pi)$ counts the increasing $k$ -tuples $x_1<\dots<x_k$ in $[n]$ with $\pi(x_i)<\pi(x_j)\iff\tau(i)<\tau(j)$ , and the subpermutation density is $t(\tau,\pi)=\Lambda(\tau,\pi)/\binom nk$ for $k\le n$ and $0$ for $k>n$ . A permutation sequence $(\sigma_n)$ is convergent if $t(\tau,\sigma_n)$ converges for every fixed $\tau\in\mathcal S$ .

A limit permutation is a Lebesgue measurable $Z:[0,1]^2\to[0,1]$ such that $Z(x,\cdot)$ is a cdf (non-decreasing, right-continuous, $Z(x,1)=1$ ) for every $x$ and $\int_0^1 Z(x,y)\,dx=y$ for every $y$ ; the set of them is $\mathcal Z$ . Each $Z$ has an associated random point $(X,Y)$ with $X\sim U[0,1]$ and conditional cdf $Z(X,\cdot)$ , joint distribution function $F(x,y)=\int_0^x Z(t,y)\,dt$ , and pattern densities $t(\tau,Z)$ (the probability that $k$ independent copies of $(X,Y)$ form the pattern $\tau$ ).

For $\sigma\in S_n$ , the step limit permutation $Z_\sigma$ spreads the permutation matrix of $\sigma$ uniformly over the corresponding $n\times n$ grid cells. The rectangular distance of $Z_1,Z_2\in\mathcal Z$ is

d_\square(Z_1,Z_2)=\sup_{x_1<x_2,\ y_1<y_2}\left|\int_{x_1}^{x_2}\big(Z_1(x,y_2)-Z_1(x,y_1)\big)dx-\int_{x_1}^{x_2}\big(Z_2(x,y_2)-Z_2(x,y_1)\big)dx\right|,

the largest difference between the probabilities the two random points give to an axis-parallel rectangle, and $d_\infty(Z_1,Z_2)=\sup_{x,y}|F_1(x,y)-F_2(x,y)|$ . On permutations of possibly different lengths, $d_\square(\sigma,\pi):=d_\square(Z_\sigma,Z_\pi)$ . A sequence is Cauchy with respect to $d_\square$ if for every $\varepsilon>0$ there is $n_0$ with $d_\square(\sigma_n,\sigma_m)<\varepsilon$ for all $n,m\ge n_0$ .

Formalization targets

Goal: Theorem 1.8, under $|\sigma_n|\to\infty$

|\sigma_n|\to\infty\ \Longrightarrow\ \Big((\sigma_n)\ \text{convergent}\iff(\sigma_n)\ \text{is } d_\square\text{-Cauchy}\Big).

Milestones

In the order the proof uses them:

Lemma 3.5: $|t(\tau,\sigma)-t(\tau,Z_\sigma)|\le\frac1n\binom k2$ for $\tau\in S_k$ , $\sigma\in S_n$ , $k\le n$ .
Eq. (49): for $|\sigma_n|\to\infty$ , $\sigma_n\to Z\iff Z_{\sigma_n}\xrightarrow{t}Z$ .
Eq. (34): $d_\infty\le d_\square\le 4\,d_\infty$ on $\mathcal Z$ .
Lemma 2.1: for uniform marginals, weak convergence is equivalent to uniform convergence of joint distribution functions.
Lemma 2.2 (a): every law on $[0,1]^2$ with uniform marginals has a limit permutation as its conditional cdf.
Lemma 5.3: weak, $d_\square$ - and density convergence on $\mathcal Z$ coincide.
Theorem 1.6 (i): a convergent sequence with $|\sigma_n|\to\infty$ converges to some $Z\in\mathcal Z$ .
Claim 2.4: a convergent sequence with $|\sigma_n|\not\to\infty$ is eventually constant.
Theorem 1.8 ( $\Rightarrow$ ): every convergent sequence is $d_\square$ -Cauchy, with no condition on lengths.

Significance

Theorem 1.8 identifies density convergence, defined through infinitely many pattern counts, with a single metric condition. With Theorem 1.6 it shows that the completion of $(\mathcal S,d_\square)$ is $\mathcal Z$ modulo almost-everywhere equality, which is compact; permutations are isolated points of it (Claim 2.4). This is the permutation counterpart of the cut-distance theory of graph limits, and it is the metric in which the paper's testability and sampling results (Lemma 4.2) are quantitative.

The theorem is proved in the paper. To the best of current knowledge neither it nor the underlying permuton theory is formalized in any proof assistant. The mission produces machine-checked statements of the rectangular distance, its comparison with the sup-norm distance of distribution functions, and the Cauchy characterization, all reusable for quasirandom permutations and permutation property testing.

Difficulty

The direction "convergent $\Rightarrow$ Cauchy" needs a limit permutation for the sequence and the equivalence of density and $d_\square$ convergence on $\mathcal Z$ (Lemma 5.3), which is not formal: density convergence involves every pattern, $d_\square$ a supremum over rectangles. For "Cauchy $\Rightarrow$ convergent", completeness of bounded functions under the sup norm gives a uniform limit $F$ of the distribution functions, but a uniform limit of distribution functions of limit permutations is not visibly the distribution function of a limit permutation. Identifying it needs weak compactness, Lemma 2.1 and the regular conditional cdf of Lemma 2.2.

The literal statement also fails for sequences whose lengths do not tend to infinity, as explained under Formalization scope; the reduction "we may assume $|\sigma_n|\to\infty$ " covers only one direction.

Formalization scope

$[0,1]$ is Mathlib's unitInterval with Lebesgue measure; a limit permutation is a curried real function Z : I → I → ℝ, almost-everywhere measurable on the square, with the cdf and integral conditions for every $x$ and every $y$ . $S_n$ is Equiv.Perm (Fin n) (0-based) and a permutation sequence is ℕ → Σ n, Equiv.Perm (Fin n).
$d_\square$ on $\mathcal Z$ is the integral form of the paper's Eq. (32); $d_\infty$ is Eq. (33) with $F_i(x,y)=\int_0^x Z_i(t,y)\,dt$ . Both are real suprema of bounded families. $Z_\sigma$ is in closed form, with the first row used at $x=0$ (a null-set choice).
$d_\square$ on permutations is defined for every pair of lengths as $d_\square(Z_\sigma,Z_\pi)$ , the paper's extension (Sect. 4.1); the same-length formula (31) is not needed. A definition that returned $0$ or junk for different lengths would make every sequence with growing lengths Cauchy and is ruled out.
Correction. The paper states Theorem 1.8 for all sequences. Without $|\sigma_n|\to\infty$ , "Cauchy $\Rightarrow$ convergent" is false: interleaving $\sigma=(1,2)$ with permutations $\tau_k$ , $|\tau_k|\to\infty$ , $d_\square(Z_{\tau_k},Z_\sigma)\to0$ , gives a Cauchy sequence along which $t(\sigma,\cdot)$ alternates between $1$ and values tending to $3/4$ . The goal carries $|\sigma_n|\to\infty$ ; the true direction without it is milestone 9.
"Convergent" is the paper's Definition 1.2 (all densities converge), not the existence of a limit $Z$ . The Cauchy condition uses the explicit $\varepsilon$ – $n_0$ form with strict inequality, not a metric-space instance.
Theorem 1.6 (i) is also the goal of mission I; it is restated here in this mission's namespace.

Needed infrastructure: Prokhorov compactness of probability measures on the square, the Portmanteau theorem, completeness of bounded functions under the sup norm, and conditional cdfs (ProbabilityTheory.condCDF). Contributions on any milestone, and alternative proofs of the Cauchy characterization, are welcome.

Selected references

C. Hoppen, Y. Kohayakawa, C. G. Moreira, B. Ráth, R. M. Sampaio, Limits of permutation sequences, arXiv:1103.5844v2, 2012; J. Combin. Theory Ser. B 103 (2013). https://arxiv.org/abs/1103.5844v2
J. N. Cooper, Quasirandom permutations, J. Combin. Theory Ser. A 106 (2004) no. 1, 123–143 (cited as [7] in arXiv:1103.5844v2).
L. Lovász, B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96 (2006) 933–957. https://doi.org/10.1016/j.jctb.2006.05.002
C. Borgs, J. T. Chayes, L. Lovász, V. T. Sós, K. Vesztergombi, Convergent sequences of dense graphs I: Subgraph frequencies, metric properties and testing, Adv. Math. 219 (2008) 1801–1851. https://doi.org/10.1016/j.aim.2007.08.004
P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962

21 thms4 active usersReviewed

Completed

Convex Optimization Graph Theory Linear algebra+2·Captain: mikedeng1

Lifts of Convex Sets and Cone Factorizations III: Stable Set Polytopes Have No Small Semidefinite LiftsResearch Paper

Motivation

Many polytopes of combinatorial optimization have exponentially many facets, yet linear optimization over them is tractable because they are projections of simpler convex sets: affine slices of a nonnegative orthant (linear programming) or of the cone of positive semidefinite matrices (semidefinite programming). The size of such a representation, the number of variables of the extended formulation, is the natural measure of how compactly a polytope can be optimized over. Yannakakis (Expressing combinatorial optimization problems by linear programs, JCSS 1991) characterized polyhedral representations through nonnegative factorizations of the slack matrix. Gouveia, Parrilo and Thomas (arXiv:1111.3164, Mathematics of Operations Research 2013) extended the characterization to lifts into arbitrary closed convex cones, in particular to cones of positive semidefinite matrices.

The stable set polytope of a graph is the standard test case. For a perfect graph on $n$ vertices it is a linear image of an affine slice of the cone of $(n+1)\times(n+1)$ positive semidefinite matrices (Lovász's theta body construction, stated in the paper as Theorem 5.1 with a citation to Lovász & Schrijver, SIAM J. Optim. 1991); this is the reason the maximum weight stable set problem is solvable in polynomial time on perfect graphs. The question addressed by this mission is whether a smaller matrix size could suffice. Theorem 5.2 of Gouveia–Parrilo–Thomas answers it: for every graph on $n$ vertices, matrices of size $n$ do not suffice.

Setting

Let $G$ be a graph with vertex set $V = \{1,\dots,n\}$ . A set $S \subseteq V$ is stable if no edge joins two of its elements, and its incidence vector $\chi_S \in \{0,1\}^n$ has $(\chi_S)_i = 1$ exactly when $i \in S$ . The stable set polytope is

\mathrm{STAB}(G) = \mathrm{conv}\{\chi_S : S \text{ stable}\} \subseteq \mathbb R^n .

Let $\mathcal S^k_+$ be the cone of $k \times k$ real symmetric positive semidefinite matrices, with the trace inner product $\langle A, B\rangle = \mathrm{tr}(AB)$ , under which it is self-dual. For a closed convex cone $K$ , a set $C$ has a $K$ -lift if $C = \pi(K \cap L)$ for an affine subspace $L$ and a linear map $\pi$ ; the lift is proper if $L$ meets the interior of $K$ .

For a polytope $P$ with vertices $p_1,\dots,p_v$ and facet inequalities $h_1(x) \ge 0, \dots, h_f(x) \ge 0$ , the slack matrix is the nonnegative $v\times f$ matrix $(h_j(p_i))$ . A $K$ -factorization of a nonnegative matrix $M$ assigns $a^i \in K$ to each row and $b^j \in K^*$ to each column with $\langle a^i, b^j\rangle = M_{ij}$ . In Lean the objects are stab, HasPSDLift, HasConeLift, HasProperConeLift, IsSlackMatrix, HasConeFactorization and HasPSDFactorization in the namespace ConeLifts.StableSet.

Formalization targets

Goal: Theorem 5.2

For every $n \ge 1$ and every graph $G$ on $n$ vertices,

\neg\ \exists\, L,\ \pi:\quad \mathrm{STAB}(G) = \pi(\mathcal S^n_+ \cap L).

The statement excludes all lifts, proper or not, and holds for every graph, perfect or not.

Milestones

Theorem 3.3 (first sentence). If a full-dimensional polytope $P$ with the origin in its interior has a proper $K$ -lift, then every slack matrix of $P$ admits a $K$ -factorization.
Rows of the submatrix. The origin and $e_1,\dots,e_n$ are vertices of $\mathrm{STAB}(G)$ .
Columns of the submatrix. For $n \ge 1$ , each $\{x \in \mathrm{STAB}(G) : x_i = 0\}$ is a facet, and some facet does not contain the origin.
The core lemma. For every $s \in \mathbb R^n$ the block matrix

S' = \begin{pmatrix} 1 & 0_n \\ s & I_n\end{pmatrix}

has no $\mathcal S^n_+$ -factorization.

Significance

Theorem 5.2 shows that the semidefinite representation of $\mathrm{STAB}(G)$ for perfect graphs has the smallest possible matrix size: $n+1$ cannot be lowered to $n$ . As Remark 5.3 of the paper notes, the same argument shows that no polytope in $\mathbb R^n$ with a vertex at which it locally looks like the nonnegative orthant has an $\mathcal S^n_+$ -lift. It is also an instance of the factorization method: a statement about all possible semidefinite representations is reduced to a finite obstruction on a small submatrix of the slack matrix.

The theorem is proved in the paper. To the best of our knowledge no machine-checked proof of it, of the factorization theorem for cone lifts, or of any positive semidefinite lower bound for a polytope exists in Mathlib or on this platform. A formalization produces reusable statements about positive semidefinite factorizations, slack matrices and lifts, and a verified instance of the general lower-bound technique.

Difficulty

The step from lifts to factorizations is where the direct argument fails. Theorem 3.3 applies only to proper lifts and only to polytopes with the origin in their interior, while the goal concerns all lifts of a polytope that has the origin as a vertex. Applying Theorem 3.3 to $\mathrm{STAB}(G)$ and an arbitrary lift therefore does not match its hypotheses, and the printed proof does not spell out how the two gaps are closed (see Formalization scope). Theorem 3.3 itself is a consequence of the general factorization theorem of the paper (Theorem 2.4), whose proof rests on conic duality. The core lemma about $S'$ is a statement about every family of $2(n+1)$ positive semidefinite matrices, so it cannot be settled by any finite search.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); vertex $i+1$ of the paper is i : Fin n; graphs are SimpleGraph (Fin n) and stability is SimpleGraph.IsIndepSet. Vertices of a polytope are Set.extremePoints ℝ. $\mathcal S^k_+$ is the set of real $k\times k$ matrices satisfying Matrix.PosSemidef (which includes symmetry), and the ambient space of a positive semidefinite lift is all $k \times k$ matrices; this does not change which sets have lifts, because a lift in the symmetric matrices extends linearly and a lift in all matrices restricts to them. Positive semidefinite factorizations require both factor families to be positive semidefinite and use $\mathrm{tr}(A_iB_j)$ .

Reading decisions: the goal assumes $n \ge 1$ , the paper's meaning of "a graph with $n$ vertices", since for $n = 0$ the polytope $\{0\}$ is the image of $\mathcal S^0_+$ and the printed statement fails. Milestone 3 also assumes $n \ge 1$ , and so does Milestone 1 (Theorem 3.3): in $\mathbb R^0$ the point $\{0\}$ has a proper lift to the whole space $\mathbb R^m$ , whose dual cone $\{0\}$ cannot factor the slack matrix $(1)$ . In Milestone 4 the column $*_n$ is an arbitrary real vector. The slack matrices of Theorem 3.3 are encoded through the identification on p. 9 of the paper: rows are vertices of $P$ , columns are extreme points $y$ of the polar $P^\circ = \{y : \langle x, y \rangle \le 1\ \forall x \in P\}$ , the canonical entry is $1 - \langle p, y\rangle$ , and every slack matrix is the canonical one with positively scaled columns. Facets in Milestone 3 are nonempty proper exposed faces of dimension one less than the polytope.

The goal must not be weakened to proper lifts, and lifts must use equality $\mathrm{STAB}(G) = \pi(\mathcal S^n_+ \cap L)$ with $\pi$ linear and $L$ affine; with inclusion, or with arbitrary maps, the statement becomes trivial or false. The core lemma is meaningful only with both factor families positive semidefinite; without that requirement $S'$ factors trivially.

Beyond the milestones, a complete proof of the goal needs two facts the paper uses without stating them as claims of this proof: (a) an $\mathcal S^n_+$ -lift that is not proper is a proper lift to a face of $\mathcal S^n_+$ (p. 5), every face of $\mathcal S^n_+$ is isomorphic to some $\mathcal S^r_+$ with $r \le n$ (Example 4.2, p. 12), and an $\mathcal S^r_+$ -factorization yields an $\mathcal S^n_+$ -factorization; (b) lifts are preserved by affine maps (Proposition 2.9, pp. 6–7), and translating a polytope changes its slack matrices only by positive column scalings, which is how Theorem 3.3 applies to $\mathrm{STAB}(G)$ , whose origin is a vertex rather than an interior point. Stating (a) and (b) as separate lemmas is welcome.

Needed infrastructure: positive semidefinite matrices and the trace pairing, the face structure of $\mathcal S^n_+$ , invariance of lifts under affine maps, and conic duality for Theorem 3.3. All of these are reusable beyond this mission. Contributions welcome: proofs of the milestones, the bridging facts (a) and (b), and alternative routes to the goal.

Selected references

J. Gouveia, P. A. Parrilo, R. R. Thomas, Lifts of Convex Sets and Cone Factorizations, Mathematics of Operations Research 38(2):248–264, 2013. arXiv:1111.3164v2. https://arxiv.org/abs/1111.3164
M. Yannakakis, Expressing combinatorial optimization problems by linear programs, Journal of Computer and System Sciences 43(3):441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
L. Lovász, A. Schrijver, Cones of matrices and set-functions and 0-1 optimization, SIAM Journal on Optimization 1(2):166–190, 1991. https://doi.org/10.1137/0801013

14 thms4 active usersReviewed

Completed

Combinatorics Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis I: Valuated MatroidsTextbook

Motivation

Matroids abstract the combinatorial content of linear independence: which sets of columns of a matrix are independent, which are maximal (bases), and how bases relate to each other. This abstraction, isolated independently by Whitney (1935) and van der Waerden's school, turned out to be exactly the right level of generality for a large family of greedy and augmenting-path algorithms — a base of a matroid can always be reached from another by a sequence of single-element swaps, and this exchange property is what makes local search on bases correct and efficient.

A natural question, raised in the 1980s once matroid-based combinatorial optimization was mature, is what happens when bases are not merely present or absent but carry real-valued weights that must interact well with the exchange structure. Dress and Wenzel answered this with the notion of a valuated matroid: a real-valued function on the bases of a matroid satisfying a weighted strengthening of the exchange axiom. Their motivation was explicitly algorithmic — valuated matroids are exactly the structures for which a greedy algorithm computes an optimal basis under linear objectives, and more generally under the family of "tilted" objectives obtained by adding an arbitrary linear functional. Independently, valuated matroids arise from the classical Grassmann–Plücker relation applied to matrices over a field with a valuation (hence the name), connecting them to tropical geometry.

This mission formalizes the two theorems of Murota's Discrete Convex Analysis (2003, §2.4) that make this story precise: the classical correspondence between a matroid's base family and its rank function (Theorem 2.29), and the characterization of valuations by a perturbation-robustness property (Theorem 2.32). Theorem 2.32 is also historically the entry point of the book's central theme — it is the special case, for the two-valued lattice $\{0,1\}^V$ , of the general local-exchange criterion for M-convex functions that occupies chapters 6 and 7.

Setting

Let $V$ be a finite set (the ground set). A matroid on $V$ is a pair $(V, \mathcal B)$ where $\mathcal B$ , the base family, is a nonempty family of subsets of $V$ satisfying the simultaneous exchange axiom (B): for every $J, J' \in \mathcal B$ and every $i \in J \setminus J'$ , there exists $j \in J' \setminus J$ such that both

J - i + j := (J \setminus \{i\}) \cup \{j\} \in \mathcal B \quad\text{and}\quad J' + i - j := (J' \setminus \{j\}) \cup \{i\} \in \mathcal B.

Equivalently (Theorem 2.29 below), a matroid can be described by its rank function $\rho : 2^V \to \mathbb Z$ , a set function satisfying:

(R1) $0 \le \rho(X) \le |X|$ for every $X \subseteq V$ ;
(R2) monotonicity: $X \subseteq Y \implies \rho(X) \le \rho(Y)$ ;
(R3) submodularity: $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$ .

A valuation of a base family $\mathcal B$ is a function $\omega : \mathcal B \to \mathbb R$ satisfying the axiom (VM): for every $J, J' \in \mathcal B$ and $i \in J \setminus J'$ , there is $j \in J' \setminus J$ with $J - i + j, J' + i - j \in \mathcal B$ and

\omega(J) + \omega(J') \le \omega(J - i + j) + \omega(J' + i - j).

The pair $(V, \omega)$ is then a valuated matroid. For $p : V \to \mathbb R$ , the perturbation of $\omega$ by $p$ is

\omega[-p](J) = \omega(J) - \sum_{j \in J} p(j).

Formalization targets

Goal: Theorem 2.32 (the valuated matroid characterization)

\omega \text{ is a valuation of } \mathcal B \iff \forall\, p : V \to \mathbb R,\ \{J \in \mathcal B : \omega[-p](J') \le \omega[-p](J)\ \forall J' \in \mathcal B\} \text{ is a nonempty family satisfying (B)}.

The right-hand side says: for every linear perturbation $p$ , the set of $\omega[-p]$ -maximal bases is again the base family of a matroid. The universal quantifier over $p$ is not optional — a version of this statement quantified over a single fixed $p$ is either vacuous or false, and does not capture what makes valuated matroids useful.

Milestone: Theorem 2.29 (the base-family / rank-function correspondence)

The maps

\rho(X) = \max\{|X \cap J| : J \in \mathcal B\}, \qquad \mathcal B = \{J \subseteq V : \rho(J) = |J| = \rho(V)\}

are mutually inverse bijections between nonempty families satisfying (B) and set functions satisfying (R1)-(R3). This is weaker groundwork than the goal, stated first because it fixes the exact axiomatic vocabulary — (B) and (R) — that Theorem 2.32 is built on.

Significance

The result itself. Theorem 2.32 is the reason valuated matroids are the right object for weighted combinatorial optimization on matroids: it says a function on bases behaves correctly under every linear re-weighting of the ground set exactly when it satisfies the local exchange inequality (VM). This is what guarantees, for instance, that a greedy algorithm which is correct for the unweighted matroid extends correctly to families of tilted objectives, and it is the germ of the general local-optimality criterion for M-convex functions (chapters 6–7), which underlies most of the algorithmic content of the rest of the book. Theorem 2.29 is the classical result — due jointly to the development of matroid theory from the 1930s onward — that the base-exchange and rank-submodularity axiomatizations of a matroid carry the same information; it is the finite, unweighted precursor of Theorem 2.32.

Formalizing it. Neither theorem has a machine-checked proof on the platform prior to this mission (see Formalization scope for the prior-art check). Theorem 2.29's own proof is elementary but has two independent halves (each map preserves its target axiom class, and the two maps compose to the identity in both directions) that must all be established; Theorem 2.32's proof, as given in the source, defers entirely to a later, more general chapter-6 theorem, so a solver working only from this mission must either reconstruct a direct combinatorial argument for this special case or await chunk 06 (DiscreteConvex.MConvexFunctions, a separate mission) and specialize its main theorem.

Difficulty

The obvious approach to Theorem 2.32 — fix an optimal basis $J$ for $\omega[-p]$ and try to show the exchange condition on maximizers directly from (VM) — proves one direction (VM implies the maximizer property) in a few lines, since perturbing does not change which exchange moves are available. The converse is the substantial direction: from "the maximizer set is always a matroid, for every $p$ ," one must recover the single global inequality (VM) that must hold for all pairs $J, J' \in \mathcal B$ , not just optimal ones. The standard argument constructs, for a given non-optimal pair, a perturbation $p$ under which that specific pair becomes simultaneously optimal, and this construction is exactly the step the book skips by citing chapter 6's general theorem. A formalization attempting to bypass this by only checking the maximizer property for a finite or generic sample of perturbations would trivialize the statement to something false or vacuous — a pitfall the goal's explicit ∀ p is designed to prevent.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $2^V$ is represented as Finset (Finset V), and $V \to \mathbb R$ as a plain function type. The rank function is $\mathbb Z$ -valued (matching the book's own convention for matroid rank, as opposed to the $\mathbb R$ -valued conventions used from chapter 6 onward for general M-convex functions); RankOfFamily is implemented with Finset.sup over $\mathbb N$ rather than a partial max', so that it is a total function — its junk value at the empty family is never invoked, since every hypothesis in this mission supplies nonemptiness explicitly, matching the book's own phrasing.

A trivializing formalization of the goal is one that quantifies over a single fixed $p$ , or allows $\mathcal B$ to be empty; both are explicitly excluded by keeping $\mathcal B.\text{Nonempty}$ a hypothesis and $p$ universally quantified inside the theorem statement itself.

Checked against Mathlib (commit 0df444a360eaa60ab8c11dca51a86af692955474): Mathlib's Matroid structure is axiomatized via the single-element (asymmetric) exchange property, classically but not definitionally equivalent to Murota's simultaneous axiom (B) used throughout this book, and Mathlib provides no constructor recovering a base family or a Matroid from a bare rank function satisfying (R1)-(R3). Theorem 2.29 is therefore genuine, reusable infrastructure, not a restatement of existing Mathlib API. No reference item was found on the platform for either theorem (GET /theorems?q=matroid, q=valuated matroid return only unrelated tropical-geometry and k-server results). Contributions to a shared DiscreteConvex.Combinatorial definitions layer (the exchange and rank axioms) are welcome from later chunks of this series that build on matroid or base-polyhedron structure.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
H. Whitney, "On the abstract properties of linear dependence," American Journal of Mathematics, 57(3), 1935, pp. 509–533.
A. W. M. Dress, W. Wenzel, "Valuated matroids," Advances in Mathematics, 93(2), 1992, pp. 214–250.
R. A. Brualdi, "Comments on bases in dependence structures," Bulletin of the Australian Mathematical Society, 1(2), 1969, pp. 161–167.

13 thms4 active usersReviewed

Completed

Machine Learning Operations Research Optimization+2·Captain: mikedeng1

A Distributional Interpretation of Robust Optimization II: Box-Robust Sample Average Optimization Is ConsistentResearch Paper

Why robustify a sampled stochastic program

Many decision problems under uncertainty take the form of a stochastic program: choose a decision $v$ from a feasible set $\mathcal F$ to maximise the expected utility $\mathbb E_{x\sim\mu}[f(v,x)]$ , where the distribution $\mu$ of the uncertain parameter $x\in\mathbb R^m$ is known only through i.i.d. samples $x_1,\dots,x_n$ . The standard remedy, sample average approximation, maximises $\frac1n\sum_i f(v,x_i)$ instead. Its consistency (convergence of the optimal expected utility of its solutions to the true optimum) is classical, but it needs regularity assumptions of its own, for example those of King and Wets (Stochastics and Stochastic Reports, 1991), cited on p. 98 of the paper; the paper presents its construction as a route to consistency under weaker conditions.

Robust optimization (RO) takes a different route: it protects each sample by an uncertainty set and optimises against the worst point in it. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that RO over several overlapping uncertainty sets is equivalent to a distributionally robust stochastic program (their Theorem 2.1, the subject of mission I of this series). Section 3 of the paper uses that equivalence to show that a specific robustification of the sampled problem, with $\ell_\infty$ boxes of shrinking radius around each sample, is consistent under only boundedness and equicontinuity of $f$ . This mission formalizes that result, Theorem 3.1.

Setting

Equip $\mathbb R^m$ with the sup norm $\|z\|_\infty=\max_k|z_k|$ , its Borel $\sigma$ -algebra and Lebesgue measure $dx$ . The data are:

a set of decisions $V$ and a nonempty feasible set $\mathcal F\subseteq V$ ;
a utility $f:V\times\mathbb R^m\to\mathbb R$ , Borel measurable in $x$ for each $v$ ;
a true density $h^*$ on $\mathbb R^m$ (nonnegative, $\int h^*\,dx=1$ ) and i.i.d. samples $x_1,x_2,\dots$ with distribution $h^*(x)\,dx$ ;
radii $\epsilon(n)>0$ .

For a sample $x_1,\dots,x_n$ the boxes are $\mathcal Z_i=\{x_i+\delta\mid\|\delta\|_\infty\le\epsilon(n)\}$ , and the box-robust sample objective is

J_n(v)=\frac1n\sum_{i=1}^n\ \inf_{\|\delta_i\|_\infty\le\epsilon(n)}f(v,x_i+\delta_i)=\sum_{i=1}^n\frac1n\inf_{x_i'\in\mathcal Z_i}f(v,x_i').

The RO solution $v(n)$ is a maximiser of $J_n$ over $\mathcal F$ . The equicontinuity modulus of $f$ is

d(\epsilon)=\sup_{v,\,x,\ \|\delta\|_\infty\le\epsilon}|f(v,x)-f(v,x+\delta)|.

The proof works with the distribution set $\mathcal P_n$ of probability measures $\mu$ with $\mu(\bigcup_{i\in S}\mathcal Z_i)\ge|S|/n$ for every $S\subseteq\{1,\dots,n\}$ , and with the uniform box kernel density estimator

h_n(x)=(n\epsilon(n)^m)^{-1}\sum_{i=1}^nK\Big(\frac{x-x_i}{\epsilon(n)}\Big),\qquad K(z)=\frac{\mathbf 1(\|z\|_\infty\le1)}{2^m}.

Formalization targets

Goal: Theorem 3.1 (p. 98)

Assume $|f(v,x)|\le C$ for all $v,x$ ; $d(\epsilon)\to0$ as $\epsilon\downarrow0$ ; $\epsilon(n)\downarrow0$ and $n\epsilon(n)^m\uparrow\infty$ . Then for every choice of maximisers $v(n)$ , with probability one,

\lim_{n\to\infty}\int_{\mathbb R^m}f(v(n),x)\,h^*(x)\,dx=\sup_{v\in\mathcal F}\int_{\mathbb R^m}f(v,x)\,h^*(x)\,dx .

Milestones (proof of Theorem 3.1, p. 99)

$h_n$ is the density of a probability measure in $\mathcal P_n$ .
$J_n(v)\le\int f(v,x)\,h_n(x)\,dx$ for every $v$ .
Oscillation over a box: $\sup_{\mathcal Z_i}f(v,\cdot)-\inf_{\mathcal Z_i}f(v,\cdot)\le d(2\epsilon(n))$ .
Eq. (7): with $M_n=C\int|h_n-h^*|\,dx$ , for every $v$ ,

J_n(v)-M_n\le\int f(v,x)h^*(x)\,dx\le J_n(v)+M_n+d(2\epsilon(n)).

Strong $L^1$ consistency of the box kernel density estimator: if $\epsilon(n)\to0$ and $n\epsilon(n)^m\to\infty$ , then $\int|h_n-h^*|\,dx\to0$ almost surely.

Milestones 1–4 are deterministic statements about a fixed sample; milestone 5 is the only probabilistic input.

Significance

Theorem 3.1 gives consistency of a tractable robust reformulation of a sampled stochastic program under conditions the paper notes are weaker than those of King and Wets for sampled stochastic programs: $f$ need only be bounded and equicontinuous in $x$ , uniformly in $v$ , and the true distribution need only have a density. It also gives an explicit schedule for the size of the uncertainty set, $\epsilon(n)\to0$ with $n\epsilon(n)^m\to\infty$ , the bandwidth condition of kernel density estimation. Section 4 of the paper applies the same distributional interpretation to regularised learning methods such as the support vector machine and the Lasso.

The result is proved in the paper, with the $L^1$ consistency of kernel density estimators (Devroye 1983; Devroye and Györfi 1985) cited rather than proved. No part of it is formalized in Lean or on this platform as far as a search of the platform found. A complete development would produce, besides Theorem 3.1, a machine-checked strong $L^1$ consistency theorem for kernel density estimators, which is a basic result of nonparametric statistics in its own right.

Difficulty

The deterministic part (milestones 1–4) is measure-theoretic bookkeeping: the kernel integrates to one only because the box is a sup-norm ball of volume $(2\epsilon)^m$ , and every infimum and supremum must be handled with care, since $f$ need not attain them.

The obstacle is milestone 5. Almost-sure $L^1$ convergence of $h_n$ to an arbitrary density $h^*$ , with no continuity or support assumption, does not follow from the strong law of large numbers applied pointwise: $h_n(x)$ is an average of $n$ terms whose law changes with $n$ through $\epsilon(n)$ , and almost-sure convergence at each fixed $x$ does not give convergence of the integral along a single sample path. The theorem needs both a bias estimate valid for every integrable density and a concentration estimate for the random $L^1$ error. Mathlib has Lebesgue differentiation and the strong law, but no kernel density estimator and no such concentration result.

Formalization scope

$\mathbb R^m$ is Fin m → ℝ, whose Mathlib norm is the sup norm; boxes are Metric.closedBall. The integrals $\int f(v,x)h^*(x)\,dx$ are Bochner integrals against Lebesgue measure of integrable integrands.
The samples are a sequence X : ℕ → Ω → Fin m → ℝ on a probability space, independent (iIndepFun) and each with law volume.withDensity h*; $x_1,x_2,\dots$ become X 0, X 1, …, and the $n$ -th problem uses the first $n$ . "With probability one" is ∀ᵐ ω ∂P.
The goal quantifies over every selection $v(n)$ of maximisers, with no measurability assumed; a version with one chosen maximiser would be weaker and is ruled out.
Readings and corrections of the printed text:
- the kernel argument printed $(x-x_i)/\epsilon$ on p. 98 is read as $(x-x_i)/\epsilon(n)$ , as the proof on p. 99 writes it;
- " $\max_{v,x}|f(v,x)|\le C$ " is read as the uniform bound $|f|\le C$ and the "max" in $d(\epsilon)$ as a supremum;
- " $d(\epsilon)\downarrow0$ " is read as $d(\epsilon)\to0$ as $\epsilon\downarrow0$ ;
- implicit hypotheses made explicit: $\mathcal F\ne\emptyset$ , $\epsilon(n)>0$ , measurability of $f(v,\cdot)$ , $h^*$ a Lebesgue density;
- the monotonicity in " $\epsilon(n)\downarrow0$ , $n\epsilon(n)^m\uparrow\infty$ " is kept in the goal; milestone 5 uses the limits only, as the paper states it;
- the paper's $M_n$ ("there exists $\{M_n\}\to0$ ") is made explicit as $M_n=C\int|h_n-h^*|$ , so Eq. (7) is stated for every sample.
Remark 3.2 and Appendix B (an integrable envelope in place of boundedness) are not part of this mission.
Every real infimum and supremum ranges over a nonempty set of values bounded by $C$ in absolute value, so no statement holds through a junk value; a formalization in which the supremum over $\mathcal F$ or the box infimum could be vacuous is excluded.
The definitions (boxes, $\mathcal P_n$ , the kernel, the estimator, $J_n$ , $d$ ) live in one definition file. $\mathcal P_n$ duplicates, with weights $1/n$ , the distribution set of mission I; the duplication is deliberate because draft missions cannot import each other.
Welcome contributions: the kernel density estimator and its strong $L^1$ consistency as reusable infrastructure, and any of the deterministic milestones.

Selected references

H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
L. Devroye, The equivalence of weak, strong and complete convergence in $L_1$ for kernel density estimates, Annals of Statistics 11(3):896–904, 1983.
L. Devroye, L. Györfi, Nonparametric Density Estimation: The $L_1$ View, Wiley, 1985.
A. J. King, R. J.-B. Wets, Epi-consistency of convex stochastic programs, Stochastics and Stochastic Reports 34(1), 1991 (reference [22] of the paper).

7 thms4 active usersReviewed

Completed

Linear Optimization Operations Research Optimization+1·Captain: mikedeng1

Robust solutions of Linear Programming problems contaminated with uncertain data: A Violation-Probability Bound for the Robust CounterpartResearch Paper

Motivation

Linear programs solved in practice carry data that are measured, estimated or rounded. Ben-Tal and Nemirovski (Math. Program. 88, 2000) examined the NETLIB collection of real-world LPs and found that in 13 of them a relative perturbation of only 0.01% in the "ugly" coefficients of the inequality constraints can make the nominal optimal solution more than 50% infeasible (§2.3). Their remedy is the robust counterpart methodology: replace the nominal problem by a deterministic problem whose feasible solutions remain nearly feasible for every, or for all but a small probability of, data realizations.

The paper made the approach concrete for entry-wise uncertainty and gave the probabilistic guarantee that became a standard tool of robust and chance-constrained optimization. The main steps of the history are:

1973, A. L. Soyster: the interval (worst-case, "box") counterpart, here called (IRC).
1998–1999, Ben-Tal and Nemirovski (Math. Oper. Res. 23; Oper. Res. Lett. 25), and independently El Ghaoui and co-authors: robust optimization with ellipsoidal uncertainty sets.
2000, this paper: the ellipsoid-plus-box counterpart (RC[ε, δ, Ω]) and Proposition 1, which bounds each constraint's violation probability by $\exp\{-\Omega^2/2\}$ under independent symmetric perturbations.
2004, Bertsimas and Sim (Oper. Res. 52): the budgeted counterpart, with an analogous probability bound.

Setting

An uncertain linear program is

\text{minimize } c^Tx\quad\text{s.t.}\quad Ex=e,\qquad Ax\le b,\qquad \ell\le x\le u,\tag{LP}

with $x\in\mathbb{R}^n$ , $E\in\mathbb{R}^{p\times n}$ , $A=(a_{ij})\in\mathbb{R}^{m\times n}$ , and bounds $\ell_j\in\mathbb{R}\cup\{-\infty\}$ , $u_j\in\mathbb{R}\cup\{+\infty\}$ . For each inequality row $i$ a set $J_i\subseteq\{1,\dots,n\}$ lists the uncertain entries $a_{ij}$ , $j\in J_i$ . Only these entries are uncertain; $E,e,b,\ell,u,c$ are exact.

Given an uncertainty level $\epsilon>0$ and a feasibility tolerance $\delta>0$ , write $b_i^+=b_i+\delta\max[1,|b_i|]$ .

$x$ is reliable if it is feasible for (LP) and $\sum_{j\notin J_i}a_{ij}x_j+\sum_{j\in J_i}\tilde a_{ij}x_j\le b_i^+$ for every $i$ and every choice of $\tilde a_{ij}$ with $|\tilde a_{ij}-a_{ij}|\le\epsilon|a_{ij}|$ .
In the random symmetric uncertainty model, the true coefficients are $\tilde a_{ij}=(1+\epsilon\xi_{ij})a_{ij}$ , where $\xi_{ij}=0$ for $j\notin J_i$ and, for each row $i$ , $\{\xi_{ij}\}_{j\in J_i}$ are independent random variables, each symmetrically distributed in $[-1,1]$ .
$x$ is almost reliable with level $\kappa$ if it is feasible for (LP) and $\Pr\{\sum_j\tilde a_{ij}x_j>b_i^+\}\le\kappa$ for every $i$ .

The robust counterpart (RC[ε, δ, Ω]), with a safety parameter $\Omega>0$ , has variables $x_j$ , $y_{ij}$ , $z_{ij}$ and constraints $Ex=e$ , $Ax\le b$ , $\ell\le x\le u$ , $-y_{ij}\le x_j-z_{ij}\le y_{ij}$ for all $i,j$ , and

\sum_j a_{ij}x_j+\epsilon\Big[\sum_{j\in J_i}|a_{ij}|y_{ij}+\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}\Big]\le b_i^+\qquad\forall i.

The interval robust counterpart (IRC[ε, δ]) has variables $x_j,y_j$ and the constraint $\sum_ja_{ij}x_j+\epsilon\sum_{j\in J_i}|a_{ij}|y_j\le b_i^+$ with $-y_j\le x_j\le y_j$ , besides the nominal ones. Problem (∗) is the same with $y_j$ replaced by $|x_j|$ .

Formalization targets

Goal: Proposition 1 (pp. 418–419)

If $x$ extends to a feasible solution $(x,y,z)$ of (RC[ε, δ, Ω]), then $x$ is feasible for (LP) and, for every $i$ ,

\Pr\Big\{\sum_j(1+\epsilon\xi_{ij})a_{ij}x_j>b_i+\delta\max[1,|b_i|]\Big\}\le\exp\{-\Omega^2/2\}.

Milestones

The reduction in the proof of Proposition 1 (p. 419), in corrected pointwise form: a violation of row $i$ forces $\sum_{j\in J_i}\xi_{ij}a_{ij}z_{ij}>\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}$ .
Eq. (1), p. 419: for independent symmetric $\eta_j\in[-1,1]$ and reals $p_j$ ,

\Pr\Big\{\sum_j\eta_jp_j>\Omega\sqrt{\textstyle\sum_jp_j^2}\Big\}\le\exp\{-\Omega^2/2\}.

$x$ is reliable iff it is feasible for (∗) (p. 417).
(∗) is equivalent to (IRC[ε, δ]) (pp. 417–418).
Every feasible solution of (IRC) yields one of (RC) with $y_{ij}=y_j$ , $z_{ij}=0$ (p. 420).
Feasibility for (LP) together with $\sum_ja_{ij}x_j+\epsilon\beta_i(x)\le b_i^+$ , $\beta_i(x)=\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2x_j^2}$ , suffices to extend $x$ to (RC) (p. 420).
The ratio $\alpha_i(x)/\beta_i(x)$ , $\alpha_i(x)=\sum_{j\in J_i}|a_{ij}||x_j|$ , is at most $\sqrt{\mathrm{card}(J_i)}/\Omega$ , with equality attained (p. 420, corrected).

Significance

Proposition 1 turns a probabilistic requirement, which is hard to handle directly, into a single convex (second-order-cone) program. The bound $\exp\{-\Omega^2/2\}$ does not depend on the dimension, on the number of uncertain entries, or on which symmetric distributions the perturbations follow, so $\Omega$ can be chosen from the desired reliability level alone. Together with milestones 3–6, the mission certifies the whole chain: the worst-case notion of reliability is exactly Soyster's linear program (IRC), and (RC) is never more conservative than (IRC), with an advantage that can reach the factor $\sqrt{\mathrm{card}(J_i)}/\Omega$ .

The results are proved in the paper; to our knowledge none of them is machine-checked. A formal development produces a reusable model of entry-wise uncertain LPs, the counterparts (∗), (IRC) and (RC) as Lean predicates, and a Hoeffding-type bound for weighted sums of symmetric bounded variables in the exact form (1). The platform's HighDimProb.Concentration.hoeffding_rademacher covers the Rademacher special case only.

Difficulty

The deterministic parts (milestones 1, 3–7) are elementary: worst cases of interval perturbations, and the Cauchy–Schwarz inequality. The obstacle lies in the probabilistic step. The printed proof passes from $\xi_{ij}a_{ij}$ to $\xi_{ij}|a_{ij}|$ with an equality that holds only in distribution, and contains index misprints, so it cannot be transcribed line by line; the reduction has to be restated pointwise. Eq. (1) is a tail bound for general symmetric variables in $[-1,1]$ , not only for random signs; the step (c) of the printed proof of (1) is written as an equality that holds only for random signs, so that proof too needs repair. The degenerate case $\sum_jp_j^2=0$ must be handled rather than assumed away.

Formalization scope

Data are a structure UncertainLP n p m over Fin indices (0-based), with A : Matrix (Fin m) (Fin n) ℝ, J : Fin m → Finset (Fin n) arbitrary, and EReal bounds so that infinite bounds are expressible. The objective $c$ is omitted: no statement involves it.
The probability space is $(S,\mathbb P)$ with IsProbabilityMeasure; the name $S$ avoids a clash with the safety parameter $\Omega$ . Symmetry is equality of the laws of $\xi_{ij}$ and $-\xi_{ij}$ ; values lie in $[-1,1]$ at every outcome; independence is required within each row only, with no identical distribution (§3.1 says only "independent", which is weaker than the "iid" of §2.2). Probabilities are P.real.
The hypotheses $\epsilon>0$ , $\delta>0$ , $\Omega>0$ are the paper's standing assumptions and are carried by every theorem that mentions the parameter.
Corrections of the printed text: $a_{ij}x_i\to a_{ij}x_j$ in (IRC); $\sum_{j\in J}\to\sum_{j\in J_i}$ in (RC); the reduction of milestone 1 is stated with $a_{ij}$ and $z_{ij}$ in place of the printed $|a_{ij}|$ , $x_i-y_{ij}$ and $y_j$ , $y_{ij}$ ; and the ratio of milestone 7 carries the factor $1/\Omega$ that the printed " $\sqrt{\mathrm{card}(J_i)}$ " omits.
Ruling out trivializations: the violation event uses the signed multiplicative model $(1+\epsilon\xi_{ij})a_{ij}$ , never $|a_{ij}|$ or an additive perturbation; the goal concludes both nominal feasibility (i) and the probability bound (ii′) for every row; no hypothesis excludes the degenerate case $\sum_{j\in J_i}a_{ij}^2z_{ij}^2=0$ ; and the probability model is satisfiable (e.g. by $\xi\equiv0$ or by Rademacher signs), so the goal is not vacuous.
The numerical remarks of the paper (0.92, 5.24, $10^{-6}$ , "at least 30") and the NETLIB case study are not formalized.
Reusable beyond this mission: the uncertain-LP model and the three counterparts, and the tail bound (1). Contributions of general lemmas about symmetric bounded random variables are welcome.

Selected references

A. Ben-Tal, A. Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Math. Program. Ser. A 88 (2000) 411–424. https://doi.org/10.1007/s101070000163
A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Oper. Res. 21 (1973) 1154–1157. https://doi.org/10.1287/opre.21.5.1154
A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23 (1998) 769–805. https://doi.org/10.1287/moor.23.4.769
A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Oper. Res. Lett. 25 (1999) 1–13. https://doi.org/10.1016/S0167-6377(99)00016-4
D. Bertsimas, M. Sim, The price of robustness, Oper. Res. 52 (2004) 35–53. https://doi.org/10.1287/opre.1030.0065
W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

12 thms4 active usersReviewed

Completed

Algorithmic Game Theory Linear Optimization Operations Research·Captain: mikedeng1

The Assignment Game I: The Core 2: The High-Price and Low-Price Corners of the CoreResearch Paper

Motivation

A two-sided market in which each seller owns one indivisible good (a house, in the paper's example) and each buyer wants at most one is the simplest model in which prices emerge from bargaining between individuals rather than from a supply curve. Shapley and Shubik, The Assignment Game I: The Core (Int. J. Game Theory 1 (1971)), treat this market as a cooperative game with transferable utility and describe its core, the set of payoff divisions that no group of traders can improve upon by trading among themselves. The paper is the foundation of the literature on assignment markets, auctions of heterogeneous items, and two-sided matching with money.

This mission formalizes the paper's structural result on the shape of the core, Theorem 3 (p. 121): among all core outcomes there is a high-price corner in which every seller simultaneously receives the highest payoff available in the core and every buyer the lowest, and a low-price corner with the roles reversed; these two corners are the farthest-apart pair of core points. The authors note (p. 121, footnote 2) that a similar theorem for markets without money is proved by Gale and Shapley (1962), where it becomes the existence of seller-optimal and buyer-optimal stable matchings.

Setting

Let $M$ be a finite set of sellers and $N$ a finite set of buyers, with $m = |M|$ and $n = |N|$ not necessarily equal. For each seller $i$ and buyer $j$ a number $a_{ij} \ge 0$ is given: the gain the pair can realize by trading (Eq. (2.5), p. 114; Sec. 2.3, p. 116).

A coalition $S \subseteq M \cup N$ is described by its seller part $A = S \cap M$ and buyer part $B = S \cap N$ . A matching inside $(A, B)$ is a set $P \subseteq A \times B$ of seller–buyer pairs in which no player occurs twice. The characteristic function (Eq. (2.6), p. 115) gives the coalition the best total gain it can realize by pairing its members:

\operatorname{worth}(A, B) = \max_{P \text{ matching in } (A,B)} \sum_{(i,j) \in P} a_{ij}.

A matching of the whole market attaining $\operatorname{worth}(M, N)$ is an optimal assignment.

A payoff vector is a pair $(u, v)$ with $u \in \mathbb{R}^M$ (sellers' payoffs) and $v \in \mathbb{R}^N$ (buyers' payoffs). The core (p. 118) consists of the payoff vectors with

\sum_{i \in M} u_i + \sum_{j \in N} v_j = \operatorname{worth}(M, N) \quad (3.5), \qquad \sum_{i \in A} u_i + \sum_{j \in B} v_j \ge \operatorname{worth}(A, B) \ \text{ for all } A \subseteq M,\ B \subseteq N \quad (3.6).

Singleton coalitions have worth $0$ , so core vectors are nonnegative; the paper calls them "imputations in the core".

For a seller $i$ , write $u^*_i$ and $u_{*i}$ for the highest and lowest value of $u_i$ over the core; for a buyer $j$ , write $v^*_j$ and $v_{*j}$ likewise.

Formalization targets

Goal: Theorem 3 (p. 121)

The low-price corner $(u_*, v^*)$ and the high-price corner $(u^*, v_*)$ are in the core, and for all core vectors $(u', v')$ , $(u'', v'')$ ,

\sum_{i \in M} (u'_i - u''_i)^2 + \sum_{j \in N} (v'_j - v''_j)^2 \le \sum_{i \in M} (u_{*i} - u^*_i)^2 + \sum_{j \in N} (v^*_j - v_{*j})^2 .

Milestones, in attack order

Sec. 3.2, p. 118 — the core is nonempty.
Sec. 3.3, p. 120 — the core is closed, convex and bounded (a polytope).
Sec. 3.3, proof of the Lemma, p. 121 — on an optimal assignment $P$ , every core vector has $u_i + v_j = a_{ij}$ for $(i, j) \in P$ and pays $0$ to players $P$ leaves unassigned.
Lemma, p. 121 — for core vectors $(u', v')$ , $(u'', v'')$ , the vectors $(\min(u', u''), \max(v', v''))$ and $(\max(u', u''), \min(v', v''))$ (coordinatewise) are in the core.
Sec. 3.3, p. 122 — any two core vectors satisfy $|u'_i - u''_i| \le u^*_i - u_{*i}$ and $|v'_j - v''_j| \le v^*_j - v_{*j}$ for every $i$ and $j$ .

Milestone 5 is the strongest form of the distance clause of the goal: it gives the same conclusion for every distance that depends only on the absolute values of the coordinate differences, as the paper remarks on p. 122.

Significance

The result. Theorem 3 says that the core of an assignment market is elongated along the direction of market-wide price movements: "intergroup allocations are relatively indeterminate, intragroup allocations are relatively precise" (p. 121). The high-price corner is the outcome most favourable to all sellers at once, and the low-price corner the one most favourable to all buyers; that such simultaneous optima exist is a property of this game, not of cores in general. The low-price corner, the buyers' optimum, is the outcome reached by the ascending multi-item auction of Demange, Gale and Sotomayor (J. Polit. Econ. 94 (1986)), and the lattice structure underlies the incentive analysis of assignment mechanisms.

Formalizing it. The theorem is classical and fully proved in the paper; Prove2Me has no formalization of it, and nothing on the platform treats transferable-utility assignment games (the platform's stable-matching material concerns the non-transferable-utility model). The mission produces a reusable definition of the assignment game and its core, the lattice property of the core, and the extremal-corner theorem, stated with the core's extrema defined intrinsically rather than as parameters.

Difficulty

The proof in the paper takes a finite family of core vectors realizing all the extremal values and applies the Lemma repeatedly (p. 122). That argument presupposes that each extremum $u^*_i$ , $u_{*i}$ , $v^*_j$ , $v_{*j}$ is attained by some core vector, which the paper takes from the core being a nonempty polytope without stating it separately. Nonemptiness is itself the substantive result of the paper's linear-programming analysis (Theorem 2, via the duality theorem and the integrality of the assignment polytope), and it is not available here as a black box. The other nontrivial point is the Lemma's efficiency claim: that the coordinatewise min/max vectors still distribute exactly $\operatorname{worth}(M, N)$ , which depends on the structure of an optimal assignment and fails for the naive combination $(\max(u', u''), \max(v', v''))$ .

Formalization scope

Players and matrix. $M$ and $N$ are arbitrary finite types (Fintype); either may be empty and $m \ne n$ is allowed. The matrix is a : M → N → ℝ, and every theorem carries the paper's standing assumption $a_{ij} \ge 0$ as a hypothesis. No other hypothesis is added.
Coalitions are pairs (A, B) : Finset M × Finset N. Matchings are finsets of pairs with injective projections. The paper maximizes over exactly $k = \min(|S \cap M|, |S \cap N|)$ disjoint pairs; the formalization maximizes over matchings of every size, which gives the same value because $a_{ij} \ge 0$ .
Naming. The characteristic function is worth, since v denotes buyers' payoffs.
Core is a Set ((M → ℝ) × (N → ℝ)) defined by (3.5) and (3.6) over all coalitions, with no separate nonnegativity clause (it follows from singleton coalitions).
Extremal payoffs uHi, uLo, vHi, vLo are sSup/sInf in ℝ of the image of the core under a coordinate. On an empty or unbounded set these return $0$ ; the goal does not assume the core nonempty or bounded, so it is not vacuous and does not hide milestones 1–2 as hypotheses. The goal's membership clauses imply attainment of the extrema.
Distance. The goal uses the Euclidean distance on $\mathbb{R}^M \times \mathbb{R}^N$ through sums of squared coordinate differences. Lean's default dist on a product of function types is the sup-distance and is not used.
Ruled out. A formalization in which $u^*, u_*, v^*, v_*$ are free parameters constrained only by the conclusion, or in which the goal assumes a nonempty bounded core, would trivialize or weaken Theorem 3; the extrema here are computed from the core.
Not formalized. The dimension statements of p. 120 ("typically equal to min(m,n)") are informal. The LP characterization of the core (Theorem 2) is the subject of the companion mission of this series and is not restated.
Welcome contributions. Lemmas about matchings inside coalitions (injectivity, sums over images), the implication "dual feasible $\Rightarrow$ coalitionally rational", and general facts about sSup/sInf of compact coordinate images are reusable for any assignment-market or TU-matching development.

Selected references

L. S. Shapley and M. Shubik, The Assignment Game I: The Core, International Journal of Game Theory 1 (1971), 111–130. https://doi.org/10.1007/BF01753437
D. Gale and L. S. Shapley, College Admissions and the Stability of Marriage, American Mathematical Monthly 69 (1962), 9–15. https://doi.org/10.2307/2312726
G. Demange, D. Gale and M. Sotomayor, Multi-Item Auctions, Journal of Political Economy 94 (1986), 863–872. https://doi.org/10.1086/261393
G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179

7 thms4 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

Learnability, Stability and Uniform Convergence III: For an ERM, Leave-One-Out Stability, Universal Consistency and Universal Generalization Are EquivalentResearch Paper

Motivation

Algorithmic stability asks how much the output of a learning algorithm changes when its training sample is perturbed. Since Devroye and Wagner (IEEE Trans. Inf. Theory 1979) it has served as a route to generalization bounds that does not go through the complexity of the hypothesis class. Bousquet and Elisseeff (JMLR 2002) popularised uniform stability, and Mukherjee, Niyogi, Poggio and Rifkin (Adv. Comput. Math. 2006) showed that for empirical risk minimisation in supervised learning, a leave-one-out type of stability is necessary and sufficient for consistency.

Shalev-Shwartz, Shamir, Srebro and Sridharan (JMLR 11, 2010) study stability in Vapnik's General Learning Setting, where uniform convergence can fail even though the problem is learnable. In Appendix A.2 they compare replace-one and leave-one-out (LOO) stability. For an empirical risk minimiser they prove that LOO stability is equivalent to consistency and to generalization, provided each property holds with one rate for all distributions (Theorem 31, p. 2667). This mission formalizes that theorem and the lemmas of Section 5.3 on which its proof rests.

Timeline:

1979, Devroye–Wagner: leave-one-out estimates for local rules.
2002, Bousquet–Elisseeff: uniform stability implies generalization.
2002, Kutin–Niyogi (UAI 2002): a taxonomy of stability notions.
2006, Mukherjee et al.: LOO stability characterises consistency of ERM in supervised learning.
2010, Shalev-Shwartz et al.: in the General Learning Setting, for ERMs, LOO stability, universal consistency and universal generalization are equivalent (Theorem 31). Universally consistent AERMs need not be LOO stable (Example 6).

Setting

A learning problem consists of an instance space $\mathcal Z$ with a $\sigma$ -algebra, a nonempty hypothesis class $\mathcal H$ , and an objective $f:\mathcal H\times\mathcal Z\to\mathbb R$ with $|f(h;z)|\le B$ for all $h,z$ . For a probability measure $\mathcal D$ on $\mathcal Z$ :

the risk is $F(h)=\mathbb E_{z\sim\mathcal D}[f(h;z)]$ and the optimal risk is $F^*=\inf_{h}F(h)$ ;
for a sample $S=(z_1,\dots,z_m)\sim\mathcal D^m$ of $m$ i.i.d. draws, the empirical risk is $F_S(h)=\frac1m\sum_{i}f(h;z_i)$ , and $F_S(\hat h_S)=\inf_hF_S(h)$ denotes the minimal empirical risk;
a learning rule $A$ maps each sample of size $m\ge1$ to a hypothesis $A(S)$ . It is an ERM if $F_S(A(S))=F_S(\hat h_S)$ for every sample. It is an AERM with rate $\varepsilon_{\mathrm{erm}}$ if $\mathbb E[F_S(A(S))-F_S(\hat h_S)]\le\varepsilon_{\mathrm{erm}}(m)$ ;
$A$ is consistent with rate $\varepsilon$ if $\mathbb E_{S\sim\mathcal D^m}[F(A(S))-F^*]\le\varepsilon(m)$ . It generalizes with rate $\varepsilon$ if $\mathbb E[|F(A(S))-F_S(A(S))|]\le\varepsilon(m)$ , and it on-average generalizes if $|\mathbb E[F(A(S))-F_S(A(S))]|\le\varepsilon(m)$ ;
writing $S^{\setminus i}$ for $S$ with $z_i$ removed, $A$ is LOO stable with rate $\varepsilon$ (Definition 29) if

\frac1m\sum_{i=1}^m\mathbb E_{S\sim\mathcal D^m}\Big[\big|f(A(S^{\setminus i});z_i)-f(A(S);z_i)\big|\Big]\le\varepsilon(m).

A rate is a sequence $\varepsilon(m)$ that is non-increasing and tends to $0$ . A property holds universally if it holds under every $\mathcal D$ with one and the same rate.

Formalization targets

Goal: Theorem 31

For an ERM $A$ :

A\ \text{universally LOO stable}\iff A\ \text{universally consistent}\iff A\ \text{universally generalizes}.

The statement has no rates. Each side asserts that some rate exists and serves every distribution.

Milestones

In the order the proof uses them:

Utility Lemma 12: $\mathbb E|X-\mathbb EX|\le B/\sqrt m$ for the mean $X$ of $m$ i.i.d. variables bounded by $B$ .
Utility Lemma 13: $X\le Y$ a.s. implies $\mathbb E|X|\le|\mathbb EX|+2\mathbb E|Y|$ .
Lemma 14: an AERM that on-average generalizes with rate $\varepsilon_{\mathrm{oag}}$ generalizes with rate $\varepsilon_{\mathrm{oag}}+2\varepsilon_{\mathrm{erm}}+2B/\sqrt m$ .
Lemma 15: under the same hypotheses the rule is consistent with rate $\varepsilon_{\mathrm{oag}}+\varepsilon_{\mathrm{erm}}$ .
Lemma 16 (Main Converse Lemma): in a learnable problem, $\mathbb E|F_S(\hat h_S)-F^*|\le2\varepsilon_{\mathrm{cons}}(m')+2B/\sqrt m+2Bm'^2/m$ for $2\le m'\le m/2$ .
Lemma 17: Eq. (12), together with an AERM that is consistent, gives generalization with rate $\varepsilon_{\mathrm{emp}}+\varepsilon_{\mathrm{erm}}+\varepsilon_{\mathrm{cons}}$ .
First display of the proof of Theorem 31: a generalizing ERM is LOO stable with rate $\varepsilon_{\mathrm{gen}}(m-1)$ .
Second display: a LOO stable ERM on-average generalizes on samples of size $m-1$ with rate $\varepsilon_{\mathrm{stable}}(m)+2B/m$ .

Significance

Theorem 31 shows that for exact ERMs, LOO stability is not only sufficient but necessary for consistency. It transfers the supervised-learning characterisation of Mukherjee et al. to the General Learning Setting, where uniform convergence is no longer available as an intermediate. The hypothesis is sharp in one direction: Example 6 of the paper gives a universally consistent AERM that is not LOO stable. The equivalence therefore depends on exact minimisation, and an asymptotic minimiser does not suffice.

The lemmas are useful on their own. Lemmas 14 and 15 are the standard bridges between on-average generalization, generalization and consistency. Lemma 16 says that the minimal empirical risk estimates $F^*$ consistently in every learnable problem, even when no ERM learns. Lemma 16 also underlies Theorem 7, the paper's main characterisation of learnability, which is the subject of mission I of this series.

The results are proved in the paper. As far as is known they have not been formalized in any proof assistant. The platform has the textbook side of this framework (Shalev-Shwartz and Ben-David, Understanding Machine Learning, Chapter 13). Those statements are in $\mathbb R^d$ and use a replace-one stability notion; they do not cover leave-one-out stability or the General Learning Setting.

Difficulty

The implications between stability and generalization change the sample size: $S^{\setminus i}$ has $m-1$ points, so a statement about the rule at size $m$ has to be compared with the rule at size $m-1$ under the marginal law of the reduced sample. The step from universal consistency to generalization needs Lemma 16. That lemma estimates $F^*$ from a sample on which the ERM itself may be inconsistent, and it is the only place where universality of the consistency rate is used. Per-distribution consistency of an ERM does not imply generalization (Example 1 of the paper). An argument that fixes $\mathcal D$ throughout therefore cannot succeed.

Formalization scope

Samples are tuples $S:\mathrm{Fin}\,m\to\mathcal Z$ with law Measure.pi (the i.i.d. product), and $S^{\setminus i}$ is Fin.removeNth i S. A learning rule is a family $A_m:\mathcal Z^m\to\mathcal H$ . Its value at $m=0$ is never used, and LOO stability is required only for $m\ge2$ . $F_S(\hat h_S)$ is the infimum $\inf_hF_S(h)$ and no minimiser is chosen. An ERM is a rule attaining this infimum at every sample. A rate is non-increasing on $m\ge1$ and tends to $0$ . Universal properties are stated as "there exists $\varepsilon$ with IsRate ε such that for every probability measure $\mathcal D$ …", with the rate chosen before the distribution. The bound $B$ is any bound on $|f|$ ; the paper's $B$ is $\sup|f|$ , and all its rates increase with $B$ .

Measurability is not discussed in the paper. The formalization assumes that each $f(h;\cdot)$ is measurable and that the rule is measurable in the sense that $(S,z)\mapsto f(A_m(S);z)$ is jointly measurable. Lemmas 14–17 also assume that $S\mapsto\inf_hF_S(h)$ is measurable. For a measurable ERM this holds automatically, so Theorem 31 makes no such assumption. Without these assumptions Lean's integral of a non-measurable function is $0$ and every rate bound would hold trivially. For the same reason Utility Lemma 13 assumes $X,Y$ integrable. The ERM hypothesis of the goal must not be weakened to an AERM: the statement would then be false (Example 6).

One statement corrects the printed text. In the second display of the proof of Theorem 31 (p. 2668), the chain adds $2B/m$ and then drops it. The milestone states the bound the argument proves, $\varepsilon_{\mathrm{stable}}(m)+2B/m$ . The rate-free Theorem 31 is unaffected.

The development needs product measures, independence and variance bounds, all available in Mathlib, and the marginals of Measure.pi under removal of a coordinate. The definitions of risks, rules and stability notions can be reused by other stability results. Proofs of any milestone are welcome, and so are alternative proofs of the goal.

Selected references

S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, Stability and Uniform Convergence, Journal of Machine Learning Research 11 (2010) 2635–2670. https://jmlr.org/papers/v11/shalev-shwartz10a.html
O. Bousquet, A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
S. Mukherjee, P. Niyogi, T. Poggio, R. Rifkin, Learning theory: stability is sufficient for generalization and necessary and sufficient for consistency of empirical risk minimization, Advances in Computational Mathematics 25 (2006) 161–193. https://doi.org/10.1007/s10444-004-7634-z
S. Kutin, P. Niyogi, Almost-everywhere algorithmic stability and generalization error, UAI 2002. https://arxiv.org/abs/1301.0579
L. Devroye, T. Wagner, Distribution-free performance bounds for potential function rules, IEEE Transactions on Information Theory 25(5) (1979) 601–604. https://doi.org/10.1109/TIT.1979.1056087

11 thms4 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization+2·Captain: mikedeng1

Learnability, Stability and Uniform Convergence II: Tikhonov-Regularized ERM Learns Convex Lipschitz Stochastic Optimization in Hilbert Space with High ProbabilityResearch Paper

Motivation

Statistical learning theory asks when a rule that sees only an i.i.d. sample $z_1,\dots,z_m$ from an unknown distribution $D$ can return a hypothesis whose expected loss is close to the best possible. In supervised classification the classical answer is uniform convergence: learnability holds exactly when empirical risks converge to expected risks uniformly over the hypothesis class, and then empirical risk minimization (ERM) learns. Shalev-Shwartz, Shamir, Srebro and Sridharan (JMLR 11, 2010) showed that in Vapnik's broader General Learning Setting this picture breaks down. Their motivating example is stochastic convex optimization in a Hilbert space: minimizing an expected convex, Lipschitz objective over a bounded convex set from samples. This problem underlies regularized linear prediction, kernel methods and online-to-batch conversions, and the paper shows (§4.1) that in infinite dimension uniform convergence can fail and the plain empirical minimizer can fail to converge, while the problem is still learnable.

This mission formalizes the positive half of that example: Tikhonov-regularized ERM learns every such problem, with an explicit bound holding with probability $1-\delta$ (Theorem 3, p. 2644), through the stability of strongly convex empirical minimization (Theorem 2).

Setting

Let $Z$ be a measurable space of instances and $E$ a real Hilbert space. A stochastic convex optimization problem consists of a nonempty, closed, convex, bounded set $\mathcal H\subseteq E$ and an objective $f:E\times Z\to\mathbb R$ such that for every $z$ the map $h\mapsto f(h;z)$ is convex and $L$ -Lipschitz on $\mathcal H$ , each $f(h;\cdot)$ is measurable, and $|f(h;z)|\le C$ on $\mathcal H\times Z$ . For a distribution $D$ on $Z$ define the risk and optimal risk

F(h)=\mathbb E_{z\sim D}[f(h;z)],\qquad F^*=\inf_{h\in\mathcal H}F(h),

and for a sample $S=(z_1,\dots,z_m)\sim D^m$ the empirical risk $F_S(h)=\frac1m\sum_{i=1}^m f(h;z_i)$ . A function $g$ is $\lambda$ -strongly convex on $\mathcal H$ if $g-\frac\lambda2\|\cdot\|^2$ is convex there. The regularized empirical minimizer is

\hat h_\lambda\in\operatorname*{arg\,min}_{h\in\mathcal H}\Big(F_S(h)+\frac\lambda2\|h\|^2\Big).\tag{5}

For the general part, a learning rule $A$ maps samples to hypotheses; it is an AERM with rate $\varepsilon_{\mathrm{erm}}$ if $\mathbb E[F_S(A(S))-\inf_hF_S(h)]\le\varepsilon_{\mathrm{erm}}(m)$ , consistent with rate $\varepsilon_{\mathrm{cons}}$ if $\mathbb E[F(A(S))-F^*]\le\varepsilon_{\mathrm{cons}}(m)$ , and uniform-RO stable with rate $\varepsilon_{\mathrm{stable}}$ if replacing any one sample point changes the loss at any test point by at most $\varepsilon_{\mathrm{stable}}(m)$ on average over the replaced index (Definition 4).

Formalization targets

Goal: Theorem 3

If $\|h\|\le B$ on $\mathcal H$ , $L,B>0$ , $\delta\in(0,1)$ , $m\ge1$ and $\lambda=\sqrt{16L^2/(\delta B^2m)}$ , then with probability at least $1-\delta$ over $S\sim D^m$

F(\hat h_\lambda)-F^*\ \le\ 4\sqrt{\frac{L^2B^2}{\delta m}}\Big(1+\frac8{\delta m}\Big).

The constants are the paper's.

Milestones, in the order the proof uses them

Quadratic growth at a minimizer of a $\lambda$ -strongly convex $g$ : $g(h')-g(h)\ge\frac\lambda2\|h'-h\|^2$ (§4.2, p. 2644).
Eq. (6): if $f(\cdot;z)$ is $\lambda$ -strongly convex and $L$ -Lipschitz, empirical minimizers of $S$ and of $S^{(i)}$ satisfy $|f(\hat h_S,z)-f(\hat h_S^{(i)},z)|\le 4L^2/(\lambda m)$ for all $z$ (p. 2645).
Theorem 8: a uniform- or average-RO stable AERM is consistent with rate $\varepsilon_{\mathrm{stable}}+\varepsilon_{\mathrm{erm}}$ and generalizes with rate $\varepsilon_{\mathrm{stable}}+2\varepsilon_{\mathrm{erm}}+2C/\sqrt m$ (p. 2649).
$\mathbb E_{S\sim D^m}[F(\hat h_S)-F^*]\le 4L^2/(\lambda m)$ for the strongly convex empirical minimizer (p. 2645).
Theorem 2: with probability $1-\delta$ , $F(\hat h_S)-F^*\le 4L^2/(\delta\lambda m)$ (p. 2644).
Theorem 2 applied to $r(h;z)=\frac\lambda2\|h\|^2+f(h;z)$ : with probability $1-\delta$ , $\frac\lambda2\|\hat h_\lambda\|^2+F(\hat h_\lambda)\le\inf_h\big(\frac\lambda2\|h\|^2+F(h)\big)+4(L+\lambda B)^2/(\delta\lambda m)$ (p. 2645).

Significance

The result. Theorem 3 shows that every convex, Lipschitz, bounded stochastic optimization problem over a bounded subset of a Hilbert space is learnable at rate $O(LB/\sqrt{\delta m})$ , with no dimension dependence and no uniform convergence. Together with the counterexamples of §4.1 it separates learnability from uniform convergence and from ERM, and it motivates the paper's general characterization: a problem is learnable if and only if it admits a uniform-RO stable asymptotic empirical risk minimizer (Theorem 7). Theorem 8 is the sufficiency half of that characterization and is reused wherever stability arguments give generalization bounds.

Formalizing it. The results are proved in the paper; to our knowledge none has a machine-checked proof. The closest platform material is the textbook treatment in Understanding Machine Learning, chapter 13 (Shalev-Shwartz and Ben-David): Corollary 13.9 (UnderstandingML.convex_lipschitz_bounded_learnable), Corollary 13.6 (rlm_lipschitz_stable) and Lemma 13.5 (strongly_convex_lemma). Those are stated in $\mathbb R^d$ , bound the risk in expectation, use the regularizer $\lambda\|w\|^2$ over all of $\mathbb R^d$ , and have different constants; the present mission works in an arbitrary Hilbert space, over a constraint set $\mathcal H$ , with high-probability bounds and the paper's constants. Its definitions of learning rules, AERM, consistency and replace-one stability in the General Learning Setting are reusable by the other missions of this series.

Difficulty

The obvious route, bounding $\sup_{h\in\mathcal H}|F(h)-F_S(h)|$ , is unavailable: §4.1 exhibits problems of exactly this type in which that supremum stays bounded away from zero for every sample size. Any successful argument therefore has to rely on a property of the learning rule rather than of the class $\mathcal H$ , and the plain empirical minimizer does not have it: §4.1 shows it can stay a constant away from $F^*$ at every sample size. A second difficulty is purely formal: the regularization parameter $\lambda$ depends on $\delta$ and $m$ , so the regularized minimizer changes with them, and all expectations involve a data-dependent hypothesis in a possibly non-separable Hilbert space, where measurability is not automatic.

Formalization scope

Lean conventions, fixed for every item:

$E$ is a real inner product space with CompleteSpace E, never assumed finite-dimensional; $\mathcal H$ is Hset : Set E, and all infima, suprema, strong convexity and Lipschitz conditions are taken on Hset only. $F^*$ is ⨅ h : Hset, F h.
Samples are Fin m → Z, $D^m$ is Measure.pi, $S^{(i)}$ is Function.update S i z', and $m\ge1$ throughout.
The paper's standing loss bound $|f|\le B$ (p. 2637) is named $C$ , because Theorem 3 uses $B$ for the norm bound $\|h\|\le B$ . $L>0$ and $B>0$ are implicit in Theorem 3's choice of $\lambda$ and are stated.
Strong convexity is Mathlib's StrongConvexOn Hset λ, which is the paper's definition.
Minimizers are selections $S\mapsto\hat h_S\in\mathcal H$ satisfying the minimization property; the theorems hold for every such selection, hence for the minimizer, which is unique by strong convexity.
Measurability, not discussed in the paper, is the series' single standing convention: each $f(h;\cdot)$ is measurable and the selection makes $(S,z)\mapsto f(\hat h_S;z)$ jointly measurable; for Theorem 8, the rule is measurable in the same sense and $S\mapsto\inf_hF_S(h)$ is measurable.
"With probability at least $1-\delta$ " is the bound $D^m\{\text{failure}\}\le\delta$ with $0<\delta<1$ .

No statement of the paper is corrected: all printed constants were checked against the proofs and are reproduced exactly.

A formalization in which the expected excess risk is a Bochner integral of a non-measurable or non-integrable function, or in which $F^*$ is an infimum over all of $E$ or over an unbounded family, would make the bounds trivially true; the measurability hypotheses, the bound $|f|\le C$ and the infimum over the nonempty set $\mathcal H$ rule this out.

Contributions welcome: proofs of the milestones in order, and in particular a reusable replace-one identity $\mathbb E[F_S(A(S))]=\frac1m\sum_i\mathbb E[f(A(S^{(i)});z'_i)]$ under Measure.pi, and Markov's inequality in the form used for high-probability bounds.

Selected references

S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, Stability and Uniform Convergence, Journal of Machine Learning Research 11 (2010) 2635–2670. https://jmlr.org/papers/v11/shalev-shwartz10a.html
S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Stochastic Convex Optimization, COLT 2009. https://www.cs.mcgill.ca/~colt2009/papers/018.pdf
O. Bousquet, A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://jmlr.org/papers/v2/bousquet02a.html
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, chapter 13. https://doi.org/10.1017/CBO9781107298019
V. N. Vapnik, Statistical Learning Theory, Wiley, 1998.

9 thms4 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: mikedeng1

Three Partition Refinement Algorithms 2: Refining by the Smaller HalfResearch Paper

Motivation

Many equivalence problems on finite structures reduce to computing the coarsest partition of a finite set that is compatible with a relation. Deciding whether two states of a finite labelled transition system are bisimilar, testing congruence of finite-state processes in Milner's calculus of communicating systems (CCS), and minimizing a deterministic finite automaton are all instances. Kanellakis and Smolka studied the relational version in connection with CCS equivalence and gave an $O(mn)$ -time algorithm, conjecturing that $O(m \log n)$ was possible. Paige and Tarjan's 1987 paper answers that conjecture with an algorithm that has since become the standard method for bisimulation minimization in model checkers and process-algebra tools.

Timeline:

1971 — Hopcroft gives an $O(n \log n)$ algorithm for minimizing deterministic finite automata, i.e. for the coarsest partition stable with respect to one or more functions, using the rule "process the smaller half".
1983/1990 — Kanellakis and Smolka give an $O(mn)$ -time, $O(m + n)$ -space algorithm for the relational problem, and $O(c^2 n \log n)$ when every element has at most $c$ successors; they conjecture an $O(m \log n)$ algorithm.
1987 — Paige and Tarjan combine Hopcroft's smaller-half strategy with refinement by unions of blocks and obtain $O(m \log n)$ time and $O(m + n)$ space for the relational problem.

Setting

Let $U$ be a finite set with $n = |U|$ elements and let $E \subseteq U \times U$ be a binary relation on $U$ ; write $xEy$ for $(x, y) \in E$ and $m = |E|$ . For $S \subseteq U$ the preimage of $S$ is

E^{-1}(S) = \{x \in U \mid \exists y \in S,\ xEy\}.

A partition of $U$ is a family of nonempty, pairwise disjoint subsets of $U$ , its blocks, whose union is $U$ . A partition $R$ is a refinement of a partition $P$ if every block of $R$ lies inside a block of $P$ .

A set $B \subseteq U$ is stable with respect to $S \subseteq U$ if $B \subseteq E^{-1}(S)$ or $B \cap E^{-1}(S) = \emptyset$ : either every element of $B$ has an $E$ -successor in $S$ , or none does. A partition is stable with respect to $S$ if all its blocks are, and a partition is stable if it is stable with respect to each of its own blocks.

Given $E$ and an initial partition $P$ , the coarsest stable refinement of $P$ is a stable partition $Q$ refining $P$ such that every stable partition refining $P$ is a refinement of $Q$ . The relational coarsest partition problem asks for it.

The algorithms refine by the operation $\mathrm{split}(S, Q)$ , which replaces each block $B$ of $Q$ that meets both $E^{-1}(S)$ and its complement by the two blocks $B \cap E^{-1}(S)$ and $B - E^{-1}(S)$ . The set $S$ is a splitter of $Q$ if $\mathrm{split}(S, Q) \neq Q$ .

The naïve algorithm starts from $Q = P$ and, while possible, picks a splitter $S$ of $Q$ that is a union of blocks of $Q$ and replaces $Q$ by $\mathrm{split}(S, Q)$ .
The improved algorithm also maintains a partition $X$ , initially $\{U\}$ , of which $Q$ is a refinement. While $Q \neq X$ , it picks a block $S \in X$ that is not a block of $Q$ and a block $B \in Q$ with $B \subseteq S$ and $|B| \le |S|/2$ , replaces $S$ in $X$ by $B$ and $S - B$ , and replaces $Q$ by $\mathrm{split}(S - B, \mathrm{split}(B, Q))$ .

The improved algorithm is analysed under the standing assumption $|E(\{x\})| \ge 1$ for all $x \in U$ : every element has at least one successor. (The paper reduces the general case to this one by a preprocessing step.)

Formalization targets

Goal: the improved algorithm

For every run $(Q_0, X_0) = (P, \{U\}), \dots, (Q_K, X_K)$ of the improved algorithm with refining blocks $B_0, \dots, B_{K-1}$ :

at every stage $Q_j$ and $X_j$ are partitions, $Q_j$ refines $X_j$ , and $Q_j$ is stable with respect to every block of $X_j$ ;
if $Q_K = X_K$ , then $Q_K$ is the coarsest stable refinement of $P$ ;
if $Q_K \neq X_K$ , another step applies;
$K \le n - 1$ ;
every $x \in U$ satisfies

\#\{\, j < K \mid x \in B_j \,\} \le \log_2 n + 1.

Items 1–4 are the correctness of the improved algorithm, which the paper deduces from that of the naïve one. Item 5 is the counting fact on which the $O(m \log n)$ bound rests.

Milestones

§3, p. 978: $S$ is a splitter of $Q$ if and only if $Q$ is unstable with respect to $S$ .
Properties (1)–(3), p. 978: stability is inherited under refinement and under union; $\mathrm{split}$ is monotone in its second argument.
§3, p. 979: a stable partition is stable with respect to every union of its blocks.
Lemma 2, p. 979: every stable refinement of $P$ refines each partition produced by the naïve algorithm.
Theorem 2, p. 979: the naïve algorithm stops after at most $n - 1$ steps at the unique coarsest stable refinement.
Property (4), p. 978: $\mathrm{split}$ is commutative, and $\mathrm{split}(S, \mathrm{split}(Q, P))$ is the coarsest refinement of $P$ stable with respect to both $S$ and $Q$ .
Lemma 3, p. 980: the three-way split of a block $D$ into $D_{11}$ , $D_{12}$ and $D_2$ , including $D_{12} = D_1 \cap (E^{-1}(B) - E^{-1}(S - B))$ .

Significance

The coarsest stable refinement of the partition of states by their labels is the bisimilarity relation of a finite transition system, so the goal certifies, for any sequence of choices, the correctness of the refinement loop at the core of bisimulation minimization. The halving count is the combinatorial half of the $O(m \log n)$ bound: once the implementation charges $O(|B| + \sum_{y \in B} |E^{-1}(\{y\})|)$ per refining block $B$ , the count bounds the total work.

The results are proved in the paper, some by one-line arguments and the elementary properties (1)–(4) not at all ("stated without proof"). No machine-checked proof of the Paige–Tarjan algorithm's correctness or of its halving count is known to be available in Lean or Mathlib. The mission produces a checked account of the invariant, the final correctness and the counting argument for every run, not only for a particular implementation.

Difficulty

The correctness of the improved algorithm is not a special case of the naïve one read off directly. An improved step refines by $B$ and by $S - B$ , and $S - B$ is a union of blocks of $Q$ only because $Q$ refines $X$ . The invariant that $Q$ is stable with respect to every block of $X$ is what makes $Q = X$ a stopping condition, and it holds initially only under the standing assumption. The naive idea of reusing Hopcroft's argument fails: for relations, stability with respect to $S$ and $B$ does not imply stability with respect to $S - B$ , which is why both refinements are performed. For the halving count, the refining blocks that contain a fixed element must be shown to be nested across steps, which requires tracking how blocks of $X$ are replaced.

Formalization scope

$U$ is a Fintype with decidable equality, $E$ a decidable relation U → U → Prop. Partitions are Finset (Finset U) with an explicit predicate IsPartition (nonempty, pairwise disjoint blocks covering $U$ ); blocks are required to be nonempty, which the paper leaves implicit.
"Coarsest" means: every stable partition refining $P$ refines it. The paper's "every other stable partition" is read this way, since a stable partition that does not refine $P$ need not refine the answer.
Algorithms are step relations; a run is a finite sequence of states indexed by Fin (K + 1), with the choices $S_j, B_j$ recorded. Every statement holds for every run, so no choice rule is fixed.
Added hypotheses: $U$ nonempty (so $\{U\}$ is a partition and "at most $n - 1$ steps" is meaningful); the standing assumption $\forall x\, \exists y,\ xEy$ for the goal only. Lemma 2 is stated for every stable refinement of $P$ , which is what its proof gives and what Theorem 2 uses; it implies the printed form.
Explicit forms: $|B| \le |S|/2$ is 2 * B.card ≤ S.card, $K \le n - 1$ is K + 1 ≤ n, $\log_2$ is Real.logb 2 of $n$ cast to $\mathbb{R}$ . The termination bound for the improved algorithm is not printed in the paper and is derived as in the proof of Theorem 2. Running times ( $O(mn)$ , $O(m \log n)$ ) and the data structures of the implementation are out of scope.
A trivializing reading is ruled out: the goal quantifies over all runs from $(P, \{U\})$ with every side condition of the step (in particular $S \notin Q$ and the half-size condition), and the conclusion is a full correctness statement, not the existence of some stable partition; the discrete partition is stable but is not the answer in general.
Reusable beyond this mission: preimage, stability, $\mathrm{split}$ and its algebra (properties (1)–(4)), which apply to Hopcroft's algorithm and to bisimulation minimization in general. Contributions proving the elementary properties first, then Lemma 2 and Theorem 2, are the natural attack order.

Selected references

R. Paige, R. E. Tarjan, Three Partition Refinement Algorithms, SIAM Journal on Computing 16(6):973–989, 1987. https://doi.org/10.1137/0216062
P. C. Kanellakis, S. A. Smolka, CCS expressions, finite state processes, and three problems of equivalence, Information and Computation 86(1):43–68, 1990. https://doi.org/10.1016/0890-5401(90)90025-D
J. E. Hopcroft, An n log n algorithm for minimizing states in a finite automaton, in Theory of Machines and Computations, Academic Press, 1971, pp. 189–196. https://doi.org/10.1016/B978-0-12-417750-5.50022-1
A. V. Aho, J. E. Hopcroft, J. D. Ullman, The Design and Analysis of Computer Algorithms, Addison-Wesley, 1974.

12 thms4 active usersReviewed

Completed

Control Theory Dynamic Programming Operations Research+1·Captain: mikedeng1

Robust Control of Markov Decision Processes with Uncertain Transition Matrices 1: Perfect Duality and the Robust Dynamic Programming Recursion for Finite-Horizon MDPsResearch Paper

Motivation

A Markov decision process (MDP) is solved by dynamic programming once its transition probabilities are known. In practice they are estimated from data, and the optimal policy of an MDP can be sensitive to estimation error: a policy computed from point estimates may perform much worse under the true transition matrices. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) study the robust version of the problem, in which the controller minimises the worst-case expected cost when the transition matrices are only known to lie in given uncertainty sets, and motivate it with aircraft routing under uncertain weather.

Earlier work on MDPs with uncertain transition probabilities includes Satia and Lave (1973) and White and Eldeib (1994), which treat interval and set-valued transition models, and Givan, Leach and Dean (1997) on bounded-parameter MDPs. The robust Bellman recursion under a rectangularity assumption was obtained independently by Iyengar (Columbia technical report 2002, published as Robust dynamic programming, Math. Oper. Res. 30(2), 2005). This mission targets the finite-horizon result of Nilim and El Ghaoui: Theorem 1, which shows that the robust problem is solved by a recursion of the same shape as the nominal one and that the associated min–max game has a value.

Setting

The states form a finite set $\mathcal X=\{1,\dots,n\}$ , the decision horizon is $T=\{0,1,\dots,N-1\}$ , and the action set $\mathcal A$ is finite, nonempty and the same in every state. Costs are $c_t(i,a)\ge0$ for $t\in T$ , and there is a terminal cost $c_N(i)$ . The system starts in a given state $i_0$ .

Write $\Delta_n=\{p\in\mathbb R^n_+ : p^{\mathsf T}\mathbf 1=1\}$ for the probability simplex. For every action $a$ and state $i$ , a nonempty set $\mathcal P_i^a\subseteq\Delta_n$ describes the possible $i$ -th rows of the transition matrix under $a$ . No convexity or closedness is assumed. The rectangular uncertainty property says the uncertainty set of the matrix $P^a$ is the product $\mathcal P^a=\mathcal P_1^a\times\cdots\times\mathcal P_n^a$ .

A controller policy $\pi=(\mathbf a_0,\dots,\mathbf a_{N-1})$ consists of maps $\mathbf a_t:\mathcal X\to\mathcal A$ , and $\Pi=\mathcal A^{nN}$ is the set of such policies. A policy of nature $\tau=(P_t^a)_{a\in\mathcal A,t\in T}$ picks, for every stage, action and state, a row $p_i^a(t)\in\mathcal P_i^a$ . The admissible set is $\mathcal T=(\bigotimes_a\mathcal P^a)^N$ , so nature may change the matrices from stage to stage. The expected total cost is

C_N(\pi,\tau)=\mathbf E\Big(\sum_{t=0}^{N-1}c_t(i_t,\mathbf a_t(i_t))+c_N(i_N)\Big),

where the state $i_t$ evolves as a Markov chain with transition matrix $P_t^{\mathbf a_t(i)}$ from state $i$ . The support function of a set $\mathcal P$ is $\sigma_{\mathcal P}(v)=\sup\{p^{\mathsf T}v : p\in\mathcal P\}$ . The robust recursion (7) starts from $v_N=c_N$ and sets

v_t(i)=\min_{a\in\mathcal A}\big(c_t(i,a)+\sigma_{\mathcal P_i^a}(v_{t+1})\big),

and for a fixed $\pi$ the evaluation recursion (10) starts from $v_N^\pi=c_N$ and sets $v_t^\pi(i)=c_t(i,\mathbf a_t(i))+\sigma_{\mathcal P_i^{\mathbf a_t(i)}}(v_{t+1}^\pi)$ .

Formalization targets

Goal: Theorem 1 (Robust Dynamic Programming)

\min_{\pi\in\Pi}\sup_{\tau\in\mathcal T}C_N(\pi,\tau)=v_0(i_0)=\sup_{\tau\in\mathcal T}\min_{\pi\in\Pi}C_N(\pi,\tau),

together with three further statements. First, $\sup_{\tau}C_N(\pi,\tau)=v_0^\pi(i_0)$ for every $\pi$ . Second, every policy that chooses actions attaining the minimum in (7) (rule (8)) achieves $v_0(i_0)$ in the worst case. Third, every nature policy whose rows attain the suprema $\sigma_{\mathcal P_i^a}(v_{t+1})$ (rule (9)) forces the value $v_0(i_0)$ on every controller.

Milestones

Lemma 1: a problem $\max q^{\mathsf T}v_0$ subject to $v_t\le g_t(v_{t+1})$ with monotone $g_t$ and $q\ge0$ is solved by the recursion $v_t=g_t(v_{t+1})$ .
Support functions of nonempty subsets of $\Delta_n$ are componentwise nondecreasing.
The constraint maps of problems (15) and (16) are componentwise nondecreasing.
Eq. (14): for fixed $\pi$ and fixed matrices, $C_N(\pi,\tau)$ is the value of a linear program.
Eq. (16): $\sup_{\tau\in\mathcal T}C_N(\pi,\tau)=v_0^\pi(i_0)$ .
Eq. (15): $\sup_{\tau\in\mathcal T}\min_{\pi}C_N(\pi,\tau)=v_0(i_0)$ .

Significance

Theorem 1 shows that, under rectangular uncertainty, robustness costs one inner optimisation per state and action: the expected continuation cost $p^{\mathsf T}v_{t+1}$ of nominal dynamic programming is replaced by the support function $\sigma_{\mathcal P_i^a}(v_{t+1})$ . The equality of the min–max and max–min values says that it does not matter whether nature commits before or after the controller. The optimal controller policy remains deterministic and Markov. The later sections of the paper build on this recursion. They cover the discounted infinite-horizon case, the gap between stationary and time-varying uncertainty, and the computation of $\sigma$ for likelihood and entropy models, which the other missions of this series formalize.

The result is proved in the paper, and independently by Iyengar. It has no machine-checked proof that this mission is aware of. A formal proof yields a reusable development: a finite-horizon MDP with a forward-defined expected cost, the link between that expectation and backward linear programs, and the finite-horizon robust Bellman equation for arbitrary nonempty uncertainty sets.

Difficulty

The nominal Bellman recursion is standard. The robust statement is harder than "apply the nominal recursion under the worst matrix", because no single worst matrix need exist. The sets $\mathcal P_i^a$ are neither closed nor convex, so the suprema in $\sigma$ need not be attained, and $\mathcal T$ is not compact. Minimax theorems for convex–concave or compact games therefore do not apply. The expected cost is defined forward, as an expectation over a Markov chain, while the recursions run backward, and connecting the two is part of the work. The max–min side needs nature policies that come within any tolerance of the value simultaneously at every stage, state and action.

Formalization scope

States are Fin n and stages Fin N. Values $v_0,\dots,v_N$ are indexed by natural numbers, and only $t\le N$ is meaningful. Vectors are Fin n → ℝ with the componentwise order.
The model is a structure holding the costs ( $c_t\ge0$ ), the terminal cost (no sign assumed), and the row sets. Every row set must be nonempty and contained in stdSimplex ℝ (Fin n). Nonemptiness is implicit in the paper: without it $\mathcal T$ is empty, and a real supremum over an empty index is $0$ .
Rectangularity is built in: a nature policy is a function $\tau(t,a,i)$ with $\tau(t,a,i)\in\mathcal P_i^a$ . Nature does not observe the realised trajectory, and stationary nature ( $\mathcal T_s$ ) is not the set used here.
$C_N$ is defined by the forward state distribution, not by a backward recursion. Defining it backward would make the evaluation statements hold by definition, which is the trivializing formalization this choice rules out.
$\sigma_{\mathcal P}$ is the real sSup of $\{p^{\mathsf T}v\}$ . This is the true supremum because the set is nonempty and bounded above by $\max_j v_j$ .
Maxima over nature are suprema: ⨆ τ in the goal and IsLUB in the milestones, because the row sets need not be closed. Minima over the finite nonempty $\Pi$ and over $\mathcal A$ are ⨅. The argmax rule (9) is stated only for nature policies attaining the row suprema. The argmin rule (8) is stated for every attaining policy.
The terminal value $v_N=c_N$ is not printed in Theorem 1. It is taken from the proof and from Step 1 of the paper's algorithm (p. 785). The composition $g_1\circ\cdots\circ g_N$ in Lemma 1 is read as $g_0\circ\cdots\circ g_{N-1}$ .
Not included: Corollary 1 (the sequential game) and the accuracy part of Theorem 2. Contributions of either as additional theorems on these definitions are welcome.

Selected references

A. Nilim, L. El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
J. K. Satia, R. E. Lave, Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
C. C. White, H. K. Eldeib, Markov Decision Processes with Imprecise Transition Probabilities, Operations Research 42(4):739–749, 1994. https://doi.org/10.1287/opre.42.4.739
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

11 thms4 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization+1·Captain: mikedeng1

A Unified Framework for High-Dimensional Analysis of M-Estimators with Decomposable Regularizers: Error Bounds under Decomposability and Restricted Strong ConvexityResearch Paper

Motivation

High-dimensional statistics studies estimation when the number of parameters $p$ is comparable to, or larger than, the number of observations $n$ . The standard estimators in this regime are regularized M-estimators: minimise an empirical loss plus a penalty that encodes structure, such as the Lasso ( $\ell_1$ penalty, sparse vectors), the group Lasso (block norms, group sparsity) and nuclear-norm regularization (low-rank matrices). Before 2009 each of these estimators came with its own consistency proof. Negahban, Ravikumar, Wainwright and Yu (arXiv:1010.2731; Statistical Science 27(4), 2012, doi:10.1214/12-STS400) isolated two properties that these proofs share, decomposability of the regularizer and restricted strong convexity of the loss, and proved one deterministic theorem from them. The Lasso rates of Bickel, Ritov and Tsybakov (arXiv:0801.1095), rates under $\ell_q$ -sparsity, and group-sparse and low-rank rates then follow as corollaries. The framework is the organising principle of Chapter 9 of Wainwright's textbook High-Dimensional Statistics (Cambridge University Press, 2019).

Setting

Let $E$ be a finite-dimensional real inner product space with inner product $\langle\cdot,\cdot\rangle$ and induced error norm $\|\cdot\|$ . Given a loss $\mathcal L:E\to\mathbb R$ , a regularizer $\mathcal R:E\to\mathbb R$ and a constant $\lambda_n>0$ , program (1) is

\hat\theta_{\lambda_n}\in\arg\min_{\theta\in E}\{\mathcal L(\theta)+\lambda_n\mathcal R(\theta)\}.

For a subspace $S$ write $u_S$ for the orthogonal projection of $u$ onto $S$ , and $S^\perp$ for the orthogonal complement.

Decomposability. For subspaces $\mathcal M\subseteq\overline{\mathcal M}$ , the norm $\mathcal R$ is decomposable with respect to $(\mathcal M,\overline{\mathcal M}^\perp)$ if $\mathcal R(\theta+\gamma)=\mathcal R(\theta)+\mathcal R(\gamma)$ for all $\theta\in\mathcal M$ and $\gamma\in\overline{\mathcal M}^\perp$ . Example: the $\ell_1$ -norm with $\mathcal M=\overline{\mathcal M}=\{\theta:\theta_j=0\ \forall j\notin S\}$ .
Dual norm. $\mathcal R^*(v)=\sup_{\mathcal R(u)\le1}\langle u,v\rangle$ .
Subspace compatibility constant. $\Psi(\overline{\mathcal M})=\sup_{u\in\overline{\mathcal M}\setminus\{0\}}\mathcal R(u)/\|u\|$ ; for the $\ell_1$ -norm on an $s$ -dimensional coordinate subspace, $\Psi=\sqrt s$ .
The set $\mathbb C$ . For a point $\theta^*\in E$ ,

\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)=\{\Delta\mid\mathcal R(\Delta_{\overline{\mathcal M}^\perp})\le3\mathcal R(\Delta_{\overline{\mathcal M}})+4\mathcal R(\theta^*_{\mathcal M^\perp})\}.

Restricted strong convexity (RSC). With the Taylor error $\delta\mathcal L(\Delta,\theta^*)=\mathcal L(\theta^*+\Delta)-\mathcal L(\theta^*)-\langle\nabla\mathcal L(\theta^*),\Delta\rangle$ , the loss satisfies RSC with curvature $\kappa_{\mathcal L}>0$ and tolerance $\tau_{\mathcal L}(\theta^*)$ if $\delta\mathcal L(\Delta,\theta^*)\ge\kappa_{\mathcal L}\|\Delta\|^2-\tau^2_{\mathcal L}(\theta^*)$ for every $\Delta\in\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$ .

The conditions of the paper's main theorem are (G1): $\mathcal R$ is a norm, decomposable with respect to $(\mathcal M,\overline{\mathcal M}^\perp)$ with $\mathcal M\subseteq\overline{\mathcal M}$ ; and (G2): $\mathcal L$ is convex, differentiable and satisfies RSC. The Lean development lives in the namespace UnifiedMEstimator.General, with these objects named IsNormFn, IsDecomposable, dualNorm, compat, setC, taylorErr, RSC and IsOptimal.

Formalization targets

Goal: Theorem 1 (p. 10), tolerance term corrected

Under (G1) and (G2), if $\lambda_n>0$ and $\lambda_n\ge2\mathcal R^*(\nabla\mathcal L(\theta^*))$ , then every optimal solution of program (1) satisfies

\|\hat\theta_{\lambda_n}-\theta^*\|^2\le9\,\frac{\lambda_n^2}{\kappa_{\mathcal L}^2}\,\Psi^2(\overline{\mathcal M})+\frac{2\tau_{\mathcal L}^2(\theta^*)+4\lambda_n\mathcal R(\theta^*_{\mathcal M^\perp})}{\kappa_{\mathcal L}}.

The bound holds for every pair $(\mathcal M,\overline{\mathcal M})$ over which $\mathcal R$ decomposes, and for every optimum, not only a distinguished one.

Milestones

Lemma 1 (p. 7): under the dual-norm condition on $\lambda_n$ , the error $\hat\Delta=\hat\theta_{\lambda_n}-\theta^*$ lies in $\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$ . This milestone links an existing platform statement of the same lemma (Wainwright, Proposition 9.13).
Section 2.4, p. 10, first display: if $\theta^*\in\mathcal M$ and $\Delta\in\mathbb C$ , then $\mathcal R(\Delta)\le4\Psi(\overline{\mathcal M})\|\Delta\|$ .

Further statements

Corollary 1 (p. 11): if $\theta^*\in\mathcal M$ and $\tau_{\mathcal L}(\theta^*)=0$ , then $\|\hat\theta_{\lambda_n}-\theta^*\|\le3\lambda_n\Psi(\overline{\mathcal M})/\kappa_{\mathcal L}$ and $\mathcal R(\hat\theta_{\lambda_n}-\theta^*)\le12\lambda_n\Psi^2(\overline{\mathcal M})/\kappa_{\mathcal L}$ .
Section 2.4, p. 10, second display: a lower bound $\delta\mathcal L\ge\kappa_1\|\Delta\|^2-\kappa_2 g\,\mathcal R^2(\Delta)$ on the unit ball gives curvature $\kappa_1-16\kappa_2\Psi^2(\overline{\mathcal M})g$ on $\mathbb C$ when $\theta^*\in\mathcal M$ .
Example 1 (p. 5) and the value $\Psi(\mathcal M(S))=\sqrt{|S|}$ (p. 9): the $\ell_1$ -norm instance, which shows that the hypotheses of the goal can be met.

Significance

Theorem 1 reduces a consistency proof for a new regularized estimator to two checks: that the regularizer decomposes over a pair of subspaces adapted to the model, and that the loss is curved on the set $\mathbb C$ , together with a bound on $\mathcal R^*(\nabla\mathcal L(\theta^*))$ that is usually a concentration inequality. The paper derives from it the $s\log p/n$ Lasso rate under restricted eigenvalue conditions, rates for weakly sparse ( $\ell_q$ -ball) vectors, and group-Lasso rates; companion papers use it for low-rank matrix estimation, matrix completion and generalized linear models. Because the bound holds for every pair $(\mathcal M,\overline{\mathcal M})$ , it gives an explicit trade-off between an estimation error and an approximation error $\mathcal R(\theta^*_{\mathcal M^\perp})$ .

The theorem is proved in the paper's supplementary appendix. No machine-checked proof of it is known. On Prove2Me, Wainwright's textbook restatement (Theorem 9.19, HighDimStat.Decomposability.thm9_19_general_bound) is a related but different statement: its RSC condition is local, on a ball, with a tolerance proportional to $\mathcal R^2(\Delta)$ , and it has extra side conditions and a different bound. A formal proof of the present goal certifies the deterministic core that every corollary of the paper relies on.

Difficulty

The obvious argument compares the objective at $\hat\theta$ and at $\theta^*$ and applies RSC to the error. RSC, however, is available only on the set $\mathbb C$ , not on all of $E$ : in high dimensions the loss is flat in many directions, so strong convexity fails. The work is to show first that the error lies in $\mathbb C$ (Lemma 1, which rests on decomposability and the choice of $\lambda_n$ ), and then to relate the regularizer to the error norm through the projections onto $\overline{\mathcal M}$ and $\overline{\mathcal M}^\perp$ . The distinction between $\mathcal M$ and $\overline{\mathcal M}$ matters throughout: the compatibility constant is taken on the larger space $\overline{\mathcal M}$ , while the approximation error projects $\theta^*$ onto the complement of the smaller one. The bound comes from a quadratic inequality in $\|\hat\Delta\|$ , and the constants depend on how its terms are split.

Formalization scope

Representation. The parameter space is an arbitrary finite-dimensional real inner product space E (equivalently $\mathbb R^p$ with any inner product, as the paper allows); matrices are covered by the same abstraction. Subspaces are Submodule ℝ E, projections are Submodule.starProjection, and the gradient is Mathlib's gradient, under the hypothesis that $\mathcal L$ is differentiable. The dual norm and $\Psi$ are real suprema (sSup). They equal the paper's quantities because $\mathcal R$ is required to be a genuine norm (nonnegative, definite, absolutely homogeneous, subadditive) and $E$ is finite-dimensional; $\Psi(\{0\})=0$ . The tolerance is a real number $\tau$ entering as $\tau^2$ ; RSC contains $\kappa>0$ and is quantified over exactly $\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$ for the same pair and point as the decomposability. Every statement is for every optimal solution of program (1). The data $Z_1^n$ are fixed and absorbed into $\mathcal L$ , and $\theta^*$ is an arbitrary point: the paper's requirement that $\theta^*$ minimise the population risk is never used by the theorem and is dropped.

Corrections of the printed statements.

Display (22) prints the tolerance term as $\frac{\lambda_n}{\kappa_{\mathcal L}}\cdot2\tau^2_{\mathcal L}(\theta^*)$ . As printed the statement is false: for $E=\mathbb R$ , $\mathcal R=|\cdot|$ , $\mathcal M=\overline{\mathcal M}=\mathbb R$ , $\mathcal L(\theta)=(\max(0,|\theta|-1))^2$ , $\theta^*=0.9$ , $\lambda_n=0.01$ , $\kappa_{\mathcal L}=1/2$ , $\tau^2_{\mathcal L}=10$ , the optimum is $0$ and $\|\hat\Delta\|^2=0.81$ exceeds the printed bound $0.4036$ . The goal states $2\tau^2_{\mathcal L}(\theta^*)/\kappa_{\mathcal L}$ ; the two forms agree when $\tau_{\mathcal L}=0$ , and the constants $9$ and $4$ are the paper's.
Corollary 1's (25a) prints $\|\hat\theta-\theta^*\|\le9\lambda_n^2\Psi^2(\overline{\mathcal M})/\kappa_{\mathcal L}$ , which fails for $\mathcal L(\theta)=(\theta-0.002)^2$ , $\theta^*=0.001$ , $\lambda_n=0.004$ on $\mathbb R$ ; the mission states $3\lambda_n\Psi(\overline{\mathcal M})/\kappa_{\mathcal L}$ . Its " $\mathbb C(\mathcal M,\overline{\mathcal M},\theta^*)$ " is read as $\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$ .

Trivializations ruled out. A regularizer predicate weaker than a norm would let the real suprema collapse to the junk value $0$ and make the $\lambda_n$ condition or the $\Psi$ term free; RSC over all of $E$ would be classical strong convexity, and RSC over the cone without the $4\mathcal R(\theta^*_{\mathcal M^\perp})$ slack would make the goal false; decomposability without $\mathcal M\subseteq\overline{\mathcal M}$ or with the bars misplaced changes the theorem. None of these is used. The $\ell_1$ example and a checked one-dimensional instance show that all hypotheses of the goal can hold simultaneously.

Infrastructure and contributions. A complete development needs: Hölder's inequality for a norm and its dual norm, boundedness of the two suprema in finite dimension, the decomposability inequality $\mathcal R(\theta^*+\Delta)-\mathcal R(\theta^*)\ge\mathcal R(\Delta_{\overline{\mathcal M}^\perp})-\mathcal R(\Delta_{\overline{\mathcal M}})-2\mathcal R(\theta^*_{\mathcal M^\perp})$ , the first-order characterization of convexity, and the solution of a scalar quadratic inequality. The dual-norm and compatibility-constant lemmas are reusable for every decomposable-regularizer mission. Proofs of the milestones, of the goal, and of the $\ell_1$ instance are all welcome.

Selected references

S. N. Negahban, P. Ravikumar, M. J. Wainwright, B. Yu, A Unified Framework for High-Dimensional Analysis of M-Estimators with Decomposable Regularizers, Statistical Science 27(4), 2012, 538–557. arXiv:1010.2731v3, doi:10.1214/12-STS400
P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous Analysis of Lasso and Dantzig Selector, Annals of Statistics 37(4), 2009, 1705–1732. arXiv:0801.1095
M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 9. doi:10.1017/9781108627771

5 thms4 active usersReviewed

Completed

Combinatorics Linear Optimization Operations Research+1·Captain: Shuze Chen

Disjunctive Programming XV: Dominants of Polytopes and Upper SeparationTextbook

Motivation

Many real-world disjunctive models are not unions of polyhedra in a single shared space, but unions of polyhedra in different spaces linked by a logical implication: some action affecting one set of entities has consequences for another. Balas's treatment of such models (§17 of the book, following [17]) reduces to understanding a single auxiliary object attached to each polytope in isolation: its dominant, the set of points that dominate (coordinatewise) some feasible point. Dominants and their duals, blockers, have a long history in combinatorial optimization — blocking-pair theory for covering and packing polyhedra traces to Fulkerson (D. R. Fulkerson, Blocking and anti-blocking pairs of polyhedra, Mathematical Programming 1 (1971), 168–194, https://doi.org/10.1007/BF01584085) — but this chapter develops a self-contained, constructive theory tailored to polytopes inside the unit cube, culminating in an exact, facet-complete description of the dominant for an arbitrary such polytope.

Setting

For a polyhedron $P \subseteq \mathbb{R}^n_+$ , the dominant is $P^+ := P + \mathbb{R}^n_+ = \{y \ge 0 : y \ge x \text{ for some } x \in P\}$ , and the blocker is $P^* := \{\pi \in \mathbb{R}^n_+ : \pi x \ge 1 \text{ for all } x \in P\}$ — the covering inequalities valid for $P$ . (The blocker is not the reverse polar of 02b-polarity: restricting to the nonnegative orthant is essential and changes the object.) For $x^* \in \mathbb{R}^n_+$ , the upper-separation value is $\alpha_P(x^*) := \min\{\pi x^* : \pi \in P^*\}$ ; a violated covering inequality for $x^*$ exists exactly when $\alpha_P(x^*) < 1$ . A polytope $P \subseteq [0,1]^n$ is upper monotone (with respect to $[0,1]^n$ ) if $P = P^+ \cap [0,1]^n$ — the natural "closure" condition under which the theory of this chapter applies cleanly.

For $S \subseteq N := \{1,\dots,n\}$ , write $a(S) := \sum_{j\in S} a_j$ . Given $P \subseteq \mathbb{R}^n$ and a coordinate subset $S$ , the projection $P^S$ keeps only the $S$ -coordinates, letting the rest range freely. $I^S$ is the set of valid inequalities $\pi x \ge 1$ of $P^S$ with $\pi_j > 0$ exactly on $S$ , tight at $|S|$ linearly independent points of $P^S$ .

Formalization targets

Proposition 13.1. For an upper monotone $P = \bigcap_i P_i$ (each $P_i$ a single inequality in $[0,1]^n$ ), $P^+ = \bigcap_i P_i^+$ .

Theorem 13.3. For $P = \{x \in [0,1]^n : ax \ge 1\}$ ( $a \ge 0$ ) upper monotone,

P^+ = \Big\{x \ge 0 : \sum_{j\in S} \frac{a_j x_j}{1-a(N\setminus S)} \ge 1 \text{ for every } S\subseteq N \text{ with } 1-a(N\setminus S)>0\Big\}.

Theorem 13.5. For the same $P$ and any $x^* \ge 0$ , with $x^*_q$ the greatest coordinate value $x^*_j$ satisfying $a(N\setminus S(x^*_j))<1$ and $x^*_j \le g(x^*_j)$ : $S(\alpha_P) = S(x^*_q)$ and $\alpha_P = g(x^*_q)$ , an explicit, computable value.

Theorem 13.7 (goal). For an arbitrary polytope $P \subseteq [0,1]^n$ (not necessarily upper monotone):

P^+ = \{x \ge 0 : \pi x \ge 1 \text{ for every } S \subseteq N \text{ and } \pi \in I^S\},

and every one of these inequalities is facet-defining for $P^+$ .

Corollary 13.8. Every facet-defining inequality of $P^+$ has at most $\dim(P)+1$ nonzero coefficients.

The targets move from the intersection-distributivity fact (13.1) through an explicit, exponentially-large but fully closed-form facet system for the single-inequality case (13.3) and its constructive, polynomial evaluation recipe (13.5) to the fully general facet characterization (13.7, requiring no monotonicity assumption at all) and its immediate corollary on facet sparsity (13.8).

Significance

Theorem 13.7 is a rare case in polyhedral combinatorics of a complete and exact facet description obtained for the dominant of an arbitrary polytope, not merely a valid relaxation or an algorithmic separation oracle — every facet is accounted for, and every listed inequality is genuinely a facet, not merely valid. Corollary 13.8's support bound is the mechanism that makes Theorem 13.10 (not part of this mission) tractable: it lets the facets of a dominant built from a disjunction of polytopes in different spaces be characterized purely in terms of each factor's own low-dimensional facets, avoiding an exponential blowup in the combined space.

Both directions are proved in the source (Balas's own treatment, following the joint framework of [17]) but have no counterpart on this platform: nothing existing treats dominants, blockers, or upper monotonicity. This mission produces the first Lean statements of all five targets.

Difficulty

The obvious shortcut for Theorem 13.7 is to state only the validity half of the claim (every inequality from $I^S$ is valid for $P^+$ ) and treat "facet-defining" as a decoration — after all, Proposition 13.1's polar-style validity argument generalizes easily. But the theorem's actual force is the converse: not merely that these inequalities suffice to describe $P^+$ , but that none of them is redundant, and no other facet exists. The book's own converse proof needs a genuine perturbation argument (splitting a facet candidate with fewer than $|S|$ independent tight points into two distinct valid inequalities averaging back to it, contradicting facetness) — this is where the real content lives, and a formalization that only captures the forward direction would understate the theorem substantially.

For Theorem 13.5, the difficulty is that $S(\alpha)$ and $g(\alpha)$ are themselves defined in terms of $\alpha$ , so "the largest $x^*_j$ satisfying [a condition stated in terms of $S(x^*_j)$ and $g(x^*_j)$ ]" is a genuinely self-referential extremal characterization, not a closed-form formula one could simply plug into — hence its faithful statement (via IsGreatest over an explicit, self-referential candidate set) rather than an unwound algebraic expression.

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default. Dominant/Blocker are given their own names (not reusing, even informally, 02b-polarity's polar/reverse-polar vocabulary), per BRIEF.md's explicit warning that the nonnegativity restriction makes these different objects. PolyDim/IsFacet are restated from 02b-polarity/11a-intersection-cuts (affine dimension via Module.finrank of vectorSpan, faces via IsExtreme), since Chapter 2 already pins these down precisely for this series and Chapter 13's own facet claims use the same notion. IsUpperMonotone is stated exactly as Definition 4 (P = P⁺ ∩ [0,1]ⁿ), not paraphrased as coordinatewise monotonicity, per BRIEF.md's explicit warning that these are different conditions.

IsInIS (membership in $I^S$ ) uses LinearIndependent ℝ directly for the "|S| linearly independent points" hypothesis, matching the book's own wording; since every such point satisfies $\pi x=1$ , a linear dependence among them is automatically an affine dependence (the coefficients of any nontrivial linear relation among them must sum to zero), so this is not a weakening of the more familiar "affinely independent" reading a reader might otherwise expect. A trivializing formalization to rule out explicitly: describing Theorem 13.7's $P^+$ using only the validity half of the claim (dropping "each of these inequalities is facet-defining for $P^+$ ") — this mission states both conjuncts, since the facet-exactness is the theorem's genuine content beyond a Farkas-style validity certificate.

This mission depends on no other chunk's Lean definitions; it restates the affine-dimension/facet vocabulary of 02b-polarity/11a-intersection-cuts only informally, per the series convention. Corollary 13.6 (an $O(n)$ -time algorithmic claim for computing $\alpha_P$ ) is out-of-cone per BRIEF.md: it is fully quantified, not a veto-V3 case, but is a computational-complexity statement outside this mission's polyhedral-characterization scope.

Selected references

D. R. Fulkerson, Blocking and anti-blocking pairs of polyhedra, Mathematical Programming 1 (1971), 168–194. https://doi.org/10.1007/BF01584085
E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs (for the broader monotonization-of-polyhedra context cited by this chapter's introduction), European Journal of Operational Research 4 (1980), 224–234. https://doi.org/10.1016/0377-2217(80)90106-X
E. Balas, Disjunctive Programming, Springer, 2018, Chapter 13, §13.1–13.2. https://doi.org/10.1007/978-3-030-00148-3

8 thms4 active users

Completed

Linear Optimization Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming XIV: Disjunctive Cuts from the V-Polyhedral RepresentationTextbook

Motivation

The lift-and-project cut-generating LP (CGLP) is the workhorse of the book's cutting-plane machinery, but its number of variables grows with $q$ , the number of terms in the disjunction — a real computational cost for disjunctions with many terms. An alternative representation of the same disjunctive hull, built from vertices and extreme rays rather than from a dual LP, trades this away: its number of variables is fixed at $n$ regardless of $q$ , at the price of a constraint set that is generally exponential in size (T. H. Kim, V-polyhedral disjunctive cuts, PhD thesis and papers with E. Balas; the underlying representation traces to the classical Minkowski–Weyl theorem for polyhedra). This mission formalizes the chapter's capstone: the V-polyhedral, lift-and-project, and generalized-intersection-cut families — three representations that look structurally different — coincide exactly.

Setting

A disjunctive set in V-polyhedral (vertex-ray) form is $F := \bigcup_{h\in Q} P^h$ , $P^h := \mathrm{conv}\,V^h + \mathrm{cone}\,R^h$ , where $V^h$ / $R^h$ are the (finite) sets of vertices and extreme rays of the $h$ -th disjunct. The conic hull of a set $S$ is the set of all finite nonnegative combinations of its elements. For a reference point $x_F \in F$ , the disjunctive cone $C_{x_F}$ is the homogenization, at $x_F$ , of the translated disjunctive system: $(x',x_0') \in \mathbb{R}^n \times \mathbb{R}_+$ with $Ax' + (Ax_F-b)x_0' \ge 0$ and $\bigvee_h(D^hx' + (D^hx_F-d^h_0)x_0' \ge 0)$ .

For a relaxation $\tilde P^h$ of each disjunct with $P^h \subseteq \tilde P^h \subseteq C(x^h)$ (the LP cone at the disjunct's own optimum $x^h$ ), write $\tilde V^h$ , $\tilde R^h$ for its vertices and rays, and $C := \mathrm{conv}(\bigcup_h \tilde V^h) + \mathrm{cone}(\bigcup_h \tilde R^h)$ for the single combined polyhedron they generate. The associated L&P cut-generating LP is

\alpha = u^h \tilde D^h, \qquad \beta \le u^h \tilde d^h_0 \quad (h\in Q), \qquad \textstyle\sum_{h\in Q} u^h e = 1, \qquad u^h \ge 0.

Formalization targets

Proposition 12.1. $\alpha x \ge \beta$ is valid for $F$ if and only if $\alpha p \ge \beta$ for every $p \in V^h$ and $\alpha r \ge 0$ for every $r \in R^h$ , over every $h \in Q$ .

Proposition 12.3. For a cut $\alpha x \ge \beta$ tight at $x_F$ ( $\alpha x_F = \beta$ ) and $x \in F$ : $\alpha x < \beta$ if and only if $\alpha(x - x_F) < 0$ for the corresponding point $(x - x_F, 1)$ of $C_{x_F}$ .

Theorem 12.4. If $(\alpha,\beta)$ satisfies $\alpha p \ge \beta$ for every $p \in \tilde V^h$ and $\alpha r \ge 0$ for every $r \in \tilde R^h$ (over every $h$ ), and the mixed-integer feasible set $P_I$ lies in the combined polyhedron $C$ , then $\alpha x \ge \beta$ is valid for $P_I$ .

Theorem 12.5 (goal). $(\alpha,\beta)$ is valid for the combined vertex-ray system if and only if there exists a multiplier $u = \{u^h\}_{h\in Q}$ making it simultaneously a feasible solution of the CGLP above and a generalized intersection cut from

S := \{x \in \mathbb{R}^n : u^h \tilde D^h x \le u^h \tilde d^h_0,\ h \in Q\}.

The targets move from the elementary generator-validity fact (12.1) and its algorithmic companion (12.3, which the iterative cut-generation procedure of §12.1 uses to search only adjacent extreme points) through the same validity criterion generalized to a relaxed system (12.4) to the three-way unification (12.5) that is the entire point of introducing the V-polyhedral representation in the first place.

Significance

Theorem 12.5 explains why the V-polyhedral approach is worth having at all: it produces exactly the same cuts as the lift-and-project CGLP, so nothing is lost by switching representations, while the computational cost profile is reversed (the book's own estimate, not part of this mission's targets, shows the V-polyhedral approach at least $q^3$ times cheaper for a $q$ -term disjunction using $\tilde P^h = C(x^h)$ ). This matters directly for disjunctions with many terms — split disjunctions used one or two at a time throughout most of the earlier chapters — which the CGLP approach makes increasingly expensive as $q$ grows, but which the V-polyhedral approach handles without a growing variable count.

Both directions are proved in the source (this book's own §12, citing the underlying V-polyhedral cut idea to Balas's joint work with T. H. Kim, and the GIC-to-L&P equivalence to §11.4's own Theorem 11.5) but have no formalized counterpart on this platform: nothing existing treats V-polyhedral representations, disjunctive cones, or a three-way cut-family equivalence. This mission produces the first Lean statements of all four targets.

Difficulty

The obvious shortcut for Theorem 12.5 is to state only "the V-polyhedral cuts and the L&P cuts coincide" and treat the GIC leg as a footnote, since the book's own two-line proof dispatches the GIC equivalence by citing an earlier theorem rather than re-deriving it. But the theorem's actual claim is a three-way equivalence with a specific, described $S$ built from the very multipliers that solve the CGLP — dropping the GIC leg, or defining $S$ independently of those multipliers, would understate what is being asserted (the book's own remark following the theorem stresses that the GIC-defining points and the V-polyhedral vertices are typically different points that nonetheless yield equivalent cuts, which is exactly the content a two-way statement would erase).

For Theorem 12.4, the subtlety is that $C$ (the combined polyhedron) is not the union $\bigcup_h \tilde P^h$ but its convex hull — a strictly larger set in general — so validity for $C$ 's generators is a priori a stronger requirement than validity for each $\tilde P^h$ separately; the theorem's force is that this stronger validity is still exactly what is needed (and obtained) to conclude validity for $P_I$ .

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default, with the disjunction index Q left as a general type for Propositions 12.1/12.3 (so the same Ph/DisjSet definitions serve any finite disjunction) and specialized to [Fintype Q] where a finite sum over disjuncts is needed (Theorem 12.4's combined polyhedron, the CGLP of Theorem 12.5). V^h/R^h (Proposition 12.1) and Ṽ^h/R̃^h (Theorem 12.4) are formalized with the same underlying definitions (Ph, IsVPolyhedralValid) applied to different vertex/ray data, per BRIEF.md's explicit warning that these are distinct objects — not by duplicating the definitions under two names. "Is a generalized intersection cut from $S$ " (IsGICFromS) is formalized via the exact characterization Theorem 11.4's own remark in 11a-intersection-cuts gives for the GIC family (valid outside $S$ 's interior, and a genuine cut), rather than by re-deriving the underlying extreme-ray construction — a trivializing formalization this mission rules out would instead drop this leg's dependence on the same multiplier u that witnesses the CGLP leg, decoupling S from the solution it is supposed to come from.

This mission depends on no other chunk's Lean definitions; it restates 02a-convex-hull's vertex/extreme-point vocabulary, 11a-intersection-cuts's cut apparatus, and 11b-monoidal-strengthening's disjunctive-cut conventions only informally, per the series convention. Theorem 12.2 (the extreme-ray/edge correspondence underlying the "adjacent vertices only" search strategy) was not drafted this pass — see HARD.md — since a faithful, non-circular formalization of "edge of a polytope incident with a point" needs face-lattice machinery beyond what any earlier chunk in this series has built. The ConicHull/DisjunctiveCone/CombinedC definitions are reusable by any later mission touching V-polyhedral cut generation.

Selected references

E. Balas and T. H. Kim, Cutting planes from extended LP formulations, Mathematical Programming 156 (2016), 587–606. https://doi.org/10.1007/s10107-015-0885-2
E. Balas and M. Perregaard, Generalized intersection cuts and a new cut generating paradigm, Mathematical Programming A 137 (2013), 19–35. https://doi.org/10.1007/s10107-011-0483-x
A. Kazachkov, Non-Recursive Cut Generation, PhD dissertation, Carnegie Mellon University, 2018 (cited by Balas for the relaxation-based V-polyhedral cut generator of §12.2).
E. Balas, Disjunctive Programming, Springer, 2018, Chapter 12. https://doi.org/10.1007/978-3-030-00148-3

7 thms4 active users

Completed

Linear Optimization Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming XIII: Monoidal Cut Strengthening and the Gomory Mixed-Integer CutTextbook

Motivation

The Gomory mixed-integer (GMI) cut is the single most widely deployed cutting plane in practical mixed-integer programming: every commercial solver generates it, from a simplex tableau row, essentially for free. Yet the GMI cut is not the strongest cut derivable from the same row: once a subset of the variables is known to be integer-constrained, that integrality can be used to tighten the cut's coefficients further, a technique due to Balas and Jeroslow that predates and motivates most of the general disjunctive-cut machinery of this book (E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs, European Journal of Operational Research 4 (1980), 224–234, https://doi.org/10.1016/0377-2217(80)90106-X). This mission formalizes the culmination of that line of work: two refinements of the GMI cut, each strictly stronger than the plain GMI coefficient on part of the variable set, obtained by applying monoidal cut strengthening — optimizing a cut's coefficients over an algebraic monoid of admissible integer shifts — to the two-term split disjunction that produces the GMI cut in the first place (E. Balas and R. Jeroslow, as above; the monoidal strengthening framework itself due to R. E. Gomory and E. L. Johnson, and formalized in the generality used here by G. Nemhauser and L. Wolsey and by J. -P. P. Richard, Y. Li and A. Miller).

Setting

Fix a row of a simplex tableau: $y = a_0 - \sum_{j\in J} a_j x_j$ , with $x_j \ge 0$ for $j \in J$ , $x_j$ integer for $j$ in a subset $J_1 \subseteq J$ , and $0 < a_0 < 1$ . If $y$ is itself integer-constrained, every feasible solution satisfies the split disjunction $y \le 0 \lor y \ge 1$ , from which the ordinary GMI cut $\alpha x \ge 1$ follows, with $\alpha_j := \max\{a_j/a_0,\ -a_j/(1-a_0)\}$ uniformly over all of $J$ .

For a general $q$ -term disjunction $\bigvee_{h\in Q}(\sum_j a^h_j x_j \ge a^h_0)$ with a known background lower bound $b^h_0 \le a^h_0$ on each term's left side, the cut monoid is

M := \{\mu \in \mathbb{Z}^q : \textstyle\sum_{h\in Q} \mu_h \ge 0\}.

Given the disjunction and the lower bounds, replacing each term's coefficient $a^h_j$ (for $j$ in the integer-constrained set $J_1$ ) with $a^h_j + \mu^j_h(a^h_0 - b^h_0)$ for any fixed $\mu^j \in M$ leaves the disjunction — and hence the disjunctive cut it implies — valid; optimizing this replacement over the whole monoid strengthens the resulting cut. For the normalized $q$ -term disjunction $\bigvee_{i\in Q}(\sum_j a_{ij}x_j \ge a_{i0})$ (each right-hand side scaled to a common reference), the unstrengthened cut coefficient is $\beta_j := \max_{i\in Q} a_{ij}/a_{i0}$ .

Formalization targets

Theorem 11.19. For the general $q$ -term disjunctive-cut situation, every $x \ge 0$ satisfying the background lower bound and the disjunction also satisfies the monoidally-strengthened cut $\sum_j \alpha_j x_j \ge \alpha_0$ , with

\alpha_j = \begin{cases} \inf_{\mu^j\in M}\max_{h\in Q}\theta_h[a^h_j+\mu^j_h(a^h_0-b^h_0)], & j\in J_1, \\ \max_{h\in Q}\theta_h a^h_j, & j\in J\setminus J_1,\end{cases} \qquad \alpha_0 = \min_{h\in Q}\theta_h a^h_0.

Proposition 11.22. For the normalized disjunction, and any fixed monoid elements $m^j \in M$ ( $j\in J_1$ ), every $x\ge0$ integer on $J_1$ satisfying the disjunction and the background lower bound also satisfies the strengthened disjunction with each term's coefficients shifted by $m^j$ — the fact that licenses optimizing over the whole monoid afterward.

Corollary 11.25. For each disjunct index $k$ , the cut $\delta^k x \ge 1$ is valid, with $\delta^k_j := \min\{(a_{kj}+a_{k0}-b_k)/a_{k0},\ \beta_j\}$ on $J_1$ and $\delta^k_j :=\beta_j$ elsewhere — a version of monoidal strengthening needing no optimization over $M$ at all.

Theorem 11.26 (goal). Specializing the same monoidal strengthening machinery to the two-term split disjunction $y \le 0 \lor y \ge 1$ itself: both $\alpha^+ x \ge 1$ and $\alpha^- x \ge 1$ are valid cuts, with $\alpha^+$ given by a three-case piecewise formula (eq. (11.55)) refining the GMI coefficient on part of $J_1$ , and $\alpha^-$ symmetric (eq. (11.56)).

The targets move from the general monoidal-strengthening theorem (11.19) through its validity engine in normalized form (Proposition 11.22, directly cited by the intermediate Theorem 11.23 that the goal specializes) and its optimization-free cousin (Corollary 11.25, immediately preceding the goal in the same subsection) to the concrete payoff for the single most-used cut in practice.

Significance

Theorem 11.26's cuts are not a theoretical curiosity: Corollary 11.27 (not drafted this pass) gives an explicit, checkable condition under which each cut is strictly stronger than the plain GMI cut, and Example 4 (p. 187–188) gives a fully worked six-variable instance where the improvement is concrete and numerically verifiable. Since the GMI cut is generated by essentially every mixed-integer solver at essentially every node of a branch-and-cut search, a cheap, always-valid strengthening of it — derivable from the same tableau row with no extra data beyond knowing which variables are integer-constrained — has direct practical reach far beyond this one book.

Both directions are proved in the source (Balas and Jeroslow 1980 for the underlying strengthening idea; this book's own Theorem 11.19/Proposition 11.22/Theorem 11.23 chain for the general monoidal framework applied here) but have no counterpart on this platform: nothing existing treats monoidal cut strengthening, the cut monoid itself, or a refinement of the GMI cut. This mission produces the first Lean statements of all four targets.

Difficulty

The obvious shortcut for Theorem 11.26 is to collapse $\alpha^+$ 's three-case definition into the plain GMI formula $\max\{a_j/a_0,\ -a_j/(1-a_0)\}$ applied uniformly — after all, that formula already gives a valid cut, and the strengthened cases can only make individual coefficients smaller (better). But a uniform formula reproduces exactly the plain GMI cut and can never be strictly stronger than it, which is the entire content the goal theorem (via Corollary 11.27) is building toward; the piecewise case split over $J^+_1$ (where $a_j>1$ ), $J^{>}_1$ (where $a_0-1\le a_j\le1$ ), and the rest is not incidental bookkeeping but the mechanism by which integrality actually buys something.

For Proposition 11.22 and Theorem 11.19, the difficulty is that the strengthening must remain valid simultaneously for every choice of the monoid element $\mu^j$ (or $m^j$ ) — not merely for some cleverly chosen one — since Theorem 11.19's conclusion then takes an infimum over the entire monoid $M$ , which is generally infinite. Fixing a single "obviously good" $\mu^j$ and stopping there would prove a weaker, non-optimized statement.

Formalization scope

The ambient space is Fin n → ℝ throughout, matching the series default, with the disjunction index set Q represented as Fin q and the cut monoid CutMonoid q : Set (Fin q → ℤ). Theorem 11.19 is formalized with scalar per-term coefficients $a^h_j$ (one real number per disjunct $h$ and variable $j$ ), rather than the fully general "each term a multi-row system $A^h x \ge a^h_0$ " framing the book's surrounding prose (§11.8's opening) sketches before specializing: every downstream result this mission needs (Proposition 11.22 onward, via (11.38)) is already stated at the single-inequality-per-term level, so this is not a weakening relative to what is actually used, only relative to a more general preamble that is never itself given a numbered, formalizable statement. AlphaJStrengthened uses sInf over the (possibly infinite) monoid literally, not a fixed near-optimal representative. AlphaPlus/AlphaMinus use the exact three-case structure of (11.55)/(11.56) — collapsing them into the uniform GMI formula is the trivializing formalization this mission rules out, since a uniform formula could never realize the theorem's actual (strictly stronger, on part of the domain) claim.

This mission depends on no other chunk's Lean definitions; it restates 11a-intersection-cuts's disjunctive-cut vocabulary only informally (the underlying disjunctive-cut idea, not any specific Lean declaration), per the series convention. A complete development needs: properties of sInf over an unbounded-below-safe subset of ℤ-indexed reals, and case analysis on Int.floor/ Int.ceil for the piecewise formulas. The cut-monoid and unstrengthened/strengthened-coefficient definitions are reusable by any later mission touching monoidal strengthening (e.g. a future mission on Theorem 11.23's full Lopsided-cut construction or the multiple-term-disjunction material of §11.9.2–11.9.3, not drafted this pass).

Selected references

E. Balas and R. G. Jeroslow, Strengthening cuts for mixed integer programs, European Journal of Operational Research 4 (1980), 224–234. https://doi.org/10.1016/0377-2217(80)90106-X
R. E. Gomory and E. L. Johnson, T-space and cutting planes, Mathematical Programming 96 (2003), 341–375. https://doi.org/10.1007/s10107-003-0389-3
J.-P. P. Richard, Y. Li, and L. A. Miller, Valid inequalities for MIPs and group polyhedra from approximate liftings, Mathematical Programming A 118 (2009), 253–277. https://doi.org/10.1007/s10107-007-0190-9
E. Balas, Disjunctive Programming, Springer, 2018, Chapter 11, §11.8–11.9. https://doi.org/10.1007/978-3-030-00148-3

8 thms4 active users

Completed

Linear Optimization Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming VIII: Nonlinear Higher-Dimensional RepresentationsTextbook

Motivation

Chapter 2's convex-hull machinery gives an exact, finitely-generated linear description of a disjunctive set's convex hull, but for a mixed 0-1 program with $p$ binary variables that description lives in a space with roughly $pn$ auxiliary variables — one full lift per disjunction. This chapter surveys the alternative nonlinear higher-dimensional constructions that several authors proposed for the same target, $\mathrm{conv}(K_0)$ : multiplying the constraint system by products of $x_j$ and $1-x_j$ and linearizing the resulting quadratic terms, rather than disjoining and projecting one variable at a time. Two such constructions — Lovász and Schrijver's "cones of matrices" lift $N(K)$ , and Sherali and Adams's hierarchy $K_t$ — both converge to the integer hull, and the chapter's central point is that both convergence proofs reduce, after all the nonlinear machinery is stripped away, to results already established by disjunctive programming's own one-variable-at-a-time convexification (Theorem 2.1, specialized here to Theorem 7.1, and the sequential-convexifiability theorem of Chapter 3).

Setting

$K := \{x \in \mathbb R^n : Ax \ge b,\ x \ge 0,\ x_j \le 1,\ j=1,\dots,p\} = \{x : \tilde A x \ge \tilde b\}$ is the LP relaxation of a mixed 0-1 program with $p$ of its $n$ variables 0-1 constrained, and $K_0 := K \cap \{x_j \in \{0,1\},\ j=1,\dots,p\}$ its feasible set. $P_j(K)$ (Section 7.1) multiplies $\tilde A x \ge \tilde b$ by $(1-x_j)$ and $x_j$ , linearizes $y_i := x_ix_j$ and $x_j := x_j^2$ , and projects onto $x$ ; iterating over a coordinate sequence gives $P_{i_1,\dots,i_t}(K)$ . $N(K)$ (Section 7.2, Lovász-Schrijver) instead linearizes with a single symmetric matrix $Y$ ( $Y_{ij} = Y_{ji} = x_ix_j$ for every pair) before projecting, and iterates as $N^t(K) := N(N^{t-1}(K))$ . $K_t$ (Section 7.3, Sherali-Adams) multiplies by every product of $t$ literals $\prod_{j\in J_1}x_j\prod_{j\in J_2}(1-x_j)$ ( $|J_1\cup J_2|=t$ ), linearizes each resulting monomial with a fresh "moment" variable, and projects.

Formalization targets

Theorem 7.6 (goal) — the Sherali-Adams hierarchy reaches the integer hull

K_p = \mathrm{conv}(K_0).

The chain of results building toward it

Theorem 7.1 ( $P_j(K)$ equals the one-variable convex hull, a special case of Theorem 2.1), Theorem 7.2 (iterating $P_j$ over a fixed sequence reaches the hull of imposing $0/1$ on all of them), Corollary 7.3 (iterating over every 0-1 index reaches $\mathrm{conv}(K_0)$ ), Theorem 7.4 ( $N(K) \subseteq P_j(K)$ for every $j$ ), Theorem 7.5 (iterating $N$ over $p$ steps reaches $\mathrm{conv}(K_0)$ , by the same containment), and Theorem 7.7 ( $K_t \subseteq P_{1,\dots,t}(K)$ , proved by a genuine induction re-deriving every valid inequality of $P_{1,\dots,t}(K)$ from $(NL_t)$ 's own rows).

Significance

The results themselves. This chapter is disjunctive programming's account of why three independently-developed convexification hierarchies — its own lift-and-project, Lovász-Schrijver, and Sherali-Adams — all reach the same integer hull: not by coincidence, but because each one's convergence proof is, at bottom, a disguised instance of the book's own Theorem 2.1 and Chapter 3 machinery. This is part of what situates disjunctive programming as the unifying framework behind several major lift-and-project hierarchies used throughout integer programming.

Formalizing it. No object in this mission exists on the platform prior to it or in Mathlib. This mission restates 03-sequential-convex's and 02a-convex-hull's vocabulary locally (per the series convention that a draft mission cannot import another draft mission's definitions), specialized throughout to the split disjunction $x_j \in \{0,1\}$ .

Difficulty

The chapter's own account of the Sherali-Adams construction (Section 7.3) is narrative rather than displaying an explicit linear system for $(NL_t)$ , unlike every other construction in this chapter (contrast eq. (7.1) and eq. (7.4), both displayed explicitly) — Step 1 says only "multiply $\tilde Ax \ge \tilde b$ with every product of the form $\prod_{j\in J_1}x_j \cdot \prod_{j\in J_2}(1-x_j)$ ." Deriving the actual linear system this multiplication produces requires expanding every $(1-x_j)$ factor via inclusion-exclusion over $S \subseteq J_2$ before the monomials can be linearized — a real, if mechanical, derivation step this mission had to carry out itself (RowNLt, see MODERATION_NOTES.md) rather than transcribe from a displayed equation. Theorem 7.7's own proof is a genuine argument (an induction re-deriving a valid inequality of $P_{1,\dots,t}(K)$ from $(NL_t)$ 's rows layer by layer), not a restatement, so it is included as a milestone with real mathematical content rather than assumed.

Correcting BRIEF.md. The brief's "Recommended goal theorem" section mislabels Theorem 7.6 as the Lovász-Schrijver result " $K^p = \mathrm{conv}(K_0)$ " — cross-checked directly against the PDF, Theorem 7.6 (p. 95, PDF 101) is stated [112] Kp = conv(K0), cited to Sherali and Adams, appearing immediately after Section 7.3 introduces $K_t$ . The actual Lovász-Schrijver iteration-reaches-the-hull result, cited [99], is Theorem 7.5 (Np(K) = conv(K0)), formalized in this mission as a milestone (lovasz_schrijver_reaches_hull) rather than the goal. See STATUS.md.

Formalization scope

Three distinct convexification operators are kept fully distinguishable throughout, as BRIEF.md warns: Pj/IteratedSplit (one-variable-at-a-time, Section 7.1, Def_..._Basic), NOp/MK (Lovász-Schrijver, Section 7.2, Def_..._Lifts), and KtSet/IsXt (Sherali-Adams, Section 7.3, Def_..._Lifts) — no shared abbreviation or lemma conflates their defining predicates, even though all three converge to the same hull.

$N^t(K)$ 's iteration (Theorem 7.5) is formalized via a dependent family of representations A t, b t for t : Fin (p+1) with a hypothesis relating consecutive steps to NOp's image at the previous step — the same pattern 04-normal-forms's Theorem 4.10 uses — since each successive $N^t(K)$ genuinely has a different, larger ambient constraint system, not a fixed matrix's power.

Theorem 7.7 is stated for an arbitrary $t$ -subset $S \subseteq N'$ rather than the literal prefix $\{1,\dots,t\}$ the book's own statement uses (its own proof, by induction, treats an arbitrary inequality of $P_{1,\dots,t}(K)$ with no dependence on the prefix's specific ordering), which is what the goal theorem's proof, applied at $S = N'$ , actually needs.

The Bienstock-Zuckerberg results quoted narratively in Section 7.5 ("Theorem 1"/"Theorem 2", [43]/[44]) are out-of-cone: the book itself presents them only as a survey of a further lift operator, under their own source papers' numbering, not as Balas's own numbered results, and does not restate their proofs.

Selected references

E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 7.
L. Lovász, A. Schrijver, Cones of matrices and set-functions and 0-1 optimization, SIAM Journal on Optimization 1 (1991), 166-190 (cited in the text as [99], the origin of the $N(K)$ construction and Theorems 7.4-7.5).
H.D. Sherali, W.P. Adams, A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems, SIAM Journal on Discrete Mathematics 3 (1990), 411-430 (cited in the text as [112], the origin of the $K_t$ construction and Theorem 7.6).

16 thms4 active users

Completed

Linear Optimization Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming VII: Lift-and-Project Cuts for Mixed 0-1 ProgramsTextbook

Motivation

A mixed 0-1 program's feasible region is a disjunctive set built from the split disjunctions $x_j \le 0 \lor x_j \ge 1$ , one per binary variable — a special case general enough that Chapter 2's convex-hull machinery applies directly, yet structured enough to produce closed-form cutting planes efficiently. The resulting lift-and-project (L&P) cuts, generated by solving a small auxiliary linear program (the cut-generating LP, CGLP) rather than by hand-derived combinatorial argument, were part of a cluster of ideas that drove a dramatic improvement in commercial mixed-integer solvers' practical performance from the mid-1990s onward. This chapter develops the theory that makes L&P cuts computationally practical: how to bound how many rounds of cutting are needed (disjunctive rank), what can and cannot be guaranteed about intermediate fractional solutions during sequential convexification, how to generate a cut cheaply by solving the CGLP only over the LP relaxation's active variables and lift the result back to the full variable space in closed form, and how to strengthen a single-disjunction cut into one valid for the whole integer program using the integrality of the other 0-1 variables.

Setting

For the mixed 0-1 program $\min\{cx : Ax \ge b,\ x \ge 0,\ x_j \in \{0,1\},\ j=1,\dots,p\}$ , let $P$ be its LP relaxation (written $\{x : \tilde A x \ge \tilde b\}$ after folding in the bound constraints) and $D := \{x \in P : x_j \le 0 \lor x_j \ge 1,\ j=1,\dots,p\}$ its disjunctive feasible set. Sequential convexification produces $P_1 := \mathrm{conv}(P \cap \{x_1 \in \{0,1\}\})$ , then $P_{1j} := \mathrm{conv}(P_1 \cap \{x_j \in \{0,1\}\})$ , and so on. The cut-generating LP (CGLP) for the disjunction on coordinate $j$ asks for $(\alpha,\beta)$ and multipliers $u,v \ge 0$ , scalars $u_0,v_0$ , satisfying $\alpha - u\tilde A + u_0 e_j = 0$ , $\alpha

v\tilde A - v_0 e_j = 0 $,$ \beta - u\tilde b = 0 $,$ \beta - v\tilde b - v_0 = 0 $. Solving `(CGLP)` only over a **restricted** set of active rows/columns$ M_R, R$ gives (CGLP)^R, whose solution can be lifted back to a solution of the full (CGLP) in closed form.

Formalization targets

Theorem 6.4 (goal) — the general mixed-integer cut-lifting formula

\gamma_k = \min\{\alpha^1_k + u_0\lceil \bar m_k\rceil,\ \alpha^2_k - v_0\lfloor \bar m_k\rfloor\} \ (k \in N'), \qquad \gamma_k = \alpha_k\ (k \notin N'), \qquad \bar m_k = \frac{\alpha^2_k - \alpha^1_k}{u_0+v_0},

with $\gamma x \ge \beta$ valid for the whole mixed 0-1 program, strengthening a cut $\alpha x \ge \beta$ valid only for the single disjunction on $j$ .

The chain of results building toward it

Theorem 6.1 (an extreme point of $P_1$ cut off at a facet of $P_{1j}$ cannot be fractional in $x_1$ without being fractional in $x_j$ too), Theorem 6.2 (an explicit closed-form extension of a restricted CGLP solution to the full CGLP), and Corollary 6.3 (the same fact, stated transparently via a $\max\{\alpha^1,\alpha^2\}$ formula and asserted feasible for the full CGLP).

Significance

The results themselves. Theorem 6.4 is what turns lift-and-project cuts from "valid for one binary variable's split" into genuine cuts for the whole mixed-integer program, using no information beyond the integrality of the other 0-1 variables — this strengthening step is part of why L&P cuts became practically competitive with other cutting-plane families. Theorem 6.2 and Corollary 6.3's cut-lifting property is, independently, what makes generating L&P cuts affordable at industrial scale: solving the CGLP only over a problem's few hundred active variables rather than its hundreds of thousands of total variables, then reading off the remaining coefficients in closed form.

Formalizing it. No object in this mission — the cut-generating LP, its restricted version, or the mixed-integer cut-lifting formula — exists on the platform prior to this mission or in Mathlib. This mission restates the disjunctive-set and convex-hull vocabulary of the earlier missions in this series locally (per the series convention that a draft mission cannot import another draft mission's definitions), applied specifically to the split disjunction on a single 0-1 variable.

Difficulty

The natural first attempt at Theorem 6.1 assumes that once $x_1$ has been "locked in" by sequential convexification, every subsequent cut generated while processing later variables respects that integrality — the book's own Figures 6.1-6.2 refute this directly, exhibiting facet- defining cuts that cut through the interior of an edge at a point fractional in every coordinate. Theorem 6.1's genuine content is the narrower but still useful fact that extreme points of the right intersection cannot exhibit this failure. The difficulty in Theorem 6.4 is recognizing that naively substituting $x_j - mx \le 0 \lor x_j - mx \ge 1$ for varying integer vectors $m$ gives a family of valid cuts, not a single one — the theorem's content is the closed-form choice of $m$ (via rounding $\bar m_k$ up or down, whichever yields the smaller coefficient) that is provably optimal within this family, not merely one valid choice among many.

Formalization scope

All results are stated over Fin n → ℝ with the CGLP's row space left as an abstract finite type M (rather than fixing the exact m+p+n-row block structure the book's own augmented matrix Ã has), since the substantive content of every theorem in this chapter depends only on dot products against columns of Ã, never on which literal row a given bound constraint occupies. Alpha1/Alpha2 (Corollary 6.3's row-restricted dot products) and Alpha1_64/Alpha2_64 (Theorem 6.4's eq.-(6.4) values, which add or subtract $u_0$ / $v_0$ at the disjunction coordinate) are kept as separate definitions throughout, per BRIEF.md's explicit warning that the two chapters' " $\alpha^1,\alpha^2$ " notation refers to different formulas despite the shared symbol.

Theorem 6.2's closed-form extension is formalized via the values it assigns (matching every printed formula for ū_{m+i}, v̄_{m+i}, ᾱ_i), without committing to the book's own literal row-block indexing (m+i vs. m+n+i) for the fresh rows a full reading of the source does not fully disambiguate for variables outside the 0-1 index set — Corollary 6.3, the chapter's own "more transparent" restatement of the same fact, is instead formalized with an explicit fresh-row construction (AtilExt, BtilExt) verifying genuine feasibility for the extended (CGLP). In Theorem 6.4, $u_0, v_0 > 0$ is stated as an explicit hypothesis, matching BRIEF.md's flag that this positivity (needed for $\bar m_k$ 's division) is implicit in the CGLP feasibility setup rather than a free-standing assumption of the printed theorem.

A trivializing formalization is ruled out explicitly: Theorem 6.4's conclusion is stated as genuine validity for the full MIPDisjunctiveSet (imposing $0/1$ simultaneously on every $k \in N'$ ), not merely as the closed-form formula for $\gamma$ with no accompanying validity claim, which would omit the theorem's actual mathematical content.

Selected references

E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 6.
E. Balas, S. Ceria, G. Cornuéjols, A lift-and-project cutting plane algorithm for mixed 0-1 programs, Mathematical Programming 58 (1993), 295–324 (cited in the text as [19], the origin of Theorems 6.2 and the CGLP construction).
E. Balas, M. Perregaard, A precise correspondence between lift-and-project cuts, simple disjunctive cuts, and mixed integer Gomory cuts for 0-1 programming, Mathematical Programming 94 (2003) (cited in the text as [20], the origin of Corollary 6.3).

8 thms4 active users

Completed

Linear Optimization Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming V: Moving Between Conjunctive and Disjunctive Normal FormsTextbook

Motivation

Chapter 2 gives a compact lifted description of the closed convex hull of a disjunctive set once it is written as a union of polyhedra (its disjunctive normal form, DNF). But most discrete optimization problems present their feasible region the opposite way: as a conjunction of many small disjunctions (the conjunctive normal form, CNF) — "linear constraints, and $x_1 \in \{0,1\}$ , and $x_2 \in \{0,1\}$ , and so on" — each easy to reason about on its own but expensive to convert to DNF directly, since converting a CNF with $t$ conjuncts of $q_1,\dots,q_t$ terms each can blow the DNF up to as many as $q_1 \times \cdots \times q_t$ polyhedra. Chapter 4 develops the machinery for moving between these two extremes without paying that combinatorial cost all at once: the basic step, which merges two conjuncts into one, and the hull-relaxation, an intermediate polyhedral relaxation that tightens monotonically with every basic step performed, converging exactly to the true convex hull once the disjunctive set reaches DNF.

Setting

A disjunctive set is in regular form (RF) if $F = \bigcap_{j \in T} S_j$ with each $S_j = \bigcup_{i \in Q_j} P_i$ a union of polyhedra. $S_j$ is elementary if every $P_i$ is a halfspace (the RF is then the CNF), and improper if $S_j$ literally equals a single polyhedron $P_i$ . Writing $T^*$ for the improper indices, $P_0 := \bigcap_{j \in T^*} S_j$ is $F$ 's polyhedral part. The hull-relaxation of a regular form is

h\text{-}\mathrm{rel}(F) := \bigcap_{j \in T} \mathrm{cl}\,\mathrm{conv}(S_j),

a relaxation of $F$ distinct from $\mathrm{cl}\,\mathrm{conv}(F)$ itself: it convexifies each conjunct before intersecting, which is generally weaker. A basic step replaces two conjuncts $S_k, S_l$ ( $k \ne l$ ) of a regular form by their intersection $S_k \cap S_l$ (itself brought to DNF via distributivity), reducing the number of conjuncts by one; repeating this $|T|-1$ times brings any regular form to DNF. For a convex set $S$ , its extreme direction vectors are the extreme rays of its recession cone.

Formalization targets

Theorem 4.7 (goal) — the hull-relaxation hierarchy

For a sequence of regular forms $F_0, \dots, F_t$ of the same disjunctive set, with $F_0$ in CNF, $F_t$ in DNF, and each $F_i$ obtained from $F_{i-1}$ by a basic step:

P_0 = h\text{-}\mathrm{rel}(F_0) \supseteq h\text{-}\mathrm{rel}(F_1) \supseteq \cdots \supseteq h\text{-}\mathrm{rel}(F_t) = \mathrm{cl}\,\mathrm{conv}(F_t).

The chain of lemmas the goal is built from

Theorem 4.1 ( $S_k \cap S_l = \bigcup_{(i,j)}(P_i \cap P_j)$ , the basic-step identity), Theorem 4.4 (the hull of a union of halfspaces is $\mathbb{R}^n$ or the halfspace itself), Lemma 4.5 ( $h\text{-}\mathrm{rel}(F_0) = P_0$ for a CNF $F_0$ ), and Lemma 4.6 ( $\mathrm{cl}\,\mathrm{conv}(S_1 \cap S_2) \subseteq \mathrm{cl}\,\mathrm{conv}(S_1) \cap \mathrm{cl}\,\mathrm{conv}(S_2)$ , driving each inclusion of the chain).

The sharpening and payoff results

Theorem 4.8 (an exact extreme-point/extreme-direction criterion for when Lemma 4.6 is equality), Corollary 4.9 (a worked case where merging "0-1" disjunctions brings no gain), and Theorem 4.10 (any regular form is the projection of a mixed 0-1 program using no more binary variables than the original CNF).

Significance

The results themselves. Theorem 4.7 turns the exponential CNF-to-DNF blowup into a controllable, monotone process: rather than converting all at once, a solver can perform basic steps selectively — wherever Theorem 4.8's criterion promises a genuine tightening — and always have a valid, improving polyhedral relaxation available at every intermediate stage. Theorem 4.10 is what makes this practical for integer programming specifically: it shows the number of 0-1 variables needed never has to grow, no matter how many basic steps are performed, only the number of continuous lifted variables does.

Formalizing it. No object in this mission — regular form, the hull-relaxation operator, basic steps, or extreme direction vectors — exists on the platform prior to this mission or in Mathlib. This mission restates the disjunctive-set and convex-hull vocabulary of the earlier missions in this series locally (per the series convention that a draft mission cannot import another draft mission's definitions).

Difficulty

The obvious first attempt collapses h-rel to cl conv throughout, reasoning that since the chain ends at $\mathrm{cl}\,\mathrm{conv}(F_t)$ , the intermediate terms should behave the same way. This is exactly backwards: h-rel is always at least as large as the true convex hull at every intermediate stage (Lemma 4.6 gives containment, not equality, in general), and the chapter's own Example 1 exhibits a CNF whose hull-relaxation strictly exceeds $\mathrm{cl}\,\mathrm{conv}(F)$ until enough basic steps have been performed. The real difficulty Theorem 4.8 isolates is recognizing which basic steps actually tighten the relaxation: merging conjuncts whose extreme points and directions already coincide with those of the pairwise intersections gains nothing (Corollary 4.9's worked case), while merging conjuncts that interact more intricately can produce a strictly tighter bound — and no general rule beyond Theorem 4.8's own extreme-point criterion identifies which case holds.

Formalization scope

All results are stated over Fin n → ℝ with matrices Matrix (Fin m) (Fin n) ℝ. A regular form's conjuncts are represented as an arbitrary function T → Set (Fin n → ℝ) (rather than requiring every conjunct's internal polyhedral structure to be uniformly tracked through the whole chapter), with IsDisjunctiveUnion/IsElementaryDisjunction as existential well-formedness predicates asserting each conjunct genuinely is a union of polyhedra/halfspaces where that matters. IsBasicStepOf states a basic step abstractly via an index-type equivalence, since its mathematical content is which two conjuncts merge and into what, not any particular relabeling scheme; Theorem 4.7's own sequence of regular forms is a dependent family T : Fin (t+1) → Type* precisely because each basic step genuinely changes the index type (one fewer conjunct).

Theorem 4.7's three-part conclusion (initial equality, step-by-step containments, final equality) is stated as a conjunction rather than a single chained relation, since Lean has no native mixed equality/containment chain notation; this preserves the chapter's own warning that only the last hull-relaxation in the chain is asserted equal to the true convex hull. Theorem 4.10's index set $M_i$ (which term of each original disjunction a given conjunct's disjunct picked) is taken as given structural data satisfying the book's own defining relationship, matching the source's own treatment of $M_i$ as a named auxiliary index set rather than a from-scratch construction. Chapter 4's §4.5–4.6 (a machine-sequencing application with its own bespoke scheduling objects, Theorems 4.11–4.12) is out of scope for this mission — it introduces application-specific vocabulary not shared by the chapter's general hull-relaxation theory, not because it is difficult.

A trivializing formalization is ruled out explicitly: every theorem is stated for generic finite index types, never fixed at a small size that would collapse a union or intersection to a single term, and the chapter's own propositional-logic DNF/CNF conversion (informal narrative via truth tables in §1.3) is not itself a formalization target — this mission works entirely at the polyhedral-set level the chapter's own numbered results occupy.

Selected references

E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 4, §4.1–4.4.
V. Chvátal, Linear Programming, W. H. Freeman, 1983 (cited in the text as [12], the origin of Theorem 4.1's basic step).
E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998), 3–44 (the origin of the hull-relaxation hierarchy).

11 thms4 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming IV: Sequential Convexification of Disjunctive SetsTextbook

Motivation

Computing the convex hull of a disjunctive set — a union of finitely many polyhedra — is generally hard in direct proportion to how many polyhedra are in the union: Chapter 2's Theorem 2.1 gives a compact lifted description, but working with it still means reasoning about all the disjunctions of the program simultaneously. A natural question, with obvious practical consequences for integer and combinatorial optimization, is whether the convex hull can instead be built up incrementally: impose one disjunction, take the convex hull of what results, then impose the next disjunction on that, and so on. If this "sequential convexification" procedure always reached the true convex hull, computing facets of a hard disjunctive set would reduce to a sequence of much easier single-disjunction computations. Balas shows the answer is negative in general — a two-variable integer program is a standard counterexample — but identifies an important class of disjunctive programs, the facial ones, for which sequential convexification always works. This class includes 0-1 programming (pure or mixed), nonconvex quadratic programming, separable programming, and the linear complementarity problem, though not general integer programming.

Setting

Let $F_0 := \{x \in \mathbb{R}^n : Ax \ge b,\ x \ge 0\}$ . A disjunctive program in conjunctive normal form has constraint set

F := \Big\{x \in F_0 : \forall j \in S,\ \exists\, i \in Q_j,\ d_i x \ge d_{i0}\Big\},

for a finite set $S$ and, for each $j \in S$ , a finite set $Q_j$ of halfspace data $(d_i, d_{i0})_{i \in Q_j}$ — one elementary disjunction per $j \in S$ . The program is facial if every inequality $d_i x \ge d_{i0}$ appearing in some disjunction defines a face of $F_0$ , i.e. $F_0 \cap \{x : d_i x \ge d_{i0}\}$ is an extreme subset of $F_0$ for every such $i$ . Fixing an ordering $\sigma$ of $S$ , the sequential-convexification recursion sets $F_0$ (step zero) to be the base polyhedron and, for each subsequent step, imposes the next disjunction and reconvexifies: $F_{k+1} := \mathrm{conv}\big[\bigcup_{i \in Q_{\sigma(k)}} (F_k \cap \{x : d_i x \ge d_{i0}\})\big]$ .

For the necessity direction, write $D_j := \bigvee_{i \in Q_j}(d_i x \ge d_{i0})$ and, reversing every inequality, $\bar D_j := \bigvee_{i \in Q_j}(d_i x \le d_{i0})$ .

Formalization targets

Theorem 3.1 (goal) — faciality is sufficient

F \text{ facial} \implies F_{|S|} = \mathrm{conv}(F), \quad \text{for every ordering } \sigma \text{ of } S.

This is the weakest correct statement of the recursion's endpoint: it asserts the sequential procedure reaches exactly $\mathrm{conv}(F)$ (not, say, some fixed superset), and — since $\sigma$ is universally quantified — that this holds regardless of the order in which disjunctions are imposed.

Lemma 3.2 — the halfspace-intersection lemma

P \subseteq H^+ \implies H^- \cap \mathrm{conv}(P) = \mathrm{conv}(H^- \cap P),

for a union $P$ of finitely many polyhedra and opposite halfspaces $H^+, H^-$ .

Theorem 3.3 — the exact necessary-and-sufficient condition

\mathrm{conv}\big[(\mathrm{conv}\,F_{j-1}) \cap D_j\big] = \mathrm{conv}(F_{j-1} \cap D_j) \iff \text{the constraint boundary condition holds for } F_{j-1}, D_j.

Significance

The results themselves. Theorem 3.1 is what makes sequential convexification a practical tool rather than a theoretical curiosity: for a 0-1 program with $n$ binary variables, it lets the convex hull be built in $n$ stages, each requiring only the facets of a two-term disjunction — tractable, in contrast to generating facets of the full integer hull directly. Theorem 3.3 puts the boundary of applicability on rigorous footing: faciality is sufficient but not necessary, and Theorem 3.3 pins down the exact condition, showing precisely why sequential convexification is a genuinely restrictive property (holding for 0-1 programs but not general integer programs) rather than a universal fact about unions of polyhedra.

Formalizing it. No object in this mission — faciality, the sequential-convexification recursion, or the relative-boundary constraint condition — exists on the platform prior to this mission or in Mathlib. This mission restates the disjunctive-set vocabulary of the earlier missions in this series locally (per the series convention that a draft mission cannot import another draft mission's definitions) and is otherwise self-contained.

Difficulty

The natural first guess is that sequential convexification should always work, since at each step the procedure only discards points excluded by a valid disjunction. The book's own two-variable integer-programming example (imposing integrality on $x_1$ , then on $x_2$ ) refutes this directly: the resulting set strictly contains the true integer hull. The reason faciality repairs this is subtle and is exactly what Lemma 3.2 isolates: the recursion's correctness at each step needs the previous partial hull, intersected with the new disjunction's halfspace, to already equal the convex hull of the intersection taken before convexifying — and this commutation of convex hull and halfspace intersection is exactly what fails when the halfspace does not respect a face of the underlying polyhedron. Theorem 3.3 shows this is not merely Lemma 3.2's specific route to a sufficient condition, but the precise dividing line: the "if" direction says checking the boundary condition only for segments between two points already suffices, which is what makes facial sufficiency provable by induction in the first place.

Formalization scope

All results are stated over Fin n → ℝ with matrices Matrix (Fin m) (Fin n) ℝ. The disjunction structure uses a finite index type S with a dependent family of finite index types Qidx : S → Type*, matching the book's S, Q_j. Faciality (Facial) uses Mathlib's IsExtreme directly, matching the book's own primary definition of "defines a face" rather than its immediate "clearly equivalent" restatement (F₀ ⊆ {d_i x ≤ d_{i0}}). The relative boundary in Theorem 3.3 ("the boundary of $\bar D_j$ in the affine space spanned by $\bar D_j$ ") is Mathlib's intrinsicFrontier, the standard formalization of a set's boundary relative to its own affine hull. The book's own " $\in$ " in the constraint boundary condition's conclusion (rather than " $\subseteq$ ", which set-membership syntax would require for a set on the left) is read as set inclusion, the only mathematically sound reading, and is transcribed as ⊆ in the Lean statement while the milestone's verbatim text preserves the book's own " $\in$ " unchanged, per the verbatim-quotation convention.

A trivializing formalization is ruled out explicitly: Theorem 3.1 is stated for an arbitrary finite S and Qidx, not fixed at a small size (e.g. |S| = 1, which would make the recursion's endpoint trivially equal to a single step and prove nothing about sequencing), and the recursion's ordering σ is universally quantified rather than fixed to a canonical choice, matching the theorem's own order-independence claim.

Selected references

E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 3.
E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998), 3–44 (cited in the text as [6], the origin of Theorem 3.1).
R. Stubbs, S. Mehrotra, A branch-and-cut method for 0-1 mixed convex programming, Mathematical Programming 86 (1999), 515–532 (cited in the text as [116], extending sequential convexifiability to convex mixed 0-1 programs).

6 thms4 active usersReviewed

Completed

Convex Optimization Functional Analysis Operations Research·Captain: mikedeng1

Proximité et dualité dans un espace hilbertien II: Proximal Maps Are the Nonexpansive Subgradient Selections of Convex FunctionsResearch Paper

Motivation

The proximal map of a convex function is the basic building block of proximal-point, forward–backward, Douglas–Rachford and ADMM methods, which are used throughout large-scale convex optimization, signal processing and operator splitting. All of these methods treat $\operatorname{prox}_g$ as a nonexpansive operator and use the fact that it is a gradient. The questions this mission formalizes go back to the paper that introduced the map: J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), 273–299 (DOI 10.24033/bsmf.1625). Which maps $p : H \to H$ are proximal maps, and how can a function be recognized as the "potential" of one?

Moreau's answer (Corollaire 10.c) is intrinsic. A map is a proximal map exactly when it is nonexpansive and selects, at every point, a subgradient of some convex function. This characterization is the Hilbert-space origin of later results on firmly nonexpansive operators and on resolvents of maximal monotone operators (Minty 1962; Rockafellar 1970). It is still how one checks that a given nonexpansive operator is a proximal map.

Setting

Throughout, $H$ is a real Hilbert space with inner product $(x \mid y)$ and norm $\|x\|$ .

$\Gamma_0(H)$ is the class of functions $f : H \to \,]-\infty, +\infty]$ that are convex (convex epigraph), lower semicontinuous and not identically $+\infty$ .
The dual function of $f$ is $g(y) = \sup_{x \in H}[(x \mid y) - f(x)]$ . For $f \in \Gamma_0(H)$ , $g \in \Gamma_0(H)$ and $f$ is the dual of $g$ .
A vector $y$ is a subgradient of $\varphi$ at $z$ , written $y \in \partial\varphi(z)$ , when $\varphi(z)$ is finite and $\varphi(z) + (u - z \mid y) \le \varphi(u)$ for all $u$ . For $f \in \Gamma_0(H)$ this is the paper's condition $f(z) + g(y) = (z \mid y)$ , i.e. $z$ and $y$ are conjugate points.
For $f \in \Gamma_0(H)$ and $z \in H$ , the function $u \mapsto \tfrac12\|u - z\|^2 + f(u)$ has a unique minimizer, the proximal point $\operatorname{prox}_f z$ . A map $p : H \to H$ is a prox map when $p = \operatorname{prox}_g$ for some $g \in \Gamma_0(H)$ .
A multivalued map $z \mapsto Pz \subseteq H$ contracts distances when $x \in Pz$ , $x' \in Pz'$ imply $\|x - x'\| \le \|z - z'\|$ .
For dual functions $f, g$ , the primitive of $\operatorname{prox}_g$ is $\varphi(z) = \tfrac12\|\operatorname{prox}_g z\|^2 + f(\operatorname{prox}_f z)$ . With $\mathcal{Q}(z) = \tfrac12\|z\|^2$ , a function $\varphi$ is less convex than $\mathcal{Q}$ when $\varphi + \gamma = \mathcal{Q}$ for a convex $\gamma$ , and $\theta$ is more convex than $\mathcal{Q}$ when $\theta = \mathcal{Q} + \gamma$ for a convex $\gamma$ with values in $]-\infty, +\infty]$ .

The Lean names are GammaZero, conj, subgrad, IsProx, prox, IsProxMap, ContractsDistances, primitive, LessConvexThanQ, MoreConvexThanQ and IsProxPrimitive, all in the namespace MoreauProx.Characterization.

Formalization targets

Goal: Corollaire 10.c

For every map $p : H \to H$ ,

p \text{ is a prox map} \iff \Big(\|p(z) - p(z')\| \le \|z - z'\| \ \ \forall z, z'\Big) \ \wedge\ \exists \varphi \text{ convex},\ \forall z \in H,\ p(z) \in \partial\varphi(z).

Nothing is assumed of $\varphi$ beyond convexity.

Milestones, in the order of the paper

Proposition 3.a. For $f \in \Gamma_0(H)$ , $u \mapsto \tfrac12\|u - z\|^2 + f(u)$ has a strict minimum.
Proposition 4.a (Moreau decomposition). For $f \in \Gamma_0(H)$ with dual $g$ : $z = x + y$ and $f(x) + g(y) = (x \mid y)$ if and only if $x = \operatorname{prox}_f z$ and $y = \operatorname{prox}_g z$ .
(5.1). Conjugate pairs are monotone: $(x - x' \mid y - y') \ge 0$ .
Proposition 5.b. $\|\operatorname{prox}_f z - \operatorname{prox}_f z'\| \le \|z - z'\|$ , so $\operatorname{prox}_f$ is continuous.
Proposition 7.b. The primitive $\varphi$ of $\operatorname{prox}_g$ lies in $\Gamma_0(H)$ , and its dual is $g + \tfrac12\|\cdot\|^2$ .
Proposition 7.d. $\varphi$ is Fréchet differentiable with $\nabla\varphi(z) = \operatorname{prox}_g z$ .
Proposition 9.b. For $\varphi$ : ( $\varphi \in \Gamma_0(H)$ less convex than $\mathcal{Q}$ ) $\iff$ ( $\varphi \in \Gamma_0(H)$ with dual more convex than $\mathcal{Q}$ ) $\iff$ ( $\varphi$ is the primitive of a prox map).
Proposition 10.b. Each of these is equivalent to: $\varphi \in \Gamma_0(H)$ and $z \mapsto \partial\varphi(z)$ contracts distances.

Three further results of the paper are included as unmilestoned companions: Proposition 8.a ( $\operatorname{prox}_g = \operatorname{prox}_{g'}$ implies $g' = g + K$ ), Proposition 9.a ( $\mathcal{Q}$ is the only function equal to its dual) and Proposition 9.d (nonnegative combinations $\sum \alpha_i p_i$ of prox maps with $\sum \alpha_i \le 1$ are prox maps).

Significance

The result. Corollary 10.c turns "is a prox map" into two checkable properties of $p$ , one metric and one variational, with no need to exhibit $g$ . Proposition 9.d is one consequence: closure of prox maps under subconvex combinations. Proposition 10.b gives the dual picture, which recognizes primitives of prox maps among the functions of $\Gamma_0(H)$ by a Lipschitz condition on their subdifferential. The intermediate results are the standard toolkit of proximal analysis. They include the Moreau decomposition, the nonexpansiveness of $\operatorname{prox}_f$ , and the smoothness of the Moreau envelope $\varphi(z) = \inf_u[\tfrac12\|u - z\|^2 + f(u)]$ (Remark 7.c) with gradient $z - \operatorname{prox}_f z = \operatorname{prox}_g z$ .

Formalizing it. All statements were proved in 1965 and are textbook material (Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., 2017, Ch. 12–14 and 24). None of them has a machine-checked proof in Mathlib, which has no $\Gamma_0(H)$ class, no extended-valued Fenchel conjugate and no proximal map on a Hilbert space. A complete development here would give reusable infrastructure: the conjugate of extended-valued functions with the Fenchel–Moreau theorem, the proximal map and its nonexpansiveness, and the differentiability of the Moreau envelope. Downstream convergence proofs of proximal algorithms need this layer.

Difficulty

The necessity half of 10.c follows quickly from 5.b and 7.d once those are available. The sufficiency half is the hard one. Given only a nonexpansive $p$ and a convex $\varphi$ with $p(z) \in \partial\varphi(z)$ , one must produce $g \in \Gamma_0(H)$ with $p = \operatorname{prox}_g$ . The obvious move is to take $g$ to be something built from $\varphi$ directly. This fails because the candidate is only defined through a duality that needs $\varphi \in \Gamma_0(H)$ and a precise convexity comparison with $\mathcal{Q}$ . Neither is given, and neither follows from a pointwise argument. The intermediate milestones involve biconjugation of extended-valued functions, upper envelopes of affine functions in infinite dimension, and lower semicontinuity of functions taking $+\infty$ . These are the places where finite-dimensional or finite-valued shortcuts do not apply.

Formalization scope

Conventions committed to in Lean:

$H$ is [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]. Functions with values in $]-\infty, +\infty]$ are H → EReal.
$\Gamma_0(H)$ : never $-\infty$ , somewhere finite, convex epigraph in $H \times \mathbb{R}$ , lower semicontinuous in the norm topology. The paper defines $\Gamma_0(H)$ via upper envelopes of continuous affine functions and states this equivalent description on the same page.
The dual function is ⨆ x, (⟪x, y⟫ : EReal) - f x, computed in EReal (a complete lattice).
Subgradients use the affine-minorant form, which requires $\varphi(z)$ finite. It agrees with the paper's (2.4) on $\Gamma_0(H)$ and is meaningful for the merely convex $\varphi$ of the goal.
IsProx f z x says that $x$ minimizes $\tfrac12\|u - z\|^2 + f(u)$ . The function prox f picks such a minimizer by choice (junk value $0$ if none exists). Every theorem using prox assumes $f \in \Gamma_0(H)$ . A prox map is ∃ g, GammaZero g ∧ ∀ z, IsProx g z (p z).
The primitive is real-valued and built from the pair $(f, g)$ as in Définition 7.a. Theorems about it assume $f \in \Gamma_0(H)$ and $g$ equal to the dual of $f$ (the paper's "duales l'une de l'autre", which this implies).
In the goal, $\varphi$ is taken real-valued and convex (ConvexOn ℝ Set.univ). This is equivalent to the paper's $]-\infty, +\infty]$ -valued $\varphi$ , because a subgradient at every point forces $\varphi$ finite everywhere. The contraction condition is §10.a applied to $z \mapsto \{p(z)\}$ .
In 9.b and 10.b the auxiliary convex $\gamma$ may take $+\infty$ . Property (III) does not assume $\varphi \in \Gamma_0(H)$ .

Trivializing formalizations are ruled out. The goal's $\varphi$ is required to be convex and to have $p(z)$ as a genuine subgradient at every point, with $\varphi(z)$ finite. $\Gamma_0(H)$ excludes the constant $+\infty$ , under which every point would minimize the proximal objective. No theorem applies prox outside $\Gamma_0(H)$ , where its junk value would make statements vacuous.

Needed infrastructure: Fenchel–Moreau biconjugation for EReal-valued functions on a Hilbert space, existence of minimizers of coercive lsc convex functions (weak compactness of balls), and a Fréchet-derivative argument for the envelope. Contributions are welcome at every milestone. Also welcome are helper lemmas on EReal arithmetic for convex functions, and alternative proofs of 10.c via Minty's theorem on firmly nonexpansive maps.

Selected references

J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), 273–299. https://doi.org/10.24033/bsmf.1625
J.-J. Moreau, Fonctions convexes duales et points proximaux dans un espace hilbertien, C. R. Acad. Sci. Paris 255 (1962), 2897–2899.
G. J. Minty, Monotone (nonlinear) operators in Hilbert space, Duke Math. J. 29 (1962), 341–346. https://doi.org/10.1215/S0012-7094-62-02933-2
R. T. Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (1970), 209–216. https://doi.org/10.2140/pjm.1970.33.209
H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

12 thms4 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: Shuze Chen

Disjunctive Programming III: Projecting Polyhedra and the Convex Hull via PolarityTextbook

Motivation

Theorem 2.1 (the previous mission in this series) shows that the closed convex hull of a union of polyhedra has a compact description after lifting to a higher-dimensional space. That description comes in two dual flavors: a primal one, as the projection of an explicit lifted polyhedron, and a polar one, characterizing the hull's facets directly via a cone built from the disjuncts' own data. Both flavors matter in practice: a cutting-plane algorithm needs to know exactly which inequalities are facet-defining (so as not to waste effort generating redundant cuts), and the two routes — projection and polarity — offer complementary tools for deciding this. This mission formalizes both routes and the machinery connecting them, closing out Chapter 2 of Balas, Disjunctive Programming (Springer, 2018).

The projection route (§2.2–2.3) develops general facts about projecting an arbitrary polyhedron that predate and underlie the disjunctive-programming application: the classical projection formula via extreme rays of a projection cone, how dimension and facet structure behave under projection, and a refinement (via a coordinate transformation) that eliminates the redundant inequalities the plain projection formula can produce. The polarity route (§2.4) develops the reverse polar, an object introduced by Balas specifically for this purpose, whose iterated application recovers the closed convex hull of a disjunctive set directly, culminating in an exact characterization of when an inequality is facet-defining purely in terms of extreme rays of an explicit cone $W_0$ .

Setting

For a matrix system $(A,B,b)$ with $m$ rows, let $Q := \{(u,x) \in \mathbb{R}^p \times \mathbb{R}^q : Au+Bx \le b\}$ , and let $\mathrm{Proj}_x(Q) := \{x : \exists\, u,\ (u,x) \in Q\}$ be its projection onto the $x$ -space. The projection cone is $W := \{v : vA=0,\ v \ge 0\}$ . A vector $v$ is an extreme ray of a cone $W$ if $v \ne 0$ , $v \in W$ , and the ray it generates is an extreme subset of $W$ . The dimension $\dim(P)$ of a polyhedron is the dimension of its affine hull, and a set $F$ is a facet of $P$ if it is a proper face of $P$ of dimension $\dim(P)-1$ . Partitioning $(A,B,b)$ 's rows into those tight throughout $Q$ (the equality subsystem) and the rest, $r$ and $r^*$ denote the rank of the tight rows' combined and $A$ -only submatrices, respectively.

For $S \subseteq \mathbb{R}^n$ , the polar is $S^0 := \{x : xy \le 1\ \forall y \in S\}$ and the reverse polar is $S^\# := \{x : xy \ge 1\ \forall y \in S\}$ ; more generally the scaled polar at level $\alpha_0$ is $F_{(\alpha_0)} := \{y : xy \ge \alpha_0\ \forall x \in F\}$ . For a disjunctive set $F = \bigcup_{h \in Q} P_h$ with $P_h := \{x : A_h x \ge b_h\}$ and $Q^* := \{h : P_h \ne \emptyset\}$ , the cone $W_0 := \{(\alpha,\alpha_0) : \exists\, (u_h)_{h \in Q^*},\ \forall h,\ u_h A_h = \alpha,\ \alpha_0 \le u_h b_h,\ u_h \ge 0\}$ .

Formalization targets

Theorem 2.18 (goal) — facet characterization via polarity

For a full-dimensional disjunctive set $F$ ( $\dim(F)=n$ ) and $\alpha_0 \ne 0$ :

\alpha x \ge \alpha_0 \text{ defines a facet of } \mathrm{cl\,conv}(F) \iff (\alpha,\alpha_0) \text{ is an extreme ray of } W_0.

The polarity chain feeding the goal

Proposition 2.13 ( $0 \in \mathrm{cl\,conv}(S) \iff S^\# = \emptyset \iff S^\#$ bounded), Theorem 2.14 ( $S^{\#\#} = \mathrm{cl\,conv}(S) + \mathrm{cl\,cone}(S)$ when $0 \notin \mathrm{cl\,conv}(S)$ ), Corollary 2.15 ( $\mathrm{cl\,conv}(S) = S^{00} \cap S^{\#\#}$ ), Theorem 2.16 (the scaled polar stabilizes: $F_{(\alpha_0)}^{\#\#\#} = F_{(\alpha_0)}^{\#}$ ), and Corollary 2.17 ( $F_{(\alpha_0)} = \{\alpha : (\alpha,\alpha_0) \in W_0\}$ ) — each the weakest statement needed for the next.

The projection track (independent of the goal's direct proof, sharing its definitions)

Theorem 2.5 ( $\mathrm{Proj}_x(Q) = \{x : (vB)x \le vb,\ v \in \mathrm{extr}(W)\}$ ), Proposition 2.6 (projection preserves integrality), Theorem 2.7 ( $\dim(\mathrm{Proj}_x(Q)) = \dim(Q)-p+r^*$ ), Corollaries 2.8–2.10 (facet/face behavior under projection), and Proposition 2.11 / Corollary 2.12 (sharper facet characterizations via a coordinate-transformed projection cone).

Significance

The results themselves. Theorem 2.18 is the practical payoff of the entire polarity apparatus: it turns "is this inequality facet-defining for the convex hull of a union of polyhedra" from a geometric question into an algebraic one about extreme rays of an explicit, finitely-generated cone built directly from the disjuncts' own constraint data — exactly the kind of question a cutting-plane algorithm needs answered to avoid generating redundant cuts. The projection track is foundational general polyhedral theory in its own right (Theorem 2.5's formula underlies Benders decomposition and classical Fourier-Motzkin elimination as special cases, per the book's own remarks), independently useful beyond the disjunctive setting.

Formalizing it. No object in this mission — polars, reverse polars, projection cones, extreme rays of a cone, or the dimension/facet apparatus of a polyhedron — exists on the platform prior to this mission or in Mathlib (a q=polar search returns only an unrelated cyclic-polytope construction from the Hirsch-conjecture series, with different conventions and object). This mission restates the disjunctive-set vocabulary of the companion ConvexHull mission locally (per the series convention that a draft mission cannot import another draft mission's definitions) and builds the polarity apparatus from scratch on top of it.

Difficulty

The natural first attempt at Theorem 2.18 tries to characterize facets of $\mathrm{cl\,conv}(F)$ directly from the lifted-polyhedron representation of Theorem 2.1, projecting facet by facet. This misses the point of the polarity route entirely: Theorem 2.18's proof instead goes through $F_{(\alpha_0)}$ , showing a vertex of $F_{(\alpha_0)}$ corresponds to a nonhomogeneous subset of rank $n$ of $F_{(\alpha_0)}$ 's own defining system being tight — algebra entirely in the dual space of multipliers, never touching the lifted polyhedron's facets directly. The two obstacles Theorem 2.14 and Proposition 2.13 exist to clear are, respectively: reverse polars do not satisfy the ordinary polar's clean involution property (an extra $\mathrm{cl\,cone}(S)$ summand appears, capturing recession directions the reverse-polar construction alone cannot see), and reverse polars are either empty or automatically unbounded (never merely "small"), which is why the apparatus needs the normalization $0 \notin \mathrm{cl\,conv}(F)$ throughout.

Formalization scope

All results are stated over finite index sets and matrices Matrix (Fin (m h)) (Fin n) ℝ (disjunctive-set data, m : Q → ℕ dependent) or Matrix (Fin m) (Fin p) ℝ / Matrix (Fin m) (Fin q) ℝ (projection-track data). PolyDim and IsFacet are stated generically over any real vector space (via Module.finrank of vectorSpan and Mathlib's IsExtreme), so the same definitions serve both Poly2-shaped pairs and cl conv F ⊆ Fin n → ℝ directly in Theorem 2.18. IsExtremeRay is likewise stated generically, reused for cones in plain vector space, (v,v0)-space, and the triple (v,w,v0)-space Proposition 2.11 needs.

Two results (Proposition 2.11, Corollary 2.12) build on a coordinate-transformed polyhedron Q̃/cone W̃ that the book itself only cites from [14] rather than constructing; consistent with the book's own treatment, this mission takes W̃ (or its (v,v0)-projection) as given data together with its defining relationship to Proj_x(Q), rather than re-deriving the transformation — a choice recorded in MODERATION_NOTES.md, not a weakening of either statement's content. Proposition 2.11's complexity remark ("O(max{m,q}³)") is a proof aside about the transformation's cost, not part of either result's mathematical claim, and is out of scope per the book-wide disposition (triage.json).

A trivializing formalization is ruled out explicitly: the projection-track results are stated for generic m, p, q, never fixed at small values, and Theorem 2.18 is stated for a generic finite disjunctive index set Q, not specialized to |Q| = 1 (which would collapse W_0 to ordinary LP polarity and prove nothing about unions).

Selected references

E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 2, §2.2–2.4.
E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998), 3–44 (cited in the text as [6], the origin of the reverse-polar apparatus alongside [10]).
Balas, Pordli (cited as [14] in the text) — the coordinate-transformation construction behind Proposition 2.11 and Corollary 2.12.
Balas, Portugal (cited as [30] in the text) — the source of the dimensional results of §2.2.2.

19 thms4 active users

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

Adversarially Robust Generalization Requires More Data 1: A Robust-Error Lower Bound in the Gaussian ModelResearch Paper

Motivation

Classifiers trained to high standard accuracy on image benchmarks can be made to fail by perturbations of the input that are small in the $\ell_\infty$ norm (Szegedy et al., 2014; Goodfellow et al., 2015). Adversarial training reaches high robust accuracy on the training set, but on CIFAR10 the robust accuracy on held-out data is much lower than on the training set (Madry et al., 2018). That is, robust generalization fails.

Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285) ask whether this is a statistical phenomenon: does learning a robust classifier need more samples than learning an accurate one, even in the simplest distributional model? This mission formalizes their answer for a mixture of two Gaussians. In that model, with $\|\theta^\star\|_2 = \sqrt d$ and $\sigma \le c\, d^{1/4}$ , a single sample suffices for standard generalization (their Theorem 4). Robust generalization, by contrast, needs a number of samples that grows polynomially with the dimension, for every learning algorithm.

Setting

Write $\mathbb R^d$ for the feature space and $\{\pm 1\}$ for the labels.

The $\ell_\infty$ perturbation set of radius $\varepsilon$ around $x$ is $\mathcal B_\infty^\varepsilon(x) = \{x' \in \mathbb R^d : \|x' - x\|_\infty \le \varepsilon\}$ .
For $\theta \in \mathbb R^d$ and $\sigma > 0$ , the $(\theta, \sigma)$ -Gaussian model $P_{\theta,\sigma}$ is the law of $(x, y)$ obtained by drawing $y$ uniformly from $\{\pm1\}$ and then $x \sim \mathcal N(y\theta, \sigma^2 I)$ (Definition 1). Here $\sigma$ is a standard deviation.
The $\ell_\infty^\varepsilon$ -robust classification error of a classifier $f : \mathbb R^d \to \{\pm1\}$ under a distribution $P$ is $\mathbb P_{(x,y) \sim P}[\exists\, x' \in \mathcal B_\infty^\varepsilon(x) : f(x') \ne y]$ (Definitions 2–3). With $\varepsilon = 0$ it is the ordinary classification error.
A learning algorithm $g_n$ maps $n$ labelled samples $S \in (\mathbb R^d \times \{\pm 1\})^n$ to a classifier $f_n = g_n(S)$ .
The expected robust error $\Xi$ of $g_n$ is the robust error of $g_n(S)$ under $P_{\theta,\sigma}$ , averaged over $S \sim P_{\theta,\sigma}^{\otimes n}$ and then over a prior $\theta \sim \mathcal N(0, I)$ . The learner sees $S$ but not $\theta$ .

Formalization targets

Goal: Corollary 23 (p. 30)

For every learning algorithm $g_n$ , every $\sigma > 0$ and every $\varepsilon \ge 0$ ,

n \le \frac{\varepsilon^2\sigma^2}{8\log d} \quad\Longrightarrow\quad \Xi \ \ge\ \Big(1 - \frac1d\Big)\frac12 .

Theorem 11 (p. 28)

For every learning algorithm $g_n$ , every $\sigma > 0$ and every $\varepsilon \ge 0$ ,

\Xi \ \ge\ \frac12\, \mathbb P_{v \sim \mathcal N(0, I)}\Big[\sqrt{\tfrac{n}{\sigma^2+n}}\,\|v\|_\infty \le \varepsilon\Big].

Intermediate statements (milestones)

Eq. (2). Given $n$ samples $z_i \sim \mathcal N(\theta, \sigma^2 I)$ , the posterior of $\theta \sim \mathcal N(0, I)$ is $\mathcal N(\mu', \Sigma')$ with $\mu' = (\sigma^2+n)^{-1}\sum_i z_i$ and $\Sigma' = \frac{\sigma^2}{\sigma^2+n} I$ . The expectations over $\theta$ and over the samples may therefore be exchanged.
Eq. (3). Averaging $P_{\theta,\sigma}$ over $\theta \sim \mathcal N(m, s^2 I)$ gives $P_{m, \sqrt{s^2+\sigma^2}}$ .
The bound on $\Psi$ . If $\|m\|_\infty \le \varepsilon$ , every classifier has $\ell_\infty^\varepsilon$ -robust error at least $\frac12$ under $P_{m,s}$ .
The law of $\bar z$ . The sample mean $\bar z$ of the $z_i$ is marginally $\mathcal N(0, (1+\sigma^2/n) I)$ .
Maximum of $d$ Gaussians. $\mathbb P_{v\sim\mathcal N(0,I_d)}[\|v\|_\infty \le 2\sqrt{2\log d}] \ge 1 - 1/d$ .

Corollary 23 is the goal because it is the statement the paper advertises: its main-text Theorem 6 is Corollary 23 with $\sigma = c_1 d^{1/4}$ .

Significance

In the same model with $\|\theta^\star\|_2 = \sqrt d$ and $\sigma$ of order $d^{1/4}$ , a single sample suffices to reach standard error below 1% (Theorem 4 of the paper), and on the order of $\varepsilon^2\sqrt d$ samples suffice for robust error below 1% when $\varepsilon$ is below a small constant (Theorem 5; Corollary 22, formalized in mission 3 of this series). Corollary 23 shows that, up to the logarithmic factor, no learner can do better. Robust generalization then needs $\varepsilon^2 \sqrt d / \log d$ times as many samples as standard generalization. The gap is information-theoretic: it concerns every algorithm, not a particular training procedure or model class. The authors present this as a candidate explanation for the robust-generalization gap observed on CIFAR10. The ½ is tight: a constant classifier attains it.

The paper's proof is complete and short. As far as a search of the platform shows, none of its statements has been formalized. A machine-checked version requires multivariate Gaussian conjugacy, Gaussian convolution identities, the outer-measure robust event, and a union bound for the maximum of Gaussians. The Gaussian conjugacy and convolution facts are standard and appear throughout Bayesian statistics. As of this Mathlib version they are not available for stdGaussian on EuclideanSpace.

Difficulty

The obvious attempt fixes $\theta$ and bounds the robust error for each $\theta$ . That fails: a learner may ignore the data and output the Bayes-optimal robust classifier for one fixed $\theta$ , so for each $\theta$ some learner does well. The lower bound holds only on average over the prior on $\theta$ . The classifier $f_n$ depends on the samples, and the samples depend on $\theta$ , so the classifier and the test distribution are correlated through $\theta$ . A second obstacle is measure-theoretic. The robust error of a classifier is the probability of an $\ell_\infty$ -thickening of an arbitrary set $\{f \ne y\}$ . Such a set need not be Borel, and it must be bounded below with no structure on the classifier beyond what the learner provides. The same statement with the $\ell_2$ ball is a different theorem.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra; $\mathcal N(0, I)$ is Mathlib's stdGaussian; $\mathcal N(m, s^2 I)$ is its image under $v \mapsto m + s v$ , so every Gaussian parameter in the development is a standard deviation.
The $\ell_\infty$ ball is written coordinatewise ( $|x'_i - x_i| \le \varepsilon$ for all $i$ ), because the ambient norm is $\ell_2$ . $\|v\|_\infty \le r$ is written the same way.
Labels are Bool, with true for $+1$ . A classifier is ℝ^d → Bool, and a learning algorithm is (Fin n → ℝ^d × Bool) → ℝ^d → Bool.
A model is a measure on $\mathbb R^d \times$ Bool; $n$ samples form the product measure Measure.pi.
The robust event need not be Borel. Its probability is the outer measure, which is its probability under the completion. The expectations are lower Lebesgue integrals.
Theorem 11 and Corollary 23 assume the learner is jointly measurable in (samples, input). This is the only condition on it. $\log$ is the natural logarithm. With Lean's conventions $\log 0 = \log 1 = 0$ and $x/0 = 0$ , the goal's hypothesis forces $n = 0$ for $d \le 1$ , where the statement is still true.
The paper writes the posterior mean as $\frac{n}{\sigma^2+n}\bar z$ , with " $\bar z = \sum_i z_i$ " on p. 28. The formalization uses $(\sigma^2+n)^{-1}\sum_i z_i$ , which is the posterior mean. It agrees with the paper when $\bar z$ is read as the sample mean, as it is on p. 30.

A formalization that fixes $\theta$ instead of averaging over the prior, that restricts the learner (to linear classifiers, or to classifiers that do not depend on the data), that uses the $\ell_2$ ball, or that assumes the posterior formula as a hypothesis states a different theorem. These are ruled out by the definitions file.

Needed infrastructure: the multivariate Gaussian conjugacy and convolution identities for stdGaussian pushforwards, translation invariance of outer measure under Gaussian shifts, and a sub-Gaussian tail bound for one coordinate. The Gaussian identities are reusable well beyond this mission. Contributions of general Gaussian lemmas, stated for stdGaussian on any finite-dimensional inner product space, are welcome. Related platform work: missions 2–4 of this series formalize the Bernoulli-model lower bound and the two upper bounds of the same paper.

Selected references

L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, NeurIPS 2018; arXiv:1804.11285v2, 2018. https://arxiv.org/abs/1804.11285
A. Madry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, R. Fergus, Intriguing properties of neural networks, ICLR 2014. https://arxiv.org/abs/1312.6199
I. Goodfellow, J. Shlens, C. Szegedy, Explaining and Harnessing Adversarial Examples, ICLR 2015. https://arxiv.org/abs/1412.6572
S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013 (Theorem 5.8). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

8 thms4 active usersReviewed

Completed

Convex Optimization Functional Analysis Operations Research·Captain: mikedeng1

Proximité et dualité dans un espace hilbertien I: Moreau's Decomposition into Proximal Points of a Function and Its DualResearch Paper

Motivation

Proximal maps are the basic building block of first-order methods for nonsmooth convex optimization: the proximal point algorithm, forward–backward splitting (ISTA/FISTA), Douglas–Rachford splitting and ADMM all proceed by evaluating maps of the form $z \mapsto \operatorname{argmin}_u \big[\tfrac12\|u - z\|^2 + f(u)\big]$ . The notion and its name come from J.-J. Moreau, who introduced proximal points in two 1962 notes in the Comptes rendus and gave the systematic theory in Proximité et dualité dans un espace hilbertien (Bull. Soc. Math. France 93 (1965), 273–299).

The central result of that paper, which Moreau calls the key proposition, links proximal maps to conjugate duality: every point of a Hilbert space splits uniquely into the proximal point of $z$ relative to a convex function plus the proximal point relative to its dual function. The identity $z = \mathrm{prox}_f z + \mathrm{prox}_{f^*} z$ is used throughout modern optimization, for example to compute the proximal map of a norm from the projection onto the dual-norm ball, and in the analysis of primal–dual splitting methods.

Timeline. Moreau (1962) announces proximal points and the decomposition along mutually polar cones. Moreau (1965) proves the general decomposition theorem for $\Gamma_0(H)$ and derives from it the characterization of proximal maps and the maximal monotonicity of subdifferentials in Hilbert space. Rockafellar (Pacific J. Math. 33 (1970)) extends maximal monotonicity of subdifferentials to Banach spaces.

Setting

Let $H$ be a real Hilbert space with inner product $(x \mid y)$ and norm $\|x\|$ . Functions take values in the extended real line $[-\infty, +\infty]$ .

The class $\Gamma_0(H)$ consists of the functions $f : H \to\ ]-\infty, +\infty]$ that are convex (their epigraph $\{(x, r) : f(x) \le r\}$ is convex in $H \times \mathbb R$ ), lower semicontinuous, and not identically $+\infty$ .

The dual function of $f$ is

f^{*}(y) = \sup_{x \in H}\,\big[(x \mid y) - f(x)\big].

Two points $x$ and $y$ are conjugate with respect to $f$ and $g = f^*$ when $f(x) + g(y) = (x \mid y)$ ; the set of such $y$ is the subdifferential $\partial f(x)$ .

For $f \in \Gamma_0(H)$ and $z \in H$ , the proximal point $\mathrm{prox}_f z$ is the unique minimizer of

\Phi(u) = \tfrac12\|u - z\|^2 + f(u).

When $f$ is the indicator function of a nonempty closed convex set $C$ (zero on $C$ , $+\infty$ outside), $\mathrm{prox}_f z$ is the nearest-point projection $\mathrm{proj}_C z$ .

Formalization targets

Goal: Proposition 4.a (Moreau's decomposition)

Let $f \in \Gamma_0(H)$ and $g = f^*$ . For all $x, y, z \in H$ ,

\Big(z = x + y \ \text{ and } \ f(x) + g(y) = (x \mid y)\Big) \iff \Big(x = \mathrm{prox}_f z \ \text{ and } \ y = \mathrm{prox}_g z\Big).

Milestones

(2.3), the Fenchel–Young inequality: $f(x) + f^*(y) \ge (x \mid y)$ for all $x, y$ .
§2.b, biconjugation: $f^* \in \Gamma_0(H)$ and $f^{**} = f$ for $f \in \Gamma_0(H)$ .
Proposition 3.a: $\Phi(u) = \tfrac12\|u - z\|^2 + f(u)$ has a strict minimum, so $\mathrm{prox}_f z$ is well defined.

Companions

Corollaire 4.b: for a closed convex cone $P$ and its polar cone $Q = \{y : (x \mid y) \le 0\ \forall x \in P\}$ , $z = x + y$ with $x \in P$ , $y \in Q$ , $(x \mid y) = 0$ iff $x = \mathrm{proj}_P z$ and $y = \mathrm{proj}_Q z$ .
(5.1): the conjugacy relation is monotone, $(x - x' \mid y - y') \ge 0$ .
Proposition 12.b: the relation $y \in \partial f(x)$ is maximal monotone.

Significance

The decomposition theorem gives, for every $z$ , a unique splitting into a pair of conjugate points, and conversely identifies every conjugate pair summing to $z$ with the two proximal points. Special cases are the orthogonal decomposition along a closed subspace and its complement, and the decomposition along a pair of mutually polar cones (Corollaire 4.b). In the rest of Moreau's paper it yields that proximal maps are nonexpansive, that the Moreau envelopes of $f$ and $f^*$ add up to $\tfrac12\|z\|^2$ , and that the subdifferential of a function in $\Gamma_0(H)$ is maximal monotone (Proposition 12.b). In algorithms it lets one evaluate $\mathrm{prox}_{f^*}$ from $\mathrm{prox}_f$ at no extra cost, which is the basis of dual and primal–dual proximal methods.

All results in this mission are classical and proved (Moreau 1965; see also Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., 2017, Thm. 14.3). What the mission adds is a machine-checked development. Mathlib contains convex functions, lower semicontinuity and Hilbert-space projections onto closed convex sets, but as of this mission's environment it has no Legendre–Fenchel conjugate for extended-valued functions on a Hilbert space, no proximal map and no maximal monotone operators. The Hilbert projection theorem is on the platform as FamousTheorems.hilbert_projection_theorem; it is the special case of Proposition 3.a for indicator functions.

Difficulty

The two directions of the goal are unequal. That conjugate points summing to $z$ are the two proximal points needs only the definition of the dual function. The converse must produce the conjugacy identity $f(x) + f^*(z - x) = (x \mid z - x)$ from the bare fact that $x$ minimizes $\tfrac12\|u - z\|^2 + f(u)$ , and a pointwise first-order argument is unavailable because $f$ need be neither finite nor differentiable anywhere.

The milestones carry the analytic weight. Proposition 3.a needs existence of a minimizer of a function that is neither continuous nor coercive by itself on an infinite-dimensional space, so compactness arguments in the norm topology fail. Biconjugation (§2.b) is the Fenchel–Moreau theorem, which requires a separation theorem in $H \times \mathbb R$ applied to a closed convex epigraph whose values may be $+\infty$ .

Formalization scope

Everything lives in the namespace MoreauProx.Decomposition, over {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]; the paper's $(x \mid y)$ is ⟪x, y⟫_ℝ. The following conventions are committed to:

Functions are H → EReal. $\Gamma_0(H)$ (GammaZero) is the structure: never ⊥, not everywhere ⊤, convex epigraph in H × ℝ, and LowerSemicontinuous in the norm topology. The paper defines $\Gamma_0(H)$ as suprema of nonempty families of continuous affine functions, other than $+\infty$ , and states the equivalence with this description (§2.a); the second description is the one formalized. Weak and strong lower semicontinuity agree for convex functions, as the paper remarks, so no weak topology appears.
The dual function is conj f y = ⨆ x, ⟪x, y⟫_ℝ - f x in EReal; since a - ⊤ = ⊥, this matches both lines of (2.2).
" $x = \mathrm{prox}_f z$ " is the predicate IsProx f z x: $x$ minimizes proxObjective f z u = ‖u - z‖ ^ 2 / 2 + f u. With Proposition 3.a it is equivalent to the paper's notation; no choice function is used.
The goal assumes GammaZero f and g = conj f; the paper's " $f, g \in \Gamma_0(H)$ dual to each other" follows from this by §2.b, so the goal is not weaker than the paper's.
The polar cone uses $\le 0$ (the negative of Mathlib's innerDual), and $\mathrm{proj}_C z$ is the predicate IsProj C z x (nearest point).
Maximal monotonicity is the paper's definition: monotone, and contained in no strictly larger monotone relation.

A formalization that drops the requirement that $f$ be not identically $+\infty$ , drops the factor $\tfrac12$ , replaces the duality hypothesis by unrelated $f, g$ , or reads values through EReal.toReal would make the statement false or vacuous; the definitions above rule these out.

Contributions welcome: proofs of the three milestones and of the goal; reusable infrastructure for extended-valued convex analysis on Hilbert spaces (conjugates, subdifferentials, proximal maps), which the companion mission Proximité et dualité dans un espace hilbertien II builds on.

Selected references

J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), 273–299. https://doi.org/10.24033/bsmf.1625
J.-J. Moreau, Fonctions convexes duales et points proximaux dans un espace hilbertien, C. R. Acad. Sci. Paris 255 (1962), 2897–2899.
R. T. Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (1970), 209–216. https://doi.org/10.2140/pjm.1970.33.209
H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

7 thms4 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

A Branch and Bound Algorithm for the Generalized Assignment Problem: The Knapsack Penalty Bound Equals the Lagrangean Bound at Second-Smallest CostsResearch Paper

Motivation

The generalized assignment problem (GAP) asks for the cheapest way to give each of $n$ tasks to exactly one of $m$ agents when every agent has a limited amount of a resource and different agents consume different amounts of it for the same task. It models assigning jobs to machines or computers, software tasks to programmers, commercials to time slots, and customers to single-source plants in capacitated facility location. The problem is NP-hard, so exact methods rely on lower bounds that are cheap to compute and strong enough to prune a branch and bound tree.

G. Terry Ross and Richard M. Soland (Mathematical Programming 8, 1975) gave such a bound. The relaxation that ignores the resource limits is solved by giving every task to its cheapest agent; the overloaded agents are then repaired by one small binary knapsack problem each, whose optimal values are added as penalties. Their paper then shows that this repaired bound is not an ad hoc heuristic: it is exactly the value of a Lagrangean relaxation of the GAP at an explicit choice of multipliers. This identity made the Ross–Soland bound the reference point for the later Lagrangean and column-generation methods for the GAP (for example Fisher, Jaikumar and Van Wassenhove, Management Science 1986 and Savelsbergh, Operations Research 1997).

Setting

Agents are $I=\{1,\dots,m\}$ and tasks $J=\{1,\dots,n\}$ . Giving task $j$ to agent $i$ costs $c_{ij}$ and uses $r_{ij}\ge 0$ units of agent $i$ 's resource; agent $i$ has $b_i>0$ units. The problem is

\text{(P)}\qquad \min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}x_{ij}\le b_i\ (i\in I),\quad\sum_{i\in I}x_{ij}=1\ (j\in J),\quad x_{ij}\in\{0,1\}.

Dropping the resource constraints gives the relaxation (PR). It is solved by choosing, for each task $j$ , a cheapest agent $i_j$ with $c_{i_jj}=\min_{i}c_{ij}$ and setting $x_{i_jj}=1$ ; its value is $Z=\sum_jc_{i_jj}$ . Let $J_i=\{j: i_j=i\}$ be the tasks this solution gives to agent $i$ , $I'=\{i:\sum_{j\in J_i}r_{ij}>b_i\}$ the overloaded agents, and $d_i=\sum_{j\in J_i}r_{ij}-b_i$ the excess of agent $i$ . The penalty of moving task $j$ away from $i_j$ is $p_j=\min_{k\ne i_j}(c_{kj}-c_{i_jj})$ . For $i\in I'$ the binary knapsack problem

\text{(PK}_i)\qquad\min\ z_i=\sum_{j\in J_i}p_jy_{ij}\quad\text{s.t.}\quad\sum_{j\in J_i}r_{ij}y_{ij}\ge d_i,\quad y_{ij}\in\{0,1\}

chooses the cheapest set of tasks to move off agent $i$ ; call its optimal value $z^*_i$ . The knapsack bound is

\mathrm{LB}=Z+\sum_{i\in I'}z^*_i .

Dualizing the assignment constraints with multipliers $\lambda_j$ gives the Lagrangean relaxation

\text{(PR}_\lambda)\qquad\min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}+\sum_{j\in J}\lambda_j\Bigl(1-\sum_{i\in I}x_{ij}\Bigr)\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}x_{ij}\le b_i\ (i\in I),\quad x_{ij}\in\{0,1\}.

Finally $c_{1j}$ and $c_{2j}$ are the smallest and second smallest of $c_{1j},\dots,c_{mj}$ , counted with multiplicity.

Formalization targets

Goal: the knapsack bound is the Lagrangean bound at $\lambda=c_2$

For every cheapest-agent choice $j\mapsto i_j$ and every choice of optimal knapsack solutions,

\mathrm{LB}=\min\Bigl\{\sum_{i}\sum_{j}c_{ij}x_{ij}+\sum_{j}c_{2j}\Bigl(1-\sum_{i}x_{ij}\Bigr)\ :\ x\ \text{feasible for (PR}_\lambda)\Bigr\},

the minimum being attained, and consequently $\mathrm{LB}\le\sum_i\sum_jc_{ij}x_{ij}$ for every $x$ feasible for (P). This is the paper's "principal result of this Lagrangean analysis" (§2, p. 96). It has no constants to improve; it is an identity between two optimization problems.

Milestones

In the paper's order of use: (PR) is solved by the cheapest agents (pp. 93–94); every lower bound on (PR $_\lambda$ ) is a lower bound on (P) (p. 95); (PR $_\lambda$ ) separates into one binary knapsack per agent (p. 95); at $\lambda=c_2$ the variables that are zero in the (PR) solution can be fixed at zero, the substitution $y_{ij}=1-x_{ij}$ turns agent $i$ 's part into (PK $_i$ ), $p_j=c_{2j}-c_{1j}$ , and agent $i$ 's part has value $-\sum_{j\in J_i}p_j+z^*_i$ (p. 96). Two side results close the section: the solution obtained by moving the tasks the knapsacks select has cost exactly LB, so it is optimal whenever it is feasible (pp. 94–95); and the optimal dual multipliers of the bounded-variable linear program (PR $_L$ ) are exactly the vectors with $c_{1j}\le\lambda_j\le c_{2j}$ (pp. 95–96).

Significance

The identity says that a bound computed from one sorting pass and a handful of small knapsacks equals a Lagrangean dual bound at a closed-form multiplier. Validity of LB for (P) then follows from weak Lagrangean duality alone, and the multiplier $c_2$ is the upper end of the range of optimal dual multipliers of the linear program (PR $_L$ ), which the paper singles out as a suitable choice of multipliers. The rebuilt solution gives the algorithm a feasible incumbent at no extra cost whenever the knapsack repairs happen to respect all budgets.

The result is proved in the paper, in one sentence. The mission turns that sentence into checked statements: the separation of (PR $_\lambda$ ), the reduction of each agent's subproblem to (PK $_i$ ), the handling of ties among cheapest agents, and the role of nonnegative resources. As far as a search of the platform shows, nothing about the generalized assignment problem or its Lagrangean bounds has been formalized; the definitions here (assignment relaxations, per-agent knapsacks, bounded-variable duals) are reusable for other GAP and facility-location missions.

Difficulty

The Lagrangean relaxation at $\lambda=c_2$ is a larger problem than the knapsack bound suggests: a feasible $x$ may give a task to several agents or to none, and may use any agent, not only the cheapest one. The knapsack bound, by contrast, only looks at the tasks each agent receives in the (PR) solution. The paper bridges the two in one sentence of three observations, and each observation depends on a condition the sentence does not state: the sign of the resource coefficients, the treatment of agents that are not overloaded (for which no knapsack is solved), and ties among cheapest agents, which make some penalties zero and require the statement to hold for every tie-break. An inequality in one direction only (LB is a valid bound) is not the claim; the equality needs a feasible point of (PR $_\lambda$ ) whose value is exactly LB.

Formalization scope

Agents are Fin m and tasks Fin n, indexed from 0. Costs, resources, budgets, multipliers and variables are real numbers; a 0-1 variable is a real equal to 0 or 1, so the paper's sums are literal. The cheapest-agent selection is an arbitrary function a : Fin n → Fin m with IsCheapest c a, so every statement holds for every tie-break. $p_j$ and $c_{2j}$ are minima over the other agents, which requires $m\ge2$ (hm : 1 < m); $c_{2j}$ is proved to be the second smallest cost with multiplicity. Optimal values are never encoded as sInf: $z^*_i$ is the objective of a given optimal knapsack solution, and "the bound provided by (PR $_\lambda$ )" is stated as a lower bound over all feasible points that is attained.

Standing hypotheses: $b_i>0$ (printed on p. 92), $r_{ij}\ge0$ (implicit in "the resource required", and necessary: with a negative $r_{ij}$ both (PR $_\lambda$ ) and (P) can fall below LB), and $m\ge2$ . All costs are finite; the "not permissible" pairs of the paper's numerical example are outside the model.

A formalization that states only $\mathrm{LB}\le$ every (PR $_\lambda$ ) value, or that restricts the (PR $_\lambda$ ) competitors to the (PR) support or to at most one agent per task, would be a weaker theorem and does not meet the goal. The (PR $_L$ ) dual is written out explicitly with multipliers $u_{ij}\ge0$ for the bounds $x_{ij}\le1$ ; "each optimal dual multiplier lies anywhere in the range $c_{1j}\le\lambda_j\le c_{2j}$ " is read as "the optimal multipliers are exactly this box".

Needed infrastructure is only finite sums over Fin and Finset.inf'. Proofs of the milestones, and lemmas on separable binary programs that could serve other Lagrangean-relaxation missions, are welcome.

Selected references

G. T. Ross and R. M. Soland, A branch and bound algorithm for the generalized assignment problem, Mathematical Programming 8 (1975) 91–103. https://doi.org/10.1007/BF01580430
A. M. Geoffrion, Lagrangean relaxation for integer programming, Mathematical Programming Study 2 (1974) 82–114. https://doi.org/10.1007/BFb0120690
M. L. Fisher, R. Jaikumar and L. N. Van Wassenhove, A multiplier adjustment method for the generalized assignment problem, Management Science 32 (1986) 1095–1103. https://doi.org/10.1287/mnsc.32.9.1095
M. Savelsbergh, A branch-and-price algorithm for the generalized assignment problem, Operations Research 45 (1997) 831–841. https://doi.org/10.1287/opre.45.6.831

10 thms4 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+1·Captain: mikedeng1

Cones of Matrices and Set-Functions and 0–1 Optimization II: One Round of N on the Stable Set Polytope Gives Exactly the Odd Hole ConstraintsResearch Paper

Motivation

The stable set problem (vertex packing) asks for a largest set of pairwise non-adjacent nodes of a graph. It is NP-hard, and its polyhedral study, the description of the stable set polytope $\mathrm{STAB}(G)$ by linear inequalities, is one of the most studied topics of polyhedral combinatorics. Classes of valid inequalities (clique, odd hole, odd antihole, wheel constraints) and the graph classes they describe exactly (perfect, $t$ -perfect, $h$ -perfect graphs) organize much of that literature; see Grötschel, Lovász and Schrijver, Geometric Algorithms and Combinatorial Optimization (Springer, 1988).

Lovász and Schrijver (SIAM J. Optim. 1(2), 1991) introduced a general lift-and-project procedure for 0–1 programs: lift a relaxation $K$ into a space of matrices, impose linear conditions that every 0–1 point satisfies, and project back. One round of their operator $N$ gives a tighter relaxation $N(K)$ that still contains every 0–1 point of $K$ ; $n$ rounds give the 0–1 hull. The procedure is an ancestor of the Sherali–Adams and Lasserre hierarchies, and the stable set problem is its first test case. This mission formalizes the paper's exact description of what one round of $N$ does to the fractional stable set polytope: it adds precisely the odd hole constraints.

Setting

Let $G = (V, E)$ be a finite graph with no isolated nodes, $n = |V|$ . Vectors of $\mathbb{R}^{V \cup \{0\}}$ have a distinguished coordinate $x_0$ ; $\mathbb{R}^V$ sits inside as the hyperplane $H_0 = \{x_0 = 1\}$ , via $x \mapsto (1, x)$ .

$\mathrm{FRAC}(G) \subseteq \mathbb{R}^V$ is the solution set of the nonnegativity constraints $x_i \ge 0$ ( $i \in V$ ) and the edge constraints $x_i + x_j \le 1$ ( $ij \in E$ ).
$\mathrm{FR}(G) \subseteq \mathbb{R}^{V\cup\{0\}}$ is the cone given by $x_i \ge 0$ and $x_i + x_j \le x_0$ ; it is the cone spanned by the vectors $(1, x)$ with $x \in \mathrm{FRAC}(G)$ .
$Q$ is the cone spanned by the 0–1 vectors with $x_0 = 1$ . For a convex cone $K$ , its polar cone is $K^* = \{u : u^{\mathsf T}x \ge 0 \ \forall x \in K\}$ .
$M(K) = M(K, Q)$ is the set of $(n+1)\times(n+1)$ matrices $Y = (y_{ij})$ that are symmetric, satisfy $y_{ii} = y_{0i}$ for $i \in V$ , and satisfy $u^{\mathsf T} Y v \ge 0$ for all $u \in K^*$ , $v \in Q^*$ .
$N(K) = \{Y e_0 : Y \in M(K)\}$ , and $N(G) = \{x \in \mathbb{R}^V : (1, x) \in N(\mathrm{FR}(G))\}$ .
A set $C \subseteq V$ is an odd hole if it induces a chordless cycle of odd length $|C| \ge 3$ (triangles included). Its odd hole constraint is $\sum_{i \in C} x_i \le \frac12(|C| - 1)$ .

Formalization targets

Goal: Theorem 2.3 (p. 178)

For every finite graph $G$ without isolated nodes,

N(G) = \Big\{x \in \mathbb{R}^V : x_i \ge 0\ (i \in V),\ \ x_i + x_j \le 1\ (ij \in E),\ \ \sum_{i \in C} x_i \le \tfrac12(|C|-1)\ (C \text{ an odd hole})\Big\}.

Milestones, in the order the proof uses them

Lemma 1.3 (p. 171): for a convex cone $K \subseteq Q$ and $i \in V$ , $N(K) \subseteq (K \cap H_i) + (K \cap G_i)$ , with $H_i = \{x_i = 0\}$ , $G_i = \{x_i = x_0\}$ .
Lemma 2.2 (p. 178): if both the deletion and the contraction of some node $v$ give inequalities valid for $K$ , then $a^{\mathsf T}x \le b$ is valid for $N(K)$ .
Part (1) of the proof of Theorem 2.3 (p. 178): for an odd hole $C$ and $i \in C$ , the deletion and contraction of $i$ in the odd hole constraint are valid for $\mathrm{FRAC}(G)$ .
Observation of Section 2.b (p. 177): every $Y \in M(\mathrm{FR}(G))$ has $y_{ij} = 0$ for $ij \in E$ .
Part (2) of the proof of Theorem 2.3 (p. 178): $x \in N(G)$ if and only if some nonnegative symmetric $Y$ with $y_{00} = 1$ , $y_{i0} = y_{ii} = x_i$ satisfies $x_i + x_j + x_k - 1 \le y_{ik} + y_{jk} \le x_k$ for all $i, j, k$ with $ij \in E$ .
Lemma 2.4 (p. 178): a system $a(ij) \le y_i + y_j \le b(ij)$ , $y \ge 0$ , $y|_U = 0$ on a graph is infeasible if and only if a walk with a negative alternating sum of one of four types exists.

Significance

Theorem 2.3 gives a complete description of one round of $N$ on the stable set problem: the only new constraints are the odd hole constraints. Consequences:

For $t$ -perfect graphs (those for which nonnegativity, edge and odd hole constraints describe $\mathrm{STAB}(G)$ ), $N(G) = \mathrm{STAB}(G)$ .
It is the base case for the paper's bounds on the $N$ -index of stable set inequalities (Theorem 2.13), and it contrasts with the semidefinite operator $N_+$ , which after one round already satisfies clique, odd antihole and wheel constraints.
Lemma 2.4 is a combinatorial feasibility criterion for systems with two variables per inequality, useful beyond this paper.

The result has been proved since 1991. At the time of drafting, Prove2Me holds no formalization of it or of any part of the Lovász–Schrijver construction, and Mathlib has none. The mission produces a formal account of the $N$ operator on the stable set polytope and a formal proof of the walk criterion for two-variable systems.

Difficulty

The inclusion of $N(G)$ in the odd hole system is a short argument once Lemma 1.3 is available. The reverse inclusion is the substance: given $x$ satisfying all odd hole constraints, one must exhibit a lifted matrix $Y$ . A direct appeal to Farkas' lemma yields a certificate with no visible relation to odd cycles; the difficulty is to show that every obstruction to solvability of the matrix system forces a violated odd hole constraint, which is what Lemma 2.4 and the analysis of its four walk types accomplish. Case (d) of that analysis needs the odd hole constraints; the other cases need only the edge constraints. Lemma 2.4 itself is called folklore on the page and is stated without proof there.

A further point: Lemma 2.4 is stated for lower bounds $0 \le a$ , while the lower bounds that arise from the matrix system, $x_i + x_j + x_k - 1$ , can be negative.

Formalization scope

Coordinates of $\mathbb{R}^{V\cup\{0\}}$ are indexed by Option V, with none the coordinate $x_0$ . Graphs are Mathlib SimpleGraphs on a finite type $V$ with decidable adjacency. Every statement about a graph carries the paper's standing assumption that $G$ has no isolated nodes (∀ v, ∃ w, G.Adj v w).
$M$ is defined by condition (iii), never by its rewritings. Lemma 1.3 and Lemma 2.2 take the cone $K$ closed, a hypothesis the paper leaves tacit (its cones are polyhedral); for a non-closed $K$ Lemma 1.3 is false. $\mathrm{FR}(G)$ is polyhedral, so the goal needs no such hypothesis.
$\mathrm{FR}(G)$ is defined by its constraints; this agrees with the cone over $\mathrm{FRAC}(G)$ because $G$ has no isolated nodes.
Lemma 2.2 is stated in cone form: $K$ is any closed convex cone inside $\mathrm{FR}(G)$ , and validity is read on the slice $x_0 = 1$ . The paper's extra hypothesis $\mathrm{STAB}(G) \subseteq K$ is dropped, which strengthens the lemma.
Deletion and contraction of a node are coefficient vectors on the same graph (coefficients set to $0$ ), not inequalities on the subgraphs $G - v$ and $G - \Gamma(v) - v$ .
Odd holes are chordless odd cycles including triangles; triangles are needed, as $\tfrac12\mathbf 1$ satisfies all other constraints on a triangle.
The matrix system of part (2) is stated as an equivalence; the page uses one direction.
Lemma 2.4 uses edge values on unordered pairs and strict inequalities, exactly as printed.

A trivializing formalization is ruled out: the goal is the set equality for every graph without isolated nodes, not the existence of a lifted matrix and not a single graph.

Not formalized here: the semidefinite operator $N_+$ , the operator $\hat N$ , algorithmic statements (Theorems 1.6, 2.1, Corollary 2.5), and the set-function results of Section 3.

Reusable beyond this mission: the matrix cone layer ( $Q$ , $M$ , $N$ ), the stable-set cones, and the two-variable feasibility criterion of Lemma 2.4. Contributions of any of the milestones, and of general facts about polar cones of polyhedral cones in this setting, are welcome.

Selected references

L. Lovász and A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2) (1991) 166–190. https://doi.org/10.1137/0801013
M. Grötschel, L. Lovász and A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4
H. D. Sherali and W. P. Adams, A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems, SIAM Journal on Discrete Mathematics 3(3) (1990) 411–430. https://doi.org/10.1137/0403036

13 thms4 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Robust Mean-Covariance Solutions for Stochastic Optimization III: Concave Utilities with a Monotone Second Derivative Have a Closed-Form Robust ObjectiveResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 7

Milestones

Significance

Difficulty

Formalization scope

Selected references

Limits of Permutation Sequences II: Convergence Is Equivalent to Being Cauchy in the Rectangular DistanceResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.8, under ∣σn∣→∞|\sigma_n|\to\infty∣σn​∣→∞

Milestones

Significance

Difficulty

Formalization scope

Selected references

Lifts of Convex Sets and Cone Factorizations III: Stable Set Polytopes Have No Small Semidefinite LiftsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Discrete Convex Analysis I: Valuated MatroidsTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 2.32 (the valuated matroid characterization)

Milestone: Theorem 2.29 (the base-family / rank-function correspondence)

Significance

Difficulty

Formalization scope

Selected references

A Distributional Interpretation of Robust Optimization II: Box-Robust Sample Average Optimization Is ConsistentResearch Paper

Why robustify a sampled stochastic program

Setting

Formalization targets

Goal: Theorem 3.1 (p. 98)

Milestones (proof of Theorem 3.1, p. 99)

Significance

Difficulty

Formalization scope

Selected references

Robust solutions of Linear Programming problems contaminated with uncertain data: A Violation-Probability Bound for the Robust CounterpartResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 1 (pp. 418–419)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Assignment Game I: The Core 2: The High-Price and Low-Price Corners of the CoreResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 121)

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Learnability, Stability and Uniform Convergence III: For an ERM, Leave-One-Out Stability, Universal Consistency and Universal Generalization Are EquivalentResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.8, under $|\sigma_n|\to\infty$