Optimization

Motivation

An assignment problem pairs each of $n$ sources with exactly one of $n$ destinations while minimizing a specified cost. A permutation records those pairings. The number of permutations grows as $n!$, so a direct search quickly becomes impractical. In discrete optimal transport, the same data can be placed in a linear optimization problem over nonnegative matrices: a matrix entry records how much mass moves from one source to one destination. That formulation permits a source's mass to be split, which gives it many more feasible solutions than the assignment problem. The question for this mission is whether the added flexibility can improve the optimum when every source and destination carries the same mass. The setting and answer are given in Peyré and Cuturi, Computational Optimal Transport, §2.2–2.3.

This capstone is the first in a series based on the textbook. It links a finite combinatorial optimization problem to the matrix model used throughout later chapters. The general transport model is needed again when marginals are unequal, when cost matrices come from distances, and when entropy is added to the objective. The uniform matching case isolates a useful boundary: relaxing an assignment to allow fractional flows expands the feasible set, yet it does not change the best objective value.

Setting

Fix an integer $n>0$ and a real $n\times n$ cost matrix $C$. The entry $C_{ij}$ is the cost of sending a unit of mass from source $i$ to destination $j$. No sign or metric assumption is imposed on $C$. A permutation $\sigma$ assigns source $i$ to destination $\sigma(i)$, with every destination used once. The assignment objective of equation (2.2) is

$$A_C(\sigma)=\frac1n\sum_{i=1}^{n}C_{i,\sigma(i)}.$$

The factor $1/n$ matters: it treats each source as having mass $1/n$, so the assignment and transport objectives use the same total mass.

A histogram is a vector of masses. The uniform histogram $u$ has $u_i=1/n$ at each of the $n$ indices. A coupling of histograms $a$ and $b$ is a nonnegative matrix $P$ with row sums $a$ and column sums $b$. The set of such matrices is

$$U(a,b)=\left\{P\in\mathbb R_+^{n\times m}:\sum_jP_{ij}=a_i\ \text{for each }i,\quad\sum_iP_{ij}=b_j\ \text{for each }j\right\}.$$

Its linear cost is $\langle C,P\rangle=\sum_{i,j}C_{ij}P_{ij}$, and $L_C(a,b)$ denotes the minimum cost over $P\in U(a,b)$, as in equations (2.10)–(2.11). For a permutation $\sigma$, the scaled permutation matrix $P_\sigma$ has entry $1/n$ in column $\sigma(i)$ of row $i$ and zero elsewhere. Consequently $P_\sigma$ is a coupling of $u$ with itself, and its transport cost equals $A_C(\sigma)$. A general member of $U(u,u)$ may distribute a row's mass across several columns.

Formalization targets

Relaxation bound

Because every scaled permutation matrix is feasible for the transport problem, the unrestricted minimum cannot exceed the assignment minimum:

$$L_C(u,u)\le \min_{\sigma\in\operatorname{Perm}(n)}A_C(\sigma).$$

This is the weaker claim in the milestone list. The symmetry of couplings under transposition and the identity $\langle C,P_\sigma\rangle=A_C(\sigma)$ supply reusable statements about the model. The list also states the book's scaled form of Birkhoff's extreme point characterization.

Proposition 2.1: tightness for uniform marginals

The goal is the stronger statement: there is an assignment that also minimizes over the full coupling polytope,

$$\exists\sigma^\star\in\operatorname{Perm}(n):\quad P_{\sigma^\star}\in U(u,u),\quad \langle C,P_{\sigma^\star}\rangle=L_C(u,u),\quad A_C(\sigma^\star)=\min_{\tau\in\operatorname{Perm}(n)}A_C(\tau).$$

This is Proposition 2.1, pp. 372–373. It quantifies over every real cost matrix of the given size. The equality of optimal values follows from the stated common optimizer; the proposition does not claim that every optimal transport plan is a permutation matrix.

Significance

The result gives an exact linear relaxation for uniform assignment. One can optimize over a convex set of matrices without paying an optimal value penalty for allowing fractional mass. The conclusion has a precise limit: it guarantees at least one integral, scaled permutation optimizer, while other optimal couplings can coexist when the cost matrix has ties. When source and destination weights are unequal, the assignment formulation may not even be feasible; the broader coupling model then carries information that a permutation cannot represent.

