Operations Research

Motivation

A constraint $\mathbb E[v(x,\tilde z)] \le w$ on a decision $x$ requires the distribution of the random vector $\tilde z$. In practice that distribution is known only partially: its support, a few moments, or the probability mass of some regions estimated from data. Distributionally robust optimization asks that the constraint hold for every distribution consistent with this information. Wiesemann, Kuhn and Sim (Optimization Online 3757, 2013; Oper. Res. 62(6), 2014) proposed one standardized format for this information. Their format contains, as special cases, many ambiguity sets used earlier: support and moment information (Delage and Ye, 2010), and mean–covariance and directional-deviation information (Goh and Sim, 2010). They then characterized exactly when a worst-case expectation constraint over such a set has a finite conic reformulation. This mission formalizes that characterization: the paper's Theorem 1 and the steps of its proof.

Setting

The uncertain parameters are $\tilde z \in \mathbb R^P$, and an auxiliary random vector $\tilde u \in \mathbb R^Q$ may be added to describe structure of $\tilde z$. A proper cone $\mathcal K$ is a closed convex cone with $\mathcal K \cap(-\mathcal K) = \{0\}$ and nonempty interior. Write $x \preccurlyeq_{\mathcal K} y$ for $y - x \in \mathcal K$, and $\mathcal K^\star = \{y : x^\top y \ge 0\ \forall x \in \mathcal K\}$ for the dual cone. For indices $i \in \mathcal I = \{1,\dots,I\}$ the confidence sets are

$$\mathcal C_i = \{(z,u) : C_i z + D_i u \preccurlyeq_{\mathcal K_i} c_i\},$$

with matrices $C_i, D_i$, vectors $c_i$ and proper cones $\mathcal K_i$. The ambiguity set is

$$\mathcal P = \Big\{\mathbb P : \mathbb E_{\mathbb P}[A\tilde z + B\tilde u] = b,\ \ \mathbb P[(\tilde z,\tilde u) \in \mathcal C_i] \in [\underline p_i,\overline p_i]\ \ \forall i \in \mathcal I\Big\},$$

where $0 \le \underline p_i \le \overline p_i \le 1$. The paper imposes three conditions:

• (C1) $\mathcal C_I$ is bounded and $\underline p_I = \overline p_I = 1$;
• (C2) some $\mathbb P \in \mathcal P$ meets every non-degenerate probability bound strictly;
• (C3) the constraint function is a maximum of finitely many bi-affine pieces,

$$v(x,z) = \max_{l = 1,\dots,L} \big[(S_l z + s_l)^\top x + \mathbf t_l^\top z + t_l\big].$$

The distributionally robust constraint (3) is $\mathbb E_{\mathbb P}[v(x,\tilde z)] \le w$ for all $\mathbb P \in \mathcal P$.

A set $A$ is strictly included in $B$, written $A \Subset B$, if $A$ lies in the interior of $B$. The nesting condition (N) requires that any two distinct confidence sets be strictly nested or disjoint. For each $i$, $\mathcal A(i) = \{i\} \cup \{i' : \mathcal C_i \Subset \mathcal C_{i'}\}$ indexes the confidence sets containing $\mathcal C_i$.

Formalization targets

Goal: Theorem 1 (pp. 10–11)

Under (C1)–(C3), (N) and the two regularity conditions (S1)–(S2) described below, the constraint (3) holds if and only if there are $\beta \in \mathbb R^K$, $\kappa,\lambda \in \mathbb R^I_+$ and $\phi_{il} \in \mathcal K_i^\star$ such that, for all $i \in \mathcal I$ and $l$,

