Optimization

Convex Optimization·Captain: mikedeng1

On Conjugate Convex Functions: Conjugation Is a Symmetric Correspondence Between Lower Semicontinuous Convex FunctionsResearch Paper

Motivation

Convex duality in optimization rests on one transformation: to a convex function $f$ one associates the function $\varphi(\xi) = \sup_x(\Sigma x\xi - f(x))$ , which records, for each slope $\xi$ , the best affine lower bound of $f$ with that slope. Lagrangian duality, the duality theory of linear and conic programming, the analysis of first-order methods through smoothness and strong convexity of conjugates, and the dual representations of risk measures and divergences all read off properties of $f$ from properties of $\varphi$ . Each of these uses needs one fact: that the transformation loses no information, so that applying it twice returns $f$ .

That fact, for functions on $\mathbb R^n$ , is the theorem of W. Fenchel's five-page note On conjugate convex functions (Canad. J. Math. 1 (1949) 73–77). Its timeline:

1912. W. H. Young proves the inequality $ab \le F(a) + G(b)$ for a pair of mutually inverse increasing functions $F', G'$ of one variable (Proc. R. Soc. Lond. A 87, 1912).
1949. Fenchel defines the conjugate of a convex function on a convex subset of $\mathbb R^n$ , without any differentiability, and proves that conjugation is a symmetric correspondence on convex functions that are semi-continuous from below and whose domain is closed relative to the function (Fenchel 1949).
1965. J.-J. Moreau develops conjugation for convex functions with values in $(-\infty, +\infty]$ on a real Hilbert space, together with the proximal map (Bull. SMF 93, 1965); the biconjugation theorem in this generality is called the Fenchel–Moreau theorem.
1970. R. T. Rockafellar's Convex Analysis makes the conjugate the central object of finite-dimensional convex analysis (Princeton, 1970).

Setting

Points of $\mathbb R^n$ are $x = (x_1,\dots,x_n)$ , and $\Sigma x\xi = x_1\xi_1 + \dots + x_n\xi_n$ .

A standing pair $(G, f)$ consists of a set $G \subseteq \mathbb R^n$ and a real function $f$ defined in $G$ such that

$G$ is nonempty and convex;
$f$ is convex on $G$ : $f((1-\theta)x' + \theta x'') \le (1-\theta)f(x') + \theta f(x'')$ for $x', x'' \in G$ , $0 < \theta < 1$ ;
$f$ is semi-continuous from below on $G$ : $\liminf_{x \to x^*,\, x \in G} f(x) \ge f(x^*)$ for $x^* \in G$ ;
$G$ is closed relative to $f$ : $f(x) \to +\infty$ as $x \to x^*$ within $G$ , for every boundary point $x^*$ of $G$ not in $G$ .

$G$ need be neither open, nor closed, nor bounded. The paper writes the lower limit as a "lim" with a bar under it; the milestone texts write it $\lim_{x\to x^*}$ , and it always means $\liminf$ .

The conjugate pair of $(G, f)$ is

\Gamma = \{\xi \in \mathbb R^n : x \mapsto \Sigma x\xi - f(x) \text{ is bounded above on } G\}, \qquad \varphi(\xi) = \sup_{x \in G}\bigl(\Sigma x\xi - f(x)\bigr)\quad (\xi \in \Gamma).

The same construction applied to $(\Gamma, \varphi)$ gives the pair $(G^*, f^*)$ , with $f^*(x) = \sup_{\xi\in\Gamma}(\Sigma\xi x - \varphi(\xi))$ . An interior point of $G$ is a point of the relative interior of $G$ , its interior within its affine hull.

In Lean: IsClosedConvexPair G f, conjDomain G f $= \Gamma$ , conjFun G f $= \varphi$ , and $(G^*, f^*)$ is conjDomain (conjDomain G f) (conjFun G f), conjFun (conjDomain G f) (conjFun G f).

Formalization targets

Goal: Fenchel's theorem (§3, p. 75)

For every standing pair $(G, f)$ :

(\Gamma,\varphi) \text{ is a standing pair},\qquad \Sigma x\xi \le f(x) + \varphi(\xi)\ \ (x\in G,\ \xi\in\Gamma), \tag{5}

with equality for some $\xi \in \Gamma$ at every interior point $x$ of $G$ ;

G^* = G, \qquad f^*(x) = f(x)\ \ (x \in G);

and every standing pair $(\Gamma', \varphi')$ whose conjugate pair is $(G, f)$ equals $(\Gamma, \varphi)$ .

Milestones, in the order of the proof

(5), with no hypothesis on $(G, f)$ .
$\Gamma \ne \emptyset$ , and $\varphi(\xi) = \Sigma x^\circ\xi - f(x^\circ)$ for some $\xi\in\Gamma$ at each interior point $x^\circ$ .
$\Gamma$ and $\varphi$ are convex.
$\varphi$ is semi-continuous from below and $\Gamma$ is closed relative to $\varphi$ .
(6): $G \subseteq G^*$ and $f^* \le f$ on $G$ .
Two convex functions, semi-continuous from below on $G$ and equal at the interior points of $G$ , are equal on $G$ .
$f^* = f$ on $G$ .
(7): $\sup_{\xi\in\Gamma}(\Sigma\xi x^\circ - \varphi(\xi)) = \infty$ for every $x^\circ \notin G$ .

Significance

The theorem identifies, among convex functions on convex subsets of $\mathbb R^n$ , exactly the class on which conjugation is a bijection and an involution. It is the finite-dimensional base case of the Fenchel–Moreau theorem and underlies Fenchel's duality theorem for $\inf(f - g)$ , the conjugate-based optimality conditions of convex programming, and the inversion of gradients of conjugate differentiable convex functions (the paper's §6, the Legendre transformation). The pair form is also how the result is used in practice: the conjugate of a function finite on a set comes with an explicit domain $\Gamma$ , and the theorem says that domain determines and is determined by $G$ .

The result has been proved for 75 years. What a formalization adds is the theorem in Fenchel's own form: a real-valued function on an explicit convex domain rather than an extended-real function on all of $\mathbb R^n$ , the domain identity $G^* = G$ together with the identity of values, and the attainment of equality in (5) at relative-interior points. Machine-checked versions of biconjugation exist in other forms: for extended-real functions on Hilbert spaces, for finite convex functions on all of $\mathbb R^n$ , and for functions on a set with a closed restricted epigraph over continuous linear functionals. None of them states the domain identity or the attained equality, and none is in the paper's pair form.

Difficulty

Milestones 1, 3, 4 and 5 follow from the definition of the conjugate alone. The content sits in three places.

Supporting hyperplanes at relative-interior points. When $G$ is lower-dimensional, the topological interior of $G$ is empty, and a supporting hyperplane must be produced inside the affine hull of $G$ and then extended. Points that are interior to a segment of $G$ but on its relative boundary do not suffice.
Passing from the interior to the boundary of $G$ . Equality $f^* = f$ at interior points does not by itself give equality at boundary points of $G$ ; it needs semi-continuity from below of both functions and convexity along segments ending at the boundary point.
$G^* \subseteq G$ . Points outside the closure of $G$ and boundary points of $G$ not in $G$ behave differently: a boundary point cannot be separated from $G$ by a hyperplane, and the inclusion there depends on the condition that $G$ be closed relative to $f$ . Without that condition the inclusion is false: for $G = (0, 1]$ and $f \equiv 0$ , the point $0$ lies in $G^*$ .

Formalization scope

$\mathbb R^n$ is Fin n → ℝ with its product topology, which is the Euclidean one; $\Sigma x\xi$ is Mathlib's x ⬝ᵥ ξ. The paper's $\Sigma\xi x$ in $G^*, f^*$ is ξ ⬝ᵥ x, equal by commutativity.
$f$ is a total function (Fin n → ℝ) → ℝ, but every hypothesis and conclusion concerns its values on $G$ only: ConvexOn ℝ G f, LowerSemicontinuousOn f G, and Tendsto f (𝓝[G] x) atTop for x ∈ closure G \ G.
$\varphi$ is the real sSup, which is $0$ on unbounded sets; it is evaluated only on $\Gamma$ .
Three readings are fixed and disclosed in the goal's Formalization Note:
- (P1) $G$ is nonempty. The paper assumes it tacitly and proves $\Gamma \neq \emptyset$ .
- (P2) Interior points are relative-interior points (intrinsicInterior ℝ G). The paper's segment definition makes the equality clause false, and the topological interior makes it vacuous for lower-dimensional $G$ .
- (P3) Uniqueness is stated as the symmetry gives it. The literal "one and only one $\Gamma$ , $\varphi$ with these properties, (5) and equality at interior points" is false: for $G = [0,1]$ , $f \equiv 0$ , the pair $\Gamma' = \{0\}$ , $\varphi'(0) = 0$ also qualifies.
A statement of the goal that asserts only $f^* = f$ on $G$ and drops $G^* = G$ is a different and much weaker theorem; the goal carries the domain identity.
Needed infrastructure: supporting hyperplanes to convex sets at relative-interior points (Mathlib has separation theorems for Fin n → ℝ and the intrinsic interior), affine minorants of convex functions on lower-dimensional domains, and the boundary-limit argument of milestone 6. All of these are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome.

Selected references

W. Fenchel, On conjugate convex functions, Canadian Journal of Mathematics 1 (1949), 73–77. https://doi.org/10.4153/CJM-1949-007-x
W. H. Young, On classes of summable functions and their Fourier series, Proceedings of the Royal Society of London A 87 (1912), 225–229. https://doi.org/10.1098/rspa.1912.0076
J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bulletin de la Société Mathématique de France 93 (1965), 273–299. https://doi.org/10.24033/bsmf.1625
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

12 thms2 active usersReviewed

Completed

Convex Optimization Functional Analysis Operations Research·Captain: mikedeng1

On the Douglas–Rachford Splitting Method and the Proximal Point Algorithm for Maximal Monotone Operators: Generalized Douglas–Rachford Splitting Converges Weakly if A+B Has a Zero, Else Is UnboundedResearch Paper

Motivation

Many problems in convex optimization, variational inequalities and equilibrium modelling reduce to finding a point $x$ with $0 \in A x + B x$ , where $A$ and $B$ are maximal monotone operators on a real Hilbert space $\mathcal H$ : for example, minimizing $f + g$ for closed proper convex $f, g$ is the case $A = \partial f$ , $B = \partial g$ . When the resolvent of $A + B$ is hard to evaluate but the resolvents of $A$ and $B$ separately are easy, one uses a splitting method. Douglas–Rachford splitting, introduced for monotone operators by Lions and Mercier (1979) after an alternating-direction scheme of Douglas and Rachford (1956) for the heat equation, is the most widely used one; through its dual form it underlies the alternating direction method of multipliers (ADMM) used throughout large-scale optimization and statistics.

Eckstein and Bertsekas (MIT report LIDS-P-1919, 1989; Mathematical Programming 55, 1992) showed that Douglas–Rachford splitting is a special case of the proximal point algorithm applied to a single derived operator, the splitting operator $S_{\lambda,A,B}$ . This identification lets the convergence theory of the proximal point algorithm transfer to splitting, and yields a generalized method with inexact resolvent evaluations and relaxation.

Timeline.

Minty (1962): a monotone $T$ is maximal iff $I + T$ is onto.
Rockafellar (1976): the proximal point algorithm with variable stepsizes and summable errors converges weakly to a zero.
Lions and Mercier (1979): Douglas–Rachford splitting for maximal monotone $A$ , $B$ ; its map $G_{\lambda,A,B}$ is firmly nonexpansive.
Gol'shtein and Tret'yakov (1979): relaxed proximal iterations with factors $\rho_k \in (0,2)$ , in finite dimension, with a fixed stepsize.
Eckstein and Bertsekas (1989/1992): the splitting operator; Douglas–Rachford as a proximal point method; the generalized proximal point algorithm and the generalized Douglas–Rachford method, including the case with no solution.

Setting

An operator on $\mathcal H$ is a subset $T \subseteq \mathcal H \times \mathcal H$ , with $Tx = \{y \mid (x,y) \in T\}$ ; it may be multivalued and partially defined. Its domain is $\operatorname{dom} T = \{x \mid Tx \ne \emptyset\}$ , its image $\operatorname{im} T$ the projection on the second coordinate, its inverse $T^{-1} = \{(y,x) \mid (x,y) \in T\}$ . Scaling and sum are $cT = \{(x, cy)\}$ and $A + B = \{(x, y+z) \mid (x,y) \in A, (x,z) \in B\}$ ; $I$ is the identity. $T$ is monotone if $\langle x' - x, y' - y\rangle \ge 0$ for all $(x,y),(x',y') \in T$ , and maximal monotone if no other monotone operator strictly contains it. The resolvent is $J_{cT} = (I + cT)^{-1}$ , and $\operatorname{zer} T = \{x \mid 0 \in Tx\}$ . An operator $J$ is firmly nonexpansive if $\|y'-y\|^2 \le \langle x'-x, y'-y\rangle$ for all $(x,y),(x',y') \in J$ .

For $\lambda > 0$ the Douglas–Rachford map is $G_{\lambda,A,B} = J_{\lambda A} \circ (2J_{\lambda B} - I) + (I - J_{\lambda B})$ , and the splitting operator is

S_{\lambda,A,B} = \{(v + \lambda b,\ u - v) \mid (u,b) \in B,\ (v,a) \in A,\ v + \lambda a = u - \lambda b\}.

Its zero set is $Z^*_\lambda = \{u + \lambda b \mid b \in Bu,\ -b \in Au\}$ .

Formalization targets

Goal: Theorem 7 (generalized Douglas–Rachford splitting)

Let $A$ , $B$ be maximal monotone, $\lambda > 0$ , and let $\{z^k\}, \{u^k\}, \{v^k\} \subseteq \mathcal H$ , $\alpha_k, \beta_k \ge 0$ and $\rho_k$ satisfy

\|u^k - J_{\lambda B}(z^k)\| \le \beta_k,\quad \|v^{k+1} - J_{\lambda A}(2u^k - z^k)\| \le \alpha_k,\quad z^{k+1} = z^k + \rho_k (v^{k+1} - u^k),

with $\sum \alpha_k < \infty$ , $\sum \beta_k < \infty$ and $0 < \inf \rho_k \le \sup \rho_k < 2$ . Then

\operatorname{zer}(A+B) \ne \emptyset \implies z^k \rightharpoonup z^* \text{ for some } z^* \in Z^*_\lambda,\qquad \operatorname{zer}(A+B) = \emptyset \implies \{z^k\} \text{ unbounded}.

Milestones

In the paper's order: Minty's theorem (Theorem 1); properties of firmly nonexpansive operators (Lemma 1); the monotone / firmly nonexpansive correspondence (Theorem 2, Corollaries 2.1–2.3); zeros as fixed points of resolvents (Lemma 2); the generalized proximal point algorithm (Theorem 3): weak convergence to a zero of $T$ under summable errors, relaxation in $(0,2)$ and stepsizes bounded away from $0$ , unboundedness when $\operatorname{zer} T = \emptyset$ ; (maximal) monotonicity of $S_{\lambda,A,B}$ (Theorem 4) and firm nonexpansiveness of its resolvent (Corollary 4.1); $\operatorname{zer} S_{\lambda,A,B} = Z^*_\lambda$ (Theorem 5); and $(I + S_{\lambda,A,B})^{-1} = G_{\lambda,A,B}$ (Theorem 6).

Significance

Theorem 7 gives convergence of Douglas–Rachford splitting with both resolvents evaluated inexactly and with over- or under-relaxation, and it characterizes the case without a solution: the iterates are unbounded exactly when $A + B$ has no zero. The relaxed, inexact form is the one implementations actually run, and through Gabay's identification of ADMM with Douglas–Rachford on the dual it is the basis of the paper's Theorem 8, a convergence theorem for a generalized ADMM. Theorem 3, used to prove Theorem 7, is itself a standard reference form of the inexact relaxed proximal point algorithm.

All results here are proved in the paper (one step in the unbounded case of Theorem 3 rests on results of Rockafellar 1969 and 1970 on sums of maximal monotone operators). As of 2026, neither Douglas–Rachford splitting in this generality nor the generalized proximal point algorithm is formalized in Lean or Mathlib. Mathlib has Hilbert spaces, weak topologies and summability, but no theory of maximal monotone operators, Minty's theorem or resolvents. The mission builds that layer and machine-checks the paper's results on it.

Difficulty

The convergence argument cannot be strong: in infinite dimensions the proximal point algorithm need not converge in norm (Güler 1991), so the conclusion is weak convergence, and identifying the weak limit as a zero requires the weak–strong closedness of the graph of a maximal monotone operator. The maximality halves of Theorems 2 and 4 need Minty's theorem, whose proof requires a nontrivial existence argument (all known proofs use Zorn's lemma or an equivalent). The unbounded case of Theorem 3 is a contradiction argument that truncates $T$ by the subdifferential of the indicator of a ball and invokes two external facts: maximality of the sum of two maximal monotone operators under an interiority condition (Rockafellar 1970), and existence of zeros for maximal monotone operators with bounded domain (Rockafellar 1969). Neither is available in Lean. The natural first idea for Theorem 7, iterating the firm nonexpansiveness of $G_{\lambda,A,B}$ , gives neither the error tolerance on both resolvents nor the unbounded case without the full machinery of Theorem 3.

Formalization scope

$\mathcal H$ is a real inner product space that is complete ([CompleteSpace H]). An operator is a map H → Set H. Monotonicity, maximal monotonicity, $\operatorname{dom}$ , $\operatorname{zer}$ and the function-level resolvent predicate IsResolvent are the published definitions ThreeOpSplitting_Convergence_MonotoneOperators; weak convergence is the published WeakTendsto ( $\langle z^k, y\rangle \to \langle z^*, y\rangle$ for every $y$ ).
§2 notions are graph notions (opResolvent, IsFirmlyNonexpansiveOp, ...), so Theorem 2 and Corollary 2.1 can speak of resolvents that are a priori partial or multivalued. In Theorems 3, 6 and 7 the resolvents are maps $J : \mathcal H \to \mathcal H$ with $\lambda^{-1}(x - J x) \in A(Jx)$ for all $x$ , unique by Corollary 2.2.
$S_{\lambda,A,B}$ is defined by its set formula, not as $G_{\lambda,A,B}^{-1} - I$ ; with the latter, Theorem 6 and Corollary 4.1 would be unfoldings. Taking free resolvent functions without the IsResolvent hypothesis would make the iteration unrelated to $A$ and $B$ ; the hypothesis is always present.
$\inf \rho_k > 0$ , $\sup \rho_k < 2$ are encoded as $\exists\, \rho_1, \rho_2$ with $0 < \rho_1 \le \rho_k \le \rho_2 < 2$ ; $\inf c_k > 0$ as $\exists\, c_0 > 0$ , $c_0 \le c_k$ . Summability is Summable with nonnegative terms. Sequences start at $k = 0$ ; $v^0$ is unused. Unboundedness is ¬ Bornology.IsBounded (Set.range z).
Printed slips corrected and disclosed in the items: Theorem 7 states its sequences in $\mathbb R^n$ (read $\mathcal H$ ); Theorem 3 prints $(1 - \rho_k) w^k$ (read $\rho_k w^k$ , as on p. 9 and in the proof) and $(I + cT)^{-1}$ (read $(I + c_k T)^{-1}$ ).
Not included: Corollary 2.4, Corollaries 6.1–6.2 (special cases of Theorem 7), §5 (partial inverses, generalized ADMM). The second sentence of Corollary 6.1 (convergence of $J_{\lambda B}(z^k)$ ) is deliberately excluded: its argument does not transfer weak convergence (Svaiter 2011).
Welcome contributions: Minty's theorem in Hilbert space, the resolvent calculus of §2, and weak-limit lemmas (Opial-type arguments) are reusable well beyond this mission.

Selected references

J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, MIT report LIDS-P-1919, 1989; Mathematical Programming 55 (1992) 293–318. https://doi.org/10.1007/BF01581204
P.-L. Lions and B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM J. Numer. Anal. 16 (1979) 964–979. https://doi.org/10.1137/0716071
G. J. Minty, Monotone (nonlinear) operators in Hilbert space, Duke Math. J. 29 (1962) 341–346. https://doi.org/10.1215/S0012-7094-62-02933-2
R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM J. Control Optim. 14 (1976) 877–898. https://doi.org/10.1137/0314056
O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM J. Control Optim. 29 (1991) 403–419. https://doi.org/10.1137/0329022
B. F. Svaiter, On weak convergence of the Douglas–Rachford method, SIAM J. Control Optim. 49 (2011) 280–287. https://doi.org/10.1137/100788100

17 thms2 active usersReviewed

Linear Optimization Operations Research Probability+1·Captain: mikedeng1

Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time 2: The Two-Phase Shadow-Vertex Simplex Method Has Polynomial Smoothed ComplexityResearch Paper

Motivation

The simplex method solves linear programs by moving between vertices of a feasible polyhedron. Its worst-case number of moves can grow exponentially, yet it often performs well on ordinary inputs. Worst-case examples alone therefore give an incomplete account of the method’s behavior. Spielman and Teng introduced smoothed analysis to measure expected performance after small random perturbations of an arbitrary input. Their result for a two-phase shadow-vertex simplex method gives a polynomial bound in the input dimensions and inverse perturbation scale. The pinned preprint is the source for every theorem number and constant in this mission.

The paper separates a geometric result about the expected size of a polytope’s shadow (Theorem 4.0.1) from the algorithmic result here (Theorem 5.0.1). That separation matters: a plane chosen before perturbation and a plane chosen by a running algorithm have different distributions. This mission addresses the latter. It complements the standard-form simplex theorems already formalized in the Introduction to Linear Optimization series and the worst-case Klee–Minty result in the Smale’s Ninth Problem mission; those results concern different algorithms or input models and are context rather than imported statements.

Setting

A linear program is specified by vectors $a_1,\ldots,a_n\in\mathbb R^d$ , right-hand sides $y_1,\ldots,y_n\in\mathbb R$ , and an objective vector $z\in\mathbb R^d$ :

\max_x\langle z,x\rangle\quad\text{subject to}\quad \langle a_i,x\rangle\le y_i\qquad(1\le i\le n).

The paper’s two-phase shadow-vertex method first draws a collection $\mathcal I$ of $d$ -element subsets of $[n]$ and chooses one whose constraint matrix $A_I$ has the largest smallest singular value. It sets a power-of-two scale $M$ from the input norm and a power-of-two scale $\kappa$ from that singular value. These determine positive relaxed right-hand sides $y'_i$ : $M$ for $i\in I$ and $\sqrt d M^2/(4\kappa)$ otherwise. A coefficient vector $\alpha$ is chosen uniformly from $A_{1/d^2}=\{\alpha:\sum_{i\in I}\alpha_i=1,\ \alpha_i\ge1/d^2\}$ . The first phase solves the relaxed program LP′ from the objective $A_I\alpha$ .

