Optimization

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models 1: Augmented Greedy Earns a (1 − 1/e) Fraction of the Optimal Revenue from the Complete Customer TypesResearch Paper

Motivation

Retailers that carry a limited range of products often know something about a customer before choosing which of those products to display. The customized assortment problem asks which products to carry when the displayed assortment may be tailored to the arriving customer's type. This separates the first-stage capacity decision from the later offer decision. El Housni and Topaloglu study the problem under a mixture of multinomial logit choice models and develop an approximation framework for it in their SSRN paper. This mission isolates their structural guarantee for Augmented Greedy, Theorem 4.2 of the PDF version dated 7 December 2021. The theorem identifies the revenue recovered from customer types whose optimal personalized offers agree with a chosen product subset.

The paper contrasts this setting with ordinary assortment optimization, where every type sees the same products. Its later approximation results use the structural guarantee here as a component. The classical comparison is the cardinality-constrained greedy bound for monotone submodular functions, associated with Nemhauser, Wolsey and Fisher (1978). The paper's Appendix B gives an instance in which the customized revenue function lacks global submodularity, so that classical result does not apply directly. El Housni and Topaloglu, §§4 and App. B.

Setting

Let $N=\{1,\ldots,n\}$ be a finite product set. Product $i$ has positive revenue $r_i$ , and products are indexed with $r_1\ge\cdots\ge r_n>0$ . Let $M=\{1,\ldots,m\}$ be customer types. A type- $j$ customer arrives with probability $\theta_j\ge0$ , with $\sum_{j\in M}\theta_j=1$ , and assigns each product $i$ a nonnegative preference weight $v_{ij}$ . The no-purchase option has weight one. Offering an assortment $T\subseteq N$ to that customer gives MNL expected revenue

\operatorname{Rev}_j(T)= \frac{\sum_{i\in T}r_i v_{ij}}{1+\sum_{i\in T}v_{ij}}.

If the retailer initially carries only $S\subseteq N$ , it can still choose the best offer to each customer type. Thus $f_j(S)=\max_{T\subseteq S}\operatorname{Rev}_j(T)$ . For $C\subseteq M$ , write $f^C(S)=\sum_{j\in C}\theta_j f_j(S)$ , and abbreviate $f=f^M$ . The first-stage capacity is $K$ ; an optimal solution $S^*$ of CAP maximizes $f(S)$ among sets with at most $K$ products. These definitions and the standing data assumptions are stated in §2 and §4 of the paper.

For each product $i$ , the prefix $V_i=\{1,\ldots,i\}$ contains products at least as early in the revenue ordering. Greedy starts at the empty set, repeatedly adds an available product that maximizes the new objective value, and stops at cardinality $k$ or when the prefix is exhausted. Augmented Greedy runs Greedy on $V_i$ for each $i$ , using $S\mapsto\sum_{j\in C}\theta_j\min(f_j(S),r_i)$ , and returns whichever candidate has the greatest $f^C$ value. Both stages may break ties arbitrarily. El Housni and Topaloglu, §4.1.

For type $j$ , use the optimal personalized assortment $S_j^*=\{i\in S^*:r_i\ge f_j(S^*)\}$ , characterized by Lemma E.1. A type $j\in C$ is complete with respect to $P\subseteq N$ when $P\cap S_j^*=P\cap S^*$ ; let $C_P$ collect these types. The threshold choice matters because zero-weight products can be present in other optimal offers without helping a customer. El Housni and Topaloglu, Definition 4.1 and App. E.

Formalization targets

Theorem 4.2: complete-type revenue

For every $C\subseteq M$ , $P\subseteq N$ , $k$ with $|P\cap S^*|\le k$ , and every output $\Delta$ of Augmented Greedy on $C,k$ ,

f^C(\Delta)\ge(1-1/e)\,f^{C_P}(P\cap S^*).

This is the mission goal, the structural performance statement of Theorem 4.2, p. 11. It does not assert a constant-factor approximation to all of CAP: it identifies the contribution from complete customer types.

Supporting targets

The milestone list follows the results used with this bound: monotonicity of $f_j$ from Appendix C; the MNL threshold assortment of Lemma E.1; submodularity of $S\mapsto\min(f_j(S),r_i)$ on $V_i$ from Lemma 4.3; and the cited $1-1/e$ Greedy guarantee for a nonnegative monotone submodular objective. The greedy milestone compares its output against every feasible set of cardinality at most $k$ .

Significance

The theorem says that one algorithmic output captures a fixed fraction of the benchmark supplied by complete types, despite the absence of global submodularity of $f$ . It connects the local behavior of truncated type revenues to the full customized assortment objective. The paper uses this result in the development of later algorithms; without it, the standard submodular greedy theorem gives no immediate conclusion for CAP. El Housni and Topaloglu, §§4–5.

The mathematical results are proved in the 2021 paper. The formalization work here is to give machine-checkable statements for the objective, the algorithm with all its legal tie choices, and the four supporting targets, then supply proofs. The MNL revenue formula is already available as a published platform definition; the local CAP and algorithm definitions specify the extra model needed by this theorem. A completed development could also support later CAP missions that use the same threshold and submodularity properties.

Difficulty

The tempting argument applies the classical greedy guarantee directly to $f$ , since $f$ increases when more products are carried. Appendix B of the paper shows that this fails: even for one customer type, $f$ need not be submodular. Restricting the ground set to a revenue prefix and truncating each $f_j$ at that prefix's revenue level changes the submodularity question, but the final guarantee must still concern the untruncated $f^C$ objective. The threshold condition in the definition of $C_P$ is what makes that comparison meaningful. El Housni and Topaloglu, App. B, Lemma 4.3 and Theorem 4.2.

Formalization scope

Products and types are Fin n and Fin m; their zero-based Lean indices correspond to the paper's indices plus one. Assortments and type groups are finite sets. The model assumes $r_i>0$ , $v_{ij}\ge0$ , $\theta_j\ge0$ , $\sum_j\theta_j=1$ , and decreasing revenue order. The no-purchase weight is exactly one. CAP and personalized revenue use maxima over nonempty finite powersets, so empty input sets have their intended value rather than an arbitrary real supremum. The theorem keeps the source's optimality assumption on $S^*$ , even though its particular inequality uses less.

The Greedy predicate describes each successive maximizer and the exact stopping rule. Augmented Greedy requires a Greedy output at every prefix and an $f^C$ -maximizing choice among them. Thus the output is constrained by the printed algorithm, and the statement covers every tie-break. The type- $j$ assortment is defined from $S^*$ by the Lemma E.1 threshold, rather than supplied as a free set. These choices rule out a size-only output condition, an arbitrarily chosen $S_j^*$ , a vacuous run predicate, and real supremum defaults. The target includes the corner cases $k=0$ , $C=\varnothing$ , and $P\cap S^*=\varnothing$ , where its right side is zero. Arrival probabilities summing to one force $m\ge1$ ; Augmented Greedy has an output only when at least one product exists.

The reusable parts are the MNL threshold characterization, finite-set submodularity and the general Greedy bound. Contributions toward those lemmas, the paper's case analysis for Lemma 4.3, and the final structural theorem are in scope. Runtime claims, the paper's later logarithmic approximation theorems and its computational experiments are outside this mission.

Selected references

Omar El Housni and Huseyin Topaloglu, Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models: Value of Personalized Assortments, SSRN 3830082, version of 7 December 2021; published as Operations Research 71(4), 2023. SSRN preprint. The mission's numbering and page citations use the pinned 2021 PDF.
George L. Nemhauser, Laurence A. Wolsey and Marshall L. Fisher, An Analysis of Approximations for Maximizing Submodular Set Functions—I, Mathematical Programming 14, 265–294, 1978. DOI.

9 thms2 active usersReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Intrinsic Robustness of the Price of Anarchy III: For Every Set of Cost Functions, Congestion Games Are Tight — the Worst-Case Pure Price of Anarchy Equals the Best Smoothness BoundResearch Paper

Motivation

In a congestion game, each player chooses resources and pays a cost that depends on how many players use each chosen resource. Such games model shared facilities and network use, where independently chosen strategies can cost more in total than a coordinated choice. The price of anarchy measures this inefficiency by comparing the social cost of an equilibrium with the minimum social cost. A familiar way to bound it is to prove a smoothness inequality that applies to every pair of strategy profiles. That inequality has a useful reach: once established, it bounds not only pure Nash equilibria but also broader equilibrium notions. The question in this mission is how much that reach costs in sharpness. Roughgarden (2015) proves that for congestion games it costs nothing at the level of the worst case over any fixed collection of allowed resource cost functions.

For affine resource costs, earlier analyses had already identified a worst-case value of $5/2$ , attained by a finite congestion game and matched by a smoothness bound. The 2015 paper asks whether this agreement reflects affine costs or a general property of congestion games. Its Theorem 5.8 gives the latter answer, even when the collection of allowed functions is infinite and has no prescribed formula. The mission treats the theorem at that generality, while giving the finite positive case and the boundary case their own supporting targets. Roughgarden (2015), §§2.3 and 5.

Setting

A finite congestion game has a finite player set, a finite resource set $E$ , and for each player $i$ a nonempty set $S_i$ of subsets of $E$ called strategies. Each resource $e$ has a cost function $c_e:\mathbb N\to\mathbb R$ . For a strategy profile $A=(A_i)_i$ , its load $x_e(A)$ is the number of players whose selected strategy contains $e$ . Player $i$ pays $C_i(A)=\sum_{e\in A_i}c_e(x_e(A))$ , and the social cost is $C(A)=\sum_i C_i(A)$ . A profile is a pure Nash equilibrium when no player can lower its own cost by changing its strategy alone. These are the objects of Example 2.5 in Roughgarden (2015).

Fix a nonempty set $\mathcal C$ of resource cost functions, each nonnegative, nondecreasing, and not identically zero on positive loads. The class $\mathcal G(\mathcal C)$ contains every finite congestion game whose resource functions belong to $\mathcal C$ . It permits any finite number of players and resources and any nonempty strategy families. The pure price of anarchy $\rho_{\mathrm{pure}}(G)$ is the largest equilibrium-to-optimum cost ratio in one game, allowing $+\infty$ when an equilibrium costs more than zero but the optimum costs zero.

A game is $(\lambda,\mu)$ -smooth if, for every two feasible profiles $A,A^*$ , the sum of the player costs after each player individually switches from $A_i$ to $A_i^*$ is at most $\lambda C(A^*)+\mu C(A)$ . The set $\mathcal A(\mathcal G(\mathcal C))$ consists of pairs with $\mu<1$ that satisfy this inequality for every game in the class. A related resourcewise set $\mathcal A(\mathcal C)$ asks, for every $c\in\mathcal C$ , current load $x\ge0$ , and comparison load $x^*\ge1$ , that

c(x+1)x^*\le\lambda c(x^*)x^*+\mu c(x)x.

Its best ratio is $\gamma(\mathcal C)=\inf_{(\lambda,\mu)\in\mathcal A(\mathcal C)}\lambda/(1-\mu)$ , with value $+\infty$ if there is no admissible pair. The bounded-load versions $\mathcal A(\mathcal C,n)$ and $\gamma(\mathcal C,n)$ use $0\le x\le n$ and $1\le x^*\le n$ . Roughgarden (2015), equations (34)–(36) and (41).

Formalization targets

Tightness of the congestion-game class

Theorem 5.8, in the form of equation (34), is the goal:

\sup_{G\in\mathcal G(\mathcal C)}\rho_{\mathrm{pure}}(G) =\inf_{(\lambda,\mu)\in\mathcal A(\mathcal G(\mathcal C))}\frac{\lambda}{1-\mu}.

It applies to every nonempty set $\mathcal C$ satisfying the standing cost-function conditions, whether finite, countable, or uncountable. Neither the number of players nor the number of resources is fixed. The equality is stronger than the routine upper bound from smoothness: it says that the best upper bound available from a uniform smoothness argument matches actual worst-case pure-equilibrium inefficiency. Roughgarden (2015), Theorem 5.8 and (34).

Resourcewise characterization

The paper also identifies the common value with $\gamma(\mathcal C)$ :

\sup_{G\in\mathcal G(\mathcal C)}\rho_{\mathrm{pure}}(G)=\gamma(\mathcal C).

The milestone list follows the paper's statements: the general upper bound; nonnegativity of $\mu$ ; passage from resource constraints to game smoothness; the bound for one game; the two finite optimization lemmas; the finite lower-bound theorem; the infinite-price boundary case; the countable case; and the characterization by $\gamma(\mathcal C)$ . The finite lower-bound target uses the one-sided conclusion established in the proof of Theorem 5.6. Roughgarden (2015), §§5.1–5.5.

Significance

The equality rules out a uniform improvement of the worst-case pure price-of-anarchy bound by using features of pure Nash equilibrium that a smoothness argument ignores. In this domain the broader applicability of smoothness does not force a worse class-wide bound. For a chosen cost-function family, the resourcewise characterization expresses that bound through explicit inequalities rather than a search over every possible finite game. Roughgarden (2015), §§2.4 and 5.5.

The result is proved in the paper. The remaining work here is a machine-checked proof of its formal statement and supporting theorems. The published congestion-game model supplies loads, player costs, feasible profiles, and pure Nash equilibria. The definitions of smoothness parameters and prices of anarchy built for this mission can also support later work on other cost-function classes and equilibrium bounds. The goal statement itself is a proof target, not an already verified result.

Difficulty

The smoothness inequality immediately gives an upper bound on equilibrium costs, but it does not by itself show that a game attains or approaches that bound. The difficult direction relates a small family of resourcewise constraints to actual games with inefficient equilibria. For finite positive cost-function sets, the optimum parameter value may be attained or may be approached only at infinity in parameter space; the two cases have different statements in Lemmas 5.3 and 5.5. The general theorem must also cover functions that vanish at a positive load, unbounded worst-case ratios, and sets of functions of arbitrary cardinality. Simply optimizing a bound for one fixed game would miss the supremum over the entire class. Roughgarden (2015), §§5.2–5.4.

Formalization scope

Lean represents players and resources by Fin k and Fin m and quantifies over every $k,m\in\mathbb N$ . A strategy is a finite resource subset, a strategy family is finite and nonempty, and all costs are real-valued at each load. The value $c(0)$ is unrestricted because it is unused in a player's cost and is multiplied by zero in (35). The all-zero function is excluded as in §5.1. Nonemptiness of $\mathcal C$ , stated at the start of that section, is carried into the finite optimization lemmas because their conclusions select functions from $\mathcal C$ . Zero-player and zero-resource games are allowed and do not raise the worst-case supremum.

Prices of anarchy and the values $\gamma$ are extended nonnegative reals. Thus an empty smoothness-parameter set has infimum $+\infty$ ; a positive equilibrium cost over zero optimum gives $+\infty$ ; and a game with no equilibrium contributes zero to the supremum. The paper's finite congestion games with nonempty strategy sets do have pure equilibria. The conversion of a real ratio $\lambda/(1-\mu)$ into this type does not truncate admissible class-wide ratios: if some cost function has $c(1)>0$ , a one-resource game forces the ratio to be at least one; if none does, the parameter set is empty. Smoothness and optimum quantify over feasible profiles only. These choices prevent the equality from becoming vacuous through an empty real infimum, total division by zero, or a supremum over a fixed small game size.

The complete development needs finite-set sums, function updates, extended nonnegative infima and suprema, and the published congestion-game definitions. Reusable contributions include lemmas about the resourcewise parameter sets and their relation to game smoothness. The paper's uncountable approximation paragraph has a gap for flat cost functions; the theorem remains the stated target, and a formal proof may use a different argument at that stage. Roughgarden (2015), pp. 31–32.

Selected references

Tim Roughgarden, Intrinsic Robustness of the Price of Anarchy, Journal of the ACM 62(5), Article 32, 2015. DOI. The source used here is the author's final version dated July 14, 2015; the cited page numbers are its printed pages.

13 thms2 active usersReviewed

Completed

Convex Optimization Dynamical Systems·Captain: mikedeng1

A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights II: The ODE Solution Satisfies f(X(t)) − f⋆ ≤ 2‖x₀ − x⋆‖²/t²Research Paper

Motivation

Nesterov's accelerated gradient method (Nesterov, 1983) minimizes a smooth convex function $f$ with the update

x_k=y_{k-1}-s\nabla f(y_{k-1}),\qquad y_k=x_k+\frac{k-1}{k+2}(x_k-x_{k-1}),

and, for step size $s\le 1/L$ , attains $f(x_k)-f^\star\le 2\|x_0-x^\star\|^2/(s(k+1)^2)$ . The rate $O(1/k^2)$ is optimal among first-order methods, yet the classical proof proceeds by an "estimate sequence" argument that offers little insight into why the momentum coefficient $(k-1)/(k+2)$ works.

Su, Boyd and Candès (arXiv:1503.01243, J. Mach. Learn. Res. 17, 2016) showed that, as $s\to0$ , the iterates track the solution of the second-order ordinary differential equation

\ddot X+\frac3t\dot X+\nabla f(X)=0,\qquad X(0)=x_0,\ \dot X(0)=0,

under the time identification $t\approx k\sqrt s$ . Their Theorem 3 is the continuous-time counterpart of Nesterov's rate. Its short proof by an energy (Lyapunov) function became the template for a large literature on continuous-time models of accelerated methods, including Wibisono, Wilson and Jordan's variational perspective (PNAS 2016) and Attouch, Chbani, Peypouquet and Redont's analysis of the damped system $\ddot x+\frac\alpha t\dot x+\nabla\Phi(x)=0$ (Math. Program. 2018).

This mission formalizes Theorem 3 and the three steps of its proof.

Setting

Let $n\ge0$ and let $\mathbb R^n$ carry the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . For $f:\mathbb R^n\to\mathbb R$ differentiable, $\nabla f$ is its gradient.

For $L>0$ , the class $\mathcal F_L$ consists of the convex, continuously differentiable $f$ with $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$ . The class $\mathcal F_\infty$ is $\bigcup_{L>0}\mathcal F_L$ .
A minimizer $x^\star$ is any point with $f(x^\star)\le f(y)$ for all $y$ , and $f^\star=f(x^\star)$ .
A solution of the ODE (3) with initial point $x_0$ is a curve $X$ on $[0,\infty)$ , twice continuously differentiable on $(0,\infty)$ and continuously differentiable on $[0,\infty)$ , with $X(0)=x_0$ , $\dot X(0)=0$ , and $\ddot X(t)+\frac3t\dot X(t)+\nabla f(X(t))=0$ for every $t>0$ . The damping coefficient $3/t$ is singular at $t=0$ ; the paper's Theorem 1 shows that a unique such solution exists for every $f\in\mathcal F_\infty$ .
The energy along a solution is

\mathcal E(t)=t^2\big(f(X(t))-f^\star\big)+2\Big\|X(t)+\frac t2\dot X(t)-x^\star\Big\|^2 .

In the Lean development these are IsFL, IsFinfty, IsSolution f 3 x₀ X V and energy f xstar X V t, in the namespace NesterovODE.Rate, where V is the velocity $\dot X$ .

Formalization targets

Goal: Theorem 3 (p. 7)

For every $f\in\mathcal F_\infty$ , every minimizer $x^\star$ , every $x_0$ and every solution $X$ of (3),

f(X(t))-f^\star\le\frac{2\|x_0-x^\star\|^2}{t^2}\qquad\text{for all }t>0.

Milestones (proof of Theorem 3, pp. 7–8)

Derivative of the energy. For $t>0$ ,

\dot{\mathcal E}=2t(f(X)-f^\star)+t^2\langle\nabla f(X),\dot X\rangle+4\Big\langle X+\frac t2\dot X-x^\star,\frac32\dot X+\frac t2\ddot X\Big\rangle .

The energy is nonincreasing. Using the ODE,

\dot{\mathcal E}=2t(f(X)-f^\star)+4\Big\langle X-x^\star,-\frac t2\nabla f(X)\Big\rangle=2t(f(X)-f^\star)-2t\langle X-x^\star,\nabla f(X)\rangle\le0 .

The bound chain. $\mathcal E$ is nonincreasing on $[0,\infty)$ and, for $t>0$ ,

f(X(t))-f^\star\le\frac{\mathcal E(t)}{t^2}\le\frac{\mathcal E(0)}{t^2}=\frac{2\|x_0-x^\star\|^2}{t^2}.

Significance

Theorem 3 is the statement that makes the ODE a faithful model of Nesterov's scheme at the level of rates: under $t\approx k\sqrt s$ , the bound (7) reproduces the discrete bound (6) with the same constant 2. The paper also shows that the constant cannot be improved (p. 8). The energy $\mathcal E$ is the continuous analogue of the potential used in discrete proofs, and the same template, with other weights, gives the paper's later results on the generalized damping $r/t$ and on strongly convex objectives.

The result is proved in the paper. As far as the platform and Mathlib are concerned it is not formalized: Mathlib has the calculus (derivatives of inner products and norms along curves, the first-order characterization of convexity, monotonicity from a sign of the derivative) but no statement about this ODE. A machine-checked proof establishes the Lyapunov argument for the singular-at-zero system, including the endpoint $t=0$ where only one-sided regularity is available, and supplies reusable lemmas for the other missions of this series and for formalizations of inertial dynamics with vanishing damping.

Difficulty

The algebra is short; the care lies in the analytic bookkeeping that the paper leaves implicit.

The energy is defined through $f\circ X$ and $\|X+\frac t2\dot X-x^\star\|^2$ , so its derivative needs the chain rule for a $C^1$ function along a differentiable curve and the derivative of a squared norm of a curve.
The ODE holds only for $t>0$ and the coefficient $3/t$ blows up at $0$ . Monotonicity of $\mathcal E$ on the closed half-line therefore needs right-continuity of $\mathcal E$ at $0$ , which follows from right-continuity of $X$ and $\dot X$ there, together with $t\dot X(t)\to0$ ; the derivative argument alone gives monotonicity only on $(0,\infty)$ .
The sign of $\dot{\mathcal E}$ needs the first-order inequality $f(x^\star)\ge f(X)+\langle\nabla f(X),x^\star-X\rangle$ for a differentiable convex function.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient f. $f\in\mathcal F_L$ is 0 < L ∧ ConvexOn ℝ Set.univ f ∧ ContDiff ℝ 1 f ∧ LipschitzWith L (gradient f) with L : NNReal.
A solution is encoded as a pair of curves $(X,V)$ : $X(0)=x_0$ , $V(0)=0$ , $X$ has right derivative $V(0)$ at $0$ , $V$ is right-continuous at $0$ , and for every $t>0$ , $X$ has derivative $V(t)$ and $V$ has derivative $-\frac3tV(t)-\nabla f(X(t))$ . For continuous $\nabla f$ this is exactly the paper's regularity class $C^2((0,\infty))\cap C^1([0,\infty))$ with the ODE and the initial conditions. Values of $X$ for $t<0$ are unconstrained and never used.
The paper states Theorem 3 for "the unique global solution". The Lean statements quantify over every solution and every minimizer, which by Theorem 1 is the same statement and does not depend on Theorem 1 (formalized in a separate mission of this series).
No hypothesis beyond the paper's is added. The Lipschitz constant is part of $\mathcal F_\infty$ and is kept although the proof of Theorem 3 does not use it quantitatively.
The bound is stated for $t>0$ only. At $t=0$ the right-hand side $2\|x_0-x^\star\|^2/0$ is $0$ in Lean, and the inequality would be false.
The derivative statements use HasDerivAt rather than deriv, so no derivative silently takes the default value $0$ ; the solution predicate is satisfiable (for $f(x)=\|x\|^2/2$ , $x_0=0$ , the zero curve is a solution), so the goal is not vacuous.

Contributions welcome: proofs of the three milestones and of the goal; general lemmas on the derivative of $t\mapsto f(X(t))$ and $t\mapsto\|X(t)+\frac t2V(t)-x^\star\|^2$ ; and the first-order convexity inequality in gradient form, which the strongly convex and generalized-damping missions of this series also need.

Selected references

W. Su, S. Boyd, E. J. Candès, A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights, J. Mach. Learn. Res. 17(153):1–43, 2016; cited from arXiv:1503.01243v2, 2015. https://arxiv.org/abs/1503.01243
Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27(2):372–376, 1983.
A. Wibisono, A. C. Wilson, M. I. Jordan, A variational perspective on accelerated methods in optimization, Proc. Natl. Acad. Sci. 113(47):E7351–E7358, 2016. https://doi.org/10.1073/pnas.1614734113
H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168:123–175, 2018. https://doi.org/10.1007/s10107-016-1065-5

5 thms2 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition IV: Stochastic Gradient Rates LC²/(2kμ²) and (1 − 2μα)^k [f(x_0) − f*] + LC²α/(4μ)Research Paper

Motivation

Stochastic gradient (SG) methods are the default algorithms for training machine-learning models: when an objective is an average over a very large number of training examples, computing its full gradient even a few times is infeasible, while the gradient of a single randomly chosen example is cheap. The classical convergence theory of SG rates its expected suboptimality under strong convexity — the $O(1/k)$ rate of Nemirovski, Juditsky, Lan and Shapiro (2009) — yet common models such as least squares with a rank-deficient design and logistic regression are convex but not strongly convex.

Karimi, Nutini and Schmidt (2016) observed that the much older Polyak–Łojasiewicz (PL) inequality of Polyak (1963) is enough to recover linear rates for gradient descent and its variants without any convexity. Their Theorem 4 transfers this observation to SG: under PL alone, SG with a decreasing step attains the $O(1/k)$ rate known from the strongly convex case, and SG with a constant step converges linearly to a neighbourhood of the optimum whose size is proportional to the step. This mission formalizes that theorem.

Setting

Let $d\ge0$ and let $\mathbb R^d$ carry the Euclidean norm $\|\cdot\|$ . An index $i$ ranges over a measurable space $I$ with a probability measure $\nu$ , and each index has a differentiable component function $f_i:\mathbb R^d\to\mathbb R$ . The stochastic optimization problem (7) is to minimize

f(x) = \mathbb E_{i\sim\nu}[f_i(x)],

of which the finite sum $f = \frac1n\sum_{i=1}^n f_i$ (8) is the case of the uniform distribution on $n$ indices. The component gradients are unbiased: $\mathbb E_{i\sim\nu}[\nabla f_i(x)] = \nabla f(x)$ for every $x$ .

The SG method (9) starts from a point $x_0$ and, given step sizes $\alpha_k>0$ and indices $i_0,i_1,\dots$ drawn independently from $\nu$ , iterates

x_{k+1} = x_k - \alpha_k\nabla f_{i_k}(x_k).

The iterate $x_k$ is a random vector, a function of $i_0,\dots,i_{k-1}$ .

The standing assumptions on $f$ (§2 of the paper) are:

$\nabla f$ is $L$ -Lipschitz: $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$ , with $L>0$ ;
the solution set is non-empty: some $x^*$ minimizes $f$ , and $f^* = f(x^*)$ ;
the PL inequality (3) with constant $\mu>0$ : $\tfrac12\|\nabla f(x)\|^2\ge\mu\,(f(x)-f^*)$ for all $x$ .

Theorem 4 adds a second-moment bound along the iterates: $\mathbb E_{i\sim\nu}\big[\|\nabla f_i(x_k)\|^2\big]\le C^2$ for every iterate $x_k$ .

Formalization targets

Goal: Theorem 4 (p. 6)

Under the assumptions above,

with the decreasing step $\alpha_k = \dfrac{2k+1}{2\mu(k+1)^2}$ ,

\mathbb E[f(x_k)-f^*]\le\frac{LC^2}{2k\mu^2}\qquad(k\ge1);

with a constant step $\alpha_k=\alpha$ , $0<\alpha<\dfrac1{2\mu}$ ,

\mathbb E[f(x_k)-f^*]\le(1-2\mu\alpha)^k\,[f(x_0)-f^*]+\frac{LC^2\alpha}{4\mu}\qquad(k\ge0).

The second-moment bound is assumed separately for the run of each scheme, with the same constant $C$ .

