Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign formalizes classical polynomial-time algorithms that estimate this optimal energy. At ratio , the goal is one randomized classical algorithm which, for every input graph, outputs a number satisfying
The upper bound holds for every random outcome; the approximation ratio is guaranteed in expectation. The optimum includes entangled quantum states. The algorithm returns a classical numerical estimate and requires no physical state preparation. Higher approximation ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Planning in a Markov decision process with a large or infinite state space cannot visit every state. The trajectory tree method of Kearns, Mansour and Ng (2000) finds a near-best policy in a class with a number of generative-model calls independent of the state space, but exponential in the horizon . Chapter 6 of S. M. Kakade's PhD thesis, On the Sample Complexity of Reinforcement Learning (University College London, 2003), trades that exponential factor for a weaker notion of optimality. The weaker notion is tied to a reset distribution that encodes prior knowledge of where good policies spend their time, such as a desired trajectory in robotic control or a known operating regime of a queueing network.
The resulting algorithm, μ-PolicySearch, chooses one decision rule per time step, backward in time, from a hypothesis class , optimizing each against states drawn from . The same idea was later published as Policy Search by Dynamic Programming (Bagnell, Kakade, Ng and Schneider, NeurIPS 2003). Conservative policy iteration (Kakade and Langford, ICML 2002) carries the same reset-distribution idea into the discounted setting.
Timeline:
A T-epoch MDP has a finite state set , a finite nonempty action set , a transition kernel , a deterministic reward and a horizon . Decision epochs are . A non-stationary policy gives a distribution over actions at each state and epoch. A decision rule is a map . A class of decision rules induces the class of deterministic policies that use a rule of at every epoch.
Values are normalized. The -value is times the expected reward collected from epoch to when starting in at epoch , so . The value is . The state-action value is , and the advantage is . The future state-time distribution of from is on .
A μ-reset distribution is a family of distributions on , one per epoch . Its joint law, uniform over epochs, is . For a decision rule the μ-advantage is
and is defined in the same way. The ℓ1 distance of two functions on is .
If a policy satisfies for all and , then for all and all start states ,
Theorem 6.3.1 states what μ-PolicySearch buys. The guarantee holds at every start state, whereas the trajectory tree guarantee holds only at the root it was built for. The policy is guaranteed to compete with each policy of whose future state-time distribution is close to . The penalty makes the role of the reset distribution precise: it is the price of the change from the "training" distribution to the "test" distribution . With Theorem 6.3.2 at , the exact algorithm attains the bound with no slack. The sample-based analysis (Theorem 6.3.3) reduces to controlling the condition.
The results are proved in the thesis, and no machine-checked version is known to exist. The mission produces a Lean development of the normalized T-epoch model (non-stationary policies, -values, advantages, future state-time distributions) together with the undiscounted performance difference lemma. These pieces are the common substrate of Chapters 4–6 of the thesis and of later finite-horizon policy-search analyses.
The performance difference lemma relates two objects defined in opposite directions of time: the state distribution of runs forward from , while the -values of are defined backward from the horizon. A formal statement must keep the epochs of the two aligned, including the boundary epochs and . The change of measure needs the bound , which holds only because values are normalized and rewards lie in . With unnormalized rewards the constant in front of the ℓ1 term is wrong.
A first idea is to read the hypothesis as "the advantages are small under ". That reading is not available. The hypothesis controls averages under only, and the gap between the two distributions is exactly the penalty term.
Fintype S), so expectations and the ℓ1 distance are finite sums. The thesis also allows infinite state spaces in this chapter, with integrals in place of sums.π t s a together with a validity predicate. Deterministic policies enter as indicator policies .The T-epoch layer (policies, state distributions, values, advantages, the future state-time distribution) is shared with the other missions of this series (namespaces SampleComplexityRL.PolicyGrad and SampleComplexityRL.Mismeasure); the μ-reset objects are defined in SampleComplexityRL.MuPolicySearch; IsTransitionKernel and IsPolicy are published definitions. Contributions of the performance difference lemma and of general facts about the T-epoch layer (values in , sums to one) are welcome.
Let be a connected graph and a set of vertices of even cardinality. A -join is a set of edges in which exactly the vertices of have odd degree. A -cut is a cut with odd. Write for the minimum size of a -join and for the maximum number of pairwise disjoint -cuts. Every -cut meets every -join, so . When equality holds is a central question of combinatorial optimization because of its links to integral multiflows. Seymour (1981) proved equality for all in bipartite graphs. Middendorf and Pfeiffer (1998) showed that deciding equality is NP-complete.
Korach and Penn (1992) proved that a minimum -join with connected components satisfies
So a minimum -join with few components certifies a large packing of -cuts, and a connected one certifies . Sebő and Tannier (Math. Oper. Res. 2004) therefore study the problem MTSC: given , and an integer , is there a minimum -join with at most connected components? They show it can be solved in polynomial time for and is NP-complete in general (their Theorem 5). The hardness proof reduces three-dimensional matching (3DM) to MTSC. This mission formalizes the correctness of that reduction.
Three-dimensional matching. An instance consists of three pairwise disjoint sets , , , each of cardinality , and a set of triples . A matching is a subset in which every element of occurs in exactly one triple.
The graph . Take a further set of points and put , so . The graph has as vertices the points of , the triples of , and one new vertex for every unordered pair of distinct points of . Its edges are:
There are no other edges. In Lean, is gadget q H and is gadgetT q H.
-joins and components. For and a vertex , is the number of edges of at . is a -join (IsTJoin) if is odd exactly for . It is a minimum -join (IsMinTJoin) if no -join of is smaller. The connected components of are those of the graph , where is the set of endpoints of edges of . Their number is numComponents F.
This statement is quantified over every and every , and it is the full mathematical content of the reduction.
The result. The Claim shows that minimizing the number of components of a minimum -join is NP-hard. A Korach–Penn certificate for a large packing of -cuts therefore cannot in general be found by optimizing the component count. This sets the case, which Sebő and Tannier solve in polynomial time through isometric embeddings of tree metrics, apart from the general case.
Formalizing it. The Claim is proved in the paper, in one paragraph. No machine-checked version is known, and the platform has no -join library. The mission produces a reusable vocabulary for -joins, minimum -joins and the components of an edge set, together with a checked proof that a concrete gadget is correct. One sentence of the published argument is false as written (see Difficulty); a formal proof settles the conclusion independently of it.
The direction from a matching to a -join is a direct verification. The converse has to control an arbitrary minimum -join: its size, the shape of each of its components, and how the components meet , and . A first reading of the printed proof suggests that every vertex outside that carries edges of is adjacent to at most one vertex of each of , , . This is false for the inner vertex of a path joining two vertices of the same class, and the construction joins every pair of points of , including pairs inside . Such components really occur in minimum -joins, so the count of components has to cover them as well. The stated conclusion (at least components, with equality only in the matching-like configuration) remains true.
On the Lean side, the components of an edge set are not the components of the graph with that edge set on all vertices: there every untouched vertex would be a component, and the Claim would become false.
Fin q), so their disjointness holds by construction. and are finite sets of triples in Fin q × Fin q × Fin q. IsMatching q M requires each element of each class to be the corresponding coordinate of exactly one triple of , and is a separate hypothesis. A covering-only or at-most-one version would be a different problem.Sym2) and is a Finset of edges of . Parity uses . Minimality is " for all -joins ", never an infimum on .Contributions welcome: proofs of the milestones, general lemmas on -joins (a -join in a graph where is independent has at least edges), and lemmas on the components of an edge set, which are reusable well beyond this mission.
UnrelatedSched.ThreeHalves.ThreeDimMatching (Lenstra–Shmoys–Tardos) encodes 3DM with an indexed family of triples and the covering form of a matching, a different encoding from the paper's set with "exactly one".Binary classification asks for a rule that predicts a label from a feature vector , given labelled examples. A classical way to measure how hard this is, due to Mammen and Tsybakov (1999), treats classification as the estimation of a set, the region where label is more likely, and asks how fast the excess misclassification risk of a data-driven classifier can tend to zero. The answer depends on two parameters: the complexity of the class of candidate sets, measured by entropy with bracketing, and the margin parameter , which measures how sharply the conditional probability of label moves away from near the decision boundary.
Tsybakov (2004) showed that empirical risk minimization over a suitable net attains the rate , which approaches ("fast rates") for favourable margins and simple classes, and that this rate is minimax optimal. In practice neither nor is known. The main result of the paper, Theorem 3, constructs a single classifier that adapts to both and attains the optimal rate up to a logarithmic factor simultaneously over a whole family of classes. The margin condition introduced here, often called the Tsybakov margin (or noise) condition, became a standard assumption of statistical learning theory, used for instance in the analysis of support vector machines and of plug-in rules (Audibert and Tsybakov 2007).
Observations are i.i.d. pairs with law . Write for the law of and for the regression function. A classifier is a Borel set , predicting on . The Bayes classifier is , and the excess risk of is
where . Two pseudodistances between sets are used: and its empirical analogue . The empirical risk is .
A class of sets has complexity bound if its -entropy with bracketing for is at most for . The margin assumption (A1) requires whenever , with . A class of distributions is a -class if every has , satisfies (A1), and has complexity bound (Definition 4).
Aggregation. Given classes with complexities and nested approximating sets , let minimize over . With the thresholds
an index is admissible if, for every , some has . The adaptive classifier is with the smallest admissible index.
Under assumptions (A3)–(A4), with a -class for each , , and , fixed, there is such that for all and every ,
Theorem 3 says that a procedure which knows neither the class containing nor the margin parameter loses at most a factor against the optimal rate on every class at once; combined with the lower bound of Theorem 2 it identifies the optimal adaptive rate up to logarithms. Corollary 1 extends it to a continuum of classes . The selection rule is a Lepski-type pairwise comparison of empirical risks, and the analysis is one of the early results on adaptation to the margin.
The result is proved in the paper, with an Appendix that derives the empirical-process inequalities from van de Geer (2000). No part of it is known to have a machine-checked proof. A formalization would produce reusable infrastructure: entropy with bracketing for classes of sets, ratio-type deviation inequalities for empirical processes, and the excess-risk identity for 0–1 loss.
The obvious argument controls each separately and takes a union bound over . That fails: the bound for at a class that does not contain says nothing about , and the adaptive rule compares classifiers from different classes through random thresholds that depend on the empirical distance . The central steps are to show that the true index is admissible with probability uniformly over a polynomially growing number of classes, and to replace by inside the thresholds at a constant-factor cost. Both rest on exponential, ratio-type deviation bounds for suprema over classes of infinite entropy, which are not in Mathlib.
is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, labels are Bool with true ↔ 1, and a distribution is a pair with a probability measure and measurable with values in ; the law of a pair is the published UnderstandingML.condLaw (, then ). Classifiers are sets, risk is measured by via identity (2), and the complexity bound is stated as "some bracketing with exists".
The Section 3 data (, classes, nets, complexities, distribution classes) are indexed by . The formalization commits to the following readings of the page, all disclosed in the items:
Expectations are Lebesgue integrals over the sample, so each one carries the hypothesis that the data-dependent set is jointly measurable in (sample, point). This rules out the trivializing formalization in which a non-measurable classifier has integral and every rate bound holds for free. Probabilities of events involving suprema over uncountable classes are outer measures. Appendix suprema are real suprema over index sets bounded above. The goal is not vacuous: a solution-folder check exhibits a setup satisfying all hypotheses with .
Contributions welcome: bracketing-entropy chaining bounds, the van de Geer inequalities (5.42)–(5.43), and the Appendix lemmas as standalone results.
Supply disruptions — fires, quality failures, capacity shortfalls at a supplier — are a first-order risk in manufacturing supply chains. A buying firm has two broad responses. It can dual source, splitting orders between suppliers so that one supplier's shortfall is partly covered by the other, or it can invest in process improvement at a single supplier (kaizen events, supplier development programmes) to make that supplier more reliable. Wang, Gilland and Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement? (M&SOM 12(3):489–510, 2010), build a two-stage newsvendor model that captures both levers and compare them analytically.
This mission formalizes the paper's analysis of the improvement lever on its own: the firm commits early to one supplier, decides how much effort to spend improving it, and then orders. The paper's Theorem 3 shows that, without committed costs, this improvement problem is a concave program with an explicit first-order condition, and its Corollary 2 derives how the optimal effort responds to costs, revenue and the chance that improvement succeeds. These are the facts the paper's later comparisons between improvement and dual sourcing rest on.
A firm sells one product over one season at unit revenue , salvage value and unit penalty for unmet demand. Demand has distribution function and finite mean. The firm orders units from a supplier with design capacity , unit cost and committed cost : the firm pays when units are delivered.
The supplier suffers a random capacity loss and delivers . The law of has a continuous distribution function that depends on the supplier's reliability index ; a larger index means a stochastically smaller loss, for . Demand and losses are independent.
With and , the second-stage expected profit at index is
and is its optimal value.
In the first stage the firm may improve the supplier from its initial index . The paper reparametrizes effort by the target index: reaching index needs effort , where is convex and nondecreasing with . Effort costs per unit and succeeds with probability . The first-stage profit of early commitment is Eq. (7):
Assume and that is concave on for every (decreasing marginal reliability improvement). Then is concave on , and an optimal index , with an optimal order at , satisfies
Theorem 3 turns the firm's improvement decision into a one-dimensional concave program, so that the first-order condition (8) characterizes the optimum and comparative statics are available. Corollary 2 is the managerial content: cheaper or more reliable improvement, a cheaper supplier and a more valuable product all justify more improvement effort. The paper's later results — when late commitment beats early commitment (§4.2.2) and when single sourcing with improvement beats dual sourcing (§5) — compare the optimal values these results describe.
The results are proved in the paper's online appendix; none of them has a machine-checked proof. A complete development provides formal proofs of the layer-cake representation of the random-capacity newsvendor profit, of its critical-fractile solution, and of the concavity and envelope arguments on top of it.
is an optimal value, a supremum over order quantities, and suprema of concave functions are not concave in general. The obvious route — " is concave in for each , hence so is the supremum" — fails, because is not concave in for a fixed beyond the critical fractile. Any argument has to control how the optimal order moves with under random capacity, where the delivered quantity is a minimum of the order and a random effective capacity. The first-order condition then requires differentiating an expectation of a non-smooth function of in the parameter of 's law. Corollary 2 must be argued on the set of maximizers, since is concave but not strictly concave.
The Lean development lives in the namespace MitigateSupplyRisk.Improvement. Model bundles , a demand law and the family of loss laws; and are their cdf. Expectations are Bochner integrals over and over the product . Model.Assumptions collects the standing assumptions of §3: , , (implicit in the paper's division by ), a nonnegative integrable demand, nonnegative atomless losses, and the stochastic order in . Demand needs no density. Effort bundles with , and convex, nondecreasing on , ; taking as primitive assumes every index is reachable. is a real supremum and is built from it, never from the critical fractile. Every statement about carries or , which makes the supremum finite. "Optimal" always means a maximizer over the whole feasible set, and "increasing" is weak throughout, as on p. 492 of the paper.
The paper's proofs are in an online appendix that was not used here. Deviations from the page, each disclosed in the item's Formalization Note:
A trivializing formalization is ruled out: is built from the supremum (not from at a fixed order), the supremum is finite under the stated hypotheses, and every expectation is of an integrable function, so no statement holds through a junk value.
Reusable beyond this mission: the random-capacity newsvendor objects (delivered quantity, expected profit, layer-cake representation) and a Topkis-type monotone comparative statics lemma on a chain. Contributions of either, and proofs of the milestones in any order, are welcome.
The Lasso fits a linear model by least-norm regression with an penalty, and its most used property is that it returns sparse coefficient vectors: many features receive weight exactly zero. Most sparsity guarantees for the Lasso are statistical. They assume a generative model and an incoherence or irrepresentability condition on the design, and conclude that the support is recovered (Tropp 2006; Zhao and Yu 2006).
Xu, Caramanis and Mannor (arXiv:0811.1790v1, 2008; IEEE Trans. Inf. Theory 56(7), 2010) show that the Lasso's -regularized regression problem is exactly a robust regression problem in which each feature column is perturbed independently within a norm ball (their Theorem 1; mission 1 of this series). Section IV of the paper uses this robust view to give a sparsity criterion that needs no generative model: a feature gets zero weight if some allowable perturbation makes it irrelevant. This mission formalizes that criterion, Theorem 5, together with the more general Theorem 5′ it specializes, and the geometric consequence Theorem 6.
Fix integers . The data are the features , the columns of a matrix , and a response . For , . A disturbance perturbs column to .
Given radii , the feature-wise uncoupled uncertainty set is
For a set of disturbances, the robust objective is
and the robust regression problem is . It has a solution supported on if some minimizer has for all .
For a disturbance , agrees with on the features in and is zero elsewhere, and . Given numbers for , the enlarged set of Theorem 5′ is
In Lean these are uncertaintySet c, restrictedSet c I, enlargedSet c l I, robustObjective a b V x, IsRobustSolution and HasSolutionSupportedOn, all in the namespace RobustRegLasso.Sparsity.
If there is a disturbance that is zero on the features in and such that
has a solution supported on , then has a solution supported on .
Theorem 5 is Theorem 5′ applied to the perturbed matrix with radii off , and .
The result separates sparsity from statistics. Theorem 5 asks only that the features outside can be made irrelevant by a perturbation within the uncertainty budget; it involves no noise model and no probability. Theorem 6 turns this into an incoherence-type condition: features that lie within of being orthogonal to the response and to the relevant features receive zero weight. Because the robust problem over is the -regularized regression (Theorem 1), these are sparsity statements about that Lasso-type problem. The same argument gives the paper's further results on angular separation and nearly dependent features, which it defers to a companion report.
These results are proved in the paper; none of them has a machine-checked proof on Prove2Me or, to our knowledge, elsewhere. The mission formalizes the known proof. It also records a correction: Theorem 6 as printed claims that every optimal solution vanishes off , which is false (a two-dimensional counterexample is in the milestone's statement); the proof gives existence of one such solution, and that is what is posed.
The proof of Theorem 5′ is short, and the work is in the bookkeeping. The obvious attempt treats "max" as a real supremum and compares values directly; it has to know that each uncertainty set is nonempty and that the residual is bounded on it, and the enlarged set is nonempty only because . The two equalities of the first display require reassigning the columns outside of a disturbance (to zero, or to a feasible value) without changing the residual at , which works only because there. The specialization of Theorem 5′ to Theorem 5 changes the radius vector and the base matrix at the same time, and needs to coincide with the feature-wise set whose radii are on and off it. Theorem 6 additionally needs the equivalence of the robust problem with an -regularized problem, an orthogonal projection onto a span, and the existence of a minimizer of a coercive (or, for , least-squares) objective.
a : Fin m → EuclideanSpace ℝ (Fin n); a disturbance is δ : Fin m → EuclideanSpace ℝ (Fin n); is the family a + δ. Index sets are Finset (Fin m) (0-based). The loss is the norm, as stated in the paper (which remarks that any norm works).EReal (⨆ δ ∈ V). With nonnegative radii every set used is nonempty and bounded, so the value is a finite, attained real number; no junk value of a real sSup can make a statement vacuous. "Optimal solution" means a minimizer of this objective over all of ; existence of a minimizer is assumed where the paper assumes it (Theorem 5′) and concluded where the paper concludes it (Theorems 5, 6).Firms that buy from unreliable suppliers face two broad remedies: spread orders across several suppliers (dual sourcing), or invest in making a supplier more reliable (process improvement). Wang, Gilland and Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement? (M&SOM 12(3):489–510, 2010), compare the two in a single newsvendor model in which suppliers deliver less than ordered because of random capacity losses. This mission covers the first half of that comparison: the pure dual-sourcing strategy, in which the firm improves nobody and only chooses how much to order from each of two suppliers.
A single-supplier random-capacity model was studied by Ciarallo, Akella and Morton (Management Science 40(3), 1994); in that model, as the paper notes, the firm never orders more than demand to hedge against capacity shortfall. Dada, Petruzzi and Schwarz (M&SOM 9(1), 2007) studied several unreliable suppliers but gave only necessary conditions for optimal orders. The paper states necessary and sufficient conditions for two suppliers (its Theorem 1) and, for deterministic demand, a closed-form optimal order in each of six demand regions (Theorem 2). Its proofs are in an online appendix.
A product sells at unit revenue , is salvaged at , and unmet demand costs per unit, with . Two suppliers have unit cost , committed-cost fraction and design capacity . Supplier suffers a random capacity loss whose continuous distribution function depends on a reliability index : a larger index makes the loss stochastically smaller, for . The losses are independent of each other and of demand , which has distribution function .
For an order vector , supplier delivers and is paid . The realized profit is
and the second-stage expected profit is . With and this is the paper's Eq. (3). The optimal value is , and an optimal procurement vector is a attaining it.
Let demand be deterministic, , let , let , let each be strictly increasing on a support with , and let . With , , and , an optimal vector is
In – the firm orders more in total than demand: the quantity hedge.
Theorem 2 is the paper's explicit description of how a buyer splits orders between two unreliable suppliers: single sourcing when capacity is ample, dual sourcing at total order equal to demand, then deliberate over-ordering, and finally ordering full capacity. The quantity hedge is the paper's main qualitative finding for dual sourcing, since, as the paper notes, over-ordering of this kind does not occur with one random-capacity supplier. Corollary 1 says how this hedge responds to reliability, which is the comparison with process improvement that the rest of the paper builds on; Lemma 2(b) is the value of reliability used there.
None of these results has a machine-checked proof, and the paper's proofs are in an online appendix not used here. A formalization would also settle the printed statement, which contains a slip (below) that a formal proof must avoid.
is submodular but not jointly concave in , so the usual route (concavity plus first-order conditions) is not available, and the paper invokes unimodality instead. Under deterministic demand is not differentiable on the line , where the and optima sit, so Theorem 1 cannot simply be specialized to Theorem 2: optimality there needs one-sided arguments. In every region the claim is global optimality over all , including orders above the design capacities, and the feasible set is unbounded.
Suppliers are indexed by Fin 2 (index 0 is supplier 1). The capacity losses are a family of probability measures on without atoms and with , and is their distribution function. is the Bochner integral of against for a demand law . Every theorem assumes is a probability measure on with finite mean. Deterministic demand is . Theorem 1 and Eq. (6) add Lebesgue (the paper's density). "Optimal" means a global maximizer over , and "increasing" is weak, as the paper declares. Added standing hypotheses: , , and , which bound above so that is a genuine supremum. is the generalized inverse .
Corrections to the printed Theorem 2, each disclosed in its item:
Theorem 1's "" is read as . Lemma 2(a) is not formalized: optimal orders are not unique and no reading of " is increasing" was found that is both faithful and safely true.
Stating Theorem 2 as " satisfies the first-order conditions", or optimality only within a region's face, would trivialize it; the statement requires for every . Proofs need integrals of piecewise-linear functions of independent variables, differentiation under the integral sign, and facts about generalized inverses of continuous distribution functions. Lemma 1 and the generalized-inverse facts are reusable beyond this mission; proofs of any milestone are welcome.
In a linearly parameterized bandit a decision maker repeatedly chooses an arm from a set and observes a noisy reward whose mean is linear in an unknown vector . The model covers problems in which many arms share a few underlying features: products described by a handful of characteristics, prices, or routes whose costs depend on a few parameters. Because the arms are correlated through , a good policy can learn about every arm from the rewards of any arm, and its regret can be made to depend on the dimension instead of on the number of arms, which may be infinite.
Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, published in Mathematics of Operations Research, 2010) prove an lower bound on the regret when the arms form the unit sphere, give a matching phase-based policy for strongly convex arm sets, and propose the Uncertainty Ellipsoid (UE) policy for arbitrary compact arm sets. The UE policy is close to the algorithms of Auer (2002) and Dani, Hayes and Kakade (2008), with two differences: it does not need to know the horizon , and it allows and the noise to be unbounded. This mission formalizes its regret bound for general compact arm sets, Theorem 4.1 of the paper.
Fix and a compact set of arms , with the Euclidean norm . Playing arm in period yields
where the noises are independent of each other and of , identically distributed in for each arm, and have mean zero. A policy chooses the arm of period as a function of the history . The regret given and the Bayes risk are
Assumption 1 (p. 13) fixes constants such that, for every : (a) for every arm and every ; (b) every arm has , and contains linearly independent arms with .
The UE policy keeps the ordinary least squares estimate , where , and, with and , the uncertainty radius
It plays in the first periods and then, in each period , an arm maximizing over , with ties broken arbitrarily.
There are constants depending only on such that for every , every compact arm set satisfying Assumption 1, every run of the UE policy, all and all ,
The constants are not fixed: any positive values that work suffice.
The proof in Appendix B proceeds through large deviation inequalities for adaptive least squares (Theorem B.1 for finitely many arms; Lemmas B.3, B.4, B.5 leading to Theorem B.2 for infinitely many), the radius bound (Lemma B.6), the instantaneous regret bound (Lemma B.7), the regret decomposition
(Lemma B.8), and the deterministic Lemmas B.9–B.11, which bound by the value of an optimization problem and that value by .
Theorem 4.1 shows that one policy achieves regret within a factor of the lower bound for every compact arm set, finite or infinite, with sub-Gaussian unbounded noise and without knowledge of . The dependence on the problem is only through and the three constants of Assumption 1; the number of arms does not appear. The large deviation inequalities of Appendix B.1 are also the input of the paper's Theorem 4.2 for finitely many arms.
The result is proved on paper; no machine-checked proof of it is known. A formal development would produce reusable components that are currently absent from Mathlib: a Chernoff-type bound for least squares estimates built from adaptively chosen regressors, the self-normalized inequality of De la Peña, Klass and Lai in the form of Lemma B.3, the determinant recursion behind Lemma B.9, and the law of a bandit history driven by a policy and an arm-dependent noise kernel.
The arms depend on past noise, so with is not a sum of independent terms with fixed weights, and the classical Chernoff bound does not apply. For finitely many arms a union bound over the possible pull counts suffices (Theorem B.1), but its bound grows like and is useless for infinite arm sets. Theorem B.2 instead needs a self-normalized martingale inequality and a covering argument over directions to compare with in the Loewner order. A second difficulty is that the sum of the radii played is not bounded term by term: each term can be as large as , and only the multiplicative recursion of Lemma B.9 shows that large terms are rare.
is EuclideanSpace ℝ (Fin r), so norms are Euclidean. The constants are written ubar, lam0. Policies are deterministic, history-dependent and measurable (measurability is implicit in the paper). The noise is a Markov kernel giving the law of for each arm; the history given is built period by period with fresh independent noise, which is the law of the paper's history. Assumption 1(a) is a bound on a lower Lebesgue integral, so it also asserts finiteness; is . The standing assumptions of Sec. 1.1 (compact , , independent mean-zero noise identically distributed in ) are hypotheses. equals for an infinite arm set. A UE run is any measurable policy that plays first and then a maximizer of after every history that starts with ; on those histories is a genuine inverse.
Deviations from the page, all disclosed in the items: Lemma B.4 is printed for but its proof needs , and at the printed claim fails; it is stated for . Lemmas B.4 and B.5 are printed without "" and are stated for each fixed , the form in which the paper uses them. Lemmas B.9 and B.10 ("with probability one") are stated for every arm sequence that starts with and stays in the ball of radius , which is stronger. Theorem B.1 carries the hypothesis that is finite.
The regret is minus the expected total reward, whose integrand is bounded, so it is never a junk value; the risk bound asserts integrability of the regret in and assumes . The constants are chosen before , the arm set and the instance, so a formalization in which they depend on or on does not prove the goal.
Welcome contributions include proofs of any milestone, in particular the deterministic Lemmas B.9–B.11, and reusable lemmas on matrix determinants, self-normalized bounds and bandit history measures. The source is arXiv:0812.3465v2; its printed page numbers equal the PDF page numbers.
A set of vertices of a graph is a metric generator when every vertex is determined by its vector of distances to the elements of . The minimum size of such a set is the metric dimension, studied in graph theory since the 1970s and surveyed by Chartrand, Eroh, Johnson and Oellermann (Discrete Appl. Math. 2000). Metric generators also appear in combinatorial search, where identifying a vertex from distance queries is the same as weighing false coins.
Sebő and Tannier (Math. Oper. Res. 2004) ask a converse question. Suppose an isometric copy of is already placed inside a second graph . When does that placement extend to an isometric embedding of the whole graph into ? With the question contains clique detection and is NP-hard (p. 385), so the interest lies in hypotheses on that make it tractable. The paper's answer, Theorem 4, is the tool behind its main application: deciding whether a graph has a connected minimum -join (§3.2), a question raised by Frank (1996).
All graphs are finite, simple, undirected and connected. For a graph , is the number of edges of a shortest path between and .
In Lean these are IsMetricGenerator, IsStrongMetricGenerator, IsIsometry, IsIsometryOn, Extends, Represents, candSet, cand and cStar in the namespace MetricGenerators.IsometryExt.
Let be a strong metric generator of with a forest, and an isometry. Then
and if exists, is a representation with for every representation , so it is the unique inclusionwise maximal one.
A further theorem states the criterion behind Corollary 1 (p. 389): an extension exists iff every is nonempty.
Theorem 4 turns a global question (does an isometric embedding with prescribed values on exist?) into a local one about adjacencies among candidate sets, and the procedure settles it in at most rounds. In §3.2 of the paper the theorem is applied to a tree with its set of leaves (all but one leaf forms a strong metric generator, Theorem 3), and this yields the characterization and polynomial-time recognition of graphs with a connected minimum -join. Without the forest hypothesis the characterization fails: Figure 2 of the paper gives a representation, with a triangle in , for which no extension exists.
The result is proved in the paper. To our knowledge none of it has a machine-checked proof: Mathlib has graph distances (SimpleGraph.dist), acyclicity and induced subgraphs, but no metric generators, no isometry-extension results and no metric dimension. A formal proof would provide that vocabulary and a verified decision criterion. It would also be the first step towards formalizing the -join application of the same paper.
The necessity half and the maximality of are bookkeeping. The difficulty is sufficiency: from a representation one must build an actual isometry. The obvious idea is to pick any for every , but this fails: two independently chosen candidates for adjacent vertices need not be adjacent, and condition (ii) only guarantees some adjacent partner. The choices must be coordinated along . Even with coordinated choices, the distance between images must be bounded above along every shortest path of , including paths that leave one component of , pass through , and return. Figure 2 shows that without the forest hypothesis no such choice need exist. Lemma 1 supplies the matching lower bound, and its proof needs the strong generator property, not just the metric-generator property.
Fintypes; graphs are SimpleGraphs, and both and are assumed Connected in every statement. SimpleGraph.dist is -valued and equals on unreachable pairs, so connectivity is load-bearing.Finset of vertices of ; is a function on the subtype of , so it has no values outside .H.induce (↑T)ᶜ, and "forest" is IsAcyclic. is allowed.Sets; the recursion follows the page's union form, and is the stage .Represents. Without it the empty family would represent every and the right-hand side of the goal would be trivially true. "Unique inclusionwise maximal" is stated as "a representation containing every representation".sInf.Reusable infrastructure: metric generators and strong metric generators of graphs, isometries between graph metrics, and lemmas relating SimpleGraph.dist to shortest paths through a vertex. Contributions are welcome on any milestone and on general SimpleGraph.dist lemmas they need.
Barabási and Albert (Science 1999) proposed preferential attachment as a mechanism behind the heavy-tailed degree distributions observed in the web graph and other networks: vertices arrive one at a time and attach to existing vertices with probability proportional to their degree. Empirical work on such networks reported that typical distances are very small compared with their size. The original description left the model underdetermined (the joint law of the edges of a new vertex was not specified), so its distances could not be analysed as stated.
Bollobás and Riordan (Combinatorica 2004) fixed a precise version of the model, the LCD model, and determined its diameter: for edges per vertex it is asymptotically . For the graph is a forest (with loops), and a result of Pittel states essentially that its diameter is of order . Together with the degree-sequence analysis of Bollobás, Riordan, Spencer and Tusnády (Random Struct. Alg. 2001), the paper is one of the first rigorous results on a scale-free random graph model.
The process . Vertices are . Vertex sends a single edge to a vertex , chosen given the past with
where is the degree of in the graph built so far (a loop counts twice). Loops () are allowed.
The graph . Run and identify the vertices into a single vertex , for . The resulting random graph on is . The paper's graph has loops and multiple edges; its diameter is the largest graph distance between two vertices of the underlying simple graph.
Almost every. For fixed , a.e. has a property if its probability tends to as . All logarithms are natural.
The endpoint model (for the upper bound). Let be independent with density on (), their sorted values, , , . Given , the random graph joins each vertex to and , independent with for . The events (Lemma 7) say that the follow the profile and that the spacings are neither too small nor too large in specified ranges.
For fixed and , a.e. is connected and
The theorem shows that the diameter of this scale-free graph is smaller by a factor than that of a classical random graph with the same constant average degree, and identifies versus as the dividing line. It made the "small world" claims about the Barabási–Albert model precise for one exact version of it, and the LCD representation and the endpoint model introduced here were used in later work on preferential attachment.
The result is proved in the paper; nothing here is open. The work of the mission is formalizing the known proof. As far as is known, no machine-checked development of preferential-attachment graphs exists in Mathlib or elsewhere. A complete development would supply a reusable probability space for the attachment process, a Chernoff–Janson inequality for heterogeneous Bernoulli sums, a negative-correlation lemma for the process, and order-statistic estimates for i.i.d. samples, each of independent use.
The lower bound is a first-moment count of short paths, but the edges of are not independent: an earlier edge into a vertex raises the chance of later ones. Lemmas 2–4 show that small subgraphs still appear with probability comparable to an independent model with edge probabilities ; Lemma 3 requires a description of the process in which the needed independence is visible.
The upper bound is the hard half. A naive breadth-first expansion from a vertex fails: the weight of the next neighbourhood has the right mean but a very skewed distribution, and vertices near the end of the ordering have few early neighbours. The paper replaces the process by a conditionally independent model given the sorted endpoints , controls the globally (Lemma 7), handles late vertices separately (Lemmas 8–10), and runs a weighted expansion with a growing blow-up factor (Lemmas 11–12). Each step needs uniformity in : every must depend on only.
Vertices are stored as Fin N (0-based) and statements read 1-based labels through the accessors tgt and lab. A sequence is a dependent function (t : Fin N) → Fin (t+1), its probability is the product of the exact conditional factors , and probabilities are finite weighted sums. , and are Mathlib simple graphs: loops and multiple edges are dropped, which does not change connectivity or distances. The model is the paper's: not uniform attachment, not independent choices per vertex, and with the self-loop term.
in the goal is SimpleGraph.diam, which is on a disconnected graph; the goal therefore keeps connectivity explicit, as the page does. Every other diameter bound uses "every two vertices are joined by a walk of length ", and lower bounds use its negation, so a disconnected graph never satisfies an upper bound by default. Hidden constants follow the paper's quantifier order: the constants of Lemmas 2 and 4 come before every index; each of §§7–8 is a function chosen before (a bound chosen after would make these statements nearly empty); "for sufficiently large" is before or . Theorem 5 assumes the bound of Lemma 4 for its constant . Every statement about assumes . Lemma 7 is stated as "the probability of the complement tends to " under the product law of ; the coupling is stated as the equivalent stochastic-domination inequality for every property preserved under adding edges.
Not formalized: Lemma 9 (a conditional bound given the history of a breadth-first exploration), the LCD representation of (§2), and Theorem 13 (), which the paper states without proof.
Contributions welcome: proofs of any milestone, the identity with , the LCD representation, and general lemmas about the attachment process and Bernoulli tails.
Conic quadratic optimization — linear optimization over products of quadratic (second-order, Lorentz) cones — covers robust linear programming, portfolio problems with risk constraints, norm minimization and many engineering design problems. Andersen, Roos and Terlaky describe the primal-dual interior-point method implemented in the MOSEK optimizer for this problem class (Math. Program. 95 (2003)). Their algorithm does not solve the primal and dual problems directly. It solves the homogeneous model, an embedding that has a solution whether or not the original problem is feasible, and from which either an optimal pair or a certificate of infeasibility is read off.
The convergence argument of such a method rests on one algebraic property of its search direction: a step along the Newton direction reduces the infeasibility of the homogeneous model and its complementarity gap at the same rate. For linear programming this is classical (Xu, Hung and Ye, 1996; Andersen and Andersen, 2000). This mission formalizes the conic quadratic version, Lemma 4.1 of the paper, in which the diagonal complementarity products of linear programming are replaced by arrow-head matrices.
The cone is a product . Each factor is one of three kinds:
Vectors are partitioned by cones, , and . To each cone is attached a symmetric orthogonal matrix : the identity for and , and for the identity with its leading block replaced by . For the arrow-head matrix is
At a point put , , and let , , be block diagonal with blocks , , . Let be the first unit vector of and .
The data are , , . A current point is , with
For a centering parameter the Newton direction solves the linear system (22):
The new point is for a step size (23).
Under (22) and (23),
Lemma 4.1 is what makes the homogeneous algorithm analyzable. Because the three residuals and the gap shrink by the same factor , their ratios are invariant along the iterates, and a step with and makes measurable progress toward a solution of the homogeneous model. The paper notes (p. 14) that all properties stated in Lemma 4.1 hold for the Nesterov–Todd-scaled direction (27) as well, the direction actually implemented, for which polynomial complexity is shown by Monteiro and Tsuchiya (2000).
The result is proved on the page; it is not open. As far as the platform's catalogue shows, it has not been formalized. Machine-checked versions exist only for linear-programming analogues, with diagonal complementarity products in place of arrow-head matrices. The formalization adds two things. First, it fixes three printed slips: the third line of (22) prints for ; the fourth identity of (24) prints ; and the proof's evaluation on p. 14 ends with where is correct, since and the equation contributes the extra . Second, the arrow-head identities (61) and the p. 14 equality are reusable for missions on the complementarity conditions (Lemma 3.1) and the scaled directions of the same paper.
The first three identities of (24) are linear and follow from the first three lines of (22) alone. The content is in the last two. They need an inner-product identity that turns the fourth line of (22), a statement about arrow-head matrix products, into a statement about the scalar quantity . The naive reading treats as an abstract linear image of and loses exactly this link. What is needed is that the first row of is , that has first entry , and that every is symmetric and orthogonal. The last fails for the rotated cone when , so the dimension conventions are not decoration. The bookkeeping constant must also be tracked correctly; the page itself gets it wrong.
Fin k; block is Fin (n i) → ℝ, and indices are 0-based (the paper's is v 0). is given by its column blocks , so , and . The second line of (22) and of (24), and the fourth line of (22), are stated block by block; this is equivalent because , , are block diagonal.ConicQuadIPM.Complementarity.Setting provides the cone kinds, (Tmat), (arrow), (e1) and the predicate WellFormed; this mission's ConicQuadIPM.NewtonStep.Setting adds (mu0) and the system (22) (NewtonSystem). WellFormed is the paper's implicit dimension convention (, , for the three kinds).WellFormed. This is a disclosed addition: the paper never states the dimensions, and without them a block of dimension breaks . The ranges and are kept as on the page, although the identities hold for all real values. No interiority or cone membership of the current point is assumed, because Lemma 4.1 does not use any. The of (22)'s third line is .arrow and Tmat. Replacing by an abstract linear map, or by directly, would turn milestone 4 into a definition and empty the goal. Milestone 5 states the corrected constant ; the printed is false whenever and .The Lasso fits a linear model to data by penalizing the norm of the coefficient vector. Xu, Caramanis and Mannor (arXiv:0811.1790) showed that -regularized regression is exactly a robust regression problem: it minimizes the worst-case residual when every feature column may be disturbed within a norm ball. That reading explains Lasso through what it protects against, not through a prior or a sparsity heuristic.
The paper's Section V turns the same identity into a statistical statement. For a fixed coefficient vector , the robust loss on the training data equals a worst-case expected loss: the largest expected squared prediction error over a class of probability distributions built around the samples. One of these distributions is a kernel density estimator of the data, and from this the authors derive the consistency of Lasso using robustness alone. This mission formalizes that bridge, Corollary 3 of the paper, together with the steps of its proof in Appendix D.
The same authors later generalized the underlying equivalence (Proposition 1 here) to weighted, possibly overlapping uncertainty sets in A distributional interpretation of robust optimization (Math. Oper. Res. 2012).
There are samples and features. The data are a response vector and an observation matrix ; its -th row is the feature vector of sample . A coefficient vector is , and is a fixed budget (the paper writes because its later consistency argument lets it depend on ). Norms are and .
A pair , with and with columns , is admissible if and for every column . Each admissible pair defines one box per sample,
a rectangle around the observed pair in the joint response–feature space. The box-constrained class is the set of Borel probability measures on such that
The empirical distribution of the samples belongs to it, and so does any distribution that spreads the mass of each sample over its box. Finally is the union of these classes over all admissible .
The equation holds for every data set: there is no assumption on how was generated (Remark 1 of the paper).
The remaining step of the proof applies Proposition 1 of the paper: for Borel sets , . Its general weighted form is already posed on the platform as DistInterpRO.Equivalence.theorem_2_1 (inf form, weights summing to one; take and ), and the one-set case (Lemma 2) as DistInterpRO.Equivalence.corollary_2_1. They are credited here and not posed again.
The result. Corollary 3 gives Lasso a distributional reading: minimizing is, up to the additive constant , minimizing the worst-case root mean squared error over all distributions that stay, sample by sample, inside boxes of controlled size around the data. Because a box kernel density estimator lies in , the paper's Theorem 7 derives the consistency of Lasso from this identity when suitably. Without the corollary that argument has no starting point.
Formalizing it. The result is proved in the paper but has no machine-checked proof. A formal development yields three reusable pieces: the robust-regression identity with a perturbed response, the decomposition of a worst case over a product of boxes into per-sample worst cases, and the finite-dimensional instance of Proposition 1 with uniform weights. Together they are the deterministic half of a formal consistency proof for Lasso.
The left-hand side of (8) is a worst case over perturbations of the data; the right-hand side is a worst case over probability measures. Bounding the right-hand side above requires controlling for every in the class, and the constraint on is not that each box receives mass : the boxes may overlap, and a measure may concentrate mass on intersections. The natural argument of moving each sample's mass to the worst point of its box therefore does not apply to a general member of the class. A second, smaller difficulty is the order of the suprema: is a union over , and the square root must be exchanged with a supremum over measures.
Fin (m+1) → ℝ with its product (= Borel) σ-algebra, response first: , . This matches the boxes; the paper's ordering is notation only. is a Matrix (Fin n) (Fin m) ℝ, indices are Fin n, Fin m.IsLUB), with no claim that it is attained. The integral is the Lebesgue integral of the nonnegative integrand with values in , never a Bochner integral. The "max" of the first display is an attained maximum (IsGreatest). The equalities of suprema in the second and third displays are stated as "the same real number is the least upper bound of each set". The inner supremum over a nonempty compact box is encoded as the greatest value of the loss on it.sSup with a junk value and no Bochner integral that could silently vanish appear in any statement. The class keeps the constraint for every , including , which forces each measure onto ; dropping it would make the supremum infinite.DistInterpRO.Equivalence.theorem_2_1 is reusable well beyond this mission. Proofs of either milestone, of the uniform-weight Proposition 1 for boxes, and of the goal are all welcome.Many problems in system identification, collaborative filtering, low-dimensional embedding and model reduction ask for the matrix of least rank in an affine space. Affine rank minimization — given a linear map and , find a matrix of minimum rank with — is NP-hard in general. Recht, Fazel and Parrilo (arXiv:0706.4138; SIAM Review 52(3), 2010, doi:10.1137/070697835) showed that the convex relaxation which minimizes the nuclear norm (the sum of the singular values) instead of the rank recovers the minimum-rank solution exactly whenever satisfies a restricted isometry property on low-rank matrices. That deterministic theorem is the subject of the companion mission in this series.
A deterministic condition is only useful if maps satisfying it exist and are common. This mission formalizes the paper's second main result: random linear maps from a broad class — including Gaussian, symmetric Bernoulli and sparse random matrices — satisfy the restricted isometry property with overwhelming probability once the number of measurements is of order . This parallels the role of random matrices in compressed sensing (Candès–Tao 2005; Baraniuk, Davenport, DeVore and Wakin 2008), where the vector restricted isometry property is established for random measurement matrices by a concentration and covering argument.
Write for the trace inner product on and for the Frobenius norm. A linear map is given by measurement matrices through ; is the Euclidean norm in , and is the operator norm.
The -restricted isometry constant (Definition 3.1) is the smallest such that
A random linear map is nearly isometrically distributed (Definition 4.1) if for every , ; for every and ,
and for some and all , .
For subspaces of a Euclidean space, the projection distance is , the operator norm of the difference of the orthogonal projections (4.10). For subspaces , , the subspace consists of the matrices whose column space lies in and whose row space lies in .
Fix . There are depending only on such that for all with , all , and every nearly isometric random map ,
The theorem supplies the hypothesis of the paper's recovery theorem for random measurements: with and rank , it shows that random linear measurements suffice for nuclear norm minimization to recover every matrix of rank at most exactly. Since a rank- matrix has degrees of freedom, this is within a logarithmic factor of the information-theoretic count. The result made the nuclear norm heuristic a guaranteed method and seeded the theory of low-rank matrix recovery, including matrix completion.
The result is proved in the paper, though Lemma 4.5 rests on Szarek's covering estimates for the Grassmannian, cited without proof. To the best of the curators' search of the platform, none of these statements is machine-checked: there is no formal treatment of the matrix restricted isometry property, of nets on Grassmannians in the projection metric, or of nearly isometric random maps. A formalization would supply the probabilistic half of a fully verified low-rank recovery guarantee, together with reusable pieces — the projection distance, the stability of near isometry under subspace perturbation, and a covering bound for Grassmannians.
The set of matrices of rank at most is not a subspace, so concentration for one matrix and a union bound over a single net in do not suffice: a net of the unit ball of all matrices has size exponential in , which would require of order . The set must instead be covered by finitely many -dimensional subspaces, which requires a quantitative covering of the Grassmannians and in the projection distance — the content of Lemma 4.5, whose source in the literature (Szarek) does not give the constant explicitly. A second subtlety is that the event " is a near-isometry on all of a subspace" involves an uncountable family of matrices, and the bound for the supremum of over a unit sphere has to be controlled from the finitely many points of a net.
All statements live in the namespace MinRankRecovery.RandomRIP. Matrices are Matrix (Fin m) (Fin n) ℝ; the Frobenius norm and the trace inner product come from the published module HighDimStat_MatrixRank_Core. A linear map is represented by its measurement matrices Xs : Fin p → Matrix (Fin m) (Fin n) ℝ, which loses no generality. A random map is Xs : Ω → Fin p → Matrix … on a probability space (Ω, μ), with measurable entries.
Conventions committed to:
EuclideanSpace ℝ (Fin m × Fin n), which carries the Frobenius inner product. Lemma 4.4 is stated on EuclideanSpace ℝ ι for any finite index type.Real.log is the natural logarithm.Two printed statements are corrected. Theorem 4.2 assumes : at , and a two-point random scalar map is nearly isometric while violating the conclusion. Lemma 4.5 is posed for , since for large the right side drops below .
The constants of the goal are quantified before the dimensions, the distribution and ; a formalization in which they may depend on or on the distribution, or in which the near-isometry hypothesis is unsatisfiable, would be trivial and is ruled out by these choices.
A complete development needs: orthogonal projections and operator norms on finite-dimensional inner product spaces (Mathlib), volumetric -nets of spheres in subspaces, covering bounds for real Grassmannians in the projection metric, and the measure-theoretic union bound. The Grassmannian covering bound and the stability lemma are reusable beyond this mission. Contributions of any milestone, including Lemma 4.5 on its own, are welcome.
The Lasso (Tibshirani 1996; Chen, Donoho and Saunders 1998) fits a linear model by penalizing the ℓ¹ norm of the coefficients. It is one of the standard tools of high-dimensional statistics and signal processing, and its usual justification is statistical or geometric: the ℓ¹ penalty is a convex surrogate for sparsity, or the negative log-density of a Laplace prior. Xu, Caramanis and Mannor (arXiv:0811.1790v1, 2008; IEEE Trans. Inf. Theory 56(7), 2010) give a different justification: an ℓ¹-regularized regression is exactly a robust regression, the problem of fitting the data well in the worst case when every feature of the observation matrix may be corrupted by a bounded disturbance.
This observation is the foundation of the rest of their paper (dual-norm regularizers from coupled disturbances, sparsity from robustness, consistency of the Lasso through a worst-case-expectation reading). It also connects two literatures. On the robust side, El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) computed the worst-case residual when the whole data matrix is disturbed in a Frobenius-norm ball, obtaining ; that result is already on the platform as RobustLS.Unstructured.worst_case_residual_closed_form. On the distributional side, Blanchet, Kang and Murthy (J. Appl. Probab. 56(3), 2019) obtained the square-root Lasso as a Wasserstein distributionally robust problem (RWPI.SqrtLasso.theorem_1). The present mission formalizes the feature-wise result that sits between them.
Fix integers (samples) and (features). The observation matrix has columns , the features. The response is and a coefficient vector is , so that . All norms on are Euclidean, .
A disturbance of is a family of vectors , one per column; the disturbed matrix has columns . Given budgets , the feature-wise uncoupled uncertainty set is
Each feature is disturbed independently: no constraint couples the . The robust objective is the worst-case residual
and robust linear regression is problem (1), . The ℓ¹-regularized regression problem is (3), with
The loss in is the norm of the residual, not its square. In the Lean development, is matVec a x, is uncertaintySet c, is robustObjective a b c, is l1RegularizedObjective a b c, and the disturbance of the proof is worstCaseDisturbance c x u.
For and budgets , problem (1) with uncertainty set (2) is equivalent to problem (3): for every ,
No minimizer is asserted to exist; the paper does not claim one.
with the maximum attained.
The result. Theorem 1 turns a min–max problem whose inner maximization is nonconvex into a single convex, second-order-cone-representable problem, and it gives the regularization weights a concrete meaning: is the size of the disturbance feature is protected against. With equal budgets it recovers the Lasso with the unsquared loss, which coincides with the usual Lasso up to a data-dependent change of the regularization coefficient. Every later result of the paper (Theorem 3 for arbitrary norms, the coupled uncertainty sets of Corollary 1, the sparsity theorems of §IV, the kernel-density reading of §V) builds on this identity or its proof pattern.
Formalizing it. The theorem is proved in the paper; the mission formalizes that proof. No machine-checked version of it exists on the platform or, to our knowledge, elsewhere. The definitions here (the uncertainty set, the worst-case objective as a genuine supremum, the explicit worst-case disturbance) are the base on which the companion missions of this series (coupled norms, sparsity, worst-case expectation) restate their own objects.
The upper bound (4) is the triangle inequality. The substance is the lower bound: one must exhibit a single admissible disturbance that makes every column perturbation push the residual in the same direction, and check that it is admissible and that the resulting norm adds up exactly. Two edge cases make the obvious argument fail as written. When the direction is undefined and an arbitrary unit vector must be used instead, which requires ; for the identity reads and is false. When the sign must be , not , for the computation in (5) to go through. Passing from the per- identity to the equivalence of the two minimization problems is then routine, but it must be done without assuming that either problem has a minimizer.
EuclideanSpace ℝ (Fin n); is the family of its columns a : Fin m → EuclideanSpace ℝ (Fin n), and . Indices are Fin m. A disturbance is δ : Fin m → EuclideanSpace ℝ (Fin n), and is matVec (a + δ) x.EReal, so it is on an empty set and on an unbounded one and carries no junk value. That the maximum is attained is stated separately, as IsGreatest of the set of residual norms (milestone 3). "min" in (1) and (3) is read as: the same set of minimizers (IsMinOn … Set.univ) and the same infimum, computed in EReal. No existence of minimizers is claimed.0 < n), which the paper leaves implicit. The budgets are the paper's own assumption on (2).Real.sign, with .sSup with junk value is used, so the identities cannot hold vacuously.EReal order theory are needed. The squared-loss Lasso definitions already on the platform (XuMannorRobust.Lasso.*, LassoDantzig.*) are different objects and are not used. Contributions are welcome on each milestone independently; a proof of the per- identity for an arbitrary norm on would also serve Theorem 3 of the paper.Stochastic programs of the form are rarely solvable exactly, because the expectation is an integral over a large or continuous scenario space. The standard remedy is sample average approximation (SAA), also called the Monte Carlo or sample path method: draw an i.i.d. sample from and minimize the sample average instead. Two-stage linear programs with recourse are the main case in practice. There each is the value of a second-stage linear program, hence piecewise linear and convex, and the scenario distribution is often discrete with an astronomically large but finite support.
Shapiro and Homem-de-Mello (SIAM J. Optim. 11(1), 2000) observed that in this discrete, piecewise linear regime SAA does far better than the usual statistical rate suggests: the SAA problem often returns an exactly optimal solution of the true problem. In their median example, a sample of solves a problem with scenarios exactly with probability about . This mission formalizes the version of that phenomenon that allows the true problem to have many optimal solutions.
Timeline. In 2000, Shapiro and Homem-de-Mello proved almost-sure exactness of SAA under a sharp-minimum condition (Theorem 2.1) and for finite piecewise linear problems with possibly non-unique optima (Theorem 2.3). They then showed that both events fail with exponentially small probability (Theorems 3.1 and 3.2). In 2002, Kleywegt, Shapiro and Homem-de-Mello extended exponential rates to SAA for discrete stochastic optimization. In 2002, Shapiro, Homem-de-Mello and Kim related the exponential constant for convex piecewise linear programs to a conditioning measure of the problem.
Let be the feasible set, a finite set of scenarios with a probability measure , and . The true problem (1.1) and the SAA problem (1.2) are
where is one i.i.d. sequence with law , defined on an auxiliary probability space . Write for the set of optimal solutions of the true problem and for that of the SAA problem. depends on the sample path, and either set may be empty.
The standing assumptions of Theorem 2.3 are:
A subset of a convex set is a face of if is convex and every open segment of that meets lies in . The event of interest is
Under assumptions 1–4 there is with
The constant is not specified; the goal asserts only that the failure probability decays exponentially.
Under the same assumptions, is compact, convex and polyhedral, and with probability one is a nonempty face of for all large enough.
The milestones are the three parts of Lemma 2.4 (p. 6) and the two steps of the proof of Theorem 3.2 (pp. 12–13).
The result explains the observed behaviour of SAA on two-stage linear programs with discrete distributions. For a fixed problem, the sample size needed to recover an optimal face of the true problem with a prescribed probability grows only logarithmically in the inverse failure probability. When the true optimum is not unique, the theorem still gives a structural guarantee: every SAA optimal solution is optimal for the true problem, and every vertex of is a vertex of . Theorem 2.3 is the almost-sure consequence, by Borel–Cantelli.
The results are proved in the paper; none of them has a machine-checked proof that we know of. Formalizing them requires a library of polyhedral convex analysis that Mathlib lacks: the cell decomposition of a piecewise linear function, faces of polyhedra, and finiteness of the set of extreme points. It also requires one-dimensional exponential tail bounds for empirical means of finite-valued variables. The mission makes precise one point the paper leaves implicit. The paper first reduces to the unconstrained case by an exact penalty, and the strict gap recalled on p. 12 holds for the penalized function. For the original the lemma is stated with instead of the printed .
The probabilistic part is routine. Once Lemma 2.4 (c) is available, the event lies in a finite union of events, each a deviation of one real sample mean from its expectation, and each of those decays exponentially. The difficulty is the deterministic Lemma 2.4 (c). Its points must be independent of the sample. The argument that all , and hence every , are affine wherever is affine needs every scenario to have positive mass. Passing from local information near to global optimality of uses convexity on a polyhedral neighbourhood of built from finitely many cells. The natural first idea, uniform convergence of to on a compact set, gives only that approaches , not that , and certainly not that is a face.
EuclideanSpace ℝ (Fin m), and is a Fintype with measurable singletons.ω : ℕ → S → Ω of measurable, independent maps with law ; are its first terms. At the sample average is the junk value .Convex ℝ F ∧ IsExtreme ℝ A F;Set.extremePoints.i.val < ℓ and ℓ ≤ j.val in Fin q.The empty set is a face of every set, and so is itself. therefore carries nonemptiness explicitly, and "face" is not weakened to . Lemma 2.4 (c) also carries the gap : without it, repeating an extreme point among the would make (2.13) unsatisfiable and the lemma empty.
The subdifferential is the published ShorNonsmooth.Subdiff.subdifferential with domain . Contributions are welcome in three areas: polyhedral convex analysis (cells of a piecewise linear convex function, faces and extreme points of polytopes, exact penalties); Hoeffding or Cramér bounds for i.i.d. bounded means; and proofs of the milestones in any order. The polyhedral lemmas are reusable well beyond this mission.
An insurance company whose surplus falls below zero is ruined. The probability of ruin is the classical measure of solvency risk in actuarial mathematics. A company can lower it in two ways: it can invest part of its surplus in a risky asset, and it can pass part of each claim to a reinsurer in exchange for part of the premium. Which mix of investment and reinsurance minimises the probability of ruin is a stochastic control problem. It is studied in risk theory and in applied probability, and it is a model case for control problems with jumps.
Hipp and Plum (2000) solved the problem with investment alone. They wrote down the Hamilton–Jacobi–Bellman (HJB) equation and showed that it has a smooth solution. H. Schmidli (2002) added proportional reinsurance. He proved a verification theorem (his Theorem 1) and an existence theorem (his Theorem 2) for the combined problem. This mission formalizes the existence theorem and the analytic statements it rests on.
Claims arrive as a Poisson process with rate . The claim sizes are independent with distribution function , where and is continuous. The insurer collects premiums at rate . A risky asset follows a geometric Brownian motion with drift and volatility . Under proportional reinsurance with retention level , the insurer pays the fraction of each claim and pays the reinsurer a premium at rate . The function is decreasing and continuous, , , and there is with for and for . In particular, full reinsurance costs more than the premium income.
Write for an unnormalised survival probability, with for . The HJB equation (1) of the problem is
where is the amount invested. Eliminating and substituting turns (1) into the integral equation (5):
Condition (6) at is . In Lean, ReinsPremium, ClaimLaw, tail, den (), SolvesEq5On, H and SolvesHJB (equation (1)) live in the shared module SchmidliRuin.Verif.Setting; HasBoundedDensity, Cond6, SolvesEq3At and SolvesHJBAtZero live in SchmidliRuin.Exist.Setting.
If has a bounded density, then
Lean states this as two conjuncts: existence, and equality on of any two strictly decreasing solutions.
The existence theorem completes the dynamic-programming solution of the problem. By the verification theorem, divided by is the maximal survival probability . The maximisers of the HJB equation define the optimal feedback strategy: the investment and the retention level . Without Theorem 2 the verification theorem would be a statement about a function that might not exist. Equation (5) is also the basis of the paper's numerical scheme (§5), which iterates (5) to compute and the optimal strategies.
Theorem 2 has a published proof. As far as is known, none of the results above has a machine-checked proof, and nothing on Prove2Me states them. The work is to formalize the published argument. This takes the local existence result of Hipp and Plum, which the paper cites rather than reproves, and a continuation argument for a nonlinear Volterra-type equation whose kernel is an infimum over a control parameter. Milestones 6 and 7 are the purely analytic content of the verification theorem that the uniqueness part of Theorem 2 uses. The paper derives milestone 7 stochastically, and an analytic proof is equally welcome.
The denominator vanishes at : , because . The integral in (5) is therefore improper at the origin. A Picard iteration started from a constant does not work, because it does not control . One needs the exact square-root rate , and Lemma 4 obtains it only through Lemma 3 (no reinsurance near ) and the Hipp–Plum analysis of the reinsurance-free equation. Lemma 4's proof in the paper is a two-line citation, so a solver must formalize that local existence result.
The second difficulty is continuation. A solution can be continued as long as condition (6) holds, and Lemma 5 has to exclude that (6) degenerates at a finite endpoint. There the infimum over interacts with the vanishing of . The paper's argument uses a Gronwall estimate and the shape of around , and the minimiser in need not be unique or continuous.
Model data. are real parameters, all strictly positive. The claim law is a probability measure on , with cdf ν, and continuous. "Bounded density" means has a measurable density with values in . is .
Premium. is a real function, used on . The condition is the lower bound near , which is equivalent. A real-valued excludes the case that the paper allows when .
Conventions.
tail, never by Lean's .IsLUB … 0). Lean's sSup would return on an unbounded family, for example when , and that would make " solves (1)" true by accident.Trivialising readings ruled out.
Infrastructure needed.
ContractingWith).The continuation and closure lemmas (milestones 3–5) are reusable for other HJB equations of risk theory with a jump term. Contributions that state and prove intermediate claims of the paper's proofs are welcome as sub-results.
Deciding whether a system of real polynomial equations, inequations and inequalities has a solution is the basic feasibility question behind nonconvex quadratic programming, polynomial optimization, robustness analysis in control, and combinatorial relaxations. Over the complex numbers, Hilbert's Nullstellensatz turns infeasibility into an algebraic identity whose bounded-degree instances are found by linear algebra. Over the reals this fails: has no real solution, yet is not in the ideal generated by .
The real substitute is the Positivstellensatz of Stengle (Stengle 1974; see Bochnak–Coste–Roy, Real Algebraic Geometry, Theorem 4.4.2): a real polynomial system is infeasible exactly when an identity holds, with built from sums of squares and the inequality constraints, a product of the inequation polynomials and in the ideal of the equations. Parrilo (2003), building on his thesis (2000), observed that once the degrees are bounded, the search for such an identity is a semidefinite program (SDP), because a polynomial is a sum of squares exactly when it has a positive semidefinite Gram matrix. This yields a hierarchy of SDPs that is sound at every level and complete in the limit, and it is the origin of the sum-of-squares (SOS) method used throughout polynomial optimization.
Timeline:
Write for real polynomials in variables. Fix three finite, possibly empty, families: (inequalities), (inequations), (equations). They define the basic semialgebraic set
A cone of is a subset closed under addition and multiplication that contains every square ; is the smallest cone containing , and is the set of sums of squares. is the multiplicative monoid generated by the (with the empty product ), and is the ideal generated by the .
For a degree bound , let be the vector of all monomials of total degree at most ; it has entries. For a real matrix indexed by these monomials, the Gram polynomial is .
The degree- Positivstellensatz SDP : with and , find positive semidefinite matrices over the monomials of degree at most , one for each , and polynomials of degree at most , such that
Its unknowns are finitely many real numbers, the constraint is linear in them, and the matrices are constrained to be positive semidefinite.
The first half says every feasible point is a refutation; the second says the hierarchy is complete once the degree bound is large enough. No bound on is asserted, matching the paper.
Theorem 5.1 is the statement that makes Positivstellensatz certificates computable: it converts an existence theorem of real algebraic geometry into a sequence of convex feasibility problems, each solvable by interior-point methods, and any solution is an exact proof of infeasibility. Lower bounds in polynomial optimization (Example 5.4), the copositivity tests of §7.5, SOS relaxations for MAX-CUT and stable sets, and Lyapunov-function searches in control are all instances of this scheme.
The paper proves only the soundness direction of the Positivstellensatz and cites the converse. A complete formal development therefore contains the first machine-checked statement chain from Stengle's theorem to the SDP hierarchy. To the best of current searches, neither Mathlib nor Prove2Me contains the real Positivstellensatz, the Gram matrix characterization of sums of squares, or the monomial count; Mathlib has sums of squares in rings (IsSumSq), positive semidefinite matrices, and the complex Nullstellensatz.
The soundness half is elementary. Completeness rests on Stengle's Positivstellensatz, whose standard proofs pass through real closed fields, orderings of rings and the Tarski–Seidenberg transfer principle, none of which is available in Mathlib in usable form. A tempting shortcut, proving completeness by reasoning only about -points, does not work: the certificate must be an algebraic identity, and points cannot produce it.
A second, smaller difficulty is degree bookkeeping. Each level of the hierarchy has a fixed shape (the exponent of the and the degree of every multiplier are tied to ), while a certificate supplied by the Positivstellensatz has arbitrary degrees and exponents. A Gram representation also needs a degree bound on every square in a sum of squares, not only on the sum.
MvPolynomial (Fin n) ℝ; are arbitrary natural numbers, including ; the families are indexed by Fin s, Fin t, Fin u. The set (4.4) lives in = Fin n → ℝ.RingPreordering is not used: it excludes , which an infeasible system's cone typically contains.IsSumSq; positive semidefiniteness is Matrix.PosSemidef (symmetric, which is the paper's ); is Submonoid.closure, is Ideal.span.A retailer that carries several substitutable products, such as brands of the same item or sizes of the same garment, must choose stock levels before demand is known. When a product runs out, some of its customers buy another product instead. Inventory models with this demand substitution go back to McGillivray and Silver (1978, INFOR 16(1)) and Parlar and Goyal (1984). When the products are run by different firms, each firm's stock affects the demand its competitors see, and stocking becomes a game. Parlar (1988) proved existence and uniqueness of the equilibrium for two products; Lippman and McCardle (1997) treated a symmetric version of the game with an arbitrary number of firms.
Netessine and Rudi (SSRN 303779, working paper 2002; journal version in Operations Research 51(2), 2003) treat products with a general joint demand distribution and general prices and costs, under both centralized and competitive management. This mission formalizes their analysis of the competitive game (§2.2): the first-order characterization of its Nash equilibria (Proposition 3) and the existence, uniqueness and global stability of the equilibrium (Proposition 4).
There are products, indexed , sold in a single period. Product is stocked at units at unit cost , sold at unit price , and leftovers are salvaged at , with . Write (underage cost) and (overage cost).
The first-choice demand is a random vector with a known continuous joint distribution with positive support. A fraction of the customers who want product and find it out of stock buy product instead, with and for every ; a customer whose second choice is also out of stock is lost. The effective demand for product is
which depends on the other products' stocks but not on .
In the competitive model, firm chooses and earns the expected profit
A best response of firm to is a stock maximizing , and a Nash equilibrium is a stock vector from which no firm gains by deviating.
A Nash equilibrium exists, the equilibria are exactly the nonnegative solutions of the first-order conditions
and if either for all or for all , the equilibrium is unique and globally stable: every sequence of simultaneous best responses started at any nonnegative stock vector converges to .
Proposition 4 makes the competitive equilibrium a well-defined object: a single stock vector, characterized by (10), which can be compared with the centralized optimum (the paper's Proposition 6) and which best-response adjustment reaches from any starting point. Without uniqueness, comparative statements about "the" competitive stocking level would be about an arbitrary selection.
The paper's argument has two gaps that this mission makes explicit. The proof asserts that best responses are single-valued because each profit is concave, and differentiates the best response using a density of ; the bound on the Jacobian is then stated in derivative form. The formal statements replace the derivative bounds by difference (Lipschitz) bounds, which need no differentiability, and state the positivity of the density on which single-valuedness rests. The paper also proves existence by citation to Lippman and McCardle; here existence is part of the goal. No machine-checked proof of these results is known.
The obvious route differentiates the best response implicitly, as the paper does. That requires to have a continuous, positive density at the equilibrium quantile, which is not a consequence of a continuous joint law: is a piecewise-linear function of , and its distribution function may have kinks. A second point is that concavity of alone does not make the best response unique: a demand law whose support has a gap gives a flat stretch and an interval of maximizers. Global stability must hold for every sequence of best responses, not for the iterates of one selected best-response function. Finally, the probabilities in (10) use strict inequalities, and their identification with uses that has no atoms, which needs a measure-theoretic argument about under an absolutely continuous law.
Products are indexed by Fin n (0-based). The model data and the standing assumptions , , and are fields of a structure Model n. a i j is the share of 's unmet demand going to , so uses a j i. The demand law is a probability measure on that is absolutely continuous with respect to Lebesgue measure, gives every coordinate a positive value almost surely, and has integrable coordinates; this is the reading of "a known continuous multivariate demand distribution with positive support". Expectations are Bochner integrals and probabilities are μ.real of events, with the strict and weak inequalities as printed.
The stocks range over , with no upper bound. A best response maximizes over ; a Nash equilibrium is defined by the absence of a profitable deviation, not by (10). Defining equilibria by (10) would make Proposition 3 and half of Proposition 4 true by definition, and is ruled out.
One hypothesis is added beyond the page and disclosed in every statement that uses it: has a Lebesgue density that is strictly positive on the open positive orthant. It is used for single-valued best responses, the slope and contraction bounds, and the goal; the derivative, concavity and Proposition 3 do not use it. In the goal, the second branch of the uniqueness condition, for all , coincides with the standing assumption of §2, so uniqueness always applies within the model; the disjunction is kept as printed. The paper's proof attaches the one-norm bound to the first branch, which is a column-sum condition on ; both branches are true, with the one-norm used for row sums and the infinity-norm for column sums.
A complete development needs: differentiation under the integral sign for piecewise-linear integrands, the absence of atoms of under an absolutely continuous law, quantiles of strictly increasing continuous distribution functions, and the Banach fixed-point theorem on the closed nonnegative orthant (Mathlib's ContractingWith). The first two are reusable for every newsvendor model with substitution. Proofs of the milestones in any order are welcome.
A retailer that carries several substitutable products (brands of the same good, sizes of the same item) faces demands that are linked in two ways: a customer who finds the first-choice product out of stock may buy another one, and the first-choice demands themselves are statistically dependent. Inventory planners routinely assume multivariate normal demand and need to know how the dependence between demands affects what the assortment earns. In the single-product newsvendor and in classical risk-pooling arguments, positive correlation is known to hurt; with substitution it is not obvious, because substitution is itself a form of pooling whose value depends on whether two products run out together.
Netessine and Rudi (SSRN 303779, 2002; journal version in Operations Research 51(2), 2003) settle the question for the centralized model with an arbitrary number of products: under multivariate normal demand, the retailer's expected profit decreases in every demand correlation. The authors note that this effect had been observed numerically by Rajaram and Tang (working paper, UCLA, 1999) and Ernst and Kouvelis (1999) but not proved. They prove the analogous statement for each firm in the competitive model with stocking quantities held fixed.
There are products. Product is stocked in quantity at unit cost , sold at price , and salvaged at value , with . Write (underage cost) and (overage cost). The substitution fraction is the share of the unmet demand for product that switches to product ; and .
The first-choice demand is a random vector . The effective demand of product , after substitution from the other products, is
For one realization, product earns
and a single centralized company owning all products earns . The expected profits are (the paper's equation (1)) and (equation (9), the profit of firm when each product is owned by a separate firm).
In this mission is multivariate normal with mean and positive semidefinite covariance matrix . The correlation of products is . Raising means passing from to where and every other entry, in particular every variance, is unchanged.
A function is supermodular if for the componentwise maximum and minimum, and submodular if is supermodular. A random vector is smaller than in the supermodular order, , if for every supermodular whose expectations exist.
For obtained from by raising one covariance , ,
and, for every maximizer of and every maximizer of over ,
These are the two readings of "stocking quantities held fixed or adjusted optimally".
The result. Proposition 2 says that, under normal demand, positive dependence between substitutable products is costly to the retailer whatever the substitution pattern, the number of products, and the cost parameters, and that re-optimizing the stocking levels cannot undo this. It turns an empirical regularity of numerical studies into a structural statement, and it gives a reason to prefer assortments of products whose demands are less correlated. Proposition 5 gives the same conclusion for each competing firm when stocking quantities are fixed; the paper does not claim it when firms re-optimize, since equilibrium quantities move in ways that need not favour every firm.
Formalizing it. The result is proved in the paper, partly by citation: the comparison of normal laws in the supermodular order is a theorem of Müller and Scarsini that is quoted, not proved, there. No machine-checked version of that comparison is known on the platform: the existing Slepian and Sudakov–Fernique comparisons concern expected suprema and tail probabilities, not expectations of arbitrary supermodular functions. A formal proof of milestone 4 would therefore be reusable well beyond inventory theory, wherever supermodular functionals of Gaussian vectors are compared (portfolio risk, dependence orderings, stop-loss premiums).
The deterministic steps (milestones 1–3) are elementary lattice arguments. The difficulty is milestone 4. The natural route is Gaussian interpolation: connect the two laws through and differentiate in . That argument needs twice differentiable with controlled growth, while the statement must hold for every supermodular that is merely integrable under the two endpoint laws, such as the piecewise-linear profits of this model, and for singular covariance matrices. Passing from smooth to general supermodular functions, without assuming integrability along the interpolation path, is where the work lies. The paper's own route to the "adjusted optimally" clause, a total derivative along a differentiable optimal path, presumes a smoothness of the optimizer that is not available, since the expected profit need not be concave in ; the goal is stated as a comparison of optimal values, which avoids it.
All declarations live in DemandSubstitution.Correlation. Products are indexed by Fin n, 0-based. The model data and the standing assumptions , , , form a structure Model n; and are definitions. The paper's §2 assumption that demand is continuous with positive support is dropped, as the paper drops it: a normal law charges negative demands. is Mathlib's multivariateGaussian on EuclideanSpace ℝ (Fin n), pushed forward to Fin n → ℝ; every statement assumes both covariance matrices positive semidefinite, because Mathlib's construction returns a Dirac mass otherwise. Correlations are encoded through covariances with fixed variances, which is equivalent to raising . "Decreasing" is weak. Expectations are Bochner integrals; the profit integrands are Lipschitz and integrable under every normal law, and this integrability is to be proved, not assumed. Supermodularity and the supermodular order reuse the platform definitions SupermodularOn and SupermodularOrder.
A trivializing formalization is ruled out: the Müller–Scarsini comparison is a milestone theorem, never a hypothesis of the goal or of Proposition 5, and the "adjusted optimally" clause quantifies over every pair of maximizers, not over one chosen optimizer.
Contributions welcome: integrability of Lipschitz functions under multivariateGaussian; Gaussian interpolation for supermodular functions; the supermodular comparison itself, which would be reusable on its own.
Optimal control problems with pointwise bounds on the control, such as
reduce, after eliminating the state, to a quadratic program in with a pointwise upper bound. The primal-dual active set strategy solves such problems by guessing the set where the bound is active, solving one linear system on that guess, and updating the guess from the new primal and dual values. It is used routinely in PDE-constrained optimization because each iteration costs one linear solve and, in practice, very few iterations are needed.
Hintermüller, Ito and Kunisch (SIAM J. Optim. 13 (2002) 865–888; authors' version hal-01660511) showed that this strategy is a semismooth Newton method for a nonsmooth reformulation of the optimality system, built on the notion of slant differentiability of Chen, Nashed and Qi (SIAM J. Numer. Anal. 38 (2000) 1200–1216). In finite dimension this gives local superlinear convergence (missions I–IV of this series). This mission concerns the paper's function-space result, Theorem 4.1: in , under a norm gap on the operator, the method still converges locally superlinearly. Ulbrich (SIAM J. Optim. 13 (2003) 805–841) developed a related semismooth Newton theory for superposition operators in function spaces, which also requires a norm gap.
Let be a finite measure space (the paper takes a bounded domain with Lebesgue measure) and the real Lebesgue spaces, with inner product on . The paper writes for an operator and calligraphic , for active and inactive sets.
Slant differentiability (Definition 1). For Banach spaces , , a map is slantly differentiable in an open set if there is , a slanting function, with
For , the candidate slanting function of the pointwise max is if , if , if (4.1).
The problem. Given and a self-adjoint with
minimize subject to . The solution and its multiplier are the unique solution of
for any fixed . The norm gap hypothesis is
The algorithm. From , set , , and solve
A sequence obeying this rule for every is a run. Superlinear convergence of means and, for every , eventually .
The page reads: "Assume that (H1), (H2) hold and that ψ and f are in L^q(Ω). Then the primal-dual active set strategy or, equivalently, the semismooth Newton method converge superlinearly if ‖y⁰ − y*‖ is sufficiently small and λ⁰ = β(y⁰ − ψ)." The formalized goal is the statement the proof establishes: with , there is such that every run with
converges superlinearly to in . The initialization differs from the printed one; see Formalization scope.
Two companion items accompany the goal: existence of a run from every , and Proposition 4.1(i), the paper's counterexamples showing that fails to be a slanting function from to .
Theorem 4.1 is the infinite-dimensional justification of a method used throughout control-constrained optimal control: it shows that the method converges locally superlinearly for the continuous problem itself, not only for each discretization. Example 1 of the paper shows that distributed control of the Poisson equation, and boundary control with Sobolev embeddings, satisfy (H2). Proposition 4.1 isolates the structural reason: the pointwise max is a Newton-differentiable map only between spaces with a norm gap.
None of these results is known to be machine-checked. A complete development would provide slant differentiability in Banach spaces, the Chen–Nashed–Qi local convergence theorem, the norm-gap differentiability of between Lebesgue spaces, and invertibility of block operators on of a measurable partition. Each of these is reusable for other semismooth Newton analyses in function space.
The obvious argument fails at the max. In finite dimension, is slantly differentiable with because a small perturbation does not change the sign of any nonzero component. In , a perturbation of small norm can flip the sign of on a set of positive measure, and on that set the error is as large as . Proposition 4.1(i) shows that this error is not in for any . Superlinear convergence in therefore needs the argument of the max to be controlled in a stronger norm than the error is measured in, which is what (H2) and provide. A second difficulty is that the two-variable algorithm is not literally a Newton method for a map of alone; it must be identified with the reduced algorithm, and that identification depends on the initialization.
Lp ℝ p μ on an arbitrary finite measure space; is an extended real with 2 < q. The paper's bounded Lipschitz domain is replaced by a finite measure space: the proofs use only , and Mathlib has no notion of Lipschitz boundary.run_exists shows that the runs the goal quantifies over exist.PDASNewton.FunSpace.Setting): slanting functions, superlinear convergence, , property (A) for , system (4.2), one step and runs of the algorithm. These duplicate the finite-dimensional definitions of the other missions of the series in a separate namespace.Proofs of any milestone are welcome, as are reusable lemmas on Lebesgue spaces (Hölder on sets of small measure, multiplication operators, Lax–Milgram on of a measurable subset).
Policy gradient methods search a parameterized family of stochastic policies , , by following the gradient of the policy's performance. They are the standard tool when the state space is too large for tabular dynamic programming and when a compact policy class (a neural network, a linear softmax) is easier to represent than a value function. Every such method rests on one identity: a formula for the gradient of the value with respect to that involves only quantities of the current policy, so that it can be estimated from the policy's own trajectories.
Chapter 4 of S. M. Kakade's PhD thesis, On the Sample Complexity of Reinforcement Learning (University College London, 2003), states this identity in two settings, the -epoch undiscounted setting and the -discounted setting, both in the thesis's normalized convention, in which values lie in . The thesis then uses the formula to analyse how many samples a gradient estimate needs (§4.2.3), and in §5.4.2 rewrites it in terms of advantages to explain why gradient methods can stall far from optimal: the gradient weights advantages by the current policy's state distribution, not by the distribution of an optimal policy.
Timeline:
A finite MDP has a finite state set , a finite nonempty action set , a transition kernel and a deterministic reward .
-epoch case. Epochs are , . A non-stationary policy chooses at epoch in state with probability . Starting from , is the probability of being in at epoch . The normalized -value is
the state-action value is with , and the future state-time distribution on is .
Discounted case. For a stationary policy and , the normalized value, state-action value, advantage and discounted future state distribution are
A parameterized policy is a family (resp. ) of policies indexed by , each entry differentiable in ; is the gradient in .
The statement asserts that is differentiable at the given parameter and that its derivative is the right-hand side. It is the thesis's version of the Sutton–McAllester–Singh–Mansour theorem, and the result the rest of the thesis's discussion of gradient methods builds on.
The result. The gradient formula contains no derivative of the state distribution: the effect of on which states are visited cancels, and the gradient is an expectation over states drawn from the current policy, weighted by a sum over actions. This is what makes Monte Carlo and actor-critic estimators possible, and it is the reason the thesis's sample-size analysis of §4.2.3 has no dependence on the size of the state space. The advantage form makes the limitation equally explicit: a small gradient certifies small advantages only under , while the performance difference lemma (Lemma 5.2.1) shows that closeness to optimal is governed by advantages under . That gap motivates the conservative policy iteration of Chapter 7.
Formalizing it. The theorems are proved in the thesis and in the cited literature; none of them is machine-checked in this normalized convention. The platform has a proved finite-horizon policy gradient theorem for a scalar parameter, a stationary policy and unnormalized values (policy_gradient_discounted_finite, policy_gradient_finite_horizon), and a posed direct-parameterization gradient for Agarwal et al.'s unnormalized discounted value (PolicyGradTheory.ProjGA.direct_gradient). This mission adds the multi-parameter statements, the non-stationary -epoch version with its state-time distribution, and the infinite-horizon discounted version, where differentiability of an infinite series must be established rather than computed from a finite recursion.
In the -epoch case the value is a finite polynomial in the policy entries, and the work is bookkeeping: unrolling the backward recursion for against the forward recursion for so that the terms involving telescope. In the discounted case the obvious route, differentiating the recursion term by term and recursing forever, presupposes that is differentiable, which the thesis's proof takes for granted. The value is an infinite series in , so that differentiability is a genuine part of the claim, and the resulting formula must be matched with and , which are themselves defined as infinite series.
Fintype), nonempty; transition kernel IsTransitionKernel P; rewards in as a standing hypothesis of every statement; ; . The thesis's later chapters allow infinite state spaces; this mission is finite.ApproxOptRL.Shared.Model (value, qValue, advantage, futureStateDist; is futureStateDist at the point mass on ). The -epoch layer is defined in this mission (TEpoch): 0-based epochs, tValue by backward recursion, tQValue, stateDist, stateTimeDist.EuclideanSpace ℝ (Fin k). Every statement assumes that (resp. for ) is a probability distribution for every , and that each entry is differentiable at the parameter ("the derivatives exist", p. 48). Differentiability of the value is not assumed.HasFDerivAt: the value map has the right-hand side as its Fréchet derivative at . A statement with fderiv of the value alone, or with a policy that does not depend on , would reduce to and is ruled out.Most practical reinforcement-learning methods do not compute value functions exactly. They alternate between estimating a value function from data, usually with a parametric approximator, and acting greedily with respect to that estimate. Approximate value iteration and approximate policy iteration are the two classical schemes of this kind, and their error analysis decides how accuracy in the estimation step translates into quality of the policies produced. Chapter 3 of S. M. Kakade's thesis On the Sample Complexity of Reinforcement Learning (University College London, 2003) collects the basic guarantees, developed from Bertsekas (Dynamic Programming: Deterministic and Stochastic Models, 1987) for greedy policies, Singh and Yee (1994), and Bertsekas and Tsitsiklis, Neuro-Dynamic Programming (Athena Scientific, 1996). The bounds are stated in terms of the worst-case (max-norm) error of the evaluation step, and the thesis uses them to argue that max-norm error is the obstacle to state-space-independent sample complexity results for these methods, which motivates the later chapters of the thesis.
A finite discounted Markov decision process consists of a finite set of states , a finite nonempty set of actions , a transition kernel (for every a probability distribution over ), a deterministic reward , and a discount factor . A policy is a probability distribution over actions for every state; a deterministic policy is a map , identified with the policy that plays with probability one.
Values are normalized: the value of at is
and the state-action value is . With rewards in , every value lies in . An optimal policy has for every policy and state ; write and . The max norm is on state vectors and on state-action arrays.
The backup operator is . A deterministic policy is greedy with respect to if for every .
The policies need not converge; the statement bounds where they end up.
The results give the standard performance guarantee for greedy approximate dynamic programming: an evaluation error of in max norm costs at most in max-norm suboptimality, uniformly over the asymptotic set of policies, with a geometric rate of approach. Example 3.1.2 of the thesis shows that the factor of Theorem 3.1.1 is attained, so the greedy step itself cannot be improved; the two factors of the horizon in the limit bound are the reason the thesis turns to other error measures in later chapters.
All the statements are classical and proved in the literature (Bertsekas–Tsitsiklis 1996, Chapter 6, in the unnormalized model and with a factor to spare in the limit bounds); Lemma 3.2.3 and Theorem 3.2.2 are stated in the thesis without proof. To our knowledge none has a machine-checked proof. The mission produces formal proofs in the normalized model shared with the formalization of Kakade–Langford (2002) on this platform, so later chapters of the series (conservative policy iteration, policy search) can compare against them.
Approximate policy iteration is not monotone: with evaluation errors, can be worse than at some states, so the argument of exact policy iteration, which uses everywhere, does not apply. The difficulty of Lemma 3.2.3 is to control the distance to optimality without improvement at each step, combining the greedy step with the lack of monotonicity of the new policy's value; the thesis calls the proof of Theorem 3.2.2 "somewhat technical" and omits it. A second, mechanical difficulty is that the normalized value is defined as an infinite series, so its Bellman equation , the optimality equation and the bound have to be derived from that definition before any of the recursions can be run.
ApproxOptRL.Shared.Model: value P r γ π is (defined as times a tsum), qValue is . and are finite types, nonempty; satisfies IsTransitionKernel; every statement assumes and .IsOptimalPolicy P r γ πstar (a stationary stochastic policy dominating every stationary stochastic policy at every state). Such a policy exists for every finite MDP (p. 26 of the thesis), and for finite MDPs it is optimal among all policies.S → A, and are evaluated through the indicator policy detPolicy. "Greedy" is the relation ∀ s a, Q s a ≤ Q s (f s): every tie-breaking rule is covered.ℕ, with the greedy and accuracy conditions as hypotheses at every index; the value-iteration condition is written for indices and .S → ℝ and S → A → ℝ.value for indicator policies, , monotonicity and contraction of policy-evaluation and backup operators in the normalized model, and the bound . Contributions of these lemmas are welcome.Two-stage stochastic linear programming chooses a first-stage decision before a random parameter is revealed and pays an optimal second-stage (recourse) cost afterwards. The classical model fixes the distribution of the random parameter. In practice it is rarely known beyond a few moments, and a decision maker who is averse to risk does not evaluate the recourse cost by its plain expectation. Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) take both points seriously: the distribution is only known to belong to the class of all distributions with given mean and second-moment matrix, the cost is passed through a convex piecewise-linear disutility, and the decision is evaluated against the worst distribution in the class.
Moment-based worst-case bounds go back to Scarf's newsvendor and to the Chebyshev-type bounds of the moment problem (Isii 1962; Bertsimas and Popescu 2005). Delage and Ye (Oper. Res. 58(3), 2010) showed that a broad class of such minimax problems is solvable in polynomial time by the ellipsoid method. For the case in which the uncertainty sits in the objective of the second-stage linear program, this paper gives a single semidefinite program (its Theorem 2.1, the subject of a companion mission) and, in §2.2, identifies the distributions that come arbitrarily close to the worst case. This mission is about the second result.
The first-stage region is . For the recourse set is and the second-stage cost of an objective vector is
The disutility is with . The moment class consists of the distributions of a random vector with and . The worst-case value at is
Its dual (6) is
with symmetric and . Its semidefinite reformulation (8) has the dual (9):
Its variables are scaled conditional moments: is the probability that the th piece of is active, and , are the first and second moments of on that event, multiplied by .
The standing assumptions are Assumption 3, for every , so that is finite, and Assumption 4, . Recourse sets are assumed nonempty.
For every there is a sequence with , and
where all three are finite optimal values: a supremum over a nonempty bounded-above set, an infimum over a nonempty bounded-below set, and a supremum over a nonempty bounded-above set.
Theorem 2.2 says that the semidefinite bound is tight and that the worst case is approached by explicit mixtures. With probability the cost vector sits at the conditional mean , and with a small probability it is perturbed by a large Gaussian. The construction tells which scenarios a minimax solution guards against. The paper's numerical section uses it to stress-test solutions computed under other distributional assumptions. For the risk-neutral case () the bound collapses to Jensen's bound . For it is a combination of Jensen bounds, one per piece of the disutility.
Theorem 2.2 is proved in the paper; no part of it, nor the strong duality of the moment problem that it relies on, is formalized on the platform or, to our knowledge, elsewhere. The mission asks for machine-checked proofs of the identity and of the steps of the extremal construction. Several of these are reusable beyond this paper: weak and strong duality of moment problems, the existence of optimal solutions of moment-type semidefinite programs, and Jensen's inequality for the value function of a linear program.
Most of the argument is linear programming and bookkeeping. The step is a strong-duality theorem for an infinite-dimensional linear program over measures. The paper cites it from Isii's theory of the moment problem, and none of that theory exists in Mathlib. The construction of near-extremal distributions also needs care. A single distribution in generally cannot attain , so the bound is reached only along a family whose second moments are matched by rare, large perturbations. Lemma 2.1 needs measurable selections of an active piece of and of a dual optimal solution of the second-stage program as functions of . When the optimal solution of (9) has zero-weight blocks, the mixture is undefined until the solution is first rearranged.
Vectors are Fin d → ℝ, matrices Matrix (Fin r) (Fin d) ℝ, and distributions are probability measures on Fin d → ℝ with square-integrable coordinates. They are not densities as in the paper's (5). The moment class uses the published MomentDRO.Conf definitions, and is the uncentred second moment. The paper writes both for the dimension of and for dual vectors. Here the dimension is and dual vectors are named π. Indices are zero-based. Bordered matrices are Matrix.fromBlocks on Fin d ⊕ Fin 1 and is Matrix.PosSemidef. is a real infimum and the optimal values are real sSup/sInf of value sets. Every statement that uses an optimal value also asserts IsLUB/IsGLB, so junk values cannot make a statement true.
As printed, Assumption 2 (complete recourse) and Assumption 3 for all contradict each other whenever has a row. The formalization keeps Assumption 3 for all and replaces complete recourse by nonemptiness of , which is what §2's proofs use. Assumption 1 is not used and is omitted. The hypotheses are jointly satisfiable, for example by , , , and .
The sequence clause of Theorem 2.2 alone holds for every finite supremum, so it does not capture the theorem. The goal therefore also asserts the equalities , with all three values genuine, and these carry the content. A formalization that drops them, or states them only through junk values, is ruled out.
A complete development needs the duality theory of the moment problem, Jensen's inequality for concave functions on , compactness arguments for semidefinite feasible sets, and multivariate Gaussian mixtures (ProbabilityTheory.multivariateGaussian in Mathlib). Proofs of individual milestones are welcome. So is a general moment-problem duality theorem from which strong_duality follows.
Zara ships inventory from a central warehouse to each of its stores every week, and for a short-lived fashion item the warehouse holds a limited amount of each size. Deciding how many units of each size to ship to each store is therefore a constrained allocation problem whose objective is the expected sales a store will realize from a given inventory. Caro and Gallien (working paper, 2007; published in Operations Research, 2010) built such a model, embedded it in a weekly shipment optimization, and tested it in a field experiment in Zara's store network. The store-level sales model has one unusual feature, taken from Zara's practice: as soon as one of the major sizes of an item runs out, the whole item is removed from display, so stock-outs of different sizes interact.
The expected sales under that policy have no closed form usable inside a mixed integer program. The paper replaces them by an explicit piecewise-linear function and asserts that this replacement is an upper bound. This mission formalizes that claim, the chain of identities and inequalities that lead to it, and the paper's statement that its shipment program represents the approximation exactly.
A reference is offered in a finite set of sizes , with major sizes and minor sizes . Sale opportunities for size follow a Poisson process with rate , independent across sizes, where is the time since the last replenishment and is the time between replenishments.
Given an inventory vector , the virtual stockout time of size is , and for a set of sizes . Writing , the number of sales in one period is
since every size stops selling when the first major size runs out, and a minor size also stops when it runs out itself. The expected sales function is .
For the approximation, let be the lower incomplete Gamma function, and define the tangent coefficients
with the tangent at equal to the constant . For each size choose a nonempty finite set of tangent indices. The approximate expected sales function is
with . In Lean the objects are expectedSales, hA (), a, b, tangent and gTilde in the namespace FastFashion.Approx.
For every independent Poisson family with positive rates, every , every nonempty , every choice of nonempty finite tangent sets, and every ,
The statement fixes no tangent set, so it covers the paper's numerical choice (7) and every refinement of it.
In the shipment program (MIP) (13)–(19) of §3.2, with positive prices, every optimal solution has at every store .
The upper bound is what makes the paper's optimization coherent: the MIP maximizes , and the bound guarantees that this objective never underestimates the expected revenue of a shipment plan, with an error controlled by the number of tangents. Identity (6) exhibits as a concave function of with explicit Erlang-type slopes; (2) is a standard optional-sampling identity for compensated Poisson processes stopped at a bounded stopping time; and the MIP statement is the step that turns a minimum of affine functions into linear constraints.
The paper proves none of these in detail: (2), (4) and (5) are justified by a reference to the optional sampling theorem, (6) by a sentence on discrete concavity, and the upper bound and the MIP claim by one sentence each. None of the statements has a machine-checked proof. A formalization produces a checked chain from the Poisson model to the deterministic program, fixes the indexing error in the printed coefficients of (6), and isolates the exact hypotheses (nonempty major sizes, nonempty tangent sets, positive prices) under which the claims hold.
The deterministic parts — (3) given pathwise monotonicity, the envelope inequality given concavity, and the MIP argument — are short. The probabilistic identities are not. Equation (2) needs the optional sampling theorem for the compensated process in continuous time, applied at (the paper cites Karatzas and Shreve 1991), which requires showing that is a stopping time for the joint filtration of the family and that is still a martingale with respect to that larger filtration; this is where independence across sizes enters. Equation (4) needs the distribution of , the -th arrival time, which is Erlang; the statement in the model is about first hitting times of a counting process, not about sums of exponential inter-arrival times, so the link between the two descriptions has to be built. Equation (5) needs the identity between Poisson tails and the incomplete Gamma function.
A tempting shortcut is to define directly by formula (2), or by formula (4); both make the corresponding milestones definitional and the goal a statement about formulas rather than about sales. The formalization defines from and from the stopping times.
Finset and the minor sizes its complement. The demand is a structure IsPoissonFamily λ N P: each is a counting process with , non-decreasing right-continuous paths with unit jumps, Poisson increments of mean , independent increments, and the processes are independent across sizes. is a probability measure.WithTop ℝ), so the infimum of an empty set is , never ; is a real number in .The paper's further remark that inherits the qualitative properties of Proposition 1, and the multicolor extension of Appendix §5.2, are not included. Contributions of general infrastructure are welcome: optional sampling for continuous-time counting processes, Erlang hitting-time laws for Poisson processes, and the Poisson-tail/incomplete-Gamma identity are all reusable well beyond this mission.
A large control system is often built from many subsystems , each of which is input-to-state stable (ISS) with respect to the states of the others. Whether the interconnection is again ISS is decided by a small gain condition on the matrix of interconnection gains. For two subsystems this goes back to Jiang, Teel and Praly (1994) and to the Lyapunov version of Jiang, Mareels and Wang (1996). For subsystems, Dashkovskiy, Rüffer and Wirth formulated the condition as a property of a monotone operator on (2007). Rüffer's thesis (2007) and the paper on which this mission is based (arXiv:0901.1842, SIAM J. Control Optim. 2010) turned it into a Lyapunov construction.
The construction needs a geometric object: a path in the positive orthant, unbounded in every coordinate, along which the gain operator strictly decreases every component. For a linear gain matrix this is a Perron vector. For nonlinear gains, its existence is the first of the paper's two main results (Theorem 5.2). This mission formalizes that theorem and the lemmas of §8 that prove it. The companion mission formalizes the second main result, the Lyapunov function built from such a path.
Write . Vectors in are compared componentwise: means for all , and means for all . A function is of class if it is continuous, strictly increasing and , and of class if it is moreover unbounded.
A gain matrix is with and . A monotone aggregation function (MAF) is a continuous with for , whenever , and as . Typical examples are sums and maxima. Given MAFs , the gain operator is
The paper assumes from p. 8 on that , restricted to the coordinates of the nonzero entries of row , still has the strict monotonicity (Remark 2.6). The small gain condition (SGC) is : for every , at least one component of is strictly smaller than the corresponding component of . The set
collects the points that every component of strictly decreases.
An -path (Definition 5.1) is a continuous with every component such that (i) each is locally Lipschitz on ; (ii) on every compact the derivatives of all , where they exist, lie in for constants depending on only; and (iii) for all .
Let be a gain matrix and a compatible vector of MAFs. Assume one of: (i) is linear with spectral radius less than one; (ii) is irreducible and ; (iii) and ; (iv) the entries of are bounded and . Then
In cases (i)–(iii) the entries are in , and in case (iv) they are in .
The milestones follow §8 in the order the proof uses them.
An -path turns a small gain condition into a Lyapunov function. If each is an ISS Lyapunov function of , then is one for the network (Theorem 5.3). So Theorem 5.2 is the step that makes the small gain condition a certificate of network stability, and the corollaries of §5–§7 (sums, maxima, neural networks) all pass through it.
The results are published and proved on paper. None is machine-checked: no proof assistant library contains MAFs, gain operators, the sets and , or -paths. The paper cites three ingredients without proof: Lemma 8.6, Proposition 8.9 and the scaling step of Theorem 8.11. It also gives Theorem 8.14 only as a sketch. Formalizing them closes those gaps in one place.
For bounded gains the problem is easy: far out, every point of a large ray lies in , and the only work is the descent to the origin. With entries, is unbounded and no ray need stay in . Following the image of a single point fails, because forward iterates go to , not to infinity. The paper instead uses backward orbits inside . That this set is nonempty and unbounded is a fixed-point argument of Knaster–Kuratowski–Mazurkiewicz type (Propositions 8.9 and 8.10), not a monotonicity argument. A second obstacle is strictness. A backward orbit is only -increasing, while Definition 5.1 needs strictly increasing components with derivative bounds. This is where the diagonal scalings of Lemmas 8.6–8.7 enter.
is ℝ≥0 and is Fin n → ℝ≥0, with subsystems indexed from . The strict order is a named predicate (SLt), never Lean's < on functions, which means " and ". The small gain condition is ∀ s ≠ 0, ¬ s ≤ T s. The inverses are carried as explicit two-sided inverses, and derivatives are ordinary real derivatives at points where they exist. Compatibility (Remark 2.6) and are hypotheses of every statement about . Irreducibility is the matrix-power form of p. 12, which Mathlib's Matrix.isIrreducible_iff_exists_pow_pos connects to Matrix.IsIrreducible. The spectral-radius hypothesis says that every complex eigenvalue has modulus . The 1-norm defines .
Hypotheses made explicit or corrected:
A path with , or with Lean's < on functions, is not an -path. Such a reading would make the goal follow from the origin alone, and it is ruled out.
Needed infrastructure: comparison-function calculus (inverses and compositions of functions), piecewise linear interpolation in with Lipschitz inverse bounds, and a KKM-type argument on the simplex. The first two are reusable well beyond this mission. Contributions of any milestone, proofs of the cited ingredients (Lemma 8.6, Proposition 8.9, Proposition 8.10, the scaling step of Theorem 8.11) and a full proof of Theorem 8.14 are welcome.
A central question of the theory of learning in games is whether simple adaptive behavior leads players to a Nash equilibrium. Many natural dynamics — fictitious play, best-reply dynamics, replicator dynamics — fail to converge in some games, and the failures are usually exhibited one dynamic at a time. Hart and Mas-Colell (AER 2003) asked a structural question instead: is there any continuous-time dynamic, satisfying one informational restriction, that converges to Nash equilibrium for all games in a reasonable family? The restriction is uncoupledness: each player's adjustment may depend on the current strategy profile and on that player's own payoff function, but not on the payoff functions of the others. This is the situation of players who do not know the opponents' preferences.
Their answer is negative, and the paper proves it with two examples. This mission formalizes the second, built on a three-player game introduced by James Jordan (GEB 1993) in his study of learning mixed-strategy equilibria. A companion mission formalizes the first example, a two-player game on the unit disk.
Three players each choose between two pure strategies, and . A game is identified with its payoff functions , . A state is a mixed profile , where is the probability that player plays (top row, left column, left matrix). Payoffs extend to by expectation over independent randomizations, and is a Nash equilibrium when no player can raise its expected payoff by changing its own coordinate.
Jordan's family consists of the games
indices modulo 3, with parameters close to : each player wants to mismatch the next player. Jordan's game is the member with all ; every game of has a unique Nash equilibrium , and .
A dynamic for a family is a vector field on , one for each . It is uncoupled if whenever give player the same payoff function. When every game of has a single Nash equilibrium , is Nash-convergent for if, for every , is a rest point, every solution converges to it, is , and the Jacobian of at is hyperbolic and stable: all its eigenvalues have negative real parts.
Let have the single-Nash-equilibrium property and contain every game of that is close to . Then
Two further items record the paper's observations: uncoupledness forces , and such a matrix has an eigenvalue with positive real part when and spectrum otherwise. A last item shows that the coupled dynamic is Nash-convergent.
The theorem says that convergence to Nash equilibrium is not a property that adaptive dynamics can deliver on informational grounds alone: as soon as a family contains the games near , any rule in which players respond only to their own payoffs fails for some game, even though every game in the family has a unique equilibrium and a coupled rule converges for all of them. The finite example matters because it shows that the obstruction is not an artifact of continuum strategy spaces: it occurs in a game in mixed strategies. The paper contrasts it (§IV) with the existence of uncoupled dynamics that converge to correlated equilibria: Nash equilibrium cannot be reached in an uncoupled way, while correlated equilibrium, a notion based on coordination, can. Follow-up work extends the impossibility to stochastic uncoupled dynamics (Hart and Mas-Colell, GEB 2006) and surveys the area (Hart, Econometrica 2005).
The result has been proved since 2003; no machine-checked proof of it is known. A formal proof requires an equilibrium computation in a parametric family of finite games, a careful treatment of the derivative of a vector field defined only on a cube, and a spectral fact about real matrices. The definitions of uncoupled and Nash-convergent dynamics written here are reusable for other impossibility results of the same kind.
The obvious attempt is to analyze a particular dynamic and show that it cycles around . That proves nothing about other dynamics: the statement quantifies over every uncoupled , so the argument must extract a constraint on from uncoupledness alone. Uncoupledness only relates the dynamic at different games through single coordinates of , and Nash-convergence only constrains at the equilibria of the games in ; neither says anything directly about the Jacobian at . Formally, the delicate steps are the uniqueness of the equilibrium for all nearby parameters, which requires excluding pure and partially mixed equilibria, and the passage from vanishing along a segment to a vanishing partial derivative.
Players are indexed in Lean (the page's player is index ), strategies are Fin 2, and a game is Fin 3 → (Fin 3 → Fin 2) → ℝ. The state space is ; a dynamic is any map , whose values outside never matter. Committed conventions:
FatkhullinPolyak.Discrete.IsHurwitz), and convergence of every solution. The Jacobian is the derivative within .The family cannot be vacuous: Jordan's games with satisfy both hypotheses, and the coupled-dynamic item certifies that Nash-convergence itself can be met, so the goal's force rests on uncoupledness. Contributions welcome include the equilibrium computation for , the spectral lemmas (which are independent of game theory), and the calculus step from vanishing along a segment to a vanishing partial derivative within a cube.