The second phase uses a lifted program LP⁺ in $\mathbb R^{d+1}$ . For each original constraint it forms $a_i^+=((y'_i-y_i)/2,a_i)$ and $y_i^+=(y'_i+y_i)/2$ , together with two artificial constraints at first coordinates $1$ and $-1$ . LP⁺ connects LP′ to the original program and makes infeasibility detectable. Its shadow is taken in the plane of $(0,z)$ and $z^+=(1,0,\ldots,0)$ .

For positive right-hand sides, an optimal polar simplex is a $d$ -subset of constraints whose scaled vectors $a_i/y_i$ form a facet of $\operatorname{ConvHull}(0,a_1/y_1,\ldots,a_n/y_n)$ and whose unscaled cone contains an objective $q$ . The shadow for objectives $t,z$ is the union of these simplices over all $q$ in $\operatorname{Span}(t,z)$ . Its size bounds the number of polar pivots. In Section 5 the paper writes $S'_z$ for the first-phase shadow size and $S_z^+$ for the second-phase shadow size without the two artificial pivots.

The input is perturbed by independent Gaussians: each coordinate of $a_i$ and each $y_i$ has its prescribed center and common standard deviation $\sigma R$ , where $R=\max_i\|(\bar y_i,\bar a_i)\|_2$ . The algorithm has separate random choices of $\mathcal I$ and $\alpha$ .

Formalization targets

The immediate targets bound the two phases: Lemma 5.2.1 gives an explicit expectation bound for $S'_z$ and Lemma 5.3.1 gives one for $S_z^+$ . Lemma 5.1.1 and its corollaries control the chance that the chosen basis has a very small singular value. Corollary 4.3.3 extends the geometric shadow bound to positive, unequal right-hand sides and general Gaussian covariance. These are the mission’s milestone targets.

The goal is the shape of Theorem 5.0.1. With $C(A,y,z)=\mathbb E_{\mathcal I,\alpha}(S'_z+S_z^++2)$ , there are a single polynomial $\mathcal P$ and a positive constant $\sigma_0$ such that, for all $n>d\ge3$ and all centers and objectives,

\mathbb E_{A,y}C(A,y,z)\le \min\left\{\mathcal P\left(d,n,\frac1{\min(\sigma,\sigma_0)}\right), \binom nd+\binom n{d+1}+2\right\}.

The polynomial is uniform over the dimensions and inputs; its coefficients are not prescribed. The bound on $C$ implies the corresponding result for the actual pivot count through the paper’s step-to-shadow comparison. The goal is stated with a positive center scale $R$ , the case in which the paper’s Gaussian rescaling applies.

Significance

The theorem places the number of pivots of a complete simplex method under one explicit perturbation model, including the work needed to find a starting feasible basis and handle an arbitrary right-hand side. The trivial binomial bound is retained because it controls rare events in the proof and is part of the stated result. The polynomial bound says that even when the unperturbed LP is adversarial, Gaussian noise of a controlled scale makes the expected shadow-size cost polynomial.

The paper proves the mathematical result. This mission asks for machine-checked proofs of its statement and the listed milestones; the draft Lean declarations are targets with sorry, not completed proofs. The reusable formal infrastructure is the finite polar simplex and shadow construction, product Gaussian input law, smallest-singular-value events for sampled minors, and the uniform truncated-simplex coefficient law. The two shadow-size lemmas also require explicit handling of measurable finite-valued counts and their expectations.

Difficulty

The basic shadow estimate fixes its projection plane before perturbing the constraints. In LP′, the initial objective $A_I\alpha$ uses a basis selected after the perturbation, so the relevant plane depends on the random LP. The fixed-plane theorem cannot be substituted directly. For LP⁺, the normalized lifted vectors $a_i^+/y_i^+$ are nonlinear functions of Gaussian data; they are generally not Gaussian vectors. Thus the same shadow estimate does not apply directly to their law either. A further issue is that a poor sampled basis can make $y'$ very large. These are distinct obstacles, reflected in the milestone groups from Sections 5.1, 5.2, and 5.3.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), constraints are Fin n → EuclideanSpace ℝ (Fin d), and index families are finite sets of Fin n. The paper’s $[n]$ starts at one; Fin n starts at zero. The Gaussian constructor receives variance $\sigma^2$ , not standard deviation $\sigma$ . The $3nd\ln n$ draws are rounded upward and are independent uniform draws with replacement. Equal singular values are resolved by the first sampled set. The uniform law on $A_\delta$ is represented by normalized independent exponential weights followed by the affine shift that imposes $\alpha_i\ge\delta$ .

The Lean definition of $C$ is exactly the Section 5 shadow-size upper bound $\mathbb E(S'_z+S_z^++2)$ , computed from the sampled LP data. It is not an arbitrary cost variable. The actual algorithmic step bound needs the paper’s polar algorithm and Lemma 3.3.5. The goal explicitly asks for inner and outer integrability so Lean’s default value for a nonintegrable Bochner integral cannot make the result vacuous. The source’s all-zero center scale is excluded because it gives zero perturbation and defeats the rescaling used in Theorem 5.0.1.

For LP⁺ the vectors live in $\mathbb R^{d+1}$ , so the two LP⁺ milestone bounds use $\mathcal D(n,d+1,\cdot)$ . The preprint prints $d$ in those calls even though the preceding extension theorem would be applied in dimension $d+1$ . Lemma 5.2.1 is written as an inequality: its printed equality is stronger than the bound established on page 71. These corrections are visible in the theorem titles and notes. Contributions that prove the exact statements, establish the measurability and Gaussian law facts, or formalize the step-to-shadow comparison are welcome.

Selected references

Daniel A. Spielman and Shang-Hua Teng, Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time, arXiv:cs/0111050v7, 2003, preprint. The PDF used here is the 96-page version with printed and PDF page numbers aligned.

22 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning·Captain: mikedeng1

SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives II: The 4n/k Rate of the Averaged Iterate without Strong ConvexityResearch Paper

Motivation

Many problems in statistics and machine learning minimize an average of $n$ losses, one per data point, plus a regularizer: least squares, logistic regression, and their $\ell_1$ - or $\ell_2$ -penalized versions. When $n$ is large, a full gradient costs $n$ component gradients, while stochastic gradient descent, which uses one component per step, needs decreasing step sizes and converges slowly. Incremental gradient methods with variance reduction (SAG, SVRG, SDCA, Finito, MISO) use one component gradient per step but converge at the rate of a full-gradient method.

SAGA (Defazio, Bach and Lacoste-Julien, NIPS 2014, arXiv:1407.0202) is a method of this family. It handles a non-smooth regularizer through its proximal operator, and it comes with a guarantee when the losses are convex but not strongly convex. This mission covers that second guarantee, Theorem 2 of the paper. A companion mission covers the linear rate under strong convexity (Theorem 1, Corollary 1).

Timeline.

2012: SAG (Le Roux, Schmidt and Bach) gives a linear rate for smooth, strongly convex finite sums. Its analysis does not cover a proximal term.
2013: SVRG (Johnson and Zhang) gives a linear rate for the strongly convex case, using periodic full-gradient passes.
2013: SDCA (Shalev-Shwartz and Zhang) works on the dual and needs strong convexity.
2014: Prox-SVRG (Xiao and Zhang, arXiv:1403.4699) extends SVRG to composite objectives. Its key inequality is reused by SAGA's Theorem 2.
2014: SAGA proves both a linear rate under strong convexity and an $O(n/k)$ rate for the averaged iterate under convexity alone, for composite objectives.

Setting

Let $d\ge 0$ and $n\ge 1$ . The components $f_1,\dots,f_n:\mathbb R^d\to\mathbb R$ are convex and differentiable, and each gradient $f_i'$ is $L$ -Lipschitz ( $L>0$ ). Write

f(x)=\frac1n\sum_{i=1}^n f_i(x),\qquad f'(x)=\frac1n\sum_{i=1}^n f_i'(x).

The regularizer $h:\mathbb R^d\to\mathbb R$ is convex but possibly non-differentiable. The objective is the composite function $F=f+h$ , and $x^*$ is any minimizer of $F$ . Minimizers need not be unique, and $f'(x^*)$ need not vanish.

The proximal operator with parameter $\gamma>0$ is

\mathrm{prox}_\gamma^h(y)=\arg\min_{x\in\mathbb R^d}\Big\{h(x)+\frac1{2\gamma}\|x-y\|^2\Big\}.

SAGA keeps an iterate $x^k$ and a table of points $\phi_1^k,\dots,\phi_n^k$ , initialized as $\phi_i^0=x^0$ . At step $k+1$ it draws an index $j$ uniformly from $\{1,\dots,n\}$ , independently of the past, and sets

w^{k+1}=x^k-\gamma\Big[f_j'(x^k)-f_j'(\phi_j^k)+\frac1n\sum_{i=1}^n f_i'(\phi_i^k)\Big],\qquad x^{k+1}=\mathrm{prox}_\gamma^h(w^{k+1}).

It then sets $\phi_j^{k+1}=x^k$ and leaves the other table entries unchanged. The averaged iterate is $\bar x^k=\frac1k\sum_{t=1}^k x^t$ , which excludes $x^0$ .

Formalization targets

Goal: Theorem 2 (p. 11)

With step size $\gamma=1/(3L)$ , for every $k\ge1$ ,

\mathbb E\big[F(\bar x^k)\big]-F(x^*)\le\frac{4n}{k}\Big[\frac{2L}{n}\|x^0-x^*\|^2+f(x^0)-\langle f'(x^*),x^0-x^*\rangle-f(x^*)\Big].

The expectation is over the indices $j^1,\dots,j^k$ . The constants are those printed in the paper.

Milestones (in attack order)

Lemma 1 (p. 6) is an inner-product bound for averages of $\mu$ -strongly convex functions with $L$ -Lipschitz gradients. It is stated for $\mu\ge0$ , and Theorem 2 uses the case $\mu=0$ .
Lemma 2 (p. 7): $\frac1n\sum_i\|f_i'(\phi_i)-f_i'(x^*)\|^2\le 2L\big[\frac1n\sum_i f_i(\phi_i)-f(x^*)-\frac1n\sum_i\langle f_i'(x^*),\phi_i-x^*\rangle\big]$ .
The bound on $\Delta$ (p. 12). Write $\Delta=-\frac1\gamma(w^{k+1}-x^k)-f'(x^k)$ for the gradient error. For every $\beta>0$ , $\mathbb E\|\Delta\|^2\le(1+\beta^{-1})\mathbb E\|f_j'(\phi_j^k)-f_j'(x^*)\|^2+(1+\beta)\mathbb E\|f_j'(x^k)-f_j'(x^*)\|^2$ .
The prox-SVRG inequality (p. 12): $\alpha\mathbb E\|x^{k+1}-x^*\|^2\le\alpha\|x^k-x^*\|^2-2\alpha\gamma\mathbb E[F(x^{k+1})-F(x^*)]+2\alpha\gamma^2\mathbb E\|\Delta\|^2$ .
The one-step Lyapunov decrease (p. 12): $\mathbb E[T^{k+1}]-T^k\le-\frac1{4n}\mathbb E[F(x^{k+1})-F(x^*)]$ . Here $T(x,\phi)=\frac1n\sum_i f_i(\phi_i)-f(x^*)-\frac1n\sum_i\langle f_i'(x^*),\phi_i-x^*\rangle+(c+\alpha)\|x-x^*\|^2$ , with $c=\frac{3L}{2n}$ and $\alpha=\frac{3L}{8n}$ .

In milestones 3–5, $\mathbb E$ is the expectation over the single index $j$ of the next step, given the current state.

Significance

The result. Theorem 2 shows that one method, with a step size that depends only on $L$ , covers composite problems that are not strongly convex. Examples are $\ell_1$ -regularized least squares and logistic regression without a ridge term. On these problems the method converges in expected objective value at rate $O(n/k)$ . SAG has no proximal analysis, and SDCA requires strong convexity. With the same step size $1/(3L)$ , the paper also states adaptivity to strong convexity, so no strong convexity constant has to be known in advance. The bound is in terms of $T^0$ , a quantity computable from the starting point.

Formalizing it. The result is proved on paper, but the proof is not self-contained. Its central inequality (milestone 4) is quoted from the prox-SVRG analysis of Xiao and Zhang, with only the remark that their argument uses $\mathbb E[\Delta]=0$ . A machine-checked proof must therefore reconstruct that argument for SAGA's estimator. To our knowledge, no machine-checked proof of SAGA, SVRG or prox-SVRG exists in Lean or Mathlib. The mission also produces reusable statements about convex functions with Lipschitz gradients (Lemmas 1 and 2) and an explicit finite model of a randomized incremental method.

Difficulty

The naive approach applies the non-expansiveness of the proximal operator to $\|x^{k+1}-x^*\|^2$ , as in the strongly convex proof. That bounds distances, but it produces no term in $F(x^{k+1})-F(x^*)$ . Without strong convexity, the distance terms cannot be traded for function values, so the argument yields no rate.

The function-value term comes from the prox-SVRG inequality (milestone 4), which the paper does not prove. Its difficulty is that $x^{k+1}$ depends on the same random index as $\Delta$ , so the cross term between them does not vanish in expectation even though $\mathbb E[\Delta]=0$ . A second difficulty is bookkeeping: $w^{k+1}$ uses the old table, the table entry $j$ receives $x^k$ and not $x^{k+1}$ , and the constants must make three coefficients vanish exactly. A final step converts the bound on $\frac1k\sum_t\mathbb E[F(x^t)]$ into a bound on $\mathbb E[F(\bar x^k)]$ , which requires Jensen's inequality for the convex $F$ .

Formalization scope

Space and indices. Points live in EuclideanSpace ℝ (Fin d). Components are indexed by Fin n (0-based), with $n\ge1$ .
Gradients and smoothness. The gradients are given maps f' with HasGradientAt (f i) (f' i x) x at every point. Smoothness is the Lipschitz bound $\|f_i'(x)-f_i'(y)\|\le L\|x-y\|$ .
Convexity. Convexity is ConvexOn ℝ Set.univ. Lemma 1 uses StrongConvexOn Set.univ μ, whose modulus $\frac\mu2\|x-y\|^2$ is the paper's.
The regularizer. $h$ is real-valued and convex. Extended-valued regularizers such as indicator functions are outside the statement.
The proximal map. The proximal operator enters as any map $P$ such that $P(y)$ minimizes $h(z)+\frac1{2\gamma}\|z-y\|^2$ for every $y$ . For convex $h$ this determines $P=\mathrm{prox}_\gamma^h$ .
State and expectation. The state is the pair $(x^k,\phi^k)$ . The expectation over $k$ steps is the uniform average over the $n^k$ index sequences, which is exactly the law of $k$ independent uniform indices.

Two trivializations are excluded. The averaged-iterate bound carries $k\ge1$ , since at $k=0$ the factor $4n/k$ collapses to $0$ . The left side is $F$ evaluated at the averaged point, not the average of $F(x^t)$ , which is a weaker intermediate step.

A complete development needs the descent lemma and co-coercivity for convex functions with Lipschitz gradients, the characterization and non-expansiveness of the proximal operator, and finite-sum manipulations over index sequences. The lemmas on smooth convex functions and on proximal operators are reusable beyond this mission. Contributions are welcome at every level: proofs of the milestones, a reusable proximal-operator library, and the telescoping argument for the goal.

Selected references

A. Defazio, F. Bach, S. Lacoste-Julien, SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives, NIPS 2014. arXiv:1407.0202
L. Xiao, T. Zhang, A Proximal Stochastic Gradient Method with Progressive Variance Reduction, SIAM J. Optim. 24(4), 2014. arXiv:1403.4699
N. Le Roux, M. Schmidt, F. Bach, A Stochastic Gradient Method with an Exponential Convergence Rate for Finite Training Sets, NIPS 2012. arXiv:1202.6258
R. Johnson, T. Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, NIPS 2013. NeurIPS proceedings
S. Shalev-Shwartz, T. Zhang, Stochastic Dual Coordinate Ascent Methods for Regularized Loss Minimization, JMLR 14, 2013. arXiv:1209.1873
Y. Nesterov, Introductory Lectures on Convex Optimization, Kluwer, 2004. doi:10.1007/978-1-4419-8853-9

11 thms2 active usersReviewed

Convex Optimization Operations Research Reinforcement Learning·Captain: mikedeng1

Twice Regularized MDPs and the Equivalence Between Robustness and Regularization 1: The Robust Value Function Is the Optimum of a Policy- and Value-Regularized Convex ProgramResearch Paper

Motivation

A Markov decision process (MDP) is solved for one model of its dynamics and rewards, but in practice that model is estimated from data, and a policy that is optimal for the estimate can perform poorly on the true system (Mannor et al., 2007). Robust MDPs address this by evaluating a policy against the worst model in an uncertainty set $\mathcal U$ (Iyengar, 2005; Nilim and El Ghaoui, 2005; Wiesemann, Kuhn and Rustem, 2013). Robust planning, however, solves an inner optimization over $\mathcal U$ at every Bellman update, which is expensive and does not scale to learning settings.

A separate line of work regularizes the policy (entropy, KL, Tsallis penalties) and observes empirically that regularized policies are robust to perturbations (Geist, Scherrer and Pietquin, 2019). Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) make this precise: for uncertainty sets centred at a nominal model, the robust value function is the solution of a regularized problem posed on the nominal model alone, with a regularizer that is the support function of the uncertainty set. This mission formalizes that equivalence: Proposition 3.1, Theorem 3.1 and Theorem 4.1 of the paper.

Setting

Let $\mathcal S$ and $\mathcal A$ be finite sets of states and actions, $\mathcal A$ nonempty, and $\mathcal X := \mathcal S\times\mathcal A$ . Fix a discount factor $\gamma\in(0,1)$ and a strictly positive initial distribution $\mu_0\in\Delta_{\mathcal S}$ . A transition kernel $P$ assigns to every pair $(s,a)$ a probability distribution $P(\cdot\mid s,a)$ on $\mathcal S$ ; a reward is $r\in\mathbb R^{\mathcal X}$ . A policy $\pi\in\Delta_{\mathcal A}^{\mathcal S}$ assigns to every state an action distribution $\pi_s$ .

For $v\in\mathbb R^{\mathcal S}$ write $r^\pi(s) = \sum_a\pi_s(a)r(s,a)$ , $P^\pi(s'\mid s) = \sum_a\pi_s(a)P(s'\mid s,a)$ , and define the evaluation Bellman operator

T^\pi_{(P,r)}v := r^\pi + \gamma P^\pi v .

The inner product on $\mathbb R^{\mathcal S}$ is $\langle v,\mu\rangle = \sum_s v(s)\mu(s)$ , and the support function of a set $C\subseteq\mathbb R^{\iota}$ is $\sigma_C(y) = \max_{a\in C}\langle a,y\rangle$ .

Given a set $\mathcal U$ of models $(P,r)$ , the robust Bellman operator is

[T^{\pi,\mathcal U}v](s) := \min_{(P,r)\in\mathcal U}T^\pi_{(P,r)}v(s),

and the robust value function $v^{\pi,\mathcal U}$ is its fixed point. Around a nominal model $(P_0,r_0)$ , an s-rectangular uncertainty set $\mathcal U = (P_0+\mathcal P)\times(r_0+\mathcal R)$ is given by sets $\mathcal P_s\subseteq\mathbb R^{\mathcal X}$ and $\mathcal R_s\subseteq\mathbb R^{\mathcal A}$ , one per state: its models are $P(s'\mid s,a) = P_0(s'\mid s,a)+P_s(s',a)$ and $r(s,a) = r_0(s,a)+r_s(a)$ , with $P_s\in\mathcal P_s$ and $r_s\in\mathcal R_s$ chosen independently for each $s$ . Finally $[v\cdot\pi_s](s',a) := v(s')\pi_s(a)$ .

Formalization targets

Goal: Theorem 4.1 (general robust MDP)

For $\mathcal U = (P_0+\mathcal P)\times(r_0+\mathcal R)$ and every policy $\pi$ , $T^{\pi,\mathcal U}$ has a unique fixed point $v^{\pi,\mathcal U}$ , and it is the optimal solution of

\max_{v\in\mathbb R^{\mathcal S}}\langle v,\mu_0\rangle\quad\text{s.t.}\quad v(s)\le T^\pi_{(P_0,r_0)}v(s)-\sigma_{\mathcal R_s}(-\pi_s)-\sigma_{\mathcal P_s}(-\gamma v\cdot\pi_s)\quad\forall s\in\mathcal S. \tag{2}

Milestones

Proposition 3.1. For any uncertainty set $\mathcal U = \mathcal P\times\mathcal R$ with $\mathcal P$ a nonempty compact set of kernels and $\mathcal R$ a nonempty compact set of rewards, $v^{\pi,\mathcal U}$ is the optimal solution of the robust program $\max_{v}\langle v,\mu_0\rangle\quad\text{s.t.}\quad v\le T^\pi_{(P,r)}v\ \ \forall(P,r)\in\mathcal U. \tag{$P_{\mathcal U}$}$
Theorem 3.1. For $\mathcal U=\{P_0\}\times(r_0+\mathcal R)$ , $v^{\pi,\mathcal U}$ is the optimal solution of $\max_v\langle v,\mu_0\rangle$ s.t. $v(s)\le T^\pi_{(P_0,r_0)}v(s)-\sigma_{\mathcal R_s}(-\pi_s)$ for all $s$ .
Robust counterpart (proof of Theorem 4.1, App. B.1). For every $v$ and $s$ ,

\max_{(P,r)\in\mathcal U}\{v(s)-r^\pi(s)-\gamma P^\pi v(s)\} = \sigma_{\mathcal P_s}(-\gamma v\cdot\pi_s)+\sigma_{\mathcal R_s}(-\pi_s)+v(s)-T^\pi_{(P_0,r_0)}v(s).

Theorem 3.1 is the special case $\mathcal P_s=\{0\}$ of the goal; it is listed separately because it is the paper's statement that policy regularization is equivalent to reward uncertainty.

Significance

The goal says that a robust MDP with s-rectangular uncertainty in both reward and transitions is a regularized MDP on the nominal model, with two regularizers: a policy regularizer $\sigma_{\mathcal R_s}(-\pi_s)$ coming from reward uncertainty, and a regularizer $\sigma_{\mathcal P_s}(-\gamma v\cdot\pi_s)$ coming from transition uncertainty that depends on both the policy and the value. For ball-shaped sets these support functions are explicit ( $\alpha^r_s\|\pi_s\|$ and $\alpha^P_s\gamma\|v\|\|\pi_s\|$ , Corollary 4.1 of the paper), which leads to the twice regularized (R²) Bellman operators of Section 5 and to robust planning at the cost of non-robust planning. Theorem 3.1 also explains why standard policy regularizers (negative entropy, KL, Tsallis) yield robustness: each is the support function of a reward uncertainty set.

The results are proved in the paper (appendices A.1, A.2, B.1); none has a machine-checked proof. The mission produces formal statements and proofs of the equivalence, the robust Bellman operator's fixed-point theory for stochastic policies and general compact uncertainty sets, and a closed-form robust counterpart that later R² results can import. The paper's printed proof of Proposition 3.1 treats $T^{\pi,\mathcal U}$ as linear in one step; a formal proof settles the statement independently of that step.

Difficulty

The obvious argument reads Proposition 3.1 as linear-programming duality, as for a single MDP. That fails: $T^{\pi,\mathcal U}$ is a minimum of affine maps, hence concave and not affine, and the feasible set of $(P_{\mathcal U})$ is an intersection of infinitely many half-space systems; the argument has to go through monotonicity and contraction of $T^{\pi,\mathcal U}$ , which in turn requires every model in $\mathcal U$ to be a genuine transition kernel. For the goal, the paper invokes Fenchel–Rockafellar duality to evaluate the inner maximum; the work in Lean is to separate the maximum over the product set $\mathcal U$ into per-state maxima, which needs the s-rectangular structure and attainment of every maximum (compactness), and to track the index order of the perturbation $P_s(s',a)$ against the kernel $P(s'\mid s,a)$ .

Formalization scope

States and actions are finite types, A nonempty; values are S → ℝ ordered pointwise; a transition array is P : S → A → S → ℝ with P s a s' $=P(s'\mid s,a)$ , and the kernel property is the published IsTransitionKernel; $P^\pi(s'\mid s)$ is the published InducedTransition. A policy has π s ∈ stdSimplex ℝ A for every s.
Perturbations $P_s$ are functions S × A → ℝ indexed $(s',a)$ , as in the paper's $\mathbb R^{\mathcal X}$ ; rewards perturbations are A → ℝ.
Minima and maxima (in $T^{\pi,\mathcal U}$ and in $\sigma$ ) are real sInf/sSup. Every theorem assumes the sets nonempty and compact, so these are attained; nothing is quantified over an unbounded set.
The robust value function is encoded as the fixed point of $T^{\pi,\mathcal U}$ , and each theorem asserts its existence and uniqueness. The paper's definition $v^{\pi,\mathcal U}(s)=\min_{(P,r)\in\mathcal U}v^\pi_{(P,r)}(s)$ (p. 4) coincides with it for rectangular sets by a cited result; the proofs use only the fixed-point property. For the non-rectangular sets of Proposition 3.1 the pointwise minimum can be strictly larger than the fixed point and is then not the optimum of $(P_{\mathcal U})$ , so the fixed point is the object the proposition is true for.
"The optimal solution" means: feasible, objective-maximal, and the unique maximizer (uniqueness uses $\mu_0>0$ ).
Disclosed hypotheses: $\mathcal U=\mathcal P\times\mathcal R$ with $\mathcal P$ , $\mathcal R$ nonempty and compact and every transition in $\mathcal P$ a kernel (Prop. 3.1); $\mathcal P_s$ , $\mathcal R_s$ nonempty and compact and every perturbed row $P_0(\cdot\mid s,a)+P_s(\cdot,a)$ in $\Delta_{\mathcal S}$ (Thm 4.1); reward sets rectangular in Thm 3.1, as its proof uses. These are the robust-MDP standing assumptions of p. 4 ( $\mathcal P\subseteq\Delta^{\mathcal X}_{\mathcal S}$ ) and what makes "min" and "max" well defined.
Not drafted: Corollary 4.1, whose ℓ²-ball $\mathcal P_s$ contains perturbations that leave the simplex, so $P_0+\mathcal P$ is not a set of kernels; Corollary 3.1 and Proposition 3.2 (consequences after the goal; Prop. 3.2 depends on an unspecified policy parametrization).
A formalization that asserts only that the feasible sets of $(P_{\mathcal U})$ and (2) coincide, or that drops the kernel condition or the existence of the fixed point, does not count: the goal names the robust value function and its optimality.
"Convex" in the statement of Theorem 4.1 is descriptive and is not part of the formal goal.

Contributions welcome: the monotone-contraction fixed-point lemma for $T^{\pi,\mathcal U}$ and the per-state separation of maxima over rectangular sets are reusable for any robust MDP mission.

Selected references

E. Derman, M. Geist, S. Mannor, Twice regularized MDPs and the equivalence between robustness and regularization, NeurIPS 2021. arXiv:2110.06267v1
G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. doi:10.1287/moor.1040.0129
A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. doi:10.1287/opre.1050.0216
W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov decision processes, Mathematics of Operations Research 38(1), 2013. doi:10.1287/moor.1120.0566
M. Geist, B. Scherrer, O. Pietquin, A theory of regularized Markov decision processes, ICML 2019. PMLR 97
S. Mannor, D. Simester, P. Sun, J. N. Tsitsiklis, Bias and variance approximation in value function estimates, Management Science 53(2), 2007. doi:10.1287/mnsc.1060.0614

8 thms2 active usersReviewed

Completed

Convex Optimization Machine Learning·Captain: mikedeng1

SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives I: Linear Convergence under Strong ConvexityResearch Paper

Motivation

Many problems in machine learning and statistics are finite sums: an empirical risk $f(x)=\frac1n\sum_{i=1}^n f_i(x)$ over $n$ data points, often plus a regulariser $h$ such as an $\ell_1$ penalty. When $n$ is large, a full gradient of $f$ costs $n$ component gradients, while stochastic gradient descent uses one component per step but converges only sublinearly because its gradient estimate has non-vanishing variance. Incremental gradient methods with variance reduction keep the per-step cost of one component gradient and still converge linearly on strongly convex problems.

SAGA, introduced by Defazio, Bach and Lacoste-Julien at NIPS 2014 (arXiv:1407.0202), is one of the standard methods of this family, alongside SAG, SVRG, SDCA and Finito/MISO. It keeps a table of past component gradients and handles a non-smooth regulariser through its proximal operator.

Timeline. Le Roux, Schmidt and Bach (2012) gave SAG the first linear rate for strongly convex finite sums at the cost of one gradient per step. Shalev-Shwartz and Zhang (2013) proved linear rates for SDCA, a dual method. Johnson and Zhang (2013) introduced SVRG, with periodic full-gradient passes; Xiao and Zhang (2014) extended it to composite objectives (prox-SVRG). SAGA (2014) combines an unbiased SVRG-style estimator with a SAG-style table, and proves a linear rate in the composite strongly convex case with a simple Lyapunov argument.

Setting

Let $\mathbb R^d$ carry the Euclidean inner product. There are $n\ge1$ differentiable components $f_1,\dots,f_n:\mathbb R^d\to\mathbb R$ with gradients $f_i'$ . Each $f_i$ is $\mu$ -strongly convex ( $\mu>0$ ): $f_i(ax+by)\le af_i(x)+bf_i(y)-ab\frac\mu2\|x-y\|^2$ for $a,b\ge0$ , $a+b=1$ . Each gradient is $L$ -Lipschitz: $\|f_i'(x)-f_i'(y)\|\le L\|x-y\|$ . Write $f=\frac1n\sum_i f_i$ and $f'=\frac1n\sum_i f_i'$ . The regulariser $h:\mathbb R^d\to\mathbb R$ is convex, and the goal is to minimise the composite objective $F=f+h$ ; $x^*$ denotes its minimiser, which is unique.

The proximal operator with step $\gamma>0$ is

\operatorname{prox}^h_\gamma(y)=\operatorname*{argmin}_{x}\Big\{h(x)+\tfrac1{2\gamma}\|x-y\|^2\Big\}.

SAGA keeps an iterate $x^k$ and points $\phi_1^k,\dots,\phi_n^k$ at which the stored gradients $f_i'(\phi_i^k)$ were taken. It starts from $x^0$ with $\phi_i^0=x^0$ . At iteration $k+1$ it draws $j$ uniformly from $\{1,\dots,n\}$ , independently of the past, and sets

w^{k+1}=x^k-\gamma\Big[f_j'(x^k)-f_j'(\phi_j^k)+\frac1n\sum_{i=1}^n f_i'(\phi_i^k)\Big],\qquad x^{k+1}=\operatorname{prox}^h_\gamma(w^{k+1}),

then $\phi_j^{k+1}=x^k$ , with every other entry unchanged.

The analysis uses the Lyapunov function

T(x,\{\phi_i\})=\frac1n\sum_i f_i(\phi_i)-f(x^*)-\frac1n\sum_i\langle f_i'(x^*),\phi_i-x^*\rangle+c\|x-x^*\|^2 .

Formalization targets

Goal: Corollary 1 (p. 8)

With $\gamma=\frac1{2(\mu n+L)}$ , for every $k\ge0$ ,

\mathbb E\|x^k-x^*\|^2\le\Big(1-\frac{\mu}{2(\mu n+L)}\Big)^k\Big[\|x^0-x^*\|^2+\frac{n}{\mu n+L}\big(f(x^0)-\langle f'(x^*),x^0-x^*\rangle-f(x^*)\big)\Big],

where the expectation is over the indices drawn in the first $k$ iterations. The constants are the paper's.

Theorem 1 (p. 7)

With $\gamma$ as above, $c=\frac1{2\gamma(1-\gamma\mu)n}$ and $\kappa=\frac1{\gamma\mu}$ , for every state $(x^k,\{\phi^k_i\})$ ,

\mathbb E\big[T^{k+1}\big]\le\Big(1-\frac1\kappa\Big)T^k ,

with the expectation over the next index only.

Supporting lemmas

Lemma 4 (p. 10), a lower bound combining strong convexity and smoothness; Lemma 1 (pp. 6–7), its average over the components; Lemma 2 (p. 7), which bounds the stale-gradient variance by the table part of $T$ ; and Lemma 3 (p. 7), a second-moment bound for the SAGA step.

Significance

The result. Corollary 1 gives an $\varepsilon$ -accurate iterate in expectation after $O\big((n+L/\mu)\log(1/\varepsilon)\big)$ component-gradient evaluations. This is the complexity of full-gradient descent with the condition number decoupled from $n$ , and it holds in the composite setting, so it covers the lasso and elastic-net problems that SAG's analysis does not reach. The paper notes that the rate improves on the published rates of SAG and SVRG and is within a factor 2 of SDCA's. Theorem 1 is the template of later Lyapunov analyses of variance-reduced methods.

Formalizing it. The result has been proved since 2014, and no machine-checked proof is known to this mission. The work left is to formalize the known proof: the convexity inequalities (Lemmas 4, 1, 2), the variance computation (Lemma 3), the one-step contraction (Theorem 1), and the passage from conditional to total expectation along the random index sequence (Corollary 1). The paper's Lemma 3 has a sign misprint, which the formalization corrects; see the scope section.

Difficulty

The obvious argument for SGD-type methods bounds $\mathbb E\|x^{k+1}-x^*\|^2$ in terms of $\|x^k-x^*\|^2$ alone. That fails here: the variance of the SAGA estimator depends on the stale table points $\phi_i^k$ , which can be far from $x^*$ even when $x^k$ is close. One needs a potential that also measures the table. Balancing the terms of $T$ then requires the four round-bracket coefficients in the paper's display (10) to be non-positive for the specific $\gamma$ , $c$ and an auxiliary $\beta=(2\mu n+L)/L$ . Checking these coefficients is routine but long algebra in $\mu$ , $L$ , $n$ . The composite case adds one step: since $f'(x^*)\neq0$ in general, the argument goes through the fixed-point identity $x^*=\operatorname{prox}^h_\gamma(x^*-\gamma f'(x^*))$ and the non-expansiveness of the proximal operator, neither of which is a numbered result of the paper.

Formalization scope

Space and data. The space is EuclideanSpace ℝ (Fin d). Components are indexed by Fin n (0-based), with 0 < n. The gradients $f_i'$ are given maps with HasGradientAt (f i) (f' i x) x. Strong convexity is Mathlib's StrongConvexOn Set.univ μ, whose modulus $\frac\mu2\|x-y\|^2$ is the paper's.
Regulariser and minimiser. $h$ is real-valued and convex; extended-valued regularisers are out of scope, as on the page. A minimiser $x^*$ of $f+h$ is a hypothesis.
Proximal operator. It is any map $P$ such that $P(y)$ minimises $h(x)+\frac1{2\gamma}\|x-y\|^2$ for every $y$ (IsProxPoint). The minimiser is unique, so $P$ is $\operatorname{prox}^h_\gamma$ .
State and expectation. The state is the pair $(x,\phi)$ . The run after $k$ steps is a deterministic function of the index sequence in Fin k → Fin n. The expectation in Corollary 1 is the average over all $n^k$ sequences, which is exactly the law of $k$ independent uniform indices; no measure theory is involved. Theorem 1's conditional expectation is the average over the next index.
Constants and corrections. Constants are as printed and fixed, not "for some constant" and not "for all small enough steps". Lemma 4 carries the hypothesis $\mu<L$ , which its fractions $1/(L-\mu)$ require. Lemma 3 is stated with $+\gamma f'(x^*)$ , as in its proof and its use in Theorem 1; the printed $-\gamma f'(x^*)$ is false whenever $f'(x^*)\neq0$ .
Trivializing formalizations, ruled out. Taking the proximal step as merely non-expansive, fixing an index sequence instead of averaging over all of them, measuring $x^*$ against $f$ instead of $f+h$ , or restricting Theorem 1 to reachable states changes the theorem and is excluded.
Infrastructure. A complete development needs:
- the co-coercivity inequality for convex functions with Lipschitz gradient;
- existence, uniqueness and non-expansiveness of the proximal map of a finite convex function;
- the optimality condition $x^*=\operatorname{prox}^h_\gamma(x^*-\gamma f'(x^*))$ ;
- finite-sum variance identities.
These pieces are reusable well beyond SAGA, by SVRG, SAG and proximal-gradient analyses. Contributions of any of them, or of proofs of the individual milestones, are welcome.

Selected references

A. Defazio, F. Bach, S. Lacoste-Julien, SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives, NIPS 2014. arXiv:1407.0202
N. Le Roux, M. Schmidt, F. Bach, A Stochastic Gradient Method with an Exponential Convergence Rate for Finite Training Sets, NIPS 2012. arXiv:1202.6258
R. Johnson, T. Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, NIPS 2013. NeurIPS proceedings
L. Xiao, T. Zhang, A Proximal Stochastic Gradient Method with Progressive Variance Reduction, SIAM J. Optim. 24(4), 2014. arXiv:1403.4699
S. Shalev-Shwartz, T. Zhang, Stochastic Dual Coordinate Ascent Methods for Regularized Loss Minimization, JMLR 14, 2013. arXiv:1209.1873
Y. Nesterov, Introductory Lectures on Convex Optimization, Kluwer, 2004. doi:10.1007/978-1-4419-8853-9

11 thms2 active usersReviewed

Discrete Geometry Linear Optimization Operations Research+1·Captain: mikedeng1

Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time 1: The Expected Shadow of a Gaussian-Perturbed Polytope Has Polynomially Many VerticesResearch Paper

Why the shadow of a perturbed polytope matters

The simplex method solves linear programs very fast in practice, yet for most pivot rules there are inputs on which it takes exponentially many steps (Klee and Minty, 1972, for Dantzig's rule; Goldfarb, 1983, for the shadow-vertex rule). Average-case analyses (Borgwardt, 1980s; Smale, 1983) explained good behaviour on random inputs, but random inputs look nothing like real ones. Spielman and Teng introduced smoothed analysis to close this gap: the input is chosen by an adversary and then perturbed by a small Gaussian, and the running time is measured in expectation over the perturbation. They proved that the shadow-vertex simplex method has smoothed complexity polynomial in the number of constraints $n$ , the dimension $d$ and $1/\sigma$ (Spielman–Teng, J. ACM 2004; this mission follows the preprint arXiv:cs/0111050v7). The work received the Gödel Prize (2008) and the Fulkerson Prize (2009).

Timeline. Borgwardt (1977–1987) bounded the expected number of shadow-vertex pivots for rotationally symmetric random data. Spielman and Teng (2001, STOC; journal 2004) proved the first smoothed bound, with a shadow bound of order $nd^3/\sigma^6$ — the theorem of this mission. Deshpande and Spielman (FOCS 2005) improved the shadow bound, Vershynin (2009) reduced the dependence on $n$ to polylogarithmic, and Dadush and Huiberts (STOC 2018) obtained $O(d^2\sqrt{\log n}\,\sigma^{-2})$ for small $\sigma$ .

Setting

Fix $d\ge3$ and $n>d$ . The data are vectors $a_1,\dots,a_n\in\mathbb R^d$ , the constraint vectors of the linear program $\max\langle z|x\rangle$ subject to $\langle a_i|x\rangle\le1$ for all $i$ . Each $a_i$ is a Gaussian of standard deviation $\sigma$ centered at a point $\bar a_i$ with $\|\bar a_i\|\le1$ : it has density

\mu_i(a)=\Big(\tfrac{1}{\sqrt{2\pi}\,\sigma}\Big)^d e^{-\|a-\bar a_i\|^2/2\sigma^2},

and the $a_i$ are independent (joint density $\prod_i\mu_i(a_i)$ ).

For a direction $q\in\mathbb R^d$ , $\mathrm{optSimp}_q(a_1,\dots,a_n)$ is the set of index sets $I\subseteq\{1,\dots,n\}$ with $|I|=d$ such that $(a_i)_{i\in I}$ is linearly independent, the simplex $\triangle(A_I)=\mathrm{ConvHull}(a_i:i\in I)$ is a facet of $\mathrm{ConvHull}(0,a_1,\dots,a_n)$ , and $q$ lies in the cone $\{\sum_{i\in I}\alpha_ia_i:\alpha_i\ge0\}$ . In polar terms, $I$ is the set of tight constraints at the vertex of the feasible polyhedron that maximizes $\langle q|x\rangle$ .

For linearly independent $t,z$ , the shadow $\mathrm{Shadow}_{t,z}(a_1,\dots,a_n)$ is the set of index sets $I$ that belong to $\mathrm{optSimp}_q$ for some nonzero $q\in\mathrm{Span}(t,z)$ . Its size is the number of vertices of the projection of the feasible polyhedron onto the plane $\mathrm{Span}(t,z)$ ; the shadow-vertex method walks along this polygon, one pivot per vertex. Finally

\mathcal D(n,d,\sigma)=\frac{58{,}888{,}678\,nd^3}{\min\big(\sigma,\,1/(3\sqrt{d\ln n})\big)^6}.

Formalization targets

Goal: Theorem 4.0.1 (Shadow Size)

\mathbb E_{a_1,\dots,a_n}\big[\,|\mathrm{Shadow}_{t,z}(a_1,\dots,a_n)|\,\big]\le\mathcal D(n,d,\sigma)

for every $d\ge3$ , $n>d$ , every pair of linearly independent $t,z$ , every $\sigma>0$ and all centers of norm at most $1$ .

Milestones

The milestones follow the paper's proof, leaves first.

Probability tools: the chi-square bound (Corollary 2.4.6), the combination lemma (Lemma 2.3.5), almost polynomial densities (Lemma 2.3.7), and comparing Gaussian tails (Lemma 2.4.11).
Reduction: the measure of the event $P=\{\|a_i\|\le2\ \forall i\}$ (Proposition 4.0.5), and the discretization of the shadow into $m$ equally spaced directions (Lemma 4.0.6).
Angle bound: the probability, conditioned on $P$ , that the ray through a fixed unit vector $q$ passes within angle $\varepsilon$ of the boundary of its optimal facet is $O(nd^3\varepsilon/\sigma^6)$ (Lemma 4.0.7, from Lemma 4.0.11).
Distance and incidence: in Blaschke coordinates $a_i=R_\omega b_i+sq$ , a deterministic split (Lemma 4.0.12), a distance bound (Lemmas 4.1.1–4.1.3) and an angle-of-incidence bound (Lemmas 4.2.1–4.2.3).

Significance

The result. Theorem 4.0.1 is the geometric heart of the smoothed analysis of the simplex method. Section 4.3 of the paper extends it to arbitrary centers, covariances and right-hand sides, and Section 5 combines these extensions with a two-phase method to show that the simplex method has polynomial smoothed complexity. The same shadow bound underlies later analyses of the simplex method, of perturbed polytopes' diameters, and of condition numbers of random linear programs.

Formalizing it. The theorem has been proved, and improved constants are known, but none of this is machine-checked. A formal proof would verify a long and delicate argument: a change of variables of integral geometry (Blaschke's formula), several conditional-density estimates, and explicit constants in the millions. The mission also produces reusable statements about Gaussian vectors and convex hulls of random points.

Difficulty

The obvious approach is to count, for each candidate facet $I$ , the probability that $I$ appears in the shadow; there are $\binom nd$ candidates, so a union bound is exponential in $d$ . The paper avoids this by discretizing the angle of $q$ (Lemma 4.0.6) and bounding, for each fixed direction, the probability that the optimal facet changes within a small angular step. That needs a lower bound on the angle between $q$ and the boundary of its optimal facet, conditioned on the facet being optimal. The conditioning changes the distribution of $a_1,\dots,a_d$ , so the bound cannot come from the Gaussian density alone. The proof changes variables to the facet's normal $\omega$ , offset $s$ and in-plane coordinates $b_i$ (Corollary 2.5.3), whose Jacobian contributes the factors $\langle\omega|q\rangle$ and $\mathrm{Vol}(\triangle(b))$ . It then shows that both the distance of the origin to a face of the in-plane simplex and the angle of incidence $\langle\omega|q\rangle$ are unlikely to be small. Measure-theoretic bookkeeping is as hard as the geometry: densities known only up to normalization, conditioning on events of positive measure, and the measure-zero degeneracies the paper sets aside.

Formalization scope

Points live in EuclideanSpace ℝ (Fin d). Constraint vectors are indexed by Fin n (0-based), so the paper's $\{1,\dots,d\}$ is $\{i:i<d\}$ . The Gaussian of standard deviation $\sigma$ centered at $c$ is Lebesgue measure with the density above, and the joint law is the product measure. Lemma 4.0.6 also uses Mathlib's multivariateGaussian with a positive definite covariance. Expectations of shadow sizes are lower Lebesgue integrals of $[0,\infty]$ -valued counts, and their measurability is part of each conclusion. "Density proportional to $\nu$ " and conditional probabilities are stated cross-multiplied, $\int_{E}\nu\le\text{bound}\cdot\int\nu$ , so no $0/0$ appears.

The shadow is the set of index sets $I$ , and the direction $q=0$ is excluded. Including it would add every facet of $\mathrm{ConvHull}(0,a_1,\dots,a_n)$ to the shadow, since $0$ lies in every cone, and make the goal false. $\mathrm{ang}(q,\emptyset)=\infty$ is represented exactly in $[0,\infty]$ , never by a real infimum. Where the paper omits a hypothesis it uses, it is added and recorded in the item: the standing assumptions $d\ge3$ , $n>d$ and $\sigma\le1/(3\sqrt{d\ln n})$ (Lemma 4.2.3 is false without a bound on $\sigma$ ), unit length of the reference vector $q$ , $s\ge0$ , and $\varepsilon>0$ for strict inequalities. Lemma 2.3.7 is stated with $\le$ rather than the page's $<$ , which fails in an edge case.

Infrastructure a complete development needs: Gaussian tail and chi-square estimates; faces and facets of convex hulls; the Blaschke change of variables and the latitude–longitude change of variables on the sphere (not in Mathlib); surface measure on $S^{d-1}$ (Mathlib's Measure.toSphere); and the disintegration of the joint law used in the combination lemma. The Gaussian estimates, the combination lemma and the Blaschke formula are useful beyond this mission. Proofs of any milestone, and of supporting lemmas such as the change-of-variables formulas, are welcome.

Selected references

D. A. Spielman, S.-H. Teng, Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time, arXiv:cs/0111050v7, 2003. https://arxiv.org/abs/cs/0111050v7
D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: Why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. https://doi.org/10.1145/990308.990310
K. H. Borgwardt, The Simplex Method: A Probabilistic Analysis, Springer, 1987.
V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, 159–175.
A. Deshpande, D. A. Spielman, Improved smoothed analysis of the shadow vertex simplex method, FOCS 2005, 387–396.
R. Vershynin, Beyond Hirsch conjecture: walks on random polytopes and smoothed complexity of the simplex method, SIAM J. Comput. 39(2):646–678, 2009. https://doi.org/10.1137/070683386
D. Dadush, S. Huiberts, A friendly smoothed analysis of the simplex method, STOC 2018; arXiv:1711.05667. https://arxiv.org/abs/1711.05667

29 thms2 active usersReviewed

Operations Research Theoretical Computer Science·Captain: mikedeng1

A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time: Minimal Optimal Predecessor Lists Are Characterized by Strictly Increasing BreakpointsResearch Paper

Motivation

The dynamic lot size model asks when, and how much, to order of a single item over a planning horizon of $n$ periods with known, time-varying demands, setup costs, unit order costs and holding costs. It is the textbook model of production planning and the building block of material requirements planning, multi-item scheduling and many decomposition schemes for larger supply-chain problems.

Wagner and Whitin (1958) showed that some optimal policy orders only when inventory is zero, which turns the problem into a shortest-path recursion with $O(n^2)$ running time. For more than thirty years this was the standard algorithm. In 1991 three groups independently reduced the complexity: Federgruen and Tzur (Management Science 37(8), 1991), Wagelmans, van Hoesel and Kolen (Operations Research 40, 1992) and Aggarwal and Park (Operations Research 41, 1993). Each obtained $O(n \log n)$ in general and $O(n)$ under special cost structures. The Federgruen–Tzur algorithm is a forward algorithm: at iteration $j$ it keeps a short list of periods that could still be the best last setup period for some future horizon, and updates it by local tests on neighbouring entries. This mission formalizes the theorem that justifies those tests.

Setting

For periods $i = 1, 2, \dots$ let $d_i$ be the demand, $K_i$ the setup cost, $c_i$ the variable per unit order cost and $h_i$ the cost of carrying a unit of inventory at the end of period $i$ . Write $D(i) = \sum_{k=1}^{i} d_k$ and $H(i) = \sum_{k=1}^{i} h_k$ , so $D(0) = H(0) = 0$ . For $i < j$ let $c_{ij} = c_i + h_i + \dots + h_{j-1}$ , let $\tilde C(i) = c_i - H(i-1)$ , and let

S(i, j) = \sum_{r=i}^{j-1} h_r\,\bigl(D(j) - D(r)\bigr)

be the carrying cost of an order placed in period $i$ that covers the demands of periods $i, \dots, j$ .

The costs are given by the zero-inventory recursion (2): $F(0) = 0$ and, for $1 \le l \le t$ ,

F(l, t) = F(l-1) + K_l + S(l, t) + c_l\,[D(t) - D(l-1)], \qquad F(t) = \min_{1 \le l \le t} F(l, t).

$F(l, t)$ is the cost of the first $t$ periods when the last setup is in period $l$ .

For two periods $k < l$ the difference $\Delta_{k,l}(t) = F(k,t) - F(l,t)$ is affine in $D(t)$ , with intercept $A(k,l)$ given by (4) and slope $c_{k,l} - c_l = \tilde C(k) - \tilde C(l)$ . Its root $G(k,l)$ is defined by (5): $A(k,l)/(\tilde C(l) - \tilde C(k))$ when the slopes differ, and $+\infty$ or $-\infty$ according to the sign of $A(k,l)$ when they agree. It is extended symmetrically, $G(l,k) = G(k,l)$ .

At iteration $j$ the future demands are unknown, so a future horizon has a potential cumulative demand $x \ge D(j)$ . The $j$ th Minimal Optimal Predecessors list $\Omega(j)$ is the set of periods $l \le j$ that are the lowest-index optimal last setup period, among $\{1, \dots, j\}$ , for every potential cumulative demand in some open interval above $D(j)$ .

Formalization targets

Goal: Theorem 1(a)

Let $j \ge 1$ and let $S = \{i_1, \dots, i_r\}$ with $\Omega(j) \subseteq S \subseteq \{1, \dots, j\}$ , ranked so that $\tilde C(i_1) \ge \dots \ge \tilde C(i_r)$ , with equal $\tilde C$ -values in ascending order of index. Put $g(1) = D(j)$ and $g(l) = G(i_l, i_{l-1})$ for $l = 2, \dots, r$ . Then

S = \Omega(j) \iff g(1) < g(2) < \dots < g(r) < \infty. \tag{6}

Milestones

In attack order:

identity (1a) for the carrying costs;
Lemma 2(a)–(d), the linearity of $\Delta_{k,l}$ and the sign test against its root $G(k,l)$ ;
the claim that $\Omega(j)$ contains an optimal last setup period for the horizon $j$ ;
the strict chains (7)–(8) of the Appendix;
Theorem 1(b), that under (6) the first entry $i_1$ is an optimal last setup period $l(j)$ ;
Theorem 1(c)(i)–(iii), the three elimination rules: $g(2) \le D(j)$ removes $i_1$ , $g(k+1) \le g(k)$ removes $i_k$ , and $g(r) = \infty$ removes $i_r$ .

A supporting item potCost_spec certifies that the potential costs used to define $\Omega(j)$ agree with the paper's $F(l,t)$ , up to a term that does not depend on $l$ .

Significance

Theorem 1 is what makes the forward algorithm correct. Part (a) reduces the minimality of a candidate list to a condition on consecutive pairs of a sorted list. Part (c) says which entry to delete when the condition fails. Part (b) says where to read off the optimal last setup period. With these, $\Omega(j)$ is maintained by deletions at the ends and in the interior of a list ordered by $\tilde C$ , and each period is inserted and deleted at most once; the $O(n \log n)$ bound, and the $O(n)$ bound under the paper's special cost structures, follow from this bookkeeping. The same lower-envelope reasoning appears in the other 1991–1993 algorithms and in later extensions to backlogging and capacitated variants.

The result has a complete published proof. To our knowledge there is no machine-checked development of the Wagner–Whitin recursion or of any of the fast lot-sizing algorithms. This mission produces the model, the breakpoints and the Minimal Optimal Predecessors lists as reusable definitions, and a checked proof of the characterization. It also records two small corrections that a formal reading forces on the printed text (see Formalization scope).

Difficulty

Each piece in isolation is elementary algebra on affine functions. The difficulty is in the combinatorics of the lower envelope with ties. The natural argument "consecutive breakpoints increase, so each line owns an interval" must handle three things:

equal slopes, where $G = \pm\infty$ ;
several lines meeting at one point;
the lowest-index tie-breaking that makes $\Omega(j)$ minimal.

The "only if" direction needs every failure of (6) to be traced to an element that is never the unique lowest-index optimum on an interval. Ties are exactly where the printed definition of $\Omega(j)$ , read literally at a single demand value, breaks the theorem. A proof that ignores ties proves a statement that is false.

Formalization scope

Data and costs. The data are four functions $\mathbb N \to \mathbb R$ bundled in a structure; values at index $0$ are unused, and no sign conditions are imposed. $F$ is defined by the recursion (2) with $F(0) = 0$ . Its identification with the minimum cost over all feasible policies is the paper's Lemma 1 (Wagner–Whitin), which is not part of this mission. The horizon $n$ is not a parameter.
Breakpoints. $G$ and the critical values $g(\cdot)$ take values in EReal, so $\pm\infty$ are kept distinct from every real number. The final " $< \infty$ " of (6) is part of the condition.
Ranked lists. A ranked set is a duplicate-free List ℕ. Lean lists are 0-based, so the paper's $i_{m+1}$ and $g(m+1)$ are entry $m$ and gval j L m.
Disclosed change 1, $\Omega(j)$ . The page asks for a single potential cumulative demand $D \ge D(j)$ at which $l$ is the lowest-index optimum. With that reading, Theorem 1(a) "only if" and Theorem 1(c) fail when two lines tie exactly at a breakpoint (an explicit five-period instance is in the definition's note). The formalization requires $l$ to be the lowest-index optimum on a nondegenerate open interval of potential demands above $D(j)$ . This is the paper's own description of the list on p. 915: "the unique optimal last setup period for any horizon … with potential cumulative demand $g(k) < D < g(k+1)$ ".
Disclosed change 2, Lemma 2(d). The printed hypothesis " $c_{k,l} < c_l$ " duplicates part (c) and is read as " $c_{k,l} = c_l$ ". The equivalence " $\Delta_{k,l} \ge 0$ iff $D(t) \ge G(k,l)$ " is stated under $A(k,l) \ne 0$ , since $A(k,l) = 0$ gives $G = +\infty$ by (5).
Ruling out trivial formalizations. The hypotheses of the goal are satisfiable for every $j \ge 1$ : rank $\{1, \dots, j\}$ itself. $\Omega(j)$ is nonempty (a milestone). $F(t)$ for $t \ge 1$ is a minimum over the nonempty set $\{1, \dots, t\}$ , never a default value. $G$ is never replaced by a real-valued junk value at equal slopes.
Out of scope. Lemma 1, Lemma 3, Corollaries 1–5, Theorem 2, the Algorithm's pseudo-code and its complexity analysis, and the submodularity discussion of §5.
Reusable infrastructure. The model, the recursion (2), $A$ , $G$ and $\Omega(j)$ can be reused for the paper's algorithmic results and for related lot-sizing papers. Proofs of the milestones, in any order, are welcome.

Selected references

A. Federgruen and M. Tzur, A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time, Management Science 37(8):909–925, 1991. https://doi.org/10.1287/mnsc.37.8.909
H. M. Wagner and T. M. Whitin, Dynamic Version of the Economic Lot Size Model, Management Science 5(1):89–96, 1958. https://doi.org/10.1287/mnsc.5.1.89
A. Wagelmans, S. van Hoesel and A. Kolen, Economic Lot-Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40(1-supplement-1):S145–S156, 1992. https://doi.org/10.1287/opre.40.1.S145
A. Aggarwal and J. K. Park, Improved Algorithms for Economic Lot Size Problems, Operations Research 41(3):549–571, 1993. https://doi.org/10.1287/opre.41.3.549

16 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems: Algorithm OPT Returns an Optimal Reorder Point and Order QuantityResearch Paper

Motivation

(r, Q) policies are the standard replenishment rule for a single item under continuous review: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point $r$ , an order of size $Q$ is placed. They are known to be optimal in the classical models with Poisson or compound renewal demand, constant or exogenous lead times and full backlogging, and they are used widely in practice and in multi-item and multi-echelon systems where they are applied item by item.

For decades, computing an optimal pair $(r, Q)$ exactly was not routine. The textbook treatment of Hadley and Whitin (1963) gives approximations; as Browne and Zipkin (1991) put it, "until recently, there was no reliable, straightforward method for computing an optimal (r, Q) policy, even in the simple case of Poisson demand processes." Many heuristics were proposed (surveyed by Lee and Nahmias, 1989); the only exact procedure in circulation was in Zipkin's classnotes, based on a result of Sahin (1982).

Federgruen and Zheng (1992) give a short exact algorithm, Algorithm OPT, whose work is linear in the optimal order quantity $Q^*$ . It rests only on the form of the cost, not on a particular demand model.

Setting

Inventory positions are integers (demand arrives unit by unit). A fixed cost $\kappa>0$ is charged per order, and $G:\mathbb Z\to\mathbb R$ is the expected holding and backlogging cost rate as a function of the inventory position $y$ . In all the models of the paper the long-run average cost of the $(r,Q)$ policy, for an integer $r$ and an integer $Q\ge1$ , has the form

C(r,Q)=\Big[\kappa+\sum_{y=r+1}^{r+Q}G(y)\Big]\Big/Q. \tag{1}

The paper's standing assumptions on $G$ are:

$-G$ is unimodal: there is an integer $m$ with $G$ nonincreasing on $\{y\le m\}$ and nondecreasing on $\{y\ge m\}$ (flat stretches allowed);
$\lim_{|y|\to\infty}G(y)=\infty$ .

The sequence $y_Q$ . Let $y_1$ be an integer minimizing $G$ . Given $y_1,\dots,y_Q$ , let $L(Q)=\min\{y_1,\dots,y_Q\}$ and $R(Q)=\max\{y_1,\dots,y_Q\}$ , and set

y_{Q+1}=\begin{cases}L(Q)-1 & \text{if } G(L(Q)-1)\le G(R(Q)+1),\\ R(Q)+1 & \text{otherwise.}\end{cases}

So the window $[L(Q),R(Q)]$ grows by one point at a time towards the smaller neighbouring value, ties going left. Write $r^*(Q)$ for an optimal reorder point for a given $Q$ , and

C^*(Q)=\Big[\kappa+\sum_{i=1}^{Q}G(y_i)\Big]\Big/Q .

Algorithm OPT, Step 1. Variables $S,Q,C^*,r,R$ start at $S=\kappa+G(y_1)$ , $Q=1$ , $C^*=S$ , $r=y_1-1$ , $R=y_1+1$ . Each pass compares $G(r)$ and $G(R)$ ; on the smaller side (left on ties) it stops if $C^*$ is at most that value, and otherwise adds the value to $S$ and moves $r$ one step left or $R$ one step right; then $Q:=Q+1$ and $C^*:=S/Q$ . The output is the final $(r,Q)$ .

Formalization targets

Goal: Theorem 1

Under the standing assumptions, Step 1 of Algorithm OPT, started from any global minimizer $y_1$ of $G$ , stops after finitely many passes, and its output $(r,Q)$ satisfies $Q\ge1$ and

C(r,Q)\le C(r',Q')\qquad\text{for all integers } r' \text{ and all integers } Q'\ge 1 .

The goal fixes no constants and no demand model: it is a statement about every $G$ satisfying the standing assumptions.

Milestones, in proof order

§2, p. 811: $\{y_1,\dots,y_Q\}$ is the contiguous block $[L(Q),R(Q)]$ of $Q$ integers and carries the $Q$ smallest values of $G$ .
Figure 1 (p. 809): $y_{Q+1}$ has the least $G$ -value outside the window; in particular $G(y_1)\le G(y_2)\le\cdots$ .
Lemma 1: $L(Q)-1$ is an optimal reorder point for $Q$ .
Corollary 1: $r^*(Q)-1\le r^*(Q+1)\le r^*(Q)$ .
Display before (6): $\min_r C(r,Q)=C^*(Q)$ .
(6): $C^*(Q+1)=[QC^*(Q)+G(y_{Q+1})]/(Q+1)$ , and $C^*(Q+1)<C^*(Q)$ iff $G(y_{Q+1})<C^*(Q)$ .
Lemma 2: the smallest $q$ with $C^*(q)\le G(y_{q+1})$ exists and is an optimal order size.
Step 1 tracks the sequence: from the state $(\kappa+\sum_{i\le Q}G(y_i),\,Q,\,C^*(Q),\,L(Q)-1,\,R(Q)+1)$ one pass stops with $(L(Q)-1,Q)$ exactly when $C^*(Q)\le G(y_{Q+1})$ and otherwise moves to the same state for $Q+1$ .

Significance

The result turns the joint minimization of (1) over $(r,Q)\in\mathbb Z\times\mathbb Z_{\ge1}$ , an unbounded two-dimensional integer problem, into a single scan whose length is $Q^*$ plus the distance to the minimizer of $G$ . Because it uses only the form (1) and the unimodality of $-G$ , it applies at once to Poisson and compound Poisson demand, to stochastic lead times with an equilibrium lead-time demand, and to cost structures with stockout penalties; the paper also notes extensions to $(r,nQ)$ policies. Lemma 1 and Corollary 1 additionally give the structure of the optimal reorder point as a function of $Q$ .

The result has been proved on paper since 1992. What this mission adds is a machine-checked proof of the algorithm's correctness for general $G$ under exactly the paper's hypotheses. The platform already has the linear-cost special case of the underlying lemmas for one discrete demand model (InventoryControl.rq_discrete_recursion, rq_discrete_joint_optimal), but with $C(Q)$ and $Q^*$ given as hypotheses and no algorithm; nothing on the platform states the algorithm or treats general unimodal $-G$ .

Difficulty

The obvious argument says: for fixed $Q$ the sum in (1) should cover the $Q$ smallest values of $G$ , and the greedy window collects exactly those. Both halves need care on the integers with flat stretches of $G$ : "the $Q$ smallest values" is ambiguous under ties, and the claim that a greedy window holds them relies on $y_1$ being a global minimizer together with the unimodality of $-G$ , not on convexity.

The stopping rule is the second point. Lemma 2 looks like a first-order condition, but $C^*(\cdot)$ need not be convex; optimality of the first stopping $q$ for all larger $Q$ uses that the values $G(y_i)$ are nondecreasing along the sequence, which the paper uses without stating. Termination of the algorithm is not discussed on the page; it needs $G\to\infty$ , and fails for constant $G$ .

Finally, the goal is about an imperative loop. Connecting its five variables to $y_Q$ , $C^*(Q)$ and $L(Q)$ is an invariant argument that has to match the tie-breaking and the non-strict stopping tests exactly.

Formalization scope

Types. $G:\mathbb Z\to\mathbb R$ , $\kappa\in\mathbb R$ with $\kappa>0$ , reorder points in $\mathbb Z$ , order quantities in $\mathbb N$ with $Q\ge1$ required wherever a cost appears. Lean's $x/0=0$ makes $C(r,0)=0$ , so optimality is always quantified over $Q'\ge1$ and the goal asserts that the returned $Q$ is $\ge1$ .
Assumptions. " $-G$ unimodal" is NegUnimodal G: $\exists m$ , $G$ antitone on $(-\infty,m]$ and monotone on $[m,\infty)$ . " $\lim_{|y|\to\infty}G=\infty$ " is Coercive G: $G\to+\infty$ along atBot and atTop. Mathlib's QuasiconvexOn ℤ is not used: over $\mathbb Z$ -weights it holds for every function.
The sequence. $L(Q),R(Q)$ are defined by recursion on the window, and $y$ is 1-based with an unused value at index 0; that $L,R$ are the minimum and maximum of $\{y_1,\dots,y_Q\}$ , as the paper defines them, is the first milestone.
The algorithm. Step 1 is transcribed literally, including $G(r)\le G(R)$ → left and the non-strict tests $C^*\le G(r)$ , $C^*\le G(R)$ ; $G$ is evaluated directly instead of through the $\Delta G$ bookkeeping. The loop runs with a pass budget and returns nothing when the budget runs out; the goal states that for every large enough budget it returns an optimal pair.
Step 0 is not formalized. It scans $L=0,1,\dots$ for the first $L$ with $\Delta G(L)\ge0$ , under the paper's simplification $y_1>0$ ; under unimodality alone it can stop on a plateau before the minimum. The goal starts Step 1 from a given global minimizer $y_1$ , which is the paper's own §2 setup and matches its p. 812 remark that Step 0 may be replaced by a bisection search.
Not formalized: Theorem 1's second sentence (the operation count), the derivations of (1) for specific demand models, and (5).
Corrected slips. The printed proof of Lemma 2 writes $C(Q)-C(Q^*)$ with $C^*(Q)$ inside the bracket; the correct identity has $C^*(Q)-C^*(Q^*)$ and $C^*(Q^*)$ . Lemma 2's " $Q^*$ " is formalized as existence of the smallest $q$ with the property plus its optimality, since minimizers need not be unique; likewise " $r^*(Q)=L(Q)-1$ " means $L(Q)-1$ is an optimal reorder point.
Ruled out. Defining the algorithm's output as an argmin of $C$ , or by searching for Lemma 2's $q$ , would make the goal trivial; the algorithm is defined by its steps. A statement of the form "if the run returns a pair, it is optimal" would be vacuous for a loop that never stops; termination is part of the goal.

Proofs of any milestone are welcome, as are general lemmas on windows of unimodal integer sequences, which are reusable beyond this mission.

Selected references

A. Federgruen and Y.-S. Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808
G. Hadley and T. M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
S. Browne and P. Zipkin, Inventory Models with Continuous, Stochastic Demands, Annals of Applied Probability 1(3):419–435, 1991. https://doi.org/10.1214/aoap/1177005875
H. L. Lee and S. Nahmias, Single-Product, Single-Location Models, in Handbooks in OR & MS vol. 4, 1993 (cited by the paper as a 1989 working paper).
I. Sahin, On the Objective Function Behavior in (s, S) Inventory Models, Operations Research 30(4):709–724, 1982. https://doi.org/10.1287/opre.30.4.709

10 thms2 active usersReviewed

Convex Optimization Linear algebra Operations Research·Captain: mikedeng1

A Nonlinear Programming Algorithm for Solving Semidefinite Programs via Low-rank Factorization: A Regular Local Minimum That Stays Locally Minimal After Adding a Zero Column Solves the SDPResearch Paper

Motivation

Semidefinite programs (SDPs) arise as convex relaxations of combinatorial problems such as maximum cut and the Lovász theta function, and in control and eigenvalue optimization. Interior-point methods solve them reliably but manipulate dense $n\times n$ matrices, which limits the size of the instances they can handle. Burer and Monteiro (Math. Program. 95 (2003)) proposed replacing the matrix variable $X\succeq 0$ by a factorization $X=RR^{T}$ with $R$ having only $r$ columns, and solving the resulting nonconvex program by a first-order augmented Lagrangian method. The approach rests on a theorem of Barvinok (1995) and Pataki (1998): an SDP with $m$ linear constraints has an optimal solution of rank $r$ with $r(r+1)/2\le m$ , so a small number of columns suffices.

Because the factorized problem is nonconvex, a local minimum it returns is not automatically a solution of the SDP. Section 2 of the paper gives conditions under which it is. This mission formalizes those conditions, culminating in Proposition 2.5, which justifies the paper's strategy of increasing the rank one column at a time.

Setting

For real $p\times q$ matrices, the trace inner product is $A\bullet B=\operatorname{trace}(A^{T}B)$ . The data are symmetric matrices $C, A_1,\dots,A_m\in\mathcal S^n$ and a vector $b\in\mathbb R^m$ . The primal SDP and dual SDP are

\text{(1)}\quad \min\{C\bullet X : A_i\bullet X=b_i,\ i=1,\dots,m,\ X\succeq0\},\qquad \text{(3)}\quad \max\Big\{b^{T}y : S=C-\sum_{i=1}^m y_iA_i,\ S\succeq0\Big\}.

The standing assumptions of the paper are that $A_1,\dots,A_m$ are linearly independent and that there are feasible $X^*$ and $(S^*,y^*)$ with $C\bullet X^*=b^{T}y^*$ .

For a positive integer $r\le n$ , the low-rank program is

(N_r)\qquad \min\{C\bullet(RR^{T}) : A_i\bullet(RR^{T})=b_i,\ i=1,\dots,m,\ R\in\mathbb R^{n\times r}\}.

Its Lagrangian is $L(R,y)=C\bullet(RR^{T})-\sum_i y_i(A_i\bullet(RR^{T})-b_i)$ , and $S(y)=C-\sum_i y_iA_i$ . A feasible $R$ is a local minimum if it minimizes the objective among nearby feasible points; it is a regular point if $A_1R,\dots,A_mR$ are linearly independent; it is a stationary point with multiplier $y$ if $\nabla_RL(R,y)=0$ . The injection of $R\in\mathbb R^{n\times r}$ is $\hat R=[\,R\ \ 0\,]\in\mathbb R^{n\times(r+1)}$ , obtained by appending a zero column.

Formalization targets

Goal: Proposition 2.5

Let $r<n$ and let $R^*$ be a regular local minimum of $(N_r)$ with multiplier $y^*$ , $S^*=S(y^*)$ , $S^*R^*=0$ . If $\hat R$ is a local minimum of $(N_{r+1})$ , then

X^*=R^*(R^*)^{T}\ \text{solves (1)}\quad\text{and}\quad (S^*,y^*)\ \text{solves (3)}.

Milestones

The derivative formulas (9): $\nabla_R(A_i\bullet(RR^T)-b_i)=2A_iR$ , $\nabla_RL(R,y)=2SR$ , and $L''_{RR}(R,y)[D,D]=2S\bullet(DD^T)$ .
Proposition 2.3: at a regular local minimum of $(N_r)$ there is a unique $y^*$ with $S^*R^*=0$ , and $S^*\bullet(DD^T)\ge0$ for every $D$ with $A_iR^*\bullet D=0$ for all $i$ .
Proposition 2.1: feasible $X$ and $(S,y)$ are simultaneously optimal if and only if $X\bullet S=0$ .
Proposition 2.4: a stationary point of $(N_r)$ whose $S^*$ is positive semidefinite gives optimal $X^*=R^*R^{*T}$ and $(S^*,y^*)$ .

Significance

Proposition 2.5 is a certificate of global optimality for a nonconvex problem obtained from local information alone. It is the basis of the rank-increase scheme described on p. 8 of the paper: compute a local minimum of $(N_r)$ for a small $r$ ; if the zero-column extension is still a local minimum of $(N_{r+1})$ , the current point solves the SDP; otherwise a better point of $(N_{r+1})$ exists and $r$ is increased. Proposition 2.4 gives the companion test, valid for every $r$ : positive semidefiniteness of the multiplier matrix at a stationary point. These statements underlie the later convergence analysis of the method (Burer & Monteiro 2005) and the literature on benign landscapes of low-rank SDP formulations (Boumal, Voroninski & Bandeira 2016).

The results are proved in the paper. What this mission adds is a machine-checked version of the full chain from the standard-form SDP to the rank-increase certificate, including the matrix calculus (9), the first- and second-order necessary conditions for an equality-constrained program over rectangular matrices, and SDP complementary slackness in standard form. No machine-checked proof of these results is recorded in Mathlib or on the platform.

Difficulty

The SDP side (Propositions 2.1 and 2.4) is linear algebra: weak duality and the fact that the trace inner product of two positive semidefinite matrices is nonnegative. The substance lies in Proposition 2.3. The feasible set of $(N_r)$ is a variety cut out by $m$ quadratic equations, and the multiplier rule and, especially, the second-order necessary condition require a constraint qualification and a curve in the feasible set realizing every tangent direction. Mathlib provides a first-order Lagrange multiplier rule, but not the second-order condition on the tangent space. A naive attempt to read Proposition 2.5 off Proposition 2.4 fails: local minimality of $R^*$ alone does not make $S^*$ positive semidefinite (when $r$ is below the minimal optimal rank, it is not); the hypothesis on $(N_{r+1})$ is indispensable.

Formalization scope

Matrices are Matrix (Fin n) (Fin r) ℝ with 0-based indices. The trace inner product is frob A B = trace(Aᵀ * B), defined for rectangular matrices. The data carry explicit symmetry hypotheses C.IsSymm and (A i).IsSymm; without them the formulas (9) are false. Primal feasibility uses Mathlib's PosSemidef, which over $\mathbb R$ includes symmetry. Optimality for (1) and (3) is defined relative to their entire feasible sets. The standing assumptions are a separate predicate carried as a hypothesis by Propositions 2.1, 2.3, 2.4 and 2.5, and every statement about $(N_r)$ carries $0<r$ and $r\le n$ (or $r<n$ ). Gradients are Fréchet derivatives under the Frobenius norm, identified with matrices through the trace inner product; local minima use IsLocalMinOn on the feasible set of $(N_r)$ together with feasibility. The injection appends the zero column as the last column.

The statement admits several trivializing encodings, all excluded here: optimality defined relative to the factorized feasible set instead of the whole SDP, an empty or unconstrained $(N_r)$ (an unconstrained local minimum or a local minimum without feasibility), a stationarity notion that already includes $S\succeq0$ , and an injection other than the zero-column extension.

A complete development needs the matrix calculus of $R\mapsto RR^{T}$ , a second-order necessary optimality condition under linear independence of the constraint gradients, and standard-form SDP weak duality and complementary slackness; all of these are reusable well beyond this mission. Proofs of individual milestones, in particular the derivative formulas and Proposition 2.4, are welcome independently of the goal.

Selected references

S. Burer and R. D. C. Monteiro, A nonlinear programming algorithm for solving semidefinite programs via low-rank factorization, Mathematical Programming 95 (2003), 329–357. https://doi.org/10.1007/s10107-002-0352-8 (statements cited from the authors' manuscript of March 9, 2001)
A. Barvinok, Problems of distance geometry and convex properties of quadratic maps, Discrete & Computational Geometry 13 (1995), 189–202. https://doi.org/10.1007/BF02574037
G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues, Mathematics of Operations Research 23 (1998), 339–358. https://doi.org/10.1287/moor.23.2.339
R. D. C. Monteiro and M. Todd, Path-following methods for semidefinite programming, in Handbook of Semidefinite Programming, Kluwer, 2000 (source of Proposition 2.1).
S. Burer and R. D. C. Monteiro, Local minima and convergence in low-rank semidefinite programming, Mathematical Programming 103 (2005), 427–444. https://doi.org/10.1007/s10107-004-0564-1
N. Boumal, V. Voroninski and A. S. Bandeira, The non-convex Burer–Monteiro approach works on smooth semidefinite programs, NeurIPS 2016. https://arxiv.org/abs/1606.04970

10 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research·Captain: mikedeng1

On Sequential Decisions and Markov Chains 3: A Deterministic Stationary Procedure Minimizes the Ratio of Two Long-Run Average CostsResearch Paper

Motivation

Many controlled systems are judged by a ratio of two long-run quantities rather than by a single one: cost per unit of output, cost per unit of time when the time spent in a state depends on the decision, cost per customer served, or expected cost per cycle of a renewal process. In a finite Markov decision model each of these is a quotient of two average costs per unit time. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (DOI 10.1287/mnsc.9.1.16) introduced this ratio-of-costs criterion in its §4, prompted by the fractional linear program that its §3 uses to solve the total-cost problem as a linear program, and pointed to Klein's work on maintenance policies as an example of the problem.

The paper's §4 first observes that, restricted to stationary randomized procedures, the ratio criterion is a ratio of two linear functions of the stationary state-decision frequencies, so it can be minimized by the fractional linear programming lemma of §3. The question it then raises is the one this mission formalizes: is the procedure optimal over stationary procedures also optimal over all procedures, including history-dependent and randomized ones? Derman's Theorem 3 answers yes under an irreducibility assumption, by reducing the ratio problem to a family of ordinary average-cost problems with costs of either sign.

Timeline, as far as it bears on this mission:

1960: Manne, Linear Programming and Sequential Decisions, shows that linear programming applies to the average-cost problem, in the context of an inventory problem; Wagner, On the Optimality of Pure Strategies, shows by linear programming that a deterministic stationary procedure is optimal for it.
1960: Howard, Dynamic Programming and Markov Processes, gives policy iteration for the average-cost problem over stationary procedures.
1962: Derman proves that a deterministic stationary procedure is optimal over all procedures for the average-cost criterion (Theorem 1), formulates the average and total cost problems as linear programs under irreducibility assumptions (Theorem 2), and extends the optimality of deterministic stationary procedures to the ratio criterion (Theorem 3).
1962: Klein, Inspection-Maintenance-Replacement Schedules Under Markovian Deterioration, gives a problem of the ratio type (cited by Derman, p. 18).
1963: Jewell, Markov-renewal programming, treats the gain rate (reward per unit sojourn time) of semi-Markov decision processes, over stationary policies.

Setting

A system is observed at times $t = 0, 1, \dots$ in one of finitely many states $0, \dots, L$ . After each observation one of the decisions $d_1, \dots, d_K$ is made, all of them available in every state. If the system is in state $i$ and decision $d_k$ is made, the next state is $j$ with probability $q_{ij}(k) \ge 0$ , where $\sum_j q_{ij}(k) = 1$ .

A procedure $R$ chooses the decision at time $t$ at random, with probabilities $D_k(X_0, \Delta_0, \dots, X_t)$ that may depend on the whole past; the class of all procedures is $C$ . The class $C'$ consists of the stationary randomized procedures, for which the probability of $d_k$ in state $i$ is a fixed number $D_{ik}$ , whatever the past and the time. The class $C''$ consists of the deterministic stationary procedures, those of $C'$ with every $D_{ik} \in \{0, 1\}$ ; it is finite. A procedure of $C'$ turns the states into a Markov chain with transition probabilities $p_{ij} = \sum_k q_{ij}(k) D_{ik}$ .

Let $w'_{ik} > 0$ and $w''_{ik} > 0$ be two sets of costs incurred when decision $d_k$ is made in state $i$ . For a fixed procedure $R$ started at $X_0 = i$ , let $W'_t$ and $W''_t$ be the expected costs at time $t$ . The ratio criterion is

\psi_R(i) = \limsup_{T\to\infty} \frac{\sum_{t=0}^{T} W'_t}{\sum_{t=0}^{T} W''_t}.

For a single cost set $w$ with expected costs $W_t$ , the average cost per unit time is $Q_R(i) = \limsup_{T\to\infty} \frac1T \sum_{t=0}^{T} W_t$ .

Assumption A says that for every procedure of $C'$ all states $0, \dots, L$ belong to the same class of the induced Markov chain.

Formalization targets

Goal: Theorem 3 (p. 23)

Under Assumption A, for every initial state $i$ there is a deterministic stationary procedure $R_3 \in C''$ with

\psi_{R_3}(i) = \min_{R \in C} \psi_R(i),

that is, $\psi_{R_3}(i) \le \psi_R(i)$ for every procedure $R \in C$ .

Steps of the proof (milestones)

Theorem 1 (1) for costs of either sign: for every real cost $w$ there is $R_1 \in C''$ with $Q_{R_1}(i) \le Q_R(i)$ for all $R \in C$ and all $i$ .
For any procedure $R$ , $\psi_R(i) \le m$ implies $Q_R(i) \le 0$ for the costs $w_{ik} = w'_{ik} - m\, w''_{ik}$ .
Under Assumption A, for $R^* \in C''$ , $Q_{R^*}(i) \le 0$ for those costs implies $\psi_{R^*}(i) \le m$ .
For $R \in C'$ under Assumption A, $\psi_R(i) = \dfrac{\sum_{s}\sum_k \pi_s D_{sk} w'_{sk}}{\sum_s\sum_k \pi_s D_{sk} w''_{sk}}$ , with $\pi$ the stationary distribution of $(p_{sj})$ .

Significance

Theorem 3 justifies solving ratio problems over stationary procedures only. Combined with the display of milestone 4 it shows that the fractional linear program over stationary state-decision frequencies yields a procedure optimal against every procedure, including those that remember the past or randomize. The same reduction, minimizing $w' - m w''$ and adjusting $m$ , underlies later parametric methods for fractional Markov decision problems and the analysis of semi-Markov decision processes, where the denominator is the expected sojourn time.

All four steps and the theorem are classical and proved on paper. None of them is formalized on Prove2Me: the platform has average-cost optimality statements with nonnegative costs (Sennott's Proposition 6.2.3) and Jewell's gain-rate results restricted to stationary policies, but no statement of a ratio criterion over history-dependent procedures. This mission produces the statement of Theorem 3, the signed-cost version of Theorem 1 that it uses, and the two translation steps between the ratio criterion and the average-cost criterion.

Difficulty

The obvious argument restricts to stationary procedures, where all Cesàro limits exist and the ratio criterion is a ratio of two linear functionals of a stationary distribution. It says nothing about a history-dependent procedure, whose averages $\frac1T\sum_{t\le T} W'_t$ and $\frac1T\sum_{t \le T} W''_t$ need not converge, and for which the limit superior of the ratio is not the ratio of the limits superior. The translation from the ratio to an average cost therefore works in one direction for every procedure (milestone 2) and in the other direction only for stationary ones (milestone 3). The other ingredient, optimality of a deterministic stationary procedure for the average-cost criterion against all procedures with costs of either sign (milestone 1), is the substance of Derman's Theorem 1 and requires a vanishing-discount or equivalent argument over history-dependent procedures.

Formalization scope

The dynamics and the procedures come from the published definitions SennottDP_AvgFinite_Model: the system is an MDC S Act with [Fintype S] [Fintype Act] and the hypothesis ∀ s, M.A s = Finset.univ (all decisions available); the class $C$ is Policy M, history-dependent and randomized; $C''$ is StationaryPolicy M through .toPolicy; the law of the history is histProb. The cost field M.C of that structure plays no role: the costs $w'$ , $w''$ and the signed cost of milestone 1 are explicit real arguments S → Act → ℝ.

The local definitions are: the expected cost at time $t$ for a real cost, as a finite sum over histories of length $t+1$ ; $Q_R(i)$ with Derman's normalization ( $T+1$ terms divided by $T$ ); $\psi_R(i)$ as the limit superior of the ratio of partial sums; the induced matrix $p_{ij}$ ; Assumption A as Matrix.IsIrreducible of $p$ for every row-stochastic $D \ge 0$ ; and membership of a procedure in $C'$ with probabilities $D$ . All limits superior are real, of bounded sequences; positivity of $w'$ and $w''$ is a hypothesis of every statement involving $\psi$ , which keeps the denominators positive.

The goal quantifies "for every initial state there is $R_3$ ", following the proof. The competitors in the goal and in milestone 1 range over all of Policy M; a version comparing only with stationary procedures is a different and easier theorem and does not close this mission. Assumption A is kept in the goal although the proof does not visibly use it, because the theorem states it.

Contributions welcome: proofs of the milestones, in particular the signed-cost Theorem 1 (which may reduce to Sennott's Proposition 6.2.3 by shifting costs by a constant), Cesàro limits for stationary procedures on finite chains (reusable for milestones 3 and 4), and the final compactness argument over the finite class $C''$ .

Selected references

C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
M. Klein, Inspection-Maintenance-Replacement Schedules Under Markovian Deterioration, Management Science 9(1), 1962.
H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3), 1960.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6):938–948, 1963. https://doi.org/10.1287/opre.11.6.938
L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037

7 thms2 active usersReviewed

Convex Optimization Operations Research·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources VII: A Locally Quasiconcave Objective Always Has a Quasistable Optimal ScheduleTextbook

Motivation

Resource-constrained project scheduling asks for start times of the activities of a project that respect precedence-type time lags and the capacities of renewable resources (machines, crews, equipment). Classical project scheduling minimizes the project duration, a regular objective: delaying an activity never helps. Many objectives met in practice are not regular. The resource investment problem minimizes the cost of the resource capacities that must be procured; resource levelling problems minimize fluctuations of resource usage over time; the resource renting problem trades fixed procurement against time-dependent renting costs; net present value and earliness–tardiness objectives reward late as well as early starts. For such objectives the familiar fact that "some active schedule is optimal" fails, and algorithms need another finite set of candidate schedules that is guaranteed to contain an optimum.

Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2), organizes the objective functions of project scheduling into seven classes and pairs each class with a class of schedules that contains an optimal schedule. This mission formalizes §3.3 of that chapter. The classification goes back to Neumann, Nübel and Schwindt (2000) and Zimmermann (2001); the two locally defined classes, and the matching schedule classes of quasiactive and quasistable schedules, are the book's device for covering discontinuous resource-based objectives.

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$ , $n\ge 1$ , where $0$ and $n+1$ are fictitious activities marking the project beginning and completion. Activity $i$ has an integer duration $p_i$ ( $p_0=p_{n+1}=0$ , $p_i>0$ otherwise). The project network has an arc set $E$ with integer weights $\delta_{ij}$ ; a schedule is a vector $S=(S_0,\dots,S_{n+1})$ of real start times with $S_0=0$ , $S\ge 0$ , and it is time-feasible if $S_j-S_i\ge\delta_{ij}$ for all $\langle i,j\rangle\in E$ . A maximum project duration $\bar d\in\mathbb N$ is prescribed through a backward arc $\langle n+1,0\rangle$ of weight $-\bar d$ , so $S_{n+1}\le\bar d$ . Each renewable resource $k$ has capacity $R_k$ , activity $i$ uses $r_{ik}$ units while in progress, and $r_k(S,t)$ is the total usage at time $t$ . The feasible region $\mathcal S$ consists of the time-feasible schedules with $r_k(S,t)\le R_k$ for all $k$ and $t$ .

For an objective function $f:\mathbb R^{n+2}_{\ge 0}\to\mathbb R$ , problem $PS|temp,\bar d|f$ asks for an optimal schedule: some $S\in\mathcal S$ with $f(S)\le f(S')$ for all $S'\in\mathcal S$ .

A schedule induces the strict order $O(S)=\{(i,j)\mid i\ne j,\ S_j\ge S_i+p_i\}$ of precedences it realizes. The equal-order set of $S$ is

\mathcal S_T^{=}(O(S))=\{S'\text{ time-feasible}\mid S'_j\ge S'_i+p_i\ \forall (i,j)\in O(S),\ O(S')=O(S)\},

a polytope with part of its boundary removed. The distinct equal-order sets partition $\mathcal S$ into finitely many pieces.

Schedule classes are defined through shifts. A shift from a feasible $S$ to a feasible $S'\ne S$ is order-preserving if $O(S)\subseteq O(S')$ ; it is a left-shift if $S'\le S$ . Two shifts from $S$ to $S'$ and $S''$ are opposite if $S''-S=\lambda(S'-S)$ with $\lambda<0$ . A feasible schedule is active if no feasible left-shift exists, quasiactive if no order-preserving left-shift exists, stable if no pair of opposite shifts to feasible schedules exists, and quasistable if no pair of opposite order-preserving shifts exists.

Objective classes: $f$ is regular if $S\le S'$ implies $f(S)\le f(S')$ ; quasiconcave on a set $M$ if $f(\lambda S+(1-\lambda)S')\ge\min[f(S),f(S')]$ for $S,S'\in M$ , $\lambda\in[0,1]$ ; lower semicontinuous if $f(S)\le\liminf_{S'\to S}f(S')$ on $\mathbb R^{n+2}_{\ge 0}$ . Then $f$ is locally regular (class 6) if it is lower semicontinuous and regular on every equal-order set $\mathcal S_T^{=}(O(S))$ , $S\in\mathcal S$ , and locally quasiconcave (class 7) if it is lower semicontinuous and quasiconcave on every such set.

Formalization targets

Goal: Theorem 3.3.13

For every locally quasiconcave $f$ ,

\mathcal S\ne\emptyset\ \Longrightarrow\ \exists\,S\ \text{quasistable with}\ f(S)=\min_{S'\in\mathcal S}f(S').

Milestones

Class 1 (§3.3.2): every regular $f$ has an active optimal schedule when $\mathcal S\ne\emptyset$ .
Class 5 (§3.3.6): every quasiconcave $f$ has a stable optimal schedule when $\mathcal S\ne\emptyset$ .
Eq. (3.3.11): the equal-order sets form a finite partition of $\mathcal S$ .
Propositions 3.3.5 and 3.3.6: the resource investment objective $\sum_k c_k\max_t r_k(S,t)$ with $c_k\ge 0$ is constant on each equal-order set and lower semicontinuous, hence locally regular.
Theorem 3.3.9: every locally regular $f$ has a quasiactive optimal schedule when $\mathcal S\ne\emptyset$ .

Significance

Quasiactive and quasistable schedules are finite in number: they are the minimal points and the vertices of the finitely many schedule polytopes. Theorem 3.3.13 therefore turns the minimization of any locally quasiconcave objective over a disconnected, non-convex feasible region into a finite search. Class 7 contains the resource levelling objectives $\sum c_k\sum r_{kt}^2$ and $\sum c_k\sum o_{kt}$ , the total variation of the resource profiles, and the resource renting objective (Propositions 3.3.10 and 3.3.12, and Nübel 2001). The enumeration schemes and decision sets of §3.5–3.7 rest on this result, and Theorem 3.3.9 plays the same role for class 6 (resource investment, changeover times).

The results are proved in the book and the cited papers. As far as a search of the platform shows, none of them, and none of the schedule classes, has a machine-checked formalization; Mathlib supplies lower semicontinuity and quasiconcavity but nothing about schedules. The mission produces a checked version of the classification theorems in the book's exact generality: general time lags (cycles in the network allowed), real start times, and arbitrary objectives given only by their class.

Difficulty

The optimum need not exist a priori: objectives of classes 6 and 7 are discontinuous, and the feasible region is a finite union of polytopes that is in general disconnected. Existence of a minimizer needs compactness of $\mathcal S$ (which depends on the deadline arc and the network's path structure) together with lower semicontinuity.

The main obstacle is that the objective is only controlled piecewise. Quasiconcavity holds on each equal-order set separately, and an equal-order set is not closed: a schedule polytope $\mathcal S_T(O(S))$ also contains schedules inducing strictly larger orders, where the hypothesis on $f$ says nothing about its relation to the values on $\mathcal S_T^{=}(O(S))$ . The obvious argument, taking an optimal schedule and invoking quasiconcavity along the segment of a pair of opposite order-preserving shifts, only relates $f$ at points of one equal-order set, and it does not by itself produce a schedule that admits no such pair at all. The same issue arises for Theorem 3.3.9 with order-preserving left-shifts, which may cross from one equal-order set into another.

Formalization scope

Activities are Fin (n + 2), with 0 and Fin.last (n + 1) fictitious. Start times are real; objective functions are total functions (Fin (n + 2) → ℝ) → ℝ whose regularity, quasiconcavity and lower semicontinuity are required only on the nonnegative orthant (lower semicontinuity is Mathlib's LowerSemicontinuousOn on the orthant). The deadline $S_{n+1}\le\bar d$ is the network's backward arc, as in §3.1. The project structure records the book's standing property (p. 8) that from each node $i$ there is a path to $n+1$ of length at least $p_i$ ; this bounds every activity by $\bar d$ . The resource constraints are imposed for all $t\ge 0$ , which under that property is the book's $0\le t\le\bar d$ . The peak $\max_t r_k(S,t)$ in the resource investment objective is a supremum in $\mathbb N$ over $t\ge 0$ of a nonempty finite set, hence attained.

"Optimal" always means minimizing $f$ over the whole feasible region $\mathcal S$ , and the theorems quantify over every function in the class; a formalization with a fixed objective, or with optimality over a single polytope or a single equal-order set, would be a different and weaker statement. The schedule classes are defined through shifts, never as minimal or extreme points, so no statement is true by definition. The only hypothesis besides the class of $f$ is $\mathcal S\ne\emptyset$ .

The mission restates locally the project model, the induced orders and the shift classes also drafted by the companion missions on schedule classes of this series. Useful contributions beyond the milestones: compactness of $\mathcal S$ and closedness of the schedule polytopes, the representation of $\mathcal S$ as a finite union of feasible order polytopes, and the finiteness of the sets of quasiactive and quasistable schedules.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.3. doi:10.1007/978-3-540-24800-2
K. Neumann, H. Nübel, C. Schwindt, Active and stable project scheduling, Mathematical Methods of Operations Research 52 (2000), cited in the book as Neumann et al. (2000).
J. Zimmermann, Ablauforientiertes Projektmanagement: Modelle, Verfahren und Anwendungen, Gabler, 2001.

11 thms2 active usersReviewed

Bandit Algorithms Convex Optimization Machine Learning+1·Captain: mikedeng1

Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems V: Bandit Convex Optimization with One-Point FeedbackTextbook

Motivation

In bandit convex optimization a forecaster repeatedly picks a point $x_t$ of a convex set $\mathcal K\subseteq\mathbb R^d$ , and an adversary picks a convex loss $\ell_t$ . The forecaster pays $\ell_t(x_t)$ and observes only that number: it never sees the function, its gradient, or its value elsewhere. This is the model of online optimization with only function-value access, as in tuning a system online from measured costs, dynamic pricing with an unknown convex demand-cost curve, or routing with path costs observed only on the route taken. The question is how fast the forecaster can approach the best fixed point in hindsight.

Chapter 6 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2, Foundations and Trends in Machine Learning 5(1), 2012) treats the problem through spherical gradient estimates fed to projected gradient descent. The one-point method is due to Flaxman, Kalai and McMahan (SODA 2005, arXiv:cs/0408007), who obtained an $\mathcal O(n^{3/4})$ regret bound. Agarwal, Dekel and Xiao (COLT 2010) showed that two function evaluations per round allow $\mathcal O(\sqrt n)$ . Whether one-point feedback admits $\sqrt n$ regret was open when the monograph was written (p. 94); Bubeck, Eldan and Lee (STOC 2017, arXiv:1607.03084) later obtained $\sqrt n$ regret up to logarithmic and polynomial-in- $d$ factors for convex losses, with a different and much more involved algorithm.

Setting

Let $\mathbb B=\{x\in\mathbb R^d:\|x\|\le1\}$ be the closed Euclidean unit ball and $\mathbb S=\{x:\|x\|=1\}$ the unit sphere, with unnormalized spherical measure $\sigma$ , so that $\sigma(\mathbb S)=d\,\mathrm{Vol}(\mathbb B)$ . Fix $\delta>0$ . For a loss $\ell$ , the smoothed loss is $\widetilde\ell(x)=\mathbb E\,\ell(x+\delta B)$ with $B$ uniform on $\mathbb B$ .

The set $\mathcal K$ is closed and convex with $r\mathbb B\subseteq\mathcal K\subseteq R\mathbb B$ . The losses $\ell_1,\ell_2,\dots:\mathbb R^d\to\mathbb R$ are $G$ -Lipschitz, differentiable and convex, and are fixed before the game (an oblivious adversary).

OSGD (Online Stochastic Gradient Descent) on a set $\mathcal K'$ with learning rate $\eta$ starts at $x_1=0$ and sets $x_{t+1}=\operatorname{argmin}_{y\in\mathcal K'}\|y-(x_t-\eta\widetilde g_t(x_t))\|$ , where $\widetilde g_t$ is a gradient estimate. With $S_1,S_2,\dots$ independent and uniform on $\mathbb S$ :

the two-point estimate (6.1) is $\widetilde g_t(x_t)=\frac d{2\delta}\big(\ell_t(X_t^+)-\ell_t(X_t^-)\big)S_t$ with $X_t^\pm=x_t\pm\delta S_t$ ; the played point is $X_t^+$ or $X_t^-$ by a fair coin;
the one-point estimate (6.3) is $\widetilde g_t(x_t)=\frac d\delta\,\ell_t(\widetilde X_t)S_t$ with played point $\widetilde X_t=x_t+\delta S_t$ .

OSGD runs on the shrunken set $\mathcal K'=(1-\delta/r)\mathcal K$ , so that the perturbed points stay in $\mathcal K$ . The pseudo-regret is

\overline R_n=\mathbb E\sum_{t=1}^n\ell_t(\widetilde X_t)-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t(x).

Formalization targets

Goal: Theorem 6.2, tuned

If in addition $|\ell_t|\le L$ on $\mathcal K$ , and $\delta=(2n)^{-1/4}\sqrt{RdL/((3+R/r)G)}$ , $\eta=(2n)^{-3/4}\sqrt{R^3/(dL(3+R/r)G)}$ , then one-point OSGD satisfies

\overline R_n\le 4n^{3/4}\sqrt{RdL\,(3+R/r)\,G}.

Milestones

Lemma 6.1: $\nabla\int_{\mathbb B}\ell(x+\delta b)\,db=\frac1\delta\int_{\mathbb S}\ell(x+\delta s)s\,d\sigma(s)$ .
Lemma 6.2: $\frac d\delta\mathbb E[\ell(x+\delta S)S]=\nabla\mathbb E\,\ell(x+\delta B)$ .
Eq. (6.2): $|\ell(x)-\widetilde\ell(x)|\le\delta G$ .
Lemma 6.3: the queried points' regret against $x$ is at most the smoothed regret of the iterates against $(1-\xi)x$ , plus $3\delta Gn+\xi GRn$ .
Theorem 6.1: two-point OSGD has $\overline R_n\le R^2/\eta+\eta(Gd)^2n+\delta(3+R/r)Gn$ , and $\overline R_n\le 2RGd\sqrt n+\delta(3+R/r)Gn$ for $\eta=R/(Gd\sqrt n)$ .
Theorem 6.2, first display: one-point OSGD has $\overline R_n\le R^2/\eta+\frac{(dL)^2}{\delta^2}\eta n+\delta(3+R/r)Gn$ for every $0<\delta\le r$ and $\eta>0$ .

Significance

The $n^{3/4}$ bound shows that a single function value per round suffices for sublinear regret against any oblivious sequence of Lipschitz convex losses, with a forecaster whose only operations are a random perturbation and a Euclidean projection. The smoothing identity of Lemmas 6.1–6.2 is the basic tool of zeroth-order (derivative-free) optimization, used well beyond bandits, and Theorem 6.1 is the $\sqrt n$ benchmark for two-point methods.

All results are proved in the source. To the best of current knowledge none is formalized: the related items of the Introduction to Online Convex Optimization series on Prove2Me (Hazan's Lemma 6.7 and Theorem 6.9) were formalized with missing hypotheses and are recorded as disproved. This mission produces machine-checked statements with every hypothesis explicit, and the formal infrastructure (sphere measure calculus, a projected stochastic gradient analysis) for later zeroth-order results.

Difficulty

Two steps resist a direct formal treatment. First, Lemma 6.1 is a divergence-theorem identity on the ball; Mathlib has the sphere measure and polar coordinates, but its divergence theorem covers boxes rather than balls, so differentiating the ball average in $x$ requires either such a theorem or a direct argument about translates of the ball. Second, the regret analysis takes expectations of quantities that depend on the whole past: the iterate $x_t$ is a function of $S_1,\dots,S_{t-1}$ , and unbiasedness $\mathbb E[\widetilde g_t\mid x_t]=\nabla\widetilde\ell_t(x_t)$ holds only conditionally, via independence of $S_t$ from the past. A pathwise gradient-descent inequality must be combined with this conditional expectation round by round, with measurability of the projected iterates established along the way. The naive approach of treating the estimate as the true gradient of $\ell_t$ fails: it is a gradient of $\widetilde\ell_t$ , and the gap is handled only by Eq. (6.2) and Lemma 6.3.

Formalization scope

Points are in EuclideanSpace ℝ (Fin d) with $d\ge1$ ; rounds are $t=1,2,\dots$ , sums run over Finset.Icc 1 n. $\sigma$ is Mathlib's Measure.toSphere of Lebesgue measure; the uniform laws are normalized restrictions. Randomness lives on an arbitrary probability space; the directions $S_t$ are measurable, mutually independent (iIndepFun) and uniform on $\mathbb S$ , and in Theorem 6.1 the pairs $(S_t,C_t)$ are independent with $C_t$ a fair sign independent of $S_t$ . A run of OSGD is a predicate (start at $0$ , each iterate a Euclidean projection onto $(1-\delta/r)\mathcal K$ ), which determines the run uniquely, so the forecaster uses only observed values and its own randomness. The losses are Lipschitz, differentiable and convex on all of $\mathbb R^d$ ; the bound $|\ell_t|\le L$ is on $\mathcal K$ , because a convex function bounded on $\mathbb R^d$ is constant. The minimum over $\mathcal K$ is an infimum over the subtype $\mathcal K$ , attained in every theorem.

Conventions and corrections, each stated in the item's Formalization Note:

Lemma 6.1 carries the factor $1/\delta$ that the printed statement omits and the proof contains (corrected misprint).
Theorem 6.1's second display prints $\eta=R/(GD\sqrt n)$ and a limit "for $\delta\to0$ "; the item states $\overline R_n\le 2RGd\sqrt n+\delta(3+R/r)Gn$ for $\eta=R/(Gd\sqrt n)$ and every admissible $\delta$ , which implies the limit (corrected misprint).
Theorems 6.1 and 6.2 add $0<\delta\le r$ , which the proofs need for $X_t^\pm,\widetilde X_t\in\mathcal K$ ; for the tuned $\delta$ of the goal it is a condition on $n$ .
The goal adds $G,L>0$ and $n\ge1$ , which its formulas for $\delta,\eta$ need; the constant $4$ is the book's rounding of $2\cdot2^{3/4}$ and is kept, as is the form $R^2/\eta$ .

The statements cannot be satisfied trivially: the run is pinned by its recursion, the losses are fixed before the randomness, the expectations are of bounded measurable functions (no zero-valued Bochner integrals), and the minimum is over the nonempty compact $\mathcal K$ . Section 6.3 (Lemma 6.4, Theorem 6.3) is not included, because its algorithm box and proof use different stage lengths and its unimodality condition is stated on a smaller set than the proof uses.

Needed infrastructure: calculus of ball averages and sphere integrals, symmetry of the uniform sphere law, nonexpansiveness of projections onto closed convex sets, and conditional-expectation bookkeeping for adapted iterates. Each is reusable for zeroth-order optimization; contributions of any of them as separate lemmas are welcome.

Selected references

S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2, doi:10.1561/2200000024
A. Flaxman, A. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005. arXiv:cs/0408007
A. Agarwal, O. Dekel, L. Xiao, Optimal algorithms for online convex optimization with multi-point bandit feedback, COLT 2010. link
S. Bubeck, R. Eldan, Y. T. Lee, Kernel-based methods for bandit convex optimization, STOC 2017. arXiv:1607.03084

10 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Dimensioning Large Call Centers I: The Rationalized Staffing Function Is Asymptotically OptimalResearch Paper

Motivation

A call center with $N$ agents facing Poisson arrivals at rate $\lambda$ and exponential service at rate $\mu$ is the M/M/N (Erlang-C) queue. Choosing $N$ trades the cost of agents against the cost of customers waiting, and in practice it is done with the square-root safety-staffing rule $N \approx R + y\sqrt R$ , where $R = \lambda/\mu$ is the offered load. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) turned that rule of thumb into an optimization result: for a general convex staffing cost and a general waiting-cost function, they identify the safety factor $y$ that makes the rule asymptotically optimal as the arrival rate grows.

Timeline of the asymptotic regime the paper builds on:

1917. Erlang's delay formula $\pi(N,\nu)$ for the M/M/N queue.
1981. Halfin and Whitt (Oper. Res. 29(3)) show that with $N = R + \beta\sqrt R$ servers the probability of waiting converges to a limit $P(\beta) \in (0,1)$ , the quality-and-efficiency-driven regime.
2000/2004. Borst, Mandelbaum and Reiman classify cost structures into a rationalized, an efficiency-driven and a quality-driven regime, and prove asymptotic optimality of an explicit staffing rule in each.

This mission is the first of a series of four on that paper and covers the rationalized regime (Section 5), where staffing and waiting costs are of the same order.

Setting

The service rate $\mu > 0$ is fixed and the arrival rate $\lambda$ grows. A staffing cost $F$ , defined on $(0,\infty)$ , is convex and strictly increasing; it does not depend on $\lambda$ . For each $\lambda > 0$ a waiting-cost function $D_\lambda$ satisfies $D_\lambda(0)=0$ , is strictly increasing on $[0,\infty)$ , and makes

G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)\,e^{-(N\mu-\lambda)t}\,dt

finite for every $N > \lambda/\mu$ . With the Erlang-C formula

\pi(N,\nu) = \frac{\nu^N}{N!}\Big\{\big(1-\tfrac{\nu}{N}\big)\sum_{n=0}^{N-1}\frac{\nu^n}{n!}+\frac{\nu^N}{N!}\Big\}^{-1},

the expected total cost of staffing $N > \lambda/\mu$ agents is $C(N,\lambda) = F(N) + \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda)$ , and $N^*_\lambda$ is any integer $N > \lambda/\mu$ minimizing it (7).

In normalized units $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$ the paper defines $F_\lambda(x) = F(N_\lambda(x)) - F(\lambda/\mu)$ , $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$ , the continuous delay probability $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$ with

H(M,\alpha) = \Big\{\alpha\int_0^\infty e^{-\alpha t}\,t\,(1+t)^{M-1}\,dt\Big\}^{-1},

and $C_\lambda(x) = F_\lambda(x) + \pi_\lambda(x)G_\lambda(x)$ , minimized at $x^*_\lambda$ (8). A surrogate $C[z;\hat F,\hat\pi,\hat G] = \hat F(z)+\hat\pi(z)\hat G(z)$ approximates it. Rounding is measured by

S_\lambda(x) = \min\{C(\lfloor N_\lambda(x)\rfloor,\lambda),\,C(\lceil N_\lambda(x)\rceil,\lambda)\}. \tag{10}

The Halfin–Whitt delay function is $P(x) = \big(1 + x/h(-x)\big)^{-1}$ , with $h = \phi/(1-\Phi)$ the standard normal hazard rate (11). Asymptotic equality $a_\lambda \stackrel{\infty}{\approx} b_\lambda$ means $a_\lambda/b_\lambda \to 1$ as $\lambda\to\infty$ .

Formalization targets

Goal: Theorem 5.1

Assume the rationalized condition (18): for some $\kappa > 0$ , $F_\lambda(\kappa)/G_\lambda(\kappa) \to \gamma \in (0,\infty)$ . Let $y^*_\lambda$ minimize $F_\lambda(y) + P(y)G_\lambda(y)$ over $y>0$ (19). Then

\lim_{\lambda\to\infty}\frac{S_\lambda(y^*_\lambda) - F(\lambda/\mu)}{C(N^*_\lambda,\lambda) - F(\lambda/\mu)} = 1.

The goal fixes no constant and no rate: it asserts only that the excess cost of the explicit rule is asymptotically the optimal excess cost.

Milestones

Lemma C.1: $G_\lambda$ is strictly convex and strictly decreasing on $(0,\infty)$ .
Section 3, p. 12: $H(N,\nu) = \pi(N,\nu)$ at integers $N > \nu > 0$ .
Lemma 3.1, Lemma 3.2, Corollary 3.3: the approximation principle. If the surrogate approximates $C_\lambda$ at both $x^*_\lambda$ and its own minimizer $z^*_\lambda$ , then rounding $N_\lambda(z^*_\lambda)$ is asymptotically optimal.
Eqs. (13)–(14): $F_\lambda$ preserves $\limsup$ -separation of ratios.
Lemma 4.1 (Halfin & Whitt): for bounded $x_\lambda$ , $\pi_\lambda(x_\lambda)/P(x_\lambda) \to 1$ .

Significance

The theorem justifies the square-root staffing rule from first principles for a broad cost class. In Example 5.3 of the paper (linear staffing cost $c$ per agent, linear waiting cost $a$ per unit time) it gives $N^* \approx R + y^*(a/c)\sqrt R$ , with $y^*(r)$ the minimizer of $y + rP(y)/y$ , a one-dimensional rule computable once for all loads. Corollary 3.3 is reused verbatim by the efficiency-driven and quality-driven theorems of the paper (missions II and III of this series), and Lemma 4.1 is the analytic input of all three.

The result has been proved since 2000; no machine-checked proof of it, or of the Halfin–Whitt limit for the continuous extension $\pi_\lambda$ , is known to exist. The mission produces a formal proof of the regime theorem together with reusable formal statements of the Erlang-C function, its integral representation, and the Halfin–Whitt limit.

Difficulty

The reduction from discrete to continuous staffing (Lemmas 3.1–3.2) is elementary once unimodality of $C_\lambda$ is available, but unimodality rests on convexity of $\pi_\lambda$ , which the paper cites rather than proves, and on Lemma C.1, which needs differentiation under an improper integral. The central difficulty is Lemma 4.1: the paper derives it from Halfin and Whitt's limit theorem, which is stated for integer server counts, while $\pi_\lambda$ is evaluated at non-integer $N_\lambda(x_\lambda)$ ; a proof needs a uniform Laplace-type asymptotic for the integral defining $H$ . A further obstacle is bounding $x^*_\lambda$ : the obvious route through continuity of the optimizer fails because nothing converges, and the paper instead argues by contradiction via (14).

Formalization scope

All objects live in DimCallCenters.Rationalized. The arrival rate is a real lam, and every limit is Filter.atTop on $\mathbb R$ with $\mu$ fixed. The queue itself is not modelled; the paper's theorems are statements about the closed-form cost $C(N,\lambda)$ , and so are these. Committed conventions:

The standing assumptions are a structure WaitModel ( $\mu>0$ ; $D_\lambda(0)=0$ ; $D_\lambda$ strictly increasing on $[0,\infty)$ ; $t\mapsto D_\lambda(t)e^{-\theta t}$ integrable on $(0,\infty)$ for every $\theta>0$ , which is the paper's finiteness of $G$ ). $F$ is convex and strictly increasing on $(0,\infty)$ .
Staffing levels in $C(N,\lambda)$ are natural numbers; $G$ and $H$ take real $N$ .
Argmins ( $N^*_\lambda$ , $x^*_\lambda$ , $z^*_\lambda$ , $y^*_\lambda$ ) are hypotheses that a given function is a minimizer, for every $\lambda>0$ ; ties are allowed and the theorems hold for every choice.
In $S_\lambda$ the floor term is omitted when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$ , where $C$ is undefined.
$\limsup$ and $\liminf$ relations are written with ∃ᶠ/∀ᶠ, not Filter.limsup on $\mathbb R$ .
Added hypothesis. The goal assumes $G(N,\lambda)\to\infty$ as $N\downarrow\lambda/\mu$ . The paper asserts this limit on p. 12, but it does not follow from its assumptions (it fails for bounded $D_\lambda$ ); it is equivalent to $D_\lambda$ being unbounded and is what makes the continuous optimum exist.

The hypotheses are met by linear staffing and waiting costs ( $F(N)=cN$ , $D_\lambda(t)=at$ ), for which (18) holds with $\gamma = c\kappa^2/a$ , so the goal is not vacuous. It is not trivialized by junk values either: the ratio's denominator is positive at every $\lambda>0$ , and $S_\lambda$ never evaluates $C$ at an unstable level.

Needed infrastructure: Laplace asymptotics for $\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt$ , differentiation under the integral sign for $G$ , and convexity of $\pi_\lambda$ . All of these are reusable for missions II–IV. Proofs of the milestones in any order are welcome, as are proofs of the convexity facts the paper cites from its references [9], [10].

Selected references

S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000; Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektroteknikeren 13, 1917.

21 thms2 active usersReviewed

Linear Optimization Operations Research·Captain: mikedeng1

A Multicut Algorithm for Two-Stage Stochastic Linear Programs 2: Multicut for Simple Recourse Stops Within J·m2 + 1 IterationsResearch Paper

Motivation

Two-stage stochastic linear programs model decisions taken before uncertainty is resolved (first stage) and corrected afterwards at a cost (second stage, the recourse). The standard solution method for problems with finitely many scenarios is the L-shaped method of Van Slyke and Wets (1969), an outer linearization in the style of Benders decomposition: a master program approximates the expected recourse function by cutting planes, one cut per iteration. Birge and Louveaux (1988) proposed the multicut variant, which approximates the recourse function of each realization separately and can add several cuts per iteration, and compared the two methods by worst-case counts of major iterations.

The paper's §5 treats the special case of simple recourse, where the second stage only penalizes shortage and surplus of each component of the first-stage output against a random target. Simple recourse arises in production planning, inventory and capacity models, and is the case in which the recourse function separates into one-dimensional pieces. There the paper derives an explicit LP (25) equivalent to the problem, a dedicated multicut algorithm for it, and the bound of $Jm_2+1$ iterations quoted below. This mission formalizes that section.

Setting

First-stage data are $c\in\mathbb R^{n_1}$ , $A\in\mathbb R^{m_1\times n_1}$ , $b\in\mathbb R^{m_1}$ , and the first-stage feasible set is $K_1=\{x\mid Ax=b,\ x\ge0\}$ . A deterministic technology matrix $T\in\mathbb R^{m_2\times n_1}$ , with rows $T_i$ , maps $x$ to the tender $\chi=Tx\in\mathbb R^{m_2}$ . Problem (3) of the paper is

\min\ z(x)=cx+\Psi(Tx)\quad\text{s.t. } x\in K_1 .

For each row $i=1,\dots,m_2$ the random vector $\xi_i=(q_i^+,q_i^-,h_i)$ takes $J$ values $\xi_{ij}=(q^+_{ij},q^-_{ij},h_{ij})$ with probabilities $p_{ij}$ . The simple recourse cost (20) of row $i$ is the optimal value of a one-row LP,

\psi_i(\chi_i,\xi_{ij})=\min\{q^+_{ij}y^+ + q^-_{ij}y^- \mid y^+-y^-=h_{ij}-\chi_i,\ y^+,y^-\ge0\},

and by separability (19) the expected recourse function is $\Psi(\chi)=\sum_i\Psi_i(\chi_i)$ with $\Psi_i(\chi_i)=\sum_j p_{ij}\psi_i(\chi_i,\xi_{ij})$ . Write $q_{ij}=q^+_{ij}+q^-_{ij}$ .

The multicut algorithm for simple recourse problems (p. 389) keeps a set $I$ of identified pairs $l=(i,j)$ , initially empty. Step 1 solves the master program (26),

\min\ cx+\sum_{i,j}p_{ij}q^-_{ij}(T_ix)+\sum_{l\in I}u_l\quad\text{s.t. } Ax=b,\ x\ge0,\ u_l\ge e_l-E_lx,\ u_l\ge0\ (l\in I),

with $E_l=p_{ij}q_{ij}T_i$ and $e_l=p_{ij}q_{ij}h_{ij}$ . Step 2 adds to $I$ every pair for which the constraint $0\ge p_{ij}q_{ij}(h_{ij}-T_ix^\nu)$ (27) is violated at the master's solution $x^\nu$ , and returns to Step 1; when no pair is added the algorithm stops.

Formalization targets

Goal: the $Jm_2+1$ bound, with correctness

The paper states (p. 389): "The initial problem (26) involves $m_1$ constraints and $n_1$ variables. For this problem, the worst-case situation is when at each iteration, only one constraint (27) is violated in Step 2. Then, the maximal number of iterations is $Jm_2+1$ ." The goal asserts, for every run of the algorithm (any optimal solution of (26) may be used at each Step 1):

\nu\text{-th solve of Step 1 takes place}\ \Longrightarrow\ \nu\le Jm_2+1,

and, when the algorithm stops at $x^\nu$ , $x^\nu\in K_1$ and $cx^\nu+\Psi(Tx^\nu)\le cx+\Psi(Tx)$ for all $x\in K_1$ .

Milestones

(22)–(23): for $q^++q^-\ge0$ the LP (20) attains its minimum $\max\{q^-(\chi-h),q^+(h-\chi)\}$ , so each $\theta_{ij}$ has only two cuts.
(24)–(25): the simple recourse problem is equivalent to the LP (25): same optimal $x$ , and the value of (25) at $x$ with the best slacks is $z(x)$ .
Relaxation and stopping: (26) is a relaxation of (25), and if no unidentified pair violates (27) at an optimum of (26), that optimum (extended by zero slacks) is optimal for (25).
Facets: each $\Psi_i$ is a maximum of $J+1$ affine functions, so $\Psi$ is a maximum of at most $(J+1)^{m_2}$ affine functions.

Significance

The bound is linear in $m_2$ and $J$ , while the L-shaped method may need as many iterations as $\Psi$ has facets, up to $(J+1)^{m_2}$ (milestone 4). This is the paper's clearest instance of the multicut method's worst-case advantage, and the equivalence (25) shows that simple recourse problems are LPs of size linear in $m_2J$ , a fact used throughout the later literature on simple and integrated recourse.

The results are proved in the paper, briefly. To our knowledge none has a machine-checked proof. Formalizing them produces a checked reduction of simple recourse to an explicit LP, a checked correctness proof of a constraint-generation algorithm with an explicit iteration bound, and the piece count of a sum of one-dimensional convex piecewise linear functions.

Difficulty

The counting argument is short once the algorithm is pinned down; the difficulty lies in the rest. Correctness at stopping requires relating three optimization problems (3), (25) and (26) whose objectives differ by a constant and by slack variables that are only present for identified pairs, and doing so for an arbitrary optimal solution of the master. The step from (20) to (22)–(23) requires solving an LP in closed form, as an infimum that must first be shown finite. The facet count requires showing that a sum of $J$ convex functions, each with one breakpoint, is a maximum of exactly $J+1$ affine functions, which is not a consequence of convexity alone.

Formalization scope

All vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, realizations are indexed by Fin J, and pairs $(i,j)$ by Fin m2 × Fin J. The second-stage value $\psi$ is the EReal infimum of the LP (20), not its closed form; expectations are finite sums weighted by $p_{ij}\ge0$ with $\sum_jp_{ij}=1$ .

Readings pinned down, each recorded in the item statements:

$q_{ij}\ge0$ . The paper never states it, but without it (20) is unbounded below and (25) is not equivalent to (3). It is a field of the model.
$x\ge0$ belongs to (3) and is omitted in the displays of (25) and (26); it is kept in both.
Step 2 ranges over unidentified pairs. The paper writes "for each $i$ and $j$ "; read literally, an identified pair whose $u_l$ already covers it could be re-added forever. The paper's remark that (27) "identifies any constraints in (25) that are not met" fixes the reading. The state of the algorithm is the set of identified pairs; the order of identification, and so the index $t$ , is immaterial.
Stopping rule. It is implicit in the paper: stop when (27) is violated for no pair.
Counting. The paper writes "the maximal number of iterations is $Jm_2+1$ "; we count solves of Step 1, the stopping solve included, which is what its argument counts.
Constant. The objective of (26) omits the constant $-\sum p_{ij}q^-_{ij}h_{ij}$ of (25), as printed.
Facets. " $\Psi_i$ contains $J+1$ facets" is read as "is a maximum of $J+1$ (not necessarily distinct) affine functions".

A formalization in which the master step could fire without a violated, unidentified pair, or in which the algorithm's optimal solutions were fixed in advance, would make the bound either false or empty; the definitions exclude both. The goal includes optimality at stopping so that it is not only a statement about a set growing inside a finite set.

Needed infrastructure: elementary LP feasibility and optimality, finite sums in EReal, and piecewise linear convex functions on $\mathbb R$ . Contributions of any of the milestones, in any order, are welcome; milestone 1 is the natural first step.

Selected references

J.R. Birge and F.V. Louveaux, A multicut algorithm for two-stage stochastic linear programs, European Journal of Operational Research 34 (1988) 384–392. https://doi.org/10.1016/0377-2217(88)90159-2
R.M. Van Slyke and R. Wets, L-shaped linear programs with applications to optimal control and stochastic programming, SIAM Journal on Applied Mathematics 17 (1969) 638–663. https://doi.org/10.1137/0117061
J.R. Birge and F.V. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

7 thms2 active usersReviewed

Analysis Operations Research·Captain: mikedeng1

The Łojasiewicz Inequality for Nonsmooth Subanalytic Functions with Applications to Subgradient Dynamical Systems I: The Łojasiewicz Inequality at Critical Points of Continuous Subanalytic FunctionsResearch Paper

Motivation

For a real-analytic function $f : U \to \mathbb{R}$ on an open set $U \subseteq \mathbb{R}^n$ and a critical point $a$ (so $\nabla f(a) = 0$ ), the Łojasiewicz gradient inequality says that there is an exponent $\theta \in [0,1)$ such that $|f - f(a)|^{\theta} / \|\nabla f\|$ stays bounded near $a$ . It is the standard tool for proving that bounded gradient trajectories $\dot x = -\nabla f(x)$ have finite length and converge to a single critical point, and, in its descendants (the Kurdyka–Łojasiewicz property), for proving convergence of the whole iterate sequence of nonconvex descent methods: proximal gradient, alternating minimization, PALM, ADMM. Those algorithmic results all assume a nonsmooth version of the inequality, for functions that may take the value $+\infty$ and are not differentiable.

Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007)) supplied that nonsmooth version. This mission formalizes their first main result, Theorem 3.1: the inequality at critical points of subanalytic functions that are continuous on a closed domain.

Timeline.

1963: Łojasiewicz proves the inequality for real-analytic functions (Une propriété topologique des sous-ensembles analytiques réels), and in 1984 derives convergence of bounded analytic gradient trajectories.
1998: Kurdyka (Ann. Inst. Fourier 48) extends it to $C^1$ functions definable in an o-minimal structure, with a desingularizing function in place of the power.
2006: Bolte, Daniilidis and Lewis prove a nonsmooth Sard theorem (J. Math. Anal. Appl. 321): a subanalytic function continuous on its closed domain is constant on each connected component of its critical set.
2007: The present paper proves the nonsmooth inequality for continuous subanalytic functions (Theorem 3.1) and for lower semicontinuous convex ones (Theorem 3.3).
2007: Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18) extend it to lower semicontinuous functions definable in o-minimal structures (the KL property).

Setting

Write $\mathbb{R}^n$ with its Euclidean norm. A function $f : \mathbb{R}^n \to \mathbb{R} \cup \{+\infty\}$ has domain $\operatorname{dom} f = \{x : f(x) < +\infty\}$ .

Subanalytic sets (Definition 2.1). A set $A \subseteq \mathbb{R}^n$ is semianalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ on which $A \cap V = \bigcup_{i=1}^{p}\bigcap_{j=1}^{q}\{x \in V : f_{ij}(x) = 0,\ g_{ij}(x) > 0\}$ with $f_{ij}, g_{ij}$ real-analytic on $V$ . It is subanalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ such that $A \cap V$ is the projection onto $\mathbb{R}^n$ of a bounded semianalytic subset of $\mathbb{R}^n \times \mathbb{R}^m$ , $m \ge 1$ . A function $f$ is subanalytic if its graph $\{(x,\lambda) \in \mathbb{R}^n \times \mathbb{R} : f(x) = \lambda\}$ is subanalytic. Semialgebraic functions, and functions locally built from analytic ones by finitely many algebraic operations, max/min and compositions, are subanalytic.

Subdifferentials (Definition 2.10). The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y \to x,\, y \ne x} \frac{f(y) - f(x) - \langle x^*, y - x\rangle}{\|y - x\|} \ge 0$ (empty off $\operatorname{dom} f$ ). The limiting subdifferential $\partial f(x)$ is the set of limits of $x^*_k \in \hat\partial f(x_k)$ along $x_k \to x$ with $f(x_k) \to f(x)$ .

Slope and critical points. The nonsmooth slope is $m_f(x) = \inf\{\|x^*\| : x^* \in \partial f(x)\}$ , equal to $+\infty$ when $\partial f(x) = \emptyset$ (equation (4)). The critical set is $\operatorname{crit} f = \{x : 0 \in \partial f(x)\}$ (Definition 2.11).

Formalization targets

Goal: Theorem 3.1

Let $f$ be subanalytic with closed domain and $f|_{\operatorname{dom} f}$ continuous, and let $a \in \operatorname{crit} f$ . Then there is $\theta \in [0,1)$ such that

\frac{|f - f(a)|^{\theta}}{m_f} \ \text{ is bounded around } a,

with the conventions $0^0 = 1$ and $\infty/\infty = 0/0 = 0$ . In division-free form: there are $C$ and a neighbourhood $U$ of $a$ with $|f(x) - f(a)|^{\theta} \le C\|x^*\|$ for all $x \in U$ and $x^* \in \partial f(x)$ . The exponent is existential; the goal fixes no value of $\theta$ or $C$ .

Milestones

Remark 2.12, for $f$ continuous on a closed domain: the graph of $\partial f$ is closed; $\operatorname{crit} f$ is closed; $m_f$ is lower semicontinuous; $\operatorname{crit} f = m_f^{-1}(0)$ .
Proposition 2.13(ii), its clause on the critical set: if $f$ is subanalytic and relatively bounded on its domain, then $\operatorname{crit} f$ is subanalytic.
Equation (6), recalled from the nonsmooth Sard theorem: $f$ is constant on the connected component of $\operatorname{crit} f$ containing $a$ .
The curve selection lemma, recalled from Bierstone–Milman: a boundary point of a subanalytic set is the origin of an analytic arc entering the set.

Significance

The result. Theorem 3.1 is the nonsmooth Łojasiewicz inequality at critical points. With the subgradient in place of the gradient, it yields finite length of bounded trajectories of subgradient systems $\dot x \in -\partial f(x)$ (Section 4 of the paper) and is the template for the Kurdyka–Łojasiewicz property that underlies convergence proofs for proximal and splitting methods on nonconvex, nonsmooth problems (e.g. Attouch–Bolte–Redont–Soubeyran 2010, Bolte–Sabach–Teboulle 2014). Those papers assume the KL property and cite this line of results to know it holds for semialgebraic and subanalytic objectives.

Formalizing it. The theorem is proved; this mission produces a machine-checked proof. To our knowledge no proof assistant has a formal definition of subanalytic sets or of the nonsmooth Łojasiewicz inequality. The definitions layer (semianalytic and subanalytic sets, the slope, the inequality) is reusable by any later formalization of KL-based convergence analyses, and the milestones on Remark 2.12 are general facts about limiting subdifferentials that apply well beyond subanalytic geometry.

Difficulty

The obvious argument restricts $f$ and $m_f$ to an analytic curve and compares their Puiseux expansions. That step needs three pieces of subanalytic geometry that no library has: curve selection, the structure of one-variable subanalytic functions (monotonicity and Puiseux expansions), and the fact that the sets built in the proof (sets of points with a subgradient satisfying an inequality, level-wise infima of $m_f$ ) are again subanalytic, which in the paper goes through global subanalyticity and the projection theorem. The second obstacle is that $f$ is not smooth: the classical proof differentiates $f$ along a curve, while here only Fréchet subgradients are available, and the chain rule along an analytic curve holds only almost everywhere. The constancy of $f$ on critical components, equation (6), is itself a nonsmooth Sard-type theorem whose published proof uses stratification. A solver who replaces subanalytic by semialgebraic, or assumes $f$ real-valued and $C^1$ , proves a different and much weaker statement.

Formalization scope

Space and values. The space is EuclideanSpace ℝ (Fin n). The function is f : E → EReal with f x ≠ ⊥ for every x. The domain is {x | f x ≠ ⊤}; it is assumed closed, and f is assumed ContinuousOn it.
Subdifferentials. $\hat\partial f$ and $\partial f$ are the published platform definitions NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff, which match Definition 2.10 for functions never equal to $-\infty$ .
Subanalyticity. It is defined on any finite-dimensional real normed space, so that the same definition covers $\mathbb{R}^n$ , $\mathbb{R}^n \times \mathbb{R}$ and $\mathbb{R}^n \times \mathbb{R}^m$ . Analyticity is AnalyticOnNhd ℝ. The boundedness of the semianalytic set in Definition 2.1(ii) is part of the definition: without it every projection of a semianalytic set would count.
Slope. The slope is valued in $[0,+\infty]$ , with $+\infty$ on points without subgradients.
The inequality. It is the predicate LojIneqAt f a θ: one constant $C$ and one neighbourhood of $a$ , quantified over all limiting subgradients. Under $0^0 = 1$ the value $\theta = 0$ never works at a critical point, as under the paper's conventions.
Not assumed. The goal does not assume lower semicontinuity, real values, global subanalyticity, compactness of the critical set, or $f(a) = 0$ . These are reductions inside the paper's proof. Any formalization that adds them, fixes $\theta$ , or replaces the class of $f$ by semialgebraic or $C^1$ functions trivializes the target.
Infrastructure. A complete proof needs: curve selection; the monotonicity lemma and Puiseux expansions for one-variable globally subanalytic functions; the projection theorem or an equivalent definability argument; the nonsmooth Sard theorem (6); and a chain rule for Fréchet subgradients along analytic curves. Each of these is welcome as a separate contribution, and the subanalytic-geometry results are reusable well beyond this mission.

Selected references

J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17 (2007) 1205–1223. https://doi.org/10.1137/050644641
J. Bolte, A. Daniilidis, A. Lewis, A Sard theorem for non-differentiable functions, J. Math. Anal. Appl. 321 (2006) 729–740.
E. Bierstone, P. Milman, Semianalytic and subanalytic sets, Publ. Math. IHÉS 67 (1988) 5–42. https://doi.org/10.1007/BF02699126
K. Kurdyka, On gradients of functions definable in o-minimal structures, Ann. Inst. Fourier 48 (1998) 769–783. https://doi.org/10.5802/aif.1638
J. Bolte, A. Daniilidis, A. Lewis, M. Shiota, Clarke subgradients of stratifiable functions, SIAM J. Optim. 18 (2007) 556–572. https://doi.org/10.1137/060670080
S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, in Les Équations aux Dérivées Partielles, CNRS, Paris, 1963, 87–89.
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Grundlehren 317, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

12 thms2 active usersReviewed

Convex Optimization Probability·Captain: mikedeng1

The Entropic Barrier: A Simple and Optimal Universal Self-Concordant Barrier: The Entropic Barrier of a Convex Body in ℝⁿ Is a (1 + εₙ)n-Self-Concordant Barrier with εₙ ≤ 100√(log n / n)Research Paper

Motivation

Interior-point methods minimize a linear function $x\mapsto\langle c,x\rangle$ over a convex set $\mathcal K\subset\mathbb R^n$ by following the minimizers of $\langle c,x\rangle+\frac1t g(x)$ as $t\to\infty$ , where $g$ is a self-concordant barrier for $\mathcal K$ . Each Newton step of such a method shrinks $1/t$ by a factor $1-1/\sqrt\nu$ , where $\nu$ is the self-concordance parameter of $g$ , so $\nu$ controls the iteration count of every interior-point method built on $g$ (Nesterov and Nemirovski 1994; Nesterov 2004).

Timeline:

1994. Nesterov and Nemirovski construct the universal barrier for any convex body and show it is a $\nu$ -self-concordant barrier with $\nu\le Cn$ for a universal constant $C$ . They also show that $\nu\ge n$ is necessary for some bodies (the simplex, the cube).
2014–2015. Hildebrand (Math. Oper. Res. 2014) and Fox (Ann. Mat. Pura Appl. 2015) show that the canonical barrier of a convex cone has parameter equal to the dimension, which gives parameter $n+1$ for convex bodies.
2015. Bubeck and Eldan (arXiv:1412.1587, COLT 2015) show that the Fenchel dual of the log-Laplace transform of the uniform measure on $\mathcal K$ , which they call the entropic barrier, is a $(1+o(1))n$ -self-concordant barrier, with an explicit $o(1)$ term.

Beyond optimization, the entropic barrier is the mirror map that pairs naturally with the exponential-family sampling scheme in bandit linear optimization, which the paper discusses in its §3.1.

Setting

Let $\mathcal K\subset\mathbb R^n$ be a convex body: compact, convex, with non-empty interior $\operatorname{int}(\mathcal K)$ . The log-Laplace transform of $\mathcal K$ is

f(\theta)=\log\left(\int_{x\in\mathcal K}\exp(\langle\theta,x\rangle)\,dx\right),\qquad\theta\in\mathbb R^n,

and the entropic barrier is its Fenchel dual

f^*(x)=\sup_{\theta\in\mathbb R^n}\ \langle\theta,x\rangle-f(\theta),\qquad x\in\operatorname{int}(\mathcal K).

For a function $g:\operatorname{int}(\mathcal K)\to\mathbb R$ write $\nabla g(x)[h]$ , $\nabla^2g(x)[h,h]$ , $\nabla^3g(x)[h,h,h]$ for its directional derivatives. Following Definition 1 of the paper:

$g$ is a barrier for $\mathcal K$ if $g(x)\to+\infty$ as $x\to\partial\mathcal K$ ;
a $C^3$ convex $g$ is self-concordant if $\nabla^3g(x)[h,h,h]\le2(\nabla^2g(x)[h,h])^{3/2}$ for all $x\in\operatorname{int}(\mathcal K)$ , $h\in\mathbb R^n$ ;
it is $\nu$ -self-concordant if moreover $\nabla g(x)[h]\le\sqrt{\nu\cdot\nabla^2g(x)[h,h]}$ for all such $x,h$ .

The proof works with the canonical exponential family $p_\theta$ , the probability measure with density $\exp(\langle\theta,x\rangle-f(\theta))\mathbb 1\{x\in\mathcal K\}$ , its mean $x(\theta)$ , covariance $\Sigma(\theta)$ and third central moment $T(\theta)$ ; with $Y=\langle\theta/\|\theta\|,X\rangle$ for $X\sim p_\theta$ and its density $\rho$ ; and with the section marginal $\lambda(y)=\mathrm{Vol}_{n-1}(\mathcal K\cap\{y\theta/\|\theta\|+\theta^\perp\})/\mathrm{Vol}(\mathcal K)$ .

Formalization targets

Goal: Theorem 1

For every $n\ge80$ and every convex body $\mathcal K\subset\mathbb R^n$ , $f^*$ is a $\nu$ -self-concordant barrier for $\mathcal K$ with

\nu=(1+\varepsilon_n)\,n,\qquad\varepsilon_n=100\sqrt{\frac{\log n}{n}}.

Milestones, in attack order

Lemma 1 (p. 5): strict convexity of $f$ , $f^*$ ; $\nabla f^*:\operatorname{int}(\mathcal K)\to\mathbb R^n$ is a bijection; $\nabla^2f=\Sigma$ , $\nabla^3f=T$ (eqs. (4)–(5)); $\nabla^2f^*(x)=\Sigma(\theta(x))^{-1}$ (eq. (6)).
$f^*$ is a barrier (§4, p. 6).
Lemma 2 (p. 7): $\mathbb EX^3\le2(\mathbb EX^2)^{3/2}$ for a real centered log-concave $X$ ; its consequence $\mathbb E_{p_\theta}\langle X-x(\theta),h\rangle^3\le2(\mathbb E_{p_\theta}\langle X-x(\theta),h\rangle^2)^{3/2}$ ; $f^*$ is self-concordant (§4, pp. 6–7).
Reduction of (3) (p. 7): $f^*$ satisfies (3) with parameter $\nu$ iff $\langle\Sigma(\theta)\theta,\theta\rangle\le\nu$ for all $\theta$ .
$\lambda$ is $n$ -concave on its support (p. 9) and Lemma 5 (p. 9): $\varphi$ is $n$ -concave iff $(\log\varphi)''\le-\frac1n((\log\varphi)')^2$ .
Lemma 3 (p. 8): $\rho(y+y_0)=\rho(y_0)\zeta(y)e^{-y^2/(2\sigma^2)}$ on $[-M,M]$ , with $\zeta\in[0,1]$ unimodal, $M=\sqrt{7n\log n}/\|\theta\|$ , $\sigma^2=\frac{n}{\|\theta\|^2}\frac{1}{1-\sqrt{7\log(n)/n}}$ ; and its consequence (9): $\mathbb E(|Y-y_0|^2\mid|Y-y_0|\le M)\le\sigma^2$ .
Lemma 4 (p. 8): $(1-2c(\varepsilon)\varepsilon\log^2(1/\varepsilon))\mathrm{Var}(X)\le\int_{x_1}^{x_2}(x-x_0)^2\lambda(x)dx\le\mathbb E(|X-x_0|^2\mid X\in[x_1,x_2])$ for log-concave $X$ .
(7) (p. 7): $\mathrm{Var}(Y)\le\frac{n}{\|\theta\|^2}(1+\varepsilon_n)$ .

Significance

The result. Theorem 1 gives, for every convex body, an explicit barrier whose parameter is $n$ up to a second-order term, against the $Cn$ of the universal barrier, and it is optimal up to that term because $\nu\ge n$ is necessary for some bodies. The barrier is defined by a single formula, its derivatives are moments of an explicit probability measure, and its parameter bound reduces to a variance bound for one-dimensional log-concave marginals. Lemmas 2 and 4 are self-contained facts about log-concave laws on $\mathbb R$ (a sharp third-moment bound and a variance-localization bound) that are usable outside this paper.

Formalizing it. The theorem is proved in the paper; nothing here is formalized elsewhere. The platform has a definition of self-concordance (reused here) and results for given self-concordant functions, but no universal or entropic barrier, no exponential family over a convex body, and no moment bounds for log-concave laws. A complete development produces machine-checked versions of the duality facts of Lemma 1, of the two log-concave lemmas, and of the Brunn–Minkowski consequence for section volumes. Two steps of the paper are sketched rather than proved in full: the end of the proof of Lemma 2 ("We omit further details of this proof", p. 12) and, in Lemma 4, a normalization step that cites a lemma stated for isotropic densities. A formal proof either fills or replaces them.

Difficulty

Self-concordance of $f^*$ reduces to self-concordance of $f$ by a general duality fact, and that reduces to Lemma 2; the difficulty there is the sharp constant $2$ , since generic moment comparisons for log-concave laws give a worse constant. The parameter bound is the hard part. The obvious bound $\langle\Sigma(\theta)\theta,\theta\rangle\le Cn$ follows from standard concentration for log-concave measures, but any argument that loses a constant factor proves only the 1994 result. The $1+o(1)$ requires the one-dimensional marginal of the tilted measure to be compared with a Gaussian of variance $n/\|\theta\|^2$ to within a factor $1+O(\sqrt{\log n/n})$ , using the fact that $\lambda$ is $n$ -concave and not merely log-concave. The paper does this pointwise near the mode (Lemma 3) and controls the tails separately (Lemma 4). The pointwise argument assumes $\rho$ smooth, which holds for smooth bodies, and an approximation argument passes to general convex bodies.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so $n$ is the dimension, not a separate parameter. A convex body is compact, convex, with non-empty interior; a lower-dimensional set is excluded, which rules out a formalization in which the barrier and self-concordance clauses hold vacuously.
$f^*$ is a real supremum. On $\operatorname{int}(\mathcal K)$ it is the true supremum; elsewhere Lean returns a junk value that no statement reads. The barrier property is a limit within $\operatorname{int}(\mathcal K)$ at every frontier point.
Self-concordance (2) is the published ConvexOptimization.IsSelfConcordantOn on interior K, stated by line restrictions with an absolute value. It is equivalent to (2), because $h\mapsto-h$ flips the sign of the third derivative.
The goal states the parameter as the explicit number $\nu=(1+100\sqrt{\log(n)/n})\,n$ . The page says $\varepsilon_n\le100\sqrt{\log(n)/n}$ , and (3) is monotone in $\nu$ , so this is the same claim. An existential $\nu$ is not used.
Corrections and implicit hypotheses:
- Lemma 4 is stated for $0<\varepsilon<1$ . The page says $\varepsilon>0$ , but the statement is false for $\varepsilon\ge1$ and the paper applies it only with $\varepsilon<1$ .
- Lemma 5 assumes $\varphi>0$ , which is implicit in $\zeta=\log\varphi$ .
- The reduction of (3) assumes $\nu\ge0$ .
- Lemma 3 and (9) carry the smoothness of $\rho$ (the paper's own without-loss-of-generality step on p. 7) as a hypothesis, and the theorem's range $n\ge80$ .
Section volumes use Mathlib's unnormalized $(n-1)$ -dimensional Hausdorff measure. The normalization constant cancels in $\rho$ and does not affect $n$ -concavity. $\lambda$ and $\rho$ are fixed pointwise functions, because Lemma 3 evaluates $\rho$ at a maximizer.
Log-concavity on $\mathbb R$ is the published ConvexOptimization.LogConcaveOn on the whole line.
Needed infrastructure that is reusable beyond this mission:
- differentiation under the integral sign for exponential families on compact sets;
- Fenchel duality for smooth strictly convex functions;
- Brunn's concavity theorem for sections of convex bodies;
- moment and tail bounds for log-concave densities on $\mathbb R$ .
Contributions to any of these, or proofs of single milestones, are welcome.

Selected references

S. Bubeck, R. Eldan, The entropic barrier: a simple and optimal universal self-concordant barrier, COLT 2015; arXiv:1412.1587v3. https://arxiv.org/abs/1412.1587
Y. Nesterov, A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
R. Hildebrand, Canonical barriers on convex cones, Mathematics of Operations Research 39:841–850, 2014.
D. Fox, A Schwarz lemma for Kähler affine metrics and the canonical potential of a proper convex cone, Annali di Matematica Pura ed Applicata 194:1–42, 2015.
B. Klartag, On convex perturbations with a bounded isotropic constant, Geometric and Functional Analysis 16(6):1274–1290, 2006.
C. Borell, Convex set functions in d-space, Periodica Mathematica Hungarica 6(2):111–136, 1975.

21 thms2 active usersReviewed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization 3: Fractional Double Greedy on the Multilinear Extension Achieves 1/2 of the OptimumResearch Paper

Motivation

Unconstrained submodular maximization (USM) asks for a subset $S$ of a finite ground set $\mathcal N$ maximizing a nonnegative submodular function $f$ . It contains Max-Cut, Max-DiCut and maximum facility location as special cases, and it is the basic subproblem of many constrained submodular maximization algorithms. Because $f$ is given only through a value oracle, the question is how close to the optimum a polynomial number of queries can get.

Timeline of the approximation ratio for USM in the value oracle model:

Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) showed that a uniformly random set achieves $1/4$ , local search achieves $1/3$ and $2/5$ , and that no algorithm making polynomially many queries achieves $1/2 + \varepsilon$ for any fixed $\varepsilon > 0$ .
Oveis Gharan and Vondrák (SODA 2011) reached $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) reached $0.42$ .
Buchbinder, Feldman, Naor and Schwartz (FOCS 2012) closed the gap with the double greedy algorithms: a deterministic $1/3$ -approximation and a randomized $1/2$ -approximation, both linear in the number of oracle calls. Their Appendix A gives a third, fractional variant, which is the subject of this mission.

This is the third mission on the FOCS 2012 paper; the first two treat the deterministic and the randomized double greedy on sets.

Setting

Let $\mathcal N$ be a finite ground set with $n$ elements and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$ . The function $f$ is submodular if

f(A) + f(B) \ge f(A \cup B) + f(A \cap B) \qquad \text{for all } A, B \subseteq \mathcal N .

Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$ and let $OPT$ be a maximizing set.

The multilinear extension of $f$ is the function on vectors $x \in [0,1]^{\mathcal N}$

F(x) = \sum_{S \subseteq \mathcal N} f(S) \prod_{u \in S} x_u \prod_{u \notin S} (1 - x_u) = \mathbb E\bigl[f(R(x))\bigr],

where the random set $R(x)$ contains each element $u$ independently with probability $x_u$ . A set is identified with its characteristic vector, so $F$ agrees with $f$ on $\{0,1\}^{\mathcal N}$ , and $\{u\}$ also denotes the unit vector at $u$ . For vectors, $x \vee y$ and $x \wedge y$ are the coordinate-wise maximum and minimum.

Algorithm 4 (MultilinearUSM). Fix an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and start from $x_0 = \emptyset$ and $y_0 = \mathcal N$ (the vectors $\mathbf 0$ and $\mathbf 1$ ). In iteration $i = 1, \dots, n$ compute

a_i = F(x_{i-1} + \{u_i\}) - F(x_{i-1}), \qquad b_i = F(y_{i-1} - \{u_i\}) - F(y_{i-1}),

set $a_i' = \max\{a_i, 0\}$ , $b_i' = \max\{b_i, 0\}$ , and update

x_i = x_{i-1} + \frac{a_i'}{a_i' + b_i'} \{u_i\}, \qquad y_i = y_{i-1} - \frac{b_i'}{a_i' + b_i'} \{u_i\},

with the convention that the two fractions are $1$ and $0$ when $a_i' = b_i' = 0$ . The output is the random set $R(x_n)$ . Every choice before the output is deterministic; the algorithm queries $F$ at four points per element.

For the analysis, $OPT_i = (OPT \vee x_i) \wedge y_i$ .

Formalization targets

Goal: Theorem A.1, oracle-access clause

For every nonnegative submodular $f$ and every order of the ground set,

x_n = y_n \qquad\text{and}\qquad f(OPT) \le 2\,F(x_n) = 2\,\mathbb E\bigl[f(R(x_n))\bigr].

Milestones, in the order the proof uses them

$a_i + b_i \ge 0$ at every iteration (proof of Lemma A.2; the page cites Lemma II.1).
Endpoints: $OPT_0 = OPT$ with $F(OPT) = f(OPT)$ , and $OPT_n = x_n = y_n$ .
(4) and (5): if $a_i \ge 0$ and $b_i > 0$ , then $F(x_i) - F(x_{i-1}) = a_i^2/(a_i+b_i)$ and $F(y_i) - F(y_{i-1}) = b_i^2/(a_i+b_i)$ .
(6): in the same case, $F(OPT_{i-1}) - F(OPT_i) \le a_i b_i/(a_i + b_i)$ , whether or not $u_i \in OPT$ .
Lemma A.2: for every $1 \le i \le n$ ,

F(OPT_{i-1}) - F(OPT_i) \le \tfrac12\bigl[F(x_i) - F(x_{i-1}) + F(y_i) - F(y_{i-1})\bigr].

Telescoped display: $F(OPT_0) - F(OPT_n) \le \tfrac12[F(x_n) - F(x_0)] + \tfrac12[F(y_n) - F(y_0)] \le \tfrac12(F(x_n) + F(y_n))$ .

Significance

The result. Theorem A.1 shows that the double greedy analysis survives a change of domain: the factor $1/2$ is obtained by a procedure that never flips a coin until the end, and whose state is a pair of fractional points. The ratio matches the Feige–Mirrokni–Vondrák hardness bound, so it cannot be improved in the value oracle model. Its output is a fractional point together with an independent rounding, which separates the optimization from the rounding step.

Formalizing it. The result is proved on paper; no machine-checked proof of a double greedy guarantee is known. A complete development yields reusable facts about the multilinear extension of a submodular function on a finite type: $F$ is affine in each coordinate, its coordinate increments are antitone in the other coordinates on $[0,1]^{\mathcal N}$ , and $F$ restricted to characteristic vectors is $f$ . These are the standard tools of every continuous-relaxation argument for submodular maximization.

Difficulty

The proof on the page is short, but it relies on two facts it does not prove. First, the page justifies $a_i + b_i \ge 0$ "by Lemma II.1", which is a statement about sets; for vectors it requires that the increment of $F$ along a coordinate decreases as the other coordinates increase, a property of the multilinear extension of a submodular function that must be derived from the sum defining $F$ . Second, inequality (6) is written out only for $u_i \notin OPT$ , and Case 2 of Lemma A.2 is omitted as analogous; the formal statements cover all cases. The main technical work is the bookkeeping of the run: that each coordinate is touched once, that $x_{i-1}(u_i) = 0$ and $y_{i-1}(u_i) = 1$ when it is touched, that $x_i \le OPT_i \le y_i$ , and that every state stays in $[0,1]^{\mathcal N}$ , where the antitonicity applies.

Formalization scope

The ground set is a Fintype $X$ with decidable equality; sets are Finset X; $f$ is real-valued, with nonnegativity a hypothesis ∀ S, 0 ≤ f S wherever the page uses it (the goal and the telescoped display). Submodularity is the published NonmonotoneSubmod.Shared.Submodular, the lattice form $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$ ; $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT; $F$ is the published NonmonotoneSubmod.Shared.F, the sum above, defined for every $x : X \to \mathbb R$ .
The order $u_1, \dots, u_n$ is a duplicate-free list containing every element; $u_i$ is the entry at index $i-1$ , and $n$ is the list's length. The state after $i$ iterations is obtained by folding one step over the first $i$ entries from $(\mathbf 0, \mathbf 1)$ . Statements hold for every such order.
The footnote's convention $a_i'/(a_i'+b_i') = 1$ , $b_i'/(a_i'+b_i') = 0$ when $a_i' = b_i' = 0$ is an explicit case split; with Lean's $0/0 = 0$ it would otherwise be reversed and the run would no longer end with $x_n = y_n$ .
Corrected slips of the page: lines 3–4 of Algorithm 4 assign $a_i', b_i'$ but define $a_i, b_i$ ; " $f : \mathcal N \to \mathbb R^+$ " means $f : 2^{\mathcal N} \to \mathbb R^+$ ; " $F(x) \triangleq \mathbb E[R(x)]$ " means $\mathbb E[f(R(x))]$ ; "NSM" in Theorem A.1 means USM. The main text's one-line definition of submodularity, read literally, forces monotonicity; the footnote's lattice form is used.
Not formalized: the sampling clause of Theorem A.1 (ratio $(1/2) - o(1)$ without oracle access to $F$ , whose proof the paper refers to Calinescu, Chekuri, Pál and Vondrák) and the running time. The guarantee is stated for the algorithm as printed, so the trivial existence of a $1/2$ -approximation by exhaustive search does not satisfy it. A statement in which $x_n$ is an arbitrary point, or the state any process with $x_i \le y_i$ , would not be this theorem.
Contributions welcome: the multilinear-extension facts above as general lemmas, the run invariants, and proofs of the milestones in any order.

Selected references

N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012, 649–658. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205; its numbering differs and is not used here).
U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011, 1133–1153. https://doi.org/10.1137/090779346
S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011, 1098–1117. https://doi.org/10.1137/1.9781611973082.83
M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011, 342–353. https://doi.org/10.1007/978-3-642-22006-7_29
G. Calinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a Monotone Submodular Function Subject to a Matroid Constraint, SIAM J. Comput. 40(6), 2011, 1740–1766. https://doi.org/10.1137/080733991

11 thms2 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

Gradient Convergence in Gradient Methods with Errors II: With Zero-Mean Stochastic Errors, Almost Surely Either f(x_t) → −∞ or f(x_t) Converges and ∇f(x_t) → 0Research Paper

Motivation

Stochastic gradient methods minimize a function $f$ when only noisy estimates of its gradient are available: each step moves along a descent direction corrupted by random noise. They are the standard training algorithm for neural networks and the basic tool of stochastic approximation, and the question every user faces is what can be guaranteed when $f$ is nonconvex, possibly unbounded below, and the noise is allowed to grow with the gradient.

D. P. Bertsekas and J. N. Tsitsiklis, Gradient Convergence in Gradient Methods with Errors, SIAM J. Optim. 10(3):627–642, 2000 (DOI), answer this under minimal assumptions. Noise with variance growing in $\|\nabla f(x_t)\|$ had been handled for related methods (Poljak and Tsypkin 1973), but typically together with a lower bound on $f$ , under which $f(x_t)$ is approximately a supermartingale and the supermartingale convergence theorem applies (see the monographs of Kushner and Clark 1978; Benveniste, Métivier and Priouret 1990; Kushner and Yin 1996). Section 4 of the paper (p. 635) removes the lower bound: it proves that, with probability 1, either $f(x_t)\to-\infty$ or $f(x_t)$ converges and $\nabla f(x_t)\to 0$ , without assuming bounded iterates. Section 5 shows that the randomized incremental gradient method for a finite-sum objective is a special case. This mission formalizes Section 4 and the Section 5 application. A companion mission covers the deterministic counterpart (Proposition 1 of the same paper).

Setting

Let $f:\mathbb R^n\to\mathbb R$ be continuously differentiable with a Lipschitz gradient: there is $L\ge 0$ with

\|\nabla f(x)-\nabla f(\bar x)\|\le L\|x-\bar x\|\qquad\forall x,\bar x. \tag{2.1}

Let $(\Omega,\mathcal F,P)$ be a probability space and $\mathcal F_0\subseteq\mathcal F_1\subseteq\cdots$ an increasing sequence of $\sigma$ -fields (a filtration; $\mathcal F_t$ is the history of the algorithm just before the noise $w_t$ is drawn). The stochastic gradient method generates random vectors by

x_{t+1}=x_t+\gamma_t(s_t+w_t),

where $\gamma_t>0$ is a deterministic stepsize, $s_t$ is a descent direction and $w_t$ is a noise term. The assumptions of Proposition 3 are:

(a) $x_t$ and $s_t$ are $\mathcal F_t$ -measurable;
(b) there are $c_1,c_2>0$ with $c_1\|\nabla f(x_t)\|^2\le-\nabla f(x_t)'s_t$ and $\|s_t\|\le c_2(1+\|\nabla f(x_t)\|)$ for all $t$ ; (4.1)
(c) for all $t$ , with probability 1, $E[w_t\mid\mathcal F_t]=0$ (4.2) and $E[\|w_t\|^2\mid\mathcal F_t]\le A(1+\|\nabla f(x_t)\|^2)$ (4.3), with $A>0$ deterministic;
(d) $\sum_t\gamma_t=\infty$ and $\sum_t\gamma_t^2<\infty$ .

The noise variance in (c) may grow quadratically with $\|\nabla f(x_t)\|$ and is therefore unbounded in general. A point $\bar x$ is stationary if $\nabla f(\bar x)=0$ .

Formalization targets

Goal: Proposition 3 (p. 635)

Under (2.1) and (a)–(d), with probability 1,

f(x_t)\to-\infty\quad\text{or}\quad\Bigl(f(x_t)\to\ell\in\mathbb R\ \text{ and }\ \nabla f(x_t)\to 0\Bigr),

and every limit point of $(x_t)$ is a stationary point of $f$ . The dichotomy is per sample path: different paths may take different branches.

Milestones

(4.4), p. 636. The pathwise one-step inequality: if $\gamma\,2Lc_2^2\le c_1/2$ and $s$ satisfies (4.1) at $x$ , then for every $w$ ,

f(x+\gamma(s+w))\le f(x)-\gamma\tfrac{c_1}{2}\|\nabla f(x)\|^2+\gamma\nabla f(x)'w+\gamma^2 2Lc_2^2+\gamma^2L\|w\|^2.

Lemma 2, p. 637. If $r_t$ is $\mathcal F_{t+1}$ -measurable with $E[r_t\mid\mathcal F_t]=0$ , $E[\|r_t\|^2\mid\mathcal F_t]\le B$ and $\sum\gamma_t^2<\infty$ , then $\sum_{t\le T}\gamma_tr_t$ and $\sum_{t\le T}\gamma_t^2\|r_t\|^2$ converge almost surely.
Lemma 6, p. 640. For every $\delta>0$ , almost surely $f(x_t)$ converges to a finite value or to $-\infty$ , and if the limit is not $-\infty$ then $\limsup_t\|\nabla f(x_t)\|\le\delta$ .

Further result: §5, pp. 641–642

For $f=\frac1m\sum_i f_i$ with Lipschitz gradients $\nabla f_i$ satisfying $\|\nabla f_i(x)\|\le C+D\|\nabla f(x)\|$ (5.2), the randomized incremental gradient method $x_{t+1}=x_t-\gamma_t\nabla f_{k(t)}(x_t)$ , with independent uniform indices $k(t)$ , satisfies the conclusion of Proposition 3.

Significance

Proposition 3 is a convergence guarantee for stochastic gradient descent on smooth nonconvex objectives that needs neither a lower bound on $f$ , nor bounded iterates, nor bounded noise variance. It contains, as special cases, stochastic gradient descent with unbiased gradient estimates whose variance grows with the gradient, the randomized incremental (single-sample) gradient method for finite sums of Section 5, and scaled or approximate gradient directions through condition (4.1). Its conclusion is the strongest one available at this generality: if $f(x_t)$ stays bounded below along a path, then the gradient vanishes along that path and every limit point is stationary.

The result is proved in the paper; to our knowledge it has not been machine-checked. Its formalization requires a working theory of generalized conditional expectations of non-integrable noise, square-integrable martingales in $\mathbb R^n$ and pathwise arguments over random interval partitions, which is reusable for other stochastic approximation results (Robbins–Monro type schemes, TD-learning, stochastic subgradient methods).

Difficulty

The natural first idea is to view $f(x_t)$ as a supermartingale up to summable errors and apply the supermartingale convergence theorem (Robbins–Siegmund). This fails here: the theorem needs $f(x_t)$ bounded below, and $f$ is not assumed bounded below; in addition the noise term $\gamma_t^2L\|w_t\|^2$ in (4.4) has conditional mean of order $\gamma_t^2\|\nabla f(x_t)\|^2$ , which is not summable when the gradient is unbounded. Any argument must therefore extract a decrease of $f$ that dominates noise of the same order as the gradient itself, without a lower bound to anchor a supermartingale, and must do so along every sample path while the hypotheses are only conditional-expectation statements about non-integrable noise.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient f, $f$ is ContDiff ℝ 1, and the Lipschitz constant is L : ℝ≥0 with LipschitzWith L (gradient f) (the standing assumption (2.1), equivalent to the page's form).
The probability space is a Measure Ω with IsProbabilityMeasure, the $\sigma$ -fields are a Mathlib Filtration ℕ, and measurability in (a) is StronglyMeasurable[ℱ t]. The recursion and (4.1) hold on every sample path. Stepsizes are deterministic.
Conditional expectations of the noise. The page assumes no integrability of $w_t$ , of $\|w_t\|^2$ or of $f(x_t)$ , and none is added. Mathlib's condExp is $0$ for non-integrable functions, so stating (4.2)–(4.3) with it would make them hold vacuously for any non-integrable noise; that encoding is ruled out. Instead (4.3) says that for every $\mathcal F_t$ -measurable set $S$ , $\int_S\|w_t\|^2\,dP\le\int_S A(1+\|\nabla f(x_t)\|^2)\,dP$ (in $[0,\infty]$ ), and (4.2) says that $\int_S w_t\,dP=0$ for every $\mathcal F_t$ -measurable $S$ on which $w_t$ is integrable. These are exactly the generalized conditional-expectation statements of the page.
In Lemma 2 the bound $B$ is a constant, so Mathlib's condExp is used there, with integrability of $\|r_t\|^2$ stated explicitly; the page's hypothesis implies it. Lemma 2 is stated over any finite-dimensional real inner-product space, since the paper applies it to real and to vector-valued sequences.
$\sum\gamma_t=\infty$ is divergence of the partial sums; $\sum\gamma_t^2<\infty$ is Summable. Convergent random series (Lemma 2) are convergence of partial sums, not Summable, which would mean unconditional convergence. " $\limsup\|\nabla f(x_t)\|\le\delta$ " is "for every $\delta'>\delta$ , eventually $\|\nabla f(x_t)\|\le\delta'$ ". Limit points are MapClusterPt.
In the §5 result the page's references to "section 4" and "(4.1)" are read as section 3 and condition (3.1), the indices $k(t)$ run from $t=0$ , $x_0$ is deterministic, and the stepsizes are nonnegative as on the page.
Not stated: Lemma 3 (it needs the random interval construction of p. 636 as a definition), Lemmas 4–5 (steps that depend on the proof's own choice of $\epsilon$ ), and the Remarks of §4.

Contributions welcome: a proof of Lemma 2 from Mathlib's martingale convergence theorems (Submartingale.exists_ae_tendsto_of_bdd), a proof of (4.4) from the descent lemma, a general bridge between the set-integral encoding of conditional expectations and Mathlib's condExp on localizing sets, and the interval construction behind Lemmas 3–6.

Selected references

D. P. Bertsekas and J. N. Tsitsiklis, Gradient Convergence in Gradient Methods with Errors, SIAM J. Optim. 10(3):627–642, 2000. https://doi.org/10.1137/S1052623497331063
B. T. Poljak and Y. Z. Tsypkin, Pseudogradient adaptation and training algorithms, Automat. Remote Control 12 (1973), 83–94.
H. J. Kushner and D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978.
H. J. Kushner and G. Yin, Stochastic Approximation Methods, Springer, 1996 (as cited in the paper).
A. Benveniste, M. Métivier and P. Priouret, Adaptive Algorithms and Stochastic Approximations, Springer, 1990.
D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996.

4 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Air Travel Demand and Airline Seat Inventory Management III: Gaussian EMSR Protection Levels and Their SensitivityTextbook

Why protection levels and their inputs matter

An airline sells the seats of one flight leg in several fare classes at different prices. Low-fare passengers usually book first, so the airline must decide how many seats to keep back, or protect, for later high-fare passengers. Peter Belobaba's 1987 MIT dissertation introduced the expected marginal seat revenue (EMSR) rule for this decision, and EMSR-type rules became a standard of airline revenue management practice (Talluri and van Ryzin 2004). A protection level is computed from a demand forecast, and forecasts are uncertain. Section 6.2 of the dissertation asks how the protection level moves when its inputs move: the mean of forecast demand, its standard deviation, and the ratio of the two fares. That question decides where forecasting effort pays off, and this mission formalizes the answers the dissertation gives for Gaussian demand.

This is the third mission in a series on the dissertation. The first treats marginal allocation among distinct fare classes, and the second the two-class nested protection level in the discrete model, including its revenue optimality. This mission takes the continuous Gaussian model of Chapter 6 on its own terms.

Setting

Let $r$ be the number of requests for a fare class, a real random variable with law $\mu$ . For a seat level $S \in \mathbb R$ the tail probability is

\bar P(S) = P[r \ge S],

and for the fare $f$ of the class the expected marginal seat revenue is $\mathrm{EMSR}(S) = \bar P(S)\cdot f$ (Eqs. (6.1)–(6.2)).

There are two classes: class 1 with fare $f_1$ and class 2 with fare $f_2$ , where $0 < f_2 < f_1$ . Requests for class 1 are Gaussian with estimated mean $\bar r$ and estimated standard deviation $\hat\sigma > 0$ , written $r_1 \sim N(\bar r, \hat\sigma^2)$ . A real number $S$ is an EMSR protection level for class 1 against class 2 when

\bar P_1(S) = P[r_1 \ge S] = \frac{f_2}{f_1} \qquad \text{(Eq. (6.10))}.

The standardized level $Z$ is the value "which has a probability of $f_2/f_1$ of being exceeded" by a standard normal variable:

P[N(0,1) \ge Z] = \frac{f_2}{f_1}.

In the Lean development these are tailProb, emsr, gaussianLaw rbar σ, stdNormal, IsProtectionLevel rbar σ f₁ f₂ S and IsStdNormalLevel f₁ f₂ Z, all in the namespace SeatInventory.Gaussian.

Formalization targets

Goal: the Gaussian protection level and its sensitivity to $\hat\sigma$

For $\hat\sigma > 0$ and $0 < f_2 < f_1$ :

Eq. (6.10) has exactly one solution $S$ , and the standard normal equation has exactly one solution $Z$ ;
they satisfy

S = \bar r + Z\hat\sigma \qquad \text{(Eq. (6.12))};

$Z < 0$ if $f_2/f_1 > 1/2$ , $Z > 0$ if $f_2/f_1 < 1/2$ , $Z = 0$ if $f_2/f_1 = 1/2$ (Eq. (6.14)), and $S = \bar r$ in the last case;
if $\hat\sigma' > \hat\sigma$ and $S'$ solves (6.10) for $N(\bar r, \hat\sigma'^2)$ , then $S' < S$ , $S' > S$ or $S' = S$ according as $f_2/f_1$ is above, below or equal to $1/2$ .

The goal states no numerical constant and no particular fare ratio; it fixes only the shape of the dependence.

Milestones, in attack order

Eq. (6.1)–(6.2): for any request law, $\bar P$ and $\mathrm{EMSR}$ are non-increasing in $S$ .
Eq. (6.10): the Gaussian protection level exists and is unique.
Eq. (6.11)–(6.12): $S = \bar r + Z\hat\sigma$ .
p. 154: with $\hat\sigma$ and the fares fixed, replacing $\bar r$ by $\bar r + c$ replaces $S$ by $S + c$ .
Eq. (6.14): the sign of $Z$ , and $S = \bar r$ at fare ratio $1/2$ for every $\hat\sigma$ .
p. 154: the effect of $\hat\sigma$ on $S$ (part 4 of the goal on its own).
p. 157: $Z$ and $S$ decrease strictly as the fare ratio $f_2/f_1$ increases.

The dissertation's constant-coefficient-of-variation form, Eq. (6.13), $S = \bar r(1 + Zk)$ with $k = \hat\sigma/\bar r$ , follows from (6.12) by substitution and is not stated separately.

Significance

The result gives every Gaussian protection level as a closed form in one standard normal quantile. From it come the three sensitivities that Sect. 6.2 uses to argue for better forecasts. The protection level moves one-for-one with mean demand. The standard deviation moves it in a direction fixed only by whether the discount fare is above or below half the full fare. A higher fare ratio always lowers it. The dissertation uses these facts, and its Figures 6.1 and 6.2, to argue that reducing the estimated standard deviation of demand narrows the range of protection levels a forecast can produce. The same quantile structure is behind Littlewood's rule and the newsvendor critical fractile, so the statements here are the Gaussian specialization of a pattern that recurs throughout revenue management and inventory theory.

All the statements are classical and easy to believe. None of them, to our knowledge, has a machine-checked proof. Mathlib provides the Gaussian law and its affine images, but no standard normal quantile and no statement that a Gaussian tail is a strictly decreasing bijection onto $(0,1)$ . Formalizing this mission produces both, in a form that can be used again wherever a normal critical fractile appears.

Difficulty

Most of the work is in the existence and uniqueness of the two tail solutions. The tail $S \mapsto P[r_1 \ge S]$ must be shown continuous, strictly decreasing, and to take every value in $(0,1)$ . Strictness needs the Gaussian density to be positive everywhere, and existence needs a limit argument at both ends. Monotonicity alone, which holds for every law (Eqs. (6.1)–(6.2)), gives neither, because a general law can have flat stretches and jumps in its tail. The relation $S = \bar r + Z\hat\sigma$ then requires transporting the tail of $N(\bar r,\hat\sigma^2)$ to that of $N(0,1)$ through the affine map $x \mapsto (x - \bar r)/\hat\sigma$ , and the sign of $Z$ requires the symmetry of $N(0,1)$ , namely $P[N(0,1) \ge 0] = 1/2$ . Once uniqueness is available, each sensitivity statement follows from these facts. The tempting shortcut of reading $S = \bar r + Z\hat\sigma$ as a definition is ruled out below.

Formalization scope

Continuous seats. Protection levels and $Z$ are real numbers, as in the dissertation's own Gaussian example ( $Z = -0.675$ at fare ratio $0.75$ ). This differs from the first two missions of the series, which count seats in $\mathbb N$ . For a continuous law $P[r \ge S] = P[r > S]$ , so the two definitions of $\bar P$ the dissertation uses (Eq. (5.2) and Eq. (6.2)) coincide here.
Gaussian law. $N(\bar r, \hat\sigma^2)$ is Mathlib's gaussianReal rbar (σ^2), parameterised by the variance. Every theorem assumes $\hat\sigma > 0$ ; at $\hat\sigma = 0$ the law is a Dirac mass and (6.10) has no solution.
Fares. $0 < f_2 < f_1$ , so $f_2/f_1 \in (0,1)$ . This is the dissertation's " $f_2 < f_1$ " together with positive fares.
Relational sensitivity. The sensitivity statements compare any two solutions of (6.10) under the two input values. Together with uniqueness, this is the same as monotonicity of the solution map. No function is defined by a choice operator.
Tail as a real number. $\bar P(S)$ is the measure of $[S,\infty)$ as a real number. The law is a probability measure, so nothing is truncated.
No trivialization. $S$ is defined only by the tail equation (6.10) for $N(\bar r, \hat\sigma^2)$ , and $Z$ only by the tail equation for $N(0,1)$ . Neither is defined by the formula $S = \bar r + Z\hat\sigma$ , which would make Eq. (6.12) true by definition.
Not covered. The revenue optimality of the level defined by (6.10) belongs to the second mission. The multi-class EMSR rules (5.19)–(5.29) are not optimal for three or more classes and are not stated. The empirical analysis of Sect. 6.1 is out of scope.

Useful infrastructure, all reusable: the strict monotonicity, continuity and range of Gaussian tails; the standard normal quantile; and tail transport under affine maps. Contributions of these as separate lemmas are welcome.

Selected references

P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT Flight Transportation Laboratory Report R87-7, 1987. (no DOI; the source PDF of this mission).
P. P. Belobaba, Application of a probabilistic decision model to airline seat inventory control, Operations Research 37(2):183–197, 1989. https://doi.org/10.1287/opre.37.2.183
K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4:111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134
K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

9 thms2 active usersReviewed

Operations Research·Captain: mikedeng1

Sequencing with Earliness and Tardiness Penalties: With Due-Date Tolerances, the Least Optimal Common Due Date Puts One Job at an End of Its Tolerance WindowResearch Paper

Motivation

Earliness/tardiness (E/T) scheduling penalizes a job both for finishing late and for finishing early. It models just-in-time production, where an early job ties up inventory and a late one delays a customer. Baker and Scudder's review (Oper. Res. 38 (1990) 22–36) organized the single-machine E/T literature around a short list of structural properties of optimal schedules for a common due date shared by all jobs. For the problem without tolerances these properties go back to work the review surveys, beginning with Kanet (1981) for equal penalties.

The review then turns to due-date tolerances: a job pays nothing if it completes within a window around the due date, as in contracts that accept delivery within a few days of a target. Cheng (1988) studied a version in which the penalty is discontinuous at the window ends. Baker and Scudder state the continuous version and prove two generalized properties, III(G) and IV(G), in the paper's Appendix (pp. 34–35). They are the paper's own results; the rest of the review cites results proved elsewhere.

Setting

Fix $n \ge 1$ jobs, processed on one machine in a fixed order, one after another, starting at time $0$ with no idle time between them. The job in position $j$ has a processing time $p_j$ , so it completes at $C_j = p_1 + \dots + p_j$ . All jobs share a common due date $d \in \mathbb R$ , which is a decision variable. Job $j$ has tolerances $u_j, v_j \ge 0$ and is free of penalty when $C_j \in [d - u_j,\ d + v_j]$ . Outside its window it pays a unit earliness penalty $\alpha_j > 0$ or a unit tardiness penalty $\beta_j > 0$ :

E_j = (d - C_j - u_j)^+,\qquad T_j = (C_j - d - v_j)^+,\qquad f(d) = \sum_{j=1}^n \bigl(\alpha_j E_j + \beta_j T_j\bigr).

The tolerances are small compared with the processing times: $p_j - v_j - u_i > 0$ for distinct jobs $i \ne j$ . Under this condition at most one job can avoid penalty costs. A due date is optimal if it minimizes $f$ over $\mathbb R$ , and the least optimal due date is the smallest optimal one. The paper minimizes $d$ as a secondary criterion when there are alternative optima.

In Lean the model is BakerScudder1990.Tolerance.Instance n, with fields p u v α β : Fin n → ℝ, completion times I.C, earliness I.earliness d, tardiness I.tardiness d, total penalty I.cost d, and the predicates I.IsOptimalDueDate and I.IsLeastOptimalDueDate.

Formalization targets

Goal: Property IV(G)

Let $d$ be the least optimal due date and let $b$ be the number of jobs with $T_j = 0$ . Then a least optimal due date exists, and exactly one of the following holds:

\begin{aligned} C_b &= d + v_b \quad\text{with}\quad \textstyle\sum_{i<b}\alpha_i < \sum_{i\ge b}\beta_i,\ \ \sum_{i<b}\alpha_i \ge \sum_{i>b}\beta_i,\\ C_b &= d - u_b \quad\text{with}\quad \textstyle\sum_{i<b}\alpha_i < \sum_{i>b}\beta_i,\ \ \sum_{i\le b}\alpha_i \ge \sum_{i>b}\beta_i. \end{aligned}

The case labels follow the paper's proof. The printed statement swaps them (see Formalization scope).

Milestones

Case 1 of the proof of III(G). Between the window of job $j-1$ and the window of job $j$ , $f$ is affine with slope $\sum_{i<j}\alpha_i - \sum_{i\ge j}\beta_i$ . Before the first window and after the last, the slopes are $-\sum_i\beta_i$ and $\sum_i\alpha_i$ .
Case 2 of the proof of III(G). Inside the window of job $j$ , $f$ is affine with slope $\sum_{i<j}\alpha_i - \sum_{i>j}\beta_i$ .
Property III(G). A least optimal due date exists, and at it some job completes at $d - u_j$ or at $d + v_j$ .
The two optimality conditions. The first pair of inequalities above makes $C_j - v_j$ the least optimal due date, and the second pair makes $C_j + u_j$ the least optimal due date.

Significance

III(G) reduces the choice of an optimal common due date for a given sequence to $2n$ candidates. IV(G) goes further and names the candidate directly from prefix and suffix sums of the penalties. Baker and Scudder use this to say which V-shaped sequences remain candidates for optimality, so that an enumeration over sequences can discard the others. With $u_j = v_j = 0$ the two properties reduce to the classical common-due-date conditions: some job completes exactly at $d$ , and which one is fixed by a weighted-median condition.

The results are proved in the paper, so the formalization does not settle an open question. It produces a machine-checked version of the Appendix, with two printed errors corrected, and a reusable model of single-machine E/T costs with tolerance windows. No earliness/tardiness model or result was formalized on Prove2Me as of October 2026.

Difficulty

Each linear piece of $f$ is elementary. The work lies in showing that the pieces are the claimed ones: the tolerance condition must imply that a job before position $j$ is early, and a job after it tardy, throughout each gap and window. That needs the ordering $C_i + u_i < C_j - v_j$ for every $i < j$ , not only for consecutive jobs. The second point is the least optimal due date. Optimality alone does not determine $d$ on a flat stretch of $f$ , where every point is optimal and only the left end satisfies the strict inequalities. Existence of a least minimizer also has to be shown, from the two outer slopes and finitely many breakpoints. Finally, the count $b$ of jobs without tardiness must be matched to the position of the critical job at both kinds of breakpoint.

Formalization scope

Jobs are indexed by 0-based positions Fin n, so the paper's job $b$ is position $k = b - 1$ and the goal states the count of untardy jobs as $k+1$ . Data are real numbers. $(x)^+$ is max 0 x.
The sequence starts at time $0$ and $d$ ranges over all of $\mathbb R$ ; this is the unrestricted problem, which is the one where the paper asserts III(G) and IV(G). Shifting the start time is equivalent to shifting $d$ .
"In an optimal schedule" is read for a fixed sequence and its least optimal due date. If a sequence and due date are jointly optimal with $d$ least among such optima, then $d$ is the least optimal due date for that sequence, so this reading implies the paper's.
The tolerance condition is assumed only for distinct jobs. That is a weaker hypothesis than the literal "for all pairs $(i,j)$ ", so the theorems are stronger.
Errata, corrected and disclosed. (i) IV(G) is printed (p. 30 and p. 35) with its two case labels swapped relative to its own proof. One job with $u_1, v_1 > 0$ has least optimal due date $C_1 - v_1$ , so $C_1 = d + v_1$ while the first condition pair holds. (ii) In Cases 1 and 2 the identity is printed as $f(S) - f(S') = [\dots]\varepsilon$ ; the correct one is $f(S') - f(S) = [\dots]\varepsilon$ . The milestone texts are quoted as printed; the Lean states the corrected mathematics.
Existence of a least optimal due date is a conjunct of III(G) and of IV(G), and both assume $n \ge 1$ . A version quantifying only over least optimal due dates without existence would be vacuous. A version for every optimal due date would be false. Neither is acceptable.
The optimality conditions are stated as sufficient. Their converse fails when $u_j = v_j = 0$ .
Properties I and II (no inserted idle time, V-shaped sequences) are quoted in the paper, not proved there, and are not formalized. Optimization over sequences is out of scope.
Welcome contributions: proofs of the two slope identities (finite sums of max 0 terms with a sign determined on each piece), a general lemma that a convex piecewise-linear coercive function on $\mathbb R$ attains its least minimizer at a breakpoint, and the special cases $u = v = 0$ as corollaries.

Selected references

K. R. Baker and G. D. Scudder, Sequencing with earliness and tardiness penalties: a review, Operations Research 38(1) (1990) 22–36. https://doi.org/10.1287/opre.38.1.22
J. J. Kanet, Minimizing the average deviation of job completion times about a common due date, Naval Research Logistics Quarterly 28 (1981) 643–651 (as cited in Baker and Scudder 1990).
U. Bagchi, R. S. Sullivan and Y.-L. Chang, Minimizing mean absolute deviation of completion times about a common due date, Naval Research Logistics Quarterly 33 (1986) 227–240 (as cited in Baker and Scudder 1990).
T. C. E. Cheng, Optimal common due date with limited completion time deviation, Computers & Operations Research 15 (1988) 91–96 (as cited in Baker and Scudder 1990).

6 thms2 active usersReviewed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

Online Scheduling of a Single Machine to Minimize Total Weighted Completion Time: Delayed SWPT Has Competitive Ratio 2Research Paper

Motivation

A single machine must process $n$ jobs that arrive over time. Job $j$ is released at time $r_j$ , needs $p_j$ units of uninterrupted processing, and has weight $w_j > 0$ ; the goal is to minimize the total weighted completion time $\sum_j w_j C_j$ . Offline, with all release dates equal to zero, Smith's rule (sequence by nondecreasing $p_j/w_j$ ) is optimal (Smith 1956); with arbitrary release dates the problem $1\,|\,r_j\,|\,\sum w_j C_j$ is strongly NP-hard (Lenstra, Rinnooy Kan and Brucker 1977).

In the online version the scheduler learns of job $j$ only at time $r_j$ , and at each moment must either start a released job or keep the machine idle. Its quality is measured by its competitive ratio: the worst case, over all instances, of the ratio between the online schedule's cost and the offline optimum. Release-date scheduling is one of the basic test cases of online optimization.

Timeline:

1996. Hoogeveen and Vestjens show that no online algorithm has competitive ratio below 2, even with equal weights, and give the 2-competitive algorithm Delayed SPT for equal weights.
1997. Hall, Schulz, Shmoys and Wein give a $(3+\varepsilon)$ -competitive algorithm for arbitrary weights, based on geometric intervals and linear programming.
1998. Phillips, Stein and Wein give another 2-competitive algorithm for equal weights, which does not extend to arbitrary weights.
2002. Goemans, Queyranne, Schulz, Skutella and Wang obtain a $(1+\sqrt2)$ -competitive deterministic algorithm from an LP relaxation.
2004. Anderson and Potts show that Delayed SWPT has competitive ratio exactly 2 for arbitrary positive weights, matching the lower bound.

Setting

An instance has jobs $j \in J = \{1,\dots,n\}$ with integer release dates $r_j \ge 0$ , integer processing times $p_j \ge 1$ and real weights $w_j > 0$ . A schedule assigns each job an integer start time $S_j$ . It is feasible if $S_j \ge r_j$ for every $j$ and no two intervals $[S_j, S_j + p_j)$ overlap; idle time is allowed. Its cost is $C(S) = \sum_j w_j (S_j + p_j)$ .

Delayed SWPT runs over unit time slots $[t, t+1)$ . When the machine is available at time $t$ , it looks at the jobs released by $t$ and not yet started, and selects one with the smallest ratio $p_j/w_j$ . Ties go to the smaller $p_j$ , then to the smaller index. If $p_j \le t$ , it starts $j$ at $t$ and the machine is busy until $t + p_j$ . Otherwise the machine stays idle and the rule is applied again at $t+1$ . The resulting schedule is written $\pi$ , or dswpt I in Lean. In particular no job starts before time $p_j$ .

The proof uses three auxiliary problems:

the doubled problem (2P), with data $(2r_j, 2p_j, w_j)$ ;
the extended problem (E), with release dates $r'_j = \max\{p_j, f(r_j)\}$ , where $f(t)$ is the first time at or after $t$ at which $\pi$ leaves the machine free;
one unit-length gap job $g_t$ for each slot $[t,t+1)$ in which Delayed SWPT idles although a job $j$ is available. The gap job has release date $f(r_j)$ and weight $w_j/p_j$ .

The schedule $\pi_E$ of (E) runs the original jobs as in $\pi$ and each $g_t$ in $[t,t+1)$ .

Formalization targets

Goal: Theorem 8

\min\Bigl\{\rho \;:\; \sum_j w_j C_j(\pi) \le \rho \sum_j w_j C_j(S)\ \text{for every instance and every feasible schedule } S\Bigr\} = 2.

Lean: IsLeast {ρ | ∀ n I S, IsFeasible I.r I.p S → cost I.w I.p (dswpt I) ≤ ρ * cost I.w I.p S} 2. Both halves are required: the upper bound $2$ and the fact that no smaller constant is valid for this algorithm.

Milestones

$\pi_j \ge p_j$ for every job (§2) and $r'_j \le \max\{2r_j, p_j\}$ (§3.2).
$\pi_E$ is feasible for (E) (§3.2).
Lemma 1. If $\pi^*$ and $\mu^*$ are optimal for (P) and (2P), then $C(\mu^*) = 2\,C(\pi^*)$ .
Lemma 2. $\pi_E$ is optimal for (E).
Lemma 3. If $\mu^*$ is optimal for (2P) and a feasible $\sigma_E$ for (E) satisfies

\sum_{j\in J} w_j C_j(\sigma_E) + \sum_{g\in G} w_g C_g(\sigma_E) \le \sum_{j\in J} w_j C_j(\mu^*) + \sum_{g\in G} w_g C_g(\pi_E), \tag{1}

then $C(\pi) \le 2\,C(S)$ for every feasible $S$ . 6. Inequality (1) holds for some feasible $\sigma_E$ , for every optimal $\mu^*$ of (2P) (§§3.4–3.6).

Significance

The theorem shows that a deterministic online algorithm can match the lower bound of Hoogeveen and Vestjens for arbitrary positive weights. This settles the best competitive ratio for deterministic online algorithms for $1\,|\,r_j\,|\,\sum w_j C_j$ . The algorithm needs no linear program. The analysis also does not compare the algorithm with a lower bound on the optimum. Instead it shows that the online schedule is optimal for a modified problem (E), and it converts an optimal schedule of (2P) into a schedule of (E).

The result was proved on paper in 2004. Neither Mathlib nor the Prove2Me catalog contains a machine-checked proof of it, or of any competitive ratio for online scheduling with release dates. This mission provides several reusable pieces:

an executable, verified-terminating definition of an online scheduling rule;
the doubling lemma for release-date problems;
the optimality criterion behind Lemma 2;
the block-by-block exchange argument of §§3.3–3.6.

Difficulty

The obvious argument fails at Lemma 2. Delayed SWPT is far from optimal for (P) itself, and its idle time is unbounded in relative terms. The proof therefore has to show that the inserted gap jobs make every idle slot "justified", so that a preemptive best-available argument becomes valid for (E). That argument rests on an optimality criterion of Belouadah, Posner and Potts (1992), which is not in Mathlib.

The second difficulty is inequality (1). Once $\mu^*$ is doubled and the gap jobs are inserted, nongap jobs must be shifted, and the gain of each gap-generating job must be charged against the delay of the gap jobs in its block. That accounting (Lemmas 4–7 of the paper) is an induction over blocks with signed differences of completion times.

The natural first idea, plain online SWPT (start the available job with the smallest $p_j/w_j$ whenever the machine is free), has no finite competitive ratio (Example 1 of the paper), so the delay $\pi_j \ge p_j$ is essential to the bound and must be tracked through the whole argument.

Formalization scope

Conventions committed to in Lean:

Data. Jobs are Fin n (0-based, so "smallest index" is the order of Fin n). Times are natural numbers, the paper's standing integer-data assumption (p. 688), and weights are real. Every instance carries $p_j \ge 1$ and $w_j > 0$ .
Schedules and optimality. Schedules are integer start times. Feasibility, cost and optimality are defined for any finite job type, so (E), with job type Fin n ⊕ gapTimes I, uses the same notions. "Optimal" means optimal among all feasible nonpreemptive schedules with integer start times.
The algorithm. Delayed SWPT is a def: a unit-time simulation that compares ratios by cross-multiplication and re-applies the rule at every slot. It runs to the horizon $\sum_j (r_j + 2p_j) + 1$ . A sorry-free check (not uploaded) shows that every job has started by then, and that the simulation reproduces Examples 3 and 4 of the paper, including the gap times $0,2,3,4,5,6$ of Table 2.
Completion times. In (2P) the completion time is $\mu^*_j + 2p_j$ , and gap jobs have unit length.

The goal quantifies over every feasible schedule of every instance. It cannot be met by restricting the competitor to schedules without idle time or to list schedules, by dropping release-date feasibility, or by leaving jobs unscheduled.

Out of scope:

The general lower bound "no online algorithm beats 2" (Example 2 of the paper, due to Hoogeveen and Vestjens) is not part of the mission. The lower half of the goal concerns Delayed SWPT only.
The Belouadah–Posner–Potts optimality criterion is an external ingredient of Lemma 2. Solvers may formalize it as a supporting theorem.

Infrastructure that a complete development needs:

simulation invariants for the algorithm;
exchange and left-shift arguments for single-machine schedules;
the job-splitting relaxation behind the best-available criterion.

The schedule vocabulary and the criterion are reusable for other release-date scheduling results. Contributions toward the block lemmas of §§3.3–3.6 (Lemmas 4–7, the bound (9)) are welcome as supporting theorems.

Selected references

E. J. Anderson and C. N. Potts, Online Scheduling of a Single Machine to Minimize Total Weighted Completion Time, Mathematics of Operations Research 29(3), 686–697, 2004. https://doi.org/10.1287/moor.1040.0092
J. A. Hoogeveen and A. P. A. Vestjens, Optimal On-Line Algorithms for Single-Machine Scheduling, IPCO 1996, LNCS 1084, 404–414. https://doi.org/10.1007/3-540-61310-2_30
L. A. Hall, A. S. Schulz, D. B. Shmoys and J. Wein, Scheduling to Minimize Average Completion Time: Off-line and On-line Approximation Algorithms, Mathematics of Operations Research 22(3), 513–544, 1997. https://doi.org/10.1287/moor.22.3.513
C. Phillips, C. Stein and J. Wein, Minimizing Average Completion Time in the Presence of Release Dates, Mathematical Programming 82, 199–223, 1998. https://doi.org/10.1007/BF01585872
M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella and Y. Wang, Single Machine Scheduling with Release Dates, SIAM Journal on Discrete Mathematics 15(2), 165–192, 2002. https://doi.org/10.1137/S089548019936223X
H. Belouadah, M. E. Posner and C. N. Potts, Scheduling with Release Dates on a Single Machine to Minimize Total Weighted Completion Time, Discrete Applied Mathematics 36(3), 213–231, 1992. https://doi.org/10.1016/0166-218X(92)90255-9
J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3, 59–66, 1956. https://doi.org/10.1002/nav.3800030106

11 thms2 active usersReviewed

Completed

Convex Optimization Numerical Analysis·Captain: mikedeng1

The Rate of Convergence of Nesterov's Accelerated Forward-Backward Method is Actually Faster than 1/k^2 I: For α > 3, (Ψ + Φ)(x_k) − min(Ψ + Φ) = o(k⁻²) and ‖x_{k+1} − x_k‖ = o(k⁻¹)Research Paper

Motivation

Many problems in signal processing, statistics and machine learning take the form

\min_{x\in\mathcal H}\ \Psi(x)+\Phi(x),

where $\Phi$ is smooth and convex (a data-fit term) and $\Psi$ is convex but possibly nonsmooth or infinite-valued (an $\ell^1$ penalty, the indicator function of a constraint set). The forward-backward method alternates a gradient step on $\Phi$ with a proximal step on $\Psi$ and reduces the objective gap at rate $O(k^{-1})$ after $k$ iterations. Combining it with Nesterov's extrapolation scheme gives the accelerated forward-backward method, best known as FISTA, which improves the guaranteed rate to $O(k^{-2})$ . FISTA and its variants are standard solvers for sparse recovery and image reconstruction.

Timeline:

1983. Nesterov introduces the extrapolation scheme for smooth convex minimization, with an $O(k^{-2})$ rate for function values (Nesterov 1983).
2009. Beck and Teboulle extend it to the composite problem above (FISTA), with the $O(k^{-2})$ rate (doi:10.1137/080716542).
2014. Su, Boyd and Candès read the scheme as a discretization of the ODE $\ddot x+\frac{\alpha}{t}\dot x+\nabla\Theta(x)=0$ (arXiv:1503.01243).
2014–2015. Chambolle and Dossal (doi:10.1007/s10957-015-0746-4) and, independently, Attouch, Chbani, Peypouquet and Redont (arXiv:1507.04782) prove weak convergence of the iterates for the variant with parameter $\alpha>3$ . Before that, convergence of the iterates had been open for about two decades.
2015. May shows that for $\alpha>3$ the continuous-time gap is $o(t^{-2})$ (arXiv:1509.05598).
2016. Attouch and Peypouquet prove the discrete analogue: for $\alpha>3$ the function gap of the algorithm is $o(k^{-2})$ and the velocity is $o(k^{-1})$ (arXiv:1510.08740, SIAM J. Optim. 26(3):1824–1834).

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . Let:

$\Psi:\mathcal H\to\mathbb R\cup\{+\infty\}$ be proper (finite somewhere), lower semicontinuous and convex;
$\Phi:\mathcal H\to\mathbb R$ be convex and continuously differentiable, with gradient $\nabla\Phi$ Lipschitz continuous with constant $L$ ;
$\Theta=\Psi+\Phi$ , and assume the set of minimizers $S=\operatorname{argmin}\Theta$ is nonempty.

For $s>0$ , the proximal map $\operatorname{prox}_{s\Psi}(z)$ is the unique minimizer of $u\mapsto\Psi(u)+\frac1{2s}\|u-z\|^2$ . Given $\alpha>0$ , a step size $0<s<1/L$ and starting points $x_0,x_1$ , algorithm (2) generates

y_k=x_k+\frac{k-1}{k+\alpha-1}(x_k-x_{k-1}),\qquad x_{k+1}=\operatorname{prox}_{s\Psi}\big(y_k-s\nabla\Phi(y_k)\big),\qquad k\ge1.

The common choice is $\alpha=3$ ; this mission concerns $\alpha>3$ .

The proofs use the operator $G_s(y)=\frac1s\big(y-\operatorname{prox}_{s\Psi}(y-s\nabla\Phi(y))\big)$ , the sequence $z_k=x_k+\frac{k-1}{\alpha-1}(x_k-x_{k-1})$ , a minimizer $x^*$ , and the quantity

\mathcal E(k)=\frac{2s}{\alpha-1}(k+\alpha-2)^2\big(\Theta(x_k)-\Theta(x^*)\big)+(\alpha-1)\|z_k-x^*\|^2 .

Write $\theta_k=\Theta(x_k)-\Theta(x^*)$ and $d_k=\frac1{2s}\|x_{k+1}-x_k\|^2$ .

Formalization targets

Goal: Theorem 1 (p. 2)

For $\alpha>3$ and $0<s<1/L$ ,

\lim_{k\to\infty}k^2\big(\Theta(x_k)-\min\Theta\big)=0\qquad\text{and}\qquad\lim_{k\to\infty}k\,\|x_{k+1}-x_k\|=0.

The statement fixes no constants, so it is unaffected by later improvements of the explicit bounds below.

Milestones (in attack order)

(9), p. 2. If $sL\le1$ , then for all $x,y$ : $\Theta(y-sG_s(y))\le\Theta(x)+\langle G_s(y),y-x\rangle-\frac s2\|G_s(y)\|^2$ .
(13), p. 3. For $\alpha\ge3$ and $k\ge1$ : $\mathcal E(k+1)+2s\frac{\alpha-3}{\alpha-1}k\,\theta_k\le\mathcal E(k)$ .
Fact 1, p. 3. $(\mathcal E(k))$ is nonincreasing and has a finite limit.
Fact 2, p. 3. $\theta_k\le\frac{(\alpha-1)\mathcal E(1)}{2s(k+\alpha-2)^2}$ and $\|z_k-x^*\|^2\le\frac{\mathcal E(1)}{\alpha-1}$ for $k\ge1$ .
Fact 3, p. 3. For $\alpha>3$ : $\sum_{k\ge1}k\,\theta_k\le\frac{(\alpha-1)\mathcal E(1)}{2s(\alpha-3)}$ .
(14), p. 4. $\Theta(x_{k+1})+d_k\le\Theta(x_k)+\frac{(k-1)^2}{(k+\alpha-1)^2}d_{k-1}$ for $k\ge1$ .
Fact 4, p. 4. For $\alpha>3$ : $\sum_{k\ge1}k\,d_k\le\frac{\alpha(3\alpha-5)\mathcal E(1)}{4s(\alpha-1)(\alpha-3)}$ .
Lemma 2, p. 4. For $\alpha>3$ , $\lim_k\big[k^2d_k+(k+1)^2\theta_{k+1}\big]$ exists and is finite.

Significance

The result. The $O(k^{-2})$ rate of FISTA is often quoted as optimal for first-order methods. Theorem 1 shows that for $\alpha>3$ the worst-case rate along every single run is strictly better, $o(k^{-2})$ , and that the steps $\|x_{k+1}-x_k\|$ decay faster than $1/k$ . No better power is possible: by Attouch et al., Example 2.13 there is no $p>2$ with an $O(k^{-p})$ rate for every $\Phi$ and $\Psi$ . The intermediate estimates (Facts 2–4) give explicit, quantitative bounds that are reused in the analysis of inexact and perturbed variants (Theorem 4 of the paper) and in mission II of this series, which proves weak convergence of the iterates.

Formalizing it. The result is proved on paper. As far as we know, no machine-checked proof of the $O(k^{-2})$ rate of FISTA in this Hilbert-space, extended-valued setting exists in Mathlib or on this platform, and neither does the $o(k^{-2})$ refinement. A complete development would provide reusable statements about proximal-gradient steps for functions valued in $\mathbb R\cup\{+\infty\}$ . The page also has a factor slip in Fact 4 and Lemma 2 (see Formalization scope); checking it mechanically is one of the outputs.

Difficulty

The $O(k^{-2})$ bound follows from the monotonicity of $\mathcal E$ alone. That argument cannot give $o(k^{-2})$ : it controls $k^2\theta_k$ only by the constant $\mathcal E(1)$ , and summability of $k\theta_k$ (Fact 3) gives a decay of $k^2\theta_k$ only along a subsequence, not of the whole sequence. The missing ingredient is convergence of a weighted combination of function gaps and velocities, which is Lemma 2. The bookkeeping is delicate: every step carries explicit coefficients in $k$ and $\alpha$ , and the inequalities must hold in the extended reals because $\Psi$ may be $+\infty$ at the starting point.

Formalization scope

Space and functions. $\mathcal H$ is a real inner product space that is complete. $\Psi$ takes values in EReal and satisfies the published predicate IsProperClosedConvex (never $-\infty$ , finite somewhere, lower semicontinuous, convex epigraph). $\Phi:\mathcal H\to\mathbb R$ is ConvexOn and ContDiff ℝ 1, and gradient Φ is LipschitzWith L for some L : ℝ≥0.
Step size. $0<s<1/L$ is written 0 < s and s * L < 1, so that $L=0$ is allowed (s < 1 / L would be unsatisfiable when $L=0$ ). Display (9) uses the page's $s\le1/L$ , written s * L ≤ 1.
Proximal map. It is a map P with the published predicate IsProx s Ψ P, which determines $P=\operatorname{prox}_{s\Psi}$ for proper closed convex $\Psi$ and $s>0$ .
The run. It is required to follow (2) for every $k\ge1$ , with $x_0,x_1$ arbitrary; the coefficient of $x_0$ vanishes at $k=1$ .
Extended reals. $\Theta$ , $\mathcal E$ and the function-value statements live in EReal. No value is ever converted to $\mathbb R$ with toReal, which would turn $+\infty$ into $0$ . "The limit exists" (Fact 1, Lemma 2) means convergence to a real number, because in EReal every monotone sequence converges. Infinite series of nonnegative terms are stated as bounds on every partial sum. $\min\Theta$ in the goal is ⨅ y, Θ y together with the hypothesis that a minimizer exists.
Corrected slips. Fact 2 is stated with $\mathcal E(1)$ for $k\ge1$ ; the page writes $\mathcal E(0)$ for $k\ge0$ , which needs an iterate $x_{-1}$ . Fact 4 is stated for $\sum k\,d_k$ ; the page prints $\sum k\|x_{k+1}-x_k\|^2$ with the same constant, which is off by the factor $2s$ and false in general. Lemma 2 is stated for the bracket $k^2d_k+(k+1)^2\theta_{k+1}$ of its proof (16).
Ruled out. The goal assumes nothing about $\mathcal E$ , $z_k$ , $\theta_k$ or $d_k$ . A statement of the first limit for toReal values, or with an extended-real "limit exists", would be trivially weaker and is not what is asked.
Welcome contributions. Proofs of any milestone; general facts about proximal maps of EReal-valued convex functions and about the descent property of $L$ -smooth convex functions, which are reusable well beyond this mission.

Selected references

H. Attouch, J. Peypouquet, The Rate of Convergence of Nesterov's Accelerated Forward-Backward Method is Actually Faster than $1/k^2$ , SIAM J. Optim. 26(3):1824–1834, 2016. arXiv:1510.08740v4, doi:10.1137/15M1046095
H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168:123–175, 2018. arXiv:1507.04782
A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sci. 2(1):183–202, 2009. doi:10.1137/080716542
A. Chambolle, C. Dossal, On the convergence of the iterates of the "fast iterative shrinkage/thresholding algorithm", J. Optim. Theory Appl. 166:968–982, 2015. doi:10.1007/s10957-015-0746-4
R. May, Asymptotic for a second order evolution equation with convex potential and vanishing damping term, 2015. arXiv:1509.05598
Y. Nesterov, A method of solving a convex programming problem with convergence rate $O(1/k^2)$ , Soviet Math. Dokl. 27:372–376, 1983. mathnet
W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17(153):1–43, 2016. arXiv:1503.01243

11 thms2 active usersReviewed

Bandit Algorithms Machine Learning Reinforcement Learning·Captain: mikedeng1

Reinforcement Learning: An Introduction I: The Gradient Bandit Algorithm Is Stochastic Gradient AscentTextbook

Motivation

The multi-armed bandit is the simplest setting in which a learner must trade off exploiting what it knows against exploring what it does not: one situation, $k$ actions, and a reward drawn from an unknown distribution each time an action is taken. Chapter 2 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) uses it to introduce, in the smallest possible setting, ideas that run through the rest of the book: incremental estimation with a step size, the bias introduced by the initial estimate, soft-max policies over learned preferences, and learning by following the gradient of expected reward.

The chapter ends with the gradient bandit algorithm (§2.8), which learns a numerical preference for each action instead of a value estimate. A shaded box on pp. 38–40 shows that its expected update is exactly a gradient-ascent step on the expected reward, so the algorithm is an instance of stochastic gradient ascent. The same argument, a score-function (likelihood-ratio) identity with a baseline, reappears in Chapter 13 as the REINFORCE algorithm and the policy gradient theorem. The bandit case is where the book first carries it out in full.

Setting

Actions are $1, \dots, k$ . Each action $x$ has a reward distribution $\nu_x$ on $\mathbb R$ with finite mean $q_*(x)$ , the true action value. At each step the learner holds a vector of action preferences $H = (H(1), \dots, H(k)) \in \mathbb R^k$ and selects action $A$ with the soft-max probability

\pi(a) = \frac{e^{H(a)}}{\sum_{b=1}^k e^{H(b)}} \qquad (2.11).

Given $A = x$ , a reward $R \sim \nu_x$ is received. The expected reward is $\mathbb E[R] = \sum_x \pi(x)\, q_*(x)$ , a smooth function of $H$ . With a step size $\alpha > 0$ and a baseline $B \in \mathbb R$ , the gradient bandit update (2.12) is

H'(A) = H(A) + \alpha (R - B)(1 - \pi(A)), \qquad H'(a) = H(a) - \alpha (R - B)\,\pi(a) \ \ (a \ne A).

The chapter's estimation sections use a single action's rewards $R_1, R_2, \dots$ . The sample average after $n-1$ selections is $Q_n = (R_1 + \cdots + R_{n-1})/(n-1)$ , with an arbitrary initial value $Q_1$ . A constant step size $\alpha \in (0,1]$ updates $Q_{n+1} = Q_n + \alpha [R_n - Q_n]$ (2.5). The trace of one $\bar o_0 = 0$ , $\bar o_n = \bar o_{n-1} + \alpha (1 - \bar o_{n-1})$ defines the step size $\beta_n = \alpha / \bar o_n$ (2.8)–(2.9).

Formalization targets

Goal: the expected update is the gradient step

For every action $a$ , with $A \sim \pi$ and $R \mid A = x \sim \nu_x$ ,

\mathbb E\bigl[H'(a)\bigr] = H(a) + \alpha\, \frac{\partial\, \mathbb E[R]}{\partial H(a)} ,

that is, the update (2.12) equals the exact gradient-ascent step (2.13) in expected value, for every baseline $B$ that does not depend on the selected action.

Milestones

(2.3): $Q_{n+1} = Q_n + \tfrac1n [R_n - Q_n]$ for $n \ge 1$ , including $Q_2 = R_1$ for arbitrary $Q_1$ .
(2.6): $Q_{n+1} = (1-\alpha)^n Q_1 + \sum_{i=1}^n \alpha(1-\alpha)^{n-i} R_i$ , with weights summing to one.
Exercise 2.7: with $\beta_n = \alpha/\bar o_n$ , $Q_{n+1} = \sum_{i=1}^n \frac{\alpha(1-\alpha)^{n-i}}{\bar o_n} R_i$ for $n \ge 1$ , weights summing to one, and no dependence on $Q_1$ .
Shift invariance (p. 37): adding a constant $c$ to every preference leaves $\pi$ unchanged.
Exercise 2.9: for $k = 2$ , $\pi(1) = \sigma(H(1) - H(2))$ with $\sigma(x) = 1/(1+e^{-x})$ .
Soft-max derivative (p. 40): $\partial \pi(x)/\partial H(a) = \pi(x)(\mathbb 1_{a=x} - \pi(a))$ .
Zero-sum gradient (p. 39): $\sum_x \partial \pi(x)/\partial H(a) = 0$ .
Performance gradient as an expectation (p. 39): $\partial \mathbb E[R]/\partial H(a) = \mathbb E[(R - B)(\mathbb 1_{a=A} - \pi(a))]$ .

Significance

The result. The identity makes a model-free algorithm, which uses only the sampled action and reward, an unbiased estimator of the gradient of a quantity that depends on the unknown $q_*$ . It therefore places the gradient bandit algorithm within stochastic approximation, where convergence theory for stochastic gradient methods applies. It also explains the role of the baseline: any baseline independent of the action leaves the expected update unchanged, so the choice of baseline can only affect the variance of the update, as Figure 2.5 shows empirically. The estimation milestones make precise two claims the chapter uses repeatedly: sample averages can be maintained incrementally, and constant step sizes produce an exponentially recency-weighted average biased by $Q_1$ . Exercise 2.7 removes that bias.

Formalizing it. All of these results are elementary and proved (or left as routine exercises) in the book. None of them is formalized on Prove2Me or, as far as is known, in Mathlib. What this mission adds is a machine-checked version of the book's argument with the reward model and baseline condition stated precisely, and a reusable soft-max layer (definition, partial derivatives, shift invariance) for later missions of this series, in particular the policy gradient theorem of Chapter 13.

Difficulty

The mathematics is beginning calculus, as the book says. The formal difficulty lies elsewhere. The goal is an identity between an expectation over a two-stage random experiment (an action from $\pi$ , then a reward from $\nu_A$ ) and a partial derivative in one coordinate of a vector-valued parameter. A proof has to justify exchanging the finite sum with the derivative and splitting the reward integral, and it has to use integrability of each $\nu_x$ . It also needs the fact that the baseline term vanishes because $\sum_x \partial\pi(x)/\partial H(a) = 0$ . A scalar-parameter version of the log-sum-exp derivative does not suffice: the book differentiates in one coordinate $H(a)$ while all other preferences are held fixed. For Exercise 2.7 the obvious unrolling of (2.6) does not apply directly, because the step size $\beta_n$ varies with $n$ and the book states neither the weights nor the range of $\alpha$ .

Formalization scope

Actions are Fin k. Every statement quantifies over some action, so $k \ge 1$ whenever it has content. Preferences are vectors Fin k → ℝ. The partial derivative in coordinate $a$ is the derivative of $h \mapsto f(\text{update } H\ a\ h)$ at $H(a)$ . The soft-max derivative milestone is stated with HasDerivAt, so it also asserts differentiability.
Rewards: each $\nu_x$ is a probability measure on $\mathbb R$ with Integrable identity and mean $q_*(x)$ . The expectation of a function of $(A, R)$ is $\sum_x \pi(x) \int \cdot \, d\nu_x$ . The book's normal-distribution testbed is only an example.
The baseline is a fixed real $B$ , the book's "any scalar that does not depend on" the action (pp. 39–40). The book's $B_t = \bar R_t$ , the average of past rewards, is covered once one conditions on the past. Footnote 1 on p. 37 states that the chapter's experiments used a $\bar R_t$ that also included $R_t$ . That baseline depends on $A_t$ , and the identity does not cover it.
Rewards of one action are a sequence indexed from $1$ . $Q_1$ is arbitrary, and $0^0 = 1$ as in the book (p. 33), so $\alpha = 1$ is included in (2.6).
Exercise 2.7 speaks of "a conventional constant step size $\alpha > 0$ ". The formalization takes $\alpha \in (0,1]$ , the range of the constant step size in (2.5). For $\alpha = 2$ the trace $\bar o_n$ vanishes at every even $n$ and $\beta_n$ is undefined. "Without initial bias" is read as "for $n \ge 1$ , $Q_{n+1}$ is the displayed weighted average of $R_1, \dots, R_n$ with weights summing to one", which in particular does not involve $Q_1$ .
Exercise 2.9 is read as the two equalities $\pi(1) = \sigma(H(1)-H(2))$ and $\pi(2) = \sigma(H(2)-H(1))$ .
A trivializing formalization is ruled out: the goal is about the expected value of the algorithm's update (2.12) under the joint law of action and reward, not the soft-max derivative alone and not a version in which the reward is replaced by its mean or the expectation is taken over $A$ only.
Not formalized: the UCB rule (2.10) and the 10-armed testbed, which carry no provable claim in the chapter, and the stochastic-approximation conditions (2.7), which the book cites without proof.
Welcome contributions: a general soft-max library (derivatives, Jacobian, log-sum-exp) over a finite type, reusable for Chapter 13, and proofs of the milestones in the listed order.

Selected references

R. S. Sutton, A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 2, pp. 25–46. http://incompleteideas.net/book/the-book-2nd.html
R. J. Williams, Simple statistical gradient-following algorithms for connectionist reinforcement learning, Machine Learning 8 (1992) 229–256. https://doi.org/10.1007/BF00992696
H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586

11 thms2 active usersReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources IX: Deciding Feasibility with Cumulative Resources Is NP-Complete Even for Acyclic Project NetworksTextbook

Motivation

Project scheduling with cumulative resources models production and logistics projects in which activities fill and empty storage: an activity withdraws material from an inventory when it starts and deposits its output when it completes, and every inventory must stay between a safety stock and a storage capacity. Neumann, Schwindt and Zimmermann treat this model in §2.12 of Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2) and use it in their process-industry applications.

Before any optimization, a scheduler must know whether a feasible schedule exists at all. Theorem 2.12.1 of the book answers the complexity of this question: it is NP-complete, and it stays NP-complete when the project network has no cycles. The contrast with renewable resources (machines, workers) is the point of the theorem: with renewable resources, the feasibility problem is NP-complete as well (Theorem 2.3.13, after Bartusch, Möhring and Radermacher, 1988), but an acyclic network always admits a feasible schedule when every requirement is within capacity.

The mission also collects the two other reductions the book proves in full: Proposition 2.5.4 (recognizing whether an activity lies in some minimal delaying alternative, the branching object of the book's branch-and-bound procedures, is NP-complete) and Proposition 3.4.2 (maximizing weighted start-time deviations, a resource-levelling objective, is NP-hard without any resource constraints).

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$ ; activity $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has a duration $p_i\in\mathbb N$ , with $p_0=p_{n+1}=0$ . The project network $N$ has arc set $E$ ; an arc $\langle i,j\rangle$ with integer weight $\delta_{ij}$ imposes the temporal constraint $S_j-S_i\ge\delta_{ij}$ on the start times. A schedule is a real vector $S=(S_i)_{i\in V}$ with $S_0=0$ and $S_i\ge0$ ; it is time-feasible if it meets every temporal constraint.

Cumulative resources $k\in\mathcal R^\gamma$ carry integer demands $r_{ik}$ : $r_{ik}<0$ depletes $-r_{ik}$ units at the start $S_i$ , $r_{ik}>0$ replenishes $r_{ik}$ units at the completion $S_i+p_i$ , and $r_{0k}$ is the initial stock. The inventory at time $t$ is

r_k(S,t)=\sum_{i:\ r_{ik}<0,\ S_i\le t} r_{ik}+\sum_{i:\ r_{ik}>0,\ S_i+p_i\le t} r_{ik}.

With safety stock $\underline R_k$ and storage capacity $\overline R_k$ (integers, $\underline R_k\le\sum_{i\in V}r_{ik}\le\overline R_k$ by (2.12.1)), $S$ is feasible if it is time-feasible and $\underline R_k\le r_k(S,t)\le\overline R_k$ for every $k$ and every $t\ge0$ . The decision problem of $PSc|temp|C_{\max}$ asks whether a feasible schedule exists.

For renewable resources $k\in\mathcal R$ with capacities $R_k$ and requirements $r_{ik}\in\mathbb N$ , a set $F\subseteq V$ is forbidden if $\sum_{i\in F}r_{ik}>R_k$ for some $k$ . A delaying alternative for $F$ is a set $B\subseteq F$ such that $F\setminus B$ is not forbidden; it is minimal if no proper subset of $B$ is one.

In $PS\infty|temp,\bar d|f$ there are no resources, schedules must also satisfy $S_{n+1}\le\bar d$ , and the objective here is $f(S)=-\sum_{i\in V}\sum_{j>i}w_{ij}|S_j-S_i|$ with weights $w_{ij}\ge0$ .

NP and NP-completeness are taken in the sense of Cook's Turing-machine formulation, with instances written in binary.

Formalization targets

Goal: Theorem 2.12.1

Assuming PARTITION is NP-complete,

L=\{\text{codes of instances of }PSc|temp|C_{\max}\text{ with a feasible schedule}\}\ \text{ and }\ L_{\mathrm{acyc}}=L\cap\{N\text{ acyclic}\}

are both NP-complete.

Milestones

Membership (proof of Theorem 2.12.1): $L\in\mathrm{NP}$ and $L_{\mathrm{acyc}}\in\mathrm{NP}$ .
Reduction correctness (proof of Theorem 2.12.1): for sizes $s(1),\dots,s(\nu)$ with even sum, the project with $r_0=r_{n+1}=-\sum s(i)/2$ , $r_i=s(i)$ , $\underline R=\overline R=0$ , $d^{\min}_{0,n+1}=1$ has an acyclic network, and it has a feasible schedule iff the sizes split into two parts of equal sum.
Polynomial transformation: $\mathrm{PARTITION}\le_p L_{\mathrm{acyc}}$ .
Proof of Proposition 2.5.4, one resource: for $j^*\in B\subseteq F$ , $B$ is a minimal delaying alternative iff $R-\min_{j\in B}r_j<\sum_{i\in F\setminus B}r_i\le R$ .
Proof of Proposition 2.5.4, with $r_{j^*}=1$ : a minimal delaying alternative contains $j^*$ iff some $A\subseteq F\setminus\{j^*\}$ has $\sum_{i\in A}r_i=R$ .
Proposition 2.5.4: assuming SUBSET SUM is NP-complete, deciding whether some minimal delaying alternative for a forbidden set $F$ contains $j^*\in F$ is NP-complete.
Proof of Proposition 3.4.2: a graph has a cut of at least $M$ edges iff the constructed instance has a schedule with $S_i\in\{0,1\}$ and $\sum_{i<j}w_{ij}|S_j-S_i|\ge M$ .
Proposition 3.4.2: assuming SIMPLE MAX CUT is NP-complete, the decision version of $PS\infty|temp,\bar d|-\sum\sum w_{ij}|S_j-S_i|$ is NP-hard.

The goal follows from milestones 1 and 3 together with the transfer of NP-completeness along $\le_p$ (on the platform as CookPvsNP.npComplete_of_polyReducible).

Significance

The result. Theorem 2.12.1 explains why the book's methods for cumulative resources enumerate precedence relations between depleting and replenishing activities (minimal surplus and shortage sets, Theorem 2.12.4) instead of relying on a constructive feasibility test: unless P = NP, no polynomial algorithm decides feasibility, even for acyclic networks, where the renewable-resource case is trivial. Proposition 2.5.4 does the same for the branching scheme of §2.5, and Proposition 3.4.2 places the resource-levelling objectives of Chapter 3 among the hard ones.

Formalizing it. The three results are proved in the book, as short reductions whose delicate steps are left implicit: the polynomial size of a certificate for real-valued schedules, the handling of instances outside the construction (odd sums, empty index sets, oversized items), and the passage from an optimization problem to its decision version. None of the three reductions is machine-checked anywhere known. The mission states them against a single Turing-machine model and a single binary encoding, reusing the published definitions CookPvsNP_defs, so that the reductions compose with the Cook–Levin development already on the platform.

Difficulty

The mathematical content of the reductions is short; the difficulty is in the complexity-theoretic layer. Two steps resist the obvious argument.

First, NP membership. The book's certificate is a schedule, and a schedule is a real vector: it is not a string. A verifier needs a finite certificate of polynomial length, and it is not immediate that a feasible instance has a feasible schedule with small rational (or integer) start times, since the inventory constraints involve strict orderings between event times.

Second, polynomial-time computability in a concrete Turing-machine model. The transformation must compute, on a one-tape machine, binary codes of sums and halves of the input sizes, an arc list of quadratic length, and must map malformed strings to fixed no-instances. Informal "clearly polynomial" arguments have to become explicit machine constructions or a reusable library of closure properties.

Formalization scope

The Lean development fixes the following conventions.

Activities are Fin (n + 2), with the completion Fin.last (n + 1); resources are Fin m. Start times are real.
The inventory constraints hold for every $t\ge0$ , not only for $0\le t\le\bar d$ as (2.12.2) is printed; the book's proofs use this reading.
Real activities may have duration $0$ in $PSc|temp|C_{\max}$ : the reduction of Theorem 2.12.1 uses only such activities.
Instances are coded as lists of integers written in binary over the alphabet $\{0,1,-,\#\}$ ; arc weights are listed for every ordered pair of activities together with an arc indicator. Well-formedness (standing assumptions such as $n\ge1$ , $p_0=p_{n+1}=0$ , no loops, (2.12.1), $r_{ik}\le R_k$ ) is part of each language.
"Acyclic" means the nodes admit a numbering increasing along every arc.
The NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT (Karp, 1972) enters as a hypothesis of the corresponding theorem; these are not results of the book.
Proposition 3.4.2 is stated for the decision version of the optimization problem, with natural-number weights and threshold.

A trivializing formalization is ruled out: the languages contain only codes of well-formed instances, the encoding is injective, and the hypotheses on the source problems are true theorems, so the goal cannot hold vacuously or by a degenerate encoding.

A complete development needs closure properties of polynomial-time computable functions in Cook's model (composition, binary arithmetic, list manipulation), transitivity of $\le_p$ , and a small-certificate lemma for systems of difference constraints with strict and non-strict inequalities. These are reusable for every NP-hardness proof stated in the same framework. Contributions to any of them, to the instance-level milestones 2, 4, 5 and 7, or to the NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT in this model, are welcome.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. doi:10.1007/978-3-540-24800-2
M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16, 1988.
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972. doi:10.1007/978-1-4684-2001-2_9
S. Cook, The P versus NP Problem, Clay Mathematics Institute problem description. claymath.org

14 thms2 active usersReviewed

Missions

On Conjugate Convex Functions: Conjugation Is a Symmetric Correspondence Between Lower Semicontinuous Convex FunctionsResearch Paper

Motivation

Setting

Formalization targets

Goal: Fenchel's theorem (§3, p. 75)

Milestones, in the order of the proof

Significance

Difficulty

Formalization scope

Selected references

On the Douglas–Rachford Splitting Method and the Proximal Point Algorithm for Maximal Monotone Operators: Generalized Douglas–Rachford Splitting Converges Weakly if A+B Has a Zero, Else Is UnboundedResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 7 (generalized Douglas–Rachford splitting)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time 2: The Two-Phase Shadow-Vertex Simplex Method Has Polynomial Smoothed ComplexityResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives II: The 4n/k Rate of the Averaged Iterate without Strong ConvexityResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 11)

Milestones (in attack order)

Significance

Difficulty

Formalization scope

Selected references

Twice Regularized MDPs and the Equivalence Between Robustness and Regularization 1: The Robust Value Function Is the Optimum of a Policy- and Value-Regularized Convex ProgramResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1 (general robust MDP)

Milestones

Significance

Difficulty

Formalization scope

Selected references

SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives I: Linear Convergence under Strong ConvexityResearch Paper

Motivation

Setting

Formalization targets

Goal: Corollary 1 (p. 8)

Theorem 1 (p. 7)

Supporting lemmas

Significance

Difficulty

Formalization scope

Selected references

Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time 1: The Expected Shadow of a Gaussian-Perturbed Polytope Has Polynomially Many VerticesResearch Paper

Why the shadow of a perturbed polytope matters

Setting

Formalization targets

Goal: Theorem 4.0.1 (Shadow Size)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time: Minimal Optimal Predecessor Lists Are Characterized by Strictly Increasing BreakpointsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1(a)

Milestones

Significance

Difficulty

Formalization scope

Goal: the $Jm_2+1$ bound, with correctness