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.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A stochastic approximation algorithm is a recursion with decreasing step sizes and a noise term . Recursions of this form appear in stochastic gradient methods, adaptive control, learning in games (fictitious play, reinforcement learning) and urn models. The ODE method compares the iterates with the solutions of . In Benaïm's lecture notes (Benaïm 1999), the comparison is phrased through the continuous-time interpolated process . Under standard noise conditions, is almost surely an asymptotic pseudotrajectory of the flow of , and its limit set is almost surely internally chain transitive.
That theorem constrains where the process may end up. It does not say which of several candidate sets the process actually reaches. When the ODE has several attractors, for example several stable equilibria of a learning dynamic or several stable compositions of an urn, an application needs to know that each attractor is reached with positive probability. Section 7 of the notes answers this question. The answer is a criterion of attainability: if the process can, with positive probability and at arbitrarily late times, enter the basin of an attractor, then it converges to that attractor with positive probability.
Timeline.
Let be a metric space and let be a semiflow on : a continuous map with and .
Now let be a process on a probability space with continuous paths in , adapted to a filtration . The standing assumption of Section 7 is that for all , and ,
for a function with as .
A point is attainable if for every and every open neighbourhood of . is the set of attainable points.
If is locally compact, is an attractor of , and , then
This statement contains no constants and no rates, so it does not depend on how (24) is quantified for a particular algorithm.
If is open and relatively compact with , there are , depending only on (and on , ), such that for every process satisfying the standing assumption and every
The result. Theorem 7.3 turns a question about the long-run limit of a random process into a question about where the process can go. Attainability is usually checked by a controllability argument: the noise can push the iterates in every direction. For urn processes with an urn function mapping the simplex into its interior, every point is attainable (Example 7.2 of the notes). Then every attractor of the mean ODE is reached with positive probability. Combined with nonconvergence results for unstable sets (Section 9 of the notes), this characterizes the possible limits of many learning and urn processes. Theorem 7.3 is the positive half of that picture.
Formalizing it. The theorem has a published proof (p. 32 of the notes) and no machine-checked version. A formal proof needs the following:
The obvious argument says: once enters a compact part of the basin, the flow carries it into . That fails because is not a trajectory of the flow. Each window of length adds an error, and errors over infinitely many windows can push the process out of the basin.
Two things are needed instead:
A naive union bound over all times is useless: it does not use the conditional form of (24).
Flow ℝ≥0 M on a metric space; local compactness is LocallyCompactSpace M.X : ℝ≥0 → Ω → M with continuous paths. The paper's alternative of càdlàg paths is not covered.Filtration ℝ≥0. is a probability measure.These choices rule out the trivializing formalizations: a conditional-probability hypothesis that holds vacuously, invariance read as inclusion, constants that depend on the process or on , and a probability bound without monotonicity.
A complete development needs:
The first and second are reusable well beyond this mission. Contributions toward either, and alternative proofs of Lemma 6.8, are welcome.
A stochastic approximation algorithm is a recursion
in , where is a vector field, are small step sizes and is noise. Such recursions go back to Robbins and Monro's root-finding scheme (Robbins–Monro 1951) and underlie stochastic gradient descent, temporal-difference learning, adaptive control and learning in games. The ODE method studies them by comparing the iterates with the trajectories of .
Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (and the iterates are bounded, or is Lipschitz and bounded on a neighbourhood of them), the interpolated process is an asymptotic pseudotrajectory of the flow of . A probabilistic step then verifies A1 for concrete noise models. This mission formalizes the first such verification, Proposition 4.2: martingale difference noise with bounded -th moments and step sizes with . The result is described as a particular case of a general theorem of Métivier and Priouret (1987); the same estimates reappear later in the notes.
Let be a deterministic sequence with , and (a step sequence). Put , , and let
be the index of the step that contains time . For a sequence define the piecewise constant processes and , so that step occupies the time interval of length .
Assumption A1 asks that for every
or, in the form the notes call equivalent, for every , where
Let be a probability space with a nondecreasing sequence of sub--algebras, and continuous. A sequence given by the recursion above is a Robbins–Monro algorithm if is deterministic, is -measurable, and .
For a Robbins–Monro algorithm and some real , if
then with probability one the realised noise sequence satisfies A1, in both of its forms, simultaneously for all .
Proposition 4.2 is the standard sufficient condition under which the ODE method applies to stochastic gradient-type recursions with martingale noise. With it covers step sizes with (for example ) and noise with bounded variance; larger trades stronger moment assumptions for slower decay of the steps, down to . Combined with Proposition 4.1 it shows that the interpolated process of a Robbins–Monro algorithm with bounded iterates is almost surely an asymptotic pseudotrajectory of the flow of ; the limit set theorems of the notes then locate the limit points of the algorithm.
The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would supply reusable pieces that Mathlib currently lacks, most notably a Burkholder (or Burkholder–Davis–Gundy) inequality for discrete-time vector martingales in , and the continuous-time bookkeeping of the step processes , and the noise deviation , shared by the other missions of this series.
The obvious argument controls each window by Doob's maximal inequality and sums over windows. That works for only. For the second moment of the window sums is not summable under , and one needs an maximal inequality whose right-hand side is the -th moment of the square function. That inequality, Burkholder's, is not in Mathlib. Converting the square function into the moment bound requires a Hölder-type inequality with tuned exponents, and passing from the discrete sums to requires handling partial steps at both ends of . A second subtlety is that A1 quantifies over all : the almost-sure statement must hold on a single event of full probability for every , not on an event that depends on .
The space is as EuclideanSpace ℝ (Fin d); time is real; is a real number with , and all powers are real powers of nonnegative quantities. The sequences and are indexed by , and their values at are unused, as the paper indexes them from . The filtration is a Mathlib Filtration ℕ, is required to be -strongly measurable and integrable, and the martingale difference condition is almost surely. Expectations of nonnegative quantities, the suprema in A1 and , and the moment bound are taken in , so no default value of a non-integrable expectation or of an empty supremum can make a statement hold vacuously; the supremum over an empty range of is .
The following readings are excluded and are not acceptable formalizations: a moment hypothesis that holds vacuously, a conditional expectation hypothesis on non-integrable noise, the conclusion "for each , A1 holds almost surely" in place of "almost surely, A1 holds for all ", and fixed to or restricted to integers.
All hypotheses are satisfiable: , , and with satisfy every one of them.
Contributions welcome: a general Burkholder inequality for discrete-time martingales in finite-dimensional spaces (reusable well beyond this mission), lemmas on the step processes and (measurability, local integrability, additivity), and the proofs of the milestones.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It uses the same density estimate as the companion entry, for with (explicit Selberg sieve, weighted first moment, eighth moment of the singular-series factor, Hölder). It then replaces Schnirelmann's sumset inequality by Mann's theorem, for sets containing :
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It keeps the explicit Selberg sieve and Schnirelmann's original sumset inequality from the entry, and improves only the density estimate:
Only Chebyshev-type prime bounds, the Selberg upper-bound sieve, Hölder's inequality and Schnirelmann's inequality are used.
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It keeps the explicit Selberg sieve and Schnirelmann's original sumset inequality from the entry, and improves the density estimate:
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
A stochastic approximation algorithm is a recursion with decreasing steps and noise . Stochastic gradient descent, the Robbins–Monro procedure, reinforcement-learning updates and learning dynamics in games all have this form. The ODE method compares such a recursion with the deterministic dynamics . Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) do this in two steps. First, the limit set of the interpolated process is internally chain transitive for the semiflow of (Theorem 5.7, the subject of mission 1 of this series). Second, internally chain transitive sets are located using properties of the dynamics alone.
The most common tool in the second step is a Lyapounov function: a function that decreases strictly along every trajectory outside a set and is constant on . Proposition 6.4 of the notes states exactly when such a function forces every internally chain transitive set into . It is the step behind the convergence of stochastic gradient algorithms to critical points (Corollary 6.7) and behind convergence results for learning in potential games.
Timeline.
Let be a metric space, with no compactness or completeness assumed. A semiflow on is a continuous map , , with and .
Let be compact invariant and a Lyapounov function for , and assume that has empty interior in . Then for every internally chain transitive set ,
The result. Proposition 6.4 converts a statement about real numbers, that has empty interior, into a statement about dynamics: the chain recurrent behaviour of is confined to . With Theorem 5.7 it gives the following. If has such a Lyapounov function, then the limit set of any precompact asymptotic pseudotrajectory, in particular of a bounded stochastic approximation process, lies in , and is constant on it. When is the set of equilibria and is Lebesgue-null by Sard's theorem, this is the convergence of stochastic gradient algorithms to connected sets of critical points (Corollary 6.7). Remark 6.5 gives a flow on the circle with a strict Lyapounov function, where the circle itself is internally chain transitive. So the empty-interior hypothesis cannot be removed.
Formalizing it. The result is proved, in the notes and in the earlier literature. No machine-checked version of chain recurrence for semiflows on metric spaces, Conley's attractor lemma, or Bowen's characterization of chain transitive sets is known to us. The mission therefore adds the following:
Flow;The obvious argument does not work. It runs: decreases along trajectories, so along an orbit in the value of must settle on . But points of an internally chain transitive set are joined only by pseudo-orbits. At each of the jumps, may increase by an amount that is small but not controlled in number, so monotonicity of along true trajectories says nothing directly about . Remark 6.5 shows that the conclusion is genuinely false without a condition on . The difficulty is therefore global: pseudo-orbits that climb back up through many small jumps must be excluded using information about the restricted semiflow as a whole, not the monotonicity of along single trajectories. Milestones 1 and 2 are the general facts about chain transitive sets that this requires, and their own proofs involve compactness and uniform-continuity estimates over arbitrarily long pseudo-orbits.
MetricSpace, and the semiflow is Flow ℝ≥0 M.interior (V '' Λ) = ∅ in , not countability, finiteness or measure zero.IsGLB, not a real sInf.The following formalizations are trivializing and are excluded:
A complete development needs elementary facts about ω-limit sets of points of a compact invariant set: they are nonempty, compact and invariant. It also needs the attractor construction and the open sets used in Proposition 5.3. These are reusable for any work on Conley theory. Contributions of any of these lemmas, or of proofs of the milestones in any order, are welcome.
Reinforcement learning formulates control as maximizing reward accumulated over time. For continuing tasks, where interaction never terminates, the standard textbook objective is the discounted return with a discount rate . Chapter 10 of Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018), argues that once values are approximated by a function of features rather than stored per state, this objective is the wrong one, and it proposes the average-reward setting, long standard in dynamic programming (Puterman, Markov Decision Processes, 1994), as its replacement.
The central piece of evidence is a short calculation printed in the box The Futility of Discounting in Continuing Problems (p. 254). If one tries to rescue discounting by averaging discounted values over the states the policy actually visits, the resulting objective is a constant multiple of the average reward, so the discount rate has no effect on which policy is preferred. This mission formalizes that calculation together with the definitions of §10.3 that it rests on, and the two exercises of §10.3 that illustrate the differential value (10.13).
A finite MDP has finite state set , finite action set , finite reward set and dynamics , a probability distribution over next state and reward for each state–action pair (3.2)–(3.3). Write . A policy is a distribution over actions for each state. It turns the MDP into a Markov chain with transition matrix and expected one-step reward , so that and .
A stationary distribution of is a probability vector on with
The average reward of is
the second form holding when the steady-state distribution exists and does not depend on (an ergodic MDP).
The discounted value function is , and the objective of the box is
Finally, the differential value of a state (10.13) is .
For , every policy and every stationary distribution of ,
and therefore, for a fixed and policies with their own stationary distributions,
The book prints no answers to Exercises 10.6 and 10.7; the values above were computed for this mission.
The result itself. The identity shows that the discount rate cannot enter the ranking of policies once performance is measured over the on-policy state distribution: any objective of the form "discounted value averaged over where the policy goes" is the average reward up to a positive factor. The book draws from it the conclusion (p. 253) that changes from a problem parameter to a solution-method parameter, and that discounting algorithms with function approximation, which do not optimize this averaged objective, are not guaranteed to optimize average reward either. Milestones 1–2 connect the closed form of to its definition as a long-run rate; milestone 4 explains why differential methods determine values only up to an offset; the exercises show that (10.13) gives finite differential values in periodic chains where the differential return (10.9) has no limit.
Formalizing it. The results are classical and elementary, but the book's derivation is informal: it takes the Bellman equation for granted, sums a geometric series of equalities, and leaves implicit which distribution is meant and when (10.6) and (10.7) agree. This mission fixes each of those points: is defined from returns, the identity is proved for every stationary distribution, and the ergodicity hypothesis is made the exact limit condition the text states. No machine-checked version of these statements is known to exist; the platform's Markov-chain and average-reward libraries (Puterman's unichain optimality equation, Doeblin convergence) state different results.
The box reads as a chain of equalities, and each individual step is short. The one step that is not algebra is "(Bellman Eq.)": with defined as an expected discounted return, the Bellman equation requires exchanging an infinite sum with a finite expectation and shifting the index of a convergent series, which needs absolute convergence for and bounded rewards. The final line, which unrolls into a geometric series, is only valid because is finite. For milestone 1, the book's hypothesis is the existence of an -independent limiting distribution, not irreducibility or aperiodicity; replacing it by either would change the statement. The exercises require the iterated limit in (10.13) to be computed explicitly: the inner limit is a periodic series summed in closed form, and the outer limit is a removable singularity at .
The Lean development lives in the namespace SuttonBartoRL.AverageReward. States, actions and rewards are finite; one action set serves every state; the dynamics are the four-argument . Probabilities and are computed from the matrix powers . The discounted value is a real series ; it is not defined as the solution of the Bellman equation, since that definition would reduce the goal to three lines of algebra. The average reward and take the state distribution as an explicit argument; the goal holds for every stationary distribution of and assumes no ergodicity, which is all the box uses (under ergodicity is the unique one). is allowed. The differential value (10.13) is stated as the existence of both limits with the given value, with from below, so no default value of a nonexistent limit can make a statement true. The optimality equations use a nonempty action set. The sum of (10.6) is written with the index shifted to .
The Lean does not formalize a trajectory probability space: expectations and probabilities are the matrix expressions above, which is what they equal for a Markov chain. The Exercise 10.6 hypothesis constrains expected rewards of one policy, which is all the exercise uses.
Reusable parts: the finite-MDP layer duplicates the one drafted for the other missions of this series and is expected to be merged with it; the Cesàro and stationary-distribution lemmas of milestones 1–2 are general facts about finite Markov chains. Contributions welcome: proofs of any milestone, and a proof of the goal from milestone 3.
Optimization problems with orthonormality constraints arise throughout numerical linear algebra and its applications: computing a few eigenvectors or singular vectors, Procrustes problems in statistics and shape analysis, orthogonal factor rotation, independent component analysis, and the orthogonality constraints of electronic-structure calculations. The feasible set of such a problem is the Stiefel manifold of orthonormal -frames in . Riemannian optimization algorithms on this manifold (Riemannian gradient, Newton and trust-region methods; see Absil, Mahony and Sepulchre, Optimization Algorithms on Matrix Manifolds, 2008) take a step in a tangent direction and then need a retraction: a map that brings the updated point back onto the manifold while agreeing with the geometry to first order.
The most natural way to come back to a constraint set is to take the nearest point. P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds (SIAM J. Optim. 22(1), 2012; the mission follows the authors' version, HAL hal-00651608v2), show in their Proposition 3.2 that the metric projection onto a smooth submanifold yields a retraction, and then work out the projection explicitly for several matrix manifolds. For the Stiefel manifold, their Proposition 3.4 identifies the projection with a factor of the singular value decomposition, equivalently with the orthonormal factor of the polar decomposition. The paper notes that this result was mentioned without proof in Higham's survey of matrix nearness problems, and gives a proof along the lines of Horn and Johnson, Matrix Analysis, §7.4.
Section 4.5 of the same paper treats a second, "orthographic" retraction on the Stiefel manifold, which corrects a tangent step by a normal vector instead of projecting; for the orthogonal group (the case ) it admits a closed form through a matrix square root (Proposition 4.12).
Fix natural numbers . Matrices are real, and carries the Frobenius norm
The Stiefel manifold is
the set of matrices with orthonormal columns; is the orthogonal group .
The singular values of are , the square roots of the eigenvalues of . A singular value decomposition of is a factorization with , , and zero off its diagonal, with nonnegative nonincreasing diagonal entries. For every singular value equals ; in particular .
A projection of onto is a point with for all . A polar decomposition of is a factorization with and symmetric positive definite.
Let and let satisfy . For every singular value decomposition ,
and is the of the polar decomposition : it is the orthonormal factor of every polar decomposition of , and a polar decomposition with this factor exists.
The statement asserts existence, uniqueness and the closed form of the projection on the whole open ball of radius , for whichever singular value decomposition is supplied.
for , skew-symmetric and symmetric with ; and Proposition 4.12,
stated as: is the unique symmetric correction of smallest Frobenius norm.
Proposition 3.4 makes the projective retraction on the Stiefel manifold computable from one singular value decomposition of an matrix, and identifies it with the polar factor, which is also what many numerical codes already compute for re-orthonormalization. Combined with Proposition 3.2 of the paper, it yields a second-order-accurate retraction usable in any Riemannian algorithm on . The same statement is the orthogonal Procrustes problem in the special case of a full-rank target: the nearest orthonormal frame to .
The result is classical and proved; the paper's argument is short but cites two external facts (Weyl's perturbation bound for singular values and the uniqueness of the polar decomposition). To our knowledge no machine-checked proof of the nearest-orthonormal-frame property, of the uniqueness of the polar factor, or of the closed form of Proposition 4.12 exists in Mathlib or on this platform. A formalization produces reusable pieces: the trace inequality over the Stiefel manifold, the uniqueness of the polar decomposition, and the full-rank property near , all of which recur in matrix analysis and in the analysis of Riemannian algorithms.
Existence of a nearest point is easy (the Stiefel manifold is compact), and attainment of the trace bound is a direct computation. The content is in two places. First, the bound for every requires transporting by the orthogonal factors of the singular value decomposition and bounding diagonal entries of a matrix with orthonormal columns. Second, uniqueness does not follow from the trace argument: when is rank deficient there are many maximizers. Uniqueness needs both a perturbation bound (singular values are 1-Lipschitz in the Frobenius norm, so near ) and the uniqueness of the polar factor, which in turn rests on the uniqueness of the positive-semidefinite square root of . Mathlib has singular values of linear maps and the spectral theorem but, at the pinned revision, neither Weyl's inequality for singular values nor the polar decomposition.
For Proposition 4.12, the printed proof compares only two solutions of (4.14), while (4.14) has other symmetric solutions (mixed signs of the square roots, or non-diagonal ones on repeated eigenvalues); minimality must be proved against all of them.
Matrices are Matrix (Fin n) (Fin m) ℝ with the Frobenius norm brought in by open scoped Matrix.Norms.Frobenius. The Stiefel manifold is the set stiefel n m of matrices with Xᵀ * X = 1. Singular values are Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin X, re-indexed to be 1-based as on the page (sv X m is ). A singular value decomposition is the predicate IsSVD X U S V of display (3.5), and is U * E * Vᵀ with E the rectangular identity (frameOfSVD U V). The projection is the set of nearest points, using the published predicate RandomGradFree.Nonsmooth.IsMetricProjection; "exists and is unique" is equality of that set with a singleton. Positive definiteness is Mathlib's Matrix.PosDef, which over includes symmetry.
Standing assumptions and added hypotheses: is the page's assumption of §3.3; is added so that is meaningful. The radius is with strict inequality, kept in that form although its value is . Two misprints of the page are corrected in the Lean and kept in the verbatim milestone texts: the display of Proposition 3.4 reads for , and the distance identity reads for . The uniqueness of the polar factor is stated for positive semidefinite factors under the rank hypothesis, which contains the positive definite case of Proposition 3.4. The matrix square root of §4.5 is defined through Mathlib's spectral theorem; Proposition 4.12 is stated for every admissible symmetric correction, and is vacuous only when no symmetric correction exists.
A trivializing formalization is ruled out: the projection is not taken as a hypothesis or chosen by definition; the goal asserts that the nearest-point set equals the singleton of the explicit matrix, for every singular value decomposition supplied, so neither existence nor uniqueness can be assumed away.
Contributions welcome beyond the stated items: Weyl's inequality in Mathlib's singular-value API, existence of a singular value decomposition in the matrix form (3.5), and the polar decomposition with its uniqueness, all reusable well beyond this mission.
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.
The simplex method solves linear programs by moving between vertices of a feasible polyhedron. Its worst-case number of moves can grow exponentially, yet it often performs well on ordinary inputs. Worst-case examples alone therefore give an incomplete account of the method’s behavior. Spielman and Teng introduced smoothed analysis to measure expected performance after small random perturbations of an arbitrary input. Their result for a two-phase shadow-vertex simplex method gives a polynomial bound in the input dimensions and inverse perturbation scale. The pinned preprint is the source for every theorem number and constant in this mission.
The paper separates a geometric result about the expected size of a polytope’s shadow (Theorem 4.0.1) from the algorithmic result here (Theorem 5.0.1). That separation matters: a plane chosen before perturbation and a plane chosen by a running algorithm have different distributions. This mission addresses the latter. It complements the standard-form simplex theorems already formalized in the Introduction to Linear Optimization series and the worst-case Klee–Minty result in the Smale’s Ninth Problem mission; those results concern different algorithms or input models and are context rather than imported statements.
A linear program is specified by vectors , right-hand sides , and an objective vector :
The paper’s two-phase shadow-vertex method first draws a collection of -element subsets of and chooses one whose constraint matrix has the largest smallest singular value. It sets a power-of-two scale from the input norm and a power-of-two scale from that singular value. These determine positive relaxed right-hand sides : for and otherwise. A coefficient vector is chosen uniformly from . The first phase solves the relaxed program LP′ from the objective .
The second phase uses a lifted program LP⁺ in . For each original constraint it forms and , together with two artificial constraints at first coordinates and . LP⁺ connects LP′ to the original program and makes infeasibility detectable. Its shadow is taken in the plane of and .
For positive right-hand sides, an optimal polar simplex is a -subset of constraints whose scaled vectors form a facet of and whose unscaled cone contains an objective . The shadow for objectives is the union of these simplices over all in . Its size bounds the number of polar pivots. In Section 5 the paper writes for the first-phase shadow size and for the second-phase shadow size without the two artificial pivots.
The input is perturbed by independent Gaussians: each coordinate of and each has its prescribed center and common standard deviation , where . The algorithm has separate random choices of and .
The immediate targets bound the two phases: Lemma 5.2.1 gives an explicit expectation bound for and Lemma 5.3.1 gives one for . Lemma 5.1.1 and its corollaries control the chance that the chosen basis has a very small singular value. Corollary 4.3.3 extends the geometric shadow bound to positive, unequal right-hand sides and general Gaussian covariance. These are the mission’s milestone targets.
The goal is the shape of Theorem 5.0.1. With , there are a single polynomial and a positive constant such that, for all and all centers and objectives,
The polynomial is uniform over the dimensions and inputs; its coefficients are not prescribed. The bound on implies the corresponding result for the actual pivot count through the paper’s step-to-shadow comparison. The goal is stated with a positive center scale , the case in which the paper’s Gaussian rescaling applies.
The theorem places the number of pivots of a complete simplex method under one explicit perturbation model, including the work needed to find a starting feasible basis and handle an arbitrary right-hand side. The trivial binomial bound is retained because it controls rare events in the proof and is part of the stated result. The polynomial bound says that even when the unperturbed LP is adversarial, Gaussian noise of a controlled scale makes the expected shadow-size cost polynomial.
The paper proves the mathematical result. This mission asks for machine-checked proofs of its statement and the listed milestones; the draft Lean declarations are targets with sorry, not completed proofs. The reusable formal infrastructure is the finite polar simplex and shadow construction, product Gaussian input law, smallest-singular-value events for sampled minors, and the uniform truncated-simplex coefficient law. The two shadow-size lemmas also require explicit handling of measurable finite-valued counts and their expectations.
The basic shadow estimate fixes its projection plane before perturbing the constraints. In LP′, the initial objective uses a basis selected after the perturbation, so the relevant plane depends on the random LP. The fixed-plane theorem cannot be substituted directly. For LP⁺, the normalized lifted vectors are nonlinear functions of Gaussian data; they are generally not Gaussian vectors. Thus the same shadow estimate does not apply directly to their law either. A further issue is that a poor sampled basis can make very large. These are distinct obstacles, reflected in the milestone groups from Sections 5.1, 5.2, and 5.3.
Vectors are EuclideanSpace ℝ (Fin d), constraints are Fin n → EuclideanSpace ℝ (Fin d), and index families are finite sets of Fin n. The paper’s starts at one; Fin n starts at zero. The Gaussian constructor receives variance , not standard deviation . The draws are rounded upward and are independent uniform draws with replacement. Equal singular values are resolved by the first sampled set. The uniform law on is represented by normalized independent exponential weights followed by the affine shift that imposes .
The Lean definition of is exactly the Section 5 shadow-size upper bound , computed from the sampled LP data. It is not an arbitrary cost variable. The actual algorithmic step bound needs the paper’s polar algorithm and Lemma 3.3.5. The goal explicitly asks for inner and outer integrability so Lean’s default value for a nonintegrable Bochner integral cannot make the result vacuous. The source’s all-zero center scale is excluded because it gives zero perturbation and defeats the rescaling used in Theorem 5.0.1.
For LP⁺ the vectors live in , so the two LP⁺ milestone bounds use . The preprint prints in those calls even though the preceding extension theorem would be applied in dimension . Lemma 5.2.1 is written as an inequality: its printed equality is stronger than the bound established on page 71. These corrections are visible in the theorem titles and notes. Contributions that prove the exact statements, establish the measurability and Gaussian law facts, or formalize the step-to-shadow comparison are welcome.
Reinforcement learning methods must explore in order to find good behaviour, yet the quantity they usually want to evaluate is the value of a different, often deterministic, policy. Off-policy prediction separates the two roles: episodes are generated by a behaviour policy , and the goal is the value function of a target policy . Almost every off-policy method in Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018), and in the literature that follows it, rests on importance sampling: a return observed under is reweighted by the relative probability of its trajectory under and . Section 5.5 of the book introduces the idea for Monte Carlo prediction, §5.6 gives the incremental form of the weighted estimator, and §§5.8–5.9 refine the weights using the internal structure of the return: discounting-aware importance sampling, after Sutton, Mahmood, Precup and van Hasselt (2014), and per-decision importance sampling, introduced by Precup, Sutton and Singh (2000). The book's remarks on the variance of the two estimators (p. 105) cite Precup, Sutton and Dasgupta (2001). Later chapters (7, 11, 12) reuse the same ratios for -step, gradient-TD and eligibility-trace methods.
This mission is the fifth in a series formalizing the book's central mathematical claims. It covers §§5.5–5.9 (pp. 103–115).
A finite Markov decision process has finite sets of states (terminal states included), actions and rewards , and dynamics : for each a probability distribution over next state and reward. The state-transition probability is . A policy gives a distribution over actions in every state.
An episode from a start state is a sequence in which are nonterminal and is terminal. Under it has probability . The return is with discount rate , and the value is the expected return of an episode generated by from .
The behaviour policy covers the target policy if implies . The importance-sampling ratio of decisions is
and the per-decision return weights each reward only by the ratio of the decisions that precede it:
The book writes these objects at a general time and conditions on ; by the Markov property this is the same as starting the episode at , which is what the formal statements do.
For episodes generated by from ,
The first equality is Eq. (5.4) (p. 104); the second is the statement of §5.9 (p. 114).
Eq. (5.4) is the reason the first-visit ordinary importance-sampling estimator (5.5) is unbiased, and it is the template for every importance-sampling correction in the rest of the book. The per-decision identity shows that an estimator with fewer ratio factors per reward, (5.15), has the same expectation, which is the starting point for per-decision and control-variate methods for multi-step off-policy learning (Precup, Sutton and Singh 2000). Example 5.5 shows that unbiasedness says nothing about variance: the ordinary estimator can have infinite variance on a two-action problem, which motivates weighted importance sampling and the incremental weighted update of §5.6.
The results of these sections are classical and proved informally in the book, partly as exercises (5.10, 5.13) left without solution. No machine-checked version exists on the platform: a search for importance sampling, off-policy and per-decision returned no statements. The mission produces a formal trajectory model of an episodic MDP under two policies, which later missions on -step off-policy returns and off-policy traces can reuse.
Eq. (5.4) itself is a termwise identity: for every episode, under coverage. The per-decision identity is not termwise. The later factors of multiply a reward that was received before the corresponding decisions, and removing them requires summing over all continuations of an episode prefix, of every remaining length, and using that each factor has conditional expectation one (5.13) and that the continuation terminates with probability one. The obvious attempt, cancelling the factors episode by episode, fails: on a single episode and differ.
In Example 5.5 the episodes have no length bound, so the expected square is an infinite series over episode lengths whose divergence must be shown directly.
Contributions welcome: proofs of the milestones, a general measure-theoretic version of the trajectory model without the bounded-horizon hypothesis, and variants for action values (Exercise 5.6).
The simplex method solves linear programs very fast in practice, yet for most pivot rules there are inputs on which it takes exponentially many steps (Klee and Minty, 1972, for Dantzig's rule; Goldfarb, 1983, for the shadow-vertex rule). Average-case analyses (Borgwardt, 1980s; Smale, 1983) explained good behaviour on random inputs, but random inputs look nothing like real ones. Spielman and Teng introduced smoothed analysis to close this gap: the input is chosen by an adversary and then perturbed by a small Gaussian, and the running time is measured in expectation over the perturbation. They proved that the shadow-vertex simplex method has smoothed complexity polynomial in the number of constraints , the dimension and (Spielman–Teng, J. ACM 2004; this mission follows the preprint arXiv:cs/0111050v7). The work received the Gödel Prize (2008) and the Fulkerson Prize (2009).
Timeline. Borgwardt (1977–1987) bounded the expected number of shadow-vertex pivots for rotationally symmetric random data. Spielman and Teng (2001, STOC; journal 2004) proved the first smoothed bound, with a shadow bound of order — the theorem of this mission. Deshpande and Spielman (FOCS 2005) improved the shadow bound, Vershynin (2009) reduced the dependence on to polylogarithmic, and Dadush and Huiberts (STOC 2018) obtained for small .
Fix and . The data are vectors , the constraint vectors of the linear program subject to for all . Each is a Gaussian of standard deviation centered at a point with : it has density
and the are independent (joint density ).
For a direction , is the set of index sets with such that is linearly independent, the simplex is a facet of , and lies in the cone . In polar terms, is the set of tight constraints at the vertex of the feasible polyhedron that maximizes .
For linearly independent , the shadow is the set of index sets that belong to for some nonzero . Its size is the number of vertices of the projection of the feasible polyhedron onto the plane ; the shadow-vertex method walks along this polygon, one pivot per vertex. Finally
for every , , every pair of linearly independent , every and all centers of norm at most .
The milestones follow the paper's proof, leaves first.
The result. Theorem 4.0.1 is the geometric heart of the smoothed analysis of the simplex method. Section 4.3 of the paper extends it to arbitrary centers, covariances and right-hand sides, and Section 5 combines these extensions with a two-phase method to show that the simplex method has polynomial smoothed complexity. The same shadow bound underlies later analyses of the simplex method, of perturbed polytopes' diameters, and of condition numbers of random linear programs.
Formalizing it. The theorem has been proved, and improved constants are known, but none of this is machine-checked. A formal proof would verify a long and delicate argument: a change of variables of integral geometry (Blaschke's formula), several conditional-density estimates, and explicit constants in the millions. The mission also produces reusable statements about Gaussian vectors and convex hulls of random points.
The obvious approach is to count, for each candidate facet , the probability that appears in the shadow; there are candidates, so a union bound is exponential in . The paper avoids this by discretizing the angle of (Lemma 4.0.6) and bounding, for each fixed direction, the probability that the optimal facet changes within a small angular step. That needs a lower bound on the angle between and the boundary of its optimal facet, conditioned on the facet being optimal. The conditioning changes the distribution of , so the bound cannot come from the Gaussian density alone. The proof changes variables to the facet's normal , offset and in-plane coordinates (Corollary 2.5.3), whose Jacobian contributes the factors and . It then shows that both the distance of the origin to a face of the in-plane simplex and the angle of incidence are unlikely to be small. Measure-theoretic bookkeeping is as hard as the geometry: densities known only up to normalization, conditioning on events of positive measure, and the measure-zero degeneracies the paper sets aside.
Points live in EuclideanSpace ℝ (Fin d). Constraint vectors are indexed by Fin n (0-based), so the paper's is . The Gaussian of standard deviation centered at is Lebesgue measure with the density above, and the joint law is the product measure. Lemma 4.0.6 also uses Mathlib's multivariateGaussian with a positive definite covariance. Expectations of shadow sizes are lower Lebesgue integrals of -valued counts, and their measurability is part of each conclusion. "Density proportional to " and conditional probabilities are stated cross-multiplied, , so no appears.
The shadow is the set of index sets , and the direction is excluded. Including it would add every facet of to the shadow, since lies in every cone, and make the goal false. is represented exactly in , never by a real infimum. Where the paper omits a hypothesis it uses, it is added and recorded in the item: the standing assumptions , and (Lemma 4.2.3 is false without a bound on ), unit length of the reference vector , , and for strict inequalities. Lemma 2.3.7 is stated with rather than the page's , which fails in an edge case.
Infrastructure a complete development needs: Gaussian tail and chi-square estimates; faces and facets of convex hulls; the Blaschke change of variables and the latitude–longitude change of variables on the sphere (not in Mathlib); surface measure on (Mathlib's Measure.toSphere); and the disintegration of the joint law used in the combination lemma. The Gaussian estimates, the combination lemma and the Blaschke formula are useful beyond this mission. Proofs of any milestone, and of supporting lemmas such as the change-of-variables formulas, 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:
Policy iteration alternates two steps: evaluate the current policy, then replace it by a policy that is greedy with respect to the evaluated action values. The policy improvement theorem guarantees that each greedy step does not make the policy worse, and that the process stops only at an optimal policy. When the action values are estimated from experience rather than computed from a model, as in Monte Carlo control, a greedy policy is a problem: it never tries the actions it does not currently prefer, so their values are never re-estimated. Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., 2018), §5.4, resolve this without the unrealistic assumption of exploring starts by moving the policy only toward a greedy one, to an ε-greedy policy that keeps every action's probability at least ε/|A|.
The question this mission formalizes is whether policy iteration still works under that restriction. The book's answer (pp. 101–102) is yes, in a precise sense: an ε-greedy step never makes an ε-soft policy worse, and it fails to make it strictly better only when the policy is already the best among all ε-soft policies. This is the dynamic-programming fact that justifies on-policy first-visit Monte Carlo control for ε-soft policies, and more broadly every ε-greedy on-policy control scheme that is analysed with exact action values.
A finite Markov decision process has a finite state set S, a finite nonempty action set A used in every state, a finite reward set R ⊂ ℝ and dynamics p(s′, r | s, a) ≥ 0 with . A policy π gives, for each state s, a probability distribution π(· | s) on A. With a discount rate , the state value is the expected discounted return , and the action value is
For ε > 0, a policy is ε-soft if for all s and a. A policy π′ is ε-greedy with respect to if at each state some maximizer of receives probability and every other action receives ; ties among maximizers are broken arbitrarily. A policy π is optimal among the ε-soft policies if it is ε-soft and for every ε-soft π″ and every state s.
The book's analysis uses a new environment with the same states, actions and rewards, in which with probability 1 − ε the chosen action is executed and with probability ε a uniformly random action replaces it:
Its optimal value function is written .
For , , an ε-soft policy π and any ε-greedy policy π′ with respect to ,
The goal is stated in terms of the original MDP and ε-soft policies only; the new environment appears only in the milestones.
The result is what makes ε-greedy on-policy control a form of generalized policy iteration: monotone improvement at every step, and a characterization of where the process can stop. It also locates precisely what is lost by exploring, namely that the fixed point is optimal among ε-soft policies, not among all policies. The value of the new environment is the benchmark against which ε-greedy methods converge when action values are exact.
The book presents the argument informally and states the stochastic policy improvement theorem without proof ("we will not go through the details", p. 79). A formalization supplies the missing proof of the stochastic case, the identification of the best ε-soft policy value with the optimal value of a modified MDP, and the uniqueness of that value. As far as a search of the platform shows, no statement about ε-soft or ε-greedy policies has been formalized there; existing finite-MDP results (Bellman optimality in the Foundations of Machine Learning and Bertsekas series) use different reward models and do not cover the modified environment.
The improvement half follows from (5.2) and the policy improvement theorem, but both need work in the return-based model: the theorem requires comparing infinite discounted sums under two different Markov chains, and (5.2) uses the identity , which is a theorem about returns, not a definition. The equality half is where the obvious argument fails. The deterministic-policy argument of Chapter 4 shows that an unimproved greedy policy satisfies the ordinary Bellman optimality equation; here the unimproved policy satisfies a different equation, and nothing in the original MDP identifies its solution with the best ε-soft value. That identification needs two further facts: every policy of the new environment corresponds to an ε-soft policy of the original one with the same values, and conversely (at ε = 1 only the uniform policy is ε-soft); and the altered optimality equation has exactly one solution.
Everything is stated in the namespace SuttonBartoRL.EpsSoft on a finite MDP with four-argument dynamics, one finite nonempty action set for all states (so , the book's footnote 3, p. 48), and a finite reward set. The conventions are:
Defining as the solution of the Bellman expectation equation, or as the solution of the altered optimality equation, would make milestones 3–5 and the goal's equality half hold by definition; the formalization does neither. The goal is not the statement "" alone: the equality case is part of the book's claim and part of the goal.
The finite-MDP definitions duplicate those of other missions in this series and are expected to be merged later. Useful contributions include the Neumann-series identity , the Bellman expectation equation, the contraction property of Bellman operators, and the correspondence between policies of the new environment and ε-soft policies of the original one; these are reusable for the other finite-MDP missions of the series.
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.