Fast Integer Multiplication on Multitape Turing Machines: Schönhage–Strassen and the ToolkitResearch Paper
Motivation
Every fast integer-multiplication algorithm in the literature is stated for the multitape Turing machine. The algorithms are built from a small set of standard subroutines whose costs are usually quoted as "well known":
linear-time addition;
sorting by merging on tapes;
fast matrix transposition;
a crude O(n1+δ) multiplier, used for the small multiplications inside fixed-point arithmetic.
Harvey–van der Hoeven (2021) use all of these in §2.1, §2.3 and §4–§5 of their O(nlogn) paper. They cite Brent–Zimmermann for the arithmetic, Knuth vol. 3 for merge sort, and Bostan–Gaudry–Schost for transposition.
This mission formalizes that toolkit in the shared machine model IntMul_MultitapeModel. Its goal is the classical Schönhage–Strassen bound M(n)=O(nlognloglogn). The toolkit is exactly what is missing before the recursive step of the companion mission, Harvey–van der Hoeven Proposition 5.4, can be decomposed. Proposition 5.4 is the last open link on that mission's main line.
Timeline (multitape Turing model).
Folklore: schoolbook multiplication in O(n2); addition in O(n).
2007: Bostan–Gaudry–Schost, Appendix: transposing an m×k matrix with N bits in total in O(Nlogmin(m,k)) on a multitape machine.
2019/2021: Harvey–van der Hoeven, O(nlogn), using all of the above.
Setting
The machine model, input and output conventions, and the time-bound predicate MulTimeBound are those of IntMul_MultitapeModel. That model follows Montanaro's lecture notes:
k≥2 one-way tapes, with a read-only input tape and a separate output tape;
▹ appears only in cell 0 of each tape;
START=HALT, and the halting state freezes the configuration.
For subroutines whose input is not of the form x#y, the new definitions file IntMul_MultitapeWords starts the machine on an arbitrary word over {0,1,#}. It also provides the encodings
bits(x), a bit string written as a word;
u1#u2#⋯#um, a list of words joined by separators.
Formalization targets
Goal: Schönhage–Strassen
MulTimeBound(n↦nlnnlnlnn): a single multitape machine multiplies n-bit integers for every n≥1 in worst-case time O(nlognloglogn).
Milestones
Schoolbook multiplication: MulTimeBound(n2).
Karatsuba–Ofman: MulTimeBound(nlog23).
Linear-time addition: on input x#y with ∣x∣=∣y∣=n, output binn+1(valx+valy) within c(n+1) steps.
Merge sort on tapes:
Input:m records, each a key of ℓ bits and a payload of q bits, written as k1#p1#k2#p2#⋯.
Output: the records stably sorted by key value, in the same format.
Time:c(N+1)(⌈log2m⌉+1), where N is the input length.
Matrix transposition:
Input: an m×k matrix (m,k≥1) with entries of ℓ≥1 bits, in row-major order. Entries are separated by # and rows by ##.
Output: the transpose, in the same format.
Time:c(N+1)(⌈log2min(m,k)⌉+1).
Formalization scope
Constants may depend only on the machine. All time bounds count exact steps of one fixed machine in the shared model. Building machines by composing smaller ones (subroutine calls, scratch tapes, recursion) is the solvers' business; any reusable infrastructure for it is welcome as published lemmas.
Selected references
A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7 (1971), 281–292.
A. Karatsuba, Yu. Ofman, Multiplication of multidigit numbers on automata, Soviet Physics Doklady 7 (1963), 595–596.
D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching, 2nd ed., Addison-Wesley, 1998, §5.4.
A. Bostan, P. Gaudry, É. Schost, Linear recurrences with polynomial coefficients and application to integer factorization and Cartier–Manin operator, SIAM J. Comput. 36 (2007), 1777–1806, Appendix.
R. P. Brent, P. Zimmermann, Modern Computer Arithmetic, Cambridge University Press, 2011, Ch. 1.
D. Harvey, J. van der Hoeven, Integer multiplication in time O(nlogn), Ann. of Math. 193 (2021), §2.1.
A. Montanaro, Computational Complexity, lecture notes, §3–§4.
A Proximal Alternating Direction Method of Multiplier for Linearly Constrained Nonconvex Minimization: With Small Stepsizes the Smoothed Proximal ADMM Iterates Approach the KKT SetResearch Paper
Motivation
The alternating direction method of multipliers (ADMM) and the closely related augmented Lagrangian method are workhorses for linearly constrained optimization: they split a problem into cheap primal steps and a dual (multiplier) update, and they scale to large and distributed instances (Boyd et al., 2011). For convex objectives their convergence theory is classical (Eckstein–Bertsekas, 1992). Many applications, however, have nonconvex objectives: matrix factorization, sparse principal component analysis, and problems from signal processing and machine learning. There the simple inexact augmented Lagrangian method, which takes one projected-gradient step on the augmented Lagrangian before each multiplier update, can oscillate or diverge, and an example of this is given in §6 of the paper.
Zhang and Luo (SIAM J. Optim. 30(3), 2020) stabilize the method with a proximal term centred at an exponentially averaged copy of the primal iterates. They prove global convergence to stationary points for a smooth nonconvex objective, under linear equality constraints and box constraints, and an O(1/ε2) iteration complexity, without assuming that A has full row rank. Earlier analyses of nonconvex ADMM, for example Hong–Luo–Razaviyayn, 2016 and Boţ–Nguyen, 2020, rely on other structure, such as a smooth last block or Kurdyka–Łojasiewicz properties. This mission formalizes the convergence theorem.
Setting
Let f:Rn→R be differentiable, A∈Rm×n, b∈Rm, and let P={x∈Rn:ℓi≤xi≤ui} be a box with ℓi<ui. The problem is
xminf(x)subject toAx=b,x∈P.(1.1)
A point x is stationary if there are multipliers y∈Rm and μ,ν∈Rn with
X∗ is the set of stationary points and W the set of primal-dual pairs(x,y) for which such μ,ν exist. Strict complementarity means that for every such tuple and every i, exactly one of μi and ℓi−xi is zero and exactly one of νi and xi−ui is zero.
Assumption 2.2 asks for three things: (a) 0 lies in the relative interior of {Ax−b:x∈P}; (b) strict complementarity holds; (c) ∥∇f(x)−∇f(x′)∥≤L∥x−x′∥ on P for some L>0. A constant γ, possibly negative, satisfies ⟨∇f(x)−∇f(x′),x−x′⟩≥γ∥x−x′∥2 on P.
With constants Γ>0 and p>0, the proximal augmented Lagrangian is
K(x,z;y)=f(x)+y⊤(Ax−b)+2Γ∥Ax−b∥2+2p∥x−z∥2.
Algorithm 2.2 starts from x0,z0∈P and y0∈Rm, and for t=0,1,… sets
where [⋅]+ is the projection onto P, α>0 and 0<β≤1 are the dual and smoothing stepsizes, and 0<c<1/LK with LK=L+p+Γ∥A∥2.
Formalization targets
Goal: Theorem 2.4
Assume Assumption 2.2, p>−γ, p>0, Γ>0 and 0<c<1/LK. There is α0>0 such that for every α∈(0,α0) and every y0 there is β0>0 such that for every β∈(0,min{1,β0}], every run of Algorithm 2.2 from y0 satisfies: {yt} is bounded,
and every limit point of {(xt,yt)} lies in W. The thresholds are existential, as in the paper, which proves only that "sufficiently small" stepsizes work.
Milestones
The milestones follow the paper's proof:
weak duality (2.10);
the primal, dual and proximal descent lemmas (Lemmas 3.1–3.3);
the Lipschitz bounds of Lemma 3.5 and the primal error bounds (3.10)–(3.11);
the lower bound (3.5) on the potential ϕt=K(xt,zt;yt)−2d(yt,zt)+2M(zt);
dual boundedness (Lemma 3.4);
Lemma 3.6 and Corollaries 3.7–3.8;
the Hoffman bound (Proposition 3.9) and the local dual error bound (3.15);
Here d(y,z) and x(y,z) are the minimum value and the minimizer of K(⋅,z;y) over P, and M(z) and x∗(z) are those of f+2p∥⋅−z∥2 over the feasible set.
Companion: Theorem 4.2
Under the same hypotheses, for every run there is B>0 such that for every t>0 some (xs+1,ys+1) with s<t is a B/t-solution: ∥Ax−b∥≤ε and some v∈∇f(x)+A⊤y+∂ιP(x) has ∥v∥≤ε.
Significance
Theorem 2.4 is a global convergence guarantee for a single-loop, gradient-based primal-dual method on nonconvex problems with general linear constraints. Each iteration costs one gradient evaluation and one projection onto a box. Its hypotheses do not include full row rank of A or a Kurdyka–Łojasiewicz property, and strict complementarity is generic by Proposition 2.3 of the paper. Theorem 4.2 turns the same argument into an O(1/ε2) iteration bound, which the paper reports as an improvement over the previously best known O(1/ε3).
The result is proved on paper and has not been machine-checked. A formalization would check the three-case argument for (3.37), whose printed Case 1 leaves a step implicit (it needs dist(zt,X∗)≤Δ but derives only a bound on ∥xt+1−zt∥). It would also produce reusable components: a projected-gradient descent and error-bound library on boxes, Danskin's formula for the value of a strongly convex parametric problem, and Hoffman's bound for mixed linear systems.
Difficulty
None of the three terms K, −d and M decreases monotonically along the iteration, and the dual step can increase K by α∥Axt−b∥2. A direct Lyapunov argument on K therefore fails. The paper's potential cancels the dual increase against the dual ascent of d, but leaves a negative term pλ∥x(yt+1,zt)−x∗(zt)∥2. Controlling that term needs a dual error bound, which holds only locally (near X∗ and for small dual residual) and only under strict complementarity. Away from that region, compactness of P and the smallness of β are used instead. The constants involved (Δ, σ5, δ(⋅) from Corollaries 3.7–3.8) are not explicit, which is why the threshold for β is not explicit either. Hoffman's bound and Danskin's theorem, both used in the proof, are not in Mathlib.
Formalization scope
Vectors live in EuclideanSpace ℝ (Fin n). A is a continuous linear map, A⊤ is its adjoint, and the paper's σ (largest singular value) is the operator norm ∥A∥. The box projection is defined coordinatewise by the paper's formula (2.1). Assumption 2.2 is split into its three parts; the relative interior is Mathlib's intrinsicInterior, and "exactly one is zero" is an exclusive or. The Lipschitz bound and the constant γ hold on P only, as on the page.
The minimizers x(y,z) and x∗(z) are not built by choice. Statements take functions with the minimizer property, which exist because P is compact and are unique when p>−γ. The values d, M and the potential are computed at them. Distances are Metric.infDist, and on Rn×Rm this uses the maximum of the two Euclidean distances, an equivalent metric. A limit point is a cluster point of the sequence.
Standing assumptions of the paper that the Lean states explicitly: Γ>0, p>0, p>−γ, 0<c<1/LK, 0<β≤1, α>0. Additions relative to the page, each disclosed in the item: x∈P in (2.10), z∈P in Lemma 3.4 and in (3.15), nonemptiness of the polyhedron in Proposition 3.9, and the hypotheses of Theorem 2.4 for Theorem 4.2. The third constant of Lemma 3.5 is σ/(p+γ), as in (3.12), not the printed (p+γ)/σ. Constants that the paper writes with a division by ∥A∥ are multiplied out.
A trivializing formalization is ruled out. The stepsizes are quantified as "there is a threshold, then every smaller stepsize and every run". All six conclusions of Theorem 2.4 are stated. Its hypotheses are exactly the paper's. It does not mention the potential or the auxiliary minimizers. The sets X∗, W and Y∗(z) are nonempty under the hypotheses, so no distance to an empty set decides a statement. A sorry-free check shows that the hypotheses are jointly satisfiable, including strict complementarity, and that runs and minimizer selections exist.
Contributions welcome: proofs of the milestones in any order, general-purpose lemmas (projected-gradient error bounds, Danskin's theorem, Hoffman's bound) as separate theorems, and a repair of Case 1 of (3.37) if one is needed.
Selected references
J. Zhang and Z.-Q. Luo, A proximal alternating direction method of multiplier for linearly constrained nonconvex minimization, SIAM J. Optim. 30(3):2272–2302, 2020. https://doi.org/10.1137/19M1242276
S. Boyd, N. Parikh, E. Chu, B. Peleato and J. Eckstein, Distributed optimization and statistical learning via the alternating direction method of multipliers, Found. Trends Mach. Learn. 3(1):1–122, 2011. https://doi.org/10.1561/2200000016
J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, Math. Program. 55:293–318, 1992. https://doi.org/10.1007/BF01581204
M. Hong, Z.-Q. Luo and M. Razaviyayn, Convergence analysis of alternating direction method of multipliers for a family of nonconvex problems, SIAM J. Optim. 26(1):337–364, 2016. https://doi.org/10.1137/140990309
R. I. Boţ and D.-K. Nguyen, The proximal alternating direction method of multipliers in the nonconvex setting: convergence analysis and rates, Math. Oper. Res. 45(2):682–712, 2020. https://doi.org/10.1287/moor.2019.1008
F. Facchinei and J.-S. Pang, Finite-Dimensional Variational Inequalities and Complementarity Problems, Springer, 2003. https://doi.org/10.1007/b97543
Linear Convergence of First Order Methods for Non-Strongly Convex Optimization III: Projected Gradient Contracts dist(·, X*) at Every Feasible Point If and Only If f Has Quadratic Functional GrowthResearch Paper
Motivation
Linear convergence of first order methods is classically tied to strong convexity. Many problems in data fitting, machine learning and control are not strongly convex, yet gradient methods are observed to converge linearly on them: least squares with a rank-deficient matrix, the dual of a linearly constrained quadratic program, f(x)=g(Ax) with g strongly convex and A singular. Their optimal sets are not single points, so strong convexity fails, and some weaker property of f has to explain the observed rates.
I. Necoara, Yu. Nesterov and F. Glineur (arXiv:1504.06298v4, 2016; Math. Program. 175 (2019)) introduce a chain of relaxations of strong convexity — quasi-strong convexity, quadratic under-approximation, quadratic gradient growth, quadratic functional growth — and prove linear rates for several first order methods under each. Among these results, Theorem 13 singles out one condition: for the projected gradient method with constant step size, linear convergence (in the sense made precise below) holds if and only iff has quadratic functional growth. This mission formalizes that equivalence and the two results it rests on, Theorem 5 and Theorem 12.
Related conditions appear in Łojasiewicz's gradient inequality, in Luo and Tseng's error bounds (1993), in the Polyak–Łojasiewicz condition studied by Karimi, Nutini and Schmidt (2016), and in Drusvyatskiy and Lewis's equivalence of quadratic growth and error bounds (2018).
Setting
Work in Rn with the Euclidean inner product ⟨u,v⟩=u⊤v and norm ∥⋅∥. Problem (P) is
f∗=x∈Xminf(x),
with X⊆Rn closed and convex and f convex, with gradient Lipschitz on X with constant Lf>0:
∥∇f(x)−∇f(y)∥≤Lf∥x−y∥∀x,y∈X.(1)
The optimal setX∗={x∈X:f(x)≤f(y)∀y∈X} is assumed nonempty. The projection[u]S of u onto a nonempty closed convex set S is the nearest point of S to u. For x∈X write xˉ=[x]X∗.
The projected gradient step from x is x+=[x−Lf1∇f(x)]X, and xˉ+=[x+]X∗. The projected gradient method (GM) starts at x0∈X and iterates xk+1=[xk−αk∇f(xk)]X for k≥0.
f has quadratic functional growth with constant κf>0, written f∈FLf,κf, when
f(x)−f∗≥2κf∥x−xˉ∥2∀x∈X.(22)
The condition number is μf=κf/Lf.
Formalization targets
Goal: Theorem 13 (p. 23)
Under the standing assumptions of (P):
if f satisfies (22) with constant κf>0, then for every x∈X
∥x+−xˉ+∥2≤1+μf1∥x−xˉ∥2;
if for some 0<β<1 the step contracts the distance to the optimal set,
∥x+−xˉ+∥≤β∥x−xˉ∥∀x∈X,
then f satisfies (22) with constant Lf(1−β)2.
Together these say that a uniform one-step contraction of dist(⋅,X∗) by the gradient step with step size 1/Lf is equivalent to quadratic functional growth.
Milestones
(28): f(x+)≤f(x)−2Lf∥x+−x∥2;
(26): under the contraction hypothesis, (1−β)∥x−xˉ∥≤∥x−x+∥;
Theorem 5: contraction implies (22) with κf=Lf(1−β)2;
the one-step inequality ∥xk+1−x∥2≤∥xk−x∥2−2αk(f(xk+1)−f(x)) for 0<αk≤1/Lf and all x∈X;
(52): under (22), ∥xk+1−xˉk+1∥2≤1+κfαk1∥xk−xˉk∥2;
Theorem 12: along (GM) with αk=1/Lf, ∥xk−xˉk∥2≤(1+μf)−k∥x0−xˉ0∥2.
A companion item states the function-value rate (53), f(xk)−f∗≤2Lf∥x0−xˉ0∥2(1+μf)−(k−1) for k≥1.
Significance
The result. Theorem 13 identifies quadratic functional growth as the exact condition, in the paper's hierarchy, for linear convergence of projected gradient: every stronger class (strong, quasi-strong convexity, quadratic gradient growth, quadratic under-approximation) gives linear convergence through it, and no condition weaker than (22) can. It also gives explicit constants in both directions: rate (1+μf)−1 per step from growth, and growth constant Lf(1−β)2 from contraction factor β.
Formalizing it. The results are proved in the paper; to the knowledge of this mission none of them has a machine-checked proof. The work is to formalize the known proofs: the descent inequality (28) and the variational inequality of the projection onto a closed convex set, the one-step inequality of the projected gradient method, and the two directions of Theorem 13. The projection lemmas and the one-step inequality are reusable for any analysis of projected gradient on convex sets.
Difficulty
The ⇒ direction is a contraction argument along one step; its difficulty is the projection calculus: the variational inequality characterizing [u]X, applied with u=xk−αk∇f(xk), and the descent lemma (2), which must be derived from (1) on the convex set X only, since f need not be smooth off X. The nearest point xˉk+1 of xk+1 differs from xˉk; the argument must compare distances to two different optimal points.
The ⇐ direction is not a statement about one run of the method: it needs the contraction hypothesis at every feasible point. A version with a multi-step rate along runs (dist(xk,X∗)≤Cqk) is not what the paper proves, and the one-step hypothesis cannot be recovered from it without extra work.
Formalization scope
Lean represents Rn as EuclideanSpace ℝ (Fin n) and ∇f as gradient f. f is a function on all of Rn that is differentiable at every point of X; only its values and gradients on X enter. The standing assumptions of p. 3 are explicit hypotheses of every theorem: X closed and convex, f convex on X, (1) with Lf>0, and a named minimiser x⋆∈X∗; the paper's "simple" (cheap projection) is not a mathematical hypothesis and is dropped, and "closed" for f is implied by continuity on X. The optimal value is f(x⋆), or f(xˉ), never an infimum. Projections are predicates (IsNearest), never chosen points, and every statement quantifies over all nearest points; they exist and are unique on nonempty closed convex sets. Iterates are indexed from k=0. The page prints "for k≥1" in (GM); this slip is not copied. Theorem 12's "converges linearly to some optimal point" is formalized as the rate (51) only, since convergence of the iterates themselves is not proved on the page. In the goal, part 1 is stated in the squared form of (52).
The formalization does not define the projection by a choice function, does not allow an empty optimal set (which would make every growth inequality vacuous), and does not read the gradient off the set where f is assumed differentiable.
Needed infrastructure: the variational characterization of the Euclidean projection onto a closed convex set, the descent lemma on a convex set, closedness and convexity of X∗, and existence of nearest points. Contributions of these lemmas, of the milestones in any order, and of the goal are welcome.
Selected references
I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Math. Program. 175 (2019) 69–107. https://arxiv.org/abs/1504.06298
Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
H. Karimi, J. Nutini, M. Schmidt, Linear convergence of gradient and proximal-gradient methods under the Polyak–Łojasiewicz condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
D. Drusvyatskiy, A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Math. Oper. Res. 43 (2018) 919–948. https://arxiv.org/abs/1602.06661
Linear Convergence of First Order Methods for Non-Strongly Convex Optimization VI: Feasible Descent Methods Converge Linearly in Function Values under Quadratic Functional GrowthResearch Paper
Motivation
Many first order methods used in large-scale convex optimization do not take an exact projected gradient step. Proximal point iterations, random or cyclic coordinate descent, extragradient methods and matrix splitting methods all produce iterates that behave like a projected gradient step corrupted by an error which is small relative to the step itself. Luo and Tseng (Ann. Oper. Res. 1993) grouped these schemes under the name feasible descent methods and proved that they converge linearly when the problem satisfies an error bound, a condition relating the distance to the optimal set to the size of the projected gradient residual. Wang and Lin (JMLR 2014) gave global iteration complexity bounds for the same family under the same kind of error bound.
Necoara, Nesterov and Glineur (arXiv:1504.06298v4, published in Math. Program. 2019) study a chain of conditions weaker than strong convexity under which first order methods still converge linearly. The weakest of them that the paper uses for algorithms is quadratic functional growth: the objective grows at least quadratically in the distance to the optimal set. Their Theorem 15 shows that the whole feasible descent family converges linearly in function values under quadratic functional growth alone. This mission formalizes that theorem and the steps of its proof.
Setting
Let Rn carry the Euclidean inner product ⟨u,v⟩=u⊤v and the norm ∥u∥. For a set S and a point u, a nearest pointp=[u]S is a point p∈S with ∥u−p∥≤∥u−z∥ for every z∈S.
Problem (P) is f∗=minx∈Xf(x), where
X⊆Rn is closed and convex;
f is convex on X and differentiable at every point of X, with gradient ∇f Lipschitz on X with constant Lf>0: ∥∇f(x)−∇f(y)∥≤Lf∥x−y∥ for all x,y∈X (inequality (1) of the paper);
the optimal set X∗={x∈X:f(x)≤f(y)∀y∈X} is nonempty; f∗ is the value of f on X∗.
The function f has quadratic functional growth with constant κf>0 (Definition 4, inequality (22)) if, for every x∈X and its nearest point xˉ=[x]X∗,
f(x)−f∗≥2κf∥x−xˉ∥2.
The class FLf,κf(X) consists of the convex functions satisfying (1) and (22).
A run of the feasible descent method (FDM) with constants β,L,Lˉf>0 consists of stepsizes αk, error vectors ek and iterates xk (k≥0) with x0∈X and, for every k,
The errors are part of the run: any vectors meeting the two conditions are allowed. With αk=1/Lf, ek=0 and L=Lf a run is the projected gradient method (GM) of the paper.
Formalization targets
Goal: Theorem 15
For f∈FLf,κf(X) and every run of (FDM), for all k≥0,
The one-step contraction: f(xk+1)−f∗≤(1+4(Lf+Lˉf+βLˉf)2Lκf)−1(f(xk)−f∗).
Significance
Theorem 15 replaces the error bound assumption of Luo–Tseng and Wang–Lin by quadratic functional growth, a condition stated purely in terms of function values. Since the paper shows (Theorems 6 and 7) that, for convex f with Lipschitz gradient, the error bound and quadratic functional growth are equivalent up to constants, the theorem gives a direct route to linear convergence for every scheme known to be a feasible descent method, with an explicit rate in the three constants L, Lf, Lˉf and the error ratio β. The paper also notes (p. 30) that linear convergence of xk to a point of X∗ follows from the function-value rate and (22).
The result is proved in the paper. No machine-checked version is known to exist: the prior-art search found no formalization of feasible descent methods, of the Luo–Tseng framework, or of linear convergence under quadratic functional growth on a constrained set. A formal proof would make the general feasible descent template available for instantiation by concrete methods (coordinate descent, proximal point), each of which then needs only to verify the two run conditions.
Difficulty
The obvious argument for projected gradient methods compares xk+1 with a fixed minimizer and uses strong convexity to contract the distance; here neither is available. There is no strong convexity, X∗ need not be a singleton, and there is no upper bound on the stepsize, so the usual sufficient decrease estimate of the gradient method cannot be derived and is instead an assumption of the run. The error ek is only controlled relative to the step xk+1−xk, not absolutely, and the stepsize is only bounded below, so any estimate has to be uniform in αk and has to measure progress against the moving nearest point xˉk+1 of the optimal set rather than a fixed minimizer.
Formalization scope
The ambient space is EuclideanSpace ℝ (Fin n); f is a function on all of Rn, and only its values and gradients (Mathlib's gradient) at points of X enter. The nearest point [u]S is the predicate IsNearest S u p, never a choice function, so a run of (FDM) is any pair of sequences (xk), (ek) with stepsizes (αk) satisfying the predicate IsFDMRun. Statements about xˉk+1 hold for every nearest point; since X∗ is closed and convex the nearest point is unique. The optimal set is nonempty because a minimizer x∗ is a hypothesis, and f∗ is f(x∗), not an infimum. Sequences are indexed from 0.
Standing assumptions of p. 3 are hypotheses: X closed and convex, f convex on X, differentiable on X, (1) with Lf>0, X∗ nonempty. The word "simple" (projection is cheap) is not a mathematical condition and is dropped; closedness of f follows from continuity on X. The class hypothesis f∈FLf,κf is unbundled into convexity, (1) and (22) with κf>0. The constants satisfy β,L,Lˉf>0, as on the page, and no upper bound on αk is imposed. The milestone (65) drops every hypothesis it does not need (it uses only convexity of X), and the chain after (65) does not assume (22).
Trivializing formalizations are ruled out: the projection is not a choice that could return a junk point, X∗ is never empty, gradients are only evaluated at points of X where f is differentiable, and the run conditions are satisfiable by non-stationary sequences (for f(x)=21∥x∥2 on X=Rn, αk=21, ek=0, xk=2−kx0).
A complete development needs the variational characterization of Euclidean projections onto convex sets, the first order characterization of convexity for a function differentiable on a convex set, existence of nearest points in closed convex nonempty sets of Rn, and an induction on the one-step contraction. The first three are reusable well beyond this mission. Proofs of the milestones, and of instances of (FDM) for concrete methods, are welcome.
Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Annals of Operations Research 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
P.-W. Wang, C.-J. Lin, Iteration complexity of feasible descent methods for convex optimization, Journal of Machine Learning Research 15 (2014) 1523–1548. https://jmlr.org/papers/v15/wang14a.html
A Forward-Backward Splitting Method for Monotone Inclusions Without Cocoercivity 5: The Three-Operator Forward-Reflected-Backward Method Converges Weakly to a Zero of A + B + CResearch Paper
Three-operator monotone inclusions
Many problems in convex optimization and variational analysis have the form of a monotone inclusion with three pieces of structure: a nonsmooth part that is only accessible through its resolvent (a subdifferential of a proximable function, or a normal cone of a constraint set), a smooth convex part whose gradient is Lipschitz, and a monotone but non-gradient part such as the skew operator (z1,z2)↦(z2,−z1) of a saddle-point problem. Composite saddle-point problems minumaxvf(u)+h(u)+Φ(u,v)−g(v) with a smooth h and a bilinear coupling Φ lead to such inclusions. Splitting methods that use each piece separately, and in the way that is cheapest for it, are the standard tools for these problems.
Timeline of the relevant results:
1979: Lions and Mercier study splitting algorithms for the sum of two monotone operators, among them forward-backward splitting, which needs a cocoercive forward operator (Lions–Mercier 1979).
2000: Tseng's forward-backward-forward method removes cocoercivity for a Lipschitz monotone operator, at the cost of two forward evaluations per iteration (Tseng 2000).
2017: Davis and Yin's three-operator splitting handles A+B′+C with two resolvents and a cocoercive C (Davis–Yin 2017).
2020: Malitsky and Tam introduce the forward-reflected-backward method for A+B with B monotone and Lipschitz, and in §5 a three-operator variant for A+B+C with C cocoercive (arXiv:1808.04162v4; SIAM J. Optim. 30(2), 2020).
Setting
Let H be a real Hilbert space with inner product ⟨⋅,⋅⟩. A set-valued operatorA:H⇉H assigns to each x a subset A(x)⊆H. It is monotone if ⟨x−y,u−v⟩≥0 whenever u∈A(x), v∈A(y), and maximally monotone if moreover its graph is not properly contained in the graph of another monotone operator. For γ>0, the resolventJγA=(I+γA)−1 sends w to the unique point p with γ−1(w−p)∈A(p).
A single-valued B:H→H is monotone if ⟨x−y,B(x)−B(y)⟩≥0 and L1-Lipschitz if ∥B(x)−B(y)∥≤L1∥x−y∥. A single-valued C:H→H is L21-cocoercive (L2>0) if
L21∥C(x)−C(y)∥2≤⟨C(x)−C(y),x−y⟩∀x,y∈H.
The problem (46) is to find x∈H with 0∈(A+B+C)(x); its solution set is the zero set(A+B+C)−1(0)={x:−(B+C)(x)∈A(x)}. For a step size λ>0 and initial points x0,x−1∈H, the three-operator forward-reflected-backward scheme (47) is
xk+1=JλA(xk−2λB(xk)+λB(xk−1)−λC(xk))∀k∈N.
A sequence (xk)converges weakly to xˉ if ⟨xk,v⟩→⟨xˉ,v⟩ for every v∈H.
Formalization targets
Goal: Theorem 5.2
If A is maximally monotone, B is monotone and L1-Lipschitz, C is L21-cocoercive, (A+B+C)−1(0)=∅ and
0<λ<4L1+L22,
then every sequence generated by (47) converges weakly to a point of (A+B+C)−1(0).
Milestones
(48), proof of Lemma 5.1: the monotonicity of A at xk+1 and at a zero x, expanded into six inner-product terms.
Lower bound (proof of Theorem 5.2): the energy on the left of Lemma 5.1, with ε removed, is nonnegative.
Significance
The two-operator forward-reflected-backward method applied to A and B+C would require λ<1/(2L1+2L2), since B+C is only known to be (L1+L2)-Lipschitz. Theorem 5.2 shows that using C through a plain forward step, without reflection, enlarges the range to λ<1/(2L1+21L2). In particular, with B=0 the scheme is the forward-backward method and the range is λ<2/L2, the classical one; with C=0 it is the forward-reflected-backward method with its range λ<1/(2L1). The result therefore interpolates between the two methods, with one resolvent, one new evaluation of B and one evaluation of C per iteration.
The theorem is proved in the paper, partly by reference: the proof says it is "more or less the same as Theorem 2.5" with Lemma 5.1 in place of Lemma 2.4. No machine-checked proof of Theorem 5.2 or of the two-operator Theorem 2.5 is known to exist. A formalization makes explicit the steps the paper leaves to the reader (the Opial-type argument and the identification of weak cluster points as zeros), and the energy inequality of Lemma 5.1 is reusable for rates and inertial variants.
Difficulty
The energy inequality is a careful but elementary computation with inner products. The difficulty lies in passing from it to weak convergence. The energy is not ∥xk−x∥2 but ∥xk−x∥2 plus a cross term in B and a step-length term, so Fejér monotonicity of (xk) with respect to the zero set is not available, and the existence of lim∥xk−x∥ for each zero x is not immediate from the energy inequality. The identification of weak cluster points as zeros requires that the graph of the maximally monotone operator A+B+C be sequentially closed in the weak-strong topology, which in turn needs maximal monotonicity of a sum of a maximally monotone operator and a continuous monotone operator. A naive approach that treats B+C as a single Lipschitz operator only reaches the smaller step range and does not prove the theorem.
Formalization scope
All statements live in a real inner product space H (NormedAddCommGroup, InnerProductSpace ℝ H), with CompleteSpace H for the goal. Set-valued operators are H → Set H. The operator vocabulary (monotone, maximally monotone, Lipschitz with a real constant, cocoercive, resolvent family) is the published module ThreeOpSplitting.Accel.MonotoneOperators. Conventions:
The resolvent is a hypothesis: a family J : ℝ → H → H with IsResolventFamily A J (for each γ>0, γ−1(w−Jγw)∈A(Jγw)). For maximally monotone A it exists and is unique, so this is not an extra assumption.
Indices are shifted by one: Lean's x j is xj−1, and both initial points are arbitrary. The step size is one constant λ.
"L21-cocoercive" is IsCocoercive L₂⁻¹ C with L2>0; the Lipschitz constant satisfies L1≥0, and L1=0 is allowed.
The zero set is {x:−(B+C)(x)∈A(x)}, and weak convergence is ⟨xk,v⟩→⟨xˉ,v⟩ for all v.
The goal is not trivialized by these choices: the step range is exactly (0,2/(4L1+L2)), not the smaller two-operator range; C enters (47) through −λC(xk) only; and the conclusion is weak convergence to a point of the zero set of A+B+C, not of A+B. A sorry-free sanity file shows that all hypotheses are jointly satisfiable.
A complete development needs: demiclosedness of maximally monotone graphs, maximal monotonicity of the sum of a maximally monotone and a continuous monotone single-valued operator, and Opial's lemma for weak convergence. These are general and reusable beyond this mission, as is the weak-convergence infrastructure via inner products. Contributions of these lemmas, of proofs of the milestones, and of the goal are welcome.
Selected references
Y. Malitsky and M. K. Tam, A Forward-Backward Splitting Method for Monotone Inclusions Without Cocoercivity, SIAM J. Optim. 30(2), 2020; arXiv:1808.04162v4. https://arxiv.org/abs/1808.04162v4
H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
P.-L. Lions and B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM J. Numer. Anal. 16(6), 1979. https://doi.org/10.1137/0716071
A Forward-Backward Splitting Method for Monotone Inclusions Without Cocoercivity 2: For Strongly Monotone A the Forward-Reflected-Backward Method Converges R-Linearly to the Unique ZeroResearch Paper
Motivation
Many problems in optimization, variational inequalities and saddle-point problems reduce to a monotone inclusion: find x in a real Hilbert space H with
0∈(A+B)(x),
where A is set-valued and maximally monotone and B is single-valued and monotone. Splitting methods solve such inclusions by evaluating B directly (a forward step) and A only through its resolvent (a backward step). The classical forward-backward method needs B to be cocoercive; Tseng's forward-backward-forward method removes that requirement at the price of two evaluations of B per iteration.
Malitsky and Tam (arXiv:1808.04162, SIAM J. Optim. 30(2), 2020, doi:10.1137/18M1207260) introduced the forward-reflected-backward method, which needs only monotonicity and Lipschitz continuity of B and one evaluation of B per iteration. Their Theorem 2.5 gives weak convergence (a separate mission of this series). This mission targets their Theorem 2.9: when A is strongly monotone, the method converges at a linear rate. Linear rates under strong monotonicity are the standard benchmark against which first-order methods for monotone inclusions are compared, and they decide how the method behaves on regularized saddle-point problems in practice.
Timeline:
1979: Lions and Mercier analyse forward-backward splitting for cocoercive B.
2000: Tseng's forward-backward-forward method handles Lipschitz monotone B with two forward steps per iteration (doi:10.1137/S0363012998338806).
2015: Malitsky's projected reflected gradient method treats the variational-inequality special case A=NC (doi:10.1137/14097238X).
2018–2020: Malitsky and Tam prove weak convergence of the forward-reflected-backward method for general maximally monotone A, and R-linear convergence for strongly monotone A (Theorem 2.9).
Setting
H is a real Hilbert space with inner product ⟨⋅,⋅⟩. A set-valued operator A:H⇉H is monotone if ⟨x−y,u−v⟩≥0 whenever u∈A(x), v∈A(y); it is maximally monotone if no monotone operator has a strictly larger graph; it is m-strongly monotone if m>0 and ⟨x−y,u−v⟩≥m∥x−y∥2 for all such pairs. The resolvent of A with step γ>0 is JγA=(I+γA)−1, characterised by γ−1(w−JγAw)∈A(JγAw); for maximally monotone A it is single-valued and defined everywhere. A single-valued B:H→H is monotone if ⟨x−y,B(x)−B(y)⟩≥0 and L-Lipschitz if ∥B(x)−B(y)∥≤L∥x−y∥.
The zero set is (A+B)−1(0)={x:−B(x)∈A(x)}. Given a step λ>0 and two starting points x0,x−1∈H, the constant-step forward-reflected-backward method is
Let A be maximally monotone and m-strongly monotone, B monotone and L-Lipschitz, (A+B)−1(0)=∅, and λ∈(0,2L1). Then (A+B)−1(0)={xˉ} and there are q∈(0,1) and M with
∥xk−xˉ∥≤Mqkfor all k.
The rate q is left existential, as in the paper's phrase "converges R-linearly"; the explicit rate implied by the proof appears in the milestones.
(27): with ε=min{21−λL,5mλ}>0, (1+4mλ)ak+1+bk+1+ε∥xk+1−xk∥2≤ak+bk.
bk≥0.
With α=min{1+4mλ−43ε,1+2ε}>1: α(ak+1+bk+1)≤ak+bk.
ak+1≤ak+1+bk+1≤α−(k+1)(a0+b0).
(A+B)−1(0) has at most one point.
Significance
The result. Theorem 2.9 shows that the single-forward-evaluation method keeps the linear rate that the forward-backward method enjoys under cocoercivity, and that Tseng's method enjoys at twice the cost per iteration. The paper also notes that strong monotonicity of B instead of A reduces to this case by shifting mI from B to A, so the theorem covers strongly monotone saddle-point problems with Lipschitz couplings, for which it gives a geometric bound on the distance to the solution with an explicit contraction factor α−1/2.
Formalizing it. The theorem is proved in the paper; nothing about it is open. As far as is known it has no machine-checked proof. The mission produces a checked proof of the rate together with the constants ε and α of the paper. One step of the printed derivation, the last inequality of (28), does not hold for every step λ∈(0,2L1) (it needs (λL)2≤81). The combined inequality of milestone 4, with the paper's constant α, does hold on the whole range, and a formal proof settles this point.
Difficulty
The iteration is not a fixed-point iteration of a contraction in xk alone: xk+1 depends on xk and xk−1, and the natural Lyapunov quantity bk contains the cross term 2λ⟨B(xk)−B(xk−1),x−xk⟩, which has no sign. The obvious argument, bounding ∥xk+1−x∥ by a multiple of ∥xk−x∥, fails because the reflected term λB(xk−1) couples consecutive steps; the contraction holds only for a combined energy, and only after showing that energy is nonnegative. The constants must be balanced so that the gain 4mλ from strong monotonicity outweighs what is spent controlling the cross term, uniformly in λ up to 2L1.
Formalization scope
H is a type with [NormedAddCommGroup H] [InnerProductSpace ℝ H], plus [CompleteSpace H] in the goal. Operators are A : H → Set H and B : H → H. Monotonicity, strong monotonicity, maximal monotonicity, Lipschitz continuity and resolvents come from the published definition module ThreeOpSplitting.Accel.MonotoneOperators. Strong monotonicity sits on A, with 0<m a separate hypothesis; B is only monotone.
The resolvent is a hypothesis, not a construction: the method is driven by a family J : ℝ → H → H with J γ a resolvent of A for every γ>0. For maximally monotone A such a family exists and is unique.
Indices are shifted by one: Lean's x j is the paper's xj−1, so x 0 is x−1 and x 1 is x0. The starting points are arbitrary. The energies aSeq, bSeq follow the same shift.
L>0 is pinned, because the step range (0,2L1) divides by L.
"R-linear convergence" is stated as an explicit geometric bound ∥xk−xˉ∥≤Mqk with a fixed q∈(0,1), and uniqueness of the zero is part of the conclusion, not a hypothesis. A statement with plain norm convergence, a rate depending on k, a hypothesis that the zero is unique, or strong monotonicity on B or on A+B instead of A is not the theorem; neither is a variable-step run.
The milestones drop maximality of A and completeness of H where the step does not use them, and milestones 3 and 6 are stated with fewer hypotheses than in the proof; each is a stronger statement.
No infrastructure beyond Mathlib and the published operator module is needed. Proofs of the milestones, alternative proofs of the goal and sharper rates are all useful contributions.
P.-L. Lions, B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM J. Numer. Anal. 16(6), 1979. https://doi.org/10.1137/0716071
Y. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM J. Optim. 25(1), 2015. https://doi.org/10.1137/14097238X
Production Scheduling for Strategic Open Pit Mine Planning: A Mixed-Integer Programming Approach 2: Clique and Lifted Clique Cuts on Pairwise Incompatible Clusters Are ValidResearch Paper
Motivation
Strategic open pit mine planning decides which parts of an ore body are excavated, when, and where each block of material is sent. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research 68(5), 2020) model the problem as a mixed-integer program, the precedence-constrained production scheduling problem with clusters (PCPSP-C), generalising the formulation of Bienstock and Zuckerberg (2010). Its integer versions have large integrality gaps on production scheduling instances, so the authors derive several families of cutting planes. This mission concerns the first family, the extraction cuts of §5.1: early start cuts, diamond cuts, and clique and lifted clique cuts. They exploit only the mining capacity of each period and the precedence structure, and they are valid both under full integrality and under the partial integrality used in commercial mine planning software.
Clique inequalities for precedence-constrained knapsack problems go back to Boyd (1993); early start cuts to Gaupp (2008, doctoral dissertation, Colorado School of Mines); the diamond cuts resemble cuts of Zhu, Bard and Yu (2006) for multimode project scheduling. The paper's contribution is their extension to the multi-period clustered model and to partial integrality.
All page references are journal pages of the published Operations Research article.
Setting
An instance has finite sets B of blocks, D of destinations and C of clusters, the latter a partition of B, and periods T={1,…,T}. Block b lies in cluster c(b) and has weight qb≥0. A precedence relation b1≺b2 on blocks induces one on clusters (c1≺c2 if some block of c1 precedes some block of c2), assumed to be a strict partial order. The arc set A is its transitive reduction: (c,c′)∈A when c′ is an immediate predecessor of c. The closure is cl(c)={c}∪{c′:c′≺c}, the reverse closurercl(c)={c}∪{c′:c≺c′}, and for a set S of clusters q(S)=∑c∈S∑b∈cqb, with qc=q({c}).
Variables xc,t give the fraction of cluster c extracted in period t and yb,d,t the fraction of block b sent to destination d in period t. The constraints (2)–(7) of p. 1427 are
together with an integrality condition: full integrality (10) xc,t∈{0,1} defines the PCPSP-F, and partial integrality (11), "∑t′≤txc,t′>0 implies ∑t′≤txc′,t′=1 for (c,c′)∈A", defines the PCPSP-P. The general rows Gy≤g include the mining capacity rows (8), ∑b∑dqbyb,d,t≤Ut.
The cuts are written in the cumulative variables wc,t=∑t′=1txc,t′ (17), and with Qt=∑t′=1tUt′. Two clusters c1,c2, neither preceding the other, are f-incompatible in time t if q(cl({c1,c2}))>Qt, and p-incompatible if q(cl({c1,c2})∖{c1,c2})>Qt.
Formalization targets
Goal: Theorem 4 (clique and lifted clique cuts), p. 1433
For a set {c1,…,ck} of clusters and t∈T, the clique inequality
i=1∑kwci,t≤1(23)
is valid for the PCPSP-F if the ci are pairwise f-incompatible, and for the PCPSP-P if they are pairwise p-incompatible. If moreover c≺ci for every i, the lifted inequality ∑i=1kwci,t≤wc,t is valid under the same conditions. The goal is the conjunction of these four validity claims.
Milestones
(18)–(20), p. 1432: wc,t≤wc,t+1, wc,t≤wc′,t for (c,c′)∈A, and ∑cqcwc,t≤Qt at every feasible point satisfying (8).
(21), p. 1432: under full integrality, wc,t∈{0,1}. Its partial counterpart (22), "wc,t>0 implies wc′,t=1 for (c,c′)∈A", is condition (11) verbatim in this formalization, which writes (11) in cumulative form, so it has no item of its own.
Theorem 2 (early start cuts), p. 1432: if q(cl(c))>Qt, then wc,t=0 is valid for the PCPSP-F, and if qc>0, wc,t≤(Qt−q(cl(c)∖{c}))+/qc is valid for the PCPSP-P.
Theorem 3 (diamond cuts), p. 1433: for t1≤t2 and c1≺c2, wc2,t2≤wc1,t1 is valid for the PCPSP-F if q(cl(c2)∩rcl(c1))>Qt1,t2=∑t′=t1t2Ut′, and for the PCPSP-P if q((cl(c2)∩rcl(c1))∖{c1,c2})>Qt1,t2.
Significance
Each of these inequalities cuts off fractional points of the linear relaxation while keeping every integer (or partially integer) schedule, and early start cuts can fix variables to zero before the solve. The paper motivates them by the large integrality gaps it observes on production scheduling instances (§5, p. 1432) and evaluates them, with its production cuts, in the computational study of §8. Because they use only the precedence order and the mining capacity, the extraction cuts apply to any multi-period precedence-constrained knapsack structure, beyond mining.
The results are proved in the paper, by short contradiction arguments. None of them has a machine-checked proof. Formalizing them yields a reusable model of the PCPSP-C with its two integrality regimes, and a checked account of exactly which rows of the formulation each cut relies on: in particular that validity needs the capacity rows (8) and the integrality condition, and fails for the LP relaxation.
Difficulty
The arguments rely on facts the paper uses in one line. Under partial integrality, wc,t>0 forces wc′,t=1 for every predecessor c′ of c, not only for the immediate ones of A; this requires chaining condition (11) along covering arcs of a finite strict order, and showing that every precedence is a chain of immediate ones. The counting step needs x≥0, which is not a constraint of the formulation but follows from xc(b),t=∑dyb,d,t, y≥0 and the nonemptiness of clusters. The diamond cut further splits the capacity Qt1,t2 between periods and uses monotonicity of w in time. A natural first attempt, arguing directly from the closure of ≺, does not apply: the formulation constrains only the arcs of A.
Formalization scope
Blocks, destinations and clusters are finite types; periods are Fin T, index t standing for period t+1. An instance carries the block-to-cluster map, the block precedence, values, discount rate, weights, capacities and m side rows Gy≤g. Cluster precedence is derived from block precedence; A is its covering relation, and constraints (4) and (11) range over A only. The closure of a pair, which the page does not define, is cl(c1)∪cl(c2). Incompatibility includes incomparability of the two clusters, as on the page; "pairwise" ranges over distinct members of a finite set, which may be empty or a singleton.
The standing assumptions of §2.1 are hypotheses of every statement: clusters cover B (so each is nonempty), ≺ is a strict partial order on clusters, r>0, and qb≥0. A cut "valid for the PCPSP-F (PCPSP-P)" is stated as: at every point feasible for the formulation with full (partial) integrality whose mining capacity rows (8) hold, the inequality holds. The capacity rows enter as an explicit hypothesis because the paper assumes they are among the rows of Gy≤g; without them every cut is false. Validity is never asserted for the LP relaxation, where the cuts do not hold, so the integrality condition cannot be dropped. In Theorem 2 the division by qc is guarded by qc>0, as on the page.
The development needs only finite sums, finite sets and orders from Mathlib. Contributions are welcome on the chaining lemma for covering relations of finite strict orders and on the nonnegativity and monotonicity of w, which every milestone shares.
Selected references
O. Rivera Letelier, D. Espinoza, M. Goycoolea, E. Moreno, G. Muñoz, Production Scheduling for Strategic Open Pit Mine Planning: A Mixed-Integer Programming Approach, Operations Research 68(5):1425–1444, 2020. https://doi.org/10.1287/opre.2019.1965
D. Bienstock, M. Zuckerberg, Solving LP Relaxations of Large-Scale Precedence Constrained Problems, Proc. 14th Conf. Integer Programming and Combinatorial Optimization (IPCO), 2010, pp. 1–14.
E. A. Boyd, Polyhedral results for the precedence-constrained knapsack problem, Discrete Applied Mathematics 41(3):185–201, 1993.
G. Zhu, J. F. Bard, G. Yu, A Branch-and-Cut Procedure for the Multimode Resource-Constrained Project-Scheduling Problem, INFORMS Journal on Computing 18(3):377–390, 2006.
A Forward-Backward Splitting Method for Monotone Inclusions Without Cocoercivity 4: The Relaxed Inertial Forward-Reflected-Backward Method Converges Weakly to a Zero of A + BResearch Paper
Motivation
Many problems in optimization, game theory and partial differential equations reduce to a monotone inclusion: find x in a real Hilbert space H with 0∈(A+B)(x), where A is a maximally monotone set-valued operator with an easily computed resolvent and B is a single-valued monotone operator. Saddle-point problems, variational inequalities and composite convex minimization are all of this form. Splitting methods solve such inclusions by evaluating B forward and A backward (through its resolvent), never inverting A+B.
The classical forward-backward method requires B to be cocoercive, which excludes the skew operators arising from saddle-point problems. Tseng's forward-backward-forward method (2000) removed that assumption at the price of a second evaluation of B per iteration. Malitsky and Tam (arXiv:1808.04162, SIAM J. Optim. 2020) introduced the forward-reflected-backward method, which needs only monotonicity and Lipschitz continuity of B and evaluates B once per iteration. Its §4, the subject of this mission, adds inertia (extrapolation along xk−xk−1) and relaxation (averaging with the previous iterate). Inertial and relaxed variants are used in practice to accelerate convergence and to enlarge the range of admissible step sizes; the inertial proximal point algorithm goes back to Alvarez and Attouch (2001).
Setting
Let H be a real Hilbert space. A set-valued operator A:H⇉H is monotone if ⟨x−y,u−v⟩≥0 whenever u∈A(x), v∈A(y), and maximally monotone if its graph is not properly contained in the graph of another monotone operator. Its resolvent with step γ>0 is JγA=(I+γA)−1, a single-valued map on all of H when A is maximally monotone. A map B:H→H is L-Lipschitz if ∥B(x)−B(y)∥≤L∥x−y∥ and L1-cocoercive if L1∥B(x)−B(y)∥2≤⟨B(x)−B(y),x−y⟩ for all x,y. The zero set is (A+B)−1(0)={x:−B(x)∈A(x)}.
Given parameters α≥0, β,λ>0 and starting points x0,x−1∈H, the relaxed inertial forward-reflected-backward scheme (34) is
With B′=B−λαI it is equivalently (35), in which the inertial term is absorbed into B′. The case α=0, β=1 is the forward-reflected-backward method; β=1 alone gives the inertial method (45).
Formalization targets
Goal: Theorem 4.3
If A is maximally monotone, B monotone, (A+B)−1(0)=∅, α∈[0,1), β∈(0,1], λ>0, and either (a) B is L-Lipschitz and
λ<min{2L2−β−αβ−2α,βL1−α−αβ},
or (b) B is L1-cocoercive, α<2+β2−β and
λ<min{2L2−β−αβ+2α,βL1−α+αβ},
then the sequence (xk) of (34) converges weakly to a point of (A+B)−1(0).
Milestones
Lemma 4.1: B−ρI is (L+ρ)-Lipschitz if B is L-Lipschitz, and (L−ρ)- or ρ-Lipschitz if B is L1-cocoercive and ρ≤L/2 or ρ>L/2.
(37): the resolvent inequality of Proposition 2.3 in the form used in §4.
Lemma 4.2: the energy inequality for (35), with bk=2λ⟨B(x)−B(xk),x−xk⟩≥0.
(40): the sharper energy inequality with (1−β)bk, from the proof of Lemma 4.2.
(43): the step-size conditions give ε=min{22−β(1+α),β1−α}−λL′>0.
The telescoped bound βε∥xk+1−x∥2+ε∑i=1k∥xi+1−xi∥2≤C0, with C0 depending only on x0,x−1.
(xk) is bounded and ∥xk−xk+1∥→0.
A companion item states Corollary 4.4, the case β=1, where the conditions become α<31 with λ<2L1−3α (Lipschitz) or λ<2L1+α (cocoercive).
Significance
Theorem 4.3 gives an explicit region of (α,β,λL) for which a single-evaluation, inertial, relaxed splitting method converges for monotone Lipschitz B, with no cocoercivity. In the cocoercive case it shows that inertia enlarges the admissible step size beyond that of the plain method (Corollary 4.4(b) allows λL<21+α); in the Lipschitz case it quantifies the opposite effect. With B=0 it recovers the convergence of the inertial proximal point algorithm by an argument different from the classical one.
The theorem is proved in the paper; to our knowledge none of §4 has been machine-checked. The mission produces a formal proof of Theorem 4.3 and of the Lyapunov inequalities behind it. The proof in the paper ends with "the remainder of the proof follows a similar argument to Theorem 2.5"; making that remainder explicit, in particular the convergence of the energy terms bk, which rests on the factor 1−β in (40) rather than on Lemma 4.2 as printed, is part of the work.
Difficulty
The natural energy ∥xk−x∥2 is not monotone along the iteration: both the reflected term B(xk)−B(xk−1) and the inertial term xk−xk−1 make it increase at some steps, and the standard Fejér argument for forward-backward methods does not apply. The energy that does decrease couples three consecutive iterates through ⟨B′(xk+1)−B′(xk),x−xk+1⟩ and the residual bk, and this cross term has no sign. Showing that the energy controls ∥xk+1−x∥2 from below, and that the step-size conditions (41) and (42) make all the coefficients positive, is where the specific constants come from. Passing from boundedness to weak convergence then needs an Opial-type argument and the demiclosedness of the graph of the maximally monotone operator A+B, in an infinite-dimensional space where bounded sequences only have weakly convergent subsequences.
Formalization scope
The Lean development works in a real inner product space H, complete for the goal and the corollary; the intermediate inequalities need neither completeness nor maximality of A and assume only monotonicity. Operator notions come from the published module ThreeOpSplitting.Accel.MonotoneOperators; "L1-cocoercive" is IsCocoercive L⁻¹ B. The resolvent is supplied as a family J : ℝ → H → H with the hypothesis that J γ is the resolvent of γA for every γ>0; for maximally monotone A such a family exists and is unique, so this loses nothing. Sequences are shifted by one index: Lean's x j is xj−1 and z j is zj−1; the values z 0, z 1 are never used. Weak convergence is ⟨xk,v⟩→⟨xˉ,v⟩ for all v, not norm convergence.
Committed conventions: L>0 is assumed (the step-size bounds divide by L); B is assumed monotone in both cases, as printed; the constants of (41), (42), (43) and Lemma 4.2 are copied exactly. The resolvent hypothesis is not vacuous (the identity is a resolvent family of A≡{0}), the step-size range is not shrunk, and the conclusion is weak convergence to a zero, not a weaker boundedness or cluster-point statement.
A complete development needs: the Lyapunov inequalities (milestones 2–6), Opial's lemma for sequential weak cluster points, weak sequential compactness of bounded sets in a Hilbert space, and weak–strong closedness of the graph of a maximally monotone operator. The last three are reusable well beyond this mission and contributions of them are welcome.
Selected references
Y. Malitsky, M. K. Tam, A Forward-Backward Splitting Method for Monotone Inclusions Without Cocoercivity, SIAM J. Optim. 30(2), 2020. arXiv:1808.04162, doi:10.1137/18M1207260
P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38(2), 2000. doi:10.1137/S0363012998338806
F. Alvarez, H. Attouch, An inertial proximal method for maximal monotone operators via discretization of a nonlinear oscillator with damping, Set-Valued Anal. 9, 2001. doi:10.1023/A:1011253113155
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. doi:10.1007/978-3-319-48311-5
Algorithms for Online Matching, Assortment, and Pricing with Tight Weight-Dependent Competitive Ratios III: No Online Algorithm Earns More Than F(𝒫) Times the Expected Offline OptimumResearch Paper
Motivation
A firm sells several products, each in limited supply. Customers arrive one at a time, and each product can be offered at one of a few prices. This is the setting of airline fare classes, hotel rate plans and e-commerce discounting. Because future demand is unknown, the firm must decide online whether to sell a unit now at a low price or keep it for a customer who may pay more later. The competitive ratio measures how much an online policy loses against an omniscient benchmark in the worst case.
Ma and Simchi-Levi (arXiv:1905.04770; Oper. Res. 2020, doi:10.1287/opre.2019.1957) give online algorithms whose competitive ratio depends on the price set 𝒫 of each item through a number F(𝒫), and prove that this dependence is the best possible. This mission formalizes the second half, the impossibility result: no online algorithm can beat F(𝒫).
Timeline of the single-price precursors:
Karp, Vazirani and Vazirani (1990) introduced the upper-triangular random-permutation instance and showed that 1 − 1/e is optimal for online bipartite matching.
Ma and Simchi-Levi (2019, preprint v1) add phases of customers who pay different prices. With the phase lengths chosen adversarially, the bound becomes F(𝒫).
Setting
A setup has n items. Each item has starting inventory k ∈ ℕ, k ≥ 1, and the same price set 𝒫 = {r⁽¹⁾ < … < r⁽ᵐ⁾}, with r⁽¹⁾ > 0 and r⁽⁰⁾ := 0.
An arrival sequence 𝒜 has T customers. For each customer t, item i and price j it gives a purchase probability p⁽ʲ⁾{t,i}. It is deterministic if every p⁽ʲ⁾{t,i} is 0 or 1.
When customer t arrives, an online algorithm offers at most one in-stock item at one price. It decides using only the setup, the past, and the present customer's probabilities. A deterministic customer buys exactly when p⁽ʲ⁾_{t,i} = 1. A sale earns r⁽ʲ⁾ and uses one unit. ALG(𝒮, 𝒜) is the total revenue. A randomized online algorithm picks a deterministic one at random, ω ↦ alg(ω) with ω ~ μ.
The benchmark OPT(𝒮, 𝒜) is the value of the linear program (5):
The booking limits α⁽¹⁾, …, α⁽ᵐ⁾ of Proposition 1 are the unique positive numbers summing to 1 with
1−e−α(1)=1−r(j−1)/r(j)1−e−α(j),j=2,…,m.(7)
The tight ratio is F(𝒫) = 1 − e^{−α⁽¹⁾}. For a single price F(𝒫) = 1 − 1/e. As r⁽ᵐ⁾/r⁽¹⁾ → ∞, F(𝒫) decreases.
Formalization targets
Goal: Theorem 3 (p. 17), in ε-form
For every k ≥ 1, every price set 𝒫 and every ε > 0, there are a setup with all items of inventory k and price set 𝒫 and a finite distribution over deterministic arrival sequences, with 𝔼[OPT] > 0, such that every (measurable) randomized online algorithm satisfies
EAE[ALG(S,A)]≤(1−e−α(1)+ε)EA[OPT(S,A)].
The statement only asserts that such an instance exists; it does not fix the paper's construction.
Milestones
The instance of §5 has n items and nk customers in n groups of k. The groups are ordered by a uniformly random permutation π: group g wants items π_g, …, π_n. The groups are split into m phases; phase j pays up to r⁽ʲ⁾ and contains a fraction β_j = B_j − B_{j+1} of the groups. The milestones are:
(35): r⁽ʲ⁻¹⁾/r⁽ʲ⁾ ≤ e^{−α⁽ʲ⁾};
Proposition 4: the system B_j r⁽ʲ⁾ e^{−α⁽ʲ⁾} = r⁽¹⁾e^{−α⁽¹⁾} has a unique solution with 0 < B_m < … < B₁ = 1;
(25): on the instance, OPT = Σⱼ (r⁽ʲ⁾ − r⁽ʲ⁻¹⁾)Bⱼnk up to rounding;
Lemma 5: the maximum of the concave program (27) is (28);
(29): (28) at j = 1, τ = 1 equals F(𝒫) times (25);
Lemma 4: the expected revenue of any online algorithm is at most the maximum of (26), up to εnk for large n.
Significance
The theorem shows that the guarantees of the paper's online algorithms cannot be improved. Theorem 2 of the paper (Multi-price Ranking is F(𝒫)-competitive in the deterministic case) and Corollary 1 (Multi-price Balance tends to F(𝒫) as inventories grow) meet this bound, by Yao's minimax principle. So F(𝒫) is the exact competitive ratio for each price set. Without the theorem, the algorithms' ratios would only be lower bounds. The paper also shows (Proposition 2) that F(𝒫) exceeds the ratios of earlier approaches, so the tight value has practical bite.
The result is proved in the paper, with proofs in §5 and Appendix D, but not machine-checked. The formalization adds three things. First, an explicit treatment of rounding, which the paper sets aside as negligible for large n. Second, a corrected Lemma 5, which as printed is false for small τ. Third, a reusable model of online algorithms with deterministic arrivals and their randomized mixtures, and of the random-permutation instance.
Difficulty
The bound must hold for every online algorithm, including adaptive and randomized ones. An algorithm's decision can depend on everything it has seen, and the instance is averaged over n! permutations. So computing the best online algorithm's revenue directly is hopeless. The single-price instances of earlier work do not suffice either. On them all reasonable algorithms perform alike, whereas here the adversary's phase lengths must leave exactly one optimal way to ration inventory across phases. The upper bound on online revenue holds only asymptotically: the paper approximates harmonic sums by logarithms as n → ∞ and ignores the rounding of phase lengths. That is why the goal is in ε-form. Finally, the concave program that evaluates the bound has a closed-form optimum only when the candidate maximizer is nonnegative; Lemma 5 as printed omits this condition.
Formalization scope
Lean conventions:
Items and customers are 0-based (Fin n, Fin T); prices are 1-based functions ℕ → ℝ with r⁽⁰⁾ = 0 via price.
The booking limits α and the phase sizes B are hypotheses (IsBookingLimits, IsPhaseB), not chosen functions; Propositions 1 and 4 make them unique.
OPT is the real supremum of the LP's objective, a true maximum because the feasible set is nonempty and bounded.
A deterministic online algorithm is a rule taking the rows of customers 0, …, t to an optional (item, price) offer. It never sees later customers, or T. In the deterministic case this is the paper's information set.
A randomized algorithm is alg : Ω → OnlineAlg n on any probability space. Its expected revenue is a Bochner integral, with measurability in ω assumed; without that the integral could be 0 and the bound trivial.
The instance's phase borders are ⌊(1 − B_j)n⌋ and customer t is in group ⌊t/k⌋.
Disclosed departures from the page:
The goal and Lemma 4 carry an ε, as their proofs require.
The goal assumes 𝔼[OPT] > 0, because an empty arrival sequence would otherwise satisfy it trivially.
Lemma 5 assumes every candidate λ_ℓ = α⁽ℓ⁾ − (A_j − τ)/(m − j + 1) is nonnegative; the paper's one use (j = 1, τ = 1) satisfies this.
(25) is stated with an explicit rounding error of at most k(r⁽ᵐ⁾ − r⁽¹⁾).
The quantifier order is part of the theorem: the instance and distribution are fixed before the algorithm. A statement in which each algorithm gets its own hard instance is weaker and is not this theorem.
Needed infrastructure: finite sums over permutations, measure-theoretic expectation over the algorithm's randomness, harmonic-sum asymptotics, and one-dimensional concave maximization. The definitions of online algorithms and of the random-permutation instance are reusable for other Karp–Vazirani–Vazirani-type lower bounds. Contributions are welcome on any milestone. (35), Proposition 4 and (29) are elementary; (25) needs LP weak duality on the instance; Lemma 4 is the main work.
N. Golrezaei, H. Nazerzadeh, P. Rusmevichientong, Real-time optimization of personalized assortments, Management Science 60(6), 2014. https://doi.org/10.1287/mnsc.2014.1939
Distributed Stochastic Gradient Tracking Methods II: With Stepsizes θ/(m+k), DSGT's Mean-Square Error Is at Most 2θ²σ²/(n(θμ−1)(m+k)) Plus Higher-Order TermsResearch Paper
Motivation
Many learning and estimation problems are solved by a group of computing agents that each hold part of the data and can talk only to their neighbours in a communication network. Each agent i has a private cost fi, and the group wants a minimizer of the average f=n1∑ifi without a central coordinator. In machine learning the agents usually cannot evaluate exact gradients either; they draw noisy stochastic gradients from samples, as in stochastic gradient descent (SGD).
Pu and Nedić (Math. Program. 187 (2021) 409–457) study distributed stochastic gradient tracking (DSGT), where each agent keeps an auxiliary variable that tracks the network-average gradient. With deterministic gradients, gradient tracking achieves linear convergence under a constant stepsize (Nedić, Olshevsky and Shi 2017; Qu and Li 2018). The question for the stochastic setting is whether a network of n agents, each with noisy gradients, matches centralized SGD that averages n samples per step. This mission is the second of two on the paper: it covers the diminishing stepsize αk=θ/(m+k) and Theorem 2, which gives an O(1/k) rate whose leading constant does not depend on the network.
Setting
There are n agents and a decision space Rp with p≥1. Agent i has a differentiable cost fi:Rp→R that is μ-strongly convex with L-Lipschitz gradient (Assumption 2); x∗ denotes the minimizer of f=n1∑ifi. A query of agent i at a point x returns gi(x,ξi), where ξi∈Rd is a random sample. The samples ξi,k (agent i, iteration k) are mutually independent, and for every fixed x
(Assumption 1). Agents communicate through a nonnegative coupling matrixW=[wij] that is doubly stochastic, has some positive diagonal entry, and whose positive off-diagonal entries form a connected undirected graph (Assumptions 3–4). Write ρw for the spectral norm of W−n111⊤; it is below 1 (Lemma 1).
Stack the local variables as x=[x1,…,xn]⊤∈Rn×p, let xˉ=n1∑ixi, and use the Frobenius norm, so that ∥x−1xˉ∥2=∑i∥xi−xˉ∥2 is the consensus error. DSGT (4) starts from an arbitrary deterministic x0 and yi,0=gi(xi,0,ξi,0), and iterates
Let θ>1/μ and let m satisfy condition (14) of the paper: m exceeds 2θ(μ+L) and 1−ρw24θLρw2+2θLρw1+3ρw2, and a second explicit inequality in θ,m,μ,L,ρw and ∥W−I∥ holds. Then there are constants C1,C2,C3, independent of k, such that for all k≥0
The constants may depend on every datum of the run (network, costs, noise law, starting point, θ, m), but not on k.
Milestones
(29)–(30), p. 425. The mean-square errors Uk=E∥xˉk−x∗∥2, Xk=E∥xk−1xˉk∥2, Yk=E∥yk−1yˉk∥2 satisfy a componentwise linear system Vk+1≤AkVk+bk with an explicit 3×3 matrix Ak.
(31), p. 425. The positivity of βk, used in Ak, reduces to an explicit lower bound on m.
(32)–(36), pp. 425–427. By induction, Uk≤U^/(m+k), Xk≤X^/(m+k)2 and Yk is bounded, with explicit U^ and X^.
p. 427. The refined recursion Uk+1≤(1−αkμ)Uk+μn2αkL2Xk+nαk2σ2.
p. 427. Product bounds ∏t=0k−1(1−m+tθμ)≤mθμ/(m+k)θμ and their tail versions.
p. 427. Sum–integral bounds for ∑t<k(m+t)θμ−3 and ∑t<k(m+t)θμ−2.
Significance
The leading term 2θ2σ2/(n(θμ−1)(m+k)) involves neither ρw nor the graph: after a transient, the network-average iterate behaves like centralized SGD run on n samples per step, and the error decreases as 1/n with the number of agents (Remark 3 of the paper). The consensus error decays one order faster, as 1/k2. The result is a reference point for later analyses of stochastic gradient tracking, which refine the transient time and the dependence on the network.
The theorem is proved in the paper; to the best of current knowledge no part of it is machine-checked. A complete development formalizes the stacked stochastic model, the conditional-expectation estimates behind the linear system, the induction with tuned constants, and the elementary analytic bounds. Two steps of the printed proof need extra care (see Formalization scope), and repairing them is part of the work.
Difficulty
The estimate for the tracker error Yk couples all three quantities: bounding Yk+1 requires Uk and Xk, and Xk+1 requires Yk. A direct estimate of any single error therefore does not close, and the rate for Uk cannot be read off from a scalar recursion until Xk=O(1/k2) is known. The induction closes only for the constants of the paper and under condition (14), which must be checked to hold for all k at once. The probabilistic estimates need independence of the samples across agents and times, since the variance bound σ2/n for the averaged noise uses that the agents' noises are uncorrelated. Finally, the products and sums of real powers (m+t)θμ−2 must be bounded uniformly in k, including the regimes θμ<2 and θμ>2.
Formalization scope
Points of Rp are EuclideanSpace ℝ (Fin p); stacked variables are functions Fin n → E p, and every matrix norm ∥x∥ is the Frobenius sum ∑i∥xi∥2, never the sup norm of the product type. ∥W−I∥ is the Frobenius norm and ρw the operator norm of Matrix.toEuclideanCLM applied to W−n111⊤. The noise space is Rd (the paper's Rm; m is the stepsize offset). Expectations are Bochner integrals, and every bounded expectation comes with an integrability conjunct, so a non-integrable error cannot satisfy a bound by having integral 0. Powers with real exponents are Real.rpow.
Standing assumptions and additions, all stated in the items:
Assumptions 1–4 hold in every run statement; the paper's Theorem 2 cites only Assumptions 1 and 2, but ρw<1 rests on Assumptions 3–4.
Assumption 1's "each random vector is independent" is read as mutual independence of all ξi,k; its conditional moments given a deterministic x become unconditional moments for each fixed x. The oracle gi is jointly measurable.
p≥1, and ρw>0 (condition (14) and C divide by ρw2).
The linear system (29) and the induction carry 3αkL≤1 (respectively 3θL≤m), which the derivation of Lemma 4 (20) uses on p. 445 without stating it. The sum bound for ∑(m+t)θμ−3 carries θμ=2. The goal carries neither: its constants absorb a finite transient.
The constants C1,C2,C3 of the goal are quantified after all data and before k; a statement with the constants chosen after k would be trivially true and is not this theorem. The goal mentions only the iterates, x∗, θ, m and the constants of the page, not the auxiliary quantities of the proof.
Contributions welcome: proofs of the analytic milestones (products, sums), the conditional-expectation estimates behind (29), and the repair of the two gaps of the printed proof. The model definitions are shared with the companion mission on constant stepsizes.
A. Nedić, A. Olshevsky and W. Shi, Achieving geometric convergence for distributed optimization over time-varying graphs, SIAM Journal on Optimization 27 (2017) 2597–2633. https://doi.org/10.1137/16M1084316
G. Qu and N. Li, Harnessing smoothness to accelerate distributed optimization, IEEE Transactions on Control of Network Systems 5 (2018) 1245–1260. https://doi.org/10.1109/TCNS.2017.2698261
A. Nemirovski, A. Juditsky, G. Lan and A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19 (2009) 1574–1609. https://doi.org/10.1137/070704277
Multistage Distributionally Robust Mixed-Integer Programming with Decision-Dependent Moment-Based Ambiguity Sets III: Under Slater, the Delage–Ye-Type Stage Bellman Equation Is One SDP MinimizationResearch Paper
Motivation
In many multistage decision problems the probability law of the next uncertainty depends on the decision taken now: opening a facility changes the demand it attracts, a price changes the distribution of sales, maintenance changes failure rates. Distributionally robust optimization (DRO) handles an imperfectly known law by optimizing against the worst distribution in an ambiguity set. When that set itself moves with the decision, the model is decision-dependent, and the classical reformulations, which treat the ambiguity set as fixed, do not apply directly.
X. Yu and S. Shen (arXiv:2002.12518v3, 2020; Math. Program., DOI 10.1007/s10107-020-01580-4) study multistage mixed-integer DRO with binary state variables and decision-dependent moment-based ambiguity sets over a finite support. Their Theorems 1–3 turn each stage's min–max Bellman equation into a single minimization, which is the input to a stochastic dual dynamic integer programming (SDDiP) algorithm. This mission covers their main result, Theorem 3, for the most general of their three sets: a Delage–Ye-type set in which the mean lies in an ellipsoid around a decision-dependent estimate and the centred second-moment matrix is bounded by a decision-dependent matrix.
Timeline. Delage and Ye (Oper. Res., 2010, DOI 10.1287/opre.1090.0741) introduced the ellipsoid-plus-second-moment set for a decision-independent law and gave a semidefinite reformulation. Luo and Mehrotra (Optim. Lett., 2020) derived duality-based reformulations for decision-dependent moment sets in a single stage. Yu and Shen (2020) carry these into the multistage mixed-integer setting with binary states.
Setting
Fix one stage t. The data are:
a stage feasible set S⊆{0,1}I×RI×J of pairs (x,y) (state and stage variable) and a stage cost g(x,y);
a finite support ξ1,…,ξK∈RJ of the next-stage random vector (the same for every decision);
next-stage values Qk(x)=Qt+1(x,ξk);
a decision-dependent mean estimate μ(x)∈RJ, a matrix Σ(x)∈RJ×J (written Sig in Lean), and size parameters γ,η∈R.
For weights p∈RK write Mk(x)=(ξk−μ(x))(ξk−μ(x))⊤ and ξˉ(p)=∑kpkξk. The Type 3 ambiguity set (14) is
Assume that for every feasible (x,y)∈S, Σ(x)≻0, and that Slater's condition holds: some probability vector p satisfies the ellipsoid constraint strictly and ∑kpkMk(x)≺ηΣ(x). Then the minimum of the Bellman equation exists exactly when the minimum of the mixed-integer semidefinite program (15) exists, and the two are equal:
subject to s−2z2⊤ξk+Mk(x)∙Y≥Qk(x) for all k, Z=(z1z2⊤z2z3)⪰0, Y⪰0, and (x,y)∈S.
Milestones (proof of Theorem 3, pp. 37–39)
The ellipsoid constraint (C-20d) is equivalent to (Σ(x)(τ−μ(x))⊤τ−μ(x)γ)⪰0.
The Lagrangian identity (C-21).
The dual function: maximizing the Lagrangian over p≥0, τ∈RJ gives the stated objective under the stated constraints, and +∞ otherwise.
Weak duality: every p∈PD3(x) is bounded by every dual-feasible objective value.
Strong duality (C-22) under Slater, with both sides attained.
A companion statement from §4.2.2 (p. 15) is also included: the cones DD(U) built from diagonally dominant matrices consist of positive semidefinite matrices.
Significance
The result. Theorem 3 replaces a min–max problem, whose inner maximum ranges over a set that moves with x, by one minimization in which x enters only through the data μ(x), Σ(x). With affine μ, Σ and binary x, the bilinear terms can then be linearized, giving the mixed-integer SDP (16)–(17) to which the paper applies SDDiP-type cutting planes. Without the reformulation there is no single-level stage problem to generate cuts from.
Formalizing it. The result is proved on paper; it has no machine-checked proof that we know of. The proof in the paper is brief: it cites convexity and Slater for strong duality and does not check that the domain p≥0, the Schur-complement rewrite and the strict inequalities fit the conic duality theorem it relies on. A formal proof checks these points, and the per-stage duality lemmas (milestones 4 and 5) can be reused by any moment-based DRO model over a finite support.
Difficulty
Weak duality and the regrouping of the Lagrangian are routine. The difficulty is strong duality with dual attainment (milestone 5): the inner problem has an inverse-matrix constraint and a semidefinite constraint, and the duality theorem must be applied to the conic form after the Schur rewrite, with a Slater point of that form. The paper states Slater for "a vector p". A Slater point with negative entries does not lie in the domain p≥0, so it gives no interior point there. Passing from per-state duality to the equality of the two outer minima also needs care: the Bellman minimum is over pairs at which the inner maximum is attained, and the reformulated minimum is a joint minimization over (x,y) and the dual variables.
Formalization scope
Indices are 0-based (Fin I, Fin J, Fin K). States are Fin I → ℝ, the support is ξ : Fin K → Fin J → ℝ, and Σ, Z, Y are Mathlib matrices. ⪰ and ≻ are PosSemidef/PosDef of the difference (both include symmetry). The block Z is indexed by Fin J ⊕ Unit, with the same z2 in both off-diagonal blocks.
Minima and maxima are IsLeast/IsGreatest on sets of values, so attainment is part of every claim. The goal reads: for all q, q is the least stage value iff q is the least value of (15).
Added hypotheses, disclosed:Σ(x)≻0 at feasible x (implicit on the page, which writes Σ(x)−1; Mathlib's inverse of a singular matrix is 0). p≥0 in the ambiguity set ((C-20f); Assumption 3 calls p a probability). The Slater point is a probability vector (Theorem A.3 says "a probability measure").
Dropped hypotheses, disclosed generalization: linearity of g and compactness and polyhedrality of S are not used. μ and Σ are arbitrary functions of x; the affine form (12) is imposed only later in the paper. Qk is an arbitrary real function, because the stage theorem uses nothing about the recursion. Binary states are kept as a hypothesis.
Printed text not copied: the Slater clause of Theorem 3 is cut at the right margin of p. 12 and is restored from Theorem B.6 (p. 36). "u∈Rd" on p. 38 is read as u∈RJ.
No trivializing reading: the strict inequalities of Slater are kept, since non-strict ones would make the theorem false. No sSup/sInf values are used, so there are no junk values. An empty S makes both sides empty, so the equivalence carries no content there. A sorry-free check confirms that the hypotheses are satisfiable on a two-point instance with value 3.
Needed infrastructure: Schur complements for positive definite blocks (in Mathlib), the trace inequality for products of PSD matrices, and a conic strong-duality theorem with dual attainment under Slater for semidefinite constraints. Contributions of the last as a reusable lemma are welcome.
Selected references
X. Yu, S. Shen, Multistage distributionally robust mixed-integer programming with decision-dependent moment-based ambiguity sets, arXiv:2002.12518v3, 2020; Math. Program., 2020. https://arxiv.org/abs/2002.12518
E. Delage, Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Oper. Res. 58(3), 2010. https://doi.org/10.1287/opre.1090.0741
F. Luo, S. Mehrotra, Distributionally robust optimization with decision dependent ambiguity sets, Optimization Letters, 2020, pp. 1–30 (as cited by Yu & Shen).
A. A. Ahmadi, G. Hall, Sum of squares basis pursuit with linear and second order cone programming, Algebraic and Geometric Methods in Discrete Mathematics, Contemp. Math. 685, 27–53, 2017 (as cited by Yu & Shen).
Algorithms for Online Matching, Assortment, and Pricing with Tight Weight-Dependent Competitive Ratios I: Multi-price Balance Is minᵢ F̃ᵢ-Competitive, F̃ᵢ Bounded via F(𝒫ᵢ), G(𝒫ᵢ)/2 and kᵢResearch Paper
Firms that can also choose a price for each sale face a different problem. Selling an item cheaply now uses inventory that a later customer might have paid more for. Ma and Simchi-Levi (2020) study this setting. Each item can be offered at one of finitely many prices, and the attainable competitive ratio depends on those prices. Their Multi-price Balance algorithm attains, as inventories grow, a ratio that their Theorem 3 shows no online algorithm can beat. This mission formalizes their Theorem 1, the guarantee of Multi-price Balance for finite inventories.
Setting
A firm sells items i from a finite set. Item i starts with ki≥1 units and has a price setPi of mi≥1 prices 0<ri(1)<⋯<ri(mi), with ri(0):=0. Customers t=1,…,T arrive one by one. On arrival of customer t the firm learns pt,i(j)∈[0,1], the probability that t buys item i at price j. It offers at most one item, at one price. The customer accepts with that probability, and a sale earns ri(j) and uses one unit. An online algorithm decides using only the setup, the past, and the present customer's probabilities.
An algorithm is c-competitive on a setup if E[ALG]≥c⋅OPT for every arrival sequence (6).
For a price set P, the booking limitsα(1),…,α(m) are the unique positive numbers summing to 1 with
1−e−α(1)=1−r(j−1)/r(j)1−e−α(j)(j=2,…,m),
and the values σ(j) are the unique positive numbers summing to 1 with σ(1)=σ(j)/(1−r(j−1)/r(j)) (Proposition 1). Write F(P)=1−e−α(1) and G(P)=σ(1), and L(j)=α(1)+⋯+α(j).
Multi-price Balance (Algorithm 1) gives each item random segment borders 0=L~i(0)≤⋯≤L~i(mi)=1 in {0,1/ki,…,1} and a nondecreasing value functionΦ~i on that grid with Φ~i(0)=0. Both are drawn from a randomized procedure, independently across items. With Ni units of item i sold, customer t is offered a pair (i,j) maximizing
pt,i(j)(Φ~i(L~i(j))−Φ~i(Ni/ki))
when this maximum is positive. Two procedures are used. Definition 3 draws one uniform seed W and rounds every L(j)k up or down with it, then sets Φ~ by formula (20). The procedure (45), for k=1, draws configuration d with probability σ(d) and sets Φ~(1)=r(d)/σ(1).
Formalization targets
Goal: Theorem 1 (p. 16)
Give each item a mode. A perturbed item uses Definition 3. A split item is replaced by ki single-unit copies, each using (45). With
bi=(1+ki)(e1/ki−1)F(Pi)(i),bi=2G(Pi)(ii, split),bi=(1+ki)(1−e−1/ki)1−1/e(iii, if ∣Pi∣=1),
Multi-price Balance with those modes satisfies, for every arrival sequence, every tie-breaking rule and every feasible x of (5),
(iminbi)t,i,j∑pt,i(j)ri(j)xt,i(j)≤E[ALG].
Milestones
Weak duality for (5) and its dual (19) (p. 19).
Theorem 4 (p. 19). If every item's procedure satisfies
then Algorithm 1 is c-competitive.
3. Proposition 3 (p. 21). E[L~(j)]=L(j), and ∣(L~(j)−L~(j′))−(L(j)−L(j′))∣≤1/k.
4. (35) (p. 39). r(j−1)/r(j)≤e−α(j).
5. Theorem 5 (p. 22). Definition 3 satisfies (17)–(18) with c=F(P)/((1+k)(e1/k−1)), and with c=F(P)/((1+k)(1−e−1/k)) when m=1.
6. (45) (p. 44). For k=1, the procedure (45) satisfies (17)–(18) with c=σ(1)/2.
Significance
For a single price, bound (iii) improves the dependence on ki of the guarantee of Golrezaei et al. (2014). For several prices, bound (i) tends to F(Pi) as ki→∞ (Corollary 1). Mission III of this series formalizes Theorem 3, by which no online algorithm beats F(P), so Theorem 1 makes that ratio tight. Bound (ii) uses a different procedure and gives a guarantee for small inventories that does not rely on perturbing the ideal value function. The paper's Section 6 applies the same framework to the Adwords problem and to assortment problems with multiple prices.
The paper's proofs are in its Appendix B: Theorem 4 by a randomized primal–dual argument, Proposition 3 and Theorem 5 by analysis of the comonotone rounding, (45) by solving a small system, and Theorem 1 by assembling them. None of these results has a machine-checked proof. A complete formalization would yield a reusable, checked primal–dual framework for randomized online allocation: Theorem 4 holds for any family of procedures satisfying (17)–(18).
Difficulty
The primal–dual proof of Theorem 4 sets the dual variables yi=E[Φ~i(NT,i/ki)] and zt=E[Zt], where Zt is the pseudorevenue. These are expectations over both the initialization and the purchase decisions, and the dual constraint holds only after conditioning on the history and taking expectations. A deterministic value function does not suffice for multiple prices with finite inventory, since the borders L(j)ki are generally not integers. This is why the value functions are random. Rounding each border independently would break the segment-length control. Theorem 5 needs the comonotone bound (22), and an induction over segments with careful bookkeeping of the rounding errors.
Formalization scope
Indices. Items form an arbitrary nonempty finite type. Customers are indexed 0,…,T−1. Prices are 1-based with r(0)=0. Probabilities pt,i(j)∈[0,1], ki≥1, mi≥1 and 0<ri(1)<⋯<ri(mi) are hypotheses.
Booking limits.α and σ enter as functions satisfying the defining systems (7) and (8) with positivity and unit sum. By Proposition 1 they are the paper's values.
Unit indices. Borders are stored as kL~(j)∈{0,…,k} and value functions as N↦Φ~(N/k). In (17) the range of N is N<kL~(j).
The algorithm. The offer at customer t is computed from that customer's probabilities and the sales counts. The count in (16) is read as min(Ni,ki), which equals Ni because the algorithm never sells a stocked-out item. Ties are broken by an arbitrary rule returning a maximizer, and every statement holds for every such rule.
Expectations. Expected revenue is a finite sum over configurations, weighted by product probabilities, combined with a backward recursion over accept/reject outcomes. Definition 3's configuration probabilities are Lebesgue measures of seed sets.
Competitive ratio. The ratio is always stated as c⋅(5a)(x)≤E[ALG] for every feasible x of the original LP (5). This rules out the trivializations through x/0=0 when OPT=0, through an infimum over arrival sequences, and through a benchmark taken on the split setup instead of the original one.
F~i is not used. The printed theorem is phrased through F~i, the optimum of the problem (44). The proof never shows that this optimum is attained. Its bound (ii) also comes from splitting the item, not from a procedure feasible for (44). The goal is therefore stated with explicit bounds and modes; choosing the better mode per item gives the printed minimax{…}.
Not posed. Corollaries 1–2 and the optimality and uniqueness claims about (45).
Weak duality is shared with mission II and (35) with mission III; each mission defines its own copy of the model. Contributions welcome: proofs of the milestones, and of the goal from them.
A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and generalized online matching, Journal of the ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321
N. Golrezaei, H. Nazerzadeh, P. Rusmevichientong, Real-time optimization of personalized assortments, Management Science 60(6), 2014. https://doi.org/10.1287/mnsc.2014.1939
Linear Convergence of First Order Methods for Non-Strongly Convex Optimization II: Quadratic Functional Growth with Constant κ Gives the Global Error Bound with Constant κ/(1 + μ + √(1 + μ))Research Paper
Motivation
First order methods (projected gradient, fast gradient) converge only sublinearly on general smooth convex problems, at rates O(1/k) and O(1/k2) in function value. Linear convergence is classically proved under strong convexity, which fails for many problems arising in practice: least squares with a rank-deficient matrix, dual problems of linearly constrained programs, and compositions f(x)=g(Ax) of a strongly convex g with a singular linear map. For such problems the optimal set is not a single point, yet projected gradient methods are still observed to converge linearly.
Necoara, Nesterov and Glineur (arXiv:1504.06298, later Math. Program. 175 (2019)) introduce a hierarchy of relaxations of strong convexity, each obtained by evaluating a strong convexity inequality only at the projection of a point onto the optimal set, and show that first order methods converge linearly on each class. Two of these relaxations are the subject of this mission: quadratic functional growth and the global error bound stated with the gradient mapping. Error bounds of this kind go back to Luo and Tseng (Ann. Oper. Res. 46 (1993)) and Tseng's analysis of feasible descent methods; quadratic growth conditions appear in Anitescu and in Drusvyatskiy–Lewis (Math. Oper. Res. 43 (2018)).
Setting
Work in Rn with the Euclidean inner product ⟨u,v⟩=u⊤v and norm ∥⋅∥. Problem (P) is
f∗=x∈Xminf(x),
with X⊆Rn closed and convex and f convex on X, differentiable on X, with Lipschitz continuous gradient of constant Lf>0 on X: ∥∇f(x)−∇f(y)∥≤Lf∥x−y∥ for all x,y∈X. The optimal setX∗={x∈X:f(x)≤f(y)∀y∈X} is assumed nonempty.
For a set S and a point u, [u]S denotes a point of S nearest to u; for nonempty closed convex S it exists and is unique. Write xˉ=[x]X∗. The projected gradient step from x∈X is x+=[x−Lf1∇f(x)]X, and the gradient mapping is
g(x)=Lf(x−x+).
When X=Rn, g(x)=∇f(x).
f has quadratic functional growth (22) with constant κf>0 if f(x)−f∗≥2κf∥x−xˉ∥2 for all x∈X.
f satisfies the global error bound (31) with constant κf>0 if ∥g(x)∥≥κf∥x−xˉ∥ for all x∈X.
The condition number is μf=κf/Lf. In Lean these are QuadFunGrowth X f κ and ErrorBound X f Lf κ, with g(x) written Lf • (x - xp).
Formalization targets
Goal: Theorem 7
Quadratic functional growth with constant κf implies the global error bound with constant 1+μf+1+μf1⋅κf:
∥g(x)∥≥1+μf+1+μfκf∥x−xˉ∥∀x∈X.
In class notation, FLf,κf(X)⊆ELf,κf/(1+μf+1+μf)(X).
Milestones
The decrease (28) of a projected gradient step: f(x+)≤f(x)−2Lf∥x+−x∥2.
The gradient mapping inequality (29): f(y)≥f(x+)+⟨g(x),y−x⟩+2Lf1∥g(x)∥2 for y∈X.
The first chain of the proof of Theorem 7: with xˉ+=[x+]X∗, ⟨g(x),x+−xˉ+⟩+2Lf1∥g(x)∥2≥f(x+)−f∗≥2κf∥x+−xˉ+∥2.
The error bound at x+: ∥g(x)∥≥(Lf(κf+Lf)−Lf)∥x+−xˉ+∥.
Companion: Theorem 6
The converse direction, also included as a draft theorem: the error bound with κf implies quadratic functional growth with constant μf⋅κf.
Significance
Theorems 6 and 7 together show that, for convex functions with Lipschitz gradient on a closed convex set, quadratic functional growth and the gradient-mapping error bound define the same class of functions up to a change of constant depending only on μf. A linear convergence proof for projected gradient methods under one condition therefore transfers to the other, and the paper uses this to place the error-bound class E inside its hierarchy of relaxations of strong convexity. The explicit constant matters downstream: rates of the form (1−cμf)k inherit it.
The results are proved in the paper. No machine-checked proof of Theorems 6–7 is known to exist. Related statements formalized elsewhere on the platform concern the unconstrained case (Karimi–Nutini–Schmidt, where ∇f replaces g) or the proximal-gradient error bound on sublevel sets (Drusvyatskiy–Lewis), with different constants. A complete development here yields a reusable library of projected-gradient facts on a general closed convex set: the descent inequality, the gradient-mapping inequality and the existence and characterization of projections.
Difficulty
The obvious approach applies (22) at x and tries to bound f(x)−f∗ by ∥g(x)∥∥x−xˉ∥, as in the unconstrained case where g=∇f and convexity gives f(x)−f∗≤⟨∇f(x),x−xˉ⟩. On a constrained set this fails: g(x) is not a subgradient of f at x, and the available inequality for the gradient mapping, (29), controls f only through the value f(x+) at a different point. Relating the distance to X∗ at that point to the distance at x, without losing the exact constant κf/(1+μf+1+μf), is the central difficulty.
At the Lean level, the descent inequality (2) has to be derived on a convex set from a Lipschitz condition assumed only on X, and the variational characterization of the Euclidean projection has to be connected to the nearest-point predicate.
Formalization scope
Rn is EuclideanSpace ℝ (Fin n). f is a real function on all of Rn, convex on X (ConvexOn ℝ X f), differentiable at every point of X, with ∇f = gradient f; its values off X never enter.
Standing assumptions of p. 3 as hypotheses: X closed and convex; (1) on X with 0<Lf; a named optimal point x⋆∈X∗, so X∗ is never empty. The paper's "simple" (cheap projection) is not a mathematical assumption and is dropped; "closed convex function" adds nothing for a real-valued convex function continuous on X. X∗ closed and f∗ finite follow and are not assumed.
Projections are predicates (IsNearest), not choice functions; x+ is the predicate IsPGStep. Every statement quantifies over all points satisfying them. Nearest points in nonempty closed convex sets exist, so these quantifiers are not vacuous.
f∗ is written f(xˉ) for xˉ∈X∗, never as an infimum.
The constant of Theorem 7 is written κ/(1+κ/Lf+1+κ/Lf), of Theorem 6 κ/Lf⋅κ. κf≤Lf is not assumed.
(29) is stated for x∈X rather than x∈Rn, since ∇f is only meaningful on X under the standing assumptions.
A trivializing formalization is ruled out: the error bound uses the gradient mapping g(x) and not ∇f(x), the projections are not defined by choice, X∗ is nonempty, and no junk gradient value off the differentiability set is used.
Needed infrastructure: the descent lemma on a convex set, the obtuse-angle characterization of the projection onto a closed convex set, existence of nearest points (Mathlib's exists_norm_eq_iInf_of_complete_convex), and closedness and convexity of X∗. These are reusable well beyond this mission; proofs of the milestones and of Theorem 6 are welcome independently.
Selected references
I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Math. Program. 175 (2019) 69–107. https://arxiv.org/abs/1504.06298
Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
D. Drusvyatskiy, A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Math. Oper. Res. 43 (2018) 919–948. https://doi.org/10.1287/moor.2017.0889
H. Karimi, J. Nutini, M. Schmidt, Linear convergence of gradient and proximal-gradient methods under the Polyak–Łojasiewicz condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
Linear Convergence of First Order Methods for Non-Strongly Convex Optimization VII: g(Ax) with g Strongly Convex and Smooth Is Quasi-Strongly Convex on a Polyhedron with κ = σ_g/θ²(A, C)Research Paper
Motivation
Linear convergence of gradient-type methods is classically proved under strong convexity. Many problems that arise in practice are not strongly convex: dual formulations of linearly constrained convex problems, least-squares and logistic-type regression with rank-deficient data matrices, convex quadratic programs, and routing problems in data networks all have objectives of the form f(x)=g(Ax), where g is strongly convex and smooth but the matrix A has a nontrivial kernel. Such an f is constant along kerA, so it is not strongly convex, and its set of minimizers need not be a single point.
Necoara, Nesterov and Glineur (arXiv:1504.06298v4, published in Math. Program. 175 (2019)) introduce a chain of relaxations of strong convexity: quasi-strong convexity, quadratic gradient growth and quadratic functional growth. They show that projected and fast gradient methods still converge linearly under them. Section 4 of the paper supplies the main examples: compositions g(Ax), possibly with a linear term and polyhedral constraints. This mission formalizes those examples. The tool behind them is the error bound of Hoffman (1952) for systems of linear inequalities; its use for linear convergence goes back to Luo and Tseng (1993) and Wang and Lin (2014).
Setting
Work in Rn with the Euclidean inner product ⟨u,v⟩=uTv and norm ∥⋅∥. For a set X and a function f, the optimal set is X∗={x∈X:f(x)≤f(y)∀y∈X} and f∗ is the optimal value. A nearest pointxˉ=[x]S of a set S to x is a point of S minimizing ∥x−z∥ over z∈S.
The data are:
a linear map A:Rn→Rm, A=0, with operator (spectral) norm ∥A∥;
a polyhedral feasible set X={x:Cx≤d}, with C:Rn→Rp linear and the inequality read componentwise;
a differentiable function g:Rm→R that is σg-strongly convex, g(αu+(1−α)v)≤αg(u)+(1−α)g(v)−2σgα(1−α)∥u−v∥2, and whose gradient is Lg-Lipschitz.
The objective is f(x)=g(Ax), or f(x)=g(Ax)+cTx in the extensions. The function f has Lipschitz gradient with constant Lf on X if ∥∇f(x)−∇f(y)∥≤Lf∥x−y∥ for x,y∈X. It is quasi-strongly convex with constant κ if, for every x∈X and xˉ=[x]X∗,
f∗≥f(x)+⟨∇f(x),xˉ−x⟩+2κ∥x−xˉ∥2.
The class qSLf,κf(X) collects the convex functions with Lf-Lipschitz gradient on X satisfying this inequality with κf. The classes GLf,κf (quadratic gradient growth, ⟨∇f(x)−∇f(xˉ),x−xˉ⟩≥κ∥x−xˉ∥2) and FLf,κf (quadratic functional growth, f(x)−f∗≥2κ∥x−xˉ∥2) are defined the same way.
A Hoffman constantθ(A,C)>0 for the polyhedron P={z:Az=t,Cz≤d} is a number with
∥x−xˉ∥≤θ(A,C)∥Ax−t∥2+∥[Cx−d]+∥2∀x∈Rn,xˉ=[x]P,
where [v]+ is the componentwise positive part.
Formalization targets
Goal: Theorem 8
If x∗ is optimal for minx∈Xg(Ax) and θ(A,C)>0 is a Hoffman constant for {z:Az=Ax∗,Cz≤d}, then
f=g∘A∈qSLf,κf(X),Lf=Lg∥A∥2,κf=θ2(A,C)σg.
Milestones
∥∇f(x)−∇f(y)∥≤Lg∥A∥2∥x−y∥ on X.
(39): Ax∗ and ∇f(x∗) are the same for every x∗∈X∗.
X∗={x:Ax=Ax∗,Cx≤d}.
For feasible x, ∥x−xˉ∥≤θ(A,C)∥Ax−Axˉ∥.
Companions
Theorem 9: without constraints, g(Ax)+cTx∈GLg∥A∥2,σg/θ2(A,0)(Rn).
Theorem 10: on X={Cx≤d} and for every M>0, g(Ax)+cTx∈FLf,κf(XM) on the sublevel set XM={x∈X:f(x)−f∗≤M}, with κf=σg/(θ2(A,c,C)(1+Mσg+2cg2)) and cg=∥∇g(Ax∗)∥.
Example 1:21x12+x2 on R+2 has no global quadratic growth constant, but κf(M)=min{1,1/M} works on {f≤M} for M≥1.
Significance
Theorem 8 makes the linear convergence results of the paper apply to the whole family g(Ax) over polyhedra. That family covers the duals of linearly constrained strongly convex problems and regression with arbitrary design matrices. The rate is explicit in σg, Lg, ∥A∥ and the Hoffman constant. Theorems 9 and 10 extend the picture to a linear term, at the cost of moving to weaker classes. Example 1 shows that the sublevel restriction in Theorem 10 is needed.
All of these results are proved in the paper. None of them has a machine-checked proof that this mission is aware of. A formal development would produce a Lean proof of the class membership, a formal chain-rule computation of the gradient of g∘A, and the strict-convexity argument that A is constant on the optimal set. These pieces are reusable wherever a composite objective with a rank-deficient linear map appears.
Difficulty
The obvious route, strong convexity of f, fails as soon as kerA={0}. Two separate facts have to replace it. The first is that the minimizers of a strongly convex function composed with A share the image point Ax∗, so the optimal set is itself a polyhedron. The second is that the distance to that polyhedron is controlled linearly by the residual ∥Ax−Ax∗∥ on feasible points, which is exactly a Hoffman error bound. Neither follows from local information at a single minimizer. In Theorem 10 the linear term destroys the first fact's simplicity: the value cTx must also be controlled, and that is possible only on bounded sublevel sets.
Formalization scope
Rn is EuclideanSpace ℝ (Fin n). A and C are continuous linear maps, so ∥A∥ is the operator norm, which is the spectral norm of the page; it is never the Frobenius norm. Strong convexity is Mathlib's StrongConvexOn Set.univ σg g, which is (5) on all of Rm. The page's "Lg-Lipschitz gradient on X" is read on Rm, the domain of g. The gradient of the composition is always gradient (fun z => g (A z)), and the identity ∇f(x)=AT∇g(Ax) is a proof step, not part of any statement. f∗ is the value at a nearest point of X∗, which is exact because that point is optimal.
Standing assumptions of p. 3: the feasible set is closed and convex (automatic for a polyhedron), the optimal set is nonempty (a named optimal point x∗ is a hypothesis), and f has Lipschitz gradient (a conclusion here). The "simple" set and "closed" function add no mathematical content and are dropped. The Hoffman constant is a hypothesis, because the page cites its existence (Hoffman 1952) rather than proving it. The hypothesis is the Hoffman inequality for the specific polyhedron {Az=Ax∗,Cz≤d}, not for every right-hand side.
Trivializing formalizations are ruled out. The projection is a predicate (IsNearest), never a choice function. The optimal set is nonempty by hypothesis. g is differentiable everywhere, so no gradient takes a junk value. A sorry-free sanity file shows that the hypotheses of Theorems 8–10 are jointly satisfiable (A=id on R1, g=∥⋅∥2/2, θ=1).
A complete development needs the chain rule for gradients through a continuous linear map and its adjoint, first-order characterizations of strong convexity, and optimality conditions for convex differentiable functions on convex sets. Contributions of these as reusable lemmas are welcome, as are proofs of the companion theorems.
Selected references
I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Math. Program. 175 (2019) 69–107. https://arxiv.org/abs/1504.06298
A. J. Hoffman, On approximate solutions of systems of linear inequalities, J. Res. Nat. Bur. Standards 49 (1952) 263–265. https://doi.org/10.6028/jres.049.027
Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
P.-W. Wang, C.-J. Lin, Iteration complexity of feasible descent methods for convex optimization, J. Mach. Learn. Res. 15 (2014) 1523–1548. https://jmlr.org/papers/v15/wang14a.html
Production Scheduling for Strategic Open Pit Mine Planning: A Mixed-Integer Programming Approach 1: Under G, g ≥ 0 Every Minimal Optimal Schedule Stays inside the Ultimate Pit LimitResearch Paper
Motivation
Strategic planning of an open pit mine decides, over a horizon of 20 to 50 years, which parts of an ore body are excavated, when, and where the excavated material is sent. A deposit is discretized into blocks, often millions of them, and the decisions are constrained by wall-slope precedences between blocks, by mining and processing capacities, and by blending and other operational rules. The resulting mixed-integer programs are far beyond the reach of general-purpose solvers, so practitioners and researchers rely heavily on preprocessing: rules that provably remove variables before the model is solved.
The oldest such rule is the ultimate pit limit. Lerchs and Grossmann (1965) showed that the most profitable pit, ignoring time and capacities, is a maximum-weight closure of the precedence graph and can be computed by a graph algorithm. Caccetta and Hill (2003) used this limit to eliminate blocks in the capacitated pit problem (C-PIT), where each block has a predefined destination. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research, 2020) extend that result to the general precedence-constrained production scheduling problem with clusters (PCPSP-C) of Bienstock and Zuckerberg (2009): multiple destinations per block, clusters of blocks extracted together, arbitrary nonnegative side constraints, and either full or partial integrality. This mission formalizes that extension, Theorem 1 of the article, together with the surrounding claims of §2 and §4. The source is the published Operations Research article; all page numbers are journal pages.
Setting
A PCPSP-C instance consists of a finite set of blocks B, destinations D, and periods T={1,…,T}. Sending block b to destination d is worth pb,d (possibly negative); in period t it is worth pb,d,t=pb,d/(1+r)t for a discount rate r>0. A relation b1≺b2 means that b1 must be extracted no later than b2. The blocks are partitioned into clustersC, with c(b) the cluster of b; clusters inherit precedence (c1≺c2 if some block of c1 precedes some block of c2), this relation is assumed to be a partial order, and A is the set of immediate precedences: (c,c′)∈A when c′ immediately precedes c. Blocks have weights qb≥0, and a matrix inequality Gy≤g collects all side constraints (capacities and others).
The variables are xc,t, the fraction of cluster c extracted in period t, and yb,d,t, the fraction of block b sent to d in period t. The PCPSP-C maximizes ∑b,d,tpb,d,tyb,d,t subject to
and to an integrality condition: full (xc,t∈{0,1}) or partial (once a cluster has started, each of its immediate predecessors must be completely extracted). An optimal solution is minimal if no other optimal solution lies componentwise below it.
With pˉc=∑b∈cmaxdpb,d, the ultimate pit limit problem U-PIT is the linear program
maxc∈C∑pˉcxcs.t.xc≤xc′((c,c′)∈A),xc∈[0,1].
The pit limit of a vector x∈[0,1]C is {c:xc>0}; for a PCPSP-C solution it is the pit limit of xc1=∑txc,t.
Formalization targets
Goal: Theorem 1 (p. 1431)
If G≥0 and g≥0, then for either integrality condition, every minimal optimal solution (x∗,y∗) of the PCPSP-C and the minimal optimal solution xU of U-PIT satisfy
POPT={c:t∑xc,t∗>0}⊆PU-PIT={c:xcU>0}.
Milestones
Nested pits (§2.2, p. 1428). For a feasible x, the sets B(x;t)={b:∑t′≤txc(b),t′>0} are pits and increase with t.
x1 is U-PIT feasible (§4.1, p. 1431).
Uniqueness of the minimal optimum of U-PIT (§4.1, claim (b), p. 1431). This is what makes "the" pit limit PU-PIT well defined.
Existence of an optimum (§2.1, p. 1427) under either integrality condition, whenever the problem is feasible.
Dominated triplet elimination (§4.2, p. 1431). If (b,d1,t) uses no more of every resource than (b,d2,t) and is worth at least as much, some optimal solution has yb,d2,t=0.
Significance
Theorem 1 turns an expensive mixed-integer program into a smaller one using a single maximum-closure computation that ignores time and resources: every cluster outside PU-PIT can be deleted from the instance. In the article's computational study this preprocessing is part of the pipeline that solves industrial instances to near-optimality. The result covers the partial-integrality models used in commercial mine-planning software, not only the full-integrality model of the earlier literature.
The article's proof of Theorem 1 is in an online e-companion; the companion claims of §2 and §4 are stated in the text with brief or cited justifications (claim (b) is attributed to the maximum closure literature, Hochbaum 2008). None of these results has a machine-checked proof. The mission produces a formal model of the PCPSP-C that the sibling missions of this series (clique, variable-right-hand-side and hourglass cuts) share, and a verified justification of a preprocessing step in practical use.
Difficulty
The obvious argument, "a cluster outside the ultimate pit has nonpositive value, so drop it", fails on two counts. First, value is not additive over clusters: U-PIT optimality only says that the clusters outside PU-PIT that can be added to it as a closed set have nonpositive total value, not that each cluster outside it does. Second, the PCPSP-C is a multi-period problem in which a cluster may be extracted in fractions over several periods with different discount factors, and with side constraints that may forbid extracting it at all. The statement therefore depends on the discount factors being decreasing in time, on the side constraints being monotone (G,g≥0), and on minimality of the PCPSP-C solution, without which an optimal solution may also extract clusters of zero value outside the limit.
Formalization scope
Everything lives in the namespace OpenPitMIP.UltPit. An instance is a structure over finite types of blocks, destinations and clusters, with periods Fin T (index t is period t+1, so the discount factor is (1+r)t+1). Block precedence is primitive; cluster precedence and the arc set A (the transitive reduction) are derived from it, and the precedence rows (4) and (13) range over A only. The standing assumptions of §2.1 are bundled in one hypothesis: the clusters partition the blocks (every cluster is nonempty), cluster precedence is a strict partial order, r>0, and qb≥0. The integrality condition is a parameter ranging over {full, partial}, and Theorem 1 is stated for both. Optimality and minimality are taken over the whole feasible set, with the componentwise order on the pair (x,y). At least one destination is assumed, so that maxdpb,d exists. U-PIT is the linear program over [0,1]C, not a binary closure problem.
The theorem is not trivialized: no minimal optimal solution is assumed to exist beyond what the hypotheses give, the discounting is part of the model (with arbitrary period values the theorem is false), and the hypotheses are jointly satisfiable (one block, one cluster, one period, p=−1, with the zero solution minimal optimal in both problems).
Contributions welcome: proofs of the milestones, a proof of Theorem 1, and reusable lemmas on closure polytopes (lattice structure, binary minimal optima), which are of interest beyond mining.
Selected references
O. Rivera Letelier, D. Espinoza, M. Goycoolea, E. Moreno, G. Muñoz, Production Scheduling for Strategic Open Pit Mine Planning: A Mixed-Integer Programming Approach, Operations Research 68(5):1425–1444, 2020. https://doi.org/10.1287/opre.2019.1965
L. Caccetta, S. P. Hill, An application of branch and cut to open pit mine scheduling, Journal of Global Optimization 27(2–3):349–365, 2003.
D. Bienstock, M. Zuckerberg, A new LP algorithm for precedence constrained production scheduling, working paper, Columbia University, 2009.
D. S. Hochbaum, The pseudoflow algorithm: A new algorithm for the maximum-flow problem, Operations Research 56(4):992–1009, 2008. https://doi.org/10.1287/opre.1080.0524
H. Lerchs, I. F. Grossmann, Optimum design of open-pit mines, Transactions of the Canadian Mining Institute 58(1):47–54, 1965.
Solving Chance-Constrained Problems via a Smooth Sample-Based Nonlinear Approximation 1: Smoothed Sample Feasible Sets Lie in the True Feasible Set with Probability ≥ 1 − ⌈1/β⌉⌈2LD/t⌉ⁿ exp(−2NM²)Research Paper
Motivation
A chance-constrained program minimizes a cost f(x) over a closed set X⊆Rn subject to a constraint that must hold with high probability rather than surely:
x∈Xminf(x)s.t.P(C(x,ξ)≤0)≥1−α,
where ξ is a random vector, C(x,ξ)=maxjcj(x,ξ) collects the uncertain constraints, and α∈(0,1) is the tolerated risk. Such models are used in power-system dispatch, portfolio selection, and supply-chain and process design, wherever a constraint may be violated in rare scenarios at a controlled rate.
The probability is rarely computable, so in practice it is replaced by an estimate from an i.i.d. sample ξ1,…,ξN. The empirical frequency is a step function of x and yields a mixed-integer program. Peña-Ordieres, Luedtke and Wächter (arXiv:1905.07377v2; SIAM J. Optim. 30(3), 2020) replace the indicator by a smooth approximation, which turns the sample problem into a smooth nonlinear program that standard solvers can handle. The question this mission addresses is whether a point accepted by the smoothed sample problem is actually feasible for the true chance constraint, and with what probability.
Timeline. Luedtke and Ahmed (SIAM J. Optim. 19 (2008)) proved finite-sample feasibility guarantees for the empirical (non-smooth) sample approximation, first for finite X and then, under a Lipschitz condition on C, for bounded X (their Theorem 10). Peña-Ordieres, Luedtke and Wächter (2020) extended these guarantees to the smoothed approximation (Theorems 3.8, 3.11 and 3.13 of the preprint).
Setting
Let ε>0 and let γε:[−ε,ε]→[0,1] be admissible: strictly decreasing, symmetric in the sense γε(−y)=1−γε(y), and such that the smoothed indicator
Γε(y)=⎩⎨⎧1γε(y)0y≤−ε−ε<y<εy≥ε
is differentiable on R. The paper's concrete choice is a quartic-kernel polynomial (its (2.6)).
For a decision x and a level t, define
the true cdfF(t;x)=P(C(x,ξ)≤t);
the smoothed cdfFε(t;x)=∫Γε(C(x,ξ)−t)dPξ;
the smoothed sample cdfFεN(t;x)=N1∑i=1NΓε(C(x,ξi)−t).
The true feasible set is Xα={x∈X∣F(0;x)≥1−α}, and the shifted sample feasible set with shift t and sample risk level δ is
Xε,δN,t={x∈X∣FεN(−t;x)≥1−δ}.
Throughout, C(x,ξ) has a continuous distribution for each x∈X (Assumption 3.1). The margin of a point is Mx=F(0;x)−Fε(−t;x)+(α−δ); Assumption 3.7 asks that δ∈[0,α] and M:=infx∈XMx>0.
Formalization targets
Goal: Theorem 3.13
Suppose X is bounded with sup-norm diameter D, that ∣C(x,ξ)−C(y,ξ)∣≤L∥x−y∥∞ for all x,y∈X with probability one (Assumption 3.12), and that Assumption 3.7 holds with t>0 and δ>0. Then for every β∈(0,δ],
P(Xε,(δ−β)N,2t⊆Xα)≥1−⌈1/β⌉⌈2LD/t⌉nexp{−2NM2}.
Milestones
Theorem 3.8. For x∈X∖Xα, P(FεN(−t;x)≥1−δ)≤exp{−2NMx2}.
Theorem 3.11. For finite X, P(Xε,δN,t⊆Xα)≥1−∣X∖Xα∣exp{−2NM2}.
The net claim (proof of Theorem 3.13). Each slice Xj of X by the value of F(0;⋅) at resolution 1/⌈1/β⌉ has a finite subset Zj with ∣Zj∣≤⌈2LD/t⌉n that is a t/L-net of Xj in ∥⋅∥∞.
(3.5). Theorem 3.11 applied to the net Z with levels α−β and δ−β.
The transfer step.x∈Xε,(δ−β)N,2t and ∥x−z∥∞≤t/L imply FεN(−t;z)≥1−δ+β.
Corollary 3.9 (companion). If C(x,ξ) has a density strictly decreasing on (−ε,ε) and F(0;x)<1−α, then βx=F(0;x)−Fε(0;x)>0 and P(FεN(0;x)≥1−α)≤exp{−2Nβx2}.
Significance
The result. Theorem 3.13 gives an explicit, non-asymptotic sample size N under which every point accepted by the smoothed sample problem (with a small shift 2t and a slightly tightened risk level δ−β) is feasible for the original chance constraint, uniformly over an infinite decision set. Solving the smooth approximation therefore yields certifiably feasible solutions with a quantified failure probability, the bound depending on the dimension n only through the covering number ⌈2LD/t⌉n. Corollary 3.9 adds that, under a monotone density near zero, the unshifted smoothed approximation is conservative.
Formalizing it. The results are proved in the paper; none is formalized anywhere to our knowledge. A formal development would produce a machine-checked one-sided Hoeffding bound for averages of bounded functions of an i.i.d. sample, a union bound over a finite candidate set, and a sup-norm covering lemma, assembled into a uniform feasibility guarantee. These ingredients are reused across the sample-average-approximation literature.
Difficulty
The obvious argument is a union bound over X, which fails for infinite X: the event Xε,(δ−β)N,2t⊆Xα involves uncountably many points, and is not even obviously measurable. Discretizing X by a sup-norm grid is not enough on its own either: a grid point may be infeasible while nearby points are feasible, and the true cdf F(0;⋅) need not be continuous in x. The paper's device is to discretize simultaneously in x and in the value of F(0;x), which requires covering each level slice separately and then transferring sample feasibility from a point to its representative, at the price of the shift 2t→t and the level change δ→δ−β. Keeping the constants exactly as printed, with ⌈1/β⌉ slices and ⌈2LD/t⌉n points per slice, is part of the task.
Formalization scope
Decisions are Fin n → ℝ, whose Mathlib norm is the sup norm ∥⋅∥∞ used in Assumption 3.12 and Theorem 3.13. X is closed (the paper's standing hypothesis).
ξ takes values in a measurable space Ξ with probability law Pξ. The sample is N≥1 measurable maps ξi:Ω→Ξ on a probability space, mutually independent, each with law Pξ. C(x,⋅) is assumed measurable for x∈X (a disclosed addition: it makes C(x,ξ) a random variable). Assumption 3.1 is encoded as Pξ(C(x,ξ)=y)=0 for all y.
Statements of the form "P(A)≥1−b" are stated as P(not A)≤b with P evaluated as an outer measure; this implies the printed form and assumes no measurability of the event.
Assumption 3.7's infimum M is a parameter with M>0 and M≤Mx on X, equivalent to the infimum because the bounds decrease in M.
"Bounded with diameter D" is ∥x−y∥∞≤D on X with D>0. Positivity is necessary: for a single infeasible point and n≥1 the printed bound with D=0 would read P≥1.
A formalization in which these hypotheses are unsatisfiable, the event is assumed measurable, or M is a junk infimum is ruled out: a sorry-free sanity file exhibits the quartic kernel (2.6) as admissible and a one-point instance meeting the goal's diameter and margin hypotheses.
Not posed: Hoeffding's inequality (Theorem 3.6), whose one-sided form is in Mathlib (ProbabilityTheory.measure_sum_ge_le_of_iIndepFun with hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero); and Corollary 3.10, whose printed exponent does not follow from its proof.
Contributions welcome: proofs of any milestone, in particular the sup-norm covering lemma and the Hoeffding step, which are reusable beyond this mission.
J. Luedtke, S. Ahmed, A sample approximation approach for optimization with probabilistic constraints, SIAM J. Optim. 19(2), 2008. https://doi.org/10.1137/070702928
Linear Convergence of First Order Methods for Non-Strongly Convex Optimization I: Strong ⇒ Quasi-Strong Convexity ⇒ Quadratic Gradient Growth ⇒ Quadratic Under-Approximation ⇒ Functional GrowthResearch Paper
Motivation
First-order methods (projected gradient, fast gradient, feasible descent) converge linearly on smooth strongly convex problems, but many problems met in practice are not strongly convex: least squares with a rank-deficient matrix, the dual of a linearly constrained problem, or g(Ax) with g strongly convex and A singular. Such problems have a whole set of minimisers, and strong convexity, which forces a unique minimiser, fails. Necoara, Nesterov and Glineur (arXiv:1504.06298; Math. Program. 175 (2019)) introduce a family of conditions that relax strong convexity by testing it only against the projection onto the optimal set, and prove that the classical first-order methods still converge linearly under them.
Related unconstrained conditions predate the paper: restricted strong convexity for X=Rn (Zhang and Cheng, Optim. Lett. 2015, the paper's reference [16]), and the error bounds of Luo and Tseng (1993). Karimi, Nutini and Schmidt (arXiv:1608.04636, 2016) compared similar unconstrained conditions with the Polyak–Łojasiewicz inequality. The constrained hierarchy treated here, with one constant along the whole chain, is the first section of the Necoara–Nesterov–Glineur paper and the basis of its convergence results.
This mission formalizes that hierarchy: Theorem 4 of the paper (arXiv v4, p. 9) and the results it is assembled from.
Setting
Let X⊆Rn be a closed convex set, with the Euclidean inner product ⟨u,v⟩=u⊤v and norm ∥u∥. Let f be a convex function on X, differentiable at every point of X, with gradient ∇fLipschitz on X with constant Lf>0:
∥∇f(x)−∇f(y)∥≤Lf∥x−y∥∀x,y∈X.(1)
The optimal setX∗={x∈X:f(x)≤f(y)∀y∈X} is assumed nonempty, and f∗ is the optimal value. For x∈X, xˉ=[x]X∗ denotes the projection of x onto X∗: the point of X∗ nearest to x.
For a constant κ>0 the paper considers five inequalities, for all x,y∈X:
The classes SLf,κ(X), qSLf,κ(X), GLf,κ(X), ULf,κ(X), FLf,κ(X) are the convex functions satisfying (1) and, respectively, (7), (10), (17), (13), (22). In Lean these are the predicates StrongIneq, QuasiStrong, QuadGradGrowth, QuadUnder and QuadFunGrowth of NecoaraNG.Chain.Setting, over optSet X f and the nearest-point predicate IsNearest.
The goal is the conjunction of the four implications under the standing assumptions.
Milestones
The projection onto X∗ is constant along [xˉ,x]: [xˉ+t(x−xˉ)]X∗=xˉ for t∈[0,1] (proof of Theorem 3, p. 8).
(11), p. 5: (7)⇒(10).
Theorem 1, p. 6: (10)⇒(13).
Theorem 2, p. 7: (10)⇒(17).
Theorem 3, p. 8: (17)⇒(13).
Proof of Theorem 4, p. 9: (13)⇒(22).
A companion item states the remark on p. 7: for convex f, (10) alone or (13) alone gives (17) with constant κ/2.
Significance
The chain gives the hierarchy that the paper's convergence theorems are stated for: the projected gradient method converges linearly on qS and, in distance to X∗, exactly on F; the fast gradient method keeps its accelerated rate on qS; and g(Ax) with g strongly convex is in qS on a polyhedron. Each such result transfers down the chain once the inclusions are known, and the fact that one κ survives every link is what keeps the rates' constants explicit.
All the statements are proved in the paper. None of them is formalized: the platform has unconstrained analogues (the Karimi–Nutini–Schmidt chain, with an existential constant and no feasible set), but no constrained statement and no statement with a fixed constant. A formal proof would also check the projection-invariance step that the paper uses without comment.
Difficulty
The links (7)⇒(10) and (13)⇒(22) are one-line substitutions. The substance is in Theorems 1 and 3, and specifically in the constant: combining (10) or (13) with the convexity inequality at a single pair of points gives (17) only with constant κ/2 (the companion item), and the same loss of a factor 2 appears in a direct derivation of (13) from (10). Keeping the full constant κ is what makes (23) a chain of inclusions with one index, and it is where the geometry of the optimal set enters: the conditions are tested only against the projection xˉ, which moves with x. Convexity of f cannot be dropped: (10) alone does not even imply convexity (p. 5).
Formalization scope
Rn is EuclideanSpace ℝ (Fin n); ∇f is Mathlib's gradient f. The function f is defined on all of Rn, with differentiability assumed at every point of X; "continuously differentiable" on X follows from (1).
Standing assumptions as hypotheses of every theorem: X closed and convex, f convex on X (ConvexOn ℝ X f), (1) with Lf>0, a minimiser x∗∈X∗, κ>0. "Simple" (cheap projection) and "closed" for f carry no mathematical content here and are dropped.
[x]X∗ is the predicate IsNearest (optSet X f) x xbar; each condition is required for every nearest point. f∗ is written f(xˉ), which is exact because xˉ∈X∗.
An empty optimal set would make every condition vacuous; the hypothesis x∗∈X∗ excludes this. The projection is never a choice function, and the gradient is only evaluated at points of X, where f is differentiable, so no junk value enters a statement. (7) is the first-order inequality with ∇f, not Mathlib's StrongConvexOn.
Needed infrastructure: the fundamental theorem of calculus along a segment for a function differentiable on a convex set, first-order optimality for a minimiser over a convex set, and the elementary geometry of nearest points. All of it is reusable for the other missions of this series.
Selected references
I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Math. Program. 175 (2019) 69–107. https://arxiv.org/abs/1504.06298
H. Karimi, J. Nutini, M. Schmidt, Linear convergence of gradient and proximal-gradient methods under the Polyak–Łojasiewicz condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
H. Zhang, L. Cheng, Restricted strong convexity and its applications to convergence analysis of gradient type methods in convex optimization, Optim. Lett. 9 (2015) 961–979. https://doi.org/10.1007/s11590-014-0795-x
Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
Optimal Approximation for Submodular and Supermodular Optimization with Bounded Curvature II: Column-Subset Selection Has Total Curvature at Most 1 − 1/κ(A)²Research Paper
Why column-subset selection and curvature
The column-subset selection problem (CSSP) asks for k columns of a real matrix A whose span approximates all of A as well as possible in squared Frobenius norm. It is a basic primitive of low-rank approximation, feature selection and numerical linear algebra, studied both for its exact complexity and for approximation algorithms (see Boutsidis, Drineas and Magdon-Ismail, doi:10.1137/12086755X, cited as [2] in the source paper).
Sviridenko, Vondrák and Ward study submodular maximization and supermodular minimization when the objective has bounded total curvature, a parameter c∈[0,1] introduced by Conforti and Cornuéjols that measures how far a monotone set function is from being linear. Their guarantees improve as c decreases. Section 8 of the paper applies this to CSSP: it bounds the curvature of the CSSP objective in terms of the condition number of A, so that a well-conditioned matrix has small curvature. This mission formalizes that bound (Lemma 8.2) and the steps of its proof.
Setting
Let A be a real m×n matrix with columns c1,…,cn∈Rm, so that Ax=∑ixici for x∈Rn, and let ∥⋅∥ be the Euclidean norm. For S⊆[n] write projS(x) for the orthogonal projection of x onto span{ci:i∈S}, the point of that subspace nearest to x (proj∅=0). The CSSP objective is
fA(S)=i=1∑n∥ci−projS(ci)∥2,
the squared Frobenius distance from A to the nearest matrix whose columns lie in the span of the selected columns.
For a set function f on a finite set X, the marginal value of i at A is fA(i)=f(A+i)−f(A). The function f is monotone decreasing if every fA(i)≤0. Following (1.1) of the paper, a monotone decreasing f has total curvature at most c when, for every j∈X,
fX−j(j)≤(1−c)f∅(j),
i.e. the last marginal of j is at least a (1−c) fraction of its first marginal in absolute value.
When the columns of A are linearly independent, the condition number is
κ(A)=inf∥x∥=1∥Ax∥sup∥x∥=1∥Ax∥∈[1,∞).
Formalization targets
Goal: Lemma 8.2 (p. 11)
For A with linearly independent columns,
f[n]−jA(j)≤κ2(A)1f∅A(j)for all j∈[n],i.e.c(fA)≤1−κ2(A)1.
Milestones
The identity fA(S)=∑i(∥ci∥2−∥projS(ci)∥2) (p. 11).
Lemma 8.1, monotone part: S↦∥projS(v)∥2 is monotone increasing (p. 11).
fA is monotone decreasing (p. 11).
∣f∅A(i)∣=∑j∥proj{i}(cj)∥2 (p. 11).
Some unit x has ∥Ax∥≥∣f∅A(i)∣ (p. 12).
∣f[n]−iA(i)∣=∥ci−proj[n]−i(ci)∥2 (p. 12).
Some unit x′ has ∥Ax′∥≤∣f[n]−iA(i)∣ (p. 12).
κ2(A)≥f∅A(i)/f[n]−iA(i) for each i, under independence (p. 12).
Items 1–7 hold for arbitrary columns; only item 8 and the goal assume independence.
Significance
Lemma 8.2 turns a spectral quantity into a combinatorial one. With it, any curvature-dependent guarantee for monotone decreasing set functions can be stated for CSSP in terms of κ(A). The paper's Lemma 8.3 shows the bound is asymptotically tight, so 1−Θ(1/κ2) is the right order of the curvature.
There is a caveat that the formalization makes explicit. The paper deduces from Lemma 8.1 that fA is supermodular, and on that basis quotes its supermodular-minimization algorithm for CSSP with factor 1+(κ2−1)e−1+κ2O(ϵ) (p. 12). Both the submodularity half of Lemma 8.1 and the supermodularity of fA are false as printed. With c1=e1, c2=e1+e2 and v=e2 in R2, the function F(S)=∥projS(v)∥2 has F({1,2})+F(∅)=1>21=F({1})+F({2}). With columns e1,e1+e2,2e2, fA({1})+fA({2})=215>7=fA({1,2})+fA(∅). A small perturbation gives a counterexample with independent columns. This is the "suppressor variable" phenomenon of regression. The curvature bound itself does not depend on supermodularity and is true, so it is the goal here. The approximation factor for CSSP is not posed, because it rests on the false claim and is stated with O(ϵ).
As far as is known, none of these statements has a machine-checked proof. The results are proved on paper, except the two false claims above. The mission adds a formal proof of the curvature–conditioning bound, and makes explicit which parts of §8 survive.
Difficulty
The individual steps are short linear algebra, but they rest on infrastructure that has to be assembled: orthogonal projections onto spans of finite column families, the Pythagorean identities that relate fA to projections, and the variational characterization of sup and inf of ∥Ax∥ over the unit sphere.
The paper's own route to the large unit vector (milestone 5) does not work as printed. It sets xj∝∥proj{i}(cj)∥ and uses ci⋅cj=∥ci∥∥proj{i}(cj)∥, which is false when ci⋅cj<0, so the signs of the inner products have to be accounted for. In the final step, the ratio f∅A(i)/f[n]−iA(i) is a quotient of two negative numbers. Comparing it with κ2 requires the supremum to be finite and the infimum to be strictly positive, which is exactly what independence of the columns provides.
Formalization scope
Columns are a family c : Fin n → EuclideanSpace ℝ (Fin m), and Ax is ∑ j, x j • c j. Subsets of [n] are Finset (Fin n). [n]−i is Finset.univ.erase i and S+i is insert i S.
projS is Mathlib's Submodule.starProjection onto Submodule.span ℝ (c '' S), which is finite-dimensional, so the argmin of the page exists and is unique.
κ(A) is a real quotient of ⨆ and ⨅ of ∥Ax∥ over the unit-sphere subtype of Rn. It is used only under LinearIndependent ℝ c, the page's "non-singular", where both are finite and positive. The page's κ=∞ for dependent columns is not encoded.
Monotonicity is the marginal form of §2.1. Curvature is the product form above, which agrees with the ratio of (1.1) whenever f∅(j)=0 and avoids Lean's x/0=0.
For n=0 the goal has no j and is empty, as on the page.
A trivializing reading is ruled out by the encoding: had κ evaluated to a junk value 0, the goal would reduce to monotonicity. Under independence the supremum and infimum are genuine, so the bound 1−1/κ2 is the paper's.
Not in scope: Lemma 8.3 (stated with O(⋅)), the CSSP approximation factor, and the false submodularity and supermodularity claims.
Useful infrastructure that would be reusable beyond this mission includes Pythagoras for starProjection, monotonicity of projection norms under inclusion of subspaces, and extremal characterizations of sup∥x∥=1∥Ax∥ and inf∥x∥=1∥Ax∥. Contributions of any of the milestones, or of these general lemmas, are welcome.
Selected references
M. Sviridenko, J. Vondrák, J. Ward, Optimal approximation for submodular and supermodular optimization with bounded curvature, SODA 2015 (version of Oct. 9, 2014); journal version Math. Oper. Res. 42(4), 2017. https://doi.org/10.1287/moor.2016.0842
M. Conforti, G. Cornuéjols, Submodular set functions, matroids and the greedy algorithm: tight worst-case bounds and some generalizations of the Rado–Edmonds theorem, Discrete Appl. Math. 7(3), 1984. https://doi.org/10.1016/0166-218X(84)90003-9
C. Boutsidis, P. Drineas, M. Magdon-Ismail, Near-optimal column-based matrix reconstruction, SIAM J. Comput. 43(2), 2014. https://doi.org/10.1137/12086755X
A. Das, D. Kempe, Submodular meets spectral: greedy algorithms for subset selection, sparse approximation and dictionary selection, ICML 2011. https://arxiv.org/abs/1102.3975
Production Scheduling for Strategic Open Pit Mine Planning: A Mixed-Integer Programming Approach 4: Hourglass Production Cuts Are Valid under Full and Partial IntegralityResearch Paper
Motivation
Strategic open pit mine planning decides which parts of an ore body are excavated, in which period, and to which destination (a processing plant, a stockpile, a waste dump) each block of material is sent. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research 68(5), 2020) model this as a mixed-integer program, the precedence-constrained production scheduling problem with clusters (PCPSP-C), which extends the PCPSP of Bienstock and Zuckerberg (2010) by grouping blocks into clusters that are extracted together. The integer versions of the model have weak linear relaxations on production scheduling instances, so the authors derive cutting planes. Their production cuts (§5.2) exploit the capacity of a single destination together with the precedence structure. This mission concerns the second family of production cuts, the hourglass cuts: they bound how much material must be sent away from a capacitated destination once a cluster is started, using both the predecessors and the successors of that cluster.
Valid inequalities for precedence-constrained knapsack problems have been studied since Boyd (1993) (cited on p. 1433); the paper's contribution is the extension to several destinations, several periods, clusters and partial integrality, the condition used in commercial mine planning software.
All page references are journal pages of the published Operations Research article.
Setting
An instance has finite sets B of blocks, D of destinations and C of clusters, the latter a partition of B, and periods T={1,…,T}. Block b lies in cluster c(b) and has weight qb≥0. A precedence relation b1≺b2 on blocks induces one on clusters (c1≺c2 if some block of c1 precedes some block of c2), assumed to be a strict partial order. The arc set A is its transitive reduction: (c,c′)∈A when c′ is an immediate predecessor of c. The closure is cl(c)={c}∪{c′:c′≺c} and the reverse closurercl(c)={c}∪{c′:c≺c′}; b(S) is the set of blocks of a set S of clusters, and q(S) is the total weight of a set of blocks.
Variables xc,t give the fraction of cluster c extracted in period t and yb,d,t the fraction of block b sent to destination d in period t. The constraints (2)–(7) of p. 1427 are
with an integrality condition: full integrality (10), xc,t∈{0,1}, defines the PCPSP-F, and partial integrality (11), "∑t′≤txc,t′>0 implies ∑t′≤txc′,t′=1 for (c,c′)∈A", defines the PCPSP-P. The rows Gy≤g include the destination capacity rows (9), ∑bqbyb,d,t≤Utd. The cuts are written in the cumulative variableswc,t=∑t′=1txc,t′ (17).
The simplified setting of §5.2.1 is the mode-knapsack set MK (p. 1433): for a directed acyclic graph G=(B,A), weights q>0 and a capacity U>0, the triples (x,yP,yW) with ∑bqbybP≤U, ybP+ybW=xb≤1, yP,yW≥0, and xb>0⇒xb′=1 for every arc (b,b′). Here P is processing and W is waste.
Formalization targets
Goal: Theorem 8 (hourglass cuts), p. 1435
Let d∈D, 1≤t1≤t≤T, cˉ∈C, and let S⊆b(cl(cˉ)∖{cˉ}) be a set of blocks with q(S)≥∑s=t1tUsd. With R=rcl(cˉ)∖{cˉ}, the inequality
is valid for the PCPSP-C, that is, for both the PCPSP-F and the PCPSP-P.
Milestones
Proof of Theorem 8, p. 1435: if wcˉ,t>0, every cluster preceding cˉ has wc,t=1.
Proof of Theorem 8, p. 1435: the blocks of S, of cˉ and of b(R) together respect the capacity Usd of every period.
Theorem 6, p. 1434: the simplified hourglass cut (q(S)+qb−U)xb≤∑b′∈S∪{b}qb′yb′W is valid for MK when S⊆cl(b)∖{b} and q(S)≥U.
The lifted inequality of p. 1434, which adds ∑b′∈rcl(b)∖{b}qb′yb′P to the left-hand side of Theorem 6.
Display (38), p. 1436: the block set S∗={b:c(b)≺cˉ,wcˉ,t∗>wc(b),t∗−∑s=t1tyb,d,s∗} maximizes the violation of (37) at any point (w∗,y∗).
Significance
In the computational study of §8 (Table 5, p. 1440; discussion on p. 1442) the authors add early start, lifted clique, VRHS and hourglass cuts to the LP relaxation and drop one class at a time; they observe that all classes improve the bound and that the hourglass cuts have the most significant impact. Display (38) makes the separation of the most violated hourglass cut a single pass over the blocks for each cluster, destination and period window. The cuts are valid under partial integrality, the weaker condition that mine planning software imposes, so they strengthen the relaxation of the model actually solved in practice.
Theorem 8 is proved in the paper by a direct calculation; no machine-checked proof exists. A formal proof would certify the inequality in exactly the generality of the model (clusters, several destinations, several periods, both integrality conditions), and the formal model of the PCPSP-C built for it is shared with the other missions of this series.
Difficulty
The inequality is false for the LP relaxation: a fractional start of cˉ need not force its predecessors to be complete. Every proof therefore has to use integrality, and the two integrality conditions behave differently. Under partial integrality (11) the implication "started implies predecessors complete" is stated only along the arcs of the transitive reduction A, and has to be propagated along chains of immediate predecessors to reach every predecessor of cˉ. The capacity step needs that the strict predecessors, cˉ itself and its strict successors are pairwise disjoint block sets, which is where the strict partial order is used. The w terms are cumulative from period 1 while the y terms are summed from t1; the two must not be aligned.
Formalization scope
Periods are Fin T, so index t denotes period t+1. Cluster precedence is derived from the block relation, and A is its covering relation. The standing assumptions of §2.1 (clusters partition the blocks, ≺ a strict partial order on clusters, discount rate r>0, weights q≥0) are a single hypothesis on the instance. "Valid for the PCPSP-C" is stated as: for each integrality condition, at every feasible (x,y) whose destination capacity rows (9) hold, which is the page's assumption that (9) is among the rows Gy≤g. The destination d, unbound on the page, is a fixed arbitrary destination. In Theorem 8 S is a set of blocks and q(S∪{cˉ}) is the weight of S together with the blocks of cˉ. In MK an arc (b,b′) means b′ precedes b, and ≺ is reachability in G.
Reading "valid" as "valid for the LP relaxation" would make the goal false, while dropping the condition S⊆b(cl(cˉ)∖{cˉ}), or the capacity rows, would make it a different statement; neither is the target. In (38) the maximum is taken over all S⊆b(cl(cˉ)∖{cˉ}) as on the page, without the side condition q(S)≥∑Usd, which S∗ need not satisfy.
A complete development needs only finite sums, finsets and the transitive closure of a relation from Mathlib. Proofs of the milestones, of the MK results and of the goal are all welcome; the lemma that partial integrality propagates along chains of arcs is reusable across all production cuts of the paper.
Selected references
O. Rivera Letelier, D. Espinoza, M. Goycoolea, E. Moreno, G. Muñoz, Production scheduling for strategic open pit mine planning: a mixed-integer programming approach, Operations Research 68(5):1425–1444, 2020. https://doi.org/10.1287/opre.2019.1965
D. Bienstock, M. Zuckerberg, Solving LP relaxations of large-scale precedence constrained problems, Proc. 14th Conf. Integer Programming and Combinatorial Optimization (IPCO), 1–14, 2010 (reference list of the article above).
E. A. Boyd, Polyhedral results for the precedence-constrained knapsack problem, Discrete Applied Mathematics 41(3):185–201, 1993 (reference list of the article above).
A Single Timescale Stochastic Approximation Method for Nested Stochastic Optimization: NASA with Stepsizes 1/√N Drives the Expected Stationarity Measure E[V(x_R, z_R)] Below C/(√N − 1)Research Paper
Motivation
Many learning and risk-averse decision problems minimize a function of an expectation that is itself passed through another function: F(x)=f(g(x)) with g(x)=E[G(x,ξ)]. Examples are mean–deviation risk measures, stochastic variational inequalities rewritten as minimization, and policy evaluation in reinforcement learning. Only noisy samples of g, of its Jacobian and of ∇f are available, and the plug-in estimate ∇g(x)⊤∇f(G) of ∇F(x) is biased because f is nonlinear. Classical stochastic gradient analysis does not apply directly.
Timeline of sample complexities for smooth nonconvex two-level problems, measured by the number of samples needed to reach an ε-stationary point:
2017 — Wang, Fang and Liu (Math. Program.) introduce stochastic compositional gradient descent with two time scales; the unconstrained nonconvex rate is O(ε−4) in their measure.
2017 — Wang, Liu and Fang (JMLR) accelerate it to O(ε−2.25) for smooth unconstrained problems, still with two time scales.
2019–2020 — Ghadimi, Ruszczyński and Wang (arXiv:1812.01094, SIAM J. Optim. 2020) propose NASA, a single-time-scale method with one sample per iteration, and prove O(ε−2) for constrained problems. This mission formalizes that result.
Setting
Problem (1.1) is
x∈XminF(x)=f(g(x)),
where f:Rm→R and g:Rn→Rm are continuously differentiable, X⊆Rn is closed and convex, and nothing is convex. Assumption 2 asks that f, g, ∇f, ∇g be Lipschitz with constants Lf,Lg,L∇f,L∇g; then ∇F is Lipschitz with L∇F=Lg2L∇f+LfL∇g. F∗ is the infimum of F over X.
For β>0 the subproblem solution is yˉ(x,z,β)=argminy∈X{⟨z,y−x⟩+2β∥y−x∥2}=ΠX(x−z/β), with ΠX the Euclidean projection. A pair (x,z) is judged by the optimality measure
V(x,z)=∥yˉ(x,z,1)−x∥2+∥z−∇F(x)∥2,
which vanishes exactly when z=∇F(x) and −∇F(x) lies in the normal cone to X at x.
The NASA method (Algorithm 1) keeps three sequences: iterates xk∈X, gradient averages zk and value averages uk. With parameters a,b>0, regularization β>0 and stepsizes τk∈(0,1/a]:
Assumption 1 governs the oracle. Given Fk, the outputs Gk+1, Jk+1 and sk+1 are conditionally unbiased for g(xk+1), ∇g(xk+1) and ∇f(uk). Their second moments are bounded by σG2,σJ2,σs2, and sk+1, Jk+1 are conditionally independent. The analysis rests on the merit functionW(x,z,u)=a(F(x)−F∗)−η(x,z)+2γ∥g(x)−u∥2, where η is the optimal value of the subproblem.
Formalization targets
Goal: Theorem 2(c), (3.37)
With a=b=1, β=(α(1+α)2Lg2+4α)L∇f for some α>0, τ0=1, τk=1/N for k≥1, N≥2, and R uniform on {1,…,N−1}:
The constants L1,L2 (3.32) and σ^2 are explicit in the problem data. This is the paper's headline rate, and every other statement of the mission feeds it.
Milestones
Lemma 1: ∥yˉ(x,z,1)−x∥≤max(1,β)∥yˉ(x,z,β)−x∥.
Lemma 2: ∇F is L∇F-Lipschitz.
Lemma 3: η has an L∇η-Lipschitz gradient in (x,z).
(3.21): ⟨z,d⟩+β∥d∥2≤0 for the subproblem step d.
Lemma 4: the pathwise descent inequality c∑τk(∥dk∥2+∥g(xk)−uk∥2)≤W(x0,z0,u0)+∑rk+1.
Proposition 1(a): moment bounds on zk and dk.
Proposition 1(b): ∑E[rk+1]≤σ^2∑τk2.
(3.29): V(x,z)≤max(1,β2)∥d∥2+∥z−∇F(x)∥2.
Theorem 2(a): the weighted gradient-tracking error.
Theorem 2(b): the bound on E[V(xR,zR)] for general admissible stepsizes.
Significance
The result. Theorem 2(c) gives E[V(xR,zR)]≤ε after O(ε−2) iterations with one oracle call each. That matches the complexity of stochastic gradient descent on single-level smooth nonconvex problems, so the nested structure costs only constants. The bound holds with constraints, and zR comes with a certified estimate of ∇F(xR). The same merit-function technique underlies later single-time-scale methods for multi-level and conditional stochastic optimization.
Formalizing it. The result is proved on paper, not formalized. A machine-checked proof requires the whole chain, Lemma 4 through Theorem 2, to be stated with constants that the argument actually supports. Several printed constants do not meet that bar (see Formalization scope), so the formalization also certifies a corrected version of the theorem. The deterministic milestones (Lemmas 1–3, (3.21), (3.29)) are general facts about Euclidean projections and value functions of strongly convex subproblems, and other projected-gradient developments can reuse them.
Difficulty
The obvious approach fails. Analyzing F(xk) alone does not work because the step uses zk, a biased and correlated estimate of ∇F(xk), and its error does not vanish at a single time scale. The analysis instead tracks the coupled potential W. Each of its three terms needs a different tool: the descent lemma for F, the smoothness of the value function η (Lemma 3, which needs differentiability of a parametric minimum), and a recursion for uk. These pieces must combine under the single coupling condition (3.16). The probabilistic part is delicate as well. The cross terms vanish only in expectation, they require conditional independence of Jk+1 and sk+1, and their integrability is not automatic. Theorem 2(a) adds a weighted unrolling of the z-recursion through the products Γk and the summation condition (3.30).
Formalization scope
Points live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). Jacobians are continuous linear maps with the operator norm, and ∇g(x)⊤ is the adjoint. The projection is a function P with the published predicate SpectralProjGrad.Shared.IsProjOnto X P, and yˉ(x,z,β)=P(x−β−1z). η is the subproblem objective evaluated at yˉ, and Lemma 3 places (x,z) in the L2 product WithLp 2 (ℝⁿ × ℝⁿ). F∗ is sInf over X, and F is assumed bounded below on X. The regularization βk≡β and the stepsizes are deterministic.
The randomness lives on a standard Borel probability space. Assumption 1 is stated with respect to any filtration to which xk,zk,uk are adapted, which includes the paper's natural filtration. It requires square-integrable oracle outputs, so that no conditional-expectation hypothesis is vacuous. Statements printed with conditional expectations on the left and constants on the right (Proposition 1, Theorem 2(a)) are stated in total expectation, which is what the proofs establish. Every conclusion about an expectation includes the integrability of the integrand, so a bound cannot hold because a non-integrable integral defaults to 0. E[V(xR,zR)] is the τ-weighted average of E[V(xk,zk)] over k=1,…,N−1 (3.34). Lemma 4 is deterministic: it holds along every path of the recursions, whatever the oracle outputs. The recursions tie yk to the projection and zk,uk to the oracle outputs, so the goal cannot be satisfied by arbitrary sequences or by a vacuous oracle.
Corrections to printed constants, each stated in the item's Formalization Note:
(3.18): the noise term of rk+1 carries γb2, not b2. The printed Lemma 4 has a counterexample.
(3.26): σ^2 uses aL∇F, max(σJ2σs2,∥z0∥2)/β2 (the k=0 term) and γb2σG2.
(3.33): the coefficient of max(1,β2)σ^2 is 1/c, not acˉ/c. The two agree when acˉ=1.
(3.37): the denominator is αL∇f, not αL∇F, since the proof sets c=αL∇f/4. The proof also fixes γ=αL∇f in W and σ^2.
Proposition 1(a): the bound E∥zk∥2≤σJ2σs2 is false conditionally on Fk−1 and is stated in expectation.
Hypotheses the proofs use but the statements omit: τk≤1, bτk≤1, aβ≥c and γb≥2c, τ0=1/a (Theorem 2(a),(b)), N≥2, and L∇f>0.
The second claim (3.38) of Theorem 2(c) is excluded: its printed constant is smaller than what the proof gives. Theorem 3 (asymptotics) and the ASA variant of §4 are out of scope. Contributions are welcome at every milestone. Solvers will need Euclidean projection characterizations, differentiability of the squared distance to a convex set, conditional-independence product rules for conditional expectations, and Abel-type summation for the Γk weights.
Selected references
S. Ghadimi, A. Ruszczyński, M. Wang, A Single Time-Scale Stochastic Approximation Method for Nested Stochastic Optimization, arXiv:1812.01094v2, 2019; SIAM J. Optim. 30(1), 2020. https://arxiv.org/abs/1812.01094
M. Wang, E. X. Fang, H. Liu, Stochastic compositional gradient descent: algorithms for minimizing compositions of expected-value functions, Math. Program. 161, 2017. https://doi.org/10.1007/s10107-016-1017-3
S. Ghadimi, G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23(4), 2013. https://doi.org/10.1137/120880811
A. Ruszczyński, Nonlinear Optimization, Princeton University Press, 2006.
Dynamic Pricing in the Presence of Social Learning and Strategic Consumers 2: Under Responsive Pricing, Social Learning Raises Optimal Expected Profit When Consumers Are Impatient or PatientResearch Paper
Motivation
A firm launching a new experience good does not know how good the product is, and neither do its customers. Early buyers post reviews, and customers who wait learn from them: this is social learning (SL). Forward-looking customers anticipate this and may delay their purchase until reviews are available, which cuts into the firm's early sales. Papanastasiou and Savva (Management Science 2017) ask whether SL helps or hurts a monopolist facing such strategic consumers.
This mission formalizes their answer for responsive pricing, where the firm cannot commit to a second-period price and instead sets it after observing the reviews. Without learning, this is the classical price-skimming game of Besanko and Winston (1990), in which a firm without commitment power is hurt by consumer patience. With learning, two effects compete: reviews make the second-period market more informative (an informational effect the firm can exploit by repricing), and the option to learn makes waiting more attractive (a behavioral effect that hurts the firm).
Setting
A monopolist sells over two periods at unit cost c∈[0,1) to a unit mass of consumers with preference types x uniform on [0,1]. The mean quality is unknown, with prior N(0,σp2), and reviews are noisy with variance σq2; the SL influence parameter is γ=σp2/σq2≥0. Consumers discount second-period utility by δc∈[0,1]; the firm does not discount.
If a set B⊆[0,1] of types buys in period 1, its mass ∣B∣ is the mass of reviews, and the posterior mean qu, seen from period 1, has the pre-posterior lawN(0,σp2∣B∣γ+1∣B∣γ) (Lemma 1 and Definition 1 of the paper). In period 2 the remaining types value the product at x+qu.
Under responsive pricing the firm sets p1; consumers decide whether to buy now or wait; reviews realize qu; the firm sets p2=s(qu) to maximize the second-period profit
π2(p2)=(p2−c){x∈[0,1]∖B:x+qu≥p2}.
An equilibrium after p1 is a measurable buyer set B and a measurable rule s that is optimal at every qu, such that every type in B weakly prefers x−p1 to the discounted expected value δcE[(x+qu−s(qu))+] of waiting, and every type outside B weakly prefers waiting. The firm's expected profit is πr=(p1−c)∣B∣+E[π2(s(qu))], and πr∗ is its supremum over all p1 and all equilibria. The benchmark "absence of SL" (γ→0 in the paper) is the same model at γ=0, where qu=0 with certainty.
The thresholds are left unspecified; the statement asserts only that SL raises the optimal profit near both ends of the patience range.
Milestones
Lemma 3: the second-period price p2∗(qu,xˉ) of (6) is optimal when [0,xˉ) remains.
(5): without SL, the first-period buyers are the types x≥χ(p1)=2−δc2p1−cδc.
Proposition 4: the benchmark optimum p1∗=6−4δc2c+δc2(1−c)+4(1−δc), p2∗=2χ(p1∗)+c, and monotonicity in δc.
Lemma 4: with SL, the first-period threshold ζ(p1) solves the implicit equation (7).
(8): the expected profit as a function of the threshold (with a corrected integrand).
Proposition 5: adoption inertia is never optimal; the on-path second-period price.
Example 3: the endpoint δc=0.
Continuity of πr∗ in δc∈[0,1] (proof of Proposition 6).
Significance
The result shows that the benefit of reviews to a firm that reprices dynamically, previously established for non-strategic consumers, survives when consumers strategically wait for information. It is one half of the paper's comparison between commitment and responsiveness: under SL the firm's flexibility to react to reviews becomes valuable, which reverses the classical ranking of pre-announced over responsive pricing.
The paper proves the result on paper only. This mission produces a machine-checked model of a two-period game with a continuum of consumers, Bayesian learning and subgame-perfect pricing, and machine-checked versions of the equilibrium characterizations. The paper's numerical evidence that the result holds for all δc is not part of the goal.
Difficulty
The first-period threshold is defined implicitly: in (7) the law of qu has a variance that depends on the threshold itself, and the second-period price inside the integral is a piecewise function of both. Existence, uniqueness and the comparison with the benchmark all go through this fixed-point equation.
The endpoint δc=1 relies on Proposition 5(i), that inducing adoption inertia is strictly suboptimal. At δc=1 the alternative price used in the printed proof yields exactly the inertia profit, so this endpoint is not settled by the page's witness. Passing from the two endpoints to the thresholds requires continuity of an optimal value taken over an unbounded price set and over implicitly defined equilibria; the paper cites the Maximum Theorem, whose hypotheses must be established.
Formalization scope
Everything lives in namespace SLPricing.Resp. The model file is shared, verbatim, with the two other missions of this series. Conventions:
Best responses are weak, so buyer sets are unique only up to null sets.
The second-period rule must be optimal at every realization and measurable. In the exit region qu≤c−xˉ every optimal price sells nothing; (6)'s value c is a convention there.
Optimal values are suprema in EReal over all real prices and all their equilibria, so neither an empty nor an unbounded family produces a junk value. Defining πr∗ as the profit at a closed-form price, or the benchmark by dropping the second period, would make the goal circular; the formalization does neither.
The thresholds are in the half-open intervals of the page; closed intervals would make the goal trivial.
Hypotheses added or restricted relative to the page, each disclosed in its item:
(5) assumes p1≥c (the printed formula is wrong below cost) and states uniqueness for δc<1 (at δc=1 non-threshold equilibria exist).
Proposition 4 states uniqueness only for δc<1 (at δc=1 every p1≥(1+c)/2 is optimal).
Lemma 4 assumes p1≥0; its monotonicity sentence is not posed.
Lemma 3's uniqueness assumes xˉ>0 and qu>c−xˉ.
(8) is stated with last integrand ζ(qu−c); the page prints ζqu, which contradicts the proof of Lemma 3.
Contributions welcome: Gaussian integral estimates for (7), the second-period optimization of Lemma 3, a witness against inertia at δc=1, and a continuity argument for optimal values over parametrized equilibria, which is reusable for the series' other missions.
Selected references
Y. Papanastasiou, N. Savva, Dynamic Pricing in the Presence of Social Learning and Strategic Consumers, Management Science 63(4):919–939, 2017. https://doi.org/10.1287/mnsc.2015.2378 (cited from the accepted manuscript MS-14-00028.R2, 2016)
D. Besanko, W. L. Winston, Optimal Price Skimming by a Monopolist Facing Rational Consumers, Management Science 36(5):555–567, 1990. https://doi.org/10.1287/mnsc.36.5.555
Y. Aviv, A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
Optimal Approximation for Submodular and Supermodular Optimization with Bounded Curvature I: Swap-Local Optima of the Non-Oblivious Potential Are (1 − c/e)-Approximate for Submodular MaximizationResearch Paper
Motivation
Maximizing a monotone submodular function over the bases of a matroid is the standard model for coverage, facility location, sensor placement and welfare maximization. The best possible approximation factor in the value-oracle model is 1−1/e (Nemhauser–Wolsey 1978; Călinescu–Chekuri–Pál–Vondrák 2011). Many functions met in practice are far from the worst case: they are close to linear. Total curvature measures how close. Conforti and Cornuéjols (1984) showed that the greedy algorithm achieves (1−e−c)/c on uniform matroids and 1/(1+c) on general matroids when the curvature is at most c; Vondrák (RIMS Kôkyûroku Bessatsu, 2010) obtained (1−e−c)/c for every matroid, for a weaker curvature notion.
Sviridenko, Vondrák and Ward (SODA 2015; journal version Math. Oper. Res. 2017) improve this to 1−c/e, show it is optimal, and obtain the matching factor 1+1−cce−1 for minimizing a monotone decreasing supermodular function. One of their two algorithms is a non-oblivious local search, a single-swap search guided not by f but by an auxiliary potential. This mission formalizes the exact guarantee of that local search. All numbering below is that of the SODA 2015 version (authors' copy dated Oct. 9, 2014).
Setting
Let X be a finite set. A set function assigns a real number f(A) to every A⊆X. Its marginal value at i∈X over A is fA(i)=f(A+i)−f(A). The function is submodular if f(A)+f(B)≥f(A∩B)+f(A∪B) for all A,B; supermodular if −f is submodular; monotone increasing if every fA(i)≥0, and monotone decreasing if every fA(i)≤0.
A monotone increasing f has total curvature at most c if fX−j(j)≥(1−c)f∅(j) for every j∈X: adding j last is worth at least a (1−c) fraction of adding it first. For c=0 the function is linear up to a constant; c=1 is no restriction. For a monotone decreasing f the inequality is reversed: fX−j(j)≤(1−c)f∅(j).
A matroidM=(X,I) is given by its independent sets; its basesB(M) are the maximal independent sets, and its dualM∗ has the complements X∖B of bases as bases.
For a monotone increasing submodular f, §6.1 of the paper splits f=g+ℓ with a linear part and a remainder,
ℓ(A)=j∈A∑fX−j(j),g(A)=f(A)−ℓ(A).
The local search uses the Filmus–Ward potential of g and the potential ψ:
A base S is a swap-local optimum of ψ if ψ(S−a+b)≤ψ(S) for every a∈S and b∈X∖S with S−a+b a base.
Formalization targets
Goal: exact core of Theorem 6.1
For f≥0 monotone increasing and submodular with curvature at most c∈[0,1], every swap-local optimum S of ψ satisfies
f(S)≥(1−ec)f(O)for every O∈I.
The printed Theorem 6.1 asserts a randomized polynomial-time algorithm losing O(ϵ); the goal is the ϵ=0 statement its proof establishes for local optima.
Milestones
Lemma 2.1: ∑j∈AfX−j(j)≥(1−c)f(A), for f(∅)=0.
Lemma A.1: g=f−ℓ is submodular, monotone increasing and nonnegative.
Lemma 5.1 (Brualdi): two bases A,B admit a bijection π:A→B with A−x+π(x) a base for every x∈A.
§5.1: a swap-local optimum S satisfies g(S)+ℓ(S)≥(1−e−1)g(O)+ℓ(O) for every base O.
Companion statements
Lemma 2.2, Lemma A.2 and the exact core of Theorem 6.2: for f≥0 monotone decreasing and supermodular with curvature at most c∈[0,1), a swap-local optimum S of the corresponding ψ in M∗ yields a base X∖S of M with
f(X∖S)≤(1+1−cce−1)f(O)for every O∈I.
Lemmas A.3 and A.4 are the curvature constructions behind the paper's matching lower bounds.
Significance
The factor 1−c/e equals 1−1/e at c=1 and tends to 1 as c→0, so it recovers the classical bound and improves it for every curvature below 1; Theorem 7.1 of the paper shows that no algorithm using polynomially many value queries does better. The decomposition f=g+ℓ and the joint guarantee g(S)+ℓ(S)≥(1−e−1)g(O)+ℓ(O) are reusable: they give the supermodular-minimization result of Theorem 6.2, and §8 of the paper applies that result to column-subset selection.
The results are proved in the literature; none is machine-checked. The mission produces a formal proof of the exact local-search guarantee, of Brualdi's bijective exchange for Mathlib matroids, and of Filmus and Ward's inequality for their potential h, which underlies other non-oblivious local searches for submodular functions.
Difficulty
The reduction from the goal to the §5.1 claim is short. The work is in (5.4): the obvious argument, summing submodularity over the swaps, controls ∑i[g(A)−g(A−ai+bi)] and gives only the oblivious factor 1/2. The potential h averages g over all subsets of A with Beta-type weights, and (5.4) is an identity-level computation with the integrals ∫01eppk−1(1−p)m−kdp. Brualdi's lemma needs a Hall-type argument on the exchange graph; Mathlib has only single-element exchange. Lemma 2.1 also hides a point the paper skips: it is false unless f(∅)=0, so the goal needs a normalisation f↦f−f(∅) that leaves marginals, ℓ and the swap-local optima unchanged.
Formalization scope
Subsets are Finset X over [Fintype X] [DecidableEq X] with X : Type; set functions are Finset X → ℝ, and the paper's codomain R≥0 is a hypothesis ∀ A, 0 ≤ f A. Submodularity is the published definition NonmonotoneSubmod.Shared.Submodular. Total curvature is in the product form above, not the ratio of (1.1), which is undefined when some f∅(j)=0. Matroids are Mathlib's Matroid X, with M.E = Set.univ wherever f and M meet, so that X∖S is complemented in the right set; the dual is M✶. e is Real.exp 1. The bijection of Lemma 5.1 is a function π : X → X with Set.BijOn π A B, and sums over i=1,…,r are sums over a∈A with b=π(a).
Conventions that differ from the page, each disclosed in the item's Formalization Note:
the B=∅ term of h is excluded (on the page it is g(∅)∫01p−1⋯dp, finite only when g(∅)=0);
(5.4), Lemma 5.2 and the §5.1 claim assume g monotone and nonnegative, the setting of Filmus and Ward and of every use in the paper;
Lemma 2.1 adds f(∅)=0, Lemma A.2's nonnegativity adds f(X)=0, and Lemmas A.3 and A.4 take c>0; Lemma A.4 is stated as its proof proves it (supermodular, monotone decreasing).
The goal is about every swap-local optimum of ψ, not about the existence of a good base: "some base satisfies f(S)≥(1−c/e)f(O)" is trivially true by taking S optimal, and is not the theorem.
Welcome contributions: Brualdi's lemma for Mathlib matroids (reusable well beyond this mission), the Beta-integral identities behind h, and the normalisation argument. The polynomial-time algorithm, the sampling estimate of ψ (§5.2), the continuous greedy of §4 and the lower bounds of §7 are out of scope.
Selected references
M. Sviridenko, J. Vondrák, J. Ward, Optimal approximation for submodular and supermodular optimization with bounded curvature, SODA 2015; Math. Oper. Res. 42(4), 2017. https://doi.org/10.1287/moor.2016.0842
Y. Filmus, J. Ward, Monotone submodular maximization over a matroid via non-oblivious local search, SIAM J. Comput. 43(2), 2014. https://doi.org/10.1137/110832318
M. Conforti, G. Cornuéjols, Submodular set functions, matroids and the greedy algorithm: tight worst-case bounds and some generalizations of the Rado–Edmonds theorem, Discrete Appl. Math. 7(3), 1984. https://doi.org/10.1016/0166-218X(84)90003-9
R. A. Brualdi, Comments on bases in dependence structures, Bull. Austral. Math. Soc. 1(2), pp. 161–167, 1969.
G. L. Nemhauser, L. A. Wolsey, Best algorithms for approximating the maximum of a submodular set function, Math. Oper. Res. 3(3), 1978. https://doi.org/10.1287/moor.3.3.177
G. Călinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a monotone submodular function subject to a matroid constraint, SIAM J. Comput. 40(6), 2011. https://doi.org/10.1137/080733991
J. Vondrák, Submodularity and curvature: the optimal algorithm, RIMS Kôkyûroku Bessatsu B23, pp. 253–266, 2010.
Multistage Adaptive Robust Optimization for the Unit Commitment Problem II: Under the W_it-Policy, Robust Generation and Ramping Limits Reduce to the Extreme Total-Load ScenariosResearch Paper
Motivation
Unit commitment (UC) is the daily scheduling problem of electricity system operators: decide which generators are switched on in each hour of the next day, and how much each produces, so that supply meets the net load at minimum cost while respecting generation limits, ramping limits and transmission limits. With growing shares of wind and solar power, the net load is uncertain at the time the commitment is fixed. Adaptive robust UC protects the schedule against every net-load trajectory in an uncertainty set.
Lorca, Sun, Litvinov and Zheng (Oper. Res., 2016) argue that the dispatch must be nonanticipative (the output at hour t may depend only on loads observed up to t) and propose a multistage robust UC model. To make it computable they restrict the dispatch to affine policies of the observed loads, in the spirit of Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 99, 2004). The paper solves the model on the IEEE 118-bus test case and on the 2718-bus Polish system. The two results of this mission are what makes the simplest such policy cheap to solve: under it, the semi-infinite robust constraints on generation, ramping and energy balance collapse to finitely many deterministic constraints.
Setting
There are Ng generators i, Nd load nodes j and periods t∈T={1,…,T}. A net-load trajectory is d=(djt), and its total load in period t is ∑j∈Nddjt. The budget uncertainty set (3) is
with nominal loads dˉ, deviations d^>0 and a conservativeness parameter Γ≥0.
The Wit-policy (10) sets the output of generator i in period t to an affine function of the current total load,
pit(d)=wit+Witj∈Nd∑djt,
and the Wi-policy (9) is the special case in which Wit=Wi does not depend on t. Given commitments xit,uit,vit, output limits pimin,pimax and ramp rates RD,RU,SD,SU, the robust constraints of the affine model (8) require, for all d∈D: generation limits piminxit≤pit(d)≤pimaxxit (8c); ramping limits −RDitxit−SDitvit≤pit(d)−pit−1(d)≤RUitxit−1+SUituit ((8d), (8e)); and energy balance ∑ipit(d)=∑jdjt (8g).
The extreme total-load scenarios are a trajectory dmax∈D whose total load is maximal over D in every period (19), a trajectory dmin∈D whose total load is minimal in every period (20), and the mixed scenarios
Under the Wit-policy (or the Wi-policy), for every generator i and period t:
(8c) over D⟺(8c) over {dmin,dmax},(8d), (8e) at t over D⟺(8d), (8e) at t over {dmin,dmax,dminmax(t),dmaxmin(t)}.
Milestones
Proof of (i) (pp. ec1–ec2): (8c) over D is equivalent to four deterministic inequalities, at the total loads of dmax and dmin.
(23)–(24) (p. 19): because D is a product over periods, the worst case of Wit∑jdjt−Wi,t−1∑jdjt−1 over D is a maximum over Dt minus a minimum over Dt−1.
(25a)–(25d) (p. 19): both the maximum and the minimum of that difference over D are attained in {dmin,dmax,dminmax(t),dmaxmin(t)}.
Companion: Proposition 4
For a full-dimensional uncertainty set, the robust energy balance (8g) holds if and only if ∑iwit=0 and ∑iWit=1 for all t ((15)); for the Wi-policy, ∑iwit=0 and ∑iWi=1 ((14)).
Significance
Proposition 6 removes the constraints (8c)–(8e) from the constraint-generation loop of the affine robust UC: they can be imposed before the algorithm starts, through two scenarios per generation constraint and four per ramping constraint, leaving only the worst-case cost constraint and the transmission constraints to be separated. Proposition 4 turns the semi-infinite energy balance into 2T linear equalities. Together they are the reason the Wit-policy scales to the 2718-bus system in the paper's experiments.
Both results are proved in the paper, and the proofs are short. No machine-checked version is known. The formalization fixes the exact handling of the first period (the initial dispatch pi0), the exact definition of the mixed scenarios, and the dependence of part (ii) on the product structure of D, all of which the paper leaves implicit or states loosely.
Difficulty
Part (i) needs only that the constraint is affine in the scalar total load of one period. Part (ii) is where the obvious argument fails: the ramping constraint couples two periods, and a set that is not a product over periods may not contain a trajectory that is simultaneously maximal in period t and minimal in period t−1. The separability of D is exactly what puts dminmax(t) and dmaxmin(t) in D. The labels the paper attaches to (25a) and (25d) are swapped relative to (21)–(22); following them literally sends the argument to the wrong scenario.
Formalization scope
Representation. Generators, load nodes and periods are Fin Ng, Fin Nd, Fin T; trajectories are Fin T → Fin Nd → ℝ. Periods are 0-based: Lean period t is the paper's period t+1, so "periods 1,…,t−1" in (21)–(22) are the Lean periods s < t.
First period. The dispatch "at t−1" for the first period is the initial dispatch pi0 and xit−1 is the initial status xi0; both are data.
Commitments are arbitrary reals: the results do not use x,u,v∈{0,1}.
Scenarios are hypotheses.dmax and dmin are any members of D with maximal, respectively minimal, total load in every period, never a chosen witness. A formalization in which they are arbitrary trajectories, or in which the four-scenario set is not tied to D, is ruled out: part (ii) is false for it.
Extrema in milestone 2 are taken in EReal, under the standing assumptions Γ≥0, d^>0 that make every Dt nonempty and bounded.
Policies. Everything is stated for the Wit-policy; the Wi-policy is the instance Wit=Wi.
Proposition 4 is stated for a general set with nonempty interior, as on the page, with the added hypothesis Nd≥1: with no load node the statement is false.
The development needs only finite sums, products of sets, and order facts about affine functions; it reuses nothing beyond Mathlib. Proofs of the milestones, the goal and Proposition 4 are welcome.
Selected references
Á. Lorca, X. A. Sun, E. Litvinov, T. Zheng, Multistage adaptive robust optimization for the unit commitment problem, Operations Research, 2016 (manuscript of September 29, 2014). https://doi.org/10.1287/opre.2015.1456
A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99:351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
D. Bertsimas, E. Litvinov, X. A. Sun, J. Zhao, T. Zheng, Adaptive robust optimization for the security constrained unit commitment problem, IEEE Transactions on Power Systems 28(1):52–63, 2013. https://doi.org/10.1109/TPWRS.2012.2205021
Learning in Games via Reinforcement and Regularization 1: Under Regularized Reinforcement Learning, Every Iteratively Dominated Strategy Becomes ExtinctResearch Paper
Motivation
A basic test of any model of learning in games is whether it respects strict dominance: a strategy that does worse than another against every behaviour of the opponents should eventually be abandoned, and, after it is gone, so should every strategy that becomes dominated in what remains. For the replicator dynamics of evolutionary game theory this is classical: elimination of dominated and iteratively dominated strategies goes back to Akin (1980), Nachbar (1990) and Samuelson and Zhang (1992), whose notion of extinction of a mixed strategy is the one used here; Weibull (1995) gives the textbook account, including a conditional result for weakly dominated strategies.
The replicator dynamics are the continuous-time limit of exponential weights (the logit choice rule), one member of a large family of learning schemes in which every player accumulates the payoffs of their strategies into a score and turns scores into mixed strategies by a regularized best response. Different regularizers give different dynamics: the Gibbs entropy gives the replicator dynamics, the Euclidean square gives the projection dynamics, and many others are used in online optimization. Mertikopoulos and Sandholm (arXiv:1407.6267, Mathematics of Operations Research 41(4), 2016) analyse this whole family in a single framework. In particular they do not assume that the regularizer is steep, so play can reach the boundary of the simplex in finite time and the induced dynamics on the simplex can fail to be well-posed. Their first rationality result is that every iteratively dominated strategy becomes extinct under every scheme of the family.
Setting
A finite game has a finite set of players N, a finite set Ak of pure strategies for each player k, and payoffs uk:∏ℓAℓ→R. A mixed strategy of player k is a point xk of the simplex Xk=Δ(Ak), and uk(x) is the expected payoff (2.1) at a mixed profile x=(xk)k. The payoff vector of player k is vk(x)=(vkα(x))α∈Ak, where vkα(x)=uk(α;x−k) is the payoff of the pure strategy α against x−k.
A penalty function on a simplex Δ (Definition 2.1) is a function h:Δ→R that is continuous, smooth on the relative interior of every face of Δ, and strongly convex with some constant K>0:
Its choice map is Q(y)=argmaxx∈Δ{⟨y∣x⟩−h(x)} (Definition 2.2). Each player k has a penalty function hk and choice map Qk. The reinforcement learning dynamics are
y˙k=vk(x),xk=Qk(yk),(RL)
so that yk(t) is the cumulative payoff of player k's pure strategies and x(t)=Q(y(t)) is the resulting play. Strategy pk is dominated by pk′, written pk≺pk′, if uk(pk;x−k)<uk(pk′;x−k) for all x (4.1). Removing dominated strategies and repeating gives the iteratively dominated strategies. A mixed strategy pkbecomes extinct along x(t) if min{xkα(t):α∈supp(pk)}→0.
The analysis runs through the Fenchel couplingFh(p,y)=h(p)+h∗(y)−⟨y∣p⟩, where h∗(y)=maxx∈Δ{⟨y∣x⟩−h(x)}, and the Bregman divergenceDh(p,x)=h(p)−h(x)−h′(x;p−x), defined with the one-sided directional derivative so that it makes sense at boundary points where h has no gradient.
Formalization targets
Goal: Theorem 4.1
For every orbit x(t)=Q(y(t)) of (RL), every player k, and every mixed strategy pk that is dominated, possibly only after some rounds of elimination,
t→∞limmin{xkα(t):α∈supp(pk)}=0.
The penalty functions are arbitrary in the sense of Definition 2.1, including non-steep ones, and may differ across players.
Milestones
Proposition C.3: Fh(p,y)≥21K∥Q(y)−p∥2, hence Fh≥0, and Fh(p,yj)→0 iff Q(yj)→p.
(4.6)–(4.8): if pk≺pk′ with payoff gap at least δ, then Fk(pk,yk(t))≥Vk(yk(0))+δt.
Proposition C.2 (i)–(iii): Dh(p,⋅) is finite, at least 21K∥x−p∥2, and continuous on Δp={x∈Δ:xα>0 whenever pα>0}.
(C.11): Fh(p,y)=Dh(p,Q(y)) whenever Q(y)∈Δp.
Proposition C.4: if Fh(p,yj)→+∞, then Q(yj) has no limit point in Δp.
Theorem 4.1 for strategies dominated in the original game.
Two companion statements extend the goal: Proposition 4.2, the rate xkα(t)≤φk(ck−γkδkt) under the rescaled dynamics (RLγ) with decomposable penalties, which gives extinction in finite time when the kernel is not steep at 0; and Proposition 4.3, a conditional extinction result for weakly dominated strategies.
Significance
The theorem shows that elimination of iteratively dominated strategies is a property of the whole class of regularized reinforcement learning schemes, not only of exponential weights. It is also unilateral: a player who follows (RL) stops playing dominated strategies whatever the other players do (Remark 4.2). The proof does not use the dynamics induced on the simplex, which need not be well-posed for non-steep regularizers; it works with the scores in the dual space. Proposition 4.2 then shows that the regularizer sets the speed of elimination: exponential for the entropy, finite time for the Euclidean square.
The result is proved in the paper; nothing here is open. No part of it is formalized. The mission produces the paper's convex-analytic toolkit for penalty functions on a simplex (Fenchel coupling, the one-sided Bregman divergence, their comparison with the Euclidean distance) and a machine-checked proof of the elimination theorem on top of it. The same toolkit is used by the paper's results on strict equilibria and zero-sum games.
Difficulty
The familiar argument for the replicator dynamics shows that the Kullback–Leibler divergence DKL(pk,xk(t)) diverges. For a general penalty function the analogous Bregman divergence uses dh(x), which does not exist at boundary points, and non-steep dynamics spend time on the boundary. The proof therefore tracks the Fenchel coupling Fk(pk,yk(t)), whose growth is easy to bound, and must convert its divergence into extinction. That conversion (Propositions C.2–C.4) needs continuity of the one-sided Bregman divergence on Δp, including at points of lower-dimensional faces, and a compactness argument that turns "no limit point in Δp" into a statement about every time sequence. The iterated case adds an induction in which the payoff gap is only positive on the surviving profiles, so the trajectory's distance to those profiles must be controlled.
Formalization scope
Lean conventions:
Players form a Fintype ι; strategies are Fintype (A k); payoffs are u : ι → (∀ k, A k) → ℝ. Mixed strategies, mixed profiles and expected payoffs are those of the published agt_games definition.
A penalty function is IsPenalty h K: continuity on the simplex, C∞ along smooth curves in the relative interior of a face (footnote 5), and (2.5) with the Euclidean norm. Steepness is not assumed.
The choice map is the predicate IsChoice h y x (x maximizes ⟨y∣⋅⟩−h on the simplex), never a chosen maximizer.
An orbit of (RL) is a pair of trajectories (y,x) with xk(t)=Qk(yk(t)) and y˙kα(t)=vkα(x(t)) for t≥0 (right derivative at 0). This is the differential form of the paper's integral equation and is equivalent to it along continuous orbits.
Iterated dominance eliminates pure strategies round by round, each time removing those strictly dominated by a mixed strategy supported on the survivors, against profiles supported on the survivors. A mixed strategy is iteratively dominated when it is dominated in this sense at some round.
Extinction is stated as a limit: for every ε>0 there is T such that for every t≥T some α∈supp(pk) has xkα(t)<ε.
The one-sided Bregman divergence is handled through a predicate asserting that the one-sided derivative is a given real number. The value +∞ is never encoded as a real number.
Trivializing formalizations are ruled out. Orbits are not vacuous: a sorry-free check exhibits an explicit orbit of a game with a strictly dominated action, under the quadratic penalty. The choice map is not a junk argmax. Steepness, which would keep play interior, is not added. Extinction is not weakened to a liminf.
Needed infrastructure: properties of strongly convex functions on a simplex, the conjugate and its maximizers, one-sided derivatives of convex functions along segments, and compactness of the product of simplices. Most of this is reusable beyond the mission. Contributions are welcome on the Appendix-C lemmas, which are independent of the game, as well as on the goal.
Selected references
P. Mertikopoulos and W. H. Sandholm, Learning in games via reinforcement and regularization, Mathematics of Operations Research 41(4), 2016; preprint arXiv:1407.6267v2. https://arxiv.org/abs/1407.6267
E. Akin, Domination or equilibrium, Mathematical Biosciences 50, 239–250, 1980.
J. H. Nachbar, Evolutionary selection dynamics in games, International Journal of Game Theory 19, 59–89, 1990.
L. Samuelson and J. Zhang, Evolutionary stability in asymmetric games, Journal of Economic Theory 57, 363–391, 1992.
J. W. Weibull, Evolutionary Game Theory, MIT Press, 1995.
K. C. Kiwiel, Free-steering relaxation methods for problems with strictly convex costs and linear constraints, Mathematics of Operations Research 22(2), 326–349, 1997.
EXTRA: An Exact First-Order Algorithm for Decentralized Consensus Optimization 2: If g Is Restricted Strongly Convex and α < 2μ_g λmin(W̃)/L_f², ‖z^k − z*‖²_G Converges Q-Linearly to 0Research Paper
Decentralized consensus optimization
In decentralized consensus optimization, n agents connected by a communication network cooperatively solve
x∈Rpminfˉ(x)=n1i=1∑nfi(x),
where agent i privately holds the convex function fi and may only exchange vectors with its neighbours. The model covers distributed estimation and learning over sensor networks, multi-agent control and decentralized machine learning, where no agent may collect all the data. The classical method, decentralized gradient descent (DGD), lets every agent average its neighbours' iterates and take a local gradient step. With a fixed step size DGD stalls at a neighbourhood of the solution whose size is proportional to the step, so exact convergence requires diminishing steps and is slow.
Shi, Ling, Wu and Yin (arXiv:1404.6264; SIAM J. Optim. 25 (2015)) introduced EXTRA, an "exact first-order algorithm" that keeps a fixed step size and still converges to the exact solution. This mission formalizes the second main result of that paper: under restricted strong convexity, EXTRA converges linearly. The companion mission of the series covers the sublinear rates for general convex objectives.
Setting
Agent i keeps a local copy x(i)∈Rp; the stacked variablex∈Rn×p has these copies as rows, with Frobenius inner product ⟨x,y⟩F=∑i⟨x(i),y(i)⟩. Write f(x)=∑ifi(x(i)), let ∇f(x) be the matrix with rows ∇fi(x(i)), and for a symmetric matrix M let ∥x∥M2=trace(xTMx).
Two symmetric mixing matricesW,W~∈Rn×n satisfy Assumption 1: their off-diagonal entries vanish between non-neighbours of a connected graph; null{W−W~}=span{1} and W~1=1; and W~≻0, 2I+W⪰W~⪰W. Each fi is convex with Lf-Lipschitz gradient (Assumption 2), and the problem has a solution x∗ (Assumption 3). With step size α>0, EXTRA is
Each agent uses only its own gradient and its neighbours' iterates.
The analysis uses U=(W~−W)1/2, the auxiliary sequence qk=∑t=0kUxt, an optimal pair (q∗,x∗) with x∗=1(x∗)T, q∗=Up, Uq∗+α∇f(x∗)=0, and the stacked pair zk=(qk;xk), z∗=(q∗;x∗) measured in ∥z∥G2=∥q∥F2+∥x∥W~2.
A gradient map ∇h is restricted strongly convex with respect to x~ with constant μ>0 if ⟨∇h(x)−∇h(x~),x−x~⟩≥μ∥x−x~∥2 for all x. The condition is imposed on the penalized function
g(x)=f(x)+4α1∥x∥W~−W2,∇g(x)=∇f(x)+2α1(W~−W)x.
Formalization targets
Goal: Theorem 3.7 (p. 15)
If g is restricted strongly convex with respect to x∗ with constant μg>0 and α<2μgλmin(W~)/Lf2, then there is δ>0 such that for all k
∥zk−z∗∥G2≥(1+δ)∥zk+1−z∗∥G2,
and consequently ∥xk−x∗∥W~2=O((1+δ)−k). The goal asserts the existence of a contraction factor, not a particular value of δ, so it survives any improvement of the constants.
Milestones
the summed form (3.5) of EXTRA and Lemma 3.2, the error recursion
the descent inequality (3.29), for every tunable η>0;
the dual bound (3.35), controlling ∥qk+1−q∗∥F2 by primal quantities through σmax and the smallest nonzero eigenvalue λ~min(W~−W);
the critical inequality (3.30) for every δ below the explicit minimum (3.38), under η∈(0,2μg) and αLf2<ηλmin(W~) (3.39).
A companion item states Proposition 3.6: fˉ is restricted strongly convex at x∗ if and only if g is at 1(x∗)T.
Significance
Theorem 3.7 is what separates EXTRA from DGD: a fixed step size gives linear convergence to the exact solution, with the strong convexity requirement placed on g, not on the individual fi (Remark 1). By Proposition 3.6 this is the same as restricted strong convexity of the global objective fˉ, so agents with merely convex local losses still converge linearly. EXTRA is an early member of the family of exact decentralized methods (gradient tracking, NIDS, exact diffusion), whose linear-rate analyses use Lyapunov functions of the same primal–dual type.
The result is proved in the paper. Neither it nor any other decentralized optimization rate is formalized in Mathlib or on the platform. A formal development would produce a reusable layer for stacked variables, Frobenius geometry, matrix-weighted norms and mixing-matrix assumptions, on which other decentralized algorithms could be stated.
Difficulty
The obvious Lyapunov function ∥xk−x∗∥2 does not contract: EXTRA is a primal–dual method in disguise, and the primal error alone can increase. The contraction holds only for the joint quantity ∥zk−z∗∥G2, and the descent inequality (3.29) controls only the primal part of ∥zk+1−z∗∥G2. The dual error qk+1−q∗ must be bounded separately. That bound (3.35) works only because qk+1−q∗ lies in the range of W~−W, where W~−W is invertible with smallest nonzero eigenvalue λ~min. Restricted strong convexity of g also gives curvature only toward the single point x∗, not between arbitrary pairs.
Formalization scope
Stacked variables are Fin n → EuclideanSpace ℝ (Fin p). The sup norm Lean puts on this type is never used: Frobenius quantities go through an explicit inner product frob, and ∥x∥M2 is the quadratic form frob x (mix M x), also for indefinite M as in (3.29). λmin, λmax, λ~min and σmax are pinned by their characterisations (an eigenvalue that is extreme among all eigenvalues). U is any symmetric positive semidefinite matrix with U2=W~−W. Assumptions 1–3 are standing hypotheses of every item except Proposition 3.6, which assumes only Assumptions 1 and 2, as printed. Assumption 2 uses one common Lipschitz constant Lf. The step-size conditions are multiplied out (αLf2<2μgλmin(W~)), so that Lf=0 is not turned into α<0 by Lean's x/0=0. The gradients of fˉ and g are written as explicit formulas.
The goal does not mention η, θ, the minimum (3.38) or (3.30). A version assuming those intermediate inequalities would be trivial, and so would one with a free δ allowed to depend on k. The printed "In addition" sentence of Proposition 3.6 (μg≥μfˉ) is false; the companion item states the direction proved in Appendix A.
The infrastructure needed is: Frobenius inner products of stacked variables, quadratic-form bounds by extreme eigenvalues, the range/nullspace argument for symmetric positive semidefinite matrices, and the elementary inequality ∥a+b∥2≤θ∥a∥2+θ−1θ∥b∥2. Proofs of any milestone, and reusable lemmas on matrix-weighted norms, are welcome.
Selected references
W. Shi, Q. Ling, G. Wu, W. Yin, EXTRA: An Exact First-Order Algorithm for Decentralized Consensus Optimization, SIAM J. Optim. 25(2) (2015) 944–966; arXiv:1404.6264v4. https://arxiv.org/abs/1404.6264
A. Nedić, A. Ozdaglar, Distributed Subgradient Methods for Multi-Agent Optimization, IEEE Trans. Automat. Control 54(1) (2009) 48–61. https://doi.org/10.1109/TAC.2008.2009515
K. Yuan, Q. Ling, W. Yin, On the Convergence of Decentralized Gradient Descent, SIAM J. Optim. 26(3) (2016) 1835–1854; arXiv:1310.7063. https://arxiv.org/abs/1310.7063
M.-J. Lai, W. Yin, Augmented ℓ1 and Nuclear-Norm Models with a Globally Linearly Convergent Algorithm, SIAM J. Imaging Sci. 6(2) (2013) 1059–1091 (the source of the restricted strong convexity notion). https://doi.org/10.1137/120863290