Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Ordinary least squares and its robust relatives (least absolute deviations, Huber, -insensitive and quantile regression) fit a linear predictor by minimizing an average loss over the training sample. That average estimates the out-of-sample error poorly when the sample is small, and the usual fix is to add a regularization penalty such as a norm of the weights. Choosing that penalty is often a heuristic. Distributionally robust optimization gives one principled derivation of it: hedge against every data-generating distribution that is close to the empirical one in a Wasserstein distance, and minimize the worst-case expected loss.
S. Shafieezadeh-Abadeh, D. Kuhn and P. Mohajerin Esfahani, Regularization via Mass Transportation (arXiv:1710.10016v3, 2019; JMLR 20, 2019), show that for linear regression with a convex Lipschitz loss this worst-case problem is exactly a regularized empirical risk problem, with an explicit dual-norm penalty. The same identity appears for the logistic loss in Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn, Distributionally Robust Logistic Regression (NeurIPS 2015, arXiv:1509.09259). For a general convex loss it is Theorem 10 of the tutorial by Kuhn, Mohajerin Esfahani, Nguyen and Shafieezadeh-Abadeh (arXiv:1908.08729). Blanchet, Kang and Murthy (arXiv:1610.05627) obtain the square-root Lasso from a type-2 transport cost. This mission formalizes the regression theorem of the first paper, Theorem 3.1(ii) on p. 8. The source PDF is the arXiv preprint v3, and every page and label cited here refers to it.
Data. Inputs are and outputs are . A pair is written . The training samples are for , and is their empirical distribution (§2.1, p. 5).
Hypotheses and loss. A weight vector defines the linear hypothesis . A univariate convex loss defines the regression loss (§3.1, p. 8). The residual is the pairing of with the vector .
Norms. carries an arbitrary norm with dual norm (§1.1, p. 4). The Lipschitz modulus of is , and the convex conjugate is (§1.1).
Wasserstein ball. With transport cost , the Wasserstein distance (Definition 2.2, p. 7) is
where the infimum runs over couplings of and . The ball of radius is (3). The distributionally robust regression problem is
Let , , , and let be nonnegative, convex and Lipschitz continuous. Then for every
so (4) and the regularized problem (6) have the same optimal value.
WassersteinDRO.Duality.strong_duality_worst_case_risk_v2, which covers it for .The result. The theorem turns an infinite-dimensional min–max problem over distributions into a finite convex program over : an empirical average plus a norm penalty. The penalty is not but , because the transport cost moves outputs as well as inputs. It scales with the radius and with the Lipschitz modulus of the univariate loss. With the Huber, -insensitive and pinball losses it gives Corollaries 3.2–3.4 of the paper. It also gives a statistical reading of the regularization weight as a Wasserstein radius, which the paper's §4 turns into generalization bounds.
Formalizing it. The theorem is proved in the paper; none of its items is formalized yet except Lemma A.1. Lemma A.1 is available in a general form (any , any closed support set, ) as a proved platform theorem from the mission Wasserstein Distributionally Robust Optimization. The per- identity also follows from the proved WassersteinDRO.Duality.convex_loss_p1_v2 (Theorem 10 of the tutorial, also present as WassersteinDRO.Regularization.convex_loss_p1_v2; the public mission Wasserstein Distributionally Robust Optimization IV has it as goal) once one shows that . No platform item states that factorization. What this mission adds is the paper's explicit form of the penalty, Lemma A.3 (the inner supremum for an arbitrary convex Lipschitz loss and an arbitrary norm), and the conjugate description of the Lipschitz modulus. The last two are reusable in classification (mission I of this series states them again in its own namespace) and in every Wasserstein-regularization result with linear hypotheses.
The obvious argument is to write the worst case as a supremum over perturbations of the samples and bound each perturbed loss by its Lipschitz constant. That gives only the inequality "", and only for one Lipschitz constant. The identity needs two further steps that this bound does not supply. First, the bound must be attained: the supremum over distributions has to be shown to reach , a matching lower bound that a Lipschitz estimate cannot give. Second, must be the modulus, not any constant: an upper Lipschitz constant makes the identity false. In Lemma A.3 the case sits exactly on the boundary between a finite and an infinite supremum. A further point is that the duality of Lemma A.1 needs , while the theorem includes .
E with its Borel σ-algebra. A continuous linear isomorphism e : E ≃L[ℝ] (Fin n → ℝ) × ℝ reads off inputs and outputs. The theorem therefore covers every norm on ; fixing a concrete norm would prove it for that norm only. The functional is pairing e w, and is its operator norm.WassersteinDRO_Duality_ambiguitySet, _worstCaseRisk_v2, _empiricalDistribution and _lipschitzModulus. The worst case is taken in the extended reals, and expectations follow the convention of nominalRisk_v2 (no junk value for non-integrable losses). takes values in .A basic question of additive combinatorics asks how a set grows under repeated addition. If a finite set in an abelian group satisfies for some finite set , how large can the iterated sumsets be? Plünnecke's inequality gives the answer used throughout the subject: some nonempty part of grows by at most a factor per added copy of . Combined with Ruzsa's triangle inequality it becomes the Plünnecke–Ruzsa inequality , which underlies Freĭman-type structure theorems, sum–product estimates and the polynomial Freĭman–Ruzsa programme.
Timeline.
Let be a group with finite subsets , , . The product set is , and denotes cardinality. In an abelian group, written additively, the sumset is , and for the iterated sumset is with summands, . It is not the dilate .
A nonempty subset has minimal growth under if
Such an exists whenever is nonempty, since has finitely many subsets. In Lean, is a Group or AddCommGroup with decidable equality, the sets are Finset G with the pointwise operations of Mathlib (A * B, A + B, h • B), and cardinalities are #A cast to ℝ.
For finite , in an abelian group with nonempty and , there is a nonempty with
The point is the order of quantifiers: one serves all .
FamousTheorems.pluennecke_petridis (additive notation, cross-multiplied), and enters the mission as a reference.Theorem 3.1 is the form of Plünnecke's inequality used in applications. Two consequences follow directly. Taking gives whenever . Combining one for all with Ruzsa's triangle inequality gives (Theorem 1.2 of the paper). With a separate for each , the second step would need the same set for and , and that is exactly what Theorem 3.1 provides. Theorem 1.5 is the non-abelian ingredient: missions 2 and 3 of this series apply it to obtain explicit Plünnecke-type bounds for and in arbitrary groups.
Formalizing it. The results are proved and classical. Mathlib already contains Proposition 2.1 (Finset.pluennecke_petridis_inequality_mul) and the Plünnecke–Ruzsa inequality Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add. Its proof runs through a private lemma that bounds for one fixed minimiser, but no public statement in Mathlib or on the platform asserts Theorem 3.1 or Theorem 1.5 in the form "there exists a nonempty for all " (respectively "for all "). This mission adds those statements as reusable, citable nodes in the paper's numbering.
A first attempt iterates the hypothesis directly: would follow if again grew by a factor under , but nothing controls the growth of . The ratio is not monotone in , and passing to subsets of can only help if the subset is chosen correctly. Choosing a different good subset for each gives Theorem 1.1 but loses the uniformity. The work is to show that one fixed subset controls all the products simultaneously, and in the non-abelian Theorem 1.5 to keep the order of the factors , , throughout.
AddCommGroup with DecidableEq. Theorem 1.5 is stated in a Group, with no commutativity, as on the page. The factor order is preserved.h • B (the -fold sumset; 0 • B = {0}), and "for all " ranges over all natural numbers, including the true case .ℝ. No hypothesis is added: it follows from the hypotheses once and are nonempty (with empty they force only , and every conclusion is still true).Finset.ruzsa_covering_mul, Finset.ruzsa_triangle_inequality_mul_mulInv_mul) and are not items of this mission.Single-item inventory theory asks how much stock to order each period when the order carries a fixed cost on top of a per-unit cost and demand is random. With independent, identically distributed demand, Scarf (1960) showed that the optimal finite-horizon policy has the form: when the stock falls below the reorder point , order up to the level ; otherwise order nothing. His proof introduced -convexity.
In practice demand is rarely i.i.d. It depends on economic conditions, seasons, or the stage of a product's life cycle, which change over time and carry over from one period to the next. Song and Zipkin (1993) modeled this by letting a Markov chain of "world states" modulate the demand distribution. Sethi and Cheng (1997) treat a general discrete-time model of this kind. The demand density, the cost parameters and the surplus cost all depend on the period and on the current demand state. They prove that a state-dependent policy is optimal over a finite horizon. They require no growth condition on the backlog cost, and they allow and to be .
Timeline:
There are demand states and periods . The state in period follows a Markov chain with transition matrix . Given , the demand has density , with mean at most . At the start of period an order is placed and arrives at once. Then demand is subtracted, and unmet demand is backlogged:
Ordering costs , with for and otherwise, and . A surplus costs , a convex, nonnegative function with and .
A decision may depend on the whole observed history: the states up to the current one and the past demands. The objective and the value function are
With
the dynamic programming equations are and
A function is -convex if for all , .
Assume, for and all ,
Then there are extended reals such that the rule
(a) attains the infimum in the dynamic programming equation at every , , , and (b) generates a policy whose expected cost equals , the infimum over all admissible history-dependent policies.
The theorem shows that the form survives when demand is driven by a Markov environment, with fixed costs that may vary by state and period. The only coupling condition is (4.1), under which today's fixed cost is at least the expected fixed cost of the next period. It needs no assumption on the backlog side, such as . When ordering never pays, the levels are . The result is the base case of the paper's later extensions: no-ordering periods, capacity limits, and the discounted infinite horizon (a separate mission in this series). Policies of this kind are what practitioners compute.
The result is proved in print. The paper delegates Theorems 3.1–3.2 to Beyer, Sethi and Taksar (1998). It contains gaps, which this mission records and repairs:
A machine-checked proof settles these points. No formalization of the theorem or of its verification step exists. Published platform results cover the narrower Lemma 4.2.1 of Bertsekas, for continuous functions coercive at both ends.
The -convexity calculus is elementary. The difficulty lies elsewhere:
Conventions committed to in Lean, namespace SethiChengSS.Finite:
Fin L; periods are natural numbers with the paper's base.(t, states i_n…i_{n+t}, demands ξ_n…ξ_{n+t−1}). It is admissible if it is nonnegative and measurable in the demands. So it cannot see the current or future demand, and nothing restricts it to Markov rules.lintegral/⨅ in .EReal, with and only if .Trivializations excluded:
K-convexity is the published definition BertsekasKConvex. The published Bertsekas lemmas (BertsekasDP.kconvex_of_convex, kconvex_combination, kconvex_expectation, kconvex_sS_structure) are included as references. Each is narrower than its counterpart here: positive coefficients only, finite support only, continuity and coercivity at both ends. The posed SongZipkinFluct.FixedCost.theorem3 concerns a different, continuous-time model with integer levels and linear costs and is not used.
Welcome contributions: reusable infrastructure for path-space expectations of Markov-modulated processes; verification theorems for finite-horizon DPs with history-dependent policies; the extended-real -convexity lemmas of Proposition 4.2.
Split Euclidean space into finitely many measurable cells and record, for each cell, its Gaussian first moment, the integral of against the standard Gaussian measure over that cell. How large can the sum of the squared lengths of these vectors be? The propeller conjecture predicts that, with at least three cells in dimension at least two, the answer is , attained by three planar sectors of angle (a "propeller") times the orthogonal complement. The question arose in Khot and Naor's work on approximate kernel clustering (Mathematika 2009), where this Gaussian partition parameter determines both the approximation ratio of Gaussian rounding and the matching Unique-Games hardness threshold. The surprise is that more cells or more dimensions do not help: the optimum uses only three cells in a plane.
This mission asks for a formal proof of the propeller bound in every dimension, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be the standard Gaussian probability measure on , with density . For a measurable set , its centroid is the unnormalized vector
A measurable partition of consists of measurable sets such that almost every point (for ) lies in exactly one of them; empty cells and arbitrary cell probabilities are allowed. Its value is . The propeller is the partition of , , into the three sets , where are the planar sectors of opening bounded by the rays at angles and , with any further cells empty.
For all positive integers and every measurable partition of ,
and for , the propeller is a measurable partition attaining equality.
The result itself. It settles the propeller conjecture in all dimensions and for all numbers of cells, without constraints on cell masses. Through Khot and Naor's analysis, the constant fixes the loss factor of Gaussian rounding for identity-target kernel clustering; combined with the companion Unique Games preprint, the preprint deduces NP-hardness of any better fixed loss factor (Theorem 6.1, p. 18). The bound also gives a sharp inequality for expected Gaussian maxima (Corollary 5.1, p. 17).
Formalizing it. A formal proof needs Gaussian measures on Euclidean space (available in Mathlib as stdGaussian), a compactness argument for extremal partitions, the convex case of the Ehrhard inequality, and the three-dimensional theorem of Heilman, Jagannath and Naor, which the preprint uses as an established input and which itself relies on a finite computer verification. Each of these is a reusable component; the three-dimensional case alone would be a substantial formalization.
The optimization runs over all measurable partitions, with both shapes and probabilities free. Khot and Naor's reduction gives conical extremizers whose nonzero centroids span an -dimensional space, so the three-dimensional theorem disposes of active cells. The remaining cases cannot be handled by any fixed finite computation. The preprint constrains them in two ways: deleting one score costs a definite amount of expected maximum, via concavity from the Ehrhard inequality (Section 3), and competition against two residual scores constrains a covariance determinant (Section 4, Lemma 4.1 and Corollary 4.2, pp. 11–12). Combining these must rule out every configuration with five or more cells.
Space d is EuclideanSpace ℝ (Fin d) and the measure is stdGaussian. IsPartition A asks each cell to be measurable and almost every point to lie in exactly one cell, matching the paper's convention that partitions are taken up to null sets.centroid A is the Bochner integral of the identity over A; value sums squared Euclidean norms. Integrability holds because Gaussian measures have finite first moments.propeller d k (cells empty) is a partition with value exactly . The sectors are written with closed inequalities, so they overlap only on null rays.Many learning tasks run on data about people: medical records, purchase histories, survey answers. A learner whose output reveals too much about any one training example is unusable on such data, however accurate it is. Differential privacy (Dwork, McSherry, Nissim and Smith, 2006) makes "reveals too much" precise: changing one individual's record may change the probability of any outcome of the algorithm by at most a factor .
Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith asked which concept classes can be learned under this constraint, and at what cost in examples. This mission formalizes their first answer (§3 of the paper): every finite concept class can be learned privately in the agnostic model, with a sample size that grows only logarithmically in the size of the class. The result is the private counterpart of the cardinality version of Occam's razor (Kearns and Vazirani, An Introduction to Computational Learning Theory, 1994, p. 35). The paper appeared in SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; all indices below are those of arXiv:0803.0924v3.
The learner is an instance of the exponential mechanism of McSherry and Talwar (FOCS 2007), which selects an output with probability exponentially weighted by a quality score.
A database of size over a domain is a vector . Databases are neighbors if they differ in exactly one entry. A randomized algorithm is described by the law of its output on each input. It is -differentially private (Definition 2.1) if
for all neighbors and all measurable sets of outputs.
Learning uses a finite set of examples and labels . A hypothesis is a map , and is a finite nonempty class of hypotheses; in the theorem , the concept class itself. Data are drawn i.i.d. from an arbitrary probability distribution on (the agnostic setting, Definition 2.5). The error of is , and . On a database the score is and the training error is .
The exponential mechanism outputs with probability proportional to . In Lean these objects are IsDP, err, OPT, score, errT and expMech in the namespace PrivLearn.Generic.
There is an absolute constant such that for every finite , every finite nonempty , every and all :
the mechanism run on i.i.d. samples from satisfies
The constant is left unspecified, as the paper's leaves it. The qualitative first sentence of Theorem 3.4 (classes of size are privately agnostically learnable) follows at once, because then is polynomial in .
Theorem 3.4 shows that privacy costs little in sample complexity when computation is unconstrained. Any class that some learner with polynomially long output can learn is learnable privately from polynomially many examples. The non-private agnostic bound is ; the private one is larger by a factor when , and is the same otherwise (Remark, p. 12). The theorem is the baseline the rest of the paper refines: an efficient private learner for parity (§4) and the equivalence of local privacy with statistical query learning (§5). It also underlies later work on the sample complexity of private learning, such as Beimel, Kasiviswanathan and Nissim (TCC 2010).
The result is proved in the paper; to our knowledge it has not been machine-checked. The mission produces a checked statement of the exponential mechanism's privacy and of its learning guarantee with an explicit dependence on , , and . It also provides a reusable bounded i.i.d. Hoeffding inequality (Theorem A.2) in the form learning theory uses. Formalizing the proof with any explicit constant is welcome. The constant printed at the end of the proof does not, by itself, make the last inequality close (the two error terms add to more than ), so a correct constant is a genuine contribution.
Privacy and accuracy pull in opposite directions. Empirical risk minimization, the obvious learner, is not private: replacing one example can change which hypothesis minimizes the training error, and the output then changes with probability one. Smoothing the choice must not destroy accuracy, and the accuracy argument must hold simultaneously for every hypothesis in the class, with the mechanism's randomness and the sample's randomness combined into one failure probability. In Lean the measure-theoretic bookkeeping is non-trivial: the output is a measure on a function space, the failure probability integrates the mechanism's law against the product measure , and the privacy bound must hold for every measurable event, not only for single hypotheses.
Fin n → X × Bool, indexed from ; neighbors differ in exactly one coordinate.X → Bool with the product σ-algebra. It is a probability measure because is nonempty and all weights are positive; the theorems assume nonempty, and the definition does not build normalization in.Type so that the absolute constant can precede it.Bool, standing for . Logarithms are natural (Real.log), as in the paper's .ComputationalLearning.vcDim (Kearns–Vazirani's Definition 9, the same notion as the paper's Definition 3.5) and references the platform's proved Sauer lemma.Contributions welcome: proofs of any milestone, a measurable-structure library for finite output laws, and a general exponential-mechanism privacy theorem from which Lemma 3.3 follows.
In a road or communication network, traffic is routed by many independent users, each choosing a route that is fastest for itself given the congestion caused by everyone else. The resulting Nash flow (also called a Wardrop equilibrium, after Wardrop 1952) need not minimize the total delay experienced by all users: Braess's paradox shows that adding a road can make everyone slower. Network designers, transport economists and the designers of Internet congestion-control protocols therefore ask how much total delay is lost to selfish routing, compared with a centrally optimized routing of the same traffic.
Roughgarden and Tardos (J. ACM 2002) gave the first general answers. For linear latency functions they showed that the loss is at most a factor . For general latency functions they showed that no such factor exists, and proved instead a bicriteria bound: selfish routing is never worse than optimal routing of twice the traffic. This mission formalizes that bicriteria bound (§3 of the paper) together with its variants for an arbitrary traffic increase (Theorem 3.2) and for approximate equilibria (§5.1).
Timeline:
A network has edges and routes ; route is a set of edges. There are commodities ; commodity is served by a set of routes and has a rate , the amount of traffic it must send. A flow assigns an amount to each route; it is feasible for the rates if for every . The flow on edge is .
Each edge has a latency function , nonnegative, continuous and nondecreasing on : the delay of one unit of traffic crossing when the edge carries . The latency of a route is , and the cost of a flow is the total delay
A feasible flow is at Nash equilibrium (Definition 2.1) if no amount of the flow on a route , moved to another route , would find a latency on smaller than the latency it had on . Lemma 2.2 shows this is equivalent to the Wardrop condition: every route carrying flow has minimum latency among the routes of its commodity. Definition 5.1 relaxes the equilibrium by a factor .
In the Lean development: pathLatency A ℓ x r is , cost A ℓ x is , IsNashFlow A s ℓ rate x is Definition 2.1, IsApproxNashFlow A s ℓ rate ε x is Definition 5.1, and barLatency is the auxiliary latency of the proof of Theorem 3.1. Edge flows and feasibility are the published KellyStochasticNetworks.linkFlow and wardropFeasible.
If is a Nash flow for the rates and is any flow feasible for the rates , then
The comparison is with every flow of twice the rates, not only an optimal one.
The edge form of the cost (§2.1), Lemma 2.2 (Nash Wardrop), Lemma 2.3 ( for the common latency of the flow-carrying routes of commodity ), and the two displayed inequalities of the proof of Theorem 3.1:
Theorem 3.2: for and feasible for ,
Lemma 5.2 (the approximate analogue of Lemma 2.2) and Theorem 5.3: for , an -approximate Nash flow and feasible for ,
The price of anarchy, the ratio of the cost of a Nash flow to the minimum cost, is unbounded for general latencies: with two parallel links of latencies and , the ratio tends to infinity as grows. Theorem 3.1 shows that the inefficiency of selfish routing can nevertheless always be offset by doubling capacity, in the sense that the optimal cost of twice the traffic is at least the Nash cost. Theorem 3.2 quantifies the trade-off for any traffic increase and is essentially tight. These results were among the first quantitative bounds of the price-of-anarchy programme and are a standard part of algorithmic game theory courses.
All statements here are proved in the paper (Theorem 5.3 with its proof omitted there as a close copy of Theorem 3.1). To our knowledge none has a machine-checked proof. This mission produces Lean proofs of Theorem 3.1, its supporting lemmas and its two variants, on top of the published Wardrop-equilibrium definitions of Kelly and Yudovina's chapter on road traffic; existence of a Wardrop equilibrium is already proved on the platform (KellyStochasticNetworks.wardrop_equilibrium_exists), so the goal's hypothesis is satisfiable.
The obvious comparison of with route by route fails: can place its traffic on edges whose latency is much lower than the Nash latencies, and nothing in the latency functions bounds how much lower, since they are only continuous and nondecreasing. A naive bound on the ratio is ruled out by the example above, so any proof must use the doubled rates essentially. In the Lean development, the passage from Definition 2.1 (a statement about perturbed flows) to the Wardrop condition needs a limit through continuity on , and the cost manipulations need exchanges of finite double sums over routes and edges.
A, each assigned a commodity by s. The paper's family of simple – paths is one instance; the statements therefore hold for every route family (a disclosed generalization; the proofs use no graph structure). Two copies of one edge set serving two commodities are two routes.wardropFeasible s (fun i => 2 * rate i); for it is wardropFeasible s (fun i => (1 + γ) * rate i). Replacing by would make the goal false (Pigou's example), and comparing only with an optimal would weaken it.Needed infrastructure: finite double-sum exchanges, a one-sided limit argument for continuous functions on , and bookkeeping of the perturbed flow . The lemmas relating Definition 2.1 to the Wardrop condition are reusable by every later result on nonatomic routing games, including the other missions of this series. Contributions of proofs of any milestone are welcome.
Telephone call centers are among the largest employers of service labour, and their staffing decisions are made with queueing models. The classical model is the Erlang-C queue : Poisson arrivals, agents, exponential service, infinitely patient callers. Real callers hang up. Garnett, Mandelbaum and Reiman (M&SOM 2002) argued that a model ignoring abandonment is misleading exactly in the regime where large call centers operate, near full utilization: the Erlang-C queue is unstable when the offered load exceeds the number of agents, while a real center simply loses the excess callers. They advocated the Erlang-A queue , in which each caller also has an exponential patience, and developed its many-server asymptotics.
The first of their asymptotic results, Theorem 1 of the paper, settles the most basic performance measure, the fraction of callers who abandon, to first order as the center grows. Its proof combines a utilization argument with two monotonicity properties proved by Bhattacharya and Ephremides (1991) and an asymptotic expansion of Erlang's loss formula due to Jagerman (1974).
Callers arrive as a Poisson process of rate . There are statistically identical agents, each serving one caller at a time with exponentially distributed service times of rate . The waiting room is unlimited and is served in order of arrival. Each caller carries a patience, an exponential random variable of rate independent of everything else; a caller whose wait in queue reaches his patience abandons and does not return.
The number of callers in the system, , is a birth–death process with birth rate in every state and death rate
in state . Its stationary distribution (Appendix B of the paper, with infinite buffer) is
with normalizing. The abandonment probability is the probability that a caller arriving in steady state abandons. An arrival finding callers in the system abandons with probability , so
The blocking probability of the loss system with the same rates is Erlang's formula .
The asymptotic regime. The -th system has agents, arrival rate , service rate independent of , and patience rate . As in §4 of the paper, and . The traffic intensity is .
If for some , then
with . The limit does not depend on .
KellyStochasticNetworks.erlang_strictMono).Theorem 1 is the law-of-large-numbers description of an overloaded or critically loaded many-server queue with abandonment. It says that an overloaded center sheds exactly its excess load, , to abandonment, and that a critically loaded center () already has vanishing abandonment. This is what directs attention to the Halfin–Whitt (quality-and-efficiency-driven) regime , where the paper's later results (Theorems 2 and 4) refine the picture to order . It is also the fluid-scale input of later work on staffing with abandonment.
The theorem has been proved in the paper; to our knowledge none of the statements above has a machine-checked proof. The mission produces a formal model of the Erlang-A queue with its stationary law, a verified bridge between the Erlang-A and Erlang-B (loss) systems, and a formal limit theorem for Erlang's loss formula under linear load, each reusable in other many-server problems.
The heuristic is immediate: utilization is at most one, so gives the lower bound . The upper bound is the substance. A direct estimate of the series defining involves -dependent products whose asymptotics are not elementary, and the result must hold uniformly over patience rates that are only known to be positive. Two further obstacles remain: the monotonicity of in and in is a stochastic-ordering property of the birth–death process, not a term-by-term inequality between the series, and any comparison with the loss system needs the asymptotics of Erlang's formula under a load that is linear in only up to . Nothing is assumed about how approaches its limit, so the critical case cannot be read off from either side.
ErlangA.Abandonment. The death rates, the unnormalized weights , (a tsum) and are explicit definitions of the parameters and ; is the published KellyStochasticNetworks.erlang (λ/μ) N.QueueingFundamentals.BirthDeath.IsSteadyState). The time limit is not formalized. The buffer is infinite.Filter.Tendsto along ; "" is Asymptotics.IsEquivalent; is "for every , eventually ".tsum, a divergent normalizing series would make and , which would make the underloaded case of the goal vacuous; milestone 1 asserts that is a genuine probability distribution for every and , and the goal is stated for exactly these parameters.AdaBoost (Freund and Schapire, 1997) combines many weak classifiers into a weighted vote . At each round it fits a classifier to a reweighted training sample, sets from the weighted error , and multiplies the weights of the misclassified points by . The algorithm was introduced as a procedure for boosting the accuracy of weak learners in the PAC sense, and its good test performance was at first not explained by any statistical model.
Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) recast boosting as stagewise fitting of an additive model by minimizing the exponential criterion . Their Lemma 1 shows that is minimized at half the log-odds, so an additive fitted this way estimates a logistic regression model. Result 1 of that paper, the subject of this mission, shows that Discrete AdaBoost is exactly such a fitting procedure: in its population version, each round is a Newton-like step on followed by an exact line search, and the resulting reweighting is AdaBoost's. This view underlies gradient boosting, LogitBoost and the loss-function analysis of boosting in later work.
Let be a measurable space of features and let be a probability law of the pair on . The conditional law of given is the disintegration , and is the integral against it. A current estimate is a measurable , and the exponential criterion is
With weight , the weighted conditional expectation and the weighted expectation are
A classifier is a measurable ; its weighted error is . The paper's candidate update is with
Algorithm 1 (p. 338) uses and the update followed by renormalization.
For measurable with :
so the population reweighting coincides with Algorithm 1's after renormalization.
The result. Result 1 turns AdaBoost from a combinatorial reweighting scheme into an optimization method with a known objective. It identifies the population quantity the algorithm estimates (via Lemma 1, half the log-odds), explains the specific constant as an exact line search, explains why the weights of misclassified points are inflated by , and shows that a weak learner worse than chance is used with reversed sign. It is the template for the other population results of the paper (Real AdaBoost, LogitBoost, Gentle AdaBoost) and for later functional-gradient views of boosting.
Formalizing it. The result is proved on paper; it has not been machine-checked. The paper's argument is stated informally ("≈", "arg min", "Newton-like"); this mission fixes each claim as a precise statement about measures on . The sample version of Corollary 2 is already proved on the platform (UnderstandingML.adaboost_reweighted_error) and is reused; everything else is new.
Each step is elementary on its own; the work is in carrying the population statements through measure theory. The weighted expectations are ratios of integrals that are meaningful only under integrability of , and the line-search claim compares for all real , all of which must be shown finite before they can be compared as real numbers. The pointwise claim (16)–(18) uses the conditional law of given , which exists only as a disintegration kernel; passing from it to the unconditional (17) requires the disintegration identity and measurability of (18) in . The tempting shortcut of treating as its quadratic approximation does not prove the line-search claim: (20) is the exact minimizer of , not of the approximation.
Labels are Booleans, with for true and for false. is a lower Lebesgue integral in and is compared there; and are ratios of Bochner integrals, the conditional one against ν.condKernel x. Disclosed additions, each needed for the page's formulas to be defined: and measurable, , and wherever is used. No condition is imposed. Ties go to , as printed. The "≈" of the expansion is read as "second-order Taylor polynomial in ", and derivatives are stated with HasDerivAt.
Trivializing formalizations are excluded: is not defined by a conditional formula or as a Bochner integral (which would return on non-integrable weights and make every step optimal), the logarithm is never applied outside its domain, and the class of stays -valued (over real-valued the Newton step is Gentle AdaBoost's, a different result).
Everything is in the namespace AddLogReg.Discrete, with one definitions file (Setting) holding , , the classifier (18), and the coefficient (20). Reusable pieces are lemmas on disintegrations of laws on and on weighted expectations. Proofs of any milestone are welcome independently.
Retailers accept large volumes of returned merchandise, and a common default is the full refund: a buyer who is unhappy with a product brings it back and gets the whole price back. Many consumers only learn how much they value a product after they have it at home — clothes that do not fit, a gadget that does not suit the buyer's needs. A returns policy therefore plays two roles at once. It raises the buyer's willingness to pay before purchase, and after purchase it decides which units stay with consumers and which go back to the seller to be salvaged.
Xuanming Su's paper Consumer Returns Policies and Supply Chain Performance (SSRN 1020451; published in Manufacturing & Service Operations Management 11(4), 2009, doi:10.1287/msom.1080.0240) puts this effect into a newsvendor model with random demand. The earlier literature it builds on, notably Che (1996) and Davis, Gerstner and Hagerty (1995), asked whether a seller should offer full refunds or no returns at all. Su's model makes the refund amount a separate decision variable. The answer it gives is closed-form and sharp: the optimal refund equals the salvage value. This mission formalizes Sections 3–4 of the paper: the single-seller model, the full-refund benchmark, and the optimal partial refund.
A seller stocks a quantity before a selling season at unit cost . Unsold and returned units are salvaged at value . Market demand is a nonnegative random variable with law , distribution function and . Each consumer who buys learns a valuation after purchase. Valuations are i.i.d. with law and finite mean , and the standing assumption is .
The seller chooses a price , a quantity and a refund . Once a consumer has bought, they keep the product if and return it otherwise. The keep and return probabilities are
Before purchase a consumer's expected utility from buying is , so this is the reservation price. Every consumer buys if and nobody buys otherwise (the demand rule (6)). With the expected sales of a stock , the seller's expected profit (7)–(8) is
and otherwise. Two special cases serve as benchmarks. Under full refunds () every consumer buys and the profit is , from (1)–(2). Under no returns the price is and the profit is , from (3). Social welfare (12)–(13) is the sum of consumer surplus and seller profit, , again subject to the demand rule.
With , and any satisfying
the triple maximizes over all prices, all refunds and all quantities :
The result separates two things that a full refund ties together: the price and the refund. Setting sends every unit back to its more valuable use. Consumers who value the product above its salvage value keep it, and the rest return it to be salvaged. The price then extracts the whole expected surplus. Consequences follow directly. Partial refunds dominate both full refunds and no returns (Corollary 1). They raise the stocking quantity, which benefits an upstream manufacturer paid per unit ordered. With valuation uncertainty resolved only after purchase, the monopoly outcome is welfare-maximizing (Corollary 2). Section 5 of the paper, formalized in the companion mission, uses Proposition 2's triple as the first-best target that supply chain contracts must implement.
The results are proved on paper with short arguments in Appendix A of the paper. None of them has a machine-checked proof. The mission's contribution is a formal model of consumer returns with the demand rule built in, plus checked versions of Propositions 1–2 and Corollaries 1–2 for general valuation laws (with atoms), not only densities.
The paper's proof treats the problem as separable: first maximize the margin over , then solve a newsvendor problem in . Two steps that are routine on paper need care. First, the margin bound must hold over the whole constrained region , including refunds above the price and negative prices. It rests on comparing with , which needs the closed half-line convention to hold up at atoms of . Second, the newsvendor step must be done for a demand law that may have atoms, where has no inverse. Without the demand rule the problem is not separable at all: formula (8) alone is unbounded in . Without nonnegativity of demand and quantity it is unbounded in the other direction.
Lean represents all prices, refunds, costs, quantities and profits as real numbers. The valuation law is a probability measure ν on ℝ with integrable identity, so a density is not required. The demand law is a probability measure D on ℝ with D (Set.Iio 0) = 0. is (ν (Set.Ici r)).toReal and is (ν (Set.Iio r)).toReal, following the page's tie rule (keep iff ). is SupplyChainTheory.expSales D q from the published module SupplyChainTheory_contracts, and is 1 - ProbabilityTheory.cdf D. Printed page numbers equal PDF page numbers throughout the source.
Committed conventions and readings:
A trivializing formalization is ruled out: and are the explicit values and , not an argmax chosen by Classical.choose. The maximization ranges over all and all , not a set restricted to . The returned-units cash flow appears in the profit.
The newsvendor step reuses the proved platform theorem SupplyChainTheory.chain_optimal_fractile. The other pieces needed are elementary lemmas on integrals over half-lines and the concavity of . They are reusable for any newsvendor-type model. Proofs of any milestone, and a general-law newsvendor optimality lemma that does not need a continuous , are welcome.
The log-Sobolev constant of a finite Markov chain controls how fast the chain forgets its starting point in relative entropy and in , and it gives sharper mixing-time bounds than the spectral gap when the stationary distribution has very small atoms. Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996)) made this constant a standard tool for finite chains. A practical obstacle runs through their paper: is defined by a nonlinear variational problem, and exact values are known for very few chains. Lower bounds on for a complicated chain are usually obtained by comparison with a simple chain whose constant is known exactly.
The Appendix of that paper computes such a reference value. For the chain that forgets its state in one step, , it determines in closed form for every positive , and with it the log-Sobolev constant of every chain on two points and of the random walk on the complete graph.
Timeline. Rothaus's work on log-Sobolev inequalities (references [38–40] of the paper) studied the constant through its minimizers, the approach the Appendix follows. Diaconis and Saloff-Coste (1996) give the formula , and note that Higuchi and Yoshida independently found the asymmetric two-point value.
Let be a finite set and a Markov kernel on it: and . Let be an invariant probability, , with for every . Functions on are real. Write , , , and .
The Dirichlet form is . The entropy functional is
which is nonnegative and vanishes exactly when is constant. The spectral gap and the log-Sobolev constant are
Equivalently, is the best constant in .
The chain of the mission is : at each step it draws a fresh point from , ignoring its current state. Its invariant measure is , and is its smallest atom. In Lean the objects are dirichlet, entL, gap, logSobolev, indepChain and piMin in the namespace LogSobolevMC.TwoPoint.
For a positive probability on with , the chain has
and in particular, for with , . The goal is an equality, so it contains both a log-Sobolev inequality with this constant and the existence of functions that make it sharp.
Corollary A.3 (every two-point chain), Corollary A.4 ( for every finite chain) and Corollary A.5 (the complete graph, , and on ).
The result. Theorem A.1 is one of the few exact log-Sobolev constants known for a whole family of chains. Since this chain has , the formula shows that can be smaller than by a factor of order , which answers the question on p. 715 of how far and can be apart. Corollary A.4 turns this into a general tool: any spectral gap bound gives a log-Sobolev bound, losing only a factor . Corollary A.3 settles every chain on two points, and Corollary A.5 gives the complete graph, a frequent reference chain for comparison arguments.
Formalizing it. These results are proved in the paper. To our knowledge none of them, nor the log-Sobolev constant of a finite Markov chain itself, has a machine-checked formalization. The mission produces the definitions of , , and for finite chains, and exact values that later comparison arguments can cite.
The upper bound needs only a good test function. The lower bound is the hard part: it is a statement about every function on , and is neither quadratic nor convex. The obvious route, comparing with the spectral gap, loses exactly the logarithmic factor the theorem is about. Reducing to two-valued functions requires the infimum to be attained and analysed through its minimizers. The two-point problem that remains is a one-parameter inequality on an interval. The authors describe its solution as a calculus exercise that depended on numerical guessing, and it has removable singularities at .
is a Fintype with decidable equality. is a Matrix V V ℝ and a function V → ℝ. Stochasticity, invariance, distributions and reversibility are the published MarkovMixing predicates (IsStochastic, IsStationary, IsDist, DetailedBalance) from mm_basic, and is MarkovMixing.distVar from mm_lower. Positivity of is a hypothesis throughout, as in §2.1. The infima and are Lean sInfs over exactly the sets of (2.4) and (3.1). is the bilinear form . is the variational gap, not the eigenvalue-based MarkovMixing.spectralGap, which agrees with it only for reversible chains.
Disclosed additions, all at removable singularities of the printed formulas: in Theorem A.1 (and in its uniform case); the explicit limit value at in Theorem A.2; strict in Corollary A.3; and in Corollary A.5. In (A.3), reversibility, positivity of and are added. Irreducibility is not assumed anywhere.
Trivializing formalizations are ruled out. A closed form evaluated at would be Lean's value , so each such case is excluded or replaced by its limit. Real.log of a nonpositive number and an sInf over an empty or unbounded set do not occur under the stated hypotheses. Dropping the positivity or invariance of , or replacing by the eigenvalue gap, would change the statements. Stating the goal for two points only, or assuming the minimizer is two-valued, would state a step of the proof.
Contributions welcome: the general facts , and the existence of minimizers are reusable for every log-Sobolev development on finite spaces. The two-point calculus of Theorem A.2 is self-contained real analysis.
MarkovMixing definitions used here). https://doi.org/10.1090/mbk/058The Metropolis algorithm turns a simple random walk into a Markov chain with a prescribed stationary distribution, by accepting or rejecting the walk's proposals. It is the basic tool of Markov chain Monte Carlo, and the practical question it raises is quantitative: how many steps are needed before the chain's distribution is close to the target? For most chains used in practice there is no rigorous answer.
Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996) 695–750) developed logarithmic Sobolev inequalities for finite Markov chains as a tool for exactly this question. Their first illustration, stated as Theorem 1.1 in the introduction, is the Metropolis chain for the binomial distribution: a one-dimensional chain for which the spectral gap gives a bound of order steps, while the log-Sobolev constant gives the correct order . This mission formalizes that theorem and the chain of results the paper uses to prove it: the log-Sobolev constant of a product chain, of the hypercube walk, of the Ehrenfest chain, a comparison principle, and a discrete-time convergence bound.
Let be a finite set. A Markov kernel on is a matrix with and ; , written , is the law of the chain after steps from . A probability on is invariant if ; throughout, charges every point. is reversible if .
For real functions on write , , and . The Dirichlet form is , and
The spectral gap and the log-Sobolev constant are
For reversible , is the smallest eigenvalue of . The total variation distance is .
The chain of the goal lives on , , with the binomial distribution . The base chain is the nearest-neighbour walk for , holding with probability at and at . The Metropolis chain accepts a proposed move with probability , so for , and . Explicitly, for and above, symmetrically for ; this is the kernel (1.9) of the paper.
Two auxiliary chains appear in the proof: the hypercube walk on , which flips a uniformly chosen coordinate, and the Ehrenfest chain , on , which records the number of coordinates equal to .
For every , every starting point , every and every integer ,
The goal is stated about the explicit chain (1.9) only; it fixes the constants as printed.
The theorem shows that the Metropolis chain for the binomial distribution mixes in steps, matching the lower bound of order quoted in the paper's converse. The spectral gap together with only yields order ; the improvement comes from replacing by , which is what the log-Sobolev constant buys. The intermediate results are reusable on their own: the tensorization of and (Lemma 3.2), the comparison principle (Lemma 3.3) and the discrete-time bound (Corollary 3.8) apply to any finite chain, and the exact log-Sobolev constants of the two-point chain, the hypercube and the Ehrenfest chain are standard inputs elsewhere.
All results are proved in the paper (the gap of the Ehrenfest chain is quoted there as known). To our knowledge none of them is machine-checked: there is no log-Sobolev constant of a Markov chain in Mathlib or on the platform. The work is to formalize the known proofs.
The natural first idea is to bound the distance to stationarity by the spectral gap: . With as small as and , this needs of order , so no amount of care with this argument reaches the theorem. The proof instead goes through the log-Sobolev constant, which is hard to compute even for simple chains: the paper obtains only through a sequence of exact computations (two points, products, a projection) followed by a comparison. Each step involves the nonlinear functional , whose tensorization and behaviour under comparison of measures are less elementary than those of the variance. The passage from continuous to discrete time also needs control of , since a chain with eigenvalue near does not converge.
The state space is Fin (n + 1), is Fin 2 (, ), and is Fin n → Fin 2. Kernels are real matrices Matrix V V ℝ; stochasticity, invariance, irreducibility, reversibility (detailed balance), total variation, the rows , the product chain (2.9) and the generic Metropolis rule are the published MarkovMixing definitions (mm_basic, mm_mixing, mm_continuous, mm_mcmc). Functions are real valued. Time is a natural number and thresholds are compared in .
, and are defined variationally as real infima (sInf). is the minimum of the Rayleigh quotient , which is the smallest eigenvalue for reversible chains. The eigenvalue-based MarkovMixing.spectralGap is not used, since it equals only for reversible chains. Two hypotheses are added where Lean's conventions would otherwise falsify a statement: Lemma 3.2 assumes every factor has at least two points (Lean evaluates the infimum over an empty set as , the paper as ), and Corollary 3.8 assumes (Lean evaluates as , the paper as ). Lemmas 3.1 and 3.3 are stated without the section's irreducibility assumption, which they do not need.
A trivializing formalization is ruled out: the goal mentions only the explicit chain , the binomial distribution, and total variation, not a chain assumed to have ; positivity and invariance of are never dropped; and no statement relies on a junk value of sInf, Real.log or division. The converse half of Theorem 1.1, for , is asymptotic and proved in the paper only by citation; it is not part of the mission. The second statement of Corollary 3.8 (the uniform bound on ) is also left out.
A complete development needs the semigroup and the hypercontractivity theorem of the paper (Theorem 3.5) on the way to Corollary 3.8, a spectral decomposition of reversible kernels, and the entropy inequalities behind Lemmas 3.2 and 3.3. The general results (Lemmas 3.1–3.3, Corollary 3.8) are reusable beyond this mission. Contributions to any milestone, and alternative routes to the goal, are welcome.
MarkovMixing definitions). https://doi.org/10.1090/mbk/058Biometric readings, typed passphrases and physical measurements are secrets that are never reproduced exactly: a second reading of the same fingerprint differs from the enrolled reading in a few positions. Dodis, Ostrovsky, Reyzin and Smith (arXiv:cs/0602007, SIAM J. Comput. 38(1), 2008) introduced the secure sketch, public helper data that lets anyone holding a nearby recover while leaking as little as possible about , and the fuzzy extractor, which in addition turns into a nearly uniform key. Their constructions for the Hamming, set-difference and edit metrics are the standard reference for this primitive in cryptography.
A construction is judged by its entropy loss: how much min-entropy of the secret the published sketch destroys. To call a construction optimal one needs a lower bound on that loss which holds for every sketch, whatever its algorithm. Appendix C of the paper supplies such a bound from coding theory. It shows that, for uniformly distributed inputs, the code-offset sketch for the Hamming metric and the set-difference sketches lose no more entropy than any sketch must. This mission formalizes that bound, Lemma C.1.
A metric space is a finite set with an integer-valued distance ; the paper also requires exactly when , symmetry, and the triangle inequality (§2.1, p. 7). Random variables are identified with their laws; logarithms are base 2.
The min-entropy of a random variable is . For a pair the average min-entropy is
the negative logarithm of the probability that an adversary who sees guesses .
An -secure sketch (Definition 3, p. 11) is a pair of randomized procedures: maps to a string , and maps back to . Correctness: if then . Security: for every distribution on with , one has .
An -code (§2.2, p. 8) is a set of points such that every ball around a point contains at most one codeword. For , is the largest for which an -code lies inside , and . Finally (Appendix C, p. 40)
the worst case, over all sets of points, of the largest -error-correcting code inside .
In the Lean development these are minEntropy, avgMinEntropy, IsSecureSketch, IsCode, K dis t S and L dis t N hN, in the namespace FuzzyExtractors.LowerBound.
If is an -secure sketch and is a natural number with , then
The bound fixes no particular metric and no particular sketch; it is stated for every finite integer-valued metric and every sketch, with an arbitrary type of sketch values.
The proof in Appendix C has three steps, each a milestone. For uniform on a set of points:
A fourth milestone is the lemma's second sentence: when ,
The result. Lemma C.1 converts any secure sketch into a code: the residual entropy of the sketch can be no larger than the logarithm of the best -error-correcting code inside a worst-case set of points. For uniform inputs it says , so the entropy loss is at least . The code-offset construction built from an optimal code attains that loss, which is how the paper certifies its Hamming and set-difference constructions as optimal for uniform passwords. The companion Lemma C.2 gives the analogous bound for fuzzy extractors, up to a term. Lower bounds of this shape are what separate an efficient construction from a provably best one.
Formalizing it. The lemma has a complete, short proof in the paper; it has no machine-checked proof that we know of. The mission produces a checked version of the bound for arbitrary finite integer metrics and arbitrary randomized sketches, together with reusable definitions of min-entropy and average min-entropy on probability mass functions, of secure sketches, and of -error-correcting codes in a general finite metric space.
The combinatorial core, that the preimage set of one sketch value is a code, is immediate from correctness. The work lies in the probabilistic bookkeeping. One must pass from an average bound on guessing probability to a single good sketch value, which requires handling sketch values of probability zero and an infinite (possibly uncountable) space of sketch outputs. One must then pass from " for all " to "at least points carry positive probability", and compute the min-entropy of a uniform distribution exactly. Finally the bound must be transferred to the minimum over all sets of size , a finite but large family. A first idea, to reason only about deterministic sketches, does not suffice: Definition 3 allows randomized and , and the statement quantifies over them.
Laws are Mathlib PMFs; randomized procedures are maps into PMF. The sketch value type V is arbitrary, standing in for . Average min-entropy is written in the equivalent joint form , which avoids conditioning on null events. "Min-entropy " is read as , and are real numbers. is randomized and correctness asks that it return with probability one for every possible sketch value of .
The explicit choices:
Two trivializing formalizations are ruled out: is the largest size of a code in , not a count of codes; and a code is defined by the ball condition, not by "distinct codewords are at distance greater than ", which is weaker in the absence of the triangle inequality.
Needed infrastructure: the min-entropy of a uniform PMF on a finset, the averaging argument over a tsum of ENNReal values, and monotonicity of Finset.inf'. The min-entropy and code definitions are reusable by every other mission of this paper. Contributions are welcome on any milestone, in any order.
Linear programming algorithms often compute a solution to an auxiliary problem before extracting a solution to the original primal and dual pair. For a homogeneous self-dual formulation, the extraction requires a positive scaling coordinate. If that coordinate vanishes, the same auxiliary solution may instead describe infeasibility or unboundedness. Ye, Todd, and Mizuno introduced a homogeneous self-dual linear program that can start from arbitrary positive primal and dual slack vectors, even when the original programs have no known feasible point (Ye–Todd–Mizuno 1994).
Their Theorem 3 concerns strictly self-complementary optimal solutions of the auxiliary program. Theorem 9 addresses a different question: under a regularity assumption on the original programs, does a general optimal solution of the auxiliary program still have a positive scaling coordinate? The distinction matters because optimality alone does not require every complementary pair to have a positive member. This mission formalizes the statement of Theorem 9 and the numbered identities that frame it.
Fix a real matrix , a right-hand side , and a cost vector . The primal linear program (LP) minimizes subject to and . Its dual (LD) maximizes subject to ; is unrestricted. The dual slack is .
An interior feasible point of (LP) is an with and every . An interior feasible point of (LD) is a with every component of positive. “Interior” here is the paper's strict coordinatewise feasibility condition, not the topological interior of an equality-constrained set in ambient space. The existence of such a point implies ordinary feasibility for the corresponding program.
The paper builds an auxiliary program (HLP) from initial vectors , , and . It uses the derived data
A point is a tuple with and free . Its equality constraints are
The objective is to minimize . A feasible point is optimal when no feasible point has a smaller objective. The paper calls an optimal point self-complementary, whether or not its complementary pairs satisfy strict inequalities (p. 57, after Theorem 2(v)). After introducing the general construction, the paper fixes and , the all-ones vector. That is the instance used in Theorem 9.
If both (LP) and (LD) have interior feasible points, then every self-complementary solution of this fixed (HLP) satisfies
The theorem quantifies over every optimal point, including those that are not strictly self-complementary. The printed tuple writes ; Theorem 2(iv) entails that fact from optimality, so it is not an extra hypothesis in the goal (Theorem 9, p. 64).
Theorem 2(iv) states that (HLP) has zero optimal value and, for every feasible point under arbitrary positive initial , satisfies
Corollary 4 states that a positive at an optimum under the fixed initialization entails infeasibility of (LP) or (LD). Equation (9) states the corresponding normalization identity
These are separate milestone statements, each tied to its index and page in the paper (Theorem 2(iv), p. 57; equation (9), p. 58; Corollary 4, p. 59).
Theorem 9 says that the auxiliary model does not lose its positive scale at any optimum when the primal and dual programs are both strictly feasible. With , the homogeneous primal and dual variables can be divided by to recover solutions in the original scale. The result applies even when the auxiliary optimum lacks strict complementarity; that is the additional coverage beyond the strictly self-complementary case of Theorem 3 (Ye–Todd–Mizuno 1994, pp. 58 and 64).
The mathematical result was proved in 1994. This mission's remaining work is a machine-checked proof of the stated regularity result and its supporting claims in the paper's specific (HLP) model. The definitions of the homogeneous feasible set, its slacks, and its optimality relation are reusable for the other results in the same paper. The full algorithm and complexity estimate belong to the other missions in this series.
The optimality condition controls the objective, and Theorem 2(iv) identifies that objective with a sum of complementarity terms. Those facts alone permit ; they do not force the scaling coordinate to be positive. Theorem 3's assertion for a strictly self-complementary point cannot be applied to an arbitrary optimal point, because its strict support condition may fail. The challenge is to use interior feasibility of both original programs to exclude all zero-scale optima while retaining the full set of HLP optima in the quantifier.
The Lean model uses finite-dimensional real vectors indexed by Fin m and Fin n, a real matrix , and a six-field HLP point in the paper's order . The standard-form primal and dual feasible sets are reused from a published LP definition with the same minimization and maximization orientation. Paper-specific interior predicates and the homogeneous program are defined locally. Slack fields in an HLP point are constrained to equal their formulas, so they cannot be chosen independently to make a statement true.
The model first defines (HLP) for general and then substitutes the paper's choice (7). It treats self-complementarity as objective minimization over the whole feasible set. Defining it by or by a complementarity equation would erase the content of Theorem 2(iv). The objective and normalization constants are exact, including the in the fixed instance. No real supremum or infimum is used to define optimality; it is a direct comparison against every feasible point.
The dimensions may be zero. Empty coordinatewise inequalities then have their usual vacuous meaning, but the equations remain in force. In particular the prescribed point is strictly feasible for every , as a separate sorry-free local verification checks. This excludes an empty-feasible-set reading of the HLP definitions. Contributions proving the three numbered milestones, the goal, or reusable finite-dimensional LP lemmas are within scope.
A semidefinite program minimizes a linear objective subject to a matrix being positive semidefinite. It includes linear programs and many matrix optimization problems, while allowing constraints on eigenvalues that ordinary coordinate inequalities cannot express. Vandenberghe and Boyd’s 1996 survey helped establish this form as a common language for control, combinatorial optimization, and numerical optimization. A useful dual certificate turns a feasible matrix into a lower bound on every feasible primal objective value. The question here is when that bound reaches the primal optimum and when optimizers exist.
The survey states the weak-duality identity on p. 64 and Theorem 3.1 across pp. 64–65. The theorem is a classical result, not an open conjecture. The paper points to Nesterov and Nemirovskii’s account of convex optimization and Rockafellar’s convex analysis for proofs. The published survey also gives a small feasible example with unequal optimal values, showing that some regularity condition is genuinely needed.
Let be natural numbers. The data are a vector and symmetric matrices . For a decision vector , define the affine matrix map
A symmetric matrix is positive semidefinite, written , when for every vector . It is positive definite, written , when this inequality is strict for every nonzero vector. The primal problem minimizes over vectors with . A vector satisfying this constraint is primal feasible. The dual problem maximizes over symmetric matrices satisfying for each . A matrix satisfying these conditions is dual feasible.
Write for the infimum of primal objective values and for the supremum of dual objective values. These are extended-real optimal values: an infeasible primal has , and an infeasible dual has . An unbounded objective can give the other infinite value. The optimal sets and contain feasible points whose objective value equals and , respectively. Equality of optimal values alone need not put a point in either set.
The entry points are the trace identity and weak duality from p. 64 of the survey. For any primal feasible and dual feasible ,
The goal, Theorem 3.1, adds strict feasibility. The primal is strictly feasible if some has . The dual is strictly feasible if some dual feasible has . With either condition, and without a finiteness assumption on the optimal values,
If both conditions hold, the theorem also asserts
The milestone list includes the paper’s positive-semidefinite trace fact, equations (30) and (31), weak duality of values, the finite-value primal strict-feasibility case already proved on the platform, and the complementary-slackness statements on p. 65. The listed finite case is a qualified part of Theorem 3.1; the goal retains its full extended-real statement.
An optimal dual matrix certifies a lower bound for the primal objective; when the values agree, it can certify optimality. Theorem 3.1 specifies a sufficient condition for that certificate to reach the exact value. Its last clause also ensures that both sides can supply actual optimizers when both strict-feasibility conditions hold. Complementary slackness then states that their positive semidefinite matrices have zero product. These statements connect the numerical practice of primal-dual semidefinite programming to the exact optimization problem in the survey.
The theorem is mathematically proved in the literature but is not yet formalized in full here. A published Prove2Me theorem proves a finite-value primal strict-feasibility case and dual attainment for a sign-reversed inequality convention; another proves self-duality of the positive-semidefinite cone. The remaining work includes the dual strict-feasibility case, infinite optimal values, the two-set attainment clause, and an audited bridge between the survey’s exact definitions and existing results. The definitions and weak-duality statements are reusable for other semidefinite programs whose constraints have the same affine matrix form.
Weak duality gives only . It does not produce a dual feasible matrix with objective approaching the primal optimum, and it does not show that either infimum or supremum is attained. The example on p. 65 has feasible primal and dual problems but and . Thus mere feasibility cannot replace positive definiteness in Theorem 3.1. Even equality of values by itself would leave the theorem’s existence claim unaddressed. The challenge is to cover both asymmetric strict-feasibility conditions and both optimizer sets while preserving the cases where an optimal value is infinite.
Lean represents by Fin m → ℝ and matrices by Matrix (Fin n) (Fin n) ℝ. The paper’s coefficients are stored as a zero-indexed family; is a separate argument. Symmetric real matrices use IsHermitian. Mathlib’s PosSemidef and PosDef encode the matrix order and include symmetry. Dual equalities use ; cyclicity of trace identifies this with the paper’s . The objective uses the finite dot product.
Both optimal values use EReal, with an infimum or supremum over the image of the feasible set. This preserves the empty-set and unbounded-value conventions; a real-valued infimum or an infimum over all vectors would change the theorem. The goal states symmetric data explicitly, strict feasibility as positive definiteness, and both nonempty optimal sets under the conjunction of the two strict-feasibility conditions. It makes no linear-independence assumption on : the paragraph on p. 63 uses that assumption only to reparameterize the dual. The natural-number dimensions include zero; the formal statements retain the same meanings in those edge cases. The survey’s printed “dual semidefinite program (1)” on p. 64 means dual problem (27), as identified by its displayed constraints and objective.
A complete development needs matrix trace algebra, positive-semidefinite matrix theory, extended-real order and suprema, and a suitable separation or convex-duality result. Contributions to the weak-duality and complementary-slackness lemmas, to the dual strict-feasibility case, and to the extended-real boundary cases are all useful. The local definitions of the primal and dual feasible sets, values, and optimal sets are intended as reusable interfaces.
The multiarmed bandit problem asks how a gambler should allocate successive plays among independent projects, each of which changes state only when it is played, so as to maximize the expected total-discounted reward. Gittins and Jones (1974) showed that it is optimal to play, at every epoch, a project of greatest Gittins index, a number computed from that project alone. The result underlies job scheduling on a single machine, sequential clinical trials and many stochastic resource-allocation models.
Weber (1992) gave a short proof of the index theorem through prevailing charges, and used the same idea to prove a result that was new: the optimal value is a submodular function of the set of projects that are available. Submodularity of the value says that the marginal worth of an extra project shrinks as more projects are on hand. Two consequences appear in the paper: for statistically identical projects started in a common state, the optimal value is concave in their number; and a bound of Tsitsiklis (1986) for a problem with a retirement option is a special case.
Timeline. Gittins and Jones (1974): the index theorem, by an interchange argument (book-length treatment in Gittins (1989)). Whittle (1980): a proof through a retirement option. Varaiya, Walrand and Buyukkoc (1985): the interchange argument in a general setting. Tsitsiklis (1986): a short proof of the index theorem, including the bound for a retirement bandit. Weber (1992): the prevailing-charge proof and the submodularity of the value (Theorem 4).
There are bandits . Bandit is a Markov chain on a state space with transition kernel ; at each epoch the gambler plays one bandit , receives the reward , the played bandit moves one step of its chain and the others stay where they are. Rewards are nonnegative and uniformly bounded, and is the discount factor. The initial states are fixed. A policy chooses from the history; its value is .
For a set of bandits , the restricted problem is the same game played with the bandits of only, each started in its state in , and
The fair charge of a state is the largest ratio of expected discounted reward to expected discounted time over stopping times of a single bandit started at (Weber's (4)). On a fixed realisation, where bandit passes through states on its successive plays, the prevailing charge after plays is , a nonincreasing sequence. is the sum of the first terms of the interleaving of the sequences , , into nonincreasing order.
This holds for arbitrary bandits (no identical-bandit hypothesis) under the standing assumptions of the paper's Section 1.
the expectation over independent realisations of the bandits' state sequences.
Submodularity of the value is a structural fact about the bandit problem that the index theorem alone does not give: the index theorem identifies an optimal policy for a fixed set of projects, while (9) compares optimal values across sets. It yields diminishing returns from adding projects, the concavity of the value in the number of identical projects, and Tsitsiklis's retirement bound, which separates one project from the rest. Bounds of this kind are used when choosing which projects to make available before allocation begins.
Theorem 1 of the paper, the optimality of the Gittins index policy, is already on Prove2Me as BanditAlgorithm.gittins_index_theorem (Proved, Shuze Chen), together with the discounted Markov bandit model and the Gittins index (GittinsIndex, Shuze Chen) and a finite-horizon form of the prevailing-charge coupling (BanditAlgorithm.gittins_finite_prevailing_charge_eq_stack_coupling_value, Harry_Xu). This mission builds on those items. Theorem 4, inequality (10) and the infinite-horizon representation of have no machine-checked proof that we know of. The other two missions of this series formalize Weber's Theorem 2 (mission 1, a suboptimality bound by prevailing charges) and Theorem 3 (mission 2, a suboptimality bound by index gaps); this mission does not depend on them.
Inequality (10) concerns sums of largest terms of merged sequences; it fails without nonnegativity when and are disjoint, and a proof must use both the monotonicity of each sequence and the sign of the terms. The representation of requires the fair-game property of prevailing charges in infinite horizon: that the optimal policy of collects in expectation exactly the discounted charges it pays, and that, on a common probability space of independent bandit trajectories, the charges paid by the optimal policy are the nonincreasing interleaving. The finite-horizon coupling is on the platform; passing to infinite horizon, identifying the interleaving with the play of an index policy, and handling ties and measurability are the remaining work. Finally, (10) is an undiscounted, pathwise statement while (9) compares discounted expectations, so the two must be connected through series of increments of and an exchange of expectation and series.
The model is the published BanditAlgorithm discounted Markov bandit: one standard Borel state space , one kernel and one measurable reward shared by all bandits; bandits with different dynamics are encoded by a disjoint union of state spaces. is the mean reward. The value of a policy is the series of per-round expected rewards (markovBanditDiscountedValue), equal to the expectation of the discounted sum for bounded rewards. The fair charge is the published gittinsIndex.
Explicit readings of the paper's phrases:
restrictedValue), with set explicitly;Measure.pi (fun j => markovChainMeasure P (x j));partialInterleavedSum, the maximum over allocations of plays of the sum of initial segments, equal to the interleaving sum for nonincreasing sequences, with ; the sequences start at (the printed is a misprint);StandardBorelSpace S and Measurable r;Trivializing formalizations are ruled out: and are defined as rather than obtained from a supremum over an empty type, the supremum defining is over a nonempty family bounded by , is a maximum over a finite nonempty set, and the hypotheses are satisfiable (checked on a one-bandit instance).
A complete development needs: the infinite-horizon prevailing-charge identity for index policies, measurability of the charge stacks (the measurability of gittinsIndex is on the platform), and a combinatorial lemma on merges of nonincreasing sequences. Inequality (10) and the merge lemmas are reusable beyond bandits, for sums of largest elements and weighted rank functions of uniform matroids.
In the on-line prediction model studied by Littlestone and Warmuth (Inform. and Comput. 108, 1994), a learner receives instances one at a time, predicts a binary label for each, and is then told the correct label. No probabilistic assumption is made: performance is measured by the number of mistakes on a worst-case sequence. When every label is given by some function of a known target class , the best attainable worst-case number of mistakes is a combinatorial invariant of , characterized by Littlestone (Mach. Learn. 2, 1988) through mistake trees, now called the Littlestone dimension.
Real data are rarely labelled exactly by a member of the class. Littlestone and Warmuth measure the departure by the number of anomalies: the number of trials inconsistent with the best function in the class. Their Weighted Majority algorithm makes a number of mistakes that grows linearly in the number of anomalies, and the rate of growth can be pushed towards mistakes per anomaly by the choice of the update factor . Theorem 8.1 of the paper shows that no deterministic learner does better: rate is forced for every class with at least two members. This mission formalizes that lower bound.
Let be an arbitrary set (the domain) and a set of functions , possibly infinite. A trial is a pair , and a sequence of trials is finite; an instance may occur several times with different labels.
A complete -mistake tree for is a complete binary tree of height whose internal nodes carry instances of such that every labelling of a root-to-leaf path is realized by some ; in Lean this is the predicate ShattersTree F k v.
For every class with and every ,
The constant is the paper's, and the statement holds for infinite classes, including those with .
UnderstandingML.soa_mistake_bound (), referenced together with UnderstandingML.ldim_le_mistake_bound; together they identify with the Littlestone dimension.The theorem settles the optimal rate at which mistakes must grow with the number of anomalies for deterministic learners: per anomaly, uniformly over all non-trivial classes. Together with the upper bounds of §2 of the paper, it shows that the deterministic Weighted Majority algorithm is within an arbitrarily small factor of optimal in its dependence on the anomalies, and it explains the factor of that separates deterministic from randomized prediction (Theorem 8.2, a separate mission of this series, gives rate for randomized learners).
The result is proved in the paper; to the best of a search of the platform it has not been formalized. The mission produces a machine-checked lower bound in a general setting: arbitrary domain, arbitrary (possibly infinite) class, extended-natural-valued optimal bounds. The noise-free side, the Littlestone dimension and the Standard Optimal Algorithm, is already published on the platform from Shalev-Shwartz and Ben-David's textbook, and this mission connects it to the noisy setting.
The obvious argument forces one mistake per trial and stops: an adversary that always contradicts the learner leaves no function of with few anomalies once the trials outnumber the mistake tree. The difficulty is to spend the anomaly budget so that each anomaly buys two mistakes while the sequence stays in , and to do so against an arbitrary algorithm, which may behave adversarially itself. The definition of through a minimum over the class (not a fixed target) and the possibility that is infinite both have to be handled.
X; the class is F : Set (X → Bool); the hypothesis is F.Nontrivial, which is meaningful for infinite classes (a cardinality ncard would be there).UnderstandingML_Online (OnlineAlg X Bool, history, mistakes, ShattersTree); an algorithm is an arbitrary function of the history and the current instance, so every deterministic learner is covered.Fin T → X × Bool for every finite length T, with repeated instances and conflicting labels allowed.opt F η : ℕ∞ is an infimum over algorithms of a supremum over sequences in ; is a natural number. Membership in is "some has at most anomalies", which is the paper's minimum over .toNat truncation would give a different statement; neither is used.Needed infrastructure: the identification (sequences with no anomaly are exactly the realizable ones), the existence of a shattered tree of depth from the published Littlestone-dimension results, and the two-stage adversary. Contributions of general lemmas about ShattersTree (subtrees, truncation to smaller depth) are reusable for the randomized mission and beyond.
Link-based ranking of web pages rests on a small number of linear-algebraic facts. Kleinberg's HITS algorithm (Hyperlink-Induced Topic Search), introduced in Kleinberg 1999, assigns each page of a hyperlinked collection two scores: an authority score, high for pages that many good hubs point to, and a hub score, high for pages that point to many good authorities. The scores are computed by a simple alternating iteration, and the paper's justification for using them is a convergence theorem: the iteration settles, and its limits are the principal eigenvectors of two symmetric matrices built from the link structure. HITS, together with PageRank (Brin–Page 1998), founded the study of link analysis, and the eigenvector characterization is what later work on the stability and uniqueness of such rankings starts from (for example Ng–Zheng–Jordan 2001 and Farahat et al. 2006).
This mission formalizes that convergence theorem, §3 of the paper, together with the steps of its proof.
A collection of hyperlinked pages is a directed graph with ; an edge means that page links to page . Its adjacency matrix is the matrix with if and otherwise. Self-links are allowed.
Each page carries an authority weight and a hub weight , collected into vectors . Two operations update them:
Normalizing a vector rescales it so that its squares sum to .
The procedure Iterate starts from . In round it applies to , obtaining ; applies to , obtaining ; and normalizes and to get and . It returns .
For a real symmetric matrix , list its eigenvalues with multiplicity in order of decreasing absolute value, . The paper's standing Assumption (†) is
so that the eigenspace of is a line. A principal eigenvector is a unit vector spanning that line; it is determined up to sign.
Assume (†) for and for . Then there are with
The authority scores converge to the principal eigenvector of the co-citation matrix , and the hub scores to that of the bibliographic coupling matrix .
A companion item states Proposition 6.1 (§6): and have the same characteristic polynomial, and maps each eigenvector of with nonzero eigenvalue to an eigenvector of with the same eigenvalue.
The theorem turns a heuristic, mutually reinforcing update into a well-defined object: the HITS scores of a graph are the principal eigenvectors of and , independent of the number of rounds run, and computable by any eigenvector algorithm. It also locates where the definition is fragile: when (†) fails, the limit depends on the starting vector, which is the starting point of the later stability analyses cited above.
The result has been proved since 1999; its proof in the paper is a short appeal to the power method and to a Perron-type non-negativity fact. What this mission adds is a machine-checked version of the whole chain, from the combinatorial update rules on a directed graph to the spectral characterization, with the hypotheses made explicit. Two generic power-method theorems are already proved on the platform (Trefethen–Bau, Lecture 27) and are included as references; to our knowledge no formalization of HITS, of Assumption (†), or of the non-negativity of principal eigenvectors of non-negative symmetric matrices exists in Mathlib or on the platform.
The obvious argument — "the power method converges" — is only half of the proof. The power method converges from a start vector that has a nonzero component along the dominant eigenvector, and the start vectors here are fixed: for the hubs and for the authorities. Showing that they are not orthogonal to the principal eigenvectors needs a Perron-type fact (the principal eigenvector of a non-negative symmetric matrix can be chosen non-negative), which in turn needs that the dominant eigenvalue is the spectral radius itself and not its negative. For the authorities the start vector is , not , and the argument must also use : when has a zero dominant eigenvalue the iterates are . A second difficulty is the passage from the rescaled power iterates of the referenced platform theorem to the normalized iterates of the algorithm, and from a statement on an abstract inner product space to one about matrices on .
Pages are Fin n; the link relation is a decidable relation E : Fin n → Fin n → Prop; adjMatrix E is the real 0/1 matrix (Mathlib's SimpleGraph.adjMatrix is undirected and loopless and is not used). The operations , are defined as neighbour sums, not as matrix products, so that milestone 1 has content. normalize v divides by the Euclidean norm and sends to ; no statement is true only because of that convention. hitsIter E k is , with the step applied to the unnormalized as on the page. Convergence is in the product topology of .
Assumption (†) is encoded as Dagger M: an eigenvalue with one-dimensional eigenspace, for every other eigenvalue , and . The last clause is the paper's own reading ("as dictated by Assumption (†)", p. 11); without it, the one-page graph with no link satisfies (†) vacuously and Theorem 3.2 fails. Theorems 3.1 and 3.2 assume (†) for both and , as the paper does. "The principal eigenvector" is a predicate, IsPrincipalEigenvector, true of both unit vectors in the principal eigenspace. Added hypotheses, each disclosed in its item: in the power-iteration milestone (the claim fails for ; it costs nothing for the positive semidefinite , ); the closed form is stated for . The non-negativity of is true but not part of Theorem 3.2 and is not asserted.
A formalization in which and are matrix products by definition, or in which Theorem 3.1 alone is the goal (a sequence converging to would satisfy it), is ruled out: the goal pairs convergence with membership of the limit in the principal eigenspace as a unit vector.
Useful infrastructure, reusable beyond this mission: normalized power iteration for real symmetric matrices, and the non-negativity of the principal eigenvector of a non-negative symmetric matrix under a simple dominant eigenvalue. Contributions of either, and of the bridge between Matrix.toLin'-eigenspaces and Matrix.IsHermitian.eigenvalues, are welcome.
When many users share a network and each routes its own traffic selfishly, the outcome is a Nash equilibrium rather than a centrally optimized assignment. Koutsoupias and Papadimitriou, in Worst-case equilibria (STACS 1999; journal version 2009), proposed to measure the loss caused by this lack of coordination by the worst-case ratio between the social cost of an equilibrium and the social optimum. The ratio, first called the coordination ratio and now the price of anarchy, became a central quantity of algorithmic game theory, studied for routing, scheduling, congestion games, auctions and network design.
The paper analyses the simplest setting in which the question is nontrivial: agents sending traffic over parallel links, which is the same as scheduling independent jobs on parallel machines with the jobs choosing their machines. For two identical links it determines the price of anarchy exactly.
Timeline.
There are agents and identical parallel links. Agent has an amount of traffic to send over one link. A pure profile assigns a link to each agent; the load of link is , and the cost of agent is , the traffic on its own link.
A mixed strategy of agent is a probability distribution on the links; the agents randomize independently, so occurs with probability . The cost to agent of a mixed profile is its expected cost . The profile is a Nash equilibrium if no agent can lower its expected cost by changing its own distribution while the others keep theirs.
The expected traffic on link is , and the cost of agent when its traffic is assigned to link is .
The social cost of is the expected maximum load,
and the social optimum is the least maximum load over all pure assignments, the optimum of the -way partition problem for .
The proof of the main theorem uses two further quantities: the contribution probability , the probability that agent is on the (lexicographically first) link of maximum load, and the collision probability of agents and .
For any number of agents with positive traffics and identical links, every Nash equilibrium satisfies
In the order the proof of Theorem 3 uses them:
The second sentence of Theorem 1 (on two links some equilibrium has ), which shows the goal is tight, and the fact from its proof that the uniform profile of unit agents on links is an equilibrium.
Theorem 3 and the instance of Theorem 1 show that on two identical links selfish randomized routing never costs more than above the optimum, whatever the number of agents and their traffics, and that this factor is attained. Theorem 2 gives a per-agent guarantee for any number of links: the expected cost an individual agent experiences at any equilibrium is within of the optimum, the same factor as Graham's list-scheduling bound. Together they separate the individual and the social view: individual costs stay within a constant, while the expected maximum load, the social cost, can be a factor above the optimum.
The results are proved in the paper. As far as is known they have not been machine-checked. Formalizing them produces a verified model of mixed equilibria in load balancing games, with the social cost as an expected maximum over the product distribution, which is the starting point of the later literature on links with speeds, on general congestion games and on smoothness arguments. The intermediate identities (the contribution and collision probabilities) are reusable for any expected-maximum bound over independent random assignments.
The social cost is an expectation of a maximum over outcomes, and the equilibrium probabilities are given only implicitly, as the solution of a linear system determined by the agents' supports. The natural first idea, to bound the expected maximum load by the maximum expected load , fails: the expected maximum can be much larger, and bounding it is exactly what makes the problem hard (for links it grows like the maximum occupancy of balls in bins). Computing the equilibrium probabilities explicitly does not help either; the paper gives them for two links and notes it does not see how to use them to bound the social cost. The argument has to relate the per-agent expected costs, which the equilibrium condition controls, to the expected maximum, which it does not control directly.
Agents are Fin n and links Fin m (the goal uses Fin 2); the paper's agent and link are indices , . A mixed profile is p : Fin n → Fin m → ℝ with p i j . The game is built on the published definitions agt_games (AGT.IsMixedNash, AGT.expectedPayoff, AGT.profileProb). That vocabulary maximizes payoffs, so the payoff of an agent is minus the load of its link, and the expected cost is minus the expected payoff. The equilibrium is the full mixed Nash condition, including that each is a probability distribution; the support description is a milestone, not the definition. The social cost is the expected maximum load over the product distribution, never the maximum expected load. is a minimum over pure assignments, with the number of links an explicit argument. The lexicographically first maximum link is the lowest-indexed link of maximum load.
Traffics are positive, as in the paper's model; some milestones need only nonnegative traffics or no sign condition, and say so. Statements over links assume . Price-of-anarchy statements are inequalities for every equilibrium, never a quotient , whose value at would be a junk . A formalization in which the social cost is , or in which the equilibrium is only a support condition without the requirement that the be distributions, would trivialize or falsify the goal and is ruled out by these definitions.
A complete development needs finite sums over the pure profiles, marginalization of product distributions, and the case analysis of the final step. The marginalization lemmas (summing out the other agents, collision probabilities of independent choices) are reusable beyond this mission. Proofs of the milestones, alternative arguments for Theorem 3, and a proof of Theorem 2 for its own sake are all welcome.
Page numbers are those of the PDF file of the journal version; it prints a page number only on its first page.
Many algorithms for convex bodies need the body to be well rounded: sandwiched between two concentric ellipsoids whose size ratio is controlled by the dimension. The ellipsoid method, volume and integration algorithms, and preconditioning for linear programming use such roundings. For a polytope given by its vertices , John's theorem guarantees an ellipsoid with
the minimum-volume circumscribed (Löwner–John) ellipsoid scaled about its centre; for centrally symmetric sets the factor improves to . The associated D-optimal design problem is a convex optimization problem. Khachiyan (1996) uses this connection to obtain a finite approximation algorithm.
Khachiyan shows that barycentric coordinate descent (BCD) computes a -rounding in arithmetic operations. For fixed dimension and tolerance, this is linear in the number of points; the iteration bound depends on that number only through . Khachiyan (1996)
The paper builds on the Kiefer–Wolfowitz optimality conditions (1960). Later work revisits the method's complexity and variants; see Todd and Yıldırım (2007).
Let and let be the unit simplex of weights , . For write
and let . Maximizing over is the D-optimal design problem (2.3); is its optimal value. A point satisfies the -relaxed optimality conditions (2.10) if for every ; the accuracy is the least such .
The BCD method starts at and repeats
where is an index with largest and is the th vertex of : it moves weight towards the worst-covered point by the exact line-search step.
For a centrally symmetric set () the ellipsoid is the candidate rounding. For a general set the method runs on the lift , and the rounding ellipsoid is the intersection of with the hyperplane , where is the ellipsoid (3.4) of the block matrix with blocks , and , and aggregates the weights of .
There is a universal constant such that for every , every with affine hull , every and every BCD run on , some iterate with
meets the stopping test with and yields an ellipsoid with
the shrinking taken about the centre of .
For centrally symmetric full-dimensional , : within iterations,
Lemma 1 (), existence of a maximizer, the line identity (2.6), the Kiefer–Wolfowitz conditions (2.9), Lemma 2(i)–(ii) (relaxed optimality gives value and rounding guarantees), Lemma 3 (the per-step increase and the gap bound), the three steps (2.25), (2.27) and the halving bound of the proof of Lemma 4, Lemma 4 (the iteration bound), the rank-one update of , Theorem 1, and Lemma 5 (from the lift back to ). Three further items complete §4: Lemma 2(iii), the slicing property (4.1) and Theorem 3 (approximating the Löwner ellipsoid to relative volume accuracy ).
The result gives a rounding of a vertex-described polytope at nearly the cost of reading the input, using only rank-one updates; the same iteration approximates the minimum-volume enclosing ellipsoid, a basic primitive in statistics (D-optimal design, outlier detection), computational geometry (core sets) and convex optimization (initialization of interior-point and ellipsoid methods). The doubly logarithmic dependence on is what makes the method practical for large point sets, and the analysis is the template for the later Frank–Wolfe-type analyses of minimum-volume ellipsoid algorithms.
The results are proved in the paper; none of them has a machine-checked proof. The platform has the Löwner–John ellipsoid itself (existence, uniqueness, John's -rounding) and the concavity of , but no algorithmic statement about it. This mission produces a verified iteration bound for a concrete method, together with the D-optimal design identities (Lemma 1, (2.6), (2.9)) and the rank-one update, which are reusable for any later formalization of optimal design or of Frank–Wolfe methods on the simplex.
The accuracy need not decrease at every step, so a bound based on per-step improvement in fails. The determinant objective and the geometric rounding condition are different quantities: controlling one must be shown to control the other, including the inner inclusion of the ellipsoid. For a general set, the lift changes the dimension and the relevant ellipsoid is a slice at ; the inner inclusion for this slice needs a separate geometric justification.
Points are vectors Fin n → ℝ; is the range of a family a : Fin m → Fin n → ℝ (repetitions allowed). The definitions take any finite index, so they apply both to and to the lift, indexed by Fin m ⊕ Fin m. is Mathlib's stdSimplex. uses Real.log, which returns rather than on singular matrices, so every comparison of values of is restricted to and is the supremum over . Ellipsoids are the published LinearOptimization.ellipsoid; scaled ellipsoids about the origin use the pointwise scalar multiple, and shrinking a non-centred ellipsoid is the homothety about its centre.
Standing assumptions are hypotheses: in §2, central symmetry (2.1), full dimension (2.2) and (p. 309); in §3, full dimension (3.1) and . Items that do not need them drop them. The BCD run is a predicate on sequences that allows any maximizing index at every step, with no tolerance parameter; the tolerance enters only through the stopping test.
Each is a universal constant quantified before the dimension, the points, and the run. The paper counts arithmetic operations; the formal statements bound the index of an iterate meeting the stopping test, and the cost per iteration and the initialization are not formalized. The goal's bound is stated in the lifted parameters , which agrees with the page's up to the constant and stays positive at .
The goal assumes nothing about the run beyond its definition: the stopping test, the positive definiteness of , the rounding inclusions and the iteration bound are all conclusions. A statement in which the constant may depend on the instance, or in which a shrunken ellipsoid is scaled about the origin, would be a different, trivial or false, theorem.
Contributions welcome: the determinant and inverse identities ((2.6), Lemma 1, the rank-one update) are self-contained linear algebra; Lemma 2 needs the KKT characterisation of the minimum-volume ellipsoid; Lemma 5 is finite-dimensional convex geometry.
A seller with one limited inventory pool can choose which fare products to show in each selling period. When customers choose among the displayed products, showing another fare can both add sales and divert buyers from a more expensive fare. A fixed ranking of fares therefore does not by itself tell the seller which products to offer. Talluri and van Ryzin's working paper studies the optimal offer decision under a general discrete choice model, without specifying a logit or independent-demand formula for customer choice (working paper, 2001, pp. 5–8; published article, 2004). The present mission concerns the paper's first main result: how to reduce the collection of possible offer sets and how the best choice changes with inventory and time.
There are fare products, indexed by . Product earns a nonnegative revenue . In each period, a customer arrives with probability , independent of the remaining time. The seller offers a set . Conditional on arrival, the customer buys product with probability or buys nothing with the remaining probability. Thus and . The purchase probability is , while the expected revenue conditional on arrival is . The empty set is a possible offer; it has .
Time is counted backward: is the number of periods still available, and is the number of inventory units left. Let be the maximum expected revenue from that state, with . For , the marginal value of capacity is . The Bellman equation is
The paper calls a set dominated if a randomization over offer sets achieves either strictly more expected revenue with no greater purchase probability, or no less expected revenue with strictly lower purchase probability. A set is nondominated if neither comparison applies. This two-clause definition is specific to the paper. It differs from the one-clause “efficient set” used for a related model in Talluri and van Ryzin's book; the published formalization of that book's optimal policy theorem is therefore related work rather than a replacement for this goal.
Proposition 1 characterizes the nondominated sets by a positive tradeoff value : a set lies on the relevant frontier exactly when it maximizes for some . Proposition 2 says that dominated sets can be excluded from the Bellman maximization when , and that a nondominated optimum exists when the marginal value is zero. Proposition 3 orders the nondominated sets so that both and are nondecreasing (working paper, pp. 8–12).
Among indices maximizing , let be the greatest one when there are ties. Lemmas 1 and 2 say that is nonincreasing in . The paper's Lemmas 3 and 4 say that marginal capacity values decrease as inventory increases and increase as the number of remaining periods increases. For the admissible states , the goal is Theorem 1:
where is an optimal offer, and the greatest optimal index is nondecreasing in and nonincreasing in (working paper, pp. 12–15, Theorem 1). These are claims about the index in the nondominated ordering; the offer sets themselves need not be nested by inclusion.
Theorem 1 replaces a search over all offer sets at each state with a search over the nondominated sets. It also tells an operator how the preferred position in that ordered list changes as seats are sold or as the selling horizon shortens. The later sections of the paper add conditions under which this ordering corresponds to fare-order nesting; those conditions are treated in separate missions (working paper, §3).
The model's value recursion and the marginal-value inequalities already have published Prove2Me formalizations in the Talluri–van Ryzin book setting. The book's marginal-value theorem is proved and serves here as a referenced milestone after reindexing its forward time convention. The paper's two-clause dominance concept, its ordered frontier, and Theorem 1 itself remain the formalization work of this mission. Keeping those distinctions explicit makes the resulting definitions reusable for other choice models with the same purchase and revenue coordinates.
A set with high expected revenue need not be attractive when capacity is scarce: it may also consume inventory more often. Ranking sets by revenue alone therefore fails. Conversely, an offer set can tie another at a single marginal value, so selecting an arbitrary maximizer does not give a monotone index across states. The paper resolves ties by taking the greatest optimal index. Formalization must also retain the full randomized dominance relation: using only strict revenue improvement would leave sets on the wrong frontier. These issues arise even with finitely many products and without a specialized formula for .
Products are Fin n, and offers are finite subsets of them. The published RevenueManagement_singleResource definition supplies the choice-model predicate, , , and the backward value recursion. This mission defines the paper's own dominance relation, stage objective, exhaustive ordered list of nondominated sets, and greatest-maximizer predicate. Every possible offer set, including the empty set, participates in the Bellman maximum. The list must contain all nondominated sets exactly once; otherwise choosing from it would weaken Theorem 1.
The assumptions and are the model's arrival-probability and nonnegative-fare conventions. The paper indexes fares in decreasing order, but Section 2's claims do not use that order, so the Lean targets omit it. Proposition 2's assertion that a dominated set is never optimal requires ; that condition is placed on that clause alone. Decisions and marginal values are stated for . The paper prints Lemma 3 also at , where its right side is undefined; the referenced formalization states the meaningful range . The imported book theorem uses forward time, reindexed here as the number of periods remaining. The goal does not assume the dominance reduction or the marginal-value monotonicities that its milestones supply.
A complete development uses finite sums and maxima, the choice-value recursion, a finite frontier argument for Proposition 1, and order properties of the stage objective. The dominance and ordered-frontier definitions can support later results on nested policies. Contributions that establish the stated milestones under the same conventions are within scope.
A cutting-stock shop receives orders for pieces of several lengths and cuts them from a limited menu of longer stock lengths. Each stock length has a cost. The shop can repeat any cutting pattern, so the central optimization question is which patterns meet the demand at least cost. The direct linear program has a variable for every possible pattern. Even a modest menu of piece lengths can yield too many columns to list before optimization begins. Gilmore and Gomory's 1961 article addresses this large-column obstacle by testing whether an as-yet-unlisted pattern could lower the cost of a current basic solution.
The article studies the linear programming relaxation: cutting activities may have nonnegative real weights rather than integer repetition counts. It does not claim that the resulting fractional optimum is always an integer cutting plan. Its worked example happens to have an integer optimum of cost 170; the authors explicitly note that this integrality is fortuitous (Gilmore and Gomory 1961, p. 858). The target here is the exact stopping condition for the relaxation.
An instance has ordered piece lengths , demand for each piece length, and stock lengths with real costs . A cutting pattern for stock is a vector of nonnegative integer counts with . An activity consists of that stock choice and its fitting pattern. Its demand column is and its cost is . A surplus column for demand row has coefficient in that row, zero elsewhere, and zero cost. The paper uses such columns to turn its demand inequalities into equations (Gilmore and Gomory 1961, p. 850, (1)–(3)).
A feasible solution assigns nonnegative real weights to finitely many activities and surplus columns so that activity output minus surplus equals in every row. Its cost is the weighted sum of stock costs. A basis lists columns with invertible coefficient matrix and cost row . The associated bordered matrix, demand column, tableau column, and multipliers are
A feasible basis has nonnegative basic values, the last entries of . Those values on the basic columns, with zero on every other column, form the current basic solution. The first entry of is its cost. These definitions follow the matrix and tableau of routine steps (2)–(4) (Gilmore and Gomory 1961, pp. 854–855).
The goal is the stopping statement of step (4). If no nonbasic surplus column has a negative multiplier, and no available stock has a fitting pattern satisfying , then the current solution is feasible and minimizes cost across all feasible activity and surplus assignments:
The six milestones record the paper's ingredients: the first row of and the meaning of ; the entering-column price test (4)–(5); the surplus-column test of step (3); the integer-pattern form (6)–(7); the maximum-pattern test; and the dynamic programming recurrence for (Gilmore and Gomory 1961, pp. 852–855). The paper has no numbered theorems or lemmas; each milestone is drawn from a sentence or display on those pages.
The result makes a finite tableau a certificate for an optimization problem whose set of potential cutting activities is much larger than the current basis. A failed pricing search is meaningful only when it covers every fitting pattern for every stock length; the goal makes that full scope explicit. In the example, the final multipliers are and the relevant knapsack maxima for stock lengths , , and are , , and , matching their stopping prices and the cost 170 (Gilmore and Gomory 1961, p. 858).
The mathematical argument is known from the 1961 article. This mission asks for a machine-checked Lean proof of its particular cutting-stock formulation, including the bounded-pattern search, bordered tableau, surplus columns, and global optimality conclusion. The proposal statements compile with proof placeholders; they are not already proved by those placeholders. Published general LP results are listed as references, but their finite-indexed formulations do not directly state the cutting-stock theorem.
Checking only the columns already in a tableau cannot establish optimality: an unlisted pattern might still fit a stock length and have a price greater than its cost. The article reduces this large search to an integer knapsack maximum for each stock length (Gilmore and Gomory 1961, pp. 852–853). Formalization must retain the distinction between a basis of columns and the full collection of possible columns. Strict improvement also needs care at a degenerate basic solution. The paper directs zero-ratio pivots to a separate degeneracy procedure (Gilmore and Gomory 1961, p. 855); the sufficient directions of the pricing milestones therefore require positive basic values, while the goal's optimality direction does not.
Lean indexes piece types from zero and uses a separate initial cost coordinate followed by the demand coordinates for . Thus the paper's st bordered row corresponds to Lean demand index . Patterns are vectors in ; the zero pattern is included. A solution is a finitely supported real weighting of all activity and surplus columns. Global minimality quantifies over every such feasible weighting, including activities not in the current basis. No sign condition is imposed on stock costs or stock lengths in the goal; the goal is a conditional optimality statement and remains valid whenever its hypotheses hold.
The knapsack value uses extended real numbers, giving when no pattern fits, rather than an accidental real value from an empty supremum. The maximum-pattern milestone assumes positive piece lengths and nonnegative stock length, so the feasible set is finite and nonempty. The recursion milestone assumes positive lengths for all types through the newly added one; without the earlier positivity, a negative earlier length could let the new piece count exceed the displayed upper bound. The nondegeneracy hypotheses are confined to the sufficient directions of the three improvement milestones.
Reusable contributions include lemmas connecting the bordered inverse with , finite-support linear program identities, and the integer knapsack recurrence. The source's rounding discussion, heuristic search, and under-specified anti-cycling device are outside this mission. An encoding that compares the current solution only with basis columns or generated columns would miss the paper's stopping claim.
Prove that CLIQUE is NP-complete by reducing the existing 3-SAT language, KSat.KSAT 3, to it. An instance consists of a finite simple undirected graph and an input threshold; it asks whether the graph contains a clique of at least that size.
(https://prove2.me/theorems/d82e8682-c490-4742-a5e5-dd3a0b870b90). The construction specializes Karp’s SAT-to-CLIQUE reduction to 3-SAT.
A Markov decision process with finitely many states and actions and a discounted cost criterion can be solved in three classical ways: policy iteration, value iteration, and linear programming. The third goes back to F. d'Epenoux's paper A Probabilistic Production and Inventory Problem (Management Science 10(1), 1963, partly redrafted from a translation of d'Epenoux's 1960 article in the Revue Française de Recherche Opérationnelle), which showed that the optimal discounted cost of a stochastic production and inventory model is the solution of a single linear program. Together with Manne's linear program for the average-cost case (1960), it is the origin of the linear programming approach to dynamic programming, which underlies occupation-measure methods, constrained Markov decision processes, and approximate linear programming for large models.
Timeline:
The stock at the beginning of a period is , where is the stock capacity. The decision is the potential , the quantity available for the period (output plus initial stock), with . Given the potential , the stock at the end of the period is with probability ; each row is a probability vector. The expected cost of a period with initial stock and potential is a real number . Costs one period ahead are discounted by , .
A strategy is a map with for every : the potential depends only on the current stock. It has the transition matrix and the cost vector . The cost of following forever is the solution of (2), . The optimal cost solves the fundamental equation (7),
For a vector put . The set consists of the vectors satisfying the linear constraints (9), for all admissible pairs . The set consists of the vectors with for every .
The system (7) has a solution, and every solution is the greatest element of :
Moreover, for every weight vector with all and , is the unique optimal solution of
The result turns a fixed-point equation with a minimum in it into a linear program with linear constraints. Its consequences are the ones the paper draws in Section 6: the dual of has a probabilistic interpretation (discounted state–action frequencies), its optimal basic solutions are optimal strategies, and every linear programming algorithm becomes an algorithm for discounted dynamic programs. The uniqueness clause is what makes the weighted objective recover the whole cost vector; with a single objective , as the paper notes, the optimum need not determine the complete optimal strategy when the states decompose into several groups.
The dynamic programming half of the paper (Sections 2–4: policy evaluation, policy iteration, value iteration) is already formalized and proved on the platform for the general finite discounted model, as Bertsekas, Dynamic Programming and Optimal Control, Prop. 7.3.1 (BertsekasDP.discounted_main_theorem); it enters this mission as a reference item, and the mission's model is an instance of the same published structure BertsekasSSPModel. The linear programming half is not formalized. Related items in other models are posed elsewhere: Bäuerle and Rieder's Theorem 7.5.9 (finite-state linear program in a measure-theoretic reward model, open) and Denardo's Programs I–II in an abstract contraction model; neither states the componentwise maximality of in in this model.
The individual steps are short, but the goal combines several facts that are easy to state wrongly. The paper calls the invertibility of and the positivity of its inverse "known and obvious"; in Lean they are statements about an arbitrary stochastic matrix over Fin m, for which Mathlib provides no default matrix norm, and the comparison of with depends on them. Uniqueness of the optimum of needs both strict positivity of the weights and the componentwise maximality; with a zero weight it fails. The obvious first idea for the strict maximum, that indecomposability of the optimal strategy's matrix alone suffices, is not the formalized statement: only the sufficient condition over all strategies is posed.
Stock levels and potentials are Fin (σ + 1), -based. The kernel is an arbitrary stochastic kernel indexed by the potential, and the costs are arbitrary reals; the paper's demand-driven kernel and its cost decomposition are an instance and are not built in, because the arguments of Sections 2–5 use only stochasticity (the paper itself remarks on p. 101 that its methods apply far beyond the inventory problem). Only admissible pairs enter , , the minimum in (7), and strategies. The discount is called lam in Lean. Equation (7) is the fixed-point equation of the Bellman operator BertsekasDiscountedBellmanOp of the model.
Explicit readings of the paper's phrases:
IsGreatest in the componentwise order.Ruled out: defining as the optimum of the linear program, as a supremum of , or as a limit (which would make the goal circular); assuming a solution of (7) without the existence conjunct; constraining also the inadmissible pairs (which can exclude from ); and weakening the weights to .
Not formalized: the demand-driven kernel, the finite-horizon recursion of Section 2, the monotone convergence remark of Section 4 (c), the count of strategies, the reformulations and , and all of Section 6 (duality). Contributions welcome: proofs of the milestones and of the goal, and, as a follow-up mission, the dual programs of Section 6. The matrix facts (3)–(5) are stated for arbitrary stochastic matrices and are reusable beyond this mission.
A retailer that sets both its replenishment quantities and its prices over a finite selling season faces a coupled decision: the price shapes the demand that the inventory must serve, and the inventory position shapes which price is worth charging. With a fixed cost per order, the classical inventory answer is the (s, S) policy of Scarf (1960): when the stock falls below a reorder point , order up to the level . Thomas (1974) asked what happens when the price is also a decision, and conjectured that an (s, S, p) policy — an (s, S) ordering rule together with a price that depends on the stock level — is optimal "under fairly general conditions". He also gave a counterexample when prices are restricted to a discrete set.
Chen and Simchi-Levi (Operations Research 52(6), 2004) settled the conjecture for the finite horizon. When demand is additive in a random shock, , the conjecture holds (§3, Theorem 3.1). When the shock is not additive, it fails, and a weaker policy class is optimal (§4, the second mission of this series). This mission formalizes the additive case.
Timeline:
There are periods . In period the firm starts with inventory , orders up to a level at cost , where is a fixed cost, a unit cost and if and otherwise, and sets a price. Demand is for a random pair with , ; in the additive case . Unmet demand is backlogged, and an end-of-period inventory costs , a convex function.
Since price and expected demand determine each other, the decision is an expected demand , with price and expected revenue , assumed concave. With , the profit-to-go functions satisfy and, for ,
where maximizes over . A function is k-convex if for all , , (Definition 2.1), and k-concave if is k-convex. Assumptions 3–5 of the paper give the stated one-sided growth limits and polynomial growth , and give demand a finite -th moment.
For additive demand and every period : attains its maximum at some , the functions and are k-concave, and there exist such that
maximizes over , , and a best expected demand exists at ; the price is of it.
The theorem identifies the structure of an optimal policy for a basic model of coordinated pricing and replenishment: two numbers per period determine the ordering decision, and the price is a function of the post-order stock. It confirms Thomas's conjecture in the additive case and tells a computation or an approximation scheme which policy class it may restrict to; §5 of the paper extends it to a nonincreasing fixed cost, the infinite horizon and Markovian demand.
The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization adds checked versions of the k-convexity toolkit (the equivalence of the two standard definitions; the (s, S) structure lemma), a checked monotone-selection argument for a parametric maximization, and a checked finite-horizon induction in which an expectation, a maximization over a continuous action and a fixed cost interact. The proof of part (a) is omitted in the paper ("similar to that of Theorem 1 in Federgruen and Heching (1999)"), so formalizing it supplies a missing argument.
The obvious argument fails at the expectation. A k-concave function composed with a shift is k-concave for a fixed , but here the demand decision depends on , and k-concavity, unlike concavity, is not preserved under an arbitrary reparametrization: Definition 2.2 is asymmetric in its two points. The inequality needed for the continuation value requires the post-demand levels to be ordered like the inventory levels . That is the content of Lemma 2, and it uses additivity; for multiplicative demand the ordering fails, and so does the theorem (§4).
The second difficulty is analytic: each step of the induction needs a continuous continuation value of polynomial growth, so that the expectation in (3) is finite and continuous, the maximum over is attained, and is coercive.
The model is a structure of real data indexed by , with periods ; the law of is a probability measure on and expectations are Bochner integrals. The formalization works in expected-demand space , equivalent to price space because is a continuous strictly decreasing bijection. Additivity is " almost surely". The profit-to-go is defined by recursion on the number of periods to go, with . Maxima are written as real suprema; every target that uses them asserts that they are attained, so the convention that an unbounded supremum is never enters. k-convexity is the platform's BertsekasKConvex (Definition 2.1); k-concavity of is k-convexity of .
Conventions and restrictions relative to the printed page:
A trivializing formalization is ruled out: the targets assert attainment of every maximum they mention and the identity between and the maximized objective, so a supremum that defaults to , or an integral of a non-integrable function, cannot make them hold vacuously; and the assumptions are satisfiable (a one-period instance with meets all of them).
A complete development needs: continuity of parametric integrals under polynomial domination; attainment of maxima over compact intervals; Topkis-style monotone selection for functions with increasing differences; the (s, S) structure lemma for k-convex functions (proved on the platform); and the closure of k-concavity under the operations above. The k-convexity results and the monotone-selection lemma are reusable for the general-demand mission of this series and for other fixed-cost inventory models. Contributions to any milestone are welcome, including proofs that rely on platform results by Topkis (Supermodularity.Monotonicity.argmax_increasing_of_increasing_differences).
The ellipsoid method is the cutting-plane algorithm that settled the polynomial-time solvability of linear programming and, more generally, of convex optimization over any set that comes with an efficient separation oracle. It was introduced for convex minimization by Shor and by Yudin and Nemirovski in the 1970s, and Khachiyan used it in 1979 to give the first polynomial-time algorithm for linear programming. Grötschel, Lovász and Schrijver later turned it into the general equivalence between separation and optimization that underlies much of combinatorial optimization.
This mission is the second of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980v2). Its goal is the convergence guarantee of the ellipsoid method, Theorem 2.4 (p. 250), together with the geometric lemma and the steps of the proof on which it rests.
Timeline:
Write for the space of real -vectors, with the dot product . An ellipsoid is a set
where is its center and is a symmetric positive definite matrix.
A convex body is a compact convex set with non-empty interior. The objective is continuous and convex on with values in , and are such that lies in the Euclidean ball of center and radius and contains some Euclidean ball of radius . A subgradient of at is a vector with for all .
The method starts from , . At step it asks for a vector :
It then replaces by the ellipsoid given by
After iterations the output is the best of the queried centers that lie in .
For and every , , some queried center lies in , and every output satisfies
and for the explicit ellipsoid (2.5)–(2.6) works. 3. The remark before Theorem 2.4 (p. 250): a point of can leave the current ellipsoid only at a step with , and then its value exceeds . 4. Two steps reused from Theorem 2.1 (pp. 246–247): for , and on .
Theorem 2.4 bounds the oracle complexity of the ellipsoid method: accuracy needs oracle calls. Each step costs arithmetic operations plus one oracle call. With the separation oracles of linear and semidefinite programs this gives polynomial overall complexity (p. 250). The rate depends on the instance only through and , so the method needs no smoothness and no strong convexity. Lemma 2.3 is also the geometric step of the ellipsoid method for linear feasibility.
The result has a textbook proof. The work of this mission is to formalize it. The same update is published on the platform from Bertsimas and Tsitsiklis's Introduction to Linear Optimization (Theorem 8.1), with a proved volume factor of . That factor is weaker than (2.4)'s and does not give Theorem 2.4's constant. The sharper factor and the optimization version of the method (subgradient cuts, the output rule and the value bound) are not formalized on the platform.
There are two difficulties: Lemma 2.3 with the sharp constant, and the bookkeeping that turns per-step volume decrease into a value bound.
For the lemma, the volume of the explicit ellipsoid is times that of . Bounding it by rather than by the cruder needs the scalar inequality of milestone 1 for every . The reduction from a general ellipsoid to the unit ball also needs determinants under an affine map.
For the theorem, the obvious argument compares with . This only works if no cut removes an optimal point and if every removed point of is worse than a queried center. At the threshold the admissible is exactly , so a non-strict volume bound alone does not close the argument there.
Fin n → ℝ with Lebesgue measure, as in the reused Bertsimas–Tsitsiklis ellipsoid definitions (LinearOptimization.ellipsoid, ellipsoidUpdateCenter, ellipsoidUpdateMatrix, IsSubgradientOn).Fin n → ℝ is the sup norm.IsEllipsoidRun. Every theorem holds for every admissible oracle answer. The update is the published one with .Conventions and hypotheses added to the page:
A run predicate whose separation branch does not require , or that accepts with an update, would make the statements false or vacuous. Both are excluded.
Lemma 2.3's volume factor is . The weaker published factor does not prove that milestone. The published theorem LinearOptimization.ellipsoid_update_halfspace_volume is included as a reference: it supplies the containment (2.3) and positive definiteness. Contributions are welcome on every milestone. A determinant formula for the volume of an ellipsoid would be reusable well beyond this mission.