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.
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?
Paging is the problem of managing a fast memory that holds pages out of : when a requested page is not in fast memory (a page fault), some resident page must be evicted, and the cost of an algorithm is its number of faults. Practitioners have many eviction rules. Least-recently-used (LRU) performs well on real workloads but can be times worse than the optimal off-line schedule; the randomized marking algorithm of the same paper is -competitive and so has better worst-case guarantees. Fiat, Karp, Luby, McGeoch, Sleator and Young asked in 1991 whether one on-line algorithm can combine the advantages of several given ones, and answered the question exactly: the attainable combinations of ratios are characterized by one inequality (arXiv:cs/0205038, §6).
The question of combining on-line algorithms has since become a theme of its own: combining heuristics with worst-case-safe algorithms, and, more recently, combining machine-learned predictions with robust fallbacks, both ask for the same kind of guarantee against several reference algorithms at once.
A type consists of servers and a finite set of vertices with the uniform metric: two distinct vertices are at distance . This is paging: vertices are pages, the vertices covered by servers are the pages in fast memory, and a server move is a page fault.
A deterministic on-line algorithm of type has an initial configuration of its servers and, after each request , moves servers so that some server covers ; its configuration after a request sequence depends only on that sequence. Its cost on a request sequence is the total distance its servers travel, i.e. the number of server moves.
For algorithms and of the same type and a constant , is -competitive against if there is a constant such that for every request sequence
A sequence of positive reals is realizable if for every type and every deterministic on-line algorithms of that type there is a deterministic on-line algorithm of the same type that is -competitive against for every .
For and positive reals ,
In the order of the paper's proof:
The result. Theorem 6 is an exact characterization, not a bound: the region of simultaneously attainable ratios against arbitrary deterministic paging algorithms is . For example, any two paging algorithms can be combined into one that is -competitive against each, and no better symmetric pair is possible in general. Combined with Theorem 7 of the same paper (not part of this mission), the same region is attainable against randomized algorithms, which is how LRU's practical behaviour and the marking algorithm's worst-case guarantee can be obtained within constant factors by one algorithm.
Formalizing it. The theorem has been proved since 1991; no machine-checked proof is known. A formal proof produces a reusable notion of competitiveness of one on-line algorithm against another, built on the published KServer_model definitions, and a formal account of the scheduling fact at the core of the sufficiency proof.
Sufficiency looks like an averaging argument, but the combined algorithm cannot simulate the and follow one of them: switching between their configurations costs up to per switch, which no additive constant absorbs. The accounting has to charge each of 's faults to a specific move of a specific , and the charge must be injective; the paper's claim that is at least the number of punishments is where this happens, and it depends on how server intervals are matched. The allocation of faults to algorithms is then a deadline-scheduling problem whose feasibility is exactly , and the floor functions make the counting delicate at the boundary. The paper's own definition of punishment only counts intervals that start with a move, so the first faults of (servers on their initial vertices) need separate treatment; they are absorbed by the additive constant.
Necessity needs the right family of hard instances: the algorithms must never move at the same step, which pins the type to .
The Lean development works in the namespace CompetitivePaging.Combining and imports the published KServer_model definitions: KServer.OnlineAlgorithm k M (a configuration map from request prefixes to Fin k → M with a serving condition) and OnlineAlgorithm.cost. Committed conventions:
k : ℕ and any finite M : Type with a metric in which distinct points are at distance ; realizability quantifies over all of them, never over one fixed type;Trivializing encodings are ruled out: realizability is not stated for a single fixed type, the metric is not the metric of Fin n, and the competitive constant is not allowed to depend on the request sequence.
A complete proof needs the construction of the punishing algorithm as a KServer.OnlineAlgorithm (a lazy, injective algorithm whose moves depend on the prefix and on the 's configurations), the injective charging argument, the scheduling lemma, and the explicit shuttle algorithms. The scheduling lemma and the charging lemma are independent of paging and reusable. Proofs of any milestone are welcome, as are alternative statements of the sufficiency construction.
The Hitchcock transportation problem asks how to ship a commodity from supply points to demand points at minimum total cost. It was posed by Hitchcock in 1941 and is one of the founding problems of linear programming and network optimization; it is solved routinely in logistics, and its structure (a bipartite network with supplies, demands and per-unit costs) recurs in assignment, optimal transport and matching.
The classical algorithms for it, the Ford–Fulkerson primal–dual method among them, augment flow one path at a time. With integral data their number of augmentations is bounded only by the total supply , which is exponential in the number of binary digits used to write the data. Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems (J. ACM 19(2), 1972, doi:10.1145/321694.321699), introduced capacity scaling: solve a coarse version of the problem first, then refine one binary digit at a time. Their Theorem 9 (p. 260) bounds the total number of augmentations by a quantity proportional to times the number of bits of the data, which made the transportation problem, and through standard reductions the minimum-cost flow problem, one of the first network problems with a polynomial-time ("good") algorithm in the sense of Edmonds.
Timeline. Hitchcock (1941) posed the problem; Ford and Fulkerson (1956–1962) gave the primal–dual labeling method and the optimality conditions by node potentials; Edmonds and Karp (1972) gave the scaling method and the bound formalized here. Strongly polynomial algorithms, independent of the size of the numbers, came later (Tardos 1985; Orlin 1988).
The network of Figure 1 (p. 259) has a source , a sink , supply nodes and demand nodes , with . Its arcs are with capacity and cost ; with capacity and cost ; with capacity and cost ; and the return arc with capacity and cost . The supplies and demands are positive integers with .
A flow assigns a nonnegative number to every arc, at most the capacity, with inflow equal to outflow at every node. Write , , ; the value of is , and a maximum flow is one of largest value. Its cost is ; a flow is extreme if no flow of the same value is cheaper. A flow is pseudo-extreme if there are real with for all and whenever .
An augmenting path relative to is a sequence of distinct nodes from to in which each step either follows an arc with spare capacity or traverses backwards an arc carrying positive flow; augmenting pushes the minimum spare amount along it and raises by .
For , Problem has the same network and costs, with capacities and . Choose with every . The scaling method solves Problems in turn. Each phase performs augmentations keeping every flow pseudo-extreme, until no augmenting path is left. Problem starts from the zero flow, and Problem starts from twice the final flow of Problem .
For every run of the scaling method, the total number of flow augmentations satisfies
The bound holds for every admissible for the data and every choice of costs, and is stated with the paper's constant exactly.
The result. Theorem 9 shows that scaling reduces the number of augmentations from order to order , which is roughly the length of the binary encoding of the data. Combined with the cost of one augmentation it gives a polynomial-time algorithm for the transportation problem; through the reduction of minimum-cost flow to transportation (p. 261) it gives one for minimum-cost flow. Capacity and cost scaling became standard techniques in network optimization and in combinatorial optimization generally. Theorem 8 and the pseudo-extreme criterion are the optimality certificates for transportation, a special case of linear-programming complementary slackness.
Formalizing it. The theorem has been proved since 1972. This mission produces a machine-checked version of the bound, of the exact counting argument (eq. (6)) and of the arithmetic estimate that turns it into the stated constant, together with the potential-based optimality conditions for the transportation network. To our knowledge no machine-checked bound on the number of augmentations of a flow algorithm exists on the platform.
The obvious argument bounds the number of augmentations by the increase in flow value, since each augmentation raises the value by a positive integer. Applied to Problem 0 directly this gives only . The scaling bound needs three things that the naive count does not supply. First, doubling the final flow of Problem must give a feasible, still pseudo-extreme, starting flow for Problem (Lemma 3). Second, the gap between that start and the optimum of Problem must be small, which requires the exact maximum-flow value of each scaled problem. Third, the telescoping sum of the gaps must be estimated against with the floors handled exactly. Integrality of every intermediate flow is not assumed; it has to be carried along the run from the integral capacities and the zero start.
Everything lives in the namespace EdmondsKarp.Scaling. Nodes form an inductive type (s, t, src i, dst j). A flow is a structure with components f0, fx, fz, ret for the four arc families, real valued; the infinite capacities are encoded by the absence of an upper bound. IsMaxFlow is a predicate comparing values with every flow, not a supremum. Problem uses natural-number division for . Augmenting paths are lists of distinct nodes from s to t whose consecutive pairs have positive residual amount (resCap, valued in WithTop ℝ); they never use the return arc.
A run of the scaling method (IsScalingRun) is a family of phases for . It starts from in Problem , restarts from in Problem , and advances by one augmentation per step. Every flow is pseudo-extreme, and each phase ends with no augmenting path left. The paper's path-selection rule (minimum weight for the modified reduced costs ) is abstracted to this invariant, which the paper states for it, so every run of the paper's method is covered.
The goal compares the count, cast to , with , using Real.logb 2 and Int.floor. The constant is the printed one; neither nor a weaker constant is acceptable. Positivity of all is a hypothesis, because without it the printed bound is false (for , , , one augmentation is needed and the bound is negative). A formalization in which runs could be empty or never reach a maximum flow would trivialize the goal; the run predicate forbids this, and it is satisfiable (for instance with , , and one augmentation).
A complete development needs max-flow/min-cut for the bipartite network, integrality of flows along a run, the exact value of , the telescoping identity and floor/logarithm estimates. LP duality or complementary slackness is needed only for Theorem 8. The augmenting-path and max-flow lemmas are reusable for other bipartite flow problems. Contributions welcome: proofs of any milestone, and a formalization of the paper's exact path rule showing that it satisfies the invariant.
The economic order quantity (EOQ) is the most widely used formula in inventory management. It assumes that demand is a deterministic constant stream. Real demand is random, and the model that accounts for this, the continuous-review policy with stochastic demand, has no closed-form optimum: for decades its optimal parameters were computed numerically, one instance at a time, which gave little insight into how the stochastic system behaves. Practitioners nevertheless kept using the EOQ quantity in stochastic systems and observed that the cost penalty was small (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978), without an analytical explanation.
Zheng (Management Science 38(1), 1992) supplied that explanation. By minimising the average cost first over the reorder point and then over the order quantity, he obtained two simple optimality equations and compared the stochastic model with the EOQ model under the same cost structure. One of the results is the goal of this mission: for every leadtime-demand distribution, using the EOQ order quantity in the stochastic system raises the average cost by at most one eighth. The paper extends Federgruen and Zheng (1988), who treated the discrete-demand version of the cost function.
A single item faces demand at rate . Orders are delivered after a fixed leadtime , and stockouts are backordered. Each order costs a fixed . Inventory is held at cost rate per unit and backorders are penalised at cost rate per unit. Let be the demand during a leadtime, with mean . The newsvendor cost
is the rate at which expected inventory costs accrue at time when the inventory position at time is . It is convex, and it is assumed, as in the paper, to attain its minimum at a unique point .
A policy orders units whenever the inventory position falls to the reorder point . Its long-run average cost is
For a fixed let be an optimal reorder point, and set
is the average cost when the reorder point is chosen optimally for ; an order quantity minimising over is the optimal order quantity, and is the optimal cost.
The EOQ model is the special case in which the leadtime demand is the constant . Its cost rate is , and its optimal order quantity is
The subscript marks every object of the EOQ model (, , ).
is the stochastic cost at the EOQ quantity with the reorder point re-optimised for it. The bound holds for every leadtime-demand distribution and every value of the parameters.
In the order the goal's proof uses them:
The theorem is a distribution-free worst-case guarantee for the most common heuristic in inventory practice. It says that the EOQ formula, which needs only the mean demand rate and three cost parameters, loses at most against the true optimum, and that the loss is smaller when is close to or to . Combined with the paper's Theorem 2 (the gap is bounded as grows), it implies that the relative loss vanishes as the fixed ordering cost grows. The milestones along the way (the optimality conditions of Theorem 1, the monotonicity of the optimal reorder point, the comparison of with its EOQ counterpart) are the standard structural facts about continuous systems and are reused throughout the inventory literature.
The result is proved in the paper. No machine-checked version of it, or of the optimality conditions for the continuous cost (1), is known to exist. The platform has related but different formalizations: the discrete cost function with integer (InventoryControl_rqDiscrete), the cost under normal demand (InventoryControl_rq), and the EOQ without backorders (InventoryControl_eoq). A complete development here provides the continuous machinery for an arbitrary leadtime-demand distribution.
The paper's proofs differentiate and twice (Eqs. (4), (5)), which presupposes a leadtime demand with a smooth density. The formalization does not assume one, so that discrete demand, such as the Poisson demand of the paper's own numerical study, is covered. Every step that the paper takes through derivatives, in particular the convexity of and the slope bound , has to be established by other means: through one-sided derivatives or chord arguments for the convex function , whose kinks are where the derivative-based argument breaks. The definition of as a minimiser also means its existence and uniqueness must be proved before any property of , or can be used.
IsQRModel: , the conditions on , and the unique minimiser of (paper, p. 90). is a separate hypothesis. No density is assumed.In stochastic optimization the law of a random return is rarely known exactly, while its mean and variance can be estimated. A robust mean-covariance decision maker therefore evaluates a utility by its worst case
Popescu (Operations Research 55(1), 2007) shows that for large classes of utilities this infinite-dimensional problem collapses to a one-dimensional one. The paper projects multivariate problems to a single dimension (the subject of the first mission of this series) and then asks for which the univariate worst case sits on laws with two support points. This mission formalizes the answer the paper gives for utilities whose marginal utility is decreasing and changes curvature once, with finite limits: log-logistic utilities used in statistics and classification, and catenary-type utilities , each plus a concave quadratic.
The result has a bounded-support precursor: Birge and Dulá (Annals of Operations Research 30, 1991, Theorem 5.1, as cited on p. 102 of Popescu 2007) proved an analogous two-point statement for functions on a bounded interval. Popescu's Proposition 5 is the unbounded version on the whole real line.
Let .
and (lemma1Quad).
partnerPoint) and (prop5Gap).If is differentiable, is inverse S-shaped, and the limits and exist and are finite, then
The result. Through the paper's Proposition 4, two-point support turns the worst-case expected utility over all laws with mean and variance into a minimization over a single parameter of . Combined with the projection property of the paper's Section 2, this gives tractable robust counterparts of multivariate stochastic programs whose objective depends on a linear combination of random returns. Proposition 5 is the paper's sufficient condition that places a concrete class of utilities in this regime; it is also closed under adding any quadratic.
Formalizing it. The result is proved on paper; no machine-checked version is known. The formalization produces a checked characterization of two-point support (Lemma 1), a reusable encoding of convex-concave and S-shaped functions, and a proof of Proposition 5. The printed final step of the paper's proof is incomplete (see Difficulty), so a complete formal proof requires an argument the paper does not spell out.
Conditions (a) and (b) of Lemma 1 come from a sign change of on : the two limits in milestone 4 need a l'Hôpital-type argument and the continuity of a monotone derivative. The central difficulty is condition (c): showing that the quadratic built from a pair lies below on the whole line. The obvious argument takes any zero of and counts the intersections of the linear with the inverse S-shaped . This fails when is affine on an interval: a zero of can then produce a quadratic that coincides with on but crosses above just left of . A proof must therefore choose the zero of , or the pair , with care, and the curvature hypotheses are not strict.
ℝ → ℝ; is deriv u, and the goal assumes Differentiable ℝ u. Finite limits are Tendsto (deriv u) atBot (𝓝 l) and Tendsto (deriv u) atTop (𝓝 l) for some real l; the one-sided limit at is along 𝓝[<] μ.StrictMono); the paper writes "nondecreasing" for the weak notion. Convexity and concavity are ConvexOn/ConcaveOn on the open half-lines Set.Iio x₀, Set.Ioi x₀, as printed.Useful infrastructure: l'Hôpital's rule at infinity (Analysis/Calculus/LHopital), Darboux's theorem for derivatives, the intermediate value theorem, and one-sided limits of monotone functions. The shape definitions of Definition 2 are reusable for S-shaped value functions elsewhere (prospect theory, sigmoidal utilities). Proofs of the milestones, of the goal, and alternative arguments for condition (c) are all welcome. Related platform work: Wasserstein Distributionally Robust Optimization II.
Online convex optimization is a repeated game between a learner and an adversary. In each round the learner commits to a point of a convex set ; only then is a convex cost function revealed, and the learner pays . The learner is judged by its regret: its total cost minus the total cost of the best fixed point chosen in hindsight. The model covers online portfolio selection, online regression, prediction with expert advice and the analysis of stochastic gradient methods, and it is the standard language of online learning theory.
Zinkevich (ICML 2003) showed that projected gradient descent with step sizes of order has regret for any convex costs with gradients bounded by on a set of diameter , and this rate cannot be improved for linear costs. Hazan, Agarwal and Kale (Machine Learning 69, 2007) asked what curvature buys. Their first result, the subject of this mission, is that the same algorithm with the faster step sizes has regret only logarithmic in once every cost function is -strongly convex. The paper's other three results (the Online Newton Step, Follow the Approximate Leader and Exponentially Weighted Online Optimization, for exp-concave costs) are the subject of the other missions of this series.
Fix and a nonempty, closed, bounded, convex set , with the Euclidean norm (§2.1, p. 171).
IsProj P y z).(IsOGDRun P η f x).
For , cost functions that are -strongly convex on with gradients bounded by on , and any run of Online Gradient Descent whose step after round is , for every and every :
This is LogRegretOCO.OGD.ogd_regret_bound. The constant is the paper's, and at the bound reads .
UnderstandingML.projection_lemma, and is reused as a reference item.The last step of the argument is the harmonic-sum bound , which Mathlib already provides (harmonic_le_one_add_log).
The result. Theorem 1 separates two regimes of online convex optimization: regret for general convex costs and for strongly convex ones, with an algorithm that costs one gradient and one projection per round. Through the online-to-batch conversion, the same step-size schedule gives the rate of stochastic gradient descent on strongly convex objectives. The theorem is also the reference point for the paper's weaker exp-concavity assumption, under which the other three algorithms obtain regret.
Formalizing it. The result is proved and well known; what this mission adds is a machine-checked proof with the paper's exact constant. The Prove2Me platform holds a statement of the textbook version of this theorem (Hazan, Introduction to Online Convex Optimization, Theorem 3.3), OnlineConvexOpt.FirstOrder.online_gradient_descent_strongly_convex_regret, but it is Disproved: its regret is written with a real infimum over the decision set, which Lean evaluates to a junk value. No proved version of the logarithmic bound is on the platform. The strong-convexity inequality, the one-step projected-gradient inequality and the telescoping argument are reusable by every later formalization of gradient methods on the platform.
The argument is short, and its difficulty lies in the bookkeeping. The telescoping sum of squared distances cancels exactly only with the right step-size indexing: the step taken after round must be . Reading Fig. 1 literally with makes the step after round equal to , and the sum then leaves an uncancelled term that the printed bound does not contain. Strong convexity is a statement about the Hessian, so the curvature inequality (1) needs a second-order Taylor expansion along a segment of ; convexity of keeps the segment inside the set where the Hessian bound holds. The projection step needs the obtuse-angle property of Euclidean projection onto a convex set.
Points are EuclideanSpace ℝ (Fin n), so is the Euclidean norm (the sup norm of Fin n → ℝ would change the gradient bound). Cost functions are functions on all of , as the paper's use of gradients and Hessians presupposes; the gradient is Mathlib's gradient, and the Hessian quadratic form is the second Fréchet derivative applied to . Rounds are 1-based: x 0, f 0 and η 1 are never read, and sums run over Finset.Icc 1 T. The run of the algorithm is a predicate on the whole trajectory, required at every round; the projection is a predicate (nearest point of ), which is unique for nonempty closed convex .
Choices and corrections relative to the printed text:
η (t + 1) = 1 / (H * t) for on the step sizes of Fig. 1.A regret bound written with a real ⨅/sInf over , or a bound for an arbitrary sequence satisfying Eq. (2) instead of a run of the paper's algorithm, would not be Theorem 1; the goal quantifies over every comparator in and carries the run predicate, the Hessian hypothesis and the gradient bound. The hypotheses are jointly satisfiable: on the closed unit ball, with meets all of them.
Contributions welcome: proofs of the two inequalities and of the goal; a general projection lemma for positive semidefinite (Lemma 8 in full, needed by the Online Newton Step mission) is reusable beyond this mission.
In Witten's cubic open string field theory (Witten 1986) the interaction glues half-strings together, and in the usual center-of-mass variables the action contains infinitely many time derivatives. Such a theory has no evident initial value formulation, which obstructs a Hamiltonian treatment and a direct discussion of causality.
Erler and Gross (2004) show that after a unitary change of basis in which the string field depends on the lightcone component of the string midpoint (and on transverse center-of-mass coordinates), the cubic vertex contains no derivatives with respect to lightcone time. This reduces to five linear relations among the Neumann coefficients of the three-string vertex, the midpoint identities (A.6)–(A.10) of the paper. One of them, (A.8), is a closed numerical identity: a specific infinite series built from Neumann coefficients equals , where is the zero-mode Neumann coefficient. This mission formalizes that identity and the chain of intermediate results the paper uses to prove it (Appendix B), together with a divergence statement from Section 2 explaining why other midpoint bases fail.
Define real constants () by the expansion
For real the left side is , so is the -th Taylor coefficient of at (e.g. ). The even Neumann vector and the vector are
In Lean these are ErlerGross.neumannA, ErlerGross.neumannMEven (with neumannMEven n ) and ErlerGross.betaVec. Two auxiliary objects appear in the proof: the (B.3) terms
(ErlerGross.b3Term) and the -basis integrand
(ErlerGross.kappaIntegrand), which arises from the continuous spectrum of the Neumann matrices (Rastelli–Sen–Zwiebach 2001).
formalized as: the series converges absolutely (Lean HasSum) to .
In the paper, (A.8) is one of the relations which, together with (A.6), (A.7), (A.9), (A.10), removes lightcone-time derivatives from the cubic vertex. This is what gives the theory an initial value formulation in lightcone time and makes the Hamiltonian BRST quantization of Section 4 possible. Unlike the other four identities, which are relations between distributions and are verified in the paper's spectral basis, (A.8) is an equality of real numbers. It can therefore be checked completely in Lean.
A complete formalization would produce a machine-checked proof of a Neumann-coefficient identity. It would also add reusable material: Taylor coefficients of , the integral, and digamma-type evaluations of rational series.
The goal defines through Taylor coefficients, which have no closed form. The paper does not sum the series in the mode basis. It moves to the continuous basis of the Neumann spectrum and closes a contour. That step rests on eigenvector expansions and the principal-value distribution , neither of which is in Mathlib. A direct route has to connect the coefficients to the integral , or to the series , some other way. The terms of decay like . The terms of the goal series decay only like , so the goal series converges slowly.
iteratedDeriv.HasSum is unconditional (equivalently absolute) convergence. Every statement asserts convergence, so no statement can hold only because Lean assigns to a divergent tsum.Chapter 3 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks which of the assumptions behind the index theorem can be dropped and which cannot, using the simplest bandit processes there are: jobs, which pay a single reward when they complete. Along the way it settles three questions that matter on their own. When identical machines run in parallel, which schedule of deterministic jobs minimizes the total completion time (Baker's theorem), and what does the equal-ratio case look like (Theorem 3.3)? When an object is hidden in one of several boxes and each search costs money and may fail, in what order should the boxes be searched (Blackwell's search-index theorem, Theorem 3.6)? And when two bandit processes discount at different rates, is there still an index policy (Nash's Theorem 3.4)? The search theorem is the chapter's example of what the index machinery yields once undiscounted criteria are admitted through the limit ; the scheduling results are the source of the counterexamples that show a second machine breaks the index structure.
Jobs on parallel machines. There are jobs with service times and weights , and identical machines. A schedule assigns each job a machine and a position in that machine's processing order; each machine processes its jobs consecutively. The completion time of a job is the total service time of the jobs on its machine up to and including it; the flow time is and the weighted flow time . The load of a machine is the total service time assigned to it, and is its excess over the average . The SPT list schedule sorts the jobs by increasing service time and deals them out cyclically to the machines. The level of a job is its position counted from the end of its machine's schedule.
The search problem (Problem 3). A stationary object is hidden in one of boxes, in box with probability . A search of box costs and finds the object with probability if it is there. A search policy is a sequence of boxes; after unsuccessful searches of box the posterior probability that the object is there is proportional to , and the search index of the box is , the current probability of finding the object per unit cost. The expected cost of a policy is .
Two discount factors. Bandit process (state space , kernel , reward ) discounts at rate and at rate ; a reward obtained at time is worth or times its face value according to which process produced it. The cross indices are and with the roles exchanged: each is computed from one process's stopping times but with the other's discount factor in the denominator. The book prints the denominator as and compares with at every time; both are corrected here (see the Theorem 3.4 item), since the printed rule is not optimal. The family is the two-armed Markov bandit of the Bandit Algorithms model on the disjoint union .
For prior probabilities summing to one, detection probabilities and costs , a search policy is optimal if and only if at every step it searches a box of maximal current index :
Theorem 3.3, as the identity when ; Theorem 3.4 in discrete time and corrected, that a policy selecting, at time , when and when attains the supremum of the bandit-dependently discounted payoff; Theorem 3.7, that SPT minimizes the flow time on machines and that the optimal schedules are exactly those placing the -th block of longest jobs at level from the end, for some order of the equal jobs.
Theorem 3.6 is the classical solution of the discrete search problem (Blackwell, reported by Matula 1964; Kadane 1969): the greedy rule in probability-per-cost is optimal, and every optimal policy is of that form. The book derives it from the index theorem through an auxiliary family of bandit processes (Problem 3A) and the undiscounted limit (Corollary 3.5), which is why it sits in this chapter; as a statement it is elementary and self-contained, and it is the template for the tax problems and Klimov's model of Chapter 4. Theorem 3.7 and Theorem 3.3 are the positive results about parallel machines that survive the loss of the index structure; Theorem 3.4 shows the index theorem's shape persisting under bandit-dependent discounting, with two twists: each index depends on the other process's discount factor, which is exactly why it does not extend to three processes, and the comparison at time weighs the indices by and , so the rule is not stationary in the states. The printed statement misses the second twist and misnormalizes the first; two one-state bandits paying () and () are best played and then forever, which no stationary rule does.
None of these is machine-checked. Formalizing them gives the platform an optimality theorem for an infinite-horizon search process with an explicit index characterization in both directions, the standard parallel-machine flow-time results with a precise uniqueness clause, and a first statement on the Bandit Algorithms two-armed model with unequal discounting.
For Theorem 3.6 the obvious route, comparing two adjacent searches, gives only that interchanging a pair in the wrong index order lowers the cost; turning that into optimality over all infinite sequences needs that an optimal policy exists (costs are bounded below by zero and the index policy has finite cost), that a policy neglecting a box of positive prior has infinite cost, and that any first deviation from the index rule can be improved by moving a later search forward, which requires tracking how the not-found probability changes along the whole tail. The converse direction is the same interchange run backwards, and the tie case must be handled so that the equivalence is exact. Theorem 3.7's first part follows from writing the flow time as with the level and applying a rearrangement inequality over the multiset of levels, but the multiset of levels itself depends on how many jobs each machine gets, so balancing the machine counts is part of the argument; the uniqueness clause needs both that the multiset is forced and that the pairing of levels with service times is forced by strict monotonicity. Theorem 3.4 is the hardest: the book's proof changes the time scale of each process so that the two share a discount factor, which produces a semi-Markov family, and applies the index theorem there; in discrete time on the Markov model one needs either a discrete analogue of that argument or a direct prevailing-charge proof with two charge scales.
Schedules are assignments of machines and positions with distinct positions on a machine, without idling; the flow-time quantities are finite sums over Fin n. The SPT schedule is defined by the ascending rank of a job (ties broken by index) and carries its own injectivity proof. The search cost is a series in of nonnegative terms, so no summability hypothesis is needed and "infinite cost" is literal; the index is stated unnormalized, , which orders the boxes exactly as the posterior index does. The two-discount family uses the platform's MarkovBanditPolicy 2 (S_A ⊕ S_B) and markovBanditMeasure with the kernel that moves an -state by and a -state by ; the payoff is the round-by-round series , absolutely summable for bounded rewards, and the policy condition is imposed at histories whose current states have the right types (all reachable histories do). Hypotheses: , service times positive; , , , ; countable state spaces, bounded rewards, .
Trivializing readings are excluded: the search "iff" is over all sequences, not a finite horizon; the uniqueness clause is stated in full, with ties resolved by any ranking of the equal jobs; the cross indices are suprema over positive stopping times (denominators at least one), and the two-discount rule weighs the indices by , . Welcome contributions: the rearrangement and level-count lemmas for schedules, the interchange lemma for the search cost, and a discrete prevailing-charge argument for Theorem 3.4.
An initial value problem , , is the standard way a law of motion, a growth model or a circuit equation is written down, and only a small minority of such problems can be integrated in closed form. Single-step methods advance the solution by small increments: Euler's method takes the tangent line at the current point, and the higher-order Runge-Kutta schemes refine the same idea. What justifies them is a pair of theorems: that the problem has a unique solution at all, and that the computed polygon approaches that solution as the step size decreases.
This mission is the seventh in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 9, Métodos Numéricos para EDO's, up to the convergence of Euler's method.
Consider the initial value problem
with defined on a rectangle .
Picard's method replaces the differential equation by the integral equation and iterates it:
With , and , the source states the bound on , where is the exact solution.
Euler's method with step produces , . Its local error is per step and its global error .
The goal theorem is the global error statement: for an initial value problem whose exact solution is twice continuously differentiable on and whose right-hand side is Lipschitz in there, there is a constant such that for every step size and every grid point ,
This is the precise form of the source's assertion .
The milestones are the results the chapter states on the way: local existence and uniqueness for the initial value problem under a Lipschitz condition in (Teorema 9.4.1), the Picard error bound, the convergence of the Picard iterates to the solution, and the one-step Taylor identity behind Euler's method.
The global error bound is what makes Euler's method a method rather than a heuristic: it converts an arbitrary choice of step size into a guaranteed accuracy, and it exhibits the characteristic loss of one order between the local error and the global error that recurs for every single-step scheme. The existence and uniqueness theorem is the prerequisite for all of it — without uniqueness there is no well-defined object for the numerical solution to approximate — and the Picard iteration is both the constructive proof of that theorem and a method in its own right.
The global error proof has to handle the interaction of two error sources: the local truncation error at each step and the amplification of previous errors by the Lipschitz constant, which gives the discrete Gronwall recursion . Carrying that recursion to the closed-form bound, and doing it uniformly in , is the core of the mission. The Picard bound requires the iterates to remain inside the rectangle so that the hypotheses on continue to apply — that is what the choice is for — and an induction on with the factorial denominator.
The unknown is a real function of a real variable and is a function of two real variables. A solution is a function satisfying and having derivative at every point of the relevant interval. The Lipschitz condition in the second variable is stated explicitly, , in place of the source's hypothesis that is bounded; for the global-error goal it is assumed for all real and all in the interval, and in the Picard milestones only inside the rectangle. Uniqueness is stated as agreement of any two solutions on the interval, not as uniqueness of a function on all of , since a solution is unconstrained outside the interval. Euler's iterates and the Picard iterates are explicit recursive definitions; the Picard integral is the interval integral, which is total, so no integrability side condition appears in the definition. The constant in the goal is asserted to exist and to be positive, uniformly over step sizes in ; the restriction merely normalizes the range of steps considered.
Chapter 2's tail bounds mostly rest on moment-generating-function control, obtained either directly (sub-Gaussianity) or through explicit combinatorial arguments (Hoeffding, bounded differences). The entropic method offers a different, more structural route: bound a specific information-theoretic quantity — the -entropy of — and convert that bound mechanically into a tail bound via a short ODE argument (the Herbst argument). This method's real payoff appears once it is combined with the tensorization property of entropy across independent coordinates, which is what lets it handle Lipschitz functions of many independent variables — including cases, such as separately convex functions, that elude the purely martingale-based techniques of Chapter 2. This mission formalizes the entropic method's two foundational entropy-to-tail conversions and its central Lipschitz-concentration application, following Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 3.
For (), , the -entropy of a nonnegative random variable is (Eqs. (3.1)-(3.2)). Writing for the moment generating function of , the entropy of has the explicit form (Eq. (3.3)).
A function is separately convex if, for each coordinate , the univariate function obtained by fixing every coordinate but the -th is convex — strictly weaker than joint convexity of itself. is -Lipschitz with respect to the Euclidean norm if for all .
Let be independent, each supported on , and separately convex and -Lipschitz. Then for all ,
If for all ( or ), then for all — the basic entropy-to-sub-Gaussian-tail conversion.
The sub-exponential analogue: if for , then on the same range.
Propositions 3.2 and 3.3 are the two basic entropy-to-tail conversions the entire chapter's entropic method rests on — every subsequent Lipschitz-concentration result in the chapter (including Theorem 3.4 and the more advanced Theorem 3.24) is obtained by first establishing an entropy bound of one of these two forms and then invoking the corresponding proposition. Theorem 3.4 is itself the direct analogue, for independent bounded variables, of Chapter 2's Gaussian Lipschitz concentration (Theorem 2.26) — but crucially requires the extra hypothesis of separate convexity, which the Gaussian case does not need and which cannot be dropped in general.
Formalizing it. No faithful prior art exists on the platform. The one candidate flagged in
BRIEF.md, Talagrand.lipschitz_concentration, was read in full: it is a weighted-Hamming-
distance concentration bound for functions on a finite-alphabet product space Fin n → α,
proved via Talagrand's convex-distance method — a different underlying space (finite alphabet
vs. real-valued bounded coordinates) and a different Lipschitz norm (weighted Hamming vs.
Euclidean) from Theorem 3.4, and not reused here. A search for "log-Sobolev" and "Herbst" turned
up bousquet_herbst_cgf_le_phi_via_herbst/bousquet_herbst_cgf_le_phi_double_integration: these
are abstract calculus lemmas about a generic function satisfying an ODE-type growth
condition (), concluding — a genuinely different statement
shape from Proposition 3.2/3.3's entropy-to-CGF conversions (which conclude a quadratic, not
exponential, bound on ), and not a faithful match. All
three theorems here are drafted as open goals (:= by sorry).
The naive approach to Theorem 3.4 — try to adapt the bounded-differences (martingale) method of Chapter 2 directly — fails, because the bounded-differences method needs to have small coordinatewise oscillation in an absolute sense, while separate convexity alone gives no such uniform bound (a separately convex function can vary arbitrarily fast within the interior of its domain, only its slope is controlled by the Lipschitz condition). The entropic method sidesteps this by working with the -entropy of directly: entropy has a tensorization property across independent coordinates (not itself part of this mission, but what the entropic method's proof of Theorem 3.4 uses) that reduces a multivariate entropy bound to a sum of "one coordinate at a time" contributions, each of which convexity and the Lipschitz condition jointly control — a route with no analogue in the bounded-differences approach.
Separate convexity and Euclidean-Lipschitzness are both restated locally in this chapter's own
sub-namespace (HighDimStat.Concentration), per this book series' rule against importing
another chapter's draft definitions, even though Chapter 2 already defines an
IsLLipschitz for the same Euclidean condition. φ_X'(\lambda)$ (Proposition 3.3) is realized via Mathlib's deriv, a legitimate way to state a hypothesis on a derivative without separately proving differentiability, appropriate at the draft-statement stage. Explicit Integrable`
hypotheses guard the Bochner integral's junk value on non-integrable functions throughout (trap
2), not literal in the book's own propositions but implied by what "the entropy exists" (an explicit qualifier the book itself makes when introducing Eq. (3.2)) means.
Goal substitution, disclosed. BRIEF.md recommends Theorem 3.24 (the two-sided, jointly
convex analogue) as the primary goal, but explicitly names Theorem 3.4 as a fallback "if 3.24's
dependence on the unnumbered transportation-cost inequality (Eq. 3.73, attributed to Samson)
proves too heavy to state faithfully in the time available." Theorem 3.24's proof route depends
on Theorem 3.19 (a general "transportation cost implies concentration" result for an abstract
metric measure space, itself needing a from-scratch formalization of the transportation-cost
inequality (3.58) and the concentration function ) plus the
unproven-in-chapter Eq. (3.73). Building this full stack faithfully was judged to exceed this
chunk's time budget; Theorem 3.4 is drafted instead, using this mission's own budget on
Propositions 3.2 and 3.3 (the two most load-bearing entropy-to-tail conversions of the chapter)
rather than the heavier transportation-cost machinery. Theorem 3.19, Theorem 3.24, and Eq.
(3.73) are all out of scope for this mission and named here as natural follow-on work.
Chapter 7 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) asks when a limit of functions inherits the properties of its members. Pointwise convergence preserves almost nothing: Rudin's opening examples give continuous with discontinuous limit, and sequences where . Uniform convergence is the hypothesis that repairs this, and the chapter's second half asks the converse question — which functions arise as uniform limits from a given family — answered by the Stone–Weierstrass theorem (Theorem 7.32): an algebra of continuous real functions on a compact set that separates points and vanishes nowhere is uniformly dense in all continuous functions there.
The classical Weierstrass approximation theorem (7.26) — polynomials are dense in — is the special case that made the general theorem worth proving, and is used in Chapter 8 for Fourier series and in Chapter 11 for the density of continuous functions in .
This mission is the seventh in a series formalizing Rudin Chapters 1–11; it uses the compactness results of Mission II, the continuity results of Mission IV and the Riemann–Stieltjes integral of Mission VI.
A sequence converges uniformly to on if for every there is with for all and all — the same for every point. A family is equicontinuous on if a single serves all its members in the definition of uniform continuity; it is pointwise bounded if each orbit is bounded, and uniformly bounded if one bound works for all and all .
A set of real functions is an algebra if it is closed under addition, multiplication and multiplication by real scalars; it separates points on if for in some has ; it vanishes at no point of if for each some has . The uniform closure of on is the set of uniform limits on of sequences from .
Let be compact and let be an algebra of real continuous functions on which separates points on and vanishes at no point of . Then
every continuous real function on is a uniform limit on of members of .
Uniform convergence is the standard hypothesis under which limits commute with continuity, integration and (with an extra condition) differentiation, and Theorems 7.11, 7.12, 7.16 and 7.17 are used throughout the rest of the book; Chapter 8 in particular builds the exponential, trigonometric and Gamma functions as uniform limits and differentiates them term by term on the strength of 7.17. Theorem 7.18 shows how weak pointwise differentiability is as a consequence of continuity: a uniform limit of piecewise-linear functions can fail to be differentiable anywhere. Arzelà–Ascoli is the compactness criterion for families of functions, and it is the standard route to existence theorems for differential and integral equations.
Stone–Weierstrass is the structural theorem of the chapter: it replaces the combinatorial Bernstein-polynomial proof of Weierstrass's theorem with a statement about algebras of functions, applicable to trigonometric polynomials, polynomials in several variables, and Lipschitz algebras alike.
Mathlib contains a Stone–Weierstrass theorem for subalgebras of C(X, ℝ) on compact Hausdorff
spaces, and a version of Arzelà–Ascoli. This mission states the results in Rudin's terms — plain
sets of functions on a compact subset of a metric space, uniform closure defined by
sequences — so that they can be used together with the Riemann–Stieltjes integral built in
Mission VI, which is not part of the library.
Stone–Weierstrass is the one theorem in this mission whose proof is genuinely structural: from the algebra one first produces as a uniform limit of polynomials in (which needs the polynomial approximation of on and so cannot be circular with Theorem 7.26), then maxima and minima of pairs, then functions matching prescribed values at two points, and only then the local-to-global patching over a finite subcover. Each step is short; keeping the uniform closure a lattice and an algebra simultaneously is the bookkeeping burden.
Two hypotheses are easy to lose and both are necessary: an algebra that vanishes at a point cannot approximate functions that do not, and one that fails to separate two points cannot approximate functions that distinguish them.
Conventions fixed by this mission:
TendstoUniformlyOn … atTop; complex-valued sequences are
used where Rudin allows complex values.Rudin.IsFunctionAlgebra, Rudin.SeparatesPointsOn, Rudin.VanishesAtNoPointOn,
Rudin.UniformClosureOn, defined for sets of functions X → ℝ and a compact subset K.
The goal's conclusion is membership in the uniform closure, i.e. the existence of an
approximating sequence from the algebra.Rudin.EquicontinuousOn,
Rudin.PointwiseBoundedOn, Rudin.UniformlyBoundedOn, stated with explicit and
as in Definitions 7.19 and 7.22.The discrete-time Riccati equation is the central object of linear-quadratic optimal control — the design equation behind LQR/LQG controllers in every modern control stack. Proposition 4.4.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005, §4.1) packages its asymptotic theory: under controllability and observability the Riccati iteration converges to the unique positive semidefinite solution of the algebraic Riccati equation and the resulting closed loop is stable. Alongside it, Lemma 4.2.1 of §4.2 develops K-convexity, the analytical engine behind Scarf's optimality of inventory policies — a foundational result of operations research. Neither the Riccati asymptotics nor K-convexity exists in Mathlib.
Matrices , , , . The Riccati operator (BertsekasRiccatiMap)
is controllable if has rank (BertsekasControllablePair); is observable if is controllable (BertsekasObservablePair). Separately, is -convex (BertsekasKConvex, Def. 4.2.1) if for all , , .
with — BertsekasDP.riccati_convergence_stability (goal). Milestones: Lemma 4.2.1(a)–(d) (kconvex_of_convex, kconvex_combination, kconvex_expectation, kconvex_sS_structure), culminating in the structure theorem for continuous coercive -convex functions.
The Riccati result is the mathematical license behind steady-state LQR design: it guarantees the design equation has one meaningful solution, that iterating the finite-horizon recursion finds it, and that the resulting feedback is stabilizing. Formally it would seed a Mathlib-adjacent theory of matrix fixed-point iterations, positive semidefinite order, and spectral-radius stability. The K-convexity milestones are self-contained real analysis, each of independent reuse value for inventory theory; part (d) is the engine of -policy optimality. All results are classical and proved in the book; the formal work is new.
The Riccati proof interleaves monotonicity of on the psd cone, boundedness from controllability (a steering argument), positivity from observability, and stability extracted from the fixed-point identity via a Lyapunov argument — several pieces of matrix analysis (psd order, congruence, Schur-type manipulations, spectral radius vs. convergence of powers) that must be built or located in Mathlib. The naive route of diagonalizing fails: nothing is symmetric about . For Lemma 4.2.1(d), the difficulty is that is not convex: the minimizer structure must come from the K-convexity inequality applied at carefully chosen points, plus continuity and coercivity.
Real matrices over Fin n; Matrix.PosSemidef/PosDef; matrix inverse is Mathlib's total inverse (zero on singular input — harmless here since along the relevant iterates, which the proof must establish); convergence in the entrywise topology; eigenvalues via spectrum ℂ of the complexified matrix, all strictly inside the unit circle. Rank-based controllability exactly as Def. 4.1.1. K-convexity is stated for all real ; note is forced whenever it is satisfiable (), and the expectation milestone is stated for finitely supported disturbances (integrability automatic).
The Pontryagin Minimum (Maximum) Principle is the fundamental necessary condition of optimal control, in continuous use since 1956 across aerospace guidance, robotics, and mathematical economics. Chapter 3 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops it from the dynamic programming side: the HJB sufficiency theorem (Prop. 3.2.1), an envelope lemma (Lemma 3.3.1), the Minimum Principle itself (Prop. 3.3.1), and its discrete-time counterpart (Prop. 3.3.2). Mathlib's optimal-control coverage is currently near zero — no HJB equation, no adjoint equations, no maximum principle — which makes this the mission with the largest gap between textbook maturity and formal coverage in the series.
Minimize, over admissible pairs, the cost
with continuously differentiable (BertsekasCTModel). Admissible controls are piecewise continuous on — formalized as: bounded image and continuous off a finite set (BertsekasPiecewiseContinuousOn) — and state trajectories are continuous, satisfying the ODE off a finite set (BertsekasCTAdmissibleFrom, parametrized by an arbitrary start ). The Hamiltonian is (BertsekasHamiltonian).
For an optimal admissible pair : there exist an adjoint and a constant with
away from finitely many times — BertsekasDP.pontryagin_minimum_principle (goal). Milestones: Prop. 3.2.1 (hjb_sufficiency_of_continuous), Lemma 3.3.1 (envelope_gradient_lemma), Prop. 3.3.2 (discrete_minimum_principle).
The HJB milestone carries the hypotheses that and are jointly continuous — the consequence of the §3.1 standing assumptions that its proof uses. An earlier version without any regularity hypothesis was disproved: with a discontinuous running cost the cost integrand need not be integrable, and the library's integral of a non-integrable function is .
The Minimum Principle converts an infinite-dimensional optimization into a two-point boundary value problem — the basis of shooting methods and of every "bang-bang" analysis. None of it exists in Mathlib; even the HJB verification theorem would be new. The discrete-time milestone is self-contained multivariable calculus and gives early value; the envelope lemma is reusable well beyond control theory. The results are classical (Pontryagin et al. 1962; the book's Chapter 3); the formal proof of Prop. 3.3.1 will need an honest variational argument — the book's own HJB-based derivation is explicitly informal.
For the goal: the classical proofs go through needle variations and a separation argument, or through regularity of the value function — neither is in Mathlib. The book's derivation assumes differentiability of the optimal value function, which is not a hypothesis of the statement; a formal proof must either supply a rigorous variational argument or add intermediate lemmas as new platform problems (sketching is encouraged). For the HJB milestone, the work is differentiating along a trajectory that satisfies the ODE only off a finite set, then integrating.
States and controls in EuclideanSpace ℝ (Fin n) / (Fin m); gradients in Mathlib's gradient; the ODE and adjoint via HasDerivAt off a finite exceptional set; costs via intervalIntegral. Piecewise continuity includes boundedness of the image, so the cost integrand of an admissible pair is genuinely integrable — the junk-value escape (non-integrable integrand ⇒ integral 0) is closed. Fixed initial state, fixed terminal time, free terminal state; time-independent dynamics (so the Hamiltonian is constant, per the book's remark that time-varying systems lose constancy). is an arbitrary set — no compactness or convexity is assumed in the goal.
Pontryagin's principle as presented by Luenberger is the decisive necessary condition in continuous-time optimal control. It converts an optimization over functions into a pointwise comparison of a Hamiltonian, coupled to the original state equation and a backward costate equation. Luenberger derives the minimum-Hamiltonian convention from vector-space multiplier ideas and a first-order comparison principle. Formalization is especially valuable here because the printed theorem contains a standard but consequential regularity oversight: it asserts a condition at every time even though controls are only piecewise continuous and the cost is an integral. This mission preserves the intended theorem while replacing that false pointwise claim by the mathematically canonical almost-everywhere statement.
Fix t₀ < t₁, a finite-dimensional Euclidean state space OCState n, a Euclidean control space OCControl m, and a permitted-control set Omega. A state-control pair (x,u) is admissible when x t₀ = xInit, the state is absolutely continuous on the interval, the control is almost everywhere strongly measurable and lies in Omega almost everywhere, the differential equation x' = F(x,u) holds almost everywhere in the interior, and the running cost is interval integrable. An optimal pair globally minimizes the interval integral among all admissible pairs.
The dynamics F and running cost ell are continuous jointly in state and control and continuously differentiable in the state variable. Their state derivatives Fx and ellx vary continuously. A global Lipschitz estimate controls changes of F in both state and control. Because an a.e. measurable control need not be bounded, the optimal control is explicitly assumed to have an a.e. norm bound on the compact interval, matching the boundedness inherited from the source's piecewise-continuous model. The operator-valued paths Fx (x₀ t) (u₀ t) and ellx (x₀ t) (u₀ t) are also assumed interval integrable along the optimum. Together these hypotheses provide the measure-theoretic regularity needed for the adjoint and state perturbations. The Hamiltonian uses Luenberger's minimum convention,
The root VectorSpaceOpt.pontryagin_minimum_principle asserts the existence of an absolutely continuous costate lambda with terminal value lambda t₁ = 0. Almost everywhere it satisfies the weak inner-product form of
and almost everywhere on the control interval it satisfies
Two milestones capture source dependencies. control_state_lipschitz_estimate is the Grönwall stability estimate used on p. 263 to control the state response by the integral distance between controls; it explicitly assumes interval integrability of both the state-difference norm and the control-difference norm, so Mathlib's totalized integral cannot hide a nonintegrable input. adjoint_lagrangian_comparison formalizes §9.6, Proposition 1: under an implicit state equation, differentiability in the state, Lipschitz dependence of the state solution, and an adjoint identity, the objective difference agrees with a frozen-state Lagrangian difference up to an explicit filter-level little-o remainder.
This is the flagship analytic mission of the continuation. It connects finite-dimensional differential calculus, Bochner integration, absolute continuity, ODE constraints, adjoints, and localized control variations in one reusable theorem. The definitions form a minimal control framework that can support terminal costs, endpoint constraints, and alternative maximum-principle conventions later. The corrected a.e. conclusion also demonstrates a central benefit of formalization: informal conventions about representatives of controls and isolated time values must be resolved before a theorem can be accepted.
The weak inner-product adjoint equation avoids introducing a coordinate transpose and remains invariant under the Euclidean-space representation. That choice makes the result immediately reusable in later vector-space treatments of transversality and endpoint multipliers.
The difficulty is very high. Mathlib supplies finite-dimensional calculus, interval integration, absolute continuity, measure-theoretic almost-everywhere statements, and Grönwall tools, but not an assembled Pontryagin framework. The mission must coordinate a state-solution stability estimate, state differentiability of the dynamics and cost, existence and regularity of the backward costate, and Hamiltonian comparison against arbitrary admissible values. The control is measurable rather than globally continuous, so every pointwise expression must be placed under an a.e. quantifier where appropriate. The proposition milestone additionally requires a precise little-o interface instead of an unnamed asymptotic remainder.
The proposal covers §9.6, Proposition 1 and Theorem 1, with the regularity inherited from the surrounding discussion made explicit. Both the optimal state and the costate are absolutely continuous. Admissible controls are a.e. strongly measurable, which is a broader measure-theoretic proxy for the source's piecewise-continuous controls and is compatible with integral objectives; the root additionally requires the optimal control to be essentially norm bounded on Icc t₀ t₁, restoring the compact-interval boundedness used by the source. The maps F, ell, Fx, and ellx are jointly continuous; state derivatives are supplied by HasFDerivAt; a uniform Lipschitz bound is stated; and both derivative coefficients along the optimal path are interval integrable. The separate Grönwall milestone requires its state and control norm differences to be interval integrable. The interval is required to have positive length.
There is a documented source erratum. The sentence on printed p. 263 states Hamiltonian minimality for every t, while the proof on p. 264 chooses a neighborhood on which a purported strict violation persists. That step requires continuity at the selected time. Moreover, changing a piecewise-continuous control at a single isolated time changes neither its a.e. class, the state equation, nor the integral cost. Therefore no condition can be forced at an arbitrary jump value. The Lean root uses an a.e. conclusion on Icc t₀ t₁; an alternative source-faithful repair would assert the inequality at every continuity point of u₀. The mission does not claim existence of an optimal pair, compactness of Omega, endpoint constraints, nonsmooth dynamics, or a sufficiency theorem.
AI generated but i think correct. I think the milestones make it really annoying but the central theorem looks correct.
The matrix-multiplication exponent measures the asymptotic number of field operations needed to multiply two square matrices. A bound means that, for every , two matrices can be multiplied using arithmetic operations. Matrix multiplication is a central benchmark in algebraic complexity and a primitive for many algorithms in linear algebra, graph theory, and symbolic computation.
After Strassen showed that , a sequence of tensor constructions reduced the exponent further. Schönhage's asymptotic sum inequality made it possible to exploit simultaneous matrix products rather than a single square product. In 1990, Don Coppersmith and Shmuel Winograd combined an explicit low-border-rank tensor with a block extraction argument based on Salem--Spencer sets. Their basic analysis gave ; coupling the random weights in the tensor square sharpened this to , hence the exact rational consequence .
This mission formalizes that historical Coppersmith--Winograd result. It follows the source tensor and its actual block restrictions, while excluding placeholder “laser values” that are not backed by extracted direct sums of matrix-multiplication tensors.
For a field , an order-three tensor is represented by three finite-dimensional -vector spaces and an element of their tensor product. The matrix-multiplication tensor
encodes multiplication of an matrix by a matrix. A restriction applies one linear map to each tensor leg. A degeneration permits those maps to depend polynomially on a formal parameter and selects their first nonzero coefficient. Thus a degeneration from the diagonal tensor is a border-rank certificate .
The Coppersmith--Winograd tensor with parameter is
It has border rank at most . Its coordinates carry three classes, indexed by , and its six nonzero block types are
The first three blocks are matrix-multiplication tensors with dimensions , , and ; the other three are scalar products. Tensor powers therefore contain many typed rectangular matrix products. The laser method selects a large family with disjoint coordinate blocks and applies Schönhage's asymptotic sum inequality to all surviving products simultaneously.
For every field ,
The Lean goal has the same quantified proposition and the same matMulExp definition as the existing Schönhage-bound mission; only the theorem identifier and rational endpoint change.
The development records the characteristic-free order-three degeneration
and the exact matrix-product dimensions associated with every supported type sequence in . These statements identify the algebraic input before any asymptotic counting is used.
For , the tensor-square grading and the coupled-weight pruning must produce the direct sums and asymptotic inequality stated in Section 8 and in the coupled-constituent lemma on journal pp. 270--272. The final numerical milestone certifies the rational endpoint from exact inequalities, rather than treating the decimal as a proof object.
The result was the strongest matrix-multiplication bound for roughly two decades and introduced the tensor family that underlies the classical laser-method line of work. A formal proof supplies a checked bridge from an explicit border-rank identity to an exponent bound whose combinatorial extraction is substantially more delicate than the earlier Schönhage examples.
The formalization also produces reusable infrastructure. The order-three CW degeneration is an explicit polynomial-family test case over arbitrary fields. The six block identifications and type-count formulas can be reused in analyses of tensor powers. A faithful extraction predicate, stated through actual restrictions to direct sums of MMObj tensors, separates sound laser arguments from formulas that count incompatible or coordinate-sharing blocks as independent.
The mathematical bound is known. The open work is its machine-checked reconstruction in Lean. The border-rank theorem, per-type matrix-product restriction layer, tensor-square support invariant, balanced block calculation, Salem--Spencer set theorem, and exact numerical endpoint are already proved. The unrestricted value/rank bridge, the coupled-constituent extraction, and the full Section 8 auxiliary inequality remain the substantive frontier.
The main difficulty is not expanding or evaluating a decimal logarithm. A tensor power contains exponentially many typed terms, but most share variables. They cannot all be placed in a direct sum, and counting all joint type sequences overestimates the usable matrix products. The source hashes coordinate blocks into a large progression-free set and prunes collisions so that the surviving blocks are genuinely independent.
The improvement adds a second layer. It begins with , regroups variables into five classes, couples weights that were independent in the simpler analysis, and estimates a nontrivial central block by a further extraction. A formal proof must track the direction of every restriction, the exact multiplicities of all block types, and the loss introduced by pruning. Replacing exponential surviving-block counts by a polynomial number of blocks, or using joint entropy without the marginal compatibility constraints, changes the mathematical claim and is outside the mission.
The mission uses the existing TensorObj, MMObj, TensorObj.Restrict, Degenerates, tensorAsymptoticRank, matMulExp, and matMulExp_strassen declarations in the Mathlib environment pinned by the earlier matrix-multiplication mission. Tensor dimensions and type counts are natural numbers; exponent and optimization inequalities are real-valued. All top-level bounds quantify over an arbitrary field, matching the integral polynomial identities used by the construction.
Laser statements must exhibit, directly or through a faithful reusable predicate, restrictions from a tensor power to a finite direct sum of concrete matrix-multiplication tensors. The number and dimensions of the summands remain part of the witness. A constant-valued “laser functional,” a vacuous witness hypothesis, or a capacity definition that discards the exponential number of surviving blocks does not satisfy the mission.
Welcome contributions include restriction composition lemmas, tensor-power block equivalences, multinomial and entropy estimates with all marginal constraints, formal Salem--Spencer pruning, exact real-inequality certificates, and the coupled central-block value lemma. Every milestone should cite the corresponding equation, table, or lemma in the primary paper.
The whole series so far lived in discrete time on finite state spaces. Chapters 20–21 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) lift both restrictions. Running the jumps of a chain at the arrivals of a rate-one Poisson clock produces the continuous-time chain, whose transition semigroup — the heat kernel — converges to stationarity for every irreducible chain, with no aperiodicity hypothesis: continuous time washes out periodicity. On countable state spaces, existence of a stationary distribution is no longer automatic, and the trichotomy of transience, null recurrence, and positive recurrence replaces it; the convergence theorem survives exactly on the positive-recurrent class. The chapter's crown jewel — and this mission's goal — is Pólya's theorem: simple random walk on the lattice is recurrent in dimensions one and two and transient in dimension three and higher. "A drunk man will find his way home, but a drunk bird may get lost forever."
Continuous time (Ch. 20). For a finite chain , the heat kernel at time is defined by Poissonization,
the law at time of a walk taking -steps at Poisson arrival times ( as a matrix exponential). With , the continuous distance and mixing time are and . The lazy version of a discrete chain is ; from Mission VII, the spectral gap is with the largest eigenvalue . The product chain on a product of coordinate spaces picks a uniform coordinate and updates it by that coordinate's chain.
Countable state spaces (Ch. 21). A chain on a countable state space is a function with nonnegative entries and rows summing to one (as convergent series); -step probabilities are defined recursively, and trajectory probabilities are countable sums of path weights. The first return time to is ; a state is recurrent when (tails tend to zero), positive recurrent when moreover (tails summable), and null recurrent when recurrent but not positive recurrent. A stationary distribution is a nonnegative summing to one with (as convergent series). Simple random walk on steps from to one of its nearest neighbours uniformly at random.
Pólya's theorem (§21.2, Examples 21.8–21.9), the capstone of Chapters 20–21:
The results. Theorem 20.1 explains why laziness and aperiodicity pervade the discrete theory — periodicity is an artifact of the discrete clock. The product-chain theorem 20.7 is the cleanest instance of the paradigm (independent coordinates mix in relaxation time ) and the template for the hypercube cutoff of Mission XI. Chapter 21's trichotomy is the backbone of applied Markov chain theory — queueing, branching, renewal — and Kac's lemma with the convergence theorem 21.14 is the standard equipment of any probability course. Pólya's theorem is one of the most celebrated results of twentieth-century probability, the birth of the random-walk-in-dimension- paradigm.
Formalizing them. Mathlib has no continuous-time Markov chains, no Poissonization, and no recurrence/transience theory (its PMF random walks stop far short). The countable-state layer built here — summable stationary equations, tail-sum return times, the recurrence dichotomy — is the missing infrastructure for formalized applied probability; Pólya's theorem is a famous target in its own right, and the half has never been formalized in any assistant to our knowledge.
The heat kernel is an infinite series of matrices: convergence (dominated by the Poisson weights), the semigroup property, and the interchange of the series with matrix products and limits must all be established by hand over tsum. Theorem 20.1 avoids aperiodicity by the number-theoretic fact that the Poisson distribution smears over residue classes — formally, the continuous chain is automatically aperiodic because for . The product-chain bounds need the machinery of Mission VII applied coordinatewise and a careful union bound; the lower bound is a Gaussian-free second-moment argument. On the countable side, everything is series bookkeeping in the absence of Fintype: the recurrence dichotomy is a generating-function (renewal) identity handled through partial sums; Kac's lemma is a mass-transport double-count over trajectories; and Theorem 21.14 needs an aperiodicity-based coupling on a countable product space, the technical summit of the mission. Pólya's theorem itself combines a local central-limit-type estimate for the return probabilities (, obtained by Stirling in and by a comparison argument in higher dimension) with the dichotomy of Proposition 21.3.
Chapter 20 lives on finite state spaces: the heat kernel is a tsum over of Poisson weights times matrix powers (summability is provable, not assumed), continuous distance is a supremum over states, and the continuous mixing time is an sInf over nonnegative reals (junk if the set were empty — excluded under the theorems' hypotheses). Discrete-vs-continuous comparison (Theorem 20.3) is stated with eventual thresholds (), matching the book's asymptotic phrasing. Chapter 21 lives on a Countable type: stochasticity and stationarity are HasSum statements, -step powers are defined recursively with tsum convolutions, return-time tails are countable sums of path weights over finite horizons, and recurrence/positive recurrence are the tail-limit and tail-summability conditions above — measure theory never enters. Pólya's theorem is stated for the origin of with the walk defined by nearest-neighbour steps; the and halves are separate conjuncts of one statement.
How fast does a Markov chain forget its starting point? For a reversible chain the complete answer is coded in the eigenvalues of its transition matrix: the largest eigenvalue is always , and the size of the gap between and the rest of the spectrum is the chain's fundamental time constant — a large gap means fast mixing, a small gap means slow mixing. Chapters 12–13 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop this spectral theory and culminate in the discrete Cheeger inequality of Jerrum–Sinclair and Lawler–Sokal, which says that the spectral gap (an analytic quantity, defined below) and the bottleneck constant (a geometric quantity from Mission IV, also recalled below) control each other:
A chain mixes rapidly exactly when its state space has no bottleneck. This inequality is the backbone of the Markov-chain approach to approximate counting and of spectral graph theory at large; alongside it the chapters provide Wilson's method — the sharpest general technique for mixing-time lower bounds — and the comparison machinery that transfers spectral estimates between chains.
All chains live on a finite state space . A chain with transition matrix and stationary distribution is reversible when the detailed balance equations hold; reversibility is the standing assumption of both chapters. The yardsticks of the series are the total variation distance , the worst-case distance to stationarity , and the mixing time , with ; we write .
The spectral vocabulary: an eigenfunction of is a nonzero with , where ; the number is then an eigenvalue. Out of the spectrum one forms
Functions on carry the weighted inner product — the geometry, denoted , in which a reversible is self-adjoint — and the Dirichlet form
the average squared variation of along the chain's transitions. Finally, from Mission IV: the bottleneck ratio of a set of states is , the conditional probability at stationarity of escaping in one step, and the bottleneck constant is .
Theorem 13.14, the discrete Cheeger inequality: for a reversible irreducible chain,
The results. Theorems 12.3–12.4 sandwich the mixing time between and — the fundamental equivalence of spectral and mixing estimates for reversible chains, prerequisite for the cutoff criterion of Mission XI. The Cheeger inequality converts isoperimetry into spectral bounds; it is the mathematical core of the Jerrum–Sinclair program of polynomial-time approximate counting, and its graph version underlies expander theory. Wilson's method produced the sharp lower bounds for adjacent transpositions and hypercube-type chains; the comparison lemma is the engine behind the shuffle bounds cited in Mission V (§16.1).
Formalizing them. Mathlib has the spectral theorem for symmetric matrices but nothing connecting spectra to Markov chains: no spectral gap, no relaxation time, no Dirichlet forms, no Cheeger inequality in any form. A formalized discrete Cheeger inequality would be a landmark reusable well outside this series (spectral graph theory, expanders); the eigenvalue and Rayleigh-quotient layer built here is what Missions IX (tree relaxation, block dynamics) and XI (cutoff criterion) consume.
Everything routes through one change of basis: conjugating by the diagonal matrix with entries produces a matrix that is symmetric precisely because the chain is reversible, so Mathlib's spectral theorem applies — but transporting the resulting eigenbasis back to , keeping track of orthonormality with respect to the weighted inner product, is a genuine formal-linear-algebra project; nothing about it is deep, all of it is fussy. The definitions of and as suprema over the set of non-unit eigenvalues (finite, and nonempty once ) must be reconciled with the eigenbasis enumeration before any variational argument runs. The upper half of Cheeger is direct from the variational characterization — test it on the indicator function of a bottleneck set , recentred to have mean zero; the lower half is the hard half: the standard proof takes an optimal , decomposes it over its level sets , and applies Cauchy–Schwarz twice, and formalizing that level-set sweep is the main effort of the mission. Wilson's method needs a supermartingale-style iteration of the eigenfunction estimate; its constants are exact, so the inequalities cannot be rounded.
Eigenvalues are defined by real eigenvectors (); for reversible chains this captures the whole spectrum, and all statements assume reversibility wherever the book does. and are suprema of explicit sets of reals; on a one-point space these sets are empty and the supremum takes a junk value, so the affected statements carry the explicit hypothesis , matching the book's implicit assumption of a non-degenerate chain. with total inverse. Theorem 12.3 carries an explicit absorbing the rounding of a real-valued bound to an integer time. The cycle eigenvalue statement exhibits eigenvalues (existence of eigenfunctions); completeness of that list is not asserted. The variational characterization asserts both the minimization identity and its attainment, so it can be used in either direction.
Welcome contributions: the symmetrization API (conjugation by ), Rayleigh-quotient lemmas, level-set (layer-cake) infrastructure — all reused by Missions IX and XI.
Missions II–III produce upper bounds on mixing times. Whether such a bound is sharp is a different question: an bound on a chain that actually mixes in steps hides the truth. Chapter 7 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develops the standard toolkit of lower bounds: the counting and diameter bounds (a chain cannot spread faster than its transition graph allows), the bottleneck ratio (a chain cannot mix faster than it crosses its worst cut), and distinguishing statistics (a chain is far from stationarity as long as some statistic separates from by several standard deviations). The bottleneck bound — closely related to the conductance of the chain and, via Mission VII, to the Cheeger inequality — is the single most important obstruction result in the subject: it is how slow mixing (torpid mixing of Ising at low temperature, in Mission IX) is proved.
For a chain with stationary distribution , the edge measure is , the bottleneck ratio of a set of states is
and the bottleneck ratio of the chain is . The maximal one-step out-degree is ; the diameter is measured in the graph joining when . For a statistic and distribution , and are the finite-sum expectation and variance, and denotes the pushforward of under .
This is Theorem 7.3, the bottleneck-ratio lower bound, the chapter's central theorem.
The counting bound for chains with uniform stationary distribution (§7.1.1, display (7.2)); the diameter bound: any two states satisfy for (§7.1.2, display (7.3)); Proposition 7.8 (a statistic separating means by standard deviations forces ); Lemma 7.9 (projection under a statistic does not increase TV distance); Proposition 7.13 (the lazy hypercube walk satisfies ); and Proposition 7.14 (the top-to-random shuffle needs shuffles, matching the upper bound of Mission III).
The results. Together with Mission III this pins the top-to-random shuffle at — the first sharp mixing result of the series, and the prototype of the cutoff phenomenon formalized in Mission XI. Proposition 7.13 similarly matches the hypercube upper bound and feeds the cutoff analysis. The bottleneck bound is used in Mission IX to prove exponentially slow mixing of the mean-field Ising model at low temperature, and its two-sided refinement is the Cheeger inequality of Mission VII.
Formalizing them. Mathlib has no notion of conductance/bottleneck ratio of a chain, no distinguishing-statistic method, and no mixing-time lower bound of any kind. The pushforward and variance infrastructure over finitely supported distributions is elementary but new, and reusable wherever second-moment methods appear (Wilson's method in Mission VII).
The bottleneck theorem's proof is short but exact: it hinges on the identity for conditioned on , followed by a telescoping estimate of ; the formal cost is manipulating conditioned measures and one-sided TV sums (Remark 4.3 from Mission II). For Proposition 7.8, the second-moment argument runs through Chebyshev on both distributions plus optimization of a threshold — the constants are exact, not asymptotic, so the formal inequalities must be done carefully. Proposition 7.13 requires the binomial mean/variance computation for Hamming weight under both and , including the negative-correlation bound for unrefreshed coordinates. The naive route to a lower bound — "the chain has not left a small set, so it is far from " — is precisely the counting bound and is too weak for the sharp results; the statistics method is what closes the gap.
is an infimum over the subtype of nonempty sets with ; on a one-point space this subtype is empty and the infimum takes a junk value, making the goal trivially true there (the bound carries content only for , as in the book). The counting bound divides by with total division ( gives a trivially true statement). The diameter bound is stated for arbitrary pairs of states through SimpleGraph.dist of the transition graph, which subsumes the book's diameter formulation. Propositions 7.13 and 7.14 are stated for all integer times (resp. ), using monotonicity of instead of evaluating at a real-valued time — this avoids floor artifacts while keeping the book's content. Proposition 7.14 quantifies " large, then large" exactly as the book's iterated limit.
Welcome contributions: monotonicity of in ; conditioned-measure lemmas; variance API for distExp/distVar.
The Convergence Theorem of Mission II says an irreducible aperiodic chain mixes geometrically, but with constants coming from a crude Doeblin decomposition — useless for actual chains, whose state spaces are exponentially large. Chapters 5–6 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develop the two classic probabilistic techniques that give useful upper bounds: coupling — run two copies of the chain jointly so that they meet quickly, and read a TV bound off the meeting time — and strong stationary times — random times at which the chain is exactly stationary, independent of the time. The flagship application is the top-to-random shuffle: repeatedly take the top card of a deck of cards and reinsert it at a uniform position; the deck is well mixed after shuffles, with error at most .
A Markovian coupling of a chain (with the stay-together convention (5.2)) is a chain on pairs whose coordinate marginals are both and which moves diagonal states to diagonal states. The coupling time is the hitting time of the diagonal; its tails are expressed with the trajectory calculus of Mission I.
A randomized stopping time is presented by its stopping rule: for each time and trajectory prefix , a number , the conditional probability of stopping at given the trajectory so far and no earlier stop. A strong stationary time for the chain started at is an almost surely finite such with
i.e. independent of . The separation distance is .
The mission also fixes the concrete chains it bounds: the lazy walk on the discrete torus , the Metropolis chain on proper -colorings of a graph, the Glauber dynamics of the hardcore model with fugacity , and the top-to-random shuffle on decks of cards (states are arrangements, i.e. permutations; position is the top).
Let ,
for the top-to-random shuffle on cards — display (6.16) of the book, the chapter's flagship bound, proved by combining the strong stationary time with the coupon collector tail of Mission I.
Theorem 5.2 and Corollary 5.3 (the coupling bound: , hence ); Theorem 5.5 ( for the lazy torus walk); Theorem 5.7 (Metropolis colorings, : mixing in ); Theorem 5.8 (hardcore Glauber, : mixing in ); Proposition 6.1 with Example 6.7 ( is a strong stationary time); Lemma 6.11 (); Lemma 6.13 (); Proposition 6.10 ().
The results. The coupling bound is the single most used upper-bound technique in the subject: Missions VIII (path coupling), IX (Ising) and XI (cutoff examples) all instantiate it. Strong stationary times and separation distance return in Mission XI (separation cutoff) and underlie perfect sampling in Mission XIII. The three concrete bounds (torus, colorings, hardcore) are the standard first applications and give the first polynomial mixing results of the series; the colorings and hardcore chains are the objects of intense ongoing research on sampling thresholds.
Formalizing them. Nothing here exists in Mathlib. The novel infrastructure is the stopping-rule formalization of randomized stopping times over trajectory prefixes — measure-theory-free, but expressive enough for the strong stationarity identity — and the Markovian-coupling predicate on pair chains. Both are reused later in the series (Matthews method, cutoff, CFTP).
The coupling bound itself is short once Proposition 4.7 (Mission II) is available; the work is in the applications. For the torus, the coordinatewise coupling requires assembling one-dimensional couplings and bounding the coupling time by a sum of one-dimensional meeting times — the formal bookkeeping of "couple coordinate by coordinate" is the real cost, and the constant absorbs it. For Theorem 5.7 and 5.8 the argument is a grand coupling over all colorings/configurations simultaneously; the formal statements quantify only over the resulting bound, but a solver must build the coupling. For Proposition 6.1, the crux is the induction "given cards under the original bottom card, all orders are equally likely" — an exchangeability argument that must be carried through the stopping-rule encoding. Lemma 6.11 is where the definition of strong stationarity does its work; the naive attempt to prove Proposition 6.10 directly from the coupling characterization fails, which is exactly why separation distance is introduced.
Couplings of chains are transition matrices on with marginal conditions stated row by row; the stay-together convention is part of the predicate, matching (5.2). Stopping rules take the trajectory prefix (which includes the starting state), so times "depending on the starting position" are covered; strong stationarity packages the stopping rule bounds, almost-sure finiteness (), and the product identity. The colorings chain lives on the subtype of proper colorings; the hardcore chain is the Glauber dynamics of Mission II restricted to the subtype of hardcore configurations (transitions never leave it). Mixing-time upper bounds carry an explicit for integer rounding where the book's real-valued display would otherwise be false for the integer-valued . The torus statement fixes ; for near the display is false as stated in the book.
Welcome contributions: interface lemmas between setAvoidTailProb of the pair chain and the two coordinates; the taboo-matrix form of coupling-time tails; exchangeability infrastructure for the deck chains (reused in Mission V).
Two quadratic functions can be compared losslessly. The S-procedure says that, when the constraint is strictly feasible, the implication
holds if and only if a single nonnegative multiplier certifies it as a matrix inequality, for some . It is a cornerstone of control theory, trust-region methods and robust optimization, and a rare case in which a nonconvex problem has zero duality gap. The route runs through the theory this mission builds from Boyd & Vandenberghe §5.8–5.9 and Appendix B: strong alternatives for convex inequality systems, cone-program strong duality under a generalized Slater condition, semidefinite programming duality, the LMI theorems of alternatives, and the hidden convexity of the joint range of two quadratic forms.
Log-concave functions are the meeting point of convex analysis and probability: densities of Gaussian, exponential, uniform and Wishart distributions are all log-concave, and countless facts of applied probability flow from one structural theorem — integrating out variables preserves log-concavity. This mission builds the convex-analysis spine of Boyd & Vandenberghe's Convex Optimization (Chapters 2–3) — separation and supporting hyperplanes, dual cones, the first- and second-order differential characterizations of convexity, Fenchel conjugacy — and climbs to Prékopa's theorem via the Prékopa–Leindler inequality, a landmark of Brunn–Minkowski theory absent from Mathlib.
Value decomposition — approximating the value of a joint state by a sum of per-agent local values — is a staple of multi-agent dynamic programming and reinforcement learning, from index policies for restless bandits to modern MARL architectures, yet it is normally used without justification. Chen and Peng (arXiv:2506.02385) supply one. They show a multi-agent MDP admits an exact value decomposition precisely when its transition matrix is not entangled — a notion built in direct analogy with quantum entanglement — and then turn that qualitative characterisation into a quantitative one: a measure of Markov entanglement bounds the decomposition error in general. This mission formalizes that core theory. The goal is Theorem 6, the general N-agent bound in the occupancy-weighted norm; the milestones are the equivalence between separability and exact decomposition, the perturbation machinery that carries a one-step transition error into a value-function error, and the extensions to shared global state and shared rewards. The paper's restless-bandit application, which needs mean-field machinery of its own, is left to a second mission in the series.
The Monge optimal transport problem on the real line with the classical distance cost famously fails to have a unique solution. Juillet (2019) restored uniqueness by considering the strictly concave power costs with and letting : the limit selects a distinguished optimal plan, the excursion coupling, built from the level sets of the difference of the cumulative distribution functions. This mission formalizes the completed-graph construction, the generalized Banach indicatrix identities of Bertoin-Yor, the alternating crossing structure of almost every level, and the marginal identities for the crossing counting measures. It culminates in Propositions 3.5-3.6: every monotone transport plan is concentrated on the paired routes, and the marginals uniquely determine the coupling carried by those routes, including in the presence of atoms.
This mission formalizes the key implication 3=>4 in Juillet's Main Theorem.
How much flow can be sent from a source to a sink through a network with arc capacities — and what certifies that no more is possible? This mission formalizes §7.4-7.5 of Bertsimas & Tsitsiklis. The circulation calculus of §7.4 supplies the two structural tools: the flow decomposition theorem (Lemma 7.1 — every nonzero nonnegative circulation is a positive combination of simple circulations with only forward arcs, with integer when is integer) and the optimality criterion for the minimum cost network flow problem (Theorem 7.6 — a feasible flow is optimal if and only if there is no unsaturated cycle with negative cost). Section 7.5 then formulates the maximum flow problem ( s.t. , , for , ), defines augmenting paths (Definition 7.2: on forward arcs, on backward arcs) and the Ford–Fulkerson algorithm, and proves integer invariance and finite termination for integer capacities (Theorem 7.8). The goal is Theorem 7.10:
(a) if the Ford–Fulkerson algorithm terminates because no augmenting path can be found, the current flow is optimal;
(b) the value of the maximum flow equals the minimum cut capacity
— the archetypal combinatorial min-max theorem, which the book notes can also be read as LP duality (pp. 311-312).
Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time and a recommendation must be sound (wrong with probability at most ) while minimizing . The information-theoretic complexity is : every sound strategy needs , and the Track-and-Stop algorithm — the goal theorem — achieves exactly. The mission also covers the fixed-budget counterpart, sequential halving.
When rewards are binary — a click or no click, a cure or no cure — the subgaussian machinery of Missions I–III is not tight: the variance of a Bernoulli arm degrades near the boundary of , and the correct exponential rate is governed by the binary relative entropy rather than a squared distance. Chapter 10 of Lattimore–Szepesvári develops Chernoff's tail bound in its information-theoretic form and the KL-UCB algorithm, whose upper confidence bounds are level sets of . The goal theorem shows KL-UCB attains
— asymptotic optimality with exactly the constant demanded by the lower bound of Mission VII, strictly improving subgaussian UCB on every Bernoulli instance.