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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. A high-probability approximation guarantee is a separate claim requiring an explicit probability bound. The optimum includes entangled states. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Many feasibility problems ask for a point satisfying several constraints at once. When each constraint set admits a manageable Euclidean projection, a parallel method can project onto all sets independently and combine the results. Chapter 5 of Boyd, Parikh, Chu, Peleato and Eckstein (2011) places this construction inside the alternating direction method of multipliers (ADMM). That connection matters when a single projection onto the intersection is difficult but projections onto its individual factors are available.
The chapter first rewrites constrained convex optimization as a split problem. It then treats feasibility for two sets and finally an arbitrary finite collection of sets. For the latter, the product of the sets captures the separate constraints, while a consensus set forces all copies of the variable to agree. These are ordinary finite dimensional convex sets, so the account applies to geometric feasibility and to constrained optimization subproblems in which projection is the computational primitive. The mission isolates the identities that let the product-space algorithm run through parallel individual projections and one average.
A Euclidean projection of a vector onto a set is a point closest to in Euclidean distance. Each set , for , is assumed nonempty, closed and convex, and . These properties give a unique projection for every input. They do not require the common intersection to be nonempty: the iteration and the algebraic identities still make sense when the feasibility problem has no solution.
A block vector belongs to the product set exactly when for all . The consensus set consists of constant block vectors . The block average is . Distances in the stacked space use the ordinary Euclidean metric, whose square is . A block vector need not carry a function-space norm in the formalization for this metric to be stated precisely.
Starting with arbitrary and , the parallel projection ADMM run has three updates: each is the projection of onto ; is the average of ; and . The are scaled dual variables, formed using a penalty parameter . The source presents these equations as the specialization of scaled ADMM for the indicator functions of and §5.1.2, pp. 35–36.
The first targets identify the projections that make the iteration parallel:
The goal is the full reduction of a run. Its dual average is zero after every update, and its common vector equals the primal average from the following update onward:
Consequently, for every and every , the same iterates obey the simpler two-line algorithm
If , those last identities hold already for . The index qualification is necessary because is arbitrary, and still contains the initial dual average unless that average was zero. This is the precise reading of the source's “after the first step” statement §5.1.2, p. 36. The milestone list also records the indicator-function projection update on p. 33 and the averaged identities on p. 36.
The result identifies what information must pass between the parallel projection steps: each local step needs the shared average and its own dual displacement. It also fixes the relationship between the displayed three-variable ADMM iteration and the shorter project-and-average rule. Without the dual-average identity, replacing by is not justified at the initial indices. The product and consensus projection identities explain why the update can be decomposed into independent local projections followed by a mean §5.1.2, p. 35.
The chapter's identities are known mathematical results; this mission asks for machine-checked proofs of their stated finite dimensional version. A completed development supplies reusable statements about nearest-point projection onto products and diagonal sets, and a precise run predicate for later analysis of parallel ADMM. The goal is a statement about every valid run rather than a claim of convergence or existence of a feasible common point. Neither convergence nor feasibility of the intersection is concluded on these pages. Those distinctions keep the mission aligned with the actual scope of Chapter 5.
The product projection uses a sum of squared component distances. Treating a block vector as an arbitrary function and applying its default norm would change the metric, so a projection theorem stated that way would describe a different algorithm. The consensus projection likewise depends on the Euclidean sum and the finite average, including the condition . The run reduction has a separate indexing difficulty: the vanishing average follows after one dual update, but the first simplified projection step can occur later because it uses the previous common vector. An argument that silently assumes would erase the arbitrary initialization on the source page.
Lean represents each as EuclideanSpace ℝ (Fin n) and the blocks as a function on Fin N; the latter is the source's -based indexing shifted to -based indices. Squared stacked distance is defined as the sum of squared component norms. The average uses the real factor only under . Individual projections reuse the published nearest-point relation RandomGradFree.Nonsmooth.IsMetricProjection. A run records the three updates as conditions on sequences, with arbitrary and unused . The source's scaled dual variable appears directly; cancels from these projection updates once it is positive.
The source assumes closed convex sets; nonemptiness is stated explicitly here because a projection onto an empty set does not exist. The book prints in its averaged dual update on p. 36, while its defining update on p. 35 and the next line on p. 36 require . The formal statement uses the corrected index. The book also calls the individual sets in its closing sentence; the sets defined for this subsection are . The milestone quote preserves the printed intermediate index. The goal includes the simplified primal and dual updates, since asserting only that the dual average vanishes would omit the chapter's advertised reduction.
The development needs finite sums in Euclidean spaces, convex-set projection, and elementary properties of product and diagonal sets. Product and consensus projection results are useful beyond ADMM. Contributions proving the four milestones, the full run theorem, or equivalent projection lemmas at the same generality are within scope.
In distributionally robust modelling, a baseline probability model on a space is distrusted, and the analyst reports the largest expected loss over every model within a budget of . Blanchet and Murthy (arXiv:1604.01446; Math. Oper. Res. 44(2), 2019, doi:10.1287/moor.2018.0936) measure the budget with an optimal transport cost and prove strong duality for the resulting worst-case expectation on an arbitrary Polish space, with a lower semicontinuous cost and an upper semicontinuous performance function. Duality computes the worst-case value. A risk manager also wants the worst-case model: a distribution that attains the value, whose structure explains which perturbation of is most harmful.
Such a model need not exist. Unlike the Kantorovich problem, where the set of couplings with two fixed marginals is weakly compact, the feasible set here fixes only one marginal and is not compact in general. Section 5 of the paper gives an example on where the supremum is not attained, then gives abstract conditions under which it is (Proposition 9), and growth conditions on a locally compact normed space that imply them (Corollary 1). Related existence results in were obtained by Gao and Kleywegt (arXiv:1604.02199, 2016) and, for empirical baselines and norm costs, by Mohajerin Esfahani and Kuhn (arXiv:1505.05116, 2018).
Let be a Polish space with its Borel -algebra, a probability measure on , a budget, a cost and a performance function. The standing assumptions are:
The primal feasible set consists of the probability measures on with first marginal and (transport plans out of of cost at most ). The primal objective is and the primal value is . The dual feasible set consists of pairs with , universally measurable and for all . The dual objective is and the dual value is . For put .
Section 5 assumes throughout that is a dual optimal pair with . Write for the plans in concentrated on .
(P-Compactness): for every there are a compact with and such that has compact closure. (P-USC): whenever converge weakly to .
On a normed space : (A3) for , with nondecreasing and . (A4) for an increasing with ; and for every , once .
Let be a real normed space that is locally compact, and let satisfy (A1)–(A4). Under the standing assumption, if there is with
The result. An attained worst case turns duality into a structural statement. By Theorem 1(b) of the paper, an optimizer moves mass from only to maximizers of and, when , uses the full budget. When those maximizers are unique (Remark 8: convex in , concave) the worst-case model is unique and is the image of under a transport map. That map is what stress tests and robust estimators are built from. Without existence, these statements describe an object that may not be there.
Formalizing it. The paper's proofs are complete; nothing here is open. No machine-checked version of this result is known: the worst-case optimal transport literature, including the strong duality of this paper, is unformalized. The mission produces the transport objects of §2 in a form that keeps the paper's generality (Polish space, lower semicontinuous real cost, universally measurable dual variables, the convention), a tightness argument for nearly optimal one-marginal plans, and an upper semicontinuity argument for unbounded upper semicontinuous integrands under uniform integrability.
The obvious argument takes a maximizing sequence and extracts a weak limit. Both steps fail without more structure. First, is not tight: only the first marginal is fixed, and a sequence may push mass to infinity at bounded cost. That is exactly what happens in Example 2 (p. 26), where and the value is approached but never reached. Tightness has to come from the dual: nearly optimal plans concentrate near maximizers of , and (A3)–(A4) with confine those maximizers. Second, is only upper semicontinuous and unbounded, so weak convergence alone does not give . A uniform integrability bound is needed, and it uses the restriction to in an essential way. A third, Lean-specific difficulty is measure-theoretic: is only universally measurable, and the gaps of Remark 4 are integrals against completions.
All declarations sit in the namespace ModelRiskOT.PrimalOpt. Values of , , , and are in EReal. is with lower integrals, and Mathlib's realises the paper's reading of the supremum (footnote 2, p. 5). Integrals of nonnegative or extended-real functions are lower integrals (lintegral), never Bochner integrals. Universal measurability is the published BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. Weak convergence is the topology of ProbabilityMeasure (S × S). Measures on use the product -algebra.
The following readings are fixed:
EReal convention.LocallyCompactSpace. It also carries PolishSpace, which is redundant, since a locally compact real normed space is finite-dimensional.The goal cannot be satisfied by a junk value: and are EReal suprema and infima, not real sSup, and the hypothesis is kept because Example 2 shows the conclusion fails without it. A sorry-free check that , on satisfy (A1), (A3) and (A4) accompanies the drafts.
A complete development needs Prokhorov's theorem (in Mathlib), a Fatou lemma for weakly converging measures with a lower semicontinuous integrand, an upper semicontinuity theorem for uniformly integrable upper semicontinuous integrands, and the change of variables for universally measurable . The last three are reusable well beyond this mission. Proofs of any milestone, and these general lemmas as separate contributions, are welcome.
A probability model for a risk quantity, such as the reserve process of an insurer or the path of a queue, is usually chosen for tractability or fitted to limited data, and the true law of the system is unknown. Distributional model risk asks how large a probability of interest could be if the true law were any model "close" to . When closeness is measured by an optimal transport cost rather than a likelihood ratio, the competing models may put mass where puts none, which is the situation for rare events such as ruin or buffer overflow: the event of interest often lies outside the support of the baseline.
Blanchet and Murthy (arXiv:1604.01446, Mathematics of Operations Research 44(2), 2019) prove strong duality for worst-case expectations over an optimal-transport ball on a general Polish space, with a lower semicontinuous cost. Their §2.4 specializes the duality to worst-case probabilities of a closed set and obtains a closed-form answer: the worst-case probability of is the baseline probability of an inflated version of . This mission formalizes that result, Theorem 3 of the paper, together with the numbered statements its proof uses.
Let be a Polish space with its Borel -algebra, its probability measures, and the baseline. A cost satisfies Assumption (A1): it is nonnegative, lower semicontinuous, and if and only if .
For , a coupling of and is a probability measure on with marginals and ; is the set of couplings, and the optimal transport cost is
For a budget , the primal feasible set consists of the probability measures on with first marginal and .
Fix a nonempty closed set and let be the cheapest cost of moving unit mass from into . The worst-case probability is
Its dual is the univariate problem
and for a minimizer of (13) the paper defines
If attains the infimum in (13) and , then
Theorem 3 converts a supremum over an infinite-dimensional ball of probability measures into a single probability under the baseline: of the set of points that can reach at cost at most , where is determined by through the one-dimensional function . For the cost of a metric this is the baseline probability of the -neighbourhood of . The paper uses it to compute worst-case ruin probabilities for the Cramér–Lundberg model around a Brownian approximation (§3, §6.1), where is a path space; the result applies there because nothing in it uses local compactness of .
The result is proved in the paper. As far as the platform's corpus shows, neither it nor the strong duality behind it has been formalized. A formal development produces, beyond Theorem 3: a reusable definition of optimal transport costs with lower semicontinuous costs on Polish spaces; the coupling reformulation of the transport ball, which rests on the existence of optimal transport plans (Villani, Optimal Transport, Theorem 4.1), not in Mathlib; and an -optimal-plan argument that avoids assuming a primal optimizer exists.
The heuristic derivation on pp. 9–10 constructs an optimal transport plan that moves each with to a nearest point of and leaves the others in place. It needs a nearest point to exist and to be selectable measurably, which fails for general closed in a non-locally-compact space, and it needs a primal optimizer, which need not exist. Theorem 3 assumes neither, so the construction is not a proof. A second point is the boundary level : when charges it, as for atomic baselines, the identity (15) can fail (for a point mass at distance from and , the worst case is , not ), and the hypothesis is exactly what excludes this. Measurability is a second obstacle: is an infimum of a lower semicontinuous function over and in general only universally measurable, so integrals of it are taken against the completion of .
All objects live in the namespace ModelRiskOT.WorstProb. carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]; is a Measure S with IsProbabilityMeasure; the cost is a real-valued c : S → S → ℝ with (A1) bundled as a structure (nonnegativity, lower semicontinuity on , and ). Committed conventions:
ℝ≥0∞; integrals are lower Lebesgue integrals and the positive part is ENNReal.ofReal. For the universally measurable functions and sets that occur, lower integrals and outer measures agree with the completion of , which is the paper's reading (p. 4). No Bochner integral is used.A formalization in which the transport ball fixes only the first marginal would contain every probability measure and give for every nonempty ; the definitions here fix both marginals of the couplings in , and the hypothesis is kept as stated rather than replaced by continuity of .
A complete development needs the existence of optimal couplings for lower semicontinuous costs (tightness and Prokhorov's theorem, available in Mathlib), the strong duality of the paper's Theorem 1 specialized to indicators (milestone 3; a separate mission in this series formalizes Theorem 1 in general), and universal measurability of through projections of Borel sets. The transport-cost definitions and the coupling reformulation are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs that derive (13) from the general strong duality once that is published.
In classical single-machine stochastic scheduling, jobs with independent random processing requirements are processed one after another, and the makespan (the completion time of the last job) is the same for every schedule that never idles: it is . Research therefore concentrated on weighted flow times and rewards. Browne and Yechiali (Operations Research 38(3), 1990, 495–498) studied jobs that deteriorate while they wait: the longer a job is delayed, the more processing it needs. Such models arose in the control of queueing and communication systems (Browne 1988; Browne and Yechiali 1989) and in inventory issuing, where stored items lose quality at item-specific rates. Under deterioration the actual processing times depend on the order, so the makespan, and its expectation, become functions of the schedule, and the basic question is which order minimizes the expected makespan.
There are jobs, all available at time , and a single processor. Job has an initial processing requirement , a random variable on a probability space : the time needed to complete job if it is processed first. Under linear deterioration, a job whose processing is delayed until time needs
where is its deterministic growth rate. A job stops deteriorating once it is put on the processor.
Only nonpreemptive strategies without idling are allowed, so a policy is a permutation of , with meaning that job is the -th processed. The completion times follow the model: , and the job in position starts at and takes , so
The makespan is and the expected makespan is . In Lean these are completionTime X α π k ω, makespan X α π ω and expectedMakespan P X α π in the namespace DeterioratingJobs.Makespan.
The paper's Lemma 1 concerns, for real numbers and , the sum (1)
the Lean lemma1Sum μ γ π (empty product ).
If the are integrable, , and schedules the jobs by increasing values of , then
The result is an index rule: each job receives a number computed from its own data, , and sorting by that number is optimal. It needs only the means of the initial requirements, not their distributions, and it holds without independence. The same reduction to Lemma 1 gives the paper's other index rules: the variance of the makespan under independent requirements, the Poisson-shock model (5), Lévy-type growth (6) and setup/detach times (7). In inventory issuing, it says which stored item to issue first when items lose value at item-specific linear rates. Lemma 1 itself, which the paper attributes to Rau (1971) and relates to optimal search, is a general statement about ordering products of factors along a sequence.
The result is proved in the paper by an appeal to Lemma 1, whose proof is given there as one sentence ("direct upon an interchange argument"). None of these statements has a machine-checked proof on Prove2Me or in Mathlib. This mission produces a formal model of linear deterioration on a single machine, a formal proof of the interchange lemma with ties handled, and the formal index rule.
The algebra of one adjacent interchange is short. The work is in passing from that local comparison to optimality over all permutations, with ties allowed: the paper speaks of "the permutation ordered by increasing values", but with equal indices several permutations qualify, and each of them must be shown optimal. The natural route, "an optimal permutation exists and must be sorted", needs care, because a sorted permutation is not unique and the swap that improves an unsorted permutation may only weakly improve it. On the probabilistic side, the expectation of the makespan must be reduced to the expectations of the ; the makespan is a polynomial in the with deterministic coefficients, so this is linearity of the integral, but integrability has to be carried through the recursion.
Fin N (0-based: Lean job i is the paper's job ); a policy is π : Equiv.Perm (Fin N) with π k the job in position k, as in the paper's . is allowed.(Ω, P) with [IsProbabilityMeasure P]; is Ω → ℝ; expectations are Bochner integrals, and every theorem about them assumes each integrable. The growth rates are deterministic reals.Monotone), and "decreasing" means Antitone; "is minimized" means against every permutation; "expected" means the integral of an integrable random variable.PalmQueueing.Ordering.interchange_permutations (interchange permutations of a GI/GI/1 queue) and the additive, non-deteriorating completion-time models MooreLateJobs.Shared.completionTime and NumStochOpt.ListScheduling.Makespan.Contributions welcome: proofs of the milestones, a reusable "sorted permutation minimizes a sum of products" lemma, and the variance index (3) as an extension.
The alternating direction method of multipliers (ADMM) is one of the most widely used algorithms for large-scale convex optimization in statistics, machine learning and signal processing. Its appeal is decomposition: a problem whose objective splits into two parts, coupled only by a linear constraint, is solved by alternately minimizing over each part and updating a dual variable. Each subproblem is often a proximity operator, a projection or a small linear system, so ADMM turns problems such as the lasso, sparse inverse covariance selection and consensus fitting across many machines into sequences of simple steps. The survey of Boyd, Parikh, Chu, Peleato and Eckstein (DOI 10.1561/2200000016) made the method standard, and every algorithm in its later chapters is justified by one convergence result, stated in §3.2.1 and proved in Appendix A. This mission formalizes that result and the inequalities behind it.
The method goes back to Gabay and Mercier (1976). Eckstein and Bertsekas (1992) proved convergence through the theory of maximal monotone operators, by identifying ADMM with Douglas–Rachford splitting applied to the dual problem. The proof in Appendix A of the survey is different: it is a direct Lyapunov argument in finite dimensions that uses only convexity and elementary algebra.
Let and , let , and . The problem is
with optimal value . The augmented Lagrangian with parameter is
and is the ordinary Lagrangian. For , ADMM generates iterates by
The state is ; plays no role. The primal residual is , the dual residual is , and .
Two assumptions are made. Assumption 1: and are closed, proper and convex. Assumption 2: has a saddle point , i.e. for all . Nothing is assumed about the ranks of and . The convergence proof uses the Lyapunov function
Under Assumptions 1 and 2 and for , every ADMM run satisfies
The statement fixes no rate and no constant. It does not claim convergence of or , which fails in general (p. 17).
In the order of Appendix A:
The theorem is what licenses every specialized ADMM of the survey (lasso, basis pursuit, covariance selection, consensus and sharing, distributed model fitting): each of these chapters only computes the subproblem solutions, and correctness of the overall method is inherited from §3.2.1. Inequality (3.11) and its corollary in §3.3.1 justify the primal/dual residual stopping criterion (3.12) used in practice: small residuals certify small suboptimality.
The result itself is classical and proved; it is not open. To our knowledge no machine-checked proof of convex two-block ADMM convergence exists in Lean's Mathlib. Formalizing it produces a reusable development of the augmented Lagrangian method with explicit domain handling for extended-valued convex functions, and checks a proof whose index bookkeeping the printed text leaves loose (the monotonicity step and (A.1) need , see below).
The obvious argument, "the subproblem optimality conditions plus the saddle point give a decreasing quantity", works only once the right Lyapunov function is found and the cross term is controlled. That term has no sign from the optimality conditions of a single iteration, and at the first iteration, where is an arbitrary starting point, the decrease (A.1) can genuinely fail. A second obstacle is that and need not converge or even be bounded when or is rank deficient, so objective convergence cannot pass through limits of the primal iterates; it has to come from the two-sided bounds (A.2) and (A.3). Finally, the subdifferential sum rule used to linearize each subproblem must be handled for functions taking the value .
EuclideanSpace ℝ (Fin n); matrices act through Matrix.toEuclideanLin; the problem data are bundled in a structure Problem n m p.ShorNonsmooth.Subdiff.subdifferential relative to the domain.A complete development needs the subdifferential of a convex function plus a differentiable quadratic, the first-order characterization of a constrained minimizer, and elementary limits; all of this is reusable for the later missions of the series, which take ADMM runs as given. Proofs of individual milestones are welcome independently.
Two-stage optimization separates a decision made before uncertainty is observed from one made after a scenario is known. A fully adaptive policy can choose a different second-stage decision in each scenario, while a static robust solution commits to a single second-stage decision that works in every scenario. Static solutions can be simpler to implement, but their worst-case cost may be higher. Bertsimas and Goyal ask how large this cost difference can be when both the right-hand sides of the constraints and the second-stage prices vary. Their Theorem 5.1 gives a factor of four when the paired uncertainty set is symmetric and nonnegative, even when both stages contain integer variables.
The distinction matters in planning problems where one policy is fixed in advance and another could respond to realized demand or prices. A uniform bound lets a planner assess the cost of the static restriction without solving every adaptive policy exactly. The source is the authors' manuscript; all page and result numbers in this mission refer to that manuscript, not to the journal pagination.
Fix matrices and . A scenario supplies a right-hand side and a second-stage cost vector . The first-stage cost vector is . For a set of designated integer coordinates, write for the nonnegative real vectors whose coordinates in are integers. After relabelling, this is the paper's .
In the robust problem , one first-stage decision and one second-stage decision must satisfy for every scenario. Their cost is . In the adaptive problem , is still chosen once, but may depend on the scenario. Its constraints are for every , and its cost is . The optimal values and are infima over feasible decisions in these respective problems; these are models (1.5)–(1.6).
The paired uncertainty set is . It is symmetric when it contains a point such that belongs to the set exactly when does, for every displacement . The point is itself a scenario realization. The smallest coordinatewise bounding hypercube has lower and upper corners and ; its center is . These are Definition 1.2 and displays (2.5)–(2.7).
The goal is Theorem 5.1:
The factor applies to every nonnegative symmetric paired uncertainty set and to both continuous and mixed-integer decisions. The theorem does not require an optimal adaptive policy to attain its infimum. The milestones record the source's geometric Lemma 2.3 and the estimates labelled (5.1)–(5.4), which supply the center-scenario cost and feasibility statements with the explicit factor four. They are stated for arbitrary feasible adaptive policies so the conclusion also covers nonattained infima.
The result bounds the price of committing to a single second-stage decision, despite uncertainty in both the constraints and the objective. In this setting the comparison is independent of the number of scenarios and of the dimensions . The paper also considers right-hand-side-only uncertainty, positive sets, and hypercubes; this mission isolates its symmetric paired-uncertainty result §5.1.
The theorem is proved in the paper. The remaining formalization work is a machine-checked development of the model, the bounding-hypercube geometry, the cost inequalities, and the passage from arbitrary feasible policies to the optimal values. The resulting definitions of mixed-integer domains, robust and adaptive feasibility, and extended-real optimal values can also support the other results in this paper's mission series. The theorem statements here are open proof targets, with no machine-checked proofs claimed.
The worst-case maximizer of can vary with , and an adaptive policy can choose a different integer vector in every scenario. Selecting one of those vectors as a static decision therefore gives no immediate cost or feasibility guarantee. The point of symmetry is a realizable scenario, but it must control both components of every other paired scenario. Without nonnegative data, doubling the center-scenario decision may fail to cover a positive right-hand side, and the cost comparison can fail as well. Integer coordinates also constrain which scalings preserve the decision domain; the exact factor in the theorem is compatible with doubling, unlike arbitrary fractional rescalings.
Vectors are real functions on finite index types, matrices use Mathlib's matrix-vector product, and inequalities are componentwise. The scenario set is the range of , with a product-space symmetry predicate. No probability measure or measurability structure is used in these worst-case problems. Both stages may have integer coordinates designated by sets ; no continuous-only second-stage restriction is imposed.
Optimal values and worst-case costs use extended real numbers. An infeasible problem has value ; a real infimum over an empty feasible set would incorrectly return a default zero. Symmetry includes a center belonging to the scenario range, so the scenario set is nonempty. Combined with nonnegative coordinates, symmetry bounds every scenario coordinate and makes the bounding-hypercube endpoints meaningful. The hypotheses retain , , and , which the source uses in its factor-four estimate. A statement restricted to continuous recourse, an assumed optimal adaptive policy, or a zero-valued infeasible problem would not express this target.
The source prints in (1.5)–(1.6), although the model's second-stage integer count is ; the domain here follows the surrounding convention. Lemma 2.3 is stated here for nonnegative sets, the regime needed for its second inequality. Its coordinatewise suprema and infima agree with the printed maxima and minima in this bounded symmetric setting. Contributions to the shared domain and geometry lemmas, the mixed-integer scaling fact, and the optimal-value comparison are all useful to the goal.
Many operations problems are decided in two stages: a first-stage decision is fixed before an uncertain quantity is revealed, and a second-stage (recourse) decision is chosen afterwards. Two classical ways to optimize such a problem differ in how they treat the uncertainty. Two-stage stochastic optimization minimizes the expected cost under a probability distribution over scenarios, with a recourse decision adapted to each scenario. Robust optimization fixes a single solution that must be feasible for every scenario in an uncertainty set, and minimizes the worst-case cost. The robust problem is usually far easier to solve, but it is conservative; the question is how much it can lose.
Bertsimas and Goyal (Math. Oper. Res. 35(2), 2010) answer this for uncertain right-hand sides. Their main positive result (Theorem 2.1) bounds the stochasticity gap: if the uncertainty set and the probability measure are both symmetric, the robust optimum is at most twice the stochastic optimum. This mission formalizes the companion negative result, Theorem 2.6: once the uncertainty set is not symmetric, the gap is not bounded by any constant. The example is the simplest non-symmetric set in practice, the corner of the unit simplex, with the uniform distribution on it. It shows that the symmetry hypothesis in the positive result is not an artefact of the proof.
Fix matrices , and costs , . Let be a set of scenarios, the right-hand side realized in each scenario, and the uncertainty set. Let be a probability measure on .
In general some coordinates of and are required to be integers; in this mission's instance there are none. A set is symmetric (Definition 1.2) if some satisfies for every .
The instance of Theorem 2.6 has no first stage (, so , ), , , and . The uncertainty set is the corner simplex (2.29)
and is the uniform probability measure on it: .
On this instance,
The constant is the paper's, and it is exact: the robust optimum is and the stochastic optimum is at most .
The result. Together with Theorem 2.1, Theorem 2.6 locates the boundary of the paper's positive theory. Theorem 2.1 says a static robust solution loses at most a factor of against the fully adaptive stochastic optimum under symmetry; Theorem 2.6 says that without symmetry the factor can be , hence arbitrarily large as the dimension grows. The paper's later results (the bound for "positive" uncertainty sets, Theorem 2.7) are motivated by this example: some structural condition replacing symmetry is necessary. The same instance also separates the adaptive problem from the stochastic one (p. 21), which shows that the gap comes from comparing a worst case with an expectation, not from the lack of adaptivity.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The formalization adds two things beyond the paper. First, it pins down the problems as optimization problems over integrable policies with values in the extended reals, so that the inequality cannot hold for a degenerate reason. Second, it requires the volume of the corner simplex and the first moment of a coordinate on it, which the paper calls "standard computation". Neither is in Mathlib at the time of writing: Mathlib has the standard simplex as a convex set but no volume formula for it.
The optimization part is short: one feasible stochastic policy and the vertices of the simplex give both bounds. The work is in the measure theory. The volume and the moment are iterated integrals with variable upper limits, and the paper calls them "standard computation"; as statements about Lebesgue measure on they are dimension-dependent identities that Mathlib does not contain, for the simplex or for the convex hull of points. The other technical point is the scenario model: the uniform measure lives on , while the integrals live on , so the expectation must be moved through the push-forward of by .
Fin k → ℝ with the componentwise order; products are A *ᵥ x and c ⬝ᵥ x. The paper's -th coordinate is index of Fin n, and is lastUnit n.EReal infima over the feasible set, equal to when the problem is infeasible. No optimal solution is assumed to exist.Needed infrastructure: the volume of the corner simplex in and the integral of a coordinate over it (reusable well beyond this mission, for example for Dirichlet distributions and order statistics), and the change of variables from to through the push-forward. Contributions of either simplex integral, in any form that implies the stated milestones, are welcome.
This completed entry lowers the sufficient exponent cutoff for the sharp diagonal Hlawka formula from 90 to 87. The goal is already proved in Lean on Prove2Me: for every real p ≥ 87, the foundation's cyclic constant K_p is the least constant that works for every triple of complex coordinate vectors in every finite dimension.
The statement includes arbitrary unequal-norm and zero triples, as well as dimension zero. It uses the foundation's unchanged definitions and combines admissibility with uniform optimality. This concerns complex diagonal matrices; it does not claim the corresponding result for general matrices or settle the conjecture for all p ≥ 2.
The campaign template is instantiated with value 87. Both items reference the existing accepted theorems.
The proof extends the accepted cutoff-90 Lean development by BrunoDCDO, adapting Ezzeri Esa's construction and analytic argument. The contributions at cutoffs 89, 88 and 87 were submitted by moona3k.
For p ≥ 88, the proof uses the accepted cutoff-88 result. On 87 ≤ p ≤ 88, it retains the localization, box-convexity and cyclic-averaging argument, with confinement parameter q₀ = 5351/15000, an improved cyclic witness (3/(4p))^(1/p), sharper Taylor estimates and exact rational polynomial certificates.
The foundation established cutoff 256; the supplied argument was formalized at cutoff 90. The subsequent accepted results extend the same formula to cutoffs 89, 88 and 87. This entry records the proved cutoff 87 on the campaign timeline; the campaign's cutoff-85 mission remains open.
The Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the accepted cutoff-87 theorem already covers every , the new work is the range from 85 to 87.
The cutoff came down from 90 to 87 in a day, through moona3k's proofs at 89, 88 and 87. The 89 proof reran the cutoff-90 argument with sharper, second-order estimates. A numerical model of that argument with retuned constants puts its limit between about 86.6 and 87.5: two of its steps pull the same parameter in opposite directions, and below that point no setting satisfies both. So reaching 85 is expected to need a new idea, not just tighter numbers. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 85 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryAssortment optimization asks a retailer which products to offer when customers substitute among them. The nested logit model groups products into nests and is one of the most used choice models in revenue management, because it relaxes the independence of irrelevant alternatives of the plain multinomial logit model while keeping choice probabilities in closed form. Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) study how the tractability of the assortment problem under this model depends on two features: whether the dissimilarity parameters of the nests are at most one, and whether a customer who selects a nest always buys there (fully-captured nests).
When the dissimilarity parameters are at most one and the nests are fully captured, offering the highest-revenue products in every nest is optimal (Theorem 4 of the paper). This mission concerns what survives when a dissimilarity parameter exceeds one, the regime the paper calls possibly synergistic products. Then the problem is NP-hard (Theorem 5), and the paper shows that the same nested-by-revenue assortments still achieve an explicit, data-dependent fraction of the optimal expected revenue.
There are nests and products in every nest. Product of nest has a revenue and a preference weight , ordered so that . Nest has a dissimilarity parameter , and is the weight of leaving without choosing a nest. Throughout this mission the nests are fully captured: the within-nest no-purchase weights are zero. For an assortment in nest ,
and the expected revenue of is
Problem (2) maximizes ; its optimal value is . The nested-by-revenue assortment collects the highest-revenue products of nest , with and .
Problem (2) is equivalent to the linear program (3): minimize subject to and for every nest and every . Problem (4) keeps the second family of constraints only for candidate assortments; here the candidates are , which gives a linear program with variables and constraints. The performance factor of the nested-by-revenue assortments is
Assume for every nest, for some nest, positive revenues and . If is an optimal solution of (4) over the nested-by-revenue assortments, then
Combined with Theorem 1 of the paper this yields for the assortment read off the small linear program; that consequence is a companion item.
Two companion statements follow the goal: the bounds and when revenues, respectively preference weights, within each nest differ by at most the factors , ; and the guarantee .
Because problem (2) is NP-hard once a dissimilarity parameter exceeds one (Theorem 5 of the paper), an exact polynomial algorithm is not expected, and a guarantee for a polynomial-size candidate family is the natural substitute. Theorem 7 gives one with an explicit factor computed from the data: when revenues within each nest are balanced, when preference weights within each nest are balanced, and the nests may differ arbitrarily from one another. The same linear-programming argument (Theorem 1) is reused for partially-captured nests in §6 of the paper.
The result is proved in the paper (Appendix A.1); no machine-checked version is known. A formalization verifies an appendix argument that is stated with little detail, and fixes the conventions that the page leaves implicit, such as the value of the objective of (8) at and the role of the standing assumption that some exceeds one.
Theorem 7 is a feasibility statement for the exponentially many constraints of (3), one per subset of every nest, while optimality of only controls the nested-by-revenue constraints per nest. The obvious approach, comparing each subset directly with a nested-by-revenue assortment, fails: when the nested-by-revenue assortments are not optimal within a nest, and the example of §4.1 shows that they can lose an unbounded factor. The constant must absorb the gap between a fractional assortment and its two neighbouring nested-by-revenue assortments, which the dual-style solution of the small program does not see.
Lean 4 with Mathlib. Nests form a finite type ι; products are Fin n, indexed from , so is nbr n j = {k | k < j} and product of the page is ⟨k - 1, _⟩. Powers are real powers (Real.rpow), and division is total (), which gives and value for the objective of (8) at .
Standing assumptions in every statement: , , , , , revenues ordered within each nest (§1); for every nest and for some nest (§4, p. 16). Added and disclosed: wherever (6) appears, so that no denominator of (6) vanishes; , the nonempty range of (6); only in the guarantee , inherited from Theorem 1. The factor enters as a real number with the hypothesis that it is the greatest element of the set of terms of (6). An optimal solution of (4) is a feasible pair whose is minimal among feasible pairs.
A trivializing formalization is ruled out: is the maximum of (6), not an arbitrary upper bound, and the goal states feasibility for the full program (3) over every subset of every nest, not for (7) or for the candidate collection.
Needed infrastructure: maximization of a continuous function on , the greedy solution of a continuous knapsack, monotonicity of weighted averages and elementary real-power calculus. These are reusable beyond this mission. Proofs of any milestone, of the companions, and of the §4.1 example are welcome.
A portfolio manager who maximizes expected utility needs the distribution of asset returns, but in practice only estimates of its first two moments are available, and these estimates are themselves noisy. Distributionally robust optimization handles this by optimizing against the worst distribution in a set of plausible ones. Delage and Ye (Operations Research 58(3), 2010) proposed a set of distributions defined by confidence bounds on the mean and on the second-moment matrix, showed that the resulting problems are solvable in polynomial time for a large class of costs, and applied the framework to portfolio selection.
The set contains an upper bound on the covariance but no lower bound. Remark 1 of the paper says a lower bound "leads to important computational difficulties" and argues it should be unnecessary: for a concave utility, a less predictable market can only reduce expected utility, so the worst distribution should already have the largest covariance allowed. Proposition 3 in §5.2 turns this argument into a theorem for piecewise-linear concave utilities and unconstrained support. This mission formalizes Proposition 3 and the steps of its proof.
Let assets have a random return vector , and let be a portfolio, so the return is . A distribution of is a Borel probability measure on with finite second moments. For symmetric matrices, (the Loewner order) means is positive semidefinite.
Given a support set , a centre , a positive definite matrix and , , the distributional set of Assumption 3 is
The second constraint, (1b), is the covariance constraint.
The utility is piecewise linear concave, with pieces, and the cost of a return is :
With estimates , of the mean and covariance, the inner problem of the robust portfolio problem with unconstrained support and an exactly known mean () is
The proof relates (18) to a semidefinite program in variables , , :
For every (the mean-uncertainty radius of the robust portfolio problem (16); (18) is the case ),
The worst-case expectation is attained, and at a distribution for which the covariance constraint holds with equality. The statement holds for every portfolio , every , every , every , every , every and every .
The proposition justifies a modelling decision of the whole paper: for portfolio problems with piecewise-linear concave utility, adding a lower bound (display (2)) to the distributional set cannot change the robust decision, so the computational difficulty that lower bound would cause is avoided at no loss. It also shows that, under these assumptions and with , the paper's semidefinite formulation solves the known-moment portfolio problem of Popescu (2007) in polynomial time (Remark 4). The worst case is explicit: a finite mixture of distributions with prescribed first and second moments, read off an optimal solution of (19).
The result is proved in the paper; no machine-checked version is known. Formalizing it requires a moment-problem argument (from a distribution to a feasible point of an SDP) and its converse (from an SDP solution to a distribution), both of which are reusable for other moment-based distributionally robust results. The proposition concerns the robust portfolio problem with ; the paper's proof writes out only "for simplicity of our derivations". The goal states the proposition for every ; the milestones follow the written proof and are stated for .
The obvious argument, "a concave utility prefers less spread, so the adversary maximizes spread", does not prove anything by itself: increasing the second-moment matrix of a given distribution in the Loewner order does not determine its law, and the expected cost depends on the whole law, not on the moments. The proof goes through the semidefinite program (19). Two steps carry the weight. First, every distribution in must be mapped to a feasible point of (19) with no smaller value, although the cost is only piecewise affine in . Second, an optimal point of (19) must be turned back into a distribution in ; this needs the existence of random vectors with prescribed first and second moments, and care with blocks where , which the paper sets aside "without loss of generality" although such a block can carry a nonzero that the mixture would lose.
Fin n → ℝ; all Euclidean quantities are dot products, never the sup norm. Matrices are Matrix (Fin n) (Fin n) ℝ; is (B - A).PosSemidef; is Mathlib's matrix inverse, used only with .Measure (Fin n → ℝ) that is a probability measure and whose coordinates are in (MemLp _ 2). This makes every mean, second moment and expected cost a genuine integral; without it a non-integrable expectation would evaluate to .[NeZero K]).The source is the authors' draft of 20 February 2008 of the Operations Research paper; every page, display and label in this mission refers to that draft.
Markovian decision processes with the long-run average cost criterion model systems run indefinitely: inventories, queues, maintenance schedules, communication links. For a finite state space the theory was settled by the early 1960s. Howard's policy improvement (policy iteration) procedure (1960) finds an optimal stationary rule in finitely many steps, and Gillette (1957) and Derman (1962) showed that a stationary deterministic rule is optimal over all rules, history-dependent and randomized included (Derman 1962).
Many models of interest, such as queues with unbounded buffers and inventories with unbounded backlog, have a denumerable state space, and there the finite theory breaks down. Derman's paper (Ann. Math. Statist. 37 (1966) 1545–1553) gives two counterexamples in §2, both under bounded costs and finitely many decisions per state. In the first, due to Maitra, no optimal rule exists. In the second, a randomized stationary rule beats every deterministic one. It then gives sufficient conditions under which a stationary deterministic optimal rule exists and policy improvement finds it.
Timeline:
The system is observed at times in a state of a denumerable set . At state one of decisions is made (condition (A)). It costs , and the next state is with probability . The costs are bounded (condition (B)) and may have either sign. A rule chooses the decision at each time with probabilities that may depend on the whole history. The class of all rules is , and is the class of stationary deterministic rules ("make decision at state "). The average cost of from is
A rule is optimal over if for every and every .
The optimality equation (1) asks for a number and a bounded with
and equation (2) is its version for one rule , with in place of the minimum. Condition (C): every induces an irreducible Markov chain all of whose states are positive recurrent. Condition (E): every has a solution of (2), bounded uniformly in and . Condition (F): for every the Cesàro limits of satisfy . One policy improvement iteration replaces by a rule whose decisions minimize at every state.
Under (A), (B), (C), (E) and (F), let be any sequence of policy improvement iterations from an arbitrary . Then the sequence has a limit point , and every limit point satisfies
with .
Theorem 1 is the countable-state verification theorem. It is the template for all later average-cost theory on infinite state spaces, which replaces boundedness of by growth or Lyapunov conditions. Theorem 4 extends policy improvement, the standard algorithm for finite average-cost problems, to denumerable state spaces, under conditions that do not reduce the problem to a finite one.
Derman proved these results in 1966. None of them has been machine-checked: the platform has finite-state average-cost policy iteration and finite-state verification theorems, but no countable-state result of this kind. A formal development checks the analytic steps that the paper treats briefly. These are the interchange of limits and infinite sums in (3), (9) and (11), and the identification of the Cesàro limits of a positive recurrent chain with its steady-state probabilities.
On a finite state space, policy improvement terminates because there are finitely many rules and the average cost strictly decreases. On a denumerable state space is uncountable, so neither step works. The sequence need not terminate. With ties in the minimization it need not converge either. A strict decrease of does not force the gaps to vanish. That needs (F), a uniform positive lower bound on the long-run occupation of each state. Passing to the limit in (2) along a subsequence requires a limit interchange in an infinite sum, which works only because is uniformly bounded. Finally, comparing with history-dependent randomized rules needs the finite-horizon argument behind (6). A stationary-rule comparison is not enough.
The model is the published Markov decision chain SennottDP.AvgFinite.MDC: a countable state type, a finite nonempty Finset of decisions at each state (so (A) is built in), and transition probabilities in summing to one. History-dependent randomized rules are Policy M, and is StationaryPolicy M. The chain notions (irreducibility, positive recurrence, steady state ) come from the published SennottDP.MarkovCost.Chain. The conventions are as follows.
w with (B). The nonnegative cost field of MDC is unused, and is not assumed.limsup with the paper's normalization .Two trivializing formalizations are ruled out: optimality is over all history-dependent randomized rules, never only over , and is computed from the process law, never defined through (2).
A complete development needs Cesàro convergence of -step probabilities to for positive recurrent chains, dominated convergence for bounded functions against stochastic kernels, the finite-horizon dynamic programming principle for history-dependent rules, and a diagonal (Tychonoff) argument in . The first and third are reusable well beyond this paper. Contributions of these lemmas as separate theorems are welcome.
Graham (1966) showed that list scheduling finds a schedule within a factor of optimal for precedence-constrained jobs on identical parallel machines, the first performance guarantee for an approximation algorithm. When the machines run at different speeds (uniformly related machines), the same analysis breaks down, and for two decades the problem resisted a guarantee independent of the speeds better than .
Timeline:
The mission formalizes the makespan half of that paper, up to its Theorem 3.7.
An instance has jobs and machines. Job requires units of processing, and machine runs at speed , so job takes time units on machine . A strict partial order on the jobs gives precedence constraints: means that job may not start until job has completed.
A schedule runs each job without interruption on one machine , from a start time to its completion time . A machine processes at most one job at a time, and forces . Its length is . is the length of an optimal schedule.
Let be the distinct speeds and the number of machines of speed . An assignment names the speed class at which job is to run. Its loads are , and its chain bound is the largest value of over chains of . Speed-based list scheduling is Graham's rule restricted by the assignment: whenever a machine of speed is idle, it starts the first available job on the list with .
The linear program LP has variables , and . It minimizes subject to the following constraints:
From a solution, with , the assignment algorithm gives each job the speed class of largest capacity .
There is an absolute constant such that for every instance with machines and distinct speeds, the better of the two schedules below has length at most
The result gives the first guarantee for , independent of the speeds, and a guarantee depending only on the number of distinct speeds. Through the batching technique of Shmoys, Wein and Williamson it extends to release dates (Corollary 3.8). Since LP also relaxes the preemptive problem, it gives an bound on the ratio between the nonpreemptive and preemptive optima (Corollaries 3.9, 3.10). The "In fact" form, relative to an arbitrary feasible LP solution, drives the paper's algorithm in §4.
The result is proved in the literature but, as far as is known, not formalized. A formal proof requires machine-checking the following:
Later work gave a combinatorial -approximation (Chekuri and Bender, 2001) and an -approximation (Li, 2017). These are not part of this mission.
Graham's argument has two lower bounds:
With different speeds, the first bound fails: a chain may have been run on slow machines, and its length then says nothing about . Forcing every job onto a fast machine repairs chains but can leave most machines idle, so the second bound fails. The paper only guarantees that all machines of one speed are busy at each moment of an idle period. Making this pay off requires an assignment that controls chain lengths and per-class loads simultaneously. That assignment is the delicate part: Theorem 2.1 is the bookkeeping, while Lemmas 3.2 and 3.4 rely on the LP. Two of the formal steps are routine on paper but fiddly in Lean: time-interval accounting over a continuous-time schedule, and the counting of rounded speed classes.
Fin n and machines Fin m with . and . is a strict partial order, and a chain is a finite set of pairwise comparable jobs. is the maximum completion time, or with no jobs.Proofs of any milestone are welcome. Reusable beyond this mission are the following: the model of nonpreemptive schedules on uniformly related machines with precedence, the speed-based list-scheduling predicate with Theorem 2.1, and the LP.
Fashion and consumer-electronics retailers sell a product at full price early in a season and mark down what is left. Consumers learn the pattern, and some of them wait for the markdown. Such strategic consumers lower the revenue of the full-price period, and the retailer's stocking decision affects how deep the markdown is expected to be. Quick response — a second, more expensive replenishment placed after demand is observed — is usually valued as a way to match supply with exogenous demand (Fisher and Raman 1996; Cachon and Terwiesch, Matching Supply with Demand, 2005). Cachon and Swinney ask how strategic waiting changes that value.
The source is the authors' working paper of April 2007, revised November 25, 2007, not the 2009 Management Science version, whose numbering and wording may differ. Its answer: with strategic consumers the retailer stocks less (Theorem 1), and under an explicit cost condition, quick response is worth more to a retailer facing strategic consumers than to one facing only myopic consumers (Theorem 3).
A retailer sells over two periods. It sells at the exogenous full price in period 1 and at a markdown price chosen at the start of period 2. Leftover units are worth . First-period demand has density and distribution function , and satisfies the monotone scaled likelihood ratio (MSLR) property: for every , is monotonic on the support of .
The market has three segments:
The standing assumptions are and . Let be the fraction of strategic values above .
By a threshold argument (Lemma 1), strategic consumers with value below some buy at and the rest wait. A fraction of demand then buys in period 1, and the inventory left for period 2 is . The period-2 revenue counts the waiting strategic consumers with value at least and, if , the bargain hunters, up to the inventory . The retailer's expected profit at unit cost is
With quick response, units ordered before the season cost and units ordered after observing cost , with . The second order covers all first-period demand and may add stock for the sale. The resulting profit is .
In the sale period, waiting strategic consumers are rationed: they effectively face the inventory , where measures their place in the queue. A strategic consumer with value who waits gains, in expectation,
where is the demand level below which the retailer clears stock at . A rational expectations equilibrium is a pair in which maximizes and is a best response of consumers who correctly expect . The superscript denotes the benchmark with only myopic consumers (): and are the optimal myopic profits without and with quick response.
Assume MSLR and no rationing, , , , and condition (6):
Let be any equilibrium without quick response, any equilibrium with it, and , the myopic optima. Then
The milestones follow the paper's path:
Corollary 1 is the percentage form, .
Theorem 3 identifies a second channel through which quick response creates value. Beyond matching supply to demand, it lets the retailer keep its initial stock low enough that a deep markdown becomes unlikely, so strategic consumers buy at full price. Under (6), all of them do. Quick response thus reduces strategic waiting without withholding availability, unlike the inventory-signalling remedies in the literature, and the theorem quantifies when this effect dominates.
The results are proved in the working paper, partly in a technical appendix. No machine-checked version of them, or of the underlying markdown game, is known. A formalization pins down several statements that the paper states loosely:
It also produces reusable components: the newsvendor with salvage and the reactive-capacity fractile under a general density, and a rational-expectations equilibrium predicate for a retailer–consumer game.
The profit is not concave: with strategic consumers it is concave–convex (Figure 4 of the paper). The newsvendor argument therefore does not give a unique optimal order, and Lemma 3's quasi-concavity rests on MSLR in a short appendix step.
Existence (Theorem 1) needs a fixed point of the map best response, but the consumer best response is a correspondence, not a function, so the printed intermediate-value argument does not apply directly. Theorem 3 needs a statement about every equilibrium with quick response, while Theorem 2's proof only exhibits one. Ruling out an equilibrium with requires comparing the derivative (4) of with the myopic derivative along the whole demand distribution.
Lean represents prices, quantities and valuations as reals, demand by a density on , and expectations as Lebesgue integrals against . The model carries the standing assumptions of §3 as fields, plus the following additions and corrections, each disclosed in the item notes:
Optimal revenues are suprema over all prices (and with quick response). "Optimal order" means a maximizer over all , never a stationary point, and the myopic benchmarks are the same functions at . Defining the optimal revenue by Lemma 2's closed form would make Lemma 2 and the first-order conditions definitional; it is not done.
The fill rate is , set to when no strategic consumer waits. With Lean's instead, would be a best response to every order and Theorem 2's last claim would be trivial.
A complete development needs:
The last two are reusable beyond this mission. Proofs of any milestone, alternative existence arguments, and sorry-free proofs of the newsvendor items are welcome. The comparison ", " of Theorem 2 and §8's numerical study are outside the scope.
In a stochastic multi-armed bandit a player repeatedly chooses one of arms and receives a random reward drawn from that arm's unknown distribution; the aim is to pull suboptimal arms as rarely as possible. Lai and Robbins (1985) and, for general models, Burnetas and Katehakis (1996) showed that any reasonable strategy must pull a suboptimal arm at least times in rounds, where is a minimal Kullback–Leibler divergence defined below. A strategy whose expected number of pulls matches this constant is asymptotically optimal.
For rewards in , classical index policies such as UCB (Auer, Cesa-Bianchi and Fischer, 2002) achieve pulls but with a constant governed by the gap of the means, not by . Cappé, Garivier, Maillard, Munos and Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Ann. Statist. 41(3), 2013 (arXiv:1210.1136v4), introduce the KL-UCB family of index policies and prove finite-time bounds whose leading term is the Lai–Robbins/Burnetas–Katehakis constant. This mission formalizes their result for empirical KL-UCB (Algorithm 3, Theorem 2), which is asymptotically optimal in the nonparametric model of finitely supported distributions on . A companion mission covers kl-UCB in one-parameter exponential families (Theorem 1).
Timeline: Lai and Robbins (1985), lower bound for parametric families; Burnetas and Katehakis (1996), lower bound and asymptotically optimal policies for general models; Honda and Takemura (2010, 2011), the DMED algorithm, asymptotically optimal for finitely supported and bounded rewards; Cappé et al. (2013), the first index policy with a non-asymptotic bound whose leading term is optimal in this model.
A bandit has arms with reward distributions in a known model : the set of probability distributions over with finite support. Write , and ; arm is suboptimal if . At each round the player picks an arm based on past observations and observes a reward drawn from . is the number of pulls of arm up to round .
Equivalently, each arm has a reward stack of i.i.d. draws from , all stacks independent, and the -th pull of arm returns . The empirical distribution of the first rewards is , and .
The minimal divergence is
the smallest Kullback–Leibler divergence from to a distribution of the model whose mean exceeds .
Empirical KL-UCB (Algorithm 3) pulls each arm once, then for pulls an arm maximizing
where is the set of probability distributions carried by and . The added point is essential: without it the index is the empirical-likelihood bound, which equals the empirical mean when every observation is .
Assume for all arms and . There is a constant depending only on and such that, for every suboptimal arm and all ,
The constants are the paper's. is the one quantity the main text does not give; it is existentially quantified, before the bandit, so it may depend on nothing but .
Theorem 2 gives a finite-time bound whose leading term, , equals the Burnetas–Katehakis lower bound for the model . Hence empirical KL-UCB is asymptotically optimal among all strategies for finitely supported rewards in , and the regret inherits the optimal constant. Since is at least the Bernoulli divergence of the means, and usually larger, the bound improves on kl-UCB and UCB for the same rewards. Proposition 1 is a non-asymptotic coverage bound for the empirical-likelihood upper confidence bound with the point added, valid for every law on , not only finitely supported ones.
The proofs of Theorem 2 and Proposition 1 are in the paper's supplemental article (Appendix B), not in the main text; no machine-checked proof of either exists. The mission produces formal statements of the theorem and of the proof skeleton (5)–(10) that the paper shares with Theorem 1, and of the two facts about that the bound needs. A formal proof would supply an explicit , which the paper defines only inside the supplement.
The skeleton (5)–(10) is elementary bookkeeping; the difficulty lies in the two sums it leaves, both of which must be shown to be with explicit constants. The second, , needs a deviation estimate for the empirical of a suboptimal arm that is precise enough to keep the leading constant : a bound that only controls the deviation of the empirical mean loses it, since depends on the whole distribution. The first, , concerns the optimal arm after a random number of pulls , which the algorithm itself determines, so fixed-sample bounds such as Proposition 1 do not apply directly. Both need regularity of as a function of a distribution in an infinite-dimensional model, where none of the closed forms of the exponential-family case is available.
Arms are Fin K, and arm of the paper is index . The bandit is the platform's stack-of-rewards model RegretBandits.Stochastic.IsStochasticBandit: (indexed from ) are independent, identically distributed within each arm, with mean . Pull counts and are the platform's pullCount and bestMean. Added to the page, and disclosed in each statement: every reward lies in pathwise (a representation of " is carried by "), every arm choice is measurable, and in the goal the strategy is non-anticipating ( is measurable with respect to the arms and rewards of rounds ). A run of Algorithm 3 is a pathwise predicate: rounds pull distinct arms, and every later round pulls a maximizer of , with ties broken by any rule. KL is Mathlib's InformationTheory.klDiv in , with the empirical distribution as first argument. is kept in and converted to a real number only in the final bounds, where it is finite and positive. Probabilities of events whose measurability is not asserted are outer probabilities. The page's in (10) is stated as the finite sum over that (8) produces. The probability space of Theorem 2 lies in Type.
Trivializing formalizations are ruled out. The index is a supremum over a set that is nonempty (it contains ) and bounded above, so it is never Lean's junk value. and range over , not over all measures. The run predicate has both the initialization and the argmax clause. is quantified before the bandit and the horizon.
Reusable beyond this mission: for , the empirical-likelihood bound of (15), and Proposition 1, a concentration inequality for empirical that applies to any bounded i.i.d. sample. Proofs of any milestone are welcome, as are proofs of the skeleton (5)–(10) that also apply to the companion kl-UCB mission.
In online routing of virtual circuits, connection requests between pairs of nodes of a capacitated network arrive one at a time. Each request must be accepted and routed on a single path with bandwidth , or rejected, immediately and irrevocably, and no edge may carry more than its capacity. The goal is to maximize the number of accepted requests (the throughput). The model goes back to Awerbuch, Azar and Plotkin (FOCS 1993), whose deterministic algorithm has a logarithmic competitive ratio when edge capacities are at least logarithmic in the size of the network, and it underlies the analysis of admission control in circuit-switched and bandwidth-reserved networks.
Buchbinder and Naor (Math. Oper. Res. 2009) recover an algorithm with the same competitive factor from a general recipe: an online primal–dual scheme first produces a feasible fractional routing online, and an online version of Raghavan's pessimistic estimator (J. Comput. Syst. Sci. 1988) then rounds it, also online. This mission formalizes that construction and its guarantee (Section 5.2 of the paper, with the Section 3 scheme it uses).
Timeline:
Let be a finite set of edges with capacities , and . Requests arrive online; request comes with a finite list of admissible paths, each a set of edges, all of size at most .
A fractional routing assigns flows ; it is feasible when for every request and the load of every edge is at most . Its value is ; is the largest value of a feasible routing of the arrived requests, an upper bound on the integral optimum.
The fractional scheme. The covering LP paired with the routing LP (the paper's primal, Fig. 3) has variables (cost ) and (cost ) with constraints . When arrives, its paths are visited in order; for each path whose constraint fails, is raised from to the least value restoring it, while for and follow the flow ( the load of , the flow of ). The parameters are and .
The rounding. With the rounding scale , the integral edge usage and the number of served requests, the potential is ,
After the fractional round of , the algorithm serves on a path (adding to for ) if this gives potential at most the potential before the round; otherwise it rejects .
For every request sequence, the algorithm never exceeds a capacity, and for every feasible fractional routing ,
The fractional scheme's flows are feasible and for every feasible .
initially, always, and whenever the flows of a request are raised by a non-negative amount of total at most , serving the request on some path or rejecting it does not increase .
The result shows that a deterministic online algorithm for throughput-competitive routing, previously designed by hand, falls out of two generic components: an online fractional packing scheme and an online pessimistic estimator. A side product is that the fractional phase alone produces, online, a near-optimal routing that respects all capacities exactly, independently of their size. When the rounding loses only a constant factor and the algorithm is -competitive, as in Awerbuch–Azar–Plotkin.
The results are proved in the paper; none is machine-checked. A formalization supplies a checked instance of the online primal–dual method together with derandomized online rounding, and fixes the constants the paper leaves inside . Related platform content: the monograph's OnlinePrimalDual.Routing.per_copy_guarantee and routing_competitive concern the Buchbinder–Naor -competitive algorithm with copies of the graph, a different scheme.
The fractional guarantee is argued in the paper continuously (rates of change of the primal and dual values), while the scheme as formalized is discrete: each flow is the least value restoring a constraint, and every primal variable is a maximum whose branch may switch during the increase. The continuous argument does not transfer verbatim, and feasibility depends on the least value restoring the constraint with equality.
The rounding is a derandomization. The existence of a good path or a good rejection is established in the paper as an expectation over a random trial; a deterministic statement about finitely many alternatives is what the mission asks for, with all exponential terms of under control at once. A frequent first attempt compares with the potential after the fractional round; the rule compares with , before the flow increase, and the guarantee is stated for that comparison.
Fintype E; capacities are real and positive. A request is a List (Finset E) of paths; the request sequence is a list. Simple paths of a graph are a special case; nothing in the argument uses graph structure. is a parameter with every path of size at most .List (List ℝ) of the shape of the request sequence. is quantified as "every feasible fractional routing".sInf). Ties among good paths are broken by list order; only paths that received flow in the current round are candidates for serving, so a request whose flow was not increased is rejected.Contributions welcome: proofs of the milestones, a reusable lemma "convex combination value some outcome value" for derandomization, and the discrete-to-continuous bridge for the Section 3 scheme.
Retailers of seasonal goods (fashion, electronics, airline seats) sell a fixed stock over a finite season to customers who arrive over time, and those customers know that prices may fall. A customer who expects a markdown waits, and a seller who ignores this loses revenue. The classical revenue-management literature (Gallego and van Ryzin 1994; Talluri and van Ryzin 2004) models myopic customers who buy on arrival or leave; the literature on forward-looking (strategic) buyers, for instance Aviv and Pazgal (2008), studies particular price paths.
Board and Skrzypacz ask the mechanism-design question: among all selling schemes, which maximizes the seller's expected discounted revenue when buyers arrive over time, have private values and time their purchases strategically? Their answer, published in the Journal of Political Economy in 2016, is that the optimal mechanism has a simple structure: in every period the seller sells to the highest remaining buyer if and only if his value exceeds a cutoff that depends only on the period and the number of units left. When demand is weakly decreasing over time, the cutoffs are characterized by one-period indifference conditions, which in the continuous-time limit can be implemented by posted prices. The source used here is the authors' accepted manuscript of February 6, 2015; all page numbers refer to that manuscript.
A seller has units of a good and sells them over periods ; unsold units are worth zero after period . Payoffs are discounted by . At the start of period a random number of buyers arrives, independently across periods, with a law that may depend on . Each buyer wants one unit; his value is drawn independently from a distribution with continuous density , distribution function and support . The marginal revenue of a buyer with value is
assumed strictly increasing and continuously differentiable, with .
By the standard mechanism-design reduction (§2.1, eq. (2.5)), the seller's problem is to choose when to serve each buyer so as to maximize the expected discounted sum of the served buyers' marginal revenues. The state in period , after the period- entrants have arrived, is the number of units left and the values of the buyers present. The value and the pre-entry value satisfy the Bellman equation (4.3):
where is the set of buyers left after the highest are served and the next period's entrants. Selling one unit to today rather than none gives the difference function
and the cutoff is the smallest with . Comparing selling to today with waiting and selling at least one unit tomorrow (to the best of and the entrants) gives (p. 17). Demand is weakly decreasing in the usual stochastic order if for all and .
If is weakly decreasing in the usual stochastic order then, for every ,
and is the unique root of in for : the seller is indifferent between selling to the cutoff type today and waiting one period to sell that unit tomorrow (the one-period-look-ahead property).
For every and , the optimal rule sells to the highest buyer iff , whatever the values of the lower buyers; ; and is the unique root of .
In attack order:
After the goal, (4.7) gives the period- cutoff equation .
Theorem 1 says that the optimal allocation does not depend on how many buyers are present or what their values are, only on time and inventory. This is what makes the optimal mechanism implementable without eliciting values from buyers as they arrive. Theorem 2 turns the global dynamic program into local indifference conditions. In the continuous-time limit (§5 of the paper) these become differential equations, and the optimum is implemented by posted prices with an auction at the end of the season. Under weakly decreasing demand, therefore, the classical revenue-management practice of posting prices loses nothing against the best possible mechanism.
The paper's results are proved, in prose, with envelope-theorem and coupling arguments. They have not been machine-checked. A formal development would produce a verified backward-induction model of multi-unit dynamic allocation with random arrivals, with the structural results (monotonicity, deterministic cutoffs, monotone comparative statics in inventory and time) that recur across dynamic pricing and optimal stopping. Two printed gaps are recorded below: the positivity of , and the restriction of footnote 12 to .
The obvious argument fails at "deterministic". A priori the cutoff for the highest buyer depends on the values of the lower buyers, because selling a unit today changes which of them will be served later and when. Lemma 3(a) holds only under the induction hypothesis that all future cutoffs are already deterministic and decreasing in inventory, so Lemma 3, Theorem 1 and (A.1) form a single backward induction over periods and units, and none of them can be proved in isolation. The value function is an expectation, over a random number of i.i.d. entrants, of a maximum over sorted values, so continuity and strict monotonicity in (Lemma 3(b), and the same for ) are not available from general facts. The tempting argument for Theorem 2, that cutoffs fall over time simply because fewer buyers arrive later, is incomplete: Lemma 4 has to compare two periods with different arrival laws and different future cutoffs at once.
Periods are natural numbers with , and units are natural numbers. Values, marginal revenues and profits are real numbers. The buyers present form a finite multiset of reals, and an absent buyer is absent, never a value . The value law is the measure with density ; the density is positive and continuous on and zero outside, and is defined from and . Expectations over a cohort are lower Lebesgue integrals against of nonnegative bounded quantities, so no non-measurable or non-integrable integrand can silently become . The value function is defined by the Bellman equation (4.3), with . The sequence problem (4.1) over purchase times is not formalized; the paper says either may be used (footnote 16).
Standing assumptions and handled gaps:
The cutoff is defined from , never as the threshold of an optimal policy, and "optimal" always means maximal in (4.3) over every number of units sold. A formalization that postulates a threshold policy, replaces the random cohort by its mean, or sets absent buyers to value would trivialize or change the statements and is ruled out. The mechanism-design reduction (IC/IR to (2.5)) and the continuous-time results of §5 are out of scope.
The usual stochastic order is the published platform definition StochasticOrders.Usual.UsualOrder. A complete development needs finite-horizon dynamic programming over multisets, expectations of functions of sorted i.i.d. samples, envelope arguments, and monotone coupling for the usual stochastic order on ; these parts are reusable beyond this mission. Proofs of any milestone are welcome, as is a proof that (4.3) agrees with the sequence problem (4.1).
Newton's method is the basic second-order method of continuous optimization: at the current point it replaces the objective by its second-order Taylor model and jumps to the stationary point of that model. Its defining property is speed near a nondegenerate minimum, where the error is squared at every step, so that the number of correct digits roughly doubles per iteration. This local behaviour is what makes Newton's method the inner engine of interior point methods, the polynomial-time algorithms for linear, conic and general convex programming (Nesterov and Nemirovski, 1994). In S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2), §5.3.2 recalls the traditional local analysis of Newton's method, Theorem 5.3, before turning to the affine-invariant self-concordance analysis used for interior point methods. This mission formalizes that theorem and the four steps of its proof.
Let carry the Euclidean norm , and write for the operator norm of a linear map , so that . Let be a function, with gradient and Hessian , a linear map (the derivative of the gradient map). For a real number , means for all .
The Hessian is -Lipschitz if for all .
Newton's method starts at and iterates, for ,
A point is a local minimum of if for all in a neighbourhood of ; it has strictly positive Hessian if for some .
Assume the Hessian of is -Lipschitz, , and is a local minimum with , . If , then Newton's method from is well defined (every Hessian along the iterates is invertible, so the sequence exists and is unique) and
The theorem gives a quantitative basin of quadratic convergence: an explicit radius , depending only on the curvature at the minimum and the Lipschitz constant of the Hessian, inside which Newton's method needs only iterations to reach accuracy . It is the classical statement whose shortcomings (dependence on a choice of norm, constants that change under linear changes of variables) motivate the self-concordance theory of the following subsections, and it is the local convergence result invoked whenever a damped or globalized Newton scheme is shown to enter its quadratic phase.
On the formal side, Mathlib has the calculus this needs (Fréchet derivatives, interval integrals of vector-valued maps, operator norms) but no convergence theorem for multivariate Newton's method for minimization. A formal proof produces reusable pieces: the integral form of the mean value theorem for gradients, the stability of a positive-definite lower bound under Lipschitz perturbations, and an inverse-operator norm bound from a quadratic-form lower bound. The result itself is classical and fully proved in the literature; what is open here is its machine-checked proof in this form.
The individual inequalities are short, but the argument is an induction in which well-definedness and the rate are proved together: the Hessian at is invertible only because is still in the ball of radius , and stays in that ball only because of the rate. A proof that first assumes the sequence exists and then bounds it is circular. The proof also passes between two kinds of control on the Hessian, a lower bound on its quadratic form and an operator-norm bound on its inverse, and the second is only meaningful once invertibility is established. Finally, the integral manipulations need integrability of the maps , which comes from the continuity of the Hessian.
is EuclideanSpace ℝ (Fin n). The gradient and Hessian are explicit maps and with ContDiff ℝ 2 f, HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every point; the norm on is Mathlib's operator norm, as on the page. is the quadratic-form inequality. A Newton run is a sequence indexed from satisfying the linear system ; no inverse of a possibly singular operator appears in any hypothesis, and "well defined" is a conclusion: a unique run exists from and every Hessian along it is bijective. The rate and are asserted for every run. The error representation is stated with both sides multiplied by , which is equivalent to the printed form once the Hessian is invertible. Milestones 3 and 4 use only the Lipschitz property and are stated for any Lipschitz map .
Added hypothesis: (the radius divides by ; with , Lean's convention would collapse the hypothesis to ). Convexity of is not assumed, as on the page; is a local minimum and is derived, not assumed. Encoding the Newton step with Lean's inverse (which returns on singular maps), or replacing by mere invertibility, would change the theorem and is ruled out.
A complete development needs the fundamental theorem of calculus for vector-valued maps along segments, Hessian-based quadratic-form estimates, and operator-norm bounds for inverses; all are reusable for the analysis of damped Newton, cubic regularization and interior point methods. Proofs of the milestones independently of the goal are welcome.
First-order methods, which query only function values and gradients, are the workhorse of large-scale optimization in machine learning, signal processing and operations research, because each step costs little more than one gradient evaluation. For a function that is both strongly convex and smooth, plain gradient descent converges geometrically, but the number of steps needed to reach accuracy scales with the condition number of the problem. In 1983 Nesterov showed that a gradient method with a carefully chosen momentum term needs a number of steps proportional to instead, and that this is optimal for black-box first-order methods. On ill-conditioned problems, where is in the thousands or millions, the difference between and is the difference between practical and impractical.
This mission is the tenth of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2). It covers §3.7.1, the smooth and strongly convex case of Nesterov's accelerated gradient descent, and its main result, Theorem 3.18.
Work in with the Euclidean inner product and norm . Let be differentiable with gradient .
Nesterov's accelerated gradient descent starts at an arbitrary point and iterates, for ,
The point is a gradient step from , and moves beyond in the direction by the fixed momentum factor .
The analysis in the book uses auxiliary quadratic functions (an estimate sequence), defined from the points by
together with their centres (with and the recursion (3.21) of the book) and their minimum values .
For every run of the method and every ,
The geometric form in milestone 3 is slightly stronger than the goal, which follows from .
Theorem 3.18 gives -accuracy after gradient evaluations. Projected gradient descent with step on the same class contracts only at the rate (Theorem 3.10 of the book). The lower bound of Theorem 3.15 shows that no black-box first-order method can do better than , so the accelerated rate is optimal up to constants. The estimate-sequence argument is the template for many later accelerated methods: proximal, stochastic and variance-reduced variants such as Katyusha, and accelerated coordinate descent.
The result is classical and fully proved on paper. No machine-checked proof of the accelerated rate for strongly convex smooth functions is known to exist in Lean's Mathlib. This mission produces one, with the estimate sequence , its centres and its minimum values as reusable objects, and with every algebraic identity of the book's proof stated separately.
The algorithm is two lines, but its analysis is not a one-step contraction: neither nor decreases by the factor at every step. A Lyapunov argument for gradient descent, applied directly to , gives only the rate . The book obtains the rate through the auxiliary functions . The inequality (3.18) is easy, but (3.19), that the minimum of never drops below , depends on the exact choice of the momentum factor. It holds only through the identity , which ties the centre of to the iterates. Formally, the obstacles are the bookkeeping of the recursive quadratics on and the algebra in , and .
EuclideanSpace ℝ (Fin n). The gradient is an explicit map g with HasGradientAt f (g x) x at every point, which is part of the smoothness predicate IsBetaSmooth f g β. Strong convexity is the published definition OnlineConvexOpt.ConvexBasics.StronglyConvexOn Set.univ f g α, which is the book's (3.13).IsNesterovSCRun g α β x y on two sequences indexed from , with arbitrary. Every theorem holds for every run, that is, every starting point.kappa α β = β / α. All theorems assume and . The second is implied by the other hypotheses for ; no hypothesis is added.ConvexOptAlg.NesterovStrong. β-smoothness duplicates the predicate of other missions of the series and will be merged afterwards. Contributions welcome: proofs of the milestones, and general lemmas on quadratics that the algebraic milestones need.Regularized logistic regression and the support vector machine (SVM) are two of the most widely used linear classifiers. Both are usually introduced as empirical risk minimization plus a norm penalty whose size is tuned by cross-validation, with the penalty justified heuristically as a guard against overfitting. Distributionally robust optimization (DRO) offers a different reading: instead of minimizing the average loss on the training sample, minimize the worst average loss over all distributions close to the empirical one. Blanchet, Kang and Murthy (arXiv:1610.05627v4; J. Appl. Probab. 56(3), 2019) show that, for a suitable notion of closeness based on optimal transport, the robust problem and the penalized problem coincide exactly. The penalty is then the price of robustness against perturbations of the predictors, and the regularization parameter becomes the radius of an uncertainty set, which the same paper later chooses by a statistical criterion (the robust Wasserstein profile).
Related earlier work: Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) studied Wasserstein-robust logistic regression with a metric that charges a finite price for flipping a label, and obtained regularized logistic regression only in the limit . The result formalized here is the exact statement at , together with the analogous statement for the hinge loss.
Training data are pairs with predictors and labels , . Their empirical distribution is , a probability measure on .
For a cost , the optimal transport cost between probability measures and on is
The cost used here is the label-preserving cost: for ,
Every distribution with has the same label distribution as ; only the predictors are perturbed. The exponent is the conjugate of , .
The losses are the log-exponential loss and the hinge loss , for a coefficient vector . The worst-case expected loss at radius is , the supremum over probability measures on .
For every and every ,
and consequently the two identities obtained by taking on both sides, which is how the paper prints the theorem.
The theorem identifies two standard estimators as exact solutions of a robust decision problem. Consequences: the penalty has a quantitative meaning (the adversary's transport budget), the regularization parameter can be chosen by the paper's robust Wasserstein profile instead of cross-validation, and the norm of the penalty is tied to the geometry of the perturbations (perturbations measured in give an penalty). The same identity is the input of the paper's coverage bound (Proposition 6) for .
The result is proved on paper; no machine-checked version is known. The formalization adds a precise statement of the objects involved (couplings with both marginals fixed, an infinite cost across labels, expectations of nonnegative losses with values in ), a checked version of the duality step specialised to this cost, and the treatment of boundary cases (, , ) that the paper does not discuss.
The identities are short once Proposition 1 is available, so the weight of the mission lies in two places. First, Proposition 1 itself is a strong duality theorem for optimal transport over all probability measures on , with a cost that takes the value and an unbounded loss, and with attainment of the dual minimum; it is quoted from Blanchet and Murthy (Math. Oper. Res. 2019) and not proved in this paper. The weak-duality inequality is routine; the reverse inequality requires constructing near-optimal distributions from the dual, which needs measurable selection of near-maximizers and does not follow from finite-dimensional convex duality. Second, the inner suprema require an exact Hölder-attainment argument for the pair of conjugate norms and , including and , and for the hinge loss a minimax exchange over . Bypassing duality by a direct construction of the worst distribution is possible for the upper value but not obviously for the lower bound at the boundary .
Fin d → ℝ, a data point is (Fin d → ℝ) × ℝ with the product Borel σ-algebra, and samples are indexed by Fin n with 0 < n. Labels are real numbers with the hypothesis , which Theorem 2 inherits from Example 2; the cost is defined on all of .PiLp q, with q p : ℝ≥0∞ and p.HolderConjugate q; and are included, and no further restriction on is imposed.WassersteinDRO.Regularization.empiricalDistribution.PiLp, and calculus for the logistic function. Contributions to any of these are welcome, as are proofs of the inner suprema, which are independent of Proposition 1.Upper bounds for an optimization method say how fast it converges; oracle complexity lower bounds say how fast any method of a given kind can possibly converge. Chapter 3 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015, arXiv:1405.4980) proves upper bounds for subgradient descent on Lipschitz functions and for gradient methods on smooth functions. Section 3.5 (Lower bounds, pp. 279–283) shows that these rates cannot be improved by more than a numerical constant, as long as the number of queries is smaller than the dimension. For smooth convex functions the matching lower bound is what identifies Nesterov's accelerated gradient descent, with its rate, as an optimal method.
Timeline. The lower bounds first appeared in A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization (Wiley, 1983). The presentation followed by the book, with an explicit tridiagonal quadratic as the hard instance and the "span of past gradients" restriction on the method, is that of Y. Nesterov, Introductory Lectures on Convex Optimization (Kluwer, 2004), §2.1.2. Nesterov's accelerated method (1983) attains the matching upper bound.
Work in with the Euclidean inner product , coordinates , canonical basis and balls . A first-order oracle for answers a query with a subgradient (the gradient when is differentiable). A black-box procedure maps the history to the next query . Section 3.5 restricts attention to procedures with
which covers gradient descent, its accelerated variants and conjugate gradient. A function is -smooth if its gradient is -Lipschitz; -Lipschitz on if every subgradient at every point of has norm at most ; -strongly convex if is convex.
The hard smooth instance uses, for , the symmetric tridiagonal matrix with entries on the first diagonal positions and on the neighbouring off-diagonal positions of the leading block, zero elsewhere, and the quadratics
For and there are a -smooth convex and a minimizer such that every procedure satisfying (3.15) has
The constant is the book's.
For and there are a convex , -Lipschitz on , and a first-order oracle for it such that every procedure satisfying (3.15) has ; and for there are an -strongly convex , -Lipschitz on , and an oracle with gap at least over that ball.
The upper bounds of Chapter 3 (projected subgradient descent at rate , accelerated gradient descent at rate ) become optimal statements only through these lower bounds: no method in the class (3.15) can be faster by more than a constant factor while is below the dimension. The restriction to is necessary, since Chapter 2's cutting-plane methods converge exponentially once the number of queries exceeds the dimension.
The results are classical and proved. Formalizing them yields machine-checked versions of the quadratic-form computation for the tridiagonal matrix, of the Krylov-type support argument under (3.15), and of the explicit minimizer of , each reusable in other lower-bound arguments (Theorem 3.15 in , lower bounds for strongly convex smooth functions, conjugate gradient analyses). The platform held no formal statement of these oracle lower bounds when this mission was drafted.
Each analytic step is elementary; the difficulty is in the bookkeeping. The span argument is an induction that must track, at each step, that the gradient of a tridiagonal quadratic at a vector supported on the first coordinates is supported on the first , and that the span hypothesis transfers this to the next query. The minimizer computation requires solving on the leading block and showing that the coordinates beyond do not affect . A natural first attempt, choosing the hard function after seeing the procedure, proves a much weaker statement and is excluded by the quantifier order: the function is fixed first and must defeat every procedure.
is EuclideanSpace ℝ (Fin n). Coordinates in Lean are 0-based; the definitions provide the book's 1-based coordinate coord x i and basis vector basisVec n i, and the matrix tridiag n k translates book index to Fin n index . The query sequence starts at index . The oracle is a fixed map , so (3.15) reads with . In Theorem 3.14 the oracle is the gradient, given as a map with HasGradientAt everywhere; -smoothness is the Lipschitz bound on that map. In Theorem 3.13 the oracle is part of what is constructed, because the book's proof uses a specific "resisting" subgradient selection and the claim fails for an arbitrary one.
Committed conventions, each stated in the item's Formalization Note: the minimum over is the bound for every such , and is required; is ; the minimizer is existentially chosen together with (the hard function has many minimizers when , and the bound is false for some of them); the minimum over a ball is the bound against every point of the ball; is the real infimum, asserted to be attained.
A formalization that let the function depend on the procedure, dropped , or took the span over gradients at points other than the queries would state a different and weaker theorem; the statements here keep (and the oracle) before the universally quantified procedure.
Infrastructure needed: quadratic forms of explicit matrices on EuclideanSpace, gradients of quadratics, and span/support lemmas for EuclideanSpace.single-type vectors. Contributions of proofs for any milestone, and of the strongly convex lower bound (Theorem 3.15, not included here), are welcome.
Many planning problems are made in two stages: a first decision (capacity, inventory, a network design) is fixed before an uncertain demand is revealed, and a second decision (recourse, routing, overtime) is taken afterwards. Two-stage stochastic optimization models the demand as random and minimizes expected cost; its second stage is a whole policy , and the problem is intractable in general, especially with integer variables (Dyer and Stougie, 2006). Robust optimization instead picks one static pair that is feasible for every possible demand and minimizes its worst-case cost; it is a single deterministic mixed-integer program and needs no knowledge of the distribution (Ben-Tal and Nemirovski, 2002; Bertsimas and Sim, 2004).
The question this mission addresses is how much is lost by solving the robust problem in place of the stochastic one. Bertsimas and Goyal (Math. Oper. Res. 2010) show that when only the right-hand side is uncertain, the uncertainty set is symmetric and the distribution is centred at its point of symmetry, the loss is at most a factor of two, and that this factor is tight.
Fix , and nonnegative costs , . A set of scenarios carries a probability measure , and each scenario has a right-hand side . The uncertainty set is . First-stage variables are nonnegative, with integer values on a designated set of coordinates; second-stage variables are nonnegative reals ().
The stochastic problem , (1.1), chooses and a policy :
The robust problem , (1.2), chooses one for all scenarios:
A set is symmetric (Definition 1.2) if there is with for all ; is its point of symmetry. Hypercubes, ellipsoids and norm balls are symmetric. A probability measure on a symmetric set is symmetric (Definition 1.4) if it gives a set and its reflection the same mass.
If is symmetric with point of symmetry , , and satisfies
then
The result. The robust problem is one mixed-integer program, independent of ; the stochastic problem optimizes over policies and requires the distribution. Theorem 2.1 says that under symmetry the static robust solution used in every scenario is a 2-approximation of the optimal expected cost, for every centred distribution at once. The companion results of the paper show the hypotheses matter: the bound is tight for symmetric sets, the gap is unbounded (at least ) on the non-symmetric simplex (Theorem 2.6), and unbounded when costs are uncertain as well (Theorem 3.1). The theorem also underlies later work on the power of static and affine policies in adaptive optimization (Bertsimas and Goyal, 2012).
Formalizing it. The theorem and its proof are published; nothing in this mission is open mathematics. To our knowledge none of these statements has a machine-checked proof. The mission produces a reusable Lean model of two-stage stochastic and robust mixed-integer covering problems with arbitrary scenario spaces, extended-real optimal values and genuine expectations, together with the elementary geometry of point-symmetric sets. The same objects are used by the other missions of this series (the simplex and cost-uncertainty gaps, and the adaptability gap).
Each step of the published argument is short; the difficulty is in stating it at the right generality. The paper begins "consider an optimal solution" of ; optimal policies need not exist for an arbitrary scenario space, so the statement is about infima and every step must work for an arbitrary feasible pair. Passing from " for all " to "" needs integrability of the policy and of and linearity of the Bochner integral through a matrix. The bound uses symmetry together with nonnegativity of the uncertainty set; symmetry alone does not give it. Integrality of the second stage breaks the argument, since need not be integral.
Fin k → ℝ with the componentwise order, products A *ᵥ x and inner products c ⬝ᵥ x. The mixed-integer domain is "nonnegative with integer values on a set of coordinates", which is the paper's up to relabelling.Set.range b. Constraints hold for every scenario, not almost surely.EReal, equal to when infeasible; no attainment is assumed. A real-valued infimum would return on an infeasible robust problem and make the goal trivial; that formalization is ruled out.Contributions welcome: proofs of the milestones and the goal, and general lemmas on point-symmetric sets and on interchanging Bochner integrals with matrix–vector products, both reusable outside this mission.
Many constrained optimization problems in machine learning and statistics have a feasible set over which a linear function is cheap to minimize but a Euclidean projection is expensive: the -ball, the simplex, the nuclear-norm ball, the convex hull of a combinatorial family. Projected gradient descent needs a projection at every step. Conditional gradient descent, introduced by Frank and Wolfe in 1956 for quadratic programming, replaces the projection by a call to a linear minimization oracle over , and its iterates are convex combinations of oracle outputs, which makes them sparse when is a polytope.
This mission is the seventh of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015, arXiv:1405.4980v2). It covers Section 3.3, whose main result, Theorem 3.8, is the rate of the method in the form given by Jaggi (2013), going back to Dunn and Harshbarger (1978).
Let be a finite-dimensional real vector space with an arbitrary norm . For a linear form on , written , the dual norm is . Let be nonempty, compact and convex, with diameter .
Let be differentiable with gradient , a linear form on . For , is β-smooth with respect to on if
A point with is fixed throughout, and .
Given step sizes , a run of conditional gradient descent is a pair of sequences with and, for every ,
The minimizer need not be unique; any choice is allowed.
If is convex and -smooth with respect to and for , then every run satisfies, for every ,
Theorem 3.8 is the basic guarantee for projection-free first-order optimization. Its rate does not depend on the dimension, and it depends on the geometry only through the product , both measured in the same norm, which may be chosen to fit : for the -ball, smoothness in with dual norm gives much better constants than the Euclidean analysis. The book applies it this way to a LASSO-type problem (Section 3.3, pp. 274–276), and the same bound underlies the sparse-approximation corollary on the simplex (p. 273) and the many later variants of the method (away steps, stochastic and online conditional gradient).
The result is classical and proved in the book. What this mission adds is a machine-checked statement and proof in an arbitrary finite-dimensional normed space, with the dual norm as the operator norm on linear forms, and a reusable encoding of norm-smoothness and of conditional gradient runs. On Prove2Me a related result is already proved: Lan's Theorem 7.1 (First-order and Stochastic Optimization Methods), which bounds by with a different indexing; after the diameter bound it yields at Bubeck's iterate , which is weaker than Theorem 3.8 by one step.
The difficulty is in the bookkeeping of norms and indices, not in a deep idea. Inequality (3.4) is proved in the book only for the Euclidean norm, where and the Cauchy–Schwarz inequality is used; in a general norm it needs the pairing between a linear form and a vector and the bound . The rate is attained only by starting the induction at , where the step erases the dependence on the starting point; at the bound can fail, since is arbitrary. A first attempt that runs the induction from with an arbitrary does not give the stated constant.
is a type with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]; nothing is specialised to the Euclidean norm. The gradient is an explicit derivative map f' : E → (E →L[ℝ] ℝ) with HasFDerivAt f (f' x) x for every x; is f' x v, and is the operator norm, which equals . is Metric.diam X, which equals the supremum of over because is compact. Sequences are indexed by ℕ with the first iterate at index 1.
Committed conventions: compact, convex and containing (hence nonempty); convexity of and the Lipschitz bound on the gradient are assumed on only, which is weaker than the book's global assumptions; ; the existence of the minimizer is the book's standing assumption (p. 242); the conclusion is stated for , as in the book. Runs are predicates: is any minimizer of the linear form over and is required, so the goal quantifies over every run with . A formalization in which need not lie in , or in which smoothness is assumed only along the iterates, states a different theorem and is excluded.
A complete development needs the descent inequality (3.4) for Fréchet derivatives in a normed space (reusable for every smooth method in the series and beyond), the fact that the iterates stay in , and a scalar induction. Proofs of the milestones are welcome independently; milestone 4 is a statement about real sequences only.
Gradient descent is a basic method for minimizing a differentiable function when evaluating its gradient is practical but solving the optimization problem directly is not. The rate at which its iterates approach an optimizer depends on the assumptions about the function. For a convex function with a Lipschitz gradient, the value error decreases at a sublinear rate. Adding strong convexity changes the behavior: the distance from the optimizer contracts at each step, giving an exponential bound on the value error. This section of Bubeck's monograph identifies a fixed step size that uses both the smoothness and curvature constants and gives the corresponding rate.
The result matters when a high-accuracy answer is needed. A sublinear bound makes each extra digit progressively more expensive; an exponential bound says that a fixed number of additional gradient evaluations reduces the error by a fixed factor. The theorem is a textbook result, already proved mathematically. This mission asks for its precise machine-checked statement and the source's supporting inequalities, rather than for a new optimization method.
Work in Euclidean space with , equipped with its usual inner product and norm. A differentiable function has gradient . It is -smooth when its gradient is -Lipschitz: for every . It is -strongly convex when, for every ,
The first condition limits how rapidly the gradient changes. The second gives a quadratic lower bound on the function around any point. Here and . In positive dimension, the two conditions together entail , so the condition number is at least one. The case remains part of the target.
A point is a global minimizer when for every . The book assumes such a point exists as a standing convention. A gradient descent run is a sequence satisfying at each positive index. Its first iterate is arbitrary. The step size in this mission is fixed at , rather than chosen by line search or adapted along the run.
The central target is Theorem 3.12 of Bubeck, p. 279. For every integer , the gradient descent run satisfies
At this is a smoothness bound on the initial value gap. For subsequent iterations it gives a linear convergence rate with the explicit exponential factor stated in the book. No initial-radius bound or bounded domain is imposed: the actual squared distance appears in the conclusion.
The milestones trace the mathematical claims stated in the source. Equation (3.6) is the co-coercivity inequality for gradients of convex smooth functions. The proof of Lemma 3.11 introduces , and identifies it as convex and -smooth. Lemma 3.11 combines curvature and smoothness into a sharper inequality for two gradients. The proof of Theorem 3.12 then gives a value-gap bound, a one-step distance contraction, and its iterated exponential form. These statements are separately useful: the co-coercivity and contraction bounds can be reused in analyses of related first-order methods.
The theorem states a complete guarantee for the algorithm: an explicit rule, the hypotheses on the objective, and a bound valid for every iteration count. It makes the role of visible. When is close to one, the contraction is strong; when the smoothness constant is much larger than the curvature constant, more iterations are needed for the same error reduction. The stated dependence supports comparisons with projected and accelerated gradient methods elsewhere in the same monograph.
Formalizing the result requires a common interface for actual gradients, smoothness, strong convexity, and algorithm runs. The strong-convexity predicate is an existing published definition, while the local smoothness and run definitions use Bubeck's conventions. Once these interfaces and the inequalities are proved, later missions can use the resulting declarations to compare rates without translating between informal meanings of “smooth” or changing the iterate index. The source provides a mathematical proof; these draft Lean theorems carry sorry and do not yet constitute machine-checked proofs.
The main issue is getting the sharp contraction factor from two assumptions that control different parts of the gradient step. A direct Lipschitz estimate on the update map does not by itself express the mixed inner-product term with the constants needed for the stated factor. Lemma 3.11 is the source's precise bridge between the gradient difference, the point displacement, and their inner product. The case also needs to remain valid: a proof route that divides by cannot cover that boundary by the same calculation.
The last display in the proof of Theorem 3.12 joins a one-step inequality involving to an exponential inequality involving . The latter is the cumulative statement after steps. Keeping these as separate milestones makes each quantified claim explicit while preserving the theorem's bound.
Lean represents as EuclideanSpace ℝ (Fin n), with . The gradient is an explicit map required to be the actual gradient of at every point. Smoothness is the gradient Lipschitz condition, not a quadratic upper bound used as a definition. Strong convexity uses the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn predicate on the whole space; its formula is the book's (3.13). Iterates are indexed from one, and index zero imposes no condition. The norm, inner product, constants, and real exponential follow the printed formulas.
The added explicit conditions are , , and where Equation (3.6) divides by . Positive dimension excludes a degenerate space where curvature imposes no restriction on smoothness. The positivity of makes meaningful; the source treats it as a positive strong-convexity parameter. The minimizer hypothesis is the book's standing convention. There is no assumption that : that property follows from global minimality and differentiability. A gradient map unrelated to would trivialize the model, so the smoothness definition includes the gradient identity.
The local development needs Euclidean inner-product identities, convexity, differentiability, Lipschitz gradient bounds, and real exponential estimates. The auxiliary function and the two co-coercivity inequalities are reusable outside this chapter. Contributions should prove the exact milestone statements and the final theorem, including and , without weakening constants or substituting another gradient descent step.
A shortest path problem asks how to reach a destination at minimum cost. In a stochastic shortest path problem, a decision at a state selects a probability distribution over successor states, so both the route and its total cost are random. Costs may have either sign. This makes the problem relevant to finite-state control models where rewards and expenses occur before eventual termination. Bertsekas and Tsitsiklis analyze this setting without requiring all one-stage costs to be nonnegative or all to be nonpositive. Their condition instead rules out an improper stationary policy whose costs stay finite from every initial state. Bertsekas and Tsitsiklis (1991), pp. 580–583.
Earlier treatments established Bellman-equation and algorithmic conclusions under positive or nonnegative costs. The 1991 paper traces the finite-control development from Eaton and Zadeh and the compact-control extension from Kushner, then removes the sign restriction while retaining finite state space. It also explains why the Bellman mapping need not contract when an improper policy is available. Bertsekas and Tsitsiklis (1991), pp. 581, 585. A separate, proved Prove2Me theorem from Bertsekas's textbook treats the special case in which every policy is proper and controls are finite; the result here permits improper policies and compact control spaces.
There are states. State is the destination. At state , a control incurs a real cost and moves the process to state with probability . A selector chooses one control at every state. A policy may change selectors over time; a stationary policy repeats one selector. The matrix has entries , and is the vector of one-stage costs. Bertsekas and Tsitsiklis (1991), p. 582.
The cost vector is the coordinatewise limit inferior of expected partial costs, including the possibility of infinite values. The optimal cost is the infimum of over all policies, including nonstationary ones. Optimality of a policy means it attains that infimum from every initial state. The fixed-selector operator is ; the Bellman operator takes the coordinatewise infimum of these vectors over selectors. Bertsekas and Tsitsiklis (1991), pp. 582–583, equations (2)–(6).
A stationary policy is proper when its probability of reaching state tends to one from every starting state. Assumption 1 says state is absorbing and cost-free, at least one proper stationary policy exists, and every improper stationary policy has a partial-cost coordinate tending to . Assumption 2 makes each control space compact, each cost function lower semicontinuous, and each transition-probability coordinate continuous. Work takes place in . Bertsekas and Tsitsiklis (1991), pp. 583–584.
Under Assumptions 1 and 2, the optimal cost is finite and is the unique fixed point of in . Every initial has
A stationary selector is optimal exactly when ; an optimal proper stationary selector exists. These are all clauses of Proposition 2, rather than separate targets selected from it. Bertsekas and Tsitsiklis (1991), p. 586, Proposition 2.
The milestone list follows the source's Proposition 1, Lemmas 1–3, and the numbered equations used by their proof. Proposition 1 supplies a weighted maximum-norm contraction when every stationary policy is proper. Lemma 1 describes fixed costs of a proper policy and characterizes properness through a Bellman inequality. Lemma 2 gives continuity of . Lemma 3 controls limits of proper policies; its second part detects a limit that becomes improper through diverging costs. Appendix equations (22) and (24), and the policy-improvement equation (15), provide the paper's intermediate targets. Bertsekas and Tsitsiklis (1991), pp. 585–587, 591–592.
Proposition 2 identifies the cost of the best policy by a finite-dimensional Bellman equation even though the definition of optimal cost ranges over all, possibly nonstationary, policies. Its convergence clause justifies value iteration from any vector whose destination coordinate is zero. Its policy criterion and existence clause connect a fixed point to an implementable stationary decision rule. The paper applies these conclusions to successive approximation and policy iteration in §4. Bertsekas and Tsitsiklis (1991), pp. 586, 590–591.
The paper proves these statements. This mission seeks machine-checked proofs of their exact finite-state formulation and of the listed intermediate results. The resulting finite stochastic-matrix, hitting, and policy-cost infrastructure can also support other undiscounted control problems. The related proved Prove2Me result for the all-proper finite-control case does not settle this mission's compact-control or improper-policy cases.
When every stationary policy is proper, a common weighted maximum norm makes the Bellman mapping contract. An improper policy can destroy this route: Figure 2 has an absorbing destination and satisfies both assumptions, yet is not a contraction in any norm on . The main result therefore needs a way to retain fixed-point uniqueness and convergence without a uniform contraction rate. Compactness matters because a sequence of proper selectors may converge to an improper selector; Lemma 3 explains the associated cost behavior. Bertsekas and Tsitsiklis (1991), pp. 585–586, 591–595.
States are Fin n, with the paper's state represented by 0; the model requires . A control set is a type with a metric, with compactness asserted for its whole carrier. Transition rows explicitly have nonnegative entries summing to one. These are the probability-vector conditions implicit in the word “probability.” Assumption 1 supplies a selector and therefore nonempty control sets. The paper writes ; where a theorem uses only Assumption 1, finite real Bellman infima are made explicit through TRealValued. Under Assumption 2, compactness and lower semicontinuity give real attained minima. Bertsekas and Tsitsiklis (1991), pp. 582–584.
Policy costs and their infimum use extended reals so that an improper policy's cost is represented without a default finite value. Proposition 2 concludes, rather than assumes, that has real coordinates. Its policy infimum ranges over every sequence of selectors. Matrix products use the identity at time zero; is the identity. The destination-zero restriction is retained in every fixed-point and iteration claim. Defining optimal cost as a Bellman fixed point, or restricting the infimum to stationary policies, would remove the result the paper proves. Solvers can contribute the finite-chain, matrix-inverse, semicontinuity, and convergence arguments needed by these targets.