Optimization

Completed

Calculus of Variations·Captain: wenxinzhang

Vector Space Methods VII: Euler–Lagrange EquationsTextbook

Motivation

The calculus of variations replaces optimization over finitely many coordinates by optimization over paths. Its necessary conditions underlie geodesics, minimum-energy curves, classical mechanics, and many optimal-control models. Chapter 7 of David G. Luenberger's Optimization by Vector Space Methods presents this transition as an application of differentiation in normed vector spaces: a local extremum first forces every directional derivative to vanish, and the resulting integral identity forces a differential equation along the optimizing path. This mission formalizes the scalar, fixed-endpoint version in §§7.4–7.5. The target is intentionally the theorem actually isolated by the source, not a stronger modern Sobolev-space variant.

Setting

Fix real numbers $a<b$ . A $C^1$ path on the segment is represented in Lean by two functions, $x,\dot x:\mathbb R\to\mathbb R$ . Both are continuous on $[a,b]$ , and $x$ has derivative $\dot x(t)$ at every $t\in(a,b)$ . Ordinary two-sided derivatives are not demanded at $a$ or $b$ ; this makes the formal endpoint convention match the one-sided role of endpoints in a closed interval.

Let $L(y,v,t)$ be a scalar Lagrangian. Along a candidate path, write

L_x(t)=\frac{\partial L}{\partial y}(x(t),\dot x(t),t),\qquad L_v(t)=\frac{\partial L}{\partial v}(x(t),\dot x(t),t).

The Lean statement records these partial derivatives with HasDerivAt and assumes that $L_x$ and $L_v$ are continuous on $[a,b]$ . A fixed-endpoint variation is another $C^1$ pair $(h,\dot h)$ with $h(a)=h(b)=0$ . The first variation already computed from the action is

\delta J(x;h)=\int_a^b\bigl(L_x(t)h(t)+L_v(t)\dot h(t)\bigr)\,dt.

The main theorem begins from the stationarity identity $\delta J(x;h)=0$ for every such variation. It does not claim that the complete passage from a local extremum in Luenberger's $C^1$ norm to this integral formula has already been bundled into the root statement.

Formalization targets

Main goal: Euler–Lagrange equation

From the computed first-variation identity, prove that

\frac{d}{dt}L_v(t)=L_x(t)\qquad(t\in(a,b)).

The conclusion is expressed as HasDerivAt Lv (Lx t) t, so it asserts both differentiability of $L_v$ and the equality of its derivative with $L_x$ . This is equation (2) and the conclusion reached on printed pages 180–181.

Milestones

The first milestone formalizes §7.4, Theorem 1: a local minimum or maximum of a real functional has zero derivative along every direction whenever that scalar directional derivative exists. The remaining milestones are the three fixed-endpoint fundamental lemmas from §7.5. They respectively show that a continuous coefficient annihilating all variations is zero, that a continuous coefficient annihilating all variation derivatives is constant, and that an identity involving both $h$ and $\dot h$ forces the second coefficient to have derivative equal to the first. These are stated with the same $C^1$ variation class used by the goal.

Significance

The result turns an infinite family of scalar integral equalities into a pointwise differential equation. Once available, the same interface can support standard variational examples by supplying a concrete $L$ , its two partial derivatives, and a stationary path. It also provides the analytic core needed before treating natural boundary conditions, vector-valued paths, higher derivatives, or weak Euler–Lagrange equations.

The formalization adds reusable interval-sensitive infrastructure. In particular, IsC1OnSegment separates a path from its chosen continuous derivative and avoids silently imposing derivatives outside the optimization interval. The three fundamental lemmas are useful independently of the named Euler–Lagrange theorem: they are test-function principles for interval integrals and can serve later missions involving integration by parts or weak formulations. The mathematics is classical and proved in the cited text; the open work is a machine-checked Lean development of these exact statements in the pinned Mathlib environment.

Difficulty

The source argument uses informal phrases such as “arbitrary $C^1$ function vanishing at the endpoints” and treats endpoint differentiation according to standard calculus convention. In Lean, those phrases must determine a precise domain, derivative witness, continuity requirement, and interval-integral orientation. Replacing $C^1$ variations by merely continuous functions would change Lemmas 2 and 3, while requiring HasDerivAt at the endpoints would add a hypothesis not present in the book.

Another tempting shortcut is to assume from the outset that $L_v$ is differentiable and then use integration by parts. That would trivialize the central regularity conclusion of Lemma 3: the book derives differentiability of $L_v$ from stationarity and continuity. The root therefore assumes only continuity of the two coefficient functions and concludes a HasDerivAt assertion on the open interval. Conversely, constructing the first variation from a local extremum of the action requires a separate differentiation-under-the-integral development and a topology on bundled $C^1$ paths; it is not hidden inside the main goal.

Formalization scope

The scalar field, path values, time variable, and action values are all real. The interval is nondegenerate through the explicit hypothesis $a<b$ . Integrals use Mathlib's oriented interval integral, but all principal statements are made in the forward orientation. Paths and variations are total functions on $\mathbb R$ whose relevant regularity is restricted to $[a,b]$ . The Lagrangian is finite-valued. No measurability or integrability premise is omitted: continuity of the coefficient and variation factors on the compact interval supplies the intended finite integrals.

The goal starts from an already computed first-variation identity. Contributions connecting a genuine local extremum of the action in the norm $\max|x|+\max|\dot x|$ to that identity are welcome as a strengthening, but they must not be advertised as part of the present root theorem. Other welcome contributions include reusable continuous test-function constructions and endpoint-aware interval integration lemmas. Sobolev paths, vector-valued state spaces, free endpoints, and weak derivatives are outside this mission and should be proposed separately rather than obtained by weakening the stated hypotheses until the result becomes vacuous.

Selected references

David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 7, §§7.4–7.5, pp. 178–181; definition of $D[a,b]$ on p. 23. Open Library record

6 thms2 active usersReviewed

Completed

Functional Analysis·Captain: wenxinzhang

Vector Space Methods VI: Pseudoinverse OperatorsTextbook

Motivation

Linear equations between Hilbert spaces need not have unique solutions and may not even be exactly solvable for a given right-hand side. Least squares selects a vector with the smallest residual; when several such vectors exist, minimum norm selects one canonical representative. Luenberger packages this two-stage optimization into the pseudoinverse of a continuous linear operator with closed range. The construction unifies exact equations, approximation, normal equations, and orthogonal projections, while retaining a bounded linear operator suitable for subsequent optimization methods (Luenberger, §§6.9--6.11, pp. 159--165).

This mission continues the series into Chapter 6. Its capstone formalizes the structural identities of the pseudoinverse, including involution, compatibility with adjoints, reflexive inverse laws, self-adjoint projection products, and factorizations through the normal operators. Earlier milestones establish the adjoint facts and minimum-norm characterizations on which that operator calculus depends.

Setting

Let $G$ and $H$ be real Hilbert spaces, represented in Lean by complete real inner-product spaces, and let $A:G\toL[\mathbb R]H$ be a continuous linear map whose range is closed. The Hilbert adjoint is written $A^\dagger$ in the Lean statements and is Mathlib's adjoint continuous linear map. It is characterized by the inner-product relation and satisfies $\|A^\dagger\|=\|A\|$ (Luenberger, §6.5, Theorem 1, p. 151). Closed range gives the range-kernel identity

\operatorname{range}(A^\dagger)=\ker(A)^\perp,

the Hilbert-space specialization of the closed range theorem used in the chapter (§6.6, Theorem 2, p. 156).

For $y\in H$ , a vector $x\in G$ is a least-squares solution when $\|Ax-y\|$ is no larger than $\|Az-y\|$ for every $z$ . A least-squares solution is minimum norm when its norm is no larger than that of every other least-squares solution. A continuous linear map $B:H\toL[\mathbb R]G$ satisfies VectorSpaceOpt.IsPseudoinverse A B when, for every $y$ , $By$ has both properties. This predicate is the mission's one lightweight definition, directly encoding the definition in §6.11 (pp. 163--164).

Formalization targets

Adjoint and closed-range milestones

Formalize $\|A^\dagger\|=\|A\|$ . Under closed range, formalize

\operatorname{range}(A^\dagger)=\ker(A)^\perp.

These record §6.5, Theorem 1 and the Hilbert form of §6.6, Theorem 2.

Normal equations and minimum-norm solutions

Formalize the least-squares equivalence

x\text{ minimizes }\|y-Ax\| \quad\Longleftrightarrow\quad A^\dagger A x=A^\dagger y,

as in §6.9, Theorem 1 (p. 160). For solvable $Ax=y$ and closed-range $A$ , characterize the minimum-norm solution by $x=A^\dagger z$ with $AA^\dagger z=y$ , following §6.10, Theorem 1 (pp. 161--162). Finally, formalize existence and uniqueness of a continuous linear $B$ satisfying IsPseudoinverse A B.

Pseudoinverse identities

Given such a $B$ , formalize that $A$ is the pseudoinverse of $B$ , that $B^\dagger$ is the pseudoinverse of $A^\dagger$ , and that

BAB=B,\qquad ABA=A,\qquad (BA)^\dagger=BA.

Also produce pseudoinverses $C$ of $A^\dagger A$ and $D$ of $AA^\dagger$ satisfying

B=CA^\dagger, \qquad B=A^\dagger D.

Together with the continuous-linear-map type of $B$ , these clauses encode all nine items of §6.11, Proposition 1 (p. 165).

Significance

The pseudoinverse turns a possibly inconsistent or underdetermined equation into a canonical bounded linear solution operator. The normal equations connect residual minimization with the self-adjoint operator $A^\dagger A$ ; the minimum-norm theorem selects the component orthogonal to the kernel. The capstone identities show that the construction behaves like an inverse on the effective ranges and that $BA$ is self-adjoint, while the two factorizations reduce pseudoinverse questions to the normal operators.

The underlying results are proved in Luenberger's text. Their Lean formalization supplies a reusable predicate for minimum-norm least squares and an operator-level API linking adjoints, kernels, ranges, composition, and optimization characterizations. This bridges the earlier missions on minimum norm and estimation with later chapters that use normal operators and generalized inverses. It also records explicitly which conclusions require closed range, preventing accidental use of a bounded pseudoinverse where only an unbounded generalized inverse could exist.

Difficulty

Pointwise existence of a best residual is not enough. The selected minimum-norm solutions must collectively form a linear bounded map, and closed range is the hypothesis that makes this global operator well behaved. Without closed range, least-squares minimizers may fail to exist and the inverse on the effective range need not be bounded. A formulation that chooses an arbitrary minimizer for each target would therefore miss the main analytic content.

Several notationally similar operations must also remain distinct. The book writes a star for the adjoint and a superscript dagger-like symbol for the pseudoinverse; Mathlib's displayed dagger denotes the Hilbert adjoint. The mission consequently names the generalized inverse through IsPseudoinverse instead of overloading dagger notation. Orthogonal complements apply to submodules, compositions must retain their source and target spaces, and each factorization involves a different normal operator. These typing constraints expose domain/codomain mistakes that paper notation suppresses.

Formalization scope

The mission uses real Hilbert spaces only: NormedAddCommGroup, InnerProductSpace ℝ, and CompleteSpace. Operators are ContinuousLinearMap, composition is ∘L, the Hilbert adjoint is Mathlib's †, and the closed-range assumption is IsClosed (A.range : Set H). The orthogonal complement in the range theorem is the submodule A.kerᗮ.

IsPseudoinverse A B requires two pointwise inequalities for every target: B y minimizes residual norm among all inputs, then minimizes norm among all residual minimizers. The second clause cannot be dropped or weakened to exact solutions, because it is what makes the choice canonical for inconsistent as well as underdetermined systems. The minimum-norm-solution milestone states y ∈ A.range explicitly; the source treats solvability as part of speaking about a solution. The capstone accepts a continuous linear $B$ satisfying the predicate, so linearity and boundedness are represented by its type, corresponding to the first two items of Proposition 1. Contributions may add reusable lemmas about adjoints, orthogonal complements, closed range, normal equations, or uniqueness of optimizers, but must preserve the closed-range and completeness assumptions in the public operator theorems.

Selected references

David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 6, especially §§6.5--6.11, pp. 151--165. Public scan.

7 thms2 active usersReviewed

Completed

Functional Analysis·Captain: wenxinzhang

Vector Space Methods IV: Minimum-Distance DualityTextbook

Motivation

Best approximation asks how closely a point can be represented by a prescribed linear model. In a Hilbert space, orthogonality turns this into a geometric projection problem. A general normed space has no inner product and may have no nearest point, so the corresponding certificate must live in the continuous dual rather than in the original space. Chapter 5 of Luenberger's Optimization by Vector Space Methods develops exactly this passage from geometry to duality: the Hahn--Banach theorem supplies continuous linear functionals that detect norms, separate points from closed subspaces, and certify an infimum distance even when that distance is not attained (Luenberger, §§5.4--5.8, pp. 111--120).

This mission continues the book's vector-space formalization series at the point where minimum-norm arguments cease to be specifically Hilbertian. Its capstone identifies the distance from a point to a linear subspace with the largest value at that point among all norm-at-most-one continuous linear functionals annihilating the subspace. The statement is a prototype for dual certificates throughout approximation theory and convex optimization.

Setting

Let $X$ be a real normed space and let $M$ be a linear subspace. In Lean, $M$ is represented by Submodule ℝ X; no topological closure assumption is imposed on the capstone. A continuous linear functional is an element $f : X \toL[\mathbb R] \mathbb R$ , with operator norm $\|f\|$ . It annihilates $M$ when $f(m)=0$ for every $m\in M$ . The set of all such functionals is the annihilator $M^\perp$ in the book's terminology.

For $x\in X$ , the infimum distance to $M$ is

d(x,M)=\inf_{m\in M}\|x-m\|.

The Lean target uses Metric.infDist x (M : Set X). Since every submodule contains zero, the underlying set is nonempty and this extended geometric notion is an ordinary nonnegative real number here. A functional $f$ is aligned with a vector $v$ when $f(v)=\|f\|\,\|v\|$ . Alignment is the normed-space replacement for the familiar inner-product equality associated with a projection direction.

Two auxiliary dual notions are also formalized. A norm-preserving Hahn--Banach extension takes a functional on a subspace and extends it to all of $X$ without changing its norm. A norming functional for $x$ is a nonzero functional aligned with $x$ . Finally, for closed $M$ , the preannihilator of its annihilator is exactly $M$ : the functionals vanishing on $M$ distinguish every point outside it (Luenberger, §§5.4 and 5.7, pp. 112--118).

Formalization targets

Norm-preserving extension and norming functionals

For a continuous functional $f$ on $M$ , formalize an extension $F$ satisfying

F|_M=f,\qquad \|F\|=\|f\|.

For nontrivial $X$ and every $x\in X$ , formalize the existence of a nonzero $f$ with $f(x)=\|f\|\,\|x\|$ . These are Corollaries 1 and 2 of §5.4 (pp. 112--113).

Closed-subspace double annihilator

For closed $M$ , formalize

\{x\in X: \forall f,\ f|_M=0 \Rightarrow f(x)=0\}=M.

This is the concrete set-valued form of Theorem 1 in §5.7 (p. 118).

Minimum-distance duality

For arbitrary $M$ and $x$ , produce one functional $f$ with $\|f\|\le 1$ , $f|_M=0$ , and

f(x)=d(x,M),\qquad g(x)\le d(x,M)

for every other $g$ of norm at most one annihilating $M$ . Thus $f$ realizes the dual maximum. If a best approximant $m_0\in M$ exists, the same certificate also satisfies

f(x-m_0)=\|f\|\,\|x-m_0\|.

This packages both parts of the minimum-distance theorem in §5.8 (Theorem 1, pp. 119--120).

Significance

The capstone gives an exact lower-bound certificate for an infinite-dimensional approximation problem. Every feasible dual functional supplies the inequality $g(x)\le d(x,M)$ , while the distinguished functional reaches equality. Consequently, the primal infimum is identified without assuming reflexivity, strict convexity, finite dimension, closedness of $M$ , or existence of a nearest point. When a nearest point does exist, alignment records the equality case of the norm estimate and links the dual certificate back to the geometry of the residual.

The source result is classical and proved in the book; the open work here is its machine-checked Lean formalization in the same namespace as the earlier vector-space missions. The reusable output includes norm-controlled extension infrastructure, norming functionals, a concrete double-annihilator theorem, and a certificate form of distance duality suitable for later convex-separation and constrained-optimization missions.

Difficulty

The obvious Hilbert-space formulation fails because a normed space has no canonical orthogonal complement and a minimizing element of $M$ need not exist. Replacing the minimum by Metric.infDist avoids an unjustified attainment assumption, but the desired dual maximizer must still be an actual continuous functional, not merely a limiting family. Norm control is essential: an algebraic separator without continuity cannot serve as a bounded dual certificate.

There are also degenerate cases that informal notation can hide. The distance may be zero even when $x\notin M$ if $M$ is not closed, and then the zero functional is the correct capstone witness. Conversely, the book's assertion that a norming functional is nonzero requires a nontrivial ambient space. The formal statements must handle these cases without silently strengthening the main theorem to closed subspaces or positive distance.

Formalization scope

All spaces and functionals are real, matching the chapter and avoiding extra complex-scalar conjugation conventions. The ambient object uses Mathlib's NormedAddCommGroup, NormedSpace, Submodule, and ContinuousLinearMap; completeness is not assumed because the cited Hahn--Banach consequences do not require it. The distance is exactly Metric.infDist, and annihilation is written pointwise rather than by introducing a new annihilator definition. This keeps the capstone self-contained while the double-annihilator milestone states the same construction explicitly as a set.

No claim is made that a best approximant exists. The alignment clause is conditional on an element already satisfying the global minimum property. No closedness assumption may be added to the capstone, since the zero-distance/nonclosed case is part of the source theorem's generality. The norming-functional milestone alone assumes [Nontrivial X]; this prevents a vacuous encoding of “nonzero functional” on the zero space. Contributions may establish the four stated theorems and any generally useful lemmas about restrictions, quotient norms, annihilation, or Metric.infDist, provided the public statements retain these conventions.

Selected references

David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 5, especially §§5.4, 5.7, and 5.8, pp. 111--120. Public scan.

4 thms2 active usersReviewed

Completed

Linear Optimization Operations Research·Captain: Shuze Chen

Introduction to Linear Optimization VI: Farkas' Lemma and Separating HyperplanesTextbook