$$b^\top\beta + \sum_{i}\big[\overline p_i\kappa_i - \underline p_i\lambda_i\big] \le w,\qquad c_i^\top\phi_{il} + s_l^\top x + t_l \le \sum_{i' \in \mathcal A(i)}[\kappa_{i'} - \lambda_{i'}],$$ $$C_i^\top\phi_{il} + A^\top\beta = S_l^\top x + \mathbf t_l,\qquad D_i^\top\phi_{il} + B^\top\beta = 0.$$

Milestones

1. Theorem 1, sufficiency. The system implies (3), under (C1), (C3) and (N) alone.
2. Lemma 1 (p. 34). For a strictly feasible conic confidence set, the semi-infinite constraint $v(x,z) + f^\top z + g^\top u \le h$ on the set holds iff multipliers $\phi_l \in \mathcal K^\star$ exist with $c^\top\phi_l + s_l^\top x + t_l \le h$, $C^\top\phi_l = S_l^\top x + \mathbf t_l + f$ and $D^\top\phi_l = g$.
3. The dual of the moment problem (p. 35). Constraint (3) holds iff some $\beta$, $\kappa,\lambda \ge 0$ have objective value $\le w$ and satisfy $[Az+Bu]^\top\beta + \sum_i \mathbf 1_{\mathcal C_i}(z,u)[\kappa_i - \lambda_i] \ge v(x,z)$ on $\mathcal C_I$.
4. The partition step (p. 35). Under (N), the indicator constraint on $\mathcal C_I$ is equivalent to constraints with the constant $\sum_{\mathcal A(i)}$ on the pieces $\overline{\mathcal C}_i = \mathcal C_i \setminus \bigcup_{\mathcal C_{i'} \Subset \mathcal C_i} \mathcal C_{i'}$.
5. The boundary step (pp. 35–36). The $i$-th constraint holds on $\overline{\mathcal C}_i$ iff it holds on all of $\mathcal C_i$.

Significance

When the $\mathcal K_i$ are orthants, second-order cones or semidefinite cones, Theorem 1 turns the semi-infinite, measure-valued constraint (3) into a linear, conic-quadratic or semidefinite system of size polynomial in the data. The paper's Theorem 2 shows that when nesting fails, even checking $\mathcal P \neq \emptyset$ is strongly NP-hard. Theorem 1 is therefore the tractable side of a sharp dividing line. The paper builds its conservative approximation for non-nested sets (Theorem 3) and its lifting results (Section 3) on it.

The result is proved in the paper; nothing here is open. The formalization contributes two things. First, the duality theory for finite moment problems over measures on a compact set, and conic strong duality for strictly feasible sets: neither exists in Mathlib as stated. Second, a corrected statement. As printed, the "only if" direction of Theorem 1 is false, because (C2) does not give the strong duality the proof attributes to it. No machine-checked version of Theorem 1 is known.

Difficulty

The sufficiency half is weak duality: a pointwise inequality on $\mathcal C_I$ integrated against any $\mathbb P \in \mathcal P$. The necessity half needs three facts.

• Strong duality, with attainment, for an infinite-dimensional linear program over nonnegative measures. Here the obvious reference to a general conic duality theorem needs a constraint qualification on all moment constraints jointly, and (C2) controls only the probability bounds.
• A geometric step: under (N), a constraint imposed on $\overline{\mathcal C}_i$ extends to all of $\mathcal C_i$. This uses convexity of $v$ in $(z,u)$ together with the compactness of $\mathcal C_i$ and the strict inclusion of its descendants.
• Conic duality with dual attainment for each confidence set (Lemma 1), which fails without strict feasibility.

Formalization scope

Vectors are Fin n → ℝ, products are Matrix.mulVec and dotProduct, and the outcome space is (Fin nP → ℝ) × (Fin nQ → ℝ) with its Borel $\sigma$-algebra. The index set is Fin (nI + 1), 0-based, with $\mathcal C_I$ = Fin.last nI. Probabilities are μ.real. Constraint (3) is stated in its "for all $\mathbb P$" form, so no supremum of reals appears. The scalar $t_l$ and the vector $\mathbf t_l$ are separate fields.

Every member of $\mathcal P$ is a probability measure with finite first moment, so $\mathbb E_{\mathbb P}[A\tilde z + B\tilde u]$ is a genuine integral and not Lean's default value $0$. The expectation $\mathbb E_{\mathbb P}[v(x,\tilde z)]$ is genuine as well, since $v$ grows at most linearly. Hypothesis (C2) keeps $\mathcal P$ nonempty, so (3) cannot hold vacuously. A sorry-free sanity file exhibits two nested intervals for which all hypotheses of the goal hold at once.

Hypotheses added to the paper's, each needed for a true statement:

• (S1) moment-problem regularity. Every small common shift of $b$ and of each probability interval stays feasible over finite measures on $\mathcal C_I$. It is needed because with $\mathcal C_1$ the unit disk, $\mathbb E[\tilde z_1] = 1$, $v = z_2$ and $w = 0$, constraint (3) holds but the system has no solution.
• (S2) strict feasibility of every confidence set. It is needed because a confidence set that is a single boundary point of a second-order cone constraint admits no dual multipliers in Lemma 1.
• $\mathcal C_i \subseteq \mathcal C_I$ and $P + Q \ge 1$ in the partition and boundary steps. In dimension zero a set is strictly included in itself and $\overline{\mathcal C}_i$ can be empty.

(S1) also excludes some instances the page allows: $\overline p_i = 0$ or $\underline p_i = 1$ for $i \ne I$, and expectation rows that cannot be shifted in every direction by measures on $\mathcal C_I$.

The sufficiency milestone drops (C2) and the standing bounds $0 \le \underline p_i \le \overline p_i \le 1$, which only strengthens it.

Needed infrastructure, all reusable: conic duality for closed convex cones, Lagrangian duality for linear programs over finite measures on a compact set, and the extension of a convex inequality from the boundary of a compact set. Contributions of any of these as separate lemmas are welcome.

Selected references

• W. Wiesemann, D. Kuhn, M. Sim, Distributionally Robust Convex Optimization, Optimization Online preprint 3757, version of September 22, 2013. https://optimization-online.org/wp-content/uploads/2013/02/3757.pdf ; Operations Research 62(6):1358–1376, 2014. https://doi.org/10.1287/opre.2014.1314
• A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, chapter 7, Kluwer, 2001 (reference [56] of the paper; the result the proof of Theorem 1 cites as Proposition 3.4).
• E. Delage, Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• J. Goh, M. Sim, Distributionally robust optimization and its tractable approximations, Operations Research 58(4):902–917, 2010. https://doi.org/10.1287/opre.1090.0712
• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718829

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

Motivation

Polynomial optimization asks for the global minimum of a polynomial $f$ over a set $K \subseteq \mathbb R^n$ cut out by polynomial equations and inequalities. It contains nonconvex quadratic programming, max-cut, and many problems from control and engineering. Lasserre's hierarchy (Lasserre 2001) replaces this problem by a sequence of semidefinite programs whose optimal values $f_k$ increase towards the true minimum $f_{\min}$. Under the archimedean condition, Putinar's Positivstellensatz (Putinar 1993) gives asymptotic convergence $f_k \to f_{\min}$.

In computations the hierarchy usually reaches $f_{\min}$ exactly at a small order (Henrion and Lasserre), while the theory guaranteed only the limit. Known failures of finite convergence were special constructions, for example the Motzkin polynomial on the unit ball. Nie (2014) resolves this gap: finite convergence holds whenever the classical optimality conditions of nonlinear programming hold at every global minimizer.

Timeline. Lasserre (2001) introduces the hierarchy and proves $f_k \to f_{\min}$ under archimedeanness. Laurent (2007) and Nie (2013) prove finite convergence when $h = 0$ has finitely many complex, respectively real, solutions. Marshall (2006, 2009) introduces the boundary hessian condition and proves that it yields a representation of $f - f_{\min}$ in the quadratic module. Nie (arXiv 2012, Math. Program. 2014) shows that the classical optimality conditions imply the boundary hessian condition, and derives finite convergence.

Setting

Fix polynomials $f, h_1, \dots, h_{m_1}, g_1, \dots, g_{m_2} \in \mathbb R[x]$, $x \in \mathbb R^n$, and the problem

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

with feasible set $K$ and minimum value $f_{\min}$. Put $g_0 := 1$. A polynomial is SOS if it is a sum of squares of polynomials. For $k \in \mathbb N$ the truncated ideal and the truncated quadratic module are

$$\langle h\rangle_{2k} = \Big\{\sum_{i} \phi_i h_i : \deg(\phi_i h_i) \le 2k\Big\}, \qquad Q_k(g) = \Big\{\sum_{j=0}^{m_2} \sigma_j g_j : \sigma_j \text{ SOS},\ \deg(\sigma_j g_j) \le 2k\Big\},$$

and $Q(g) = \bigcup_k Q_k(g)$. The order-$k$ relaxation is $\max \gamma$ s.t. $f - \gamma \in \langle h\rangle_{2k} + Q_k(g)$, with optimal value $f_k$. The archimedean condition asks that $R - \sum_i x_i^2 \in \langle h\rangle_{2t} + Q_t(g)$ for some $t$ and some $R > 0$. The hierarchy has finite convergence if $f_k = f_{\min}$ for some $k$.

At a point $u$ with active set $J(u) = \{j : g_j(u) = 0\}$:

• the constraint qualification (CQC) asks that $\nabla h_i(u)$ ($i \in [m_1]$) and $\nabla g_j(u)$ ($j \in J(u)$) be linearly independent;
• multipliers $\lambda, \mu$ satisfy (1.3)–(1.4) if $\nabla f(u) = \sum_i \lambda_i \nabla h_i(u) + \sum_j \mu_j \nabla g_j(u)$, $\mu_j g_j(u) = 0$ and $\mu_j \ge 0$;
• strict complementarity (SCC) asks $\mu_j + g_j(u) > 0$ for all $j$;
• second order sufficiency (SOSC) asks $v^T \nabla^2_x L(u) v > 0$ for all nonzero $v$ orthogonal to every $\nabla h_i(u)$ and every active $\nabla g_j(u)$, where $L = f - \sum_i \lambda_i h_i - \sum_{j \in J(u)} \mu_j g_j$.

The boundary hessian condition (BHC) at $u$ asks for local parameters $t_1, \dots, t_\ell$ of the variety $V_{\mathbb R}(h)$ near $u$ such that $t_j = g_{\nu_j}$ for $j \le r$ and $K$ is locally $\{t_1, \dots, t_r \ge 0\}$. In these parameters the linear part of $f$ must be $a_1 t_1 + \dots + a_r t_r$ with all $a_j > 0$, and its quadratic part on $t_1 = \dots = t_r = 0$ must be positive definite.

Formalization targets

Goal: Theorem 1.1

If the archimedean condition holds and CQC, SCC and SOSC hold at every global minimizer of the problem, then

$$\exists\, k \in \mathbb N : \quad f_k = f_{\min}.$$

The goal fixes no order $k$ and no rate; it asserts exactly the paper's finite convergence.

Milestones

1. Theorem 3.1: at a local minimizer, CQC + SCC + SOSC imply BHC.
2. Theorem 2.4 (Marshall): archimedean and BHC at every global minimizer imply $f - f_{\min} \in I(V_{\mathbb R}(h)) + Q(g)$.
3. Real Nullstellensatz: $p \equiv 0$ on $V_{\mathbb R}(h)$ implies $p^{2e} + \sigma_2 \in \langle h\rangle$ for some SOS $\sigma_2$.
4. $1 + t + c t^{2e}$ is SOS for some $c > 0$ ($e \ge 1$).
5. The $\varepsilon$-argument: a representation $f - f_{\min} \in I(V_{\mathbb R}(h)) + Q(g)$ makes $\gamma = f_{\min} - \varepsilon$ feasible at one order $k_0$ for all $\varepsilon > 0$.
6. $f_k \le f_{\min}$ for all $k$ and $\{f_k\}$ is nondecreasing.
7. Companion, Proposition 3.4: if every relaxation attains its value and the first order condition fails at a global minimizer, there is no finite convergence.

Significance

The theorem turns an algebraic question (does a degree-bounded certificate of $f - f_{\min} + \varepsilon$ exist uniformly in $\varepsilon$?) into conditions checkable by linear algebra at the minimizers. Combined with the paper's second main result, that these conditions hold off a proper Zariski-closed set of input data, it shows that finite convergence of Lasserre's hierarchy is generic under archimedeanness. This is the theoretical explanation for the finite convergence observed in practice, and it underlies later work on flat truncation and the detection of optimality in moment relaxations.

Formalizing it produces the first machine-checked statements of Lasserre's hierarchy, truncated quadratic modules and the boundary hessian condition on the platform. The paper's own argument (Theorem 3.1 and the $\varepsilon$-argument) is short. Two cited results it rests on, Marshall's Theorem 9.5.3 and the Real Nullstellensatz, are proved in the literature but, as far as is known, have no formal proof in Mathlib or elsewhere. The result itself is proved (Nie 2014); none of it is formalized.

Difficulty

The obvious route is Putinar's Positivstellensatz applied to $f - f_{\min} + \varepsilon$. It gives a certificate for each $\varepsilon > 0$, but its degree grows as $\varepsilon \to 0$, so it yields only $f_k \to f_{\min}$. Finite convergence needs a certificate whose degree is bounded uniformly in $\varepsilon$, which is a statement about $f - f_{\min}$ itself, a polynomial that vanishes on $K$ and is therefore not strictly positive. Putinar's theorem says nothing there. Marshall's theorem supplies the missing representation under the boundary hessian condition, and its proof uses local real-analytic geometry at the zeros of $f - f_{\min}$, together with real algebra of quadratic modules.

Theorem 3.1 asks for a smooth local parametrization of $V_{\mathbb R}(h)$ whose first coordinates are prescribed constraint functions, and for control of the Taylor coefficients of $f$ in those parameters; Mathlib has the analytic ingredients but no such constructions for real varieties. The Real Nullstellensatz depends on the theory of real fields and real ideals. Neither cited result is available in Mathlib.

Formalization scope

Polynomials are MvPolynomial (Fin n) ℝ, points are Fin n → ℝ, and the paper's indices $1, \dots, m$ are Fin m; $m_1 = 0$ or $m_2 = 0$ is allowed. Gradients and Hessians come from formal partial derivatives. SOS is Mathlib's IsSumSq. $f_k$ is a supremum in EReal (it is $-\infty$ when the relaxation is infeasible). $f_{\min}$ is a real number that is the least value of $f$ on $K$, which excludes only $K = \emptyset$. The archimedean condition is the truncated form of p. 2, equivalent to §2.2's. $I(V)$ is Mathlib's vanishingIdeal. The multipliers of SCC and SOSC are the ones that satisfy (1.3)–(1.4). The boundary hessian condition is encoded with a $C^\infty$ parametrization $\Psi$ of $V_{\mathbb R}(h)$ near $u$ that is an immersion and a homeomorphism onto its image, together with nonsingularity of $u$ in the real-algebraic sense ($n - \ell$ polynomials vanishing on $V_{\mathbb R}(h)$ with independent gradients at $u$); Marshall's analytic parameters give the same condition, because both requirements are invariant under a change of parameters that fixes $t_1, \dots, t_r$.

Several encodings would make the statements trivial or false, and the formalization excludes them. Degree bounds are per term, on each $\phi_i h_i$ and each $\sigma_j g_j$ (including $\sigma_0$), never on the sum. $f_k$ is never a real sSup, which would be $0$ on an infeasible relaxation. CQC is linear independence of an indexed family, not of a set, so repeated gradients are dependent. The boundary hessian condition is not defined through the chart of the proof of Theorem 3.1. Finite convergence is $f_k = f_{\min}$, not $f - f_{\min} \in \langle h\rangle_{2k} + Q_k(g)$.

A complete development needs: truncated quadratic modules and their monotonicity; univariate SOS criteria; the Real Nullstellensatz; Marshall's representation theorem; and local parametrizations of real varieties at nonsingular points (Theorem 3.1). The definitions of the hierarchy and of the optimality conditions are reusable for any work on moment-SOS relaxations. Proofs of any milestone are welcome, as are proofs of the cited results under weaker hypotheses.

Selected references

• J. Nie, Optimality conditions and finite convergence of Lasserre's hierarchy, Math. Program. 146 (2014) 97–121; preprint arXiv:1206.0319v2 (2013). https://arxiv.org/abs/1206.0319
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM J. Optim. 11 (2001) 796–817. https://doi.org/10.1137/S1052623400366802
• M. Putinar, Positive polynomials on compact semi-algebraic sets, Indiana Univ. Math. J. 42 (1993) 969–984. https://doi.org/10.1512/iumj.1993.42.42045
• M. Marshall, Positive Polynomials and Sums of Squares, Mathematical Surveys and Monographs 146, AMS, 2008 (Theorem 9.5.3). https://doi.org/10.1090/surv/146
• M. Marshall, Representations of non-negative polynomials, degree bounds and applications to optimization, Canad. J. Math. 61 (2009) 205–221. https://doi.org/10.4153/CJM-2009-010-4
• J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Springer, 1998 (Corollary 4.1.8). https://doi.org/10.1007/978-3-662-03718-8

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

Motivation

In an aggregative game, a player's cost depends on its own decision and on a summary of all players' decisions. An electricity producer, for example, may choose its output while the market price depends on total output. When players communicate only with neighbours, each player must estimate the aggregate before making an update. Koshal, Nedić, and Shanbhag study this setting with communication links that can change over time, and prove convergence of a synchronous algorithm using only local messages Koshal–Nedić–Shanbhag, 2016.

The mission targets Proposition 2 of the pinned preprint. It treats the algorithm itself as a mathematical object: the claim must hold for every sequence satisfying its graph, weight, stepsize, and projected update conditions. The result addresses a concrete information constraint. Players cannot read the true aggregate while the algorithm runs; they have individual estimates constructed from their neighbours' estimates.

Setting

There are $N\ge1$ players. Player $i$ chooses $x_i\in K_i\subseteq\mathbb R^n$, with each $K_i$ nonempty, compact, and convex. Write $x=(x_i)_i$, $K=\prod_i K_i$, and $\bar x=\sum_i x_i$. The attainable aggregate set is $\bar K=\{\sum_i x_i:x\in K\}$. A map $F_i(x_i,u)$ gives the component of the game's gradient field at player $i$'s decision and aggregate argument $u$. Its profile field is $\phi_i(x)=F_i(x_i,\bar x)$.

The target point is a solution of the variational inequality $\operatorname{VI}(K,\phi)$: it belongs to $K$ and satisfies

$$\sum_{i=1}^N (x_i-x_i^*)^\top\phi_i(x^*)\ge0\qquad\text{for every }x\in K.$$

The paper obtains this field from differentiable player costs. The convergence theorem is stated for the field and the VI, while the connection to a Nash equilibrium is established separately in Proposition 1 Koshal–Nedić–Shanbhag, pp. 4–6. Strict monotonicity of $\phi$ on $K$ says that $(\phi(x)-\phi(x'))^\top(x-x')>0$ whenever feasible $x\ne x'$. Together with compactness and continuity, this yields the unique VI solution used in the target.

At time $k$, player $i$ keeps a decision $x_i^k$ and an estimate $v_i^k$ of the average decision, initially $v_i^0=x_i^0$. A matrix $W(k)=(w_{ij}(k))$ mixes estimates along an undirected communication graph. Each row and column of $W(k)$ sums to one; non-neighbours receive zero weight, while every neighbour and the player itself receive at least $\delta>0$. The union of the communication graphs over any $Q\ge1$ consecutive times is connected. The local aligned estimate and the two updates are

$$\hat v_i^k=\sum_j w_{ij}(k)v_j^k,\qquad x_i^{k+1}=\Pi_{K_i}\bigl[x_i^k-\alpha_k F_i(x_i^k,N\hat v_i^k)\bigr],\qquad v_i^{k+1}=\hat v_i^k+x_i^{k+1}-x_i^k.$$

Here $\Pi_{K_i}$ denotes Euclidean nearest-point projection. The stepsizes $\alpha_k$ decrease, their sum diverges to $+\infty$, and their squares are summable. The paper calls these graph, weight, and stepsize conditions Assumptions 4–6 Koshal–Nedić–Shanbhag, pp. 7–9.

Formalization targets

Unique VI solution

The first milestone makes the existence and uniqueness statement used in the proof explicit:

$$\exists!x^*\in K:\quad(x-x^*)^\top\phi(x^*)\ge0\quad\text{for all }x\in K.$$

The other milestones follow the paper's numbered Lemmas 1–4 and 6 and its displayed relations (19)–(20). They state that the mean of the players' estimates is the true mean decision, that the matrix products mix geometrically, that the relevant gradients and estimate errors are controlled, and that the weighted estimate errors have finite total sum Koshal–Nedić–Shanbhag, pp. 9–14.

Proposition 2

For every synchronous run under Assumptions 1–6, the goal asserts both a unique VI solution and convergence of the whole decision sequence:

$$\exists!x^*\in K\text{ solving }\operatorname{VI}(K,\phi), \qquad x^k\longrightarrow x^*.$$

The target is a qualitative convergence result. It does not prescribe a convergence rate for $x^k$ Koshal–Nedić–Shanbhag, Proposition 2, p. 13.

Significance

The theorem says that local estimate mixing is sufficient for every player's projected gradient decision to approach the same equilibrium, even when the communication graph changes, provided connectivity recurs within a fixed window. The result gives a precise condition under which access to the aggregate can be replaced by neighbour messages. Its milestone on the matrix products supplies an explicit estimate for how information spreads; the summability milestones connect that estimate to the optimization error.

The paper contains a mathematical proof, but this mission's Lean declarations are open statements with sorry bodies. A completed formalization would turn the paper's VI existence, mixing, projection, and convergence arguments into individually reusable verified results. The general product-set VI and nearest-point relation are separated from the paper's particular synchronous model so later developments can use them without importing graph-specific definitions.

Difficulty

The obvious single-agent projected-gradient argument assumes each update uses $F_i(x_i^k,\bar x^k)$. Here it uses $F_i(x_i^k,N\hat v_i^k)$ instead, and the estimate errors depend on a changing product of weight matrices. Connectivity of each individual graph is not assumed, so a one-step contraction statement is unavailable. The proof must control time-varying mixing and accumulate its error without losing convergence. Strict monotonicity then identifies the limit, but it does not by itself bound the transient disagreement.

The printed hypotheses also leave a domain issue. The algorithm evaluates $F_i$ at $N\hat v_i^k$, which need not lie in $\bar K$; the paper's footnote on p. 10 acknowledges that $\hat v_i^k$ may leave its apparent feasible aggregate region. The printed Lipschitz condition covers only $\bar K$, so the target explicitly requires it for all aggregate arguments. The printed Lemma 3 also gives only unit column sums, which allow arbitrarily large negative and positive entries; its mission item carries the graph and positive-weight assumptions needed for the bound. These changes are recorded in the item notes and in the source analysis Koshal–Nedić–Shanbhag, pp. 7–10.

Formalization scope

Decisions live in EuclideanSpace ℝ (Fin n) and players in Fin N; Lean player zero is the paper's player one. A profile is a finite function, and its squared Euclidean norm is the sum of the squared norms of its blocks. The conclusion uses the equivalent finite product topology. The variational inequality's inner product is written as a sum over players, avoiding the sup norm carried by a Lean function space. Graphs are undirected SimpleGraphs; self-neighbours are included explicitly. The product $\Phi(k,s)$ places the newest matrix on the left. Projection is a relation requiring a genuine nearest point in $K_i$, rather than a total function with an arbitrary value on an empty set.

The target fixes $N\ge1$, $\delta>0$, and nonempty $K_i$. It uses continuity of $F_i$ on $K_i\times\bar K$ as the field-level part of Assumption 1, and the extended all-$\mathbb R^n$ form of Assumption 3 stated above. The stepsize sum is represented by partial sums tending to $+\infty$, and $\sum_k\alpha_k^2<\infty$ by summability. Existence and uniqueness are part of the goal conclusion; no bound on the gradients or summability of the estimate error is assumed by the goal. A complete development needs reusable compact-product VI existence, Euclidean projection facts, matrix-product mixing for changing graphs, finite-dimensional norm estimates, and real-series convergence. Contributions proving these milestones and their intermediate lemmas are welcome.

Selected references

• J. Koshal, A. Nedić, U. V. Shanbhag, Distributed Algorithms for Aggregative Games on Graphs, Operations Research 64(3):680–704, 2016. arXiv:1605.00267v2; DOI:10.1287/opre.2016.1501. This mission cites the pinned arXiv page indices.

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