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.
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?
Potential games (Monderer and Shapley, 1996) are the finite games whose unilateral payoff differences are all differences of a single function, the potential. They always have a pure Nash equilibrium, and many natural learning dynamics (best response, fictitious play, logit response) converge in them. Most games met in applications are not exactly potential games, so a recurring question is how much of this theory survives for a game that is close to a potential game.
Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405, journal version Math. Oper. Res. 36(3), 2011) decompose the space of finite games into potential, harmonic and nonstrategic components. Section 6 of the paper equips the space of games with a weighted inner product under which this decomposition is orthogonal, computes the closest potential game to any game in closed form, and shows that approximate equilibria of a game and of its closest potential game correspond, with an explicit loss controlled by the distance between them. This mission formalizes that last result together with the statements it rests on.
A finite game has a finite set of players ; each player has a nonempty finite strategy set with elements, and a utility on the set of strategy profiles . For a profile , denotes with player 's strategy replaced by .
A profile is an -equilibrium if for every player and strategy (equation (2) of the paper). A game is a potential game if there is with for all , , , (Definition 2.1).
A game is identified with its tuple of utilities, an element of where . The game graph has the profiles as nodes, with an edge between two profiles that differ in exactly one player's strategy. The operator sends to its differences along the edges where player deviates, , is the gradient of the game graph, , and is the Moore–Penrose pseudoinverse. Definition 4.2 defines the potential, harmonic and nonstrategic subspaces
and a harmonic game is a game in .
Section 6 introduces the weighted inner product and norm
A closest potential game to is a potential game with for every potential game ; a closest harmonic game is defined in the same way.
Let be the closest potential game to and . Then for every , every -equilibrium of is an -equilibrium of , and every -equilibrium of is an -equilibrium of , where
The result. Theorem 6.3 reduces the study of approximate equilibria of an arbitrary finite game to a potential game, where pure equilibria exist and are maximizers of the potential. Section 7 of the paper reports that, in a companion paper, best-response and fictitious-play dynamics are shown to converge to a neighbourhood of equilibria in near-potential games, with the size of the neighbourhood governed by the distance of the game to its closest potential game. Theorems 6.1 and 6.2 make that distance computable: the closest potential game is an orthogonal projection, given by linear operators of the game graph.
Formalizing it. All four statements are proved in the paper; none of them is machine-checked anywhere known to this mission. A formal development produces a verified operator layer for games on the game graph (gradient, pseudoinverses, the projections ), a verified proof that the weighted inner product, and not the unweighted one, makes the decomposition orthogonal, and a reusable perturbation lemma for -equilibria.
Lemma 2.1 and the final step of Theorem 6.3 are elementary inequalities. The obvious way to approximate a game by a potential game, taking the identical-interest part of its zero-sum/identical-interest split, does not give the closest potential game: the paper's Table 7 (p. 35) shows a potential game whose identical-interest part is far from it. The closest potential game has to come from the projection of Section 6. The weight of the mission is in Theorems 5.1, 6.1 and 6.2. They need the decomposition theorem of Section 4 (every game splits uniquely into , , ) and properties of pseudoinverses of the operators and that Mathlib does not provide: Mathlib has no operator pseudoinverse at all. The orthogonality under the weighted product rests on the specific spectral structure of the Laplacian of the graph of a single player's deviations; it is not a general fact, and it fails for the unweighted product when the differ, so the standard orthogonal-complement machinery cannot be applied to with its default inner product.
Players are a finite type ι with decidable equality; strategy sets are finite types E m. Utilities are plain functions u : ι → (∀ m, E m) → ℝ, the shape used by the published MondererShapley.ClosedPath.IsPotentialGame, which is referenced for Definition 2.1. The operator layer works in PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)) with the unweighted inner product of Section 4; edge flows carry the inner product of (7). The weighted inner product (55) and norm (56) are plain functions, not a second instance on the same type. "Closest" is the minimizing property itself, not an infimum of distances.
Hypotheses made explicit: every strategy set is nonempty (the paper's ), so ; in Theorem 6.3 the set of players is nonempty, which the maximum over players needs. The paper's "an -equilibrium for some " is stated as "a -equilibrium", which is equivalent because (2) is monotone in . Both directions of Lemma 2.1 and Theorem 6.3 are included.
The goal is stated for the closest potential game, as printed. A version for an arbitrary potential game at distance would be a different theorem, and the hypothesis is not vacuous: Theorem 6.2 shows the closest potential game exists. Theorem 6.2 is stated as an "if and only if" characterization, so it gives existence and uniqueness as well as the formula.
Contributions welcome: the Penrose identities for the pseudoinverse, the identities and , and the decomposition theorem of Section 4, all of which are reusable by the other missions of this series.
Many estimation problems ask for a low-rank matrix from far fewer linear measurements than it has entries: matrix completion, quantum state tomography, recovery of positions from partial distances. The rank minimization problem subject to is NP-hard, so one solves a tractable surrogate instead, either the nuclear-norm minimization subject to or an iterative scheme such as the iteratively reweighted least squares algorithm IRLS-M of Fornasier, Rauhut and Ward (arXiv:1010.2471).
Guarantees for these surrogates rest on conditions on the measurement map. Two are standard. The restricted isometry property (RIP) asks that nearly preserve the Frobenius norm of every low-rank matrix; it holds with high probability for many random maps, and it is what one can verify in practice. The null space property asks that no nonzero matrix in the kernel of be concentrated on few singular directions; it is what the recovery proofs actually use. This mission formalizes the bridge between them in the paper's form: a small restricted isometry constant implies the strong rank null space property (SRNSP) that drives the convergence analysis of IRLS-M.
Timeline.
Fix integers . A measurement map is a linear map ; it is given by matrices through , where . The Frobenius norm is , the nuclear norm is the sum of the singular values of , and is the Euclidean norm of the vector . A matrix is -rank if its rank is at most .
The restricted isometry constant (Definition 1.1) is the smallest such that
The map has the strong rank null space property of order with constant (Definition 6.4) if for every and every decomposition with -rank, there is another decomposition with , , , , and
In Lean these are IRLSM.RIP.ripConst A k, IRLSM.RIP.SRNSP A k η and IRLSM.RIP.measSq A X , built on the published module HighDimStat_MatrixRank_Core (traceInner, frobeniusNorm, nuclearNorm, observationOp).
If and
then satisfies the SRNSP of order with constant
The constant is the paper's explicit one; the goal asserts the full property for every kernel element and every decomposition, including .
The result. Proposition 6.8 is the step that turns a verifiable, probabilistically typical hypothesis (a small rank restricted isometry constant, which Gaussian and many other random maps satisfy once is of order ) into the deterministic null-space hypothesis under which the paper proves that IRLS-M converges to the nuclear-norm minimizer and recovers every -rank matrix exactly (Theorem 6.11, Proposition 2.1). Through Lemma 6.6 and Corollary 6.7 of the same paper, the SRNSP also gives stable recovery by nuclear-norm minimization, with error controlled by the best -rank approximation error in the nuclear norm.
Formalizing it. The result is proved on paper; it has no machine-checked proof that we know of. A complete development supplies the rank restricted isometry constant as a usable object (its monotonicity, its polarization estimate Lemma 6.9), the nuclear norm's additivity on orthogonal pieces, its comparison with the Frobenius norm, and the block-splitting of the singular value decomposition. These tools are reusable across low-rank recovery. The sibling mission of this series, IRLS-M Converges to the Nuclear-Norm Minimizer Under the Strong Rank Null Space Property, takes the SRNSP as its hypothesis; together the two give Proposition 2.1 of the paper.
The obvious argument would bound directly by the restricted isometry inequality, but that inequality controls only Frobenius norms of low-rank matrices, while the kernel element has full rank in general and the property is stated in nuclear norms. The restricted isometry hypothesis therefore cannot be applied to , or to , as a whole, and the constant depends on how the high-rank part is handled. In Lean, the singular value decomposition of a rectangular matrix and the behaviour of singular values under block operations are the main missing infrastructure: Mathlib has the spectral theorem for Hermitian matrices but little on singular values of rectangular matrices.
Matrix (Fin n) (Fin p) ℝ; the paper treats real and complex matrices indifferently. is and is traceInner.observationOp); is a sum of squares, not Mathlib's sup norm on Fin m → ℝ.n ≤ p assumption: the proof does not use it.A formalization that proved only , or only the existence of some decomposition without the bound , or that defined as any admissible constant rather than the smallest one, would not be this mission's goal.
Welcome contributions: singular value decomposition for rectangular real matrices in the Core encoding, singular values of block-diagonal and orthogonally-equivalent matrices, and proofs of the milestones in any order.
Network data often come as a single observed graph, and the simplest summary of a graph is its degree sequence, the list of the numbers of neighbours of its vertices. A statistical model in which the degree sequence is a sufficient statistic is an exponential family on graphs, and the simplest such family is the β-model: each vertex carries a parameter , and edges appear independently with log-odds . The model appears in the directed case in Holland and Leinhardt (1981), in the undirected case in Park and Newman (2004) and Blitzstein and Diaconis (2011), and it is a close relative of the Bradley–Terry model for paired comparisons.
Fitting the model means solving the maximum likelihood equations. The difficulty for classical theory is that the number of parameters, , equals the number of vertices: the parameter dimension grows with the sample, and standard consistency arguments for maximum likelihood do not apply. Chatterjee, Diaconis and Sly (2011) prove that, nevertheless, for parameters in a fixed bounded range the maximum likelihood estimate exists, is unique, and estimates every coordinate of uniformly at rate , with probability . This mission formalizes that result (Theorem 1.3 of the paper) and the lemmas of §4 on which its proof rests.
Let and . The β-model is the law of the random simple graph on vertices in which, for each pair , the edge is present with probability
independently of all other edges. Write for the degrees of . The maximum likelihood equations for an estimate are
The sup norm is .
Two further objects enter the proof. is the set of degree sequences of simple graphs on vertices and the set of expected degree sequences of as ranges over . For and the slack is
which is nonnegative for every degree sequence of a graph (the Erdős–Gallai inequalities). Finally , , is the map whose fixed points are the solutions of (3).
For every there is such that for every and every with ,
The constant depends only on , and the statement holds for all , small being absorbed into .
The theorem is a consistency result in a regime where the number of parameters is as large as the number of nodes, and it comes with a uniform rate: every vertex parameter is recovered to accuracy simultaneously, from one graph. Existence of the MLE is itself not automatic (it fails, for instance, whenever the observed graph has an isolated vertex), so the theorem also says that the estimator is defined with high probability. The paper uses the same machinery for its graph-limit results on uniform random graphs with a given degree sequence (missions 4–5 of this series), and the β-model is the base case of a large family of exponential random graph models used in network analysis.
The result is proved in the paper; this mission produces the machine-checked version. None of the statements here is formalized on the platform or in Mathlib. Theorems 1.4 and 1.5 are the goals of missions 2 and 1 of this series and are restated here; a proof there transfers directly.
Standard maximum likelihood asymptotics fix the parameter dimension and let the sample size grow; here both grow together, and the ratio of squared dimension to number of observations, , stays bounded, so the usual heuristic for when asymptotics apply is borderline at best. The likelihood is concave, but concavity alone gives neither existence of a maximizer (the supremum may be approached at ) nor a bound on its size that is uniform in . The central step, Lemma 4.1, is a deterministic bound on that does not depend on ; it requires control of how the coordinates of can spread out, expressed through a quantitative Erdős–Gallai margin. A coordinatewise argument cannot give it, because each equation of (3) involves all coordinates.
Vertices are Fin n, graphs are SimpleGraph (Fin n) with the discrete σ-algebra, and is the finite sum of point masses with the independent-edge weights ; vectors are Fin n → ℝ with Mathlib's sup norm. Probabilities are values of this measure in , compared with . Expected degrees are integrals against ; is not defined as the range of the right-hand side of (3), since that identification is part of the content of Theorem 1.4.
Every "constant depending only on …" is a quantifier placed before : in Theorem 1.3, depends on only; in Lemma 4.1, is a function of alone, bounded on compact subsets of its domain, as §4 defines the phrase; in Lemma 4.2, on and on . Choosing after and would make Theorem 1.3 trivial, since for large ; this formalization rules that out. The paper's is the hypothesis , and the paper's is the bound for every admissible (a finite nonempty family). The phrase "there exists a unique solution … that satisfies [the bound]" is read as: a solution exists, it is unique, and it satisfies the bound. Lemma 4.1 assumes , not (for existence would be immediate). Theorem 1.5 is stated, as in mission 1, for and .
A complete development needs: the β-model as a measure and its exponential-family formula; Hoeffding's inequality for sums of independent non-identical indicators transported to (Mathlib has Hoeffding for independent bounded variables); compactness in ; and the results of missions 1 and 2. The β-model measure and the Erdős–Gallai slack are reusable beyond this mission. Proofs of any milestone, and of the transfer between the independent-edge and the product-space descriptions of , are welcome.
A random conductance model puts a random conductivity on every edge of the lattice . It is the simplest discrete model of diffusion in a heterogeneous medium, and its generator is the generator of a random walk in a random environment. Classical stochastic homogenization shows that on large scales the random operator behaves like a constant-coefficient elliptic operator whose homogenized coefficient is deterministic. The characterization of , however, involves an equation on the whole lattice for every realization of the coefficients. In practice one computes a spatial average over a box of size of the energy density of an approximate corrector, as in Gloria and Otto (arXiv:1104.1291, §1). The random part of the error of this procedure is a variance. Its size as a function of determines how large a computational box must be.
Timeline:
Fix and . Sites are and is the canonical basis. An edge carries a conductivity ; such a field belongs to the class . The discrete gradients are and , and .
The conductivities are i.i.d.: they are distributed according to the product over all edges of one probability law on . No density is assumed, so atomic laws are allowed. is the expectation and the variance.
For a direction with and a cut-off , the approximate corrector solves
The zero-order term introduces the length scale . The Green's function is the solution of in weak form.
A mask is supported in the box , sums to and satisfies . The averaged energy density is
There are an exponent and a threshold , depending only on , and for each mask constant a constant , such that for every law on , every unit , every , every and every mask :
The statement fixes the shape of the bound, not the value of or , which is why it is the goal.
The milestones follow the paper's proof:
The result. The estimate says that smooth averages of the energy density fluctuate as if the density were independent from site to site, at the rate . That rate is the best possible, since the coefficients themselves are independent. In the error analysis of approximations of , this controls the random error and separates it from the systematic error caused by the cut-off . Proposition 2.1, a byproduct, shows that the approximate corrector has all moments bounded uniformly in when , which yields a stationary corrector (Corollary 2.1 of the paper).
Formalizing it. The theorem has been proved since 2011, and no machine-checked version is known. A formal proof would combine three components that are reusable well beyond this paper:
The obvious argument fails because the energy density is not independent from site to site: the corrector couples all conductivities through the inverse of a random elliptic operator. Bounding the variance needs the sensitivity of to each single conductivity, and that sensitivity is expressed through gradients of the Green's function. Pointwise bounds on that are uniform in the coefficients do not exist: the continuum counterpart fails, by examples from quasi-conformal mappings. Only averaged decay on dyadic annuli and a small gain of integrability are available, which is why the proof needs the moment bounds of Proposition 2.1. In the Green's function does not decay, so only BMO-type control is available, and a logarithm of is lost.
Statements follow the arXiv v1 reprint (arXiv:1104.1291v1) of the Annals of Probability article; theorem and page numbers refer to it.
Fin d → ℤ. An edge is the pair (z, i), and a coefficient field is a real function on edges; the theorems assume it takes values in .Measure.infinitePi of one probability measure on with .Ruling out a trivial formalization. If the constant were allowed to depend on the law or on the mask, the goal would follow from the boundedness of the energy average alone. If the variance were taken of a function that is not square-integrable, it would be by convention. The goal fixes before and and requires square-integrability as part of the conclusion.
Not formalized:
Welcome contributions are proofs of any milestone and reusable infrastructure: infinite-product variance inequalities, discrete integration by parts, and discrete maximum principles.
A standard way to build a random network with a prescribed degree sequence is to choose a graph uniformly at random from the set of all simple graphs with that degree sequence. The model arises in testing whether the exponential family with the degree sequence as sufficient statistic fits network data, in simulating networks with given degrees, and, for constant degrees, as the random regular graph (Blitzstein–Diaconis, Chatterjee–Diaconis–Sly). Quantities such as the expected number of triangles of such a graph are usually estimated by simulation.
For dense graphs, those whose number of edges is of order , the Lovász–Szegedy theory of graph limits (Lovász–Szegedy 2006) describes a large graph by a symmetric function . Chatterjee, Diaconis and Sly identify this limit for uniformly random graphs with a given degree sequence. The answer is the limit of the β-model, a random graph with independent edges whose edge probabilities are . The limit gives exact asymptotic formulas for subgraph counts without simulation.
Graphs and densities. For a finite simple graph on and a simple graph on vertices, the homomorphism density is
where is the set of edge-preserving maps . For ,
with one factor per edge. Graphs on vertices converge to the limit represented by if for every finite simple graph .
Degree sequences and scaling limits. For each let be the degree sequence of some simple graph on vertices. The sequence has scaling limit , a nonincreasing function on , if
is the set of nonincreasing functions on that are left continuous on . It carries the modified norm . is the set of all scaling limits of degree sequences.
The random graphs. is chosen uniformly from the simple graphs on with degree sequence . In a random graph with independent edges each pair is an edge with probability , independently of the other pairs. The β-model is the case .
If lies in the interior of for , there is a function , unique on , such that
and almost surely for every finite simple graph .
The proof also uses three results posed in sibling missions of this series: Proposition 1.2 (mission 4, the interior of ), Lemma 4.1 (mission 3, existence and boundedness of the MLE) and Theorem 1.5 (mission 1, geometric convergence of the iteration ). They are not restated here.
The theorem turns questions about a uniformly random graph with given degrees, a law with no independence, into questions about an explicit graphon. Every subgraph density, the limiting degree distribution, and every graph parameter continuous for the graph-limit topology of the uniform model is computed from . The function solves a continuum version of the β-model maximum-likelihood equations, which connects the combinatorial model with exponential-family statistics.
The result is proved in the paper, which is published in the Annals of Applied Probability (2011). To our knowledge it has no machine-checked proof. Formalizing it requires a Lean development of dense graph limits (homomorphism densities, graphon densities, graph-limit convergence), none of which exists in Mathlib. It also requires a bounded-differences concentration inequality, and a transfer argument from independent-edge models to models conditioned on degrees. Each of these is reusable beyond this mission.
The uniform measure on graphs with a fixed degree sequence has no independence, so concentration inequalities do not apply to it directly. The obvious route is to condition an independent-edge model on its degree sequence. This works only if the probability of the conditioning event is larger than the concentration bound, which is . A crude lower bound of is too small. Lemma 6.2 supplies , and it needs a combinatorial completion step (Claim 6.3).
The second difficulty is analytic. The maximum-likelihood parameters for different live in different dimensions. One must show that their step-function profiles converge in to a limit and that this solves the continuum equation at every point of , not only almost everywhere. Several steps of the paper's argument are only sketched. Among them are the almost-sure convergence of the β-model graphs to and the estimate (pp. 33–34).
Fin n (the paper's vertex is ), graphs are SimpleGraph (Fin n), and a test graph is a SimpleGraph (Fin k), which loses nothing because densities are invariant under relabelling.ℝ → ℝ, and only their values on matter. Uniqueness of is equality on .SimpleGraph (Fin n) is discrete.A formalization that replaces almost-sure convergence by convergence in expectation or in probability, that fixes a single coupling, or that asserts the existence of only almost everywhere states a weaker theorem and does not close this mission.
Welcome contributions include a general graph-limit library (densities, convergence, the counting lemma), McDiarmid's bounded-differences inequality for finitely many independent Bernoulli variables, the Gale–Ryser theorem in the form needed by Claim 6.3, and proofs of the milestones.
A degree sequence records how many neighbours each vertex of a graph has. In network statistics it is often the only summary of a graph that is observed or trusted, and the natural probability models for graphs in which "the degree sequence captures the information" are exponential families whose sufficient statistic is the degree sequence. Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 2011) call the resulting model the β-model and study its maximum likelihood theory and its use for sampling random graphs with a prescribed degree sequence.
For any exponential family, the first question about estimation is which values of the sufficient statistic can be matched by a parameter: the maximum likelihood equations say exactly "the expected statistic equals the observed one". Theorem 1.4 of the paper answers this for the β-model. Up to taking a closure, the expected degree sequences of the β-model fill the whole convex hull of the degree sequences. The paper notes that the result can also be derived from classical results on the mean space of exponential families (Barndorff-Nielsen 1978; Brown 1986; Wainwright and Jordan 2008, Theorem 3.3), and gives a self-contained proof in §3. Lemma 4.1 of the same paper uses Theorem 1.4 to show that the maximum likelihood estimator exists.
Fix and the vertex set . A graph is undirected and simple: no loops and no multiple edges. Its degree sequence is , and
is the finite set of all degree sequences. Its convex hull is a polytope in .
For , the β-model is the law of the random graph in which each pair , , is an edge with probability
independently of all other pairs. The expected degree sequences form the set
Two functions on appear in the proof. The first is with
The second is, for each ,
The Lean development names these objects betaModel, D, R, g and fy in the namespace GivenDegreeSeq.MeanPolytope.
The statement fixes no constants. The closure cannot be dropped: for the degree sequence of the empty graph lies in but not in , because every expected degree is positive.
and along some sequence. 7. The gradient (p. 16): .
The theorem describes the mean space of the β-model. Its interior contains every degree sequence that lies strictly inside the polytope, and for these sequences maximum likelihood estimation is well posed. The paper's consistency result (Theorem 1.3) and the existence part of Lemma 4.1 start from this description. The polytope is studied in its own right; its extreme points are the degree sequences of threshold graphs (Mahadev and Peled 1995).
Theorem 1.4 is proved, and as far as this mission's authors know it is not machine-checked anywhere. Formalizing it means turning the paper's short proof into a complete argument. That includes the steps the page dismisses as easy: the exponential-family formula for the independent-edge law, the expectation computation, the Hessian bound for , and the passage from a sequence of approximate critical points to the closure. Lemma 3.1, a descent-type gradient bound for a function bounded above, is a general fact of real analysis and is independent of graphs.
The inclusion is direct: an expectation is an average. The reverse inclusion is the content. For in the interior of the polytope, one would like to find with by maximizing the concave function . For on the boundary of the polytope, however, need not attain its supremum. So the argument cannot rely on the existence of a maximizer, and it has to produce points with without ever solving . Compactness arguments on fail for the same reason: the relevant sequences are unbounded.
Fin n, so the paper's vertex is the index . Graphs are SimpleGraph (Fin n), a finite type. Its σ-algebra is Mathlib's SimpleGraph.instMeasurableSpace, under which every set of graphs on Fin n is measurable.Fin n → ℝ, whose product topology is the Euclidean topology, so the closure is unambiguous. Gradients and Hessians are taken on EuclideanSpace ℝ (Fin n). There "twice differentiable" means that and its Fréchet derivative are differentiable, and the Hessian norm is the norm of the second Fréchet derivative, which equals the operator norm of the Hessian matrix.Contributions of any milestone are welcome. Lemma 3.1 and the gradient identity are self-contained calculus. The probability formula and the expected-degree identity are finite computations on graphs.
The capacitated vehicle routing problem (CVRP) asks for delivery routes from a depot that serve every client exactly once without exceeding a vehicle capacity, at minimum total length. It was introduced by Dantzig and Ramser in 1959 and is the reference problem of the vehicle routing literature: most exact methods for richer routing models (time windows, heterogeneous fleets, split deliveries) are first developed and benchmarked on it.
Exact CVRP algorithms are driven by the lower bound of a linear relaxation. Two families dominated before 2005. Branch-and-cut works with the edge variables and the rounded capacity inequalities (Lysgaard, Letchford and Eglese 2004, among others); its bound degrades as the number of vehicles grows. Lagrangean and column-generation methods work with q-routes, walks from the depot of bounded total demand that may revisit clients (Christofides, Mingozzi and Toth 1981). Fukasawa, Longo, Lysgaard, Poggi de Aragão, Reis, Uchoa and Werneck combine the two in one linear program over the intersection of the two polytopes, priced by column generation with every cut written on the edge variables. According to the abstract, the resulting branch-and-cut-and-price solves to optimality all instances from the literature with up to 135 vertices. The design is called robust because cuts are written on the edge variables and therefore never change the structure of the pricing problem.
This mission formalizes the formulation itself (§2 of the paper) and the two exact facts of its column generation (§3.1).
Let be an undirected graph on . Vertex is the depot; are the clients, client having a positive demand . Each edge has a length . There are vehicles of capacity , both positive integers.
A list of clients describes the closed walk . Its edge incidence is the number of times the walk traverses (a one-client walk traverses twice); its load is , with repetitions.
For , is the set of edges with one end in , , and . The paper's constraints on and on weights of the q-routes are
is ; is the set of satisfying (1) together with some satisfying (5), (6); the Explicit Master is the projection onto of the system (1)–(6) with one . The Dantzig–Wolfe Master (DWM) is the LP in alone obtained by substituting (5) into (1)–(4), giving the rows (8)–(11), with objective (7) . The bounds are .
For a loop-free graph with positive demands and capacity, and arbitrary lengths:
with (7) equal to . The bounds are stated in lower-bound form: every lower bound of over or is one over , and every lower bound over is at most the cost of every solution.
The formulation theorem is what makes the algorithm exact: integer points of are solutions, so branching on terminates at an optimum, and is a relaxation, so is a valid bound that dominates both classical bounds. The DWM description is what makes it computable: is optimized by column generation over q-routes, and milestones 8 and 10 show that any cut on can be added without changing the pricing problem, which remains a shortest q-route problem with edge costs .
The paper proves none of these claims formally; most are stated in a sentence, and milestone 9 is stated with "It can be shown" and no proof. To our knowledge none of them has a machine-checked proof. A formal development produces a library of walks, edge incidences, cut values and column families on a general graph that later missions on branch-cut-and-price (subset-row cuts, ng-routes, other routing variants) can import.
Most items are linear-algebra bookkeeping on finite sums, but they require a working theory of walks: edge incidences along a closed walk, the cut value of an incidence vector, and the fact that a walk from the depot crosses every client set an even number of times. The integrality statements (milestones 5 and 9 and goal part 1) are the hard part: an integer vector satisfying degree constraints need not come from routes through the depot, and the statements must exclude every other structure. For there are no capacity cuts at all, so the capacity of the routes must be recovered from the columns, and the paper states this case without proof. The obvious reduction "an integer point of is an integer combination of q-routes" fails: may be fractional even when is integral.
Vertices are Fin (n+1) with depot 0; edges are Sym2 (Fin (n+1)); the graph is an edge set E assumed loop-free where needed. Edge vectors are functions on all unordered pairs that vanish off E, which encodes . Demands , and are natural numbers; positive demands, and (the paper's standing assumptions, p. 1) are carried by the integrality statements and the goal, while is used by no statement and is omitted. Loads count repeated visits. The cut value , the demand and are the published definitions LysgaardCVRP.Shrink.cut, .demand and .roundedCapacityBound. The matrix is replaced by finitely supported weights on client lists ranging over all q-routes without 2-cycles. and OPT are never real infima, since is empty for infeasible instances.
Three trivializations are ruled out by construction: is defined from the Explicit Master display, not as ; a CVRP solution is defined by its routes, not as an integer point of a polytope; and the columns are not a fixed finite list, which would turn into a restricted master.
The strictness of "CVRP routes q-routes" (p. 2) depends on the instance and is not stated. Contributions of reusable lemmas on walks and cut values of incidence vectors are welcome, as are proofs of any milestone.
Sample covariance matrices are the basic object of multivariate statistics: principal component analysis, factor models and signal detection all start from the eigenvalues of built from observations of variables. When is comparable to , the largest eigenvalue of is no longer a consistent estimate of the largest population eigenvalue, and the question of when a "spike" in the population covariance is visible in becomes a question about the law of at large .
Timeline.
This mission formalizes the critical and subcritical side of that transition, Theorem 1.1(a) of the 2005 paper.
Let with independent real normal variables of mean and variance : a standard complex Gaussian. Let , , , be i.i.d. standard complex Gaussians. Fix an unitary matrix and positive reals , the population eigenvalues, and put . The samples are , mean-zero complex Gaussian vectors with covariance . The sample covariance matrix is and is its largest eigenvalue. Write .
The limit laws are built from the Airy function , integrated along a contour from to , and the Airy kernel
For , (with the pole above the contour) and . The Fredholm determinant of a kernel on is its Fredholm series
and
is the GUE Tracy–Widom distribution and .
Fix integers . Let with , and suppose , and stay in a compact subset of . Then for every real ,
The goal leaves arbitrary and allows to vary inside along the sequence. A companion item states Corollary 1.1(a): in probability.
Theorem 1.1(a) shows that is the exact threshold. Spikes strictly below it do not change the Tracy–Widom limit of . spikes exactly at it produce a new family of limit laws on the same scale. Together with part (b), where separates and fluctuates on the scale , it gives the first complete description of the transition. It is the reference point for spiked-model results on detection limits in PCA, for the real case (Bloemendal–Virág, Mo) and for finite-rank perturbations of Wigner matrices (Péché, Féral–Péché).
The paper's proof is complete and has been in the literature since 2005. No part of it is machine-checked. The mission produces:
The obvious approach is to compute the law of from the eigenvalue density, which is explicit (61). It fails because the density is an -fold integral whose integrand is a signed determinant, so no direct limit exists. The paper converts it into a Fredholm determinant of a double contour integral kernel. Two steps then carry the difficulty.
First, the steepest-descent analysis. With spikes at , the poles of the integrand sit exactly at the double critical point of the phase function. The contour cannot pass through the critical point and must enclose these poles, so it has to be routed at distance of order to the left of . All estimates must be uniform in and in the remaining spikes.
Second, the passage from kernel convergence to convergence of Fredholm determinants. It needs bounds strong enough to control every term of the Fredholm series, which is what the exponential tails in Proposition 3.1 provide. The functions grow polynomially, so even the finiteness of (Lemma 3.3) needs an argument.
Lean encoding:
Trivializing formalizations ruled out:
Infrastructure needed and reusable:
The Fredholm-determinant layer and the Airy function are reusable in any Tracy–Widom result. Andréief's identity and Hankel's formula are reusable well beyond random matrices.
Contributions welcome: proofs of any milestone, and lemmas that bound Fredholm series by Hadamard's inequality.
Potential games (Monderer and Shapley, 1996) are the finite games whose incentives are captured by a single function on strategy profiles: every unilateral change of strategy changes the deviator's payoff by exactly the change of a common potential. They have pure Nash equilibria, and natural learning dynamics such as better-reply and fictitious play converge in them. Most games are not potential games, however, and before Candogan, Menache, Ozdaglar and Parrilo there was no canonical way to say how far a given game is from one, or what the remainder looks like.
Their paper (arXiv:1005.2405; Math. Oper. Res. 36(3), 2011) answers this by viewing a game as a flow on a graph. The payoff differences between profiles that differ in one player's strategy form an edge flow on the game graph, and the classical Helmholtz (Hodge) decomposition of edge flows into gradient, harmonic and curl parts (Jiang, Lim, Yao, Ye, 2011) pulls back to a decomposition of the game itself. Every finite game becomes the sum of a potential game, a harmonic game and a component that carries no strategic information. The decomposition is the basis for the rest of the paper (equilibria of harmonic games, projections onto potential games, approximate equilibria) and for later work on dynamics in near-potential games.
Fix a finite set of players and, for each player , a finite nonempty strategy set with elements. A strategy profile is , and denotes the strategies of the players other than . A game is a family of utilities with , so the space of games is , where with .
Two profiles are -comparable if they are distinct and differ only in player 's strategy. The game graph has the profiles as nodes and an edge between comparable profiles. An edge flow is a function that is antisymmetric on edges and zero off edges; the space of edge flows carries . Triangular flows live on ordered 3-cliques.
The operators are: the gradient , with the edge indicator; the curl on 3-cliques; the per-player gradient , with the indicator of -comparability; and , , the flow of pairwise comparisons of . Adjoints are written and Moore–Penrose pseudoinverses . The space carries the unweighted inner product . Further, , , , and .
A game is normalized if for all and (Definition 4.1). The potential, harmonic and nonstrategic subspaces are (Definition 4.2)
and every game splits as with
where is a potential function of , i.e. .
Lemma 4.6 (the unique normalized game with the same pairwise comparisons is ) is included as a supporting theorem.
The decomposition turns questions about a game into questions about its three components. The potential component inherits the equilibrium and convergence theory of potential games. The harmonic component has a sharply different structure: harmonic games generically have no pure equilibrium, and in each of them the uniformly mixed profile is a mixed equilibrium. The nonstrategic component does not affect any equilibrium notion. The closed-form expressions also give the potential game closest to a given game, and with it bounds relating the approximate equilibria of the two games. The other missions of this series formalize those consequences; all of them rest on the operator layer and the subspaces defined here.
Theorem 4.1 is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces graph-flow infrastructure that Mathlib does not yet have: edge and triangular flows with their inner products, the combinatorial gradient and curl, the Helmholtz decomposition of a finite graph, and an operator Moore–Penrose pseudoinverse on finite-dimensional inner product spaces. The paper leaves Theorem 3.1 to the literature, so a full development needs a proof of it. The pseudoinverse identities of Lemma 4.4 also have a short appendix argument in the paper that a formal proof has to make complete.
The decomposition is not orthogonal decomposition along a single map. The subspaces and are defined through , which is assembled player by player from the , while the flow conditions involve and the combined operator . Connecting the two requires the player operators to have mutually orthogonal ranges ( for ) and the explicit form of as a scaled projection. Without these, (Lemma 4.4 (iv)) and (Lemma 4.4 (v)) are not available, and they are what make the formulas for and land in and . A direct attempt to apply the Helmholtz decomposition to produces a flow decomposition, not a game decomposition; the pullback through is not formal, because is neither injective nor surjective.
Players form a Fintype ι; strategy sets are E : ι → Type with Fintype, DecidableEq and Nonempty instances, and is Fintype.card (E m). Profiles are ∀ m, E m, and is Function.update p m q. The game graph is a Mathlib SimpleGraph; comparability requires , so the graph has no loops, as the Laplacian (15) requires. is EuclideanSpace ℝ on profiles. and are type synonyms of the subspaces of antisymmetric (resp. alternating) functions, with inner products built from (7), including the factor on . Lemma 4.4 (i) fails without it. The space of games is PiLp 2 of copies of , whose inner product is the unweighted sum used on p. 14, not the weighted inner product of the paper's Section 6. Adjoints are LinearMap.adjoint. The pseudoinverse is defined explicitly as the inverse of on composed with the orthogonal projection onto .
, and are defined by (28), not as the ranges of the component maps; the direct-sum part of the goal is stated independently of the formulas, so the goal cannot be satisfied by construction. Lemma 4.4 is split into five items, one per identity. "Orthogonal decomposition" in Theorem 3.1 is stated as pairwise orthogonality plus spanning. The paper's statements have no hypotheses beyond the setting, and none were added except nonemptiness of the strategy sets, which the paper assumes by writing .
Welcome contributions: a proof of the Helmholtz decomposition on a finite simple graph, general facts about the pseudoinverse (Penrose identities, is the projection onto , invariance under rescaling of inner products), and the explicit adjoint formulas (12) and (22).
A uniformly random simple graph with a prescribed degree sequence is a basic null model in network science, statistics and combinatorics: it is what a network "looks like" when nothing but its degrees is known. Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 2011) show that when the normalized degree sequences converge to a limiting profile , these random graphs converge almost surely to an explicit graph limit (their Theorem 1.1). That theorem has a hypothesis: must lie in the interior of the set of all possible limiting degree profiles. A hypothesis of that kind is only useful if it can be checked, and the paper's Proposition 1.2 supplies the check, in the form of a continuum version of the Erdős–Gallai criterion (Erdős and Gallai, Mat. Lapok 1960), the classical test for whether a list of integers is the degree sequence of a simple graph.
This mission formalizes Proposition 1.2 and the steps of its proof in §5 of the paper, together with the Erdős–Gallai criterion itself, which the paper cites and uses in both directions.
A degree sequence on vertices is a vector of nonnegative integers for which some simple graph (undirected, no loops, no multiple edges) on vertices has for every . Such sequences are written in nonincreasing order .
The space consists of the functions on that are nonincreasing and left continuous at every point of . It carries the modified norm
Suppose that for every a degree sequence on vertices is given. The sequence has scaling limit , a nonincreasing function on , if
The set consists of the that arise as scaling limits of degree sequences. Its interior is taken in with the topology of : is interior if every with lies in , for some .
For and the paper defines
At , approximates the slack in the -th Erdős–Gallai inequality.
In Lean these objects are IsGraphic, InDprime, norm1', Gf, HasScalingLimit, setF and InteriorF, in the namespace GivenDegreeSeq.Interior.
A function in belongs to the interior of if and only if
Proposition 1.2 turns the hypothesis of the paper's graph-limit theorem into two explicit conditions on . With it, for example, the constant profile with , the degree profile of the Erdős–Rényi graph , is seen to be interior (Remark 3, p. 6). The proposition also describes which limiting degree profiles are robust under small perturbations: away from the boundary given by the continuum Erdős–Gallai inequality and the trivial bounds and .
The Erdős–Gallai criterion is a standard tool for degree sequences, threshold graphs and network models. To the knowledge of this mission it is formalized neither in Mathlib nor on the platform, and a proof of it here is reusable well beyond this paper. The continuum objects , , scaling limits and are shared with the companion mission on the graph-limit theorem (mission 5 of this series). The proposition is proved in the paper; none of it has a machine-checked proof.
The obvious argument passes the Erdős–Gallai inequalities to the limit and back. Going to the limit is routine. Coming back is not, for two reasons. First, the discrete inequalities must hold for every , and near the normalized slack tends to , so positivity of alone gives nothing for . The bounds and of condition (i) are what control this range. Second, the approximating integer sequences must satisfy the parity condition and stay nonincreasing, while still converging in the sense of (2).
For openness, the interior must be taken under , and positivity of near has to be recovered for every nearby from condition (i), not from uniform convergence alone. In the converse direction, perturbations must stay inside , which constrains how may be modified near a zero of .
ℝ → ℝ. Only their values on enter , , , (2) and . Integrals are interval integrals. Every is monotone, hence bounded and integrable on .Fin n, so the paper's is d n ⟨i-1,_⟩ and the paper's is f ((i+1)/n). Degree sequences are vectors in Fin n → ℕ realized by a SimpleGraph (Fin n) and are nonincreasing.Infrastructure needed: the Erdős–Gallai theorem for finite sequences (both directions); Riemann-sum approximation of integrals of monotone functions; an integer-rounding construction with a parity fix. Proofs of the Erdős–Gallai criterion, and of the analytic lemmas on , are welcome independently of the goal.
The -model is the simplest exponential random graph model in which every vertex has its own parameter. It was studied by Holland and Leinhardt (1981) in the directed case and by Park and Newman (2004) and Blitzstein and Diaconis (2011) in the undirected case, and it is a close relative of the Bradley–Terry model for paired comparisons. Its sufficient statistic is the degree sequence of the observed graph, so fitting the model to data means solving a system of nonlinear equations in unknowns, one per vertex, where can be in the thousands.
Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 21 (2011)) give a simple iteration for this system and prove that it converges geometrically fast whenever a solution exists, at a rate that does not deteriorate with the number of vertices, and that it detects when no solution exists. The same estimate is then used in the paper's consistency theorem for the maximum likelihood estimator (Theorem 1.3) and in its graph-limit theorem (Theorem 1.1). This mission formalizes that algorithmic result, Theorem 1.5, together with the chain of numbered displays in Section 2 that proves it.
Let and label the vertices . For , the -model puts an edge between distinct vertices and independently with probability
Given an observed graph with degrees , the maximum likelihood estimate must satisfy the ML equations
The sup norm of is . For put , and define the map by
Starting from any , the fixed-point iteration is . The fixed points of are exactly the solutions of (3).
For an matrix , the operator norm is . For , the class consists of the matrices with , and for . For , is the matrix with entries .
There are functions and , continuous, independent of and , such that for every and every : if (3) has a solution , then , it is the unique solution of (3), and for all and
and if (3) has no solution, then every orbit is unbounded.
and . 6. (10), p. 13: a single , continuous in its arguments, with and .
The theorem turns an implicit statistical object, the MLE of an -parameter model, into the limit of an explicit iteration with three guarantees: a convergence rate that depends on the size of the parameters but not on ; an a posteriori error bound in terms of the computable step ; and a certificate of non-existence. The uniqueness of the MLE comes out of the same estimate. In the paper, the a priori bound is the device that proves consistency of the MLE (Theorem 1.3, applied with ), and the two-step contraction is reused in the proof of the graph-limit theorem.
The result is proved in the paper; no machine-checked proof of it is known. The work here is to formalize the known proof. The matrix inequality of Lemma 2.1 and the derivative bounds (6)–(7) are self-contained and can be attacked independently of the iteration.
The obvious approach is to show that is a contraction and apply Banach's fixed-point theorem. This fails: every row of the Jacobian of has absolute sum exactly , so is only non-expansive in the sup norm, never strictly contracting. Contraction appears only for the two-step map , through the sign pattern of the Jacobian (positive diagonal, uniformly negative off-diagonal), and only on bounded sets, with a factor that tends to as the norms grow. A second difficulty is uniformity: the factor must be bounded away from independently of , which needs , hence . For the converse, there is no fixed point to anchor the orbit, so boundedness of the orbit has to be converted into convergence before a fixed point exists.
Fin n ; vectors are Fin n → ℝ, whose Mathlib norm is the sup norm . Matrix norms are the explicit maximal absolute row sum.Needed infrastructure: calculus of (derivatives of of a sum of exponentials), the integral form of the mean value theorem for maps , and elementary matrix-norm estimates. The class and Lemma 2.1 are reusable for other diagonally dominant iterations. Proofs of any milestone are welcome, in any order.
Firms that buy from unreliable suppliers have two broad ways to protect themselves against supply disruptions: dual sourcing, which splits the order between two suppliers so that a shortfall at one is cushioned by the other, and process improvement, which invests in a supplier's operations so that it fails less often. Wang, Gilland and Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement? (M&SOM 12(3):489–510, 2010), compare the two in a single-period model in which the uncertainty is in the supplier's capacity, not in a proportional yield.
Real supply bases are rarely symmetric. Suppliers differ in cost, reliability and capacity because of their history or location, and the paper (p. 501) cites evidence that global sourcing has widened those differences. This mission formalizes the paper's analytical answer to one question this raises: as two otherwise identical suppliers drift apart in unit cost, which strategy gains? The paper's answer (Theorem 7, p. 502) is that the advantage of single sourcing with improvement over dual sourcing grows with the cost gap.
A firm sells one product over one season with unit revenue , salvage value and penalty per unit of unmet demand; demand has a known law with finite mean. Supplier has unit cost , committed-cost fraction and design capacity . Its realized capacity loss has a continuous distribution indexed by a reliability index ; a larger index means a stochastically smaller loss: implies for all . Losses are independent of each other and of demand.
An order delivers and costs . The realized profit is
the second-stage expected profit is , and .
In Lean these objects are MitigateSupplyRisk.Heterogeneity.Model (with Pi2, Pi2star, PiDS, Pi1single, PiSSI, Pi1) and SymData (with costModel Δ and etaModel Δ).
For suppliers identical except in unit cost,
The statement fixes no parameter values and no particular distribution; it asserts only the direction of the effect.
Theorem 7 turns a strategy comparison into a comparative-statics statement: once SSI is preferred at some cost gap, it stays preferred at every larger gap, so the preference switches at most once along a cost-heterogeneity path. Theorem 6 shows separately that both strategies benefit from heterogeneity, which is immediate for a single-sourcing strategy but not for dual sourcing, where one supplier improves and the other deteriorates. Lemma 5 is the structural fact the paper uses for the combined strategy: improvement efforts at the two suppliers are substitutes.
The results are proved in the paper's online appendix, which this formalization does not use. To our knowledge none of them has a machine-checked proof. A formal development would supply reusable pieces: an expected-profit model for random capacity with integrable profits, envelope and convexity arguments for suprema of affine families, and monotone comparative statics for single- and dual-supplier newsvendor problems.
and are both nondecreasing in (Theorem 6), so the goal compares the growth rates of two optimal values. Neither has a closed form. Both are suprema of families affine in , so they are convex but may have kinks, and an optimal improvement level need not exist when the index set is unbounded. The comparison concerns orders at different cost levels and under different strategies, so it needs a link between the dual-sourcing order from the cheaper supplier and the single-sourcing order and its response to improvement. Evaluating each side at a fixed optimizer does not give it, because the two optimizers move with . For Lemma 5, submodularity of in for each fixed does not pass to the supremum over by itself.
Fin 2. Each is the cdf of a measure ν i a on ℝ. Expectations are Bochner integrals against the product of the two loss laws and the demand law. The integrand is bounded by a constant times , so the integrals are genuine.Model.Standing and SymData.Standing):
MonotoneOn.Contributions are welcome at every level: integrability and boundedness lemmas for , convexity of the optimal values in , the symmetry argument behind Theorem 6(b), and monotone comparative statics of single-supplier orders in the reliability index.
Many data problems ask for a matrix of low rank from far fewer linear measurements than it has entries: matrix completion (recommender systems, where a few ratings of a large user–item table are observed), system identification, and quantum state tomography. Minimizing the rank under the measurement constraints is NP-hard in general. The standard convex surrogate replaces the rank by the nuclear norm, the sum of the singular values, and recovers the low-rank matrix exactly when the measurement map is well conditioned on low-rank matrices (Recht, Fazel, Parrilo 2010; Candès, Recht 2009).
Solving the nuclear norm problem at scale is itself a numerical challenge: interior point methods do not scale, and first-order methods such as singular value thresholding (Cai, Candès, Shen 2010) need many iterations. Fornasier, Rauhut and Ward proposed an alternative, iteratively reweighted least squares for matrices (IRLS-M), which replaces the nonsmooth problem by a sequence of weighted least squares problems whose weights are recomputed from the current iterate. It is the matrix analogue of the IRLS method for sparse vectors of Daubechies, DeVore, Fornasier, Güntürk 2010, and a closely related algorithm was studied at the same time by Mohan and Fazel (Allerton 2010; journal version JMLR 2012).
Timeline. 2008–2010: nuclear norm recovery under rank restricted isometry (Recht–Fazel–Parrilo) and the rank null space property (Recht–Xu–Hassibi). 2010: convergence of IRLS for under the vector null space property (Daubechies et al.). 2010–2011: IRLS-M and its convergence under the strong rank null space property (this paper, arXiv:1010.2471, SIAM J. Optim. 21(4), 2011).
Throughout, is a real matrix with , with singular values . The Frobenius norm is , the nuclear norm is , and . A linear measurement map is given by matrices through ; the data are .
The best -rank approximation error is . The map has the strong rank null space property (SRNSP) of order with constant if every nonzero and every split with admit another split with , , , and .
For the weight of is , where and . The IRLS-M algorithm with parameters and starts from , and repeats
with the weight of at level ; it stops when . Two functionals organize the analysis: , of which IRLS-M is an alternating minimization, and with for and otherwise.
For , any , a surjective and any run :
(ii) If , the iterates are relatively compact, their accumulation points minimize on the feasible set, and the sequence converges when that minimizer is unique; under the SRNSP with , every accumulation point satisfies, for every feasible and ,
(iii) Under the same SRNSP, if a feasible matrix of rank at most exists, then .
In attack order: the weighted least squares step (Lemma 5.1, the optimality condition (5.4)); the weight step (Lemma 5.2, Proposition 5.3); monotonicity of along the run (Proposition 6.1); singular value facts (Weyl's Theorem 7.1, attainment of at the spectral truncation, Lemma 6.10, Proposition 7.2); null space theory (Theorem 6.3, the inverse triangle inequality Lemma 6.6 with (6.5), Corollary 6.7); and the two steps of the proof of (ii), the optimality condition (6.10) for and the bound (6.11).
Theorem 6.11 is the convergence guarantee of IRLS-M. Combined with the fact that a small rank restricted isometry constant implies the SRNSP (Proposition 6.8, the companion mission), it yields Proposition 2.1 of the paper: under , IRLS-M recovers every rank- matrix exactly and approximately low-rank matrices stably. Part (iii) says that the algorithm detects exact low-rank data on its own: the smoothing parameter must vanish.
The result is proved on paper; no machine-checked proof exists. A complete formalization would give a machine-checked convergence proof of an IRLS-type method; none is on the platform, for vectors or matrices. It also produces reusable matrix analysis: Weyl's perturbation bound for singular values, the nuclear norm best rank- approximation (a Mirsky-type theorem), additivity of the nuclear norm under orthogonality, the null space characterization of nuclear norm recovery, and optimality conditions for spectral functions.
Two steps resist the obvious argument. First, the weight update is a constrained minimization over the positive definite cone; identifying its solution (Proposition 5.3) requires a duality or spectral argument rather than setting a gradient to zero, because the constraint is active on small singular values. Second, in case (ii) the limit functional is convex but not strictly convex, so accumulation points cannot be pinned down by uniqueness; the analysis must instead pass the optimality condition (5.4) of the iterates to the limit, using continuity of the weights in the iterate, and derive (6.10). The step relating to needs the differentiability of unitarily invariant spectral functions, which the paper imports from Lewis and Sendov. Weyl's inequality and the spectral truncation facts, routine on paper, are not yet in Mathlib for rectangular matrices.
All matrices are real (Matrix (Fin n) (Fin p) ℝ); the paper treats real and complex matrices alike. The paper's standing assumption is a hypothesis wherever objects (, , , ) occur. Nuclear norm, Frobenius norm, trace inner product and singular values come from the published definition HighDimStat_MatrixRank_Core; sv X i is , 0-based. The measurement map is given by measurement matrices (observationOp), which represents every linear map to . The weight is defined with Mathlib's continuous functional calculus, and is cfc Real.sqrt W. The algorithm is the relation IsRun: each is some minimizer of (2.9), is free, and after a stop. Accumulation points are MapClusterPt; uniqueness of a nuclear norm minimizer is a strict inequality against every other feasible matrix.
The goal cannot be satisfied vacuously: IsRun has a run for every surjective and every (Lemma 5.1 supplies the minimizers), it carries no positivity or uniqueness assumption a real run could violate, and the theorem keeps all three parts, including the unique-minimizer clause of (i) and the error bound of (ii) for every feasible and every admissible .
Two printed slips are corrected and disclosed: (5.5) omits the factor of (5.1), and (6.5) reverses the bracket of (6.4) at . Contributions welcome: Weyl's inequality and the Mirsky-type truncation theorem for rectangular matrices, the spectral calculus behind Propositions 5.3 and (6.10), and proofs of the null space results, which are independent of the algorithm.
A -join of a graph is a set of edges such that exactly the vertices of a prescribed even set have odd degree in . Minimum -joins are a classical object of combinatorial optimization: they contain shortest paths (), Chinese postman tours and perfect matchings as special cases, and their duality with -cuts connects them to integral multiflows. Whether the minimum size of a -join equals the maximum number of disjoint -cuts has been studied extensively; equality always holds in bipartite graphs (Seymour 1981).
Sebő and Tannier (Math. Oper. Res. 2004) study the number of connected components of a minimum -join, motivated by the observation that a minimum -join with few components yields a large integral packing of -cuts. Deciding whether some minimum -join has at most components is NP-complete in general (their Theorem 5). This mission formalizes the opposite end, : Theorem 6 characterizes exactly when a minimum -join can be chosen connected, in terms of the shortest-path metric of restricted to . The result first appeared in the authors' IPCO paper Connected joins in graphs (2001); the 2004 article derives it from its theory of isometric embeddings.
All graphs are finite, simple, undirected and connected. For vertices of , is the number of edges of a shortest – path. For , is the restriction of to pairs of vertices of .
For an edge set , is the number of edges of at ; is a -join if is odd exactly when . A minimum -join has the fewest edges among all -joins; a minimal one has no proper subset that is a -join. is the set of endpoints of edges of ; is connected (a tree) when the graph is connected (a tree), and is the distance in .
An isometry from to is a map with for all . A metric on a finite set is a tree metric if there is a tree (unit edge lengths) and an isometry from to ; the pair is a realization. A realization is inclusionwise minimal if no proper subtree of contains . A tree is an -join if its vertices of odd degree are exactly those of .
For connected and nonempty of even cardinality,
The conditions are required of every minimal realization; all of them are isomorphic.
Theorem 6 turns the existence of a connected minimum -join, a question about all -joins of , into conditions on the finite metric alone plus one isometric embedding of a tree into . Tree metrics can be recognized and their minimal realization constructed efficiently (Buneman 1974), and the embedding problem is the one solved in §2 of the paper, since contains all leaves of . The authors deduce that connected minimum -joins can be found in polynomial time, which contrasts with the NP-completeness of the same question for components. A consequence stated in the paper: if the minimal realization of is not a -join, then no minimum -join is connected.
The result is proved in the paper. No machine-checked version of Theorem 6, of Lemma 2, or of the uniqueness of minimal tree realizations is known to exist; Mathlib has graph distances, trees and walks, but neither -joins nor tree metrics. The mission produces these definitions and a formal proof of the characterization; the complexity consequence is out of scope.
The central difficulty is in the necessity direction. A connected minimum -join is itself a minimal realization of (Lemma 2), so satisfies the conditions; but the conditions concern the minimal realization, and transferring them from to an arbitrary minimal realization requires that minimal realizations are unique up to a label-preserving isomorphism. That uniqueness (milestone 3) is the step where the obvious approach stops: it is a statement about all trees realizing a metric, not about the graph .
SimpleGraph V with [Fintype V] [DecidableEq V]; G.Connected is a hypothesis of every statement about (SimpleGraph.dist is on unreachable pairs). Distances are natural numbers (SimpleGraph.dist).Finset (Sym2 V). Connectivity, the tree property and refer to the graph with edge set induced on , not on all of .Fin N together with a map Fin N; this avoids quantifying over a universe. A tree metric must satisfy .Reusable beyond this mission: the -join vocabulary, the path decomposition of minimal -joins, and tree metrics with the uniqueness of minimal realizations. Contributions to any milestone are welcome, as are alternative proofs of milestone 3.
Many objective functions in engineering and statistics are nonsmooth and nonconvex: the spectral abscissa of a parametrized matrix, the largest eigenvalue of a symmetric matrix function, the norm of a closed-loop system, or a maximum of finitely many smooth functions. Such functions are typically differentiable almost everywhere, yet their minimizers usually sit exactly where the gradient fails to exist. Gradient descent then zig-zags or stalls, and bundle methods, which are designed for convex functions, lose their guarantees.
Burke, Lewis and Overton (SIAM J. Optim. 15 (2005) 751–779) proposed the gradient sampling (GS) algorithm: at each iterate, sample gradients at random nearby points, take the element of least norm in their convex hull, and search along its negative. The method needs nothing beyond gradients at points of differentiability, and it has since become a standard tool for nonsmooth, nonconvex minimization (Burke, Curtis, Lewis, Overton, Simões, 2020). This mission formalizes the paper's convergence theory.
Timeline. Goldstein (1977) introduced the -subdifferential of a Lipschitz function and a conceptual descent method built on it. Clarke's generalized gradient (Clarke 1983) supplied the stationarity notion. Burke, Lewis and Overton (2005) made Goldstein's idea implementable by random sampling and proved almost-sure convergence to Clarke -stationary points for a fixed sampling radius. Kiwiel (2007) revisited the analysis and proved convergence for a modified version of the algorithm.
Let be locally Lipschitz, and let be an open dense set on which is continuously differentiable. Write for the closed Euclidean unit ball, and fix such that the level set is compact.
The Clarke subdifferential is the convex hull of all limits with and differentiable at each . For define
and the Clarke -subdifferential . A point is Clarke -stationary if , and Clarke stationary if .
The GS algorithm. Fix , , , , , and a sample size . At iteration :
With and the radius stays fixed, : this is fixed-radius mode.
In fixed-radius mode, with probability , either the algorithm stops at some iteration with , or it runs forever and there is a subsequence with
The theorem asserts nothing about along ; the authors list as an open question.
The milestones follow the paper's argument: the minimax characterization of the search direction (Lemma 2.1), the line-search descent estimate and the descent property of the iterates (§2), the almost-sure absence of a Step 1 stop, upper semicontinuity of and the uniform covering of Lemma 3.2(iv)–(v), Lebourg's mean value theorem (Theorem 3.3), the representation , the estimate of Lemma 3.1, the inclusion , and the closed graph of .
Well-posedness of the algorithm (every sample realization admits a run), Corollary 3.5(1) (the case: ), Corollary 3.6 (Clarke -stationary points with cluster at Clarke stationary points, and with a unique stationary point in the sets converge to it in the Hausdorff sense), Corollary 3.7 (with a unique stationary point in , small forces the run near it), and Theorem 3.8 (the variable-radius mode with ).
Theorem 3.4 is the first convergence guarantee for a practical method on general locally Lipschitz, nonconvex functions that uses only gradients at points of differentiability. It holds for a fixed sampling radius, the setting where most of the work is, and Corollaries 3.6–3.7 and Theorem 3.8 transfer it to radii decreasing to zero, which is how the method is used in practice. Later gradient sampling variants and their analyses start from these results.
The results are proved on paper; no machine-checked proof of them is known. A formalization would make the probabilistic structure precise, which the paper leaves informal (see Formalization scope), and would certify the hypotheses under which the theorem holds. Already the statements record two such corrections.
The natural argument, " decreases and is compact, so the steps tend to zero, hence ", fails: can go to zero while stays bounded away from zero. The difficulty is to show that, on the event , the random samples land infinitely often in a configuration whose sampled hull nearly realizes at a fixed nearby point, uniformly over a compact set of iterates, and that the failed trial step at such an iteration contradicts the Armijo rule. The iterates depend on all past samples, so independence across iterations cannot be used directly.
EuclideanSpace ℝ (Fin n), is Mathlib's gradient, the Clarke subdifferential is the published ClarkeGradients.Shared.generalizedGradient, and is Metric.infDist 0 C. Local Lipschitz continuity is Mathlib's LocallyLipschitz; continuous differentiability on is ContDiffOn ℝ 1 f D.IsGSRun on the iterates, radii, tolerances, step lengths, least-norm vectors, directions and a stopping index , imposing Steps 0–4 up to . "" is the least admissible , and the Armijo and (2) inequalities are strict.IsRandomGSRun) lives on a probability space with a filtration : the samples are uniform on , independent within an iteration, and independent of , while are -measurable. The Step 4 choice may use the past and extra randomness but never future samples. "With probability 1" is ∀ᵐ. The paper's event , the realizations that hit every positive-measure subset of infinitely often, is not used, because no sequence has that property.Multiplying matrices is a basic operation whose asymptotic cost is measured by the number of scalar arithmetic operations needed as the matrix dimensions increase. The familiar entry-by-entry algorithm has cubic cost. The question addressed here is how small an exponent can describe exact multiplication of square matrices when algorithms may use more elaborate finite computations. OpenAI's October 2, 2026 paper establishes the bound for matrices over the complex numbers. Its Theorem 1.1 concerns asymptotic arithmetic complexity, with arbitrarily small positive slack in the exponent.
An arithmetic program is a finite sequence of register computations. A step can load a field constant, read an input entry, or add, subtract, or multiply two values from preceding registers. Constant loads and input reads have zero cost. Each addition, subtraction, and multiplication has cost one. There is no division operation in this program model. Outputs are selected registers, and a program is correct only when these outputs equal the matrix product for every pair of input matrices.
For a field , a real number is an admissible exponent if, for every real , there exists a real constant such that every integer size admits a correct program with cost at most . The constant must work uniformly for all sizes and all input entries. The chosen program may depend on and . The definition does not charge for a separate procedure that constructs these programs. The arithmetic matrix multiplication exponent is the real infimum of the set of admissible exponents.
The goal is exactly the complex-field exponent conclusion of OpenAI's Theorem 1.1:
In the Lean source, the quantity on the left is OAI.MatrixMultiplication.Arithmetic.omega ℂ. The bound on the right is the exact real rational (9 : ℝ) / 4, equal to . The inequality is non-strict. The theorem does not assert a strict inequality below , and it is not quantified over arbitrary fields.
The paper also states the corresponding algorithmic conclusion with every positive exponent slack. The goal here retains the exact infimum formulation used by its released comparator challenge. In particular, the bound should not be read as asserting that one fixed family has cost without any slack, or that an algorithm is efficient at a specified finite matrix size.
The result places above the asymptotic arithmetic exponent in a model with explicitly defined programs, outputs, correctness, and operation counts. It gives a statement that other formal developments can use without leaving those conventions implicit. The dependence on the complex field is part of that statement, so results using another field or another computational model require their own justified connection.
This is a port and verification of an existing proof, not a claim that the source theorem remains unproved. The released Lean development contains the proof entry point. Keeping the original definitions and conclusion allows compatibility changes to be reviewed independently of the mathematical claim.
An asymptotic exponent bound requires one uniform cost constant for every positive matrix size, while correctness quantifies over all pairs of matrices at each size. A computation for selected dimensions or selected inputs cannot satisfy those requirements. Arguments about tensors must also support the stated arithmetic program cost, including the operations needed for the relevant linear combinations. The infimum formulation makes its defining set and the interpretation of its bounds part of the supporting mathematics, rather than assumptions to insert into the target theorem.
The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Matrices are functions on finite index sets. Program evaluation and output selection give exact field values. The main theorem fixes the field to , excludes size zero from admissibility, and uses real powers for its cost estimates. Constants may be arbitrary complex numbers; no bit-cost interpretation is asserted.
The definition item preserves the original source block, including its rectangular matrix multiplication definitions and complex dual exponent. Those additional definitions support the shared source development but are not additional mission goals. A complete proof must establish the displayed bound without an admitted lemma, a new axiom, or an assumption equivalent to that bound. Reusable components include the arithmetic program model, finite tensor constructions, asymptotic bounds, and the bridge from tensor rank to arithmetic operations.
A backward stochastic differential equation (BSDE) prescribes the terminal value of a process instead of its initial value. Pardoux and Peng (1990) proved that a BSDE with Lipschitz driver has a unique adapted solution. Coupled with a forward diffusion it gives a forward–backward SDE (FBSDE), which represents the solution of a semilinear parabolic PDE (nonlinear Feynman–Kac formula) and, in mathematical finance, the price and hedging strategy of a contingent claim, including path-dependent ones such as lookback and Asian options (El Karoui, Peng and Quenez, 1997). In high dimension or with path-dependent payoffs the PDE route is impractical, so one wants a time-discretization of the FBSDE itself, with a proven rate of convergence.
Zhang (2004) gave such a scheme for terminal values that are Lipschitz functionals of the whole path of the forward diffusion, and proved that it converges in mean square at rate , and at rate for -Lipschitz or Markovian terminal values. The key input is a new -regularity estimate for the martingale integrand . The same regularity estimate underlies the analysis of the Bouchard–Touzi scheme (2004) and of regression-based Monte Carlo methods (Gobet, Lemor and Warin, 2005).
Fix , a probability space carrying a one-dimensional standard Brownian motion , and its natural filtration augmented by the null sets. For the FBSDE is
where , , are deterministic functions and is a deterministic functional of the path .
Assumption 2.3 asks that be continuous, -Hölder in time and Lipschitz in the space variables, that be -Lipschitz,
for càdlàg paths , all with one constant , and that . is -Lipschitz if the supremum can be replaced by .
A partition is , with and ; it is -uniform if for all . The Euler scheme is , , and its step process is on . With the backward scheme is and, for ,
with . The numerical approximations are the step processes and on .
Assume Assumption 2.3 and that is càdlàg. If does not depend on , or is -uniform, then
for , and, if moreover is -Lipschitz or , the same left-hand side is at most (6.6). The constant depends only on , , and . The goal fixes the rates and leaves unspecified.
Theorem 6.1 gives an explicit, implementable scheme for FBSDEs with path-dependent terminal values and a mean-square rate that is sharp up to the logarithm: by Remark 4.3 the factor cannot be removed for -Lipschitz functionals, since it is already present in the uniform error of the Euler step process. Theorem 3.1 is reusable on its own: any time-discretization of a BSDE whose error is measured against needs it.
All results are proved in the paper. As far as is known, none has a machine-checked proof; the platform has no prior BSDE discretization result. The work is formalizing the known proofs, which needs the Itô integral, Itô's isometry and martingale representation, the standard a priori estimates for SDEs and BSDEs, and Doob's maximal inequality in continuous time.
The obvious argument compares the BSDE and the scheme step by step and closes with a discrete Gronwall inequality (Lemma 5.4). Its error terms include , and no pointwise estimate is available: is only square integrable in time, with no continuity modulus in general. The proof therefore needs the summed -regularity of Theorem 3.1, whose proof goes through smooth approximations of the coefficients and of , the representation of by the variational process , and the martingale inequality of Lemma 3.3. The rate comes from the maximum of Gaussian increments, which an estimate of cannot see.
Time is ℝ≥0; the state space is EuclideanSpace ℝ (Fin d); the Brownian motion is the coordinate of a Fin 1-indexed standard Brownian motion; is the augmented filtration. These, the Itô integral and the class are reused from the published modules Peng1990_SMP_Stochastic and ReflectedBSDE_Existence_Setting. Every expectation and time integral of a square is a lower Lebesgue integral in , so a non-integrable error cannot make a bound vacuous; this rules out the trivializing formalization in which a Bochner integral of a non-integrable error is .
The solutions and are quantified as solutions of their equations; the Euler scheme, , , , are constructed. Each constant is chosen before the probability space, the data, the solution and the partition. Disclosed readings: (i) the log-rate statements assume , the paper's " fine enough" (p. 478); (ii) " is càdlàg" includes ; (iii) the uniformity constant of Definition 5.2 is , not , and may depend on it; (iv) the Hölder constant in time is ; (v) , , ; (vi) Lemma 3.3 uses in place of , which strengthens it; (vii) Lemma 5.4 assumes . Completeness of the probability space is not used.
Not formalized here: Lemma 2.2 (smooth approximation of , cited from Ma–Zhang), the background Lemmas 2.4–2.7, and the representation (6.3)–(6.4) of the scheme by functions of the Euler grid values. Welcome contributions: the SDE and BSDE a priori estimates under Lipschitz coefficients, Itô's isometry and martingale representation for the reused Itô integral, and Doob's inequality in continuous time; all are reusable well beyond this mission.
In a linearly parameterized bandit, the expected rewards of many arms are driven by a small number of unknown parameters. Each arm is a vector , and its expected reward is the inner product with an unknown parameter vector . Problems of this kind arise in marketing and revenue management, where each product is described by features (price, popularity, …) and the expected revenues of thousands of products are, to a good approximation, linear in a few unknown feature weights. Pulling one arm then reveals information about all of them, and a good policy has to exploit this correlation.
Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, 2010) studied this model with unbounded, sub-Gaussian noise and a prior on . They proved an lower bound, a matching policy for smooth arm sets, and the Uncertainty Ellipsoid (UE) policy for arbitrary arm sets. This mission formalizes their Theorem 4.2: when the set of arms is finite, the regret of UE grows like , within a constant factor of the Lai–Robbins lower bound for the classical multi-armed bandit (Lai and Robbins, 1985).
Timeline.
Let and let be a finite, nonempty set of arms. Fix , the value of the unknown parameter. Playing arm in period yields the reward . The noise is drawn afresh in each period from a law that depends only on the arm played, independently of the past. A policy chooses the arm of period as a function of the history . The regret given is
and for a prior of the Bayes risk is . The gap of arm is , and is the number of periods among the first in which is played.
Assumption 1.
The UE policy first plays . It then forms the least squares estimate with , and plays an arm maximizing . The uncertainty radius is
with and . Ties are broken arbitrarily.
There are constants depending only on such that for all and ,
If moreover each has a point mass at and a density bounded by on , there are depending only on with
The constants are left unspecified, as in the paper. Their existence, uniformly in and in the arm set, is the content.
The result. For a fixed finite arm set, Theorem 4.2 shows that a single anytime policy, which does not know , has regret for every parameter and Bayes risk . It does this with unbounded noise and correlated arms. The dependence on the problem enters only through the gaps and the number of arms. The companion result for general compact arm sets (Theorem 4.1) gives only . The finite case shows that the same policy adapts to the easier problem.
Formalizing it. The theorem is proved on paper. As far as is known, it has no machine-checked proof. The platform's finite-armed bandit library (Lattimore–Szepesvári) has the regret decomposition and UCB pull-count bounds for independent arms, e.g. BanditAlgorithm.bandit_regret_decomposition. Those statements live in a different model and do not apply to correlated linear rewards with a least squares estimator. This mission adds:
The arms are chosen adaptively, so the design matrix is random and depends on the noise. Applied with the realized , the classical Chernoff bound for a fixed weighted sum of independent noises is not valid. The obvious union bound over arms does not apply either: the event concerns the random matrix , not one arm. In the pull-count bound, the radius of arm must be controlled through the number of times was played, although mixes all arms, and the Gram matrix of the other arms may be singular.
EuclideanSpace ℝ (Fin r), so is Euclidean. The source is arXiv:0812.3465v2; its printed page numbers equal the PDF's.Set, and is its ncard. Theorem B.2 and Lemma B.6, which the paper states for any compact arm set, are stated for compact nonempty arm sets, as printed.A reinforcement-learning agent that does not know its environment has to act and learn at once. Each step spent gathering information about unfamiliar states is a step not spent collecting reward, and an agent that only exploits what it already knows may never find better behaviour. Chapter 8 of Kakade's thesis (Kakade 2003) turns this trade-off into a counting question. Run an algorithm for an arbitrarily long time on one unbroken path of experience, with no resets. At how many timesteps does it fail to act optimally with respect to a fixed planning horizon ? Kakade calls this number the sample complexity of exploration.
The question builds on two algorithms. (Kearns and Singh 2002) gave the first polynomial-time guarantee for near-optimal behaviour in an unknown MDP. (Brafman and Tennenholtz 2002) replaced 's explicit explore-or-exploit switch by optimism: unknown states are treated as maximally rewarding. Kakade's chapter sharpens the analysis of . For deterministic MDPs it shows that the number of non-optimal steps is at most , which matches its own lower bound. The thesis notes that its deterministic results are similar to those of Koenig and Simmons (1993), with the dependence on , and made explicit (pp. 99, 104). The later PAC-MDP literature (for example Strehl, Li and Littman 2009) took this counting notion as its standard measure of exploration efficiency.
An MDP has a finite set of states, a finite nonempty set of actions, a transition model and a deterministic reward . A deterministic MDP has a next-state map , with exactly when .
Online model. An algorithm is a deterministic function that maps the path observed so far, , to the next action . Started at , it produces one path ; is the subpath up to . The -step end time of is the smallest multiple of larger than . The -step value of the algorithm on is the normalized reward it collects until ,
and is the supremum of this quantity over all algorithms continuing from .
-step policies. A -step policy is a sequence of deterministic decision rules . Its -value is , and is the supremum over -step policies. For a set of states , the induced MDP agrees with on and makes every state outside absorbing with reward . The escape probability is the probability that the path of in leaves . A transition model is an -approximation to if for every .
For every , and there is one algorithm such that, for every deterministic MDP with rewards in , every start state and every ,
The result. The bound does not depend on . However long the agent runs, only a fixed number of its steps fail to be -step optimal. The thesis's Theorem 8.3.6 shows that every algorithm has such steps on some deterministic MDP, so for deterministic MDPs the upper and lower bounds coincide. The induced-MDP lemmas carry over unchanged to stochastic MDPs. Together with Lemmas 8.5.4 and 8.5.5, they give the chapter's general bound (Theorem 8.3.1). They are the template for later optimism-based analyses, which compare an optimistic model with the true one and charge the difference to the probability of leaving the known region.
Formalizing it. The results are proved in the thesis; neither Mathlib nor the Prove2Me catalog contains a machine-checked version of any of them. A complete development would contain:
The proof of Lemma 8.5.5 in the thesis uses a Chernoff bound of the form . This form fails for the upper tail when , so the pinned statement needs a different argument.
The algorithm must be fixed before the MDP. It knows nothing about or beyond what its own path reveals, yet the count has to hold for every MDP, every start state and every run length at once. A direct approach could explore each state-action pair once and then plan. That does not bound the count. Exploration is interleaved with exploitation, the agent can only reach unknown pairs through known states, and every step on the way is judged against the full -step optimum of the current cycle. The work lies in charging each non-optimal step to a distinct newly tried state-action pair, with at most steps charged per pair, while the planning policy is recomputed every time the set of known states grows. In the stochastic lemmas, the main issue is that is a supremum over all -step policies, so the comparison has to go through for every competing policy, not only the planner's.
IsTransitionKernel functions .List (S × A × ℝ) → S → A. The run is defined by recursion and is infinite. is the realised normalized sum up to the end time, and is the backward recursion , which is the supremum over algorithms by the Markov property. The count runs over for every .Four formalizations would make the goal trivial or false, and each is excluded:
Reusable beyond this mission are the finite-horizon value layer, the induced-MDP and escape-probability lemmas, and the concentration bound. Contributions to any of these are useful independently of the goal.
Firms that buy from unreliable suppliers can protect themselves in two ways: they can spread orders across several suppliers, or they can invest in improving a supplier's reliability, for example through supplier-development programmes or joint process-improvement projects. Wang, Gilland and Tomlin (MSOM 12(3):489–510, 2010) compare the two strategies in a newsvendor model with random supplier capacity.
This mission formalizes one part of that comparison: single sourcing with improvement, in which improvement efforts may fail. The firm must then decide when to choose its supplier. Under early commitment it picks one supplier, invests in it, and buys from it whatever the outcome. Under late commitment it invests in both suppliers, observes which efforts succeeded, and only then buys from the better one. Empirical work on supplier development documents both practices and the reluctance of suppliers whose improvement efforts previously failed (Handfield et al. 2000, as cited by Wang et al. 2010, p. 496; Krause et al. 2007). The question is how much the option to postpone the choice is worth.
A firm sells a single product over one season. It earns a unit revenue , salvages leftovers at , and pays a penalty per unit of unmet demand, with . Demand is nonnegative with finite mean.
Supplier has design capacity , unit cost and committed-cost fraction . Its capacity loss has a continuous distribution that depends on a reliability index ; a higher index means a stochastically smaller loss. An order delivers . The firm pays , and the realized profit of single sourcing from is
The second-stage expected profit is , and is its optimal value.
Improvement. Supplier starts at index . Effort to reach index costs , where is convex and increasing with . The effort succeeds with probability ; on failure the index stays at .
and .
Let the suppliers be identical except for their unit costs, , with common , , and , and let be an optimal early-commitment index of supplier 2. Then
The results identify when the flexibility of postponing supplier selection has value. Late commitment never hurts. It has no value when one supplier dominates the other, even after the other's improvement. For suppliers that differ only in cost, Theorem 5 gives a checkable sufficient condition for strict value. The condition weighs the gain from switching in the outcome "the costlier supplier improves, the cheaper one does not", which has probability , against the cost of improving the costlier supplier. Together with Lemma 4 the results say that keeping the choice open lowers the reliability target but can raise expected profit. Corollary 3(a) says this value is easiest to obtain when costs are close.
The paper's proofs are in an online appendix that is not used here, and none of these statements has a machine-checked proof. The mission produces formal versions of the statements, with the hypotheses that the printed versions leave implicit made explicit (see Formalization scope), and invites proofs of them.
The late-commitment profit (9) is a probability-weighted sum of maxima of two optimal-value functions. It is "neither concave nor unimodal" (p. 498), so first-order conditions do not characterize its optimum, and optimizers need not be unique.
Everything is in the namespace MitigateSupplyRisk.LateCommit, with one definition module Model.
sSup over the feasible set. The sign conventions , make these sets bounded above, so no supremum is a junk value, and no optimum is assumed to be attained.Supplier record (committed cost, capacity, loss family) and the same Improvement record ().IsMaxOn), never as claims.Proofs of the milestones are welcome. A reusable lemma, that the supremum of expectations is monotone under first-order stochastic dominance of the loss, would serve the other missions of this series too.
Planning in a Markov decision process with a large or infinite state space cannot visit every state. The trajectory tree method of Kearns, Mansour and Ng (2000) finds a near-best policy in a class with a number of generative-model calls independent of the state space, but exponential in the horizon . Chapter 6 of S. M. Kakade's PhD thesis, On the Sample Complexity of Reinforcement Learning (University College London, 2003), trades that exponential factor for a weaker notion of optimality. The weaker notion is tied to a reset distribution that encodes prior knowledge of where good policies spend their time, such as a desired trajectory in robotic control or a known operating regime of a queueing network.
The resulting algorithm, μ-PolicySearch, chooses one decision rule per time step, backward in time, from a hypothesis class , optimizing each against states drawn from . The same idea was later published as Policy Search by Dynamic Programming (Bagnell, Kakade, Ng and Schneider, NeurIPS 2003). Conservative policy iteration (Kakade and Langford, ICML 2002) carries the same reset-distribution idea into the discounted setting.
Timeline:
A T-epoch MDP has a finite state set , a finite nonempty action set , a transition kernel , a deterministic reward and a horizon . Decision epochs are . A non-stationary policy gives a distribution over actions at each state and epoch. A decision rule is a map . A class of decision rules induces the class of deterministic policies that use a rule of at every epoch.
Values are normalized. The -value is times the expected reward collected from epoch to when starting in at epoch , so . The value is . The state-action value is , and the advantage is . The future state-time distribution of from is on .
A μ-reset distribution is a family of distributions on , one per epoch . Its joint law, uniform over epochs, is . For a decision rule the μ-advantage is
and is defined in the same way. The ℓ1 distance of two functions on is .
If a policy satisfies for all and , then for all and all start states ,
Theorem 6.3.1 states what μ-PolicySearch buys. The guarantee holds at every start state, whereas the trajectory tree guarantee holds only at the root it was built for. The policy is guaranteed to compete with each policy of whose future state-time distribution is close to . The penalty makes the role of the reset distribution precise: it is the price of the change from the "training" distribution to the "test" distribution . With Theorem 6.3.2 at , the exact algorithm attains the bound with no slack. The sample-based analysis (Theorem 6.3.3) reduces to controlling the condition.
The results are proved in the thesis, and no machine-checked version is known to exist. The mission produces a Lean development of the normalized T-epoch model (non-stationary policies, -values, advantages, future state-time distributions) together with the undiscounted performance difference lemma. These pieces are the common substrate of Chapters 4–6 of the thesis and of later finite-horizon policy-search analyses.
The performance difference lemma relates two objects defined in opposite directions of time: the state distribution of runs forward from , while the -values of are defined backward from the horizon. A formal statement must keep the epochs of the two aligned, including the boundary epochs and . The change of measure needs the bound , which holds only because values are normalized and rewards lie in . With unnormalized rewards the constant in front of the ℓ1 term is wrong.
A first idea is to read the hypothesis as "the advantages are small under ". That reading is not available. The hypothesis controls averages under only, and the gap between the two distributions is exactly the penalty term.
Fintype S), so expectations and the ℓ1 distance are finite sums. The thesis also allows infinite state spaces in this chapter, with integrals in place of sums.π t s a together with a validity predicate. Deterministic policies enter as indicator policies .The T-epoch layer (policies, state distributions, values, advantages, the future state-time distribution) is shared with the other missions of this series (namespaces SampleComplexityRL.PolicyGrad and SampleComplexityRL.Mismeasure); the μ-reset objects are defined in SampleComplexityRL.MuPolicySearch; IsTransitionKernel and IsPolicy are published definitions. Contributions of the performance difference lemma and of general facts about the T-epoch layer (values in , sums to one) are welcome.
Let be a connected graph and a set of vertices of even cardinality. A -join is a set of edges in which exactly the vertices of have odd degree. A -cut is a cut with odd. Write for the minimum size of a -join and for the maximum number of pairwise disjoint -cuts. Every -cut meets every -join, so . When equality holds is a central question of combinatorial optimization because of its links to integral multiflows. Seymour (1981) proved equality for all in bipartite graphs. Middendorf and Pfeiffer (1998) showed that deciding equality is NP-complete.
Korach and Penn (1992) proved that a minimum -join with connected components satisfies
So a minimum -join with few components certifies a large packing of -cuts, and a connected one certifies . Sebő and Tannier (Math. Oper. Res. 2004) therefore study the problem MTSC: given , and an integer , is there a minimum -join with at most connected components? They show it can be solved in polynomial time for and is NP-complete in general (their Theorem 5). The hardness proof reduces three-dimensional matching (3DM) to MTSC. This mission formalizes the correctness of that reduction.
Three-dimensional matching. An instance consists of three pairwise disjoint sets , , , each of cardinality , and a set of triples . A matching is a subset in which every element of occurs in exactly one triple.
The graph . Take a further set of points and put , so . The graph has as vertices the points of , the triples of , and one new vertex for every unordered pair of distinct points of . Its edges are:
There are no other edges. In Lean, is gadget q H and is gadgetT q H.
-joins and components. For and a vertex , is the number of edges of at . is a -join (IsTJoin) if is odd exactly for . It is a minimum -join (IsMinTJoin) if no -join of is smaller. The connected components of are those of the graph , where is the set of endpoints of edges of . Their number is numComponents F.
This statement is quantified over every and every , and it is the full mathematical content of the reduction.
The result. The Claim shows that minimizing the number of components of a minimum -join is NP-hard. A Korach–Penn certificate for a large packing of -cuts therefore cannot in general be found by optimizing the component count. This sets the case, which Sebő and Tannier solve in polynomial time through isometric embeddings of tree metrics, apart from the general case.
Formalizing it. The Claim is proved in the paper, in one paragraph. No machine-checked version is known, and the platform has no -join library. The mission produces a reusable vocabulary for -joins, minimum -joins and the components of an edge set, together with a checked proof that a concrete gadget is correct. One sentence of the published argument is false as written (see Difficulty); a formal proof settles the conclusion independently of it.
The direction from a matching to a -join is a direct verification. The converse has to control an arbitrary minimum -join: its size, the shape of each of its components, and how the components meet , and . A first reading of the printed proof suggests that every vertex outside that carries edges of is adjacent to at most one vertex of each of , , . This is false for the inner vertex of a path joining two vertices of the same class, and the construction joins every pair of points of , including pairs inside . Such components really occur in minimum -joins, so the count of components has to cover them as well. The stated conclusion (at least components, with equality only in the matching-like configuration) remains true.
On the Lean side, the components of an edge set are not the components of the graph with that edge set on all vertices: there every untouched vertex would be a component, and the Claim would become false.
Fin q), so their disjointness holds by construction. and are finite sets of triples in Fin q × Fin q × Fin q. IsMatching q M requires each element of each class to be the corresponding coordinate of exactly one triple of , and is a separate hypothesis. A covering-only or at-most-one version would be a different problem.Sym2) and is a Finset of edges of . Parity uses . Minimality is " for all -joins ", never an infimum on .Contributions welcome: proofs of the milestones, general lemmas on -joins (a -join in a graph where is independent has at least edges), and lemmas on the components of an edge set, which are reusable well beyond this mission.
UnrelatedSched.ThreeHalves.ThreeDimMatching (Lenstra–Shmoys–Tardos) encodes 3DM with an indexed family of triples and the covering form of a matching, a different encoding from the paper's set with "exactly one".The eigenvalues of a large non-Hermitian random matrix are hard to study directly. For Hermitian matrices, the empirical spectral distribution (ESD) is controlled by the resolvent and the Stieltjes transform, both stable under small perturbations. For non-Hermitian matrices no such tool exists: eigenvalues can move a long way under tiny perturbations, and the moment method fails because moments do not determine a measure on . The route that works, going back to Girko (1984) and used by Bai (1997), Götze–Tikhomirov (2007), Pan–Zhou (2007) and Tao–Vu (2008), passes through logarithmic determinants. The identity links the ESD to a scalar quantity. That scalar is computable from the singular values of , which are eigenvalues of a Hermitian matrix.
Tao and Vu, with an appendix by Krishnapur (Ann. Probab. 38 (2010) 2023–2065), turn this link into an exact criterion. Theorem 1.15 of that paper states that the ESD of a normalized i.i.d. random matrix converges to a measure if and only if the normalized log-determinants converge to the logarithmic potential of for almost every . The same holds for a regularized version built from the singular values. This mission formalizes Theorem 1.15 and the main steps of its proof (§8 and Appendix A of the published article).
Let be a complex random variable with and , and let be independent copies of on a probability space . For each , . Let be deterministic complex matrices with
and put .
For with eigenvalues , counted with algebraic multiplicity, the ESD is . Its singular values are . A sequence of random measures converges in probability to a deterministic if, for every continuous compactly supported , tends to in probability. It converges almost surely if, with probability one, for all such at once. The logarithmic potential of a measure is .
Hypothesis (1.4) states that, for almost every , the ESDs of the deterministic matrices converge to a limit.
In Lean everything lives in the namespace UnivESD.LogDet. The ESD is esd, the one-based singular value is sv, logPotential is the logarithmic potential, and ConvInProb/ConvAS/ESDConvInProb/ESDConvAS are the modes of convergence. IIDArray is the entry model, HSBound is (1.3), shiftA M xs z n ω is , and Cond14 is (1.4).
Let be a probability measure on with . The following are equivalent:
in probability.
Under (1.4) the same equivalence holds with almost sure convergence throughout.
Theorem 1.15 reduces convergence of a non-Hermitian ESD to a family of scalar limit statements. Each of these can be attacked through Hermitian tools, because the regularized log-determinant in (iii) is a smooth functional of the singular values. Corollary 1.16 of the paper derives from it a practical criterion: the ESD converges to once the singular value distributions of converge for a.e. to laws with . With the universality principle (Theorem 1.5, the companion mission) and Mehta's computation for complex Gaussian matrices, this yields the circular law for i.i.d. matrices with finite variance.
The theorem is proved in the source. To our knowledge neither it nor any of its milestones has a machine-checked proof. Mathlib has the ingredients for the objects (characteristic polynomials and their roots, LinearMap.singularValues, the strong law of large numbers) but not the results. A formal proof would give the platform its first verified bridge between eigenvalue and singular value asymptotics. Lemma A.3 alone, Weyl's multiplicative majorization, is a standard linear-algebra fact absent from Mathlib.
Two things make the obvious argument fail. First, is unbounded at . Vague convergence of controls only for continuous compactly supported , while has a singularity at and grows at infinity. Passing between (i) and (ii) therefore requires uniform control of the eigenvalues (and singular values) near after the shift: the contribution of the smallest ones must vanish. Second, eigenvalues are not stable under perturbation, so this control cannot be read off the eigenvalues. It has to come from the singular values, through a lower-tail bound on that is exponentially small in a power of , and through a deterministic inequality transferring bounds from singular values to eigenvalues. The smallest singular values ( below ) need a separate polynomial lower bound (the paper's Lemma 4.1, posed in the companion mission). The tail bound in its printed form is false at that end of the range.
Conventions committed to in Lean:
Integrable (‖w‖²) μ. The logarithmic potential is a Bochner integral, which is when not integrable; by (8.1) this happens only for a null set of , which "for a.e. " ignores.Real.log 0 = 0. In (ii), a singular matrix would contribute instead of ; for this model the determinant is almost surely nonzero eventually. Every milestone with or carries positivity of those quantities in its conclusion.sv A i is Mathlib's singularValues (i-1)). Eigenvalue enumerations are Fin n-indexed, and the paper's is index .Disclosed corrections to the printed text:
A trivializing formalization is ruled out by construction. The goal mentions only and . The proof's comparison ensemble is not a hypothesis. No statement takes a log-potential or a log-determinant as an input that could be fixed to make it hold.
The companion mission (Theorem 1.5, universality) poses Theorem 2.1 (the replacement principle), Lemma 1.7 (tightness) and Lemma 4.1 (least singular value), which the proof here also uses. They are not restated here. Once that mission is published they belong here as references. Contributions are welcome on the linear-algebra layer (Lemma A.3, multiplicative Weyl majorization), the Fubini argument of (8.1), and the singular-value tail bound (8.3). These are reusable well beyond this paper.
Supply disruptions — fires, quality failures, capacity shortfalls at a supplier — are a first-order risk in manufacturing supply chains. A buying firm has two broad responses. It can dual source, splitting orders between suppliers so that one supplier's shortfall is partly covered by the other, or it can invest in process improvement at a single supplier (kaizen events, supplier development programmes) to make that supplier more reliable. Wang, Gilland and Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement? (M&SOM 12(3):489–510, 2010), build a two-stage newsvendor model that captures both levers and compare them analytically.
This mission formalizes the paper's analysis of the improvement lever on its own: the firm commits early to one supplier, decides how much effort to spend improving it, and then orders. The paper's Theorem 3 shows that, without committed costs, this improvement problem is a concave program with an explicit first-order condition, and its Corollary 2 derives how the optimal effort responds to costs, revenue and the chance that improvement succeeds. These are the facts the paper's later comparisons between improvement and dual sourcing rest on.
A firm sells one product over one season at unit revenue , salvage value and unit penalty for unmet demand. Demand has distribution function and finite mean. The firm orders units from a supplier with design capacity , unit cost and committed cost : the firm pays when units are delivered.
The supplier suffers a random capacity loss and delivers . The law of has a continuous distribution function that depends on the supplier's reliability index ; a larger index means a stochastically smaller loss, for . Demand and losses are independent.
With and , the second-stage expected profit at index is
and is its optimal value.
In the first stage the firm may improve the supplier from its initial index . The paper reparametrizes effort by the target index: reaching index needs effort , where is convex and nondecreasing with . Effort costs per unit and succeeds with probability . The first-stage profit of early commitment is Eq. (7):
Assume and that is concave on for every (decreasing marginal reliability improvement). Then is concave on , and an optimal index , with an optimal order at , satisfies
Theorem 3 turns the firm's improvement decision into a one-dimensional concave program, so that the first-order condition (8) characterizes the optimum and comparative statics are available. Corollary 2 is the managerial content: cheaper or more reliable improvement, a cheaper supplier and a more valuable product all justify more improvement effort. The paper's later results — when late commitment beats early commitment (§4.2.2) and when single sourcing with improvement beats dual sourcing (§5) — compare the optimal values these results describe.
The results are proved in the paper's online appendix; none of them has a machine-checked proof. A complete development provides formal proofs of the layer-cake representation of the random-capacity newsvendor profit, of its critical-fractile solution, and of the concavity and envelope arguments on top of it.
is an optimal value, a supremum over order quantities, and suprema of concave functions are not concave in general. The obvious route — " is concave in for each , hence so is the supremum" — fails, because is not concave in for a fixed beyond the critical fractile. Any argument has to control how the optimal order moves with under random capacity, where the delivered quantity is a minimum of the order and a random effective capacity. The first-order condition then requires differentiating an expectation of a non-smooth function of in the parameter of 's law. Corollary 2 must be argued on the set of maximizers, since is concave but not strictly concave.
The Lean development lives in the namespace MitigateSupplyRisk.Improvement. Model bundles , a demand law and the family of loss laws; and are their cdf. Expectations are Bochner integrals over and over the product . Model.Assumptions collects the standing assumptions of §3: , , (implicit in the paper's division by ), a nonnegative integrable demand, nonnegative atomless losses, and the stochastic order in . Demand needs no density. Effort bundles with , and convex, nondecreasing on , ; taking as primitive assumes every index is reachable. is a real supremum and is built from it, never from the critical fractile. Every statement about carries or , which makes the supremum finite. "Optimal" always means a maximizer over the whole feasible set, and "increasing" is weak throughout, as on p. 492 of the paper.
The paper's proofs are in an online appendix that was not used here. Deviations from the page, each disclosed in the item's Formalization Note:
A trivializing formalization is ruled out: is built from the supremum (not from at a fixed order), the supremum is finite under the stated hypotheses, and every expectation is of an integrable function, so no statement holds through a junk value.
Reusable beyond this mission: the random-capacity newsvendor objects (delivered quantity, expected profit, layer-cake representation) and a Topkis-type monotone comparative statics lemma on a chain. Contributions of either, and proofs of the milestones in any order, are welcome.
The Lasso fits a linear model by least-norm regression with an penalty, and its most used property is that it returns sparse coefficient vectors: many features receive weight exactly zero. Most sparsity guarantees for the Lasso are statistical. They assume a generative model and an incoherence or irrepresentability condition on the design, and conclude that the support is recovered (Tropp 2006; Zhao and Yu 2006).
Xu, Caramanis and Mannor (arXiv:0811.1790v1, 2008; IEEE Trans. Inf. Theory 56(7), 2010) show that the Lasso's -regularized regression problem is exactly a robust regression problem in which each feature column is perturbed independently within a norm ball (their Theorem 1; mission 1 of this series). Section IV of the paper uses this robust view to give a sparsity criterion that needs no generative model: a feature gets zero weight if some allowable perturbation makes it irrelevant. This mission formalizes that criterion, Theorem 5, together with the more general Theorem 5′ it specializes, and the geometric consequence Theorem 6.
Fix integers . The data are the features , the columns of a matrix , and a response . For , . A disturbance perturbs column to .
Given radii , the feature-wise uncoupled uncertainty set is
For a set of disturbances, the robust objective is
and the robust regression problem is . It has a solution supported on if some minimizer has for all .
For a disturbance , agrees with on the features in and is zero elsewhere, and . Given numbers for , the enlarged set of Theorem 5′ is
In Lean these are uncertaintySet c, restrictedSet c I, enlargedSet c l I, robustObjective a b V x, IsRobustSolution and HasSolutionSupportedOn, all in the namespace RobustRegLasso.Sparsity.
If there is a disturbance that is zero on the features in and such that
has a solution supported on , then has a solution supported on .
Theorem 5 is Theorem 5′ applied to the perturbed matrix with radii off , and .
The result separates sparsity from statistics. Theorem 5 asks only that the features outside can be made irrelevant by a perturbation within the uncertainty budget; it involves no noise model and no probability. Theorem 6 turns this into an incoherence-type condition: features that lie within of being orthogonal to the response and to the relevant features receive zero weight. Because the robust problem over is the -regularized regression (Theorem 1), these are sparsity statements about that Lasso-type problem. The same argument gives the paper's further results on angular separation and nearly dependent features, which it defers to a companion report.
These results are proved in the paper; none of them has a machine-checked proof on Prove2Me or, to our knowledge, elsewhere. The mission formalizes the known proof. It also records a correction: Theorem 6 as printed claims that every optimal solution vanishes off , which is false (a two-dimensional counterexample is in the milestone's statement); the proof gives existence of one such solution, and that is what is posed.
The proof of Theorem 5′ is short, and the work is in the bookkeeping. The obvious attempt treats "max" as a real supremum and compares values directly; it has to know that each uncertainty set is nonempty and that the residual is bounded on it, and the enlarged set is nonempty only because . The two equalities of the first display require reassigning the columns outside of a disturbance (to zero, or to a feasible value) without changing the residual at , which works only because there. The specialization of Theorem 5′ to Theorem 5 changes the radius vector and the base matrix at the same time, and needs to coincide with the feature-wise set whose radii are on and off it. Theorem 6 additionally needs the equivalence of the robust problem with an -regularized problem, an orthogonal projection onto a span, and the existence of a minimizer of a coercive (or, for , least-squares) objective.
a : Fin m → EuclideanSpace ℝ (Fin n); a disturbance is δ : Fin m → EuclideanSpace ℝ (Fin n); is the family a + δ. Index sets are Finset (Fin m) (0-based). The loss is the norm, as stated in the paper (which remarks that any norm works).EReal (⨆ δ ∈ V). With nonnegative radii every set used is nonempty and bounded, so the value is a finite, attained real number; no junk value of a real sSup can make a statement vacuous. "Optimal solution" means a minimizer of this objective over all of ; existence of a minimizer is assumed where the paper assumes it (Theorem 5′) and concluded where the paper concludes it (Theorems 5, 6).