Quantum algorithms for optimizers 2: Simon's algorithm: n+t uniform samples orthogonal to a contain n−1 independent vectors with probability ≥ 1 − 2^{−(t+1)}Textbook
Motivation
This mission develops Chapter 2 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.
Setting and conventions
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Chapter goal
This is the sampling bound behind the classical post-processing of Simon's algorithm.
Let n≥1 and t≥0 be integers, and let F2={0,1} be the field with two elements. Fix a nonzero vector a∈F2n and let
Va={k∈F2n:k⋅a=∑i=1nkiai≡0(mod2)}
be the (n−1)-dimensional subspace of vectors orthogonal to a. Draw k(1),…,k(n+t) independently and uniformly at random from Va. Then
Pr[some n−1 of k(1),…,k(n+t) are linearly independent over F2]≥1−2t+11.
The bound does not depend on n, so n+O(1) runs of Simon's circuit suffice to determine the hidden string a with high probability.
Formalization Note The probability is the fraction of all ∣Va∣n+t tuples (k(1),…,k(n+t))∈Van+t for which there are n−1 distinct indices whose vectors are linearly independent; vectors of F2n are functions Finn→Z/2Z.
Significance
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Supporting targets
Proposition 2.8: Simon's algorithm: n+t uniform samples orthogonal to a contain n−1 independent vectors with probability ≥ 1 − 2^{−(t+1)}.
Formalization scope
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
The secretary problem is the standard example of an optimal stopping problem with partial information. It is also known as the marriage problem, the sultan's dowry problem, the fussy suitor problem, the googol game and the best choice problem. It is studied in applied probability, statistics and decision theory. Its solution is often called the 37% rule: a simple rule picks the single best of n applicants with probability about 1/e≈0.368, whether there are 100 or 100 million applicants (Wikipedia: Secretary problem). The problem is a standard example of the exploration–exploitation dilemma.
Timeline (as recounted in the Wikipedia article's History section, following Ferguson 1989):
1949: Merrill M. Flood introduces the problem (as the "fiancée problem") in a lecture. It then spreads as folklore through the 1950s.
1958: Flood circulates a letter outlining a proof of the optimal strategy. Its appendix by R. Palermo proves that every strategy is dominated by one of the form "reject the first p unconditionally, then accept the next candidate who is better".
1960: First publication, in Martin Gardner's Scientific American column (February 1960), with the analysis supplied by Leo Moser and J. R. Pounder.
1966: Gilbert and Mosteller, "Recognizing the maximum of a sequence", a detailed study of the problem and many variants.
1989: Ferguson, "Who solved the secretary problem?", a historical survey.
2000: Bruss's odds theorem, which the article calls the shortest rigorous proof known.
Setting
There is a single position and there are n applicants, where n is known. If seen together, the applicants can be ranked from best to worst with no ties. They are interviewed one at a time in a uniformly random order: each of the n! orders is equally likely. Right after each interview the applicant is either accepted, which ends the process, or rejected for good. The decision may depend only on the relative ranks of the applicants interviewed so far. The objective is to maximize the probability of selecting the best applicant of the whole group.
An order is a permutation σ of {0,…,n−1}. The applicant interviewed at time i has quality σ(i), where larger means better. The relative rank of the applicant interviewed at time j is the number of applicants interviewed before time j who are worse than them. A stopping rules maps the list of relative ranks observed so far to "accept" or "reject". Its success probabilityPn(s) is the fraction of the n! orders on which the applicant accepted by s is the overall best. A rule that never accepts anyone fails. The optimal success probability is
Vn=ssupPn(s).
A candidate is an applicant who is better than every applicant interviewed before them. The cutoff rule with cutoff r rejects the first r−1 applicants and then accepts the first candidate after that point.
Formalization targets
Goal: the 37% rule
n→∞limVn=e1.
Milestones (following the article's derivation)
Pn(cutoff 1)=1/n.
For 2≤r≤n: Pn(cutoff r)=nr−1i=r∑ni−11.
Some cutoff rule with 1≤r≤n is optimal among all rank-based stopping rules.
The table of optimal cutoffs and optimal success probabilities for n=1,…,10.
If rn/n→x∈[0,1], then Pn(cutoff rn)→x∫x1tdt=−xlogx.
On [0,1] the function −xlogx has maximum value 1/e, attained only at x=1/e.
Optimal cutoffs satisfy rn/n→1/e.
Vn≥1/e for every n≥1.
Significance
The result. The 37% rule is the classical result of optimal stopping. It shows that a fixed fraction of the best possible success probability survives as the number of options grows without bound, and that a simple threshold policy achieves it. The structure of its solution has three parts: optimal rules may be taken to be threshold rules, there is an exact formula in terms of the records of a uniformly random permutation, and a limit turns a harmonic sum into an integral. This structure recurs throughout the best-choice literature, including the prophet-secretary and multi-choice secretary problems.
Formalizing it. The result has been proved since the late 1950s and early 1960s. The remaining work is to formalize the known proof: a model of rank-based stopping rules over uniformly random permutations, the exact success probability of cutoff rules, the optimality of cutoff rules among all rank-based rules, and the asymptotics.
Difficulty
The success probability of a fixed cutoff rule and the calculus limit are elementary. The central step is the optimality of cutoff rules (Milestone 3). A stopping rule may depend arbitrarily on the whole history of relative ranks, and one has to show that no such rule beats the best cutoff rule. Evaluating cutoff rules alone does not prove the goal, because Vn is a supremum over all rank-based rules. A second, smaller difficulty is that the limit statements need control of the harmonic sums along a varying cutoff rn, not only along a fixed ratio.
Formalization scope
The sample space is the finite set Equiv.Perm (Fin n) with uniform weights. successProb n s is the ratio (number of winning permutations) / n! in R.
A stopping rule is a deterministic function List ℕ → Bool, applied to the list of relative ranks observed so far. Through the length of the list it also knows the current time. It never sees absolute qualities. Randomized rules are not modelled. A randomized rule is a mixture of deterministic ones, so it cannot do better.
optimalProb n is the real supremum of successProb n s over all such rules. The values lie in [0,1], so the supremum is the usual least upper bound.
Times are 0-based in Lean (Fin n). Cutoffs r are 1-based, as in the article: cutoffRule r accepts at time i exactly when i+1≥r and the current applicant is a candidate.
1/e is written Real.exp (-1).
The 1/e-law of best choice (unknown number of applicants, Bruss 1984), the odds algorithm, cardinal-payoff variants and the other generalizations in the article are outside this mission.
All declarations live in the namespace ClassicalSecretary. Reusable contributions are welcome, in particular facts about records of uniformly random permutations (independence of relative ranks, the probability that position i is a record) and a backward-induction principle for finite-horizon stopping problems.
J. Gilbert, F. Mosteller, Recognizing the maximum of a sequence, Journal of the American Statistical Association 61(313), 35–73, 1966. https://doi.org/10.2307/2283044
Stochastic Dual Dynamic Integer Programming 3: The Convex Lower Envelope of a Function on {0,1}^n Is Piecewise Linear and Agrees with It at Every Binary PointResearch Paper
Motivation
Multistage stochastic integer programs model sequential decisions under uncertainty in which some decisions are discrete: unit commitment in power systems, capacity expansion, production planning with setups. The standard decomposition methods for multistage stochastic linear programs, nested Benders decomposition and stochastic dual dynamic programming (SDDP), approximate each stage's expected cost-to-go function from below by finitely many affine cuts. This works because those functions are convex and polyhedral. With integer variables the cost-to-go functions are in general nonconvex, and no family of affine cuts can be exact at every evaluated state.
Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) observe that the obstruction disappears when the state variables passed between stages are binary. Their Theorem 1 (p. 467) states that every real function of binary variables is represented exactly, at all binary points, by a convex polyhedral function on the unit cube. This is the structural fact on which their stochastic dual dynamic integer programming (SDDiP) algorithm rests: the cost-to-go function only ever needs to be evaluated at binary states, and there a convex piecewise linear under-approximation can be tight. Mixed integer states are reduced to binary ones by binary expansion (§5 of the paper).
Setting
Let n≥0 and write {0,1}n⊆Rn for the binary points, the vectors each of whose coordinates is 0 or 1, and Cn=[0,1]n for the unit cube. Let f be a real valued function defined on {0,1}n.
For a set X in a real vector space and f:X→R, a convex underestimator of f is a function h that is convex on the convex hull conv(X) and satisfies h(x)≤f(x) for every x∈X (Definition 3, p. 496). The largest convex underestimator of f on conv(X), that is, a convex underestimator e with h≤e on conv(X) for every convex underestimator h, is the convex lower envelope of f. In this mission X={0,1}n.
A function e is convex piecewise linear with finitely many linear pieces on Cn if there are α1,…,αK∈Rn and β1,…,βK∈R with e(x)=maxk(αk⊤x+βk) for all x∈Cn.
The proof works with the polyhedron of affine minorants of f,
Π={(α,β)∈Rn×R:α⊤x+β≤f(x) for all x∈{0,1}n},
the function g(x)=max(α,β)∈Π{α⊤x+β}, and the linear program (P) defining g(x) together with its dual
(D)mini=1∑Nf(x^i)λis.t.X^λ=x,e⊤λ=1,λ≥0,
where X^=[x^1,…,x^N] lists the N=2n binary vectors.
Formalization targets
Goal: Theorem 1 (p. 467)
f has a convex lower envelope, and every convex lower envelope e of f satisfies
e is convex on [0,1]n,e(x)=k=1,…,Kmax(αk⊤x+βk)(x∈[0,1]n),e(x)=f(x)(x∈{0,1}n)
for some finite family of affine functions.
Milestones (proof of Theorem 1, p. 496)
conv({0,1}n)=[0,1]n.
For x∈[0,1]n, (P) and (D) both attain their optima, with common value g(x); in particular g(x)<∞.
g(x)=f(x) for every x∈{0,1}n.
g is convex on [0,1]n and is there the maximum of finitely many affine functions whose coefficients are extreme points of Π.
h(x)≤g(x) for every x∈[0,1]n and every convex underestimator h of f.
Significance
The result. Theorem 1 is what makes exact cutting-plane approximation possible for nonconvex value functions of binary states. In SDDiP, the expected cost-to-go function of each node is approximated from below by affine cuts; Theorem 1 guarantees that a convex polyhedral function exists that agrees with the true value function at every binary state, so a finite collection of valid cuts can be tight at every state the algorithm visits. Without it, the finite convergence of SDDiP to an optimal policy (Theorem 2 of the paper, with Lagrangian cuts from Theorem 3) would have no target to converge to. The statement fails for general finite sets in place of {0,1}n: on {0,1,2}⊆R with f(1)>(f(0)+f(2))/2, no convex underestimator reaches f(1).
Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization produces the identity conv({0,1}n)=[0,1]n, a finite-dimensional LP duality statement for the pair (P)–(D), and a characterization of the convex lower envelope on the cube, each of independent use for later formalizations of binary and mixed integer programming (Lagrangian relaxations, convex closures, extended formulations).
Difficulty
Two steps carry the weight. The first is that the maximum defining g is attained, with finitely many pieces coming from extreme points of the unbounded polyhedron Π: this needs LP duality and the existence of an optimal vertex for a pointed polyhedron, neither of which is a one-line consequence of Mathlib's convexity library. The second is the domination step. The printed argument handles interior points of the cube by writing a convex underestimator as a supremum of affine minorants, and binary points separately; the remaining boundary points of [0,1]n (for example (1/2,0) when n=2) are covered by the paper's conclusion but not by those two cases, and require an argument that works on all of conv({0,1}n). Exactness at binary points uses that a binary point is not a nontrivial convex combination of other points of the cube.
Formalization scope
Points of Rn are Fin n → ℝ with the componentwise order; Cn is Set.Icc 0 1, the binary points are the vectors with every coordinate 0 or 1, and α⊤x is the dot product. f is a total function on Rn of which only the values at binary points enter any statement. Convexity of an underestimator is required on conv({0,1}n), exactly as in Definition 3, not on all of Rn; the identification of this hull with [0,1]n is milestone 1, not a definition. The value n=0 is allowed and no hypothesis on n is added.
The readings of informal words are: "the convex lower envelope" is a predicate (largest convex underestimator on conv(X)), so Theorem 1 asserts its existence and then its properties for every function satisfying it; "convex piecewise linear with a finite number of linear pieces" is "the maximum of finitely many affine functions on the cube"; "max" over Π is an attained maximum, stated with IsGreatest; "min" in (D) is stated with IsLeast. The proof's function g is a real supremum, used only after its attainment is proved.
The convex lower envelope is not defined as g (or as the value of (D)): under that definition convexity and piecewise linearity would be unfoldings, and Theorem 1's content, that the largest convex underestimator of Definition 3 has this form and is exact at binary points, would be lost.
A complete development needs: convex hulls of finite sets in Rn, LP duality for a finite system of inequalities, extreme points of polyhedra and attainment of linear maxima at them, and Jensen's inequality for finite convex combinations. The cube identity and the LP duality milestone are reusable beyond this mission. Proofs of individual milestones, alternative proofs of Theorem 1 that bypass LP duality, and generalizations of the definitions are welcome.
Selected references
J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Mathematical Programming, Ser. A 175 (2019) 461–502. https://doi.org/10.1007/s10107-018-1249-5
M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52 (1991) 359–375. https://doi.org/10.1007/BF01582895
Stochastic Dual Dynamic Integer Programming 2: Lagrangian Cuts from the Local-Copy Reformulation Are Valid and Tight at Binary StatesResearch Paper
Motivation
Multistage stochastic integer programs model sequential decisions under uncertainty in which some decisions are discrete: unit commitment in power systems, capacity expansion, production planning with setups. Their linear (continuous) counterparts are routinely solved by nested decomposition methods such as stochastic dual dynamic programming (SDDP; Pereira and Pinto, 1991), which approximate each node's expected cost-to-go function from below by a maximum of linear cuts. With integer variables the cost-to-go functions are no longer convex, and cuts from linear programming duality are in general not exact at the points where they are generated.
Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) restrict the state variables passed between stages to be binary and introduce a local copy zn of the parent's state at every node. Dualizing only the copy constraint zn=xa(n) gives a class of cuts, the Lagrangian cuts, which the authors call "one of the major results of the paper" (p. 478). Their Theorem 3 shows that these cuts are valid (they never overestimate the true value function) and tight (they reproduce the current approximate value at the binary state where they are generated). Together with finiteness, these are the sufficient conditions of the paper's Definition 2 under which SND and SDDiP find an optimal solution in finitely many iterations with probability one (Theorem 2 of the paper, the subject of a companion mission).
Setting
Fix a node n of the scenario tree and an iteration i of the algorithm. The node has:
a nodal constraint setXn⊆Rd×Rd×Rℓ of triples (zn,xn,yn), where xn is the node's state, yn its local variables and zn the local copy of the parent's state. By assumption (A1)Xn is nonempty, compact and mixed integer polyhedral: the points of a polyhedron {w:Aw≥b} with some coordinates integer;
a linear objective fn(xn,yn)=c⊤xn+e⊤yn;
children m∈C(n) with conditional probabilities qnm≥0, a lower bound Ln, and the children's cut coefficients (vmℓ,πmℓ) for ℓ=1,…,i.
Let Xn′={(z,x,y)∈Xn:x∈{0,1}d,z∈[0,1]d} and let Xn′′ add a variable θ≥Ln that dominates every aggregated cut. The Lagrangian function and Lagrangian dual (4.3)–(4.4) are
An optimal π^ and v^=Lni(π^) define the Lagrangian cut θ≥v^+π^⊤xa(n). Given true value functions Qm of the children and Qn=∑mqnmQm, the true nodal value (2.3) is Qn(xa)=min{fn(x,y)+Qn(x):(z,x,y)∈Xn,z=xa,x∈{0,1}d}.
Formalization targets
Goal: Theorem 3 at one node
For binary x^∈{0,1}d and π^ optimal for (Rni):
v^+π^⊤x^=Qni(x^,ψni+1)(tightness, (3.5)),
and, if the children's cuts are valid for Qm on {0,1}d and Qn≥Ln there,
Qn(xa)≥v^+π^⊤xafor all xa∈{0,1}d(validity, (3.4)).
The paper's statement for the whole collection of cuts of an iteration follows by applying this at every sampled node from the last stage backwards, exactly as its proof does by induction.
Milestones
(4.5): v^+π^⊤x^=min{fn+θ:(z,x,y,θ)∈conv(Xn′′),z=x^}, for any parent state at which (Rni) has an optimal solution.
Binary face: for binary x^, conv(Xn′′)∩{z=x^}=conv(Xn′′∩{z=x^}).
Tightness (display after (4.5)).
Validity, base case: at a last-stage node, Qn(xa)≥Lni(π)+π⊤xa.
Validity, induction step ((4.6) and the display after it).
Significance
Tightness at binary states is what separates Lagrangian cuts from the cuts of continuous relaxations or of a direct Lagrangian relaxation of the constraints coupling stages: the paper's Example 2 shows a direct relaxation whose cut is not tight even at a binary state, and Example 1 shows that with a non-binary state the duality gap is positive. With valid, tight and finite cuts, SND and SDDiP become exact algorithms for multistage stochastic integer programs with binary states, and through binarization they approximate problems with general mixed-integer states.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it requires a Lean statement of Geoffrion's theorem for this nodal problem (Lagrangian duality equals optimization over the convex hull of a mixed integer set), which is of independent use for integer programming, and the binary-face fact for sets inside the unit cube.
Difficulty
The validity half is weak duality and is short. The difficulty is in tightness. Step (4.5) is a strong duality statement for a nonconvex set: it needs that the convex hull of Xn′′ is a polyhedron, which follows only because Xn is compact and mixed integer polyhedral (so Xn′ is a finite union of polytopes), and then linear programming duality with attainment over that polyhedron. Neither the polyhedrality of convex hulls of finite unions of polytopes with a common recession direction nor finite-dimensional LP strong duality in the needed form is readily available in Mathlib. A tempting shortcut, Lagrangian duality from convex analysis with a Slater point, does not apply: a binary x^ lies on the boundary of the projection of conv(Xn′′) onto z, so the constraint qualification fails and polyhedrality is genuinely needed.
Formalization scope
States, copies and multipliers are vectors in Rd (Fin d → ℝ); a state is binary when each coordinate is 0 or 1. Points of Xn′′ are tuples (z, x, y, θ). Assumption (A1) is three fields of the node structure (nonempty, compact, mixed integer polyhedral after concatenating coordinates). Cuts are indexed by Fin i and children by Fin nC; probabilities are only required to be nonnegative. A last-stage node is nC = 0 with L = 0. The constraint z∈[0,1]d (2.1c) is kept in Xn′ and folded into Xn in (2.3) and (3.1), as in the paper.
Readings of informal words:
"min" in ψni+1, Lni, Qni, Qn: the definitions use sInf of the set of objective values, and every theorem states the minimum as an attained least element (IsLeast) or as a lower bound over all feasible points, so no junk value of sInf on an empty or unbounded set is used. The hypothesis Xn′′=∅ makes Lni a genuine minimum.
"π^ optimal for (4.3)": maximizes π↦Lni(π)+π⊤x^ over all of Rd.
"the cuts are valid": Qn(xa)≥v^+π^⊤xa is stated as a lower bound over every feasible point of (2.3), which is the paper's convention Qn=+∞ on infeasible states.
The induction hypothesis of the validity proof is made explicit: all children's cuts ℓ=1,…,i are valid, and Qn≥Ln on binary states.
Tightness is stated with ψni+1; the proof's last line writes ψni, a misprint.
A trivializing formalization is ruled out: Qni is the primal value of the forward problem (3.1) with ψni+1 from (3.2) and is never defined through the dual, and validity is required at every binary xa, not only at x^.
A complete development needs: polyhedrality of convex hulls of bounded mixed integer sets, LP strong duality with attainment (or Geoffrion's theorem directly), Carathéodory-type reasoning in product spaces, and the fact that a binary point which is a positive convex combination of points of [0,1]d equals each of them. The first two are reusable well beyond this mission. Proofs of individual milestones are welcome independently; the validity milestones are accessible first.
A. M. Geoffrion, Lagrangean relaxation for integer programming, Math. Program. Study 2 (1974) 82–114. https://doi.org/10.1007/BFb0120690
M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52 (1991) 359–375. https://doi.org/10.1007/BF01582895
Strict Constraint Qualifications and Sequential Optimality Conditions for Constrained Optimization III: SAKKT-Regularity Is the Weakest Strict Constraint Qualification for SAKKTResearch Paper
Motivation
Algorithms for smooth constrained optimization stop when an approximate optimality test passes. The tests used in practice are sequential optimality conditions: properties of a sequence of iterates xk→x∗ rather than of the limit point alone. Every local minimizer satisfies them, with or without a constraint qualification. The price is that a point passing such a test need not satisfy the Karush–Kuhn–Tucker (KKT) conditions. A strict constraint qualification for a sequential condition S is a property of the constraints at x∗ under which S implies KKT for every objective function. The weaker this property, the larger the class of problems on which the condition certifies KKT points.
The Strong Approximate KKT (SAKKT) condition of Haeser and Schuverdt (J. Optim. Theory Appl. 149(3), 2011) asks for approximate Lagrange multipliers whose inequality part vanishes on every constraint that is strictly satisfied at the current iterate. It strictly implies the Approximate KKT condition (AKKT). Haeser and Schuverdt also showed that SAKKT is equivalent to the Approximate Gradient Projection condition AGP(0) of Martínez and Svaiter (2003). Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) determined the weakest strict constraint qualification associated with each of AGP, CAKKT, LAGP and SAKKT. For AKKT the answer, the Cone Continuity Property, had been found earlier (Andreani et al. 2016). This mission formalizes the SAKKT case, Theorem 4.5 of the preprint.
Setting
Consider the nonlinear program
minf(x)subject toh(x)=0,g(x)≤0,(1.1)
with h=(h1,…,hm) and g=(g1,…,gp) continuously differentiable on Rn. The feasible set is Ω={x:h(x)=0,g(x)≤0}, and J(x∗)={j:gj(x∗)=0} is the set of active inequalities. The KKT condition holds at x∗ for f if there are λ∈Rm and μ∈R+p, with μj=0 for j∈/J(x∗), such that ∇f(x∗)+∑iλi∇hi(x∗)+∑jμj∇gj(x∗)=0.
The linearized cone is LΩ(x∗)={d:⟨∇hi(x∗),d⟩=0∀i,⟨∇gj(x∗),d⟩≤0∀j∈J(x∗)}, and K∘={v:⟨v,k⟩≤0∀k∈K} is the polar of a set K. For a convex set S, the normal coneNS(y)={w:⟨w,z−y⟩≤0∀z∈S} is defined for y∈S and is empty for y∈/S. PS is the Euclidean projection onto a nonempty closed convex set S.
For a point x, the linearized setΩ(x,0) consists of the z with
⟨∇hi(x),z−x⟩=0 for all i;
⟨∇gj(x),z−x⟩≤0 for every j with gj(x)≥0.
It keeps the inequalities that are active or violated at x and drops those strictly satisfied at x.
A feasible x∗ satisfies SAKKT for f if there are xk→x∗, λk∈Rm and μk∈R+p, with μjk=0 whenever gj(xk)<0, such that
It satisfies AGP(0) for f if there is xk→x∗ with PΩ(xk,0)(xk−∇f(xk))−xk→0. The outer limitlimsupz→z∗F(z) of a set-valued map is the set of limits of sequences wk∈F(zk) with zk→z∗ (1.6). The point x∗ is SAKKT-regular (Definition 4.3) if
x→x∗limsupNΩ(x,0)(x)⊂NΩ(x∗,0)(x∗).
Formalization targets
Goal: Theorem 4.5
For continuously differentiable constraints and a feasible x∗,
x∗SAKKT-regular⟺(∀f∈C1:SAKKT at x∗⇒KKT at x∗).
The forward implication says SAKKT-regularity is a strict constraint qualification for SAKKT; the backward one says it is implied by every such qualification.
Milestones
Proposition 3.1: for nonempty closed convex C and x∈C, ω∈NC(x)⟺PC(x+ω)=x.
Proposition 4.4: if x+ε∈Ω(x,0), every element of NΩ(x,0)(x+ε) is ∑iλi∇hi(x)+∑gj(x)≥0μj∇gj(x) with μ≥0 and μj⟨∇gj(x),ε⟩=0; and NΩ(x,0)(x+ε)⊂NΩ(x,0)(x).
AGP(0) ⟺ SAKKT, for every C1 objective (p. 6, from Haeser–Schuverdt).
−∇f(x∗)∈LΩ(x∗)∘⟺ KKT at x∗.
(4.22): NΩ(x∗,0)(x∗)=LΩ(x∗)∘ at a feasible x∗.
(4.23)–(4.24): an AGP(0) sequence for f puts −∇f(x∗) in limsupx→x∗NΩ(x,0)(x).
(4.26): every ω∗ in that outer limit makes AGP(0) hold for f(x)=−⟨ω∗,x⟩.
Significance
Theorem 4.5 describes exactly the constraint systems on which a SAKKT sequence converging to x∗ certifies a KKT point, for every objective. Any constraint qualification already known to make SAKKT imply KKT implies SAKKT-regularity; at a point that is not SAKKT-regular, some linear objective has a SAKKT sequence converging to a non-KKT point. Because SAKKT is stronger than AKKT and AGP, its regularity condition is weaker than theirs, and Section 5 of the paper places it in the hierarchy of constraint qualifications next to AGP-regularity and CAKKT-regularity. By Proposition 4.4, SAKKT-regularity reads geometrically: the cone generated by the gradients of the equality constraints and of the inequalities that are active or violated at x varies outer semicontinuously as x→x∗.
The paper's result is proved, and no part of it is formalized on the platform. The mission adds machine-checked statements of the characterization and of the polyhedral convex-analysis facts behind it: the projection characterization of normal cones, the description of normal cones of Ω(x,0) at perturbed points, and the identification of NΩ(x∗,0)(x∗) with LΩ(x∗)∘.
Difficulty
The forward direction passes to the limit in normal cones of sets Ω(xk,0) that change with k: the set of rows kept depends on the sign of gj(xk) at the moving point, not on the active set at x∗. Projections land at yk=xk+εk, while SAKKT-regularity speaks of normal cones at xk, so the normal vectors must be transported from yk to xk; this is Proposition 4.4, a Farkas-type statement for the cone of active rows. Moving between SAKKT and AGP(0) requires the Haeser–Schuverdt equivalence, which the paper cites rather than proves. The backward direction must build an objective function and a sequential certificate from an arbitrary element of an outer limit, which needs existence and nonexpansiveness of projections onto every Ω(xk,0). Finally, LΩ(x∗)∘ and the KKT multipliers are linked by Farkas' lemma for a finitely generated cone.
Formalization scope
Rn is EuclideanSpace ℝ (Fin n); indices are Fin m and Fin p; gradients are Mathlib's gradient.
The standing hypothesis is that every hi and gj is C1. "Smooth objective" in Theorem 4.5 is read as C1, which is all the argument uses. The objective is quantified inside the equivalence, for fixed constraints and a fixed feasible x∗.
KKT is the multiplier form with sign and complementarity. The paper's reading −∇f(x∗)∈LΩ(x∗)∘ is a milestone.
SAKKT imposes μjk=0 when gj(xk)<0, at the iterate and not at x∗, and adds no complementarity limit. The page's "xk→x" is read as xk→x∗.
The normal cone is empty outside the set, and the projection is a predicate (a nearest point), not a choice function. The outer limit is the sequential one of (1.6), with x ranging over all of Rn.
Definition 4.3 is the inclusion; its trailing identity with LΩ(x∗)∘ is milestone 5. Proposition 4.4's "elements in Rm" is read as Rn.
Junk gradients (no C1 hypothesis where continuity is used), a normal cone that is nonempty at points outside the set, an objective quantified outside the equivalence, a support condition placed at x∗, or KKT without sign or complementarity would each trivialize or change the statement; the definitions above rule them out.
All objects are defined in the namespace StrictCQ.SAKKT. Proofs of milestones 1, 2, 4 and 5 are reusable convex analysis beyond this mission; contributions toward a proof of the Haeser–Schuverdt equivalence (milestone 3) are welcome independently of the goal.
Selected references
R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, Strict constraint qualifications and sequential optimality conditions for constrained optimization, Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018. https://doi.org/10.1287/moor.2017.0879
J. M. Martínez, B. F. Svaiter, A practical optimality condition without constraint qualifications for nonlinear programming, J. Optim. Theory Appl. 118:117–133, 2003. https://doi.org/10.1023/A:1023617925436
R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, A cone-continuity constraint qualification and algorithmic consequences, SIAM J. Optim. 26(1):96–110, 2016. https://doi.org/10.1137/15M1008488
Strict Constraint Qualifications and Sequential Optimality Conditions for Constrained Optimization II: AGP-Regularity Is the Weakest Strict Constraint Qualification for AGPResearch Paper
Motivation
Algorithms for smooth constrained optimization stop when an approximate optimality test passes. The tests used in practice are sequential optimality conditions: properties of a sequence of iterates xk→x∗ rather than of the limit alone. Every local minimizer satisfies them, with or without a constraint qualification, which makes them natural stopping criteria. The price is that a point passing such a test need not satisfy the Karush–Kuhn–Tucker (KKT) conditions. A strict constraint qualification for a sequential condition S is a property of the constraints at x∗ under which S implies KKT for every objective function. The weaker this property, the more problems on which the stopping test is guaranteed to certify a KKT point.
The Approximate Gradient Projection (AGP) condition was introduced by Martínez and Svaiter (2003) and is the natural stopping criterion of inexact restoration methods. It is strictly stronger than the Approximate KKT condition (AKKT), and it does not require Lagrange multiplier estimates. Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) determined the weakest strict constraint qualification associated with AGP and with several other sequential conditions. For AKKT the answer had been found earlier: the Cone Continuity Property of Andreani, Martínez, Ramos and Silva (2016). This mission formalizes the AGP case, Theorem 4.2 of the preprint, together with its linear-constraint variant, Theorem 4.6.
Setting
Consider the nonlinear program
minf(x)subject toh(x)=0,g(x)≤0,(1.1)
with h=(h1,…,hm) and g=(g1,…,gp) continuously differentiable on Rn. The feasible set is Ω={x:h(x)=0,g(x)≤0}, and J(x∗)={j:gj(x∗)=0} is the set of active inequalities. The KKT condition holds at x∗ for f if there are λ∈Rm and μ∈R+p, with μj=0 for j∈/J(x∗), such that ∇f(x∗)+∑iλi∇hi(x∗)+∑jμj∇gj(x∗)=0.
The linearized cone is LΩ(x∗)={d:⟨∇hi(x∗),d⟩=0∀i,⟨∇gj(x∗),d⟩≤0∀j∈J(x∗)}, and K∘={v:⟨v,k⟩≤0∀k∈K} is the polar of a set K. For a convex set S, the normal coneNS(y)={w:⟨w,z−y⟩≤0∀z∈S} is defined for y∈S and is empty for y∈/S. PS denotes the Euclidean projection onto a closed convex set S.
For γ∈[−∞,0] and a point x, the linearized setΩ(x,γ) of (4.2) consists of the z with
⟨∇hi(x),z−x⟩=0 for all i;
⟨∇gj(x),z−x⟩≤0 if gj(x)≥0;
gj(x)+⟨∇gj(x),z−x⟩≤0 if γ<gj(x)<0.
A feasible x∗ satisfies AGP(γ) for f if there is a sequence xk→x∗ with
PΩ(xk,γ)(xk−∇f(xk))−xk→0.(4.1)
The outer limitlimsupz→z∗F(z) of a set-valued map is the set of limits of sequences wk∈F(zk) with zk→z∗ (1.6). The point x∗ is AGP-regular (Definition 4.1) if
(x,ε)→(x∗,0)limsupNΩ(x,−∞)(x+ε)⊂NΩ(x∗,−∞)(x∗).
Formalization targets
Goal: Theorem 4.2
For continuously differentiable constraints and a feasible x∗,
x∗AGP-regular⟺(∀f∈C1:AGP(−∞) at x∗⇒KKT at x∗).
The forward implication says AGP-regularity is a strict constraint qualification for AGP; the backward one says it is implied by every such qualification.
Milestones
Proposition 3.1: for nonempty closed convex C and x∈C, ω∈NC(x)⟺PC(x+ω)=x.
Nonexpansiveness of PC, used in (4.10).
(4.6): NΩ(x∗,−∞)(x∗)=LΩ(x∗)∘ at a feasible x∗.
−∇f(x∗)∈LΩ(x∗)∘⟺ KKT at x∗.
(4.8): NΩ(xk,γ)(xk+εk)⊂NΩ(xk,−∞)(xk+εk) for k large.
(4.7)–(4.9): under AGP-regularity, AGP(γ) implies KKT for every γ∈[−∞,0).
(4.10)–(4.11): every ω∗ in the outer limit makes AGP(−∞) hold for f(x)=−⟨ω∗,x⟩.
Companion: Theorem 4.6
The same characterization for the Linear AGP condition (LAGP), in which the linear constraints are kept exact and the iterates stay in the set ΩL they define. LAGP-regularity (Definition 4.4) is outer semicontinuity of (x,ε)↦NΩNL(x,−∞)∩ΩL(x+ε) relative to x∈ΩL. Two further items accompany it: Proposition 4.1, the explicit form of NΩ(x,−∞)(x+ε), and the equality NΩNL(x∗,−∞)∩ΩL(x∗)=LΩ(x∗)∘ appended to Definition 4.4.
Significance
Theorem 4.2 gives the exact boundary of the problems on which an AGP-based stopping test certifies KKT points. Any constraint qualification already known to make AGP imply KKT, for instance the Cone Continuity Property, implies AGP-regularity. Conversely, at a point that is not AGP-regular some objective function has an AGP sequence converging to a non-KKT point. In Section 5 of the paper the theorem places AGP-regularity in the hierarchy of constraint qualifications, with the regularity notions for CAKKT and SAKKT next to it.
The paper's result is proved, and no part of it is formalized on the platform. The mission adds machine-checked statements of the characterization and of the convex-analysis facts it rests on: the projection characterization of normal cones, nonexpansiveness, and the polyhedral normal cone of Ω(x∗,−∞) as the polar of the linearized cone. These facts are reusable for any sequential optimality condition built on projections.
Difficulty
The forward direction passes to the limit in normal cones of sets Ω(xk,γ) that vary with k and are evaluated at perturbed points xk+εk, which may lie outside Ω(xk,−∞). For finite γ the inclusion of NΩ(xk,γ) in NΩ(xk,−∞) fails at such points. It holds only for k large, through a continuity argument on the inactive constraints. The backward direction must manufacture an objective function and an AGP sequence from an arbitrary element of an outer limit, which requires existence of projections onto every Ω(xk,−∞). The identification of NΩ(x∗,−∞)(x∗) with LΩ(x∗)∘ needs the localization of a polyhedral normal cone, and the link between LΩ(x∗)∘ and KKT multipliers is Farkas' lemma for a finitely generated cone.
Formalization scope
Rn is EuclideanSpace ℝ (Fin n); indices are Fin m and Fin p; gradients are Mathlib's gradient.
The standing hypothesis is that every hi and gj is C1. Objectives in the characterizations are C1 and are quantified inside the equivalence, for fixed constraints and fixed feasible x∗.
KKT is the multiplier form with sign and complementarity. The paper's reading −∇f(x∗)∈LΩ(x∗)∘ is a milestone.
γ is an extended real and −∞ is its bottom element. The goal states AGP as AGP(−∞). The paper's AGP is the γ-independent condition of Martínez–Svaiter, which this paper does not prove; milestone 6 gives the forward direction for every γ<0.
The normal cone is empty outside the set. A normal cone that is nonempty at infeasible points makes AGP-regularity a different, stronger condition. The projection is a predicate (a nearest point), not a choice function.
The outer limit is sequential, as in (1.6).
The paper says the inclusion (4.8) "always holds"; it is stated for k large, which is what the proof uses. Definition 4.4's "ΩL×Rm" is read as ΩL×Rn.
A formalization with junk gradients (no C1 hypothesis where the proof needs continuity), an objective quantified outside the equivalence, or KKT without sign or complementarity is ruled out by the statements above.
All objects are defined in the namespace StrictCQ.AGP. Proofs of the convex-analysis milestones are reusable beyond this mission.
Selected references
R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, Strict constraint qualifications and sequential optimality conditions for constrained optimization, Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018. https://doi.org/10.1287/moor.2017.0879
J. M. Martínez, B. F. Svaiter, A practical optimality condition without constraint qualifications for nonlinear programming, J. Optim. Theory Appl. 118:117–133, 2003. https://doi.org/10.1023/A:1023617925436
R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, A cone-continuity constraint qualification and algorithmic consequences, SIAM J. Optim. 26(1):96–110, 2016. https://doi.org/10.1137/15M1008488
Shortest Paths in Graphs of Convex Sets II: For Compact 𝒳 the Set-Based Relaxation 𝒮′ of Z = xyᵀ Is Exact at Every Extreme Point of a Polytope 𝒴Research Paper
Motivation
The shortest-path problem in a graph of convex sets (SPP in GCS), introduced by Marcucci, Umenberger, Parrilo and Tedrake (arXiv:2101.11565, SIAM J. Optim. 2024), asks for a path through a directed graph whose vertices carry convex sets, together with a point in each visited set, minimizing a sum of convex edge lengths. It models motion planning around obstacles, hybrid-system control and other problems that mix a discrete choice with continuous positions. The paper formulates it as a mixed-integer convex program whose only nonconvexity, before relaxation, is a family of bilinear equalities Z=xy⊤ that couple the continuous positions x with the flow variables y.
Section 7 of the paper studies the convex relaxation used for these bilinear equalities in isolation. Products of valid inequalities linearized by Z=xy⊤ are the idea behind the McCormick envelope (McCormick 1976) and the Reformulation-Linearization Technique of Sherali and Adams. This mission formalizes the paper's result that the relaxation is exact at every extreme point of the polytope Y, which is the property that makes the mixed-integer formulation exact at binary flows.
Setting
Fix X⊆Rn and Y⊆Rm. Points of Rn×Rm×Rn×m are written (x,y,Z).
The perspective of X (Definition 4.1) is X~:=cl{(x,λ):λ≥0,x∈λX}⊆Rn×R.
The cone of valid inequalities (Definition 4.8) is X∘:={(a,b):a⊤x+b≥0 for all x∈X}.
The dual cone of K⊆Rn×R is K∗:={(a,b):a⊤x+bλ≥0 for all (x,λ)∈K}.
The bilinear set (7.1) is S:={(x,y,Z):x∈X,y∈Y,Z=xy⊤}.
The set-based relaxation (7.2) multiplies every valid inequality of X by every valid inequality of Y and replaces xy⊤ by Z:
S′:={(x,y,Z):a⊤Zc+da⊤x+bc⊤y+bd≥0 for all (a,b)∈X∘,(c,d)∈Y∘}.
A polytope is a bounded set Y={y:ci⊤y+di≥0 for all i∈I} with I finite. Its asymmetric relaxation (7.3) is {(x,y,Z):(Zci+dix,ci⊤y+di)∈X~ for all i∈I}.
Always S⊆S′, and S′ is convex.
Formalization targets
Goal: Lemma 7.4 (p. 13)
Let X be compact and convex, let Y be a polytope and let y^ be an extreme point of Y. Then for all x and Z,
(x,y^,Z)∈S⟺(x,y^,Z)∈S′.
Milestones
(7.2), p. 12: S⊆S′ for arbitrary sets.
The sentence after (7.2), p. 12: for closed convex X,Y, every point of S′ has x∈X and y∈Y.
Lemma 4.9, p. 6: for nonempty closed convex X, (X~)∗=X∘ and (X∘)∗=X~.
Proposition 7.1, inclusion ⊆, p. 12: S′ is contained in the asymmetric relaxation (7.3), for every family of halfspaces.
Remark 4.2, p. 5: for compact convex X, X~={(x,λ):λ≥0,x∈λX}, without closure.
Proof of Lemma 7.4, p. 13: at an extreme point of a polyhedron with finitely many inequalities, m linearly independent inequalities are active.
Proposition 7.1, p. 12: S′ equals (7.3), when the trivial inequality 1≥0 is a nonnegative combination of the defining inequalities.
Remark 7.5, p. 14: if Y⊆[0,1]m, every point of Y∩{0,1}m is an extreme point of Y.
(7.4), p. 13: for compact convex X and Y=conv{y^j}j∈J, convS={∑j(xj,λjy^j,xjy^j⊤):∑jλj=1,(xj,λj)∈X~}.
Significance
The result. In the paper's mixed-integer program each vertex v contributes a bilinear set Sv in which X is the convex set at v and Y is the polytope of flows on the edges at v. Binary flows corresponding to a path are extreme points of these polytopes, so Lemma 7.4 says that replacing Sv by Sv′ loses nothing at the integer points of the program. This gives the paper's second, geometric proof that its mixed-integer convex formulation is exact (Theorem 5.7). By Remark 7.5 the lemma also extends a known property of the first-level Reformulation-Linearization Technique for bilinear programs with binary variables from polytopes X to compact convex sets X. Proposition 7.1 is what makes the relaxation finite: it replaces the infinitely many inequalities of S′ by one perspective-cone constraint per facet of Y.
Formalizing it. The results are proved on paper; none of them has a machine-checked proof. The formalization also settles the exact hypotheses. Three statements of this section are false as printed (see Formalization scope), and the corrected versions are posed here with the counterexamples recorded. The perspective cone, the cone of valid inequalities and their duality (Lemma 4.9) are general convex-analysis facts that recur across conic and disjunctive programming.
Difficulty
The direction S⊆S′ is one line, since (a⊤x+b)(c⊤y+d)≥0. The converse at y^ needs three ingredients that are each standard and none of which is in Mathlib in this form.
The duality between X~ and X∘ is a bipolar theorem for the closed cone generated by X×{1}, in the product Rn×R with the pairing a⊤x+bλ. The cone needs care at λ=0.
The active-constraint characterization of extreme points of a polyhedron in halfspace form has to be proved directly.
The step "(u,0)∈X~ implies u=0" is where boundedness enters. For unbounded X the slice λ=0 of X~ is the recession cone, and the argument, and the lemma, fail.
Proposition 7.1 as an equality needs an affine Farkas lemma, and its printed proof skips the case of the valid inequality (0,1).
Formalization scope
Rn is Fin n → ℝ, inner products are dotProduct, Zc is Z *ᵥ c and xy⊤ is Matrix.vecMulVec x y. Triples are (x, y, Z) in (Fin n → ℝ) × (Fin m → ℝ) × Matrix (Fin n) (Fin m) ℝ. A polytope is given by a finite family (c i, d i) over a Fintype index and the hypothesis Bornology.IsBounded; extreme points are Mathlib's Set.extremePoints ℝ, never a predicate defined through active constraints. The dual cone uses the pairing a⊤x+bλ on the product, not an inner product.
Hypotheses added relative to the page, each with a counterexample to the printed form:
Lemma 7.4 and (7.4): X compact. Section 7.1 only asks X to be closed and convex. For X=[0,∞), Y=[0,1] and y^=0, the point (1,0,21) is in S′ but not in S. Compactness is the standing assumption of Section 2 on the sets Xv that X stands for.
Lemma 4.9: X nonempty. For X=∅, X~=∅ but (X∘)∗={0}.
Proposition 7.1 (equality): 1≥0 is a nonnegative combination of the rows. For Y={0} written as {y≥0,−y≥0} and X=[0,1], the point (5,0,0) satisfies (7.3) but not (7.2). The hypothesis holds for every polytope with an interior point and for the flow polytopes of the paper.
Several hypotheses are dropped where they are not needed, which strengthens the statements: nonemptiness of X throughout, and boundedness and finiteness in the inclusion of Proposition 7.1 and in the active-constraint milestone.
Trivializing formalizations ruled out: S′ quantifies over all of X∘×Y∘ and is not replaced by (7.3) in the goal; X is never allowed to be merely closed in the goal; the hypotheses of the goal are satisfiable (X=Y=[0,1], y^=0 is checked in Lean).
A complete development needs the bipolar theorem for closed convex cones in Rn×R, the closedness of the cone over a compact convex set, the active-constraint characterization of extreme points, and a finite affine Farkas lemma. All of these are reusable well beyond this mission and are welcome as separate contributions.
G. P. McCormick, Computability of global solutions to factorable nonconvex programs: Part I — Convex underestimating problems, Math. Program. 10, 1976. https://doi.org/10.1007/BF01580665
H. D. Sherali, W. P. Adams, A Reformulation-Linearization Technique for Solving Discrete and Continuous Nonconvex Problems, Kluwer, 1999. https://doi.org/10.1007/978-1-4757-4388-3
Strict Constraint Qualifications and Sequential Optimality Conditions for Constrained Optimization I: MFCQ or a Full Active-Gradient Cone Is the Weakest Strict CQ for Scaled-AKKTResearch Paper
Motivation
Practical algorithms for nonlinear programming do not stop at an exact Karush–Kuhn–Tucker (KKT) point; they stop when an approximate stationarity test passes. Sequential optimality conditions formalize what such tests certify: they are properties of a feasible point x∗ phrased through sequences xk→x∗ and multiplier estimates, and every local minimizer satisfies them without any constraint qualification. The question that links them back to classical theory is which conditions on the constraints guarantee that a point satisfying a sequential condition is in fact a KKT point. Andreani, Martínez, Ramos and Silva call these strict constraint qualifications and ask, for each sequential condition, for the weakest one.
For the Approximate KKT condition (AKKT) the answer, the Cone Continuity Property, was given by Andreani, Martínez, Ramos and Silva in 2016 (SIAM J. Optim. 26(1)). Section 2 of the present paper treats the Scaled-AKKT condition, which divides the stationarity residual by the size of the multipliers. This scaling appears in the stopping criteria of practical codes and in complexity analyses of nonlinear programming methods. Scaled-AKKT is weaker than AKKT, and the paper uses it as the first, self-contained example of the analysis it then carries out for AGP, CAKKT and SAKKT.
Setting
Fix n,m,p≥0 and continuously differentiable functions h1,…,hm, g1,…,gp:Rn→R, where Rn carries the Euclidean inner product ⟨⋅,⋅⟩ and norm ∥⋅∥. The feasible set is Ω={x:hi(x)=0,gj(x)≤0 for all i,j}, and x∗∈Ω is fixed. An index j is active when gj(x∗)=0.
For an objective f, the point x∗satisfies KKT if there are λ∈Rm and μ∈Rp with μ≥0, μj=0 for inactive j, and ∇f(x∗)+∑iλi∇hi(x∗)+∑jμj∇gj(x∗)=0.
Scaled-AKKT holds at x∗ for f if there are sequences xk→x∗, λk∈Rm and μk∈Rp with μk≥0, such that min{μjk,−gj(xk)}→0 for every j, and
where ∥⋅∥∞ is the supremum norm of a multiplier vector.
The Mangasarian–Fromovitz constraint qualification (MFCQ) holds at x∗ if ∇h1(x∗),…,∇hm(x∗) are linearly independent and some d satisfies ⟨∇hi(x∗),d⟩=0 for all i and ⟨∇gj(x∗),d⟩<0 for all active j. The cone of active gradients is
Goal: the weakest strict constraint qualification for Scaled-AKKT
For a C1 constraint system and a feasible x∗,
(MFCQ at x∗ or K(x∗)=Rn)⟺∀f∈C1:(Scaled-AKKT at x∗ for f)⇒(KKT at x∗ for f).(2.3)
The forward implication says that (2.3) is a strict constraint qualification for Scaled-AKKT; the backward implication says that every strict constraint qualification for Scaled-AKKT implies (2.3).
Milestones
If K(x∗)=Rn, then x∗ is a KKT point for every objective (p. 3).
Scaled-AKKT with a bounded multiplier set {λk,μk} implies KKT (p. 3).
Scaled-AKKT with an unbounded multiplier set yields λ, μ≥0 supported on the active set, with max{∥λ∥∞,∥μ∥∞}=1, solving ∑iλi∇hi(x∗)+∑j activeμj∇gj(x∗)=0, display (2.4) (pp. 3–4).
Such a normalized solution of (2.4) excludes MFCQ (p. 4).
Conversely, failure of MFCQ yields a normalized solution of (2.4) (p. 4).
Given a normalized solution of (2.4), Scaled-AKKT holds at x∗ for every linear objective f(x)=⟨x,c⟩ (p. 4).
Significance
The result separates Scaled-AKKT sharply from AKKT. For AKKT the weakest strict constraint qualification (the Cone Continuity Property) is implied by many classical conditions, including CPLD and RCPLD. For Scaled-AKKT it is essentially MFCQ, a much stronger requirement. A stopping test of the Scaled-AKKT type therefore certifies a KKT point only under MFCQ, apart from the degenerate case of a full active cone. The other sections of the paper characterize the weakest strict constraint qualifications for AGP, CAKKT and SAKKT, using the same "iff over all objectives" template that this mission formalizes in its simplest form.
The paper's argument is a half-page sketch. A formalization makes explicit several points it leaves implicit: the role of the 1 in the scaling factor, the vanishing of inactive multipliers forced by the complementarity limit, and the theorem of the alternative that converts failure of MFCQ into a nonzero solution of (2.4). None of these results is formalized on Prove2Me or, to our knowledge, in Mathlib.
Difficulty
The forward direction splits on whether the multipliers stay bounded, and the unbounded case requires normalizing by max{1,∥λk∥∞,∥μk∥∞} and extracting a convergent subsequence. Along that subsequence one must check that the normalized multipliers have supremum norm exactly one, that the normalized objective gradient tends to zero, and that inactive multipliers tend to zero; only then does the limit contradict MFCQ. The backward direction needs a theorem of the alternative (Motzkin or Gordan type) for the active gradients, together with linear dependence of the equality gradients. The paper uses it without stating it. It also needs a vector c with −c∈/K(x∗). The printed text chooses c∈/K(x∗), which has the wrong sign for the objective ⟨x,c⟩; milestone 6 is stated for every c, so the sign issue does not propagate.
Formalization scope
Rn is EuclideanSpace ℝ (Fin n); the constraints are index families Fin m → E → ℝ and Fin p → E → ℝ; gradients are Mathlib's gradient. Multiplier vectors live in Fin m → ℝ and Fin p → ℝ, whose Mathlib norm is the supremum norm, while residuals use the Euclidean norm. Standing hypotheses: every hi, gj is C1 (the paper's "continuous first-order derivatives"), every objective in the goal is C1, and x∗ is feasible. The objective is quantified inside the equivalence, so the left side of the goal depends on h, g, x∗ alone. "or" is inclusive. The cone condition is equality of the cone with all of Rn, not with its linear span. KKT carries both the sign condition μ≥0 and complementarity. MFCQ is defined in its primal (direction) form; defining it as "no nonzero nonnegative null combination" would make milestones 4 and 5 hold by definition, and that reading is excluded. Milestone 2 omits the MFCQ hypothesis present in the paper's sentence because the bounded case does not use it.
A complete development needs subsequence extraction in finite-dimensional spaces, continuity of gradients of C1 functions, and a theorem of the alternative for finitely many vectors. The last two are reusable beyond this mission. Proofs of individual milestones are welcome independently.
Selected references
R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, Strict constraint qualifications and sequential optimality conditions for constrained optimization, Optimization Online 5197 (2015); Mathematics of Operations Research 43(3), 2018. https://doi.org/10.1287/moor.2017.0879
R. Andreani, J. M. Martínez, A. Ramos, P. J. S. Silva, A cone-continuity constraint qualification and algorithmic consequences, SIAM Journal on Optimization 26(1), 2016. https://doi.org/10.1137/15M1008488
O. L. Mangasarian, S. Fromovitz, The Fritz John necessary optimality conditions in the presence of equality and inequality constraints, Journal of Mathematical Analysis and Applications 17, 1967. https://doi.org/10.1016/0022-247X(67)90163-1
R. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60(5), 2011. https://doi.org/10.1080/02331930903578700
On Solving Multistage Stochastic Programs with Coherent Risk Measures: The Inner-Approximation Policy's Nested Risk-Adjusted Cost Is at Most the Upper Bound yResearch Paper
Motivation
Multistage stochastic linear programs model decisions taken over time under uncertainty: reservoir releases in hydro-thermal scheduling, production and inventory plans, capacity expansion. Their standard solution method, stochastic dual dynamic programming (SDDP, Pereira and Pinto 1991), approximates each stage's cost-to-go function from below by cutting planes. This gives a lower bound on the optimal value and a candidate policy, but no guaranteed upper bound: in the risk-neutral case the policy's expected cost is estimated by Monte Carlo simulation.
Planners who are averse to risk replace the expectation in each stage by a coherent risk measure (Artzner, Delbaen, Eber and Heath 1999), nested stage by stage so that the resulting dynamic risk measure is time consistent (Ruszczyński and Shapiro 2006). Under such a nested objective, simulation no longer estimates the cost of a policy: the nested risk of a policy is not an average over sampled scenarios. Philpott, de Matos and Finardi (2013) address this by an inner approximation of the cost-to-go functions from above, built from convex combinations of finitely many points with known upper bounds. Their Proposition 5 shows that the optimal value y of the resulting first-stage problem bounds the nested risk-adjusted cost of the policy defined by the inner approximation. This gives a deterministic upper bound that complements the SDDP lower bound, and they apply it to the Brazilian hydro-thermal system.
Setting
There are T≥2 stages. The decision at stage t is xt∈Rn; At,Et are m×n matrices and ct∈Rn. Stage 1 is deterministic: A1x1=b1. For t≥2 a random outcome ωt ranges over a finite set Ωt, independently of earlier stages, and enters through the right-hand side bt(ωt). The feasible set of stage t given the previous decision xt−1 is
Xt(ωt)={xt≥0:Atxt=bt(ωt)−Etxt−1}.
A coherent risk measureρ maps random costs Z:Ω→R to R and is subadditive, monotone (Z1≤Z2⇒ρ(Z1)≤ρ(Z2)), positively homogeneous and translation equivariant (ρ(λ+Z)=λ+ρ(Z)). Larger is worse: these are costs. Each stage t≥2 carries a one-step coherent risk measure ρt on random costs over Ωt. It is extended to costs in R∪{+∞} by ρˉt(Z)=+∞ whenever some outcome has infinite cost.
For s=2,…,T fix points xs−11,…,xs−1Js−1 and numbers qs1,…,qsJs−1. The inner approximation is the lower boundary of the convex hull of the pairs (xs−1j,qsj):
The numbers qsj are upper bounds when qsj≥ρˉs(qs(xs−1j,ωs)) for all s and j. A policy defined by the inner approximation, π^, takes at each state xt−1 and outcome ωt an action x^t(xt−1,ωt) solving (13), and a first-stage action x^1 solving (8). The actual risk-adjusted cost of π^ over stages t,…,T is
with no future term at t=T. The nested risk-adjusted cost of the policy is v(π^)=c1⊤x^1+ρˉ2(v^2(x^1,ω2)).
Formalization targets
Goal: Proposition 5
v(π^)≤y.
The bound holds for every T≥2, every family of coherent ρt, every choice of points satisfying the upper-bound property, and every minimizing selection π^.
Milestones
The convexity display of §2: subadditivity and positive homogeneity imply ρ(αZ1+(1−α)Z2)≤αρ(Z1)+(1−α)ρ(Z2).
Q^s is the lower boundary of the convex hull H of the pairs (xs−1j,qsj) (its epigraph is H plus the vertical half-line), hence convex with Q^s(xs−1j)≤qsj, and every convex function bounded by the qsj at the points lies below Q^s.
qt(⋅,ωt) is convex in xt−1.
The interpolation bound ρˉt(qt(xt−1,ωt))≤Q^t(xt−1).
The induction claim ρˉt(v^t(xt−1,ωt))≤Q^t(xt−1) for t=2,…,T and every xt−1.
Companions
Proposition 3, the risk-neutral case ρt=E. Proposition 4, the subgradient rule ∑mpmζ~mg(x~,ωm)∈∂xρ(Z(x,ω)) for ρ given by its dual representation. The existence of a policy π^, which shows that the hypotheses of the goal can be met.
Significance
Proposition 5 makes the inner approximation a certificate. Any policy computed by minimizing against Q^t+1 has nested risk-adjusted cost at most y, a number obtained by solving one linear program. Together with the lower bound z from outer approximation it brackets the risk-adjusted optimal value. The gap y−z then measures the quality of a risk-averse SDDP policy without simulation, which the nested objective does not allow. The bound covers every coherent nesting used in practice, such as mixtures of expectation and CVaR.
The results are proved in the paper. None of them is machine-checked. A formalization adds a precise account of the infinite values the paper does not discuss: infeasible stages, points outside the convex hull, and the extension of ρt to +∞. It also pins down the exact form of the upper-bound hypothesis the induction needs.
Difficulty
The obvious reading of the hypothesis on p. 16, "qt+1j is an upper bound on ρt+1(Qt+1(xtj,ωt+1))" with the true value function Qt+1, does not support the induction. The policy π^ does not act optimally, so its cost can exceed the true value, and the inductive step compares v^t with the policy's own stage value qt, not with Qt. The hypothesis that works bounds the risk-adjusted optimal value of the policy's stage problem (13) at the points, which is what the paper's Upper Bound Computation actually computes.
The second difficulty is infinite values, which the paper never discusses. A risk measure is defined on real random costs, yet stage problems can be infeasible, Q^s is +∞ off a convex hull, and a convex combination may put zero weight on a point whose bound is +∞. Every inequality of the paper has to be re-read in R∪{+∞}, and the extended-real arithmetic must not silently produce a value the paper does not intend.
Formalization scope
Vectors are Fin n → ℝ, all stages share n and m, and costs that may be infinite are EReal. Minima are EReal infima, +∞ on an empty set. Attainment of a minimum is never built into a definition: the policy is a selection with a minimizing property, required at every state where the stage problem is feasible. Stages are natural numbers. Points and bounds are indexed by the stage s of the function Q^s they define, so pts s j is xs−1j and qv s j is qsj. Stagewise independence is built in: ωt ranges over Ωt whatever happened before.
Standing assumptions made explicit in the statements:
T≥2;
ρt coherent for t=2,…,T (all four axioms, though the proof uses only monotonicity and convexity);
the terminal convention ρT+1(QT+1)=0, so Q^T+1≡0;
(8) without the constraint x1≥0, as printed;
the upper-bound hypothesis in the form above.
The risk measures ρt act on real random costs and are extended by ρˉt(Z)=+∞ when some outcome has infinite cost. In Proposition 4, ρ is given by its dual representation (10); the representation theorem itself is not part of the mission. The existence statement adds solvability of A1x1=b1 and boundedness below of the last-stage program, without which (8) or the last stage has no solution.
The goal is not to be trivialized. Its hypotheses mention neither v^t nor the induction claim; the policy must minimize at every feasible state, not only along visited states; and the statement is for general T and general coherent ρt, not the expectation. The bound is trivially true when y=+∞ and is informative when x^1 lies in the convex hull of the stage-1 points.
A complete development needs:
convexity of extended-real linear-programming value functions in their right-hand side;
convexity of the convex-hull function Q^;
finite Jensen-type inequalities for monotone convex risk measures;
linear-programming attainment, for the existence companion.
The first two are reusable for any SDDP-type development. Proofs of the milestones in any order are welcome.
Selected references
A. B. Philpott, V. L. de Matos, E. Finardi, On Solving Multistage Stochastic Programs with Coherent Risk Measures, Operations Research 61(4), 2013. https://doi.org/10.1287/opre.2013.1175
M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52, 1991. https://doi.org/10.1007/BF01582895
Product Price, Quality and Service Decisions under Consumer Choice Models VI: Consumer Surplus Rises as the Firm Also Controls Service Duration, and Again as It Also Controls QualityResearch Paper
Who gains when a firm controls more decisions
A firm that sells differentiated products sets more than prices. It chooses quality levels (features, materials, reliability) and the ancillary services that come free with a product, such as a factory warranty or free maintenance for a fixed period. Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study the joint choice of price, quality and service duration when consumers choose according to the multinomial logit (MNL) model.
A firm allowed to make more decisions can never earn less: it may always ignore the extra instruments. The question this mission formalizes is what happens to consumers. A natural guess is that every new instrument lets the firm extract more of the consumers' surplus. Section 2.3 of the paper (Proposition 5) shows that under MNL demand this guess is wrong: consumer surplus also rises, so more control is a "win–win". The welfare measure is the logit consumer surplus of Anderson, de Palma and Thisse (Discrete Choice Theory of Product Differentiation, MIT Press, 1992).
The mission is the sixth of a series on the paper; each mission defines its own copy of the model in its own namespace.
Setting
There are N products i∈N={1,…,N}. Product i has a price pi, a quality levelqi and a service durationti, which must lie in a fixed interval [ts,tl]. The parameters are: αi, the consumers' sensitivity to quality; si, the utility of one unit of service time; ci>0, so that producing one unit at quality qi costs ciqi2; and ai,bi, so that service costs ai−biqi per unit of time. The sign of bi is free: higher quality may make service cheaper (bi>0), dearer (bi<0), or leave it unchanged (bi=0).
A consumer buys product i with the MNL choice probability
and the bracket is the markup of product i. Consumer surplus is
CS(p,q,t)=log(1+i∈N∑exp(αiqi−pi+tisi)).
Three problems are compared, at the same pre-determined qualities q and durations t∈[ts,tl]N:
price only: maximize Π(⋅,q,t) over p∈RN, with a maximizer p†;
price and service: maximize Π(⋅,q,⋅) over p∈RN and t′∈[ts,tl]N, with a maximizer (p‡,t‡);
price, quality and service, problem (4): maximize Π over all three, with a maximizer (p∗,q∗,t∗).
Section 5.1 adds the manufacturer's short-term problem (10): qualities are fixed, and the firm also chooses which products S⊆N to offer.
Formalization targets
Goal: Proposition 5 (p. 13)
For every maximizer of each of the three problems,
CS(p†,q,t)≤CS(p‡,q,t‡)≤CS(p∗,q∗,t∗).
The inequalities are weak; equality holds, for instance, when the pre-determined q,t are already optimal.
Milestones
Equation (17) (p. 26). For fixed q,t, the equation r=∑iexp(αiqi−ciqi2+ti(si−(ai−biqi))−r−1) has a unique root r†; a price vector is optimal if and only if every markup equals 1+r†; the optimal profit is r†.
Proposition 8 (p. 21). In problem (10) all products should be offered, an optimum uses durations ts or tl according to the sign of bi and the position of qi, every optimal markup is 1+r∗, and r∗ is the unique root of the corresponding equation.
Consumer surplus at an optimum (Online Supplement p. 1). If every markup is 1+r and the profit is r, then CS=log(1+r).
Ordering of profits (Online Supplement p. 2): r†≤r‡≤r∗.
Significance
The result separates two effects that are usually conflated. More instruments raise profit; Proposition 5 says that under MNL demand the extra profit comes from serving more consumers (fewer choose the outside option), not from extracting more surplus from each. Proposition 8 states the corresponding structure for a firm whose product designs are already fixed: offer everything, use extreme service durations, and keep markups equal across products.
The paper proves these results; none is formalized. A machine-checked development produces the welfare comparison together with the price step of the MNL multi-product pricing problem (equal markups at every optimum, uniqueness of the optimal profit as a fixed point) as reusable statements, and pins down the boundary cases of Proposition 8 that the printed statement leaves implicit.
Difficulty
The ordering of profits is immediate from the nesting of feasible sets. The obstacle is translating it into consumer surplus: consumer surplus is not monotone in profit along arbitrary price vectors, and the argument needs that at every maximizer of each problem all markups are equal to 1+r, with r the optimal profit. That requires a global optimality analysis of the multi-product MNL pricing problem: the profit is not concave in prices, and both the uniqueness of the fixed point and the characterization of all maximizers (not only a stationary point) must be established. Comparing values log(1+r) with r defined as the optimal profit, without linking them to the maximizers, proves nothing about consumer surplus.
Formalization scope
Products are Fin N (0-based); N is arbitrary and N=0 is allowed. The outside option is the 1 in the denominator, not a product.
Parameters α,a,b,c,s:FinN→R; only ci>0 and ts≤tl are assumed throughout. No sign is imposed on bi, αi, ai or si, and products are not assumed identical.
Qualities range over R, not the model's normalized range [0,ai/bi), because the paper's joint optimum is computed over unconstrained qualities. Proposition 8(b) adds the model's bound qi≤ai/bi for bi>0, without which the printed rule can fail.
"Optimal" means a global maximizer over the stated feasible set. The goal quantifies over all maximizers of the three problems; their existence is not part of Proposition 5.
The MNL formula and the log-sum consumer surplus are definitions; their derivation from Gumbel random utilities is cited, not formalized.
Problem (10) is printed with Π(p,q,t;N); the profit of the offer set S is meant and is what is formalized.
A formalization in which the maximizers are given by the paper's closed-form prices, in which r†,r‡,r∗ are defined as optimal values and only log(1+r) is compared, or in which there is a single product, would make the goal trivial or different and is ruled out.
Contributions are welcome on the MNL price step (equation (17)), which is reusable for any multi-product logit pricing model, and on the per-product separation of the duration choice in Proposition 8.
Product Price, Quality and Service Decisions under Consumer Choice Models III: The Optimal Uniform Service Duration Is the Shortest or the LongestResearch Paper
Motivation
Firms that sell durable goods compete on price, on product quality and on the services bundled with the product: a factory warranty, free maintenance, technical support. Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study the joint choice of all three when consumers choose among the firm's products according to a multinomial logit (MNL) model. Their first result (Theorem 1, the subject of mission I of this series) is that when each product may receive its own service duration, every optimal duration is the shortest or the longest allowed.
In practice many firms do not differentiate service across products: every Apple product, for example, comes with the same one-year factory warranty. The paper's Section 3 therefore studies a benchmark in which one uniform service duration is attached to all products, and compares it with differentiated service to measure the value of service differentiation. Theorem 3, the goal of this mission, says that the extreme-duration structure survives the uniformity constraint.
The pricing side builds on a line of work on multi-product pricing under logit demand. Hanson and Martin (1996) showed that the MNL profit is not jointly concave in prices; Li and Huh (2011) and Gallego and Wang (2014) showed that, nevertheless, optimal markups (price minus cost) are equal across the products of a firm under the MNL and nested logit models.
Setting
A firm sells N products, N={1,…,N}. For product i:
αi is the consumers' sensitivity to quality, si the utility of service per unit time;
ciqi2 is the unit production cost at quality qi, with ci>0;
ai−biqi is the expected service cost per unit time, with base cost ai and a marginal effect bi of quality on service cost that may be positive, negative or zero.
The firm chooses prices p, qualities q and service durations t. Under the MNL choice model (2) a consumer buys product i with probability
Problem (7) has an optimal solution whose uniform duration is an endpoint. The goal says nothing about the optimal prices, qualities or profit value; those belong to the milestones.
Milestones (the paper's proof, pp. 29–30)
(24). At a fixed uniform duration t, the root r(t) of
is unique, and it is the optimal profit over prices and qualities, attained at qi=(αi+tbi)/(2ci), pi=1+r+ciqi2+t(ai−biqi).
2. ∂r/∂t.r(t) is differentiable with r′(t)=∑iAiGi/(1+∑iGi).
3. The numerator.∑iAiGi has nonnegative derivative.
4. Quasi-convexity.r(t) is quasi-convex in t.
5. (25). The root equation is equivalent to r=y(t)/exp(1+r) with y(t)=∑iexp(⋅), so r(t) increases with y(t).
6. Convexity of y.y is convex in t.
Milestones 2–4 and 5–6 are the paper's two routes from (24) to Theorem 3. A further item states the universal reading of Theorem 3 (every optimal uniform duration is ts or tl) under ts<tl and the non-degeneracy assumption that some product has bi=0 or ai=si.
Significance
Theorem 3 is the basis of the paper's Section 3. It shows that a firm restricted to one service policy should still go to an extreme, and it makes the uniform benchmark a comparison of two candidate durations. Comparing that benchmark with Theorem 1's differentiated optimum measures the value of service differentiation, which the paper reports numerically. Equation (24) also gives the optimal profit at every uniform duration as the root of a scalar equation, which is the form any sensitivity analysis in t starts from.
On the formal side, the paper's results are proved on paper but, as far as is known, none is machine-checked. The mission requires formalizing the reduction of the joint MNL price–quality problem to a scalar fixed point (the equal-markup property of Li and Huh, extended to quality), an implicit-function derivative and a Cauchy–Schwarz step, or alternatively a convexity argument. The equal-markup reduction is shared with missions I and VI of this series.
Difficulty
The obvious argument fails at the first step: the MNL profit is not jointly concave in the price vector (Hanson and Martin 1996), let alone in prices, qualities and the duration together, so "maximize a concave function and check the endpoints" does not apply. The extreme-point structure holds only after prices and qualities have been optimized out, and that requires knowing the optimal profit at each t exactly: as the root of (24), a fixed-point equation in which r appears on both sides. The global optimality in (24) is itself the hard part, since a first-order condition alone does not give a global maximum of a non-concave function on R2N.
Formalization scope
Conventions committed to in Lean:
Products are Fin N, 0-based; N=0 is allowed. The outside option is the constant 1 in the MNL denominator, not a product.
Parameters α,a,b,c,s:Fin N→R, with only ci>0 assumed; no sign on bi, and bi=0 is allowed.
Prices and qualities range over all of RN. The model's normalization qi∈[0,ai/bi) (p. 8) is not imposed, matching the paper's derivation of qi=(αi+tbi)/(2ci) by a first-order condition.
A uniform duration is the constant vector fun _ => t; the goal assumes ts≤tl.
"Optimal" means a global maximizer; existence of an optimum is part of the goal's conclusion.
The goal is the existential reading of Theorem 3. The universal reading is false in the degenerate case bi=0, ai=si for all i, where the optimal profit does not depend on t, and is stated separately with that case excluded.
The root r(t) is not a definition: milestones quantify over any function R with R(t)=∑iGi(R(t),t) for every t, which (24) shows is unique.
These formalizations would trivialize the goal and are ruled out: a single product (then Theorem 3 is Theorem 1(a)); qualities fixed rather than chosen; a duration vector t∈[ts,tl]N instead of one shared t; and an existential statement in which t∗ may be any point of [ts,tl].
The definitions needed are the MNL choice probability and profit, plus the scalar functions Gi, Ai and y of the proof. Mathlib's QuasiconvexOn, ConvexOn, HasDerivAt and Finset.sum_mul_sq_le_sq_mul_sq cover the rest. A proof of (24), the global optimality of equal markups and per-product quality under MNL, would be reusable across the whole series. Contributions to any milestone are welcome.
H. Li, W. T. Huh, Pricing multiple products with the multinomial logit and nested logit models: concavity and implications, Manufacturing & Service Operations Management 13(4) 549–564, 2011. https://doi.org/10.1287/msom.1110.0344
G. Gallego, R. Wang, Price optimization and competition for multi-products under the nested logit model with product-differentiated price coefficients, Operations Research 62(2) 450–461, 2014. https://doi.org/10.1287/opre.2013.1249
On the tightness of SDP relaxations of QCQPs 5: The Multiplicity Bound k ≥ aff dim{b(γ) : γ ∈ F} + 1 Cannot Be Lowered by OneResearch Paper
Motivation
A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. QCQPs contain max-cut, binary programming, the trust-region subproblem and many problems from signal processing and control, and are NP-hard in general. The standard convex approach is the Shor semidefinite relaxation, which lifts x to the matrix Y=(1xx⊤xx⊤) and relaxes xx⊤ to an arbitrary positive semidefinite completion. Two questions decide how useful the relaxation is for a given QCQP: is its optimal value equal to the QCQP's (SDP exactness), and does its projected epigraph equal the convex hull of the QCQP's epigraph (convex hull exactness)?
A. L. Wang and F. Kılınç-Karzan (arXiv:1911.09195v3, Math. Program. 2021) give sufficient conditions for both, in terms of the faces of a dual set Γ and a symmetry parameter k, the quadratic eigenvalue multiplicity. Their Theorems 1 and 2 require Γ to be polyhedral and k≥affdim{b(γ):γ∈F}+1 on every semidefinite face F. This mission formalizes §4.3 of the paper, which shows that neither hypothesis can be weakened on its own.
Timeline. Fujie and Kojima (1997) recorded the dual description of the SDP value used here. Ye and Zhang (2003) and Beck and Eldar (2006) gave sufficient conditions under which the trust-region subproblem with one additional quadratic inequality has a tight SDP relaxation; Locatelli (2016) gave an exactness condition for a variant of the trust-region subproblem, and Burer and Ye (2019) for diagonal QCQPs. Wang and Kılınç-Karzan (2020) unified these conditions through the facial structure of Γ, and showed in their Propositions 2 and 3 that their own hypotheses are sharp.
Setting
A QCQP in N variables with m≥1 constraints, mI of them inequalities, is
with qi(x)=x⊤Aix+2bi⊤x+ci, Ai∈SN. Its epigraph is D={(x,t):q0(x)≤2t,x feasible}. With Qi=(cibibi⊤Ai) and Y=(1xx⊤X), the SDP relaxation minimizes ⟨Q0,Y⟩ subject to ⟨Qi,Y⟩≤0 or =0 and Y⪰0; its value is OptSDP, and DSDP is the set of (x,t) for which some feasible X has ⟨Q0,Y⟩≤2t.
For γ∈Rm write A(γ)=A0+∑iγiAi, b(γ)=b0+∑iγibi and q(γ,x)=q0(x)+∑iγiqi(x). The dual set is
Γ={γ∈Rm:A(γ)⪰0,γi≥0∀i∈[[mI]]}.
Assumption 1: the QCQP is feasible and A(γ∗)≻0 for some γ∗ with γi∗≥0 on the inequalities. Assumption 2: supγ∈Γq(γ,x) is attained whenever it is finite. Assumption 3: Γ is polyhedral. A faceF of Γ is definite if some γ∈F has A(γ)≻0, and semidefinite otherwise. The quadratic eigenvalue multiplicity is the largest k such that every Ai equals Ik⊗Ai for some Ai∈Sn, N=kn.
The Lean development uses the same names: QCQP N m, Opt, OptSDP, D, DSDP, Gamma, bγ, qγ, Assumption1–Assumption3, IsSemidefiniteFace, IsQuadEigMult, affdim.
The milestones pin the paper's witness, the QCQP (13): min{−x12−xn+12−⋯−x(k−1)n+12:∥x∥2≤1,x(j−1)n+1=0∀j}.
Lemma 1: under Assumption 1, DSDP={(x,t):supγ∈Γq(γ,x)≤2t} and OptSDP=minxsupγ∈Γq(γ,x).
Assumption 1 holds for (13).
For (13), Γ={γ:γ1≥1}, so Assumption 3 holds.
For (13), affdim{b(γ):γ1=1}=k.
For (13), OptSDP≤supγ∈Γq(γ,0)=−1 and Opt=0.
Companion: Proposition 3
There is a QCQP in N=2 variables with m=2 constraints satisfying Assumptions 1 and 2, with multiplicity k=1 and k≥affdim{b(γ):γ∈F}+1 on every semidefinite face, but with Opt=OptSDP. The companion items about its witness (14) state Γ=B(0,2−1/2), supγ∈Γq(γ,x^)=q0(x^)+∥x^∥2, OptSDP=1/2 and Opt=1.
Significance
The result. Theorems 1 and 2 of the paper are the general sufficient conditions behind many earlier exactness results for SDP relaxations. Propositions 2 and 3 show that the two hypotheses are each necessary in the sense that relaxing either one by the smallest possible amount produces a counterexample: lowering the multiplicity bound by one, or replacing polyhedrality by mere attainment of the dual supremum. Anyone trying to extend the theorems therefore has to change the form of the conditions, not just their constants.
Formalizing it. Both propositions are proved in the paper; none of this has been machine-checked. A formal proof requires Lemma 1, a strong-duality statement for a parametric SDP that is reusable across the whole paper, and explicit computations of faces, affine dimensions and multiplicities for two concrete families. The multiplicity claim in particular ("the largest k") is asserted but not argued on the page, and a formal proof must supply it.
Difficulty
The concrete computations for (13) and (14) are elementary in isolation; the work lies in three places. First, Lemma 1 is a conic duality statement, including attainment of the outer minimum, that depends on Assumption 1; it is the bridge from the SDP to the dual set, and Mathlib has no semidefinite duality theory to build on. Second, the face structure: one must show that the hyperplane {γ1=1} is the only semidefinite face of the halfspace Γ of (13), and that every face of the disk Γ of (14) gives a single point b(γ)=b0. Third, "the multiplicity is k" requires ruling out every larger block structure Ik′⊗Ai, not only exhibiting one of size k. A naive witness with only Ai=Ik⊗Ai shown would establish a lower bound on the multiplicity, which is not the statement.
Formalization scope
Points of RN are Fin N → ℝ; the paper's constraint i is index i−1 of Fin m, and constraint i is an inequality exactly when its index is below mI. Opt and OptSDP are infima in EReal, so infeasible and unbounded programs take the values ±∞ rather than a junk real. A supremum bound supγ∈Γq(γ,x)≤2t is written as q(γ,x)≤2t for every γ∈Γ. Faces are nonempty convex extreme subsets of Γ. The quadratic eigenvalue multiplicity is the greatest k admitting a block form, under the identification of block j, entry s with coordinate s+nj. Proposition 3 says "n=2 variables"; the construction lives in R2, so the formal statement uses N=2.
The goal is existential, as on the page, and a solver may exhibit any witness; it cannot be met trivially, because the multiplicity must equal k exactly, the dimensions N=nk, m=k+1 are fixed by the type, and both Opt=OptSDP and conv(D)=DSDP are required.
The QCQP (13) is given in full: the page states only the matrices Ai, and the linear terms encode the constraints x(j−1)n+1=0 as qj+1(x)=x(j−1)n+1. Lemma 1 is the reusable piece, and proofs of it are welcome independently of this mission; so are general lemmas on faces of halfspaces and balls and on Kronecker block structure.
T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, Journal of Global Optimization 10 (1997) 367–380. https://doi.org/10.1023/A:1008282830093
S. Burer, Y. Ye, Exact semidefinite formulations for a class of (random and non-random) nonconvex quadratic programs, Mathematical Programming 181 (2019) 1–17. https://doi.org/10.1007/s10107-019-01367-2
M. Locatelli, Exactness conditions for an SDP relaxation of the extended trust region problem, Optimization Letters 10(6) (2016) 1141–1151. https://doi.org/10.1007/s11590-016-1001-0
A. Beck, Y. C. Eldar, Strong duality in nonconvex quadratic optimization with two quadratic constraints, SIAM Journal on Optimization 17(3) (2006) 844–860. https://doi.org/10.1137/050644471
On the tightness of SDP relaxations of QCQPs 2: Polyhedral Γ with 0 ∉ Proj_V(F){b(γ) : γ ∈ F} on Every Semidefinite Face Makes Every SDP Optimizer FeasibleResearch Paper
Why SDP exactness for QCQPs matters
A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. The class contains nonconvex problems such as max-cut, Boolean least squares, the trust-region subproblem and its generalizations, and robust least squares, and it is NP-hard in general. The standard convex approach is the Shor semidefinite relaxation: lift x to the matrix Y=(1xx⊤X)⪰0 and linearize. The relaxation always gives a lower bound OptSDP≤Opt. When the bound is exact, the nonconvex problem is solved by one semidefinite program, and an optimizer of the QCQP can be read off the SDP solution.
Earlier exactness results cover special structure: problems with a single constraint (the S-lemma), diagonal QCQPs under sign conditions (Burer–Ye 2019), and the extended trust-region problem under a perturbation condition (Locatelli 2016). A. L. Wang and F. Kılınç-Karzan (arXiv:1911.09195, Math. Program. 2021) give a single framework that produces sufficient conditions for both exactness (Opt=OptSDP) and the stronger convex-hull property (conv(D)=DSDP). Both kinds of condition are stated through the faces of a dual object Γ. This mission formalizes the exactness result for polyhedral Γ, Theorem 3 of §5.
Setting
Fix N≥0 variables and m≥1 constraints, of which the first mI are inequalities and the remaining mE=m−mI equalities. For i=0,…,m let qi(x)=x⊤Aix+2bi⊤x+ci with Ai symmetric. The QCQP is
and its epigraph is D={(x,t):q0(x)≤2t,x feasible}. With Qi=(cibibi⊤Ai), the SDP relaxation minimizes ⟨Q0,Y⟩ over Y=(1xx⊤X)⪰0 with ⟨Qi,Y⟩≤0 or =0. Its value is OptSDP, and its projected epigraphDSDP is the set of (x,t) for which some X is feasible with ⟨Q0,Y⟩≤2t.
For multipliers γ∈Rm put A(γ)=A0+∑iγiAi, b(γ)=b0+∑iγibi, and the Lagrangian q(γ,x)=q0(x)+∑iγiqi(x). The dual object is
Γ={γ∈Rm:A(γ)⪰0,γi≥0(i≤mI)}.
A faceF of Γ is definite if some γ∈F has A(γ)≻0, and semidefinite otherwise. A semidefinite face has the shared zero eigenspaceV(F)={v:A(γ)v=0∀γ∈F}. For x^∈RN, F(x^)=argmaxγ∈Γq(γ,x^).
The standing hypotheses are Assumption 1 (the QCQP is feasible and some γ∗ with γi∗≥0 for i≤mI has A(γ∗)≻0) and Assumption 3 (Γ is polyhedral). ProjV denotes the orthogonal projection onto a subspace V.
Formalization targets
Goal: Theorem 3 (p. 23)
Under Assumptions 1 and 3, suppose that every semidefinite face F of Γ satisfies
0∈/ProjV(F){b(γ):γ∈F}.
Then every (x∗,t∗)∈argmin(x,t)∈DSDP2t lies in D, and in particular
Opt=OptSDP.
Milestones
Lemma 1 (p. 7): under Assumption 1, DSDP={(x,t):supγ∈Γq(γ,x)≤2t} and OptSDP=minxsupγ∈Γq(γ,x).
Lemma 2 (p. 9): a semidefinite face has a unit vector in V(F).
Lemma 3 (p. 9): under Assumptions 1 and 2, a point of DSDP whose face F(x^) is definite lies in D.
Lemma 8 (p. 13): for polyhedral Γ, Γ=Γe+cone(Γr) with polytopes Γe,Γr, and F(x^)=Fe(x^)+cone(Fr(x^)).
Separation step of the proof of Theorem 3 (p. 24): on a semidefinite face satisfying the hypothesis, some nonzero v∈V(F) and ϵ>0 have v⊤b(γ)≤−ϵ for all γ∈F.
Companion: Theorem 4 (p. 25)
If a sequence hj→0 in RN has 0∈/ProjV(F){b(γ)+hj:γ∈F} for every semidefinite face and every j, then Opt=OptSDP.
Significance
Theorem 3 gives exactness without the convex-hull property, and the paper uses it to recover known exactness results: Proposition 5 (p. 28) shows that the hypotheses of the Burer–Ye theorem for diagonal QCQPs imply those of Theorem 3, and Proposition 4 (p. 27) shows that Locatelli's hypotheses for the extended trust-region problem imply those of Theorem 4. The conclusion is also algorithmic: the x-block of any optimal lifted matrix of the SDP is optimal for the QCQP, so no rounding is needed. Theorem 4 extends exactness to limits of problems satisfying the condition; Example 4 is a problem where the SDP is exact but conv(D)=DSDP.
The results are proved in the paper; none of them has a machine-checked proof. A formalization adds a checked version of the Lagrangian description of the Shor relaxation (Lemma 1), which every SDP-exactness argument for QCQPs uses, and a reusable Minkowski–Weyl decomposition of the faces of a polyhedral dual set (Lemma 8).
Difficulty
The natural attempt is to show directly that an SDP optimizer (x∗,t∗) is feasible for the QCQP. This works when the face F(x∗) is definite (Lemma 3), but nothing in the SDP forces that. When the face is semidefinite, the multipliers on it give no curvature in the directions of V(F). The difficulty is to rule out a semidefinite optimal face using only first-order information about b(γ) on that face. The argument must also control every multiplier off the face uniformly, which is where polyhedrality enters, through the finitely many extreme points and rays of Lemma 8. The paper's argument for Theorem 3 uses polyhedrality at exactly this point.
Lemma 1 itself needs conic duality with attainment: strict feasibility of the dual SDP from Assumption 1, and a minimax step to identify the value.
Formalization scope
A QCQP is a structure QCQP N m with symmetric A₀, A i, vectors b₀, b i, scalars c₀, c i, and mI ≤ m. Constraint i : Fin m is the paper's constraint i+1 and is an inequality iff i < mI. The paper's standing assumption m≥1 (p. 1) is a hypothesis of the goal and of Theorem 4.
Opt and OptSDP are infima in EReal, so infeasibility and unboundedness are representable and no default value enters. "supγ∈Γq(γ,x)≤2t" is written as a bound for every γ∈Γ.
Faces are nonempty convex extreme subsets of Γ. The empty face plays no role in the paper.
The projection is the orthogonal projection in EuclideanSpace ℝ (Fin N), because Fin N → ℝ carries the sup norm.
"Any optimizer of 2t over DSDP" is a point of DSDP with 2t∗≤2t for all points of DSDP. Existence of an optimizer is not assumed, and Opt=OptSDP is stated as a separate conclusion.
Lemma 8 formalizes Fr(x^) as a subset of Γr. The page prints Γe, a slip that the proof and its uses correct.
The goal assumes neither that F(x∗) is definite nor any separating vector. Those are milestones, so the goal cannot be closed by restating a hypothesis.
A complete development needs conic (SDP) strong duality with attainment, a Minkowski–Weyl theorem for polyhedra in Rm, faces of convex sets, strict separation of a point from a closed convex set, and closedness of linear images of polyhedra. All of these are reusable beyond this mission. Proofs of the milestones, of these general tools, and of the optional comparisons with Burer–Ye and Locatelli (Propositions 4, 5) are welcome.
T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, Journal of Global Optimization 10(4) (1997) 367–380.
S. Burer, Y. Ye, Exact semidefinite formulations for a class of (random and non-random) nonconvex quadratic programs, Mathematical Programming 181 (2019) 1–17.
M. Locatelli, Exactness conditions for an SDP relaxation of the extended trust region problem, Optimization Letters 10(6) (2016) 1141–1151.
On the tightness of SDP relaxations of QCQPs 3: Quadratic Eigenvalue Multiplicity k ≥ m + 2 Gives conv(D) = D_SDP Without PolyhedralityResearch Paper
Motivation
A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. The class contains nonconvex problems such as binary programs, max-cut, the trust-region subproblem and many problems in signal processing and control. A standard convex approximation is the Shor semidefinite programming (SDP) relaxation, which replaces the rank-one matrix xx⊤ by a positive semidefinite matrix X⪰xx⊤. The relaxation always gives a lower bound; the question studied by Wang and Kılınç-Karzan (arXiv:1911.09195v3, Math. Program. 2020, doi:10.1007/s10107-020-01589-9) is when it is tight, either in the sense of objective values or in the stronger sense that the relaxation describes the convex hull of the problem's epigraph.
Earlier exactness results are of two kinds. One kind concerns special structure: one constraint (the S-lemma, the trust-region subproblem), or two constraints under extra conditions. The other kind, due to Beck (Quadratic matrix programming, SIAM J. Optim. 2007, Corollary 4.4), exploits block symmetry: if every quadratic form is of the form Ik⊗Ai with k≥m, the SDP bound equals the optimal value. The paper under formalization recasts both kinds in one framework. Its convex hull results (Theorems 1 and 2) assume that a certain dual set Γ is polyhedral, and its Proposition 3 shows that without polyhedrality the convex hull result can fail. This mission is about Theorem 7, which removes the polyhedrality assumption at the price of a larger symmetry parameter.
Setting
Fix N≥1 variables and m=mI+mE≥1 constraints. For i∈[[0,m]] let qi(x)=x⊤Aix+2bi⊤x+ci with Ai a symmetric N×N matrix, bi∈RN and ci∈R. The QCQP is
Its epigraph is D={(x,t)∈RN×R:q0(x)≤2t,x feasible for (1)}. With Qi=(cibibi⊤Ai) and Y=(1xx⊤X), the Shor relaxation imposes Y⪰0, ⟨Qi,Y⟩≤0 for inequalities and ⟨Qi,Y⟩=0 for equalities; its projected epigraphDSDP is the set of (x,t) for which some symmetric X satisfies these constraints and ⟨Q0,Y⟩≤2t. Always conv(D)⊆DSDP.
For γ∈Rm write A(γ)=A0+∑iγiAi and q(γ,x)=q0(x)+∑iγiqi(x), and let Γ={γ:A(γ)⪰0,γi≥0∀i∈[[mI]]}. Assumption 1 asks that (1) be feasible and that A(γ∗)≻0 for some γ∗ that is nonnegative on the inequality indices.
The quadratic eigenvalue multiplicity (Definition 3) is the largest integer k such that N=kn and, for every i∈[[0,m]], Ai=Ik⊗Ai for some symmetric n×n matrix Ai. Here Ik⊗A is block diagonal with k copies of A, and for y∈Rk, z∈Rn the vector y⊗z∈RN has j-th block yjz. Every QCQP has multiplicity at least 1.
Formalization targets
Goal: Theorem 7 (p. 29)
Assumption 1 and k≥m+2⟹conv(D)=DSDP.
Milestones (in the order of the proof)
Lemma 1 (p. 7): under Assumption 1, DSDP={(x,t):supγ∈Γq(γ,x)≤2t} and OptSDP=minxsupγ∈Γq(γ,x).
A(γ)⪰0⟺A(γ)=A0+∑iγiAi⪰0 (p. 29).
Under Assumption 1, every (x^,t^)∈DSDP admits Z∈Sn with Z⪰0, q0(x^)+⟨A0,Z⟩≤2t^, qi(x^)+⟨Ai,Z⟩≤0 on inequalities and =0 on equalities: the system (17), p. 29.
If k≥m+2, for any x^ and z there is a unit y∈Rk with ⟨Aix^+bi,y⊗z⟩=0 for all i∈[[0,m]]: the system (18), p. 30.
If k≥m+2, every (x^,t^,Z) satisfying (17) has (x^,t^)∈conv(D) (pp. 29–30).
A supporting item (not a milestone) states the expansion used in the induction step: for A=Ik⊗A with A symmetric and unit y, q(x^±y⊗z)=q(x^)±2⟨Ax^+b,y⊗z⟩+⟨A,zz⊤⟩ (p. 30).
Significance
The result. Theorem 7 is the convex hull counterpart of Beck's value-exactness result: under Assumption 1 and enough block symmetry, the Shor relaxation does not merely give the right optimal value but describes conv(D) exactly, so every linear objective in (x,t) over the relaxation is exact. It needs neither the polyhedrality of Γ nor the attainment Assumption 2 used elsewhere in the paper. Problems with this structure include quadratic matrix programs (Beck 2007), in which the variable is a matrix X∈Rn×k and every quadratic form is a trace tr(X⊤AiX). The companion Theorem 8 (a separate mission of this series) relaxes k≥m+2 to k≥m+1 at the price of intersecting with the optimal hyperplane, and Remark 14 records that the authors conjecture these thresholds are sharp.
The formalization. Theorem 7 is proved in the paper; no machine-checked proof of it, or of the Shor relaxation's convex hull results in general, is known. The milestones isolate the three ingredients of the proof as reusable statements: the dual description of DSDP (Lemma 1, shared with the polyhedral results of the paper), conic duality applied to a Kronecker-structured SDP, and a rank-reduction argument for Kronecker-structured quadratic forms.
Difficulty
The inclusion conv(D)⊆DSDP is immediate; the content is the reverse inclusion. A point of DSDP comes with a matrix X⪰xx⊤, and the naive idea is to decompose X−xx⊤ into rank-one pieces and move x along them. In RN this fails in general: moving along an arbitrary direction changes each constraint by a first-order term that cannot be controlled, and Proposition 3 of the paper exhibits a QCQP with conv(D)=DSDP. The theorem therefore depends on the Kronecker structure and on the count k≥m+2 in an essential way, and on an exact dual certificate, whose existence needs the strict feasibility of Assumption 1 and a dual attainment theorem for SDPs that is not yet in Mathlib.
Formalization scope
All objects are defined locally in the namespace QCQPTightness.MultHull.
Variables live in Fin N → ℝ; constraints are indexed by Fin m, the paper's constraint i+1 being index i, and index i is an inequality iff i<mI. The standing assumption m≥1 (p. 1) is a hypothesis of the goal.
Opt, OptSDP and supγ∈Γq(γ,x) are taken in EReal, so an empty or unbounded set never produces the junk value of a real infimum. "supγ∈Γq(γ,x)≤2t" is stated as q(γ,x)≤2t for all γ∈Γ.
⟨Q,Y⟩ is tr(QY); ⪰0 and ≻0 are Mathlib's PosSemidef and PosDef; conv is convexHull ℝ in RN×R.
Ik⊗A is Mathlib's Kronecker product, transported to Fin N by (j,s)↦s+nj; y⊗z uses the same map.
The goal uses the largest k (IsQuadEigMult k) exactly as Definition 3. The milestones are stated for an arbitrary explicit representation Ai=Ik⊗Ai, which makes them at least as strong. Milestone 2 carries k≥1, which the paper notes always holds.
The goal does not assume the existence of a certificate Z for (17): that existence is milestone 3 and is where Assumption 1 is used. A formalization that assumes it, or that drops Assumption 1, states a different theorem.
A complete development needs: SDP strong duality with dual attainment under a Slater condition (the platform's ConvexOptimization.sdp_strong_duality states a related form), the spectral decomposition of a positive semidefinite matrix into rank-one terms, Kronecker product identities for block-diagonal matrices, and the existence of nonzero solutions of underdetermined homogeneous linear systems. The duality and Kronecker lemmas are reusable beyond this mission; proofs of any milestone are welcome.
A. Beck, Quadratic matrix programming, SIAM Journal on Optimization 17(4):1224–1238, 2007 (reference [5] of the paper).
T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, Journal of Global Optimization 10(4):367–380, 1997 (reference [26] of the paper).
N. Z. Shor, Dual quadratic estimates in polynomial and boolean programming, Annals of Operations Research 25:163–168, 1990 (reference [47] of the paper).
Product Price, Quality and Service Decisions under Consumer Choice Models I: Under MNL Demand, Optimal Service Durations Are Extreme, Qualities Are Set Product by Product, and Markups Are EqualResearch Paper
Motivation
Manufacturers rarely sell a bare product. A laptop, a vacuum cleaner or a car comes with an ancillary service (a factory warranty, maintenance, technical support) whose length the firm chooses together with the price and the quality of the product. The three decisions interact: a longer warranty makes a product more attractive to consumers but costs the firm more, and how much more depends on quality, since a more reliable product fails less often while a more complex one may be costlier to service. Firms in practice offer very few service options across large product lines: Amazon's Fire tablets come with either a 90-day or a 1-year warranty, and Dyson's vacuum cleaners with either a 2-year or a 5-year warranty.
Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study the joint choice of price, quality and service duration for a firm selling substitutable products to consumers who choose according to the multinomial logit (MNL) model. Their first main result, Theorem 1, explains the observation above: under MNL demand, every product's optimal service duration is either the shortest or the longest allowed. The same theorem gives the optimal quality in closed form and shows that all products carry the same optimal markup, extending the equal-markup property of MNL price optimization (Li and Huh 2011, doi:10.1287/msom.1110.0335; Li, Rusmevichientong and Topaloglu 2015, doi:10.1287/opre.2015.1355) to quality and service.
Setting
A firm sells products i∈N={1,…,N}. For product i it chooses a price pi∈R, a quality level qi∈R and a service duration ti in a fixed interval [ts,tl] of admissible durations. The parameters of product i are:
αi, the consumers' sensitivity to quality;
si, the consumers' utility from one unit of service time;
ci>0, the production-cost coefficient (unit production cost ciqi2);
ai and bi, the base service cost per unit time and the effect of quality on it (service cost ai−biqi per unit time). The sign of bi is not fixed: bi>0 when quality improves reliability, bi<0 when it adds complexity, bi=0 when it is irrelevant to service.
A consumer buys product i with the MNL probability
the 1 in the denominator being the option to buy nothing. The markup of product i is pi−ciqi2−ti(ai−biqi), and with the market size normalized to one the firm's total expected profit is
The firm solves problem (4): maximize Π over p∈RN, q∈RN and t∈[ts,tl]N. In Lean the model is PriceQualityService.Joint.Model (attraction, choiceProb, markup, profit, and the exponent φi(τ) below as durationExponent).
Formalization targets
Goal: Theorem 1
Write φi(τ)=4cibi2τ2+(si−ai+2ciαibi)τ+4ciαi2. Theorem 1 asserts that problem (4) has an optimal solution (p∗,q∗,t∗) with
and that r∗ equals the optimal profit. The goal also states the converse: every optimal solution has this quality and price structure, and, when ts<tl, every optimal duration of a product with bi=0 or ai=si is ts or tl.
Milestones
The milestones follow the proof in Appendix B: the fixed-point form (15) of the profit; the price step (each markup is 1+r); the price-only optimum (17); the quality step (18); the duration step (19); uniqueness of the root r∗; and Proposition 2, which says which endpoint is optimal for each product.
Significance
Theorem 1 reduces a 3N-dimensional nonconcave optimization over prices, qualities and durations to a choice between two durations per product, decoupled across products, plus a one-dimensional equation for the common markup. Proposition 2 then settles each product's duration by comparing a threshold built from its own parameters with the midpoint (ts+tl)/2. The same reduction underlies the later results of the paper: the oligopoly equilibrium, the uniform-service problem, the nested logit extension and the consumer-surplus comparisons all rest on the fixed-point characterization of the optimal profit.
The theorem is proved in the paper; no machine-checked proof exists. This mission formalizes the model and the theorem with its explicit constants, including the uniqueness of r∗, the claim that r∗ is the optimal profit, and the existence of an optimum, which the paper's argument takes for granted. The fixed-point form of MNL profit is a reusable tool for any MNL pricing model with additive utilities.
Difficulty
The profit function is not concave in prices, qualities or durations jointly, so first-order conditions alone do not identify a maximum. The obvious argument (set every partial derivative to zero) yields stationary points without showing that any of them is a global maximum, and says nothing at the boundary of [ts,tl], where the optimum actually lies. The three decisions are also coupled through the shared MNL denominator: changing one product's price or quality changes every product's demand, so the claim that each quality is set from the product's own parameters, and that all markups coincide, is not visible coordinate by coordinate. Finally, the statement must hold for every sign of bi: for bi=0 the dependence on the duration is linear rather than quadratic, and when moreover ai=si every duration is optimal, so the "every optimum is extreme" clause has to exclude exactly that case.
Formalization scope
Products are Fin N, 0-based; the paper's product i is index i−1. Any N≥0 is allowed; for N=0 the optimal profit is r∗=0.
The outside option is the "1+" in the MNL denominator, not an element of Fin N.
Prices and qualities range over all of R. The model's normalization qi∈[0,ai/bi) (p. 8) is not imposed, as in the paper's proof, which maximizes over qi∈R.
Durations satisfy ti∈[ts,tl] with ts≤tl; the universal "every optimal duration is extreme" clause assumes ts<tl.
ci>0 for every product (the paper's increasing convex production cost); no other sign is assumed, and bi may be positive, negative or zero.
"Optimal" means a global maximizer over the whole feasible set, and the existence of an optimum is part of the goal, not a hypothesis.
The MNL formula is the definition of the choice probability; its derivation from Gumbel utilities is not part of this mission.
A formalization that fixes N=1 or identical products, fixes the sign of bi, states only first-order conditions, or defines r∗ or the optimum by the paper's formula is not this theorem and is ruled out.
The development needs only real analysis from Mathlib: the exponential function, monotonicity of one-variable functions, convexity of exp composed with a convex quadratic, and finite sums. Proofs of any milestone, alternative arguments for the goal, and reusable lemmas on the fixed-point form of MNL profit are welcome.
H. Li, W. T. Huh, Pricing Multiple Products with the Multinomial Logit and Nested Logit Models: Concavity and Implications, Manufacturing & Service Operations Management 13(4), 549–564, 2011. https://doi.org/10.1287/msom.1110.0335
G. Li, P. Rusmevichientong, H. Topaloglu, The d-Level Nested Logit Model: Assortment and Price Optimization Problems, Operations Research 63(2), 325–341, 2015. https://doi.org/10.1287/opre.2015.1355
D. McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in Frontiers in Econometrics, P. Zarembka (ed.), Academic Press, New York, 105–142, 1974.
On the tightness of SDP relaxations of QCQPs 4: Quadratic Eigenvalue Multiplicity k ≥ m + 1 Gives conv(D ∩ H) = D_SDP ∩ H and Opt = Opt_SDPResearch Paper
Motivation
A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. QCQPs model trust-region subproblems, max-cut and other binary programs, phase retrieval, and many problems in signal processing and control; in general they are NP-hard. The standard tool for bounding and solving them is the Shor semidefinite relaxation (Shor 1990), which lifts the variable x to a matrix Y=(1xx⊤X)⪰0 and replaces every quadratic term by a linear function of Y. The relaxation is a convex program, so it can be solved efficiently, but it is only useful when one knows that it is tight: that its optimal value equals that of the QCQP, or, more strongly, that it describes the convex hull of the QCQP's epigraph.
Wang and Kılınç-Karzan (arXiv:1911.09195v3, Math. Program. 2021) give sufficient conditions for tightness. Section 6 of the paper concerns QCQPs with symmetry: when every quadratic form is k identical copies of one smaller form, Ai=Ik⊗Ai. Such problems arise as quadratic matrix programs in the sense of Beck 2007, where the variable is a matrix and the objective and constraints are traces of quadratic matrix expressions. Beck showed (Corollary 4.4) that k≥m gives value exactness under a regularity assumption; Theorem 7 of the paper gives the convex-hull result for k≥m+2; this mission's Theorem 8 covers k≥m+1.
Setting
Fix N≥1 variables and m=mI+mE≥1 constraints. For i∈[[0,m]] let qi(x)=x⊤Aix+2bi⊤x+ci with Ai∈SN symmetric, bi∈RN, ci∈R. The QCQP is
and its projected epigraphDSDP is the set of (x,t) for which some X satisfies the constraints with ⟨Q0,Y⟩≤2t. Always conv(D)⊆DSDP and Opt≥OptSDP.
For γ∈Rm write A(γ)=A0+∑iγiAi and q(γ,x)=q0(x)+∑iγiqi(x), and let Γ={γ:A(γ)⪰0,γi≥0∀i∈[[mI]]}. Assumption 1 requires that the QCQP be feasible and that some γ∗ with γi∗≥0 on the inequalities have A(γ∗)≻0.
The quadratic eigenvalue multiplicity (Definition 3) is the largest integer k such that N=kn and every Ai, i∈[[0,m]], equals Ik⊗Ai for some Ai∈Sn. Finally,
H={(x,t)∈RN+1:2t=OptSDP}
is the hyperplane on which the SDP relaxation attains its value.
Formalization targets
Goal: Theorem 8 (p. 30)
Under Assumption 1, if k≥m+1, then
conv(D∩H)=DSDP∩HandOpt=OptSDP.
Milestones (App. B, pp. 35–36)
Lemma 1 (p. 7): DSDP={(x,t):supγ∈Γq(γ,x)≤2t} and OptSDP=minxsupγ∈Γq(γ,x).
Dual attainment: every (x^,t^)∈DSDP∩H has Z∈Sn with
Feasibility of (20): if k≥m+1, some unit y∈Rk has ⟨Aix^+bi,y⊗z⟩=0 for all i∈[[m]].
The objective direction vanishes: on DSDP∩H, with Z=zz⊤+Z′, Z′⪰0, and y as in (20), ⟨A0x^+b0,y⊗z⟩=0.
Rank induction: if k≥m+1, every (x^,t^)∈H with some Z satisfying (19) lies in conv(D∩H).
Significance
Theorem 8 says that one copy of symmetry fewer than Theorem 7 requires still makes the SDP relaxation exact in value, and identifies the relaxation's optimal set: every optimal point of the relaxation, projected to (x,t), is a convex combination of optimal epigraph points of the QCQP. In particular the relaxation's optimal points can be decomposed into QCQP optima, which is what makes the relaxation a solution method and not only a bound. Remark 14 of the paper places the result between Beck's k≥m (only D∩H=∅) and Theorem 7's k≥m+2 (the full convex hull), and records the conjecture that all three thresholds are sharp.
The theorem is proved in the paper (Appendix B). No machine-checked proof of it, or of the multiplicity results of Section 6, is known to exist. A formal proof needs a Lean development of the Shor relaxation, its Lagrangian dual, conic strong duality with dual attainment for an SDP with sign-constrained multipliers, and the Kronecker structure of the data.
Difficulty
The inclusion conv(D∩H)⊆DSDP∩H is routine. The converse needs, for an SDP-optimal point, a decomposition into feasible QCQP points that are themselves optimal. A rank-one decomposition of the SDP matrix X−xx⊤ does not suffice in general: its terms leave the feasible set unless the perturbation directions are orthogonal to all the linear parts Aix^+bi, including the objective's. With multiplicity k≥m+2 there is room for all m+1 orthogonality conditions; with k≥m+1 only the m constraint conditions can be imposed, and the objective condition has to come from elsewhere. The difficulty sits in that last condition and in the conic duality step, whose dual must attain its value under Assumption 1 alone (no polyhedrality of Γ, no attainment assumption).
Formalization scope
The Lean development lives in the namespace QCQPTightness.MultTight. The data are a structure QCQP N m with symmetric Ai, constraints indexed by Fin m, and constraint i an inequality exactly when (i : ℕ) < mI (the paper's inequalities come first). Vectors are Fin N → ℝ; points of RN+1 are pairs (x, t). Opt and OptSDP are infima in EReal, and H is defined from that EReal value; this is why the goal states Opt=OptSDP as a separate conjunct: if OptSDP were ±∞, H would be empty and the first conjunct trivial. ⟨Q,Y⟩ is (Q * Y).trace; Y⪰0 is PosSemidef; Sk−1 is y ⬝ᵥ y = 1. The identification Rk⊗Rn≅RN sends block j, entry s to coordinate s + n * j.
Standing assumptions: the goal carries m≥1 (p. 1) and Assumption 1. The multiplicity is the largest k (IsGreatest), as on the page. The milestones take an explicit representation Ai=Ik⊗Ai instead, which makes them apply to every representation, and drop m≥1 and Assumption 1 where the step does not use them. The rank-induction milestone carries (x^,t^)∈H, which the page's sentence omits but its proof uses ("by minimality of t^"); without it the claim is false.
A trivializing formalization would assume system (19), or the vanishing of ⟨A0x^+b0,y⊗z⟩, in the goal; the goal assumes neither, and both are milestones to be proved.
Reusable infrastructure: the QCQP and Shor-relaxation definitions are shared with the other missions of this series, and a general SDP strong-duality statement exists on the platform (ConvexOptimization.sdp_strong_duality) in a different form (a minimization without sign-constrained variables). Contributions welcome: proofs of the milestones, a conic duality lemma with sign-constrained multipliers, and Kronecker-product lemmas such as (Ik⊗A)(y⊗z)=y⊗Az.
Bridging Bayesian and Minimax Mean Square Error Estimation via Wasserstein Distributionally Robust Optimization 2: The Fully Adaptive Frank-Wolfe Algorithm Converges LinearlyResearch Paper
Motivation
The Frank-Wolfe algorithm (also called the conditional gradient method) minimizes a smooth convex function over a compact convex set using only a linear minimization oracle in place of a projection. Each step solves a linearized problem over the feasible set and moves toward its solution. This makes it the method of choice when projections are expensive but linear subproblems are cheap or have closed-form solutions: nuclear-norm balls, polytopes, and the semidefinite feasible sets that come up in distributionally robust estimation.
Nguyen, Shafieezadeh-Abadeh, Kuhn and Mohajerin Esfahani (arXiv:1911.03539v2, Math. Oper. Res. 48(1), 2023) need such a method for a nonlinear semidefinite program that computes Wasserstein minimax mean square error estimators. Its feasible set is not strongly convex in the traditional sense, and the linear subproblems can only be solved approximately. Section 6.1 of the paper analyses a fully adaptive Frank-Wolfe algorithm under these conditions: it uses an inexact oracle, a backtracking estimate of the smoothness constant, and a weakened, gradient-dependent notion of strong convexity of the feasible set. The section proves a linear convergence rate. This mission formalizes that rate and the lemmas of its proof.
Timeline. Frank and Wolfe (1956) introduced the method for quadratic programs. Levitin and Polyak (1966) proved linear convergence over strongly convex sets when the gradient is bounded away from zero, with the adaptive stepsize (6.4); Garber and Hazan (2015) revisited this regime. Pedregosa, Négiar, Askari and Jaggi (2020) introduced the backtracking line search with adaptive smoothness parameters β_t used here, and proved its sublinear O(1/t) rate. Section 6.1 combines that line search with inexact oracles and blockwise strong convexity with respect to f.
Setting
The decision variable is s=(s[1],…,s[K]) with blocks s[k]∈Rdk, and Rd1×⋯×RdK carries the Euclidean norm ∥s∥2=∑k∥s[k]∥2. The problem is
f⋆=s∈Sminf(s),
where S=×k=1KS[k] is a product of convex compact sets and f is convex and differentiable on S. The partial gradient with respect to block k is ∇[k]f(s).
An inexact oracle with precisionδ∈[0,1] is a map F:S→S with
(F(s)−s)⊤∇f(s)≤δz∈Smin(z−s)⊤∇f(s).
For δ=1 it returns an exact solution of the linearized problem. At a point s the search direction is d=F(s)−s and the surrogate duality gap is g=−d⊤∇f(s)≥0.
Assumption 6.1 consists of three conditions:
β-smoothness: ∥∇f(s)−∇f(sˉ)∥≤β∥s−sˉ∥ on S;
α-strong convexity of the blocks with respect tof: for all s,sˉ∈S, θ∈[0,1] and k,
Algorithm 1 starts from s0∈S with parameters β−1>0, τ>1 and ζ>1. At iteration t it sets dt=F(st)−st and gt=−dt⊤∇f(st). It then picks βt as the smallest element of (βt−1/ζ)⋅{1,τ,τ2,…} that passes the sufficient-decrease test
The result. Theorem 6.2 gives a linear rate for a Frank-Wolfe method that never needs the global smoothness constant β, that tolerates approximate linear subproblems, and that works on feasible sets which are strongly convex only in the weak, gradient-dependent sense of Assumption 6.1 (ii). In the paper it justifies the algorithm used to compute Nash equilibria of Wasserstein minimax MMSE estimation problems at dimensions where interior-point SDP solvers run out of memory. The analysis is generic and applies to any problem meeting Assumption 6.1.
Formalizing it. The result is proved in the paper, but the printed constant is wrong. In Lemma 6.3 (ii) the factor δθ(1−θ)/(1−δθ) is maximized at θ⋆=(1−1−δ)/δ, where it equals (1−1−δ)2/δ; the page drops the square. Lemma 6.3 (ii), (6.12) and Theorem 6.2 are therefore false as printed for δ∈(0,1). A two-dimensional instance (unit disk, linear objective, δ=0.19) violates the printed rate after one step. The printed and corrected rates agree for an exact oracle (δ=1). The mission states the corrected constant throughout and quotes the printed text in the milestones. No machine-checked proof of a linear rate for Frank-Wolfe with adaptive line search is known to us.
Difficulty
The obvious argument, "β-smoothness plus a contraction per step", does not go through directly. The line search may pick βt far below β, so the contraction factor in case (ii) is controlled by βt and needs the separate fact that βt never exceeds max{τβ,β−1}. That fact depends on βt being the smallest accepted trial value, and it fails for an arbitrary accepted one. The lower bound of Lemma 6.3 (ii) comes from testing the oracle inequality against a point built from Assumption 6.1 (ii). That point is assembled block by block, and the step back to ∥dt∥2 uses the Euclidean (not the sup) norm on the product space. The constant then comes from an explicit one-variable optimization, which is where the printed proof errs.
Formalization scope
The space is PiLp 2 (fun k : Fin K => EuclideanSpace ℝ (Fin (d k))), so ‖·‖ is Euclidean and ∇[k]f(s) is the block gradient f s k. Conventions:
f is a function on the whole space, convex on S and differentiable at every point of S;
f⋆ is a real number that is the least element of f(S);
the minimum in (6.2) is written as "≤ δ (z − s)ᵀ∇f(s) for all z ∈ 𝒮", which is equivalent on the compact set 𝒮;
each of β,α,ε is positive and δ∈[0,1];
the run of Algorithm 1 is infinite (no stopping criterion), and "smallest element" is encoded as an index j that passes with all i<j failing;
at dt=0, where the page's stepsize is undefined, Lean's 0/0=0 gives ηt=0.
Disclosed changes relative to the page:
the square in (1−1−δ)2 in Lemma 6.3 (ii), (6.12) and Theorem 6.2;
δ>0 in Lemma 6.3 (ii), and δθ<1 in (6.8), where the page divides by these quantities;
nonzero partial gradients at the point in (6.8) and Lemma 6.3 (ii), so the normalization of Assumption 6.1 (ii) is defined;
(6.10) is stated with −ηtgt, which is what (6.5) gives (the printed −gt is valid only when ηt=1);
the inner-loop iteration count, which contains a typo, is replaced by termination;
minima over k are expressed through an arbitrary lower bound m of all ∥∇[k]f(s)∥.
Trivializing readings are excluded. A sorry-free companion file exhibits, for every δ∈[0,1], an instance (interval [−1,1], linear objective, exact oracle) satisfying every hypothesis of the goal, together with an explicit infinite run whose initial suboptimality is positive. The run predicate forces the smallest accepted βt, and the norm is Euclidean.
Everything needed is in Mathlib: gradients in Hilbert spaces, convexity, PiLp. The descent lemma along a segment for a function with Lipschitz gradient on a convex set, used for (6.9), is reusable beyond this mission. Contributions welcome: proofs of the milestones, and a Lean proof that the printed constant fails on the disk instance.
Selected references
V. A. Nguyen, S. Shafieezadeh-Abadeh, D. Kuhn, P. Mohajerin Esfahani, Bridging Bayesian and Minimax Mean Square Error Estimation via Wasserstein Distributionally Robust Optimization, Math. Oper. Res. 48(1), 2023. arXiv:1911.03539v2, doi:10.1287/moor.2021.1176
M. Frank, P. Wolfe, An algorithm for quadratic programming, Naval Res. Logist. Q. 3, 1956. doi:10.1002/nav.3800030109
E. S. Levitin, B. T. Polyak, Constrained minimization methods, USSR Comput. Math. Math. Phys. 6(5), 1966. doi:10.1016/0041-5553(66)90114-5
D. Garber, E. Hazan, Faster rates for the Frank-Wolfe method over strongly-convex sets, ICML 2015. arXiv:1406.1305
F. Pedregosa, G. Négiar, A. Askari, M. Jaggi, Linearly convergent Frank-Wolfe with backtracking line-search, AISTATS 2020. arXiv:1806.05123
Product Price, Quality and Service Decisions under Consumer Choice Models V: A Dealer Optimally Offers a Markup-Ordered Assortment and Attaches Long Service to an Adjusted-Markup-Ordered SetResearch Paper
Motivation
Car dealers, electronics retailers and office suppliers sell products whose prices and features are set upstream by manufacturers, and bundle each product with a service of their own: maintenance, repairs or a warranty. The dealer's short-term problem is then purely combinatorial. Which products should be carried, and which of them should come with a long rather than a short service? Longer service makes a product more attractive to consumers but costs the dealer more per unit sold, and the cost per unit of service time depends on the product's quality.
Wang, Ke and Cui (SSRN 3766191, accepted at Manufacturing & Service Operations Management) study price, quality and service decisions under multinomial logit (MNL) and nested logit demand. Section 5.2 of the paper treats the dealer's problem and shows that its solution has a two-threshold structure. This mission formalizes that result, Theorem 5, together with the steps of its proof in the Online Supplement.
The single-service version of the question is classical: under MNL demand with fixed prices, the profit-maximizing assortment consists of the products with the highest margins, a revenue-ordered (here: markup-ordered) assortment (Talluri & van Ryzin 2004). Theorem 5 extends this to two service options per product, where the choice is between three actions for each product (not offered, short service, long service) and the margin of each action differs.
Setting
There are products N={1,…,N}. Product i has a fixed price pi and quality qi, a quality sensitivity αi, a service utility per unit time si, a unit production cost ciqi2, and a service cost per unit time ai−biqi. Two service durations are available: a short one ts and a long one tl.
The dealer chooses two disjoint sets Sl,Ss⊆N: products in Sl are offered with service duration tl, products in Ss with ts, and the others are not offered. A product i offered with duration t has attractionexp(αiqi−pi+tsi) and markuppi−ciqi2−t(ai−biqi). Under MNL demand with an outside option, product i∈Sl is bought with probability
A markup-ordered assortment is a set of the products with the highest values of zi; an adjusted markup-ordered set is a set of the products with the highest values of xi.
Formalization targets
Goal: Theorem 5
Assume ts<tl, si>0 and ai−biqi≥0 for all i. There are thresholds θ,θ′ such that, with Si∗={i:zi≥θ} and Sj♮={i:xi≥θ′},
Sj♮⊆Si∗andΠs(p,q;Sl,Ss)≤Πs(p,q;Sj♮,Si∗∖Sj♮) for all disjoint (Sl,Ss).
Part (a) of the paper (a markup-ordered assortment is an optimal offer set) and part (b) (long service on an adjusted markup-ordered subset of it, short service on the rest) are one statement about the same Si∗.
Milestones from the proof (Online Supplement p. 8)
(EC.11). For disjoint (Sl,Ss), r=Πs(Sl,Ss) if and only if r=∑i∈Slhil(r)+∑i∈Sshis(r), where hil(r)=[yi−r]exp(αiqi−pi+tlsi), his(r)=[zi−r]exp(αiqi−pi+tssi) and yi=pi−ciqi2−tl(ai−biqi).
The fixed point.H(r)=maxSl,Ss{∑Slhil(r)+∑Sshis(r)}=∑imax{hil(r),his(r),0}; H is non-increasing; r=H(r) has a unique root r∗, and r∗ is the optimal value of (13).
Breakpoints.xi,yi,zi are the roots of hil=his, hil=0, his=0, and xi≤yi≤zi.
Piecewise form.hi=hil on r≤xi, his on xi<r≤zi, 0 on r>zi.
Level sets at r∗.Sl={xi≥r∗} and Ss={zi≥r∗}∖Sl is an optimal pair with profit r∗.
Significance
Problem (13) has 3N feasible pairs. Theorem 5 reduces the search to at most O(N2) pairs indexed by two thresholds, and it says which products deserve the long service: those with the highest adjusted margin xi, which charges each unit of service cost at the rate Ai>tl rather than at tl. The paper's managerial reading is that high-margin products go with long service, as with retailers that attach longer warranties to expensive items.
The result is proved in the paper; none of it is machine-checked. A formal proof gives a verified two-service extension of the MNL revenue-ordered assortment theorem, and the fixed-point reduction (milestones 1 and 2) is a reusable device for MNL assortment problems with several options per product.
Difficulty
The profit is a ratio of sums, so exchanging one product's service changes every choice probability, and pairwise exchange arguments do not directly compare assortments. The naive idea of ranking products by a single margin fails: the long-service margin yi and the short-service margin zi order products differently, and the long service also raises the product's attraction. Neither ordering alone decides which products get long service. The adjusted markup xi is the breakpoint at which long and short service become equally profitable, and the three breakpoints xi≤yi≤zi must line up for the threshold structure to hold. This ordering uses ai−biqi≥0: with a negative service cost the long service can be optimal for a product whose adjusted markup is below that of a product left unserved, and part (b) fails.
Formalization scope
Products are Fin N (0-based); N=0 is allowed. All parameters α,a,b,c,s,p,q are arbitrary real vectors and ts,tl real numbers; prices and qualities are fixed data, not decisions.
The outside option is the constant 1 in the denominator. The MNL formula is the definition; its derivation from Gumbel utilities is cited, not formalized.
Decisions are pairs of Finset (Fin N) with Disjoint Sl Ss; optimality is a global inequality against every disjoint pair.
"Markup-ordered" and "adjusted markup-ordered" are upper level sets {i:zi≥θ}, {i:xi≥θ′} with real thresholds. Each is a prefix of every decreasing relabelling, so no tie-break is fixed; the empty and the full set are allowed.
The model's standing assumptions are explicit hypotheses wherever they are used: ts<tl (shortest and longest duration), si>0 (service utility) and ai−biqi≥0 (service cost). The first two make Ai well defined; Ai is a total Lean function that returns 0 when its denominator vanishes, a value no statement relies on. No sign is imposed on bi or ci.
Trivializing formalizations are ruled out: the statement has two service levels (a single level would be the Talluri–van Ryzin theorem), uses level sets rather than a fixed relabelling with strict orders, ties the long-service set to the same offered set in (a) and (b) instead of using independent existentials, and states the three hypotheses rather than leaving them implicit.
Definitions: the MNL choice probabilities and profit (12)–(13), and the auxiliary functions hil,his,hi,H, Ai, xi. Proofs of the milestones need only finite sums, max and elementary real analysis. Proofs of any milestone, and alternative routes to Theorem 5, are welcome.
Selected references
Ruxian Wang, Chenxu Ke, Shiliang Cui, Product Price, Quality and Service Decisions under Consumer Choice Models, Manufacturing & Service Operations Management, 2022 (accepted manuscript, SSRN 3766191). https://ssrn.com/abstract=3766191 — DOI of the published version: https://doi.org/10.1287/msom.2020.0947
Kalyan Talluri, Garrett van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
Daniel McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in Frontiers in Econometrics, Academic Press, 1974.
Product Price, Quality and Service Decisions under Consumer Choice Models IV: Under the Two-Stage Nested Logit Model, Qualities Are Set Product by Product and Markups Are Nest-InvariantResearch Paper
Motivation
A firm that sells durable products with an attached service (a warranty, a maintenance plan, a support contract) chooses three things for each product: its price, its quality, and how long the service lasts. Wang, Ke and Cui (SSRN 3766191, Manufacturing & Service Operations Management, 2022) study this joint decision when consumers choose among the products according to a discrete choice model. Under the multinomial logit (MNL) model they show that every product's optimal service duration is either the shortest or the longest available, so that the products split into a short-service group and a long-service group.
That conclusion suggests a different model of the consumer. In business procurement, and more generally when the buyer first decides how long a product will be used, the consumer plausibly chooses a service duration first and a product second. The two-stage nested logit (NL) model (Ben-Akiva 1973; McFadden 1980) captures exactly this: the two service groups become nests, and products within a nest are closer substitutes than products in different nests. Section 4 of the paper asks whether the MNL structure of optimal qualities and prices survives in this model. This mission formalizes its answer, Theorem 4.
Price optimization under the nested logit model has a substantial literature. For prices alone, the optimal prices within a nest share one markup and the problem reduces to a one-dimensional fixed point (Li & Huh 2011; Gallego & Wang 2014). Theorem 4 adds quality as a decision, with production cost quadratic in quality and service cost depending on quality.
Setting
There are two nests x∈{s,l}. Nest x contains mx products i=1,…,mx, and every product of nest x is sold with the same fixed service duration tx. Product i of nest x has parameters αxi (quality sensitivity), axi (base service cost per unit time), bxi (marginal effect of quality on service cost), cxi>0 (production-cost coefficient) and sxi (service utility per unit time). The firm chooses a price pxi and a quality qxi for every product.
The total attractiveness of nest x is ex=∑i=1mxexp(αxiqxi−pxi+txsxi). With upper-level scale parameter μ1≥1 (the nest coefficient is 1/μ1; the lower-level scale is normalized to 1), a consumer chooses nest x with probability
dx(p,q)=1+es1/μ1+el1/μ1ex1/μ1,
buys nothing with the remaining probability, and, having chosen nest x, picks product i with probability di∣x=exp(αxiqxi−pxi+txsxi)/ex. The probability of buying product i of nest x is dxi=dxdi∣x. The markup of a product is its price minus production cost cxiqxi2 minus service cost tx(axi−bxiqxi), and the firm's expected profit (market size one) is
has a unique real solution r†. With pxi†=μ1+r†+cxiqxi†2+tx(axi−bxiqxi†),
ΠM(p,q)≤ΠM(p†,q†)=r†for all (p,q),
and (p†,q†) is the only maximizer.
Milestones
The milestones follow the paper's proof in the Online Supplement:
(EC.5): at an optimal price vector, every product i of nest x has markup 1+r/μ1+(1−1/μ1)rx, where r is the profit and rx the nest's average markup; so markups are constant within a nest.
(EC.6): with a common markup ρx per nest, the profit is ∑xρxdx(ρ,q); at the optimal markups, ρx−μ1=r for each nonempty nest.
(EC.7): for every r, the right-hand side above, as a function of q, is maximized exactly at q†.
(EC.8): that right-hand side is strictly decreasing in r, so the fixed-point equation has exactly one root.
Significance
The result. Theorem 4 has two consequences. First, each product's optimal quality depends only on its own parameters and its nest's service duration, not on any other product, although all products are substitutes. At this quality, the marginal production and service cost of quality equals the consumer's marginal utility from it. Second, every product in both nests carries the same markup, μ1+r†: the optimal profit plus the reciprocal of the nest coefficient. A pricing problem with ms+ml prices reduces to finding the root of a single monotone function. Proposition 7 of the paper uses these closed forms to compare consumer surplus with and without quality control under the NL model.
Formalizing it. The paper's proof writes down first-order conditions and assumes an optimum exists. The goal here is global optimality and uniqueness over all real prices and qualities, which the paper does not prove. A complete formalization needs the existence of the maximizer or a direct upper bound, together with the first-order identities. The related platform item DLevelNestedLogit.Pricing.stationary_point_iff (Li et al. 2015) characterizes stationary points of the price-only revenue in a d-level nested logit model. It has no costs and no quality, and it is not used here. No result of this mission has a machine-checked proof yet.
Difficulty
The profit ΠM is not concave in prices (under the nested logit model, concavity is known only after a change of variables to market shares, Li & Huh 2011), so a first-order condition does not by itself certify a global maximum. The paper's argument shows only that any optimum satisfies the stated formulas. For a global result, the critical points must be shown to coincide with the maximizers, and the profit must be bounded above by r† everywhere, including at decisions where markups differ across products of a nest or are negative. The two reductions, to nest markups and then to the scalar r, are only valid at the optimum and have to be carried out with that in mind. The exponent 1/μ1≤1 makes ex1/μ1 concave rather than linear in the nest attractiveness. This is the step where the MNL argument does not transfer verbatim.
Formalization scope
Nests are a two-element type Nest (s, l). Products of nest x are Fin (m x), 0-based. Nests may be empty: an empty nest has ex=0, 01/μ1=0, and contributes nothing.
The outside option is the "1+" in the denominator of dx, not a nest.
Durations ts,tl are fixed data, not decisions, with no order assumed between them. The nests are fixed.
Prices and qualities range over all of R. The model's normalization q≥0 is not imposed, as in the paper's own formula.
Standing hypotheses: μ1≥1 (general; μ1=1 is allowed but is not the only case) and cxi>0. No sign is imposed on α,a,b,s.
Powers are Real.rpow of nonnegative sums of exponentials.
"Optimal" means a global maximizer over all real vectors. The milestones that the paper derives from first-order conditions are stated as properties of a global maximizer.
The price formula p† takes r as an argument, and the theorem must identify r=r†.
The following versions are trivializing and are excluded: μ1=1 only (the MNL case), a single nest, first-order conditions in place of global optimality, fixed qualities, or an optimum defined by the paper's formula.
The definitions (Model, MarkupProblem, Optimum) are self-contained and can be reused for other nested logit pricing results. Contributions are welcome on each milestone, on a sorry-free derivative of ΠM in pxi, and on an existence result for the maximizer.
M. Ben-Akiva, Structure of Passenger Travel Demand Models, PhD thesis, Massachusetts Institute of Technology, 1973 (no stable link; cited as in the source's bibliography).
D. McFadden, Econometric Models for Probabilistic Choice Among Products, Journal of Business 53(3), S13–S29, 1980. https://doi.org/10.1086/296093
H. Li, W. T. Huh, Pricing Multiple Products with the Multinomial Logit and Nested Logit Models: Concavity and Implications, Manufacturing & Service Operations Management 13(4), 549–564, 2011. https://doi.org/10.1287/msom.1110.0344
G. Gallego, R. Wang, Price Optimization and Competition for Multi-Products under the Nested Logit Model with Product-Differentiated Price Coefficients, Operations Research 62(2), 450–461, 2014 (cited as in the source's bibliography; link not verified in this session).
On the tightness of SDP relaxations of QCQPs 1: Polyhedral Γ and Large Shared Zero Eigenspaces on Semidefinite Faces Give conv(D) = D_SDP and Opt = Opt_SDPResearch Paper
Motivation
Quadratically constrained quadratic programs (QCQPs) minimize a quadratic function subject to quadratic inequality and equality constraints. They model facility location, pooling, max-cut, trust-region steps and robust optimization problems, and every {0,1} integer program can be written as one; in general they are NP-hard. The standard tractable approach is the Shor semidefinite relaxation, which lifts x to the matrix xx⊤ and relaxes the rank-one condition to positive semidefiniteness. A recurring question is when this relaxation loses nothing: when its optimal value equals that of the QCQP (SDP tightness), and, more strongly, when its projected epigraph equals the convex hull of the QCQP's epigraph (convex hull exactness). The second property also describes the convex hull of the nonconvex feasible set's epigraph, which is useful in branch-and-bound and cutting-plane methods.
Timeline. The S-lemma (Yakubovich, 1971) gives SDP tightness for one inequality constraint, and Fujie and Kojima (1997) recorded the dual description of the SDP value used below. For the trust-region subproblem and its generalization, convex hull descriptions of the epigraph were given by Ho-Nguyen and Kılınç-Karzan (2017) and by Wang and Kılınç-Karzan (arXiv:1907.08843, 2019). Beck (2007) and Beck, Drori and Teboulle (2012) gave SDP tightness results for quadratic matrix programs. Wang and Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs (arXiv:1911.09195v3, Math. Program. 2021), introduced a general framework based on the faces of a dual set Γ and proved convex hull and tightness results for polyhedral Γ and for QCQPs with large quadratic eigenvalue multiplicity. This mission formalizes the paper's first convex hull theorem (Theorem 1, p. 13) and the framework it rests on.
Setting
Fix N variables and m≥1 constraints, the first mI inequalities and the remaining mE=m−mI equalities. Each function is
The QCQP (1) is Opt=inf{q0(x):qi(x)≤0(i≤mI),qi(x)=0(i>mI)}, and its epigraph is D={(x,t):x feasible,q0(x)≤2t}.
With Qi=(cibibi⊤Ai) and Y=(1xx⊤X), the SDP relaxation (3) minimizes ⟨Q0,Y⟩ over X∈SN with Y⪰0 and the constraints ⟨Qi,Y⟩≤0 or =0; its value is OptSDP and its projected epigraph is DSDP={(x,t):∃X,(x,X) feasible,⟨Q0,Y⟩≤2t} (4). Always conv(D)⊆DSDP and Opt≥OptSDP.
For γ∈Rm let A(γ)=A0+∑iγiAi, and similarly b(γ), c(γ) and the Lagrangian q(γ,x)=q0(x)+∑iγiqi(x). The dual object is
Γ={γ∈Rm:A(γ)⪰0,γi≥0for i≤mI}.
Assumption 1: the QCQP is feasible and some γ∗ with γi∗≥0 for i≤mI has A(γ∗)≻0. Assumption 3: Γ is polyhedral. For x^∈RN, F(x^)=argmaxγ∈Γq(γ,x^). A faceF of Γ is definite if some γ∈F has A(γ)≻0 and semidefinite otherwise, with shared zero eigenspaceV(F)={v:A(γ)v=0∀γ∈F}. Finally affdim denotes affine dimension.
Formalization targets
Goal: Theorem 1 (p. 13)
Under Assumptions 1 and 3, if every semidefinite face F of Γ satisfies dimV(F)≥affdim{b(γ):γ∈F}+1, then
conv(D)=DSDPandOpt=OptSDP.
Milestones
Lemma 1 (p. 7): under Assumption 1, DSDP={(x,t):supγ∈Γq(γ,x)≤2t} and OptSDP=minxsupγ∈Γq(γ,x).
Lemma 2 (p. 9): a semidefinite face has a unit vector in V(F).
Lemma 3 (p. 9): under Assumptions 1 and 2, a point of DSDP with definite F(x^) lies in D.
Observation 1 (p. 10): under Assumption 1, a face of affine dimension m is definite.
Lemma 4 (p. 10): under Assumptions 1, 2 and the decomposition condition (7), the two conclusions of Theorem 1 hold.
Lemma 8 (p. 13): under Assumption 3, Γ=Γe+cone(Γr) with polytopes Γe,Γr, and F(x^)=Fe(x^)+cone(Fr(x^)) when the supremum is finite.
Lemma 7 (p. 13): under the hypotheses of Theorem 1, condition (7) holds.
Companions
Lemma 6 (p. 11: dimV(F)≥k for the quadratic eigenvalue multiplicity k), Theorem 2 (p. 15: the hypothesis of Theorem 1 with k in place of dimV(F)), and Corollaries 1–4 (pp. 16–18: convex quadratic programs, one constraint, bi=0, scalar quadratic forms with m≤N).
Significance
The result. Theorem 1 gives a checkable sufficient condition, stated on the faces of a polyhedral dual set, under which the Shor relaxation is exact in the strongest sense: it describes conv(D), so the SDP value equals the QCQP value and, by Remark 7, conv(D) is second-order cone representable. Through Lemma 6 it becomes Theorem 2, the symmetry condition k≥affdim{b(γ)}+1; its corollaries recover the convex hull results for the trust-region subproblem and its generalization and give new ones for simultaneously diagonalizable and "Swiss cheese" problems. The sharpness of the bound is shown in §4.3 of the paper.
Formalizing it. The theorem is proved in the paper; nothing in it is machine-checked. A formal proof needs strong conic duality for the SDP in Lemma 1, the Minkowski–Weyl decomposition in Lemma 8, and the face-by-face decomposition argument of Lemma 7. These pieces are shared with the paper's SDP tightness result (Theorem 3), which uses Lemmas 1–3 and 8 again.
Difficulty
The obvious attempt is to take (x^,t^)∈DSDP, recover a rank-one solution of the SDP, and read off a point of D. This fails because an optimal Y need not have rank one, and a rank-reduction step can leave the feasible set of a nonconvex constraint. The paper instead moves (x^,t^) along a direction v in the shared zero eigenspace of the face F(x^), and must show that both endpoints of the move stay in DSDP while the face strictly grows in affine dimension. Controlling the endpoints needs finiteness of the relevant family of quadratic functions, which is where polyhedrality enters; without it (§4.3) the argument and the theorem fail. Lemma 1 also needs a strong duality theorem for semidefinite programs with a minimax step, neither of which is elementary in Lean.
Formalization scope
The Lean development lives in the namespace QCQPTightness.ConvHull. A QCQP is a structure with symmetric A0,Ai, vectors b0,bi, scalars c0,ci and a count mI≤m; constraints are indexed by Fin m, constraint i being an inequality exactly when i<mI. Conventions:
Opt and OptSDP are infima in EReal, never real infima; points of RN+1 are pairs (x,t), and conv is convexHull ℝ.
Faces of Γ are nonempty convex extreme subsets; the page's convention affdim∅=−1 makes the empty face irrelevant, while Lean's affine dimension of ∅ would be 0.
"supγ∈Γq(γ,x)≤2t" is written ∀γ∈Γ,q(γ,x)≤2t; "a convex combination of points with property P" is membership in the convex hull of the set of such points; the unit sphere is v⊤v=1.
The goal carries exactly the paper's hypotheses plus its standing assumption m≥1 (p. 1); Assumption 2 is not assumed because Assumption 3 implies it.
Lemma 8 is printed with "Fr(x^) is the face of Γe"; it is formalized with Γr, as the proof and Lemma 7 use it.
A trivializing formalization would assume condition (7), the decomposition of Lemma 8, or any property of F(x^) in the goal; the goal assumes none of these, and the dimension hypothesis is satisfiable with semidefinite faces present (for q0=−x2, q1=x2−1, the face {γ1=1} is semidefinite with dimV=1).
Infrastructure needed: SDP strong duality (the platform has ConvexOptimization.sdp_strong_duality), the Minkowski–Weyl theorem for polyhedra, faces of convex sets and affine dimension. Proofs of any milestone, of the companions, and reusable lemmas about faces of spectrahedra are welcome.
T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, J. Global Optim. 10 (1997) 367–380. https://doi.org/10.1023/A:1008282830093
N. Ho-Nguyen, F. Kılınç-Karzan, A second-order cone based approach for solving the trust-region subproblem and its variants, SIAM J. Optim. 27 (2017) 1485–1512. https://doi.org/10.1137/16M1065197
A. L. Wang, F. Kılınç-Karzan, The generalized trust region subproblem: solution complexity and convex hull results, arXiv:1907.08843 (2019). https://arxiv.org/abs/1907.08843
Douglas-Rachford Splitting and ADMM for Nonconvex Optimization: Tight Convergence Results IV: The Image Function (Bg) Is Lsc on B dom g Exactly When Condition (5.5) HoldsResearch Paper
Why the image function matters for ADMM
The alternating direction method of multipliers (ADMM) solves problems of the form minx,zf(x)+g(z) subject to Ax+Bz=b. Themelis and Patrinos (arXiv:1709.05747v4, SIAM J. Optim. 30(1):149–181, 2020) show that, for nonconvex f and g, ADMM is the Douglas–Rachford splitting method applied to a reformulated problem whose second term is the image functionφ2=(Bg), (Bg)(s)=inf{g(z)∣Bz=s}. Their convergence theory for DRS requires the nonsmooth term to be proper and lower semicontinuous (Assumption IIa4), so whether (Bg) inherits lower semicontinuity from g decides whether the theory applies to a given ADMM instance.
Image functions, also called epi-compositions or infimal post-compositions, are classical objects of variational analysis (Rockafellar and Wets, Variational Analysis; Bauschke and Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces; Auslender and Teboulle, Asymptotic Cones and Functions). For convex g the question of when (Bg) is closed has a long history through recession functions; Section 5.4.1 of the paper gives a characterization that needs no convexity.
Setting
Let R=R∪{+∞}. For g:Rn→R the domain is domg={z∣g(z)<∞}; g is lower semicontinuous (lsc) if its epigraph is closed, and level bounded if every set {z∣g(z)≤α}, α∈R, is bounded.
Fix a matrix B∈Rp×n. The image function of g under B (Definition 5.1) is
(Bg)(s)=z∈Rninf{g(z)∣Bz=s},s∈Rp,
with values in [−∞,+∞]. Its domain is Bdomg: outside that set the infimum is over values +∞ only.
Condition (5.5) at a point zˉ∈domg compares the best value of g on the affine fibre zˉ+kerB with the values of g far away along directions that B nearly annihilates:
∥d∥→∞Bd→0liminfg(zˉ+d)≥d∈kerBinfg(zˉ+d).
The right side equals (Bg)(Bzˉ).
Formalization targets
Goal: Theorem 5.11, on Bdomg
For every lsc g:Rn→R and every B∈Rp×n,
(Bg)is lsc at every sˉ∈Bdomg⟺(5.5)holds at every zˉ∈domg.
Milestones
The right side of (5.5) is (Bg)(Bzˉ).
The "if" direction: (5.5) on domg gives lower semicontinuity of (Bg) at every point of Bdomg.
The "only if" direction: lower semicontinuity of (Bg) on Bdomg forces (5.5) on domg.
Companion results
The "In particular" clause of Theorem 5.11, as printed: if g is lsc and level bounded, then (Bg) is lsc on all of Rp.
The properness clause of Proposition 5.10: if g is proper and lsc and, for some β>0, minz{g(z)+2β∥Bz−s∥2} is attained for every s, then (Bg) is proper.
Significance
Theorem 5.11 turns Assumption IIa4, a property of a derived function, into a checkable condition on g and B. Its level-bounded corollary covers every lsc g with bounded sublevel sets, and the characterization explains why the pathological example (5.4) of the paper, in which g is even C1, fails: a minimizing sequence on the fibre escapes to infinity while B applied to it converges. Combined with the convergence theorem for ADMM in the same paper (Theorem 5.6), this identifies the ADMM instances to which the tight DRS stepsize theory applies.
The theorem is proved in the paper. As far as is known, no machine-checked proof of it, or of any closedness criterion for image functions, exists in Lean or in Mathlib. A formalization fixes the exact range of the equivalence, which the printed statement gets wrong (see Formalization scope), and supplies reusable infrastructure: the image function in EReal, and liminfs along the filter "∥d∥→∞, Bd→0".
Difficulty
Lower semicontinuity of (Bg) at sˉ asks that values of g on fibres {Bz=s}, s→sˉ, not drop below (Bg)(sˉ). The natural argument picks near-minimizers zk on these fibres and passes to a limit; this works only when the zk stay bounded, and nothing in lsc of g alone prevents them from escaping to infinity. The difficulty is to account exactly for the unbounded case, which must be compared with the fibre through sˉ by a translation zk−zˉ, and that requires a point zˉ∈domg with Bzˉ=sˉ. The converse requires turning a failure of (5.5), stated as a filter liminf, into a sequence witnessing the failure of lower semicontinuity.
Formalization scope
Rn and Rp are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin p); B is a continuous linear map between them. Every dimension, including 0, is allowed.
R is EReal, and g is assumed never to take the value −∞. The image function is the EReal infimum infz,Bz=sg(z), which may be −∞ and is +∞ off Bdomg. Properness of g is not assumed in the goal: if domg=∅ both sides hold.
Lower semicontinuity at a point is Mathlib's LowerSemicontinuousAt, the neighbourhood form of the page's sequential level-set criterion.
The liminf in (5.5) is taken in the complete lattice [−∞,+∞] along the meet of the cobounded filter (∥d∥→∞) and the preimage under B of the neighbourhood filter of 0. When no such d exist (e.g. B injective) the filter is trivial, the liminf is +∞, and (5.5) holds, as an empty liminf does on the page.
Correction. As printed, Theorem 5.11 asserts lsc of (Bg) everywhere, and its "if" direction is then false. Take n=2, p=1, B=[10], and g the indicator of the closed set {(x,y):x>0,xy≥1}. Condition (5.5) holds at every zˉ∈domg, since its right side is 0 and g≥0; but (Bg)(s)=0 for s>0 and +∞ for s≤0, so (Bg) is not lsc at 0. The proof begins "given sˉ∈dom(Bg)" and covers exactly Bdomg; both directions establish the corrected equivalence, which is the goal. The "In particular" clause is true as printed and is stated with lsc everywhere. The lsc clause of Proposition 5.10 fails for the same reason and is not formalized.
Assumption IIa2 enters Proposition 5.10 only through the solvability of minz{g(z)+2β∥Bz−s∥2} for every s.
A trivializing formalization is ruled out: the goal assumes only lsc of g and linearity of B, as on the page, and is not restricted to proper or level-bounded g (that is the separate companion).
Contributions welcome: proofs of the milestones, a general Mathlib-style lemma that the infimum of an lsc function over the fibres of a linear map is lsc on its domain under (5.5), and the closedness of image functions under level-boundedness.
A. Auslender, M. Teboulle, Asymptotic Cones and Functions in Optimization and Variational Inequalities, Springer, 2003 (cited as 2002 in the paper). https://doi.org/10.1007/b97594
Understanding the Acceleration Phenomenon via High-Resolution Differential Equations V: Along the High-Resolution ODE of NAG-C, inf ‖∇f(X(u))‖² ≤ (12 + 9sL)‖x₀ − x⋆‖²/(2√s(t³ − t₀³))Research Paper
Motivation
Nesterov's accelerated gradient method for smooth convex functions, called NAG-C in the source paper, minimizes an L-smooth convex function f with function values decreasing at the rate O(L/k2). That rate is optimal among first-order methods (Nesterov, 1983). A line of work starting with Su, Boyd & Candès (2016) studies such methods through ordinary differential equations obtained in the limit of vanishing step size. Their low-resolution ODEX¨+t3X˙+∇f(X)=0 reproduces the O(1/t2) function-value rate. The same ODE also models the heavy-ball method, so it cannot explain why Nesterov's method behaves differently from heavy-ball.
Shi, Du, Jordan & Su (arXiv:1810.08907v3) keep the O(s) terms of the limit, where s is the step size. The resulting high-resolution ODEs contain a gradient-correction term s∇2f(X)X˙, which is absent from the heavy-ball ODE. This mission formalizes the paper's analysis of the high-resolution ODE of NAG-C (Section 4.1, pp. 21–24). Along this ODE the smallest squared gradient norm up to time t decays like 1/t3, while the low-resolution ODE gives only 1/t2. Small gradients are the natural stopping criterion in practice and the natural target in nonconvex and dual problems, which is why the squared gradient norm is studied separately from function values (Nesterov, 2012).
Setting
Let f:Rn→R have gradient ∇f and Hessian ∇2f. For L>0, the class FL1(Rn) consists of the differentiable f with
With s=0 it reduces to the Lyapunov function of Su, Boyd and Candès.
Formalization targets
Goal: Theorem 5 (p. 21)
For every f∈FL2(Rn), every step size s>0, and every solution X of (1.12),
t0≤u≤tinf∥∇f(X(u))∥2≤2s(t3−t03)(12+9sL)∥x0−x⋆∥2for all t>t0.
With s=1/L this is O(L/t3). The infimum cannot be dropped, because the gradient norm need not decrease along the trajectory.
Milestones (pp. 22–23)
The exact derivative of E along (1.12) (first display of the proof of Lemma 4.1, p. 23).
Lemma 4.1, (4.2): dtdE≤−[st2+(L1+2s)t+2Ls]∥∇f(X)∥2 for t≥t0.
The integrated form: ∫t0t[su2+(L1+2s)u+2Ls]∥∇f(X(u))∥2du≤E(t0)−E(t)≤E(t0).
(4.3): the infimum is at most E(t0) divided by s(t3−t03)/3+(L1+2s)(t2−t02)/2+2Ls(t−t0).
E(t0)≤3s⋅2L∥x0−x⋆∥2+2∥x0−x⋆∥2, from the initial conditions.
(4.4): the same bound as (4.3) with numerator (2+1.5sL)∥x0−x⋆∥2. Keeping only the cubic term of the denominator gives Theorem 5.
A companion item states Corollary 4.2 (p. 24): f(X(t))−f(x⋆)≤t(2t+s)(4+3sL)∥x0−x⋆∥2 for t>t0.
Significance
Theorem 5 is the continuous-time model of the paper's Theorem 6, which shows that NAG-C itself, without modification, drives mini≤k∥∇f(xi)∥2 to zero at the rate O(L2/k3). Combining the O(1/t2) function-value rate with ∥∇f∥2≤2L(f−f⋆) gives only O(L/t2). Previously known O(L2/k3) rates required modified methods (Ghadimi & Lan, 2016). The proof attributes the improvement to the gradient-correction term: the factor ∥∇f(X)∥2 in Lemma 4.1 comes from the term ts∇f(X) in (4.1), which exists only because of the Hessian term in (1.12). The authors conjecture that the low-resolution ODE does not achieve the 1/t3 rate (p. 23).
The results of Section 4.1 are proved in the paper; no machine-checked version of them is known. Formalizing them produces a checked Lyapunov analysis of a second-order ODE with Hessian damping and explicit constants. It also gives a template that the discrete analysis of NAG-C (a separate mission in this series) mirrors step by step. Related Hessian-damped systems are analysed in Attouch, Chbani, Fadili & Riahi (2020), with qualitative integrability conclusions instead of an explicit bound on the infimum.
Difficulty
The obvious route goes through the function-value rate and the inequality ∥∇f∥2≤2L(f−f⋆). It loses a factor of t and yields only 1/t2. The cubic rate needs a Lyapunov function whose derivative contains a term proportional to t2∥∇f(X)∥2. Proving the derivative identity requires differentiating t↦∇f(X(t)) through the chain rule with the Hessian, and then cancelling that derivative against the gradient-correction term of the ODE. The derivative bound also uses the co-coercivity inequality f(x⋆)≥f(X)+⟨∇f(X),x⋆−X⟩+2L1∥∇f(X)∥2 of L-smooth convex functions. The remaining steps are measure-theoretic: integrate a one-sided derivative bound on [t0,t], and compare an infimum with a weighted average.
Formalization scope
Rn is EuclideanSpace ℝ (Fin n), ∇f is Mathlib's gradient, and ∇2f(x)v is the Fréchet derivative of the gradient map applied to v.
The classes FL1 and FL2 are stated in the first-order form printed on p. 8. The Hessian's Lipschitz constant is existential, since the paper fixes none.
The minimizer x⋆ is a hypothesis f(x⋆)≤f(z) for all z. The paper presupposes it exists.
The step size is any s>0; there is no condition s≤1/L.
A solution of (1.12) is a pair (X,V) with X(t0)=x0 and V(t0)=−s∇f(x0). For every t≥t0, X has derivative V(t) and V has the derivative prescribed by (1.12), both relative to [t0,∞).
Every statement quantifies over all solutions. Existence and uniqueness (the paper's Proposition 2.2) are not assumed.
The infimum inft0≤u≤t ranges over the points of the interval [t0,t]. Statements involving it hold for t>t0, as on the page.
Derivative bounds assert that the derivative exists.
The integral bound asserts integrability of its integrand.
Ruled out. A formalization would hold for junk reasons in any of these cases: the infimum is written as a bounded infimum over all reals (in Lean this is ≤0); the velocity is not tied to X˙; the goal is stated at t=t0 (where Lean divides by 0); or derivatives are written with deriv, which is 0 where a function is not differentiable. The statements here avoid all of these.
Infrastructure. A complete development needs:
the chain rule for ∇f∘X along a path;
the co-coercivity inequality for L-smooth convex functions;
the fundamental theorem of calculus for one-sided derivatives on [t0,t];
the mean-value comparison of an infimum with a weighted average.
The co-coercivity inequality and the interval-integral comparison are reusable beyond this mission. Proofs of the milestones in any order are welcome, as are independent proofs of the goal.
Selected references
B. Shi, S. S. Du, M. I. Jordan, W. J. Su, Understanding the Acceleration Phenomenon via High-Resolution Differential Equations, arXiv:1810.08907v3, 2018; Math. Program. (2021), DOI 10.1007/s10107-021-01681-8. https://arxiv.org/abs/1810.08907
W. Su, S. Boyd, E. J. Candès, A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights, J. Mach. Learn. Res. 17(153), 2016. https://arxiv.org/abs/1503.01243
Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Math. Dokl. 27, 1983. https://www.mathnet.ru/eng/dan46009
S. Ghadimi, G. Lan, Accelerated gradient methods for nonconvex nonlinear and stochastic programming, Math. Program. 156, 2016. https://arxiv.org/abs/1310.3787
H. Attouch, Z. Chbani, J. Fadili, H. Riahi, First-order optimization algorithms via inertial systems with Hessian driven damping, Math. Program., 2020. https://arxiv.org/abs/1907.10536
Understanding the Acceleration Phenomenon via High-Resolution Differential Equations IV: The High-Resolution Heavy-Ball ODE Satisfies f(X(t)) − f(x⋆) ≤ 7‖x₀ − x⋆‖² e^(−√μ t/4)/(2s)Research Paper
Why a high-resolution ODE for the heavy-ball method
Polyak's heavy-ball method and Nesterov's accelerated gradient method for strongly convex functions (NAG-SC) are the two classical momentum methods of smooth convex optimization. With step size s and momentum α=(1−μs)/(1+μs) they differ only by a gradient-correction term, yet NAG-SC is accelerated for every μ-strongly convex, L-smooth objective while the heavy-ball method can fail to converge outside the quadratic case (Lessard, Recht & Packard 2016). The classical continuous-time limit cannot see this difference: as s→0 both methods converge to the same low-resolution ODEX¨+2μX˙+∇f(X)=0 (Su, Boyd & Candès 2016 treat the convex analogue).
Shi, Du, Jordan & Su (2018/2021) keep the O(s) terms of the limit and obtain high-resolution ODEs, one per method, which do distinguish the two algorithms. This mission formalizes their convergence theorem for the high-resolution ODE of the heavy-ball method (Theorem 2 of arXiv:1810.08907v3). A companion mission in the same series treats the high-resolution ODE of NAG-SC (Theorem 1), whose only difference is a Hessian-driven damping term s∇2f(X)X˙.
Setting
Work in Rn with the standard inner product ⟨⋅,⋅⟩ and Euclidean norm ∥⋅∥. A function f:Rn→R belongs to FL1(Rn) if L>0, f is differentiable and convex in the form f(y)≥f(x)+⟨∇f(x),y−x⟩, and ∥∇f(x)−∇f(y)∥≤L∥x−y∥ for all x,y. It belongs to Sμ,L1(Rn) if moreover 0<μ≤L and
f(y)≥f(x)+⟨∇f(x),y−x⟩+2μ∥y−x∥2for all x,y,
and to Sμ,L2(Rn) if in addition f is twice continuously differentiable with a Lipschitz-continuous Hessian. Write x⋆ for the minimizer of f.
Given a step size s>0 and an initial point x0, the high-resolution ODE of the heavy-ball method is
The coefficient inequality, p. 14: for 0<μs≤1, the bracket above is <7/2.
Significance
The result. Theorem 2 gives a linear rate e−μt/4 for the heavy-ball ODE with an explicit constant, valid for every Sμ,L2 objective and every step size up to 1/L. Read next to Theorem 1 (rate e−μt/4, constant 2/s for the NAG-SC ODE), it shows that at the continuous level both high-resolution ODEs converge at the accelerated rate; the paper locates the difference between the two discrete methods in the discretization, where only the gradient correction of NAG-SC lets the Lyapunov argument survive (its Theorems 3 and 4 and §3.3). The Lyapunov function (3.3) is the NAG-SC function (2.4) with the s∇f(X) term removed, and the two coincide at s=0.
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked proof exists. The mission produces a checked chain from the ODE to the rate: a one-sided derivative computation along a trajectory in Rn, a differential inequality, a Grönwall-type integration, and a closed-form estimate of E(0) from the initial conditions and L-smoothness. The derivative computation and the Grönwall step reuse directly in the companion missions on the NAG-SC and NAG-C high-resolution ODEs.
Difficulty
The algebra is short; the formal difficulty is analytic. The derivative of t↦f(X(t)) must be obtained by the chain rule from a one-sided derivative of X at t=0 and f's differentiability, and the derivative of the two squared norms from those of X and V=X˙. Passing from Lemma 3.2 to E(t)≤e−μt/4E(0) is a comparison argument for a function known only to have one-sided derivatives on [0,∞); the naive route through dtd(eμt/4E)≤0 requires a monotonicity theorem for functions with derivatives within a half-line. Finally, the estimate of E(0) needs f(x0)−f(x⋆)≤2L∥x0−x⋆∥2 and ∥∇f(x0)∥≤L∥x0−x⋆∥, both consequences of L-smoothness and ∇f(x⋆)=0 that must be derived from the class definition, and the constant 7/2 needs a one-variable inequality in μs∈(0,1].
Formalization scope
Rn is EuclideanSpace ℝ (Fin n), ∇f is Mathlib's gradient, and ∇2f(x) is fderiv ℝ (gradient f) x. The classes FL1, Sμ,L1, Sμ,L2 are structures carrying the paper's first-order inequalities (§1.4, p. 8), with 0<μ≤L; the Lipschitz constant of the Hessian is existential, as the paper fixes none. The minimizer is a point x⋆ with f(x⋆)≤f(z) for all z.
A solution of (1.10) is a pair of curves X,V:R→Rn with X(0)=x0, V(0)=−2s∇f(x0)/(1+μs), V(t) the derivative of X and −2μV(t)−(1+μs)∇f(X(t)) the derivative of V at every t≥0, both taken within [0,∞); values for t<0 play no role. The theorems quantify over every such solution. Existence and uniqueness (the paper's Propositions 2.1–2.2) are not assumed, and no a priori bound on X or V is added. Derivative claims assert that the derivative exists and has the stated value or bound, so a statement cannot hold merely because a derivative is undefined. The goal states the decay of f(X(t))−f(x⋆) with the printed constant 7/(2s); it does not assume any decay of E, and an ODE predicate in which V is not the derivative of X would be a different, trivial statement.
All drafts live in the namespace HighResODE.HeavyBallODE, with one definitions file (classes, ODE, Lyapunov function). Contributions are welcome at every milestone; a general lemma "φ′≤−cφ within [0,∞) implies φ(t)≤e−ctφ(0)" and the L-smoothness estimates around a minimizer are reusable well beyond this mission.
Selected references
B. Shi, S. S. Du, M. I. Jordan, W. J. Su, Understanding the Acceleration Phenomenon via High-Resolution Differential Equations, Mathematical Programming (2021); cited here in its preprint version arXiv:1810.08907v3. https://arxiv.org/abs/1810.08907
W. Su, S. Boyd, E. J. Candès, A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights, Journal of Machine Learning Research 17 (2016). https://arxiv.org/abs/1503.01243
L. Lessard, B. Recht, A. Packard, Analysis and Design of Optimization Algorithms via Integral Quadratic Constraints, SIAM Journal on Optimization 26 (2016). https://arxiv.org/abs/1408.3595
B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Computational Mathematics and Mathematical Physics 4 (1964). https://doi.org/10.1016/0041-5553(64)90137-5
From Differential Equation Solvers to Accelerated First-Order Methods for Convex Optimization 6: Nesterov's Method Has ℒ_k ≤ ℒ₀·min{4L/(√γ₀k + 2√L)², (1 − √(min{γ₁, μ}/L))^k}Research Paper
Motivation
Nesterov's accelerated gradient method minimises a smooth convex function f to accuracy ε in O(L/ε) gradient evaluations, and a μ-strongly convex one in O(L/μlog(1/ε)); both counts match the lower bounds for first-order methods. Nesterov's own analysis (Y. Nesterov, Introductory Lectures on Convex Optimization, 2004, Ch. 2) proceeds by estimate sequences, an algebraic device that certifies the rate but says little about where the method comes from. Since Su, Boyd and Candès (arXiv:1503.01243), accelerated methods have been read as discretisations of ordinary differential equations, with convergence proved by discrete Lyapunov functions.
H. Luo and L. Chen, From differential equation solvers to accelerated first-order methods for convex optimization (arXiv:1909.03145, Math. Program. 2022), introduce the NAG flow, a first-order system in a position x, an auxiliary variable v and a scaling parameter γ whose Lyapunov function decays exponentially for every μ≥0. In §6 they show that Nesterov's general scheme of optimal method (Algorithm 1) is itself a corrected semi-implicit discretisation of this flow, and they reprove its rates with one Lyapunov function that covers μ=0 and μ>0 at once. This mission formalises that analysis, Theorem 6.1.
Setting
Let V be a real Hilbert space with inner product ⟨⋅,⋅⟩ and norm ∥⋅∥. A function f:V→R with gradient map ∇f belongs to Sμ1 (μ≥0) if it is continuously differentiable and μ-convex,
f(x)−f(y)−⟨∇f(y),x−y⟩≥2μ∥x−y∥2∀x,y∈V,
and to Sμ,L1,1 if moreover ∇f is L-Lipschitz, with 0≤μ≤L<∞. A point x∗ minimises f globally.
Algorithm 1 (Nesterov accelerated gradient method) takes x0,v0∈V and γ0>0. For k=0,1,… it computes the positive root αk of Lαk2=(1−αk)γk+μαk, sets γk+1=(1−αk)γk+μαk and
yk=γk+μαkαkγkvk+γk+1xk,
chooses any xk+1 with the sufficient decreasef(xk+1)≤f(yk)−2L1∥∇f(yk)∥2 (for instance the gradient step xk+1=yk−L1∇f(yk)), and sets
vk+1=γk+11[(1−αk)γkvk+αk(μyk−∇f(yk))].
The Lyapunov function is
Lk=f(xk)−f(x∗)+2γk∥vk−x∗∥2,(74)
and Cγ0,L=γ0L(f(x0)−f(x∗))+2L∥v0−x∗∥2 (89).
Formalization targets
Goal: Theorem 6.1
For f∈Sμ,L1,1, every run of Algorithm 1 has 0<αk≤1 and
All four conclusions are part of the goal: (98) alone does not carry a rate.
Milestones
The equivalent form (96)–(97) (p. 24): Algorithm 1 is the scheme αkγk+1−γk=μ−γk, αkyk−xk=γk+1γk(vk−yk), αkvk+1−vk=γk+1μ(yk−vk)−γk+11∇f(yk) with the decrease step (97) and Lαk2=γk+1.
The formulas for vk and vk+1 in terms of yk, xk, ∇f(yk) (p. 24).
The direct-computation identity for 2γk+1∥vk+1−x∗∥2−2γk(1−αk)∥vk−x∗∥2 (p. 24).
Its μ-convexity bound (p. 25).
The one-step boundLk+1−(1−αk)Lk≤f(xk+1)−f(yk)+2γk+1αk2∥∇f(yk)∥2 (p. 25).
Lemma B.1 (p. 37): for Lkαk2=γk+1, γk+1=(1−αk)γk+μαk, positivity, αk≤1, αk≥min{γ1,μ}/L, and the bounds (129)–(130) on ∏i<k(1−αi).
A companion item states (103) of Remark 6.3 for Algorithm 1: with μ=0, γ0=L, v0=x0, f(xk)−f(x∗)≤k24L∥x0−x∗∥2.
Significance
Theorem 6.1 recovers, by a Lyapunov argument, the optimal rates of Nesterov's method in both regimes: O(L/(γ0k2)) for convex f and (1−μ/L)k for strongly convex f once γ1≥μ, with the parameter γk moving between them automatically. It covers every sufficient-decrease choice of xk+1, not only the gradient step, and it places Nesterov's method in the same family as the predictor–corrector and gradient-corrected schemes of §5, whose analyses share the Lyapunov function (74) and the rate lemmas of Appendix B. Comparing (99) with the rate (1+μ/L)−k of those schemes shows that Nesterov's method is slightly faster per step, with the same complexity.
The result is proved in the paper; the proof of (100) is omitted as similar to that of (88). Nesterov's rates for related parameterisations have been stated on this platform (Bubeck's monograph, Theorems 3.18–3.19), but not for Algorithm 1 with the adaptive parameter γk, and no machine-checked proof of Theorem 6.1 or Lemma B.1 is known. A formalisation checks the omitted step, pins down where αk≤1 is used, and adds a discrete Lyapunov toolkit for accelerated methods in Hilbert space.
Difficulty
Reading Algorithm 1 directly gives a three-sequence recursion with no visible monotone quantity: f(xk) itself need not decrease. The contraction (98) holds only for the specific combination (74), and only after the cross terms in ∇f(yk) produced by the v-update are matched exactly against the sufficient-decrease step; any slack in the step rule Lαk2=γk+1 leaves a positive gradient term. A second difficulty is uniformity in μ: when μ=0 the linear factor 1−min{γ1,μ}/L equals 1, so the O(1/k2) rate must come from a separate estimate of ∏i<k(1−αi) in terms of the step sizes, which are defined only implicitly by a quadratic equation.
Formalization scope
V is a real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace); the paper's duality pairing and dual norm are the inner product and the norm (Riesz identification).
The gradient is an explicit map gradf : V → V with HasGradientAt f (gradf x) x at every point; Mathlib's gradient is not used.
The classes are structures IsS1 and IsS11; Sμ,L1,1 includes 0<L and μ≤L, and the upper bound (4) is a consequence, not an assumption.
A run of Algorithm 1 is a structure IsNAGRun of hypotheses on given sequences, one per step. Step 2 records only αk>0 (the page writes αk∈(0,1), but αk=1 occurs when μ=L, and αk≤1 is a conclusion of the theorem). Step 5 is an inequality, not the gradient step. The step sizes are not replaced by a closed form.
x∗ is a global minimiser of f (the paper's standing assumption, p. 2); γ1 is the value produced by the run.
Indices start at 0; (1−s)k and (1−s)k−1 are natural powers, with (100) stated for k≥1; (99) is stated for all k≥0.
Milestones 2 and 3 are stated for one step of (96) with αk,γk,γk+1>0; milestones 4 and 5 along runs of Algorithm 1 under the hypotheses of Theorem 6.1.
In Lemma B.1, L:=supkLk is replaced by an arbitrary real upper bound L; the conclusions involving L weaken as L grows, so this is equivalent when the supremum is finite.
A statement that assumes the contraction (98) for arbitrary sequences, or fixes xk+1 to the gradient step, or states only (98), would not be Theorem 6.1 and is ruled out: the goal quantifies over all runs of Algorithm 1 and states all four conclusions.
Contributions welcome: proofs of Lemma B.1 (a self-contained statement about real sequences), the algebraic milestones 1–3, and the convexity steps 4–5. The definitions are local to this mission and duplicate those of the other missions of the series, to be merged later.
Selected references
H. Luo, L. Chen, From differential equation solvers to accelerated first-order methods for convex optimization, Math. Program. 195 (2022); arXiv:1909.03145v4. https://arxiv.org/abs/1909.03145
W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17 (2016); arXiv:1503.01243. https://arxiv.org/abs/1503.01243
S. Bubeck, Convex Optimization: Algorithms and Complexity, Found. Trends Mach. Learn. 8 (2015); arXiv:1405.4980. https://arxiv.org/abs/1405.4980
Douglas-Rachford Splitting and ADMM for Nonconvex Optimization: Tight Convergence Results III: ADMM Is Douglas-Rachford Splitting on the Image-Function Problem, for Every RelaxationResearch Paper
Motivation
The alternating direction method of multipliers (ADMM) solves linearly constrained problems
by alternating a minimization in x, a minimization in z and a multiplier update. It is one of the standard methods for distributed optimization, statistical learning and signal processing, and in practice it is often applied to nonconvex f or g (see Boyd et al., Distributed optimization and statistical learning via the alternating direction method of multipliers, 2011, doi:10.1561/2200000016).
For convex problems, ADMM with λ=1 is classically Douglas–Rachford splitting (DRS) applied to the Fenchel dual of (1.2) (Gabay 1983). The dual reading needs convexity. Themelis and Patrinos (arXiv:1709.05747v4, §5; SIAM J. Optim. 30(1), 2020, doi:10.1137/18M1163993) prove a primal equivalence instead: for arbitrary f,g and for every relaxation parameter λ, one ADMM update is one DRS step on a reformulation of (1.2) built from image functions. A primal equivalence for λ=1 was noted earlier by Bauschke and Koch (2015, Rem. 3.14) for A=−B=I, and Yan and Yin (2016, Thm. 1) showed that this case loses no generality. This mission formalizes the general statement and the convergence theorem for nonconvex ADMM that the paper derives from it.
Setting
All spaces are Euclidean, R=R∪{+∞}, A∈Rp×m, B∈Rp×n, b∈Rp. A function is proper if it never takes the value −∞ and is finite somewhere. The proximal mapping of h with stepsize γ>0 is the set
proxγh(s)=wargmin{h(w)+2γ1∥w−s∥2}.
For h:Rn→R and a linear map C, the image function is
(Ch)(s)=xinf{h(x)∣Cx=s}∈[−∞,+∞].
The β-augmented Lagrangian of (1.2) is Lβ(x,z,y)=f(x)+g(z)+⟨y,Ax+Bz−b⟩+2β∥Ax+Bz−b∥2. One ADMM update with penalty β>0 and relaxationλ>0 maps (x,y,z) to (x+,y+,z+):
One DRS step with stepsize γ and relaxation λ on φ1+φ2 maps s to s+=s+λ(v−u), where u∈proxγφ1(s) and v∈proxγφ2(2u−s). The reformulation of (1.2) is
s∈Rpminimize(Af)(s)+(Bg)(b−s),(5.1)
that is, φ1=(Af) and φ2=(Bg)(b−⋅). The regular subdifferential is ∂^, the limiting one ∂.
Formalization targets
Goal: primal equivalence (Theorem 5.5)
Let f,g be proper, β>0 large enough that every ADMM subproblem has a solution, and λ>0. With s=Ax−y/β, u=Ax, v=b−Bz and s+,u+,v+ the same expressions at (x+,y+,z+), and γ=1/β,
together with φ1(u+)=f(x+), φ2(v+)=g(z+), −y+∈∂^φ1(u+), −A⊤y+∈∂^f(x+) and dist(−B⊤y+,∂^g(z+))≤β∥B∥∥Ax++Bz+−b∥.
Milestones
Proposition 5.2(i)–(iii) (properness of (Ch), (Ch)(Cxβ)=h(xβ), prox(Ch)/β⊇CXβ), Proposition 5.3 (C⊤∂^(Ch)(sˉ)⊆∂^h(xˉ)), the inclusions (5.3a) and (5.3b), and the identity s+λ(v−u)=s+.
Companions
Theorem 5.5(vi): if A is surjective, (Af) is L-smooth and β>L, then φγDR(s+)=Lβ(x+,z+,y+). Theorem 5.6: under Assumption II and (γ,λ) in the ranges of Theorem 4.1 with β=1/γ, Lβ decreases by (1+γL)2cλ2∥Axk+Bzk−b∥2 per step, mini≤k∥Axi+Bzi−b∥=o(1/k), cluster points are KKT points with common cost, and the iterates are bounded when Φ is level bounded.
Significance
Theorem 5.5 reduces nonconvex ADMM to nonconvex DRS: any descent, convergence or rate statement for DRS on φ1+φ2 becomes one for ADMM, with the Douglas–Rachford envelope becoming the augmented Lagrangian (5.5(vi)). This is how the paper obtains Theorem 5.6, with explicit penalty bounds for every λ∈(0,4) permitted by Theorem 4.1, under assumptions weaker than earlier nonconvex ADMM analyses (Li and Pong, 2015, doi:10.1137/140998135, require A=I and coercivity).
The results are proved in the paper. No machine-checked proof of a primal ADMM–DRS equivalence is known; the platform holds formalizations of proximal ADMM variants and of convex DRS for monotone operators, but not of image functions. The mission produces a reusable library of image functions and their proximal and subdifferential calculus, and a precise statement of relaxed ADMM in the nonconvex, extended-real setting.
Difficulty
The individual steps are short, but the objects are extended-real and set-valued. An image function may equal −∞, and its infimum need not be attained; that (Af) is proper and that the infimum is attained at x+ must be derived from the solvability of the ADMM subproblems, not assumed. The proximal mappings are multivalued, so the equivalence is an inclusion between argmin sets, and the algebra relating y+/2, y+ and s+ has to be matched to the relaxation exactly. The subgradient claims require regular subdifferentials of extended-real functions, and (v) requires the optimality condition of the z-subproblem, whose quadratic term couples z+ with the residual. Theorem 5.6 additionally rests on the whole DRS convergence analysis of §4.
Formalization scope
Points are EuclideanSpace ℝ (Fin _), matrices are continuous linear maps, A⊤ is ContinuousLinearMap.adjoint, and ∥B∥ is the operator norm. Extended-real functions are EReal-valued; the image function imageFn is the EReal infimum over {x∣Cx=s}, so it is +∞ off the range and may be −∞. Proximal mappings and Xβ are sets, and an ADMM update (IsADMMStep) is any selection of minimizers in the order y+/2,x+,y+,z+. The two subproblems minimize the terms of Lβ that depend on the minimized variable, because the dropped constant g(z) may be +∞ at a starting point and would make every x a minimizer. "Large enough penalty" is SubproblemsSolvable. The regular and limiting subdifferentials are the published IsRegularSubgrad and LimitingSubdiff.
Added hypotheses: f and g proper in Theorem 5.5 and 5.5(vi), and h proper in Proposition 5.2(i). The page omits them, and they are necessary: for h≡+∞ every Xβ(s) is the whole space while (Ch)≡+∞ is not proper. Claim (v) is stated as the existence of w∈∂^g(z+) with ∥−B⊤y+−w∥≤β∥B∥∥Ax++Bz+−b∥, which is stronger than the distance bound and avoids the distance to an empty set. Theorem 5.6 uses the constants c of Theorem 4.1 as derived in its proof ((4.8), (4.10)); the printed (4.3) has the sign of one entry of a max reversed and the printed (4.5) an extra factor 1/λ, and both are then false (counterexamples in the companion mission on DRS convergence). Theorem 5.6 adds L>0; its run is indexed so that the paper's (xk,yk,zk) is the term k+1, with the starting triple at index 0.
The goal does not assume the DRS relations or (5.3a)–(5.3b), and s+,u+,v+ are defined from the ADMM iterates by (5.2), not chosen independently; a formalization that quantifies over an arbitrary prox selection, or that hard-codes λ=1, is a different statement.
Needed infrastructure: image functions and their proximal calculus, regular subgradients of extended-real functions under linear maps, and, for Theorem 5.6, the DRS convergence theory of §4 (formalized in the companion mission I of this series). Proofs of individual milestones are welcome independently.
Selected references
A. Themelis, P. Patrinos, Douglas–Rachford splitting and ADMM for nonconvex optimization: tight convergence results, SIAM J. Optim. 30(1):149–181, 2020. arXiv:1709.05747v4, doi:10.1137/18M1163993
H. H. Bauschke, V. R. Koch, Projection methods: Swiss army knives for solving feasibility and best approximation problems with halfspaces, in Infinite Products of Operators and Their Applications, Contemp. Math. 636, pp. 1–40, AMS, 2015.
M. Yan, W. Yin, Self equivalence of the alternating direction method of multipliers, in Splitting Methods in Communication, Imaging, Science, and Engineering, pp. 165–194, Springer, 2016.
G. Li, T. K. Pong, Global convergence of splitting methods for nonconvex composite optimization, SIAM J. Optim. 25(4):2434–2460, 2015. doi:10.1137/140998135
S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed optimization and statistical learning via the alternating direction method of multipliers, Found. Trends Mach. Learn. 3(1), 2011. doi:10.1561/2200000016
D. Gabay, Applications of the method of multipliers to variational inequalities, in Augmented Lagrangian Methods, Studies in Mathematics and Its Applications 15, pp. 299–331, Elsevier, 1983.