For formalization, the result fixes a finite transport interface that later missions can compare with their own conventions: nonnegative matrix entries, prescribed row and column sums, and a cost that is linear in the matrix. Mathlib already contains Birkhoff's theorem for doubly stochastic matrices with row sums equal to $1$. This mission's formal target uses the probability normalization $1/n$, so the scaling is part of the mathematical statement. The textbook result is known; the goal here is a machine checked Lean proof of this precise version and its cited supporting claims. The listed Lean declarations are currently open statements with sorry placeholders.

Difficulty

The evident inequality points in the easy direction: enlarging a feasible set can only reduce a minimum. It gives no reason why a minimizer over the larger set should happen to be a permutation matrix. A generic feasible coupling can split mass between several destinations, and even a unique assignment need not be the only point under consideration in the relaxed problem. The central issue is the geometry of the uniform coupling polytope and its relation to permutation matrices. Its normalization differs from the usual doubly stochastic convention, so a proof using a standard library theorem must retain the factor $1/n$ at every point where a matrix or objective is converted.

Formalization scope

The Lean index types are Fin n and Fin m; they have $n$ and $m$ elements but are numbered from zero. Histograms are real valued functions on those types, and couplings are real matrices constrained to be nonnegative with exact finite row and column sums. The pairing is a finite double sum. The goal assumes $n>0$ so that the displayed $1/n$ is meaningful and the assignment problem has an index to assign. There is no additional positivity requirement on $C$. The minimum values are represented by real infima only in statements where the uniform coupling polytope and permutation set are nonempty and their finite dimensional objectives are bounded below.

An optimal coupling in the goal is compared with all matrices in $U(u,u)$, including fractional ones. Restricting that comparison to permutation matrices would erase the proposition's content. The definitions of coupling feasibility, scaled permutation matrices, and the assignment cost are reusable beyond this chapter. Contributions that establish the scaling relation to Mathlib's doubly stochastic matrices, the extreme point characterization in this normalization, or the goal from these components fit the mission. The optional strict inclusion claim on p. 372 is excluded from the milestones because its printed formulation fails at $n=1$; it would require a separate $n\ge2$ statement. The page also prints row and column sums of $P_\sigma$ as $\mathbf1_n$ despite defining entries $1/n$; the Lean statement uses $\mathbf1_n/n$.

Selected references

• G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019, DOI: 10.1561/2200000073.
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 2.7, publisher record. Cited in the proof of Proposition 2.1.

Motivation

A manufacturer that sells through an independent retailer may also open its own direct channel, an online store or a factory outlet. This is called supply chain encroachment. The operations literature has asked whether encroachment helps or hurts the two firms. The usual approach compares the double-marginalization cost of a pure retail channel with the competition the direct channel creates. With quality exogenous and uniform across channels, Arya, Mittendorf and Sappington (2007) showed that encroachment can lead to a win–win outcome when the manufacturer's direct selling cost is large, because it pushes the wholesale price down.

