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?
The proximal algorithm is the basic implicit scheme for minimizing a function : from the current point it moves to a minimizer of plus a quadratic penalty on the distance travelled. For convex its convergence theory is classical (Martinet 1970, Rockafellar 1976). For nonconvex, nonsmooth the situation is different: descent and boundedness give only that limit points are critical, and the whole sequence may fail to converge even for smooth (Palis–de Melo; Absil, Mahony and Andrews, SIAM J. Optim. 2005).
Attouch and Bolte (Math. Program. 116, 2009, online 2007; author's version hal-00803898) showed that the Łojasiewicz inequality, which holds for real-analytic functions and for continuous subanalytic functions, restores convergence of the whole sequence for the nonsmooth proximal algorithm, together with explicit rates. The argument is Łojasiewicz's original gradient-flow idea transferred to a discrete, nonsmooth setting. It became the template for the later convergence analyses of proximal alternating minimization, forward–backward splitting and PALM under the Kurdyka–Łojasiewicz property, which are used throughout nonconvex optimization, signal processing and machine learning.
Timeline:
Points live in with the Euclidean norm . Let be proper (never , finite somewhere) and lower semicontinuous, with domain .
The limiting subdifferential is the set of limits of Fréchet subgradients along sequences with . A point with is critical, and the set of critical points is .
Fix and step sizes . From an arbitrary the proximal algorithm produces
Any minimizer may be selected. The standing hypotheses are
with the convention (Remark 4). The number in (5) at a point is a Łojasiewicz exponent of that point.
denotes the set of limit points of .
Under (H1), (H2), (H3), if is bounded then
It fixes no constants and holds for every admissible step sequence and every selection in (2).
Theorem 5 (rates): with a Łojasiewicz exponent of , gives finite termination, gives with , and gives . Also: well-posedness of (2) under (H1), Proposition 2 (v), and Remark 2.
The theorem turns subsequential convergence into convergence of the whole sequence, with finite length, for a class that includes semi-algebraic, real-analytic and continuous subanalytic functions. Finite length is the property later used to analyse splitting and alternating schemes under the Kurdyka–Łojasiewicz property, and Theorem 5 is the first rate classification by the Łojasiewicz exponent for a nonsmooth algorithm.
The results are proved on paper. No machine-checked proof of Theorem 4 or Theorem 5 is known to exist. A formalization adds a checked convergence theorem for the nonsmooth proximal algorithm with extended-real-valued , and a reusable set of descent, limit-set and uniformization lemmas that apply to other Łojasiewicz-type analyses.
Descent and give only , which does not imply convergence: the iterates can circle a continuum of critical points with square-summable but non-summable steps, as in the counterexamples for smooth functions. The step that must be supplied is summability of itself. The local inequality (5) holds only near one critical point with its own constants, while the iterates approach a whole compact set , so the local constants first have to be made uniform near that set. The nonsmooth setting adds two difficulties: takes the value , and subgradients are limits of Fréchet subgradients, so their closure properties have to be established for this subdifferential.
is EuclideanSpace ℝ (Fin n); is allowed. is EReal-valued and proper means never and somewhere not . Lower semicontinuity is Mathlib's LowerSemicontinuous. (H2) is ContinuousOn f {x | f x ≠ ⊤}. The limiting subdifferential and are the published platform definitions NonconvexSplitting.Shared.LimitingSubdiff and NonsmoothLojasiewicz.Continuous.crit. Algorithm (2) is a predicate on a sequence (every step is some minimizer), not a proximal map. Limit points are cluster points of the sequence. The power in (5) is lojPow θ s = if s = 0 then 0 else s ^ θ, which implements ; real values of are used only where is finite.
Standing assumptions carried by the goal and Theorem 5: proper and lower semicontinuous, (H1), (H2), (H3), with , a sequence complying with (2), and boundedness of its range. Milestones drop the assumptions their claims do not use. The milestones (8) and (9) also assume for all and use . Both come from the proof's normalization. This reduction is not a hypothesis of Theorem 4: a goal that assumed it, mentioned the constants , or assumed (8) would not be the paper's theorem.
The development needs the closure properties of the limiting subdifferential, the Fermat rule for proximal steps, and compactness and connectedness of limit sets of sequences with vanishing steps. These are reusable for every Łojasiewicz-type convergence proof. Proofs of individual milestones, of the rate lemmas in the proof of Theorem 5, and of the example are welcome.
Augmented Lagrangian methods (the method of multipliers of Hestenes, Powell and Rockafellar) solve a constrained nonlinear program by a sequence of easier subproblems in which some constraints are moved into the objective through a penalty term plus a multiplier estimate. Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); preprint HAL hal-01295437) split the constraints into upper-level constraints, which are penalized, and lower-level constraints, which are kept in every subproblem and may be arbitrary (not only bounds). This is the design of the solver ALGENCAN and of its successors.
A practical method usually cannot guarantee that its iterates approach a feasible point: the problem may be infeasible, and even when it is not, a local method may stall. The question this mission formalizes is what a limit point of the method is when the penalty parameter is or is not driven to infinity. The answer, Theorem 4.1 of the paper, states that infeasible limit points are not arbitrary: they are stationary for the problem of minimizing the upper-level infeasibility over the lower-level set, unless a weak constraint qualification fails there.
The problem is (2.1):
with , , , , , all continuously differentiable. Write and .
The PHR augmented Lagrangian (2.2) with respect to is, for , , ,
Algorithm 3.1 has parameters , , , boxes and , and tolerances with . At outer iteration it finds and lower-level multipliers , satisfying the approximate KKT conditions (3.1)–(3.4) of minimizing over to tolerance ; it chooses new safeguarded multipliers , in the boxes; and it keeps when
and sets otherwise. A run is a sequence produced this way in which the subproblem of Step 2 is always solvable.
A point is a KKT point of a problem with objective , equalities and inequalities if it is feasible and for some and some vanishing on inactive inequalities. The constant positive linear dependence condition (CPLD, Qi and Wei) holds at if every nontrivial null combination of gradients of equalities and active inequalities, with nonnegative coefficients on the inequalities, has gradients that remain linearly dependent at every point near . CPLD is weaker than both LICQ and the Mangasarian–Fromovitz condition.
Let be a run and a limit point of it. If is bounded, then . Otherwise at least one of the following holds:
Theorem 4.1 is the feasibility half of the global convergence theory of the method; Theorem 4.2 of the same paper (a companion mission) shows that feasible limit points satisfying CPLD are KKT points of (2.1). Together they say that the method either finds a stationary point of the original problem or a stationary point of the infeasibility, under a constraint qualification weaker than MFCQ and only at the limit point. Because the lower-level set is arbitrary, the theorem covers the many variants in which bounds, linear constraints or structured sets are kept out of the penalty.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it requires the gradient of the PHR function, a conic Carathéodory theorem with linear independence (Mathlib contains only the convex-hull version), and the subsequence and normalization arguments of the proof. Each is reusable: milestone 5 is used again, unchanged, in the proof of Theorem 4.2.
The bounded case is elementary. The unbounded case is where the work lies. Dividing the approximate stationarity condition by removes the objective and the multiplier estimates, but the lower-level multipliers divided by need not stay bounded, so no limit can be taken directly. The supports of the lower-level combinations must first be reduced to linearly independent ones, uniformly along a subsequence, before the bounded/unbounded dichotomy on the reduced multipliers yields either a KKT point of (4.1) or a nontrivial null combination at whose gradients are independent at points arbitrarily close to . Taking limits of the original multipliers without this reduction does not work.
is EuclideanSpace ℝ (Fin n); constraint maps are families of real functions indexed by Fin m. Continuous differentiability "on a sufficiently large and open domain" is read as on all of . The norm in (3.1) is the Euclidean one; (3.4), Step 4 and the vectors , use the sup norm. The paper's norm is arbitrary and the results do not depend on the choice. A run is a predicate on sequences indexed by : x 0 is the initial point , the outer iterations are , the three subproblem tolerances are kept separate, and is the true gradient of the defined function (2.2). "Limit point" is a cluster point of the sequence; "bounded" is boundedness above of . KKT and CPLD are defined once for arbitrary finite index types; CPLD carries no feasibility clause, and linear independence is that of a family indexed by a disjoint union, so a repeated gradient counts as dependent.
No hypothesis is added to Theorem 4.1 beyond the reading. Junk values cannot trivialize the statement: the run evaluates (2.2) and only at ; the gradients are taken of functions; the run is satisfiable; and both alternatives (i) and (ii) can fail at the same point, so the second half of the theorem has content.
Contributions are welcome on every milestone. The gradient computation (4.2) and the conic Carathéodory theorem are self-contained and useful beyond this paper.
Multistage stochastic linear programs model sequential decisions under uncertainty: capacity and reservoir planning, hydro-thermal scheduling, inventory and asset–liability management. When the data process is stagewise independent, the problem decomposes by dynamic programming into one linear program per stage, coupled through expected cost-to-go functions. These functions are convex and piecewise linear, and the stochastic dual dynamic programming (SDDP) method of Pereira and Pinto (1991) approximates them from below by cutting planes. SDDP is the standard solution method in the long-term planning of hydro-dominated power systems, and its convergence theory determines what the bounds it reports actually mean.
Shapiro's paper (Optimization Online 2009/12/2509; European J. Oper. Res. 209(1), 2011, doi:10.1016/j.ejor.2010.08.007) analyses SDDP applied to a sample average approximation (SAA) of the true problem, with all of the data random. Its convergence result, Proposition 3.1, asserts finite convergence with probability one when the forward scenarios are subsampled independently. A related almost-sure finite convergence theorem for a different algorithm (DOASA, with randomness only in the right-hand sides and cut sharing across outcomes) is due to Philpott and Guan (2008); it is posed as a separate mission on this platform and is not restated here.
There are stages. The decision satisfies and, at the first stage, with deterministic data . For the data are replaced by a sample , , each with probability , independently across stages, and the stage- constraint is . The SAA cost-to-go functions are defined backwards from :
A scenario is a choice ; there are of them, each of probability . A policy depends only on the outcomes up to stage ; it is optimal for the SAA problem if it is feasible on every scenario and its expected cost is minimal.
SDDP keeps, for each stage, a finite set of cuts whose maximum lies below . An iteration has a forward step: scenarios are sampled, and along each of them the decisions solve the stage problems with in place of , (3.13)–(3.14). It also has a backward step: from down to , at each trial point the stage- problems with the current cuts are solved for all outcomes, and the cut (3.17) is added, where averages over basic optimal (extreme-point) dual solutions .
Suppose the forward scenarios are drawn independently and uniformly from the SAA scenarios, (A1) holds ((3.13) and (3.14) have finite optimal values for every scenario at every iteration), and the backward steps use basic optimal dual solutions. Then
The goal fixes no iteration count, no rate and no number of forward scenarios .
The result separates SDDP's sampling from its convergence: on a finite scenario tree, independent subsampling of forward paths suffices for the method to stop at an optimal policy, without ever enumerating the tree. It explains why the lower bound eventually equals the SAA optimal value, which is what makes the gap-based stopping rules of the paper (§3, Remarks 4–6) meaningful. The paper's closing remark stresses that without independence of the forward scenarios there is no guarantee of convergence.
The proposition is proved in the paper. No machine-checked proof of it, or of any SDDP convergence theorem, exists to our knowledge. Formalizing it requires a precise account of what the method is: which dual solutions, which forward solutions, which order of updates. Several of these points are left implicit on the page.
Finiteness of the cut universe (milestones 4–5) is a statement about extreme points of dual polyhedra whose dimension grows with the cut sets of the next stage, so it must be organized stage by stage from down. The central difficulty is the last step of the argument. Once the approximations have stopped changing, one must show that the stable cuts are exact where the forward policy goes, so that the forward policy satisfies (3.18). The obvious argument, "if (3.18) fails at the last stage where it fails, the next cut there increases ", does not work as printed: (3.18) holding at later stages does not by itself make the next-stage approximation exact at the trial point. Closing this step is where the conventions on forward solutions and on sampling listed below become essential.
The Lean development is in the namespace ShapiroSDDP.Convergence. Stages are numbered
; the data of stage are stored under index (the coupling matrix is indexed by the
decision it multiplies); V t is , with V t ≡ 0 for . Cost-to-go
values are real infima, used only on reachable decisions. The explicit readings are:
iIndepFun);Optimality of a policy is defined by expected cost, never by (3.18), so that milestone 6 is not definitional. Sampling is stated as i.i.d. uniform draws, not as "every scenario recurs", which is milestone 7. All of depend on the outcome. If some lacks full row rank, no basic dual solution exists and no run exists; a sorry-free witness instance shows that all hypotheses of the goal can hold together.
Useful infrastructure: LP weak and strong duality (LinearOptimization.lp_weak_duality,
LinearOptimization.lp_strong_duality exist on the platform in their own encoding), finiteness of
extreme points of polyhedra, attainment for polyhedral objectives, and the second Borel–Cantelli
lemma (ProbabilityTheory.measure_limsup_eq_one). Proofs of any milestone, and reusable lemmas on
LPs with cut epigraphs, are welcome.
In shop scheduling, jobs consist of chains of operations, each to be processed on a prescribed machine, and the goal is to minimize the makespan, the time at which the last operation finishes. Almost every approximation algorithm for job shops, acyclic job shops and flow shops is analysed against one quantity: the trivial lower bound , where the congestion is the largest total processing time requested on one machine and the dilation is the largest total processing time of one job. Any schedule has makespan at least .
How weak can this bound be? Leighton, Maggs and Rao (1994) showed that for acyclic job shops with unit-length operations the optimum is . For operations of arbitrary length, Feige and Scheideler (2002) proved an upper bound of for acyclic job shops, and gave acyclic job shop instances whose optimum is . Flow shops, in which every job visits every machine in one common order, are much more structured, and no flow shop instance with optimum was known. Feige and Scheideler asked whether flow shops admit a significantly better upper bound. Mastrolilli and Svensson (J. ACM 2011, Theorem 1.1) answered this negatively by constructing flow shops whose optimal makespan is a factor above .
Timeline:
A job shop instance has machines and jobs; job is a sequence of operations , operation needs time units without interruption on machine . A feasible schedule assigns a start time to every operation so that each operation starts after the previous operation of its job has completed, and no two operations on one machine overlap. A zero-length operation therefore still occupies an instant on its machine: it cannot be performed strictly inside another operation there. The makespan is the largest completion time.
The instance , for natural numbers :
Operations of positive length are long-operations, the others short-operations. For a schedule, the -th long-operation of a job of frequency is good if the delay from its end to the start of the next long-operation of is at most ; the last long-operation of a job is never good. is the set of first halves of the good long-operations on machine , and the total time they cover.
For all natural numbers and : every job of has length , every machine has load (so ), and every feasible schedule satisfies
With this gives the paper's statement, an optimal makespan of .
The theorem shows that the lower bound , against which all known flow shop algorithms are analysed, can be off by a factor growing with . Any flow shop algorithm with guarantee relative to the optimum must therefore use a stronger lower bound than . The same frequency construction is the gap gadget behind the paper's inapproximability results for generalized flow shops and job shops (Theorems 1.2 and 1.3).
The result has been proved since 2011; as far as is known it has no machine-checked proof. The mission produces a formal model of the instance , a formal proof of the explicit bound for every , , and reusable statements about delays and first-half intervals in the published job shop model JobShopLTAS.Core.Instance.
The bound must hold for every feasible schedule, with no structural restriction such as a permutation or non-delay schedule. The obvious approach, comparing each machine's load with the makespan, only gives , since every machine carries exactly . The gain comes from interaction between machines of different frequencies in one group: a high-frequency job running in parallel with a low-frequency long-operation is held back by its zero-length operation on the low-frequency machine. Turning this into a quantitative bound requires controlling, for every job at once, how long it waits between consecutive long-operations, and that waiting is only bounded when the makespan is already small. Encoding the index arithmetic of (groups, frequencies, copies, positions of the long-operations) and the zero-length operations faithfully is a substantial part of the work.
JobShopLTAS.Core.Instance: machines Fin m, jobs Fin n, real processing times and start times, IsFeasibleSchedule Finset.univ s (nonnegative starts, chain precedence, disjunctive machine constraint s o + p o ≤ s o' ∨ s o' + p o' ≤ s o) and makespan Finset.univ s. Under that constraint a zero-length operation cannot sit strictly inside another operation on its machine, which the paper's argument needs.Welcome contributions: proofs of the counting facts about the encoding, of the milestones, and general lemmas about feasible schedules in JobShopLTAS.Core.Instance (completion time of a job bounds its delays; disjoint intervals in have total length at most ).
A sparse graph that approximates a dense one, in the sense that both have nearly the same Laplacian quadratic form, can stand in for it in every algorithm that only reads cuts or solves Laplacian linear systems. Spielman and Teng introduced such spectral sparsifiers and built them in nearly linear time; the construction is the sparsification step of their nearly-linear-time Laplacian solver (arXiv:0808.4134, SIAM J. Comput. 40(4), 2011).
Sampling edges at random works well only inside a graph of high conductance, where no vertex set is separated from the rest by few edges. A general graph is therefore first cut into pieces of high conductance, with few edges running between the pieces. Section 7 of the paper proves that such a decomposition always exists. A similar result was obtained independently by Trevisan (2005). The decomposition theorem, together with the sampling theorem of §6, already shows that every graph has a spectral sparsifier with edges; the algorithmic decomposition of §8, which the fast algorithm uses, is an approximate version of it, and its analysis rests on the same certificate lemma.
Let be a finite simple undirected graph with edges, and write for the degree of vertex . For disjoint , is the set of edges with one end in and one in . The volume of is ; in particular .
For a vertex set and , the conductance of inside is
and the conductance of is over proper subsets, with when . Volumes are always measured with the degrees of , never with the degrees inside the induced subgraph ; consequently is at most the usual conductance of , and lower bounds on transfer to it.
A decomposition of is a partition of . It is a -decomposition if for all , and its boundary is the set of edges between different parts,
In Lean: vol G S, cutEdges G S T , condRel G B S , cond G B , and decompBoundary G P for a Finpartition P of the vertex set, all in the namespace SpectralSparsify.Decomp.
Every graph without isolated vertices has a decomposition with
The constants are the paper's. Both conditions must hold for one and the same partition.
The theorem says that every graph is, after removing at most half of its edges, a disjoint union of pieces of conductance . By Cheeger's inequality each piece then has normalized spectral gap , which is the hypothesis under which the random sampling of §6 produces a spectral approximation; applying the theorem recursively to the removed edges gives the existence of spectral sparsifiers with edges (§7.2). Decompositions of this kind, now called expander decompositions, have become a standard tool in graph algorithms.
The theorem is proved in the paper; to the knowledge of this mission it has no machine-checked proof. What the mission produces is a formal proof of the existence statement with the paper's explicit constant, a formal Lemma 7.2 (the certificate lemma that also drives the approximate version, Theorem 8.1), and reusable Lean definitions of volume, relative conductance and decomposition boundary for finite simple graphs.
The obvious argument, cutting along any sparse set until no sparse set is left, controls the conductance of the final parts but not the number of edges cut: a long sequence of small sparse cuts can remove far more than half of the edges. The difficulty is to show that one well-chosen cut leaves a remainder whose conductance is certified without further search, which is the content of Lemma 7.2. Its hypothesis is a maximality condition over all subsets of , and its conclusion concerns all subsets of , a different set measured with the same ambient degrees, so the two cannot be compared directly. The existence statement then needs a well-founded description of the recursion, a bound on its depth, and an accounting of the cut edges level by level, all against the explicit constant .
Graphs are SimpleGraph V on a finite vertex type with decidable adjacency; vertex sets are Finset V; volumes, conductances and the bound on are real numbers; decompositions are Finpartition (Finset.univ : Finset V); is Real.logb (4/3).
Hypotheses made explicit:
∀ v, 0 < G.degree v) in Theorem 7.1, Lemma 7.2 and the milestones that divide by a volume. The paper leaves it implicit: is for sets of isolated vertices, and with Lean's Lemma 7.2 would be false (one edge plus two isolated vertices is a counterexample). Under the hypothesis forces , and Theorem 7.1 is then trivially true.Conventions: is the minimum over proper subsets, the empty set contributing ; for ; counts ordered adjacent pairs in , which is the edge count for disjoint sets. Neither conclusion of Theorem 7.1 may be dropped: the partition into singletons satisfies the conductance bound and the partition into one part satisfies the boundary bound, so a formalization keeping only one conclusion is trivial.
Not formalized: idealDecomp as an object (step 2 involves a choice, so it is a relation rather than a function; the goal is the existence statement), its termination and depth bound as separate items, the λ-spectral decomposition remark via Cheeger's inequality, the existence sketch for sparsifiers in §7.2, and the algorithmic analogue of §8. Contributions welcome: proofs of the milestones, a formal recursion for idealDecomp, and lemmas on volume and edge-boundary arithmetic that other graph-partitioning missions can reuse.
Many graph algorithms run in time proportional to the number of edges. A sparsifier of a weighted graph is a graph on the same vertices with far fewer edges that approximates for the purpose at hand, so that the algorithm can be run on instead. Benczúr and Karger (1996) showed that every graph has a sparsifier with edges preserving the weight of every cut up to a factor . Spielman and Teng (2004) introduced the stronger spectral notion, in which the Laplacian quadratic form is preserved for every real vector, not only for cut indicators; their sparsifiers had edges for a large constant and were the first step of their nearly-linear-time solvers for symmetric diagonally dominant linear systems.
Spielman and Srivastava (arXiv:0803.0929, STOC 2008, SIAM J. Comput. 2011) proved that independent sampling of edges, each edge with probability proportional to its weight times its effective resistance, yields a spectral sparsifier. The result improved both earlier bounds, replaced a recursive partitioning construction by a one-line sampling rule, and made effective resistance a standard tool in graph algorithms. Batson, Spielman and Srivastava (arXiv:0808.0163) later obtained edges deterministically, by a slower method built on the same matrix .
Let be a connected weighted undirected graph with vertices, edges and weights . Orient every edge arbitrarily, so that it has a head and a tail (distinct vertices).
There are an absolute constant and a threshold such that, for every , every connected weighted graph on vertices and every , with , with probability at least
The constant is left unfixed; the statement asserts the shape with the paper's explicit dependence on .
Theorem 1 says that every weighted graph is spectrally approximated by a reweighted subgraph with edges. A spectral approximation preserves cut weights, the eigenvalues of the Laplacian up to , effective resistances, and the condition number of as a preconditioner, so any algorithm whose output depends on these quantities can run on . Combined with fast approximate computation of effective resistances (the second mission of this series), it gives a nearly-linear-time construction, and it is the sampling step used in Laplacian solvers, in sparsification of sums of rank-one matrices, and in leverage-score sampling for regression, where is exactly the statistical leverage of a row.
The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission formalizes the statement and the paper's proof structure: the linear algebra of (Lemma 3), the deterministic reduction from quadratic forms to a spectral-norm bound (Lemma 4), and the matrix concentration inequality (Lemma 5), which is the substantive analytic input and is itself a reusable result about sums of independent rank-one matrices.
The deterministic part is linear algebra over the pseudoinverse. The obstacle is concentration: the expected Laplacian of equals , but bounding the deviation uniformly over all is a statement about the spectral norm of a random matrix, and a union bound over a net of directions costs a factor of in the sample count rather than . Scalar Chernoff bounds per cut, which suffice for cut sparsifiers, do not give the spectral statement. Lemma 5 is the matrix inequality that removes this loss, and no inequality of this kind (a concentration bound for the spectral norm of a sum of independent random matrices) is in Mathlib.
All declarations sit in the namespace EffResSparsify.Sampling.
WGraph V E with orientation maps head, tail : E → V, weights w : E → ℝ, and the fields head e ≠ tail e (no loops) and 0 < w e. Parallel edges are allowed; nothing in §3 uses simplicity. Connectivity is a separate hypothesis on the underlying simple graph and includes . In Theorem 1 the vertex type is Fin n; the edge type is an arbitrary finite type.HarmonicGames.Decomposition.pinv of on Euclidean ; it equals the spectral formula above and is the gauge-fixed inverse, never "some solution of ".Matrix.Norms.L2Operator); vector norms in Lemma 5 are Euclidean; is natural (the base is absorbed into ).Reusable beyond this mission: the weighted Laplacian with its pseudoinverse and effective resistances, and Lemma 5, which applies to any sampling scheme for sums of rank-one matrices (leverage-score sampling, column subset selection). Contributions toward a matrix Chernoff or Rudelson-type inequality in Mathlib are welcome.
The effective resistance between two vertices of a weighted graph is the voltage difference that appears between them when the graph is viewed as an electrical network, edge weights being conductances, and one unit of current is injected at one vertex and extracted at the other. Effective resistances drive the spectral sparsification algorithm of Spielman and Srivastava (arXiv:0803.0929): sampling each edge with probability proportional to its weight times its effective resistance yields a sparse graph whose Laplacian approximates the original one. They are also used as a distance on graphs in the analysis of social and small-world networks, where they reflect how many short paths connect two vertices.
Computing every effective resistance exactly requires the pseudoinverse of the Laplacian, which costs far more than the size of the graph. Section 4 of the paper shows that all of them can be approximated in nearly linear time: a random projection compresses the relevant vectors to dimensions, and the projected vectors are obtained from calls to a fast approximate Laplacian solver (Spielman–Teng). This mission formalizes the deterministic statement that makes this procedure correct, Lemma 9: approximate solves, at a stated accuracy, do not destroy the approximation that the random projection provides.
Let be a connected, simple, weighted undirected graph with vertices, edge set and edge weights . Orient every edge arbitrarily, so that it has a head and a tail. The signed incidence matrix has if is the head of , if is its tail, and otherwise. With the diagonal matrix of weights, the Laplacian is , a symmetric positive semidefinite matrix whose kernel is spanned by the all-ones vector when is connected. Its Moore–Penrose pseudoinverse is , where are orthonormal eigenvectors of with nonzero eigenvalues .
For a vertex let be its indicator vector. The effective resistance between and is
and for an edge with endpoints . The -norm of is . Let and be the smallest and largest edge weights.
A resistance sketch is a matrix (columns indexed by ) with
where is the Euclidean norm. In the paper, for a random matrix with , and the Johnson–Lindenstrauss lemma makes it a sketch with high probability. Write and for the -th rows of and of an approximation , as vectors in .
Let . If is a resistance sketch, if every row satisfies
and if
then for every pair
The lemma is stated for arbitrary , and : nothing about the random projection or the solver enters beyond (4) and the sketch property.
Lemma 9 is the correctness half of the paper's Theorem 2: together with a Johnson–Lindenstrauss lemma and the Spielman–Teng solver it yields a data structure, built in time, that returns any effective resistance to within a factor in time. This in turn makes the effective-resistance sampling of the paper's Theorem 1 run in nearly linear time, and the same sketch-and-solve pattern has been reused in later work on Laplacian solvers, graph sparsification and electrical-flow algorithms.
The result is proved in the paper. Formalizing it produces machine-checked statements of three facts that recur throughout spectral graph theory: the trace identity (Foster's theorem in its weighted form), the lower bound on effective resistances by comparison with the complete graph, and the stability of a resistance sketch under relative -norm errors. Neither Mathlib nor this platform states any of them for the linear-algebraic definition of effective resistance used here.
The hypothesis (4) controls the error row by row, in the -norm on , while the conclusion concerns the columns of applied to , in the Euclidean norm on , and it is a relative bound for every pair at once. A relative bound cannot hold unless is bounded below uniformly over all pairs of distinct vertices, which is where the factors , and of (5) come from. Such a lower bound is false for multigraphs, whose parallel edges can make arbitrarily small, and the relation between the -norm of a row and the Euclidean norms of the columns involves every edge of the graph, not only a path between and .
Proposition 10 is classically derived from Rayleigh's monotonicity law. Its standard formal statement on this platform concerns the probabilistic definition of effective resistance through hitting probabilities of a random walk, which is a different definition from ; no theorem relating the two is available.
The graph is a structure WGraph V E over finite types (vertices, Fintype.card V) and (edges), with head, tail : E → V, head e ≠ tail e, weights w : E → ℝ with 0 < w e. Connectivity is that of the underlying simple graph (Mathlib's SimpleGraph.Connected, which includes ); simplicity means that no two edges join the same unordered pair. Matrices are Mathlib matrices indexed by and . is the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of on the Euclidean space , converted back to a matrix; for symmetric this is the spectral pseudoinverse of §2.2. is the sum of squares of the coordinates, not Lean's sup norm. is the real number .
Choices committed to, relative to the page:
A trivializing formalization is ruled out: the goal does not assume the intermediate inequality of the proof, nor a stronger condition on than (5); its hypotheses are satisfiable (for example with and ), and its conclusion is not vacuous for .
Infrastructure that a complete development needs, and that is reusable beyond this mission: the identity and as the projection onto for a connected Laplacian; the trace identity; Loewner-order monotonicity of in the edge weights; and the effective resistances of the complete graph. Contributions of any of these as separate lemmas are welcome. The random projection (Johnson–Lindenstrauss) and the solver's running time are outside this mission.
Markov decision processes model sequential decisions under uncertainty, and their optimal policies are computed from transition probabilities that in practice are estimated from data. Optimal policies can be sensitive to estimation error in those probabilities. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. Garud Iyengar's Robust dynamic programming (CORC Tech Report TR-2002-07, 2002, rev. 2004; Mathematics of Operations Research 30(2), 2005) set up this theory for countable state spaces and history-dependent policies. It isolated the Rectangularity assumption under which the robust problem keeps a Bellman equation. In the same period, Nilim and El Ghaoui studied robust control of Markov decision processes with finite state spaces.
Timeline:
A discounted ambiguous Markov decision process has a countable state set , for each state a nonempty set of admissible actions, for each admissible pair a nonempty set of probability measures on (the ambiguity set), a bounded reward and a discount factor . Decisions are made at epochs .
A policy maps each history to a probability measure on . is the set of all such policies. A deterministic Markov policy plays for maps with . A stationary policy uses one such rule at every epoch.
Under Rectangularity, the adversary picks a law separately at every epoch and history, and may pick a different law each time a state–action pair recurs. This is the dynamic model, and the set of path measures it generates is . In the static model the adversary fixes one per pair. The robust value of a policy and the robust value function are
Let be the bounded functions on with . For a set of deterministic Markov rules, the robust Bellman operator is
is the only bounded solution of this equation, and for every some stationary deterministic policy has .
Corollary 2(b) justifies computing the robust value function by solving a state-wise max–min equation. Value iteration, policy iteration and their approximations all rely on that equation. It also shows that a decision maker facing a history-dependent adversary loses at most by committing to a stationary deterministic rule. Corollary 2(a) and Lemma 2 make robust policy evaluation a fixed point problem and a robust optimization problem. Lemma 3 shows that, for stationary policies, the dynamic model costs nothing relative to the static model, in which the true transition law is fixed but unknown.
The results are proved on paper. The page proves Theorem 4 only by citation to Puterman's non-robust arguments. No machine-checked proof of any of them is known. The platform has finite-state analogues posed by the Nilim–El Ghaoui and Satia–Lave missions, which compare only stationary or Markov controllers. This mission poses the countable, history-dependent version, and proving it would establish them in this generality.
The contraction property is a state-by-state -argument. The hard step is to identify the fixed point with the value of the game against all history-dependent randomized policies. The adversary's choices at different epochs interact only through Rectangularity, so splitting the infimum over path measures into a first-step infimum and a continuation infimum must be justified for an infinite horizon, uncountably many adversary strategies and no attainment of the infima. The ambiguity sets need not be convex or closed. The naive route, "take the minimizing law at each state", is unavailable, and every bound must be carried with an slack. Truncating the infinite sum needs the uniform reward bound. Theorem 4 needs a separate argument that randomization and history dependence do not help the decision maker against the dynamic adversary.
States and actions are countable Lean types; and are sets, assumed nonempty, with no convexity or closedness. Laws are PMFs and as a tsum. The rewards satisfy on admissible actions. This is the reading of the page's "", which its bounds require. The discount factor satisfies . Epochs start at , so the first reward is undiscounted.
A policy maps to a PMF supported on . The dynamic adversary maps to a law in . The path law is built by PMF.bind, and the discounted reward is , which converges absolutely. Values are real infima and suprema over nonempty families bounded by , so no junk value arises. is the predicate "bounded", and is a supremum (the page writes max). All uniqueness claims are uniqueness among bounded functions.
is a supremum over all history-dependent randomized policies. Defining it over deterministic Markov or stationary policies would make Theorem 4 trivial and weaken the goal, so it is ruled out. The adversary in is the dynamic one; the static adversary appears only in Lemma 3.
The mission deviates from the page in three places:
Only the first claim of Lemma 1 is posed. Its second claim, that an -greedy rule is -optimal, is false as printed.
A complete development needs a general toolkit that is reusable beyond this mission: path laws of countable controlled processes with history-dependent policies, a uniform -optimal selection argument for real infima over arbitrary sets, and the Banach fixed point theorem on bounded functions (Mathlib's ContractingWith). Proofs of individual milestones are welcome in any order. Theorem 5(a) is the natural entry point.
Many classical search algorithms are random walks: a Markov chain on a finite state space is run until it hits a marked state. Szegedy (2004) attached to every such chain a unitary quantum walk , and Magniez, Nayak, Roland and Santha (SIAM J. Comput. 2011, arXiv:quant-ph/0608026) used it to search quadratically faster than the classical walk for every reversible ergodic chain. The search runs Grover-style rotations, and each rotation needs the reflection about the stationary state . Preparing exactly can cost far more than one step of the walk, so the paper builds an approximate reflection from the walk alone, by phase estimation. Theorem 6 of the paper is the guarantee for that circuit, and this mission formalizes it.
Timeline:
is a finite set of size . A Markov chain is a row-stochastic matrix . It is ergodic if some power of has all entries positive. A stationary distribution satisfies , and . The time-reversed chain is defined by , and is reversible if .
The space is with basis . Put and , and
For a subspace , , where is the orthogonal projector onto . The quantum walk is , and the stationary state is .
The discriminant matrix is . Its singular values lie in . The phase gap is , where is the smallest angle in such that is a singular value of .
The phase-estimation circuit acts on . It is
where is the Walsh–Hadamard matrix and is the -point Fourier transform.
The circuit uses and acts on . It is built in three steps:
For ergodic and reversible on states, and every integer :
The milestones follow the order in which the paper's proof uses them:
Theorem 6 replaces the reflection about with a circuit that only calls the walk. Its cost scales as rather than as the cost of preparing . Combined with , where is the eigenvalue gap, this gives the search cost of Theorem 7, up to logarithmic factors. The same approximate-reflection device recurs in later quantum-walk and amplitude-amplification algorithms.
The results are proved in the paper, which takes Theorem 4 from Szegedy and Theorem 5 from Cleve et al. As far as the platform index shows, none of Theorems 4, 5 or 6 has a machine-checked proof. The mission produces three reusable components: a Lean definition of the Szegedy walk and of the phase-estimation circuit, a formal Jordan-type spectral theorem for products of two reflections, and the analysis of phase estimation on an eigenvector.
Most of the work is linear algebra. The proof of Theorem 6 has a short outline: expand in eigenvectors of , apply Theorem 5 to each, and bound each amplitude by . Three steps carry the weight:
EuclideanSpace ℂ (X × X), with the first coordinate the first register.Fin (2^s), and registers by Fin k → Fin (2^s); the all-zeros state is the zero index.Submodule.reflection.Matrix.IsPrimitive.LinearMap.singularValues.Real.logb 2 and the ceiling is Nat.ceil.Deviations from the page.
Only exact statements are formalized. The cost halves (gate counts, calls to -, "", the qubit count, uniformity) are out of scope.
The circuit is the explicit composition above, built from . It is neither "some circuit with properties 2–3" nor anything defined through the projector onto , either of which would make the goal a tautology.
Contributions welcome: proofs of the milestones, Jordan's lemma for two subspaces as a standalone result, and the bound of §3.3.
In an online linear decision problem a decision maker chooses, on each period , a decision from a set , and only then learns a state vector and pays the cost . The online shortest path problem, the experts problem, online binary search trees and list update are all of this form. Kalai and Vempala showed that a single offline optimisation oracle is enough to compete with the best fixed decision in hindsight: Follow the Perturbed Leader plays the leader of a randomly perturbed history (Kalai & Vempala 2005; the idea goes back to Hannan 1957).
Each period of FPL calls the oracle once and may change the decision. When an oracle call is expensive, or when switching decisions carries a cost (rotating a search tree, re-routing traffic), this is wasteful. The same paper introduces Follow the Lazy Leader: versions FLL and FLL* of FPL and FPL* that correlate the perturbations across periods so that the decision rarely changes, while each single period is distributed exactly as before. Lemma 1.2 of the paper is the statement that this works, and it is the result of this mission.
Vectors are elements of ; , and with .
The four algorithms, period :
For every period :
The first line is the FLL half, the second the FLL* half. The constant is the paper's.
Lemma 1.2 transfers every guarantee proved for FPL and FPL* to FLL and FLL*: Theorem 1.1 of the paper bounds expected costs period by period, so equal per-period expectations give the same additive bound and the same multiplicative bound for the lazy algorithms. In addition, the expected number of oracle calls and decision changes over periods is at most , which is at the usual tuning . The paper uses this for online binary search trees with few rotations.
The result is proved in the paper. As far as is known there is no machine-checked proof of it. This mission produces a Lean statement of all four claims and of the six steps of the proof, against explicit Lean definitions of the grid point, the FLL* step and the law sequence . The uniformity of a random-grid point and the invariance of a Laplace law under a Metropolis-type step are reusable facts beyond online learning.
The FLL half asks for the exact law of the grid point , a piecewise translation of whose pieces depend on . The page settles it in one line ("by symmetry"); in Lean it is an equality of push-forward measures, and the obvious attempt, a single change of variables , fails because the shift is different on different pieces of the cube.
The FLL* half is a statement about measures on given as a mixture of point masses. The page argues with densities, pointwise in ; the formal statement is an equality of measures, with the update written as a Measure.bind against a kernel whose two branches move mass in different directions. The density computation of display (8) does not by itself give this equality.
Fin n → ℝ, is dotProduct, is written out as ∑ i, |x i|. States are indexed from 1; s 0 is unused.prefixSum and is perturbLaw n ε from the published definition OracleRO.ApproxFPL.FPL. The oracle is the predicate IsArgminOracle Dset M, and every statement holds for every such .laplaceLaw n ε carries its normalising constant , so it is a probability measure for .fllGridPoint ε x p is the explicit formula . It is the unique grid point in the half-open cube for , and it is measurable. The half-open and closed cubes differ by a null set, and the closed-cube law is used throughout.fllStarJoint ε v ν of , built with Measure.bind and Measure.dirac. The acceptance probability is . The law fllStarLaw ε s t is the recursion started at , not itself.The formalization rules out the following trivializations:
Classical.choose;Welcome contributions:
Measure.bind lemmas for finite mixtures of Dirac kernels;Grover's algorithm finds a marked element among with queries by alternating two reflections: one about the initial state and one that flips the sign of marked states. In quantum-walk search, the initial state encodes the stationary distribution of a Markov chain, and the reflection about is too expensive to implement exactly. Magniez, Nayak, Roland and Santha (arXiv:quant-ph/0608026, SIAM J. Comput. 2011) obtain the reflection approximately, by phase estimation on the quantum walk, and need a search procedure that tolerates the approximation error without paying extra cost to reduce it. Their Section 4 supplies one: a variant of the recursive amplitude amplification (RAA) of Høyer, Mosca and de Wolf (ICALP 2003) in which the reflection about is replaced, at recursion level , by an approximate circuit of precision . The two lemmas of that section, stated "in full generality for potential further applications" (p. 11), are the exact engine of the paper's headline Theorem 3 (search with cost ).
Timeline: Grover (1996) gives quadratic speedup for unstructured search; Brassard, Høyer, Mosca and Tapp (2002) generalize it to amplitude amplification; Høyer, Mosca and de Wolf (2003) introduce RAA to tolerate a bounded-error marking reflection; Szegedy (2004) defines quantum walks for arbitrary reversible chains with detection guarantees; Magniez, Nayak, Roland and Santha (STOC 2007, SIAM 2011) adapt RAA to an approximate initial-state reflection and obtain search, not only detection, for every reversible ergodic chain.
Let be a finite set and a set of marked elements. The state space is . The initial state is any unit vector (Lemmas 1 and 2 never use its quantum-walk form), and the marked weight is , where projects onto the basis states with .
For each level an extra register (a finite-dimensional space with a basis state ) is given together with a unitary on , playing the role of :
On the marked subspace consists of states whose first register is marked, and .
Approximate RAA is the unitary with and
where multiplies by every basis state in which some register , , is not , and otherwise applies to . Write and .
Tolerant RAA first samples (succeeding with probability ); otherwise, for , it applies to the state left over from the previous failed measurement, with , and measures ; a failure collapses the state to .
Let , let satisfy whenever , and let be the smallest non-negative integer with . The probability that Tolerant RAA ends with a marked element satisfies
With the smallest non-negative integer such that , for every ,
In the order of the proofs: Fact 1 (the error operator kills and has norm on states with clean registers ); the one-level bound ; the two trigonometric inequalities on ; the surrogate bound ; Lemma 1; the three terms of the drift recursion (5); and the accumulated drift .
Lemma 2 turns any family of approximate reflections whose error decays like into a search procedure that succeeds with constant probability, needs only a lower bound on , and costs calls. Combined with the phase-estimation reflection of the paper's Theorem 6 it yields Theorem 3, the general quantum-walk search theorem that has become the standard tool for walk-based algorithms (element distinctness, triangle finding, group commutativity). Nothing in the lemma refers to Markov chains, so it applies to any setting with an approximate reflection about the initial state.
The results are proved in the paper. None of them is machine-checked: the platform holds a formal Grover search with one marked basis state and exact reflections, but no amplitude amplification with approximate or recursive reflections. A formal proof would also settle the steps the paper passes over quickly, notably that the trigonometric inequalities, claimed for angles in , are applied to the actual angles , which may exceed by at the last level.
The ideal analysis (every reflection exact, angle tripled at each level) is a two-dimensional rotation argument. With approximate reflections the state leaves the plane spanned by and , and each level both triples the error already present and injects a new one; the errors stay bounded only because converges and the injection at level is weighted by . Fact 1 is not a restatement of the hypothesis on : it holds only because step 4 flips the phase of states whose earlier registers are dirty, and because never touches . In Lemma 2 the attempts reuse the leftover state, not a fresh , so the state at the decisive attempt has drifted; bounding the drift needs the normalised unmarked parts to move little from level to level, which again depends on the error bounds of Lemma 1.
EuclideanSpace ℂ (X × X × ((j : Fin T) → κ (j+1))); operators are complex matrices. Registers are 0-based in Lean (index is ).Real.arcsin; the interval is closed.Contributions welcome: proofs of the trigonometric milestones and of (pure real analysis), Fact 1 (finite-dimensional linear algebra with a block structure on registers), and the vector inequality that the drift bounds share. The register and controlled-unitary infrastructure is reusable for other recursive quantum algorithms.
An investor who trades continuously in a market driven by Brownian motion, and who may only hold portfolios in a prescribed set, wants to maximize the expected utility of terminal wealth. With power utility , , this is the constant-relative-risk-aversion problem that goes back to Merton (Merton 1971). When there are fewer stocks than sources of noise the market is incomplete, and when portfolio proportions are restricted (no short sales, bounded positions, a fixed allocation) the problem is constrained.
For convex constraints, duality methods settle the problem (Cvitanić–Karatzas 1992; Kramkov–Schachermayer 1999). They do not apply when the constraint set is closed but not convex, as for integer-lot or "all-or-nothing" restrictions. Hu, Imkeller and Müller (2005, arXiv:math/0508448) treat that case by a martingale optimality principle: they build a process that is a supermartingale for every admissible strategy and a martingale for one, and obtain it from a backward stochastic differential equation (BSDE) with a driver that grows quadratically in . The existence theory for such equations is due to Kobylanski (2000).
This mission formalizes the power-utility result, Theorem 14 of the paper. A companion mission treats the exponential-utility result, Theorem 7.
Fix a horizon and a probability space carrying an -dimensional Brownian motion ; is the augmentation of its natural filtration. is the Euclidean norm, and is Lebesgue measure on .
Market. There is a bond with zero interest and stocks with prices . The rates and the volatility are predictable and uniformly bounded, and for constants . The market price of risk is .
Constraints. A closed set of row vectors constrains the proportions of wealth held in the stocks. In the variable the constraint reads . For a closed , , and is the (possibly multi-valued) projection.
Wealth and admissible strategies. From initial capital the wealth (11) is
The admissible class (Definition 13) consists of predictable with for -a.e. and a.s. The value is (12), .
The BSDE. is the class of predictable, -a.e. bounded processes and that of predictable with . The BSDE (15) is
A BMO martingale is one with over stopping times (equation (2)).
(15) has a unique solution , and for
attained by some with
The page prints ; its proof measures utility by , so the value of (12) with carries the factor (see Formalization scope).
The theorem gives the value of a constrained power-utility problem in closed form through one scalar, , of a BSDE, and identifies an optimal strategy as a measurable selection of a projection onto the constraint set. Convexity of the constraint is not needed; when is a convex cone the result recovers the strategy obtained by other methods (Remark 16 of the paper). The same scheme handles exponential and logarithmic utility in the paper's other sections, and the dynamic programming principle of Proposition 15 follows from it.
The result is proved in the paper. As far as the platform's records show, none of it is formalized: there is no quadratic BSDE, no BMO martingale and no continuous-time utility-maximization statement on the platform. A complete formalization would add an existence and uniqueness theory for BSDEs with quadratic growth, the BMO criterion for stochastic exponentials, and a verification theorem for constrained portfolio problems, each reusable well beyond this paper.
The verification argument is short on paper; its inputs are not. Existence for (15) rests on Kobylanski's existence theorem for drivers of quadratic growth, which is not in Mathlib; the Lipschitz theory does not cover a driver growing like . Uniqueness needs a comparison principle for such drivers. Lemma 17 and the martingale property of need the theory of BMO martingales and of their stochastic exponentials, also absent. The comparison milestone concerns processes that are only local supermartingales. A naive attempt that treats as a martingale for every admissible fails: for a general , which is only locally square integrable, it is merely a local supermartingale.
All declarations live in HuImkellerMuller.Power. Time is ℝ≥0; vectors of are EuclideanSpace ℝ (Fin m), with products as inner products; is a Set (Fin d → ℝ). The Brownian motion, the augmented filtration, the measure and the Itô-integral operator I are reused from published definitions (EthierKurtz_IsStandardBrownian, CvitanicKaratzas92_Optimality_Market). The wealth is constructed from I, and ; is computed from and .
Conventions and disclosed readings:
The value is a supremum of lower integrals, never of Bochner integrals: a Bochner expectation of a non-integrable is and would make the supremum meaningless. The goal asserts existence of a solution of (15) and does not take one as a hypothesis, so it cannot hold vacuously.
Contributions welcome: a theory of BSDEs with quadratic growth (Kobylanski), BMO martingales and Kazamaki's criterion, measurable selection of metric projections, and proofs of the deterministic milestone (14) and the growth bound (H1).
Scheduling jobs whose durations are uncertain is the normal situation in project management, manufacturing and computing: a job's processing time becomes known only when the job finishes, but a distribution for it is available in advance. Stochastic machine scheduling models this by random, independent processing times and asks for a scheduling policy, a rule that decides online which jobs to start, using only the information observed so far, that minimizes the expected total weighted completion time . Optimal policies are known only in a few special cases, and they can depend on the full conditional distributions of the remaining processing times, so the research focus has been on simple policies with provable performance guarantees.
Skutella and Uetz (SIAM J. Comput. 34(4), 2005) gave the first constant-factor guarantees for stochastic parallel-machine scheduling with precedence constraints. Their policies are list scheduling policies whose priority list comes from an optimal solution of a linear program built on the load inequalities of Möhring, Schulz and Uetz (J. ACM 46(6), 1999). This mission formalizes their second main result: for in-forest precedence constraints and no release dates, plain Graham list scheduling in LP order is a -approximation.
Timeline.
There are a finite set of jobs, identical parallel machines, and nonnegative weights . Jobs are processed nonpreemptively; each machine handles one job at a time. Precedence constraints form an acyclic digraph : an arc means starts only after completes. The constraints form an in-forest if each job has at most one successor. There are no release dates.
The processing times are independent random variables. A realization is a vector ; a schedule assigns start times , with completion times ; it is feasible if it respects precedence and at most jobs are in process at any time. A policy maps each realization to a feasible schedule, and it is nonanticipatory if what it has started by time depends only on what has been observed by (the processing times of completed jobs and which jobs are still running).
With and a common bound with (i.e. ), define
The LP-relaxation minimizes subject to for all , for arcs , and . A priority list sorts the jobs by nondecreasing ; is the set of jobs up to and including in , and the jobs after .
Graham's list scheduling starts, at every decision time, as many available jobs as possible in the order of . For a schedule, a critical predecessor of is a predecessor that completes last among 's predecessors, at a positive time; following critical predecessors backwards gives the critical chain of , whose total processing time is .
For every feasible nonanticipatory policy ,
The theorem gives a constant performance guarantee for stochastic in-forest scheduling, uniform in the distributions once their coefficients of variation are bounded. For NBUE distributions (exponential, uniform, Erlang, …), where , the guarantee is , compared with for general precedence constraints and release dates with Algorithm CMNS (Table 1, p. 792). The analysis shows that for in-forests, deliberate idle time is unnecessary: Lemma 4.3 replaces it.
The result is proved in the paper, partly by reference: Theorem 3.1 and Lemma 3.3 are cited from Möhring, Schulz and Uetz. To our knowledge none of these results has a machine-checked proof. A complete formalization requires the load inequalities of stochastic scheduling, which are of independent use for every LP-based stochastic scheduling result, and a reusable treatment of list schedules, critical chains and nonanticipatory policies.
Two parts carry the weight. The first is the load inequalities (Theorem 3.1): they hold for nonanticipatory policies only, because a policy's start time of job must be independent of ; turning the informal "dynamic view" of policies into a statement that yields this independence, and then the variance bookkeeping, is the probabilistic core. The second is Lemma 4.3: the naive argument "a waiting job of high priority blocks lower-priority jobs" fails for general precedence constraints, where Graham's algorithm can be arbitrarily bad; the in-forest structure is used through a counting argument at time , in which the critical predecessors of the jobs started at that time must be distinct.
Lean represents jobs by a Fintype V, precedence by a relation A : V → V → Prop with acyclic transitive closure, and in-forests by "at most one outgoing arc". Schedules are start-time vectors in ℝ, with machine capacity by counting jobs in process on half-open intervals. Policies are maps from realizations to start times with an explicit nonanticipation condition. Graham's list scheduling is characterized by rules (feasibility, greedy, list order, decision times); critical chains are taken for every admissible tie-breaking selector. The CV bound includes and . Zero processing times are allowed.
Standing assumptions and disclosed additions: processing times are independent and nonnegative; the comparator policies have integrable completion times; the completion times and critical-chain lengths of Graham's schedule are assumed almost-everywhere measurable (the paper asserts measurability in §5 without proof); "-approximation" is stated against every comparator policy rather than an optimal one.
A trivializing formalization is ruled out: the comparator ranges over every feasible nonanticipatory policy with integrable completion times, is optimal over all load inequalities , and the Graham family must satisfy the rules for every nonnegative realization.
Welcome contributions: the load inequalities, existence and measurability of Graham schedules, and general lemmas on list schedules.
A linear multistage stochastic program chooses decisions over stages while a random vector is revealed one piece at a time; each decision may depend only on what has been observed so far. Such programs model production planning, capacity expansion, hydro scheduling and portfolio problems. Computing their optimal value exactly is intractable in general: Shapiro and Nemirovski argue that even medium-accuracy solutions are out of reach when the number of stages grows (Shapiro–Nemirovski 2005), and already the one-stage problem is #P-hard (Dyer–Stougie 2006, Theorem 3.2, as cited by the paper).
Linear decision rules restrict every decision to be an affine function of the observations. Introduced for robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004) and carried into stochastic programming by Shapiro and Nemirovski and by Chen, Sim, Sun and Zhang (2008), they turn the problem into a finite one whose optimal value is an upper bound. Kuhn, Wiesemann and Georghiou (Optimization Online 2009/02/2218; Math. Program. 130, 2011) apply the same restriction to the dual problem, which yields a lower bound. They show that, for polyhedral supports, both bounds are values of explicit linear programs. This mission formalizes the multistage version of that statement, Theorem 3 of the preprint.
Stages are . The uncertainty is with and ; by convention and . The history at stage is , , and the truncation operator maps to . The law of has support , a nonempty bounded polyhedron spanning , whose first two constraints encode . denotes conditional expectation given , and is the second-order moment matrix.
A stage- decision is a square-integrable Borel function of (written ). The program minimizes
with deterministic matrices , and . The linear conditional mean assumption requires almost surely for some ; it holds, for example, for stagewise independent data.
The primal approximation sets and slacks . The dual approximation keeps general rules but imposes the slack equations only in the weak form . The linear programs (4.2) and (4.6) are written in the matrices , multipliers and slack matrices , with .
Under the standing assumptions, the linear conditional mean assumption, and strict feasibility of ,
as extended-real optimal values. Both equalities are part of the goal.
The theorem makes both linear-decision-rule bounds on a multistage stochastic program computable by linear programming, with size polynomial in , , and and hence typically linear in the number of stages. The gap between the two values measures the suboptimality of the primal linear rule. These results underlie later work on piecewise-linear and lifted decision rules and on multistage robust and distributionally robust optimization.
The preprint omits the proof of Theorem 3 ("it widely parallels the argumentation in Section 2"), so a formal proof has to supply the multistage details: the conditional-expectation bookkeeping, the truncation operators and the transfer of the one-stage cone description to non-anticipative slacks. No part of this paper has been machine-checked before; the companion mission of this series formalizes the one-stage Theorem 1.
The obvious route repeats the one-stage argument stage by stage, and it breaks at the slack constraints of . A slack must be a function of alone, while the one-stage cone characterization of moment vectors concerns functions of the full ; Lemma 3 bridges them only through the linear conditional mean assumption and conditional expectations. A second difficulty is the closure gap between that cone and its polyhedral outer description: the equality of and relies on strict feasibility, and a proof that ignores it is wrong. On the primal side, the passage from almost sure constraints to identities of matrices needs both that every point of is charged by and that spans .
Vectors are functions Fin d → ℝ; stage is the Fin T index and coordinate is index 0. The history dimension is kbar kk t, the truncation is the restriction to the first coordinates, and is also given as a matrix. is Mathlib's condExp with respect to the σ-algebra generated by . " is the support of " means: closed, , and every ball around a point of has positive mass. Decision rules are Borel functions of the history whose composition with is in . Optimal values are infima in EReal ( if infeasible, if unbounded), and "equivalent" means equal optimal values. The matrices are data, with the conditional-mean identity as a hypothesis.
Three conventions are fixed where the page is silent or misprinted. Strict feasibility of , not defined in §4, is the analogue of (2.9) for the standard form (4.1): slacks at least almost surely. The equality constraint of is printed with inside ; the formalization follows (4.7), where the sum covers only . The sign condition in (4.5c) is printed as for a function of , and is read as . The theorem's last sentence (polynomial size, efficient solvability) is informal and not formalized. One hypothesis is added: the goal's second equality assumes or that some row of (the rows of below (2.1b)) is nonzero (the first equality is stated without it). For the support is the single point , and if has no nonzero row beyond (2.1b) the cone of Proposition 3 is all of ; the printed second equality then fails (a strictly feasible one-stage instance has while (4.6) is unbounded below). The added hypothesis excludes exactly this case.
Expectations are Bochner integrals, which vanish on non-integrable functions; under the standing assumptions is bounded almost surely, so all integrands involving square-integrable rules are integrable and no constraint is satisfied vacuously. Matrix.inv returns on singular matrices, but is positive definite under the standing assumptions. The linear conditional mean hypothesis cannot be dropped from Lemmas 2 and 3: without it need not exist.
A complete development needs the support and moment facts of §2 (, almost sure constraints extend to ), Farkas-type duality for the polyhedron , the tower property of conditional expectation, and the cone results of Propositions 3 and 4 of the preprint. These are reusable across the series. Proofs of the milestones, or of these supporting facts as separate lemmas, are welcome.
Quantum walks give quadratic speed-ups for a class of search problems that classical algorithms solve by running a Markov chain until it hits a marked state. Ambainis's element-distinctness algorithm (Ambainis 2007) and Szegedy's quantization of reversible Markov chains (Szegedy 2004) are the two starting points. Magniez, Nayak, Roland and Santha (arXiv:quant-ph/0608026v4, SIAM J. Comput. 2011) combined them into one search algorithm whose cost is governed by the eigenvalue gap of a reversible chain .
For a non-reversible chain the relevant spectral quantity is not the eigenvalue gap of . It is the singular value gap of a related matrix, the discriminant . In §5 the paper observes that its search algorithm and the proof of its main theorem carry over to non-reversible chains once the eigenvalue gap of is replaced by the singular value gap of . Positivity of that gap therefore decides whether the algorithm can be used at all. The paper also notes that irreducibility, and even ergodicity, does not guarantee a positive gap. Its Proposition 3 (p. 17, proved in the appendix on pp. 20–21) gives a simple sufficient condition: every state has a positive probability of staying where it is. This mission formalizes that proposition.
Let be a finite set of states. A Markov chain on is a real matrix with nonnegative entries whose rows sum to one; is the probability of moving from to . The graph underlying has an edge whenever . The chain is irreducible if this graph is strongly connected, so that every state can be reached from every other state.
A stationary distribution of is a vector with
Every irreducible chain has exactly one.
The discriminant of is the matrix
viewed as an operator on with the inner product . Its singular values are the square roots of the eigenvalues of , repeated according to multiplicity. The vector satisfies and , so is always a singular value of . When is reversible, is symmetric and its singular values are the absolute values of the eigenvalues of . In general the two can differ.
If is an irreducible Markov chain on a finite state space with for every , then has exactly one singular value equal to :
Together with the bound below, this says that , i.e. the singular value gap is positive. The goal asserts no explicit lower bound on the gap, so it does not depend on any quantitative estimate.
The result. Proposition 3 is what makes the search algorithm of the paper usable with non-reversible chains. Theorem 8 of the paper bounds the cost of finding a marked element in terms of the singular value gap of , and it needs that gap to be positive. The hypothesis costs little: replacing by for any makes every self-loop positive and keeps the stationary distribution. The proposition also connects to the classical study of non-reversible chains: the squared singular values of are the eigenvalues of the multiplicative reversiblization , which Fill (1991) used to bound convergence to stationarity.
Formalizing it. The proposition and its proof are in the paper and are not in dispute. To our knowledge neither is machine-checked anywhere. The work is a formal proof of the known argument. It exercises Mathlib's recently added singular values of linear maps between finite-dimensional inner product spaces and its theory of irreducible nonnegative matrices, in a setting where the matrix is neither symmetric nor normal.
The obvious route goes through eigenvalues. Irreducibility plus self-loops make aperiodic, so by Perron–Frobenius the eigenvalue of is simple and every other eigenvalue has modulus less than . This does not settle the question. The singular values of a non-normal matrix are not the moduli of its eigenvalues, and the paper points out ergodic chains whose discriminant has zero singular value gap even though their eigenvalue gap is positive. Simplicity of the eigenvalue of therefore says nothing about the multiplicity of the singular value of .
The real content is the equality case of a Cauchy–Schwarz inequality in . It has to be translated into an edge-by-edge relation between the coordinates of the left and right singular vectors, then propagated along directed paths of the chain's graph. The self-loops are what identify the left and right singular vectors with each other. Bookkeeping that is routine on paper costs effort here: passing between the eigenvalue sequence of and the dimension of its -eigenspace, and between paths in Mathlib's quiver of positive entries and chains of equalities.
Fintype with decidable equality. is a real matrix in Matrix.rowStochastic ℝ X, and irreducibility is Mathlib's Matrix.IsIrreducible (nonnegative entries and a strongly connected quiver with an edge iff ). For a row-stochastic matrix this agrees with "every state is reachable from every other state".EuclideanSpace ℂ X. Its singular values are Mathlib's LinearMap.singularValues, a sequence indexed by that is beyond . The goal counts the indices with . The inner product is Mathlib's inner ℂ u (D(P) w). Since the equality-case milestone assumes this equals exactly, no phase ambiguity remains.Scheduling jobs whose processing times are not known in advance is a basic problem of production planning, project management and computing systems. In the stochastic machine scheduling model only the distribution of each processing time is known beforehand; the actual duration of a job is revealed when the job completes. A solution is then not a schedule but a scheduling policy, which decides at every point in time what to start next on the basis of what has been observed so far.
For precedence-constrained problems, constant-factor guarantees for policies were long unavailable. Möhring, Schulz and Uetz (J. ACM 1999) introduced LP relaxations with load inequalities for stochastic scheduling and obtained the first constant-factor policies for independent jobs. In the deterministic setting, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 2001) gave a list scheduling algorithm with deliberate idle times for . Skutella and Uetz (SIAM J. Comput. 2005) combined the two and gave the first constant-factor approximation for stochastic scheduling with precedence constraints and release dates. This mission formalizes that result.
A finite set of jobs is to be scheduled on identical parallel machines, nonpreemptively. Precedence constraints are the arcs of an acyclic digraph: an arc requires to start no earlier than completes, and is a predecessor of if a directed path leads from to . Job has a release date , before which it must not start, and a weight . Following §2 of the paper, release dates are assumed to respect the precedence constraints (Assumption 2.1: whenever is a predecessor of ).
The processing time of job is a random variable with finite mean ; the are stochastically independent. For a realization of the processing times, a feasible schedule assigns start times such that for every arc and at most jobs are in process at any time. A policy maps realizations to feasible schedules; it is nonanticipatory if what it has started by time depends only on what has been observed by . The completion time of under is .
The coefficient of variation is ; the mission assumes for all and some . With , the set function
defines the LP relaxation: minimize subject to for all , for , and .
Algorithm CMNS takes a priority list and a parameter . Whenever a machine is idle and the first job of the residual list (the jobs not yet scheduled) is available, it is scheduled. Otherwise the first available job of the residual list is deliberately delayed; idle machines accumulate deliberate idle time charged to , and once has been charged it is scheduled out of order. The critical chain of a job is traced backwards through critical predecessors (those completing last, after ); its length is .
If is an optimal LP solution, orders the jobs by nondecreasing and , then for every feasible nonanticipatory policy
The theorem gives a policy with a performance guarantee independent of the number of jobs for , using only the expected processing times and a bound on their coefficients of variation. For NBUE distributions () and it yields , matching the deterministic guarantee of Chekuri et al. The analysis separates cleanly into an algorithmic half (Theorem 2.8, valid for arbitrary distributions) and a polyhedral half (load inequalities and Lemma 3.3), both reused for the in-forest results of the same paper and in later work on stochastic scheduling.
The result is proved in the paper; it has no machine-checked proof. Formalizing it produces a precise definition of nonanticipatory policies and of a list scheduling algorithm with deliberate idle times in continuous time, a formal proof of the Möhring–Schulz–Uetz load inequalities, and a verified approximation guarantee for a stochastic scheduling policy.
Lemma 2.6 is the step where the stochastic setting departs from the deterministic one: the set of out-of-order jobs is random and correlated with the schedule, and the identity holds only because the decision to start a job out of order is taken before its processing time is revealed. Making this rigorous requires a formal notion of nonanticipation and an independence argument over a random set. On the algorithmic side, the bookkeeping of deliberate idle time, which accumulates at a rate equal to the number of idle machines, must be made precise at instants where several jobs start, including jobs of length zero. The load inequalities compare every nonanticipatory policy at once and involve second moments of the processing times, so they cannot be checked policy by policy.
Jobs form a finite type; arcs are a relation whose transitive closure is irreflexive; machine capacity is the counting condition "at most jobs in process", with half-open processing intervals. Processing times may be zero. The CV bound is encoded as finite second moments, positive means and .
Algorithm CMNS is characterized by its rules: a decision order nondecreasing in time, the scheduling rule at each decision, and the condition that after the decisions at any time nothing remains to be done. A CMNS policy is a map with this property for every realization. Nonanticipation and measurability of , which the paper asserts without proof (p. 795; §5), are hypotheses. Critical chains use a fixed tie-breaking order.
Standing assumptions and added hypotheses: independence, Assumption 2.1, , and finite means appear in every statement where they are used. is assumed wherever appears (Lemma 2.7, Theorem 2.8), where the page allows with . Lemma 2.6 assumes that is a linear extension, as in the surrounding Lemma 2.5 and Theorem 2.8; with zero processing times it fails otherwise. Comparator policies have integrable completion times and, like , are measurable for the law of , which §5's requirement that every policy be universally measurable implies.
The goal is not trivialized: comparators range over every feasible nonanticipatory policy, not over list policies or the algorithm itself; is optimal over all , not merely feasible; and the expected cost of CMNS is asserted to be finite, so neither side can collapse to a default integral value.
Contributions welcome: proofs of any milestone, in particular Theorem 3.1 and Lemma 3.3, which are reusable for the companion in-forest mission, and a proof that the CMNS rules determine a unique, nonanticipatory, measurable policy.
Linear stochastic programs with recourse model decisions that are taken after an uncertain parameter has been observed: the decision is a decision rule , a function of the data. Computing the optimal value exactly is intractable in general. Dyer and Stougie showed that already two-stage linear stochastic programs are #P-hard (Math. Program. 2006), and the same holds for the one-stage problem below even when is uniform on a cube.
A widely used remedy restricts decision rules to be linear in . Ben-Tal, Goryashko, Guslitzer and Nemirovski introduced this restriction in robust optimization (Math. Program. 2004); Shapiro and Nemirovski (2005) and Chen, Sim, Sun and Zhang (Oper. Res. 2008) carried it into stochastic programming. The restriction yields an upper bound, but on its own it says nothing about how much optimality is lost. Kuhn, Wiesemann and Georghiou (Optimization Online 2009/02/2218; published in Math. Program. 2011) also apply the linear restriction to the dual multipliers. This gives a lower bound, so the gap between the two computable bounds estimates the approximation error. This mission formalizes the paper's model result for the case of fixed recourse and polyhedral support (§2, Theorem 1).
Uncertainty is a probability measure on . The support of is the smallest closed set of probability one. A decision rule is an element of , the Borel measurable, square-integrable functions . Inequalities between vectors and matrices are componentwise.
The data are a fixed recourse matrix , matrices and giving the costs and right-hand sides , and , . The stochastic program is
The standing assumptions of §2 are:
The second-order moment matrix is . is strictly feasible (2.9) if some , and satisfy and almost surely.
The two approximations are as follows.
Under the standing assumptions, (see Formalization scope) and strict feasibility,
where (2.3) and (2.8) are the linear programs
Because , Theorem 1 brackets the value of an intractable stochastic program between two explicit linear programs. The sizes of these programs are polynomial in . They depend on only through its support and its second-order moment matrix. The difference is therefore a computable certificate of how much the linear-decision-rule restriction can lose. Sections 3 and 4 of the paper extend the same scheme to random recourse (semidefinite programs) and to multistage problems; they are the subjects of the companion missions 2 and 3.
The theorem is proved in the paper. As far as a search of the platform shows, none of the statements above has a machine-checked proof. A formal proof would check the measure-theoretic steps that the paper passes over quickly. These are the passage from "almost surely" to "on the support", the density argument behind , and the approximation argument of Proposition 4. A formal proof would also produce reusable results on robust counterparts of polyhedral constraints and on moment cones.
The primal half is robust-optimization duality. Its only delicate point is that almost-sure constraints become constraints on all of , which uses the fact that every point of the support is charged. The dual half is harder. The constraint " has rows in " is a family of moment problems over nonnegative square-integrable densities, and is in general not closed. Replacing it by the polyhedral cone is exact only up to the boundary, and it is strict feasibility that removes the boundary effect. Without strict feasibility the optimal values of (2.6) and (2.8) are only known to bracket each other. The proof of Proposition 3 also needs a description of the closed cone generated by , and this description uses (2.1b).
Vectors in are Fin k → ℝ and matrices are Matrix (Fin m) (Fin k) ℝ. The paper's 1-based indices are 0-based in Lean, so is index 0 and the rows of (2.1b) are rows 0 and 1. The data form a structure Setting, and the standing assumptions form one predicate Standing. The support is encoded by three conditions on : it is closed, , and every ball centred in has positive mass. This is equivalent to "smallest closed set of probability one"; alone would not be enough. Decision rules are measurable functions with MemLp x 2 P. Expectations of vector- and matrix-valued quantities are written entrywise as Bochner integrals. Under the standing assumptions is bounded almost surely, so every integrand involved is integrable and no integral defaults to .
"Equivalent" means equal optimal values. Each optimal value is the infimum of the objective over the feasible set in EReal: if the problem is infeasible and if it is unbounded below. A one-sided inequality between the values, or the bare statement that the problems are linear programs, is not Theorem 1 and does not close the goal. Strict feasibility is a hypothesis of both equalities, as printed. Proposition 1 is stated for any with a nonempty polyhedron, since nonemptiness is the only property of it uses. Proposition 3, Proposition 4 and Theorem 1 carry one hypothesis the paper does not state, (some row of below the first two is nonzero). The printed statements are false without it: for , , , every assumption holds, , so while , and (2.8) loses the sign constraint that (2.6) keeps. Under the standing assumptions the hypothesis is automatic whenever . Theorem 1's closing sentence ("the sizes of these linear programs are polynomial … efficiently solvable") is informal and is not formalized.
A complete development needs strong LP duality or Farkas' lemma for inequality systems, the support of a measure in , density of -densities in nonnegative measures, and basic facts on interiors of polyhedral cones. The Farkas lemma is on the platform (LinearOptimization.farkas_lemma). Proofs of the milestones are welcome independently. Proposition 1 and Proposition 3 are reusable outside this paper.
An investor who trades in a market with fewer stocks than sources of randomness cannot hedge every risk: the market is incomplete. If the investor also faces a liability due at the horizon and has to respect trading constraints (no short sales, limits on positions in certain stocks, a ban on trading some assets altogether), the question of how to trade optimally becomes a constrained stochastic control problem. With exponential utility , its value function gives the investor's utility indifference price of , a standard pricing rule in incomplete markets.
Earlier treatments needed convexity. Cvitanić and Karatzas (Ann. Appl. Probab. 2 (1992)) proved existence and uniqueness for utility maximization in a Brownian filtration with convex constraints, by convex duality. Delbaen, Grandits, Rheinländer, Samperi, Schweizer and Stricker (Math. Finance 12 (2002)) related exponential utility maximization to the martingale measure of minimal relative entropy. El Karoui and Rouge (Math. Finance 10 (2000)) computed the value function and optimal strategy for exponential utility by backward stochastic differential equations (BSDEs), for strategies confined to a convex cone; Sekine (preprint, 2002) obtained the same BSDE from the Cvitanić–Karatzas duality. Hu, Imkeller and Müller (Ann. Appl. Probab. 15 (2005)) gave a direct BSDE solution that works for closed, possibly nonconvex constraint sets, with a bounded liability. The tool is a BSDE whose driver grows quadratically in the control variable, whose solvability rests on Kobylanski's existence theorem for quadratic BSDEs (Ann. Probab. 28 (2000)).
Fix and an -dimensional Brownian motion on a probability space , and let be the -augmentation of the filtration generated by . There are stocks with prices ; the drift and the volatility matrix are predictable and uniformly bounded, and for constants . The market price of risk is .
A strategy is an -valued predictable process , where is the vector of amounts held in the stocks. Its wealth from initial capital is
The constraint is a closed set , not necessarily convex; in terms of it reads . A strategy is admissible, , when , for -a.e. , and is uniformly integrable. The value function is
with and a bounded -measurable liability . For a closed set , and is the set of nearest points.
Let . The BSDE
has a unique solution , the value function is
and there is an optimal strategy with .
In the order of the proof: the bound (4) on and its closedness; the measurable selection Lemma 11 (a), (b); the identity on p. 8 that dictates ; the growth bound (9) and the local Lipschitz estimate of ; existence and uniqueness for (7); the BMO property of Lemma 12; admissibility and optimality of any predictable selection ; and the comparison for every .
The theorem reduces a constrained, nonconvex control problem to a single quadratic BSDE: the value is read off the initial value , and the optimal strategy is a pointwise nearest-point selection from the constraint set. It requires neither convexity nor duality, and it exhibits non-uniqueness of the optimal strategy when has several points. It is the starting point of the quadratic-BSDE approach to utility maximization, indifference pricing and related equilibrium problems.
The result is proved in the paper; nothing in it is open. As far as is known, none of it is formalized: Mathlib has no stochastic integral against Brownian motion, no BSDE theory and no BMO martingales. A complete development would be the first machine-checked solution of a continuous-time portfolio optimization problem by BSDE methods, and its intermediate results (measurable selection of nearest points, the BMO bound for quadratic BSDEs, the verification argument) are reusable.
The deterministic steps (the identity behind the choice of , the growth and Lipschitz bounds) are short. The hard steps are elsewhere. Existence rests on Kobylanski's theorem for BSDEs with quadratic growth, whose proof is a monotone approximation argument with exponential transforms; the Lipschitz theory of Pardoux–Peng does not apply. Uniqueness and the optimality of need the BMO property of and a Girsanov change of measure with a stochastic exponential of a BMO martingale. The selection Lemma 11 (b) cannot use a projection map because is not convex; a measurable choice from a possibly multivalued nearest-point set is required. Finally the verification argument is a localization: is only a local supermartingale, and passing to the limit uses the uniform integrability built into admissibility.
Time is with ; row vectors of are EuclideanSpace ℝ (Fin m) (so is Euclidean) and products such as are inner products. The Brownian motion is the published EthierKurtz.IsStandardBrownian; the filtration and the stochastic integral come from the published module CvitanicKaratzas92_Optimality_Market (IsAugmentedBrownianFiltration, lebP for , and an Itô-integral operator I). Predictability is measurability for Mathlib's Filtration.predictable. The market price of risk and the wealth are computed from the data, not assumed.
Expectations of are minus lower integrals in , and is an extended real: a Bochner expectation would assign the junk value to non-integrable strategies and make them optimal, which is the trivializing formalization to avoid. Existence and uniqueness of the BSDE solution are part of the goal, not hypotheses, and the optimal strategy is a predictable selection of the nearest-point set, not of a choice function.
Disclosed readings: is assumed (otherwise ); constraints and (8) are read -a.e.; ellipticity holds for -a.e. and all ; is a.s. constant and the value identity holds a.s.; uniqueness is in a.s. for each and -a.e.; " given by Lemma 11" is read as any predictable selection; Lemma 11 (b) assumes full rank of . The equivalence of the - and -formulations (Remark 5), the dynamic principle (Proposition 9) and Remarks 2–10 are out of scope.
Needed infrastructure: Itô calculus for continuous semimartingales, stochastic exponentials, BMO martingales and Kazamaki's criterion, Girsanov's theorem, quadratic BSDEs, and measurable selection. Contributions to any of these are welcome; they serve the companion power-utility mission (Theorem 14) as well.
Risk measures quantify the danger of an uncertain cost by a single number. The axiomatic theory of coherent and convex risk measures (Artzner, Delbaen, Eber and Heath, Coherent measures of risk, 1999; Föllmer and Schied, Convex measures of risk and trading constraints, 2002) is static: the risk is evaluated once, with no information beyond what is known at time zero. Multistage stochastic optimization and dynamic risk management need risk evaluated conditionally: at time 1 part of the uncertainty has been resolved, and the risk of a time-2 cost should be a function of what is known at time 1.
Ruszczyński and Shapiro, in Conditional risk mappings (preprint of February 21, 2004; journal version Mathematics of Operations Research 31(3), 2006), extend their earlier static theory (Optimization of convex risk functions, Math. Oper. Res. 31(3), 2006) to this conditional setting. They define conditional risk mappings by three axioms, derive a pointwise conjugate duality, and show that positively homogeneous conditional risk mappings are, under regularity conditions, suprema of countably many conditional expectations. The last result explains the word conditional: the conditional expectation is the prototype, and every positively homogeneous conditional risk mapping is a worst case over a countable family of them.
Let be a set with -algebras ; is the information available when risk is evaluated. Let be a real vector space of -measurable functions , and a subspace of -measurable ones. Let be a real vector space of finite signed measures on with , and pair them by
Both spaces carry locally convex topologies that are compatible with this pairing: the continuous linear functionals on each space are exactly the pairings with elements of the other. Two standing conditions hold throughout: (C) if is not a nonnegative measure, some nonnegative has ; (C′) for every .
A conditional risk mapping is a map with, writing :
Costs are minimised: smaller is better. All inequalities hold at every , not almost surely. is positively homogeneous if for , and lower semicontinuous if each is.
The conjugate is and the risk envelope is . denotes the probability measures in , and those with for all . A map is weakly* -measurable if every is -measurable. For such a selection of , the operator acts on . Assumption (K): is compact, and every such maps into itself with a closed graph. Finally, is the conditional probability of given if each is -measurable and for , ; then .
If is separable, (K) holds and is a positively homogeneous, lower semicontinuous conditional risk mapping, then there are probability measures , , with
each conditional expectation being the integral against a weakly* -measurable conditional probability of .
Corollary 1 (p. 10, singleton envelopes give a conditional expectation) and Proposition 2 (p. 7, for nonnegative -step functions ) are included as further statements.
Theorem 2 identifies the positively homogeneous conditional risk mappings with suprema of conditional expectations. It is the conditional analogue of the representation of a coherent risk measure as a worst-case expectation over a set of probability measures. It shows that the axioms (A1)–(A3), stated at every , are the right abstraction of "conditional": nothing beyond conditional expectations and a supremum is needed to generate them. Theorem 1, the pointwise duality on which it rests, is what makes conditional risk mappings usable in multistage problems. Its envelope form (3.8) is what the paper's composition results and dynamic programming equations in §5–§7 manipulate.
The results are proved in the paper, partly by reference: the duality of Theorem 1 by applying the authors' earlier unconditional theorem "verbatim" at each , Lemma 1 through a measurable-selection theorem, and Theorem 2 through Kakutani's fixed-point theorem. None of them is formalized. A formalization would check these deferred steps. In particular the passage, in the proof of Lemma 1, from a dense subset of to all of uses only lower semicontinuity of , and whether that suffices in every separable paired space is open to scrutiny.
Theorem 1 needs the Fenchel–Moreau theorem in a general locally convex space, paired through integrals against signed measures. Mathlib's convex duality is mostly finite-dimensional or normed, and the extended-real bookkeeping of conjugates is delicate. The main obstacle is Lemma 1. The envelope can be uncountable, and choosing countably many selections that are simultaneously measurable in and exhaust the supremum for every requires a measurable-selection theorem for multifunctions with values in , a space that need not be metrizable. The obvious argument fixes a dense sequence , picks -optimal measures for each , and passes to general by semicontinuity. As written, that last step appears to need more than the proof supplies: approximation of by uniformly over the chosen needs more than lower semicontinuity of . The fixed-point step needs a Kakutani-type theorem in a locally convex space, which Mathlib does not provide.
and are abstract real vector spaces with their own topologies (instances of IsTopologicalAddGroup, ContinuousSMul ℝ, LocallyConvexSpace ℝ), realised by injective linear maps into and into Mathlib's SignedMeasure Ω. They are not subspaces of with the pointwise topology. The ambient MeasurableSpace Ω is ; is a structure field. The pairing is , and integrability against is a field, so no integral takes a junk value. Compatibility includes continuity of both pairings as well as the representation of continuous functionals. The paper's space is not modelled; no statement uses it.
Committed conventions:
EReal;IsLUB), never sSup on ;Two hypotheses are added where the page relies on them implicitly. is nonempty in the goal, Corollary 1 and the fixed-point milestone. for every is assumed in the goal, Proposition 3 and Corollary 1, because the paper derives measurability of from weak* measurability.
The goal cannot be satisfied by an almost-everywhere version of a conditional expectation chosen separately for each , which would allow itself as a "version". Each is integration against one kernel that is a conditional probability of . The goal mentions no selection, fixed point or Kakutani; appears only inside (K).
Contributions are welcome on all of the following:
All three are reusable beyond this mission.
Many sequential decision problems have a combinatorial decision set and a linear cost: choosing a path in a graph whose edge delays change every day, choosing a binary search tree for a stream of requests, or choosing one of experts whose losses are revealed after each round. Classical weighted-majority algorithms keep one weight per decision, which is exponential in the size of a path or tree. Kalai and Vempala (J. Comput. System Sci. 71 (2005)) showed that one call per round to an offline optimiser, applied to the cumulative costs plus a random perturbation, already gives online guarantees comparable to those of the exponential-weights algorithms. The idea goes back to Hannan's perturbed algorithm (1957); the paper's contribution is a short, general analysis in the linear setting.
The paper proves two guarantees for Follow the Perturbed Leader. The additive one (Theorem 1.1(a), a sister mission) bounds the regret by a term growing like . This mission formalizes the multiplicative one, Theorem 1.1(b): for nonnegative costs, a variant with exponentially distributed perturbations pays at most a factor more than the best fixed decision in hindsight, plus a term independent of the horizon. Such "small-loss" bounds matter when the best decision has small total cost, since the regret then scales with that cost rather than with .
Fix a dimension . A decision set and a state set are given; choosing in state costs . In this mission both sets are nonnegative: .
The decision set is accessed only through an argmin oracle with
i.e. with arbitrary tie-breaking. For a state sequence write ; the benchmark is
Two parameters measure the instance: the -diameter for , and the state size for , where .
The algorithm FPL*() acts as follows on each period : draw from the probability law with density
so each coordinate is with standard exponential, and play . Its expected cost against a fixed state sequence is
In Lean these are IsArgminOracle Dset M, laplaceLaw n ε and fplStarExpectedCost M s ε T; is the published OracleRO.ApproxFPL.prefixSum s t.
For nonnegative , and ,
Statement 7 is the bound for an arbitrary parameter; the goal is its evaluation at .
The result is the first multiplicative guarantee for a perturbation algorithm that needs only an offline linear optimiser. With tuned to it gives (p. 294). The paper applies it to online shortest paths, to the tree-update problem (giving the first efficient -competitive algorithm there), and to adaptive Huffman coding. The lazy variant FLL* of the same paper, whose per-period behaviour coincides with FPL*, inherits the bound; that is the third mission of this series.
The theorem is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces a formal proof of Theorem 1.1(b) as printed, together with the reusable ingredients: the multivariate Laplace law with its normalisation, its translation identity (7), and the expected maximum of i.i.d. exponentials. The paper's argument has small gaps that a formalization must close, notably the condition , which (b) omits but its proof uses.
The deterministic part is the be-the-leader argument with a shared perturbation; it is a finite-sum induction. The probabilistic part is where the work is. The obvious approach, bounding the difference between following and being the perturbed leader by the measure of a symmetric difference of translated sets as in the additive case, gives an additive term proportional to and cannot give a multiplicative factor. Instead (6) needs the density ratio of under translation by , which requires a change of variables against a density on , together with the nonnegativity of the integrand; without nonnegativity the inequality fails. The bound on requires the expected maximum of exponentials, which is not in Mathlib, and the identification of the coordinates of as independent scaled Laplace variables, which requires factoring a product density.
Vectors are Fin n → ℝ; is ⬝ᵥ; is written ; is the Lean norm ‖x‖, which on Fin n → ℝ is the sup norm. The decision set is Dset, the diameter Ddiam. States are indexed from ; s 0 is unused. The oracle is a hypothesis IsArgminOracle Dset M on an arbitrary function, so the theorems hold for every tie-breaking rule. The paper's parameters are hypotheses ∀ d d' ∈ Dset, ∑ i, |d i - d' i| ≤ Ddiam and ∀ x ∈ S, ∑ i, |x i| ≤ A. The bound of the paper is not used by part (b) and is omitted.
Hypotheses added to the page, each necessary: measurability of (the expectations presuppose it); ; (the parameter presupposes it); in the goal (used by the proof, p. 303); and only in the statement about a maximum over variables. Two printed slips are corrected, not copied: "exponential distributions with mean " (rate is meant) and "" (an expectation is meant).
Trivializing formalizations are ruled out as follows. The law carries its normalising constant and is shown to be a probability measure in a sorry-free sanity file; it is not the uniform law of FPL. The cost uses , not the be-the-leader . The oracle is not built with Classical.epsilon. All integrands are measurable and bounded (because has finite diameter), so no integral vanishes for lack of integrability; the sanity file checks this on a two-expert instance that satisfies every hypothesis.
A complete development needs Lebesgue change of variables under translation for densities on Fin n → ℝ, Fubini for product densities, the tail-integral formula for expectations, and a union bound. The Laplace law, its translation identity, and the expected maximum of exponentials are reusable beyond this mission; contributions of those as standalone lemmas are welcome.
Stochastic models of covariance matrices need processes that stay in the cone of positive semidefinite matrices. Wishart processes (Bru, 1991) and their extensions underlie multivariate stochastic-volatility and term-structure models in finance (see §1 of Cuchiero et al. for the literature). They are used because their Laplace transforms are explicit: they are exponential-affine in the initial state, and their exponents solve matrix Riccati equations. Cuchiero, Filipović, Mayerhofer and Teichmann (arXiv:0910.0137, Ann. Appl. Probab. 2011) classify all such affine processes on the cone. Theorem 2.4 of that paper says that affine processes on correspond one-to-one to admissible parameter sets. This mission formalizes the converse direction of that correspondence: every admissible parameter set is realized by exactly one affine process.
Timeline:
Let be the real symmetric matrices with , let be the positive semidefinite cone, and let be its interior. Write when . A time-homogeneous, possibly killed Markov process on with transition kernels is affine if it is stochastically continuous and
for functions and .
An admissible parameter set (Definition 2.3) consists of the following:
These data define the operator (2.12),
with . They also define the functions and of (2.16)–(2.17), which drive the generalized Riccati equations , and , .
For every admissible parameter set there is a transition family and there are exponents such that:
Together with the necessity direction (companion mission I in this series), the goal makes admissibility an exact characterization. Every admissible parameter set, including those with jumps of infinite activity and state-dependent killing, defines a well-posed Markov model on . Its Laplace transform is then given by the Riccati flow, which is what makes the model computationally tractable. The intermediate results are reusable on their own:
The theorem is proved in the paper; it is not formalized anywhere. No formal library contains affine processes, generalized Riccati equations on matrix cones, quasi-monotone comparison theorems or martingale problems with jumps. Formalizing them requires all of that infrastructure.
The obvious route is to solve the Riccati equation (2.15) on by Picard iteration and to show invariance of the cone from the inward-pointing condition. That route fails because need not be Lipschitz at : the integral term can have unbounded derivative there (Remark 5.4). Standard invariance theorems therefore do not apply. Instead, quasi-monotonicity keeps the solution away from the boundary.
The obvious construction of the process is also blocked. Stroock's existence and uniqueness theory for martingale problems needs and a uniformly elliptic diffusion part, and neither holds on the cone, where the diffusion degenerates at the boundary. Existence must go through regularized operators with bounded smooth coefficients, then tightness in the Skorokhod space of and a limit. Uniqueness in law comes from the Riccati solutions. The killing terms and are added last.
Conventions committed to in Lean:
Fin d → Fin d → ℝ, with and its norm.∃!.EthierKurtz.HasCadlagPaths).Trivializing formalizations are excluded:
∃! over transition families would be false at negative times, so uniqueness is stated for .Needed infrastructure, reusable beyond this mission: matrix calculus on (square roots, spectral derivatives), comparison theorems for quasi-monotone ODEs, analytic dependence of ODE solutions, tightness in Skorokhod space, and martingale problems on locally compact spaces. Contributions are welcome at any of these levels, as are alternative proofs of the milestones.
The Lasso is the standard estimator for high-dimensional linear regression: from noisy linear measurements of an unknown vector , with possibly much larger than , it minimizes the empirical squared error plus an penalty. Its theoretical guarantees are usually stated as sparsity oracle inequalities: the prediction error of the Lasso is bounded by the best trade-off, over all candidate vectors , between the approximation error of and a term proportional to the number of nonzero components of .
Before this paper, such inequalities for the Lasso carried a leading constant strictly larger than in front of the approximation error. The inequalities of Bunea, Tsybakov and Wegkamp (EJS 2007) and of Bickel, Ritov and Tsybakov (Ann. Statist. 2009, Theorem 6.1) have this form, and the paper notes that sharpness "was not achieved in the previous work on the Lasso" (p. 24). A leading constant larger than means the bound is not informative when the true regression function is far from every sparse linear combination: the inequality then only says that the Lasso is within a constant factor of the best approximation.
Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study nuclear-norm penalized estimation of low-rank matrices in the trace regression model. Their general oracle inequality for a linear subspace of matrices (Theorem 2) has leading constant . Restricted to diagonal matrices with a fixed design, the trace regression model becomes ordinary linear regression and the estimator becomes the Lasso. Section 5.4 of the paper draws the consequence: a sharp (leading constant ) sparsity oracle inequality for the Lasso with Gaussian noise, Theorem 14. This mission formalizes that theorem. The source is the arXiv preprint arXiv:1011.6256v4.
Fix integers and and fixed vectors , the rows of the design matrix . The diagonal elements of the Gram matrix are assumed not larger than . The observations are
with independent random variables, .
For , , and . For , agrees with on and vanishes on . The support of is and the sparsity is its cardinality.
Given , a Lasso estimator is any minimizer
The restricted constant at , with and , is
equal to when the set is empty, and . It is the inverse of a restricted eigenvalue computed at the single support ; the paper obtains it from its matrix quantity for . Finally is the noise vector.
Let with , . With probability at least ,
The event is uniform over all , and the statement holds for every Lasso minimizer.
Theorem 14 gives an oracle inequality for the Lasso whose leading constant is exactly . As a consequence (Corollary 4 of the paper), under the restricted eigenvalue condition RE of Bickel, Ritov and Tsybakov the Lasso's prediction error is at most the best -sparse approximation error plus , which improves the non-sharp inequality of that paper. The bound also shows that the matrix-valued argument of the paper, written for nuclear-norm penalization, specializes cleanly to the vector case; the same argument underlies the matrix completion results of the other missions of this series.
The result is proved in the paper. As far as a search of the platform shows, no formal proof of a sharp oracle inequality for the Lasso exists; the platform has the non-sharp Bickel–Ritov–Tsybakov inequality as an open statement (LassoDantzig.Oracle.theorem_6_1). This mission produces a machine-checked version of the deterministic inequality, of the Gaussian concentration step, and of their combination, with the restricted constant defined exactly as in the paper.
The deterministic part is where the obvious argument fails. The usual Lasso analysis compares the objective at and at a candidate , controls the noise cross term, and rearranges; every version of that argument in the earlier literature loses a multiplicative factor in front of the approximation error , and the factor cannot be pushed to by tuning constants. The sharp bound has to come from a finer use of the optimality of , and the cone constant in is tied to the threshold . Formally, optimality conditions for a nonsmooth convex function on (the subdifferential of ) are infrastructure that has to be in place.
The probabilistic part needs the distribution of a linear combination of independent Gaussians, a Mills-ratio tail bound that is not in Mathlib, and a union bound over coordinates, with the exact constants of the paper.
Vectors are functions Fin p → ℝ, and the design is given by its rows x i : Fin p → ℝ. All statements are in vector form, as the paper itself writes Section 5.4; no matrix library is needed. The Lasso is an argmin predicate, and statements hold for every minimizer; in the goal, is a function of the outcome that is a minimizer at every outcome, and no measurability of is assumed (the bad event is bounded in outer measure).
The restricted constant is formalized through its witnesses: the theorems hold for every in the set whose infimum is . This is equivalent to the infimum, because the bounds are continuous and increasing in . A real-valued infimum would be on an empty set and would make the oracle inequality false, so it is deliberately not used. The infimum over is stated as "for every ", inside the event.
Hypotheses added relative to the page, each disclosed in the item's Formalization Note: (for , and the printed probability divides by zero), , , and measurability of the noise variables. is the paper's standing assumption. The condition is written coordinatewise. In the deterministic milestones the noise is a fixed vector and , which is the paper's for a fixed design and centred noise. No printed slip affects these statements. The constant is kept as printed.
A trivializing formalization would assume the event in the goal, or use a real infimum for ; both are ruled out. Contributions of reusable infrastructure are welcome: the Gaussian tail bound, the law of a weighted sum of independent Gaussians, and the subdifferential of the norm.
Mathematical programs with complementarity constraints (MPCCs, also called MPECs) model optimization problems in which some constraints say that, for every index , at least one of two nonnegative quantities , must vanish. They arise in bilevel optimization, Stackelberg games, the design of equilibria in traffic and electricity markets, and contact problems in mechanics (Luo, Pang, Ralph 1996). Standard nonlinear-programming algorithms do not apply directly: at every feasible point of an MPEC the Mangasarian–Fromovitz constraint qualification fails, so the classical convergence theory of SQP or interior-point methods gives no guarantees.
Relaxation methods replace the MPEC by a sequence of better-behaved nonlinear programs with a parameter , solve each one approximately, and study the limits of the computed points. The question every relaxation method has to answer is what kind of stationary point such limits are, and under which constraint qualification.
Timeline of the result formalized here:
The MPEC (1) on is
with continuously differentiable data. At a feasible the index sets are , , (the biactive set) and .
A feasible is weakly stationary if there are multipliers with , , , such that
with on and on . It is M-stationary if the same multipliers satisfy, for every , either and , or .
The tightened program TNLP replaces the complementarity constraints by on , on and on . CPLD (constant positive linear dependence) for a nonlinear program says: whenever a set of active-constraint gradients is positive-linearly dependent at (a nontrivial vanishing combination with nonnegative coefficients on the inequalities), the same gradients stay linearly dependent on a neighbourhood of . MPEC-CPLD is CPLD for TNLP.
The relaxation of Kadrani et al. is, for ,
A stationary point of is a feasible point with KKT multipliers.
Local minimizers of an MPEC are M-stationary under weak constraint qualifications, whereas strong stationarity needs stronger ones such as MPEC-LICQ; a C-stationary point, the kind of limit the Scholtes relaxation delivers, may still admit first-order descent directions. Theorem 3.5 shows that the Kadrani et al. relaxation reaches M-stationary limits under a constraint qualification that is implied by MPEC-LICQ and MPEC-MFCQ and that holds, for instance, whenever all constraint functions are affine. It separates this scheme from the Scholtes and Steffensen–Ulbrich relaxations in the comparison of the paper.
The theorem is proved in the paper. As far as is known, no part of MPEC theory (constraint qualifications for MPECs, the stationarity hierarchy, relaxation schemes) has a machine-checked proof in Lean or Mathlib. This mission produces a formal account of the stationarity notions of Definition 2.3, of CPLD and MPEC-CPLD, and a complete formal proof of the convergence result, including the standard constraints , that the paper's proof skips for brevity.
The obvious argument passes to the limit in the KKT conditions of . This fails because the multipliers need not be bounded: unlike under MPEC-LICQ or MPEC-MFCQ, MPEC-CPLD does not by itself bound KKT multipliers, and the KKT points of the relaxed programs need not satisfy any constraint qualification themselves (Example 3.6 of the paper). The second difficulty is the biactive set : the product constraint contributes multipliers , to both and , with signs that are not fixed a priori, so a naive limit of the multipliers only gives C-stationarity-type information, or none at all.
is EuclideanSpace ℝ (Fin n) and gradients are Mathlib's gradient; indices are 0-based (Fin m, Fin p, Fin l), and may be zero. Explicit choices fixed by the formalization:
P.IsC1 of every analytic statement.LinearIndependent ℝ of a family indexed by a disjoint union of subtypes, so repeated gradients count as dependent.∀ᶠ y in 𝓝 x*.Two trivializing readings are ruled out. M-stationarity uses one multiplier tuple for both the weak-stationarity equation and the condition on ; separate multipliers would make the sign condition vacuous. MPEC-CPLD demands linear dependence on a whole neighbourhood of , not only at ; the pointwise version is a different hypothesis.
A complete development needs the gradient calculus of products and compositions on EuclideanSpace, a Carathéodory-type lemma (a conic combination can be reduced to one over linearly independent vectors with the same signs), and compactness of bounded sequences in finite dimensions. The Carathéodory lemma and the CPLD/positive-linear-dependence layer are reusable for any constraint-qualification argument in nonlinear programming. Proofs of individual milestones, and of the lemma behind (15), are welcome independently of the goal.
The dial-a-ride problem (DARP) asks for minimum-cost vehicle routes that carry users from individual pick-up points to individual drop-off points, subject to vehicle capacities, time windows, route durations and a bound on each user's ride time. It models door-to-door transport for elderly and disabled people, shared taxis and on-demand microtransit. Cordeau (Oper. Res. 54(3), 2006) gave a mixed-integer formulation of the DARP and the first branch-and-cut algorithm for it, and reported that instances with up to 30 users can be solved to optimality in reasonable time. The algorithm's strength comes from families of valid inequalities: linear constraints satisfied by every feasible route plan that cut off fractional points of the linear relaxation. Several of these families were adapted from the precedence-constrained asymmetric TSP (Balas, Fischetti and Pulleyblank 1995; Grötschel and Padberg 1985) and from the pick-up and delivery problem (Ruland and Rodin 1997); others, notably the generalized order-matching inequalities, were new in this paper.
Let be the number of users. Nodes are with pick-up nodes , drop-off nodes , origin depot and destination depot ; user travels from node to node . An instance fixes, for each node , a load , a service duration and a time window ; for each pair of nodes a travel time ; for each vehicle in a finite set a capacity and a maximal route duration ; and a maximal ride time . The standing conditions are , for , and .
A feasible solution gives each vehicle a route through distinct nodes of , start-of-service times and loads such that every node of is visited by exactly one vehicle, and are on the same route with first, and along each travelled arc, the ride time lies in , the route lasts at most , and the time windows and capacity bounds hold at every visited node. These are the constraints (2)–(14) of the paper's model.
The arc variables are when vehicle travels from to , and . For a node set write , , , , and . An inequality in is valid for the DARP when the aggregated arc variables of every feasible solution satisfy it.
Let be distinct users and let satisfy and . Then every feasible solution satisfies
The handle and the teeth are not required to be disjoint from one another beyond , and is arbitrary.
The mission also states the other propositions of §4: the lifted subtour elimination inequalities (33) and (34) (Propositions 1 and 2), the predecessor inequality (30), the two liftings (36) and (37) of the generalized order constraint (Propositions 3 and 4), the redundancy of the strengthening (40) of (39) under (30) for fractional points (Proposition 6), and the infeasible path inequality (41) under the triangle inequality for travel times (Proposition 7).
Valid inequalities are what make branch-and-cut work: each family is added to the linear relaxation by a separation heuristic, and the paper's computational section reports how the bound improves as families are added. Validity is the one property the algorithm cannot check at run time, since a cut that removes a feasible route plan silently returns a suboptimal answer. Remark 2 of the paper observes that (39) is stronger than the TSP comb inequality on the same sets, and Proposition 6 shows that its natural strengthening adds nothing once the predecessor inequalities (30) are present, which tells an implementer which families to separate.
All propositions are proved in the paper, partly in an appendix; none is formalized. A machine-checked development would give a precise route-based model of the DARP that later DARP and pick-up and delivery papers can reuse, and certified validity of the cut families that branch-and-cut codes for these problems separate.
The proofs are short on paper but argue about the shape of routes: "there exists a path connecting all nodes in ", "this path cannot finish at node because of the precedence constraint". Turning a tight subtour count into a single covering path requires knowing that the arcs of a feasible solution inside a subset of form vertex-disjoint paths, which in turn rests on each node of having exactly one predecessor and one successor and on routes containing no cycles. The arithmetic step from tight teeth to the bound on the handle needs the degree identities for every subset of , and counting the arcs leaving needs the distinctness of the users . Reasoning directly with the linear constraints (2)–(14) does not suffice: those constraints alone do not exclude cycles of zero duration.
Nodes are natural numbers, so and appear literally; , , and are Finset.range (2n+2), Icc 1 n, Icc (n+1) (2n) and Icc 1 (2n). All data and arc variables are real-valued, and every right-hand side is computed in . Feasible solutions are route-based: each vehicle has a duplicate-free list of nodes of , and the constraints of the model are imposed along that list. Read literally, the program (1)–(14) admits closed cycles when around a cycle, on which every proposition fails, and imposes (11)–(13) also at nodes a vehicle does not visit; the route encoding follows the paper's verbal definition of the DARP and its proofs, which reason about routes. Precedence ( before ) is a field of the solution, since with zero travel and service times the nonnegativity of ride times does not order the visits. The routing cost plays no role and is omitted. No positivity is assumed for travel or service times.
Added hypotheses, each necessary: sets in the subtour bound and in (30) are nonempty ( gives ); the users of Proposition 5 are distinct; the generalized order constraint (Propositions 3 and 4) has (for it is false); the ordered sets of Propositions 1 and 2 have nodes, the standing assumption of the paragraph that introduces them; Proposition 7 has and a path through distinct nodes. Proposition 6 is the only statement about fractional points: it assumes nonnegativity, no loops, (2), (3) and (30), and drops the remaining constraints of the relaxation, which makes it stronger.
The inequalities are stated for the arc variables of every feasible solution, not for an arbitrary – vector satisfying a few degree constraints; a statement of the latter kind is a different and false theorem. Useful contributions include the path structure of the arcs of a feasible solution inside a subset of , the degree identities, and the milestone proofs, which are reusable for the other propositions.
Open networks of single-server queues with general (non-exponential) interarrival and service times, generalized Jackson networks (GJNs), model manufacturing lines, communication networks and service systems. Their stationary distributions are almost never available in closed form. The standard engineering approximation replaces the scaled queue-length vector by the stationary distribution of a reflected Brownian motion (RBM) in the orthant, which is the diffusion limit of the network in heavy traffic, when every station is close to full utilisation.
The diffusion limit itself (Reiman, 1984) is a statement about the process on finite time intervals. Using the RBM's stationary law as an approximation of the network's stationary law requires interchanging two limits: time to infinity (steady state) and traffic intensity to one (heavy traffic). For a long time this interchange was assumed rather than proved.
Timeline.
There are stations. Station receives external arrivals with i.i.d. interarrival times of law (rate , or no arrivals at all) and serves jobs first-in-first-out with i.i.d. service times of law (mean , rate ). A job finishing at moves to with probability or leaves. The routing matrix is substochastic with spectral radius below one. Interarrival and service times have uniformly bounded conditional exponential moments of their residual lives (conditions (1)–(2)). The traffic equation gives the effective rates and the traffic intensities .
The queue lengths are not Markov. The state , which adds the elapsed interarrival and service times, is a Markov process on . A law on is stationary if implies for all .
Heavy traffic. Fix a critically loaded network ( for all ) and a vector . The network slows the arrivals of at station by the factor , so that for an explicit (display (17)). Let be any stationary distribution of , and let be the law of under .
The RBM. For a Brownian motion with drift and covariance , the RBM with parameters solves the Skorohod problem , with nondecreasing and increasing only when is on the boundary. Here and is the explicit covariance matrix of Reiman's theorem, built from , , and the squared coefficients of variation , of .
where is the unique stationary distribution of the -RBM. The formal goal asserts three things: a stationary distribution of the RBM exists, it is the only one, and converges weakly to it, for every choice of stationary distributions .
The result. Theorem 8 justifies the use of the RBM's stationary distribution, which is computable or at least numerically tractable, as an approximation of steady-state queue lengths of a heavily loaded network. Theorem 7 also shows that each stationary queue is of order uniformly in . Together with Theorem 8 this gives convergence of all moments (Corollary 2 of the paper) and, through Theorems 9–12, steady-state approximations of sojourn times and product-form limits.
Formalizing it. No part of this argument is machine-checked. The formalization would add reusable infrastructure for queueing theory in Lean: a Markov-state model of a generalized Jackson network with residual times, Lyapunov bounds on stationary distributions of general Markov processes (Theorems 5–6), and the link between tightness and identification of limit points for stationary laws. Reiman's theorem (Theorem 4) and the Harrison–Williams theorem (Theorem 3) are cited by the paper and are themselves open formalization targets.
Tightness and Reiman's theorem do not combine on their own. Reiman's theorem describes the network on finite time intervals, started empty, while a stationary distribution describes it as time goes to infinity; nothing in the finite-horizon limit forces a limit point of to be stationary for the RBM, or forces different subsequences to have the same limit. The interchange therefore needs the process limit from an arbitrary initial law and the uniqueness of the RBM's stationary law, besides tightness.
The tightness step is the technical core. Moment bounds must be uniform in and in the initial residual times. A Lyapunov argument on the workload over a time horizon of order requires deviation bounds of order for renewal processes started at arbitrary ages. This is why the residual-life conditions (1)–(2) appear, and why the strong approximation of Lemma A.2 is used. A naive drift argument over a fixed time horizon fails: in heavy traffic the drift of per unit time is only of order .
Fin J, vectors Fin J → ℝ, is Pᵀ, and the norm is the norm, written as an explicit sum. The spectral-radius condition is .IsGJN (positive times, conditions (1)–(2), substochastic ). and count renewal epochs in . The initial times , are residual lives given the elapsed ages , . States carry their elapsed times as reals; the predicate InStateSpace cuts out , and the uniform bounds over initial states (Lemma A.1, Propositions 2–3) and the initial laws of Theorem 4 range over only.Reiman84.QueueLength.Paths (Brownian motion with drift and covariance, and the reflection pair). An RBM stationary law must be a probability measure carried by . Weak convergence of laws on uses Mathlib's topology on ProbabilityMeasure. Theorem 4's process convergence is in coupling form with the uniform topology on .