Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A group of individuals each hold a subjective probability distribution over the same outcomes, and one wants a single distribution representing their consensus. Averaging and convolution are the obvious candidates. Eisenberg and Gale (Ann. Math. Statist. 30(1), 1959) observe that a real institution already performs such an aggregation: the pari-mutuel method of betting on horse races, in which the final "track's odds" on a horse are proportional to the total amount bet on it.
The difficulty is circular. Each bettor wants to bet where the ratio of their own probability to the track probability is largest, but the track probabilities are only known after everyone has bet. The paper asks whether track probabilities and bets compatible with both the bettors' strategies and the pari-mutuel principle exist, and whether they are determined by the data. It answers yes on both counts for the probabilities, which gives a well-defined notion of pari-mutuel consensus.
The variational problem the paper introduces, maximizing , is now known as the Eisenberg–Gale convex program. It is the standard tool for computing equilibria of linear Fisher markets, and the pari-mutuel market is the special case in which every bettor's utility for a horse is their subjective win probability.
There are bettors and horses .
Unknowns are Greek. is the track probability of and is the amount bets on . Nonnegative are equilibrium probabilities and bets when
(1) is the budget relation, (2) the pari-mutuel condition, and (3) says each bettor bets only on horses that maximize the subjective expectation .
The paper's variational problem is
with where an inner sum vanishes. From a maximizer it builds (6) and (7). In Lean the market is PariMutuel.Consensus.Market m n, equilibrium is Market.IsEquilibrium, and , , the maximizer predicate, (6) and (7) are Market.phi, D m n, Market.IsPhiMaximizer, Market.trackProb, Market.bets.
Only is unique; the paper notes that equilibrium bets need not be.
A further, non-milestone item states the referee's example (p. 168): with two bettors of equal budgets and two horses, if the first bettor's distribution is , the equilibrium probabilities are whatever the second bettor believes.
The result makes pari-mutuel odds a well-defined function of the bettors' beliefs and budgets, so the consensus can be studied as a mathematical object; the referee's example shows it behaves very differently from averaging, since a single indifferent bettor can fix it. The existence proof replaces a fixed-point argument by a concave maximization, which is the origin of the Eisenberg–Gale program, later the basis of convex-programming and combinatorial algorithms for Fisher market equilibria.
The theorems are classical and fully proved in the paper. To the knowledge of this mission they have no machine-checked proof. The mission produces a formal pari-mutuel market model, the Eisenberg–Gale program with the correct treatment of , and Lean proofs of existence and uniqueness. The platform's Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities missions (Vazirani–Yannakakis) concern a related Fisher-market model with rational piecewise-linear utilities.
The existence statement, as the paper proves it, has two delicate points. is on part of the boundary of , so "continuous on a compact set" needs the extended-real reading, and a real-valued formalization must handle the boundary separately. The first-order condition (8) has to be derived from maximality on a polytope with equality constraints on columns, not from an unconstrained critical point.
For uniqueness, the natural first idea, strict concavity of , fails: is concave but not strictly concave in , and indeed equilibrium bets are not unique. Uniqueness has to be proved for the probabilities directly, for arbitrary equilibria and not only those built from a maximizer, and it needs positivity of all , which the paper uses without proof.
Fin m and horses Fin n, indexed from 0. All data are real. Every standing assumption (rows of are probability vectors, no zero column, , ) is a field of Market; follows from .Finset.sup' over the nonempty set of bettors.Many regression problems have far more unknown coefficients than observations : gene expression studies with tens of samples and thousands of genes, imaging from few measurements, nonparametric curve recovery from a finite number of noisy samples. Estimation is hopeless in general, but becomes possible when the parameter is sparse, that is, has few nonzero entries. Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) proposed the Dantzig selector, an estimator computed by a single linear program, and showed that its squared error is within a logarithmic factor of what an oracle that knew which coefficients matter could achieve.
The estimator became one of the two standard methods for high-dimensional regression, alongside the Lasso; the comparison of the two by Bickel, Ritov and Tsybakov (arXiv:0801.1095, 2009) is built on it. This mission targets the paper's main result, the oracle inequality (Theorem 1.2). A companion mission covers the simpler bound for sparse parameters (Theorem 1.1).
Observations follow the linear model
where is a deterministic design matrix with columns , each of Euclidean norm ; is an unknown deterministic parameter; and has independent coordinates, . The vector is -sparse if at most of its entries are nonzero.
Two constants of measure how close sparse sets of columns are to being orthonormal. The restricted isometry constant is the smallest such that for every supported on at most indices. The restricted orthogonality constant (defined for ) is the smallest with whenever are supported on disjoint sets of sizes at most and . Below and .
For a tuning level , a Dantzig selector is any solution of
The ideal mean squared error is : the risk of an oracle that keeps exactly the coordinates above the noise level.
Let , , and . If is -sparse and , then with probability exceeding every Dantzig selector obeys
with the explicit constant (1.14)
The result. Theorem 1.2 says that a single linear program, which knows neither the support of nor which coefficients exceed the noise, matches the oracle risk up to a factor , uniformly over -sparse parameters and with explicit, nonasymptotic constants. For coefficients well below the noise level it is far sharper than the bound of Theorem 1.1. It is the template for later oracle inequalities for -penalized estimators under restricted isometry or restricted eigenvalue conditions.
Formalizing it. The theorem is proved in the paper, but parts of the argument are only sketched: Corollary A.2 refers to the 2005 Decoding by Linear Programming paper for its convergence argument, and Corollary A.3's bound is printed with a constant its own proof does not deliver. A machine-checked proof settles these steps. The restricted isometry and orthogonality constants used here are already published on the platform from the decoding series; the appendix lemmas on dual vectors are reusable for any compressed-sensing result in that framework. No formalization of the Dantzig selector's oracle inequality is known to us.
The natural proof compares with the hard-thresholded parameter that keeps only the large coefficients: if were feasible for the Dantzig constraint, the analysis of Theorem 1.1 would apply directly. It is not feasible in general, because the small coefficients , though individually below the noise level, can add up to a large correlation . The central difficulty is to split into a part with controlled and norm and a part invisible to the constraint; this requires constructing dual vectors with prescribed correlations (Lemma A.1, Corollary A.2), via an iterative, geometrically convergent correction. The probabilistic part is a Gaussian tail estimate plus a union bound, and the bookkeeping of constants must be carried through exactly.
Vectors are functions Fin p → ℝ, the design is Matrix (Fin n) (Fin p) ℝ, and the noise is a family z : Fin n → Ω → ℝ of mutually independent random variables (iIndepFun) each with law gaussianReal 0 σ². and are the published CandesTao.Decoding.restrictedIsometryConst X (2*S) and restrictedOrthogonalityConst X S (2*S) (infima, absolute value in the orthogonality condition). Domain: and (the paper defines for ), which forces and . A Dantzig selector is any minimizer over the feasible set; the constraint is a bound on every coordinate.
The goal bounds from above the (outer) probability of the bad event "no Dantzig selector exists, or some Dantzig selector violates (1.13)". Because the event includes non-existence, a definition no vector satisfies cannot make the theorem vacuous; and the constant is the printed (1.14), evaluated at , of , not a free constant chosen after the fact.
Corrected constant: Corollary A.3 is stated with , the bound its proof gives once Corollary A.2 is applied at an integer sparsity level; the printed statement omits the factor . Corollary A.2 carries Lemma A.1's standing hypothesis . The deterministic lemmas (3.1, 3.2, A.1–A.3) assume nothing about column norms, since their statements do not need it.
Useful infrastructure: monotonicity of and in their indices (the proof applies the lemmas at a smaller sparsity level), the Gaussian tail bound , existence of minimizers of the Dantzig linear program, and a sorting/blocking toolkit for "the largest positions". Proofs of individual milestones are welcome independently.
The gradient method minimizes a differentiable function on by moving from the current point along the negative gradient, . Every practical implementation has to choose the step . A fixed step requires knowing a Lipschitz constant of ; an exact line search is expensive. Larry Armijo's four-page note (Pacific J. Math. 16 (1966) 1–3) proved that any step achieving a sufficient decrease proportional to yields convergence, and gave the halving rule that is now called the Armijo rule or backtracking line search. The rule is the default step-size strategy of gradient, quasi-Newton and Newton-type methods in textbooks such as Nocedal–Wright and Bertsekas, and its sufficient-decrease test reappears in essentially every later line-search analysis.
Timeline:
Let be real Euclidean -space with norm , and let be continuous and bounded below. For a fixed the level set is . Write for the gradient of at . " on " means that is differentiable at every point of and is continuous there.
with when the set is empty. Condition IV forces to be the unique minimizer and the only stationary point in .
For and , the sufficient-decrease set of display (1) is
The steepest descent algorithm uses . The modified steepest descent algorithm fixes , sets , and takes with the smallest positive integer such that
Assume is continuous and bounded below and Conditions III and IV hold at . If , then for every
and every sequence with first term and for all satisfies
The theorem separates the analysis of a gradient method from the choice of its step: whatever rule produces steps in converges, and the two corollaries show that both a fixed step and a halving search started from an arbitrary qualify. The halving rule needs no knowledge of , which is why it became the standard globalization device for descent methods. The hypotheses are local to the level set: need only be Lipschitz on , not on all of , so functions whose gradient is only locally Lipschitz, such as polynomials of degree above two with bounded level sets, satisfy Condition III.
The result is classical and proved on the page; it has not, to our knowledge, been machine-checked in this form. Formalizing it provides a verified sufficient-decrease convergence theorem with level-set-local hypotheses, a verified Armijo backtracking rule with explicit constants , and , and reusable definitions (sufficient-decrease set, Armijo test with halving steps) on which later line-search results can build.
The mean value step in the proof of the descent inequality silently uses the Lipschitz bound along the whole segment from to , but Condition III gives it only on . One has to show that the segment cannot leave the closed set for ; replacing the hypothesis by a global Lipschitz condition is not acceptable, because it changes the theorem. The final step needs Condition IV in its exact form: gradients tending to zero along the iterates do not by themselves give convergence of the iterates, and the positive lower bound away from is what turns stationarity into convergence. Corollary 2 additionally requires a termination argument for the halving search and a uniform lower bound on accepted steps.
is EuclideanSpace ℝ (Fin n), is the norm and is Mathlib's gradient f. All declarations live in the namespace ArmijoGrad.Conv, with one definition file ArmijoGrad.Conv.Setting.
Committed conventions:
Continuous f, BddBelow (Set.range f), ConditionIII f x0 K, ConditionIV f x0 xstar. Milestones keep only the assumptions their claim uses, which makes them more general; nothing is added.gradient f on . The Lipschitz bound of Condition III holds on only; is part of Condition III.ℕ → EuclideanSpace ℝ (Fin n) with first term equal to , the base point of , as in the paper's notation.A trivializing formalization is ruled out: the goal assumes nothing about , the descent inequality or , Condition IV cannot hold vacuously because it names a minimizer, and all hypotheses are satisfiable by nontrivial data: satisfies Conditions III and IV with and , and both algorithms have runs for it.
A complete development needs the one-dimensional mean value inequality along a segment, a continuity argument keeping the segment in , the telescoping bound for monotone sequences bounded below, and the halving-search termination. The definitions file and the descent and Armijo-index lemmas are reusable for later line-search missions. Contributions are welcome on every milestone; the descent inequality is the natural first target.
A Markov decision problem models a system that is observed once per period and controlled by choosing an action: the action earns an immediate income and determines the probabilities of the next state. Inventory control, machine replacement, queue admission and many reinforcement-learning benchmarks are of this form. With future income discounted by a factor , Howard (Dynamic Programming and Markov Processes, 1960) showed how to compute an optimal policy by policy improvement. The undiscounted problem () is harder, because total income is typically infinite.
David Blackwell's Discrete Dynamic Programming (Ann. Math. Statist. 33 (1962) 719–726) treats as a limit of . Its Theorem 5 shows that some stationary policy is optimal simultaneously for all discount factors sufficiently close to . Such policies are now called Blackwell optimal, and the result is the base of sensitive discount optimality (Veinott, 1969) and of the standard textbook treatment of average-reward problems (Puterman, Markov Decision Processes, 1994, Ch. 10).
Timeline. Howard (1960): policy iteration for discounted and average-reward finite problems. Blackwell (1962): Theorem 5 (Blackwell optimal stationary policies exist) and the characterization of nearly optimal stationary policies (Theorem 4, the subject of the companion mission). Miller and Veinott (Ann. Math. Statist. 40 (1969) 366–370), Veinott (Ann. Math. Statist. 40 (1969) 1635–1660): Laurent expansions of in and -discount optimality.
There are finitely many states and a finite set of actions, every action available in every state. In state , action yields income (any sign) and moves the system to state with probability ; each is a probability vector.
A decision rule is a function from states to actions; is the finite set of decision rules. A policy is a sequence in : on day , in state , action is used. Policies are deterministic and Markov but may change with time. The policy uses on day and then follows ; uses every day and is called stationary.
For , is the vector and the Markov matrix . With and , the return of at discount factor is
a vector indexed by the initial state. Vectors are compared coordinatewise; means and .
A policy is -optimal if for every policy . Following §4 of the paper, a policy is optimal if it is -optimal for all sufficiently near .
There exist a decision rule and such that
One and one serve every competing policy and every .
The result. Theorem 5 shows that the infinitely many discounted problems near share a common optimal stationary policy. Such a policy is also optimal for the long-run average criterion, which settles the existence of average-optimal stationary policies in finite models without any recurrence assumption. It also justifies computing undiscounted solutions as limits of discounted ones, and it is the first case of the sensitive optimality criteria developed later.
Formalizing it. The theorem is classical and proved in the paper and in the textbooks; there is no machine-checked proof of it in Blackwell's model on the platform. A related open item, SennottDP.AvgFinite.prop_6_2_3_blackwell_optimal, states the textbook version for nonnegative costs and randomized history-dependent policies; the present mission is Blackwell's own formulation with incomes of either sign and deterministic Markov policies. A complete development also yields a verified policy improvement theorem (Theorem 3) and the rationality of discounted values in , both reusable for any finite-state discounted model.
The Corollary gives, for each , some optimal stationary policy, and is finite, so one is -optimal for infinitely many accumulating at . The obvious argument stops there: optimality on a sequence of 's says nothing about the 's in between, and a pointwise limit argument cannot produce a whole interval . The step that fails is passing from "frequently" to "eventually", and it needs structural information about how depends on , not just continuity. A second difficulty is the comparison class: optimality must hold against all time-dependent policies, not only the finitely many stationary ones, so the final step has to bring the Corollary back in for every near .
States and actions are finite nonempty Lean types St, Act; decision rules are functions St → Act and policies are sequences ℕ → St → Act, indexed from (π 0 is Blackwell's ). Incomes are real-valued with no sign restriction. The law of motion law s a s' satisfies the published predicate IsTransitionKernel. is the ordered matrix product and is the tsum of the series, which converges absolutely for ; every statement at a fixed assumes , and nothing is stated for . Vector inequalities are coordinatewise, and the strict order is " and ", not coordinatewise strict. " sufficiently near " is "there is such that for every ". The paper's §4 phrase is encoded as -optimality, so no supremum over policies appears.
The word "optimal" has two meanings in the paper: at one fixed (§3, the Corollary) and for all near (§4, Theorem 5). The Lean development keeps them apart as IsBetaOptimal β and IsOptimal. A statement of Theorem 5 at a single , with "there exists ", for a set of 's accumulating at , or against stationary policies only would be a different and weaker theorem; the goal rules all of these out.
Needed infrastructure: summation and shifting of the discounted series, Neumann series for stochastic , Cramer's rule to express as a ratio of polynomials in , and the fact that a nonzero polynomial has finitely many roots. The policy improvement theorem and the rationality lemma are reusable beyond this mission. Proofs of individual milestones are welcome independently.
Selfish routing and resource sharing are modelled by congestion games: each player picks a set of shared resources, and the cost of a resource grows with the number of players using it. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures how much worse the social cost of a worst Nash equilibrium is than the optimum. For non-atomic (infinitesimal) traffic with linear latencies, Roughgarden and Tardos (J. ACM 2002) showed the ratio is . Christodoulou and Koutsoupias (STOC 2005) turned to finite (atomic, unweighted) congestion games, where each of players controls one indivisible unit of load, and determined the pure price of anarchy for linear latencies in four settings: asymmetric or symmetric strategy sets, and average or maximum social cost. Awerbuch, Azar and Epstein (STOC 2005) obtained the value for the asymmetric average case independently.
This mission covers the symmetric average-cost entry of that table (Sect. 3.2 of the paper). It shows that when all players share one strategy set, the ratio is not but , which depends on the number of players and tends to only as .
A congestion game has a finite set of players (in Lean, Fin N), a finite set of facilities , for each player a collection of pure strategies , and for each facility a latency . A profile picks for each player (IsProfile). The load is the number of players whose strategy contains (load), the cost of player is
(cost), and the social cost is (sumCost), times the average cost. A profile is a pure Nash equilibrium (IsPureNash) if for every player and every , where replaces by .
Latencies are linear (IsLinear) when with . The game is symmetric (IsSymmetric) when all players have the same strategy set, . The pure price of anarchy of a class of games is the supremum, over games in the class and pure Nash equilibria , of , with .
For every : every pure Nash equilibrium of every symmetric linear congestion game with players satisfies
and some symmetric linear game with players has a pure Nash equilibrium and a profile with and equality. Together these state that the pure price of anarchy of the class is exactly .
The result separates symmetric from asymmetric games for every finite number of players: for the symmetric bound is , for it is , against for asymmetric games with players. Theorem 4 shows the bound is tight, so the function is the exact answer, not an artefact of the proof. The asymptotic value coincides with the asymmetric one, which says that symmetry helps only by a vanishing amount for large populations. Later work on smoothness arguments (Roughgarden, STOC 2009) takes the bound of this paper as its central example.
The theorems are proved in the paper; the authors print the proofs for identity latencies and state that they extend to . No machine-checked proof of these bounds is known to exist. This mission produces a statement for general affine latencies with nonnegative coefficients, the affine forms of the intermediate inequalities, and an explicit family of instances for every , all of which are reusable for the other entries of the paper's table.
The upper bound requires combining the deviation inequalities (player against the strategy of each player in the comparison profile) and then bounding cross terms facility by facility; the step that needs care is that the bound of Lemma 1 holds for integer loads only and fails for real numbers, so any argument that relaxes loads to reals loses the constant. The asymmetric argument, which compares player only with its own optimal strategy , gives and cannot see the dependence on .
For the lower bound, the instance must be a Nash equilibrium against every strategy in the common strategy set, which contains the equilibrium strategies of all other players as well as the optimal ones. Exact equality of the ratio requires the block sizes to be tuned to ; verifying the equilibrium condition involves counting facilities shared by pairs and triples of players.
Players are Fin N with ; facilities are an arbitrary finite type with decidable equality; strategies and profiles are Finsets of facilities, with feasibility a separate predicate. Latencies are real-valued functions of the natural-number load. Linear latencies are affine with nonnegative coefficients, as in Sect. 2 of the paper; the milestone inequalities carry the coefficients explicitly and reduce to the printed displays when , . The Nash condition is in cost form. Upper bounds are stated against every feasible profile , which is equivalent to the bound on without dividing by . All constants are computed in .
The lower bound requires : without it the statement is satisfied by zero latencies or empty strategies, where both sides vanish. Symmetry is a hypothesis of the upper bound and a property of the instance; without it the upper bound is false, since asymmetric instances reach .
A complete development needs finite-sum manipulations (double counting ), the integer inequality of Lemma 1, and an explicit facility type for the instance. The model layer is shared with the other missions of this series. Proofs of the milestones and alternative proofs of the bound are welcome.
A reproducing kernel Hilbert space (RKHS) is a Hilbert space of functions in which evaluation at each point is a continuous functional. Each such space is determined by its kernel, and in practice spaces are usually given by their kernels: Gaussian or Sobolev kernels in kernel methods and Gaussian-process regression, the Bergman and Szegő kernels in complex analysis. A recurring question is therefore how a relation between two function spaces reads on their kernels. When is one space contained in another? When do two kernels define the same space?
N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) answers both questions. §7 (pp. 354–356) compares a class with a contractively included subclass. §13 (C) (pp. 382–383) uses Banach's closed graph theorem to remove the contractivity assumption. The answer is an order relation between kernels, checkable on finite point sets. It is the standard tool for comparing RKHSs: Part II of the paper (§2, p. 387) applies §7, Theorem II to compare Bergman kernels of nested plane domains.
Let be an arbitrary set (no topology, no measure). A function is a positive matrix if
for every finite family and every . For two kernels, means that is a positive matrix.
A class with a reproducing kernel is a complex Hilbert space of functions for which there is a function with and for all and . The scalar product is linear in . Every such is a positive matrix, and by Moore's theorem (§2 (4)) every positive matrix is the kernel of exactly one such class. A linear class of functions is an (R.K.)-class if some norm makes it a Hilbert space with a reproducing kernel. Such a class carries many admissible norms, and correspondingly many kernels.
In the Lean development, is a Mathlib RKHS ℂ H X ℂ instance on a complete complex inner product space H. The class of functions is Set.range (⇑ : H → X → ℂ). The scalar kernel is kernelFn H x y = RKHS.kernel H x y 1, and is AronszajnRK.Limits.KernelLE K₁ K (the series' shared definition).
For classes with reproducing kernels :
The constant is left unspecified: it measures the norm of the inclusion operator and has no canonical value.
The result. Corollary IV₂ reduces inclusion of infinite-dimensional function spaces to positivity of finite matrices. Corollary IV₃ says when two kernels give the same space, as sets of functions with equivalent norms. Kernel-method theory uses these facts to compare hypothesis spaces of different kernels. In complex analysis they compare Bergman spaces of nested domains, since the restricted kernel of a larger domain is dominated by the kernel of a smaller one (Part II, §2, p. 387, of the paper). Theorem VI makes (R.K.)-classes a lattice under intersection and sum.
Formalizing it. All statements are classical and have been proved since 1950. To our knowledge none is machine-checked. Mathlib has RKHSs, their kernels, positive semidefiniteness of kernels and the construction of a space from a kernel. It has no comparison theorem between two RKHSs, and no characterization of an RKHS by its kernel up to inclusion or equality of function sets. This mission adds these. As a by-product it produces the closed-graph argument for RKHS inclusions in a form that other missions can reuse.
The sufficiency direction () does not follow from the definitions alone. Domination is a statement about finite quadratic forms; membership of a function of in is a statement about an infinite-dimensional space, and nothing pointwise connects the two. The paper's argument rests on the sum theorem of §6, the goal of a separate mission in this series.
The necessity direction cannot start from an assumed norm inequality, because the two norms are a priori unrelated. Producing the constant needs the closed graph theorem together with the fact that norm convergence in an RKHS implies pointwise convergence. A direct estimate of against from the inclusion alone has no route to a uniform constant.
RKHS ℂ H X ℂ instance on a complete complex inner product space H. The function of f : H is ⇑f.⟪f, g⟫_ℂ is conjugate-linear in f, so Aronszajn's is ⟪g, f⟫_ℂ, and the reproducing property is ⟪k y, f⟫_ℂ = f y.Matrix.PosSemidef over the index type X. Its quadratic form over finitely supported vectors is exactly the paper's. Over it includes Hermitian symmetry, which nonnegativity implies. is fun x y => (M : ℂ) * K x y with real .RKHS instance, since having a kernel is the conclusion. It is a complex Hilbert space with an injective linear map into the functions of .Trivializations ruled out. No statement defines a class as RKHS.OfKernel K and then asserts that its kernel is K. Classes are always compared through their sets of functions and norms. "" is never weakened to the existence of some injection .
Substrate. Mathlib's RKHS, RKHS.kernel, RKHS.kerFun, RKHS.kerFun_inner, RKHS.posSemidef_kernel, RKHS.OfKernel, Matrix.PosSemidef (with .add, .smul), Banach's LinearMap.continuous_of_isClosed_graph, and the continuous functional calculus (CFC.sqrt, for the square root in the proof of Theorem II). The sum theorem of §6, used in the proof of Theorem I, is the goal of mission I of this series. Contributions of that theorem and of reusable lemmas on RKHS inclusions are welcome.
Shadow tomography asks for predictions of many specified measurements of an unknown quantum state, while using as few prepared copies of that state as possible. The requested output is a list of acceptance probabilities, not a full description of the state. A procedure might exploit the fact that these are only numbers, even when the state has dimension . The natural question is how far this saving can go. Aaronson's paper gives upper bounds and separates two sources of difficulty: one already present for ordinary probability distributions, and one arising from noncommuting quantum measurements.
This mission concerns the first source. It formalizes Theorem 16, which says that even when the state and every requested measurement are diagonal in the same basis, the number of copies must grow with in the relevant asymptotic regime. In that special case, the unknown state is an ordinary distribution on outcomes. The theorem therefore puts a limit on any proposed improvement to shadow tomography that would promise fewer copies in all instances.
A mixed state on a -dimensional system is a positive semidefinite complex matrix with trace one. A two-outcome measurement is represented by an effect satisfying ; it accepts with probability . When is diagonal, its diagonal entries are the probabilities of the basis outcomes. When is diagonal too, it specifies a randomized yes-or-no test on those outcomes. These conventions are stated in Section 3 of the paper.
Given effects , a shadow-tomography strategy measures independent copies and outputs estimates . It succeeds on when every estimate differs from by at most . The lower bound requires success probability at least for every diagonal mixed state. The strategy may make a joint quantum measurement on all copies and may choose its estimates from its observed outcome. This is the same measurement model used in Problem 1.
The goal is the classical clause of Theorem 16. There are absolute constants and such that, for , , and , there are diagonal effects with 0/1 entries, corresponding to the known Boolean functions in Section 6.1, for which every strategy successful on all diagonal states must use
The hard measurements are chosen before the strategy is quantified. The statement therefore also rules out a strategy with a smaller copy count that works uniformly for all quantum states and measurements. Its constants and threshold express the notation in Theorem 16, rather than specifying a numerical optimum.
Four milestones come from the proof on pages 20–21: the high-probability overlap bound for independently chosen half-size subsets (Eq. (1)); the acceptance probability of a subset under its associated biased distribution; an upper bound on the mutual information between the hidden subset index and the observed samples; and the exact entropy formula with a quadratic entropy deficit. These statements expose the combinatorial and information-theoretic parts of the lower bound while leaving the goal as the paper's copy-complexity result.
Theorem 16 sets a floor for shadow tomography that survives even when all operators commute. Any uniform copy bound for the full quantum task must respect this floor. The result also distinguishes the difficulty of predicting many properties of a distribution from the extra difficulty possible for noncommuting states and measurements, which the paper treats in a separate lower bound. Section 6 presents both bounds.
A complete formalization would give machine-checked statements and proofs for the finite subset construction, the entropy calculation, the information inequality, and the reduction from a successful quantum measurement procedure on diagonal states to a lower bound on . The theorem is proved on paper; these draft statements are open Lean goals and do not claim that its proof has been machine checked. The finite-distribution and information-theory infrastructure is reusable for other lower bounds based on hidden-index families.
Counting how many possible measurements there are does not by itself show that samples reveal enough about which distribution generated them. The lower bound needs a quantitative relation between estimation accuracy and information about a hidden index, while each individual sample carries limited information. The paper's printed overlap condition (1) is too weak for the next displayed estimate: at its boundary it gives . The milestone preserves Eq. (1) as printed; closing the goal requires the correspondingly sharper overlap fact with , which follows from the same type of concentration statement after adjusting its constant. The printed assertion that learning the index requires mutual information at least is also imprecise at success probability ; a quantitative decoding inequality is needed. Neither incorrect display is a draft milestone.
Matrices are indexed by Fin D. WildeQIT.IsDensityOperator supplies the mixed-state predicate and . Diagonal states and effects use the standard matrix diagonal predicate. An effect is positive semidefinite together with its complement. The tensor power uses functions Fin k → Fin D as basis indices; at it is a one-by-one identity matrix. A strategy is a finite-outcome POVM on that tensor power, followed by a real estimate vector for each outcome. The output values are not restricted to : clipping them to this interval cannot worsen an estimate of a probability. No restriction to classical estimators is placed in the goal; that would change the allowed strategies before the theorem has been proved.
The asymptotic threshold excludes the one-dimensional and single-measurement corners where the claimed rate does not describe the problem. The bound keeps the biased distributions used on page 20 nonnegative; would permit a zero-copy constant estimate. Subset milestones require even or explicitly require a half-size subset, so has its intended meaning. The natural logarithm appears nowhere in the lower-bound rate; entropy, mutual information, and use base two. At zero probability the entropy convention is .
The finite distributions, entropy, conditional entropy, and mutual information reuse the published WildeQIT definitions. Contributions that prove the four source milestones, establish the sharper overlap fact, or supply the quantitative decoding step are welcome. The goal must retain its order of quantifiers: one hard measurement family, then every strategy, with success demanded on every diagonal state.
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.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the cutoff-90 mission already covers every , the new work is the range from 89 to 90.
The argument for was reached by tightening its estimates step by step, starting from 256. With its current choices those estimates stop working below 90, and nobody has yet found a way past that point. It is not known whether 90 is a real limit of the method or only of the choices made so far, so this mission is the smallest test of whether the cutoff can move at all. The accepted proof for and its research note are the natural starting point. The goal theorem below gives the exact statement.
This is an open entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 89 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryGradient methods are the workhorse of large-scale nonlinear optimization and of the training of statistical models. In practice the direction actually used is rarely the exact negative gradient: it may be scaled, computed incrementally one data component at a time, or perturbed by approximation error. The classical convergence theory of such methods often assumes that the iterates stay bounded, that the objective is bounded below, or that the errors vanish at a prescribed rate, and these assumptions must then be checked separately for each method.
Bertsekas and Tsitsiklis (2000) proved convergence results for gradient methods with errors that need none of these assumptions. Their deterministic result (Proposition 1) allows a general descent direction together with an error whose size is proportional to the stepsize, and concludes that either the objective values diverge to or they converge and the gradients tend to zero. It applies, among others, to the incremental gradient method for a sum of functions (Proposition 2 of the same paper), which underlies backpropagation-style training. The stochastic counterpart (Proposition 3, zero-mean errors) is the subject of a companion mission.
Throughout, is a continuously differentiable function whose gradient is Lipschitz continuous: for some constant ,
Here is the Euclidean norm and the standard inner product. The gradient method with errors generates a sequence of iterates
where is the stepsize, is a descent direction and is an error vector. Nothing is assumed about how and are produced, beyond the two conditions below, which hold for some positive scalars and every :
The stepsizes are diminishing in the standard sense:
A stationary point of is a point with ; a limit point of is the limit of some subsequence.
Under (2.1), (2.2), (2.3) and the stepsize conditions, either
or else converges to a finite value and
Furthermore, every limit point of is a stationary point of .
The milestones follow the paper's own argument, in order.
The result. Proposition 1 separates two concerns that are usually entangled: what the method guarantees, and what must be known about . It concludes stationarity of all limit points and convergence of the gradients to zero without assuming that the iterates are bounded or that is bounded below; when is bounded below the first alternative is excluded and follows outright. Because need not be the negative gradient and need not vanish faster than the stepsize, the result covers scaled gradient methods, incremental gradient methods for sums of functions, and gradient methods with deterministic approximation error. The descent inequality (2.4) and the deterministic supermartingale-type Lemma 1 are standard tools that recur throughout optimization theory.
Formalizing it. The proposition is proved in the paper; it has not been machine-checked. A formal proof would give a reusable, verified convergence theorem for a broad class of first-order methods on , together with a formal descent lemma for functions with Lipschitz gradient, which Mathlib does not currently state in this form, and a deterministic Robbins–Siegmund-type lemma for sequences.
The summability estimate (2.6) gives only . Passing to is the main step: the obvious argument (a summable series with forces the gradient norms to zero) is false in general, because a nonnegative sequence with these two properties may still have infinitely many large terms. What is missing is a bound on how far can travel while the stepsizes are small, and only (2.1) and (2.2)–(2.3) together supply it. A second difficulty is that there is no boundedness of the iterates: every estimate must hold globally, and the error is controlled only relative to , which may be unbounded along the sequence.
EuclideanSpace ℝ (Fin n), is the real inner product ⟪x, y⟫_ℝ, and is Mathlib's gradient f; the hypothesis ContDiff ℝ 1 f makes it the true gradient. The paper's statement is for and the formalization does not generalize to Hilbert spaces.LipschitzWith L (gradient f) with L : ℝ≥0; this is equivalent to (2.1) for some real constant.Contributions welcome: proofs of the descent lemma and Lemma 1 (both reusable well beyond this mission), and of the steps (2.5)–(2.6) and the excursion argument.
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.
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Salikhov's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (7.606309 : ℝ), i.e. .
Value. The bound is quoted as (e.g. by Zeilberger–Zudilin), a truncation. This entry rounds the last digit up to .
Salikhov uses integrals of rational functions that are symmetric under a group of transformations (in the spirit of Rhin–Viola), which gives larger arithmetic savings in the common denominators than Hata's construction.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Zeilberger–Zudilin's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (7.103205334138 : ℝ), i.e. .
Value. The paper states its bound as , a truncation. This entry rounds the last digit up to so that the goal follows from the published proof.
Zeilberger and Zudilin modify Salikhov's integrals and use the Almkvist–Zeilberger algorithm (creative telescoping) to find recurrences for them, then optimise the arithmetic and analytic estimates. This is the current record.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Hata's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (8.016046 : ℝ), i.e. .
Value. The paper computes the exponent as and states the rounded bound . This entry rounds the computed value's last digit up to , which is still below the paper's and above .
Hata obtains simultaneous approximations to from complex contour integrals of Legendre type, with extra arithmetic savings from primes that divide the coefficients to a predictable extent. His linear-form measure is , giving (stated in the paper as ). It stood as the record for about fifteen years.
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
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.
Many problems in signal processing, statistics and machine learning take the additively separable form
a smooth term plus a nonsmooth but "simple" term , such as an penalty or the indicator function of a convex constraint set. The forward-backward method alternates a gradient step on with a proximal step on . Beck and Teboulle's FISTA (Beck–Teboulle 2009) combined it with Nesterov's acceleration and improved the worst-case rate for function values from to . Whether the iterates of the accelerated scheme converge at all, and not just their function values, remained unsettled for a long time; in the words of Attouch and Peypouquet, it "puzzled researchers for over two decades".
Timeline.
The case , the original choice of FISTA, is not covered by this result.
Let be a real Hilbert space with scalar product and norm .
Given and , algorithm (2) generates by
The auxiliary sequence (6) is . For a point , the proof of Theorem 3 uses
A sequence converges weakly to , written , if for every .
In Lean these are theta, extrap (), IsAccelFBRun and zSeq (shared definitions in the namespace NesterovFB.Rates), and deltaSeq in the namespace NesterovFB.Weak. The predicates IsProperClosedConvex and IsProx and the predicate WeakTendsto are reused from the platform.
Under the assumptions above, with and ,
The limit is required to be a minimizer of ; weak convergence to an arbitrary point would be a weaker statement.
For every and :
The result. Theorem 3 shows that the accelerated forward-backward method with behaves like the unaccelerated method in one important respect: its iterates converge to a solution rather than just producing small function values. In infinite-dimensional settings (inverse problems, PDE-constrained optimization, signal recovery in function spaces) weak convergence is the natural notion, and strong convergence can fail. The four milestones are the steps that matter for other analyses too: a "Fejér-type" step inequality from the extrapolated point, and the convergence of the distance to every minimizer.
Formalizing it. The result is proved in the literature; no machine-checked proof of it is known. A complete formalization needs the energy estimates of the paper's §1.1–1.2 (summability of , boundedness of , and the convergence of ), which a companion mission poses separately, and Opial's lemma, which is not in Mathlib.
The unaccelerated forward-backward method is Fejér monotone: decreases for every minimizer , and Opial's lemma applies directly. The accelerated iterates are not Fejér monotone. The first milestone only compares with the extrapolated point , and can exceed by the inertial term. The quantity therefore satisfies only a second-order inequality with coefficients that grow in . The obvious attempt, to show that is eventually monotone and apply Opial's lemma as for the unaccelerated method, fails.
A second difficulty is the passage from distances to weak convergence: in a Hilbert space this needs the weak sequential compactness of bounded sets and the weak lower-semicontinuity of (to place weak cluster points in ).
InnerProductSpace ℝ H, CompleteSpace H), not ; in finite dimensions weak and strong convergence coincide and the goal would be a different, weaker theorem.EReal; is never assumed real-valued.WeakTendsto, not convergence in norm.A trivializing formalization is ruled out by the sanity check: the hypotheses are jointly satisfiable, and the goal asks for weak convergence to a minimizer, so neither a vacuous hypothesis nor an arbitrary limit point is admitted.
Infrastructure that a complete development needs, and that is reusable beyond this mission: the descent inequality (9) of the proximal-gradient operator, Opial's lemma in a real Hilbert space, the weak lower-semicontinuity of proper lower-semicontinuous convex functions, and the lemma that a bounded real sequence whose positive increments are summable converges. Contributions of any of these are welcome.
Convex duality in optimization rests on one transformation: to a convex function one associates the function , which records, for each slope , the best affine lower bound of with that slope. Lagrangian duality, the duality theory of linear and conic programming, the analysis of first-order methods through smoothness and strong convexity of conjugates, and the dual representations of risk measures and divergences all read off properties of from properties of . Each of these uses needs one fact: that the transformation loses no information, so that applying it twice returns .
That fact, for functions on , is the theorem of W. Fenchel's five-page note On conjugate convex functions (Canad. J. Math. 1 (1949) 73–77). Its timeline:
Points of are , and .
A standing pair consists of a set and a real function defined in such that
need be neither open, nor closed, nor bounded. The paper writes the lower limit as a "lim" with a bar under it; the milestone texts write it , and it always means .
The conjugate pair of is
The same construction applied to gives the pair , with . An interior point of is a point of the relative interior of , its interior within its affine hull.
In Lean: IsClosedConvexPair G f, conjDomain G f , conjFun G f , and is conjDomain (conjDomain G f) (conjFun G f), conjFun (conjDomain G f) (conjFun G f).
For every standing pair :
with equality for some at every interior point of ;
and every standing pair whose conjugate pair is equals .
The theorem identifies, among convex functions on convex subsets of , exactly the class on which conjugation is a bijection and an involution. It is the finite-dimensional base case of the Fenchel–Moreau theorem and underlies Fenchel's duality theorem for , the conjugate-based optimality conditions of convex programming, and the inversion of gradients of conjugate differentiable convex functions (the paper's §6, the Legendre transformation). The pair form is also how the result is used in practice: the conjugate of a function finite on a set comes with an explicit domain , and the theorem says that domain determines and is determined by .
The result has been proved for 75 years. What a formalization adds is the theorem in Fenchel's own form: a real-valued function on an explicit convex domain rather than an extended-real function on all of , the domain identity together with the identity of values, and the attainment of equality in (5) at relative-interior points. Machine-checked versions of biconjugation exist in other forms: for extended-real functions on Hilbert spaces, for finite convex functions on all of , and for functions on a set with a closed restricted epigraph over continuous linear functionals. None of them states the domain identity or the attained equality, and none is in the paper's pair form.
Milestones 1, 3, 4 and 5 follow from the definition of the conjugate alone. The content sits in three places.
Fin n → ℝ with its product topology, which is the Euclidean one; is Mathlib's x ⬝ᵥ ξ. The paper's in is ξ ⬝ᵥ x, equal by commutativity.(Fin n → ℝ) → ℝ, but every hypothesis and conclusion concerns its values on only: ConvexOn ℝ G f, LowerSemicontinuousOn f G, and Tendsto f (𝓝[G] x) atTop for x ∈ closure G \ G.sSup, which is on unbounded sets; it is evaluated only on .intrinsicInterior ℝ G). The paper's segment definition makes the equality clause false, and the topological interior makes it vacuous for lower-dimensional .Fin n → ℝ and the intrinsic interior), affine minorants of convex functions on lower-dimensional domains, and the boundary-limit argument of milestone 6. All of these are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome.Many problems in convex optimization, variational inequalities and equilibrium modelling reduce to finding a point with , where and are maximal monotone operators on a real Hilbert space : for example, minimizing for closed proper convex is the case , . When the resolvent of is hard to evaluate but the resolvents of and separately are easy, one uses a splitting method. Douglas–Rachford splitting, introduced for monotone operators by Lions and Mercier (1979) after an alternating-direction scheme of Douglas and Rachford (1956) for the heat equation, is the most widely used one; through its dual form it underlies the alternating direction method of multipliers (ADMM) used throughout large-scale optimization and statistics.
Eckstein and Bertsekas (MIT report LIDS-P-1919, 1989; Mathematical Programming 55, 1992) showed that Douglas–Rachford splitting is a special case of the proximal point algorithm applied to a single derived operator, the splitting operator . This identification lets the convergence theory of the proximal point algorithm transfer to splitting, and yields a generalized method with inexact resolvent evaluations and relaxation.
Timeline.
An operator on is a subset , with ; it may be multivalued and partially defined. Its domain is , its image the projection on the second coordinate, its inverse . Scaling and sum are and ; is the identity. is monotone if for all , and maximal monotone if no other monotone operator strictly contains it. The resolvent is , and . An operator is firmly nonexpansive if for all .
For the Douglas–Rachford map is , and the splitting operator is
Its zero set is .
Let , be maximal monotone, , and let , and satisfy
with , and . Then
In the paper's order: Minty's theorem (Theorem 1); properties of firmly nonexpansive operators (Lemma 1); the monotone / firmly nonexpansive correspondence (Theorem 2, Corollaries 2.1–2.3); zeros as fixed points of resolvents (Lemma 2); the generalized proximal point algorithm (Theorem 3): weak convergence to a zero of under summable errors, relaxation in and stepsizes bounded away from , unboundedness when ; (maximal) monotonicity of (Theorem 4) and firm nonexpansiveness of its resolvent (Corollary 4.1); (Theorem 5); and (Theorem 6).
Theorem 7 gives convergence of Douglas–Rachford splitting with both resolvents evaluated inexactly and with over- or under-relaxation, and it characterizes the case without a solution: the iterates are unbounded exactly when has no zero. The relaxed, inexact form is the one implementations actually run, and through Gabay's identification of ADMM with Douglas–Rachford on the dual it is the basis of the paper's Theorem 8, a convergence theorem for a generalized ADMM. Theorem 3, used to prove Theorem 7, is itself a standard reference form of the inexact relaxed proximal point algorithm.
All results here are proved in the paper (one step in the unbounded case of Theorem 3 rests on results of Rockafellar 1969 and 1970 on sums of maximal monotone operators). As of 2026, neither Douglas–Rachford splitting in this generality nor the generalized proximal point algorithm is formalized in Lean or Mathlib. Mathlib has Hilbert spaces, weak topologies and summability, but no theory of maximal monotone operators, Minty's theorem or resolvents. The mission builds that layer and machine-checks the paper's results on it.
The convergence argument cannot be strong: in infinite dimensions the proximal point algorithm need not converge in norm (Güler 1991), so the conclusion is weak convergence, and identifying the weak limit as a zero requires the weak–strong closedness of the graph of a maximal monotone operator. The maximality halves of Theorems 2 and 4 need Minty's theorem, whose proof requires a nontrivial existence argument (all known proofs use Zorn's lemma or an equivalent). The unbounded case of Theorem 3 is a contradiction argument that truncates by the subdifferential of the indicator of a ball and invokes two external facts: maximality of the sum of two maximal monotone operators under an interiority condition (Rockafellar 1970), and existence of zeros for maximal monotone operators with bounded domain (Rockafellar 1969). Neither is available in Lean. The natural first idea for Theorem 7, iterating the firm nonexpansiveness of , gives neither the error tolerance on both resolvents nor the unbounded case without the full machinery of Theorem 3.
[CompleteSpace H]). An operator is a map H → Set H. Monotonicity, maximal monotonicity, , and the function-level resolvent predicate IsResolvent are the published definitions ThreeOpSplitting_Convergence_MonotoneOperators; weak convergence is the published WeakTendsto ( for every ).opResolvent, IsFirmlyNonexpansiveOp, ...), so Theorem 2 and Corollary 2.1 can speak of resolvents that are a priori partial or multivalued. In Theorems 3, 6 and 7 the resolvents are maps with for all , unique by Corollary 2.2.IsResolvent hypothesis would make the iteration unrelated to and ; the hypothesis is always present.Summable with nonnegative terms. Sequences start at ; is unused. Unboundedness is ¬ Bornology.IsBounded (Set.range z).A manufacturer that makes one product to stock faces random demand, can produce at most units per period, and can store at most units. The classical result without the production limit is that a base-stock policy is optimal: raise inventory to a fixed level each period. With a production limit, the natural modification is to produce up to when that is possible and to produce at full capacity otherwise. Federgruen and Zipkin (1986) proved that this modified base-stock (critical-number) policy is optimal under the long-run average-cost criterion, for discrete demand with a general convex cost. Production-capacity models of this type are standard in operations management texts, and the result underlies the computational and comparative-static work that followed, starting with Part II of the same paper, which treats discounted costs.
Timeline.
Time is divided into periods . The demands are independent copies of a random variable with values in and probability mass function ; write and . At the start of period the inventory is an integer (negative values are backorders). The decision maker raises it to
pays the expected one-period cost , and demand is subtracted: . The order cost per unit is set to zero, as in the paper; this loses no generality because every policy with finite average cost has the same average order cost.
The standing assumptions are: is convex and as (Assumption 1); the characteristic function of is analytic at the origin (Assumption 2), and ; for some positive integer (Assumption 3); and (Assumption 4). The smallest global minimizer of is , and .
A Markov policy is a sequence of maps with . The critical-number policy with critical number is . A stationary policy is strongly optimal with average cost if, from every initial state , its average cost converges to , while every Markov policy has lim-inf average cost at least from every initial state.
The analysis uses the operators and , and the optimality equation
For an interval , is the largest expected sum of , over policies forced to produce at capacity below and to produce nothing above , until the inventory first returns to .
There exist , and such that solves (6), is convex with global minimizer , and
The in the optimality claim is the minimizer constructed in part (a).
The result. Theorem 1 reduces an infinite-state average-cost control problem to a one-parameter search over critical numbers. The paper then evaluates the average cost of by a renewal formula, proves it convex in (Theorem 2), and in §5 extends optimality to unlimited storage. The strong form of optimality matters: it compares with every Markov policy from every starting state, and it compares lim-infs, not only lim-sups.
Formalizing it. The theorem has a published proof, but no machine-checked one, and its proof relies on external results that are themselves unformalized: the countable-state average-cost theory of Federgruen, Schweitzer and Tijms, a fixed-point theorem on a compact convex subset of a product space, and a large-deviation estimate quoted from Feller. A formal development produces reusable infrastructure: expected first-passage sums for integer-valued random walks with a reflecting control, polynomial moment bounds for them, and the convexity-preservation argument for capacitated value iteration.
The state space is unbounded below, so the finite-state theory of average-cost Markov decision processes does not apply, and the one-period cost is unbounded. The obvious approach, letting the discount factor tend to one in the discounted problem, needs uniform bounds on relative value functions. Those bounds come from the expected cost until the inventory returns to a fixed interval, and with capacity limits that expectation must be controlled with growth uniformly over a class of policies. This is the content of Lemma 3, whose proof combines a large-deviation estimate for the demand sums with a renewal-type recursion. A second obstacle is strong optimality: comparing with policies whose lim-inf average cost is smaller requires that the relative value function grows sublinearly along every admissible trajectory (Corollary 2).
All objects are in the namespace FedergruenZipkin.AvgCost, defined in one file. States and the capacity are integers; demands are natural numbers with a real probability mass function p; is a positive natural number. Convexity on is the second-difference inequality. Expectations of a real function are series ; expected policy costs and hitting sums are -valued and need no integrability side condition. Feasibility and all properties of value functions are required only on states , which are the only states visited. Assumption 2 is stated literally, as real-analyticity of at . The order cost is zero, as in the paper. is a parameter characterised as the least minimizer of , not an infimum.
"Strongly optimal" has no displayed definition in the paper; it is read from eq. (7) in the proof of Theorem 1(b): convergence of the average cost of to from every state, together with a lim-inf lower bound for every Markov (memoryless, possibly nonstationary) policy from every state. The class is neither widened to history-dependent policies nor narrowed to stationary ones. The goal additionally records that converges, that has growth , and that ; all three follow from the paper's proof.
A trivializing reading is ruled out: the existence of , and is one existential, so cannot be decoupled from the solution of (6), and strong optimality includes the convergence of 's own average cost to , so does not satisfy it vacuously.
Not posed: Lemma 1 (quoted from Feller, and replaceable by a Chernoff bound); the renewal formulas (10)–(11) and Theorem 2; and §5 (unlimited storage). Useful contributions include a formal theory of expected hitting sums for skip-free-upward random walks, and a proof of Lemma 3 by any route.
Many problems in statistics and machine learning minimize an average of losses, one per data point, plus a regularizer: least squares, logistic regression, and their - or -penalized versions. When is large, a full gradient costs component gradients, while stochastic gradient descent, which uses one component per step, needs decreasing step sizes and converges slowly. Incremental gradient methods with variance reduction (SAG, SVRG, SDCA, Finito, MISO) use one component gradient per step but converge at the rate of a full-gradient method.
SAGA (Defazio, Bach and Lacoste-Julien, NIPS 2014, arXiv:1407.0202) is a method of this family. It handles a non-smooth regularizer through its proximal operator, and it comes with a guarantee when the losses are convex but not strongly convex. This mission covers that second guarantee, Theorem 2 of the paper. A companion mission covers the linear rate under strong convexity (Theorem 1, Corollary 1).
Timeline.
Let and . The components are convex and differentiable, and each gradient is -Lipschitz (). Write
The regularizer is convex but possibly non-differentiable. The objective is the composite function , and is any minimizer of . Minimizers need not be unique, and need not vanish.
The proximal operator with parameter is
SAGA keeps an iterate and a table of points , initialized as . At step it draws an index uniformly from , independently of the past, and sets
It then sets and leaves the other table entries unchanged. The averaged iterate is , which excludes .
With step size , for every ,
The expectation is over the indices . The constants are those printed in the paper.
In milestones 3–5, is the expectation over the single index of the next step, given the current state.
The result. Theorem 2 shows that one method, with a step size that depends only on , covers composite problems that are not strongly convex. Examples are -regularized least squares and logistic regression without a ridge term. On these problems the method converges in expected objective value at rate . SAG has no proximal analysis, and SDCA requires strong convexity. With the same step size , the paper also states adaptivity to strong convexity, so no strong convexity constant has to be known in advance. The bound is in terms of , a quantity computable from the starting point.
Formalizing it. The result is proved on paper, but the proof is not self-contained. Its central inequality (milestone 4) is quoted from the prox-SVRG analysis of Xiao and Zhang, with only the remark that their argument uses . A machine-checked proof must therefore reconstruct that argument for SAGA's estimator. To our knowledge, no machine-checked proof of SAGA, SVRG or prox-SVRG exists in Lean or Mathlib. The mission also produces reusable statements about convex functions with Lipschitz gradients (Lemmas 1 and 2) and an explicit finite model of a randomized incremental method.
The naive approach applies the non-expansiveness of the proximal operator to , as in the strongly convex proof. That bounds distances, but it produces no term in . Without strong convexity, the distance terms cannot be traded for function values, so the argument yields no rate.
The function-value term comes from the prox-SVRG inequality (milestone 4), which the paper does not prove. Its difficulty is that depends on the same random index as , so the cross term between them does not vanish in expectation even though . A second difficulty is bookkeeping: uses the old table, the table entry receives and not , and the constants must make three coefficients vanish exactly. A final step converts the bound on into a bound on , which requires Jensen's inequality for the convex .
EuclideanSpace ℝ (Fin d). Components are indexed by Fin n (0-based), with .f' with HasGradientAt (f i) (f' i x) x at every point. Smoothness is the Lipschitz bound .ConvexOn ℝ Set.univ. Lemma 1 uses StrongConvexOn Set.univ μ, whose modulus is the paper's.Two trivializations are excluded. The averaged-iterate bound carries , since at the factor collapses to . The left side is evaluated at the averaged point, not the average of , which is a weaker intermediate step.
A complete development needs the descent lemma and co-coercivity for convex functions with Lipschitz gradients, the characterization and non-expansiveness of the proximal operator, and finite-sum manipulations over index sequences. The lemmas on smooth convex functions and on proximal operators are reusable beyond this mission. Contributions are welcome at every level: proofs of the milestones, a reusable proximal-operator library, and the telescoping argument for the goal.
A Markov decision process (MDP) is solved for one model of its dynamics and rewards, but in practice that model is estimated from data, and a policy that is optimal for the estimate can perform poorly on the true system (Mannor et al., 2007). Robust MDPs address this by evaluating a policy against the worst model in an uncertainty set (Iyengar, 2005; Nilim and El Ghaoui, 2005; Wiesemann, Kuhn and Rustem, 2013). Robust planning, however, solves an inner optimization over at every Bellman update, which is expensive and does not scale to learning settings.
A separate line of work regularizes the policy (entropy, KL, Tsallis penalties) and observes empirically that regularized policies are robust to perturbations (Geist, Scherrer and Pietquin, 2019). Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) make this precise: for uncertainty sets centred at a nominal model, the robust value function is the solution of a regularized problem posed on the nominal model alone, with a regularizer that is the support function of the uncertainty set. This mission formalizes that equivalence: Proposition 3.1, Theorem 3.1 and Theorem 4.1 of the paper.
Let and be finite sets of states and actions, nonempty, and . Fix a discount factor and a strictly positive initial distribution . A transition kernel assigns to every pair a probability distribution on ; a reward is . A policy assigns to every state an action distribution .
For write , , and define the evaluation Bellman operator
The inner product on is , and the support function of a set is .
Given a set of models , the robust Bellman operator is
and the robust value function is its fixed point. Around a nominal model , an s-rectangular uncertainty set is given by sets and , one per state: its models are and , with and chosen independently for each . Finally .
For and every policy , has a unique fixed point , and it is the optimal solution of
Theorem 3.1 is the special case of the goal; it is listed separately because it is the paper's statement that policy regularization is equivalent to reward uncertainty.
The goal says that a robust MDP with s-rectangular uncertainty in both reward and transitions is a regularized MDP on the nominal model, with two regularizers: a policy regularizer coming from reward uncertainty, and a regularizer coming from transition uncertainty that depends on both the policy and the value. For ball-shaped sets these support functions are explicit ( and , Corollary 4.1 of the paper), which leads to the twice regularized (R²) Bellman operators of Section 5 and to robust planning at the cost of non-robust planning. Theorem 3.1 also explains why standard policy regularizers (negative entropy, KL, Tsallis) yield robustness: each is the support function of a reward uncertainty set.
The results are proved in the paper (appendices A.1, A.2, B.1); none has a machine-checked proof. The mission produces formal statements and proofs of the equivalence, the robust Bellman operator's fixed-point theory for stochastic policies and general compact uncertainty sets, and a closed-form robust counterpart that later R² results can import. The paper's printed proof of Proposition 3.1 treats as linear in one step; a formal proof settles the statement independently of that step.
The obvious argument reads Proposition 3.1 as linear-programming duality, as for a single MDP. That fails: is a minimum of affine maps, hence concave and not affine, and the feasible set of is an intersection of infinitely many half-space systems; the argument has to go through monotonicity and contraction of , which in turn requires every model in to be a genuine transition kernel. For the goal, the paper invokes Fenchel–Rockafellar duality to evaluate the inner maximum; the work in Lean is to separate the maximum over the product set into per-state maxima, which needs the s-rectangular structure and attainment of every maximum (compactness), and to track the index order of the perturbation against the kernel .
A nonempty; values are S → ℝ ordered pointwise; a transition array is P : S → A → S → ℝ with P s a s' , and the kernel property is the published IsTransitionKernel; is the published InducedTransition. A policy has π s ∈ stdSimplex ℝ A for every s.S × A → ℝ indexed , as in the paper's ; rewards perturbations are A → ℝ.sInf/sSup. Every theorem assumes the sets nonempty and compact, so these are attained; nothing is quantified over an unbounded set.Contributions welcome: the monotone-contraction fixed-point lemma for and the per-state separation of maxima over rectangular sets are reusable for any robust MDP mission.
Many problems in machine learning and statistics are finite sums: an empirical risk over data points, often plus a regulariser such as an penalty. When is large, a full gradient of costs component gradients, while stochastic gradient descent uses one component per step but converges only sublinearly because its gradient estimate has non-vanishing variance. Incremental gradient methods with variance reduction keep the per-step cost of one component gradient and still converge linearly on strongly convex problems.
SAGA, introduced by Defazio, Bach and Lacoste-Julien at NIPS 2014 (arXiv:1407.0202), is one of the standard methods of this family, alongside SAG, SVRG, SDCA and Finito/MISO. It keeps a table of past component gradients and handles a non-smooth regulariser through its proximal operator.
Timeline. Le Roux, Schmidt and Bach (2012) gave SAG the first linear rate for strongly convex finite sums at the cost of one gradient per step. Shalev-Shwartz and Zhang (2013) proved linear rates for SDCA, a dual method. Johnson and Zhang (2013) introduced SVRG, with periodic full-gradient passes; Xiao and Zhang (2014) extended it to composite objectives (prox-SVRG). SAGA (2014) combines an unbiased SVRG-style estimator with a SAG-style table, and proves a linear rate in the composite strongly convex case with a simple Lyapunov argument.
Let carry the Euclidean inner product. There are differentiable components with gradients . Each is -strongly convex (): for , . Each gradient is -Lipschitz: . Write and . The regulariser is convex, and the goal is to minimise the composite objective ; denotes its minimiser, which is unique.
The proximal operator with step is
SAGA keeps an iterate and points at which the stored gradients were taken. It starts from with . At iteration it draws uniformly from , independently of the past, and sets
then , with every other entry unchanged.
The analysis uses the Lyapunov function
With , for every ,
where the expectation is over the indices drawn in the first iterations. The constants are the paper's.
With as above, and , for every state ,
with the expectation over the next index only.
Lemma 4 (p. 10), a lower bound combining strong convexity and smoothness; Lemma 1 (pp. 6–7), its average over the components; Lemma 2 (p. 7), which bounds the stale-gradient variance by the table part of ; and Lemma 3 (p. 7), a second-moment bound for the SAGA step.
The result. Corollary 1 gives an -accurate iterate in expectation after component-gradient evaluations. This is the complexity of full-gradient descent with the condition number decoupled from , and it holds in the composite setting, so it covers the lasso and elastic-net problems that SAG's analysis does not reach. The paper notes that the rate improves on the published rates of SAG and SVRG and is within a factor 2 of SDCA's. Theorem 1 is the template of later Lyapunov analyses of variance-reduced methods.
Formalizing it. The result has been proved since 2014, and no machine-checked proof is known to this mission. The work left is to formalize the known proof: the convexity inequalities (Lemmas 4, 1, 2), the variance computation (Lemma 3), the one-step contraction (Theorem 1), and the passage from conditional to total expectation along the random index sequence (Corollary 1). The paper's Lemma 3 has a sign misprint, which the formalization corrects; see the scope section.
The obvious argument for SGD-type methods bounds in terms of alone. That fails here: the variance of the SAGA estimator depends on the stale table points , which can be far from even when is close. One needs a potential that also measures the table. Balancing the terms of then requires the four round-bracket coefficients in the paper's display (10) to be non-positive for the specific , and an auxiliary . Checking these coefficients is routine but long algebra in , , . The composite case adds one step: since in general, the argument goes through the fixed-point identity and the non-expansiveness of the proximal operator, neither of which is a numbered result of the paper.
Space and data. The space is EuclideanSpace ℝ (Fin d). Components are indexed by Fin n (0-based), with 0 < n. The gradients are given maps with HasGradientAt (f i) (f' i x) x. Strong convexity is Mathlib's StrongConvexOn Set.univ μ, whose modulus is the paper's.
Regulariser and minimiser. is real-valued and convex; extended-valued regularisers are out of scope, as on the page. A minimiser of is a hypothesis.
Proximal operator. It is any map such that minimises for every (IsProxPoint). The minimiser is unique, so is .
State and expectation. The state is the pair . The run after steps is a deterministic function of the index sequence in Fin k → Fin n. The expectation in Corollary 1 is the average over all sequences, which is exactly the law of independent uniform indices; no measure theory is involved. Theorem 1's conditional expectation is the average over the next index.
Constants and corrections. Constants are as printed and fixed, not "for some constant" and not "for all small enough steps". Lemma 4 carries the hypothesis , which its fractions require. Lemma 3 is stated with , as in its proof and its use in Theorem 1; the printed is false whenever .
Trivializing formalizations, ruled out. Taking the proximal step as merely non-expansive, fixing an index sequence instead of averaging over all of them, measuring against instead of , or restricting Theorem 1 to reachable states changes the theorem and is excluded.
Infrastructure. A complete development needs:
These pieces are reusable well beyond SAGA, by SVRG, SAG and proximal-gradient analyses. Contributions of any of them, or of proofs of the individual milestones, are welcome.
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.
The bullwhip effect is the observation that the variability of orders increases as one moves up a supply chain, from the retailer towards the manufacturer and its suppliers. It was documented in industry and in classroom experiments such as the Beer Game (Sterman 1989), and analysed by Lee, Padmanabhan and Whang (1997), who named demand forecasting, lead times, batch ordering, rationing and price variations as its main causes. A remedy often proposed is to centralize demand information: give every stage of the chain the customer demand data, so that no stage forecasts from the distorted orders of its downstream neighbour.
Chen, Drezner, Ryan and Simchi-Levi (2000) quantified the effect for a retailer that forecasts with a moving average and orders with an order-up-to policy. They gave an explicit lower bound on the ratio of the order variance to the demand variance in terms of the lead time, the forecasting window and the demand autocorrelation. They then showed that in a multistage chain with fully centralized demand information this ratio still grows with the total lead time upstream of each stage. This mission formalizes that result, Theorem 3.1 of the paper, together with the single-stage analysis it rests on.
Time is indexed by the integers. The customer demands seen by the retailer follow the AR(1) model
where , , and the errors are independent and identically distributed from a symmetric distribution with mean and variance . The demand is in steady state, so that and for every .
The retailer does not know the demand process. With a window of past observations it forms the moving-average estimates
where is the lead-time parameter ( means an order placed at the end of period arrives at the start of period ) and is a constant the paper leaves unspecified. The order-up-to point is for a safety factor , and the order placed in period is . It may be negative: excess inventory is returned without cost.
In the multistage chain with centralized information, stages (stage is the retailer) all observe and use the same estimate . Stage has lead time and safety factor and uses the order-up-to point . Following the paper's sequence of events, stage orders , and stage , receiving , orders .
For every stage and every period ,
with equality when . The bound holds for every choice of the constants and of the safety factors.
with equality when .
Theorem 2.2 shows that forecasting with a positive lead time is enough to make orders more variable than demand, even for independent demands (). It also says how the effect depends on each parameter: the bound decreases in the window and increases in the lead time . Theorem 3.1 is the paper's answer to the centralization remedy. When every stage sees the true customer demand and uses the same forecast and the same policy, the variability of orders at stage is still bounded below by the single-stage expression with the cumulative lead time . Centralization reduces the bullwhip effect but does not remove it. The decentralized comparison (Theorem 3.2, where the bound becomes multiplicative across stages) is a separate mission in this series.
On the formalization side, the Gaussian special case of the single-stage results is on the platform. Snyder and Shen's Fundamentals of Supply Chain Theory states Theorem 2.2, Lemma 2.1, Eq. (4) and the AR(1) moments for normally distributed errors, as the items SupplyChainTheory.bullwhip_signal_processing, bullwhip_lemma_13_1, bullwhip_order_identity and ar1_moments. This mission states them under the paper's weaker hypothesis of a symmetric error distribution. The multistage Theorem 3.1 has no machine-checked counterpart. The paper proves only Theorem 2.2 in print. For the proofs of Lemma 2.1 and Theorem 3.1 it refers to Ryan (1997) and to a working paper, so a formalization supplies arguments the published article does not contain.
Most of the algebra is routine. The difficulty is Lemma 2.1 and the covariances like it. The estimate is a square root of a quadratic form in past demands, so its covariance with a demand cannot be computed from second moments. Under Gaussian errors one can appeal to properties of Gaussian vectors. With only a symmetric error law, every distributional fact has to come from the symmetry of the errors and from the representation of the steady-state demand as an infinite series in past errors.
The printed derivation also moves faster than a proof. Expanding from Eq. (4) produces the cross terms and , which lie outside the lags of Lemma 2.1. The display after Eq. (4) does not account for them. A complete proof of milestone 4 must show that these terms vanish too. For the chain, the stage orders are defined by a recursion across stages, and the variance of involves the estimates of all stages .
Random variables are real functions on a probability space , and time is , so that exists for every . Variance and covariance are Mathlib's ProbabilityTheory.variance and ProbabilityTheory.covariance. The demand structure ChenBullwhip.Centralized.AR1Demand records (1) for every outcome and the paper's error hypotheses: independence, identical distribution, symmetry, mean and variance . It adds four disclosed conditions:
The published Gaussian structure SupplyChainTheory.AR1Demand satisfies these conditions, so this mission generalizes the Snyder–Shen items rather than referencing them. The constants are free real parameters, and in the chain is for an arbitrary function . Lead times are natural numbers, included. Sums and run over and , and stages are numbered from . The order recursion is read from the paper's sequence of events, because the paper prints no formula for .
The orders are computed from the demands through the definitions above. They are never arbitrary random variables with assumed moments. "Tight" is formalized as equality, and orders are never truncated at zero. Without the steady-state condition, a process started from an arbitrary satisfies (1) but has time-dependent moments, and the results fail; with the ratio form would be false. Both cases are excluded by the structure, not by vacuous hypotheses. The structure is satisfiable: i.i.d. standard Gaussian demands on form an instance.
A complete development needs: the series representation of a stationary AR(1) process; distributional symmetry facts for i.i.d. sequences with a symmetric law; and covariance bookkeeping for finite linear combinations. The first two are reusable for any linear time-series model with symmetric innovations. Contributions to any milestone, and to general lemmas about stationary AR(1) processes, are welcome.