Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The -model is the simplest exponential random graph model in which every vertex has its own parameter. It was studied by Holland and Leinhardt (1981) in the directed case and by Park and Newman (2004) and Blitzstein and Diaconis (2011) in the undirected case, and it is a close relative of the Bradley–Terry model for paired comparisons. Its sufficient statistic is the degree sequence of the observed graph, so fitting the model to data means solving a system of nonlinear equations in unknowns, one per vertex, where can be in the thousands.
Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 21 (2011)) give a simple iteration for this system and prove that it converges geometrically fast whenever a solution exists, at a rate that does not deteriorate with the number of vertices, and that it detects when no solution exists. The same estimate is then used in the paper's consistency theorem for the maximum likelihood estimator (Theorem 1.3) and in its graph-limit theorem (Theorem 1.1). This mission formalizes that algorithmic result, Theorem 1.5, together with the chain of numbered displays in Section 2 that proves it.
Let and label the vertices . For , the -model puts an edge between distinct vertices and independently with probability
Given an observed graph with degrees , the maximum likelihood estimate must satisfy the ML equations
The sup norm of is . For put , and define the map by
Starting from any , the fixed-point iteration is . The fixed points of are exactly the solutions of (3).
For an matrix , the operator norm is . For , the class consists of the matrices with , and for . For , is the matrix with entries .
There are functions and , continuous, independent of and , such that for every and every : if (3) has a solution , then , it is the unique solution of (3), and for all and
and if (3) has no solution, then every orbit is unbounded.
and . 6. (10), p. 13: a single , continuous in its arguments, with and .
The theorem turns an implicit statistical object, the MLE of an -parameter model, into the limit of an explicit iteration with three guarantees: a convergence rate that depends on the size of the parameters but not on ; an a posteriori error bound in terms of the computable step ; and a certificate of non-existence. The uniqueness of the MLE comes out of the same estimate. In the paper, the a priori bound is the device that proves consistency of the MLE (Theorem 1.3, applied with ), and the two-step contraction is reused in the proof of the graph-limit theorem.
The result is proved in the paper; no machine-checked proof of it is known. The work here is to formalize the known proof. The matrix inequality of Lemma 2.1 and the derivative bounds (6)–(7) are self-contained and can be attacked independently of the iteration.
The obvious approach is to show that is a contraction and apply Banach's fixed-point theorem. This fails: every row of the Jacobian of has absolute sum exactly , so is only non-expansive in the sup norm, never strictly contracting. Contraction appears only for the two-step map , through the sign pattern of the Jacobian (positive diagonal, uniformly negative off-diagonal), and only on bounded sets, with a factor that tends to as the norms grow. A second difficulty is uniformity: the factor must be bounded away from independently of , which needs , hence . For the converse, there is no fixed point to anchor the orbit, so boundedness of the orbit has to be converted into convergence before a fixed point exists.
Fin n ; vectors are Fin n → ℝ, whose Mathlib norm is the sup norm . Matrix norms are the explicit maximal absolute row sum.Needed infrastructure: calculus of (derivatives of of a sum of exponentials), the integral form of the mean value theorem for maps , and elementary matrix-norm estimates. The class and Lemma 2.1 are reusable for other diagonally dominant iterations. Proofs of any milestone are welcome, in any order.
A reinforcement-learning agent that does not know its environment has to act and learn at once. Each step spent gathering information about unfamiliar states is a step not spent collecting reward, and an agent that only exploits what it already knows may never find better behaviour. Chapter 8 of Kakade's thesis (Kakade 2003) turns this trade-off into a counting question. Run an algorithm for an arbitrarily long time on one unbroken path of experience, with no resets. At how many timesteps does it fail to act optimally with respect to a fixed planning horizon ? Kakade calls this number the sample complexity of exploration.
The question builds on two algorithms. (Kearns and Singh 2002) gave the first polynomial-time guarantee for near-optimal behaviour in an unknown MDP. (Brafman and Tennenholtz 2002) replaced 's explicit explore-or-exploit switch by optimism: unknown states are treated as maximally rewarding. Kakade's chapter sharpens the analysis of . For deterministic MDPs it shows that the number of non-optimal steps is at most , which matches its own lower bound. The thesis notes that its deterministic results are similar to those of Koenig and Simmons (1993), with the dependence on , and made explicit (pp. 99, 104). The later PAC-MDP literature (for example Strehl, Li and Littman 2009) took this counting notion as its standard measure of exploration efficiency.
An MDP has a finite set of states, a finite nonempty set of actions, a transition model and a deterministic reward . A deterministic MDP has a next-state map , with exactly when .
Online model. An algorithm is a deterministic function that maps the path observed so far, , to the next action . Started at , it produces one path ; is the subpath up to . The -step end time of is the smallest multiple of larger than . The -step value of the algorithm on is the normalized reward it collects until ,
and is the supremum of this quantity over all algorithms continuing from .
-step policies. A -step policy is a sequence of deterministic decision rules . Its -value is , and is the supremum over -step policies. For a set of states , the induced MDP agrees with on and makes every state outside absorbing with reward . The escape probability is the probability that the path of in leaves . A transition model is an -approximation to if for every .
For every , and there is one algorithm such that, for every deterministic MDP with rewards in , every start state and every ,
The result. The bound does not depend on . However long the agent runs, only a fixed number of its steps fail to be -step optimal. The thesis's Theorem 8.3.6 shows that every algorithm has such steps on some deterministic MDP, so for deterministic MDPs the upper and lower bounds coincide. The induced-MDP lemmas carry over unchanged to stochastic MDPs. Together with Lemmas 8.5.4 and 8.5.5, they give the chapter's general bound (Theorem 8.3.1). They are the template for later optimism-based analyses, which compare an optimistic model with the true one and charge the difference to the probability of leaving the known region.
Formalizing it. The results are proved in the thesis; neither Mathlib nor the Prove2Me catalog contains a machine-checked version of any of them. A complete development would contain:
The proof of Lemma 8.5.5 in the thesis uses a Chernoff bound of the form . This form fails for the upper tail when , so the pinned statement needs a different argument.
The algorithm must be fixed before the MDP. It knows nothing about or beyond what its own path reveals, yet the count has to hold for every MDP, every start state and every run length at once. A direct approach could explore each state-action pair once and then plan. That does not bound the count. Exploration is interleaved with exploitation, the agent can only reach unknown pairs through known states, and every step on the way is judged against the full -step optimum of the current cycle. The work lies in charging each non-optimal step to a distinct newly tried state-action pair, with at most steps charged per pair, while the planning policy is recomputed every time the set of known states grows. In the stochastic lemmas, the main issue is that is a supremum over all -step policies, so the comparison has to go through for every competing policy, not only the planner's.
IsTransitionKernel functions .List (S × A × ℝ) → S → A. The run is defined by recursion and is infinite. is the realised normalized sum up to the end time, and is the backward recursion , which is the supremum over algorithms by the Markov property. The count runs over for every .Four formalizations would make the goal trivial or false, and each is excluded:
Reusable beyond this mission are the finite-horizon value layer, the induced-MDP and escape-probability lemmas, and the concentration bound. Contributions to any of these are useful independently of the goal.
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".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.
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 (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.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.
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.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.
Many problems in signal processing, statistics and decision theory have two blocks of variables coupled by a smooth term: matrix factorization, blind deconvolution, feasibility problems for two sets, and models of two agents adjusting their decisions in turn. Minimizing over one block at a time (alternating minimization, or Gauss–Seidel) is the natural method. Without convexity it can oscillate, and its iterates need not converge. Attouch, Bolte, Redont and Soubeyran (Math. Oper. Res. 35(2), 2010; arXiv:0801.1780) regularize each block step by a proximal term. They prove that, when the objective satisfies the Kurdyka–Łojasiewicz (KL) inequality, every sequence of the method that does not run off to infinity has finite length and converges to a critical point.
Timeline:
Let and be proper (never , finite somewhere) and lower semicontinuous. Let be continuously differentiable, with Lipschitz on bounded sets. This is assumption (H) for
The product carries the Euclidean norm . Write .
Given and step sizes , the proximal alternating scheme is
Assumption (H1) asks that , that be proper, and that for all , for some .
The Fréchet subdifferential is the set of with . The limiting subdifferential collects the limits of along with . A point is critical if . has the KL property at if there are , a neighbourhood of and a continuous concave with , , , such that
If satisfies (H), (H1) and has the KL property at every point of , then every sequence of (5–6) satisfies
Theorem 9 makes the KL inequality the single hypothesis behind global convergence of a nonconvex block method. Semi-algebraic, subanalytic and definable data satisfy it, so the theorem covers sparse and low-rank regularizers, indicator functions of semi-algebraic sets, and polynomial couplings. With , and it yields convergence of an averaged alternating projection method between two closed sets (§3.4 of the paper). The proof pattern of sufficient decrease, a relative-error subgradient bound and the KL inequality was later abstracted for PALM and many other algorithms. A formal proof of this paper's argument therefore covers the template those analyses reuse.
The result has been proved since 2010. To our knowledge it has not been formalized in any proof assistant. Mathlib has the Fréchet derivative and the gradient, but no limiting subdifferential and no KL theory. The published Prove2Me definitions of the limiting subdifferential and of the KL property (from the Li–Pong ADMM series) are reused here, so this mission also tests that infrastructure on a second algorithm.
The decrease estimate (7) gives only . That makes steps vanish and limit points critical (Proposition 6), but it does not give convergence, because square-summable steps can have infinite total length. Turning square summability into summability needs the KL inequality. That inequality holds only near a critical point and only on a sublevel band, so the iterates must first be shown never to leave a ball , by an induction that uses the very finite-length estimate it is trying to establish. The constants in (16) are arranged so that this induction closes. A second difficulty is nonsmooth calculus: the subdifferential sum rule for and the closedness of the graph of along sequences with converging function values. Lower semicontinuity alone does not give convergence of the function values; the proximal inequalities do.
Everything lives in the namespace ProxAltMin.Conv, in Lean 4 with Mathlib. Conventions:
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and the product is the product WithLp 2 (… × …), not the sup-norm product.EReal with "never " as part of properness.Theorem and page numbers are those of arXiv:0801.1780v3 (22 Jan 2013), which is the version read; the published article has the same content.
A trivializing formalization is ruled out: the run predicate is satisfiable (Lemma 5's existence milestone; for any constant sequence is a run), the constants and are tied to the data rather than chosen by the prover, and no conclusion is a sum or a distance whose library value is on bad input.
Needed infrastructure: the subdifferential calculus behind Proposition 3 (a smooth perturbation and a separable sum), the closedness of the limiting subdifferential, existence of proximal minimizers for coercive lower semicontinuous functions on , and the elementary but delicate bookkeeping of Theorem 8. The first two are reusable well beyond this mission. Contributions welcome: proofs of any milestone, and general lemmas on limiting subdifferentials stated as separate theorems.
A busy runway is the bottleneck of an airport, and the order in which arriving or departing aircraft use it determines how many operations fit into an hour. Consecutive aircraft must be spaced by minimum separations that depend on both aircraft (a light aircraft behind a heavy one needs a long gap because of wake turbulence), so reordering the first-come-first-served (FCFS) queue can raise throughput considerably. Unrestricted reordering is unacceptable in practice: it makes the controllers' job harder and can push one aircraft to the back of the queue indefinitely. Following Dear (1976), constrained position shifting (CPS) allows each aircraft to move at most positions away from its FCFS position, with between 1 and 3 in practice.
Earlier algorithms for CPS either exploited a small number of aircraft types and ignored time windows and precedence constraints (Psaraftis 1980), or needed exponentially many parallel processors (Trivizas 1998), and Carr (2004) conjectured that runway scheduling under CPS has exponential complexity in general. Balakrishnan and Chandran (Oper. Res. 58(6), 2010) showed that, for fixed , the problem with time windows and precedence constraints is solved by dynamic programming on a network whose size is linear in the number of aircraft. This mission formalizes the core of that result: the network, its precedence pruning, and the dynamic program for the minimum makespan.
There are aircraft, labelled in FCFS order, and the landing positions are also . An instance consists of
A -CPS sequence is a bijection from positions to aircraft with for all . A feasible schedule is such a with landing times such that , for all positions , and every precedence pair is respected. The makespan is , the landing time of the last aircraft.
The CPS network has stages . A node of stage is a list of distinct aircraft occupying the positions that end at , each within of its FCFS position; its last entry is its final aircraft. An arc joins a stage- node to a stage- node when the first entries of are the last entries of . A source-sink path picks one node per stage, joined by arcs, and its sequence puts the final aircraft of the stage- node at position . The pruned network deletes the nodes that violate a precedence pair : those containing before , or at a position less than , or at a position greater than .
On , with the window of the final aircraft of , the separation between the final aircraft of and , and the predecessors of , the dynamic program is at stage 1 and
with .
where is stage of ; the second identity is stated as " is the least makespan iff is the least admissible " for every real .
The network turns a search over permutations into a shortest-path-like computation over nodes, so for the small values of used in practice the minimum makespan with time windows and precedence constraints is computed in time linear in . The same network underlies the paper's algorithms for total delay (§5.2) and, in a time-expanded form, for arbitrary separable costs without the triangle inequality (§6).
The paper's proofs are short and informal. A formalization pins down exactly what means (the paper describes it only as "arrival time of the final aircraft of node in an optimal solution"), makes precise which nodes the precedence pruning removes, and checks the correctness of the stage- rule. The result has not been machine-checked before.
Two features of the model make the correctness of the network nontrivial. First, a node records only a window of at most consecutive positions, so nothing local prevents a path from using the same aircraft twice or omitting one; Theorem 1 asserts that the global sequence is nevertheless a permutation, and Lemmas 1 and 2 assert that precedence, a global property of the sequence, is detected inside single nodes. Second, the recursion (1) adds the separation only between consecutive aircraft, while feasibility constrains every pair of aircraft; the triangle inequality is what reconciles the two, and without it Lemma 3 fails.
The obvious reading of §4.1 also fails: taking the least over all stage- nodes, as the paper prints, can select a node whose final aircraft lands after its latest time. The goal filters stage by .
All data are real numbers; aircraft and positions are Fin n, 0-based; stages are 1-based natural numbers; [NeZero n] encodes . Separations are pairwise in the definition of feasibility, never only consecutive. The recursion takes values in WithTop ℝ, with ; optima are stated with IsLeast over sets of makespans, never with a real infimum. Precedence pairs are a Finset of ordered pairs of distinct aircraft, covering both of the paper's cases.
Explicit readings of loose phrases:
Not formalized: running times (Proposition 1 and the preprocessing remark), the predecessor pointers and tie-breaking that reconstruct an optimal sequence, the removal of nodes unreachable from the source or the sink (it does not change the set of source-sink paths), asymmetric shifts (§3.2) and disjoint time windows.
A formalization that defines feasibility with consecutive separations only, defines by the recursion and states Lemma 3 as an unfolding, or states Theorem 1 as "some CPS sequence exists iff some path exists" would be trivial; the statements here avoid all three.
The definitions (instance, -CPS sequences, the CPS network and its pruning) are shared with the two other missions of this series (total delay, discrete time) and may be consolidated later. Proofs of the milestones, and lemmas about the window structure of the network, are welcome.
Runway capacity is the binding constraint at many busy airports. An aircraft landing or taking off behind another must wait a minimum separation time that depends on the two aircraft's weight classes, because of wake vortices; the US Federal Aviation Administration publishes these spacing requirements. Reordering aircraft changes the sum of the separations incurred and hence the delays, but unrestricted reordering is unacceptable to airlines and controllers: an aircraft that arrived early could be pushed to the end of the queue. Constrained position shifting (CPS), introduced by Psaraftis (1980) and used in the United States and Europe since, allows each aircraft to move at most positions from its first-come-first-served (FCFS) position.
Balakrishnan and Chandran (Operations Research 58(6), 2010) recast CPS scheduling as dynamic programming on a layered network, the CPS network, whose size is polynomial in the number of aircraft for fixed . Their §4 minimizes the makespan (the landing time of the last aircraft). §5.2 minimizes the total delay, equivalently the average delay, which measures passenger and airline cost more directly. This mission formalizes §5.2.
There are aircraft labelled in FCFS order, a maximum position shift , separations (the minimum time between leading aircraft and trailing aircraft ), and a finite set of precedence pairs with , meaning that must land before . The separations satisfy the triangle inequality , as wake-vortex separations do for arrivals-only or departures-only operations.
A -CPS sequence is a permutation of the aircraft (position receives aircraft ) with for every . A feasible schedule is a -CPS sequence that places before for each precedence pair, together with landing times (by position) such that
There are no time windows. Its total delay is , measured from time , at which all aircraft are available.
The CPS network has stages . A node of stage is a sequence of distinct aircraft that can occupy positions (each within of its position). Its last aircraft is its final aircraft. An arc joins a stage- node to a stage- node when the sequences overlap: the first aircraft of are the last aircraft of . A source-sink path picks one node per stage, and its sequence assigns position to the final aircraft of the stage- node. Precedence is incorporated by deleting every node that places before for some pair , or that places an aircraft outside the positions a pair allows it (§3.1). The result is the pruned network . For nodes , is the separation between their final aircraft.
For a node in stage and times along a path to , the paper uses the partial objective
Give the arc from stage to stage the distance , and source and sink arcs distance . Then a feasible schedule exists if and only if has a source-sink path, and
where each minimum exists exactly when the other does.
where is the set of predecessors of in .
The result turns a sequencing problem over up to orders into a shortest-path computation on a directed acyclic graph with nodes, and it does so while respecting precedence constraints, which earlier CPS algorithms (Psaraftis 1980; Trivizas 1998) could not handle. It is the average-delay counterpart of the makespan algorithm of §4 and shares its network. The same network carries the discrete-time models of §6.
The paper's proof of the equivalence is one sentence ("follows from properties of shortest paths and is omitted here"). Propositions 2 and 3 are proved in a few lines, and Theorem 1 by an argument about windows of consecutive positions. None of these results has a machine-checked proof. A formal development makes explicit the conventions the prose leaves implicit (the time origin, pairwise separations, which nodes Proposition 3 refers to) and checks that the recursion and the shortest-path value really compute the minimum total delay.
The arc distances weight the separation into stage by , the number of aircraft whose landing it delays. The equivalence needs two directions. A path's length must be the total delay of the schedule that lands each aircraft at its predecessor's time plus the separation, and that schedule must satisfy every pairwise separation, not only the consecutive ones; this is where the triangle inequality enters. Conversely, every feasible schedule must have total delay at least the length of its sequence's path, and every feasible sequence must be a path of . The last point is Theorem 1 with precedence pruning: a node sees only consecutive positions, so detecting a violated precedence pair inside one node requires the position filter of §3.1 for pairs that reverse FCFS order. Proposition 3 is false for nodes that lie on no source-sink path, which the printed statement does not exclude.
Aircraft and positions are Fin n, 0-based, and stages are 0-based natural numbers, so the arc into stage has distance . Separations are real, nonnegative and satisfy the triangle inequality; feasibility requires them between every pair of positions. Landing times are real and nonnegative. The paper fixes no time origin, but its path length equals the total delay exactly when delays are measured from , and without a lower bound on the times the objective has no minimum. Minima are stated with IsLeast on sets of values, never with a real infimum. Feasibility and the existence of a path are stated separately, because the equality of least elements alone does not force them to exist.
The following loose phrases are given explicit readings. "In an optimal solution" (Proposition 2) means a feasible schedule whose total delay is at most that of every feasible schedule. "The CPS network" in Proposition 3 means nodes lying on a source-sink path, stated for the network without precedence pruning, which also covers the pruned one. "" means the least element of the set of values of over partial schedules ending at , and the printed is read as . The boundary value is not printed and is stated explicitly. Precedence pruning uses the printed Case II rule. Running times (the bound) are not formalized.
A trivializing formalization would require separations only between consecutive aircraft, define the minimum by the recursion itself, or use a network whose nodes need not be distinct or admissible. Here the minimum is defined directly over feasible schedules, separations are pairwise, and the nodes are checked against the paper's Figure 1 (stage sizes 2, 4, 7, 14, 14, 7 and 13 paths for , ).
The development needs finite sums, permutations of Fin n and lists. The network layer (stages, arcs, precedence pruning, Theorem 1) is shared with the makespan and discrete-time missions of this series and reusable for any CPS objective. Proofs of any milestone, alternative proofs of the goal, and generalizations (asymmetric shifts, §3.2) are welcome.
A submodular function on a finite set is a function on subsets of with . Minimizing such a function is one of the central tractable problems of combinatorial optimization: it contains minimum cuts in directed graphs, matroid intersection and polymatroid problems, and many scheduling and facility-location subproblems. Grötschel, Lovász and Schrijver showed in 1981 that it can be done in polynomial time with the ellipsoid method; in 2000, Schrijver (JCTB 80, 346–355) and, simultaneously, Iwata, Fleischer and Fujishige (J. ACM 48, 2001) gave the first combinatorial strongly polynomial algorithms.
In many applications the function is not defined on all subsets of but only on a ring family: a collection closed under union and intersection, such as the order ideals of a precedence relation in scheduling, or the sets of a closure system. The last section of Schrijver's paper (§6, pp. 353–354) shows that nothing is lost: any algorithm minimizing submodular functions on all subsets of also minimizes a submodular function given only on a ring family. This mission formalizes that reduction.
Let be a finite set. A collection of subsets of is a ring family if and whenever . A real function is submodular on if
Following the paper, is normalized: , , and for all , where is the smallest set of containing . (Elements with the same can be identified.) Under this normalization is the family of lower ideals of a partial order on .
For , the closure is the smallest set of containing . For , is the largest set of not containing . The paper defines weights
with the modular extension , and the function on all subsets of
In Lean, is a type with [Fintype V] [DecidableEq V], subsets are Finset V, is C : Set (Finset V), and the objects above are IsRingFamily C, SubmodularOn C f, closure C X, M C v, L C v, cw C f v (for ), csum C f X (for ) and g C f X, all in the namespace SchrijverSFM.Ring.
Under the normalization above, for submodular on :
and, if minimizes over all subsets of , then and
Both conjuncts are needed: the second alone follows almost from the definitions, while the first is what makes an all-subsets algorithm applicable to in the first place.
The reduction means that a single algorithm for unconstrained submodular minimization serves for every ring family, given only the sets . This is how ring-family constrained problems (for example minimum-cost closures and precedence-constrained scheduling objectives) are routinely handed to general submodular-minimization codes, and it is the standard justification for stating submodular minimization algorithms over only.
On the formal side, the mission produces a small reusable layer on ring families of finite sets (closure operator, the lower-ideal representation, the largest set avoiding an element) together with the monotonization trick (24), which is of independent use whenever a function on a lattice of sets has to be made monotone by a modular correction. The result is classical and its proof in the paper is complete; to our knowledge no machine-checked version exists. Companion mission I of this series formalizes the algorithm of §§2–5 itself; this mission does not depend on it, since the algorithm enters only as the hypothesis that a minimizer of is given.
Every step is elementary, but two points are easy to get wrong. First, (24) is proved on the page by assuming ; reducing the general case to such one-element steps inside requires the normalization : without it a ring family can jump by more than one element (for with the inequality (24) fails for suitable ). Second, the weights evaluate at , which belongs to only because of the same normalization; a formalization that drops it lets values of outside leak into and . The submodularity proof (27) also needs the asymmetric closure facts — equality for unions but only containment for intersections — which is exactly why the monotonicity (24) is required.
Finset V; is a Set (Finset V).Finset V; only its values on matter, and under the hypotheses no other value enters , or the conclusions. The paper allows any ordered field; the formalization uses .∅ ∈ C, Finset.univ ∈ C, and M C u ≠ M C v for u ≠ v. No hypothesis is made; §6 does not use it.Finset.inf) of the sets of containing , and the union (Finset.sup) of the sets of avoiding ; their default values on an empty family are never reached under the hypotheses.NonmonotoneSubmod.Shared.Submodular.Contributions welcome: proofs of the milestones in the order listed, general lemmas on closure operators of ring families of Finsets, and the lower-ideal representation, which is reusable beyond this mission.
A Markov decision process is specified by numbers: transition probabilities and rewards. In practice these numbers are estimated from data, elicited from experts, or produced by aggregating the states of a larger model, and in each case what is actually known is a range for each parameter rather than its value. Givan, Leach and Dean (Artificial Intelligence, 2000) introduced bounded-parameter MDPs (BMDPs) to reason about a whole family of MDPs at once: every transition probability is only known to lie in a closed interval. Their motivation was state-space aggregation, where grouping states with similar but not identical dynamics yields exactly such interval bounds, and the same object later reappeared as the interval or "box" uncertainty set of robust MDPs (Nilim and El Ghaoui, 2005; Iyengar, 2005) and of optimistic exploration in reinforcement learning (Strehl and Littman, 2008).
Over such a family, the value of a policy is no longer a number but an interval, and "optimal" needs a definition. This mission formalizes the paper's answer: two total orders on intervals, the corresponding optimal policies, and the Bellman-like equations their interval value functions satisfy.
An exact MDP has a finite set of states, a finite nonempty set of actions, transition probabilities with , a reward for each state and a discount rate . A policy is a map ; is the set of all policies. The value function is the expected discounted sum of rewards along the Markov chain with transitions . The operators
act on value functions . is the statewise order.
A BMDP gives for each an interval with , a reward and a discount rate . Its members are the exact MDPs with that and and with . The interval value of a policy is
Intervals are compared by the optimistic order, which compares upper bounds first and breaks ties by lower bounds, and the pessimistic order, which compares lower bounds first:
A policy is optimistically optimal if for all and ; pessimistically optimal is defined with . The optimal interval value functions are and .
At every state ,
and the same with in place of . The maximum over actions is for the total order on intervals: attained by some action and an upper bound for every action.
In the order the proof uses them: Theorem 3 (second sentence: is the unique fixed point of ); Theorem 6 (comparison: implies , and its three variants); Lemma 1 (every member's values and backups are bracketed by finitely many order-maximizing MDPs); Lemma 2 (statewise composition of member MDPs dominates, or is dominated by, both components); Theorem 7 (-maximizing and -minimizing MDPs exist among the order-maximizing ones); Corollary 1 ( and are a minimum and a maximum for ); Lemma 3 (statewise composition of policies improves the upper, resp. lower, bounds); Theorem 8 (optimistically and pessimistically optimal policies exist).
Theorem 9 is the interval analogue of the Bellman optimality equation. It is what makes the optimal interval value functions computable: the paper's interval value iteration algorithms and (Section 5) iterate exactly the right-hand sides of (25) and (26). The lower half of (26) is the max-min equation of robust dynamic programming with rectangular box uncertainty, and the upper half of (25) is the max-max equation behind optimistic planning; Theorem 9 states both, together with the tie-breaking second component, in one model. Theorems 7 and 8 are of independent use: a single member MDP is worst (or best) for a policy at all states at once, and the partial orders on interval value functions nevertheless have maxima over policies.
None of these results has a machine-checked proof. The platform has robust Bellman equations in other models (costs, general rectangular sets, a sup over nature) but nothing on BMDPs, interval value functions, or the orders and . The mission produces the paper's optimality theory end to end, from the comparison principle for exact MDPs to the two Bellman-like equations, on a model shared with the companion mission on interval policy evaluation.
The orders and are total on intervals but only partial on interval value functions, and they are lexicographic. The obvious construction of an optimal policy, switching statewise to whichever of two policies has the better interval, fails: the composed policy need not dominate either component in , because lower bounds can get worse at states where the upper bounds do not change (the paper says so explicitly, eq. (20)). Existence therefore needs a two-stage argument. A second obstacle is that and are defined statewise, as minima over an uncountable family; that one member attains them at every state simultaneously is a theorem (Theorem 7), and the Bellman-like equations rest on it. Finally, the inner minima in (25) act on , the lower bound of an optimistically chosen policy, which is not the componentwise best lower bound over policies; the equation couples the two components through the tie-break.
and are finite types, is nonempty; may be empty. An exact MDP is a structure with transition function F p α q , stochastic rows, reward and discount . is defined as the convergent series , not as a solution of (2). Rewards of the BMDP are tight, as the paper assumes from footnote 3 on; reward intervals are not formalized. Members of form a subtype of exact MDPs with the BMDP's and . The minima and maxima of Definition 3 and of (25)–(26) are the real infimum and supremum over that subtype, which is nonempty and on which values are bounded, so no junk value enters. Intervals are pairs (lower, upper); the orders (17) are spelled out. Policies are deterministic stationary maps , the paper's . An ordering of is a bijection Fin |Q| ≃ Q, and the index of Definition 1 is the largest index at which expression (9) does not exceed 1 (the page's phrase admits ties; only the largest index keeps the remaining mass inside its interval). Definition 8 is read as for an optimistically optimal , so the goal is quantified over all optimistically (pessimistically) optimal policies; Theorem 8 is the milestone that makes this quantification non-vacuous. Lemma 3 is stated as in the Appendix (p. 36): part (d) concerns , where p. 17 misprints .
A formalization in which members carry their own discount, rows need not sum to one, the minima range over all functions , or is the componentwise supremum over policies would make several statements false or trivial; each is ruled out above.
Contributions welcome beyond proofs of the milestones: a reusable theory of discounted policy evaluation for finite MDPs (the series representation, the fixed-point characterization, monotonicity of ), which other missions on finite MDPs can import.
Regev's On Lattices, Learning with Errors, Random Linear Codes, and Cryptography (J. ACM 56(6), 2009, Article 34; doi:10.1145/1568318.1568324) introduced the Learning with Errors (LWE) problem and built a public-key cryptosystem on it. The source for this mission is that published J. ACM article. The paper's main theorem, a quantum reduction from worst-case lattice problems to LWE, is outside this series; this mission formalizes a self-contained piece of finite combinatorics from §5.
In the cryptosystem the public key is a list of LWE samples, and a bit is encrypted by adding up a uniformly random subset of them. Semantic security rests on one fact: if the public key were truly uniform, the sum of a random subset of it would be close to uniform, so the ciphertext would carry no information about the bit. Claim 5.3 (p. 34:36) makes this precise for an arbitrary finite abelian group . It is a special case of the leftover hash lemma of Impagliazzo and Zuckerman (1989), in which the family of functions indexed by is a universal hash family. Variants of the same statement appear in the security proofs of most lattice-based encryption schemes that use random subset sums, including the dual-Regev and GPV-style constructions.
Let be a finite abelian group, written additively, with elements, and let be an integer. For and the subset sum is the sum of the with (the empty subset gives ). The distribution of the sum of a uniformly random subset of is
The paper defines the statistical distance of two densities as , with range , and notes that the same definition applies to discrete random variables (p. 34:14). The distance of from the uniform distribution on is therefore
with no factor . Expectations and probabilities over refer to a uniform choice of , that is, the uniform distribution on all tuples, repetitions allowed: .
In Lean these objects are RegevLWE.SubsetSum.subsetSum, P, statDistUniform and expectG.
Both sentences of the claim are in the goal. The second is what the security proof (Lemma 5.4, p. 34:37) uses: for all but a fraction of public keys, the random subset sum is within of uniform. The constants are exactly as printed.
The result. Claim 5.3 is the step in the security proof of Regev's cryptosystem that removes the public key from the picture: once the key is replaced by uniform samples (by the LWE assumption), the claim shows that an encryption is statistically close to uniform, independently of the encrypted bit. The parameter choice of Lemma 5.4 is exactly what makes negligible for . Without the claim the cryptosystem would have a hardness assumption but no reduction from it.
Formalizing it. The claim is proved, with a complete argument in the paper; nothing here is open. To our knowledge no machine-checked proof of this statement, or of the leftover hash lemma for subset-sum hash families over a general finite abelian group, exists in Mathlib or on the platform. A formal proof gives a reusable, constant-exact statement of the subset-sum leftover hash lemma with the paper's normalization of statistical distance. The four milestones are standard facts about finite averages and collision probabilities that recur in many cryptographic security proofs.
There is no deep step; the work is in organizing finite counting arguments without loss. Two points need care. The collision fact holds for every pair only because the coefficients lie in : for a general linear form over a group with torsion, a nonzero coefficient vector need not give a uniformly distributed sum, so an argument that treats the coefficients as arbitrary integers fails. And passing from the bound to the expected distance requires the exchange of expectation and square root in the right direction (concavity), which is easy to misapply. The bound must hold for every finite abelian group and every , including and , with no asymptotic slack.
[AddCommGroup G] [Fintype G] [DecidableEq G]; , and is allowed (then is the point mass at and the claim holds). No hypothesis is added to the paper's statement: holds for every group.Fin l → Bool; ranges over all functions Fin l → G, so the uniform choice of is over all tuples with repetition, not over -element subsets of .Real.sqrt (Real.sqrt x).A backward stochastic equation determines its current value from a conditional expectation of future values. A forward equation determines its current value from past values. Coupling the two makes existence depend on more than integrability of the data: the feedback between the past and future can prevent a solution. Antonelli's 1993 paper studies this interaction in an space for equations driven by bounded variation processes, motivated in part by recursively defined stochastic utility in finance (Antonelli 1993, pp. 777–778).
The paper first gives an existence and uniqueness condition for a coupled system. It then tests the size of that condition with two examples. The first uses a singular coefficient matrix; the second, targeted here, uses a nonsingular linear coupling. This distinction matters because the failure of existence in the first example could otherwise be attributed to the singular matrix. The second example places the obstruction at a particular time horizon while retaining a linear map with Lipschitz constant one (Antonelli 1993, pp. 791–792).
Fix a complete probability space with a right-continuous filtration , where . At time , describes the information available. Let be an integrable, strictly positive, -measurable random variable. Let be a strictly positive, bounded, -measurable random variable. Both positivity statements are almost sure.
The unknowns are real-valued stochastic processes and . The forward equation starts from and accumulates :
The backward equation sets equal to the conditional mean, given current information, of a future integral and the terminal input:
These are equations (3.10)–(3.11) of the paper. Their coefficient functions are and , each with Lipschitz constant for the paper's sum norm on pairs. The associated linear coefficient matrix is nonsingular. A solution is sought in for each component: the expected time integral of its absolute value is finite, and the equations hold in that space. This is the same integrability regime used to state the coupled system in §3 (Antonelli 1993, p. 785).
The terminal value is the random variable . Conditional-expectation processes in the intermediate identities are denoted and . Jointly measurable versions are used when these processes appear inside time integrals.
For any positive horizon, the paper derives an equation for in terms of , a weighted future integral of , and . With the sign consistent with the preceding display, the identity is
The printed equation (3.12) places inside the negative conditional expectation. That is inconsistent with both the preceding display and the next closed form; the formal statement uses the consistent sign and records the discrepancy (Antonelli 1993, p. 792).
The remaining intermediate targets are the paper's closed form for , equation (3.13) for , and the terminal-mean relation:
The last identity is stated without division, so it also has meaning when . These identities give the milestones in the order they occur on p. 792.
At the specific horizon , the coupled equations have no solution:
Strict positivity makes the right side of the mean identity positive, while its left side vanishes. The statement is a nonexistence result for the same broad solution class as the paper, rather than a claim about a narrower pathwise class.
Example 2 shows that a nonsingular coupling can still lose existence at a finite horizon. Thus the obstruction exhibited by the earlier singular example is not explained by singularity alone. The example also marks a limitation of replacing the paper's smallness condition with the assumption that the Lipschitz constant is merely finite. At and , the product exceeds one, as the paper notes (Antonelli 1993, p. 791).
A completed formalization would connect conditional expectations, jointly measurable time-indexed versions, and integration in in a reusable Lean development. The paper proves the mathematical result. This mission asks for machine-checked statements and proofs of its intermediate identities and nonexistence conclusion; it does not claim that the result is an open mathematical problem.
The main challenge is that the equations are equalities of integrable processes, not pointwise equalities at every time and outcome. A value assigned to by an arbitrary representative of an class is uncontrolled, so the terminal value must instead be reconstructed from the forward integral. Conditional expectations are defined only up to almost-sure equality at each time, yet the subsequent formulas integrate their time-indexed versions. This requires a jointly measurable version and careful movement between almost-sure statements at fixed times and statements.
There is also a printed sign inconsistency in (3.12). Propagating that sign would contradict the later sine-cosine formula. Finally, the paper's quotient formula for cannot be used at , because its denominator vanishes there. The undivided mean identity is the meaningful target at the critical horizon.
Time is represented by , and all integrals over time use ; for Lebesgue measure this agrees with the paper's ordinary time integrals. The ambient probability measure is a probability measure, and the filtration satisfies right continuity and completion at time zero. The two unknown processes are jointly measurable and have finite lower-integral norms. A solution uses a jointly measurable version of the conditional-expectation process, with each conditional-expectation argument explicitly integrable. The terminal is defined from and , independently of an arbitrary endpoint value of .
The source calls and positive; the formalization reads this as strict positivity almost surely, because allowing both to vanish admits the zero solution. is integrable as required by the standing assumption on in §3; remains bounded as Example 2 states. The four intermediate identities are stated for general , while only the main result fixes . Their process equalities hold in , and the terminal identity holds almost surely. This keeps the target from becoming true simply because endpoint representatives can be chosen freely.
The needed development includes product measurability, conditional expectation, Fubini's theorem, time integration, and the trigonometric identities in the closed form. The and version definitions can be reused for other coupled systems with deterministic time integrators. Contributions that establish the intermediate identities under the stated integrability assumptions, or develop the corresponding measurable-version tools, support the goal directly.
The trust-region subproblem — minimizing a quadratic, possibly nonconvex, over a Euclidean ball — is the inner step of every trust-region method for nonlinear optimization, and it also appears in regularized least squares and in the analysis of quadratic constraints. It is one of the few nonconvex problems whose global minimizers are characterized exactly: by the classical results of Moré and Sorensen (1983) and Gay (1981), a feasible point is a global solution if and only if it satisfies the Kuhn–Tucker conditions with a multiplier that makes the shifted matrix positive semidefinite.
Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998)) solve the problem with DCA, a descent method for difference-of-convex programs. DCA converges to Kuhn–Tucker points, and a Kuhn–Tucker point need not be a global solution. Section 4.2 of the paper closes this gap: it tests a Kuhn–Tucker point for global optimality with one eigenvalue computation, and when the test fails it writes down, explicitly, a feasible point with strictly smaller objective value from which DCA can be restarted. The resulting algorithm GDCA alternates DCA runs and restarts. This mission formalizes that restart construction.
Let be a real symmetric matrix, and . Write for the Euclidean inner product and for its norm. The trust-region subproblem (Q1) is
A point is a Kuhn–Tucker point of (Q1) with multiplier when
In Lean, is EuclideanSpace ℝ (Fin n), is a self-adjoint continuous linear operator on it, is quad A b, and the four conditions are IsKKT A b r xs lamStar.
Let be an eigenpair of : and . If then
so is a direction of negative curvature of the shifted matrix. For a direction and , the restart step of (23) is the nonzero root of , so that lies on the sphere (Lean: restartGamma w xs r s, with a sign choosing between the two roots when ).
This is the "Summing up" claim of §4.2 (p. 493). It asserts only the existence of a better feasible point; the explicit construction is spread over the milestones.
A companion item records the paper's remark that, for , the root of (23) with the larger gives the smaller .
The restart claim turns a local method into a global one. Combined with the convergence of DCA to Kuhn–Tucker points (Theorem 4.1 of the paper) and the global-optimality characterization of (Q1), it shows that each DCA run either ends at a certified global solution or yields a feasible point that strictly improves on it, with the improvement given in closed form from one eigenvector. The construction is elementary, but its case analysis — the sign of , whether the constraint is active, whether the eigenvector is orthogonal to — is exactly where an informal argument can go wrong, and the printed (b.2) bounds contain two errors (see Formalization scope).
The result is proved in the paper; to our knowledge none of it has a machine-checked proof. The mission produces a checked version of the case analysis with the corrected constants, and reusable facts about quadratics on the Euclidean ball (Lemma 4.2, the step to the sphere along a negative-curvature direction) that apply to any trust-region method.
The obvious argument — move from along the negative-curvature eigenvector until the boundary is reached — fails in one case. When and , the line leaves the ball for every , so no step along is feasible. The paper repairs this by tilting towards , and the tilt must keep the curvature negative while making the direction non-orthogonal to ; the admissible range of the tilt depends on the signs of and . A second subtlety is that the identity needs the term of Lemma 4.2 to vanish, which uses complementarity when and when the constraint is active.
All statements live in namespace TaoAnDCA.Restart on EuclideanSpace ℝ (Fin n), with a continuous linear operator and symmetry the hypothesis IsSelfAdjoint A; throughout. The objective quad is the bare quadratic, with feasibility stated separately.
Conventions and disclosed deviations from the page:
A trivializing formalization is ruled out: the goal's hypothesis is the eigenvalue test , never " is not a global solution", which would make the conclusion a restatement of the hypothesis.
No infrastructure beyond Mathlib's inner product spaces is needed. Contributions welcome: proofs of the milestones, and of the goal from them.
In the periodic-review inventory model with lost sales, demand that cannot be met from stock is lost rather than backordered. With a positive order lead time the state of the system is a vector of length : on-hand stock plus the orders still in the pipeline. This model is standard in retail, where a customer facing an empty shelf buys elsewhere. Its optimal policy is not a base-stock policy and depends on the whole pipeline vector, which makes it much harder to analyse than the backorder model.
A basic question for any stochastic inventory model is how its optimal cost responds to uncertainty in demand. For the backorder model it is classical that more variable demand costs more (Song 1994). Zipkin's paper (Oper. Res. 56(4), 2008, 937–944) recasts the lost-sales model in a transformed state in which the optimal cost functions are L-convex. Its §5 uses this structure to prove the lost-sales analogue: if demand becomes more variable in the convex order, the optimal cost does not decrease. The paper presents this as new in the lost-sales setting.
Timeline of the structural results the mission rests on:
The order lead time is a positive integer . The cost factors are the unit procurement cost , the unit holding cost , the unit lost-sales penalty and the discount factor . Demands in different periods are independent and nonnegative, with a common law. The paper treats states and orders as continuous.
Transformed state. A state is a vector , where is the stock on hand plus all orders due to arrive or more periods hence, and by convention. So is the inventory position and is the stock on hand. The state space is
The action is , where is the order quantity, and is the all-ones vector. After demand , the next state is
Costs and recursion. The end-of-period holding and penalty cost is , and its expectation given on-hand stock is . The optimal cost functions satisfy
with . This is the paper's recursion (1)–(2), written in the state .
Program (4). Fix a demand . Choosing the next stock level , with and , gives
Here is the leftover stock and the unmet demand.
Parametric demand. The demand depends on a real parameter , with law , and is the optimal cost under . A random variable is smaller than in the convex order if for every convex for which both expectations exist. This forces equal means and a variance that does not decrease.
If is increasing in with respect to the convex order, then for all and all ,
Theorem 11 is a comparative-statics statement: replacing demand by a mean-preserving spread cannot lower the optimal cost from any starting state, at any horizon. It justifies valuing variance reduction in lost-sales systems, for example forecasting or demand pooling, without solving the high-dimensional dynamic program. The induction pattern of the proof transfers to other parametric questions about the model; §6 of the paper notes that the parametric analysis remains valid in several extensions.
The paper proves Theorem 11 in a few lines on top of Theorem 4. No machine-checked proof of the result or of its structural prerequisites is known: neither the lost-sales recursion in the transformed state nor its convexity is formalized. A complete development checks the measure-theoretic steps the paper leaves implicit: that the optimal costs are finite, the existence of the expectations, and the passage from convexity in on to the convex order's test functions on .
The argument looks immediate: the costs are convex, so the convex order should apply directly. It does not. The function to which the convex order must be applied is the end-of-period cost as a function of demand. In recursion (1) that function is , where the next state depends on through the kink . Convexity of alone does not make this composition convex in . The paper avoids the issue by passing to program (4), where the amount of demand filled is a decision. That requires two facts: that selling as much as possible is optimal (milestone 1), and that the program is jointly convex in state, action and demand (milestone 3), which needs convexity of on all of (milestone 2). A second difficulty is analytic: the optimal costs are defined by infima and expectations, and one must show that these are finite and integrable before any order comparison applies.
Fin L → ℝ with 0-based indices matching the paper. is the helper vext. is the set of antitone, nonnegative vectors.fbar … (μ φ) k v.StochasticOrders.Convex.ConvexOrder (Shaked–Shanthikumar (3.A.1)), applied to the identity on . Equal means are a consequence and are not assumed.Ruled out. Value functions that collapse to a junk constant would make Theorem 11 trivially true. This is excluded because the recursion is defined, not assumed, and every cost and demand hypothesis is imposed for every . Replacing the convex order by "variance nondecreasing", by the increasing convex order, or by test functions convex only on changes the theorem and is not accepted.
Infrastructure and contributions. A complete development needs:
The model file is shared in shape with the series' missions 1 (L-convexity) and 2 (policy bounds), and its convexity lemmas are reusable for other parametric comparisons of the lost-sales model. Proofs of any milestone, and alternative arguments that bypass program (4), are welcome.
Network design problems often ask for a cheap spanning tree in which no vertex is overloaded: in multicast and overlay networks the degree of a node bounds the number of copies it must forward, and in physical networks it bounds the number of ports. The minimum bounded degree spanning tree problem asks for a minimum-cost spanning tree whose degrees respect given bounds. Deciding whether a graph has a spanning tree of maximum degree 2 is already the Hamiltonian path problem, so exact solutions are out of reach, and the question becomes how little the bounds and the cost must be relaxed.
Some problems also impose lower bounds: a vertex that must serve as a hub, or a leaf-avoidance requirement, asks for degree at least . Singh and Lau (STOC 2007) showed that the iterative rounding method they used for upper bounds extends to both kinds at once: a spanning tree of cost at most the LP optimum whose degree at every vertex lies in .
Timeline. Fürer and Raghavachari (1994) found a spanning tree of maximum degree at most in the unweighted case. For costs, Goemans (FOCS 2006) obtained cost at most OPT with degrees at most . Singh and Lau (STOC 2007) improved this to , which is the best possible additive violation unless P = NP, and gave the extension to lower and upper bounds formalized here. The journal version appeared in J. ACM 62(1), 2015.
Let be a finite simple graph with edge costs ; no sign or triangle inequality is assumed. Let be a forest on with no edge in common with . A set is an -tree if is a spanning tree of , and is the number of edges of at . Integer lower bounds are given on and integer upper bounds on . The minimum bounded degree connecting tree problem asks for a cheapest -tree with on and on ; with it is the spanning-tree problem.
The supernodes are the vertex sets of the components of , isolated vertices included, and is the family of unions of supernodes. For , and are the edges with both endpoints in , the edges with exactly one endpoint in , and . The linear relaxation LP-MBDCT minimizes subject to
MBDCT Algorithm2 (Figure 5 of the paper) repeats: if is a spanning tree, stop; otherwise take a basic optimal solution , delete the edges with , move one edge with (if any) into and lower and by one at its endpoints, and otherwise remove from and one vertex whose support degree is at most two.
For every well-formed instance whose LP is feasible, MBDCT Algorithm2
The statement fixes no constants beyond the paper's , and it is uniform over every choice of basic optimal solution, 1-edge and removed vertex.
In the order the proof uses them: Lemma 5.3 (a basic solution is determined by a laminar family of tight sets and tight lower and upper degree rows, with ); Claims 5.4, 5.7, 5.8 and 5.9 (special supernodes, cut sizes, the value on the edges between the members of , and when a set is special); Lemma 5.6 (every set of keeps at least three tokens, exactly three only if it is special or ); and Lemma 5.1 (a basic solution has an edge with or a vertex of with support degree two).
The theorem gives, in one algorithm, a tree that is no more expensive than the LP lower bound and whose degrees miss both bounds by at most one. For the pure upper-bound problem it implies the guarantee, which cannot be improved to unless P = NP, since a Hamiltonian path is the case . With lower bounds it also covers prescribed minimum degrees.
The result is proved in the paper; no machine-checked proof of it, or of any iterative rounding analysis, is known to exist. No platform item treats bounded-degree spanning trees or iterative rounding; the nearest related item is the open Williamson–Shmoys minimum-degree spanning tree local-search goal, which concerns a different, unweighted problem. Formalizing this mission requires the extreme-point structure of the spanning tree polytope with degree constraints (uncrossing to a laminar family), the token counting argument, and the induction over the algorithm's recursion, all of which are reusable for other iterative rounding results.
The obvious argument rounds an optimal LP solution once. It fails: an optimal vertex may be entirely fractional, and no single rounding keeps both the cost and the degrees. The algorithm instead re-solves the LP after each change, and its correctness rests on Lemma 5.1, that every extreme point of the current LP has an integral edge or a vertex with support degree two. That lemma is a counting statement about extreme points: the rank bound from a laminar basis must be contradicted by a token distribution. With upper bounds only, every set of the laminar family can collect four tokens. With lower bounds a set may collect only three, and the proof must characterize those sets (special sets, Definition 5.5) and show by linear independence that the remaining cases cannot occur. A second difficulty is that the guarantee concerns the final tree after many iterations, so the degree accounting must survive the changes of , , , and along the run.
Vertices form a Fintype; edges are elements of Sym2 V with no loops, and , are finite sets of edges with acyclic and disjoint from . LP vectors are functions on Sym2 V that vanish off . Right-hand sides are computed in , degree bounds are integers, and the subtour rows range over nonempty (at the literal row would make the LP empty). A basic solution is a feasible that is the only vector on satisfying with equality every constraint tight at , including the tight rows . Supernodes are never contracted: the paper's contraction of a supernode with one active vertex is a proof device, and all of §5.1's notions are stated on the original instance.
The paper's loose phrases are made explicit as follows.
Two trivializations are ruled out. Existence of a cheap tree with degrees in is not the target: the statement is about the algorithm's outputs and quantifies over all of them. And a run that never terminates does not satisfy the goal, which requires a run to exist and every run to be bounded.
Contributions are welcome at every level: the laminar uncrossing argument (Lemma 5.3), which is reusable for any spanning-tree LP with degree rows; the counting claims; and the invariants of the recursion.
A G/GI/N queue has identical servers, a general arrival process, a first-come-first-served waiting room and i.i.d. service times with a general distribution of mean . In the Halfin–Whitt regime the number of servers grows while the traffic intensity approaches at rate ; this is the standard asymptotic model for large call centers, where a positive fraction of customers wait but waiting times are short. Halfin and Whitt (Oper. Res. 1981) obtained a diffusion limit for exponential service times. Reed (arXiv:0912.2837, Ann. Appl. Probab. 2009) proved the corresponding limit for general service times: the centred and scaled queue length converges (Theorem 5.1) to the solution of a nonlinear stochastic convolution equation, (5.33) below.
Equation (5.33) is written in terms of an infinite-server limit, and it is not evident from its form that it reduces to the Halfin–Whitt diffusion when service is exponential. Section 5.5 of the paper gives a second representation, Corollary 5.2, in which the convolution against is replaced by a convolution against the renewal function of . With exponential service the renewal function is , and the representation becomes the Halfin–Whitt diffusion. This mission formalizes Corollary 5.2 and the renewal-theoretic steps of its proof.
Timeline. Halfin–Whitt (1981): exponential service, diffusion limit. Reed (2009): general service with finite mean; Corollary 5.2 links the general limit back to 1981. Karlin–Taylor (1975) and Ross (1983): the renewal-type equation and the renewal equation that the proof cites.
Let be a probability measure on with mean (the service-time law), its distribution function and its tail. The equilibrium distribution is
Let be the -fold convolution of (the law of the th renewal epoch ). The renewal measure is and the renewal function is , the expected number of renewals by time .
A path is càdlàg on if it is right continuous at every with finite left limits at every ; only its values on matter. Fix a càdlàg driving path (in the paper , (5.40)) and . Write and . The two equations are
All Stieltjes integrals are over the closed interval .
For every service law , every càdlàg and every :
and (5.41) has a càdlàg solution that is unique on among càdlàg paths.
The result. Corollary 5.2 expresses the many-server diffusion limit as an equation that is linear in the driving process and whose only nonlinearity is the idle-server term . This is how the paper verifies that its general-service limit agrees with Halfin and Whitt's for exponential service, and the paper's sequel interprets the integral term as the limiting idle time of the servers. Uniqueness in (5.41) also yields the paper's remark that , the solution of (5.41).
The formalization. The result is proved in the paper, but only partly written: the printed proof shows that the solution of (5.33) satisfies (5.41), while the converse and the uniqueness are asserted. The mission states both. It also produces, independently of queueing, the renewal measure of a law on with possible atoms, its finiteness on bounded sets, the renewal equation and the solution of renewal-type equations, and the identity ; none of these is in Mathlib or published on the platform. To our knowledge nothing in this mission has a machine-checked proof.
The forward direction is formal once (5.42)–(5.43) is available, but (5.42)–(5.43) itself needs the renewal measure to be finite on bounded intervals when may have an atom at , and the uniqueness half needs an argument that does not assume the kernel has mass below one on any window starting at . The converse direction, (5.41) (5.33), cannot be read off the printed proof, because (5.41) is not an equation of renewal type in . The uniqueness of (5.41) is not a contraction argument either: the atom of at has mass , which may exceed , so a naive Picard estimate on fails.
negPart.BellmanDP.Inventory.renewal_equation_exists_unique (a renewal equation with a density kernel of mass below ); ChenWhitt93.Reflection.Basic (càdlàg paths on ). Reusable output: the renewal measure, (5.39) and (5.42)–(5.43) serve any renewal-theoretic development. Alternative proofs of the converse and of uniqueness are welcome.Random partitions of the positive integers are the common language of population genetics, Bayesian nonparametrics and the theory of coalescent processes. When a sample of genes, customers or particles is grouped into classes, the grouping is a partition, and in most models its law is exchangeable: it does not depend on the labels. The best-known example is the Ewens sampling formula of population genetics (Ewens 1972); Kingman's representation theory (Kingman 1978) describes all exchangeable random partitions of .
Pitman's two-parameter family of exchangeable partitions, the partitions (Pitman 1995; Pitman and Yor 1997), contains Ewens' family as and is the partition counterpart of the two-parameter Poisson–Dirichlet distribution. Theorem 12 of Pitman 1999 shows that two natural random operations act on this family in a dual way: merging blocks of an partition according to an independent exchangeable partition (coagulation) and splitting each block of an partition by independent exchangeable partitions (fragmentation) produce the same joint law of a fine and a coarse partition. The paper uses it to describe the Bolthausen–Sznitman coalescent (Bolthausen and Sznitman 1998).
Timeline. 1972: Ewens' sampling formula, the case . 1978: Kingman's correspondence between exchangeable partitions and random mass partitions. 1995: Pitman introduces exchangeable partition probability functions and the formula (15). 1997: Pitman and Yor study the two-parameter Poisson–Dirichlet law. 1999: this paper proves the coagulation–fragmentation duality (Theorem 12) and its sharper converse, by reduction to an identity between explicit formulas. The duality is treated again in Pitman's lecture notes Combinatorial Stochastic Processes (2006).
A partition of a set is a collection of disjoint nonempty blocks whose union is the set. Write for the partitions of and for those of ; the restriction of to keeps the nonempty sets . carries the -algebra generated by the . Writing lists the blocks in increasing order of least elements.
A random partition of is exchangeable with EPF if for every and every partition of ,
For and the EPF is
with factors of and cancelled before evaluation when or . An partition is an exchangeable random partition with EPF .
Coagulation (Definition 5): for and , the -coagulation of has blocks . is a -coagulation of if, given , it is the -coagulation of for an independent with EPF . Fragmentation (Definition 11): is a -fragmentation of if, given , restricted to the -th block of equals restricted to that block, for independent with EPF . In Lean these are coag, frag, pdEPF and IsEPFLaw in LambdaCoalescent.CoagFrag.Setting.
For , , , the following are equivalent: (i) is an partition and is a -coagulation of ; (ii) is an partition and is an -fragmentation of . Formally, with laws of EPFs :
for every measurable .
Theorem 12 identifies one law of a nested pair of exchangeable partitions from both ends. Read from (i) to (ii), it shows that coagulating an partition by an independent partition yields an partition; read backwards, that an partition fragmented by partitions yields an partition. Through Kingman's correspondence it gives Corollary 13 on Poisson–Dirichlet laws, and with it connects the two-parameter family with Ewens' family. In the paper it is the tool for describing the Bolthausen–Sznitman coalescent through Poisson–Dirichlet laws. The sharper form shows the parameter relations (64) are forced.
The theorem has been proved since 1999. What this mission adds is a machine-checked development: exchangeable random partitions of with their EPFs, the coagulation and fragmentation kernels, and the reduction of identities between laws on to identities between finite-dimensional formulas. None of these objects is in Mathlib, and no formalization of the duality is known.
The algebraic heart, the EPF identity, is a finite computation with rising factorials. The difficulty is measure-theoretic and combinatorial. A law on must be pinned down by its values on the cylinder events . Computing under the coagulation kernel requires that the blocks of meeting are exactly the first blocks in order of least elements, and that the induced partition of has law given by the EPF; under the fragmentation kernel it requires the independence of the and that the restriction of an exchangeable partition to an arbitrary finite set (not an initial segment ) is governed by the same EPF. The converse in Lemmas 34 and 35 needs the bookkeeping that the formula on refining pairs exhausts total mass. Lemma 9 is an existence theorem for a projective family of laws, which the paper cites rather than proves.
A partition of is an equivalence relation on Lean's (PInf := Setoid ℕ), a partition of one on Fin n; labels shift by one, which preserves the order of least elements, and block indices are 0-based. The -algebra on PInf is generated by the coordinates , equivalently by the . Coagulation is stated with (Definition 5's case ). The EPF is the cancelled form
equal to (15) for ; this is needed because at . Conditional laws "for all " are encoded as joint laws, and equalities of laws are stated on preimages of measurable sets, so no Measure.map of an unproved-measurable map appears. Fragmenting partitions are one sample of Measure.infinitePi (fun _ => κ). In the sharper form, is written as , since PAR allows .
Not formalized: the stick-breaking characterization (12)–(13) in Lemma 9, Corollary 13 and Kingman's correspondence, and the auxiliary fact "", which as printed fails at .
A formalization in which no measure satisfies IsEPFLaw (pdEPF α θ) would make Theorem 12 and Lemmas 34–35 vacuous; Lemma 9 rules this out and must be proved for the parameters used, not assumed.
Infrastructure needed: cylinder-set uniqueness on PInf, the law of the restriction of an exchangeable partition to a finite set, block enumeration by least elements, and rising-factorial algebra (ascPochhammer). The partition, EPF and kernel definitions are reusable for any work on exchangeable partitions, Chinese restaurant processes or -coalescents. Proofs of Lemma 9, of Lemmas 34–35 and of the EPF identity are each welcome as independent contributions.