Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Blackwell approachability is the vector-payoff analogue of von Neumann's minimax theorem. In a repeated game where each round's outcome is a vector , a player wants the running average of these vectors to converge to a target set , whatever the opponent does. Blackwell (1956) showed when this is possible, and approachability has since become a standard tool for calibrated forecasting, regret minimization with respect to general benchmarks, and learning in games.
Online linear optimization (OLO) is the problem of choosing points in a fixed decision set against a sequence of linear losses , with performance measured by regret against the best fixed point in hindsight. Algorithms with regret — "no-regret" algorithms such as online gradient descent (Zinkevich, 2003) — are among the most studied objects of machine learning.
Abernethy, Bartlett and Hazan (COLT 2011) showed that the two problems are algorithmically equivalent: each can be converted into the other with explicit control of the rates. This mission covers the direction from OLO to approachability.
Timeline:
A Blackwell instance consists of compact convex sets , , a payoff that is affine in each argument (biaffine), and a closed convex target set . Write for the Euclidean distance to a set, and for the closed Euclidean ball of radius .
A halfspace oracle takes a halfspace and returns a point ; it is valid if for every halfspace , for all .
A set is a cone if for all , . For , , and the polar cone of is .
An OLO algorithm maps past loss vectors to a point , and its regret is
Algorithm 2 runs on when is a cone: at round it sets , plays , observes , and feeds back to .
When is compact but not a cone, it is lifted: with and the concatenation, put and , and run Algorithm 2 on .
For a Blackwell instance with nonempty and compact, any valid halfspace oracle for the lifted instance, any OLO algorithm with values in , any and any , the run of Algorithm 2 on the lifted instance satisfies
The bound holds for every and every adversary, with no rate assumed for ; a no-regret then gives approachability.
The result. Corollary 18 turns any no-regret algorithm into an approachability strategy for a compact convex target, provided a valid halfspace oracle is available, with rate . Combined with online gradient descent it gives an approachability rate, and through the choice of OLO algorithm it lets approachability inherit the computational efficiency of online learning. The paper uses this route to build an efficient calibrated forecaster (Section 5). Together with the converse reduction (Theorem 16), it shows that the two problems are equivalent.
Formalizing it. The results are proved in the paper; none of them has been machine-checked. Formalizing them requires the conic duality formula for distances (Lemma 13), a quantitative lifting lemma (Lemma 14) and the bookkeeping of an interactive protocol. The proof of Lemma 14 on the page is a sketch: it refers to an undefined point and uses a triangle-similarity argument, so a complete proof is new work.
The reduction's core is Lemma 13: the distance to a cone is a maximum of a linear function over the polar cone's unit ball. Lemma 13 needs projection onto a cone in Euclidean space; for a non-closed cone the projection may not exist, and the argument must go through the closure. The lifting Lemma 14 is a geometric statement whose page proof relies on a picture and an undefined point, so the factor 2 has no complete written argument. Finally, connecting the average lifted payoff to the lift of the average payoff, and the halfspace guarantee to the regret, requires keeping the round indexing and the oracle's validity domain exactly aligned.
All spaces are EuclideanSpace ℝ (Fin d). The concatenation lives in EuclideanSpace ℝ (Fin (d+1)) with coordinate 0 equal to , so ; a product type with the sup norm would change every distance and is ruled out. Distances are Metric.infDist. The polar cone uses the paper's sign (), the negative of Mathlib's innerDual. A halfspace is the pair ; a valid oracle must answer every halfspace containing , including , not only the halfspaces the algorithm happens to query. The OLO algorithm is a map from histories Fin t → ℝᴰ with values in at every history. Rounds are , and the run of Algorithm 2 is given as hypotheses on sequences , which exist and are unique by recursion. The minimum in the regret and are written as sInf/sSup of images over nonempty compact sets, where they are attained.
Hypotheses added relative to the page: and in the goal; in Lemma 13 (the empty set is a cone under Definition 11 and the identity fails for it); in Lemma 14. Corrected misprints, each disclosed in the item's note: "" in Corollary 18 and (9) denotes the regret of the OLO algorithm on the lifted losses; Lemma 14's "" has a stray ; is the maximal norm of the set, not its diameter. The oracle in the goal is a valid oracle for the lifted instance, which is what applying Algorithm 2 to requires.
A formalization in which the oracle is valid only at the run's own queries, the OLO algorithm is unconstrained, the regret's minimum ranges over all of , or the middle term of the goal is dropped, is a different statement and is ruled out.
The development needs: the dual formula for the distance to a convex cone, nearest-point projection onto closed convex sets (in Mathlib), compactness of polar-cone slices, and finite sums of biaffine payoffs. The cone layer (Lemma 13) is reusable for the converse direction of the paper and for conic duality generally. Proofs of any milestone, and of the bridge from an oracle for the original instance to one for the lifted instance, are welcome.
Reinforcement learning methods estimate the value function of a policy : the expected discounted sum of future rewards from each state. When the state space is large, cannot be stored as a table and is approximated by a parametrized function. The most studied case is linear function approximation, where each state carries a feature vector and the estimate is . Temporal-difference learning with this approximation, linear semi-gradient TD(0), is one of the basic algorithms of the field, and Chapter 9 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) presents its analysis: where the algorithm can converge, why that point exists, and how good it is.
The history is short. Sutton (1988, doi:10.1007/BF00115009) introduced TD learning and showed positive definiteness of the matrix governing its expected update. Dayan (1992, doi:10.1007/BF00992701) extended convergence to TD(λ). Tsitsiklis and Van Roy (1997, doi:10.1109/9.580874) proved convergence with probability one for linear TD(λ) under on-policy sampling and bounded the error of the limit. Bradtke and Barto (1996) introduced least-squares TD (LSTD), which computes the same limit directly.
A finite Markov decision process has finite sets of states , actions and rewards , and dynamics , the probability of next state and reward after action in state . A policy is a probability distribution over actions for each state. It induces a Markov chain on states with transition matrix , , and expected one-step reward . For a discount rate , the true value is , the expected discounted return.
A state distribution is stationary if ; write . The feature matrix is the matrix with rows . The mean square value error of a weight vector is
Linear semi-gradient TD(0) updates . In steady state its expected update involves
and the TD fixed point is . A real square matrix , not necessarily symmetric, is positive definite if for every . The key matrix is .
Under the hypotheses above, with every and linearly independent feature columns, is invertible, , and
Positive definiteness of is the reason on-policy linear TD(0) is stable: it makes the expected iteration contract toward the fixed point for small step sizes, and it guarantees that the fixed point exists and is unique. The error bound (9.14) quantifies the price of bootstrapping: the limit of TD can be worse than the best linear approximation, but by at most the factor . The same objects , and the key matrix reappear in LSTD, in the analysis of off-policy divergence (Chapter 11 of the book, where is no longer the stationary distribution of and positive definiteness fails), and in gradient-TD methods.
All results here are known. The book gives the positive definiteness argument in a box and cites (9.14) without proof. None of them has a machine-checked proof on the platform; the general Woodbury identity (FamousTheorems.woodbury_identity) is available, and (9.22) is its rank-one case written for the LSTD recursion. The mission produces a formal account of the finite-state theory of linear TD(0), with every hypothesis the book leaves implicit stated.
The key matrix is not symmetric, so the usual tools for symmetric positive definite matrices do not apply directly, and is positive definite only because of the specific interplay between and : if is replaced by a non-stationary distribution the claim is false (this is the off-policy counterexample of Chapter 11). The error bound (9.14) is not a consequence of positive definiteness alone. The TD fixed point is not the minimizer of , and has to be compared with the error of the -weighted projection of , which requires controlling in the -weighted norm. The book gives no argument for this step.
The Lean development lives in the namespace SuttonBartoRL.LinearTD. The MDP has four-argument dynamics with a finite reward set and one action set for all states; policies are stochastic. is defined from expected discounted returns as the series , never from a Bellman equation or from . and are defined as the book's steady-state expectations (9.11), as finite sums over , and ; the matrix form is a milestone, not a definition. Features are a matrix Matrix S (Fin d) ℝ with rows ; linear independence of its columns is LinearIndependent ℝ Xᵀ. Positive definiteness is a custom predicate , not Mathlib's Matrix.PosDef, which requires symmetry. The minimum in (9.14) is expressed by quantifying over every . The matrix inverse is Mathlib's, which is zero on singular matrices; the goal therefore asserts invertibility of explicitly.
Hypotheses the book leaves implicit and the statements make explicit: (the continuing case); a stationary distribution of the chain induced by with for every (otherwise the key matrix is only positive semidefinite); linearly independent feature columns (the book's "degenerate cases", p. 205). The box calls the off-diagonal entries of the key matrix "negative"; they are zero wherever , so the criterion is stated with nonpositive entries. The book's sentence that "ensures that is always invertible" (p. 229) is false in general, because the summands are not positive semidefinite: with , , , , one gets . It is not stated; (9.22) carries invertibility of and a nonzero denominator as hypotheses.
A statement in which is defined as the solution of the projected equation, or in which is assumed invertible or positive definite, would make the goal trivial or empty; neither is done. Convergence of the stochastic algorithm with probability one is not stated, since the book says it needs conditions and a step-size schedule it does not give. The bound for the episodic case and for other bootstrapping methods (p. 208) is stated only by reference in the book and is not a target.
Useful infrastructure: the -weighted inner product and orthogonal projection onto the column space of , the non-expansiveness of a stochastic matrix in the norm of its stationary distribution, and the positive definiteness criterion for non-symmetric matrices. All of these are reusable in the off-policy and average-reward chapters of the book. Contributions of these lemmas, and of alternative proofs of the milestones, are welcome.
Open networks of single-server queues with general interarrival and service distributions are the standard model of job shops, communication networks and service systems. Outside the product-form (Jackson) case their queue-length distributions are not known in closed form. When every station is close to saturation, a heavy-traffic limit replaces the network by a diffusion process. Martin I. Reiman's paper Open Queueing Networks in Heavy Traffic (Mathematics of Operations Research 9(3), 1984) proves such a limit for the vector of queue lengths of a general open network. The limit is a reflected Brownian motion on the nonnegative orthant. That process has since become the default diffusion approximation for open networks, and it is the starting point of later work on its stationary distribution and on control of networks in heavy traffic.
Timeline:
(These attributions follow Reiman's own account, pp. 441–442 of the 1984 paper.)
There are single-server stations and a nonempty set of stations that receive customers from outside. The primitives are mutually independent sequences of IID random variables: interarrival times (), service times , and routing indicators . When the th customer served at station finishes, it moves to station , or leaves if . The parameters are the service rates , the service-time variances , the arrival rates (with for ), and the interarrival variances . The routing matrix , , has spectral radius strictly less than one, so every customer eventually leaves.
Let be the number of exogenous arrivals to station by time , and the number of service completions at in units of busy time. Let , with . The queue length and the busy time are the unique solution of
A sequence of such networks, indexed by , shares , and . Its parameters converge to finite limits . With , the heavy-traffic condition is
Moments of order of the interarrival and service times are bounded uniformly in . The scaled queue length is , .
Let be a Brownian motion with drift and covariance matrix , where
Let be its reflection with reflection matrix . Then
The goal fixes no constants beyond the parameters' limits. It is stated for every network sequence satisfying (20)–(26).
The milestones follow the paper's proof, in order:
Theorem 1 justifies the diffusion approximation of a heavily loaded open network. Writing reduces questions about the network to questions about one reflected Brownian motion, whose data are explicit functions of the first two moments of the primitives and of the routing matrix. The same limit, with Lemma 2, gives the paper's Theorem 2 on sojourn times. It is the model case for the multiclass heavy-traffic theory that followed.
The result has been proved since 1984. No machine-checked version exists. The mission's contributions would be:
The obvious route applies a functional central limit theorem to directly. That fails because is not a sum of independent terms: each station serves only while its queue is nonempty, so the service process is evaluated at the random busy time , which depends on the whole network. The proof therefore has to separate the netput process, which obeys a central limit theorem, from the regulator . It then has to show that the random time change converges to the identity, i.e. that idleness vanishes on the diffusion scale. Weak convergence must also be transported through a reflection map that is defined on all of but is known to be continuous only at continuous paths.
The Lean development uses the following conventions:
Fin K, vectors are row vectors Fin K → ℝ, and a row vector times a matrix is Matrix.vecMul.Fin (K+1), with 0 meaning "leaves" and j.succ meaning station .iIndep of their σ-algebras), IID within each sequence, everywhere positive and square integrable.ℕ; (25)–(26) are imposed for , (22) and (26) over , and is the same for all .Added hypotheses, each implicit on the page:
No positivity hypothesis on the limits is added: (25) and (26) bound the means of the service and interarrival times, so the limits are positive.
The statement is not to be weakened. Ruled out are:
Each of these is a different theorem.
Useful contributions, all reusable beyond this mission:
A hotel sells rooms of several types, in limited numbers, to guests who each want one room. The revenue-optimal way to sell is known only in special cases: for buyers with several private values, optimal mechanisms can be randomized, involve lotteries, and lack a closed form (Manelli–Vincent 2007; Chawla, Hartline, Kleinberg 2007). In practice sellers post prices. The question is how much revenue posting prices gives up.
Chawla, Hartline, Malec and Sivan (arXiv:0907.2435v2, STOC 2010) answer it for a broad class of single- and multi-parameter problems. For unit-demand buyers of multiple copies of multiple items they show that a menu of posted prices, offered to the buyers in whatever order they arrive, earns at least of the revenue of any deterministic truthful mechanism (Theorem 14). This mission formalizes that result together with the two steps it is built from: a reduction from the multi-parameter problem to a single-parameter one with "copies" of each buyer (Lemma 3, Theorem 4), and an order-oblivious pricing for the intersection of two partition matroids (Theorem 13).
Single-parameter problem (BSMD). Finitely many agents have independent private values , each with a density on a bounded interval. A seller may serve any set in a downward-closed set system . A deterministic mechanism maps reported values to a served set and payments ; it is truthful if reporting the true value is a dominant strategy and no agent ends with negative utility. Its expected revenue is . For prices , agent desires service if , and is the class of maximal feasible sets of desiring agents. The order-oblivious revenue is
a lower bound on the revenue of posting the prices to the agents in an adversarial order.
Multi-parameter unit-demand problem (BMUMD). There are buyers and a finite set of services, partitioned into the groups of services targeted at buyer . Buyer has value for each , all values independent with , and the set system is unit-demand: for feasible . A mechanism is truthful if no buyer gains by misreporting its whole vector , and individually rational if a buyer receiving pays at most and a buyer receiving nothing pays .
Copies. The instance replaces each buyer by single-parameter agents, one per service with value , under the same .
Price menus. Given prices and an arrival order , the price-menu mechanism approaches the buyers in order; buyer is offered the services of that can still be feasibly allocated, at prices , and buys a utility-maximizing one if some has .
Multiple copies of items. With items and copies of item , services are pairs and a set of services is feasible if it gives each buyer at most one item and uses at most copies of : the intersection of two partition matroids.
For regular distributions there are prices such that, for every arrival order , the price-menu mechanism is truthful and
for every individually rational, truthful deterministic mechanism .
The result shows that for unit-demand buyers, a seller loses at most a constant factor by replacing the optimal, possibly opaque, truthful mechanism with a menu of prices that does not depend on the order in which buyers arrive. The reduction of Theorem 4 is generic: any order-oblivious pricing for the single-parameter instance with copies, under any unit-demand constraint, transfers to the multi-parameter instance with the same factor. Theorem 13 supplies one such pricing for the intersection of two partition matroids, which is exactly the shape of the multi-unit, multi-item constraint.
All results here are proved in the paper and none is formalized elsewhere; the platform has Myerson's single-unit optimal auction and weak monotonicity in an abstract quasilinear model (Börgers), but no posted-price approximation, no copies reduction, and no order-oblivious revenue. The formal development adds a machine-checked account of the reduction (in particular that the price-menu mechanism is truthful and allocates a maximal feasible set for every order), a precise version of the probabilistic claim behind the constant , and reusable definitions of order-oblivious revenue and of multi-parameter truthfulness with the paper's individual rationality.
Lemma 3 needs more than the observation that the copies instance has more competition: one must build a truthful single-parameter mechanism with at least the same revenue. The allocation is copied, but the payments must be threshold payments of the copies mechanism, and showing they dominate the original payments uses both weak monotonicity and the paper's individual rationality, through the taxation principle.
Theorem 13 compares order-oblivious revenue with Myerson's revenue through the bound of Lemma 2, at prices built from Myerson's service probabilities scaled by . The step that is easy to get wrong is the probability that an agent is considered: the events "part is not full" and "part is not full" depend on overlapping agents, so the product bound does not follow from Markov's inequality alone; it holds because both events are decreasing in the set of desiring agents (Harris' inequality). The comparison must also be uniform: one set of prices must serve against every truthful mechanism, which requires an optimal mechanism to exist.
Needed infrastructure, reusable beyond this mission: Myerson's characterization of truthful single-parameter mechanisms and the revenue–virtual-surplus identity for densities on intervals, Harris' inequality for product measures, and the taxation principle for deterministic multi-parameter mechanisms. Contributions on any of these are welcome.
Many statistical procedures minimize an average observed loss. This treats two candidates with the same average as equally attractive even when one has much more variable losses across the sample. Adding a multiple of the empirical standard deviation can distinguish them, but the resulting objective need not be convex even when each individual loss is convex. Duchi and Namkoong study a distributionally robust alternative: they maximize expected loss over a small neighborhood of the empirical distribution, then minimize that worst-case value. Their paper identifies when this convex robust value agrees exactly with the mean-plus-standard-deviation expression and how far apart the two can be otherwise. The finite-sample statement is Theorem 1 of the pinned preprint.
The relation matters to someone choosing a loss function for stochastic optimization. The variance expression has a direct statistical interpretation, while the robust expression preserves convexity in a decision parameter when the loss is convex. Theorem 1 makes the relationship quantitative for a single bounded random variable, before the paper turns to uniform guarantees over whole classes of losses. This mission isolates that first step and its finite optimization model.
Take observed real values , with . Their empirical mean and empirical variance are
The variance uses , not the unbiased-estimator factor . A weight vector is feasible when its entries are nonnegative, sum to one, and satisfy
This is the paper's χ² neighborhood of the uniform empirical weights. Its robust sample expectation is
For a random variable with law supported on , write and . An independent sample supplies the vector . The paper describes through a -divergence from the empirical distribution, with ; its finite maximization problem (8) is the weight-vector form used here. The preprint, pp. 2 and 5–7 fixes these conventions.
For every sample in , the robust value lies between the empirical mean plus a corrected variance penalty and the full penalty:
This is inequality (10). The correction is explicit, so this target records more than an asymptotic approximation.
When and the sample size obeys
the goal is the high-probability equality
This is Theorem 1's equality (11) with the missing -dependent sample-size requirement supplied from the proof. The exact expansion is the mission goal; display (30), inequality (10), and Lemma A.2 form the milestone list, and the exact value under condition (9) is a further statement of the mission.
The deterministic result states how large the discrepancy between a convex robust risk and a variance penalty can be for any bounded sample. The equality says that, with the stated confidence, no discrepancy remains once the population variance and sample size make the penalty compatible with nonnegative probability weights. These are the numerical facts later sections need when they move from one loss variable to families of losses and minimizers. The claims and constants come from Theorem 1 and Section 2.1.
The paper develops arguments for these results, although its printed (11) needs the correction described below; the statements in this mission have no machine-checked proofs yet. The formalization work includes the finite χ² feasible set, its real supremum, exact handling of tied observations, empirical moments with the paper's normalization, and a product-law event for the probability estimate. The Samson concentration milestone is reusable for other bounded independent-coordinate models. Solvers can also contribute a different route to the corrected exact expansion; the goal concerns the statement, not one chosen argument.
Without the nonnegativity requirement on , optimizing a linear function over the centered Euclidean ball gives the mean plus a standard-deviation term. The candidate weights can become negative when a sample coordinate is far below the mean, so that calculation alone cannot certify the robust value. Condition (9) records precisely when the candidate is feasible. The probability target then needs a quantitative guarantee that the sample variance is large enough often enough, with the stated exponential constant. A pointwise inequality for a fixed sample does not by itself yield that probability estimate. These are separate obligations in Section 2.1 and Appendix A.
The sample is a function Fin n → ℝ; feasible weights have the same type. chiSqBall, robustSup, empMean, and empVar mirror equations (8) and the definitions on p. 6. Every theorem assumes and , so the weight ball is nonempty and its real supremum is bounded. The high-probability theorem uses a probability measure on the reals, supported on , and the independent product measure on Fin n → ℝ. Its conclusion bounds the measure of the event on which equality fails. The positive population variance hypothesis makes division by and meaningful. The deterministic bounds include every sample in the interval and use .
The paper prints the threshold without in (11), but its Appendix A invokes the corresponding inequality, and the printed claim fails for sufficiently large . The goal includes that term. The paper's route through Lemmas A.1 and A.4 contains misprinted lower-tail and moment claims, so those are not milestones. Lemma A.3's displayed (31b) is also omitted because its correction term has the wrong scaling; the corrected goal stands as a target to establish independently. These discrepancies are detailed in the local moderation notes and the pinned source, pp. 7 and 32–35.
No hypothesis may force the bad event to be empty, and the robust value must optimize over all feasible weights, not a selected optimizer. The supporting definitions are intended for reuse in later missions on uniform variance expansions. Contributions to the finite optimization facts, the concentration statement, and the probability goal are welcome.
Most physical supply chains hold stock at several levels: a factory warehouse feeds a regional depot, which feeds a retail outlet. Each level orders from the one above it, and a shortage upstream delays replenishment downstream. Optimizing such a multi-echelon system by dynamic programming looks hopeless, because the state is a vector of stock levels and stock in transit at every installation, and the value function of a two-installation system with a two-period shipping lag already depends on three continuous variables.
Andrew J. Clark and Herbert Scarf (Management Science 6(4):475–490, 1960) showed that for a serial system this curse of dimensionality disappears. Working with echelon stock (the stock at a level plus everything below it or in transit to a lower level), the optimal system cost separates into the cost of the lowest installation, optimized as if it stood alone, plus a function of echelon stock only. The result is the foundation of multi-echelon inventory theory: the echelon base-stock policies used in practice, the stationary analyses of Federgruen and Zipkin (1984) and Chen and Zheng (1994), and textbook treatments (Zipkin, Foundations of Inventory Management, 2000; Snyder and Shen, Fundamentals of Supply Chain Theory) all descend from it.
Timeline. Arrow, Harris and Marschak (1951) and Arrow, Karlin and Scarf (1958) set up periodic-review inventory models with discounted costs. Karlin and Scarf (1958) treated a single installation with a delivery lag, reducing it to a problem without lag (the paper's facts 1–3). Clark and Scarf (1960) proved the decomposition for serial systems with linear shipping costs and a setup cost permitted only at the top. Federgruen and Zipkin (1984) extended it to infinite horizons and Chen and Zheng (1994) gave a lower-bound proof that reaches more general structures.
Two installations are in series. Customer demand occurs only at installation 1; its demand in each period is non-negative with density on , independent across periods, and excess demand is backlogged. Installation 2 ships to installation 1 with a two-period lead time at unit cost . The system orders units from outside at cost for and (eq. (5)); these arrive at installation 2 one period later. Costs periods ahead are discounted by , .
The state at the start of a period is : is the stock on hand at installation 1, the stock that reaches installation 1 next period, and the echelon-2 stock (on hand at both installations plus in transit), so . Installation 1 pays the expected holding and shortage cost (1),
and echelon 2 pays a natural one-period cost (Assumption 3).
With periods remaining, the optimal system cost satisfies, with ,
where is installation 1's target (stock on hand plus in transit after shipping). Installation 1 in isolation, buying at unit cost with a two-period lag, has optimal cost , :
In Lean these are ClarkScarf.Serial.Model.sysCost and isoCost; the expressions in braces are sysObj and isoObj, indexed by for the problem with periods remaining.
There are functions with such that, for all and ,
and installation 1 acts optimally by aiming at an isolated-optimal target and taking , as much as installation 2 can supply. The goal fixes no form for and needs no critical numbers.
The result. Theorem 1 replaces one three-dimensional dynamic program by two one-dimensional ones. Installation 1 solves its own problem (15), whose solution is a critical-number policy, and echelon 2 solves a single-installation problem in with one-period cost . When is convex the augmented cost is convex (the paper remarks this for Expression (10)), so the echelon-2 policy is of type by Scarf's theorem, and the whole system runs on echelon base-stock rules. Every later serial-system result, finite or infinite horizon, uses this decomposition or its proof idea, and the "induced penalty" is the prototype of the penalty functions used in the multi-echelon literature.
Formalizing it. The theorem is classical and proved, but no machine-checked version exists. The published platform items on Clark–Scarf are a stationary single-period decomposition with normal demand and a disproved infinite-horizon base-stock recursion, neither of which is this finite-horizon dynamic program. A formal development produces the value functions (14)–(15) with real infima and set integrals, the measurability and integrability of value functions defined by infima, the convexity propagation through the recursion (7), and the decomposition itself, which are reusable for any finite-horizon inventory recursion with lead times.
The obvious induction on substitutes (16) into (14) and separates the minimizations over and . The separation is immediate; the hard step is that the constrained minimum over differs from the unconstrained one by an amount that a priori depends on . Showing that it depends on alone is the content of Theorem 1; nothing in the separation step itself rules out a dependence on . On the measure-theoretic side, every value function is defined by an infimum over an uncountable set and then integrated against . Its measurability and integrability are not automatic, and they must be established before any identity between integrals can be manipulated.
Everything lives in ClarkScarf.Serial, one definition file Def_ClarkScarf_Serial_Model and seven theorem files. Conventions committed to:
structure Model whose fields carry the data and the standing hypotheses: ; with ; and two additions the page leaves implicit, disclosed in each statement: a finite demand mean (otherwise (1) is infinite for ) and non-negative, continuous and of at most linear growth (Assumption 3 leaves unspecified; these make every expectation in (14) finite and measurable). No discount bound , no convexity of , no and no sign condition on is assumed.A formalization in which the feasible set of (14) is empty, in which the expectations are junk zeros of non-integrable integrands, or in which may depend on would make (16) trivial; the domain restriction, the integrability conditions and the order rule these out. A sorry-free check (not part of the mission) verifies and and exhibits a model with exponential demand satisfying all hypotheses.
Needed infrastructure: Fubini-type rearrangement of iterated set integrals against a density, integrability of functions of linear growth against a finite-mean density, convexity preserved under infimal projection and under convolution with a density, and measurability of infimum-defined functions. Contributions of these general lemmas, of the base cases , and of any milestone are welcome.
Routing and network optimization often require the length of the best route between every ordered pair of points. Robert W. Floyd's Algorithm 97 gives a compact procedure for this task: it receives a matrix of direct-link lengths and changes the matrix in place until each entry is meant to represent a shortest-path length. The procedure is a small historical source for an algorithm now used as a standard all-pairs shortest-path routine. Its published text consists of the ALGOL code and a short explanatory comment, without a correctness proof.
The same page contains Floyd's Algorithm 96, a Boolean procedure for ancestor relations. Its output records whether a chain of parent links connects two individuals. Floyd cites Warshall's theorem on Boolean matrices in both comments. The Boolean procedure and the length procedure use the same order of three loops; together they expose the distinction between discovering that a route exists and determining its best length. This mission formalizes both claims from Floyd's published page, with the shortest-path statement as its goal.
A directed network has numbered points. Its length matrix assigns a real number to a direct link from to . The value means that the direct link is absent. Links may have negative lengths, and the initial diagonal entries are unrestricted. The paper's matrix index range is ; the Lean development uses in the same order.
A path from to is a sequence with links. The points are distinct, as are . Thus a path between different points has no repeated point, while a path from a point to itself is a simple closed path with at least one link. Its length is ; a missing link gives length . Write for the minimum length among these paths, taking when there is no finite-length path. Since , this is a minimum over a finite family.
The no-negative-cycle condition says that every closed path has nonnegative length. Individual links can still be negative. This condition matters because, in a network with a negative cycle, repeated travel around that cycle can keep reducing a walk's length. Floyd's comment does not state the condition, although the claimed output needs it.
Algorithm 97 scans a pivot , then row , then column , each in increasing order. It enters the column scan when the current is finite; if the current is also finite, it computes and replaces when . Every replacement affects subsequent reads of the same matrix. Algorithm 96 makes the corresponding Boolean update: when and are true, it sets to true.
For Algorithm 96, let be the transitive closure of the initial parent relation , using chains of one or more links. Its comment asserts
For Algorithm 97, the separate unreachable-pair sentence asserts that, whenever no finite-length path runs from to ,
This second target needs no condition on cycle lengths. Both statements are milestones because they are claims printed in the two algorithm comments, rather than lemmas invented for the formalization.
The goal is the whole output claim of Algorithm 97. For every , every matrix with no negative cycle, and all points ,
The equality includes paths with negative individual links, diagonal entries, and unreachable pairs. It fixes the entire final matrix, rather than only an upper or lower bound.
The goal connects an explicit in-place matrix program with a route-based definition of shortest length. Once established, it permits later formal developments to use the procedure as a justified all-pairs distance computation, including networks whose individual links have negative lengths. The Boolean milestone similarly identifies the final state of an ancestor procedure with the transitive closure of the initial relation. Neither assertion requires treating an implementation's output as the definition of the mathematical answer.
Floyd's 1962 paper states these outcomes but supplies no proof. This mission supplies precise Lean statements and definitions for a proof to target. A completed machine-checked development would establish the published procedure's correctness under the missing necessary premise. The statements in this proposal are currently open theorem targets; compiling their declarations checks syntax and types, not their proofs. Supporting work on finite paths, cycle decompositions, and matrix updates can be reused in other finite directed-network arguments.
The array is changed in place. During a pivot's sweep, an entry used in a later update may already differ from its value at the start of that pivot. The test on is evaluated before the column loop, but the same entry is read again within every column iteration. A proof based only on a simultaneous, out-of-place matrix recurrence does not directly describe these reads. Negative individual links also prevent arguments that rely on every update decreasing only through a nonnegative segment. The no-negative-cycle condition must control what happens when a proposed route returns to a point already visited.
Points are Fin n, including the empty network at and the single-point network at . Lengths are WithTop ℝ, where ⊤ represents the paper's ₁₀10 sentinel as mathematical infinity. The paper's literal sentinel is ; a finite bound cannot represent arbitrarily long paths, so this mission uses infinity in its goal. The ALGOL real operations are represented by exact real arithmetic. The printed procedure's loop order, strict comparison, two finiteness guards, and immediate assignments are part of the Lean definition.
The initial diagonal is not normalized. Therefore a path from to itself has at least one link, and the final diagonal denotes a shortest closed-path length when one exists. The Boolean comment's “is true if” is read as an equivalence, supported by its following explanation of the final matrix; chains have one or more links, matching Lean's Relation.TransGen.
The sole added hypothesis in the main goal is absence of negative cycles. It is necessary: with one point and self-link length , the procedure changes that entry to , although the shortest simple closed path has length . No nonnegative-link or zero-diagonal premise is imposed. The unreachable-pair milestone omits the cycle hypothesis because its claim holds without it. The benchmark is a finite minimum of summed link lengths, defined independently of Algorithm 97; defining it from the procedure or its recurrence would empty the goal of its intended content. Contributions proving the printed algorithms' statements, or establishing reusable finite-path and update results needed for them, fit this scope.
Long-running projects such as construction, plant engineering or software development involve payments to and from the contractor at many points in time: disbursements when activities are carried out, progress payments when milestones are reached. When the planning horizon is long, money received later is worth less, and the natural financial objective is the net present value of all cash flows. Scheduling a project to maximize its net present value subject to minimum and maximum time lags was studied by Russell (1970) and Grinold (1972), and the problem is the prototype of a nonregular objective: delaying an activity can be profitable, because disbursements lose value when they are postponed.
This mission follows Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). The book shows that the net present value objective belongs to the class of binary-monotone objective functions (§3.3.5), and it uses this in §3.9.1 to give a combinatorial optimality criterion for the resource-free problem: a vertex schedule is optimal exactly when the subprojects cut off by the arcs of a spanning tree have net present values of the right sign (Proposition 3.9.2). That criterion drives the book's parametric analysis of the net present value as a function of the discount rate and the deadline.
A project consists of activities , , where is the project beginning and the project completion. Activity has an integer duration , with and otherwise. Temporal constraints are the arcs of a project network : an arc with integer weight requires for the start times . A maximum project duration is the arc with weight . The time-feasible region is
Let be the discount rate ( for an interest rate ) and the cash flow of activity , paid at its completion time . The problem (3.9.1) is
and a minimizer is a time-optimal schedule. A vertex of is an extreme point. A spanning tree is associated with if , has arcs and a connected underlying undirected graph, and is the unique solution of , for . Deleting a tree arc splits into two subtrees; is the node set of the one not containing . The arc is forward if the tree path from passes it from to and backward otherwise, and
is the net present value of the subproject . Finally, is binary-monotone if it is monotone on every line with direction (Definition 3.3.2).
Assume every node is reached from by a path of nonnegative length (the standing convention of §1.2) and let be a vertex of .
The book states "if and only if … for each arc of the corresponding spanning tree", where the corresponding tree is chosen using optimality. The two directions above are the reading that makes the statement well defined: sufficiency for every associated tree, necessity for some associated tree.
Proposition 3.9.2 turns a nonconvex continuous optimization problem into a finite check on a spanning tree. Read as an economic statement, it says that at an optimal schedule no subproject with positive net present value can be started earlier and no subproject with negative net present value can be postponed. The book builds on it the parametric procedure of §3.9.1, which tracks the optimal tree as the discount rate or the deadline varies (Propositions 3.9.3 and 3.9.4), and the steepest descent method of §3.5.2 terminates exactly when the criterion holds.
The results are proved in the book, partly by reference to network optimization (Ahuja et al., 1993) and to Schwindt and Zimmermann (2001, 2002). None of them is formalized on the platform or, as far as is known, anywhere else. A formal proof would give the first machine-checked optimality certificate for a nonregular project scheduling objective, and the spanning-tree description of vertices (Proposition 3.2.16) is shared with Mission VI of this series.
The objective is neither convex nor concave when cash flows of both signs occur, so local optimality at a vertex does not imply global optimality by a convexity argument, and a first-order check along the edges of is not obviously enough. The criterion is also not a statement about one tree: a degenerate vertex, where more than temporal constraints are binding, has several associated trees, and the sign conditions may hold on some and fail on others. Necessity therefore requires producing a suitable tree, not checking a given one. Finally, the combinatorial objects (the subtree , forward and backward orientation relative to the root) have to be connected to the geometry of through Proposition 3.2.16, whose proof in the book is a citation.
Activities are Fin (n + 2) with 0 the project beginning and Fin.last (n+1) the project completion; start times are real; durations are natural numbers and arc weights integers. The deadline is a structure field together with the backward arc of weight . is Real.rpow, and every statement assumes as the book does (p. 203). Vertices are Set.extremePoints ℝ. A spanning tree is a Finset of arcs whose SimpleGraph.fromRel is connected; is the set of nodes not reachable from once the arc is deleted.
Three readings are committed and disclosed in the item statements. Necessity is stated only for : at the objective is constant, every schedule is optimal, and the sign conditions can fail on every tree. The standing convention of §1.2 (a path of nonnegative length from to every node) is a hypothesis of Proposition 3.2.16 and of the goal; without it a vertex can be fixed by rather than by arcs of , and necessity fails. The existence of an optimal vertex assumes nonempty and bounded, which the book asserts in §3.1. Chapter 3's resource constraints do not occur in this mission, which concerns only.
The goal cannot be discharged by choosing the tree freely: associated trees must consist of arcs of that are binding at and determine uniquely, and sufficiency must hold for every such tree. Contributions welcome beyond the milestones: a proof of Proposition 3.2.16 reusable by Mission VI, and a general lemma relating binding spanning trees of difference constraints to extreme points.
Semidefinite programs (SDPs) arise as convex relaxations of combinatorial problems such as maximum cut and the Lovász theta function, and in control and eigenvalue optimization. Interior-point methods solve them reliably but manipulate dense matrices, which limits the size of the instances they can handle. Burer and Monteiro (Math. Program. 95 (2003)) proposed replacing the matrix variable by a factorization with having only columns, and solving the resulting nonconvex program by a first-order augmented Lagrangian method. The approach rests on a theorem of Barvinok (1995) and Pataki (1998): an SDP with linear constraints has an optimal solution of rank with , so a small number of columns suffices.
Because the factorized problem is nonconvex, a local minimum it returns is not automatically a solution of the SDP. Section 2 of the paper gives conditions under which it is. This mission formalizes those conditions, culminating in Proposition 2.5, which justifies the paper's strategy of increasing the rank one column at a time.
For real matrices, the trace inner product is . The data are symmetric matrices and a vector . The primal SDP and dual SDP are
The standing assumptions of the paper are that are linearly independent and that there are feasible and with .
For a positive integer , the low-rank program is
Its Lagrangian is , and . A feasible is a local minimum if it minimizes the objective among nearby feasible points; it is a regular point if are linearly independent; it is a stationary point with multiplier if . The injection of is , obtained by appending a zero column.
Let and let be a regular local minimum of with multiplier , , . If is a local minimum of , then
Proposition 2.5 is a certificate of global optimality for a nonconvex problem obtained from local information alone. It is the basis of the rank-increase scheme described on p. 8 of the paper: compute a local minimum of for a small ; if the zero-column extension is still a local minimum of , the current point solves the SDP; otherwise a better point of exists and is increased. Proposition 2.4 gives the companion test, valid for every : positive semidefiniteness of the multiplier matrix at a stationary point. These statements underlie the later convergence analysis of the method (Burer & Monteiro 2005) and the literature on benign landscapes of low-rank SDP formulations (Boumal, Voroninski & Bandeira 2016).
The results are proved in the paper. What this mission adds is a machine-checked version of the full chain from the standard-form SDP to the rank-increase certificate, including the matrix calculus (9), the first- and second-order necessary conditions for an equality-constrained program over rectangular matrices, and SDP complementary slackness in standard form. No machine-checked proof of these results is recorded in Mathlib or on the platform.
The SDP side (Propositions 2.1 and 2.4) is linear algebra: weak duality and the fact that the trace inner product of two positive semidefinite matrices is nonnegative. The substance lies in Proposition 2.3. The feasible set of is a variety cut out by quadratic equations, and the multiplier rule and, especially, the second-order necessary condition require a constraint qualification and a curve in the feasible set realizing every tangent direction. Mathlib provides a first-order Lagrange multiplier rule, but not the second-order condition on the tangent space. A naive attempt to read Proposition 2.5 off Proposition 2.4 fails: local minimality of alone does not make positive semidefinite (when is below the minimal optimal rank, it is not); the hypothesis on is indispensable.
Matrices are Matrix (Fin n) (Fin r) ℝ with 0-based indices. The trace inner product is frob A B = trace(Aᵀ * B), defined for rectangular matrices. The data carry explicit symmetry hypotheses C.IsSymm and (A i).IsSymm; without them the formulas (9) are false. Primal feasibility uses Mathlib's PosSemidef, which over includes symmetry. Optimality for (1) and (3) is defined relative to their entire feasible sets. The standing assumptions are a separate predicate carried as a hypothesis by Propositions 2.1, 2.3, 2.4 and 2.5, and every statement about carries and (or ). Gradients are Fréchet derivatives under the Frobenius norm, identified with matrices through the trace inner product; local minima use IsLocalMinOn on the feasible set of together with feasibility. The injection appends the zero column as the last column.
The statement admits several trivializing encodings, all excluded here: optimality defined relative to the factorized feasible set instead of the whole SDP, an empty or unconstrained (an unconstrained local minimum or a local minimum without feasibility), a stationarity notion that already includes , and an injection other than the zero-column extension.
A complete development needs the matrix calculus of , a second-order necessary optimality condition under linear independence of the constraint gradients, and standard-form SDP weak duality and complementary slackness; all of these are reusable well beyond this mission. Proofs of individual milestones, in particular the derivative formulas and Proposition 2.4, are welcome independently of the goal.
In many sequential decision problems the learner sees side information before acting. A news site chooses an article for a visitor whose history and location it knows; an ad server chooses an advertisement for a query. Only the reward of the chosen action is observed. These are contextual bandit problems, and Chapter 4 of Bubeck and Cesa-Bianchi's monograph Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems (arXiv:1204.5721v2) surveys several of their formal versions. In a contextual problem the learner is compared with the best policy, a map from contexts to arms, rather than with the best single arm.
This mission covers three of the chapter's models. The first marks each round with a context from a finite set. In the second, experts give advice, as in prediction with expert advice. The third is the bandit multiclass problem: a linear classifier predicts one of labels and then learns only whether its prediction was right. The goal is the mistake bound of the Banditron (Kakade, Shalev-Shwartz and Tewari, ICML 2008). The bound shows that one bit of feedback per round suffices to compete with every linear classifier, at regret .
There are arms (or labels) and rounds .
Adversarial losses. At round an adversary assigns losses to the arms and may adapt to the forecaster's past plays . The forecaster draws at random from a distribution that depends on what it has observed, and it observes only . Expectations are over the forecaster's draws.
Side information. Each round carries a context from a finite set , and the sequence is fixed in advance. The pseudo-regret against context-to-arm maps is
The S-Exp3 forecaster runs one instance of Exp3 (Section 3.1 of the book) on each context.
Expert advice. At each round each of experts proposes a distribution over arms, which may depend on the forecaster's past plays. The contextual pseudo-regret is
Exp4 (Fig. 4.1) runs exponential weights over the experts with importance-weighted loss estimates.
Bandit multiclass. The examples are fixed in advance, with (Euclidean). A matrix classifies by . Its multiclass hinge loss on round is . Write for the cumulative hinge loss, for its average, and for the Frobenius norm. The multiclass Perceptron predicts and, after seeing , adds to row and subtracts it from row . The Banditron (p. 58) predicts from . It observes only and updates , where . Its number of mistakes is .
For , , every example sequence as above and every matrix ,
Theorem 4.7 shows that, on any sequence of examples, the bandit version of online multiclass classification costs at most mistakes beyond the hinge loss of the best linear classifier. The full-information Perceptron, by comparison, pays . The bound has no stochastic assumption and has explicit constants. Theorems 4.1–4.3 are the basic regret guarantees for side information and expert advice. Theorem 4.3 in particular lets learning algorithms serve as experts inside Exp4, which is the construction behind Theorem 4.5.
The mission produces machine-checked statements, and eventually proofs, of these results with fully explicit constants and an explicit model of adaptive adversaries and adaptive advice. To the curators' knowledge none of the Banditron, the multiclass Perceptron bound, S-Exp3 or Theorem 4.3 is formalized anywhere. The platform's Bandit Algorithms series has a proved Exp4 bound, but only for advice and rewards fixed in advance. The book proves all four milestones and the goal; two printed statements (4.2 and 4.3) contain misprints that this mission corrects.
The Banditron bound concerns a randomized process whose weight matrix depends on all earlier random predictions. The Perceptron argument tracks and . It carries over only in conditional expectation, and the second moment of the importance-weighted update is of order on rounds where and of order otherwise. Combining these into one inequality for and then for requires solving a quadratic inequality in the presence of expectations, and the constants must come out as printed. For the Exp3/Exp4 results, the obstacle is that losses and advice adapt to past plays. The standard potential argument has to be run conditionally on the history, and a version that fixes the losses in advance proves a weaker theorem.
Fin K. The law of the first plays is the product over sequences , and expectations are finite sums against it. The adversary and the experts are deterministic functions of past plays; an independent randomized adversary is a mixture of these. The examples of the Banditron are fixed.Useful reusable infrastructure: the path-law expectation for history-dependent sampling, the exponential-weights potential argument under adaptive losses, and Perceptron-type inner-product arguments for matrices. Proofs of any milestone and of the goal are welcome.
Many controlled systems are judged by a ratio of two long-run quantities rather than by a single one: cost per unit of output, cost per unit of time when the time spent in a state depends on the decision, cost per customer served, or expected cost per cycle of a renewal process. In a finite Markov decision model each of these is a quotient of two average costs per unit time. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (DOI 10.1287/mnsc.9.1.16) introduced this ratio-of-costs criterion in its §4, prompted by the fractional linear program that its §3 uses to solve the total-cost problem as a linear program, and pointed to Klein's work on maintenance policies as an example of the problem.
The paper's §4 first observes that, restricted to stationary randomized procedures, the ratio criterion is a ratio of two linear functions of the stationary state-decision frequencies, so it can be minimized by the fractional linear programming lemma of §3. The question it then raises is the one this mission formalizes: is the procedure optimal over stationary procedures also optimal over all procedures, including history-dependent and randomized ones? Derman's Theorem 3 answers yes under an irreducibility assumption, by reducing the ratio problem to a family of ordinary average-cost problems with costs of either sign.
Timeline, as far as it bears on this mission:
A system is observed at times in one of finitely many states . After each observation one of the decisions is made, all of them available in every state. If the system is in state and decision is made, the next state is with probability , where .
A procedure chooses the decision at time at random, with probabilities that may depend on the whole past; the class of all procedures is . The class consists of the stationary randomized procedures, for which the probability of in state is a fixed number , whatever the past and the time. The class consists of the deterministic stationary procedures, those of with every ; it is finite. A procedure of turns the states into a Markov chain with transition probabilities .
Let and be two sets of costs incurred when decision is made in state . For a fixed procedure started at , let and be the expected costs at time . The ratio criterion is
For a single cost set with expected costs , the average cost per unit time is .
Assumption A says that for every procedure of all states belong to the same class of the induced Markov chain.
Under Assumption A, for every initial state there is a deterministic stationary procedure with
that is, for every procedure .
Theorem 3 justifies solving ratio problems over stationary procedures only. Combined with the display of milestone 4 it shows that the fractional linear program over stationary state-decision frequencies yields a procedure optimal against every procedure, including those that remember the past or randomize. The same reduction, minimizing and adjusting , underlies later parametric methods for fractional Markov decision problems and the analysis of semi-Markov decision processes, where the denominator is the expected sojourn time.
All four steps and the theorem are classical and proved on paper. None of them is formalized on Prove2Me: the platform has average-cost optimality statements with nonnegative costs (Sennott's Proposition 6.2.3) and Jewell's gain-rate results restricted to stationary policies, but no statement of a ratio criterion over history-dependent procedures. This mission produces the statement of Theorem 3, the signed-cost version of Theorem 1 that it uses, and the two translation steps between the ratio criterion and the average-cost criterion.
The obvious argument restricts to stationary procedures, where all Cesàro limits exist and the ratio criterion is a ratio of two linear functionals of a stationary distribution. It says nothing about a history-dependent procedure, whose averages and need not converge, and for which the limit superior of the ratio is not the ratio of the limits superior. The translation from the ratio to an average cost therefore works in one direction for every procedure (milestone 2) and in the other direction only for stationary ones (milestone 3). The other ingredient, optimality of a deterministic stationary procedure for the average-cost criterion against all procedures with costs of either sign (milestone 1), is the substance of Derman's Theorem 1 and requires a vanishing-discount or equivalent argument over history-dependent procedures.
The dynamics and the procedures come from the published definitions SennottDP_AvgFinite_Model: the system is an MDC S Act with [Fintype S] [Fintype Act] and the hypothesis ∀ s, M.A s = Finset.univ (all decisions available); the class is Policy M, history-dependent and randomized; is StationaryPolicy M through .toPolicy; the law of the history is histProb. The cost field M.C of that structure plays no role: the costs , and the signed cost of milestone 1 are explicit real arguments S → Act → ℝ.
The local definitions are: the expected cost at time for a real cost, as a finite sum over histories of length ; with Derman's normalization ( terms divided by ); as the limit superior of the ratio of partial sums; the induced matrix ; Assumption A as Matrix.IsIrreducible of for every row-stochastic ; and membership of a procedure in with probabilities . All limits superior are real, of bounded sequences; positivity of and is a hypothesis of every statement involving , which keeps the denominators positive.
The goal quantifies "for every initial state there is ", following the proof. The competitors in the goal and in milestone 1 range over all of Policy M; a version comparing only with stationary procedures is a different and easier theorem and does not close this mission. Assumption A is kept in the goal although the proof does not visibly use it, because the theorem states it.
Contributions welcome: proofs of the milestones, in particular the signed-cost Theorem 1 (which may reduce to Sennott's Proposition 6.2.3 by shifting costs by a constant), Cesàro limits for stationary procedures on finite chains (reusable for milestones 3 and 4), and the final compactness argument over the finite class .
Resource-constrained project scheduling asks for start times of the activities of a project that respect precedence-type time lags and the capacities of renewable resources (machines, crews, equipment). Classical project scheduling minimizes the project duration, a regular objective: delaying an activity never helps. Many objectives met in practice are not regular. The resource investment problem minimizes the cost of the resource capacities that must be procured; resource levelling problems minimize fluctuations of resource usage over time; the resource renting problem trades fixed procurement against time-dependent renting costs; net present value and earliness–tardiness objectives reward late as well as early starts. For such objectives the familiar fact that "some active schedule is optimal" fails, and algorithms need another finite set of candidate schedules that is guaranteed to contain an optimum.
Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2), organizes the objective functions of project scheduling into seven classes and pairs each class with a class of schedules that contains an optimal schedule. This mission formalizes §3.3 of that chapter. The classification goes back to Neumann, Nübel and Schwindt (2000) and Zimmermann (2001); the two locally defined classes, and the matching schedule classes of quasiactive and quasistable schedules, are the book's device for covering discontinuous resource-based objectives.
A project consists of activities , , where and are fictitious activities marking the project beginning and completion. Activity has an integer duration (, otherwise). The project network has an arc set with integer weights ; a schedule is a vector of real start times with , , and it is time-feasible if for all . A maximum project duration is prescribed through a backward arc of weight , so . Each renewable resource has capacity , activity uses units while in progress, and is the total usage at time . The feasible region consists of the time-feasible schedules with for all and .
For an objective function , problem asks for an optimal schedule: some with for all .
A schedule induces the strict order of precedences it realizes. The equal-order set of is
a polytope with part of its boundary removed. The distinct equal-order sets partition into finitely many pieces.
Schedule classes are defined through shifts. A shift from a feasible to a feasible is order-preserving if ; it is a left-shift if . Two shifts from to and are opposite if with . A feasible schedule is active if no feasible left-shift exists, quasiactive if no order-preserving left-shift exists, stable if no pair of opposite shifts to feasible schedules exists, and quasistable if no pair of opposite order-preserving shifts exists.
Objective classes: is regular if implies ; quasiconcave on a set if for , ; lower semicontinuous if on . Then is locally regular (class 6) if it is lower semicontinuous and regular on every equal-order set , , and locally quasiconcave (class 7) if it is lower semicontinuous and quasiconcave on every such set.
For every locally quasiconcave ,
Quasiactive and quasistable schedules are finite in number: they are the minimal points and the vertices of the finitely many schedule polytopes. Theorem 3.3.13 therefore turns the minimization of any locally quasiconcave objective over a disconnected, non-convex feasible region into a finite search. Class 7 contains the resource levelling objectives and , the total variation of the resource profiles, and the resource renting objective (Propositions 3.3.10 and 3.3.12, and Nübel 2001). The enumeration schemes and decision sets of §3.5–3.7 rest on this result, and Theorem 3.3.9 plays the same role for class 6 (resource investment, changeover times).
The results are proved in the book and the cited papers. As far as a search of the platform shows, none of them, and none of the schedule classes, has a machine-checked formalization; Mathlib supplies lower semicontinuity and quasiconcavity but nothing about schedules. The mission produces a checked version of the classification theorems in the book's exact generality: general time lags (cycles in the network allowed), real start times, and arbitrary objectives given only by their class.
The optimum need not exist a priori: objectives of classes 6 and 7 are discontinuous, and the feasible region is a finite union of polytopes that is in general disconnected. Existence of a minimizer needs compactness of (which depends on the deadline arc and the network's path structure) together with lower semicontinuity.
The main obstacle is that the objective is only controlled piecewise. Quasiconcavity holds on each equal-order set separately, and an equal-order set is not closed: a schedule polytope also contains schedules inducing strictly larger orders, where the hypothesis on says nothing about its relation to the values on . The obvious argument, taking an optimal schedule and invoking quasiconcavity along the segment of a pair of opposite order-preserving shifts, only relates at points of one equal-order set, and it does not by itself produce a schedule that admits no such pair at all. The same issue arises for Theorem 3.3.9 with order-preserving left-shifts, which may cross from one equal-order set into another.
Activities are Fin (n + 2), with 0 and Fin.last (n + 1) fictitious. Start times are real; objective functions are total functions (Fin (n + 2) → ℝ) → ℝ whose regularity, quasiconcavity and lower semicontinuity are required only on the nonnegative orthant (lower semicontinuity is Mathlib's LowerSemicontinuousOn on the orthant). The deadline is the network's backward arc, as in §3.1. The project structure records the book's standing property (p. 8) that from each node there is a path to of length at least ; this bounds every activity by . The resource constraints are imposed for all , which under that property is the book's . The peak in the resource investment objective is a supremum in over of a nonempty finite set, hence attained.
"Optimal" always means minimizing over the whole feasible region , and the theorems quantify over every function in the class; a formalization with a fixed objective, or with optimality over a single polytope or a single equal-order set, would be a different and weaker statement. The schedule classes are defined through shifts, never as minimal or extreme points, so no statement is true by definition. The only hypothesis besides the class of is .
The mission restates locally the project model, the induced orders and the shift classes also drafted by the companion missions on schedule classes of this series. Useful contributions beyond the milestones: compactness of and closedness of the schedule polytopes, the representation of as a finite union of feasible order polytopes, and the finiteness of the sets of quasiactive and quasistable schedules.
In bandit convex optimization a forecaster repeatedly picks a point of a convex set , and an adversary picks a convex loss . The forecaster pays and observes only that number: it never sees the function, its gradient, or its value elsewhere. This is the model of online optimization with only function-value access, as in tuning a system online from measured costs, dynamic pricing with an unknown convex demand-cost curve, or routing with path costs observed only on the route taken. The question is how fast the forecaster can approach the best fixed point in hindsight.
Chapter 6 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2, Foundations and Trends in Machine Learning 5(1), 2012) treats the problem through spherical gradient estimates fed to projected gradient descent. The one-point method is due to Flaxman, Kalai and McMahan (SODA 2005, arXiv:cs/0408007), who obtained an regret bound. Agarwal, Dekel and Xiao (COLT 2010) showed that two function evaluations per round allow . Whether one-point feedback admits regret was open when the monograph was written (p. 94); Bubeck, Eldan and Lee (STOC 2017, arXiv:1607.03084) later obtained regret up to logarithmic and polynomial-in- factors for convex losses, with a different and much more involved algorithm.
Let be the closed Euclidean unit ball and the unit sphere, with unnormalized spherical measure , so that . Fix . For a loss , the smoothed loss is with uniform on .
The set is closed and convex with . The losses are -Lipschitz, differentiable and convex, and are fixed before the game (an oblivious adversary).
OSGD (Online Stochastic Gradient Descent) on a set with learning rate starts at and sets , where is a gradient estimate. With independent and uniform on :
OSGD runs on the shrunken set , so that the perturbed points stay in . The pseudo-regret is
If in addition on , and , , then one-point OSGD satisfies
The bound shows that a single function value per round suffices for sublinear regret against any oblivious sequence of Lipschitz convex losses, with a forecaster whose only operations are a random perturbation and a Euclidean projection. The smoothing identity of Lemmas 6.1–6.2 is the basic tool of zeroth-order (derivative-free) optimization, used well beyond bandits, and Theorem 6.1 is the benchmark for two-point methods.
All results are proved in the source. To the best of current knowledge none is formalized: the related items of the Introduction to Online Convex Optimization series on Prove2Me (Hazan's Lemma 6.7 and Theorem 6.9) were formalized with missing hypotheses and are recorded as disproved. This mission produces machine-checked statements with every hypothesis explicit, and the formal infrastructure (sphere measure calculus, a projected stochastic gradient analysis) for later zeroth-order results.
Two steps resist a direct formal treatment. First, Lemma 6.1 is a divergence-theorem identity on the ball; Mathlib has the sphere measure and polar coordinates, but its divergence theorem covers boxes rather than balls, so differentiating the ball average in requires either such a theorem or a direct argument about translates of the ball. Second, the regret analysis takes expectations of quantities that depend on the whole past: the iterate is a function of , and unbiasedness holds only conditionally, via independence of from the past. A pathwise gradient-descent inequality must be combined with this conditional expectation round by round, with measurability of the projected iterates established along the way. The naive approach of treating the estimate as the true gradient of fails: it is a gradient of , and the gap is handled only by Eq. (6.2) and Lemma 6.3.
Points are in EuclideanSpace ℝ (Fin d) with ; rounds are , sums run over Finset.Icc 1 n. is Mathlib's Measure.toSphere of Lebesgue measure; the uniform laws are normalized restrictions. Randomness lives on an arbitrary probability space; the directions are measurable, mutually independent (iIndepFun) and uniform on , and in Theorem 6.1 the pairs are independent with a fair sign independent of . A run of OSGD is a predicate (start at , each iterate a Euclidean projection onto ), which determines the run uniquely, so the forecaster uses only observed values and its own randomness. The losses are Lipschitz, differentiable and convex on all of ; the bound is on , because a convex function bounded on is constant. The minimum over is an infimum over the subtype , attained in every theorem.
Conventions and corrections, each stated in the item's Formalization Note:
The statements cannot be satisfied trivially: the run is pinned by its recursion, the losses are fixed before the randomness, the expectations are of bounded measurable functions (no zero-valued Bochner integrals), and the minimum is over the nonempty compact . Section 6.3 (Lemma 6.4, Theorem 6.3) is not included, because its algorithm box and proof use different stage lengths and its unimodality condition is stated on a smaller set than the proof uses.
Needed infrastructure: calculus of ball averages and sphere integrals, symmetry of the uniform sphere law, nonexpansiveness of projections onto closed convex sets, and conditional-expectation bookkeeping for adapted iterates. Each is reusable for zeroth-order optimization; contributions of any of them as separate lemmas are welcome.
Classifiers trained on images, speech and text can be made to change their prediction by perturbations of the input that are tiny in norm (Szegedy et al., 2014). Empirical defences against such adversarial examples have repeatedly been broken by stronger attacks (Athalye, Carlini, Wagner, 2018), which motivates certified defences: classifiers that come with a proof that their prediction at a given input cannot change inside a stated ball around it.
Randomized smoothing turns any classifier, however large or opaque, into one with such a certificate in the norm. It was introduced with weaker radii by Lecuyer et al. (2019) and Li et al. (2018). Cohen, Rosenfeld and Kolter (arXiv:1902.02918v2, ICML 2019) proved the radius that is now standard, and showed it cannot be enlarged. Their guarantee underlies most later work on certified robustness, including Salman et al. (2019).
This mission formalizes the robustness guarantee, Theorem 1 of that paper. Page numbers below are PDF pages of the arXiv v2 preprint, which has no printed page numbers.
Inputs are points of with the Euclidean norm and inner product . Classes form a set . A base classifier is a deterministic or random function . A random is described by the probabilities , which for each form a probability distribution on .
Fix a noise level and let be isotropic Gaussian noise. The class probabilities at are , and the smoothed classifier is
The paper leaves undefined when the maximizer is not unique. "" therefore means that every class other than has strictly smaller probability.
Write for the standard Gaussian cumulative distribution function and for its inverse. is a real number on , and , .
Suppose that at a specific there are a class and numbers with
Then for every with , where
The statement covers every base classifier and every set of classes. The radius is infinite when or .
The milestones are the paper's own steps, in attack order:
Theorem 1 turns three numbers at one input into a guarantee over a whole ball: a lower bound on the top-class probability, an upper bound on the other classes, and the noise level. These bounds can be estimated by sampling and certified with confidence intervals (the paper's CERTIFY procedure). That is what lets randomized smoothing certify ImageNet-scale networks, where exact verification methods do not scale. The companion result (Theorem 2, a separate mission of this series) shows that no larger ball can be certified from the same information.
The theorem has a short pen-and-paper proof; no machine-checked proof of it is recorded on Prove2Me. A formal development adds:
Every step is classical, so the difficulty lies in the missing infrastructure, not in the idea.
EuclideanSpace ℝ (Fin d). is the pushforward of Mathlib's stdGaussian under , with a hypothesis.f : ℝᵈ → PMF 𝒴 with measurable class probabilities; deterministic classifiers are point masses. is an arbitrary type, with no finiteness assumed. The class probability is the published Gaussian smoothing RandomGradFree.Shared.smoothing, applied to .Contributions are welcome at every level: proofs of the milestones, and general lemmas such as the Gaussian density, the law of linear functionals of a Gaussian vector and properties of the normal quantile. These lemmas are reusable well beyond this mission.
Exact and heuristic methods for resource-constrained project scheduling do not search the whole continuum of start-time vectors. They enumerate a finite candidate set that is guaranteed to contain an optimal schedule. For machine scheduling and precedence-only project scheduling the classical candidate sets (semiactive and active schedules) are defined by shifting single activities earlier. With general time lags — minimum and maximum delays between the starts of activities — several activities can be rigidly tied together, and single-activity shifts no longer describe the right candidate sets.
Neumann, Nübel and Schwindt (Neumann et al. 2000) introduced shifts of sets of activities and four resulting classes of schedules: active, semiactive, pseudoactive and quasiactive. Section 2.4 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (Springer 2003), characterizes each class geometrically as the minimal points of a subset of the feasible region. The branch-and-bound procedures of §2.5 of the book enumerate exactly these objects: each enumeration node is a strict order together with the minimal point of its order polyhedron.
A project has activities ; and are fictitious activities marking the project beginning and completion, and are the real activities. Activity has an integer duration , with and otherwise. Time lags are the arcs of the project network with integer weights . A schedule is a vector of real start times with and . It is time-feasible if for all ; these schedules form the polyhedron .
There are renewable resources with capacity ; activity uses units while it is in progress. With the active set , a schedule is resource-feasible if for every and every . The feasible region is . It is in general neither convex nor connected.
A schedule induces the strict order . For a strict order , the order polyhedron is . is feasible if . is the schedule polyhedron of .
A left-shift from to means componentwise and . For feasible , the shift is global; it is local if a continuous trajectory joins to ; it is order-preserving if and order-monotone if or . A feasible schedule is active, semiactive, pseudoactive or quasiactive if no global, local, order-monotone or order-preserving left-shift, respectively, starts at it. A minimal point of is a point such that no satisfies , .
For a feasible schedule :
Part (a) is close to a restatement of the definitions. The content lies in (b), which passes from trajectories to connected components; in (c), which replaces a condition on shifts by a condition on finitely many polyhedra; and in (d), which reduces quasiactivity to a single polyhedron.
The characterization makes each schedule class checkable and enumerable. By (d), deciding quasiactivity is a longest-path computation in the schedule network. Deciding activeness is NP-hard (Neumann et al. 2000); the same holds for semiactive and pseudoactive schedules, which is why exact algorithms enumerate the quasiactive schedules. Remark 2.4.10 and Proposition 2.10.2 then give the two facts every such algorithm relies on: an optimal schedule lies among the (integer-valued) quasiactive schedules, and all of them fit into the horizon . Regular objective functions other than the project duration (§2.10) inherit the same candidate sets.
On the formal side, the mission produces a reusable model of with real start times and general time lags: time-feasible and resource-feasible schedules, schedule-induced orders, order polyhedra and the four schedule classes. No part of this material is formalized on Prove2Me or, as far as is known, anywhere else. The results are all proved in the literature (Neumann et al. 2000; the book gives proofs or calls them obvious); the work here is to formalize them.
The obvious argument for (b) says "a trajectory stays in one component, so local shifts move within components". The converse needs that two schedules in the same connected component of are joined by a path inside . That is false for general sets and has to come from the structure of as a finite union of order polyhedra (the basic structural theorem of Bartusch, Möhring and Radermacher), which is not part of this mission's statements and must be proved on the way.
For (c), the difficulty is that an order-monotone shift may shrink the order . The proof has to produce, from a feasible sub-order whose polyhedron has a smaller minimal point, a shift that is short enough to keep every overlap of . This requires the resource feasibility of whole order polyhedra, i.e. that for feasible . Resource feasibility is a condition on all times , while the orders only record pairwise relations between activities.
Activities are Fin (n + 2), with 0 and Fin.last (n + 1) the fictitious ones. Durations are natural numbers, arc weights integers, and start times real. Resource requirements and capacities are natural numbers. The resource constraints hold for every ; (2.1.4) writes , but the book's proofs use the unrestricted form. Minimal points are Mathlib's Minimal for the componentwise order on Fin (n + 2) → ℝ. Components in (b) are connected components (connectedComponentIn), while local shifts are defined by continuous trajectories from the unit interval, as in Definition 2.4.3. The theorem is stated for feasible , since the schedule classes consist of feasible schedules by definition. The lower bound is a vector of real infima and is used only for nonempty order polyhedra.
Defining "active" as "minimal point of ", or any class through its right-hand side, would make the goal trivial. That is ruled out: every class is defined through the shifts of Definitions 2.4.1–2.4.6, including the trajectory condition and the orders .
Remark 2.4.8 (the minimal point of is the vector of longest path lengths in ) is not stated, since it needs path lengths and the reachability conventions of Remarks 1.1.2. Contributions of that network layer, and of the structural theorem (Theorem 2.3.7), are welcome as supporting lemmas.
For a real-analytic function on an open set and a critical point (so ), the Łojasiewicz gradient inequality says that there is an exponent such that stays bounded near . It is the standard tool for proving that bounded gradient trajectories have finite length and converge to a single critical point, and, in its descendants (the Kurdyka–Łojasiewicz property), for proving convergence of the whole iterate sequence of nonconvex descent methods: proximal gradient, alternating minimization, PALM, ADMM. Those algorithmic results all assume a nonsmooth version of the inequality, for functions that may take the value and are not differentiable.
Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007)) supplied that nonsmooth version. This mission formalizes their first main result, Theorem 3.1: the inequality at critical points of subanalytic functions that are continuous on a closed domain.
Timeline.
Write with its Euclidean norm. A function has domain .
Subanalytic sets (Definition 2.1). A set is semianalytic if every point of has a neighbourhood on which with real-analytic on . It is subanalytic if every point of has a neighbourhood such that is the projection onto of a bounded semianalytic subset of , . A function is subanalytic if its graph is subanalytic. Semialgebraic functions, and functions locally built from analytic ones by finitely many algebraic operations, max/min and compositions, are subanalytic.
Subdifferentials (Definition 2.10). The Fréchet subdifferential is the set of with (empty off ). The limiting subdifferential is the set of limits of along with .
Slope and critical points. The nonsmooth slope is , equal to when (equation (4)). The critical set is (Definition 2.11).
Let be subanalytic with closed domain and continuous, and let . Then there is such that
with the conventions and . In division-free form: there are and a neighbourhood of with for all and . The exponent is existential; the goal fixes no value of or .
The result. Theorem 3.1 is the nonsmooth Łojasiewicz inequality at critical points. With the subgradient in place of the gradient, it yields finite length of bounded trajectories of subgradient systems (Section 4 of the paper) and is the template for the Kurdyka–Łojasiewicz property that underlies convergence proofs for proximal and splitting methods on nonconvex, nonsmooth problems (e.g. Attouch–Bolte–Redont–Soubeyran 2010, Bolte–Sabach–Teboulle 2014). Those papers assume the KL property and cite this line of results to know it holds for semialgebraic and subanalytic objectives.
Formalizing it. The theorem is proved; this mission produces a machine-checked proof. To our knowledge no proof assistant has a formal definition of subanalytic sets or of the nonsmooth Łojasiewicz inequality. The definitions layer (semianalytic and subanalytic sets, the slope, the inequality) is reusable by any later formalization of KL-based convergence analyses, and the milestones on Remark 2.12 are general facts about limiting subdifferentials that apply well beyond subanalytic geometry.
The obvious argument restricts and to an analytic curve and compares their Puiseux expansions. That step needs three pieces of subanalytic geometry that no library has: curve selection, the structure of one-variable subanalytic functions (monotonicity and Puiseux expansions), and the fact that the sets built in the proof (sets of points with a subgradient satisfying an inequality, level-wise infima of ) are again subanalytic, which in the paper goes through global subanalyticity and the projection theorem. The second obstacle is that is not smooth: the classical proof differentiates along a curve, while here only Fréchet subgradients are available, and the chain rule along an analytic curve holds only almost everywhere. The constancy of on critical components, equation (6), is itself a nonsmooth Sard-type theorem whose published proof uses stratification. A solver who replaces subanalytic by semialgebraic, or assumes real-valued and , proves a different and much weaker statement.
EuclideanSpace ℝ (Fin n). The function is f : E → EReal with f x ≠ ⊥ for every x. The domain is {x | f x ≠ ⊤}; it is assumed closed, and f is assumed ContinuousOn it.NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff, which match Definition 2.10 for functions never equal to .AnalyticOnNhd ℝ. The boundedness of the semianalytic set in Definition 2.1(ii) is part of the definition: without it every projection of a semianalytic set would count.LojIneqAt f a θ: one constant and one neighbourhood of , quantified over all limiting subgradients. Under the value never works at a critical point, as under the paper's conventions.A learning algorithm is judged by its generalization error, its expected loss on a fresh example, which cannot be computed because the data distribution is unknown. Practitioners estimate it either by the empirical error on the training set or by the leave-one-out error, which retrains the algorithm once per example. Classical learning theory justifies these estimates through uniform convergence over the whole hypothesis space (VC dimension, covering numbers). That route says nothing useful about algorithms such as nearest-neighbour rules or regularized kernel methods, whose effective hypothesis space is huge or unknown.
An alternative is to bound the deviation through a property of the algorithm itself: how much its output changes when one training example is removed. This idea goes back to Rogers and Wagner (1978) and Devroye and Wagner (1979) for local rules, and Kearns and Ron (1999) gave it a name. Bousquet and Elisseeff (JMLR 2002) systematized it with several stability notions and corresponding bounds; their paper is the standard reference for algorithmic stability in learning theory. This mission formalizes its first family of results, the polynomial bounds of §4.1.
Let and let be a probability distribution on . A training set consists of examples drawn i.i.d. from . A learning algorithm maps a training set to a hypothesis ; it is deterministic and symmetric, meaning it does not depend on the order of the examples. A cost with defines the loss of a hypothesis at .
For each index , is with removed, and is with replaced by an independent fresh draw . The three error quantities are
Two stability notions (Definitions 3 and 4) control them. has hypothesis stability if for every , and pointwise hypothesis stability if for every .
For , under hypothesis stability and pointwise hypothesis stability , for every , each of the following holds with probability at least over :
Theorem 11 is the weakest-assumption bound in the paper: it requires only average-case stability, not the uniform (worst-case) stability behind the exponential bounds of §4.2. It shows that both the resubstitution and the deleted estimate are within of the risk whenever the stability parameters decay like , with no reference to the size of the hypothesis class. It also extends Devroye and Wagner's leave-one-out analysis for classification to bounded regression losses and to the empirical estimator. Later work on average stability and on generalization of stochastic gradient methods (for example Hardt, Recht and Singer, 2016) starts from these notions.
The result is proved in the paper; as far as is known it has no machine-checked proof. A formal development has two concrete payoffs. First, it fixes the constants: in checking the argument, two printed slips were found (the empirical constant in Theorem 11 and the third term of Lemma 25's first inequality), and the formal statements record the versions that the paper's proof actually establishes. Second, the Lemma 25 and Lemma 9 machinery — exchangeability of i.i.d. samples under renaming, and second-moment control through stability — is reusable for any later stability result.
The obvious route is the Efron–Stein (Steele) variance inequality, Theorem 1 of the paper. It bounds the variance of , not its second moment, and leaves the bias to be handled separately; the paper notes that it gives worse constants. The direct route of Appendix A instead expands and rewrites each correlation term by renaming i.i.d. variables: training points, fresh test points and replacement points are exchanged with one another, and the algorithm is retrained on sets with . Every renaming is a measure-preserving map on a product of copies of , and each must be justified by the symmetry of . Doing this rigorously, rather than as "a matter of renaming", is the core of the work. The leave-one-out case is only sketched in the paper ("it is easy to see"), so its formal proof has to be reconstructed.
Multiset (X × Y) → (X → Y'). Symmetry in the training set is built into the type, and the same algorithm acts on sets of every size, as and require. A sample is S : Fin m → X × Y with law (Measure.pi); fresh points , , are further independent coordinates, via product measures and .FoundationsML.Stability definitions (Loss, EmpiricalError, GeneralizationError).Contributions are welcome at every level: proofs of the milestones, a general exchangeability lemma for symmetric algorithms on product measures, and Markov/Chebyshev glue for the final step.
Learning from a finite sample is useful only if changing the sample has a controlled effect on the learned predictor. Uniform stability asks for a bound on the change in loss at every test point when one training example is removed. Bousquet and Elisseeff use this property to obtain generalization bounds for learning algorithms, and identify regularization as a source of stability in methods built from reproducing kernels. The present mission isolates their result for a squared norm penalty in a reproducing kernel Hilbert space (RKHS). It concerns the sensitivity of the optimizer itself, before any probability bound on a random training sample is applied. The result is Theorem 22 of Bousquet and Elisseeff (2002).
Let be an input space, a label space, and a real reproducing kernel Hilbert space of real-valued predictors on . A kernel and a feature representative express the reproducing identity and . Thus . The source assumes that all diagonal kernel values satisfy .
A labeled example is . Its loss under is , where is a real-valued cost. Let be the set of predictions that some element of can produce at some input. The loss is -admissible when is convex for every label and for all and . Here is a nonnegative Lipschitz constant. The definition compares any two attainable predictions, even when they arise at different inputs.
Fix a sample , a deleted index , and a regularization weight . The paper's full and truncated objectives, with squared RKHS norm regularization, are
The factor in both objectives is . Let and be minimizers of these respective objectives over all of . The statements allow any minimizer satisfying the relevant global optimality condition; they do not choose one by an arbitrary fallback rule.
The central target is the explicit deletion stability estimate of Theorem 22. For every test point ,
Its four milestones follow the paper's route through Lemma 20, the point-evaluation inequality (25), and the two quantitative inequalities displayed in the proof of Theorem 22. In particular, the intermediate RKHS distance bound is when . The main theorem uses , so it does not need a choice of sign for . These numerical constants are part of the target, rather than placeholders for unspecified bounds.
The theorem supplies a deterministic, uniform sensitivity estimate for kernel methods trained by squared norm regularization. The bound applies simultaneously to every test example and decreases as either the sample size or the regularization weight increases. It is one of the ingredients that lets the paper apply its earlier stability-to-generalization results to concrete learning procedures. The loss need not be bounded for this theorem; bounding it is a separate question addressed later in the paper.
The result is proved in the source article. This mission asks for a machine-checked version of its exact pairwise claim and the reusable infrastructure around it: the paper's admissibility condition, the two objectives, the general regularizer inequality, and the RKHS evaluation bound. The existing Prove2Me library already has definitions for loss, empirical error, and the RKHS reproducing identity, so the new definitions concentrate on what is specific to these pages. The related replace-one estimate in Mohri, Rostamizadeh and Talwalkar's Foundations of Machine Learning uses a different perturbation and constant; it is not interchangeable with this result.
The two minimizers solve different objectives, and the deleted example appears in only one of them. A comparison of their objective values alone does not directly give a bound on their distance in the Hilbert norm. The source also distinguishes an abstract convex class of functions in Lemma 20 from the full RKHS used in Theorem 22. A proof must keep those domains straight while preserving the precise normalization of the truncated objective. Another delicate point is that the kernel bound controls evaluations through the reproducing identity; a bound on is not by itself a bound on loss unless the admissibility condition is also used.
The Lean model uses an abstract complete real inner product space , an evaluation map , a feature map , and the published IsRKHSOf predicate tying these to . The completeness instance matches the source's Hilbert-space assumption. Samples have type Fin m → X × Y, so an index i : Fin m already forces . Minimization ranges over the entire for Theorem 22 and over the declared convex class for Lemma 20. The objective definitions use the published Loss and EmpiricalError objects. No probability measure or measurability assumption is needed for these deterministic assertions.
There is a printed mismatch that affects what “deletion” means. Theorem 22 names an algorithm defined by equation (26), which, run afresh on points, would normalize its data term by . Lemma 20 and the proof of Theorem 22 instead compare the full objective with equation (20), whose data term uses . The formalized goal states that comparison, with its explicit constant, and records the discrepancy for audit. This excludes the tempting shortcut of treating the two normalizations as identical. The regularizer is the genuine squared norm and the second minimizer is required to minimize the genuine truncated objective; neither a restricted hypothesis ball nor an artificially assumed distance bound enters the goal. Contributions that establish minimizer existence or connect the pairwise bound to an algorithmic selection would extend this core without changing its statement.
Eligibility traces are one of the basic mechanisms of reinforcement learning. A trace is a short-term memory vector with one component per weight. It records which components contributed to recent value estimates, so that an error observed now can be credited to the right components without storing the past. Chapter 12 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) organizes the topic around two ways of describing an algorithm. A forward view updates each state toward a target built from rewards that arrive later. A backward view makes an update at every step from the current error and the trace.
The chapter proves one exact equivalence between the two views itself, in §12.6: "This is the only equivalence of forward- and backward-views that we explicitly demonstrate in this book" (p. 301). The setting is linear Monte Carlo prediction, and the backward view uses a dutch trace. The same trace appears in true online TD(), whose exact equivalence to the online -return algorithm (van Seijen and Sutton, 2014; van Seijen et al., 2016) the book cites without proof. Of that proof, §12.6 "gives some of the flavor ... but is much simpler" (p. 301).
The older equivalence of §§12.1–12.2 goes back to Sutton (1988). If the weights are held fixed during an episode, the summed updates of TD() with accumulating traces equal the summed updates of the off-line -return algorithm. The book leaves it as Exercises 12.3–12.4.
Fix a dimension , a step size and an episode of length with feature vectors . The episode ends with a single return ("a single reward received at the end of the episode ... and ... no discounting", p. 301). The forward view is the linear gradient Monte Carlo, or LMS, rule (12.13): from an initial ,
Let be the fading matrix. The backward view keeps two vectors that are updated at each step in time without knowledge of . The dutch trace is , . The auxiliary vector is , with .
For the second part, an episode carries states and rewards, and is a differentiable value function with . For one fixed weight vector , define the following, with and :
The left side is the forward view after LMS updates. On the right, and are produced by the incremental recursions above. The goal is about the two algorithms, not only about the closed-form product identity.
The goal says that an -per-step algorithm reproduces the Monte Carlo/LMS result exactly. That algorithm never stores the feature vectors or the intermediate weight vectors. The book draws the conclusion that eligibility traces "are not specific to TD learning at all" (p. 303). The dutch trace in the case is the same object that true online TD() (12.11) uses for general . The fading-matrix products and their incremental forms are therefore the vocabulary of any later formalization of true online TD() and of the online -return algorithm.
Exercises 12.3–12.4 are the fixed-weight equivalence of TD() and the off-line -return algorithm. They are the standard justification for calling TD() an approximation of the -return algorithm. Exercise 12.1 and (12.3) are the identities the rest of the chapter uses to manipulate -returns.
On status: all of these results are known and elementary on paper, and the book prints the derivation of (12.14). To our knowledge none of them has a machine-checked proof, and the platform has no statement about -returns, eligibility traces or TD(). What this mission adds is formal statements with every convention fixed, including one correction to the printed text. It also adds reusable definitions of -step returns, -returns and traces.
The algebra is elementary. The difficulty lies in the conventions, and a careless reading of the page produces a false statement. The book initializes , and taken literally that makes the goal false. The -return is an infinite series, whose tail collapses only because every -step return that reaches past termination equals the full return. That convention has to be built into the definition of , together with the terminal value . Exercises 12.3 and 12.4 are true only when the weights stay fixed. With the algorithms' changing weights the -step returns (12.1) use , and neither identity holds. The boundary indices (, the empty product at , ) must come out right.
Namespace SuttonBartoRL.Traces. Vectors of §12.6 are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and is Matrix.vecMulVec x x. The ordered product fadeProd α x j t is , the identity when . Feature sequences are indexed by ; only enter. is a hypothesis wherever appears. The identities of §12.6 are stated for every real and , a harmless strengthening of the book's positive step size.
For §§12.1–12.2, weights are EuclideanSpace ℝ (Fin d), is Mathlib's gradient, and each is assumed differentiable in Exercise 12.4. An episode is a length , states and rewards. The value at time is . (12.2) is a tsum over of , and , the range the book gives with (12.2). Milestone 5 concludes summability, so the junk value of a divergent tsum cannot make it trivial. Exercises 12.3–12.4 take one weight binder w, used in every return, TD error and gradient. That is the book's fixed- assumption, stated in the binders.
Correction. The printed initialization (p. 302) contradicts the printed definition and (12.14). The counterexample is , , , , , : the forward view gives , while . The mission states the corrected result with , equivalently the same recursion started from . The printed text is kept verbatim in the milestone.
A trivializing formalization is ruled out: the goal is not the closed-form identity with and defined as the products and sums. Those vectors are defined by their -free incremental recursions, and the closed forms are separate milestones.
Out of scope: the equivalence of true online TD() and the online -return algorithm (cited, p. 300), the truncated-return identity (12.10), the error bound (12.8), and all convergence claims. Proofs of the milestones, and reuse of the definitions in later missions on true online TD(), are welcome.
Stochastic approximation algorithms are recursions driven by small steps and noise ; they include the Robbins–Monro scheme, stochastic gradient methods and learning dynamics in games. The ODE method studies their long-run behaviour by comparing a time-interpolation of the iterates with the trajectories of a deterministic dynamical system. In Benaïm's lecture notes (Benaïm 1999) this comparison is formalized by the notion of an asymptotic pseudotrajectory, introduced in Benaïm and Hirsch (1996): a path that, over every window of fixed length, shadows the deterministic orbit started at its current position with an error that vanishes as time goes to infinity.
The pathwise results of the earlier sections of the notes concern algorithms whose step sizes decrease fast enough, typically or . When the step sizes go to zero more slowly, the limit sets of the process can no longer be characterized precisely: with steps of order the process may fail to converge even when the chain recurrent set of the ODE consists of isolated equilibria. Section 10, which is mainly based on work of Benaïm and Schreiber, describes instead the statistical behaviour of such processes in terms of the deterministic dynamics. It introduces a weaker, conditional notion, the weak asymptotic pseudotrajectory, and proves in Theorem 10.1 that the empirical distribution of the time spent by the process in different regions of the state space accumulates only on invariant measures of the deterministic dynamics. This is an ergodic-theoretic counterpart of the limit-set theorems of Section 5.
A semiflow on a metric space is a continuous map , , with and for . Throughout, is a separable metric space with its Borel -algebra.
Let be a probability space and a nondecreasing family of sub--algebras. A process is a weak asymptotic pseudotrajectory of if
Let be the space of Borel probability measures on with the topology of weak convergence. A measure is -invariant if for every ; the set of invariant measures is . The occupation measure of the process at time is the random probability measure
and is the set of its weak limit points as .
If is a weak asymptotic pseudotrajectory of , there is a set with such that for all
No tightness is assumed, so may be empty; the statement asserts the inclusion, not nonemptiness.
Fix a uniformly continuous and , and set for . The milestones are the numbered displays of the proof on pp. 62–63:
The result. Theorem 10.1 locates the long-run statistics of a stochastic process that only shadows a deterministic semiflow in conditional probability. When the occupation measures are tight, for example when the path has compact closure, is nonempty, and the theorem restricts where the process spends its time to the supports of invariant measures. Right after the theorem the notes define the minimal center of attraction of the process from the supports of the measures in ; the conclusion applies to processes, such as slowly decreasing step-size algorithms, for which the pathwise limit-set theorem of Section 5 is not available.
Formalizing it. The theorem has a complete published proof. No machine-checked version of it, of weak asymptotic pseudotrajectories, or of occupation-measure limit theorems for continuous-time processes is known to exist. The mission produces a formal definition of progressively measurable weak asymptotic pseudotrajectories, occupation measures of measurable paths and their weak limit points, and a proof that combines a martingale law of large numbers in discrete time with weak convergence in .
The obvious route is to apply the pathwise argument for asymptotic pseudotrajectories along each path. It fails, because condition 2 controls only conditional probabilities: the deviation events may occur infinitely often along almost every path while their conditional probabilities tend to zero. The proof therefore has to work with averages and conditional expectations instead of with individual paths: a strong law of large numbers for bounded martingale differences transfers conditional statements to time averages, and this must be done for one test function and one horizon at a time. Passing from countably many test functions to invariance requires a countable family of uniformly continuous functions that determines weak convergence on the separable space , and the a.s. sets must be intersected over that family and over rational horizons. Measurability is a second difficulty: paths are not assumed continuous, so the integrals, suprema and conditional expectations involved must be shown to be well defined from progressive measurability alone.
Time is ; the semiflow is Mathlib's Flow ℝ≥0 M; the filtration is a Filtration ℝ≥0; is ProbabilityMeasure M with its topology of weak convergence. is a separable metric space with its Borel -algebra; it is not assumed compact, complete or Polish. Progressive measurability is stated literally for every . The conditional probability in condition 2 is the conditional expectation of the indicator of the deviation event, which is required to be measurable (the paper's presupposes an event); the supremum over is taken in . Invariance for the semiflow is for all , the form the proof establishes; for a flow it agrees with the definition of Section 8.3. Weak limit points are cluster points of as ; the occupation measure is a genuine probability measure for every measurable path and .
The following formalizations would trivialize the statement and are excluded by the definitions: an "occupation measure" equal to the zero measure for a non-measurable path; a conditional probability of a non-measurable event, which Lean evaluates to and which would make condition 2 vacuous; invariance defined through images , which need not be Borel for a semiflow; and a compactness or Polish assumption on , which the theorem does not make.
A complete development needs: Fubini-type measurability for progressively measurable processes, square-integrable martingale convergence and Kronecker's lemma (both largely in Mathlib), conditional expectations of time integrals, a convergence-determining countable family of uniformly continuous functions on a separable metric space, and the identification of weak convergence with convergence of integrals of bounded continuous functions. The martingale law of large numbers (Eqs. (47), (50)) and Eq. (53) are reusable outside this mission. Proofs of any milestone, and alternative arguments for the goal, are welcome.
A stochastic approximation algorithm updates an estimate by small noisy steps, , with step sizes and noise . Such recursions underlie stochastic gradient descent, adaptive control, reinforcement learning (Q-learning, temporal-difference methods) and learning in games (fictitious play, reinforcement models). The ODE method compares the long-run behaviour of the algorithm with that of the ordinary differential equation . Classical versions of this comparison (Ljung 1977, Kushner and Clark 1978) assume the ODE has a globally asymptotically stable equilibrium, or a Lyapunov function, and cannot describe algorithms whose ODE has periodic orbits, heteroclinic cycles or chaotic sets.
Benaïm and Hirsch (1996) replaced these special assumptions by a single dynamical statement: the interpolated algorithm is an asymptotic pseudotrajectory of the flow of , and the limit set of every precompact asymptotic pseudotrajectory is internally chain transitive. This mission formalizes that limit set theorem as it is presented in Michel Benaïm's lecture notes Dynamics of Stochastic Approximation Algorithms (Séminaire de Probabilités XXXIII, 1999).
Timeline. Bowen (1975) and Conley (1978) introduced -pseudo-orbits and chain recurrence, and Conley proved that the chain recurrent set of a flow on a compact space is internally chain recurrent. Benaïm (1996, SIAM J. Control Optim.) related limit sets of stochastic approximation processes to the chain recurrence of the ODE; Benaïm and Hirsch (1996) introduced asymptotic pseudotrajectories for semiflows on metric spaces and proved the limit set theorem in the form formalized here. The 1999 notes give a self-contained proof through the translation semiflow on a space of curves.
Let be a metric space. A semiflow on is a continuous map , , with and . A set is invariant if for every ; then denotes the restricted semiflow on .
A continuous curve is an asymptotic pseudotrajectory of if
and it is precompact if has compact closure. Its limit set is .
For , , a -pseudo-orbit from to consists of partial trajectories, given by points (and an endpoint ) and times with , for , and . One writes if such pseudo-orbits exist for all . A nonempty compact invariant set is internally chain transitive if for the restricted semiflow for all , so that all lie in ; it is internally chain recurrent if for for every . An attractor is a nonempty compact invariant set with a neighbourhood such that uniformly in .
For every semiflow on a metric space and every precompact asymptotic pseudotrajectory of ,
The result. Theorem 5.7 (i) is the bridge between probability and dynamics in the ODE method. Once a stochastic approximation process is shown to be an asymptotic pseudotrajectory (missions 2 to 4 of this series do that under martingale-noise conditions), every statement about its limit points becomes a statement about internally chain transitive sets of the ODE: convergence to equilibria when a Lyapunov function exists (Proposition 6.4), convergence to attractors with positive probability (Theorem 7.3), and the analysis of learning dynamics in games. The theorem is sharp in the sense that every internally chain transitive set is a limit set of some asymptotic pseudotrajectory (Theorem 5.7 (ii), proved in Benaïm and Hirsch 1996 and not part of this mission).
Formalizing it. The result is proved in the literature; it is not formalized. Mathlib has semiflows (Flow), omega limit sets and the compact-open topology, but no pseudo-orbits, chain recurrence, Conley's theory of attractors, or asymptotic pseudotrajectories. This mission produces that layer for semiflows on general metric spaces, which is reusable for any later formalization of the ODE method, of Conley theory, or of learning in games.
The obvious approach follows from a point to a point : returns near and near infinitely often, and on windows of length it is close to a trajectory, so concatenating windows gives a pseudo-orbit. The pseudo-orbit obtained this way has its points on the curve , not in ; this only shows that is chain transitive for on , a strictly weaker property. Producing pseudo-orbits whose points lie in itself is the central difficulty, and it is where precompactness of is used. Invariance , with equality, also needs a compactness argument, since a semiflow is not invertible.
A semiflow is Mathlib's Flow ℝ≥0 M on a [MetricSpace M]; is arbitrary, with no compactness, completeness or local compactness. Time is ℝ≥0. Curves are functions ℝ≥0 → M; continuity is part of being an asymptotic pseudotrajectory, and precompactness is IsCompact (closure (Set.range X)). Invariance is equality . Internally chain recurrent and internally chain transitive sets are nonempty by definition, and their pseudo-orbits are those of the restricted semiflow on the subtype , so every point of the pseudo-orbit lies in . Attractors converge uniformly on a neighbourhood. Lemma 3.1 and Theorem 3.2 are stated on (C(ℝ≥0, M), compact-open topology) with the half-line distance; the notes write , but with the convention for that version fails for semiflows (a periodic trajectory is a counterexample), and the notes themselves describe asymptotic pseudotrajectories as points of .
Ruled out: pseudo-orbits with no trajectory piece (), pseudo-orbits allowed to leave , invariance as mere inclusion , and any compactness assumption on . Each of these makes the goal weaker than the theorem of the notes.
A complete development needs: elementary properties of pseudo-orbits (concatenation, continuity estimates), Arzelà–Ascoli on C(ℝ≥0, M), Conley's attractor construction, and the conjugacy between and the translation semiflow on . Proofs of the milestones, alternative direct proofs of the goal (Benaïm 1996), and reusable lemmas about chain recurrence for Flow are all welcome.
A stochastic approximation algorithm is a recursion
in , driven by a vector field , decreasing step sizes and perturbations . Robbins–Monro root finding, stochastic gradient descent, adaptive filters, learning dynamics in games (fictitious play, reinforcement learning) and urn models all have this form. The ODE method, introduced by Ljung (1977) and developed by Kushner and Clark (1978), Métivier and Priouret (1987) and Kushner and Yin (1997), studies such a recursion by comparing it with the differential equation .
Benaïm and Hirsch (1996) gave the comparison a dynamical form: the continuous-time interpolation of is an asymptotic pseudotrajectory of the flow of . Proposition 4.1 of Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) states that deterministic comparison theorem under two assumptions: a noise condition (A1) and either bounded iterates (A2) or a Lipschitz, bounded vector field near the iterates (A2′). The notes then verify A1 almost surely for martingale noise (Propositions 4.2 and 4.4) and use the asymptotic pseudotrajectory property to describe limit sets, attractors and nonconvergence.
Let be continuous. It is globally integrable if through every point there is exactly one integral curve , ; the flow is the value at time of the integral curve through .
The step sizes satisfy , and . Set , , and . The affine interpolated process and the piecewise constant processes are, for ,
The noise enters through
A continuous is an asymptotic pseudotrajectory of if for every
No rate and no constant appear; the statement holds under either alternative.
with depending only on and on (through its Lipschitz constant and bound on the neighbourhood).
Proposition 4.1 separates the dynamics of a stochastic approximation algorithm from its noise. Any noise condition implying A1 almost surely (Propositions 4.2 and 4.4 of the notes for -bounded and subgaussian martingale differences) combines with it to give: almost every sample path, after interpolation, is an asymptotic pseudotrajectory of . The limit set theorem (Theorem 5.7: limit sets are internally chain transitive), the Lyapunov-function criterion (Proposition 6.4) and the attractor results (Section 7) then apply path by path. Estimate (11) gives the quantitative version used for rates.
The result is proved in the notes, building on Benaïm and Hirsch (1996). No machine-checked proof of it, or of the asymptotic pseudotrajectory framework, is known to exist. A formal proof would supply a checked bridge between discrete recursions with step sizes and flows of vector fields, which every ODE-method convergence proof crosses.
The obvious argument compares directly with the flow by Gronwall's inequality. It needs Lipschitz along both the interpolated path and the flow line, which holds under A2′ but not under A2, where is only continuous and solutions are unique without any Lipschitz bound. Under A2 the comparison must go through compactness instead: equicontinuity of the translates, identification of every limit point as an integral curve, and uniqueness of integral curves. The last step is where global integrability is used, and it cannot be replaced by a quantitative estimate.
Under A2′ the iterates may be unbounded, so no compactness is available, and the path and the flow line must be kept inside the region where is controlled for the whole window .
EuclideanSpace ℝ (Fin d); time is ℝ≥0 for the pseudotrajectory and ℝ inside integrals. Sequences are ℕ → · with the paper's indices; and are unused.Trivializing formalizations are ruled out: the goal keeps both alternatives A2 and A2′ (neither a global Lipschitz condition nor bounded iterates is assumed in place of the disjunction), is the explicit piecewise affine interpolation rather than any curve with the desired property, and the constant in (11) is fixed before the sequences, so it cannot depend on the run.
A complete development needs Gronwall's inequality (in Mathlib), Arzelà–Ascoli on , continuous dependence of solutions on initial data under uniqueness (Kamke's theorem, not in Mathlib), and interval integrals of step functions. The asymptotic pseudotrajectory definitions and Theorem 3.2 are reusable for the other missions on these notes. Proofs of individual milestones are welcome; Eq. (9) and the comparison of and are the natural entry points.
An airline sells the seats of one flight leg in several fare classes at different prices. Low-fare passengers usually book first, so the airline must decide how many seats to keep back, or protect, for later high-fare passengers. Peter Belobaba's 1987 MIT dissertation introduced the expected marginal seat revenue (EMSR) rule for this decision, and EMSR-type rules became a standard of airline revenue management practice (Talluri and van Ryzin 2004). A protection level is computed from a demand forecast, and forecasts are uncertain. Section 6.2 of the dissertation asks how the protection level moves when its inputs move: the mean of forecast demand, its standard deviation, and the ratio of the two fares. That question decides where forecasting effort pays off, and this mission formalizes the answers the dissertation gives for Gaussian demand.
This is the third mission in a series on the dissertation. The first treats marginal allocation among distinct fare classes, and the second the two-class nested protection level in the discrete model, including its revenue optimality. This mission takes the continuous Gaussian model of Chapter 6 on its own terms.
Let be the number of requests for a fare class, a real random variable with law . For a seat level the tail probability is
and for the fare of the class the expected marginal seat revenue is (Eqs. (6.1)–(6.2)).
There are two classes: class 1 with fare and class 2 with fare , where . Requests for class 1 are Gaussian with estimated mean and estimated standard deviation , written . A real number is an EMSR protection level for class 1 against class 2 when
The standardized level is the value "which has a probability of of being exceeded" by a standard normal variable:
In the Lean development these are tailProb, emsr, gaussianLaw rbar σ, stdNormal, IsProtectionLevel rbar σ f₁ f₂ S and IsStdNormalLevel f₁ f₂ Z, all in the namespace SeatInventory.Gaussian.
For and :
The goal states no numerical constant and no particular fare ratio; it fixes only the shape of the dependence.
The dissertation's constant-coefficient-of-variation form, Eq. (6.13), with , follows from (6.12) by substitution and is not stated separately.
The result gives every Gaussian protection level as a closed form in one standard normal quantile. From it come the three sensitivities that Sect. 6.2 uses to argue for better forecasts. The protection level moves one-for-one with mean demand. The standard deviation moves it in a direction fixed only by whether the discount fare is above or below half the full fare. A higher fare ratio always lowers it. The dissertation uses these facts, and its Figures 6.1 and 6.2, to argue that reducing the estimated standard deviation of demand narrows the range of protection levels a forecast can produce. The same quantile structure is behind Littlewood's rule and the newsvendor critical fractile, so the statements here are the Gaussian specialization of a pattern that recurs throughout revenue management and inventory theory.
All the statements are classical and easy to believe. None of them, to our knowledge, has a machine-checked proof. Mathlib provides the Gaussian law and its affine images, but no standard normal quantile and no statement that a Gaussian tail is a strictly decreasing bijection onto . Formalizing this mission produces both, in a form that can be used again wherever a normal critical fractile appears.
Most of the work is in the existence and uniqueness of the two tail solutions. The tail must be shown continuous, strictly decreasing, and to take every value in . Strictness needs the Gaussian density to be positive everywhere, and existence needs a limit argument at both ends. Monotonicity alone, which holds for every law (Eqs. (6.1)–(6.2)), gives neither, because a general law can have flat stretches and jumps in its tail. The relation then requires transporting the tail of to that of through the affine map , and the sign of requires the symmetry of , namely . Once uniqueness is available, each sensitivity statement follows from these facts. The tempting shortcut of reading as a definition is ruled out below.
gaussianReal rbar (σ^2), parameterised by the variance. Every theorem assumes ; at the law is a Dirac mass and (6.10) has no solution.Useful infrastructure, all reusable: the strict monotonicity, continuity and range of Gaussian tails; the standard normal quantile; and tail transport under affine maps. Contributions of these as separate lemmas are welcome.
An agent learning to control an unknown environment must balance rewards it can collect now against information that improves later decisions. In a finite Markov decision process (MDP), every action changes the distribution of the next state, so a mistaken transition estimate can affect decisions many steps later. Regret measures this loss against a policy that already knows the transition probabilities. The paper of Azar, Osband and Munos gives high-probability regret bounds for two variants of upper confidence bound value iteration (UCBVI) in finite-horizon reinforcement learning. This mission targets its Chernoff–Hoeffding variant, UCBVI-CH, whose bonus depends only on the horizon and the visit count. Theorem 1 improves the paper's cited earlier dependence on the number of states from to in the leading term for sufficiently many interactions. Azar, Osband and Munos, 2017, pp. 2, 4–5.
The paper was released in 2017 alongside work on the attainable dependence of episodic regret on the horizon , state count , action count , and total interaction time . Its second algorithm, UCBVI-BF, uses a variance-dependent bonus and is the subject of the next mission in this series. UCBVI-CH has a simpler bonus and its own explicit bound, making it a distinct mathematical target. Azar, Osband and Munos, 2017, pp. 1–5.
The state set and action set are finite and nonempty, with cardinalities and . A stationary transition kernel gives the probability of moving to state after action in state ; each row is nonnegative and sums to one. The known, deterministic reward lies in . An episode lasts steps. The environment chooses its starting state before episode and may base that choice on earlier episodes. It cannot see the current episode's future random draws. Azar, Osband and Munos, 2017, §2 and Assumption 1, pp. 2–3.
A policy selects an action from the current state and the step number. Its value is the expected sum of rewards from step through step when starting in state . The terminal value is , and is the maximum of over all such policies. Since the state, action and step sets are finite, this maximum is over a finite nonempty policy class. The paper's sentence describing rewards uses a shifted terminal convention; this series follows the reward steps of Algorithms 1–2. Azar, Osband and Munos, 2017, pp. 3–4.
At the start of episode , UCBVI-CH forms visit counts and from earlier completed transitions. On a visited pair it uses the empirical row . Algorithm 2 computes values backward from zero at the terminal step. For a visited pair, is the minimum of the preceding episode's , , and the empirical Bellman value plus Algorithm 3's bonus. For an unvisited pair, . A maximizing action is chosen at every state, including states outside the realized path. Azar, Osband and Munos, 2017, Algorithms 1–3, pp. 3–4.
For episodes and , regret sums the gap . The goal is the paper's printed bound, with its constants:
Algorithm 3 itself uses in its bonus . Both logarithms remain as printed. The probability is over the MDP's next-state draws, for every admissible starting-state rule and every way of breaking ties between maximizing actions. Azar, Osband and Munos, 2017, Algorithm 3, p. 4; Theorem 1, p. 5.
Four milestones retain the source's indexed attack path: the Bernstein bound (9) for the empirical value error, the count-deviation display before (11), Lemma 18 on optimism, and the weighted recursion displayed in the proof of Lemma 3. The last milestone preserves the signed weights that appear before the paper's final simplification. Azar, Osband and Munos, 2017, pp. 17, 20–21, 28.
Theorem 1 gives a finite-sample failure probability with explicit dependence on and . It covers a learner whose initial state can change between episodes, a feature that matters in episodic learning where the experimenter does not fix a single starting distribution. For the regime stated after Theorem 1, the leading rate is . This is a result claimed by the paper; the present Lean declarations are open proof targets, not machine-checked proofs of that claim. Azar, Osband and Munos, 2017, p. 5.
Formalizing the result creates reusable finite objects for adaptive interaction: a constructed probability law on complete paths, empirical transition counts pooled across steps, a policy value defined by its expected reward, and confidence events with their domains stated explicitly. The concentration and optimism milestones can then be investigated independently of the final regret bound. The later UCBVI-BF mission uses the same paper's model with a different bonus. Azar, Osband and Munos, 2017, pp. 3–5, 14–17.
The visit count is random and depends on earlier observations and decisions. A concentration inequality for a predetermined number of samples therefore does not immediately give a statement that holds at every episode start. The algorithm also reuses the previous episode's estimate through a minimum. Any optimism claim must account for this dependence across episodes as well as the backward dependence across steps. In the regret analysis, the terms called martingale differences can have either sign, so replacing a positive weight by a larger common bound can reverse an inequality. These are concrete obstacles to the printed chain of estimates. Azar, Osband and Munos, 2017, pp. 4, 17, 20–21, 28.
States, actions, steps, episodes and complete outcome arrays are finite. Probabilities are finite sums of products of transition rows. The transition-row predicate is a published general definition; this mission defines the paper-specific reward-bounded MDP, policies, UCBVI-CH recursion, and path law on top of it. The starting-state rule can inspect only earlier episodes. Greedy tie-breaking is universally quantified. is a maximum over policies, and the bonus is read only at positive counts. A model that assigns an arbitrary probability law, fixes one starting state, or omits Algorithm 2's minimum does not represent this target. Azar, Osband and Munos, 2017, pp. 2–4.
Lean uses steps and terminal index in place of the paper's algorithmic . The appendix sometimes puts the terminal value at . The weighted recursion therefore runs through the final reward step, rather than ending one step early. Its typical-state threshold is , as required by (34)–(36), whereas Appendix B.1 prints . The proof's correction term dominates its other terms under , which is made explicit in that milestone. The printed (11) loses a factor of two from the count display before it; only the preceding display is a milestone. Lemma 18 is stated under the empirical-model part of the confidence event and , the domain on which its bonus comparison holds. The weighted milestone retains its coefficients because the bracketed martingale terms can be negative. Azar, Osband and Munos, 2017, pp. 14–17, 20–21, 28.
The goal retains Theorem 1's constant . Appendix C.1 cites Lemmas 15 and 18, but the sketch of Lemma 15 does not track that constant explicitly. Formalizing the printed bound may therefore expose a gap in its proof; the mission records the claim without weakening its constants. Contributions establishing or repairing the explicit bound, as well as the four stated milestones and reusable finite concentration results, are within scope. Azar, Osband and Munos, 2017, pp. 5, 27, 29.
In the classical secretary problem a decision maker sees candidates in a uniformly random order and must accept or reject each one on arrival, irrevocably, aiming to accept a valuable one. Its online, random-order structure models hiring, selling an item to sequentially arriving buyers, and posting prices in online markets. Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study the discounted secretary problem, where the reward of a selection depends on when it is made: a candidate accepted late is worth less (or more) by a time-dependent factor, as with a seller whose revenue decays with time, or a firm that loses value the longer a position stays empty.
Timeline of the setting:
There are elements, indexed by . Element has a value , and each time has a discount . The elements arrive in a uniformly random order , a bijection from times to elements: element arrives at time . Selecting the element that arrives at time earns , and an algorithm selects at most one element.
The offline optimum on the order is . It is a random variable, and the benchmark is its expectation
For a real parameter , algorithm selects the first time at which and earns that product; if no time qualifies, it selects nothing and earns . It knows and , sees the values one at a time, and never sees the future of . Its expected value is .
The proof uses three derived objects:
For every , all discounts , all values and every real ,
Taking gives , a -competitive algorithm when the expected optimum is known.
The result. The discounted problem separates sharply by information: a logarithmic gap is unavoidable without prior knowledge, while knowledge of the single number , or of any lower estimate of it, closes the gap to a constant. The algorithm is a fixed posted threshold, so read as a mechanism it is a posted price, which is truthful for single-parameter agents (§1). The paper also notes that when all values are known, can be estimated by sampling (its Lemma A.1), which yields a constant-competitive algorithm in that setting. The companion lower bound (Theorem 4.6) shows that even complete knowledge of the values does not give a ratio better than .
Formalizing it. The result is proved on paper; no machine-checked proof is known. The formalization yields a checked version of the paper's counting argument on permutations (Claim 4.8) and of the tie-breaking step behind Eq. (4.3), and reusable finite random-order bookkeeping: expectations over as averages, threshold stopping rules, and the decomposition of an online algorithm's value by the time and element it selects.
The obvious argument fails when rarely selects. earns at least whenever it selects anything, so . That settles the case and nothing else: the probability of selecting can be tiny while is still large, because the optimum may be concentrated on a few orders with a large product. In that case the bound must come from comparing the algorithm with the optimum pair by pair: every time–element pair with must be realized by on a positive fraction of the orders.
Two points need care in a formal proof:
Neither (4.2) nor the map appears in the statements, so solvers may replace either with any argument they like.
Fin n; the paper's time is the index . An order is π : Equiv.Perm (Fin n), read as time ↦ element, as on p. 3. The instance [NeZero n] encodes , so the maximum over times is a genuine maximum (Finset.sup').Equiv.Perm (Fin n) and on first-hitting times are reusable beyond this mission.