Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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).
Let and write for the binary points, the vectors each of whose coordinates is or , and for the unit cube. Let be a real valued function defined on .
For a set in a real vector space and , a convex underestimator of is a function that is convex on the convex hull and satisfies for every (Definition 3, p. 496). The largest convex underestimator of on , that is, a convex underestimator with on for every convex underestimator , is the convex lower envelope of . In this mission .
A function is convex piecewise linear with finitely many linear pieces on if there are and with for all .
The proof works with the polyhedron of affine minorants of ,
the function , and the linear program defining together with its dual
where lists the binary vectors.
has a convex lower envelope, and every convex lower envelope of satisfies
for some finite family of affine functions.
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 : on with , no convex underestimator reaches .
Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization produces the identity , a finite-dimensional LP duality statement for the pair –, 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).
Two steps carry the weight. The first is that the maximum defining 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 (for example when ) are covered by the paper's conclusion but not by those two cases, and require an argument that works on all of . Exactness at binary points uses that a binary point is not a nontrivial convex combination of other points of the cube.
Points of are Fin n → ℝ with the componentwise order; is Set.Icc 0 1, the binary points are the vectors with every coordinate or , and is the dot product. is a total function on of which only the values at binary points enter any statement. Convexity of an underestimator is required on , exactly as in Definition 3, not on all of ; the identification of this hull with is milestone 1, not a definition. The value is allowed and no hypothesis on is added.
The readings of informal words are: "the convex lower envelope" is a predicate (largest convex underestimator on ), 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 is stated with IsLeast. The proof's function is a real supremum, used only after its attainment is proved.
The convex lower envelope is not defined as (or as the value of ): 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 , 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.
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 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 is a property of the constraints at under which 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.
Consider the nonlinear program
with and continuously differentiable on . The feasible set is , and is the set of active inequalities. The KKT condition holds at for if there are and , with for , such that .
The linearized cone is , and is the polar of a set . For a convex set , the normal cone is defined for and is empty for . is the Euclidean projection onto a nonempty closed convex set .
For a point , the linearized set consists of the with
It keeps the inequalities that are active or violated at and drops those strictly satisfied at .
A feasible satisfies SAKKT for if there are , and , with whenever , such that
It satisfies AGP(0) for if there is with . The outer limit of a set-valued map is the set of limits of sequences with (1.6). The point is SAKKT-regular (Definition 4.3) if
For continuously differentiable constraints and a feasible ,
The forward implication says SAKKT-regularity is a strict constraint qualification for SAKKT; the backward one says it is implied by every such qualification.
Theorem 4.5 describes exactly the constraint systems on which a SAKKT sequence converging to 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 varies outer semicontinuously as .
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 at perturbed points, and the identification of with .
The forward direction passes to the limit in normal cones of sets that change with : the set of rows kept depends on the sign of at the moving point, not on the active set at . Projections land at , while SAKKT-regularity speaks of normal cones at , so the normal vectors must be transported from to ; 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 . Finally, and the KKT multipliers are linked by Farkas' lemma for a finitely generated cone.
EuclideanSpace ℝ (Fin n); indices are Fin m and Fin p; gradients are Mathlib's gradient.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.
A switch network is a set of queues served by servers. In every time slot each server can serve at most one queue, so a scheduler must pick a matching of queues to servers. Such systems model input-queued packet switches, crowdsourcing platforms that route job types to worker types, and wireless links with unknown channel quality. When the success probability of each queue–server link is unknown, the scheduler has to learn it from the services it observes while the queues are building up. This makes switch scheduling a multi-armed bandit problem in which the cost is not cumulative reward but queue length.
Krishnasamy, Sen, Johari and Shakkottai (arXiv:1604.06377, Operations Research 2021) measure a scheduler by its queue-regret: the expected difference between its queue lengths and those of a genie that knows the best matching. They show that the queue-regret has two regimes. In the late stage, once the queues regularly empty, it decays like (their Theorem 3, the subject of a sibling mission). In the early stage it grows like , as the regret of a classical bandit does, and the system is then effectively unstable. This mission is about the early stage, made precise in the paper's Theorem 8: in heavy traffic, where the arrival rates are close to the best service rates, every reasonable policy pays logarithmic queue-regret for a long time.
The lower-bound technique descends from Lai and Robbins (1985): a policy that does well on every instance must explore each sub-optimal link about times, a count obtained by a change of measure and the Bretagnolle–Huber inequality.
Queues are indexed by and servers by . In every slot , queue receives an arrival , and link offers a service . All of these are independent and i.i.d. over slots. Notation:
Assumption 1 asks that every queue have a unique best server and that the best servers of distinct queues be distinct. Assumption 2 is for every . Assumption 3 draws the initial queue vector from the stationary law of the genie queues.
A scheduler picks a matching , so queue is served by server . Its decision may use the past schedules, the services observed on the scheduled links, and private randomness. The queues evolve as . The genie always schedules and has queues . The queue-regret is . The schedule counts are .
A policy is -consistent () if on every instance for all and all , with a constant that may depend on the instance. The key constant is
where is the Bernoulli Kullback–Leibler divergence.
Fix , an -consistent policy and . There exist constants and , the same for every arrival vector , such that, with and :
Theorem 8 complements the late-stage lower bound. Together they show that queue-regret goes through a phase transition. Up to time of order , the queue-regret of any consistent policy grows like . Since the left end of the window does not move as while the right end grows like , the heavily loaded regime is exactly where learning costs are visible in queue lengths. The theorem also explains why algorithms designed for the late stage (Q-UCB, Q-ThS in the same paper) cannot avoid this early cost.
The formalization adds a machine-checked statement of a lower bound whose constants are pinned down precisely. In particular it states which quantities and may depend on (see below). Along the way it builds a reusable model of a learning switch scheduler: randomized, history-dependent policies, the coupled genie system and the stationary initial law. It also provides a Lai–Robbins-type count bound (Lemma 19) for matching bandits. The results are proved on paper in the held preprint (§9.2). To the best of the platform's records none of them has been formalized.
The obvious route to Theorem 8 is to bound the queue-regret below by the regret of the corresponding bandit. That fails, because queue-regret is not cumulative: an empty queue forgives past mistakes. The proof therefore needs the stationary start (Assumption 3), so that and the sub-optimal schedules show up as a drift (Lemma 22). This holds only up to a load term , which limits the window.
The count bound (Lemma 19) requires a change of measure between two instances that swap the best servers of two queues. It needs a chain rule for the KL divergence of adaptively collected observations, where the policy's own randomness must cancel. Neither the swapped instances nor the trajectory law are standard Mathlib objects.
Fin U and servers are Fin K, with and . is trivial, and for it is an empty minimum.Fin U ↪ Fin K.The source is the arXiv v4 preprint; the paper's proofs are in its §§8–9. Welcome contributions include the KL chain rule for adaptively scheduled Bernoulli observations, stationarity of the geometric law for the genie chain, and measurability of the trajectory.
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 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 is a property of the constraints at under which 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.
Consider the nonlinear program
with and continuously differentiable on . The feasible set is , and is the set of active inequalities. The KKT condition holds at for if there are and , with for , such that .
The linearized cone is , and is the polar of a set . For a convex set , the normal cone is defined for and is empty for . denotes the Euclidean projection onto a closed convex set .
For and a point , the linearized set of (4.2) consists of the with
A feasible satisfies AGP() for if there is a sequence with
The outer limit of a set-valued map is the set of limits of sequences with (1.6). The point is AGP-regular (Definition 4.1) if
For continuously differentiable constraints and a feasible ,
The forward implication says AGP-regularity is a strict constraint qualification for AGP; the backward one says it is implied by every such qualification.
The same characterization for the Linear AGP condition (LAGP), in which the linear constraints are kept exact and the iterates stay in the set they define. LAGP-regularity (Definition 4.4) is outer semicontinuity of relative to . Two further items accompany it: Proposition 4.1, the explicit form of , and the equality appended to Definition 4.4.
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 as the polar of the linearized cone. These facts are reusable for any sequential optimality condition built on projections.
The forward direction passes to the limit in normal cones of sets that vary with and are evaluated at perturbed points , which may lie outside . For finite the inclusion of in fails at such points. It holds only for 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 . The identification of with needs the localization of a polyhedral normal cone, and the link between and KKT multipliers is Farkas' lemma for a finitely generated cone.
EuclideanSpace ℝ (Fin n); indices are Fin m and Fin p; gradients are Mathlib's gradient.All objects are defined in the namespace StrictCQ.AGP. Proofs of the convex-analysis milestones are reusable beyond this mission.
An agent whose preferences change over time cannot simply optimize. Under non-exponential discounting, for instance hyperbolic or pseudo-exponential discount functions, a plan that is optimal today stops being optimal tomorrow, and a later self deviates from it. Strotz (1955) proposed that a sophisticated agent treat future selves as players in a game and look for a subgame-perfect equilibrium strategy instead. In discrete time this notion is unambiguous. In continuous time, Ekeland and Lazrak (2006) gave the first rigorous definition, through a first-order (derivative-type) condition, and nearly all later work on time-inconsistent stochastic control in continuous time uses it.
Huang and Zhou (2021) point out that this standard notion, here called a weak equilibrium, can admit strategies that the agent strictly wants to abandon over arbitrarily short intervals. They introduce a strong equilibrium, which rules out every profitable short deviation. For a controlled finite-state Markov chain they characterize both notions and prove that both exist under compactness. This mission formalizes that existence theorem together with the expansions and characterizations it rests on.
Let . A continuous-time Markov chain on is controlled through its generator , with -th row . A row must lie in
and an admissible set is fixed for each state. The control space is .
A payoff rate is paid at time difference when the chain is in state and uses row . The standing assumptions are that is continuous on and that, for every , is integrable in . The expected payoff is
For , the concatenation follows on and afterwards.
The first-order gain of a row in state is .
Suppose every is nonempty, convex and compact, is continuous on , and is concave. Then
If moreover is strictly concave and satisfies the and remainder conditions of Lemma 3.2, then
Theorem 3.3 is the general existence result of the paper. Theorem 3.1 and Proposition 3.2 give a way to find equilibria in a given model, but they do not say whether one exists. Remark 3.4 shows that without compactness of the , no equilibrium need exist. The strong half shows that the stricter concept is not empty in general: under strict concavity a strong equilibrium exists. Example 4.3 of the paper shows that weak equilibria need not be strong, so the two halves are different results.
The paper gives a proof, and none of it has been formalized. A formalization produces a checked equilibrium-existence theorem for a controlled continuous-time Markov chain. It also produces reusable small-time expansions of matrix-exponential payoffs. These expansions are shared by the paper's other results: the two-state example and the convergence of discrete-time equilibria.
The fixed-point step itself is routine once its hypotheses are in place. The work lies in the analysis that feeds it. First, the continuity of needs a limit passage under an infinite-horizon integral, which requires a uniform integrable bound on along a converging sequence of generators. Second, the step from a fixed point to a weak equilibrium goes through Theorem 3.1, whose hypothesis (3.3) is not among those of Theorem 3.3. Showing that without (3.3) is not one of the paper's numbered statements. Third, the strong half needs Proposition 3.2. Its proof treats deviations that agree with in the current state, which are felt only at second or higher order in , through the first order at which the chain can reach a state where the deviation differs. The obvious argument, comparing first-order terms only, says nothing in that case.
States are Fin N, so state of the paper is index . Rows are Fin N → ℝ and generators are Matrix (Fin N) (Fin N) ℝ with the entrywise topology. Expectations are not built from a Markov process. Under the law of given is the -th row of , so . Under the transition matrix is for and afterwards. Integrals are Bochner integrals over . The norm in (2.3) is the sup norm, which is equivalent because (2.3) quantifies over every . The liminf in the weak-equilibrium definition is encoded as "for every , eventually ". "Increasing" in (3.4) and (3.15) means nondecreasing.
Two hypotheses are added to the printed Theorem 3.3:
The shift bound (3.3) is deliberately not assumed in the weak half. No statement assumes integrability of a payoff; it follows from (2.3) because is a stochastic matrix. The time derivative in Lemma 3.2 is tied to by a derivative condition, and is meaningless otherwise. These choices rule out formalizations that are trivially true because an integral is junk or an admissible set is empty. Every hypothesis on ranges over only.
A complete development needs:
The matrix-exponential facts about generators are reusable beyond this mission. Contributions to any milestone are welcome, and so are lemmas on generators and .
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 that couple the continuous positions with the flow variables .
Section 7 of the paper studies the convex relaxation used for these bilinear equalities in isolation. Products of valid inequalities linearized by 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 , which is the property that makes the mixed-integer formulation exact at binary flows.
Fix and . Points of are written .
Always , and is convex.
Let be compact and convex, let be a polytope and let be an extreme point of . Then for all and ,
The result. In the paper's mixed-integer program each vertex contributes a bilinear set in which is the convex set at and is the polytope of flows on the edges at . Binary flows corresponding to a path are extreme points of these polytopes, so Lemma 7.4 says that replacing by 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 to compact convex sets . Proposition 7.1 is what makes the relaxation finite: it replaces the infinitely many inequalities of by one perspective-cone constraint per facet of .
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.
The direction is one line, since . The converse at needs three ingredients that are each standard and none of which is in Mathlib in this form.
Proposition 7.1 as an equality needs an affine Farkas lemma, and its printed proof skips the case of the valid inequality .
is Fin n → ℝ, inner products are dotProduct, is Z *ᵥ c and 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 on the product, not an inner product.
Hypotheses added relative to the page, each with a counterexample to the printed form:
Several hypotheses are dropped where they are not needed, which strengthens the statements: nonemptiness of throughout, and boundedness and finiteness in the inclusion of Proposition 7.1 and in the active-constraint milestone.
Trivializing formalizations ruled out: quantifies over all of and is not replaced by (7.3) in the goal; is never allowed to be merely closed in the goal; the hypotheses of the goal are satisfiable (, is checked in Lean).
A complete development needs the bipolar theorem for closed convex cones in , 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.
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 phrased through sequences 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.
Fix and continuously differentiable functions , , where carries the Euclidean inner product and norm . The feasible set is , and is fixed. An index is active when .
For an objective , the point satisfies KKT if there are and with , for inactive , and .
Scaled-AKKT holds at for if there are sequences , and with , such that for every , and
where is the supremum norm of a multiplier vector.
The Mangasarian–Fromovitz constraint qualification (MFCQ) holds at if are linearly independent and some satisfies for all and for all active . The cone of active gradients is
For a constraint system and a feasible ,
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).
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 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.
The forward direction splits on whether the multipliers stay bounded, and the unbounded case requires normalizing by 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 with . The printed text chooses , which has the wrong sign for the objective ; milestone 6 is stated for every , so the sign issue does not propagate.
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 , is (the paper's "continuous first-order derivatives"), every objective in the goal is , and is feasible. The objective is quantified inside the equivalence, so the left side of the goal depends on , , alone. "or" is inclusive. The cone condition is equality of the cone with all of , not with its linear span. KKT carries both the sign condition 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 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.
Data-driven control asks for a controller computed directly from measured trajectories of an unknown system, without first identifying a model. When the measurements are corrupted by unknown process noise, many systems explain the same data, and a controller designed from the data alone is only trustworthy if it stabilizes every one of them. Van Waarde, Camlibel, Eising and Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) show that this robust design problem is an implication between two quadratic matrix inequalities (QMIs), and they develop matrix versions of Yakubovich's S-lemma and of Finsler's lemma to decide such implications by a linear matrix inequality (LMI).
Timeline:
All matrices are real. is the set of symmetric matrices; () means is symmetric positive semidefinite (definite), and means .
QMI solution sets. For partitioned with , ,
with and defined by "" and "". The generalized Schur complement is , with the Moore–Penrose pseudo-inverse, and is the class of with , and .
Data. The unknown system is with , . The measured data are and ; and are the first and last columns of . The unknown noise satisfies for a given . The systems compatible with the data form
and . The data are informative for quadratic stabilization (Definition 2.1) if some and satisfy for all .
Let be the -square matrix
For and data generated by the system:
(a) the data are informative if and only if with (5.5);
(b) if moreover and , the data are informative if and only if with (5.6);
(c) whenever (5.5) or (5.6) holds, satisfies the Lyapunov inequality with that and makes Schur stable for every .
The vector S-lemma, strict S-lemma and Finsler's lemma (Lemmas 4.1–4.3); the completion and lifting lemmas 4.4–4.5; the reduction of matrix inclusions to vector implications (Theorem 4.6); the matrix S-lemmas
(Theorems 4.7, 4.10–4.12, Corollary 4.13); and the three claims of §5.1 that put Theorem 5.1 in the form of Corollary 4.13: , the Lyapunov inequality is , and , .
Theorem 5.1(a) is an exact test, with no rank condition on the data and no Slater condition on the noise model, for the existence of one state-feedback gain with a common quadratic Lyapunov function that stabilizes every system consistent with noisy data. The test is a semidefinite feasibility problem in and returns the controller . It covers energy bounds, per-sample bounds, sample-covariance bounds, noise in a known subspace and exact data within one statement, and its matrix S-lemmas are the tools reused in the paper's further results (the reduced LMI and explicit gain of §5.2, Petersen's lemma in §4.5).
None of these results has a machine-checked proof. Mathlib has the Loewner order, positive (semi)definiteness and spectral theory of symmetric matrices, but no S-lemma, no Finsler lemma, no Moore–Penrose pseudo-inverse for matrices and no theory of QMI solution sets. A formalization would supply these as reusable linear-algebra results and would certify the design rule .
The "if" directions are direct computations: multiply out a Schur complement. The difficulty is in the "only if" directions. The S-lemma's converse relies on the hidden convexity of the joint range of two quadratic forms (Dines' theorem), which is not a consequence of finite-dimensional convex duality alone. Passing from matrices to vectors requires Lemma 4.5, which builds a full matrix solution of the QMI from one vector; it uses the pseudo-inverse factorization of and fails without . In Theorem 4.11 the existence of the margin comes from a compactness argument on an unbounded solution set, after splitting off the kernel of . The obvious approach, applying the strict matrix S-lemma (Theorem 4.10) directly, does not work because is only semidefinite in the noise models of interest.
Matrices are Matrix ι ι ℝ over finite index types; a matrix in is indexed by ι ⊕ κ, and block matrices are Matrix.fromBlocks / Matrix.fromRows. and are Mathlib's PosSemidef and PosDef, which include symmetry, as the paper's §1.1 convention does. The pseudo-inverse is defined as the unique matrix satisfying the four Penrose conditions, not Matrix.inv, which returns on singular matrices. "Stabilizing gain for all of " is stated as the Lyapunov inequality with the LMI's together with .
The following are added or made explicit:
The goal adds no hypothesis . A formalization in which may be empty, or in which the pseudo-inverse is a junk value, would be trivial or false, and the definitions rule both out.
Contributions are welcome for the pseudo-inverse API (existence, uniqueness, identities), the S-lemma and Finsler's lemma (reusable beyond this mission), and the Schur-complement factorizations (3.2)–(3.4). Platform items ConvexOptimization.s_procedure (inhomogeneous S-procedure) and ConvexOptimization.field_of_values_psd_witness (Dines) are natural proof tools for Lemma 4.1.
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 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.
There are stages. The decision at stage is ; are matrices and . Stage 1 is deterministic: . For a random outcome ranges over a finite set , independently of earlier stages, and enters through the right-hand side . The feasible set of stage given the previous decision is
A coherent risk measure maps random costs to and is subadditive, monotone (), positively homogeneous and translation equivariant (). Larger is worse: these are costs. Each stage carries a one-step coherent risk measure on random costs over . It is extended to costs in by whenever some outcome has infinite cost.
For fix points and numbers . The inner approximation is the lower boundary of the convex hull of the pairs :
which is off the convex hull of the points, with . The policy's stage problem (13) and the first-stage problem (8) are
The numbers are upper bounds when for all and . A policy defined by the inner approximation, , takes at each state and outcome an action solving (13), and a first-stage action solving (8). The actual risk-adjusted cost of over stages is
with no future term at . The nested risk-adjusted cost of the policy is .
The bound holds for every , every family of coherent , every choice of points satisfying the upper-bound property, and every minimizing selection .
Proposition 3, the risk-neutral case . Proposition 4, the subgradient rule for given by its dual representation. The existence of a policy , which shows that the hypotheses of the goal can be met.
Proposition 5 makes the inner approximation a certificate. Any policy computed by minimizing against has nested risk-adjusted cost at most , a number obtained by solving one linear program. Together with the lower bound from outer approximation it brackets the risk-adjusted optimal value. The gap 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 to . It also pins down the exact form of the upper-bound hypothesis the induction needs.
The obvious reading of the hypothesis on p. 16, " is an upper bound on " with the true value function , does not support the induction. The policy does not act optimally, so its cost can exceed the true value, and the inductive step compares with the policy's own stage value , not with . 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, 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 , and the extended-real arithmetic must not silently produce a value the paper does not intend.
Vectors are Fin n → ℝ, all stages share and , 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 of the function they define, so pts s j is and qv s j is . Stagewise independence is built in: ranges over whatever happened before.
Standing assumptions made explicit in the statements:
The risk measures act on real random costs and are extended by 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 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 nor the induction claim; the policy must minimize at every feasible state, not only along visited states; and the statement is for general and general coherent , not the expectation. The bound is trivially true when and is informative when lies in the convex hull of the stage-1 points.
A complete development needs:
The first two are reusable for any SDDP-type development. Proofs of the milestones in any order are welcome.
Multistage stochastic programs model sequential decisions under uncertainty: hydro-thermal scheduling, inventory and capacity planning, portfolio management. The dominant solution methods, Stochastic Dual Dynamic Programming (SDDP, Pereira and Pinto 1991) and its relatives CUPPS and DOASA, never compute the Bellman (future-cost) functions of the problem. Instead they build outer approximations of them by cutting planes: affine minorants obtained from the optimal values and Lagrange multipliers of one-stage subproblems. Practitioners run these methods on very large problems, so the question of whether, and in what sense, the approximations converge is of direct practical relevance.
Earlier convergence proofs (Philpott and Guan 2008; Shapiro 2011) rely on linear stage problems, where only finitely many distinct cuts can be generated and convergence is finite. Girardeau, Leclère and Philpott (Math. Oper. Res. 2015) prove convergence for convex stage problems, where infinitely many distinct cuts may appear and finite termination is lost. This mission covers the first half of that paper: the deterministic multistage problem (§2), whose proof contains the whole scheme of the argument. The stochastic scenario-tree version is the companion mission of this series.
Fix a horizon . States lie in and controls in ; values are in . The data are state sets , control multifunctions , stage costs , linear dynamics , a final cost and an initial state . The problem (1) is
The Bellman functions are on and elsewhere, with .
Assumptions (H₁) require to be a convex multifunction with convex compact values; and to be convex, lower semicontinuous and proper; and to be finite and Lipschitz on . They also require extended relatively complete recourse (ERCR): for some , on the enlarged set (a -neighbourhood inside the affine hull of ) the cost is finite and some admissible control leads into .
The cutting-plane method keeps approximations , starting from and with . At iteration it runs forward from . At each stage it solves the one-stage problem with in place of , which gives a minimizer , the optimal value and a Lagrange multiplier of the constraint . It then adds the cut
and moves to . The approximate cost-to-go is .
For every run of the method and every ,
The first limit says the computed decisions become optimal for the true Bellman functions; the second says the cuts become exact at the visited states. Nothing is claimed away from the generated trajectories.
In the order the proof uses them:
Companion items state that runs exist under (H₁) and give Kelley's cutting-plane lemma (Lemma 2.1), the warm-up result of §2.
Theorem 2.1 is a convergence guarantee for cutting-plane decomposition of nonlinear convex multistage problems. It does not depend on finitely many dual extreme points, so it covers problems with nonlinear convex costs and convex control constraints. The result is the template for the stochastic Theorem 3.1, which covers SDDP, CUPPS and DOASA as special cases of a general node-selection scheme. Along the way the paper isolates ERCR, a constraint qualification that is exactly what bounds the Lagrange multipliers and makes the cuts uniformly Lipschitz.
The result is proved in the paper; as far as is known it has no machine-checked proof. This mission produces a Lean statement of the deterministic algorithm, with extended-real Bellman functions, cut validity, and multiplier selection as a predicate on runs. It also supplies the statements of the reusable lemmas: marginal-function convexity, the monotone-minorant lemma, Kelley's method. Formal proofs of the milestones, alternative arguments, and explicit Lipschitz constants are all open.
The naive argument, "the approximations increase and are bounded by , so they converge", only gives pointwise convergence of to some limit below . It does not show that the limit equals at the states actually visited, and the visited states change from iteration to iteration. The proof must control cuts computed at one state when they are evaluated at another. This needs a uniform bound on the multipliers . That bound comes from ERCR (moving a distance in every direction of the affine hull stays where the cost is finite), together with Lipschitz continuity of on a compact set lying inside the relative interior of its domain. Without ERCR the multipliers can be unbounded and the argument breaks. A second difficulty is the backward induction itself: the conclusion at stage uses both limits at stage , and passing from to needs a compactness argument (Lemma 5.2).
States are EuclideanSpace ℝ (Fin d) and controls EuclideanSpace ℝ (Fin p); costs and value functions are EReal-valued. Convexity of an extended-real function means convexity of its epigraph. Minima are EReal infima ( over an empty set), with attainment stated separately. is extended by outside .
The Lagrange multiplier condition is encoded by (12): lies in the direction space of and is a subgradient, on , of the stage optimal value at . A run is a predicate on : any minimizer and any multiplier are allowed. The paper's iteration is Lean's k + 1.
Standing assumptions added to (H₁), all used by the paper's proofs:
Deviations from the page:
Limits are Tendsto … (𝓝 0) in EReal. There, convergence to forces the differences to be eventually finite, so a value of cannot make a limit hold for free. The goal's hypotheses are exactly (H₁) and the run predicate. Statements that only assert the existence of a good run, or bound instead of the cuts, are not formalizations of Theorem 2.1.
A complete development needs:
All three are reusable well beyond this mission. Proofs of any milestone are welcome, as are proofs of the companion items.
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.
There are products . Product has a price , a quality level and a service duration , which must lie in a fixed interval . The parameters are: , the consumers' sensitivity to quality; , the utility of one unit of service time; , so that producing one unit at quality costs ; and , so that service costs per unit of time. The sign of is free: higher quality may make service cheaper (), dearer (), or leave it unchanged ().
A consumer buys product with the MNL choice probability
where the is the outside option of buying nothing. With market size one, the firm's profit is
and the bracket is the markup of product . Consumer surplus is
Three problems are compared, at the same pre-determined qualities and durations :
Section 5.1 adds the manufacturer's short-term problem (10): qualities are fixed, and the firm also chooses which products to offer.
For every maximizer of each of the three problems,
The inequalities are weak; equality holds, for instance, when the pre-determined are already optimal.
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.
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 , with 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 with defined as the optimal profit, without linking them to the maximizers, proves nothing about consumer surplus.
Fin N (0-based); is arbitrary and is allowed. The outside option is the in the denominator, not a product.A formalization in which the maximizers are given by the paper's closed-form prices, in which are defined as optimal values and only 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.
Firms that sell durable goods set three things at once: a price, a quality level, and the length of an ancillary service that comes free with the product, such as a warranty. Wang, Ke and Cui (SSRN 3766191; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2020.0947) study these joint decisions under multinomial logit (MNL) demand. For a monopolist offering several products they show (their Theorem 1) that each service duration is extreme (the shortest or the longest allowed), each quality is set product by product, and all markups are equal.
A natural question is whether that structure survives competition. In practice, quality and warranty terms are long-term strategic choices while prices react to rivals; if competition changed the optimal qualities and durations, the monopoly analysis would say little about real markets. Section 2.4 of the paper answers the question for an oligopoly of single-product firms. This mission formalizes that answer, Theorem 2.
There are firms; firm sells product . Product has a quality sensitivity , a base service cost per unit time , a marginal effect of quality on service cost (of either sign, or zero), a production-cost coefficient (cost ), and a service utility per unit time . Firm chooses a price , a quality and a service duration .
A consumer buys product with the MNL choice probability
where the is the outside (no-purchase) option. The payoff of firm is its markup times its market share:
A Nash equilibrium is a profile with every such that no firm can raise by changing its own triple , jointly, to any other triple with duration in . The monopolistic case is problem (4): one firm maximizes over all prices and qualities in and durations in . Finally, the duration index of product is
Assume for all , , and for all . Then
for every optimal solution of the monopolist's problem, which exists. The goal compares with any monopoly optimum and does not presuppose the monopoly formulas of Theorem 1.
The proof in the Online Supplement (pp. 2–3) passes through the following statements, which are the mission's milestones:
The result. Theorem 2 says that the quality and service rules of the monopoly are robust to competition: each firm sets quality where marginal consumer utility equals marginal cost, and offers the shortest or the longest service, regardless of what its rivals do. Only prices respond to competition, and they fall. The proof also shows that the competitive aggregate exceeds the monopolist's, so more consumers buy and consumer surplus is higher than under monopoly. Uniqueness makes comparative statics well defined.
Formalizing it. The theorem is proved in the paper and, to our knowledge, not formalized anywhere. A formal proof requires the MNL price-competition equilibrium argument (existence and uniqueness through a one-dimensional aggregate), which is a standard tool in operations management and industrial organization (Anderson, de Palma and Thisse 1992) and has independent reuse value. Making the argument precise also exposes two points the paper leaves implicit: the tie case in the duration choice, and the domain on which the bound holds.
The game is not concave: is not concave in firm 's own strategy (its best attainable value is convex in the duration , which is why durations end up extreme), and strategies are unbounded in price and quality, so the standard existence theorems for concave games with compact strategy sets do not apply. Writing down the first-order conditions and solving them produces candidates, but it shows neither that a candidate is a global best response nor that no other equilibrium exists. Uniqueness also fails without the no-indifference condition (see below).
Fin N (0-based); is arbitrary. The outside option is the 1 + in the denominator, not an element of Fin N.CarbonDoubleCount.Planner.IsPureNash) with Function.update: deviations are unilateral and joint in , not coordinate by coordinate.Formalizations that do not count: a price-only game with qualities and durations fixed at the monopoly values (that is the paper's reduction, not the theorem); a two-firm version; an equilibrium notion checked one coordinate at a time; or an equilibrium assumed rather than proved to exist.
A complete development needs real analysis of one-variable functions (monotonicity, the intermediate value theorem, maximization of -type functions) and finite sums. The pure-Nash definition and the MNL price-competition milestones (4–8) are reusable beyond this paper. Proofs of any milestone, and alternative arguments for the price-equilibrium uniqueness, are welcome.
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.
A firm sells products, . For product :
The firm chooses prices , qualities and service durations . Under the MNL choice model (2) a consumer buys product with probability
the being the no-purchase option. With unit market size, the total expected profit (3) is
Service durations lie in an interval , the shortest and longest durations the firm may offer.
The uniform-duration problem (7) adds the constraint for all :
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.
is unique, and it is the optimal profit over prices and qualities, attained at , . 2. . is differentiable with . 3. The numerator. has nonnegative derivative. 4. Quasi-convexity. is quasi-convex in . 5. (25). The root equation is equivalent to with , so increases with . 6. Convexity of . is convex in .
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 or ) under and the non-degeneracy assumption that some product has or .
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 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.
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 exactly: as the root of (24), a fixed-point equation in which 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 .
Conventions committed to in Lean:
Fin N, 0-based; is allowed. The outside option is the constant in the MNL denominator, not a product.fun _ => t; the goal assumes .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 instead of one shared ; and an existential statement in which may be any point of .
The definitions needed are the MNL choice probability and profit, plus the scalar functions , and 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.
Dynamic pricing asks a seller to post prices to a stream of customers and learn demand from purchase decisions alone. Luo, Sun and Liu study the contextual version in which a customer's valuation is linear in a covariate vector plus noise with an unknown distribution (arXiv:2109.07340v2; Mathematics of Operations Research, 2024). Their DIP policy estimates the linear part, discretizes the remaining price residual, and then runs an upper-confidence-bound rule on the discretized problem. Because the linear part is only estimated, the discretized problem is not an ordinary linear bandit: its reward parameter drifts from period to period by an amount controlled by the estimation error. The paper calls this a perturbed linear bandit (PLB) and proves an upper bound for it whose dominant extra term is linear in the perturbation size times the horizon.
This mission formalizes the matching statement: no algorithm can avoid that linear term. It is the paper's Proposition 2 (p. 22), proved in its Appendix A (pp. 44–46).
Fix a dimension . A perturbed linear bandit with perturbation constant consists of parameters , finite action sets and noise variables , with for all periods . In period an algorithm sees the action set and the history of its past actions and rewards, plays , and observes the reward
The algorithm may randomize. The parameters are never observed.
For a central parameter the paper defines the parameter set
so any sequence in has perturbation at most .
The PLB regret over periods compares each action with the best action of the current period:
The expectation is over the algorithm's randomness and the noise.
For every with positive entries (and ) there is depending only on such that for every with and every algorithm there are parameters and action sets with
The formal statement also records that the constructed instance is a PLB with perturbation , that its action sets are nonempty, and that every action has a single nonzero entry with , which places the hard instance inside the class covered by the paper's upper bound (Lemma 3, Conditions 1 and 3).
The result. Lemma 3 of the paper bounds the regret of its M-LinUCB algorithm on a PLB by a -type term plus . Proposition 2 shows that the second term is not an artefact of the analysis: an adversary who may move the parameter inside a box of width forces every algorithm to pay order . In the pricing application the perturbation is proportional to the estimation error of the linear part, so the lower bound explains why the paper's pricing regret bound (Theorem 1) carries a term linear in the accumulated estimation error. The result also separates the PLB from the zero-perturbation linear bandit, where regret is achievable.
Formalizing it. The proposition is proved in the paper; it has not been machine-checked. A formal proof requires an explicit model of randomized, history-dependent algorithms interacting with an adversarially chosen but deterministic parameter sequence, which the mission supplies. The model and the two-point construction are reusable for other two-hypothesis lower bounds in linear and contextual bandits.
The obvious argument fixes one hard instance and shows that every algorithm suffers on it. That fails: for a fixed parameter sequence, an algorithm that always plays the optimal action of that sequence has zero regret. The instance must therefore be chosen after the algorithm, and it must be chosen period by period, because the law of the period- action depends on the rewards of periods , which depend on the parameters already chosen. The parameters must nevertheless be deterministic: the adversary may react to the law of the algorithm's action, not to its realization. Making this recursive construction precise, together with the measurability needed for "the probability that " to be meaningful, is the main formal work. The arithmetic of each period is elementary.
A second point concerns the dimension: the construction needs two distinct coordinates, and for the statement fails, since every parameter in is then positive and playing the largest action has zero regret.
Fin d (0-based); periods are 1-based. Vectors are Fin d → ℝ, and is Mathlib's sup norm on that type. Action sets are finite sets (Finset). The maximum over an empty action set is set to ; every statement requires nonempty action sets.Contributions welcome: proofs of the two milestones, the measurability of the recursively defined actions, and the summation step from the per-period bound to the goal.
Quadratically constrained quadratic programs (QCQPs) minimize a quadratic function subject to quadratic inequality and equality constraints. They model trust-region subproblems, robust least squares, max-cut and many problems in signal processing and control. They are NP-hard in general, so practice relies on convex relaxations, and the standard one is the Shor semidefinite (SDP) relaxation. The SDP relaxation lifts variables to an positive semidefinite matrix, which is expensive for large .
For an important subclass, the simultaneously diagonalizable QCQPs (SD-QCQPs), a much cheaper relaxation is available: after a change of variables all quadratic forms are diagonal, and the products can be relaxed by new variables . This is a second-order cone (SOCP) relaxation, studied by Ben-Tal and den Hertog (2014) and Locatelli (2016) for the trust-region problem with additional constraints and related problems. Whether one may use the SOCP relaxation in place of the SDP relaxation without losing anything, for the optimal value and for the convex-hull description, is the question settled here.
This mission formalizes Proposition 1 of A. L. Wang and F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs (Math. Program., 2021; arXiv:1911.09195v3), §4.2.1 and App. A, together with Lemma 9 of §4.2.
A QCQP (1) in variables has data , , for , with constraints of which the first are inequalities. Writing ,
The SDP relaxation (3) uses and the lifted variable with :
Its projected epigraph (4) is the set of for which some satisfies these constraints together with .
A family is simultaneously diagonalizable (SD) if there is an invertible with every diagonal (Definition 4); an SD-QCQP is a QCQP whose matrices are SD (Definition 5). Changing variables by gives a diagonal QCQP (10): with , so with . For it, the SOCP relaxation (11) is
and (12) is the set of for which some satisfies these constraints and .
The dual set is .
For a diagonal QCQP (10),
No regularity assumption is made; both values may be or .
For any SD-QCQP, is polyhedral.
The result. Proposition 1 transfers every SDP-tightness and convex-hull criterion to the SOCP relaxation of an SD-QCQP. The paper's main theorems give sufficient conditions for and for under the assumption that is polyhedral; Lemma 9 shows this assumption holds for every SD-QCQP, and Proposition 1 then gives the same conclusions for an SOCP with only additional variables and convex quadratic constraints instead of an semidefinite matrix (Remark 12). The value identity was first recorded by Locatelli (2016); the set identity is, according to the authors, new in the paper.
Formalizing it. The result is proved in the paper; no machine-checked version is known. The mission produces Lean definitions of the QCQP, its Shor relaxation, its projected epigraph and the lifted SOCP relaxation that are shared with the other missions of this series on the same paper, and a checked transfer from SDP to SOCP relaxations that downstream tightness results can use.
The argument is short on paper; the formal work is in the matrix bookkeeping. The inclusion needs a Schur complement for a block matrix whose top-left block is the scalar , in the block indexing , and the identity inside a trace of block products. The reverse inclusion needs an explicit lifted matrix, and its positive semidefiniteness is a global property of an matrix that the coordinatewise inequalities do not give entry by entry. The value identity is an identity of infima in the extended reals, where either side may be , so real arithmetic on the values is not available.
QCQP N m with symmetric , vectors , scalars and . Constraint is the paper's constraint , an inequality iff .EReal, so infeasibility gives and unboundedness . is , and in the SDP is symmetric.IsUnit U.Matrix.fromBlocks positive-semidefiniteness results), traces of block products, and EReal infima. A reusable lemma "" is welcome beyond this mission.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 by a positive semidefinite matrix . 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 with , 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.
Fix variables and constraints. For let with a symmetric matrix, and . The QCQP is
Its epigraph is . With and , the Shor relaxation imposes , for inequalities and for equalities; its projected epigraph is the set of for which some symmetric satisfies these constraints and . Always .
For write and , and let . Assumption 1 asks that (1) be feasible and that for some that is nonnegative on the inequality indices.
The quadratic eigenvalue multiplicity (Definition 3) is the largest integer such that and, for every , for some symmetric matrix . Here is block diagonal with copies of , and for , the vector has -th block . Every QCQP has multiplicity at least .
A supporting item (not a milestone) states the expansion used in the induction step: for with symmetric and unit , (p. 30).
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 exactly, so every linear objective in 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 and every quadratic form is a trace . The companion Theorem 8 (a separate mission of this series) relaxes to 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 (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.
The inclusion is immediate; the content is the reverse inclusion. A point of comes with a matrix , and the naive idea is to decompose into rank-one pieces and move along them. In 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 . The theorem therefore depends on the Kronecker structure and on the count 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.
All objects are defined locally in the namespace QCQPTightness.MultHull.
Fin N → ℝ; constraints are indexed by Fin m, the paper's constraint being index , and index is an inequality iff . The standing assumption (p. 1) is a hypothesis of the goal.EReal, so an empty or unbounded set never produces the junk value of a real infimum. "" is stated as for all .PosSemidef and PosDef; is convexHull ℝ in .Fin N by ; uses the same map.IsQuadEigMult k) exactly as Definition 3. The milestones are stated for an arbitrary explicit representation , which makes them at least as strong. Milestone 2 carries , which the paper notes always holds.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.
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.
A firm sells products . For product it chooses a price , a quality level and a service duration in a fixed interval of admissible durations. The parameters of product are:
A consumer buys product with the MNL probability
the in the denominator being the option to buy nothing. The markup of product is , and with the market size normalized to one the firm's total expected profit is
The firm solves problem (4): maximize over , and . In Lean the model is PriceQualityService.Joint.Model (attraction, choiceProb, markup, profit, and the exponent below as durationExponent).
Write . Theorem 1 asserts that problem (4) has an optimal solution with
where is the unique real solution of
and that equals the optimal profit. The goal also states the converse: every optimal solution has this quality and price structure, and, when , every optimal duration of a product with or is or .
The milestones follow the proof in Appendix B: the fixed-point form (15) of the profit; the price step (each markup is ); the price-only optimum (17); the quality step (18); the duration step (19); uniqueness of the root ; and Proposition 2, which says which endpoint is optimal for each product.
Theorem 1 reduces a -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 . 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 , the claim that 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.
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 , 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 : for the dependence on the duration is linear rather than quadratic, and when moreover every duration is optimal, so the "every optimum is extreme" clause has to exclude exactly that case.
Fin N, 0-based; the paper's product is index . Any is allowed; for the optimal profit is .Fin N.A formalization that fixes or identical products, fixes the sign of , states only first-order conditions, or defines 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 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.
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.
There are products . Product has a fixed price and quality , a quality sensitivity , a service utility per unit time , a unit production cost , and a service cost per unit time . Two service durations are available: a short one and a long one .
The dealer chooses two disjoint sets : products in are offered with service duration , products in with , and the others are not offered. A product offered with duration has attraction and markup . Under MNL demand with an outside option, product is bought with probability
and similarly with for (eq. (12)). The dealer's expected profit, with market size one, is
and problem (13) is to maximize over disjoint pairs .
Two orderings of products appear in the answer. The short-service markup is . The adjusted markup is
A markup-ordered assortment is a set of the products with the highest values of ; an adjusted markup-ordered set is a set of the products with the highest values of .
Assume , and for all . There are thresholds such that, with and ,
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 .
Problem (13) has feasible pairs. Theorem 5 reduces the search to at most pairs indexed by two thresholds, and it says which products deserve the long service: those with the highest adjusted margin , which charges each unit of service cost at the rate rather than at . 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.
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 and the short-service margin 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 is the breakpoint at which long and short service become equally profitable, and the three breakpoints must line up for the threshold structure to hold. This ordering uses : 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.
Fin N (0-based); is allowed. All parameters are arbitrary real vectors and real numbers; prices and qualities are fixed data, not decisions.Finset (Fin N) with Disjoint Sl Ss; optimality is a global inequality against every disjoint pair.max and elementary real analysis. Proofs of any milestone, and alternative routes to Theorem 5, are welcome.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.
There are two nests . Nest contains products , and every product of nest is sold with the same fixed service duration . Product of nest has parameters (quality sensitivity), (base service cost per unit time), (marginal effect of quality on service cost), (production-cost coefficient) and (service utility per unit time). The firm chooses a price and a quality for every product.
The total attractiveness of nest is . With upper-level scale parameter (the nest coefficient is ; the lower-level scale is normalized to ), a consumer chooses nest with probability
buys nothing with the remaining probability, and, having chosen nest , picks product with probability . The probability of buying product of nest is . The markup of a product is its price minus production cost minus service cost , and the firm's expected profit (market size one) is
The firm maximizes over all real price and quality vectors. When the model is the MNL model.
Let . The equation
has a unique real solution . With ,
and is the only maximizer.
The milestones follow the paper's proof in the Online Supplement:
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, : the optimal profit plus the reciprocal of the nest coefficient. A pricing problem with 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 -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.
The profit 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 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 , are only valid at the optimum and have to be carried out with that in mind. The exponent makes concave rather than linear in the nest attractiveness. This is the step where the MNL argument does not transfer verbatim.
Nest (s, l). Products of nest are Fin (m x), 0-based. Nests may be empty: an empty nest has , , and contributes nothing.Real.rpow of nonnegative sums of exponentials.The following versions are trivializing and are excluded: 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 in , and on an existence result for the maximizer.
Discrete-time linear iterations with entrywise nonnegative appear wherever a quantity is redistributed along the edges of a network: consensus and tracking protocols for multi-agent systems, positive switched systems, and Markov-type averaging schemes. Such an iteration converges to zero exactly when the spectral radius , the largest modulus of an eigenvalue, is less than one. For a sub-stochastic matrix (all row sums at most one) the classical bound settles marginal stability, and strict stability needs only one row of sum below one that "reaches" the others.
Shi, Zheng, Shao and Cheng (arXiv:2004.01867v2, SIAM J. Control Optim. 2021) study bipartite tracking over signed networks, where asynchronous updates and larger step sizes produce iteration matrices with some row sums above one. For these matrices the norm bound is useless: . Their §2.2 introduces super-stochastic matrices and gives conditions under which the spectral radius is nevertheless below one. These conditions are what the later sections use to allow larger control gains than a sub-stochastic analysis permits. This mission formalizes the main spectral result for a single super-stochastic matrix, Theorem 2.6, together with its companions Theorem 2.7 and Theorem 2.8 (products).
Let be a real matrix. Its -th row sum is , and its infinity norm is . The eigenvalues of are complex numbers, and is the largest of their moduli.
is super-stochastic (Definition 2.5) if for all and there is a set of rows with for and otherwise. The rows split into
A non-zero element chain from row to row is a list of entries , all non-zero, with consecutive indices distinct; is its number of elements. The theorem assumes one chain from some for each , and is the largest number of elements among these chains. The constants are
For a sequence , the product is ordered with later factors on the left, .
If and are non-empty, the chains exist, and
then
Theorem 2.6 is a stability criterion that applies when the standard norm test fails because some row sums exceed one. The criterion is computable: it needs only the row sums, the smallest positive entry and the lengths of paths in the directed graph of from rows of sum below one to the remaining rows. Theorem 2.8 extends this to products, which is the form needed for switched systems in which every subsystem may be individually unstable () while the periodic product is stable. The paper's tracking results for second-order and general linear agents (§§5–13) use these product bounds.
On the formal side, Mathlib has the spectrum of a matrix, Gershgorin's circle theorem and the norm on matrices, but no bounds on the spectral radius in terms of row sums along paths, and nothing on sub- or super-stochastic matrices. None of these results has a machine-checked proof. The mission produces the first formal version of these chain arguments and a reusable eigenvalue–norm inequality for real matrices.
The obvious argument — — fails at once, because . One has to pass to a power and show that every row sum of drops below one. For the rows of the drop comes only from the deficit of a row of , transported along a chain whose length varies from row to row; the bound must be made uniform in the length, which is where and the exponents enter, and where the growth factor competes with the gain . Formally, the induction mixes matrix powers, row sums of products and the indexing of chains. The final step needs the inequality between eigenvalues of , viewed over , and the infinity norm of a power of , which is not available in Mathlib in this form.
All statements live in the namespace SubSuperStoch.SuperSpec. Matrices are Matrix (Fin n) (Fin n) ℝ with -based indices. Row sums, the infinity norm (a supremum over Fin n, equal to when ), the complex spectrum, chains, super-stochasticity and ordered products are defined in one definitions file. Committed conventions:
A trivializing formalization is excluded: the hypotheses are satisfied by the paper's own example on p. 9 (, , , , radicand ), checked in Lean.
Contributions welcome: proofs of the milestones, the general eigenvalue–norm inequality (reusable for any spectral-radius argument over real matrices), and the two companion theorems.
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 and momentum they differ only by a gradient-correction term, yet NAG-SC is accelerated for every -strongly convex, -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 both methods converge to the same low-resolution ODE (Su, Boyd & Candès 2016 treat the convex analogue).
Shi, Du, Jordan & Su (2018/2021) keep the 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 .
Work in with the standard inner product and Euclidean norm . A function belongs to if , is differentiable and convex in the form , and for all . It belongs to if moreover and
and to if in addition is twice continuously differentiable with a Lipschitz-continuous Hessian. Write for the minimizer of .
Given a step size and an initial point , the high-resolution ODE of the heavy-ball method is
for . The initial velocity matches the first step of the discrete method. The paper's Lyapunov function is
For , every step size , and every ,
The result. Theorem 2 gives a linear rate for the heavy-ball ODE with an explicit constant, valid for every objective and every step size up to . Read next to Theorem 1 (rate , constant 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 term removed, and the two coincide at .
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 , a differential inequality, a Grönwall-type integration, and a closed-form estimate of from the initial conditions and -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.
The algebra is short; the formal difficulty is analytic. The derivative of must be obtained by the chain rule from a one-sided derivative of at and 's differentiability, and the derivative of the two squared norms from those of and . Passing from Lemma 3.2 to is a comparison argument for a function known only to have one-sided derivatives on ; the naive route through requires a monotonicity theorem for functions with derivatives within a half-line. Finally, the estimate of needs and , both consequences of -smoothness and that must be derived from the class definition, and the constant needs a one-variable inequality in .
is EuclideanSpace ℝ (Fin n), is Mathlib's gradient, and is fderiv ℝ (gradient f) x. The classes , , are structures carrying the paper's first-order inequalities (§1.4, p. 8), with ; the Lipschitz constant of the Hessian is existential, as the paper fixes none. The minimizer is a point with for all .
A solution of (1.10) is a pair of curves with , , the derivative of and the derivative of at every , both taken within ; values for 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 or 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 with the printed constant ; it does not assume any decay of , and an ODE predicate in which is not the derivative of 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 " within implies " and the -smoothness estimates around a minimizer are reusable well beyond this mission.
Nesterov's accelerated gradient method minimises a smooth convex function to accuracy in gradient evaluations, and a -strongly convex one in ; 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 , an auxiliary variable and a scaling parameter whose Lyapunov function decays exponentially for every . 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 and at once. This mission formalises that analysis, Theorem 6.1.
Let be a real Hilbert space with inner product and norm . A function with gradient map belongs to () if it is continuously differentiable and -convex,
and to if moreover is -Lipschitz, with . A point minimises globally.
Algorithm 1 (Nesterov accelerated gradient method) takes and . For it computes the positive root of , sets and
chooses any with the sufficient decrease (for instance the gradient step ), and sets
The Lyapunov function is
and (89).
For , every run of Algorithm 1 has and
All four conclusions are part of the goal: (98) alone does not carry a rate.
A companion item states (103) of Remark 6.3 for Algorithm 1: with , , , .
Theorem 6.1 recovers, by a Lyapunov argument, the optimal rates of Nesterov's method in both regimes: for convex and for strongly convex once , with the parameter moving between them automatically. It covers every sufficient-decrease choice of , 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 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 , and no machine-checked proof of Theorem 6.1 or Lemma B.1 is known. A formalisation checks the omitted step, pins down where is used, and adds a discrete Lyapunov toolkit for accelerated methods in Hilbert space.
Reading Algorithm 1 directly gives a three-sequence recursion with no visible monotone quantity: itself need not decrease. The contraction (98) holds only for the specific combination (74), and only after the cross terms in produced by the -update are matched exactly against the sufficient-decrease step; any slack in the step rule leaves a positive gradient term. A second difficulty is uniformity in : when the linear factor equals , so the rate must come from a separate estimate of in terms of the step sizes, which are defined only implicitly by a quadratic equation.
NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace); the paper's duality pairing and dual norm are the inner product and the norm (Riesz identification).gradf : V → V with HasGradientAt f (gradf x) x at every point; Mathlib's gradient is not used.IsS1 and IsS11; includes and , and the upper bound (4) is a consequence, not an assumption.IsNAGRun of hypotheses on given sequences, one per step. Step 2 records only (the page writes , but occurs when , and 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.A statement that assumes the contraction (98) for arbitrary sequences, or fixes 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.
The alternating direction method of multipliers (ADMM) solves linearly constrained problems
by alternating a minimization in , a minimization in 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 or (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 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 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 was noted earlier by Bauschke and Koch (2015, Rem. 3.14) for , 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.
All spaces are Euclidean, , , , . A function is proper if it never takes the value and is finite somewhere. The proximal mapping of with stepsize is the set
For and a linear map , the image function is
The -augmented Lagrangian of (1.2) is . One ADMM update with penalty and relaxation maps to :
One DRS step with stepsize and relaxation on maps to , where and . The reformulation of (1.2) is
that is, and . The regular subdifferential is , the limiting one .
Let be proper, large enough that every ADMM subproblem has a solution, and . With , , and the same expressions at , and ,
together with , , , and .
Proposition 5.2(i)–(iii) (properness of , , ), Proposition 5.3 (), the inclusions (5.3a) and (5.3b), and the identity .
Theorem 5.5(vi): if is surjective, is -smooth and , then . Theorem 5.6: under Assumption II and in the ranges of Theorem 4.1 with , decreases by per step, , cluster points are KKT points with common cost, and the iterates are bounded when is level bounded.
Theorem 5.5 reduces nonconvex ADMM to nonconvex DRS: any descent, convergence or rate statement for DRS on 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 permitted by Theorem 4.1, under assumptions weaker than earlier nonconvex ADMM analyses (Li and Pong, 2015, doi:10.1137/140998135, require 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.
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 is proper and that the infimum is attained at 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 , and 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 -subproblem, whose quadratic term couples with the residual. Theorem 5.6 additionally rests on the whole DRS convergence analysis of §4.
Points are EuclideanSpace ℝ (Fin _), matrices are continuous linear maps, is ContinuousLinearMap.adjoint, and is the operator norm. Extended-real functions are EReal-valued; the image function imageFn is the EReal infimum over , so it is off the range and may be . Proximal mappings and are sets, and an ADMM update (IsADMMStep) is any selection of minimizers in the order . The two subproblems minimize the terms of that depend on the minimized variable, because the dropped constant may be at a starting point and would make every a minimizer. "Large enough penalty" is SubproblemsSolvable. The regular and limiting subdifferentials are the published IsRegularSubgrad and LimitingSubdiff.
Added hypotheses: and proper in Theorem 5.5 and 5.5(vi), and proper in Proposition 5.2(i). The page omits them, and they are necessary: for every is the whole space while is not proper. Claim (v) is stated as the existence of with , which is stronger than the distance bound and avoids the distance to an empty set. Theorem 5.6 uses the constants 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 , and both are then false (counterexamples in the companion mission on DRS convergence). Theorem 5.6 adds ; its run is indexed so that the paper's is the term , with the starting triple at index .
The goal does not assume the DRS relations or (5.3a)–(5.3b), and 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 , 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.
Nesterov's accelerated gradient method minimises a smooth convex function to accuracy in gradient evaluations, and a -strongly convex one in , which is optimal for first-order methods. The method's original derivation by estimate sequences gives little insight into why it accelerates. Since Su, Boyd and Candès (arXiv:1503.01243) a large literature reads accelerated methods as discretisations of second-order ordinary differential equations and proves their rates with Lyapunov functions transported from the continuous to the discrete setting.
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 variable , a velocity-like variable and a scaling parameter , whose Lyapunov function decays exponentially for every . They then show that standard ODE-solver constructions applied to this flow (implicit Euler, Gauss–Seidel splitting, predictor–corrector, gradient correction) produce explicit methods with accelerated rates, and that Nesterov's method is one of them. This mission formalises the paper's analysis of the predictor–corrector scheme of §5.2, its first explicit accelerated method.
Let be a real Hilbert space with inner product and norm . A function with gradient map belongs to (with ) if it is continuously differentiable and -convex:
It belongs to if moreover is -Lipschitz with . The value (plain convexity) is allowed throughout. A point minimises globally.
The method keeps two iterates , a step size and a parameter that evolves by the implicit parameter equation
The predictor–corrector scheme computes a predictor , then , then the corrector :
Every line is linear in the unknown, so one step costs one gradient evaluation. The Lyapunov function is
The Gauss–Seidel step (80) is the scheme without the predictor: and the -update evaluated at .
If and the step sizes satisfy , then every run of (83) with (73) satisfies
with . All three conclusions are part of the goal; (86) alone would not carry the rate.
Theorem 5.1 gives a single explicit method, with one gradient call per step and no restart, whose rate is when and when and ; the parameter interpolates between the two regimes automatically. Both rates are the optimal ones for first-order methods. The same Lyapunov argument, with Lemma B.2 as its rate engine, is reused in the paper for the gradient-corrected scheme (Theorem 5.2), Nesterov's method (Theorem 6.1) and the composite methods of §7, so the milestones of this mission are the shared core of the series.
The result is proved in the paper, with the proof of Lemma B.2 omitted as similar to that of Lemma B.1. No machine-checked proof of Theorem 5.1, Lemma 5.1 or Lemma B.2 is known. A formalisation checks the omitted proof, fixes the exact hypotheses of each step (which estimate needs only -convexity and which needs the Lipschitz gradient), and supplies a reusable discrete Lyapunov toolkit for accelerated methods in Hilbert space.
The obvious approach, imitating the continuous argument with the Gauss–Seidel splitting (80), fails: Lemma 5.1 leaves the cross term , which has no sign, and bounding it by Cauchy–Schwarz as in (82) produces a positive gradient term that destroys the contraction. The predictor–corrector scheme is designed so that this cross term cancels exactly against the descent inequality for between and , and the remaining square vanishes only under the precise step rule . Turning the contraction into the rates (87)–(88) requires lower bounds on that hold uniformly in , which is the content of Lemma B.2. When the linear-rate bound is vacuous, so the rate must come from a separate estimate.
NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace); the paper's duality pairing and dual norm are the inner product and the norm, by the Riesz identification.gradf : V → V with HasGradientAt f (gradf x) x at every point; Mathlib's gradient, which is at non-differentiable points, is not used.IsS1 and IsS11. The class includes and ; the upper quadratic bound (4) is a consequence, not an assumption.A statement that assumed and derived only the rates, or that quantified over arbitrary sequences rather than runs of (83), would be Lemma B.2's corollary and not Theorem 5.1; the goal quantifies over runs of the scheme.
The development needs elementary Hilbert-space identities, the descent inequality (4) for functions with Lipschitz gradient, and real-sequence estimates for products and square roots. The same definitions and Lemma B.2 recur in the series' missions on Theorems 5.2, 7.2 and 7.3. Proofs of any milestone, and of (4) as an auxiliary lemma, are welcome.
Accelerated first-order methods, beginning with Nesterov's 1983 scheme, reach the optimal iteration complexity among gradient methods for smooth convex minimization, but their classical derivations ("estimate sequences") give little insight into why acceleration works. A line of work started by Su, Boyd and Candès (arXiv:1503.01243) reads accelerated methods as discretizations of second-order ordinary differential equations and proves their rates with Lyapunov functions: a quantity that decreases along the continuous trajectory and, after discretization, along the iterates.
Luo and Chen (arXiv:1909.03145, Math. Program. 2022) introduce the NAG flow, a first-order system in two variables with a time-varying parameter , and derive several accelerated methods from it as numerical ODE solvers. Their §4 treats the simplest discretization, the fully implicit (backward Euler) scheme. It is not a practical method by itself, since each step solves a nonlinear equation, but it is the case in which the continuous Lyapunov argument transfers to the discrete level almost word for word, and it is the benchmark for the semi-implicit and explicit schemes of §§5–7. This mission formalizes its convergence theorem, Theorem 4.1.
Let be a real Hilbert space with inner product and norm ; the duality pairing is identified with the inner product. Let and . The function belongs to the class if it is continuously differentiable with gradient and satisfies the -convexity inequality
For this is convexity, for strong convexity. A global minimiser of is fixed throughout.
Given positive step sizes and , the implicit scheme (72)–(73) relates consecutive iterates and by
All right-hand sides are evaluated at the new iterate, which is what makes the scheme implicit. The Lyapunov function (74) is
For with and every run of (72)–(73) with and ,
No condition links to or to any smoothness constant, and need not have a Lipschitz gradient.
A companion item states (76): each step of (72) is a proximal point step with explicit , and .
Theorem 4.1 gives a linear rate for every convex , not only strongly convex ones, as long as ; larger steps give faster decay. It is the exact discrete counterpart of the exponential decay of the NAG flow (Lemma 3.2 of the paper), and the semi-implicit and explicit schemes of §§5–7 are analysed by comparison with it: their proofs follow the same difference computation and must control the extra terms that the implicit scheme does not produce. Through (76), the implicit scheme is an extrapolated proximal point method, close to Güler's accelerated proximal point algorithm when .
The result is proved on paper. To the knowledge of this mission it has no machine-checked proof. Formalizing it fixes the exact hypotheses of the discrete Lyapunov argument (in particular that and are what make the dropped squares nonpositive) and provides the algebraic identities reused by the later schemes of the paper.
The argument is algebraic, but the bookkeeping is where it can fail. The difference produces terms in , , , and , which must cancel or carry the right sign exactly. The naive attempt, to bound by as in an explicit Euler analysis, fails: the implicit scheme controls the decrease by the new value , and the contraction factor comes from solving for it. The -terms close only because (73) is also discretized implicitly, so that , not , multiplies .
is a type with NormedAddCommGroup, InnerProductSpace ℝ V and CompleteSpace V. The gradient is an explicit map gradf : V → V with HasGradientAt f (gradf x) x at every point, and continuity of gradf encodes "continuously differentiable". The class , the Lyapunov function, one step of (72)–(73), and a run are definitions; the scheme's equations are kept in the page's difference-quotient form, as hypotheses on given sequences. Nothing asserts that the implicit system has a solution, and iterates are not defined by choice. Sequences are indexed from .
Conventions committed to: is a global minimiser (the paper's standing assumption that is nonempty); and as on p. 16; the one-step milestones that divide by assume , which along a run follows from (73). The prox in (76) is stated as membership in the argmin through the published predicate GoldenRatioVI.Shared.IsProxPoint.
A trivializing formalization is ruled out: the goal is stated for sequences satisfying the scheme (72)–(73) itself, never for sequences assumed to satisfy (75), and no Lipschitz-gradient class or step-size rule from later sections is imported.
The definitions of and are shared with the other missions of this series and will be consolidated. Contributions welcome: proofs of the identities, of (75), of the goal, and of (76).