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.
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?
A learning algorithm that picks a function from a class by minimizing an empirical average is only as good as the gap between the empirical average and the true mean , uniformly over the functions it might choose. The classical way to control this gap uses a global complexity of the whole class, such as its Rademacher average, and yields rates of order . These rates are too slow in many problems of statistics and learning theory, where the functions that matter (those close to the best one) have small variance. Bartlett, Bousquet and Mendelson (arXiv:math/0508275, Annals of Statistics 33 (2005) 1497–1537) showed that the gap can instead be controlled by a local complexity, the Rademacher average of the small-variance part of the class. The resulting bounds give fast rates, often of order , and the paper is the standard reference for this method in empirical process theory and statistical learning.
The method builds on Koltchinskii and Panchenko (2000), Massart (2000) and Lugosi and Wegkamp (2004), and its concentration step uses Bousquet's form of Talagrand's inequality (2002). It is the basis of the fast-rate analyses in Koltchinskii's 2006 Annals of Statistics paper on local Rademacher complexities and oracle inequalities, and in later work on variance-regularized risk minimization.
Let be a probability space and independent random variables with law . For a function write
Let be independent signs, . For a class of functions, the empirical Rademacher average is
the expectation over the signs with the sample fixed, and the Rademacher average is its expectation over the sample.
The star-hull of around is . A functional assigns a number to each function; it plays the role of a variance proxy (for instance or ).
A function is sub-root if it is nondecreasing and is nonincreasing on . A nontrivial sub-root function has a unique positive fixed point , the solution of (Lemma 3.2 of the paper).
Let be a class of functions with values in , , and a functional with , and for , . Let be sub-root with fixed point and assume, for every ,
Then for every and , with probability at least ,
and, with probability at least ,
The theorem replaces the global complexity that a direct application of Talagrand's inequality would give by the fixed point , which is never larger and is often much smaller. For a class with a Bernstein-type variance condition (, as for excess losses of empirical risk minimizers), is of order for VC-type classes and of order of the eigenvalue tail for kernel classes, which yields the fast rates of the paper's Sections 4–6. The second part, formalized here, gives better constants than the first by working with the star-hull of the class, and it is the version the paper's later results (Theorem 4.1 and its corollaries) are built on.
On the formal side, nothing of local Rademacher theory is in Mathlib or, beyond the definitions reused here, on the platform. The concentration inequality used in the proof (Theorem 2.1, from Bousquet's form of Talagrand's inequality) is posed but unproved on the platform. A complete formalization would make the fixed-point machinery available to every fast-rate result built on it. The paper's printed constants for this statement are wrong (see below), so a machine-checked version also settles which constants the argument supports.
The obvious approach applies a concentration inequality directly to and bounds the complexity term by a single Rademacher average; this loses the variance information and gives only rates. The localized argument needs a level that is simultaneously above the fixed point and large enough that the deviation of the rescaled class is at most . Converting a bound on the rescaled class back into a bound on requires the multiplicative structure of . The probabilistic core is Talagrand's concentration inequality for suprema of empirical processes with Bousquet's constants, whose proof (entropy method) is the main piece of missing infrastructure. Measurability of the suprema involved is a separate technical obstacle.
X → ℝ on a measurable space with a probability measure P; the sample is s : Fin n → X under the product measure, with n ≥ 1. is empMean s f, is empRademacher (the average over all sign vectors of a real supremum, without absolute value), is expRademacher, and IsSubRoot is Definition 3.1; these are reused published definitions.empRademacher; elementary sub-root calculus. The sub-root lemmas and the containment step are reusable by any later mission on local Rademacher complexities.A binary classifier is judged by its misclassification probability, the chance that it mislabels a fresh example. That probability is unknown; what a learner sees is the training error, the fraction of mistakes on the sample it was trained on. A generalization bound controls the gap between the two simultaneously for every classifier in a class, so that a classifier chosen by looking at the data still has a guaranteed error. The classical bounds of Vapnik and Chervonenkis measure the class by its VC dimension, a fixed combinatorial quantity that does not depend on the data distribution, and the paper recalls evidence that such fixed complexity penalties cannot be universally effective for model selection (p. 464).
Bartlett and Mendelson's paper in the Journal of Machine Learning Research (2002) studies two data-dependent alternatives, the Rademacher and Gaussian complexities, and proves risk bounds and structural rules for them. This mission formalizes the paper's classification bound, Theorem 5(b), which replaces the VC penalty by half the Rademacher complexity of the class. The source is the published JMLR article (jmlr.org/papers/v3/bartlett02a), pp. 463–482; all page numbers below are the journal's.
Timeline. Uniform convergence of empirical frequencies with a VC-dimension rate is due to Vapnik and Chervonenkis (1971). Rademacher penalties for model selection were introduced by Koltchinskii (2001) and by Bartlett, Boucheron and Lugosi (2002), who also proved Theorem 5(a) with the maximum discrepancy. The 2002 paper proves part (b) in Appendix B (p. 480) by adapting its proof of the general risk bound, Theorem 8 (p. 467).
Let be a measurable space and a probability distribution on ; a pair is an example with label . Let be a set of -valued functions on (the classifiers), and let be an i.i.d. sample drawn from .
and the Rademacher complexity is with i.i.d. (Definition 2, p. 464). Note the factor and the absolute value.
For every , with probability at least over the sample, every satisfies
The bound is uniform: the probability that some violates it is at most .
Supporting platform items, referenced and not restated: McDiarmid's inequality for i.i.d. samples (StabGen.Uniform.mcdiarmid_inequality, open) and the symmetrization lemma in the normalization of Shalev-Shwartz and Ben-David (UnderstandingML.representativeness_le_rademacher, proved).
The result. Theorem 5(b) is a distribution-dependent risk bound for classification whose complexity term can be estimated from a single sample. The paper shows (Theorem 6, p. 465) that it is never much worse than the VC bound, since the empirical Rademacher complexity of a class is in terms of its empirical VC dimension , and it can be much better. It also serves as the template for margin bounds for large-margin classifiers, kernel machines and voting methods in Section 4 of the paper.
Formalizing it. The result is proved in the paper; no machine-checked proof is known to exist. A formal proof needs McDiarmid's inequality, a symmetrization argument with a ghost sample, and the reduction of the 0–1 loss class to the classifier class through the identity . The milestones split these, so they can be proved independently. The symmetrization milestone also corrects a printed slip (see Formalization scope).
The bounded-difference step and the final union of the two halves are short. The difficulty is in the symmetrization. The supremum over an uncountable class is not automatically measurable, so the expectations in the paper's chain need not exist as written; a proof must work with exactly the random variables it integrates and use only the measurability it is given. The exchange of a sample point with its ghost copy, the conditioning on the sample, and the replacement of by must each be justified on finite sign averages and product measures. The obvious shortcut, bounding the gap by the Rademacher complexity of the loss class , does not give the stated term: with the absolute value of Definition 2, the loss class's complexity is not , because contributes a sign sum that does not depend on .
Lean conventions:
ENNReal.ofReal on the real terms.Hypotheses added relative to the page, each necessary or a reading of the page:
UnderstandingML.representativeness_le_rademacher. They hold, for instance, for countable classes.Corrected slip: the chain on p. 480 ends "". The last equality is only "": carries an absolute value, and for the left side of that step is while . The symmetrization milestone states the chain's conclusion with , which is all Theorem 5(b) needs.
Not a valid formalization: a version with a real-valued supremum or Bochner integral for (which would read on an unbounded or non-integrable class and make the bound false or free), one that drops the absolute value or uses the normalization, or one that measures of the loss class instead of . Theorem 5(a) (maximum discrepancy, due to Bartlett, Boucheron and Lugosi) is not part of this mission.
Contributions welcome: proofs of the three milestones and the goal; the general McDiarmid inequality (the referenced open item); and reusable lemmas on measurable suprema of classifier families.
A learning algorithm picks a predictor from a class after looking at training examples, and the quantity of interest is its expected loss on a fresh example. Since depends on the data, its training error is a biased estimate of that loss, and a risk bound quantifies the bias uniformly over the class: with high probability, every has expected loss at most an observable sample average plus a complexity penalty. Classical penalties (VC dimension, covering numbers, fat-shattering dimension) are fixed in advance; data-dependent penalties such as the Rademacher complexity can be estimated from the sample itself and adapt to the distribution, which matters for model selection by complexity regularization.
Bartlett and Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results (JMLR 3, 2002, jmlr.org), state such a bound in a general decision-theoretic setting (Theorem 8, p. 467): the loss is any -valued function of an outcome and an action, and the sample average is taken of a dominating cost , which may be Lipschitz and hence amenable to the structural results of the paper's §3 even when is a discontinuous – loss. Multiclass classification with error-correcting output codes is the paper's example. The ingredients — McDiarmid's inequality (McDiarmid, 1989) and symmetrization — are standard; the paper combines them for this setting with a centred cost class. The source is the published JMLR article (pp. 463–482); all page numbers below are its printed pages.
Let be an input space, an output space and an action space with a distinguished action , each a measurable space. A probability measure on generates independent examples , and is a fresh draw from .
with independent uniform signs, and the Rademacher complexity is , the expectation over an i.i.d. sample (Definition 2, p. 464). The factor is and the absolute value is inside the supremum.
In Lean these are RadGauss.RiskBound.empiricalRademacher, rademacherComplexity, empMean, supDev (the uniform deviation ), doubleSupDev and phiTildeComp.
For every integer and every , with probability at least over the sample, every satisfies
The event is uniform over . The constant is the printed one.
The platform's Proved UnderstandingML.representativeness_le_rademacher (Shalev-Shwartz and Ben-David, Lemma 26.2) is included as a supporting reference: it is the middle inequality of milestone 5 in the , absolute-value-free normalization.
Theorem 8 bounds the expected loss of any predictor in the class, including one selected by the data, by quantities the learner can compute or estimate: the empirical cost and the Rademacher complexity of the centred cost class, which concentrates around its empirical version. Combined with the paper's structural results (§3: contraction by Lipschitz maps, convex hulls, sums), it yields margin bounds for voting methods, neural networks and kernel machines (§4) from complexities of simple base classes. Centring by matters: with the absolute value inside the supremum, can exceed by order even for a single function.
The result is proved in the paper. As far as the platform's catalog shows, it has no machine-checked proof in this normalization; McDiarmid's inequality in the non-identically distributed form, the bounded-difference step and the absolute-value Rademacher symmetrization with factor are not on the platform. A Lean proof would give a reusable risk-bound template for any loss dominated by a bounded cost.
The obvious argument — bound for a fixed by Hoeffding's inequality — does not survive the choice of after seeing the data: the deviation must be controlled uniformly over , and is typically infinite. The supremum over is a single random variable, but its expectation is not obviously small, and relating it to the Rademacher complexity requires a ghost sample and a sign-swap symmetry of the product measure. In a formal development, the supremum of an uncountable family is not automatically measurable; the expectations the argument manipulates must be genuine, not lower integrals, which is why the statements carry explicit measurability hypotheses. McDiarmid's inequality itself, for independent but not identically distributed coordinates, is a martingale-difference concentration argument that is not in Mathlib in this form.
S : Fin n → X × Y, its law the product Measure.pi (fun _ => P). "With probability at least , every satisfies …" is encoded by bounding the (outer) measure of by , with .Fin n → Bool, true ) of -valued suprema; is its Lebesgue integral. The goal is stated in , with the real terms embedded by ENNReal.ofReal (all are nonnegative). A real supremum or a Bochner integral would silently return on an unbounded class or a non-integrable integrand, making the bound trivially false or vacuous; this is ruled out by the choice of codomain.[Zero A]).UnderstandingML.representativeness_le_rademacher.Contributions welcome: a proof of McDiarmid's inequality for Measure.pi (reusable well beyond this mission), the ghost-sample symmetrization with the sign-swap invariance of , and the final assembly.
The newsvendor problem is the basic model of inventory under uncertain demand. A decision maker orders units before demand is observed, and pays a unit backordering cost for each unit of unmet demand and a unit holding cost for each unit left over. When the demand distribution is known, the optimal order is a quantile of it. In practice the distribution is unknown and the decision maker holds historical data, often including features: observable covariates such as the day of the week, the weather or a recent sales trend, recorded alongside each past demand.
Rudin and Vahn (MIT Sloan Working Paper 5036-13, version of February 6, 2014, from MIT DSpace; published as Ban and Rudin, Operations Research 67(1), 2019, doi:10.1287/opre.2018.1757) propose to learn the order quantity directly as a linear function of the features, by minimizing the empirical newsvendor cost over the training data, with or without a regularization penalty. Their question is the one any data-driven decision rule must answer: how much worse can the learned rule do on new data than it did on the data it was fitted to? When the number of features is comparable to the sample size ("big data"), a bound that grows with says nothing, and the paper's Theorem 2 gives one for the regularized rule that does not depend on .
This mission formalizes that bound, Theorem 2 of the working paper, together with the results its proof is assembled from. All page and result numbers refer to the 2014 working paper, not to the published article.
Cost. For an order and a demand , the newsvendor cost is
Write .
Data. A data point is a pair of a feature vector and a demand . Features lie in a domain inside the ball , and demands lie in . A sample consists of independent draws from an unknown probability distribution concentrated on .
Rules and risks. A vector defines the linear decision rule . Its true risk and empirical risk are
The regularized algorithm (NV-reg). For a parameter , the rule minimizes
The objective is strictly convex, so the minimizer is unique. Following Appendix B of the paper, the rules the algorithm outputs on samples from are assumed to map into (the paper's ): the learned order quantity is never negative and never exceeds the demand cap.
Uniform stability. An algorithm is uniformly stable with parameter if removing one observation from any sample changes the loss of its output at any test point by at most (Bousquet and Elisseeff's Definition 6, the paper's Definition 1).
For every and , with probability at least over ,
The dimension appears nowhere in the bound.
The result. Theorem 2 bounds the generalization gap of the regularized feature-based newsvendor rule at rate with constants that depend on the costs, the demand cap, the feature radius and , but not on the number of features. It gives a theoretical basis for regularizing when is not small, and it indicates how to scale with the feature radius. The companion bound for the unregularized rule (Theorem 1) grows linearly in .
Formalizing it. The theorem is proved in the paper, but its proof is short and relies on cited results: Theorem 5 and Theorem 6 are stated with references to Bousquet and Elisseeff and no proof of their own, and the paper's Theorem 6 is a two-sided variant of Bousquet and Elisseeff's Theorem 12 that is only sketched. None of these results has a machine-checked proof. A formalization produces a checked two-sided stability-to-generalization theorem for general algorithms (reusable for any stable learner), a checked stability bound for a regularized piecewise-linear loss, and the newsvendor bound itself, with the constants the proof actually supports.
The bound is not a uniform-convergence argument: the class of linear rules on has complexity growing with , so any bound that holds simultaneously for all rules in the class depends on . The bound must exploit the specific rule produced by the algorithm. The two analytic steps that carry this are the stability of the regularized minimizer, which needs a strong-convexity comparison between the full and the leave-one-out objective, and a concentration inequality of bounded-differences type for a function of the whole sample whose differences are controlled only through stability.
The leave-one-out comparison is a known pitfall. If the leave-one-out problem is run literally on points it carries the weight , and the comparison argument then gives twice the constant of Theorem 4. The stated constant holds for the leave-one-out objective that keeps the weight , which is the form of Theorem 5.
Representation. Features are EuclideanSpace ℝ (Fin p), rules are vectors acting by the inner product, and data points live in EuclideanSpace ℝ (Fin p) × ℝ. The cost is the published newsboy loss with overage cost and underage cost ; the empirical and true risks are the published empirical and generalization errors, and the (NV-reg) objective and its -weighted leave-one-out version are the published regularized objectives of Bousquet and Elisseeff. The regularizer is (the display prints both and ; the text calls the problem a quadratic program). "With probability at least " is stated as: the event on which the gap exceeds the bound has measure at most under the product measure .
Standing assumptions and pinned hypotheses.
Trivializing formalization ruled out. The range assumption is quantified only over feature vectors in and over samples drawn from ; stated over the whole ball , it would force (both and would lie in ) and the goal would be nearly empty.
What is needed and reusable. McDiarmid's two-sided bounded-differences inequality under product measures; integrability of bounded measurable losses; existence and properties of minimizers of strongly convex objectives on ; the comparison argument behind Theorem 5. Theorem 6 is stated for an arbitrary data space and hypothesis space and is reusable for any uniformly stable algorithm. Contributions to the Theorem 5 reference and to McDiarmid's inequality benefit other missions as well.
Prove that -SAT is NP-complete for every fixed , with at most literal occurrences per clause.
Construct the reductions and certificate verifier using the existing WordRAM definitions. We reuse proved polynomial backend and Cook–Levin SAT completeness.
Many systems consist of units that form themselves into clusters: individuals at a gathering forming conversational groups, monomers forming polymers, particles coagulating and fragmenting. Chapter 8 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) treats such clustering processes as Markov processes whose state counts the clusters of each type, and shows that when the process is reversible its equilibrium distribution has an explicit product form. The chapter opens with a model of social grouping (§8.1), develops a general basic model (§8.2) and later applies it to polymerization (§8.4).
The basic model sits in the same family as the migration processes and queueing networks of the earlier chapters: the method is to guess reversibility, solve the detailed balance equations, and normalize. Its specific feature is that the transitions are unions and break-ups of clusters, with rates quadratic in the cluster counts, rather than movements of single individuals.
There is a countable collection of cluster types . A state is a vector of non-negative integers, being the number of -clusters present, with only finitely many non-zero. For cluster types let be the -th unit vector and
the union of an -cluster with an -cluster into a -cluster, and the break-up of a -cluster into an -cluster and an -cluster. Given non-negative parameters and , the clustering process has transition rates
A closed clustering process lives on a finite irreducible state space . The open clustering process additionally lets one-clusters enter at rate and leave at rate ,
and its state space is the countable set of all with finite, every state being reachable from every other.
An equilibrium distribution is a collection of positive numbers summing to one that satisfies the equilibrium equations ; the process is reversible in equilibrium exactly when satisfies the detailed balance conditions .
If there are positive numbers with
then the open clustering process has equilibrium distribution
it is reversible, and the counts are independent, being Poisson with mean .
Theorem 8.2 gives the equilibrium of a whole class of coagulation–fragmentation dynamics in closed form: the cluster counts are independent Poisson variables, and the equation system (8.8) is the only thing to solve. Quantities such as the expected number of clusters of each type, or the proportion of units in clusters of a given size, are then read off directly. Theorem 8.1 gives the corresponding result for a closed system, where the normalizing constant couples the types; opening the system removes that coupling. The results are the base of the polymerization models of §8.4 and of the later literature on reversible coagulation–fragmentation processes.
The results are proved in the book, with short proofs that state the detailed balance computation is "readily verified". To our knowledge they have no machine-checked proof. The work this mission asks for is the formal verification of that computation for the aggregated rate function, including unions in which two clusters of the same type meet, and the normalization of an infinite product over a countable set of types, which the book takes for granted.
The book calls the detailed balance computation readily verified; the bookkeeping is where a formal check can fail. Two different unions, or a break-up and the entry of a one-cluster, can lead from the same state to the same state when a cluster type is reproduced by the transition, so the rate between two states is a sum over transitions, and the identity has to be checked for the sums, not for single transitions. The same-type case carries the falling factorial rather than .
The normalization is the second difficulty. The state space of the open process is countably infinite, the product (8.10) runs over infinitely many types, and the interchange that makes it sum to one requires (8.9). Without (8.9) the weights are not summable; this is the content of the book's remark that (8.9) is necessary.
Cluster types are an arbitrary countable type R carrying a linear order, used only to count each unordered pair of types once. States are finitely supported vectors R →₀ ℕ. The rate is the sum of the rates (8.3) of all unions and break-ups taking to , plus, for the open process, the rates (8.7); a transition is present only when the clusters it consumes exist, and holds because every transition changes the number of clusters. The one-cluster type is a distinguished element one. The closed state space is a finite non-empty set closed under positive-rate transitions and irreducible. The open process carries the book's assumptions that every state is reachable from every other and that the total rate out of each state is finite.
The statements are at the level of rates: reversibility is detailed balance for a positive, normalized , the equivalence with reversibility of the stationary process being Kelly's Theorem 1.3. That is the law of a stationary Markov process with these rates is not formalized. Independence and the Poisson laws are stated as the joint law of every finite set of counts. A formalization in which may vanish, in which detailed balance is imposed only for a degenerate choice of rates, or in which (8.10) is not normalized does not meet the goal: the are positive, the rates are arbitrary non-negative symmetric parameters, and both detailed balance and total mass one are required.
The development uses the published definitions KellyStochasticNetworks_Balance (detailed balance and the equilibrium equations) and the proved implication from detailed balance to the equilibrium equations. Lemmas on summing products over finitely supported vectors, and on infinite products of exponentials, are reusable beyond this mission. Lemma 8.3, a partial converse to Theorem 8.1, is not part of this mission; a faithful statement of it, with the units structure of the clusters, is a welcome addition.
Chapter 4 of F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) applies the product-form theory of Chapter 3 to concrete systems. Two of its results have numbered statements, and they answer two practical questions.
The first comes from the design of store-and-forward communication networks (telegraph and packet-switched data networks). Messages queue at channels; the designer chooses each channel's capacity subject to a budget, and wants to minimize the delay messages suffer. Because the equilibrium law at every channel is geometric under several different modelling assumptions (§4.1, pp. 95–96), the mean delay has a closed form, and the budget allocation problem becomes a small convex program with an explicit solution. This square-root capacity assignment goes back to L. Kleinrock's work on communication nets (Communication Nets, McGraw-Hill, 1964) and remains the textbook example of optimal design for a network of queues.
The second comes from compartmental models in biology, birth–illness–death processes and manpower planning (§4.5, pp. 113–115). Individuals enter a system as a Poisson stream and move through it independently. Equilibrium results follow from Chapter 3; Theorem 4.2 describes the transient behaviour exactly, starting from an empty system.
Capacity allocation (§4.1). A network has channels. Channel receives traffic at average rate and is given capacity . In equilibrium the number of messages at channel has the geometric law (4.1),
which requires . Its mean is . Capacity on channel costs per unit and the total budget is , giving the cost constraint (4.2)
The mean number of customers in the network is
and the feasible set is the set of with for every that satisfy (4.2). In Lean these are meanNumberInNetwork a φ and FeasibleCapacities a f F. The proof works with the Lagrangian lagrangian a f F y φ .
Compartmental model (§4.5). Individuals arrive in a Poisson stream of rate at a system of compartments that is empty at time . Let be the probability that an individual is in compartment a time after its arrival; and , since individuals may leave. Let be the number of individuals in compartment at time , and
In Lean the model is the predicate IsCompartmentModel P ν t p M T Loc, the counts are compartmentCount M Loc j, and is alpha p j t.
If , , and , then
is feasible and minimizes over the feasible set, and every other feasible has .
The proof's generating-function identity, for ,
and the theorem itself: are independent and is Poisson with mean .
Theorem 4.1 is a closed-form design rule. Every channel first receives the capacity needed to carry its traffic; the remaining budget is shared in proportion to , not to the traffic . Sizing capacity in proportion to the load, which is the obvious rule, is therefore not optimal. The same calculation applies to any network whose stations have the geometric law (4.1), for example a manufacturing job shop (p. 97). The mean number in the network and the mean time a customer spends in it are minimized together.
Theorem 4.2 is the exact transient law of a network of infinite-server queues started empty. It holds however complicated the motion of an individual is, provided individuals move independently, and letting it recovers the equilibrium Poisson law of §4.5.
Both results are classical and proved in the book. Neither is formalized on Prove2Me. The platform has the geometric equilibrium law of the M/M/1 queue (KellyStochasticNetworks.mm1_equilibrium) but not its mean, and no result on Poisson thinning or marking by independent random locations. The formal work for Theorem 4.1 is a strict-convexity and Lagrangian-sufficiency argument in . For Theorem 4.2 it is a Poisson marking theorem in measure-theoretic probability. Both pieces are reusable.
For Theorem 4.1, the book's proof sets the partial derivatives of the Lagrangian to zero. A stationary point is not a global minimizer in general, so the formal proof must show that is (strictly) convex on the open region , and it must use Lagrangian sufficiency, not first-order conditions alone. The region is open and the objective is unbounded near its boundary. Feasibility of needs , which the book leaves implicit.
For Theorem 4.2, the steps of the proof that read "conditional on " have to be carried out with measure-theoretic independence. One step averages a product over independent uniform instants. Another sums the Poisson mixture into an exponential. The last turns a factorized generating function into mutual independence of counts with Poisson marginals. Mathlib has the Poisson distribution (ProbabilityTheory.poissonMeasure) but no marking or thinning theorem, and no uniqueness theorem for multivariate probability generating functions.
Channels and compartments are indexed by Fin J; all rates, costs and capacities are real numbers.
Theorem 4.1. The statement carries the book's implicit hypotheses explicitly: , , , . Stability is part of the feasible set. The conclusion is global optimality over the feasible set (IsMinOn) together with feasibility of , plus strict optimality against every other feasible point. Uniqueness is a slight strengthening of the book's "the optimal allocation is", and it holds by strict convexity. A statement that satisfies (4.2), or that it is a stationary point of the Lagrangian, is not the theorem: those are one-line computations or the proof method, and the goal is stated as global optimality to rule them out.
Theorem 4.2. The model is pinned down as in the proof on p. 115:
"Individuals move independently" is formalized as this conditional independence. The are measurable sub-probabilities, not assumed to sum to one. The conclusion is mutual independence of the counts (iIndepFun) together with the Poisson probability mass function of each. Infinite time horizons and the point-process description of the system are out of scope.
Useful contributions: a reusable Lagrangian-sufficiency lemma for separable convex objectives under one linear constraint; a Poisson marking (colouring) theorem for finitely many colours; the multivariate generating-function uniqueness lemma for -valued random vectors.
A migration process is a continuous-time Markov model of a population spread over sites, called colonies, in which individuals move one at a time: between colonies, out of the system, or into it from outside. The model was introduced by Whittle (1967) and Kingman (1969) and is the framework of Chapter 2 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979). It covers closed and open networks of queues (Jackson networks), linear population models and the movement of particles between cells. Its central fact is that the equilibrium distribution is a product form: the joint law of the colony sizes factorizes into one term per colony, and for open processes the colony sizes are independent in equilibrium.
In the migration processes of Chapter 2 the rate at which an individual leaves colony depends on the number there, but not on the number already present in the colony it joins. Chapter 6 (§6.1) lifts this restriction. The rate of a move into colony is multiplied by a function of the receiving colony's occupancy, which can model blocking (a crowded colony slows arrivals) or attraction (as in the models of social grouping of §6.2). The price is that product form survives only under a reversibility condition on the routing parameters. This mission formalizes the two theorems of §6.1 on top of the already-formalized results of Chapter 2.
Timeline. Whittle (1967) and Kingman (1969) introduced migration processes and their product-form equilibria; Kelly (1976) treated networks of queues with general routes; Kelly (1979, Ch. 2) states the closed and open product forms (Theorems 2.3, 2.4) and the time reversal of an open process (Theorem 2.5); Kelly (1979, §6.1) states the reversible versions with receiving-colony dependence (Theorems 6.1, 6.2).
There are colonies. The state is , with the number of individuals in colony . Three operators change the state by one individual: moves one individual from colony to colony , removes one from colony , and adds one to colony .
The model is given by non-negative constants (with ), , , and functions with , for , and for all . A closed reversible migration process with individuals has state space and transition rates
An open reversible migration process has state space and, in addition to (6.2), the rates
The parameters are required to make the process irreducible: in the closed case an individual can pass between any two colonies along pairs with ; in the open case it can reach every colony from outside and leave from every colony. Setting recovers the migration processes of Chapter 2.
Given positive constants , the candidate equilibrium is
with chosen so that sums to one over the state space.
If positive satisfy
and every colony series converges, then (6.3) with is in detailed balance with the rates (6.2), (6.5), (6.6), satisfies the equilibrium equations, is positive and sums to one, and under it are independent with marginals .
Theorems 2.3–2.5 are already proved on the platform and enter as references.
The result. Theorem 6.2 shows that product form and independence of colony sizes are not tied to routing that ignores the destination's occupancy. Any positive is allowed, provided the routing is reversible in the sense of (6.4) and (6.7). This is what makes the social-grouping models of §6.2 and the clustering models of Chapter 8 tractable, and it identifies (6.4) as the structural condition: Exercise 6.1.1 shows that without it the process cannot be reversible. Through Theorem 1.3 of the book, detailed balance also gives that the stationary process looks the same run backwards in time.
Formalization. The Chapter 2 results (Theorems 2.3–2.5) are formalized and proved on the platform, at the level of transition rates, in the KellyStochasticNetworks series. Theorems 6.1 and 6.2 are not formalized anywhere to our knowledge. The new work is the detailed-balance verification with the receiving-colony factor, the normalization over the finite set in the closed case, and the summation over the countable space with the marginal computation that expresses independence in the open case.
The equilibrium equations of a migration process with blocking have no simple solution in general (p. 135); a direct attack on the full balance equations does not close. Detailed balance is a local condition, but the formal statement has to be careful with transitions that do not exist: a move out of an empty colony, a departure that would make a count negative, and the coincidences between operators at the boundary ( when ). In the open case the bookkeeping is in infinite sums: positivity and normalization need convergence of each colony series, and independence needs the marginal of on one colony to be computed as a sum over the remaining coordinates.
Colonies are Fin J; states are Fin J → ℕ; rates are real-valued functions of two states, assembled as sums of indicator terms over the possible transitions, reusing the operators Tjk, Tout, Tin and the predicates DetailedBalance, FullBalance of the published definitions KellyStochasticNetworks_Migration and KellyStochasticNetworks_Balance. Transitions out of an empty colony carry the factor and so vanish. The hypotheses , non-negativity of the rates, positivity of (), () and , and the book's irreducibility requirements are binders of each theorem.
The statements are at the level of transition rates: "reversible" is read as detailed balance of the equilibrium distribution, and "equilibrium distribution" as positive, summing to one, and satisfying the equilibrium equations. The stochastic process itself is not constructed. In the closed case the distribution lives on and vanishes off , which is equivalent because every transition preserves ; is assumed so that is nonempty. In the open case stationarity is the convergence of each colony series, carried as HasSum hypotheses with sums .
The normalizing constant is never free: satisfies detailed balance, so a statement that leaves unconstrained, or omits the factor from (6.2), (6.6) and (6.3), is not this theorem. Contributions welcome: proofs of Theorem 6.1 and 6.2, reusable lemmas on detailed balance for indicator-sum rates, and on products of summable families over Fin J → ℕ.
A mixed state of a -dimensional quantum system is a positive semidefinite matrix of trace . Writing down takes about real numbers, and is exponential in the number of qubits, so learning in full is expensive. Holevo's theorem and the random access code bounds of Ambainis, Nayak, Ta-Shma and Vazirani say that an -qubit state carries far fewer usable classical bits than its amplitudes suggest. Shadow tomography, introduced by S. Aaronson (arXiv:1711.01053), makes this quantitative: given known two-outcome measurements , how many copies of an unknown are needed to estimate every acceptance probability to within ?
Aaronson shows that copies suffice, polylogarithmic in and . The question this mission addresses is the converse: how many copies are necessary. Section 6 of the paper proves two lower bounds. Theorem 16 gives even when and the are diagonal (a classical distribution). Theorem 19, the goal here, strengthens the dimension term to for genuinely quantum states.
Timeline:
Fix a dimension . A two-outcome measurement is a Hermitian matrix with ; it accepts with probability . The tensor power is the matrix of independent copies. A strategy using copies is a measurement of with finitely many outcomes , given by positive semidefinite matrices with , together with outputs . It succeeds on when, with probability at least over , for every .
The proof works with these further objects, all defined in the mission:
There are a universal constant and a threshold such that for all , all with and all , some measurements on force every strategy that succeeds on every mixed state to use
copies. The goal fixes only the shape , not a constant, so a sharper constant does not invalidate it.
The milestones follow the proof, which sets and :
Theorem 19 shows that the dependence of shadow tomography cannot be removed, and that for shadow tomography is as hard as full tomography: as grows the bound becomes the tomography lower bound, which it therefore contains. Compared with the classical Theorem 16, it shows that quantum states need quadratically more copies in the dimension term. The factor matches the upper bound of Proposition 20 for the decision version, so the -dependence of the lower bound is tight in that setting.
The results are proved in the paper; none of them has a machine-checked proof that we know of. Formalizing the argument requires von Neumann entropy and its additivity on tensor products, the bound , a Holevo-plus-Fano step that turns successful estimation into mutual information, and the existence of many nearly orthogonal half-dimensional subspaces. Each is reusable well beyond this mission.
The obvious attempt adapts the classical argument of Theorem 16, which hides subsets of in a biased distribution. Quantum states allow hidden subspaces instead of subsets, which is where comes from, but two steps change character. First, the hiding family must be shown to exist: Eq. (2) is a concentration statement for random subspaces, and the lemma the paper cites for it (Lemma 18) is misstated, as explained below. Second, the information bound must be carried out for quantum states: the step "learning from requires " needs Holevo's bound and Fano's inequality, adjusted for success probability rather than certainty.
Matrices are Matrix n n ℂ over a finite index type; the goal uses . Conventions committed to:
WildeQIT.IsDensityOperator (positive semidefinite, trace ), reused as a reference item.Fin k → Fin D, with deterministic outputs ; classical randomness can be absorbed into the outcome set.vnEntropy returns on non-Hermitian matrices, which no statement uses.A trivializing formalization is ruled out: the goal does not mention , , , or , the success condition quantifies over all mixed states rather than a vacuous class, and the measurements are fixed before the strategy.
Not drafted:
Contributions welcome: proofs of the milestones; a Haar-measure version of Eq. (2); von Neumann entropy infrastructure (additivity, the dimension bound, concavity); Holevo's bound and Fano's inequality for finite-dimensional states.
Many problems in optimization, image reconstruction and statistics reduce to the convex feasibility problem: given closed convex sets , , find a point of their intersection . A classical approach is the relaxation method: from the current point, move to the nearest point of one of the sets, and repeat. For Euclidean distance and half-spaces this is the method of Agmon and of Motzkin and Schoenberg (1954); for hyperplanes it is Kaczmarz's method.
L. M. Bregman's 1967 paper replaced the Euclidean distance by an abstract function satisfying six conditions. The resulting D-projections include what are now called Bregman projections, and the paper is the origin of the Bregman divergence , used today in mirror descent, entropy maximization and the theory of row-action methods (Censor and Zenios, 1997).
The paper proves convergence for two rules for choosing which set to project onto. This mission covers the second one, Theorem 2: always project onto the set that is farthest from the current point in the sense of (the "remotest-set" or maximal-distance control).
Let be a real linear topological space and a family of closed convex subsets of ; the index set is arbitrary and may be infinite. Let be convex with , and let satisfy:
A relaxation sequence starts at and sets ; the sequence of indices is the control. The control is remotest-set if at every step realizes
In the Lean development these objects are DConditions A S D P (conditions I–IV and VI), CondV S D ((⋂ j, A j) ∩ S) (condition V), IsRelaxSeq S P i x (in the series' shared namespace BregmanRelax.Cyclic) and IsRemotestControl D P i x (in BregmanRelax.Remotest).
For every remotest-set control and every relaxation sequence it generates, every limiting point is a common point:
Theorem 2 is the first convergence result for greedy (most-violated-constraint) selection in projection methods with a non-Euclidean distance. Unlike the cyclic Theorem 1 of the same paper, it applies to infinite families of sets, which covers semi-infinite systems of convex inequalities. Lemma 1, the generalized Pythagorean inequality, is the basic estimate for Bregman projections and recurs throughout mirror-descent and row-action analyses; Lemma 2 records the Fejér-type monotonicity of the iterates with respect to .
The results are classical and proved in the paper. To our knowledge they are not formalized in Lean or another proof assistant at this level of generality. The mission produces a machine-checked version of the abstract D-projection framework, with the conditions stated so that the Bregman divergence of §2 of the paper, and the Euclidean distance, are instances.
The obvious argument for Euclidean projections uses Fejér monotonicity and the fact that a bounded sequence in has convergent subsequences. Here neither the triangle inequality nor symmetry of is available, and need not be normed or finite-dimensional. The remotest-set rule controls only the D-distance from the iterate to each projection, in that argument order; turning "these distances tend to zero along a subsequence" into "the limit lies in every " requires the interplay of conditions V and VI, and it must hold uniformly over a possibly infinite index set.
Conventions committed to in Lean:
A trivializing formalization is ruled out: the hypotheses are jointly satisfiable with a genuine run (in with , , , and ), checked locally without sorry, so neither the goal nor the lemmas holds vacuously.
A complete development needs subsequence extraction from sequentially compact sets, one-sided limits of difference quotients, and monotone convergence of real sequences — all available in Mathlib. The D-projection framework, Lemma 1 and Lemma 2 are shared with the cyclic-control mission of the same paper and are reusable for any Bregman-projection algorithm. Proofs of the lemmas, of Theorem 2, and of the instance showing the Euclidean distance satisfies conditions I–VI are welcome.
Discounted dynamic programming with bounded cost per stage is the standard setting in which infinite-horizon sequential decision problems are well posed: the optimal cost exists, satisfies Bellman's equation, and can be computed by iterating the DP operator. Shapley proved this for stochastic games in 1953 (Shapley 1953), Blackwell for discounted Markov decision processes in 1965 (Blackwell 1965), and Denardo observed in 1967 that the arguments use only two properties of the DP operator: monotonicity and contraction in the supremum norm (Denardo 1967). Bertsekas (1975, 1977) and Bertsekas and Shreve (1978) turned this observation into an abstract dynamic programming framework, in which a single mapping encodes stochastic, deterministic, minimax and multiplicative-cost problems at once (Bertsekas 1977).
Chapter 4 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case, is the contraction part of that framework. Its results are the abstract form of what every course on Markov decision processes proves for the discounted case, and they are what later work on abstract DP (Bertsekas, Abstract Dynamic Programming, 2022) and on robust and regularized MDPs builds on.
A model consists of a state space , a control space , a nonempty constraint set for each , a mapping , where is the set of functions , and a function with . is monotone: implies .
A selector is a function with ; is the set of selectors, and a policy is a sequence in . The operators are
The cost of is , the optimal cost is , and is the cost of the stationary policy .
is the Banach space of bounded real functions on with . Assumption C asks for a closed set containing and invariant under and every ; that every limit defining exist and be real; and that for some integer and scalars , ,
Under Assumption C,
implies and implies for ; each is the unique fixed point of in ; and for every
The statement carries no constants beyond those of Assumption C.
Proposition 4.2 is the existence-and-uniqueness theorem for Bellman's equation in the contraction regime, together with the convergence of value iteration from an arbitrary start in . Propositions 4.3 to 4.5 turn it into statements about policies: when a stationary optimal policy exists, how one is found from the DP algorithm, and how much is lost when Bellman's equation is solved only approximately. Proposition 4.11 shows the assumption is met by a concrete class of problems, discounted minimax control, and so certifies that the abstract theorems are not vacuous.
The results are classical and have been proved in print since 1978; none of them is open. What this mission adds is a machine-checked version of the abstract theory itself, rather than of a single model. Mathlib has the Banach fixed point theorem for a contracting map of a complete space (ContractingWith) and a lemma for contracting iterates, but not the version on a closed subset with norm convergence of every orbit, and nothing on abstract DP. The platform has proved the finite-state discounted case for a concrete model (BertsekasDP.discounted_main_theorem); the abstract statements here cover infinite state spaces, minimax problems and -step contractions, and are reused by the later missions of this series (generalized models, Chapter 6) and by papers that cite the book.
The first idea is to apply the contraction mapping principle to and read off as its fixed point. That gives a fixed point of but says nothing about , which is defined as an infimum over all, generally nonstationary, policies of limits of compositions. The identification of the fixed point with is the content of the proposition, and it is where the Lipschitz condition (2) on all of , not only on , enters.
Two further features block a direct appeal to Mathlib. The contraction is only -step, so neither nor need be a contraction. And takes extended-real values, so every passage between and the Banach space must be justified by the invariance of .
The state and control spaces are arbitrary types. is S → EReal; is Mathlib's lp (fun _ : S => ℝ) ⊤, whose norm is the supremum norm, and toF embeds into . is an arbitrary closed subset of , not itself, and uniqueness of fixed points is asserted within . Policies are sequences ℕ → M; applies first. is the pointwise limit (limUnder), which exists and is real under Assumption C; is the infimum over all policies.
The book computes in with , whereas Mathlib's EReal has . No statement adds infinities of opposite sign. A norm bound between functions of is the predicate SupDistLe: both functions are real at every point and differ by at most , which is what the bound means under the book's arithmetic. Condition (2) is imposed on all of , as on p. 53. The scalars of Assumption C are explicit parameters, so the constant of Proposition 4.5 is the book's exact expression. The Fixed Point Theorem assumes nonempty, which the page leaves implicit and without which the statement is false.
Defining as the fixed point of , or replacing it by the infimum over stationary policies, would make the goal trivial. Neither is done here: is the infimum of the policy costs, exactly as in Eq. (8) of Chapter 2.
A complete development needs the -step fixed point theorem on closed subsets of a Banach space, which can be reused well beyond dynamic programming; the elementary calculus of SupDistLe and of the embedding of into S → EReal; and the monotone-operator inequalities of Section 2.1. Contributions of any of these, or alternative proofs of the milestones, are welcome.
A matching of a graph is a set of edges no two of which share a vertex. A matching with as many edges as possible is a basic object of combinatorial optimization. Assignment problems, pairing and scheduling problems, and the Chinese postman problem reduce to it, and it is the standard example of a problem with a polynomial-time algorithm that is not an instance of linear programming over a bipartite structure.
For bipartite graphs the problem was settled by the 1950s, through the theorems of König and Hall and the Hungarian method of Kuhn, whose correctness rests on linear programming duality. As Berge notes on p. 842, that duality "no longer subsists when the graph is not bipartite". C. Berge's three-page note of 1957 (doi:10.1073/pnas.43.9.842) gave the criterion that works for every graph: a matching is maximum exactly when it admits no augmenting chain.
Timeline.
Let be a finite graph without loops or multiple edges, with vertex set and edge set . A matching is a set of edges no two of which have a vertex in common. Its size is its number of edges. A matching is maximum if no matching of has more edges. This is a statement about cardinality: a matching to which no edge can be added (maximal under inclusion) need not be maximum.
Fix a matching . Its edges are strong, all other edges weak. A vertex is neutral if no strong edge contains it, and is the set of neutral points. An alternating chain is a walk in that does not use the same edge twice and in which, of any two consecutive edges, one is strong and the other weak. Vertices may repeat.
For the milestones, Berge adds a new vertex joined by strong edges to every neutral point, which gives a graph . Whenever an alternating chain of runs from to a vertex , its last edge carries an arrow from to . The non-neutral vertices then fall into four classes:
The mission's Lean development uses the same names: IsNeutral, IsAlternatingChain, IsMaximumMatching, barGraph, Arrow, IsInaccessible, IsWeakPt, IsStrongPt, IsMedium.
The statement fixes nothing beyond finiteness: the graph need not be connected, and no bound on its size is assumed.
Theorem 1 reduces the optimality of a matching, a statement about all matchings of the graph, to the absence of one kind of local structure. Its consequences include:
A matching that is not maximum can be certified by exhibiting the chain, and a maximum matching is certified by the labelling of Lemmas 1–4.
Theorem 1 has been proved since 1957 and appears in every textbook on matching theory. It is not formalized in Mathlib at the revision this mission uses. Mathlib has matchings as subgraphs, perfect matchings, alternating cycles and Tutte's theorem, but no augmenting-path characterization. This mission adds a formal statement of the theorem, together with the labelling of Berge's proof in a form that later missions on Edmonds' algorithm can reuse.
The "only if" direction is a local computation: the symmetric difference along an augmenting chain is again a matching, with one more edge. Even this needs care, because an alternating chain is only a trail and may a priori revisit vertices, while the augmentation needs a path.
The converse is the substance. In bipartite graphs, a search from the neutral points that alternates weak and strong edges labels each vertex at most one way, and its failure yields a cover of the same size as the matching. In general graphs an odd cycle lets a vertex be reached both through a strong and through a weak edge (the medium points). The bipartite labelling then fails, and no cover of size need exist: in a triangle the maximum matching has one edge and the minimum cover two. The proof has to treat these odd structures separately, and that is what Lemmas 1 and 4 do.
SimpleGraph V on a Fintype V. The paper's "unoriented graph (or 1-dimensional regular complex)" may have parallel edges, but a matching uses at most one edge of a parallel class, so nothing is lost. The matching is a subgraph M with M.IsMatching, and its size is M.edgeSet.ncard. Maximum means cardinality-maximum over all matching subgraphs. Internally stable sets and covers are Mathlib's IsIndepSet and IsVertexCover.Option V, with = none. An arrow needs an alternating chain of positive length from .IsMedium in Lean, because M names the matching.Any proof of the goal is welcome, whether it follows Berge's induction, uses the symmetric difference of two matchings, or goes through the Tutte–Berge formula. Reusable infrastructure is especially welcome: augmentation along a path, the symmetric difference of two matchings as a union of paths and cycles, and trails that alternate with respect to a matching.
Nash's theorem guarantees that every finite game has a mixed equilibrium, but says nothing about how hard one is to find. Daskalakis, Goldberg and Papadimitriou (SIAM J. Comput. 39(1), 2009) showed that computing a Nash equilibrium is complete for the class PPAD of total search problems whose solutions are guaranteed by a parity argument on a directed graph (Papadimitriou 1994). Their proof simulates an arithmetic circuit by a graphical game: a multiplayer game in which each player's payoff depends on a few neighbours only, built from small game gadgets whose equilibria compute , , , constants and comparisons on mixed-strategy probabilities.
These gadgets are the reusable core of the reduction. The PPAD-completeness results for three-player games, and the later results for two-player games and for approximate equilibria, all rest on gadget analyses of this kind.
Timeline.
A game has finitely many players; player has a finite set of pure strategies and a nonnegative payoff for each pure profile . A mixed profile gives each player a probability distribution , and denotes the product of the probabilities of the components of a partial profile . The expected payoff of a pure strategy of is .
An -Nash equilibrium (the paper's notion, an -approximately well-supported equilibrium, Eq. (2)) is a mixed profile in which no player puts weight on a pure strategy that another of its pure strategies beats by more than :
For this characterizes Nash equilibria.
A player with strategies is binary; is the probability that it plays , and is the probability that plays . The affects graph (Definition 2.2) has an edge between distinct players when the payoff of is a nonconstant function of the action of . A legal -coloring (Definition 4.8) gives each player one of colors so that the two ends of an edge differ and two distinct players with a common successor differ.
The game (Fig. 11) has inputs , output and intermediate players , all binary except , which has strategies . Its payoff tables are fixed by nonnegative integers ; the inputs' payoffs are unconstrained.
For nonnegative integers with , the affects graph of has a legal 3-coloring, and for every , at every -Nash equilibrium,
The case is exact computation at every Nash equilibrium.
The result. The paper reduces -player games to three-player games by building a graphical game from gadgets, legally coloring it with three colors, and turning each color class into one player of a normal-form game (§4.2, §4.5). Proposition 4.18 supplies a gadget that computes and can be glued into such a construction while keeping it legally 3-colorable (p. 233), at the price of an error constant instead of the constant of the elementary gadgets. The error bound is what carries the reduction over to approximate equilibria: an -Nash equilibrium of the gadget computes its function to within .
Formalizing it. All results here are proved in the paper (Proposition 4.5 is stated with the remark that its proof is similar to those of Propositions 4.2 and 4.3). None of them has a machine-checked proof, and no graphical-game or gadget infrastructure exists in Lean. The mission formalizes the known proofs and produces a library of verified gadgets with explicit error bounds, the first layer of any formal treatment of the PPAD-hardness of Nash equilibria.
Each claim is a case analysis on which strategy of an intermediate player is dominated by more than , but the cases interact. Claim 3 needs Claims 1 and 2 as inputs, and it is the step where both and are used: without them one of the regimes of cannot be excluded. The three-strategy player cannot be handled by the "binary player copies or disagrees" argument of the elementary gadgets; its weight on and on must be tracked separately. The error constants and propagate through products of approximate quantities, so a proof that is loose at any step does not reach them.
On the Lean side, the expected payoff of a pure strategy is a sum over all pure profiles of a ten-player game; every claim first has to reduce it to the few coordinates the player's payoff actually depends on.
Games, mixed profiles and expected payoffs are those of the published agt_games bundle: a finite player type, strategy types S i, payoffs u : ι → (∀ i, S i) → ℝ, AGT.IsMixedProfile, AGT.expectedPayoff. The expected payoff of a pure strategy is the expected payoff of the profile with 's strategy replaced by the point mass at . An -Nash equilibrium requires a genuine mixed profile.
Each gadget is one explicit game on its own player type, with the payoff tables of the paper. Binary strategies are Fin 2 with the paper's labels , and is the weight on 1; 's strategies are an inductive type {zero, one, star}. The input players' payoffs are unconstrained in the paper; here they are , which makes the -condition at the inputs vacuous. Since every non-input payoff depends only on gadget players, "-Nash equilibrium of the standalone gadget" quantifies over all mixed strategies of the inputs and imposes the condition exactly on the other players, which is the paper's meaning when the gadget sits inside a larger game. The affects graph is computed from the payoff functions, without self-loops, and colors are Fin k. The ranges (Proposition 4.18) and (Propositions 4.2, 4.3, 4.5) follow the paper; is added where the paper writes only .
The paper states Proposition 4.18 and Lemma 5.3 as "there is a graphical game"; an existential statement would be met by a game whose output has a dominant strategy and whose inputs are forced, so both are stated for the explicit game of the proof, with free inputs.
A complete development needs a computation lemma for the pure-strategy payoff in each gadget (reusable for any gadget on these definitions) and the case analyses of the claims. Proofs of the elementary gadgets, which are short, and of Claims 1 and 2 are good first contributions; Claim 3 is the main step.
A single machine must process a set of jobs, each with a processing time and a due date, and the cost of a schedule depends on how late the jobs finish. Total tardiness is the classical criterion, but in many applications lateness is penalised more than proportionally: a job one week late costs more than twice a job half a week late, and a quadratic or other convex penalty describes this better. Hamilton Emmons's 1969 paper in Operations Research (DOI 10.1287/opre.17.4.701) derives dominance rules for total tardiness and then asks which of them survive when total tardiness is replaced by for an arbitrary convex nondecreasing loss .
Timeline of the relevant results:
A finite set of jobs is to be sequenced on one machine. Job has a processing time and a due date . All jobs are available at time , and the machine processes them one after another without idle time. A schedule is an ordering of the jobs of . The completion time of in is the sum of the processing times of and of every job before it; its waiting (starting) time is , and its tardiness is
A loss function , convex and nondecreasing on , is fixed, the same for every job. The objective is , and a schedule is optimal if no schedule of has a smaller objective. With this is total tardiness.
Where the paper uses job indices, the jobs are indexed in SPT order: implies , or and . The notation means that some optimal schedule has before ; for a set of jobs, means that some optimal schedule has before every job of , and is the set of jobs of not in . An EDD schedule sequences the jobs in nondecreasing order of due dates.
If an EDD schedule of satisfies
then minimises over all schedules of , for every convex and nondecreasing on .
The goal fixes no constant and no particular : it is a statement about the whole class of convex nondecreasing penalties.
Two further statements of the same section are included as items: Corollary 1.3* (the SPT schedule is optimal if it coincides with the EDD schedule) and Theorem 3 for the generalised objective.
The goal says that EDD is optimal for every convex nondecreasing tardiness penalty as long as no job starts after its due date. The classical sufficient condition, that at most one job is tardy, follows from Jackson's rule; Emmons's condition allows any or all jobs to be tardy, provided each is tardy by at most its own processing time. Because the conclusion holds for the whole class of penalties at once, an instance satisfying it needs no knowledge of : total tardiness, total squared tardiness, and any other convex nondecreasing cost are minimised by the same sequence. Theorems 1* and 2* are the dominance rules that the paper's ordering procedure applies pairwise; they reduce the search space of branch-and-bound methods for convex tardiness objectives.
The results are proved in the paper (for the proofs are said to be "easily established" and omitted). None of them has, to our knowledge, a machine-checked proof. The mission produces formal statements and proofs of the generalised results, including the omitted ones, on top of a reusable single-machine model.
The total-tardiness proofs compare changes in tardiness additively: an interchange is good if the decrease in one job's tardiness is at least the increase in another's. For a convex this comparison is not enough, because a unit of tardiness costs more at higher tardiness levels; the changes must also occur at the right height on the curve, and part (b) of the proof of Theorem 1 fails for this reason. Each generalised argument therefore has to check, for every job whose tardiness changes, both the size and the location of the change, including jobs whose tardiness changes from zero to positive. Ties for the latest due date are a further obstacle: the printed proof of Corollary 2.1 cites Theorem 2, whose hypothesis is strict, so a job sharing the maximum due date is not covered by the argument as written, although the corollary is stated without excluding ties.
Jobs are elements of a type ; the job set is a Finset , processing times and due dates are real functions . Where the paper's index matters, is linearly ordered and its order is the job index, together with the SPT-indexing hypothesis. A schedule is a duplicate-free list whose elements are exactly , and completion times are the published single-machine definition MooreLateJobs.Shared.completionTime (Moore 1968), which starts the machine at time with no idle time. Optimality is against every schedule of . The relation is formalised as the existence of an optimal schedule with before (keeping the premise in the conclusion where the theorem has one); the paper's cumulative reading of the notation is not formalised.
Standing assumptions and deviations:
A trivializing formalization is ruled out: the goal requires optimality of the given EDD list against every schedule of , not of some EDD list, and a sorry-free check shows its hypotheses hold on a two-job instance in which both jobs are tardy.
A complete development needs list lemmas for moving one job to a later position, the effect of such moves on completion times, and slope inequalities for convex functions on . The schedule-manipulation lemmas are reusable for other single-machine sequencing results. Proofs of any milestone, of the two further items, and of general interchange lemmas are welcome.
The complexity of computing a Nash equilibrium is usually studied for an approximate equilibrium, because an exact equilibrium of a game with three or more players can require irrational probabilities. Two approximation notions are in use, and results proved for one do not automatically transfer to the other. Daskalakis, Goldberg and Papadimitriou (SIAM J. Comput. 39(1), 2009) prove their PPAD-hardness results for the stronger notion, the ε-approximately well-supported Nash equilibrium, and then show in their §4.7 (Lemma 4.28, announced as Lemma 2.1) that any ε-approximate Nash equilibrium can be turned, by an explicit and cheap transformation, into an approximately well-supported one with a polynomially worse accuracy. This is what lets their hardness results hold for both notions. A weaker version of the relation had been pointed out by Chen, Deng and Teng (FOCS 2006, reference [9] of the paper).
This mission formalizes Lemma 4.28 together with the steps of its proof: the best-response inequality (28), Claims 5 and 6, and the Lipschitz estimate of Lemma 4.26 (used in the proof as Lemma 4.29).
A game in normal form has players. Player has a finite set of pure strategies; is the set of pure strategy profiles and the set of profiles of the players other than . For each player and profile there is a payoff ; for and the payoff to at the profile is written . The number is the largest entry over all players and all profiles.
A mixed profile assigns to each player a probability distribution on ; the players randomize independently, and for we write . The expected payoff of player for playing the pure strategy against the others is
The trimmed profile of with parameter deletes the strategies whose expected payoff is more than below and renormalizes:
In the Lean development these are purePayoff u x p j, maxPurePayoff u x p, maxPayoff u, IsEpsApproxNash u x ε, IsEpsWellSupportedNash u x ε, trimMass u x ε k p and trim u x ε k, all in the namespace DGPNash.WellSupported.
For and an -approximate Nash equilibrium , the trimmed profile with is a mixed profile and a
The constant is the paper's. The statement is about the specific profile built from , not about the existence of some well-supported equilibrium.
The result. Lemma 4.28 makes the two approximation notions polynomially equivalent for computation: every well-supported equilibrium is approximate with the same , and conversely an approximate equilibrium yields a well-supported one at accuracy for fixed and payoff range. Hardness results proved for well-supported equilibria, including the PPAD-completeness of 3-player Nash in the paper and the two-player result of Chen, Deng and Teng, therefore apply to approximate equilibria as well, and algorithms for one notion give algorithms for the other. Lemma 4.26, the Lipschitz dependence of expected payoffs on the opponents' strategies in , is a general tool for perturbation and rounding arguments in finite games.
Formalizing it. The result is proved in the paper; as far as we know there is no machine-checked version, and the platform has neither approximation notion. The mission produces both definitions, on top of the published game vocabulary agt_games, and the quantitative chain from an approximate equilibrium to a well-supported one. These definitions are what any later formalization of approximate-equilibrium algorithms or hardness results would need.
The obvious attempt, to show that itself is approximately well-supported, fails: an approximate equilibrium may put small positive probability on a strategy that is far from optimal, which a well-supported equilibrium forbids for any accuracy. Removing those strategies changes the opponents' expected payoffs, so the well-supported condition must be checked for , computed from , not for . The accuracy of the result therefore depends on how far all opponents' strategies move, which is why the bound carries the factor . Lemma 4.26 is a statement about product distributions: the change in a multilinear expected payoff is controlled by the sum of the per-player distances, not by their product.
ι with decidable equality; player p has a finite strategy type S p; payoffs are u : ι → (∀ i, S i) → ℝ with the standing hypothesis ∀ p s, 0 ≤ u p s of §2.1. The number of players is Fintype.card ι, and 2 ≤ Fintype.card ι is assumed in every statement, as in §2.1. Strategy sets may differ between players.AGT.IsMixedProfile and AGT.IsLottery from agt_games; both equilibrium notions include the requirement that the profile be mixed. is AGT.expectedPayoff after player alone switches to the pure strategy , and the approximate-Nash condition compares AGT.expectedPayoff before and after player alone switches to a lottery , which is the paper's inequality (27).AGT.nash_existence) a δ-well-supported equilibrium exists for every δ ≥ 0, so the goal is stated for , defined from , and not as an existence claim.Contributions welcome: proofs of the milestones, in particular the decomposition of the expected payoff, which Eq. (28) and the goal both need, and Lemma 4.26, which is reusable in any perturbation argument for finite games.
Many regression problems have far more unknown coefficients than observations : gene expression studies with tens of samples and thousands of genes, imaging from few measurements, nonparametric curve recovery from a finite number of noisy samples. Estimation is hopeless in general, but becomes possible when the parameter is sparse, that is, has few nonzero entries. Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) proposed the Dantzig selector, an estimator computed by a single linear program, and showed that its squared error is within a logarithmic factor of what an oracle that knew which coefficients matter could achieve.
The estimator became one of the two standard methods for high-dimensional regression, alongside the Lasso; the comparison of the two by Bickel, Ritov and Tsybakov (arXiv:0801.1095, 2009) is built on it. This mission targets the paper's main result, the oracle inequality (Theorem 1.2). A companion mission covers the simpler bound for sparse parameters (Theorem 1.1).
Observations follow the linear model
where is a deterministic design matrix with columns , each of Euclidean norm ; is an unknown deterministic parameter; and has independent coordinates, . The vector is -sparse if at most of its entries are nonzero.
Two constants of measure how close sparse sets of columns are to being orthonormal. The restricted isometry constant is the smallest such that for every supported on at most indices. The restricted orthogonality constant (defined for ) is the smallest with whenever are supported on disjoint sets of sizes at most and . Below and .
For a tuning level , a Dantzig selector is any solution of
The ideal mean squared error is : the risk of an oracle that keeps exactly the coordinates above the noise level.
Let , , and . If is -sparse and , then with probability exceeding every Dantzig selector obeys
with the explicit constant (1.14)
The result. Theorem 1.2 says that a single linear program, which knows neither the support of nor which coefficients exceed the noise, matches the oracle risk up to a factor , uniformly over -sparse parameters and with explicit, nonasymptotic constants. For coefficients well below the noise level it is far sharper than the bound of Theorem 1.1. It is the template for later oracle inequalities for -penalized estimators under restricted isometry or restricted eigenvalue conditions.
Formalizing it. The theorem is proved in the paper, but parts of the argument are only sketched: Corollary A.2 refers to the 2005 Decoding by Linear Programming paper for its convergence argument, and Corollary A.3's bound is printed with a constant its own proof does not deliver. A machine-checked proof settles these steps. The restricted isometry and orthogonality constants used here are already published on the platform from the decoding series; the appendix lemmas on dual vectors are reusable for any compressed-sensing result in that framework. No formalization of the Dantzig selector's oracle inequality is known to us.
The natural proof compares with the hard-thresholded parameter that keeps only the large coefficients: if were feasible for the Dantzig constraint, the analysis of Theorem 1.1 would apply directly. It is not feasible in general, because the small coefficients , though individually below the noise level, can add up to a large correlation . The central difficulty is to split into a part with controlled and norm and a part invisible to the constraint; this requires constructing dual vectors with prescribed correlations (Lemma A.1, Corollary A.2), via an iterative, geometrically convergent correction. The probabilistic part is a Gaussian tail estimate plus a union bound, and the bookkeeping of constants must be carried through exactly.
Vectors are functions Fin p → ℝ, the design is Matrix (Fin n) (Fin p) ℝ, and the noise is a family z : Fin n → Ω → ℝ of mutually independent random variables (iIndepFun) each with law gaussianReal 0 σ². and are the published CandesTao.Decoding.restrictedIsometryConst X (2*S) and restrictedOrthogonalityConst X S (2*S) (infima, absolute value in the orthogonality condition). Domain: and (the paper defines for ), which forces and . A Dantzig selector is any minimizer over the feasible set; the constraint is a bound on every coordinate.
The goal bounds from above the (outer) probability of the bad event "no Dantzig selector exists, or some Dantzig selector violates (1.13)". Because the event includes non-existence, a definition no vector satisfies cannot make the theorem vacuous; and the constant is the printed (1.14), evaluated at , of , not a free constant chosen after the fact.
Corrected constant: Corollary A.3 is stated with , the bound its proof gives once Corollary A.2 is applied at an integer sparsity level; the printed statement omits the factor . Corollary A.2 carries Lemma A.1's standing hypothesis . The deterministic lemmas (3.1, 3.2, A.1–A.3) assume nothing about column norms, since their statements do not need it.
Useful infrastructure: monotonicity of and in their indices (the proof applies the lemmas at a smaller sparsity level), the Gaussian tail bound , existence of minimizers of the Dantzig linear program, and a sorting/blocking toolkit for "the largest positions". Proofs of individual milestones are welcome independently.
The gradient method minimizes a differentiable function on by moving from the current point along the negative gradient, . Every practical implementation has to choose the step . A fixed step requires knowing a Lipschitz constant of ; an exact line search is expensive. Larry Armijo's four-page note (Pacific J. Math. 16 (1966) 1–3) proved that any step achieving a sufficient decrease proportional to yields convergence, and gave the halving rule that is now called the Armijo rule or backtracking line search. The rule is the default step-size strategy of gradient, quasi-Newton and Newton-type methods in textbooks such as Nocedal–Wright and Bertsekas, and its sufficient-decrease test reappears in essentially every later line-search analysis.
Timeline:
Let be real Euclidean -space with norm , and let be continuous and bounded below. For a fixed the level set is . Write for the gradient of at . " on " means that is differentiable at every point of and is continuous there.
with when the set is empty. Condition IV forces to be the unique minimizer and the only stationary point in .
For and , the sufficient-decrease set of display (1) is
The steepest descent algorithm uses . The modified steepest descent algorithm fixes , sets , and takes with the smallest positive integer such that
Assume is continuous and bounded below and Conditions III and IV hold at . If , then for every
and every sequence with first term and for all satisfies
The theorem separates the analysis of a gradient method from the choice of its step: whatever rule produces steps in converges, and the two corollaries show that both a fixed step and a halving search started from an arbitrary qualify. The halving rule needs no knowledge of , which is why it became the standard globalization device for descent methods. The hypotheses are local to the level set: need only be Lipschitz on , not on all of , so functions whose gradient is only locally Lipschitz, such as polynomials of degree above two with bounded level sets, satisfy Condition III.
The result is classical and proved on the page; it has not, to our knowledge, been machine-checked in this form. Formalizing it provides a verified sufficient-decrease convergence theorem with level-set-local hypotheses, a verified Armijo backtracking rule with explicit constants , and , and reusable definitions (sufficient-decrease set, Armijo test with halving steps) on which later line-search results can build.
The mean value step in the proof of the descent inequality silently uses the Lipschitz bound along the whole segment from to , but Condition III gives it only on . One has to show that the segment cannot leave the closed set for ; replacing the hypothesis by a global Lipschitz condition is not acceptable, because it changes the theorem. The final step needs Condition IV in its exact form: gradients tending to zero along the iterates do not by themselves give convergence of the iterates, and the positive lower bound away from is what turns stationarity into convergence. Corollary 2 additionally requires a termination argument for the halving search and a uniform lower bound on accepted steps.
is EuclideanSpace ℝ (Fin n), is the norm and is Mathlib's gradient f. All declarations live in the namespace ArmijoGrad.Conv, with one definition file ArmijoGrad.Conv.Setting.
Committed conventions:
Continuous f, BddBelow (Set.range f), ConditionIII f x0 K, ConditionIV f x0 xstar. Milestones keep only the assumptions their claim uses, which makes them more general; nothing is added.gradient f on . The Lipschitz bound of Condition III holds on only; is part of Condition III.ℕ → EuclideanSpace ℝ (Fin n) with first term equal to , the base point of , as in the paper's notation.A trivializing formalization is ruled out: the goal assumes nothing about , the descent inequality or , Condition IV cannot hold vacuously because it names a minimizer, and all hypotheses are satisfiable by nontrivial data: satisfies Conditions III and IV with and , and both algorithms have runs for it.
A complete development needs the one-dimensional mean value inequality along a segment, a continuity argument keeping the segment in , the telescoping bound for monotone sequences bounded below, and the halving-search termination. The definitions file and the descent and Armijo-index lemmas are reusable for later line-search missions. Contributions are welcome on every milestone; the descent inequality is the natural first target.
A Markov decision problem models a system that is observed once per period and controlled by choosing an action: the action earns an immediate income and determines the probabilities of the next state. Inventory control, machine replacement, queue admission and many reinforcement-learning benchmarks are of this form. With future income discounted by a factor , Howard (Dynamic Programming and Markov Processes, 1960) showed how to compute an optimal policy by policy improvement. The undiscounted problem () is harder, because total income is typically infinite.
David Blackwell's Discrete Dynamic Programming (Ann. Math. Statist. 33 (1962) 719–726) treats as a limit of . Its Theorem 5 shows that some stationary policy is optimal simultaneously for all discount factors sufficiently close to . Such policies are now called Blackwell optimal, and the result is the base of sensitive discount optimality (Veinott, 1969) and of the standard textbook treatment of average-reward problems (Puterman, Markov Decision Processes, 1994, Ch. 10).
Timeline. Howard (1960): policy iteration for discounted and average-reward finite problems. Blackwell (1962): Theorem 5 (Blackwell optimal stationary policies exist) and the characterization of nearly optimal stationary policies (Theorem 4, the subject of the companion mission). Miller and Veinott (Ann. Math. Statist. 40 (1969) 366–370), Veinott (Ann. Math. Statist. 40 (1969) 1635–1660): Laurent expansions of in and -discount optimality.
There are finitely many states and a finite set of actions, every action available in every state. In state , action yields income (any sign) and moves the system to state with probability ; each is a probability vector.
A decision rule is a function from states to actions; is the finite set of decision rules. A policy is a sequence in : on day , in state , action is used. Policies are deterministic and Markov but may change with time. The policy uses on day and then follows ; uses every day and is called stationary.
For , is the vector and the Markov matrix . With and , the return of at discount factor is
a vector indexed by the initial state. Vectors are compared coordinatewise; means and .
A policy is -optimal if for every policy . Following §4 of the paper, a policy is optimal if it is -optimal for all sufficiently near .
There exist a decision rule and such that
One and one serve every competing policy and every .
The result. Theorem 5 shows that the infinitely many discounted problems near share a common optimal stationary policy. Such a policy is also optimal for the long-run average criterion, which settles the existence of average-optimal stationary policies in finite models without any recurrence assumption. It also justifies computing undiscounted solutions as limits of discounted ones, and it is the first case of the sensitive optimality criteria developed later.
Formalizing it. The theorem is classical and proved in the paper and in the textbooks; there is no machine-checked proof of it in Blackwell's model on the platform. A related open item, SennottDP.AvgFinite.prop_6_2_3_blackwell_optimal, states the textbook version for nonnegative costs and randomized history-dependent policies; the present mission is Blackwell's own formulation with incomes of either sign and deterministic Markov policies. A complete development also yields a verified policy improvement theorem (Theorem 3) and the rationality of discounted values in , both reusable for any finite-state discounted model.
The Corollary gives, for each , some optimal stationary policy, and is finite, so one is -optimal for infinitely many accumulating at . The obvious argument stops there: optimality on a sequence of 's says nothing about the 's in between, and a pointwise limit argument cannot produce a whole interval . The step that fails is passing from "frequently" to "eventually", and it needs structural information about how depends on , not just continuity. A second difficulty is the comparison class: optimality must hold against all time-dependent policies, not only the finitely many stationary ones, so the final step has to bring the Corollary back in for every near .
States and actions are finite nonempty Lean types St, Act; decision rules are functions St → Act and policies are sequences ℕ → St → Act, indexed from (π 0 is Blackwell's ). Incomes are real-valued with no sign restriction. The law of motion law s a s' satisfies the published predicate IsTransitionKernel. is the ordered matrix product and is the tsum of the series, which converges absolutely for ; every statement at a fixed assumes , and nothing is stated for . Vector inequalities are coordinatewise, and the strict order is " and ", not coordinatewise strict. " sufficiently near " is "there is such that for every ". The paper's §4 phrase is encoded as -optimality, so no supremum over policies appears.
The word "optimal" has two meanings in the paper: at one fixed (§3, the Corollary) and for all near (§4, Theorem 5). The Lean development keeps them apart as IsBetaOptimal β and IsOptimal. A statement of Theorem 5 at a single , with "there exists ", for a set of 's accumulating at , or against stationary policies only would be a different and weaker theorem; the goal rules all of these out.
Needed infrastructure: summation and shifting of the discounted series, Neumann series for stochastic , Cramer's rule to express as a ratio of polynomials in , and the fact that a nonzero polynomial has finitely many roots. The policy improvement theorem and the rationality lemma are reusable beyond this mission. Proofs of individual milestones are welcome independently.
Selfish routing and resource sharing are modelled by congestion games: each player picks a set of shared resources, and the cost of a resource grows with the number of players using it. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures how much worse the social cost of a worst Nash equilibrium is than the optimum. For non-atomic (infinitesimal) traffic with linear latencies, Roughgarden and Tardos (J. ACM 2002) showed the ratio is . Christodoulou and Koutsoupias (STOC 2005) turned to finite (atomic, unweighted) congestion games, where each of players controls one indivisible unit of load, and determined the pure price of anarchy for linear latencies in four settings: asymmetric or symmetric strategy sets, and average or maximum social cost. Awerbuch, Azar and Epstein (STOC 2005) obtained the value for the asymmetric average case independently.
This mission covers the symmetric average-cost entry of that table (Sect. 3.2 of the paper). It shows that when all players share one strategy set, the ratio is not but , which depends on the number of players and tends to only as .
A congestion game has a finite set of players (in Lean, Fin N), a finite set of facilities , for each player a collection of pure strategies , and for each facility a latency . A profile picks for each player (IsProfile). The load is the number of players whose strategy contains (load), the cost of player is
(cost), and the social cost is (sumCost), times the average cost. A profile is a pure Nash equilibrium (IsPureNash) if for every player and every , where replaces by .
Latencies are linear (IsLinear) when with . The game is symmetric (IsSymmetric) when all players have the same strategy set, . The pure price of anarchy of a class of games is the supremum, over games in the class and pure Nash equilibria , of , with .
For every : every pure Nash equilibrium of every symmetric linear congestion game with players satisfies
and some symmetric linear game with players has a pure Nash equilibrium and a profile with and equality. Together these state that the pure price of anarchy of the class is exactly .
The result separates symmetric from asymmetric games for every finite number of players: for the symmetric bound is , for it is , against for asymmetric games with players. Theorem 4 shows the bound is tight, so the function is the exact answer, not an artefact of the proof. The asymptotic value coincides with the asymmetric one, which says that symmetry helps only by a vanishing amount for large populations. Later work on smoothness arguments (Roughgarden, STOC 2009) takes the bound of this paper as its central example.
The theorems are proved in the paper; the authors print the proofs for identity latencies and state that they extend to . No machine-checked proof of these bounds is known to exist. This mission produces a statement for general affine latencies with nonnegative coefficients, the affine forms of the intermediate inequalities, and an explicit family of instances for every , all of which are reusable for the other entries of the paper's table.
The upper bound requires combining the deviation inequalities (player against the strategy of each player in the comparison profile) and then bounding cross terms facility by facility; the step that needs care is that the bound of Lemma 1 holds for integer loads only and fails for real numbers, so any argument that relaxes loads to reals loses the constant. The asymmetric argument, which compares player only with its own optimal strategy , gives and cannot see the dependence on .
For the lower bound, the instance must be a Nash equilibrium against every strategy in the common strategy set, which contains the equilibrium strategies of all other players as well as the optimal ones. Exact equality of the ratio requires the block sizes to be tuned to ; verifying the equilibrium condition involves counting facilities shared by pairs and triples of players.
Players are Fin N with ; facilities are an arbitrary finite type with decidable equality; strategies and profiles are Finsets of facilities, with feasibility a separate predicate. Latencies are real-valued functions of the natural-number load. Linear latencies are affine with nonnegative coefficients, as in Sect. 2 of the paper; the milestone inequalities carry the coefficients explicitly and reduce to the printed displays when , . The Nash condition is in cost form. Upper bounds are stated against every feasible profile , which is equivalent to the bound on without dividing by . All constants are computed in .
The lower bound requires : without it the statement is satisfied by zero latencies or empty strategies, where both sides vanish. Symmetry is a hypothesis of the upper bound and a property of the instance; without it the upper bound is false, since asymmetric instances reach .
A complete development needs finite-sum manipulations (double counting ), the integer inequality of Lemma 1, and an explicit facility type for the instance. The model layer is shared with the other missions of this series. Proofs of the milestones and alternative proofs of the bound are welcome.
Shadow tomography asks for predictions of many specified measurements of an unknown quantum state, while using as few prepared copies of that state as possible. The requested output is a list of acceptance probabilities, not a full description of the state. A procedure might exploit the fact that these are only numbers, even when the state has dimension . The natural question is how far this saving can go. Aaronson's paper gives upper bounds and separates two sources of difficulty: one already present for ordinary probability distributions, and one arising from noncommuting quantum measurements.
This mission concerns the first source. It formalizes Theorem 16, which says that even when the state and every requested measurement are diagonal in the same basis, the number of copies must grow with in the relevant asymptotic regime. In that special case, the unknown state is an ordinary distribution on outcomes. The theorem therefore puts a limit on any proposed improvement to shadow tomography that would promise fewer copies in all instances.
A mixed state on a -dimensional system is a positive semidefinite complex matrix with trace one. A two-outcome measurement is represented by an effect satisfying ; it accepts with probability . When is diagonal, its diagonal entries are the probabilities of the basis outcomes. When is diagonal too, it specifies a randomized yes-or-no test on those outcomes. These conventions are stated in Section 3 of the paper.
Given effects , a shadow-tomography strategy measures independent copies and outputs estimates . It succeeds on when every estimate differs from by at most . The lower bound requires success probability at least for every diagonal mixed state. The strategy may make a joint quantum measurement on all copies and may choose its estimates from its observed outcome. This is the same measurement model used in Problem 1.
The goal is the classical clause of Theorem 16. There are absolute constants and such that, for , , and , there are diagonal effects with 0/1 entries, corresponding to the known Boolean functions in Section 6.1, for which every strategy successful on all diagonal states must use
The hard measurements are chosen before the strategy is quantified. The statement therefore also rules out a strategy with a smaller copy count that works uniformly for all quantum states and measurements. Its constants and threshold express the notation in Theorem 16, rather than specifying a numerical optimum.
Four milestones come from the proof on pages 20–21: the high-probability overlap bound for independently chosen half-size subsets (Eq. (1)); the acceptance probability of a subset under its associated biased distribution; an upper bound on the mutual information between the hidden subset index and the observed samples; and the exact entropy formula with a quadratic entropy deficit. These statements expose the combinatorial and information-theoretic parts of the lower bound while leaving the goal as the paper's copy-complexity result.
Theorem 16 sets a floor for shadow tomography that survives even when all operators commute. Any uniform copy bound for the full quantum task must respect this floor. The result also distinguishes the difficulty of predicting many properties of a distribution from the extra difficulty possible for noncommuting states and measurements, which the paper treats in a separate lower bound. Section 6 presents both bounds.
A complete formalization would give machine-checked statements and proofs for the finite subset construction, the entropy calculation, the information inequality, and the reduction from a successful quantum measurement procedure on diagonal states to a lower bound on . The theorem is proved on paper; these draft statements are open Lean goals and do not claim that its proof has been machine checked. The finite-distribution and information-theory infrastructure is reusable for other lower bounds based on hidden-index families.
Counting how many possible measurements there are does not by itself show that samples reveal enough about which distribution generated them. The lower bound needs a quantitative relation between estimation accuracy and information about a hidden index, while each individual sample carries limited information. The paper's printed overlap condition (1) is too weak for the next displayed estimate: at its boundary it gives . The milestone preserves Eq. (1) as printed; closing the goal requires the correspondingly sharper overlap fact with , which follows from the same type of concentration statement after adjusting its constant. The printed assertion that learning the index requires mutual information at least is also imprecise at success probability ; a quantitative decoding inequality is needed. Neither incorrect display is a draft milestone.
Matrices are indexed by Fin D. WildeQIT.IsDensityOperator supplies the mixed-state predicate and . Diagonal states and effects use the standard matrix diagonal predicate. An effect is positive semidefinite together with its complement. The tensor power uses functions Fin k → Fin D as basis indices; at it is a one-by-one identity matrix. A strategy is a finite-outcome POVM on that tensor power, followed by a real estimate vector for each outcome. The output values are not restricted to : clipping them to this interval cannot worsen an estimate of a probability. No restriction to classical estimators is placed in the goal; that would change the allowed strategies before the theorem has been proved.
The asymptotic threshold excludes the one-dimensional and single-measurement corners where the claimed rate does not describe the problem. The bound keeps the biased distributions used on page 20 nonnegative; would permit a zero-copy constant estimate. Subset milestones require even or explicitly require a half-size subset, so has its intended meaning. The natural logarithm appears nowhere in the lower-bound rate; entropy, mutual information, and use base two. At zero probability the entropy convention is .
The finite distributions, entropy, conditional entropy, and mutual information reuse the published WildeQIT definitions. Contributions that prove the four source milestones, establish the sharper overlap fact, or supply the quantitative decoding step are welcome. The goal must retain its order of quantifiers: one hard measurement family, then every strategy, with success demanded on every diagonal state.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the cutoff-90 mission already covers every , the new work is the range from 89 to 90.
The argument for was reached by tightening its estimates step by step, starting from 256. With its current choices those estimates stop working below 90, and nobody has yet found a way past that point. It is not known whether 90 is a real limit of the method or only of the choices made so far, so this mission is the smallest test of whether the cutoff can move at all. The accepted proof for and its research note are the natural starting point. The goal theorem below gives the exact statement.
This is an open entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 89 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryThe irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Salikhov's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (7.606309 : ℝ), i.e. .
Value. The bound is quoted as (e.g. by Zeilberger–Zudilin), a truncation. This entry rounds the last digit up to .
Salikhov uses integrals of rational functions that are symmetric under a group of transformations (in the spirit of Rhin–Viola), which gives larger arithmetic savings in the common denominators than Hata's construction.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Hata's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (8.016046 : ℝ), i.e. .
Value. The paper computes the exponent as and states the rounded bound . This entry rounds the computed value's last digit up to , which is still below the paper's and above .
Hata obtains simultaneous approximations to from complex contour integrals of Legendre type, with extra arithmetic savings from primes that divide the coefficients to a predictable extent. His linear-form measure is , giving (stated in the paper as ). It stood as the record for about fifteen years.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
A forecaster announces, each day, a probability that it will rain; afterwards nature reveals whether it did. The forecaster is calibrated if, on the days on which it announced roughly 30%, it rained roughly 30% of the time, and likewise for every other announced value. Calibration is a minimal consistency requirement for probabilistic forecasts, used in meteorology, in the evaluation of probabilistic classifiers, and in game theory, where calibrated forecasts of the opponents' play lead to correlated equilibrium (Foster and Vohra, 1997).
Calibration is achievable even against an adversary who chooses the outcomes, provided the forecaster randomizes. Timeline:
This mission formalizes the last result, Theorem 22 of the 2011 paper, in the explicit form given by its proof.
Fix a positive integer and the grid width . Each round the forecaster chooses a probability vector in the simplex over the grid indices , draws and announces . Nature then reveals .
Vectors live in with the Euclidean norm . The ℓ₁ norm is , the ℓ₁ ball is , and the unit cube is .
The calibration game (11) has payoff
The -calibration rate (Definition 19) of the announced forecasts is . Replacing each indicator by its expectation gives the rate of the forecast distributions,
which is for the average payoff .
The forecaster is Algorithm 5. It keeps a point in the cube, starting from with arbitrary. After round it takes a projected gradient step (Algorithm 4, online gradient descent) against the loss vector :
where is the Euclidean projection. It then sets to the output of the oracle Algorithm 3 on , which puts weight on at most two adjacent grid points where changes sign.
For , , every outcome sequence and every run of Algorithm 5 with ,
This is the bound of display (14) with the paper's constant .
The bound shows that a forecaster with logarithmic per-round cost has calibration error vanishing at rate against every outcome sequence. Earlier calibrated forecasters required solving a linear program or computing a fixed point each round. The construction is also the paper's worked instance of its general equivalence: a calibration problem, posed as approachability of an ℓ₁ ball, is solved by a no-regret learner on the dual unit cube together with a halfspace oracle.
The result is proved in the paper; no machine-checked version is known to exist. The formalization makes explicit three points the paper leaves informal: the step size, the sign of the gradient step, and the gap between the forecast distributions and the sampled forecasts. The milestones are reusable on their own: the ℓ₁/ℓ∞ duality, and the regret bound of online gradient descent for linear losses on a general closed convex set.
The chain (12)–(14) looks like a direct composition, but each link has content. The oracle guarantee needs a case analysis over the sign pattern of , including the degenerate case . The reduction (12) needs the duality (13) with attained minima, and it holds only outside the ball . The regret bound of online gradient descent needs the non-expansiveness of the Euclidean projection and a telescoping argument. The tempting shortcut of quoting "OGD has regret " does not give the stated constant without fixing the step size.
Vectors are EuclideanSpace ℝ (Fin (m+1)), with grid index as Fin (m+1) and as a real quotient; the ℓ₁ norm and the cube are written out coordinatewise. Rounds are . Minima over sets are stated through IsLeast or as the infimum of the image of a nonempty bounded set. Algorithm 3 is a relation that allows every sign-change index the binary search might return. The projection is any Euclidean minimizer onto the cube.
Conventions and corrections, each disclosed in the item's Formalization Note:
A trivializing formalization is ruled out. The rate is defined from Definition 19's formula, not as a distance, and the step size is pinned. A free step size would make the bound false, and an empty oracle relation would make it vacuous; milestone 3's existence clause excludes the latter.
Contributions are welcome on each milestone. The online gradient descent bound and the ℓ₁/ℓ∞ duality are independent of calibration. The published one-step inequality LogRegretOCO.OGD.one_step_inequality is included as a reference item for the regret bound.
A matching in a graph is a set of edges no two of which share a node. Given a real weight on every edge, the maximum-weight matching problem asks for a matching of largest total weight. It is one of the basic problems of combinatorial optimization: assignment, pairing and scheduling problems reduce to it, and it is the standard example of a combinatorial problem that is solvable in polynomial time although it is not obviously a linear program.
For bipartite graphs the problem is a linear program in disguise: the polytope cut out by nonnegativity and the node-degree inequalities has only 0–1 vertices (the Birkhoff–von Neumann theorem in the square case; Mathlib has it as extremePoints_doublyStochastic). For general graphs this fails already on a triangle, where the vector with every coordinate satisfies all degree inequalities but is not a combination of matchings. Edmonds' 1965 paper (DOI 10.6028/jres.069b.013) adds one family of inequalities, one for each odd set of nodes, and proves that the resulting polyhedron has exactly the matching vectors as its vertices. The companion paper Paths, trees, and flowers gives the cardinality algorithm on which the weighted algorithm of §7 is built.
Timeline:
Let be a finite graph with node set and edge set ; each edge meets two different nodes, its ends. Real variables correspond to the edges . The polyhedron is the set of vectors satisfying
The matching vectors are the vectors with every component or that satisfy (2); they are the incidence vectors of matchings. For edge weights , the linear form (4) is .
The dual program has a variable for each node and for each odd set (, ). Its objective is (5) , subject to (6) and (7) for every edge with ends . For a matching , conditions (8)–(10) are the complementary slackness conditions: at nodes not covered by , equality in (7) on , and every odd set with contains exactly edges of .
A blossom sequence (Theorem (M)) starts from with matching and repeatedly shrinks an odd circuit (a blossom, edges of which are matched) to a single node, carrying node weights and edge weights that obey conditions (a)–(k) of p. 127.
In the Lean development these are Graph, IsMatching, incidence, matchingPolyhedron (), matchingVectors (), W, U, DualFeasible ((6)–(7)), CompSlack ((8)–(10)) and BlossomSequence, all in the namespace EdmondsMatching65.Polyhedron.
The vertices (extreme points) of are exactly the matching vectors of . Hence the maximum weight of a matching equals for every .
The result. Theorem (P) turns maximum-weight matching in general graphs into a linear program over an explicitly described polyhedron, and Theorem (M) with the §5 translation gives a short certificate of optimality for every maximum matching. Together they established the template of polyhedral combinatorics: describe the convex hull of the combinatorial objects by inequalities, and prove the description through linear programming duality and an algorithm. The matching polytope underlies the analysis of the weighted blossom algorithm, separation over odd-set inequalities (Padberg–Rao), and many later integrality results; Edmonds' own §8 states the extension to degree-constrained subgraphs.
Formalizing it. The theorem has been proved since 1965 and appears in every text on combinatorial optimization; this mission asks for a machine-checked proof of the polytope statement for general finite graphs, including parallel edges, together with the duality certificate and the blossom-sequence characterization. The prove2me platform has a proved form of Edmonds' perfect matching polytope theorem on complete graphs in convex-decomposition form (MetricTSP.pm_polytope_decomposition), a different polytope with a different conclusion; nothing states Theorem (P) or Theorem (M).
The inclusion and weak duality are routine. The difficulty is the reverse inclusion: showing that no fractional point of is a vertex. The bipartite argument (a fractional point has a cycle of fractional edges along which it can be perturbed both ways) breaks on odd cycles: perturbing along an odd circuit violates a degree inequality, and the odd-set inequalities that cut off the half-integral points are exponentially many and overlap. The paper's route needs, for every weight vector, an optimal matching together with a dual solution satisfying (6)–(10), and the existence of that certificate is the substance of the weighted matching algorithm: the blossom sequence of Theorem (M) must be constructed, and the translation (11)–(16) from node and edge weights of the contracted graphs to must be verified through the whole shrinking history.
V, a finite edge type E and an end map ends : E → Sym2 V with no loops. Parallel edges are allowed: the contracted graphs of Theorem (M) have them, and Theorem (P) holds for multigraphs; simple graphs are the case of an injective end map.E → ℝ, one coordinate per edge. Vertices are Mathlib's Set.extremePoints ℝ. Odd sets carry an explicit r : ℕ with 1 ≤ r and |S| = 2r + 1; even sets and singletons carry no inequality.|V|.z is a function on all node sets of which only odd sets are read.Gᵢ is a partition of V into blocks; an edge of G is an edge of Gᵢ when its ends lie in different blocks. Each Mᵢ must be a matching of Gᵢ, and all of (a)–(k) appear as fields of BlossomSequence; a sequence missing any of them would make milestone 6 trivial or milestone 5 false.Sym2 V → ℝ) leave non-edge coordinates free and give a polyhedron with no extreme points, and the goal is stated as equality of extreme points, not as a convex-hull identity or as the existence of a dual certificate.