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.
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?
Integer programs are routinely solved by first solving their linear programming (LP) relaxation and then searching for an integer optimum near the fractional one. How near an integer optimum must be is the subject of proximity theorems. They bound the search region of branch-and-bound and of dynamic programming, and they turn a fractional optimum into a starting point for exact algorithms.
The classical bound is due to Cook, Gerards, Schrijver and Tardos (Math. Programming 34, 1986): for an integer program in inequality form that is feasible and bounded, every optimal LP solution has an optimal integer solution with , where is the largest absolute value of a subdeterminant of . For programs in standard form with rows this gives, via the Hadamard bound, , which grows with the number of variables .
Eisenbrand and Weismantel (ACM Trans. Algorithms 16(1), Article 5, 2019; conference version SODA 2018) removed the dependence on altogether, using the Steinitz lemma on rearranging vectors so that all partial sums stay short. Their bound depends only on and on the largest absolute value of an entry of , and it is the basis of their faster algorithms for integer programs with few constraints.
Fix natural numbers (rows) and (variables). The data are a matrix , a right-hand side , an objective and upper bounds . A natural number bounds the entries: for all . The integer program (10) is
and its LP relaxation is the same problem over . Its feasible region is a polytope, lpPolytope A b u. An optimal vertex solution is an optimal solution of the LP relaxation (IsLPOptimal) that is an extreme point of . An optimal integer solution is IsIPOptimal. Both are maxima.
Distances are measured in the -norm .
A vector is a cycle of (Eq. (14)) if and, for every , and : an integer kernel vector that is sign-compatible with and dominated by it (IsCycle).
The Steinitz lemma (Theorem 1.1) concerns vectors in an -dimensional normed space with and . It asserts a permutation with for all , and the paper uses Sevast'anov's constant .
If (10) has an integer feasible point and is an optimal vertex solution of its LP relaxation, then there is an optimal solution of (10) with
The constant is the paper's. The goal holds for all , , , and ; only and enter the bound.
The bound is independent of the number of variables. Combined with the paper's dynamic program, it gives the paper's running-time results for integer programs with upper bounds: an optimal LP vertex is computed, and the integer optimum is searched for within an -ball of radius around it. Eq. (21) bounds the absolute integrality gap by the same quantity, scaled by . The Steinitz lemma with constant is a general tool in discrepancy theory and in scheduling algorithms.
All of these results have published proofs. No machine-checked proof of Theorem 3.3 or of the Steinitz lemma is known to this mission, and Mathlib has no Steinitz lemma. The mission asks for complete Lean proofs of the milestones and of the goal. A proof of the Steinitz lemma with constant for arbitrary norms is reusable well beyond integer programming.
Lemmas 3.1 and 3.2 and the counting step are elementary. The substance lies in two places. The first is the Steinitz lemma with the linear constant for an arbitrary norm: the bound must hold uniformly in the number of vectors, and the constant must be exactly , because the goal's constant counts integer points of -norm at most . The second is the passage from a vertex to at most fractional coordinates. The paper argues this in one sentence (" has at most positive entries"), which is not literally true for (10) with upper bounds: coordinates at their upper bound are positive. The correct fact concerns coordinates strictly between and , and it has to be derived from the extreme-point property of .
IPProximity.Eisenbrand. The data are integral: A : Matrix (Fin m) (Fin n) ℤ, b : Fin m → ℤ, c : Fin n → ℤ, u : Fin n → ℕ (entries allowed), Δ : ℕ. They are cast to ℝ once, inside the LP definitions. and are allowed.Set.extremePoints ℝ (lpPolytope A b u). It is not defined through bases or by counting fractional coordinates.∑ i, |(z i : ℝ) - x i|. Mathlib's norm on Fin n → ℝ is the sup norm, and it is used only where the paper has (the of Eq. (21)).Contributions welcome: proofs of any milestone, in particular the Steinitz lemma, and a proof of the goal from the milestones.
The maximum flow problem asks how much of a commodity can be sent from a source to a sink through a network whose arcs have capacities. It underlies bipartite matching, transportation, scheduling and many reductions in combinatorial optimization. The classical method for it, the labeling method of Ford and Fulkerson (Flows in Networks, 1962), repeatedly finds an augmenting path and pushes flow along it. With integer capacities it terminates, but the number of augmentations can be as large as the maximum flow value itself, and Edmonds and Karp exhibit a four-node network on which this happens (p. 250). With irrational capacities the method need not terminate at all.
Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, J. ACM 19(2):248–264, 1972 (doi:10.1145/321694.321699), showed that two simple rules for choosing the augmenting path repair this. The first, augmenting along a path with fewest arcs, is the subject of mission 1 of this series. This mission covers the second (§1.3): augment along a path that gives the largest possible augmentation. For integer capacities the number of augmentations then grows only logarithmically in the maximum flow value.
A network has a finite set of nodes, a source and a sink , and a set of arcs, ordered pairs with , at most one from each node to another. One arc is the return arc ; the other arcs form the set , and each has a capacity . A flow is a nonnegative function on the arcs of with on and flow conservation at every node, and included. Its value is , the flow returned along the return arc; a maximum flow has the largest value among all flows, and denotes that value.
The residual network has an arc whenever and , or and . An augmenting path is a directed path of distinct nodes in . Each of its arcs has a residual amount , equal to , , or according to which of , lie in , and the path's augmentation is . Augmenting increases by and changes the flow on the arcs of the path accordingly, with the paper's own rule when both and are arcs. The labeling method produces flows by augmenting along a path relative to as long as one exists.
The rule studied here chooses, at every step, an augmenting path whose is at least that of every other augmenting path relative to the current flow. The bound involves an integer such that every partition of the nodes into and has at most arcs of with one end on each side.
For a network with integer capacities, as above, and a run of the labeling method with maximum augmentations started from an integer-valued flow,
and if no augmenting path relative to exists, then is a maximum flow.
The milestone list follows the paper's argument:
Theorem 2 was among the first bounds showing that a maximum flow algorithm can be made polynomial in the size of the numbers rather than in their values: since and is at most times the average capacity, the bound is in terms of the number of nodes and the average capacity (p. 254). The largest-augmentation rule, often called the fattest-path or maximum-capacity augmenting path rule, is a standard textbook variant, and its geometric-decrease argument is the model for later capacity-scaling methods, including the scaling algorithm for the Hitchcock problem in §2 of the same paper (mission 3 of this series).
The theorem has been proved since 1972 and appears in standard texts. As far as a platform search shows (2026-09-26), no machine-checked proof of it exists on Prove2Me. The platform does contain LinearOptimization.max_flow_min_cut and LinearOptimization.max_flow_ford_fulkerson_integer_termination, which state max-flow min-cut and termination of the generic method in a different network model (parallel arcs, extended nonnegative capacities, no return arc); they give no count of augmentations and are related work only. This mission would contribute a formal proof of the counting bound together with the general labeling-method facts (milestones 1–3), which mission 1 needs as well.
The obvious argument, that each augmentation raises the value by at least 1, gives only the bound , and on the four-node example of p. 250 that bound is attained by an arbitrary choice of paths. The logarithmic bound needs a lower bound on the size of the largest augmentation in terms of the remaining gap . The largest augmentation is defined by comparison with all augmenting paths relative to the current flow, while the gap is a global quantity of the network, and neither integrality nor the maximum-augmentation rule alone controls it. Milestone 2's converse, that a non-maximum flow always admits an augmenting path, is itself the max-flow min-cut theorem in this model, and the formal proof has to establish it for the paper's return-arc model rather than import it from a different one.
V with decidable equality. A : Finset (V × V) contains no loops and not . Capacities are real, c : V → V → ℝ, positive on A. Integrality is the hypothesis IntegralCaps N, and for the initial flow IsIntegralOn N (f 0) (integer values on the arcs of , the return arc included).V → V → ℝ constrained only on the arcs of . A maximum flow is the predicate IsMaxFlow, comparing with every flow, not a supremum. The goal takes a maximum flow g as a hypothesis and sets ; every network has one.IsMaxAugRun N K f P. Its initial flow is arbitrary except for integrality, and each later flow is the augmentation of the previous one along a path of maximum among all augmenting paths.CrossArcsBounded N M counts the arcs of , return arc included, with one end on each side of every – partition. This is the literal reading of p. 253.(K : ℝ) ≤ 1 + Real.logb ((M : ℝ) / ((M : ℝ) - 1)) (g N.t N.s) with a natural number. When , Real.logb gives and the bound reads . The contraction factor is 1 - (M : ℝ)⁻¹.Von Neumann's minimax theorem says that in a zero-sum game with real payoffs, Player I can guarantee an expected gain of at least the value and Player II can hold it to at most . In a long series of plays, the law of large numbers turns this into a statement about the average payoff: I can make it exceed , II can keep it below , with probability approaching one.
Blackwell's 1956 paper asks the same question when the payoff of each play is a vector in rather than a number. A single player then cannot optimize "the" payoff, and the natural question becomes geometric: can a player force the running average of the payoff vectors to converge to a prescribed set , whatever the opponent does? The resulting notion, approachability, became a basic tool in repeated games with incomplete information (Aumann–Maschler), in the theory of calibration and regret minimization (Foster–Vohra; Hart–Mas-Colell), and in online learning, where no-regret algorithms and Blackwell approachability are known to be equivalent (Abernethy–Bartlett–Hazan 2011).
Timeline.
Fix integers and , and a closed, bounded, convex set . The game is an matrix whose entries are probability distributions concentrated on . Write for the mean of , for the simplex of mixed actions of Player I, and for that of Player II.
A strategy of I is a sequence of measurable maps from the -tuples of past outcomes to ; is a point of . Strategies of II take values in . A play of is a sequence of random vectors such that, given , the players draw and independently from and , and is drawn from . The average payoff is , and is its distance from .
A set is approachable with if for every there is such that for every strategy of II,
It is excludable with if there is such that for every there is such that for every strategy of I,
is approachable (excludable) if some strategy approaches (excludes) it. Finally, for and ,
is the set of expected payoffs I can guarantee to stay in by playing , and the set II can confine them to by playing .
For a closed convex set ,
and if then is excludable with the stationary strategy . In particular every closed convex set is either approachable or excludable. Both sentences are part of the goal.
The result. THEOREM 3 is the vector analogue of the minimax theorem. For a closed convex target it reduces an infinite-horizon stochastic question, about every strategy of the opponent over all histories, to a finite family of one-shot conditions on the mean matrix , and it shows that the game is determined for convex targets: one of the two players always wins. Its sufficient condition, THEOREM 1, is the origin of the "Blackwell strategy", which steers the average toward the target by playing, at each step, a mixed action that pushes the expected next payoff across the supporting hyperplane. Regret-matching, calibration algorithms and the reductions between online linear optimization and approachability are instances of this construction.
Formalizing it. The result is proved in the paper; to the best of available knowledge no machine-checked proof of it exists. This mission produces one: the stochastic model of a repeated game with vector payoffs, the probabilistic estimates (THEOREM 2 and the LEMMA) with the uniform rate the paper claims, and the minimax reduction for convex sets. A related platform mission, Introduction to Online Convex Optimization XIII, states a deterministic, sufficiency-only textbook variant for bounded sets; the present mission covers the stochastic model, unbounded convex targets, and the excludability half.
The obvious argument shows that the expected squared distance decreases like . That is not approachability: the definition asks for the probability that the average is ever again -far after time , uniformly over the opponent's strategies. Controlling the whole tail of the path, with a threshold that does not depend on the opponent, is the step that fails for a naive expectation bound and is why the paper needs a maximal inequality for sums with negative conditional drift. On the geometric side, the "only if" direction is not automatic: it requires that approachability and excludability be incompatible, which in turn requires that a play of every pair of strategies exists.
Points live in EuclideanSpace ℝ (Fin N); pure actions are Fin r and Fin s; mixed actions are elements of stdSimplex. The game is a structure carrying (closed, bounded, convex) and the distributions (probability measures with ). A play is described by the conditional law of the next outcome given the past, and approachability and excludability quantify over every probability space in Type carrying such a play. Distances are extended (Metric.infEDist), equal to to the empty set.
Conventions and disclosed additions:
is not assumed bounded or nonempty. With the real-valued distance, the empty set would be approachable with every strategy and THEOREM 3 would be false; the extended distance rules this out. Stating only the sufficiency direction, fixing the approaching strategy in the hypotheses, or assuming a play exists would each trivialize the goal, and none is done.
A complete development needs: conditional laws of the next outcome from a strategy pair (Ionescu–Tulcea, Kernel.traj in Mathlib), a nonnegative-supermartingale maximal inequality, the metric projection onto closed convex sets, and the minimax theorem (Mathlib's Sion theorem). The maximal inequality of THEOREM 2 and the LEMMA are reusable beyond this mission. Contributions to any milestone, and to a construction of plays, are welcome.
The Steiner problem in graphs asks for the cheapest way to connect a prescribed set of nodes of a network, where intermediate nodes may be used freely. It is the network version of the classical Euclidean Steiner tree problem surveyed by Gilbert and Pollak (SIAM J. Appl. Math. 16, 1968), and it arises wherever a few sites must be joined through an existing network at minimum total cost: communication and pipeline layout, VLSI routing, and phylogenetics. With two terminals it is the shortest-path problem; with all nodes as terminals it is the minimum spanning tree problem; in between it is NP-hard.
Dreyfus and Wagner (Networks 1(3):195–207, 1971) gave the first exact algorithm whose running time is exponential only in the number of terminals and polynomial in the number of nodes. The paper states it, as Algorithm A, together with its proof of correctness and an exact count of its elementary operations.
Timeline. 1968: Gilbert and Pollak survey Steiner minimal trees. 1971: Dreyfus and Wagner, a dynamic program over subsets of terminals running in time proportional to . 1987: Erickson, Monma and Veinott give the same subset recursion for general network flow problems. 2007: Björklund, Husfeldt, Kaski and Koivisto (STOC 2007) improve the exponential dependence on for small integer weights. The Dreyfus–Wagner recursion remains the standard exact method and the basis of the fixed-parameter tractability of the problem in .
A graph has a finite set of nodes and a set of undirected arcs, each arc having a positive length ; is connected. For a set of arcs, . A set connects a node set if all members of are joined by paths composed only of arcs in .
Given , a Steiner path (or Steiner tree) connecting is a set that connects with minimum. Its length is the Steiner length . For nodes , is the length of a shortest path from to ; .
Algorithm A fixes a linear order of (so that each nonempty set has a first element ), picks , sets , and fills a table for nonempty and :
and returns
A minimum over an empty set is . In the Lean development these objects are steinerLength, pathDist, tableA and algorithmA in the namespace DreyfusWagner.Steiner.
For every finite connected graph with positive arc lengths, every linear order on its nodes, every with and every ,
This is the caption of Algorithm A ("Computes the length of the Steiner tree connecting ", p. 203). The statement is an equality, not a bound.
In the order the proof uses them:
Two companion items accompany the goal: the numerical illustration of §3 (seven nodes, , Algorithm A returns ), and the exact count of elementary statements of §5, .
The result turns the Steiner problem with few terminals into a polynomial computation in the size of the network: for fixed the running time is including all-pairs shortest paths. It is the reference exact algorithm against which heuristics and approximation algorithms for Steiner trees are evaluated, a standard example of dynamic programming over subsets, and the origin of the fixed-parameter tractability of the Steiner tree problem parameterized by the number of terminals. The subset recurrence reappears in group Steiner, prize-collecting and directed Steiner variants.
The paper's proof is complete and the result is classical; it has not, to our knowledge, been machine-checked. This mission produces a checked account of the exactness of the recursion: the structural facts about minimum connecting arc sets (acyclicity, optimality of branches, the three-way decomposition) and the passage from these to the algorithm's table. These facts about weighted graphs, minimum connecting arc sets and shortest paths are reusable well beyond this paper.
The upper bound is routine: each term of each minimum is the length of some connecting arc set, so no term can beat the optimum. The content is the reverse inequality, which needs the Optimal Decomposition Theorem: one must show that some optimal tree actually splits at a single node into a shortest path to and two optimal subtrees whose terminal sets partition into two nonempty parts. The naive choice fails when is a leaf, and the choice of the first branching node fails when the path from meets another terminal first; the paper handles these as separate cases. A second difficulty is the passage from arc sets to trees: minimum connecting sets are forests only because lengths are positive, and "the arcs of involved in connecting" a set of terminals must be identified with a subtree. Finally the table recursion must be matched with the recurrence, including the restriction that enumerates each splitting once.
Nodes are a finite type V with a LinearOrder (the paper's "(ordered) set"; the goal holds for every order). The graph is a SimpleGraph V with decidable adjacency, arcs are unordered pairs Sym2 V, and lengths are ℓ : Sym2 V → ℝ. Every theorem assumes the paper's standing hypotheses of p. 195: all arcs of have positive length (∀ e ∈ G.edgeSet, 0 < ℓ e) and is connected. The paper allows several arcs between the same two nodes; the simple-graph model keeps one, which does not change any Steiner length since an optimal set uses only the shortest of parallel arcs. Connecting means reachability in the graph formed by the arcs of . Steiner lengths, and all minima of the algorithm take values in WithTop ℝ, where ⊤ is , ⊤ + x = ⊤ and an empty minimum is ⊤; no real-valued infimum with a junk value is used. is a minimum over paths of .
The goal assumes , the paper's own hypothesis (Appendix A, p. 205). For Algorithm A as printed returns because line (18) admits no set ; the two-node case is covered by milestone 2. The algorithm is defined from , addition and minima only: a formalization in which tableA or algorithmA refers to Steiner lengths, or in which the goal only asserts , would be trivial and is ruled out. The loop order of lines (4)–(14) is replaced by recursion on , which the paper states is immaterial (p. 203).
Useful infrastructure: sums of lengths along walks and paths, reachability in edge-subgraphs, acyclicity of minimum connecting sets, and splitting a tree at a node. Contributions of these as reusable lemmas are welcome, as are proofs of individual milestones in any order. Tree reconstruction (§2, p. 200) and the empirical running times (p. 205) are out of scope.
Infinite-horizon sequential decision problems (deterministic optimal control, Markov decision processes, minimax control) share one computational question: does the dynamic programming (DP) algorithm, which starts from a terminal cost and repeatedly applies the Bellman operator, converge to the optimal cost? For discounted problems with bounded costs the answer is yes, by the contraction mapping theorem (Blackwell 1965; Denardo 1967). Without discounting and boundedness the answer depends on the sign structure of the problem. Strauch's negative programming model (Strauch 1966) and Blackwell's positive programming model behave differently, and in the former the DP algorithm can fail to converge to the optimal cost even for simple deterministic problems.
Bertsekas (1977) recast these models in one abstract framework: a monotone mapping that encodes the one-stage problem, with no probabilistic or additive structure assumed. Two sign conditions organise the theory: uniform increase (Assumption I, containing Strauch's model) and uniform decrease (Assumption D, containing the deterministic version of Blackwell's positive model, e.g. deterministic problems with nonpositive stage costs). This mission formalizes the uniform-decrease half of Section 5: under D, the finite-horizon problems are solved by the DP algorithm, is the limit of the finite-horizon values, Bellman's equation holds, and the DP algorithm converges to . The same framework became the basis of Bertsekas–Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978) and of Bertsekas's Abstract Dynamic Programming (2013, 3rd ed. 2022).
States, controls, policies. (nonempty) and are sets. Each has a nonempty constraint set . is the set of selectors with for all , and a policy is a sequence of selectors. The policy is stationary if for all .
Functions and the mapping . is the set of functions , ordered pointwise, and is the constant function . A mapping is given, and it is monotone: implies for every and . It defines
is the -fold composition, with the identity, and applies first.
Costs. A terminal function with is given. The cost of a policy, the optimal cost, the -stage optimal cost and the limit of the DP algorithm are
all pointwise. denotes the cost of the stationary policy .
Assumptions. D: for all , . Under D every sequence above is nonincreasing, so the limits exist in . D.1: for every sequence with , . D.2: there is such that for all and .
If D holds, and either D.1 holds or for every , then
The goal is the paper's answer, in the uniform-decrease case, to the question it poses in the introduction: when is ?
The result. Proposition 9 justifies value iteration from for every problem that fits Assumption D, including deterministic and stochastic control with nonpositive costs (reward maximization with nonnegative rewards) and minimax problems satisfying D.1. Propositions 6 and 8 characterise as the largest solution of Bellman's equation below and give a verification test for stationary policies. The hypotheses are sharp in the sense the paper documents: its Counterexamples 2 and 3 show when D.1 is dropped together with D.2 or with the finiteness condition . Under the mirror assumption I, can fail, so the asymmetry between the two sign conditions is part of the content.
Formalizing it. All results are proved in the 1977 paper and reappear in later monographs. No machine-checked version of this abstract framework is known. The platform's existing dynamic programming items are finite-state, real-valued and contraction-based, so this mission would add the first formal treatment of extended-real-valued, non-contractive dynamic programming, and a model definition that other results of the same theory can reuse.
The obvious argument for Proposition 9, " and ", hides two separate interchanges of limits and infima. Lemma 1 interchanges with , which works only because every sequence is monotone in the right direction under D. Proposition 3 is where the work is: the -stage infimum over policies must be matched by the iterated infimum , which requires building near-optimal selectors stage by stage and passing a limit through times, using D.1, or controlling accumulated errors through D.2. The latter breaks down when values reach , which is why that branch needs . All arithmetic is in , where expressions such as are not defined, and , , may equal even though does not.
The model is a Lean structure MonotoneDP.Decrease.Model S C with fields U, U_nonempty, H, mono, Jbar, Jbar_ne_bot and S_nonempty; is S → EReal. Policies are ℕ → Selector, where a selector is a function with values in the constraint sets. is an infimum over U x only, and , are infima over admissible policies. and are limUnder atTop; every theorem assumes D, under which both sequences are nonincreasing and converge, so these are the paper's limits. In D.1 both limits are limUnder. D.2 carries its scalar as a parameter, and "D.2 holds" is ∃ α, AssumptionD2 α. Only real scalars are ever subtracted from extended reals.
is defined for every , and Propositions 3 and 9 quantify over as the paper does. In Proposition 3 the condition belongs to the D.2 branch only. No hypothesis beyond the page is added. Nonempty constraint sets and are the paper's standing assumptions, stated in the model, not in the theorems. Without nonempty constraint sets there would be no policies, and would be , and several statements would hold trivially; the model rules this out.
Useful contributions: general lemmas about monotone sequences in EReal (interchanging ⨅ and limits), the monotonicity facts (25) and under D, and reusable constructions of near-optimal selectors. Corollary 6.1 (the finite-state D.2 variant) is not included.
Many problems in convex optimization, variational inequalities and signal processing reduce to finding a zero of a sum of three monotone operators, one of which is single-valued and smooth. Davis and Yin (Set-Valued Var. Anal. 25, 2017) introduced a splitting scheme that evaluates each of the three operators separately: the two set-valued ones through their resolvents, the single-valued one through a forward step. With a fixed stepsize, their Algorithm 1 converges weakly but can be slow: the paper's Section 3.4 constructs examples where the squared distance of the iterates to the solution decays no faster than for every .
When one of the operators is strongly monotone (for example the subdifferential of a strongly convex function), first-order splitting methods can be accelerated by letting the stepsize shrink like ; the paper relates its stepsizes to those of Chambolle and Pock's accelerated primal–dual method (J. Math. Imaging Vis. 40, 2011, Algorithm 2) and of Boţ, Csetnek, Heinrich and Hendrich (Math. Program. 150, 2015, Algorithm 5). Section 3.3 of Davis–Yin carries this device over to three-operator splitting and obtains an rate for the squared distance. This mission formalizes that result.
Let be a real Hilbert space. A set-valued operator is monotone if for all , , and maximal monotone if its graph is not properly contained in the graph of another monotone operator. It is -strongly monotone if for all such pairs. A single-valued is -cocoercive if , and -Lipschitz if .
The problem is to find , that is, , where , are maximal monotone and is monotone and single-valued. For the resolvent is the map with .
Algorithm 3 fixes stepsizes and an initial point , sets , , and iterates for
The stepsize changes in the middle of an iteration. Two stepsize rules are considered, each defined recursively from :
Let be -strongly monotone with .
The goal asserts the shape of the rate only; the constant is not fixed.
The theorem shows that strong monotonicity of or can be converted into a quadratically decaying distance bound without knowledge of the solution, with stepsizes that are computable from the strong monotonicity and cocoercivity (or Lipschitz) constants alone. Since the rate is established for , it applies directly to splitting schemes for strongly convex composite problems with smooth, where is the proximal point of .
The result is proved in the paper; no machine-checked version is known. The formalization adds a precise statement of the admissible parameter ranges, a check of the index conventions of a scheme whose stepsize changes mid-iteration, and a correction of the one-step inequalities at the first iteration (see Formalization scope). The stepsize limits are statements about explicit real recursions and are of independent use for other accelerated schemes.
The one-step inequalities (3.9) and (3.10) are long but elementary chains of inner-product identities and Young's inequality; the work lies in bookkeeping two stepsizes per iteration. The rate itself does not follow from the one-step inequality alone: telescoping gives a bound of the form , and one must then show decays exactly like . The rules (3.6) and (3.7) are nonlinear recursions without closed form, so their asymptotics require a Stolz–Cesàro type argument, which is not available in Mathlib under that name. Choosing a stepsize sequence of the form instead is a different algorithm and not covered by the theorem.
InnerProductSpace ℝ H, CompleteSpace H), not a Euclidean space.JA JB : ℝ → H → H required to satisfy the resolvent inclusion for every ; for maximal monotone operators such maps exist and are unique, so nothing is lost.Contributions are welcome at every level: proofs of the real-sequence milestones (a general Stolz–Cesàro lemma would be reusable well beyond this mission), of the two one-step inequalities, and of the telescoping argument that assembles the goal.
Conic quadratic problems (also called second-order cone programs) arise directly in applications such as contact problems with Coulomb friction, and a wide range of nonlinear convex problems can be rewritten in this form (Lobo, Vandenberghe, Boyd and Lebret 1998). Interior-point methods solve them in polynomial time, but around 2000 the available software for conic quadratic problems handled far fewer variables than linear programming software. Ben-Tal and Nemirovski (2001) therefore asked whether a conic quadratic problem can be replaced by a linear program of comparable size. Their construction replaces each second-order cone by a polyhedral cone that is exact up to a factor . The feasible set of the resulting linear program, projected back to the original variables, lies between the feasible set of the original problem and that of its -relaxation.
This sandwich is only useful if the relaxed problem is close to the original one, and in general it is not: the paper notes that (CQP) can be infeasible while every relaxation with is feasible. Proposition 4.1 of the paper, the target of this mission, gives a sufficient condition under which the two feasible sets are -close.
For let be the Euclidean norm. A conic quadratic problem in the variable is
where is a matrix and (the inequality is componentwise), and for each the matrix is , , and . For the -relaxation is
denotes the feasible set of a problem ; in Lean these are feas P and feasRelaxed P ε, subsets of Fin n → ℝ, for a problem datum P : CQP n k₀ m.
Two conditions on (CQP) are used.
IsStrictlyFeasible P x̄ r).IsSemibounded P R).Put .
If (CQP) has conic constraints and is strictly feasible and semibounded, then for every with ,
The left-hand side is the image of under , not a Minkowski sum.
The milestones follow the paper's proof in order.
The result. Proposition 4.1 turns the qualitative sandwich "exact ⊆ polyhedral ⊆ relaxed" into a quantitative statement. When a problem is strictly feasible with margin and its conic right-hand sides are bounded by on the feasible set, the relaxed feasible set, shrunk towards by , lies inside the exact one. The error of the relaxation is thus controlled by , which is linear in . Together with the paper's main theorem, that a polyhedral -approximation of the Lorentz cone with variables and inequalities exists, this measures how well a linear program of moderate size approximates the conic problem. The paper uses it this way for the examples in its introduction.
The formalization. The proposition is proved in the paper; no machine-checked version is known. This mission produces a Lean formalization of conic quadratic problems and their relaxations with the Euclidean norm, together with the strict feasibility and semiboundedness conditions and the proof. The Lorentz-cone approximation results of the same paper are the subject of the companion missions I and II of this series.
The right inclusion is immediate. The left inclusion does not follow from convexity alone. A relaxed-feasible point may violate every conic constraint of (CQP), and nothing about bounds how far it is from . The needed information comes from semiboundedness, which constrains only feasible points of (CQP). That hypothesis therefore cannot be applied to itself, and the shrink factor must be obtained without any bound on given in advance. The obvious attempt, bounding the violation at by , fails for exactly this reason.
Fin n → ℝ; the conic constraints are indexed by Fin m (0-based) with a dependent family of matrices (ℓ : Fin m) → Matrix (Fin (k ℓ)) (Fin n) ℝ, so the row sizes may differ. The norm is written out as eucNorm y = √(∑ i, y i ^ 2); Mathlib's norm on Fin k → ℝ is the sup norm and is not used.IsStrictlyFeasible states.eucNorm, or a transfer to EuclideanSpace ℝ (Fin k)) and linearity of Matrix.mulVec and dotProduct. A convexity lemma for feas P would be reusable beyond this mission, and contributions of it are welcome.A linear program is solved with known data, but in planning problems the data are often only known in distribution when the main decision is taken: demands, yields and requirements are revealed later, and a corrective action is taken after they are. E. M. L. Beale's 1955 paper On Minimizing a Convex Function Subject to Linear Inequalities formulates this situation in its §5, "Linear Programming with Random Coefficients", as what is now called a two-stage stochastic linear program with recourse. Beale's motivating example is the transportation problem of Hitchcock (1941) with random requirements at the destinations, where every unit of shortage or excess incurs a loss. The same model was put forward in the same year by Dantzig, Linear Programming under Uncertainty (Management Science, 1955), as the paper's note added in proof acknowledges.
Timeline:
Constants , and an matrix are given. The data , an matrix, and are random variables on a probability space : their distribution is known when the first-stage decision , , is chosen, and their values are known when the second-stage decision , , is chosen. The cost is
For a right-hand side the second-stage value is
and for fixed data the cost of a first-stage decision is . The expected cost is
The problem is to choose minimising . In Lean the value is secondStageValue D f b, the cost is cost c f D A β x, and the expected cost is expectedCost P c f D A β x, all in the namespace BealeConvexMin.RandomLP.
Assume that for every the second-stage minimum is attained for almost every outcome and that is integrable. Then
that is, is convex on the non-negative orthant. The statement fixes no distribution class: it is claimed for any known distribution of .
The result. Theorem 2 is the basic structural fact of two-stage stochastic linear programming: the first-stage problem is a convex program in , whatever the distribution of the data. It is what makes local optimality global for the first-stage problem, what justifies cutting-plane and decomposition methods that approximate from below by supporting hyperplanes, and what makes sample-average approximations convex programs. Theorem 3, joint convexity in the data, gives through Jensen's inequality the comparison between the stochastic problem and its mean-value problem that Beale draws on p. 182. The discrete reformulation (5.5)–(5.6) is the deterministic-equivalent linear program used for finitely many scenarios.
Formalizing it. The theorems are proved in the paper, and their content is classical. The mission produces machine-checked statements of the model with its implicit hypotheses made explicit (attainment of the second stage, integrability of the cost), and proofs of the three results in Lean. The platform already has related statements in other models (finite scenario sets with extended-real recourse, and a complete-recourse, finite-second-moment version); none has Beale's hypotheses, and none states convexity of for an arbitrary distribution.
The mathematics is short; the difficulty is in the encoding. The second-stage value is a minimum that may fail to exist: the second stage may be infeasible for some and some outcomes, or unbounded below. A real-valued infimum then takes an arbitrary default value, and convexity would become a statement about that default. Similarly, the mean value only exists when the cost is integrable. A faithful statement has to carry attainment and integrability exactly where the paper tacitly assumes them, on the domain the paper uses, and no stronger condition (such as complete recourse or moment bounds) that the paper does not make. In the discrete reformulation, the minimum over the whole family has to be matched with the probability-weighted sum of per-scenario minima.
Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, inner products dotProduct, and is the componentwise order. The random data are functions A : Ω → Matrix (Fin m) (Fin n) ℝ and β : Ω → Fin m → ℝ on a measurable space with a probability measure P; no measurability of the data is assumed beyond integrability of the cost.Many computations in scientific computing, statistics and machine learning need the trace of a matrix that is never formed explicitly: may be for a large sparse , an inverse , or a product of operators, and the only access to it is the ability to compute products for chosen vectors . Examples are log-determinant estimation in Gaussian process regression, counting triangles in graphs through , computing charge densities in electronic structure calculations, and generalized cross-validation in regularized regression. For such matrices the diagonal entries are not available, and computing them one at a time costs matrix–vector products.
Randomized trace estimators replace this by a small number of products: draw random vectors from a fixed distribution with and average the quadratic forms. Hutchinson (1989) introduced the estimator with Rademacher vectors and computed its variance; Silver and Röder (1997) used Gaussian vectors. Before Avron and Toledo (2011), the analyses of these estimators were variance computations, which do not say how many samples guarantee a given relative accuracy with a given probability. Avron and Toledo gave the first such sample bounds for several estimators, stated in terms of an guarantee; this mission formalizes their bound for the Gaussian estimator. Later work (Roosta-Khorasani and Ascher 2015; Cortinovis and Kressner 2022) sharpened these bounds and extended them to indefinite matrices.
Let be symmetric positive semi-definite, and write . Fix a number of samples . Let be random vectors whose entries are independent standard normal random variables. The Gaussian trace estimator (Definition 3.1) is
Each term has expectation , so is unbiased. A randomized trace estimator is an -approximator of (Definition 4.1) if
that is, if its relative error is at most except on an event of probability at most .
The analysis uses the eigenvalues of , listed with multiplicity, and the polynomial , where ranges over subsets of ; it satisfies .
For every symmetric positive semi-definite , every , every and every natural number with
the estimator is an -approximator of . The sample count depends on neither nor .
The theorem gives a number of matrix–vector products, , that suffices for a relative-error guarantee on the trace of any positive semi-definite matrix, independent of its dimension and spectrum. It is the reference row of the paper's Table I, against which the Hutchinson, normalized Rayleigh-quotient and unit-vector estimators are compared, and it is the form in which trace estimation enters the analysis of randomized algorithms for log-determinants, spectral densities and matrix functions.
The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The mission produces a machine-checked version with the constant and the range of made explicit, and with the misprints of the printed argument resolved (see Formalization scope). It also produces reusable pieces: the moment generating function of a Gaussian quadratic form, and the bound on elementary symmetric sums by powers of the power sum. Sharper constants, the removal of the restriction , or a direct formalization of the lower tail through a tail bound are welcome as further theorems.
Unbiasedness and the variance formula do not give the result: Chebyshev's inequality with yields , with a polynomial rather than logarithmic dependence on . A logarithmic bound needs exponential moments of , and the exponential moment of is finite only for below ; the argument has to choose inside that range uniformly in the spectrum, using only . The second obstacle is distributional: is not a sum of independent terms in the coordinates of , and reducing it to a weighted sum of independent variables requires the rotation invariance of the standard Gaussian vector. The paper proves only the upper tail with an explicit constant and states that the lower tail follows "using the same technique"; that step has to be supplied.
Matrices are Matrix (Fin n) (Fin n) ℝ; "symmetric positive semi-definite" is A.PosSemidef, "symmetric" is A.IsHermitian, and eigenvalues are Matrix.IsHermitian.eigenvalues. The sample space is Fin M → Fin n → ℝ with the product measure of copies of gaussianReal 0 1, so the law of the samples is constructed, not assumed; . Probabilities are Measure.real; the moment generating function is Mathlib's mgf; the variance is Mathlib's variance, and Lemma 5.1 asserts square integrability so that neither the integral nor the variance takes its default value. The sample count is a natural number ; and are real.
Corrections of the printed text, each recorded in the item's Formalization Note:
A formalization that makes the goal trivial is ruled out: the estimator's law is the explicit product Gaussian measure rather than a hypothesis, ranges over all natural numbers above the threshold, and the approximator predicate is evaluated on the genuine event .
A complete development needs rotation invariance of the standard Gaussian on (Mathlib's stdGaussian_map), the moment generating function of a squared standard normal, independence of products of Gaussian vectors, and a Chernoff bound from the moment generating function. The Gaussian quadratic-form results (milestones 1 and 2) are reusable for the other Gaussian estimators of the paper, such as the rank estimator of Lemma 5.3. Proofs of any milestone, alternative proofs of the lower tail, and helper lemmas on moment generating functions are welcome.
Retailers of fashion and seasonal goods sell at a premium price early in the season and mark down later. When customers anticipate the markdown, some of them wait, and the seller's pricing problem becomes a game between the seller and a population of forward-looking (strategic) customers. Aviv and Pazgal (MSOM 10(3), 2008) study this game in a model with limited inventory, stochastic arrivals and valuations that decline over the season, under two classes of seller policies: contingent pricing, where the discount depends on the inventory left, and announced fixed-discount pricing, where the seller commits to both prices upfront. Their numerical study (§7.3) compares the two classes and finds that precommitment can raise expected revenue by up to about 8%.
That comparison needs, for every announced price path, the customers' equilibrium response. Theorem 2 of the paper (p. 348) supplies it: a threshold purchasing policy, pinned down by a scalar fixed-point equation for the probability that a waiting customer is served. This mission formalizes Theorem 2. A companion mission of the same series formalizes Theorem 1, the contingent-pricing counterpart.
A seller has units to sell over a season , split at a fixed time with . Customers arrive by a Poisson process with rate . Customer has a base valuation drawn from a continuous distribution (tail ), and at time values the product at , where the decline factor is common to all customers.
Under an announced price path the seller commits to a premium price on and a discount price from on; does not depend on the remaining inventory. Customers know the initial inventory but not the current one.
A customer arriving at buys immediately if and only if (i) the current surplus is nonnegative and (ii) it is at least the expected surplus of waiting,
where is the probability that a unit will be allocated to the customer at time . Units left at are rationed at random among the customers who request one.
For a threshold function on the paper defines three segment rates: , the expected number of customers who buy at ; , those who could buy at but wait and want to buy at ; and , those whose valuation was below and who want to buy at . Each is times an integral over of at scaled prices (p. 345). With the Poisson probabilities, the allocation probability of units is
For let
and suppose solves
Then, when all other customers use (so that a waiting customer is served with the probability on the right of (8)), every customer arriving at buys immediately if and only if : the symmetric threshold profile is a Nash equilibrium.
Theorem 2 reduces the customers' equilibrium under an announced path to a single scalar . Everything downstream in §5 and §7 rests on it: the seller's expected revenue (p. 348) is written in terms of , the seller's optimal announced path maximizes it, and the comparison between announced and contingent pricing uses the resulting value . The theorem also explains the qualitative prediction of the model: the threshold exceeds exactly when the announced discount is deep relative to the decline of valuations, and it rises with the perceived availability .
The result is proved in the paper; to the best of our search it has no machine-checked proof. A formal development contributes the model objects (segment rates for threshold policies, the allocation probability for random rationing among Poisson requesters) in a form reusable by the rest of the series and by other strategic-customer pricing models, and a checked proof of the equilibrium property. The existence of a solution to (8) is not proved in the paper and is a natural further target.
The best-response part of the argument is elementary once the availability is known. The substance of the statement lies in the availability itself: the probability that a waiting customer is served is not a free parameter but the one generated, through (8), by the other customers' use of the same threshold. A formalization must connect the segment rates, the Poisson counts and random rationing into one expression and keep the fixed-point coupling between and intact; dropping it turns the theorem into a one-line inequality about an arbitrary . The division by also degenerates when and , and has to be excluded explicitly.
The Lean development lives in namespace SeasonalPricing.Announced. Conventions:
μ : Measure ℝ with IsProbabilityMeasure μ, = ProbabilityTheory.cdf μ, and continuity of (the paper's "continuous distribution") is a hypothesis of the goal. No support condition on is imposed; the statement quantifies over every real base valuation .tsum) as printed, not its closed form.availability is the right-hand side of (8), with built from by (7).Readings of the paper's informal words:
A formalization in which is an arbitrary number in , not tied to (8), is ruled out: it is the best-response lemma alone, not Theorem 2. Contributions welcome: proofs of the two milestones and the goal; lemmas such as and summability of its series; the closed form of printed on p. 346; and an existence result for (8).
In high-dimensional regression the number of candidate predictors can far exceed the number of observations . A regression function can then be estimated only if it is well approximated by a combination of a few elements of a large dictionary. The Lasso is the most widely used estimator in this regime. The question this mission formalizes is how well the Lasso predicts when the truth is not assumed to be sparse, or even to lie in the span of the dictionary.
A sparsity oracle inequality answers it. It bounds the prediction error of the estimator by the error of the best sparse approximation of the truth, which only an oracle knowing the truth could compute, plus a remainder proportional to the sparsity of that approximation times . Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 37(4), 2009) proved such an inequality for the Lasso under their restricted eigenvalue (RE) condition. Earlier oracle inequalities for Lasso-type estimators in fixed design (Bunea, Tsybakov and Wegkamp, 2006–2007) required the Gram matrix to be positive definite or to satisfy a mutual-coherence condition. The RE condition is weaker and allows , and it is now the standard hypothesis in this literature.
A dictionary is evaluated at fixed points . This gives the design matrix and, for an unknown regression function , the vector . The observations are
Nothing is assumed about . For the empirical norm is , and for we write . The column norms are assumed nonzero, with and . The support of is and its sparsity is .
The Lasso is any minimiser of
and .
Assumption RE holds with constant if, for every with and every with ,
The paper's is the largest such constant.
Fix , , , , and let RE hold with constant . With probability at least , every Lasso solution satisfies, simultaneously for all with ,
The theorem says that, up to the factor and a remainder of order , the Lasso predicts as well as the best -sparse linear combination of the dictionary. This is the case even when is not sparse and not in the span of the dictionary. The remainder is the parametric rate for parameters, inflated by and by the ill-posedness factor . Together with Theorem 5.1 of the same paper (mission II of this series), it shows that the Lasso and the Dantzig selector are within the same distance of the sparse oracle. The oracle inequality is used in aggregation, in model selection, and as a black box in later sparse-estimation papers.
The result is proved in the paper. It has not been formalized: at the time of writing, no Lasso oracle inequality and no probabilistic Lasso bound exist on Prove2Me or in Mathlib. What this mission contributes is a machine-checked proof of the paper's Theorem 6.1 with an explicit constant . The paper leaves unspecified, and its proof fixes the value used here. The mission also formalizes the Gaussian-tail step (B.4) and the deterministic basic inequality (B.1), both of which are shared with the paper's other Lasso results.
There is no sparse truth, so the usual argument does not apply. That argument places the error in the RE cone and reads off a rate. Here the competitor is arbitrary, and the approximation error can dominate the penalty terms, in which case the error is not in the cone. The RE assumption can be used only where the error does lie in a cone, and the cone constant available there depends on and on the column-norm ratio , because the penalty is weighted while RE is stated for unweighted vectors. What RE then yields is an inequality quadratic in with a cross term, not the form directly, and the constant is determined by how that cross term is absorbed. On the probabilistic side, the whole argument must run on one event of probability at least . That event may depend neither on nor on the choice of minimiser. The Lasso need not have a unique solution.
Matrix (Fin n) (Fin M) ℝ) and the target only through , which is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, independent random variables, each with law gaussianReal 0 σ², and .Classical non-cooperative game theory randomizes with objective, independent devices: each player spins a private wheel whose odds everyone agrees on. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) asks what changes when the randomizing events are ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. The paper introduced correlated equilibrium, and it also separates two effects that the classical model fuses: subjectivity (players disagree about probabilities) and correlation (players peg their choices on common or dependent events).
This mission formalizes the paper's result on subjectivity without correlation. Example 2.3 of the paper exhibits a three-person game in which strategies pegged on subjective but mutually secret events form an equilibrium that every player prefers to every classical mixed equilibrium. Proposition 5.1 shows that this cannot happen with two players.
A game has a finite set of players, a finite set of pure strategies for each player, a finite set of outcomes and an outcome function from onto . Player has a utility ; write for .
A randomizing structure consists of a set of states of the world with a -field of events, a sub--field for each player (the events is informed about), and a probability measure on for each player (the subjective probability of ). A strategy of is a map whose level sets lie in . For a profile of strategies the payoff of is
computed under player 's own beliefs. An equilibrium point is a profile with for every player and every strategy of .
An event is -secret if and every other player regards as independent of every event in the -field generated by the , : . A strategy is mixed if its level sets are -secret, and objective if each level set has the same probability under every . A measure is non-atomic on a -field if every event of of positive measure contains an event of of strictly smaller positive measure; a roulette is a sub--field of on which every is non-atomic. Throughout, Assumption II holds: every player has a -field of -secret events on which every is non-atomic.
For distributions on the classical payoff is , and is a Nash equilibrium point if no player gains by switching to another distribution.
Let and assume
Then for every equilibrium point in mixed strategies there is an equilibrium point in objective mixed strategies with
The game need not be zero-sum.
The result. Proposition 5.1 isolates correlation as the source of the new equilibrium payoffs of the subjective model in two-person games: disagreement about probabilities alone, with strategies pegged on secret events, reproduces only payoffs already achievable by classical mixed strategies (by Proposition 4.3, only Nash equilibrium payoffs). The paper uses it to explain Example 2.9, where two zero-sum players both expect more than the value, as an effect of subjectivity combined with correlation. Proposition 4.3 is the bridge that embeds classical Nash theory in the subjective model; with Nash's theorem it gives existence of equilibrium points in every game.
Formalizing it. The results are proved in the paper; to our knowledge none of them has been machine-checked. The mission produces a reusable measure-theoretic model of randomized strategies with private information and subjective beliefs (secret events, mixed and objective strategies, roulettes), a non-atomicity notion relative to a sub--field, and the Lyapunov-type construction of Lemma 7.1, none of which exists in Mathlib at the pinned revision.
The equilibrium conditions quantify over all strategies of the deviator, i.e. all -measurable maps, and the deviator may know events on which the opponent's mixed strategy is pegged. The obvious computation of as a sum of products of marginal probabilities is valid only because the opponent's strategy is pegged on secret events, which is the content of Lemma 7.3; for correlated strategies it fails, and Example 2.9 shows the proposition then fails. A second obstacle is that the replacement must reproduce player 2's beliefs about , while player 1's own equilibrium condition is stated under ; condition (5.2) is what transfers " is played with positive probability" from one player's beliefs to the other's. Constructing objective strategies with prescribed probabilities (Lemmas 7.1 and 4.1) needs the convexity of the range of a non-atomic vector measure (Lyapunov's theorem), which is not in Mathlib.
Players are a finite type (Fin 2 in the goal, players ); the and are finite types, and is surjective. The -field is an explicit parameter mΩ of the structure RandomizingStructure ι Ω mΩ, which carries the and the probability measures . Probabilities are -valued Mathlib measures. Utilities and are data (Assumption I is used only to compare lotteries by expected utility; the uniqueness of is not encoded). is a Bochner integral; for strategy profiles the integrand has finitely many values and is measurable, hence integrable. Non-atomicity on a sub--field is defined directly; Mathlib's NoAtoms (singletons are null) would trivialize Assumption II and is not used. "Mixed" means pegged on the family of all -secret events, not on the -field of Assumption II. Classical distributions, and Nash equilibrium points are AGT.IsLottery, AGT.expectedPayoff and AGT.IsMixedNash from the published definition agt_games.
A formalization that restricted deviations to mixed or objective strategies, or dropped "mixed" from the hypothesis on , would state a different theorem and is ruled out.
Useful contributions: Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures (or the special case needed for Lemma 7.1), the factorization of Lemma 7.3, and the payoff identities used in the proof of Proposition 4.3. The model definitions are shared in meaning with the companion mission on two-person zero-sum games.
In high-dimensional linear regression one observes with a design matrix whose number of columns may far exceed the sample size . The two standard estimators of a sparse , the Lasso (Tibshirani, 1996) and the Dantzig selector (Candès and Tao, 2007), both come with error bounds of order for an -sparse , but only under a condition on : since has a non-trivial kernel when , some form of restricted invertibility is unavoidable.
Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 2009) introduced the restricted eigenvalue (RE) condition, which asks for invertibility of only on a cone of approximately sparse vectors. It is weaker than the conditions used before it and has since become the default assumption in the sparse-estimation literature. Section 4 of the paper relates RE to the earlier conditions:
This mission formalizes those implications.
Fix integers and and a matrix with columns . The Gram matrix is . For and , is the vector equal to on and off ; , are the and Euclidean norms; is the number of non-zero coordinates of ; is the complement of .
The cone condition for and is
Assumption RE holds with constant if for every with and every satisfying (4.1). For , let be a set of indices outside carrying the largest , and ; Assumption RE replaces by .
The restricted eigenvalues are and , the minimum and maximum of over with . The restricted correlations are the maximum of over disjoint index sets with and non-zero . Two constants are attached to them:
is the orthogonal projector in onto the span of the columns , .
For integers , , and , if Assumption 2 holds, then , RE and RE hold with constant , and for every with and every satisfying (4.1)
Assumption 2 involves no correlations, only extreme eigenvalues of small principal submatrices of .
For and , Assumption 1 implies the same conclusions with and constant .
For and , each of
(Assumptions 3, 4, 5) implies RE, with the constants , and respectively.
The milestones are the steps of the proof in Appendix A — the projection inequality (A.1), the block bound (A.2), the shelling bound (A.3), the Candès–Tao correlation bound used for part (i) — followed by part (i) and the three coherence-type implications.
RE with and is the hypothesis of the paper's prediction and bounds for the Lasso and the Dantzig selector (Theorems 5.1, 6.1, 7.1, 7.2), and RE is the hypothesis of its bounds. Assumptions 1–5 are stated through quantities that are standard in compressed sensing and random matrix theory, so known bounds for , and of random designs transfer, through this mission's theorems, to every result stated under RE. Lemma 4.1 also shows that RE is weaker than the Candès–Tao condition used for the Dantzig selector.
The results are proved in the paper; parts of Lemma 4.1's proof (the correlation bound for part (i)) are cited from Candès and Tao without proof. None of these results is formalized: the platform has pairwise-incoherence and restricted-nullspace statements from Wainwright's textbook (a different conclusion and normalization) and restricted isometry definitions, but neither restricted eigenvalues , restricted correlations , nor the RE condition in this form.
The naive attempt to bound from below splits and applies an eigenvalue bound to each part. This fails: can have up to non-zero coordinates, and no condition on - or -sparse submatrices controls directly. The cone condition bounds only the norm of , while eigenvalue conditions speak about norms of sparse vectors; bridging the two with the right constant , and keeping track of how the leading block interacts with the rest through the projector , is where the work lies. For part (i), the interaction between disjoint sparse blocks has to be controlled by rather than by .
Matrix (Fin n) (Fin M) ℝ; vectors are Fin M → ℝ and Fin n → ℝ; . The projector is Mathlib's orthogonal projection on EuclideanSpace ℝ (Fin n) onto the span of the columns indexed by .RE X s c0 κ asserts the RE inequality with constant for all admissible and . The paper's is the largest such (the minimum is attained), so "RE holds with " is exactly " is a witness". This avoids a real infimum over an empty set when .sInf/sSup over nonempty bounded sets (a basis vector for ; two disjoint singletons for , since ), so they equal the paper's attained min/max. , , are natural numbers; is written .Generalized pattern search (GPS) is a class of derivative-free methods for minimizing a function that can only be evaluated, not differentiated. Such objectives arise in engineering design, where one evaluation is an expensive simulation that may fail and return no value at all. The helicopter rotor design problem of Booker et al. is one example: no value was returned for roughly 66% of the trial points (Booker et al., 1999). A method for such problems has to tolerate objectives that are discontinuous or take the value .
Earlier convergence theory for GPS assumed continuous differentiability of the objective on a neighbourhood of the level set. Torczon established it for unconstrained problems (SIAM J. Optim. 7, 1997), and Lewis and Torczon extended it to bound constraints (1999) and to finitely many linear constraints (SIAM J. Optim. 10, 2000). Audet and Dennis (SIAM J. Optim. 13, 2003) replaced these analyses with a single argument. Its conclusions are local and are graded by the smoothness of the objective at the limit point only, through Clarke's generalized directional derivative. That paper is the source of this mission. Its analysis is the basis of the later mesh adaptive direct search (MADS) theory (Audet, Dennis, SIAM J. Optim. 17, 2006).
The problem is
with and in . The algorithm works with the barrier function , equal to on and to elsewhere.
The algorithm uses a finite set of directions , the columns of the product of a nonsingular and an integer matrix . The directions form a positive spanning set: their nonnegative combinations give all of . At iteration , with iterate and mesh size parameter , the mesh is . A poll set is drawn from a positive spanning subset . Each iteration ends in one of two ways:
Here is rational and are integers. The assumptions are A1 , A2 is rational, and A3 all iterates lie in a compact set. A refining subsequence is an infinite set of mesh local optimizers along which (Definition 3.5). For Lipschitz near , Clarke's derivative is
Assume A1–A3. Let be the limit of a refining subsequence, and let be a direction polled at a feasible point for infinitely many in the subsequence. If is Lipschitz near , then
Theorem 3.7 gives a first-order conclusion at a limit point from a local hypothesis at that point alone. It does not require smoothness elsewhere, finiteness of elsewhere, or continuity. It turns the heuristic "the method stopped improving on ever finer meshes" into a statement about generalized derivatives. The unconstrained stationarity result (Theorem 3.9) and the linearly constrained KKT result (Theorem 3.14) follow from it, and they recover the Torczon and Lewis–Torczon theorems under weaker smoothness assumptions. The chain Lemma 3.2 → Lemma 3.3 → Proposition 3.4 → Theorem 3.6 shows that the goal's hypothesis is always met. Every run satisfying A1 and A3 has a refining subsequence, which rests on the rationality of and on the integer structure of .
All results in this mission are proved in the source paper. None of them has, to the best of our knowledge, a machine-checked proof. The mission contributes a formal model of the GPS algorithm class as a class of runs, a formal Clarke directional derivative, and checked proofs of the mesh-refinement chain and the main theorem.
Given a refining subsequence, the goal is a comparison of limsups: the poll inequalities give nonnegative difference quotients at the points , which converge to . The difficulty lies in two places. First, the objective is extended-valued, and the barrier hides at infeasible poll points, where the poll inequality says nothing. The hypothesis on has to supply feasibility, and the Lipschitz hypothesis has to supply finiteness near . Second, the existence of refining subsequences is not a compactness argument alone. Coarsening is allowed, so need not decrease, and with an irrational or a direction set that is not an integer lattice image (for instance in ) the meshes can be dense and can be positive. The lattice argument behind Proposition 3.4 is where the integrality hypotheses are used.
Points of are Fin n → ℝ, takes values in WithTop ℝ, and the bounds are EReal-valued, so gives . The barrier is defined by cases, never by extended addition. Directions are the columns of G * Zbar indexed by Fin p, and is a Finset (Fin p). A GPS run is a structure of sequences and a per-iteration predicate "mesh local optimizer", subject to exactly the two update rules above, , rational and the exponent bounds. The SEARCH step, the choice of and the exponents are left free, since the paper allows any strategy. A subsequence is a strictly increasing map . The Clarke derivative of a real function is an EReal-valued limit superior along , . " Lipschitz near " means that agrees near with a real function Lipschitz there, and the conclusions are stated for every such function. Strict differentiability is the directional notion of Section 3.4 of the paper.
The goal is not trivialized by an empty run class: Theorem 3.6, on the same class, asserts that refining subsequences exist. The mesh-local-optimizer branch requires the complete poll inequality over . The Clarke limit superior cannot take a default value. The direction must be polled at feasible points infinitely often, which is the paper's " was evaluated".
Contributions welcome: proofs of any milestone, and reusable lemmas on positive spanning sets, lattice points in compact sets, and the Clarke derivative (for instance, that it equals under strict differentiability).
Maximizing a submodular set function without constraints contains Max Cut, Max Directed Cut, maximum facility location and several graph and hypergraph cut problems as special cases, and it appears in operations research wherever a value exhibits diminishing returns but is not monotone (profit that combines coverage with a cost, for example). These problems are NP-hard, so the question is which fraction of the optimum an efficient algorithm can guarantee when the function is accessible only through a value oracle that returns for a queried set .
Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor approximation algorithms for maximizing a general nonnegative submodular function. The simplest of them returns a uniformly random set and achieves of the optimum; this mission is about the next one, a nonadaptive algorithm: it decides all of its oracle queries before seeing any answer, then computes a set from the answers. Such an algorithm can be run in one round of parallel queries. The paper shows that this restricted access already beats and reaches .
Timeline. For Max Directed Cut, a random cut achieves . Feige, Mirrokni and Vondrák (FOCS 2007; journal version 2011) proved for a random set and nonadaptively for general nonnegative submodular functions, and by adaptive local search, and that requires exponentially many queries. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012, SIAM J. Comput. 2015) later reached the optimal with a randomized double-greedy algorithm.
Let be a finite ground set with elements. A function is submodular (Definition 1.1) if
Throughout, is nonnegative, the paper's standing assumption, and .
For , denotes the random subset of containing each element independently with probability ; is a uniformly random subset. For a set , is the analogous random subset of . The averaged marginal value of an element (Definition 2.4) is
Algorithm NA (p. 1139):
Given the estimates, the expected value NA returns is .
For every nonnegative submodular and every estimate with for all ,
The printed theorem says "at least "; the term is what the proof establishes (p. 1140, last display).
Milestones 3–7 are the displayed steps of the proof of Theorem 2.6, stated for arbitrary sets where the page's argument does not use the optimality of .
The theorem shows that nonadaptive access, a fixed batch of polynomially many value queries followed by a computation, suffices for a -approximation of unconstrained nonnegative submodular maximization, strictly better than the of any algorithm that must return one of its queried sets (the paper shows is optimal in that class, §4.2). The quantity generalizes the in-degree/out-degree test for Max Directed Cut to arbitrary submodular functions, and Lemmas 2.2 and 2.3 are general sampling inequalities for submodular functions that the paper reuses for its adaptive smooth local search.
Formalizing it produces machine-checked versions of Lemmas 2.2 and 2.3 as statements about exact finite averages, a reusable expectation operator on product-distributed random subsets, and a checked version of the argument with its explicit error term. The result is proved in the paper; to our knowledge none of it has been formalized in a proof assistant.
The two regimes the proof separates, " is already good" and "one of , is large", must be tied to the value of a uniformly random set, whereas the elements of and are chosen from estimated averages, not from the optimal set . The natural attempt, comparing with element by element, fails because is not monotone: adding elements of to can decrease the value. The accuracy of the estimates must also be propagated through a sum over up to elements, which is where the error term comes from. The sampling lemmas require handling expectations over pairs of independent random subsets of possibly overlapping sets.
Fintype X with DecidableEq, assumed Nonempty, so and the divisions by and are genuine; sets are Finset X; is real valued with nonnegativity as an explicit hypothesis. Lemmas 2.2 and 2.3 are stated for real with no sign condition, as printed.Finset.univ.sup' _ f, the true maximum over all subsets.Welcome contributions: proofs of Lemmas 2.2 and 2.3 (reusable for mission IV of this series), the identity , and general lemmas about the operator (splitting a uniform random set along a partition).
The continuous-review policy is the standard replenishment rule of inventory theory: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point , order a fixed order quantity . It is used in practice and taught in every operations management course, usually after the deterministic economic order quantity (EOQ) model, which is the same system with a constant demand stream.
Practitioners and textbooks rely on a robustness property of the EOQ: its cost is very insensitive to the choice of order quantity. If the order quantity is off by a factor , the cost rises only by the factor ; ordering 50% too much costs about 8% extra. The insensitivity of the stochastic system to its control parameters had been observed numerically (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978), but, as Zheng notes, no analytical result on it was known.
Timeline:
Demands arrive at rate ; orders arrive after a fixed leadtime ; all stockouts are backordered. Each order costs ; holding costs accrue at rate per unit in stock and penalty costs at rate per unit backordered. The leadtime demand has distribution with finite mean .
The inventory cost rate at inventory position is
assumed to attain its minimum at a unique point . The long-run average cost of the policy is
For fixed let be a reorder point minimizing , and let
is the cost of the order quantity when the reorder point is always chosen optimally for it. An optimal order quantity minimizes over , and .
The EOQ model is the same system with the constant leadtime demand . Its cost rate is , and , , are the objects above at , with optimum and .
The goal holds for every demand distribution satisfying the standing assumptions and every optimal . Both regimes, and , are included.
In the order the proof uses them:
In the EOQ model the relative cost of a scaled order quantity is exactly (Eq. (25) of the paper). Theorem 4 shows that the stochastic system is at least as forgiving. The bound holds for every leadtime-demand distribution with a unique newsvendor minimizer, and it does not depend on the parameters , , , or . Because the reorder point is re-optimized for each quantity, the bound applies to the practical question of how much a misestimated lot size costs when the safety stock is set correctly.
Together with the other results of the paper (the bound for the EOQ heuristic and the bounds between and , which are separate missions of this series), it gives a closed-form account of why the EOQ is a good heuristic for stochastic systems.
The result has a complete published proof. It has not been machine-checked. The work that remains is a formal proof for general distributions: the paper differentiates and twice, and a formal proof has to replace those derivatives with arguments that need no density.
is defined through an inner minimization over the reorder point, so its shape in is controlled by the implicitly defined function rather than by directly. The obvious approach would bound with the reorder point fixed at . That approach is the wrong comparison: it bounds a larger quantity, and the resulting bound depends on the distribution.
The paper's proof uses three properties of : that it is convex, that its slope never exceeds the EOQ slope , and that it dominates . The paper obtains these from the derivatives and under a smooth demand distribution. Without a density, is only an argmin and need not be differentiable, so none of these three properties can be read off a derivative formula; the asymptotic slope in particular depends on the finite mean and on the behaviour of at .
The mission is set in Lean 4 with Mathlib. All objects are real valued.
QRModel bundles , a probability measure on with integrable identity, , almost surely, and the unique-minimizer hypothesis on . is implicit in the paper and made explicit here. No density is assumed; deterministic and discrete demands are allowed, and the paper's own numerical study uses Poisson demand.IsOptQty Q, meaning and for all . Its existence is asserted in the Eq. (8) milestone, so the goal is not vacuous. "" is a real with real division . In Lemma 9 the integral is oriented, as on the page.A complete development needs the following:
These facts about newsvendor cost functions are reusable in the other missions of this series. Contributions of any of them as separate lemmas are welcome.
The continuous-review policy is the standard control rule for a single stocked item with random demand: whenever the inventory position falls to the reorder point , an order of fixed size is placed. It is implemented in a large share of commercial inventory systems. Choosing the two parameters jointly has traditionally required numerical search (Hadley and Whitin, 1963; Federgruen and Zheng, 1992). In practice the order quantity is therefore often taken from the deterministic economic order quantity (EOQ) formula with backorders, and the reorder point is then set for the random demand.
Zheng (1992) turned this practice into a question with an exact answer: how does the optimal order quantity of the stochastic model compare with the EOQ quantity computed from the same cost data and the same mean demand? Its Theorem 2 answers it with a two-sided bound. This mission formalizes that theorem. Companion missions of the same series formalize the paper's cost bounds (Theorem 3), the flatness of the cost curve (Theorem 4) and the bound on the cost of using the EOQ quantity (Theorem 5).
Demand arrives at rate and replenishment orders arrive after a fixed leadtime . Shortages are backordered. Holding costs accrue at rate per unit held, backorder penalties at rate per unit short, and every order costs . The leadtime demand is a nonnegative random variable with law and mean . The expected inventory cost rate at inventory position is the newsvendor cost
assumed, as in the paper, to attain its minimum at a unique point . The long-run average cost of the policy is
For each , let be an optimal reorder point, i.e. a minimizer of . The analysis runs through the curves
and through the cost of order quantity with the reorder point set optimally. The optimal order quantity is the minimizer of over .
The EOQ model is the case of a constant leadtime demand . Its cost rate is , and the same construction gives , , and the optimal quantity
For , let , , be the positive solutions of
Each has exactly one positive solution, and
Moreover, with and the demand law fixed, is nondecreasing on and converges to a finite constant as .
The milestones are the paper's own numbered results that feed Theorem 2, listed in the order the argument uses them:
The result. Theorem 2 says that the EOQ formula always underestimates the optimal order quantity when leadtime demand is random. The underestimate is bounded by , a quantity that stays bounded however large the ordering cost is. So the relative error of the EOQ quantity vanishes as grows. The first inequality, , is also an ingredient of the paper's Theorem 3 (cost bounds) and Theorem 5 (the EOQ quantity raises costs by at most ). The explicit bounds , , bracket and give a search interval for it.
Formalizing it. The theorem has been proved on paper since 1992. No machine-checked version of it, or of the continuous-review cost of Eq. (1), exists on this platform. The inventory items already here treat the discrete cost with integer order quantities, a normally distributed demand, or the EOQ without backorders. This mission provides a machine-checked version of the paper's optimality conditions for a general demand distribution. The paper's argument differentiates twice, i.e. it tacitly assumes a density. The formal statements do not, so a formal proof must redo those steps with one-sided (convexity) arguments. The printed argument for the limit in part (b) shows only that a derivative tends to zero. A complete proof of convergence is part of the work.
The obvious route to compares the two cost curves and directly. It fails because pointwise, and a pointwise inequality between two convex functions says nothing about the order of their minimizers. The stochastic curve is defined only implicitly, as evaluated at a minimizer of a parametric integral, so its growth relative to the linear has to be established before any comparison of order quantities. For part (b), a vanishing derivative does not imply convergence ( also has a vanishing derivative), so the printed proof of the limit does not go through as written.
Without a density, need not be differentiable. Every derivative in the paper's proofs (of , and ) must be replaced by monotonicity or chord arguments.
The Lean development uses the namespace ZhengQR.OrderQty. Its conventions:
Infrastructure needed includes the following. Much of it is reusable for any single-item inventory model:
Contributions welcome: proofs of the milestones in any order, general lemmas on the newsvendor cost, and a complete convergence argument for part (b).
Firms that can buy the same item from two suppliers, a cheap slow one and a fast expensive one, face the dual-sourcing inventory problem: how much to order from each source in every period when demand is random and unmet demand is backlogged. Global sourcing (offshore regular supply plus a near-shore express supply) is the standard example (Allon and Van Mieghem 2010). When the two lead times differ by more than one period, the optimal policy depends on the whole pipeline of outstanding orders. No simple optimal policy is known, and dynamic programming is intractable for long lead times.
The tailored base-surge (TBS) policy orders a constant amount from the slow source and uses the fast source to bring the expedited inventory position up to a fixed level. It is simple, and it is used in practice. Janakiraman, Seshadri and Sheopuri (JSS, Management Science 2015) showed that its best parameters solve a convex program that does not depend on the regular lead time, and they conjectured, with numerical support, that TBS is near-optimal when that lead time is long.
Timeline:
Let be a nonnegative random variable with finite mean that is not almost surely constant. Demands are i.i.d. copies of . The regular source has lead time , the express source has lead time , and . In period the controller orders and ; then arrives and is realized, so the on-hand inventory evolves as and may be negative. Initially nothing is on order and , where the are further i.i.d. copies of and , .
The per-period cost is with , where and is the express premium (the regular unit cost is normalized to ). An admissible policy chooses the two orders in period as deterministic measurable functions of . Its long-run average cost is
With the expedited inventory position , the TBS policy orders and . A best TBS pair minimizes over and (first in through , then in ).
The constants and are explicit functionals of the law of and of . They are built from , , , the mean absolute deviation , and the large-deviation quantities of (p. 441).
For all , and ,
The threshold does not depend on , so the statement gives an explicit, inverse-polynomial rate. Its limit form is Corollary 1 of the paper.
In the order the proof uses them:
The theorem shows that one of the simplest dual-sourcing heuristics is asymptotically optimal as the regular lead time grows. This is the regime where exact dynamic programming is hopeless. The best TBS parameters come from a convex program independent of , so the result yields an algorithm whose running time does not grow with and whose optimality gap is bounded explicitly for every finite . It extends the lower-bounding technique of Xin and Goldberg's lost-sales work (Operations Research 2016) from a static to a dynamic relaxation.
Formalization adds the following. To the best of available knowledge, none of the objects involved (average-cost inventory control with backlog, TBS policies, Lindley-type maxima of random walks with their Spitzer identity) exists in Mathlib or on the platform. The paper's proof defers several ingredients to the literature or omits them: Lemma 1, Eq. (3), Lemma 3, and the details of Lemmas 5 and 7. A complete formal proof must supply them. The result is proved on paper but not formalized anywhere.
An optimal dual-sourcing policy need not be stationary, its induced Markov chain need not have a stationary distribution, and the inventory is unbounded below. The natural argument would compare the optimal policy's steady state with the TBS steady state, and it fails at its first step. Theorem 2 replaces the steady state by a vector with a few distributional properties, built from time averages. That construction, and the independence structure it must carry, is the central technical step. The conditional Jensen step then leads to a single-source problem with possibly negative demand, where textbook interchange-of-limits theorems do not apply directly. Finally, bounding away from requires a quantitative lower bound on the growth of random-walk maxima under only a first-moment assumption.
Conventions of the Lean development (namespace XinGoldbergTBS.Asymptotic):
Lemma 1, Eq. (3) and Lemma 3 are results the paper quotes from Sheopuri et al. (2010), JSS and Scarf (1960). Proposition 1 (conditional-expectation form of the bound) is not included.
A trivializing formalization is ruled out: ranges over the full admissible class, the constants are definitions rather than hypotheses, and the goal includes an existence clause.
Reusable beyond this mission: average-cost inventory models with lead times, discounted single-source backlog value functions, and Spitzer-type identities for random-walk maxima. Contributions to any milestone are welcome.
A Markovian decision process (Howard, 1960) models a controller who, in each of finitely many states, picks a decision, earns a reward and moves to a random next state according to known transition probabilities. In applications (inventory control, equipment replacement, quality control) those probabilities are estimated, not known. Satia and Lave (Operations Research 21(3), 1973) treat the uncertainty in two ways: a game-theoretic formulation, in which each unknown row only lies in a given set, and a Bayesian formulation, going back to Silver (1963) and Martin (1967), in which the controller holds a prior on the unknown matrix and learns from observed transitions.
The Bayesian problem is the natural one but its state includes the whole prior, so it cannot be solved exactly beyond small cases. The paper's contribution in the Bayesian part is a pair of computable bounds on the Bayesian optimal return in terms of the two game-theoretic values (max-max and max-min). This mission formalizes those bounds and the chain of facts they rest on.
There are states and, in state , a finite nonempty set of decisions. A transition under decision earns and rewards are discounted by , . The row of transition probabilities is unknown; it is known to lie in a closed convex nonempty set of probability vectors, and .
A prior is a probability distribution on matrices whose rows are all probability vectors. Its means are . After a transition under decision the prior is replaced by the Bayes transformation (Eq. (8)), with the normalizing constant. The Bayesian optimal return solves the recursion
The max-max and max-min values , solve
with max for and min for . Finally , the prior probability that the true matrix lies in .
The Lean development lives in the namespace SatiaLave.Bayes: UncertainMDP, IsPrior, pbar, bayes, SolvesEq10, SolvesVplus, SolvesVminus, alpha, rmax, rmin, policyValue.
For every bounded solution of (10), all solutions , , every prior and every state ,
together with the existence of , and . Both halves are the paper's printed statements.
The result. The bounds sandwich an intractable quantity between two quantities computable by finite algorithms (the max-max and max-min policy-iteration procedures of the same paper), weighted by a single prior probability . When the prior concentrates on () the bounds become : the Bayesian return lies between the pessimistic and optimistic robust values. They are the upper and lower bounds on the return that the paper's implicit-enumeration method (the decision tree of its Fig. 2 and Proposition 12) uses to compare decisions. The Jensen step is a value-of-information inequality (Bayesian optimal return is at most the expected full-information optimal return), which recurs throughout Bayesian control and bandit theory.
Formalizing it. The results are proved on paper (Propositions 6 and 8 by reference to Martin's book and Satia's thesis, Propositions 9 and 10 in the text); none is machine-checked. The mission produces a Lean model of Bayes-adaptive Markov decision processes with priors as measures, the Bayes transformation and its fixed-point recursion, and the link between the Bayesian and the robust (rectangular) formulations. Martin's existence-uniqueness theorem and the convexity of the Bayesian value are reusable for any Bayes-adaptive model.
The prior space is infinite-dimensional and not a vector space, so the recursion (10) lives on a space of measures, and the usual finite-state arguments do not apply verbatim. Proposition 8 gives convexity only along finite mixtures, while the proof of Proposition 9 applies Jensen's inequality to the integral mixture of point masses; bridging the two, or proving the value-of-information inequality directly, is the central step. The paper also restricts the point masses to , which cannot represent a prior with mass outside ; the formal statement integrates over every transition matrix, as the next line of the paper's display requires. Measurability of is not automatic, since is only characterized by a functional equation.
Fintype S; decisions a dependent family D i of nonempty finite types. A matrix is P : (i : S) → D i → S → ℝ with the product Borel -algebra.bayes then returns . That posterior is always multiplied by in (10), so the choice is immaterial.⨆/⨅ over a nonempty bounded set. "Obviously " is stated for every pure stationary policy , not only a max-min optimal one. The policy return is the componentwise series .Welcome contributions: the Banach fixed-point argument for (10) on bounded functions of priors; lemmas that bayes maps priors to priors and that point masses are fixed; continuity of the known- optimal value in ; a general Jensen inequality for functions convex along mixtures of probability measures.
Semidefinite programming (SDP) optimizes a linear function over the intersection of the cone of positive semidefinite matrices with an affine subspace. It contains linear programming as the diagonal case and is the computational core of relaxations in combinatorial optimization, control theory and polynomial optimization. Its standard duality theory, however, is weaker than that of linear programming. The Lagrangian dual of an SDP can have a strictly positive duality gap, can fail to attain its optimal value, and an infeasible semidefinite system need not have a certificate of infeasibility of the naive Farkas form. All the classical strong duality theorems for SDP therefore assume a constraint qualification such as Slater's condition (a strictly feasible point).
M. V. Ramana (1997, Math. Program. 77, 129–162) constructed a dual, the Extended Lagrange–Slater Dual (ELSD), whose size is polynomial in the data and which enjoys every property of linear programming duality for every SDP, with no constraint qualification. The same construction yields an exact theorem of the alternative for semidefinite feasibility and the complexity consequence that semidefinite feasibility lies in NP if and only if it lies in co-NP in the Turing model.
Timeline:
Let be natural numbers, the space of real matrices, and the symmetric ones. On the inner product is . For symmetric , means is positive semidefinite. The data are symmetric and . The primal SDP is
with feasible region , a spectrahedron. Define by and write for " and ".
For let be the set of tuples of real matrices with and, for ,
The need not be symmetric. and are the sets of last components and ; . The ELSD is
and Weak-ELSD is the same program with . For the milestones: the polar , the algebraic polar , and .
For all data :
Propositions 7(vi) and 7(vii) (facts on PSD matrices), Lemma 9 (annihilation ), weak duality over every , Lemma 10 (nested subspaces), Lemma 13 (), Corollary 14, Claims 17 and 16, the central Theorem 12,
the translation invariance of (§2.5), and system (14) (dual attainment at value 0). Theorems 19–21 (Farkas lemma for SDP, optimality condition, primal attainment) are further items stated on the same definitions.
The Duality Theorem gives SDP a dual with the full strength of linear programming duality for every instance, at polynomial size. Consequences in the paper: an exact theorem of the alternative for semidefinite feasibility (Theorem 19); semidefinite characterizations of optimality of a given point and of primal attainment (Theorems 20, 21); and the complexity results that semidefinite feasibility is in NP iff it is in co-NP in the Turing model and in NP ∩ co-NP in the Blum–Shub–Smale model (Theorem 25, not part of this mission). Theorem 12 separately gives an exact semidefinite description of the polar of any spectrahedron containing the origin.
The results are proved on paper and are classical. No machine-checked version is known to exist; the platform's existing SDP duality theorem assumes Slater's condition. A formalization would provide the first constraint-qualification-free SDP duality in Lean, together with reusable infrastructure on PSD matrices (range inclusion, ) and on polars of convex sets.
The obvious route to SDP strong duality separates the primal's value from the image of the PSD cone under a linear map and invokes a closed-cone Farkas lemma. That step fails: the linear image of the PSD cone need not be closed, which is exactly why Lagrangian duality has gaps. In this mission the obstruction reappears as the non-closedness of the algebraic polar (Lemma 13 only gives ). The difficulty is to show that finitely many, and at most , corrections by the sets close (Claims 16, 17), and to control dimensions in doing so. A proof by assuming closedness, strict feasibility or a Slater point is a different theorem.
Everything lives in the namespace ExactSDPDuality.ELSD, in one definition file. Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin m → ℝ; "" is Mathlib's PosSemidef (which over ℝ includes symmetry); is the entrywise sum on all of ; is the dot product. The data carry symmetry hypotheses in every statement, as the paper assumes throughout. is encoded by sequences with , so ; for the index is . Optimal values are least upper and greatest lower bounds of the value sets, never real sSup/sInf. The polar is the one-sided polar. In §2.4 statements the standing assumption is a hypothesis. In Claim 16 the index satisfies , the range where is introduced, and is the rank of the span of .
Theorems 20 and 21 are printed with ; both are false as printed (counterexamples in the items) and are stated with the corrected that the paper's derivation from Theorem 6 gives.
Trivializing formalizations are ruled out: no Slater or other constraint qualification appears; the dual is the ELSD built from the recursively defined , not the Lagrangian dual or an arbitrary subspace; the range over all of , not only symmetric matrices (the paper's Example 4 needs a nonsymmetric ).
Needed infrastructure: PSD matrix facts (Proposition 7), bipolar theorem for closed convex sets containing the origin (Proposition 11), closedness arguments for linear images of cones, and dimension counting of subspaces of . Contributions of any milestone, of these general lemmas, and of alternative proofs (for instance via facial reduction) are welcome.
Many problems in optimization and equilibrium modelling reduce to a system of equations whose map is Lipschitz but not differentiable: reformulations of nonlinear complementarity problems through the componentwise minimum or the Fischer–Burmeister function, Karush–Kuhn–Tucker systems of constrained programs, and gradients of augmented Lagrangians all have kinks. Newton's method, , is the standard fast local solver for smooth systems, but it needs a derivative at every iterate.
Qi and Sun (Math. Programming 58, 1993) replaced the Jacobian by an arbitrary element of Clarke's generalized Jacobian and showed that the resulting method converges locally superlinearly under a regularity condition they called semismoothness, extending Mifflin's notion for functionals (Mifflin, SIAM J. Control Optim. 15, 1977) to vector-valued maps. This theorem is the foundation of the family of semismooth Newton methods used in complementarity, variational inequalities and PDE-constrained optimization.
Timeline. Robinson (1988) and Pang (Math. OR 15, 1990) studied Newton methods built on B-derivatives, with convergence proved under a strong Fréchet derivative at the solution; Kummer (1988) gave an abstract framework for Newton methods for nonsmooth equations; Qi and Sun (1993) proved local superlinear convergence for the generalized-Jacobian iteration under semismoothness and nonsingularity of , with order under -order semismoothness.
Let be locally Lipschitz. By Rademacher's theorem is differentiable on a set of full measure; write for the Jacobian at . The generalized Jacobian is
the convex hull of all limits of Jacobians along sequences of differentiability points converging to . The one-sided directional derivative is .
is semismooth at if it is Lipschitz near and, for every , the limit of over , , exists. For , is -order semismooth at if in addition for , .
For , the nonsmooth Newton method is
where any element of may be chosen at each step. A run is a pair of sequences , with and for all . A root () is regular when every is nonsingular.
Let be locally Lipschitz, , semismooth at , and every nonsingular. Then there is such that every with is nonsingular, a Newton step from such a stays within of , and every run with satisfies
The goal asserts only the shape of the convergence (superlinear) and fixes no constants.
If moreover is -order semismooth at , , there are and with
for every run started within of .
The milestones follow the paper's route: Proposition 2.1 (the limit in the definition of semismoothness is the directional derivative), Lemma 2.2 (Lipschitz continuity of and its realisation by an element of ), Theorem 2.3 (semismoothness is equivalent to and to the corresponding condition at differentiability points), the Remark's expansion (2.17), Proposition 3.1 (uniform invertibility near a regular point), the order- sentence of Theorem 3.2, and Corollary 2.5 (strong Fréchet differentiability implies semismoothness).
The theorem gives a locally superlinearly convergent method for Lipschitz equations with no smoothness beyond semismoothness at the root. Convex, smooth and subsmooth functions are semismooth, as are sums and scalar products of semismooth functions (the paper, citing Mifflin), and later work showed that the complementarity and KKT reformulations on which semismooth Newton solvers are built are semismooth as well; the order- variant gives local quadratic convergence for strongly semismooth maps. Mission II of this series treats the paper's global convergence theorem on a ball, and Mission III the semismoothness of augmented Lagrangian gradients, which supplies the application.
The results are proved in the paper. No machine-checked version of the generalized Jacobian, of semismoothness or of the nonsmooth Newton method is known to exist in Mathlib or on this platform; the platform's formalized Newton results concern one-dimensional functions (MetodosNumericos.newton_local_convergence) and smooth convex minimization. A complete development would provide the first formal library for Clarke's generalized Jacobian and semismooth maps.
The classical Newton proof compares with its linearization and uses continuity of the Jacobian at . Here neither is available: need not be differentiable at or at any iterate, the element is chosen arbitrarily from a set, and need not be close to any fixed linear map. The comparison has to go through the directional derivative , which is only positively homogeneous, not linear. The analytic content therefore sits in Section 2: showing that semismoothness, defined through a limit over a set-valued map, controls uniformly in the direction, and that is small. Both rest on Clarke's mean-value inclusion and on compactness and upper semicontinuity of , none of which is in Mathlib. The superlinear rate also requires a uniform bound on in a whole neighbourhood, not just at .
Everything lives in the namespace NonsmoothNewton.Local. Section 2 results are stated for maps between finite-dimensional real normed spaces (the paper's is the Euclidean instance); Section 3 results use EuclideanSpace ℝ (Fin n). Conventions fixed by the Lean statements:
fderiv; the generalized Jacobian is the convex hull (no closure) of limits of fderiv along sequences of differentiability points.lineDeriv; its value is a limUnder, used only where existence is a hypothesis or a consequence.IsUnit in the ring of continuous linear endomorphisms; is a two-sided inverse of operator norm at most .IsLittleO along atTop; the printed Theorem 3.2 states only well-definedness and convergence. "Order " is pinned as with and uniform over runs. Every in (2.8), (2.9) and (2.17) is its – form with a non-strict inequality , and every is an explicit constant and radius.HasStrictFDerivAt, which corrects the misprint for in the paper's display (2.16).A trivializing formalization is ruled out: the update is not written with a junk inverse (which would make a singular step "well defined"), the generalized Jacobian is the paper's nonempty set rather than one that could be empty, and the theorem quantifies over every run rather than asserting that some run converges.
A complete development needs Clarke's mean-value inclusion (2.2), compactness and upper semicontinuity of for locally Lipschitz maps (via Rademacher's theorem, available in Mathlib), and perturbation bounds for inverses of linear maps. The generalized-Jacobian and semismoothness layer is reusable beyond this mission, in particular for Missions II and III of this series. Contributions of proofs of any milestone, and of general lemmas about , are welcome.
Connecting a set of terminals by a network of direct links of least total length is one of the oldest problems of combinatorial optimization. R. C. Prim's 1957 paper in the Bell System Technical Journal (DOI) was motivated by the rate structure for Bell System leased-line services, in which the charge for connecting a set of terminals depends on the length of a shortest network connecting them. The paper states two local construction principles, P1 and P2, and shows that any sequence of their applications produces a shortest network, first for points in the plane and then for arbitrary connected labelled graphs with arbitrary real edge lengths. The paper's §V specialization of the principles, growing a single fragment, is what is now called Prim's algorithm, and its §IV statement is the form of the minimum spanning tree theorem used throughout network design, clustering and approximation algorithms.
Timeline. O. Borůvka (1926) solved the problem for an electrical network in Moravia; V. Jarník (1930) gave the single-fragment procedure; J. B. Kruskal (1956, Proc. AMS 7, 48–50) proved that adding globally shortest links avoiding cycles yields a shortest spanning tree; Prim (1957) gave the more permissive principles P1 and P2, which contain both the Jarník procedure and Kruskal's rule as special orders of application; E. W. Dijkstra (1959) rediscovered the single-fragment procedure.
Let be a finite set of terminals and a simple graph on , the labelled graph whose edges are the possible links. Each edge carries a real length ; lengths may be negative, zero, or tie. For a finite set of links, denotes the graph on whose edges are the links of .
Only edges of are possible links; in Prim's distance table a missing edge has length .
For every finite connected graph and every ,
This is the sentence "P1 and P2 will provide a SSS for any connected labelled graph with any set of real edge lengths." It fixes nothing about the order of applications, the component chosen, or the tie-breaking.
The goal is the correctness theorem of a whole family of greedy minimum spanning tree procedures at once: Jarník–Prim (one growing fragment), Kruskal (globally shortest link first) and Borůvka-style interleavings all produce sequences of P1/P2 applications. Because lengths are arbitrary reals, it also covers maximum spanning trees by a sign change (p. 1397) and graphs that are not complete.
The result is classical and fully proved in the literature. What this mission adds is a machine-checked statement in exactly Prim's generality. Mathlib has spanning trees of connected graphs (SimpleGraph.Connected.exists_isTree_le) and the edge count of trees, but no minimum spanning tree theory. Existing Prove2Me items on minimum spanning trees are either restricted to complete graphs with distance matrices or state a cut property in existence form at a single vertex; none states Prim's principles or his necessary conditions.
The obvious argument, "each link P1 or P2 adds belongs to the shortest network", uses a unique shortest network, and that fails with ties: when two links tie, a P1/P2 link need not lie in a given SSS. Prim's own treatment of ties (§III) is an informal perturbation argument; the formal statement must hold for every tie-breaking choice made during a construction, not only for a generic perturbed instance. Negative lengths remove the easy reading "shortest connected spanning subgraph": the minimum must range over trees only. The statements also involve the component structure of as it changes during a construction, and tree paths in an arbitrary, not necessarily complete, graph.
Namespace ShortestConnection.Principles, Mathlib SimpleGraph. Conventions:
Fintype with decidable equality; is a SimpleGraph V (at most one link per pair, no loops, which is Prim's setting). Lengths are w : Sym2 V → ℝ; only values on edges of matter.Finset (Sym2 V); linkGraph F is SimpleGraph.fromEdgeSet F. A spanning subtree requires ↑F ⊆ G.edgeSet and (linkGraph F).IsTree.linkGraph F; the P2 condition is a single inequality against every -edge leaving it, which is equivalent to "nearest neighbor and shortest link" in Prim's sense.List (Sym2 V) checked entrywise against l.take i; complete means length Fintype.card V - 1 (natural subtraction, used only for nonempty ).sInf of the lengths of spanning subtrees; continuity is in the product topology.Implicit hypotheses made explicit: connected (hence ) wherever an SSS or a complete construction is involved; at least two terminals for Necessary Condition 1; nonempty and for Necessary Condition 2; pairwise distinct edge lengths only in milestone 4, as in the paper's temporary assumption.
The goal's existence clause rules out a vacuous formalization in which no complete construction exists; the step predicates are defined from lengths and components only, never through shortest spanning subtrees, and they are not restricted to one growing fragment or to the globally shortest link.
Needed infrastructure: tree exchange (adding an edge to a spanning tree creates one cycle; removing any other cycle edge yields a spanning tree), component counts under edge addition, and minima of finitely many continuous functions. The exchange and counting lemmas are reusable for any matroid-greedy or spanning-tree mission. Contributions of intermediate lemmas, and proofs of the milestones in any order, are welcome.
Quasi-Newton methods minimize a smooth function on by moving along , where is the gradient and is an approximation of the inverse Hessian built from observed gradient differences. The BFGS update is the most widely used way of building , but it stores a dense matrix, which is prohibitive for large .
Nocedal's 1980 paper (Math. Comp. 35, 773–782) proposed keeping only the last correction pairs and rebuilding the matrix from a simple initial matrix at every step. The resulting method, called SQN in the paper, is now known as L-BFGS, and it is the default large-scale unconstrained optimizer in many numerical libraries and in machine learning. The paper's main theoretical claim is that this truncation does not destroy the finite termination of BFGS on quadratics.
Timeline:
Let be a symmetric positive definite matrix and , and let , a strictly convex quadratic with gradient and unique minimizer .
Exact line search. Along a direction from , the step minimizes .
BFGS update. For a pair with and , the BFGS update of is
Special BFGS matrices. Fix symmetric positive definite and a number of stored corrections. Given pairs , the special matrix is updated by the pairs , oldest first (the paper's (4)–(5)). Only the most recent pairs enter, and the matrix is rebuilt from .
SQN. Starting from , with :
with the exact step and the special matrix built from the last pairs.
PCG with fixed preconditioner . , , with .
For every , every symmetric positive definite and , every , and every ,
where are the SQN iterates. The statement fixes no constant beyond the dimension bound .
The result shows that storing only correction pairs costs nothing on quadratics: for any , SQN terminates in at most steps, like full BFGS and conjugate gradients. It explains why L-BFGS with small is competitive, and it is the model case for later analyses of limited-memory methods (their linear convergence on uniformly convex functions, and their relation to Krylov methods). Property (b) is the reason one expects efficiency to grow with : the matrix satisfies the secant equation on the most recent directions.
The claims are classical and generally accepted, but the paper argues them in a few lines ("it is straightforward to show"), deferring the PCG facts (15)–(16) to a reference. No machine-checked proof of the termination of BFGS, L-BFGS or preconditioned conjugate gradients is known to this mission. A formalization would provide a verified model of L-BFGS on quadratics and a reusable development of conjugate-direction methods with a preconditioner.
The obvious route, "SQN is BFGS and BFGS terminates", fails: SQN discards old corrections, so the classical BFGS argument (hereditary secant conditions on all past directions) does not apply once more than steps have been taken. The paper asserts the identity of SQN with preconditioned conjugate gradients in one sentence ("using a similar argument as for the SCG"), and the PCG relations it relies on are quoted from a technical report. The other difficulty is bookkeeping: the window of stored pairs shifts, the matrix is a nested product, and the runs must remain meaningful after the minimizer is reached.
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, is dotProduct, and is Matrix.vecMulVec. Symmetric positive definiteness is Matrix.PosDef. Indices are 0-based, as in the paper. The exact line search is the closed-form step . The iterations have no stopping rule: once the gradient vanishes the direction and step are zero and the iterate stays at the minimizer (Lean's ). Past that point the zero pair stored by SQN leaves the BFGS step unchanged. The hypotheses are exactly the paper's: , , and exact line searches. need not be diagonal.
Two misprints are corrected and flagged in the items: the denominator of in (13) is (as in (12) and p. 778), and the second relation of (16) is stated for (as used on p. 778), since it fails for .
Ruled out: SQN is defined through its own matrices (4)–(5), rebuilt from and the last pairs. It is not defined through the PCG recurrence, not by one BFGS update of the previous matrix, and not with a stop rule that returns . The standing assumption is not a hypothesis of any statement about a run (it fails after termination and would make the goal vacuous). With SQN is steepest descent and the goal is false, so is required.
Needed infrastructure: algebra of rank-one updates and of Matrix.PosDef under congruence, conjugate-direction lemmas for quadratics, and the fact that mutually -orthogonal vectors in include a zero vector. The PCG results (milestones 5–7) are reusable beyond this mission. Proofs of any milestone, or of the goal directly, are welcome.
Newton's method is the standard second-order algorithm for unconstrained minimization, but without safeguards it has no global guarantee: far from a minimizer the Newton step can increase the objective, and at a point where the Hessian is indefinite the step can head for a saddle point or a maximum. The usual repairs (line search, trust regions, Levenberg–Marquardt damping) come with convergence proofs, but for nonconvex objectives those proofs typically give no rate at all, or only the rate of the gradient method.
Nesterov and Polyak (Math. Program. 108 (2006) 177–205) proposed to regularize the second-order Taylor model of the objective with a cubic term and to take as the next iterate a global minimizer of the regularized model. They showed that the resulting method has a global worst-case rate of convergence to points satisfying the second-order necessary conditions, for every objective with a Lipschitz continuous Hessian and without any convexity. That rate, for the gradient norm, is better than the of the gradient method. It became the reference point for the complexity theory of nonconvex second-order optimization: adaptive variants (Cartis, Gould and Toint, Math. Program. 127 (2011) 245–295) and lower bounds showing that iterations are optimal among second-order methods (Carmon, Duchi, Hinder and Sidford, Math. Program. 184 (2020) 71–120) are stated against it.
This mission formalizes the general convergence result of that paper, Theorem 1 of Section 3, together with the properties of the cubic step from Section 2 on which it rests.
Let be a closed convex set with nonempty interior, and let be twice differentiable on with gradient and Hessian . A starting point is fixed, and is assumed to contain the level set in its interior. Assumption 1: the Hessian is Lipschitz continuous on in the spectral norm, for all , with .
For a parameter the cubic model of at is
The cubic-regularized Newton step is any global minimizer of over ; it exists because the model is continuous and coercive. Write and .
The cubic regularization of Newton method (3.3) fixes , starts at and, for , chooses such that , then sets . The choice always passes the test.
Write for the smallest eigenvalue of a symmetric matrix . The measure of local optimality is
It is nonnegative and vanishes exactly when and .
If for all , then every run of method (3.3) satisfies, for every ,
The constant and the exponent are the paper's; the statement holds for every admissible choice of the parameters and of the global minimizers .
Inequality (3.4) is a global, dimension-free complexity bound for reaching approximate second-order stationarity. It controls both the gradient norm, , and the most negative curvature, , along the best iterate, from a single scalar potential . The second claim of Theorem 1 gives the asymptotic counterpart: every limit point satisfies the second-order necessary conditions. Section 4 of the paper derives its faster rates for star-convex and gradient-dominated functions from the same Section 2 lemmas.
The result is proved on paper and widely cited; to our knowledge no machine-checked proof of it or of the Section 2 lemmas exists. A formalization adds a checked statement of the method with its exact constants, and reusable facts about global minimizers of cubic models (Proposition 1 in particular) that the companion missions on star-convex, gradient-dominated and locally quadratic convergence also rely on.
Most steps are short inequalities, but two are not. Proposition 1 is a statement about a global minimizer of a nonconvex function: the first- and second-order conditions of a local minimizer give only , which is weaker. The natural first attempt, "take the second-order optimality condition of the model at ", therefore fails. The paper proves it in Section 5.1 through a one-dimensional dual characterization of the minimizer.
The second is Lemma 2's second claim, used for (2.12): showing that stays in requires a boundary argument along the segment from to , since the Taylor bounds are only available inside . The remaining work is calculus in : the integral form of Taylor's theorem for the gradient under a Lipschitz Hessian, and eigenvalue perturbation for the second entry of .
The space is EuclideanSpace ℝ (Fin n) for arbitrary n : ℕ. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every x ∈ F. At boundary points of this asks for two-sided derivatives, a mild strengthening of "twice differentiable on ". The Lipschitz condition uses the operator norm, which is the spectral norm. is represented by the predicate IsCubicStep (global minimizer of cubicModel), and every lemma is stated for every such minimizer. The run predicate IsCubicNewtonRun is 0-based. It writes as plus the model value at , which is the minimum because attains it. is lamMin, the Rayleigh-quotient infimum over the unit sphere, which equals the smallest eigenvalue for the (symmetric) Hessian. The lower bound is required on only. The minimum over is written as the existence of an index attaining the bound.
A stationary point of the cubic model is not an admissible step, and the run must keep the test and the acceptance test. Replacing the step by any point with makes the goal false, and dropping the square root in makes Lemma 5 false. The statements rule out all three. Lemma 5 carries the hypothesis , which its printed proof uses and which holds at every iterate.
A complete development needs the Taylor bounds (2.2)–(2.3) for vector-valued derivatives on convex sets, and first- and second-order optimality for the cubic model. It also needs a proof of Proposition 1 (Section 5.1 or any other correct argument) and eigenvalue perturbation via Rayleigh quotients. The cubic-model lemmas and Proposition 1 are reusable across the whole series. Proofs of any milestone, alternative proofs of Proposition 1, and general Mathlib-level lemmas about Rayleigh quotients are welcome.
A maximal independent set (MIS) of a graph is a set of vertices, no two adjacent, to which no further vertex can be added. Sequentially an MIS is found greedily in linear time, but the greedy scan is inherently serial. Whether an MIS can be found fast in parallel was a central question of parallel complexity in the early 1980s: an MIS algorithm is a subroutine for maximal matching, vertex colouring with colours, and many other symmetry-breaking tasks.
Luby's algorithm is the standard textbook example of a randomized parallel algorithm and remains the basis of distributed MIS algorithms in the LOCAL model. Its analysis rests on one statement, Theorem 1 of the paper, which this mission formalizes.
All algorithms in the paper run the same loop on a finite simple undirected input graph with vertices. The current graph is , initially . For the neighbourhood is . One execution of the loop body selects a set independent in , adds it to the output, and replaces by the subgraph induced on . The loop stops when is empty.
For write for its neighbours and for its degree. The two Monte Carlo select steps are:
Let be the number of edges of before the -th execution of the loop body. The number of edges eliminated by that execution is : exactly the edges of with at least one endpoint in . For the paper uses the weight .
For the current graph and ,
The constants are those printed in the paper. No connectivity, degree or size condition on is assumed.
Theorem 1 says that each round removes, in expectation, a constant fraction of the remaining edges. From it the paper derives that the expected number of rounds of either algorithm is , and hence that MIS has a Monte Carlo algorithm running in expected time on a CRCW P-RAM and on an EREW P-RAM with processors. Algorithm B and the proof of part (2) are also the basis of the paper's deterministic algorithm: the analysis of Lemma B uses only pairwise independence of the coins. The companion mission (A Simple Parallel Algorithm for the Maximal Independent Set Problem II) formalizes that derandomization and reuses the statements of milestones 2, 5 and 6.
The results are proved in the paper and reproduced in textbooks (e.g. Motwani and Raghavan, Randomized Algorithms), but not formalized: no statement of Theorem 1, Lemma A or Lemma B was found on the platform. A formal proof would make the per-round analysis of a standard parallel randomized algorithm reusable. That includes the degree-weighted counting of milestone 6 and the Bonferroni-type bound of the Technical Lemma, both of which recur in later analyses of distributed symmetry breaking.
The obvious argument tries to show that a fixed vertex enters with good probability. That fails, because a high-degree vertex rarely wins against all its neighbours. The analysis instead bounds the probability that a vertex is removed, i.e. lands in . This event is a union over neighbours of dependent events, so the first Bonferroni inequality alone does not give a lower bound: the pairwise-intersection terms must be controlled. The union bound can also be very lossy when is large, which is why the conclusion involves a minimum with a constant.
A second obstacle is the passage from vertices to edges: vertices of small can have high degree while contributing little probability. The per-vertex bounds therefore have to be summed with degree weights and redistributed over edges. For Algorithm A there is an additional complication: priorities from can collide, so the argument about a uniformly random order holds only on the event that is injective. That event appears as the factor .
SimpleGraph V on a finite type with decidable adjacency, and . The degree is SimpleGraph.degree, is neighborFinset, and is edgeFinset.card.Theorem 1 is false for arbitrary distributions of priorities or coins. A formalization that takes "Pr" as an unconstrained parameter, conditions on the event of interest, or replaces by does not state the paper's theorem.
A complete development needs finite product probability spaces, inclusion–exclusion (Bonferroni) inequalities for finite unions, the symmetry of uniform priorities conditioned on injectivity, and degree-sum identities (SimpleGraph.sum_degrees_eq_twice_card_edges). The Technical Lemma and milestones 5 and 6 are reusable beyond this mission. Proofs of any milestone, and alternative proofs of Lemmas A and B, are welcome.