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?
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 .In an online decision problem a decision maker chooses actions one period at a time, and only after each choice learns what that choice cost. The classical instance is prediction with expert advice: each day one of experts is followed, and afterwards every expert's loss is revealed. The goal is a strategy whose total cost is close to that of the best single fixed action in hindsight, whatever the sequence of costs.
Many structured problems have exponentially many actions, such as paths in a graph whose edge delays change daily. Weighted-majority methods keep one weight per action and are then inefficient. A. Kalai and S. Vempala (J. Comput. System Sci. 71 (2005) 291–307) showed that it suffices to be able to solve the offline problem: given total costs, find the best single action. Their algorithm, Follow the Perturbed Leader (FPL), adds a random perturbation to the accumulated costs and calls the offline solver once per period. The idea goes back to J. Hannan (1957); the paper's analysis made it short and broadly applicable, and FPL has since become a standard tool in online learning and online combinatorial optimization.
Timeline.
Decisions and states are vectors in . The decision set is a possibly infinite set and the state set is . In period the decision maker picks , then the state is revealed, and the cost is the dot product . The state sequence is fixed in advance (an oblivious adversary).
Write , with . The offline oracle is a map with
Because costs are linear, the best fixed decision after periods has cost
Three parameters measure an instance, with :
FPL(), for a parameter : in each period , draw uniformly at random from the cube and play . Its expected cost is .
Hannan(): the same rule with uniform on .
For every state sequence and every ,
The constants are the paper's. With the expected regret is at most .
For any state sequence in , any and any ,
This bound needs no knowledge of . It is included as a separate theorem, not a milestone of the goal.
The result. Theorem 1.1(a) reduces online linear optimization over any decision set to its offline counterpart, at the price of one oracle call per period and regret . Applied to online shortest paths, spanning trees and other combinatorial problems it gives efficient algorithms where weighted majority would maintain exponentially many weights. Later uses of FPL (approximate oracles, robust optimization via online learning) start from this bound.
Formalizing it. The theorem has been proved in print for twenty years; it has no machine-checked proof that we know of. The platform already holds a formalization of Ben-Tal, Hazan, Koren and Mannor's approximate-oracle variant (OracleRO.ApproxFPL), which takes a maximising oracle and an oscillation bound and therefore yields a weaker constant () in this setting. This mission states the exact-oracle bound with the paper's constant , where bounds itself. A correct proof must handle that constant carefully; see the next section.
Display (4), Lemma 3.1 and display (5) are finite-sum arguments from the defining property of . Lemma 3.2 is a statement about Lebesgue measure of a cube and its translate.
The central difficulty is the stability step: bounding, period by period, how much worse it is to play than . The obvious argument says that the two perturbed points have laws that agree on a fraction, and on the rest "one can only be larger". Under the printed definition of the difference of two costs can be as large as , so this per-period bound fails for costs of mixed sign: with , and suitable , the per-period difference is , while . The theorem itself, with , remains true, but a proof cannot proceed by the per-period comparison as written. Proving the goal with the stated constant, rather than , is the substantive part of the mission.
Fin n → ℝ; is dotProduct (⬝ᵥ); is written out as ; is the Lean norm ‖x‖, which on Fin n → ℝ is the sup norm. The sets are Dset and S; the diameter is Ddiam.s : ℕ → Fin n → ℝ indexed from (s 0 is unused); the hypothesis is imposed for .IsArgminOracle Dset M: and for all . Every theorem quantifies over all such ; the oracle is never a chosen Classical.epsilon minimiser.OracleRO.ApproxFPL.FPL: prefixSum s t ; perturbLaw n ε, the uniform law on ; and fplExpectedReward M s ε T , which with an argmin oracle is the expected cost of FPL() (its name reflects a maximisation source). Using one integral per period is the paper's own observation that fresh and shared perturbations give the same expectation.Contributions welcome: proofs of the milestones, the goal and Theorem 3.3, and reusable lemmas on uniform laws over translated cubes.
Classical arbitrage pricing fixes one probabilistic model of the underlying asset and prices a contingent claim as an expectation under an equivalent martingale measure. When the volatility is not known, a seller who wants to be safe under every plausible model has to superreplicate: hold an initial capital and a trading strategy whose terminal value dominates the claim under all models at once. The uncertain volatility model (UVM) of Avellaneda, Levy and Parás (Appl. Math. Finance 1995) and Lyons (Appl. Math. Finance 1995) is the standard instance: the volatility is only known to lie in an interval .
The family of laws describing such uncertainty is not dominated by a single reference probability, so "almost surely" and the usual stochastic integral are not available. Denis and Martini (Ann. Appl. Probab. 2006) replace them by a capacity and a quasi-sure stochastic integral, and show that the superreplication price of a broad class of path-dependent European claims is a supremum of expectations over martingale laws. This framework is a precursor of quasi-sure analysis and -expectations (Denis, Hu and Peng, Potential Anal. 2011; Soner, Touzi and Zhang, Electron. J. Probab. 2011).
Fix . is the space of continuous paths with , with the uniform norm, Borel -field and canonical filtration . A martingale measure is a probability on under which is an -martingale; denotes the set of these.
A nonzero measure on with continuous distribution function bounds the bracket. Hypothesis on a set says for every ; adds a lower bound . In the UVM, and .
The capacity of a bounded continuous is , extended to all functions through lower semicontinuous majorants. A set is polar if its capacity is , and a property holds quasi-surely (q.s.) outside a polar set. is the completion of under . Elementary integrands have integrals , and is their completion for . is the space of attainable gains. The superreplication price of a claim is
Assume and that is Hölder continuous. There is a set of martingale measures satisfying such that
for every bounded continuous of the form , or , with (and the cylindrical ) bounded continuous. The goal leaves unspecified, as the paper does.
In attack order: the transfer of a.s. inequalities to q.s. ones (Lemma A.7); the pathwise moment bound q.s. (Proposition 2.9) and its price form (Proposition 2.13); a universal bracket (Lemma 2.10) approximated by realized variance (Lemma 2.14); weak duality (Lemma 2.15); the representation over probabilities on the Stone–Čech compactification (§5, p. 19) and the Cauchy–Schwarz inequality for (Lemma 4.3); the martingale property and continuity of under each (Proposition 5.2); the bracket bounds for the induced law (Lemma 5.3); membership of the three claim families in the class of with (Lemmas 5.4–5.6); and Theorem 3.1 for the literal class .
Further statements: Theorem 6.1 (all martingale measures with form a valid ), Proposition 3.2 (the case ), Proposition 2.12 (measures not charging polar sets inherit the bracket bounds), Theorem A.8 (closedness of under ).
The theorem identifies the cheapest model-free hedge of path-dependent European claims (cylindrical payoffs, Asian-type averages, lookbacks on the maximum) with a worst-case expectation over martingale laws obeying the same bracket bounds. Theorem 6.1 specializes it to the generalized UVM, where the dual set is all martingale measures with ; the paper notes this is new even for the Lebesgue case. The result supplies a rigorous non-dominated duality on which robust pricing bounds and -expectation pricing rest.
The theorem is proved in the paper; no part of it is machine-checked. A formalization would produce the first Lean development of a capacity on path space, of a quasi-sure stochastic integral, and of a continuous-time quadratic variation on the canonical space. These objects are absent from Mathlib, which has discrete- and continuous-time martingales, the Stone–Čech compactification and the Riesz–Markov–Kakutani theorem, but no stochastic integral.
The family is not dominated, so neither the Itô integral of a single model nor a common null set is available: every inequality obtained under one by the Itô formula must be lifted to a quasi-sure one, and every limit taken in the capacity. The natural dual argument (Hahn–Banach on ) produces linear forms whose representation as measures on is not available because need not be all of . The paper's route works on bounded continuous claims and compactifies; the price is that the dual measures live on , where is unbounded and must be extended by truncation, and the identity linking back to holds only for a class of claims that has to be checked family by family.
is a subtype of C(Set.Icc 0 T, ℝ) (paths with ) with the Borel -field of the sup-norm topology. Distribution functions are continuous StieltjesFunctions vanishing at and positive at . The quadratic variation is a predicate: an adapted process with -a.s. continuous nondecreasing paths from such that is a martingale. The capacity takes values in with the Appendix's Lebesgue extension; q.s. means outside a set of capacity zero. , and are membership predicates on functions. is the image of the completion . and every supremum are extended reals. is Mathlib's StoneCech, and is the set of Borel probabilities on it dominated by on .
Standing assumptions, stated as hypotheses: on for all §2 results, where the page assumes it, and Hölder continuity of for every result of §4–§5 and the goal (p. 12: "From now on, we assume that is Hölder continuous"). The goal replaces the class , which is defined only inside the proof, by the three families of Lemmas 5.4–5.6. The literal form is a milestone. Lemma 2.14 adds . Lemma 5.3 is stated for the law on .
The following trivializing formalizations are ruled out. An empty with a real-valued would make the goal ; here both sides are . Defining q.s. as "a.s. for every " would make Lemma A.7 a tautology. Replacing by the closure of elementary integrals would shrink . Dropping the martingale condition from the quadratic-variation predicate would make satisfiable by any deterministic process.
A complete development needs Itô's formula and the Burkholder–Davis–Gundy inequalities for continuous martingales, Doob–Meyer uniqueness, a Kolmogorov continuity criterion, and the theory of regular Choquet capacities. These are reusable well beyond this mission, and contributions of any of them are welcome.
Large call centers, cloud server farms and hospital wards are modeled as many-server queues: identical servers, customers arriving according to a counting process, each customer served by one server for a random time drawn from a distribution , and customers who find all servers busy waiting in a first-come first-served queue. When is large, the number of customers is of order and the natural object of study is the fluid limit, obtained by dividing all quantities by and letting . For exponential service times the fluid limit is a finite-dimensional ordinary differential equation. For a general service distribution — and call-center data show service times far from exponential (lognormal, in Brown et al., 2005) — the state must record how long each customer in service has been served, and the fluid limit is a measure-valued process.
Kaspi and Ramanan (Ann. Appl. Probab. 21 (2011) 33–114) characterize this limit by a pair of fluid equations for general with a density, prove that they have at most one solution, show that the scaled -server processes converge to it, and describe its long-time behavior. This mission is the last of these results: in the critically loaded fluid system, every solution converges to equilibrium.
Timeline. Whitt (2006) introduced a fluid model of the many-server queue with general service times and abandonment, and stated the case of property (1) of the goal theorem without proof (his Theorem 7.3). Kaspi and Ramanan (2011) gave the measure-valued formulation with the age process, uniqueness and existence of fluid solutions, and the convergence to equilibrium formalized here. Reed (2009) treated the related queue in the Halfin–Whitt regime.
The service distribution has a density , is carried by , and has mean one: . Let , and let be the hazard rate on .
The fluid state at time is a number , the scaled number of customers in system, and a measure on of total mass at most one: is the scaled number of customers in service whose age (time already spent in service) lies in . The input is a nondecreasing càdlàg arrival function with , an initial number and an initial age measure , satisfying (servers are idle only when nobody waits). The set of such triples is .
A càdlàg pair solves the fluid equations if the cumulative departures are finite, the entries into service satisfy the transport equation
for every compactly supported test function on (ages grow at unit rate, customers leave at rate , new customers enter at age ), mass is conserved, , and the system is non-idling, .
The equilibrium measure is on , a probability measure by the mean-one normalization. With (arrival rate equal to the total service capacity), and is a constant solution. Assumption 2 asks that be bounded or lower semicontinuous near . The renewal measure of is , the unit mass at included.
Under Assumption 2:
Theorem 3.9(2) is the stability statement of the fluid model in the critically loaded case: whatever the initial occupancy and the initial ages, the age distribution of customers in service converges to the stationary excess distribution of . It justifies using as the operating point around which diffusion approximations of many-server queues are built, and it is the fluid counterpart of the classical fact that the age of a stationary renewal process has density . Part (1) gives the transient behavior of an underloaded or critically loaded system started empty.
The result is proved in the paper; nothing here is open. To our knowledge none of it has been formalized. A formalization adds machine-checked statements of a measure-valued fluid model that the companion mission (uniqueness of fluid solutions, Theorem 3.5) shares, and exercises renewal theory — the renewal measure, a key renewal theorem for laws with a density, Lorden's inequality — in a form usable by other queueing developments.
The naive argument would show that is given by an explicit formula and pass to the limit. The explicit age representation of a solution involves , which is known only through a renewal equation whose forcing term depends on itself; there is no closed form unless the system never fills up. For the system can alternate between full and not full, and the convergence must be proved without knowing when. Two ingredients carry the weight: a comparison showing that the occupancy tends to one, and a key renewal theorem for the backward recurrence time of a renewal process with a density, which needs total-variation rather than vague convergence because the test functions are only bounded and continuous. The uniform-in-time control of Lemma 6.3 is where the second moment enters.
Everything lives in ManyServerFluid.Equilibrium. The service law is a structure holding the density with , on , , and mean one. Time is , read on . Age measures are Mathlib FiniteMeasure ℝ carried by , with the weak topology, so "càdlàg" is in the paper's topology. The departures are lower integrals in ; and are Lebesgue–Stieltjes measures. The convolution powers are the published QueueingFundamentals.MG1.convPow.
Explicit choices, each also stated in the item that uses it:
Weak convergence in Theorem 3.9(2) is against all bounded continuous functions, not compactly supported ones; vague convergence would let mass escape towards and is not the theorem. The monotonicity in part (1) is part of the statement. A formalization in which these were dropped, or in which omitted the unit mass at , would state a different result.
Existence. The paper's proof of Theorem 3.9(2) compares an arbitrary solution with the solution started empty, which it obtains from its Theorem 3.7 (existence via the -server limit); that theorem is not part of this series. Here every solution is a hypothesis, so nothing false is stated, but a proof of the goal must construct the empty-start solution for . It is explicit: has density on while , and from on it equals (Proposition 6.1, Remark 3.8, Lemma 3.4).
Contributions welcome: general renewal theory (local finiteness of , Lorden's inequality, the key renewal theorem for spread-out laws in total variation), and lemmas on the fluid equations shared with the uniqueness mission (the monotonicity of , the renewal equation (4.5), the age representation (3.11)).
Principal component analysis estimates the eigenvalues of a population covariance matrix by those of the sample covariance matrix . Before random matrix theory turned to the regime where the dimension grows with the sample size, the classical question was the opposite one: the number of variables is fixed and the number of samples tends to infinity. In that regime almost surely, and the next question is the size and shape of the fluctuations of the sample eigenvalues. When has a repeated eigenvalue, the sample eigenvalues near it do not fluctuate independently: they repel each other, and their joint limit law is that of the eigenvalues of a random Hermitian (or symmetric) matrix. Anderson (1963) derived these limits for real Gaussian samples.
Baik, Ben Arous and Péché (2005) study complex Gaussian samples whose covariance matrix is the identity apart from finitely many "spiked" eigenvalues, and find a phase transition for the largest sample eigenvalue as together. Their Proposition 1.1 is the fixed-dimension counterpart: with fixed and all population eigenvalues equal, fluctuates on the scale with the law of the largest eigenvalue of a Gaussian unitary ensemble (GUE). The paper places it beside its Theorem 1.1(b), where a -fold spike above the critical value gives the same GUE limit when . This mission formalizes Proposition 1.1.
Fix and . A standard complex Gaussian is with independent centred real Gaussians of variance , so . For each , let , , , have independent standard complex Gaussian entries (sampleLaw M k), and let the samples be : mean zero, covariance . The sample covariance matrix is
a Hermitian matrix (sampleCov), and is its largest eigenvalue (largestEig). The general model sampleVec U ℓ G m is specialized to and , because a Hermitian matrix with all eigenvalues equal to is .
Write (vandSq). The finite-GUE distribution (Definition 1.2) is
the distribution function of the largest eigenvalue of a GUE matrix. In Lean these are G k x and Z k.
For every real and every ,
The second statement is in probability.
With , , and :
The proposition identifies the fixed-dimension limit of the top sample eigenvalue under a degenerate population spectrum: the sample eigenvalues near , rescaled by , behave like a GUE spectrum, and like its maximum. For it reduces to the central limit theorem for the sample variance of one complex Gaussian variable, with limit by (29). For general it shows that the GUE limit of the supercritical regime in Theorem 1.1(b) is already present when the dimension does not grow.
The result is proved in the paper (§5, p. 1691) by an exact computation. No machine-checked proof of it, of the complex Wishart eigenvalue density, or of the Gaussian and Laguerre cases of Selberg's integral is known to exist in Mathlib or on the platform. The formalization requires the joint eigenvalue density of a complex Wishart matrix (a Weyl-type integration formula over the unitary group), two Selberg-type integral evaluations, a Stirling asymptotic for products of factorials, and a dominated-convergence argument on . The first three are reusable well beyond this mission.
The limit itself follows from (304) and the constant asymptotics. The hard part is (302): passing from the law of the matrix to the joint law of its eigenvalues. This requires the change of variables with unitary, the Jacobian , and the integration over the unitary group. A direct central limit argument for the entries of gives the Gaussian limit of as a GUE matrix. To get from there to one needs the continuity of the largest eigenvalue in the matrix entries and a matching normalisation, so it is a different route from the paper's. Either route requires spectral facts about Hermitian matrices that Mathlib does not yet package. The Selberg evaluations (27) and (303) are classical but have no short proof: the standard arguments use orthogonal polynomials or an induction with a Dixon–Anderson type integral.
(sampleLaw M k).real of explicit sets.Contributions are welcome on each milestone. Particularly reusable are the complex Wishart eigenvalue density, the Gaussian and Laguerre Selberg integrals, and the measurability and continuity of eigenvalues of Hermitian matrix families.
Affine processes are Markov processes whose Laplace transform depends exponential-affinely on the initial state. On the cone of positive semidefinite matrices they model stochastic covariance matrices in multivariate stochastic volatility, interest-rate and credit models. Examples include the Wishart process of Bru (Bru 1991) and Ornstein–Uhlenbeck processes driven by matrix Lévy subordinators (Barndorff-Nielsen and Stelzer 2007, reference [3] of the paper). Cuchiero, Filipović, Mayerhofer and Teichmann (2011) characterize all affine processes on by admissible parameter sets.
On the canonical state space , Duffie, Filipović and Schachermayer (2003) showed that regular affine processes are exactly the infinitely decomposable Markov processes: the law started at is a -fold convolution of laws started at the . That property drives their existence proof. On with it fails. The Wishart marginals are not infinitely divisible, a classical result of Paul Lévy. This mission formalizes the exact characterization: Theorem 2.9 of Cuchiero et al.
is the space of real matrices and the symmetric ones. carries the pairing and the norm . is the closed convex cone of positive semidefinite matrices, and its one-point compactification. The point is the cemetery, where a killed process goes.
A transition family consists of sub-stochastic kernels on satisfying and the Chapman–Kolmogorov equations. It is stochastically continuous if weakly as . The process is affine (Definition 2.1) if there are and with
Theorem 2.4 of the paper attaches to every affine process a unique admissible parameter set . In it, is the diffusion parameter, the constant drift, and the killing rates, and and the jump measures. The exponents solve the generalized Riccati equations , , with given by (2.16)–(2.17).
The canonical space consists of paths that stay at once they reach it, with coordinate process . is the set of families of laws on under which is a stochastically continuous Markov process with . The convolution is the image of under . A family is infinitely decomposable (Definition 2.7) if for every there is with . It is infinitely divisible if every marginal is.
For and , the following are equivalent:
The theorem separates two classes that coincide on . On with , a diffusion component, which must satisfy , is incompatible with taking -th roots, because the root would need drift . So the existence proof of Duffie–Filipović–Schachermayer, which builds a process from infinitely divisible kernels, covers exactly the pure-jump affine processes on . Processes with a diffusion part need the martingale-problem approach of the paper's §5. Proposition 5.11 gives the alternative existence proof for (§5.3).
The theorem is proved in the paper. As far as is known, none of it has been machine-checked: no formal library has affine processes on matrix cones, convolution of path measures, or the Lévy–Khintchine form on . Formalization contributes a checked equivalence that rests on the paper's other main theorem (Theorem 2.4), together with reusable statements about Cauchy's equations on cones and Laplace functionals of Markov families. It is the third mission of a series. Missions I and II formalize the two halves of Theorem 2.4.
The equivalence links three layers: path-space laws, one-dimensional kernels, and Riccati exponents. (i) (ii) first needs the multiplicative structure of Laplace functionals in the initial state. That gives affinity of the process and of each -th root, with exponents . Then it needs the fact that the root's parameter set is and is again admissible, so for all . The second step relies on the full necessity theorem, in particular Proposition 4.18. The first fails without strict positivity of the Laplace functional: Cauchy's exponential equation has non-exponential solutions that vanish somewhere (Remark 6.3). (ii) (iii) requires every Riccati solution to stay in the Lévy–Khintchine cone. This is clear for finite-variation jumps via Picard iteration, but the general case needs the approximation . (iii) (i) must produce a Markov family of -th roots on path space, not merely roots of each marginal. The case shows that cannot be dropped: there the Cox–Ingersoll–Ross process has and is infinitely decomposable.
Fin d → Fin d → ℝ, with and . is the subtype of matrices with Mathlib's PosSemidef.OnePoint of the cone, with its Borel σ-algebra. Addition is extended with absorbing. is the space of all paths with the product σ-algebra; every notion in the theorem depends only on finite-dimensional distributions. Absorption at and the Markov property with transition family are imposed through finite-dimensional distributions. The path-sum map is measurable, which is checked in Lean, so the convolution is a genuine push-forward.In the local model of differential privacy, no trusted curator ever sees the raw data: each individual randomizes their own record before handing it to the analyst. This is how private telemetry is collected in practice (randomized response and its descendants), and it raises a basic question: which learning tasks remain possible when the learner only sees locally randomized records?
Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith answered it in What Can We Learn Privately? (arXiv:0803.0924v3, the accepted version of SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; theorem numbers below are the arXiv v3's). They showed that local private learning is equivalent, up to polynomial factors, to learning in Kearns' statistical query (SQ) model (Kearns 1998), where an algorithm sees a distribution only through approximate expectations. This mission formalizes one direction of that equivalence: every SQ algorithm can be run by a local algorithm (§5.1.1, Theorem 5.7). The other direction (Lemma 5.8) is a separate mission of this series.
Timeline. Blum, Dwork, McSherry and Nissim (PODS 2005) observed that SQ algorithms can be simulated by a trusted curator adding noise to sums. Dwork, McSherry, Nissim and Smith (TCC 2006) introduced the Laplace mechanism. Kasiviswanathan et al. (FOCS 2008; journal version 2011) showed the simulation works even in the local model, with each record entering a single randomizer.
A database is a vector ; two databases are neighbors if they differ in exactly one entry. A randomized algorithm is -differentially private if for all neighbors and all measurable sets of outputs. An -local randomizer is an -differentially private map applied to a single record: for all .
The Laplace distribution has density .
An SQ oracle for a distribution on receives a query and a tolerance , and may return any with . An SQ algorithm with queries asks , where may depend on the earlier answers (adaptive), and outputs a function of all answers. A vector is a valid transcript against if every is within of the true mean of the query asked at that point.
For one query , the randomizer with is applied to each record, and the local algorithm outputs the average . The simulation of an SQ algorithm answers its -th query by running on the -th block of fresh entries and finally outputs what the SQ algorithm outputs on these answers.
There is an absolute constant such that, for every SQ algorithm with queries into , and every ; the accuracy claim further takes every tolerance at least , , and :
On that event the simulation outputs exactly what the SQ algorithm outputs against a valid oracle. The constant is left unspecified, as in the paper.
Theorem 5.7 is the inclusion "SQ ⊆ local" in the paper's characterization of local private learning: every concept class learnable with statistical queries is learnable by an -local algorithm, with sample size growing like . Combined with the converse simulation (Lemma 5.8), it identifies local private learnability with SQ learnability (Theorem 5.14). It thereby transfers the known SQ lower bounds, such as the one for parity, to the local model. It also shows that nonadaptive SQ algorithms become noninteractive local protocols.
The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization fixes what "the simulation gives the same output" means against an adversarial oracle and an adaptive algorithm. It also supplies reusable Lean objects for local differential privacy, Laplace noise and SQ algorithms.
The privacy half is the easy-looking part, but it is adaptive: the query asked in block depends on the noisy answers from blocks . A database change in block therefore changes the law of all later answers, not only . The argument must use that every entry enters exactly one randomizer and compose along the adaptive transcript.
The accuracy half has the same adaptivity issue: the union bound over queries needs, for each , the failure probability of block conditioned on everything before it. That is where the fresh blocks and measurability are used. The concentration step for Laplace averages is sub-exponential, not sub-Gaussian. The naive use of the paper's appendix lemma (A.3) fails: it is stated as an equality for every deviation , but its proof only covers deviations of order the Laplace scale.
Databases are Fin n → D (0-based). Randomized algorithms are identified with the laws of their outputs (Measure); differential privacy is required on all measurable sets. An SQ algorithm is a deterministic adaptive strategy (SQAlg): a randomized one is a mixture over its coins, to which the result transfers. "At most queries" is "exactly " after padding with dummy queries. Queries are real valued with , as the paper allows after Definition 5.4. Block consists of the database indices , so the blocks are disjoint by construction, and the simulated answers are a deterministic function of the database and the noise array. The natural logarithm replaces the paper's base 2, which only changes . Constants are existential and quantified before everything else.
Explicit choices, each recorded in the item that makes it:
A trivializing formalization is ruled out: the oracle is not replaced by the exact expectation, accuracy is required for every query actually asked (not only the first), privacy holds for every database (not only i.i.d. samples), and the constant cannot depend on , , , , or the algorithm.
Needed infrastructure: the Laplace distribution as a probability measure and its moment generating function, a Hoeffding bound for bounded i.i.d. variables, the Laplace mechanism, and adaptive composition along a transcript. All of these are reusable beyond this mission. Proofs of the milestones, of standalone Laplace and composition lemmas, and of the goal are welcome.
Markov decision processes assume that the transition law is known exactly. In practice it is estimated from data, and the optimal policy computed for the point estimate can perform badly when the true law differs. 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. The worst case is taken against an adversary (nature) who may choose a law from the set at every step.
For this worst case to be computable by backward induction, the set of path measures of a policy has to decompose epoch by epoch. Garud Iyengar named this property Rectangularity and proved that under it the classical finite horizon theory carries over: a robust Bellman equation holds, and deterministic Markov policies are optimal among all history dependent randomized policies, with state and action sets that may be countably infinite and ambiguity sets that need not be convex (Iyengar, CORC Tech Report TR-2002-07, rev. 2004; published in Math. Oper. Res. 30(2), 2005).
Timeline:
A finite horizon ambiguous Markov decision process (AMDP) has decision epochs , , and a terminal epoch . States lie in a countable set and actions in a countable set . In state at epoch the admissible actions form a nonempty set . For each admissible action , the next state is drawn from some probability measure , where is a nonempty set of probability measures on , the ambiguity set. The decision maker receives when is taken in and the next state is , and at the terminal epoch.
A history at epoch is . A policy assigns to each history a probability measure on . It is deterministic () if every is a point mass, and deterministic Markov () if moreover the chosen action depends on the current state alone. denotes all history dependent randomized policies.
Under Rectangularity (Assumption 1), the set of path measures consistent with is a product of one-epoch sets: nature chooses, for every epoch , every history and every admissible action , a measure , and the path measure is . The robust value of from and the robust value function are
The optimistic values , replace the infimum over by a supremum.
For , depends on only through ; for , ; and
The mission also contains, as a draft theorem that is not a milestone, the per-policy identity of the proof of Theorem 1, eq. (12): for each policy, .
Theorem 2 is the basis of robust dynamic programming in finite horizon: computing an optimal robust policy reduces to backward passes, each a family of one-stage problems . It also justifies restricting attention to deterministic Markov policies, which is what every algorithm in the robust MDP literature computes. Theorem 1 isolates the role of Rectangularity: without it the worst case over path measures does not decompose and the recursion characterizes nothing.
The results are proved on paper; no machine-checked proof is known. The platform holds the finite-state, Markov-controller special case (the Nilim–El Ghaoui RobustMDP series, posed, not proved), whose comparison class is too small to express the claim suffices against . A formal proof here supplies the history dependent policy and adversary machinery on countable spaces that the discounted robust theory and the robust MDP literature reuse.
The obvious argument writes the robust value as an inf–sup over path measures and pushes the infimum inside the expectation epoch by epoch. That step is the content of (12): the infimum of an expectation equals the expectation of an infimum only because nature's continuation choice may depend on the realized action and next state, so near-worst continuations for different branches can be glued into one admissible adversary. Infima need not be attained (the ambiguity sets are arbitrary, the state set countable), so the gluing is an -argument over countably many branches. The supremum over policies needs a matching splicing of -optimal continuation policies (13)–(14). Finally, randomized decision rules must be eliminated (15), which uses Rectangularity again, now per action. Restricting either the policies or the adversary to Markov ones from the start is not allowed: it changes the comparison class and makes the goal circular.
S and one countable action type A serve all epochs; the page's epoch-dependent sets embed into their disjoint union. Epochs are 0-based natural numbers, with terminal epoch M.N and 1 ≤ N.(Fin n → S × A) × S. Probability measures are PMF; as a tsum. The expected reward under a policy and an adversary is computed by backward iterated sums, which is the expectation under the product path measure (3).t < N; the supremum over equals that over the page's because uses only . An adversary chooses for every epoch, history and admissible action.Definitions: AMDP, History, History.extend, IsPolicy, Policy, IsDeterministic, IsDetMarkov, Adversary, Selection, expect, expTail, expectedReward, V, Vstar, Vbar, VbarStar, all in RobustDP.FiniteHorizon. Lemmas about gluing adversaries along history prefixes and about suprema of bounded families indexed by subtypes are reusable. Contributions to any milestone are welcome, in any order; (15) is a one-epoch statement independent of the rest.
A multistage stochastic program chooses decisions over time periods while a random input is revealed one stage at a time; the decision at stage may use what has been observed so far and nothing more. Such models are used for capacity expansion, hydro-thermal power scheduling, asset–liability management and production planning. In practice the true input process is never used directly: it is replaced by an estimate, a discretization or a scenario tree with few branches, and the program is solved for that approximation. Whether the optimal value of the approximate program is close to the true one is therefore the basic question behind every scenario-tree method.
For two-stage programs () the answer is classical: the optimal value is Lipschitz continuous with respect to suitable distances of probability distributions (Rachev and Römisch, 2002). For that methodology breaks down, because the multistage objective depends on conditional expectations given the past, and hence on the information structure of the input, not only on its distribution. Heitsch, Römisch and Strugarek (SIAM J. Optim. 2006) showed that the gap is closed by adding one more term: a distance between the filtrations generated by the true and the approximate inputs. Their estimate is the basis of later work on scenario-tree construction and on the nested distance of Pflug and Pichler.
Let be a probability space and a process with . The information available at stage is , and is the σ-field it generates; is deterministic, so . The linear multistage program (1) is
where is a polyhedron, for are polyhedral cones, and are fixed matrices, and the costs and right-hand sides are affine functions of the current input . Write for the objective and for the feasible set.
Which data are random fixes two integrability exponents: if only the costs are random, and ; if only the right-hand sides are random, ; otherwise . The input lives in and the decisions in , and is the distance of two inputs.
Three conditions are imposed: (A1) complete fixed recourse, for ; (A2) is finite and is level-bounded locally uniformly at : for some there are and a bounded set such that the level set is nonempty and contained in whenever ; (A3) .
The filtration distance at stage compares how well a near-optimal decision of one problem is predicted from the other problem's information:
Under (A1)–(A3) and boundedness of there are positive constants , , such that
for every input with and finite. The constants are existential: the theorem asserts the shape of the estimate, not its numerical values.
The theorem identifies what an approximation of a multistage input must preserve: closeness in alone is not enough, and the filtration term measures exactly the information that is lost or gained. It justifies scenario-tree construction by forward selection and reduction (Heitsch and Römisch, 2009), where both terms are controlled, and it is the precursor of the nested distance, for which analogous Lipschitz bounds are proved. Without such an estimate a scenario tree that matches the marginal distributions can still give an arbitrarily wrong optimal value.
The result is proved in the paper; it has not been formalized. A machine-checked version needs, and would produce, a formal theory of linear programs with decisions adapted to a generated filtration in spaces, Lipschitz continuity of polyhedral set-valued maps, and measurable selections of conditional-expectation projections. Each of these is reusable well beyond this paper.
The obvious argument — take a near-optimal policy for and evaluate it for — fails at once: that policy is adapted to , not to , so it is not feasible for the perturbed problem, and projecting it by conditional expectation onto destroys the equality constraints. Any repaired policy must again be -measurable at every stage, and an error made at stage propagates to all later stages through the recursion , where it must stay controlled in the right norm. The three integrability regimes need separate estimates; in the regime the error must be bounded essentially, not only on average.
The program is encoded in a single definitions file. Stages are natural numbers with dimension functions , . is given by finitely many linear inequalities and each , , by finitely many homogeneous ones, so "polyhedral" and "polyhedral cone" are built in. The matrices are linear maps between Euclidean spaces; and . A randomness pattern (costs, rhs, both) carries the exponents and its restriction on the data: for costs, for rhs, none for both.
The committed conventions are:
condExp;Trivializing formalizations are ruled out: the constants , , are quantified before ; the theorem covers all three randomness patterns; the level sets are nonempty, so the suprema are not vacuous; and a sorry-free check exhibits data satisfying (A1) with a feasible policy, so the hypotheses are satisfiable.
Contributions are welcome on Lipschitz continuity of polyhedral set-valued maps (Walkup–Wets), measurable selections, conditional expectation of set-constrained random vectors, and any of the case estimates.
A mathematical program with complementarity constraints (MPEC, also called MPCC) is a nonlinear program in which some pairs of constraint functions must be nonnegative with at least one of each pair equal to zero. Such programs model bilevel optimization, Stackelberg games, contact problems in mechanics, and traffic equilibrium design; see Luo, Pang and Ralph, Mathematical Programs with Equilibrium Constraints (Cambridge University Press, 1996). The complementarity constraints make every standard constraint qualification of nonlinear programming fail at every feasible point: neither LICQ nor MFCQ ever holds. Off-the-shelf NLP theory and solvers therefore do not apply directly.
Relaxation methods work around this by replacing the MPEC with a family of ordinary nonlinear programs indexed by a parameter and letting . The oldest of these is the global relaxation of Scholtes (SIAM J. Optim. 11, 2001). The relaxed programs are only useful if they are themselves well posed: a local minimizer of a relaxed program should carry Lagrange multipliers, so that the sequence of KKT points the method computes actually exists. Hoheisel, Kanzow and Schwartz (Preprint 299, Univ. Würzburg, 2010; published in Mathematical Programming) compare five relaxation schemes, prove convergence under weaker MPEC constraint qualifications than before, and ask which standard constraint qualification the relaxed programs satisfy. This mission formalizes their answer for Scholtes' scheme, Theorem 3.2.
A standard nonlinear program (2) on minimizes subject to and for finitely many and . At a feasible , the active set is . A family is positive-linearly dependent if some combination vanishes with and not all coefficients zero. The Mangasarian–Fromovitz constraint qualification (MFCQ) holds at if the gradients are linearly independent and some direction has for every active and for every .
The MPEC (1) minimizes subject to
with continuously differentiable data. At a feasible point the indices of the complementarity pairs split into (), () and (). The tightened program TNLP replaces each pair by equalities on the components that vanish at and a sign constraint on the other. MPEC-MFCQ holds at if standard MFCQ holds for TNLP at .
Scholtes' relaxed program , for , keeps , , , and replaces by . Its feasible set is . Lean notation: the MPEC is MPEC n m p l, TNLP is P.TNLP xs, is P.RS t, and MFCQ of an NLP Q at x is Q.IsMFCQ x.
If is feasible for the MPEC and MPEC-MFCQ holds at , there are a neighbourhood of and such that
The neighbourhood is fixed before and works for every .
Theorem 3.2 says that the relaxed programs inherit a standard constraint qualification from the MPEC. Consequently every local minimizer of near is a KKT point, which is exactly the hypothesis of the convergence theorem for Scholtes' method (Theorem 3.1 of the paper: limits of KKT points of are C-stationary under MPEC-MFCQ). Without it, the convergence theorem could be about sequences that do not exist. The result also replaces the MPEC-LICQ-based regularity results of earlier work by the weaker MPEC-MFCQ.
The theorem is proved in the paper; to our knowledge no part of this theory has been machine-checked. A formal development delivers a reusable layer for nonlinear programming in Lean: positive-linear dependence, MFCQ and its dual characterization, the tightened program of an MPEC and the MPEC constraint qualifications. Sibling missions of this series formalize Theorem 3.1 and the Kadrani–Dussault–Benchakroun relaxation (Theorem 3.5) on the same vocabulary.
The obvious argument is a continuity argument: MFCQ is an open condition, so it should persist near . This fails as stated, because MFCQ for is not a perturbation of MFCQ for TNLP: the two programs have different constraints, and the active set of at changes with and . Near a biactive index , the product constraint can be active, and its gradient tends to zero as . So it cannot be treated as a small perturbation of any gradient in the TNLP family. In addition, the neighbourhood must be uniform in , while the active product constraints depend on . The step that needs care is the regrouping of the multiplier equation of into a combination of TNLP-type gradients, with every coefficient's sign accounted for. The separate step from MPEC-MFCQ to positive-linear independence needs a theorem of the alternative (Motzkin's transposition theorem), which is not in Mathlib in this form.
EuclideanSpace ℝ (Fin n); is the inner product of gradient f x with d. Indices are Fin m (0-based), and are allowed.P.IsC1 on the goal and on milestones 3–5. Milestones 1–2 do not need it.𝓝 xs chosen before .The goal would be trivialized by a weakened MFCQ, for instance one that omits the linear independence of the equality gradients or requires the strict inequality only for some of the active constraints. Such a formalization is ruled out: IsMFCQ requires both conditions, over the full active set of . The neighbourhood must be a genuine element of 𝓝 xs, so an empty is excluded.
Welcome contributions: a proof of Remark 2.2, general lemmas on persistence of positive-linear independence under continuous perturbation, and the final assembly. These lemmas apply to nonlinear programming in general, not only to this mission.
Volume-preserving box transport supplies geometric operations for a finite computation. The selected goal assembles these into a force and a fixed particle observer. The pinned manuscript supplies the research context.
A finite machine and input determine effective velocity and force coefficients. The force depends affinely on positive viscosity, and after time one the velocity is periodic and depends only on the machine.
The selected goal is OAI.BalancedTransport.balanced_three_stack_realization. Its central assertion is
The theorem states that there exist velocity fields U(M,w), force coefficients f₀(M,w) and f₁(M,w), material flows X(M,w), and a globally 1-periodic velocity field R(M) for each finite deterministic tape machine M, with the following properties for every finite input word w. On nonnegative time and ℝ³, U, f₀ and f₁ are smooth and vanish outside a common spatial compact set independent of time; every mixed space-time derivative of U is uniformly bounded. Moreover, f₀ = ∂ₜU + (U·∇)U and f₁ = −ΔU. All three families are uniformly effective from the encoded machine and input: algorithms approximate every mixed derivative component at rational space-time points within 2⁻ⁿ, provide global integer bounds on these derivatives, and provide integer support radii. The velocity is 1-periodic after time 1 and satisfies U(M,w)(t,x) = R(M)(t,x) for every t ≥ 1, so its later field depends only on M. The flow satisfies X(0,a) = a and ∂ₜX(t,a) = U(t,X(t,a)); its trajectory starting at (4,0,0) enters (−1,2)³ at some nonnegative time exactly when M halts on w, meaning that a configuration with no next transition is reached after finitely many machine steps. For every viscosity ν > 0, the force f = f₀ + νf₁ is smooth, has uniformly bounded mixed derivatives, and is 1-periodic after time 1; U with pressure zero solves the incompressible Navier–Stokes equation ∂ₜU + (U·∇)U = νΔU + f with U(0,·) = 0. This velocity is unique among smooth zero-data solutions in the comparison class, and every such solution has spatially constant pressure. The comparison class requires the velocity and all spatial derivatives through order two to be continuous in time as L² functions, the velocity to be continuously differentiable in time in L², velocity and first spatial derivatives to be bounded on each finite time slab, and pressure, after subtracting a time-dependent scalar, together with its first spatial derivatives to be continuous in time in L²; (U,0) belongs to this class. Finally, derivative approximations and global derivative bounds for f are computable when ν is computable, and computable relative to any rational name of ν whose nth approximation has error at most 2⁻ⁿ.
The balanced three-stack realization is the main goal; balanced box routing is a separate supporting reference. The exact conclusion permits spatially constant pressure in competing solutions and explicitly states its comparison class. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Uniform effectiveness, compact support, periodic behavior and uniqueness must all coexist with exact halting detection.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.A force whose derivatives decay rapidly can still encode a computation in a particle trajectory. The selected construction makes the observer condition and effectiveness requirements precise. The pinned manuscript supplies the research context.
For each finite deterministic machine and valid input, compilers produce smooth force and velocity fields on nonnegative time and real three-space, with common compact spatial support.
The selected goal is OAI.AlternatingNS.alternating. Its central assertion is
The theorem states that for every positive real viscosity ν computable by rational approximations with error at most 2⁻ⁿ, there exist computable compilers for a force f and velocity U, and one compact set K⊂ℝ³, with the following property for every well-formed finite deterministic Turing machine M and valid finite input w. The compiled programs describe smooth fields f,U on [0,∞)×ℝ³, both spatially supported in K for all nonnegative times, such that every mixed space-time derivative D satisfies sup_{t≥0,x}(1+t+‖x‖)ᴶ‖Df(t,x)‖<∞ and the analogous bound for U, for every nonnegative integer J. Each program supplies rational approximations to all mixed derivatives at rational space-time points with requested error 2⁻ᵏ, effective moduli of continuity on bounded regions, and integer bounds for all these weighted derivative norms. The velocity starts from zero, is divergence-free, and solves the classical forced Navier–Stokes equation ∂ₜU+(U·∇)U=νΔU+f with identically zero pressure; specifically f=∂ₜU+(U·∇)U−νΔU. On every interval [0,T], U is continuous in H² and continuously differentiable in L², and U and its spatial derivative are uniformly bounded in space and time. Moreover, any classical solution (v,p) with the same force and zero initial velocity equals (U,0) pointwise for all nonnegative times, provided on every [0,T] it has v continuous in H², continuously differentiable in L², and uniformly bounded, and p continuous in H¹. Here these Sobolev continuity conditions mean continuous L² representatives of every spatial derivative through the indicated order; time derivatives at zero are taken within [0,∞). Every initial point a has a unique trajectory X(a,t) for t≥0 satisfying X(a,0)=a and ∂ₜX(a,t)=U(t,X(a,t)). Finally, the trajectory starting at (−1,0,0) has strictly positive first coordinate at some nonnegative time if and only if M halts on w, where encountering a missing instruction also counts as halting.
The goal is the alternating-coordinate construction at every positive computable viscosity. It includes Sobolev time regularity, effective bounds, zero initial velocity and the exact observer condition, rather than all three manuscript constructions. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The encoding must preserve all weighted derivative bounds and uniqueness in the stated comparison class while recording arbitrarily long computations.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.