Ha, Long and Nasiry (Quality in Supply Chain Encroachment, MSOM 18(2), 2016; authors' manuscript SSRN 3970373) make product quality a decision of the manufacturer. Their main model lets her commit to the qualities of both channels before the retailer orders. In that model quality differentiation is not always optimal: for some parameters she sells the same quality in both channels (their Proposition 4).

Commitment is a modelling assumption. When design lead times are short, the manufacturer can redesign the direct-channel product after seeing the retailer's order, so she cannot credibly announce its quality in advance. Section 6.3 of the paper studies this fast-design case. Its only analytical result is Proposition 7: without commitment, quality differentiation across channels is always optimal. This mission formalizes that proposition and the three steps of its proof.

Setting

Consumers. A consumer has quality sensitivity $\theta$, uniform on $[0,1]$, and obtains surplus $\theta u - p$ from one unit of quality $u>0$ at price $p$. The manufacturer sells $q_M$ units of quality $u_M$ directly and the retailer sells $q_R$ units of quality $u_R$. Each consumer buys at most one unit, and the market-clearing prices depend on which product has the higher quality:

• if $u_R\le u_M$: $\;p_M = u_M(1-q_M)-u_Rq_R,\quad p_R = u_R(1-q_M-q_R)$;
• if $u_M<u_R$: $\;p_M = u_M(1-q_M-q_R),\quad p_R = u_R(1-q_R)-u_Mq_M$.

At $u_M=u_R=u$ both channels clear at $u(1-q_M-q_R)$.

Costs. One unit of quality $v$ costs the manufacturer $kv^2$, with $k>0$. She pays a selling cost $c\ge0$ for each unit sold directly; the retailer's selling cost is $0$.

Profits. For a wholesale price $w$,

$$\Pi_R = (p_R-w)\,q_R,\qquad \Pi_M = (w-ku_R^2)\,q_R + (p_M-c-ku_M^2)\,q_M .$$

Timing without commitment.

1. The manufacturer announces the retailer's quality $u_R$ and the wholesale price $w$.
2. The retailer chooses its order $q_R$.
3. The manufacturer chooses the direct-channel quality $u_M$ and quantity $q_M$.

The game has perfect information and is solved by backward induction. A strategy profile $\sigma$ has three parts: a stage-1 choice $(w,u_R)$, a retailer rule $(w,u_R)\mapsto q_R$, and a stage-3 rule $(w,u_R,q_R)\mapsto(u_M,q_M)$. The profile is a subgame perfect equilibrium (SPE) when, at every history on or off the path, the mover's action is feasible and no feasible alternative gives the mover more. The manufacturer encroaches when $q_M>0$ on the equilibrium path.

Formalization targets

Goal: Proposition 7 (p. 21)

For every $k>0$, $c\ge0$ and every SPE $\sigma$ whose equilibrium path has $q_M>0$ and $q_R>0$,

$$u_M \neq u_R \quad\text{on the equilibrium path.}$$

Milestones (proof of Proposition 7, p. 37)

Write $u_M=\tau u_R$ with $\tau>0$.

1. Stage-3 value functions. For $\tau\ge1$ the optimal direct quantity is $q_M(\tau,q_R,u_R)=\big((-c-q_Ru_R-k\tau^2u_R^2+\tau u_R)/(2\tau u_R)\big)^+$. When it is positive the optimal profit is

$$\Pi^{HF}_M=\frac{(c+u_R(q_R+\tau(k\tau u_R-1)))^2}{4\tau u_R}+q_R(w-ku_R^2).$$

The case $\tau\le1$ gives $\Pi^{LF}_M$ in the same way, and the two agree at $\tau=1$. 2. Derivatives (31)–(32). The $\tau$-derivatives of $\Pi^{HF}_M$ and $\Pi^{LF}_M$, their values at $\tau=1$, and the equivalence

$$q_M(1,q_R,u_R)>0\iff c+u_R(q_R+ku_R-1)<0.$$

3. Stage-3 contradiction. At any history with $u_R>0$ and $q_R>0$, no optimal stage-3 choice has both $u_M=u_R$ and $q_M>0$.

Milestone 3 is stronger than the goal: it holds at every stage-3 history, not only on the equilibrium path.

Significance

The result. Proposition 7 shows that the structure of the optimal product line depends on the timing of design decisions. With commitment, the manufacturer sometimes keeps a single quality. A lower-quality direct product would draw a larger retail order but forgo market segmentation, and with some parameter values she accepts that trade. Without commitment, the direct-channel quality can no longer influence the retailer's order. She then always differentiates, so whenever both channels sell, consumers face a two-product line. The paper's numerical work (Figure 6) compares the two regimes. The analytical statement that differentiation is universal without commitment is this proposition.

Formalizing it. The proposition has a short, informal proof in the e-Companion. That proof argues through first-order conditions, "given that $\tau=1$ is optimal". It uses the strict signs printed in (31) and (32), although optimality gives only weak inequalities. Its contradiction relies on the retailer's order being positive, which the statement leaves implicit. A machine-checked proof pins down exactly which hypotheses the result needs. It also contributes reusable facts about Cournot-type stage games with vertically differentiated products. No part of this paper has been formalized before.

Difficulty

The stage-3 problem is a joint choice of quality $u_M$ and quantity $q_M$, and the demand system changes form at $u_M=u_R$, so the manufacturer's profit is not differentiable in $u_M$ there. The value function after optimizing $q_M$ is a piecewise expression: $\Pi^{HF}_M$ to the right of $\tau=1$, $\Pi^{LF}_M$ to the left, and the linear profit $q_R(w-ku_R^2)$ wherever the optimal $q_M$ is zero. An argument that $\tau=1$ is not optimal has to work with one-sided derivatives of this function at a kink. It must also check that the optimal quantity stays positive on both sides near $\tau=1$.

An obvious shortcut is to argue that differentiation is optimal because segmentation always pays. That argument fails at $q_R=0$. There the manufacturer is a one-product monopolist, and $u_M=u_R$ is optimal whenever $u_R$ happens to equal her monopoly quality. The positive retail order is therefore essential.

Formalization scope

All definitions live in the namespace QualityEncroach.NoCommit. They are real-valued throughout, and the formalization fixes the following conventions:

• the wholesale price $w$ ranges over $\mathbb R$, since the paper states no sign restriction;
• qualities satisfy $u_R,u_M>0$, and quantities satisfy $q_R,q_M\ge0$;
• the inverse demand is the formula above for all nonnegative quantities, as in the paper;
• the paper derives the case $u_M<u_R$ "similarly" (p. 15), and its explicit form is the one stated above;
• $\tau$ is not named in the paper's text; its formulas read $u_M=\tau u_R$;
• subgame perfection is stated in one-shot-deviation form at every history, which in this three-stage game is equivalent to subgame perfection;
• the goal adds the hypothesis $q_R>0$ on the path, reading "across channels" as both channels selling (see Difficulty).

A trivializing formalization is ruled out: the stage-3 rule maps $(w,u_R,q_R)$ to $(u_M,q_M)$, so $u_M$ is chosen after the order. Putting $u_M$ at stage 1 would give the committed game, where the proposition is false. The goal is conditional on an SPE existing, which the paper does not prove. A verification file checks the price formulas on hand instances in both branches. At $k=1$, $c=0.05$, $u_R=0.3$, $q_R=0.1$ and $w=0.15$, it checks that the basic parameter conditions hold and a uniform stage-3 choice is strictly beaten by $u_M=0.33$. The numerical check does not establish the existence of an optimal stage-3 choice or an SPE.

A complete development needs elementary real analysis only: maximization of concave quadratics, one-variable derivatives, and one-sided optimality conditions at a kink. Proofs of any milestone, and proofs of the goal from milestone 3, are welcome.

Selected references

• A. Y. Ha, X. Long, J. Nasiry, Quality in Supply Chain Encroachment, Manufacturing & Service Operations Management 18(2), 2016. https://doi.org/10.1287/msom.2015.0562 (authors' manuscript: https://ssrn.com/abstract=3970373)
• A. Arya, B. Mittendorf, D. E. M. Sappington, The Bright Side of Supplier Encroachment, Marketing Science 26(5), 651–659, 2007. https://doi.org/10.1287/mksc.1070.0280
• M. Mussa, S. Rosen, Monopoly and Product Quality, Journal of Economic Theory 18(2), 301–317, 1978. https://doi.org/10.1016/0022-0531(78)90085-6

Motivation

Best subset selection with ridge shrinkage asks for a coefficient vector $\beta\in\mathbb R^p$ that fits a response $y\in\mathbb R^n$ through a design matrix $X\in\mathbb R^{n\times p}$ while using few nonzero coefficients:

$$\min_{\beta\in\mathbb R^p}\ \tfrac12\|y-X\beta\|_2^2 + \lambda_0\|\beta\|_0 + \lambda_2\|\beta\|_2^2 .$$

This $\ell_0\ell_2$-regularized least squares problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (BnB). The speed of BnB is governed by the strength of the continuous relaxation solved at every node: a larger relaxation value prunes more nodes. Hazimeh, Mazumder and Saab (arXiv:2004.06152, Mathematical Programming 2022) build the solver L0BnB on a perspective formulation and compare its relaxation with two standard alternatives. Their Proposition 1 quantifies that comparison, and their experiments (Section 4.2.1 of the paper) report speed-ups of more than 90× from using the perspective formulation with a tight bound $M$ instead of the bound-free formulation.

The mission formalizes Proposition 1 together with the three steps of its proof in the paper's Appendix A.

Setting

Fix $X$, $y$, regularization parameters $\lambda_0,\lambda_2>0$ and a bound $M>0$ on $\|\beta\|_\infty$; write $[p]=\{1,\dots,p\}$.

The Big-M formulation $B(M)$ introduces indicators $z_i$ and minimizes $\tfrac12\|y-X\beta\|_2^2+\lambda_0\sum_i z_i+\lambda_2\|\beta\|_2^2$ subject to $-Mz_i\le\beta_i\le Mz_i$, $z_i\in\{0,1\}$. Its interval relaxation lets $z_i\in[0,1]$; its optimal value is $V_{B(M)}$.

The reverse Huber penalty is $\mathcal B(t)=|t|$ for $|t|\le1$ and $(t^2+1)/2$ for $|t|\ge1$. Put

$$\psi_1(b;\lambda_0,\lambda_2)=2\lambda_0\,\mathcal B\big(b\sqrt{\lambda_2/\lambda_0}\big),\qquad \psi_2(b;\lambda_0,\lambda_2,M)=\Big(\frac{\lambda_0}{M}+\lambda_2M\Big)|b|,$$

and let $\psi=\psi_1$ if $\sqrt{\lambda_0/\lambda_2}\le M$ and $\psi=\psi_2$ if $\sqrt{\lambda_0/\lambda_2}>M$. The paper's Theorem 1 shows that the interval relaxation of the perspective formulation $\mathrm{PR}(M)$ is equivalent to

$$\min_{\|\beta\|_\infty\le M} F(\beta),\qquad F(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi(\beta_i;\lambda_0,\lambda_2,M), \tag{5}$$

and $V_{PR(M)}$ denotes the optimal value of (5). Without a bound, the relaxation value of $\mathrm{PR}(\infty)$ is

$$V_{PR(\infty)}=\min_{\beta\in\mathbb R^p}G(\beta),\qquad G(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi_1(\beta_i;\lambda_0,\lambda_2). \tag{6}$$

Finally $h(\lambda_0,\lambda_2,M)=\lambda_0/M+\lambda_2M-2\sqrt{\lambda_0\lambda_2}$, and $\beta^*$ denotes an optimal solution of (5).

Formalization targets

Goal: Proposition 1

For $\sqrt{\lambda_0/\lambda_2}>M$,

$$V_{PR(M)}\ \ge\ V_{B(M)}+\lambda_2\big(M\|\beta^*\|_1-\|\beta^*\|_2^2\big), \tag{7}$$ $$V_{PR(M)}\ \ge\ V_{PR(\infty)}+h(\lambda_0,\lambda_2,M)\,\|\beta^*\|_1. \tag{8}$$

Milestones

1. (37): $V_{B(M)}=\min_{\|\beta\|_\infty\le M}H(\beta)$ with $H(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_i\big(\tfrac{\lambda_0}{M}|\beta_i|+\lambda_2\beta_i^2\big)$; the Big-M relaxation expressed in $\beta$ alone. It holds for every $M>0$.
2. (7) alone.
3. The linear case of $\psi_1$: if $|b|\le M<\sqrt{\lambda_0/\lambda_2}$ then $\psi_1(b;\lambda_0,\lambda_2)=2|b|\sqrt{\lambda_0\lambda_2}$.
4. (8) alone (the paper's (38)).

The goal is the conjunction of milestones 2 and 4.

Significance

In the regime $\sqrt{\lambda_0/\lambda_2}>M$ both added terms are nonnegative: $M\|\beta^*\|_1\ge\|\beta^*\|_2^2$ because $\|\beta^*\|_\infty\le M$, and $h>0$ because $\lambda_0/M+\lambda_2M>2\sqrt{\lambda_0\lambda_2}$ whenever $M\ne\sqrt{\lambda_0/\lambda_2}$. So the perspective relaxation is at least as strong as both the Big-M relaxation and $\mathrm{PR}(\infty)$, strictly so as soon as one coordinate of $\beta^*$ lies strictly inside $(0,M)$ in absolute value (for (7)) or $\beta^*\ne0$ (for (8)). The bounds are explicit in the relaxation's own solution, so they can be evaluated at a BnB node. This is the theoretical justification for the paper's design choice of building its solver on $\mathrm{PR}(M)$ with a valid, tight $M$; the regime $\sqrt{\lambda_0/\lambda_2}\le M$, where (5) is (6) with the additional box constraint $\|\beta\|_\infty\le M$, is complementary.

Proposition 1 is proved in the paper; it has no machine-checked proof. The mission produces one, together with reusable Lean definitions of the three relaxation values and of the reverse Huber penalty that other statements about perspective relaxations of sparse regression can be stated against.

Difficulty

The arithmetic of the coordinate-wise penalties is short. The substance is in comparing optimal values that are defined as infima over different feasible sets. The obvious argument "$V_{PR(M)}-V_{B(M)}\ge F(\beta^*)-H(\beta^*)$" requires that the Big-M relaxation, which is posed over pairs $(\beta,z)$, have value at most $H(\beta^*)$; that is the content of (37), a statement about a different feasible set in more variables. Likewise (8) needs $V_{PR(\infty)}\le G(\beta^*)$, i.e. that the infimum in (6) is a genuine lower bound of a set bounded below, and both inequalities use the regime $\sqrt{\lambda_0/\lambda_2}>M$, in which $\psi=\psi_2$. Dropping the regime hypothesis makes (8) false in general: for $\sqrt{\lambda_0/\lambda_2}\le M$ one has $\psi=\psi_1$ and $h\ge0$, and the right side can exceed $V_{PR(M)}=V_{PR(\infty)}$.

Formalization scope

All objects live in the namespace L0BnB.Strength. Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M as hypotheses; $[p]$ is Fin p. Norms are explicit sums: $\|v\|_2^2$ is ∑ i, v i ^ 2, $\|\beta\|_1$ is ∑ i, |β i|, and $\|\beta\|_\infty\le M$ is ∀ i, |β i| ≤ M. The regime is written M < Real.sqrt (lam0 / lam2).

Optimal values are sInf of the image of the feasible set in ℝ. Each set is nonempty ($\beta=0$, $z=0$) and bounded below by $0$ under the positivity hypotheses, so sInf is the true infimum and never a junk value. $V_{B(M)}$ is defined over pairs $(\beta,z)$ with $z_i\in[0,1]$, not through $H$; (37) is a theorem. $V_{PR(\infty)}$ is (6) as printed: the paper attributes to its reference [21] the identification of (6) with the interval relaxation of $\mathrm{PR}(\infty)$ in $(\beta,z,s)$ variables, and that identification is not part of the mission. $V_{PR(M)}$ is the value of (5), which is the paper's definition; Theorem 1 (the equivalence of (5) with the $(\beta,z,s)$ relaxation) belongs to a sibling mission.

The optimal solution $\beta^*$ is a binder with the hypotheses $\|\beta^*\|_\infty\le M$ and $F(\beta^*)\le F(\beta)$ for every $\beta$ in the box. A formalization in which $\beta^*$ is an arbitrary feasible point, or in which $V_{B(M)}$ or $V_{PR(\infty)}$ is defined through a chosen minimizer, would change the statement and is ruled out. The paper uses no $O(\cdot)$ in this result, so no constant is instantiated.

Needed infrastructure is light: continuity of $H$ and compactness of the box for the attainment in (37), and csInf lemmas on ℝ. Contributions of proofs of any milestone, and of the attainment of the infimum in (5), are welcome.

Selected references

• H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2, 2021; Mathematical Programming (2022). https://arxiv.org/abs/2004.06152
• H. Hazimeh, R. Mazumder, Fast Best Subset Selection: Coordinate Descent and Local Combinatorial Optimization Algorithms, Operations Research 68(5), 1517–1537, 2020. https://doi.org/10.1287/opre.2019.1919
• H. Dong, K. Chen, J. Linderoth, Regularization vs. Relaxation: A conic optimization perspective of statistical variable selection, arXiv e-prints, 2015 (the paper's reference [21], source of (6) for $\mathrm{PR}(\infty)$). https://arxiv.org/abs/1510.06083

Motivation

The optimal assignment problem asks for a one-to-one matching of $n$ points to $n$ objects of least total cost. It is the discrete optimal transport problem between two uniform measures with the same number of atoms, and by the Birkhoff–von Neumann theorem it coincides with the Kantorovich linear program on that instance (Peyré and Cuturi, Computational Optimal Transport, Proposition 2.1). Assignment solvers are therefore the inner routine of exact discrete optimal transport, of matching-based estimators in statistics and of many combinatorial optimization pipelines.

The auction algorithm was introduced by Bertsekas in 1981 (Bertsekas 1981) and refined with ε-scaling by Bertsekas and Eckstein in 1988 (Bertsekas & Eckstein 1988). It is a dual coordinate method with an economic reading: unassigned points bid for objects, prices of contested objects move, and an object changes hands when outbid. Its practical appeal is that each iteration is local and cheap, and that it parallelizes well. Peyré and Cuturi present it in §3.7 of their monograph (pp. 417–422) as an alternative use of the machinery of C-transforms, and as a precursor to the Sinkhorn algorithm of Chapter 4.

Setting

Fix $n\ge 2$, write $[\![n]\!]=\{1,\dots,n\}$, and let $\mathbf C\in\mathbb R^{n\times n}$ be a cost matrix: $\mathbf C_{i,j}$ is the cost of assigning point $i$ to object $j$. A permutation $\sigma$ of $[\![n]\!]$ is an assignment, of cost $\sum_i \mathbf C_{i,\sigma_i}$.

A dual vector (price vector) $\mathbf g\in\mathbb R^n$ is indexed by the objects. Its $\bar{\mathbf C}$-transform is $(\mathbf g^{\bar{\mathbf C}})_i=\min_j \mathbf C_{i,j}-\mathbf g_j$, the best adjusted cost available to point $i$; a pair $(\mathbf f,\mathbf g)$ is dual feasible if $\mathbf f_i+\mathbf g_j\le \mathbf C_{i,j}$ for all $i,j$.

The algorithm maintains a triplet $(S,\xi,\mathbf g)$: a set $S\subseteq[\![n]\!]$ of assigned points, a partial assignment vector $\xi$ (an injective map from $S$ to $[\![n]\!]$) and a dual vector $\mathbf g$. The state satisfies ε-complementary slackness (ε-CS) if

$$\forall i\in S,\qquad \mathbf C_{i,\xi_i}-\mathbf g_{\xi_i}\le \varepsilon+\min_j\big(\mathbf C_{i,j}-\mathbf g_j\big).$$

One iteration picks a point $i\notin S$, a lowest adjusted cost index $j^1_i\in\operatorname{argmin}_j \mathbf C_{i,j}-\mathbf g_j$ and a second lowest $j^2_i\in\operatorname{argmin}_{j\neq j^1_i}\mathbf C_{i,j}-\mathbf g_j$, and performs

$$\mathbf g_{j^1_i}\leftarrow \mathbf C_{i,j^1_i}-\big(\mathbf C_{i,j^2_i}-\mathbf g_{j^2_i}\big)-\varepsilon, \tag{3.9}$$

removes from $S$ the point $i'$ with $\xi_{i'}=j^1_i$ (if there is one), sets $\xi_i=j^1_i$ and adds $i$ to $S$. The algorithm starts from $S=\emptyset$, $\mathbf g=0_n$, and terminates when $S=[\![n]\!]$.

Formalization targets

Goal: Proposition 3.9 (p. 422)

For every $\varepsilon>0$ and every run of the algorithm that terminates, the final $\xi$ is a permutation and

$$\sum_i \mathbf C_{i,\xi_i}\;\le\;\sum_i \mathbf C_{i,\sigma_i}+n\varepsilon\qquad\text{for every permutation }\sigma.$$

The goal fixes no particular tie-breaking rule and no order in which unassigned points bid: it holds for all of them.

Milestones

1. (3.8), p. 419. If $\mathbf C_{i,\sigma_i}-\mathbf g_{\sigma_i}=\min_j \mathbf C_{i,j}-\mathbf g_j$ for every $i$, then $\sigma$ is an optimal assignment and $(\mathbf g^{\bar{\mathbf C}},\mathbf g)$ is an optimal dual pair.
2. Properties (b)–(c), pp. 419–420. At each iteration the size of $S$ does not decrease, some price decreases by at least $\varepsilon$, and no price increases.
3. Proposition 3.7, p. 420. Every state of every run satisfies ε-CS.

Companion: Proposition 3.8 (p. 421), corrected

For $\mathbf C\ge 0$, every run has at most $n\big(\lfloor\|\mathbf C\|_\infty/\varepsilon\rfloor+1\big)$ iterations. This is the termination statement; the goal does not depend on it.

Significance

Proposition 3.9 is the accuracy guarantee of the auction algorithm. With integer costs and $\varepsilon<1/n$ it yields an exactly optimal assignment, which is how the algorithm is used as an exact solver; combined with ε-scaling it gives the complexity bounds quoted in Remark 3.3. The argument is also the template for every ε-relaxed primal–dual method: an approximate optimality certificate maintained by local moves, turned into a global suboptimality bound by weak duality.

The results are classical and proved in the book and in Bertsekas's monographs; they are not open. What this mission adds is a machine-checked account of the algorithm with all of its nondeterminism (ties in the argmins, the order of bidders) quantified explicitly, together with the corrected iteration bound. To the best of the mission's prior-art search, no Lean formalization of the auction algorithm exists on the platform or in Mathlib, which has the assignment problem only implicitly (through permutations and doubly stochastic matrices).

Difficulty

The obvious argument for the goal sums the ε-CS inequality over $i$ and compares with an arbitrary permutation $\sigma$. The sum telescopes only if the final $\xi$ is a bijection, so the proof must carry, through every iteration, the invariant that $\xi$ is injective on $S$, and this invariant interacts with the removal of the displaced point in step 2: the set update has to remove exactly the point holding $j^1_i$, which needs injectivity at the previous step.

Preserving ε-CS for the points that are not bidding relies on prices only ever decreasing, which in turn needs $\varepsilon\ge 0$ and the specific form of (3.9); preserving it for the bidder needs the second-best index $j^2_i$ to realize the minimum over $j\neq j^1_i$, including in the presence of ties. The printed termination bound is false (see below), so the companion requires reconstructing the counting argument: an object that is still unassigned has never been bid on and keeps price $0$, which caps the number of bids on any other object.

Formalization scope

• $[\![n]\!]$ is Fin n; $\mathbf C$ is a Matrix (Fin n) (Fin n) ℝ; prices are Fin n → ℝ; $\min_j$ is the infimum over the finite nonempty index set.
• A state is a structure with fields S : Finset (Fin n), ξ : Fin n → Fin n and g : Fin n → ℝ. Only the values of ξ on S are meaningful; injectivity on S is a property to be proved, not a field.
• An iteration is a relation between consecutive states (AuctionStep), with the choice of bidder, of $j^1_i$ and of $j^2_i$ existential. A run of $T$ iterations is a sequence of states starting from $S=\emptyset$, $\mathbf g=0$; it is terminated when $S=[\![n]\!]$ at step $T$. The results hold for every run, whatever the tie-breaking.
• Costs are the unnormalized sums $\sum_i \mathbf C_{i,\sigma_i}$, as in the book's proof of Proposition 3.9. Under the $\frac1n$ normalization of (2.2) the gap $n\varepsilon$ becomes $\varepsilon$.
• Added hypotheses: $n\ge2$ in the goal (the second-best index requires it); $\varepsilon>0$ throughout; $\mathbf C\ge0$ in the corrected Proposition 3.8, which its proof uses.
• Printed slips. Proposition 3.8 as printed ($N=n\|\mathbf C\|_\infty/\varepsilon$) fails for $\mathbf C=0$; the companion states the bound the proof gives. Property (b) "can only increase" is stated as non-decrease; property (c) refers to an object index $j$.
• Trivialization ruled out. The run predicate forces the initial state, the exact update (3.9) and the set update of step 2 at every iteration, and the goal requires $S=[\![n]\!]$ at the end; a terminated run exists already for $n=2$, so the goal is not vacuous.

Contributions welcome: the injectivity invariant of ξ on S as a reusable lemma; the milestones in any order; a proof of termination (the companion) and of the existence of a terminated run for every $n\ge2$.

Selected references

• G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019, §3.7. https://doi.org/10.1561/2200000073
• D. P. Bertsekas, A new algorithm for the assignment problem, Mathematical Programming 21:152–171, 1981. https://doi.org/10.1007/BF01584237
• D. P. Bertsekas and J. Eckstein, Dual coordinate step methods for linear network flow problems, Mathematical Programming 42:203–243, 1988. https://doi.org/10.1007/BF01589417
• D. P. Bertsekas, Auction algorithms for network flow problems: A tutorial introduction, Computational Optimization and Applications 1:7–66, 1992. https://doi.org/10.1007/BF00247653