When is a system of linear constraints infeasible? Sections 4.6-4.7 of Bertsimas-Tsitsiklis answer with the archetypal theorem of the alternative. The capstone is Farkas' lemma (Theorem 4.6): for an $m \times n$ matrix $A$ and $b \in \mathbb{R}^m$ , exactly one of the following holds — (a) some $x \ge 0$ satisfies $Ax = b$ , or (b) some $p$ satisfies $p'A \ge 0'$ and $p'b < 0$ ; such a $p$ is a certificate of infeasibility, geometrically a hyperplane separating $b$ from the cone of the columns of $A$ . The mission also carries the cone-membership restatement (Corollary 4.3), the inequality form (Theorem 4.7: every solution of $Ax \le b$ satisfies $c'x \le d$ iff some $p \ge 0$ has $p'A = c'$ and $p'b \le d$ ), and the application to asset pricing (Theorem 4.8: a market's prices admit no arbitrage iff there is a nonnegative state-price vector $q$ with $p_i = \sum_s q_s r_{si}$ ). The book proves Farkas' lemma from LP strong duality; Section 4.7 then reverses the arrow from first principles: every polyhedron is closed (Theorem 4.9), Weierstrass' theorem (Theorem 4.10, already in Mathlib), and the separating hyperplane theorem (Theorem 4.11: for nonempty closed convex $S$ and $x^* \notin S$ there exists $c$ with $c'x^* < c'x$ for all $x \in S$ ), from which Farkas' lemma — and hence the duality theorem itself — follows geometrically.

8 thms2 active usersReviewed

Completed

Linear Optimization·Captain: Shuze Chen

Introduction to Linear Optimization III: Fourier–Motzkin Elimination and Projections of PolyhedraTextbook

Is the shadow of a polyhedron again a polyhedron? §2.8 of Bertsimas–Tsitsiklis answers this with perhaps the oldest method for solving linear programming problems: Fourier–Motzkin elimination. Given $P = \{x \in \mathbb{R}^n \mid \sum_{j=1}^n a_{ij}x_j \ge b_i,\ i = 1, \dots, m\}$ , one sorts the constraints by the sign of the coefficient of $x_n$ — rewriting them as $x_n \ge d_i + \mathbf{f}_i'\bar{x}$ , $d_j + \mathbf{f}_j'\bar{x} \ge x_n$ , or $0 \ge d_k + \mathbf{f}_k'\bar{x}$ — and forms the polyhedron $Q \subset \mathbb{R}^{n-1}$ whose constraints are all pairwise combinations $d_j + \mathbf{f}_j'\bar{x} \ge d_i + \mathbf{f}_i'\bar{x}$ together with the constraints not involving $x_n$ . The capstone, Theorem 2.10, states that $Q$ is exactly the projection $\Pi_{n-1}(P)$ of $P$ onto its first $n-1$ coordinates: a value of $x_n$ can be interpolated if and only if every lower bound is below every upper bound. Though hopeless as an algorithm (the number of constraints can grow exponentially), elimination has powerful theoretical corollaries, all formalized here: projections $\Pi_k(P)$ of polyhedra are polyhedra (Corollary 2.4), the image of a polyhedron under any linear mapping is a polyhedron (Corollary 2.5), and the convex hull of finitely many vectors is a polyhedron (Corollary 2.6) — the first half of the finite-basis picture completed by the resolution theorem of Mission VII.

6 thms2 active usersReviewed

Completed

Linear Optimization Operations Research·Captain: Shuze Chen

Introduction to Linear Optimization II: Existence and Optimality of Extreme PointsTextbook

Where should one look for the optimum of a linear programming problem? Chapter 1 of Bertsimas–Tsitsiklis suggests that optima "tend to occur at corners" of the feasible polyhedron; §§2.5–2.6 turn this intuition into theorems. Not every polyhedron has a corner — a halfspace in $\mathbb{R}^n$ ( $n > 1$ ) has none — and the exact dividing line is the presence of an infinite line: a nonempty polyhedron

P = \{x \mid a_i'x \ge b_i,\ i = 1, \dots, m\}

has an extreme point if and only if it does not contain a line, if and only if $n$ of the vectors $a_1, \dots, a_m$ are linearly independent (Theorem 2.6). In particular every nonempty bounded polyhedron and every nonempty standard-form polyhedron has a basic feasible solution (Corollary 2.2). The capstone, Theorem 2.8, is the sharpest form of the corner principle: if $P$ has at least one extreme point, then for any cost vector $c$ either the optimal cost is $-\infty$ , or there is an extreme point of $P$ that is optimal — existence of an optimal solution comes for free once the cost is bounded below. Its companion Theorem 2.7 places an optimal extreme point under the weaker assumption that an optimal solution exists, and Corollary 2.3 — the fundamental theorem of linear programming — concludes that every feasible LP either has optimal cost $-\infty$ or attains an optimal solution, in stark contrast with nonlinear problems such as minimizing $1/x$ over $x \ge 1$ . These results license the extreme-point search that the simplex method (Mission IV) performs.

12 thms2 active usersReviewed

Convex Optimization Operations Research·Captain: mikedeng1

A Primal-Dual Smoothing Framework for Max-Structured Non-Convex Optimization: The Framework Returns an ε-Near-Stationary Point Within an Explicit Number of IterationsResearch Paper

Motivation

Many problems in robust optimization, adversarial learning, distributionally robust learning and min-max games have the max-structured form

\min_{x\in\mathcal X}\ q(x):=f(x)+r(x),\qquad f(x):=\max_{y\in\mathcal Y}\ \Phi(x,y)-g(y),

where $\Phi$ is smooth in $x$ but not convex, and concave in $y$ . The function $f$ is neither smooth nor convex, so gradient methods do not apply directly and convex duality does not close the problem. The standard target is then a near-stationary point: a point close to its own proximal point. In Hilbert spaces this notion and the matching algorithms are well developed (Davis and Drusvyatskiy 2019, doi:10.1137/18M1178244; Thekumparampil et al. 2019, arXiv:1907.01543). Many applications, however, live on simplices or spectral sets where the natural norm is $\ell_1$ or a Schatten norm and the natural proximal geometry is a Bregman divergence (entropy, for example).

R. Zhao (Mathematics of Operations Research, 2024; arXiv:2003.04375) gives a primal-dual smoothing framework for this problem in arbitrary finite-dimensional normed spaces. The dual variable is smoothed by a strongly convex function, and the primal problem is handled by an inexact Bregman proximal-point method. This mission formalizes the outer-loop guarantee of that framework: an explicit iteration bound after which the method returns an $\varepsilon$ -near-stationary point.

Setting

Let $\mathbb X$ and $\mathbb Y$ be finite-dimensional real normed spaces with arbitrary norms. Write $\mathcal X\subseteq\mathbb X$ for a nonempty closed convex set, the domain of a convex lower semicontinuous $r$ , and $\mathcal Y\subseteq\mathbb Y$ for a nonempty convex compact set. The function $g$ is convex and continuous on $\mathcal Y$ . $\Phi$ is jointly continuous, $\Phi(x,\cdot)$ is concave, and $\Phi(\cdot,y)$ is differentiable and $\gamma$ -weakly convex on $\mathcal X$ for some $\gamma>0$ :

\Phi(x',y)-\Phi(x,y)-\langle\nabla_x\Phi(x,y),x'-x\rangle\ge-\tfrac\gamma2\|x'-x\|^2 .

A distance generating function $\omega_{\mathcal X}$ is continuous and 1-strongly convex on $\mathcal X$ , and differentiable at every point of $\mathcal X$ with a $\beta_{\mathcal X}$ -Lipschitz gradient ( $\beta_{\mathcal X}\ge1$ ). Its Bregman divergence is $D_{\omega_{\mathcal X}}(x',x)=\omega_{\mathcal X}(x')-\omega_{\mathcal X}(x)-\langle\nabla\omega_{\mathcal X}(x),x'-x\rangle$ . For $0<\lambda<\gamma^{-1}$ , the proximal point $\mathrm{prox}(q,x,\lambda)$ minimizes $Q^\lambda(x';x)=q(x')+\lambda^{-1}D_{\omega_{\mathcal X}}(x',x)$ over $\mathcal X$ . A point $x\in\mathcal X$ is an $\varepsilon$ -NS point if, for some such $\lambda$ , $\|\lambda^{-1}(x-\mathrm{prox}(q,x,\lambda))\|\le\varepsilon/\beta_{\mathcal X}$ .

Dual smoothing: for a 1-strongly convex continuous $\omega_{\mathcal Y}$ on $\mathcal Y$ , set $f_\rho(x)=\max_{y\in\mathcal Y}\Phi(x,y)-g(y)-\rho\,\omega_{\mathcal Y}(y)$ , $q_\rho=f_\rho+r$ , and $R_{\mathcal Y}(\omega_{\mathcal Y})=\sup_{\mathcal Y}|\omega_{\mathcal Y}|$ .

Algorithm 1 fixes $\eta>0$ , $\lambda\in(0,\gamma^{-1})$ and $\rho=2\eta/R_{\mathcal Y}(\omega_{\mathcal Y})$ , and starts from $x_1\in\mathcal X$ . Iteration $k$ finds $x_{k+1}\in\mathcal X$ with $Q^\lambda_\rho(x_{k+1};x_k)\le\min_{\mathcal X}Q^\lambda_\rho(\cdot\,;x_k)+\eta$ , where $Q^\lambda_\rho$ is $Q^\lambda$ with $q_\rho$ in place of $q$ . It stops at the first $K$ with $\|x_{K+1}-x_K\|\le\sqrt{2\eta/(\lambda^{-1}-\gamma)}$ and outputs $x_K$ .

Formalization targets

Goal: Corollary 4.1

For $\lambda\in(0.8\gamma^{-1},\gamma^{-1})$ , $\varepsilon>0$ and $\eta=\varepsilon^2\lambda(1-\gamma\lambda)/(32\beta_{\mathcal X}^2)$ , every run of Algorithm 1 stops at a first index

K\le\left\lceil\frac{32\beta_{\mathcal X}^2(q(x_1)-q^*)}{5\varepsilon^2\lambda(\gamma\lambda-0.8)}\right\rceil+1,

and $x_K$ is an $\varepsilon$ -NS point. Here $q^*$ is the optimal value, or any lower bound of $q$ on $\mathcal X$ .

Milestones

(3.7): $|f_\rho-f|\le\rho R_{\mathcal Y}(\omega_{\mathcal Y})$ on $\mathcal X$ .
$Q^\lambda(\cdot\,;x)$ is $(\lambda^{-1}-\gamma)$ -strongly convex on $\mathcal X$ (p. 13).
$Q^\lambda_\rho(\cdot\,;x)$ is $(\lambda^{-1}-\gamma)$ -strongly convex on $\mathcal X$ (p. 15).
Lemma 4.2: $\|x_K-\mathrm{prox}(q_\rho,x_K,\lambda)\|\le2\sqrt{2\eta/(\lambda^{-1}-\gamma)}$ .
Lemma 4.3: $\|\mathrm{prox}(q_\rho,x,\lambda)-\mathrm{prox}(q,x,\lambda)\|\le2\sqrt{\rho R_{\mathcal Y}(\omega_{\mathcal Y})/(\lambda^{-1}-\gamma)}$ .
Theorem 4.1: with $\eta$ as above, $\|x_K-\mathrm{prox}(q,x_K,\lambda)\|\le\varepsilon\lambda/\beta_{\mathcal X}$ , so $x_K$ is $\varepsilon$ -NS.
Theorem 4.2: termination within $\lceil(q(x_1)-q^*)/((\frac{\gamma\lambda}{1-\gamma\lambda}-4)\eta)\rceil+1$ iterations.

Significance

Corollary 4.1 bounds the number of outer iterations, that is, approximate proximal subproblems, needed to reach an $\varepsilon$ -NS point. The bound is $O(\beta_{\mathcal X}^2(q(x_1)-q^*)/\varepsilon^2)$ for fixed $\gamma\lambda$ , and it holds in any norm. In the paper this count is combined with an accelerated primal-dual solver for each subproblem to obtain the overall gradient complexities (its Corollary 4.2 and Table 1). The paper reports these as the first complexity results for near-stationarity of (1.1) in the non-Hilbertian setting. The outer-loop count is the part of that analysis that does not depend on the inner solver, so it applies to any inner method that meets the $\eta$ -accuracy of Step 2.

The result is proved in the paper. It has no machine-checked proof on Prove2Me or, as far as is known, elsewhere. A formal development would provide reusable infrastructure: strong convexity of Bregman proximal objectives built from weakly convex parts in a general normed space, existence of Bregman proximal points in finite dimension, and the stability of proximal points under uniform perturbation of the objective.

Difficulty

The arithmetic of the final bound is short. The work lies in the analytic facts underneath it, which a Hilbert-space intuition gets wrong. In a general norm $\|\cdot\|^2$ is not smooth and weak convexity cannot be rewritten as convexity of $\Phi+\tfrac\gamma2\|\cdot\|^2$ . Strong convexity of $Q^\lambda$ must therefore come from the gradient inequality and the 1-strong convexity of $\omega_{\mathcal X}$ , passed through a supremum over $\mathcal Y$ . The paper's remark cites only $\lambda^{-1}>\gamma$ and the strong convexity of $\omega_{\mathcal X}$ . The weak convexity of $f$ and the convexity of $r$ are also needed. Existence of the proximal point is not automatic: it requires lower semicontinuity of $f+r$ on the closed set $\mathcal X$ , which comes from compactness of $\mathcal Y$ and joint continuity of $\Phi$ , together with coercivity from strong convexity in finite dimension. Finally, Theorem 4.1 is stated at the termination index, and termination itself (Theorem 4.2) requires $\lambda>0.8\gamma^{-1}$ .

Formalization scope

$\mathbb X,\mathbb Y$ are E, F with NormedAddCommGroup, NormedSpace ℝ and FiniteDimensional ℝ. No inner product is assumed. Gradients are fderiv, dual norms are operator norms on E →L[ℝ] ℝ, and differentiability is assumed at every point of $\mathcal X$ where a gradient is used. Maxima are real suprema over the subtype $\mathcal Y$ . Strong convexity is Mathlib's StrongConvexOn. The proximal point is a predicate IsProx, not a function. Iterates are indexed from 1. A run constrains only the iterations actually executed, those before the first stop. $r$ is real-valued, with values off $\mathcal X$ irrelevant. The optimal value is encoded as any lower bound of $q$ on $\mathcal X$ , and $\eta$ -optimality in Step 2 as a bound against every $x'\in\mathcal X$ . If $R_{\mathcal Y}(\omega_{\mathcal Y})=0$ , Lean sets $\rho=0$ (no smoothing); the paper leaves this case undefined, and all statements remain true. Hypotheses of the paper not used here are omitted, which only strengthens the statements: the Lipschitz bounds (1.2)–(1.3), Assumption 1.3, $\gamma\le L_{xx}$ , essential smoothness and property (i) of the distance generating functions. Lemma 4.3 is stated as (4.12) for $\rho\ge0$ . Theorem 4.1 is stated at a first stopping index, without a termination claim.

Trivializing formalizations are ruled out. The norms are general, not Euclidean. Weak convexity is the gradient inequality (1.4). The suprema are over a nonempty compact $\mathcal Y$ with continuous integrands, so they are finite. Existence of proximal points and termination are conclusions, never hypotheses. $K$ is the first stopping index of a genuine run.

Welcome contributions: the strong convexity of $Q^\lambda$ and $Q^\lambda_\rho$ (milestones 2–3), a general existence lemma for minimizers of strongly convex lower semicontinuous functions on closed convex sets in finite dimension, and the quadratic-growth estimate at a minimizer of a strongly convex function.

Selected references

R. Zhao, A Primal-Dual Smoothing Framework for Max-Structured Non-Convex Optimization, Mathematics of Operations Research, 2024. arXiv:2003.04375v5. https://arxiv.org/abs/2003.04375
D. Davis, D. Drusvyatskiy, Stochastic model-based minimization of weakly convex functions, SIAM J. Optim. 29(1), 2019. https://doi.org/10.1137/18M1178244
K. K. Thekumparampil, P. Jain, P. Netrapalli, S. Oh, Efficient Algorithms for Smooth Minimax Optimization, NeurIPS 2019. https://arxiv.org/abs/1907.01543
Yu. Nesterov, Smooth minimization of non-smooth functions, Math. Program. 103, 2005. https://doi.org/10.1007/s10107-004-0552-5

10 thms1 active userReviewed

Machine Learning Statistics·Captain: mikedeng1

High-Dimensional Learning Under Approximate Sparsity with Applications to Nonsmooth Estimation and Regularized Neural Networks: Excess-Risk Bounds at S3ONC Solutions of MCP-Regularized M-EstimationResearch Paper

Motivation

High-dimensional statistical learning (HDSL) fits a model with $p$ parameters from $n$ samples when $p$ may far exceed $n$ . The standard guarantees for sparse estimators, such as the Lasso, rest on restricted strong convexity (RSC) or restricted eigenvalue conditions on the empirical risk (Negahban et al., 2012; Loh & Wainwright, 2015). These conditions fail or are hard to verify for many losses that matter in operations research and machine learning: nonsmooth losses, losses of neural networks, and M-estimation problems whose population risk is not strongly convex near any sparse vector.

Liu, Ye and Lee (arXiv:1903.00616v2; Operations Research, 2022) remove RSC entirely. They regularize the empirical risk with a folded concave penalty, the minimax concave penalty (MCP) of Zhang (2010), and analyse not a global minimizer (intractable, since the problem is nonconvex) but any point satisfying a weak second-order stationarity condition. They also replace exact sparsity by approximate sparsity: the best sparse vector need only be $\varepsilon_A$ -optimal for the population risk. Their main result, Theorem 1, gives an excess-risk bound whose sample complexity is poly-logarithmic in $p$ .

Setting

Observations $Z_1, \dots, Z_n$ are i.i.d. copies of a random element $Z$ of a measurable space $\mathcal W$ . A loss $L(\beta, z)$ , with parameter $\beta \in \mathbb R^p$ , defines the population risk $\mathbb L(\beta) = \mathbb E[L(\beta, Z)]$ , assumed finite for every $\beta$ and bounded below, the empirical risk $\mathcal L_n(\beta) = \frac1n\sum_i L(\beta, Z_i)$ , and the regularized objective

\mathcal L_{n,\lambda}(\beta) = \mathcal L_n(\beta) + \sum_{j=1}^p P_\lambda(|\beta_j|), \qquad P_\lambda(\theta) = \int_0^\theta \frac{[a\lambda - t]_+}{a}\,dt,

The standing assumptions are:

smoothness (11): each partial derivative $\partial L/\partial\beta_j$ is $U_L$ -Lipschitz along coordinate $j$ , for almost every $z$ ;
Assumption 3: the centred losses $L(\beta, Z_i) - \mathbb E L(\beta, Z_i)$ are sub-exponential with $\psi_1$ -norm at most $\sigma \ge 1$ on the box $\|\beta\|_\infty \le R$ ;
Assumption 4: $L(\cdot, z)$ is $\mathcal C(z)$ -Lipschitz on the box, where $\mathcal C(Z_i)$ is sub-exponential around its mean ( $\psi_1$ -norm at most $\sigma_L \ge 1$ ) and $\mathbb E\,\mathcal C(Z_i) \le \mathcal C_\mu$ , $\mathcal C_\mu \ge 1$ ;
Assumption 1 (A-sparsity): some $\beta^*_{\varepsilon_A}$ with $\|\beta^*_{\varepsilon_A}\|_\infty \le R$ , $R \ge 1$ , and $s = \|\beta^*_{\varepsilon_A}\|_0 > 1$ nonzero entries satisfies $\mathbb L(\beta^*_{\varepsilon_A}) - \inf_\beta \mathbb L(\beta) \le \varepsilon_A$ . Assumption 2 replaces $\inf_\beta \mathbb L$ by any lower bound $L^*_g$ .

A vector $\hat\beta$ satisfies the S³ONC (significant subspace second-order necessary conditions, Definition 1) at a sample if it is a KKT point of $\mathcal L_{n,\lambda}$ , with subgradients $\kappa_j \in \partial|\hat\beta_j|$ , and $U_L + P''_\lambda(|\hat\beta_j|) \ge 0$ whenever $|\hat\beta_j| \in (0, a\lambda)$ . With $\tilde\zeta = \ln(3eR(\sigma_L + \mathcal C_\mu))$ , Theorem 1 fixes $\lambda = \sqrt{8\sigma/(c a n^{2/3})\,[\ln(n^{2/3}p) + \tilde\zeta]}$ , where $c \in (0, 1/2]$ is the constant of the Bernstein inequality (12).

Formalization targets

Goal: Theorem 1 (p. 18)

For $a < \min\{1/U_L, 1\}$ and any random $\hat\beta$ with $\|\hat\beta\|_\infty \le R$ satisfying the S³ONC almost surely:

(i) if $\mathcal L_{n,\lambda}(\hat\beta) \le \mathcal L_{n,\lambda}(\beta^*_{\varepsilon_A}) + \Gamma$ almost surely and $n > C_3[((\Gamma + \varepsilon_A)/\sigma)^3 + s(\ln(np) + \tilde\zeta)]$ , then with probability at least $1 - 2(p+1)e^{-n/C_3} - 6e^{-n^{1/3}/C_3}$ ,

\mathbb L(\hat\beta) - \inf_\beta \mathbb L(\beta) \le C_3\sigma\Big[\frac{s(\ln(np)+\tilde\zeta)}{n^{2/3}} + \sqrt{\frac{s(\ln(np)+\tilde\zeta)}{n}} + \frac{1}{n^{1/3}}\Big] + C_3\sqrt{\frac{\sigma(\Gamma+\varepsilon_A)}{n^{1/3}}} + \Gamma + \varepsilon_A;

(ii) if $\hat\beta$ is no worse in $\mathcal L_{n,\lambda}$ than a Lasso solution $\hat\beta^{\ell_1}$ , the $\Gamma$ -free bound (22) holds under (21).

$C_3, C_4$ are universal constants. The goal fixes the polynomial rate $n^{-1/3}$ ; the general-rate result is Proposition 1.

Milestones (the paper's proof chain)

Proposition 2: the S³ONC forces $|\hat\beta_j| \notin (0, a\lambda)$ almost surely.
Lemma EC.1: the empirical risk is $(2\sigma_L + \mathcal C_\mu)$ -Lipschitz on the box with high probability.
Proposition 3: uniform deviation of $\mathcal L_n$ from $\mathbb L$ over $\{\|\beta\|_\infty \le R, \|\beta\|_0 \le p'\}$ .
Proposition 4: $\|\hat\beta\|_0 \le p'_u - 1$ with high probability.
Lemma EC.2: comparison of the Lasso solution with $\beta^*_{\varepsilon_A}$ in $\mathcal L_{n,\lambda}$ .
Proposition 5: the joint sparsity and excess-risk events for general $\varrho \in (0, 1/2)$ .
Proposition 1: the excess-risk bounds (16), (18) at S³ONC solutions for general $\varrho$ .

Significance

The theorem shows that second-order stationarity, which first- and second-order methods can certify (the paper's Theorem 2 gives a pseudo-polynomial algorithm), suffices for poly-logarithmic sample complexity in $p$ without convexity or RSC. The paper builds on it for nonsmooth losses through smoothing (Theorem 3) and for regularized neural networks (Theorem 4). The same definitions layer (MCP, S³ONC, A-sparsity) serves those results.

The result is proved on paper, in the electronic companion of the cited preprint. Nothing of it is formalized: the platform has no folded concave penalty, no S³ONC and no excess-risk bound for sparse M-estimation without RSC. This mission provides the definitions, the goal and the proof chain as stated by the authors, with two disclosed adjustments (see Formalization scope).

Difficulty

The obvious argument bounds $\mathcal L_n(\hat\beta) - \mathbb L(\hat\beta)$ uniformly over the box $\|\beta\|_\infty \le R$ and then compares $\hat\beta$ with $\beta^*_{\varepsilon_A}$ . It fails: a covering of a $p$ -dimensional box costs a factor $p$ , not $\ln p$ , in the sample size. The usual repair, RSC, which localizes the estimator near a sparse target, is exactly what the paper does without. $\hat\beta$ is moreover only a stationary point of a nonconvex objective, not a minimizer, so no optimality inequality over the whole space is available. The probabilistic part requires keeping the constants consistent across several union bounds and two Bernstein inequalities, with failure probabilities that must stay summable in the sparsity level. In Lean, an additional obstacle is that suprema over uncountable sparse sets are not obviously measurable.

Formalization scope

Data: an abstract measurable space $\mathcal W$ (its embedding in $\mathbb R^q$ plays no role), independent $Z_i$ with common law $\mu$ . $L(\beta, \cdot)$ is measurable and $\mu$ -integrable for every $\beta$ , and $\mathbb L$ is bounded below, so $\inf_\beta \mathbb L(\beta)$ is a genuine infimum.
Norms: the Euclidean norm is written out (Mathlib's norm on Fin p → ℝ is the sup norm). $\|\cdot\|_{\psi_1}$ is the published Orlicz norm HighDimProb.Concentration.subexponentialNorm, always together with an explicit witness of sub-exponentiality. The paper cites the equivalent moment form; the difference is absorbed by the universal constants.
Bernstein constant: (12) and the analogous bound for $\mathcal C(Z_i)$ used in Lemma EC.1 are hypotheses with their constant $c$ , quantified first. Every universal constant ( $C_1$ – $C_4$ , $\tilde c$ ) comes after $c$ and before every problem object: $p$ , $n$ , the distribution, $L$ , $\hat\beta$ , $\Gamma$ . Remark 1 asserts that such a $c \in (0, 1/2]$ exists; the platform's proved bernstein_weighted supplies one.
Derivatives: the gradient enters through coordinate partial derivatives, which is all (11), (13), (14) use. $P'_\lambda, P''_\lambda$ are derivatives of the literal integral (4).
Probabilities: "with probability at least $1-\delta$ " is an upper bound $\delta$ on the outer measure of the failure set.
Random vectors: $\hat\beta$ and $\hat\beta^{\ell_1}$ are arbitrary measurable maps with the stated almost-sure properties; no statement constructs them.
Corrections: $a < 1$ is added to Theorem 1 and Proposition 1. It is Proposition 5's hypothesis, which their printed proofs invoke. Proposition 4's $\zeta_1(\epsilon)$ prints $\sigma_C$ , and $\sigma_L$ is meant. Theorem 1's $\lambda$ is kept as printed ( $\ln(n^{2/3}p)$ ), although Proposition 1 at $\varrho = 1/3$ uses $\ln(n^{1/3}p)$ .

The trivializing formalizations are ruled out explicitly: constants chosen after the instance, junk values of non-integrable expectations, empty infima or undefined derivatives, the sup norm in place of the Euclidean norm, and an estimator chosen by the theorem.

Welcome contributions: proofs of the milestones in order; a Lean proof that Assumption 3 implies (12), via the published Bernstein inequality; a measurable-selection or outer-measure lemma for suprema over sparse boxes, which is reusable across high-dimensional statistics.

Selected references

H. Liu, Y. Ye, H. Y. Lee, High-dimensional learning under approximate sparsity with applications to nonsmooth estimation and regularized neural networks, Operations Research, 2022; preprint arXiv:1903.00616v2, 2021. https://arxiv.org/abs/1903.00616
C.-H. Zhang, Nearly unbiased variable selection under minimax concave penalty, Annals of Statistics 38(2), 2010. https://arxiv.org/abs/1002.4734
J. Fan, R. Li, Variable selection via nonconcave penalized likelihood and its oracle properties, Journal of the American Statistical Association 96, 2001. https://doi.org/10.1198/016214501753382273
S. N. Negahban, P. Ravikumar, M. J. Wainwright, B. Yu, A unified framework for high-dimensional analysis of M-estimators with decomposable regularizers, Statistical Science 27(4), 2012. https://arxiv.org/abs/1010.2731
P.-L. Loh, M. J. Wainwright, Regularized M-estimators with nonconvexity: statistical and algorithmic theory for local optima, Journal of Machine Learning Research 16, 2015. https://arxiv.org/abs/1305.2436
R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, Cambridge University Press, 2012. https://arxiv.org/abs/1011.3027

11 thms1 active userReviewed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Dynamic Resource Allocation in the Cloud with Near-Optimal Efficiency: The Multiplicative Weight Algorithm Nearly Matches the Offline Dynamic Optimum's Work While Approximately Satisfying Every SLAResearch Paper

Motivation

Cloud platforms divide a shared physical resource, such as a pool of processors, among many users at once. Each user is promised a service level agreement (SLA): a fraction $\beta(i)$ of the resource that it should effectively receive whenever it has work to do. The operator wants two things that pull against each other: to keep the resource busy (total work done should be large) and to honour every SLA. The difficulty is informational. The operator does not see future demand, and in the setting of Perez-Salazar, Menache, Singh and Toriello (arXiv:1809.02688) it does not even see current demand: at each step it only learns which users have a non-empty queue.

The paper answers with a multiplicative weight rule. Multiplicative weight methods go back to online learning (Freund and Schapire, 1997; survey: Arora, Hazan and Kale, 2012) and can be read as entropic mirror descent (Beck and Teboulle, 2003). Their classical guarantees compare an online learner with the best fixed decision in hindsight. This paper compares the algorithm with the best time-varying offline allocation instead, and proves the comparison directly, without the standard regret analysis.

Setting

There are $N \ge 2$ users and discrete time steps $t = 1, 2, \dots$ . Each user $i$ has an SLA $\beta(i) \ge 0$ , with $\sum_i \beta(i) \le 1$ . Loads $L_t(i) \ge 0$ arrive online. User $i$ keeps a queue $Q_t(i)$ of unfinished work. At each step:

the decision maker observes the active users $A_t = \{i : Q_t(i) > 0\}$ ;
it chooses an allocation $h_t$ with $h_t(i) \ge 0$ and $\sum_i h_t(i) \le 1$ ;
the load $L_t$ arrives, user $i$ completes $w_t(i) = \min\{h_t(i),\, L_t(i) + Q_t(i)\}$ , and $Q_{t+1}(i) = \max\{0,\, L_t(i) + Q_t(i) - h_t(i)\}$ .

The total work of an allocation sequence $h$ up to time $t$ is $\mathrm{work}_h(t) = \sum_i \sum_{\tau \le t} w_\tau(i)$ .

Algorithm 1 has parameters $0 < \varepsilon \le 1/10$ and $0 < \eta < 1/3$ , and sets $\lambda = \varepsilon^2/(8N)$ . It keeps $h_t$ in the truncated simplex $\Delta_\varepsilon = \{x : \sum_i x(i) = 1,\ x(i) \ge \varepsilon/N\}$ , starting anywhere in $\Delta_\varepsilon$ . At step $t$ it assigns the gain $g_t(i) = 1 + \lambda$ to active users below their SLA ( $A^1_t$ : $h_t(i) < \beta(i)$ ), $g_t(i) = 1$ to the other active users ( $A^2_t$ ) and $g_t(i) = 0$ to inactive users. It then sets $\widehat h_{t+1}(i) = h_t(i)e^{\eta g_t(i)}$ and takes $h_{t+1} = \pi_{\Delta_\varepsilon}(\widehat h_{t+1})$ , the KL projection: the minimizer over $\Delta_\varepsilon$ of $\sum_i x(i)\ln(x(i)/\widehat h_{t+1}(i))$ .

Formalization targets

Goal: Theorem 1 with the explicit constants of p. 10

Let $\beta(i) \ge 2\varepsilon/N$ for all $i$ and let $h$ be any run of Algorithm 1. For every offline allocation sequence $h^*$ and every time $t$ ,

\mathrm{work}_{\mathrm{alg}}(t) \ge (1 - 4\varepsilon)\,\mathrm{work}_{h^*}(t) - 2000\,\frac{N}{\varepsilon^2\eta}\ln\frac{N}{\varepsilon},

and for every user $i$ , every comparator $h'$ with $0 \le h'_t(i) \le \beta(i)$ and every $t$ ,

\sum_{\tau \le t} w_\tau(i) \ge (1 - 2\varepsilon)\sum_{\tau \le t} w'_\tau(i) - \beta(i)\,\tilde p, \qquad \tilde p = \frac{32N^2}{\varepsilon^3\eta}\ln\frac{N}{\varepsilon}.

Intermediate targets (milestones)

Theorem 3: against every sequence of $(1-4\varepsilon)$ -allocations, $\mathrm{work}_{h^*}(t) - \mathrm{work}_{\mathrm{alg}}(t) \le \frac{8N}{\varepsilon^2\eta}\ln\frac{N}{\varepsilon} + 2$ at every $t$ .
Theorem 4: if $\beta(j) > e^{\eta(1+\lambda)}\varepsilon/N$ for all $j$ , each user's work by time $t + \lceil\tilde p\rceil$ is at least what the constant share $(1-2\varepsilon)\beta(i)$ completes by time $t$ .
Lemma 1 and Lemma 2: per-step growth factors $1 + c$ , $1 - \varepsilon c$ and $1 + c'$ of a busy user's allocation, with $c = \varepsilon\eta/(4N)$ and $c' = \varepsilon\eta\lambda/(2N)$ .
Proposition 1(b): the closed form of the KL projection onto $\Delta_\varepsilon$ .
Proposition 2 (weak-duality half), Claims 3.1 and 3.2 (first conclusion): the amortization behind Theorem 3.
The scaling step of p. 10: scaling an allocation by $\kappa \le 1$ keeps at least a $\kappa$ fraction of its work, and work is monotone in the allocation.
Existence and uniqueness of the KL projection, hence of the run from each start.

Significance

The result. Theorem 1 is a bicriteria guarantee against a dynamic benchmark. The work benchmark may change its allocation arbitrarily over time with full knowledge of all loads, and the algorithm, which sees only which queues are non-empty, loses only an additive amount that does not grow with time, at the price of a $4\varepsilon$ fraction of capacity. At the same time every user receives, up to a fixed delay, at least the work of a dedicated $(1-2\varepsilon)$ fraction of its SLA. The paper also shows (arXiv:1809.02688, Theorem 2) that against the unscaled offline optimum every deterministic online algorithm loses $\Omega(\sqrt T)$ work on some load sequence, so some form of slack is unavoidable.

Formalizing it. The result is proved on paper; no machine-checked proof exists. A formalization would check the constant bookkeeping, where the printed text has slips (an $\varepsilon$ versus $\varepsilon/4$ in Theorem 1, a real block length $\tilde s$ used as an integer, an off-by-one in Claim 3.1). It would also produce a reusable deterministic queueing model and a verified closed form of the KL projection onto a truncated simplex.

Difficulty

The obvious first idea, the regret analysis of mirror descent, does not apply. Regret bounds compare with a fixed decision, but here the benchmark changes over time. The algorithm's gains also depend on its own past decisions through the queues, so they are not an exogenous sequence of losses. The paper notes (p. 10) that its guarantees do not follow from the standard analysis of mirror descent. A second obstacle is the feedback: a busy user is not the same as a user that uses its whole allocation. A user whose queue empties during a step completes less than its allocation, so utilization and work done can differ. Finally, the constants matter, because the goal states them explicitly. The printed derivation mixes $\varepsilon$ and $\varepsilon/4$ , uses the real number $\tilde s$ as a block length, and is off by one step when it identifies the work done with the arrived load.

Formalization scope

Model. Everything is real-valued. Time is 0-based: Lean's step $t$ is the paper's step $t + 1$ , the queue at Lean time $t$ is the paper's $Q_{t+1}$ , and $\sum_{\tau=1}^{t}$ is a sum over the first $t$ steps. Queues start empty, a convention the paper uses but does not state. Loads form an infinite sequence; the horizon $T$ is not a parameter and every bound holds at every $t$ .
Runs. The KL projection is a predicate for positive inputs, the domain where the logarithm is defined; Algorithm 1 always projects a positive vector. A run is any sequence satisfying the recursion. The gains are computed from the queues the run itself produces before step $t$ , so $h_{t+1}$ never uses the load of step $t$ or later. A milestone proves that each start in $\Delta_\varepsilon$ has exactly one run, and a sorry-free sanity check exhibits one. Statements about runs are therefore not vacuous.
Benchmarks. "The optimal offline sequence" is replaced by every allocation sequence with $\sum_i h^*_t(i) \le 1$ (or $\le 1 - 4\varepsilon$ ), which is equivalent and avoids a supremum. The SLA comparator ranges over every sequence with $h'_t(i) \le \beta(i)$ , not only the constant one.
Disclosed readings and corrections. Part 1 of the goal uses the $(1 - 4\varepsilon)$ form of p. 10 for the same $\varepsilon$ , not the headline's $(1-\varepsilon)$ . Theorem 3 carries a $+2$ for integer blocks. Claim 3.1 is stated in its corrected 0-based form. Theorem 4 assumes the SLA bound strictly. $0 < \eta < 1/3$ (Algorithm 1's input) is assumed throughout. $\sum_i \beta(i) \le 1$ replaces the $= 1$ used in the proof of Lemma 2.
Ruled out. The goal is stated for every run of the algorithm, with the active sets read from the run's own queues, against every offline sequence. A formalization that fixes a closed-form allocation, decouples the queues from the allocations, or restricts the benchmark to static allocations does not count.
Needed and reusable. The deterministic single-user queue with its work and monotonicity facts, KKT conditions for an entropic objective over a box-constrained simplex, and elementary exponential and logarithm inequalities. The queue model and the projection closed form are reusable beyond this mission. Contributions to any milestone are welcome.

Selected references

S. Perez-Salazar, I. Menache, M. Singh, A. Toriello, Dynamic Resource Allocation in the Cloud with Near-Optimal Efficiency, arXiv:1809.02688v3, 2021 (Operations Research, 2022). https://arxiv.org/abs/1809.02688
Y. Freund, R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, Journal of Computer and System Sciences 55(1), 1997. https://doi.org/10.1006/jcss.1997.1504
S. Arora, E. Hazan, S. Kale, The multiplicative weights update method: a meta-algorithm and applications, Theory of Computing 8, 2012. https://doi.org/10.4086/toc.2012.v008a006
A. Beck, M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3), 2003. https://doi.org/10.1016/S0167-6377(02)00231-6

13 thms1 active userReviewed

Operations Research Probability·Captain: mikedeng1

Stochastic Knapsack Revisited: The Service Level Perspective: Anticipative Policies Need at Most 2Δ More Capacity Than Adaptive Policies to Meet Type-I Service LevelsResearch Paper

Motivation

A central planner holds a single pool of $Q$ units of a product and must supply $N$ customers whose demands $\tilde d_1, \dots, \tilde d_N$ are random. Each customer $i$ asks to be fully served, i.e. to receive her entire demand, with probability at least a target $\alpha_i$ . This Type-I service level (the persistency value of the stochastic knapsack) is the standard requirement in supply-chain allocation and in humanitarian logistics. The planner's question is how much capacity the targets require.

The answer depends on when the planner learns the demands. Lyu, Chou, Teo, Zheng and Zhong (SSRN 3674463, 2021) compare three information regimes:

a responsive policy sees every demand before allocating;
an adaptive policy learns a customer's demand only once it has decided to serve her, and may choose the next customer in light of what it has seen (Dean, Goemans and Vondrák, 2008);
an anticipative policy fixes a priority order before any demand is realized (Alptekinoğlu, Banerjee, Paul and Jain, M&SOM 15(1), 2013).

Anticipative rules are the ones used in practice, because they are simple to announce and to audit. The paper's main result quantifies what they cost in capacity compared with adaptive rules.

Timeline. Alptekinoğlu et al. (2013) introduced capacity pooling with differentiated service probabilities under anticipative priority rules. Dean, Goemans and Vondrák (2008) bounded the adaptivity gap of the stochastic knapsack for revenue maximization by a constant factor. Zhong, Zheng, Chou and Teo (Management Science 64(4), 2018) treated the Type-II (fill-rate) version, in which partial service counts in proportion. They showed that its achievable region is a polymatroid $\Gamma(Q)$ and that anticipative policies are optimal there. Lyu et al. (2021) use this Type-II system to compare the Type-I classes.

Setting

Customers are $i \in \{1, \dots, N\}$ . The demands are random variables on a probability space $(\Omega, \mathcal F, \mathbf P)$ . An allocation run with capacity $Q \ge 0$ serves customers one at a time. A chosen customer is fully served if her demand does not exceed the remaining capacity, and her demand is then deducted. Otherwise she is not fully served, and the run stops.

A deterministic adaptive policy chooses the next customer as a function of the customers chosen so far and their realized demands.
A deterministic anticipative policy is a priority order $\sigma$ , fixed in advance.
A randomized policy in either class is a finite mixture $\sum_k w_k A_k$ of deterministic ones, drawn independently of the demands.

The optimal Type-I capacities are

Q^{\mathrm{Adap}}_I = \inf\{Q \ge 0 : \text{some randomized adaptive policy has } \mathbf P(i \text{ fully served}) \ge \alpha_i\ \forall i\},

and $Q^{\mathrm{Anti}}_I$ is defined in the same way with anticipative policies. These are the optimal values of problem (CPP-A) of the paper.

On the Type-II side, $\Gamma(Q)$ is the set of $\alpha$ with $\sum_{i \in U} \alpha_i \mathbf E[\tilde d_i] \le \mathbf E[\min(Q, \sum_{i\in U} \tilde d_i)]$ for every $U \subseteq \{1,\dots,N\}$ . $Q_{II}$ is the least $Q \ge 0$ with $\alpha \in \Gamma(Q)$ . For a priority order $\sigma$ , the greedy fill $x^*_i(\sigma, \tilde d, Q) = \min\{\tilde d_i, \max(0, Q - \sum_{j \text{ ahead of } i} \tilde d_j)\}$ solves the fractional knapsack (CPP-F).

Standing assumptions (§3.3): the demands are independent and positive, and almost surely $\max_i \tilde d_i \le \Delta$ for a constant $\Delta > 0$ . The targets satisfy $0 \le \alpha_i \le 1$ .

Formalization targets

Goal: Theorem 5

Q^{\mathrm{Anti}}_I - Q^{\mathrm{Adap}}_I \le 2\Delta.

The bound is uniform in $N$ and in the joint law of the demands, subject only to the standing assumptions.

The two halves: Theorems 3 and 4

Q^{\mathrm{Anti}}_I \le Q_{II} + \Delta, \qquad Q^{\mathrm{Adap}}_I \ge Q_{II} - \Delta.

Milestones inside the proofs

Achievability of $\Gamma(Q)$ in fill rate by randomized priority orders (p. 21, from Zhong et al. 2018).
Structure of the greedy fill: it is fractional for at most one customer, and positive exactly when the demand ahead is below $Q$ (p. 17).
$\mathbf E[x^*_i]/\mathbf E[\tilde d_i] \le \mathbf P(x^*_i > 0)$ (p. 17).
Theorem 3.
The rounded adaptive policy $A'$ , which also serves the one customer the run turns away, satisfies $\mathbf E[\sum_{k\in U}\tilde d_k y^{A'}_k] \ge \sum_{k \in U} \mathbf E[\tilde d_k]\alpha_k$ (p. 37).
Adaptive feasibility of $Q$ implies $\alpha \in \Gamma(Q + \Delta)$ (p. 37). The page writes $Q^{\mathrm{Adpt}}_I$ , a misprint for $Q^{\mathrm{Adap}}_I$ .
Theorem 4.

Significance

The result. Theorem 5 says that the information an adaptive planner gains costs at most two maximal demands of capacity, independently of the number of customers. Anticipative priority rules are therefore near-optimal for Type-I service whenever individual demands are small relative to the pool. This contrasts with the responsive regime: Example 1 of the paper shows that $Q^{\mathrm{Adap}}_I$ can exceed $Q^{\mathrm{Resp}}_I$ by an unbounded factor. In Theorems 3–4 the Type-II capacity $Q_{II}$ serves as a common yardstick, so each policy class is compared with an explicitly computable polymatroid quantity.

Formalizing it. The theorem is proved on paper. To our knowledge none of it is machine-checked. A formal development has to make precise what the paper leaves informal: what a randomized adaptive policy is, why the event "customer $i$ is reached" is independent of $\tilde d_i$ , and why the infima defining the optimal capacities are over non-empty sets. The milestones on the greedy fill and the polymatroid $\Gamma(Q)$ can be reused for other fill-rate and persistency problems.

Difficulty

The obvious comparison fails because the two classes face different constraints. A Type-I requirement is an all-or-nothing event, so a deterministic priority order cannot hedge. With three identical unit-demand customers and targets $1/3$ , any fixed order needs $Q = 3$ , while $Q_{II} = 1$ . Randomization over orders is therefore essential on the anticipative side, and the link between a Type-I requirement and the Type-II region $\Gamma(Q)$ is not a statement about any single order. On the adaptive side, the decisions depend on revealed demands. Whether customer $k$ is fully served is correlated with $\tilde d_k$ , so a Type-I service probability does not translate directly into a bound on the expected demand served, which is what $\Gamma(Q)$ constrains. Conditioning arguments that ignore this correlation give false inequalities.

Formalization scope

Demands are a vector d : Fin N → Ω → ℝ on a probability space. Probabilities are μ.real, expectations are Bochner integrals. The standing assumptions are bundled in Standing μ d Δ α: measurable, iIndepFun, almost surely positive, almost surely ≤ Δ, 0 < Δ, and α i ∈ [0, 1].
A run has at most $N$ steps. A demand equal to the remaining capacity is served. Every run, anticipative ones included, stops at the first customer not fully served.
Adaptive policies are functions of the chosen list and the demand vector that depend only on the chosen customers' demands, with measurable decision events. Anticipative policies are permutations, embedded as adaptive policies that ignore the demands.
Randomized policies are finite mixtures. Service levels are probabilities, not the long-run scenario frequencies of p. 11.
$Q^{\mathrm{Adap}}_I$ , $Q^{\mathrm{Anti}}_I$ and $Q_{II}$ are real infima. Under the standing assumptions every feasible set is non-empty ( $Q = N\Delta$ works) and bounded below by $0$ , so no value is a junk default. $Q_{II}$ uses the subset form $\Gamma(Q)$ , which p. 17 shows equals the Type-II problem (CPP-B).
The greedy fill is stated for a priority order $\sigma$ rather than for weights $\theta'$ . It equals $x^*(\theta', \tilde d, Q)$ for every $\theta'$ whose decreasing order, ties broken by index, is $\sigma$ .
Two encodings would trivialize the goal, and both are excluded. Restricting to deterministic priority orders makes Theorem 3 false. Letting adaptive runs skip an oversized customer and continue enlarges the adaptive class beyond the paper's.

The infrastructure the proofs need: measurability of runs, independence of functions of disjoint coordinates, continuity of $Q \mapsto \mathbf E[\min(Q, S)]$ (so that $Q_{II}$ is attained), and the greedy description of a polymatroid's base polytope. Proofs of any milestone are welcome. So are alternative proofs of milestone 1 that avoid the general polymatroid theorem.

Selected references

G. Lyu, M. C. Chou, C.-P. Teo, Z. Zheng, Y. Zhong, Stochastic Knapsack Revisited: The Service Level Perspective, SSRN working paper 3674463, 2021. https://ssrn.com/abstract=3674463
Y. Zhong, Z. Zheng, M. C. Chou, C.-P. Teo, Resource Pooling and Allocation Policies to Deliver Differentiated Service, Management Science 64(4), 1555–1573, 2018.
A. Alptekinoğlu, A. Banerjee, A. Paul, N. Jain, Inventory Pooling to Deliver Differentiated Service, Manufacturing & Service Operations Management 15(1), 33–44, 2013.
B. C. Dean, M. X. Goemans, J. Vondrák, Approximating the Stochastic Knapsack Problem: The Benefit of Adaptivity, Mathematics of Operations Research 33(4), 945–964, 2008. https://doi.org/10.1287/moor.1080.0330

9 thms1 active userReviewed

Machine Learning Operations Research·Captain: mikedeng1

Risk Guarantees for End-to-End Prediction and Optimization Processes: The Excess Squared-Loss Risk Bounds the Squared Excess Optimality-Gap Risk, Scaled by the Squared Diameter of the Feasible SetResearch Paper

Motivation

Many operational decisions are optimization problems whose cost vector is unknown when the decision is made but can be predicted from observed features: shortest paths under predicted travel times, portfolios under predicted returns, production plans under predicted prices. The common practice, predict-then-optimize, first fits a regression model $g$ mapping features $w$ to a cost estimate $g(w)$ and then solves the optimization problem with $g(w)$ in place of the true cost $c$ . What the decision maker cares about is not the prediction error but the optimality gap of the resulting decision under the true cost. Elmachtoub and Grigas (arXiv:1710.08005, Management Science 2022) introduced the SPO+ surrogate to train predictors against that gap directly, and established its Fisher consistency.

Ho-Nguyen and Kılınç-Karzan (arXiv:2012.15046, Management Science 2022) ask which surrogate losses give quantitative guarantees: when does a small excess surrogate risk force a small excess optimality-gap risk, uniformly over a class of data distributions? Their answer adapts the calibration theory of Steinwart (Constructive Approximation 26, 2007) to the end-to-end setting, and its most striking consequence concerns the ordinary squared loss.

Setting

Let $X \subset \mathbb R^m$ be a non-empty convex compact set and $f$ a convex function, continuous on $X$ . For a cost vector $c$ the decision maker solves

\min_{x \in X}\ \{ f(x) + c^\top x \}.

An argmin selection is a fixed map $x^* : \mathbb R^m \to X$ with $x^*(d)$ a minimizer of $f(x) + d^\top x$ over $X$ for every $d$ . Using a prediction $d$ instead of the true cost $c$ incurs the true loss

L(d,c) = f(x^*(d)) + c^\top x^*(d) - \min_{x \in X}\{f(x) + c^\top x\} \ \ge 0 .

Features and costs form a random pair $(w,c) \in W \times \mathbb R^m$ with joint law $\mathbb P$ . For a loss $\ell$ and a measurable predictor $g : W \to \mathbb R^m$ , the risk is $R_\ell(g,\mathbb P) = \mathbb E[\ell(g(w),c)]$ and the Bayes risk is $R_\ell(\mathbb P) = \inf_g R_\ell(g,\mathbb P)$ over measurable $g$ ; for $\ell = L$ these are written $R(g,\mathbb P)$ and $R(\mathbb P)$ . The squared loss is $\ell_{LS}(d,c) = \|d - c\|_2^2$ .

Given a set $C \subset \mathbb R^m$ , the class $\mathcal P$ consists of the laws for which every conditional law $\mathbb P[\cdot \mid w]$ is concentrated on $C$ , is square integrable, and has mean $\mathbb E[c \mid w] \in \mathrm{Conv}(C)$ . Assumption 2 asks that $C$ be bounded. The constants are $B_X = \max_{x,x' \in X}\|x - x'\|_2$ , $B_f = \max_{x,x' \in X}\{f(x) - f(x')\}$ and $B_C = \max_{c \in C}\|c\|_2$ .

A loss $\ell$ is $\mathcal P$ -uniformly calibrated if for every $\epsilon > 0$ there is $\delta > 0$ such that, for every law in $\mathcal P$ , every $w$ and every $d$ , a conditional excess $\ell$ -risk $\mathbb E[\ell(d,c)\mid w] - \inf_{d'}\mathbb E[\ell(d',c)\mid w]$ below $\delta$ forces a conditional excess true risk below $\epsilon$ . The largest such $\delta$ is the calibration function $\delta_\ell(\epsilon;\mathcal P)$ .

