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 trust-region subproblem asks for the minimum of a quadratic function over a Euclidean ball,
with a real symmetric matrix that may be indefinite. It is solved at every iteration of a trust-region method for nonlinear optimization (Moré and Sorensen 1983; Conn, Gould and Toint 2000), so a method for it is used many thousands of times in a single run. Classical methods based on factorizations of do not scale to large sparse problems.
Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998)) apply to their DCA, a general algorithm for d.c. programs (minimizing a difference of two convex functions). For a suitable splitting of the objective, one DCA iteration is a matrix–vector product followed by a scaling onto the ball. This mission formalizes the convergence theorem for that iteration (Theorem 4.1 of the paper), together with the general DCA convergence results it is derived from (Theorem 3.7 and the Appendix).
Timeline (as recorded in the paper's introduction):
Let with inner product and norm . For a function , , and is the set of proper, lower semicontinuous, convex functions. For the conjugate is , and the subdifferential at is . The function is -convex () if is convex.
A d.c. program is with , under the convention and the standing inclusions , . Its dual objective is . The simplified DCA builds two sequences from :
For let (), its indicator, and . Fix with positive semidefinite and split as in (16):
The resulting DCA starts at any and, with , sets if and otherwise; equivalently . A Kuhn–Tucker point of is an with some such that , and .
For every run of the DCA,
decreases to a limit , , and every limit point of is a Kuhn–Tucker point.
In attack order:
The equality case of Theorem 3.7(i) and Theorem 3.7(ii) (the dual descent) are included as further draft theorems.
Theorem 4.1 makes the DCA a descent method for whose accumulation points satisfy the first-order conditions. That property is what the paper's restarting procedure (§4.2) builds on: at a Kuhn–Tucker point that is not a global minimizer, one eigenvector computation gives a better feasible point, and the DCA reaches a global solution after at most restarts, where is the number of distinct negative eigenvalues of . Theorem 3.7 is the convergence theorem for the DCA on general d.c. programs, used throughout the later DCA literature.
All of these results are proved in the paper. As far as is known, none of them has a machine-checked proof: Mathlib has convex conjugates and subdifferentials in pieces, but no d.c. duality, no DCA and no analysis of the trust-region subproblem. This mission produces that development: a statement layer for d.c. programming with extended values, a formal proof of the general descent and criticality theorem, and its specialization to .
Every inequality of the analysis runs over . The differences and need the paper's convention , and the finiteness of each value along a run has to be derived from the standing inclusions. The hard step is the passage to limit points in Theorem 3.7(iv). Lower semicontinuity of , and gives only one-sided inequalities at a limit point, while the theorem asserts equalities of values there. The naive argument of passing to the limit in and fails, because and need not have the same limit unless . For the specialization needs boundedness of the iterates, finiteness of , and the subdifferential of the indicator of the ball. None of these is a hypothesis of Theorem 4.1, so each must be proved from the run.
is EuclideanSpace ℝ (Fin n). Extended values are EReal, and every d.c. difference is dcSub g h x, equal to when and to otherwise, because Mathlib's EReal has . , subgradients and the conjugate come from published platform definitions (IsProperClosedConvex, IsSubgradient, CondatPD.FinDim.conj). The modulus of strong convexity is never defined as a supremum. Statements take explicit constants with " is -convex", which is what the paper requires of them. Hypotheses "" become . The matrix is a self-adjoint continuous linear operator. " is the smallest eigenvalue of " is encoded by quantifying over every with . A limit point is a cluster point. The objective is outside , and the run starts from an arbitrary , as on the page. Statements involving are for . Theorem 3.7(iv)'s limit identity is stated along a common convergent subsequence, as in its proof.
Ruled out: the goal is stated for the explicit iteration a)/b) of p. 490, never for an abstract run assumed to satisfy Theorem 3.7, and it carries no hypothesis of boundedness, finite or convergence. A run predicate that no sequence satisfies would make everything vacuous, and a sanity file exhibits concrete runs.
Needed infrastructure: the Fenchel–Young equality and its equality case for functions in EReal, subdifferential inversion , strong-convexity versions of the subgradient inequality, and the normal cone of a Euclidean ball. These are reusable well beyond this mission and are welcome as separate contributions.
The newsvendor problem is the basic model of a one-period inventory decision: a seller orders units at unit cost before a random demand is observed, and sells units at unit price . A perfectly rational newsvendor orders the critical fractile , where is the distribution function of . Laboratory experiments (Schweitzer and Cachon 2000; Bolton and Katok 2008) found that human subjects systematically deviate from : their orders are noisy and, on average, pulled toward mean demand.
Su (2008) explains these patterns with a model of bounded rationality taken from the logit choice literature (Luce 1959; McFadden 1981). The decision maker does not pick the best order; instead each order is chosen with probability density proportional to the exponential of its expected profit, scaled by a noise parameter . The resulting random order, the behavioral solution , is the object of the paper. For uniform demand it is a truncated normal and its moments are explicit (§4.1). For a general demand distribution there is no closed form, and §4.3 of the paper characterizes the moments of through a single function instead. This mission formalizes that characterization, Proposition 2.
Demand has a density : , for , and . For an order quantity , the expected sales are and the expected profit is (eq. (3))
The decision domain is the smallest interval containing the support of : the boundedly rational newsvendor may order any quantity between the smallest and the largest possible demand. The behavioral solution is the random order with density (eqs. (4), (11))
and for .
A family of densities forms an -dimensional exponential family if they have the form (eq. (10)); the are the natural parameters, the the sufficient statistics and the log-partition function. Su observes that the choice densities are of this form with , natural parameters and , statistics and , and
In the Lean development these objects are IsDemandDensity f, expMin f, nvProfit f p c (), decisionDomain f (), logitDensity S (nvProfit f p c) β (), logitExp S u β g (the expectation ) and logPartition f η₁ η₂ (), all in the namespace BoundedNV.ExpFam.
With and , both partial derivatives of exist at , and
Proposition 2 turns the computation of the expected order and the expected profit of a boundedly rational newsvendor, which are integrals against the density (11), into the differentiation of one function of two variables. The paper uses this in two ways (p. 575): moments of can be approximated numerically from finite differences of , and can be estimated from aggregate laboratory data by the method of moments, choosing so that at matches the observed average order.
The result is classical in structure: (13) is the standard identity for exponential families (see, e.g., Lehmann and Casella 1998). What the formalization adds is the verification that the identity applies to this particular family under the paper's hypotheses, including demand distributions with unbounded support, where the decision domain is a half-line and the integrals are improper. To our knowledge, no part of the paper has been formalized before.
The identity (13) rests on differentiating under the integral sign in (12). The textbook justification requires the natural parameter to lie in the interior of the natural parameter space, together with a dominating function for the derivative of the integrand. Neither is on the page: the paper states the Fact for exponential families in general. For bounded the domination is immediate; for unbounded it is not, and the natural first idea, to bound by the mean of , fails because the paper assumes no finite mean. The required control comes instead from the growth of , which is sublinear in , against the linear decay with . This must be established uniformly for parameters in a neighborhood of .
All quantities are real. Integrals are Lebesgue (Bochner) integrals over or over , and partial derivatives are derivatives of the one-variable sections and . The conventions committed to are:
Junk values ruled out. In Lean, , , the integral of a non-integrable function is , and deriv of a non-differentiable function is . If the statements used these silently, every identity could hold because every term vanishes. The milestones therefore assert integrability and positivity of the normalizer and that integrates to . Every derivative is stated with HasDerivAt, which asserts differentiability.
The Fact (13) is not formalized for abstract exponential families, whose hypotheses the page does not state; it is specialized to this family. The method-of-moments remarks after Proposition 2 and the empirical §5 are not part of the mission.
The infrastructure needed is differentiation of parametric integrals over unbounded domains (Mathlib's hasDerivAt_integral_of_dominated_loc_of_deriv_le) and elementary facts about : continuity, for , and sublinear growth. The last of these is reusable for any newsvendor model with general demand. Contributions of proofs for each milestone, and of a lemma establishing the uniform domination near , are welcome.
The source is the published article in Manufacturing & Service Operations Management (2008); page numbers are the journal's.
A d.c. program minimizes a difference of two convex functions,
with and proper, lower semicontinuous and convex. Every twice continuously differentiable function is d.c. on compact convex sets, so the class covers most smooth nonconvex optimization, and it includes the trust-region subproblem that motivates the paper of Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998) 476–505). Global minimization of a d.c. function is NP-hard in general, so practical algorithms, in particular the DCA of the same authors, compute local minimizers and critical points. The theory of local optimality is therefore what those algorithms can actually certify.
D.c. programs come with a dual program built from conjugate functions, , which has the same optimal value. Toland (J. Math. Anal. Appl. 66 (1978)) showed that global solutions correspond under this duality. For local solutions the correspondence is subtler, and §3.2 of the paper gives conditions under which a local minimizer of the primal produces one of the dual. Toland's earlier version required to be differentiable on the whole space; Corollary 3.5 of the paper needs only a condition at the single point .
Let with inner product and norm ; the dual space is identified with . Functions take values in . is the set of proper lower semicontinuous convex functions. For :
Differences are taken under the convention . Throughout, satisfy the standing inclusions
A point is a local minimizer of if is finite and there is a neighbourhood of with for all (display (4) of the paper); under the convention this is the same as requiring it for . It is a critical point if . The set collects the points satisfying the classical necessary condition. "Local minimizer of " is the same definition applied to the dual pair .
Let have an open neighbourhood with for all , and let . If
then is a local minimizer of .
then on , and is a local minimizer.
Corollary 3.5 lets a local solution of the primal d.c. program be read off as a local solution of the dual one. This matters when the dual program is easier to handle locally, and it is the local counterpart of the global duality of Theorem 3.1. Theorem 3.2(ii), which the authors present as new, is a sufficient condition for primal local optimality stated through the dual objective. Corollaries 3.3 and 3.4 are the sufficient conditions on which the convergence analysis of the DCA rests: they explain when the critical points that the DCA reaches are in fact local minimizers, for instance when is polyhedral.
These results have been proved on paper since 1997–1998 and are not open. To our knowledge none of them has a machine-checked proof. Formalizing them produces the local optimality theory of d.c. programming on top of an extended-real convex analysis layer (conjugates, subdifferentials, the convention ), which the sibling missions of this series (global optimality, the DCA for the trust-region subproblem) can reuse.
Theorem 3.2 and Corollaries 3.3–3.4 are short arguments built on the Fenchel–Young inequality and its equality case. The obstacle in the goal is that the dual application of Theorem 3.2(ii) needs its hypothesis on a whole neighbourhood of , while (12) is a condition at the single point . Bridging this requires the upper semicontinuity of the subdifferential of at an interior point of its domain. That rests on two facts: is continuous and locally bounded there, and the subdifferential is locally bounded with closed graph. Neither is in Mathlib for extended-real functions. The dual application also needs to satisfy the standing assumptions, which needs biconjugation for , again in the extended-real setting. A first attempt that works only with finite-valued convex functions does not apply: is typically outside a bounded set.
EuclideanSpace ℝ (Fin n) and values are EReal. , and the conjugate are the published definitions ThreeOpSplitting.ConvexRates.IsProperClosedConvex, InertialFB.IFB.IsSubgradient and CondatPD.FinDim.conj (an EReal supremum over all of ). The subgradient predicate requires the base point to lie in the domain, as the paper does.dcSub, which returns whenever . Mathlib's EReal subtraction is not used for it, because Mathlib sets , and that would make every point outside a global minimizer with value .IsLocalMin is not used), and the goal's conclusion includes the finiteness of .DCStanding and are a hypothesis of every item.EReal-valued functions;In a strategic game, players may repeatedly change their own choices when a change raises their payoff. This gives a simple model of decentralized adjustment: each move uses the current profile and one player's immediate incentive. The central question is whether such adjustment can continue forever. Monderer and Shapley introduced the finite improvement property (FIP) to state that every sequence of strict unilateral improvements ends. Their 1996 paper, pp. 128–130, relates that dynamic property to a real-valued function on the game's strategy profiles.
An ordinal potential records each player's strict preference between two of their strategies when the other players' strategies are fixed. Such a function is useful because it assigns one common direction to the players' individual choices. The paper gives a two-player game that has the FIP but no ordinal potential, then introduces a weaker, generalized ordinal potential and proves that it captures exactly the finite games with the FIP (Monderer and Shapley, pp. 129–130). This mission isolates that characterization from the paper's other results about exact potentials and congestion games.
Let be a finite set of players. Player has a strategy set , and a strategy profile selects one strategy for each player. The payoff function gives player 's payoff at a profile. Write for the profile obtained by replacing player 's strategy in by . A finite game has finite for every player. These are the paper's conventions at the start of §2 (p. 127).
A path is a sequence of profiles in which each step changes exactly one player's strategy to a different strategy. It is an improvement path when the moving player strictly increases their payoff at every step. The game has the FIP if no infinite improvement path exists. Thus the property concerns paths of any length and every allowed choice of deviator, rather than the behavior of one selected update rule (p. 128).
An ordinal potential satisfies
for every player , opponents' profile , and . A generalized ordinal potential replaces this equivalence by the forward implication only. The two notions are distinct, as the game on p. 129 shows (equations (2.1) and (2.3), pp. 127, 129).
For every finite game ,
This is Lemma 2.5, p. 129. It specifies a precise characterization rather than choosing a particular potential or a particular update schedule.
The milestone list follows the paper's statements: Lemma 2.3 says a finite ordinal potential game has the FIP; the proof of Lemma 2.5 says the finite-improvement reachability relation is transitive under the FIP; and it concludes that the whole strategy-profile set can be represented by a real function increasing along that relation (pp. 128–130). Corollary 2.6 and the explicit game record the boundary between ordinal and generalized ordinal potentials: under its distinct-payoff condition a finite game with the FIP has an ordinal potential, while shows that condition cannot simply be omitted (pp. 129–130). Lemma 2.1 and Corollary 2.2 concern equilibria: an ordinal potential game has the same pure equilibria as the game in which every player receives the potential, so a maximizer of the potential is an equilibrium, and every finite ordinal potential game has a pure-strategy equilibrium (p. 128).
The goal connects a property of all possible strict improvement paths to the existence of a single real-valued certificate on profiles. In a finite game, such a certificate describes a common direction for unilateral payoff gains, regardless of which improving player moves next. The distinction between ordinary and generalized ordinal potentials matters: an ordinary potential must also preserve indifference, whereas the FIP alone does not require that (Monderer and Shapley, p. 129).
The characterization is proved in the paper; the remaining work in this mission is a Lean proof of its faithful finite-game statement. The local platform index used for this proposal has no published theorem expressing this characterization. The definitions of improvement paths and improvement reachability can also support other formal results about game dynamics. The game serves as a concrete check on the strict distinction between the two potential notions.
The payoff vector itself does not give an immediate numerical order on whole profiles: each step compares one player's payoff, and the next step may involve another player. Finiteness rules out an endlessly increasing sequence only after a suitable profile-level ordering has been established. The converse direction therefore requires more than observing that each individual move helps its deviator. The paper's also rules out replacing the generalized potential in the goal with an ordinary ordinal one (p. 129).
Players form a finite Lean type ι with decidable equality; each player's strategies form a type Y i. A theorem about a finite game additionally assumes every Y i is finite. These types may be empty: in that case there is no strategy profile, and the corresponding FIP and potential statements retain their ordinary quantified meaning. No nonemptiness assumption is inserted into Lemma 2.5. Corollary 2.2 alone assumes every strategy set nonempty, which the page takes for granted: without it there is no profile and no equilibrium. An equilibrium point is a pure Nash equilibrium in the sense of the published definition AGT.IsPureNash (no player gains strictly by a unilateral deviation), and "P admits a maximal value in Y" in Lemma 2.1 is read as "P attains its maximum on Y". The finite player assumption follows the standing convention on p. 127; the finite strategy assumption is added only where the source says “finite game.”
The expression is Function.update y i x. IsStep requires one coordinate to change to a different value. HasFIP forbids an infinite natural-number-indexed path of strict payoff improvements, so it cannot be satisfied merely because each separately described finite path has finite length. A finite path stores its deviator at each step; the genuine-step condition determines that deviator uniquely. The same path bundle contains the paper's path sum and closed-path predicates for consistency across this paper's missions, although only finite improvement paths are used here. The relation ImprovesTo u x y means that a finite strict improvement path leads from to a distinct .
The necessary development comprises the two potential predicates, path and FIP definitions, the finite improvement relation, the transitivity and representation milestones, and the goal characterization. Contributions that prove these statements or simplify their proof dependencies are within scope. A definition that checks only finite paths, allows null steps, or confuses the one-way condition (2.3) with the two-way condition (2.1) would change the result.
In sequential prediction, several forecasters can issue different answers for the same instance. A master algorithm must combine their advice before the true label is known. Littlestone and Warmuth's Weighted Majority framework gives worst-case guarantees for this setting: the instances and labels need not come from a probability distribution. The paper first studies binary predictions and then allows real predictions and labels in the unit interval. The continuous version matters when the distance between a prediction and a label carries information that a binary mistake count discards. The formal target here is the paper's total absolute-loss guarantee for that continuous master, WMC (Littlestone and Warmuth 1994, §5).
The result is part of the paper's generalized analysis, which also covers a binary master WMG and a randomized master WMR. These algorithms share a range of allowed weight updates, but their predictions and losses differ. This mission isolates WMC's deterministic, continuous-label theorem and the numbered lemmas on which its statement rests. The finite-sequence convention is explicit in the paper's notations and assumptions (Littlestone and Warmuth 1994, p. 220).
Fix a finite nonempty pool of forecasters and a finite sequence of trials. At trial , expert predicts , and after the master predicts, a label is revealed. Expert has weight before that trial. Every initial weight is positive, and weights remain nonnegative. The total weight and weighted mean prediction are
WMC predicts . Its loss on the trial is the absolute error , and its total absolute loss is . Write and for total weight before the first and after the final update (Littlestone and Warmuth 1994, pp. 232–233).
WMC updates on every trial. For , it multiplies each weight by a factor in the interval
The factor may depend on both trial and expert. The paper permits any choice in this interval, so WMC denotes a class of runs rather than one fixed recurrence. Its convention is used when and an expert has zero error (Littlestone and Warmuth 1994, p. 233, eq. (5.1)).
For every run with positive final total weight, the target is the paper's explicit inequality
The bound uses the run's actual initial and final weights, so it applies whether the upper or lower permitted update factor was selected, or a factor between them. The finite-valued statement assumes ; the paper regards the bound as vacuous when the denominator of the logarithm is zero (Littlestone and Warmuth 1994, p. 236, Theorem 5.2).
Lemma 5.1 states for and , ensuring the update interval is nonempty. Lemma 5.2 states the logarithmic potential estimate under only the update's upper inequality, including the special case in which and a master's unit loss forces the final total weight to zero. Lemma 5.3 turns those same conditions into the displayed total-loss bound. Each is a separate milestone with the paper's statement and page provenance (Littlestone and Warmuth 1994, pp. 233–236).
The theorem controls the master's accumulated real-valued prediction error by an observable change in the total pool weight. It requires no distributional assumption on the trial sequence and no single choice of update factor. That breadth lets the same estimate be used for different update rules within the allowed range, while the explicit constant records the dependence on the algorithm's parameter. The paper also uses Lemma 5.3 in its analysis of WMR's expected loss (Littlestone and Warmuth 1994, pp. 236, 240).
The paper proves these results; this mission asks for machine-checked proofs of their exact Lean statements. Its definition of a permitted continuous run and its upper-update potential conditions can also support subsequent formalizations of WMG and WMR. Lemma 5.1, the potential estimate, and the final loss bound remain distinct proof targets so that a solver can use or improve the underlying analytic infrastructure without changing the goal.
A binary mistake indicator cannot express the magnitude of an error between two unit-interval values. The generalized update contains a real exponent, absolute values, and a range of legal factors. An argument that handles only a selected endpoint of that range would leave permitted WMC runs uncovered. A further boundary occurs at : an allowed update can reduce a positive weight to zero, and real logarithms in Lean have a defined value at zero although the paper's logarithmic bound is infinite there. The formal statements therefore distinguish the zero-final-weight clause from the finite-logarithm clause.
The pool is Fin n with and the trials are Fin t; an empty sequence of trials is allowed. Lean's trial index starts at zero, so w 0 represents and w t represents the weights after all trials. The inputs are the prediction array and label array. Instances are not stored separately because the theorem refers to them only through expert predictions. Values, factors, totals, and losses are real numbers. The run predicate requires positive initial weights, nonnegative weights, predictions and labels in , , and a permitted factor for every expert on every trial.
The theorem quantifies over every permitted run. A sorry-free local example exhibits a one-trial run with positive final weight, ruling out a globally empty run predicate. For positive final weight, the update conditions ensure earlier total weights are positive, so every weighted mean used in the loss has its intended denominator. The finite logarithmic conclusions assume positive final weight because Real.log 0 would otherwise introduce an unrelated total-function value. The definition layer supplies total weight, weighted mean, loss, base conditions, the upper-update conditions, and WMC runs; the proof development needs finite-sum and real logarithm inequalities from Mathlib. Contributions that establish the three numbered lemmas or the goal under this interface are in scope.
Bounds on the upper tail of a sum of independent random variables are used throughout probability, statistics, queueing and risk theory: they control ruin probabilities, the error of empirical averages, and the size of the largest deviations of random walks. The classical exponential inequalities (Bernstein, Hoeffding, Bennett) require the summands to be bounded or to have finite exponential moments of a fixed order. The polynomial bounds of Fuk and Nagaev only require finite power moments, at the price of a power-law rate.
Between these two regimes lie summands whose right tails decay like for a function growing faster than a logarithm — Weibull-type and other subexponential or superexponential tails. For such summands the natural size parameter is not a power moment but a generalized moment . Section 2 of S. V. Nagaev's survey Large deviations of sums of independent random variables (Ann. Probab. 7, 1979, doi:10.1214/aop/1176994938) develops bounds on in terms of these quantities. Theorem 2.5 of that section, attributed to S. K. Sakoyan and Nagaev, treats the case where has a positive nondecreasing derivative — the case of the paper — and gives a bound in product form whose exponential order is .
Let be a probability space and independent real random variables with distribution functions . Write
Let be differentiable with a derivative that is positive and nondecreasing; in particular is convex and increasing, and as .
For each summand define the generalized moment
and, for a real , the negative-part factor
The factor is always finite, since its integrand lies in ; may be infinite, and the theorem is meaningful only when every is finite. In Lean these objects are S n X, bg P X g j and bj P X g g' j s in the namespace NagaevLD.GenMoment.
For every ,
The statement holds for every , every distribution of the summands with finite , and every admissible ; no constant is hidden.
The proof of the paper passes through the following displays, all on pp. 767–768, with where indicated:
The bound separates the tail of into a product of one-summand quantities. For fixed and one has , so for large (the paper's (2.49)); compared with the elementary lower bound (2.50), this shows the exponential order is the right one when the right tails of the summands are of order . The only case where the right side does not depend on is , the classical Chernoff regime, of which the theorem is a generalization.
The result is a published theorem with a complete half-page proof; it is not open. As far as a search of the Prove2Me catalogue shows, no part of it has been machine-checked: the catalogue contains single-variable Chernoff bounds (Mathlib's measure_ge_le_exp_mul_mgf) but no bound in terms of generalized moments. The mission produces a formal proof of the theorem and, along the way, reusable statements about tilted truncated moments of independent sums.
Each step of the argument is short; the work is in carrying it through real-valued measure theory. The exponential Chebyshev step requires the moment generating function of a sum of independent variables to factor, which needs the integrability of every — a fact that here must be derived from the finiteness of and the bound on , not assumed. The supremum in (2.46) has to be identified as a maximum attained at , which rests on the convexity of on obtained from a monotone derivative. Finally the split of at must match the definition of exactly: a mismatch at the single point breaks the theorem.
The summands are X : Fin n → Ω → ℝ on a probability space, each measurable and jointly independent (iIndepFun); index in Lean is the paper's . Integrals over a set of are written as expectations restricted to the corresponding event, so no distribution functions appear. Probabilities are P.real, and is P.real {ω | x ≤ S n X ω}.
Committed conventions and disclosed additions:
sSup: (2.46) is stated for every upper bound of on , and (2.47) as IsGreatest.A complete development needs the factorization of exponential moments of independent sums (available in Mathlib as iIndepFun.mgf_sum), Markov's inequality, splitting a Bochner integral over an event and its complement, and the tangent-line inequality for a function with monotone derivative. Proofs of the milestones, alternative arguments, and lemmas on truncated exponential moments are all welcome.
Congestion games model situations in which agents choose sets of shared resources and the payoff of each resource depends only on how many agents use it: drivers choosing routes through road segments, jobs choosing machines, flows choosing links in a network. Rosenthal (A class of games possessing pure-strategy Nash equilibria, Int. J. Game Theory 2, 1973) showed that every such game has a pure-strategy Nash equilibrium, by exhibiting a single real function on strategy profiles whose changes track every player's unilateral payoff changes.
Monderer and Shapley (Potential Games, Games Econ. Behav. 14, 1996) isolated that property and called games having it potential games. Their Section 3 shows that the property characterizes congestion games: Rosenthal's argument gives Theorem 3.1 (every congestion game is a potential game), and Theorem 3.2 gives the converse up to a renaming of strategies. Potential games have since become a standard tool in algorithmic game theory (convergence of best-response dynamics, price of stability bounds, learning in games), and Theorem 3.2 is the reason that results proved for congestion games apply to all finite potential games.
A game in strategic form has a finite set of players , for each player a strategy set , the profile set , and payoff functions . For a profile and , is with player 's strategy replaced by . The game is finite if every is finite.
A function is a potential for (condition (2.2) with unit weights) if
and is a potential game if it has a potential (IsPotential, IsPotentialGame).
A congestion model has players , a finite set of facilities , for every player a set of strategies, each a nonempty subset of , and for every facility a vector , where is the payoff to each user of when exactly players use it. The associated congestion game has strategy sets and payoffs
Two games with the same players are isomorphic (IsIsomorphic) if there are bijections with for every player and profile .
Formally: for every finite set of players, finite strategy sets and payoffs admitting a potential, there are and a congestion model on the facilities , all of whose strategies are nonempty facility sets, whose congestion game is isomorphic to .
The milestones follow Appendix B of the paper.
Theorems 3.1 and 3.2 together say that, up to renaming strategies, the finite potential games and the congestion games are the same class. Consequently any statement about finite congestion games that is invariant under isomorphism (existence of pure equilibria, convergence of improvement dynamics, the structure of equilibrium sets) holds for all finite potential games, and conversely any potential game can be realized as a resource-sharing model. The representation is also the starting point of the later literature on the number of facilities needed to represent potential games, which the paper itself begins with a remark at the end of Appendix B.
Theorem 3.1 is already machine-checked on the platform, as Rosenthal's potential identity PriceOfStability.Harmonic.rosenthal_potential_change (Proved); it is included in this mission as a reference item. Theorem 3.2 is proved in the paper but has no machine-checked proof that we know of. The mission adds a formal statement of the theorem, of isomorphism of games, of congestion games as games in strategic form, and of the explicit construction of Appendix B; and, once proved, a verified converse to Rosenthal's theorem.
The theorem is an explicit construction, and its difficulty is bookkeeping rather than a single hard idea. The facility set is a product of Boolean cubes, one per player; each player's strategy is the set of facilities with a 1 in a given coordinate; and the facility payoffs are defined only at load and load , by two auxiliary vectors whose definitions involve a choice of representative. Showing that the resulting congestion game reproduces every payoff requires identifying, for every profile, exactly which facilities are used by one player and which by all players, and showing that the "load 1" facilities pick up precisely the part of that player cannot influence. The paper leaves the two key set identities as "it can be verified"; they are the milestones.
The construction as printed does not cover one player: with the vectors and are the same vector, defined twice. The theorem is still true for one player, and the formal goal does not exclude it, so a complete proof must treat that case separately.
ι with decidable equality; strategy sets are types Y i, finite in the goal ([∀ i, Fintype (Y i)]). is Function.update y i x. No nonemptiness of the strategy sets and no lower bound on the number of players is assumed.CongestionPoA.AsymSum.CongestionGame ι M (reference item): strategies i is the finite family and latency j k is the paper's , an arbitrary real number. No sign change is made; the published names "latency" and "cost" are only names. Values of latency at and above never enter (3.1).congestionPayoff G, whose strategy set for player is the subtype of G.strategies i. Because the isomorphism maps onto that subtype, the strategies of a player are distinct facility sets.Fin m for an existentially quantified , and nonemptiness of every strategy, which is part of the definition of a congestion model on p. 133 but not of the published structure, is a separate conjunct. Dropping it, or replacing "congestion game" by an arbitrary game whose payoffs equal , would make the goal a different, weaker statement; the formal goal does neither.FacilityConstruction) indexes the coordinates of player by itself instead of ; is passed as a full profile whose -th coordinate is ignored; and select a representative by choice, the chosen -th coordinate playing the role of the arbitrary in (B.4).Contributions welcome: proofs of the milestones, a proof of the goal (by the paper's construction, with the one-player case handled separately, or by any other construction), and general lemmas about transporting potentials along isomorphisms.
Monotone comparative statics asks when the optimal choice of a decision maker moves in a predictable direction as a parameter of the problem changes: when a firm facing a higher price produces more, when a monopolist facing lower costs sets a lower price, when a player in a game best-responds with a higher strategy to higher strategies of the others. The classical sufficient conditions, due to Topkis (Topkis 1978), are supermodularity of the objective in the choice variable and increasing differences in the choice and the parameter. Both are cardinal conditions: they can be destroyed by a strictly increasing change of the units in which the objective is measured, although such a change does not alter any optimal choice.
Milgrom and Shannon (Econometrica 1994) replaced these conditions by ordinal ones, quasisupermodularity and the single crossing property, and showed that the ordinal conditions are necessary and sufficient for the set of maximizers to be monotone in the parameter and the constraint set (their Theorem 4). This mission concerns the relation between the ordinal notion and the cardinal one: in which sense is a quasisupermodular function "a supermodular function up to a change of units"? Section 3 of the paper answers it with Theorem 8. An earlier notion in the same direction, supermodularizable functions, was studied by Li Calzi (1991).
Let be a lattice: a partially ordered set in which every two elements have a least upper bound (join) and a greatest lower bound (meet). Examples are and products of finite chains, ordered componentwise.
A function is supermodular on a set if
It is quasisupermodular (p. 162) if for all
A function is strictly increasing if implies . A function is supermodularizable if is supermodular on for some strictly increasing .
For the set is closed under and ; it is the sublattice generated by and and has at most four points.
Quasisupermodularity depends only on the order of the values of , so it is preserved by strictly increasing transformations; supermodularity is not. Every supermodular function is quasisupermodular, and so is every supermodularizable function.
is quasisupermodular if and only if there is such that (i) is strictly increasing for every , and (ii) for every ,
The Lemma is the "only if" direction of Theorem 8 on a single sublattice; Example 1 shows why the transformation in Theorem 8 must be allowed to depend on .
Theorem 8 characterizes an ordinal property by a family of cardinal ones: quasisupermodularity is exactly local supermodularizability, on every two-generated sublattice. It explains why quasisupermodularity, and not supermodularity, is the natural hypothesis of ordinal comparative statics, and Example 1 marks the boundary: a single global transformation is not enough, so supermodularizable functions form a strictly smaller class. The paper states an analogous characterization of the single crossing property (Theorem 9, p. 166) without proof.
On the formalization side, none of these results is machine-checked anywhere known to this mission. The platform already holds Topkis's lattice-theoretic definitions and theorems (supermodularity, increasing differences, monotonicity of the argmax under the cardinal conditions); this mission adds the ordinal notion and its characterization on top of the published definition of supermodularity. A formal proof of the Lemma also requires constructing a strictly increasing map of all of that moves one prescribed value, which is reusable for other "ordinal versus cardinal" results.
The "if" direction and the invariance and supermodularizability remarks are short unfoldings of the definitions. The work is in the Lemma. On a four-point lattice the values of at need not satisfy , and the obvious attempt, applying one transformation fixed in advance (such as an exponential), fails: the needed transformation depends on the four values. A strictly increasing of the whole real line must be chosen to separate the values while preserving their order, and the degenerate configurations in which some of the four values coincide, or in which and are comparable so that the lattice has fewer than four points, have to be handled separately. A second subtlety is that quasisupermodularity is used for both orders of the pair .
Lattice class; joins and meets are ⊔ and ⊓. Functions are real valued.QuasiSupermodularOn g S, relativized to a set ; the paper's notion on is QuasiSupermodularOn f Set.univ. It quantifies over all ordered pairs of .Supermodularity.Monotonicity.SupermodularOn (Topkis series), also relativized to a set; supermodularity "on the sublattice" is SupermodularOn _ {x₁, x₂, x₁ ⊔ x₂, x₁ ⊓ x₂}.StrictMono. With merely monotone transformations the statements trivialize: a constant transformation is supermodular on every set, which would make the "if" direction of Theorem 8 false and the second half of Example 1 false. The formal statements rule this out.g : ℝ → X → X → ℝ; it may depend on but not on . Transformations are defined on all of , as printed, not only on the values of .Fin 2 × Fin 4 with the product order.Contributions welcome: proofs of the milestones and the goal; a general lemma producing strictly increasing maps with prescribed values on finitely many points.
The speed at which a finite reversible Markov chain approaches its stationary distribution is controlled by its eigenvalues. For a chain with eigenvalues , the distance to stationarity after steps is governed by , where (Diaconis and Stroock 1991, Proposition 3). Upper bounds on the second eigenvalue are the familiar half of this picture, and they are what Cheeger-type and Poincaré inequalities provide. The other half is the smallest eigenvalue : a chain whose smallest eigenvalue is close to oscillates almost periodically and mixes slowly whatever is. A chain is aperiodic exactly when , but that qualitative fact gives no rate.
Diaconis and Stroock's paper gives geometric bounds for both ends of the spectrum, expressed through systems of paths in the graph of the chain. Their bound on uses closed paths with an odd number of edges, the combinatorial witnesses of aperiodicity. The paper has been a standard reference for path (canonical-path, multicommodity-flow) methods in the analysis of Markov chain Monte Carlo since its publication.
Timeline:
Let be a finite set and the transition matrix of an irreducible Markov chain on , reversible with respect to a probability distribution :
The operator is self-adjoint on , with inner product , so its eigenvalues are real. Write and let be the smallest eigenvalue of .
The graph of the chain has vertex set , an edge from to when , and a self-loop at when . An odd closed path at is a sequence of edges from back to , with an odd number of edges, in which no directed edge is traversed twice. Its length is
A system of odd paths chooses one such path for every point, and its load is
the maximum over directed edges of the weighted length of the paths through (display (1.7) of the paper).
For the random walk on a graph , when , with the degree, and . There is the maximum degree, the largest number of edges of a path in , and .
For an irreducible, aperiodic, reversible chain and every system of odd closed paths,
Proposition 2 turns aperiodicity into a number. With Proposition 1, which bounds through paths between pairs of points, it bounds the absolute spectral gap entirely in terms of path geometry, and so bounds the variation distance to stationarity through Proposition 3. Corollary 2 is the form most often applied: for a random walk on a non-bipartite graph, a choice of short odd cycles that do not crowd any single edge certifies that the walk does not oscillate.
Proposition 2 and its corollary are proved in the paper. As far as a search of the platform shows, no machine-checked proof exists. The platform already has the vocabulary (stochastic matrices, stationarity, reversibility, eigenvalues and the inner product, from the published Levin–Peres–Wilmer layer) and the qualitative fact that is not an eigenvalue of an irreducible aperiodic chain. This mission adds the quantitative bound, the identity (1.8), and the path inequality, all reusable for other path-based eigenvalue estimates.
Each step is elementary, but the bookkeeping is where a proof can go wrong. The Cauchy–Schwarz step is applied along each path separately, and the resulting double sum over points and over the edges of their paths must be exchanged into a sum over edges. That exchange is exact only if each path traverses each directed edge at most once. A path that crosses an edge twice contributes twice, while counts it once. Self-loops are edges here, and the sum over directed edges in the last step must match the sum over ordered pairs , including , in the identity (1.8). The alternating signs work only because the number of edges is odd; an even closed path cancels instead of doubling it.
The bound is also only as good as the chosen paths: short odd cycles that spread their load over many edges give a small , and the choice of is part of every application.
The chain is a real matrix P : Matrix V V ℝ on a Fintype V, with the published predicates IsStochastic, Irreducible, Aperiodic, IsStationary (which includes that is a probability vector) and DetailedBalance. is edgeMeasure, the inner product innerPi, eigenvalues IsEigenvalue (a real eigenvalue with a nonzero real eigenfunction). is the infimum of the real eigenvalues of , a minimum for a stochastic matrix on a nonempty set.
Paths are vertex lists. A path traverses the directed edges between consecutive vertices, each with . The paper defines "by analogy with (1.4)", whose paths may not repeat an edge. For the directed edges of §1C this rule is read as "no directed edge twice". Under the unordered reading a vertex of degree one would have no odd closed path, contradicting the page's remark that such paths always exist for irreducible aperiodic chains. is a real supremum over the finite set of directed edges with , and it is only when there is no edge. A system of odd paths on a nonempty set excludes that case, so the bound is never reduced to by . The system is a universally quantified hypothesis of every statement, never an existential one. No milestone assumes the inequality of milestone 3 or the identity (1.8) as a hypothesis. No assumption is made.
Milestones 3 and 4 do not assume aperiodicity: the existence of an odd path system implies it. The identity (1.8) assumes only stochasticity and stationarity. Corollary 2 assumes only that the graph is connected and not 2-colorable; the chain properties follow from these. In Corollary 2, counts paths through a directed edge, which is at most the count through the unordered edge, so the stated bound implies the one with the unordered count. Only the first half of Remark 1.3 is stated; its second half needs Proposition 1's quantity, which belongs to another mission of the series.
Contributions welcome: proofs of the milestones in order, a general Cauchy–Schwarz-along-paths lemma shared with the Poincaré inequality, and the existence of odd path systems for irreducible aperiodic chains.
How fast a finite Markov chain forgets its starting point is the central quantitative question in the analysis of Monte Carlo algorithms, card shuffling and random walks on groups. The classical tool is the spectral gap , which controls convergence in but loses a factor when converted into a bound for a chain started at a point. Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996) 695–750) brought the logarithmic Sobolev constant , introduced by Gross for Gaussian measures (Amer. J. Math. 97 (1975)), into the study of finite chains, and showed that it gives sharper mixing bounds in many examples.
The entropy route to ergodicity is the cleanest consequence of a log-Sobolev inequality: the relative entropy of the chain's law with respect to stationarity decays exponentially at rate , and at rate for reversible chains. The paper notes that the reversible case is contained in Bakry's Saint-Flour lectures (Lecture Notes in Math. 1581, 1994) and Stroock's notes on Gibbs states (Lecture Notes in Math. 1563, 1993), and that Miclo (preprint, 1995) treated the nonreversible case.
Let be a finite set and a Markov kernel: and . Let be an invariant probability, , with for every . Functions act on the right, , and is the inner product of , with norms . The chain is reversible if for all .
The continuous-time heat semigroup is
acting on functions by and on probability measures by . The row is the law at time of the chain started at .
The Dirichlet form is ; it is bilinear but not symmetric unless the chain is reversible. With
the log-Sobolev constant is
The relative entropy of a probability is , and the total variation distance is .
For every probability measure on ,
and, if is reversible,
For an irreducible chain, every and ,
with replaced by for reversible chains.
Theorem 3.6 turns a single functional inequality into a convergence statement valid for every initial law, with no spectral assumption and no reversibility in the first half. Through Pinsker's inequality it gives (3.3), whose prefactor replaces the factor of the spectral bound . When is exponentially small in the size of the problem, as for random walks on large groups or product spaces, is polynomial where is exponential, and the time needed to make the bound small drops accordingly. This is the mechanism behind the sharp mixing bounds the paper derives from .
The results are proved in the paper and are classical; they are not, to our knowledge, formalized. The platform has measure-theoretic statements of Pinsker's inequality and the published finite Markov chain vocabulary of Levin–Peres–Wilmer (stochastic matrices, stationarity, total variation, the heat kernel), but nothing about log-Sobolev constants of finite chains, the entropy derivative along a Markov semigroup, or entropy decay. A formal development provides the entropy layer of the finite-chain theory: the adjoint semigroup, the dissipation identity, the comparison of with , and Pinsker's inequality in the encoding used by the mixing-time library.
The statement is about measures, while the natural quantities to differentiate are densities with respect to , and for a nonreversible chain the density of evolves under the adjoint semigroup, not under . The Dirichlet form is not symmetric, so the order of its arguments matters at every step, and the improvement from to holds only under reversibility.
The obvious first idea, differentiating term by term, meets wherever the density vanishes. The initial law may be a point mass, and for a reducible chain the density can stay zero at positive times. The argument must therefore handle the boundary and the degenerate laws separately from the smooth interior. The constant is defined as an infimum over all functions, with no claim that it is attained or positive.
The state space is a Fintype with decidable equality, is a real matrix with the published predicate MarkovMixing.IsStochastic, satisfies MarkovMixing.IsStationary K π and for all , and reversibility is MarkovMixing.DetailedBalance K π. is the published MarkovMixing.heatKernel K t (the Poisson series), the adjoint kernel is MarkovMixing.timeReversal K π, and total variation is MarkovMixing.tvDist. Time is real, and the decay statements are for .
The local definitions are , the norms , , as a real infimum over the ratios with , , and as the row vector . Lean's Real.log 0 = 0 implements . The goal does not assume irreducibility: it is true for every stochastic with a positive invariant probability, and a reducible chain has . The companion (3.3) keeps irreducibility, the standing assumption of Section 3. In Lemmas 2.5 and 2.7 the paper's is strengthened to , because is at a zero of on the page and in Lean.
Several encodings would make the goal trivially true and are ruled out. is not assumed positive. is a probability, since for the entropy is a positive constant in . is invariant and positive, so is meaningful. The eigenvalue-based MarkovMixing.spectralGap is not used. Applying to as a function, , is not the same as for a nonreversible chain.
A complete development needs: termwise differentiation of the heat-kernel series and the semigroup property ; the adjoint identity for ; elementary convexity inequalities for and ; the symmetric form of for reversible chains; Pinsker's inequality on a finite set; and a scalar Grönwall lemma. The heat-kernel calculus and Pinsker's inequality in the MarkovMixing.tvDist encoding are reusable by the other missions of this series and by any mixing-time development. Proofs of individual milestones are welcome independently of the goal.
Prove a deterministic algorithm for integer 3SUM in the campaign's shared word-RAM model, improving the verified bound.
A promising parameter choice is , , , and . Lean-checked arithmetic certificates give , , and . The predicted Exact Triangle saving is , giving a 3SUM cutoff of and a strict margin below the target.
The algorithmic claim remains open. The milestones are to establish the faster inner solver, then verify the integer computations for and and prove the total Exact Triangle cost, including preprocessing and scans. The existing verified reductions and foundation definitions can then be reused. The numerical certificates alone do not prove the mission.
The multi-armed bandit problem with discounted rewards asks how to allocate effort among independent projects, only one of which can be worked on at a time, when the project worked on evolves randomly and the others stay frozen. It models job scheduling, research planning, search, and sequential clinical experimentation. Gittins and Jones showed in 1974 that the problem has an index solution: each state of each project has a number, computed from that project alone, and it is optimal always to work on the project whose current state has the largest number. The result turns an -dimensional dynamic program into one-dimensional computations.
Several proofs followed, each with its own model and its own definition of the index:
There are bandit processes. Bandit has a finite nonempty state space , and is their disjoint union. When bandit at state is played, a random reward is received, the bandit is busy for a random time , and it then moves to a random state ; the other bandits do not move. The joint law of depends only on , and different plays are independent.
A policy is a map : at time zero and at every play completion time it chooses the bandit to play from the current states. With the start time and the reward of the -th play and a discount rate , the expected discounted reward from the initial joint state is
A policy is optimal if it maximizes for every initial state . A priority rule is a policy for which some ordering of makes it always play the bandit whose current state is ordered highest.
The reward rate of a state is
Reducing bandit by removing a state merges every play that ends in with the following run of plays at into one composite play, whose reward rate is of (2.3). The index algorithm repeatedly picks a state of maximal current rate, sets its index to that rate, and reduces its bandit by removing (or removes the bandit if was its last state).
Let be the indices of a run of the index algorithm. Then every priority rule whose ordering satisfies
is optimal. Ties in may be ordered either way, and the run may break ties in its own choices arbitrarily.
The theorem shows that the optimal priority order is determined by numbers that, by the reduction formulas, depend only on the statistics of each bandit separately. It is the basis of index policies in scheduling (the rule and its semi-Markov generalizations), of Klimov's problem and of branching bandits, which the paper's Section 3 obtains by modifying the same argument.
The result has been proved many times, but not in this generality on Prove2Me. The platform has a discrete-time Gittins index theorem for arms sharing one transition kernel and one reward function, with the index defined as a stopping-time supremum. This mission adds semi-Markov dynamics with random play durations and continuous discounting, heterogeneous finite bandits, priority rules, and the index algorithm as the definition of the index. A complete development would also give a machine-checked proof of correctness of a state-elimination algorithm for computing Gittins indices.
Lemma 2.1 compares an optimal stationary policy with a modified policy that is not stationary, and closes the gap by the optimality of stationary policies, which itself requires the dynamic-programming theory of discounted semi-Markov decision problems with finite state spaces. The reduction step requires an exact identification of the values of all top-priority policies with values in a different problem whose plays are composite and may never end. Theorem 2.1 is an induction over a family of problems with shrinking state spaces that are no longer raw semi-Markov bandits. Theorem 2.2 adds ties: a priority order compatible with the indices need not be the order of the given run, and one needs another run with the same indices.
Fin n (), with and each state type finite and nonempty. is the sigma type Σ i, X i, disjoint by construction.A formalization in which the value of a policy is defined through rates or indices, or in which is any function compatible with some order rather than the output of the algorithm, would make the goal trivial or empty; both are excluded by the definitions above.
Needed infrastructure: the convergence of the -play values and the first-step (Bellman) equation for ; existence of an optimal stationary policy for finite discounted semi-Markov problems; the value identity for composite plays. The last two are reusable for any finite semi-Markov decision problem. Proofs of individual milestones, alternative arguments (Weber's prevailing charge, the retirement formulation), and the separability statement of p. 198 ("the index algorithm can be carried out separately for each different bandit") are welcome.
Many decision problems under uncertainty take the form of minimizing an expected cost over a convex feasible set, where is a random parameter whose distribution can be sampled but not integrated in closed form. Evaluating even approximately can cost exponentially many evaluations of in the dimension of , so the classical deterministic notion of an approximate solution is unusable. A practical alternative, going back to Nemirovski and Yudin, asks for a random output whose expected objective value is close to the optimum: . Stochastic subgradient methods achieve this; Nesterov's paper Primal-dual subgradient methods for convex problems (Math. Program. 120 (2009)) shows that the same guarantee holds for a stochastic version of his method of simple dual averages, a scheme that aggregates all past subgradients in the dual space instead of taking projected steps with decreasing step sizes.
Dual averaging has since become a standard tool in stochastic and online convex optimization (regularized dual averaging, AdaGrad's primal-dual variant, distributed dual averaging). Section 6 of Nesterov's paper is the original statement of its expected-accuracy guarantee.
Let be a finite-dimensional real vector space with an arbitrary norm and dual space with dual norm . Let be closed and convex, and let be a prox-function of : continuous on and strongly convex on with convexity parameter ,
with prox-center and . For and the point is well defined. The scalar sequence is given by and for .
The stochastic problem is given by a probability space and a cost with well defined on , and a minimizer of over with . Assumption 1: each is convex on . Assumption 2: a stochastic oracle returns a subgradient of at , and for all , .
The method of stochastic simple averages (SSA, (6.3)) fixes , starts from and , and for draws a fresh independent sample and sets
Its deterministic counterpart, the method of simple dual averages (SDA, (2.21)), is the same recursion with arbitrary answers in place of . The quality of the points is measured by the gap . Write and for the expectation over these independent samples.
For every ,
Theorem 7 gives an explicit, non-asymptotic bound on the expected optimality gap of the averaged SSA point. Since , the bound is , the optimal rate for nonsmooth stochastic convex optimization with bounded subgradients. Two features distinguish it from the classical stochastic subgradient bound: it holds in an arbitrary norm with a non-Euclidean prox-function (for example the entropy on the simplex with the norm), and the feasible set need not be bounded, since only enters. The constant is explicit and can be tuned to .
The result is proved in the paper; to our knowledge no machine-checked proof of Theorem 7 or of the dual averaging bounds of the paper exists. A formalization yields a reusable verified analysis of dual averaging in a general normed space, a template for expectation bounds over i.i.d. sample paths of an adaptive algorithm, and checked constants.
The pathwise part is a consequence of the deterministic Theorem 2, which itself rests on the general Dual Averaging bound (the companion mission's Theorem 1) and on the strong convexity estimates for . The probabilistic part looks routine on paper but is where formal arguments break: the iterate is a function of , and the identity requires measurability of the whole run and a Fubini argument on the product space. Measurability of the run in turn depends on continuity of the argmin map , and integrability of and of the gap is not assumed but must be derived from the uniform bound and the boundedness of the iterates. Pathwise bounds alone do not suffice: (6.5) controls the gap on each sample, not .
Theorem numbers and page numbers refer to source.pdf, the author's revised CORE discussion-paper version (September 2005) of the Math. Program. article; printed pages equal PDF pages.
StrongDual ℝ E with the operator norm, and is s x. Strong convexity is Mathlib's StrongConvexOn Q σ d, which is exactly (1.8); .ℝ → StrongDual ℝ E → E with the hypothesis that lies in and minimizes for every ; no choice function is used.A complete development needs the deterministic dual averaging analysis (Lemma 1, Lemma 2, Theorem 1 of the paper, restated here only through Theorem 2), measurability and continuity of , and Fubini on finite products of probability spaces. The dual averaging lemmas and the product-measure lemmas for adaptive sample paths are reusable beyond this mission. Proofs of any milestone, and supporting lemmas on measurability of the SSA run, are welcome.
A firm that holds a single stock of one product often faces demand from several classes of customers that differ in importance: emergency and routine orders for spare parts, contract and spot customers, high- and low-priority users of a military supply system. When stock runs low it can pay to refuse a less important demand now in order to keep stock for a more important demand that may arrive later. Veinott (Operations Research 13 (1965), 761–778) studied a dynamic inventory model with several demand classes but required the specific policy that serves every class whenever stock is available. Topkis (Management Science 15 (1968), 160–176) treated the dynamic version, in which demands arrive over the intervals of a period between two procurements, and showed that the optimal rationing policy has a simple form described by one critical rationing level per class and interval.
This mission concerns how those critical levels move over time. The paper's Theorem 2 gives a condition under which, without backlogging, the levels are monotone in the interval index, so that rationing is at least as strict early in the period as late in it. It is the second of four missions on the paper; the first establishes the critical-level policy itself (Theorem 1).
A period is divided into intervals, indexed backwards: interval has intervals after it, so interval is the first and interval 1 the last. There are demand classes, class the most important. At the start of interval the demand vector is observed; demands of different intervals are independent, and each class has a finite mean. With backlog and stock , one decides the vector of outstanding demand left unsatisfied, , using units of stock, so the stock at the end of the interval is . A fraction of the unsatisfied demand is carried as backlog into the next interval: is complete backlogging, none.
The costs are a penalty with (Assumption (C)), a holding cost continuous and convex on (Assumption (A)), and a salvage cost at the end of the period, with , convex and continuous and bounded below (Assumption (B)). Here denotes the right derivative. The optimal costs satisfy the recursion (1)
with .
With the -th unit vector, the critical rationing level is if is strictly decreasing on , and the smallest minimizer of on otherwise. Under the paper's Theorem 1 the rationing level policy , with , is optimal: class is served from stock only while the stock stays at or above .
Let , , , and for . If
The result says that, in intervals without backlogging, the stock reserved against a class is never larger late in the period than early in it, provided the class's penalty in the earlier interval plus the eventual marginal holding cost does not exceed its penalty in the later interval. Together with Theorem 1 it reduces the dynamic rationing problem to a family of one-dimensional critical numbers with a known order in both the class and the time index. The paper's example on p. 170 shows that the analogous monotonicity fails with backlogging, so the hypothesis is essential.
The paper's proofs are complete but informal: they interchange expectation and right-derivative limits, and rest on Lemma 2 (convexity and attainment) and Theorem 1 (c). No part of this paper has been machine-checked. This mission produces formal statements of Theorem 2 and the three lemmas it rests on; contributions that formalize the known proofs, or that settle whether the extra hypothesis on earlier backlogging fractions (below) can be dropped, are equally in scope.
The central difficulty is Lemma 7, the comparison of the marginal value of stock in two consecutive intervals. The value functions are defined through an infimum and an expectation, so they are convex but not differentiable, and the minimizer in (1) changes regime each time the stock crosses a critical level; differentiating (1) directly is not available. Right derivatives may also be at , and statements about them have to survive an interchange of expectation and a one-sided limit. The lemma depends on the optimal policy of Theorem 1, which is the subject of the first mission of this series. The claim of Lemma 7 is false when and (p. 168), so no argument can ignore the case split.
Fin n (paper class is index ); intervals are natural numbers counted backwards; vectors are Fin n → ℝ with the pointwise order.sInf and the Bochner integral, and every statement restricts to , , where the paper's Lemma 2 (proved in the first mission of the series) makes the infimum finite and attained and the integrand integrable.derivWithin, which would return where the right derivative is . Sums of right derivatives are taken in EReal.Model.Standing; (B)'s limit condition is read as " is bounded below".WithTop ℝ satisfying the defining predicate (strictly decreasing ⇒ , otherwise the smallest minimizer); the theorem holds for any such choice. Their existence is a milestone of the first mission; a sanity check exhibits a model in which all hypotheses of Theorem 2 hold with .A family of linear forms turns independent observations into a single random maximum. Examples include the largest value of a collection of statistical scores and the norm of a random vector sum, which can itself be expressed through the continuous dual of a normed space. A bound for each form separately does not automatically control the supremum over an infinite family. Talagrand's 1995 paper gives a concentration inequality in which the coefficient scale, rather than the number of forms, controls the deviation Talagrand 1995, §8.1. The Banach-space consequence in Chapter 13 applies the same principle to norms of vector sums Talagrand 1995, Theorem 13.2.
The two results have a direct relationship: the norm of a vector is the supremum of its evaluations by continuous linear functionals of norm at most one. The formalization therefore gives a setting in which a general real-valued supremum theorem and a vector-valued corollary can be audited together. It also tests whether the concentration statement remains faithful when the family of forms is infinite and the coordinate laws differ.
Fix a finite number of coordinates and a nonempty family of coefficient vectors . The coefficients may have either sign. Write , and let . The mission treats the case in which this coefficient scale is finite and positive. Let be independent real random variables, with an individual interval containing each almost surely. The center and the law of may vary with . The object of interest is
A median of means that both and are at least . This definition permits more than one median and makes no choice among them. With a bounded coefficient family and bounded coordinates, the supremum is finite for each input. The mission also assumes that is measurable, because an uncountable supremum of measurable functions need not be measurable automatically. These are the mathematical conditions needed to give the displayed probability its ordinary meaning.
The supporting observation uses Talagrand's convex-hull distance. For a set of coordinate tuples and a point , form the binary vectors for which there is some such that every coordinate with agrees between and . Let be their convex hull in . The distance is the Euclidean distance from zero to . If is empty, this distance is . This convention preserves the intended meaning of a distance to an empty target Talagrand 1995, §4.1.
For , put and . The first milestone is Eq. (8.1.3): if is nonempty, then for every some has disagreement set with
The second milestone is the deterministic observation in Eq. (8.1.2):
The goal, Theorem 8.1.1, asserts that every median of and every satisfy
The third milestone is Theorem 13.2. For vectors in a real Banach space , define the weak variance scale . If the independent real variables satisfy , the theorem bounds deviations of from any median :
The statement is made for . With , the displayed event has threshold zero and probability one, while the right side falls below one for large ; the printed inequality therefore needs that qualification Talagrand 1995, p. 198.
Theorem 8.1.1 controls a supremum using only the largest Euclidean norm of its coefficient vectors. Its statement does not charge a factor for the cardinality of , so it applies equally to a finite collection and to an infinite measurable supremum. The coordinatewise interval condition allows different distributions and different centers. Theorem 13.2 converts the same concentration scale into a statement about Banach-space vector sums, where the dual unit ball supplies the coefficient family Talagrand 1995, pp. 156, 198.
Both results are proved in the paper. The work here is to formalize their exact statements and the distance interface used between them. The reusable pieces are the median convention, an extended-valued convex distance on arbitrary product spaces, a measurable supremum over a general set of coefficient vectors, and the weak variance scale for Banach-space vectors. None of the two claimed concentration inequalities is treated as already machine checked by this mission.
For a single fixed vector , bounded-coordinate concentration gives information about . Applying that estimate to every member of and taking a union would introduce a dependence on the number of vectors. It would also give no useful bound for a genuinely infinite family without additional covering information. Talagrand's target avoids a cardinality term, so a direct collection of fixed-form estimates does not establish the stated result Talagrand 1995, §8.1.
The deterministic distance statement presents a second issue for formalization. Its set can be empty, and the paper's distance then has value . A real-valued infimum with a default value at the empty set would erase that distinction. The exact Euclidean norm also matters: the usual norm on a Lean function space need not be the paper's norm. These choices affect the mathematical meaning of the milestone before any concentration argument begins.
Coordinates are indexed by Fin N, corresponding to the paper's indices . The independent observations live on the canonical product of their individual real-valued laws. Each law gives probability one to its own interval ; identical distribution is not assumed. The coefficient family is a set, not a finite list. Its nonemptiness, finite norm supremum and positive scale are explicit. Measurability of the real supremum is also explicit, following the paper's convention of ignoring measurability questions Talagrand 1995, pp. 81–82.
The mismatch vectors and their convex hull are defined over the whole underlying product type. The distance is an extended nonnegative real infimum of Euclidean lengths, so an empty target has distance . Eq. (8.1.2) uses extended arithmetic for the positive part of , which keeps the empty-sublevel case meaningful. The probability bounds retain the paper's constants , , and . A zero coefficient scale cannot be used to make the goal a vacuous division-by-zero statement; the Banach result likewise requires a positive weak variance scale.
The mission welcomes proofs of the two concentration statements, the deterministic distance observation, and supporting facts about the supremum's finiteness and measurability. General lemmas about product measures, medians, extended distances, and dual norms would be useful beyond this chapter. The statements do not restrict to a finite or countable subset, so a proof must address the general family under the explicit measurability assumption.
Subgradient methods are the basic tool for minimizing a nonsmooth convex function when only a black-box oracle returning one subgradient per query is available. In the classical method the new subgradient enters the iterate with a weight that decreases over time, so information collected late is counted less than information collected early, and the method has no natural certificate of its own accuracy.
Yu. Nesterov's paper Primal-dual subgradient methods for convex problems (Math. Program. 120 (2009) 221–259; first circulated as a CORE discussion paper, March 2002, revised September 2005) introduces Dual Averaging (DA): the method accumulates all past subgradients with nondecreasing weights in the dual space and maps the aggregate back to the feasible set through a strongly convex prox-function. One analysis, Theorem 1 of the paper, gives at once an upper bound on a primal-dual gap, a bound on the iterates that holds even on unbounded feasible sets, and a bound on the averaged subgradients. From it the paper derives rates for minimization over simple sets, problems with functional constraints, saddle points, variational inequalities, and stochastic optimization. Dual Averaging later became a standard method in online learning and regularized stochastic optimization (e.g. L. Xiao, Dual averaging methods for regularized stochastic learning and online optimization, JMLR 11 (2010)).
Let be a finite-dimensional real vector space with an arbitrary norm , and its dual. The value of at is , and the dual norm is . Balls are .
Let be closed and convex. A prox-function of is a function , continuous on , that is strongly convex on with convexity parameter :
The prox-center minimizes on , and . Two examples: the Euclidean norm with , and the norm on the simplex with the entropy .
For and set and
and let .
Given sequences , , , write , (), , the gap function
and the upper gap function .
The DA-scheme (2.14) starts at with and ; at step it receives (the oracle answer at ), chooses and , and sets
A point is a solution in the sense (2.8) if for all .
For every run of the DA-scheme, every and every ,
if is a solution in the sense (2.8), then
and if moreover for some , then
The theorem leaves the step sizes and the parameters free; every rate in the paper is obtained by choosing them.
In the order the proof uses them: Lemma 6 (unique minimizer of a strongly convex function, quadratic growth (9.5), p. 36); Lemma 1 (convexity, differentiability, and its -Lipschitz continuity, p. 7); (2.5) ; (2.6) ; (2.2) monotonicity of in ; Lemma 2 (p. 8); (2.11) the representation ; (2.13) ; and (2.18), the telescoped estimate along the scheme (p. 10).
Theorem 1 is the single estimate behind the whole paper. With growing like it gives the rate of Dual Averaging for nonsmooth convex minimization with simple or weighted averages (Theorems 2 and 3), and through the gap it gives primal-dual certificates for saddle-point problems and variational inequalities (§§3–5) and the stochastic version (§6, the companion mission). Part 2 is the reason the method can run on unbounded feasible sets: the iterates stay in a ball around any solution. Part 3 bounds the averaged subgradients, which yields approximate dual solutions.
The result is proved in the paper. As far as a search of Mathlib and the Prove2Me catalog shows (October 2026), none of its statements is machine-checked: Mathlib has strong convexity (StrongConvexOn) and Fréchet derivatives, but no prox-functions in an arbitrary norm, no Danskin-type differentiability of a maximum, and no analysis of Dual Averaging. A formalization produces these as reusable pieces: Lemma 6 in an arbitrary finite-dimensional norm, the smoothness of (a form of the duality between strong convexity and Lipschitz gradients of the conjugate), and the definitions of the scheme and its gap functions, on which the paper's §§3–6 can then be built.
The bookkeeping of the proof is short; the analytic content sits in Lemma 1 and Lemma 6. Lemma 1 asserts differentiability of a function defined as a maximum over a possibly unbounded set, in an arbitrary norm, where the gradient lives in and no inner product is available to identify it with a vector. The prox-function is only continuous and strongly convex, never assumed differentiable (footnote 2, p. 5), so first-order optimality conditions for are not available. Lemma 6's existence claim needs boundedness of the level sets of in finite dimension; the printed argument ends with "this contradicts continuity of ", which does not by itself close the argument, so a complete proof has to supply the missing step. Finally, (2.18) pairs a sum from with a sum from and depends on being the prox-center, so an off-by-one in the indices of the scheme changes the statement.
is a finite-dimensional real normed space with an arbitrary norm; is StrongDual ℝ E with the operator norm, which is , and is s x. No inner product is used, so the /entropy example remains an instance. The prox-function is a real function on of which only its values on are used, strongly convex in Mathlib's sense StrongConvexOn Q σ d (exactly (1.8)), with (the paper's "" at (1.8) is corrected by its Definition 1). The maxima , , are real suprema, finite for , ; every statement assumes these ranges, including Lemma 2 and (2.13), where the page writes but is not defined. The argmin map is a hypothesis on a given map, not a construction, and the run of (2.14) starts at the prox-center and takes the oracle answers as free data. Indices start at . Pages and equation numbers are those of the CORE discussion-paper version (September 2005) used as source, not the journal's pp. 221–259.
A trivializing formalization is ruled out: the run must set to the argmin point and must carry its argmin property, without which the statements would be false, and the setting is satisfiable (E = ℝ, , , , ), so the theorem is not vacuous.
Needed infrastructure: Lemma 6 in an arbitrary norm; a Danskin-type differentiability lemma for ; Lipschitz continuity of the argmin map; suprema manipulations for , , under boundedness. Contributions of any of the milestones, of general lemmas on strongly convex functions in normed spaces, and of the remaining parts of Theorem 1 are welcome.
Pick independent points uniformly in and let be the length of the longest increasing subsequence. Because the points are almost surely distinct, has the law of the longest increasing subsequence of a uniform random permutation of . This is Ulam's problem, one of the most studied random combinatorial quantities. Hammersley (1972) showed converges, and Vershik–Kerov and Logan–Shepp (1977) identified the limit as . That leaves the size of the fluctuations of around its typical value.
Timeline.
Section 7.2 of the same paper applies the same idea to the longest common subsequence of two random words, a quantity tied to the edit distance used in genetics and speech recognition.
Let and . For , is the largest integer for which there are indices with . For , the level set is .
Fix a probability on without atoms (Lebesgue measure, for instance) and let be the product probability on ; the coordinates are the random points . A median of is a number with and .
The tool is Talagrand's convex hull distance. For and , let be the set of for which some agrees with at every coordinate with ; let be its convex hull in ; and let be the Euclidean distance from to (with if ).
A function on an arbitrary probability space is a configuration function if, for every , some set of exactly coordinates satisfies for all .
For two sequences and , is the largest with , and for all .
For every median of and every ,
The result. Since is of order , the goal confines to a window of width of order around its median with Gaussian-type tails. For much larger than the upper bound becomes exponential in , the natural tail of a quantity bounded by the size of a witnessing configuration. Theorem 7.1.3 isolates what is used: every integer quantity certified by a configuration of exactly its own size has the same concentration. This abstraction became the notion of certifiable functions used widely in random graph theory and probabilistic combinatorics (see the treatment of Talagrand's inequality in Alon–Spencer, The Probabilistic Method). For the longest common subsequence, the bound is useful when the alphabet is large and , where it improves on Azuma's inequality.
Formalizing it. All four results are proved in the paper; none is formalized in Lean as far as a search of the Prove2Me corpus shows. A finite-alphabet certifiable-function inequality (Talagrand.certifiable_concentration) has been posed on the platform as an open statement; it uses a Lipschitz hypothesis and no median, so it is a relative of Theorem 7.1.3, not the same statement. The mission produces a general- formalization of the configuration-function principle, its application to the continuous Ulam problem, and the common-subsequence variant.
The deterministic inequalities (Lemma 7.1.1, Eq. (7.2.3)) relate the Euclidean distance , defined through a convex hull in , to purely combinatorial counts of disagreeing coordinates; this needs the infimum defining to be attained and a duality between the convex hull and its extreme points. The probabilistic step rests on Talagrand's convex hull inequality (Theorem 4.1.1, Eq. (4.1.2)), , for a general product probability; that inequality is not in Mathlib. A bounded-difference (Azuma or McDiarmid) argument does not suffice: changing one point changes by at most , which gives deviations of order , not . The point of the configuration property is that only the coordinates of a witness matter.
Fin N → Ω (0-based), and is Measure.pi (fun _ => μ). For the goal, is unitInterval and is any probability measure on it with for all . Theorem 7.2.1 uses the product of Measure.pi measures on (Fin N → ℝ) × (Fin N' → ℝ) for a probability on . Eq. (7.2.3) lives on Fin (N + N') → unitInterval, with the first coordinates forming the first sequence.Fin p → Fin N. and take values in ℕ.ℝ≥0∞, with the Euclidean norm written out as . Mathlib's default norm on Fin N → ℝ is the sup norm and would give a different, much weaker statement. The deterministic inequalities are stated in the rearranged form in .The mission uses the shared definition of the convex hull distance from Section 4.1. A general- proof of Eq. (4.1.2) and of the attainment of would be reusable for every Part II chapter of the paper. Contributions are welcome in particular for the deterministic Lemma 7.1.1 and Eq. (7.2.3), the measurability of and , and the reduction of Theorem 7.1.2 to Theorem 7.1.3.
Primal-dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal-dual pairs whose complementarity products are all equal. Every such method confines its iterates to a neighbourhood of that path, and the neighbourhood governs both the theory and the practice. The first primal-dual path-following algorithm, by Kojima, Mizuno and Yoshise (1989), used the one-sided neighbourhood and attained precision in iterations. Kojima–Mizuno–Yoshise and Monteiro–Adler then switched to the narrow Euclidean neighbourhood and improved the bound to . Practical codes nevertheless favour wide neighbourhoods, which allow long steps.
Mizuno, Todd and Ye (Cornell ORIE Technical Report 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993) analyse adaptive-step algorithms, which at every iteration take the longest step that keeps the iterate in the neighbourhood. This mission formalizes their §4: the adaptive-step algorithm in the wide neighbourhoods and attains precision in iterations. With close to , contains almost all of the strictly feasible set.
Fix , , , , , and consider
The strictly feasible pairs are the with , , , and for some . For such a pair the duality gap is , and the duality measure is . Write , and .
Norms: is the Euclidean norm, the maximum norm, and , with and . For the wide neighbourhoods are
The second says only that for every .
The search direction with centering parameter solves, for some ,
and the step is , . The scaled quantities , , satisfy and . The componentwise product is the second-order term .
Algorithm 2 with neighbourhood and starts at with . While , it computes from (2), takes the largest such that for all , and sets .
Let with , and let be or . Every run of Algorithm 2 reaches for some
The paper states " iterations"; the count above is the one its inequality (15) yields.
Theorem 2 shows that the adaptive long-step method in a neighbourhood covering almost all of keeps the worst-case complexity of the original Kojima–Mizuno–Yoshise algorithm. Its per-iteration analysis (Lemma 5, Lemma 1(c)) is also what the paper reuses for its potential-reduction variant (§5, Theorem 3) and for its probabilistic explanation of why such methods take far fewer iterations in practice (§6). Lemma 1(b)–(c) are the standard bounds on the second-order Newton term, and they recur throughout the interior-point literature.
The results are proved in the paper. As far as the platform's corpus shows, none of them has a machine-checked proof: there is no formalization of the wide neighbourhoods , , of the Newton system (2), or of an adaptive-step iteration. A complete development yields a reusable layer for primal-dual interior-point analysis in standard form (the neighbourhoods, the scaled direction, the second-order bounds) and the first formally verified iteration bound for a long-step primal-dual method.
Most of the steps are finite-dimensional inequalities. The sticking points are the following.
Vectors are Fin n → ℝ, with coordinates indexed , and A : Matrix (Fin m) (Fin n) ℝ. Mathlib's default norm on Fin n → ℝ is the sup norm, so the Euclidean norm norm2 and the norms normInf, normInfNeg, normInfPos are defined explicitly. divides by as a real number. Here is the natural logarithm and is a real power with .
Committed conventions and repairs:
IsGreatest of the set of admissible step lengths, and is not capped at . When no maximum exists (always the case for , where ), no iteration exists. A run is then possible only if it has already stopped, and the theorem holds trivially. A sorry-free check confirms that an iteration exists for .The goal is not to be read with a hidden constant. A statement of the form "there is with at most iterations", with allowed to depend on the instance, would be trivially true and is ruled out by the explicit count. Lemma 1(a) and Lemma 2(a), 2(b) belong to the paper's predictor–corrector analysis, which is a separate mission.
Contributions are welcome at every level: proofs of the milestones, helper lemmas about the norms on Fin n → ℝ, and the run-to-count argument.
The concentration of measure phenomenon says that in a product probability space a set of probability not too small is "large" in the sense that most points lie within a small distance of it. M. Talagrand's 1995 memoir Concentration of measure and isoperimetric inequalities in product spaces develops this phenomenon through exponential moment bounds for distances to sets. Its Section 2.1 treats the Hamming distance on an arbitrary product space and recovers the bounds obtainable by martingale methods (McDiarmid, On the method of bounded differences, 1989).
Section 2.3, the subject of this mission, specialises to the two-point space with biased coordinates. This is the setting of the binomial law, of random subsets of a finite set, and of monotone properties of random graphs. Two things happen there that do not happen in general. First, the bias of the coordinates enters the bound through the variance , which gives sharper tails when is close to or . Second, when one counts only the coordinates where has a and the point of has a , and measures under a second, more heavily biased product measure, the exponential moment bound becomes independent of the dimension . The paper calls this the first of its results that "apparently cannot be obtained via martingales". Bounds of this one-sided kind are the natural tool for upper tails of increasing functions on the biased cube, the regime of the binomial law near when samples are drawn at rate .
Let . For let be the probability on with , , and let be the product probability on , whose points are written . For a set and a point , the Hamming distance from to is
the least number of coordinates of that must be changed to land in . The one-sided distance counts only changes from to :
Both are when is empty. A second probability on has , and . For and the paper uses two constants,
In the Lean development these are hammingDistToSet, oneSidedDistToSet, bConst, aConst, the measure productMeasure N p, and the integrand expMul t z .
If , then for every , every , every and every ,
For small one has . When and , the paper's explicit threshold is . At equality, the bound becomes , with no dependence on . The main theorem also includes the endpoint cases and without using this ratio.
Milestones 1–3 concern the two-sided Hamming distance; milestone 4 is the one-coordinate inequality behind the goal.
The results. Proposition 2.3.1 and Corollary 2.3.2 give, for every set in the biased cube, a tail bound for the Hamming distance whose Gaussian part has the variance of the binomial law, not the worst case . The paper notes that this matches the quality of the optimal isoperimetric inequalities that are known only for hereditary (monotone) sets. Theorem 2.3.4 is a statement with no dimension in it: it controls how many s of a -sample must be switched off to reach a set that is not small under the more biased .
Formalizing it. These results are proved in the paper; the local Prove2Me index contains no machine-checked proof of these statements. Mathlib has the Bernoulli measure, finite products of measures and lower Lebesgue integrals, but no exponential moment bound for these distances to sets. A complete development would add reusable facts about biased Boolean products, their distance functions and exponential moments, and the uniform cubic error term in Corollary 2.3.2.
The obvious route to a Hamming-distance tail bound is a martingale (bounded differences) argument. It yields -type bounds that do not see the bias , and its variance proxy grows with , so it gives no bound independent of ; the paper states that Theorem 2.3.4 apparently cannot be obtained this way. Theorem 2.3.4 measures under while the integral is under , so a one-coordinate estimate must account for two different probabilities and keep the factor exactly equal to for small . Lemma 2.3.5 must handle as well as interior values. Corollary 2.3.2 requires a cubic error bound uniform in and .
Bool with = true; reuses the published TalagrandCore.bernPi Bernoulli product measure with p : unitInterval converted to a nonnegative real, over Fin N (0-based coordinates). Every subset of is measurable, so the paper's convention of ignoring measurability costs nothing here.ℝ≥0∞, with ; integrals are lower Lebesgue integrals ∫⁻ in ; is computed in , so gives .The mission also imports the published TalagrandCore.bernPi definition for the Boolean product law. Reusable pieces include evaluation of over under a Bernoulli measure and facts about product measures over Fin N. Contributions to any of the four milestones or the goal are welcome.
The proximal point algorithm replaces a hard optimization or equilibrium problem by a sequence of better-conditioned ones: from the current point it solves the original problem with a quadratic penalty added, and takes the solution as . The method is a building block of modern convex optimization. Augmented Lagrangian methods, Douglas–Rachford and ADMM splitting, and many bundle methods are proximal point iterations applied to suitable problems (Rockafellar 1976; Eckstein–Bertsekas 1992).
The algorithm was introduced by B. Martinet in a five-page note in the Revue française d'informatique et de recherche opérationnelle in 1970 (Martinet 1970). The note treats three cases: monotone variational inequalities on a bounded convex set (§II), convex–concave min–max problems (§III), and convex minimization (§IV). This mission formalizes §IV.
Timeline.
Let be a real Hilbert space with inner product and norm . Let be a nonempty, closed, convex set, and let be a convex, lower semicontinuous function such that, for every , the sublevel set is bounded. These are the standing hypotheses of §4.1 (Lean: Standing f C). The problem is
and its solution set (solSet f C) is the set of with for all .
The regularization algorithm (13) starts from and, given , takes
Lean encodes one step as IsProxStep f C xn y ( and for all ) and a run as IsProxSeq f C x.
A point is a weak cluster point of (IsWeakClusterPt) if every neighbourhood of in the weak topology of contains for infinitely many . A sequence is minimizing if .
These are the paper's claims in §4.1 ("Ces hypothèses assurent l'existence d'une solution pour (12)") and §4.2 ("solution unique").
For every sequence generated by (13),
The goal asserts no rate and no constant. It is the statement the paper makes, with both conclusions in one theorem.
If in addition is uniformly convex, i.e. for , , with for , then (12) has a unique solution and .
The result. Théorème 3 says that the proximal iterates make progress on the objective, not only on the distance to the solution set. A user of the method can stop on a value criterion. The convergence also needs no step-size tuning, no smoothness of , and no bound on beyond the boundedness of the sublevel sets. The well-posedness of (13) is what makes the method an algorithm. Each step is a strongly convex subproblem with a unique solution, and later inexact and splitting variants rely on that.
Formalizing it. The note gives no proof of Théorème 3 ("On peut faire une démonstration directe de ce théorème") and none of Remarque 1. The mission asks for a complete machine-checked proof of the convex minimization case of the original proximal point paper. To our knowledge, none of these statements has a machine-checked proof. Mathlib has convexity, lower semicontinuity, the weak topology of a normed space and uniform convexity of functions, but no proximal point algorithm.
Each iterate is defined only implicitly, as the minimizer of a problem that changes with . Monotonicity of follows at once from comparing with . Monotonicity alone gives convergence of to some limit, but not to . Closing that gap needs information about the minimizers of (12) and their distance to the iterates.
The cluster-point statement is about the weak topology. A norm-continuity argument does not apply: is only lower semicontinuous in norm, and passing to weak limits requires the weak lower semicontinuity of convex lower semicontinuous functions. The boundedness that makes weak cluster points exist comes from the sublevel-set hypothesis, not from , which may be unbounded.
For Remarque 1, the obvious argument controls , and the hypothesis on is only positivity. Passing from to is not immediate without a monotone modulus.
All statements live in MartinetReg.ConvexMin. The conventions the formalization commits to:
InnerProductSpace ℝ H, CompleteSpace H). The paper says "espace de Hilbert", and its inequalities make it real.IsProxSeq accepts any sequence with satisfying (13) at every step. Existence and uniqueness of the step are a separate milestone, not built into a definition by choice.sInf takes on sets unbounded below. As a side effect, the theorem asserts that is bounded below on .WeakSpace ℝ H. A norm cluster point would weaken the conclusion and is not used.UniformConvexOn Set.univ φ f with for . It keeps every hypothesis of §4.1.The goal does not assume that (12) has a solution, that is bounded below on , or that the iterates are bounded. Each of these would remove part of the content of Théorème 3, and the first two are consequences proved as milestones.
Not formalized here: Remarque 2 (p. 158), a comment that convexity seems indispensable; and the Exemple (p. 158). The Exemple's linear system corresponds to . For the printed , (13) gives . The variational inequality case (§II) is the companion mission I of this series.
Reusable beyond this mission: the existence of minimizers of convex lower semicontinuous functions with bounded sublevel sets on closed convex subsets of a Hilbert space, and the weak lower semicontinuity it rests on. Contributions of these general lemmas, and of strong-convexity facts for , are welcome.
Inventory systems in which unmet demand is lost, not backlogged, are the norm in retail: a customer who finds an empty shelf buys elsewhere. With a positive lead time between ordering and delivery, the optimal policy for such a system depends on the entire pipeline of outstanding orders, so dynamic programming is intractable beyond small . Optimal policies are not of base-stock type, and for decades no policy with a provable guarantee on its expected cost was known for this model.
Levi, Janakiraman and Nagarajan (Math. Oper. Res. 33(2), 2008) gave the first such guarantee. Their dual-balancing policy balances, in every period, the expected holding cost against the expected lost-sales penalty of the units ordered now, and it costs at most twice as much as an optimal policy.
Timeline.
Page and display numbers in this mission refer to the authors' accepted manuscript (28 pages, pp. 1–28), not to the journal's pages 351–374.
Periods are . An order placed in period arrives at the start of period , where is an integer. Before the horizon there are units on hand and pipeline orders for . Demands have finite means. The information available at the start of period contains and possibly more. A feasible policy chooses as an -measurable quantity.
The on-hand inventory at the start of period , after the arrival, satisfies and
Demand is lost. Costs are a holding rate , a lost-sales penalty and an ordering cost per unit, where and are non-increasing in .
Marginal cost accounting. Under first-ordered-first-consumed bookkeeping, is the ordering cost plus the holding cost that the units incur until the end of the horizon, and is the lost-sales penalty in the period in which they arrive. The cost of a policy is
It omits only costs that are the same for every policy.
The truncated inventory position of period with respect to is . For two policies and , the set holds the periods with for every , and holds the remaining periods .
A dual-balancing policy orders, in each period , the amount that equalises the two conditional expectations
If demands are independent, then for every feasible policy
Comparing with every feasible , rather than with an optimal policy, gives the guarantee without assuming that an optimum is attained.
The result. The theorem gives a constant-factor guarantee for a lost-sales system with lead times, for arbitrary independent and non-identical demand distributions. The policy is computed online, one period at a time, from one-dimensional conditional expectations, which an optimal policy cannot be. The guarantee holds with time-dependent holding costs and with non-increasing ordering and penalty costs. Section 5 of the paper extends it to correlated demand structures, which are out of this mission's scope.
Formalizing it. The theorem is proved on paper and, to our knowledge, has no machine-checked proof. The mission produces the lost-sales dynamics, the truncated inventory position, marginal cost accounting and the sample-path amortization lemmas as reusable Lean objects. It also produces a formal treatment of the conditional-expectation step under independence, which the backlogging analysis does not need. The sibling mission on the backlogging model, LeviBalancing.DualBalancing, provides the shared instance and policy definitions that are reused here.
In the backlogging model, is decided by information available at time , so the cost comparison can be made period by period after conditioning on . With lost sales this fails: the truncated positions of and of the benchmark can cross from below to above and back inside the window . Whether is therefore not known at time , and conditioning on that event moves the conditional expectations of and away from . A newcomer's first idea, to reuse the backlogging argument with -measurable indicators, does not apply. The lost-sales penalty also cannot be charged period by period: Lemma 3.3 is a global amortization over intervals. The non-increasing penalties are what make that amortization possible when varies.
order. Instance, cumDemand, order, DemandProcess and IsFeasiblePolicy are reused from LeviBalancing.DualBalancing. The new layer is one definition file, LostSalesBalancing.DualBalancing.Model.Contributions welcome: proofs of the sample-path lemmas, which need only finite sums and the recursion; the conditional-expectation lemmas, which need a Harris-type argument for independent coordinates; and the existence of a measurable balancing order, which this mission does not pose.
Many estimation problems ask for a matrix of low rank that is consistent with a small number of linear measurements: completing a partially observed ratings matrix, identifying a low-order linear system, or embedding points from a few pairwise distances. Rank minimization under linear constraints is NP-hard, and the standard convex surrogate replaces the rank by the nuclear norm, the sum of the singular values (Recht, Fazel and Parrilo, 2010). Under incoherence assumptions the surrogate recovers the low-rank matrix exactly (Candès and Recht, 2009).
The surrogate is a semidefinite program, and interior point methods for it do not scale past matrices of a few hundred rows. Ma, Goldfarb and Chen (2009) proposed a first-order method for the regularized form of the problem: a gradient step on the data-fit term followed by singular value shrinkage. Their algorithms FPC and FPCA are built on this two-line iteration, and the paper's one convergence theorem says that the iteration, run with a fixed step size, converges to a minimizer. This mission formalizes that theorem and the lemmas used to prove it.
Timeline of the closest results:
Fix natural numbers . Matrices carry the Frobenius norm and the nuclear norm . A linear map is given by matrices through ; equivalently for a matrix . Its adjoint is , and , the square of its spectral norm. Fix and .
Problem (1.8) is
and denotes its set of optimal solutions. Write for the gradient of the data-fit term and for a gradient step of size .
For , the matrix shrinkage operator takes a singular value decomposition to , where . The fixed point iterations (2.1) start from an arbitrary and repeat
For and every starting point, there is with
The goal fixes no rate and no particular limit: it asserts convergence of the whole sequence to some minimizer.
The mission also contains the paper's Theorem 2, the optimality condition for (1.8) written with a reduced singular value decomposition : if and only if some satisfies , , and . The chain to Theorem 4 does not use it.
Theorem 4 is the correctness guarantee for FPC and FPCA, which were among the first algorithms to solve nuclear norm regularized problems with matrices in the thousands of rows. It certifies that the output of the plain iteration is an exact minimizer in the limit, for every starting point and every step below . Lemmas 1–3 are the reusable part: non-expansiveness of the matrix shrinkage with a precise equality case, and the fixed point characterization of the optimal set, are the ingredients of every proximal gradient analysis with nuclear norm regularization.
Status: the theorem is proved on paper, and it is also a special case of the general convergence of forward–backward splitting. No machine-checked proof of it is known. The platform holds general forward–backward and inertial forward–backward convergence statements in Hilbert space (for example NesterovFB.Weak.theorem_3, InertialFB.IFB.theorem1_convergence) and the nonexpansiveness of abstract proximal maps (MoreauProx.Characterization.prox_nonexpansive). None is stated for the nuclear norm, for matrix shrinkage defined through the SVD, or with Ma, Goldfarb and Chen's equality cases. Formalizing this mission connects Mathlib's singular values to these operator-theoretic statements.
The obvious route goes through Fejér monotonicity: every step brings the iterate no farther from any minimizer, so the iterates are bounded and have a limit point. Two steps of this route do not come for free. First, the argument presupposes a minimizer; nothing in the hypotheses provides one, so the existence of an optimal solution of (1.8) has to be established from the data. Second, a limit point must be shown to be optimal, which requires the equality cases of Lemmas 1 and 2, not just the inequalities. Lemma 1's equality case concerns the singular value decompositions of two unrelated matrices whose singular vectors need not be aligned; non-expansiveness alone does not deliver it. Nonexpansive maps in general need not have convergent iterates (a rotation is nonexpansive), so continuity plus boundedness is not enough.
Matrix (Fin m) (Fin n) ℝ. The Frobenius norm, the nuclear norm (the sum of Mathlib's LinearMap.singularValues), the linear map as matrices Aop, its adjoint and spectral norm, and the shrinkage relation IsShrink are reused from the published Cai–Candès–Shen definitions.IsShrink ν Y X: is the shrinkage of for some reduced SVD (orthonormal columns, positive singular values). Every statement takes the shrinkage output as a variable with an IsShrink hypothesis. The paper's Definition 4 also allows zero singular values, which shrink to zero and change nothing.A complete development needs the SVD of real matrices in terms of Mathlib's singular values, the subdifferential of the nuclear norm, and a Fejér-monotone convergence argument in finite dimension. The first two are reusable for any nuclear norm or spectral function result, and contributions of general lemmas about singular value shrinkage (functionality of IsShrink, its proximal characterization) are welcome.
Inspection and revision cost money, but continued production can allow a deteriorating process to remain in a costly state. A controller therefore needs a rule that converts incomplete information about the process into an action. Ross's two-state model makes that decision precise: the process can be good or bad, the bad state persists until revision, and inspection reveals the current state. The observable state for decision making is a probability rather than the underlying process state. This setup is useful when quality is inferred from occasional inspection and actions must be chosen before the state is known. Ross proved structural results for discounted control in this model, including sufficient conditions for a policy with one inspection interval and for a policy with no inspection at all. Ross (1971)
The conditions in Theorem 3.7 use the model's optimal value itself. They are therefore structural tests for the shape of an optimal rule, rather than parameter-only design formulas. The preceding concavity, monotonicity and Lipschitz estimates explain which features of that value function support the tests. The mission records those estimates alongside the main result, so the target is a coherent part of the paper rather than an isolated inequality. Ross (1971), pp. 589–593
The belief is the probability that the production process is in the bad state at the beginning of a period. A good process becomes bad during a period with probability if it is not revised. A bad process remains bad. Thus producing without inspection changes the next belief to . The discount factor is . Producing without inspection has cost in the good state and cost in the bad state, so its expected current cost is . Inspection costs in either state, and revision costs in either state. The standing order is . The explicit records that is a cost and makes the quotient in Theorem 3.7 meaningful.
Write for the discounted value starting from belief . Inspection reveals the current state: the next belief is after observing a good process and after observing a bad one. Revision resets the next belief to . The three current-plus-continuation costs are
The Bellman equation is . A stationary rule is -optimal here when it chooses an action attaining this minimum at every admissible belief. This is the paper's decision rule criterion associated with equation (3). Ross (1971), p. 590, equation (3)
The first target is the sufficient condition for an optimal three-region rule. Set . If
there are thresholds such that an optimal rule produces for , inspects for , and revises for . The revise interval may be empty: if no admissible belief has revision as an optimal action, may exceed . If revision is optimal somewhere, the conclusion includes . This is a repair to the printed bound in Theorem 3.7(a); the proof on p. 593 explicitly lets a missing threshold be infinite. Ross (1971), pp. 592–593, Theorem 3.7(a)
The second target gives an optimal no-inspection rule. If
then some gives an optimal rule that produces below and revises from onward. A threshold above is allowed and means that the rule produces throughout the admissible belief interval. Both alternatives in the source's condition are retained. Ross (1971), p. 592, Theorem 3.7(b)
The theorem identifies two kinds of simple stationary rule that can be optimal despite the value function depending on an unobserved process state. It says more than the existence of an optimal action at each belief: the selected actions can be arranged in belief intervals, and in the second regime inspection can be omitted entirely. These statements provide a compact description of decisions over the full continuum . Ross (1971), Theorem 3.7
The result was proved in the 1971 paper. This mission asks for machine-checked Lean proofs of its two repaired clauses, the value equation, and the stated shape estimates. The definitions and finite-horizon bound can also support later formalizations of related belief-state control models. No proof of this mission's draft theorem is claimed merely by compiling its statement.
The action costs have different shapes as functions of belief: inspection and revision give affine and constant expressions, while the production alternative includes the value at an updated belief. The apparent order of their pairwise crossings does not by itself establish that one selected rule attains the minimum at every belief. Equalities at a threshold also matter, since the rule must be optimal at the boundary points. The printed upper bound on the last threshold fails when revision never minimizes the Bellman equation; imposing it without qualification would make the formal target false.
Lean represents a belief as a real number and restricts all claims to . It defines and obtains by taking the minimum of the three action costs with continuation , exactly as in equation (4). The value is the limit of these iterates; convergence and boundedness are part of the equation (3) milestone. This prevents an arbitrary function satisfying a convenient fixed-point hypothesis from replacing the value the paper studies. The rule types are total real-to-action functions, while optimality is checked for every admissible belief, including and both thresholds.
The paper's general Lemma 2.1 is represented by its scalar two-state instance. The finite-horizon Lipschitz bound and its limiting corollary use . The last quotient in Corollary 3.6 divides by , so that second inequality is stated under ; the first inequality, and the main theorem, cover . If , then . Lean's real division gives a zero quotient in that case; the two implications in Theorem 3.7 remain valid under this convention. The development needs reusable results about convergence of discounted value iteration, concavity and monotonicity on an interval, and elementary estimates for affine belief updates. Contributions establishing those results or proving either sufficient-condition clause are within scope.
A production process can deteriorate without an operator seeing its current condition. Producing a unit, inspecting the process, and revising the process have different immediate costs and different effects on what can be known or controlled next period. The operator therefore needs a rule based on a belief about deterioration, rather than on the hidden physical state. Ross's two-state model asks when the simplest rule, producing every period without inspection, is actually optimal over an unlimited discounted horizon Ross 1971.
The question matters whenever an action has a cost now but may reduce future losses. Paying for inspection only supplies information; paying for revision restores a deteriorated process. The answer depends on the bad-state production cost, the deterioration probability, the revision charge, and the weight assigned to future periods. A comparison of immediate costs alone cannot settle whether revision is worthwhile. Ross's Theorem 3.4 gives an exact boundary between a regime where producing forever is optimal from every initial belief and a regime where revision is forced when deterioration is nearly certain Ross 1971, Theorem 3.4.
There are two underlying states: good and bad. The current state is hidden, and is the probability that it is bad at the beginning of a period. Producing without inspection costs zero in the good state and in the bad state, so its expected immediate cost is . A good process becomes bad with probability in one period; a bad process remains bad until revision. Thus a period of production without inspection changes the belief to . These are the conventions of the paper's Section 3 Ross 1971, p. 590.
The other actions are inspection, at cost , and revision, at cost . Inspection reveals the current state: the next belief is when the state was bad and when it was good. Revision returns the process to the good state before its next transition, so the next belief is . The standing parameter conditions are , , and ; is the discount factor. The paper explicitly assumes and a discount factor in . Positive states the intended positive bad-state cost and makes the threshold comparison meaningful Ross 1971, pp. 588, 590.
For a future-cost function , the three Bellman alternatives at belief are , , and . Their minimum defines one step of finite-horizon value iteration, beginning with . The limit is the optimal discounted cost. Write for the rule that always produces without inspection, and define its cost from the actual discounted series Ross 1971, equations (3)–(5).
The first target establishes that value iteration converges on , gives a bounded solution to the two-state Bellman equation, and identifies that solution uniquely among bounded functions. The iterated update and Ross's equation (5) then evaluate the cost of :
The sensitivity milestones retain the exact finite-horizon factor in Lemma 3.5 and the infinite-horizon bound in Corollary 3.6. In particular, for ,
The mission goal is both clauses of Theorem 3.4. The always-produce rule is optimal from every initial belief exactly at and above the threshold
Below that threshold, revision is the unique minimizing action for beliefs sufficiently near from the left Ross 1971, pp. 591–592.
The theorem gives a parameter test for omitting both inspection and revision from an optimal policy in this model. Its second clause adds a local statement when that test fails: near certain deterioration, merely allowing revision as one optimal choice is insufficient; any optimal choice must revise. The sensitivity bounds quantify the effect of imperfect knowledge of the state and supply continuity of the value function used in the paper's treatment of that neighborhood Ross 1971, Theorem 3.4 and Corollary 3.6.
Ross proved these results in 1971. This mission asks for machine-checked proofs of the paper's exact statements in a concrete two-state discounted model. The reusable formal objects are the belief update, the three-action Bellman operator, finite-horizon values, and the always-produce cost series. The goal and milestones here are open formalization targets; their mathematical status as published theorems is distinct from their proof status in Lean.
The cost of always producing can be computed explicitly, but equality with the optimal value is a global assertion about all beliefs and all three available actions. A comparison at one belief does not certify optimality everywhere. The reverse implication also has to recover a parameter inequality from optimality of a policy, rather than from its immediate cost alone. The strict conclusion near requires control of the value as the belief varies; pointwise action comparison at does not itself establish an interval Ross 1971, pp. 591–592.
The Lean model uses real parameters and a real belief restricted to . It has three explicit actions and the exact right-hand sides of equation (3). Its value is the limit of iteration from , so matches the paper. Convergence, boundedness, and Bellman uniqueness are stated as a milestone. The always-produce cost is the infinite series of actual stage costs, with its closed form reserved for a separate milestone. Consequently, defining the cost by equation (5) cannot make that milestone true by definition.
The discounted-optimality claim for means for every . The phrase “every optimal policy revises” is represented by revision being strictly cheaper in the Bellman equation than both other actions; this expresses a unique minimizing action for a stationary decision at that belief. “Near ” means a one-sided neighborhood within . The second inequality in Corollary 3.6 is stated only when , because division by has a default value in Lean. The first inequality and Theorem 3.4 retain the case.
The development needs real series, limits, finite-horizon recursion, elementary inequalities, and bounded fixed-point reasoning. Proofs of the model-specific Bellman equation, cost identity, exact sensitivity bounds, and Theorem 3.4 are welcome. General tools for discounted Bellman operators or real-series identities would also be useful beyond this mission. No policy class is smuggled in as an arbitrary hypothesis: the value and the cost of are computed from the model data.
Scheduling independent jobs on unrelated parallel machines to minimize the makespan is one of the basic NP-hard problems of scheduling theory: each job has its own processing time on each machine, with no relation between machines, and the goal is to finish all jobs as early as possible. When the number of machines is part of the input, Lenstra, Shmoys and Tardos showed that no polynomial algorithm can come within a factor below 3/2 of the optimum unless P = NP. When the number of machines is a fixed constant, the picture is different: the problem admits a polynomial approximation scheme, a family of algorithms that reach any accuracy .
Such a scheme was already known. Horowitz and Sahni (1976) gave a fully polynomial approximation scheme for fixed , but its space requirement grows like . The second application of the Rounding Theorem in the 1987 report of Lenstra, Shmoys and Tardos is a scheme whose space is polynomial in the input size, in , and in . This mission formalizes the approximation guarantee of that scheme (Theorem 3 of the report).
Timeline:
There are machines and jobs. If job is scheduled on machine it takes time units, a positive integer; is the processing-time matrix. A schedule assigns every job to one machine. The load of machine is , the makespan is the largest load, and is the smallest makespan over all schedules.
Fix an integer deadline and an accuracy . Assigning job to machine is long if and short otherwise. A schedule of long assignments is a partial assignment of jobs to machines using only long assignments; its long load on machine is , and is admissible if for every .
For a threshold and deadlines , the linear program (LP) of the Rounding Theorem has a variable for every pair with , the constraints for each job, and for each machine. The residual LP of is (LP) for the jobs left unassigned by , with and .
The procedure , on input , tries every admissible ; if the residual LP is feasible it takes a vertex , rounds it to a 0-1 solution of the integer program (IP) of the Rounding Theorem, and combines the result with . It answers 'no' if no residual LP is feasible. A -relaxed decision procedure answers 'no' only when no schedule has makespan at most , and otherwise returns a schedule of makespan at most . The binary search of Lemma 1 runs such a procedure on deadlines between and , where is the makespan of the greedy schedule, and returns the best schedule found.
For every , every positive integer matrix , every , every LP solver , the procedure run with exists, and the binary search driven by any such procedure returns a schedule with
Theorem 3 shows that for a fixed number of unrelated machines, the makespan can be approximated to any accuracy in polynomial time while keeping the memory polynomial in . It is an early instance of the pattern "enumerate the large items, solve an LP for the small ones, round", which recurs in later approximation schemes for scheduling and packing. Together with the 2-approximation of the same paper (mission 1 of this series) and the 3/2 hardness bound (mission 3), it delimits what is achievable for unrelated machines.
The theorem is proved in the paper; none of it is known to have a machine-checked proof. Formalizing it requires a precise account of the enumeration of long assignments, the residual LP, and the binary search, and it exercises the Rounding Theorem, which this series poses in mission 1, outside its original setting (with a non-integral threshold ).
The arithmetic of the scheme is short; the content lies in the Rounding Theorem, which turns a vertex of the residual LP into a 0-1 schedule exceeding each deadline by at most the threshold. The obvious argument, rounding an arbitrary feasible LP solution, fails: a non-vertex solution may split many jobs across many machines, and rounding them can overload a machine by far more than . The bound depends on the structure of vertices of (LP), which an arbitrary feasible point does not have. A second difficulty is the count of milestone 1, which must be done with a real exponent and a strict inequality.
Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive. Load, makespan and optimal schedules are those of the published MatousekLP.Scheduling.Schedule, applied to the real cast of P.Set.extremePoints of its feasible region. Variables absent from the paper's (LP) are kept as matrix entries fixed to , which leaves the vertices unchanged.Real.rpow.Welcome contributions: a proof of the Rounding Theorem in the generality of real deadlines and thresholds, proofs of the counting bound, and lemmas on the binary search that are reusable for any relaxed decision procedure.