Operations Research

Motivation

Lasserre's hierarchy is a sequence of semidefinite relaxations for minimizing a polynomial over a set defined by polynomial equations and inequalities (Lasserre 2001). Under the archimedean condition its optimal values converge to the true minimum, but only asymptotically in general; in practice the hierarchy is often exact at a small relaxation order. J. Nie's paper (arXiv:1206.0319v2, Math. Program. 146 (2014)) explains this gap in two steps. Its Theorem 1.1 shows that finite convergence follows when the classical optimality conditions of nonlinear programming hold at every global minimizer. Its Theorem 1.2, the subject of this mission, shows that those optimality conditions hold at every local minimizer for all input data outside the zero set of finitely many polynomials in the coefficients. Together the two results give finite convergence of Lasserre's hierarchy for generic archimedean problems.

The genericity statement is also of independent interest in nonlinear programming: it says that degenerate local minimizers (failing constraint qualification, strict complementarity or second order sufficiency) are an algebraically exceptional phenomenon for polynomial data of fixed degrees.

Setting

Fix $n$ variables $x=(x_1,\dots,x_n)$ and write $\mathbb R[x]_d$ for the real polynomials of degree at most $d$. Problem (1.1) is

$$\min f(x)\quad\text{s.t.}\quad h_i(x)=0\ (i\in[m_1]),\qquad g_j(x)\ge 0\ (j\in[m_2]),$$

with feasible set $K$. For $u\in K$ the active set is $J(u)=\{j: g_j(u)=0\}$. At $u$:

• the constraint qualification condition (CQC) holds if $\nabla h_1(u),\dots,\nabla h_{m_1}(u),\nabla g_j(u)$ ($j\in J(u)$) are linearly independent;
• Lagrange multipliers $\lambda,\mu$ satisfy (1.3) $\nabla f(u)=\sum_i\lambda_i\nabla h_i(u)+\sum_j\mu_j\nabla g_j(u)$ and (1.4) $\mu_jg_j(u)=0$, $\mu_j\ge0$;
• strict complementarity (1.5) is $\mu_j+g_j(u)>0$ for all $j$;
• with $L=f-\sum_i\lambda_ih_i-\sum_{j\in J(u)}\mu_jg_j$, the second order sufficiency condition (1.7) is $v^T\nabla^2L(u)v>0$ for every $v\neq0$ orthogonal to all active constraint gradients.

