Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
In a birth-and-death population model, an expected population curve does not determine the amount of random variation. Births and deaths can occur frequently while nearly canceling in the mean, or one of the two rates can vanish while giving the same mean. This distinction matters when a prescribed growth curve is used to model a population: two processes can agree on their expected size at every time and differ substantially in their uncertainty. In §6 of Kendall's 1948 paper, the question is posed directly: among time-varying birth and death rates giving a fixed mean curve, which choice minimizes the variance of the population size?
Kendall cites Arley's observation for constant rates with the same positive net growth. His §6 moves from that special case to an arbitrary prescribed mean curve and identifies a unique minimum-fluctuation rate pair. The paper also gives a logistic-growth example, connecting the stochastic rate choice to a familiar deterministic population law. The historical result is proved in the paper; this mission concerns its Lean formalization, including the exact time-dependent variance comparison and uniqueness claim.
The process starts with one ancestor. At time , each member gives birth at rate and dies at rate ; the rates are nonnegative. Let be the population size and its expectation. Kendall works with the population probabilities and their generating function rather than constructing sample paths. This mission likewise uses his explicit formulas for the mean and variance, so that the comparison has a precise real-valued expression.
Define the integrated net death rate and the fluctuation by
Kendall's equations (13) and (14c) identify and for the one-ancestor process. A pair is admissible here when both rates are continuous and nonnegative on . It has mean when for every . In particular, the initial value is . These definitions let the mission quantify over every admissible rate pair with the prescribed mean.
For a positive continuously differentiable mean curve, write . The minimum-fluctuation rates are and . When the mean decreases, only deaths occur; when it increases, only births occur; when it is locally constant, both rates are zero. This is Kendall's equation (56), expressed without first naming intervals of monotonicity.
The goal is the simultaneous variance bound
The statement also establishes that is admissible and has the required mean. Its uniqueness clause says that if one admissible pair has the same variance as the candidate at every nonnegative time, then its two rates equal the candidate rates at every nonnegative time. Equality at only one selected time does not express Kendall's claim. The formal milestones record the fixed rate difference (55), the integral decomposition displayed in §6, and the nonnegative excess in variance that precedes (56). A companion statement covers the logistic example (58)–(60): for and , has minimum-fluctuation death rate zero and birth rate .
The result distinguishes mean growth from population risk. Fixing fixes the mean curve, but it leaves room for births and deaths that offset one another. Kendall's theorem determines the lowest variance compatible with the given curve and specifies the rate pair attaining it. The uniqueness statement identifies a model, rather than only a numerical lower bound. His logistic example shows the choice concretely: positive logistic growth is realized by a purely reproductive process in the minimum-fluctuation model.
The paper already derives these formulas. A complete formalization would connect the exact variance expression to a universal optimization claim over continuous nonnegative rate functions, and it would verify that equality throughout time identifies the rates. The definitions of the integrated rate, mean condition and variance functional can also support the other results in Kendall's paper. This proposal uses a local copy of because the geometric-solution mission is being drafted in parallel and its definition has not been published for import.
The constraint imposed by a given mean fixes the difference but not either rate separately. The variance is an integral over the full past, multiplied by a term involving that same integrated difference. Consequently, a pointwise observation about the current sum does not by itself state the required comparison of variances over every time horizon. The equality case is also global: a single time's variance cannot generally identify the rates at all earlier times. The formal result must keep the shared mean condition, the variance integral and the quantifiers over both rate pairs and all nonnegative times aligned.
The Lean development represents rates and the prescribed mean as functions . Every stochastic claim is restricted to ; the integrals are oriented interval integrals from zero. Both rates are continuous on all of and nonnegative on nonnegative time. The mean is , positive on all of , and equals one at zero. Extending the regularity and positivity assumptions to negative time makes the total functions defining , and continuous without changing any comparison on . These are explicit convenience assumptions beyond Kendall's wording. No denominator is used without the positivity assumption.
Kendall presents (56) after assuming that positive time splits into decreasing, increasing and constant intervals of . The goal uses positive and negative parts of and therefore covers any positive curve, including one without such a partition. On each of Kendall's three types of interval the formula agrees with his stated rates. The variance functional is exactly the last expression in (14c); its identification with the variance of the geometric population law is treated in the companion geometric-solution mission. The local statements do not construct a Markov process. The minimum is taken over all admissible continuous nonnegative rate pairs with the prescribed mean, not merely over the two candidate functions or over pointwise values of .
The development needs real differentiation, continuity, exponentials and interval integrals from Mathlib. Contributions that relate the explicit functional to the population law, prove the comparison and its equality case, or extend the regularity regime while preserving Kendall's claim are within scope. The logistic example provides a concrete instance of the general result.
A recurring task in martingale theory is to compare a sum of nonnegative random variables with the sum of their predictable projections : the conditional expectation of each term given the information available one step earlier. Such comparisons are the step that turns a statement about the conditional square function of a martingale into a statement about the martingale itself, and they recur in the proofs of the Burkholder–Davis–Gundy inequalities and of their conditional variants.
In his 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Burkholder 1973), D. L. Burkholder proves two such comparisons for a function applied to the sums. For convex of moderate growth, the sum of predictable projections is controlled by the sum itself, up to a constant (Lemma 16.1, the "convexity lemma", §16). For concave , §20 proves the reverse comparison, with the explicit constant . This mission is the concave case, Theorem 20.1.
The same section derives Theorem 20.2 from it: for a martingale and concave , . For the concave powers , , that bound had been proved by another method in Burkholder, Davis and Gundy 1972. Comparisons of the same kind between an increasing process and its compensator were later systematized as the Lenglart domination principle (Lenglart 1977).
Let be a probability space and a non-decreasing sequence of sub--fields of . In Lean this is a probability measure P together with a filtration ℱ : Filtration ℕ mΩ, ℱ k .
Let be nonnegative measurable functions on , with values in . They need not be integrable, and they need not be adapted: is only -measurable. For a nonnegative function the conditional expectation always exists as an -measurable function with values in , determined up to null sets by for . Put
and, for , the partial sums , over .
A function is concave as above in the paper's sense if it is non-decreasing and continuous on , , it satisfies the growth condition for , and it is concave on . Concavity alone already gives . Examples: for , , .
For a martingale with differences (), the maximal function is and the conditional square function is .
for every concave as above and all nonnegative measurable . The constant is universal: it does not depend on , on the growth constant , on the probability space or on the .
For a martingale and concave as above,
It is posed as a separate theorem and is not a milestone of the goal.
Theorem 20.1 holds without any integrability and without adaptedness, so it applies to arbitrary nonnegative sequences. With it compares the square function of a martingale with : for concave , . Together with the Burkholder–Davis–Gundy comparison of and , this is one route from the conditional square function to the maximal function in the range of exponents , where the convex methods of the rest of the paper do not apply. Theorem 20.2 is the result of this kind that the paper states.
The paper proves Theorem 20.1 in about half a page. As far as is known, neither Theorem 20.1 nor Theorem 20.2 has been formalized in any proof assistant. Mathlib provides the -valued conditional expectation (condLExp), filtrations, stopping times and Lebesgue integrals of extended nonnegative functions. It has no comparison theorem of this type between a sum and its predictable projections. A formal proof would therefore add a new, reusable tool to Mathlib's discrete-time martingale library, one that an eventual formal Lenglart inequality or conditional BDG inequality would need.
The obvious first idea is Jensen's inequality for conditional expectations. For concave it gives term by term, but of a sum is not the sum of the 's, and summing the termwise bounds loses the comparison. Another first idea, comparing and (which are equal by the tower property), handles only linear , and both sides may be infinite.
The content lies in two places. The first is the truncated inequality for , where neither nor is integrable in general and the comparison must hold level by level. The second is the passage from the truncated family to an arbitrary concave . It needs a representation of concave through the truncations , including the cases and and a possibly infinite right derivative at (as for ). Both steps must be carried out in arithmetic.
ℝ≥0∞-valued; expectations are lower Lebesgue integrals ∫⁻. The conditional expectation is Mathlib's condLExp (notation P⁻[z | ℱ k]), never the Bochner P[z | ℱ k]. The Bochner version is on non-integrable functions and would make the goal false (take ).z (k+1) is and is paired with ℱ k , so is conditioned on , as in the paper. z 0 is unused.IsPhi Φ c for an arbitrary constant c, together with IsConcavePhi Φ: concavity of on , read through real values. This is honest because IsPhi forces to be finite on finite arguments. The growth condition is required for every , which is equivalent to (6.1) by continuity. The paper's exclusion of is dropped, since the conclusion is trivial there.l : ℝ≥0).Martingale f ℱ P. It reads f n only for , with the paper's convention . Mathlib's extra constraint on f 0 is no restriction, since every martingale of the paper extends by .condLExp for indicators of -sets, monotone convergence for condLExp, and the integral representation of a concave non-decreasing with as a mixture of the functions plus a linear part. The last is reusable well beyond this mission. Contributions to any of these are welcome.A martingale can have individually well behaved increments while the sum of their squares remains large on rare sample paths. The square function records that accumulated variation. Bounds on its distribution tell probabilists how much a martingale can fluctuate even when a terminal value alone gives little pathwise information. In Section 19 of Distribution Function Inequalities for Martingales, D. L. Burkholder studies a conditional tail bound for squared increments and obtains an explicit exponential moment for the entire square function. The result is Theorem 19.1, with a one-parameter constant fixed exactly as for (Burkholder 1973, p. 37).
The paper calls the linear span of martingales satisfying this normalized tail condition BMO, and notes that bounded martingales belong to it after a suitable scaling. It connects this martingale notion to bounded mean oscillation of functions, introduced by John and Nirenberg, and to the surrounding work on the duality with (Burkholder 1973, p. 38). The mission isolates the article's concrete exponential estimate, which can be read and used without developing the whole later theory of BMO.
Let be a probability space and let be an increasing sequence of sub-sigma-fields. A real martingale is written relative to . Following the article's convention, put for its difference sequence, so and for . The partial square function and the full square function are
These are nonnegative random variables and the full one may initially take the value . The paper fixes this notation in Section 1 (Burkholder 1973, p. 20).
The condition used here is a bound on the expected squared-increment tail after conditioning on the information available at time :
The sum starts at , including , and the conditioning sigma-field is . Both indices matter; shifting either changes the hypothesis. The value is a normalization, not an unnamed bound whose choice can depend on the martingale (Burkholder 1973, p. 37).
The first milestone is the distribution estimate displayed in the proof of Theorem 19.1. For every ,
It records exactly the quantitative link between the conditional hypothesis and the distribution of the full square function (Burkholder 1973, p. 37).
The second milestone is Lemma 18.1. For a nonnegative measurable and a constant , suppose
Then has an exponential moment at every , bounded by . The lemma is stated for any probability space and any nonnegative measurable , so it is reusable beyond martingale square functions (Burkholder 1973, p. 36).
Under (19.1), the goal is the article's explicit estimate
In particular, is finite almost surely. The exact coefficient and the whole open interval for are part of the target (Burkholder 1973, p. 37).
The conclusion gives more than finiteness of the square function or any fixed moment: one conditional second-moment tail condition yields a family of exponential bounds for its square. The paper points out that bounded martingales meet the condition after scaling, placing a familiar class within this BMO framework (Burkholder 1973, pp. 37–38). The constant makes the normalization of (19.1) visible and allows later users to choose a value of without recovering an unspecified constant.
Formalizing this result produces a reusable interface between conditional expectations of nonnegative series, tail probabilities, and exponential moments. The exact Theorem 19.1 and Lemma 18.1 are posed as Lean statements here; their proofs are not yet machine checked in this mission. Mathlib supplies probability measures, filtrations, martingales, extended nonnegative integrals, and generalized conditional expectation. Completing the mission would establish the paper's stated quantitative bound in that setting, while the standalone exponential lemma could also be imported by developments with different stochastic objects.
The hypothesis bounds a conditional expectation of the entire future squared-increment tail at every time. It does not bound pointwise: rare paths may accumulate a large sum while the conditional average remains controlled. A direct attempt to bound the exponential term by bounding each increment separately loses the dependence across times and does not yield the stated coefficient. The central mathematical gap is therefore the passage from time-indexed conditional tail information to a global distribution estimate that is strong enough for the exact exponential constant (Burkholder 1973, pp. 36–37).
The Lean development represents and by explicit definitions and as the supremum of its partial square functions, valued in . Thus a divergent square function has value , rather than a default real supremum. Probability tails and expectations of nonnegative functions use extended nonnegative measures and integrals. Condition (19.1) uses generalized conditional expectation of the nonnegative series; ordinary real conditional expectation could return a default zero on a non-integrable tail and make the assumption empty. The inequality holds almost everywhere, as conditional expectations are determined only up to null sets.
The article starts its martingale at index one and sets for differences. Mathlib's martingale is indexed from zero. Its index-zero value can be supplied by a conditional expectation of ; the shared difference-sequence definition still reads the paper's . The squared tail begins at and is conditioned on . The goal states almost-sure finiteness of as a conclusion before applying the real exponential to its finite value. This avoids treating as zero through an extended-real conversion. No finiteness of , integrability of its square, or exponential moment is assumed at the outset. The zero martingale on a one-point probability space satisfies the condition, so the hypotheses admit a concrete instance.
The common martingale definitions also include maximal functions, stopped values, norms, a conditional square function, and the class of moderate-growth functions used by other missions from this article. The reusable contributions especially welcome here are the tail integral lemma for extended nonnegative functions and results connecting generalized conditional expectation with a nonnegative infinite sum. The exact source indices, constants, and boundary conventions are fixed by the source pages cited above.
A martingale is a sum of increments each of which has conditional mean zero given the past. Most quantitative statements about martingales compare the size of the maximal function with some measure of the size of the increments. Two such measures are classical: the square function , which sums the realized squared increments, and the conditional square function , which sums their predicted conditional variances. The conditional square function is the discrete analogue of the predictable quadratic variation of a continuous-time martingale, and it is the quantity that appears in martingale central limit theorems, Freedman- and Bernstein-type exponential bounds, and in the analysis of stochastic approximation algorithms, where the noise is typically described through its conditional variance.
This mission formalizes Theorem 21.1 of D. L. Burkholder's 1971 Wald Memorial Lectures, Distribution Function Inequalities for Martingales (Ann. Probability 1 (1973) 19–42). The theorem bounds by and the size of the largest jump, for every of moderate growth.
Timeline. Rosenthal (1970) proved, for sums of independent mean-zero random variables and , that the -th moment of the sum is comparable to (Israel J. Math. 8 (1970)). Burkholder and Gundy (1970, [6] in the paper) developed extrapolation methods for martingale operators, including Example 8.2, which shows that fails for general (Acta Math. 124 (1970)). Theorem 21.1 follows from Theorem 3.1 of Burkholder, Davis and Gundy (1972, [5] in the paper), as remarked at the top of p. 553 of Burkholder's 1970 ICM address ([4] in the paper). In the Wald lectures Burkholder gives a direct proof by a distribution function inequality, which this mission formalizes.
Let be a probability space and a nondecreasing sequence of sub--fields of . Let be a martingale relative to , and set , so that the difference sequence is and for . Define
The first conditional expectation is taken with respect to . All three quantities may be infinite.
A function satisfies the conditions of Section 7 if it is nondecreasing and continuous, , and it has moderate growth:
The constant is the growth constant. The powers , , are the basic examples; need not be convex.
In Lean the shared layer is BurkholderDFI.CondSquare.Martingale: dseq f is , maxFn f is , maxFn (dseq f) is , condSqFn ℱ P f is and IsPhi Φ c is the class above.
For every growth constant there is a constant such that for every martingale and every satisfying the conditions of Section 7,
The constant depends only on , and no value for it is fixed, so the goal remains valid under any improvement of the constant.
Two consequences recorded in §21 are included as draft theorems: (21.5), , and the upper half (21.4) of Rosenthal's inequality for independent mean-zero sums.
The result. Theorem 21.1 controls the maximal function by predictable information (the conditional variances) plus the single largest jump, for every of moderate growth, convex or not. The jump term cannot be dropped: the paper notes that an inequality of the form fails for general (Example 8.2 of Burkholder–Gundy 1970), so some account of large individual increments is necessary. Specialized to independent increments, becomes the deterministic and the theorem yields the upper half of Rosenthal's inequality. The martingale version applies wherever increments are dependent but their conditional variances are controlled, as in stochastic approximation.
Formalizing it. The result is proved in the paper; to our knowledge neither Theorem 21.1 nor Rosenthal's inequality has a machine-checked proof. Mathlib has Doob's maximal inequality and martingale convergence, but not the conditional square function, good- inequalities, or -moment inequalities with moderate growth. A complete development produces all three, together with the stopping-time manipulations (a martingale started at one stopping time and stopped at another) that most of the paper's arguments reuse.
The obvious approach is to use theory: for a square-integrable martingale, so and are comparable in . This identity gives nothing for other , and in particular for with or there is no direct comparison of and : can be small while one increment is huge. A bound for general must therefore handle the event where a single increment dominates, and it must work for every level simultaneously, using nothing about beyond monotonicity and the growth condition (6.1). Without convexity of , no Jensen- or duality-type argument applies.
The Lean conventions committed to are:
ℝ≥0∞, lower Lebesgue integrals), so infinite values are meaningful and no junk value arises.condLExp, which need no integrability of . The Bochner conditional expectation or condVar would return on non-integrable and must not be substituted.ℱ : Filtration ℕ _ is indexed from , with ℱ k ; the -th summand of pairs with ℱ k. The paper states that is a martingale relative to ; the formalization states that is a Mathlib martingale, which also constrains the index- term. This is no restriction, since the extension is always possible, and all definitions use the paper's , never Lean's f 0.IsPhi Φ c imposes (6.1) for every , which is equivalent to the paper's condition by continuity. The paper's hypothesis that is not identically zero is dropped, since every inequality is trivial for .Type. A constant chosen after or would trivialize the goal whenever the right-hand side is positive, and that formalization is ruled out.Needed infrastructure, reusable beyond this mission: the conditional square function and its basic properties for stopped martingales; a good- lemma for moderate-growth (Lemma 7.1, shared with the other missions of this series); and the layer-cake formula for a Lebesgue–Stieltjes . Proofs of the milestones, proofs of (21.5) and Rosenthal's inequality from the goal, and independent proofs of any of them are all welcome.
A backward stochastic differential equation (BSDE) prescribes the value of a process at a terminal time and asks for an adapted process that reaches it while following a given drift . Adaptedness forces a second unknown , the integrand of a martingale term. Pardoux and Peng (1990) proved that Lipschitz BSDEs are well posed. BSDEs then became a standard language for stochastic control, for pricing and hedging in mathematical finance, and for probabilistic representations of semilinear parabolic PDEs.
Many such problems carry a constraint. The value of an American option must stay above its exercise payoff, and the value of an optimal stopping problem must stay above the reward for stopping now. El Karoui, Kapoudjian, Pardoux, Peng and Quenez (1997) introduced the reflected BSDE: the solution is kept above a given obstacle by an increasing process that acts only when the constraint binds. This mission formalizes the paper's first main result, existence and uniqueness of the reflected BSDE, together with the estimates its proof rests on.
Let be a -dimensional standard Brownian motion on a probability space . Let be its natural filtration, augmented by the -null sets. Fix a horizon . The data are:
with the standing assumption a.s.
A solution is a triple of progressively measurable processes, valued in , and , such that
(vii), and is continuous and nondecreasing with and (viii). Condition (viii) says that increases only when touches . The integrability conditions are (v), , and (v′), and .
Under (i)–(iv) and , the reflected BSDE with (v)–(viii) has a solution, and any two solutions satisfying (v)–(viii) coincide:
Theorem 5.2 is the foundation of the theory of reflected BSDEs. With it, the solution gives the value of a mixed optimal stopping problem (Proposition 2.3). For concave it gives the value of a combined stopping and control problem, and in a Markovian setting it gives the unique viscosity solution of the obstacle problem for a semilinear parabolic PDE. The other two missions of this series formalize those consequences, and both use the existence and uniqueness proved here. The model has many later extensions (two obstacles and Dynkin games, jumps, quadratic growth), and the pricing of American options under constrained or nonlinear dynamics is formulated through it.
The result is classical and fully proved in the paper. As far as is known, no machine-checked proof of existence for a (reflected or plain) BSDE exists. The remaining work is the formalization of the known proof: the Skorohod lemma, the optimal-stopping representation, the a priori and stability estimates, and the Picard contraction. The milestones are reusable well beyond this paper, in particular the Skorohod lemma, the estimates, and the identification of the reflected solution with a Snell envelope.
The natural first idea is to treat (vi) as a forward equation and reflect it pathwise with the Skorohod map, as in forward reflected SDEs. This fails: the pathwise reflection of a backward equation produces a process that is not adapted (Proposition 2.2 gives as a supremum over the future). The adaptedness of comes only from the choice of , i.e. from a martingale representation. Any construction must produce and together, and the estimates must control the contribution of using only the minimality condition (viii). In the formal setting, Mathlib has Brownian motion, filtrations, stopping times and conditional expectations, but no stochastic integral (the platform definition Peng1990.SMP.IsItoIntegral supplies one, without any calculus), no Itô formula, no martingale representation, no Burkholder–Davis–Gundy inequality and no Snell envelope theory in continuous time.
The Lean development builds on the published definitions Peng1990.SMP.Stochastic: standard -dimensional Brownian motion, as L2F, and the Itô integral IsItoIntegral. It commits to the following conventions:
ℝ≥0, with , and only matters;Proposition 2.3 additionally assumes , which the paper's Remark 3.2 allows without loss of generality, so that every conditional expectation in it is of an integrable variable. The constants of Propositions 3.5 and 3.6 are quantified before the Brownian dimension, probability space, data and solution, and depend only on ; a per-solution constant would make both statements trivial. The condition is part of every statement, since without it no solution exists. Proposition 3.1 and Corollary 3.3 (β) are not posed.
A complete proof needs Itô's formula for , the Burkholder–Davis–Gundy inequality, Gronwall's lemma, martingale representation for the Brownian filtration, and the Snell envelope with its Doob–Meyer decomposition. Each of these is reusable on its own, and contributions of any of them are welcome, as are proofs of individual milestones.
The square function of a martingale with differences and its maximal function are the two basic size measures of a martingale. Inequalities comparing them, and the reverse, are used throughout probability and harmonic analysis: they control stochastic sums by their quadratic variation, give bounds for martingale transforms, and transfer to singular integrals and area integrals in classical analysis.
D. L. Burkholder's 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Ann. Probability 1 (1973) 19–42), organise these comparisons around distribution function (good-) inequalities. Chapter IV of the paper begins with "some of the consequences of nonnegativity". This mission formalizes one of them: for a nonnegative martingale, the square function is controlled by the maximal function in every moment of moderate growth, convex or not.
A short history of the comparison:
Let be a probability space and a filtration. A nonnegative martingale is a sequence of integrable random variables with , measurable with respect to , and . With , its difference sequence is , . The objects compared are
In Lean these are sqFn f and maxFn f; the finite versions and are sqFnN f n and maxFnN f n.
For , the exit time (with ) is exitTime f λ, and , the square function of stopped just before it first exceeds , is sqFnAt f (exitTime f λ - 1), with and .
A function satisfies the conditions of Section 7 (IsPhi Φ c) if it is non-decreasing and continuous, , and it has moderate growth:
The powers , , are the model examples.
For every growth constant there is , depending only on , such that for every nonnegative martingale and every satisfying the conditions of Section 7,
The goal fixes no value of the constant, so it is the statement that survives any later improvement of .
with equality on the left for martingales. 2. (18.5) (p. 37): for a nonnegative martingale and ,
The result. Theorem 18.3 removes the convexity hypothesis from one half of the Burkholder–Davis–Gundy comparison, at the price of nonnegativity. It covers the concave powers , , and every other of moderate growth, including those that are neither convex nor concave. Nonnegative martingales are the natural objects in likelihood ratios, branching processes and Radon–Nikodym densities. For , , the paper derives from Theorem 18.2 and Lemma 7.1 the bound with the order in the constant (p. 37). Theorem 18.2 is the distribution function inequality behind the theorem and is itself a sharper statement than any moment inequality it yields.
Formalizing it. The result is proved in the paper. As far as is known it has no machine-checked proof, and Mathlib has neither the martingale square function nor any good- machinery. A formalization produces reusable components: the square function and stopped square function of a discrete martingale, Lemma 2.1, and Lemma 7.1, which is shared by every inequality in the paper and many outside it.
For general martingales, a good- inequality bounding by a small multiple of is false: a single large jump can make large while the martingale is stopped before grows, which is why the general results need convexity or a jump bound. The first idea, transferring the convex case of Burkholder–Davis–Gundy, does not work for concave : the convex proof uses convexity of in an essential way (Lemma 16.1 of the paper), and for general martingales the conclusion itself is false for , . A bound on alone, as in Lemma 2.1, is also not enough; the good- inequality needs control of the tail of above every level , which is where nonnegativity enters. Passing from the distribution inequality to all at once also requires care with infinite values of and .
Martingale f ℱ P with f : ℕ → Ω → ℝ and ℱ : Filtration ℕ mΩ, ℱ k = 𝒜_k. Statements read f n only for , with the paper's ; Mathlib's additional constraint at index is no restriction, since any martingale relative to extends to one by . Nonnegativity is "almost surely, for ".ℝ≥0∞-valued (∫⁻), so both sides of the goal may be infinite and no junk value arises from a non-integrable function.IsPhi Φ c imposes the growth condition at every , which is equivalent to (6.1) for . The paper's exclusion of is dropped (the inequalities are trivial then). No convexity is assumed anywhere in this mission.∀ c, ∃ C > 0, ∀ Ω P ℱ f Φ, with in Type: the constant may depend on only, never on , or . A constant chosen after the data would make the goal trivial whenever its right-hand side is positive; that reading is ruled out by the quantifier order.Real.sqrt; with this is .The shared definitions file declares the series-wide layer (including , convexity and concavity predicates used by other missions of the series). Proofs of any milestone are welcome, as are auxiliary lemmas on the stopped square function, on the Stieltjes representation , and on the layer-cake formula in ℝ≥0∞.
Martingale estimates describe how a process built from successive, conditionally fair increments can fluctuate. A basic object is its square function: the square root of the sum of the squared increments along a sample path. Square functions are useful because they record accumulated variation even when positive and negative increments cancel in the martingale itself. Burkholder's 1973 lectures study the distributions of square functions and maximal functions and compare their moments under several kinds of hypotheses (Burkholder 1973, §1).
The present mission concerns a sharper phenomenon for a nonnegative martingale. If the process is stopped just before its absolute value first exceeds a fixed threshold, the resulting square function has an exponential moment of its square. The distinction matters: a second moment controls one scale of variation, while an exponential square moment controls a range of larger deviations. Burkholder states the second-moment stopped estimate in Lemma 2.1 and the exponential estimate in Theorem 18.1 (Burkholder 1973, pp. 21, 35).
Let be a probability space with an increasing sequence of sub--fields . A martingale is observed relative to . Burkholder sets for the purpose of defining its difference sequence: and for . For each let
Fix . The exit time is , with if the set is empty. The quantity in this mission is . On a path with it includes differences only through ; on a path with it is . Nonnegative means almost surely for every . These conventions are those of §§1, 2 and 18 of the paper (Burkholder 1973, pp. 20–21, 35).
The goal is Theorem 18.1. For every nonnegative martingale and every , is finite almost everywhere and
The constant and the full range of are part of the target; replacing the claim by the existence of one positive exponential parameter would lose the paper's quantitative conclusion (Burkholder 1973, Theorem 18.1, p. 35).
The milestone path contains four statements from the paper. Lemma 2.1 bounds the second moment of the stopped square function and stopped value. Display (18.5) bounds an integrated tail past by times the tail at . The paragraph following it gives the full integrated-tail bound with . Lemma 18.1 converts an integrated-tail condition for a nonnegative measurable function into an exponential moment estimate. The milestone order follows their role in Theorem 18.1, while the tail-to-moment lemma also stands independently of martingales (Burkholder 1973, pp. 21, 36–37).
The theorem gives a uniform quantitative bound for the square function accumulated before a nonnegative martingale crosses . It strengthens the conclusion available from Lemma 2.1 under boundedness. The tail-to-moment lemma has a second use later in the paper: Burkholder invokes it for the square function of a martingale satisfying a bounded conditional-tail condition in Theorem 19.1 (Burkholder 1973, §§18–19).
The mathematical result is proved in the paper. This mission asks for a machine-checked development of its precise statements. That development would make the stopped square function, its exit-time convention, the integrated-tail estimates and the exponential-moment implication available as individually reusable objects. No machine-checked proof of these statements is known on Prove2Me; the related martingale inequalities already there (Doob's maximal inequality, an bound for Robbins–Monro noise sums) have different data and conclusions.
The first obvious estimate, Lemma 2.1, gives a second moment but does not by itself give an exponential moment. The exit time also depends on the same martingale path whose variation is being measured, so a fixed-time estimate does not immediately describe . Nonnegativity is essential to the stronger statement: the paper contrasts the general -bounded case, where it states only control, with the nonnegative case, where it asserts exponential square integrability (Burkholder 1973, pp. 21, 35).
Lean uses Mathlib's filtration and martingale predicates for a real-valued process indexed by natural numbers. The paper starts at index and fixes only in its difference sequence. Mathlib's martingale predicate also constrains an auxiliary value at index ; any paper martingale can be extended there by a conditional expectation. Every square function and exit time in this mission ignores that auxiliary value. Nonnegativity is almost everywhere at each positive index. The convergence value in Lemma 2.1 is supplied with an almost-everywhere convergence hypothesis, recording explicitly the convergence that follows from the paper's boundedness assumption.
Square functions, norms, tail probabilities and their nonnegative integrals take values in . This represents a genuinely infinite square function without a default real-valued supremum. At , subtraction of one in leaves , as the paper intends. The exponential-moment statements assert almost-everywhere finiteness before converting an extended value to a real exponent; otherwise the conversion of to zero could make a false bound look true. The threshold is positive, and the same appears in the stopping time and in every bound.
The shared definition layer also records the paper's maximal function, norm, conditional square function and class of functions of moderate growth for reuse across this nine-mission series. The conditional square function uses generalized nonnegative conditional expectation. Its condition includes the endpoints and ; these add no restriction under the paper's continuity and zero-at-zero conventions. The zero function is allowed, since the inequalities in which it appears then hold trivially. Contributions establishing the four milestones, the needed stopping-time measurability facts, or the goal theorem are within scope. A version that assumes the desired exponential moment, or replaces by a fixed-time square function, would miss the target.
Actuaries, reliability engineers and demographers ask how much longer an item or a person will live given that it has already survived to a great age . For a lifetime with distribution function , this is the law of the residual life time given , and the question is what this law looks like as . Balkema and de Haan (Ann. Probab. 2 (1974) 792–804) determined all possible limit laws of the suitably normed residual life time and the distribution functions attracted to each. When only a scale normalization is allowed, the possible continuous limits are the exponential law and the Pareto-type laws , the counterparts in residual-life theory of the Gumbel and Fréchet laws of extreme value theory. Both theories rest on Karamata's theory of regular variation (de Haan 1970).
Section 5 of the paper restates the domain of attraction of in terms of moments: weak convergence of the scaled residual life times is equivalent to convergence of a single conditional moment of the scaled residual life. For an exponential limit the analogous link between weak convergence and first moments had been studied by Meilijson (1972). Moment conditions of this form underlie the mean-excess and Hill-type diagnostics used in heavy-tail statistics and in the peaks-over-threshold method (Pickands 1975).
Let be a real random variable with law and distribution function , and write for its tail. The standing assumption is for every real , i.e. : has no finite upper endpoint, and conditioning on makes sense for every .
For , the conditional distribution function of given is
which vanishes for . For a real exponent , the conditional -th moment is
For the limit law is for and for . The shifted function equals for : the Pareto law of index on . The distribution function is in the domain of residual life time attraction when
In Lean the tail is BalkemaDeHaan.LimitTypes.tail; the scaled conditional distribution and moment are BalkemaDeHaan.Moments.scaledResidualCDF and BalkemaDeHaan.Moments.condMoment. The limit law is BalkemaDeHaan.ParetoBounds.GammaLaw.
For for all and :
the left side being . 2. The value of the limit: for . 3. The "only if" half: implies a finite -th moment and convergence of the conditional moment to . 4. The "if" half, corrected: the converse.
The theorem replaces a distributional limit, required at every , by one numerical limit, for any order . In statistics this justifies testing or estimating heavy-tail behaviour through empirical conditional moments above a high threshold, and it identifies the limit value , from which can be read off. Combined with Theorem 4 of the same paper (), it gives a moment criterion for the Fréchet domain of attraction of extreme value theory.
The result is classical and proved, by reduction to Karamata's theorem on integrals of regularly varying functions. No machine-checked proof is known. Mathlib has no theory of regular variation, no Karamata theorem and no domains of attraction, so a formal proof also produces a reusable piece of the theory of regularly varying tails: the direct and converse halves of Karamata's integral theorem for tails of probability laws.
Both directions pass through the asymptotics of against . The direct half requires uniform control of over to exchange the limit with an integral over an unbounded range; pointwise convergence of the tail ratio alone does not dominate the integrand. The converse half must recover regular variation of from the behaviour of a single integral functional, and here the limit value matters: the page's hypothesis that the limit merely exists does not identify (see below), so an argument that never uses the value cannot succeed.
μ : Measure ℝ with IsProbabilityMeasure μ; for all is ∀ x, 0 < μ (Set.Ioi x). All conditional quantities divide by μ (Set.Ioi t), which this hypothesis keeps nonzero.IntegrableOn (fun y => y ^ ξ) (Set.Ioi 0) μ (real power on positive bases). In the "only if" half it is part of the conclusion, never an assumption; Lean's value for a non-integrable Bochner integral therefore cannot make the statements hold trivially. Milestone 1 asserts integrability of on as well.Tendsto … atTop along real ; the limit form of is required for every , as printed (the limit is continuous, so this is weak convergence). The goal uses this explicit form, the one given after "i.e." on the page, not a separate definition of .ProbabilityTheory.cdf) is ; milestone 2 asserts such a measure exists and computes the moment for every such measure.A complete development needs regularly varying functions, uniform convergence (or Potter bounds) for regularly varying tails, and Karamata's integral theorem with its converse; all are reusable beyond this mission. Proofs of the milestones, of these general tools, and of the Pareto moment computation are welcome.
A lifetime observed only after it has survived to a high age is described by its residual life: the additional time until failure, conditional on survival so far. Reliability analysis asks whether these conditional distributions settle into a stable shape after scaling and shifting. Extreme-value theory asks a related question about the largest observation in a large independent sample. Balkema and de Haan identify an exact connection between these questions for the exponential residual-life limit and the Gumbel maxima limit in Theorem 3 of their 1974 article. The connection lets one recognize the asymptotic form of old-age lifetimes from the domain of attraction of sample maxima, provided the lifetime distribution has no finite upper endpoint.
The article studies several residual-life limits. This mission isolates its exponential case, where the limiting conditional excess has distribution function for . The other continuous family and the paper's discrete limits have separate hypotheses and attraction domains; they are outside this theorem.
Let have a probability distribution function on , and let its survival function be . For a threshold with , the residual-life distribution function is
It is zero for . The class consists of the distributions with for every real . This says that the upper endpoint is infinite and makes meaningful at every threshold.
A law belongs to the domain of residual-life attraction when and there are a positive scale and a shift such that converges weakly to as . The shift here acts on , the residual lifetime. Weak convergence means convergence at every continuity point of the limiting distribution function; it does not require convergence at a jump.
For maxima, belongs to the domain of attraction if there are sequences and for which converges weakly to as . The power is the distribution function of the maximum of independent observations after the indicated normalization. The relevant limit laws are the exponential residual-life law and the Gumbel law:
These definitions and formulas come from the introduction and §2 of the published article, printed pages 792–793 and 798.
The goal is the identity stated on printed page 798:
Both inclusions are required. In particular, membership in the maxima domain alone is insufficient: the maximum of a sample can have a Gumbel limit even when the underlying distribution has a finite upper endpoint, while residual life cannot be conditioned on survival beyond that endpoint. The condition is therefore part of the mathematical claim.
The milestone list follows the statements used in the article's treatment of Theorem 3: the convergence-of-types remark on page 795; Lemma 3's asymptotic ratio ; the tail criterion associated with Gumbel attraction; the inclusion ; and the passage from this tail limit on to all . The last step retains the same normalization sequences. The article presents the criterion in one direction and relies on its converse at the end; the formal milestone records both directions with the same sequences.
The identity translates a conditional limit at a moving high threshold into a classical maxima-domain statement. A theorem about sample extremes can therefore characterize whether normalized remaining lifetime is asymptotically exponential. Conversely, observing exponential residual-life attraction determines a Gumbel maxima limit once the tail normalization is extended across the real line. The condition marks exactly where the conditional lifetime exists; omitting it would misstate the equivalence.
The article proves the result mathematically. The Lean targets here provide a precise representation of its distributions, normalizations, and limiting claims, with Theorem 3 still posed for formal proof. A complete development would add proofs of the supporting tail and convergence-of-types statements, then establish both inclusions. The definitions of weak convergence at continuity points, survival functions, and attraction domains can also support later formalizations of the paper's Pareto and discrete cases.
The simple comparison only relates the two limits after a suitable normalization is already available. The reverse direction starts with conditional residual-life convergence indexed by real thresholds, whereas maxima attraction needs a sequence indexed by integers. Sampling thresholds must preserve the tail asymptotics despite possible atoms. More seriously, the residual-life statement initially yields the required scaled-tail convergence only for positive arguments. The maxima limit must hold on the whole real line. A proof confined to that half-line cannot establish ; the continuation across its left boundary is the central difficulty highlighted by the article on printed pages 798–799.
Lean represents as the cumulative distribution function of a probability measure on and uses real-valued probabilities of intervals for and . The residual-life denominator is positive wherever is asserted. The extrema normalization is indexed by natural numbers, while the residual-life normalization is indexed by real thresholds. The scale is positive at every index; only large indices affect the limit. Weak convergence is encoded at every continuity point of the limit. As and are continuous, their particular domain conditions amount to convergence at every real argument.
The paper uses two shift conventions: shifts , while the scaled-tail expressions shift . Each statement uses the convention of its source passage. The convergence-of-types remark makes explicit the antitonicity and right-continuity of its limiting tails and states its identity where both arguments lie in the half-line on which convergence is known. Gnedenko's criterion is formalized as an equivalence: the printed sentence states the forward implication, and the conclusion of Theorem 3 uses the converse. The page-799 expression has a missing in the denominator; the formal statement uses the intended , consistent with conditional probability and with equation (11). These choices prevent a zero-denominator quotient or an out-of-domain limit identity from trivializing a target. In particular, is part of the definition of : without it a law with a finite upper endpoint would have for large , the conditional distribution would be the junk quotient , and the domain would be mis-specified. In Lemma 3 the limit is the distribution function of a probability measure, assumed continuous on all of .
The development needs measure-theoretic cumulative distributions and interval probabilities, filters for limits, and real exponential identities. The domain definitions and scaled-tail predicate are reusable beyond this theorem. Contributions that prove the stated milestones, or supply general lemmas about weak convergence and normalized tails, fit the scope.
A component that has survived to age has a residual life time , and in reliability, actuarial work and the analysis of excesses over high thresholds the question is what its conditional law looks like when is large. Balkema and de Haan (Ann. Probab. 2 (1974), 792–804) answered this in full generality: after an affine normalization, the only possible limit laws are the exponential law , the Pareto-type laws , and a two-parameter family of discrete laws . The continuous half of their classification became the Pickands–Balkema–de Haan theorem behind the peaks-over-threshold method of extreme-value statistics. The discrete half is less known, and this mission treats it: Theorem 5 of the paper (§3, p. 800) describes exactly which lifetimes are attracted to .
Discrete limits appear only when the normalization is allowed both a scale and a shift. They describe lifetimes that live, asymptotically, on a lattice-like set of ages whose spacing grows geometrically, with a fixed fraction of survivors failing at each lattice point.
The source is the published article in The Annals of Probability (DOI 10.1214/aop/1176996548); page numbers below are the journal's.
Let be a real random variable with law , distribution function and tail , and assume for every . The residual life distribution function at age is (1), p. 792,
A family of distribution functions converges weakly to if at every continuity point of . The domain of residual life time attraction (p. 798) is the set of with for all for which some and give
For and the discrete limit law is (p. 793), for ,
and for ; is the integer part. Its tail takes the values and jumps at , (at if ).
A distribution function is discrete with jump sequence if the are unbounded, each carries positive mass and there is no other mass. Two distribution functions with for all are tail equivalent if as . The conditions of §3 are
For and ,
Theorem 5, together with Theorems 1, 3 and 4 of the paper, completes the description of residual-life attraction: every nondegenerate limit is of one of the listed types, and each type's domain of attraction is identified. For the discrete types the answer is a statement purely about the geometry of the atoms of an approximating law, which makes membership checkable for concrete lifetimes (geometric-type laws on fall under , laws on a geometric grid under ). It also explains why discrete limits are invisible when only a scale normalization is allowed.
The theorem has been proved since 1974; it has not been formalized. A machine-checked development would supply weak convergence of distribution functions at continuity points, residual-life normalizations and tail equivalence as reusable objects, and would check a proof that the paper compresses into a page, including a convergence-of-types step on a half line that the paper cites from its own §1.
The "if" half is close to a computation, but the computation is about weak convergence to a step function: the normed tails converge only off the jumps, and the normalization must be extended from the jump times to all real ages .
The "only if" half is the core. From alone one has to manufacture the atoms of a discrete law that itself need not have. The obvious attempt, reading the atoms off the jumps of , fails because may be continuous: membership in only says that drops by a factor close to over short stretches, relative to the normalization, and never by an intermediate factor. Making "never by an intermediate factor" precise uniformly in the age , with normalizations about which nothing but their existence is known, is where the work lies; the same lack of control over is what makes the gap ratio (12a) hard to extract.
A law is a measure μ : Measure ℝ with IsProbabilityMeasure μ; the tail is (μ (Set.Ioi x)).toReal, and is μ((t, t+x]) / μ((t,∞)). (InDr) includes for all , normalizations for all real , and "weakly" means convergence at every continuity point of and nowhere else; requiring convergence at the jumps of would make empty. (piPC) is defined by cases / with Int.floor, so that is not the junk value of a division by zero; it is used only with , . A discrete law with jump sequence (IsDiscreteWithJumps) has strictly increasing and tending to , positive mass at each and no mass elsewhere. (12a) is indexed from . Tail equivalence (TailEquiv) includes for both laws.
Conventions and disclosed readings:
No statement is trivialized: is nonempty (the geometric law on lies in ), and Theorem 5 is not a definitional unfolding, since is defined by weak convergence and the right-hand side by discrete approximation.
A complete development needs: weak convergence of distribution functions at continuity points, a convergence-of-types lemma on a half line (the Remark after Lemma 1 of the paper, p. 795), and elementary facts on step functions. The first two are reusable across the whole paper and across extreme-value theory. Contributions of either half of the theorem, or of the convergence-of-types lemma, are welcome.
Szemerédi's regularity lemma partitions the vertex set of any graph into a bounded number of parts between which edges are distributed almost randomly. It is a central tool of extremal graph theory, but the number of parts it needs is a tower of exponentials in , which makes it unusable in algorithms. In 1996 and 1999 Frieze and Kannan introduced a weaker notion, now called weak regularity: a partition is good if, for every pair of disjoint vertex sets , the number of edges between them is predicted, up to an additive error , by the densities between the parts. This weaker requirement is enough to approximate dense instances of Max-Cut and other problems, and it can be met with only parts.
The paper Frieze and Kannan, Quick approximation to matrices and applications, Combinatorica 19 (1999) derives such partitions from a matrix decomposition. Section 5.1 shows that if the adjacency matrix of a graph is approximated by a sum of a few cut matrices with small error in the cut norm, then the atoms of the sets defining those cut matrices form a pseudo-regular partition. The weak regularity of this paper later became the basis of the cut-distance theory of graph limits (Lovász, Large networks and graph limits, AMS, 2012).
Let be a simple graph with vertices and adjacency matrix . For a real matrix and write . A cut matrix has entry on and elsewhere. A cut decomposition of width is a sum of cut matrices ; its error is .
Let be a partition of with index set , write , let be the number of edges between disjoint sets and , and let be the density between parts. The deviation from regularity is
and is -pseudo-regular if for all disjoint .
For a partition , the block average of takes the value on , and is compatible with if it is constant on every block . The atom partition of is the coarsest partition of in which every and is a union of parts; it has at most parts.
If the cut decomposition has error at most , that is
then the atom partition of the sets satisfies
i.e. it is -pseudo-regular. The width is unconstrained: the statement holds for decompositions of any width, and the width only enters through the bound on the number of parts.
Claim (50) is the bridge from matrix approximation to graph partitions. Combined with Theorem 7 of the same paper (every matrix has a cut decomposition of width at most with cut-norm error for a graph), it gives the weak regularity lemma: every graph has a -pseudo-regular partition into at most parts. Pseudo-regularity in turn means that is determined up to by the numbers , which reduces Max-Cut and related problems on dense graphs to a search over a bounded-dimensional space. Lemma 7(a) is of independent use: Section 5.1.1 of the paper applies it again to pass to an equitable refinement.
The results are proved in the paper. Mathlib contains Szemerédi's regularity lemma in its equipartition form, and the platform has a published statement of it; neither the Frieze–Kannan weak regularity statement, the deviation , nor Lemma 7 has a machine-checked proof known to this mission. The mission produces a formal statement and proof of the partition half of the weak regularity lemma, reusable with any cut decomposition, including the existence result of the companion mission on cut decompositions.
The identity (47) and the compatibility of are bookkeeping, but bookkeeping over Mathlib's Finpartition, atomise and the rational-valued edgeDensity, with sums over parts that must be regrouped into sums over vertices. The substance lies in Lemma 7(a). The obvious argument bounds by , and the difficulty is the second term: is constant on the blocks of , but its block sums on arbitrary have to be controlled by block sums of , on which and need not agree. The printed argument handles only disjoint , while the lemma is stated, and needed, for all pairs; a complete proof must cover pairs that overlap.
All objects are defined in one definitions item in the namespace FriezeKannan.PseudoReg. The vertex set is a Fintype with decidable equality, the graph a SimpleGraph V with decidable adjacency, and its adjacency matrix Mathlib's adjMatrix over . A partition of is a Finpartition of Finset.univ, whose parts are the index set ; refinement is Mathlib's order . Densities are SimpleGraph.edgeDensity, cast to , for all pairs of parts. For distinct parts this is the paper's . For a part with itself it is the block average , not the value printed in the §5 preamble: with the printed value the identity (47) fails on diagonal blocks, and the proof of (50) uses (47). The atom partition is Mathlib's Finpartition.atomise of the family . The Frobenius norm is the square root of the sum of squared entries.
The paper takes the cut matrices from its Theorem 2, a randomized algorithm. The goal replaces this by the one property its proof uses: the hypothesis for all (Theorem 2 bounds the cut norm, a maximum over all pairs, by ). The paper's symmetrised error is not needed. Lemma 7 is stated for an arbitrary real matrix , and the suprema of Lemma 7(a) are written as "every bound on the right-hand family gives the bound on the left-hand family", over all pairs . No hypothesis is added to any statement.
The partition in the goal is fixed as the atom partition. A formalization that let the partition vary would be trivial: the partition into singletons has .
Needed infrastructure: regrouping sums over a Finpartition, and block sums of matrices constant on the blocks of a partition, on arbitrary and on block-compatible sets. These are reusable for any statement about cut norms of block-constant matrices. Proofs of the milestones, of the companions, and of the goal are all welcome.
Bound constrained minimization asks for a low value of a smooth objective while each variable stays between prescribed lower and upper limits. Such limits occur in nonlinear optimization models even when the objective itself has no special convexity. Coleman and Li's interior reflective method was designed to approach a solution from inside those limits while using curvature information from a Newton system. Its local convergence claim explains what the method does after an iterate reaches the neighborhood of a suitably regular solution. The source is Coleman and Li (1994), especially Section 6 and Theorem 13.
The local result is distinct from a claim about finding that neighborhood. An algorithm can have excellent behavior near a solution without being guaranteed to reach it from every starting point. This mission isolates the precise local claim for the method in Fig. 11, including its reflected motion at a bound. It also records a regularity correction: the paper's stated twice continuous differentiability assumption alone does not imply a quadratic rate.
Let be the objective and let describe a box . A lower bound may be and an upper bound may be . The strict interior consists of points satisfying for every coordinate. Write and .
The method's scaling vector selects a bound according to the sign of . If , it uses when is finite and otherwise. If , it uses when is finite and otherwise. Put . The first order equation is . At an interior point, Fig. 11 chooses a scaled Newton direction from and sets , where is the scaled Hessian plus the diagonal correction in (2.5).
A reflective path follows and folds a coordinate back into the box whenever it crosses a finite bound. For a bounded coordinate this folding repeats after later crossings. The accepted value obeys and produces another strict interior point. Fig. 11 prints the rule as ; the squared scaling is a second disclosed correction, explained below. The iteration is .
At a candidate limit point , nondegeneracy says that any coordinate with lies strictly between its bounds. The free coordinates are those strictly between bounds. The second order sufficient conditions used here require that is feasible, , and the Hessian quadratic form is positive on every nonzero direction supported on the free coordinates. Section 6 also defines a finite family whose allowed coordinate choices come from (6.4). Coleman and Li, pp. 193–194 and 211–213 give these definitions and the local algorithm.
The supporting targets establish that the family vanishes at and has regular Jacobians there, that a scaled Fig. 11 direction is a Newton step for one family member, and that the reflected displacement is close to that direction. Lemma 12 makes the closeness quantitative at the coordinates that are active at . Theorem 11 states the corresponding abstract local Newton result for a finite family of maps. These are the five milestones of the mission, ordered from the model and abstract estimate through the step and path estimates.
The goal is the corrected local form of Theorem 13. For a fixed bound on the permitted step size deviation, a common neighborhood and constant work for every Fig. 11 run starting there:
The radius and are chosen before the run. A companion statement asserts that, when , a nearby interior point begins at least one run satisfying the algorithm's conditions.
The theorem gives a local rate for a feasible Newton method that can meet and reflect from finite bounds. It connects the behavior of the actual reflected iterates to Newton systems whose Jacobians are regular near . This matters when the solution is on the boundary: convergence of an unconstrained Newton step by itself says nothing about whether the iterates remain feasible. Theorem 13 is a known paper result, and this mission asks for a machine checked proof of its corrected statement. None of this mission's seven draft theorems has a proof in the proposal; the published box definition is reused as an existing platform object.
The correction is mathematically material. In the one dimensional problem with no finite bounds and , the objective is and meets the paper's nondegeneracy and second order conditions. Fig. 11 with reduces to ordinary Newton iteration, whose error is of order rather than . The source's proof invokes the Lipschitz Jacobian condition (6.5) of Theorem 11; the goal therefore assumes the Hessian is locally Lipschitz at . This changes the literal hypotheses of the printed Theorem 13 and is disclosed in each relevant item.
The step-size rule needs a second correction. The proof on p. 212 asserts and so . On with and , however, , the Newton step is , and obeys the printed rule while giving . The run predicate therefore bounds by , which is as the proof needs and is still computable without knowing . Coleman and Li, Theorems 11 and 13 are the source of the two compared claims.
The scaling changes its coordinate formula when a gradient component changes sign, while the reflective path changes direction at each finite bound. A direct Newton estimate for an unreflected step does not control the displacement taken by Fig. 11. The finite family and the active-coordinate breakpoint estimate make the local statement precise across those choices. The abstract rate also needs a uniform regularity estimate for every member of that family. Twice continuous differentiability gives continuity of the Hessian, but it does not supply the linear modulus of continuity needed for a quadratic error bound.
The variables are Euclidean vectors indexed by ; the paper's first iterate is Lean's sequence index zero. Bounds use extended reals, while all distances, derivatives and norms use real Euclidean space. A published definition supplies ; this mission defines the strict interior, scaling, diagonal Newton correction, reflective map, run, nondegeneracy and second order condition, and the family . The bounded-interval reflection uses the paper's repeated folding, including steps beyond the first breakpoint. Division in Lemma 12 is accompanied by a nonzero Newton component, and Newton directions are solutions of linear equations rather than values of a possibly undefined inverse.
The paper's standing assumption says that the initial sublevel set is compact and that is on an open set containing . The local statements retain the smoothness clause and omit compactness because no local conclusion uses it. The sole added regularity hypothesis in the goal is local Lipschitz continuity of at ; the run predicate uses the corrected step-size rule . The existence companion requires : if it were zero, the only allowed step size could hit a bound exactly. Neither the goal nor the run predicate assumes the iterates are already close after the start, that they converge, or that the scaled step is a Newton step for a chosen ; those are the claims to establish. A feasible interior start is required, so a box with an empty strict interior has no run. Contributions on the general finite family Newton estimate, active-coordinate ratio, reflected path, and existence of interior runs are all directly useful to the goal.
Economic lot sizing asks when to produce goods across a finite planning horizon when demand in each period is known. Producing in a period incurs a fixed setup charge and a marginal cost per unit, while goods may be produced before the period in which they are needed. Such a decision has to balance paying another setup charge against producing more units earlier. The model is a standard setting for studying how dynamic programming and linear optimization describe the same planning decision. Wagelmans, Van Hoesel and Kolen study faster algorithms for this model and, in Section 4, connect the optimal lot-sizing cost to a greedy solution of a dual program Wagelmans et al. (1992).
The dual connection is useful in its own right. It supplies a certificate for the cost returned by the forward dynamic program: a feasible dual vector attains that cost. The paper allows demand to vanish in some periods, which makes the dual values at those periods free and forces care in defining the dynamic program. The mission targets precisely that case.
There are periods . Demand and setup cost are nonnegative for the periods in the horizon. The marginal production cost is any real number. Write for cumulative demand from through . Values at period zero and beyond the horizon are bookkeeping only; every optimization constraint concerns periods .
The forward lot-sizing cost describes the least cost of serving periods under the zero-inventory property cited by the paper. Its recursion starts with . If , no new production is needed and . If , the last production setup may occur at some , giving
This piecewise definition matters even when only one period has zero demand. Taking the displayed minimum at would charge a setup that need not occur.
Program D′ chooses free real values to maximize , subject to
“Free” means there is no nonnegativity constraint on . The paper obtains D′ from the dual of the linear relaxation of its simple plant location formulation, using the variables of Formulation III Wagelmans et al., pp. S147, S152–S153. The mission takes D′ as the defined optimization problem.
The greedy forward rule visits periods in increasing order. At a period with , the chosen value is the minimum of the upper bounds left by the constraints indexed :
When , the rule places no restriction on . This matches the paper's statement that it may be assigned an arbitrary value. One concrete recursive vector in the definitions sets each such value to zero, but the goal covers every assignment.
The goal says that every vector satisfying the greedy rule is feasible for D′, agrees with the dynamic-programming cost at every prefix, and is optimal among all feasible D′ vectors:
The milestone path follows the Section 4 statements: feasibility of the greedy vector; decreasing greedy values across positive-demand periods; the prefix upper bound for any feasible dual vector; and Equation (2), which expresses a greedy prefix value using a minimizing production period. Equation (2) is stated with the induction hypothesis that appears immediately before it in the paper. The goal combines these claims without treating the desired value identity as a hypothesis.
The result identifies a dual certificate whose value matches the forward lot-sizing cost. It also explains why a greedy forward assignment can solve D′ despite each constraint linking the current value with all later periods. The full-horizon identity recovers the cost , and the comparison with every feasible vector makes the word “optimal” precise. The paper additionally says that this dual computation directly provides an optimal primal solution; this mission does not encode that reconstruction because it would require the primal formulation and its correspondence to Wagelmans et al., p. S153.
A formal proof would provide a reusable finite-horizon certificate theorem for this dual formulation and a careful treatment of empty and zero-demand prefixes. The paper's result is already proved mathematically. The Lean files in this proposal state the goal and its milestones; their theorem proofs remain to be supplied by solvers. Related platform goals about the convex hull of other lot-sizing formulations and the Federgruen–Tzur forward algorithm concern different objects, so they are credited as neighboring work rather than imported as this theorem.
A current greedy value is limited by every earlier production index, and feasibility must still hold for the entire horizon, not merely for the constraints truncated at the current period. Equality with also has to survive periods with zero demand, where the dual coordinate is unrestricted but its weighted contribution vanishes. The forward recurrence has a separate branch at exactly those periods. A formulation that assumes every demand is strictly positive would avoid the delicate case and would miss a feature the authors explicitly retain.
Lean represents the horizon by natural-number indices and the demand, setup, marginal-cost and dual sequences by functions . Finite sums use closed intervals; the sum before period uses , so it is empty when . Minima are over the nonempty finite set , only when . The horizon has empty sums and no constraints. The cost and dual values are real, with no sign condition on or .
Several informal phrases are made explicit. “The solution is feasible” means every D′ constraint through holds. “Optimal” includes feasibility, every prefix identity, and comparison with every feasible dual vector. “Can be given an arbitrary value” is represented by no greedy-rule condition at zero demand; the theorem quantifies over all vectors that satisfy the positive-demand conditions. The paper states monotonicity for consecutive nonzero-demand periods; the milestone uses any two positive-demand periods, skipping zero-demand positions so it holds for every choice of their dual values. The weak-duality milestone spells out the paper's reference to “duality and the structure of D′” as an inequality for each feasible vector and prefix.
The identification of with the optimum of the primal lot-sizing model relies on the zero-inventory property cited by the authors and is not separately formalized. Neither the equivalence of Program D and D′ nor the recovery of a primal production plan is an item here. The paper's running-time claims, including for the greedy forward algorithm and for its backward algorithm, are outside the scope: the paper does not fix a machine model or constants for them. A definition of as the optimum of D′ would make the value identity circular; the proposal defines it by the paper's forward recursion instead. The backward algorithm of pp. S153–S155 belongs to a separate development.
The multi-armed bandit problem asks how to allocate effort sequentially among independent projects, only one of which can be worked on at a time, so as to maximise expected total discounted reward. It is the model behind research planning, clinical-trial allocation and job scheduling, and it is the prototypical example of a Markov decision problem whose state space grows exponentially in yet whose optimal policy is simple. Gittins and Jones (1974) and Gittins (1979) showed that each project can be given an index computed from that project alone, and that it is optimal always to engage a project of largest index. P. Whittle's 1980 paper gave a short proof of this theorem by attaching a retirement option to the process, and extended it to projects with individual horizons.
Timeline:
There are projects. Project has a state in a measurable space . Engaging project in state earns the expected reward and moves its state by a Markov kernel ; the other projects' states do not change. Rewards are discounted by , , and bounded:
The operator evaluates engaging project for one step.
In the -process one may also retire at any time for the reward . Its value solves (4), and the value of the single-project -process solves (9).
With per-project horizons, project may be operated at most more times. A project with is active, and lowers by one. The single-project value satisfies and
is the maximal expected reward of the -process under these limits. The index is the infimal with , and is the Gittins index. Finally
and is attained by the policy that, at , engages a project maximising when this maximum exceeds , and otherwise retires. The Lean goal has three conjuncts: , every measurable index rule (any tie-breaking) earns , and no feasible measurable Markov policy earns more than .
Theorem 1 reduces an -project problem, whose state space is a product, to one-dimensional retirement problems. The formula (13) shows more than optimality of the index rule: the derivative of the multi-project value in is the product of the single-project derivatives, so the multi-project value is computable from the projects separately. The finite-horizon version gives an inductive argument that avoids the interchange arguments of earlier proofs, and the infinite-horizon identity (12) follows from it.
The result is classical and proved. What this mission adds is a machine-checked version in a generality not yet on the platform: heterogeneous projects (each with its own kernel and reward on its own measurable space), a retirement option, and per-project horizons. The platform already has a proved index theorem for identical arms sharing one kernel and reward without retirement, BanditAlgorithm.gittins_index_theorem (Lattimore–Szepesvári, Theorem 35.9), single-arm retirement values in charge form (GittinsFiniteRetirementValue), and open Beta–Bernoulli special cases from Bäuerle–Rieder (MDPFinance.InfiniteHorizonApplications.proposition_7_6_7, proposition_7_6_9, theorem_7_6_10). None of these states Theorem 1, formula (13) or formula (12).
The obvious approach, value iteration on the product state space, gives existence of an optimal policy but says nothing about its structure. The content of Theorem 1 lies in the identity of a multi-dimensional value with an integral of a product of one-dimensional derivatives. Verifying it requires differentiating single-project values in (they are convex, but have a kink exactly at the index, where the choice of one-sided derivative matters), an integration by parts against a Stieltjes measure in , and an exchange of the expectation over the next state with the -integral. The exhausted projects () and the boundary need separate care in every step.
Fin N (0-based; the paper uses ). State spaces are arbitrary measurable spaces; no finiteness or countability is assumed. Kernels are Markov, rewards measurable and bounded as in (1), and (β = 0 is allowed). and are any constants satisfying (1).s : Fin N → ℕ; is Function.update s i (s i - 1) and is only applied to active projects.index takes the junk value 0 there; every use (the index rule, , ) ranges over active projects only.Option (Fin N) (none = retire), feasible (they engage only active projects) and measurable (each decision set is measurable), so that their expected rewards are well defined. The index rule allows arbitrary tie-breaking; the goal quantifies over every such rule.A complete development needs measurability of the recursive values, convexity of in with one-sided derivatives, Lebesgue–Stieltjes integration by parts, and Fubini for kernels. Convexity of finite-horizon retirement values and the integration-by-parts identity are reusable beyond this mission. Contributions to any milestone, and sorry-free lemmas on these ingredients, are welcome.
Universities schedule lectures and examinations every term. When students choose their courses freely, with no fixed curriculum, the basic requirement is that no student is asked to attend two lectures at the same time. On top of this come local constraints: a course cannot take place at some periods (its teacher or a suitable room is unavailable), and some lectures are fixed in advance at a given period. D. de Werra's invited review An introduction to timetabling (Eur. J. Oper. Res. 19 (1985) 151–162) surveys the graph models of these problems. Its §3.1 shows that course scheduling, with unavailabilities and preassignments, is exactly a node colouring problem. This reduction is the standard starting point for graph colouring heuristics in timetabling, including the examination timetabling literature.
A course scheduling instance has courses , course consisting of lectures , and students; student takes a set of courses. There are periods.
The lecture graph has one lecture-node for each lecture of each course . Two lecture-nodes of the same course are adjacent. Two lecture-nodes of distinct courses , are adjacent whenever some student takes both courses.
A feasible course schedule in periods assigns a period to each lecture so that two lectures of one course are at different periods and no student has two lectures at the same period.
A course scheduling problem with unavailabilities and preassignments (CSUP) adds, for each course , a set of forbidden periods, and for some lectures a prescribed period . A solution is a feasible schedule with for every lecture of and for every preassigned lecture.
The graph of a CSUP adds one period-node per period to . All pairs of period-nodes are adjacent. A lecture-node of is adjacent to period-node if . A lecture-node of a lecture preassigned to is adjacent to every period-node .
A node colouring with colours assigns one of colours to each node so that adjacent nodes get different colours.
The result. Proposition 3.1 turns a family of constrained timetabling problems into one well-studied problem. Any exact or heuristic method for node colouring (sequential colouring, DSATUR, implicit enumeration; §3.2 of the paper) applies directly to course scheduling with forbidden and fixed periods, and lower bounds on the chromatic number become lower bounds on the number of periods. Proposition 3.2 adds that preassignments cost nothing for node colouring: a precoloured instance is again a plain colouring instance. For edge colouring the paper contrasts this with the NP-completeness of precoloured edge colouring.
The formalization. The results are proved on the page in a few lines and are not machine-checked anywhere. This mission makes the reduction precise. It writes out the graph as a definition, isolates the consistency condition that Proposition 3.2 needs, and states the correspondence between colourings and schedules in a form other formal timetabling and scheduling developments can use. The definitions of course instances, CSUP and can serve formal work on examination timetabling and on the complexity of timetabling problems.
The forward direction of Proposition 3.1 is direct: colour each lecture-node with its period and each period-node with itself. The converse is where care is needed. A colouring of need not give period-node the colour ; the colours of the period-nodes can be any permutation of the palette. The schedule must therefore be read through the colours of the period-nodes, and the fact that the period-nodes form a clique is what makes this well defined.
For Proposition 3.2, the obvious reading of the page is false. If two adjacent lecture-nodes are precoloured with the same colour, no colouring respects the precolouring, yet removing both nodes deletes the edge between them and the reduced graph may still be colourable. The same happens when a node is precoloured with the colour of a period-node it is adjacent to. The proposition therefore needs a consistency condition the page leaves implicit. The page's "1–1 correspondence" between colourings fails when precolours are fixed colours of the palette, since 's colourings can permute the colours of the period clique; the target is the equivalence of the proposition.
Courses, students, lectures of a course and periods are indexed from (Fin q, Fin r, Fin (lectures b), Fin p). A lecture is a dependent pair Σ b, Fin (lectures b), and the nodes of are Lecture ⊕ Fin p. Graphs and colourings are Mathlib's SimpleGraph, SimpleGraph.Coloring and SimpleGraph.Colorable. Unavailability is per course and preassignment per lecture, as on the page. The set-valued constraint of the Figure 5 example ("1 lecture of at period 1 or 2") is not modelled. Feasibility includes the clique on the lectures of each course even when no student takes the course, because the page's graph contains it. is allowed.
The paper states Proposition 3.1 as "one can construct a graph such that …". The existential form is trivially true (pick a complete graph on nodes or an edgeless graph according to the answer), so the goal is stated about the specific graph csupGraph P built in the proof.
Proposition 3.2 is stated for any graph whose period-nodes form a clique, with two disclosed consistency hypotheses: no precoloured node is adjacent to its own period-node, and no two adjacent nodes are precoloured with the same period-node's colour. A sanity file shows that the equivalence fails without them. "Precoloured" means "receives the colour of period-node ", the reading of the proof of Proposition 3.1.
Not targeted: the NP-completeness remarks (cited, not proved), the heuristics of §3.2–§3.4, and the hypergraph classroom model of §3.5, whose "1–1 correspondence" has the same palette-permutation issue as Proposition 3.2.
Contributions welcome: proofs of the milestones and the goal, and general lemmas about colourings of graphs containing a clique of size equal to the number of colours.
In 1950 the United States Supreme Court appeared to be moving toward treating corporate integration, horizontal or vertical, as illegal per se under the antitrust laws. Joseph J. Spengler's note in the Journal of Political Economy argued that this conflates two different things: horizontal integration can suppress competition, but vertical integration, the joining of successive stages of production under one owner, can lower prices when the stages are already imperfectly competitive. The note is the standard origin of what industrial organization now calls double marginalization: when a monopolist upstream sells to a monopolist downstream, each adds its own markup, and the final price is higher than a single integrated monopolist would charge.
The argument underlies the modern economics of vertical mergers and vertical restraints (resale price maintenance, two-part tariffs, franchise fees) and the supply-chain coordination literature in operations research, where a wholesale-price contract between a supplier and a retailer reproduces the same distortion.
A short timeline: Cournot (1838, Chapter IX) analysed complementary monopolists selling inputs to a common product; Spengler (1950) gave the successive-monopoly version and drew the antitrust conclusion; Tirole's textbook (1988, §4.2) made it the canonical example of vertical externalities; Cachon and Lariviere (2005) and the coordination literature studied the same inefficiency in newsvendor supply chains.
A product passes through three successive stages before reaching consumers. Production uses fixed proportions: one unit of stage A's product goes into one unit of B's, and one unit of B's into one unit of C's, so all stages handle the same quantity. Each stage has a constant unit variable cost (marginal cost equal to average variable cost at every relevant output).
Final demand is a function : units of are bought at price . A firm with constant unit cost that sells at price earns the profit (return above variable outlay)
and is a profit-maximizing price at cost when for every .
Unintegrated chain. Stage A sells to B at a transfer price , B sells to C at . Their per-unit profits are and ; horizontal integration within each stage lets these be positive "monopolistic surcharges". Stage C's unit cost is ; it charges a profit-maximizing price at that cost and sells . The chain's aggregate profit is with .
Integrated firm. One firm owns all three stages. Its unit cost is ; it charges a profit-maximizing price at that cost and sells , earning .
The price elasticity of demand at is (positive for a downward-sloping curve) and the marginal revenue is . The consumers' surplus gained when the price falls from to is .
For every non-increasing demand curve , all unit costs , and all transfer prices with , , if is profit-maximizing at cost , is profit-maximizing at cost , is differentiable at and , then
The goal fixes no functional form and no numbers; it is the general statement behind the paper's "under all cases conceivable … within the framework here employed".
The result. The theorem shows that removing an upstream markup can only lower the final price and raise output, so that producers and consumers gain together. This is the economic content of the rule that vertical integration is not anticompetitive as such, and it is the reason modern merger guidelines credit the "elimination of double marginalization" as an efficiency of vertical mergers. Milestone 3, monotonicity of the monopoly price in cost, is the general comparative-statics fact used in tax incidence and cost pass-through.
Formalizing it. The result is classical and proved in every industrial-organization textbook, usually for linear demand. The mission states it for an arbitrary non-increasing demand curve, without concavity, continuity or uniqueness of the profit maximizer, which makes explicit which hypotheses the strict conclusions actually need. Related items on the platform formalize double marginalization in a different model, the newsvendor wholesale-price contract of Cachon and Lariviere, where the supplier-induced order quantity falls short of the integrated one; this mission covers the price-setting, deterministic-demand version.
The weak inequalities (, , profit ) follow from comparing the two maximization problems (the price comparison also uses : if , every price is profit-maximizing). The strict inequalities do not: a demand curve with a kink can have the same profit-maximizing price at two different costs, so integration need not change the price at all. The strict claims therefore need a first-order condition at , and the argument has to combine global optimality (all prices) with local information (a derivative at one point) without assuming the profit function is concave or the maximizer unique. The consumers'-surplus clause requires a lower bound on an integral of a monotone, possibly discontinuous function.
Antitone D).IsProfitMax D c p), never closed forms; the closed form appears only for straight-line demand.deriv and division return on bad input.IsLocalMax.hasDerivAt_eq_zero), interval integrals of monotone functions, and real arithmetic. Proofs of the general milestones are reusable for any monopoly-pricing comparative statics.A finite directed graph on vertices is recorded by its adjacency matrix, a array of zeros and ones. Many questions about the graph are questions about reachability: can vertex be reached from vertex by following one or more edges? In the late 1950s this question arose in the analysis of programs. Prosser (Applications of Boolean matrices to the analysis of flow diagrams, 1959) represented the flow diagram of a program by a boolean matrix and read off properties such as which blocks can follow which; Marimont (A new method of checking the consistency of precedence matrices, J. ACM 1959) used the same matrices to check precedence relations for consistency.
In both works the reachability matrix is described as a boolean sum of boolean powers of the adjacency matrix. Computed that way, it costs boolean matrix products, that is on the order of operations per product. Stephen Warshall's two-page note (A theorem on Boolean matrices, J. ACM 9 (1962) 11–12) proves that a much shorter procedure, passes of row updates performed in place, gives the same matrix. The same procedure was published in the same year by Floyd as Algorithm 96: Ancestor (Comm. ACM 5 (1962) 344), and its weighted version is Floyd's Algorithm 97: Shortest Path. The procedure is now taught as the Floyd–Warshall or Roy–Warshall algorithm.
Timeline. 1959: Prosser and Marimont describe reachability as a sum of boolean powers. 1959: Roy publishes the same closure construction in French (C. R. Acad. Sci. Paris 249). 1962: Warshall's note proves the in-place construction correct; Floyd's Algorithm 96 publishes it as code, and Algorithm 97 extends it to shortest paths.
Fix a natural number and let be a matrix each of whose entries is or .
In Lean the matrix is M : Fin d → Fin d → Bool. The power sum is powerSum M, the chain relation ChainRel M i j, the recursion warshallRec M n, all in the namespace WarshallBool.Closure. The construction is the published FloydAlgorithms.ShortestPath.algorithm96 M.
This is the transformation the introduction asks for, combined with the THEOREM's assertion and footnote 2. The goal has no hypothesis beyond the shape of .
It is already on the platform as FloydAlgorithms.ShortestPath.algorithm96_eq_transGen, stated with Mathlib's transitive closure Relation.TransGen, and it is not posed again.
This is not a milestone of the goal; it identifies the in-place construction with its stage-by-stage recursion.
The result. The theorem says that reachability in a directed graph on vertices, defined through matrix powers, can be computed by passes of in-place row operations, on the order of row updates instead of full boolean matrix products. The same scheme, with in place of , is the Floyd–Warshall shortest-path algorithm; with other semirings it computes regular expressions of finite automata (Kleene, McNaughton–Yamada) and path problems in general. Footnote 3's recursion is the form in which the algorithm is usually proved correct today, and its equivalence with the in-place version is what justifies running it without a second copy of the matrix.
Formalizing it. The chain form of the THEOREM is already machine-checked on Prove2Me (algorithm96_eq_transGen). What this mission adds is the statement in the paper's own terms: the introduction's power sum , footnote 2's equivalence between powers and chains, which requires that chains can be shortened to length at most , and footnote 3's in-place versus recursive equivalence. None of these three is on the platform. The paper itself proves only the THEOREM; footnotes 2 and 3 are stated without proof.
Footnote 2 calls the equivalence "trivial", but one direction needs a pigeonhole argument: a chain of arbitrary length witnesses some power , and the power sum stops at . A chain with repeated indices has to be shortened, and the shortening must keep at least one step, since there is no reflexive part ( only through a cycle). For a -cycle the diagonal entries appear only in , so the range is exact.
Footnote 3 compares two computations that read different data. The construction overwrites entries during a pass, and later steps of the same pass read the overwritten values; the recursion reads only the previous stage. The two agree only because of what a pass does and does not overwrite, and the published algorithm96 is three nested left folds over List.finRange, so the comparison has to be made against that concrete loop structure rather than an idealized simultaneous update.
Fin d → Fin d → Bool, with as true. Indices are instead of the page's ; the pivot of pass (1-based) is the 0-based index .boolProd A B i j is decide (∃ k, A i k = true ∧ B k j = true). Mathlib's matrix product on Matrix (Fin d) (Fin d) Bool is not the boolean product: Bool is a boolean ring there, its addition is exclusive or, and that product counts walks modulo 2. A formalization through * or ^ on Matrix _ _ Bool states a different, false theorem and is ruled out.boolPow M p is the page's for ; the base boolPow M 0 is the identity matrix, which is not on the page and does not enter the sum. powerSum M i j holds iff boolPow M p i j for some . No reflexive closure is included anywhere.ChainRel M i j is the existence of a list (possibly empty) making a List.IsChain of true entries.warshallRec M n uses the 0-based pivot at stage and is constant after stage , which footnote 3 never uses.algorithm96, which fixes the inner loops over rows and columns in ascending order; Warshall leaves that order open, and it does not affect the result.TransGen, ChainRel or warshallRec, and powerSum is defined from boolPow, not from the closure or the algorithm.Reusable beyond this mission: the boolean matrix product and powers, the power-sum characterization of the transitive closure of a relation on Fin d (footnote 2), and the in-place/recursive equivalence (footnote 3), which carries over to Floyd's Algorithm 97. Proofs of milestone 2 and of the companion are welcome independently of the goal.
A market in which each trader owns one indivisible good has a basic coordination question: can all goods be reassigned so that no group of traders can withdraw its own goods and improve every member's outcome? Houses are the paper's running example. Monetary transfers and fractional houses are absent, so ordinary convex allocation arguments do not describe the setting. Shapley and Scarf use games without side payments to express what each coalition of owners can achieve, and identify a balance property of this game in their Section 4 theorem (Shapley and Scarf, 1974).
The paper states that a general balanced-game theorem gives a nonempty core once balance has been established. Its Section 4 contribution is the classification of this particular housing market game. The separate top-trading-cycles construction in Section 6 gives another route to a core allocation and is the subject of the second mission in this series (Shapley and Scarf, 1974).
Let be a nonempty finite set of traders. Trader brings one indivisible item . Trader 's ranking of item is represented by a real number . Only comparisons within one trader's row matter: means that prefers to , while equality represents indifference. No strict-preference or positivity assumption is imposed on the preference matrix .
A coalition can redistribute the items brought by its members. Its allocation matrix has when trader receives item , and zero otherwise. An -allocation puts exactly one 1 in each column indexed by and has zeros in rows and columns outside . An -permutation is an -allocation with row sums at most one, so every member of receives exactly one of the coalition's items. Rows index traders and columns index items.
For a proposed payoff vector , define the acceptability matrix
The coalition payoff set is
Thus a coalition can reach a payoff threshold if it can give each member an item that member values at least as highly. The comparison is weak, so ties count as acceptable. This is the characteristic function used in the paper's Section 4 (Shapley and Scarf, 1974, pp. 109–110 of the source printing).
A balanced family is a family of nonempty coalitions with nonnegative real weights , zero outside , such that every trader has total covering weight one:
The weights may be zero even for a coalition listed in . A balanced game is a game without side payments whose feasible payoff sets obey
for every balanced family . This includes overlapping families, not merely partitions (Shapley and Scarf, 1974, pp. 108–109).
The goal is the paper's Section 4 theorem:
It contains four requirements. For each nonempty , is closed; it is downward closed in the coordinates of ; and its payoff slice after removing the interiors of singleton payoff sets is bounded and nonempty. The fourth requirement is the balanced-family inclusion displayed above.
The milestones name the paper's intervening claims in their order: the three game conditions, the identity , the doubly stochastic character of a balanced mixture , and the existence of a grand-coalition permutation when . The final milestone states the matrix existence claim made at the end of Section 4, without committing the theorem statement to a particular construction.
The result establishes that the finite housing market falls under the paper's general balance framework. In the paper, the cited theorem that balanced games have nonempty cores then yields a core existence conclusion for this market. That general existence theorem is external to the Section 4 proof and is not asserted by this mission's goal (Shapley and Scarf, 1974, pp. 109–110).
The formal development supplies reusable definitions of games without side payments and balanced families alongside the market-specific allocation and acceptability matrices. It also gives precise targets for the matrix claims used in the paper. The source result is proved in print; these Lean statements are proposed formalization targets and their proof bodies remain open. Nearby platform items about transferable-utility games, including the Bondareva–Shapley goal, use a real value for each coalition and do not define this paper's payoff-set game. They are not substituted for these objects.
The challenge is the passage from coalition-wise feasibility to feasibility for all traders together. A balancing family can overlap: choosing one feasible permutation for each coalition does not immediately give a single permutation of . Their weighted mixture has fractional matrix entries. The condition also has to survive the move from such a mixture to an actual zero-one permutation matrix. Without that last assertion, the balancing equations alone do not prove the inclusion requires. Separately, the bounded nonempty payoff-slice condition must be checked for every nonempty coalition; merely proving closedness and downward closure would define a weaker class of games.
Traders are an arbitrary finite nonempty Lean type, and payoffs live in . The paper's is encoded as the coordinate subspace of vectors zero outside ; interiors are taken in the product topology on . The boundedness and nonemptiness test applies to the intersection of that subspace with after removing the singleton interiors. All conditions defining a game quantify over nonempty coalitions. The market formula is also defined at , where it yields all of .
Allocation matrices are real zero-one matrices. An -permutation retains the paper's column, support, and row conditions; it is not replaced by an unconstrained permutation of all traders. The inequality between matrices is entrywise. The acceptability matrix has a 1 exactly when and ; its columns are not independently restricted to . Balancing weights are nonnegative, may vanish inside the family, and cover every trader in . These choices exclude the trivializations , balance tested only on partitions, and coalitions using outsiders' items.
The definitions need finite-sum and matrix support from Mathlib, while the eventual proof can use Mathlib's doubly stochastic matrix and permutation-matrix library. Contributions that establish the stated game conditions or any of the four sourced matrix milestones are within scope. The paper's Section 8 counterexample and the optional superadditivity observation are outside this mission's attack path.
Spare-parts provisioning for repairable ("recoverable") items is a classical inventory problem: aircraft components fail, are sent to repair, and a stock of spares covers the units in the repair pipeline. Sherbrooke's METRIC model (Sherbrooke 1968), developed at RAND for the U.S. Air Force, measures the performance of a stock level by the expected number of backorders, the average number of unfilled demands outstanding at a random time. Every allocation computed by METRIC is driven by this quantity, and in particular by how it depends on the mean demand of each item.
For a new item that mean is not known. Air Force practice at the time produced a single engineering estimate of mean demand and computed backorders from it as if it were exact. In the section Demand Prediction (pp. 138–139) Sherbrooke argues that this practice is biased in one direction: under Poisson demand and any positive spare stock, the point estimate always understates expected backorders whenever the true mean is genuinely uncertain. This is his reason why a Bayesian treatment of demand is "of fundamental importance for all items, not merely low-demand items". The mission formalizes that claim and the computation behind it.
Fix one item. Its spare stock is stock on hand plus on order plus in repair, minus backorders; under one-for-one replenishment it is constant. Let the number of units in resupply at a random time be Poisson distributed with mean :
The expected backorders at spare stock are, by the paper's eq. (2),
In eq. (2) the mean is (customer rate times mean resupply time); on p. 138 it is the mean demand over a unit time interval. Only the mean enters, so it is written as one parameter . In Lean this is SherbrookeMetric.PointEstimate.backorders s lam, built on the published Poisson probabilities ServiceParts.StockLevels.poissonPmf.
Uncertain mean demand. The true mean takes the values , ( finite), with probabilities , . The point estimate is the mean of this distribution, , and the expected backorders accounting for the uncertainty are . The paper's example (p. 138) takes with probability each, so ; its procedure (p. 139) discretizes a gamma prior to five to ten values.
If two distinct values both carry positive probability, then for every spare stock
and for the two sides are equal for every prior. The goal fixes no constants and no particular prior.
and second derivative for . 2. Strict convexity, p. 139: for , is strictly convex on . 3. The worked example, p. 138 (off the goal's path): and .
The result. Expected backorders are the objective METRIC minimizes, item by item, subject to a budget. If the objective is evaluated at a point estimate, every item with uncertain demand looks better stocked than it is, and since the size of the error varies by item, the marginal comparisons that drive the allocation are distorted. The inequality is the quantitative statement behind the paper's recommendation to compute backorders as a posterior mixture over possible mean demands. It also says that an underestimate of demand costs more than an overestimate of the same size when backorders are the objective. For the bias vanishes because is linear.
Formalizing it. The paper proves the statement in one line ("it is easy to show") by differentiating twice. No machine-checked version exists. A formal proof needs termwise differentiation of the Poisson backorder series, a closed form for its second derivative, and the passage from a positive second derivative to strict convexity and then to a strict finite Jensen inequality under a nondegenerate prior. The resulting facts about are reusable in any Poisson inventory model (base-stock, policies, METRIC and VARI-METRIC). Convexity of in the stock level , the paper's eq. (3), is a different statement; it is already posed on the platform as ServiceParts.StockLevels.backorder_differences (compound Poisson demand) and is not repeated here. The definition of the Poisson probabilities is the published ServiceParts.StockLevels.Basic (Muckstadt 2005).
Each step is classical, but none is a one-liner in Lean. The series is an infinite sum whose terms depend on both through and through , so differentiating it twice under the summation sign requires a uniform summability bound for the derivative series on a neighbourhood of . The tempting shortcut of reasoning with deriv alone fails: deriv returns at points of non-differentiability, so a formula for deriv (deriv B) says nothing about smoothness, and the milestone is stated with HasDerivAt for this reason. The strict inequality further needs strict convexity, not just convexity, and a hypothesis that the prior is not concentrated on one value: with a one-point prior both sides coincide.
tsum over of for and otherwise. The family is summable for every real ; no statement relies on the tsum junk value.deriv alone (vacuous at non-differentiable points) does not meet the target.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.
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.