Milestones (proof of Theorem 4, p. 7)

One-step bound. For any point $x$ with $\mathbb E_i\|\nabla f_i(x)\|^2\le C^2$ and any step $a$ ,

\mathbb E_i[f(x-a\nabla f_i(x))]\le f(x)-a\|\nabla f(x)\|^2+\frac{LC^2a^2}{2}.

Recursion (10). Along the run, whenever $\alpha_k\ge0$ ,

\mathbb E[f(x_{k+1})-f^*]\le(1-2\alpha_k\mu)\,\mathbb E[f(x_k)-f^*]+\frac{LC^2\alpha_k^2}{2}.

Decreasing step rate, the first half of the goal.
Constant step rate, the second half of the goal.

Significance

The result. Theorem 4 places SG under PL on the same footing as SG under strong convexity: the same $O(1/k)$ rate, with constants depending on $L$ , $\mu$ and $C$ only, and no convexity. Since PL holds for least squares with any design matrix and, over any compact set, for logistic regression (§2.3 of the paper), the theorem gives explicit SG rates for these models. The constant-step bound quantifies the practitioners' rule of halving the step when progress stalls: halving $\alpha$ at least halves the noise floor $LC^2\alpha/(4\mu)$ .

Formalizing it. The result is proved, in a short argument, in the paper. To our knowledge no machine-checked proof exists: the existing Lean formalizations of SG rates on Prove2Me concern stationarity of non-convex objectives under a variance bound, a different noise model with a different conclusion. The remaining work is to formalize the paper's proof, which requires a usable treatment of expectations over an i.i.d. index sequence (conditioning the step from $x_k$ on the past) — infrastructure that every later analysis of a stochastic first-order method can reuse.

Difficulty

The deterministic content is elementary: the descent lemma, unbiasedness, the PL inequality, a telescoping sum and a geometric series. The difficulty is probabilistic bookkeeping. Recursion (10) takes the expectation of a one-step inequality with respect to $i_k$ alone, holding $x_k$ fixed; this is legitimate because $i_k$ is independent of $i_0,\dots,i_{k-1}$ , of which $x_k$ is a function. Making this precise requires measurability of the iterates in the sample path and a Fubini-type decomposition of the product law into the first $k$ coordinates, the $k$ -th coordinate and the rest. A second subtlety is that the second-moment bound holds only at the iterates, not at every point, so the one-step bound must be applied pointwise in the path, on a set of full measure, rather than once and for all.

Formalization scope

The space is EuclideanSpace ℝ (Fin d) and $\nabla$ is Mathlib's gradient. The index law is an arbitrary probability measure $\nu$ on a measurable space, and the path law is the infinite product Measure.infinitePi (fun _ => ν); the run is a deterministic function sgRun of the path. The Lipschitz-gradient assumption is stated literally on $\nabla f$ ; the PL inequality is the published predicate ShiOptRates.PolyakLojasiewicz f (gradient f) μ (f xstar) (inequality (3) multiplied by 2); the solution set is a point xstar with ∀ y, f xstar ≤ f y, and $f^*$ is f xstar, never a free real.

Every expectation of a gap is a lower Lebesgue integral of $\max(f(x_k)-f^*,0)$ with values in $[0,\infty]$ , which equals $\mathbb E[f(x_k)-f^*]$ because $f^*$ is the minimum; no integrability side condition can make a bound hold by default. The second-moment bound is the lower Lebesgue integral of $\|\nabla f_i(x_k)\|^2$ , required for almost every path and every $k$ . Unbiasedness and problem (7) carry explicit integrability, so a non-integrable gradient cannot turn them into trivialities.

The second-moment bound is deliberately not imposed at every point $x$ . With the bound at every point, $\|\nabla f\|\le C$ everywhere, so $f-f^*\le C^2/(2\mu)$ by PL, while along the gradient-ascent flow $f-f^*$ grows exponentially unless it vanishes; hence $f$ would be constant and the theorem vacuous. Along the iterates the hypothesis is met by non-constant objectives such as $f(x)=\tfrac12\|x\|^2$ .

Additions relative to the page, all disclosed in the statements: each $f_i$ is differentiable; $(i,x)\mapsto\nabla f_i(x)$ is jointly measurable, so that the iterates are random variables; the constant step is positive; the decreasing-step rate is stated for $k\ge1$ ; and "each $f$ has an $L$ -Lipschitz continuous gradient" is read as a condition on $f$ , the only one the proof uses. The page's proof of the constant-step bound writes the exponent $k$ where $k+1$ is meant; the statements follow the theorem's (correct) form.

Contributions welcome: the measurability of the run, the conditioning step for infinitePi, the deterministic one-step bound, and the two scalar recursions, each of which is reusable for other SG analyses.

Selected references

H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition, ECML PKDD 2016; arXiv:1608.04636v4, 2020. https://arxiv.org/abs/1608.04636
B. T. Polyak, Gradient methods for minimizing functionals, USSR Computational Mathematics and Mathematical Physics 3(4), 1963. https://doi.org/10.1016/0041-5553(63)90382-3
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4), 2009. https://doi.org/10.1137/070704277
F. Bach, E. Moulines, Non-strongly-convex smooth stochastic approximation with convergence rate O(1/n), NeurIPS 2013. https://arxiv.org/abs/1306.2119

7 thms2 active usersReviewed

Convex Optimization·Captain: mikedeng1

Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming 1: The AG Method Converges on Smooth Nonconvex Problems and Attains the Optimal Rate When Ψ Is ConvexResearch Paper

Motivation

Accelerated gradient (AG) methods go back to Nesterov (1983), who showed that a first-order method with a momentum-like extrapolation reaches an $\epsilon$ -optimal value of a smooth convex function in $O(1/\sqrt\epsilon)$ iterations, against $O(1/\epsilon)$ for gradient descent, and that this rate is optimal among first-order methods. Many objectives met in practice (training losses, nonconvex penalties, problems with unknown convexity) are smooth but not convex. For those, gradient descent is known to drive the gradient norm to zero, with $\min_{k\le N}\|\nabla\Psi(x_k)\|^2=O(1/N)$ , while the classical AG method has no convergence guarantee at all.

Saeed Ghadimi and Guanghui Lan (arXiv:1310.3787v1, 2013; Mathematical Programming 156, 2016) modified the AG method with a third step size and proved that one algorithm handles both cases: on a smooth nonconvex problem it has the gradient-descent rate for $\min_k\|\nabla\Psi\|^2$ , and when the problem turns out to be convex it keeps Nesterov's optimal rate for the optimality gap. This mission formalizes that result, Theorem 1 of the paper, and its proof path in §2.1.

Setting

Let $\Psi:\mathbb R^n\to\mathbb R$ be differentiable with Lipschitz gradient: there is $L_\Psi>0$ with

\|\nabla\Psi(y)-\nabla\Psi(x)\|\le L_\Psi\|y-x\|\qquad\forall x,y\in\mathbb R^n, \tag{1.2}

and bounded from below, with $\Psi^*=\inf_x\Psi(x)$ (problem (1.1)). $\Psi$ need not be convex.

Algorithm 1 (AG). The inputs are a starting point $x_0$ and step sizes $\{\alpha_k\},\{\beta_k\},\{\lambda_k\}$ , $k\ge1$ , with $\alpha_1=1$ , $\alpha_k\in(0,1)$ for $k\ge2$ , $\beta_k>0$ and $\lambda_k>0$ . Set $x^{ag}_0=x_0$ and, for $k=1,2,\dots$ ,

x^{md}_k=(1-\alpha_k)x^{ag}_{k-1}+\alpha_kx_{k-1},\qquad x_k=x_{k-1}-\lambda_k\nabla\Psi(x^{md}_k),\qquad x^{ag}_k=x^{md}_k-\beta_k\nabla\Psi(x^{md}_k).

One gradient is evaluated per iteration, at the middle point $x^{md}_k$ ; $x_k$ takes a long step $\lambda_k$ and the aggregated point $x^{ag}_k$ a short step $\beta_k$ . With $\beta_k=\lambda_k$ the method reduces to gradient descent, with $\beta_k=\alpha_k\lambda_k$ to a variant of Nesterov's method.

The weights are $\Gamma_1=1$ , $\Gamma_k=(1-\alpha_k)\Gamma_{k-1}$ ( $k\ge2$ ), and for a horizon $N$ and $1\le k\le N$

C_k=1-L_\Psi\lambda_k-\frac{L_\Psi(\lambda_k-\beta_k)^2}{2\alpha_k\Gamma_k\lambda_k}\Big(\sum_{\tau=k}^N\Gamma_\tau\Big).

Formalization targets

Goal: Theorem 1 (p. 5)

Fix $N\ge1$ .

a) If $C_k>0$ for $k=1,\dots,N$ , then

\min_{k=1,\dots,N}\|\nabla\Psi(x^{md}_k)\|^2\le\frac{\Psi(x_0)-\Psi^*}{\sum_{k=1}^N\lambda_kC_k}.

b) If $\Psi$ is convex with a minimizer $x^*$ , and for $k=1,\dots,N$ one has $\alpha_k\lambda_k\le\beta_k<1/L_\Psi$ and $\alpha_1/(\lambda_1\Gamma_1)\ge\alpha_2/(\lambda_2\Gamma_2)\ge\dots$ , then

\min_{k=1,\dots,N}\|\nabla\Psi(x^{md}_k)\|^2\le\frac{\|x_0-x^*\|^2}{\lambda_1\sum_{k=1}^N\Gamma_k^{-1}\beta_k(1-L_\Psi\beta_k)},\qquad \Psi(x^{ag}_N)-\Psi(x^*)\le\frac{\Gamma_N\|x_0-x^*\|^2}{2\lambda_1}.

The theorem leaves the step-size policy open: any sequences meeting the conditions are covered, and the rates of Corollary 1 ( $O(1/N)$ in part a, $O(1/N^2)$ for the gap in part b) follow by substitution.

Milestones

The milestones follow the proof in §2.1: the quadratic bound (2.1); Lemma 1, which unrolls the recursion $\theta_k\le(1-\alpha_k)\theta_{k-1}+\eta_k$ ; the nonconvex chain (2.13), (2.15), the identity for $x^{ag}_k-x_k$ , (2.16), (2.17), (2.18) and (2.19); and the convex chain (2.20)–(2.25).

Significance

The result. Theorem 1 is the first convergence guarantee for an accelerated gradient method on nonconvex smooth problems. It shows that acceleration costs nothing in the nonconvex case (the same $O(1/N)$ rate for the squared gradient norm as gradient descent) while keeping the optimal $O(1/N^2)$ gap when the function is convex, so a user need not know in advance which case holds. The same analysis is the template for the composite and stochastic results of the paper (Theorems 2–4) and for the later literature on accelerated methods for nonconvex optimization.

Formalizing it. The theorem is proved on paper; it is not known to have a machine-checked proof. The mission produces a Lean definition of the AG run with its three step sizes, a formal Lemma 1 (a reusable tool for any Nesterov-type analysis), and the two chains of estimates with all constants explicit. These pieces are reused by the composite and stochastic missions of the same paper.

Difficulty

The standard analysis of Nesterov's method is an estimate-sequence or potential argument that relies on convexity at every step: it bounds $\Psi(x^{md}_k)$ below by a linearization. Without convexity that lower bound fails, and the potential need not decrease. Part a) instead tracks the decrease of $\Psi$ along the $x_k$ sequence, where gradients are evaluated at a different point $x^{md}_k$ ; the error this creates is governed by the gap $x^{ag}_k-x_k$ , which accumulates all past gradients with weights $\Gamma_k/\Gamma_\tau$ . Controlling that accumulated term, and showing it is absorbed by the condition $C_k>0$ with $C_k$ depending on the horizon $N$ , is the delicate step. Part b) needs the monotonicity (2.10) to turn a weighted telescoping sum into a single initial-distance term.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). The gradient is an explicit map g, tied to $\Psi$ by the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth Ψ g LΨ (differentiable with gradient $g$ , and (1.2)); $L_\Psi>0$ as in (1.2). The quadratic bound (2.1) is the published, proved ConvexOptAlg.SmoothGD.lemma_3_4.
The run is a definition (agRun, with xSeq, xagSeq, xmdSeq), computed by (2.2)–(2.4) from $x_0$ ; indices are 1-based as in the paper. $\Gamma_k=\prod_{i=2}^k(1-\alpha_i)$ , so $\Gamma_1=1$ . $C_k$ is C LΨ α β lam N k and depends on $N$ .
"Bounded from below" is BddBelow (Set.range Ψ) and $\Psi^*$ is ⨅ x, Ψ x. The minimum over $k=1,\dots,N$ is Finset.inf' over Finset.Icc 1 N with $N\ge1$ . Convexity is ConvexOn ℝ Set.univ Ψ; $x^*$ is any global minimizer.
Conditions (2.7), (2.9), (2.10) are imposed for $k=1,\dots,N$ only.
Trivializing formalizations are excluded: the conclusion is about the AG run itself, not an arbitrary sequence; $g$ is the gradient of $\Psi$ ; $\Gamma_1=1$ , not $0$ (with which every bound would divide by zero); and the minimum ranges over $k\le N$ , not over all $k$ .

Welcome contributions: proofs of Lemma 1 and of the algebraic milestones (the identity before (2.16), (2.16), (2.17), (2.22), (2.25)), which are independent of $\Psi$ ; then the descent chains; then Theorem 1.

Selected references

S. Ghadimi, G. Lan, Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming, arXiv:1310.3787v1, 2013; Math. Program. 156 (2016) 59–99. https://arxiv.org/abs/1310.3787
Y. E. Nesterov, A method for unconstrained convex minimization problem with the rate of convergence O(1/k²), Doklady AN SSSR 269 (1983) 543–547.
Y. E. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
S. Bubeck, Convex Optimization: Algorithms and Complexity, Found. Trends Mach. Learn. 8 (2015), arXiv:1405.4980. https://arxiv.org/abs/1405.4980

18 thms2 active usersReviewed

Combinatorics Operations Research Probability·Captain: mikedeng1

Online Contention Resolution Schemes with Applications to Bayesian Selection Problems 2: The Degree Relaxation of Matching Has a (b, e^(−2b))-Selectable Randomized Greedy OCRSResearch Paper

Why online matching needs a stronger rounding guarantee

In online selection, candidate items reveal themselves one at a time and an algorithm must decide immediately whether to keep each one. When the kept items must form a matching, accepting one edge can prevent a later edge sharing an endpoint from being accepted. A fractional solution supplies useful marginal probabilities, but it does not by itself specify which active edges can be kept under an unfavorable arrival order. Online contention resolution schemes provide that missing rounding step: they turn independent edge activity into a feasible online selection while guaranteeing each edge a chance of selection. Feldman, Svensson, and Zenklusen introduced the strong selectability guarantee used here, which protects an edge even against an arrival order chosen with knowledge of all random outcomes (Feldman–Svensson–Zenklusen, §1.1).

This mission isolates the matching result of their paper. It concerns a degree relaxation that is weaker than the full matching polytope, so the result applies even when the input fractional point satisfies only local vertex constraints. The source states the existence theorem as Theorem 2.7 and gives its numerical guarantee explicitly (Theorem 2.7, p. 13).

Finite graphs, fractional edges, and greedy families

Let $G=(V,E)$ be a finite graph. An edge $g$ has two distinct endpoints; multiple edges may have the same endpoints. A matching is a set of edges with no shared vertex. For a vertex $u$ , write $\delta(u)$ for its incident edges. The degree relaxation is

P_G=\left\{x\in\mathbb R_{\ge0}^{E}:\sum_{g\in\delta(u)}x_g\le1\text{ for every }u\in V\right\}.

Since each edge meets a vertex, these constraints also give $x_g\le1$ . Every matching has a characteristic vector in $P_G$ . The degree relaxation can contain points outside the convex hull of matchings, which makes the theorem stronger than a statement restricted to the matching polytope (§2.2, p. 13).

For $x\in[0,1]^E$ , the active set $R(x)$ includes each edge $g$ independently with probability $x_g$ . A greedy family $\mathcal F_x$ is a downward closed family of matchings containing the empty set. A greedy online scheme accepts an active edge if adding it to the already accepted set remains in $\mathcal F_x$ . The family may itself be random, sampled independently of $R(x)$ .

An edge $g$ is selectable for a realized active set and greedy family when every member $I\in\mathcal F_x$ with $I\subseteq R(x)$ can be extended by $g$ while staying in $\mathcal F_x$ . Thus selectability promises acceptance regardless of which eligible active edges preceded $g$ . A scheme is $(b,c)$ -selectable if this event has probability at least $c$ for every $x\in bP_G$ and every edge. The probability includes both the active-set draw and any random family draw (Definitions 1.3–1.5, pp. 3–4).

Formalization targets

Theorem 2.7: a randomized matching scheme

For every $b\in[0,1]$ and every finite loopless graph $G$ ,

\exists\text{ a randomized greedy scheme for }P_G\text{ that is }(b,e^{-2b})\text{-selectable}.

Equivalently, for each $x\in bP_G$ and each edge $g\in E$ , the probability that $g$ is selectable is at least $e^{-2b}$ . The statement includes edges with $x_g=0$ ; the selectability event concerns the ability to add an edge, rather than the probability that it becomes active. The milestones are the steps the source states in its proof, in attack order (proof of Theorem 2.7, pp. 13–14):