Formalization targets

Goal: Corollary 3 (p. 22)

For every law $\mathbb P \in \mathcal P$ with $\mathbb E\|c\|_2^2 < \infty$ and every measurable predictor $g$ ,

\big(R(g,\mathbb P) - R(\mathbb P)\big)^2 \ \le\ B_X^2\,\big(R_{\ell_{LS}}(g,\mathbb P) - R_{\ell_{LS}}(\mathbb P)\big).

Milestones

Lemma 2 (p. 10): $g^*(w) = \mathbb E[c \mid w]$ attains $R(\mathbb P)$ , and $R(\mathbb P) = \mathbb E[\min_{d'}\mathbb E[L(d',c)\mid w]]$ .
Remark 5 (p. 19): the conditional excess true risk equals $f(x^*(d)) - f(x^*(\bar c)) + \bar c^\top(x^*(d) - x^*(\bar c))$ with $\bar c = \mathbb E[c\mid w]$ , and is at most $B_f + B_C B_X$ .
Lemma 3 (p. 20): uniform calibration holds iff $\delta_\ell(\epsilon;\mathcal P) > 0$ for all $\epsilon > 0$ .
Lemma 4 (p. 21): the alternative form (14) of $\delta_\ell$ .
Lemma 5 (p. 21): $\|d - \bar c\|_2 \ge \max\{0, f(x) - f(x') + \bar c^\top(x - x')\}/\|x - x'\|_2$ when $x^*(d) = x \ne x' = x^*(\bar c)$ .
Lemma 6 (p. 22): $\delta_{\ell_{LS}}(\epsilon;\mathcal P)$ is the purely geometric infimum of $\|d - \bar c\|_2^2$ .
Theorem 4 (p. 22): $\ell_{LS}$ is $\mathcal P$ -uniformly calibrated, with $\delta_{\ell_{LS}}(\epsilon;\mathcal P) \ge \epsilon^2/B_X^2 > 0$ .
Theorem 3 (p. 20): for any uniformly calibrated $\ell$ , $\delta^{**}_\ell(R(g,\mathbb P) - R(\mathbb P)) \le R_\ell(g,\mathbb P) - R_\ell(\mathbb P)$ , with $\delta^{**}_\ell$ the convex minorant of $\delta_\ell$ on $(0, B_f + B_C B_X]$ .

The goal is stated with the constant $B_X^2$ and no other problem data: it is independent of $f$ , of $C$ beyond boundedness, and of the law of the data.

Significance

The corollary says that a predictor trained by ordinary least squares, without any information about $f$ or $X$ , has excess optimality-gap risk at most $B_X\sqrt{R_{\ell_{LS}}(g,\mathbb P) - R_{\ell_{LS}}(\mathbb P)}$ . Since the excess squared-loss risk separates over coordinates, coordinate-wise regression bounds suffice for end-to-end guarantees (Remark 7). Any learning-theoretic rate for least-squares regression therefore transfers to a rate for the decision problem, up to a square root. Theorem 3 gives the same transfer for any uniformly calibrated surrogate, and is the template for the paper's further results on separable symmetric losses.

The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires a measure-theoretic treatment of conditional risks through kernels, a Lean version of Steinwart's convexified calibration inequality in this setting, and the geometric bound of Lemma 5. Each milestone is a self-contained target.

Difficulty

