Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Hypergraph Turán problems ask how many edges a -uniform hypergraph on vertices can have without containing a fixed sub-hypergraph. For graphs () the theory is well developed; for exact answers are rare and are known mostly for small, dense configurations such as the Fano plane or expanded triangles. Paths are the natural sparse test case. For graphs, Erdős and Gallai (1959) showed that a graph on vertices without a path of length has at most edges. For hypergraphs there are several notions of path: Berge paths (Győri, Katona and Lemons, 2010), loose paths (Mubayi and Verstraëte, 2007, asymptotic bounds) and the most restrictive notion, linear paths. The case of two edges was solved by Frankl (1977), and the case asymptotically by Frankl and Füredi (1987).
Füredi, Jiang and Seiver (arXiv:1108.1247v1, published in Combinatorica 34 (2014), doi:10.1007/s00493-014-2838-4) determined the Turán number of every -uniform linear path exactly, for and large, together with the unique extremal families. It is one of the few exact hypergraph Turán results for an infinite family of forbidden hypergraphs.
The vertex set is . A family is a set of subsets of ; it is -uniform if , the set of all -element subsets.
A linear path of length is a sequence of distinct sets such that
The -uniform linear path of length is written ; a family contains it if some of its members form a linear path. The Turán number is the maximum size of a -uniform family on that does not contain .
Two counting functions describe the answer:
For a set of elements, is the number of -sets meeting (the star family of ), and adds the -sets of that contain two fixed vertices (the even family).
The proof is phrased in the language of the delta-system method: -stars (sets pairwise meeting in a common kernel), the kernel degree (the largest for which an -star with kernel exists), -homogeneous families (k-partite families whose intersections follow a single intersection-closed pattern of subsets of , each intersection being the kernel of an -star), the rank of , the kernel graph of , and the -blowup of a graph .
For every and there is such that for all :
and in each case a -uniform, path-free family of that size is exactly the star family of some -set (odd case), respectively the even family of some -set and two distinct vertices (even case).
In the order the proof uses them:
The theorem gives the exact extremal number and the unique extremal configuration for every linear path when , and its proof yields a stability statement (Theorem 5.1 of the paper): a path-free family of nearly extremal size is close to a star family. The method is the standard template for exact results on sparse hypergraphs: delta-system decomposition, an asymptotic bound from a graph theorem applied to a kernel graph, then stability and cleaning.
The result is proved in the paper. As far as the platform's catalog shows, none of it is formalized: Mathlib has the intersecting Erdős–Ko–Rado theorem () but not the -intersecting version with uniqueness for large , not Erdős' matching theorem, not the Erdős–Gallai circumference theorem, and no delta-system machinery. A formalization would produce reusable libraries for each of these, and the first machine-checked exact hypergraph Turán number for an infinite family.
The obvious argument — bound the number of members through each vertex and sum — gives only with a wrong leading constant, because a path-free family can have vertices of almost full degree. Exactness needs three layers that do not reduce to one another. First, the intersection semilattice lemma (Lemma 3.1) is a deep structural theorem with a doubly exponential constant; it is cited, not proved, in the paper. Second, the asymptotic bound passes through the Erdős–Gallai circumference theorem, itself a nontrivial graph result. Third, the exact value requires a stability argument with several error terms (, ) that must be balanced, followed by Erdős' matching theorem and the 2-intersecting Erdős–Ko–Rado theorem for large , both with uniqueness. The structural lemmas of §§3–4 are elementary but involve greedy embeddings in which disjointness of the new vertices has to be maintained carefully.
Vertices are Fin n; families are Finset (Finset (Fin n)); -uniformity is 𝓕 ⊆ univ.powersetCard k. A linear path is an injective map Fin ℓ → Finset (Fin n) into the family with consecutive members meeting in exactly one vertex and non-consecutive members disjoint. The Turán number is a Finset.sup of cardinalities over all path-free -uniform subfamilies, a finite attained maximum for ; at the feasible set is empty and Lean returns zero, which no theorem here uses. Partitions into parts are part maps Fin n → Fin k; stars are finsets of distinct petals; the rank is a minimum computed with sInf, exact because intersection patterns consist of proper subsets of . "Sufficiently large " and every are explicit existential constants chosen before and the family.
Hypotheses added relative to the page: Theorem 3.8 assumes the homogeneous family is nonempty (the empty family is homogeneous for every pattern, and the proof starts from a member). Lemma 4.2 states , implicit in the paper's definition of a blowup using new vertices; it excludes a false zero-threshold case at . Lemma 4.3 is stated for an arbitrary choice of a vertex in each member, a generalization of the printed lemma, whose proof uses only . Bound (1) is posed for . Claims 2–3 are stated stand-alone with the -set existentially quantified.
Trivializing formalizations are ruled out: the goal asserts the value and the uniqueness of the extremal family, the Turán number is a true maximum rather than a junk supremum, the linear path requires intersections of size exactly one and disjointness of non-consecutive members, and all constants are quantified before .
Needed infrastructure: the delta-system method (Lemma 3.1), Erdős–Gallai for circumference, Erdős' matching theorem and -intersecting Erdős–Ko–Rado for large . Each is reusable well beyond this mission, and contributions of any of them are welcome.
Quantum information often describes a system through a state shared among many small registers. One would like to replace the state on a few registers by a product of their individual states, because product states are easier to estimate and optimize over. The usual finite quantum de Finetti theorems obtain such approximations from permutation symmetry. A physical preparation, however, need not be symmetric. Berta, Borderi, Fawzi and Scholz give a quantitative statement that instead selects the retained registers at random and conditions on measurements of other registers. Their Theorem 2.5 is the target here.
The authors place this result alongside their hierarchy for constrained bilinear optimization, but the theorem without symmetry is independent of the hierarchy. In §2.6 they compare its polynomial dependence on the local dimension and the number of retained registers with the earlier no-symmetry approximation discussed in their reference [12]. The result identifies exactly what random selection and measurement can supply when a global permutation-invariance hypothesis is unavailable.
Let be a quantum system of dimension , and let be an arbitrary density operator on copies of . Choose a uniformly random permutation of these copies. Its first positions form an ordered tuple of systems to retain; the remaining positions form an ordered tuple available for measurement. There is no symmetry condition on .
A measurement on has finitely many outcomes and positive operators whose sum is the identity. Measure the first systems , where , and condition the retained state on the observed outcomes. Write for that conditional state and for its marginal on the th retained system. The trace norm measures the error between and . The expectation is over the uniform permutation and the measurement outcomes, with their Born-rule probabilities.
The distortion with side information of a fixed measurement is the largest ratio between an input trace norm and the norm left after measuring only its factor. The input ranges over Hermitian operators on , over every finite-dimensional side system , with zero partial trace on both and . The paper's is the infimum of this distortion over all measurements on equation (10). A state two-design is a finite family of rank-one projectors whose average second tensor power is the projector onto the symmetric subspace with the normalization in Lemma D.1. The projectors give an explicit measurement with distortion at most .
The principal target is the explicit form of Theorem 2.5. For , put . With the two-design measurement, some satisfies
Here the in the expectation is the outcome string for the first members of . The same is chosen before taking that expectation. This rate is stated with its constants and its two consecutive inequalities; an existence assertion without the error bound would lose the theorem's content.
The milestone path also states the telescoping trace-norm inequality of equation (12), the measurement estimate of Lemma D.1, and the final averaged inequality on p. 11. A companion milestone treats any fixed POVM with its own distortion. That formulation captures the proof's arbitrary-measurement step without treating the infimum as if every measurement attained it.
For an arbitrary multipartite state, random ordering and conditioning give one measured prefix length at which the selected registers have small expected distance from a product. The explicit rate is polynomial in and and decays as . It therefore gives a quantitative approximation guarantee under a selection rule that can be applied without first establishing exchangeability Berta et al., §2.6.
The theorem is proved in the paper; the work here is to express its state, measurement, conditional distribution, and norm bound in Lean and to connect the estimate to reusable finite-dimensional quantum-information definitions. The local statements are currently proof obligations, not machine-checked proofs. The published density-operator, trace-norm, and partial-trace definitions are reused. Once proved, the statements can serve as a precise interface for subsequent formal work on randomized subsystem selection and information-theoretic decoupling.
Randomly choosing systems does not turn the original state into a product state. A direct bound on the distance to a product can be large even when each one-system marginal is simple, because correlations among the retained systems remain. Equation (12) breaks the total error into successive correlation terms; the paper controls their average by measuring other systems and using information-theoretic estimates. A second difficulty is that a measurement can erase distinctions between different input operators. The two-design estimate supplies a dimension-dependent bound on that loss, uniformly over the size of a side system.
The printed theorem leaves the measurement unspecified while using the minimum distortion over all measurements. A trivial measurement cannot satisfy that reading. The proof explicitly permits the measurement built from a state two-design, with replacing ; that is the measurement used in the goal proof of Theorem 2.5, p. 10.
The system has basis Fin dB; copies have basis Fin n → Fin dB. The formalization writes , assumes , and ranges over . A state is a positive semidefinite complex matrix with trace one. Permutations act on the copy coordinates, and their finite uniform average models the paper's random ordered tuples. Measurement outcomes are finite words; the conditional state divides the unnormalized post-measurement state by its probability. A zero-probability outcome uses Lean's zero inverse and contributes zero to the weighted expectation. The existence of a state and of a nonempty two-design rules out zero-dimensional and empty-outcome instances in the goal.
The fixed-measurement distortion and take values in extended nonnegative reals, so a measurement that destroys a nonzero operator has infinite distortion. The logarithm is base two except for . The definitions use the paper's unnormalized trace norm, with no factor . No mutual-information estimate or Pinsker inequality is assumed in the goal: both belong to possible proofs. Contributions proving the stated milestones, the positivity and normalization of the conditional states, or reusable trace-norm facts for finite tensor products all advance the target.
Large network games can be described by a graphon, a measurable kernel that assigns an interaction weight to each pair of players in a continuum. This representation is useful when a finite network is viewed as an approximation to a limiting network. A basic question is whether a small change in interaction weights can cause a large change in equilibrium behavior. Carmona, Cooney, Graves, and Laurière answer this question for a static game with real actions, noisy player states, and costs coupled through an aggregate state. Their static graphon games paper establishes existence and uniqueness under different hypotheses, and Theorem 3.20 gives an explicit stability estimate under its contraction condition.
The mission isolates that stability estimate and the results on which it depends. It belongs to the same development as the paper's existence theorem, but has a narrower question: how sensitively does the equilibrium respond when one graphon is replaced by another? The paper later studies finite-player approximations, for which understanding the limiting graphon game's equilibrium is useful. Those later approximation theorems are outside this mission.
The player set is with Lebesgue probability measure. Every player chooses a real action. A strategy profile assigns an action to almost every player and belongs to . Profiles that differ only on a null set represent the same strategy.
A graphon is a symmetric, real-valued, measurable, square-integrable function on . It defines an integral operator on by
Its norm is the -to- operator norm. In particular, interaction weights are allowed to be negative and are not restricted to . A second graphon has operator , and is the operator norm of their difference.
A player's state is , where is the player's action, is an aggregate state, and has a common centered probability law with finite second moment. Assumption 1 bounds squared changes in by times the squared action change plus times the squared aggregate change. For a profile , its aggregate is the solution of
Proposition 3.1 states that this aggregate exists and is unique when . This equation is the deterministic aggregate obtained from the paper's continuum model.
The expected cost of action at aggregate is . Assumption 4 says that is continuously differentiable and uniformly -strongly convex, and its action derivative changes at most when the aggregate changes. The best response minimizes this cost pointwise. A Nash equilibrium is an profile whose action minimizes for almost every player. Assumption 5 adds the uniform bound .
The first targets are the unique aggregate of Proposition 3.1, the best-response bound of Lemma 3.7, and the aggregate bound (15) of Lemma 3.16. Together these support the uniqueness condition in Proposition 3.17:
Lemma 3.19 then bounds the change of aggregate when the same profile is placed in two graphons. The goal, Theorem 3.20, concerns an equilibrium for and any equilibrium for :
Here satisfies both and (17), while is required only to satisfy . The displayed coefficient is the paper's expression, including its common factor.
The theorem gives a quantitative guarantee: as long as the original game's contraction condition holds, the distance between equilibria is controlled by the operator distance between graphons. The bound identifies how state sensitivity , cost sensitivity , strong convexity , and the state bound enter that guarantee. The result also separates two questions: whether an equilibrium exists for a changed graphon, and how far any such equilibrium can lie from the original one.
The mathematical theorem is proved in the paper; the Lean goal is open. A complete formal development would establish the integral-operator estimates, the aggregate and best-response regularity results, the unique equilibrium under (17), and finally the stability inequality. The definitions of real-valued graphons, aggregates, and their extended-valued operator norm can support later work on graphon games beyond this particular estimate. The paper's §4 finite-player results, including Theorems 4.3, 4.7, and 4.9, are not posed here.
An equilibrium is a fixed point of a response to an aggregate, so changing the graphon changes both the aggregate and the equilibrium profile. A direct comparison of costs at two equilibria does not by itself separate these effects or yield the printed constant. The aggregate is defined only as an equivalence class, while its equation and pointwise best responses use representatives. The formalization must keep those almost-everywhere statements aligned with the operator norm estimate. It must also retain the paper's asymmetric hypotheses: (17) is assumed for the original graphon, while the second graphon is allowed to have any Nash equilibrium under its own aggregate condition.
Lean uses unitInterval with its volume measure for , real actions, functions with MemLp for profiles, and almost-everywhere equality for profiles and aggregates. IsGraphon includes measurability, symmetry, and square integrability. IsAggregate records equation (6) and membership in . The integral cost is computed from , , and rather than supplied as an unrelated function. Assumptions 1, 4, and 5 are explicit; the centered noise law is part of the standing model. Lemma 3.7 is stated for an arbitrary cost satisfying Assumption 4, as on the page.
The paper defines equilibrium through a best-response map on a rich Fubini extension. Proposition 3.6 identifies that with the almost-everywhere pointwise minimization condition under Assumption 4. The mission uses that equivalent condition as its equilibrium predicate. This is a disclosed model choice because the Fubini extension itself is not formalized. A best response is selected by classical choice; Assumption 4 gives the minimizer that makes the selection meaningful.
Norm inequalities use extended nonnegative reals. For a square-integrable graphon, its operator norm is finite, and real hypotheses use that finite value. The operator norm is never a real supremum with a default value for unbounded inputs; an equilibrium always includes an aggregate; and an infinite left-side norm is never converted to zero. These choices prevent the stability claim from becoming empty at a bad input. Contributions to the integral-operator infrastructure, the existence and uniqueness of aggregates, and the five named milestones are all within scope.
First order primal–dual algorithms are used when a linear program is too large for a direct factorization or when matrix operations are cheaper than solving a sequence of linear systems. Their basic guarantees often bound an averaged duality gap by a quantity proportional to after steps. A restart discards the current inner iteration history and begins again from an averaged output. For problems with a suitable error bound, restarts can turn sublinear progress into geometric decrease in distance to the solution set. Applegate, Hinder, Lu and Lubin analyze this mechanism for a class that includes proximal point, extragradient, primal–dual hybrid gradient and ADMM methods, with constants listed in their Table 1. Their adaptive rule is useful when the sharpness constant is unavailable to the algorithm designer. Applegate et al., arXiv:2105.12715v4, §§2–4
Let and be closed convex sets. The primal–dual problem is , where is differentiable, convex in and concave in . A point is feasible when . Its saddle-point set contains the feasible pairs satisfying for every and . Distances and balls use a chosen seminorm ; this matters for methods whose natural geometry is degenerate. Applegate et al., arXiv:2105.12715v4, pp. 2–3
For , put . The normalized duality gap is . At it is the upper limit as positive radii decrease to zero. The gap can be infinite under a seminorm, so its values are extended real. A problem is -sharp on when for every and every . This condition connects a computable local gap to the distance of interest. Applegate et al., arXiv:2105.12715v4, pp. 3, 11, (4), Definition 1
The base algorithm begins at and supplies averaged outputs for positive inner times . Property 3 requires constants , uniform over every feasible start and output run, for which , , and . An outer run starts at , runs its inner algorithm for steps, and sets . Its first length is selected by the user. At later outer indices, it restarts at the first positive time when the normalized gap has fallen below times the gap at the previous outer transition, with . Applegate et al., arXiv:2105.12715v4, pp. 9–10, 15–16, Property 3, Algorithm 1, (30)
The goal is both parts of Theorem 2. Assume all outer starts lie in one set on which the problem is -sharp, with . Define the ceiling time . For every the target is
The milestones are Proposition 8's treatment of zero displacement, the displayed restart comparison in the proof of (33), the bound (33) itself, and the repeated normalized-gap inequality in the proof of part (ii). Each is tied to the arXiv version's printed page and label. The assertion begins at : the first interval is free and need not be at most . Applegate et al., arXiv:2105.12715v4, pp. 17–18
The first conclusion gives a uniform bound on the inner work of every subsequent adaptive interval. The second translates the gap-based restart rule into a geometric distance guarantee while retaining the user-selected first interval as a visible factor. Together, they explain why an algorithm that does not know can have the same characteristic restart scale as one using a fixed frequency chosen from . The paper proves this theorem and gives linear-programming settings in which its sharpness premise holds; this mission asks for a machine-checked statement and, eventually, a machine-checked proof of that known result. Applegate et al., arXiv:2105.12715v4, Theorems 1–2 and Lemma 5
Formalizing the result also produces reusable interfaces for saddle sets, seminorm distances, localized duality gaps, uniform algorithm properties, and first-trigger restart runs. Those interfaces can support other primal–dual analyses without committing to a particular inner update map. A complete proof can later connect Property 3 to the paper's individual algorithms, while this mission preserves the abstract theorem that they share. Applegate et al., arXiv:2105.12715v4, Proposition 4 and §4
The restart test uses a gap evaluated at the moving radius , whereas sharpness relates a gap at the radius of the previous outer transition to distance from . This mismatch must be reconciled while preserving the exact ceiling constant. A zero seminorm displacement is a separate boundary case: sharpness only speaks about positive radii, but the algorithm can still encounter radius zero. The theorem also needs the first qualifying time; knowing merely that a later time satisfies the test gives no upper bound on the interval length. Applegate et al., arXiv:2105.12715v4, pp. 16–18
Lean represents and by finite-dimensional Euclidean spaces and by their product, allowing either dimension to be zero. The geometry on that product is an explicit Seminorm, never the product type's default norm. is the set of saddle pairs. The standing problem predicate includes closed convex feasible sets, separate convexity and concavity, and differentiability on the whole ambient product space. It also requires , a disclosed strengthening of the paper's standing feasibility and finite-optimum assumptions so the real-valued distance to cannot collapse to an empty-infimum default. The infimum defining distance is over saddle points only; the supremum defining the gap is over feasible pairs only. The normalized gap and diameter use extended reals so an unbounded seminorm ball does not silently acquire value zero. Applegate et al., arXiv:2105.12715v4, pp. 2–4
The base method is a relation from a start to possible averaged-output sequences. Property 3 fixes before quantifying over starts, runs and positive times. The theorem assumes initial feasibility; Property 3 then makes restarted outer points feasible. An adaptive run records the positive first interval and the first qualifying positive time for each later interval. The ceiling is Nat.ceil; the factor is division in the reals. A formalization with arbitrarily chosen qualifying restart times, sharpness only along one chosen trajectory, a real-valued supremum over an unbounded ball, or a vacuous solution set would change the result. Contributions to the gap and seminorm infrastructure and to either half of Theorem 2 are useful; the individual algorithm implementations are outside this mission's core. Applegate et al., arXiv:2105.12715v4, pp. 9–10, 16–18
Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571, ICLR 2018) train classifiers against adversarial perturbations by solving a Lagrangian relaxation of a Wasserstein distributionally robust problem. The inner problem, , is strongly concave, and hence solvable by gradient ascent with the paper's certificates, exactly when the penalty exceeds the input-smoothness constant of the loss: the Lipschitz constant of . For a deep network this constant is not given; §4 of the paper ("Bounds on smoothness of neural networks") supplies an explicit upper bound in terms of the weights' spectral norms and per-layer constants of the activations. The bound tells a practitioner how large must be for the robustness guarantees to apply, and it is of the same type as the spectral-norm Lipschitz bounds used for adversarial robustness and generalization of deep networks (Szegedy et al. 2014; Bartlett, Foster, Telgarsky 2017), but at the level of the derivative rather than the function.
A layered network of depth has widths (pre-activation of layer ) and (output of layer ), with the input dimension and the number of classes. Its parameters are weight matrices , and each linear layer is followed by a nonlinear operation (an activation, possibly combined with pooling). The output of the first layers is
and its Jacobian in is . All spaces carry the Euclidean norm , and is the -operator (spectral) norm.
Assumption E. For , the map is -Lipschitz for , its Jacobian is -Lipschitz from to , and . From these constants define
The classification loss is the softmax loss with , for a class .
Under Assumption E, for every class and all inputs ,
Under Assumption E, for ,
In the order the paper's proof uses them: Lemma 6 (the chain rule for , recursively and as a product); Proposition 5, first part; the telescoping representation (34) of ; Proposition 5, second part; the softmax constants of §B.9 (gradient , Lipschitz constant , smoothness constant ); and the recursion of §B.9 for with its instance for a softmax output layer.
Corollary 4 converts the abstract hypothesis of the paper's convergence and certification results (missions 1 and 2 of this series) into a checkable condition on a trained network: , computable from spectral norms of the weights and from constants of standard activations (the paper lists average pooling, sigmoid and ELU). Proposition 5 is a reusable statement about any composition of smooth maps with linear layers, independent of the softmax and of robust optimization.
The results are proved in the paper (§B.8–§B.9). No machine-checked proof of them is known to exist. This mission produces a formal development of the input Jacobian of a layered network with varying widths, the telescoping estimate for its variation, and the smoothness constants of the softmax loss, all with the paper's explicit constants.
The function-level bound (first part of Proposition 5) is a direct induction. The derivative-level bound is not: the obvious induction on needs both a bound on , which comes from the Lipschitz half and the differentiability of every layer, and a bound on the variation of the Jacobian of the previous layers, and the two must be combined so that the constant comes out as exactly of (21), whose definition uses quotients by . For the corollary, the softmax loss must be shown to have Lipschitz constant (a supremum that is not attained) and a -Lipschitz derivative; the paper's eigenvalue argument for the latter is loose and its displayed initial condition for the recursion of the constants is misprinted, so the printed text cannot be transcribed line by line. In Lean, the widths change from layer to layer, so the network is a family of maps between different Euclidean spaces, and every product of Jacobians is a dependently typed composition.
EuclideanSpace ℝ (Fin n); weights are continuous linear maps, so ‖θ l‖ is the spectral norm; Jacobians are Fréchet derivatives with the operator norm. A Frobenius or entrywise norm would state a different theorem and is not used.l is the paper's layer (θ l, σ l, L0 l, L1 l); F l, α L0 l, β L0 L1 l carry the paper's index . Widths vary with the layer; they are not collapsed to a single dimension.Fin K; the goal uses Mathlib's gradient, whose norm equals the operator norm of the derivative.A complete development needs the chain rule for the network map, the mean value inequality for the softmax loss, and the algebra of (21). The definitions of the layered network and of the softmax loss are independent of robust optimization and are reusable for other Lipschitz and smoothness bounds of deep networks. Proofs of any milestone, and alternative arguments with sharper constants stated as separate theorems, are welcome.
An inventory policy chooses how much stock to order before demand is observed. Its quality is assessed by the holding and backlogging costs it incurs on future demand. A policy chosen to perform well on historical demand can overfit those observations. A useful statistical guarantee therefore controls the difference between historical and future costs simultaneously over the policies that the procedure may select. Xie, Ma and Xin establish such guarantees for stationary base-stock, , and nonstationary base-stock policy classes.
This formalization covers the principal bound families in that paper. Its first goal is the expected generalization and estimation bound for nonstationary base-stock policies with no fixed ordering cost, Corollary 4.10. Its supporting targets include Theorem 4.9 and the constructive product-sample partition in Lemma 4.12. The other principal bounds remain in the explicit scope below and await their own full Lean declarations. The companion inventory-information project needs these results as proved dependencies; merely citing the paper does not close that project's formal proof obligations.
There are periods, a deterministic lead time , and demand bounded by . The first order arrives in period . Average loss means the sum of holding and backlogging costs in periods , divided by the positive horizon . The initial pipeline is empty, and initial inventory is nonpositive for the base-stock models. Holding and backlogging cost coefficients are . Nonstationary base-stock policies in the first goal have no fixed ordering cost and use levels .
The Lean model indexes the first period by zero. It uses the source's explicit finite-maximum formula for post-replenishment inventory, with the demand interval summed up to, but excluding, the observation period. In mathematical notation the inventory in period is . Cost is evaluated after subtracting the current demand . This is a backlog model; applications to lost sales require a separate equivalence argument.
Data comprise IID demand trajectories from a probability measure on the bounded trajectory space. Different periods of the same trajectory can be dependent. Generalization error is the one-sided supremum , where is expected average loss and is empirical average loss. Estimation error is , for an empirical minimizer and a best-in-class population policy. It is not the error relative to every history-dependent inventory policy. These conventions follow Sections 3 and 4.
The first goal, Corollary 4.10, asserts the existence of one absolute constant such that
The constant is quantified before the horizon, lead time, support, costs, demand distribution, sample size, and policy selections. The first inequality explicitly refers to actual minimizers, with an integrable selected risk. The GE conclusion holds independently of whether a particular selector has been supplied.
Its principal complexity target is Theorem 4.9: for each relevant period and , the normalized inventory class has fat-shattering dimension at most . The Lean statement says directly that every -shattered indexed sample has cardinality at most that number. It uses the source convention of a strict upper label and non-strict lower label.
Lemma 4.12 partitions all product indices into groups of indices. Every coordinate of every group traverses the original row indices exactly once. The formal statement uses a bijection between anchor-offset pairs and complete index tuples, together with a coordinate-permutation assertion. The dimension is positive, and and are included.
The full scope also retains Theorem 4.1 and Corollary 4.2 (stationary policies), Theorem 4.4 and Corollary 4.5 ( upper bounds), Theorem 4.7 and Corollary 4.8 ( fat-shattering and GE lower bounds), and the expected Product ERM comparison in equation (4.7). They are catalogued with their assumptions but are not yet all encoded. The GE lower bound is not asserted to be a minimax policy-regret lower bound.
The nonstationary policy vector grows with the horizon, while the expected average-loss bound has no horizon factor. A verified version supplies a reusable statistical ingredient for finite-horizon inventory learning. Total-cost bounds require multiplication by the horizon. Absolute uniform deviation, period-dependent costs, high-probability statements, initial-state reductions, and censoring require further bridge theorems. They are not attributed to Corollary 4.10 without those proofs.
The cyclic partition has a complete locally checked Lean proof with axiom dependencies only propext and Quot.sound. The two statistical targets remain open. Neither a drafted declaration nor a local proof is described as a server-verified contribution.
Ordinary pseudodimension can grow with the horizon for the nonstationary class, so it does not by itself give the desired horizon-free rate. A full proof needs scale-sensitive complexity, probability, and integration infrastructure. For Product ERM, coordinate independence must be explicit: the groups in the partition need not be independent of each other. The expected comparison transfers upper bounds; it cannot reverse direction to transfer a GE lower bound.
The shared environment is Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Demand and policy coordinates are bounded real subtypes with their usual measurable structures. Probability is over IID whole trajectories. Finite maximum indices are nonempty. Positive prevent zero denominators in the targets. General definitions remain total, and their behavior outside these hypotheses is exposed in the independent read-backs.
Complete proofs must establish the boundedness and measurability needed for the real suprema and integrals to have their usual meaning. They may not assume the convergence bound, replace arbitrary probability measures by finite-support distributions, or silently restrict the policy class. The branch additionally needs explicit unbounded-domain conventions when holding or backlogging costs vanish. Reusable contributions include shattering, symmetrization, entropy bounds, selection and integrability facts, and finite-product sampling.
Large data sets make clustering and subspace fitting expensive because a candidate solution must be evaluated against every input point. A dimensionality reduction replaces the data by a lower-rank matrix whose costs approximate those of the original input for an entire class of candidate solutions. Feldman, Schmidt, and Sohler study reductions that retain enough information for -means, principal component analysis, and projective clustering. Their journal paper identifies a rank truncation and one residual scalar that preserve the fitting cost of every shape lying in a low-dimensional linear subspace Feldman, Schmidt, and Sohler (2020), Theorem 22.
The published article also records that some coreset sizes in its 2013 conference version were incorrect. This mission uses the 2020 journal statement and its page numbering throughout. The authors cite earlier SVD-based approximations to -means on p. 613, while their Theorem 22 gives a uniform cost guarantee for arbitrary nonempty shapes contained in a -dimensional subspace Feldman, Schmidt, and Sohler (2020), pp. 603, 613, 620.
The input is a real matrix . Its rows are points in . For a nonempty set of candidate locations or shapes , let be the infimum of Euclidean distances from row to points of . The shape cost is
The set need not be closed and need not be a subspace. For example, it can be a finite set of cluster centers. The restriction is that all of its points lie in some linear subspace of dimension . This matches the paper's shape class in §5; the affine case is treated separately Feldman, Schmidt, and Sohler (2020), pp. 619–620.
Fix a singular value decomposition , where and are orthogonal and the diagonal entries of the rectangular matrix are nonnegative and nonincreasing. The entry is indexed from one. The rank- truncation keeps the first diagonal entries and sets the rest to zero. Its squared Frobenius residual is . The corrected cost of is Feldman, Schmidt, and Sohler (2020), Definition 1 and §2.
The milestones first record the matrix Pythagorean identity, the projection and residual bounds, and the lower bound on the cost of a linear -subspace. They then state the residual-corrected approximation in Corollary 16:
Here has orthonormal columns spanning the complement of the candidate subspace. Corollary 20, Corollary 21, and display (9) connect these linear estimates to costs of general sets Feldman, Schmidt, and Sohler (2020), pp. 604, 613–615, 619–620.
The goal is Theorem 22. For , , and , every nonempty contained in a linear -dimensional subspace satisfies
The quantifier over makes this a guarantee for every admissible candidate on the same reduced data, rather than a statement about one selected optimum Feldman, Schmidt, and Sohler (2020), Theorem 22, p. 620.
The theorem preserves objective values after replacing by a rank- matrix and one number. For a fixed and accuracy parameter, the rank threshold depends on and , with no direct dependence on the number of points or ambient dimension except the upper bound on feasible . In the paper, the result leads to a guarantee for -means candidates, since centers span a linear subspace of dimension at most Feldman, Schmidt, and Sohler (2020), Corollary 23, p. 621.
The result is proved in the paper, but this mission's Lean theorems are posed with sorry; they do not yet have machine-checked proofs. A completed development would connect a reusable rectangular SVD model, matrix projection identities, infimum distances to arbitrary nonempty sets, and a uniform cost inequality. The SVD definition is already published in the platform library; the row-cost and singular-value conventions here supply the interface needed for this paper Feldman, Schmidt, and Sohler (2020), §§2, 3, 5.
The linear subspace bound compares a projection cost with a tail sum of squared singular values. The paper recalls that fact in §3 without proving it, so the formal development needs a suitable singular-value inequality or a derivation from existing matrix approximation results. For general shapes , a bound on the cost of one linear subspace does not by itself control the distance from each projected point to every point of . The remaining milestones state the projection error, the squared-distance perturbation bound, and the Pythagorean cost split that address that gap Feldman, Schmidt, and Sohler (2020), pp. 613, 619–621.
The proof printed after Theorem 22 invokes earlier corollaries under a stronger rank threshold than the theorem states. The mission keeps the printed theorem threshold, whose claim remains valid; a formal proof must bridge that discrepancy Feldman, Schmidt, and Sohler (2020), pp. 620–621.
Matrices are Matrix (Fin n) (Fin d) ℝ, and rows are points of EuclideanSpace ℝ (Fin d). Squared Frobenius norm is an explicit finite sum of squared entries. Shape cost sums squared Metric.infDist values over rows. Since Mathlib assigns a real default value to distance from the empty set while the paper assigns infinity, every theorem about a general shape requires C.Nonempty. This is the page's own requirement for Theorem 22 and Corollary 21, and is also needed for display (9).
The SVD and its truncation use the published ProjLikeRetr.FixedRank.IsSVD and truncSVD. Every SVD statement quantifies over an arbitrary valid triple ; tied singular values do not fix a unique truncation. The local is one-based, while truncSVD m keeps zero-based diagonal positions below . Orthonormal columns of satisfy , their orthogonal complement has columns, and projection in ambient coordinates is . Theorem 22 quantifies over arbitrary nonempty contained in a linear -subspace; it does not restrict to subspaces or replace linear containment by affine containment.
The integer inequalities in Lean use additive forms such as to avoid truncated natural-number subtraction. The theorem retains the printed threshold, including the proof gap described above. Running-time clauses are outside the mission's mathematical statements. Contributions are welcome toward the singular-value lower bound, the projection and infimum-distance identities, and the final uniform inequality; the matrix and distance definitions are reusable in the companion affine-subspace mission.
Many problems in quantum information theory ask for the maximum of a linear functional over pairs of quantum states, one on each of two systems, subject to linear constraints on each state. The best success probability of an approximate quantum error-correcting code of given size is of this form: the encoder and the decoder are quantum channels, their Choi matrices are states with fixed marginals, and the objective is bilinear in the two (Berta, Borderi, Fawzi & Scholz, arXiv:1810.12197, §4). Such constrained bilinear programs are nonconvex. Seesaw methods give lower bounds that often converge in practice, but they offer no guarantee of global optimality. What is needed is a hierarchy of efficiently computable outer bounds that converges to the optimum, with an explicit rate.
For the unconstrained problem, the optimisation over separable states, such a hierarchy is classical: the Doherty–Parrilo–Spedalieri hierarchy of -extendible states, whose convergence follows from finite quantum de Finetti theorems (Christandl, König, Mitchison & Renner 2007; Brandão & Harrow 2013). The standard de Finetti approximant is, however, a mixture of product states that need not satisfy the linear constraints, so it says nothing about the constrained problem. The paper proves a de Finetti theorem with linear constraints (Theorem 2.3) and derives from it a semidefinite hierarchy for constrained bilinear programs with a convergence guarantee (Theorem 3.1).
A -dimensional quantum system has operator space ; a state is a positive semidefinite with . Let and be systems of dimensions and . The data are an objective , arbitrary linear maps and , and matrices , . The constrained bilinear program is
For let be copies of . A state on is symmetric with respect to if it is invariant under every permutation of the copies , . Write , and . The level- program is
It is a semidefinite program of size polynomial in and .
The rate involves the trace norm , the Schatten -norm (largest singular value), and the minimal distortion with side information of ,
the infimum over measurements on and the supremum over all finite-dimensional ; is the analogue with product measurements . Throughout, is base 2.
The page states with . The goal makes explicit the rate the proof gives.
Theorem 3.1 turns a nonconvex problem into a sequence of semidefinite programs whose values decrease to the optimum at rate , with a constant that depends polynomially on and logarithmically on . Every level is a certified upper bound; together with any feasible point it brackets . The same argument applied to channel fidelities gives converging outer bounds on the success probability of approximate quantum error correction (§4 of the paper), and the constrained de Finetti theorem is the key step there as well. Theorem 2.3 is of independent interest: it is the first finite de Finetti theorem in which the approximating separable state inherits linear constraints of the extension.
The results are proved in the paper; none of them has been machine-checked. A complete formalization requires the quantum relative entropy and mutual information with their chain rule, the quantum Pinsker inequality, state two-designs and their existence, and a weighted Hölder inequality for Schatten norms; most of this is absent from Mathlib, and each piece is reusable beyond this mission.
The obvious route measures every copy with a fixed informationally complete measurement and uses the resulting classical de Finetti statement. This approximates by a mixture of product states, but the states in the mixture need not satisfy , and projecting them onto the constraint set destroys the error bound. The paper instead conditions on the outcomes of only copies and keeps quantum; the constraint on then transfers to the conditional state of by symmetry. Making this rigorous needs the chain rule of conditional mutual information with classical conditioning, and the distortion of the measurement must be bounded independently of the side system , which is what Lemma D.1 provides. The Schatten-norm estimate there is elementary but requires a weighted Hölder inequality and a careful choice of weight.
Systems are finite index types: is indexed by Fin dA × (Fin N → Fin dB), is Mathlib's Kronecker product, and the permutation action permutes the word in Fin N → Fin dB. States, trace norm and partial traces are the published definitions WildeQIT_IsDensityOperator, WildeQIT_traceNorm and WildeQIT_partialTrace. The linear maps , are arbitrary -linear maps (not assumed positive or trace preserving), applied blockwise to one tensor factor. The objective is the real part of , equal to for Hermitian . Each "max" is the supremum of the set of objective values over the feasible set, never over all matrices. Wherever the page has copies of , the Lean has n + 1: SDPval … n is the page's , and the bounds have denominator . The distortions and take values in ; the standalone bound on assumes .
No feasibility hypothesis is added to the goal. The feasible sets of and of every level are empty or nonempty together, and the empty case reads . The goal mentions only , , , , and ; a formalization in which or were free real numbers, or in which the de Finetti mixture was not required to satisfy the constraints, would be a different and much weaker statement.
Contributions are welcome at every milestone, and especially in the reusable infrastructure: quantum relative entropy and mutual information on matrices, the quantum Pinsker inequality, unitary and state designs, and Hölder inequalities for Schatten norms.
Online sellers of loans, insurance, travel and retail goods observe data about each arriving customer before quoting a price. Using that data to price individually is attractive only if the seller can learn, from its own sales, how demand responds to price for customers with given characteristics. Two features make this hard in practice. The number of recorded characteristics is often large, possibly larger than the selling horizon , while only a few of them matter. And price sensitivity is itself heterogeneous: different customers respond to the same price change differently.
Ban and Keskin (Management Science 67(9), 2021) model both features and ask how fast the revenue lost to learning can grow. Their answer is that a seller who learns with lasso-regularized quasi-likelihood estimation and occasional price experiments loses revenue of order up to logarithmic factors, where is the number of relevant characteristics, and that no policy can do better than order . This mission formalizes the upper bound for the general (nonlinear-link) model with unknown sparsity, Theorem 3 of the paper.
In each period a customer arrives with a raw feature vector . The are i.i.d., take values in a compact set inside a ball of radius , have mean zero and positive definite covariance . The seller sees the augmented vector , charges a price with , and observes the demand
Here is an unknown parameter in a compact rectangle , the link is known, differentiable and increasing with on the relevant domain, and the demand shocks form a sub-Gaussian martingale difference sequence. The term is the customer's own price sensitivity. With the argument of is .
The sparsity of is , . The seller does not know .
The expected revenue of price is , and the clairvoyant price maximizes it; it is assumed to lie in the interior of for , . The regret of a policy over periods is
The policy ILQX charges the experimental price in periods and in periods , and otherwise charges , where maximizes the lasso-penalized quasi-likelihood
over the experimental periods (), and is the projection onto . The regularization level is for a constant .
There is a finite constant such that
is fixed with the model and is uniform over ; since varies over , the factor carries content.
Theorem 3 says that a seller facing many potentially relevant customer characteristics, without knowing which matter and under a nonlinear demand link such as logit, loses revenue at a rate governed by the number of relevant characteristics and only logarithmically by the total number . Combined with the paper's lower bound (Theorem 1, for the linear model), it makes ILQX first-order optimal up to logarithmic factors. An unregularized policy would pay order , which is linear in when exceeds .
The paper's proofs are in its electronic companion, which this mission does not reproduce; no machine-checked version of the result exists. A complete formalization would also produce a reusable high-probability error bound for lasso-regularized quasi-likelihood estimation under adaptively collected data (Lemma 3), and a machine-checked model of feature-based dynamic pricing on which related policies can be stated.
The estimation error must be controlled on data collected by the policy itself. The design vectors use only two prices, so the information about the price sensitivity accrues only from the experimental periods. Standard lasso error bounds assume a fixed or i.i.d. design and a restricted-eigenvalue condition on it; here a restricted-eigenvalue-type property of the random Kronecker design must be derived from and , and the noise enters through a martingale whose conditional law may depend on past prices. The quasi-likelihood is not a least-squares objective, so the curvature comes from the bounds , which hold only on the bounded domain and not at an unconstrained estimate. Finally, the regret bound has to turn a squared-error bound holding with probability into an expected revenue loss, which requires the revenue loss to be second order in the parameter error at an interior optimum.
Fin (d+1) → ℝ with the intercept at index 0; is Fin 2 × Fin (d+1) → ℝ with , . Periods are 1-based. .Contributions welcome: existence of a measurable maximizer of the objective, the counting lemma, and supporting lemmas for Lemma 3 and the regret bound.
Linear programs at very large scale are increasingly solved by first-order primal-dual methods, which use only matrix-vector products instead of matrix factorizations. Such methods parallelize well and have a small memory footprint, but on their own they are slow to reach moderate or high accuracy. Applegate, Hinder, Lu and Lubin (arXiv:2105.12715, Math. Program. 2022) showed that periodically restarting a primal-dual method from the average of its iterates turns its sublinear ergodic rate into a linear rate on sharp problems, a class that contains every linear program. The analysis underlies PDLP, a restarted PDHG solver studied computationally by Applegate et al. (arXiv:2106.04756) and shipped in Google OR-Tools.
This mission formalizes the paper's first convergence theorem: with restarts at a fixed frequency, the distance from the restart points to the solution set shrinks by a factor per restart.
Let and be closed convex sets and let be differentiable, convex in and concave in . Problem (1) is
with feasible region and primal-dual points . Its solution set is the set of saddle points : for all , . Throughout, .
Distances are measured in a semi-norm , which the paper allows in order to cover ADMM. Write , , and . The primal-dual gap (3) at is , and the normalized duality gap (4a)–(4b) is
By Definition 1, problem (1) is -sharp on if for all and all .
The base method is abstract. From a start it outputs averaged points , . It has Property 3 with constants if, for every start and every , and
i. ,
ii. .
Algorithm 1 with fixed-frequency restarts (29) runs the base method from for
steps, sets , and repeats, with .
If the base method has Property 3 and (1) is -sharp on with , then for every
Proposition 2 (p. 8) and Proposition 4 (p. 10) show where Property 3 comes from. A generic algorithm (6) with iterates and targets has Property 1 with if for every (12). It has Property 2 with if or .
Fact 1 (p. 11), that is non-decreasing in , is included as well.
Theorem 1 converts any primal-dual method with an ergodic rate on the normalized duality gap into a linearly convergent method on sharp problems. The rate is iterations to reach (Remark 3). Through Proposition 4 it applies to PPM, EGM, PDHG and ADMM. Combined with the paper's Lemma 5, which shows that linear programs are sharp with the inverse of a Hoffman constant, it yields linear convergence of restarted PDHG for LP. The paper also shows that this rate matches a lower bound for a general class of primal-dual methods.
The result is proved in the paper. As far as is known, no part of it, and no normalized duality gap or primal-dual sharpness notion, has a machine-checked proof. The mission adds a checked version of the restart argument, with every degenerate case resolved: zero displacements, unbounded balls, and semi-norms that are not norms.
Each proof is short, but the statements are delicate in ways the paper passes over.
A direct contraction argument that applies sharpness at an arbitrary radius, or on all of , does not prove the theorem as stated.
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). and are allowed.Seminorm ℝ on their product, never the product's built-in norm.EReal, so unbounded sets give and not a junk . is a real infimum over the nonempty set .Standing assumptions and added hypotheses:
Departures from the page:
The goal is not trivialized by its hypotheses. A companion check file exhibits on , with the sup norm and an oracle base method, on which every hypothesis of Theorem 1 holds and . Sharpness is assumed only where Definition 1 and the theorem assume it: replacing by , or the radius range by all , would weaken the theorem.
A complete development needs elementary facts about suprema in EReal, Jensen's inequality for convex-concave functions on averages, and geometric sums. The definitions of , sharpness and Property 3 are reusable for the adaptive-restart theorem of the same paper (Theorem 2, a separate mission) and for other restart analyses. Proofs of any milestone or companion are welcome.
Posted prices turn an offline allocation problem into a sequential choice process: each agent sees a menu of outcomes and prices, then chooses an outcome without revealing its full valuation. The balanced prices framework of Dütting, Feldman, Kesselheim, and Lucier gives welfare guarantees by comparing the revenue collected from an allocation with the welfare that remains feasible after it. Its appeal is that the comparison can be checked in a deterministic full-information setting before any probability distribution over valuations enters the analysis. Dütting et al., 2020
One valuation class at a time would make that framework difficult to reuse. Combinatorial auction valuations are often built by taking pointwise maxima of simpler valuations or by adding values from separate markets. Section 5 of the paper asks whether a price construction balanced for the simple class remains balanced after these operations. Theorem 5.3 gives the maximum closure result; Theorem 5.4 gives addition across markets. Appendix B extends both to the weaker balancing condition used elsewhere in the paper. Dütting et al., 2020, §5 and Appendix B
There are agents in a fixed order. Agent receives an outcome from a space containing a null outcome. A profile is feasible when it lies in . The model assumes downward closure: removing the outcomes of any group of agents from a feasible profile keeps it feasible. For a set of agents , write for the profile retaining on and assigning the null outcome elsewhere. The prefix retains only the agents before . Dütting et al., 2020, §2
A valuation profile assigns each agent a function . The welfare of is . Every base valuation takes values in , the normalization stated in §2. For any set of profiles, denotes the best welfare achievable in . An allocation rule ALG chooses a feasible profile from a valuation profile. A pricing rule assigns a nonnegative, possibly infinite price to outcome when the partial profile is ; an infeasible extension has infinite price. Dütting et al., 2020, pp. 547–548
An exchange-compatible family specifies a set of comparison profiles for each profile . It is exchange compatible when replacing any one coordinate of by the corresponding coordinate of any gives a feasible profile. This property is required for every in the full outcome space. A rule is -balanced for valuation , ALG, and that family, for constants and (Definition 3.1), when both inequalities hold for every feasible and every :
The maximum extension of a base valuation space consists of nonempty finite pointwise maxima of elements of . A base profile supports an extended profile at if at every outcome and for every agent. ALG is consistent when whenever supports at . The optimal allocation rule has this property by Lemma 5.2. Dütting et al., 2020, p. 554
The goal is Theorem 5.3. Given one exchange-compatible family and a collection balanced for every base profile, consistency of ALG preserves the same constants for every extended profile and every corresponding supporting base profile:
The milestone list records the welfare supremum comparison and the two price inequalities in the paper's proof. The family remains the same for all base and extended profiles. Dütting et al., 2020, Theorem 5.3 and proof
Theorem 5.4 treats separate allocation problems. The joint outcome and feasible set are products; values and prices add across components; ALG applies each component's rule. It asserts balancedness with the same and . Appendix B changes the second balancedness bound to and requires strong consistency for maximum closure. Theorems B.2 and B.3 preserve under maxima and addition, respectively. Dütting et al., 2020, Theorems 5.4, B.2, B.3
The maximum closure theorem lets a balanced-price construction for a simple valuation class cover finite maxima of that class without worsening its balancing constants. The addition theorem lets separately priced markets be combined by summing prices. Together these two operations account for the XOS composition discussed immediately after Theorem 5.4; the paper uses the results to connect its general framework to combinatorial auctions and multidimensional matroid settings. Dütting et al., 2020, p. 555
These results have paper proofs. The work here is to state their exact deterministic content in Lean so later formalizations of the price constructions can import the closure theorems. The definitions of supporting valuations, exchange-compatible families, and extended-real prices are reusable beyond this mission. The companion statements keep the product-market and weak-balancedness variants alongside the central theorem, while their proofs remain to be formalized.
For maximum closure, the prices are indexed by a base profile but must be balanced for a different profile that is pointwise larger. A supporting profile agrees with only at ALG's outcome , while condition (a) refers to , an outcome ALG chooses for a different input, and both conditions refer to optimal welfare over , where and can differ. Balancedness of for therefore says nothing about on its own; without a hypothesis tying ALG's choices for and together the statement is false, which is why consistency (Definition 5.1) is part of the theorem. The formal statement must keep the real-valued optimum meaningful for maxima of base valuations, so the normalization of §2 is carried through to . Dütting et al., 2020, Definition 5.1 and Theorem 5.3
For addition, a direct product of the component comparison families has an edge case: a component family can be empty while another is nonempty. The paper's displayed product family then makes the lower balancedness inequality too strong. The theorem statements ask for an exchange-compatible family to exist, as the printed theorems do; they do not require that failing product family. This discrepancy is recorded for review. Dütting et al., 2020, proof of Theorem 5.4
Agents and markets use zero-based finite indices; the paper writes agent indices from one. A profile's prefix contains exactly the agents with smaller indices. Valuations are functions to with base values in . The maximum extension uses a nonempty finite set of base functions, so its maximum is defined at every outcome. Optimal welfare is a real supremum; bounded valuations keep it finite, and the empty set has value zero. Prices are extended nonnegative reals so is retained. The lower balancedness inequality embeds its real right side using ofReal, which handles a negative lower bound consistently with nonnegative prices. The upper inequality keeps the price sum in extended reals.
The maximum theorem quantifies over every extended profile and every supporting base profile, including genuinely new maxima. It keeps one exchange-compatible family for all valuations. The maximum-closure theorems require every base price to satisfy the pricing-rule condition and conclude it for the supporting price. ALG feasibility is assumed on , which contains the base profiles. The product theorems construct joint outcomes, additive values, componentwise ALG, and summed prices from the component data; they do not admit an unrelated joint allocation rule. Downward closure and a zero price for the null outcome at feasible partial allocations are included for the product statements. The latter is a disclosed assumption satisfied by the paper's pricing examples and needed to handle empty component families. No distribution or posted-price run is part of this deterministic mission. Lemma 5.2 and the strong-consistency companion take an optimal rule to be one that attains the welfare supremum over on every profile in , the profiles to which Definitions 5.1 and B.1 apply it; the product companions additionally conclude that the summed prices form a pricing rule (infinite off ). Their ALG feasibility premise concerns the component profiles supplied in the theorem.
The development needs finite dependent products and sums, finite maxima, real suprema of bounded sets, and extended nonnegative arithmetic. Contributions proving the three maximum-closure milestones, the goal, or the product-market companions are all within scope. A proof that specializes the supporting profile to would lose the intended maximum extension and does not satisfy the goal's universal quantification.
An online player repeatedly chooses a subset of coordinates and pays the sum of their losses. In many applications the player sees only that sum, not the losses of the selected coordinates. This bandit feedback makes it harder to identify which coordinate within each chosen subset is responsible for a favorable or unfavorable outcome. Audibert, Bubeck and Lugosi studied how this information limit changes regret in online combinatorial optimization. Their Theorem 5 establishes a lower bound that scales linearly with the number of selected coordinates and with the square root of the ambient dimension and horizon. Audibert, Bubeck and Lugosi, 2013, pp. 13–14
The result is part of a comparison among full-information, semi-bandit and bandit feedback in the same action model. Under full information the player sees the complete loss vector after each round; under semi-bandit feedback the player sees losses at selected coordinates; under bandit feedback the player sees only one scalar. The paper proves upper bounds for semi-bandit play and a bandit lower bound. The latter is the target of this mission. Audibert, Bubeck and Lugosi, 2013, pp. 2–3, 14
Fix a dimension , a horizon , and a finite nonempty set . Each action has exactly entries equal to one. At round , the player selects a probability distribution on , draws an action , and simultaneously an adversary selects a loss vector . The player pays the scalar . In the bandit protocol, that scalar is the only new information made available for the next round. A player strategy can use every previous action and observed scalar loss, and can randomize at every round. Audibert, Bubeck and Lugosi, 2013, pp. 2–3
The paper measures performance by pseudo-regret against the best fixed action in expectation:
The expectation covers the player's randomization and, when present, the adversary's randomization. This benchmark chooses one action for the whole horizon after comparing expected cumulative losses. It is the sole notion of regret used in the paper. Audibert, Bubeck and Lugosi, 2013, p. 2 and footnote 1
For the lower bound, the appendix arranges the coordinates as parallel games with choices per game. An action selects one coordinate from each game. The adversary can associate a favoured choice with each game and assign independent Bernoulli losses whose means are at the favoured coordinates and elsewhere. The player still sees only the sum of the selected losses. These are the -adversaries that underlie the milestone statements. Audibert, Bubeck and Lugosi, 2013, pp. 16–17
The goal is Theorem 5 with the divisibility condition used by its appendix construction. For and , there is an action set such that every bandit strategy faces some bounded loss law with
The order of the choices is part of the claim: the action set is fixed first; then each player strategy may face its own adversary. The lower bound retains the paper's explicit constant . Audibert, Bubeck and Lugosi, 2013, p. 14, Theorem 5; p. 16
The milestones follow the appendix's stated results: Lemma 5 bounds a logarithm; Lemma 4 and its corrected second case bound the divergence between sums of independent Bernoulli variables; the one-round observation bound and the horizon bound control information revealed by bandit feedback. Equations (9), (10), and (11) connect that information to expected regret and symmetry. The final averaged bound on the chance of selecting a favoured choice closes the path to the goal. The milestones are stated for deterministic players, as in the first three steps of the appendix; the passage to randomized players (the appendix's fourth step) is part of the goal's proof and is not a separate milestone. Audibert, Bubeck and Lugosi, 2013, pp. 17–18, 20–21
The theorem prevents a uniform regret guarantee of smaller order than for this bandit action model. It shows that aggregating selected losses into a single observation imposes a cost beyond what a player can avoid by choosing a different randomized strategy. In particular, the quantifier over every strategy makes the claim about the feedback model, rather than about one named algorithm. The paper proves the result in Appendix B, with the Bernoulli-sum estimate in Appendix C. Audibert, Bubeck and Lugosi, 2013, pp. 14, 16–18, 20–21
The formalization work is to prove the existing paper result in Lean from a finite protocol that represents all behavioural player strategies, together with the finite laws of the appendix's adversaries. The resulting definitions of action paths, scalar observations, finite probability laws, and divergence estimates can support other finite-horizon bandit lower bounds. These statements are drafted as open Lean theorems; compilation checks their types, while proofs remain for solvers. The paper's mathematical proof does not itself constitute a machine-checked proof.
A scalar bandit observation sums losses from several games. The player cannot separate the contribution of the favoured coordinate in one game from the other selected losses by inspecting that observation. A bound for the divergence of a single Bernoulli variable therefore does not directly bound the information available to the player. The appendix's central estimate concerns sums of independent Bernoulli variables, followed by the law of the whole sequence of scalar observations. Audibert, Bubeck and Lugosi, 2013, pp. 16, 18, 20
There is also a correction to make explicit. Lemma 4 is false for some parameters allowed by its printed statement: taking , , and violates the displayed bound. The error is in the second case of its proof, which applies Lemma 5 outside its range when . The mission states Lemma 4 with the additional condition , which holds whenever , and states the corrected second case separately: for , . Through the corrected case, the one-round bound used by the goal holds for the full range , so Theorem 5 and its constant are unaffected. Audibert, Bubeck and Lugosi, 2013, pp. 20–21, Lemmas 4–5
Actions are functions constrained to zero or one, with coordinate sum . Coordinates and rounds are indexed from zero. A behavioural strategy maps every history of chosen actions and real-valued observed losses to a probability distribution on the finite action set. Its domain includes every real history, even though the appendix's particular Bernoulli adversaries generate integer observations. The strategy may randomize; restricting the goal to deterministic players or allowing it to inspect an unobserved loss vector would change the game.
The goal's exhibited adversary is an oblivious, finitely supported probability law on loss sequences in . It belongs to the broader adversary class of the paper, so this existential formulation is stronger. All expectations are finite sums. The regret comparator is a minimum over the nonempty action set, not a default value assigned to an empty set. The action set has binary entries and equal coordinate sums, and every loss lies in the unit interval; these clauses rule out trivial lower bounds from malformed actions or unbounded losses.
The hypothesis is added to the printed theorem because Appendix B assumes it to partition coordinates into equally sized games. When , it forces and the claimed lower bound is zero. The milestone model uses functions with , deterministic players, finite Bernoulli product laws, and a finite real KL sum. Its log ratios are meaningful on the common support ensured by the stated parameter bounds. Reusable contributions include the finite bandit protocol and observation laws, as well as proofs of the KL and averaging milestones.
A partially observable Markov decision process describes a controlled system whose state is hidden but whose observations are available to a decision maker. The distribution of the hidden state conditional on the observations is the belief state. Replacing the hidden state by this distribution turns the model into a fully observed decision process, provided the resulting belief transition has the regularity needed by the usual existence and dynamic programming results. Feinberg, Kasyanov, and Zgurovsky give sufficient conditions for that regularity in their study of total-cost POMDPs, Theorems 3.6 and 3.7.
Their observation-kernel condition is continuity in total variation. Example 4.1 of the same paper tests its sharpness: the authors construct a two-state model with setwise-continuous observations for which the belief transition fails to be weakly continuous. This matters when selecting assumptions for a POMDP theorem. Setwise convergence already requires convergence of the probabilities of every fixed observation event, so it can look adequate for belief updates. The example shows that it is still too weak for the stated conclusion.
The hidden state space is and the observation space is with Lebesgue probability measure . The action space is , equipped with the topology inherited from . The state does not move: its transition law is the point mass at for every action. Its continuity in total variation is immediate from this fixed-state behavior.
At hidden state 1 the observation law is always . At hidden state 2, action zero also produces . Under action , state 2 produces a law . The density equals zero on the open left half of each cell in the -part dyadic partition and equals two elsewhere, including the cell endpoints. Equation (4.1) gives the exact intervals. These laws oscillate more rapidly as grows, and the paper establishes for every fixed Borel set . Thus the observation kernel is setwise continuous even at the accumulation action zero. Example 4.1, pp. 13–14.
A belief assigns a probability to each hidden state. For a current belief and an action , the joint law covers the next state and its observation, and is the observation marginal. A filter is a conditional law of the next state given observation : it satisfies the disintegration identity (3.3). The belief transition is the law of the random posterior when has law . These objects are defined in (3.1)–(3.5) of the paper. Different versions of agree only almost everywhere for each current belief and action, yet they yield the same belief transition.
At the uniform belief , action zero reveals nothing, while every positive-index action produces the same two-point posterior law:
The mission's goal asserts that is total-variation continuous, is a setwise-continuous probability kernel, a valid filter exists, and the positive-index laws fail to converge weakly to the zero-action law as . It states the failure for every filter satisfying (3.3), so it is a property of the POMDP rather than of a selected version of its conditional distribution. The milestone list follows the paper's assertions: setwise convergence of the dyadic laws, setwise continuity of , the two posterior values almost everywhere, and the explicit laws of .
The example identifies a precise boundary of the sufficient condition in Theorems 3.6 and 3.7. Those theorems use total-variation continuity of the observation law to obtain a weakly continuous belief transition; replacing that premise by setwise continuity makes their continuity conclusion false in this model. The explicit law also shows the size of the discrepancy: the positive-index belief transition has two fixed atoms, while the zero-action transition is concentrated at the original belief. Example 4.1, pp. 13–14.
A machine-checked development would add reusable definitions of sequential kernel continuity, the joint state-observation law, conditional filters, and the belief transition on the Borel space of probability measures. It would also formalize a concrete setwise-convergent sequence of densities whose induced posterior laws do not converge weakly. The paper proves the example; the Lean statements in this proposal are open proof targets, with no completed machine-checked proof claimed here.
Setwise continuity controls for each fixed Borel set . A posterior is a probability measure determined by the observation, and the belief transition tests the distribution of those posterior measures. The observation regions distinguishing the states change with , so convergence on fixed observation sets does not imply convergence of their posterior distributions. This is the gap in the immediate argument that tries to pass from setwise convergence of to weak convergence of .
The conditional filter adds a second precision issue. Equation (3.3) determines its values only almost surely under the observation marginal, and different versions may disagree on null observations. Any claim about a posterior value at every would exceed the source; the posterior milestone therefore has an almost-everywhere qualifier, while the goal quantifies over every valid version of .
Lean represents by Fin 2, with 0 for the paper's state 1 and 1 for state 2; by unitInterval; and by the specified subtype of . Positive integers are a subtype of , so the density and the action are never evaluated at . The measure is volume on unitInterval, which has total mass one. The density follows (4.1) literally, with open zero intervals and density two at their endpoints. The general transition and observation law use Mathlib kernels; the example instantiates them directly. The goal includes the probability-kernel property of the concrete and existence of a valid , guarding the universal filter clause against vacuity.
Weak, setwise, and total-variation convergence are sequential, as on page 4. The weak test class consists of bounded continuous real functions; the setwise test class consists of all Borel sets. The target space of carries the Borel σ-algebra of the weak topology on , stated explicitly because Mathlib's default measurable structure on that type is the Giry σ-algebra. The filter predicate requires measurability in for fixed in both structures. Joint measurability in is described in the paper but is not encoded in this local predicate; only the fixed-parameter property is used by (3.3) and (3.5). This choice and its quantifier effect are recorded in the moderation notes.
No cost, initial observation kernel, initial prior, or discount factor enters Example 4.1. Contributions on the dyadic law, kernel continuity, conditional posterior values, and the resulting belief-law identity are all within scope. A filter hard-coded to return the prior belief, a discrete topology on , or a claim for only one version of would change the counterexample and is excluded by the definitions and goal.
A partially observable Markov decision process (POMDP) models a controller that cannot see the state of the system it steers, only noisy observations of it. Inventory control with unrecorded demand, machine maintenance with imperfect inspection, and target tracking from sensor readings all have this form. The standard way to solve a POMDP is to replace it by its belief MDP, also called the completely observable MDP (COMDP): the state becomes the posterior distribution of the hidden state given everything observed so far. The belief MDP is fully observed, so the theory of Markov decision processes applies to it, but only if the belief MDP satisfies that theory's hypotheses. For MDPs with Borel state and action spaces, unbounded costs and possibly noncompact action sets, the hypothesis that yields optimality equations, convergence of value iterations and stationary optimal policies is Assumption (W*) of Feinberg, Kasyanov and Zadoianchuk (Math. Oper. Res. 2012): the cost is -inf-compact and the transition probability is weakly continuous.
Before Feinberg, Kasyanov and Zgurovsky (arXiv:1401.2168v2, published in Math. Oper. Res. 41(2), 2016), sufficient conditions for the belief MDP to be weakly continuous required a weakly continuous filter (Hernández-Lerma, 1989, as recalled on p. 11 of arXiv:1401.2168v2), a condition that fails in many natural models. The paper replaces it by a condition on the primitive data of the POMDP.
Let (states), (observations) and (actions) be Borel subsets of Polish spaces. Let be the transition kernel on given , the observation kernel on given , and a Borel one-step cost bounded below. is the set of probability measures on with the topology of weak convergence ( for bounded continuous ). A sequence converges setwise if for every Borel , and in the total variation if over Borel with values in . A kernel is weakly (setwise, total-variation) continuous if implies the corresponding convergence of the measures.
For a belief and an action , let be the joint law of the next state and observation (3.1), and its observation marginal (3.2). A filter is a kernel with (3.3): is the posterior after observing . The belief MDP has state space , action set , cost (3.8), and transition , the law of when (3.5). A cost is -inf-compact on if its restriction to has compact level sets for every compact .
If either Assumption (D) () or Assumption (P) ( and ) holds, is bounded below and -inf-compact on , is weakly continuous and is continuous in the total variation, then the belief MDP satisfies Assumption (W*):
Theorem 3.6 supplies the hypothesis under which the cited general MDP theory gives stationary optimal policies, optimality equations and convergence of value iterations for total-cost POMDPs in terms of , and alone, without compactness of the action set, boundedness of the cost or continuity of the filter. It covers, for example, observation kernels with densities continuous in , and the paper applies it to inventory control with incomplete records and to the Kalman filter. Example 4.1 of the same paper shows that total-variation continuity of cannot be weakened to setwise continuity.
The result is proved in the paper; this proposal poses its formal statement and the supporting results as proof targets. Completing them would provide a checked bridge from POMDPs to the general MDP theory under weak continuity, together with reusable facts about weak, setwise and total-variation convergence: equicontinuity of integrals against weakly continuous kernels (Theorem 5.2), the convergence-in-probability criterion (Theorem 5.5), and the generalized Fatou lemmas.
The posterior is defined only for -almost every and has no continuous version in general, so weak continuity of cannot be read off from continuity of . The tempting argument, that continuous and make the Bayes posterior move continuously, fails: need not be countable and need not have densities. What has to be controlled is the joint law on sets uniformly in the observation set ; convergence for each fixed is not enough. Turning this uniform control into almost-sure convergence of posteriors along a subsequence requires a diagonal argument over a countable base of . On the cost side, the difficulty is that may take the value and is not continuous; -inf-compactness has to be transported through integration against a weakly converging sequence of measures.
All definitions live in FeinbergPOMDP.WStar.Model. are separable metrizable spaces with their Borel σ-algebras (PolishSpace is not assumed, since Borel subsets of Polish spaces need not be Polish); is additionally nonempty and standard Borel in Theorems 3.6 and 3.7, where a filter must exist. is Mathlib's ProbabilityMeasure with the weak topology. All continuity notions are the paper's sequential ones; total variation is the supremum over Borel functions with values in , written in – form, while the set-indexed suprema of (5.15) and (5.17) keep their set form. The cost is written with and taking values in , so , exact even when on a set of positive measure. -inf-compactness is the published FeinbergLiang.ACOE.KInfCompact. A filter is a map that satisfies (3.3) and is jointly Borel measurable in , as the paper's stochastic kernel is; is the image of under for the Borel σ-algebra of the weak topology on .
Since does not depend on the choice of filter, every statement about is made for every filter satisfying (3.3). A fixed filter that ignores the observation, such as , would make a point mass and the weak continuity trivial; it satisfies (3.3) only when observations carry no information, and is excluded by quantifying over all filters.
The goal states the Assumption (W*) conclusion of Theorem 3.6. Its tail, "statements (i)–(vi) of Theorem 3.1 hold", invokes Theorem 2.1 of Feinberg et al. (2012) applied to the belief MDP; it is cited rather than proved in this paper. Generalized Fatou's lemmas 5.1(i) and 5.1(ii) are referenced from the published Schäl (1993) items. A complete development needs weak and setwise convergence on ProbabilityMeasure, portmanteau-type arguments, disintegration (Measure.condKernel) and the identification of the Borel and Giry σ-algebras on ; the last is missing from Mathlib and is a welcome contribution in its own right. Proofs of any milestone, and alternative arguments for Theorem 3.7, are welcome.
Wasserstein distributionally robust optimization (DRO) replaces the empirical risk of a loss by its worst case over all distributions within Wasserstein distance of the empirical law . Gao, Chen and Kleywegt (arXiv:1712.06050; Operations Research, 2024, doi:10.1287/opre.2022.2383) show that, for small radii, this worst-case risk is the empirical risk plus times a variation of the loss (a norm of its gradient or local slope), up to a remainder. This links DRO to gradient-norm regularization, as used in adversarial training and in data-driven newsvendor and pricing models.
For smooth losses the remainder is of order . Many losses used in practice are only piecewise smooth: hinge, ReLU networks, newsvendor costs, . Near the set where the pieces meet, the first-order expansion fails, and the paper's Theorem 1(I)–(II) carries an extra boundary term . Theorem 1(III) shows that this term is small with high probability, uniformly over the loss class, provided the data distribution does not concentrate near the non-smooth points. This mission formalizes that probabilistic bound.
Let be a metric space with its Borel -algebra, a probability measure on , and an i.i.d. sample from , with empirical law . The sampling law is the product on , and is its expectation. The formal statements also assume the metric space is second countable.
Let be a set of losses , and for each let be its non-smooth set: for a piecewise smooth with pieces , the union of the pairwise intersections of their closures (Assumption 1). The paper assumes is -null. The distance to a set is , with .
The objects of the mission are:
In Lean the boundary gap is the shared WassVarReg.PInf.boundaryGap; nearIndicator, indicatorClass, empRademacher, rademacher and Assumption3 are in WassVarReg.Boundary. The sample law is the published MinimaxWass.DataDep.sampleLaw.
Under Assumption 3 there exist such that for all , and , with probability at least , for every ,
The constants and are left unspecified; they depend only on Assumption 3.
The result. With and a class of bounded complexity, the right side of the goal is . Combined with Theorem 1(I)–(II), it gives the paper's conclusion that -Wasserstein DRO with is asymptotically equivalent to empirical variation regularization, , for non-smooth losses, uniformly over the class. Without it, the boundary term is only bounded by , and the expansion has no better accuracy than first order. Assumption 3 is the condition under which the non-smooth set does not matter statistically.
Formalizing it. The result is proved in the paper; it has no machine-checked proof. Its proof composes a uniform deviation bound (McDiarmid's inequality plus symmetrization) with a bounded-density estimate. The mission produces a general Rademacher deviation bound for bounded classes on an arbitrary metric space with a measurability guard, reusable by any statistical-learning mission, and fixes the printed constant of Lemma EC.5 ( on the page, from its proof).
The deterministic parts are short. The difficulty is in Lemma EC.5. McDiarmid's inequality must be applied to the uniform deviation over an arbitrary, possibly uncountable, class. Symmetrization must then be carried out with Bochner integrals over and a finite sign space. Neither tool is in Mathlib in this form. A tempting shortcut, bounding each fixed by Hoeffding's inequality and taking a union bound, fails: the class is infinite, and the bound must hold simultaneously for all inside a single event. A second point is Assumption 3: it controls only the shell , so the mass of has to come from the null closure of .
[MeasurableSpace Z] [BorelSpace Z] [SecondCountableTopology Z] in the goal-level statements. Second countability is an added technical hypothesis used throughout this paper's mission series. A sample is ω : Fin n → Z with , and its law is Measure.pi. Empirical means are .Metric.infEDist, which is on . A loss with thus has boundary gap and is excluded from , as on the page. The real-valued Metric.infDist (which is on ) would give such a loss gap and is not used.D : (Z → ℝ) → Set Z. The goal-level statements assume each is closed and -null, the standing consequence of its construction in Assumption 1. The details of the piecewise smooth loss model are not needed for this probability estimate.Contributions welcome: a general McDiarmid inequality for product measures, a symmetrization lemma for measurable classes, and proofs of the milestones in any order.
A seller learning a demand curve normally adjusts prices as new observations arrive. A price-change limit prevents that continual adjustment: a price may have to be chosen before the seller knows which demand curve it faces, then held through a block of sales. This matters when repricing is operationally costly, constrained by contracts, or visible to customers. Chen, Chao and Wang study pricing jointly with inventory replenishment under censored demand. Their Theorem 2 asks how much regret is unavoidable when the seller can change price at most times, regardless of the learning policy it uses (SSRN revision, pp. 10–11, 35–42).
The lower bound is paired with their Theorem 1: in the well-separated setting an algorithm attains regret proportional to for large horizons, while Theorem 2 asserts the same exponent cannot be improved uniformly over admissible policies (SSRN revision, p. 10). The paper appeared as an Operations Research technical note in 2020 (DOI 10.1287/opre.2020.1993); this mission cites the authors' SSRN revision dated 2020-02-10, whose page and result numbers are used throughout.
The horizon has periods. At each period the seller posts a price and replenishes inventory to one unit. Demand is either zero or one, so all demand can be served and the observed sale equals demand. The unknown scalar parameter belongs to . Conditional on the posted price, the probability of one unit of demand is
Holding and shortage costs are zero. Hence expected one-period revenue is . The clairvoyant benchmark is : it is attained by the feasible price . The local Lean sanity check proves this maximum property, so the benchmark does not rely on a default value of a supremum. The model is the explicit Bernoulli construction in the proof of Theorem 2 (SSRN revision, p. 35).
An admissible randomized policy may draw random bits and use past posted prices and observed sales when choosing its next price. Its action cannot depend on future demand or on the unknown parameter. Every realized seed and demand path must satisfy the price-change constraint
The regret is the expected sum of under the policy and the demand law at parameter . The paper's admissibility and change constraint are stated on pp. 5–6; its randomized policy factorization is displayed in (49) on p. 35 (SSRN revision).
The goal is the minimax reading of Theorem 2. For each fixed , there is a positive constant and a horizon threshold , independent of the policy and the horizon, such that
The parameter is selected after the policy. The proof's objective (56) is a worst-case parameter choice for each policy (SSRN revision, p. 37). The printed theorem sentence can also be read as one fixed instance defeating every algorithm; that order is false because a policy supplied with that instance's can post in every period.
Five milestones expose the source's quantitative ingredients. The hierarchy (50) constructs parameters from signs and scales . Its parameters lie in for large . Different signs are separated at scale . Lemma 1 bounds one-period regret by the squared error in a nearest-instance selection. The pointwise inequality underlying (57) gives a cost of at least for a wrong sign. A corrected Lemma 2 supplies a quadratic Bernoulli relative-entropy bound under an explicit interior condition (SSRN revision, pp. 36–37).
The exponent quantifies the cost of the change budget: fixing leaves a polynomial regret floor even though the Bernoulli demand law is one-dimensional and observed without censoring. Since the constructed instance fixes inventory at a level that serves every demand, a lower bound here also applies to policies in the joint pricing and inventory setting whenever that instance is admitted. It identifies the information loss caused by limited repricing, independently of lost sales and censoring.
The paper states the lower bound and gives a proof, but its printed Lemma 2 is false at prices where . The subsequent Lemma 3 applies that unrestricted bound. Therefore the source proof does not, as printed, establish the minimax claim for every admissible price policy. The Lean goal is an open target; the four elementary milestones and corrected information bound are also open Lean statements. Formalizing this mission requires an argument that handles prices at the zero-demand kink, or a different route to the lower bound. No machine-checked proof of this specific result is claimed here.
The natural comparison of two nearby parameters uses the relative entropy between their observed demand laws. Away from the kink, this information is quadratic in the parameter difference. At a price that makes demand impossible under one parameter but possible under the other, the divergence in the printed direction can be linear in that difference. The unrestricted bound of Lemma 2 therefore fails at exactly the prices an arbitrary policy may choose. Restricting the policy's prices would change the target. A faithful proof must retain those prices while still controlling the policy's information and regret (SSRN revision, Lemmas 2–3, pp. 36–40).
Lean represents the horizon by Fin T; its index zero is period one in the paper. Bernoulli demand paths have type Fin T → Bool. A policy's price at a period depends on a random seed and only the earlier demand bits; with inventory level one, these bits are exactly the observed sales. A probability measure on the seed models adaptive randomization, including a pre-sampled stream of random choices. Prices are measurable functions of the seed for each finite history. The budget holds on every seed and path, not only on average.
Path probabilities are finite products of conditional Bernoulli probabilities. Regret is a finite sum of nonnegative gaps integrated over the seed with lintegral, so it cannot become zero through non-integrability of a real-valued expectation. The exponent of and the scales use real division. The arg-min in (51) is any genuine nearest-instance selection; a local proof checks that one exists. The hierarchy's validity and separation statements require a large-horizon threshold, which the unqualified printed prose omits. The corrected Lemma 2 adds to keep the Bernoulli probabilities in the interior. Its verbatim milestone retains the printed statement, and its formal statement and note disclose the correction. Lemma 3 is not stated because its printed proof relies on Lemma 2 outside that interior region.
The named Bernoulli family strengthens the theorem's existential instance wording, while also exposing a limitation: at it violates the positive-mean and identifiability conditions stated earlier in the paper. That discrepancy is recorded rather than hidden in an assumption. Definitions for randomized adapted policies, finite path laws, the parameter hierarchy, and Bernoulli relative entropy are reusable; contributions that establish the open goal or repair the information comparison are in scope.
First-order primal-dual methods (PDHG, extragradient, ADMM) are the engine of a new generation of large-scale linear programming solvers, such as PDLP, because they need only matrix–vector products with the constraint matrix. Their textbook guarantees for convex–concave saddle-point problems are sublinear, for the averaged iterate, while in practice restarted variants converge linearly on linear programs. Applegate, Hinder, Lu and Lubin (arXiv:2105.12715v4, Math. Program. 2022) explain this gap through a sharpness condition on the normalized duality gap, and show that restarts turn sharpness into linear convergence.
This mission formalizes the part of that paper which shows that linear programming is sharp: Lemma 5 (p. 15), together with the bound of the KKT residual by the normalized duality gap (Lemma 4, p. 14) and the bilinear results of §3.2. The restart theorems that consume this property are the subject of the companion missions II and III of this series.
Let , , . The standard-form LP and its dual are
and their Lagrangian form is the saddle-point problem
A primal-dual point is , the feasible region is , and is the set of saddle points of on . On the norm is the Euclidean norm , and .
For let . The normalized duality gap (4a) is
The problem is -sharp on a set (Definition 1) if for all and all .
The KKT system (20) collects primal feasibility, dual feasibility and a nonpositive duality gap as , with
The KKT residual is the Euclidean norm of the componentwise positive part, a standard stopping criterion of LP solvers. A Hoffman constant (Hoffman 1952) is a constant with
If (19) has a solution and satisfies (26), then for every the problem (19) is -sharp on with
With :
and their combination, Lemma 4:
Lemma 5 is the input that makes the paper's restart theorems apply to linear programming: combined with Theorems 1 and 2 (missions II and III), it yields linear convergence of restarted PDHG, extragradient and ADMM on any feasible LP, with a rate governed by the Hoffman constant of the KKT system. Lemma 4 is of independent use: it shows that the normalized duality gap, which restart schemes can monitor, controls the KKT residual that solvers report.
The results are proved in the paper. As far as the platform and Mathlib show, none of them is formalized: there is no normalized duality gap, no primal-dual sharpness and no Hoffman bound for KKT systems in Mathlib. The remaining work is to formalize the paper's proofs. Strong duality for standard-form LP, needed for the §3.3 companion, exists on the platform (Polyhedral.lp_strong_duality, LinearOptimization.lp_strong_duality) in a different form.
The sharpness inequality relates two quantities of different nature: is a geometric distance to an implicitly defined polyhedron, while is a supremum of a bilinear gap over a truncated ball that is cut by the constraint . The unconstrained argument of Lemma 3, which identifies with , fails once is imposed, because the ball is no longer symmetric around and the maximizing direction may leave . Control of the duality-gap row of the KKT system also depends on the size of , which is why the constant degrades with and sharpness is claimed only on bounded sets . In Lean the normalized duality gap is an extended-real supremum over a set defined by a non-default norm, so each lower bound requires exhibiting a feasible point of and computing its gap.
Vectors live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and a primal-dual point is a pair. The norm on pairs is the norm of WithLp 2, eucl. The norm instance of the bare product type is the sup norm and is not used: with the sup norm the constants and would describe different statements. and are suprema in EReal. is a real infimum, and every statement that uses it assumes ("(19) has a solution"). is defined as the set of saddle points of on . and are encoded row block by row block exactly as (20) prints them; the page's "" in (18) is a misprint for , which is what (20) encodes.
The Hoffman constant enters only through its defining property (26), quantified over all , together with . Lemma 5 is stated for every such constant. Sharpness follows Definition 1 literally, with ; replacing that range by would be a different statement. A formalization that restricts (26) to , uses the sup norm, or takes a real-valued supremum for would trivialize or change the goal and is ruled out. is the least with an eigenvalue of ; its Lean value for is .
Contributions welcome: proofs of (22) and (25), whose combination gives Lemma 4 and then Lemma 5; general lemmas on suprema over Euclidean balls in WithLp 2 products; and a Hoffman-type existence theorem for , which this mission does not pose. The bilinear statements (Lemmas 2–3) need a minimum-nonzero-singular-value API and are reusable beyond this mission.
A seller with a fixed stock must choose prices before knowing when customers will arrive or what they will be willing to pay. If customers can wait for a later price, the seller must also account for how today's price changes their purchasing decisions. Chen and Farias study this problem with strategic customers and identify a simple inventory-based policy that can be compared with the best attainable revenue. Their Theorem 1 shows that this policy, with discount rate for a season of length , earns at least of the optimal expected revenue. The policy posts the price that is optimal in the canonical discounted revenue-management problem with myopic customers (Gallego and van Ryzin, 1994; Farias and Van Roy, 2010) at the current inventory level. This mission targets the lower-bound half of its argument, stated as Lemma 9: a comparison between the policy's revenue over a fixed selling season and a discounted, infinite-horizon value. The latter comparison is meaningful independently of the paper's strategic-customer benchmark.
The seller begins with inventory and sells at most one item to each customer. Customers arrive at rate . Their nonnegative valuations have density with total mass one. Write for the probability that a valuation exceeds price . A customer who behaves myopically buys at a posted price exactly when the valuation is high enough, so sales occur at rate while that price is posted.
The paper's Assumption 1 concerns the virtual value : it is nondecreasing on nonnegative prices and has a nonnegative root. The simple policy is built from a discount rate and an infinite-horizon Bellman value . It has and, for , satisfies the sign-corrected recursion
At inventory the root price is the unique nonnegative solution of . The price posted just before a sale is , and the inventory then becomes . At zero inventory the posted price is infinity and there are no more sales. The expected sum of prices paid at sales by time is denoted . These objects come from §§2–3.1 of the paper.
The goal is Lemma 9, for every and every initial inventory :
The coefficient is part of the target. No choice of is fixed. The milestones follow the results stated in the paper: inventory monotonicity of , price monotonicity, pathwise monotonicity of the price and its revenue rate (Lemma 7), the expected-rate identity, revenue-per-time monotonicity (Lemma 8), the identification of with discounted policy revenue, and the comparison through an independent exponential horizon. The last milestone evaluates exactly for .
The bound quantifies how much of the discounted value this explicit policy earns within a finite selling season. Its factor depends only on the dimensionless product ; it does not depend on inventory, arrival rate or valuation density. Together with the paper's separate upper bound on its strategic benchmark, Lemma 9 contributes to the advertised comparison. The full comparison requires definitions and equilibrium arguments beyond this mission, so the goal here is precisely the fixed-horizon lower bound.
Chen and Farias proved these statements in the published paper. The Lean items in this proposal are statements awaiting machine-checked proofs. A completed development would establish the discounted-value verification step and the fixed-horizon comparison for an explicit pure-death sales process. Its constructions of inventory-dependent sale times and finite-horizon revenue could also be reused in other pricing models with Poisson arrivals.
The Bellman value is specified by an optimization equation, while is defined from the actual sales process. Their equality at an exponential horizon does not follow by unfolding a definition. The price chosen through the virtual-value equation must be connected to the Bellman optimum, and the inventory-dependent process must be related to the same value. The paper also relies on the fact that the root price falls as inventory rises, citing Lemma 1 of Farias and Van Roy; that fact does not follow merely from monotonicity of without control of the marginal values . Lemma 8 then concerns expected revenue over two different horizons, including paths that sell out early.
The Lean model uses a nonnegative integrable density on , zero on negative valuations and normalized to mass one. It adds for every . This disclosed condition excludes bounded-support densities: without it the paper's quotient can divide by zero and Lean would assign a spurious value. The paper says the root equation has a unique solution under Assumption 1, but nondecreasing alone does not guarantee existence or uniqueness. Accordingly, the root policy is characterized by its equation and an explicit uniqueness condition. The Bellman recursion uses a least-upper-bound predicate rather than a real supremum with a default value on an empty or unbounded set. The corrected sign in the recursion matches the paper's root equation and discounted-revenue equation.
For stock , the model uses independent rate-one exponential clocks. At inventory , the next holding time is the next clock divided by . Sales are numbered , and sale earns . The law is the myopic sales process with intensity . Expected revenues are lower integrals in the extended nonnegative reals; nonnegative prices make their real-to-extended conversion exact. An independent is represented by an outer integral over its law. The factor missing from the paper's printed compensator display is restored, and the paper's intermediate is read with the missing restored.
The strategic-customer types, stopping rules, perfect Bayesian equilibrium, and the identification of the strategic policy's revenue with myopic-sales revenue are not formalized here. Neither are Theorem 1's and benchmarks: their specification is not pinned down sufficiently in the paper for this proposal. In particular, is constructed from sale times and payments, never from , and is specified by the Bellman equation, never as the policy's revenue. Contributions toward the goal include the individual milestones and reusable facts about the clock process, its revenue, and the exponential horizon.
A seller who changes prices while learning demand faces two costs: a price experiment may earn less revenue now, while insufficient experimentation leaves later prices poorly calibrated. Customer features make the balance harder because both willingness to buy and sensitivity to price may vary between customers. Ban and Keskin study this problem when the number of recorded features can be large relative to the selling horizon. Their known-support policy, ILSX, provides the upper bound formalized here Ban and Keskin, 2021, §§2 and 4.1.
The paper's result is a statement about learning a demand model while serving sequential customers, rather than about fitting that model after all observations are available. A price at period must use information then available, including the arriving customer's features but excluding that customer's demand shock. The seller therefore needs a policy whose expected revenue loss can be bounded uniformly over the unknown parameters in a specified model Ban and Keskin, 2021, pp. 5552–5556.
In each period , a customer arrives with a feature vector . The seller observes the augmented vector , posts a price with , and then observes demand. In the linear demand model, demand equals
The intercept and slope vectors are unknown. The seller knows the sparsity structure : outside this set of coordinate indices, both parameter vectors vanish. The compressed parameter lies in a compact coordinate rectangle , and . The compressed customer vector is Ban and Keskin, 2021, pp. 5552–5555.
At price , expected single-period revenue is . The clairvoyant price is when the slope is negative. The paper assumes this price is in throughout its model domain. Expected regret is the expected sum, through period , of the clairvoyant revenue minus the revenue at the policy's price Ban and Keskin, 2021, (2)–(4), p. 5553–5554.
The ILSX policy charges one fixed experimental price at periods and a distinct price at periods . At every other period it estimates the compressed demand parameter by least squares using experimental observations, projects the estimate onto , and applies to the projected estimate and the current customer vector. Both prices lie in Ban and Keskin, 2021, (7), (8), (12), pp. 5555–5556.
The goal is Theorem 2: for the stated model and ILSX policy, a finite positive constant exists such that
The constant is chosen after the model, shock process, experimental prices, and estimator selection are fixed, but before the parameter and horizon. The theorem and Remark 5 are on pp. 5556–5557 of Ban and Keskin, 2021.
The milestones reproduce the paper's route into this claim: the experimental-period count following (7); the growth bound (15) for the price-variation statistic ; Lemma 1's minimum-eigenvalue probability bound for the experimental information matrix ; and Lemma 2's high-probability bound for its noise-driven estimation error. The least-squares error identity (11) is included as a supporting item on invertible samples, not as a milestone. The constants and thresholds in these targets remain existential where the article leaves them existential Ban and Keskin, 2021, pp. 5555–5556.
The theorem gives a guarantee for a concrete pricing policy under feature-dependent price sensitivity. The bound grows with the horizon at order for a fixed known support, with an explicit factor in the published statement. It lets a seller compare the cost of this policy with the revenue of a seller who knew the demand coefficients before pricing. The paper presents its result as matching its lower-bound benchmark up to logarithmic factors, under the paper's respective hypotheses Ban and Keskin, 2021, Theorems 1–2, pp. 5554–5556.
The mathematical result was published in 2021. This mission seeks a machine-checked statement and proof of the known-support guarantee and its stated intermediate results. The checked Prove2Me prior-art catalog contains featureless dynamic-pricing results and separate least-squares results, but no matching formalization of ILSX. A completed development would add reusable definitions for a feature-dependent price regressor, experimental information matrix, nonanticipating estimator selection, and expected regret. The article places its proofs in an electronic companion, which is not included in the held source PDF; this mission does not reproduce those proofs as source material.
The policy learns from a sparse set of deliberately chosen periods, while its regret accumulates at every period. A pointwise least-squares identity alone does not control the regret: the information matrix can be singular at early periods, and the customer features and shocks are random. In particular, the printed inverse identity (11) says “for all ”, although at the matrix has rank at most two and cannot be invertible when . The formal statement therefore confines the inverse identity to invertible samples. Lemma 2's event also includes invertibility so a default inverse of a singular matrix cannot make its error bound automatic Ban and Keskin, 2021, (9)–(11), Lemma 2, p. 5556.
Lean uses one-based periods and a support subtype of the augmented feature coordinates. Coordinate zero is the paper's intercept coordinate one. The parameter has coordinates for demand intercept or price slope and support index . The regressor gives the information matrix in (10). Euclidean squared norms are explicit sums of squares, and the minimum-eigenvalue claim is the equivalent Rayleigh inequality. The parameter rectangle is nonempty, and its Euclidean projection is coordinatewise clamping.
The standing assumptions are , , , distinct experimental prices in , bounded i.i.d. features with mean zero and positive-definite covariance, and a fixed shock process with conditional mean zero, bounded conditional second moment, and finite conditional exponential moments near zero. The feature process is measurable and integrable. The model additionally states independence of the next customer's features from the past primitives, the reading of the paper's joint probability construction used here. The slope is negative and the clairvoyant price lies in for every allowed parameter and realized feature. These conditions ensure that the price formula represents a genuine revenue maximum. The phrase about continuous features having positive measure in the interior of their domains is omitted because the page does not specify the domains or a reference measure Ban and Keskin, 2021, §2, pp. 5552–5554.
The estimator is any measurable minimizer of the experimental least-squares objective for histories with at least two observations. Its type depends only on earlier observations; at nonexperimental periods the recorded pseudo-observations are ignored by the objective. The shock law is fixed while the parameter varies. Expected regret uses a nonnegative integral, and conditional second and exponential moments use nonnegative conditional expectations. The theorem binds before the parameter and horizon, while leaving support size fixed with the model. Consequently, the stronger uniformity in suggested by Remark 5 is outside this statement. These choices exclude vacuous integrals, unconstrained estimators, and accidental bounds from a singular matrix inverse. Work on the probability estimates, least-squares identity, and regret bound is welcome under these exact definitions.
In distributionally robust optimization, a decision is judged against probability laws near a nominal law rather than against the nominal law alone. The nominal law is often the empirical distribution of observed data. For a loss function, this produces a worst-case expected loss that depends on the size and geometry of the permitted changes to the data. The infinity-Wasserstein model restricts how far any observation can be moved, apart from null events in a coupling. It is a mathematical form of the bounded perturbations used in adversarial learning. Gao, Chen and Kleywegt study when this robust loss behaves like a regularizer based on variation or local slope.
For a finite data set, the nominal law has finite support. This makes the infinity-Wasserstein case especially concrete: each atom of the empirical law has a radius-limited set of possible destinations. Yet the objective still ranges over all probability measures, and the loss need not be bounded on a metric ball. The paper's finite-support duality result and its local-slope estimate together identify the regularization term that this distributional model produces.
Let be a metric space and let be probability laws on its Borel sets. A coupling of and is a joint law on with those two marginals. The infinity-Wasserstein distance is
Given a real loss and a radius , the robust value is the supremum of over all satisfying . The regularizer is this robust value minus . For observations , the empirical law is .
The one-sided local slope records the greatest limiting rate at which can increase under a perturbation that tends to . The local growth is the largest increase among destinations with . A set marks the interfaces between pieces of a piecewise loss. Its boundary contribution at is , where the distance to an empty set is infinite. These objects appear in Definition 2 and Assumption 5(I).
For a nominal law , the first targets assert that an optimal coupling exists when is finite and that
This is Lemma EC.2 in the appendix. The values are allowed to be infinite when a local loss supremum is infinite; the printed assertion of unconditional finiteness is not included.
For an upper semicontinuous loss, the Proposition 1 case asserts
It is a companion statement: it says that the regularizer vanishes, while the main target says at which rate.
The main target is Theorem 1(I), in its general-metric form from Appendix B under Assumption 5(I). If , , and the local growth obeys
then, for a sufficiently small radius, every nonempty empirical sample and every loss in the class satisfy
The finite-support duality and the identity between the empirical regularizer and the average of are the mission's intermediate targets. The printed in Lemma EC.9 is read as , as in Theorem 1(I).
The estimate gives a precise first-order description of infinity-Wasserstein robustness: the mean local slope is its leading regularization term. The quadratic term measures local curvature or growth, while the boundary term records the effect of sample points close to interfaces between loss pieces. Setting gives the smooth-loss regime, where that interface correction vanishes. The result makes it possible to compare bounded data perturbations with explicit variation penalties using the same loss class and sample.
The paper proves the result. The formalization work here is to express its objects and quantified conditions in Lean, establish finite-support duality for the extended-real robust value, and then formalize the known local estimate. No machine-checked proof of these mission targets is claimed here. The transport and duality definitions can support other finite-support distributionally robust models; the local-slope definitions can be reused for other metric-space perturbation bounds.
The robust value is a supremum over probability laws, whereas the target bound is a finite average of pointwise quantities. Relating the two requires control of the infinity-Wasserstein constraint at every nominal atom, including cases where an infimum over couplings must be attained. A direct substitution of a pointwise supremum into an expectation does not establish the reverse inequality, and extended-real values need care when a loss is unbounded. At the local level, a slope is only a limit near a point; the inequality needed here holds uniformly for all losses, all points, and all sufficiently small radii, with a correction near .
The Lean metric space uses its Borel measurable structure and is second countable, so the distance on the product is measurable. It has no isolated points, matching §3.4. Losses in the class are measurable. Sample indices are Fin n with , and is the published empirical probability law. Infinity-Wasserstein distance takes values in ; robust values and local growth use extended reals. The theorem explicitly requires finite local slopes and finite growth values in the range where Assumption 5(I)'s real inequality is used. The regularizer is built from the supremum over all probability laws in the Wasserstein ball, and its finite-sample result states finiteness before converting its value to a real number. This rules out replacing the regularizer by the easier average of local growth.
The paper defines from intersections of closures of pieces and assumes it is null under a true law. The deterministic estimate uses only distances to , so this mission treats as supplied data and does not require nullity. Likewise, is needed for the paper's statistical setting but the target evaluates only at finite sample points, so no true law appears in this statement. The radius bound is placed before the sample because Assumption 5(I) supplies one common . These generalizations and the positive-radius reading of Assumption 5(I) are explicit in the item statements. Contributions toward the optimal-coupling lemma, extended-real finite-support duality, and the local estimate all advance the target.
In a multi-armed bandit, a decision maker repeatedly chooses an arm, observes a reward, and tries to learn which arm has the highest average reward while losing little reward during learning. A policy that requires the number of future pulls in advance cannot be used unchanged when stopping time is uncertain. Perchet and Rigollet study successive elimination (SE), which removes poorly performing arms from a shrinking active set and can run without knowing the realized horizon. Their Theorem 2.1 bounds its expected regret when the horizon is random and independent of rewards Perchet and Rigollet, 2013, Theorem 2.1.
The static-bandit theorem also supplies a concentration and elimination analysis used in the paper's broader study of bandits with covariates. This mission isolates that theorem and the intermediate estimates that make its quantitative constant explicit. The paper proves the result in §2, with a concentration lemma in the Appendix; the goal here is a machine-checked statement and, eventually, a machine-checked proof of that known result.
There are arms. For each arm , the reward stack lists the rewards that successive pulls of that arm will reveal. Rewards lie in , are identically distributed along each arm, and have mean . The stacks are mutually independent. Arms are indexed so that , and the last arm, denoted , is uniquely best. Its gap from arm is . A gap is zero only for the best arm.
The policy works in rounds. At the start of round , a nonempty set is active. It pulls each arm in once, in increasing index order, and computes the mean from that arm's first rewards. It retains an arm when its mean is within of the largest active mean, where is an integer, , and
Concatenating the rounds gives the pull sequence . For a horizon , its regret is . If is random, independent of the reward stacks, and has mean , the paper studies . For a threshold , let be the largest arm gap strictly smaller than , or zero if none exists.
The goal is Theorem 2.1, for every positive threshold :
The in this formula counts suboptimal arms; there are arms in total. The paper writes under a convention that division by zero is infinite. The real-valued Lean goal states the informative positive-threshold case.
The milestones include the Appendix's maximal Hoeffding–Azuma inequality and Lemma A.1, which controls all empirical averages up to a fixed time. In §2 they continue with the stopping-round estimate (2.2), the empirical-gap tail (2.5), the bound for a false elimination of the best arm, and the final comparison for . Each has its own statement so that a proof of the goal can import the exact estimate it needs.
The bound separates the cost of learning arms with gaps above from the remaining regret represented by . It applies when the policy uses a tuning value but the number of pulls actually made is the random variable . Thus it gives a quantitative guarantee without asking the algorithm to know its stopping time in advance. Its constants and dependence on , , , and are explicit Perchet and Rigollet, 2013, §2.
The result is proved in the paper, while the Lean declarations in this proposal are open statements. Completing them would add a reusable formal account of elimination on a reward stack and of the Appendix's time-uniform concentration estimate. Mathlib and existing platform theorems contain related Hoeffding–Azuma tools, but this paper's peeling inequality, its particular stopping rule, and the random-horizon regret conclusion still require proofs in the stated model.
An ordinary concentration bound at one sample size does not control every round in which an arm could eliminate the best arm. Taking a naive union bound over all rounds loses the dependence on needed for the displayed regret constant. The Appendix instead states a maximal inequality and a bound that holds across a range of sample sizes. The regret calculation must then account for both kinds of error: removing the best arm and retaining a suboptimal arm for too long.
The stopping round depends on the gap through , which itself contains . Its upper bound, the event decomposition across ordered arms, and the final comparison of gap-dependent terms all retain the paper's exact constants. A proof that only establishes the asymptotic rate would not close this goal.
Lean uses Fin (K+1) with zero-based indices, so its last element is the paper's arm . The published stochastic-bandit definition supplies the mutually independent reward stack and arm means. The [0,1] bound, sorted means, and unique best arm are explicit assumptions. A separate martingale-difference definition supplies the Appendix's adapted, integrable sequence, including centering of its first term; the page's one-line definition leaves that first-step condition unstated. The concentration milestones require a nondegenerate interval : the displayed maximal exponent divides by , and Lemma A.1 is false at for a zero sequence and .
The SE policy is a function of observed rewards in the stack. It uses the end-of-round test described in the text and proof of §2, with equality retained, since Policy 1's pseudocode tests at a different point in the round. The active set starts with all arms and remains nonempty; the total Lean pull function has a fallback value that is unreachable under the theorem's parameters. The policy never reads the unknown means. Empirical means and are used only at positive rounds.
The horizon is measurable and integrable, has mean , and is independent of the entire reward stack. Since regret is bounded by the horizon, its expectation is a genuine integral rather than the default value of a non-integrable Lean integral. The positive-threshold condition avoids Lean's zero-valued division at . Finite maxima are taken over finite arm sets, and is kept distinct from the ordinary logarithm in the Appendix's bounds. The paper's printed in the logarithm of (2.7) and the final comparison is read as , consistently with (2.2) and Theorem 2.1. Contributions to the concentration lemmas, stopping-round analysis, elimination events, and final regret proof all fit this scope.
A queue layout of a graph places its vertices on a line and splits its edges into classes, called queues, so that inside one queue no edge is nested inside another. The minimum number of queues is the queue-number. Queue layouts were introduced by Heath, Leighton and Rosenberg (1992) and Heath and Rosenberg (1992) as the dual of stack layouts (book embeddings): reading the vertex order from left to right, the edges of one queue are opened and closed in first-in first-out order. Queue layouts are closely tied to track layouts and, through them, to three-dimensional grid drawings of graphs (§9 of the paper).
Whether planar graphs have bounded queue-number was asked by Heath, Leighton and Rosenberg in 1992 and stayed open for 27 years. The best general bounds before 2019 grew with the number of vertices: by Heath, Leighton and Rosenberg (1992), by Di Battista, Frati and Pach (2013), and by Dujmović (2015); for Euler genus , Dujmović, Morin and Wood (2017) had . Dujmović, Joret, Micek, Morin, Ueckerdt and Wood (arXiv:1904.04791, J. ACM 2020) proved that every planar graph has queue-number at most (Theorem 1), and extended the result to every graph embeddable in a fixed surface (Theorem 2) and to every proper minor-closed class (Theorem 3).
This mission is Theorem 2: graphs of Euler genus have queue-number at most . It is the second mission of a two-mission series; the first poses Theorem 1.
All graphs are finite and simple. A linear ordering of the vertex set is fixed. Two edges and with four distinct ends nest if (after renaming the ends). A queue is a set of edges no two of which nest. A -queue layout of is a linear ordering together with a partition of into queues, and means that a -queue layout exists.
A layering of is an ordered partition of such that every edge joins two vertices of the same or of consecutive layers. A BFS layering takes one root in each connected component and puts in layer . A BFS spanning tree of a connected graph rooted at is a spanning tree with for every . A path in is vertical if the distance to grows by exactly one at every step.
The Euler genus of the orientable surface with handles is , and that of the non-orientable surface with cross-caps is ; the Euler genus of a graph is the least Euler genus of a surface it embeds in (footnote 2 of the paper). Planar graphs are exactly the graphs of Euler genus . Combinatorially, an embedding of a graph is described by an embedding scheme: a cyclic order of the edges at each vertex (a rotation system) together with a sign on every edge (twisted or not). Tracing faces through the scheme gives a face count , and with vertices, edges and components the scheme has Euler genus .
The paper states Theorem 2 as and proves the explicit bound in §5. The goal poses that explicit bound, for every finite graph, connected or not.
The result. Theorem 2 settles boundedness of the queue-number for every class of graphs embeddable in a fixed surface, with a bound linear in the Euler genus. Through the connection between queue-number and track-number, the paper derives from it (§9, Theorems 54 and 58) that a graph of Euler genus with vertices has track-number and a three-dimensional grid drawing of volume , linear in for every fixed surface. It is also a step on the paper's route to Theorem 3 (proper minor-closed classes), since graphs on surfaces are the basic pieces of the Robertson–Seymour graph minor structure theorem. Lemma 21 is of independent use: it reduces a graph on a surface to a planar graph while controlling BFS layers.
Formalizing it. The result is proved; as far as is known it has no machine-checked proof. A formalization needs queue layouts, layerings, BFS layerings and vertical paths, and, independently of queues, a usable combinatorial theory of graphs on surfaces, which Lean's Mathlib does not have. The Euler genus definition of this mission (embedding schemes and face tracing) and Lemma 21 are reusable well beyond queue layouts.
The obvious reduction, deleting few vertices to make the graph planar, is not enough: a planar subgraph alone does not control how the deleted vertices interact with a queue layout. The deleted set must be thin in every BFS layer, and the planar remainder must carry a BFS layering compatible with the original one, which is what Lemma 21 provides. Its proof cuts the surface along a subgraph made of tree paths and must show that the cut graph is planar by an Euler-characteristic count over face-tracing data, and that distances from a new root agree with the old BFS distances. In Lean, the main obstacle is the surface side: Euler's formula for embedding schemes, the cutting operation on rotation systems, and the passage between the combinatorial notion of Euler genus and the drawing-based notion of planarity. The planar input, Lemma 18, is itself the whole of mission 1's argument (Theorem 15 with Lemmas 5 and 8).
SimpleGraph V on a finite type V : Type with decidable equality and adjacency.HasQueueLayout G k: an injective map ord : V → ℕ (the linear ordering) and an assignment of the edges of (G.edgeSet, not all unordered pairs) to Fin k such that no two edges in one queue nest; nesting uses strict inequalities, so edges sharing an end never nest. Queues may be empty.L : V → ℕ; a BFS layering takes one root per component. Vertical paths are nonempty lists indexed from with distance , .EulerGenusLE G g asks for an embedding scheme (rotation permutation of the darts, cyclic at every vertex, and a symmetric edge signature) whose Euler genus , computed in , is at most . The face count is half the number of face-tracing orbits plus the number of isolated vertices. Equivalence with footnote 2's topological definition is the Heffter–Edmonds–Ringel rotation principle and its non-orientable extension, with additivity over components; it is not part of the mission.RobertsonSeymour1986.GM5.IsPlanar: a crossing-free drawing in by simple arcs. "Euler genus iff planar" is a theorem connecting the two definitions, not built into either.Sym2 V would deny edgeless graphs a -queue layout; non-strict nesting would forbid adjacent edges in one queue; a drawing that tolerates crossings would make every graph planar; a face count without halving, or without isolated vertices, would make the Euler genus too small or too large (the sanity checks confirm has a scheme of Euler genus , a twisted one of genus , and two isolated vertices genus ).Maximizing a homogeneous polynomial over the unit sphere, , covers the largest stable set of a graph (degree three), the norm of a matrix (degree four) and the best separable state problem of quantum information. For quadratic it is an eigenvalue problem; for degree at least three it is NP-hard. The sum-of-squares hierarchy of Parrilo and Lasserre replaces " on the sphere" by " is a sum of squares of polynomials of degree at most on the sphere", giving upper bounds that are computable by a semidefinite program of size and decrease to . How fast they converge decides how large has to be for a given accuracy. Fang–Fawzi, §1–1.1
Timeline:
Write , , and . A matrix polynomial has a real polynomial in each entry, and is the real matrix of values. means that the symmetric matrix is positive semidefinite. A matrix polynomial is -sos on if there are finitely many matrix polynomials , each entry of total degree at most , with
For a scalar polynomial , is the least such that (a matrix) is -sos on , and is the minimum of on . The level value is when no such exists.
The milestones use three further objects. A harmonic decomposition of a homogeneous of degree is with homogeneous of degree and . is the least constant with for all such in all dimensions. The Gegenbauer coefficients of a univariate polynomial are its coefficients against the orthogonal polynomials for the weight on , equation (9). For of degree at most , the kernel error is
For every there are constants depending only on such that, for all and every matrix polynomial , homogeneous of degree with , symmetric at every , with on :
The goal fixes only the shape and the regime , and leaves the constants open.
They follow the paper's proof, in attack order:
Theorem 2 says how the level must grow with the dimension: suffices for relative error , where Reznick's analysis needs . Theorem 10 of the paper shows that, for , the kernel error of this technique really is of order . Independence of the matrix size gives certificates for polynomials that are bihomogeneous of degree on . The paper's Theorem 15 uses this, together with the DPS duality of the companion mission, to bound the convergence of the DPS hierarchy for separability. Fang–Fawzi, pp. 3, 10, 14
The theorem is proved in the 2019 preprint and was published in Mathematical Programming in 2021. No machine-checked proof of it or of its ingredients is known. Proving it formally takes reusable infrastructure: degree-bounded matrix SOS on the sphere, harmonic decomposition of homogeneous polynomials, Gegenbauer polynomials with their coefficients and the Funk–Hecke formula, and spectra of Jacobi matrices of orthogonal polynomials. The milestones also correct the printed text, as listed under Formalization scope.
Positive semidefiniteness of at each point of the sphere does not give a factorization with factors of prescribed degree, and Reznick's kernel only reaches error . Two estimates must be uniform at once. First, harmonic projection of a degree- form must be bounded in sup norm independently of ; the bound is easy, and the sup-norm bound is the content of Proposition 5. Second, the kernel error must be bounded throughout the regime , which comes down to the location of the largest zero of a Gegenbauer polynomial. The printed bounds on that zero and on in Proposition 7 are false in small dimensions, so the paper's explicit constants cannot be relied on.
Fin d → ℝ (0-based coordinates), and is the equation , not the sup-norm sphere. Matrix polynomials are matrices over MvPolynomial (Fin d) ℝ, evaluated entrywise, and homogeneity is entrywise.Measure.toSphere.Proofs of any milestone are welcome. So are reusable developments of Gegenbauer polynomials, spherical harmonics, the Funk–Hecke formula, Jacobi matrices, and Carathéodory-type finite quadratures that turn an integral of squares into a finite sum of squares.
The newsvendor problem is the basic single-period inventory decision: a retailer orders units at unit cost before a random demand is observed, sells at unit price , and loses unsold units. When the demand law is known, the optimal order is a quantile of that law. In practice the law is rarely known, and a distributionally robust newsvendor instead hedges against the worst law in an ambiguity set of laws consistent with partial information.
Scarf (1958; reference [42] of arXiv:1806.05379) solved the case where only the mean and the variance of demand are known, and observed that for a range of small profit margins the robust newsvendor orders nothing. Demand data in retail and spare-parts settings are often heavy tailed: Pareto fits with exponent close to have been reported, so a finite mean is plausible while a finite variance is not. Das, Dhara and Natarajan (arXiv:1806.05379) therefore replace the variance by an -th moment for an arbitrary real . This mission formalizes their result that the zero-order phenomenon survives for every such .
Write the critical ratio as . A demand law is a probability measure on . Fix a real and two moments with
The ambiguity set is
the laws on with mean and -th moment . The worst-case expected shortage is
and the robust newsvendor problem (3.2) is
An optimal order quantity is a minimizer of this objective. Two thresholds appear:
In Lean these are ambiguitySet, worstCase, robustCost, eta0, q0 and IsOptimalOrder in the namespace HeavyTailNV.ZeroOrder.
, and
and the two-point law with mass at and the rest at lies in and attains the supremum. 2. Properties of (§2.1, p. 6): is non-increasing and convex, for , and as . 3. Display (3.10) (p. 14): for and ,
Proposition 3.2 shows that for every finite moment order , however high, there is a nonempty interval of critical ratios in which the robust newsvendor orders nothing, and it gives the threshold and the minimum positive order in closed form. For it recovers Scarf's zero-order region. The worst-case law associated with therefore carries a positive mass at zero demand, which is the low-service-level counterpart of the paper's heavy-tail result for high critical ratios (the companion mission of this series).
The results are proved in the paper: the proof of Proposition 3.1 follows the statement on pp. 12–13 and the proof of Proposition 3.2 is on p. 14. None of them has a machine-checked proof. Formalizing them requires a usable treatment of moment-constrained suprema over probability measures on , of the stop-loss transform , and of minimizers of convex functions on a half-line. These pieces recur across robust inventory and pricing models.
The closed form of Proposition 3.1 is the central step. The lower bound is a computation with a two-point law. The matching upper bound has to hold against every law in , including laws with unbounded support and non-integer . The paper obtains it from a dual certificate for the moment problem (3.3)–(3.4), and weak duality for this semi-infinite problem is not available off the shelf. The closed form also holds only on . To conclude anything about minimizers on all of , where no closed form is known for general (the dual leads to equations , p. 11), one needs convexity of on the whole line. Inspecting the objective on alone does not determine the global minimizers.
Measure ℝ with IsProbabilityMeasure F and F (Set.Iio 0) = 0. Moments are Bochner integrals, and the set requires Integrable (fun w => w) F and Integrable (fun w => w ^ α) F (real rpow), so that the moment equalities are genuine.sSup. Under the standing hypotheses , , the set is nonempty (it contains the two-point law of Proposition 3.1) and the expectations are bounded above by , so the value is not Lean's default for an empty or unbounded set. Every statement carries these standing hypotheses of (3.1); no other hypothesis is added except the range in (3.10), which is the paper's standing range of the critical ratio.HeavyTailNV.Tail.Model. This mission defines the thresholds, optimality predicate and two-point law in HeavyTailNV.ZeroOrder.Model. Contributions to the general moment-problem duality used by Proposition 3.1 are welcome and reusable well beyond this mission.A decision made from sampled data can be sensitive to the distribution chosen to represent future uncertainty. Robust sample average approximation addresses this by optimizing against every distribution that passes a goodness of fit test, rather than against one fitted distribution. The resulting set of plausible laws is a data driven uncertainty set. Its finite sample coverage and its behavior as the sample grows serve different purposes: coverage protects against sampling error at a chosen sample size, while convergence asks whether the uncertainty set eventually stops admitting laws far from the true one. Bertsimas, Gupta, and Kallus distinguish these properties in their Robust Sample Average Approximation paper.
This mission concerns the two tests the paper assigns to a known finite support: Pearson's test and the G test. Both compare the empirical frequencies of the observed support points with the probabilities under a proposed law. Their confidence regions give concrete uncertainty sets for discrete data. The paper's Theorem 4 states that both tests have the stronger convergence property it calls uniform consistency. That property is used in its general characterization of when robust sample average approximation converges for every admissible cost function (Theorem 2 and Table 1, pp. 13–14).
Fix a known set of possible observations, labelled . A probability law on this support is specified by probabilities , each nonnegative and summing to one. A sample of size consists of independent observations from an unknown true law . Its empirical frequency at label is
To assess a hypothetical law with probabilities , Pearson's statistic and the G statistic are, in the paper's normalization,
The confidence region for each test is the set of hypothetical laws whose statistic is at most , where is fixed across sample sizes. An observed point to which assigns zero probability makes either statistic infinite. A term with zero empirical frequency contributes zero to the G sum, including when its hypothetical probability is zero. These conventions make the regions describe the same tests at the boundary of the probability simplex as they do in its interior (§3.1, p. 8; §10.6, p. 38).
A sequence of laws is weakly convergent to when expectations of every bounded continuous function converge. On this finite support, weak convergence can be measured by the total variation distance
The paper's Definition 3 calls a test uniformly consistent when, for every true law , almost surely every sequence that fails to converge weakly to lies outside the confidence region infinitely often (Definition 3, p. 13). The almost sure event applies to all such sequences at once; this is stronger than a statement about one fixed false hypothesis.
For the Pearson and G confidence regions and with fixed , the target is
Here has the quantifier order of Definition 3: every generating , almost every infinite sample, and every nonconvergent sequence . This is Theorem 4, p. 14. Its four milestone claims are the finite support description of weak convergence, almost sure convergence of empirical frequencies, and the paper's total variation bounds for and (§10.6, p. 38).
The result says that distributions retained by either test cannot remain persistently separated from the data generating law as the sample grows. In the paper's framework, that is the statistical condition needed for its general theorem to turn test based confidence regions into convergent robust optimization values and decisions under its separate assumptions on the cost and feasible set (Theorem 2, p. 13). Theorem 4 itself concerns the tests; it does not assume a cost function or assert optimization convergence directly.
The paper proves Theorem 4, so the open work here is its Lean formalization. A complete development would also leave reusable statements for finite probability vectors, their empirical frequencies under an infinite product law, total variation, and the boundary aware Pearson and G divergences. These pieces can support other discrete goodness of fit and distributionally robust optimization results. The mission does not claim that Theorem 4 already has a machine checked proof.
Pointwise convergence of empirical frequencies does not by itself state uniform consistency. The latter quantifies over all moving hypothetical laws on one almost sure sample event, including laws chosen differently at every . A direct argument about one fixed therefore does not address the target. The finite support makes weak convergence concrete, but the formal statement must still relate that topology to a finite total variation sum and keep the quantifiers in the order required by Definition 3.
The boundary of the probability simplex is another source of difficulty. Lean's real division and logarithm have default values at zero. Using those defaults in the test statistics would accept some laws that assign zero probability to an actually observed category. Both statistics must instead retain the paper's infinite penalty there. The G expression also contains individual logarithmic terms that may be negative before summation, so its extended value cannot be built by coercing each term directly to a nonnegative extended real.
The known support is represented by Fin n. Its members are labels for the paper's distinct points ; coordinates in Euclidean space are irrelevant to these tests. Laws use Mathlib's ProbabilityMeasure (Fin n) and its weak topology. The data are coordinates of the canonical infinite product law, with Lean index zero corresponding to the paper's first observation. The empty support has no probability law; all substantive instances have . The empty sample is defined by total operations but has no bearing on an eventual or infinitely often assertion.
Pearson's statistic lives in . The squared G statistic uses extended real arithmetic so finite negative summands can be combined with an infinite boundary term. Its region compares with , equivalent to the paper's at positive . The free stands for a fixed threshold constant, including the paper's chi square quantile; no particular quantile value is built into the theorem. This makes explicit the only property of that threshold used in §10.6: independence from .
Contributions may prove the four milestone statements, connect Mathlib's finite probability and strong law interfaces to the empirical frequencies, or establish finite support versions of Cauchy–Schwarz and Pinsker with the correct infinite boundary cases. A proof of the goal must use the stated regions and preserve simultaneous quantification over every moving sequence of laws; replacing uniform consistency by convergence of would remove its main claim.