for $t>0$ , $0\le(1-e^{-t})/t\le1$ , so that an edge can be put into a random set $K$ of potential edges with probability $(1-e^{-x_g})/x_g$ ;
drawing $K$ this way and using the matchings inside $K$ as the family is a randomized greedy scheme;
an edge $g'$ with ends $u,v$ is selectable exactly when $g'\in K$ and $A\cap K\cap(\delta(u)\cup\delta(v)\setminus\{g'\})=\varnothing$ ;
the probability of that event equals $\frac{1-e^{-x_{g'}}}{x_{g'}}\,e^{-\sum_{g\in\delta(u)\cup\delta(v)\setminus\{g'\}}x_g}$ ;
for $x\in bP_G$ , $\sum_{g\in\delta(u)\cup\delta(v)\setminus\{g'\}}x_g\le2(b-x_{g'})$ ;
for $t>0$ , $e^{t}(e^{t}-1)/t\ge1$ .

Remark (p. 14): the deterministic variant

Taking $K=E$ , the deterministic greedy scheme whose family is the set of all matchings is $(b,(1-b)^2)$ -selectable for $P_G$ , $b\in[0,1]$ :

\Pr_{A\sim R(x)}\big[g\text{ is selectable for }A\big]\ \ge\ (1-b)^2\qquad\forall x\in bP_G,\ \forall g\in E.

This companion is weaker than Theorem 2.7 for every $b\in(0,1]$ and is not used by it (Remark, p. 14).

What the result contributes

The theorem gives a constant probability bound against the paper's strongest, “almighty” arrival-order adversary. The guarantee is available from vertex degree inequalities alone. Consequently it applies to points of the exact matching polytope as well, without asking the online rounding procedure to exploit its additional odd-set inequalities. The paper places this result beside analogous existence claims for matroids and knapsacks in Theorem 1.8, and uses greedy schemes as components in more general selection results (Theorem 1.8, p. 4).

The existence theorem is proved in the source; it is an open formalization target here. A completed Lean development would supply a reusable finite model of independent active sets, random greedy families, edge selectability, and matching degree relaxations. It would also put the exact $e^{-2b}$ constant and its endpoint cases under machine checking. The definitions can support future formalizations of the paper's combination and application results, although this mission claims only Theorem 2.7 and its local proof milestones.

Where the argument is delicate

The local degree constraints bound the fractional weight at each endpoint separately, while selectability must survive conflicts at either endpoint under any arrival order. Merely ensuring that the algorithm outputs a matching gives no lower bound for a particular edge: the adversary can expose competing active edges first. The theorem therefore asks for a stronger event that certifies an edge could be added after every eligible previously selected matching. The numerical guarantee must hold uniformly over all edges, even when a coordinate is zero (Definitions 1.4–1.5, pp. 3–4; proof of Theorem 2.7, p. 13).

Formalization scope

The ground set is the finite edge type $E$ . The published EdmondsMatching65.Polyhedron.Graph structure represents a graph by a map from edges to unordered pairs of vertices and includes a proof excluding self-loops; its matching predicate is reused directly. This admits parallel edges, a harmless generalization of the page's graph language. Incident edge sets and matchings are finite sets. The polytope is the set of real edge vectors satisfying precisely the nonnegativity and vertex degree inequalities above. Scaling is the pointwise set operation $bP_G$ , so $b=0$ remains meaningful. The parameter range $0\le b\le1$ is explicit.

Probability is represented by finite sums of product weights. A randomized scheme is a weight function on finite greedy families, independent of the active-set draw. Each family contains the empty set and lies inside the matchings; allowing an empty family would make selectability vacuous. The degree inequalities keep relevant coordinates in $[0,1]$ , so active-set weights are genuine probabilities. The source's ratio $(1-e^{-x_g})/x_g$ is given its continuous value $1$ at $x_g=0$ . For inputs outside the nonnegative domain, which the theorem never uses, that inclusion probability is also assigned $1$ to keep the distribution well formed. These choices and the loopless graph convention are recorded with the draft statements.

The formalization needs finite product probability identities, elementary exponential inequalities, and set facts about matchings and incident edges. Contributions proving the six listed milestones, the deterministic Remark, or the full existential theorem are welcome. The finite model of active sets, greedy families and selectability is shared with the other missions of this series (matroids, knapsack, combinations of schemes, submodular rounding).

Selected references

Moran Feldman, Ola Svensson, and Rico Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015, preprint. Published as Online Contention Resolution Schemes with Applications to Bayesian Selection Problems, SIAM Journal on Computing, 2021.

11 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization·Captain: mikedeng1

Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness III: Adaptive Restarts Take at Most ⌈2C(q+2)/(αβ)⌉ Inner Steps and Converge Linearly on Sharp ProblemsResearch Paper

Motivation

First order primal–dual algorithms are used when a linear program is too large for a direct factorization or when matrix operations are cheaper than solving a sequence of linear systems. Their basic guarantees often bound an averaged duality gap by a quantity proportional to $1/t$ after $t$ steps. A restart discards the current inner iteration history and begins again from an averaged output. For problems with a suitable error bound, restarts can turn sublinear progress into geometric decrease in distance to the solution set. Applegate, Hinder, Lu and Lubin analyze this mechanism for a class that includes proximal point, extragradient, primal–dual hybrid gradient and ADMM methods, with constants listed in their Table 1. Their adaptive rule is useful when the sharpness constant is unavailable to the algorithm designer. Applegate et al., arXiv:2105.12715v4, §§2–4

Setting

Let $X\subseteq\mathbb R^n$ and $Y\subseteq\mathbb R^m$ be closed convex sets. The primal–dual problem is $\min_{x\in X}\max_{y\in Y}L(x,y)$ , where $L$ is differentiable, convex in $x$ and concave in $y$ . A point $z=(x,y)$ is feasible when $z\in Z=X\times Y$ . Its saddle-point set $Z^\star$ contains the feasible pairs satisfying $L(x,y')\le L(x,y)\le L(x',y)$ for every $x'\in X$ and $y'\in Y$ . Distances and balls use a chosen seminorm $\|\cdot\|_p$ ; this matters for methods whose natural geometry is degenerate. Applegate et al., arXiv:2105.12715v4, pp. 2–3

For $r>0$ , put $W_r(z)=\{\hat z\in Z:\|z-\hat z\|_p\le r\}$ . The normalized duality gap is $\rho_r(z)=\sup_{\hat z\in W_r(z)}[L(x,\hat y)-L(\hat x,y)]/r$ . At $r=0$ it is the upper limit as positive radii decrease to zero. The gap can be infinite under a seminorm, so its values are extended real. A problem is $\alpha$ -sharp on $S\subseteq Z$ when $\alpha\operatorname{dist}_p(z,Z^\star)\le\rho_r(z)$ for every $z\in S$ and every $0<r\le\operatorname{diam}_p(S)$ . This condition connects a computable local gap to the distance of interest. Applegate et al., arXiv:2105.12715v4, pp. 3, 11, (4), Definition 1

The base algorithm begins at $z^0\in Z$ and supplies averaged outputs $\bar z^t$ for positive inner times $t$ . Property 3 requires constants $q,C>0$ , uniform over every feasible start and output run, for which $\bar z^t\in Z$ , $\rho_{\|\bar z^t-z^0\|_p}(\bar z^t)\le2C\|\bar z^t-z^0\|_p/t$ , and $\|\bar z^t-z^0\|_p\le(q+2)\operatorname{dist}_p(z^0,Z^\star)$ . An outer run starts at $z^{k,0}$ , runs its inner algorithm for $\tau^k$ steps, and sets $z^{k+1,0}=\bar z^{k,\tau^k}$ . Its first length $\tau^0\ge1$ is selected by the user. At later outer indices, it restarts at the first positive time when the normalized gap has fallen below $\beta$ times the gap at the previous outer transition, with $0<\beta<1$ . Applegate et al., arXiv:2105.12715v4, pp. 9–10, 15–16, Property 3, Algorithm 1, (30)

Formalization targets

The goal is both parts of Theorem 2. Assume all outer starts lie in one set $S$ on which the problem is $\alpha$ -sharp, with $\alpha>0$ . Define the ceiling time $t^\star=\left\lceil2C(q+2)/(\alpha\beta)\right\rceil$ . For every $k\ge1$ the target is

\tau^k\le t^\star, \qquad \operatorname{dist}_p(z^{k,0},Z^\star) \le\beta^k\frac{t^\star}{\tau^0}\operatorname{dist}_p(z^{0,0},Z^\star).

The milestones are Proposition 8's treatment of zero displacement, the displayed restart comparison in the proof of (33), the bound (33) itself, and the repeated normalized-gap inequality in the proof of part (ii). Each is tied to the arXiv version's printed page and label. The assertion begins at $k=1$ : the first interval is free and need not be at most $t^\star$ . Applegate et al., arXiv:2105.12715v4, pp. 17–18

Significance

The first conclusion gives a uniform bound on the inner work of every subsequent adaptive interval. The second translates the gap-based restart rule into a geometric distance guarantee while retaining the user-selected first interval as a visible factor. Together, they explain why an algorithm that does not know $\alpha$ can have the same characteristic restart scale as one using a fixed frequency chosen from $\alpha$ . The paper proves this theorem and gives linear-programming settings in which its sharpness premise holds; this mission asks for a machine-checked statement and, eventually, a machine-checked proof of that known result. Applegate et al., arXiv:2105.12715v4, Theorems 1–2 and Lemma 5

Formalizing the result also produces reusable interfaces for saddle sets, seminorm distances, localized duality gaps, uniform algorithm properties, and first-trigger restart runs. Those interfaces can support other primal–dual analyses without committing to a particular inner update map. A complete proof can later connect Property 3 to the paper's individual algorithms, while this mission preserves the abstract theorem that they share. Applegate et al., arXiv:2105.12715v4, Proposition 4 and §4

Difficulty

The restart test uses a gap evaluated at the moving radius $\|\bar z^{k,t}-z^{k,0}\|_p$ , whereas sharpness relates a gap at the radius of the previous outer transition to distance from $Z^\star$ . This mismatch must be reconciled while preserving the exact ceiling constant. A zero seminorm displacement is a separate boundary case: sharpness only speaks about positive radii, but the algorithm can still encounter radius zero. The theorem also needs the first qualifying time; knowing merely that a later time satisfies the test gives no upper bound on the interval length. Applegate et al., arXiv:2105.12715v4, pp. 16–18

Formalization scope

Lean represents $x$ and $y$ by finite-dimensional Euclidean spaces and $z$ by their product, allowing either dimension to be zero. The geometry on that product is an explicit Seminorm, never the product type's default norm. $Z^\star$ is the set of saddle pairs. The standing problem predicate includes closed convex feasible sets, separate convexity and concavity, and differentiability on the whole ambient product space. It also requires $Z^\star\ne\varnothing$ , a disclosed strengthening of the paper's standing feasibility and finite-optimum assumptions so the real-valued distance to $Z^\star$ cannot collapse to an empty-infimum default. The infimum defining distance is over saddle points only; the supremum defining the gap is over feasible pairs only. The normalized gap and diameter use extended reals so an unbounded seminorm ball does not silently acquire value zero. Applegate et al., arXiv:2105.12715v4, pp. 2–4

The base method is a relation from a start to possible averaged-output sequences. Property 3 fixes $q,C$ before quantifying over starts, runs and positive times. The theorem assumes initial feasibility; Property 3 then makes restarted outer points feasible. An adaptive run records the positive first interval and the first qualifying positive time for each later interval. The ceiling is Nat.ceil; the factor $t^\star/\tau^0$ is division in the reals. A formalization with arbitrarily chosen qualifying restart times, sharpness only along one chosen trajectory, a real-valued supremum over an unbounded ball, or a vacuous solution set would change the result. Contributions to the gap and seminorm infrastructure and to either half of Theorem 2 are useful; the individual algorithm implementations are outside this mission's core. Applegate et al., arXiv:2105.12715v4, pp. 9–10, 16–18

Selected references

D. Applegate, O. Hinder, H. Lu and M. Lubin, Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness, Mathematical Programming, 2022; mission citation basis: arXiv:2105.12715v4.

8 thms2 active usersReviewed

Probability·Captain: visuddhi

VC Theory for Inventory Policies: Xie–Ma–Xin BoundsResearch Paper

Learning inventory policies from historical demand

An inventory policy chooses how much stock to order before demand is observed. Its quality is assessed by the holding and backlogging costs it incurs on future demand. A policy chosen to perform well on historical demand can overfit those observations. A useful statistical guarantee therefore controls the difference between historical and future costs simultaneously over the policies that the procedure may select. Xie, Ma and Xin establish such guarantees for stationary base-stock, $(s,S)$ , and nonstationary base-stock policy classes.

This formalization covers the principal bound families in that paper. Its first goal is the expected generalization and estimation bound for nonstationary base-stock policies with no fixed ordering cost, Corollary 4.10. Its supporting targets include Theorem 4.9 and the constructive product-sample partition in Lemma 4.12. The other principal bounds remain in the explicit scope below and await their own full Lean declarations. The companion inventory-information project needs these results as proved dependencies; merely citing the paper does not close that project's formal proof obligations.

Demand, policy classes and statistical errors

There are $T+L$ periods, a deterministic lead time $L\ge0$ , and demand bounded by $U>0$ . The first order arrives in period $L+1$ . Average loss means the sum of holding and backlogging costs in periods $L+1,\ldots,T+L$ , divided by the positive horizon $T$ . The initial pipeline is empty, and initial inventory is nonpositive for the base-stock models. Holding and backlogging cost coefficients are $h,b\in[0,1]$ . Nonstationary base-stock policies in the first goal have no fixed ordering cost and use levels $S^t\in[0,(L+1)U]$ .

The Lean model indexes the first period by zero. It uses the source's explicit finite-maximum formula for post-replenishment inventory, with the demand interval summed up to, but excluding, the observation period. In mathematical notation the inventory in period $L+k+1$ is $\max_{0\le j\le k}(S_j-\sum_{j\le r<k+L}d_r)$ . Cost is evaluated after subtracting the current demand $d_{L+k}$ . This is a backlog model; applications to lost sales require a separate equivalence argument.

Data comprise $N>0$ IID demand trajectories from a probability measure $\mu$ on the bounded trajectory space. Different periods of the same trajectory can be dependent. Generalization error is the one-sided supremum $\mathrm{GE}=\sup_S(R(S)-\widehat R(S))$ , where $R$ is expected average loss and $\widehat R$ is empirical average loss. Estimation error is $R(\widehat S)-R(S_*)$ , for an empirical minimizer and a best-in-class population policy. It is not the error relative to every history-dependent inventory policy. These conventions follow Sections 3 and 4.

Formalization targets

The first goal, Corollary 4.10, asserts the existence of one absolute constant $C>0$ such that

\mathbb E\mathrm{EE}\le\mathbb E\mathrm{GE}\le C(L+1)U/\sqrt N.

The constant is quantified before the horizon, lead time, support, costs, demand distribution, sample size, and policy selections. The first inequality explicitly refers to actual minimizers, with an integrable selected risk. The GE conclusion holds independently of whether a particular selector has been supplied.

Its principal complexity target is Theorem 4.9: for each relevant period and $0<\gamma\le1$ , the normalized inventory class has fat-shattering dimension at most $2/\gamma+1$ . The Lean statement says directly that every $\gamma$ -shattered indexed sample has cardinality at most that number. It uses the source convention of a strict upper label and non-strict lower label.

Lemma 4.12 partitions all $N^D$ product indices into $N^{D-1}$ groups of $N$ indices. Every coordinate of every group traverses the original row indices exactly once. The formal statement uses a bijection between anchor-offset pairs and complete index tuples, together with a coordinate-permutation assertion. The dimension $D=d+1$ is positive, and $N=1$ and $D=1$ are included.

The full scope also retains Theorem 4.1 and Corollary 4.2 (stationary policies), Theorem 4.4 and Corollary 4.5 ( $(s,S)$ upper bounds), Theorem 4.7 and Corollary 4.8 ( $(s,S)$ fat-shattering and GE lower bounds), and the expected Product ERM comparison in equation (4.7). They are catalogued with their assumptions but are not yet all encoded. The GE lower bound is not asserted to be a minimax policy-regret lower bound.

What the formalization supplies

The nonstationary policy vector grows with the horizon, while the expected average-loss bound has no horizon factor. A verified version supplies a reusable statistical ingredient for finite-horizon inventory learning. Total-cost bounds require multiplication by the horizon. Absolute uniform deviation, period-dependent costs, high-probability statements, initial-state reductions, and censoring require further bridge theorems. They are not attributed to Corollary 4.10 without those proofs.

The cyclic partition has a complete locally checked Lean proof with axiom dependencies only propext and Quot.sound. The two statistical targets remain open. Neither a drafted declaration nor a local proof is described as a server-verified contribution.

Mathematical difficulty

Ordinary pseudodimension can grow with the horizon for the nonstationary class, so it does not by itself give the desired horizon-free rate. A full proof needs scale-sensitive complexity, probability, and integration infrastructure. For Product ERM, coordinate independence must be explicit: the groups in the partition need not be independent of each other. The expected comparison transfers upper bounds; it cannot reverse direction to transfer a GE lower bound.

Formalization scope and conventions

The shared environment is Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Demand and policy coordinates are bounded real subtypes with their usual measurable structures. Probability is over IID whole trajectories. Finite maximum indices are nonempty. Positive $T,N,U$ prevent zero denominators in the targets. General definitions remain total, and their behavior outside these hypotheses is exposed in the independent read-backs.

Complete proofs must establish the boundedness and measurability needed for the real suprema and integrals to have their usual meaning. They may not assume the convergence bound, replace arbitrary probability measures by finite-support distributions, or silently restrict the policy class. The $(s,S)$ branch additionally needs explicit unbounded-domain conventions when holding or backlogging costs vanish. Reusable contributions include shattering, symmetrization, entropy bounds, selection and integrability facts, and finite-product sampling.

Selected references

Yaqi Xie, Will Ma and Linwei Xin, VC Theory for Inventory Policies, arXiv:2404.11509v3, 2026. https://arxiv.org/abs/2404.11509v3
Hanzhang Qin, David Simchi-Levi and Ruihao Zhu, Information Limits of Multistage Inventory Control: Learning, Valuation, and Censoring, arXiv:2609.37380v1, 2026. https://arxiv.org/abs/2609.37380v1

6 thms2 active usersReviewed

Convex Optimization Information Theory Quantum Information·Captain: mikedeng1

Semidefinite Programming Hierarchies for Constrained Bilinear Optimization I: The Linearly Constrained de Finetti SDP Hierarchy Satisfies Q ≤ SDPₙ ≤ Q + ‖G‖∞·d_B²(d_B+1)·√((2 ln 2) log d_A / n)Research Paper

Motivation

Many problems in quantum information theory ask for the maximum of a linear functional over pairs of quantum states, one on each of two systems, subject to linear constraints on each state. The best success probability of an approximate quantum error-correcting code of given size is of this form: the encoder and the decoder are quantum channels, their Choi matrices are states with fixed marginals, and the objective is bilinear in the two (Berta, Borderi, Fawzi & Scholz, arXiv:1810.12197, §4). Such constrained bilinear programs are nonconvex. Seesaw methods give lower bounds that often converge in practice, but they offer no guarantee of global optimality. What is needed is a hierarchy of efficiently computable outer bounds that converges to the optimum, with an explicit rate.

For the unconstrained problem, the optimisation over separable states, such a hierarchy is classical: the Doherty–Parrilo–Spedalieri hierarchy of $n$ -extendible states, whose convergence follows from finite quantum de Finetti theorems (Christandl, König, Mitchison & Renner 2007; Brandão & Harrow 2013). The standard de Finetti approximant is, however, a mixture of product states that need not satisfy the linear constraints, so it says nothing about the constrained problem. The paper proves a de Finetti theorem with linear constraints (Theorem 2.3) and derives from it a semidefinite hierarchy for constrained bilinear programs with a convergence guarantee (Theorem 3.1).

Setting

A $d$ -dimensional quantum system has operator space $\mathcal S=\mathbb C^{d\times d}$ ; a state is a positive semidefinite $W\in\mathcal S$ with $\mathrm{Tr}\,W=1$ . Let $A$ and $B$ be systems of dimensions $d_A$ and $d_B$ . The data are an objective $G_{AB}\in\mathcal S_A\otimes\mathcal S_B$ , arbitrary linear maps $\Lambda_{A\to C_A}:\mathcal S_A\to\mathcal S_{C_A}$ and $\Gamma_{B\to C_B}:\mathcal S_B\to\mathcal S_{C_B}$ , and matrices $X_{C_A}$ , $Y_{C_B}$ . The constrained bilinear program is

Q=\max\ \mathrm{Tr}[G_{AB}(W_A\otimes W_B)]\quad\text{s.t. } W_A,W_B\ \text{states},\quad \Lambda_{A\to C_A}(W_A)=X_{C_A},\quad \Gamma_{B\to C_B}(W_B)=Y_{C_B}.

For $n\ge1$ let $B_1,\dots,B_n$ be copies of $B$ . A state $W_{AB_1^n}$ on $A\otimes B_1\cdots B_n$ is symmetric with respect to $A$ if it is invariant under every permutation $\mathcal U^\pi_{B_1^n}$ of the copies $B_1,\dots,B_n$ , $\pi\in\mathfrak S_n$ . Write $W_{B_1^n}=\mathrm{Tr}_A W_{AB_1^n}$ , $W_{B_1^{n-1}}=\mathrm{Tr}_{B_n}W_{B_1^n}$ and $W_{AB_1}=\mathrm{Tr}_{B_2^n}W_{AB_1^n}$ . The level- $n$ program is

\mathrm{SDP}_n=\max\ \mathrm{Tr}[G_{AB}W_{AB_1}]\quad\text{s.t. } W_{AB_1^n}\ \text{a state, symmetric with respect to } A,

(\Lambda_{A\to C_A}\otimes\mathcal I_{B_1^n})(W_{AB_1^n})=X_{C_A}\otimes W_{B_1^n},\qquad (\mathcal I_{B_1^{n-1}}\otimes\Gamma_{B_n\to C_B})(W_{B_1^n})=W_{B_1^{n-1}}\otimes Y_{C_B}.

It is a semidefinite program of size polynomial in $d_A$ and $d_B^n$ .

The rate involves the trace norm $\|X\|_1=\mathrm{Tr}|X|$ , the Schatten $\infty$ -norm $\|G\|_\infty$ (largest singular value), and the minimal distortion with side information of $B$ ,

f(B|\cdot)=\inf_{\mathcal M_B}\ \sup_{\substack{\xi_{AB}^\dagger=\xi_{AB}\\ \xi_A=0,\ \xi_B=0}}\frac{\|\xi_{AB}\|_1}{\|(\mathcal I_A\otimes\mathcal M_B)(\xi_{AB})\|_1},

the infimum over measurements $\mathcal M_B$ on $B$ and the supremum over all finite-dimensional $A$ ; $f(A,B)$ is the analogue with product measurements $\mathcal M_A\otimes\mathcal M_B$ . Throughout, $\log$ is base 2.

Formalization targets

Goal: Theorem 3.1 with its explicit rate

Q\ \le\ \mathrm{SDP}_n\ \le\ Q+\|G_{AB}\|_\infty\,d_B^2(d_B+1)\sqrt{\frac{(2\ln2)\log d_A}{n}}\quad(n\ge1),\qquad Q=\lim_{n\to\infty}\mathrm{SDP}_n.

The page states $0\le\mathrm{SDP}_n-Q\le\mathrm{poly}(d)/\sqrt n$ with $d=\max\{d_A,d_B\}$ . The goal makes explicit the rate the proof gives.

Milestones, in attack order

Lemma 2.1 (p. 6): for a permutation-invariant classical-quantum state $\rho_{AZ_1^n}$ there is $0\le m<n$ with $\mathbf E_{z_1^m}\|\rho_{AZ_{m+1}|z_1^m}-\rho_{A|z_1^m}\otimes\rho_{Z_{m+1}|z_1^m}\|_1^2\le(2\ln2)\log d_A/n$ .
Lemma D.1 (p. 29): for a state two-design $\{P_z\}$ and $\mathcal M_B$ with effects $\frac{d_B}{t}P_z$ , $\|(\mathcal I_A\otimes\mathcal M_B)(\xi_{AB})\|_1\ge\|\xi_{AB}\|_1/(d_B^2(d_B+1))$ for every Hermitian $\xi_{AB}$ .
Existence of state two-designs in every dimension (p. 29).
$f(B|\cdot)\le d_B^2(d_B+1)$ (p. 6).
Conditional constraints (p. 8): the states obtained by measuring $B_1,\dots,B_m$ and conditioning satisfy $\Lambda(\rho_{A|z_1^m})=X_{C_A}$ and $\Gamma(\rho_{B_{m+1}|z_1^m})=Y_{C_B}$ .
Theorem 2.3 (p. 7): under the constraints of $\mathrm{SDP}_n$ , $\|\rho_{AB}-\sum_ip_i\sigma^i_A\otimes\omega^i_B\|_1\le\min\{f(A,B),f(B|\cdot)\}\sqrt{(2\ln2)\log d_A/n}$ with states $\Lambda(\sigma^i_A)=X_{C_A}$ , $\Gamma(\omega^i_B)=Y_{C_B}$ .
Eq. (3) (p. 2): $Q$ equals the maximum over mixtures of feasible product states.
Hölder step (p. 11): $\mathrm{Tr}[GW]\le\mathrm{Tr}[GV]+\|G\|_\infty\|W-V\|_1$ .
$0\le\mathrm{SDP}_n-Q$ (p. 11).

Significance

Theorem 3.1 turns a nonconvex problem into a sequence of semidefinite programs whose values decrease to the optimum at rate $O(1/\sqrt n)$ , with a constant that depends polynomially on $d_B$ and logarithmically on $d_A$ . Every level is a certified upper bound; together with any feasible point it brackets $Q$ . The same argument applied to channel fidelities gives converging outer bounds on the success probability of approximate quantum error correction (§4 of the paper), and the constrained de Finetti theorem is the key step there as well. Theorem 2.3 is of independent interest: it is the first finite de Finetti theorem in which the approximating separable state inherits linear constraints of the extension.

The results are proved in the paper; none of them has been machine-checked. A complete formalization requires the quantum relative entropy and mutual information with their chain rule, the quantum Pinsker inequality, state two-designs and their existence, and a weighted Hölder inequality for Schatten norms; most of this is absent from Mathlib, and each piece is reusable beyond this mission.

Difficulty

The obvious route measures every copy $B_i$ with a fixed informationally complete measurement and uses the resulting classical de Finetti statement. This approximates $\rho_{AB}$ by a mixture of product states, but the states in the mixture need not satisfy $\Gamma(\omega^i)=Y$ , and projecting them onto the constraint set destroys the error bound. The paper instead conditions on the outcomes of only $m$ copies and keeps $B_{m+1}$ quantum; the constraint on $B_n$ then transfers to the conditional state of $B_{m+1}$ by symmetry. Making this rigorous needs the chain rule of conditional mutual information with classical conditioning, and the distortion of the measurement must be bounded independently of the side system $A$ , which is what Lemma D.1 provides. The Schatten-norm estimate there is elementary but requires a weighted Hölder inequality and a careful choice of weight.

Formalization scope

Systems are finite index types: $A\otimes B_1\cdots B_N$ is indexed by Fin dA × (Fin N → Fin dB), $\otimes$ is Mathlib's Kronecker product, and the permutation action permutes the word in Fin N → Fin dB. States, trace norm and partial traces are the published definitions WildeQIT_IsDensityOperator, WildeQIT_traceNorm and WildeQIT_partialTrace. The linear maps $\Lambda$ , $\Gamma$ are arbitrary $\mathbb C$ -linear maps (not assumed positive or trace preserving), applied blockwise to one tensor factor. The objective is the real part of $\mathrm{Tr}[G\,W]$ , equal to $\mathrm{Tr}[G\,W]$ for Hermitian $G$ . Each "max" is the supremum of the set of objective values over the feasible set, never over all matrices. Wherever the page has $n\ge1$ copies of $B$ , the Lean has n + 1: SDPval … n is the page's $\mathrm{SDP}_{n+1}$ , and the bounds have denominator $n+1$ . The distortions $f(A,B)$ and $f(B|\cdot)$ take values in $[0,\infty]$ ; the standalone bound on $f(B|\cdot)$ assumes $d_B\ge1$ .

No feasibility hypothesis is added to the goal. The feasible sets of $Q$ and of every level are empty or nonempty together, and the empty case reads $0\le0\le0+\dots$ . The goal mentions only $Q$ , $\mathrm{SDP}_n$ , $G$ , $d_A$ , $d_B$ and $n$ ; a formalization in which $Q$ or $\mathrm{SDP}_n$ were free real numbers, or in which the de Finetti mixture was not required to satisfy the constraints, would be a different and much weaker statement.

Contributions are welcome at every milestone, and especially in the reusable infrastructure: quantum relative entropy and mutual information on matrices, the quantum Pinsker inequality, unitary and state designs, and Hölder inequalities for Schatten norms.

Selected references

M. Berta, F. Borderi, O. Fawzi, V. B. Scholz, Semidefinite programming hierarchies for constrained bilinear optimization, Mathematical Programming, 2021; arXiv:1810.12197v3. https://arxiv.org/abs/1810.12197
F. G. S. L. Brandão, A. W. Harrow, Quantum de Finetti theorems under local measurements with applications, STOC 2013. https://arxiv.org/abs/1210.6367
M. Christandl, R. König, G. Mitchison, R. Renner, One-and-a-half quantum de Finetti theorems, Communications in Mathematical Physics 273, 2007. https://arxiv.org/abs/quant-ph/0602130
A. C. Doherty, P. A. Parrilo, F. M. Spedalieri, Complete family of separability criteria, Physical Review A 69, 2004. https://arxiv.org/abs/quant-ph/0308032

17 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization·Captain: mikedeng1

Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness II: Fixed-Frequency Restarts Shrink the Distance to the Solution Set by β per Restart on Sharp ProblemsResearch Paper

Motivation

Linear programs at very large scale are increasingly solved by first-order primal-dual methods, which use only matrix-vector products instead of matrix factorizations. Such methods parallelize well and have a small memory footprint, but on their own they are slow to reach moderate or high accuracy. Applegate, Hinder, Lu and Lubin (arXiv:2105.12715, Math. Program. 2022) showed that periodically restarting a primal-dual method from the average of its iterates turns its sublinear ergodic rate into a linear rate on sharp problems, a class that contains every linear program. The analysis underlies PDLP, a restarted PDHG solver studied computationally by Applegate et al. (arXiv:2106.04756) and shipped in Google OR-Tools.

This mission formalizes the paper's first convergence theorem: with restarts at a fixed frequency, the distance from the restart points to the solution set shrinks by a factor $\beta$ per restart.

Setting

Let $X \subseteq \mathbb R^n$ and $Y \subseteq \mathbb R^m$ be closed convex sets and let $L(x, y)$ be differentiable, convex in $x$ and concave in $y$ . Problem (1) is

\min_{x \in X} \max_{y \in Y} L(x, y),

with feasible region $Z = X \times Y$ and primal-dual points $z = (x, y)$ . Its solution set $Z^\star$ is the set of saddle points $z^\star \in Z$ : $L(x^\star, y') \le L(x^\star, y^\star) \le L(x', y^\star)$ for all $x' \in X$ , $y' \in Y$ . Throughout, $Z^\star \neq \emptyset$ .

Distances are measured in a semi-norm $\|\cdot\|$ , which the paper allows in order to cover ADMM. Write $\operatorname{dist}(z, Z^\star) = \inf_{z^\star \in Z^\star}\|z - z^\star\|$ , $\operatorname{diam}(S) = \sup_{s, s' \in S}\|s - s'\|$ , and $W_r(z) = \{\hat z \in Z : \|z - \hat z\| \le r\}$ . The primal-dual gap (3) at $z$ is $\sup_{\hat z \in Z}\{L(x, \hat y) - L(\hat x, y)\}$ , and the normalized duality gap (4a)–(4b) is

\rho_r(z) = \frac{1}{r}\sup_{\hat z \in W_r(z)}\{L(x, \hat y) - L(\hat x, y)\} \quad (r > 0), \qquad \rho_0(z) = \limsup_{r \to 0^+}\rho_r(z).

By Definition 1, problem (1) is $\alpha$ -sharp on $S \subseteq Z$ if $\alpha\operatorname{dist}(z, Z^\star) \le \rho_r(z)$ for all $z \in S$ and all $r \in (0, \operatorname{diam}(S)]$ .

The base method is abstract. From a start $z^0$ it outputs averaged points $\bar z^t$ , $t \ge 1$ . It has Property 3 with constants $q, C > 0$ if, for every start $z^0 \in Z$ and every $t \ge 1$ , $\bar z^t \in Z$ and

i. $\rho_{\|\bar z^t - z^0\|}(\bar z^t) \le 2C\|\bar z^t - z^0\|/t$ ,

ii. $\|\bar z^t - z^0\| \le (q + 2)\operatorname{dist}(z^0, Z^\star)$ .

Algorithm 1 with fixed-frequency restarts (29) runs the base method from $z^{n,0}$ for

t^\star = \left\lceil \frac{2C(q+2)}{\alpha\beta}\right\rceil

steps, sets $z^{n+1,0} = \bar z^{n,t^\star}$ , and repeats, with $\beta \in (0, 1)$ .

Formalization targets

Goal: Theorem 1 (p. 17)

If the base method has Property 3 and (1) is $\alpha$ -sharp on $W_R(z^{0,0})$ with $R = \frac{q+2}{1-\beta}\operatorname{dist}(z^{0,0}, Z^\star)$ , then for every $n \ge 0$

\operatorname{dist}(z^{n,0}, Z^\star) \le \beta^n \operatorname{dist}(z^{0,0}, Z^\star). \tag{31}

Milestones

Proposition 5 (p. 11): for $z \in Z$ , $\rho_r(z)$ is non-increasing in $r \in [0, \infty)$ .
Proposition 6 (p. 11): for $z \in Z$ and $r \ge 0$ , the primal-dual gap at $z$ is zero if and only if $\rho_r(z) = 0$ .
Proposition 8 (p. 17): under Property 3, $\|\bar z^t - z^0\| = 0$ implies $\bar z^t \in Z^\star$ .
First display of the proof of Theorem 1 (p. 17): if (31) holds for all $n \le N$ , then $\|z^{N+1,0} - z^{0,0}\| \le R$ , so $z^{N+1,0} \in W_R(z^{0,0})$ .
Display (32) (p. 17): if $z^{N,0}, z^{N+1,0} \in W_R(z^{0,0})$ , then

\operatorname{dist}(z^{N+1,0}, Z^\star) \le \beta\operatorname{dist}(z^{N,0}, Z^\star).

Companion statements

Proposition 2 (p. 8) and Proposition 4 (p. 10) show where Property 3 comes from. A generic algorithm (6) with iterates $z^t$ and targets $\hat z^t$ has Property 1 with $C$ if $L(\hat x^{t+1}, y) - L(x, \hat y^{t+1}) \le \frac C2\|z - z^t\|^2 - \frac C2\|z - z^{t+1}\|^2$ for every $z \in Z$ (12). It has Property 2 with $q$ if $\|\hat z^t - z^t\| \le q\operatorname{dist}(z^t, Z^\star)$ or $\|\hat z^t - z^{t-1}\| \le q\operatorname{dist}(z^t, Z^\star)$ .

Proposition 2: Property 1 gives non-expansiveness $\|z^{t+1} - z^\star\| \le \|z^t - z^\star\|$ and the ergodic rate $L(\bar x^t, y) - L(x, \bar y^t) \le C\|z - z^0\|^2/(2t)$ .
Proposition 4: Properties 1 and 2 give Property 3 for the averages $\bar z^t = \frac1t\sum_{i=1}^t \hat z^i$ , with the same $q$ and $C$ .

Fact 1 (p. 11), that $r\rho_r(z)$ is non-decreasing in $r$ , is included as well.

Significance

Theorem 1 converts any primal-dual method with an $O(1/t)$ ergodic rate on the normalized duality gap into a linearly convergent method on sharp problems. The rate is $O\big(\frac{C}{\alpha}\log\frac1\epsilon\big)$ iterations to reach $\operatorname{dist}(z, Z^\star) \le \epsilon$ (Remark 3). Through Proposition 4 it applies to PPM, EGM, PDHG and ADMM. Combined with the paper's Lemma 5, which shows that linear programs are sharp with $\alpha$ the inverse of a Hoffman constant, it yields linear convergence of restarted PDHG for LP. The paper also shows that this rate matches a lower bound for a general class of primal-dual methods.

The result is proved in the paper. As far as is known, no part of it, and no normalized duality gap or primal-dual sharpness notion, has a machine-checked proof. The mission adds a checked version of the restart argument, with every degenerate case resolved: zero displacements, unbounded balls, and semi-norms that are not norms.

Difficulty

Each proof is short, but the statements are delicate in ways the paper passes over.

The paper's argmax over $W_r(z)$ need not exist under a semi-norm, and $\rho_r(z)$ may be $+\infty$ . Proposition 5 therefore has to be proved with suprema, through the convex-combination scaling $z + \frac{r_1}{r_2}(\hat z - z)$ , not with a maximizer.
Sharpness is only available at radii in $(0, \operatorname{diam}(W_R(z^{0,0}))]$ and only at points of $W_R(z^{0,0})$ . So the induction in Theorem 1 must carry two facts together: the contraction (31), and the fact that every restart point stays in $W_R(z^{0,0})$ .
The step size $r = \|z^{N+1,0} - z^{N,0}\|$ may be zero, which is why Proposition 8, and through it Propositions 5 and 6 at $r = 0$ , is needed.

A direct contraction argument that applies sharpness at an arbitrary radius, or on all of $Z$ , does not prove the theorem as stated.

Formalization scope

$\mathbb R^n$ and $\mathbb R^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). $n = 0$ and $m = 0$ are allowed.
The semi-norm is an arbitrary Seminorm ℝ on their product, never the product's built-in norm.
The primal-dual gap, $\rho_r$ and $\operatorname{diam}$ are suprema in EReal, so unbounded sets give $+\infty$ and not a junk $0$ . $\operatorname{dist}(\cdot, Z^\star)$ is a real infimum over the nonempty set $Z^\star$ .
The base method is a map from starts to sets of admissible output sequences, because a primal-dual step can be an argmin and need not be single-valued. Property 3 quantifies over every start in $Z$ and every run, with $q$ and $C$ fixed first.
The restart length is the natural number $\lceil 2C(q+2)/(\alpha\beta)\rceil$ , and every inner loop has exactly this length.

Standing assumptions and added hypotheses:

$X$ and $Y$ are closed and convex, and $L$ is convex-concave and differentiable on the whole space.
$Z^\star \neq \emptyset$ replaces the page's "non-empty feasible region and bounded optimal value".
$\alpha > 0$ is assumed.
Property 1 is required for every $t \ge 0$ , although the paper's $\mathbb N$ starts at one: the proof of Proposition 2 telescopes from $z^0$ .
The iterates of a generic algorithm stay in $Z$ , which the page leaves implicit.

Departures from the page:

Proposition 8 asserts only $\bar z^t \in Z^\star$ . The page's " $\bar z^{n,t} = z^{n,0}$ " does not follow under a semi-norm.
Milestones that do not use a standing assumption drop it.

The goal is not trivialized by its hypotheses. A companion check file exhibits $L(x, y) = xy$ on $\mathbb R \times \mathbb R$ , with the sup norm and an oracle base method, on which every hypothesis of Theorem 1 holds and $\operatorname{dist}(z^{0,0}, Z^\star) = 1$ . Sharpness is assumed only where Definition 1 and the theorem assume it: replacing $W_R(z^{0,0})$ by $Z$ , or the radius range by all $r > 0$ , would weaken the theorem.

A complete development needs elementary facts about suprema in EReal, Jensen's inequality for convex-concave functions on averages, and geometric sums. The definitions of $\rho_r$ , sharpness and Property 3 are reusable for the adaptive-restart theorem of the same paper (Theorem 2, a separate mission) and for other restart analyses. Proofs of any milestone or companion are welcome.

Selected references

D. Applegate, O. Hinder, H. Lu, M. Lubin, Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness, Math. Program. (2022); arXiv:2105.12715v4. https://arxiv.org/abs/2105.12715 · https://doi.org/10.1007/s10107-022-01901-9
D. Applegate, M. Díaz, O. Hinder, H. Lu, M. Lubin, B. O'Donoghue, W. Schudy, Practical Large-Scale Linear Programming using Primal-Dual Hybrid Gradient, NeurIPS 2021. https://arxiv.org/abs/2106.04756
A. Chambolle, T. Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, J. Math. Imaging Vision 40 (2011). https://doi.org/10.1007/s10851-010-0251-1
A. Nemirovski, Prox-Method with Rate of Convergence O(1/t) for Variational Inequalities with Lipschitz Continuous Monotone Operators and Smooth Convex-Concave Saddle Point Problems, SIAM J. Optim. 15 (2004). https://doi.org/10.1137/S1052623403425629

8 thms2 active usersReviewed

Completed

Machine Learning Operations Research Probability·Captain: mikedeng1

Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming 3: The Two-Phase RSG Method Finds an (ε, Λ)-Solution within S(Λ)[N(ε) + T(ε, Λ)] Oracle CallsResearch Paper

Motivation

Stochastic optimization methods often see only noisy gradients. For a nonconvex objective, a useful guarantee is that an output point has a small gradient: this is a first-order stationarity certificate, even when there is no claim that the point is globally optimal. A guarantee on the expected squared gradient leaves open how often one particular run succeeds. The two-phase randomized stochastic gradient method of Ghadimi and Lan (2013) addresses that question by generating several candidates and using further oracle calls to select one. The paper gives an explicit bound on the probability of failure and on the number of oracle calls needed for a prescribed accuracy and confidence.

The work sits within stochastic approximation, where the objective may be a population expectation or another function accessible through noisy observations. The 2013 paper develops first- and zeroth-order methods for smooth nonconvex problems. This mission concerns its two-phase first-order result, Theorem 2.4, rather than the Gaussian smoothing results in its later section. The source for every index here is the arXiv v1 preprint; the printed page and PDF page coincide.

Setting

The objective is a differentiable function $f:\mathbb R^n\to\mathbb R$ bounded below, with true optimal value $f^*=\inf_x f(x)$ . Its gradient map $g=\nabla f$ is $L$ -Lipschitz: $\|g(y)-g(x)\|\le L\|y-x\|$ for all $x,y$ . The mission uses $L>0$ . No convexity is assumed.

A stochastic first-order oracle returns a vector $G(x_k,\xi_k)$ when called at the current iterate $x_k$ . Assumption A1 says that the oracle is unbiased at that iterate and has squared error of expectation at most $\sigma^2$ . The noise may depend on earlier calls. In the formal model, the mean is conditional on the past, and the oracle and squared-error random variables are integrable. This makes explicit the probabilistic assumptions used when the paper takes expectations. The model takes $\sigma>0$ because the paper's displayed stepsize and post-optimization sample size otherwise degenerate under Lean's total division convention.

A randomized stochastic gradient run starts at $x_1$ and uses $x_{k+1}=x_k-\gamma_k G(x_k,\xi_k)$ . It chooses an output index $R\in\{1,\ldots,N\}$ with the probability mass function in equation (2.3), independently of that run's oracle noise, and outputs $x_R$ . For a parameter $\widetilde D>0$ , the constant stepsize in equation (2.13) is $\gamma_k=\min\{1/L,\widetilde D/(\sigma\sqrt N)\}$ . The paper writes $D_f=\sqrt{2(f(x_1)-f^*)/L}$ and

\mathcal B_N=\frac{LD_f^2}{N}+\left(\widetilde D+\frac{D_f^2}{\widetilde D}\right)\frac{\sigma}{\sqrt N}.

The two-phase method makes $S$ independent RSG runs, yielding $\bar x_1,\ldots,\bar x_S$ . For each candidate it averages $T$ fresh oracle outputs into an estimated gradient $\widehat g_s$ . It selects a candidate $\bar x^*$ whose estimated-gradient norm is minimal. The post-optimization samples for different candidates may be recycled; the paper explicitly permits this. The candidate itself is known when its post-optimization samples are taken, so the conditional oracle assumption is stated relative to a filtration that contains it at time zero.

Formalization targets

The first target is the one-run mean bound of Corollary 2.2, $L^{-1}\mathbb E\|g(x_R)\|^2\le\mathcal B_N$ , followed by the one-run tail bound (2.19). Lemma 2.3(a) controls the squared norm of a sum of vector martingale differences. Equation (2.28) relates a selected candidate's true gradient to the best candidate and the estimation errors. Equation (2.29) factors the probability of simultaneous failure across independent runs and bounds it, while (2.30) bounds the other source of failure: every optimization run performing poorly, and at least one estimated gradient being inaccurate.

For arbitrary positive $S,N,T$ , Theorem 2.4(a) states the stronger quantitative tail bound

\Pr\left\{\|g(\bar x^*)\|^2\ge2\left(4L\mathcal B_N+\frac{3\lambda\sigma^2}{T}\right)\right\}\le\frac{S+1}{\lambda}+2^{-S}\qquad(\lambda>0).

The goal, Theorem 2.4(b), specializes those parameters to an accuracy $\varepsilon>0$ and failure probability $0<\Lambda<1$ . It sets

S=\left\lceil\log_2\frac2\Lambda\right\rceil,\qquad N=\left\lceil\max\left\{\frac{32L^2D_f^2}{\varepsilon},\left(\frac{32L(\widetilde D+D_f^2/\widetilde D)\sigma}{\varepsilon}\right)^2\right\}\right\rceil,\qquad T=\left\lceil\frac{24(S+1)\sigma^2}{\Lambda\varepsilon}\right\rceil.

An $(\varepsilon,\Lambda)$ -solution is a point satisfying $\Pr\{\|g(\bar x^*)\|^2\le\varepsilon\}\ge1-\Lambda$ . With those parameter values, the method computes such a point using at most $S(N+T)$ stochastic first-order oracle calls. The formulas and constants above are those of equations (2.24)–(2.27) of the preprint.

Significance

The result turns a mean stationarity bound into a confidence guarantee for one returned point, with an explicit accounting of both candidate generation and candidate assessment. It identifies how the number of independent runs, iterations per run, and gradient estimates scale with the requested accuracy and failure probability. Without the post-optimization phase, the paper's direct Markov estimate (2.19) gives a less favorable dependence on the failure probability for a single run.

The mathematical theorem is proved in the 2013 paper; the Lean declarations in this proposal are statements awaiting machine-checked proofs. A completed formalization would give reusable definitions for a dependent-noise gradient oracle, a random-output stochastic-gradient run, and a post-optimization selection procedure. The vector martingale estimate and finite-candidate inequality could also serve later stochastic-optimization developments. Contributions to the probability and measurability infrastructure, as well as the final rate proof, are within scope.

Difficulty

Selecting the candidate with the smallest estimated gradient need not select the one with the smallest true gradient. The estimates are random and are evaluated at candidates that are themselves random outputs of earlier oracle runs. A bound for a fixed point does not address this dependence. The argument needs a conditional oracle contract at each candidate and a separate guarantee that the optimization runs supply a sufficiently good candidate. The paper's intermediate display (2.31) applies a fixed-candidate tail estimate to the selected candidate even though the selection examines the same estimates; that step is not justified by the stated assumptions. The final bound can be phrased without treating (2.31) as a separate target.

Formalization scope

The space $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Iterations and oracle samples retain the paper's one-based indexing; candidate runs use Fin S, which reindexes the paper's $1,\ldots,S$ . The objective's true infimum is carried by IsGLB (Set.range f) fstar, so $D_f$ cannot be weakened by substituting an arbitrary lower bound. Each candidate is generated by the RSG recursion and the mass function (2.3); the one-run performance bound is a theorem, not a hypothesis of the two-phase model. Independent candidate outputs are required for (2.29). The selected candidate may be any minimizer of the estimated-gradient norm, with any tie rule; no measurability of the selection is assumed.

All expectations are Bochner integrals, with integrability included in the oracle assumptions and in the one-run conclusion. Probabilities are ℝ≥0∞ values. The noise carrier is generalized from the paper's Borel subsets of Euclidean space to a measurable type. The general vector martingale lemma omits the paper's Polish-space and trivial-time-zero conditions; neither is needed for its squared-norm bound, and the latter would conflict with a candidate known at time zero. Its non-strict tail statement is restricted to a positive sum of variance bounds, because the printed version is false when every bound is zero. The goal reads the logarithm in (2.24) as base two, matching the paper's final $2^{-S}\le\Lambda/2$ comparison. Positive $\sigma$ and $\widetilde D$ avoid zero steps and an empty post-optimization average.

The formal goal states the probability guarantee. The $S(N+T)$ oracle-call bound follows directly from the algorithm's two loops and is recorded in the theorem's prose rather than in a separate operational semantics for calls. A complete proof may use Mathlib's conditional expectations, independent random variables, finite sums, and real logarithm and ceiling libraries. No assumption may simply postulate the one-run gradient bound or the final success probability.

Selected references

Saeed Ghadimi and Guanghui Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. arXiv:1309.5549v1.

11 thms2 active usersReviewed

Machine Learning Operations Research Optimal Transport·Captain: mikedeng1

Wasserstein Distributionally Robust Optimization and Variation Regularization II: The ∞-Wasserstein Regularizer Equals ρ Times the Mean Local Slope up to ρ²‖H‖ Plus a Boundary TermResearch Paper

Motivation

In distributionally robust optimization, a decision is judged against probability laws near a nominal law rather than against the nominal law alone. The nominal law is often the empirical distribution of observed data. For a loss function, this produces a worst-case expected loss that depends on the size and geometry of the permitted changes to the data. The infinity-Wasserstein model restricts how far any observation can be moved, apart from null events in a coupling. It is a mathematical form of the bounded perturbations used in adversarial learning. Gao, Chen and Kleywegt study when this robust loss behaves like a regularizer based on variation or local slope.

For a finite data set, the nominal law has finite support. This makes the infinity-Wasserstein case especially concrete: each atom of the empirical law has a radius-limited set of possible destinations. Yet the objective still ranges over all probability measures, and the loss need not be bounded on a metric ball. The paper's finite-support duality result and its local-slope estimate together identify the regularization term that this distributional model produces.

Setting

Let $(Z,d)$ be a metric space and let $P,Q$ be probability laws on its Borel sets. A coupling $\pi$ of $P$ and $Q$ is a joint law on $Z\times Z$ with those two marginals. The infinity-Wasserstein distance is

W_\infty(P,Q)=\inf_{\pi\in\Gamma(P,Q)} \operatorname*{ess\,sup}_{(\tilde z,z)\sim\pi}d(\tilde z,z).

Given a real loss $f$ and a radius $\rho\ge0$ , the robust value is the supremum of $\mathbb E_P[f]$ over all $P$ satisfying $W_\infty(P,Q)\le\rho$ . The regularizer $R_{Q,\infty}(\rho;f)$ is this robust value minus $\mathbb E_Q[f]$ . For observations $z_1,\ldots,z_n$ , the empirical law is $P_n=n^{-1}\sum_{i=1}^n\delta_{z_i}$ .

The one-sided local slope $|\partial f|(z)$ records the greatest limiting rate at which $f$ can increase under a perturbation that tends to $z$ . The local growth $G_f(\delta,z)$ is the largest increase $f(\tilde z)-f(z)$ among destinations with $d(\tilde z,z)\le\delta$ . A set $D_f$ marks the interfaces between pieces of a piecewise loss. Its boundary contribution at $z$ is $(\delta-d(z,D_f))_+$ , where the distance to an empty set is infinite. These objects appear in Definition 2 and Assumption 5(I).

Formalization targets

Finite-support transport duality

For a nominal law $Q=\sum_j q_j\delta_{z_j}$ , the first targets assert that an optimal coupling exists when $W_\infty(P,Q)$ is finite and that

\sup_{P:W_\infty(P,Q)\le\rho}\mathbb E_P[f] =\sum_j q_j\sup_{d(\tilde z,z_j)\le\rho}f(\tilde z).

This is Lemma EC.2 in the appendix. The values are allowed to be infinite when a local loss supremum is infinite; the printed assertion of unconditional finiteness is not included.

Consistency

For an upper semicontinuous loss, the Proposition 1 case $p=\infty$ asserts

\lim_{\rho\downarrow0}R_{P_n,\infty}(\rho;f)=0=R_{P_n,\infty}(0;f).

It is a companion statement: it says that the regularizer vanishes, while the main target says at which rate.

Local-slope regularization

The main target is Theorem 1(I), in its general-metric form from Appendix B under Assumption 5(I). If $\delta_0>0$ , $M\ge0$ , and the local growth obeys

|G_f(\delta,z)-\delta|\partial f|(z)| \le H(z)\delta^2+M(\delta-d(z,D_f))_+ \quad(0\le\delta<\delta_0),

then, for a sufficiently small radius, every nonempty empirical sample and every loss in the class satisfy

\left|R_{P_n,\infty}(\rho;f) -\rho\frac1n\sum_{i=1}^n|\partial f|(z_i)\right| \le\rho^2\frac1n\sum_{i=1}^n|H(z_i)| +M\frac1n\sum_{i=1}^n(\rho-d(z_i,D_f))_+.

The finite-support duality and the identity between the empirical regularizer and the average of $G_f(\rho,z_i)$ are the mission's intermediate targets. The printed $\rho_n^2$ in Lemma EC.9 is read as $\rho^2$ , as in Theorem 1(I).

Significance

The estimate gives a precise first-order description of infinity-Wasserstein robustness: the mean local slope is its leading regularization term. The quadratic term measures local curvature or growth, while the boundary term records the effect of sample points close to interfaces between loss pieces. Setting $M=0$ gives the smooth-loss regime, where that interface correction vanishes. The result makes it possible to compare bounded data perturbations with explicit variation penalties using the same loss class and sample.

The paper proves the result. The formalization work here is to express its objects and quantified conditions in Lean, establish finite-support duality for the extended-real robust value, and then formalize the known local estimate. No machine-checked proof of these mission targets is claimed here. The transport and duality definitions can support other finite-support distributionally robust models; the local-slope definitions can be reused for other metric-space perturbation bounds.

Difficulty

The robust value is a supremum over probability laws, whereas the target bound is a finite average of pointwise quantities. Relating the two requires control of the infinity-Wasserstein constraint at every nominal atom, including cases where an infimum over couplings must be attained. A direct substitution of a pointwise supremum into an expectation does not establish the reverse inequality, and extended-real values need care when a loss is unbounded. At the local level, a slope is only a limit near a point; the inequality needed here holds uniformly for all losses, all points, and all sufficiently small radii, with a correction near $D_f$ .

Formalization scope

The Lean metric space uses its Borel measurable structure and is second countable, so the distance on the product is measurable. It has no isolated points, matching §3.4. Losses in the class are measurable. Sample indices are Fin n with $n>0$ , and $P_n$ is the published empirical probability law. Infinity-Wasserstein distance takes values in $[0,+\infty]$ ; robust values and local growth use extended reals. The theorem explicitly requires finite local slopes and finite growth values in the range where Assumption 5(I)'s real inequality is used. The regularizer is built from the supremum over all probability laws in the Wasserstein ball, and its finite-sample result states finiteness before converting its value to a real number. This rules out replacing the regularizer by the easier average of local growth.

The paper defines $D_f$ from intersections of closures of pieces and assumes it is null under a true law. The deterministic estimate uses only distances to $D_f$ , so this mission treats $D_f$ as supplied data and does not require nullity. Likewise, $H\in L^1(P_{\rm true})$ is needed for the paper's statistical setting but the target evaluates $H$ only at finite sample points, so no true law appears in this statement. The radius bound is placed before the sample because Assumption 5(I) supplies one common $\delta_0$ . These generalizations and the positive-radius reading of Assumption 5(I) are explicit in the item statements. Contributions toward the optimal-coupling lemma, extended-real finite-support duality, and the local estimate all advance the target.

Selected references

R. Gao and A. J. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research, 2023; arXiv:1604.02199. Source of the duality theory for finite $p$ that Lemma EC.1 quotes.
R. Gao, X. Chen and A. J. Kleywegt, Wasserstein Distributionally Robust Optimization and Variation Regularization, Operations Research, 2024; arXiv:1712.06050, source preprint dated 2020-10-30, especially Theorem 1(I), Assumption 5(I), Lemmas EC.2 and EC.9.

10 thms2 active usersReviewed

Completed

Operations Research Probability Statistics·Captain: mikedeng1

Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization 1: Empirical Burg-Ball DRO Bounds Cover E[h(x;ξ)] with Probability Tending to 1 − αResearch Paper

Motivation

Stochastic programs and chance-constrained models in operations research contain expectations of the form

Z_0(x)=\mathbb E_0[h(x;\xi)],

where $\xi$ is a random input under an unknown distribution $P_0$ , $x$ is a decision and $h$ is a known loss. In practice $P_0$ is seen only through i.i.d. data $\xi_1,\dots,\xi_n$ . Distributionally robust optimization (DRO) replaces the unknown expectation by the worst case over a set of plausible distributions, and a recurring question is how large that set should be so that the robust value is a statistically valid bound, without being needlessly conservative.

The usual answer, for divergence-based sets on a finite support of size $k$ , sets the radius from a $\chi^2_{k-1}$ quantile (Ben-Tal et al. 2013). This guarantee holds simultaneously for every function of the distribution, and so it is loose for a single expectation, and it degrades as $k$ grows. H. Lam (arXiv:1605.09349, Operations Research 2019) observed that if the ball is placed around the empirical distribution and measured with the Burg entropy, the right radius uses one degree of freedom, whatever the support. The DRO bounds then form an asymptotically exact confidence interval for $Z_0(x)$ . The mechanism is the empirical likelihood method of Owen (Owen 1988; Owen 2001).

Timeline:

1988: Owen proves the empirical likelihood theorem for a mean (−2 log of the profile likelihood ratio tends to $\chi^2_1$ ), the nonparametric analogue of Wilks' theorem.
2013: Ben-Tal, den Hertog, De Waegenaere, Melenberg and Rennen calibrate $\varphi$ -divergence balls on a finite support with $\chi^2_{k-1}$ quantiles.
2016: Lam (this paper) connects the empirical Burg-ball DRO to empirical likelihood, with pointwise (Theorem 2) and uniform (Theorem 4) coverage.
2016–2021: Duchi, Glynn and Namkoong (arXiv:1610.03425) develop the general $f$ -divergence version and exact coverage of optimal values.

Setting

Data: $\xi_1,\xi_2,\dots$ are i.i.d. random elements of a measurable space $\Xi$ under $P_0$ . A decision $x\in\mathbb R^m$ is fixed, and $h(x;\cdot):\Xi\to\mathbb R$ is measurable with $0<\operatorname{Var}_0 h(x;\xi)<\infty$ .

The empirical Burg-entropy divergence ball of radius $\eta$ is the set of weight vectors on the $n$ data points

\mathcal U_n(\eta)=\Big\{w\in\mathbb R^n:\ -\frac1n\sum_{i=1}^n\log(nw_i)\le\eta,\ \sum_{i=1}^n w_i=1,\ w_i\ge0\Big\},

with $\log 0=-\infty$ . It is the $\varphi$ -divergence ball around the uniform weights $1/n$ for the Burg generator $\varphi(t)=-\log t+t-1$ . Let $\chi^2_{1,1-\alpha}$ be the $(1-\alpha)$ -quantile of the $\chi^2_1$ law, i.e. $P(Y^2\le\chi^2_{1,1-\alpha})=1-\alpha$ for $Y\sim N(0,1)$ . The empirical DRO bounds are

\underline Z_n(x)=\min_{w\in\mathcal U_n(\chi^2_{1,1-\alpha}/(2n))}\sum_{i=1}^n h(x;\xi_i)w_i,\qquad \overline Z_n(x)=\max_{w\in\mathcal U_n(\chi^2_{1,1-\alpha}/(2n))}\sum_{i=1}^n h(x;\xi_i)w_i .

For a sample $z\in\mathbb R^n$ and a value $\mu$ , the profile empirical likelihood statistic is

-2\log R(\mu)=\min\Big\{-2\sum_{i=1}^n\log(nw_i):\ \sum_i w_iz_i=\mu,\ \sum_i w_i=1,\ w_i\ge0\Big\},

equal to $+\infty$ when no weight vector is feasible.

Formalization targets

Goal: Theorem 2 (p. 11)

\lim_{n\to\infty}P\big(\underline Z_n(x)\le Z_0(x)\le\overline Z_n(x)\big)=1-\alpha .

The event is two-sided and joint. No rate is claimed.

Milestones

Proposition 2 (p. 23). For every data vector and $\kappa\ge0$ ,

\min_{\mathcal U_n(\kappa/(2n))}\textstyle\sum_i w_iz_i\le\mu\le\max_{\mathcal U_n(\kappa/(2n))}\sum_i w_iz_i\iff -2\log R(\mu)\le\kappa .

Theorem 1, the empirical likelihood theorem (p. 10). $-2\log R(Z_0(x))\Rightarrow\chi^2_1$ .
The pointwise steps of the paper's proof of Theorem 1 (the proof of Theorem 5 with a one-point index set): Lemma 3 (p. 38), $\max_{i\le n}|Y_i|=o(n^{1/2})$ a.s. for square-integrable i.i.d. $Y_i$ ; the closed form (49)–(50) (pp. 25–26) of the optimal weights; the multiplier bound (52) (p. 27); the expansion (68) (p. 30), $-2\log R=n s^{-1}\bar h^2+o_p(1)$ .

Significance

Theorem 2 says that a robust optimization formulation with a data-driven Burg ball of radius $\chi^2_{1,1-\alpha}/(2n)$ yields an asymptotically exact $(1-\alpha)$ confidence interval for an expected loss, independently of the support size of $\xi$ . Proposition 2 is the bridge: it identifies the DRO interval with the empirical likelihood confidence region, so any distributional result on $-2\log R$ transfers to the DRO bounds. This is the pointwise basis of the paper's later results on feasibility of chance and expectation constraints.

The result is proved in the paper, and Theorem 1 is classical. To our knowledge none of these statements has a machine-checked proof. Formalizing them requires the empirical likelihood theorem in Lean, which is reusable well beyond DRO (empirical likelihood tests and intervals for means). The Open platform theorem GenEmpLik.Coverage.theorem_3 (Duchi, Glynn and Namkoong) implies the goal when its decision set is the single point $\{x\}$ and its generator is $2\varphi$ with radius $\chi^2_{1,1-\alpha}$ ; it is a different, more general statement and is not proved. Likewise the Open GenEmpLik.Expansion.lemma_7 implies Lemma 3, and the Proved NumStochOpt.ListScheduling.lemma_8_1_i_max_over_sqrt_ae gives Lemma 3 after passing to $|Y_i|$ .

Difficulty

Proposition 2 is a finite-dimensional convexity statement, but it needs attainment of the minimum defining $-2\log R$ , which holds only because the objective blows up at the boundary of the simplex. The central difficulty is Theorem 1. The optimal weights are explicit only through a Lagrange multiplier $\lambda$ that solves a nonlinear equation; to expand $-2\log R$ one must first show $\lambda=O_p(n^{-1/2})$ , which requires controlling the largest observation by Lemma 3 together with the law of large numbers for $s$ , and then bound the cubic Taylor remainder of $\log(1+\lambda\tilde h_i)$ uniformly in $i$ . A direct appeal to the central limit theorem for the sample mean does not suffice, since $-2\log R$ is an implicitly defined optimal value, not a smooth function of the mean.

Formalization scope

The sample is a sequence ξ : ℕ → Ω → Ξ, measurable, mutually independent and identically distributed, indexed from $0$ ; the size- $n$ sample is fun i : Fin n => h x (ξ i ω).
The moment assumption is MemLp (h x ∘ ξ 0) 2 together with 0 < variance. Positive variance cannot be dropped: for a constant loss the coverage is $1$ .
The quantile is pinned by gaussianReal 0 1 {y | y^2 ≤ q} = ofReal (1 - α) with $0<\alpha<1$ ; it is not a free parameter, and it is not the normal quantile.
The upper bound is the published GenEmpLik.Expansion.robustMean burg (q/2) (its ball has radius $\rho/n$ , so $\rho=q/2$ ); the lower bound is its infimum twin robustLower. The ball uses the published probUncertaintySet and phiDiv.
The Burg generator is $+\infty$ at $t\le0$ , and the statistic elStat minimizes over strictly positive weights with the empty infimum equal to $+\infty$ . Lean's junk value $\log 0=0$ therefore never enters: a formalization with $w_i\ge0$ and real logarithms would admit boundary weights with spurious finite divergence and is ruled out. For $n\ge1$ the value sets of the DRO bounds are nonempty and bounded, so the real infimum and supremum are not junk values.
The decision set $\Theta$ is dropped (the statements are pointwise in $x$ ). Theorem 1 is stated as convergence of distribution functions at every $t$ , which is equivalent to $\Rightarrow\chi^2_1$ since the limit is continuous. Proposition 2 is stated for general $\kappa\ge0$ and every data vector, as displayed on p. 11. Milestones (49)–(50), (52), (68) are the one-point ( $\Theta=\{x\}$ ) specialisations of the proof of Theorem 5.
Probabilities of events are outer probabilities; no measurability of events is assumed, as the paper ignores these issues (p. 14).
Not posed: the headline Theorem 4 (uniform calibration over $\Theta$ by the quantile of a $\chi^2$ -process supremum), Theorem 5 and Lemma 2, which need Donsker classes and weak convergence in $\ell^\infty(\Theta)$ , for which Mathlib has no substrate.

Contributions welcome: proofs of Proposition 2 and Lemma 3 (from the Proved reference), the KKT analysis (49)–(52), and a Lean empirical likelihood theorem.

Selected references

H. Lam, Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization, arXiv:1605.09349v1, 2016; Operations Research 67(4), 2019. https://arxiv.org/abs/1605.09349v1
A. B. Owen, Empirical likelihood ratio confidence intervals for a single functional, Biometrika 75(2), 1988. https://doi.org/10.1093/biomet/75.2.237
A. B. Owen, Empirical Likelihood, Chapman & Hall/CRC, 2001. https://doi.org/10.1201/9781420036152
A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust solutions of optimization problems affected by uncertain probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
J. C. Duchi, P. W. Glynn, H. Namkoong, Statistics of robust optimization: a generalized empirical likelihood approach, Mathematics of Operations Research 46(3), 2021. https://arxiv.org/abs/1610.03425

13 thms2 active usersReviewed

Completed

Linear algebra Numerical Analysis Theoretical Computer Science·Captain: mikedeng1

Low Rank Approximation and Regression in Input Sparsity Time 2: Sketched Multiple-Response Regression Is (1 + 4ε)-Optimal in Squared Error If the Sketch Embeds the Subspace and Approximates ProductsResearch Paper

Motivation

Least-squares regression, $\min_X\|AX-B\|_F$ for a tall matrix $A\in\mathbb R^{n\times d}$ with $n\gg d$ , is among the most frequently solved problems in numerical computation. Direct methods (QR or SVD) cost $O(nd^2)$ time, which is prohibitive when $n$ is in the millions. Sketching replaces the problem by a much smaller one: choose a matrix $S\in\mathbb R^{t\times n}$ with $t\ll n$ , form $SA$ and $SB$ , and solve $\min_X\|S(AX-B)\|_F$ instead. The question is when the solution of the small problem is nearly optimal for the original one.

Clarkson and Woodruff, Low Rank Approximation and Regression in Input Sparsity Time (STOC 2013; JACM 2017), showed that a very sparse random sketch (one non-zero per column, the CountSketch matrix) can be applied in time proportional to the number of non-zero entries of $A$ and still yields $(1+\varepsilon)$ -approximate regression and low-rank approximation. §7 of that paper isolates the deterministic part of the argument: two conditions on a fixed sketch $S$ that guarantee a near-optimal solution, whatever distribution produced $S$ .

Timeline. Sarlós (FOCS 2006) introduced sketch-and-solve regression with fast Johnson–Lindenstrauss transforms. Drineas, Mahoney, Muthukrishnan and Sarlós (Numer. Math. 2011) stated the structural conditions for single-response regression (their Lemma 1); Theorem 36 of Clarkson–Woodruff generalizes it to multiple responses. Clarkson and Woodruff then supplied the sparse sketches meeting the conditions in input-sparsity time.

Setting

All matrices are real. For a vector $v$ let $\|v\|_2^2=\sum_iv_i^2$ ; for a matrix $M$ let $\|M\|_F^2=\sum_{i,j}M_{ij}^2$ . Fix $A\in\mathbb R^{n\times d}$ of rank at most $r$ , a right-hand side $B\in\mathbb R^{n\times d'}$ and a sketch $S\in\mathbb R^{t\times n}$ . Let $C(A)=\{Ax\}$ be the column space and $U\in\mathbb R^{n\times k}$ a matrix with orthonormal columns ( $U^\top U=I$ ) spanning $C(A)$ .

$Y^*$ is a least-squares minimizer: it minimizes $\|AY-B\|_F^2$ (problem (8)).
$\tilde Y$ is a sketched minimizer: it minimizes $\|S(AY-B)\|_F^2$ (problem (7)).
$S$ is a subspace embedding for $A$ with parameter $\eta$ if $\bigl|\|SAx\|_2^2-\|Ax\|_2^2\bigr|\le\eta\|Ax\|_2^2$ for every $x$ .
$S$ satisfies the approximate matrix multiplication event (Lemma 32) for a pair $(U,W)$ with error parameter $e$ if $\|U^\top S^\top SW-U^\top W\|_F^2\le e^2\|U\|_F^2\|W\|_F^2$ .

Formalization targets

Goal: Theorem 36 (p. 24)

If $S$ is a subspace embedding for $A$ with $0\le\eta\le1/2$ and satisfies the event of Lemma 32 for $(U,B-AY^*)$ with error parameter $\sqrt{\varepsilon/r}$ , then every sketched minimizer satisfies

\|A\tilde Y-B\|_F^2\le(1+4\varepsilon)\|AY^*-B\|_F^2 .

This is the explicit form the paper's proof establishes; the printed $(1+\epsilon)$ bound on norms follows after rescaling $\varepsilon$ .

Milestones

Fact 34 (Pythagorean theorem): $C^\top D=0\Rightarrow\|C+D\|_F^2=\|C\|_F^2+\|D\|_F^2$ .
Fact 35 (normal equations): $C^-D$ is a minimizer; every minimizer $X^*$ satisfies $C^\top(CX^*-D)=0$ and $\|CX-D\|_F^2=\|C(X-X^*)\|_F^2+\|CX^*-D\|_F^2$ .
Lemma 37: for $A$ with orthonormal columns, $\|A(\tilde Y-Y^*)\|_F\le2\sqrt\varepsilon\|B-AY^*\|_F$ .
Theorem 39 (affine embeddings, an independent companion result of §7.5): under an embedding with parameter $\varepsilon\le1/2$ and the event of Lemma 32 with parameter $\varepsilon/\sqrt r$ , $\|S(AX-B)\|_F^2-\|S\tilde B\|_F^2$ equals $\|AX-B\|_F^2-\|\tilde B\|_F^2$ up to $\pm2\varepsilon\|AX-B\|_F^2$ for all $X$ , and $\|S(AX-B)\|_F^2=(1\pm3\varepsilon)\|AX-B\|_F^2$ if $S$ also preserves $\|\tilde B\|_F^2$ to $1\pm\varepsilon$ .

Significance

Theorem 36 separates the algorithm design for sketched regression from its correctness proof: any random construction (CountSketch, subsampled randomized Hadamard transforms, leverage-score sampling, Gaussian matrices) yields a $(1+O(\varepsilon))$ -approximate regression solver once it is shown to satisfy the two conditions with constant probability. Clarkson and Woodruff use it for their input-sparsity-time regression algorithm (Theorem 38) and, through Theorem 39 and affine embeddings, for low-rank approximation. The same conditions recur throughout the randomized numerical linear algebra literature (see Woodruff's survey Sketching as a Tool for Numerical Linear Algebra, 2014).

The results are proved in the paper (§7.3, §7.5 and Appendix A, p. 37). To our knowledge none has a machine-checked proof. Formalizing them produces a reusable, distribution-free layer of sketching theory: the probabilistic statements about specific sketches can then be proved separately and composed with it.

Difficulty

The obvious argument applies the subspace embedding to the residual $A\tilde Y-B$ , but that vector does not lie in $C(A)$ , so an embedding of $C(A)$ alone says nothing about it; embedding $C(A)$ augmented with the columns of $B$ instead costs a sketch dimension that grows with $d'$ . The hypotheses of Theorem 36 control the optimal residual $B-AY^*$ only through the approximate-product condition, which is far weaker than norm preservation, and the difficulty is to transfer that control to the sketched solution (Lemma 37) with the constants $2\sqrt\varepsilon$ and $1+4\varepsilon$ . A second obstacle is the passage from a general $A$ of rank at most $r$ to an orthonormal basis $U$ of $C(A)$ : it changes $\|A\|_F$ , which is why the approximate-product condition is stated for $U$ .

Formalization scope

Matrices are Matrix (Fin m) (Fin n) ℝ; squared norms are explicit sums sqNorm and frobSq; the column space is the range of Matrix.mulVecLin; rank is Matrix.rank. Everything is deterministic: $S$ is an arbitrary fixed matrix and no probability space appears. The committed conventions are:

The subspace embedding is in squared form. In Theorem 36 and Lemma 37 its parameter $\eta$ plays the paper's $\epsilon_0^2$ (so $\epsilon_0\le1/\sqrt2$ becomes $\eta\le1/2$ ), which is how the proof of Lemma 37 (p. 37) uses it; in Theorem 39 the parameter is $\varepsilon$ itself, as that proof uses it.
" $S$ satisfies Lemma 32" is the event inside the probability, for the pair $(U,B-AY^*)$ (resp. $(U,\tilde B)$ ) that the proofs use, with $\le$ in place of the printed $<$ (a weaker hypothesis).
$\tilde Y$ , $Y^*$ , $X^*$ are arbitrary minimizers; "the solution" need not be unique. The Moore–Penrose inverse is specified by the four Penrose equations.
$r\ge1$ guards $\varepsilon/r$ and $\varepsilon/\sqrt r$ ; " $n>d$ " (§7) concerns running times and is not assumed.

A trivializing formalization is ruled out: $\tilde Y$ is never defined as $Y^*$ , the approximate-product hypothesis is an inequality and not the exact identity $U^\top S^\top S(B-AY^*)=0$ , $\eta$ is non-negative, and the goal is stated for general $A$ of rank at most $r$ , not only for orthonormal $A$ . The hypotheses are jointly satisfiable (for instance $S=I$ ).

A complete development needs the Frobenius inner product and its Pythagorean identity, the normal equations for matrix least squares, the existence of the Moore–Penrose inverse, and the spectral-norm bound for a symmetric matrix from its quadratic form; all are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Theorem 36, are welcome.

Selected references

K. L. Clarkson and D. P. Woodruff, Low Rank Approximation and Regression in Input Sparsity Time, arXiv:1207.6365v4, 2013; J. ACM 64(6), 2017. https://arxiv.org/abs/1207.6365
P. Drineas, M. W. Mahoney, S. Muthukrishnan and T. Sarlós, Faster Least Squares Approximation, Numerische Mathematik 117(2), 2011. https://arxiv.org/abs/0710.1435
T. Sarlós, Improved Approximation Algorithms for Large Matrices via Random Projections, FOCS 2006. https://doi.org/10.1109/FOCS.2006.37
D. P. Woodruff, Sketching as a Tool for Numerical Linear Algebra, Foundations and Trends in Theoretical Computer Science 10(1–2), 2014. https://arxiv.org/abs/1411.4357

7 thms2 active usersReviewed

Completed

Numerical Analysis Operations Research·Captain: mikedeng1

An Augmented Lagrangian Based Algorithm for Distributed Nonconvex Optimization 1: With ρ = 0, the ALADIN Dual Update Equals the Levenberg–Marquardt Dual Newton Step of Dual DecompositionResearch Paper

Motivation

Large optimization problems often split into blocks owned by different agents (subsystems of a power grid, vehicles in a formation, scenarios of a stochastic program) that are coupled only through a few linear constraints. Distributed optimization methods solve such problems by letting each agent work on its own block and exchanging a small amount of information, typically a vector of prices for the coupling constraints. The classical method of this kind is dual decomposition (Everett 1963; Bertsekas and Tsitsiklis, Parallel and Distributed Computation, 1989): fix the prices, let every agent solve its own subproblem, then update the prices by a gradient or Newton step on the concave dual function. Dual decomposition is reliable for strictly convex problems but has no convergence guarantee for nonconvex ones.

Houska, Frasch and Diehl (SIAM J. Optim. 26 (2016)) proposed ALADIN (augmented Lagrangian based alternating direction inexact Newton), which adds a proximal term to the agents' subproblems and replaces the price update by a coupled equality-constrained quadratic program. ALADIN is used in distributed model predictive control and in power-system optimization. Remark 4.2 and Appendix A of the paper explain where it sits relative to the classical method: if the proximal term is switched off ( $\rho = 0$ ), the price update of ALADIN is exactly a regularized Newton step of dual decomposition. Lemma 5 is the precise statement of that equivalence, and it is the goal of this mission.

Setting

The problem (1.1) has $N$ blocks $x_i\in\mathbb R^n$ :

\min_x\ \sum_{i=1}^N f_i(x_i)\quad\text{s.t.}\quad \sum_{i=1}^N A_i x_i = b,\qquad h_i(x_i)\le 0,

with $f_i:\mathbb R^n\to\mathbb R$ , $h_i:\mathbb R^n\to\mathbb R^{n_h}$ twice continuously differentiable, $A_i\in\mathbb R^{m\times n}$ and $b\in\mathbb R^m$ . One iteration of Algorithm 2 (ALADIN) starts from a primal point $x$ and prices $\lambda\in\mathbb R^m$ and does the following.

Each agent solves the decoupled problem $\min_{y_i} f_i(y_i) + \lambda^\top A_i y_i + \frac\rho2\|y_i-x_i\|^2_{\Sigma_i}$ subject to $h_i(y_i)\le 0$ , returning a minimizer $y_i$ and a multiplier $\kappa_i\ge 0$ . With $\rho = 0$ this is the dual-decomposition subproblem (A.2).
Each agent forms the active-constraint Jacobian $C^*_i$ (rows $\nabla(h_i)_j(y_i)^\top$ for active $j$ , zero rows otherwise), chooses an approximation $C_i$ and a symmetric Hessian approximation $H_i$ , and computes the modified gradient $g_i = \nabla f_i(y_i) + (C^*_i - C_i)^\top\kappa_i$ .
For a parameter $\mu>0$ , a coordinator solves the coupled QP (3.3)

\min_{\Delta y, s}\ \sum_i\Big\{\tfrac12\Delta y_i^\top H_i\Delta y_i + g_i^\top\Delta y_i\Big\} + \lambda^\top s + \tfrac\mu2\|s\|_2^2\ \ \text{s.t.}\ \ \sum_i A_i(y_i+\Delta y_i) = b + s\ \mid\ \lambda_{\mathrm{QP}},\quad C_i\Delta y_i = 0,

and the new prices are $\lambda^+ = \lambda + \alpha_3(\lambda_{\mathrm{QP}}-\lambda)$ .

On the dual-decomposition side, $\nabla V(\lambda) = \sum_i A_i y_i - b$ (A.3) is the gradient of the dual function at $\lambda$ , and the (inexact) dual Newton step (A.4) with a symmetric negative semidefinite scaling matrix $M$ and step size $\alpha\in(0,1]$ is

\lambda^+_{\mathrm{DD}} = \lambda - \alpha\Big(M - \frac1\mu I\Big)^{-1}\nabla V(\lambda),

where $1/\mu$ plays the role of a Levenberg–Marquardt regularization parameter.

Formalization targets

Goal: Lemma 5 (p. 1123)

Assume every $f_i$ strictly convex, every $h_i$ convex, $C_i$ of full row rank, $H_i$ positive definite, $\rho = 0$ and $\alpha_3 = \alpha$ . Then for every $\mu>0$ , with

M = -\sum_{i=1}^N A_i\Big[H_i^{-1} - H_i^{-1}C_i^\top\big[C_iH_i^{-1}C_i^\top\big]^{-1}C_iH_i^{-1}\Big]A_i^\top,

the matrix $M - \frac1\mu I$ is invertible and

\lambda^+ = \lambda^+_{\mathrm{DD}} .

Milestones (the steps of the proof, pp. 1123–1124)

Slack elimination: $\min_s \frac\mu2\|s\|_2^2 - (\lambda_{\mathrm{QP}}-\lambda)^\top s = -\frac1{2\mu}\|\lambda_{\mathrm{QP}}-\lambda\|_2^2$ , attained only at $s = (\lambda_{\mathrm{QP}}-\lambda)/\mu$ .
Stationarity: with $\rho = 0$ , $0 = \nabla f_i(y_i) + A_i^\top\lambda + (C^*_i)^\top\kappa_i = g_i + A_i^\top\lambda + C_i^\top\kappa_i$ .
Explicit minimization over $\Delta y$ : for $H\succ 0$ and $C$ of full row rank, $-Pw$ with $P = H^{-1} - H^{-1}C^\top(CH^{-1}C^\top)^{-1}CH^{-1}$ minimizes $\frac12\Delta^\top H\Delta + w^\top\Delta$ on $\{C\Delta = 0\}$ , with value $-\frac12 w^\top Pw\le 0$ .
Argmax display: for $M$ symmetric negative semidefinite, $\lambda - (M - \frac1\mu I)^{-1}g$ is the unique maximizer of $\frac12(\nu-\lambda)^\top M(\nu-\lambda) + \nu^\top g - \frac1{2\mu}\|\nu-\lambda\|_2^2$ .

Significance

The result. Lemma 5 places ALADIN on a known map. With $\rho=0$ it inherits the convergence theory of dual decomposition for strictly convex problems for small step sizes, independently of how crude the approximations $H_i$ , $C_i$ are, as long as $H_i\succ 0$ . It also reinterprets the augmented-Lagrangian parameter $\mu$ as the inverse of a dual Levenberg–Marquardt parameter, and it isolates the proximal term $\frac\rho2\|y_i - x_i\|^2_{\Sigma_i}$ as the only ingredient that distinguishes ALADIN from dual decomposition and makes the nonconvex analysis of the paper possible.

Formalizing it. The lemma is proved in the paper; to our knowledge no machine-checked proof exists. A formal proof certifies an identity whose printed form contains a typo (see below), and produces reusable linear-algebra facts: the closed-form solution of an equality-constrained strictly convex quadratic program via the reduced inverse $P$ , the semidefiniteness of $P$ , and the closed-form maximizer of a regularized concave quadratic.

Difficulty

The proof is a chain of exact eliminations, and the work is in carrying each one out without losing a sign or a hypothesis. The step most easily done wrong is the minimization over $\Delta y$ : the constraint $C_i\Delta y_i = 0$ couples the block coordinates, the minimizer is expressed through the inverse of $C_iH_i^{-1}C_i^\top$ (invertible only because $C_i$ has full row rank). A second trap is the sign convention for $\lambda_{\mathrm{QP}}$ : it must agree with footnote 4 ( $\lambda + \mu s - \lambda_{\mathrm{QP}} = 0$ ), or the conclusion flips. The tempting shortcut of treating the max–min dual of (3.3) abstractly runs into the fact that strong duality and attainment are not free; working from the KKT system of (3.3) avoids that.

Formalization scope

Vectors are Fin n → ℝ; blocks are indexed by Fin N; matrices are Mathlib Matrix over Fin index types; the gradient is the vector of partial derivatives computed with fderiv. The step-1 output $(y_i,\kappa_i)$ is a local minimizer of the decoupled problem together with KKT multipliers (the paper assumes LICQ for the lower-level constraints). The QP (3.3) and $\lambda_{\mathrm{QP}}$ enter through the KKT system of (3.3), not through a closed-form expression: defining $\lambda_{\mathrm{QP}}$ or $\Delta y$ by the formula of the conclusion would make the goal true by definition and is ruled out. $\nabla V(\lambda)$ is the formula (A.3); that it is the gradient of the dual function is a cited fact the lemma does not use. The invertibility of $M - \frac1\mu I$ is part of the conclusion, because Mathlib's matrix inverse returns $0$ on a singular matrix.

Correction of (A.6). As printed, (A.6) has the bracket $[C_iH_iC_i^\top]^\dagger$ . This is a typo for $[C_iH_i^{-1}C_i^\top]^\dagger$ , as in (A.5) on the same page and as the explicit minimization over $\Delta y$ forces; with the printed bracket the identity fails already for $N = 1$ , $H_1 = \mathrm{diag}(1,2)$ , $C_1 = (1,1)$ , $A_1 = I$ . The mission uses the corrected matrix and writes the pseudo-inverse as an inverse, which it is under the hypotheses.

The hypotheses of strict convexity of $f_i$ , convexity of $h_i$ and $\alpha\in(0,1]$ are kept as on the page although the identity does not use them. The related platform draft GoldfarbIdnani.DualQP.properties_2_6_to_2_9 (not proved) states properties of the same reduced inverse; it is not imported. Proofs of the four milestones and of the goal are welcome; the milestones are self-contained matrix and calculus facts and can be attacked independently.

Selected references

B. Houska, J. Frasch, M. Diehl, An augmented Lagrangian based algorithm for distributed nonconvex optimization, SIAM J. Optim. 26(2) (2016), 1101–1127. https://doi.org/10.1137/140975991
D. P. Bertsekas, J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice-Hall, 1989.
H. Everett, Generalized Lagrange multiplier method for solving problems of optimum allocation of resources, Oper. Res. 11(3) (1963), 399–417. https://doi.org/10.1287/opre.11.3.399
D. P. Bertsekas, Nonlinear Programming, 2nd ed., Athena Scientific, 1999.

7 thms2 active usersReviewed

Completed

Numerical Analysis Operations Research·Captain: mikedeng1

Variable Metric Method for Minimization: Davidon's Rank-One Variable-Metric Update Recovers the Inverse Hessian of a Quadratic in N Steps and Then Steps to the Exact MinimumResearch Paper

Motivation

Quasi-Newton methods minimize a smooth function $f:\mathbb R^n\to\mathbb R$ using gradients only, while building up an approximation to the inverse of the Hessian matrix from the changes of gradient they observe. They are the default algorithms of unconstrained nonlinear optimization: BFGS and its limited-memory variant L-BFGS sit inside most numerical optimization libraries and most large-scale fitting codes in statistics and machine learning.

The family starts with William C. Davidon's Argonne report ANL-5990 of 1959, Variable Metric Method for Minimization, rejected by a journal in 1957 and published only in 1991 as the first article of the SIAM Journal on Optimization, with a preface by the author (DOI 10.1137/0801001). The report's body describes a flowchart algorithm; its Appendix describes "a simplified method embodying some of the ideas" of that algorithm, in one and a half pages. That simplified method is what is now called the symmetric rank-one (SR1) update, and the Appendix contains its quadratic-termination property: on a quadratic, after at most $n$ steps the trial matrix equals the inverse Hessian, and the next step lands at the minimum.

Timeline.

1952: Hestenes and Stiefel's conjugate gradient method minimizes a strictly convex quadratic in at most $n$ steps (J. Res. NBS 49); Davidon cites it as [2].
1959: Davidon's ANL-5990, including the Appendix method treated here.
1963: Fletcher and Powell simplify the body's method into the DFP update and prove its quadratic termination with exact line searches (Comput. J. 6).
1967: Broyden's survey of quasi-Newton methods discusses the symmetric rank-one update (Math. Comp. 21); textbooks later analyse it under the name SR1.
1980: Nocedal's limited-storage BFGS, whose termination on quadratics with exact line searches is a separate Prove2Me mission (Math. Comp. 35).

Setting

Vectors are elements of $\mathbb R^n$ and matrices are real $n\times n$ . Fix a symmetric positive definite matrix $G$ and a point $\xi$ , and let

f(x)=\tfrac12\,(x-\xi)^{\mathsf T}G\,(x-\xi)+c ,

a quadratic with constant Hessian $G$ and minimum point $\xi$ . Its gradient is $\nabla(x)=G(x-\xi)$ , display (6) of the Appendix.

The method keeps a point $x_k$ and a symmetric trial matrix $H_k$ , which plays the role of $G^{-1}$ . Write $\nabla_k=\nabla(x_k)$ . One iteration is

x_{k+1}=x_k-H_k\nabla_k \quad\text{(2)},\qquad H_{k+1}=H_k+a_k\,(H_k\nabla_{k+1})(H_k\nabla_{k+1})^{\mathsf T}\quad\text{(3)},

a full step with no line search followed by a symmetric rank-one update. With the two scalars

N_k=\nabla_{k+1}^{\mathsf T}H_k\nabla_{k+1},\qquad M_k=\nabla_{k+1}^{\mathsf T}H_k\nabla_k ,

footnote 2 of the Appendix fixes the coefficient on a quadratic to $a_k=(M_k-N_k)^{-1}$ , which makes the paper's quality measure $\Delta$ of (4) vanish. Write $S_k=x_{k+1}-x_k$ for the step and $D_k=\nabla_{k+1}-\nabla_k$ for the change of gradient. The paper writes $x$ , $H$ , $\nabla$ for the current quantities and $x^{+}$ , $H^{+}$ , $\nabla^{+}$ for the updated ones, and uses the letter $N$ both for the number of variables and for the scalar $N_k$ ; here the number of variables is $n$ .

Formalization targets

Goal: termination in $n$ steps

If $H_0$ is symmetric and $M_k\ne N_k$ for every $k<n$ , then

H_n=G^{-1}\qquad\text{and}\qquad x_{n+1}=\xi .

This is the sentence after (8) on p. 17: "After no more than $N$ steps (for which $\Delta=0$ ), $H$ will equal $G^{-1}$ and the following step will be to the exact minimum."

Milestones

Display (6): the gradient of $f$ is $G(x-\xi)$ .
Display (8): with $a=(M-N)^{-1}$ and $M\ne N$ , $H^{+}GS=H^{+}D=S$ .
Display (7): if $HGu=u$ then $H^{+}Gu=u$ , for any coefficient $a$ .
The sentence "so that $S$ becomes another such eigenvector", read along the run: if $M_i\ne N_i$ for $i<k$ , then $H_kGS_j=S_j$ for every $j<k$ .

Further statements of the Appendix

Condition 1 (p. 16): if $H$ is positive definite and $R^{-1}\le\det H^{+}/\det H\le R$ with $R>1$ , then $H^{+}$ is positive definite.
The constraint remark (p. 17): for any function and any coefficients, if $H_0$ is symmetric and $H_0b=0$ , then every step is perpendicular to $b$ and $b\cdot x_k$ is conserved.
Table (5) (p. 16): for general (non-quadratic) $f$ , the coefficient $a$ that minimizes $\Delta$ subject to condition 1, and the minimum value, on each of five ranges of $M$ .

Significance

The termination theorem says that on a quadratic the rank-one update recovers the exact inverse Hessian from $n$ gradient differences, without line searches and without positive definiteness of the trial matrix, and then takes the Newton step. This is the property that justifies the name "variable metric": the metric $H_k$ converges to the one that makes the problem trivial. The secant equation (8) and the persistence of earlier secant equations (7) are the template for the analysis of every later quasi-Newton update, and the SR1 update remains in use in trust-region methods because it does not force positive definiteness.

The result is classical and its proof is short; what this mission adds is a machine-checked version stated in the paper's own form. In particular the hypothesis is the paper's: only that each of the first $n$ coefficients is defined. Textbook statements of SR1 termination often assume in addition that the steps are linearly independent; the paper does not, and the formal goal does not either. No Lean formalization of SR1, DFP or BFGS termination was found in Mathlib or on Prove2Me. On Prove2Me, the related open targets are L-BFGS termination (Nocedal 1980) and conjugate-gradient termination (Hestenes–Stiefel 1952); the definitions here are independent of theirs.

Difficulty

Each update changes $H$ by a rank-one term, and nothing in a single step forces $H_n$ to be $G^{-1}$ : the coefficient $a_k$ depends on the current iterate and the update could, a priori, destroy what earlier steps achieved, as general rank-one updates do. The obvious count — $n$ steps, $n$ conditions — does not by itself give $n$ independent conditions on $H_n$ ; the steps produced by the method are not chosen to be independent, and the only hypothesis available is that the denominators $M_k-N_k$ are nonzero. The difficulty is to get the full conclusion from that hypothesis alone, without assuming independence, positive definiteness of $H_0$ , or a line search.

Formalization scope

Vectors are Fin n → ℝ with 0-based indices, matrices Matrix (Fin n) (Fin n) ℝ; $u^{\mathsf T}Hv$ is u ⬝ᵥ (H *ᵥ v) and $(Hg)(Hg)^{\mathsf T}$ is vecMulVec (H *ᵥ g) (H *ᵥ g). The definition file DavidonVM.Termination.Method provides quad, grad, Nval, Mval, the run predicate IsRunWith for an arbitrary gradient field and coefficients, and IsQuadRun for the quadratic with $a_k=(M_k-N_k)^{-1}$ ; DavidonVM.Termination.Delta provides the update and the quantity $\Delta$ of (4).

Committed conventions, each a reading of something the paper leaves implicit:

The function is an explicit quadratic with constant symmetric positive definite $G$ ("in the neighborhood of a minimum"); the run's gradient field is $G(x-\xi)$ , and milestone 1 ties it to the quadratic. The goal uses positive definiteness; milestones use only symmetry where that suffices; the secant milestone needs nothing on $G$ .
Only $H_0$ is assumed symmetric (the paper, p. 4: "It is to be symmetric"); positive definiteness of $H_0$ is not assumed.
"Steps for which $\Delta=0$ " is read through footnote 2 as $M_k\ne N_k$ . Lean's real inverse gives $0^{-1}=0$ , so without this hypothesis the update would silently leave $H$ unchanged.
The stopping rule "provided that $N$ is greater than some preassigned $\varepsilon$ " is not modelled; the run continues for every $k$ , and the goal looks at steps $0,\dots,n$ only.
$G^{-1}$ is Mathlib's matrix inverse, the true inverse since $G$ is positive definite.

A statement of the goal with the extra hypothesis " $S_0,\dots,S_{n-1}$ are linearly independent", or with $H_k G S_j=S_j$ assumed, would be a weaker theorem than the paper's and is ruled out. The case $n=0$ is trivial; the hypotheses are jointly satisfiable for $n=1$ (checked locally).

Welcome contributions: proofs of the four milestones and the goal; general facts about rank-one updates (determinant and positive definiteness, Sherman–Morrison form of the inverse) that the further statements need and that are reusable for DFP, BFGS and trust-region analyses.

Selected references

W. C. Davidon, Variable Metric Method for Minimization, SIAM J. Optim. 1(1) (1991) 1–17 (Argonne report ANL-5990, 1959). https://doi.org/10.1137/0801001
M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, J. Res. Nat. Bur. Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
R. Fletcher and M. J. D. Powell, A rapidly convergent descent method for minimization, Comput. J. 6 (1963) 163–168. https://doi.org/10.1093/comjnl/6.2.163
C. G. Broyden, Quasi-Newton methods and their application to function minimisation, Math. Comp. 21 (1967) 368–381. https://doi.org/10.1090/S0025-5718-1967-0224273-2
J. Nocedal, Updating quasi-Newton matrices with limited storage, Math. Comp. 35 (1980) 773–782. https://doi.org/10.1090/S0025-5718-1980-0572855-7

7 thms2 active usersReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Scheduling Problems with Two Competing Agents 7: PARTITION Reduces to Two Agents Each Bounding Their Own Makespan in the Two-Machine Flow Shop and Open ShopResearch Paper

Motivation

In multi-agent scheduling, several decision makers share one processing resource, and each one cares only about the completion of its own jobs. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) set up the two-agent version of this problem and classified its complexity for most combinations of classical objectives. Typical settings are a manufacturing cell that serves an internal and an external customer, or two departments that negotiate access to a shared machine. Most of the paper treats a single machine. Its §10 asks what happens when the shared resource is a small shop: two machines that every job must visit.

The answer is that even the simplest two-machine case is hard. In the classical single-agent setting, the two-machine flow shop makespan problem is solved by Johnson's rule (Johnson 1954) and the two-machine open shop makespan problem by Gonzalez and Sahni (1976), both in polynomial time. As soon as two agents each want their own jobs finished early, both problems become NP-hard.

Setting

There are two agents, A and B. Agent A owns jobs $J^A_1,\dots,J^A_{n_A}$ and agent B owns jobs $J^B_1,\dots,J^B_{n_B}$ . Every job consists of one operation on machine $M_1$ and one on machine $M_2$ , and $p^X_{ih}\ge 0$ is the processing time of job $J^X_i$ on machine $M_h$ . A schedule gives every operation a start time. It is feasible when no operation starts before time $0$ , each machine processes at most one operation at a time, and the two operations of one job do not overlap in time. Processing is nonpreemptive.

In the flow shop $F2$ every job is processed first on $M_1$ and then on $M_2$ .
In the open shop $O2$ the two operations of a job may be processed in either order.

The makespan of agent $X$ , $C^X_{\max}$ , is the latest completion time of an operation of one of its jobs. The recognition problem $F2\|C^A_{\max}\le Q_A,\ C^B_{\max}\le Q_B$ asks, for given thresholds $Q_A, Q_B$ , whether some feasible flow shop schedule has $C^A_{\max}\le Q_A$ and $C^B_{\max}\le Q_B$ . The problem $O2\|C^A_{\max}\le Q_A,\ C^B_{\max}\le Q_B$ is the same question for the open shop.

PARTITION (Problem 9.1 of the paper) asks whether a finite list of nonnegative integers $p_1,\dots,p_k$ can be split into two parts of equal sum $P/2$ , where $P=\sum_i p_i$ .

Formalization targets

Goal: Theorems 10.1 and 10.2

\text{PARTITION}\ \le_p\ F2\,\|\,C^A_{\max}\le Q_A,\ C^B_{\max}\le Q_B \qquad\text{and}\qquad \text{PARTITION}\ \le_p\ O2\,\|\,C^A_{\max}\le Q_A,\ C^B_{\max}\le Q_B,

with $\le_p$ polynomial-time many-one reducibility between binary-coded languages. This is how the paper proves " $F2\|C^A_{\max}:C^B_{\max}$ is NP-hard" (Theorem 10.1, p. 238) and " $O2\|C^A_{\max}:C^B_{\max}$ is NP-hard" (Theorem 10.2, p. 239).

Milestones: the two constructions

For Theorem 10.1, with $\varepsilon=1/(k+1)$ , the paper builds the instance with $k$ A-jobs of times $(\varepsilon, p_i)$ , one B-job of times $(P/2-(k-1)\varepsilon,\ P/2)$ , and thresholds $Q_A = 3P/2+\varepsilon$ , $Q_B = P+\varepsilon$ . The milestones are:

under $C^B_{\max}\le Q_B$ the B-job starts on $M_2$ by $P/2+\varepsilon$ , and the A-jobs before it on $M_2$ total at most $P/2$ ;
for even $P$ , PARTITION has a solution if and only if this instance meets both thresholds.

For Theorem 10.2 the instance has $k$ A-jobs of time $p_i$ on both machines, one B-job of time $P/2$ on both machines, and thresholds $Q_A=3P/2$ , $Q_B=P$ . The milestones are:

under $C^B_{\max}\le Q_B$ the B-job starts at $0$ on one machine and at $P/2$ on the other;
PARTITION has a solution if and only if this instance meets both thresholds.

Significance

The two theorems mark the boundary of tractability of §10. The single-agent problems $F2\|C_{\max}$ and $O2\|C_{\max}$ are polynomial. Giving the second agent a single job and a deadline is already enough to make the problems NP-hard, so no extension of Johnson's rule or of the Gonzalez–Sahni algorithm solves the two-agent versions unless P = NP. The paper also observes that any other combination of the objectives it considers is NP-hard in these shops.

The theorems are proved in the paper by short reductions. As far as we know none of them is machine-checked. This mission produces checked statements of both reductions on a general two-machine shop model with real start times. It also corrects the flow shop equivalence, which as printed does not hold for odd $P$ .

Difficulty

The hard direction of each equivalence goes from a feasible schedule to a partition. A schedule is a set of real start times, not a permutation. Nothing forces the jobs into a fixed order or rules out idle time. The proof has to extract a combinatorial split from interval packing: which A-jobs fit into the gap before the B-job on one machine and which fit into the gap after it. The sum of lengths of pairwise disjoint intervals inside a window must be bounded by the window's length.

In the flow shop the gap after the B-job has length $P/2+k\varepsilon$ , which is not $P/2$ . Integrality of the A-lengths is what closes the gap, and it only works when $P/2$ is an integer. In the open shop, the same argument has to cover both orders of the B-job's operations. Both reductions output rational data, so the goal also needs a scaling to integer data and a polynomial-time bound on the code map.

Formalization scope

Model. Jobs are numbered Fin (n_A + n_B), the A-jobs first. Start times are real numbers, and idle time and different job orders on the two machines are allowed. Flow shop feasibility is the published JohnsonFlowShop.TwoStage.IsFeasible from the Johnson (1954) series. Open shop feasibility is the definition IsOpenFeasible of this mission: no machine overlap between distinct jobs, and no time overlap between the two operations of a job. " $C^X_{\max}\le Q_X$ " is stated as "every operation of every $X$ -job ends by $Q_X$ ", so no maximum over a possibly empty set is taken.
Languages. The target languages hold the binary codes of instances with natural-number processing times and thresholds that have a feasible schedule meeting both thresholds. PARTITION is the published ProjSchedTW.Complexity.partitionLang (nonnegative sizes, zero allowed), and reducibility is CookPvsNP.PolyReducible. Both come from published definitions of the Neumann–Schwindt–Zimmermann and Cook series. NP-membership is not formalized.
Constructions. They are defined over $\mathbb R$ exactly as printed. A reduction to the $\mathbb N$ -coded languages has to rescale (for example by $2(k+1)$ ). That rescaling is the solver's to choose and is not a milestone.
Corrections. The printed flow shop equivalence uses $\lfloor P/2+k\varepsilon\rfloor = P/2$ and fails for odd $P$ : $p=(1)$ gives a yes-instance of the scheduling problem but has no partition. It also fails for $P=0$ and $k\ge 2$ , where the printed $p^B_{11}$ is negative. Milestone 2 therefore assumes $P$ even and ( $P\ge2$ or $k\le1$ ). The goal is unaffected, because odd $P$ is a PARTITION no-instance. In the open shop proof, the printed identity " $\sum p^A_i+\sum p^B_i = 2P$ " is read as "each machine carries $3P/2$ of work", and the statement is unchanged.
No trivialization. The flow shop and open shop languages are not restricted to the instances the constructions produce, so they cannot be decided by reading off the construction. A schedule must satisfy the machine and job non-overlap constraints, including in the open shop, where a definition without the job constraint would let a job run on both machines at once.
Welcome contributions. Interval-packing lemmas on $\mathbb R$ , a polynomial-time bound for list arithmetic over encNats, and a scaling lemma for shop schedules are reusable beyond this mission.

Selected references

A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2) (2004) 229–242. https://doi.org/10.1287/opre.1030.0092
S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1 (1954) 61–68. https://doi.org/10.1002/nav.3800010110
T. Gonzalez, S. Sahni, Open shop scheduling to minimize finish time, Journal of the ACM 23(4) (1976) 665–679. https://doi.org/10.1145/321978.321985
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.

11 thms2 active usersReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Scheduling Problems with Two Competing Agents 6: PARTITION Reduces to Two Agents Each Bounding Their Own Total Completion Time on One MachineResearch Paper

Two agents sharing one machine

In many production and service settings a single resource is shared by parties with different goals: two departments sending orders to the same machine, two customers of a contract manufacturer, or two classes of requests on one processor. Multi-agent scheduling models this directly. Each agent owns its own jobs and its own objective, and a schedule is judged by the pair of objective values it gives the two agents rather than by a single combined criterion.

Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004, pp. 229–242) set up the systematic study of the two-agent single-machine problem. For each pair of classical objectives they ask how hard it is to optimise one agent's objective while the other agent's objective stays within a given bound. This mission formalises their §9, the case in which both agents minimise their own total completion time. With a single agent, minimising the total completion time is solved by sorting the jobs by length (the shortest-processing-time rule of Smith, 1956). §9 shows that two agents, each with this easiest of objectives, already give an NP-hard problem (Theorem 9.2), and that the problem is solved in pseudopolynomial time by a dynamic program (Theorem 9.3).

Setting

There are two agents, A and B. Agent A owns jobs $J^A_1,\dots,J^A_{n_A}$ with processing times $p^A_h\in\mathbb N$ ; agent B owns jobs $J^B_1,\dots,J^B_{n_B}$ with processing times $p^B_k\in\mathbb N$ . All jobs are available at time $0$ and are processed on one machine, one at a time, without interruption. Since both objectives are nondecreasing in the completion times, a schedule $\sigma$ is a sequence of all $n_A+n_B$ jobs processed back to back from time $0$ . The completion time $C_j(\sigma)$ of a job is the total processing time of the job and of all jobs before it. Agent A's cost is $\sum_hC^A_h(\sigma)$ and agent B's cost is $\sum_kC^B_k(\sigma)$ .

The recognition problem $1\|\sum C^A_i\le Q_A,\ \sum C^B_i\le Q_B$ asks, for thresholds $Q_A,Q_B$ , whether some schedule has

\sum_{h=1}^{n_A}C^A_h(\sigma)\le Q_A\qquad\text{and}\qquad\sum_{k=1}^{n_B}C^B_k(\sigma)\le Q_B .

The source problem is PARTITION (Problem 9.1): given integers $p_1,\dots,p_k$ with $P=\sum_ip_i$ , is there a set $S\subseteq\{1,\dots,k\}$ with $\sum_{i\in S}p_i=\sum_{i\notin S}p_i=P/2$ ?

The paper's reduction numbers the integers so that $p_1\le\dots\le p_k$ and gives both agents identical job sets, $k$ jobs of lengths $p_1,\dots,p_k$ , with thresholds $Q_A=Q_B=T/2$ , where

T=3P+4\sum_{i=1}^k(k-i)p_i .

Writing $J[i]$ for the pair $J^A_i,J^B_i$ , an SPT schedule processes $J[1],\dots,J[k]$ in order, each pair in either internal order; $x$ denotes the total length of the pairs in which B goes first.

Formalization targets

Goal: Theorem 9.2

\text{PARTITION}\ \le_p\ 1\|\textstyle\sum C^A_i\le Q_A,\ \sum C^B_i\le Q_B

Here $\le_p$ is polynomial-time many-one reducibility between languages of binary codes: a polynomial-time Turing-machine-computable map on strings that sends codes of PARTITION yes-instances, and only those, to codes of yes-instances of the recognition problem. Together with the NP-completeness of PARTITION (Karp 1972) this is the statement " $1\|\sum C^A_i : \sum C^B_i$ is binary NP-hard".

Milestones of the proof

Every SPT schedule has $\sum C^A_i+\sum C^B_i=T$ , and $Q_A=Q_B=T/2$ .
Eqs. (5) and (6): in an SPT schedule, $\sum C^A_i=P+2\sum_i(k-i)p_i+x$ and $\sum C^B_i=P+2\sum_i(k-i)p_i+(P-x)$ .
A schedule with $\sum C^A_i\le T/2$ and $\sum C^B_i\le T/2$ processes the jobs in nondecreasing order of length.
For pairwise distinct $p_1<\dots<p_k$ : PARTITION has a solution iff some schedule meets $T/2$ for both agents.

Further result: Theorem 9.3 with recursion (7)

With each agent's jobs numbered by nondecreasing length and $P(i,j)$ the total length of $J^A_1,\dots,J^A_i,J^B_1,\dots,J^B_j$ , the recursion

F(i,j,q)=\min\bigl\{F(i-1,j,q)+P(i-1,j)+p^A_i;\ F(i,j-1,q-P(i,j))\bigr\}

with $F(0,0,q)=0$ for $q\ge0$ and $F=+\infty$ for $q<0$ yields $F(n_A,n_B,Q)=\min\{\sum C^A_i:\sum C^B_i\le Q\}$ , and $+\infty$ when no schedule meets the bound.

Significance

Theorem 9.2 fills one cell of the paper's complexity table: even when both agents use the objective that is trivial for one agent, sharing the machine makes the constrained problem NP-hard. Together with Theorem 9.3 it places $1\|\sum C^A_i:\sum C^B_i$ exactly: NP-hard under binary encoding, solvable in pseudopolynomial time, hence not strongly NP-hard unless P = NP. The later literature on two-agent and multi-agent scheduling (for example the monograph of Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal, Multiagent Scheduling, Springer 2014) cites this classification.

Neither result has a machine-checked proof that we know of. The mission adds a formal record of the reduction and of the dynamic program, reusable definitions for the two-agent total-completion-time problem, and a correction of the printed proof: the equivalence between PARTITION and the constructed instance, as printed, holds only when the integers are pairwise distinct. For $p=(1,1,1,1,10)$ PARTITION has no solution, yet a schedule meets $T/2=41$ for both agents. Theorem 9.2 itself is not affected, since PARTITION remains NP-hard, but a complete formal proof needs a reduction that is correct on every input.

Difficulty

The equivalence for distinct integers rests on two facts: the overall total $\sum C^A_i+\sum C^B_i$ is at least $T$ for every schedule, with equality only for sequences in nondecreasing order of length; and, with distinct lengths, such a sequence is made of consecutive pairs, whose split is controlled by $x$ . The naive formal argument stops at the second fact, which is false with repeated lengths: a block of equal-length jobs can be shared between the agents in ways no sequence of pairs realises. The goal adds the encoding layer: the reduction must be computable in polynomial time on a Turing machine, must handle repeated and zero sizes and odd $P$ (where $T/2$ is not an integer and the language's thresholds are), and must send strings that do not code a PARTITION instance outside the target language. For Theorem 9.3, the dynamic program is correct only because some optimal schedule orders each agent's jobs by length, and the constraint makes this exchange argument less direct than for a single agent.

Formalization scope

Jobs are Fin nA ⊕ Fin nB (Sum.inl h is $J^A_{h+1}$ , Sum.inr k is $J^B_{k+1}$ , 0-based). Schedules, completion times and the idle-free sequence model are the published MooreLateJobs.Shared.completionTime (Moore 1968 series): a schedule is a duplicate-free list containing every job once, and completion times are real numbers. Processing times and thresholds of the language are natural numbers. Reducibility is the published CookPvsNP.PolyReducible, and PARTITION, the alphabet and the binary codes are the published ProjSchedTW.Complexity.Encoding (partitionLang, whose sizes are natural numbers including $0$ ). The target language allows any job counts and any processing times; identical job sets are a property of the construction only.

The following readings are explicit:

An SPT schedule of the construction is given by a choice $x:\mathrm{Fin}\,k\to\mathrm{Bool}$ of the first agent in each pair; "feasible implies SPT" is stated as "lengths are nondecreasing along the sequence", which is what the paper's exchange argument proves.
The milestones take the integers already sorted, as a hypothesis; the paper's thresholds $T/2$ are real numbers in the milestones.
The equivalence milestone assumes $p_1<\dots<p_k$ ; the printed version with $\le$ is false, as shown above.
In recursion (7), the terms $F(-1,j,q)$ and $F(i,-1,q)$ that the paper leaves undefined are $+\infty$ .
The running time $O(n_An_BQ)$ of Theorem 9.3 is not formalised; only the correctness of (7) is. Membership in NP is not formalised.

The goal cannot be met by a trivial reduction: PolyReducible requires the map to be computed by a polynomial-time Turing machine and to be correct on every string, and the target language contains every two-agent instance, not only those with identical job sets. Contributions welcome: the exchange lemmas for total completion time on the shared sequence model, the SPT formulas, and Turing-machine constructions for list sorting and arithmetic on binary codes, which other reductions of this series reuse.

Selected references

A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2) (2004) 229–242. https://doi.org/10.1287/opre.1030.0092
R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, Plenum (1972) 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106
J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1) (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102
S. Cook, The P versus NP Problem, Clay Mathematics Institute Millennium Problems (2000). https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf
A. Agnetis, J.-C. Billaut, S. Gawiejnowicz, D. Pacciarelli, A. Soukhal, Multiagent Scheduling: Models and Algorithms, Springer (2014). https://doi.org/10.1007/978-3-642-41880-8

12 thms2 active usersReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Scheduling Problems with Two Competing Agents 2: KNAPSACK Reduces to Minimizing One Agent's Total Weighted Completion Time Under a Makespan Bound for the OtherResearch Paper

Two agents sharing one machine

In many production and logistics settings a single resource is shared by parties with different goals: two departments of a plant that send orders to the same machine, two customers of a contract manufacturer, or two classes of traffic on one processor. Multi-agent scheduling models this directly. Each agent owns its own jobs and its own objective, and a schedule is judged by the pair of objective values it gives the two agents rather than by one combined criterion.

Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004, pp. 229–242) set up the systematic study of the two-agent single-machine problem. For each pair of classical objectives they ask how hard it is to optimise one agent's objective while the other agent's objective stays within a given bound. Their Table 1 lists the outcome for each pair. This mission formalises one entry, Theorem 5.2: when agent A minimises its total weighted completion time and agent B only requires its makespan to stay below a bound, the problem is NP-hard under binary encoding of the numbers. The corresponding single-agent bicriteria problem had been shown NP-hard in the strong sense by Lenstra, Rinnooy Kan and Brucker (1977); the two-agent version differs because only B's jobs are constrained.

Setting

There are two agents, A and B. Agent A owns jobs $J^A_1,\dots,J^A_{n_A}$ ; job $J^A_h$ has a processing time $p^A_h\in\mathbb N$ and a weight $w^A_h\in\mathbb N$ . Agent B owns jobs $J^B_1,\dots,J^B_{n_B}$ with processing times $p^B_k\in\mathbb N$ . All jobs are available at time $0$ and are processed on one machine, one at a time, without interruption.

Because both objectives are nondecreasing in the completion times, there is no reason to leave the machine idle, so a schedule $\sigma$ is a sequence of all $n_A+n_B$ jobs processed back to back from time $0$ . The completion time $C_j(\sigma)$ of a job $j$ is the total processing time of $j$ and of all jobs sequenced before it. Agent A's cost is $\sum_{h}w^A_hC^A_h(\sigma)$ ; agent B's cost is its makespan $C^B_{\max}(\sigma)=\max_kC^B_k(\sigma)$ .

The paper's recognition problem $1\|\sum w_iC^A_i\le Q_A,\ C^B_{\max}\le Q_B$ asks, for given thresholds $Q_A,Q_B$ , whether some schedule has

\sum_{h=1}^{n_A}w^A_hC^A_h(\sigma)\le Q_A\qquad\text{and}\qquad C^B_k(\sigma)\le Q_B\ \text{ for all }k .

The source problem is KNAPSACK (Problem 5.1): given nonnegative integers $u_1,\dots,u_n$ , $w_1,\dots,w_n$ and integers $b,W$ , is there $S\subseteq\{1,\dots,n\}$ with $\sum_{i\in S}u_i\le b$ and $\sum_{i\in S}w_i\ge W$ ?

Formalization targets

Goal: Theorem 5.2

\text{KNAPSACK}\ \le_p\ 1\|\textstyle\sum w_iC^A_i\le Q_A,\ C^B_{\max}\le Q_B

Here $\le_p$ is polynomial-time many-one reducibility between languages of binary codes: a Turing-machine-computable, polynomial-time map on strings sending codes of KNAPSACK yes-instances, and only those, to codes of yes-instances of the recognition problem. Together with the NP-completeness of KNAPSACK (Garey and Johnson 1979) this is the statement " $1\|\sum w_iC^A_i : C^B_{\max}$ is binary NP-hard".

Milestones

The paper's reduction builds, from a KNAPSACK instance, the two-agent instance with $p^A_i=u_i$ , $w^A_i=w_i$ , a single B-job of length $p^B_1=\hat w\hat u$ (where $\hat u=\sum_iu_i$ , $\hat w=\sum_iw_i$ ), and thresholds $Q_B=b+p^B_1$ , $Q_A=\hat w\hat u+(\hat w-W)p^B_1$ . The milestones are the two directions of the proof and their combination:

Eq. (1): if $S$ solves KNAPSACK, every sequence with exactly the A-jobs of $S$ before the B-job meets both thresholds.
Eq. (2): if $\sum_iw_iu_i>0$ and a sequence meets both thresholds, the A-jobs before the B-job solve KNAPSACK.
Equivalence: under $\sum_iw_iu_i>0$ , KNAPSACK is a yes-instance iff the constructed instance is.
§8: with every B-job given due date $Q$ and $Q'=0$ , a sequence meets $\sum U^B_i\le Q'$ (and A's bound) iff it meets $C^B_{\max}\le Q$ , which carries the hardness over to $1\|\sum w_iC^A_i:\sum U^B_i$ .

Significance

Theorem 5.2 fixes the complexity of one cell of the two-agent classification. It shows that the polynomial algorithm for the unweighted case $1\|\sum C^A_i:f^B_{\max}$ (Theorem 5.5 of the same paper) cannot be extended to arbitrary weights unless P = NP. Through §8 it also settles $1\|\sum w_iC^A_i:\sum U^B_i$ . The hardness is binary, not strong: the reduction produces numbers of size about $\hat w\hat u$ , so pseudo-polynomial algorithms are not ruled out, which is consistent with the dynamic programs studied in later two-agent literature.

The result is proved in the paper; no machine-checked proof is known to exist. Formalizing it produces a complete reduction from a two-constraint knapsack problem to a scheduling recognition problem, with the encoding, the degenerate instances and the polynomial running time all made explicit. The model and the KNAPSACK language are reusable by other two-agent reductions (Theorems 9.2, 10.1 and 10.2 of the paper reduce from PARTITION in the same frame).

Difficulty

The two directions of the equivalence are short computations with completion times. The printed argument, however, is not correct as written in two places. The bounds "smaller than $\hat w\hat u$ " and "smaller than $(\hat w-W)p^B_1$ " in the derivation of (1) hold only with equality allowed. The strict inequalities in (2) fail when $\sum_iw_iu_i=0$ , and then the reduction itself fails: with all $u_i=0$ and $W>\hat w$ the KNAPSACK instance is a no-instance while the constructed instance has $Q_A=Q_B=0$ and every schedule meets both thresholds. A complete reduction must recognise such instances and treat them separately.

The construction also produces integer thresholds that can be negative ( $b<-p^B_1$ , or $W>\hat w+1$ ), while instances of the target are coded with natural numbers. Finally, the reduction must be a polynomial-time Turing machine computation over binary codes, including the decoding of arbitrary strings and the binary multiplication $\hat w\hat u$ ; that is where most of the formal work lies.

Formalization scope

Model. Jobs are Fin nA ⊕ Fin nB (0-based: Sum.inl h is $J^A_{h+1}$ , Sum.inr k is $J^B_{k+1}$ ). Schedules and completion times are the published MooreLateJobs.Shared sequence model (IsSchedule, completionTime) of the Moore (1968) series: a duplicate-free list of all jobs, processed without idle time from time $0$ . Integer processing times are cast to $\mathbb R$ .
Makespan bound. $C^B_{\max}\le Q_B$ is written as $C^B_k\le Q_B$ for every B-job; no nonemptiness of B's job set is assumed.
Languages. Polynomial-time reducibility is the published CookPvsNP.PolyReducible (Cook's Definition 3, one-tape Turing machines). Codes use the published binary encoding ProjSchedTW.Complexity.Encoding (alphabet BSym, encNat, encInt) of the Neumann–Schwindt–Zimmermann series. A KNAPSACK instance is coded as the integers $n,u_1,\dots,u_n,w_1,\dots,w_n,b,W$ ; a target instance as the natural numbers $n_A,n_B$ , the processing times and weights, and $Q_A,Q_B$ . The target language allows any $n_A,n_B\ge0$ ; the reduction uses $n_B=1$ .
Readings of the paper. "Binary NP-hard" is formalised as the reduction from KNAPSACK, without the NP-completeness of KNAPSACK and without membership in NP. The milestone Eq. (2) and the equivalence carry the added hypothesis $\sum_iw_iu_i>0$ ; the inequalities "smaller than" in (1) are read as $\le$ . Eq. (1) is stated for every order of the jobs inside $S$ and inside its complement. The §8 result is stated as the encoding-free equivalence of feasible solutions, not as a reduction between languages.
Ruled out. The goal cannot be met by a reduction that ignores the input: the equivalence must hold for every string, and the target language is exactly the codes of yes-instances of the two-agent recognition problem with B's objective the makespan. KNAPSACK here is the two-constraint problem of Problem 5.1, not subset sum.

Contributions welcome: proofs of the two directions, of the equivalence, the treatment of the degenerate instances, and the Turing machine for the reduction, which would also serve the other binary-coded reductions on the platform.

Selected references

A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2) (2004) 229–242. https://doi.org/10.1287/opre.1030.0092
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
S. Cook, The P versus NP Problem, Clay Mathematics Institute Millennium Problem description. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf
J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1) (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102

11 thms2 active usersReviewed

Completed

Linear Optimization Operations Research·Captain: mikedeng1

Obtaining Lower Bounds from the Progressive Hedging Algorithm for Stochastic Mixed-Integer Programs: The Dual Prices Give a Lower Bound on the Optimal Value in Every IterationResearch Paper

Why lower bounds matter for progressive hedging

Progressive hedging separates a stochastic optimization problem by scenario, solves those smaller problems, and coordinates their first-stage decisions through weighted aggregation and price updates. It is useful when the full extensive formulation is too large to solve directly. For stochastic mixed-integer programs, its iterates can provide feasible decisions, but a feasible cost alone does not reveal how far that cost is from the global optimum. A lower bound gives the missing comparison: the difference between a feasible cost and a valid lower bound is an optimality gap. Branch-and-bound methods also use lower bounds to discard regions whose best possible cost cannot improve the current solution. These are the reasons the authors seek a bound available during a progressive-hedging run, rather than only after convergence. Gade et al., author manuscript, §§1–3.

The paper establishes lower bounds for two-stage stochastic mixed-integer programs, extends them to scenario bundles, and studies their behavior computationally. The mission concerns the mathematical statement that the price vector produced at each completed iteration is eligible for a decomposed lower bound. The paper was published in Mathematical Programming in 2016; the theorem and page labels here follow the authors' SAND2013-9195J manuscript. Gade et al., author manuscript.

Finite-scenario two-stage setting

Let $\Xi$ be a finite set of scenarios and let $p_\xi>0$ be their probabilities, with $\sum_{\xi\in\Xi}p_\xi=1$ . A first-stage decision $x\in\mathbb R^{n_1}$ is made before the scenario is known. Its first $p_1$ coordinates are nonnegative integers; the others are unrestricted reals. It incurs cost $c^\top x$ and must satisfy $Ax\ge b$ . After scenario $\xi$ is observed, a second-stage decision $y(\xi)\in\mathbb R^{n_2}$ incurs cost $g(\xi)^\top y(\xi)$ . Its first $p_2$ coordinates are nonnegative integers, and it must satisfy $Wy(\xi)\ge r(\xi)-T(\xi)x$ . The recourse matrix $W$ is common to all scenarios. The scenario feasible set $X(\xi)$ contains pairs $(x,y)$ satisfying these restrictions for one $\xi$ . Gade et al., §2, pp. 3–5.

In the extensive scenario formulation, each scenario has a copy $x(\xi)$ of the first-stage vector, and a common vector $\hat x$ enforces implementability through $p_\xi x(\xi)-p_\xi\hat x=0$ . Its optimum is $z^*$ . Algorithm 1 starts with zero prices $w^0(\xi)=0$ , solves unpenalized scenario problems, and at iteration $\nu$ computes $\hat x^\nu=\sum_\xi p_\xi x^\nu(\xi)$ and $w^\nu(\xi)=w^{\nu-1}(\xi)+\rho(x^\nu(\xi)-\hat x^\nu)$ . Later scenario solves add both $w^\nu(\xi)^\top x$ and $(\rho/2)\|x-\hat x^\nu\|_2^2$ to their objectives. Here $\rho$ is the algorithm's scalar parameter. Gade et al., Algorithm 1, p. 6.

Formalization targets

Scenario price bound

For any scenario prices $w(\xi)$ , define the decomposed dual value by

D_\xi(w(\xi))=\inf_{(x,y)\in X(\xi)}\left(c^\top x+g(\xi)^\top y+w(\xi)^\top x\right),\qquad D(w)=\sum_{\xi\in\Xi}p_\xi D_\xi(w(\xi)).

Proposition 1 states that prices with $\sum_\xi p_\xi w(\xi)=0$ satisfy $D(w)\le z^*$ . The price invariant in §3.1 states that the update maintains this weighted zero sum. The mission's goal combines these source claims at every completed iteration $N\ge1$ of Algorithm 1:

\sum_{\xi\in\Xi}p_\xi w^N(\xi)=0,\qquad D(w^N)\le z^*.

The formal goal is the lower-bound inequality; the zero-sum statement and Proposition 1 are its two milestones. Gade et al., Proposition 1, p. 6, and §3.1, p. 7.

Bundle extension

For a partition $B$ of the scenarios, a bundle $\beta$ has probability $P_\beta=\sum_{\xi\in\beta}p_\xi$ . A bundle subproblem uses one first-stage vector for its scenarios and second-stage weights $p_\xi/P_\beta$ . Proposition 3 gives the corresponding inequality $D_B(w)\le z^*$ when $\sum_{\beta\in B}P_\beta w(\beta)=0$ . The proposal also records the bundle price invariant and the resulting inequality at each completed bundled iteration as companion statements. Gade et al., §3.3, pp. 9–10.

What the results provide

The scenario bound turns each price vector into an independent set of optimization problems whose weighted values certify a lower bound on the original mixed-integer optimum. The bound does not require the scenario first-stage decisions to agree at that iteration. The bundle result gives the same kind of certificate when several scenarios are solved together. These are the paper's known results, not new open mathematical conjectures. Gade et al., §§3.1 and 3.3.

Formalizing them requires a reusable interface for finite-support stochastic mixed-integer models, their scenario feasible sets, implementability equations, price systems, and finite prefixes of both algorithms. It also separates the general price-feasibility inequality from the algorithmic invariant. The mission currently proposes statements with open Lean proofs; it does not claim a machine-checked proof of these paper results.

Main mathematical difficulty

An iteration of progressive hedging solves scenario problems with a quadratic proximal term, while the lower-bound calculation uses scenario problems without that term. Their objective values cannot simply be identified. The relevant connection is the price vector: to apply Proposition 1 at an arbitrary iteration, its weighted zero-sum condition must follow from the actual aggregation and price-update rules. The bundle version adds normalization by $P_\beta$ , so every bundle must have positive mass and the bundle weights must cover the full scenario distribution. Gade et al., §§3.1 and 3.3.

Formalization scope

Lean represents vectors as Fin n → ℝ, linear constraints componentwise, and the extensive formulation with the weighted implementability equation printed in (15). The dimensions satisfy $p_1\le n_1$ and $p_2\le n_2$ , as required by the paper's spaces $\mathbb Z_+^{p_i}\times\mathbb R^{n_i-p_i}$ . The finite scenario weights are positive and sum to one. The first integer coordinates are nonnegative; every remaining real coordinate is free. The paper's assumptions that the SMIP has an attained finite optimum and each $X(\xi)$ is nonempty are explicit in the goal and Propositions 1 and 3. The scenario and bundle subproblem values, and $z^*$ , live in the extended reals: an unbounded-below subproblem retains $-\infty$ rather than acquiring an arbitrary real infimum. Gade et al., §§2–3.

An algorithm run is a finite prefix through its last aggregation and price update, with exact minimizers recorded as conditions on its sequences; a stopping test truncates the prefix. The proximal term is the Euclidean sum of squared coordinate differences. No positivity condition on $\rho$ is added to the lower-bound statements, since the page does not require one for these claims. Bundles form a partition, but equal bundle sizes are not required for the inequalities. Algorithm 2's printed w^ν(i) at initialization and Σ_i P_β x^ν(β) at aggregation are read with bundle indices. A bundle recourse vector is represented as a function on all scenarios, with only its coordinates inside the bundle constrained or used.

The exact equations of the scenario model and runs prevent a trivial encoding that assumes dual feasibility or the desired bound as part of a run. Contributions to the model, the price invariants, the extended-real weak-duality arguments, and the bundle extension are all within scope. The paper's convexified limit result (Proposition 2), its cited Theorem 1, and multi-stage Algorithm 3 are outside this mission.

Selected references

D. Gade, G. Hackebeil, S. M. Ryan, J.-P. Watson, R. J-B Wets, and D. L. Woodruff, Obtaining Lower Bounds from the Progressive Hedging Algorithm for Stochastic Mixed-Integer Programs, author manuscript SAND2013-9195J; published in Mathematical Programming, 2016. OSTI manuscript; DOI.

4 thms2 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Logic-Based Benders Decomposition: With Valid Benders Cuts (B1), the Generic Benders Algorithm Stops Only at an Optimal Solution, an Infeasible Problem or an Unbounded OneResearch Paper

Motivation

Benders decomposition solves an optimization problem in two groups of variables by fixing one group, solving the remaining subproblem, and turning what the subproblem's solution proves into a constraint, the Benders cut, on the fixed variables. In the classical method of Benders (1962) the subproblem is a linear program and the cut comes from its LP dual. Many problems that decompose naturally have subproblems that are not linear programs: scheduling, satisfiability, 0-1 and constraint programs. Hooker and Ottosson (Math. Program. 96, 2003) replaced the LP dual by the inference dual, the problem of inferring the strongest bound on the objective from the constraints, and obtained a Benders scheme in which any sound inference method produces cuts. This logic-based Benders decomposition has since become a standard technique for planning and scheduling problems that combine an assignment master problem with combinatorial subproblems.

The correctness of the generic scheme rests on two short theorems of the paper. Theorem 1 says that if every cut is valid, then each of the algorithm's three ways of stopping reports the right answer. Theorem 2 says that the algorithm stops when the fixed variables range over a finite set. This mission formalizes both theorems, together with the facts used in the proof of Theorem 1.

Setting

An optimization problem (1) has a domain $D$ , a feasible set $S$ and a real-valued objective $f$ ; its value is $\inf_{x\in S} f(x)$ . Optimal values lie in $[-\infty,+\infty]$ : an infeasible minimization has value $+\infty$ , an unbounded one $-\infty$ , and the reverse holds for maximization. For propositions $P,Q$ about $x$ , $P$ implies $Q$ with respect to $D$ , written $P\xrightarrow{D}Q$ , if $Q(x)$ holds at every $x\in D$ where $P(x)$ holds. The inference dual (2) of (1) is

\max\ \beta\quad\text{s.t.}\quad x\in S\xrightarrow{D} f(x)\ge\beta .

In Benders decomposition the variables are pairs $(x,y)$ with $x\in D_x$ , $y\in D_y$ , and problem (6) is $\min f(x,y)$ over $(x,y)\in S$ . Fixing $y$ at a trial value $\bar y$ gives the subproblem (7), $\min f(x,\bar y)$ over $(x,\bar y)\in S$ , with inference dual (8): $\max\beta$ s.t. $(x,\bar y)\in S\xrightarrow{D_x} f(x,\bar y)\ge\beta$ . A bounding function $\beta_{\bar y}:D_y\to[-\infty,+\infty]$ defines the cut $z\ge\beta_{\bar y}(y)$ . The cut satisfies

(B1) if every feasible $(x,y)$ of (6) satisfies $f(x,y)\ge\beta_{\bar y}(y)$ , and

(B2) if $\beta_{\bar y}(\bar y)=\beta$ , the value obtained in the subproblem dual.

The cuts generated so far form the master problem (9): $\min z$ s.t. $z\ge\beta_{y^k}(y)$ for every cut $k$ , $y\in D_y$ .

The generic Benders algorithm (Figure 1 of the paper) starts with $\bar z=-\infty$ and some $\bar y\in D_y$ . While the subproblem dual at $\bar y$ has a feasible $\beta>\bar z$ , it formulates $\beta_{\bar y}$ with $\beta_{\bar y}(\bar y)=\beta$ and adds its cut. If the master is then infeasible, it stops and reports (6) infeasible. Otherwise it takes an optimal solution $(\bar z,\bar y)$ of the master and repeats. When the loop exits, the optimal value of (6) is reported as $\bar z$ .

In Lean, LogicBenders.Generic.Setting defines all of these objects: optVal, subVal, IsDualFeasible, ValidCut, masterLHS, IsMasterOptimal and MasterInfeasible, and a Run with the predicates IsRun, StopsAtWhile and StopsAtMaster.

Formalization targets

Goal: Theorem 1 (p. 9)

Assume (B1) for every cut the run has added. Then three statements hold.

If the run stops at the While test with a finite master value $\bar z$ , then (6) has an optimal solution $(\bar x,\bar y)$ with $f(\bar x,\bar y)=\bar z$ .
If it stops with an infeasible master, then $S=\varnothing$ .
If it stops because the subproblem dual has no real feasible $\beta$ , then (6) is unbounded.

\text{(B1)}\ \Longrightarrow\ \bigl[\text{finite stop}\Rightarrow \exists\,\bar x:\ f(\bar x,\bar y)=\bar z=\min_{S} f\bigr]\wedge\bigl[\text{master infeasible}\Rightarrow S=\varnothing\bigr]\wedge\bigl[\text{dual infeasible}\Rightarrow \inf_S f=-\infty\bigr].

Milestones (statements used in the proof)

§3, p. 6: strong inference duality, $\inf_{x\in S}f(x)=\sup\{\beta: x\in S\xrightarrow{D}f(x)\ge\beta\}$ .
The subproblem value at any $\bar y$ bounds the value of (6) from above.
Under (B1), the value $\bar z$ of a master optimum bounds the value of (6) from below.
At a terminating master optimum, $\beta^*=\bar z$ .
Under (B1), an infeasible master implies that (6) is infeasible.
An infeasible subproblem dual makes the subproblem, and hence (6), unbounded.

Companion: Theorem 2 (p. 10)

If (B1) and (B2) hold, $D_y$ is finite, and the subproblem dual is solved to optimality, then no run of the algorithm continues forever.

Further items

Lemma 3 (p. 20) gives a criterion for a 0-1 inequality $ax\ge\alpha$ to imply the branching clause (29). The §4 statement (p. 7) characterizes when a feasible linear system implies $cx\ge\beta$ .

Significance

Theorem 1 is what allows any sound inference method to supply Benders cuts. Correctness needs only (B1), so the method that derives the cuts (resolution, constraint propagation, a branch-and-bound proof, LP duality) never has to be re-verified at the level of the decomposition. The paper's specializations to satisfiability, 0-1 programming and machine scheduling, and much of the later literature on logic-based Benders, rely on this theorem when they check validity of their cuts and nothing more. Theorem 2 is the matching termination guarantee, and the example on p. 10 shows that the finiteness of $D_y$ cannot be dropped.

Both theorems are proved in the paper, and to the extent known no machine-checked version exists. A formalization makes the paper's implicit conventions precise: values in $[-\infty,+\infty]$ , what "the subproblem dual is infeasible" means when $-\infty$ is always a feasible bound, and exactly which cuts the master contains at each iteration. It also exposes two gaps in the printed proofs. Theorem 1's first clause uses the attainment of the subproblem optimum without stating it. Theorem 2's printed proof claims the subproblem value increases at every iteration, which is false, although the theorem itself is true. The definitions form a small reusable layer for later formalizations of specific logic-based Benders schemes.

Difficulty

The mathematics is elementary, and the difficulty lies in stating it faithfully. Several readings of the statements are wrong. A "run" whose $(\bar z,\bar y)$ are not master optima for exactly the cuts generated so far makes Theorem 1 false. Optimal values taken as real infima turn the infeasible case into junk. Defining "dual infeasible" over the extended reals makes clause 3 vacuous. For Theorem 2, the obvious argument is the printed one, that $\beta$ (or $\bar z$ ) increases strictly. It fails: with three values of $y$ and cuts equal to $-100$ away from their own $\bar y$ , the subproblem value can decrease between iterations while $\bar z$ stays fixed. The printed argument therefore cannot be transcribed, and the theorem needs a proof the page does not give.

Formalization scope

Domains and values. Domains are Lean types: X stands for $D_x$ , Y for $D_y$ and D for $D$ . The feasible set is S : Set (X × Y) and the objective is f : X → Y → ℝ. Optimal values are EReal infima and suprema, with $+\infty$ for infeasible and $-\infty$ for unbounded problems.
Dual feasibility and the master problem. Dual feasibility ranges over EReal, so $\beta=-\infty$ is always feasible. "The subproblem dual is infeasible" is therefore stated as "no real $\beta$ is feasible". A master optimum $(z,\bar y)$ means $z=\max_{j\le k}\beta^{(j)}(\bar y)<+\infty$ and $z$ is at most that maximum at every $y$ ; the value $z=-\infty$ means the master is unbounded.
Iterations. Iterations are 0-based: iteration $k$ works at ybar k, has bound zbar k, and adds cut k. The structure IsRun encodes Figure 1 exactly: zbar 0 = ⊥, every iteration finds a dual-feasible beta k > zbar k with cut k (ybar k) = beta k, and the next $(\bar z,\bar y)$ is a master optimum for exactly the cuts 0, …, k. An unconstrained "run", or a dual infeasibility that $-\infty$ satisfies vacuously, would trivialize the goal, and both are ruled out by these definitions.
Added hypotheses. Theorem 1's first clause assumes that the subproblem optimum at the terminal $\bar y$ is attained whenever it is finite. The printed proof uses this fact ("some optimal solution $\bar x$ "), and the clause is false without it. Lemma 3 adds $J_0\cap J_1=\varnothing$ , which branching guarantees. No other hypotheses are added.
Contributions welcome. Proofs of all items, especially a correct proof of Theorem 2.

Selected references

J. N. Hooker and G. Ottosson, Logic-based Benders decomposition, Mathematical Programming 96(1):33–60, 2003. https://doi.org/10.1007/s10107-003-0375-9 (statements cited from the authors' revised manuscript of November 2000).
J. F. Benders, Partitioning procedures for solving mixed-variables programming problems, Numerische Mathematik 4:238–252, 1962. https://doi.org/10.1007/BF01386316

8 thms2 active usersReviewed

Operations Research·Captain: mikedeng1

Retail Assortment Planning in the Presence of Consumer Search III: Under Independent-Assortment Search, the Profit Change from Adding a Variant Is Quasi-Convex in Its PreferenceResearch Paper

Motivation

A retailer deciding which variants of a product to stock trades off two effects. A deeper assortment captures consumers whose favourite variant would otherwise be missing, but it splits demand among more variants, each of which then carries its operational costs (shelf space, handling, inventory) at a smaller, less efficient scale. Van Ryzin and Mahajan (Management Science 1999) showed that under multinomial-logit (MNL) demand the optimal assortment consists of the most popular variants, which reduces the search over $2^n$ assortments to $n$ candidates.

Cachon, Terwiesch and Xu (working paper, 2002; published in MSOM 2005) add consumer search: a consumer who finds nothing good enough in the store may leave to look elsewhere, and a deeper assortment makes that less likely. In their independent-assortment model the search threshold does not depend on the store's assortment, but the fraction of consumers who stay does. This mission formalizes their Theorem 5: even with this extra dependence, the profit change from adding a variant is quasi-convex in that variant's preference.

Setting

There are $n$ variants. Variant $i$ has a preference $v_i>0$ and the no-purchase option has preference $v_0>0$ (in the paper $v_i=\exp((u_i-p_i)/\mu)$ , with $u_i-p_i$ the net utility and $\mu>0$ the Gumbel scale). For an assortment $S\subseteq\{1,\dots,n\}$ the MNL purchase probability without search is

q_i^m(S)=\frac{v_i}{\sum_{k\in S}v_k+v_0},\qquad i\in S .

A consumer searches when her best alternative in the store, including no purchase, falls below a threshold $\bar U$ . With Euler's constant $\gamma$ and $\lambda=\exp[-(\bar U/\mu+\gamma)]>0$ , this happens with probability $H(\bar U,S)=\exp\bigl(-\lambda(v_0+\sum_{k\in S}v_k)\bigr)$ , and by the paper's Theorem 1 the independent-assortment demand is

q_i^{si}(S)=q_i^m(S)\bigl(1-H(\bar U,S)\bigr).

Each variant sold earns a margin $m$ , and stocking a variant with demand $q$ costs $c(q)$ , where the cost function $c$ is concave and increasing on $[0,1]$ (economies of scale). Variant $i$ 's profit is $\pi_i^{si}(S)=m\,q_i^{si}(S)-c(q_i^{si}(S))$ . Write $V_S=v_0+\sum_{i\in S}v_i$ .

Fix $S$ and a variant $j\notin S$ , and treat $j$ 's preference $v_j\ge 0$ as a variable. Let $\pi_i^{si}(v_j)$ be variant $i$ 's profit in $S_j=S\cup\{j\}$ ; its demand carries the factor $1-e^{-\lambda(v_j+V_S)}$ , not $1-e^{-\lambda V_S}$ . The cannibalization loss and the profit change are

L^{si}(v_j)=\sum_{i\in S}\pi_i^{si}(S)-\sum_{i\in S}\pi_i^{si}(v_j),\qquad h^{si}(v_j)=\pi_j^{si}(v_j)-L^{si}(v_j).

Formalization targets

Goal: Theorem 5 (common margin)

h^{si}\ \text{is quasi-convex on }[0,\infty):\qquad h^{si}(t)\le\max\{h^{si}(a),h^{si}(b)\}\quad(0\le a\le t\le b).

Milestones (the steps of the paper's proof)

Display (7): $h^{si\prime}(v_j)=J(v_j)f(v_j)+N(v_j)g(v_j)$ for $v_j>0$ , with the paper's functions $J,f,N,g$ .
$J(v_j)>0$ and $N(v_j)<0$ for $v_j>0$ .
$f$ is nondecreasing and $g$ is nonincreasing on $(0,\infty)$ .
Display (8), corrected: $h^{si\prime}(v_j)=\dfrac{e^{-\lambda(v_j+V_S)}}{(v_j+V_S)^2}\bigl[V_S D(v_j)f(v_j)-K(v_j)g(v_j)\bigr]$ .
$D$ and $K$ are positive and strictly increasing on $[0,\infty)$ , and so is $K/D$ .
Display (12): $2-2e^{-t}-te^{-t}-t<0$ for $t=\lambda(v_j+V_S)>0$ .

Significance

Quasi-convexity of $h^{si}$ says that a variant is worth adding, if at all, at an extreme of its popularity. The paper uses it to conclude that, as without search, the optimal assortment under independent-assortment search lies among the popular assortments, the sets of the $k$ most preferred variants. This reduces assortment optimization to $n$ candidates. The paper also shows that the conclusion fails in its overlapping-assortment model, so the independent-assortment case marks where this structural result survives the addition of search.

The result is proved in the paper; none of it has a machine-checked proof. The paper's proof contains gaps that a formalization must close: several sign and monotonicity facts are asserted without proof ("It can be shown", "by a similar argument as in Theorem 4"), display (8) is printed without a factor $V_S$ , and the step from (10) to (11) rests on an inequality asserted without the full expression. A complete formal proof of Theorem 5 therefore also fixes the argument.

Difficulty

The no-search analogue (Theorem 4) is easy: the numerator of $h^{m\prime}$ is increasing, so $h^{m\prime}$ changes sign at most once. Here the search factor $1-e^{-\lambda(v_j+V_S)}$ depends on $v_j$ , and the derivative splits as $Jf+Ng$ with $J>0$ , $N<0$ , $f$ nondecreasing and $g$ nonincreasing, but neither $J$ nor $N$ is monotone. So the argument used for Theorem 4 no longer applies, and when $f\ge 0$ and $g\ge 0$ the derivative cannot be written as a positive factor times a monotone one. The proof needs a separate second-order argument at critical points in that case. Showing only that $h^{si\prime}$ has at most one zero is also not enough: it must change sign from negative to positive.

Formalization scope

Variants are Fin n (0-based); the no-purchase option is a separate real v0 > 0, not an element of Fin n. All preferences are positive. The MNL probability is the published RetailVariety.Structure.share, referenced, not redefined.
One margin $m\in\mathbb R$ for every variant, including $j$ . The paper's model allows per-variant margins, but its proof of Theorem 5 writes a single $m$ throughout. With unequal margins the statement is false: one variant $i\in S$ with $v_i=0.76202736$ , $v_0=0.021273423$ , $c(q)=0.38165308\,q^{0.59833805}$ , $m_j=5.4080321$ , $m_i=6.1078441$ , $\lambda=2.6494844$ gives an $h^{si}$ that rises to about $0.246$ near $v_j\approx1.0$ , falls to about $0.152$ near $v_j\approx15.9$ , and rises again.
$c:\mathbb R\to\mathbb R$ is concave and monotone on $[0,1]$ (all demands lie in $[0,1)$ ) and, in addition to the paper's assumptions, twice continuously differentiable on $(0,1)$ , because the proof uses $c'$ and $c''$ . The milestones use only differentiability where they need it. $c'$ is Mathlib's deriv c. The value $c(0)$ is unconstrained; $h^{si}(0)=-c(0)$ .
$\lambda>0$ is a free parameter; $\mu$ , $\gamma$ and $\bar U$ enter only through it.
Adding $j$ with preference $x$ is Function.update v j x on insert j S, with $j\notin S$ . Quasi-convexity is Mathlib's QuasiconvexOn ℝ (Set.Ici 0).
The following formalizations would trivialize or change the theorem and are ruled out: demand without the factor $1-H$ (that is Theorem 4); evaluating $H$ at $S$ instead of $S_j$ inside $\pi_i^{si}(v_j)$ ; convexity in place of quasi-convexity; a specific cost function such as $\nu q^\beta$ or a linear cost.
The definitions (search-adjusted MNL demand, profit-change function) are reusable for the paper's other results. Proofs of the asserted lemmas (milestones 2, 3, 5) and of the corrected (8) are welcome independently of the goal.

Selected references

G. P. Cachon, C. Terwiesch, Y. Xu, Retail Assortment Planning in the Presence of Consumer Search, Wharton working paper, December 20, 2002. UPenn repository. Published version: Manufacturing & Service Operations Management 7(4), 2005, 330–346. doi:10.1287/msom.1050.0088
G. van Ryzin, S. Mahajan, On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments, Management Science 45(11), 1999, 1496–1509. doi:10.1287/mnsc.45.11.1496
D. McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, 1974, 105–142.

10 thms2 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Retail Assortment Planning in the Presence of Consumer Search II: Under MNL Without Search, the Profit Change from Adding a Variant Is Quasi-Convex in Its PreferenceResearch Paper

Motivation

A retailer that sells a product in many variants (colours, sizes, flavours) has to decide which variants to stock. This is the assortment planning problem. Each variant added to the shelf brings new demand. It also cannibalizes demand from the variants already stocked, and it lowers their cost efficiency, because operational costs (shelf space, handling, holding) usually show economies of scale. Cachon, Terwiesch and Xu, in Retail Assortment Planning in the Presence of Consumer Search (Wharton working paper, December 2002), study this trade-off under the multinomial logit (MNL) model of consumer choice. They compare a model without consumer search with two models in which consumers may leave to search elsewhere.

There are $2^n - 1$ nonempty assortments of $n$ variants, so full enumeration is impractical. The retailer wants to know whether attention can be restricted to the popular assortments $\{1\}, \{1,2\}, \dots, \{1,\dots,n\}$ , the assortments made of the most preferred variants.

Timeline. Van Ryzin and Mahajan (Management Science 45(11), 1999, doi:10.1287/mnsc.45.11.1496) showed that, without search and with a cost derived from the newsvendor model, the profit change from adding a variant is quasi-convex in that variant's preference. As a consequence, the optimal assortment is a popular one. Cachon, Terwiesch and Xu (working paper 2002; Manufacturing & Service Operations Management 7(4), 2005, doi:10.1287/msom.1050.0088) extended the quasi-convexity to any concave increasing cost (Theorem 4 of the working paper), and then to search with independent assortments (Theorem 5). This mission formalizes Theorem 4.

Setting

Let $N = \{1, \dots, n\}$ be the possible variants. Variant $i$ has a preference $v_i > 0$ ; in the paper $v_i = \exp((u_i - p_i)/\mu)$ , where $u_i - p_i$ is the variant's expected net utility and $\mu > 0$ is the Gumbel scale. The no-purchase option has preference $v_0 > 0$ . With assortment $S \subseteq N$ , the MNL demand of variant $i \in S$ is

q_i^m(S) = \frac{v_i}{\sum_{k \in S} v_k + v_0}. \qquad (2)

Variant $i$ has margin $m_i = p_i - c_i$ (price minus purchase cost). Stocking it incurs an operational cost $c(q_i(S))$ , where the cost function $c$ is concave and increasing on $[0,1]$ (the consumer population is normalised to $1$ , so demands lie in $[0,1]$ ). The profit of variant $i$ is $\pi_i(S) = m_i q_i(S) - c(q_i(S))$ , and the retailer's profit is $\pi(S) = \sum_{i \in S} \pi_i(S)$ .

Fix $S$ and a variant $j \notin S$ , and let $S_j = S \cup \{j\}$ . Treat $j$ 's preference $v_j$ as a variable. Write $q_i(v_j)$ for variant $i$ 's demand with assortment $S_j$ , and $\pi_i(v_j) = m_i q_i(v_j) - c(q_i(v_j))$ for its profit. The loss on the variants already stocked is

L(v_j) = \sum_{i \in S} \pi_i(S) - \sum_{i \in S} \pi_i(v_j),

and the net profit change from adding $j$ is $h^m(v_j) = \pi_j^m(v_j) - L^m(v_j)$ . Adding $j$ is profitable exactly when $h^m(v_j) > 0$ . Write $V_S = v_0 + \sum_{i \in S} v_i$ .

Formalization targets

Goal: Theorem 4 (p. 13)

h^m(v_j) = \pi_j^m(v_j) - L^m(v_j) \ \text{ is quasi-convex in } v_j \text{ on } [0, \infty),

that is, every sublevel set $\{v_j \ge 0 : h^m(v_j) \le r\}$ is an interval. The goal holds for every concave increasing $c$ and every choice of margins, and assumes no differentiability.

Milestones (proof of Theorem 4, p. 14)

(6). For $v_j > 0$ and $c$ differentiable on $(0,1)$ ,

h^{m\prime}(v_j) = \frac{\big[m_j V_S - c'\big(\tfrac{v_j}{v_j+V_S}\big)V_S\big] - \big[\sum_{i\in S} m_i v_i - \sum_{i\in S} c'\big(\tfrac{v_i}{v_j+V_S}\big)v_i\big]}{(v_j+V_S)^2}.

The numerator of (6) is nondecreasing in $v_j$ on $(0,\infty)$ .
Single crossing. $h^{m\prime}$ is either $\le 0$ on all of $(0,\infty)$ , or $\le 0$ before some threshold $a \ge 0$ and $\ge 0$ after it.

Significance

The result. A quasi-convex function on an interval attains its maximum at an endpoint. So if adding a less preferred variant $k$ to $S$ is profitable, adding a more preferred variant $j$ (with $v_j > v_k$ ) is at least as profitable. With monotone margins, this exchange argument shows that an optimal assortment with $x$ variants consists of the $x$ most popular variants. The search for the optimal assortment then reduces from $2^n - 1$ candidates to $n$ . The paper uses this structure again for the search model with independent assortments (Theorem 5) and in its analysis of a heuristic equilibrium (Theorem 8).

Formalizing it. The theorem is proved in the paper, and is not known to have been formalized anywhere. The mission produces a machine-checked proof for an arbitrary concave increasing cost, with per-variant margins. The paper's proof differentiates $c$ and writes a single common margin. A formal proof settles that neither assumption is needed. Van Ryzin and Mahajan's newsvendor-specific Lemma 1 is posed separately on Prove2Me (RetailVariety.Structure.lemma_1). It concerns a different function, a ratio $g/f$ on $[0, v_1]$ , and is not a special case of the statement here.

Difficulty

Adding $j$ changes every demand at once: $j$ 's own demand rises while all of $S$ 's demands fall, each through the shared denominator $v_j + V_S$ . The obvious approach is to show that $h^m$ is convex, and it fails: $h^m$ is in general not convex in $v_j$ , for example, when $c(q) = aq + b$ is linear and every margin equals some $m > a$ , $h^m$ is a positive multiple of the concave demand $v_j/(v_j+V_S)$ plus a constant. The paper's own argument goes through the derivative (6). It needs a derivative of $c$ , and its last step ("at most one $v_j$ with $h^{m\prime}(v_j) = 0$ ") is literally false when the numerator of (6) vanishes on an interval, for instance when $c$ is linear with slope equal to a common margin, so that $h^m$ is constant. A rigorous proof must handle a non-differentiable concave $c$ , the endpoint $v_j = 0$ where $j$ 's demand is $0$ , and a numerator that may be constant on stretches.

Formalization scope

Variants are Fin n, 0-based (the paper's variant $i$ is index $i-1$ ). The no-purchase option is not a variant: $v_0$ is a separate real, with $v_0 > 0$ and $v_i > 0$ for all $i$ .
The demand $q_i^m(S)$ is the published definition RetailVariety.Structure.share (from RetailVariety.Structure.Model), with assortments as Finset (Fin n). $q_i(v_j)$ is share applied to the preference vector with $j$ 's entry replaced by the variable, on insert j S, and $j \notin S$ is assumed.
The cost $c : \mathbb R \to \mathbb R$ is assumed concave and monotone on $[0,1]$ only (ConcaveOn ℝ (Set.Icc 0 1) c, MonotoneOn c (Set.Icc 0 1)). Nothing is assumed about $c(0)$ , so $h^m(0) = -c(0)$ .
Margins m : Fin n → ℝ are arbitrary reals. The monotone-margin assumption of §3 is not needed and not imposed.
Quasi-convexity is Mathlib's QuasiconvexOn ℝ (Set.Ici 0). The domain is the closed half-line, including $v_j = 0$ .
The milestones (6), monotone numerator and single crossing add differentiability of $c$ on $(0,1)$ , because they are stated with $c' =$ deriv c. The goal does not.

The following formalizations would trivialize the problem and are ruled out: a specific cost (newsvendor, power, linear); convexity instead of quasi-convexity; $h^m$ only on $(0,\infty)$ ; or a common margin imposed without need.

Contributions welcome: proofs of the milestones, a proof of the goal that avoids derivatives, and general lemmas on quasi-convex functions of one variable and on the algebra of MNL shares, which the companion missions of this series (I and III–V) can reuse.

Selected references

G. P. Cachon, C. Terwiesch, Y. Xu, Retail Assortment Planning in the Presence of Consumer Search, working paper, The Wharton School, December 20, 2002. Published in Manufacturing & Service Operations Management 7(4):330–346, 2005. doi:10.1287/msom.1050.0088
G. van Ryzin, S. Mahajan, On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments, Management Science 45(11):1496–1509, 1999. doi:10.1287/mnsc.45.11.1496
S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992 (Chapter 2: the MNL formula (2)). doi:10.7551/mitpress/2450.001.0001

6 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Statistics·Captain: mikedeng1

Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization 3: The Big-M Relaxation Is at Least as Strong as PR(∞) for M ≤ ½√(λ0/λ2) and at Most as Strong for M ≥ √(λ0/λ2)Research Paper

Motivation

Best subset selection with a ridge term, the $\ell_0\ell_2$ -regularized least squares problem

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

is a standard model for sparse linear regression. It can be solved to certified optimality by branch-and-bound (BnB) over a mixed integer formulation, and the speed of BnB depends on how tight the lower bounds of its node relaxations are. Two mixed integer formulations are in common use: the Big-M formulation, which links each coefficient to a binary indicator through a box $|\beta_i| \le M z_i$ (Bertsimas, King and Mazumder, 2016), and the perspective formulation, which replaces $\beta_i^2$ by an auxiliary variable constrained by a rotated second-order cone (Frangioni and Gentile, 2006; Günlük and Linderoth, 2010). Which formulation gives the stronger continuous relaxation decides which one a solver should be built on.

Hazimeh, Mazumder and Saab (2021) compare the relaxations in Section 2. Their Proposition 2 compares the interval relaxation of the Big-M formulation with that of the perspective formulation without a box, $\mathrm{PR}(\infty)$ , studied by Dong, Chen and Linderoth (2015). This mission formalizes that comparison.

Setting

Fix a design matrix $X \in \mathbb R^{n\times p}$ , a response $y \in \mathbb R^n$ , parameters $\lambda_0, \lambda_2 > 0$ and a bound $M > 0$ . Write $[p] = \{1,\dots,p\}$ and $\|\beta\|_\infty \le M$ for $|\beta_i| \le M$ for every $i \in [p]$ .

The Big-M formulation (2) is

\min_{\beta, z}\ \tfrac12\|y - X\beta\|_2^2 + \lambda_0\sum_{i\in[p]} z_i + \lambda_2\|\beta\|_2^2 \quad\text{s.t.}\quad -Mz_i \le \beta_i \le Mz_i,\ z_i\in\{0,1\}.

Its interval relaxation replaces $z_i \in \{0,1\}$ by $z_i \in [0,1]$ ; its optimal value is $V_{B(M)}$ . Eliminating $z$ gives the equivalent form (37),

V_{B(M)} = \min_{\|\beta\|_\infty\le M} H(\beta),\qquad H(\beta) = \tfrac12\|y - X\beta\|_2^2 + \sum_{i\in[p]}\Big(\frac{\lambda_0}{M}|\beta_i| + \lambda_2\beta_i^2\Big).

The reverse Huber penalty is $\mathcal B(t) = |t|$ for $|t| \le 1$ and $\mathcal B(t) = (t^2+1)/2$ for $|t| \ge 1$ , and $\psi_1(b;\lambda_0,\lambda_2) = 2\lambda_0\mathcal B(b\sqrt{\lambda_2/\lambda_0})$ . The interval relaxation of $\mathrm{PR}(\infty)$ has the value (6),

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

Let $\mathcal S(\lambda_2)$ be the set of minimizers of $G$ , and, as in (9),

\mathcal L(M) = \{\lambda_2 > 0 \;:\; \exists\beta\in\mathcal S(\lambda_2) \text{ with } \|\beta\|_\infty \le M\}.

The comparison runs through the scalar function $t(b) = 2\lambda_0\mathcal B(b\sqrt{\lambda_2/\lambda_0}) - \frac{\lambda_0}{M}|b| - \lambda_2 b^2 = \psi_1(b) - \big(\tfrac{\lambda_0}{M}|b| + \lambda_2 b^2\big)$ and through $v^*(M) = \min_{\|\beta\|_\infty\le M} G(\beta)$ .

Formalization targets

Goal: Proposition 2 (p. 7)

V_{B(M)} \ge V_{PR(\infty)}\quad\text{if } M \le \tfrac12\sqrt{\lambda_0/\lambda_2},\qquad (10)

V_{B(M)} \le V_{PR(\infty)}\quad\text{if } M \ge \sqrt{\lambda_0/\lambda_2} \text{ and } \lambda_2 \in \mathcal L(M).\qquad (11)

Milestones, in the order of the paper's proof

(37): $V_{B(M)} = \min_{\|\beta\|_\infty\le M} H(\beta)$ , attained.
(10) on its own.
Lemma 1: for $M \ge \sqrt{\lambda_0/\lambda_2}$ and $b \in [-M, M]$ , $t(b) \ge 0$ .
(41): for $M \ge \sqrt{\lambda_0/\lambda_2}$ , $v^*(M) \ge V_{B(M)}$ .

The mission also contains the scalar inequality (39) as a supporting statement (not a milestone): for $M \le \frac12\sqrt{\lambda_0/\lambda_2}$ and $|b| \le M$ , $t(b) = (2\sqrt{\lambda_0\lambda_2} - \lambda_0/M)|b| - \lambda_2 b^2 \le 0$ .

Significance

Proposition 2 says that neither relaxation dominates the other. For a tight Big-M bound the Big-M relaxation yields the larger lower bound; for a loose one, provided some optimal solution of $\mathrm{PR}(\infty)$ lies in the box, the perspective relaxation does. Equivalently, with the other data fixed, a small $\lambda_2$ favours the Big-M relaxation and a large $\lambda_2$ favours $\mathrm{PR}(\infty)$ (p. 8). Together with Proposition 1 of the same paper, which shows that the box-constrained perspective relaxation $\mathrm{PR}(M)$ beats both when $\sqrt{\lambda_0/\lambda_2} > M$ , this motivates the paper's choice of $\mathrm{PR}(M)$ as the formulation on which its BnB solver is built.

The proposition is proved in the paper (Appendix A, pp. 29–30). No machine-checked proof of it, of the reformulation (37), or of any property of the reverse Huber penalty exists on the platform. The mission produces a formal statement of both inequalities with every hypothesis explicit, and the definitions of the two relaxation values in a form that later missions on perspective relaxations can reuse.

Difficulty

The scalar inequalities (39) and Lemma 1 are elementary but split into cases at the kink of the reverse Huber penalty, $|b| = \sqrt{\lambda_0/\lambda_2}$ , and at the sign of $2\sqrt{\lambda_0\lambda_2} - \lambda_0/M$ . The passage from coordinatewise inequalities to optimal values is where care is needed. $V_{B(M)}$ is defined over pairs $(\beta, z)$ , and its identification with a minimum of $H$ over a compact box requires eliminating $z$ and showing attainment. For (11) a pointwise comparison of $G$ and $H$ on the box only bounds $V_{B(M)}$ by the box-restricted value $v^*(M)$ , not by $V_{PR(\infty)}$ , which is an infimum over all of $\mathbb R^p$ ; the hypothesis $\lambda_2 \in \mathcal L(M)$ is what closes this gap, and dropping it gives a statement the paper does not prove.

Formalization scope

Optimal values are real infima (sInf): $V_{B(M)}$ over the feasible pairs $(\beta, z)$ of the interval relaxation, $V_{PR(\infty)}$ over all of $\mathbb R^p$ , $v^*(M)$ over the box. For $\lambda_0, \lambda_2 > 0$ each set of values is nonempty ( $\beta = z = 0$ ) and bounded below by $0$ , so no infimum takes Lean's junk value. $V_{PR(\infty)}$ is defined as the displayed minimum (6); its identification with the interval relaxation of $\mathrm{PR}(\infty)$ is a result of Dong, Chen and Linderoth that the paper cites and does not prove, and it is not part of this mission. $\mathcal S(\lambda_2)$ is the set of minimizers of $G$ , as the paper uses it in the proof of (11).

All theorems assume $\lambda_0, \lambda_2, M > 0$ . The paper remarks that Proposition 2 applies for any $M \ge 0$ ; $M = 0$ is excluded because $H$ and $t$ divide by $M$ . The goal is stated for optimal values, not for the objective functions at a single point: a pointwise comparison of $H$ and $G$ is a milestone, not the proposition. Milestone (37) is stated with IsLeast, so it asserts attainment as well as the value.

The paper states no $O(\cdot)$ bounds in this result, so no constants are instantiated. Contributions welcome: proofs of the scalar lemmas, of (37) (which needs compactness of the box and continuity of $H$ ), and of the goal.

Selected references

H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2, 2021; Mathematical Programming, 2022. https://arxiv.org/abs/2004.06152
H. Dong, K. Chen, J. Linderoth, Regularization vs. Relaxation: A conic optimization perspective of statistical variable selection, arXiv preprint, 2015. https://arxiv.org/abs/1510.06083
D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, The Annals of Statistics 44(2), 813–852, 2016. https://doi.org/10.1214/15-AOS1388
A. Frangioni, C. Gentile, Perspective cuts for a class of convex 0–1 mixed integer programs, Mathematical Programming 106(2), 225–236, 2006. https://doi.org/10.1007/s10107-005-0594-3
O. Günlük, J. Linderoth, Perspective reformulations of mixed integer nonlinear programs with indicator variables, Mathematical Programming 124(1–2), 183–205, 2010. https://doi.org/10.1007/s10107-010-0360-z
A. B. Owen, A robust hybrid of lasso and ridge regression, Contemporary Mathematics 443, 59–72, 2007 (the reverse Huber penalty).

11 thms2 active usersReviewed

Completed

Information Theory Machine Learning Optimal Transport·Captain: mikedeng1

Computational Optimal Transport VII: The Entropic Optimal Coupling P_ε Tends to the Maximum-Entropy Optimal Plan as ε → 0 and to a ⊗ b as ε → ∞Textbook

Motivation

The discrete optimal transport problem of Kantorovich asks for the cheapest way to move a probability histogram $\mathbf a$ onto a histogram $\mathbf b$ when moving a unit of mass from $i$ to $j$ costs $\mathbf C_{i,j}$ . Its optimal couplings are vertices of a polytope and are typically sparse: they rely on a few routes. Two communities have reasons to blur them. In transportation planning, observed traffic is more diffuse than linear-programming predictions, which led to the "gravity" model of Wilson (1969) and Erlander (1980), as recounted in Peyré and Cuturi, §4.1. In machine learning and statistics, adding an entropy term to the objective turns the linear program into a strictly convex problem that Sinkhorn's matrix-scaling algorithm solves at scale (Cuturi, 2013).

Every use of the entropic problem raises the same question: what does the regularized solution approximate? Chapter 4 of Peyré and Cuturi's Computational Optimal Transport answers it in Proposition 4.1 for the two extreme regimes of the regularization strength $\varepsilon$ .

Timeline. Cominetti and San Martín (1994) studied the convergence of entropic penalties for linear programs, including first-order expansions near $\varepsilon = 0$ and $\varepsilon = +\infty$ . Peyré and Cuturi (2019) record the transport case as Proposition 4.1, with a short compactness proof.

Setting

Fix sizes $n, m \ge 1$ . A histogram is a vector of the probability simplex $\Sigma_n = \{\mathbf a \in \mathbb R^n_+ : \sum_i \mathbf a_i = 1\}$ . Given $\mathbf a \in \Sigma_n$ , $\mathbf b \in \Sigma_m$ , the set of couplings is

\mathbf U(\mathbf a,\mathbf b) = \{\mathbf P \in \mathbb R_+^{n\times m} : \mathbf P\mathbb 1_m = \mathbf a,\ \mathbf P^\top\mathbb 1_n = \mathbf b\},

nonnegative matrices with row sums $\mathbf a$ and column sums $\mathbf b$ . For a cost matrix $\mathbf C \in \mathbb R^{n\times m}$ write $\langle \mathbf C, \mathbf P\rangle = \sum_{i,j}\mathbf C_{i,j}\mathbf P_{i,j}$ . The Kantorovich problem is $\mathrm L_{\mathbf C}(\mathbf a,\mathbf b) = \min_{\mathbf P \in \mathbf U(\mathbf a,\mathbf b)}\langle \mathbf C,\mathbf P\rangle$ .

The discrete entropy of a coupling is

\mathbf H(\mathbf P) = -\sum_{i,j}\mathbf P_{i,j}(\log \mathbf P_{i,j} - 1),

with $0\log 0 = 0$ . For $\varepsilon > 0$ the entropic problem is

\mathrm L^\varepsilon_{\mathbf C}(\mathbf a,\mathbf b) = \min_{\mathbf P\in\mathbf U(\mathbf a,\mathbf b)}\langle \mathbf P,\mathbf C\rangle - \varepsilon\mathbf H(\mathbf P),

whose unique minimizer is $\mathbf P_\varepsilon$ . The maximum-entropy optimal coupling $\mathbf P^\star_0$ is the optimal coupling of the Kantorovich problem with the largest entropy. The Gibbs kernel is $\mathbf K_{i,j} = e^{-\mathbf C_{i,j}/\varepsilon}$ and the Kullback–Leibler divergence between matrices is $\mathrm{KL}(\mathbf P|\mathbf K) = \sum_{i,j}\mathbf P_{i,j}\log(\mathbf P_{i,j}/\mathbf K_{i,j}) - \mathbf P_{i,j} + \mathbf K_{i,j}$ .

In Lean these are couplings, frob and IsOptimalCoupling in CompOT.Assignment, and entropy, entObjective, IsEntropicOptimal, IsMaxEntropyOptimal, gibbs and klMat in CompOT.EntropicLimit.

Formalization targets

Goal: Proposition 4.1

For $\mathbf a\in\Sigma_n$ , $\mathbf b \in \Sigma_m$ and any cost matrix $\mathbf C$ ,

\mathbf P_\varepsilon \xrightarrow{\varepsilon\to 0^+} \mathbf P^\star_0,\qquad \mathrm L^\varepsilon_{\mathbf C}(\mathbf a,\mathbf b)\xrightarrow{\varepsilon\to 0^+}\mathrm L_{\mathbf C}(\mathbf a,\mathbf b),\qquad \mathbf P_\varepsilon\xrightarrow{\varepsilon\to+\infty}\mathbf a\otimes\mathbf b = (\mathbf a_i\mathbf b_j)_{i,j}.

Milestones

For $\varepsilon > 0$ , problem (4.2) has a unique optimal solution (§4.1, p. 425).
The maximum-entropy optimal coupling (4.3) exists and is unique (proof of Proposition 4.1, p. 426).
The sandwich (4.5): for an optimal $\mathbf P$ and $\varepsilon>0$ , $0 \le \langle\mathbf C,\mathbf P_\varepsilon\rangle - \langle \mathbf C,\mathbf P\rangle \le \varepsilon(\mathbf H(\mathbf P_\varepsilon) - \mathbf H(\mathbf P))$ .
$\mathbf a \otimes \mathbf b$ is the unique maximizer of $\mathbf H$ on $\mathbf U(\mathbf a,\mathbf b)$ (p. 426).
(4.7): $\mathbf P_\varepsilon$ is the KL projection of the Gibbs kernel onto $\mathbf U(\mathbf a,\mathbf b)$ (p. 428).

Significance

The result. Proposition 4.1 justifies the entropic regularization as an approximation scheme: for small $\varepsilon$ the regularized plan converges to an exact optimal plan, and specifically to a canonical one, the most diffuse among all optimal couplings, so the limit does not depend on any tie-breaking. The value $\mathrm L^\varepsilon_{\mathbf C}$ converges to the transport cost, which is what makes Sinkhorn-based estimates of transport distances meaningful. For large $\varepsilon$ the plan becomes the independent coupling $\mathbf a\otimes\mathbf b$ , which explains the interpolation between optimal transport and maximum mean discrepancy studied later in the book. The KL projection identity (4.7) is the starting point of Sinkhorn's algorithm, so this mission also supplies the bridge to the next missions of the series.

Formalizing it. The proposition is a known result with a complete proof in the source; the work is formalizing it in Lean 4 with Mathlib. To our knowledge none of these statements, nor the discrete entropic transport problem itself, has a machine-checked proof in Mathlib or on the platform. A formal proof also pins down the convention for zero entries, on which the statement silently depends.

Difficulty

The obvious argument passes to the limit in the optimality of $\mathbf P_\varepsilon$ , but this only shows that limit points are optimal for the Kantorovich problem; it does not identify which optimal coupling is the limit when the optimal set is a face of the polytope rather than a vertex. Identifying it requires a second-order argument at the level of the entropy, and the convergence of the whole family (not just a subsequence) rests on the uniqueness of the maximum-entropy optimal coupling, which in turn needs strict concavity of $\mathbf H$ on a set that may contain matrices with zero entries, where the logarithm is singular. Existence and uniqueness of $\mathbf P_\varepsilon$ face the same boundary issue: the minimizer may a priori sit on the boundary of the polytope.

Formalization scope

Indices are 0-based (Fin n, Fin m); histograms are functions Fin n → ℝ in Mathlib's stdSimplex; matrices are Matrix (Fin n) (Fin m) ℝ with the product topology, so convergence is entrywise. Entropy uses $0\log 0 = 0$ (Real.negMulLog); the book's remark that $\mathbf H = -\infty$ at a zero entry is not used, since it would contradict the continuity of $\mathbf H$ invoked in the book's proof and make (4.3) degenerate. Optimality is expressed by predicates (a minimizer over $\mathbf U(\mathbf a,\mathbf b)$ ), never by a real infimum, so no junk value of an empty infimum appears. The limit $\varepsilon \to 0$ is taken from the right. The values $\mathrm L^\varepsilon_{\mathbf C}$ and $\mathrm L_{\mathbf C}$ appear as the objectives at $\mathbf P_\varepsilon$ and $\mathbf P^\star_0$ .

In the goal, $\mathbf P_\varepsilon$ and $\mathbf P^\star_0$ are given by hypotheses (any family solving (4.2) for every $\varepsilon > 0$ , any solution of (4.3)). This is not a vacuous formalization: milestones 1 and 2 assert that such objects exist and are unique, so the hypotheses are satisfiable and determine them. Standing assumptions are exactly those of the book: $\mathbf a \in \Sigma_n$ , $\mathbf b \in \Sigma_m$ , $\varepsilon > 0$ ; no positivity of $\mathbf a$ , $\mathbf b$ or $\mathbf C$ is assumed.

A complete development needs: compactness of the transport polytope, continuity and strict concavity of $x \mapsto -x\log x$ on $[0,\infty)$ , and the Gibbs inequality on finite sums. These are reusable for the Sinkhorn and entropic-duality missions of this series. Proofs of any milestone are welcome independently.

Selected references

G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073 (§4.1, pp. 425–430)
R. Cominetti and J. San Martín, Asymptotic analysis of the exponential penalty trajectory in linear programming, Mathematical Programming 67(1–3):169–187, 1994. https://doi.org/10.1007/BF01582220
M. Cuturi, Sinkhorn Distances: Lightspeed Computation of Optimal Transport, NeurIPS 2013. https://arxiv.org/abs/1306.0895
A. G. Wilson, The use of entropy maximizing models, in the theory of trip distribution, mode split and route split, Journal of Transport Economics and Policy, 108–126, 1969 (bibliography of Peyré and Cuturi). https://doi.org/10.1561/2200000073
S. Erlander, Optimal Spatial Interaction and the Gravity Model, Vol. 173, Springer-Verlag, 1980 (bibliography of Peyré and Cuturi). https://doi.org/10.1561/2200000073

7 thms2 active usersReviewed

Missions

Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models 1: Augmented Greedy Earns a (1 − 1/e) Fraction of the Optimal Revenue from the Complete Customer TypesResearch Paper

Motivation

Setting

Formalization targets

Theorem 4.2: complete-type revenue

Supporting targets

Significance

Difficulty

Formalization scope

Selected references

Intrinsic Robustness of the Price of Anarchy III: For Every Set of Cost Functions, Congestion Games Are Tight — the Worst-Case Pure Price of Anarchy Equals the Best Smoothness BoundResearch Paper

Motivation

Setting

Formalization targets

Tightness of the congestion-game class

Resourcewise characterization

Significance

Difficulty

Formalization scope

Selected references

A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights II: The ODE Solution Satisfies f(X(t)) − f⋆ ≤ 2‖x₀ − x⋆‖²/t²Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 7)

Milestones (proof of Theorem 3, pp. 7–8)

Significance

Difficulty

Formalization scope

Selected references

Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition IV: Stochastic Gradient Rates LC²/(2kμ²) and (1 − 2μα)^k [f(x_0) − f*] + LC²α/(4μ)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4 (p. 6)

Milestones (proof of Theorem 4, p. 7)

Significance

Difficulty

Formalization scope

Selected references

Accelerated Gradient Methods for Nonconvex Nonlinear and Stochastic Programming 1: The AG Method Converges on Smooth Nonconvex Problems and Attains the Optimal Rate When Ψ Is ConvexResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 5)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Online Contention Resolution Schemes with Applications to Bayesian Selection Problems 2: The Degree Relaxation of Matching Has a (b, e^(−2b))-Selectable Randomized Greedy OCRSResearch Paper

Why online matching needs a stronger rounding guarantee

Finite graphs, fractional edges, and greedy families

Formalization targets

Theorem 2.7: a randomized matching scheme

Remark (p. 14): the deterministic variant

What the result contributes

Where the argument is delicate

Formalization scope

Selected references

Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness III: Adaptive Restarts Take at Most ⌈2C(q+2)/(αβ)⌉ Inner Steps and Converge Linearly on Sharp ProblemsResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

VC Theory for Inventory Policies: Xie–Ma–Xin BoundsResearch Paper

Learning inventory policies from historical demand

Demand, policy classes and statistical errors

Formalization targets

What the formalization supplies

Mathematical difficulty

Formalization scope and conventions

Selected references

Semidefinite Programming Hierarchies for Constrained Bilinear Optimization I: The Linearly Constrained de Finetti SDP Hierarchy Satisfies Q ≤ SDPₙ ≤ Q + ‖G‖∞·d_B²(d_B+1)·√((2 ln 2) log d_A / n)Research Paper

Motivation