Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. A high-probability approximation guarantee is a separate claim requiring an explicit probability bound. The optimum includes entangled states. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Service organizations keep repairable spare parts at a depot and at operating bases. Stock has a purchase or holding cost, while insufficient stock leaves backorders. Craig Sherbrooke's METRIC study describes how to evaluate such a system and distribute additional units among item types. Its fifth computational stage compares the reduction in expected backorders from the next unit with the cost of that unit. The comparison is delicate because the backorder function after optimizing the depot–base split can fail to be convex as a function of total item stock, even though a fixed depot-stock version is convex. Sherbrooke therefore introduces a convex extension before applying marginal analysis (Sherbrooke 1968, pp. 134–135).
This mission isolates the theorem in the paper's Appendix. It concerns abstract item functions with the properties needed for the allocation rule, so the result can be studied independently of the queueing assumptions and the FORTRAN procedure that produced those functions in METRIC. The paper supplies a proof of the Appendix theorem; the mission seeks a machine-checked formalization of its precise mathematical content (Sherbrooke 1968, pp. 140–141).
There is a finite collection of items indexed by . A decision assigns each item a stock level , where is permitted. Item has a unit cost and a real-valued function representing the backorder contribution associated with stock level . In the METRIC application, is obtained after choosing the best allocation of units between depot and bases. The Appendix theorem uses only that is nonincreasing and has a finite lower bound. “Decreasing” is read weakly: the paper's justification says that adding a unit “cannot exceed” the backorders at the previous level (Sherbrooke 1968, p. 136).
For a function , write . The function is discretely convex when at every level. The lower convex hull , written in the paper, is the greatest discretely convex function at or below . It follows the lower boundary of the convex hull of the points ; a point above that boundary is lowered, while a contact point keeps its original value (Sherbrooke 1968, pp. 135–136, 140). The existing ServiceParts.StockLevels.Basic definition supplies and for real stock-level functions; this mission reuses it.
The original objective is the separable sum
For each item, conditions (12) select the first level where adding another unit no longer lowers the convexified cost:
The second condition is automatic at , following the paper's convention (Sherbrooke 1968, p. 140, Eqs. (11)–(12)).
The Appendix goal is that each item's conditions (12) have exactly one solution and that the vector formed from those solutions minimizes the original, possibly nonconvex objective:
The milestone list follows the Appendix's claims: the lower boundary is a convex minorant; its marginal changes approach zero; (12) has a solution and that solution is unique; it minimizes the convexified single-item cost; and the selected level is a contact point where . The final comparison is with , not just with the objective formed from (Sherbrooke 1968, pp. 140–141).
The theorem licenses the paper's marginal allocation rule even when an item's original backorder function has nonconvex points. The rule can use a convex lower boundary to identify a level, yet the resulting allocation is optimal for the original function. Without the contact-point conclusion, optimality of the modified objective alone would not give that guarantee. The theorem is stated for any finite number of independent items with the listed properties, so it is reusable beyond the specific depot–base model (Sherbrooke 1968, pp. 134–136, 140–141).
The paper proves the result informally. This mission's definitions and theorem statements compile locally as open Lean goals; they do not yet constitute a machine-checked proof. A related published Prove2Me result, ServiceParts.Allocation.allocOpt_correct, proves correctness of an allocation algorithm for piecewise-linear functions assumed convex. It does not address the convexification or contact claim here. The platform's posed ServiceParts.StockLevels.optimal_stock_criterion and greedy_fill_rate_optimal concern other marginal criteria and likewise do not settle this Appendix theorem. A successful development would provide reusable Lean infrastructure for lower convex envelopes of integer sequences, their forward differences, and separable finite allocations.
A one-step marginal comparison on the raw is insufficient when its forward differences can fall and then rise: an apparent local stopping point need not minimize the full sequence. Replacing by a convex minorant restores ordered marginal changes, but a minimizer of a smaller function need not minimize the original function. The central burden is therefore the exact relation between the lower boundary and the original points at a level selected by the strict condition in (12). Ties in the objective add a second precision issue: the selected level is unique under the rule even when the objective has more than one minimizer (Sherbrooke 1968, pp. 135, 140–141).
Stock levels are natural numbers, item contributions and costs are real, and the item type is finite; the empty item type is allowed, making both the sum and the coordinatewise statement trivial. The functions are nonincreasing and bounded below, as in the Appendix. The lower hull is a pointwise real supremum over all discretely convex minorants. Its defining family is nonempty and bounded at each point under the lower-bound hypothesis, which every hull theorem carries. The hull is therefore fixed by the input function rather than supplied as an arbitrary minorant. The goal compares every vector in , without a budget restriction. The formalization does not use a default value for : the predecessor condition applies only to positive stock levels.
The paper prints with at least one positive cost. Its existence assertion fails when a particular : for , a bounded, decreasing, convex sequence, the first inequality of (12) never holds. The goal and existence milestone therefore require for every present item. The paper's phrase “unique optimizing” is interpreted as uniqueness of the stock vector determined by (12), together with its optimality. It cannot assert uniqueness among all minimizers: with , , and for , levels and tie. The proof's own wording identifies (12) as the unique selection rule (Sherbrooke 1968, p. 140).
The formalization contains separate definitions for discrete convexity, the greatest lower hull, conditions (12), and objective (11). It welcomes proofs and general lemmas about convex integer sequences and finite separable sums. The METRIC computation, empirical Air Force data, equations (7)–(9), and the discussion of Lagrangian versus combinatorial solutions are context rather than goals of this mission. A definition that simply sets , or a conclusion that minimizes only the hull objective, would omit the theorem's content.
A finite dynamic program with total reward is the basic model of sequential decision making without discounting: a system moves among finitely many states, a decision maker picks an action in each state, collects a reward, and the system moves on or stops. The quantity of interest is the expected total reward of a policy, summed over the whole (possibly infinite) horizon, and the question is whether a simple policy — one that uses the same decision rule at every step — is as good as any other.
For discounted or strictly substochastic models the answer has long been known. Shapley (1953) showed by successive approximations that, when every transition matrix has row sums strictly below one, some stationary policy maximizes the total reward among stationary policies; Howard (1960) gave the policy-improvement method for finding one; Blackwell (1962) showed that the maximum over all policies is attained among stationary ones. All of these rest on a contraction hypothesis .
Veinott's 1969 paper (DOI 10.1214/aoms/1177697379), best known for its sensitive discount optimality criteria, opens in §2 by proving these classical results under the much weaker hypothesis that each stationary policy is transient, and without requiring the transition weights to be substochastic at all. Partial results in this direction were due to Eaton and Zadeh, Derman, and Denardo. The total-reward model without a contraction assumption covers stopping problems, shortest-path type problems and models in which "transition weights" are not probabilities (growth factors, populations), which is why the generalized model is of independent interest.
There are states . In state a finite nonempty set of actions is available; taking action earns the real reward and assigns the transition weight to each state . No bound on is assumed. The set of decision rules is ; for , is the vector and the matrix .
A policy is a sequence of decision rules. The policy is stationary; uses first and then follows ; repeats the first rules of forever and is called periodic. Let and . The policy is transient if converges, and then its vector of total returns is
The one-step comparison measures the gain from deviating to for one step. Vectors are compared coordinatewise, and means , . For a matrix , and is its spectral radius. Finally and , both coordinatewise.
If every stationary policy is transient, there is with
The hypothesis concerns only the finitely many stationary policies; the conclusion compares against every policy, stationary or not.
Corollary 6 is the existence half of the theory of total-reward Markov decision processes: it says that the search for an optimal policy can be restricted to the finite set of stationary policies, and, together with Corollary 2 and Theorem 1, that such a policy is characterized by the optimality equation and by the absence of one-step improvements. Corollary 4, which the paper's introduction singles out as the section's main new result, shows that transience of the finitely many stationary policies already forces transience of every policy, uniformly; this is what makes well defined for all policies. Hoffman's Lemma 3 converts transience into a contraction in a rescaled norm, the device behind geometric convergence of value iteration (Corollary 3 of the paper).
On the formal side, Mathlib has matrices, summability and spectral radii but no total-reward decision model. These results are proved in the 1969 paper and are standard in the textbook literature on Markov decision processes; none of them has a machine-checked proof that we know of. Related platform items concern other models: the stochastic shortest path results of Bertsekas and Tsitsiklis (a cost model with a termination state, stochastic rows and an infinite-cost assumption on improper policies) and Blackwell's discounted model; neither covers nonnegative, non-substochastic weights.
Without a contraction, the standard argument — is a contraction, so it has a unique fixed point attained by a stationary policy — has nothing to start from: may exceed one for every , and the transition weights need not be probabilities, so no probabilistic coupling or stopping-time argument applies directly. Transience of each stationary policy is a statement about finitely many matrix powers , whereas the goal concerns infinite products of different matrices , whose behaviour is not controlled by the spectral radii of the factors in general. Passing from the stationary policies to all policies is the step where the obvious argument fails.
The Lean development fixes these conventions.
St; actions are a family of nonempty finite types A : St → Type, so is the dependent function type (s : St) → A s, not a common action set.Program St A with real rewards and nonnegative weights; no row-sum bound is part of the structure. Only 5° of Corollary 4 assumes .ℕ → F, indexed from : π 0 is . "All policies" means all such sequences.Summable of in the entrywise topology. is a tsum; it is the genuine series exactly for transient policies.spectralRadius ℂ of the complexified matrix, valued in .Finset.sup' over the finite set .A trivializing formalization is ruled out: the goal and Theorem 1 do not assume the competing policies transient (that would hide Corollary 4 inside the hypothesis), and since a non-summable tsum is , no statement compares of a policy whose transience is not either assumed or implied by the hypotheses. The hypothesis "every stationary policy is transient" is satisfiable (for instance when all weights are zero) and is not implied by any row-sum bound.
A complete development needs Neumann series for nonnegative matrices, the Perron–Frobenius-type fact that a nonnegative matrix with spectral radius below one has a nonnegative , and finite-dimensional spectral theory relating to . These are reusable well beyond this mission; contributions of such lemmas, and of proofs of the milestones in any order, are welcome.
A speed recorded as a vehicle passes a fixed point and a speed recorded among vehicles occupying a road segment answer different questions. Fast vehicles pass a detector more often per unit time; slow vehicles remain visible along the segment for longer. Traffic studies therefore need to identify which distribution a measurement samples before comparing average speeds. J. G. Wardrop made this distinction explicit in his 1952 treatment of road traffic, then quantified it through the variance of the spatial speed distribution (Wardrop 1952, pp. 327–331 and Appendix II).
The result belongs to the paper's mathematical account of traffic flow. It is useful even when the subsidiary streams do not describe a random vehicle process: the identities concern finite positive flows and speeds. The paper also applies the same distributions to speed samples from radar and aerial photographs and to an idealized count of overtaking events (Wardrop 1952, pp. 330, 333–334).
A road's traffic stream is divided into subsidiary streams, indexed by . Stream has flow , the number of vehicles passing a point per unit time, and speed . Its concentration is , the number of vehicles occupying a unit road length. Total flow and concentration are and . The time frequency weights each stream by how often its vehicles pass a point. The space frequency weights it by the fraction of vehicles present along the road.
The time-mean speed is . The space-mean speed is . Both are averages of the same speeds; the weights differ. Wardrop defines the space-distribution variance independently as , and the corresponding coefficient of variation as (equations (1)–(3), (7), pp. 328–331).
These are finite sums, not limits of a stochastic process. The model requires at least one subsidiary stream and positive flow and speed for each stream. Positive flows ensure that every speed in the equality criterion belongs to a present stream; positive speeds make concentration meaningful. The count is allowed to be one. In that case both means coincide and the variance is zero, as the formulas require.
The main target is Wardrop's equation (6), together with its stated comparison and equality case (p. 330; Appendix II, p. 356):
The subsidiary targets follow the paper's order. Equation (4) says for each stream, giving equation (5), . Appendix II then uses the centered identity and rewrites the time mean as . These three claims are the mission milestones. Equation (8) is included as a companion formulation:
The mission also records the paper's formulas for equally weighted time and space speed samples and the equivalent space- and time-frequency formulas for the idealized overtaking count. These companions use the same definitions without changing the main target (pp. 330–334).
The identity gives an exact size and direction for the difference between the two averages. Since the variance is nonnegative and is positive, the time mean cannot fall below the space mean. If all constituent speeds are equal, the difference vanishes; if any two present streams have different speeds, the difference is positive. The formula therefore lets a reader decide whether two reported speed averages can be compared directly, and it identifies the spatial variance as the quantity needed to convert between them.
The sample formulas sharpen that interpretation. Equal weights among vehicles passing a point make the time mean the arithmetic mean of the sampled speeds and the space mean their harmonic mean. Equal concentrations reverse which mean is arithmetic; the time mean becomes . The overtaking formulas express a single pairwise count using either frequency system, provided the speeds are ordered and the paper's assumption of no interference with overtaking is used (Wardrop 1952, pp. 330, 333–334).
Wardrop proved these formulas in print. The remaining work in this mission is a machine-checked proof of the finite-sum identities and their strict equality case. The proposal supplies typed statements and definitions, but the theorem proofs are open. The resulting concentration and frequency definitions are reusable in other traffic-flow formalizations; the statements also provide small algebraic interfaces for testing more elaborate traffic models.
The relation looks like a routine identity for weighted means, but the two weight systems are coupled through . One cannot treat the time and space frequencies as independent arbitrary probability vectors and still obtain equation (6). The strict case needs more than nonnegativity of the variance: it needs the fact that every space weight is positive, so zero variance forces every constituent speed to equal the mean. The single-stream case and every denominator need the same attention.
The overtaking statement has a separate modelling boundary. Its algebraic equalities use a rate defined by pairwise speed differences. Wardrop's physical interpretation of that rate assumes that overtaking does not interfere with other overtaking. The mission records the identities for that idealized rate, without claiming that a measured road necessarily meets the physical assumption.
Lean uses Fin C for the streams and real numbers for , , , both means, the variance, and the overtaking rate. Finite sums are taken over all streams. The theorem hypotheses require , , and for every . These requirements make , , and positive; Lean's total division would otherwise assign a zero value at a zero denominator that has no meaning in the paper's model. For the overtaking identity, StrictMono v retains Wardrop's ordering .
The variance is defined from equation (7), . Defining it by rearranging equation (6) would make the target true by definition and would erase the mathematical claim. The standard deviation uses the real square root of that variance. An observation in the sample companion is represented as one subsidiary stream of equal time or space weight; this is the formal reading of the paper's sampling paragraphs. No probability-measure library is needed, since and are explicit finite weights.
A complete proof needs finite-sum rearrangements, elementary real division under positive denominators, nonnegative weighted squares, and the equality case of a positive weighted sum of squares. The definitions and the mean identities are welcome as separate reusable contributions. The mission does not include the paper's normal approximation for overtaking density in equation (11), which Wardrop presents as an approximation rather than an exact finite-sum theorem.
A controller observes a finite system period after period, chooses an action in each state, earns an income and moves the system at random. When future income is not discounted, the natural criterion is the average return per unit time (the gain), but many policies share the maximal gain while differing in their transient income. Blackwell (1962) showed that the policies that are optimal as the discount factor tends to one, the 1-optimal policies, are exactly the stationary policies that first maximize the gain and then, among those, the bias. He gave no finite procedure for the second maximization. Veinott (1966) supplied one: an extension of Howard's policy improvement method in which a second improvement test, on the bias, is run after the gain test is exhausted, with a third vector guaranteeing termination. The method and its sensitivity hierarchy became the starting point of the -discount optimality theory developed by Veinott (1969) and treated in Puterman's Markov Decision Processes (1994), Chapter 10.
Timeline:
There are finitely many states and a finite set of actions. Choosing action in state earns the income and moves the system to state with probability . A decision rule picks an action in each state; is the vector with entries and the stochastic matrix with entries . A policy is a sequence of decision rules, is a stationary policy, and for
is the vector of expected discounted returns. For vectors, is coordinatewise and means and .
Let be the Cesàro limit of the powers of . The gain and the bias are the unique solutions of
and is the unique solution of , . Write for the decision rules of maximal gain and for those of maximal bias within .
The two improvement sets compare with a decision rule through the state-by-state tests
consists of the for which (i) holds everywhere, (ii) holds wherever (i) is an equality, some inequality is strict, and wherever both are equalities. consists of the for which (i) and (ii) are equalities at every state. For ,
and consists of the for which (iii) holds everywhere, strictly somewhere, with wherever it is an equality.
For every :
Part 2 is the stopping certificate and parts 3 and 4 are the progress guarantee; together they say that the extended method raises lexicographically and stops at a decision rule in .
Theorem 6 turns Blackwell's existence result into an algorithm. Blackwell's characterization requires maximizing the bias over , a set with no explicit description; Lemma 5 shows that maximizing over the explicitly available set suffices, and Lemma 4 shows that this maximization has the same form as the original gain maximization, so the familiar policy improvement machinery applies a second time. The same mechanism, iterated, gives the -discount optimal policies of the later sensitivity theory and the lexicographic policy improvement algorithms in standard texts.
The results are proved in the paper (with a correction to the proof of Lemma 5 credited to Bruce Miller). They are not formalized in any proof assistant known to the mission. A complete development yields machine-checked policy improvement for average and bias optimality on top of the published Blackwell model, including the convergence-free closed forms of gain, bias and and the facts about the limit matrix and the deviation matrix they rest on.
Parts 1 and 3 are Blackwell's policy improvement for the gain, transported to Veinott's set . The new content is in parts 2 and 4, and in both the obvious argument fails at the same place: the bias of cannot be compared with the bias of by a state-by-state test in the original problem, because is a product of action sets different from the original ones, and Blackwell's comparison works only after a reduction to a problem in which the reward is and the role of the gain is played by . A second difficulty is Lemma 5: may be a proper subset of (Example 3 of the paper), so maximizing the bias over does not obviously maximize it over . The certificate does not follow from the gain and bias tests at alone, and the paper's original proof of it contained an error (corrected, as the paper records, by Bruce Miller).
Everything is built on the published Blackwell definitions (BlackwellDiscreteDP.NearOne.Model, LimitMatrix, GainBias): one finite action type available in every state (Veinott's are all equal to it), decision rules St → Act, policies indexed from (π 0 is ), real vectors St → ℝ with the pointwise order, and VecGt for the paper's (not coordinatewise strict). is the published Cesàro limit , the same limit as Veinott's . The gain and bias are the published closed forms and with the deviation matrix ; the new vectors are closed forms too: and , and their characterizations by (10) and (12) are milestones. 1-optimality is the published IsNearlyOptimal, which compares against every policy. Veinott's set is HSet, to keep it apart from the deviation matrix Hf.
and are defined literally from the paper's inequalities, including the clauses "at least one strict" and " where the tests are equalities". Dropping either clause makes parts 3 and 4 false (a that only reshuffles ties would count as an improvement); replacing or by a set defined through the conclusion of the theorem would make the goal trivial. Neither is acceptable.
The reduction "replace by and by " is not instantiated, since the published model has a single action set; its two uses in the proof of Theorem 6 are milestones stated in the original model. A development of the general model with state-dependent action sets, and of the limit-matrix identities , , , would be reusable well beyond this mission. Proofs of any milestone are welcome, as is a proof of the published Theorem 3 and Lemma 1, on which most of the mission rests.
Two impossibility theorems frame the theory of collective choice. Arrow's theorem (1951) says that a rule aggregating individual preference orderings into a social ordering, subject to a short list of reasonable conditions, must be dictatorial. The Gibbard–Satterthwaite theorem (Gibbard 1973, Satterthwaite 1975) says that a voting procedure selecting a single alternative, which no voter can manipulate by misreporting, must be dictatorial once at least three outcomes are possible. Both conclusions are the same, and the two conditions—Arrow's axioms and strategy-proofness—look unrelated: one is about the coherence of a social ranking, the other about voters' incentives.
Satterthwaite's paper (Northwestern Discussion Paper No. 122, 1974; J. Econ. Theory 10, 1975) shows that the two conditions are in fact the same condition. Section 4 constructs a one-to-one correspondence between strict strategy-proof voting procedures with full range and strict social welfare functions satisfying Arrow's conditions, under which each social welfare function's top choice is the voting procedure's outcome. This mission formalizes that correspondence.
Timeline. Arrow (1951, 2nd ed. 1963) proved the general possibility theorem with conditions of non-negative response (NNR), citizens' sovereignty (CS), independence of irrelevant alternatives (IIA) and non-dictatorship. Gibbard (1973) proved that strategy-proof game forms with at least three outcomes are dictatorial, by first showing that a strategy-proof procedure induces an Arrovian social welfare function and then applying Arrow's theorem. Satterthwaite (1974/75) gave an independent direct proof of the voting-procedure theorem and proved the correspondence theorem (Theorem 2), which turns Gibbard's construction into an exact equivalence.
A committee of individuals chooses from a finite set of alternatives. A strong order on is a complete, transitive relation with no indifference between distinct alternatives; denotes strict preference. Let be the set of strong orders and the set of strict ballot sets .
Arrow's conditions on : CS—for all some gives ; IIA—if for all then ; NNR—raising an alternative in individual ballots, with the order of the other alternatives unchanged, never lowers against any other alternative in the social ordering. PO (Pareto optimality): unanimous strict preference for over yields .
For and there is a bijection
with for every and every .
The correspondence explains why the two impossibility theorems have the same conclusion: for strict preferences, a strategy-proof procedure with full range and an Arrovian social welfare function are two descriptions of one object. In particular either impossibility theorem, together with Theorem 2, yields the other. The paper draws a second consequence: a social welfare function violating rationality or IIA has a derived voting procedure that is manipulable, so Arrow's much-debated conditions are forced by the practical requirement of strategy-proofness.
On the formal side, the platform already has machine-checked proofs of the strict Arrow theorem (AGT.arrow_theorem, unanimity and pairwise IIA) and of the strict full-range Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite). Together these determine both sides of Theorem 2 as sets of dictatorships, but neither states the correspondence, the derived/underlying relation, Gibbard's construction or NNR, and nothing on the platform states Lemmas 7 or 8. The milestones here formalize the paper's direct argument, which does not pass through the impossibility theorems.
The obvious argument fails in two places. First, a strategy-proof voting procedure determines only the top of a social ordering, and the whole ordering must be recovered; Gibbard's relation does this, but proving that is transitive is the core of Gibbard's proof of the Gibbard–Satterthwaite theorem, which the paper cites rather than proves. Second, NNR as stated allows many individuals to move at once, while the manipulation argument works with one ballot at a time; one must pass from a single-voter change to an arbitrary one without losing IIA or PO along the way.
A newcomer's first idea is to prove both sides are dictatorships and match dictators. That proves the bijection but needs both impossibility theorems as inputs, and the correspondence must still carry the underlying relation for every procedure.
A, ι with decidable equality; , throughout.ι → StrongOrder A, and voting procedures and social welfare functions are defined only on them. Two social welfare functions are therefore equal exactly when they agree on every strict ballot set; this is what makes uniqueness in Lemma 8 and the bijection in Theorem 2 meaningful.Set.range v = Set.univ.Equiv together with " underlies " for every . A bare existence of a bijection between the two sets is a cardinality fact and is not the theorem.Reusable beyond this mission: the strict-preference vocabulary (strong orders, , Arrow's conditions in the paper's form) and Gibbard's construction. Contributions welcome: proofs of each milestone, and bridges to AGT.arrow_theorem and AGT.gibbard_satterthwaite.
A social welfare function turns the rankings of the members of a committee into one ranking for the committee. Arrow's general possibility theorem (Arrow, 1951/1963) shows that, once there are at least three alternatives, no such rule satisfies a short list of conditions that each look harmless unless it follows a single member's ranking. The theorem is the starting point of social choice theory and underlies the study of voting rules, preference aggregation in economics, and rank aggregation in computer science.
Arrow's own setting allows indifference: ballots and the social ordering are weak orders, and the conditions he imposed are citizens' sovereignty, non-negative response, and independence of irrelevant alternatives. Many textbook proofs, and the existing machine-checked versions, instead take strict ballots and replace the first two conditions by the Pareto condition.
Satterthwaite's discussion paper (Satterthwaite, Northwestern DP No. 122, 1974, journal version J. Econ. Theory 10 (1975)) gives a new proof of Arrow's theorem. Strict Arrovian social welfare functions correspond one-to-one to strategy-proof voting procedures with full range, and the Gibbard–Satterthwaite theorem then forces a dictator. His §6 extends the argument to weak orders by decomposing a social welfare function into a tie-breaking step followed by a strict one. This mission formalizes that weak-order extension and the strict theorem it rests on.
Timeline.
A committee of individuals ranks a finite set of alternatives. A weak order on is a complete, transitive relation, and reads " is preferred or indifferent to ". Its strict part is : and not . The weak orders form . A strong order is a weak order with no indifference between distinct alternatives, and the strong orders form . A ballot set is .
A social welfare function assigns to every ballot set a social ordering . A strict social welfare function is defined only on strong ballot sets and takes values in . For , is the set of -best elements of , and is the restriction of to .
A tie-breaking function maps every weak ballot set to a strong one while keeping every strict preference. It is regular if each individual's ties are broken by a fixed strong order .
For , and any social welfare function on weak ballot sets,
The converse is false with indifference, so the goal is one-directional.
Theorem 3' is Arrow's theorem in the setting Arrow stated it: weak-order ballots, a weak social ordering, and the conditions CS and NNR instead of the Pareto condition. Lemma 10 and Lemma 11 together say that Arrovian social welfare functions with indifference are determined by strict ones up to tie-breaking. This is the structural fact the paper also uses for its weak-order correspondence (Theorem 2').
All results here are proved in the paper. None is formalized as stated. The platform holds a proved strict Arrow theorem, AGT.arrow_theorem, for social welfare functions on strict total orders under unanimity and pairwise IIA. Theorem 3's only-if half follows from it once CS, NNR and IIA are shown to imply the Pareto condition and the two encodings are bridged. The weak-order statement, the tie-breaking lemmas, and the "if" half of Theorem 3 are new to the platform.
Passing from strict to weak orders is the hard step. Restricting a weak ordering to a pair of alternatives does not determine its choice sets on larger sets once ties are present. A social welfare function that satisfies IIA on weak orders need not induce one on strong orders through an arbitrary tie-breaker. Breaking ties ballot by ballot with a non-regular rule can destroy IIA, and breaking ties in the social ordering can destroy NNR unless the same fixed order is used throughout. The obvious reduction is "break all ties and apply the strict theorem", and it fails: the dictator of the tie-broken function could depend on the tie-breaking order. The fact that it does not is part of what must be shown.
A and ι with decidable equality. = Fintype.card ι, = Fintype.card A, and , are hypotheses as printed. All statements live in StrategyProofArrow.WeakArrow.The definitions duplicate objects drafted in the sibling missions of this series (weak and strong orders, CS, NNR, IIA). Proofs of the strict theorem from the Gibbard–Satterthwaite theorem, bridges to AGT.arrow_theorem, and reusable lemmas about tie-breaking of weak orders are all welcome.
The method of multipliers (augmented Lagrangian method), proposed independently by Hestenes and Powell in 1969, solves a constrained optimization problem by a sequence of unconstrained minimizations of a penalized Lagrangian, updating a multiplier estimate between them. It became one of the standard algorithms of nonlinear programming and is the ancestor of ADMM and of the proximal-point view of dual methods. Rockafellar's 1973 paper (Math. Programming 5, 354–373) extended the method to inequality constraints with the penalty Lagrangian and reinterpreted it as unconstrained maximization of a smooth concave dual function . Its §4 shows that primal points recovered from any maximizing dual sequence are asymptotically minimizing; its §5, the subject of this mission, asks how fast they converge.
Timeline. 1969: Hestenes and Powell introduce multiplier methods for equality constraints. 1973: Rockafellar treats inequality constraints in the convex case through and its dual (this paper), and in the same year applies the multiplier method of Hestenes and Powell to convex programming (J. Optim. Theory Appl. 12). 1976: Rockafellar's "Augmented Lagrangians and applications of the proximal point algorithm in convex programming" (Math. Oper. Res. 1) gives the general convergence theory.
Let be convex and convex. The problem is
With and a parameter , the penalty Lagrangian is
and the dual problem maximizes over all ; is its supremum. A maximizing sequence is a sequence with . The dual method of Theorem 4.1 takes a bounded maximizing sequence and, for each , a point that minimizes to within a tolerance :
The standing assumptions of §5 concern a point that is an optimal solution of (P), near which are twice continuously differentiable, and a multiplier vector satisfying with the Kuhn–Tucker conditions (, , , and minimizes over ). With the active set and , they are: (i) for ; (ii) the , , are linearly independent; (iii) for every nonzero with for all .
Under the standing assumptions, with as in (4.7), if for some
then there is a constant with
No rate for is fixed: the statement compares the primal error with the dual error, whatever method produces the dual sequence.
Corollary 5.3 is the paper's answer to the practical question of how accurately each inner minimization must be done. A tolerance proportional to the current dual gap costs nothing in the order of convergence: the primal iterates then converge at least as fast as the dual ones. Since is with a negative definite Hessian near (Theorem 5.1 (v)), any locally linearly or superlinearly convergent unconstrained method applied to yields a primal sequence with the same rate. The estimates (5.15)–(5.17) are the quantitative bridge between inner accuracy, dual error and primal error, and reappear in later analyses of inexact augmented Lagrangian methods.
The results are proved in the paper (1973) and in textbook treatments; none of them has a machine-checked proof on this platform or in Mathlib. The mission produces a formal statement of the second-order theory of the penalty Lagrangian: the local smooth structure of and , the implicit minimizer map , and the rate comparison. Complete formal proofs of each milestone are the remaining work.
The obvious argument linearizes everything at , but is only globally: has a kink in its second derivative, so smoothness of must first be established on a neighborhood of , using complementary slackness and strict complementarity (i) to fix which branch of (2.4) each constraint follows. The sequence is not assumed to converge; localizing it into that neighborhood requires the uniform statement of Theorem 5.1 (i) (with chosen after ) and the uniqueness of and . The minimizer map then comes from the implicit function theorem applied to , and the formula for needs the derivative of the envelope .
EuclideanSpace ℝ (Fin n), multipliers in EuclideanSpace ℝ (Fin m); constraint indices are Fin m (0-based), and is a separate argument.ConvexOn ℝ X, an explicit hypothesis of every theorem, the paper's standing assumption of p. 358), and twice continuous differentiability only on a neighborhood of . Smoothness of and is always a conclusion, never a hypothesis.EReal, so (4.7), (5.2), (5.3) and (5.18) are differences in ; is explicit for the penalty Lagrangian, while is defined separately.Analysis/Calculus/Implicit), second derivatives of compositions, envelope differentiation, and the quadratic-growth estimates of a function with definite Hessian. Results on Hessian forms and on strict complementarity are reusable beyond this mission. Proofs of individual milestones are welcome independently.Volatility estimates from daily high, low and closing prices have been used since Parkinson (1980) and Garman and Klass (1980): the range of a day's log-price carries much more information about the volatility than the close alone. Rogers and Satchell (1991) propose an estimator, , that is unbiased for whatever the drift of the log-price. The companion mission (Part I) formalizes that unbiasedness.
Every such estimator meets the same practical problem. The true high and low of the continuous path are never observed; one sees the maximum and minimum of the path sampled at times. The sampled maximum falls short of the true maximum by an amount , and the resulting downward bias is large in practice (Garman and Klass, and Beckers (1983), identified it). Section 3 of Rogers and Satchell proposes a correction: model by a random variable with an explicit law, compute its first two moments exactly, and subtract their effect. The constants that appear,
enter the corrected estimator directly. Their simulations (Tables 1–3 of the paper) show that the correction removes most of the bias.
Fix a volatility and a sampling mesh (in the paper ). For a level define
The factor is the probability that a Brownian bridge of duration and volatility climbs above level . The factor is a probability density on . Since and decreases continuously to , it is the survival function of a law on . This law is the paper's display (9).
A real random variable has distribution (9) if it is measurable and for every . In the paper, is the overshoot of the continuous maximum over the sampled maximum in the sampling interval to the left of the time at which is attained, and is the overshoot in the interval to the right. The paper then assumes (p. 508) that and are independent, each with distribution (9), and approximates by . Write .
In Lean, overshootSurvival σ h α is , HasOvershootLaw P σ h Z is " has distribution (9) under ", and constA, constB are and .
For and independent with distribution (9), the variables and are integrable, and
The goal combines milestones 2–5 through , which the paper uses in (11).
The result. The two identities are the coefficients of the corrected estimator (5): replacing and by and turns the high–low estimator into an equation whose positive root largely removes the discretization bias. The same constants correct the Garman–Klass estimator (p. 509). Without exact values for and the correction has no concrete form.
Formalizing it. The paper does each of the four double integrals in a line and says "after some calculation" twice. A machine-checked derivation confirms the printed constants, which are reused in the high–low volatility literature. It also states precisely what is exact (moments of the model law (9) under independence) and what is approximation (that the model describes ). To our knowledge none of these identities has been formalized before.
The statements are elementary but none of them is a one-line identity. Each moment is a double or triple improper integral with singular weights on an unbounded domain. The minimum of and couples two such integrals, and the resulting kernels and have to be integrated in closed form over the unit square. Matching and exactly leaves no room for slack. In Lean, every exchange of integration order, change of variables and passage from survival functions to moments has to be justified for non-negative but unbounded functions, and the expectations must be shown finite: the Bochner integral of a non-integrable function is .
(Ω, P) with [IsProbabilityMeasure P]. "Distribution (9)" is Measurable Z ∧ ∀ α ≥ 0, P.real {α < Z} = G σ h α, imposed only at levels : the formula is even in , and imposing it at negative levels would make the hypothesis unsatisfiable. Independence is IndepFun Z Z' P. and are max and min.Integrable, or MemLp … 2 for second moments). The conditioning "" in (9) and (10) is the modelling context in which the paper derives the law, not a hypothesis. The paper's "" in (13) is read as , as its first line shows. The integrals in (9) run over and .survival_mean_ibp (mean as an integral of the survival function, under derivative hypotheses) is related but does not fit this setting. Mathlib's layer-cake formula is the general tool for passing between survival functions and moments.The Sherrington–Kirkpatrick model assigns random interactions to every pair of spins in a system. Its partition function aggregates the weights of all spin configurations, and the logarithm of that partition function is the free energy. For a finite system, the free energy is a random quantity because the interactions are random. A useful question is therefore how far it can move from a deterministic high-temperature scale. Aizenman, Lebowitz and Ruelle (1987), and Comets and Neveu (1995) for Gaussian couplings, proved that for the variable converges in law to a normal random variable ALR 1987; Talagrand asks instead for tail estimates valid for every . Talagrand's Chapter 12 gives a finite-size tail bound and a bound on the expected free energy per site under explicit moment conditions on the interaction law Talagrand 1995.
The chapter belongs to a larger study of concentration inequalities on product spaces. Its relevance to the spin model is concrete: each pair interaction is an independent coordinate, while every spin configuration uses all those coordinates. The number of coordinates grows quadratically with the number of spins. A uniform estimate must respect both this growing dimension and the normalization in the energy Talagrand 1995, pp. 191–195.
Fix an integer . A spin configuration is a vector with each . Each unordered pair of sites has a real coupling . For an inverse temperature , the normalized partition function is
Write . The factor averages over configurations. Since every summand is positive, for every array , so this logarithm is defined without excluding any coupling array.
The couplings are independent with a common probability law on ; their joint law is . Under , a single coupling satisfies and . The chapter also assumes for some . Its main theorem adds and . These inequalities describe a class of interaction laws rather than one chosen distribution. A median of means that both and are at least Talagrand 1995, pp. 191–193.
The goal is Theorem 12.1. There is one absolute constant such that, for and ,
and the same constant satisfies
The first formula controls deviations at finite ; the second locates the expected free energy per site. The theorem leaves the absolute value of unspecified, as the source does Talagrand 1995, Theorem 12.1.
Four numbered displays form the supporting targets. Equation (12.6) bounds the change in when all couplings are changed. Equation (12.5) bounds deviations about any median. Equations (12.7) and (12.8) give first- and second-moment estimates for . Together these specify the deterministic regularity and probabilistic estimates used by the chapter Talagrand 1995, pp. 192–195.
The theorem gives a nonasymptotic probability estimate, valid for each finite size and each law meeting the stated conditions. It also bounds the difference between the mean free energy per site and as grows, for fixed . The moment estimates separately describe the scale of the partition function and limit its relative second moment. These conclusions keep the coupling law general within the stated moment class Talagrand 1995, Theorem 12.1 and Eqs. (12.7)–(12.8).
The result is proved in the cited paper; the open work here is its Lean formalization. A completed development would connect product-measure concentration, finite spin sums, exponential-moment bounds, and real-valued expectations in one reusable interface. The coupling product space and median conventions can also serve other finite random-interaction models. No machine-checked proof of this chapter's target is claimed by this proposal.
A direct bounded-differences estimate cannot be applied to this model as stated: the couplings are real and may be unbounded. An estimate that handles each coordinate must account for the law's exponential moments while still retaining the and factors in the chapter's explicit bounds. The normalization by makes a single coupling's influence small, but there are couplings, so treating the total sensitivity as dimension-free would lose the scale of the theorem. The first moment alone also does not control the lower tail of ; this is why the second-moment target is present Talagrand 1995, pp. 192–195.
Lean indexes sites by Fin N and interactions by pairs with . A spin is a Boolean choice interpreted as or , and the configuration sum is normalized by . The coupling array is a function on the pair type, carrying the finite product measure of the common law . The theorem uses , , and exactly the common-law moment assumptions above; the median deviation milestone uses because its denominator contains . The main theorem places its single universal before every size, temperature, law, and deviation level.
Expectations are Bochner integrals, so integrability is explicit in the law predicates or in each conclusion that needs it. Probability expressions are real values of measurable events under the product measure. This avoids relying on Lean's default value for a nonintegrable integral. The model retains the entire real coupling law and does not replace it with a finite alphabet or a Gaussian special case. The partition function is built from the couplings and spins, rather than supplied as an unconstrained variable.
The source's displayed (12.5) omits , whereas the derivation following (12.6) gives, for each tail separately, the range and the exponent with the factor . The formal milestone states exactly these two one-sided bounds, while its milestone text preserves the printed display verbatim. The first- and second-moment displays are kept with an absolute constant; the second-moment target uses the proof's range, since for smaller sizes the chapter's interaction-law assumptions do not ensure that is integrable. Integrability of is a conclusion of the main theorem, never a hypothesis, and the median is quantified universally, so neither the expectation in (12.4) nor the deviation bound can hold by a default value of an undefined integral or by an unsatisfiable hypothesis; the Rademacher law satisfies every assumption. Reusable contributions include integrability and measurability of and , product-law estimates, and the source's numbered inequalities.
Concentration of measure on the symmetric group concerns random permutations. A uniformly random permutation of objects appears in random assignment problems, in sampling without replacement, in the longest increasing subsequence and in the analysis of randomized algorithms. A tail bound for a function of a random permutation is useful when it does not require computing the function's distribution. The symmetric group is not a product space, so the inequalities proved for product spaces do not apply to it directly.
Timeline. B. Maurey [Maurey 1979] gave the first concentration inequality on , for distances that count the coordinates in which two permutations differ. Every permutation can be written uniquely as with , where is the transposition of and . Through this decomposition the Hamming bound (2.1.3) for product spaces carries over to . Milman and Schechtman present the result in their monograph [Milman–Schechtman 1986]. In Chapter 5 of his 1995 memoir Talagrand 1995, M. Talagrand proves the analogue on of his convex hull inequality (Theorem 4.1.1 of the memoir). In the author's words, it improves Maurey's result in the way that Theorem 4.1.1 improves Proposition 2.1.1.
is the group of permutations of and is the uniform probability on it. Fix and . A 0–1 vector is admissible if some agrees with at every coordinate where is zero:
is the convex hull of , and
is the squared convex distance from to . Unlike of Chapter 4, here is already squared. If , then and . A permutation that agrees with some element of outside coordinates has .
The proof uses three variants. counts coordinate twice, . , for , restricts that infimum to the face (Eq. (5.5)). drops coordinates and (Eq. (5.6)). In , and , with uniform probabilities and . is the transposition of and . The maps and send and , respectively, onto the permutations fixing , that is, onto .
For every and every ,
The constant is the paper's.
For every and every ,
Since , this pair implies Theorem 5.1.
The milestones are the numbered results of the induction step from to , in the order of the paper:
The result. Theorem 5.1 has the same form as Theorem 4.1.1. By Markov's inequality, . Any function on that is controlled by the convex distance therefore concentrates around its median with Gaussian tails whose scale does not depend on . Because the convex distance weighs coordinates by an arbitrary unit vector, this includes functions that are Lipschitz only in a weighted, configuration-dependent sense, which a Hamming-distance bound does not reach. This is the setting of random permutation problems such as the longest increasing subsequence and the assignment problem.
Formalizing it. The result has been proved since 1995. To the best of current knowledge none of Chapter 5 has a machine-checked proof, and the platform has no concentration statement on . This mission formalizes the statements and the induction of the chapter. Its reusable output is the convex distance on and the embedding of into through the blocks , .
sits inside through . If were the whole product, (5.2) would follow from Theorem 4.1.1. But is a very small subset of that product, and the uniform measure on is not a product measure. The decomposition into transpositions does give a product structure, but it is highly non-commutative. Coordinate distances in the decomposition do not match coordinate distances of the permutations, so it transfers only the weaker Hamming-type bound. The paper notes that a direct induction on for (5.2) itself apparently fails. The strengthened pair , is needed, and its two halves cross: is proved from , and from .
Equiv.Perm (Fin N), with indices from . In the point is Fin.last N, and composition is the group product, so is ρ * t N i.convexHull ℝ. The functionals , , and are infima of explicit sums of squares, so the sup norm on Fin N → ℝ plays no role. They take values in , so an empty infimum is and . The integrand is computed in EReal, so .ℝ≥0∞, so gives on both sides.Restricts ρ τ ( for ). and are the corresponding image sets.Contributions are welcome at every level: proofs of the deterministic lemmas, the bijections and their measure-transport facts, and the final Hölder–Lemma 4.1.3 step.
Constrained convex programs are routinely solved by turning them into a sequence of unconstrained problems. The classical route is the ordinary Lagrangian , whose dual function is in general nonsmooth and equal to off the orthant , so maximizing it requires a constrained, nonsmooth method. In 1969 Hestenes (JOTA 4, 1969) and Powell (in Optimization, ed. Fletcher, Academic Press, 1969) proposed the method of multipliers for equality constraints, which adds a quadratic penalty to the Lagrangian. Rockafellar's paper (Math. Programming 5, 1973) gives the inequality-constrained version, the penalty Lagrangian , and shows that for convex programs its dual is a smooth, unconstrained, concave maximization problem with the same solutions and value as the ordinary dual. The method of multipliers built on this Lagrangian, now called the augmented Lagrangian method, underlies ADMM and many large-scale solvers.
Timeline. Hestenes and Powell (1969): multiplier method for equality constraints. Rockafellar (1973, this paper; and JOTA 12, 1973): the inequality-constrained penalty Lagrangian, its duality theory, and convergence of the multiplier method for convex programs. Rockafellar (Math. Oper. Res. 1, 1976): the method of multipliers identified as the proximal point algorithm applied to the dual. Bertsekas (Constrained Optimization and Lagrange Multiplier Methods, 1982): the general nonconvex theory.
This mission covers the first half of the paper: the duality theory of (§3) and the theorem that maximizing the penalty dual yields asymptotically optimal primal sequences (§4, Theorem 4.1).
Let be a nonempty convex subset of a real vector space and convex real functions on . The problem is
Multipliers range over , with Euclidean norm and inner product . With and a parameter , the penalty Lagrangian is
defined for all with no sign restriction. The dual function is , and the dual problem maximizes over ; and are the same with , and is the dual optimal value. In Lean these objects are Lr, L0, gr, g0, dualValue, and Fr is the perturbed objective if , otherwise.
A sequence in is asymptotically feasible if for every . The asymptotic optimal value (asympValue) is the infimum of over asymptotically feasible sequences, and a sequence attaining it is asymptotically minimizing (IsAsympMinimizing). A maximizing sequence for is a sequence with .
Suppose the asymptotic optimal value in (P) is finite, , is a bounded maximizing sequence for , and satisfies
Then is asymptotically minimizing for (P).
Theorem 4.1 says that any procedure that drives the smooth, unconstrained dual to its supremum, while computing -minimizers only approximately, produces an asymptotically optimal primal sequence. It needs no constraint qualification, no existence of a dual or primal optimal solution, and not even feasibility of (P): only that the asymptotic optimal value is finite. Together with Theorem 3.2 it justifies the multiplier method as a dual ascent on a concave function with Lipschitz gradient, and it is the starting point of the convergence theory of augmented Lagrangian methods.
None of these statements is formalized on Prove2Me or in Mathlib, which has Lagrangian duality only in special forms and no theory of the penalty Lagrangian or of asymptotic optimal values. The Qi–Sun augmented Lagrangian items on the platform (NonsmoothNewton.AugLagrangian.*) use the -scaled function on and concern smoothness in , not the dual function. The results of this paper are classical and proved; this mission formalizes them.
The obvious argument compares the primal iterates with a saddle point: if is a dual optimal solution and (P) is normal, approximate minimizers of are approximately optimal. Theorem 4.1 assumes neither. The function need not attain its supremum, (P) need not be normal or even feasible, and there may be no Kuhn–Tucker vector, so there is no saddle point to compare with; the only data are the dual values , the boundedness of and the tolerances . The difficulty is to obtain primal feasibility and optimality information from dual convergence alone, measured against the asymptotic optimal value rather than the infimum in (P). Every ingredient is extended-real-valued: is off the orthant, may be identically , and the asymptotic optimal value may be . Mathlib does not package this part of convex analysis (partial conjugates, envelopes of extended-real concave functions, the asymptotic duality theorem).
is a bare real vector space (AddCommGroup E, Module ℝ E) with no topology, as in the paper. The functions are total functions assumed convex on ; only their values on enter. Constraint indices are Fin m (0-based) and is a separate argument. Multipliers live in EuclideanSpace ℝ (Fin m). The standing assumption of §3 ( nonempty convex, all convex) is a hypothesis of every theorem.
Explicit choices:
EReal, so are represented and no infimum is replaced by a junk real value.EReal, equivalent to the printed difference; only is assumed.The goal must not be replaced by " and ": that is the special case of normal problems with feasible solutions. Nor may it assume a Slater point, a Kuhn–Tucker vector, or feasibility of (P), each of which makes it a special case.
A complete development needs extended-real convex analysis on (partial conjugates, Moreau envelopes of concave functions, the asymptotic duality theorem), which is reusable beyond this mission. Contributions proving any milestone, or general lemmas on Moreau envelopes of extended-real concave functions, are welcome.
Concentration of measure is the observation that, on a high-dimensional product probability space, any set that is not too small already contains most of the space within a small neighbourhood. For functions of many independent random variables this yields Gaussian-type tail bounds without any explicit computation of the distribution, and these bounds are the working tool behind the analysis of random combinatorial optimisation problems (bin packing, the travelling salesman problem, the longest increasing subsequence, the assignment problem), random graphs, and empirical processes.
M. Talagrand's 1995 memoir Talagrand 1995 develops a family of such inequalities that hold on an arbitrary product of probability spaces and are proved by induction on the number of coordinates. Chapter 2 opens with the simplest instance, control by one point: the distance from to a set is measured by the number of coordinates in which differs from the best single point . The method of this chapter is the template for every later chapter of the memoir.
Timeline. Bounds of the form (2.2.7) for the Hamming distance were first obtained with martingale (bounded differences) methods, collected in McDiarmid's survey McDiarmid 1989. Talagrand's 1995 memoir gives the induction proof reproduced here, with exponent , which the paper notes is exactly the best bound obtained by martingales. Earlier, the isoperimetric inequality on the discrete cube (Harper, 1966) settles the case of the uniform measure on .
Let be a probability space and an integer. Points of the product are written , and denotes the product probability. For a set and a point , the Hamming distance to is
the least number of coordinates that must be changed to move into ; it is when is empty. Given positive weights , the weighted Hamming distance replaces the count by .
Two families of constants appear. The first is
and the second, for and ,
extended by its limit ; one checks .
For every measurable , every and every ,
and, when , for every ,
The goal is the weakest statement of the section that is stated with fully explicit, closed-form constants; the milestones are the steps the paper's proof passes through.
The result. Inequality (2.2.7) shows that if is bounded below, the set of points at Hamming distance at least from has probability at most , with no assumption on or . Applied to for a function that changes by at most one when a coordinate changes, it gives concentration of around its median at scale . The exponential moment bound (2.2.6) is the form that composes with other estimates, and the free parameter is what makes the constant in (2.2.7) attainable rather than as in (2.1.3).
Formalizing it. The results are classical and fully proved in the paper; they are not available in Mathlib, and no machine-checked proof of them is known. A formalization supplies the one-coordinate inequalities (Lemma 2.1.2 and its -version) and the induction over as reusable components: every later chapter of the memoir (two-point space, penalties, points, convex hull distance) follows the same induction with a different one-coordinate lemma.
The bound does not follow from a union bound or from independence of coordinates, because depends on all coordinates jointly through an arbitrary set : changing one coordinate of changes by at most one, but which point of is nearest can change completely. A naive coordinate-by-coordinate estimate loses either the dependence on or a constant factor in the exponent, and the constant in (2.2.7) is the sharp one, so no slack is available. The one-dimensional inequalities (Lemma 2.1.2 and its -version) are extremal problems over all measurable functions rather than over numbers, and Lemma 2.2.2 is a two-parameter inequality in which the closed form (2.2.2) is not convenient. On the measure-theoretic side, all integrands take values in and need not be measurable in general.
Fin N → Ω (0-based coordinates) and is Measure.pi (fun _ => μ). is never restricted to a finite or countable set.MeasurableSet A and the map carries an explicit Measurable hypothesis; probabilities of arbitrary sets are Mathlib's outer measure.ℝ≥0∞), so ; integrals are lower Lebesgue integrals ∫⁻ in ; is EReal.exp; and are computed in , so makes the right-hand sides .Needed infrastructure: Fubini/Tonelli for Measure.pi split as , Chebyshev–Markov for ∫⁻, and one-variable calculus for (2.2.3)–(2.2.5). The one-coordinate lemmas and the induction scheme are reusable in the later missions of this series. Proofs of individual milestones and alternative proofs (for example via martingales for (2.2.7)) are welcome.
A recurring phenomenon in probability is concentration of measure: on a product of many probability spaces, a set of non-negligible measure has a neighbourhood that carries almost all of the mass. M. Talagrand's 1995 memoir Concentration of measure and isoperimetric inequalities in product spaces developed a systematic method — induction over the number of coordinates — that yields such statements for several different ways of measuring "how far" a point is from a set. These inequalities underlie sharp tail bounds for combinatorial optimization problems (bin packing, travelling salesman, longest increasing subsequence), for empirical processes, and for spin glasses, and Part II of the memoir develops several of these applications.
This mission formalizes Section 3 of the memoir, Control by q points. In Section 2 the distance from a point to a set counts the coordinates of that a single point of fails to reproduce (the Hamming distance). Section 3 lets several points cooperate: a coordinate of is captured if any one of chosen points agrees with there. The memoir's introduction (p. 79) presents Theorem 3.1.1 as a much simpler substitute for the isoperimetric inequality of Talagrand's earlier work on sums of independent Banach-space valued random variables (Talagrand, Ann. Probab. 17 (1989), 1546–1570), whose phenomenon "had a major impact in Probability in Banach spaces"; Chapter 13 of the memoir applies it to tails of such sums.
Let be a probability space, an integer, and the product probability on . Fix an integer ; this is a standing assumption throughout the section. For and points , coordinate of is captured if . For subsets the -point control is
the least number of coordinates of that remain uncaptured when one point is chosen in each . It is a whole number between and , or when some is empty.
For the sharpening of Section 3.2, given , the number is the unique with
For all subsets of ,
and in particular, for and ,
The constant is exact: the base of the exponential moment is itself, and the dimension does not appear.
Theorem 3.1.1 gives an exponential tail for whose rate is independent of the dimension and of the space . Applied with a set of probability at least , it says that outside an event of probability a random point agrees, on all but coordinates, with one of points of . This is the form in which the memoir (Chapter 13) bounds the tail of for independent Banach-space valued : taking , on most of the space the sum is controlled by points of up to the largest terms. Proposition 3.2.1 shows the base can be improved from to order for large , and the memoir's example on shows that this is sharp up to a universal constant in the base.
None of these results has a machine-checked proof. A formalization produces reusable Lean infrastructure for the induction method on product measures (sections and projections of subsets of , Fubini on Measure.pi, one-coordinate functional inequalities) that the other chapters of the memoir — the Hamming distance of Section 2, penalties of Section 3.3, the convex hull distance of Section 4 — share.
The inequality cannot be obtained by a union bound over choices of points or by a coordinate-wise martingale argument with bounded differences: both lose a factor depending on , while (3.1.2) has none. The induction on needs a functional inequality on one coordinate that holds uniformly over functions at once, with the exact constant , and the induction step has to pass through the projections of the sets — which, for measurable , need not be measurable. The exact constant in Proposition 3.2.1 additionally requires quantitative control of the root of (3.2.2) as .
Fin N → Ω (coordinates ), is Measure.pi (fun _ => μ) with [IsProbabilityMeasure μ], and is Fin.snoc x ω.ℕ∞, so an empty gives , not ; ; integrals are ∫⁻ and probabilities are in ℝ≥0∞, where . Hence the degenerate case makes the right sides infinite and cannot trivialize any statement.A complete development needs the induction step over Measure.pi on Fin (N+1) (splitting off the last coordinate), measurability of sections, and the one-coordinate inequalities. Proofs of any milestone are welcome, as are alternative proofs of the goal.
Concentration of measure in a product space asks how much of the space lies close to a set of non-negligible probability. In the simplest setting closeness is the Hamming distance: the number of coordinates of that cannot be matched by a point of . Talagrand's 1995 memoir in Publications Mathématiques de l'IHÉS develops a family of such inequalities with one method, induction over the number of coordinates, and applies them to combinatorial optimization, random graphs, spin glasses and sums of Banach-space-valued random vectors.
Counting a missed coordinate as ignores how far apart the two coordinate values are. Sections 2.4 and 2.5 of the memoir replace the unit cost by a penalty that depends on the values being matched. The resulting bounds have the shape of Bernstein's inequality: a Gaussian tail for moderate deviations, governed by the size of the penalty, and an exponential tail for large ones, governed by its sup norm. Theorem 2.4.1 is used again in Chapter 11 of the memoir, Corollary 2.4.4 in the study of the Sherrington–Kirkpatrick model in Chapter 12, and Theorem 2.5.1 in Section 11.5.
Let be a probability space, an integer, and the product probability on . A penalty is a measurable function with for every (the paper's standing assumption (2.4.2)). For and the penalized distance is
with . For off the diagonal this is the Hamming distance. Theorem 2.4.1 also uses the symmetrized penalty .
Section 2.5 measures the penalty against sets: for ,
the infimum being over the second variable, as in . The one-coordinate steps of the two inductions use the transforms (2.4.5) and with (2.5.7), for a function on .
For each measurable and each with ,
It is the most general exponential-moment bound of the section; every tail bound of Section 2.4 is derived from it.
The results. Theorem 2.4.1 turns a single integrability condition on the penalty into a bound on the exponential moment of the distance to any set, uniform over all sets of a given probability and factorized over coordinates. Chebyshev's inequality then gives the Bernstein-type tails of Corollaries 2.4.4 and 2.4.5, which hold for every set , not only for half-spaces or for sums of independent variables. Theorem 2.5.1 replaces exponential integrability of by condition (2.5.2) on the set functional , which is much weaker: when is itself a product of spaces, times the Hamming distance on satisfies (2.5.2) but not (2.4.12). Applied to blocks of coordinates, it shows that the coordinates a typical point misses in are concentrated in few blocks.
Formalizing them. All six results are proved in the memoir with short arguments. None of them has a machine-checked proof. A complete development would give a general-alphabet version of Talagrand's induction on product measures, written once for a cost function, that later chapters (the -point control, the convex-hull distance) also rely on.
The induction over requires a one-coordinate inequality whose right-hand side does not depend on the set. The difficulty is that the natural one-coordinate quantity, a section measure , can vanish on part of , so the function takes the value , and a statement proved for finite must be extended by truncation. The other subtle point is measure theoretic: need not be measurable even when is, and the paper's convention of ignoring measurability has to be matched by explicit hypotheses. In Section 2.5 the integrand in condition (2.5.2) may be non-measurable for the sets the proof uses, and Fubini's theorem is applied to the function .
Points of are functions Fin N → Ω (coordinates indexed from ), is Measure.pi (fun _ => μ) for a probability measure μ, and double integrals are over μ.prod μ. The penalty is a real function h : Ω → Ω → ℝ with explicit hypotheses , and joint measurability, in every statement. The distance is defined by (2.4.1) with the indicator and takes values in , so ; likewise and the transform (2.5.7). All integrals are Lebesgue integrals of -valued functions, , and when .
Measurability follows the paper's convention (pp. 81–82) as explicit hypotheses: is measurable and is measurable; in the propositions, and are measurable. Condition (2.5.2) is stated for every subset with the upper integral , which the paper prescribes when measurability fails. In Corollary 2.4.5, the quotients are computed in , so a quotient by , or is when its numerator is positive. The bound is when , as the printed factor intends. No statement is restricted to a finite or countable : restricting it would turn the general theorems into their finite-alphabet special cases. Dropping or defining the distance by a real infimum (whose value on the empty set is ) would change the theorems and is ruled out.
A complete development needs product measures on Fin (N+1) → Ω split as , sections of measurable sets, Tonelli's theorem, and the elementary convexity inequalities used in the proofs; the induction scaffold is reusable for the other distance functionals of the memoir. Proofs of any milestone are welcome, as are proofs of the extension of Proposition 2.4.2 to with values in , which the paper states without number on p. 92.
Processors in a distributed system may hold separate readings of a sensor, clock, or diagnostic result while some processors give misleading reports. The aim of interactive consistency is for every functioning processor to compute the same vector of reported values and to put each functioning processor's actual private value in its corresponding position. A shared vector can then be used for a common decision. Pease, Shostak, and Lamport formulated this problem for isolated processors communicating by two-party messages; their paper discusses clock synchronization, input stabilization, and diagnostic tests as concrete applications Pease–Shostak–Lamport 1980.
In the paper's oral-message model, faulty processors can invent reports about values they received from others. The other two missions in this series formalize the recursive majority procedure for and the matching impossibility result below that bound. Section 5 changes the communication assumption: a faulty processor may refuse to pass on a received value but cannot pass on an altered value as if it came from its original sender. Under that assumption, the authors give a procedure for every , including configurations outside the oral-message threshold Pease–Shostak–Lamport 1980, §§3–5.
Let be a finite set of processors and a type of private values. Each processor has a value . A scenario records the values reported along chains of processors. A string is read from receiver to originator: receives a report ultimately attributed to . A recorded value may be NIL, meaning that no authenticated value is available. The view available to receiver is its -scenario, the restriction ; it contains no report that begins with a different receiver.
Choose a set of nonfaulty processors. At most processors may be faulty, expressed as . An authenticated scenario consistent with obeys two conditions whenever the displayed strings are in the -level scenario. If and , the report made by nonfaulty relay is truthful: . For any prefix , a chain passing through nonfaulty carries either the value at or NIL: . The second condition allows omission by later relays while excluding a changed value falsely attributed to Pease–Shostak–Lamport 1980, p. 233.
For each receiver and originator , the procedure forms , the set of all non-NIL values in 's view on strings . The intermediate string has at most distinct letters, all in . Receiver records the sole value in when this set is a singleton; otherwise it records NIL. The resulting entries, one for each , form 's proposed consistency vector Pease–Shostak–Lamport 1980, p. 233.
The first milestone covers a nonfaulty originator : every nonfaulty receiver sees exactly its true value. The second covers a faulty originator: the set of non-NIL values seen by one nonfaulty receiver is contained in the set seen by another. The same statement with the receivers exchanged gives equality of their sets.
The goal is the procedure's full interactive-consistency guarantee, for every choice of and every authenticated scenario satisfying the conditions above:
Here is the optional value recorded by processor for processor . Both clauses matter: agreement alone could be achieved by always recording NIL, while correct nonfaulty entries alone would leave faulty entries inconsistent.
The result identifies an exact communication assumption under which the paper's oral-message bound no longer governs the procedure. Even if a faulty originator gives conflicting values, nonfaulty receivers finish with identical entries for that originator; if an originator is nonfaulty, they retain its actual value. The paper describes authenticators as a practical approximation to the assumption, but the guarantee here is a mathematical statement about scenarios satisfying its two conditions, not a probability claim about a cryptographic implementation Pease–Shostak–Lamport 1980, §5.
Formalizing this result supplies precise interfaces for authenticated scenario consistency, local views, the set , and the recording rule. The paper proves the result on pp. 233–234; this mission asks for a machine-checked proof of those statements in Lean. The scenario and local-view definitions can support later formalizations of message-passing protocols with truthful or omissible relays. Contributions that establish the two source milestones and the final guarantee, or develop reusable list and finite-set facts needed by them, are within scope.
The case of a faulty originator is the central difficulty. Its private value has no required relationship to what different nonfaulty receivers hear, so simply asserting that every receiver obtains the same direct report is unjustified. A faulty relay may also omit a report, which makes equality of raw scenario entries too strong. The target must compare sets of non-NIL values obtained along admissible relay chains. At the longest allowed chain, the length bound prevents adding another relay, and the number of faulty processors is needed to establish that an admissible nonfaulty relay occurs in the chain Pease–Shostak–Lamport 1980, p. 234.
Lean represents processors by a finite set P : Finset α, values by a type V, strings by List α, and NIL by none : Option V. A scenario is a total function from strings to optional values. Only strings over of length at most are constrained by authenticated consistency, matching the -level scenario that the procedure reads. A single-letter string has a non-NIL private value for every processor in . Conditions (i) and (ii) constrain nonfaulty relays only; condition (ii) allows either the original value or NIL for every prefix over , including an empty prefix.
The procedure is applied only to 's view , so it has no access to the full scenario or to . Its intermediate strings are repetition-free, exclude both and , and have length at most . The set contains values in , not NIL; an empty set and a set with multiple values both cause a NIL record. The formal theorem retains the printed condition, although it is not needed in the proof of the stated set relationships. It also covers , , and empty or singleton processor sets when their quantified conditions apply. These conventions rule out an always-NIL decision rule and the trivial rule that reads from outside the receiver's view.
The cryptographic maps , their message encodings, and the paper's assertion that practical authenticators can meet the assumption with arbitrarily high probability are outside scope. The formal result assumes the two exact authenticated-scenario conditions. A complete development needs finite-set cardinality and list facts, especially about distinct relay strings and bounded concatenation; these facts can be reused for other authenticated relay models.
A fault-tolerant system built from several processors must let its working processors act on the same data, even though some processors may have failed in ways nobody can predict: a failed processor may stop relaying information, relay something it invented, or tell different processors different things. Pease, Shostak and Lamport (J. ACM 27 (1980) 228–234) isolated the core question in the setting of the SIFT aircraft-control computer: each of processors holds a private value, at most processors are faulty, and processors communicate only by two-party messages. Can the nonfaulty processors each compute a vector of values, one entry per processor, such that all nonfaulty processors compute the same vector and the entry of each nonfaulty processor is its true private value? This requirement is called interactive consistency.
The paper answers with a sharp threshold. Interactive consistency can be achieved when (Section 3), and it cannot be achieved when , however many rounds of message exchange are allowed (Section 4). With unforgeable signatures it can be achieved for every (Section 5). The impossibility half is the origin of the "" bound that appears throughout Byzantine fault tolerance, popularised two years later as the Byzantine Generals Problem (Lamport, Shostak, Pease, ACM TOPLAS 4 (1982)). This mission is the impossibility theorem.
Timeline:
Let be a finite set of processors and a set of values. Write for the set of strings over (the empty string included) and for the nonempty strings. A string is read as a chain of reports: was told by that was told by that 's private value is the recorded value.
A scenario is a map . The value is processor 's private value, and is the value received for the chain . For , the -scenario is the restriction of to the strings beginning with : everything ever learns.
For a set of nonfaulty processors, is consistent with if
that is, every nonfaulty processor reports truthfully what it knows or hears. Faulty processors are unconstrained.
A decision family assigns to each a map that takes a -scenario and a processor and returns a value : the entry computes for . The family assures interactive consistency for faults if for every with and every scenario consistent with ,
In the Lean development these are InteractiveConsistency.Impossibility.ConsistentWith P N σ and AssuresIC P m F, with restrict σ p the -scenario.
If and
then no family assures interactive consistency for faults. Since scenarios are defined on strings of every length, no bound on the number of rounds is assumed.
The theorem shows that the algorithm of Section 3 is optimal in its fault tolerance: with oral messages, processors are not only sufficient but necessary. Every later lower bound for Byzantine agreement, Byzantine broadcast and approximate agreement with unauthenticated messages rests on this bound or a variant of its argument, and it is the reason replicated state machines tolerating Byzantine faults use replicas. It also explains why Section 5 needs authentication: the argument depends on faulty processors being able to relay fabricated values.
The result has been proved since 1980; what is open here is its formalization. Nothing on Prove2Me models message-passing agreement, and this mission states the theorem in the paper's own model: scenarios on unbounded strings and decision functions of a single -scenario. The mission produces a reusable vocabulary (scenarios, consistency, interactive consistency) and the explicit three-scenario construction.
The obvious attempt is to argue round by round about what a processor can know after rounds; with unboundedly many rounds this never terminates in a contradiction. The paper's argument instead needs three entire scenarios, each a legitimate behaviour for a different set of faulty processors, that two processors cannot tell apart from their own views. Writing these scenarios down so that consistency holds on every string while the indistinguishability survives on every string is the delicate part: the faulty set of each scenario must relay exactly the values that keep the other scenario's view intact, and one of the defining equations () looks like a misprint but is what the argument requires. The counting step is elementary but carries the hypothesis that the printed theorem leaves implicit.
Processors are a Finset P in a type with decidable equality; strings are lists read left to right ( is the head of the list); a scenario is a total function List α → V whose values on the empty list and on lists with a letter outside carry no meaning: every condition quantifies only over strings whose letters lie in . Decision functions have type α → (List α → V) → α → V and are applied only to the -scenario fun w => σ (p :: w), never to ; giving the whole scenario would make the problem trivial (output ). Consistency with constrains only relays by members of , and includes the empty . The quorum is written , which avoids truncated subtraction on . is the existence of two distinct values.
Explicit readings of the page:
A complete development needs only finite sets and lists from Mathlib. The vocabulary of p. 232 is shared with the other two missions of this series, Reaching Agreement in the Presence of Faults 1 (the algorithm for ) and 3 (authenticated messages, ), each of which defines it in its own namespace. Proofs of the milestones and of the goal are welcome, as is a proof of the goal by a different route.
A finite two-person zero-sum game is given by a real pay-off matrix, and its value can be computed by linear programming. In 1949 George W. Brown proposed a much simpler procedure, now called fictitious play: each player in turn plays a best pure reply to the accumulated play of the opponent so far, and the running averages are read off as estimates of the value (Brown, RAND P-78, 1949). Brown conjectured that both estimates converge to the value. Julia Robinson proved the conjecture in An Iterative Method of Solving a Game, Annals of Mathematics 54 (1951).
The result is the starting point of the theory of learning in games. Fictitious play is the basic model of boundedly rational players who best-respond to empirical frequencies, and the question "for which classes of games does it converge?" has driven a long line of work.
Timeline.
Let be a real matrix, . The first player chooses a row , the second a column , and the second pays the first . A mixed strategy is a probability vector for the first player, or for the second. For all mixed strategies,
A pair for which equality holds is a solution, and the common number is the value of the game. The minimax theorem says that a solution exists.
Write for the -th row, for the -th column, and , for the largest and smallest component of a vector . A vector system for is a pair of sequences of -vectors and of -vectors with and
where and . In the alternate vector system the column satisfies instead. A row is eligible in the interval if for some , and similarly a column if for some .
With , is the payoff vector of the first player's empirical mixed strategy against each column, and that of the second player's against each row. In the Lean development these objects are vmax, vmin, IsVectorSystem, IsAltVectorSystem, RowEligible, ColEligible and IsSolution, in the namespace RobinsonFP.Convergence.
For every vector system for , and the value of the game,
The statement holds for arbitrary initial vectors with and for every way of breaking ties.
Two further items are not milestones: the Theorem for the alternate vector system, which the paper says follows by the same proofs, and the bracketing when (p. 297).
The Theorem shows that a payoff-based procedure with no linear algebra finds the value of every zero-sum matrix game. It was one of the first iterative methods for linear programs with a convergence proof, and it is the base case for every later convergence result about fictitious play: potential games, games with identical interests, games, and continuous-time best-response dynamics.
The result is proved, and its proof is short. To our knowledge it has no machine-checked proof. The mission produces a Lean proof of the Theorem and its four lemmas, together with reusable definitions of vector systems and eligibility. A statement with an explicit rate, such as Shapiro's, or a proof for the alternate system, is a natural extension.
Lemmas 1–3 are elementary estimates. The difficulty is Lemma 4. The obvious approach follows a single run of the iteration and tries to show that the gap grows sublinearly. This fails because a run can spend arbitrarily long windows in which some row or column is never a best reply, and nothing about one fixed run controls the gap over such a window. What is needed is a bound that is uniform over all vector systems, whatever their initial vectors and tie-breaking, which is why in Lemma 4 comes before the vector system, and why display (3) quantifies over every vector system of the smaller matrices. In Lean, this uniformity has to range over matrices of every smaller size, so the statements must be general in the index types.
ι, κ (the paper's ); Fin m, Fin n is a special case. The matrix is Matrix ι κ ℝ.Finset.sup' and Finset.inf' over all indices, hence attained.Tendsto … atTop (𝓝 ·); lim inf and lim sup of real sequences are stated in -form (for every , eventually), with no boundedness side conditions.IsSolution A x y v, i.e. probability vectors , with . Such a solution exists by the minimax theorem, which is proved on the platform as MatousekLP.ZeroSum.minimax_equality in a different encoding. A statement with free, or with "there exists ", would be false or would lose the identification with the value; neither is used.A general "restriction of a vector system to a submatrix" lemma would be reusable for later work on fictitious play. Proofs of any milestone are welcome, as are proofs of the two extra items.
Section 4 of Herbert Robbins's 1952 address Some aspects of the sequential design of experiments (Bull. Amer. Math. Soc. 58, 527–535, doi:10.1090/S0002-9904-1952-09620-8) isolates a problem that every user of significance tests meets: if the sample size is not fixed in advance, an experimenter can keep sampling until the test rejects. Robbins shows that a fixed-sample test then loses all control of its error probability, and he proposes the compromise of allowing the sample size to range over a window , with an explicit bound on the resulting error.
The question is still current. "Optional stopping" and "peeking" at accumulating data are a standard concern in clinical trials and online A/B testing, and the modern theory of always-valid inference and confidence sequences (for example Howard, Ramdas, McAuliffe and Sekhon, Time-uniform, nonparametric, nonasymptotic confidence sequences, Ann. Statist. 49 (2021), arXiv:1810.08240) answers exactly the question Robbins raises: how large is the probability that a running statistic crosses a boundary at some time in a range. The earlier treatment Robbins cites is Feller's 1940 discussion of the statistics of ESP experiments.
Let be independent real random variables on a probability space , each normal with mean and variance . This is the null hypothesis for observations that are normal with unknown mean and unit variance; the alternative is . Write
The fixed-sample test of size rejects if and only if
for a real constant . (In this mission always denotes this test constant; in Section 2 of the paper the same letter is the mean of a coin.) The standard normal distribution function is
For integers the window probability is
and . In Lean these are Phi, S X n ω = ∑ i ∈ Finset.range n, X i ω and g P X n₁ n₂ α, in the namespace RobbinsSeqDesign.OptionalStopping.
For integers and every real , with ,
The inequality is strict, as printed, and holds for every real , not only the large values of practical interest.
For every and real ,
For every real , with probability the inequality holds for infinitely many .
The results. (22) says that the fixed-sample test has error probability whatever is. The infinitely-often statement says that this guarantee is void under unrestricted optional stopping: sampling until (21) holds rejects a true with probability one, however large is. The goal (25) quantifies the compromise: if the stopping time is confined to , the error probability is at most the fixed-sample error divided by , where depends only on the window's ratio. For large and moderate this keeps the error of the same order as the fixed-sample error; Robbins notes that it is useful when is not too large and that sharper inequalities can be devised.
Formalizing it. The three statements are classical and their proofs are short on paper, but none is machine-checked for Gaussian partial sums. The goal needs stopping-time machinery for discrete-time Gaussian random walks; the infinitely-often statement is a consequence of the lower half of the law of the iterated logarithm, which Mathlib does not contain. On the platform, DurrettProbability.brownian_limsup_sqrt (proved) gives for Brownian motion, a different process, and AzumaWeightedSums.IteratedLog.theorem2_limsup_le_one gives an upper iterated-logarithm bound for weighted sums, the opposite direction; neither states any of the targets here, but both are related infrastructure.
The goal is a maximal inequality over a window of times. The obvious argument, a union bound over , gives , which grows with the window length instead of depending on alone, and exceeds for long windows. The events for different are strongly dependent, and the boundary is curved, so the bound has to account for when, inside the window, the boundary is first crossed; this requires stopping-time arguments for a discrete-time walk that are not yet available for Gaussian random walks in Mathlib. The strictness of the inequality also has to be tracked through the argument. The infinitely-often statement cannot be obtained from the central limit theorem alone, which gives only ; upgrading this to probability one needs a zero–one law or the law of the iterated logarithm.
The observations are X : ℕ → Ω → ℝ on a probability space (Ω, P) with [IsProbabilityMeasure P], iIndepFun X P and ∀ i, HasLaw (X i) (gaussianReal 0 1) P; the paper's is X (i - 1). The explicit readings committed to are:
cdf (gaussianReal 0 1)).P.real of the event; (22) is stated for .∀ᵐ ω ∂P, ∃ᶠ n in atTop, α * √n < S X n ω, for every real .A trivializing formalization is ruled out: is the probability of the union over the whole window (not the event at alone), is the fixed standard normal distribution function (not an arbitrary monotone function), and the parameter range excludes , where Lean's convention would replace the right side by .
A complete development needs the law of a sum of independent Gaussians, the strong Markov property of a Gaussian random walk at a stopping time (or an equivalent first-passage decomposition), and, for the infinitely-often milestone, either the lower law of the iterated logarithm for Gaussian walks or the Hewitt–Savage/Kolmogorov zero–one law combined with the central limit theorem. These pieces are reusable well beyond this mission; contributions of any of them, as separate lemmas, are welcome.
A linear program subject to , assumes that the constraint matrix is known exactly. In practice the columns of — the activity vectors, describing how much of each resource one unit of activity consumes — are estimates. A. L. Soyster's 1973 technical note in Operations Research (doi:10.1287/opre.21.5.1154) asked what a decision should satisfy if every activity vector is known only to lie in a given convex set, and the decision has to be feasible for every possible realisation. He called this inexact linear programming, a term he attributes to K. O. Kortanek.
The note is the earliest formulation of what is now called robust linear optimization. Its answer — replace each uncertain column by its coordinatewise worst case — is the "Soyster model" that later work on robust optimization takes as its point of departure: Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Math. Program. 2000) and Bertsimas and Sim (Oper. Res. 2004) both introduce their less conservative uncertainty sets as alternatives to it.
Fix integers . Vectors in are compared componentwise. For a set and a scalar , , and the sum of sets is Minkowski addition, .
Let be nonempty convex activity sets and a nonempty convex resource set. Problem (I) is
and denotes its set of feasible . Problem (Ib) is the special case for a right-hand side .
The support functional of a set is , a value in . With the -th unit vector, the auxiliary matrix is the matrix with entries
defined when all of these are finite, and LP is the linear program subject to , . Finally is the set of matrices whose -th column lies in .
In the application, the activity sets are Euclidean balls around nominal columns of a matrix , with radii .
Assume every is nonempty and convex and for all . Then
and for every objective , the optimal solutions of (Ib) and of LP coincide.
The THEOREM turns a semi-infinite constraint — one linear inequality for every matrix in , of which there are typically uncountably many — into a single linear program of the original size, whose data are the support functionals of the activity sets. Any LP solver then solves the uncertain problem. The hypersphere corollary shows the cost of this guarantee concretely: every entry of column is inflated by the full radius , which is why the model is called conservative and why later robust-optimization work introduced ellipsoidal and budgeted uncertainty sets as less conservative alternatives. The LEMMA classifies (I) as a convex program in general, for resource sets that are not half-space intersections.
The results are proved in the paper and are standard. To our knowledge they have no machine-checked proof in Lean or Mathlib. The mission produces a formal statement of the set-inclusive constraint as an actual Minkowski-sum inclusion, the support-functional reduction with its finiteness hypotheses made explicit, and the Euclidean-ball computation — a base that robust-counterpart results for other uncertainty sets can be compared against.
The individual arguments are short; the work is in the bookkeeping that the paper leaves implicit. The step from "for every " to uses that the supremum of a sum of independent terms is the sum of suprema, which needs every nonempty and the scalars nonnegative; with an empty activity set the Minkowski sum is empty and every becomes feasible. The support functional is valued in the extended reals, and its conversion to a real matrix entry is exact only under the finiteness assumption, which the paper secures by deleting columns. The ball computation needs the Euclidean norm and its dual characterisation of the maximum of a coordinate over a ball.
Fin m → ℝ and Fin n → ℝ, with indices in place of ; the order on vectors is componentwise.(∑ j, x j • K j) ⊆ R (pointwise set operations) together with . It is not defined as "for every choice ", which would make milestones 1 and 5 trivial, and is constructed from the , not an arbitrary matrix dominating , which would make the goal trivial.EReal. The entries of are its real conversions, so every statement mentioning assumes and , the paper's standing assumptions (pp. 1154–1156). Convexity of the is also kept as a hypothesis wherever the paper has it, although only the LEMMA uses convexity (of ).EuclideanSpace ℝ (Fin m)), not the sup norm of Fin m → ℝ, with radii .FenchelRobust.Counterpart.supportFun with the same body.EReal statement equating the optimal values, are welcome.An inventory controller must decide how much to order while demand changes with an observed external condition. A single demand rate misses that dependence: the same inventory position can justify different orders when the condition changes. Song and Zipkin's 1993 study asks whether a simple policy remains optimal when the condition follows a continuous-time Markov chain and orders arrive after a random lead time. The answer for linear ordering costs is a world-dependent basestock policy: each world state has one target inventory position, and an order raises the current position to that target when it lies below it.
The policy claim concerns an infinite horizon. It is stronger than showing that a particular collection of target levels performs well or that such a policy minimizes a one-step cost. Theorem 2 of Song and Zipkin identifies the targets through a limiting value function and establishes optimality for the full discounted problem. This mission formalizes that theorem and the finite-stage results the authors use to state its limit precisely.
The world state belongs to a nonempty countable set . The world evolves according to a conservative continuous-time Markov generator , with exit rate . When the world is in state , customers demand individual units at rate . The exit rates and demand rates are bounded above. Inventory is fully backlogged: a negative inventory level records unmet demand. The controller observes the world state and the inventory position , which includes outstanding orders, and chooses an order-up-to position .
An order has actual unit cost and may have fixed cost . This mission takes the linear-cost case, so the discounted fixed cost is . The lead time is a finite nonnegative random time, independent of the world and demand process. Its Laplace transform discounts the ordering costs to , where is the discount rate. Holding one unit costs per unit time; backlogging one unit costs .
Write for the number of demands during the lead time conditional on initial world state . The cost rate of an inventory level is for and otherwise. The lead-time cost and myopic cost are
where is a uniformization rate at least , , and . The paper's Assumption 1, , applies to the later results. It ensures the myopic cost has finite nonnegative minimizers. The smallest such minimizer in world state is , and .
With zero fixed cost and zero terminal cost, the -stage transformed cost minimizes the auxiliary cost over . Each combines the myopic cost with the expected discounted continuation after a demand, a world-state jump, or a self-loop. Let and denote their pointwise limits. A basestock policy orders to in state ; it never cancels an outstanding order.
The main target is the finite, smallest global minimizer of for each world state, with the inequalities of Theorem 2(c):
Here is the limit of the smallest finite-stage minimizers . Theorem 2(e) then asserts that has minimum infinite-horizon expected discounted cost from every state among all feasible policies. The milestone list states Lemmas 1, 2 and 4, Corollaries 1 and 2, all parts of Theorem 1 as identified by the paper's internal references, and the limit and optimality-equation clauses of Theorem 2. Together they fix the finite-stage and limiting objects used by the goal.
The theorem reduces a decision at every integer inventory position to one integer target for each observed world state. It gives an exact policy structure for a model with a changing demand rate and random lead time, rather than an approximation derived from a constant-demand model. The limiting inequalities also locate an optimal target relative to the myopic target and the finite-stage targets, giving a mathematically specified range for policy computation. These claims are the linear-cost part of Song and Zipkin's analysis; the paper proves the result but supplies no Lean proof.
Formalization will leave reusable definitions for countable-state uniformization with a demand counter, integer convexity of inventory cost functions, and discounted costs of history-dependent policies. The mission's theorem statements compile as open goals. The remaining work is to verify the analytic properties of the lead-time demand law, the finite-stage inequalities, convergence, and the infinite-horizon policy comparison. The fixed-order-cost and monotone-world-state results of the paper are separate missions.
The world can have countably many states, so a continuation value includes a series over possible world jumps. The stage cost grows with inventory position, so a bounded-cost finite-state dynamic-programming theorem does not directly cover the model. The minimization is over an unbounded set of integers, and the minimizers themselves change with the stage number. Convexity of a one-stage cost alone does not establish that the limiting policy beats policies that use the entire observation history. These are the specific gaps the paper's bound, ordered-difference, and limit results address.
World states are a nonempty countable Lean type, inventory positions and order-up-to levels are integers, and costs are real until policy evaluation. The lead-time law is a probability measure on finite nonnegative real times, independent of world and demand. The demand-count law is defined by exact Poisson uniformization at rate , with demand, world-jump, and self-loop branches. The infinite-horizon policy cost uses extended nonnegative reals and a supremum of finite-horizon costs, so it can express an infinite expected cost without a default real value. Policies may depend on all past observed states; the goal compares its basestock policy against every feasible deterministic policy in this class. Randomized policies are omitted because they cannot improve expected nonnegative costs on this countable state space.
Assumption 1 is attached only to the results that use it. The linear-cost recursion has and . Integer convexity means nondecreasing forward differences. Smallest minimizers and the minimum across world states are asserted to exist; neither is encoded by an integer infimum that returns a default on an empty or unbounded set. The goal requires an actual optimal policy cost comparison from every state, so solving the limiting optimality equation only within basestock policies cannot close it. Contributions to the lead-time mixture, integer convexity, boundedness of the real series and infima, and unrestricted policy comparison all fit this scope.
A fault-tolerant system often replicates a computation on several processors and needs the nonfaulty ones to act on the same data, even though some processors may fail in arbitrary ways: send wrong values, send different values to different recipients, or lie about what they were told. Pease, Shostak and Lamport posed the question in 1980, motivated by the SIFT fault-tolerant aircraft-control computer under development at SRI (Wensley et al. 1978), where it arises in clock synchronization among other places: processors, at most of them faulty, communicate by two-party messages whose sender is always identifiable, and each holds a private value. Can the nonfaulty processors all compute the same vector of values, one entry per processor, whose entry for every nonfaulty processor is that processor's true value? The paper (J. ACM 27 (1980) 228–234) calls this interactive consistency and settles it: possible if and only if when messages can be forged in relay, and possible for every when they cannot. The same problem, under the name Byzantine generals, became the standard model of arbitrary ("Byzantine") failures in distributed computing (Lamport, Shostak & Pease 1982); the bound underlies the quorum sizes of later replication protocols.
This mission covers the positive half of the paper's characterization: Section 3's recursive procedure, which achieves interactive consistency with processors in rounds of message exchange.
Let be a finite set of processors and a set of values. A string over a set is a finite sequence of elements of , repetitions allowed. For a -level scenario is a map from the nonempty strings over of length at most to . The value is 's private value ; for , is the value tells that told … that told is 's private value. A -level scenario records the outcome of rounds of message exchange.
Faults are modeled by a set of nonfaulty processors, unknown to the processors. Nonfaulty processors relay truthfully, so is consistent with when
Faulty processors are otherwise unconstrained. A processor sees only its view , the restriction of to strings beginning with .
The procedure (p. 230). Processor computes the entry for processor as follows, with and the current processor count and fault bound:
In Lean this is InteractiveConsistency.OralAlgorithm.record m P τ q with τ = fun w => σ (p :: w), values in Option V with none for NIL.
For , for every with and every -level scenario consistent with ,
This is procedure_assures_ic. It is the paper's claim about this procedure, not an existence statement.
The theorem is the upper bound in the tight characterization of when interactive consistency is achievable with unauthenticated messages; the matching impossibility (the paper's Section 4 THEOREM) shows that no procedure, with any number of rounds, does better. The procedure is the ancestor of the "oral messages" algorithm of the Byzantine generals paper, and its quorum arithmetic (, intersections of two quorums containing a nonfaulty member) recurs throughout Byzantine fault-tolerant replication.
The result is proved in the paper, in a half-page induction. What this mission adds is a machine-checked proof against an explicit model of scenarios, views and consistency with a bounded number of rounds. Machine-checked proofs exist for the related algorithm of the later Byzantine generals paper in other proof systems; this procedure, with its quorum-based step (1), has to our knowledge not been formalized in Lean, and nothing on message-passing agreement exists on this platform.
Each step of the paper's proof is short, but the bookkeeping is where an argument breaks. The recursion changes three things at once: the processor set loses , the fault bound drops by one, and the scenario becomes of one level less. The induction hypothesis must therefore be stated for every finite processor set and every scenario, and applied to a subscenario whose consistency is inherited only for strings of the right length. The mixed case, where one nonfaulty processor exits at step (1) and another recurses, is the delicate one: the two processors' computations take different branches, and since is faulty nothing forces either value to be 's private value. The thresholds are exact: in step (1) and agreeing entries in step (2), both in the current and ; off-by-one changes in either break the case analysis. Finally, step (2)'s majority value must be shown unique, so that two processors with the same vector record the same value.
Processors form a Finset α with decidable equality; strings are List α, read left to right (the receiver first, the originator last), so is σ (p :: (w ++ [q])). A scenario is a total function List α → V; consistency with (ConsistentUpTo P N (m + 1) σ) constrains it only on strings over of length at most , the domain of an -level scenario and all the procedure reads. The procedure receives only the view fun w => σ (p :: w), never or . The fault hypothesis is P.card ≤ N.card + m; is included.
Explicit readings of the paper's prose: "size " is P.card + m < 2 * Q.card; is natural-number division; "strings over of length " includes the empty string and allows repetitions; the step-(2) vector is indexed by P.erase q and includes 's own entry; the recorded value in step (1) is (the empty string forces it); when several values reach the step-(2) threshold one is chosen deterministically from the vector (under the goal's hypotheses at most one does); for a failing step (1) records NIL (never reached under the hypotheses). Two printed slips are corrected in the Lean: "records and " (for "for ") and "" (for ).
Trivializing formalizations are ruled out: the procedure never sees itself (with it, recording would be trivial), consistency constrains only relays by nonfaulty processors, and ranges over every subset of size at least .
The development needs only finite sets and lists; no library beyond Mathlib is required. The quorum-intersection lemmas and the subscenario construction are reusable for other oral-message protocols. Contributions welcome: proofs of the four milestones, the goal by induction on , and a computable version of the procedure for concrete instances. This is mission 1 of a series of three on this paper; mission 2 formalizes the impossibility THEOREM for (Section 4), and mission 3 the authenticated-message procedure for every (Section 5).
Many stochastic systems accumulate a real-valued quantity while repeatedly returning to a state at which a new cycle begins. A queue may accumulate work or cost, a component may accumulate wear, and a recurrent system may accumulate time in a state. The observations at a fixed clock time usually cut through a cycle. This makes the moments of the observed process different from the moments of a sum stopped exactly at a regeneration epoch. W. L. Smith introduced cumulative processes to state mean, variance, ergodic, and central limit results for this setting in a common language (Smith 1955, §5).
The mean growth rate describes the long-run reward per unit time. The variance growth rate also records the dependence between a cycle's length and its reward. That dependence matters in systems where unusually long cycles tend to accumulate unusually large rewards; assuming the two are independent would erase a term in Smith's formula (Smith 1955, Theorem 8). This mission targets the exact first-order mean and variance asymptotics, along with the source results Smith uses to pass from completed cycles to observations at ordinary times.
Work on one probability space . The cycle lengths are nonnegative, independent, identically distributed random variables whose common law is not concentrated at zero. Set and for . Thus is the th renewal epoch after the initial renewal at time zero. For , counts the epochs , including . The corresponding renewal function is , where is Smith's zero-delay law. These conventions come from §2·1 and §5·2 of the paper (Smith 1955, pp. 9 and 23).
A cumulative process is real valued, starts at , and has almost surely bounded variation on each finite nonnegative time interval. The cycle reward is . Write for the total variation of the path on and for its variation on . For the moment results, the cycle vectors are independent and identically distributed across . Their coordinates within one cycle may be dependent. This joint-cycle interpretation is required by Smith's common joint distribution for in the proof of Lemma 5 (Smith 1955, pp. 23–24).
Let , , and when the moments exist. Put , , and . Smith writes , with the cycle length–reward correlation. The covariance remains defined when either variance is zero. The auxiliary sum includes a reward beyond the cycles completed by time , exactly as in (5·2·1) (Smith 1955, p. 23).
The first target is the mean part of Theorem 8. If and are finite, then
The goal includes the variance part under the additional assumptions and :
Both limits are along real time, and neither assumes that a cycle's length and reward are independent. The milestone list contains the mean and variance limits for , the cycle-moment estimate used for the incomplete cycle, and Theorem 8(i) as the explicit mean target (Smith 1955, Lemmas 4, 5, 9 and Theorem 8).
The theorem gives a linear approximation to the process's expected value and variance, with errors smaller than the observation horizon. The leading variance coefficient separates reward variability, cycle-length variability, and their covariance. It can therefore be used without a false independence assumption when the duration of a cycle affects the amount accumulated during it. The formulas are first-order statements; they do not claim a bounded error or a limiting distribution (Smith 1955, (5·3·6)–(5·3·7)).
Formalizing these statements requires reusable definitions of renewal counts, path variation, random-cycle rewards, and the moment conditions that make expectations and variances genuine. The statement is a draft target, not a claim that Smith's proof already has a machine-checked reconstruction. A completed development would also give formal tools for other regenerative reward models whose observations occur between renewal epochs.
The auxiliary sum is sampled at a random index, while is observed at a deterministic clock time. They differ by part of a cycle that crosses . Ordinary laws for sums of a fixed number of independent rewards do not directly control either this random index or the crossing-cycle contribution. At second order, a bound on the mean difference alone does not determine the variance difference. The length–reward covariance must also survive the passage from completed cycles to the continuous-time process (Smith 1955, pp. 24–28).
Lean uses real time and real-valued paths. Cycle laws are represented by random variables on one probability space; the renewal at zero is explicit. The renewal count takes the value zero on a path with infinitely many renewals before a finite time, a null event under the nondegenerate i.i.d. length law. Variation is represented by Mathlib's extended nonnegative eVariationOn and converted to a real number only under the almost-sure bounded-variation condition. The theorem states integrability of and its square as consequences of the cycle-moment assumptions, avoiding default values for divergent real integrals or variance. A finite th moment is an integrability condition, not a comparison between a real number and infinity.
The paper's exact identity (5·2·2) is off by one under its own definitions of and ; the mission targets its valid asymptotic consequence (5·2·3). The last variance in the printed Lemma 5 coefficient is , while Theorem 8 and the calculation require . Milestone provenance retains the printed text; the Lean statements use the corrected coefficient. Lemma 9 is formalized for the absolute th moment of the cycle increment, which is the printed statement for a nonnegative cycle quantity such as the variation to which Theorem 8 applies it. Solvers may contribute the renewal and random-index estimates needed for the listed targets. A definition that makes rewards independent of cycle lengths would remove the covariance term and would not represent this mission's model.
The classical implicit-function theorem solves an equation for as a function of a parameter near a known solution , provided is (strongly) Fréchet differentiable in with an invertible partial derivative. Much of optimization does not meet that hypothesis. Optimality conditions of constrained problems, complementarity problems and variational inequalities are routinely rewritten as equations involving the projection onto a convex set, the componentwise , or the normal map of a polyhedron. These maps are Lipschitzian and piecewise smooth, but not differentiable. Sensitivity analysis asks whether the solution of such a system moves Lipschitz-continuously with the problem data, and the classical theorem cannot answer it.
Stephen M. Robinson, An Implicit-Function Theorem for a Class of Nonsmooth Functions, Mathematics of Operations Research 16(2), 1991, pp. 292–309, gives a theorem with the same shape as the classical one, in which differentiability is replaced by strong approximation by a function whose inverse is Lipschitzian. The paper's §4 applies it to parametric variational inequalities over polyhedral sets through the normal map.
Timeline. Robinson's Strongly regular generalized equations (Math. Oper. Res. 5, 1980) proved an implicit-function theorem for generalized equations under a linearization hypothesis called strong regularity. The 1991 paper reformulates that idea for single-valued nonsmooth equations: the approximating function need not be linear. Lemma 3.1 extends the Banach perturbation lemma for linear operators (Kantorovich–Akilov, Functional Analysis, Th. 4(2.V)) to Lipschitzian functions; after acceptance, A. Ioffe pointed the author to closely related results of Dmitruk, Milyutin and Osmolovskii (Lyusternik's theorem and the theory of extrema, Russian Math. Surveys, 1980, Theorems 1.2, 1.3), credited in the paper's footnote.
Let , , be real normed linear spaces, with complete. Fix , , a neighborhood of and a neighborhood of . Let map to , with , and let map to , with . denotes the closed ball of radius about .
Expansion modulus. For a map between metric spaces and a set ,
If , then is one-to-one on and its inverse is Lipschitzian with modulus . In Lean the mission works with lower bounds: ExpansionAtLeast f S d says on , i.e. .
Strong approximation (Definition 2.4). strongly approximates in at , written (Lean: StronglyApproxInX f F x₀ y₀), if for each there are neighborhoods of and of with
When is the partial derivative map this is strong partial Fréchet differentiability; in general may be piecewise linear or any map with a Lipschitzian inverse.
Assume (a) at ; (b) for each , is Lipschitzian on with modulus ; (c) is a neighborhood of in ; (d) . Then for each there are neighborhoods of , of and a function with
Every strictly above is claimed; is not.
where .
The result. Theorem 3.2 yields existence, local uniqueness and Lipschitz dependence of solutions of parametrized nonsmooth equations, with an explicit Lipschitz modulus arbitrarily close to . In the paper it underlies Theorem 3.3 and Corollary 3.4 (approximation and B-differentiation of the implicit function) and the sensitivity results of §4 for parametric variational inequalities over polyhedral convex sets. The same template, an equation approximated by a map with Lipschitzian inverse, is the basis of later strong-regularity and semismooth-Newton analyses in nonlinear programming and complementarity.
Formalizing it. The theorem is proved in the paper; it has not been machine-checked. The platform has the smooth implicit-function theorem (FamousTheorems.implicit_function_theorem, Rudin.ch09_implicit_function) and Mathlib has the contraction mapping principle, but there is no Lipschitz-inverse perturbation result and no notion of strong approximation. The mission produces both, together with the formal Theorem 3.2 that a follow-on mission (Theorem 3.3, Corollary 3.4, §4) would reference.
The obvious approach, differentiate and invert, is unavailable: need not have a derivative anywhere near , so neither Mathlib's implicit-function theorem nor its inverse-function theorem applies. The difficulty is to obtain surjectivity of onto a ball uniformly in from information about alone. Injectivity transfers directly from through the small Lipschitz modulus of ; surjectivity does not, because carries no information about beyond the small Lipschitz modulus of the difference, and the domain ball, the image ball and the parameter neighborhood must be chosen once for all . Completeness of is essential (the paper stresses this on p. 306) and is not available for and .
All statements live in namespace RobinsonNSIFT.Implicit. Committed conventions:
[CompleteSpace X]); , are normed spaces without completeness. Lemma 3.1's domain is a complete metric space, not a normed one.ExpansionAtLeast f S d in place of "", universally quantified. This is equivalent to the paper's statements and avoids a real infimum that would be on sets with fewer than two points.F : X → Y → Z and ; hypotheses constrain them on only, and the conclusions keep the implicit function inside the domain: , , . This makes explicit what the paper leaves implicit (its is only defined on ). Likewise , used implicitly in the paper's proof, is a conclusion of milestone 2.Metric.closedBall), radii written α / δ; neighborhoods are filter members ∈ 𝓝 _, not necessarily open; Lipschitz moduli are ℝ≥0 and Lipschitz conditions are LipschitzOnWith on the stated set.A formalization in which hypothesis (a) is the weak approximation of Definition 2.1 (only at ), in which may shrink to , is existential, or uniqueness is asserted outside , would be a different and trivial or false statement; the statements here rule these out.
Needed infrastructure: the contraction mapping principle on a closed subset of a complete space (Mathlib's ContractingWith), Lipschitz estimates on sets, and the two definitions of this mission. Lemma 3.1 is reusable for any Lipschitz-perturbation argument. Proofs of either milestone, or a direct proof of the goal, are welcome.
Classical cooperative game theory assumes that any coalition of players can form and coordinate. In many settings cooperation is mediated by pairwise relationships: communication lines, contracts, alliances, or trade links. Roger Myerson's discussion paper Graphs and Cooperation in Games (Northwestern University, 1976; published in Mathematics of Operations Research 2(3), 1977, doi:10.1287/moor.2.3.225) models such a cooperation structure as a graph on the set of players and asks how the players should share the worth of the game when only linked players can coordinate directly.
The answer, now called the Myerson value, is the starting point of the literature on communication situations and network games. It underlies later work on network formation (Jackson and Wolinsky, A strategic model of social and economic networks, JET 1996) and on allocation rules for networks, and it is a standard textbook example of an axiomatic solution concept.
Timeline:
Let be a nonempty finite set of players and the set of nonempty coalitions . A game in characteristic function form is a vector ; is the transferable wealth coalition can divide.
A link is an unordered pair of distinct players and a graph is a set of links; is the set of all graphs, the complete graph, the graph with one link removed, and the number of links. Players are connected in by if or a path of links of joins them through players of only; the classes form the partition of , and is the set of connected components of . The graph-restricted game is
An allocation rule is a function , with the payoff of player under cooperation structure . It is a fair allocation rule for if
is totally stable if for every and every link , and is superadditive if for disjoint .
A game in graph function form assigns to every pair with a closed, comprehensive (closed under decreasing coordinates), proper () set of feasible payoffs; its fair allocation rule replaces (7) by (14), .
If is superadditive, then the fair allocation rule for is totally stable:
Every has a unique fair allocation rule; every game in graph function form has a unique satisfying (14) and (10).
The fair allocation rule is
The milestones follow the paper's Section 7: the steps of the proof of Theorem 4 (displays (15)–(17)), Theorem 4, Theorem 1, the decomposition of and the efficiency and equity of (proof of Theorem 2), Theorem 2, and the monotonicity of and in a link (proof of Theorem 3). Theorem 3 is the goal because its proof uses the formula of Theorem 2, whose proof uses the uniqueness of Theorem 1, which is the transferable-utility case of Theorem 4: all four numbered results lie on one path.
The theorems give an axiomatic foundation for allocation in networks: two natural requirements, component-wise efficiency and equal gains from each link, single out one rule, and that rule is an explicit formula built from the Shapley value. At the complete graph it recovers the Shapley value itself, so the result is also a new characterization of the Shapley value. Total stability says that, for superadditive games, no player has an incentive to break a link, which connects the allocation rule to the question of which networks form.
The results are proved in the paper. A search of the platform found no formalization of cooperation graphs, the graph-restricted game, the Myerson value or total stability; the Shapley value is available as a platform definition and is reused. This mission produces machine-checked statements of all four theorems and of the intermediate steps of their proofs, together with a reusable definition layer for communication situations.
The equity condition (10) relates the payoff at a graph to the payoff at a graph with one fewer link, and it constrains only pairs of linked players; it is not evident that these conditions, together with efficiency on components, determine the rule at every graph, nor that they are consistent. Uniqueness and existence must hold simultaneously for all graphs, and the constraints couple each graph to all of its subgraphs and each player to every other player of its component. In the graph function form, efficiency becomes a boundary condition on a closed comprehensive set, and the existence and uniqueness of the relevant extremal point depend on all three properties of .
Identifying the rule with requires the efficiency of the Shapley value on each component of , which is not the efficiency of on , and equity requires tracking how the partitions change when a link is removed. Total stability is false for general games: without superadditivity a player can gain by cutting a link, so the hypothesis cannot be dropped.
Players are Fin n, with in every theorem as the paper assumes nonempty; the paper's player is index . The general game carrier has its own definition module, and the graph-specific definitions build on it. Graphs are SimpleGraph (Fin n): is ⊤, the empty graph ⊥, is h ≤ g and is h < g. A game is a function Finset (Fin n) → ℝ; its value at is a junk coordinate that no definition reads, and no theorem assumes . Superadditivity quantifies over nonempty coalitions only. The Shapley value is the platform definition Supermodularity.Cooperative.ShapleyValue, applied after resetting the value at to . is ↥S → ℝ with the product topology, and is the topological frontier.
Explicit readings of the typescript:
The equity and stability conditions quantify over links of only. Quantifying over all pairs of players would make Theorem 1 false and the goal vacuous, so that reading is ruled out. Likewise (14) is boundary membership, not membership in .
Contributions welcome: general lemmas on the partitions (refinement under link deletion, restriction to components), Möbius inversion over the subgraph lattice of a finite simple graph, the carrier and null-player properties of the Shapley value, and the extremal-point lemma for closed comprehensive sets. These are reusable beyond this mission.
In a finite stopping problem, a decision maker observes rewards one at a time and must accept one without seeing the future. A fully informed observer takes the maximum. This comparison is often called a prophet inequality. The abstract bound that an optimal stopping rule can secure at least half the expected maximum does not say how to choose a simple rule. Samuel-Cahn showed that a threshold chosen from a median of the maximum already gives this guarantee, even when the rewards are independent but differently distributed. The rule requires one number fixed before observations begin. Samuel-Cahn, 1984
The paper builds on earlier comparisons between the maximum and the best stopping value, then narrows attention to rules that accept an observation when it crosses a fixed threshold. This mission isolates its first main result, Theorem 1, and the two cases that determine whether the crossing test is strict or weak. The paper's second main result, concerning the sharpness of the constant for identically distributed rewards, belongs to the next mission in this series. Samuel-Cahn, 1984, pp. 1213–1215
Let , and let be independent, nonnegative real random variables. Write . For a threshold , the weak threshold rule takes the first with and ; the strict threshold rule uses . If no earlier observation qualifies, either rule takes , even when is below the threshold. Hence every rule returns exactly one observed reward.
The paper distinguishes the full stopped reward from its positive threshold reward. In its notation,
The last forced observation may contribute to or while contributing zero to or . This difference is essential to the theorem's middle bounds. A median of means both and . Define the excess sum , where . The two median inequalities allow an atom at , and the two threshold rules handle that boundary differently. Samuel-Cahn, 1984, pp. 1213–1214, (1.1)–(1.2)
For every median , the goal retains both of the paper's conditional conclusions:
At equality , both conclusions apply. The attack path follows the expected maximum bound (1.3), the displayed identities and probability bound in (1.4), and the companion weak threshold display. Each milestone points to an actual line of the paper. The NOTE and ASSERTION give a further interval of working thresholds: if and , then every satisfies the same chain with . Remark 1 records the special case of observations taking values in one common two point set. Samuel-Cahn, 1984, pp. 1214–1215
Theorem 1 replaces the unspecified best stopping policy with a specific threshold chosen from the distribution of the maximum. It also shows that the thresholded part of the stopped reward alone meets the factor two bound. That stronger middle statement distinguishes the theorem from an outer comparison . For a reward distribution with atoms, the theorem says exactly when to use and when to use . Its companion ASSERTION shows that a median is not the only useful threshold choice. Samuel-Cahn, 1984, p. 1214
The result is proved in the paper; the work here is to express its assumptions, boundary behavior, and all displayed inequalities as Lean statements that solvers can prove. The milestones expose reusable facts about positive parts, forced stopping, and independence of a current observation from the event that the rule has survived earlier ones. No machine checked proof of these drafted statements is claimed. The second mission can use the completed theorem to formalize why the factor two cannot be improved uniformly over threshold rules, even for identically distributed observations.
The event that a rule reaches index depends on the observations before . Establishing its independence from the excess of requires mutual independence of the whole family; pairwise independence does not express enough. A forced stop at also makes the positive threshold reward smaller than the full stopped reward whenever the last observation misses the threshold. Ignoring that last case would erase one of the theorem's conclusions. Finally, atoms at the median prevent the strict and weak crossing events from being interchanged. Samuel-Cahn, 1984, (1.1)–(1.4)
Lean indexes the observations by Fin with . Its index zero is the paper's index one, and the greatest index is the paper's mandatory final stop . The rules are the least qualifying index or that final index. The paper's and therefore become and . Observations are measurable, nonnegative almost surely, and mutually independent under a probability measure.
Expectations use the extended nonnegative integral of the positive part, taking values in . This keeps infinite expected rewards visible without imposing an integrability assumption absent from Theorem 1. The median has both strict tail inequalities from (1.1). The identities for positive stopped rewards state directly; in the goal this follows from nonnegativity and the median condition. The balance thresholds and are parameters satisfying the paper's defining equations, with no extra uniqueness hypothesis in statements that do not use it.
The goal cannot be satisfied by replacing with , by permitting a rule to return no observation, or by making the median predicate empty. Useful contributions include the measurable threshold rule interface, the pathwise excess decomposition, the factorization under mutual independence, and the remaining extended nonnegative arithmetic. Those pieces can also support other finite prophet inequality developments.