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?
In a network design game each of players must connect its own terminals in a shared graph, and the cost of every edge that is bought is split among the players who use it. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 2008) studied the fair (Shapley) split, in which the users of an edge each pay . That game is a congestion game in the sense of Rosenthal (Networks 1973), so it has an exact potential function and pure Nash equilibria always exist.
When players carry different amounts of traffic, the natural rule is to split an edge's cost in proportion to weight: a player of weight on an edge whose users have total weight pays . The paper notes that this rule is analogous to weighted generalizations of the Shapley value (Monderer and Samet, Variations of the Shapley Value, Handbook of Game Theory III, 2002). The weighted model leaves Rosenthal's framework: the share depends on which players use an edge, not only on how many, and Chen and Roughgarden (SPAA 2006) showed that weighted games with three or more players need not have a pure Nash equilibrium at all. Section 6 of the paper identifies structural conditions under which equilibria do exist. This mission covers the first of them.
Timeline. Rosenthal (1973): every congestion game has a pure Nash equilibrium, via an exact potential. Monderer and Shapley (GEB 1996): potential and weighted potential games, and the equivalence of exact potential games with congestion games. Anshelevich et al. (FOCS 2004, journal 2008): Theorem 6.1, existence when every resource is shared by at most two players, and Theorem 6.3, existence when all players share a source and a sink. Chen and Roughgarden (2006): weighted network design games with three or more players may have no pure equilibrium.
A weighted cost-sharing game consists of a finite set of players, a finite ground set of edges (resources), and for each player :
together with a fixed edge cost for every . A profile picks for every player. For an edge , is the total weight of the players with , and player 's payment is
A profile is a pure Nash equilibrium when no player has a with , where is the profile in which plays and everyone else keeps their strategy.
The strategy space of player is the set of edges that occur in at least one strategy of . The hypothesis of Theorem 6.1 is that every edge lies in the strategy spaces of at most two players: no edge can ever be shared by three players, whatever they choose.
The network design game is the instance in which is the edge set of a graph and is the set of edge sets of paths connecting player 's source to its sink .
The paper's proof uses an explicit function with when is unused, when alone uses , and when and both use it, where . It is part of the definitions of this mission.
If every edge lies in the strategy spaces of at most two players, there is a weighted potential: a real function on profiles with
and, if every is nonempty, a pure Nash equilibrium exists. The goal asserts the existence of such a rather than fixing the paper's formula, so it remains valid for any other weighted potential.
An extra item states Corollary 6.2: every two-player weighted game with nonempty strategy sets has a pure Nash equilibrium.
The result. Theorem 6.1 is one of the two existence results the paper proves for weighted cost sharing, a game that in general has no pure equilibrium. It shows that the obstruction found by Chen and Roughgarden needs resources shared by three or more players: whenever sharing is limited to pairs, the game is a weighted potential game, so improving moves cannot cycle and equilibria exist. Corollary 6.2 makes the two-player case unconditional, and the paper notes that the same potential gives a (weak) bound on the price of stability.
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. The mission produces a reusable Lean model of weight-proportional cost sharing (shared in form with the companion mission on single-source single-sink weighted games), an explicit weighted potential, and the general step from a weighted potential to a pure equilibrium, which applies to any finite game with positive weights.
The obvious approach, reusing Rosenthal's potential from the unweighted game, fails: the paper observes that in a weighted game improving moves can increase it. A player's share of an edge depends on the weights of the specific co-users, so no function of the edge loads alone can track all players' costs. The identity must therefore hold for every unilateral move, including moves that leave some edges and join others at the same time, and for every pair of possible co-users of an edge. The statement fails without the at-most-two hypothesis, so any argument has to use it in an essential way. The existence step needs the identity on all profiles reachable by feasible deviations, not only along a single path of moves.
Lean namespace PriceOfStability.WeightedPotential. Players form a Fintype ι and edges a Fintype E; a game is a structure with strategies : ι → Finset (Finset E), weight : ι → ℝ and edgeCost : E → ℝ. Standing assumptions wᵢ ≥ 1 and c_e ≥ 0 are the predicate IsStandard. Profiles are functions ι → Finset E with the feasibility predicate IsProfile; every deviation is to a feasible strategy, via Function.update. Nash equilibria are pure and in cost form. The strategy-space hypothesis is a bound on the number of players whose strategy space (the union of their strategies) contains each edge — not a bound on the users in one profile, which would be a different statement. Φ_e is computed from the current users of e; its value with three or more users is a placeholder that never arises under the hypothesis. Strategies are arbitrary subsets of the ground set, as the paper's remark after the proof allows, so the network game is a special case.
The goal is not satisfiable trivially: the function Φ must satisfy the weighted identity for every feasible unilateral deviation from every profile, and an exact (unweighted) potential is not what is asserted. Nonempty strategy sets are added explicitly for the existence part, since without a profile there is no equilibrium.
Needed infrastructure: finite sums over filtered Finsets, the improvement-path argument over the finite set of profiles. The improvement-path lemma (milestone 3) is reusable for any weighted potential game. Contributions of proofs for any milestone are welcome.
Many optimization algorithms are discretizations of a continuous-time descent: the gradient flow for smooth objectives, and its nonsmooth analogue, the subgradient dynamical system, for objectives with kinks or constraints. A basic question about such a flow is whether a bounded trajectory actually converges, rather than merely accumulating on a continuum of critical points, and how fast. For real-analytic this was settled by Łojasiewicz through his gradient inequality, which forces bounded gradient trajectories to have finite length. Without some such structure the answer is negative: there are smooth functions whose bounded gradient trajectories spiral forever around a circle of critical points.
Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the Łojasiewicz inequality to nonsmooth subanalytic functions, possibly taking the value , by replacing with the least norm of a limiting subgradient. Section 4 of the paper turns this inequality into convergence results for subgradient trajectories of convex and lower- functions. This mission formalizes that section. The same "Łojasiewicz argument" later became the Kurdyka–Łojasiewicz framework behind convergence proofs for proximal, alternating and splitting algorithms (Attouch–Bolte 2009; Bolte–Sabach–Teboulle 2014).
Timeline. Łojasiewicz (1963, 1984) proved the gradient inequality for real-analytic functions and finite length of bounded analytic gradient trajectories. Kurdyka (Ann. Inst. Fourier 1998) extended it to functions definable in an o-minimal structure. Kurdyka, Mostowski and Parusiński (2000) proved Thom's gradient conjecture for analytic functions. Bolte, Daniilidis and Lewis (2007) gave the nonsmooth subanalytic version and the trajectory results formalized here.
Let with domain . The Fréchet subdifferential is the set of with . The limiting subdifferential is the set of limits of with and . The nonsmooth slope is , equal to when , and is the set of critical points.
The standing assumptions of Section 4 are:
A trajectory of the subgradient system is an absolutely continuous curve , , with for almost every and for every . It is maximal if it admits no extension to a longer interval. The Łojasiewicz inequality holds around with exponent if is bounded near , with and . A Łojasiewicz exponent at is any such .
Under –, every bounded maximal trajectory is defined on and converges to a critical point . For every Łojasiewicz exponent at there are and such that for
and for , for all large . The constants are existential, so the goal survives any later sharpening of them.
Theorem 4.5 says that for convex or lower- subanalytic objectives, including constrained problems through indicator functions of subanalytic sets, the subgradient flow never oscillates indefinitely: bounded trajectories converge to one critical point. Theorem 4.7 adds rates that depend only on the Łojasiewicz exponent at the limit: exponential at , polynomial above it, finite time below it. These are continuous-time templates for the convergence analyses of proximal and splitting methods under the Kurdyka–Łojasiewicz property.
On the formalization side, the results are proved on paper but, to our knowledge, not formalized in any proof assistant. A development would provide reusable infrastructure: a Lean notion of a trajectory of a differential inclusion on , a chain rule for along absolutely continuous curves, and a comparison lemma for the differential inequality . The analysis of Section 4 uses subanalyticity only through inequality (20), so Theorems 4.5 and 4.7 can be attacked with (20) as an imported milestone, independently of the subanalytic geometry.
Compactness gives cluster points of a bounded trajectory, and the decrease of gives convergence of . Neither gives convergence of . The usual first idea, that forces convergence, fails, since square-integrable speed allows infinite length. The difficulty is to control rather than . That needs a lower bound on the slope in terms of the function gap near the cluster point, which is exactly what (20) supplies, plus a trapping argument showing the tail of the trajectory stays in the ball where (20) holds. In the nonsmooth setting the chain rule itself is nontrivial: is differentiable almost everywhere with derivative for every , which relies on for convex and lower- functions. Global existence on (Corollary 4.1(iii)) must also be established before any asymptotic statement makes sense.
Space is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "bounded from below" by a real number excludes . The limiting subdifferential is the published NonconvexSplitting.Shared.LimitingSubdiff, and convexity is the published MoreauProx.Characterization.EConvex (convex epigraph). The slope is valued in . The Łojasiewicz inequality is encoded as for near and every , which is the bounded ratio under the paper's conventions. Times are real numbers and . Curves are functions whose values outside are irrelevant. "Absolutely continuous on " means absolutely continuous on every compact . Velocities appear only "for almost every ". Lengths are lower Lebesgue integrals in , never Bochner integrals (which would vanish for a non-integrable speed).
Two trivializations are ruled out. Maximality is a hypothesis and is a conclusion: assuming would narrow the theorem, and dropping maximality would make it false. Rates are claimed for every Łojasiewicz exponent at the limit, not for one chosen exponent. Corollary 4.1(iii) is stated as "defined on with ", because the printed would fail for any trajectory with nonzero limit.
Needed infrastructure: absolutely continuous curves and their a.e. derivatives (Mathlib's AbsolutelyContinuousOnInterval), chain rules for convex and lower- functions, existence and uniqueness for monotone differential inclusions (Brézis), and an ODE comparison principle. Contributions to any of these are reusable well beyond this mission.
Scheduling in a multiclass queueing network asks which waiting job a server should work on next when jobs of several types share stations and revisit them along fixed routes. Such networks model semiconductor wafer fabs, job shops and communication switches. Optimal policies are rarely computable: the state space is countably infinite, and even deciding properties of optimal policies is hard (Papadimitriou and Tsitsiklis 1999). A practical substitute is the achievable region approach: describe, by constraints that every policy must satisfy, a set containing all performance vectors any policy can achieve, then optimize a linear cost over that set to get a lower bound on the optimal cost.
Bertsimas, Paschalidis and Tsitsiklis (MIT Sloan working paper 1992; Ann. Appl. Probab. 1994) gave a general method for producing such constraints for open networks, by computing the steady-state drift of quadratic potential functions. This mission formalizes their first-order bounds (Section 4).
Timeline:
A network has single-server stations and job classes. Class is served at station , and is the set of classes served at station . Class- jobs arrive from outside as a Poisson stream of rate , service times are exponential with rate , and after service a class- job becomes a class- job with probability or leaves with probability . The traffic equations
have a unique solution (the network is open), and at every station.
The state counts the jobs of each class. A Markovian policy decides from the current state which classes are in service, at most one per station and only classes with jobs present; idling is allowed. Write for the event that station serves class , and for the event that station is idle. Under such a policy is a continuous-time Markov chain. Assumption A requires that it has a unique invariant distribution and that for all . Let , which equals with the mean response time of class (Little's law), and define
For a set of classes, f-parameters are reals for such that is nonnegative and the same for all ; that common value is , and when (restriction (17)). The sums over include the exit .
For every policy satisfying Assumption A, every and every f-parameters satisfying (17),
where
The formal goal is the product form .
Theorem 4.1 gives, for each choice of and , a linear inequality on mean response times valid for all admissible policies. Minimizing a linear holding cost subject to these inequalities is a linear program whose value bounds the optimal scheduling cost from below; the paper reports numerical values of such bounds in its Section 9. Theorems 4.2–4.4 show that a polynomial-size polyhedron in the variables implies all of these inequalities at once, so the parametric search over is unnecessary.
The results are proved in the paper. As far as is known, none of them has a machine-checked proof. Formalizing them requires a Lean treatment of invariant distributions of controlled countable-state Markov chains with unbounded test functions, which is currently absent from Mathlib, and then the algebra of the drift identities. The definitions here (network data, Markovian sequencing policies, the generator, Assumption A) are the substrate that the paper's later results on routing, closed networks and higher-order bounds would reuse.
Every statement except Theorem 4.4 rests on taking expectations of the generator applied to unbounded functions (, ) under the invariant distribution. The invariance condition is stated only for indicators of single states; extending to quadratic needs an interchange of summations justified by the second-moment condition of Assumption A. The utilization identity additionally needs uniqueness of the traffic solution to identify with . Theorem 4.1 then needs the sign bookkeeping that turns an identity into an inequality: the terms dropped are nonnegative only because on , and at most one class per station is in service.
Classes are Fin R, stations Fin N, states Fin R → ℕ, all rates and probabilities real. A policy is a Bool-valued function of the state with the two admissibility constraints; work conservation is not assumed. Invariance is global balance of the generator on the countable state space; expectations are tsums. The uniformized chain and the epochs of the paper are not built: the paper notes that its expectations at are expectations under the invariant distribution of .
Conventions fixed in Lean:
A quotient-form statement of (18) would be trivially true when , and defining as would make the utilization identity hold by definition; both are excluded.
Welcome contributions: a general lemma extending global balance to test functions of polynomial growth under moment conditions; proofs of the drift identities; the deterministic Theorem 4.4.
The Łojasiewicz inequality states that near a critical point of a real-analytic function there are and with . Łojasiewicz used it in the 1960s to prove that every bounded trajectory of the gradient flow has finite length and converges to a single critical point, a conclusion that fails for general functions. The inequality has since become the standard tool for convergence analysis of descent methods on nonconvex problems.
Optimization problems are, however, rarely smooth: constraints enter through indicator functions, and objectives contain norms, maxima and penalties. Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the inequality to nonsmooth subanalytic functions, replacing by a slope built from the limiting subdifferential. Their Section 3.1 treats functions continuous on a closed domain; Section 3.2, the subject of this mission, treats lower semicontinuous convex functions, which may jump to and whose domain need not be closed. The Kurdyka–Łojasiewicz framework built on this paper (Attouch–Bolte–Svaiter 2013; Bolte–Sabach–Teboulle 2014) underlies the convergence theory of proximal and splitting algorithms used throughout operations research.
Work in with the Euclidean norm, and let with domain .
A set is semianalytic if near every point it is a finite union of finite intersections of sets with real-analytic. It is subanalytic if near every point it is the projection of a bounded semianalytic subset of . A function is subanalytic when its graph is. Semialgebraic functions (norms, polynomials, indicators of polyhedra) are subanalytic.
The Fréchet subdifferential is the set of with , for , and is empty otherwise. The limiting subdifferential is the set of limits of with . The nonsmooth slope is , equal to when , and is the set of critical points. For lower semicontinuous convex , is the subdifferential of convex analysis and is the set of minimizers. Write for the minimum value and for the distance from to . The epigraphical sum is the Moreau envelope of .
Ratios follow the paper's conventions and .
Let be lower semicontinuous, convex and subanalytic with . For every bounded set there is such that
The exponent may depend on ; neither nor the bound is fixed.
Theorem 3.3 gives, for convex subanalytic functions, a Łojasiewicz inequality that is uniform on bounded sets rather than local at one critical point, and it needs neither continuity of on its domain nor a closed domain. Remark 3.4 of the paper exhibits a convex function covered by Theorem 3.3 but not by the continuous-case Theorem 3.1. Through inequality (20) of Section 4, it yields finite length and convergence rates for the subgradient flow of such functions. The intermediate inequality (15) is a Hölderian error bound, , of the kind that drives linear and sublinear rate analyses of first-order methods.
The result is proved in the paper; no machine-checked version of it, or of the nonsmooth Łojasiewicz inequality in any form, is known. Formalizing it would add to the library: subanalytic sets and functions, the limiting subdifferential of convex functions and its agreement with the classical one, the Moreau envelope with its critical points and infimum, and the passage from a growth condition to a Łojasiewicz inequality. Remarks 3.5 and 3.6 isolate parts that need no subanalytic geometry at all.
The convex-analysis steps (inequality (16), properties of the Moreau envelope) are classical. The obstacle is subanalytic geometry. The natural first idea, applying the Łojasiewicz factorization lemma directly to and , fails: is neither continuous nor finite, and its domain need not be subanalytic even when is convex and subanalytic (Example 2.5 of the paper). The milestones route through the Moreau envelope, which is continuous and finite, but subanalyticity is not preserved by infima over unbounded sets, so the subanalyticity of the envelope (Proposition 2.9) needs a localization argument. The subanalyticity of and of rests on the stability theory of subanalytic sets (Gabrielov's complement theorem, the projection theorem for globally subanalytic sets), none of which exists in Mathlib.
The space is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "lower semicontinuous, convex, somewhere finite and never " is the published definition MoreauProx.Characterization.GammaZero, whose convexity is convexity of the epigraph. The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff; the convex subdifferential subgrad appears only in Eq. (5), which proves the agreement and is never assumed. Semianalytic and subanalytic sets are defined from scratch for any finite-dimensional real normed space, so that one definition serves and its products; global subanalyticity is not defined. is written in EReal and converted to a real number only where it is finite. The bounded ratio (14) is encoded as " for every and every ", with real powers (Real.rpow, ). Inequalities (15) and (17) are imposed only where , since Lean sends to under toReal.
Trivializing encodings are ruled out: the goal is stated with the limiting subdifferential rather than an assumed convex subdifferential, the slope is never computed in ℝ≥0∞ where would make the ratio vacuous, and remains existential in with the quantifier order "for every there is ", so that is excluded at critical points in by .
A complete development needs a working theory of subanalytic sets (stability under finite unions, complements, closure, projections of bounded sets, the factorization lemma), the Moreau envelope of a convex function on and its property, and the convex-analytic description of the limiting subdifferential. The subanalytic-geometry layer and the Moreau-envelope facts are reusable well beyond this mission; contributions to either, or proofs of the convex-only milestones (Eq. (5), (16), Remarks 3.5–3.6), are welcome independently.
In the mid-1990s, neural networks trained by gradient descent were observed to generalize well even when the number of weights far exceeded the number of training examples. The classical theory could not explain this: VC-dimension bounds for networks grow with the number of parameters, so for large networks they are vacuous. Bartlett's paper (IEEE Trans. Inform. Theory 44 (1998)) showed that, for classification with a margin, what controls generalization is the size of the weights, not the size of the network. Its two main technical results are a margin bound in terms of the fat-shattering dimension (Theorem 2, the subject of mission I of this series) and a bound on the fat-shattering dimension of networks with bounded weights (Theorem 17, the subject of this mission). The same idea of weight-norm capacity control underlies much of the later theory of margins, boosting and kernel methods.
Timeline. Kearns and Schapire (1994) introduced the fat-shattering dimension. Alon, Ben-David, Cesa-Bianchi and Haussler (1997) bounded ℓ∞ covering numbers by it. Bartlett, Kulkarni and Posner (1997) gave the matching lower bound on ℓ1 covering numbers used here as Lemma 19. Maurey's approximation lemma (reported by Pisier, 1981) was used by Jones (1992) and Barron (1993) for approximation by networks, and by Lee, Bartlett and Williamson (1996) for covering numbers of convex hulls. Bartlett (1998) combined these into Theorem 17.
Let be a set and a class of functions . For , a sequence is -shattered by if there is such that for every some satisfies for all . The fat-shattering dimension is
A cover of a class at scale for a pseudometric on functions is a set of functions such that every has some with ; is the least size of a cover. For a sample the pseudometrics , , are the maximum, the mean, and the root mean square of over , and the uniform covering numbers are .
The hidden units form a nonempty class of functions . For the two-layer network class with ℓ1-bounded output weights is
In Lean these are BartlettNN.Margin.fat, BartlettNN.Margin.coverNum and BartlettNN.Margin.Ninf (shared with mission I), and BartlettNN.FatNet.N1, BartlettNN.FatNet.N2 and BartlettNN.FatNet.combos F A.
There is a universal constant such that for every , , , and with ,
The constant is left unspecified, as in the paper, so that the goal survives any improvement of the numerical constants.
Theorem 17 bounds the capacity of a network class without reference to the number of hidden units . With Theorem 2 (mission I) it gives misclassification bounds for networks with small weights that hold for networks of any size, and by iteration it yields the bounds for deep sigmoid networks of Theorem 28 (mission III). Its method — upper-bound ℓ2 covering numbers through Maurey's lemma and compare with a lower bound in terms of fat-shattering — is a template for bounding the fat-shattering dimension of convex hulls in general.
The results are proved in the paper (Lemmas 19 and 21 by citation). None of them is formalized: the platform has no fat-shattering dimension, no uniform sample covering numbers of function classes, and only a finite-dimensional, diameter-based form of Maurey's lemma (HighDimProb.Appetizer.approx_caratheodory), which is not Lemma 21. This mission produces machine-checked statements of all five ingredients and of the theorem.
The obvious route would bound through a VC-type count of the network's parameters, which fails because is unbounded. The paper's route needs a lower bound on covering numbers by the fat-shattering dimension (Lemma 19, a combinatorial packing argument not proved in the paper), an upper bound by the fat-shattering dimension at a finer scale (Lemma 20, which goes through the Alon et al. scale-sensitive Sauer lemma and a quantization argument), and a probabilistic approximation argument in the empirical space (Lemmas 21 and 22). The final step solves a transcendental inequality (6) for , with care at the boundary where the logarithm is small.
X → ℝ; fat is valued in ℕ∞, so an unbounded shattering is , not a junk . Labels are Bool read through pm (true ↦ 1); sequences are indexed by Fin m (0-based).Metric.coveringNumber (closed balls, metric types) is not used.Contributions welcome: proofs of the five milestones and of the goal, and reusable infrastructure on fat-shattering and covering numbers of function classes.
The conditional logit model is the workhorse of discrete choice analysis in econometrics, transportation planning, marketing and revenue management. An individual facing a finite set of alternatives picks alternative with probability proportional to , where is a vector of observed attributes and an unknown parameter vector. Daniel McFadden's 1974 chapter, Conditional Logit Analysis of Qualitative Choice Behavior, derived this model from a theory of random utility maximization and set out how to estimate by maximum likelihood. McFadden received the 2000 Nobel Memorial Prize in Economic Sciences for his development of theory and methods for analyzing discrete choice.
Every confidence interval and hypothesis test computed from a fitted logit model rests on the large-sample theory in §III of that chapter: the maximum likelihood estimator exists with probability tending to one, converges to the true parameter, and is approximately normal with covariance given by the inverse information matrix. This mission formalizes that theory, Lemmas 5 and 6 of the paper, as proved in its Appendix.
Observations are indexed serially, , as in the paper's Appendix ("Let m be a serial index of trials and repetitions"). Observation offers alternatives, and alternative carries a vector of independent variables. For a parameter the selection probabilities are
The data are generated at a true parameter : the chosen alternatives are independent random variables with . The log-likelihood of the first observations is . The moment matrix of observation is
Axiom 7 asks that and uniformly, and that converge to a positive definite matrix . Axiom 6, for a given sample, asks that no nonzero satisfy for all observed and all . A maximum likelihood estimator is a measurable choice of a maximizer of , wherever one exists.
The result. Lemma 6 is what licenses reading as approximately , so that the diagonal of the inverse information matrix estimates the sampling variances and is asymptotically . Lemma 5 complements it: in finite samples the likelihood can fail to have a maximum (the observations are then "explained" by a direction of Axiom 6), and the lemma shows this failure is asymptotically negligible. The data are not identically distributed (each observation has its own alternatives), so the result is not an instance of the textbook i.i.d. maximum likelihood theorem.
Formalizing it. The results are proved in the paper, in outline. A machine-checked version adds: a complete proof of the existence part (Lemma 5), whose published argument is a sketch by induction over an infinite index set; a precise treatment of the estimator where no maximizer exists; the correction of two misprints in the published proof (the normalization in (58), which must be , and a constant in (51)); and a multivariate Lindeberg–Feller central limit theorem for bounded, independent, non-identically distributed vectors, which the proof invokes and which is reusable well beyond this paper. No machine-checked proof of these results is known.
The obvious route, "the log-likelihood is concave, so its maximizer converges", needs a maximizer to exist, and in a finite sample it may not; the estimator is defined only on an event whose probability must first be shown to tend to one. Consistency then needs a uniform law of large numbers for the gradient on a sphere around , controlled by the third-derivative bound (43). Asymptotic normality needs a central limit theorem for independent but not identically distributed score vectors, with covariances that converge only on average; the i.i.d. central limit theorem does not apply. Finally the random Hessian at an intermediate point must be shown to converge in probability, which ties the consistency result into the normality argument.
EuclideanSpace ℝ (Fin K); is the inner product, and all norms are Euclidean (footnote 11's sum-of-absolute-values norm is equivalent and gives the same qualitative axiom); derivative bounds use operator norms.TendstoInMeasure. Asymptotic normality is TendstoInDistribution to a random vector whose law is stdGaussian. is the positive semidefinite square root CFC.sqrt.The conditional logit model assigns probabilities to choices among alternatives whose observable attributes differ from trial to trial. A fitted parameter vector is usually obtained by maximizing a log-likelihood. For a finite data set, however, maximization need not produce a finite vector: some directions in parameter space can keep improving the likelihood while their length grows without bound. McFadden identifies a condition that rules out these directions and then gives a quadratic program that can test the condition. This mission formalizes that test, Lemma 4 of the published 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior.
The chapter develops a statistical model from observable choice data and addresses the existence of a maximum likelihood estimate in Lemma 3. Lemma 4 turns its existence condition into a finite optimization problem. The diagnostic matters because an optimization routine returning increasingly large parameter estimates is not, by itself, evidence that a finite maximizer exists. The result specifies a mathematical test tied to the observed choice counts and the attributes of the alternatives.
There are trials. Trial offers alternatives, indexed by and . Alternative has an attribute vector , and counts how many times it was selected in that trial. Each trial has at least two alternatives and observations. The vector is the unknown parameter of the underlying conditional logit model. Equation (16) assigns alternative a probability proportional to , with the probabilities normalized over the alternatives in the same trial McFadden, pp. 113–114, equation (16).
For the test, define the weighted difference
It is indexed by every trial and every ordered pair of alternatives, including and alternatives whose observed count is zero. Such terms simply produce zero vectors. Keeping them in the index set makes the formal statement agree with the chapter's quantifiers and its quadratic program.
Axiom 5, called full rank in the chapter, says that the rows obtained by subtracting each trial's probability weighted mean attribute vector from its alternative attributes have rank . Equivalently, the vectors span ; the probability weights in that mean are strictly positive and sum to one. Axiom 6 says that no nonzero direction satisfies for every ordered index triple. These are conditions on the same observed experiment, but they serve different roles: full rank concerns the attribute geometry, while Axiom 6 also uses the choice counts McFadden, p. 116, Axioms 5–6.
Let be the set of feasible vectors
The mission's goal is the equivalence in Lemma 4:
The right side means that the program attains a value of zero. An infimum of zero without an attained feasible point would be a weaker statement and would not express the lemma. The three milestones follow the three assertions in the printed proof: a zero minimum implies Axiom 6; an interior origin in the cone generated by the gives positive coefficients and a zero minimum; and a noninterior origin gives a separating direction that violates Axiom 6 McFadden, p. 117, Lemma 4 and equation (22).
Lemma 3 of the chapter states that Axiom 6 characterizes the existence of a vector maximizing the conditional-logit log-likelihood under the preceding axioms. Lemma 4 gives a finite quadratic-programming criterion for that same condition. It therefore allows the model's existence question to be checked from data before treating a numerical optimizer's output as an estimate McFadden, pp. 116–117, Lemmas 3–4.
The paper proves these results. The work here is to produce machine-checkable statements for the finite-dimensional data, the two axioms, the feasible set, and the equivalence, followed by proofs in the solver stage. The cone and separation milestones can support later formalizations of existence conditions in other finite exponential-family models, provided their hypotheses and signs are checked anew. This mission does not claim a general theorem for all such models.
The tempting diagnostic is to ask whether a numerical solve returns a small objective value. That does not settle the mathematical question: the objective's infimum could approach zero without the feasible set containing a zero vector. The paper's conclusion is about a minimum, so attainment must remain visible in the formal statement. There is also a distinction between positive coefficients in a cone representation and the printed constraints in equation (22). Both conditions must appear in their proper places.
The full-rank condition alone does not ensure that the vectors span the attribute space if a trial has no observed choices. The section describes repetitions of each trial, and the formal data require . This convention is needed for the strict-inequality claim in the first paragraph of Lemma 4's proof. The geometry also has to account for every ordered pair, even when its vector is zero; dropping these indices would alter the program stated in the chapter.
Lean represents a nonempty set of trials by Fin N, alternatives in trial by Fin (J n), counts by natural numbers, and attributes by EuclideanSpace ℝ (Fin K). The count is the sum of observed choice counts. The model requires and for each trial. There is no extra assumption that : the zero-dimensional case is included and the equivalence has its ordinary degenerate meaning there.
Axiom 5 is encoded through the equivalent span of within-trial attribute differences. This removes the parameter dependent logit probabilities from a theorem that only uses rank. Axiom 6 retains exactly the nonpositive sign and every from the page. The feasible set uses coefficients at least one, while the auxiliary generated cone uses nonnegative coefficients. The quadratic objective is the square of the Euclidean norm. IsLeast on its image over the feasible set expresses an attained minimum, so the statement cannot be satisfied by a vacuous or unattained infimum.
The definition bundle and the three proof-step theorems are the mission's direct scope. A complete development needs finite-dimensional inner-product geometry, finite sums, a cone interior argument, and separation. The definitions of weighted differences and the feasible set are reusable for studying nearby existence tests. Contributions that prove the stated milestones or supply faithful finite-dimensional geometry for them are welcome; substitutions that weaken the coefficient constraint or the attainment claim do not establish Lemma 4.
Neural-network classifiers can be made to change their output by perturbations of the input that are imperceptible to a person. A certified defense is a classifier together with a proof that its prediction at a point does not change for any perturbation in a stated set, typically an ball . Randomized smoothing turns an arbitrary base classifier into one with such a certificate by classifying Gaussian-noised copies of the input and returning the most likely class. Cohen, Rosenfeld and Kolter (arXiv:1902.02918v2, ICML 2019) gave the certified radius (their Theorem 1) and showed, in their Theorem 2, that this radius cannot be enlarged when only the two class-probability bounds are known about the base classifier. This mission formalizes Theorem 2. Theorem 1 is the subject of the companion mission of this series.
Earlier certificates for the same smoothed classifier, by Lecuyer et al. (2019) via differential privacy and Li et al. (2018) via Rényi divergence, gave smaller radii. Theorem 2 shows that no further analysis that uses only the class-probability bounds can improve on Theorem 1.
Inputs live in with the Euclidean norm ; classes form a set . A base classifier is a map with Borel decision regions. For a noise level , write for the isotropic Gaussian law of with . The class probability of at is , and the smoothed classifier is
Let be the standard Gaussian CDF and its inverse on . A classifier is consistent with the observed class probabilities (6) for a top class and numbers if
The certified radius is . In Lean these are gaussNoise x σ, classProb f σ x c, IsConsistent f σ x cA pA pB and radius σ pA pB in the namespace Cohen2019.Tight, with Phi and PhiInvReal from the series' shared module Cohen2019.Robust; the half-spaces and of the paper's Appendix A are setA and setB.
Quotations write the paper's underlined lower bound as p̲A and its overlined upper bound as p̄B. The PDF has no printed page numbers; every page cited is the PDF page of arXiv:1902.02918v2.
Assume , , and that some finite set of classes other than satisfies . Then for every with there is a base classifier consistent with (6) and a class with
so that under any tie-breaking. The classifier may depend on .
The class-capacity hypothesis is a correction. As printed, with only , the theorem fails for two classes: with , , and , one has , yet every consistent gives probability at least , and Theorem 1 then certifies radius .
The milestones are the steps the paper itself states, in its order: the Claims and for ; the disjointness of and (corrected to "null" when ); equations (13) and (14) for ,
the equivalence ; and the existence of the worst-case classifier satisfying (6) with equalities.
Theorem 2 makes the guarantee of Theorem 1 exact: when only (6) is known about , the set of perturbations under which the Gaussian-smoothed prediction is provably constant is exactly the open ball of radius . It settles that improvements to Gaussian-smoothing certificates must use more information about the base classifier than the two bounds, as later work on higher-order and Lipschitz-based certificates does.
The paper's proof is complete in its main lines and has two gaps that this mission records and repairs: the printed statement omits a condition on the number of classes, and the claim fails at . To our knowledge neither Theorem 1 nor Theorem 2 has a machine-checked proof. Mathlib at the pinned revision has the multivariate standard Gaussian but no normal quantile function and no Gaussian half-space lemma; this mission adds statements for both kinds of fact.
Each step is elementary on paper but rests on facts about Gaussians that Mathlib does not package: the image of the standard Gaussian on under a linear functional is the one-dimensional Gaussian with variance , and is a continuous strictly increasing bijection with . The construction of has a further step the paper leaves informal: the region between and , of mass , must be shared among "other classes" with none exceeding , which is where the capacity hypothesis enters. Measurability of the constructed decision regions must be carried along.
is EuclideanSpace ℝ (Fin d). is the pushforward of Mathlib's stdGaussian under , with a binder. is cdf (gaussianReal 0 1); is the generalized inverse , which is the true inverse on and the junk value at the endpoints, so every statement that evaluates it assumes ; at or the paper's radius is infinite and Theorem 2 is vacuous. Class probabilities are real numbers. The base classifier in the conclusion is deterministic with Borel decision regions, which is the stronger existence statement. The conclusion is the strict inequality between class probabilities, not merely the failure of to be a strict unique argmax.
A formalization in which the junk endpoint value of makes negative, or in which the classifier's decision regions are non-measurable so that its class probabilities are default values, would make the goal trivial; the hypotheses above exclude both.
Reusable beyond this mission: the Gaussian half-space probabilities and the normal quantile on . Contributions of general Mathlib-style lemmas (the law of for , properties of ) are welcome.
The classical secretary problem asks how to select one valuable candidate when candidates arrive in random order and a decision must be made when each candidate appears. Many allocation settings have several goods of unequal quality instead of a single position. An employer may have roles of different desirability, or a seller may have placements with different visibility. In the weighted secretary problem, an agent's value is multiplied by the weight of the good assigned to that agent. The algorithm must decide irrevocably as agents arrive, while the benchmark sees every value before assigning goods. Babaioff, Dinitz, Gupta, Immorlica and Talwar study this model with arbitrary fixed agent values and a uniformly random arrival order, and give a constant competitive ratio independent of the number of agents and goods (authors' version, §§2–3).
The paper also studies time discounts and matroid constraints. This mission concerns its weighted-goods result, Theorem 3.4. The result combines an online allocation rule for several comparably valuable agents with the familiar one-choice secretary rule for an unusually valuable agent. These are distinct ways in which the sorted offline assignment can earn value; both are present even when the weights are fixed in advance. The weighted model matters because matching a valuable agent to an unsuitable good can lose value despite accepting the right agent.
There are agents , each with a nonnegative value , and goods indexed in decreasing order of nonnegative weight:
An assignment gives each good to at most one agent, and each agent receives at most one good. A good may remain unassigned, represented by with . Its value is . Agent values are arbitrary, not drawn independently from a distribution. The uncertainty is the arrival order , chosen uniformly from all permutations; an agent's value becomes visible on arrival, and an allocation decision cannot be revised.
The offline optimum, , assigns the heaviest good to the highest-valued agent, the next good to the next agent, and so on. If , the extra goods remain unassigned. A consistent tie break makes the ordering unique without changing the numerical value. This sorted assignment is defined directly; the mission does not replace it with an unconstrained variable said to be optimal.
The reservation algorithm draws a sample size , observes the first agents without allocation, and retains the best sampled agents. Positive values are grouped into value classes for integer . A sampled agent in class reserves one good in that class's contiguous block, with higher classes receiving heavier blocks. A later agent receives the heaviest unassigned good reserved for its class when one is available. The classical secretary rule instead observes the first agents, then selects the first later arrival better than every predecessor; its winner receives good .
The mission's goal is the exact guarantee of Theorem 3.4 for Algorithm , which runs the reservation algorithm with probability and the classical rule with probability :
Here the expectation covers the uniform arrival permutation, the independent binomial sample size used by the reservation branch, and the mixing coin. The multiplicative inequality expresses competitiveness even when an expected payoff is zero. It uses the explicit constant in the paper's proof rather than an instance-dependent or unspecified constant.
Four source results form the milestones. The classical secretary rule selects the maximum with probability at least . Lemma 3.2 compares the starting indices and of class- blocks in the reservation and optimum assignments. Lemma 3.1 says that if the optimum assigns at least two agents from class , the reservation rule assigns at least agents from that class in expectation. Lemma 3.3 converts this to expected value at least . The target retains the paper's class condition and both numerical fractions (authors' version, pp. 4–5).
Theorem 3.4 supplies a constant factor guarantee for irrevocable allocation when goods have different weights and agents arrive in random order. The factor does not grow with or . It separates the effects of uncertain arrivals from the offline matching of high values to high weights, and it supplies a benchmark for later variants with more complicated feasibility constraints. The paper extends the reservation idea to additional combinatorial settings, including partition-matroid variants in Appendix C (authors' version, Appendix C).
The theorem is proved in the source paper, while the Lean statements in this mission are proof obligations. Formalizing them requires checking that the random-order model, sample distribution, tie convention and assignments jointly express the same algorithm. A complete development will also establish reusable finite-average facts for random permutations and binomial samples, and structural facts about sorted assignments and reserved blocks. Those pieces can support other secretary problems in the series; the mission's specific promise remains the weighted algorithm's exact bound.
A count of how many agents a class receives does not by itself control the weighted value of those goods. Goods have unequal weights, and the value of assigning the next good changes with its position in a block. A class whose offline optimum receives several agents can also lose all its sampled members from the allocation phase. Thus a direct comparison of expected class counts with expected class values is insufficient. The paper's separate count, block-position and value statements identify the claims a solver must establish; the final theorem must also account for classes represented only once in the offline assignment (authors' version, p. 5).
Agents and goods are Fin n and Fin K; their indices start at zero in Lean, so paper time corresponds to Lean index . An arrival permutation maps time to agent. Values and weights are real and explicitly nonnegative, and weights are antitone in the good index. The finite sums defining expectations are normalized by for permutations and by for sample sizes. No measurability or integration convention is needed. For the goal, makes the heaviest good available; is allowed.
Equal values are ordered by smaller original agent index throughout the sorted optimum, the sample's top agents and the classical rule. The classical rule observes exactly arrivals, and zero-valued agents reserve no value-class goods. Positive values below one use negative integer class indices. The paper says only that class holds the values “between” and (p. 4, and again in Appendix C, p. 12); the mission fixes the half-open interval , so that the classes partition the positive reals (authors' version, pp. 4, 12). A reservation assignment is built from each post-sample agent's rank within its class, so a good is offered to at most one such agent. The theorem is about this concrete algorithm and the concrete sorted offline assignment; an arbitrary favorable policy or an optimum supplied as a hypothesis would not express the source result.
The development needs a finite assignment interface, a tie-aware rank order, value classes, the two online rules, and normalized finite expectations. The assignment and finite-average definitions are reusable. Contributions that prove the structural validity of the reservation assignment, the classical success guarantee, Lemmas 3.1–3.3, or the final combination all advance the stated target.
A martingale difference sequence is the standard model of a "fair" sequence of observations whose terms may depend on the past: each new term has conditional mean zero given everything observed before it. Laws of large numbers for such sequences underlie the analysis of stochastic approximation, sequential estimation and online learning, where the noise terms are dependent but conditionally centred.
Classical strong laws concern averages in which every observation keeps the same weight as the sample grows. Kazuoki Azuma's 1967 paper Weighted sums of certain dependent random variables (Tôhoku Math. J. 19) studies weighted sums of dependent variables, and is best known for the exponential moment bound that is now called the Azuma inequality (its display (2.4) together with Remark 1). Its Theorem 3 uses that bound to prove a strong law for weighted averages in which the weights are applied in reverse order, so that the oldest observation always receives the newest, largest weight.
Timeline:
Let be a probability space and an increasing family of sub--fields of . A sequence of real random variables is a sequence of martingale differences if, for every , is -measurable and integrable and almost surely. Theorem 3 assumes moreover almost surely for every .
Let be positive increasing weights: and . Put
The sums are the reversed weighted sums. In passing from to every existing term changes its weight, so is in general not a martingale. In the Lean development, is A a n, is Sbar a x n ω, and the martingale-difference property is IsMartingaleDiff μ ℱ x.
If is a sequence of martingale differences with a.s., is positive and nondecreasing, and
then
The milestones follow the paper's proof, in attack order.
The result. Theorem 3 shows that reversed weighting does not destroy the strong law, under a growth condition on the weights that is strictly weaker than the condition of the paper's Theorem 2: the paper reproduces an example of T. Tsuchikura satisfying (4.9) but not that condition. The condition allows rapidly growing weights, provided no single weight carries more than an share of the total. Milestone 2 is the one-sided Azuma inequality in the paper's conditional-expectation form, a tool used throughout probability, combinatorics and learning theory. Milestone 4 is a maximal inequality for a process that is not a martingale, where Doob's inequality cannot be used.
Formalizing it. The theorem is proved in the paper; this mission produces a machine-checked proof. Mathlib contains sub-Gaussian moment-generating-function bounds for martingale differences in a kernel formulation (HasCondSubgaussianMGF, which assumes a standard Borel space), and the Prove2Me platform has two-sided Azuma–Hoeffding inequalities under the same assumption. Neither states Remark 1 or the one-sided tail bound in the paper's conditional-expectation form on an arbitrary probability space, and no strong law for reversed weighted sums is formalized.
The obvious route to a strong law for a martingale, Doob's maximal inequality applied along a geometric subsequence, fails at the first step: is not a martingale, because each new step reweights all earlier terms. The maximum of over a block of indices therefore needs a separate maximal inequality, and it is there that the monotonicity of the weights is indispensable. A second difficulty is quantitative: the exponential tail bound must be summable over blocks whose growth is controlled only through (4.9), which is weaker than the variance-type condition of Theorem 2, so the block sizes and the constants , and have to be chosen to fit together.
Conventions committed to in Lean:
Finset.Icc 1 n, and , are never used. Every hypothesis on and is quantified over .Filtration ℕ. Its first -field plays the role of and is arbitrary rather than trivial; the paper's is a special case, so the formal statements are at least as general.IsLittleO along atTop). is not a hypothesis, since it follows from positivity and monotonicity.limsup is used anywhere.μ.real); conditional expectations are Mathlib's μ[f | ℱ n].A formalization of the goal that replaces by the direct sums , drops the monotonicity of the weights, or strengthens (4.9) to or to states a different theorem and does not count.
A complete development needs the Azuma moment bound in conditional-expectation form, conditional Chebyshev arguments on events, the Borel–Cantelli lemma (in Mathlib) and elementary real analysis of the blocks. The one-sided Azuma inequality and the maximal inequality (4.15) are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the goal.
A finite Markov decision problem with discounting is solved by Howard's policy improvement routine: start from a stationary policy, switch to actions that do better against its value, repeat. When the discount factor tends to the total discounted income typically diverges, and the natural targets become the long-run average income and, among policies with the best average, the policy that does best in the transient phase. Howard treated this undiscounted case directly (Howard, 1960). David Blackwell's 1962 paper (Blackwell, 1962) treats as a limit of : it expands the discounted return of a stationary policy in powers of and reads off which policies remain good as . The two leading coefficients of that expansion, the gain and the bias , became the standard objects of average-reward and sensitive-discount optimality (Veinott, 1969; Puterman, 1994, Ch. 8–10).
Timeline. Howard (1960) gives policy iteration for discounted and average-income problems. Blackwell (1962) proves that some stationary policy is optimal for all near (his Theorem 5, the subject of a companion mission) and, in Theorem 4, characterizes the nearly optimal stationary policies through and . Miller and Veinott (1969) and Veinott (1969) extend the expansion to all orders (-discount optimality).
There are finitely many states and a finite nonempty set of actions. Action in state pays an income and moves the system to with probability . is the finite set of decision rules . A policy is a sequence of decision rules; uses every day, and uses first and then . For , is the vector and the Markov matrix . The discounted return of is the vector
and abbreviates . Vectors are compared coordinatewise; means and . A policy is β-optimal if its return dominates that of every policy, and is the return of a β-optimal policy. It is optimal if it is β-optimal for all sufficiently near , and nearly optimal if as .
For any Markov matrix , the limit matrix is the limit of , and the deviation matrix is . For a rule , and are those of , and
With , the set consists of the actions with , or with and ; consists of those with equality in both.
For any with for all :
Milestones: Lemma 1(b) (), Theorem 4(b) (improvement for β near 1), 4(c) (a sufficient condition for optimality), Lemma 2, and 4(d) (a sufficient condition for near optimality).
The mission also states, as intermediate results:
Theorem 4(e) says that near optimality for β near 1 is exactly lexicographic maximization: first of the average income , then of the bias . It justifies the two-level optimality equations used throughout average-reward dynamic programming and shows that, once the β = 1 improvement routine stops, the remaining problem is a bias maximization over the gain-optimal rules. Theorem 4(a) is the first two terms of the Laurent expansion of discounted values, the starting point of sensitive-discount optimality.
The results are classical and proved in the paper (Lemma 1 with a reference to Kemeny and Snell); no machine-checked proof of them is known on the platform. A complete development produces a multichain theory of Cesàro limit and deviation matrices of arbitrary finite Markov matrices, which Mathlib does not have, and the expansion of discounted returns near β = 1.
Lemma 1 must be proved for every Markov matrix, including reducible and periodic ones, where does not converge and the stationary distribution is not unique; arguments through the Perron–Frobenius eigenvector of an irreducible chain do not apply. In Theorem 4(e) the hard part is the existence of a single whose bias dominates every gain-optimal rule in every coordinate at once; a rule maximizing each coordinate separately is not enough. The final characterization compares a stationary policy with all policies, including time-dependent ones, through .
States and actions are finite nonempty types; incomes are real of any sign; a policy is a sequence ℕ → (St → Act) with π 0 the paper's . is a real tsum. is limUnder of the Cesàro means, and its existence is Lemma 1(a), not an assumption; is a matrix tsum, whose summability for is part of Lemma 1(d); uses Mathlib's total inverse, whose nonsingularity is also part of Lemma 1(d). and are defined by the closed forms and from the paper's proof, and Theorem 4(a) asserts that they are the unique solutions of the paper's defining systems. Limits "as β → 1" are along . "Nearly optimal" is encoded without : for every , for all β in some interval , every policy's return is at most in every coordinate; this is equivalent to because a β-optimal policy exists. "Optimal" (§4) and "β-optimal" (§3) are distinct definitions, and Theorem 3's β-dependent improvement set is distinct from the §4 set .
A formalization in which optimality or near optimality is tested only against stationary policies, or in which is assumed to exist or the chain to be irreducible, proves a different and easier theorem and does not meet the targets.
Contributions are welcome at every level: the Cesàro and Abel limit theory of finite Markov matrices (reusable well beyond this paper), the policy improvement theorem for fixed β, and the comparison arguments of Theorem 4. Theorem 3 and the Corollary are also drafted in the companion mission on Theorem 5 in another namespace.
Set cover is one of the basic covering problems of combinatorial optimization: given a ground set and a family of subsets with costs, choose a cheapest subfamily whose union contains every element. In many applications the elements to be covered are not known in advance but appear over time: requests for a service that must be served by opening facilities, clients that must be assigned to servers, or constraints of a covering program that are revealed one at a time. Each arriving element must be covered at once, and decisions cannot be undone. This is the online set cover problem, introduced by Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; conference version STOC 2003).
The quality of an online algorithm is measured by its competitive ratio: the worst case, over all arrival sequences, of the ratio between the algorithm's cost and the cost of an optimal offline cover of the elements that actually arrived. The paper gives a deterministic algorithm with ratio , where is the number of elements and the number of sets, and shows a nearly matching lower bound for deterministic algorithms. Its algorithm for the weighted case, analysed with a potential function, became a template for the online primal–dual method surveyed by Buchbinder and Naor (Found. Trends Theor. Comput. Sci. 3(2–3), 2009).
This mission formalizes the core of the weighted result: the algorithm that is given a value at least the optimal cost, and its guarantee (Theorem 3.4).
The ground set has elements and the family has sets; every set has a cost . Both are known to the algorithm in advance. For an element , denotes the sets containing . Elements of an unknown subset of arrive one at a time in a sequence ; on arrival each must be covered by a chosen set. The chosen family can only grow. is any family covering every arriving element, and .
The algorithm is given . It discards sets costing more than , buys sets costing at most outright, and rescales costs; on the resulting normalized instance and for every set (p. 365).
The algorithm keeps a weight for every set, initially ; the weight of an element is . With the set of covered elements and the indicator of , the potential is
with natural logarithms throughout. When arrives with nothing happens; otherwise the algorithm performs weight augmentation steps while . In a step, for each : (a) ; (b) if , add to when does not exceed its value before (a); (c) if has increased, return FAIL.
In Lean, the instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance over finite types X (elements) and T (sets), with the published elementWeight, coveredBy and potential. The run is OnlineSetCover.Weighted.Reachable inst α σ, the set of configurations reachable from initState σ under the transition relation Step.
On the normalized instance, with covering , , and , every reachable configuration is a running state (never FAIL) in which (i) every with is covered, and (ii)
The Proved platform theorem OnlinePrimalDual.OnlineSetCover.algorithm_correctness (the last paragraph of the proof of Theorem 3.4, with the invariant assumed) is included as a supporting reference.
Theorem 3.4 is the analysis of the subroutine; with the doubling over guesses of described on pp. 364–365 (which loses a factor of at most 4) it yields the paper's deterministic -competitive algorithm for weighted online set cover. The lower bound of Section 4 shows that no deterministic algorithm can do much better on general instances, so the result is close to the deterministic optimum. The technique, a potential that couples a fractional multiplicative-weights solution to a deterministic rounding, reappears in online covering and packing, online facility location and related problems.
The result is proved in the paper and restated in the Buchbinder–Naor monograph. On Prove2Me, the monograph's final step (from the invariant to the cost bound) is a Proved theorem, and its expectation form of the monotonicity lemma is Disproved because it omits the hypothesis . Neither the full statement about the algorithm's run nor Lemmas 3.1, 3.2 and the corrected Lemma 3.3 are formalized on the platform. This mission produces them, with the terms replaced by explicit expressions.
The cost bound in the last step is short once two facts about the run are available: that stays below , and that the fractional cost stays logarithmic. Neither is a local fact about one state. The first requires showing that, at every per-set step, one of the two deterministic choices (add or not) does not increase ; the paper proves this by a probabilistic argument over an auxiliary randomized choice, and the bound on the exponential term depends on the cost of the set being at most . The platform's earlier statement of this lemma, which omits that hypothesis, is Disproved. The second requires a bound on the number of augmentation steps over the whole run, which depends on the run's history and not on any single state. In Lean both are inductions over an operational semantics with real-valued exponentials and powers , where the initial bound is a genuine size condition on and .
The run is a small-step transition relation. A state records the weights, the cover, the number of augmentation steps begun, the elements not yet given, and the position inside the current step; FAIL is a separate terminal configuration. The order in which a step visits is arbitrary and may differ between steps; every statement holds for every order. "Throughout the algorithm" means every reachable configuration, including those between per-set substeps. Arrival sequences are arbitrary lists (repetitions allowed) of elements covered by .
Conventions: costs, weights and are real; and are the cardinalities of the finite types cast to ; is Real.log; and are real powers. The paper's asymptotic expressions are replaced by what its proofs establish:
The goal is a statement about the configurations the algorithm actually reaches from and the empty cover. Taking the invariant or the fractional-cost bound as a hypothesis on an arbitrary state would trivialize it, and is ruled out: those are exactly what the milestones establish. The doubling wrapper for unknown is not part of this mission.
A complete development needs an invariant for reachable states (positive weights, steps of an element processed in full), the per-set potential inequality, and the step-counting argument. The per-set inequality is reusable for the monograph's version of the algorithm. Contributions of proofs of any milestone, and of auxiliary invariants as separate lemmas, are welcome.
In the online set cover problem of Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 2009; preliminary version STOC 2003), a ground set and a family of subsets are known in advance, but the elements that actually need covering arrive one at a time, and each must be covered on arrival by sets chosen irrevocably. The paper's motivating example is a network of servers with activation costs: the set of potential clients is known, the clients that actually request service are not, and each request must be served on arrival.
The paper gives a deterministic online algorithm whose cost is within a factor of the offline optimum, where is the number of elements and the number of sets. Its Section 4 shows that this is close to optimal for deterministic algorithms: for all interesting values of and , every deterministic online algorithm has competitive ratio . The lower bound is the reason the product, rather than the of offline approximation (Feige 1998), is the right target online. The online primal–dual framework that grew out of this paper (Buchbinder and Naor 2009) cites it as the benchmark for online covering problems.
This mission formalizes the exact, non-asymptotic statements behind that lower bound: Propositions 4.1 and 4.2 of the paper.
A ground set and a family of distinct subsets of are fixed and known to the algorithm; . An adversary presents elements of one by one, choosing each after seeing the algorithm's previous responses. A deterministic online algorithm , on the arrival of , sees the earlier arrivals and , and adds a finite family of sets to its collection; sets are never removed. It is valid if after every arrival that lies in some member of , that element lies in a chosen set. After an arrival sequence the chosen collection is , and since every set has unit cost, the cost is . The offline optimum is the least number of members of covering the elements of . The competitive ratio of is at least when some arrival sequence has and .
Two families are used.
and the family consists of all ; it has members.
For all positive integers and all with
there is a family of exactly distinct subsets of an -element set such that for every valid deterministic online algorithm there is a nonempty arrival sequence , covered by a single member of , with
The goal leaves the instance existential, as the paper does, and keeps both bounds on and the bound on exactly as printed.
A supporting item (not a milestone) records the count of the block family.
The result. Proposition 4.2 is the exact statement behind the paper's lower bound: choosing of order and of order turns it into the asymptotic bound , which shows that the paper's algorithm is optimal among deterministic algorithms up to a factor. Without it, the gap between the achievable offline and the achieved online would be unexplained. Proposition 4.1 alone gives the matching bound when .
Formalizing it. Both propositions are proved in the paper; neither is formalized anywhere to our knowledge. The mission produces a reusable model of deterministic online algorithms against an adaptive adversary, with a validity notion and a cost, and machine-checked adversary arguments on it. The paper's proof tacitly lets the algorithm add one set per arrival; the statements here cover algorithms that add any number of sets per arrival, so a complete formalization also closes that gap.
The adversary must be adaptive, and the quantifiers are ordered instance, then algorithm, then arrival sequence. The obvious single-block argument (Proposition 4.1) forces only sets. To force sets with , the adversary must move to blocks that no chosen set has touched yet, which requires counting the blocks touched by the sets chosen so far. When an algorithm adds many sets at once, the paper's count "at most blocks after steps" no longer applies as written, and the stopping rule has to be phrased in terms of the cost already paid. The padding of Proposition 4.2 must reach exactly elements and exactly distinct sets without creating sets that help cover the adversary's elements.
The ground set is a Fin type: Fin (2^k) for Proposition 4.1, Fin (k r²) × Fin (2^k) (block, element) for the block family, Fin n for Proposition 4.2. A family is a Finset (Finset X), so its cardinality counts distinct sets. Bit (1-based) of is Nat.testBit j (i-1). An online algorithm is a function from (earlier arrivals in arrival order, current element) to the finite family of sets it adds; it may add any number of sets. Validity demands coverage only for elements that some member of the family contains. Costs are unit (the problem of Section 4 is unweighted).
The offline optimum is never encoded as an infimum: lower bounds exhibit a nonempty arrival sequence and a single covering set (), and the upper bound of Proposition 4.1 quantifies over all offline covers. This rules out the trivializing reading in which the empty arrival sequence satisfies as .
The statements contain no : every quantity is the paper's exact one. The asymptotic bound (8) under the range (7), whose final paragraph only sketches the choice of and , is excluded, as are the remarks on the trivial ratio- and algorithms.
Contributions welcome: proofs of the milestones; lemmas on the chosen collection (monotonicity, decomposition along a sequence); the count of the block family; and the padding construction of Proposition 4.2. The online-algorithm model is reusable for other deterministic online covering lower bounds.
Set cover asks for the fewest sets from a family of subsets of a ground set of elements whose union contains . It is NP-hard, and the best ratio achievable in polynomial time is (Feige 1998, doi:10.1145/285055.285059).
Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; preliminary version STOC 2003) introduced an online version. The instance is known in advance, but an adversary reveals elements one at a time, and each revealed element must be covered at once, by sets that can never be removed later. The set of elements that will actually be revealed is unknown. The paper's motivating example is a network of servers: the potential clients and the servers that can serve each client are known, but which clients will request service is not, and every activated server costs money.
The question is how much an algorithm loses against an offline adversary who knows and covers it with a family . This mission formalizes the paper's answer for unit costs (Section 2): a deterministic algorithm whose cover is within a factor of . Section 3 of the paper extends the algorithm to weighted sets and Section 4 proves a nearly matching lower bound; those are separate missions of this series.
An instance consists of a finite ground set with elements and a finite family of sets. For an element , is the collection of sets containing . Every set has cost , so the cost of a family is its number of members.
The adversary gives a sequence of elements (the given elements form ). A family covers if each element of lies in some member of it.
The algorithm keeps a weight for every set, initially , and a cover , initially empty. The weight of an element is , and is the set of elements covered by members of . The potential is
When the adversary gives an element :
Step (c) prescribes a property of the chosen sets, not the sets themselves. A run on is any sequence of iterations, one per arrival, in which every iteration makes an admissible choice.
For , every arrival sequence , and every family covering : a run of the algorithm on exists, and every run ends with a cover that covers every element of and satisfies
The paper states ; the displayed bound is the constant its proof produces. Because the bound holds for every covering family, it holds in particular for an optimal one.
Lemma 2.1. In every run, the number of iterations with a weight augmentation is at most
Lemma 2.2. In an iteration with a weight augmentation, from a state with positive weights, there is a family with such that
where is the potential before the iteration and the potential after it, computed with the augmented weights and the cover .
The theorem shows that online set cover over a known instance admits a deterministic -competitive algorithm. Section 4 of the paper shows this is nearly optimal: no deterministic algorithm achieves over a wide range of parameters. Its multiplicative weight updates were developed further into the online primal–dual framework for covering problems of Buchbinder and Naor (FnT TCS 3(2–3), 2009), whose Section 5.1 restates this algorithm.
The result is proved in the paper; it is not machine-checked. The Prove2Me platform has the weighted version's final counting step from the Buchbinder–Naor monograph, but no statement of Section 2. A complete development here gives a checked proof of the unweighted competitive ratio with an explicit constant, together with a reusable formal model of an online algorithm with a nondeterministic step, whose correctness includes the existence of an admissible choice at every step.
The central step is Lemma 2.2: a family of at most sets that keeps the potential from increasing must exist at every augmentation. The obvious rules fail. Adding every set of can exceed the cardinality bound, since may contain up to sets. Adding nothing, or a single set, can increase : every uncovered element sharing a set with has its weight raised, and its term grows by a factor up to . The paper's argument is non-constructive, and a formal proof must establish existence for a finite averaging statement over real powers of .
The second difficulty is that the algorithm is nondeterministic. A statement "every run has property P" is empty if no run exists, and the existence of a run is exactly Lemma 2.2 applied at every step under the invariants that weights stay positive and that each arriving element lies in some set. Feasibility (that every given element ends up covered) is not part of the algorithm's rule; it follows from the potential never increasing, which needs and a careful treatment of the initial potential, which is at most and equals when every element lies in every set.
The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (finite types E of elements and T of set indices, incidence elemSets), with the published elementWeight () and coveredBy (). Its positive cost field is not used: all sets have unit cost and the cover is measured by its cardinality. and . Weights are real numbers; is the real power.
The algorithm is the definition OnlineSetCover.Unweighted.Algorithm: a relation Step for one iteration (recording whether a weight augmentation occurred) and Run for a sequence of iterations from the initial state, counting augmentations. Arrival sequences are lists and may repeat elements.
Explicit forms of the paper's asymptotic and unspecified quantities:
The goal adds the hypothesis , which the paper's assumes tacitly: for no set may be added and the element is never covered.
Replacing the algorithm by the set of states whose potential is at most the initial one, or dropping the existence of a run from the goal, gives a weaker theorem; part (a) of the goal rules this out.
A complete development needs elementary real analysis (Real.rpow, Real.log, ), a finite probabilistic or averaging argument for Lemma 2.2, and induction over runs. Contributions are welcome on any milestone; a derandomized averaging lemma for Lemma 2.2 would be reusable in the weighted mission of this series.
The conditional logit model is the workhorse of discrete choice analysis: it is used to forecast travel mode shares, to estimate demand for differentiated products, and, in operations research, as the multinomial logit (MNL) choice model behind assortment optimization and revenue management. Its selection probabilities have the form . Daniel McFadden's 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior gave the model two behavioural foundations, one of which is the subject of this mission: the logit form is a consequence of a single axiom on how choice probabilities change when the set of available alternatives changes.
That axiom is Luce's choice axiom, which McFadden calls Independence of Irrelevant Alternatives (IIA): the relative odds of choosing one alternative over another do not depend on which other alternatives are present. Luce (1959) introduced it; McFadden (1974, §I) showed how, together with positivity and a mild condition on which alternative sets can occur, it yields the conditional logit form with a "utility indicator" shared by all alternative sets.
Timeline. Luce, Individual Choice Behavior (1959): the choice axiom and its ratio-scale representation. McFadden (1974, pp. 109–110): the derivation in the econometric setting with measured attributes , the binary-odds identities (5)–(10), and footnote 3, which removes an extra axiom (Axiom 3) by a universal benchmark alternative. McFadden (1974, pp. 111–112): the companion random-utility characterization by extreme-value shocks, treated in mission 2 of this series.
Let be the universe of objects of choice and the universe of vectors of measured attributes of decision-makers. An alternative set is a finite set ; a designated family of finite sets is the family of possible alternative sets. The selection probability is the probability that an individual drawn at random from the population, with attributes and facing , chooses . For every and possible , is a probability vector on . Whenever belong to a possible set, the pair is possible too, so binary choices are defined.
In Lean these are IsSelectionProb, PairsPossible, Axiom1, Axiom2, binProb, altSetV and IsUniversalBenchmark in the namespace McFadden1974.IIA.
Under Axioms 1 and 2 and a universal benchmark , with , for every , every possible (containing or not) and every :
The function is the same for all alternative sets; this is what distinguishes the goal from Equation (10).
The result. The goal identifies a testable axiom on choice probabilities, IIA, with a parametric functional form, the conditional logit model. It is what licenses the econometric specification estimated in the rest of McFadden's chapter, and it is the reason the MNL model is the default in assortment and pricing problems in operations research. It also makes the model's limitations precise: any population whose choices violate IIA (the auto/red-bus/blue-bus example on p. 113 of the chapter) cannot be logit.
Formalizing it. The result is classical and proved on paper. No machine-checked statement of it exists on the platform, which has the logit form only as a definition (soft-max, MNL revenue) and IIA only in Arrow's social-choice sense, a different axiom about preference aggregation. This mission produces a formal statement of the derivation with every standing assumption explicit, including two the paper leaves implicit: that selection probabilities are normalized on binary sets, and that binary subsets of possible sets are possible.
The algebra is elementary; the difficulty is bookkeeping of where each axiom may be applied. Axioms 1 and 2 are assumed only on possible alternative sets. Equation (10) needs the benchmark to lie in the alternative set, and the naive argument "pick as benchmark" produces a function that depends on the set through the choice of . The goal requires a single for all sets, including sets that do not contain , where neither Equation (10) nor the axioms on alone say anything about . A second subtlety is the diagonal: , so is set to by definition rather than read off a singleton choice.
Alternatives form a type X with decidable equality, alternative sets are Finset X, possible sets are a Set (Finset X), and selection probabilities are a real-valued function P : S → Finset X → X → ℝ. Only values P s B x with x ∈ B and B possible are constrained; no statement depends on the others. binProb sets the diagonal to 1/2. altSetV uses Real.log, which is 0 on non-positive arguments; under Axiom 2 on the binary sets its argument is always positive where it is used.
The probability-vector hypothesis on every possible set, binary sets included, is part of every statement: without it the zero function satisfies Axiom 1 vacuously and Equations (7)–(8) fail. The goal is stated with the explicit , never as "for each there is a ", which would only restate (10).
Nothing beyond Mathlib's finite sums, Real.exp and Real.log is needed. Proofs of the milestones and of the goal are welcome, as is a formal statement of the auto/bus example or of the converse (logit selection probabilities satisfy Axioms 1 and 2).
A set function on a finite ground set is submodular if it has diminishing returns, equivalently if for all . Cut functions of graphs and hypergraphs, coverage functions, entropy, and many facility-location and welfare objectives are submodular. Unconstrained Submodular Maximization (USM) asks, given a nonnegative submodular through a value oracle, for a set of maximum value. It contains Max-Cut, Max-DiCut and Max Facility Location as special cases, and it is a subroutine in algorithms for constrained submodular maximization.
Timeline:
Let be a finite ground set and a nonnegative submodular function. Write , and let denote a set attaining it.
Algorithm 1 (DeterministicUSM) fixes an arbitrary order of and maintains two solutions, starting from and . In iteration it computes
If it sets , ; otherwise , . A tie adds . After iterations , which is the output.
The analysis uses the hybrid sets , which agree with and on and with on . In Lean, the run is state f l i, the state after the first entries of the order l, and is optI O (state f l i).
For every nonnegative submodular and every order of ,
The result. Algorithm 1 is the deterministic member of the double greedy family. It makes one pass over the ground set with four value queries per element, and it guarantees of the optimum for every order, without the polynomial-but-large running time and the loss of local search. Its analysis, which charges the decrease of to the increases of and , is the template the paper then refines into the randomized -approximation (Theorem I.2) and its continuous counterpart on the multilinear extension. Theorem II.3 shows that is the exact ratio of this algorithm, so the improvement to requires randomization (or a different deterministic rule) rather than a sharper analysis.
Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal statement of the algorithm as printed, a checked proof of its guarantee for every order, and a checked tight instance. The definitions of the run and of are the same objects the randomized and fractional analyses reason about, so a complete development here is the first step toward the paper's main theorem.
The individual inequalities are short; the difficulty lies in the bookkeeping. Each step needs the invariants and , which follow from the order being an enumeration (no repetitions, every element present), and the identification of from in each branch of the algorithm. Summing Lemma II.2 needs a telescoping over the run defined as a fold. The naive idea of comparing with directly, without the hybrid sets, gives no bound: the greedy choices are made against and , not against . For Theorem II.3 the difficulty is producing an explicit instance, checking that it is submodular and nonnegative, and tracing the run, including the ties, which the algorithm resolves by adding.
X with decidable equality; subsets are Finset X; is real valued, Finset X → ℝ, and nonnegativity is the hypothesis ∀ S, 0 ≤ f S where the page uses it (the goal, the telescoped display and the tight example). Lemma II.1, Lemma II.2 and the hybrid-sequence milestone do not assume it.NonmonotoneSubmod.Shared.Submodular. The paper's main-text sentence ("for every and ") would force monotonicity when and is read as the footnote. is the published NonmonotoneSubmod.Shared.OPT f, the maximum of over all subsets.l with l.Nodup and ∀ x, x ∈ l; is l[i - 1]. Every statement quantifies over all such lists. No nonemptiness of is assumed: for an empty ground set the goal reads .O with ∀ S, f S ≤ f O.List.foldl over List.take, on membership in the states of the run, and on telescoping sums over . A reusable lemma "the run keeps and decides exactly " would serve all three missions of this paper. Contributions of proofs of any milestone, of the goal from the milestones, and of the tight instance (e.g. the paper's five-vertex directed cut function) are welcome.Weighted sums of dependent random variables occur when the weights change with the observation horizon. Even if each random variable is bounded and centered, allowing the weights in row to be chosen anew makes an almost-sure statement about all large different from a bound on a single finite sum. Kazuo Azuma's 1967 paper treats this situation under a finite-product moment condition called class [M]. Its first main theorem bounds every row of an arbitrary real triangular array at the scale given by that row's Euclidean norm and .
The condition is useful because it allows dependence. The paper notes that bounded martingale differences provide examples, but Theorem 1 is stated directly for class [M], without introducing a filtration in the result. The conclusion therefore records the property of the random variables actually used by this part of the paper, rather than restricting the mission to one familiar source of examples. Azuma, §1 and Theorem 1.
Fix a probability space . Let be real measurable random variables. They form a bounded multiplicative system with unit bounds if almost surely for every , and
The indices in are distinct. Taking a singleton shows ; taking sets of two, three, or more indices imposes the full condition used in the paper. Pairwise zero correlations by themselves do not state class [M]. All bounds and moment conditions are for the positive indices, so is outside the mathematical sequence. Azuma, p. 357, property [M].
For each , choose real coefficients . There is no relation required between different rows. Define the weighted sum and its weight norm by
Both definitions use the source's 1-based indices. A row of zero weights has and almost surely; such rows remain within the theorem. Azuma, p. 359, §3.
The goal is Theorem 1, display (3.1): for every bounded multiplicative system and every real triangular array,
The normalizing constant is exactly , and the upper bound is exactly . The mission does not assume that grows, converges, or stays positive. In Lean, the target is stated as the equivalent operational bound: for each , almost every outcome eventually satisfies . This includes zero-weight rows without assigning a meaning to a real quotient .
The milestone list follows results displayed in the paper: the corrected convexity inequality (2.2), Lemma 1's exponential moment estimate (2.1), the exponential estimate in the proof of Theorem 1 with its factor , and the almost-sure finite exponential series on the next page. Lemma 1 gives, for arbitrary real and ,
The paper prints (2.2) with a missing factor in its linear term. The mission records the printed text as provenance and states the corrected inequality in Lean; the printed version fails already when and . Azuma, pp. 357–360.
Theorem 1 turns an exponential moment bound for each finite weighted sum into a single almost-sure assertion along an entire triangular array. It gives a scale that adapts to the actual coefficients in each row: two arrays with different row norms receive different bounds, while no regularity across rows is required. The result is also the starting point for the weighted strong-law corollaries that follow it in the paper. Azuma, Theorem 1 and Corollary 1.
The mathematical theorem has been proved since 1967. This mission's remaining work is a machine-checked Lean proof of the exact theorem and its listed intermediate statements. A complete development would add reusable formal statements for bounded multiplicative systems and for their finite exponential moments. Those objects could support later work on dependent sums without importing a filtration or a stronger independence assumption. The proposal statements compile as open goals; compilation alone does not supply proofs.
The usual first step for independent bounded variables is to factor the exponential moment into one-variable expectations. Class [M] does not assume independence, so that factorization is unavailable. The condition controls every product with distinct indices, while allowing other dependence. The almost-sure conclusion must also hold when the coefficients change arbitrarily with : bounds that depend on one fixed row do not by themselves settle what happens for all sufficiently large rows. Finally, rows with require a statement that preserves the theorem rather than excluding them by an added positivity hypothesis.
The Lean development represents the probability law by a measure with IsProbabilityMeasure μ, and a random sequence by . It uses measurable variables and states the unit bound almost surely at every positive index. The class [M] predicate quantifies over every nonempty finite set of positive indices; no conditional expectations, filtration, symmetry, or independence hypotheses enter Theorem 1. Finite products and finite weighted sums use ordinary real multiplication and Finset.Icc 1 n. The triangular weights have type , and only entries with contribute.
The norm is the nonnegative real square root of the sum of squared weights. Real.log is zero at and in Lean, but the target is eventually quantified, so its asymptotic content concerns large . The exponential estimate is stated for . If , Lean's total division returns zero in the exponent's quotient; all weights in that row are zero, making this extension valid. In the almost-sure series, the term at index zero is set to zero. The source's limsup is represented by eventual inequalities for every positive excess, avoiding a real-valued limsup default on unbounded sequences.
The definition of class [M] includes every finite product, including singletons; replacing it by pairwise orthogonality would change the theorem. Measurability and the almost-sure unit bounds ensure that the finite products and the exponential functions in Lemma 1 are integrable, so their Lean integrals represent expectations. Contributions toward proofs of the corrected convexity bound, the moment estimate, the exponential series, and the final almost-sure step are all within scope. The finite-product predicate and the exponential estimate are reusable beyond this mission.
A learning algorithm generalizes when its error on fresh data is close to its error on the training sample. Bousquet and Elisseeff (JMLR 2, 2002) showed that a single property of the algorithm, uniform stability, controls this gap with exponential concentration: if removing any one example from a training set of size changes the loss of the output at every point by at most , the generalization error exceeds the empirical error by roughly with probability (their Theorem 12). The bound is useful only when , and the second half of the paper identifies algorithms with that rate: Tikhonov regularization in a reproducing kernel Hilbert space (Theorem 22), and relative-entropy regularization of mixtures (Theorem 24), the subject of this mission.
Mixtures arise whenever a learner outputs a distribution over a parametric base class instead of a single hypothesis: Bayesian posterior averaging, Gibbs and randomized classifiers, exponential weights. Regularizing by the relative entropy to a prior is the maximum-a-posteriori reading of these procedures, and Theorem 24 is one of the earliest results showing that such posteriors are uniformly stable with rate . The same mechanism (entropic regularization, stability through Pinsker's inequality) reappears in PAC-Bayesian analysis and in the stability of exponential-weights methods.
Let be a measurable space with a reference measure , and write for integration against . A base class is indexed by , and is the loss of the base hypothesis at an example .
The algorithm outputs a density with respect to : a measurable, nonnegative, integrable with . denotes the set of all densities. A density is scored by the averaged loss
the expected loss of a randomized predictor that draws from . The relative entropy of to is
with when is not absolutely continuous with respect to or the integrand is not integrable.
Fix a prior , a parameter , and a training set . The algorithm returns a minimizer over of
For an index , the truncated objective is , and denotes one of its minimizers over .
For every minimizer of (29), every minimizer of the truncated objective, and every example ,
Theorem 24 places entropy-regularized posteriors among the algorithms to which the paper's exponential generalization bound applies: combined with Theorem 12 it gives, for the averaged loss, a deviation of order . The proof also yields the bound , which by itself gives classification stability for base hypotheses with values in (remark after Theorem 24, p. 518).
The result is proved in the paper; no machine-checked proof is known to exist. A formalization produces reusable pieces that Mathlib does not have: Pinsker's inequality for densities in form (Mathlib has the Kullback–Leibler divergence InformationTheory.klDiv, but not Pinsker), the Bregman identity for the relative entropy, and a stability statement for minimizers over a space of probability densities.
The paper derives Theorem 24 from Lemma 21, which is stated for a regularizer that is defined and differentiable on a vector space. The relative entropy is defined only on the convex set of densities and is not differentiable at densities that vanish on a set of positive measure, so the general lemma does not literally apply, and the identity needs integrability conditions that the page does not state. A complete proof of the goal must either justify that application on the set of densities, or work directly with the minimizers, which requires identifying them and handling the values of . Pinsker's inequality itself requires a separate argument at the level of general measures.
IsDensity ν g: measurable, nonnegative, integrable, total mass one, with respect to a σ-finite reference measure ν. The integral is always against ν, never Lebesgue measure.r : Θ → Z → ℝ, measurable in θ, with 0 ≤ r ≤ M; the paper's costs are nonnegative (p. 502).InformationTheory.klDiv of the measures g · ν and g' · ν, in ℝ≥0∞. The objectives (29) and its truncation take values in ℝ≥0∞. A formalization that converts to a real number with toReal would send to and make the worst densities minimizers; that reading is excluded.f minimizes (29) and f' minimizes the truncated objective over all densities, for the given S : Fin m → Z and i : Fin m.Contributions welcome: proofs of Pinsker's inequality for klDiv (reusable far beyond this mission), of the Bregman identity, of Lemma 21, and of the goal by any route.
An agent can learn to act in an unknown environment by repeatedly running a finite episode, observing the states reached after its actions, and updating its model of the environment. The agent must trade off rewards in the current episode against information that may improve later decisions. A regret bound measures the cumulative value lost relative to an optimal policy that knows the true transition probabilities. Its dependence on the number of states, actions, episode steps, and interactions says how much exploration that uncertainty can force.
Azar, Osband, and Munos study this question for a finite-horizon Markov decision process with known, bounded rewards and an unknown, stationary transition kernel. Their UCBVI algorithm estimates action values from observed transitions and adds an exploration bonus. Their second version, UCBVI-BF, uses the empirical variance of the next-state value in that bonus. Their Theorem 2 gives an explicit high-probability regret bound whose leading dependence on the horizon is smaller than the bound they give for the simpler UCBVI-CH bonus. The paper states that, in a sufficiently long-run regime, its leading order matches the cited lower-bound scale up to logarithmic factors. This mission targets the explicit theorem, including its lower-order terms, rather than only that asymptotic comparison.
Let and be nonempty finite state and action sets with cardinalities and . A stationary transition kernel is a probability distribution on next states for every current state and action . The reward is deterministic, known to the learner, and lies in . These are the conditions of Assumption 1 and §2. Episodes have steps; episodes comprise interactions.
A policy chooses an action for each state and step. Its value is the expected reward from step through the final step when the state at is ; the terminal value is . The optimal value ranges over all deterministic policies of this form. At the start of episode , the environment may choose the initial state using the completed episodes. The learner then fixes a policy , observes transitions during the episode, and updates counts for the next episode. Its regret is
For each state-action pair, counts transitions to in episodes before , and . When the latter is positive, . The count records previous episodes whose state at step was . Algorithms 2 and 4 compute optimistic backward from zero terminal value, take a minimum with the previous episode's estimate and with , and choose a maximizing action at every state. Previously unseen pairs receive . The Bernstein–Freedman bonus uses the empirical variance of under and an additional term based on ; the algorithm uses .
The goal is Theorem 2 on p. 5. For any MDP and interaction described above and every , write . The target is the exact bad-event form of the printed high-probability bound:
The milestone list contains three empirical-transition deviations from the proof of Lemma 1: Eq. (9) for a value-weighted transition error, the displayed count bound before Eq. (11), and Eq. (12) for the full transition row's error. It also contains Lemma 2's variance comparison and Eq. (26), which relates cumulative conditional next-value variance to the variance of an episode return. These are source-indexed targets, with their printed constants retained.
The theorem gives a quantitative guarantee for a particular executable decision rule: its regret grows sublinearly in in the leading term, with explicit dependence on , , and . The result lets one compare the horizon dependence of a variance-sensitive bonus with a value-agnostic bonus under the same finite-horizon model. It also fixes which logarithm belongs in the algorithm and which appears in the reported bound; replacing either changes the claim.
A formal proof would connect a fully specified adaptive interaction to its finite probability law, empirical counts, backward value iteration, and the stated high-probability conclusion. The local prior-art search found reusable transition-kernel vocabulary and general concentration tools, but no published formal statement of this exact UCBVI-BF algorithm or theorem. The mission's finite path and variance definitions can also support other episodic reinforcement-learning bounds that use conditional variance.
The bonus is computed using a value function that itself depends on earlier observations and the same episode's backward recursion. A concentration inequality for a fixed transition row and a fixed test function therefore does not directly control every value estimate encountered by the algorithm. The number of samples in a row is also random and changes with the learner's past actions. The regret compares a policy's value at an environment-chosen initial state with a supremum over all policies, while the learner's greedy action must be defined at states it never visits. These dependencies are the central obstacle to turning local concentration statements into the episode-level bound.
The Lean model uses finite sums rather than measure theory. A published predicate supplies the stationary, real-valued transition kernel; a local MDP adds the known deterministic reward. State and action types are finite and nonempty. Policies are deterministic and depend on the step. The supremum defining ranges over their finite function type. A theorem quantifies over every maximizing tie-breaking rule and every initial-state rule that reads only completed episodes. The probability of an event is constructed as a sum over finite outcome sequences, each weighted by the product of true transition probabilities. Counts use all past transitions and no current or future outcomes. These choices rule out a trivialization that assumes the desired law or optimizes over an unbounded class of arbitrary functions.
Lean indexes the steps from zero, while the paper indexes them from one. The last observed next state is kept because Algorithm 4 counts states at the terminal index . At , Algorithm 4's quotient is interpreted as infinite and the capped term is ; Lean's ordinary division by zero would incorrectly produce zero. The algorithm uses , while Theorem 2's bound uses . For Eq. (26), the appendix ends its sums at under a shifted terminal convention; the local statement includes all reward steps and the terminal value used by Algorithm 2. The milestone text remains the printed text. The count milestone is the display before Eq. (11), since Eq. (11) drops a factor of under the square root present in that display.
Theorem 2 retains its printed term. The appendix's displayed Lemma 13 calculation does not reproduce that second-order constant when propagated to Lemma 14; this is a source proof gap, not a hypothesis of the theorem. Work on the probability normalization, random-count concentration, adaptive value estimates, variance identity, and a valid route to the printed explicit constants is welcome. A proof with altered constants or an asymptotic-only conclusion would be a different target.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It uses the same density estimate as the companion entry, for with (explicit Selberg sieve, weighted first moment, eighth moment of the singular-series factor, Hölder). It then replaces Schnirelmann's sumset inequality by Mann's theorem, for sets containing :
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It keeps the explicit Selberg sieve and Schnirelmann's original sumset inequality from the entry, and improves only the density estimate:
Only Chebyshev-type prime bounds, the Selberg upper-bound sieve, Hölder's inequality and Schnirelmann's inequality are used.
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It keeps the explicit Selberg sieve and Schnirelmann's original sumset inequality from the entry, and improves the density estimate:
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Optimization problems with orthonormality constraints arise throughout numerical linear algebra and its applications: computing a few eigenvectors or singular vectors, Procrustes problems in statistics and shape analysis, orthogonal factor rotation, independent component analysis, and the orthogonality constraints of electronic-structure calculations. The feasible set of such a problem is the Stiefel manifold of orthonormal -frames in . Riemannian optimization algorithms on this manifold (Riemannian gradient, Newton and trust-region methods; see Absil, Mahony and Sepulchre, Optimization Algorithms on Matrix Manifolds, 2008) take a step in a tangent direction and then need a retraction: a map that brings the updated point back onto the manifold while agreeing with the geometry to first order.
The most natural way to come back to a constraint set is to take the nearest point. P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds (SIAM J. Optim. 22(1), 2012; the mission follows the authors' version, HAL hal-00651608v2), show in their Proposition 3.2 that the metric projection onto a smooth submanifold yields a retraction, and then work out the projection explicitly for several matrix manifolds. For the Stiefel manifold, their Proposition 3.4 identifies the projection with a factor of the singular value decomposition, equivalently with the orthonormal factor of the polar decomposition. The paper notes that this result was mentioned without proof in Higham's survey of matrix nearness problems, and gives a proof along the lines of Horn and Johnson, Matrix Analysis, §7.4.
Section 4.5 of the same paper treats a second, "orthographic" retraction on the Stiefel manifold, which corrects a tangent step by a normal vector instead of projecting; for the orthogonal group (the case ) it admits a closed form through a matrix square root (Proposition 4.12).
Fix natural numbers . Matrices are real, and carries the Frobenius norm
The Stiefel manifold is
the set of matrices with orthonormal columns; is the orthogonal group .
The singular values of are , the square roots of the eigenvalues of . A singular value decomposition of is a factorization with , , and zero off its diagonal, with nonnegative nonincreasing diagonal entries. For every singular value equals ; in particular .
A projection of onto is a point with for all . A polar decomposition of is a factorization with and symmetric positive definite.
Let and let satisfy . For every singular value decomposition ,
and is the of the polar decomposition : it is the orthonormal factor of every polar decomposition of , and a polar decomposition with this factor exists.
The statement asserts existence, uniqueness and the closed form of the projection on the whole open ball of radius , for whichever singular value decomposition is supplied.
for , skew-symmetric and symmetric with ; and Proposition 4.12,
stated as: is the unique symmetric correction of smallest Frobenius norm.
Proposition 3.4 makes the projective retraction on the Stiefel manifold computable from one singular value decomposition of an matrix, and identifies it with the polar factor, which is also what many numerical codes already compute for re-orthonormalization. Combined with Proposition 3.2 of the paper, it yields a second-order-accurate retraction usable in any Riemannian algorithm on . The same statement is the orthogonal Procrustes problem in the special case of a full-rank target: the nearest orthonormal frame to .
The result is classical and proved; the paper's argument is short but cites two external facts (Weyl's perturbation bound for singular values and the uniqueness of the polar decomposition). To our knowledge no machine-checked proof of the nearest-orthonormal-frame property, of the uniqueness of the polar factor, or of the closed form of Proposition 4.12 exists in Mathlib or on this platform. A formalization produces reusable pieces: the trace inequality over the Stiefel manifold, the uniqueness of the polar decomposition, and the full-rank property near , all of which recur in matrix analysis and in the analysis of Riemannian algorithms.
Existence of a nearest point is easy (the Stiefel manifold is compact), and attainment of the trace bound is a direct computation. The content is in two places. First, the bound for every requires transporting by the orthogonal factors of the singular value decomposition and bounding diagonal entries of a matrix with orthonormal columns. Second, uniqueness does not follow from the trace argument: when is rank deficient there are many maximizers. Uniqueness needs both a perturbation bound (singular values are 1-Lipschitz in the Frobenius norm, so near ) and the uniqueness of the polar factor, which in turn rests on the uniqueness of the positive-semidefinite square root of . Mathlib has singular values of linear maps and the spectral theorem but, at the pinned revision, neither Weyl's inequality for singular values nor the polar decomposition.
For Proposition 4.12, the printed proof compares only two solutions of (4.14), while (4.14) has other symmetric solutions (mixed signs of the square roots, or non-diagonal ones on repeated eigenvalues); minimality must be proved against all of them.
Matrices are Matrix (Fin n) (Fin m) ℝ with the Frobenius norm brought in by open scoped Matrix.Norms.Frobenius. The Stiefel manifold is the set stiefel n m of matrices with Xᵀ * X = 1. Singular values are Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin X, re-indexed to be 1-based as on the page (sv X m is ). A singular value decomposition is the predicate IsSVD X U S V of display (3.5), and is U * E * Vᵀ with E the rectangular identity (frameOfSVD U V). The projection is the set of nearest points, using the published predicate RandomGradFree.Nonsmooth.IsMetricProjection; "exists and is unique" is equality of that set with a singleton. Positive definiteness is Mathlib's Matrix.PosDef, which over includes symmetry.
Standing assumptions and added hypotheses: is the page's assumption of §3.3; is added so that is meaningful. The radius is with strict inequality, kept in that form although its value is . Two misprints of the page are corrected in the Lean and kept in the verbatim milestone texts: the display of Proposition 3.4 reads for , and the distance identity reads for . The uniqueness of the polar factor is stated for positive semidefinite factors under the rank hypothesis, which contains the positive definite case of Proposition 3.4. The matrix square root of §4.5 is defined through Mathlib's spectral theorem; Proposition 4.12 is stated for every admissible symmetric correction, and is vacuous only when no symmetric correction exists.
A trivializing formalization is ruled out: the projection is not taken as a hypothesis or chosen by definition; the goal asserts that the nearest-point set equals the singleton of the explicit matrix, for every singular value decomposition supplied, so neither existence nor uniqueness can be assumed away.
Contributions welcome beyond the stated items: Weyl's inequality in Mathlib's singular-value API, existence of a singular value decomposition in the matrix form (3.5), and the polar decomposition with its uniqueness, all reusable well beyond this mission.
Blackwell approachability is the vector-payoff analogue of von Neumann's minimax theorem. In a repeated game where each round's outcome is a vector , a player wants the running average of these vectors to converge to a target set , whatever the opponent does. Blackwell (1956) showed when this is possible, and approachability has since become a standard tool for calibrated forecasting, regret minimization with respect to general benchmarks, and learning in games.
Online linear optimization (OLO) is the problem of choosing points in a fixed decision set against a sequence of linear losses , with performance measured by regret against the best fixed point in hindsight. Algorithms with regret — "no-regret" algorithms such as online gradient descent (Zinkevich, 2003) — are among the most studied objects of machine learning.
Abernethy, Bartlett and Hazan (COLT 2011) showed that the two problems are algorithmically equivalent: each can be converted into the other with explicit control of the rates. This mission covers the direction from OLO to approachability.
Timeline:
A Blackwell instance consists of compact convex sets , , a payoff that is affine in each argument (biaffine), and a closed convex target set . Write for the Euclidean distance to a set, and for the closed Euclidean ball of radius .
A halfspace oracle takes a halfspace and returns a point ; it is valid if for every halfspace , for all .
A set is a cone if for all , . For , , and the polar cone of is .
An OLO algorithm maps past loss vectors to a point , and its regret is
Algorithm 2 runs on when is a cone: at round it sets , plays , observes , and feeds back to .
When is compact but not a cone, it is lifted: with and the concatenation, put and , and run Algorithm 2 on .
For a Blackwell instance with nonempty and compact, any valid halfspace oracle for the lifted instance, any OLO algorithm with values in , any and any , the run of Algorithm 2 on the lifted instance satisfies
The bound holds for every and every adversary, with no rate assumed for ; a no-regret then gives approachability.
The result. Corollary 18 turns any no-regret algorithm into an approachability strategy for a compact convex target, provided a valid halfspace oracle is available, with rate . Combined with online gradient descent it gives an approachability rate, and through the choice of OLO algorithm it lets approachability inherit the computational efficiency of online learning. The paper uses this route to build an efficient calibrated forecaster (Section 5). Together with the converse reduction (Theorem 16), it shows that the two problems are equivalent.
Formalizing it. The results are proved in the paper; none of them has been machine-checked. Formalizing them requires the conic duality formula for distances (Lemma 13), a quantitative lifting lemma (Lemma 14) and the bookkeeping of an interactive protocol. The proof of Lemma 14 on the page is a sketch: it refers to an undefined point and uses a triangle-similarity argument, so a complete proof is new work.
The reduction's core is Lemma 13: the distance to a cone is a maximum of a linear function over the polar cone's unit ball. Lemma 13 needs projection onto a cone in Euclidean space; for a non-closed cone the projection may not exist, and the argument must go through the closure. The lifting Lemma 14 is a geometric statement whose page proof relies on a picture and an undefined point, so the factor 2 has no complete written argument. Finally, connecting the average lifted payoff to the lift of the average payoff, and the halfspace guarantee to the regret, requires keeping the round indexing and the oracle's validity domain exactly aligned.
All spaces are EuclideanSpace ℝ (Fin d). The concatenation lives in EuclideanSpace ℝ (Fin (d+1)) with coordinate 0 equal to , so ; a product type with the sup norm would change every distance and is ruled out. Distances are Metric.infDist. The polar cone uses the paper's sign (), the negative of Mathlib's innerDual. A halfspace is the pair ; a valid oracle must answer every halfspace containing , including , not only the halfspaces the algorithm happens to query. The OLO algorithm is a map from histories Fin t → ℝᴰ with values in at every history. Rounds are , and the run of Algorithm 2 is given as hypotheses on sequences , which exist and are unique by recursion. The minimum in the regret and are written as sInf/sSup of images over nonempty compact sets, where they are attained.
Hypotheses added relative to the page: and in the goal; in Lemma 13 (the empty set is a cone under Definition 11 and the identity fails for it); in Lemma 14. Corrected misprints, each disclosed in the item's note: "" in Corollary 18 and (9) denotes the regret of the OLO algorithm on the lifted losses; Lemma 14's "" has a stray ; is the maximal norm of the set, not its diameter. The oracle in the goal is a valid oracle for the lifted instance, which is what applying Algorithm 2 to requires.
A formalization in which the oracle is valid only at the run's own queries, the OLO algorithm is unconstrained, the regret's minimum ranges over all of , or the middle term of the goal is dropped, is a different statement and is ruled out.
The development needs: the dual formula for the distance to a convex cone, nearest-point projection onto closed convex sets (in Mathlib), compactness of polar-cone slices, and finite sums of biaffine payoffs. The cone layer (Lemma 13) is reusable for the converse direction of the paper and for conic duality generally. Proofs of any milestone, and of the bridge from an oracle for the original instance to one for the lifted instance, are welcome.
Reinforcement learning methods estimate the value function of a policy : the expected discounted sum of future rewards from each state. When the state space is large, cannot be stored as a table and is approximated by a parametrized function. The most studied case is linear function approximation, where each state carries a feature vector and the estimate is . Temporal-difference learning with this approximation, linear semi-gradient TD(0), is one of the basic algorithms of the field, and Chapter 9 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) presents its analysis: where the algorithm can converge, why that point exists, and how good it is.
The history is short. Sutton (1988, doi:10.1007/BF00115009) introduced TD learning and showed positive definiteness of the matrix governing its expected update. Dayan (1992, doi:10.1007/BF00992701) extended convergence to TD(λ). Tsitsiklis and Van Roy (1997, doi:10.1109/9.580874) proved convergence with probability one for linear TD(λ) under on-policy sampling and bounded the error of the limit. Bradtke and Barto (1996) introduced least-squares TD (LSTD), which computes the same limit directly.
A finite Markov decision process has finite sets of states , actions and rewards , and dynamics , the probability of next state and reward after action in state . A policy is a probability distribution over actions for each state. It induces a Markov chain on states with transition matrix , , and expected one-step reward . For a discount rate , the true value is , the expected discounted return.
A state distribution is stationary if ; write . The feature matrix is the matrix with rows . The mean square value error of a weight vector is
Linear semi-gradient TD(0) updates . In steady state its expected update involves
and the TD fixed point is . A real square matrix , not necessarily symmetric, is positive definite if for every . The key matrix is .
Under the hypotheses above, with every and linearly independent feature columns, is invertible, , and
Positive definiteness of is the reason on-policy linear TD(0) is stable: it makes the expected iteration contract toward the fixed point for small step sizes, and it guarantees that the fixed point exists and is unique. The error bound (9.14) quantifies the price of bootstrapping: the limit of TD can be worse than the best linear approximation, but by at most the factor . The same objects , and the key matrix reappear in LSTD, in the analysis of off-policy divergence (Chapter 11 of the book, where is no longer the stationary distribution of and positive definiteness fails), and in gradient-TD methods.
All results here are known. The book gives the positive definiteness argument in a box and cites (9.14) without proof. None of them has a machine-checked proof on the platform; the general Woodbury identity (FamousTheorems.woodbury_identity) is available, and (9.22) is its rank-one case written for the LSTD recursion. The mission produces a formal account of the finite-state theory of linear TD(0), with every hypothesis the book leaves implicit stated.
The key matrix is not symmetric, so the usual tools for symmetric positive definite matrices do not apply directly, and is positive definite only because of the specific interplay between and : if is replaced by a non-stationary distribution the claim is false (this is the off-policy counterexample of Chapter 11). The error bound (9.14) is not a consequence of positive definiteness alone. The TD fixed point is not the minimizer of , and has to be compared with the error of the -weighted projection of , which requires controlling in the -weighted norm. The book gives no argument for this step.
The Lean development lives in the namespace SuttonBartoRL.LinearTD. The MDP has four-argument dynamics with a finite reward set and one action set for all states; policies are stochastic. is defined from expected discounted returns as the series , never from a Bellman equation or from . and are defined as the book's steady-state expectations (9.11), as finite sums over , and ; the matrix form is a milestone, not a definition. Features are a matrix Matrix S (Fin d) ℝ with rows ; linear independence of its columns is LinearIndependent ℝ Xᵀ. Positive definiteness is a custom predicate , not Mathlib's Matrix.PosDef, which requires symmetry. The minimum in (9.14) is expressed by quantifying over every . The matrix inverse is Mathlib's, which is zero on singular matrices; the goal therefore asserts invertibility of explicitly.
Hypotheses the book leaves implicit and the statements make explicit: (the continuing case); a stationary distribution of the chain induced by with for every (otherwise the key matrix is only positive semidefinite); linearly independent feature columns (the book's "degenerate cases", p. 205). The box calls the off-diagonal entries of the key matrix "negative"; they are zero wherever , so the criterion is stated with nonpositive entries. The book's sentence that "ensures that is always invertible" (p. 229) is false in general, because the summands are not positive semidefinite: with , , , , one gets . It is not stated; (9.22) carries invertibility of and a nonzero denominator as hypotheses.
A statement in which is defined as the solution of the projected equation, or in which is assumed invertible or positive definite, would make the goal trivial or empty; neither is done. Convergence of the stochastic algorithm with probability one is not stated, since the book says it needs conditions and a step-size schedule it does not give. The bound for the episodic case and for other bootstrapping methods (p. 208) is stated only by reference in the book and is not a target.
Useful infrastructure: the -weighted inner product and orthogonal projection onto the column space of , the non-expansiveness of a stochastic matrix in the norm of its stationary distribution, and the positive definiteness criterion for non-symmetric matrices. All of these are reusable in the off-policy and average-reward chapters of the book. Contributions of these lemmas, and of alternative proofs of the milestones, are welcome.