Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Sums of independent random matrices appear wherever a large matrix is built from random pieces: sample covariance matrices in statistics, random sparsification and sampling in numerical linear algebra, random graphs and their Laplacians, and compressed sensing. The basic question is how far the largest eigenvalue of such a sum can stray above its typical value. For sums of independent real random variables the answer is given by the classical inequalities of Chernoff, Hoeffding and Bernstein, all derived by the Laplace transform method: bound the tail by the moment generating function, and use independence to factor the moment generating function of the sum.
Ahlswede and Winter (2002) showed that a matrix analogue of the Laplace transform method exists, and Oliveira (2010) refined the starting inequality. Tropp's paper (arXiv:1004.4389) replaced the Ahlswede–Winter decoupling step by a consequence of Lieb's concavity theorem (Lieb 1973) and obtained a single master tail bound from which matrix versions of the Gaussian-series, Chernoff, Bernstein and Azuma inequalities follow with sharp variance parameters. This mission formalizes that master bound, the first of five missions covering the paper.
Timeline:
All matrices are arrays of complex numbers with . A matrix is self-adjoint (Hermitian) when ; it then has real eigenvalues, and denotes the largest one. For a function and a self-adjoint with unitary and diagonal, . This defines the matrix exponential of every self-adjoint matrix and the matrix logarithm of every positive-definite matrix, with . The trace exponential is .
A random self-adjoint matrix is a measurable map from a probability space to the self-adjoint matrices. Its expectation is the matrix of the expectations of its entries. A finite sequence is independent when the maps are jointly independent. The matrix moment generating function and matrix cumulant generating function of are
which may fail to exist for some . In the Lean development these objects are lambdaMax, mexp, mlog, trExp and mean in the namespace MatrixTail.Master.
For independent random self-adjoint matrices and every ,
It contains no constants and no assumption beyond independence: every later inequality of the paper specializes it.
The master bound reduces every tail estimate for of an independent sum to semidefinite bounds on the individual cumulant generating functions. The paper's matrix Gaussian and Rademacher series bound, matrix Chernoff inequality and matrix Bernstein inequality are each one such bound away from it, and the matrix Bernstein inequality in particular is a standard tool in randomized numerical linear algebra, matrix completion and covariance estimation. Missions II–IV of this series take the master bound as their first milestone.
All results here are proved in the literature. What remains is formalization: none of Lieb's concavity theorem, the matrix Laplace transform bound or the subadditivity of matrix cumulant generating functions is in Mathlib, and a machine-checked Lieb theorem would be reusable throughout quantum information theory (strong subadditivity of entropy, joint convexity of relative entropy).
The scalar argument factors , which needs . For non-commuting matrices , so this step fails. The Golden–Thompson inequality handles two summands but its three-matrix analogue is false, so it does not iterate. Lieb's concavity theorem is the deep input; it does not follow from elementary properties of the exponential, which is neither operator monotone nor operator convex. On the formal side, the matrix functional calculus of Mathlib carries little of the trace-function theory the statements rely on.
Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d] wherever appears; for the largest eigenvalue would be and the bound would fail at . Exponential and logarithm are Mathlib's continuous functional calculus cfc. Random matrices are measurable maps for the Borel σ-algebra on the entries, independence is iIndepFun, and P is a probability measure. Expectation is entrywise.
The paper's standing assumption that expectations exist is made explicit and only where an expectation is taken: every entry of is integrable for the in question. The infimum over is stated as the bound for every at which the moment generating functions exist; since an inequality is equivalent to for every , and the paper treats a non-existent moment generating function as , this is exact. A real-valued infimum over , or dropping the integrability hypotheses, would make the statements trivially true through Lean's default values ( of an unbounded set and the integral of a non-integrable function are ); the formalization rules both out.
Useful infrastructure beyond this mission: trace inequalities for cfc on Hermitian matrices, monotonicity of the trace exponential in the semidefinite order, and Lieb's concavity theorem itself. Contributions of any of these as standalone lemmas are welcome.
Many problems in signal processing, statistics and machine learning ask for a minimizer of a smooth loss among vectors with few nonzero entries: compressed sensing with a nonlinear measurement model, sparse regression with a non-quadratic loss, sparse phase retrieval. The common abstraction is the sparsity constrained problem
where is continuously differentiable but not necessarily convex. The constraint set is a finite union of linear subspaces, so (P) is nonconvex and in general NP-hard, and its solutions are not characterized by the classical KKT theory.
Beck and Eldar (SIAM J. Optim. 2013, arXiv:1203.4580) introduced a hierarchy of necessary optimality conditions for (P) and matched each condition with an algorithm whose limit points satisfy it. Iterative hard thresholding (Blumensath and Davies 2008) reaches -stationarity for ; the greedy sparse-simplex method reaches coordinate-wise minimality, but each of its iterations calls up to one-dimensional minimizations. This mission formalizes the paper's compromise between the two: the partial sparse-simplex method, which examines only two candidate moves per saturated iteration, and whose limit points are -stationary.
Vectors live in with the Euclidean norm; is the -th unit vector. For :
The objective is continuously differentiable and bounded below (Assumption 1, standing throughout the paper). Assumption 2 asks that be Lipschitz with some constant . A constant satisfies the local Lipschitz condition (2.15) if for every pair , every and every supported in ,
The paper's local Lipschitz constant satisfies it, and .
The projection is the set of points of nearest to . For , a point is an -stationary point (Definition 2.3) if
The partial sparse-simplex method (p. 25) starts at . If , it moves to the best point over all and if that strictly decreases , and stops otherwise. If , it compares two candidates and takes the better one, preferring the second on ties:
Under Assumption 2, with satisfying (2.15), every accumulation point of a sequence generated by the partial sparse-simplex method satisfies
that is, is an -stationary point.
The theorem shows that a cheap index-selection rule does not cost optimality strength relative to iterative hard thresholding: every limit point satisfies , and since , this is a stronger necessary condition than the guaranteed by IHT with stepsize . In the paper's numerical comparison (Example 3.3 contd., Table 3) the method performs much better than IHT and only slightly worse than the greedy method, at a fraction of the greedy method's cost per iteration. The decrease estimates of Lemma 4.1 are the quantitative content: they turn each iteration into a lower bound on the objective decrease in terms of the violation of -stationarity.
The results are proved in the paper; to our knowledge none is machine-checked. This mission produces a formal model of the method (with its selection rules as inequality predicates, so every run is covered), the local descent lemma for two-sparse directions, and a checked proof of Theorem 3.4. The printed proof of the case contains two gaps (see Difficulty); a formal proof settles the argument.
The decrease estimates follow from the local descent lemma applied at well-chosen trial points, but passing to the limit is delicate. When , the supports of the subsequence eventually coincide with and becomes continuous there; when , the iterates along the subsequence may still have nonzeros, and does not by itself force , because kills the second term of . The swap move optimizes along a single off-support coordinate , chosen by the derivative at and not at the shifted point where the optimization happens. The printed display (4.19) claims the bound for the maximum over all of at the shifted point, which the argument does not give, and the final display takes a minimum of two bounds that each hold on only one class of indices. Theorem 3.4 itself is not affected, but a complete proof cannot follow those two displays as printed.
Lean works in EuclideanSpace ℝ (Fin n) (indices ), with of class and = gradient f. Conventions fixed by the formalization:
LipschitzWith Lf (gradient f)) are hypotheses.MapClusterPt xstar atTop x.The run predicate is satisfiable and does not force a STOP: on , , , the constant sequence at is a run. The conclusion is the projection condition itself, not the coordinate form (2.5), so it cannot be met by an empty or degenerate reading of stationarity.
Reusable parts: the local descent lemma for two-sparse directions, Lemma 2.2 (the coordinate characterization of , shared with the IHT mission of this series), and the order statistic . Contributions of proofs for any milestone are welcome, as is the companion result Lemma 3.3 (limit points are BF vectors without Assumption 2).
Stochastic gradient descent (SGD) is the standard method for minimizing an expected loss when only noisy gradients are available: in machine learning, is a predictor, a random example, and each step uses the gradient of the loss on one fresh example. When is strongly convex, as for regularized learning problems such as the SVM, the minimax-optimal error after oracle calls is of order . Rakhlin, Shamir and Sridharan (arXiv:1109.5647, ICML 2012) asked whether plain SGD attains this rate, or whether the bound known for averaged SGD is the truth.
Their §3 settles the case where is in addition smooth at its minimizer: both the last iterate and the average of all iterates attain , with explicit constants. This mission formalizes that section.
Timeline of the relevant bounds:
Let be a closed convex set containing , let , and let be a probability distribution on a measurable space .
Projected SGD with step sizes starts at , draws independently and sets
where is the Euclidean projection onto . The averaged iterate is . In Lean the run is UnderstandingML.sgdStrongIterates lam W g S and the average UnderstandingML.sgdStrongAverage lam W g S, for a sample S : Fin T → Z drawn from UnderstandingML.iidLaw D T.
If is -strongly convex and -smooth with respect to , then for every
The constants are the paper's. Theorem 1 is a companion of the goal rather than a step of its proof; both rest on Lemma 1.
The result. Theorem 2 shows that the factor in the standard bound for averaged SGD is not needed when grows at most quadratically away from its minimizer. Condition (2) holds for logistic and least-squares regression and, in general, for linear predictors with losses that have Lipschitz-continuous gradients. Together with the paper's Theorem 4, which shows that the factor is unavoidable for averaged SGD on some non-smooth problems, it locates where the extra logarithm comes from. Lemma 1 is the paper's key lemma: an bound on the expected squared distance of the last iterate that needs no smoothness, and it is reused in the paper's suffix-averaging analysis.
Formalizing it. All results are proved in the paper; none is formalized. The platform has UnderstandingML.sgd_strongly_convex (Shalev-Shwartz and Ben-David, Theorem 14.11), the classical bound for the same averaged iterate without smoothness. This mission adds the bounds under (2), on the same SGD run, together with a reusable expected-distance bound for the projected iterates.
The obvious route to Theorem 2 is to apply smoothness to each iterate, use Lemma 1, and average: by Jensen, , which is of order . Removing the logarithm requires controlling directly, where the iterates are dependent and the cross terms do not vanish. The resulting recursion is nonlinear in , and an induction with the constant fails at its first step unless the base case uses the sharper bound of Lemma 2. On the formal side, the expectations are over the product of independent samples, and each one-step argument needs the independence of from and the measurability of the projected iterates.
UnderstandingML.Vec d).Convex ℝ W, IsClosed W (so the projection exists; tacit in the paper) and 0 ∈ W (the paper's initialization).StrongConvexOn W lam F with 0 < lam. Combined with relative subgradients, it gives (1).OptimalSGD.Suffix.IsSubgradientOracleOn W F D g (the series' shared oracle predicate): for , g w is integrable and its mean is a subgradient of at relative to . Measurable (Function.uncurry g) and a probability measure are assumed. The second-moment bound holds at every , which is the paper's "regardless of how the iterates evolve".IsSmoothWrt W F μ wstar), with . It is not a Lipschitz-gradient assumption, and need not be differentiable.sgdStrongIterates lam W g S (T - 1), and averages indices . Statements quantify over , including ().A statement whose Bochner integral is not shown to be integrable would hold vacuously, because non-integrable functions integrate to ; the integrability conjuncts rule this out. The run and the average are the published Understanding Machine Learning definitions, so the bounds here apply to the same object as UnderstandingML.sgd_strongly_convex.
Needed infrastructure: measurability of the projected iterates in the sample, independence of from under the product measure, conditional unbiasedness of the oracle along the run, non-expansiveness of the projection (available as UnderstandingML.projection_lemma), and an elementary induction on the scalar recursions. Contributions of these as standalone lemmas are welcome, and they are reusable for mission 1 of this series (suffix averaging) and for other projected-SGD analyses.
Karmarkar's projective method (1984) was the first interior-point algorithm for linear programming with a polynomial bound that was also fast in practice. Its analysis rests on a potential function that combines the logarithm of the objective gap with a logarithmic barrier: if every iteration lowers the potential by a fixed constant, then the gap shrinks geometrically. Nesterov and Nemirovskii (1994, §4.3) carried the method over to general convex cones with self-concordant barriers, but only with short steps, which move a fraction of the way to the boundary of a ball in the local norm.
Nesterov and Todd (1997) introduced self-scaled barriers, the class behind the cones of linear, second-order cone and semidefinite programming. They used it to allow long steps, which go a large fraction of the way to the boundary of the cone itself. Section 7.1 of that paper analyses the Karmarkar method with long steps on a self-scaled cone. It shows that the potential decrease per iteration is at least the absolute constant , independent of the barrier parameter, as in the linear-programming case. This mission formalizes that analysis.
Timeline:
Let with inner product , which identifies the dual space with . Let be a closed convex cone with nonempty interior that contains no line, and let be its dual cone. A -self-scaled barrier is a self-concordant barrier that is logarithmically homogeneous, , and satisfies the two scaling conditions of Definition 2.1 of the paper. and are its gradient and Hessian.
Two measures of a direction at are used:
The point stays in exactly when .
The problem is in Karmarkar form:
with linear and surjective and . Its dual is . The standing assumptions are that (P) and the dual have strictly feasible points, and that is not constant on the feasible set of (P). The optimal value is . The method decreases the potential
which is homogeneous of degree in .
One iteration starts from a strictly feasible and a lower bound :
For a suitable , the point lies in and
The goal asserts the existence of the step, not a particular step size, so it does not commit to the step chosen in the proof.
With and the minimum of over it: if with and large enough, then
Theorem 7.2 together with Theorem 7.1 gives the iteration bound of the long-step conic Karmarkar method. The decrease constant does not depend on or on the cone. The finer bound can be much larger than , since always holds. This explains why long steps outperform short ones in practice. Lemma 7.1 shows that the lower bound obtained from dual information is valid and tight enough to drive the analysis. The paper presents it as a generalization of a result of Anstreicher (1986) for standard linear programming.
The results are proved in the paper; none of them is formalized anywhere. A formal development checks the interplay of the lower-bound update with the σ-measure and the homogeneity of , which the paper treats briefly. It also records a correction: on p. 27 the paper prints (and likewise ). The paper's own surrounding identities, in particular on p. 28, require the sign "", and the formalization uses "".
The obvious argument bounds the change of along with self-concordance in the local norm. That argument only controls steps with , and it gives a decrease that degrades with the step length. The long step goes up to , which can be much larger. Reaching it requires the long-step barrier bound for self-scaled barriers (Theorem 4.2 of the paper, stated in another mission of this series). That bound controls through instead of .
The second obstacle is the linear term. The decrease in must be compared with , which needs both the identity (7.8) and the gap bound (7.7). The gap bound is the step at which the lower-bound update is essential: without the update, is not bounded by .
The Lean development reuses the published self-scaled setting of the series SelfScaledIPM (IsProperCone, IsSelfScaledBarrier, hess, lnorm, sigma, absn) and ConvexOptimization.dualCone. Conventions:
EuclideanSpace ℝ (Fin n), with identified with .A statement with an arbitrary real, or with an arbitrary vector, would be false or vacuous. The statements here fix both by the page's construction (7.3)–(7.6), and the logarithm in is guarded by the positivity conjunct.
A proof needs the long-step barrier inequality (Theorem 4.2), the monotonicity facts of Proposition 4.1, (Theorem 3.1 (iii)), and (Proposition 6.2). These are milestones of the other missions of this series, and contributions proving them are reusable here. Elementary facts about (positive homogeneity, the boundary characterization at ) are useful beyond this mission.
Potential-reduction methods solve a linear or conic program by driving down a single merit function that combines the objective gap with a barrier for the constraint cone. For linear programming the primal version goes back to Karmarkar (1984) and, without Karmarkar's special problem form, to Gonzaga (1990, Math. Programming 49, 7–21), whose method reduces the potential by a constant at every step while updating a lower bound on the optimal value. Nesterov and Nemirovskii (1994) extended such methods to general convex cones with self-concordant barriers, but their analysis only allows short steps: steps confined to a ball of the local norm, which in practice is a small fraction of the way to the boundary.
Nesterov and Todd (1997) singled out the self-scaled cones (the nonnegative orthant, the second-order cone, the cone of positive semidefinite matrices, and their products) and showed that for them long steps are admissible. This mission formalizes their extension of Gonzaga's method (§7.2 of the paper): a primal potential-reduction step, with a lower-bound update, that decreases the potential by a constant and, when the potential parameter is large enough, by an amount that scales with how far the step can go.
Let with its inner product, identified with its dual . Let be a closed convex pointed cone with nonempty interior, and a -self-scaled barrier for : a -self-concordant logarithmically homogeneous barrier () such that for all the Hessian satisfies and , where is the dual cone and the conjugate barrier. Here .
The problem is
with linear and surjective, and dual : s.t. , . Both have strictly feasible points: and are nonempty, and the objective is not constant on the feasible region of . Let be the optimal value.
At the local norm is , its dual is , and measures how far one can move from along : the point stays in for . The uniform norm is .
For and a lower bound , the primal potential is
At an iterate with lower bound , let and be the projections of and of into with respect to : , . For put . Whenever , the number is the value of a feasible dual solution, hence a lower bound on . The updated lower bound is the larger of and the best such bound. Finally and the search direction is , which is times the projected gradient of . Write .
If , there is with and
If , there is with and
A total potential decrease from the starting pair forces , where is the minimum of on a bounded truncation of the homogenized feasible region.
Theorem 7.4 together with Theorem 7.3 gives an -iteration method for conic programming over self-scaled cones that needs only a primal strictly feasible point and a lower bound, and that, for , matches the complexity of the short-step theory. Part (b) is the substantive claim: the step may go a large fraction of the way to the boundary of (half way when ) and the guaranteed decrease is typically much larger than . This is the property that distinguishes self-scaled barriers from general self-concordant ones, for which only steps inside the local unit ball are controlled.
The results are proved in the paper. None of them, nor the long-step theory of self-scaled barriers on which they rest, is formalized in any proof assistant as far as is known.
The obvious approach bounds by the self-concordance inequality, which controls only for ; that is the short-step regime and yields at best part (a). Part (b) requires a bound on along valid all the way to , which holds for self-scaled barriers but not for self-concordant ones. The second difficulty is the interplay with the lower-bound update: the decrease of the barrier term must be paid for by the decrease of , and this needs the scaling factor of the direction to be at most , which in turn depends on how was chosen. With an arbitrary admissible lower bound the claim fails.
, are EuclideanSpace ℝ (Fin n) identified through the inner product, and the problem data are surjective, , . The cone, the barrier, the local norms (lnorm), (dnorm), (sigma) and (absn) are the published definitions of the SelfScaledIPM.ShortStep setting; the paper's starred dual norms map to dnorm at a primal point. Nondegeneracy of is part of that barrier definition, and the conjugate barrier is an sSup over .
Standing assumptions are hypotheses of every statement: surjectivity of (6.1), strict dual feasibility (6.3) (strict primal feasibility follows from the given iterate), the objective not constant on the feasible region, and . The optimal value is the infimum of the objective over the feasible set, finite under these assumptions. The projections (7.12) are given as data satisfying their defining equations. The updated lower bound is defined as , with the set of dual bounds over with , and when is empty. Because the gap is nondecreasing in , this equals the paper's value at the minimal admissible . "A suitable value of " is an existential over , and the conclusion also asserts so that the logarithm in is genuine. and of Theorem 7.3 are defined explicitly, with the infimum of over .
A statement in which is an arbitrary lower bound above , or an arbitrary vector in , or arbitrary instead of existentially chosen, would be false; the formalization fixes by (7.17) and by (7.14).
A complete development needs the theory of self-scaled barriers along a line (Theorem 4.2 and Proposition 4.1 of the paper, posed in the sibling mission I of this series), the projection identities (Propositions 6.2–6.3, posed in mission IV), weak conic duality, and the inequalities and . These are reusable across self-scaled interior-point methods; proofs of any of them are welcome.
Interior-point methods solve linear, second-order cone and semidefinite programs by following a smooth curve through the interior of the feasible region. Nesterov and Nemirovskii (1994) showed that the right object to build such methods on is a self-concordant barrier for the cone, and that the number of Newton steps needed by a path-following method is governed by the barrier parameter . For general cones, however, their analysis of Newton's method only controls a small neighbourhood of the path, so the step in the path parameter must be short.
Nesterov and Todd (1997) singled out the cones that admit a self-scaled barrier: the nonnegative orthant, the second-order cone, the cone of positive semidefinite matrices and their products. For these cones the barrier satisfies global, long-range inequalities that general self-concordant barriers do not. Section 9 of the paper uses them to sharpen the classical primal path-following method: Newton's method converges quadratically on the whole region where the proximity measure is below (extending Roos and Vial, 1992), and a predictor-corrector scheme takes a tangent step whose length adapts to the geometry of the cone at the current point.
Let with its Euclidean inner product ; the dual space is identified with . Let be a proper cone: closed, convex, containing no line, with nonempty interior . A function is a -self-scaled barrier for if it is a -self-concordant logarithmically homogeneous barrier () and, for all , and , where is the conjugate barrier (Definition 2.1). Then .
At a point the paper uses three measures of a vector :
The problem is with surjective; is the set of strictly feasible points, and the dual problem is assumed strictly feasible. For and the system
defines the projection of into with respect to .
For the penalty function is ; its minimizers over form the central path. The Newton direction is the projection of with respect to , and the proximity measure is . The tangent direction is the projection of with respect to .
One iteration of the path-following scheme (p. 39) from with is:
For one iteration of the scheme, with :
By induction from , the condition (9.3) holds at every iterate and grows geometrically.
A companion item, Theorem 9.1, states the decrease of along the damped Newton step .
Theorem 9.3 shows that the primal path-following method for self-scaled cones increases the penalty parameter by a factor at least per iteration, which yields the iteration bound, and that the step can be much longer when the ratio is large. The paper notes that this ratio is the maximal step along the normalized tangent direction that keeps in , so the rule is a "large-step" rule in disguise. Theorem 9.2 removes the restriction of the general self-concordant theory, where quadratic convergence of Newton's method is only shown on a smaller neighbourhood, by allowing any point with .
The milestones are general tools for self-scaled barriers. Theorem 4.3 is a global second-order estimate for the gradient, with no restriction on the distance between the two points; Corollary 3.1 is an exact mean-value identity with a single interior intermediate point; Propositions 6.2 and 6.3 are the basic facts about the projections that every algorithm of the paper computes.
None of these results has a machine-checked proof that we know of. The platform has general self-concordant Newton estimates (the contraction and the damped Newton decrease ), which use different measures and do not involve , or the constraint .
The obvious route to Theorem 9.2 is the standard self-concordance argument, which compares at the new point with through the local norm alone. It gives , which is weaker than the claimed bound and gives nothing near . The sharper bound needs estimates that hold only for self-scaled barriers: a second-order remainder for the gradient measured at the new point and controlled by the uniform norm (Theorem 4.3), which in turn requires the intermediate point of Corollary 3.1 and the two-sided Hessian comparison of Corollary 4.1 (iii). These fail for general self-concordant barriers, and they depend on the structure theory of §3 (Theorem 3.2 of the paper).
In Theorem 9.3 the predictor step is long in the local norm, so no estimate based on alone keeps the predictor point close enough to the central path for one corrector step to restore ; the constant in is fixed by the page and leaves little slack.
The development reuses the published setting of the 1998 Nesterov–Todd series: IsProperCone, IsSelfScaledBarrier, hess, IsPrimalStrict, IsDualStrict, lnorm (), dnorm (), sigma and absn. Its conventions are:
The paper stars dual norms; the 1998 modules do not, so dnorm F x is the paper's .
New definitions are the projection system (6.4) (IsProjection), the penalty , the Newton and tangent systems as predicates on their solutions, and the step size . Solutions of linear systems are always data satisfying these predicates, never chosen by a function. Operator inequalities are written through quadratic forms.
Every theorem of §9 assumes (6.1)–(6.3) ( surjective, a strictly feasible dual point), which the paper states on p. 38. Theorems 9.2 and 9.3 are stated for one iteration and state explicitly that the new points are interior, which the scheme presupposes. Theorem 9.3 assumes : when lies in the range of the objective is constant on the feasible set and is undefined. In Theorem 9.1 the middle bound of (9.1), which divides by , is stated under , and the outer bound in all cases.
A formalization that leaves as a free positive parameter, drops the corrector step, or treats as any number at most that is not tied to the Newton system at the new point would state a different, weaker or vacuous theorem. The goal fixes by the formula of p. 39 and bounds for every solution of the Newton system at .
Contributions welcome: proofs of the milestones, the structure results they rest on (existence of the scaling point, Theorem 3.2; the Hessian bounds of Theorem 4.1), and reusable lemmas on and the uniform norm, which also serve the other missions of this series.
Transient stability of a power grid asks whether the generators of the network return to synchronous operation after a large disturbance such as a fault or a line trip. In the classical network-reduced model the rotor angles obey second-order swing equations, and stability certificates usually come from energy functions evaluated numerically. Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012) relate this problem to a first-order system of coupled phase oscillators, the non-uniform Kuramoto model, and derive purely algebraic conditions on the network parameters under which the oscillators synchronize. Such conditions read as "the network connectivity dominates non-uniformity, losses and lack of phase cohesiveness" and are checked from the data alone, without simulation.
The paper gives two such sufficient conditions. This mission formalizes the second, Theorem V.5, which measures connectivity by the algebraic connectivity of the lossless coupling and therefore applies to sparse (connected, not necessarily complete) networks. A companion mission treats Theorem V.3, the condition for complete graphs.
Timeline. For the classical Kuramoto model, Jadbabaie, Motee and Barahona (ACC, 2004) and Chopra and Spong (IEEE TAC, 2009) analysed synchronization with the Lyapunov function , and Chopra and Spong proved frequency synchronization under cohesive phases. Dörfler and Bullo (2009–2012) extended the analysis to non-uniform time constants , phase shifts and non-complete graphs, using a weighted Lyapunov function.
There are oscillators with phases , time constants , natural frequencies , coupling weights and phase shifts (), with . The non-uniform Kuramoto model is
In this mission , and its non-zero entries induce a connected graph.
If , then
Lemma V.8 (the identity (36) that replaces by ), Lemma V.9 (a quadratic-form bound by ), the sinc estimate and the bound on the lossy coupling (p. 25), the Lyapunov-derivative bound (37), the sandwich bounds (39) on , the existence and uniqueness of from the analysis of (41), and the eventual entry of every trajectory into .
The condition is checkable from network data: of a weighted Laplacian, two vector norms and the extreme time constants. It applies to sparse networks, where the complete-graph condition of Theorem V.3 does not, and specializes for classical Kuramoto oscillators to (Remark V.7). Through the singular-perturbation argument of Section IV, conditions of this kind certify transient stability of the network-reduced power system.
The result is proved in the paper; no machine-checked version is known. A formalization fixes several points the printed text leaves loose: the norm is written on p. 23 with a double sum that counts each pair twice; the chain defining on p. 25 is printed with its inequalities reversed; and "reaches " holds only asymptotically. The formal statements make each of these precise.
The obvious Lyapunov function, , has a sign-indefinite derivative as soon as the differ, because the coupling is not symmetric. The weighted function restores a symmetric structure, but only through the non-obvious identity (36). After that, the sinusoidal coupling has to be bounded below by a quadratic form on a set where the phase differences stay below , the lossy coupling has to be bounded above uniformly in the state, and the resulting ultimate-boundedness argument has to be run with sublevel sets of , which are ellipsoids rather than balls of unless all coincide. The constants , , come from this mismatch, and the passage from sublevel sets back to balls is the most delicate step.
The prophet inequality of optimal stopping compares a gambler, who sees independent non-negative random values one at a time and must accept or reject each on arrival, with a prophet who sees them all in advance. Krengel, Sucheston and Garling showed that the gambler can secure , and Samuel-Cahn showed that a single threshold suffices. Since Hajiaghayi, Kleinberg and Sandholm (2007) and Chawla, Hartline, Malec and Sivan (2010), prophet inequalities have served as the approximation guarantees of sequential posted-price mechanisms: an online selection rule with a prophet guarantee turns into a truthful mechanism with a revenue guarantee.
The natural multi-choice generalization lets the gambler accept a set of elements, subject to a feasibility constraint. Kleinberg and Weinberg, Matroid Prophet Inequalities (STOC 2012, arXiv:1201.4764), proved that when the feasible sets are the independent sets of a matroid, the factor is still achievable, by an explicit threshold rule, and even when the order of arrival is chosen adaptively by an adversary.
Timeline:
Let be a finite ground set and a matroid; is its family of independent sets. For each a distribution on is given; the weights are independent with , and . Let and .
An online weight-adaptive adversary reveals the elements one at a time: it picks knowing but not . An online algorithm maintains a selected set and, when arrives with its weight, irrevocably accepts or rejects it, keeping independent. A threshold rule offers a threshold computed from the revealed prefix (and when ) and accepts iff .
The algorithm of the paper uses a ghost sample: an independent copy of the weights. Let be a -maximum-weight basis. For an independent set , among the partitions with and a basis, , denote one maximizing . The algorithm (9) sets
For every matroid on a finite ground set, every family of distributions on with finite means, and every online weight-adaptive adversary, the set selected by the algorithm (9) satisfies
The goal is stated for the paper's own algorithm, which is stronger than the existence statement of §3.
earns . 2. The identity behind (9) = (10), and the telescoping identity (Property (2) for ). 3. Lemma 1 (bijective basis exchange, and its weighted form), Lemma 2 ( is a maximum-weight basis of the contraction ), Lemma 3 ( is submodular on subsets of an independent set). 4. Inequalities (11) and (12), and Proposition 2:
pointwise in ; then Property (3) with for the thresholds (9).
The theorem gives the optimal constant: already for a rank-one matroid (choose one element) no online algorithm beats . It covers every matroid with one algorithm, including uniform, partition, graphic and transversal matroids, which model capacity, unit-demand and spanning-tree constraints. Through the reduction of Chawla et al., the paper derives from it order-oblivious posted-price mechanisms that are 2-approximations to the optimal revenue in single-parameter settings with matroid feasibility and, through the adaptive adversary, in multi-dimensional unit-demand settings (§6 of the paper). The decomposition through -balanced thresholds is reused in the paper for intersections of matroids, with factor .
The result has been proved since 2012; it has not been formalized. The mission produces a machine-checked development of the model (online adaptive adversaries, threshold rules, the ghost-sample expectations), of the general reduction (Proposition 1), and of the matroid facts the algorithm relies on, notably the bijective exchange lemma (Schrijver, Corollary 39.12a), which is not in Mathlib.
The obvious argument fixes the order of arrival and compares the algorithm with the prophet item by item. It fails here because the order is chosen adaptively from the revealed weights, so the set of elements still to come is random and correlated with the past. The proof must instead compare the algorithm's realized selection with a ghost optimum built from an independent sample, and bound the value the algorithm forgoes by the value the ghost optimum could still add, . The step that needs matroid structure is Property (3): the total threshold offered to any set that could still be added must be at most half of . The thresholds were computed along the history , not at the final , so the bound requires the submodularity of (Lemma 3) and a weight-dominating exchange between and in the contraction . Neither holds for general downward-closed families.
Fintype α; the matroid is Mathlib's Matroid α with ground set Set.univ; sets are Finset α; contraction is Matroid.contract.F : α → Measure ℝ, probability measures with F x (Set.Iio 0) = 0 (support in ) and Integrable id (F x) (finite means). The weight law is Measure.pi F, and every expectation is a Bochner integral over it. Finite means make , and the integrands of the thresholds integrable, so no expectation is a junk value.The goal fixes the thresholds by (9) through , and the ghost expectation; a statement in which the thresholds are free parameters assumed to satisfy (2)–(3) would be Proposition 1 and is not the goal.
Contributions are welcome at every level: the measurability of the online run, the exchange lemma for Mathlib matroids, the greedy characterization of maximum-weight bases of a contraction, and the probabilistic core (7) of Proposition 1. The matroid lemmas are reusable beyond this mission, in particular by the matroid-intersection mission of the same paper.
Fourier analysis of functions on the discrete cube is the main tool behind tight inapproximability results under the Unique Games Conjecture. In the MAX-CUT reduction of Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 2007), soundness rests on the Majority Is Stablest theorem: among bounded functions in which no coordinate has large influence, the majority function is asymptotically the most noise stable. That theorem was a conjecture when the paper was written and was proved by Mossel, O'Donnell and Oleszkiewicz (Annals of Math. 2010) using an invariance principle.
Section 6.2 of the paper records special cases of Majority Is Stablest that have short, self-contained proofs. Theorem 6 is the case where the noise parameter tends to . There the noise stability is dominated by the Fourier weight at level 1, and the statement says that a bounded function with small influences has level-one weight at most , up to an explicit error linear in the largest influence. Bounds on the level-one weight also appear in Talagrand's work on correlation of monotone sets (Combinatorica 1996), which the paper compares against (its Theorem 18), and the level-one inequality is a standard chapter of the analysis of Boolean functions (O'Donnell 2014).
Points of the discrete cube are sign vectors ; following the paper, the bit TRUE is read as and FALSE as . The cube carries the uniform probability measure, so , and real functions form an inner product space with .
For the parity ; the parities form an orthonormal basis, and the Fourier coefficient of at is . The weight of at level 1 is
The influence of coordinate on (Definition 2) is
the expected variance of when all coordinates but are fixed at random and is a uniform sign. The linear part of is , and , , .
Throughout, .
For every , every and every with for all ,
The constant is explicit, and the goal states it exactly as printed.
The result. The constant is sharp: majority on variables has influences of order and level-one weight tending to , which is for a standard Gaussian . Theorem 6 thus identifies the extremal level-one weight of low-influence bounded functions and gives a rate linear in the maximal influence. It is the instance of Majority Is Stablest, obtained without the invariance principle, and level-one bounds of this type are used in hardness reductions and in the study of noise sensitivity.
Formalizing it. The milestones together give a complete formal route from bounded functions to the stated bound, except for one step discussed below. They also produce a reusable layer of Boolean Fourier analysis: Fourier coefficients, level weights, influences in their variance form and the Fourier formula for influences. Mathlib contains no development of influences or level weights on the cube, and the platform has none either; the König–Schütt–Tomczak-Jaegermann inequality, a sharp quantitative central limit bound for Rademacher sums (J. Reine Angew. Math. 1999), has no machine-checked proof.
Status. The published proof's first step, , is valid for Boolean-valued but not for -valued ; for -valued the statement is posed as printed. For with one has , and the argument as written then yields only . Numerical search over small cubes has found no function violating the printed bound. A proof of the goal for bounded , or a counterexample, is therefore a genuine contribution.
The obvious argument replaces by a Gaussian with the same variance and uses . A central limit theorem with an error term is needed, and generic Berry–Esseen bounds give an additive error with a constant far from ; the exact constant requires the sharp Rademacher-sum inequality, whose proof is a delicate analysis of as a function of the coefficients. The second obstacle is the passage from influences to coefficients. For bounded only holds, so a bound on influences controls coefficients only at scale ; feeding that into the chain loses the linear dependence on . Recovering the printed rate for non-Boolean needs an idea beyond the published proof.
A point of the cube is Fin n → Bool, mapped to a sign by pm with pm true = -1 and pm false = 1. Expectations are normalised finite sums, so no measure theory is involved. A function is a real function with the hypothesis ∀ x, |f x| ≤ 1. The influence is defined as on the page, as the average over the cube of , which is the variance in ; it is not defined by its Fourier formula, which is a milestone. The level-one weight is . The constant is written out as 2 * (1 - Real.sqrt (2 / Real.pi)); an existentially quantified constant would be a weaker theorem. The case is allowed.
Two hypotheses are added and disclosed: in Theorem 6 and in the König–Schütt–Tomczak-Jaegermann bound. For each follows from the other hypotheses; for the influence (resp. coefficient) hypothesis is empty and is what the page assumes.
A trivializing formalization would drop the range hypothesis (then scaled dictators refute the bound and the statement is false), define influence through Fourier coefficients (which makes Proposition 7.2 definitional), or weaken the hypothesis of the goal to a bound on the coefficients ; none of these is used here. In particular, the goal is not strengthened to Boolean-valued , where the published proof applies verbatim.
Contributions welcome: proofs of Parseval-type identities for the linear part, of Proposition 7.2, of the elementary quadratic step, of the König–Schütt–Tomczak-Jaegermann inequality, and of the goal itself. The cube layer is reusable for any later formalization of Boolean function analysis.
MAX-CUT asks for a partition of the vertices of a graph that cuts as many edges, or as much edge weight, as possible. It is one of Karp's original NP-hard problems and the standard test case for approximation algorithms. A uniformly random partition cuts half of the edges in expectation. Goemans and Williamson (JACM 1995) rounded a semidefinite relaxation with a random hyperplane and obtained the ratio
Whether a better ratio can be achieved in polynomial time was a central open question.
Timeline.
A Unique Label Cover instance is a bipartite graph with left vertices , right vertices and edges , together with a bijection on each edge. A labeling assigns a label in to every vertex, and it satisfies if . is the largest fraction of edges satisfied by a labeling. The Unique Games Conjecture says that for all there is such that it is NP-hard to distinguish instances with label set and from those with .
A weighted MAX-CUT instance is a graph with nonnegative edge weights. It is at least -satisfiable if some partition cuts at least a fraction of the total weight, and at most -satisfiable if no partition cuts more than an fraction.
On the cube , with TRUE and the uniform measure, the noise stability of at is . Here is uniform and is -correlated with : each independently equals with probability . The influence is the expected variance of in the coordinate , and the low-degree influence is . Majority Is Stablest states: for and there is such that every with and all has .
Assume the UGC and Majority Is Stablest. For every and it is NP-hard to distinguish MAX-CUT instances that are at least -satisfiable from those that are at most -satisfiable, where
Choosing to minimize gives hardness of approximation within any factor above ; that consequence is not part of the goal.
Under the UGC, Theorem 1 shows that the Goemans–Williamson algorithm is optimal for MAX-CUT. It also shows that the semidefinite relaxation's integrality gap and the hardness threshold coincide. This correspondence was later extended to every constraint satisfaction problem (Raghavendra, STOC 2008). The verifier analysis here is the template for many later UGC-hardness results: dictatorship tests via noise stability, and list-decoding via low-degree influences.
The paper's result is proved, conditional on the UGC; the UGC itself is open. To our knowledge, neither the reduction nor the Majority Is Stablest theorem has a machine-checked proof. This mission produces a checked version of the conditional reduction. Its by-products are reusable: Fourier analysis on the cube (noise stability, influences, the Bonami–Beckner operator), the Long-Code verifier analysis, and a gap-hardness interface on top of a Turing-machine definition of NP.
Completeness is a short calculation. The difficulty is soundness. A proof that the verifier accepts with probability above must be decoded into a labeling that satisfies a fraction of the edges, and must not depend on the label set size . Labeling each by a coordinate of large influence of is the obvious decoding, but on its own it does not work. The test is passed with high probability by the averaged functions , not by the themselves. Ruling out functions with only small influences is exactly the content of Majority Is Stablest. The analysis needs both the reverse form of Majority Is Stablest for negative and low-degree influences, whose sum is bounded by independently of . Turning the PCP into polynomial-time gap-hardness adds further work on top of the analysis:
Fin n → Bool, with TRUE . Expectations are finite averages.GapNPHard: every NP language of the published CookPvsNP_defs maps by a polynomial-time Turing-machine computable function to Yes-instances or No-instances. Instances are encoded in unary.True/False) versions of the UGC or of Majority Is Stablest would trivialize the goal and are excluded.A manufacturer must commit to production before its retail customer knows what the market will demand, while the customer would rather postpone its purchase until better information arrives. Left uncoordinated, each firm protects itself: the customer inflates forecasts it is not bound by, and the manufacturer, discounting those forecasts, builds less than the supply chain as a whole should. Quantity flexibility (QF) contracts, used in practice in the electronics and computer industries (Sun Microsystems, Solectron, Nippon Otis and others are cited in the paper), address this by tying the customer's forecast to a band: the manufacturer guarantees supply up to a percentage above the forecast, and the customer promises to buy at least a percentage below it.
Tsay (1999) gives a two-stage model of such a contract with a demand signal that arrives between production and purchase, shows that a supply chain without commitment underproduces, and characterizes when a QF contract restores efficiency. This mission formalizes the efficiency result for the case in which the signal predicts demand perfectly (Proposition 6(a)), together with the steps of the equilibrium that it rests on.
A manufacturer (EM) produces at unit cost and sells to a retailer at unit transfer price ; the retailer sells at price , unsold units are salvaged at at either site, and each unit of unmet demand costs a goodwill loss . The standing assumptions are , and .
Before production, the retailer states a forecast . A QF contract with and obliges the EM to make up to available and the retailer to buy at least . The EM then builds . A demand signal with distribution function is observed, the retailer buys , and market demand is filled from the retailer's stock. In this mission the signal is perfect (): market demand equals , so its distribution equals .
Given , the retailer's profit from buying is
and it buys , the point of the interval closest to . The EM's expected profit (2) is . The retailer's forecast problem maximizes with the EM building . A central planner earns , maximized at
The total flexibility of the contract is .
With , the QF contract with flexibility and transfer price
is system-efficient: the retailer's unique optimal forecast is , the EM's unique optimal production given is , and the resulting expected system profit equals .
The result shows that one contract form, by choosing the transfer price as a function of the flexibility, yields a whole menu of contracts each of which coordinates the supply chain, so that the two firms can trade price against flexibility without losing system profit. Its corollaries in the paper, that any split of expected profit is achievable by some efficient contract and that more flexibility shifts profit to the manufacturer, rest on (4).
The paper prints no proofs ("All proofs are omitted due to space limitations", p. 1341). A machine-checked development supplies them, makes explicit the regularity the argument needs (finite variance, a continuous and strictly increasing , a positive efficient quantity), and gives reusable statements about newsvendor objectives with a clipped purchase. To our knowledge none of these results has been formalized before; the platform's quantity-flexibility theorems in other models (no manufacturer production stage, , retailer side only) do not cover them.
Each firm optimizes its own objective, and the efficient price must work for both at once. Making the retailer's first-order condition hold at pins down , so nothing is left to adjust for the EM, whose incentive to build more than the contracted has to be ruled out separately at that same price. The retailer's objective is an expectation of a non-smooth function of a clipped purchase, so its derivative must be computed through the distribution of on two moving thresholds and , and strict concavity must come from the strict increase of rather than from a density.
All objects live in the namespace TsayQF.EffQF. The law of is a probability measure on with , whose distribution function cdf ν is differentiable and strictly increasing on (the paper's "differentiable and invertible"). Expectations are Bochner integrals; finite variance makes every integrand integrable. Inverse distribution functions are not used: enters as a real number with the hypothesis , which determines it uniquely, and (4) is defined in its printed shape. Optimality is IsMaxOn over the decision's natural set: forecasts in , the EM's production in , purchases in , central production in .
Hypotheses made explicit: in the goal and a positive marginal value of the forecast at in Proposition 3(a), both standing for the paper's presumption that demand is almost certainly nonnegative; (Proposition 3's case). The transfer price is only required to satisfy rather than , because can exceed when . The milestones are the instances of the paper's general statements.
Two modelling choices are fixed. The retailer's forecast objective takes the EM's production to be , as §6.1 does after Proposition 2; the full game in which the retailer anticipates other EM responses is not modelled, and the goal instead verifies that the EM's unique best response at is exactly . The efficient price is the explicit formula (4), not "a price that makes optimal", which would make the goal a tautology; likewise system efficiency is stated as an inequality against at every production level, not by definition.
Needed infrastructure: derivatives of expectations of piecewise-linear functions of a clipped variable, and the newsvendor fractile characterization. Both are reusable for other contract models. Proofs of any milestone, and of the goal from the milestones, are welcome.
Periodic-review inventory models with a fixed ordering cost are the setting in which the policy is optimal: when the stock falls below a reorder point , order up to a level , otherwise order nothing. Scarf (1960) proved this for independent demands over a finite horizon by introducing -convexity, and Iglehart (1963) extended it to the discounted infinite horizon. In practice the demand distribution changes with an exogenous environment: the economy, the season, the stage of a product's life cycle. Song and Zipkin (Oper. Res. 41(2), 1993) modelled this environment as a Markov chain of demand states in continuous time with Poisson demand.
Sethi and Cheng (Oper. Res. 45(6), 1997) treat the discrete-time version with general demand densities, nonstationary costs and convex surplus costs of linear growth. The companion mission (I) covers their finite-horizon result, Theorem 4.1. This mission covers the nonstationary discounted infinite-horizon result, Theorem 6.2, together with the existence theory (Theorem 6.1, proved in the paper's Appendix) on which it rests.
Demand states form the finite set and follow a Markov chain with transition matrix . In period the demand has the conditional density given , with mean at most . Orders are placed at the start of a period and delivered at once, and unmet demand is backlogged, so the surplus evolves by (2.4). Ordering costs with (2.1), where for and otherwise. The surplus cost is convex and nonnegative, vanishes at , and satisfies (2.2).
An admissible policy chooses each order as a measurable function of the past demand states and demands. With a discount factor , the objective from period , state and surplus is
and the value function is . With (3.1), the dynamic programming equations are
The truncations keep the first periods of (6.1) (6.3), their values are (6.4), and is the cost of never ordering (6.6). The function classes are (nonnegative pointwise limits of continuous functions), (those of linear growth) and (those also uniformly continuous in ). A function is -convex if for all , (4.3). Assumption (4.1) asks , and (4.2) asks as .
Under (2.1), (2.2), (4.1), (4.2) and , there are in such that
attains the infimum in (6.2) at every , and its feedback policy, started at any period and surplus , has cost : it is optimal among all history-dependent policies.
The structural lemma behind the step from -convexity to the form, Proposition 4.2 of the paper (an extension of Bertsekas' lemma to lower semicontinuous functions coercive only at , with possibly infinite , ), is posed in the companion finite-horizon mission and is not repeated here.
Theorem 6.2 says that the classical structure survives two generalizations at once: demand driven by a Markov environment, and nonstationary data over an infinite horizon. The two levels may depend on the period and on the current demand state, so only numbers per period describe an optimal policy, and with cyclic demand only pairs are needed (Corollary 7.1 of the paper). Theorem 6.1 is a self-contained existence result for a positive-cost, unbounded-state dynamic program: value iteration from zero converges to the value function, which solves the optimality equation, and any measurable minimizer is optimal among history-dependent policies.
The results are proved in the paper, with the finite-horizon existence theory delegated to Beyer, Sethi and Taksar (1998). No machine-checked proof of any of them is known. The platform has -convexity (BertsekasKConvex) and the structure lemma of Bertsekas for continuous functions coercive at both ends; it has no discounted infinite-horizon theorem with Markov-modulated demand. The related posed items SongZipkinFluct.FixedCost.theorem5e_theorem6 and theorem5ab concern the Song–Zipkin model (continuous time, Poisson demand, integer levels, stationary data), a different model.
The obvious argument is "the finite-horizon value functions are -convex, so their limit is, and a minimizer of a -convex optimality equation is ". Three steps of it fail as stated.
First, the limit of value iteration need not be the value function, nor solve (6.2), in a positive-cost problem with unbounded actions: exchanging with requires the minimizers of the truncated problems to stay in a compact set uniformly in , and that bound is where the coercivity assumption (4.2) enters. Second, optimality against history-dependent policies, not only Markov ones, requires a verification argument along histories of states and demands. Third, the functions may be unbounded below, in which case the reorder level is and the order-up-to level does not exist; the goal allows this case.
The Lean development (namespace SethiChengSS.Infinite) commits to the following.
Fin L; periods are natural numbers with the paper's base .Pins. The paper prints ; the mission assumes , since is infinite at and the Appendix divides by . Theorem 6.2 is printed without (4.1), which its proof uses through the induction of Section 4; (4.1) is assumed for every period. Theorem 6.1 is printed under (2.1)–(2.2) only, but attainment in (6.2) can fail without coercivity and the Appendix bound (A.3) divides by ; (4.2) is added to (6.9), (6.10) and to the attainment clause of (6.5). "In class " for the sequence is read with one growth constant for all periods. The boundary condition "" of (6.5) is read as , as the next sentence of the paper states.
The goal cannot be met by a degenerate encoding: the value function is the infimum over all admissible history-dependent policies (not the solution of (6.2) by definition), the demand data must be genuine probability densities with bounded mean, and the levels may not be .
A complete development needs: monotone convergence for the path-measure costs, measurable selection of minimizers, the -convexity closure properties (Proposition 4.1 of the paper; several are proved on the platform as BertsekasDP.kconvex_*), and Proposition 4.2. The model file and the infinite-horizon verification argument are reusable for other Markov-modulated inventory models. Contributions toward any milestone, or toward general lemmas on positive-cost dynamic programs, are welcome.
Stochastic differential equations (SDEs) are simulated almost always by time-stepping schemes, and the cheapest and most widely used is the explicit Euler (Euler–Maruyama) scheme. Its strong convergence with order is classical when the coefficients are globally Lipschitz. Many models in applications are not: Langevin dynamics with confining potentials, stochastic Ginzburg–Landau equations, and population or volatility models have drifts such as that grow superlinearly.
For such drifts the explicit Euler scheme fails. Hutzenthaler, Jentzen and Kloeden showed in 2011 (Proc. R. Soc. A 467) that its absolute moments diverge to infinity whenever the drift or the diffusion grows superlinearly, so it does not converge in . Implicit schemes do converge (Higham, Mao and Stuart, SIAM J. Numer. Anal. 40, 2002), but each step requires solving a nonlinear equation.
The paper of this mission (Hutzenthaler, Jentzen and Kloeden, Ann. Appl. Probab. 22(4), 2012) introduces a tamed Euler scheme: an explicit method that costs the same as the Euler scheme, modified by a second-order term in the drift. It proves strong convergence with order under a one-sided Lipschitz drift whose derivative grows at most polynomially. The scheme started a line of work on tamed and truncated methods, among them Sabanis's schemes that tame drift and diffusion together for superlinearly growing diffusion coefficients (Ann. Appl. Probab. 26(4), 2016), formalized on this platform in the series "Euler Approximations with Varying Coefficients".
Fix and . Let be a probability space with a filtration , and let be an -dimensional standard -Brownian motion. On , is the Euclidean norm and the inner product. For a matrix , is the operator norm.
The initial value is -measurable with for every . The drift is continuously differentiable and the diffusion is . There is one constant with
for all . The exact solution is an adapted process with continuous paths and
For , let . The tamed Euler scheme is and
On its interpolation is
In Lean, states live in EthierKurtz.SDEState d, takes values in Matrix (Fin d) (Fin m) ℝ, the standing hypotheses are the structures Coefficients and Setting, and the scheme is Y, Ybar, all in the namespace TamedEuler.Convergence.
There is a family , , such that for every solution
The constants are left unspecified; only the order is asserted.
These are the ten lemmas the proof rests on, in the paper's order:
The theorem gives an explicit scheme whose cost per step is the Euler cost and whose strong error is in every , uniformly in time, for the superlinear drifts on which the explicit Euler scheme diverges. Strong error bounds of this kind are what multilevel Monte Carlo (Giles 2008) needs, as the paper notes on p. 3: its complexity analysis requires strong convergence of the coarse and fine levels, and the explicit Euler scheme supplies none for these equations. The moment bound of Lemma 3.9 answers, for the tamed scheme, the open problem Higham, Mao and Stuart formulated in 2002 on when moment bounds hold for explicit methods (quoted on p. 8).
The result is proved in the paper; it has not been formalized. The mission formalizes the statement, its ten lemmas and the scheme. The dominator construction (13)–(14) is a pathwise argument that can be checked independently of the probability. The two Burkholder–Davis–Gundy inequalities with the explicit constant are reusable tools for any numerical analysis of SDEs.
Once the moments of are bounded uniformly in , the convergence proof follows the globally Lipschitz pattern: an Itô or Gronwall argument on . The difficulty is the moment bound itself. The obvious approach is a Gronwall recursion for in terms of . For superlinear it does not close: the term grows faster than , and for the untamed scheme the moments do in fact diverge. A newcomer's first idea, using the one-sided Lipschitz bound in expectation, fails for the same reason. The paper instead dominates the scheme pathwise on events and controls the rare complement separately (Lemmas 3.1, 3.5, 3.6).
The Lean development commits to the following conventions.
ℱ.IsRightContinuous) together with adaptedness to its -completion, which is how the published SabanisEuler.Shared.IsSolution treats completeness.SabanisEuler.Shared.IsWienerMartingale, defined on rather than ; this is the usual extension. Time is ℝ≥0.IsSolution relation, whose stochastic integral is the Ethier–Kurtz Brownian Itô-integral relation. Existence and uniqueness are cited by the paper, not claimed. enters IsSolution entrywise through toDiffusion. Every norm of in a hypothesis or conclusion is the operator norm opNorm.lintegral or eLpNorm, never as a Bochner integral that could default to .A trivializing formalization is ruled out: the scheme is (8) exactly, with only the drift tamed and the step size . The error is taken against the same Brownian path that drives . The setting is satisfiable for the paper's example , with (checked in a sorry-free verification file, given any Brownian motion). Replacing the Itô integral by a postulated operator or a pathwise integral is not admitted.
A complete development needs:
The BDG inequalities and the Gaussian moment identity are reusable beyond this mission. Contributions to any lemma, or to the stochastic-calculus infrastructure underneath, are welcome.
Transient stability asks whether a power grid, after a large disturbance such as a fault or a line trip, returns to synchronous operation in which all generators rotate at a common frequency. The classical approach builds energy functions for the swing equations and estimates regions of attraction numerically; it gives no closed-form test relating synchronization to the network's parameters, and it handles transfer conductances (losses) only when they are "sufficiently small" without saying how small.
Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012) observe that, for strongly overdamped generators, the network-reduced swing equations behave like a first-order non-uniform Kuramoto model, and they give purely algebraic conditions under which this model synchronizes. The same model is a generalization of the classical Kuramoto model of coupled oscillators, studied in physics, neuroscience and control, with heterogeneous time constants, asymmetric effective coupling and phase shifts. This mission formalizes the first of the paper's two synchronization conditions, Theorem V.3, which is also statements 1)–2) of the paper's main result, Theorem III.2.
There are oscillators with phases . Each has a time constant and a natural frequency ; each pair has a coupling weight and a phase shift , with . The non-uniform Kuramoto model is
The phases live on the torus. For an arc length , the set consists of configurations whose phases all lie in the interior of some arc of length , and is its closure (with the synchronized configurations). A set is positively invariant if every solution starting in it stays in it. A solution achieves exponential frequency synchronization if all frequencies converge exponentially fast to a common value .
The condition of the theorem compares two numbers built from the parameters, with :
is the weakest lossless coupling of an oscillator to the network; measures the spread of natural frequencies and the losses. When , put , and .
If is complete ( for ) and
then (1) is positively invariant for every , and every solution starting in eventually stays in for each ; (2) every solution starting in achieves exponential frequency synchronization to some , and when the solution starts in .
The milestones follow the paper's proof. Theorem V.1 is a frequency-synchronization theorem for phase-cohesive oscillators under a globally reachable node, with the explicit rate
when and . Its supporting steps are the frequency dynamics (20) and a dihedral-angle bound. The phase-cohesiveness argument of Theorem V.3 is split into a trigonometric lower bound, a pointwise bound on the growth rate of the arc containing all phases, the characterization of by inequality (30), positive invariance, and the entry into .
The theorem turns synchronization of a heterogeneous, lossy oscillator network into one inequality among explicit parameters. For the classical Kuramoto model it specializes to (Remark V.4), which improved the sufficient conditions known at the time. For power networks it gives, through Theorem III.2, a computable sufficient condition for transient stability when generator inertia is small relative to damping.
To our knowledge none of these results has a machine-checked proof. The development needs ODE comparison arguments for a non-smooth Lyapunov function (the arc length) and an exponential convergence theorem for time-varying consensus. Both are general tools that are not in Mathlib and would be reusable for other consensus and synchronization results. The mission also records two clauses of the printed theorem that are false as stated, with counterexamples, and states the corrected theorem.
The arc length is only Lipschitz, so its decrease along solutions must be argued through Dini derivatives and a comparison lemma rather than by differentiation. Positive invariance at the boundary holds with a non-strict inequality, so a naive "strictly decreasing at the boundary" argument does not apply there. Frequency synchronization rests on a contraction property of linear consensus with time-varying, state-dependent weights. The weights are positive only after the phases have entered . Before that the frequency range can expand, which is why the range clause of the printed theorem fails for initial arcs longer than .
Phases are represented by real lifts . means that all pairwise differences of the lift are at most , and that they are strictly less than . Conclusions are stated for the same continuous lift, which is at least as strong as membership on the torus. A solution is a map with derivative (one-sided at ) equal to the right-hand side of (8) for all . Every statement quantifies over all such solutions. always denotes the vector field along the solution. Minima and maxima over are over ordered pairs, and is assumed so that they exist. The conventions are explicit hypotheses. and are defined by , and a milestone certifies that they are the unique solutions in the printed ranges. is the second-smallest eigenvalue of the symmetric Laplacian.
The source is the arXiv preprint v4 of the SICON article, cited with its own page and theorem numbers. Three corrections relative to the printed text are made and disclosed in the items:
No statement is trivially satisfiable. The solution predicate holds for actual solutions (for example the synchronous solution), condition (26) is satisfiable (take and ), the exponential rate is required to be strictly positive, and are specific numbers rather than existential witnesses.
Contributions are welcome on all milestones. The trigonometric bound, the dihedral-angle bound and the characterization are elementary. The comparison lemma for Dini derivatives and the consensus contraction theorem are reusable infrastructure.
A spectral sparsifier of a graph is a much sparser weighted graph whose Laplacian quadratic form is within a factor of the original on every vector. Spielman and Teng introduced the notion in Spectral Sparsification of Graphs as a strengthening of the cut sparsifiers of Benczúr and Karger: a spectral sparsifier preserves every cut, and in addition every quantity determined by the Laplacian quadratic form, such as effective resistances, eigenvalues and the behaviour of random walks. Sparsifiers are the reason linear systems in graph Laplacians can be solved in nearly linear time: one preconditions with a sparsifier and solves the sparse system instead (Spielman–Teng, arXiv:cs/0607105).
The construction in the paper has two halves: decompose the graph into pieces of high conductance, then sparsify each piece by random sampling. This mission is the second half, Theorem 6.1 of §6: in a graph whose normalized Laplacian has a spectral gap, keeping each edge independently with probability inversely proportional to the smaller degree of its endpoints, and reweighting kept edges by the inverse probability, produces a -spectral approximation with few edges, with high probability.
Timeline. Benczúr and Karger (1996) sampled edges with probabilities depending on edge strength and preserved cuts. Achlioptas and McSherry (2001) analysed random sampling of matrices through the random-matrix norm bound of Füredi and Komlós (1981), corrected by Vu (2007). Spielman and Teng (arXiv 2008, SIAM J. Comput. 2011) proved Theorem 6.1 by refining the Füredi–Komlós trace method for downsampling graphs that may already be sparse. Spielman and Srivastava (2008) later replaced conductance-based probabilities by effective resistances.
Let be an unweighted graph on a finite vertex set , , with degrees , adjacency matrix , diagonal degree matrix and Laplacian . Its quadratic form is
A weighted graph on with weights has the form . is a -approximation of if for all
When every degree is positive, the normalized Laplacian is ; its eigenvalues lie in , and a lower bound on its smallest non-zero eigenvalue measures how well connected each component of is (by Cheeger's inequality it is equivalent to high conductance up to squaring).
Sampling. For a parameter , edge is assigned
each edge is kept independently with probability , and a kept edge gets weight . The sampled adjacency matrix then has ; is the diagonal matrix of weighted degrees of the sampled graph.
The procedure. In Theorem 6.1 sampling is applied only to the edges of an induced subgraph , ; the other edges are kept with weight 1. sets and uses the degrees of ; the paper takes .
For , without isolated vertices whose smallest non-zero normalized Laplacian eigenvalue is at least , , and an even integer : with probability at least , simultaneously
Theorem 6.1 is the sampling engine of the first nearly-linear-time spectral sparsification algorithm: combined with a decomposition of an arbitrary graph into high-conductance pieces (§7–§10 of the paper), it yields sparsifiers with edges, which in turn give the nearly-linear-time Laplacian solvers that underlie fast algorithms for electrical flows, maximum flow approximation and graph partitioning. Lemma 6.3 is a self-contained random-matrix result: a norm bound for the normalized deviation of a downsampled graph that does not assume the original graph is dense.
The result is proved in the paper. As far as is known, none of it is formalized in Lean or Mathlib: Mathlib has the graph Laplacian (SimpleGraph.lapMatrix) and the spectral theorem for Hermitian matrices, but no normalized Laplacian, no spectral approximation and no trace-method bounds for random matrices. A complete formalization would be the first machine-checked proof of a spectral sparsification theorem, and the milestones (the trace-method moment bound, Chernoff for weighted two-point sums) are reusable on their own.
The obvious argument — bound each entry of and apply a matrix concentration inequality — needs either a matrix Chernoff bound (not in the paper, and not in Mathlib) or the Füredi–Komlós trace method, which assumes every edge can appear and so fails when the graph is already sparse: a vertex of small degree has no room for its entries to average out. The paper's sampling probabilities keep every edge at a vertex of degree at most , and the trace computation has to exploit exactly this through the moment bound of Lemma 6.6 and a combinatorial count of closed walks. Formally, the obstacles are the walk-counting argument of Lemma 6.4, the passage from a trace bound to an eigenvalue bound for the non-symmetric (similar to a symmetric matrix), and Lemma 6.2's restriction to the orthogonal complement of the kernel, which must handle disconnected in the goal.
V; graphs are SimpleGraph V with decidable adjacency; weighted graphs are weight functions V → V → ℝ (symmetric, nonnegative, loopless). The quadratic form is ; a -approximation keeps both inequalities of (2).Search engines sell advertising space query by query. Each advertiser states a bid for each keyword and a daily budget; queries arrive one at a time, and each must be assigned to an advertiser immediately, without knowledge of the queries still to come. The revenue-maximizing assignment of the day can only be computed offline. The adwords problem asks how close an online rule can get to it. It generalizes online bipartite matching, for which Karp, Vazirani and Vazirani (KVV 1990) showed that randomized ranking attains ratio , and -matching, for which Kalyanasundaram and Pruhs (KP 2000) showed that the deterministic BALANCE algorithm attains as the budget grows.
Mehta, Saberi, Vazirani and Vazirani (J. ACM 2007) gave a deterministic algorithm for arbitrary bids that weighs each bid by a function of the fraction of budget already spent, and proved that it is -competitive when bids are small compared to budgets. The algorithm and its tradeoff function became the reference point for the online budgeted-allocation literature, including the primal-dual analysis of Buchbinder, Jain and Naor (ESA 2007).
There are bidders, each with budget , and a sequence of queries . Bidder bids for the query at position . An allocation assigns each query to at most one bidder. Bidder 's spend before position is , and is alive while its spend is below . The revenue of is .
Fix an integer and split each budget into equal slabs; a spent fraction lies in slab , and in slab . Given a tradeoff function on slabs, the discrete tradeoff algorithm assigns each arriving query to an alive bidder maximizing
ties broken arbitrarily. Every allocation produced this way, for any tie-breaking, is a run.
The analysis uses the factor-revealing LP : maximize subject to and , written , , , and its dual . Its optimal dual solution is , and Theorem 8's tradeoff function is
For every there is such that for every there is such that, for every instance with bids in , every run of the algorithm with , and every allocation ,
The goal fixes no rate in or : it asserts only that the ratio tends to .
Theorem 8 gives an online algorithm for budgeted allocation with arbitrary bids whose revenue is within a factor of the offline optimum, the best possible ratio even for randomized algorithms (Theorem 9 of the same paper, the second mission of this series). It reduces to BALANCE when all bids are equal, and its tradeoff function in the limit is the function used in later work on online budgeted allocation and display-ad allocation.
The result is proved in the paper; none of it is formalized. The work here is to formalize the proof in a version that holds for actual runs. The paper's argument makes two simplifications with "negligible error": bidders of type spend exactly of their budget, and the offline optimum exhausts every budget. A formal proof must carry the bid size through the slab boundaries and compare with an arbitrary offline allocation. The LP lemmas (Lemmas 3–5) are self-contained statements about one triangular linear program and are reusable for factor-revealing analyses of BALANCE.
The milestones are short: Lemmas 3–5 are finite linear algebra with geometric sums, Lemma 6 is one application of the assignment rule plus monotonicity of spend, and Lemma 7 regroups finite sums. The difficulty is in Theorem 8. The paper's proof chains Lemmas 4, 5 and 7 through the LP , whose right-hand side is computed from the numbers of bidders of each type under the assumption that a bidder of type spends exactly . In an actual run this identity fails: a single bid can straddle a slab boundary, and types are intervals, not points. So the chain does not compose literally, and the natural first attempt, instantiating Lemma 5 with the run's quantities, does not apply. The slab-wise inequalities that do hold, with an error of order , have to replace the equalities, and the comparison with an offline allocation that does not exhaust budgets has to be made through capped revenues.
Bidders are Fin N and query positions Fin M, zero-based; slabs and LP coordinates keep the paper's 1-based ranges, with vectors as functions read on . Budgets are (the paper's standing simplification of §2). Bids are real and nonnegative.
A run is a predicate on the whole allocation: at position , if some bidder is alive the query goes to an alive maximizer of bid , where spends are computed from earlier positions only; the query is unassigned only when all budgets are exhausted. Every tie-breaking rule gives a run, and the goal holds for all of them. is the full bid of the chosen bidder; revenue is capped at the budget.
Conventions the statements commit to:
Trivializing formalizations are ruled out: a run cannot leave a query unassigned while a bidder has budget, so the empty allocation is not a run; no hypothesis of the form "bidders of type spend exactly " or "the optimum exhausts every budget" is imposed, since either would make the goal vacuous on most instances.
All definitions are local to the namespace AdWordsMSVV.Tradeoff. Related platform items analyse a different algorithm: BJNAdAuctions.Basic.* and OnlinePrimalDual.AdAuctions.* formalize the Buchbinder–Jain–Naor primal-dual algorithm, which updates a covering variable multiplicatively and has ratio ; they are not reused. Proofs of any milestone, and lemmas carrying the bid-size error through slab boundaries, are welcome.
Search engines sell advertising slots query by query. Each advertiser states a bid per keyword and a daily budget; queries arrive one at a time, and the engine must assign each to an advertiser immediately, without knowing which queries will come later. Mehta, Saberi, Vazirani and Vazirani (J. ACM 2007) called this the adwords problem and gave a deterministic online algorithm whose competitive ratio, the worst-case ratio of its revenue to the best offline revenue, tends to when bids are small compared to budgets. Section 7 of the same paper shows that this ratio cannot be beaten, even by randomized algorithms and even under the small-bids assumption. That lower bound is the subject of this mission.
Timeline of the special cases:
An instance of online b-matching has bidders and a sequence of queries . Every bidder has the same integer budget . Each query comes with the set of bidders that bid on it; the others bid .
A deterministic online algorithm processes the queries in order. When query arrives it sees the bid sets and nothing later, and it either proposes a bidder or leaves the query unallocated. The proposal succeeds if the bidder bids on the query and has won fewer than queries so far; the bidder then pays . The algorithm is not required to be greedy. Its revenue is the number of queries won. A randomized online algorithm is a probability distribution over deterministic online algorithms, fixed before the instance is chosen; its expected revenue is .
An offline allocation assigns each query to a bidder or to nobody, with full knowledge of . Its revenue is : each bidder pays for the queries it bids on, up to its budget.
The permuted round instances of the proof are as follows. For a permutation of the bidders, the instance consists of rounds of queries each, and bidders bid on the queries of round . The distribution is the uniform distribution over these instances, and denotes the average over it. The paper writes this instance with budget , bids and queries per round; the Lean development uses the same instance scaled by .
For every there is such that for all , all and every randomized online algorithm for bidders and queries, there are an instance and an allocation with
The constant is the paper's. The slack is not a weakening of the paper's claim: a competitive ratio better than would mean a ratio for some on every instance. The threshold is independent of the budget, which is how "for large " is rendered.
The result. Theorem 9 shows that the ratio attained by BALANCE for large budgets, and by the paper's tradeoff algorithm for adwords with small bids, is optimal among all online algorithms, randomized or not. Since b-matching is a special case of adwords with small bids, the same bound applies to adwords. It also answers the question of Kalyanasundaram and Pruhs on whether randomization helps for b-matching. With it contains the bipartite matching lower bound of Karp, Vazirani and Vazirani.
Formalizing it. The result has been proved since 2007; to our knowledge it has no machine-checked proof. The b = 1 case is posed on the platform as KVVMatching.UpperBound.theorem_2 (Karp–Vazirani–Vazirani), with columns arriving in reverse index order and an analysis of the algorithm RANDOM; this mission poses the budget-uniform statement in its own model. A formalization yields a reusable model of online algorithms with budgets (histories that hide the future, randomized algorithms as mixtures of deterministic rules) and a formal instance of Yao's principle for online problems.
The bound must hold for every deterministic online algorithm, including ones that are not greedy, waste proposals, or base each decision on the entire revealed history. A tempting argument fixes the algorithm's behaviour per round and treats it as oblivious to earlier rounds; that only covers a subclass. The history of the permuted instance reveals, before round , exactly which bidders dropped out in earlier rounds, so the information available to the algorithm grows round by round, and the bound on has to hold conditionally on everything revealed. Budgets interact across rounds: whether a proposal in round succeeds depends on wins in earlier rounds. Finally, the printed "at most " is false at every finite : the sum in milestone 5 exceeds by a bounded amount (about for large ), so the analytic step is genuinely asymptotic.
Fin N and query positions Fin M, both zero-based. An instance is Fin M → Finset (Fin N). A history is Fin M → Option (Finset (Fin N)) with unrevealed entries none. A deterministic algorithm is Fin M → History N M → Option (Fin N), a randomized one is a PMF over deterministic algorithms, and expected revenue is a finite sum.Khot, Kindler, Mossel and O'Donnell, Optimal Inapproximability Results for MAX-CUT and Other 2-Variable CSPs? (SIAM J. Comput. 37(1), 2007), prove that, assuming the Unique Games Conjecture, the Goemans–Williamson approximation ratio for MAX-CUT is optimal, and they extend the method to MAX-q-CUT and to Γ-MAX-2LIN(q). For the q-ary problems the key analytic input is the theorem of Mossel, O'Donnell and Oleszkiewicz (arXiv:math/0503503), the MOO theorem. It bounds the noise stability of a low-influence function with mean µ by a Gaussian quantity, the correlated Gaussian orthant probability Λ_ρ(µ): the probability that two ρ-correlated standard Gaussians both exceed the threshold t at which a single one has tail mass µ.
The hardness bounds of the paper for Γ-MAX-2LIN(q) are stated in terms of Λ_ρ(1/q). They are explicit only after Λ_ρ(µ) is estimated. Proposition 6.1 of the paper gives such an estimate in closed form, by slightly improving a bound from the proof of Lemma 11.1 of de Klerk, Pasechnik and Warners (Approximate graph colouring and MAX-k-CUT algorithms based on the theta function, J. Combin. Optim., 2004). The same quantity at µ = 1/2 is Sheppard's orthant probability (Phil. Trans. R. Soc. A 192, 1899), the source of the arccos formulas used throughout the MAX-CUT part of the paper.
This mission formalizes Proposition 6.1 and the steps of its printed proof.
Let φ be the standard Gaussian density and N the Gaussian tail probability function:
So N(x) = Pr[X ≥ x] for a standard Gaussian X. N is strictly decreasing from 1 to 0, and N(0) = 1/2.
Let X and Y be independent standard Gaussian random variables. For ρ ∈ [0, 1] put
Then (X, X′) is a centred normal pair with unit variances and covariance ρ, the pair of Definition 8 of the paper. For 0 < µ < 1 let t be the unique real number with Pr[X ≥ t] = µ, and define
The threshold t is positive exactly when µ < 1/2. Λ_ρ(µ) is the noise stability, in Gaussian space, of the indicator of a half-line of measure µ.
The proof uses two exponents. For u, v ∈ ℝ, with ρ < 1 and t > 0,
In Lean these are phi, tailN, orthantProb ρ t, Lambda ρ μ, gExp ρ t u v and hExp ρ t u v in the namespace OptInapprox.Orthant.
For any 0 ≤ µ < 1/2, let t > 0 be the number with N(t) = µ. Then for all 0 ≤ ρ ≤ 1,
The endpoint ρ = 1 is part of the goal. There X′ = X, Λ₁(µ) = µ, and (4) becomes the classical Mills-ratio inequality N(t) ≤ φ(t)/t.
Proposition 6.1 makes the MOO theorem quantitative for thresholds. With the lower bound of milestone 4 it determines Λ_ρ(µ) up to the factor 1 + ρ, and up to 1 + o(1) as µ → 0, since φ(t)/t ∼ N(t) as t → ∞ (Corollary 10, part 1). Through Corollary 10 it yields the asymptotics of qΛ_ρ(1/q) used in the paper's hardness results for MAX-q-CUT and Γ-MAX-2LIN(q). These quantities also appear in later work on q-ary noise stability and on the approximability of 2-CSPs.
The proposition is proved in the paper; nothing here is open. Mathlib (at the pinned revision) contains no proof of it, of the bivariate-normal integral representation (18), or of the Mills-ratio inequality N(t) ≤ φ(t)/t. On the platform, Mills' inequality appears only as an open statement in the two-sided form Pr[|X| > z] ≤ √(2/π)·e^{−z²/2}/z (KLTNuclear.Lasso.gaussian_tail), and there is no item for orthant probabilities. A complete development provides:
Each of these is reusable for Gaussian tail and orthant estimates.
The inequality itself is elementary once (18) and (20) are available. The work lies in the two integral identities and in their measure-theoretic glue.
For (18), the orthant probability is defined as a measure of a set under the product of two one-dimensional Gaussian laws. Writing it as a double integral of the bivariate density is a linear change of variables with Jacobian √(1 − ρ²). The shift and scaling by t then has Jacobian 1/t², and the quadratic form has to be expanded exactly.
For (20), the region u, v ≥ 0 becomes the wedge |s| ≤ r after the rotation, so the inner integral is a truncated Gaussian integral rather than a full one. The closed form appears only after an integration by parts in r, or an equivalent completion of the square.
The endpoint ρ = 1 is not covered by the printed argument, because (18) divides by √(1 − ρ²). It needs Mills' inequality separately. A proof that only treats ρ < 1 does not close the goal.
stdGaussPair is the product of two copies of Mathlib's gaussianReal 0 1 on ℝ × ℝ. orthantProb ρ t is the real-valued measure of {X ≥ t, ρX + √(1 − ρ²)Y ≥ t}, which is the representation the paper itself uses on p. 31.Lambda ρ μ chooses a t with Pr[X ≥ t] = µ, where the probability is taken under gaussianReal 0 1. Such a t is unique, so the choice does not matter. For µ ∉ (0, 1) no such t exists and the value is a placeholder 0 that no statement uses.The two remarks printed right after Proposition 6.1 (on Λ_ρ(1/2) and on removing the factor 1 + ρ) are not part of this mission.
Contributions are welcome on all four milestones, on the case ρ = 1 of the goal (Mills' inequality), and on general lemmas: N as Pr[X ≥ x], monotonicity and positivity of N, and the law of (X, ρX + √(1 − ρ²)Y) as a bivariate normal.
A sparse graph that approximates a dense one, in the sense that both have nearly the same Laplacian quadratic form, can stand in for it in every algorithm that only reads cuts or solves Laplacian linear systems. Spielman and Teng introduced such spectral sparsifiers and built them in nearly linear time; the construction is the sparsification step of their nearly-linear-time Laplacian solver (arXiv:0808.4134, SIAM J. Comput. 40(4), 2011).
Sampling edges at random works well only inside a graph of high conductance, where no vertex set is separated from the rest by few edges. A general graph is therefore first cut into pieces of high conductance, with few edges running between the pieces. Section 7 of the paper proves that such a decomposition always exists. A similar result was obtained independently by Trevisan (2005). The decomposition theorem, together with the sampling theorem of §6, already shows that every graph has a spectral sparsifier with edges; the algorithmic decomposition of §8, which the fast algorithm uses, is an approximate version of it, and its analysis rests on the same certificate lemma.
Let be a finite simple undirected graph with edges, and write for the degree of vertex . For disjoint , is the set of edges with one end in and one in . The volume of is ; in particular .
For a vertex set and , the conductance of inside is
and the conductance of is over proper subsets, with when . Volumes are always measured with the degrees of , never with the degrees inside the induced subgraph ; consequently is at most the usual conductance of , and lower bounds on transfer to it.
A decomposition of is a partition of . It is a -decomposition if for all , and its boundary is the set of edges between different parts,
In Lean: vol G S, cutEdges G S T , condRel G B S , cond G B , and decompBoundary G P for a Finpartition P of the vertex set, all in the namespace SpectralSparsify.Decomp.
Every graph without isolated vertices has a decomposition with
The constants are the paper's. Both conditions must hold for one and the same partition.
The theorem says that every graph is, after removing at most half of its edges, a disjoint union of pieces of conductance . By Cheeger's inequality each piece then has normalized spectral gap , which is the hypothesis under which the random sampling of §6 produces a spectral approximation; applying the theorem recursively to the removed edges gives the existence of spectral sparsifiers with edges (§7.2). Decompositions of this kind, now called expander decompositions, have become a standard tool in graph algorithms.
The theorem is proved in the paper; to the knowledge of this mission it has no machine-checked proof. What the mission produces is a formal proof of the existence statement with the paper's explicit constant, a formal Lemma 7.2 (the certificate lemma that also drives the approximate version, Theorem 8.1), and reusable Lean definitions of volume, relative conductance and decomposition boundary for finite simple graphs.
The obvious argument, cutting along any sparse set until no sparse set is left, controls the conductance of the final parts but not the number of edges cut: a long sequence of small sparse cuts can remove far more than half of the edges. The difficulty is to show that one well-chosen cut leaves a remainder whose conductance is certified without further search, which is the content of Lemma 7.2. Its hypothesis is a maximality condition over all subsets of , and its conclusion concerns all subsets of , a different set measured with the same ambient degrees, so the two cannot be compared directly. The existence statement then needs a well-founded description of the recursion, a bound on its depth, and an accounting of the cut edges level by level, all against the explicit constant .
Graphs are SimpleGraph V on a finite vertex type with decidable adjacency; vertex sets are Finset V; volumes, conductances and the bound on are real numbers; decompositions are Finpartition (Finset.univ : Finset V); is Real.logb (4/3).
Hypotheses made explicit:
∀ v, 0 < G.degree v) in Theorem 7.1, Lemma 7.2 and the milestones that divide by a volume. The paper leaves it implicit: is for sets of isolated vertices, and with Lean's Lemma 7.2 would be false (one edge plus two isolated vertices is a counterexample). Under the hypothesis forces , and Theorem 7.1 is then trivially true.Conventions: is the minimum over proper subsets, the empty set contributing ; for ; counts ordered adjacent pairs in , which is the edge count for disjoint sets. Neither conclusion of Theorem 7.1 may be dropped: the partition into singletons satisfies the conductance bound and the partition into one part satisfies the boundary bound, so a formalization keeping only one conclusion is trivial.
Not formalized: idealDecomp as an object (step 2 involves a choice, so it is a relation rather than a function; the goal is the existence statement), its termination and depth bound as separate items, the λ-spectral decomposition remark via Cheeger's inequality, the existence sketch for sparsifiers in §7.2, and the algorithmic analogue of §8. Contributions welcome: proofs of the milestones, a formal recursion for idealDecomp, and lemmas on volume and edge-boundary arithmetic that other graph-partitioning missions can reuse.
Many graph algorithms run in time proportional to the number of edges. A sparsifier of a weighted graph is a graph on the same vertices with far fewer edges that approximates for the purpose at hand, so that the algorithm can be run on instead. Benczúr and Karger (1996) showed that every graph has a sparsifier with edges preserving the weight of every cut up to a factor . Spielman and Teng (2004) introduced the stronger spectral notion, in which the Laplacian quadratic form is preserved for every real vector, not only for cut indicators; their sparsifiers had edges for a large constant and were the first step of their nearly-linear-time solvers for symmetric diagonally dominant linear systems.
Spielman and Srivastava (arXiv:0803.0929, STOC 2008, SIAM J. Comput. 2011) proved that independent sampling of edges, each edge with probability proportional to its weight times its effective resistance, yields a spectral sparsifier. The result improved both earlier bounds, replaced a recursive partitioning construction by a one-line sampling rule, and made effective resistance a standard tool in graph algorithms. Batson, Spielman and Srivastava (arXiv:0808.0163) later obtained edges deterministically, by a slower method built on the same matrix .
Let be a connected weighted undirected graph with vertices, edges and weights . Orient every edge arbitrarily, so that it has a head and a tail (distinct vertices).
There are an absolute constant and a threshold such that, for every , every connected weighted graph on vertices and every , with , with probability at least
The constant is left unfixed; the statement asserts the shape with the paper's explicit dependence on .
Theorem 1 says that every weighted graph is spectrally approximated by a reweighted subgraph with edges. A spectral approximation preserves cut weights, the eigenvalues of the Laplacian up to , effective resistances, and the condition number of as a preconditioner, so any algorithm whose output depends on these quantities can run on . Combined with fast approximate computation of effective resistances (the second mission of this series), it gives a nearly-linear-time construction, and it is the sampling step used in Laplacian solvers, in sparsification of sums of rank-one matrices, and in leverage-score sampling for regression, where is exactly the statistical leverage of a row.
The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission formalizes the statement and the paper's proof structure: the linear algebra of (Lemma 3), the deterministic reduction from quadratic forms to a spectral-norm bound (Lemma 4), and the matrix concentration inequality (Lemma 5), which is the substantive analytic input and is itself a reusable result about sums of independent rank-one matrices.
The deterministic part is linear algebra over the pseudoinverse. The obstacle is concentration: the expected Laplacian of equals , but bounding the deviation uniformly over all is a statement about the spectral norm of a random matrix, and a union bound over a net of directions costs a factor of in the sample count rather than . Scalar Chernoff bounds per cut, which suffice for cut sparsifiers, do not give the spectral statement. Lemma 5 is the matrix inequality that removes this loss, and no inequality of this kind (a concentration bound for the spectral norm of a sum of independent random matrices) is in Mathlib.
All declarations sit in the namespace EffResSparsify.Sampling.
WGraph V E with orientation maps head, tail : E → V, weights w : E → ℝ, and the fields head e ≠ tail e (no loops) and 0 < w e. Parallel edges are allowed; nothing in §3 uses simplicity. Connectivity is a separate hypothesis on the underlying simple graph and includes . In Theorem 1 the vertex type is Fin n; the edge type is an arbitrary finite type.HarmonicGames.Decomposition.pinv of on Euclidean ; it equals the spectral formula above and is the gauge-fixed inverse, never "some solution of ".Matrix.Norms.L2Operator); vector norms in Lemma 5 are Euclidean; is natural (the base is absorbed into ).Reusable beyond this mission: the weighted Laplacian with its pseudoinverse and effective resistances, and Lemma 5, which applies to any sampling scheme for sums of rank-one matrices (leverage-score sampling, column subset selection). Contributions toward a matrix Chernoff or Rudelson-type inequality in Mathlib are welcome.
Grover's algorithm finds a marked element among with queries by alternating two reflections: one about the initial state and one that flips the sign of marked states. In quantum-walk search, the initial state encodes the stationary distribution of a Markov chain, and the reflection about is too expensive to implement exactly. Magniez, Nayak, Roland and Santha (arXiv:quant-ph/0608026, SIAM J. Comput. 2011) obtain the reflection approximately, by phase estimation on the quantum walk, and need a search procedure that tolerates the approximation error without paying extra cost to reduce it. Their Section 4 supplies one: a variant of the recursive amplitude amplification (RAA) of Høyer, Mosca and de Wolf (ICALP 2003) in which the reflection about is replaced, at recursion level , by an approximate circuit of precision . The two lemmas of that section, stated "in full generality for potential further applications" (p. 11), are the exact engine of the paper's headline Theorem 3 (search with cost ).
Timeline: Grover (1996) gives quadratic speedup for unstructured search; Brassard, Høyer, Mosca and Tapp (2002) generalize it to amplitude amplification; Høyer, Mosca and de Wolf (2003) introduce RAA to tolerate a bounded-error marking reflection; Szegedy (2004) defines quantum walks for arbitrary reversible chains with detection guarantees; Magniez, Nayak, Roland and Santha (STOC 2007, SIAM 2011) adapt RAA to an approximate initial-state reflection and obtain search, not only detection, for every reversible ergodic chain.
Let be a finite set and a set of marked elements. The state space is . The initial state is any unit vector (Lemmas 1 and 2 never use its quantum-walk form), and the marked weight is , where projects onto the basis states with .
For each level an extra register (a finite-dimensional space with a basis state ) is given together with a unitary on , playing the role of :
On the marked subspace consists of states whose first register is marked, and .
Approximate RAA is the unitary with and
where multiplies by every basis state in which some register , , is not , and otherwise applies to . Write and .
Tolerant RAA first samples (succeeding with probability ); otherwise, for , it applies to the state left over from the previous failed measurement, with , and measures ; a failure collapses the state to .
Let , let satisfy whenever , and let be the smallest non-negative integer with . The probability that Tolerant RAA ends with a marked element satisfies
With the smallest non-negative integer such that , for every ,
In the order of the proofs: Fact 1 (the error operator kills and has norm on states with clean registers ); the one-level bound ; the two trigonometric inequalities on ; the surrogate bound ; Lemma 1; the three terms of the drift recursion (5); and the accumulated drift .
Lemma 2 turns any family of approximate reflections whose error decays like into a search procedure that succeeds with constant probability, needs only a lower bound on , and costs calls. Combined with the phase-estimation reflection of the paper's Theorem 6 it yields Theorem 3, the general quantum-walk search theorem that has become the standard tool for walk-based algorithms (element distinctness, triangle finding, group commutativity). Nothing in the lemma refers to Markov chains, so it applies to any setting with an approximate reflection about the initial state.
The results are proved in the paper. None of them is machine-checked: the platform holds a formal Grover search with one marked basis state and exact reflections, but no amplitude amplification with approximate or recursive reflections. A formal proof would also settle the steps the paper passes over quickly, notably that the trigonometric inequalities, claimed for angles in , are applied to the actual angles , which may exceed by at the last level.
The ideal analysis (every reflection exact, angle tripled at each level) is a two-dimensional rotation argument. With approximate reflections the state leaves the plane spanned by and , and each level both triples the error already present and injects a new one; the errors stay bounded only because converges and the injection at level is weighted by . Fact 1 is not a restatement of the hypothesis on : it holds only because step 4 flips the phase of states whose earlier registers are dirty, and because never touches . In Lemma 2 the attempts reuse the leftover state, not a fresh , so the state at the decisive attempt has drifted; bounding the drift needs the normalised unmarked parts to move little from level to level, which again depends on the error bounds of Lemma 1.
EuclideanSpace ℂ (X × X × ((j : Fin T) → κ (j+1))); operators are complex matrices. Registers are 0-based in Lean (index is ).Real.arcsin; the interval is closed.Contributions welcome: proofs of the trigonometric milestones and of (pure real analysis), Fact 1 (finite-dimensional linear algebra with a block structure on registers), and the vector inequality that the drift bounds share. The register and controlled-unitary infrastructure is reusable for other recursive quantum algorithms.
Scheduling jobs whose durations are uncertain is the normal situation in project management, manufacturing and computing: a job's processing time becomes known only when the job finishes, but a distribution for it is available in advance. Stochastic machine scheduling models this by random, independent processing times and asks for a scheduling policy, a rule that decides online which jobs to start, using only the information observed so far, that minimizes the expected total weighted completion time . Optimal policies are known only in a few special cases, and they can depend on the full conditional distributions of the remaining processing times, so the research focus has been on simple policies with provable performance guarantees.
Skutella and Uetz (SIAM J. Comput. 34(4), 2005) gave the first constant-factor guarantees for stochastic parallel-machine scheduling with precedence constraints. Their policies are list scheduling policies whose priority list comes from an optimal solution of a linear program built on the load inequalities of Möhring, Schulz and Uetz (J. ACM 46(6), 1999). This mission formalizes their second main result: for in-forest precedence constraints and no release dates, plain Graham list scheduling in LP order is a -approximation.
Timeline.
There are a finite set of jobs, identical parallel machines, and nonnegative weights . Jobs are processed nonpreemptively; each machine handles one job at a time. Precedence constraints form an acyclic digraph : an arc means starts only after completes. The constraints form an in-forest if each job has at most one successor. There are no release dates.
The processing times are independent random variables. A realization is a vector ; a schedule assigns start times , with completion times ; it is feasible if it respects precedence and at most jobs are in process at any time. A policy maps each realization to a feasible schedule, and it is nonanticipatory if what it has started by time depends only on what has been observed by (the processing times of completed jobs and which jobs are still running).
With and a common bound with (i.e. ), define
The LP-relaxation minimizes subject to for all , for arcs , and . A priority list sorts the jobs by nondecreasing ; is the set of jobs up to and including in , and the jobs after .
Graham's list scheduling starts, at every decision time, as many available jobs as possible in the order of . For a schedule, a critical predecessor of is a predecessor that completes last among 's predecessors, at a positive time; following critical predecessors backwards gives the critical chain of , whose total processing time is .
For every feasible nonanticipatory policy ,
The theorem gives a constant performance guarantee for stochastic in-forest scheduling, uniform in the distributions once their coefficients of variation are bounded. For NBUE distributions (exponential, uniform, Erlang, …), where , the guarantee is , compared with for general precedence constraints and release dates with Algorithm CMNS (Table 1, p. 792). The analysis shows that for in-forests, deliberate idle time is unnecessary: Lemma 4.3 replaces it.
The result is proved in the paper, partly by reference: Theorem 3.1 and Lemma 3.3 are cited from Möhring, Schulz and Uetz. To our knowledge none of these results has a machine-checked proof. A complete formalization requires the load inequalities of stochastic scheduling, which are of independent use for every LP-based stochastic scheduling result, and a reusable treatment of list schedules, critical chains and nonanticipatory policies.
Two parts carry the weight. The first is the load inequalities (Theorem 3.1): they hold for nonanticipatory policies only, because a policy's start time of job must be independent of ; turning the informal "dynamic view" of policies into a statement that yields this independence, and then the variance bookkeeping, is the probabilistic core. The second is Lemma 4.3: the naive argument "a waiting job of high priority blocks lower-priority jobs" fails for general precedence constraints, where Graham's algorithm can be arbitrarily bad; the in-forest structure is used through a counting argument at time , in which the critical predecessors of the jobs started at that time must be distinct.
Lean represents jobs by a Fintype V, precedence by a relation A : V → V → Prop with acyclic transitive closure, and in-forests by "at most one outgoing arc". Schedules are start-time vectors in ℝ, with machine capacity by counting jobs in process on half-open intervals. Policies are maps from realizations to start times with an explicit nonanticipation condition. Graham's list scheduling is characterized by rules (feasibility, greedy, list order, decision times); critical chains are taken for every admissible tie-breaking selector. The CV bound includes and . Zero processing times are allowed.
Standing assumptions and disclosed additions: processing times are independent and nonnegative; the comparator policies have integrable completion times; the completion times and critical-chain lengths of Graham's schedule are assumed almost-everywhere measurable (the paper asserts measurability in §5 without proof); "-approximation" is stated against every comparator policy rather than an optimal one.
A trivializing formalization is ruled out: the comparator ranges over every feasible nonanticipatory policy with integrable completion times, is optimal over all load inequalities , and the Graham family must satisfy the rules for every nonnegative realization.
Welcome contributions: the load inequalities, existence and measurability of Graham schedules, and general lemmas on list schedules.
In a one-stage stochastic program a decision maker observes a random outcome and then picks a decision , subject to constraints that depend on , so as to minimize expected cost. The optimization variable is a whole function , and computing the optimal value is #P-hard even for a uniform distribution on the unit cube (Dyer and Stougie, 2006, cited in the paper as [16, Theorem 3.2]). A standard tractable approximation, introduced for robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004) and carried to stochastic programming by Shapiro–Nemirovski and Chen–Sim–Sun, restricts decisions to linear decision rules . This restriction gives an upper bound on the optimal value.
Kuhn, Wiesemann and Georghiou (2009/2011) study these approximations systematically. Their §3 treats the case where the constraint matrix itself depends on (random recourse). Linear decisions then produce constraints that are quadratic in , and the paper reformulates the resulting semi-infinite problem as a semidefinite program. This mission formalizes that reformulation, the primal half of the paper's Theorem 2.
Uncertainty is a probability measure on , with outcomes . The support of is the smallest closed set of probability one. It is assumed to have the form
for symmetric matrices , where is the first standard basis vector. The first coordinate of every outcome is therefore , so linear functions of are affine functions of the remaining coordinates. is assumed nonempty and bounded, and its linear hull is assumed to be . Let denote the symmetric matrices and the second-moment matrix.
The data are (cost ), (right-hand side , with rows ), and , where the th row of the recourse matrix is . The stochastic program minimizes over square-integrable subject to almost surely. It is strictly feasible if some square-integrable and some satisfy and almost surely.
With linear decisions and quadratic slacks , , one obtains the primal approximation
and the SDP (3.14)
The theorem replaces a problem with infinitely many constraints, one per outcome, by a semidefinite program with variables. Its value is always an upper bound on , and hence on . When the support is a single ellipsoid in the hyperplane (), the bound loses nothing beyond the restriction to linear decisions. For the gap is unavoidable in general: an exact tractable reformulation would decide copositivity, which is NP-hard (Remark 7). Random recourse arises whenever technology or yield coefficients are uncertain, for example in production planning and portfolio problems with uncertain returns.
The result is proved in the paper. As far as is known it has no machine-checked proof. A formalization adds a precise statement of the hypotheses. Writing those hypotheses out showed that the unnumbered §3.2 step needs to have dimension , which spanning alone does not give for nonconvex (see Formalization scope). The other half of Theorem 2, about the lower-bounding SDP (3.18), is false in this preprint and is not part of the mission.
The semi-infinite constraints hold only -almost surely. The first step is to pass from "almost surely" to "for every ", which uses that is exactly the support and that the constraint functions are continuous. A bound alone is not enough. For the equality constraints, a quadratic form that vanishes on must vanish identically. This requires to be large enough, and the obvious argument from " spans " fails when is a finite set. For the inequality constraints with , the implication must be established on all of and not only on the slice . Doing so needs boundedness of (no recession directions) and a strictly feasible point for the S-lemma. The S-lemma itself is a nonconvex duality statement. It is available on the platform.
Outcomes live in Fin k → ℝ, with carried in the setting. Indices are 0-based: is coordinate 0, and range over Fin m, Fin l. " is the support of " is stated as: is closed, , and every ball centred in has positive measure. Mathlib has no Measure.support at this revision. The standing assumptions (probability measure, symmetric , support, nonempty, bounded, spanning) form one predicate assumed by every theorem. Decision rules are Borel measurable square-integrable functions. Optimal values are infima in EReal, for an empty feasible set and for an unbounded one. "Equivalent" means equal optimal values. Each is required symmetric in both problems; is positive semidefiniteness and is componentwise. Strict feasibility of in §3 is the paper's condition (2.9) of §2 with replaced by . The paper uses the phrase without restating it.
Repairs and narrowings:
The goal cannot be trivialized through its definitions. Feasibility is quantified -almost surely for a measure whose support is , not over an empty or arbitrary set. Both optimal values are infima of the same real objective over the problems' own feasible sets. The standing assumptions are satisfiable, for instance by , , and the uniform law on .
The definitions (support of a measure, decision rules, the random-recourse data) are reusable for the other sections of the paper and for related work on decision rules. Proofs of any milestone, Lean lemmas on quadratic forms vanishing on open cones, and an almost-sure-to-support transfer lemma are welcome.
Quantum walks give quadratic speed-ups for a class of search problems that classical algorithms solve by running a Markov chain until it hits a marked state. Ambainis's element-distinctness algorithm (Ambainis 2007) and Szegedy's quantization of reversible Markov chains (Szegedy 2004) are the two starting points. Magniez, Nayak, Roland and Santha (arXiv:quant-ph/0608026v4, SIAM J. Comput. 2011) combined them into one search algorithm whose cost is governed by the eigenvalue gap of a reversible chain .
For a non-reversible chain the relevant spectral quantity is not the eigenvalue gap of . It is the singular value gap of a related matrix, the discriminant . In §5 the paper observes that its search algorithm and the proof of its main theorem carry over to non-reversible chains once the eigenvalue gap of is replaced by the singular value gap of . Positivity of that gap therefore decides whether the algorithm can be used at all. The paper also notes that irreducibility, and even ergodicity, does not guarantee a positive gap. Its Proposition 3 (p. 17, proved in the appendix on pp. 20–21) gives a simple sufficient condition: every state has a positive probability of staying where it is. This mission formalizes that proposition.
Let be a finite set of states. A Markov chain on is a real matrix with nonnegative entries whose rows sum to one; is the probability of moving from to . The graph underlying has an edge whenever . The chain is irreducible if this graph is strongly connected, so that every state can be reached from every other state.
A stationary distribution of is a vector with
Every irreducible chain has exactly one.
The discriminant of is the matrix
viewed as an operator on with the inner product . Its singular values are the square roots of the eigenvalues of , repeated according to multiplicity. The vector satisfies and , so is always a singular value of . When is reversible, is symmetric and its singular values are the absolute values of the eigenvalues of . In general the two can differ.
If is an irreducible Markov chain on a finite state space with for every , then has exactly one singular value equal to :
Together with the bound below, this says that , i.e. the singular value gap is positive. The goal asserts no explicit lower bound on the gap, so it does not depend on any quantitative estimate.
The result. Proposition 3 is what makes the search algorithm of the paper usable with non-reversible chains. Theorem 8 of the paper bounds the cost of finding a marked element in terms of the singular value gap of , and it needs that gap to be positive. The hypothesis costs little: replacing by for any makes every self-loop positive and keeps the stationary distribution. The proposition also connects to the classical study of non-reversible chains: the squared singular values of are the eigenvalues of the multiplicative reversiblization , which Fill (1991) used to bound convergence to stationarity.
Formalizing it. The proposition and its proof are in the paper and are not in dispute. To our knowledge neither is machine-checked anywhere. The work is a formal proof of the known argument. It exercises Mathlib's recently added singular values of linear maps between finite-dimensional inner product spaces and its theory of irreducible nonnegative matrices, in a setting where the matrix is neither symmetric nor normal.
The obvious route goes through eigenvalues. Irreducibility plus self-loops make aperiodic, so by Perron–Frobenius the eigenvalue of is simple and every other eigenvalue has modulus less than . This does not settle the question. The singular values of a non-normal matrix are not the moduli of its eigenvalues, and the paper points out ergodic chains whose discriminant has zero singular value gap even though their eigenvalue gap is positive. Simplicity of the eigenvalue of therefore says nothing about the multiplicity of the singular value of .
The real content is the equality case of a Cauchy–Schwarz inequality in . It has to be translated into an edge-by-edge relation between the coordinates of the left and right singular vectors, then propagated along directed paths of the chain's graph. The self-loops are what identify the left and right singular vectors with each other. Bookkeeping that is routine on paper costs effort here: passing between the eigenvalue sequence of and the dimension of its -eigenspace, and between paths in Mathlib's quiver of positive entries and chains of equalities.
Fintype with decidable equality. is a real matrix in Matrix.rowStochastic ℝ X, and irreducibility is Mathlib's Matrix.IsIrreducible (nonnegative entries and a strongly connected quiver with an edge iff ). For a row-stochastic matrix this agrees with "every state is reachable from every other state".EuclideanSpace ℂ X. Its singular values are Mathlib's LinearMap.singularValues, a sequence indexed by that is beyond . The goal counts the indices with . The inner product is Mathlib's inner ℂ u (D(P) w). Since the equality-case milestone assumes this equals exactly, no phase ambiguity remains.Matrix completion asks to recover a large matrix from a small number of its entries. It is the abstraction behind collaborative filtering (recommender systems in which a users × items rating matrix is observed on a sparse set of pairs), sensor localization from partial distance information, and system identification. Without structure the problem is hopeless; the standard structural assumption is that the unknown matrix has low rank, and the standard convex surrogate for rank is the nuclear norm, the sum of singular values.
In the noiseless case, exact recovery by nuclear-norm minimization from about uniformly sampled entries was established by Candès and Recht (2009) and refined by Candès and Tao (2010) and Gross (2011). With noisy observations the relevant question is a rate: how fast does an estimator's error decrease with the number of observed entries? Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256, Ann. Statist. 2011) introduced a nuclear-norm penalized estimator that uses the known sampling distribution, showed that in matrix completion it is an explicit soft thresholding of the singular values of a rescaled data matrix, and proved for it sharp oracle inequalities (leading constant 1) whose rates are optimal up to logarithmic factors. This mission formalizes the version of that result for bounded responses: Theorem 4 of the paper, together with the probabilistic lemma and the matrix Bernstein inequality it rests on.
Fix positive integers and write for the real matrices, with scalar product , Frobenius norm , nuclear norm (sum of singular values) and operator norm (largest singular value). Set and write .
The matrix completion basis is
where are the canonical basis vectors of . One observes independent random pairs , where is uniformly distributed on and is real, following the trace regression model
for an unknown . Thus is a noisy reading of the entry of selected by ; this is matrix completion under uniform sampling at random (USR), entries possibly sampled more than once.
The estimator is, for a regularization parameter ,
The stochastic error is the random matrix
Assume almost surely. For and
with probability at least , simultaneously for all ,
Theorem 4 is a non-asymptotic, sharp oracle inequality: the leading constant in front of is 1, so the bound applies to misspecified targets ( not low rank) without loss. Taking and of order gives a normalized Frobenius error of order , which the paper's minimax lower bounds (§4) show to be optimal up to the logarithm. Because no model is needed for Lemma 1, the same probability bound also drives the paper's statistical-learning reformulation (Theorem 9).
The theorems here are proved in the paper. What is open is their formalization: no matrix Bernstein inequality, and no oracle inequality for nuclear-norm penalized estimators, has a machine-checked proof on this platform. Proposition 1 in particular is a reusable concentration tool well beyond this paper (covariance estimation, random graphs, sketching).
The deterministic part (milestone 2) needs the subdifferential of the nuclear norm, which is not in Mathlib. The probabilistic part is where the obvious argument fails. Bounding entrywise and summing, or bounding it by the Frobenius norm, loses a factor polynomial in the dimension; a union bound over a net of the unit sphere loses the factor that makes the rate optimal. The correct rate requires a noncommutative Bernstein inequality, controlling the operator norm of a sum of independent random matrices through the matrix variance at the price of only a factor. The matrix-analytic machinery such inequalities depend on (trace inequalities for matrix exponentials, the passage from rectangular to symmetric matrices) is not currently available in Mathlib.
All objects are local to the namespace KLTNuclear.Completion, built on the published MatrixCompletion definitions (RealMatrix, nuclearNorm, spectralNorm, frobeniusNormSq, matrixInner, coordinateMatrix). Conventions:
IsProbabilityMeasure; are hypotheses. is the natural logarithm; .Matrix, so measurability, independence and conditioning on a random matrix use its entry array with the product -algebra; expectations of matrices are entrywise.The source is the arXiv preprint arXiv:1011.6256v4. Welcome contributions: a general matrix Bernstein inequality (Hermitian and rectangular forms), the nuclear-norm subdifferential, and proofs of the deterministic milestone.