Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. A high-probability approximation guarantee is a separate claim requiring an explicit probability bound. The optimum includes entangled states. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Many systems evolve by repeated multiplication by a random linear map: the state of a linear system with randomly varying coefficients, population vectors in a random environment (Leslie models whose rates change from year to year), the transfer matrices of a disordered one-dimensional medium, and the transition operators of a Markov chain in a random environment. In each case the object of interest is the product of random matrices and its growth as .
The basic answer is due to Furstenberg and Kesten (Products of random matrices, Ann. Math. Statist. 31 (1960)): under a logarithmic moment condition and stationarity, of the size of converges. Their proof was a substantial piece of analysis. In his 1973 IMS Special Invited Paper (Kingman, Subadditive ergodic theory, Ann. Probab. 1 (1973)), J. F. C. Kingman showed that for matrices with strictly positive entries the result is a short corollary of his subadditive ergodic theorem (Theorem 1 of that paper, 1968). This mission formalizes that application: Theorem 5 of the 1973 paper, §2.2, pp. 891–892.
Timeline:
Let be a probability space, , and let be random real matrices. Write for the th entry of a matrix , and
the product taken left to right. The sequence is stationary if the joint law of equals the joint law of ; this is a statement about all finite-dimensional distributions at once, and it includes the case of independent identically distributed matrices.
The proof works with the diagonal process
and with the -norm . A family is a subadditive process (§1.1) if S₁: for ; S₂: the joint distributions of equal those of ; S₃: exists and for some constant .
Suppose the elements of the matrices are strictly positive, for every and every , and is stationary. Then there is one finite random variable such that for every
with probability one and in mean. The limit is random in general (it is constant when is ergodic); the theorem asserts its existence, its finiteness and its independence of , and nothing about its value.
The limit is the top Lyapunov exponent of the random product: it is the almost-sure exponential growth rate of every entry, and hence of every norm, of . It governs the stability of random linear recursions , the long-run growth rate of populations in random environments, and localization in one-dimensional disordered systems. Theorem 5 is the existence statement on which all of these quantitative questions rest.
The theorem has been proved since 1960, and Kingman's derivation is a classical model application of subadditive ergodic theory. To our knowledge it has no machine-checked proof: Mathlib has neither Kingman's subadditive ergodic theorem nor any limit theorem for random matrix products. This mission produces a formal statement of the result together with the formal decomposition of the proof into the steps Kingman writes down; its milestone 4 is exactly where the subadditive ergodic theorem (the goal of the companion mission Subadditive Ergodic Theory 1) is applied.
Milestones 1–3 are deterministic matrix inequalities plus integrability bookkeeping; the substance is elsewhere. First, milestone 4 needs the full subadditive ergodic theorem, almost-sure and in mean, for a non-ergodic stationary process: the classical Birkhoff theorem does not apply, because is not a sum of stationary increments. Second, passing from the diagonal entry to all entries requires controlling along a stationary sequence with only a first-moment hypothesis, and transporting an almost-sure statement about back to by stationarity, where the limit is itself random. The natural shortcut — treating as a constant — is only valid under ergodicity, which is not assumed.
Matrix (Fin k) (Fin k) ℝ with NeZero k; the paper's index is 0 : Fin k. The sequence is Y : ℕ → Ω → Matrix …, read only for ; Y 0 plays no role.List.prod of [Y (s+1), …, Y t]; is the identity.ℕ → Fin k → Fin k → ℝ with the product σ-algebra. Independence is not assumed.lam : Ω → ℝ; "in mean" is with integrable; time is with Filter.atTop. One lam serves all .liminf on unbounded sequences.Real.log 0 = 0 in Lean; the statements apply log only to entries that are strictly positive under the hypotheses, so no junk value enters. Dropping the positivity hypothesis would change the theorem, and is not an acceptable shortcut.Welcome contributions: proofs of the matrix inequalities, the integrability and stationarity transfer lemmas, a formal subadditive ergodic theorem (shared with the companion mission).
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 finite Markov decision process may have several recurrent classes under one policy. In that setting, its long-run reward depends on the initial state, and a single stationary distribution does not describe the whole decision problem. Hordijk and Kallenberg developed a linear program with two families of variables to handle this multichain case. Their Theorem 8 relates policies to feasible points of that program in both directions: optimal stationary policies give optimal dual solutions, and every optimal dual solution gives an average optimal stationary policy. This relationship explains why the dual program represents the original sequential decision problem rather than merely bounding its value. Hordijk and Kallenberg (1979)
An earlier frequency formulation associated stationary randomized policies with one family of occupation variables in a more restricted Markov-chain setting. The present theorem uses both and variables, and its policy comparison covers history-dependent randomized decisions. The corresponding formalization therefore addresses the finite multichain model of the 1979 paper, with its own dual equations and representative map. Hordijk and Kallenberg (1979), §§1 and 3.3
Let be a nonempty finite set of states. At state , an action is chosen from a nonempty finite set . It earns a real reward and moves to state with probability . The transition probabilities are nonnegative and sum to one over . A general policy may randomize and use the complete past history. Its average reward is the liminf, as the horizon grows, of expected total reward divided by the horizon when the initial state is . The optimal value is the supremum of over all such policies. A policy is average optimal when it attains that value at every state. These are the conventions of §2.1 of the paper. Hordijk and Kallenberg (1979), p. 353
A stationary randomized policy chooses each admissible action at state with a fixed probability , independently of the epoch and history. Its transition matrix is , and its reward vector is . The Cesàro limit matrix and deviation matrix describe the recurrent and transient behavior of this finite chain. In particular, . Hordijk and Kallenberg (1979), p. 359
Fix positive state weights summing to one. The primal linear program minimizes over pairs that are superharmonic: for every and , the first vector dominates its one-step expected continuation, and the sum of the two vectors dominates one-step reward plus the continuation of the second. The dual linear program maximizes over nonnegative and satisfying the two flow equations (3) and (4). Variables are present only for admissible state-action pairs. The set consists of states where . Hordijk and Kallenberg (1979), pp. 356–357
For a feasible dual point , the associated policy normalizes the row at states in and the row at other states. Conversely, equation (6) constructs a representative of a stationary randomized policy. Its coordinates use . Its coordinates use , where is zero at transient states and is chosen separately on each recurrent class by a maximum formula. The formalization restricts that formula's denominator to the recurrent class, as required by the subsequent nonnegativity calculation; the printed unrestricted denominator has a two-state counterexample. Hordijk and Kallenberg (1979), pp. 359–360
The goal is Theorem 8, with both directions in one statement:
The second implication applies to every optimal dual point. It produces the stationary randomized policy given by the printed normalization rule, including its existence as a valid policy. The first implication uses the particular representative defined by equation (6). Neither direction imposes an extreme-point condition. Hordijk and Kallenberg (1979), Theorem 8, p. 360
The milestones state the least-superharmonic characterization of ; the positivity that makes the dual-to-policy normalization meaningful; the stationary gain identity; feasibility and objective value of the representative; and Propositions 4 and 5, which describe tight actions and identify with the recurrent states of . Each is a statement about the same finite model and the same primal–dual pair. Hordijk and Kallenberg (1979), pp. 356–361
The theorem establishes an exact relation between two ways of expressing average optimality. The LP direction turns an optimal stationary policy into a dual optimum with a concrete state-action representation. The converse says an arbitrary optimal dual point can be read as an average optimal policy, even when its coordinates vanish at some states. Proposition 5 specifies what those vanishing coordinates mean for the induced chain: those states are transient. These statements permit optimization over a finite LP while preserving the policy interpretation of its solutions. Hordijk and Kallenberg (1979), Theorem 8 and Proposition 5
The result was proved in 1979; this mission asks for a machine-checked proof of its precise finite-state statement. The shared MDP model and the limit and deviation matrix definitions already exist as published formal objects. The new work is the correspondence for Hordijk and Kallenberg's dual equations, with the representative, its class-wise correction, and the connection to liminf average reward. The definitions of stationary policy mixtures, admissible-pair LP coordinates, and finite-chain recurrence can support later results about average-reward optimization.
Normalizing alone does not define a policy at every state: its row sum can be zero. The dual program's second variable supplies the action weights there, and the feasibility equations must ensure its row sum is positive. In the other direction, the natural term in need not be nonnegative. The correction is chosen by a maximum over each recurrent class, while transient states require a different case. These issues remain in a multichain process even though the state and action sets are finite. Hordijk and Kallenberg (1979), pp. 359–361
Lean uses finite types for states and actions, a nonempty state type, and a nonempty admissible action set at every state. The published StationaryMDP definition provides real rewards and stochastic transition rows. General policies are its history-dependent randomized AvgHRPolicy values; average reward is its liminf reward, and optimal gain is the supremum over that entire policy class. The mission defines its own average-optimality predicate because the published Puterman predicate uses a stronger limsup comparison. For finite rewards, the liminf gains and their supremum are bounded real numbers.
Stationary randomized weights are nonnegative, sum to one on each , and vanish outside . The dual variables are functions on the subtype of admissible state-action pairs. The primal and dual optima mean feasible points attaining the relevant objective against every other feasible point. The paper's positive, normalized remains explicit. The raw formula for is used only with a feasible dual point, and the policy-well-definedness milestone supplies its nonzero denominators. The representative uses a maximum over the ergodic class of each recurrent state, with the class-restricted denominator needed by the paper's proof; replacing by zero or by one global maximum would change the target.
The known matrix objects and are imported from the published Blackwell development. Their convergence and identities are theorem obligations, not assumptions hidden in definitions. Contributions proving the finite-chain identities, representative feasibility, complementary slackness, and the final policy comparison are within scope. A statement restricted to a unichain model, an extreme dual point, or a pure selected action would not establish this theorem.
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.
A backward-forward stochastic differential equation couples two equations that run in opposite time directions: a forward equation for a state , started from a given input, and a backward equation for a quantity , pinned at a terminal time by a random variable . Each equation's coefficients depend on both unknowns, so the solution at time depends on the past of and on the conditional future of . Such systems arise in stochastic control (the adjoint equation of the stochastic maximum principle runs backward while the state runs forward) and in mathematical finance (an asset's price is forward, a hedge or value process is backward).
Antonelli's 1993 paper (Ann. Appl. Probab. 3(3), 777–793) is one of the first treatments of the coupled problem. Pardoux and Peng (1990) had established existence and uniqueness for decoupled backward equations driven by Brownian motion. Antonelli proved existence and uniqueness for the coupled system under a smallness condition, and gave examples (§3) showing that without such a condition a solution may fail to exist. This mission formalizes the bounded-variation case of that result, Theorem 3.1.
Fix a horizon and a probability space with a filtration satisfying the usual hypotheses: it is right-continuous, and contains every -null set.
An integrator is an adapted process whose paths have bounded variation on , with . It is written with adapted, nondecreasing and right-continuous, and , the total variation of on . It is bounded: . The pathwise integral is the Lebesgue–Stieltjes integral over .
The system involves two integrators and the increasing process
whose pathwise Stieltjes measure is . The Doléans measure of on gives the norm
and is the space of jointly measurable processes with finite norm. The size of is .
The data are coefficients , a constant , a terminal value and a forward input . They satisfy:
In addition is -measurable and is adapted. The system is
and its right-hand side defines an operator , (3.3). A solution in the sense is a pair with and -a.e.
If and are dominated by and
then there is a progressively measurable solution of (3.1)–(3.2) in the sense, and any two progressively measurable solutions agree -a.e.:
The theorem identifies a regime in which a coupled forward-backward system is well posed. The integrability required is only , and the smallness condition ties the Lipschitz constant to the total mass of the driving integrators. With it reads , a small-horizon condition. The paper's Example 1 (mission 3 of this series) shows that at , a solution may fail to exist, so some restriction of this type is necessary. Later work on forward-backward equations, for instance the four-step scheme of Ma, Protter and Yong (1994), replaced the smallness condition by other structural assumptions. Antonelli's small-horizon result remains the base case those methods extend.
The result is proved in the paper. No machine-checked version of it, or of any backward stochastic differential equation, exists in Mathlib or on the platform. The formalization adds three things on top of the paper. It makes the solution concept precise: versions, integrability, and -a.e. equality. It repairs a gap in the printed proof (see Formalization scope). And it builds pathwise Lebesgue–Stieltjes integration against adapted bounded-variation processes, together with the optional projection identity (2.6), as reusable infrastructure.
The Banach fixed point theorem does the final step once the contraction estimate holds. The difficulty lies in reaching that estimate. The -component is a conditional expectation, defined for each only up to a null set, and these null sets accumulate when the process is integrated against , which may charge random times. The estimate has to be transported from "for each , almost surely" to "-almost everywhere". That needs càdlàg versions and the optional projection theorem, which Mathlib lacks. A second point: the naive bound treats the forward and backward differences separately and gives the constant . Obtaining requires combining both differences inside one conditional expectation, and that uses the adaptedness of the forward difference.
Time is with horizon ; integrators are frozen after . Each integrator carries its minimal Jordan decomposition as data, tied to Mathlib's eVariationOn. Pathwise measures are Mathlib's Stieltjes measures, and integrals are over . Norms are lower integrals in . Every conditional expectation is accompanied by the integrability of its argument, since Mathlib's condExp of a non-integrable function is . A version of must be jointly measurable and have càdlàg paths on . Without the càdlàg requirement, two versions can differ on the graph of a random time charged by , and the contraction estimate fails.
The formalization commits to these readings of the paper:
The solution concept rules out trivial solutions. It requires , the integrability of every argument of the conditional expectation, and a càdlàg version, and existence asserts a progressively measurable pair. A pair satisfying the equations only through Lean's junk values therefore does not count.
A complete development needs:
All four are reusable well beyond this mission. Contributions to any of them are welcome, as is a proof of any milestone in isolation.
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.
Interior-point methods transformed linear programming in the 1980s and 1990s. A natural question was whether the same ideas carry over to nonlinear programming, where the objective and the constraints are general smooth functions. Sequential quadratic programming (SQP) methods were then the method of choice for small and medium nonlinear problems, but each iteration solves a quadratic subproblem with all the constraints, which scales poorly. Byrd, Gilbert and Nocedal (INRIA RR-2896, 1996; journal version Math. Program. 89 (2000) 149–185) combine the two. They apply a trust-region SQP method to the barrier problem of the nonlinear program, keep the slack variables positive through the trust region and the barrier term, and prove global convergence without assuming that the constraint gradients have full rank. The algorithm became the basis of the interior-point solver KNITRO (Byrd, Hribar, Nocedal, SIAM J. Optim. 9 (1999)).
The analysis is of interest beyond this one method. It isolates the situations in which an interior-point method can fail: convergence to a stationary point of the infeasibility, or to a point where the constraint gradients of the active constraints are dependent. It shows that these are the only failure modes.
Let and be continuously differentiable. The problem is
For a barrier parameter , introduce slacks , , and the barrier problem
Write for the matrix of constraint gradients, , , and , , along a sequence of iterates. All norms are Euclidean. A second norm on is arbitrary.
Algorithm I solves (2.2) for fixed . At an iterate and a trust-region radius it computes a vertical step , which reduces the linearized constraint violation inside a smaller trust region. It then computes a horizontal step , which reduces a quadratic model of the barrier objective in the null space of the linearized constraints. Each step must give a fraction of the decrease of a scaled steepest-descent step (the Cauchy decrease conditions (2.18), (2.33)). The total step is judged by the merit function
whose penalty parameter is raised, by a factor of at least , whenever the predicted reduction would otherwise fall below times the vertical predicted reduction. A step is rejected and the radius shrunk if the merit function does not decrease by a fraction of , or if some slack component would drop below . On acceptance, and .
Algorithm II runs Algorithm I for barrier parameters (). Each inner run stops at the first point with and , where .
A sequence is asymptotically feasible if . A limit point of fails the linear independence constraint qualification (LICQ) if the columns are linearly dependent.
For a run of Algorithm II, assuming the standard regularity conditions (Assumptions 4.1) on every infinite inner run:
The milestones follow the paper's proof, in order.
together with exactly one of (i) infeasible stationarity with , (ii) an LICQ-failing limit point with , (iii) with bounded away from zero and eventually constant.
Theorem 4.3 says that the method converges to stationary points of the barrier problem unless the problem is locally infeasible or degenerate, and it says which. Theorem 5.1 turns this into first-order optimality for (2.1) at LICQ limit points of the outer iteration. The proof does not assume full-rank constraint Jacobians or bounded iterates, and it allows inexact subproblem solutions. These features distinguish this analysis from earlier ones for interior-point methods.
The results are proved in the paper; none of them is formalized. A complete development would give a machine-checked convergence theory for a practical nonlinear interior-point method, the trust-region Cauchy-decrease calculus that many trust-region analyses reuse, and a formal account of the LICQ failure modes. The formal statements also make explicit details the paper leaves to the reader: the inner rejection loop and the role of the slack reset.
The obvious argument runs as follows: the merit function decreases, it is bounded below, so the predicted reductions are summable and the iterates become stationary. This fails on two counts.
First, the penalty parameter changes, so is not monotone along the iterates. Lemma 4.4 must first bound the slacks before any summability argument applies.
Second, a small predicted reduction may come from a small trust-region radius rather than from near-stationarity. Excluding this needs a uniform statement that small steps are accepted near any non-stationary iterate. The vertical step must then be controlled by its own predicted reduction (Lemma 4.8), and that control is only available when the matrices have singular values bounded away from zero. Whether they do is exactly the dichotomy of Lemma 4.7. In Theorem 5.1(B), the multipliers of the outer iteration need not be bounded a priori; their convergence uses the LICQ at the limit point.
Points live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and stacked vectors in WithLp 2 products, so every norm is Euclidean. Matrix norms are operator (spectral) norms. is the adjoint of the derivative of . "Smooth" is read as on all of . The trust-region norm is a seminorm vanishing only at . The merit function is evaluated only at positive slacks, which the fraction-to-boundary test guarantees, so the paper's value is never needed.
A run of Algorithm I records, at every iteration, all rejected trials and the accepted one. Each trial is a valid pass through Steps 1–3: feasible approximate subproblem solutions, the range space and Cauchy conditions, and the penalty update with the constant . Rejected trials fail the acceptance test, and the radius is multiplied by a fixed after each rejection. The Cauchy conditions are stated as "at least times the decrease at every feasible multiple of the steepest-descent direction", which is equivalent to the paper's argmin form. The multipliers are not recorded, since they enter only through . Algorithm II is a sequence of such runs. The -th run is valid up to its first stopping index, or forever if it never stops. Outer iterations are numbered from .
Two hypotheses are added to the page. Lemma 4.7 assumes bounded below, which its proof uses. Lemma 2.3 assumes , which (2.27) guarantees. Algorithm II's stopping tolerances are taken positive. Where the paper divides by a quantity that may vanish and means ((2.21), (2.36)), the case is split off explicitly, so no bound degenerates to . A formalization in which a run may record only accepted steps, or in which the penalty may grow by arbitrarily small factors, would make the analysis unprovable or the statements weaker; the run predicate rules both out. A sorry-free check exhibits a run satisfying all hypotheses.
A complete development needs:
The Cauchy-decrease lemmas and the LICQ limit-point argument are reusable for other trust-region and constrained methods. Contributions to any milestone, and to auxiliary lemmas such as the identity (2.40), are welcome.
A model trained to minimize its average loss can perform poorly on subpopulations that are rare under the training distribution . Distributionally robust optimization replaces the average loss by its worst case over all distributions close to in an -divergence, which upweights the tail of the loss and controls performance on every subpopulation of sufficient size. Duchi and Namkoong (arXiv:1810.08750, Ann. Statist. 49 (2021), DOI 10.1214/20-AOS2004) study this objective for the Cressie–Read family of divergences, which interpolates between the -divergence and the KL-divergence and links the robust risk to -norms of the loss.
In practice is unknown and the robust risk is computed on the empirical distribution of a sample. Whether this plug-in estimate is close to the population robust risk, and at what rate, is the question this mission formalizes. Earlier work on the same estimator (Namkoong and Duchi 2017; Duchi, Glynn and Namkoong 2021) let the radius shrink as ; here the radius is fixed, so the robust risk is a genuinely different functional of from the mean.
Let be a measurable space, a probability measure on it, a parameter set and a loss. Fix , write , and fix a radius .
The Cressie–Read function is for and for . It is convex, nonnegative and vanishes at . The Cressie–Read divergence of from is .
The robust risk at under is
the second form writing for the likelihood ratio. Let be i.i.d. with law and their empirical measure. With and , the dual objective is
The Lean development uses the same names: cressieRead, robustRisk, empiricalMeasure, dualObjective, kstar, ck, in the namespace UniformDRO.Concentration.
Assume for all , with . For a fixed and , whenever , with probability at least ,
The goal is stated exactly as printed, constants included.
The result. Theorem 2 shows that the plug-in robust risk is a consistent estimator of the population robust risk for a fixed divergence radius, at rate up to a factor; Theorem 3 of the same paper shows this rate cannot be improved in general. Through a covering argument it yields uniform bounds over a model class (Corollaries 1–2, p. 20) and hence guarantees for the plug-in minimizer : the robust risk of the learned model is close to the best achievable robust risk. The rate degrades as , quantifying the statistical price of protecting against larger distribution shifts.
Formalizing it. The result is proved on paper; no machine-checked version exists. A formal proof requires a measure-theoretic duality theorem for -divergence balls (Lemma 1), convex concentration for product measures (Lemma 6, posed on the platform and not yet proved), and a moment bias bound (Lemma 8). Formalization already exposed two slips in the printed proof, both corrected in the milestones without changing Theorem 2.
The robust risk is a supremum over an infinite-dimensional set of likelihood ratios, so concentration cannot be read off any single empirical average. The argument goes through the dual: Lemma 1 reduces the robust risk to a one-dimensional infimum of , which is a Lipschitz function of the data only for in a bounded interval (Lemma 9), and only up to a bias, because is a nonlinear (norm-like) function of an empirical mean. Neither half is routine: the duality for general requires the closed form of and an attained infimum over , and the bias bound (Lemma 8) needs a careful case split at . The naive approach — concentrating for a fixed — fails because the optimal depends on the sample.
PhiDivRobust.Counterpart.conj is reused for Lemma 3.Real.rpow; Euclidean distances on are written out as , since the default norm on Fin n → ℝ is the sup norm.sSup (the loss is bounded, so the value set is nonempty and bounded), the divergence constraint cannot be met by non-integrable ratios, and the goal mentions only , , , , and , not the proof's auxiliary objects.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.
Many models in economics, biology and computer science are finite Markov chains that have several absorbing states or recurrent classes, so their long-run behaviour depends on where they start. Adding a small amount of noise (mistakes, mutations, experimentation) makes the chain irreducible, and the noisy chain then has a unique stationary distribution. As the noise vanishes, that distribution concentrates on some of the original recurrent classes. The stochastically stable states are the ones that keep positive weight in the limit; they are the states the system spends nearly all its time in when the noise is small but nonzero.
H. Peyton Young's The Evolution of Conventions (Econometrica, 1993) proved a general finite-state characterization of these states, which he used to select among the equilibria of coordination games under adaptive play. The characterization rests on the theory of small random perturbations of Freidlin and Wentzell (1984), developed for diffusions, and on a combinatorial lemma of theirs expressing stationary distributions through spanning trees. Kandori, Mailath and Rob (1993) characterized the limit distribution by spanning trees on the whole state space for their model of learning with mutations; Young's Lemma 1 generalizes their Theorem 1 (p. 78), and his Lemma 2 reduces the computation to the much smaller graph of recurrent classes. Foster and Young (1990) introduced stochastic stability for evolutionary dynamics, and the equilibria it selects in games coincide with the risk-dominant equilibria of Harsanyi and Selten (1988).
Let be a finite set and the transition matrix of a Markov chain on . A state is reachable from if for some ; is recurrent if every state reachable from can reach back; the recurrent communication classes are the communication classes of recurrent states.
A family of Markov chains on is a regular perturbation of if for all :
The exponent is the resistance of the transition . The graph has vertex set and an edge when for all small , weighted by .
For , a -tree is a spanning tree of edges of in which every has a unique directed path to . The potential of is
For classes , is the least resistance of a path in from to . On the complete directed graph with vertices and edge weights , the stochastic potential of is the least total weight of a -tree in .
If is the stationary distribution of for , then as , where is a stationary distribution of , and
Theorem 4 turns a limit of stationary distributions into a finite optimization: compute least-resistance paths between the recurrent classes, then a minimum-weight arborescence on the reduced graph. The answer depends only on the orders of magnitude of the perturbations, not on their exact values, which is what makes the result usable when the noise model is known only qualitatively. It underlies the equilibrium-selection results of the same paper (risk dominance in coordination games, Theorem 3) and much of the later stochastic evolutionary game theory literature.
The result is proved in the paper, with the tree formula imported from Freidlin and Wentzell. As far as is known, none of it is formalized: Mathlib has irreducible and primitive nonnegative matrices but neither the Markov chain tree formula, aperiodicity, recurrent classes of a finite chain, nor minimum arborescences. A complete development would produce these as reusable components.
The first idea is to take the limit in : compactness and (7) give that every limit point of is stationary for , but has many stationary distributions, so this neither proves convergence nor identifies the support. Both come from the tree formula, which makes a ratio of sums of products whose orders of magnitude are read off from the resistances; the absence of cancellation (all terms are nonnegative) is essential. The second difficulty is Lemma 2: an optimal -tree on the whole state space must be transformed, by the paper's tree surgery on junctions (pp. 80–83), into something comparable with a -tree on the class graph without increasing its resistance. The easy inequality glues optimal paths and zero-resistance trees together; the reverse inequality is where the work lies.
States form a Fintype X with decidable equality; chains are real matrices Matrix X X ℝ, row stochasticity is Matrix.rowStochastic, irreducibility is Mathlib's Matrix.IsIrreducible, and aperiodicity (every state has period 1) is defined in the mission. The family is a function ℝ → Matrix X X ℝ constrained only on ; all limits are one-sided (), is the real power, and "" is a real limit . Distributions are row vectors and stationarity is . Trees are parent maps with edges pointing toward the root. Potentials, class resistances and stochastic potentials are infima in EReal, where an empty infimum is ; under the hypotheses all of them are finite.
The goal quantifies over every regular perturbation, not a parametric family such as , and over every family of stationary distributions of the (unique by (6)). The recurrent classes are computed from , not supplied as data, and is computed on the class graph with weights ; defining as for some would make Lemma 2 definitional and is ruled out.
Contributions welcome: the Markov chain tree formula and the uniqueness of stationary distributions for irreducible finite chains (both reusable well beyond this mission), recurrence and the support of stationary distributions, and the arborescence surgery of Lemma 2.
StochFictPlay.* (Hofbauer and Sandholm 2002, stochastic fictitious play) and CalibratedCE.* (calibrated learning and correlated equilibrium).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.
Many iterative algorithms update only part of a vector at a time. In a parallel implementation, one processor may read a value written several rounds earlier by another processor. Random observations also perturb each update. John N. Tsitsiklis's 1994 paper gives conditions under which such an asynchronous stochastic iteration still converges. The paper develops the result to analyze Q-learning, where state-action values are revised from sampled costs and successor states. Its general theorem also applies to iterative fixed-point calculations beyond that application.
The central issue is that a processor can choose which component to update after seeing the past, and its input can be stale. A convergence theorem that presumes a fixed update schedule or current data would miss both features. The paper's Assumptions 1–3 describe when delays, sampling noise, and random step sizes remain compatible with almost-sure convergence. Assumption 5 gives a weighted maximum norm contraction for the iteration map. Theorem 3 combines these conditions into the target of this mission.
Fix a positive integer and write for the vector after round . Let be the map whose fixed point the iteration seeks. For component , the step size lies in , the noise is , and is the time from which component was read. Thus has coordinates . With when component is idle, all rounds obey the single update equation
All quantities live on a probability space with law . The increasing filtration represents information available when the step sizes and delays are selected, before the round's noise is observed. Assumption 1 says every timestamp tends to infinity almost surely: no fixed old value remains in use forever. Assumption 2 makes the initial state, chosen step sizes, delays, and noise measurable at the specified times; the noise has conditional mean zero, and its conditional second moment is bounded by a deterministic affine function of the largest squared iterate seen so far. Assumption 3 requires, for each component, divergent total step size and a square-summable step-size sequence, with a deterministic bound on all squared partial sums.
For a vector with strictly positive coordinates, the weighted maximum norm is . Assumption 5 provides and such that for every . Assumption 6, used in the boundedness milestone, requires the related growth bound for some real . The weighted norm permits different component scales.
Theorem 1 is the main intermediate target. Under Assumptions 1, 2, 3, and 6, it asserts
The bound may depend on the sample path. Lemmas 1–3 of the paper are milestones in its analysis: a scalar noisy recursion converges, its tails become uniformly small, and the pathwise bounds in the contradiction step hold.
The goal is Theorem 3, under Assumptions 1, 2, 3, and 5:
This theorem does not assume bounded iterates or Assumption 6 separately. Its proof uses Theorem 1 after deriving the needed growth bound from the contraction condition. Lemma 8 is the remaining milestone, comparing the coordinate iterates to an auxiliary deterministic recursion and a noise tail.
The result gives a fixed-point convergence guarantee when coordinates update at different times, delays can vary, and update choices can depend on past observations. In the paper's Q-learning application, these features describe exploratory sampling and possible parallel computation with old state-action values. For discounted problems, the associated Q-learning map contracts in the maximum norm, so Theorem 3 supplies the convergence step once the stochastic assumptions are checked (Tsitsiklis 1994, §7).
The mathematical results were proved in 1994; this mission asks for machine-checked proofs of their formal statements. Its reusable output would include a model of asynchronous noisy iteration, a scalar martingale-noise convergence lemma with random conditional variance bounds, and a precise interface between weighted contractions and pathwise convergence. The goal and milestone theorem files are currently statements with proof holes, while the definition file compiles without one.
A coordinate's next value depends on a vector assembled from observations at several earlier times. A direct estimate against the current error therefore does not close: the stale coordinates can reflect larger past errors. The noise condition is also tied to the largest iterate seen so far, so a deterministic global variance bound is unavailable before boundedness has been established. These two dependencies make the ordinary synchronous contraction argument insufficient. The scalar noise result and the pathwise comparison lemmas isolate the conditions needed for the boundedness and convergence statements.
Vectors are functions Fin n → ℝ, with ; the source labels coordinates , while Fin n starts at zero. Function order is componentwise. The model sets on idle rounds and uses the paper's unified update equation. It does not store the sets of update times separately. The delay values on idle rounds are left arbitrary because they do not affect the update; the source chooses the current time there. All step sizes lie in , and all delays are at most the current time, on every sample path.
The probability law is a probability measure. The filtration consists of increasing sub-σ-algebras. The iterate sequence is explicitly assumed adapted in the main theorems, matching the paper's use of and its running maximum as -measurable random variables. Conditional moment assumptions use integral inequalities over measurable sets, allowing generalized conditional expectations when the noise need not have a finite unconditional second moment. The conditional upper bound is required nonnegative almost surely, as the original inequality entails. Divergence and square summability use partial sums, so a non-summable series cannot receive a default value.
The maximum norm is the finite supremum of coordinate absolute values, and the weighted norm divides by the strictly positive coordinates of . Almost-sure boundedness means a path-dependent finite bound on every coordinate and time. Pathwise Lemmas 3 and 8 are stated on a retained sample path, with the auxiliary quantities and hypotheses established at their locations in the paper; Lemma 8 uses the proof's translated and rescaled coordinates. These conventions rule out an empty coordinate type, junk integrals, and a vacuous boundedness claim. Contributions to the stated lemmas, their probabilistic infrastructure, and the final convergence proof are within scope.
Q-learning (Watkins, 1989) learns the optimal action values of a Markov decision problem from sampled transitions, without a model of the transition probabilities. At each step only one state–action pair is updated, with a noisy estimate of the Bellman operator evaluated at possibly outdated values of the other pairs. Watkins and Dayan (1992) gave a first convergence proof for discounted problems. Tsitsiklis (1994) and, independently, Jaakkola, Jordan and Singh (1994) placed Q-learning inside the theory of stochastic approximation: the Robbins–Monro scheme of iterating with decreasing stepsizes and zero-mean noise, here in an asynchronous form where different components are updated at different times using delayed information, as in the distributed iterations of Bertsekas and Tsitsiklis (1989).
Tsitsiklis's paper proves convergence with probability 1 under two structural hypotheses on the iteration mapping : a weighted maximum-norm contraction (Theorem 3), which covers discounted Q-learning, and monotonicity (Theorem 2), which covers undiscounted (stochastic shortest path) problems, whose Bellman operator is monotone but in general not a contraction. This mission formalizes the monotone case.
A mapping with components is given, and the goal is to solve . Time is discrete, . The iterate evolves by
where is a stepsize ( when component is not updated), is noise, and are delays: the update of component may read component as it was at an earlier time. All quantities are random variables on a probability space with an increasing sequence of σ-fields , the history up to the choice of the stepsizes at time .
Vector inequalities are componentwise and is the vector of ones. The paper's assumptions are:
In Lean the algorithm is the structure AsyncSA.Monotone.Algorithm with fields F, x, α, w, τ, and the assumptions are Assumption1–Assumption4.
Under Assumptions 1–4, if is bounded with probability 1, then
Boundedness is a hypothesis, not a conclusion: for monotone it must be established separately (the paper does so for Q-learning in §7). The bound may differ between sample paths.
Theorem 2 is the convergence result for asynchronous stochastic approximation driven by a monotone mapping whose fixed point is unique. Its main application is Q-learning for stochastic shortest path problems with improper policies excluded, and more generally any learning scheme whose expected update is a monotone, sup-norm nonexpansive operator in the sense of (7) (dynamic programming operators are the standard examples). The same pattern, an a.s. bounded iterate plus a monotone mean map, recurs in later analyses of asynchronous and distributed learning algorithms.
The result has a published proof but, as far as the platform's catalog shows, no machine-checked one: there is no formalized asynchronous stochastic approximation theorem, and no formal Lemma 1 for random stepsizes and random conditional-variance bounds. A complete development provides the scalar almost-sure convergence lemma, the deterministic envelope argument for monotone maps, and the pathwise comparison steps, each of which is reusable.
The noise has a conditional variance that grows with the iterate, so it is neither bounded nor integrable a priori, and the stepsizes are random and chosen adaptively. The classical deterministic-bound argument for Lemma 1 does not apply directly. The iteration is not a contraction in any norm, so there is no Lyapunov function giving a geometric decrease, and the delays mean that the mapping is evaluated at a vector no single time index describes. Convergence has to be propagated from the deterministic envelopes to the random iterate through a sequence of random times, one envelope at a time, and each step requires the noise accumulated after a random time to be small uniformly in the remaining horizon.
Fin n (0-based); vectors are Fin n → ℝ with the componentwise order, so Monotone F is Assumption 4(a) exactly. is r • 1.CondMeanZero, CondSqLe): for every -set on which is integrable, and in . Mathlib's condExp is not used: it is for non-integrable functions and would make the noise assumptions vacuous.tsum, which is for non-summable sequences. The constants are chosen before the almost-sure quantifier; the bound on is chosen after it.Adapted).tsum for the series, a deterministic bound on , or a second unrelated ) is ruled out by the choices above.Contributions welcome: a general almost-sure convergence theorem for Robbins–Monro recursions with generalized conditional moments (Lemma 1 and its tail version ), and lemmas on monotone maps satisfying (7).
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.