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.
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?
A partially observed Markov decision process (POMDP) models a controller that cannot see the state of the system it controls. It sees only noisy observations, and so it acts on a belief: a probability vector over the hidden states. Machine maintenance, medical screening, quality control and search problems all have this form. The dynamic program of a POMDP lives on the simplex of beliefs, a continuum, so computing exact optimal policies is expensive even when the state, action and observation sets are small. Structural results reduce that cost. A value function that is monotone in the belief, or a policy known to dominate a cheap reference policy, shrinks the space a computation must search. Such results also explain the model: they say when one belief is "better" than another.
W. S. Lovejoy, Some Monotonicity Results for Partially Observed Markov Decision Processes (Operations Research 35(5):736–743, 1987), provides such results by ordering beliefs with the monotone likelihood ratio (MLR) order instead of first-order stochastic dominance.
Timeline. Smallwood and Sondik (1973) set out the finite POMDP and its piecewise-linear value functions. White (1979, 1980) obtained monotone policies and values for machine replacement, for single-stage problems, and for the completely observed and completely unobserved extremes, all under first-order stochastic dominance. Albright (1979) treated the two-state case, where the usual orders coincide. Whitt (1979, 1982) developed the likelihood-ratio orders and showed that they are preserved by Bayesian updating. Lovejoy (1987) combined these into general monotonicity results for finite POMDPs, and the MLR order has since become the standard tool for structural results in POMDPs.
Let (states) and (observations) carry their natural orders, and let be a finite, completely ordered action set. For a finite chain , is the set of probability vectors on . For , (first-order stochastic dominance) means for every . (MLR order) means whenever . For matrices on , means for all pairs, and is TP₂ if .
In each period the decision maker in state chooses and receives the reward . The state moves to with probability (matrix ), and an observation arrives with probability (matrix , with row ), generated by the new state and the action . The paper assumes throughout. The discount factor is . From a belief , the observation has probability , and the posterior is the Bayes update . With
a finite horizon with salvage value gives the optimal values and . For and , is the bounded solution of . The myopic actions are .
Under (a) nondecreasing, (b) nondecreasing, (c) for , (d) for , (e) for , and (f) for , : for every (finite horizon), or for the infinite horizon with , and every ,
where ranges over the maximizers of (resp. ).
Under (a)–(d) with every TP₂: in implies for , and, without (a), for .
The ordering facts behind both propositions: MLR implies stochastic dominance (§1), Lemma 1.1 (characterization of ), Lemma 1.3 (TP₂ prediction preserves ), Lemma 1.2 (the Bayes update is MLR-monotone in the observation, the prior and the action), the stochastic monotonicity of in the belief (proof of Proposition 1) and in the action (Lemma 2.3), the comparison of -increments with myopic increments (proof of Proposition 2), and Lemma 2.2 (dominated increments order maximizer sets).
The result. Proposition 2 makes the myopic policy, which solves a one-stage problem, a lower bound on an optimal policy for every belief and every period. In a search over policies, actions below can be discarded. When also has isotone differences, is nondecreasing, and the optimal policy is bounded below by a monotone function that is easy to compute. Proposition 1 gives MLR-monotone value functions, the input to many later structural results for POMDPs. Lemma 1.2 records the fact behind it: Bayesian updating respects the MLR order, while first-order stochastic dominance does not survive conditioning.
Formalizing it. These results are proved on paper. This mission produces machine-checked proofs, together with a reusable finite-POMDP layer (belief update, observation probabilities, Bellman operator, finite- and infinite-horizon values) and a library of the stochastic orders on finite chains. One statement in the paper is wrong: the printed "only if" direction of Lemma 1.2(1) is false. The mission states only the direction that is true and used.
The obvious induction on for Proposition 1 needs to be nondecreasing and to increase with . Both need a belief order that conditioning preserves. Under first-order stochastic dominance the posterior is not monotone in the prior, and the paper's counterexample (p. 740) shows that the induction then fails. The MLR order repairs this, but proving that the prediction step preserves it (Lemma 1.3) requires a total-positivity composition argument (Karlin–Rinott, Theorem 2.4) on product lattices. For Proposition 2 the difficulty is to compare continuation values across actions: the observation distribution and the posterior both change with the action, and two separate orderings (Lemma 2.3 and Lemma 1.2(3)) must be combined before the maximizer comparison applies. The infinite-horizon parts additionally need the Bellman fixed point characterized well enough to pass monotonicity to the limit.
Everything is finite, so all probabilities and expectations are finite sums and no measure theory is involved. States, observations and actions are finite nonempty types with a LinearOrder (any finite chain is isomorphic to ). is Mathlib's stdSimplex ℝ X. The orders are plain relations (StochGE, MLRGE, TPGE) with the larger argument first, and every statement assumes simplex membership explicitly. The standing assumptions (stochastic rows of and , , ) are fields of the structure POMDP. is computed by recursion (3) counted in steps to go, Vstar gs N t = valueToGo gs (N+1-t). The infinite-horizon is any function bounded on that solves the Bellman equation there. For such a function exists and is unique on , by contraction. The equivalence between recursion (3) and the optimum over history-dependent strategies is cited by the paper from the literature and is not part of this mission. Maximizer sets (argmaxSet) carry the "for all / there exists " quantifiers. Both halves of each part of Proposition 2 are statements.
The goal is not to be read with or replaced by an arbitrary, or an arbitrary nondecreasing, value function. That reading would reduce Proposition 2 to Lemma 2.2 plus a hypothesis. The goal quantifies only over the value functions of recursion (3) and over bounded Bellman solutions.
A complete development needs finite total-positivity composition (Mathlib's four functions theorem is the natural starting point), Abel summation for Lemma 1.1, and a contraction argument for the infinite horizon. The order library and the finite POMDP layer are reusable beyond this paper. Proofs of any milestone are welcome, as are alternative arguments for Lemma 1.3.
Many problems in statistics, engineering and operations research ask for the input level at which an unknown response function is largest, when the response can only be measured with noise: the dose that maximizes a yield, the setting that maximizes throughput in a simulation, the parameter that maximizes an expected reward. Robbins and Monro (1951) had shown how to find, by sequential noisy measurements, the root of an unknown increasing function. Kiefer and Wolfowitz (1952) adapted the idea to maximization: at each step, measure the response at two points placed symmetrically about the current estimate, and move the estimate in the direction of the observed difference. Their scheme is the origin of finite-difference stochastic approximation, the gradient-free ancestor of simultaneous-perturbation and zeroth-order methods in simulation optimization and machine learning.
Timeline. 1951: Robbins and Monro, root finding, convergence in mean square. 1952: Wolfowitz, convergence in probability for Robbins–Monro under weaker conditions; Kiefer and Wolfowitz, the present paper, convergence in probability of the maximization scheme. 1954: Blum proved almost-sure convergence of both schemes under related conditions (doi:10.1214/aoms/1177728794). Later work (Spall 1992, among many) extended the finite-difference idea to many dimensions.
For each level , an observation taken at is a random number with distribution ; the family depends measurably on . The regression function is the mean observation,
and the observations have uniformly bounded variance: for all . The function is unimodal about an unknown point : strictly increasing for and strictly decreasing for .
Two sequences of positive numbers (step sizes) and (probe widths) satisfy
for example , . Starting from an arbitrary number , the Kiefer–Wolfowitz process is
where, given everything observed so far, and are independent with laws and .
The paper imposes three regularity conditions on :
In the Lean development these objects are regFun H (), SecondMomentBound H S, Unimodal, Cond1, Cond2, Cond3, StepSizes a c and the structure IsKWProcess, all in the namespace KieferWolfowitz.Convergence.
This is the theorem of the paper (stated on p. 462, proved in §3 in the form (3.22)). It fixes no rate and no constants, so it is the stable form of the result.
The result shows that the maximizer of a function observable only through noise can be located consistently using function evaluations alone, without gradients and without a parametric model of . The conditions are qualitative: no differentiability, no specific noise distribution, and the noise may change shape with . This is the template for gradient-free stochastic optimization: simulation optimization with finite-difference gradient estimates, simultaneous-perturbation methods, and zeroth-order methods in learning are all analysed by refining the same bias–variance balance between the probe width and the step .
The theorem has been proved since 1952 and is not open. To our knowledge no machine-checked proof of it exists. A formalization produces a checked proof of a founding result of stochastic approximation and, along the way, the probabilistic infrastructure such proofs share: processes defined through conditional laws given a filtration, recursions for second moments, conditional Chebyshev arguments, and the passage from subsequence convergence to full convergence by a restart bound. Alternative proofs (via supermartingale convergence, which would give almost-sure convergence under stronger hypotheses) are welcome as separate developments but are not the goal.
The obvious approach is to show that decreases. It does not: the drift term is negative only on average and only once the probes straddle correctly, while the noise term is always positive and the finite-difference estimate of the slope has a bias of order . A one-step contraction is therefore unavailable, and summability arguments alone give smallness only along a subsequence; turning that into convergence of the whole sequence is where the difficulty lies, and it is also where Condition 3, which forbids flat stretches of away from , cannot be dispensed with. The argument needs integrability of quantities the paper treats as finite without comment, and the conditional statements require the conditional law of the observation pair, not just its unconditional moments.
Kernel ℝ ℝ. Every has , so and the variance in (2.2) are genuine integrals.z 0 is , a n, c n are , .TendstoInMeasure; "" for a nonnegative sequence is "below every infinitely often".BanditAlgorithm.kiefer_wolfowitz_equivalence; the two results share authors and nothing else.Useful infrastructure, reusable beyond this mission: conditional expectations of functions of a pair with a given conditional law, tail-sum bounds, and the passage from a restart bound plus subsequence convergence in probability to full convergence. Contributions of any milestone, of intermediate lemmas such as (3.7), (3.9), (3.13) and (3.29), and of the final assembly are welcome.
Labor markets match workers to firms, and the terms of each match (the salary) are negotiated along with the match itself. A firm's output depends on the whole team it hires, so a firm cares about sets of workers, not individual workers one at a time. Kelso and Crawford (1982) asked when such a market has a stable outcome, the core, in which no firm and group of workers can agree on terms that all of them prefer, and when a simple decentralized auction finds one.
Their answer is the gross-substitutes condition: raising some workers' salaries never makes a firm withdraw an offer from a worker whose salary has not risen. Under it, an ascending process in which firms make offers and workers reject all but their favorite reaches a core allocation. This condition became the standard hypothesis for the existence of Walrasian equilibrium with indivisible goods (Gul and Stacchetti 1999), it is the hypothesis behind matching with contracts (Hatfield and Milgrom 2005), and the process is the ancestor of ascending auction designs.
Timeline.
There are finitely many workers and firms , with at least one firm. Worker 's utility of working for firm at salary is , strictly increasing and continuous in . Firm 's gross product from hiring the set is , and its profit at the salary vector is
is the set of profit-maximizing . Each pair has a starting salary . The assumptions (p. 1486) are (MP) for ; (NFL) ; and (GS): if and , some contains .
In the discrete market with unit , firm may pay worker only , . An allocation sends each worker to a firm at a salary ; it is individually rational (D1) if and every firm's profit is nonnegative. It is a (discrete) core allocation (D3) if it is individually rational, pays permitted salaries, and no firm , set and permitted salaries satisfy for all and .
The salary-adjustment process (pp. 1488–1489), verbatim:
R1. Firms begin facing a set of permitted salaries . Permitted salaries at round , , remain constant, except as noted below. In round zero, each firm makes offers to all workers; this is costless by (MP).
R2. On each round, each firm makes offers to the members of one of its favorite sets of workers, given the schedule of permitted salaries . That is, firm makes offers to the members of , where maximizes . Firms may break ties between sets of workers however they like, with the following exception: Any offer made by firm in round that was not rejected must be repeated in round . By (GS), the firm sacrifices no profits in doing this, since (by R4) other workers' permitted salaries cannot have fallen, and the salary of a worker who did not reject an offer remains constant.
R3. Each worker who receives one or more offers rejects all but his or her favorite (taking salaries into account), which he or she tentatively accepts. Workers may break ties at any time however they like.
R4. Offers not rejected in previous periods remain in force. If worker rejected an offer from firm in round , ; otherwise . Firms continue to make offers to their favorite sets of workers, taking into account their permitted salaries.
R5. The process stops when no rejections are issued in some period. Workers then accept the offers that remain in force from the firms they have not rejected.
"The salary-adjustment process R1–R5 converges in finite time to a discrete core allocation in the discrete market for which it is defined." Formally, under the assumptions above:
Theorem 1 gives the existence of a core allocation in every discrete market satisfying (MP), (NFL) and (GS), with no convexity of production and arbitrary complementarity within the limits of (GS). It is the step from which the paper derives the existence of a strict core allocation of the continuous market (Theorem 2, by letting the unit shrink), and with additional no-ties assumptions the firm-optimality of the process's outcome (Theorem 4) and the comparative statics of entry and exit (Theorem 5).
The result is proved in the paper and has been reproved in more general settings; it has no machine-checked proof known to us. Nothing of this paper was on Prove2Me before this series. Related platform work, credited but not reused: the Gale–Shapley deferred-acceptance development (GS62CollegeAdmissions.*, proved), the no-money ancestor of this process; and the Shapley–Shubik assignment game (AssignmentGame.CoreLP), whose core the process approximates when production is additively separable. Neither states anything about this process. This mission is mission 1 of a series of seven on the paper: 2 (strict core of the continuous market), 3 (one-sided coalition formation), 4 (firm-optimality), 5 (comparative statics), 6 (gross substitutes and decreasing returns), 7 (a market without a core). Each states its own model.
The process is quantified over all tie-breakings, so no single computation settles it; the statements are about every sequence of rounds consistent with R1–R5. Two points carry the content. First, R2 imposes a constraint that may not be satisfiable: a firm must repeat its unrejected offers and choose a profit-maximizing set. Without (GS) no such set need exist and the process is not defined. Second, the core property at the stopping round compares the outcome with coalitions using salaries the process never reached; the comparison is with salaries on the discrete grid only, and it is false if coalitions may use salaries below or off the grid. Termination is not automatic either: the process may continue after a round without rejections, salaries are real numbers, and no bound on the number of rounds is given.
Lean representation, in namespace KelsoCrawford.Process:
Market W F carries u, y, σ; workers and firms are finite types, with [Nonempty F] (the paper's ; with no firms and some worker no run exists).Allocation assigns every worker to a firm (no unemployment, as in the paper's ).GrossSubstitutesOn (M.y j) (M.gridVectors δ j) for each firm: the discrete (GS), since the paper notes that a discrete market may satisfy (GS) while its continuous version does not.M.grid δ .Run records salaries, offers and tentative choices per round; IsRun is R1–R4, Stopped is R5's "no rejections", outcome is R5's allocation.Explicit readings of the paper's phrases:
The existence of a run is part of the goal: without it, statements about all runs would be vacuous. Fixing a tie-breaking rule would turn the statements into claims about a single run and is ruled out; so are the strict core D2 (false here because of ties at the grid) and an integer grid below (false for improving coalitions). Proofs of the milestones and reusable infrastructure for ascending processes are welcome.
For problems with inequality constraints only, F. John (1948) showed that every minimizer admits nonnegative multipliers , one of which belongs to the objective. The Kuhn–Tucker conditions (1951) are the stronger statement in which the objective's multiplier can be taken equal to one; they need a constraint qualification.
Problems arising in practice mix equalities and inequalities. Fritz John's theorem does not cover them, and the obvious reduction, writing each equality as the two inequalities and , destroys the content of the conditions: every feasible point then satisfies them with . O. L. Mangasarian and S. Fromovitz (1967) proved a version of Fritz John's conditions that treats equalities directly and stays informative, and from it derived the constraint qualification now known as the Mangasarian–Fromovitz constraint qualification (MFCQ). MFCQ is the standard regularity assumption in the convergence theory of sequential quadratic programming, interior-point and augmented-Lagrangian methods, and in the stability theory of parametric programs.
Timeline.
Let be -dimensional Euclidean space, and let be functions with continuous first partial derivatives on . The program is
The feasible set is . A point is a solution of (1.1) if and for all . The active set at is . The gradient of at is , and denotes the inner product.
The generalized Fritz John conditions hold at if there are and with
The Kuhn–Tucker conditions are the same system with and no nontriviality requirement.
If is a solution of (1.1), then there exist and with
No regularity of the constraints is assumed. The nontriviality requirement covers , the and the together.
The theorem is a multiplier rule for smooth programs with both kinds of constraints and no assumption on the constraints. It has two direct consequences in the paper. First, it yields MFCQ, the condition (3.4)–(3.6) under which the Kuhn–Tucker conditions hold at every solution. MFCQ is weaker than linear independence of all active gradients (LICQ), and it is equivalent to boundedness of the Kuhn–Tucker multiplier set (Gauvin, 1977). Second, the corollary identifies feasible non-minimizers at which the conditions hold anyway.
The result is classical and its proof is in every nonlinear-programming textbook. Mathlib has the equality-constrained Lagrange multiplier rule for a local extremum (IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt) and the implicit function theorem, and Prove2Me has a formalized Fritz John theorem for inequality constraints only. To our knowledge no machine-checked proof of the mixed equality–inequality Fritz John rule, of MFCQ, or of Motzkin's transposition theorem in this form exists. The formalization would provide the standard multiplier rule and qualification on which a formal theory of nonlinear programming builds.
With inequalities alone, John's theorem follows from the observation that if is a minimizer, no direction strictly decreases and every active to first order; Motzkin's (or Gordan's) theorem then produces the multipliers. With equalities the first step fails: a direction with is tangent to the equality manifold but generally leaves it, so a first-order descent direction does not yield a feasible point with smaller objective. Lemma 1 is precisely the claim that it does when the are independent, and it needs a curve inside along which the strict inequalities persist: the implicit function theorem, applied on an open set, with care that the curve stays in . The linearly dependent case must be handled separately, and it is the only place the multipliers can be nonzero with .
is EuclideanSpace ℝ (Fin n), the inner product is inner ℝ y z, and is Mathlib's gradient f xbar. "Continuous first partial derivatives on ", the standing assumption of §1, is ContDiff ℝ 1 (equivalent in finite dimension) and is a hypothesis of the goal, the corollary and the constraint qualification; Lemma 1 and Lemma 2 use ContDiffOn ℝ 1 · D on an open set , as on the page. Indices and are Fin m and Fin k, 0-based; and are allowed. The multiplier vector is split into u0 : ℝ and u : Fin m → ℝ, and is "u0 ≠ 0, or some u i ≠ 0, or some v j ≠ 0". A solution of (1.1) is a global minimizer over , as the proof on p. 42 uses. In Motzkin's theorem a matrix is the family of its columns, and "either … or …, but never both" is Xor. In Lemma 2, "the assumptions of Lemma 1" exclude the proviso (2.5) of linear independence, which the proof of Lemma 2 treats separately.
The goal does not assume linear independence of the , does not mention or Lemma 1, and requires with included; a formalization that drops from the nontriviality condition is false at , and one that requires is the Kuhn–Tucker statement, false without a qualification.
A complete development needs Motzkin's (or Gordan's) theorem of the alternative, which is reusable well beyond this mission, and the implicit function theorem on open sets in Euclidean space with a curve argument. Proofs of any milestone are welcome, as is a proof of the goal by another route.
A flexible manufacturing system is a set of machines through which parts of several types travel along fixed routes; each machine serves several buffers and must pay a set-up time whenever it switches from one buffer to another. Real-time scheduling decides, as the system evolves, which buffer each machine works on. Perkins and Kumar (IEEE Trans. Automat. Control 34, 1989) introduced simple distributed policies for this problem, of which the most natural is the clearing policy: a machine keeps working on a buffer until it is empty, and only then switches. They proved that every clear-a-fraction policy, a subclass of clearing policies, keeps every buffer bounded on acyclic systems whenever each machine has spare capacity, and left open whether clear-a-fraction policies stabilize all systems in which material flows around cycles.
Kumar and Seidman (IEEE Trans. Automat. Control 35(3), 1990, doi:10.1109/9.50339) answered no. Their Example 1 is a single part type that visits two machines in the order 1, 2, 2, 1. Every machine has spare capacity, yet under the clearing policy the buffer levels grow without bound, and they do so even when all set-up times are zero, so the instability comes from machines starving each other rather than from time lost to set-ups. Until then, instability had been suspected to require positive set-up times. Shortly afterwards Lu and Kumar exhibited instability of a static buffer-priority rule in a re-entrant network (IEEE Trans. Automat. Control 36, 1991); together these examples started the study of stability of multiclass queueing networks.
A manufacturing system has part types arriving at rates . Parts of type follow a route of length : their -th operation is at machine , and they wait for it in buffer , where each part needs processing time . Machine serves the buffers , and switching from to costs set-up time .
Flows are continuous (fluid). The level of buffer at time is , where is its cumulative output and its cumulative input: for the first buffer of a route, and the output of the preceding buffer otherwise. Each machine works in runs: run is a set-up phase of length followed by a processing phase on buffer , during which the buffer is drained at rate while it is nonempty and passed through at its inflow rate when it is empty. The system is stable if for every buffer.
A clearing policy (Definition 1) is one in which a machine processing continues until the first time that is empty and some other buffer of the same machine is nonempty, and then commences a set-up for one of the nonempty buffers.
Example 1. One part type arrives at rate and visits machine 1, machine 2, machine 2 and machine 1; its buffers are , so and . Processing times are , and is the time to set up to buffer . The parameters satisfy the critical condition and the capacity condition
The initial state is , with machine 1 set up for buffer 4 and machine 2 set up for buffer 3. Write
Assume (3)–(5).
For large enough, every clearing trajectory from reaches, at ,
with machines 1 and 2 again set up for buffers 4 and 3.
With zero set-up times and any , every clearing trajectory reaches, at ,
with machines 1 and 2 again set up for buffers 4 and 3.
The example shows that the condition on every machine, which is necessary for stability and sufficient for the existence of some stabilizing policy, does not make natural distributed policies stable once material flows around a cycle. The throughput of the line falls to part per unit time although each machine could handle the demand. This motivates the paper's two positive results: sufficient conditions under which clear-a-fraction policies are stable (Theorem 1), and a supervisory mechanism that stabilizes any policy (Theorem 2), which are the subjects of the other missions of this series. The example is also an early instance of the phenomenon later studied as instability of multiclass fluid networks under work-conserving policies.
The paper's argument is a stage-by-stage computation of piecewise linear trajectories. No machine-checked version of it exists. A formal proof has to make precise what the paper leaves to the reader: that the clearing rule determines the trajectory, that the stage formulas are what that trajectory does, and that the cycle can be restarted. The formal model of runs, set-ups and the clearing rule built here is the same as in the other missions of the series.
The arithmetic of each cycle is routine once the trajectory is known. The difficulty is in the universal quantifier: the claim covers every clearing trajectory, and the clearing rule is defined implicitly, through "the first time thereafter" at which a buffer is empty and another one is nonempty. At several switching instants the buffer a machine switches to is empty and only starts to fill at that instant, and with zero set-up times a machine may begin a run at an instant where the switching condition already holds. Showing that each switch happens exactly when the paper says, and that the fluid levels then follow the printed formulas (including the reduced rate of a machine working on an empty buffer), is a uniqueness argument for a hybrid system, not a simulation. The existence half asks for the converse: an explicit trajectory, defined for all time, with infinitely many runs whose start times tend to infinity.
Fin P, machines Fin M, buffers ⟨p, i⟩ with i : Fin (n p), paper index = Lean index ), instantiated as Example 1 with , route , and for ; staying on a buffer costs nothing.Useful contributions include lemmas about fluid trajectories that do not depend on the example (continuity of levels, the pass-through rate on an empty buffer, restarting a trajectory at a run boundary), which also serve the other missions of the series.
Comparison theorems for stochastic processes answer a practical question: if one system starts "lower" and moves "upward" less aggressively than another, does it stay below the other one for all time? Queueing, reliability and inventory models use such statements to order performance measures of two systems without computing either distribution. Results of this kind for real-valued Markov chains go back to Kalmykov (1962) and Daley (1968); O'Brien (1975) proved a comparison theorem for real sequences with general (non-Markov) dependence on the past.
Kamae, Krengel and O'Brien (1977) placed these results on a common foundation: an arbitrary partially ordered Polish space, where the state can be a vector, a path, a configuration or a measure. Their tool is a characterization of the stochastic order through monotone couplings, which goes back to Strassen (1965).
Timeline.
Let be a complete separable metric space with a closed partial order (the set is closed in ) and its Borel -algebra. Write for the probability measures on . A set is increasing if and imply ; a function is increasing if implies . For , is stochastically smaller than , written , if
A stochastic kernel from to assigns to every a probability measure on , measurably in . For , is the measure on with , and is its second marginal. A kernel on is upward if is concentrated on for every .
For partially ordered Polish spaces , the products and carry the product topology and the coordinatewise order, and are again partially ordered Polish spaces. Given and kernels from to (), the measure on is the law of when and is drawn from ; its projective limit is the law of the whole sequence.
Let and let be stochastic kernels from to , . If and
then there are random sequences , on one probability space, with initial laws , and conditional laws , , such that
The result. Theorem 2 turns an inequality between one-step transition laws into a pathwise inequality between whole trajectories. Every functional that is increasing in the path, such as hitting times of increasing sets, maxima, occupation counts or cumulative costs, is then ordered between the two processes, as Corollary 1 illustrates. Because the state space is any partially ordered Polish space, the theorem covers vector-valued queue lengths, networks, and processes whose state is itself a sequence, not just real chains. Theorem 1 is the basic tool for working with the order on such spaces: it converts between integrals, couplings, kernels and closed increasing sets.
Formalizing it. All results are proved in the paper (1977); none is machine-checked. The platform has the special case of Theorem 1 (i) (iv) for as an open statement (PalmQueueing.Ordering.strassen_st); the general partially ordered Polish case, and the sequence comparison, are new. A formal development yields a reusable library for the stochastic order on general ordered spaces and its interaction with Mathlib's Ionescu-Tulcea construction of process laws (Kernel.trajMeasure).
The obvious argument for Theorem 2 couples the processes step by step: couple , then, given the two histories, couple , and so on. Each step needs a monotone coupling of and chosen measurably in the pair of histories; the existence of one coupling for each fixed pair (Theorem 1) does not by itself give a kernel.
Theorem 1's central implication, from the integral inequality to a coupling supported on the closed set , is Strassen's theorem. On it follows from quantile functions; on a general ordered space there is no such formula. Passing from finite horizons to the infinite sequence is a further step, since an ordering of every finite-dimensional marginal must be turned into an ordering of the infinite-dimensional laws.
[TopologicalSpace E] [PolishSpace E] [MeasurableSpace E] [BorelSpace E] [PartialOrder E] [OrderClosedTopology E]. This is the paper's standing assumption (Sec. 1, p. 899) and is carried by every theorem, also where a statement says only "Polish space". All sets and functions the paper quantifies over are measurable, also by the standing assumption.StochLE P₁ P₂ is defined through bounded measurable monotone functions, exactly as on p. 899. It is not defined through increasing sets, closed increasing sets or couplings, so none of the milestones holds by definition.E (i - 1), X (i - 1), and the paper's kernel () is p (n - 2) : Kernel (Π i : Iic (n - 2), E i) (E (n - 1)), the signature of Mathlib's Ionescu-Tulcea API.Kernel.trajMeasure P₁ p. Corollary 1 is stated about these laws directly. The goal therefore cannot be met by coupling only one-dimensional marginals or finite prefixes; it asserts the joint laws of the full sequences and one almost-sure event for all indices.EReal, and "the expectation exists" means the two parts are not both infinite; expectations equal to are covered.[AddCommGroup E] [Module ℝ E] [ContinuousAdd E] [ContinuousSMul ℝ E] plus the hypothesis that translates of increasing sets are increasing.Welcome contributions: proofs of the milestones, in particular Strassen's coupling theorem on partially ordered Polish spaces, a measurable-selection lemma for monotone couplings, and general lemmas relating StochLE to increasing sets.
The source is the published version (The Annals of Probability), and printed page = PDF page + 898 throughout.
Factoring a polynomial with rational coefficients into irreducible factors is one of the basic tasks of computer algebra. Before 1982 the standard method (Berlekamp's algorithm modulo a small prime, Hensel lifting, then recombination of the -adic factors, as in Zassenhaus's approach) could take exponential time, because the number of ways to recombine modular factors grows exponentially with the number of factors. A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász gave the first deterministic polynomial-time algorithm for factoring primitive polynomials in (Math. Ann. 261, 1982). Its key idea is to replace recombination by a search for a short vector in a lattice, and the lattice basis reduction algorithm introduced for that purpose (the LLL algorithm) has since become a standard tool in number theory, cryptanalysis and integer programming.
Section 2 of the paper, Factors and Lattices, is the bridge between the two halves: it shows that an irreducible factor of can be read off from a reduced basis of a lattice built from a -adic factor of . This mission formalizes that section.
Timeline. Mignotte (1974) bounded the coefficients of a factor of an integer polynomial in terms of the polynomial itself. A. K. Lenstra (Mathematisch Centrum report IW 190/81, 1981, Theorem 2) proved the weaker statement that, under the same conditions, a short lattice vector has a nontrivial gcd with . LLL (1982) proved the sharper Propositions (2.7), (2.13) and (2.16) used here, which pin down the irreducible factor itself.
For with real coefficients, the length of is . For a positive integer , is the polynomial over obtained by reducing every coefficient modulo .
Throughout, is a prime number, a positive integer, and a polynomial of degree . A polynomial is fixed with
Write , so . Proposition (2.5) shows that has an irreducible factor with , unique up to sign; this is the factor the section recovers.
Fix an integer . The lattice is the set of polynomials of degree at most such that divides . Identifying with , is a lattice of rank with basis and determinant .
A basis of is reduced if its Gram–Schmidt data , satisfy for and for .
Assume
that is a reduced basis of , and that some satisfies
If is the largest such , then
and (2.17) holds for all .
Companion items: the basis of and (2.6), and the remark that for the vector is itself an irreducible factor of .
Proposition (2.16) is what makes the factoring algorithm of Sect. 3 correct: running the reduction for increasing , the first for which (2.15) holds produces by one gcd computation, and repeating on factors completely. Together with the polynomial running time of basis reduction (missions I and II of this series), it yields the polynomial-time factoring theorem (3.6). Proposition (2.7) on its own is a general principle, often reused: a polynomial that is divisible by modulo and has small norm relative to must share the factor with .
All results here are proved in the paper and standard in textbooks (e.g. von zur Gathen and Gerhard, Modern Computer Algebra). To our knowledge there is no machine-checked proof of (2.7), (2.13) or (2.16) in Lean or Mathlib. Mathlib has Hensel-type lemmas and the Mahler measure, including a coefficient-wise Mignotte bound and Landau's inequality, but not the form of Mignotte's bound used here, nor any of the lattice statements. A Lean development of this section would be the algebraic core of a verified LLL factoring theorem.
The obvious argument for (2.7) is to bound the resultant of and : it is divisible by when they share a factor modulo , and bounded by by Hadamard. That argument gives only , the weaker version of [8], not that divides . The paper's sharper statement needs a lattice of combinations , the projection to its top coefficients, and the congruence argument (2.11) that forces the low-degree elements of into ; formalizing it requires determinant and Hadamard bounds for a lattice of rank inside a space of polynomials.
Mignotte's bound needs the Mahler measure and the inequality , which is not the coefficient-wise form available in Mathlib. The step (2.19) needs Proposition (1.12) on reduced bases, which is the goal of mission I. The final part of (2.16) needs the primitivity of the basis vectors, which depends on being exactly the set of multiples of modulo of degree at most .
Polynomials are Polynomial ℤ; is g.map (Int.castRingHom (ZMod q)); is the square root of the sum of the squares of the coefficients over the support. Degrees are natDegree, except in (2.11), where degree with values in WithBot ℕ keeps as on the page. A polynomial of degree at most is identified with its coefficient vector in EuclideanSpace ℝ (Fin (m + 1)). Linear independence of is over on coefficient vectors; "basis for " means in , independent, and spanning over . Gram–Schmidt vectors are Mathlib's unnormalised InnerProductSpace.gramSchmidt.
Indices are 0-based: the paper's is b 0. The index of (2.16) is kept as the paper's 1-based value, , so appears unchanged. The powers , , and are real powers with real exponents.
The standing assumptions are hypotheses of every item that involves , or : prime, , , (2.1)–(2.4), . Mignotte's bound (which assumes only ) and (2.18) (pure linear algebra on polynomials of degree at most ) do not need them. The factor is any irreducible with and . A gcd is stated by its universal property (divides each, and every common divisor divides it), which determines it up to sign. Two milestones are stated slightly more generally than the page: Mignotte's bound for every divisor of degree at most , and (2.18) for every nonzero common divisor .
The goal does not assume (2.7), (2.13), Mignotte's bound, (2.18) or (2.19); these are milestones. A trivial formalization in which is an arbitrary divisor of , or in which "reduced basis" is asserted of a family that need not be a basis of , is ruled out by the definitions.
Needed infrastructure: Hensel-type arguments over , Gauss's lemma, the Mahler measure, Hadamard's inequality, and Proposition (1.12) on reduced bases. The lattice determinant results and the Mignotte bound are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the missing Mathlib infrastructure.
A lattice in is the set of integer combinations of linearly independent vectors. Many problems in algorithmic number theory, cryptography and integer programming reduce to finding a short nonzero vector of a lattice, or a few short independent ones. Finding the shortest vector exactly is hard, but in 1982 A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász introduced a notion of reduced basis that can be computed in polynomial time and whose vectors are provably short up to a factor depending only on the dimension (Lenstra, Lenstra, Lovász 1982). Their paper used it to factor polynomials in in polynomial time; the same reduction (now called LLL) became a standard tool for simultaneous Diophantine approximation (the paper's own (1.39)), for H. W. Lenstra's integer programming algorithm in fixed dimension (Lenstra 1983), and for cryptanalysis of knapsack and RSA variants.
What makes a reduced basis useful is a set of explicit inequalities proved in Section 1 of the paper, before any algorithm appears. They compare the lengths of the basis vectors with the lattice determinant and with arbitrary lattice vectors, with constants such as and . This mission formalizes those inequalities.
Let and let and be the ordinary inner product and Euclidean length on . Vectors form a basis for a lattice when they are linearly independent over and . The determinant of is
the written as columns (1.1). The Gram–Schmidt vectors and coefficients () are defined inductively by
the are pairwise orthogonal and not normalised. The basis is reduced if
and
The first condition is a size condition on the coefficients; the second (the Lovász condition) says that swapping and would not shrink the -th Gram–Schmidt length by more than the factor (pp. 516–517).
Let be a reduced basis for and let be linearly independent. Then
The statement quantifies over every reduced basis and every independent family of lattice vectors. Its case is Proposition (1.11).
In the order of the paper's proofs (pp. 517–518):
The rest of Proposition (1.6) and the remark after it: (proof of (1.6)); (1.8) ; (1.9) ; and Hadamard's inequality (1.10) for an arbitrary basis.
Proposition (1.11) says the first vector of a reduced basis approximates a shortest nonzero lattice vector within the factor ; (1.12) extends this to all of the first basis vectors, so that is within of the -th successive minimum of (the remark after (1.12)). These are the guarantees on which the paper's factoring algorithm rests: in Section 2 a reduced basis of a lattice built from a -adic factor yields, through (1.11) and (1.12), an irreducible factor of the polynomial. Inequality (1.9) gives simultaneous Diophantine approximation in polynomial time, and (1.8) bounds how far a reduced basis is from orthogonal.
All of these results are proved in the paper and in textbooks. Verified LLL developments exist in Isabelle/HOL (Bottesch et al., A verified LLL algorithm, AFP 2018), but Mathlib, the library this platform builds on, has neither the reduced-basis predicate of (1.4)–(1.5) nor these bounds. A Lean development produces a reusable definition layer for lattices with the paper's conventions, Gram–Schmidt length estimates, and Hadamard's inequality in determinant form, which the other missions of this series (the reduction algorithm and the factoring application) build on.
The estimates on Gram–Schmidt lengths are single-variable inductions once (1.5) has been rewritten using orthogonality. The step that does not follow from a direct estimate is (1.12): the vectors are arbitrary independent lattice vectors with no relation to the basis order, so a bound on each by a single Gram–Schmidt length does not by itself say which it controls. A naive argument that pairs with fails. The determinant statements need the link between Mathlib's matrix determinant of the columns and the Gram–Schmidt lengths, which Mathlib does not state in this form.
is EuclideanSpace ℝ (Fin n) (abbreviated Vec n), a basis is a family b : Fin n → Vec n, the lattice is Submodule.span ℤ (Set.range b), and "basis for " is linear independence over together with equality of that span with . The vectors are Mathlib's unnormalised InnerProductSpace.gramSchmidt, and is (1.3) verbatim. is the absolute determinant of the column matrix; it is not defined as , which would make the first companion statement true by definition. Section 1 begins "Let be a positive integer", so every statement carries .
Lean indices run from to : the paper's is Lean's b ⟨i-1, _⟩, an exponent at paper index is at Lean index , and the pair of (1.5) is . Exponents , and are real powers. The maximum in (1.12) is a Finset.sup' over the nonempty index set of the , and the statement is empty at , as on the page.
Every statement about a reduced basis also assumes linear independence: the reducedness inequalities alone hold for degenerate dependent families, whose Gram–Schmidt vectors vanish, and would make the targets trivial. The goal does not assume (1.7), (1.13) or any ordering of the ; those appear only as milestones. Proofs of the milestones and companions, and general lemmas on Gram–Schmidt and determinants that would belong in Mathlib, are welcome.
In a store-and-forward network, messages are cut into packets that travel from node to node along wires, one wire per time step, and wait in buffers between moves. Routing such traffic splits into two problems: choosing a path for each packet, and scheduling the packets along their paths, deciding at every step which packets move and which wait. Leighton, Maggs and Rao showed that the second problem always has an essentially optimal solution: once paths are fixed, two simple parameters of the paths determine the routing time up to a constant factor, on every network.
The result separates path selection from timing in the design of routing algorithms for parallel machines, and it reaches beyond networks: a job-shop problem in which every operation takes one unit of time and no job visits a machine twice is the same problem with jobs as packets and machines as edges.
Timeline.
A network is a directed multigraph: a type of nodes, a type of edges, and maps . A path is a list of edges with ; it is edge-simple if no edge occurs twice. A finite set of packets is given, each with its path.
The dilation is the largest number of edges on a path; the congestion is the largest number of paths through one edge. Since a packet crosses at most one edge per step and an edge carries at most one packet per step, every schedule needs at least steps.
A schedule assigns to every packet and every index of its path the step at which crosses its -th edge, strictly increasing in . Its length is the last crossing step. A packet waits in its initial queue before its first crossing, in the edge queue at the head of the edge it last crossed between two crossings, and in its final queue after its last crossing. Only edge queues count for queue size: the other two are fixed by the instance. A schedule is valid if at most one packet crosses each edge at each step.
For the proof, the paper measures schedules that are not yet valid through frames: a -frame is a run of consecutive steps, and the relative congestion of a frame is the largest number of packets crossing one edge in it, divided by .
There are absolute constants and such that every finite set of packets with edge-simple paths of congestion at most and dilation at most , on any network, has a valid schedule with
The constants are not fixed: the paper proves existence, and any constants are a valid answer.
The theorem shows that congestion and dilation, two quantities read off the paths alone, determine the optimal schedule length up to a constant factor on every network, with buffers of constant size. Path-selection algorithms that minimize therefore yield near-optimal routing, and the same bound holds for unit-time job shops without repeated machines. It is also an often-cited application of the Local Lemma beyond a single round of random choices: the proof applies it times in succession.
The result has been proved since 1994, and the algorithmic version since 1999. As far as is known, no part of it is machine-checked. The mission produces a formal model of store-and-forward schedules with edge queues and frames, a formal statement of the theorem that excludes the degenerate readings, and formal versions of the steps of its proof.
The naive approach gives each packet a random initial delay and then lets it move without waiting. That gives packets per edge per step, and steps after slowing down. Lemma 3.2 does better only in frames of size , not in single steps. Recursing on frames, as in Theorem 3.3, loses a constant factor per level and gives .
Removing that factor is the central difficulty. Each refinement must keep the relative congestion nearly unchanged, , which requires second-order terms in the tail estimates, delays spread over the block rather than inserted at its start, and careful handling of block boundaries. The constant queue bound needs an invariant: every packet waits at most once every steps. The Local Lemma gives existence only; the construction is non-constructive.
Conventions committed to in Lean:
V E : Type with src tgt : E → V, no finiteness or degree bound. Packets form a Fintype P; paths are List E with matching endpoints (List.IsChain) and List.Nodup.CongestionLE path c, DilationLE path d), equivalent to exact values because every bound is monotone.Timetable: time p k : ℕ, the step at which packet p crosses its k-th edge, at least 1 and strictly increasing in k. Length at most L means every crossing step is ≤ L. Valid means two different crossings of one edge happen at different steps.g at the end of step t counts crossings of g at a step ≤ t whose packet crosses its next edge at a step > t. Initial and final queues are not counted.frameCount τ g t T counts the packets that cross g at a step in [t, t+T). Relative congestion at most r in frames of size ≥ T₀ is frameCount ≤ r·T for all T ≥ 1 with T₀ ≤ T.log is Real.logb 2. Every O(1) and "sufficiently large" is a constant quantified before the instance, and in the goal ∃ K Q comes before the network.1 ≤ b, without which the page's statement is false.These choices rule out the trivial formalizations: constants chosen after the instance would make suffice; a schedule without edge exclusivity would make the greedy schedule of length a solution; a missing queue bound drops half of the theorem; and a statement without its length bound is solved by sending one packet at a time.
Not stated: Lemmas 3.6–3.10 and the summary of the refinement step (p. 20). They concern the block decomposition and delay-insertion rules of pp. 13–14 and 17–18, which the paper defines only in prose. Contributions are welcome on the Local Lemma (finite or general), the probabilistic estimates of Lemma 3.2, Lemma 3.5, the elementary simulation step, and formal definitions of the block operations from which Lemmas 3.6–3.10 can be stated. The schedule model is reusable for other routing results, such as the on-line algorithm of §2 or the results for leveled networks.
Population models often allow each individual to produce a new individual or die at rates that change over time. Seasonal conditions, exposure to an epidemic, and changing conditions in a laboratory population all make a constant rate a restrictive assumption. In Kendall's 1948 paper, the question is how the entire distribution of the population size evolves when the per-individual birth and death rates are prescribed functions of time. The distribution matters even when its mean is known: a population can have a stable expected size while still having a substantial chance of extinction. Kendall presents the varying-rate model as a generalization of the constant-rate process discussed by Feller in 1939 (Kendall 1948, §1).
This mission concerns Kendall's solution for a population descended from one ancestor. It includes the explicit distribution, the forward equations that connect it to the birth and death model, and the formulas for its mean, variance, and chance of eventual extinction. The paper has no numbered theorems; its results are identified here by its equation numbers and printed pages.
At time , let be the number of individuals. Each individual gives birth at instantaneous rate and dies at rate , so a population of size moves to at rate and to at rate . Both rates are nonnegative. The initial state is . Write for the probability that . The forward equations in §2, (2)–(4), p. 2 are
The formula for reflects that a population already at zero cannot reproduce. The term vanishes at , as it must. The model is expressed through these real-valued probability functions; it does not require a sample-space construction of a stochastic process.
Define the integrated rate difference and the function by §2, (10a)–(11), p. 4:
Set and . Kendall's modified-zero geometric law is and for . The zero state has its own mass; the positive states form a geometric tail. For the nonnegative rates in this mission, and on , so the displayed formulas have their ordinary probabilistic meaning.
The goal is the full claim of §2, (8), (10a)–(12), pp. 3–4: the explicit starts from one ancestor, is nonnegative and sums to one for every , and satisfies the forward equations above. In symbols, the distribution part is
The milestones record the paper's intermediate statements in reading order: the rational generating function in (9); the pair of equations for and obtained from the generating-function equation (6); the equations for and ; the differential equation and integral representation of ; the alternate formulas (10b)–(10c); and the explicit expressions (12). Each is a statement made in the source, with the page and equation displayed beside its milestone.
The companion target from §3, (18)–(19), p. 6 writes and states
When has finite limit , the limiting extinction chance is . Companion statements also retain the mean , all three expressions for the variance in (14c), the criterion that extinction has zero chance exactly when vanishes identically, and the necessary divergence of for almost-sure extinction (Kendall 1948, pp. 4, 6–7).
The geometric law supplies every finite-time population probability from the rate functions. Its zero mass yields an extinction probability without taking limits of an unspecified process, while its first two moments quantify expected growth and fluctuations. The extinction criterion distinguishes a population that dies out with probability one from one that retains a positive chance of survival even when its eventual mean behavior is simple. The variance formulas give later sections of Kendall's paper a way to compare rate schedules with the same expected population (§§3, 6).
The result was proved in the 1948 paper. The work here is to state its model and conclusions precisely in Lean, preserving the initial condition, normalization, boundary state, and time-dependent rate conventions. The current files are theorem statements with proof placeholders; a successful build checks their syntax and types, not the mathematical proofs. Once proved, the definitions and the moment and extinction statements can also support formal work on time-dependent branching and population models.
Knowing the expected population is insufficient to determine the distribution. The forward equation for each couples it to both neighboring states, producing an infinite system. A direct finite truncation would change the birth rate at its upper boundary and would therefore no longer be Kendall's model. The zero state also behaves differently from positive states: a purely geometric law on all does not capture its mass. The generating function has a rational form, but its time dependence must still agree with the forward system for every state and with a normalized probability law. The extinction statement adds an improper integral, whose finite and divergent regimes require distinct limits.
Lean represents as continuous functions that are nonnegative for . The paper calls the rates specified functions and assumes their nonnegativity; global continuity is an explicit convenience for the two-sided derivatives and interval integrals. Only nonnegative time appears in the probabilistic statements. The oriented intervalIntegral from zero to represents every finite integral. HasDerivAt expresses each derivative, and HasSum expresses both normalization and the moment and generating-function series. The law lives on natural-number states, with handled separately. The coefficient at state is the real number , not an implicit extension to a negative state.
The positivity of on nonnegative time must follow from the rates. The definitions are total Lean real functions, so a result that relies on a division states the hypotheses that keep its denominator nonzero. The limit expresses divergence of the paper's improper integral. No uniqueness of solutions to the forward equations is included, because the cited passage does not establish that claim. The goal requires the explicit law to solve the forward equations and to be a probability law; merely expanding its generating function would leave the population model unformalized. Contributions that prove the formulas, establish the required positivity and convergence facts, or develop reusable lemmas for time-dependent linear birth and death equations all fit the scope.
Telephone and data networks are often fully connected at the core: every pair of switching centres has a direct trunk group, and a call that finds its direct trunk full may be alternatively routed over a two-link path through a third, tandem centre. Whether such a network can absorb fluctuations of demand without losing traffic depends on how the spare capacity of lightly loaded links can be borrowed by heavily loaded ones. F. P. Kelly's survey Loss networks (Ann. Appl. Probab., 1991, doi:10.1214/aoap/1177005872) studies this question in §4.6, "Results respecting graph structure", by looking at a static snapshot of the network: random loads on the edges of a complete graph, and the question whether they can all be carried at once.
Timeline:
Let and consider the complete graph on the nodes : every unordered pair of distinct nodes is an edge, and there are edges. Every edge has capacity .
An offered load is attached to every edge . The load of may be carried on its direct edge, or on a two-edge route through a tandem node ; such a route uses the two edges and . Loads are divisible. The loads are routable with capacity if there are flows (zero when ) with such that on every edge
i.e. the directly carried part of 's own load plus all two-edge traffic passing through is at most .
The loads are random: is a nonnegative real random variable with law , and the loads are independent, each distributed as . Let
Write for the mean excess of a load over the capacity and for the mean spare capacity.
If for some and
then
With and :
The result. Theorem 4.45 says that in a large fully connected network, a load distribution whose mean overload is less than half its mean spare capacity can be served, with probability tending to one, using only direct and two-link routes. The factor reflects that each unit of overflow occupies two edges. The condition is explicit and depends on the load law only through two expectations, which makes it a design rule: capacity suffices for large networks as soon as (4.46) holds. Comment 4.47 (p. 358) observes that the two-valued law , with turns (4.46) into Hajek's threshold .
Formalizing it. The theorem is proved, in full, on one page; nothing here is open. The mission produces a machine-checked version of that proof: a precise routing event on the complete graph, the deterministic reservation argument, two Cramér–Chernoff tail bounds with rates uniform in the network size, and the union bound over edges. To our knowledge none of these steps is formalized anywhere, and no routing-feasibility event on a complete graph exists in Mathlib or on the platform.
The obvious approach is to fix an overloaded edge and argue that, among its two-edge routes, enough pass through two underloaded edges. That count is binomial and concentrates, but it does not prove the theorem: the same underloaded edge sits on two-edge routes of many overloaded pairs, so the reservations of different pairs compete for its spare capacity, and the routing decisions of different pairs are dependent. Any argument has to control, simultaneously at every edge, both the flow an overloaded edge can shed and the flow an underloaded edge is asked to absorb, with exponential rates uniform in so that a union bound over edges survives; this is the central difficulty. On the upper side the variables are unbounded, so the exponential moment of has to be carried over to the reserved flows.
The Lean development lives in the namespace KellyLossNetworks.Routing.
{e : Sym2 (Fin K) // ¬ e.IsDiag}; loads are functions Edge K → ℝ.Feasible C x lets each pair split its load arbitrarily over its direct edge and all its two-edge routes, charges a two-edge flow to both edges of its route, requires the flow sent away from a pair not to exceed its load, and imposes the capacity constraint on every edge, including overloaded ones. Flows are real (divisible loads); integer routing is a different problem.Measure.pi (fun _ : Edge K => μ), with μ a probability measure on ℝ and X ≥ 0 almost surely. is the measure of the routing event; no measurability of that event is presupposed.A trivializing formalization is ruled out: an event that allows only direct routing, ignores the capacity of the edges a detour passes through, or lets a pair send away more than its load would make the statement false or empty, and the routing event here does none of these.
A complete development needs Fubini on product measures, the Cramér–Chernoff method for averages of i.i.d. variables (both tails, with the lower tail for a bounded nonnegative variable and the upper tail under an exponential moment), measure-preserving projections of Measure.pi, and combinatorics of the triangles through an edge of the complete graph. The Cramér–Chernoff bounds with rates uniform in are reusable well beyond this mission. Contributions to any milestone are welcome; the deterministic milestones 1–2 and the expectation computations 3–4 are independent of the tail bounds and of each other.
Nonlinear conjugate gradient methods minimize a smooth function of variables using only function values, gradients and a few vectors of storage. They are the method of choice when is so large that quasi-Newton matrices cannot be stored, and they remain a standard component of large-scale optimization software. Their convergence theory is delicate: the classical results assume exact line searches, while practical codes accept any steplength satisfying inexpensive inexact conditions.
Gilbert and Nocedal (INRIA RR-1268, 1990; journal version SIAM J. Optim. 2 (1992)) organized the global convergence theory of these methods around a single device and proved two families of results. This mission covers the first: every conjugate gradient method whose parameter is bounded in absolute value by the Fletcher–Reeves value converges under the strong Wolfe line search.
Timeline. Fletcher and Reeves (1964) and Polak and Ribière (1969) introduced the two best-known choices of . Zoutendijk (1970) and Wolfe (1969, 1971) established the summability condition now called Zoutendijk's condition. Al-Baali (1985) proved that the Fletcher–Reeves method with the strong Wolfe line search and generates descent directions and satisfies . Touati-Ahmed and Storey (1990) treated nonnegative hybrids. Gilbert and Nocedal (1990) extended Al-Baali's theorem to every with , which admits negative values and yields a convergent modification of the Polak–Ribière method.
Let be a finite-dimensional real inner product space and continuously differentiable, with gradient for that inner product. Starting from , the method generates
where , is a scalar and a steplength found by a one-dimensional search. The Fletcher–Reeves and Polak–Ribière scalars are
Assumptions 2.1: the level set is bounded, and on an open neighbourhood of the gradient is Lipschitz: .
A steplength satisfies the Wolfe conditions with if
and the strong Wolfe conditions if the second inequality is replaced by . The angle between and is given by , and the Zoutendijk condition is .
Under Assumptions 2.1, for any method of the above form with
and steplengths satisfying the strong Wolfe conditions with ,
The sequence is arbitrary within the bound; the statement contains no constants.
Theorem 2.1 (ii) (the same conclusion for an ideal line search that does no worse than the first stationary point along ) and the convergence of the hybrid method (3.7), .
Theorem 3.2 shows that descent and global convergence of Fletcher–Reeves-type methods do not depend on the exact formula for , only on the bound . Its main consequence is the hybrid method (3.7), which keeps the Polak–Ribière choice whenever it lies in , and so retains the practical efficiency of Polak–Ribière while inheriting the convergence guarantee of Fletcher–Reeves. Lemma 3.1 also shows that, under these conditions, descent need not be enforced by the line search.
The results are proved in the paper. To our knowledge none of them, nor Zoutendijk's theorem for general iterations, has a machine-checked proof in Lean; Mathlib has no theory of line search methods. A formalization would provide a reusable Zoutendijk theorem for any descent method with Wolfe steps, and a verified convergence statement for the conjugate gradient methods used in practice.
The obvious route to convergence of a descent method is to show bounded away from zero and apply Zoutendijk's condition. For conjugate gradient methods this fails: accumulates previous directions and can tend to zero. The argument must instead control the growth of , which requires bounding through the line search, and this in turn requires knowing that every is a descent direction with comparable to . The threshold is exactly what keeps the geometric series in these bounds below ; the result fails without it.
All items live in the namespace NonlinCG.FRBound. The space is a finite-dimensional real inner product space E (the paper uses "the scalar product used to compute the gradient"), and gradient f is the gradient for that product. Conventions committed to:
ℕ → E, used from index 1; index 0 is never constrained.The goal does not assume Zoutendijk's condition or descent: both are consequences (Theorem 2.1 and Lemma 3.1) and assuming either would remove part of the theorem's content. The hypotheses are jointly satisfiable (for on , , , , , ), so the goal is not vacuous.
Needed infrastructure: line-search conditions, the descent lemma for functions with Lipschitz gradient on a set, and summability arguments for . Zoutendijk's theorem is reusable for any descent method. Proofs of any item, and alternative arguments, are welcome.
An investor in a continuous-time market chooses, at every instant, how to split wealth between a bond and stocks and how fast to consume, so as to maximize expected utility of consumption and terminal wealth. Without constraints on the portfolio, this problem was solved by the martingale method: Pliska (1986), Karatzas, Lehoczky and Shreve (1987) and Cox and Huang (1989) showed that in a complete market the optimal terminal wealth and consumption are explicit functions of a single state-price density, and the portfolio that finances them comes from the martingale representation theorem.
Real investors face constraints: no short selling, no borrowing, a cap on the fraction of wealth in a sector, an incomplete market in which some stocks cannot be traded at all. Each makes the market effectively incomplete, and the single state-price density no longer exists. Karatzas, Lehoczky, Shreve and Xu (1991) treated incompleteness, Xu (1990, thesis) short-selling prohibition, and He and Pearson (1991) short-sale constraints in a general setting. Cvitanić and Karatzas (1992) unified these cases: the portfolio must take values in an arbitrary nonempty closed convex set , and the problem is embedded in a family of auxiliary unconstrained markets indexed by a dual process . This mission formalizes the paper's central characterization, Theorem 10.1, and the results its proof rests on.
A standard Brownian motion in lives on a complete probability space with its augmented filtration , on a finite horizon . The market has progressively measurable interest rate , appreciation rates and volatility matrix , with , , , and a relative risk with . The state-price density is , with and .
A portfolio gives the proportions of wealth in the stocks, a consumption rate is , and the wealth solves
The pair is admissible, , if . With utility functions , (strictly increasing, strictly concave, , , ), inverse marginals and conjugates , the investor maximizes
over , the admissible pairs with integrable utility losses and almost everywhere. The value is .
The support function drives the duality. For in the class of square-integrable processes with , the auxiliary market has interest rate and appreciation rates , state-price density and unconstrained value . For in the subclass (where is finite for all ), let solve . The -optimal consumption, terminal wealth and wealth are , and .
Five conditions are considered for a capital : (A) optimality of a pair , together with ; and, for , (B) financibility: some with finances in ; (C) minimality: for all , with attained by ; (D) dual optimality: minimizes over ; (E) parsimony: for all . The theorem asserts
and, under the conditions (5.8) ( nondecreasing), (8.25) (a uniform growth bound ) and (12.2) (finiteness of the dual functional for some ), that (A) implies (B)–(E) for some with .
In proof order: the conjugate inequalities (5.5)–(5.6); the budget constraint (3.6); the unconstrained solution (Lemma 7.2, Proposition 7.3, Theorem 7.4); the embedding (8.14), ; Proposition 8.3, (B) optimality; the constrained budget constraint (9.4) and the hedging Theorem 9.1, (E) (B); and Appendix A's Lemma A.1, Lemma A.2 and Proposition A.4, the steps of (A) (B).
Theorem 10.1 turns a constrained stochastic control problem into a family of unconstrained ones plus a minimization over the dual process . Condition (D) is a convex minimization over that does not involve portfolios. It leads to the dual problem of Section 12, whose solvability gives existence of optimal constrained policies (Theorem 13.1, the companion mission). Section 9's hedging theorem is the superreplication principle under convex constraints, the basis of later work on constrained hedging and pricing. With logarithmic utility the theorem gives explicit optimal policies, and for deterministic coefficients the dual problem reduces to a deterministic one.
These results are proved in the paper, which is the standard reference for the convex-duality approach. To our knowledge they have no machine-checked proof. The mission's statements also produce a reusable Lean model of a continuous-time Itô market with stochastic coefficients, admissible portfolios, consumption, utility functions and their conjugates.
The obvious argument, Lagrange duality for subject to , fails at the first step: the constraint is on the control process, not on terminal wealth, so there is no static budget constraint to dualize. The paper's dual variable is a process, and for each candidate it changes both the interest rate and the drift. The direction (B) (A) is relatively direct. The direction (E) (B) is a hedging theorem under convex constraints (Theorem 9.1), where financing a claim requires the portfolio to land in and to satisfy the complementary-slackness identity , which no unconstrained construction delivers. The converse (A) (B) must produce the dual process from an optimal pair that is only assumed to exist, and the paper needs the extra growth conditions (5.8), (8.25), (12.2) for it. In Lean, stochastic integrals for integrands that are square integrable only almost surely, the martingale representation theorem for the Brownian filtration, and the product rule for Itô processes are not available in Mathlib.
Processes are functions constrained on ; vectors are EuclideanSpace ℝ (Fin d), matrices Matrix (Fin d) (Fin d) ℝ. The Brownian motion is the published EthierKurtz.IsStandardBrownian. The stochastic integral is a binder I, constrained only by the standing hypothesis that it is an Itô integral for every locally square-integrable integrand. This almost-sure variant of EthierKurtz.HasBrownianItoIntegral uses the published dyadic step helpers itoStepValue and itoStepSum. The hypothesis is satisfiable, by the classical construction.
The following readings are explicit in the Lean.
A formalization in which the stochastic integral is an unconstrained function, a wealth process need not solve its equation, or is real-valued (so that over an unbounded set returns ) would make the statements vacuous or false; each is ruled out above. The proof will need almost-surely-square-integrable Itô integrals, Itô's product rule, nonnegative local martingales as supermartingales, and martingale representation in the Brownian filtration. All of these are reusable well beyond this mission, and contributions of any of them are welcome.
Multi-level programs model a hierarchy of decision makers: a leader commits to a decision, a follower optimises given it, a follower of the follower optimises given both, and so on. Bilevel programs are the standard model of Stackelberg competition, toll setting, network interdiction and many other leader–follower problems in operations research (Candler and Townsley 1982; Bard and Falk 1982). When every level has a linear criterion and the constraints are linear, each player's problem looks like a linear program, and it is natural to hope that the whole hierarchy is solvable in polynomial time.
R. G. Jeroslow's 1985 paper (Math. Programming 32, 146–164) shows that this hope fails at every level of the polynomial hierarchy: a -level linear program with fixed criteria can encode the truth of a quantified Boolean sentence. The result places multi-level linear programming in the polynomial hierarchy and is widely cited for the -hardness of such programs; NP-hardness of bilevel linear programs (Corollary 4.6) is its special case .
A multi-level program has real variables , a feasible set (a polyhedron in the linear case), and players who move in that order; player controls and minimises a fixed linear criterion . The solution sets are defined from the last mover upwards: is the set of at which player 1's criterion is minimal given the choices of all earlier movers, and in general keeps the points of minimising among the points of that agree with on . The value is on , when . The sets can be empty even when is a nonempty polytope: the paper's four-level Example has because is not closed.
A propositional formula over blocks of atoms (block has atoms) is encoded by the linear system : one variable per non-atomic subformula, with the inequalities (3.1a)–(3.1c) for , , . The quantifier of block is when is even, so
is a sentence.
The game adds a bookkeeper, player , who moves last. Player controls the atoms of , and player also controls auxiliary variables ; the bookkeeper controls the , a variable fixed to , and auxiliary variables . Two gadgets, (4.1) and (4.6), let the bookkeeper and player 1 turn the linear criteria into the piecewise-linear functions (or for universal ) and , where is the length of , , and at , otherwise.
Let be the set of optimal solutions of . Then ; at every optimum all atom variables and all are binary; and
Moreover, when (3.3) holds, is player 's block in some optimum iff is binary and the sentence (4.17) holds at the truth valuation of .
In attack order: Lemma 3.1 (correctness of on binary inputs); Lemma 4.1 (robustness of near binary inputs); Lemmas 4.2 and 4.3 (the bottom two levels of a bounded linear multi-level program are solvable, via LP duality); the bookkeeper identities and in ; (4.2) and (4.3) (player 1's and player 's responses on the gadgets); Lemma 4.4 (the induction on with the higher blocks fixed). Companion theorems: Corollary 4.6 (the bilevel case: value iff ), the §2 Example, and Proposition 3.2 (the pure binary game ).
The theorem shows that deciding the value of a -level linear program with fixed criteria is at least as hard as deciding sentences, so known exact algorithms for multi-level linear programs cannot be expected to run in polynomial time once , and even recognising an optimal move is -hard. The bilevel case is an early NP-hardness proof for bilevel linear programming, and the construction (a bookkeeper player and absolute-value gadgets that force binary choices) is a template for hardness reductions to leader–follower problems.
The result is proved in the paper but, to our knowledge, has no machine-checked formalization. A formal development makes precise the solution concept (conditional rather than lexicographic minimisation), which the literature states in several inequivalent ways, and checks a proof whose printed version leaves cases to the reader (the , cases of Lemma 4.1, the universal cases of Lemma 4.4) and applies Lemma 4.3 to a feasible set that is unbounded (the (4.1) variable has no upper bound).
The obvious argument, "each existential player picks a satisfying assignment and each universal player a counterexample", works for the pure binary game (Proposition 3.2) but not for continuous variables: a player may choose fractional values, and the solution sets of a multi-level program need not exist (the §2 Example). The work is in showing that every player is forced to binary choices. Player 1's fractional choices are ruled out only through the robustness estimate of Lemma 4.1 with the weight , and the existence of optimal solutions at every level has to be established along the induction, since it fails for general three-level programs.
k : Fin p is the paper's , owned by player in .solSet encodes the conditional minimisation of (3.7), p. 152. HasValue N w requires ; the value is not modelled.A complete development needs a linear-programming duality argument for Lemma 4.2 (Mathlib has IsExtreme and Set.extremePoints; LP duality is on the platform as a single-level theorem) and an induction over the levels of the game. The definitions MultilevelProgram, solSet and the formula encoding LSys are reusable for other complexity results on hierarchical optimisation. Proofs of any milestone, including the generic Lemmas 4.2–4.3 and the formula Lemmas 3.1 and 4.1, are welcome independently.
Reliability theory classifies life distributions by how they age. A device whose failure rate tends to increase over time is "wearing out", and the class of distributions with increasing hazard rate average (IHRA) is the one that is closed under forming coherent systems of independent components (Birnbaum, Esary and Marshall, 1966). This makes IHRA the natural ageing class for systems. It also raises a question: which physical failure mechanisms produce IHRA lives?
Esary, Marshall and Proschan's paper Shock Models and Wear Processes (Ann. Probability 1, 1973) answers this for two kinds of mechanism. In the first, damage arrives in discrete amounts at the epochs of a Poisson process of shocks. In the second, damage accumulates continuously. In both, the device fails when the accumulated damage first exceeds a fixed capacity. This mission covers the second kind: a wear process and its first passage time above a level. The paper shows that the first passage time is IHRA under three qualitative conditions: wear starts at zero and only grows, the process is Markov, and accumulated wear and age make further wear more likely. Nothing else is assumed about the law of the wear.
A short timeline. Birnbaum, Esary and Marshall (1966) introduced the IHRA class and proved it is closed under coherent systems. Morey (1965) studied first passage times of wear processes under an extra monotonicity assumption. Esary, Marshall and Proschan (1973), §4, proved the IHRA property first for Poisson shocks with i.i.d. damages (Corollary 4.2, (4.7)), then for dependent damages (Lemma 4.1b, (4.7b)), and finally for continuous wear (Theorem 4.10).
Let be a probability space. "Decreasing" means non-increasing throughout.
A survival function is IHRA if is decreasing on (p. 631). For an exponential life, is constant. IHRA says the average failure rate over never decreases.
Dependent damages. Let be nonnegative random variables, the damages caused by successive shocks, and let and . The paper's conditions (p. 636) are:
Wear process. is the wear accumulated in . The conditions (pp. 640–641) are:
The first passage time above a level is . Its survival function is , and is the distribution function of the wear at time .
If satisfies (4.8), (4.9) and (4.10), then for every level
that is, has an IHRA distribution.
An optional extra item states Corollary 4.2 (4.7b): Poisson shocks of rate with damages satisfying (4.3)–(4.5) give an IHRA life .
The result. Theorem 4.10 derives an ageing property of a failure time from qualitative properties of the damage process alone: no distributional form, no stationarity and no independence of increments is assumed. Together with the closure of IHRA under coherent systems, this lets a reliability engineer conclude that a system built from components failing by wear has an IHRA life. Examples include processes with nonnegative stationary independent increments started at the origin, such as compound Poisson processes and infinitesimal renewal processes (p. 641). Lemma 4.1b is the discrete analogue: a sequence of probabilities with decreasing is what Theorem 3.1 (3.4) needs to give an IHRA life under Poisson shocks.
Formalizing it. The results are proved in the paper. As far as we know none of them has been machine-checked. The formalization needs, and would make reusable, a statement of the Markov property for a continuous-time real process in terms of Mathlib's conditional expectation, versions of conditional distributions with monotonicity constraints, and the passage from a discrete-time grid to continuous time for first passage times. Each of these is a step a probabilist writes in one line and a proof assistant does not.
The paper's proof is short, but every sentence hides a measure-theoretic step. The first claim, that the grid increments satisfy (4.3)–(4.5), requires turning the Markov property and the monotonicity of the increment law into conditional laws of given . Those conditional laws are defined only almost everywhere, and the monotonicity must be preserved along the way. Lemma 4.1b itself is an induction that integrates the monotonicity conditions against the law of . The extension from rational to arbitrary ratios uses the monotonicity of paths. The identification of as a right limit of needs the pathwise reading of (4.8). The natural first idea, approximating by a compound Poisson process, would add hypotheses the theorem does not have.
All objects sit in the namespace ShockWear.WearProcess, in one definition file. The committed conventions:
pr with IsProbabilityMeasure. Time is ; with every measurable.condDistrib. The monotonicity conditions (4.4), (4.5), (4.10) are imposed on these versions, on the paper's regions , . "Is decreasing in " is read as "has a version decreasing in ".X i is the paper's , and the kernel κ k describes given .Trivializing formalizations are ruled out: (4.9) and (4.10) are not replaced by independence or stationarity of increments, nor by a compound Poisson model. Those are examples (p. 641), not hypotheses. Monotonicity is never imposed on Mathlib's condDistrib itself, whose values off the support of are unconstrained. A sorry-free local check confirms the hypotheses are satisfiable: the deterministic process satisfies (4.8)–(4.10), and constant damages satisfy (4.3)–(4.5).
Contributions are welcome on any milestone. The reduction (milestone 2) and the induction of Lemma 4.1b are the substantial parts. Lemmas about versions of conditional distributions under Markov processes would be reusable well beyond this mission.
Reliability theory classifies life distributions by how they age. A device whose remaining life, once it has survived to age , is stochastically shorter than the life of a new device is called new better than used (NBU). The NBU class, together with the classes IHR (increasing hazard rate) and IHRA (increasing hazard rate average), organizes much of the theory of maintenance and replacement: Marshall and Proschan showed that the NBU property is what makes certain replacement policies beneficial, and Barlow and Proschan's monographs build the statistical theory of reliability on these classes.
A question that runs through this literature is where such ageing properties come from physically. Esary, Marshall and Proschan (Ann. Probability 1973) answer it for shock models: a device is hit by shocks arriving in time as a Poisson process, each shock adds a random amount of damage, and the device fails when the accumulated damage exceeds its threshold. Section 4 of their paper treats a fixed threshold and shows that the life is IHRA for every damage law. Section 5, the subject of this mission, lets the threshold itself be random, which models the variation between individual items of a production lot. It then asks which ageing properties of the threshold law are inherited by the life distribution, and which are forced if the inheritance is to hold whatever the damage law.
All distributions are laws of non-negative random variables. For a distribution on with for (a damage law), denotes the -fold convolution of , with the point mass at ; thus for independent .
A threshold law is a distribution with for ; write for its survival function. If the threshold is independent of the damages, the probability of surviving shocks is
If shocks arrive as a Poisson process of rate , the device's life distribution has survival function
A survival function is NBU if for all ; it is IHR if is non-increasing in for each , and IHRA if is non-increasing in . The discrete analogue of NBU for the sequence is submultiplicativity, .
For a threshold law with for :
the quantifier ranging over every damage law ; and if is NBU, then for every damage law and every the life distribution of (5.2) is NBU.
Theorem 5.1 (the life is exponential for every iff is exponential) and Theorem 5.2 (b), (c) (an IHR threshold makes non-increasing for every ; non-increasing for every forces to be IHRA) are posed as companion statements from the same section.
Theorem 5.3 is a characterization: the NBU class is exactly the class of threshold laws for which the cumulative-damage mechanism preserves the discrete NBU property under every damage law. Combined with Theorem 3.1 (3.5), it gives a physical derivation of NBU life distributions: an item with an NBU random strength, subject to Poisson shocks with arbitrary i.i.d. non-negative damage, has an NBU life. Theorems 5.1 and 5.2 place the exponential and the IHR/IHRA classes in the same framework, and the authors record that whether an IHRA threshold suffices in Theorem 5.2 (b) is left unresolved.
The results are proved in the paper. No machine-checked version is known to exist; this mission produces one. A complete development also supplies reusable infrastructure: convolution powers of laws on as Mathlib measures, Poisson mixtures of a sequence, and the ageing classes of p. 631 as predicates on survival functions.
The equivalence couples a property of one function, , to a family of inequalities indexed by every damage law, and the left side is about convolutions while the right side is pointwise. Two points make the statement harder than it looks. First, (5.1) as printed is , whereas the paper's proof works with ; the two agree only when and have no common discontinuities, and they can disagree as soon as has an atom where has one, a case the left side of the equivalence includes. A formal proof cannot invoke that convention. Second, the second sentence of the theorem passes through a Poisson series (5.2) whose terms involve the whole sequence , so the NBU property of is a statement about a power series in , not about any single .
Measure.conv power with , and is the mass of .Contributions welcome: proofs of the milestones, a library for Poisson mixtures and convolution powers of laws on , and the extra items of §5.
Many models in probability, statistical physics and the theory of stochastic networks are interacting particle systems: infinitely many sites, each in state 0 or 1, each updating at random according to the states of a few other sites. A basic question about such a system is ergodicity: does it have a unique stationary distribution, and does its law converge to it from every initial configuration? For infinite systems the question is hard, because the state space is uncountable and standard Markov chain arguments do not apply.
Holley and Liggett (Ann. Probab. 3 (1975), 643–663) introduced a class of such systems, the proximity processes, which arise from a coupling of more general weakly interacting systems (the settings of Vasershtein (1969), Dobrushin (1971) and Chover (1974)), and showed that each proximity process is dual to a process of finite sets, the branching process with interference. Duality turns a question about an infinite-dimensional process into a question about a process whose states are finite sets. The paper uses it to give short proofs of ergodicity criteria and, in its §5, to study the invariant measures of the voter model. Duality of this kind became one of the main tools of the field; see Liggett, Interacting Particle Systems (Springer, 1985).
This mission formalizes the discrete-time half of the paper: the duality theorem (1.6) and its first applications, Corollary (3.1) and Corollary (4.1).
Let be a countable set of sites and the set of configurations , with the product -algebra. For , is the set of occupied sites.
The data of the model are, for each site , a sequence of finite subsets of and a probability distribution on .
The proximity process is the Markov chain on whose transition function is the product measure
where puts mass on . In words: each site independently picks an index with probability and becomes exactly when the set contains an occupied site. denotes the law at time started from .
The branching process with interference (b.p.i.) is the Markov chain on the collection of finite subsets of with transition function
the sum over all sequences with : each particle at splits into particles on with probability , and particles landing on the same site merge. denotes probabilities for the chain started at .
For , .
For all , and ,
The proof is an induction on whose steps are four displayed identities on p. 647:
and the point mass on the all-zero configuration is the only stationary distribution; along the way, (3.5): .
The duality identity expresses every finite-dimensional "all vacant" probability of the proximity process, which determine its law, through a chain on finite sets. Consequences in the paper: a sufficient condition for convergence to the all-zero configuration (Corollary (3.1)), which in the nearest-neighbour example on gives ; the sharper range , i.e. , for that example (Corollary (4.1)), which the interference term makes possible; and, in continuous time, the analysis of the invariant measures of the voter model.
The results are classical and proved; a search of Prove2Me and Mathlib found no machine-checked proof of any of them. A formalization contributes a Lean model of an infinite-product Markov kernel on with its -step laws, a model of a set-valued branching chain, and the duality between them, which are reusable for other duality arguments (contact process, voter model, coalescing random walks).
The two sides of (1.7) are defined independently and live on different spaces. The left side is the time- law of a chain on the uncountable space , obtained by iterating an infinite product kernel; the right side comes from a transition matrix on the countable set of finite subsets of , whose entries are themselves infinite sums over sequences indexed by a finite set. Neither side can be computed in closed form beyond , so no direct evaluation proves the identity for general .
Two technical points stand in the way of a naive argument. Evaluating a product kernel on a cylinder event and integrating it against a previous law requires the kernel to be measurable in , a statement about cylinder sets of an infinite product that a hand proof passes over. And the natural recursion for -step probabilities of the b.p.i. adds the new step at the end, while the comparison with the proximity process needs information about the first step; the two orders agree only by a Chapman–Kolmogorov argument over a countable state space with -valued sums. Corollary (4.1) further needs quantitative estimates of survival probabilities for specific initial sets on .
All objects are in the namespace HolleyLiggett.Duality, in one definitions file.
Bool (true = 1), is Config I := I → Bool with the product -algebra, is Finset I.[Countable I], N : I → ℕ → Finset I (finite sets) with N i 0 = ∅, and f : I → PMF ℕ (probability distributions). A finite collection is the case for .Measure.infinitePi of the two-point measures; the -step law is proxLaw, iterating Measure.bind from the point mass at . Measurability of the kernel is a true fact that solvers must prove; it is not assumed.bpiProb follow the last-step recursion . All probabilities are in ℝ≥0∞, and each over sequences is an unconditional sum over ↥F → ℕ.The continuous-time duality (Theorem (2.12)), Corollaries (3.9) and (4.15) and the voter model of §5 are out of scope. Contributions welcome: the measurability and probability facts for proxStep, Chapman–Kolmogorov for bpiProb, and proofs of the milestones.
Little's law says that the long-run average number of customers in a system equals the arrival rate times the average time a customer spends there. It is one of the most used identities in queueing theory, and it holds on individual sample paths under weak conditions (Little 1961; Stidham 1974). Many quantities of interest are not head counts, however: the work in the system, the cost accumulated by customers in progress, the number of tokens a customer holds in some state. For these a more general relation is needed, between a time average and a customer average , of the form .
Heyman and Stidham (Oper. Res. 28 (1980)) prove such a relation on each sample path, for an arbitrary real-valued function attached to each customer, under a support condition that is much weaker than the continuous-sojourn assumption of the theorem. They then show by a counterexample that the support condition cannot simply be dropped, even when every customer function is an indicator.
Timeline.
Fix one sample path. Customers arrive at epochs ; ties are allowed. The arrival count is the number of with , and the arrival rate is when the limit exists.
Customer carries a real-valued function on . Its total is , and the rate is . The customer average and time average are
When is the indicator of , is the sojourn time and is the number in system, so is .
The ASSUMPTION of the paper is that for each there is with
For signed write , , and let , , , be the corresponding totals, rates and averages.
Assume (i), (ii) and (v) for every . If , and exist with and , then exists, equals , exists, and
The result. converts between a time average, which is what a system designer measures, and a customer average, which is what a customer experiences. Applied to different it yields , the relation between average work in system and average customer work, and relations between time-stationary and embedded-chain probabilities; §2 of the paper derives the GI/M/c/K relation this way. Because the support condition (i)–(ii) allows a customer's contribution to be interrupted (leaving and re-entering the system), it covers preemptive priority queues and nodes of networks, which the continuous-sojourn theorem does not. The counterexample marks the boundary: with interrupted sojourns, indicator functions and finite , alone do not suffice.
Formalizing it. The result is proved on paper, with two steps delegated to earlier work "by mimicking" Lemma 1 and Theorem 2 of Stidham 1974. The indicator special case (with strictly increasing arrivals) is already proved on Prove2Me as queueing_general_littles_law (wenxinzhang). This mission asks for the general, signed, pathwise statement and its proof steps, a counterexample with an exactly computed time average , and the ensemble corollary.
The obvious argument, exchanging the time integral of with the sum over customers, gives , but a customer that has arrived by may contribute only part of its total by . The sandwich only bounds this loss; the hard step is showing that and have the same limit, which needs to compare at time with at a slightly earlier time. Without (ii) this fails, as the counterexample shows: customers there remain "open" for a window proportional to their index.
For signed the sandwich is not available directly, and the proof splits into positive and negative parts; the exchange of sum and integral then needs the finiteness of the parts on every .
All statements except Corollary 3 are about one fixed sample path; the paper's "with probability one" is the pathwise statement applied to almost every path, and Corollary 3 states this explicitly with a probability measure and almost-sure hypotheses.
Conventions:
Monotone with ; ties are allowed.Added hypotheses: milestones (3), the identity and (6) assume , which the paper derives from (2); Corollary 3 assumes is integrable, which its definition of the ensemble average presupposes.
A formalization in which sums only over arrived customers, or in which a non-integrable or has integral , would make the statements trivial or different; the definitions rule this out by summing over all customers and requiring integrability.
Needed infrastructure: Cesàro averages and counting functions of nondecreasing sequences, interchange of countable sums and integrals for locally finite families, and harmonic sums . The counting-function lemma (2) and the squeeze for and are reusable well beyond this mission. Proofs of any milestone are welcome independently.
Newton's method for a nonlinear system , with , solves the linear system at every step. For large systems that solve is itself iterative (a Krylov method such as GMRES), and it is stopped early. The resulting inexact Newton methods, introduced by Dembo, Eisenstat and Steihaug (SIAM J. Numer. Anal. 19 (1982)), accept any step with , where the forcing term controls how accurately the linear system is solved. Their theory is local: it applies once the iterates are near a solution with invertible derivative.
Practical solvers (Newton–Krylov codes in large-scale simulation, nonlinear solver libraries such as PETSc's SNES and SUNDIALS' KINSOL) combine such inexact steps with a globalization, most often backtracking along the step. Eisenstat and Walker (SIAM J. Optim. 4 (1994)) gave the global convergence theory for this combination: what can be said about the iterates from an arbitrary starting point, with no assumption that a solution exists or that is invertible anywhere.
Timeline. Dembo, Eisenstat and Steihaug (1982) proved local convergence of inexact Newton methods. Dembo and Steihaug (Math. Program. 26 (1983)) studied truncated Newton methods for unconstrained minimization. Brown and Saad (1990) studied globalized Newton–Krylov methods with line searches and model trust regions, under the inner-product norm. Eisenstat and Walker (1994) gave the general framework treated here, for an arbitrary norm. Their 1996 paper (SIAM J. Sci. Comput. 17) proposed the forcing-term choices that are now standard.
Let be with an arbitrary norm , and let be continuously differentiable with derivative . A point is a limit point of if every ball contains for infinitely many .
Algorithm GIN (global inexact Newton method). Fix . At each , find a level and a step with
and set . Condition (2.1) says that reduces the norm of the local linear model by the factor . Condition (2.2) asks that itself decrease by a fixed fraction of that predicted reduction.
Algorithm MR (minimum reduction method). Fix and . At step , choose and a curve with for (5.1). Start at . While (2.2) fails for , replace by for some . Then set .
Algorithm INB (inexact Newton backtracking). Choose and an inexact Newton step at level . While (2.2) fails, shorten the step, , and raise the level, . INB is MR with the backtracking curve (6.1).
An algorithm does not break down if it produces an infinite sequence of iterates, in particular if every while-loop exits.
If Algorithm INB does not break down and is a limit point of at which is invertible, then
The statement assumes no solution, bounded level set, Lipschitz derivative or particular norm. The last clause says that backtracking eventually stops, so the local rate is governed by the forcing terms .
In attack order:
Further items, which are not milestones: Corollary 6.2 (exact Newton with backtracking takes full Newton steps eventually), Theorem 5.2 for Algorithm TL, Lemma 3.1 (existence of acceptable GIN steps), and Proposition 2.1 (the Goldstein–Armijo alpha condition implies (2.2) in the Euclidean norm).
The result. Theorem 6.1 is the global convergence guarantee for the inexact Newton backtracking method that Newton–Krylov solvers implement. It separates three outcomes: the iterates diverge, they accumulate only at points where is singular, or they converge to a solution with invertible derivative and eventually take the unmodified inexact Newton steps. In the third case the local theory of Dembo, Eisenstat and Steihaug applies from some iteration on, so the forcing terms alone set the convergence rate. Theorem 5.2 is the template: §§6–8 of the paper derive the convergence of backtracking, equality-curve and dogleg-type methods from it by verifying (5.6).
Formalizing it. The results are proved on paper and none of them has a machine-checked proof that we know of. The mission produces a library of algorithm-run predicates with explicit while-loops for inexact Newton methods. It also checks the paper's reduction chain (INB is a run of MR, MR is a run of GIN) and the global convergence theorems in an arbitrary finite-dimensional norm.
The obvious argument fails at both ends. Sufficient decrease (2.2) alone gives monotonicity of , but not convergence of the iterates. On the page, admits sequences satisfying (2.2) with both as limit points. Convergence of to needs , and nothing in the algorithm states this. In Theorem 5.2 it has to be derived from the exit level of the while-loop, which depends on a neighbourhood of where the linearization error is uniformly controlled. A solver must combine a limit-point argument (only infinitely many iterates are near , not all of them) with the loop's worst-case backtracking factor . The invertibility of enters only through the bound (5.6) for the backtracking curve, which must be established uniformly in .
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]). This is exactly " with an arbitrary norm". Fin n → ℝ (sup norm) and EuclideanSpace would each fix one norm. Only Proposition 2.1 assumes an inner product space, as the page does.fderiv ℝ F, with ContDiff ℝ 1 F (the paper's standing assumption). Invertibility is ContinuousLinearMap.IsInvertible, and is ContinuousLinearMap.inverse.IsGINRun, IsMRRun, IsINBRun, plus IsTLRun, IsENBRun). The steps and levels the algorithm says to "find" or "choose" are data constrained only by the stated conditions. A while-loop is recorded by its number of passes and factors . Every trial before the last fails the loop's test and the last one passes it. Termination is part of the run.MapClusterPt xstar atTop x. "For all sufficiently large " is ∀ᶠ k in atTop. The paper's "whenever is sufficiently near [and is sufficiently large]" is ∃ Γ, ∃ δ > 0, [∃ K,] ∀ k [≥ K], x k ∈ ball xstar δ → …. precedes ("independent of "), and the " large" clause appears only in (3.2), where the page has it.F = id on ) confirms that the INB, GIN and ENB run predicates and the goal's hypotheses are satisfiable, so the goal is not vacuous.Reliability theory classifies life distributions by how they age. The IHRA class (increasing hazard rate average) is the smallest class of life distributions that contains the exponential distributions and is closed under forming coherent systems and taking limits in distribution (Birnbaum, Esary and Marshall 1966). It is therefore the natural class for the lifetime of a system built from components that wear out. A distribution belongs to it when its survival function satisfies: is decreasing in .
Esary, Marshall and Proschan (Ann. Probability 1 (1973) 627–649) asked where such ageing comes from physically. Their answer is a shock model: a device receives shocks at the epochs of a Poisson process, each shock does random damage, and the device fails when the accumulated damage exceeds its capacity. The central result of their §4, formalized in this mission, is that this model always produces an IHRA life, whatever the damage distribution. In the authors' words, "the IHRA property has been obtained … as an implication of a natural physical model. The only hypothesis imposed upon is that it be the distribution of a nonnegative random variable." The paper is a standard reference of reliability theory and the source of the cumulative damage model used across maintenance and insurance applications.
Shocks arrive according to a Poisson process with rate . Write for the probability that the device survives the first shocks; then (display (2.2)). Conditioning on the number of shocks in gives the shock survival function (2.1):
with for . The weights are the Poisson probabilities.
In the cumulative damage model the th shock causes a damage , the damages are independent with common distribution function (so for ), and the device survives shocks when , for a fixed threshold . Hence (4.1)
where is the -fold convolution of and is degenerate at . A distribution with survival function is IHRA if is decreasing in ; throughout, "decreasing" means non-increasing.
For every distribution on , every and every threshold ,
This is the first of the three statements of Corollary 4.2; the second ((4.7a), independent damages that worsen with ) is an extra item of this mission, and the third ((4.7b), dependent damages satisfying (4.3)–(4.5)) belongs to mission III of this series.
Lemma 4.1a and Corollary 4.2 (4.7a); Theorem 4.4 ( is constant in iff has no mass in ); Corollary 4.5 ((4.7) is exponential iff has no mass in ); Corollary 4.11 ( is decreasing for the count of an ordinary renewal process).
The goal turns a modelling assumption into a theorem: anyone who models failure as accumulated nonnegative damage under Poisson shocks obtains, without further checks, every consequence of IHRA proved in reliability theory, including the closure of the class under the formation of coherent systems. Theorem 3.1 (3.4) is reusable on its own: it reduces the IHRA property of any Poisson mixture to a discrete condition on the , and the same scheme drives the first passage result for wear processes (Theorem 4.10, mission III). Lemma 4.1, applied to renewal processes, gives Corollary 4.11, a statement about renewal counts with no shock model in sight.
All results are proved in the paper; none has a machine-checked proof that we know of. The Mathlib library has the Poisson distribution and the convolution of measures, but no reliability classes, no total positivity and no variation diminishing property. The mission's output is a formal proof of the paper's chain of results and, along the way, reusable statements about Poisson mixtures and convolution powers.
Two steps resist a direct argument. The first is the transfer from sequences to functions: knowing that changes sign at most once says nothing pointwise about the series . The paper invokes the variation diminishing property of the totally positive Poisson kernel (Karlin, Total Positivity, 1968), which is not in Mathlib. The second is Lemma 4.1, an inequality between convolution powers of an arbitrary law: no density, moments or continuity may be assumed, atoms at and at are allowed, so any argument through densities or Laplace transforms loses generality. A further subtlety is the passage from "one sign change of for every " to the monotonicity of , which needs care where vanishes.
Measure.conv) starting from the point mass at , and is the real number .A complete development needs: the variation diminishing property of the Poisson kernel (reusable for every Poisson mixture), monotonicity of via convolution integrals, and elementary facts about real powers and sign changes. Proofs of any milestone or extra item, and general total positivity lemmas, are welcome.
Reflected Brownian motion on the orthant is the diffusion that arises as the heavy-traffic limit of open networks of queues. In a -station network the scaled queue-length vector lives in the nonnegative orthant ; in the interior it moves like a Brownian motion, and when a station empties the process is pushed back into the orthant in a direction determined by the routing of customers between stations. Harrison (1978) obtained such a limit for two queues in tandem, and Reiman (Open Queueing Networks in Heavy Traffic, Math. Oper. Res. 9 (1984)) showed that general -station open networks lead exactly to the class of processes studied here.
Classical constructions of reflected diffusions (Stroock and Varadhan 1971, Watanabe 1971) require a smooth boundary and a reflection direction varying continuously on it. The orthant has corners and the reflection direction jumps between faces, so those results do not apply. Harrison and Reiman (Reflected Brownian Motion on an Orthant, Ann. Probab. 9 (1981)) construct the process pathwise, following Skorokhod's one-dimensional approach, and derive its Markov property from the construction. The process has since become the standard object in the diffusion approximation of queueing networks.
Fix a positive integer . Vectors in are row vectors, indexed by . Let be a covariance matrix (symmetric, nonnegative definite), a drift vector, and a nonnegative matrix with zeros on the diagonal and spectral radius strictly less than one. is the nonnegative orthant.
Let be the space of continuous paths with the topology of uniform convergence on compact intervals, and the paths with . For , the Skorokhod problem asks for with, for every ,
nondecreasing with (7), and increasing only at times where (8). In matrix form, . Theorem 1 of the paper shows there is exactly one such pair, written , .
The process is obtained by feeding a Brownian path into this map. On a probability space let be a -dimensional Brownian motion with covariance matrix , drift and almost surely, with independent of the increments of . Let . Set and where , and on the exceptional null set. is reflected Brownian motion on with reflection matrix .
There is a family of Markov transition kernels on , depending only on , such that for every such , , :
Here (1)–(4) are (5)–(8) for the paths of , , . The kernel is chosen before the probability space and the initial law, which is what "stationary transition probabilities" means.
The milestones follow the proof of Theorem 1 on pp. 304–305:
Milestone 7 is the platform theorem Reiman84.QueueLength.lemma_1, posed as an open target by an earlier mission (Reiman 1984 cites it as its Lemma 1). It is referenced here and not posed again.
Corollary 1 is what makes a usable stochastic process: adaptedness and almost-sure uniqueness say is determined by the driving Brownian motion in a non-anticipating way, and the Markov property with time-homogeneous kernels is the starting point for the change-of-variable formula of §3, for generators, for stationary distributions, and for the heavy-traffic limit theorems in which appears as the limit. The pathwise map and its Lipschitz continuity are reused throughout queueing theory: the continuous-mapping argument for heavy-traffic limits rests on exactly the continuity (10) established here.
The results are classical, with complete published proofs. None of them has a machine-checked proof. Mathlib has the measure-theoretic layer (kernels, conditional expectation, independence) but no reflection maps, no construction of multidimensional Brownian motion with drift, and no Markov-process theory in continuous time. This mission provides a formal statement of the pathwise reflection theory and its probabilistic consequence on which such a development can build.
The pathwise part is a contraction argument, but the contraction is not in the original norm: the map need not be a contraction for any standard norm when only the spectral radius of is below one. The proof first changes coordinates by a positive diagonal matrix, and the right norm must be matched to the row-vector convention. The fixed-point characterization also has to be shown equivalent to the complementarity condition (8), which is where the zero diagonal of enters.
For Corollary 1, the difficulty is measure-theoretic. Adaptedness requires measurability of a path functional with respect to the uncompleted natural filtration, which uses (9) and (10) and the fact that continuous paths are determined by countably many coordinates. The Markov property requires the regeneration identity (11) together with independence of the post- increments of from , and a kernel that is jointly measurable and independent of the initial law. Conditioning on alone, without identifying the future as a fixed functional of and an independent Brownian motion, does not give a kernel that is the same for all .
Fin K → ℝ (paper index = Lean index ), with ; row vector times matrix is Matrix.vecMul. Paths are functions ℝ → Fin K → ℝ; only times are constrained.Reiman84.QueueLength.lemma_1. is PosSemidef.Reiman84.QueueLength.IsReflectionPair; (8) reads " is constant on every interval on which ". is IsCPlus; uniform convergence on compacts is UocTendsto; Brownian motion from with drift and covariance is IsDriftedBM.Out of scope: Theorem 2 (the change-of-variable formula, which needs stochastic integration), the necessity of spectral radius , and §§3–4. Useful contributions beyond the milestones include a construction of multidimensional Brownian motion with drift in Mathlib, the Skorokhod map as a function on , and general lemmas on measurability of continuous path functionals.
A firm that will receive or deliver a quantity of a commodity, currency or security at a future date carries price risk until that date. When the asset itself cannot be traded in the meantime, the standard instrument for reducing that risk is a futures contract on a correlated asset: the firm takes a position in futures and adjusts it over time, and the gains or losses of the futures position offset part of the movement of its commitment. Choosing that position is the hedging problem. The classical answer, the minimum-variance hedge ratio, is a static one-period rule. Duffie and Richardson (Ann. Appl. Probab. 1991) solved the dynamic version in continuous time with a quadratic criterion: minimize the expected squared deviation of terminal wealth from a target. Their explicit feedback solution became a reference point for the later literature on mean-variance hedging in incomplete markets (Schweizer, Gouriéroux–Laurent–Pham, and others), where the same quadratic criterion is studied under general semimartingale prices.
Fix a horizon and a probability space carrying a two-dimensional standard Brownian motion with its filtration . Let be bounded measurable functions on , with bounded away from zero and . The Brownian motion has instantaneous correlation with . The committed asset and the futures price follow
The hedger is committed to units of at time . A trading strategy is a progressively measurable process (the futures position) with ; denotes the set of them. Its futures gain is the stochastic integral , and the terminal wealth is . Given a target level , problem (3) is
With , the tracking process is , so that , and the feedback map is
where solves , . The strategy depends only on the gains realized so far and the current price .
for every commitment , every target and every solution of (10). No constant is hard-coded: the statement is the paper's for arbitrary coefficients satisfying the standing hypotheses.
Two further items, not milestones, formalize §4: Lemma 3 (a solution of (3) is mean-variance efficient) and §4.1 (maximizing the quadratic utility , , is problem (3) with ).
Proposition 1 gives the optimal dynamic hedge in closed feedback form for every target level at once. Varying traces out the whole mean-variance frontier of terminal wealth (Lemma 3), and the choice solves the quadratic-utility problem (§4.1); the minimum-variance hedge of §4.3 of the paper is obtained by optimizing over . The result is also an instance of a general pattern: a quadratic hedging problem in an incomplete market reduces to an projection onto the space of attainable gains, and the projection is computed by a linear SDE.
The result is proved in the paper, in six pages. No machine-checked version of it, or of any continuous-time hedging result, exists on the platform. A formalization requires Itô's formula for products of Itô processes, the zero-mean property of square-integrable stochastic integrals, Fubini's theorem for moments, and existence for a linear SDE with an Itô-process forcing term; each of these is reusable well beyond this paper.
The projection step (Lemma 1) is Hilbert-space geometry and the final ODE step is Grönwall. The difficulty lies in between: the orthogonality must be verified against every trading strategy , about which only is known. A computation that treats as bounded, continuous or simple does not suffice. Making the paper's moment computations rigorous requires controlling the integrability of products such as and , proving that the stochastic-integral parts of Itô's product rule are true martingales rather than local martingales, and differentiating expectations in time when the coefficients are only measurable, so that derivatives exist only almost everywhere.
The stochastic layer is the published definition file Peng1990_SMP_Stochastic (the Itô integral and Itô processes on time), imported, not redefined. The mission commits to the following conventions.
Proposition 1 would hold vacuously if equation (10) had no solution; the existence milestone rules this out and must be proved, not assumed. Contributions are welcome on Itô's product formula and the martingale property of Itô integrals in the Peng framework, on the existence of solutions of linear SDEs, and on the Grönwall-type uniqueness for (13).
Stochastic optimization asks for a decision in a set that minimises an expected loss when the distribution of the data is known only through a sample . The classical estimator, sample average approximation, replaces by the empirical distribution . Distributionally robust optimization instead minimises the worst-case expected loss over all distributions close to . Duchi, Glynn and Namkoong (arXiv:1610.03425v3; Math. Oper. Res. 46(3), 2021) take the neighbourhood to be an -divergence ball of radius and show that the robust optimal value is a calibrated upper confidence bound for the population optimum, in the spirit of Owen's empirical likelihood.
A confidence bound is useful only if the robust problem still estimates the right thing. Section 5 of the paper answers this: under essentially the conditions that make sample average approximation consistent, the robust optimal value converges to the population optimal value, and the robust minimisers approach the population minimisers. This mission formalizes that consistency result (contribution (iv), p. 3, and §5.1).
Let be i.i.d. random elements of a separable metric space with law , and let be the empirical distribution of . Let be lower semicontinuous on , with measurable for , and let be a nonempty closed feasible set, as in the paper's opening setup (p. 1).
The divergence generator is convex with ; Assumption A asks moreover that be three times differentiable near with and . For a distribution with weights on the sample points, . The robust objective and the population objective are
with radius parameter . Their solution sets are and (display (23)). The inclusion distance from a set to a set is (display (6)).
Assumption E asks for a measurable envelope with for all and for some . A class of functions on is Glivenko–Cantelli (Definition 2) if almost surely.
Let Assumptions A and E hold, let be nonempty and compact, and let be continuous on for every . Then, in outer probability,
Both conclusions belong to the goal. No rate is asserted; the statement survives any later sharpening.
The result. Corollary 1 shows that robustness against a -divergence perturbation of the data costs nothing asymptotically: the robust optimal value and its minimisers are consistent for the population problem. Together with the paper's coverage theorem, this justifies using the robust value both as a point estimate and as an upper confidence bound. Theorem 7 is stronger than what the corollary needs: it controls every reweighting in the ball uniformly over , which is the uniform law of large numbers for distributionally robust objectives, and it needs only slightly more than the first moment that sample average approximation needs.
Formalizing it. The results are proved in the paper; none is machine-checked. A formal development would supply a Glivenko–Cantelli notion for parametric loss classes, the bracketing argument behind Example 5 (a uniform strong law over a compact parameter set, not in Mathlib), and the passage from uniform convergence of objectives to convergence of optimal values and of argmin sets in the inclusion distance. The last two are standard steps of M-estimation and sample average approximation theory that are reusable well beyond this paper.
The obvious argument writes as a reweighting term plus the ordinary empirical deviation and handles the second by the Glivenko–Cantelli property. The reweighting term is the obstacle: the weights are not bounded uniformly in for every divergence, and a Cauchy–Schwarz bound would need a second moment of the envelope, which Assumption E does not provide. The exponent pair and the uniform control of Lemma 13 are what make moments enough.
For the solution sets, uniform convergence of to does not by itself place the minimisers of near those of ; compactness of and continuity of are needed to separate on the complement of an -enlargement of from its minimum. Measurability is a further obstacle: suprema over uncountable and over the divergence ball need not be measurable, which is why the paper works with outer probability and outer almost-sure convergence.
ξ : ℕ → Ω → Ξ on a probability space, measurable, mutually independent (iIndepFun) and identically distributed with ξ 0; is the law of ξ 0, and uses ξ 0, …, ξ (n-1) (0-based indices). The separable metric sample domain and lower semicontinuous loss from p. 1 are explicit in Theorem 7 and Corollary 1. Decisions live in EuclideanSpace ℝ (Fin d); ℓ x is measurable for each .ℝ → EReal satisfying the published IsPhiDivergenceFunction (never , finite on , , convex on ) plus the smoothness of Assumption A, stated on on an open interval around .probUncertaintySet f (1/n,…,1/n) (ρ/n), i.e. . Every supremum "over with " is read over , as in (4a).∀ᵐ, which requires the exceptional set to have outer measure zero; convergence in outer probability is for every with Mathlib's outer measure and no measurability hypothesis.Chance-constrained programming replaces a linear program subject to by a problem in which some data are random and each constraint only has to hold with a prescribed probability. Charnes and Cooper introduced the idea in 1959 for scheduling heating-oil production against weather-dependent demand, and the formulation is now a standard modelling tool in operations research, finance, energy systems and engineering design (Charnes and Cooper 1959; Prékopa 1995).
A chance-constrained problem is not directly solvable: its constraints are probabilities of events that depend on the decision. The 1963 paper of Charnes and Cooper (doi:10.1287/opre.11.1.18) asks when such a problem has a deterministic equivalent, an ordinary mathematical program with the same feasible decisions and corresponding objective values, and when that equivalent is a convex program. Its first answer, for the expected-value ('E') model under linear decision rules and normality, is the subject of this mission. The resulting constraint form, a mean slack dominating standard deviations, is an early instance of the second-order-cone reformulation of individual normal chance constraints used throughout modern stochastic and robust optimization.
Timeline. 1959: Charnes and Cooper, chance-constrained programming with the heating-oil model. 1963: this paper, deterministic equivalents for the E, V and P models under linear decision rules . 1965: Miller and Wagner treat joint chance constraints with independent rows (doi:10.1287/opre.13.6.930). 1971: Prékopa's logarithmically concave measures give convexity of joint chance constraints under log-concave laws.
Let be a probability space. The data are a constant matrix with rows , a random right-hand side and random objective coefficients . A linear decision rule is an real matrix ; it chooses after is observed. Write , and .
The E-model (18) is
with one probability level per row: the constraints are row-wise, as in (3) of the paper, not a single joint constraint.
For let be the standard normal -quantile. With the moment functions (30),
the paper's deterministic program (29) in the variables , , is
Assume every is square integrable, every and integrable, and uncorrelated (), every variate normal (for every and , zero variance allowed), and . Then
The result. The theorem turns a problem whose constraints are probabilities into a finite-dimensional convex program whose data are the first two moments of and the means of . The optimal rules of (18) minimize (29), whose optimal value is the negative of the maximum in (18). The slack variables separate each constraint into a "quality" part (the mean slack ) and a "risk" part ( standard deviations), which is the interpretation the paper develops in (31) and its Appendix. The same constraint set serves the V-model (33), so only the objective changes between the two models.
Formalizing it. The result is classical and its proof is elementary, but the paper's argument is informal in ways that matter for a machine-checked version: it divides by a standard deviation it then allows to vanish, writes for what must be an upper-tail function, and labels a variance as while defining as a raw second moment. This mission produces a statement in which each of these points is settled, with every hypothesis explicit. No machine-checked version of the result is known to exist.
The chance-constraint step itself is a one-dimensional fact about the normal law, but three points need care. The variance of may be zero for some and ; then the law is a point mass, the quotient in (27) is undefined, and the equivalence must be argued separately, as footnote † of p. 28 indicates. The quadratic constraint of (29) alone, , describes both nappes of a hyperboloid and is not convex; convexity needs and the positive semidefiniteness of , which comes from square integrability of and not from normality. Finally, the identity relating , and the variance requires the integrals to be genuine, so the integrability hypotheses cannot be dropped.
Everything is in the namespace ChanceDetEquiv.EModel. The probability space is (Ω, P) with [IsProbabilityMeasure P]; A : Matrix (Fin m) (Fin n) ℝ, b : Ω → Fin m → ℝ, c : Ω → Fin n → ℝ, D : Matrix (Fin n) (Fin m) ℝ; is (A *ᵥ (D *ᵥ b ω)) i. Expectations are Bochner integrals and probabilities are P.real. Explicit readings of the paper's phrases:
Convex ℝ of the feasible set of (29) in , included; for the V model it also asserts ConvexOn ℝ of ;gaussianReal μ s for some and ; joint normality of is not assumed, since it would be a stronger hypothesis;Cohen2019_Robust_Phi; in (26)–(27) is read as the upper-tail function of , and is added so that is finite;Positive variance is a hypothesis of milestones 2 and 3, where (27) has a denominator. The goal and later milestones admit zero variance. The statements admit no trivializing reading: the normality hypothesis is satisfied by constant and by Gaussian , the integrability hypotheses rule out the junk value of non-integrable expectations, and rules out the junk value of .
A complete development needs: the normal CDF and quantile, the law of an affine image of a random variable, variance as in , and convexity of the epigraph of a seminorm composed with an affine map. The convexity milestones need no probability beyond and are reusable for any second-order-cone representation of individual chance constraints. Proofs of any milestone, and of the goal from the milestones, are welcome.
The related open platform item KallMayer.Chance.chapter2_theorem2_5 (convexity of a single normal chance-feasible set in ) is credited here and not restated: no item of this mission states the convexity of the set of feasible for (18). Related published items that are about other models: DRCVRP.RCI.prob_le_iff_valueAtRisk_le (chance constraints and value-at-risk for a general law) and the log-concavity results of NumStochOpt.LogConcave.
Open shops model production and service systems in which every job must visit every machine, but the order of the visits is free: a car that needs an inspection, a wash and a tyre change, a patient who needs several tests, a student who sits several exams. The survey of Graham, Lawler, Lenstra and Rinnooy Kan (Ann. Discrete Math. 5, 1979) fixed the three-field notation that the scheduling literature still uses, and classified the complexity of the problems it can express. Among the polynomially solvable cases, the preemptive open shop with makespan objective, , is one of the few multi-machine problems whose optimal value has a closed form for any number of machines and jobs.
Timeline.
There are machines and jobs . Job consists of operations ; operation must be processed on machine for time units. The processing-time matrix is : its rows are machines and its columns are jobs. Every job is available at time .
Preemption is allowed: an operation may be interrupted and resumed later. A schedule is a finite list of pieces , each meaning that processes during . A schedule is feasible if
The makespan is the time at which the last piece ends, and is its minimum over feasible schedules. The load of machine is the row sum , the length of job is the column sum , and
A row or column is tight if its sum equals and slack otherwise. A decrementing set is a set of strictly positive entries of with exactly one element in each tight row and each tight column and at most one in each slack row and each slack column.
For every ,
This says that the optimal makespan is exactly the largest machine load or job length, and that it is attained.
The result. The theorem turns an optimization over continuous-time schedules into the computation of sums. It certifies optimality by a counting argument, it is the base case for preemptive open shops with release dates and due dates, and it is used elsewhere in the survey (§4.4.6) to reduce problems on unrelated machines with preemption to open-shop instances. Because a nonnegative matrix whose row and column sums are all equal is a multiple of a doubly stochastic matrix, the theorem is a scheduling form of the Birkhoff–von Neumann decomposition. It also underlies timetabling and edge-colouring results for bipartite multigraphs.
Formalizing it. The theorem has been proved since 1976 and is textbook material. No machine-checked proof is known to exist: Mathlib has the Birkhoff–von Neumann theorem for doubly stochastic matrices but no model of open-shop schedules. A formalization adds a reusable model of preemptive multi-machine schedules with both disjointness requirements, a checked proof of the decrementing-set construction, and a termination argument the survey asserts without proof.
The lower bound is a one-line counting argument. The difficulty is the construction of a schedule of length exactly . Scheduling each machine's operations back to back gives length , but may run one job on two machines at once. Scheduling job by job has the symmetric defect. A greedy list schedule that only respects both constraints can leave machines idle and overshoot . The construction must keep every tight line busy at every moment while never letting a slack line fall behind. The existence of the decrementing set at each stage is the combinatorial core: it is a Hall-type matching condition, not a local choice. Termination is also not automatic, because a careless choice of step length can produce infinitely many shrinking steps.
All objects live in the namespace SchedSurvey.OPmtn. Machines and jobs are Fin m and Fin n, both 0-based, and processing times and piece endpoints are real numbers; integer data are a special case. A schedule is a List of pieces. Feasibility requires nonnegative start times, disjointness for pieces sharing a machine or a job (touching intervals allowed), and exactly units of processing for every pair . Every theorem assumes .
" is the maximum" is the predicate IsMaxLoad P C: all line sums are at most and one equals . The goal is stated in threshold form and mentions no maximum at all. The display defining on p. 313 prints for the second term; the following sentence shows it means the row sums , and the formalization uses those. The hypothesis matters only for , where the empty schedule finishes by every .
A trivializing formalization is ruled out: the goal mentions neither decrementing sets nor . Its "if" direction asserts that a schedule exists. Feasibility counts work per pair (machine, job), not per job, and forbids a job from running on two machines at once. Without either requirement the statement would be a different and easier theorem.
A complete development needs: list sums of interval lengths over disjoint intervals, the existence of decrementing sets (via Birkhoff–von Neumann, König's theorem or Hall's theorem on the bipartite graph of positive entries), the step and termination lemmas, and concatenation of schedules. The schedule model and the decrementing-set lemma are reusable for other preemptive shop problems. Contributions of alternative proofs of any milestone, for example a direct Hall-theorem proof of the existence of decrementing sets, are welcome.