The true loss $L(d,c)$ is neither convex nor continuous in $d$ (Lemma 1): the decision $x^*(d)$ jumps between faces of $X$ . A pointwise comparison between $\|d - c\|_2^2$ and $L(d,c)$ fails, since a prediction close to $c$ can still select a far-away vertex when $c$ lies near a tie. The comparison only holds after conditioning on $w$ and averaging over $c$ , and it must hold uniformly over all conditional laws in $\mathcal P$ , not for a fixed distribution. The step from conditional comparisons to the integrated risks is where the uniform bound $B_f + B_C B_X$ on the conditional excess true risk and the convention at $\epsilon = 0$ in $\delta^{**}$ matter; Bayes risks are infima over predictors, so this step also needs the conditional minimizers to assemble into a measurable predictor.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin m). The standing setting (Standing X f) bundles convexity, compactness and non-emptiness of $X$ , convexity of $f$ on $X$ and continuity of $f$ on $X$ ; IsArgminSelection X f xstar is the selection property. A joint law is μ ⊗ₘ κ, with μ the law of $w$ and κ a Markov kernel giving $\mathbb P[\cdot \mid w]$ ; $\mathbb E[c \mid w]$ is the Bochner integral against κ w. Risks are $[0,\infty]$ -valued lower integrals of ENNReal.ofReal of the non-negative losses, Bayes risks are infima over measurable predictors, and excess risks are truncated differences. The class $\mathcal P$ is lsClass C, a set of conditional laws concentrated on $C`; the calibration function `deltaL` and `UniformlyCalibrated` range over such a set, which matches the page's "for all$ \mathbb P \in \mathcal P $,$ w \in W $" whenever$ W $is non-empty.$ B_X$ is Metric.diam X.

Added or pinned conventions:

measurability of xstar (the paper uses Lebesgue measurability, Lemma EC.4) and of predictors;
$\mathbb E\|c\|_2^2 < \infty$ in the goal, explicit though implied by support on bounded $C$ , to make the extended-real Bayes-risk subtraction finite;
$1/B_X^2$ multiplied out in the goal; Theorem 4 carries $B_X>0$ for its printed quotient;
the conclusion of (12) read conditionally on $w$ ;
$\delta^{**}$ constrained by $h'(0) \le 0$ (the convention $\delta_\ell(0) = 0$ of p. 19);
in Theorem 3, the identity $R_\ell(\mathbb P) = \mathbb E[\inf_{d'}\mathbb E[\ell(d',c)\mid w]]$ and finiteness of $R_\ell(\mathbb P)$ .

The Bayes risks are genuine infima over measurable predictors and the conditional excess risks are defined generically. Neither is defined by the closed form that Lemma 2 or Lemma 6 establishes, so neither lemma holds by definition.

Needed infrastructure: lower integrals against μ ⊗ₘ κ and their disintegration, measurability of the conditional mean and of the optimal value $c \mapsto \min_x\{f(x) + c^\top x\}$ , Jensen's inequality for real convex functions on a bounded interval, and the distance from a point to a half-space. The bias–variance decomposition for laws on $\mathbb R^m$ and the half-space distance formula are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for the goal that bypass Theorem 3.

Selected references

N. Ho-Nguyen and F. Kılınç-Karzan, Risk guarantees for end-to-end prediction and optimization processes, Management Science 68(12), 2022. arXiv:2012.15046v1. https://arxiv.org/abs/2012.15046
A. N. Elmachtoub and P. Grigas, Smart "predict, then optimize", Management Science 68(1), 2022. https://arxiv.org/abs/1710.08005
I. Steinwart, How to compare different loss functions and their risks, Constructive Approximation 26, 2007. https://doi.org/10.1007/s00365-006-0662-3

10 thms1 active userReviewed

Algebraic Geometry Convex Optimization Operations Research·Captain: mikedeng1

On Computing the Nonlinearity Interval in Parametric Semidefinite Optimization: The Set of Transition Points of the Optimal Partition Is FiniteResearch Paper

Motivation

Sensitivity analysis asks how the solution of an optimization problem changes when its data move. For linear optimization the answer has been known since the 1990s: as the objective is perturbed along a fixed direction, the optimal partition (which variables can be positive at an optimum and which slacks can) stays constant on open intervals and changes only at finitely many breakpoints, and the optimal value is piecewise linear with breakpoints exactly there (Adler and Monteiro, Algorithmica 8, 1992; Jansen, Roos and Terlaky, 1993). Semidefinite optimization (SDO) is used throughout control, combinatorial relaxations and polynomial optimization, and its parametric behaviour is less regular. The optimal partition can stay constant while the optimal sets move (a nonlinearity interval), and the optimal value need not be piecewise linear.

Mohammad-Nezhad and Terlaky (Optimization 69, 2020) defined invariancy intervals, nonlinearity intervals and transition points for parametric SDO. Hauenstein, Mohammad-Nezhad, Tang and Terlaky (arXiv:1908.10499v3; Mathematics of Operations Research, 2022) prove that there are only finitely many transition points (Theorem 1, p. 8) and then compute nonlinearity intervals with numerical algebraic geometry. Finiteness is what makes a computational description possible: without it, the interior of the domain need not decompose into finitely many intervals of each kind.

Timeline:

1992–1993: Adler and Monteiro, and Jansen, Roos and Terlaky, start the optimal partition approach to parametric linear optimization.
1999: Goldfarb and Scheinberg extend the optimal partition approach to parametric SDO (Applied Numerical Mathematics 29).
2020: Mohammad-Nezhad and Terlaky introduce the optimal partition approach to parametric SDO (Definitions 3–5 of the present paper are taken from there).
2019–2022: Hauenstein, Mohammad-Nezhad, Tang and Terlaky prove that the transition points are finite (Theorem 1) and give the nonlinearity-interval algorithm.

Setting

Let $\mathbb S^n$ be the real symmetric $n\times n$ matrices with $\langle M,X\rangle=\operatorname{tr}(MX)$ . Data: $A^1,\dots,A^m,C,\bar C\in\mathbb S^n$ and $b\in\mathbb R^m$ . For a real parameter $\epsilon$ consider

(\mathrm P_\epsilon)\ \inf_X\{\langle C+\epsilon\bar C,X\rangle:\ \langle A^i,X\rangle=b_i,\ X\succeq0\},\qquad (\mathrm D_\epsilon)\ \sup_{(y,S)}\Big\{b^Ty:\ \textstyle\sum_i y_iA^i+S=C+\epsilon\bar C,\ S\succeq0\Big\}.

The primal feasible set $\mathcal P$ does not depend on $\epsilon$ ; the dual one is $\mathcal D(\epsilon)$ . The optimal value function $v(\epsilon)\in\mathbb R\cup\{\pm\infty\}$ is the infimum of $(\mathrm P_\epsilon)$ , its domain is $\mathcal E=\{\epsilon:\ v(\epsilon)>-\infty\}$ , and the optimal sets are $\mathcal P^*(\epsilon)=\{X\in\mathcal P:\langle C+\epsilon\bar C,X\rangle=v(\epsilon)\}$ and $\mathcal D^*(\epsilon)=\{(y,S)\in\mathcal D(\epsilon):b^Ty=v(\epsilon)\}$ .

Standing assumptions (p. 2): Assumption 1, the $A^i$ are linearly independent; Assumption 2, there are $X^\circ\in\mathcal P$ , $(y^\circ,S^\circ)\in\mathcal D(0)$ with $X^\circ,S^\circ\succ0$ .

For $\epsilon\in\operatorname{int}(\mathcal E)$ , a maximally complementary optimal solution $(X^*(\epsilon),y^*(\epsilon),S^*(\epsilon))$ has $X^*(\epsilon)\in\operatorname{ri}\mathcal P^*(\epsilon)$ and $(y^*(\epsilon),S^*(\epsilon))\in\operatorname{ri}\mathcal D^*(\epsilon)$ (Definition 1). A point $\bar\epsilon\in\operatorname{int}(\mathcal E)$ is a transition point if every interval $(\bar\epsilon-\delta,\bar\epsilon+\delta)\cap\operatorname{int}(\mathcal E)$ contains an $\epsilon$ with $\operatorname{rank}X^*(\epsilon)\ne\operatorname{rank}X^*(\bar\epsilon)$ or $\operatorname{rank}S^*(\epsilon)\ne\operatorname{rank}S^*(\bar\epsilon)$ (Definition 5).

Formalization targets

Goal: Theorem 1 (p. 8)

\{\bar\epsilon\in\mathbb R:\ \bar\epsilon\ \text{is a transition point}\}\ \text{is finite.}

The statement names no bound on the number of transition points; it asserts finiteness only.

Milestones, in the order of the paper's argument

Remark 1 (p. 2): strictly feasible primal and dual solutions exist at every $\epsilon\in\operatorname{int}(\mathcal E)$ .
p. 2: $\mathcal E$ is an interval with at least two points; $v$ is finite and concave on $\mathcal E$ and continuous on $\operatorname{int}(\mathcal E)$ .
p. 2: for $\epsilon\in\operatorname{int}(\mathcal E)$ , $\mathcal P^*(\epsilon)$ and $\mathcal D^*(\epsilon)$ are nonempty and compact (strong duality).
(1), p. 2: on $\operatorname{int}(\mathcal E)$ , a primal–dual triple is optimal iff it is feasible and $XS=0$ .
Appendix, p. 22: the ranks at relative-interior optimal points are maximal on the optimal sets.
(19), p. 22: $\operatorname{int}(\mathcal E)=\bigcup_{\theta+\sigma\le n}\mathcal S_{(\theta,\sigma)}$ , where $\mathcal S_{(\theta,\sigma)}$ is the set of $\epsilon\in\operatorname{int}(\mathcal E)$ at which some $(X,y,S)\in\operatorname{ri}(\mathcal P^*(\epsilon)\times\mathcal D^*(\epsilon))$ has ranks $(\theta,\sigma)$ .
p. 22: $\bar\epsilon$ is a transition point iff $\bar\epsilon\in\operatorname{bd}(\mathcal S_{(\theta,\sigma)})\cap\operatorname{int}(\mathcal E)$ for some $\theta+\sigma\le n$ .
p. 23: every $\mathcal S_{(\theta,\sigma)}$ is a semi-algebraic subset of $\mathbb R$ .
[Basu–Pollack–Roy, Theorem 5.22], cited p. 22: a semi-algebraic subset of $\mathbb R$ has finitely many boundary points.

Significance

The result. Theorem 1 implies that $\operatorname{int}(\mathcal E)$ is a finite union of invariancy intervals, nonlinearity intervals and transition points (p. 8). This is the structural fact behind the paper's algorithm, which follows the optimal solution along a nonlinearity interval and detects its end points, and it extends to SDO the finite-breakpoint picture of parametric linear optimization. Without finiteness, a sensitivity report would have no finite description.

Formalizing it. The theorem is proved in the paper; nothing here is open. It has no machine-checked proof that we know of. A complete development would bring parametric conic duality into Lean (the interior point condition moving along a direction, strong duality with attainment, compactness of optimal sets), and it would connect convex analysis to semi-algebraic geometry: relative interiors, ranks of positive semidefinite matrices, and the one-dimensional case of Tarski–Seidenberg. Each of these is useful beyond this paper.

Difficulty

The obvious argument says that ranks are integers between $0$ and $n$ , so they can change only finitely often. That is false for arbitrary integer-valued functions on an interval: a rank pair could alternate on a sequence accumulating at a point, producing infinitely many transition points. Finiteness needs a structural reason why each level set $\mathcal S_{(\theta,\sigma)}$ is a finite union of points and intervals. That reason is semi-algebraicity. Proving it requires showing that the relative interior of the optimal set, and the parameter values where a rank is attained there, can be described by a first-order formula over the reals, and then eliminating the quantifiers. Mathlib has no Tarski–Seidenberg theorem, and the one-variable structure theorem for semi-algebraic sets (milestone 9) is itself missing.

A second difficulty is the parametric duality: strict feasibility is assumed only at $\epsilon=0$ , and propagating it to all of $\operatorname{int}(\mathcal E)$ (Remark 1) uses a theorem of the alternative for SDO.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; $X\succeq0$ is PosSemidef (which includes symmetry) and $X\succ0$ is PosDef. Symmetry of $A^i$ , $C$ , $\bar C$ is a hypothesis of every theorem, as are Assumptions 1–2. The optimal value $v$ is an EReal infimum over $\mathcal P$ , so $v=-\infty$ is represented faithfully and $\mathcal E$ is not a junk set. $\mathcal D^*(\epsilon)$ compares $b^Ty$ with the primal value $v(\epsilon)$ , as printed. The relative interior is Mathlib's intrinsicInterior. Definition 1 lets $X^*(\epsilon)$ be any maximally complementary solution. The formalization removes this choice by taking the supremum of ranks over relative-interior points, and milestone 5 shows that every such point has that rank. $\mathcal S_{(\theta,\sigma)}$ uses the relative interior of the product, as printed. A subset of $\mathbb R$ is semi-algebraic when its copy in $\mathbb R^1$ is a finite union of sets $\{p=0,\ g<0\}$ with real polynomials.

Trivializing formalizations are excluded:

ranks are taken at relative-interior points only, never at arbitrary optimal points;
$v$ is an extended-real infimum, never a real sInf (which would make an unbounded problem look finite with value $0$ );
transition points are defined by Definition 5 itself, not as boundary points of $\mathcal S_{(\theta,\sigma)}$ .

The paper also states that $\mathcal E$ is closed. Under Assumptions 1–2 this is false: $n=2$ , $m=1$ , $A^1=\operatorname{diag}(1,0)$ , $b=1$ , $C=\begin{pmatrix}0&1\\1&1\end{pmatrix}$ , $\bar C=\operatorname{diag}(0,1)$ gives $\mathcal E=(-1,\infty)$ . Milestone 2 omits closedness. The paper's proof of Theorem 1 does not use it.

Contributions welcome: proofs of any milestone; a semi-algebraic toolkit in Lean (closure under Boolean operations, projections from $\mathbb R^{N+1}$ to $\mathbb R$ , the one-dimensional structure theorem); conic duality for standard-form SDO.

Selected references

J. D. Hauenstein, A. Mohammad-Nezhad, T. Tang, T. Terlaky, On computing the nonlinearity interval in parametric semidefinite optimization, Mathematics of Operations Research, 2022. arXiv:1908.10499v3
A. Mohammad-Nezhad, T. Terlaky, Parametric analysis of semidefinite optimization, Optimization 69 (2020), 187–216.
I. Adler, R. D. C. Monteiro, A geometric view of parametric linear programming, Algorithmica 8 (1992), 161–176.
D. Goldfarb, K. Scheinberg, On parametric semidefinite programming, Applied Numerical Mathematics 29 (1999), 361–377.
S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, Springer, 2006.
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.

11 thms1 active userReviewed

Operations Research·Captain: mikedeng1

Optimal Use and Replenishment of Two Substitutable Raw Materials in a Stochastic Capacitated Make-to-Order Production System: A Use-Down-To/Balancing Production Policy Is OptimalResearch Paper

Motivation

Make-to-order manufacturers may use two substitutable raw materials to satisfy demand when production capacity and material deliveries are uncertain. A cheaper material may yield less finished product per unit, and the firm must decide how much of each material to preserve for later periods. A production rule based only on current unit costs can be wrong because using one material changes the inventory state from which future orders and production will be chosen. Chen, Duenyas, and Jasin study this coupled replenishment and production problem and characterize the form of an optimal production decision. Their result gives a state-dependent rule described by four curves, rather than requiring a separate optimization for every inventory state. This mission formalizes that production result from the 2016 working-paper version of their study.

Setting

There are $T\ge1$ periods and two substitutable materials. A unit of finished product requires $a^j>0$ units of type- $j$ material, with $a^1<a^2$ . Before production in period $t$ , the available material is a vector $y_t=(y_t^1,y_t^2)\in\mathbb R_+^2$ . Demand $D_t$ and production capacity $R_t$ are nonnegative random quantities with finite support. A unit of satisfied demand earns revenue $e_t$ ; a unit of lost demand incurs penalty $\sigma_t>0$ . Holding costs are $h_t^j$ and material purchasing costs are $c_t^j$ . Ordered amounts are limited by random availabilities $q_t^j$ , whose finite supports may include $+\infty$ .

The production decision is the remaining inventory $w_t$ after material use. The feasible set $E_2(y_t,D_t,R_t)$ contains vectors satisfying $0\le w_t\le y_t$ , the demand limit, and the capacity limit:

a^1w_t^1+a^2w_t^2\ge a^1y_t^1+a^2y_t^2-D_t,\qquad w_t^1+w_t^2\ge y_t^1+y_t^2-R_t.

The objective $J_t(w_t)$ adds the current cost coefficients $(a^jp_t+h_t^j-c_{t+1}^j)w_t^j$ , where $p_t=e_t+\sigma_t$ , to the next-period value $V_{t+1}(w_t)$ . The value functions are determined backward from $V_{T+1}(x)=c_{T+1}^1x^1+c_{T+1}^2x^2$ by the production and replenishment equations (1)–(5). Thus $J_t$ is an object computed from the model data and the dynamic program. These definitions follow §3 of the working paper.

Formalization targets

Optimal production rule

The goal is Theorem 1, pp. 15–16. There are two nonincreasing switching curves $\gamma_t^1,\gamma_t^2$ and two balancing curves $\alpha_t,\beta_t$ meeting at $\bar w_t$ . Together they define the use-down-to and balancing (UB) rule of Definition 1. For every nonnegative $D,R$ and every $y\in\mathbb R_+^2$ , the prescribed decision is feasible and optimal:

w_t^*(y,D,R)\in\operatorname*{arg\,min}_{w\in E_2(y,D,R)}J_t(w).

The goal also includes the theorem's four minimization characterizations: $\bar w_t$ minimizes $J_t$ on the whole nonnegative orthant; each $\gamma_t^j$ minimizes a one-coordinate section; $\alpha_t(x)$ minimizes on $a^1w^1+a^2w^2=x$ ; and $\beta_t(x)$ minimizes on $w^1+w^2=x$ , for every $x\ge0$ . The milestones retain Lemma 3(a), Lemma 3(d), the backward-induction claim for $H_t$ , Proposition 1 for the strictly convex perturbation, and Proposition 2 for the limiting policy.

Significance

The theorem identifies which material-use rule solves the production stage for any observed demand, capacity, and inventory. Its curves are independent of that period's realized $D$ and $R$ ; those realizations enter the region boundaries and the rule's arguments. This structure supports the paper's later ordering-policy and computational work without replacing the original dynamic program with an unrelated one. The same formal definitions of feasible production, finite-support expectations, and coordinatewise value-function structure can be reused in other two-resource inventory models.

The working paper proves the result mathematically; the requested machine-checked work is to prove the Lean statements. The present proposal supplies definitions and theorem targets with sorry proof bodies. It does not claim that Theorem 1 or its milestones already have Lean proofs. A completed development would connect the backward dynamic program to the curve characterization and then prove that the region-specific action is optimal.

Difficulty

The replenishment-stage objective $G_t$ is generally neither convex nor supermodular even when the subsequent value function has those properties, as the paper notes after Lemma 3. Consequently, taking a minimum in the replenishment recursion does not preserve the desired shape by an immediate standard argument. At the production stage, demand and capacity impose different coupled linear constraints on the two materials. Minimizing each material coordinate separately therefore does not produce a feasible or optimal decision in general. The source's region boundaries must account for which of these constraints binds and for their changes at $D=a^1R$ and $D=a^2R$ .

Formalization scope

Lean uses $\mathbb R\times\mathbb R$ with componentwise order for two-material vectors. Each random quantity is a finite support with nonnegative real weights summing to one; expectations are finite sums. The two availability laws are multiplied as independent laws at each period, and $+\infty$ availability is represented by WithTop ℝ. The joint law of $(D_t,R_t)$ need not factor. The dynamic program has periods $1,\ldots,T$ , and the terminal value is set at $T+1$ . Its minima are defined as infima of feasible objective images; attainment is content of the results, not part of the definitions. Lower-growth claims use eventual real inequalities for every positive error, with the other inventory coordinate fixed and nonnegative.

The paper describes revenues and costs as monetary amounts and uses sign conditions in its proof of Lemma 3. The Lean standing predicate makes explicit $e_t,h_t^j,c_t^j\ge0$ , $c_t^j+h_t^j>0$ , $a^j>0$ , and $T>0$ , in addition to the paper's $\sigma_t>0$ and $a^1<a^2$ . These assumptions are disclosed because without them the stated coercivity and attainment claims may fail. The objective in the goal is precisely $J_t$ produced by the full backward recursion; allowing an arbitrary objective with assumed structural properties would omit the dynamic-programming content.

Definition 1 calls its six regions a partition. At $D\le a^1R$ , two printed regions can overlap; a concrete Lean check is included locally. The formal policy follows the page's displayed order when more than one region matches. Region coverage is asserted for all nonnegative $D,R$ , and pairwise disjointness is asserted only when $a^1R<D$ . The first-match convention and corrected partition claim are documented with the counterexample for review. The piecewise formulas for $K^j$ , $L^j$ , and $\bar\gamma^j$ retain their source inequalities. Contributions establishing feasibility, curve existence, uniqueness for the perturbed problem, and the induction step are all useful to the mission.

Selected references

Q. Chen, I. Duenyas, and S. Jasin, Optimal Use and Replenishment of Two Substitutable Raw Materials in a Nonstationary Capacitated Make-to-Order Production System, SSRN working paper 2801786, version of 2016-06-28. SSRN.

10 thms1 active userReviewed

Convex Optimization Probability·Captain: mikedeng1

Proximal Gradient Methods with Adaptive Subspace Sampling: Random Subspace Proximal Gradient Descent Converges Linearly in ExpectationResearch Paper

Motivation

Large-scale composite problems $\min_x f(x)+g(x)$ , with a smooth loss $f$ and a nonsmooth regularizer or constraint $g$ , are routinely solved by proximal gradient methods. When the dimension is large, computing the full gradient at every step is expensive, and randomized coordinate descent updates only a few coordinates at a time. Classical proximal coordinate descent, however, requires $g$ to be separable along the coordinates, which excludes total-variation penalties, group norms with overlapping groups, and most constraint sets.

Grishchenko, Iutzeler and Malick (arXiv:2004.13356, Mathematics of Operations Research, 2021) propose a randomized proximal subspace descent (RPSD): the gradient step is taken only along a randomly drawn subspace, while the proximal step is applied to the full vector, so $g$ need not be separable. Their motivation is twofold: random subspaces include coordinate blocks as well as sketching-type projections, and the subspace distribution can later be adapted to the structure that the proximal operator identifies (§3 of the paper, not part of this mission). This mission formalizes the convergence theory of the non-adaptive method, which the adaptive variants build on.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|_2$ . The problem is

\min_{x\in\mathbb R^n} f(x)+g(x), \tag{1}

where $f$ is $L$ -smooth (differentiable with $L$ -Lipschitz gradient) and $\mu$ -strongly convex, and $g:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ is convex, proper and lower semicontinuous (Assumption 1). Problem (1) then has a unique minimizer $x^\star$ . The proximity operator of $g$ with step $\gamma>0$ is

\mathbf{prox}_{\gamma g}(v)=\operatorname*{argmin}_{y\in\mathbb R^n}\Big\{g(y)+\frac1{2\gamma}\|y-v\|_2^2\Big\}.

A selection $\mathfrak S$ is a random linear subspace of $\mathbb R^n$ ; $P_F$ denotes the orthogonal projection onto a subspace $F$ . A selection is admissible if $\mathbb P[x\in\mathfrak S^\perp]<1$ for every nonzero $x$ : no nonzero direction is almost surely missed. The average projection is the matrix

\mathsf P=\mathbb E[P_{\mathfrak S}],

and $\lambda_{\min}(\mathsf P)$ , $\lambda_{\max}(\mathsf P)$ are its extreme eigenvalues. The $\mathsf P$ -norm is $\|v\|_{\mathsf P}^2=\langle v,\mathsf Pv\rangle$ , and $\mathsf Q=\mathsf P^{-1/2}$ .

Given i.i.d. admissible selections $\mathfrak S^1,\mathfrak S^2,\dots$ (Assumption 2), a step size $\gamma$ and a starting point $z^0$ , RPSD (Algorithm 1) sets $x^1=\mathbf{prox}_{\gamma g}(\mathsf Q^{-1}z^0)$ and, for $k\ge1$ ,

y^k=\mathsf Q\big(x^k-\gamma\nabla f(x^k)\big),\qquad z^k=P_{\mathfrak S^k}y^k+(I-P_{\mathfrak S^k})z^{k-1},\qquad x^{k+1}=\mathbf{prox}_{\gamma g}\big(\mathsf Q^{-1}z^k\big).

The auxiliary sequence $z^k$ is updated only inside the random subspace $\mathfrak S^k$ . Its fixed point is $z^\star=y^\star=\mathsf Q(x^\star-\gamma\nabla f(x^\star))$ .

Formalization targets

Goal: Theorem 1 (p. 5)

For every $\gamma\in(0,2/(\mu+L)]$ , the iterates converge almost surely to $x^\star$ , with

\mathbb E\big[\|x^{k+1}-x^\star\|_2^2\big]\le\Big(1-\lambda_{\min}(\mathsf P)\frac{2\gamma\mu L}{\mu+L}\Big)^k C,\qquad C=\lambda_{\max}(\mathsf P)\,\|z^0-\mathsf Q(x^\star-\gamma\nabla f(x^\star))\|_2^2 .

Both clauses are part of the goal: the rate for every $k\ge0$ , and almost-sure convergence.

Milestones

Lemma 1 (p. 3): for an admissible selection, $\mathsf P$ is positive definite, with $\lambda_{\min}(\mathsf P)>0$ and $\lambda_{\max}(\mathsf P)\le1$ .
Lemma 2 (p. 5): with $\mathcal F^k=\sigma(\mathfrak S^1,\dots,\mathfrak S^k)$ ,

\mathbb E\big[\|z^k-z^\star\|_2^2\mid\mathcal F^{k-1}\big]=\|z^{k-1}-z^\star\|_2^2+\|y^k-y^\star\|_{\mathsf P}^2-\|z^{k-1}-z^\star\|_{\mathsf P}^2 .

Lemma 3 (p. 6), for $\gamma\in(0,2/(\mu+L)]$ :

\|y^k-y^\star\|_{\mathsf P}^2-\|z^{k-1}-z^\star\|_{\mathsf P}^2\le-\lambda_{\min}(\mathsf P)\frac{2\gamma\mu L}{\mu+L}\|z^{k-1}-z^\star\|_2^2 .

Display (a) of the proof of Theorem 1 (p. 6): $\mathbb E\|z^k-z^\star\|_2^2\le\big(1-\lambda_{\min}(\mathsf P)\tfrac{2\gamma\mu L}{\mu+L}\big)^k\|z^0-z^\star\|_2^2$ .
Display (b) of the proof of Theorem 1 (p. 6): $\|x^{k+1}-x^\star\|_2^2\le\|z^k-z^\star\|_{\mathsf P}^2\le\lambda_{\max}(\mathsf P)\|z^k-z^\star\|_2^2$ .

Significance

The theorem shows that a proximal gradient method can be randomized along arbitrary subspaces without any separability of the nonsmooth term, at the price of the change of basis $\mathsf Q$ , and that it keeps the usual step-size range of deterministic proximal gradient descent. The rate depends on the sampling only through $\lambda_{\min}(\mathsf P)$ ; for coordinate sampling with probabilities $p_i$ this is $\min_i p_i$ , which recovers the familiar dependence of coordinate methods. The same two lemmas are the template for the adaptive method ARPSD of §3, whose analysis states that Lemmas 2–3 "can be directly extended".

On the formal side, the result is proved on paper but, as far as the platform's index shows, no random-subspace or coordinate-type proximal method with a non-separable regularizer has a machine-checked convergence proof. A complete development would produce reusable pieces: the average projection of a random subspace and its spectrum, the conditional-expectation identity for a random projection update, and a pathwise-to-almost-sure convergence argument for linearly convergent mean-square errors.

Difficulty

Each step is short on paper, and the difficulty lies in what the paper takes for granted. The conditional expectation in Lemma 2 requires the iterates $z^{k-1}$ and $y^k$ to be measurable with respect to the past selections, which in turn rests on the proximity operator being single-valued and measurable, and on the integrability of every quantity being conditioned. The deterministic contraction of Lemma 3 uses two external results, the co-coercivity estimate for strongly convex smooth functions and the nonexpansiveness of the proximity operator, neither of which is stated inside the paper. Lemma 1 needs the spectral theory of a Bochner integral of projections. The step from a summable mean-square error to almost-sure convergence needs the monotone convergence theorem and a Borel–Cantelli-type argument. None of these is deep, but together they account for most of the work.

A frequent first idea is to analyse $x^k$ directly as a randomized proximal gradient iterate; this fails because $x^k$ is not a contraction in any fixed norm along a single random subspace, which is why the paper tracks the auxiliary sequence $z^k$ .

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), matrices are continuous linear maps, $P_F$ is Mathlib's Submodule.starProjection, and inner products are inner ℝ.
A selection is a random subspace: $\mathfrak S^{k+1}=\mathrm{sel}(\xi_k)$ , where $(\xi_k)_{k\ge0}$ are i.i.d. random variables in a measurable space $\Theta$ (so Lean's index $k$ is the paper's $k+1$ ). Definition 2's construction from a covering family is subsumed, since every subspace is a sum of members of the covering family of all subspaces. The map $\theta\mapsto P_{\mathrm{sel}(\theta)}x$ is assumed measurable.
$\mathsf P$ is characterized pointwise by $\mathsf Px=\int P_{\mathfrak S^1(\omega)}x\,d\mathbb P(\omega)$ ; with the measurability hypothesis this is the true expectation, never a junk zero integral.
$\mathsf Q=\mathsf P^{-1/2}$ is encoded as a positive map with $\mathsf Q\mathsf P\mathsf Q=I$ and a two-sided inverse $\mathsf Q^{-1}$ , which determines it uniquely as the positive square root of $\mathsf P^{-1}$ .
$\lambda_{\min}$ and $\lambda_{\max}$ are the Rayleigh infimum and supremum over the unit sphere. Lemma 1 adds $n\ge1$ , because $\mathbb R^0$ has no eigenvalues.
$g$ is the pair $(\operatorname{dom}g,g)$ : proper is a nonempty domain, lower semicontinuity is a closed epigraph. The prox is the published BoydADMM.Prox.IsProx with weight $1/\gamma$ . $f$ is differentiable, StrongConvexOn with modulus $\mu$ , with $L$ -Lipschitz gradient; $\mu>0$ and $L>0$ are explicit.
Added hypothesis: Lemma 3 assumes $\gamma\in(0,2/(\mu+L)]$ , which its proof uses and without which it is false. Lemma 2 and display (b) do not need the upper bound and do not assume it.
The minimizer $x^\star$ and the RPSD run are universally quantified; expectations are Bochner integrals.

The goal cannot be trivialized: $\mathsf P$ is the true average projection, $\mathsf Q$ is the positive square root of $\mathsf P^{-1}$ , admissibility, independence and identical distribution are all kept, the step-size range is exactly $(0,2/(\mu+L)]$ , the runs are universally quantified, and both the rate and the almost-sure convergence are required.

Contributions are welcome on the general infrastructure as well: the spectrum of an average of random orthogonal projections, measurability of the proximity map, and conditional expectations of random projection updates are all reusable beyond this mission.

Selected references

D. Grishchenko, F. Iutzeler, J. Malick, Proximal gradient methods with adaptive subspace sampling, Mathematics of Operations Research, 2021; arXiv:2004.13356v1. https://arxiv.org/abs/2004.13356
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011 (Prop. 12.27, Th. 26.2). https://doi.org/10.1007/978-1-4419-9467-7
S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4), 2015 (Lemma 3.11). https://arxiv.org/abs/1405.4980
P. Richtárik, M. Takáč, Iteration complexity of randomized block-coordinate descent methods for minimizing a composite function, Mathematical Programming 144, 2014. https://doi.org/10.1007/s10107-012-0614-z

8 thms1 active userReviewed

Convex Optimization Functional Analysis Operations Research·Captain: mikedeng1

Multivariate Monotone Inclusions in Saddle Form: The Asynchronous Block-Iterative Saddle Splitting Algorithm Converges Weakly to a Primal-Dual Kuhn–Tucker PointResearch Paper

Motivation

Many problems in convex optimization, variational inequalities, game theory and signal processing are systems of monotone inclusions coupled by linear operators: several unknowns $x_i$ in different Hilbert spaces, each subject to its own maximally monotone, cocoercive and Lipschitzian operators, and tied together through linear maps $L_{ki}$ and composite terms. Bùi and Combettes (arXiv:2002.06135, Mathematics of Operations Research, 2022) introduce a single model, Problem 1.1, that contains a large part of these formulations and design algorithms for it that are fully split (each operator is used separately, set-valued operators through their resolvents and single-valued ones through forward evaluations), block-iterative (only some blocks are updated at each iteration) and asynchronous (updates may use information computed up to $T$ iterations earlier).

The paper places itself after a line of primal-dual splitting methods: Briceño-Arias and Combettes (SIAM J. Optim. 2011, doi:10.1137/10081602x) for a two-operator monotone+skew model, Alotaibi, Combettes and Shahzad (SIAM J. Optim. 2014) for Fejér approximation of a Kuhn–Tucker set, Combettes and Eckstein (Math. Program. B168, 2018) for asynchronous block-iterative primal-dual decomposition, and the projective splitting methods of Johnstone and Eckstein (2020–2021). These earlier methods work in the primal-dual space $\mathcal H\oplus\mathcal G$ . The new idea is to reformulate the problem as finding a zero of a saddle operator on a larger space and to approximate that zero set from outside by half-spaces.

Setting

Let $I$ and $K$ be finite index sets and let $(\mathcal H_i)_{i\in I}$ , $(\mathcal G_k)_{k\in K}$ be real Hilbert spaces, with Hilbert direct sums $\mathcal H=\bigoplus_i\mathcal H_i$ and $\mathcal G=\bigoplus_k\mathcal G_k$ . For every $i$ and $k$ the data are:

$A_i:\mathcal H_i\to2^{\mathcal H_i}$ maximally monotone, $C_i$ cocoercive with constant $\alpha^c_i>0$ , $Q_i$ monotone and $\alpha^\ell_i$ -Lipschitzian, and $R_i:\mathcal H\to\mathcal H_i$ such that $R=(R_i)_i$ is monotone and $\chi$ -Lipschitzian on $\mathcal H$ ;
$B^m_k$ , $D^m_k$ maximally monotone on $\mathcal G_k$ , $B^c_k$ , $D^c_k$ cocoercive with constants $\beta^c_k,\delta^c_k>0$ , and $B^\ell_k$ , $D^\ell_k$ monotone and Lipschitzian with constants $\beta^\ell_k,\delta^\ell_k$ ;
bounded linear $L_{ki}:\mathcal H_i\to\mathcal G_k$ , and vectors $s^*_i\in\mathcal H_i$ , $r_k\in\mathcal G_k$ .

The parallel sum of $B,D:\mathcal G_k\to2^{\mathcal G_k}$ is $B\,\square\,D=(B^{-1}+D^{-1})^{-1}$ . Write $\mathsf B_k=B^m_k+B^c_k+B^\ell_k$ and $\mathsf D_k=D^m_k+D^c_k+D^\ell_k$ . The primal problem (1.1) asks for $\overline x\in\mathcal H$ with

s^*_i\in A_i\overline x_i+C_i\overline x_i+Q_i\overline x_i+R_i\overline x+\sum_{k\in K}L^*_{ki}\Big((\mathsf B_k\,\square\,\mathsf D_k)\Big(\sum_{j\in I}L_{kj}\overline x_j-r_k\Big)\Big)\quad(\forall i\in I).

Its set of solutions is $\mathscr P$ . The dual problem (1.2) asks for $\overline v^*\in\mathcal G$ such that some $x\in\mathcal H$ satisfies $s^*_i-\sum_jL^*_{ji}\overline v^*_j\in A_ix_i+C_ix_i+Q_ix_i+R_ix$ and $\overline v^*_k\in(\mathsf B_k\,\square\,\mathsf D_k)(\sum_jL_{kj}x_j-r_k)$ ; its set of solutions is $\mathscr D$ . The Kuhn–Tucker set $\mathsf Z\subset\mathcal H\oplus\mathcal G$ (2.13) collects the pairs $(\overline x,\overline v^*)$ satisfying the first condition at $\overline x$ and $\sum_jL_{kj}\overline x_j-r_k\in\mathsf B_k^{-1}\overline v^*_k+\mathsf D_k^{-1}\overline v^*_k$ .

On $\mathbf X=\mathcal H\oplus\mathcal G\oplus\mathcal G\oplus\mathcal G$ the saddle operator $\boldsymbol{\mathcal S}$ (2.11) maps $(x,y,z,v^*)$ to the product of the sets $-s^*_i+A_ix_i+C_ix_i+Q_ix_i+R_ix+\sum_kL^*_{ki}v^*_k$ , $\ B^m_ky_k+B^c_ky_k+B^\ell_ky_k-v^*_k$ , $\ D^m_kz_k+D^c_kz_k+D^\ell_kz_k-v^*_k$ and $\{r_k+y_k+z_k-\sum_iL_{ki}x_i\}$ . It splits as $\boldsymbol{\mathcal S}=\mathbf M+\mathbf C$ (Definition 2.4), where $\mathbf C$ collects the cocoercive operators.

Algorithm 3.4 runs, at iteration $n$ , over activated blocks $I_n\subset I$ , $K_n\subset K$ . For $i\in I_n$ it computes a resolvent step $a_{i,n}=J_{\gamma A_i}(\cdot)$ from the delayed iterate $x_{\pi_i(n)}$ ; for $k\in K_n$ it computes $b_{k,n}$ , $d_{k,n}$ from resolvents of $B^m_k$ , $D^m_k$ at the delayed iterate $\omega_k(n)$ . Blocks that are not activated keep their previous values. From these quantities it forms a half-space containing $\operatorname{zer}\boldsymbol{\mathcal S}$ , measured by a number $\Delta_n$ that involves $\alpha=\min\{\alpha^c_i,\beta^c_k,\delta^c_k\}$ . If $\Delta_n>0$ , it moves $(x_n,y_n,z_n,v^*_n)$ toward that half-space with relaxation $\lambda_n\in[\varepsilon,2-\varepsilon]$ ; otherwise the iterate stays put.

Formalization targets

Goal: Theorem 3.5

Under Assumptions 3.1–3.3 (step-size ranges tied to $\alpha$ , $\sigma>1/(4\alpha)$ and $\varepsilon$ by (3.1); every block activated at least once in every $P+1$ consecutive iterations; delays at most $T$ ), if the dual problem has a solution, then every run of Algorithm 3.4 satisfies

\sum_n\|x_{i,n+1}-x_{i,n}\|^2<\infty,\qquad x_{i,n}-a_{i,n}\to0,\qquad v^*_{k,n}-e^*_{k,n}\to0,

together with the analogous statements for $y,z,v^*$ and $b,d$ . There exist $\overline x\in\mathscr P$ and $\overline v^*\in\mathscr D$ with $(\overline x,\overline v^*)\in\mathsf Z$ such that

x_{i,n}\rightharpoonup\overline x_i,\qquad a_{i,n}\rightharpoonup\overline x_i,\qquad v^*_{k,n}\rightharpoonup\overline v^*_k.

Milestones

In attack order:

Proposition 2.2(i)–(ii): $\boldsymbol{\mathcal S}$ is maximally monotone and $\operatorname{zer}\boldsymbol{\mathcal S}$ is closed and convex.
Proposition 2.2(iii)–(iv): zeros of $\boldsymbol{\mathcal S}$ project into $\mathsf Z\subset\mathscr P\times\mathscr D$ , and $\mathscr D\neq\varnothing\Leftrightarrow\operatorname{zer}\boldsymbol{\mathcal S}\neq\varnothing\Leftrightarrow\mathsf Z\neq\varnothing\Rightarrow\mathscr P\neq\varnothing$ .
Proposition 2.5: $\boldsymbol{\mathcal S}=\mathbf M+\mathbf C$ , $\mathbf M$ maximally monotone, $\mathbf C$ $\alpha$ -cocoercive, and the half-spaces containing $\operatorname{zer}\boldsymbol{\mathcal S}$ .
Lemma A.4: the relaxed half-space outer-approximation iteration (A.3) is Fejér monotone and converges weakly when every weak sequential cluster point lies in $Z$ .
Proposition 2.6: the iteration (2.32) on $\mathbf X$ converges weakly to a zero of $\boldsymbol{\mathcal S}$ when its three stated residual conditions hold.
Lemmas A.1, A.2 and A.3: boundedness of resolvent sequences, strong monotonicity of $\gamma^{-1}\mathrm{Id}-A$ , and the vanishing of the delayed differences $x_{\vartheta_i(n)}-x_n$ .

Significance

Theorem 3.5 gives weak convergence of a method that uses each operator of Problem 1.1 separately, needs no inversion of linear operators and no knowledge of $\|L\|$ , and updates nonempty subsets of blocks subject to the coverage windows and bounded delays of Assumptions 3.2–3.3. It produces primal and dual solutions together. Section 4 of the paper derives from it algorithms for variational inequalities over sums of sets and for multivariate convex minimization with infimal convolutions. The hypothesis is dual solvability. Remark 2.3 shows that primal solvability alone is not enough: there are instances with $\mathscr P\neq\varnothing$ and $\mathsf Z=\varnothing$ .

The theorem is proved in the paper. A formalization adds machine-checked foundations that later work in splitting methods can reuse: the saddle operator and its maximal monotonicity; the Fejér outer-approximation principle in Hilbert space (Lemma A.4, cited by the paper from an encyclopedia entry); and the asynchrony lemma (Lemma A.3). To our knowledge none of these results has been formalized before.

Difficulty

The obvious approach would be to show that Algorithm 3.4 is a Fejér-monotone iteration toward $\mathsf Z$ in $\mathcal H\oplus\mathcal G$ . That approach fails: for the general Problem 1.1, no half-space separating the current point from $\mathsf Z$ can be computed from separate operator evaluations (Remark 2.3(iii)). The algorithm instead targets $\operatorname{zer}\boldsymbol{\mathcal S}$ in the larger space $\mathbf X$ . The link back to $\mathscr P$ , $\mathscr D$ and $\mathsf Z$ is Proposition 2.2.

The second difficulty is asynchrony. The half-space at iteration $n$ is built from points computed at earlier iterations, with stale step sizes. To show that the weak cluster points are zeros of $\boldsymbol{\mathcal S}$ , one has to control these delays (Lemma A.3) and use the cocoercive and Lipschitzian terms uniformly over the step-size ranges (Lemmas A.1–A.2).

Formalization scope

Spaces. Every space is a complete real inner product space. $\mathcal H$ and $\mathcal G$ are PiLp 2 over finite index types, and $\mathbf X$ is a nested WithLp 2 product, so all norms and inner products are the Hilbert ones (not sup norms).
Operators. Set-valued operators are maps E → Set E. Monotonicity, maximal monotonicity, zer, cocoercivity, resolvents and weak convergence are the published ThreeOpSplitting.Convergence definitions; inverses and sums of set-valued maps are the published DouglasRachfordPPA.GenDR ones.
Runs. A run of Algorithm 3.4 is a predicate on given sequences that pins every assignment of (3.3). This includes the delayed indices inside the step sizes, the carry-over of inactive blocks (stated at $n+1$ ), the recomputation of $e_{k,n}$ for every $k$ , and $\Delta_n$ with the factor $(4\alpha)^{-1}$ at the current iterates. The resolvents are given maps constrained by the resolvent identity at every positive step.
Constants and assumptions. $\alpha$ is pinned as the least cocoercivity constant. The delay bound $n-T\le\pi_i(n)\le n$ is written without natural-number subtraction. " $\varlimsup\Delta_n\le0$ " in Proposition 2.6 is stated as "eventually $\Delta_n\le\delta$ for every $\delta>0$ ".
Ruling out trivial readings. The run predicate determines every assignment of (3.3), so no free choice of outputs makes the theorem trivial. The hypothesis is dual solvability $\mathscr D\neq\varnothing$ exactly as in (1.2), not the stronger-looking $\operatorname{zer}\boldsymbol{\mathcal S}\neq\varnothing$ (equivalent only by Proposition 2.2). The conclusion is weak convergence to a pair that is simultaneously primal, dual and Kuhn–Tucker. A sorry-free check shows that the goal's hypotheses are jointly satisfiable.
Not included. Theorem 3.7 (strong convergence of a Haugazeau-type variant) with Proposition 2.7 and Lemma A.5, Proposition 2.2(v), and the applications of Section 4.
Reusable parts. The saddle operator and its splitting, Lemma A.4, Lemma A.3, and Lemmas A.1–A.2 are stated in general form and can serve other splitting missions. Contributions of auxiliary results are welcome, for example demiclosedness of maximally monotone operators, Minty's theorem in the published encoding, and Fejér-monotone weak convergence (Opial).

Selected references

M. N. Bùi and P. L. Combettes, Multivariate monotone inclusions in saddle form, Mathematics of Operations Research, 2022; preprint arXiv:2002.06135v3, 2021. https://arxiv.org/abs/2002.06135
H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
L. M. Briceño-Arias and P. L. Combettes, A monotone+skew splitting model for composite monotone inclusions in duality, SIAM Journal on Optimization 21, 2011. https://doi.org/10.1137/10081602x
P. L. Combettes and J. Eckstein, Asynchronous block-iterative primal-dual decomposition methods for monotone inclusions, Mathematical Programming B168, pp. 645–672, 2018 (reference [25] of arXiv:2002.06135).
P. L. Combettes, Fejér-monotonicity in convex optimization, in: Encyclopedia of Optimization, vol. 2, pp. 106–114, Springer, 2001 (reference [22] of arXiv:2002.06135; source of Lemma A.4).

13 thms1 active userReviewed

Linear algebra Operations Research·Captain: mikedeng1

Market Efficient Portfolios in a Systemic Economy: f-Efficient Bank Holdings Exist, Attain Mean Squared Deviation (bᵀv)²/(1ᵀG⁻¹1), and Are Unique if and only if There Are Exactly Two BanksResearch Paper

Motivation

When banks are hit by losses they sell assets to restore their leverage targets, and these fire sales depress prices for every other holder of the same assets. The resulting deviation of market capitalization from its fundamental value is a systemic externality: it depends not on any single bank's portfolio but on how the stock of each asset is distributed across banks. Awiszus, Capponi and Weber (arXiv:2003.10121, Operations Research 2022) ask which distribution of a fixed stock of assets among banks with fixed budgets minimizes this externality, as measured by the expected squared deviation of market capitalization from fundamentals. The question matters to macroprudential regulators, who can influence portfolio overlap among banks, and it connects to the literature on overlapping portfolios and price-mediated contagion (Greenwood, Landier and Thesmar, 2015; Capponi and Larsson, 2015).

The paper's answer is explicit: the optimal mean squared deviation has a closed form, the optimum is computed by a two-step "aggregate first, then allocate" procedure, and the optimal allocation is unique exactly when there are two banks.

Setting

There are $K$ assets and $N$ banks. A holding matrix $Q\in\mathbb R^{K\times N}$ records in entry $Q_{ki}$ the holding of asset $k$ by bank $i$ , so column $i$ is bank $i$ 's portfolio. Initial prices are normalized to $1$ .

The vector $q\in\mathbb R^K$ gives the total initial holdings of each asset in the banking sector, and $b\in\mathbb R^N$ gives the banks' budgets. The feasible holding matrices are

\mathscr D(q,b) = \{Q\in\mathbb R^{K\times N} \mid Q\mathbf 1_N = q,\ \mathbf 1_K^\top Q = b^\top\}.

Price shocks $Z_1,\dots,Z_K$ have means $\mu\in\mathbb R^K$ and are uncorrelated with variances $\sigma_k^2$ , $\sigma_k>0$ (Assumption 2). Their second-moment matrix is

G = \mu\mu^\top + \mathrm{Diag}(\sigma^2).

The systemic significance vector $v\in\mathbb R^N$ (the paper's (3.1)) summarizes each bank's leverage targeting, liquidation strategy and the assets' illiquidity. To first order, the deviation of market capitalization from fundamentals is $(Qv)^\top Z$ , and its second moment is the mean squared deviation

\mathrm{MSD}(Q) = (Qv)^\top G\,(Qv).

A holding matrix $Q^*\in\mathscr D(q,b)$ is f-efficient (Definition 1) if it minimizes $\mathrm{MSD}$ over $\mathscr D(q,b)$ .
Assumption 3: $v_i\neq v_j$ for some $i,j$ , and $b^\top v\neq 0$ .
The aggregate problem (4.3) minimizes $y^\top G y$ over $\mathscr D_y = \{y\in\mathbb R^K \mid \mathbf 1_K^\top y = b^\top v\}$ . With $z = G^{-1}\mathbf 1_K$ , put $y^* = \frac{b^\top v}{\mathbf 1_K^\top z}\,z$ .

Formalization targets

Goal: Theorem 4.1

Let $N,K\ge 2$ . Then

\exists\,Q^*\ \text{f-efficient with}\quad \mathrm{MSD}(Q^*) = \frac{(b^\top v)^2}{\mathbf 1_K^\top G^{-1}\mathbf 1_K},

the f-efficient holding matrix is unique if and only if $N=2$ , and in that case it equals

Q^{N=2} = \frac{1}{v_2-v_1}\big(\,v_2 q - y^*\;\;\; y^* - v_1 q\,\big)\in\mathbb R^{K\times 2}.

Milestones

$G$ is positive definite, $G^{-1}$ has the Sherman–Morrison form, and $\mathbf 1_K^\top G^{-1}\mathbf 1_K\neq 0$ (proof of Lemma 4.1).
Lemma 4.1: $y^*$ is the unique solution of the aggregate problem (4.3).
Proposition 4.2: for $N\ge2$ , $K\ge1$ there is $Q^*\in\mathscr D(q,b)$ with $Q^*v=y^*$ .
Proposition 4.1: $Q^*\in\mathscr D(q,b)$ is f-efficient if and only if $Q^*v$ solves (4.3).
Remark EC.1.1: $Q^*$ is f-efficient if and only if $F\,\mathrm{vec}(Q^*) = (b,q,y^*)$ for the $(2K+N)\times KN$ matrix $F$ of (EC.1.12).
The value computation $\mathrm{MSD}(Q^*) = (y^*)^\top G y^* = (b^\top v)^2/\mathbf 1_K^\top G^{-1}\mathbf 1_K$ (proof of Theorem 4.1 a).
$\mathrm{rank}(F) = 2K+N-2$ and $\mathrm{null}(F) = (N-2)(K-1)$ (proof of Theorem 4.1 b).

Significance

The result itself. Theorem 4.1 gives the smallest achievable mean squared deviation of market capitalization from fundamentals for a given asset supply, budget profile and systemic significance profile, as an explicit function of the shock moments. It is the benchmark against which the paper measures the inefficiency of observed and diversified holdings (Section 4.2 shows that full diversification is f-efficient only in a degenerate case) and drives the comparative statics of Section 5. Part b) says that with three or more banks efficiency leaves an affine family of optimal allocations of dimension $(N-2)(K-1)$ , so a regulator has residual freedom to pursue other objectives at no cost in market efficiency.

Formalizing it. The result is proved in the paper; no machine-checked version is known. The formal development delivers the theorem together with a reusable treatment of minimizing a positive definite quadratic form over a hyperplane, the existence part of the transportation-type linear system $Q\mathbf 1_N=q$ , $\mathbf 1_K^\top Q=b^\top$ , $Qv=y$ , and an exact rank computation for the structured matrix $F$ . The uniqueness characterization in part b) depends on that rank computation, which the paper carries out by Gaussian elimination on block matrices.

Difficulty

The minimization over $\mathscr D(q,b)$ is a $KN$ -dimensional quadratic program whose objective is degenerate: it depends on $Q$ only through the $K$ -vector $Qv$ . Strict convexity therefore cannot give uniqueness, since the objective is constant along every direction in which $Qv$ and the constraints do not change, and the obvious argument for part b) fails. Existence is not automatic either: $\mathscr D(q,b)$ is unbounded, and one must show that every point of the hyperplane $\mathscr D_y$ is attained as $Qv$ by a feasible $Q$ , which fails when $v$ is constant. The uniqueness statement is a dimension count: it needs the exact rank of the $(2K+N)\times KN$ constraint matrix $F$ , whose rows carry exactly two linear dependencies under Assumption 3, so that the solution set has dimension $(N-2)(K-1)$ , which is positive as soon as $N\ge3$ and $K\ge2$ .

Formalization scope

Assets are Fin K, banks are Fin N, all quantities are real; holding matrices are Matrix (Fin K) (Fin N) ℝ. The paper's banks 1 and 2 are the indices 0 and 1.
$G^{-1}$ is Mathlib's Matrix.inv, which returns $0$ on singular matrices. Every statement that mentions $G^{-1}$ , $z$ or $y^*$ assumes $\sigma_k>0$ for all $k$ (Assumption 2), and every statement that divides by $\mathbf 1_K^\top z$ assumes $K\ge1$ .
The systemic significance $v$ is a free parameter in $\mathbb R^N$ subject to Assumption 3, not derived from the primitives by (3.1). Every result of Section 4 holds for each such $v$ , and $v$ does not depend on $Q$ .
Added hypothesis: $\sum_k q_k=\sum_i b_i$ appears on the statements that need $\mathscr D(q,b)\neq\emptyset$ (Proposition 4.2 and Theorem 4.1). The paper derives it from feasibility on p. 11; without it part a) is false.
Statements that use only the first half of Assumption 3 ( $v$ not constant) assume only that half. The goal carries Assumption 3 in full.
f-efficiency is an argmin. It is the minimization over $\mathscr D(q,b)$ of Definition 1, and $\mathrm{MSD}$ is the quadratic form $(Qv)^\top G(Qv)$ . Defining f-efficiency as $Qv=y^*$ , or defining $\mathrm{MSD}$ through $y^*$ , would remove the optimization from the goal and is ruled out.
$\mathrm{vec}(Q)$ is indexed by pairs (asset, bank) instead of stacked columns, and $\mathrm{null}(F)$ is the Module.finrank of the kernel of $x\mapsto Fx$ .
$Q^{N=2}$ is defined for $v\in\mathbb R^2$ ; the goal transports it along $N=2$ with Fin.cast.

The development needs the Sherman–Morrison identity for a diagonal-plus-rank-one matrix, the minimizer of a positive definite quadratic form under one linear constraint, explicit constructions in $\mathscr D(q,b)$ , and a rank computation. Contributions of reusable lemmas for these, and of proofs of the milestones in any order, are welcome.

Selected references

K. Awiszus, A. Capponi, S. Weber, Market Efficient Portfolios in a Systemic Economy, Operations Research 70(2), 2022. Preprint arXiv:2003.10121v3. https://arxiv.org/abs/2003.10121
R. Greenwood, A. Landier, D. Thesmar, Vulnerable Banks, Journal of Financial Economics 115(3), 2015. https://doi.org/10.1016/j.jfineco.2014.11.006
A. Capponi, M. Larsson, Price Contagion through Balance Sheet Linkages, Review of Asset Pricing Studies 5(2), 2015. https://doi.org/10.1093/rapstu/rav006
D. S. Bernstein, Matrix Mathematics, Princeton University Press, 2005.

9 thms1 active userReviewed

Combinatorics Operations Research·Captain: mikedeng1

Maximizing Sequence-Submodular Functions and Its Application to Online Advertising: Any α-Greedy Sequence Achieves 1 − 1/e^α of the Optimum of a Non-Decreasing Sequence-Submodular FunctionResearch Paper

Motivation

Many allocation problems in online advertising are decisions about order, not only about membership. A search engine that rewrites an incoming query into one of several ad-matching configurations, or a publisher that runs a sequence of ad allocations over a day, extracts revenue that depends on which configurations are used and on the order in which they are applied: advertisers' budgets are spent down along the way, so a configuration run early changes what a later one can earn. Classical submodular set functions cannot express this order dependence, and the guarantees developed for them do not apply directly.

Alaei, Makhdoumi and Malekian (arXiv:1009.4153v4; Management Science, 2021) introduce sequence functions, which assign a value to every finite sequence of actions, and identify a sequence analogue of monotonicity and submodularity under which a simple greedy rule is provably near-optimal. They apply the discrete version to query rewriting in sponsored search and a continuous version to online ad allocation with budgets.

Timeline:

1978: Nemhauser, Wolsey and Fisher prove that the greedy algorithm achieves a $1-1/e$ fraction of the optimum for maximizing a monotone submodular set function under a cardinality constraint (Math. Programming 14).
2010–2021: Alaei, Makhdoumi and Malekian state the discrete and continuous sequence-submodular framework and prove the $1-1/e^{\alpha}$ guarantee for $\alpha$ -approximate greedy choices (arXiv first version 2010, journal version 2021).

Setting

Let $\mathcal S$ be a finite set of actions. A discrete sequence is a tuple $A=(s_1,\dots,s_k)$ with $k\ge0$ and every $s_i\in\mathcal S$ ; for $k=0$ it is the empty sequence $\emptyset$ . Its length is $|A|=k$ , and $\mathbb H^D(\mathcal S)$ denotes the set of all discrete sequences. The concatenation $A\perp B$ lists the elements of $A$ followed by those of $B$ . For $H=(s_1,\dots,s_T)$ the refinement $H_{[1,i]}=(s_1,\dots,s_i)$ is its prefix of length $i$ , with $H_{[1,0]}=\emptyset$ .

A sequence $A$ is dominated by $B$ , written $A\prec B$ , if $A$ can be obtained from $B$ by removing some of its elements while keeping the order of the remaining ones. Thus $(a,c)\prec(a,b,c)$ but $(c,a)\not\prec(a,b,c)$ .

A discrete sequence function is any $u:\mathbb H^D(\mathcal S)\to\mathbb R$ . The marginal value of appending $B$ after $A$ is

u(B\mid A)=u(A\perp B)-u(A).

The function $u$ is sequence-non-decreasing if $u(A)\le u(B)$ whenever $A\prec B$ , and $u(\emptyset)=0$ (display (10)). It is sequence-submodular if

u(C\mid A)\ \ge\ u(C\mid B)\qquad\text{for all }A,B,C\text{ with }A\prec B

(display (11)): appending the same sequence $C$ gains less after a longer history. Assumption 2 requires both properties.

The optimization problem (12) is, for a length budget $T\in\mathbb N$ ,

\max_{H\in\mathbb H^D(\mathcal S)}u(H)\quad\text{subject to}\quad|H|\le T.

For $\alpha\in[0,1]$ , a sequence $H=(s_1,\dots,s_T)$ is $\alpha$ -greedy if at every step its choice is within a factor $\alpha$ of the best single-action marginal value (display (13)):

u\big(s_i\mid H_{[1,i-1]}\big)\ \ge\ \alpha\max_{s\in\mathcal S}u\big(s\mid H_{[1,i-1]}\big)\qquad(i=1,\dots,T).

Formalization targets

Goal: Theorem 3 (p. 17)

Under Assumption 2, for every $\alpha\in[0,1]$ , every $\alpha$ -greedy $H$ of length $T$ and every sequence $O$ with $|O|\le T$ ,

u(H)\ \ge\ \Big(1-\frac1{e^{\alpha}}\Big)u(O).

Applied to the optimum $O$ of (12), this is the paper's display (14), $u(H)/u(O)\ge1-1/e^{\alpha}$ .

Milestones

Lemma 10 (p. 26): if $u$ is sequence-submodular, then for every $A$ and every nonempty $B$ there is $s\in\mathcal S$ with

u(s\mid A)\ \ge\ \frac1{|B|}\,u(B\mid A).

Eq. (38) (p. 26): for an $\alpha$ -greedy $H$ of length $k$ , every $O$ with $|O|\le k$ and every $i$ ,

u\big(s_i\mid H_{[1,i-1]}\big)\ \ge\ \frac{\alpha}{k}\Big(u(O)-u\big(H_{[1,i-1]}\big)\Big).

Eq. (41) (p. 27): under the same hypotheses,

u(H)\ \ge\ \Big(1-\Big(1-\frac{\alpha}{k}\Big)^k\Big)u(O).

Significance

For sets, the $1-1/e$ bound of Nemhauser, Wolsey and Fisher is the reference guarantee for greedy selection. Theorem 3 transfers it to sequences: any objective that can be shown sequence-non-decreasing and sequence-submodular inherits a $1-e^{-\alpha}$ guarantee for a greedy rule, with no further analysis. The paper uses this for query rewriting (Theorem 4) and, through the continuous analogue, for budgeted online ad allocation (Theorem 2). The parameter $\alpha$ covers the common situation in which the best next action can only be found approximately, for instance by solving a subproblem with an approximation algorithm.

Theorem 3 is proved in the paper. As far as a search of the Prove2Me catalog shows, no sequence-function model and no sequence-submodular greedy bound has been formalized there; set-function greedy bounds exist on the platform only as separate, set-based statements. This mission produces a machine-checked version of the discrete model and of the guarantee, which later missions on sequence or string submodularity can import.

Difficulty

The set-function argument compares the greedy set with the optimum by adding the optimum's elements one at a time to the current greedy set and using that the union is at least as valuable as the optimum. For sequences the comparison object is $H_{[1,i-1]}\perp O$ , and two features of the order break the direct transcription. First, sequence-submodularity only compares marginal values after a dominated history, so each comparison has to be arranged so that the shorter history is a subsequence of the longer one, in the right order. Second, the averaging over the elements of $O$ produces a factor $1/|O|$ , while the recursion needs the uniform factor $1/k$ ; the replacement relies on feasibility $|O|\le k$ together with nonnegativity of $u(O\mid H_{[1,i-1]})$ , which comes from monotonicity. A formal proof also has to handle the indices of the refinement and the edge cases $|O|=0$ , $k=0$ and $\alpha=0$ that the printed argument passes over.

Formalization scope

All declarations live in the namespace SeqSubmod.Discrete.

Sequences are Lean lists List S over a type S with [Fintype S]; concatenation is ++, the empty sequence is [], and $|A|$ is A.length.
Domination $\prec$ is List.Sublist (A <+ B), the subsequence order. It is neither the prefix order nor the subset order of the underlying sets.
marginal u B A := u (A ++ B) - u A is $u(B\mid A)$ , with the arguments in the paper's order.
Sequence-non-decreasing keeps the normalization $u(\emptyset)=0$ , so $u\ge0$ ; sequence-submodularity has the paper's direction.
The $\alpha$ -greedy condition uses Lean's 0-based indexing: H[i] is the paper's $s_{i+1}$ and H.take i is $H_{[1,i]}$ . The maximum over $\mathcal S$ is Finset.univ.sup', which needs [Nonempty S]. This is added and harmless: with no actions the only sequence is empty.
The optimum of (12) is not defined: the goal quantifies over every $O$ with $|O|\le|H|$ . This is equivalent to the statement about the optimum, which exists because there are finitely many feasible sequences.
The ratio (14) is stated in multiplied form, $(1-e^{-\alpha})\,u(O)\le u(H)$ , because the ratio is $0/0$ when $u(O)=0$ .
Lemma 10 adds $B\neq\emptyset$ , since $1/|B|$ is undefined at $|B|=0$ .

A trivializing formalization is ruled out: a prefix or subset order, a reversed (11), a dropped $u(\emptyset)=0$ , or an existentially quantified $O$ would each change the theorem, and none is used.

A complete development needs telescoping sums of marginal values along a list, an averaging argument over a finite sum, the recursion (40), and the inequality $(1-\alpha/k)^k\le e^{-\alpha}$ , which Mathlib provides. The definitions file is reusable by any later work on sequence functions, including the continuous model of the paper's §3, which is not part of this mission. Proofs of the milestones, alternative proofs of the goal, and tightness examples are all welcome contributions.

Selected references

S. Alaei, A. Makhdoumi, A. Malekian, Maximizing Sequence-Submodular Functions and Its Application to Online Advertising, Management Science, 2021; preprint arXiv:1009.4153v4 (2019). https://arxiv.org/abs/1009.4153
G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions — I, Mathematical Programming 14, 265–294, 1978. https://doi.org/10.1007/BF01588971

5 thms1 active userReviewed

Convex Optimization Operations Research·Captain: mikedeng1

Time-Varying Semidefinite Programs: Under Strict Feasibility, Feasible Polynomial Solutions Have Objective Values Converging to the TV-SDP Optimal ValueResearch Paper

Motivation

Many planning problems ask for a decision that varies over a time horizon and must satisfy a constraint at every instant, possibly with cumulative effects of past decisions. The applications in the source paper are a maximum-flow problem with time-varying pipeline capacities, a wireless coverage problem for a moving target region, and the approximation of Pareto curves of bi-objective semidefinite programs. Ahmadi and El Khadir (arXiv:1808.03994, Mathematics of Operations Research, 2021) model these as time-varying semidefinite programs (TV-SDPs), a common generalization of semidefinite programming and of the continuous linear programs of Bellman (1953), Tyndall (1965) and Levinson (1966), which are the case of diagonal matrices.

A TV-SDP is an infinite-dimensional problem: its variable is a function. The paper's main message is that, under a strict feasibility assumption, nothing is lost by searching only over polynomial solutions, and that the best polynomial solution of a fixed degree can be computed by an ordinary SDP through sum-of-squares certificates. The first statement, Theorem 4, is what justifies the second as a convergent approximation scheme, and it is the goal of this mission.

Setting

Fix integers $n, m \ge 0$ . Let $\mathbf L^n$ be the set of measurable functions $x:[0,1]\to\mathbb R^n$ that are bounded, $\sup_{t\in[0,1]}\|x(t)\|_\infty<\infty$ . The data are polynomial: an objective $c=(c_1,\dots,c_n)$ of univariate polynomials, symmetric $m\times m$ matrices $A_0(t),\dots,A_n(t)$ with polynomial entries, and symmetric $m\times m$ kernels $D_1(t,s),\dots,D_n(t,s)$ with entries polynomial in $(t,s)$ . For $x\in\mathbf L^n$ define the matrix function

\mathcal Fx(t)=A_0(t)+\sum_{i=1}^n x_i(t)A_i(t)+\sum_{i=1}^n\int_0^t x_i(s)\,D_i(t,s)\,ds .

A function $x$ is feasible if $x\in\mathbf L^n$ and $\mathcal Fx(t)\succeq0$ for almost every $t\in[0,1]$ . The TV-SDP is

\mathrm{opt}=\sup\Bigl\{\langle c,x\rangle_{\mathbf L^n}=\int_0^1\langle c(t),x(t)\rangle\,dt \;:\; x \text{ feasible}\Bigr\}\in[-\infty,+\infty].

It is strictly feasible if some $x^s\in\mathbf L^n$ and $\varepsilon>0$ satisfy $\mathcal Fx^s(t)\succeq\varepsilon I$ for almost every $t\in[0,1]$ . A polynomial solution is $x(t)=(p_1(t),\dots,p_n(t))$ for polynomials $p_i$ .

The proof uses the mollifying operators $\mathcal M_v$ , $v\in\mathbb N$ : with the bump $J(t)=c\,e^{-1/(1-t^2)}$ for $|t|<1$ , $J(t)=0$ otherwise, normalized so that $\int_{\mathbb R}J=1$ ,

\mathcal M_vf(t)=\int_0^1 v\,J(v(t-s))\,f(s)\,ds ,

applied entrywise to vector- and matrix-valued functions. In Lean these are Ln, Sm, Data, F, Feasible, StrictlyFeasible, obj, opt, polySol, J, cJ, Mv, MvVec and MvMat in the namespace TVSDP.PolyOpt.

Formalization targets

Goal: Theorem 4 (p. 11)

If the TV-SDP is strictly feasible, there are polynomial vectors $p^k$ such that every $x^k=p^k$ is feasible and

\langle c,x^k\rangle_{\mathbf L^n}\longrightarrow\mathrm{opt}\qquad(k\to\infty),

the limit taken in the extended reals, so $\mathrm{opt}=+\infty$ is included.

Milestones

Proof of Theorem 4, p. 13. For feasible $x$ and strictly feasible $x^s$ with margin $\varepsilon$ , the combination $(1-\lambda)x+\lambda x^s$ satisfies $\mathcal F(\cdot)\succeq\lambda\varepsilon I$ a.e., and its objective tends to $\langle c,x\rangle$ as $\lambda\to0^+$ .
Proposition 1, p. 11 (first two sentences). $\mathcal M_vf$ is continuous and $\int_0^1|\mathcal M_vf-f|\to0$ for bounded measurable $f$ .
Lemma 3(a), p. 12. $M(t)\succeq0$ a.e. implies $\mathcal M_vM(t)\succeq0$ for all $t\in[0,1]$ .
Lemma 3(b), p. 12, and the explicit rate of its proof: $\sup_{t\in[0,1]}|a(t)\mathcal M_vx(t)-\mathcal M_v(a\cdot x)(t)|\le L\gamma/v\to0$ for polynomial $a$ .
Proof of Theorem 4, p. 13 (minimum-eigenvalue step). If $G(t)\succeq\beta I$ on $[0,1]$ and $\sup_t\|G(t)-H_v(t)\|\to0$ , then $H_v(t)\succeq\frac\beta2 I$ on $[0,1]$ for large $v$ .
Proof of Theorem 4, pp. 13–14. $\sup_t\|\mathcal Fx(t)-\mathcal Fy(t)\|\le C\sup_t\|x(t)-y(t)\|_\infty$ with $C=\sup_{t,s\in[0,1]}\sum_i(\|A_i(t)\|+\|D_i(t,s)\|)$ .

Significance

The result. Theorem 4 says that the supremum of a strictly feasible TV-SDP over polynomial solutions equals its supremum over all bounded measurable solutions. Combined with the paper's Theorem 6, which computes the best degree- $d$ polynomial solution by an SDP, it shows that these SDP values form a nondecreasing sequence of lower bounds converging to $\mathrm{opt}$ . Without it, the polynomial restriction could have a strictly smaller value; Example 1 of the paper shows that this happens when strict feasibility fails, where the unique feasible solution is a step function.

Formalizing it. The result is proved in the paper, not formalized anywhere. A machine-checked proof also has to repair the printed argument: the operator $\mathcal M_v$ integrates over $[0,1]$ only and is not normalized near the endpoints ( $\mathcal M_v1(0)=\tfrac12$ for $v\ge1$ ), so three auxiliary statements of §3.1 are false as printed (see Formalization scope), although Theorem 4 itself is true. Any complete proof therefore needs an argument that handles the endpoints, which the formal development would record.

Difficulty

The natural route is "perturb into the strict interior, smooth, approximate by polynomials", and each step preserves feasibility only up to a uniform error, so the margin $\varepsilon$ must survive all three. The difficulty is uniformity on the closed interval: smoothing commutes with $\mathcal F$ only approximately, the Volterra term $\int_0^t x_i(s)D_i(t,s)\,ds$ couples times, and at $t=0$ and $t=1$ the mollifier of Definition 3 loses half its mass. Applying the printed Corollary 1 directly fails at the endpoints. In Lean, a further cost is the bookkeeping between "almost every $t\in[0,1]$ " for feasibility and "every $t\in[0,1]$ " for the smoothed and polynomial solutions.

Formalization scope

Conventions committed to:

Functions are total maps on $\mathbb R$ ; only their values on $[0,1]$ matter. "Almost every $t\in[0,1]$ " is with respect to Lebesgue measure restricted to $[0,1]$ (volume.restrict (Set.Icc 0 1)), never Lebesgue measure on $\mathbb R$ .
$\mathbf L^n$ is bounded and measurable, with the sup norm on $\mathbb R^n$ ; the bold $\mathbf L^1$ of the paper is $\mathbf L^n$ with $n=1$ , not Lebesgue $L^1$ .
The data are polynomial (the paper's standing assumption, p. 3), with symmetric polynomial matrices. Theorem 4 is false for general bounded measurable data.
$\mathcal F$ is defined entrywise; the kernel term is an interval integral, with variable $0$ of $D_i$ the outer time $t$ and variable $1$ the integration variable $s$ .
$\mathrm{opt}$ is an EReal supremum; the matrix inequality $X\succeq\beta I$ is positive semidefiniteness of $X-\beta I$ .
$J(\pm1)=0$ (the page's formula is undefined there); $\mathcal M_v$ is defined for $v\in\mathbb N$ exactly as in Definition 3, without normalization.
Matrix norms are the entrywise maximum; the page allows any matrix norm.

Trivializations ruled out: feasibility is a.e. on $[0,1]$ only, solutions in $\mathbf L^n$ are bounded, $\mathrm{opt}$ is not a real sSup (which would be $0$ on an unbounded set), and polynomial solutions are genuine polynomials evaluated everywhere, not functions that agree with a polynomial almost everywhere.

Deliberately absent: the third sentence of Proposition 1 (uniform convergence $\mathcal M_vf\to f$ for continuous $f$ ), Lemma 3(c) and Corollary 1. All three are false for the operator of Definition 3 because of the endpoint effect; for example, Corollary 1 fails for $x=0$ , $A_0=I$ at $t=0$ . The printed constant $C$ on p. 14 has $D_i(s,t)$ in place of $D_i(t,s)$ , and with it the Lipschitz display fails; milestone 6 uses the corrected constant. Measurability of $M$ is added in Lemma 3(a), where the paper uses it implicitly.

Infrastructure needed: interval mollification of bounded measurable functions, uniform convergence on $[0,1]$ , the Weierstrass approximation theorem for $\mathbb R^n$ -valued functions (in Mathlib), and Loewner-order perturbation bounds. The mollifier and the Loewner perturbation lemma are reusable beyond this mission. Contributions of proofs for any milestone, of the missing endpoint-robust smoothing step, and of the paper's Example 1 are welcome.

Selected references

A. A. Ahmadi and B. El Khadir, Time-varying semidefinite programs, Mathematics of Operations Research, 2021; arXiv:1808.03994v2. https://arxiv.org/abs/1808.03994
R. Bellman, Bottleneck problems and dynamic programming, Proceedings of the National Academy of Sciences 39(9), 1953. https://doi.org/10.1073/pnas.39.9.947
W. F. Tyndall, A duality theorem for a class of continuous linear programming problems, Journal of the SIAM 13(3), 1965. https://doi.org/10.1137/0113044
N. Levinson, A class of continuous linear programming problems, Journal of Mathematical Analysis and Applications 16(1), 1966. https://doi.org/10.1016/0022-247X(66)90184-3
R. A. Adams and J. J. F. Fournier, Sobolev Spaces, 2nd ed., Academic Press, 2003 (Theorem 2.29, cited for Proposition 1).

10 thms1 active userReviewed

Combinatorics Linear Optimization Operations Research·Captain: mikedeng1

Robust Optimization Approach to Process Flexibility Designs with Contribution Margin Differentials: The Alternate Long Chain Is Worst-Case Optimal Among Balanced Two-Margin Long ChainsResearch Paper

Why process flexibility matters

A factory can respond to uncertain demand by allowing a plant to make more than one product. Those extra capabilities cost money, so the design question is where to place a limited number of plant–product links. The usual measure of a flexible production system is the number of units sold. When products have different contribution margins, however, two designs with the same sales may earn different profits: capacity used for a low-margin product cannot then serve a high-margin one. Wang, Wang and Zhang study this distinction through worst-case demand and show that a particular arrangement of two product classes is optimal within the family of long chains (Wang, Wang and Zhang 2020, §§1 and 4).

The result addresses a concrete design choice. A long chain gives every plant two product capabilities and connects the system in a cycle. If half the products have high margins and half low margins, should the two classes be grouped on that cycle or spread out? The paper's answer is that alternating high- and low-margin products gives at least as good a worst-case score as every other long-chain arrangement, for a broad class of scores.

Production and uncertain demand

A flexibility design $A$ is a set of arcs $(j,i)$ from plant $j$ to product $i$ . Plant $j$ has capacity $C_j$ , product $i$ has demand $d_i$ and margin $p_i$ , and $x_{ij}$ units of product $i$ are made by plant $j$ . The maximum profit $g(A,d)$ is the optimum of the finite linear program

g(A,d)=\max_{x\ge0}\sum_{(j,i)\in A}p_i x_{ij},\qquad \sum_jx_{ij}\le d_i,\quad \sum_i x_{ij}\le C_j.

Products fall into $T$ categories with margins $P_1<\cdots<P_T$ . Write $S_t$ for the products with margin $P_t$ and $D_t(d)=\sum_{i\in S_t}d_i$ for their total demand. A deterministic score in the paper's class has the form $f(A,d)=h(g(A,d),(D_t(d))_t)$ , with $h$ strictly increasing in its profit argument when category totals are fixed. Its robust score is $R^f(A,U)=\min_{d\in U}f(A,d)$ for an uncertainty set $U$ of nonnegative demand vectors. This includes maximum profit and scores that subtract a demand-based benchmark from profit (Wang, Wang and Zhang 2020, §2.2).

A set is part-wise independently symmetric when it is a Cartesian product of its category projections and remains unchanged if products are permuted within any category. The perturbation version applies that property to $E=\{d-\mu:d\in U\}$ for a fixed centre $\mu$ . Such sets preserve the high/low distinction while treating products within each class interchangeably (Wang, Wang and Zhang 2020, Definitions 2.1–2.2).

Formalization targets

Alternate-chain optimality

In the target system there are $2k$ plants and $2k$ products, $k\ge1$ , with unit plant capacities and exactly $k$ products in each of two margin classes $0<P_L<P_H$ . A long chain places the fixed products in any cyclic order and connects each plant to two consecutive products. An alternate long chain places high- and low-margin products alternately. The goal, Theorem 3, says that for every such pair of chains, every part-wise independently symmetric $U$ , and every robust score in the class above,

R^f(\mathrm{AL},U)\ge R^f(L_{HL},U).

This is the paper's worst-case comparison, rather than a claim about a single demand instance or a single performance measure (Wang, Wang and Zhang 2020, Theorem 3, p. 21).

Margin-group comparisons

The paper defines a dual margin group index $\delta^K_\mu(A)$ by an integer program that assigns product dual values from the finite menu $\beta_{tr}=P_t-P_r$ , where $P_0=0$ . The parameter $K$ counts how many products in each category receive each nonzero menu value. Its feasible set is $Q$ . Theorem 1 expresses every robust score in terms of these indices and residual demand vectors; Theorem 2(a) says that index dominance for every $K\in Q$ implies robust-score dominance. Lemma 2 evaluates the index of an alternate chain in three cases, and Proposition 1 compares it with every long chain (Wang, Wang and Zhang 2020, pp. 17–22). These are the mission's milestones, alongside the profit LP's duality and two cyclic-window statements used in the comparison.

What the result provides

Within balanced, unit-capacity, two-margin long chains, the theorem resolves placement of the high-margin products without choosing one demand distribution or one profit-based robustness score. The dominance holds across the paper's whole class of category-symmetric uncertainty sets and scores. It gives a design rule within that family; it does not claim that an alternate chain beats every possible two-capability graph. The paper separately studies limits of that broader comparison (Wang, Wang and Zhang 2020, §4.3).

The paper proves these results on paper. This mission asks for machine-checked proofs of the stated Lean targets. Its reusable output includes the finite bipartite profit LP, its dual, category-wise demand symmetry, and the DMGI representation. None of the mission's theorems is presented here as already machine-checked.

Where the formal proof is difficult

The LP optimum must be related to a dual optimum whose product variables belong to a small, margin-dependent set. That is stronger than merely invoking an objective-value duality statement. The robust representation then has to account for both a discrete assignment of dual values and the permissible permutations of demand residuals within each product class. The last comparison is combinatorial: a general long chain can have runs of high-margin products, and its relevant cyclic windows must be compared with the alternating chain across every feasible count vector $K$ (Wang, Wang and Zhang 2020, Appendix A).

Formalization scope

The Lean development represents plants and products by finite index types, real capacities, demands and margins, and a design by a finite set of plant–product pairs. A separate general profit-LP definition is instantiated by the paper's margin-category system. Lean indices start at zero: category $t$ is the paper's category $t+1$ , and the added margin level $P_0$ is zero. The production variable is written x j i in Lean for the paper's $x_{ij}$ . Category residuals are enumerated by increasing product index; part-wise symmetry makes that choice immaterial. A long chain uses a permutation of fixed products around a cycle, so the uncertainty set stays attached to the same high- and low-margin categories.

The system requires positive numbers of plants, products and occupied margin categories, nonnegative capacities, and positive strictly increasing margins. The paper treats margins as positive profits but does not state that inequality explicitly. The model also supplies $z_j\ge0$ to the DMGI program, matching the dual program and the use of dual feasibility in the paper's proof; equations (4) and (5) omit this line. For the robust minimum, $U$ is nonempty, compact and contained in nonnegative demand, and the deterministic score is continuous there. Nonemptiness and compactness are explicit mathematical additions needed for the paper's minimum and minimizer. Every DMGI theorem restricts $K$ to $Q$ . These conditions prevent empty or unbounded real infima from supplying Lean's default zero. The $k=1$ case is included.

Contributions may establish the LP duality, dual extreme-point structure, robust representations, exact alternate-chain index, or cyclic-window comparison. The definitions use finite sums and real suprema and infima; establishing attainment is part of the theorem work.

Selected references

S. Wang, X. Wang and J. Zhang, Robust Optimization Approach to Process Flexibility Designs with Contribution Margin Differentials, Manufacturing & Service Operations Management, 2020. SSRN author version 3233721, 22 May 2020; DOI.

12 thms1 active userReviewed

Operations Research·Captain: mikedeng1

Timing It Right: Balancing Inpatient Congestion vs. Readmission Risk at Discharge: Discharge a Patient Type Only After Every Strongly Dominating Type of No Shorter StayResearch Paper

Who to discharge from a congested ward

Every day a hospital ward with a fixed number of beds decides which patients go home. Sending a patient home early frees a bed for the next admission, which matters when the ward is congested and arrivals board in the emergency department or elective surgeries are cancelled. Sending a patient home too early raises the chance that the patient is readmitted, which is costly for the patient and, under the U.S. Hospital Readmissions Reduction Program, for the hospital. Shi, Helm, Deglise-Hawkinson and Pan (SSRN 3202975; Operations Research 2021, doi:10.1287/opre.2020.2044) model this trade-off as a Markov decision process over a census of patients indexed by class and length of stay (LOS), fit personalized readmission-risk curves to hospital data, and implement the resulting discharge policy at a partner hospital.

The structural question behind their policy is who to discharge first. Hospitals usually rank patients by their current, absolute readmission risk. The paper's Theorem 2 (p. 15) instead ranks types by how fast that risk falls with a further day of stay: a type whose risk curve is flatter from now on should be discharged before a type whose risk is still dropping quickly. This mission formalizes that ranking result, in a corrected form.

Setting

There are $M$ patient classes and a maximum length of stay $J$ . A type is a pair $(m,j)$ of a class and a LOS $j\in\{0,\dots,J\}$ . A state $X=(X^{m,j})$ counts the patients of each type, and the census is $S=\sum_m\sum_j X^{m,j}$ . A discharge action $D=(D^{m,j})$ counts the patients of each type sent home. Class $m$ has a minimum LOS $\underline L_m\in[0,J]$ , and an action is feasible at $X$ when $0\le D^{m,j}\le X^{m,j}$ (3), $D^{m,j}=0$ for $j<\underline L_m$ (4), and every patient at LOS $J$ leaves.

Between two daily decision epochs $k$ and $k+1$ , new patients and readmitted patients arrive at LOS $0$ , and every patient who was not discharged ages by one day: $X^{m,0}_{k+1}=A^{m,0}_k+A'^{m,0}_k$ (5) and $X^{m,j}_{k+1}=X^{m,j-1}_k-D^{m,j-1}_k$ (6). Each epoch costs the holding cost $c_h(X)=C\,(S-N)^+$ for $N$ beds (7), plus the discharge cost $c_d(D)=\sum_{m,j}D^{m,j}\,R\,r(m,j)$ (8), where $r(m,t)$ is the readmission risk of a class- $m$ patient discharged at LOS $t$ and $R\ge0$ is the readmission penalty. Each risk curve $r(m,\cdot)$ is continuously differentiable and nonincreasing in the LOS.

Strong dominance (Definition 1, p. 14): $(m_1,t_1)\succ(m_2,t_2)$ iff

\Bigl|\frac{\partial r(m_1,t_1+t)}{\partial t}\Bigr|\le\Bigl|\frac{\partial r(m_2,t_2+t)}{\partial t}\Bigr|\qquad\forall t\ge0.\tag{15}

Writing $e_{(m,t)}$ for one discharge of type $(m,t)$ , a schedule $(D_k)$ with trajectory $(X_k)$ over a horizon $H$ has total cost $V(D)=\sum_{k<H}[c_h(X_k)+c_d(D_k)]+c_h(X_H)+c_d(X_H)$ .

Formalization targets

Goal: Theorem 2, corrected

For an initial state, an arrival path and a horizon $H$ , let $(m_1,t_1)\ne(m_2,t_2)$ with $(m_1,t_1)\succ(m_2,t_2)$ , $t_2\le t_1$ and $\underline L_{m_1}\le t_1$ . Then every feasible schedule $D$ has a feasible schedule $D'$ with $V(D')\le V(D)$ such that, for all $k<H$ ,

D'_k\cdot e_{(m_2,t_2)}>0\ \Longrightarrow\ D'_k\cdot e_{(m_1,t_1)}=X'_k\cdot e_{(m_1,t_1)}.

Since the feasible schedules are finitely many, some optimal schedule discharges a $(m_2,t_2)$ patient only after all $(m_1,t_1)$ patients.

Milestones

Proposition 2 (p. 15): for $k'>k$ , $c_d(D_k+e_{(m_1,t_1)})-c_d(D_{k'}+e_{(m_1,t_1+k'-k)})\le c_d(D_k+e_{(m_2,t_2)})-c_d(D_{k'}+e_{(m_2,t_2+k'-k)})$ .
Census invariance (proof of Theorem 2, p. 16): swapping the discharge epochs of one $(m_1,t_1)$ patient and one $(m_2,t_2)$ patient leaves the census unchanged at every epoch.
Cost identity and inequality (proof of Theorem 2, p. 16): the swapped schedule is feasible, its total-cost difference equals the four discharge-cost terms displayed in the proof, and $V^{\pi_2}-V^{\pi_1}\le0$ .

Significance

Theorem 2 is the paper's main structural result. It turns a high-dimensional MDP, whose state is a census over $M(J+1)$ types, into a ranking problem: once types are ordered by strong dominance, the remaining decision is how many patients to discharge (Corollary 1, p. 16), which the paper then approximates with a univariate linear-quadratic heuristic (§5). The ranking also has a direct operational reading: discharge by marginal, not absolute, readmission risk.

No machine-checked version of this result exists. Formalizing it settles exactly which hypotheses the interchange argument needs. Doing so already exposed that the statement as printed is false (see Difficulty), so the mission's output is the corrected theorem with a checked proof, together with a reusable finite-horizon, pathwise model of class-by-LOS patient flow.

Difficulty

The obvious argument is a single interchange: if a $(m_2,t_2)$ patient is discharged at epoch $k$ while a $(m_1,t_1)$ patient stays until a later epoch $k'$ , swap their discharge epochs. The census path does not change, and Proposition 2 shows the discharge cost does not increase. The step that fails is the one the paper defers to Appendix B.3: the dominated patient, kept from $k$ to $k'$ , may pass the maximum LOS $J$ before $k'$ , and then the swap is not available. The appendix's repair does not close the gap. With $J=3$ , $N=1$ , $C=1000$ , $R=1$ , no arrivals, $r(1,j)=10-j$ , $r(2,j)=10-2j$ and one $(1,0)$ and one $(2,2)$ patient on day $0$ , we have $(1,0)\succ(2,2)$ , yet the unique optimum discharges the $(2,2)$ patient alone (cost 1013), and every schedule that obeys the rule costs at least 1014. The added hypothesis $t_2\le t_1$ guarantees that the dominated patient can wait as long as the dominating one, so the swap always exists.

The remaining difficulty is bookkeeping: the interchange changes two cohorts by $\pm1$ over an interval of epochs, and feasibility (counts, minimum LOS, forced exit at $J$ ) must be checked along the new trajectory. Repeated interchanges must also be ordered so that fixing one epoch does not break an earlier one.

Formalization scope

Model. Classes are Fin M, LOS indices Fin (J+1), counts natural numbers, costs real numbers. Epochs start at $0$ . Arrivals, new and readmitted, form one exogenous deterministic path, as Remark 4 (p. 12) prescribes for §4. Every statement is pathwise on a finite horizon $H$ , the setting of the paper's interchange argument. The long-run average cost (9) is not used, since a finite interchange cannot change it.
Conventions added. Patients at LOS $J$ must leave, since (6) has no LOS $J+1$ . The total cost charges every patient present at the horizon as if discharged at their current LOS, so that holding a patient to the end is not free. The risk curves are $C^1$ and nonincreasing on $[0,\infty)$ (p. 15), and $R\ge0$ . Strong dominance uses Mathlib's deriv with the absolute values of (15).
Correction to Theorem 2. The goal adds $t_2\le t_1$ (the printed statement is false, as shown above), $(m_1,t_1)\ne(m_2,t_2)$ (strong dominance is reflexive, so the rule would otherwise demand every type be fully discharged once any is), and $\underline L_{m_1}\le t_1$ (otherwise $(m_1,t_1)$ patients can never be discharged). "The optimal action" becomes "some no-costlier feasible schedule obeys the rule": with ties an optimal schedule may break it.
Ruling out trivial readings. The goal quantifies over feasible schedules with the real costs (7)–(8), and the rule is required at every epoch $k<H$ along $D'$ 's own trajectory. Taking $D'=D$ does not suffice in general, and a schedule that avoids discharging $(m_2,t_2)$ by letting patients vanish is excluded by the forced exit and the terminal valuation.
Infrastructure. One definitions file holds the model, strong dominance, unit actions and the interchange. Mathlib's fundamental theorem of calculus (intervalIntegral.integral_eq_sub_of_hasDerivAt) and monotonicity of integrals are the analytic substrate for Proposition 2. The trajectory and interchange lemmas about class-by-age cohorts are reusable for other census models. Proofs of any milestone are welcome independently.

Not formalized: Theorem 1 (existence of an average-cost optimal policy), Corollary 1 (threshold form), Propositions 1 and 3, and Lemma 1.

Selected references

P. Shi, J. E. Helm, J. Deglise-Hawkinson, J. Pan, Timing it right: balancing inpatient congestion versus readmission risk at discharge, SSRN working paper 3202975, version of 2019-08-26. https://ssrn.com/abstract=3202975
P. Shi, J. E. Helm, J. Deglise-Hawkinson, J. Pan, same title, Operations Research, 2021 (published version; not the citation basis of this mission). https://doi.org/10.1287/opre.2020.2044

5 thms1 active userReviewed

Convex Optimization Numerical Analysis Operations Research·Captain: mikedeng1

Approximate Parametric Computation of Minimum-Cost Flows with Convex Costs: Linear Splines of the Marginal Costs with Bounded Step Sizes Give an (α, β)-Approximate Minimum-Cost Flow FunctionResearch Paper

Motivation

Flow networks model the movement of material, traffic, electricity, or gas through connected systems. In many such models, the required net flow at each vertex varies with a parameter, so the object of interest is a whole family of optimal flows rather than one solution. When edge costs are nonlinear, solving a new optimization problem for every parameter value gives no finite description of that family. Joachims, Klimm and Warode study two approximations of this parametric problem: one approximates each edge's marginal cost, and the other interpolates selected optimal flows. This mission concerns their marginal cost approximation result, Theorem 5.

The paper builds on an exact method for piecewise quadratic edge costs by Klimm and Warode. A piecewise linear approximation of each marginal cost has a piecewise quadratic integral, so it brings general convex costs into the class handled by that method. The question is how fine the linear interpolation mesh must be for the resulting flows to be close to optimal under the original costs. The paper gives local step size bounds involving the second derivative of each marginal cost. The target here is a corrected version of that guarantee, with the precise corrections stated below.

Setting

A network consists of finite sets of vertices $V$ and edges $E$ . Every edge has a tail and a head. The graph is strongly connected and has neither self loops nor parallel directed edges. For an edge flow $x\in\mathbb R^E$ , its net inflow at a vertex is the sum of flows entering that vertex minus the sum leaving it. Two balanced demand vectors $b^0,b\in\mathbb R^V$ determine a demand $b^0+\lambda b$ for $\lambda\in[0,\lambda^{\max}]$ . A flow is feasible when its net inflow equals that demand. In the directed case all edge flows are nonnegative; in the undirected case their signs are unrestricted.

Each edge $e$ has a marginal cost $f_e:\mathbb R\to\mathbb R$ that is strictly increasing, differentiable, nonpositive on negative arguments, and nonnegative on positive arguments. Its edge cost is $F_e(x)=\int_0^x f_e(s)\,ds$ . The total cost is the sum of edge costs, and $C(\lambda)$ is the minimum total cost of a feasible flow at parameter $\lambda$ . These sign conditions make the edge costs nonnegative. The paper calls them homogeneous marginal costs, although this is a sign condition rather than algebraic homogeneity. Section 5.2 gives the model and its approximation criterion.

For each edge, choose a strictly increasing mesh from $-x^{\max}$ to $x^{\max}$ , where

x^{\max}=\max_{0\le\lambda\le\lambda^{\max}}\frac12\sum_{v\in V}|b_v^0+\lambda b_v|.

The linear spline $s_{f_e}$ joins the values of $f_e$ at adjacent mesh points by straight chords. The minimum cost flow function $\widetilde x(\lambda)$ for these spline marginal costs is tested under the original costs: $\widetilde C(\lambda)=\sum_e F_e(\widetilde x_e(\lambda))$ . This convention is essential because a small optimal cost for the spline instance alone says nothing about the cost under $f_e$ .

Formalization targets

The milestones follow the paper's argument in order.

Edge-flow bound (§5.2.1, p. 16): every optimal edge flow satisfies $|x_e(\lambda)|\le x^{\max}$ .
Equation (17) (proof of Lemma 4, p. 16): the closeness condition (15) of marginal costs on $[-x^{\max},x^{\max}]$ gives

\frac{2}{1+\alpha}F_e(x)-\frac{\beta}{(1+\alpha)m}\le\widetilde F_e(x)\le\frac{2\alpha}{1+\alpha}F_e(x)+\frac{\beta}{(1+\alpha)m}.

The (16) case (proof of Lemma 4, p. 17): $|\widetilde f_e|\ge|f_e|$ and (16) give $F_e\le\widetilde F_e\le\alpha F_e+\beta/m$ .
Lemma 4 (p. 16): uniform control of $|\widetilde f_e-f_e|$ on $[-x^{\max},x^{\max}]$ in the sense (15) or (16) makes the minimum-cost flow function of the $\widetilde f$ instance an $(\alpha,\beta)$ -approximation.
Equation (18) (p. 17): the interpolation estimate

|f(x)-s_f(x)|\le\frac18\delta_i^2\max_{\xi\in[x_i,x_{i+1}]}|f''(\xi)|.

Spline domination under (ii) (proof of Theorem 5, p. 18): $|s_{f_e}(x)|\ge|f_e(x)|$ on $[-x^{\max},x^{\max}]$ .
Endpoint maximum under (ii) (proof of Theorem 5, p. 18): $\max_{[x_i,x_{i+1}]}|f_e''|=\max\{|f_e''(x_i)|,|f_e''(x_{i+1})|\}$ .

The goal is the corrected Theorem 5. It states that either of the paper's two explicit step size regimes, involving $\alpha>1$ , $\beta\ge0$ , $m=|E|$ , and $x^{\max}$ , makes the spline instance's minimum cost flow function satisfy

\widetilde C(\lambda)\le\alpha C(\lambda)+\beta\qquad(0\le\lambda\le\lambda^{\max}).

The first regime bounds each step by a local maximum of $|f_e''|$ and the magnitude of $f_e$ at a mesh endpoint. The second adds monotonicity and sign conditions on $f_e''$ and uses its endpoint values. The formal theorem retains the constants $2\sqrt2$ , the factor $1/8$ in (18), and both distinct denominators in Theorem 5. Theorem 5, pp. 17–18 is the source for the exact formulas.

Significance

The guarantee applies to an entire interval of demand parameters. It converts local numerical accuracy of the marginal cost splines into a bound on the original total cost at every parameter value, while preserving feasibility. The edge flow bound explains why it suffices to approximate marginal costs on a finite interval even when edge flows are otherwise real valued.

The paper proves the intended result by a paper argument, but its printed Theorem 5 has a counterexample when a mesh crosses zero without including zero: the spline can lose the marginal cost sign condition, and at zero demand the spline optimum can have positive original cost while the true optimum has cost zero. The corrected goal records a valid target for machine checked proof. Formalizing it also yields reusable definitions of finite flow networks, convex separable edge costs, parametric approximation, and chord splines. No machine checked proof of this theorem is claimed by this mission.

Difficulty

Pointwise closeness of marginal costs does not directly compare the two optimized flows, which may differ on every edge. A direct comparison at the spline optimum must also account for the original optimum and for how the edge costs accumulate across the network. The interpolation estimate alone does not settle this: a mesh interval crossing zero can change the sign of its chord at zero, even when every step size bound in the printed theorem holds. The shape condition in Theorem 5(ii), read literally with the third differentiability assumption, also forces the second derivative to vanish on the negative half line. The mission keeps that condition as printed rather than silently replacing it with a more symmetric one.

Formalization scope

Lean represents vertices and edges by finite types, net inflow by finite sums, and each edge cost by a real interval integral based at zero. A Boolean flag selects the directed case with $x_e\ge0$ or the undirected case with no sign constraint. The general finite lower and upper bounds of problem (14) are outside this mission. The optimal cost is the real infimum of feasible costs; the graph and balanced demand assumptions give feasible flows, and the sign assumptions bound their costs below. The spline is computed from its mesh values, with its end chords extended linearly outside $[-x^{\max},x^{\max}]$ . Meshes are indexed from zero in Lean, regardless of the paper's two indexing styles.

The corrected Theorem 5 requires zero to be a mesh point on every edge. In regime (i), it replaces $|f_e(x_i)|$ by $\min\{|f_e(x_i)|,|f_e(x_{i+1})|\}$ . In regime (ii), both entries of the factor $B$ are square roots of $|f_e''|$ ; this matches the equality $B^2=\max\{|f_e''(x_i)|,|f_e''(x_{i+1})|\}$ used in the printed proof. Lemma 4 and Theorem 5 explicitly require $x^{\max}>0$ , since both step-size bounds and (15), (16) divide by it (with zero demands, a one-point mesh and $\beta=0$ , Theorem 5 would otherwise fail), and its second marginal cost family is continuous, strictly increasing, and sign preserving. These conventions and corrections are recorded in the source analysis for Theorem 5.

A proof must use the chord spline determined by $f_e$ and the mesh; replacing it by an arbitrary close function would discard the numerical claim. Likewise, the bound $|\widetilde x_e(\lambda)|\le x^{\max}$ is never a hypothesis of Lemma 4 or of the goal: it is milestone 1, and assuming it would remove the combinatorial half of the argument. Milestone 6 is stated on $[-x^{\max},x^{\max}]$ rather than on all of $\mathbb R$ as printed, because the linearly extended end chord of a convex function lies below it. Contributions to the flow bound, Lemma 4, the spline estimate, or the final connection between them are all within scope. The flow and spline definitions can also support other approximation results beyond this theorem.

Selected references

Per Joachims, Max Klimm and Philipp Warode, Approximate Parametric Computation of Minimum-Cost Flows with Convex Costs, arXiv preprint, 2022. arXiv:2203.13146v1.
Max Klimm and Philipp Warode, Parametric Computation of Minimum-Cost Flows with Piecewise Quadratic Costs, Mathematics of Operations Research, articles in advance, 2021. DOI:10.1287/moor.2021.1151.

10 thms1 active userReviewed

Control Theory Operations Research·Captain: mikedeng1

Managing Self-Replicating Innovative Goods: Characterization of the Optimal Production and Sales Policies under Strong ReplicabilityResearch Paper

Why self-replicating goods

Some goods can only be made by copies of themselves. RepRap and Prusa 3D printers print the parts of new printers, seed stock is grown from seed, and livestock herds breed. For such a good the inventory is also the production capacity: a unit sold today is a unit that will not replicate tomorrow. A firm launching such a good has to decide, at every instant, how much of its stock to use for replication and how much demand to serve. Demand for an innovative good is not exogenous either. It diffuses through the market by word-of-mouth, so sales held back today also slow future demand.

B. Hu and Z. Sun (Management Science) model this as a deterministic optimal control problem. Their demand side is the Bass diffusion model (Bass, 1969) in the supply-constrained form of Ho, Savin and Terwiesch (2002) and Kumar and Swaminathan (2003), where cumulative sales rather than cumulative demand drive imitation. Hu and Sun add diminishing word-of-mouth. Their main structural result, Theorem 1, says that under a condition they call Strong Replicability the optimal policy switches only once and can be found by a one-dimensional search.

The model

Time runs over $[0,T]$ , where $T$ is the life cycle. The firm controls a production rate $p(t)$ and a sales rate $s(t)$ . The state consists of the cumulative demand $D(t)$ , the adjusted cumulative sales $S(t)$ and the inventory $I(t)$ . The demand rate is

d(t)=\Big[\alpha+\frac{\beta S(t)}{m}\Big]\big[m-D(t)\big],

where $m$ is the market size, $\alpha$ the coefficient of innovation and $\beta$ the coefficient of imitation. Problem (1) of the paper is

\max_{p,s}\int_0^T\big[\pi s(t)-cp(t)-hI(t)\big]e^{-\rho t}\,dt

subject to

D'=d,\quad S'=s-wS,\quad I'=p-s,\qquad 0\le p\le rI,\quad 0\le s\le d,\quad I(T)\ge0,

D(0)=S(0)=0,\qquad I(0)=I_L>0.

Here $\pi$ is the price, $c$ the unit replication cost, $h$ the holding cost rate, $r$ the replication rate, $\rho\ge0$ the discount rate and $w\ge0$ the rate at which word-of-mouth decays. Unmet demand is lost. The paper assumes $\pi>c$ and $r>\rho$ . Production is on when $p=rI$ and off when $p=0$ . Sales are on when $s=d$ and off when $s=0$ .

Strong Replicability is condition (2),

(r-\rho)\pi>cr+h.

It says that letting a unit replicate for a short time and selling the offspring later is worth more than selling the unit now.

Two levels of the launch inventory organise the answer. $\underline I$ is the level at which keeping production and sales always on depletes the inventory exactly at $T$ . $\overline I$ is the level at which keeping production off and sales on depletes it exactly at $T$ .

Formalization targets

Goal: Theorem 1

Assume Strong Replicability. Then:

(a) if $I_L<\underline I$ , the policy that keeps production always on and switches sales on once, at the time that depletes the inventory exactly at $T$ , is optimal;
(b) if $\underline I<I_L<\overline I$ , the policy that keeps sales always on and switches production on once, at the time that depletes the inventory exactly at $T$ , is optimal;
(c) if $I_L>\overline I$ , the policy that keeps sales always on and production off is optimal, and it leaves inventory at $T$ .

In each case, optimal means that the profit is at least

\int_0^T\big[\pi\tilde s-c\tilde p-h\tilde I\big]e^{-\rho t}\,dt

for every admissible trajectory $(\tilde D,\tilde S,\tilde I,\tilde p,\tilde s)$ , not only for policies of the stated shape. The switching times are not given in closed form, and the theorem asserts only that they exist.

Milestones

The thresholds are ordered, $\underline I<\overline I$ (preamble of Theorem 1).
Proposition 1. Once production is switched on, an optimal policy keeps it on until $T$ or inventory depletion.
Proposition 2, first half. Under Strong Replicability, every optimal trajectory has $I(t)>0$ for all $t<T$ , whatever $T$ is.

Significance

Theorem 1 turns an infinite-dimensional control problem into a choice of one switching time. Its managerial content is that a firm with a replicating good should, when stock is scarce, run replication at full capacity and hold back sales, losing some early customers, as long as the stock built up will eventually be sold. Proposition 2 says that under Strong Replicability the firm never sells out before the end of the life cycle. The paper's numerical study (§4) and its extensions (§5: backlogged demand, liquidity, stochastic diffusion) are built on this characterization.

The result has a published informal proof (pp. 36–37 of the manuscript), which applies necessary conditions from Pontryagin's maximum principle and then a perturbation and exchange argument. None of it is machine-checked. A complete formal proof would establish global optimality, against all integrable controls, for a nonlinear controlled ODE with mixed state–control constraints. That is a sufficiency statement, which the necessary conditions alone do not give.

Difficulty

The maximum principle gives necessary conditions only, and Problem (1) is not concave: the dynamics of $D$ are bilinear in $S$ and $D$ , and the constraint $p\le rI$ couples control and state. So the obvious route, solving the Pontryagin system and reading off the optimum, does not prove optimality. The paper's own argument is an exchange argument. It postpones sales or shifts production forward and claims each change improves profit, and it applies the change recursively ("by making the same argument recursively"). Making it rigorous requires comparison results for the Bass system under perturbed sales, which are delicate. Postponing sales lowers the adjusted sales $S$ , and with it all future demand. The existence of the switching times also needs a continuity argument on the depletion time as a function of the switch.

Formalization scope

The Lean development lives in the namespace SelfReplic.Strong and uses real numbers throughout.

Parameters form a structure Params with fields m, price, c, h, r, alpha, beta, rho, w, T, IL. The predicate Params.Standing collects the page's assumptions $I_L>0$ , $\pi>c$ , $r>\rho\ge0$ , $w\ge0$ . It adds the sign conditions $m>0$ , $T>0$ , $\alpha>0$ , $\beta\ge0$ , $c\ge0$ , $h\ge0$ , which the paper uses but never states. Params.StrongRepl is condition (2).
Admissible trajectories (IsAdmissible) have integrable controls $p,s$ and continuous states $D,S,I$ on $[0,T]$ . The three ODEs hold in integral form at every $t\in[0,T]$ , the constraints $0\le p\le rI$ , $0\le s\le d$ hold at every $t\in[0,T]$ , and $I(T)\ge0$ . The integral form is used because bang-bang controls are discontinuous. Continuity and integrability prevent any integral from silently taking Lean's default value $0$ . Nonnegativity of $I$ follows from $0\le p\le rI$ , as on p. 8.
Optimality (IsOptimal) compares the discounted profit with every admissible trajectory of the same parameters.
Policy shapes are pointwise statements on $[0,T]$ , and a switch instant counts as "on". The thresholds $\underline I,\overline I$ enter as real numbers with their defining property (IsLowLevel, IsHighLevel), evaluated at the same parameters with $I_L$ replaced.
Proposition 1 is read up to null sets ("production has run before $t_0$ ", conclusion almost everywhere). It carries the added hypothesis $\rho c+h>0$ , which the paper's proof uses. Without it ( $\rho=h=0$ ), pausing production is costless and the statement fails.

A formalization that states Theorem 1 inside its own policy class (the best policy of shape (a) is the best of shape (a)) would be empty. Here the competitor in every case ranges over all admissible trajectories.

Not formalized: Theorem 2 (Weak Replicability), whose closed form (3) for the production interval is inexact when $\rho>0$ ; Corollaries 1–2; the second half of Proposition 2, which fails when $I_L\ge m$ ; the unnumbered bang-bang claim of p. 9; Propositions 3–4 (§5).

Contributions that would be reusable beyond this mission include existence and uniqueness for the controlled Bass system in integral form, a comparison lemma for $D$ and $S$ under pointwise-ordered sales, and a sufficiency (verification) theorem for bang-bang controls of problems that are linear in the control.

Selected references

B. Hu, Z. Sun, Managing self-replicating innovative goods, Management Science (doi:10.1287/mnsc.2020.3936); authors' manuscript of 2020-10-18. https://doi.org/10.1287/mnsc.2020.3936
F. M. Bass, A new product growth for model consumer durables, Management Science 15(5), 215–227, 1969. https://doi.org/10.1287/mnsc.15.5.215
T.-H. Ho, S. Savin, C. Terwiesch, Managing demand and sales dynamics in new product diffusion under supply constraint, Management Science 48(2), 187–206, 2002. https://doi.org/10.1287/mnsc.48.2.187.255
S. Kumar, J. M. Swaminathan, Diffusion of innovations under supply constraints, Operations Research 51(6), 866–879, 2003. https://doi.org/10.1287/opre.51.6.866.24918
S. P. Sethi, Optimal Control Theory: Applications to Management Science and Economics, 3rd ed., Springer, 2019. https://doi.org/10.1007/978-3-319-98237-3

5 thms1 active userReviewed

Operations Research·Captain: mikedeng1

Second-Order Optimality Conditions for Nonconvex Set-Constrained Optimization Problems: A Directional Second-Order Necessary Condition via the Lower Generalized Support FunctionResearch Paper

Motivation

Optimization problems often require a smooth objective to be minimized subject to membership in a set. When that set is convex, established second-order conditions describe how curvature of the objective and constraints limits a local solution. Complementarity constraints and related models lead to nonconvex constraint sets. The tangent sets needed for a second-order condition can then be nonconvex as well, so a condition expressed only through ordinary convex support functions does not cover the general case. Gfrerer, Ye, and Zhou study this setting and state a directional necessary condition that permits a nonconvex set and a directional form of metric subregularity. Their result is Theorem 2 of arXiv:1911.04076v2, on printed page 16.

The mission concerns the first of the paper's two approaches to second-order necessary conditions. It targets the theorem that uses a lower generalized support function. The paper also develops conditions through convex duality under a stronger directional qualification; those results have different hypotheses and are outside this mission's target. The theorem here is a proved mathematical result whose statement and supporting definitions remain to be formalized and proved in Lean.

Setting

Fix natural dimensions $n$ and $m$ . A problem $(P)$ consists of twice continuously differentiable maps $f:\mathbb R^n\to\mathbb R$ and $g:\mathbb R^n\to\mathbb R^m$ , together with a closed set $\Lambda\subseteq\mathbb R^m$ . Its feasible region is $F=\{x:g(x)\in\Lambda\}$ . A point $\bar x\in F$ is a local solution if no sufficiently nearby feasible point has a smaller value of $f$ .

For a set $S$ and a point $x\in S$ , the contingent cone $T_S(x)$ collects limits of directions of feasible displacements $x+t_kd_k\in S$ as $t_k\downarrow0$ . Given a direction $d$ , the outer second-order tangent set $T_S^2(x;d)$ collects limits of $w_k$ for displacements $x+t_kd+\tfrac12t_k^2w_k\in S$ . It can be empty and need not be convex. The regular normal cone $\widehat N_S(x)$ describes vectors whose inner product with nearby displacements into $S$ is negligible to first order. Limits of these normals form the limiting normal cone $N_S(x)$ ; restricting their approach to direction $d$ gives the directional limiting normal cone $N_S(x;d)$ .

The critical cone at $\bar x$ is $C(\bar x)=\{d:\nabla g(\bar x)d\in T_\Lambda(g(\bar x)),\;\nabla f(\bar x)d\le0\}$ . Directional metric subregularity requires an error bound near $\bar x$ within a neighborhood of the ray in direction $d$ : distance to $F$ is at most a positive constant times distance from $g(x)$ to $\Lambda$ . The neighborhood is precisely $\bar x+V_{\rho,\delta}(d)$ from Definition 6, including the zero direction.

The Lagrangian is $L(x,\lambda)=f(x)+g(x)^\top\lambda$ . A directional M-multiplier at $(\bar x,d)$ satisfies $\nabla_xL(\bar x,\lambda)=0$ and $\lambda\in N_\Lambda(g(\bar x);\nabla g(\bar x)d)$ . For a set $S$ and a subset $A$ , the lower generalized support function $\widehat\sigma_{S,A}(\lambda)$ is the lower limit, as $\widetilde\lambda\to\lambda$ , of the infimum of $\widetilde\lambda^\top u$ over $u\in A$ with $\widetilde\lambda\in N_S(u)$ . Write $\widehat\sigma_S$ when $A$ is the whole space. The paper's Definition 7 assigns $+\infty$ to the unrestricted function when $S$ is empty.

Formalization targets

Let $D=T_\Lambda^2(g(\bar x);\nabla g(\bar x)d)$ and let $A_{\mathrm{opt}}=\nabla g(\bar x)T_F^2(\bar x;d)+\nabla^2g(\bar x)(d,d)$ . The main target is Theorem 2, equations (17) and (18): if $\bar x$ is a local solution, $d\in C(\bar x)$ , directional metric subregularity holds along $d$ , and $D$ is nonempty, then one directional M-multiplier $\lambda$ works for every $A\supseteq A_{\mathrm{opt}}$ :

\widehat\sigma_{D,A}(\lambda)\le\nabla_{xx}^2L(\bar x,\lambda)(d,d).

The same multiplier gives the unrestricted conclusion $\widehat\sigma_D(\lambda)\le\nabla_{xx}^2L(\bar x,\lambda)(d,d)$ . The goal retains the order “there exists $\lambda$ such that for every $A$ .” The milestones state the paper's supporting results: the distance and outer-limit identity, the tangent and second-order tangent chain rules, their error bound and nonemptiness consequence, the primal second-order necessary condition, the critical-direction derivative condition, and the inclusion of limiting normals to a second-order tangent set.

Significance

The result supplies a directional dual necessary condition for a local minimizer without assuming that $\Lambda$ is convex. Its multiplier belongs to a directional normal cone, which can be smaller than the ordinary limiting normal cone. The set $A$ also lets the condition retain information about which second-order constraint perturbations arise from feasible displacements. The paper explains that taking $A=\mathbb R^m$ gives a more tractable but weaker condition, while $A_{\mathrm{opt}}$ gives the strongest member of this family on page 17.

A complete formalization would provide checked interfaces for second-order tangent sets, directional normals, directional metric subregularity, and lower generalized support. Those objects can be reused in later work on nonconvex constrained optimization. This mission supplies statements and definitions; the published mathematical argument still needs a Lean proof. The local draft's compilation checks statement well-formedness, not the theorems' truth.

Difficulty

At a local minimum, ordinary first-order information constrains derivatives along contingent directions. The second-order tangent set is harder: it may be empty, and even when the original set is convex it need not be convex. The usual convex-support interpretation therefore cannot simply be applied to it. In addition, the error bound for the original constraint system must remain valid in the second-order linearized setting before normal-cone information can be transferred. These are the substantive points represented by Proposition 5 and Lemma 3 in the milestone list.

Formalization scope

The Lean development uses EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), so both dimensions are finite and may be zero. The standing assumptions of $(P)$ are explicit: both maps are $C^2$ and $\Lambda$ is closed. The contingent and second-order tangent sets use positive sequences tending to zero; a monotonically decreasing sequence can be selected from one of these. Tangent sets and normal cones are empty when their base point is outside the underlying set, matching the domain stated in Definitions 1, 3 and 4. Second derivatives are Fréchet derivatives applied twice to $(d,d)$ . A local minimum is stated together with feasibility.

Distances to possibly empty second-order tangent sets or outer limits use extended nonnegative reals, with distance to the empty set equal to $+\infty$ . The lower generalized support function uses extended reals, where an empty infimum is $+\infty$ ; the goal compares its value with the real Hessian value embedded in that order. This expresses the paper's “Hessian minus support is nonnegative” without undefined extended-real subtraction. Directional metric subregularity requires positive constants and the exact neighborhood in Definition 6, including $0$ ; it cannot be satisfied by making that neighborhood empty. Likewise the lower generalized support function is computed from limiting normals and is not assigned a constant extreme value.

The paper's $t_k\downarrow0$ is represented by $t_k>0$ and $t_k\to0$ . The “modulus $\kappa$ ” in Proposition 5 is represented by an admissible constant in the defining error bound. Equations (11), (12), and Corollary 1 contain printed slips in the point or derivative notation; their Lean statements use $\bar x$ and $\nabla^2g$ as their surrounding formulas and proofs require. Equation (18) uses the same multiplier as (17), by taking $A$ to be the whole space. Contributions to the definitions, chain rules, error bound, normal-cone inclusion, and final theorem are all within scope.

Selected references

H. Gfrerer, J. J. Ye, and J. Zhou, Second-order optimality conditions for non-convex set-constrained optimization problems, arXiv:1911.04076v2, 2020; published in Mathematics of Operations Research, 2022. Pinned preprint.

11 thms1 active userReviewed

Economics Operations Research·Captain: mikedeng1

Contracting, Pricing, and Data Collection Under the AI Flywheel Effect: Under Moral Hazard the Firm Collects More (Less) Data Than First Best When the Data Impact Increases (Decreases)Research Paper

Motivation

Companies often sell a machine-learning product before its model has reached its final quality. Use of the product then yields data that can improve later versions. This feedback is the AI flywheel studied by Gurkan and de Véricourt. A firm may hire a specialist to develop the model, but the specialist's effort is costly and hidden. More customer data can then change both the product's future quality and the cost of inducing effort. The authors ask how that interaction changes the firm's price and data collection relative to a firm that develops the model itself. Their working paper reports that the direction depends on how the effect of effort varies with dataset size Gurkan and de Véricourt, 2021/2022.

The setting connects a pricing decision to an incentive decision. A lower price attracts more buyers and supplies more data for the next period, yet it also gives up current revenue. When a provider trains the model, the value of additional data depends on how data alter the provider's chance of producing a high-quality result under effort and under shirking. The theorem isolates that change through one ratio rather than requiring a particular parametric learning curve.

Setting

There are two periods and a unit mass of potential buyers in each. A buyer's sensitivity to algorithm accuracy is uniformly distributed on $[0,1]$ . The algorithm's accuracy is either $\alpha_h$ or $\alpha_\ell$ , where $0<\alpha_\ell<\alpha_h$ . Given a dataset of size $d$ , a provider who exerts effort produces high accuracy with probability $\pi_w(d)$ and pays cost $\kappa>0$ ; a provider who shirks produces it with the lower probability $\pi_s(d)$ and pays no effort cost. The firm observes accuracy and can condition payments on it, while effort itself is unobservable.

If the firm collects $\delta$ data at capacity $\nu>0$ , the buyer model gives period revenue

R_\nu(\delta,\alpha) =\alpha\frac{\delta}{\nu}\left(1-\frac{\delta}{\nu}\right), \qquad 0\le\delta\le\nu.

First-period sales add data to the initial dataset $d_0$ . When the first algorithm has low accuracy, the provider retrains it on $d_0+\delta_{1\ell}$ ; when accuracy is already high, no retraining is needed. The data impact

\rho(d)=\frac{\pi_w(d)-\pi_s(d)}{\pi_w(d)}

measures the relative effect of effort on the high-accuracy probability. The paper assumes $1/\rho$ is convex on the relevant data interval Gurkan and de Véricourt, §3.2.

The firm's contract selects four nonnegative payments, one for each accuracy outcome in each period, and two first-period data quantities, $\delta_{1h}$ and $\delta_{1\ell}$ . Its expected profit and two incentive constraints are Problem (6)–(9) in the working paper. The first-best benchmark fixes each payment at $\kappa$ and removes the incentive constraints. Write $\delta^*$ for the low-accuracy data quantity of an optimal contract and $\delta^{FB}$ for that of an optimal first-best plan.

Formalization targets

The main target is Theorem 1 of the working paper. For interior optimal prices, it compares the two global optima:

\begin{aligned} \rho\text{ constant} &\Longrightarrow \delta^*=\delta^{FB},\\ \rho\text{ strictly increasing} &\Longrightarrow \delta^*>\delta^{FB},\\ \rho\text{ strictly decreasing} &\Longrightarrow \delta^*<\delta^{FB}. \end{aligned}

Since price and purchased quantity move in opposite directions in this buyer model, collecting more data corresponds to charging less than the first-best price. The three cases cover equality, underpricing, and overpricing without fixing a learning-curve formula Gurkan and de Véricourt, Theorem 1.

The milestones follow the paper's stated results. Lemma 1 characterizes the last-period myopic quantity and revenue. Lemma 2 identifies the optimal accuracy-contingent payments when first-period data choices are fixed. Proposition 1 characterizes the unique optimal contract and its reduced data-choice objective; Proposition 2 gives the unique first-best plan and places its low-accuracy data quantity above the myopic quantity. Two claims in the proof of Theorem 1 record the weak comparison and the distinctness of interior optima under strict monotonicity.

Significance

The theorem specifies the direction of a distortion in a firm's choice of data collection. Its conclusion depends on the relative change in two learning curves, not merely on the fact that more data improve model accuracy. In the increasing-impact regime, the contracting firm collects more data than the first-best firm; in the decreasing-impact regime, it collects less. The result gives a qualitative comparison for pricing and data acquisition when algorithm development is outsourced Gurkan and de Véricourt, §4.2.

The result is proved in the source paper; the task here is to give its two-period model, contract constraints, and comparison a Lean proof. The definitions also provide a reusable small model of two-outcome, two-period moral hazard with limited liability. A complete development would let later statements about welfare, capacity, or alternative contracts reuse the same precise optimization problems. No existing platform definition matches this paper's model, and the draft theorem statements currently have compilation placeholders rather than machine-checked proofs.

Difficulty

The first obstacle is the contract itself. Payments in the second period affect the provider's expected continuation payoff and thereby the first-period incentive constraint, so choosing each period's payments independently does not describe Problem (6). The data choice changes the probability of later accuracy and the incentive cost at the same time. A direct comparison of the two full objective values does not determine whether $\delta^*$ lies above or below $\delta^{FB}$ ; the paper's comparison depends on how the data impact changes with $d$ . Strict inequalities also need interior optimal choices. At a boundary, two distinct objective functions can select the same endpoint even when $\rho$ is strictly monotone.

Formalization scope

The Lean development uses real-valued data sizes, payments, probabilities, and revenues. It represents the learning curves $\pi_w$ and $\pi_s$ as functions on $\mathbb R$ , with hypotheses restricted to $[d_{\min},d_{\max}]$ . Feasible data choices lie in $[0,\nu]$ , and $d_0+\nu\le d_{\max}$ keeps every evaluated learning-curve value inside the stated domain. The standard-uniform quantile is the identity on its support. The second-period value is the supremum of revenue over $[0,\nu]$ ; Lemma 1 supplies its attained maximum. Both contract and first-best optimality are global over their respective feasible sets.

The standing assumptions include positive effort cost and low accuracy, $0\le\pi_s(d)<\pi_w(d)<1$ , strictly increasing concave learning curves $\pi_w$ and $\pi_s$ , differentiability of both curves, and convexity of $1/\rho$ . Positive $\alpha_\ell$ and strict $\pi_w<1$ make the paper's uniqueness conclusions well posed. Differentiability is weaker than the twice-continuous differentiability mentioned in the source's later proofs. The paper's condition favoring effort in both periods motivates the chosen contracting problem; effort is already imposed by its two incentive constraints. Interiority of the optimal low-accuracy quantities is an explicit hypothesis of the comparison theorem, reflecting the paper's assumption that optimal prices neither cover nor exclude the entire market Gurkan and de Véricourt, §3.4 and EC.1.

The goal concerns optimal solutions of the full six-variable contract problem and the full first-best problem. Defining $\delta^*$ and $\delta^{FB}$ only as maximizers of the reduced one-variable objectives would omit the contract's incentive constraints. A complete proof needs real optimization on compact intervals, concavity and differentiability facts, and a precise account of the payment constraints. Contributions to those components and to the stated milestones fit this mission.

Selected references

Huseyin Gurkan and Francis de Véricourt, Contracting, Pricing and Data Collection under the AI Flywheel Effect, ESMT Working Paper 20-01 (R3), August 17, 2021; subsequently published in Management Science, 2022. DOI: 10.1287/mnsc.2022.4333. The theorem numbers and printed pages in this mission follow the working-paper PDF.

8 thms1 active userReviewed

Operations Research·Captain: mikedeng1

Promotion Optimization for Multiple Items in Supermarkets: Under Additively Separable Cross-Item Effects, All Higher-Order Promotion Contributions Vanish and App(2) = App(N)Research Paper

Motivation

Supermarkets run temporary price promotions on a large share of their assortment, and the choice of which item to discount, by how much and in which week is a recurring planning decision for category managers. Promotions on one item change the sales of the others: a discount on one brand of coffee draws customers away from a competing brand (substitution), while a discount on shampoo can raise the sales of conditioner (complementarity). Promotions also have effects over time, because customers who stockpile during a promotion buy less afterwards.

M. C. Cohen, J. J. Kalas and G. Perakis (SSRN 3061451; Management Science, 2021, doi:10.1287/mnsc.2020.3641) formulate the multi-item promotion problem as a nonlinear integer program and approximate it by a hierarchy of linear integer programs $\mathrm{App}(\kappa)$ , which add up the profit contributions of promoting up to $\kappa$ items together. Their single-item predecessor, Cohen, Leung, Panchamgam, Perakis and Smith (Operations Research, 2017), corresponds to $\mathrm{App}(1)$ . The main structural result of the multi-item paper, its Theorem 1, says that under a common separability assumption on demand the hierarchy collapses at level two.

Setting

There are $N$ items and a selling season of $T$ periods. The retailer has enough inventory to meet demand throughout the season, as assumed in §2.1, so inventory does not enter the model. Item $i$ has a price ladder $q^{i0},q^{i1},\dots,q^{iK^i}$ , where $q^{i0}=q^0$ is the regular price, common to all items, and the other points are promotion prices. A plan $\gamma$ chooses a level $\gamma^i_t\in\{0,\dots,K^i\}$ for every item and period; the price of item $i$ at period $t$ is $p^i_t=q^{i\gamma^i_t}$ . Item $i$ has unit costs $c^i_t$ and a memory $M^i$ , and its demand at period $t$ is a function

d^i_t\big(p^i_t,p^i_{t-1},\dots,p^i_{t-M^i},\mathbf p^{-i}_t\big)

of its own current and $M^i$ past prices and of the other items' current prices (Assumption 1: cross past prices do not enter). The total profit of a plan is

\mathrm{MPOP}(\gamma)=\sum_{i=1}^N\sum_{t=1}^T(p^i_t-c^i_t)\,d^i_t\big(p^i_t,\dots,p^i_{t-M^i},\mathbf p^{-i}_t\big),

and the problem (Multi-POP) maximizes it over plans satisfying the business rules: at most $L^i$ promotions of item $i$ , at most one promotion of item $i$ in any $S^i+1$ consecutive periods, at most $L_T$ promotions in total and at most $C_t$ in period $t$ .

A pattern $\sigma$ assigns a level $\sigma_i$ to each item; its support $S(\sigma)$ is the set of promoted items. The pure promotion vector $\mathbf p^\sigma_t$ uses $\sigma$ at period $t$ and the regular price everywhere else, and $\mathbf p^0$ is the all-regular plan. The coefficient of $\sigma$ at $t$ is the inclusion–exclusion sum

b^\sigma_t=\sum_{U\subseteq S(\sigma)}(-1)^{|S(\sigma)|-|U|}\,\mathrm{MPOP}\big(\mathbf p^{\sigma|_U}_t\big),

where $\sigma|_U$ keeps the levels of $\sigma$ on $U$ and is regular off $U$ . With one promoted item this is $b^{kj}_t=\mathrm{MPOP}(\mathbf p^{kj}_t)-\mathrm{MPOP}(\mathbf p^0)$ , equation (5); with two it is equation (6). The App(κ) objective of a plan is

\mathrm{MPOP}(\mathbf p^0)+\sum_{t=1}^T\sum_{\sigma:\,1\le|S(\sigma)|\le\kappa}b^\sigma_t\,\mathbf 1\{\gamma^i_t=\sigma_i\ \forall i\in S(\sigma)\},

which is equation (4) for $\kappa=2$ , and $\mathrm{App}(\kappa)$ maximizes it over the same feasible set.

Formalization targets

Goal: Theorem 1

Assume the cross-item effects are additively separable,

d^i_t\big(p^i_t,\dots,p^i_{t-M^i},\mathbf p^{-i}_t\big)=h^i_t\big(p^i_t,\dots,p^i_{t-M^i}\big)+\sum_{j\neq i}H^{ji}_t(p^j_t),\qquad(8)

for arbitrary functions $h^i_t$ and $H^{ji}_t$ . Then for every $2\le\kappa\le N$ and all business-rule data,

\mathrm{App}(\kappa)\text{ objective}=\mathrm{App}(2)\text{ objective at every plan},\qquad \operatorname{argmax}\mathrm{App}(\kappa)=\operatorname{argmax}\mathrm{App}(2).

This is the chain $\mathrm{App}(2)=\mathrm{App}(3)=\dots=\mathrm{App}(N)$ of the paper.

Milestones

The recursion before (16) (p. 38): for a nonempty support $S$ , $b^\sigma_t=\mathrm{MPOP}(\mathbf p^\sigma_t)-\mathrm{MPOP}(\mathbf p^0)-\sum_{\emptyset\ne U\subsetneq S}b^{\sigma|_U}_t$ , for any demand.
Locality (p. 37): the coefficient is the sum of item–period contributions, and under (8) with $|S|\ge2$ the contributions at periods other than $t$ and of unpromoted items are zero.
Order three, (15) (p. 37): under (8), every coefficient with three promoted items is zero.
All orders (pp. 37–39): under (8), every coefficient with at least three promoted items is zero.
The binary-IP remark (p. 14): if a function of binary variables is a sum of functions each depending on at most two variables, all its inclusion–exclusion coefficients of order at least three vanish.

Significance

The size of $\mathrm{App}(\kappa)$ grows like $N^\kappa$ in the number of pairwise, triple and higher variables, and $\mathrm{App}(N)$ has a variable for every subset of items. Theorem 1 shows that under (8) nothing is gained beyond $\mathrm{App}(2)$ , an integer program with a quadratic number of variables. Equation (8) covers the demand models used in practice that the paper cites, the log-linear model with linear cross terms and the linear cross-elasticities model. The rest of the paper's solution approach works with $\mathrm{App}(2)$ : integrality of its LP relaxation for substitutable items (Theorem 2), a rounding scheme and a parametric bound (§3); Theorem 1 is what makes $\mathrm{App}(2)$ the complete cross-item model under (8).

The result is proved in the paper; its appendix carries out the order-three case explicitly and the induction step in outline, with "the details … omitted for conciseness". No machine-checked proof is known to exist. A formal proof removes the omitted cancellations and isolates the combinatorial core (milestone 5), which is a fact about pseudo-Boolean functions useful beyond promotions.

Difficulty

The coefficients are signed sums of $2^{|S|}$ total profits over all $N$ items and $T$ periods, and each profit is a product of a price margin and a demand that depends on a window of past prices. The obvious idea, expanding the products directly, gives an unmanageable number of terms. Every contribution involving three or more promoted items has to cancel, including the contributions at later periods, which see a promotion only through the memory window, and the paper omits these cancellations in the general induction step. Without (8) the claim fails: the paper notes that for demand models violating it $\mathrm{App}(2)$ is not necessarily equal to $\mathrm{App}(N)$ , and a demand with a three-way cross term already has nonzero order-three coefficients.

Formalization scope

Lean namespace PromoMulti.PairwiseExact. Items are Fin N and periods Fin T, 0-based (period $t$ of the paper is index $t-1$ ); prices, costs and profits are real. A plan is a function assigning a level Fin (K i + 1) to each item and period, level 0 being the regular price $q^0$ ; this is the binary encoding $\gamma^{ik}_t$ with $\sum_k\gamma^{ik}_t=1$ . Prices before the first period are $q^0$ (the appendix evaluates $h^i_t(p^i_t,q^0,\dots,q^0)$ ); Theorem 1 holds for any fixed history. The paper's pairwise variables $\gamma^{k\ell ij}_t$ are separate binaries tied by the consistency constraints (7); for integral plans (7) forces them to be products, and the App(κ) objective uses that product directly. The paper writes $\mathrm{App}(\kappa)$ out only for $\kappa\le2$ ; for $\kappa\ge3$ the formalization uses the inclusion–exclusion extension of (4) with the general coefficient of p. 38. The demand receives the whole current price vector; (8) reads only the coordinates $j\ne i$ . The ladder order $q^{iK^i}<\dots<q^{i1}<q^0$ is not imposed, nor any monotonicity, linearity or sign of $h$ and $H$ : Theorem 1 uses none. The business rules are those of (Multi-POP); the inter-item rules 2, 3 and 5 of §2.2 are not part of it.

The coefficients are defined by the closed alternating sum and the App(κ) objective sums every pattern with $1\le|S|\le\kappa$ ; a formalization that defines App(κ) through pairs only, defines higher coefficients as zero, or defines coefficients by the recursion (16) makes the goal trivial and is ruled out. The goal does not claim that App(2) solves (Multi-POP), which is false when past prices matter.

A complete development needs finite inclusion–exclusion over Finset.powerset, the cancellation lemma of milestone 5 (reusable for any pseudo-Boolean or multi-level function that is a sum of low-arity terms), and the bookkeeping of which plan coordinates each item–period profit reads. Contributions of proofs of any milestone, of milestone 5 in greater generality, and of alternative arguments are welcome.

Selected references

M. C. Cohen, J. J. Kalas, G. Perakis, Promotion Optimization for Multiple Items in Supermarkets, Management Science, 2021; preprint SSRN 3061451. https://ssrn.com/abstract=3061451, https://doi.org/10.1287/mnsc.2020.3641
M. C. Cohen, N.-H. Z. Leung, K. Panchamgam, G. Perakis, A. Smith, The Impact of Linear Optimization on Promotion Planning, Operations Research 65(2), 2017. https://doi.org/10.1287/opre.2016.1573

7 thms1 active userReviewed

Missions

Vector Space Methods VII: Euler–Lagrange EquationsTextbook

Motivation

Setting

Formalization targets

Main goal: Euler–Lagrange equation

Milestones

Significance

Difficulty

Formalization scope

Selected references

Vector Space Methods VI: Pseudoinverse OperatorsTextbook

Motivation

Setting

Formalization targets

Adjoint and closed-range milestones

Normal equations and minimum-norm solutions

Pseudoinverse identities

Significance

Difficulty

Formalization scope

Selected references

Vector Space Methods IV: Minimum-Distance DualityTextbook

Motivation

Setting

Formalization targets

Norm-preserving extension and norming functionals

Closed-subspace double annihilator

Minimum-distance duality

Significance

Difficulty

Formalization scope

Selected references

Introduction to Linear Optimization VI: Farkas' Lemma and Separating HyperplanesTextbook

Introduction to Linear Optimization III: Fourier–Motzkin Elimination and Projections of PolyhedraTextbook

Introduction to Linear Optimization II: Existence and Optimality of Extreme PointsTextbook

A Primal-Dual Smoothing Framework for Max-Structured Non-Convex Optimization: The Framework Returns an ε-Near-Stationary Point Within an Explicit Number of IterationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

High-Dimensional Learning Under Approximate Sparsity with Applications to Nonsmooth Estimation and Regularized Neural Networks: Excess-Risk Bounds at S3ONC Solutions of MCP-Regularized M-EstimationResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 18)

Milestones (the paper's proof chain)

Significance

Difficulty

Formalization scope

Selected references

Dynamic Resource Allocation in the Cloud with Near-Optimal Efficiency: The Multiplicative Weight Algorithm Nearly Matches the Offline Dynamic Optimum's Work While Approximately Satisfying Every SLAResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 with the explicit constants of p. 10

Intermediate targets (milestones)

Significance

Difficulty

Formalization scope

Selected references

Stochastic Knapsack Revisited: The Service Level Perspective: Anticipative Policies Need at Most 2Δ More Capacity Than Adaptive Policies to Meet Type-I Service LevelsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5

The two halves: Theorems 3 and 4

Milestones inside the proofs

Significance

Difficulty

Formalization scope

Selected references

Risk Guarantees for End-to-End Prediction and Optimization Processes: The Excess Squared-Loss Risk Bounds the Squared Excess Optimality-Gap Risk, Scaled by the Squared Diameter of the Feasible SetResearch Paper

Motivation