The input data are the coefficient vectors of $(f,h,g)\in\mathbb R[x]_{d_0}\times\prod_i\mathbb R[x]_{d_i}\times\prod_j\mathbb R[x]_{d'_j}$; a polynomial in the coefficients is a real polynomial evaluated at that vector. The paper's Condition 4.3 lists four families of such polynomials: resultants $\mathrm{Res}$ and discriminants $\Delta$ (§2.4) of subsets of the constraints, and the polynomials $\mathscr R$ of (4.6) and $\mathscr D$ of (4.11), which detect a complex projective solution of the homogenised critical-point systems (4.5) and (4.10). Homogenisation is $\tilde p(\tilde x)=x_0^{d}p(x/x_0)$ at the nominal degree $d$, with $\tilde x=(x_0,\dots,x_n)$.

Formalization targets

Goal: Theorem 1.2

For positive degrees $d_0,d_i,d'_j$ there are polynomials $\phi_1,\dots,\phi_L$ in the coefficients such that

$$\exists\,(f,h,g)\text{ admissible with }\textstyle\prod_l\phi_l\neq0,\qquad\text{and}\qquad \prod_l\phi_l(f,h,g)\neq0\ \Longrightarrow\ \text{CQC, (1.5), (1.7) at every local minimizer of (1.1).}$$

Milestones

1. Proposition 4.1: there is $\mathscr R$ with $\mathscr R(p_0,\dots,p_k;q)=0$ iff (4.5) has a solution $0\neq\tilde x\in\mathbb C^{n+1}$; and $\mathscr R\neq0$ excludes solutions of (4.4) in $\mathbb C^n$.
2. Proposition 4.2: there is $\mathscr D$ with $\mathscr D(p_0,\dots,p_k)=0$ iff (4.10) has a solution with $\tilde x\neq0$, $y\neq0$; and $\mathscr D\neq0$ makes the KKT system (4.2) nonsingular.
3. Proposition 4.4: at $u\in K$ with multipliers satisfying (1.3) and $\mu_jg_j(u)=0$, items (a)–(d) of Condition 4.3 give at most $n-m_1$ active constraints, CQC, $\lambda_i\neq0$ and $\mu_j\neq0$ on $J(u)$, and $\det H(u)\neq0$ for $H(u)=\left[\begin{smallmatrix}\nabla^2L(u)&G(u)^T\\G(u)&0\end{smallmatrix}\right]$.
4. Lemma 4.6: at a local minimizer where $G(u)$ has full rank, (1.7) holds iff $\det H(u)\neq0$.
5. Proposition 4.5: Condition 4.3 implies CQC, strict complementarity and SOSC at every local minimizer.
6. Appendix A: $\mathscr R$ and $\mathscr D$ do not vanish identically on the input space of given positive degrees.

Significance

The theorem gives the second half of the paper's explanation of finite convergence: combined with Theorem 1.1, Lasserre's hierarchy converges in finitely many steps for all archimedean problems with input outside a proper algebraic subset. Section 5 of the paper derives further consequences, for instance that Marshall's boundary Hessian condition holds on a Zariski open set of data, and that Putinar-type certificates exist generically on the boundary of the cone of nonnegative polynomials. Beyond polynomial optimization, the statement is a precise algebraic form of the folklore that "generic nonlinear programs are nondegenerate".

The result is proved in the paper; no machine-checked version is known. A formalization fixes the exact quantifier structure (the printed statement is vacuous without a nonvanishing clause, and two items of Proposition 4.4 need an extra hypothesis), and builds reusable infrastructure: projective elimination over $\mathbb C$, homogenisation at a nominal degree, and the bordered-Hessian characterization of second order sufficiency.

Difficulty

The local part (Proposition 4.4, Lemma 4.6, Proposition 4.5) is linear algebra plus first and second order necessary conditions. The global part is not. Proposition 4.1 and 4.2 need the main theorem of elimination theory: the set of coefficient vectors for which a homogeneous (or bihomogeneous) system has a nonzero complex solution is Zariski closed, defined by polynomials in the coefficients. Mathlib has the univariate resultant only. Appendix A, which shows these polynomials do not vanish identically, has to control the homogenised systems both at finite points and at points at infinity ($x_0=0$), where only the leading forms of the data are seen. Reasoning over $\mathbb R$ alone does not suffice: the set of data whose real system is solvable is not the zero set of a polynomial.

Formalization scope

Polynomials are MvPolynomial (Fin n) ℝ, points are Fin n → ℝ, and gradients and Hessians are formal partial derivatives. Homogenised polynomials have complex coefficients in n + 1 variables, variable 0 being $x_0$, and homogenisation uses the nominal degree $d$, not the actual degree. CQC is linear independence of an indexed family (repeated gradients count twice). The optimality conditions are bundled: CQC together with one multiplier pair satisfying (1.3), (1.4), (1.5) and (1.7); under CQC the multipliers are unique.

Condition 4.3 is encoded through the defining properties of Res, Δ, $\mathscr R$ and $\mathscr D$ (unsolvability of the corresponding complex projective systems) rather than through the polynomials themselves; since the goal is existential in the polynomials, this is not a weakening. Coefficient variables exist for monomials of every degree, so the goal's nonvanishing clause is asserted at an admissible input: a formal polynomial that is nonzero but vanishes on all admissible data (such as the variable of a monomial of degree $d_0+1$) does not satisfy it. Without that clause the printed theorem would be satisfied by $\phi_1=0$.

Hypotheses added to the page, each disclosed in the statements: $m_1\le n$ in Propositions 4.4 and 4.5 (Condition 4.3's standing assumption; Theorem 1.2 is stated for all $m_1$, as printed), the nonvanishing clause in Theorem 1.2, and item (a) of Condition 4.3 in Proposition 4.4 ii)–iv) (with item (b) alone, $n=1$, $g_1=x+x^2$, $g_2=-x+x^2$, $u=0$ violates CQC). Proposition 4.2's nonsingularity is asserted at all complex critical pairs.

A complete development needs projective elimination theory over $\mathbb C$ (reusable well beyond this mission), multivariate resultants and discriminants as polynomial functions of coefficients, Euler's identity for forms, and genericity facts about critical points of polynomial programs. Contributions to any of these, and direct proofs of the local milestones, are welcome.

Selected references

• J. Nie, Optimality conditions and finite convergence of Lasserre's hierarchy, Math. Program. 146 (2014); preprint arXiv:1206.0319v2, 2013. https://arxiv.org/abs/1206.0319v2, https://doi.org/10.1007/s10107-013-0680-x
• J.B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11(3) (2001) 796–817. https://doi.org/10.1137/S1052623400366802
• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977 (Theorem I.5.7A, elimination). https://doi.org/10.1007/978-1-4757-3849-0
• I. Gelfand, M. Kapranov, A. Zelevinsky, Discriminants, Resultants, and Multidimensional Determinants, Birkhäuser, 1994. https://doi.org/10.1007/978-0-8176-4771-1

Model-free bounds for lookback options

A lookback option pays a function of the running maximum of the underlying asset over the life of the contract. When the prices of European call options of all strikes at the maturity are quoted, the risk-neutral law $\mu$ of the terminal price is known, but the law of the whole path is not. The robust (model-free) superhedging cost of the lookback payoff is the cheapest initial capital that, combined with a static position in the quoted calls and dynamic trading in the underlying, dominates the payoff in every model consistent with $\mu$.

Hobson (Finance Stoch. 1998) computed this cost for $g(x)=x$ by a pathwise inequality, and identified the extremal model through the Azéma–Yor solution of the Skorokhod embedding problem (Azéma–Yor 1979). Galichon, Henry-Labordère and Touzi (Ann. Appl. Probab. 2014, arXiv:1401.3921) recast model-free bounds as a dual stochastic control problem in which the marginal constraint is penalised by a Lagrange multiplier $\lambda$. Their Theorem 3.1 recovers Hobson's bound for every $C^1$ nondecreasing $g$ from that dual, with an explicit optimal multiplier and stopping time. The result is one of the founding examples of martingale optimal transport.

Setting

Let $B$ be a real Brownian motion with continuous paths and $B_0=0$, adapted to a filtration $(\mathcal F_t)_{t\ge0}$ with increments independent of the past, and let $X_t=X_0+B_t$ for a spot $X_0\in\mathbb R$. Write $X^*_\tau=\max_{t\le\tau}X_t$. Let $\mathcal T_\infty$ be the set of stopping times $\tau$ for which the stopped process $(X_{t\wedge\tau})_{t\ge0}$ is a uniformly integrable martingale.

The marginal is a probability measure $\mu$ on $\mathbb R$ with finite first moment and mean $\int x\,\mu(dx)=X_0$. Its call prices are $c(x)=\int(y-x)^+\mu(dy)$. The payoff is $\xi=g(X^*)$ with $g:\mathbb R\to\mathbb R_+$ of class $C^1$ and nondecreasing.

For a multiplier $\lambda:\mathbb R\to\mathbb R$ and $\tau\in\mathcal T_\infty$ set $J(\lambda,\tau)=\mathbb E[g(X^*_\tau)-\lambda(X_\tau)]$ and $u^\lambda(X_0,X_0)=\sup_{\tau\in\mathcal T_\infty}J(\lambda,\tau)$. The admissible multipliers are

$$\Lambda^\mu_0=\Big\{\lambda\in\mathbb L^1(\mu):\ \sup_{\tau\in\mathcal T_\infty}\mathbb E[\lambda(X_\tau)^-]<\infty\Big\},$$

and the reduced superhedging problem (3.7) is

$$U^\mu(\xi)=\inf_{\lambda\in\Lambda^\mu_0}\Big\{\int\lambda\,d\mu+u^\lambda(X_0,X_0)\Big\}.$$

The barycenter function is $b(x)=\int_{[x,\infty)}y\,\mu(dy)/\mu([x,\infty))$ for $\mu((x,\infty))>0$ and $b(x)=x$ otherwise. The Hardy–Littlewood transform $\mu^{HL}$ is the probability measure with

$$\mu^{HL}([y,\infty))=\inf_{\xi<y}\frac{c(\xi)}{y-\xi}.$$

The Azéma–Yor stopping time is $\tau^*=\inf\{t>0:X^*_t\ge b(X_t)\}$, and the candidate multiplier is

$$\lambda^*(x)=\int_{\ell^\mu}^{x}\!\int_{\ell^\mu}^{y}g'(b(\xi))\,\frac{b(d\xi)}{b(\xi)-\xi}\,dy ,$$

that is, the convex function vanishing below $\ell^\mu$ that solves the weak ODE (3.21) with $\psi=b^{-1}$.

Formalization targets

Goal: Theorem 3.1

If $\sup_{\tau\in\mathcal T_\infty}\mathbb E[g(X^*_\tau)]<\infty$ and $\mu^{HL}(g)=\int g\,d\mu^{HL}<\infty$, then

$$U^\mu(\xi)=\mu(\lambda^*)+J(\lambda^*,\tau^*)=\mu^{HL}(g).$$

The goal is the paper's theorem for the reduced problem (3.7), in its full two-equality form: the value, its attainment by $(\lambda^*,\tau^*)$, and its closed form.

Milestones

1. The Neumann condition (3.23) for Peskir's candidate $v^\psi$.
2. Lemma 3.1: $u^\lambda\le v^\psi$ for convex $\lambda\in\Lambda^\mu_0$ and every relaxed free boundary $\psi\in\Psi^\lambda$.
3. Step (1) of Lemma 3.2: $\mu(\lambda)-\lambda(X_0)=\int(c-c_0)\,d\lambda''$, with $c_0(x)=(X_0-x)^+$.
4. Lemma 3.2: $\mu(\lambda)+u^\lambda(X_0,X_0)\le g(X_0)+\int\varphi(\psi(m),m)g'(m)\,dm$.
5. The pointwise minimizations (3.27) and (3.28).
6. Steps (2) and (3) of Lemma 3.3: properties of $\lambda^*$, and the integration by parts giving $\mu^{HL}(g)$.
7. Lemma 3.3, the upper bound $U^\mu(\xi)\le\mu^{HL}(g)$.
8. The Azéma–Yor facts: $\tau^*\in\mathcal T_\infty$, $X_{\tau^*}\sim\mu$, $X^*_{\tau^*}\sim\mu^{HL}$.
9. The lower bound $U^\mu(\xi)\ge\mu^{HL}(g)$ of Section 3.4.

Significance

The theorem identifies the model-free price of a lookback payoff as an explicit functional of the call prices, $\mu^{HL}(g)$, and exhibits the extremal model (Brownian motion stopped at $\tau^*$) and the optimal static hedge ($\lambda^*$). It shows that the dual stochastic control formulation is sharp on a nontrivial path-dependent payoff, which is the template for later work on martingale optimal transport with path-dependent costs.

The result has been proved since 2014 (and Hobson's bound since 1998). It has not been formalized. A complete development would provide machine-checked versions of the Azéma–Yor embedding, the law of the maximum at the embedding, a verification theorem for a reflected optimal stopping problem with a nonsmooth obstacle, and the convex-analytic identities linking call prices to second-derivative measures. Each of these is reusable well beyond this paper.

Difficulty

The upper bound requires a verification argument for an optimal stopping problem of the pair $(X,X^*)$ with a reflection at the diagonal, where the candidate $v^\psi$ is only as regular as the convex multiplier $\lambda$: second derivatives are measures and the free boundary $\psi$ solves its ODE only in a relaxed sense. An Itô formula for $C^2$ functions does not apply; an Itô–Tanaka (local time) argument for concave functions of $X$, with the reflection term killed by the Neumann condition, is needed, followed by a localisation that uses uniform integrability and the integrability condition in $\Lambda^\mu_0$. The lower bound needs the Azéma–Yor embedding and the law of $X^*_{\tau^*}$, neither of which is in Mathlib; the naive appeal to "the embedding exists" does not give the joint law of the stopped value and the maximum.

Formalization scope

The Lean development lives in the namespace LookbackMOT.HL and uses Mathlib's IsBrownianReal, IsStoppingTime, stoppedProcess, stoppedValue, Martingale, UniformIntegrable and HasLaw. Committed conventions:

• What is formalized. The goal is the reduced problem (3.7), not the superhedging problem (2.6): (2.6) needs stochastic integrals, which Mathlib does not have. The bridge between them (Proposition 2.1, the claim (3.4), Proposition 3.1) is outside this mission. The theorem's hypothesis $\sup_{\mathbb P\in\mathcal P_\infty}\mathbb E^{\mathbb P}[\xi^+]<\infty$ is stated through Proposition 3.1 with $\lambda=0$ as $\sup_{\tau\in\mathcal T_\infty}\mathbb E[g(X^*_\tau)]<\infty$. The horizon $T$ disappears: the stopping problem is over $\mathcal T_\infty$ with time in $[0,\infty)$.
• Standing hypotheses. The Brownian motion lives on an arbitrary filtered probability space with everywhere-continuous paths and $B_0=0$; the paper's canonical space is one instance. The mean condition and integrability of $\mu$ (p. 7) are assumed throughout. The spot $X_0$ is any real number. $\mu([0,\infty))=1$ is assumed only in (3.27).
• Added conditions. Every $\tau\in\mathcal T_\infty$ is a.s. finite (implied by uniform integrability). Every $\lambda\in\Lambda^\mu_0$ is measurable.
• Expectations of payoffs are $\mathbb E[\varphi^+]-\mathbb E[\varphi^-]$ in the extended reals, with $\infty-\infty=-\infty$; value functions are extended reals.
• Derivatives. $\lambda'$ is the right derivative and $\lambda''$ its Stieltjes measure. The weak ODE (3.21) is used both as a change of variables ($\lambda''$ is the image of $g'(m)/(m-\psi(m))\,dm$ under $\psi$) and on intervals ($\lambda'(\psi(y_2))-\lambda'(\psi(y_1))=\int_{y_1}^{y_2}g'(m)/(m-\psi(m))\,dm$), the two forms the paper's proofs use.
• The multiplier $\lambda^*$. It is written as $\lambda^*(x)=\int_{X_0<m<r^\mu}g'(m)(x-b^{-1}(m))^+/(m-b^{-1}(m))\,dm$, the change of variables $m=b(\xi)$ in (3.14) and the solution of (3.21) with $\psi=b^{-1}$ that the proof of Lemma 3.3 uses. It agrees with the $b(d\xi)$ formula when $b$ is continuous; at the jumps of $b$ (atoms of $\mu$) the Lebesgue–Stieltjes reading of (3.14) can fail to be $\mu$-integrable.
• Measures given by identities. $\mu^{HL}$ and $\lambda''$ enter as measures satisfying their defining identities on intervals; each exists and is unique.
• Printed slips not copied. (3.12) prints the numerator $c(y)$; the formalization uses $c(\xi)$. $b$, $\mu^{HL}$ and $\lambda^*$ are extended from $x\ge0$ to all of $\mathbb R$ by the same formulas.

No trivializing reading is available. Payoff expectations are never Bochner integrals (which would be $0$ for non-integrable payoffs). $\tau\equiv0$ lies in $\mathcal T_\infty$ and $\lambda\equiv0$ in $\Lambda^\mu_0$, so neither the supremum nor the infimum is over an empty set. The predicates for $\mu^{HL}$ and $\lambda''$ are satisfiable (witnessed for $\mu=\delta_{X_0}$ in a sorry-free check). $X_\tau$ is only evaluated where $\tau<\infty$ a.s. Every division has a positive denominator on the sets that carry mass.

Contributions welcome: the Azéma–Yor embedding and the law of the maximum; an Itô–Tanaka or local-time calculus sufficient for concave functions of Brownian motion and its maximum; the call-price identities of convex analysis; and the analysis of $\mu^{HL}$.

Selected references

• A. Galichon, P. Henry-Labordère, N. Touzi, A stochastic control approach to no-arbitrage bounds given marginals, with an application to lookback options, Ann. Appl. Probab. 24 (2014) 312–336. https://arxiv.org/abs/1401.3921 (v1, the version cited)
• D. Hobson, Robust hedging of the lookback option, Finance Stoch. 2 (1998) 329–347. https://doi.org/10.1007/s007800050046
• J. Azéma, M. Yor, Une solution simple au problème de Skorokhod, Séminaire de Probabilités XIII, LNM 721 (1979) 90–115. https://doi.org/10.1007/BFb0070852
• G. Peskir, Optimal stopping of the maximum process: the maximality principle, Ann. Probab. 26 (1998) 1614–1640. https://doi.org/10.1214/aop/1022855875
• L. Carraro, N. El Karoui, J. Obłój, On Azéma–Yor processes, their optimal properties and the Bachelier–drawdown equation, Ann. Probab. 40 (2012) 372–400. https://arxiv.org/abs/0902.1328

Why sequential portfolios matter

A portfolio manager chooses fractions of current wealth to place in several stocks before seeing that day’s market gains. The gains need not follow a statistical model: a sequence may be selected adversarially, with some stocks losing all value on a given day. A useful benchmark is the best constantly rebalanced portfolio, which holds the same fractions each day but trades at the end of every round to restore them. Its fixed allocation is an active strategy, and it can grow even when buying and holding each individual stock does not. Chapter 10 of Orabona’s online learning text studies guarantees against this benchmark without imposing a positive lower bound or a finite upper bound on nonzero market gains.

The chapter presents a universal portfolio: an allocation determined by a prior distribution over all fixed portfolios and reweighted according to their wealth so far. The mission focuses on the uniform-prior part of Theorem 10.1. It asks for a worst-case logarithmic regret guarantee against every fixed comparator and every admissible market sequence. This is a deterministic guarantee; no distributional assumption about the market enters its statement.

Market and strategy

There are $d\ge2$ stocks and $T\ge1$ rounds. In round $t$, the market supplies a vector $w_t\in\mathbb R_{≥0}^d\setminus\{0\}$ of nonnegative gains. A portfolio is $u\in\Delta^{d-1}$, the simplex of vectors with nonnegative coordinates summing to one. If one unit is invested initially and the allocation stays fixed, its wealth after $T$ rounds is

$$W_T(u)=\prod_{t=1}^{T}\langle w_t,u\rangle.$$

A sequential strategy chooses $x_t\in\Delta^{d-1}$ before seeing $w_t$, and has wealth $W_T=\prod_{t=1}^{T}\langle w_t,x_t\rangle$. The quantity of interest is the difference between the logarithms of benchmark wealth and sequential wealth. A fixed portfolio can have zero wealth when all the stocks it holds have a zero gain on some day; its log wealth is then $-\infty$ in the mathematical convention of the book.

Algorithm 10.1 begins with a prior $F$ on the simplex. Before round $t$, it gives each fixed portfolio $u$ weight proportional to its wealth $W_{t-1}(u)$, and chooses the resulting mean allocation:

$$x_t(i)=\frac{\int_{\Delta^{d-1}}u_i W_{t-1}(u)\,F(du)}{\int_{\Delta^{d-1}}W_{t-1}(u)\,F(du)}.$$

For this mission, $F$ is the uniform probability measure on the simplex. It is represented by Lebesgue measure in the first $d-1$ coordinates, scaled by $(d-1)!$; the final coordinate is one minus their sum. This explicit density fixes what “uniform” means and prevents the prior from being chosen to suit a particular market sequence.

Formalization targets

The goal is the uniform-prior case of Theorem 10.1. With the notation above, for every fixed portfolio of positive wealth,

$$\log W_T(u)-\log W_T \le \log\binom{T+d-1}{d-1} \le (d-1)\left[\log\left(\frac{T}{d-1}+1\right)+1\right].$$

The goal also asserts $W_T>0$, so the algorithm’s logarithmic wealth is defined. The first inequality gives an exact finite-horizon combinatorial bound; the second displays its logarithmic dependence on $T$ for fixed $d$. The book also states a Dirichlet$(1/2,\ldots,1/2)$ prior bound in the same theorem. That companion branch is not among this proposal’s draft items; its gamma-function normalization and integral identities would require a separate audited definition layer. The fixed series title follows the chapter plan, while the goal and milestone list specify the precise scope delivered here.

The attack path records four source statements. Lemma 10.5 bounds a ratio of nonnegative sums by the largest component ratio. Lemma 10.6 reduces a universal portfolio’s wealth ratio to a maximum over sequences of single-stock choices. Theorem 10.4 bounds the size of a type class, the set of sequences with the same empirical fractions of symbols. Equation (10.5) computes the monomial integral under the uniform simplex prior. These statements are from the chapter’s proof of Theorem 10.1; the equation is referred to as an exercise in Problem 10.3.

What the result provides

The theorem ensures that the uniform-prior strategy keeps its log wealth within $O(d\log(1+T/d))$ of the best constantly rebalanced portfolio, while making no bounded-gain assumption. In particular, a stock may have gain zero on one day or a very large gain on another. The guarantee is pathwise: it applies to the realized market vectors, regardless of how they were chosen. For a fixed number of stocks, dividing regret by $T$ therefore gives a vanishing average shortfall in log wealth.

The mathematical result is already proved in the cited text. This mission’s work is to give its exact algorithm, prior measure, combinatorial objects, and finite-horizon constants machine-checked statements and then proofs. The density-based prior, finite type classes, and simplex monomial integrals can also be reused in online aggregation and universal coding developments. The draft statements currently have Lean placeholders for proofs; a successful submission will still require solvers to close them.

Main difficulty

Applying a generic online convex optimization bound to the loss $-\log\langle w_t,x\rangle$ runs into unbounded gradients when a chosen portfolio has small gain. A bound based on one global Lipschitz constant cannot cover the market sequences allowed here. The integral strategy creates a different obstacle: its denominator must be positive at every round, including histories with zero gains for many fixed portfolios. Its uniform prior is a measure on a $(d-1)$-dimensional simplex embedded in $\mathbb R^d$, so ambient $d$-dimensional volume would give it mass zero. A proof must work with the intrinsic coordinate measure and its normalization. The exact binomial coefficient also depends on counting all sequences of one type without losing the boundary cases where some symbol occurs zero times.

Formalization scope

Lean represents a portfolio as a function Fin d → ℝ in Mathlib’s stdSimplex; a market is a one-based sequence of vectors of the same type. The coordinate chart maps $\mathbb R^{d-1}$ into the simplex, and a scaled restricted Lebesgue measure is pushed forward to define the uniform prior. The chart’s measurability is proved in the definition file. Algorithm 10.1 is a componentwise ratio of real integrals, and the main theorem asserts positive realized wealth. All market vectors on rounds $1,\ldots,T$ are nonnegative and nonzero. The parameter restrictions $d\ge2$ and $T\ge1$ make the dimension and printed denominators meaningful.

For Lemma 10.5, quotients use extended nonnegative reals, with $a/0=+\infty$ when $a>0$ and $0/0=0$ as printed. Lemma 10.6 is stated for a generic prior concentrated on the simplex, with its ratios in extended nonnegative reals under the same conventions, and with the hypothesis that the normalizing integral of Algorithm 10.1 is positive in every round, which is what makes the algorithm's prediction defined. A comparator with zero wealth is omitted only from the real-log statement, corresponding to log wealth $-\infty$ in the source. The prior cannot be replaced by an arbitrary point mass: the theorem names the chart-based uniform measure, and the prediction is the exact integral ratio. Contributions proving normalization, support, the integral identity, and the final regret bound are all within scope.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 10 and Appendix A.2.2. arXiv

Motivation

The asymmetric traveling salesman problem (ATSP) asks for a shortest closed walk through every vertex of a directed graph whose edge weights need not be symmetric. It models routing with one-way streets, scheduling with sequence-dependent setup times, and many other problems in which the cost of going from $u$ to $v$ differs from the cost of going back. Its standard linear relaxation, the asymmetric Held–Karp relaxation, is the lower bound used both by exact branch-and-cut codes and by approximation algorithms, and the central question about it is how far it can be from the integer optimum.

Timeline of the approximation ratio and of the integrality gap for ATSP:

• 1982: Frieze, Galbiati and Maffioli give a $\log_2 n$-approximation by repeated cycle covers.
• 2010: Asadpour, Goemans, Mądry, Oveis Gharan and Saberi reach $O(\log n/\log\log n)$ via thin trees (SODA 2010).
• 2015: Anari and Oveis Gharan bound the integrality gap by $\mathrm{poly}(\log\log n)$, non-constructively; Svensson obtains a constant factor for node-weighted digraphs.
• 2018: Svensson, Tarnawski and Végh obtain the first constant-factor approximation for general ATSP (STOC 2018); the journal version (J. ACM 2020) states the ratio $506$ and the integrality gap bound $319$.
• 2020: Traub and Vygen improve the ratio to $22+\varepsilon$ and the gap to $22$ (STOC 2020).

The lower bound on the integrality gap remains $2$ (Charikar, Goemans and Karloff, 2006).

Setting

A digraph $G=(V,E)$ has finite vertex and edge sets; each edge has a tail and a head, and parallel edges and loops are allowed. For $S\subseteq V$, $\delta^+(S)$ and $\delta^-(S)$ are the edges leaving and entering $S$, and $\delta(S)=\delta^+(S)\cup\delta^-(S)$. An ATSP input is a strongly connected digraph $G$ with a weight function $w:E\to\mathbb R_{\ge0}$.

An edge multiset $F$ gives each edge a multiplicity $F(e)\in\mathbb N$; $V(F)$ is the set of vertices it touches. $F$ is Eulerian if every vertex has as many outgoing as incoming edges of $F$, a subtour if moreover $(V(F),F)$ is connected, and a tour if it is a subtour with $V(F)=V$. Tours are exactly the closed walks visiting every vertex. The weight of $F$ is $\sum_e F(e)w(e)$.

The asymmetric Held–Karp relaxation LP$(G,w)$ is

$$\min\sum_{e\in E}w(e)x(e)\quad\text{s.t.}\quad x(\delta^+(v))=x(\delta^-(v))\ (v\in V),\qquad x(\delta(S))\ge2\ (\emptyset\ne S\subsetneq V),\qquad x\ge0,$$

and its optimum is the Held–Karp lower bound.

The mission also uses the paper's intermediate objects: laminarly-weighted instances $I=(G,\mathcal L,x,y)$, in which $\mathcal L$ is a laminar family of sets that are tight for a strictly positive feasible $x$, $y\ge0$ on $\mathcal L$, and the weight of an edge is $w_I(e)=\sum_{S\in\mathcal L:\,e\in\delta(S)}y_S$; the value $\mathrm{value}(I)=2\sum_{S\in\mathcal L}y_S$ and the lower bound $\mathrm{lb}_I(U)=\sum_{v\in U}2y_{\{v\}}$; Subtour Partition Cover and $(\alpha,\beta)$-lightness; irreducible instances; vertebrate pairs; and quasi-backbones. Each is defined, with the paper's page reference, in the two definition files of the mission.

Formalization targets

Goal: Theorem 11.1

For every strongly connected digraph $G$ with $|V|\ge2$, every $w\ge0$ and every feasible solution $x$ of LP$(G,w)$, there is a tour $F$ with

$$\sum_{e\in E}F(e)\,w(e)\ \le\ 319\sum_{e\in E}w(e)\,x(e).$$

This is the statement that the integrality gap of the asymmetric Held–Karp relaxation is at most $319$.

Milestones

The milestones are the results the paper's §11 combines, in the order it combines them:

1. Theorem 4.1: Subtour Partition Cover is $(2,0)$-light on singleton instances with $B=\emptyset$.
2. Theorem 5.1: an $(\alpha,\beta)$-light pair $(I,B)$ has a tour of weight at most $5\alpha\,\mathrm{lb}_I(\bar B)+\beta+w_I(B)$.
3. §11: every singleton instance has a tour of weight at most $10\,\mathrm{value}(I)$ ($\alpha'_S=10$).
4. Theorem 10.1: vertebrate pairs are $(4,\,2\,\mathrm{value}(I)+\mathrm{lb}_I(\bar B))$-light.
5. §11: a vertebrate pair has a tour of weight at most $2\,\mathrm{value}(I)+21\,\mathrm{lb}_I(\bar B)+w_I(B)$ ($\eta'=1+5\cdot4$).
6. Lemma 9.3: an irreducible instance has a quasi-backbone of weight at most $(\alpha_S+3)\,\mathrm{value}(I)$.
7. Theorem 9.4: tours on vertebrate pairs give a $\rho$-bound on irreducible instances, $\rho=\frac{\kappa+\eta(1-\delta)+\alpha_S+3}{2\delta-1}$.
8. Theorem 8.3: a $\rho$-bound on irreducible instances gives a $\frac{2\rho}{1-\delta}$-bound on all laminarly-weighted instances.
9. Lemma 2.2: DUAL$(G,w)$ has an optimal solution with laminar support.
10. Theorem 2.4: a bound $\alpha\,\mathrm{value}(I)$ on all laminarly-weighted instances gives $\alpha$ times the Held–Karp bound on all ATSP inputs.

Significance

The result shows that the asymmetric Held–Karp relaxation approximates ATSP within a constant factor, which settled a question open since the 1980s and made the relaxation a certified lower bound with bounded loss. The structural steps (reduction to laminarly-weighted instances, Subtour Partition Cover, irreducibility and vertebrate pairs) are the framework on which the later improvement to $22$ by Traub and Vygen is built.

The theorem is proved; to the best of available knowledge none of it has been formalized in a proof assistant. A complete development would give a machine-checked bound on the integrality gap of a central relaxation in combinatorial optimization, and its intermediate statements are reusable for the improved bounds that follow the same framework.

Difficulty

The obvious approaches do not give a constant. Repeated cycle covers lose a factor at each of logarithmically many rounds. Rounding the LP solution through thin trees needs a spanning tree that is thin in every cut, and only polylogarithmic thinness is known. The paper's route is long: the reduction to laminarly-weighted instances needs an uncrossed dual; the reduction from irreducible to general instances and the one from vertebrate pairs to irreducible instances are recursive, applying the assumed algorithm to instances built by contracting or inducing tight sets, so their hypotheses must hold on all instances and not only on the given one; and the lightness bound for vertebrate pairs (Theorem 10.1) rests on a flow-based construction with careful accounting against the laminar family.

Formalization scope

Vertices and edges are finite types; edges carry tail and head maps, so parallel edges (created by contraction) are distinct edges, and loops are allowed and lie in no cut. Edge multisets are functions $E\to\mathbb N$. Connectivity of a multiset and its components are defined by the reflexive–transitive closure of undirected adjacency along its edges.

Running times are not formalized. Every algorithmic statement is posed in its existential form, as §11 of the paper itself uses it to derive Theorem 11.1: "there is an algorithm returning a tour within $c$" becomes "every instance has a tour within $c$", and an assumed algorithm becomes a hypothesis quantified over instances on all finite vertex and edge types. The algorithmic constants $9(1+\varepsilon)$, $18+\varepsilon$, $37+36\varepsilon$ and $506$ are therefore not stated; the non-constructive constants $5$, $10$ and $21$ of §11 are.

The Held–Karp lower bound is never defined as an infimum: comparisons with it are stated for every feasible $x$, equivalently because the LP optimum is attained. Likewise $d_S$ and $D_S$ in the definition of irreducibility are expressed through walks, without an infimum.

Added hypotheses, each disclosed in the item's Formalization Note:

• $|V|\ge2$ in the goal, Theorem 2.4 and every laminarly-weighted instance: on one vertex without a loop no tour exists while LP$(G,w)$ has value $0$.
• Partition parts in Subtour Partition Cover are nonempty and different from $V$; for $B=\emptyset$ the one-part partition $(V)$ admits no solution.
• $\alpha\ge0$ in Theorem 5.1, which is false without it.
• $\alpha_S$ in Lemma 9.3 and Theorem 9.4 is a parameter with the hypothesis that singleton instances have tours within $\alpha_S\,\mathrm{value}$, instead of the fixed $18+\varepsilon$.

These choices rule out trivializing formalizations: no instance class in a hypothesis is empty (a two-vertex singleton instance is valid, irreducible and vertebrate), admissible partitions exist for every instance, and LP$(G,w)$ is feasible for every strongly connected input. The goal assumes none of the milestones.

Out of scope: the polynomial running times, §5's merge-procedure lemmas, the constructions of §7, and Corollaries 11.2–11.4 on the path version, which rest on external reductions. Contributions are welcome on every milestone, and on infrastructure that a complete development needs: LP duality and uncrossing for cut LPs, Eulerian multigraphs and their decomposition into closed walks, and circulations with lower bounds (Hoffman's theorem). The platform's proved LP strong duality (SmaleNinth.lp_strong_duality) is a natural starting point for Lemma 2.2.

Selected references

• O. Svensson, J. Tarnawski, L. A. Végh, A constant-factor approximation algorithm for the asymmetric traveling salesman problem, J. ACM 67(6), 2020. https://doi.org/10.1145/3424306 (accepted manuscript: LSE Research Online 106582, https://eprints.lse.ac.uk/106582/)
• O. Svensson, J. Tarnawski, L. A. Végh, A constant-factor approximation algorithm for the asymmetric traveling salesman problem, STOC 2018. https://doi.org/10.1145/3188745.3188824
• V. Traub, J. Vygen, An improved approximation algorithm for ATSP, STOC 2020. https://arxiv.org/abs/1912.00670
• A. Asadpour, M. X. Goemans, A. Mądry, S. Oveis Gharan, A. Saberi, An O(log n/log log n)-approximation algorithm for the asymmetric traveling salesman problem, SODA 2010. https://doi.org/10.1137/1.9781611973075.32
• A. M. Frieze, G. Galbiati, F. Maffioli, On the worst-case performance of some algorithms for the asymmetric traveling salesman problem, Networks 12(1), 1982. https://doi.org/10.1002/net.3230120103
• M. Charikar, M. X. Goemans, H. Karloff, On the integrality ratio for the asymmetric traveling salesman problem, Math. Oper. Res. 31(2), 2006. https://doi.org/10.1287/moor.1050.0172

Motivation

Many platforms match two sides of a market over time: ride-hailing platforms match riders with drivers, blood banks match donated units with patients, organ allocation matches donors with recipients, and retailers pool inventory across fulfilment centres to serve orders from several regions. Demand and supply arrive in several types (locations, blood groups, quality grades), the reward of a match depends on both types, and whatever is not matched today partly waits for tomorrow. A central operational question is which pairs to match first. Static versions of this question go back to the transportation problem and to Monge sequences: Hoffman (1963) characterized the cost matrices for which a fixed greedy order of the arcs solves a transportation problem.

Hu and Zhou (arXiv:1811.07048, published in Manufacturing & Service Operations Management 24(1), 2022) extend this to a stochastic, multi-period setting. They identify conditions on the rewards, the (weak) modified Monge conditions, under which an optimal dynamic policy matches a dominant pair before the neighbouring pairs it dominates. This mission formalizes their main structural result, Theorem 1, and the chain of results it rests on.

Setting

There are $m$ demand types $\mathcal D=\{1,\dots,m\}$, $n$ supply types $\mathcal S=\{1,\dots,n\}$, and $T$ periods $t=1,\dots,T$. In period $t$ the state is a pair of vectors $(\mathbf x,\mathbf y)\in\mathbb R^m_+\times\mathbb R^n_+$ of available demand and supply. The firm chooses a matching decision $\mathbf Q=(q_{ij})\in\mathbb R^{m\times n}$, collecting the reward

$$\mathbf R^t\circ\mathbf Q=\sum_{i=1}^m\sum_{j=1}^n r^t_{ij}q_{ij},$$

where the rewards $r^t_{ij}$ are arbitrary real numbers. The post-matching levels are $u_i=x_i-\sum_j q_{ij}$ and $v_j=y_j-\sum_i q_{ij}$, and $\mathbf Q$ is feasible if $\mathbf Q\ge0$, $\mathbf u\ge0$ and $\mathbf v\ge0$. A fraction $\alpha\in[0,1]$ of unmatched demand and $\beta\in[0,1]$ of unmatched supply carries over, and new random quantities $(\mathbf D^{t+1},\mathbf S^{t+1})\ge0$ arrive. The value function $V_t$ is defined by the dynamic program

$$V_t(\mathbf x,\mathbf y)=\max_{\mathbf Q\ \text{feasible}}H_t(\mathbf Q,\mathbf x,\mathbf y),\qquad H_t(\mathbf Q,\mathbf x,\mathbf y)=\mathbf R^t\circ\mathbf Q+\mathbb E\,V_{t+1}(\alpha\mathbf u+\mathbf D^{t+1},\beta\mathbf v+\mathbf S^{t+1}),$$

with $V_{T+1}\equiv0$. A matching policy assigns a feasible decision $\mathbf Q^t(\mathbf x,\mathbf y)$ to every period and state; it is optimal if each of these decisions maximizes $H_t$.

Two neighbouring pairs are compared by the relation $\succ_{\mathcal M}$. For $i'\ne i$, $(i,j)\succ_{\mathcal M}(i',j)$ means $r^t_{ij}>r^t_{i'j}$ for all $t$, and $r^t_{ij}-r^t_{i'j}\ge\alpha(r^{t+1}_{ij''}-r^{t+1}_{i'j''})$ for all $t\le T-1$ and all $j''$; the relation $(i,j)\succ_{\mathcal M}(i,j')$ is defined symmetrically with $\beta$. The modified Monge condition requires $r^t_{ij}+r^t_{i'j'}\ge r^t_{ij'}+r^t_{i'j}$ whenever $(i,j)$ dominates both $(i',j)$ and $(i,j')$; the paper then writes $\succ_{\mathcal M_s}$. For a pair $(i,j)$, let $a_i$ be the type-$i$ demand left after matching $i$ through all pairs that $(i,j)$ does not dominate, and $b_j$ the analogous supply residual. A decision respects $\succ_{\mathcal M_s}$ if $(i,j)\succ(i',j)$ implies $q_{i'j}=0$ or $a_i=0$, and $(i,j)\succ(i,j')$ implies $q_{ij'}=0$ or $b_j=0$.

Formalization targets

Goal: Theorem 1 (p. 12)

Under the modified Monge condition there is a single policy $P$ such that, for all $1\le t\le T$ and all $\mathbf x,\mathbf y\ge0$,

$$P_t(\mathbf x,\mathbf y)\ \text{is optimal}\quad\text{and}\quad P_t(\mathbf x,\mathbf y)\ \text{respects}\ \succ_{\mathcal M_s}.$$

Milestones

• Proposition 1 (p. 10): $V_t$ and $H_t$ are continuous and concave, and an optimal policy exists.
• Lemma A.1 (Online Appendix A, p. 1): shifting $\varepsilon$ units of demand from type $i$ to type $i'$ (or of supply from $j$ to $j'$) changes $V_t$ by at least $-\sum_\tau\sum_{j'}\lambda^\tau_{j'}(r^\tau_{ij'}-r^\tau_{i'j'})$ for some nonnegative multipliers with $\sum_\tau\alpha^{-(\tau-t)}\sum_{j'}\lambda^\tau_{j'}\le\varepsilon$.
• Lemma A.2 (p. 3): transferring matching quantity from a dominated pair to a dominant one weakly increases $H_t$.
• Theorem 2 (p. 28): without the Monge condition, some optimal policy weakly respects $\succ_{\mathcal M}$: $q_{i'j}=0$ or $u_i=0$, and $q_{ij'}=0$ or $v_j=0$.
• Monge exchange (proof of Theorem 1, p. 4): the transfer $\mathbf Q+\varepsilon(\mathbf e_{ij}+\mathbf e_{i'j'}-\mathbf e_{i'j}-\mathbf e_{ij'})$ stays feasible and weakly increases $H_t$.
• Properties (i)–(iii) imply compatibility (proof of Theorem 1, p. 5).

Significance

Theorem 1 replaces the search over all optimal policies, which are state-dependent and generally complex, by a priority structure: whenever $(i,j)$ dominates a neighbour, the neighbour is matched only once the residual capacity of $(i,j)$ is exhausted. The paper derives from it the optimality of greedy matching for "perfect" pairs (Proposition 2), the priority order for horizontal (distance-based) and vertical (quality-based) reward structures, and the match-down-to threshold structure of the optimal policy in those models. These results generalize inventory rationing and capacity allocation with upgrading.

The result is proved in the paper, but not completely: the limit argument in the printed proofs of Theorems 1 and 2 ("the quantity transferred converges to zero") is not justified, and Proposition 1 has no printed proof in this version. A machine-checked development would close these gaps and would provide a reusable finite-horizon model with continuous states, concave value functions and an exchange-argument toolkit. No part of this mission is known to be formalized.

Difficulty

The obvious argument starts from an optimal decision and repeatedly applies the transfers of Lemma A.2 and the Monge exchange. Each transfer preserves optimality, but nothing in the printed argument guarantees that the procedure terminates or that its limit has the required property: transfers of different kinds can undo each other's progress, and with equal rewards they can cycle forever. A complete proof has to select the right optimal decision without relying on such an iteration. Before that, the dynamic program itself needs care: the value function is a supremum of an expectation of the next value function, so continuity, concavity, measurability and integrability have to be established together by backward induction, and attainment of the maximum is needed for any optimal policy to exist. Lemma A.1 is a further backward induction in which the multipliers become random and must be averaged.

Formalization scope

The Lean development lives in the namespace DynTypeMatching.Priority. Types are Fin m and Fin n; states are Fin m → ℝ, Fin n → ℝ; decisions are Fin m → Fin n → ℝ. Periods are natural numbers with the paper's 1-based indexing, and $V_t=0$ for $t>T$. A model Model m n carries $T$, the rewards, $\alpha$, $\beta$ and one arrival law per period on $\mathbb R^m\times\mathbb R^n$. The paper permits exogenous correlation between periods; its recursion (1) uses per-period laws and does not specify a joint arrival process. The expectation in $H_t$ is over the law of the arrivals entering period $t+1$.

Every result assumes Model.WellPosed: each arrival law is a probability measure, supported on the nonnegative orthant and integrable, and $0\le\alpha,\beta\le1$. Integrability is not stated in the paper, but without it the expectation in (1) is undefined. The value function is a real supremum and the expectation a Bochner integral, so outside the nonnegative orthant, or for non-integrable integrands, Lean returns the junk value 0. All statements therefore quantify over nonnegative states and feasible decisions.

The following hypotheses are added relative to the page, and each is disclosed in the item where it occurs:

• Definition 1(i) is strict, $r^t_{ij}>r^t_{i'j}$, and the neighbours are distinct. With the printed weak inequality, Theorems 1 and 2 are false. Take $m=3$, $n=1$, $T=1$, all rewards equal to 2, $\mathbf x=(0,1,1)$, $\mathbf y=(1)$. Then types 2 and 3 dominate each other, every optimal decision matches one unit, and no such decision respects the relation.
• Definition 1(ii) is required only for $t+1\le T$, because $r^{T+1}$ is not part of the model.
• Lemma A.1 assumes $\alpha>0$ in part (i) and $\beta>0$ in part (ii), because $\alpha^{-(\tau-t)}$ is undefined at $\alpha=0$.
• Lemma A.2 assumes that $\mathbf Q$ itself is feasible.

Several printed index slips are corrected: the doubled $\varepsilon\mathbf e_{ij}$ in the Monge exchange, the index ranges in Lemma A.1, and "and" for "or" in the compatibility step.

An optimal decision is defined as a feasible maximizer of $H_t$ over feasible decisions, not through the equation $V_t=H_t$. This rules out a trivializing reading of the goal: a decision that respects the relation but is not optimal (for instance $\mathbf Q=0$) does not satisfy it. The goal asserts one policy that is optimal and compatible at the same time.

A complete development needs measurable-function and Bochner-integral calculus on finite-dimensional spaces, concavity and continuity of parametric suprema over polytopes, and compactness arguments for attainment. The model and the exchange lemmas are reusable for later missions on this paper (greedy matching, horizontal and vertical models). Proofs of any milestone are welcome, and so are alternative proofs of the goal.

Selected references

• Ming Hu, Yun Zhou, Dynamic Type Matching, arXiv:1811.07048v1, 2018; Manufacturing & Service Operations Management 24(1), 2022. https://arxiv.org/abs/1811.07048 · https://doi.org/10.1287/msom.2020.0952
• Alan J. Hoffman, On simple linear programming problems, Convexity, Proc. Symposia in Pure Mathematics 7, AMS, 1963, 317–327. https://doi.org/10.1090/pspum/007/0157783
• Rainer E. Burkard, Bettina Klinz, Rüdiger Rudolf, Perspectives of Monge properties in optimization, Discrete Applied Mathematics 70(2), 1996, 95–161. https://doi.org/10.1016/0166-218X(95)00103-X

Motivation

Makespan minimization on identical parallel machines, $P\|C_{\max}$, asks to assign $n$ jobs with processing times to $m$ machines so that the largest machine load is as small as possible. It is strongly NP-hard, and the question has long been how fast a $(1+\varepsilon)$-approximate schedule can be found. After rounding and scaling, a guess $T$ of the optimal makespan becomes a constant, the job sizes take only $d = O((1/\varepsilon)\log(1/\varepsilon))$ distinct values, and the problem becomes an integer program over machine packings: the configuration IP.

A short history of the running times for this problem:

• Hochbaum and Shmoys (1987) gave the first PTAS, with running time $(n/\varepsilon)^{O(1/\varepsilon^2)}$.
• Alon, Azar, Woeginger and Yadid (1997/1998), and Hochbaum and Shmoys, obtained an EPTAS with running time $2^{(1/\varepsilon)^{\mathrm{poly}(1/\varepsilon)}} + O(n\log n)$.
• Jansen (2010) used the support bound of Eisenbrand and Shmonin (2006) to reach $2^{O((1/\varepsilon)^2\log^3(1/\varepsilon))} + O(n\log n)$.
• Chen, Jansen and Zhang (2014) showed that, under the Exponential Time Hypothesis, no PTAS runs in time $2^{(1/\varepsilon)^{1-\delta}}\mathrm{poly}(n)$.
• Jansen, Klein and Verschae (arXiv 2016; Mathematics of Operations Research 2020) reached $2^{O((1/\varepsilon)\log^4(1/\varepsilon))} + O(n\log n)$, matching that lower bound up to polylogarithmic factors in the exponent. Their key ingredient is a structural theorem on the configuration IP, which this mission formalizes.

Setting

Fix $d \in \mathbb{N}$, a vector of job sizes $\pi \in \mathbb{Z}^d_{>0}$ and a capacity $T \in \mathbb{Z}_{>0}$. The knapsack polytope is $\mathcal{P} = \{c \in \mathbb{R}^d_{\ge 0} : \pi\cdot c \le T\}$, and a configuration is an integral point of it:

$$Q = \mathbb{Z}^d \cap \mathcal{P}, \qquad c \in Q \iff c \in \mathbb{Z}^d_{\ge 0},\ \ \sum_{k} \pi_k c_k \le T.$$

A configuration describes one machine: $c_k$ jobs of size $\pi_k$, of total load at most $T$. The support of a vector is the set of its nonzero coordinates, $\operatorname{supp}(c) = \{k : c_k \ne 0\}$. Throughout, $\log = \log_2$. A configuration is simple if $|\operatorname{supp}(c)| \le \log(T+1)$ and complex otherwise; $Q_c$ is the set of complex configurations.

Given the number $b_k$ of jobs of each size and the number $m$ of machines, the configuration IP [conf-IP] asks for multiplicities $x_c \in \mathbb{Z}_{\ge 0}$, one per configuration, with

$$\sum_{c\in Q} c\, x_c = b, \qquad \sum_{c \in Q} x_c = m.$$

Its LP relaxation [conf-LP] replaces $x_c \in \mathbb{Z}_{\ge 0}$ by $x_c \ge 0$. The support of a solution is $\operatorname{supp}(x) = \{c \in Q : x_c \neq 0\}$.

Formalization targets

Goal: thin solutions (Theorem 1)

If [conf-IP] is feasible, it has a feasible solution $x$ with

$$x_c > 1 \Rightarrow c \text{ simple}, \qquad |\operatorname{supp}(x)| \le 4(d+1)\log(4(d+1)T), \qquad \sum_{c\in Q_c} x_c \le 2(d+1)\log(4(d+1)T).$$

A solution with these three properties is called thin.

Milestones

1. Lemma 2 (Eisenbrand–Shmonin): if $|\operatorname{supp}(x)| > 2(d+1)\log(4(d+1)T)$ for a nonnegative integer vector $x$ on $Q$, there are disjoint nonempty $A, B \subseteq \operatorname{supp}(x)$ with $\sum_{c \in A} c = \sum_{c\in B} c$ and $|A| = |B|$.
2. Lemma 3 (Eisenbrand–Shmonin): a feasible [conf-IP] has a solution with $|\operatorname{supp}(x)| \le 2(d+1)\log(4(d+1)T)$.
3. Lemma 4 (Sparsification Lemma): every complex $c \in Q$ satisfies $2c = c_1 + c_2$ for configurations $c_1, c_2$ with $\pi\cdot c_1 = \pi\cdot c_2 = \pi\cdot c$ and $\operatorname{supp}(c_i) \subsetneq \operatorname{supp}(c)$.
4. P1: a feasible solution minimizing the potential $\Phi(x) = \sum_{c \text{ complex}} x_c|\operatorname{supp}(c)|$ uses each complex configuration at most once.
5. P2: such a solution has at most $2(d+1)\log(4(d+1)T)$ complex configurations in its support.

Companion results

• Corollary 5: every vertex of $\operatorname{conv.hull}(Q)$ is a simple configuration; and, from its proof, the number of simple configurations is at most $(L+1)d^{L}(T+1)^{L}$ with $L = \log(T+1)$, for $d \ge 1$.
• Corollary 6: a feasible [conf-LP] has a solution supported on simple configurations only.

Significance

The result. Theorem 1 says that, up to $O(d\log(dT))$ machines, every feasible configuration IP can be solved using simple configurations only. There are $2^{O(\log^2 d + \log^2 T)}$ simple configurations, far fewer than configurations in general, so an algorithm can guess the support of a solution among a much smaller family. This is what yields the $2^{O((1/\varepsilon)\log^4(1/\varepsilon))} + O(n\log n)$ EPTAS for $P\|C_{\max}$, and through the same structure PTASs for $Q\|C_{\max}$ and for $L_p$-norm and max–min objectives. Corollaries 5 and 6 are structural facts about knapsack polytopes in their own right: the integer hull has only simple vertices, and the configuration LP can be restricted to simple configurations.

Formalizing it. The results are proved in the paper; none of them has a machine-checked proof that this mission knows of. The development produces a reusable formal model of configurations and of the configuration IP and LP, a formal Eisenbrand–Shmonin support bound for this IP (a Carathéodory-type statement for integer cones that recurs across integer programming), and the sparsification lemma with its potential-function argument. The constants $4(d+1)$ and $2(d+1)$ are the paper's and are stated exactly.

Difficulty

The obvious argument applies the sparsification lemma repeatedly, replacing any complex configuration used twice by two configurations of smaller support, and then shrinks the support with the Eisenbrand–Shmonin exchange. The second step can undo the first: the exchange moves weight between configurations and may raise the multiplicity of a complex configuration above one again, so alternating the two steps has no evident termination measure. A proof has to control both properties at once. The counting behind the support bound needs the explicit inequality $(sT+1)^{d+1} < 2^s$ for every $s > 2(d+1)\log(4(d+1)T)$, which must be carried out with the exact constants rather than up to $O(\cdot)$.

Formalization scope

• Configurations are functions Fin d → ℕ with $\sum_k \pi_k c_k \le T$; solutions of [conf-IP] are finitely supported functions (Fin d → ℕ) →₀ ℕ vanishing outside $Q$, and solutions of [conf-LP] are finitely supported real-valued functions, nonnegative and vanishing outside $Q$.
• The standing assumptions of §2 are binders of every statement: $\pi_k > 0$ for all $k$ and $T > 0$. Lemma 4 does not need $T > 0$ and omits it.
• The paper writes $b \in \mathbb{R}^d$ for [conf-IP]; feasibility forces $b \in \mathbb{N}^d$, so $b$ and $m$ are natural numbers. For [conf-LP] they are real.
• $\log$ is Real.logb 2 and every bound is a real inequality; no floor is taken.
• In Lemma 2, $Mx^A = Mx^B$ is stated row by row: the sum of the configurations in $A$ equals that in $B$, and $|A| = |B|$.
• "Minimum potential" in P1 and P2 means $\Phi(x) \le \Phi(y)$ for every feasible solution $y$ of the same instance.
• A vertex of $\operatorname{conv.hull}(Q)$ is an extreme point (Mathlib's Set.extremePoints). The asymptotic count of Corollary 5 is replaced by the explicit bound of its proof, with the added hypothesis $d \ge 1$ (at $d = 0$ the explicit bound is $0$ while $Q = \{0\}$).

The goal theorem refers only to [conf-IP], its solutions, supports and the simple/complex split; it does not mention the potential, the matrix $M$ or a minimality assumption, so it cannot be discharged by choosing a special solution in the hypotheses.

Needed infrastructure: finite sums over Finsupp, the pigeonhole principle on finsets, elementary bounds on Real.logb, and, for Corollaries 5 and 6, convex hulls and extreme points of finite sets in $\mathbb{R}^d$. The definitions of configurations and of the configuration IP/LP are reusable for other configuration-IP papers (bin packing, cutting stock, scheduling). Contributions of auxiliary lemmas on supports of integer conic combinations are welcome.

Selected references

• K. Jansen, K.-M. Klein, J. Verschae, Closing the Gap for Makespan Scheduling via Sparsification Techniques, ICALP 2016; Mathematics of Operations Research, 2020. https://arxiv.org/abs/1604.07153 (version v1, the basis of every citation in this mission)
• F. Eisenbrand, G. Shmonin, Carathéodory bounds for integer cones, Operations Research Letters 34, 564–568, 2006. https://doi.org/10.1016/j.orl.2005.09.008
• K. Jansen, An EPTAS for scheduling jobs on uniform processors: using an MILP relaxation with a constant number of integral variables, SIAM Journal on Discrete Mathematics 24, 457–485, 2010.
• N. Alon, Y. Azar, G. J. Woeginger, T. Yadid, Approximation schemes for scheduling on parallel machines, Journal of Scheduling 1, 55–66, 1998.
• D. S. Hochbaum, D. B. Shmoys, Using dual approximation algorithms for scheduling problems: theoretical and practical results, Journal of the ACM 34, 144–162, 1987. https://doi.org/10.1145/7531.7535
• L. Chen, K. Jansen, G. Zhang, On the optimality of approximation schemes for the classical scheduling problem, Proceedings of the 25th ACM-SIAM Symposium on Discrete Algorithms (SODA), 657–668, 2014.

Motivation

A seller with several goods and a single buyer is the smallest setting in which multi-dimensional mechanism design differs from the one-good theory. For one good, Myerson's theorem (Myerson 1981) says the optimal mechanism posts a price. For two or more goods the optimal mechanism may use lotteries, may be non-monotone in the buyer's values, and is in general not known in closed form. Practitioners nevertheless use simple mechanisms, and the question that Hart and Nisan (arXiv:1204.1846v3) ask is quantitative: what fraction of the optimal revenue does a simple mechanism guarantee?

This mission concerns the simplest mechanism of all, bundling: one posted price for the set of all goods. When the goods are independent and identically distributed, bundling is known to become nearly optimal as the number of goods grows for a fixed distribution (Armstrong 1999; Bakos and Brynjolfsson 1999). That limit is not uniform over distributions. Theorem D of Hart and Nisan gives the uniform guarantee: for every $k\ge2$ and every distribution, bundling $k$ i.i.d. goods earns at least $c/\log k$ of the optimal revenue.

Timeline. Armstrong (1999) and Bakos–Brynjolfsson (1999) proved the asymptotic optimality of bundling for a fixed distribution. Hart and Nisan circulated the first version of this paper in 2012 (EC 2012), proving Theorems A–D; the version formalized here is arXiv:1204.1846v3 (2017), published in J. Econ. Theory 172 (2017). Li and Yao (2013) later improved separate selling for i.i.d. goods to $\Theta(1/\log k)$, and Babaioff, Immorlica, Lucier and Weinberg (2014) showed that the better of separate selling and bundling is a constant-factor approximation for independent goods.

Setting

There are $k$ goods and one buyer with additive valuation $x=(x_1,\dots,x_k)\in\mathbb R_+^k$, drawn from a known distribution. A mechanism $\mu=(q,s)$ assigns to every reported valuation $x$ an allocation vector $q(x)\in[0,1]^k$ (the probabilities of receiving each good) and a payment $s(x)\in\mathbb R$. The buyer's payoff is $b(x)=q(x)\cdot x-s(x)$. The mechanism is incentive compatible (IC) if $b(x)\ge q(\tilde x)\cdot x-s(\tilde x)$ for all $x,\tilde x$, and individually rational (IR) if $b(x)\ge0$ for all $x$. For a random valuation $X$, the expected revenue is $R(\mu;X)=\mathbb E[s(X)]$ and the optimal revenue is

$$\mathrm{Rev}(X)=\sup\{R(\mu;X):\ \mu\text{ IC and IR}\}\in[0,\infty].$$

For one good, $\mathrm{Rev}(X)=\sup_{p\ge0}p\cdot\mathbb P[X\ge p]$. The bundled revenue is the one-good revenue of the total value, $\mathrm{BRev}(X)=\mathrm{Rev}(X_1+\dots+X_k)$, and the separate revenue is $\mathrm{SRev}(X)=\sum_i\mathrm{Rev}(X_i)$.

"$k$ i.i.d. goods" means that $X_1,\dots,X_k$ are independent with a common law $\nu$ on $\mathbb R_+$. Write $R_k=\mathrm{Rev}(X_1,\dots,X_k)$ and $B_k=\mathrm{BRev}(X_1,\dots,X_k)$.

Two auxiliary objects appear in the milestones. A real random variable $X$ is stochastically dominated by $Y$ if $\mathbb P[X\ge p]\le\mathbb P[Y\ge p]$ for every $p$. The equal-revenue (ER) law is that of $V\ge1$ with $\mathbb P[V\ge p]=1/p$ for $p\ge1$. The constant $w\approx0.278$ is the unique real solution of $w\,e^{w+1}=1$.

Formalization targets

Goal: Theorem D (p. 7)

$$\exists\,c>0\ \ \forall k\ge2\ \ \forall\nu:\qquad \frac{c}{\log k}\,R_k\le B_k .$$

The constant is absolute: it is chosen before $k$ and before the distribution. This is the statement as printed; it fixes neither the constant nor the base of the logarithm.

Explicit form (proof of Theorem D, p. 27)

$$R_k\le 8(w+1)(\log_2k+2)\,B_k\qquad(k\ge2).$$

Milestones

The milestones follow the paper's proof: Myerson's formula (1); monotonicity of one-good revenue under domination (Proposition 11); the ER characterization (Lemma 20) and the tail of a weighted sum of two ER goods (Lemma 21); $\mathrm{BRev}(V_1,V_2)=2(w+1)$ (Proposition 24); $\mathrm{SRev}\ge\mathrm{BRev}/(w+1)$ for two independent goods (Proposition 13 (i)); $\mathrm{BRev}\ge\mathrm{SRev}/4$ for i.i.d. goods (Proposition 14 (ii)); the decomposition Theorem 7; the power-of-two bound $R_k\le4(\log_2k+1)B_k$; monotonicity of $R_k$ and $B_k$ in $k$; and the explicit bound above.

Significance

Theorem D says that for identically distributed goods the gap between the simplest mechanism and the optimal one grows at most logarithmically in the number of goods, uniformly over all distributions, including heavy-tailed ones with infinite mean. The i.i.d. hypothesis is essential: for independent goods with different distributions bundling can recover only a $1/k$ fraction (Example 27 of the paper). Together with Theorem C (separate selling, $c/\log^2k$) it places the two simple mechanisms on a common scale, and the decomposition Theorem 7 it rests on is a general tool for independent groups of goods.

The result is proved in the paper; no machine-checked version is known to exist. A formalization adds: a Lean model of multi-good mechanisms with IC, IR and expected revenue in the extended reals; a checked version of Myerson's one-good formula for arbitrary laws on $\mathbb R_+$; the equal-revenue law and its two-good convolution; and a checked reduction from the decomposition theorem to the logarithmic bundling guarantee. Shorter arguments or a better constant are also welcome.

Difficulty

The obvious argument fails at the first step: revenue is not monotone in the valuation for two or more goods (Hart and Reny 2015), so one cannot bound $R_k$ by replacing each good by a dominating ER good. Every comparison therefore has to pass through one-dimensional quantities, and the multi-good step (Theorem 7) is a statement about expectations of a mechanism's payments conditioned on an independent block of goods. Proposition 14 (ii) must handle distributions where no optimal one-good price exists and $\mathrm{Rev}(X_i)$ may be infinite (the paper's proof speaks of "an optimal price"). Proposition 24 is an exact evaluation whose answer is defined only implicitly, through $w\,e^{w+1}=1$. The induction itself must track how block sums of i.i.d. goods are again i.i.d.

Formalization scope

Valuations are laws: a $k$-good random valuation is a probability measure on Fin k → ℝ≥0, and $k$ i.i.d. goods with law $\nu$ form Measure.pi (fun _ : Fin k => ν). Two independent groups $Y,Z$ have the product law on the disjoint union of their index types (jointLaw); the two-good statement Proposition 13 (i) uses this encoding on Unit ⊕ Unit. A mechanism is a pair of functions; the admissible class requires $q\in[0,1]^k$, IC, IR, and a measurable payment rule, the last being the without-loss-of-generality pin of the paper's footnote 12. The expected revenue of one mechanism is an EReal difference of two lower integrals, never a Bochner integral (which would be $0$ for non-integrable payments). $\mathrm{Rev}$ is a supremum in ℝ≥0∞, so infinite revenues are represented. $w$ is a real parameter with the hypothesis $w\,e^{w+1}=1$, not a Lambert-$W$ value. Logarithms are natural in Theorem D and base 2 (Real.logb 2) in the proof's explicit bounds, as printed; every statement with a logarithm keeps $k\ge2$.

The paper states Theorem D as a lower bound on an infimum of ratios $\mathrm{BRev}/\mathrm{Rev}$; the formal goal is the multiplicative inequality, which agrees with it wherever the ratio is defined and requires $\mathrm{BRev}=\infty$ when $\mathrm{Rev}=\infty$. A formalization in which $c$ may depend on $k$ or on the distribution, or in which $\mathrm{Rev}$ is computed with a Bochner integral, would trivialize the statement and is ruled out by the binder order and the definitions above.

The definitions are a mission-local copy of the model shared by this series (missions 1–5), so they can be merged later. Not posed here: Theorem C, Proposition 25, Corollary 23, Lemma 22, Example 32, the GFOR notation, and the asymptotic optimality of bundling (Appendix A.5). Proofs of any milestone are welcome, as are reusable lemmas on posted prices, stochastic domination of sums of independent variables, and binomial medians.

Selected references

• S. Hart and N. Nisan, Approximate Revenue Maximization with Multiple Items, J. Econ. Theory 172 (2017); preprint arXiv:1204.1846v3. https://arxiv.org/abs/1204.1846
• R. Myerson, Optimal Auction Design, Math. Oper. Res. 6 (1981) 58–73. https://doi.org/10.1287/moor.6.1.58
• M. Armstrong, Price Discrimination by a Many-Product Firm, Rev. Econ. Stud. 66 (1999) 151–168. https://doi.org/10.1111/1467-937X.00083
• Y. Bakos and E. Brynjolfsson, Bundling Information Goods: Pricing, Profits, and Efficiency, Management Sci. 45 (1999) 1613–1630. https://doi.org/10.1287/mnsc.45.12.1613
• S. Hart and P. Reny, Maximal Revenue with Multiple Goods: Nonmonotonicity and Other Observations, Theoretical Economics 10 (2015) 893–922. https://doi.org/10.3982/TE1517
• X. Li and A. C.-C. Yao, On Revenue Maximization for Selling Multiple Independently Distributed Items, PNAS 110 (2013) 11232–11237. https://doi.org/10.1073/pnas.1309533110
• M. Babaioff, N. Immorlica, B. Lucier and S. M. Weinberg, A Simple and Approximately Optimal Mechanism for an Additive Buyer, FOCS 2014. https://arxiv.org/abs/1405.6146