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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. A high-probability approximation guarantee is a separate claim requiring an explicit probability bound. The optimum includes entangled states. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
Most practical reinforcement-learning methods do not compute value functions exactly. They alternate between estimating a value function from data, usually with a parametric approximator, and acting greedily with respect to that estimate. Approximate value iteration and approximate policy iteration are the two classical schemes of this kind, and their error analysis decides how accuracy in the estimation step translates into quality of the policies produced. Chapter 3 of S. M. Kakade's thesis On the Sample Complexity of Reinforcement Learning (University College London, 2003) collects the basic guarantees, developed from Bertsekas (Dynamic Programming: Deterministic and Stochastic Models, 1987) for greedy policies, Singh and Yee (1994), and Bertsekas and Tsitsiklis, Neuro-Dynamic Programming (Athena Scientific, 1996). The bounds are stated in terms of the worst-case (max-norm) error of the evaluation step, and the thesis uses them to argue that max-norm error is the obstacle to state-space-independent sample complexity results for these methods, which motivates the later chapters of the thesis.
A finite discounted Markov decision process consists of a finite set of states , a finite nonempty set of actions , a transition kernel (for every a probability distribution over ), a deterministic reward , and a discount factor . A policy is a probability distribution over actions for every state; a deterministic policy is a map , identified with the policy that plays with probability one.
Values are normalized: the value of at is
and the state-action value is . With rewards in , every value lies in . An optimal policy has for every policy and state ; write and . The max norm is on state vectors and on state-action arrays.
The backup operator is . A deterministic policy is greedy with respect to if for every .
The policies need not converge; the statement bounds where they end up.
The results give the standard performance guarantee for greedy approximate dynamic programming: an evaluation error of in max norm costs at most in max-norm suboptimality, uniformly over the asymptotic set of policies, with a geometric rate of approach. Example 3.1.2 of the thesis shows that the factor of Theorem 3.1.1 is attained, so the greedy step itself cannot be improved; the two factors of the horizon in the limit bound are the reason the thesis turns to other error measures in later chapters.
All the statements are classical and proved in the literature (Bertsekas–Tsitsiklis 1996, Chapter 6, in the unnormalized model and with a factor to spare in the limit bounds); Lemma 3.2.3 and Theorem 3.2.2 are stated in the thesis without proof. To our knowledge none has a machine-checked proof. The mission produces formal proofs in the normalized model shared with the formalization of Kakade–Langford (2002) on this platform, so later chapters of the series (conservative policy iteration, policy search) can compare against them.
Approximate policy iteration is not monotone: with evaluation errors, can be worse than at some states, so the argument of exact policy iteration, which uses everywhere, does not apply. The difficulty of Lemma 3.2.3 is to control the distance to optimality without improvement at each step, combining the greedy step with the lack of monotonicity of the new policy's value; the thesis calls the proof of Theorem 3.2.2 "somewhat technical" and omits it. A second, mechanical difficulty is that the normalized value is defined as an infinite series, so its Bellman equation , the optimality equation and the bound have to be derived from that definition before any of the recursions can be run.
ApproxOptRL.Shared.Model: value P r γ π is (defined as times a tsum), qValue is . and are finite types, nonempty; satisfies IsTransitionKernel; every statement assumes and .IsOptimalPolicy P r γ πstar (a stationary stochastic policy dominating every stationary stochastic policy at every state). Such a policy exists for every finite MDP (p. 26 of the thesis), and for finite MDPs it is optimal among all policies.S → A, and are evaluated through the indicator policy detPolicy. "Greedy" is the relation ∀ s a, Q s a ≤ Q s (f s): every tie-breaking rule is covered.ℕ, with the greedy and accuracy conditions as hypotheses at every index; the value-iteration condition is written for indices and .S → ℝ and S → A → ℝ.value for indicator policies, , monotonicity and contraction of policy-evaluation and backup operators in the normalized model, and the bound . Contributions of these lemmas are welcome.Two-stage stochastic linear programming chooses a first-stage decision before a random parameter is revealed and pays an optimal second-stage (recourse) cost afterwards. The classical model fixes the distribution of the random parameter. In practice it is rarely known beyond a few moments, and a decision maker who is averse to risk does not evaluate the recourse cost by its plain expectation. Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) take both points seriously: the distribution is only known to belong to the class of all distributions with given mean and second-moment matrix, the cost is passed through a convex piecewise-linear disutility, and the decision is evaluated against the worst distribution in the class.
Moment-based worst-case bounds go back to Scarf's newsvendor and to the Chebyshev-type bounds of the moment problem (Isii 1962; Bertsimas and Popescu 2005). Delage and Ye (Oper. Res. 58(3), 2010) showed that a broad class of such minimax problems is solvable in polynomial time by the ellipsoid method. For the case in which the uncertainty sits in the objective of the second-stage linear program, this paper gives a single semidefinite program (its Theorem 2.1, the subject of a companion mission) and, in §2.2, identifies the distributions that come arbitrarily close to the worst case. This mission is about the second result.
The first-stage region is . For the recourse set is and the second-stage cost of an objective vector is
The disutility is with . The moment class consists of the distributions of a random vector with and . The worst-case value at is
Its dual (6) is
with symmetric and . Its semidefinite reformulation (8) has the dual (9):
Its variables are scaled conditional moments: is the probability that the th piece of is active, and , are the first and second moments of on that event, multiplied by .
The standing assumptions are Assumption 3, for every , so that is finite, and Assumption 4, . Recourse sets are assumed nonempty.
For every there is a sequence with , and
where all three are finite optimal values: a supremum over a nonempty bounded-above set, an infimum over a nonempty bounded-below set, and a supremum over a nonempty bounded-above set.
Theorem 2.2 says that the semidefinite bound is tight and that the worst case is approached by explicit mixtures. With probability the cost vector sits at the conditional mean , and with a small probability it is perturbed by a large Gaussian. The construction tells which scenarios a minimax solution guards against. The paper's numerical section uses it to stress-test solutions computed under other distributional assumptions. For the risk-neutral case () the bound collapses to Jensen's bound . For it is a combination of Jensen bounds, one per piece of the disutility.
Theorem 2.2 is proved in the paper; no part of it, nor the strong duality of the moment problem that it relies on, is formalized on the platform or, to our knowledge, elsewhere. The mission asks for machine-checked proofs of the identity and of the steps of the extremal construction. Several of these are reusable beyond this paper: weak and strong duality of moment problems, the existence of optimal solutions of moment-type semidefinite programs, and Jensen's inequality for the value function of a linear program.
Most of the argument is linear programming and bookkeeping. The step is a strong-duality theorem for an infinite-dimensional linear program over measures. The paper cites it from Isii's theory of the moment problem, and none of that theory exists in Mathlib. The construction of near-extremal distributions also needs care. A single distribution in generally cannot attain , so the bound is reached only along a family whose second moments are matched by rare, large perturbations. Lemma 2.1 needs measurable selections of an active piece of and of a dual optimal solution of the second-stage program as functions of . When the optimal solution of (9) has zero-weight blocks, the mixture is undefined until the solution is first rearranged.
Vectors are Fin d → ℝ, matrices Matrix (Fin r) (Fin d) ℝ, and distributions are probability measures on Fin d → ℝ with square-integrable coordinates. They are not densities as in the paper's (5). The moment class uses the published MomentDRO.Conf definitions, and is the uncentred second moment. The paper writes both for the dimension of and for dual vectors. Here the dimension is and dual vectors are named π. Indices are zero-based. Bordered matrices are Matrix.fromBlocks on Fin d ⊕ Fin 1 and is Matrix.PosSemidef. is a real infimum and the optimal values are real sSup/sInf of value sets. Every statement that uses an optimal value also asserts IsLUB/IsGLB, so junk values cannot make a statement true.
As printed, Assumption 2 (complete recourse) and Assumption 3 for all contradict each other whenever has a row. The formalization keeps Assumption 3 for all and replaces complete recourse by nonemptiness of , which is what §2's proofs use. Assumption 1 is not used and is omitted. The hypotheses are jointly satisfiable, for example by , , , and .
The sequence clause of Theorem 2.2 alone holds for every finite supremum, so it does not capture the theorem. The goal therefore also asserts the equalities , with all three values genuine, and these carry the content. A formalization that drops them, or states them only through junk values, is ruled out.
A complete development needs the duality theory of the moment problem, Jensen's inequality for concave functions on , compactness arguments for semidefinite feasible sets, and multivariate Gaussian mixtures (ProbabilityTheory.multivariateGaussian in Mathlib). Proofs of individual milestones are welcome. So is a general moment-problem duality theorem from which strong_duality follows.
Zara ships inventory from a central warehouse to each of its stores every week, and for a short-lived fashion item the warehouse holds a limited amount of each size. Deciding how many units of each size to ship to each store is therefore a constrained allocation problem whose objective is the expected sales a store will realize from a given inventory. Caro and Gallien (working paper, 2007; published in Operations Research, 2010) built such a model, embedded it in a weekly shipment optimization, and tested it in a field experiment in Zara's store network. The store-level sales model has one unusual feature, taken from Zara's practice: as soon as one of the major sizes of an item runs out, the whole item is removed from display, so stock-outs of different sizes interact.
The expected sales under that policy have no closed form usable inside a mixed integer program. The paper replaces them by an explicit piecewise-linear function and asserts that this replacement is an upper bound. This mission formalizes that claim, the chain of identities and inequalities that lead to it, and the paper's statement that its shipment program represents the approximation exactly.
A reference is offered in a finite set of sizes , with major sizes and minor sizes . Sale opportunities for size follow a Poisson process with rate , independent across sizes, where is the time since the last replenishment and is the time between replenishments.
Given an inventory vector , the virtual stockout time of size is , and for a set of sizes . Writing , the number of sales in one period is
since every size stops selling when the first major size runs out, and a minor size also stops when it runs out itself. The expected sales function is .
For the approximation, let be the lower incomplete Gamma function, and define the tangent coefficients
with the tangent at equal to the constant . For each size choose a nonempty finite set of tangent indices. The approximate expected sales function is
with . In Lean the objects are expectedSales, hA (), a, b, tangent and gTilde in the namespace FastFashion.Approx.
For every independent Poisson family with positive rates, every , every nonempty , every choice of nonempty finite tangent sets, and every ,
The statement fixes no tangent set, so it covers the paper's numerical choice (7) and every refinement of it.
In the shipment program (MIP) (13)–(19) of §3.2, with positive prices, every optimal solution has at every store .
The upper bound is what makes the paper's optimization coherent: the MIP maximizes , and the bound guarantees that this objective never underestimates the expected revenue of a shipment plan, with an error controlled by the number of tangents. Identity (6) exhibits as a concave function of with explicit Erlang-type slopes; (2) is a standard optional-sampling identity for compensated Poisson processes stopped at a bounded stopping time; and the MIP statement is the step that turns a minimum of affine functions into linear constraints.
The paper proves none of these in detail: (2), (4) and (5) are justified by a reference to the optional sampling theorem, (6) by a sentence on discrete concavity, and the upper bound and the MIP claim by one sentence each. None of the statements has a machine-checked proof. A formalization produces a checked chain from the Poisson model to the deterministic program, fixes the indexing error in the printed coefficients of (6), and isolates the exact hypotheses (nonempty major sizes, nonempty tangent sets, positive prices) under which the claims hold.
The deterministic parts — (3) given pathwise monotonicity, the envelope inequality given concavity, and the MIP argument — are short. The probabilistic identities are not. Equation (2) needs the optional sampling theorem for the compensated process in continuous time, applied at (the paper cites Karatzas and Shreve 1991), which requires showing that is a stopping time for the joint filtration of the family and that is still a martingale with respect to that larger filtration; this is where independence across sizes enters. Equation (4) needs the distribution of , the -th arrival time, which is Erlang; the statement in the model is about first hitting times of a counting process, not about sums of exponential inter-arrival times, so the link between the two descriptions has to be built. Equation (5) needs the identity between Poisson tails and the incomplete Gamma function.
A tempting shortcut is to define directly by formula (2), or by formula (4); both make the corresponding milestones definitional and the goal a statement about formulas rather than about sales. The formalization defines from and from the stopping times.
Finset and the minor sizes its complement. The demand is a structure IsPoissonFamily λ N P: each is a counting process with , non-decreasing right-continuous paths with unit jumps, Poisson increments of mean , independent increments, and the processes are independent across sizes. is a probability measure.WithTop ℝ), so the infimum of an empty set is , never ; is a real number in .The paper's further remark that inherits the qualitative properties of Proposition 1, and the multicolor extension of Appendix §5.2, are not included. Contributions of general infrastructure are welcome: optional sampling for continuous-time counting processes, Erlang hitting-time laws for Poisson processes, and the Poisson-tail/incomplete-Gamma identity are all reusable well beyond this mission.
A large control system is often built from many subsystems , each of which is input-to-state stable (ISS) with respect to the states of the others. Whether the interconnection is again ISS is decided by a small gain condition on the matrix of interconnection gains. For two subsystems this goes back to Jiang, Teel and Praly (1994) and to the Lyapunov version of Jiang, Mareels and Wang (1996). For subsystems, Dashkovskiy, Rüffer and Wirth formulated the condition as a property of a monotone operator on (2007). Rüffer's thesis (2007) and the paper on which this mission is based (arXiv:0901.1842, SIAM J. Control Optim. 2010) turned it into a Lyapunov construction.
The construction needs a geometric object: a path in the positive orthant, unbounded in every coordinate, along which the gain operator strictly decreases every component. For a linear gain matrix this is a Perron vector. For nonlinear gains, its existence is the first of the paper's two main results (Theorem 5.2). This mission formalizes that theorem and the lemmas of §8 that prove it. The companion mission formalizes the second main result, the Lyapunov function built from such a path.
Write . Vectors in are compared componentwise: means for all , and means for all . A function is of class if it is continuous, strictly increasing and , and of class if it is moreover unbounded.
A gain matrix is with and . A monotone aggregation function (MAF) is a continuous with for , whenever , and as . Typical examples are sums and maxima. Given MAFs , the gain operator is
The paper assumes from p. 8 on that , restricted to the coordinates of the nonzero entries of row , still has the strict monotonicity (Remark 2.6). The small gain condition (SGC) is : for every , at least one component of is strictly smaller than the corresponding component of . The set
collects the points that every component of strictly decreases.
An -path (Definition 5.1) is a continuous with every component such that (i) each is locally Lipschitz on ; (ii) on every compact the derivatives of all , where they exist, lie in for constants depending on only; and (iii) for all .
Let be a gain matrix and a compatible vector of MAFs. Assume one of: (i) is linear with spectral radius less than one; (ii) is irreducible and ; (iii) and ; (iv) the entries of are bounded and . Then
In cases (i)–(iii) the entries are in , and in case (iv) they are in .
The milestones follow §8 in the order the proof uses them.
An -path turns a small gain condition into a Lyapunov function. If each is an ISS Lyapunov function of , then is one for the network (Theorem 5.3). So Theorem 5.2 is the step that makes the small gain condition a certificate of network stability, and the corollaries of §5–§7 (sums, maxima, neural networks) all pass through it.
The results are published and proved on paper. None is machine-checked: no proof assistant library contains MAFs, gain operators, the sets and , or -paths. The paper cites three ingredients without proof: Lemma 8.6, Proposition 8.9 and the scaling step of Theorem 8.11. It also gives Theorem 8.14 only as a sketch. Formalizing them closes those gaps in one place.
For bounded gains the problem is easy: far out, every point of a large ray lies in , and the only work is the descent to the origin. With entries, is unbounded and no ray need stay in . Following the image of a single point fails, because forward iterates go to , not to infinity. The paper instead uses backward orbits inside . That this set is nonempty and unbounded is a fixed-point argument of Knaster–Kuratowski–Mazurkiewicz type (Propositions 8.9 and 8.10), not a monotonicity argument. A second obstacle is strictness. A backward orbit is only -increasing, while Definition 5.1 needs strictly increasing components with derivative bounds. This is where the diagonal scalings of Lemmas 8.6–8.7 enter.
is ℝ≥0 and is Fin n → ℝ≥0, with subsystems indexed from . The strict order is a named predicate (SLt), never Lean's < on functions, which means " and ". The small gain condition is ∀ s ≠ 0, ¬ s ≤ T s. The inverses are carried as explicit two-sided inverses, and derivatives are ordinary real derivatives at points where they exist. Compatibility (Remark 2.6) and are hypotheses of every statement about . Irreducibility is the matrix-power form of p. 12, which Mathlib's Matrix.isIrreducible_iff_exists_pow_pos connects to Matrix.IsIrreducible. The spectral-radius hypothesis says that every complex eigenvalue has modulus . The 1-norm defines .
Hypotheses made explicit or corrected:
A path with , or with Lean's < on functions, is not an -path. Such a reading would make the goal follow from the origin alone, and it is ruled out.
Needed infrastructure: comparison-function calculus (inverses and compositions of functions), piecewise linear interpolation in with Lipschitz inverse bounds, and a KKM-type argument on the simplex. The first two are reusable well beyond this mission. Contributions of any milestone, proofs of the cited ingredients (Lemma 8.6, Proposition 8.9, Proposition 8.10, the scaling step of Theorem 8.11) and a full proof of Theorem 8.14 are welcome.
A central question of the theory of learning in games is whether simple adaptive behavior leads players to a Nash equilibrium. Many natural dynamics — fictitious play, best-reply dynamics, replicator dynamics — fail to converge in some games, and the failures are usually exhibited one dynamic at a time. Hart and Mas-Colell (AER 2003) asked a structural question instead: is there any continuous-time dynamic, satisfying one informational restriction, that converges to Nash equilibrium for all games in a reasonable family? The restriction is uncoupledness: each player's adjustment may depend on the current strategy profile and on that player's own payoff function, but not on the payoff functions of the others. This is the situation of players who do not know the opponents' preferences.
Their answer is negative, and the paper proves it with two examples. This mission formalizes the second, built on a three-player game introduced by James Jordan (GEB 1993) in his study of learning mixed-strategy equilibria. A companion mission formalizes the first example, a two-player game on the unit disk.
Three players each choose between two pure strategies, and . A game is identified with its payoff functions , . A state is a mixed profile , where is the probability that player plays (top row, left column, left matrix). Payoffs extend to by expectation over independent randomizations, and is a Nash equilibrium when no player can raise its expected payoff by changing its own coordinate.
Jordan's family consists of the games
indices modulo 3, with parameters close to : each player wants to mismatch the next player. Jordan's game is the member with all ; every game of has a unique Nash equilibrium , and .
A dynamic for a family is a vector field on , one for each . It is uncoupled if whenever give player the same payoff function. When every game of has a single Nash equilibrium , is Nash-convergent for if, for every , is a rest point, every solution converges to it, is , and the Jacobian of at is hyperbolic and stable: all its eigenvalues have negative real parts.
Let have the single-Nash-equilibrium property and contain every game of that is close to . Then
Two further items record the paper's observations: uncoupledness forces , and such a matrix has an eigenvalue with positive real part when and spectrum otherwise. A last item shows that the coupled dynamic is Nash-convergent.
The theorem says that convergence to Nash equilibrium is not a property that adaptive dynamics can deliver on informational grounds alone: as soon as a family contains the games near , any rule in which players respond only to their own payoffs fails for some game, even though every game in the family has a unique equilibrium and a coupled rule converges for all of them. The finite example matters because it shows that the obstruction is not an artifact of continuum strategy spaces: it occurs in a game in mixed strategies. The paper contrasts it (§IV) with the existence of uncoupled dynamics that converge to correlated equilibria: Nash equilibrium cannot be reached in an uncoupled way, while correlated equilibrium, a notion based on coordination, can. Follow-up work extends the impossibility to stochastic uncoupled dynamics (Hart and Mas-Colell, GEB 2006) and surveys the area (Hart, Econometrica 2005).
The result has been proved since 2003; no machine-checked proof of it is known. A formal proof requires an equilibrium computation in a parametric family of finite games, a careful treatment of the derivative of a vector field defined only on a cube, and a spectral fact about real matrices. The definitions of uncoupled and Nash-convergent dynamics written here are reusable for other impossibility results of the same kind.
The obvious attempt is to analyze a particular dynamic and show that it cycles around . That proves nothing about other dynamics: the statement quantifies over every uncoupled , so the argument must extract a constraint on from uncoupledness alone. Uncoupledness only relates the dynamic at different games through single coordinates of , and Nash-convergence only constrains at the equilibria of the games in ; neither says anything directly about the Jacobian at . Formally, the delicate steps are the uniqueness of the equilibrium for all nearby parameters, which requires excluding pure and partially mixed equilibria, and the passage from vanishing along a segment to a vanishing partial derivative.
Players are indexed in Lean (the page's player is index ), strategies are Fin 2, and a game is Fin 3 → (Fin 3 → Fin 2) → ℝ. The state space is ; a dynamic is any map , whose values outside never matter. Committed conventions:
FatkhullinPolyak.Discrete.IsHurwitz), and convergence of every solution. The Jacobian is the derivative within .The family cannot be vacuous: Jordan's games with satisfy both hypotheses, and the coupled-dynamic item certifies that Nash-convergence itself can be met, so the goal's force rests on uncoupledness. Contributions welcome include the equilibrium computation for , the spectral lemmas (which are independent of game theory), and the calculus step from vanishing along a segment to a vanishing partial derivative within a cube.
Regev's paper (J. ACM 56(6), Article 34, 2009) introduces the learning with errors (LWE) problem and shows that solving it is at least as hard, for quantum algorithms, as approximating standard worst-case lattice problems such as the shortest independent vectors problem (SIVP) and GapSVP. LWE is the basis of most lattice-based public-key cryptography, including the post-quantum schemes standardized since.
The reduction runs through a sampling problem: produce samples of the discrete Gaussian distribution on a lattice . The last step converts such a sampler into a solver for SIVP, which asks for short linearly independent lattice vectors. That conversion rests on one geometric fact about , Lemma 3.15 of the paper (p. 34:31): when the width is at least times the smoothing parameter of , a sample is not trapped in any proper subspace. The lemma first appeared, with only a proof sketch, in the preliminary version of Micciancio and Regev's work on worst-case to average-case reductions (SIAM J. Comput. 2007); Regev's article gives the full proof. This mission formalizes that lemma. The paper's main theorem, a quantum reduction (Theorem 3.1), is outside this series.
Work in , , with the Euclidean inner product and norm .
For an -dimensional lattice , , and every subspace with ,
The constants , and are the printed ones.
The result. Lemma 3.15 gives Corollary 3.16: independent samples of contain linearly independent vectors except with exponentially small probability. Since samples of have norm at most about with high probability, a sampler at width therefore yields short independent vectors, which is how Regev's reduction reaches SIVP (§3.3). The same property is used in later work wherever discrete Gaussian samples must generate a full-rank set of lattice vectors.
Formalizing it. The lemma is proved in the paper; it has no machine-checked proof that we know of. The work this mission asks for is the formalization of the known proof: the Gaussian-sum analysis of a discrete Gaussian on a general lattice in Mathlib's ZLattice framework, built on the platform's proved Poisson summation formula for lattices. The remark after Definition 2.10 (well-definedness of the smoothing parameter) and the normalization bound are used across the whole paper (Lemmas 3.2, 3.12, Claims 3.8, 3.9) and are reusable beyond this mission.
The obvious argument fails at the first step: there is no direct way to bound the mass of on a hyperplane, because a lattice can place many short vectors in one hyperplane and the normalization is not known in closed form. The paper's route replaces the indicator of by a Gaussian in the direction orthogonal to and moves to the dual lattice, where the smoothing hypothesis controls the sum. Formally this requires Poisson summation for an anisotropic Gaussian (a Gaussian with a non-scalar covariance), i.e. the Fourier transform of , which is not a stated Mathlib lemma, together with summability of Gaussian sums over lattices and the identification of the dual lattice used by the Poisson formula with the one in the paper. The smoothing remark needs continuity and strict monotonicity of a lattice theta series and its limits at and .
EuclideanSpace ℝ (Fin n) with Lebesgue measure. A lattice is L : Submodule ℤ (EuclideanSpace ℝ (Fin n)) with [DiscreteTopology L] [IsZLattice ℝ L] (discrete, full rank), the same shape as the referenced Poisson summation item. is LinearMap.BilinForm.dualSubmodule (innerₗ _) L; is written .tsums over the lattice or its dual; they are summable, so the values are the true sums. is a mass function on the points of , and the probability of is the sum of the masses of the lattice points outside .tsum, the smoothing hypothesis is not vacuous (), and the goal is the probability bound, not the expectation bound of milestone 3.EuclideanSpace, summability and monotonicity of lattice theta series, and the smoothing remark, each reusable in the sibling missions of this series.Many problems in signal processing, statistics and decision theory have two blocks of variables coupled by a smooth term: matrix factorization, blind deconvolution, feasibility problems for two sets, and models of two agents adjusting their decisions in turn. Minimizing over one block at a time (alternating minimization, or Gauss–Seidel) is the natural method. Without convexity it can oscillate, and its iterates need not converge. Attouch, Bolte, Redont and Soubeyran (Math. Oper. Res. 35(2), 2010; arXiv:0801.1780) regularize each block step by a proximal term. They prove that, when the objective satisfies the Kurdyka–Łojasiewicz (KL) inequality, every sequence of the method that does not run off to infinity has finite length and converges to a critical point.
Timeline:
Let and be proper (never , finite somewhere) and lower semicontinuous. Let be continuously differentiable, with Lipschitz on bounded sets. This is assumption (H) for
The product carries the Euclidean norm . Write .
Given and step sizes , the proximal alternating scheme is
Assumption (H1) asks that , that be proper, and that for all , for some .
The Fréchet subdifferential is the set of with . The limiting subdifferential collects the limits of along with . A point is critical if . has the KL property at if there are , a neighbourhood of and a continuous concave with , , , such that
If satisfies (H), (H1) and has the KL property at every point of , then every sequence of (5–6) satisfies
Theorem 9 makes the KL inequality the single hypothesis behind global convergence of a nonconvex block method. Semi-algebraic, subanalytic and definable data satisfy it, so the theorem covers sparse and low-rank regularizers, indicator functions of semi-algebraic sets, and polynomial couplings. With , and it yields convergence of an averaged alternating projection method between two closed sets (§3.4 of the paper). The proof pattern of sufficient decrease, a relative-error subgradient bound and the KL inequality was later abstracted for PALM and many other algorithms. A formal proof of this paper's argument therefore covers the template those analyses reuse.
The result has been proved since 2010. To our knowledge it has not been formalized in any proof assistant. Mathlib has the Fréchet derivative and the gradient, but no limiting subdifferential and no KL theory. The published Prove2Me definitions of the limiting subdifferential and of the KL property (from the Li–Pong ADMM series) are reused here, so this mission also tests that infrastructure on a second algorithm.
The decrease estimate (7) gives only . That makes steps vanish and limit points critical (Proposition 6), but it does not give convergence, because square-summable steps can have infinite total length. Turning square summability into summability needs the KL inequality. That inequality holds only near a critical point and only on a sublevel band, so the iterates must first be shown never to leave a ball , by an induction that uses the very finite-length estimate it is trying to establish. The constants in (16) are arranged so that this induction closes. A second difficulty is nonsmooth calculus: the subdifferential sum rule for and the closedness of the graph of along sequences with converging function values. Lower semicontinuity alone does not give convergence of the function values; the proximal inequalities do.
Everything lives in the namespace ProxAltMin.Conv, in Lean 4 with Mathlib. Conventions:
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and the product is the product WithLp 2 (… × …), not the sup-norm product.EReal with "never " as part of properness.Theorem and page numbers are those of arXiv:0801.1780v3 (22 Jan 2013), which is the version read; the published article has the same content.
A trivializing formalization is ruled out: the run predicate is satisfiable (Lemma 5's existence milestone; for any constant sequence is a run), the constants and are tied to the data rather than chosen by the prover, and no conclusion is a sum or a distance whose library value is on bad input.
Needed infrastructure: the subdifferential calculus behind Proposition 3 (a smooth perturbation and a separable sum), the closedness of the limiting subdifferential, existence of proximal minimizers for coercive lower semicontinuous functions on , and the elementary but delicate bookkeeping of Theorem 8. The first two are reusable well beyond this mission. Contributions welcome: proofs of any milestone, and general lemmas on limiting subdifferentials stated as separate theorems.
A busy runway is the bottleneck of an airport, and the order in which arriving or departing aircraft use it determines how many operations fit into an hour. Consecutive aircraft must be spaced by minimum separations that depend on both aircraft (a light aircraft behind a heavy one needs a long gap because of wake turbulence), so reordering the first-come-first-served (FCFS) queue can raise throughput considerably. Unrestricted reordering is unacceptable in practice: it makes the controllers' job harder and can push one aircraft to the back of the queue indefinitely. Following Dear (1976), constrained position shifting (CPS) allows each aircraft to move at most positions away from its FCFS position, with between 1 and 3 in practice.
Earlier algorithms for CPS either exploited a small number of aircraft types and ignored time windows and precedence constraints (Psaraftis 1980), or needed exponentially many parallel processors (Trivizas 1998), and Carr (2004) conjectured that runway scheduling under CPS has exponential complexity in general. Balakrishnan and Chandran (Oper. Res. 58(6), 2010) showed that, for fixed , the problem with time windows and precedence constraints is solved by dynamic programming on a network whose size is linear in the number of aircraft. This mission formalizes the core of that result: the network, its precedence pruning, and the dynamic program for the minimum makespan.
There are aircraft, labelled in FCFS order, and the landing positions are also . An instance consists of
A -CPS sequence is a bijection from positions to aircraft with for all . A feasible schedule is such a with landing times such that , for all positions , and every precedence pair is respected. The makespan is , the landing time of the last aircraft.
The CPS network has stages . A node of stage is a list of distinct aircraft occupying the positions that end at , each within of its FCFS position; its last entry is its final aircraft. An arc joins a stage- node to a stage- node when the first entries of are the last entries of . A source-sink path picks one node per stage, joined by arcs, and its sequence puts the final aircraft of the stage- node at position . The pruned network deletes the nodes that violate a precedence pair : those containing before , or at a position less than , or at a position greater than .
On , with the window of the final aircraft of , the separation between the final aircraft of and , and the predecessors of , the dynamic program is at stage 1 and
with .
where is stage of ; the second identity is stated as " is the least makespan iff is the least admissible " for every real .
The network turns a search over permutations into a shortest-path-like computation over nodes, so for the small values of used in practice the minimum makespan with time windows and precedence constraints is computed in time linear in . The same network underlies the paper's algorithms for total delay (§5.2) and, in a time-expanded form, for arbitrary separable costs without the triangle inequality (§6).
The paper's proofs are short and informal. A formalization pins down exactly what means (the paper describes it only as "arrival time of the final aircraft of node in an optimal solution"), makes precise which nodes the precedence pruning removes, and checks the correctness of the stage- rule. The result has not been machine-checked before.
Two features of the model make the correctness of the network nontrivial. First, a node records only a window of at most consecutive positions, so nothing local prevents a path from using the same aircraft twice or omitting one; Theorem 1 asserts that the global sequence is nevertheless a permutation, and Lemmas 1 and 2 assert that precedence, a global property of the sequence, is detected inside single nodes. Second, the recursion (1) adds the separation only between consecutive aircraft, while feasibility constrains every pair of aircraft; the triangle inequality is what reconciles the two, and without it Lemma 3 fails.
The obvious reading of §4.1 also fails: taking the least over all stage- nodes, as the paper prints, can select a node whose final aircraft lands after its latest time. The goal filters stage by .
All data are real numbers; aircraft and positions are Fin n, 0-based; stages are 1-based natural numbers; [NeZero n] encodes . Separations are pairwise in the definition of feasibility, never only consecutive. The recursion takes values in WithTop ℝ, with ; optima are stated with IsLeast over sets of makespans, never with a real infimum. Precedence pairs are a Finset of ordered pairs of distinct aircraft, covering both of the paper's cases.
Explicit readings of loose phrases:
Not formalized: running times (Proposition 1 and the preprocessing remark), the predecessor pointers and tie-breaking that reconstruct an optimal sequence, the removal of nodes unreachable from the source or the sink (it does not change the set of source-sink paths), asymmetric shifts (§3.2) and disjoint time windows.
A formalization that defines feasibility with consecutive separations only, defines by the recursion and states Lemma 3 as an unfolding, or states Theorem 1 as "some CPS sequence exists iff some path exists" would be trivial; the statements here avoid all three.
The definitions (instance, -CPS sequences, the CPS network and its pruning) are shared with the two other missions of this series (total delay, discrete time) and may be consolidated later. Proofs of the milestones, and lemmas about the window structure of the network, are welcome.
Fast-fashion retailers such as Zara replenish their stores several times a week from a central warehouse, and the warehouse holds a limited stock of each garment that must be split across hundreds of stores. Caro and Gallien built the store-level sales model behind the shipment-allocation system they developed with Zara and tested in a live pilot (Caro and Gallien, Inventory Management of a Fast-Fashion Retail Network, working paper, August 2, 2007; published in Operations Research 58(2), 2010). One display policy shapes the model. A garment (a reference) comes in several sizes, a few of which are designated major sizes. As soon as one major size runs out in a store, the whole reference is removed from the shop floor, so the remaining stock of the other sizes stops selling.
The allocation optimization only works if expected store sales have the right shape. They must grow with inventory, show decreasing marginal returns, and show complementarity across sizes. Proposition 1 of the paper establishes these properties for the model. The paper also cites the analogous result of Lu and Song (2003) for assemble-to-order systems as the template for its proof.
Fix a finite set of sizes , split into the major sizes and the minor sizes . Time is measured from the last replenishment, and the next replenishment comes at time .
Demand is random. On a probability space, each size has a counting process , the number of sale opportunities for in . It is a Poisson process with rate :
The processes of different sizes are mutually independent. In Lean this family is IsPoissonFamily lam N P.
An inventory vector gives the stock of each size right after replenishment. The virtual stockout time of size is
the time at which size would run out if it stayed on display. For a set of sizes , write and . Under the major-size policy, the random sales over one period are
The expected sales function is (expectedSales). The proof also uses (hA) and the marginal difference (delta), where is the -th unit vector.
For every and all sizes :
and is supermodular on the lattice :
The statement is uniform in the rates, the horizon and the choice of major sizes, so it covers every instance of the model.
The result. Proposition 1 justifies treating each store's expected sales as a concave, complementary function of the size profile. The paper's allocation MIP is built on that structure. It approximates by a lower envelope of tangents and embeds the approximation in a mixed integer program that allocates warehouse stock across stores. The proposition explains why sending a unit of a major size can raise the value of the minor sizes already in a store. It also explains why the marginal value of a size falls as more of it is shipped. Without these properties a greedy or envelope-based allocation would have no structural footing.
Formalizing it. The result is proved on paper, with one error in the printed proof. The last line of the Appendix display gives as a probability, but the quantity is a time. The correct value carries a factor and has in place of . This mission states the corrected identity. As far as is known, no machine-checked proof of any part of the result exists. A complete development would give a verified link from a continuous-time stochastic model to the discrete convexity properties that inventory optimization relies on. It would also produce reusable facts about Poisson processes and their hitting times along the way.
The monotonicity of is pathwise and elementary. The other properties are not pathwise properties of . Under the major-size policy, a realisation of need not have decreasing increments in . The concavity and the complementarity appear only after taking expectations and rewriting through the stopping times, using identity (2). That identity is an optional-sampling statement for the compensated Poisson processes at the bounded random times . These times depend on several independent processes at once, so the relevant filtration is the joint one. Mathlib has optional sampling only in discrete time.
The marginal-difference formula needs three ingredients:
The first idea, proving concavity of directly from (1) path by path, fails for the reason above.
All objects live in the namespace FastFashion.Structure:
Fintype with decidable equality. The major sizes are a Finset Sp and the minor sizes are its complement. No nonemptiness assumption is placed on the sizes or on ; is allowed, as in the paper.Pi.single s 1.WithTop ℝ. It is on paths that never reach , so it is never Lean's junk value , and . The truncation (stopMin) is a real number in .Supermodularity.Monotonicity.SupermodularOn, applied on the whole lattice.Two formalizations would trivialize the mission, and neither is used. is defined as the expectation of from (1), never by formula (2), and is never defined by a product-of-probabilities integral. Proposition 1 states both readings of "supermodular": the per-coordinate marginal-difference inequalities and the lattice inequality.
Deviations from the printed text:
Infrastructure a complete development needs:
The Poisson-process and hitting-time lemmas are reusable well beyond this mission and are welcome as separate contributions. The companion mission on the paper's tangent-envelope approximation uses the same model layer.
Runway capacity is the binding constraint at many busy airports. An aircraft landing or taking off behind another must wait a minimum separation time that depends on the two aircraft's weight classes, because of wake vortices; the US Federal Aviation Administration publishes these spacing requirements. Reordering aircraft changes the sum of the separations incurred and hence the delays, but unrestricted reordering is unacceptable to airlines and controllers: an aircraft that arrived early could be pushed to the end of the queue. Constrained position shifting (CPS), introduced by Psaraftis (1980) and used in the United States and Europe since, allows each aircraft to move at most positions from its first-come-first-served (FCFS) position.
Balakrishnan and Chandran (Operations Research 58(6), 2010) recast CPS scheduling as dynamic programming on a layered network, the CPS network, whose size is polynomial in the number of aircraft for fixed . Their §4 minimizes the makespan (the landing time of the last aircraft). §5.2 minimizes the total delay, equivalently the average delay, which measures passenger and airline cost more directly. This mission formalizes §5.2.
There are aircraft labelled in FCFS order, a maximum position shift , separations (the minimum time between leading aircraft and trailing aircraft ), and a finite set of precedence pairs with , meaning that must land before . The separations satisfy the triangle inequality , as wake-vortex separations do for arrivals-only or departures-only operations.
A -CPS sequence is a permutation of the aircraft (position receives aircraft ) with for every . A feasible schedule is a -CPS sequence that places before for each precedence pair, together with landing times (by position) such that
There are no time windows. Its total delay is , measured from time , at which all aircraft are available.
The CPS network has stages . A node of stage is a sequence of distinct aircraft that can occupy positions (each within of its position). Its last aircraft is its final aircraft. An arc joins a stage- node to a stage- node when the sequences overlap: the first aircraft of are the last aircraft of . A source-sink path picks one node per stage, and its sequence assigns position to the final aircraft of the stage- node. Precedence is incorporated by deleting every node that places before for some pair , or that places an aircraft outside the positions a pair allows it (§3.1). The result is the pruned network . For nodes , is the separation between their final aircraft.
For a node in stage and times along a path to , the paper uses the partial objective
Give the arc from stage to stage the distance , and source and sink arcs distance . Then a feasible schedule exists if and only if has a source-sink path, and
where each minimum exists exactly when the other does.
where is the set of predecessors of in .
The result turns a sequencing problem over up to orders into a shortest-path computation on a directed acyclic graph with nodes, and it does so while respecting precedence constraints, which earlier CPS algorithms (Psaraftis 1980; Trivizas 1998) could not handle. It is the average-delay counterpart of the makespan algorithm of §4 and shares its network. The same network carries the discrete-time models of §6.
The paper's proof of the equivalence is one sentence ("follows from properties of shortest paths and is omitted here"). Propositions 2 and 3 are proved in a few lines, and Theorem 1 by an argument about windows of consecutive positions. None of these results has a machine-checked proof. A formal development makes explicit the conventions the prose leaves implicit (the time origin, pairwise separations, which nodes Proposition 3 refers to) and checks that the recursion and the shortest-path value really compute the minimum total delay.
The arc distances weight the separation into stage by , the number of aircraft whose landing it delays. The equivalence needs two directions. A path's length must be the total delay of the schedule that lands each aircraft at its predecessor's time plus the separation, and that schedule must satisfy every pairwise separation, not only the consecutive ones; this is where the triangle inequality enters. Conversely, every feasible schedule must have total delay at least the length of its sequence's path, and every feasible sequence must be a path of . The last point is Theorem 1 with precedence pruning: a node sees only consecutive positions, so detecting a violated precedence pair inside one node requires the position filter of §3.1 for pairs that reverse FCFS order. Proposition 3 is false for nodes that lie on no source-sink path, which the printed statement does not exclude.
Aircraft and positions are Fin n, 0-based, and stages are 0-based natural numbers, so the arc into stage has distance . Separations are real, nonnegative and satisfy the triangle inequality; feasibility requires them between every pair of positions. Landing times are real and nonnegative. The paper fixes no time origin, but its path length equals the total delay exactly when delays are measured from , and without a lower bound on the times the objective has no minimum. Minima are stated with IsLeast on sets of values, never with a real infimum. Feasibility and the existence of a path are stated separately, because the equality of least elements alone does not force them to exist.
The following loose phrases are given explicit readings. "In an optimal solution" (Proposition 2) means a feasible schedule whose total delay is at most that of every feasible schedule. "The CPS network" in Proposition 3 means nodes lying on a source-sink path, stated for the network without precedence pruning, which also covers the pruned one. "" means the least element of the set of values of over partial schedules ending at , and the printed is read as . The boundary value is not printed and is stated explicitly. Precedence pruning uses the printed Case II rule. Running times (the bound) are not formalized.
A trivializing formalization would require separations only between consecutive aircraft, define the minimum by the recursion itself, or use a network whose nodes need not be distinct or admissible. Here the minimum is defined directly over feasible schedules, separations are pairwise, and the nodes are checked against the paper's Figure 1 (stage sizes 2, 4, 7, 14, 14, 7 and 13 paths for , ).
The development needs finite sums, permutations of Fin n and lists. The network layer (stages, arcs, precedence pruning, Theorem 1) is shared with the makespan and discrete-time missions of this series and reusable for any CPS objective. Proofs of any milestone, alternative proofs of the goal, and generalizations (asymmetric shifts, §3.2) are welcome.
Facility location models decide where to open depots, warehouses or service centres and which customers each one serves. Classical models assume that an open facility always works. In practice facilities are disrupted by weather, strikes, power loss or supplier failure, and a network designed for normal operation can become very expensive when its nearest facilities go down. Reliable facility location models place facilities so that the sum of the fixed cost and the expected transportation cost, taken over random facility failures, is minimal.
Cui, Ouyang and Shen (UCTC-FR-2010-02, 2010; published as Oper. Res. 58(4):998–1011) study the case in which each site fails independently with its own probability. The most direct model of this situation is a scenario-based stochastic program: list every pattern of failures, give it its probability, and let each customer be served optimally in each pattern. That program has scenarios for candidate sites and cannot be written down for realistic . The paper proposes instead a compact formulation in which each customer receives an ordered list of backup facilities ("levels") and the probability that each level is the one that serves her is carried by a small set of recursive variables. This mission is about the claim that the compact model loses nothing.
The level-assignment technique comes from Snyder and Daskin (Transp. Sci. 39(3):400–416, 2005), who treated the case of one common failure probability for all sites. The uniform-probability model of Snyder and Shen's textbook is on the platform as SupplyChainTheory_disruptions; it is a different model (one , no cap on the number of levels) and is not reused here.
There are customers with demand rates and candidate sites with fixed costs and failure probabilities . Failures are independent. Shipping one unit from site to customer costs , and each unit of missed demand of customer costs a penalty . An emergency facility with index never fails (), costs nothing to open (), and "serves" at the penalty cost .
The compact model (RUFL). Each customer is assigned to facilities at levels , with ; a level- facility serves her exactly when all her facilities at levels have failed. The variables are (site open), (facility is customer 's level- facility) and , the probability that serves at level . Constraints (1b)–(1d) say that each level holds one facility until the emergency facility appears, which happens exactly once, and that only open sites are used, each at most once. Constraints (1e)–(1f) fix : and . The objective is
The scenario model (SSP). A scenario is , with if site operates in (and always). Its probability is . With (customer served by in ), (SSP) minimizes
subject to and for regular .
If , both programs have optimal solutions, and for every optimal of (RUFL) and every optimal of (SSP),
The paper states this as "formulation (1a)–(1g) is equivalent to the stochastic programming formulation that covers all failure scenarios"; its proof shows equality of optimal values, and that is the reading formalized.
The proposition says that, with enough levels, the compact model is exact: its optimal value is the true minimum expected cost over all failure patterns. The compact model has variables and constraints against for (SSP), and after the standard linearization of the products it is an ordinary mixed-integer program to which the paper's Lagrangian relaxation applies. For the paper notes the compact model is in general not equivalent; Proposition 1 is the anchor that says what the parameter trades away.
The result is proved in the paper; as far as we know it has not been formalized. The work here is to formalize that proof: the product-measure computation behind milestone 1, the two explicit solution maps, and the exchange argument behind the normalization. The probability identity for "first success in an ordered list of independent trials" and the scenario-to-level bookkeeping are reusable for other reliability models built on Snyder–Daskin levels.
The cost identities are routine once the right bookkeeping is in place; the obstacle is that bookkeeping. In direction (RUFL) → (SSP) one must show that the recursion (1e)–(1f), which multiplies by and sums over all regular , collapses to the closed product along a customer's assigned list, using that (1b)–(1d) put exactly one facility on each level until the emergency facility and that (1c) forbids repeats. Then the sum over the scenarios must be regrouped by the first operating facility on that list, which needs milestone 1 on a product space.
The converse direction is where enters, and the naive attempt fails: an arbitrary optimal (SSP) solution may serve a customer by different, equally good facilities in different scenarios in ways that no single ordered list reproduces. The normalization step removes this freedom; only after it can one read off a single list per customer, and guarantees that this list (all open sites no farther than the penalty, then ) fits on the available levels.
Indices are 0-based; facilities are Fin (J+1) with Fin.last J the emergency facility, and levels are Fin (R+1). The extended data , , and the conventions , are definitions, not hypotheses. Scenarios are Fin J → Bool and is the explicit finite product; no measure theory is involved, and (17a) is a finite sum. Binary variables are real numbers constrained to . is expressed by taking the instance type Instance I J J; with the standing this means . Demand rates are nonnegative; no sign is assumed on , or .
Two printed constraints are corrected, and the formalization commits to the corrections. The first sum in (1b) is printed over the regular sites ; it runs here over all facilities, as the paper's own reading of (1b) requires. Constraint (17c) is printed as , which gives each site a capacity of one customer per scenario and makes Proposition 1 false; it is stated here per customer, .
The goal asserts existence of optimal solutions of both programs before comparing their values, so it cannot hold vacuously. Contributions welcome: proofs of the milestones, a general lemma on the probability that the first success among independent Bernoulli trials occurs at a given position, and an existence-of-optimum lemma for finite binary programs.
A facility location plan decides which sites to open and which customers each site serves. Real facilities fail: plants are shut by strikes, warehouses by floods, distribution centres by power outages. When a customer's facility is down, she is served by a backup facility, or not served at all at a penalty. Reliable facility location chooses sites and backup assignments together, minimizing fixed costs plus the expected transportation and penalty cost over the random failures.
Snyder and Daskin (2005) introduced the level-assignment formulation in which every customer receives a ranked list of facilities, and they assumed all sites fail with the same probability. Cui, Ouyang and Shen (2010) allow each site its own failure probability , which is the realistic case: a site in a flood plain and a site inland do not fail equally often. Their compact mixed-integer program (RUFL) is the subject of this mission.
Timeline.
There are customers with demand rates , and candidate sites with fixed costs and failure probabilities ; failures are independent. Shipping one unit from to costs , and each unserved unit of customer costs a penalty . An emergency facility with index represents non-service: , and .
Each customer is assigned at levels , . Her level- facility serves her exactly when all her facilities at levels have failed. The variables are (site open), (facility is customer 's level- facility) and , the probability that serves at level . (RUFL) minimizes
subject to: at every level a customer has exactly one facility unless she has already reached the emergency facility (1b); only open sites are used, each at most once (1c); the emergency facility is assigned exactly once (1d); and the probabilities follow the transition equations
So if a customer's levels are , then .
Assume for every customer and for every regular site. In every optimal solution of (RUFL),
where .
Proposition 2 says that for a given set of facilities assigned to a customer, the optimal order of the levels depends only on the distances, not on the failure probabilities. A solution method may therefore sort each customer's assigned facilities by distance instead of searching over orders. The paper's Lagrangian subproblem (RSP) uses exactly this: "following a similar argument to Proposition 2" (§3.3.1, p. 13), its objective depends only on the set of facilities chosen, which is what makes the set function of Proposition 3 (a separate mission of this series) well defined. The proposition does not say that the nearest open facilities are the right ones: the paper's Example 1 (p. 11) shows a farther but more reliable facility can be optimal.
The result is proved in the paper; no machine-checked proof exists. The equal-probability special case is published on Prove2Me as SupplyChainTheory.rflp_ordered_assignments (Snyder–Shen Theorem 9.10), in a different model (one , no level cap). This mission adds the site-dependent case with a level cap, and it makes explicit two hypotheses the printed statement omits.
The exchange argument is short on paper, but its bookkeeping is exactly where a formal proof has to work. The paper's modified keeps the old values at unlisted indices, and that array does not satisfy the transition equations, so feasibility of the swapped solution has to be shown with the recomputed probabilities, level by level, including the fact that levels after are unchanged. The emergency case is dismissed in one sentence; its cost change must be computed. Finally, "" needs and ; the naive reading of the printed proposition, with allowed, is false, because a level-0 facility that never fails leaves all later levels with probability zero and in arbitrary order.
Indices are 0-based. Facilities are Fin (J+1) with the emergency facility Fin.last J; levels are Fin (R+1); the extended data , are definitions. , , are real arrays, with (1g) requiring , to be or . Constraint (1b) is printed with its first sum ending at ; it is formalized with the sum over all , the reading the paper's own explanation of (1b) gives. "Optimal" means feasible with objective at most that of every feasible solution; the feasible set is nonempty (send every customer to at level 0), so the goal is not vacuous. Proposition 2 carries the hypotheses and ; without them it is false, and a statement that dropped them would be unprovable rather than trivial. The level ranges over , the range in which level exists.
The development needs only finite sums and a recursion over levels; no measure theory is required. The recomputed probabilities transProb and the two moves swapY, emergencyUpY are reusable for any exchange argument on this formulation. Proofs of the milestones, of the goal, and of the equivalence of the transition equations with the closed product form are welcome.
A submodular function on a finite set is a function on subsets of with . Minimizing such a function is one of the central tractable problems of combinatorial optimization: it contains minimum cuts in directed graphs, matroid intersection and polymatroid problems, and many scheduling and facility-location subproblems. Grötschel, Lovász and Schrijver showed in 1981 that it can be done in polynomial time with the ellipsoid method; in 2000, Schrijver (JCTB 80, 346–355) and, simultaneously, Iwata, Fleischer and Fujishige (J. ACM 48, 2001) gave the first combinatorial strongly polynomial algorithms.
In many applications the function is not defined on all subsets of but only on a ring family: a collection closed under union and intersection, such as the order ideals of a precedence relation in scheduling, or the sets of a closure system. The last section of Schrijver's paper (§6, pp. 353–354) shows that nothing is lost: any algorithm minimizing submodular functions on all subsets of also minimizes a submodular function given only on a ring family. This mission formalizes that reduction.
Let be a finite set. A collection of subsets of is a ring family if and whenever . A real function is submodular on if
Following the paper, is normalized: , , and for all , where is the smallest set of containing . (Elements with the same can be identified.) Under this normalization is the family of lower ideals of a partial order on .
For , the closure is the smallest set of containing . For , is the largest set of not containing . The paper defines weights
with the modular extension , and the function on all subsets of
In Lean, is a type with [Fintype V] [DecidableEq V], subsets are Finset V, is C : Set (Finset V), and the objects above are IsRingFamily C, SubmodularOn C f, closure C X, M C v, L C v, cw C f v (for ), csum C f X (for ) and g C f X, all in the namespace SchrijverSFM.Ring.
Under the normalization above, for submodular on :
and, if minimizes over all subsets of , then and
Both conjuncts are needed: the second alone follows almost from the definitions, while the first is what makes an all-subsets algorithm applicable to in the first place.
The reduction means that a single algorithm for unconstrained submodular minimization serves for every ring family, given only the sets . This is how ring-family constrained problems (for example minimum-cost closures and precedence-constrained scheduling objectives) are routinely handed to general submodular-minimization codes, and it is the standard justification for stating submodular minimization algorithms over only.
On the formal side, the mission produces a small reusable layer on ring families of finite sets (closure operator, the lower-ideal representation, the largest set avoiding an element) together with the monotonization trick (24), which is of independent use whenever a function on a lattice of sets has to be made monotone by a modular correction. The result is classical and its proof in the paper is complete; to our knowledge no machine-checked version exists. Companion mission I of this series formalizes the algorithm of §§2–5 itself; this mission does not depend on it, since the algorithm enters only as the hypothesis that a minimizer of is given.
Every step is elementary, but two points are easy to get wrong. First, (24) is proved on the page by assuming ; reducing the general case to such one-element steps inside requires the normalization : without it a ring family can jump by more than one element (for with the inequality (24) fails for suitable ). Second, the weights evaluate at , which belongs to only because of the same normalization; a formalization that drops it lets values of outside leak into and . The submodularity proof (27) also needs the asymmetric closure facts — equality for unions but only containment for intersections — which is exactly why the monotonicity (24) is required.
Finset V; is a Set (Finset V).Finset V; only its values on matter, and under the hypotheses no other value enters , or the conclusions. The paper allows any ordered field; the formalization uses .∅ ∈ C, Finset.univ ∈ C, and M C u ≠ M C v for u ≠ v. No hypothesis is made; §6 does not use it.Finset.inf) of the sets of containing , and the union (Finset.sup) of the sets of avoiding ; their default values on an empty family are never reached under the hypotheses.NonmonotoneSubmod.Shared.Submodular.Contributions welcome: proofs of the milestones in the order listed, general lemmas on closure operators of ring families of Finsets, and the lower-ideal representation, which is reusable beyond this mission.
A linear two-stage stochastic program with fixed recourse chooses a here-and-now decision before a random vector is observed, and pays a recourse cost afterwards. It is the basic model of stochastic programming, used in capacity planning, energy and supply-chain models. In practice the distribution of is never known exactly: it is estimated from data, replaced by a discrete scenario approximation, or perturbed for robustness. The question is how much the optimal value and the optimal decisions can move when is replaced by a nearby , and in which distance between probability measures "nearby" should be measured.
Rachev and Römisch (Math. Oper. Res. 27(4), 2002, doi:10.1287/moor.27.4.792.304; the mission cites the authors' preprint from edoc.hu-berlin.de) answer this with the method of probability metrics: they derive from the structure of the integrand a canonical distance on measures for each class of models. For linear two-stage programs the canonical distance is the Fortet–Mourier metric of order 2.
Timeline. Robinson and Wets (1987) studied qualitative stability of two-stage programs with respect to weak convergence of measures. Walkup and Wets (1969) had earlier established the piecewise-bilinear structure of the second-stage value function used here. Römisch and Schultz (1991) proved a quantitative stability result for two-stage programs with complete recourse in the Wasserstein metric . The present paper (published 2002) replaces complete recourse by relatively complete recourse plus dual feasibility, and by the metric , which it bounds by a multiple of (p. 13).
Let be a nonempty polyhedron and a polyhedron. Fix , an -matrix , and data , and an -matrix depending affine linearly on . The second-stage value is
with and . The integrand is when and , and otherwise. For a Borel probability measure on the problem is
with optimal value and solution set . Two assumptions are made: (A1) and for all ; (A2) has a finite second moment.
The Fortet–Mourier metric on , the probability measures on with finite second moment, is
For an open bounded , the growth function is , and with .
Under (A1), (A2), and an open bounded neighbourhood of , there are and such that for every with :
The constants are existential, so the goal does not depend on any particular estimate of them.
The theorem says that, under the two natural well-posedness conditions of linear recourse models, optimal values are Lipschitz continuous and solution sets move by at most , where only sees test functions with the local Lipschitz growth of the integrand. Since , the result contains the earlier stability theorem.
The results are proved in the paper, except Lemma 3.1, which it cites from Walkup and Wets (1969). None of them is formalized in Mathlib or on Prove2Me. A formalization would provide a checked model of the two-stage recourse function, the Fortet–Mourier metrics, and an end-to-end quantitative stability theorem for stochastic programs, none of which exist in Mathlib.
The obvious argument bounds by and then by . Two steps fail. First, the supremum ranges over all of , which may be unbounded, while lies in only for in a bounded set; the argument must localize to and then show, using convexity, that for close to the localized and global problems coincide. Second, the Lipschitz estimate in for requires the piecewise-bilinear structure of (Lemma 3.1) and a chaining argument across the polyhedral pieces of ; the integrand is not differentiable.
EuclideanSpace ℝ (Fin n). The paper never fixes its norm and all its constants are existential, so the Euclidean norm is a faithful instance. Second-stage vectors are coordinate vectors Fin k → ℝ; index sets are 0-based.DupacovaWets.Consistency.expect over restricted to .A Markov decision process is specified by numbers: transition probabilities and rewards. In practice these numbers are estimated from data, elicited from experts, or produced by aggregating the states of a larger model, and in each case what is actually known is a range for each parameter rather than its value. Givan, Leach and Dean (Artificial Intelligence, 2000) introduced bounded-parameter MDPs (BMDPs) to reason about a whole family of MDPs at once: every transition probability is only known to lie in a closed interval. Their motivation was state-space aggregation, where grouping states with similar but not identical dynamics yields exactly such interval bounds, and the same object later reappeared as the interval or "box" uncertainty set of robust MDPs (Nilim and El Ghaoui, 2005; Iyengar, 2005) and of optimistic exploration in reinforcement learning (Strehl and Littman, 2008).
Over such a family, the value of a policy is no longer a number but an interval, and "optimal" needs a definition. This mission formalizes the paper's answer: two total orders on intervals, the corresponding optimal policies, and the Bellman-like equations their interval value functions satisfy.
An exact MDP has a finite set of states, a finite nonempty set of actions, transition probabilities with , a reward for each state and a discount rate . A policy is a map ; is the set of all policies. The value function is the expected discounted sum of rewards along the Markov chain with transitions . The operators
act on value functions . is the statewise order.
A BMDP gives for each an interval with , a reward and a discount rate . Its members are the exact MDPs with that and and with . The interval value of a policy is
Intervals are compared by the optimistic order, which compares upper bounds first and breaks ties by lower bounds, and the pessimistic order, which compares lower bounds first:
A policy is optimistically optimal if for all and ; pessimistically optimal is defined with . The optimal interval value functions are and .
At every state ,
and the same with in place of . The maximum over actions is for the total order on intervals: attained by some action and an upper bound for every action.
In the order the proof uses them: Theorem 3 (second sentence: is the unique fixed point of ); Theorem 6 (comparison: implies , and its three variants); Lemma 1 (every member's values and backups are bracketed by finitely many order-maximizing MDPs); Lemma 2 (statewise composition of member MDPs dominates, or is dominated by, both components); Theorem 7 (-maximizing and -minimizing MDPs exist among the order-maximizing ones); Corollary 1 ( and are a minimum and a maximum for ); Lemma 3 (statewise composition of policies improves the upper, resp. lower, bounds); Theorem 8 (optimistically and pessimistically optimal policies exist).
Theorem 9 is the interval analogue of the Bellman optimality equation. It is what makes the optimal interval value functions computable: the paper's interval value iteration algorithms and (Section 5) iterate exactly the right-hand sides of (25) and (26). The lower half of (26) is the max-min equation of robust dynamic programming with rectangular box uncertainty, and the upper half of (25) is the max-max equation behind optimistic planning; Theorem 9 states both, together with the tie-breaking second component, in one model. Theorems 7 and 8 are of independent use: a single member MDP is worst (or best) for a policy at all states at once, and the partial orders on interval value functions nevertheless have maxima over policies.
None of these results has a machine-checked proof. The platform has robust Bellman equations in other models (costs, general rectangular sets, a sup over nature) but nothing on BMDPs, interval value functions, or the orders and . The mission produces the paper's optimality theory end to end, from the comparison principle for exact MDPs to the two Bellman-like equations, on a model shared with the companion mission on interval policy evaluation.
The orders and are total on intervals but only partial on interval value functions, and they are lexicographic. The obvious construction of an optimal policy, switching statewise to whichever of two policies has the better interval, fails: the composed policy need not dominate either component in , because lower bounds can get worse at states where the upper bounds do not change (the paper says so explicitly, eq. (20)). Existence therefore needs a two-stage argument. A second obstacle is that and are defined statewise, as minima over an uncountable family; that one member attains them at every state simultaneously is a theorem (Theorem 7), and the Bellman-like equations rest on it. Finally, the inner minima in (25) act on , the lower bound of an optimistically chosen policy, which is not the componentwise best lower bound over policies; the equation couples the two components through the tie-break.
and are finite types, is nonempty; may be empty. An exact MDP is a structure with transition function F p α q , stochastic rows, reward and discount . is defined as the convergent series , not as a solution of (2). Rewards of the BMDP are tight, as the paper assumes from footnote 3 on; reward intervals are not formalized. Members of form a subtype of exact MDPs with the BMDP's and . The minima and maxima of Definition 3 and of (25)–(26) are the real infimum and supremum over that subtype, which is nonempty and on which values are bounded, so no junk value enters. Intervals are pairs (lower, upper); the orders (17) are spelled out. Policies are deterministic stationary maps , the paper's . An ordering of is a bijection Fin |Q| ≃ Q, and the index of Definition 1 is the largest index at which expression (9) does not exceed 1 (the page's phrase admits ties; only the largest index keeps the remaining mass inside its interval). Definition 8 is read as for an optimistically optimal , so the goal is quantified over all optimistically (pessimistically) optimal policies; Theorem 8 is the milestone that makes this quantification non-vacuous. Lemma 3 is stated as in the Appendix (p. 36): part (d) concerns , where p. 17 misprints .
A formalization in which members carry their own discount, rows need not sum to one, the minima range over all functions , or is the componentwise supremum over policies would make several statements false or trivial; each is ruled out above.
Contributions welcome beyond proofs of the milestones: a reusable theory of discounted policy evaluation for finite MDPs (the series representation, the fixed-point characterization, monotonicity of ), which other missions on finite MDPs can import.
Many decision problems in operations research ask for the best element of a finite set of alternatives when each alternative's cost is random: which projects to fund when resource use is uncertain, which crew pairings to fly when delays are random, which items to pack into a knapsack whose overflow is penalized. The expected cost is rarely available in closed form, because it is a high-dimensional integral over the distribution of the random data. The sample average approximation (SAA) method replaces the expectation by an average over a random sample and solves the resulting deterministic problem with a standard discrete optimization routine. The method is widely used in stochastic programming (see Shapiro, Dentcheva and Ruszczyński, Lectures on Stochastic Programming, SIAM 2009, Ch. 5, https://doi.org/10.1137/1.9780898718751).
Kleywegt and Shapiro (preprint; published with Homem-de-Mello as SIAM J. Optim. 12(2):479–502, 2002, https://doi.org/10.1137/S1052623499363220) ask why the method works so well for discrete problems. Their answer is a large-deviations statement: when the feasible set is finite, the probability that the SAA problem returns a wrong answer decays exponentially in the sample size. This mission formalizes that result, Proposition 2.2 of the two-author preprint, together with its consistency companion, Proposition 2.1.
Let be a nonempty finite set, a random element of a measurable space , and such that is measurable and for every . The true problem (1.1) is
Let be an independent, identically distributed sample with the law of . The sample average function and the SAA problem (2.1) are
For , the -optimal sets are and ; at they are the optimal sets and . Two numbers drive the analysis: the maximal deviation of (2.2), and the well-conditioning number
of (2.3), the gap between the -optimal solutions and the rest.
For a real random variable with moment generating function and logarithmic moment generating function , the rate function is . Assumption A requires that for every the moment generating function of be finite in a neighbourhood of .
Under Assumption A, for every there is with
The constant is not specified: it depends on through rate functions and cannot be computed before the problem is solved. The goal asserts only its existence, which is the paper's claim.
Proposition 2.1 ( w.p.1, and w.p.1 for large enough), the almost-sure convergence of (2.2), the singleton consequence ( implies eventually), the facts , the Example of §3.2 showing that a sample size can be required, and the computation on the hypercube with best value (§4).
Proposition 2.2 explains the practical behaviour of the SAA method on discrete problems: an exact optimal solution of the true problem is obtained with probability approaching one exponentially fast, so a moderate sample often suffices even when the number of feasible solutions is astronomically large. It is the basis of the paper's replication argument (§3.2: the probability of success of one SAA replication tends to one exponentially fast) and identifies as the quantity that governs the difficulty of a stochastic discrete problem, which the numerical study of §4 then examines. Later sample-size estimates for SAA (Shapiro, Dentcheva and Ruszczyński 2009, §5.3) refine the same argument into explicit, non-asymptotic bounds.
The result is proved in the paper. The mission produces a machine-checked proof of it and of its ingredients, including a Lean statement of the Cramér–Chernoff upper bound with the rate function in the extended reals and the positivity of above the mean under a local moment condition. To our knowledge none of these is formalized on the platform or in Mathlib in this form.
The argument is short on paper; the formal difficulty is in the large-deviations step. Mathlib has the Chernoff inequality and the factorization of moment generating functions of independent sums, but the step from there to requires passing to a supremum over in the extended reals, handling where , and the case . The positivity requires , i.e. differentiating the moment generating function at an interior point of its domain. A naive attempt that works with real logarithms fails at probability zero, where is not , and an attempt that bounds by Chebyshev's inequality gives only a polynomial rate.
The feasible set is a Finset of an arbitrary type X, assumed nonempty; minima and maxima over it are Finset.inf' and Finset.sup', so they are attained. The sample is a sequence W : ℕ → Ω → 𝒲 of measurable maps on a probability space, mutually independent (iIndepFun) and identically distributed with W 0; the paper's is W (n - 1), and is the expectation of . Measurability of is Borel measurability. Logarithms of probabilities are ENNReal.log, with , and the limit superior in (2.5) is taken in the extended reals; this is the paper's convention and it makes the goal correct when , where the event is sure. Assumption A is stated as integrability of for near , not through the value of Mathlib's mgf, which is where the expectation is infinite. The logarithmic moment generating function is the published definition BellWilliams2001.ThresholdPolicy.logMGF (extended-real valued, off the domain of ), and is the supremum over only, as on p. 3. Wherever appears, the nonemptiness of is a hypothesis; the goal does not mention and needs none.
A trivializing formalization is ruled out: with Real.log the event " is sure" would give and make the goal false, and a rate function built from mgf would count infinite moment generating functions as ; neither encoding is used.
A complete development needs the Cramér–Chernoff bound for i.i.d. sums with an extended-real rate function, differentiability of the moment generating function at interior points, and the strong law of large numbers applied to finitely many functions. The large-deviations items (milestones 4 and 5, and ) are stated for an arbitrary i.i.d. real sequence and are reusable beyond this mission. Proofs of any item, including the optional examples, are welcome.
Randomized load balancing asks how much a dispatcher gains from a little information. In the supermarket model, jobs arrive at servers and each job inspects a few servers chosen at random before joining one. With one random choice every server is an independent M/M/1 queue, and the expected time a job spends in the system is at load . With two choices it is exponentially smaller as . This "power of two choices" underlies the design of distributed schedulers, hashing schemes and server farms, where querying every server is too expensive but querying two is cheap.
Timeline:
Customers arrive as a Poisson stream of rate , , at FIFO servers. Each customer chooses servers independently and uniformly at random with replacement and joins the one holding the fewest customers; service times are exponential with mean . Let be the fraction of servers holding at least customers at time .
A state is a sequence of reals with , and . The empty state has and for . As the tails follow the limiting system
A trajectory is a map , , whose values are states and whose coordinates satisfy (1) (from the right at ). Throughout, is an integer.
The fixed point is , so , , . A customer arriving in state becomes the -th customer of its queue with probability and then waits for services, so the expected time it spends in the system is
The target constant is
For and , , and:
The hypothesis holds for every initial state that comes from a finite system.
The comparison against is the quantitative content of the power of two choices: the companion mission shows as , an exponential improvement. Corollary 2 is what connects that number to the dynamics: it says the fixed point's expected time is actually reached from realistic initial states, and is an upper bound from an empty start. Theorem 2's comparison argument and Theorem 3's weighted potential are reused across the mean-field analysis of load-balancing variants (threshold policies, heterogeneous servers, work stealing), so the formal statements here are templates for that literature.
All results are proved in the paper (Theorem 3's proof is written out for with a remark that it extends). None has a machine-checked proof that we know of. The work is formalizing the known arguments for all , including the parts the paper delegates to a citation: quasimonotone comparison for countable ODE systems in Theorem 2, and the upper right Dini derivative handling of in Theorem 3.
The system is infinite-dimensional, so standard finite-dimensional ODE comparison and Lyapunov theorems do not apply as stated. Theorem 2 rests on a monotonicity property (raising the initial tails raises them for all time) that the paper justifies by a coupling intuition and a citation to a comparison theorem for quasimonotone systems; that theorem must be supplied for -bounded countable systems. The plain distance is nonincreasing along trajectories but does not decay exponentially by a direct estimate; the weights must be built so that every coordinate's contribution to is dominated by , while staying geometrically bounded so that under the doubly exponential tails of Theorem 2. Exchanging with the infinite sum defining needs uniform tail control, which is again Theorem 2.
PowerTwoChoices.Limit; λ is lam : ℝ, with , in every theorem.x : ℕ → ℝ with x 0 = 1, nonnegative and antitone. A trajectory is s : ℝ → ℕ → ℝ, a state for every , with HasDerivWithinAt on Set.Ici 0 for each coordinate : right derivative at , two-sided for .l1Dist.Filter.atTop.tsum (a divergent series would make the upper bound free and the limit attainable by a junk ), dropping the summability condition in Lemma 2 ( is also a fixed point), choosing Theorem 3's weights after the trajectory, and stating anything for only.Telephone call centers are large service systems: hundreds of agents answer callers who wait in a queue and hang up when their patience runs out. Staffing them is a trade-off between the cost of agents and the quality of service, and in large centers both the efficiency (agents busy almost all the time) and the service level (most callers answered almost immediately) can be high at once. Garnett, Mandelbaum and Reiman (M&SOM 4(3), 2002) study the simplest model that captures customer abandonment, the Erlang-A or queue, and derive approximations for it in the regime where the number of agents is large.
Their Theorem 2 is the process-level justification of these approximations: the queue-length process, centred at the number of agents and scaled by its square root, converges to a one-dimensional diffusion. The steady-state performance formulas of the paper (delay probability, abandonment probability, waiting times) are computed from this diffusion and its stationary law.
Timeline.
Fix a service rate . For each the -th system has statistically identical agents, Poisson arrivals of rate , exponential service times of rate , an unlimited waiting room served first come, first served, and exponential patience of rate for every caller. A caller whose wait in queue reaches their patience abandons and does not return. The number of callers in the system, , is a birth–death process on with birth rate and death rate in state . Its initial value is an arbitrary random variable.
The traffic intensity is . The centred and scaled process is
When it counts waiting callers and when it counts idle agents, both in units of .
For and , the drift is the piecewise-linear function
and the limit diffusion solves , where is a standard Brownian motion independent of . The noise is additive, so this means: has continuous paths and for all . Below it behaves like an Ornstein–Uhlenbeck process with restraining force , above like one with restraining force .
Assume
and for a probability law on . Then
where is the solution of with , and this solution is unique in law.
On every probability space with a standard Brownian motion and an independent initial value , the equation has a solution adapted to , and any two solutions with the same and initial value are indistinguishable.
The infinitesimal expectation and variance of at the point , as displayed on p. 224, satisfy
The result. Theorem 2 is the basis for the paper's QED (quality- and efficiency-driven) approximations , which give explicit formulas for the probability of delay, the probability of abandonment and the waiting-time distribution in terms of , and . Unlike the case, may be of either sign: abandonment keeps the system stable even when the offered load exceeds the number of agents. The resulting square-root staffing rule , with , is used in call-center practice.
Formalizing it. The result is proved in the paper by Stone's criteria for birth–death processes, with uniqueness of the limit equation delegated to the literature. No many-server process limit exists on Prove2Me or in Mathlib. A formal proof would give the first machine-checked heavy-traffic process limit for a many-server queue, and the infrastructure (Poisson time-change representation of a birth–death process, path-space weak convergence to a continuous diffusion, well-posedness of a Lipschitz additive-noise SDE) would serve every other diffusion limit in queueing theory.
The infinitesimal-moment computation is elementary; it identifies the limit but does not prove convergence. The hard step is the passage from generator convergence to weak convergence of processes on : tightness of in the Skorokhod space, which needs control of the jumps (of size ) and of the unbounded state space, and identification of every limit point as a solution of the equation, which needs uniqueness of the limit. A pointwise limit of the drifts at each fixed is not enough: the convergence has to be controlled locally uniformly along the paths. A finite-dimensional limit at fixed times is weaker than the theorem.
IsBrownianReal with every path continuous and every coordinate measurable. is independent of , which is implicit in the paper. The goal asserts existence of a solution with and uniqueness of its law; dropping the uniqueness clause, fixing to a point mass, restricting to , , , or the stationary case is a different theorem.Contributions welcome: a Poisson time-change existence theorem, tightness criteria in , well-posedness of Lipschitz SDEs with additive noise, and the martingale-problem approach to identifying limits.
Regev's On Lattices, Learning with Errors, Random Linear Codes, and Cryptography (J. ACM 56(6), 2009, Article 34; doi:10.1145/1568318.1568324) introduced the Learning with Errors (LWE) problem and built a public-key cryptosystem on it. The source for this mission is that published J. ACM article. The paper's main theorem, a quantum reduction from worst-case lattice problems to LWE, is outside this series; this mission formalizes a self-contained piece of finite combinatorics from §5.
In the cryptosystem the public key is a list of LWE samples, and a bit is encrypted by adding up a uniformly random subset of them. Semantic security rests on one fact: if the public key were truly uniform, the sum of a random subset of it would be close to uniform, so the ciphertext would carry no information about the bit. Claim 5.3 (p. 34:36) makes this precise for an arbitrary finite abelian group . It is a special case of the leftover hash lemma of Impagliazzo and Zuckerman (1989), in which the family of functions indexed by is a universal hash family. Variants of the same statement appear in the security proofs of most lattice-based encryption schemes that use random subset sums, including the dual-Regev and GPV-style constructions.
Let be a finite abelian group, written additively, with elements, and let be an integer. For and the subset sum is the sum of the with (the empty subset gives ). The distribution of the sum of a uniformly random subset of is
The paper defines the statistical distance of two densities as , with range , and notes that the same definition applies to discrete random variables (p. 34:14). The distance of from the uniform distribution on is therefore
with no factor . Expectations and probabilities over refer to a uniform choice of , that is, the uniform distribution on all tuples, repetitions allowed: .
In Lean these objects are RegevLWE.SubsetSum.subsetSum, P, statDistUniform and expectG.
Both sentences of the claim are in the goal. The second is what the security proof (Lemma 5.4, p. 34:37) uses: for all but a fraction of public keys, the random subset sum is within of uniform. The constants are exactly as printed.
The result. Claim 5.3 is the step in the security proof of Regev's cryptosystem that removes the public key from the picture: once the key is replaced by uniform samples (by the LWE assumption), the claim shows that an encryption is statistically close to uniform, independently of the encrypted bit. The parameter choice of Lemma 5.4 is exactly what makes negligible for . Without the claim the cryptosystem would have a hardness assumption but no reduction from it.
Formalizing it. The claim is proved, with a complete argument in the paper; nothing here is open. To our knowledge no machine-checked proof of this statement, or of the leftover hash lemma for subset-sum hash families over a general finite abelian group, exists in Mathlib or on the platform. A formal proof gives a reusable, constant-exact statement of the subset-sum leftover hash lemma with the paper's normalization of statistical distance. The four milestones are standard facts about finite averages and collision probabilities that recur in many cryptographic security proofs.
There is no deep step; the work is in organizing finite counting arguments without loss. Two points need care. The collision fact holds for every pair only because the coefficients lie in : for a general linear form over a group with torsion, a nonzero coefficient vector need not give a uniformly distributed sum, so an argument that treats the coefficients as arbitrary integers fails. And passing from the bound to the expected distance requires the exchange of expectation and square root in the right direction (concavity), which is easy to misapply. The bound must hold for every finite abelian group and every , including and , with no asymptotic slack.
[AddCommGroup G] [Fintype G] [DecidableEq G]; , and is allowed (then is the point mass at and the claim holds). No hypothesis is added to the paper's statement: holds for every group.Fin l → Bool; ranges over all functions Fin l → G, so the uniform choice of is over all tuples with repetition, not over -element subsets of .Real.sqrt (Real.sqrt x).A correlated equilibrium (Aumann 1974) is a probability distribution over strategy profiles of a game such that no player gains by deviating from a recommended strategy, given the recommendation. It is the solution concept of choice when players can condition on common signals, and its set is a convex polytope defined by linear inequalities, which makes it computationally tractable in a way that Nash equilibrium is not. A natural question in learning in games is whether simple adaptive behaviour by individual players, each using only their own payoffs and the observed history, leads to it.
Hart and Mas-Colell (2000) answer this with regret matching: each player switches away from their last action with probabilities proportional to the regret for not having played other actions in the past. They show that if every player uses this rule, the empirical distribution of play converges almost surely to the set of correlated equilibria. The procedure and its analysis became standard references for no-regret learning, internal (swap) regret, and the counterfactual-regret-minimization algorithms used in large imperfect-information games.
Timeline. Foster and Vohra (1997) obtained convergence to correlated equilibria by calibrated forecasting. Fudenberg and Levine (1999) gave conditionally consistent procedures with the same consequence. Hart and Mas-Colell (2000) gave the regret-matching procedure (2.2), in which a player's probabilities depend on regrets only, together with a Blackwell-approachability variant (their Theorem A, the subject of the companion mission 2 of this series).
A finite game has a finite set of players , a finite strategy set for each player, and payoffs on . A probability distribution on is a correlated -equilibrium if for every player and all
a correlated equilibrium is the case .
The game is played at , producing a history . For the regret of player is
the average gain player would have had by playing every time they played . Fix with for every , where and . Under regret matching (2.2), if player last played , then at they play each with probability and repeat with the remaining probability; the first-period mixed actions are arbitrary, and given the history the players randomize independently. The empirical distribution of play is .
Almost surely, converges to the set of correlated equilibria:
This is convergence to a set, not to a point; the paper notes that need not converge.
They follow the Appendix proof:
The squared distance satisfies a block recursion (M1). The cross term is rewritten through the transition probabilities (M2) and compared with a stationary auxiliary process (M3–M5). It then factors into a difference of consecutive matrix powers (M6), which is small (M7). This gives
Along this gives a.s. (M9–M10), and then a.s. (M11). A companion item states the strong law for dependent variables that M10 cites.
The result. The Main Theorem shows that correlated equilibrium is reached by uncoupled play: each player needs only their own payoff function and the history of play, and nothing about the others' payoffs. Steps M10–M11 give more than the goal, namely that every player's internal regrets vanish almost surely. The procedure underlies later work on swap regret, calibrated learning and regret-minimization algorithms for extensive-form games.
Formalizing it. The result is proved in the paper. As far as a search of the platform and the local index shows, it has no machine-checked proof. The mission asks for one, following the paper's eleven steps. Several pieces are general and reusable: a bound on consecutive powers of a stochastic matrix with positive diagonal (LEMMA, proof of M7); a perturbation bound for multi-step transition probabilities (LEMMA, proof of M4); and a strong law of large numbers for martingale differences with general normalizing sequences, which Mathlib does not have in this form.
The natural approach is Blackwell approachability: show that the expected regret vector moves toward the nonpositive orthant in one step. It fails here. The one-step condition holds when a player uses an invariant distribution of , which is the procedure of Theorem A, but regret matching uses a row of instead. The cross term of the one-step recursion therefore does not vanish.
The proof has to work over blocks of periods. Within a block the players' choices are not independent given , because the transition probabilities change with time. The paper therefore compares the play with a process whose transitions are frozen at time . The matrix-power estimate cannot use convergence of , since only the diagonal of is known to be positive and may be reducible or periodic in its off-diagonal structure. The block length must also balance the errors and , which is why the subsequence appears.
Players form a Fintype ι, strategies form Fintypes S i, each nonempty, and a profile is a function ∀ i, S i. is Mathlib's stdSimplex. Time is 0-based: play τ is , and a history is a tuple Fin t → ∀ i, S i. Regrets, , and are deterministic functions of a finite history. Every statement has , because the Lean value at is a default. A play of a behaviour profile on a probability space (IsPlay) is a sequence of profile-valued random variables with measurable level sets whose conditional law given any history of positive probability is the product of the players' mixed actions. Statements quantify over every probability space carrying a play, and conditional quantities given assume . The auxiliary -process is encoded by its explicit law, a power of the product transition matrix. The paper's (footnote 34) is a constant chosen after the game, and and before the initial play, the probability space and the play. Distances on are sup distances.
The hypotheses are exactly footnote 5's: and , with one for all players. The goal requires every player to follow (2.2). If other players may play arbitrarily the statement is false (§4(d)), so IsPlay constrains all of them. The goal is stated with an existential correlated equilibrium at distance less than , not with a distance to a possibly empty set, so no encoding makes it vacuous.
Disclosed choices:
Contributions are welcome at every milestone. The two LEMMAs and the strong law are self-contained and independent of the game.
Stable distributions were proposed as models of asset returns by Mandelbrot and Fama in the 1960s, because empirical returns show heavier tails than the normal law allows; Rachev and Mittnik's monograph Stable Paretian Models in Finance (2000) collects the later development. When the vector of per-share returns of assets follows a multivariate -stable law with , its distribution is determined by the stability index , a shift , and a finite Borel measure on the unit sphere, the spectral measure. The risk of a portfolio is then measured by the scale parameter of the return, and choosing an efficient portfolio becomes a deterministic optimization problem in .
In practice neither nor is known: both are estimated from data. Whether the optimal portfolio is robust to estimation error is therefore a practical question. Section 5 of Rachev and Römisch, Quantitative stability in stochastic programming: The method of probability metrics (Math. Oper. Res. 27(4), 2002; this mission follows the authors' preprint), answers it with an explicit modulus, as an application of the paper's general stability theory for stochastic programs under perturbations of the underlying probability measure.
Fix and equip with the Euclidean scalar product and norm .
For each there is such that
whenever and . The modulus is not fixed: it is whatever the growth of the unperturbed problem gives.
If is nonsingular, then (22) has a unique solution and for some and all sufficiently small .
The theorem bounds how far the optimal portfolios can move when the stability index and the spectral measure are both perturbed, with a modulus computed from the unperturbed problem alone. Combined with the companion, the efficient portfolio of a nonsingular spectral measure is unique and moves by at most . Since metrizes weak convergence on the compact sphere, any consistent estimator of in the weak topology, together with a consistent estimator of , yields consistent estimates of the optimal portfolio, and convergence rates for translate into rates for the portfolio. The paper notes (Example 5.3) that spectral measures of linear transformations of independent stable variables with a full-rank matrix are nonsingular, so the Hölder case covers the discrete spectral measures used in practice.
The result is proved in the paper; nothing here is open. To our knowledge none of it is machine-checked: Mathlib has strong convexity and the real power function but no stability theory of stochastic programs and no Fortet–Mourier metrics. The mission produces a checked proof of the result and a reusable formal treatment of the growth-function modulus in a concrete, fully explicit instance.
The obvious argument compares the optimal values of the two problems and concludes that a perturbed minimizer is nearly optimal for the unperturbed problem. Turning near-optimality into a distance bound requires the growth function and its generalized inverse; is defined by an infimum over a set that may be empty, and by a supremum that may be infinite, so this step has to be handled in extended arithmetic with care. A second difficulty is the term: the map must be shown to be -Lipschitz on the sphere uniformly over , which uses on the simplex. The change of exponent from to is controlled by a sharp calculus inequality whose constant needs . In the nonsingular case, the quadratic form must be shown to dominate , a compactness argument on the unit sphere of .
EuclideanSpace ℝ (Fin s) with coordinates indexed . The paper says "the (Euclidean) scalar product", so Euclidean norms are the paper's own.Metric.sphere 0 1. A spectral measure is a probability measure on with , and every integral is a set integral over . For the sphere is empty, no spectral measure exists, and every statement is vacuous, as in the paper.Metric.infEDist, to the empty set), and and take values in .Welcome contributions: the inequality on , strong convexity of on , and a general lemma converting a growth function and a uniform objective perturbation into a distance bound; the last is reusable for every stability result of the paper.
Many problems in statistics, signal processing and machine learning minimize the sum of a smooth function and a convex but nonsmooth one: -regularized least squares (the Lasso), bound-constrained problems, and group-sparse regression are standard examples. Tseng and Yun (Math. Program. Ser. B 117 (2009) 387–423) proposed the coordinate gradient descent (CGD) method for this class and proved that it converges linearly under a local Lipschitzian error bound, Assumption 2(a) of their paper. An assumption is only as useful as the list of problems known to satisfy it. Section 6 of the paper supplies that list, and this mission formalizes it.
Error bounds of this kind have a history in smooth constrained optimization. Luo and Tseng proved them for quadratic objectives over polyhedral sets (Luo–Tseng 1992, SIAM J. Optim.), for strongly convex functions composed with a linear map (Luo–Tseng 1992, SIAM J. Control Optim.), and for dual functionals of linearly constrained strictly convex programs (Luo–Tseng 1993, Math. Oper. Res.), and used them to derive linear rates for feasible descent methods (Luo–Tseng 1993, Ann. Oper. Res.). Tseng and Yun carry these results over to the nonsmooth problem (1) by reformulating it as a smooth problem over the epigraph of the nonsmooth part.
Throughout, carries the Euclidean norm . The problem is
where , is proper, convex and lower semicontinuous with effective domain , and is continuously differentiable on an open set containing .
The residual at is
the unique minimizer of a strongly convex function. A point is stationary if the one-sided directional derivative satisfies for every direction ; denotes the set of stationary points and the distance to it. A point is stationary exactly when its residual vanishes.
Assumption 2(a) asks that and that for every level there be constants with
Writing , problem (1) is equivalent to the smooth problem (41). Its projection residual at is the optimal solution of
is polyhedral if is the solution set of finitely many linear inequalities in ; is quadratic if with symmetric, not necessarily positive semidefinite. The four problem classes are:
Under C4, nonemptiness of is part of the conclusion. The constants are existential, so the goal does not depend on any particular estimate.
If is Lipschitz on with constant , there is depending only on with
If and C1, C2 or C3 holds, then for every there are with
where solves (42) with .
A further item, not a milestone, states the remark after Assumption 2 (p. 404) that Assumption 2(b) (stationary points with different objective values are uniformly separated) holds whenever is convex.
Theorem 4 is what makes the linear convergence theorem of the paper (Theorem 2, the subject of the second mission of this series) applicable. Through C1 it covers every problem with a quadratic and a polyhedral , including the Lasso and -regularized or bound-constrained quadratic programs, without convexity of . Through C2 it covers losses of the form with strongly convex, such as least squares , where itself is not strongly convex because may have a nontrivial kernel. These error bounds became a standard tool for linear rates of proximal and coordinate methods without strong convexity.
The paper's result is proved, but Lemma 7 is proved by citation: it applies three error bounds of Luo and Tseng to the reformulation (41). A complete formalization therefore requires those error bounds for smooth problems over polyhedral sets, which are not in Mathlib. To our knowledge none of the results of this mission has a machine-checked proof.
Lemma 6 and the C4 case of Theorem 4 are short inequality arguments. The difficulty is Lemma 7. The natural first idea, proving an error bound from strong convexity, fails for C1–C3: may be nonconvex (C1) or have a degenerate Hessian (C2, C3), and the objective of (41) is never strongly convex in . What replaces strong convexity is the polyhedral structure of , and the cited Luo–Tseng error bounds that exploit it are substantial results in their own right, each of which has to be established for a projection residual over a general polyhedron in .
is EuclideanSpace ℝ (Fin n), with indices . is the pair , its effective domain and its finite values there, with "proper, convex, lsc" given by the published ProxNewton.Inexact.IsProperClosedConvex. The value is never computed: every statement quantifies over , and membership in is x + d ∈ D ∧ P (x + d) ≤ ξ + δ. is a chosen minimizer of its subproblem, which at is the paper's unique one. The solutions of (42) enter through a predicate, and every bound is asserted for every optimal solution. Stationarity is the liminf form of . is the infimum distance. Assumption 2(a) quantifies over every real , which agrees with the paper's "" because the condition is vacuous below . In Lemma 6 the constant is quantified before the dimension and the data, so it depends on the Lipschitz constant only.
Explicit choices relative to the printed text:
A polyhedrality notion that admits only affine or constant , an Assumption 2(a) whose constants are chosen after , and a Lemma 7 whose residual is instead of the solution of (42) would all trivialize or change the statements. The encoding rules out each of them: polyhedral means a finite system of linear inequalities in , the constants precede , and Lemma 7 is stated for (42).
Welcome contributions: proofs of Lemma 6 and of the C4 case; Lipschitz continuity of polyhedral functions on their domain (Rockafellar–Wets, Example 9.35); the Luo–Tseng error bounds for affine variational inequalities and for composite strongly convex objectives over polyhedra, which can be reused well beyond this mission.
A backward stochastic equation determines its current value from a conditional expectation of future values. A forward equation determines its current value from past values. Coupling the two makes existence depend on more than integrability of the data: the feedback between the past and future can prevent a solution. Antonelli's 1993 paper studies this interaction in an space for equations driven by bounded variation processes, motivated in part by recursively defined stochastic utility in finance (Antonelli 1993, pp. 777–778).
The paper first gives an existence and uniqueness condition for a coupled system. It then tests the size of that condition with two examples. The first uses a singular coefficient matrix; the second, targeted here, uses a nonsingular linear coupling. This distinction matters because the failure of existence in the first example could otherwise be attributed to the singular matrix. The second example places the obstruction at a particular time horizon while retaining a linear map with Lipschitz constant one (Antonelli 1993, pp. 791–792).
Fix a complete probability space with a right-continuous filtration , where . At time , describes the information available. Let be an integrable, strictly positive, -measurable random variable. Let be a strictly positive, bounded, -measurable random variable. Both positivity statements are almost sure.
The unknowns are real-valued stochastic processes and . The forward equation starts from and accumulates :
The backward equation sets equal to the conditional mean, given current information, of a future integral and the terminal input:
These are equations (3.10)–(3.11) of the paper. Their coefficient functions are and , each with Lipschitz constant for the paper's sum norm on pairs. The associated linear coefficient matrix is nonsingular. A solution is sought in for each component: the expected time integral of its absolute value is finite, and the equations hold in that space. This is the same integrability regime used to state the coupled system in §3 (Antonelli 1993, p. 785).
The terminal value is the random variable . Conditional-expectation processes in the intermediate identities are denoted and . Jointly measurable versions are used when these processes appear inside time integrals.
For any positive horizon, the paper derives an equation for in terms of , a weighted future integral of , and . With the sign consistent with the preceding display, the identity is
The printed equation (3.12) places inside the negative conditional expectation. That is inconsistent with both the preceding display and the next closed form; the formal statement uses the consistent sign and records the discrepancy (Antonelli 1993, p. 792).
The remaining intermediate targets are the paper's closed form for , equation (3.13) for , and the terminal-mean relation:
The last identity is stated without division, so it also has meaning when . These identities give the milestones in the order they occur on p. 792.
At the specific horizon , the coupled equations have no solution:
Strict positivity makes the right side of the mean identity positive, while its left side vanishes. The statement is a nonexistence result for the same broad solution class as the paper, rather than a claim about a narrower pathwise class.
Example 2 shows that a nonsingular coupling can still lose existence at a finite horizon. Thus the obstruction exhibited by the earlier singular example is not explained by singularity alone. The example also marks a limitation of replacing the paper's smallness condition with the assumption that the Lipschitz constant is merely finite. At and , the product exceeds one, as the paper notes (Antonelli 1993, p. 791).
A completed formalization would connect conditional expectations, jointly measurable time-indexed versions, and integration in in a reusable Lean development. The paper proves the mathematical result. This mission asks for machine-checked statements and proofs of its intermediate identities and nonexistence conclusion; it does not claim that the result is an open mathematical problem.
The main challenge is that the equations are equalities of integrable processes, not pointwise equalities at every time and outcome. A value assigned to by an arbitrary representative of an class is uncontrolled, so the terminal value must instead be reconstructed from the forward integral. Conditional expectations are defined only up to almost-sure equality at each time, yet the subsequent formulas integrate their time-indexed versions. This requires a jointly measurable version and careful movement between almost-sure statements at fixed times and statements.
There is also a printed sign inconsistency in (3.12). Propagating that sign would contradict the later sine-cosine formula. Finally, the paper's quotient formula for cannot be used at , because its denominator vanishes there. The undivided mean identity is the meaningful target at the critical horizon.
Time is represented by , and all integrals over time use ; for Lebesgue measure this agrees with the paper's ordinary time integrals. The ambient probability measure is a probability measure, and the filtration satisfies right continuity and completion at time zero. The two unknown processes are jointly measurable and have finite lower-integral norms. A solution uses a jointly measurable version of the conditional-expectation process, with each conditional-expectation argument explicitly integrable. The terminal is defined from and , independently of an arbitrary endpoint value of .
The source calls and positive; the formalization reads this as strict positivity almost surely, because allowing both to vanish admits the zero solution. is integrable as required by the standing assumption on in §3; remains bounded as Example 2 states. The four intermediate identities are stated for general , while only the main result fixes . Their process equalities hold in , and the terminal identity holds almost surely. This keeps the target from becoming true simply because endpoint representatives can be chosen freely.
The needed development includes product measurability, conditional expectation, Fubini's theorem, time integration, and the trigonometric identities in the closed form. The and version definitions can be reused for other coupled systems with deterministic time integrators. Contributions that establish the intermediate identities under the stated integrability assumptions, or develop the corresponding measurable-version tools, support the goal directly.
The trust-region subproblem — minimizing a quadratic, possibly nonconvex, over a Euclidean ball — is the inner step of every trust-region method for nonlinear optimization, and it also appears in regularized least squares and in the analysis of quadratic constraints. It is one of the few nonconvex problems whose global minimizers are characterized exactly: by the classical results of Moré and Sorensen (1983) and Gay (1981), a feasible point is a global solution if and only if it satisfies the Kuhn–Tucker conditions with a multiplier that makes the shifted matrix positive semidefinite.
Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998)) solve the problem with DCA, a descent method for difference-of-convex programs. DCA converges to Kuhn–Tucker points, and a Kuhn–Tucker point need not be a global solution. Section 4.2 of the paper closes this gap: it tests a Kuhn–Tucker point for global optimality with one eigenvalue computation, and when the test fails it writes down, explicitly, a feasible point with strictly smaller objective value from which DCA can be restarted. The resulting algorithm GDCA alternates DCA runs and restarts. This mission formalizes that restart construction.
Let be a real symmetric matrix, and . Write for the Euclidean inner product and for its norm. The trust-region subproblem (Q1) is
A point is a Kuhn–Tucker point of (Q1) with multiplier when
In Lean, is EuclideanSpace ℝ (Fin n), is a self-adjoint continuous linear operator on it, is quad A b, and the four conditions are IsKKT A b r xs lamStar.
Let be an eigenpair of : and . If then
so is a direction of negative curvature of the shifted matrix. For a direction and , the restart step of (23) is the nonzero root of , so that lies on the sphere (Lean: restartGamma w xs r s, with a sign choosing between the two roots when ).
This is the "Summing up" claim of §4.2 (p. 493). It asserts only the existence of a better feasible point; the explicit construction is spread over the milestones.
A companion item records the paper's remark that, for , the root of (23) with the larger gives the smaller .
The restart claim turns a local method into a global one. Combined with the convergence of DCA to Kuhn–Tucker points (Theorem 4.1 of the paper) and the global-optimality characterization of (Q1), it shows that each DCA run either ends at a certified global solution or yields a feasible point that strictly improves on it, with the improvement given in closed form from one eigenvector. The construction is elementary, but its case analysis — the sign of , whether the constraint is active, whether the eigenvector is orthogonal to — is exactly where an informal argument can go wrong, and the printed (b.2) bounds contain two errors (see Formalization scope).
The result is proved in the paper; to our knowledge none of it has a machine-checked proof. The mission produces a checked version of the case analysis with the corrected constants, and reusable facts about quadratics on the Euclidean ball (Lemma 4.2, the step to the sphere along a negative-curvature direction) that apply to any trust-region method.
The obvious argument — move from along the negative-curvature eigenvector until the boundary is reached — fails in one case. When and , the line leaves the ball for every , so no step along is feasible. The paper repairs this by tilting towards , and the tilt must keep the curvature negative while making the direction non-orthogonal to ; the admissible range of the tilt depends on the signs of and . A second subtlety is that the identity needs the term of Lemma 4.2 to vanish, which uses complementarity when and when the constraint is active.
All statements live in namespace TaoAnDCA.Restart on EuclideanSpace ℝ (Fin n), with a continuous linear operator and symmetry the hypothesis IsSelfAdjoint A; throughout. The objective quad is the bare quadratic, with feasibility stated separately.
Conventions and disclosed deviations from the page:
A trivializing formalization is ruled out: the goal's hypothesis is the eigenvalue test , never " is not a global solution", which would make the conclusion a restatement of the hypothesis.
No infrastructure beyond Mathlib's inner product spaces is needed. Contributions welcome: proofs of the milestones, and of the goal from them.
In the periodic-review inventory model with lost sales, demand that cannot be met from stock is lost rather than backordered. With a positive order lead time the state of the system is a vector of length : on-hand stock plus the orders still in the pipeline. This model is standard in retail, where a customer facing an empty shelf buys elsewhere. Its optimal policy is not a base-stock policy and depends on the whole pipeline vector, which makes it much harder to analyse than the backorder model.
A basic question for any stochastic inventory model is how its optimal cost responds to uncertainty in demand. For the backorder model it is classical that more variable demand costs more (Song 1994). Zipkin's paper (Oper. Res. 56(4), 2008, 937–944) recasts the lost-sales model in a transformed state in which the optimal cost functions are L-convex. Its §5 uses this structure to prove the lost-sales analogue: if demand becomes more variable in the convex order, the optimal cost does not decrease. The paper presents this as new in the lost-sales setting.
Timeline of the structural results the mission rests on:
The order lead time is a positive integer . The cost factors are the unit procurement cost , the unit holding cost , the unit lost-sales penalty and the discount factor . Demands in different periods are independent and nonnegative, with a common law. The paper treats states and orders as continuous.
Transformed state. A state is a vector , where is the stock on hand plus all orders due to arrive or more periods hence, and by convention. So is the inventory position and is the stock on hand. The state space is
The action is , where is the order quantity, and is the all-ones vector. After demand , the next state is
Costs and recursion. The end-of-period holding and penalty cost is , and its expectation given on-hand stock is . The optimal cost functions satisfy
with . This is the paper's recursion (1)–(2), written in the state .
Program (4). Fix a demand . Choosing the next stock level , with and , gives
Here is the leftover stock and the unmet demand.
Parametric demand. The demand depends on a real parameter , with law , and is the optimal cost under . A random variable is smaller than in the convex order if for every convex for which both expectations exist. This forces equal means and a variance that does not decrease.
If is increasing in with respect to the convex order, then for all and all ,
Theorem 11 is a comparative-statics statement: replacing demand by a mean-preserving spread cannot lower the optimal cost from any starting state, at any horizon. It justifies valuing variance reduction in lost-sales systems, for example forecasting or demand pooling, without solving the high-dimensional dynamic program. The induction pattern of the proof transfers to other parametric questions about the model; §6 of the paper notes that the parametric analysis remains valid in several extensions.
The paper proves Theorem 11 in a few lines on top of Theorem 4. No machine-checked proof of the result or of its structural prerequisites is known: neither the lost-sales recursion in the transformed state nor its convexity is formalized. A complete development checks the measure-theoretic steps the paper leaves implicit: that the optimal costs are finite, the existence of the expectations, and the passage from convexity in on to the convex order's test functions on .
The argument looks immediate: the costs are convex, so the convex order should apply directly. It does not. The function to which the convex order must be applied is the end-of-period cost as a function of demand. In recursion (1) that function is , where the next state depends on through the kink . Convexity of alone does not make this composition convex in . The paper avoids the issue by passing to program (4), where the amount of demand filled is a decision. That requires two facts: that selling as much as possible is optimal (milestone 1), and that the program is jointly convex in state, action and demand (milestone 3), which needs convexity of on all of (milestone 2). A second difficulty is analytic: the optimal costs are defined by infima and expectations, and one must show that these are finite and integrable before any order comparison applies.
Fin L → ℝ with 0-based indices matching the paper. is the helper vext. is the set of antitone, nonnegative vectors.fbar … (μ φ) k v.StochasticOrders.Convex.ConvexOrder (Shaked–Shanthikumar (3.A.1)), applied to the identity on . Equal means are a consequence and are not assumed.Ruled out. Value functions that collapse to a junk constant would make Theorem 11 trivially true. This is excluded because the recursion is defined, not assumed, and every cost and demand hypothesis is imposed for every . Replacing the convex order by "variance nondecreasing", by the increasing convex order, or by test functions convex only on changes the theorem and is not accepted.
Infrastructure and contributions. A complete development needs:
The model file is shared in shape with the series' missions 1 (L-convexity) and 2 (policy bounds), and its convexity lemmas are reusable for other parametric comparisons of the lost-sales model. Proofs of any milestone, and alternative arguments that bypass program (4), are welcome.