Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A 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 ).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.
A queue layout represents a graph by placing its vertices in a line and assigning edges to queues. The order and assignment must prevent nested edges from sharing a queue. This gives a graph parameter that measures how much queue capacity is needed for a particular graph. Heath, Leighton, and Rosenberg asked whether one fixed number of queues suffices for every planar graph. The question remained open while bounds depending on the graph's number of vertices, degree, or treewidth were known. Dujmović, Joret, Micek, Morin, Ueckerdt, and Wood resolved it by proving a uniform bound of 49. Their paper also develops layered partitions, a structural tool used beyond queue layouts. These claims and the historical account appear in the source paper, pp. 3–5 and 16.
A finite simple graph has vertices and unordered edges . Choose a linear order of . Two disjoint edges nest when their endpoints appear as , with one edge joining to and the other joining to . A queue is a set of edges with no nested pair. A -queue layout is a vertex order together with an assignment of every edge to one of queues; means such a layout exists. Edges sharing an endpoint cannot nest. Empty queues are allowed, so an edgeless graph can use zero queues. These are the paper's definitions in §1, pp. 3–4.
A layering assigns vertices to layers such that endpoints of an edge lie in the same or adjacent layers. A BFS layering starts from one selected root in each connected component and places each vertex in the layer equal to its graph distance from that root. A vertex partition divides into disjoint nonempty parts. Its quotient graph has those parts as vertices; distinct parts are adjacent if an edge of joins them. An -partition may index the parts by vertices of another graph : the quotient's edges must be represented by edges of , while an indexed part may be empty. A partition has layered width at most with respect to a fixed layering if every part contains at most vertices of every layer. The exact definitions are in §2, pp. 7–9.
A graph is planar when it can be drawn in the plane with vertices at distinct points and edges as simple arcs that meet only at shared endpoints. A tree decomposition covers every vertex and edge of a graph by bags indexed by a tree, with the bags containing each vertex forming a connected subtree. Treewidth at most three means that a tree decomposition exists with every bag of size at most four. The paper uses these standard notions in §2 and §4, pp. 7, 12, and 16.
The goal is the explicit upper bound the paper derives for its Theorem 1:
The printed theorem says that planar queue-number is bounded, and the authors state 49 immediately after it. A bound that depends on would not express the result. The goal uses the paper's own constant, as given in Theorem 1 and the following sentence, p. 5.
The structural target is Theorem 15, p. 16: for every BFS layering of a planar graph, there is a partition of layered width at most three whose quotient remains planar and has treewidth at most three. The queue transfer target is Lemma 8, p. 10:
when has an -partition of layered width . Its layout orders vertices layer by layer. The milestone list also includes the rainbow characterization, the blowup lemma, the complete-graph queue number, and the five-queue bound for planar graphs of treewidth at most three. These are the stated supporting results along the route to 49 in §2–§4.1, pp. 7 and 10–16.
The goal establishes a constant queue bound for all planar graphs, independent of their size, degree, and treewidth. Theorem 15 supplies a reusable structural statement: even if the original graph has large treewidth, its quotient by small layer intersections has treewidth at most three while remaining planar. The paper goes on to treat graphs of bounded Euler genus and proper minor-closed classes, and describes connections with graph products and other graph parameters in its abstract and introduction, pp. 1 and 5.
The result is proved in the cited paper. This mission records Lean statements of the goal and six supporting milestones; their proofs remain to be formalized. A completed development would connect finite graph orders, nested-edge combinatorics, layered partitions, planar drawings, and tree decompositions in one machine-checked chain. The queue and partition definitions can also support later work on graph classes beyond the planar case.
A vertex order chosen without regard to a graph's structure can contain large rainbows, forcing many queues in that order. Planarity alone does not specify an order or an edge assignment, and a direct bound from ordinary treewidth does not cover planar graphs with arbitrarily large treewidth. The central structural requirement is to find a partition whose parts remain small in each BFS layer while its quotient has low treewidth. The queue transfer lemma must retain a layer-by-layer vertex order and account for edges within parts and between parts. The paper, pp. 10–11 and 16, identifies these as distinct constraints in its stated results.
Vertices form a finite type and edges are those of a Mathlib simple graph. A vertex order is an injective map into ; strict inequalities on four endpoints encode nesting. Queue assignments are functions on the graph's edge set, so the empty graph's zero-queue case is present. The statements use an existence predicate for , without taking a numerical infimum. Layerings are functions to , with BFS roots chosen separately for disconnected components. Theorem 15 uses a partition into nonempty parts, and the quotient has exactly those parts as vertices. Treewidth at most three uses a published tree-decomposition definition with bags of size at most four.
The locally checked drawing definition has the same fields as the published plane-drawing definition; the published module was unavailable from the local index in this run. Planarity means existence of a crossing-free drawing, not a drawing that permits crossings. The formulation does not use a universal edge carrier that would rule out zero queues, a non-strict nesting test, or a default numerical treewidth. The near-triangulation, Sperner, and tripod statements from the paper's deeper proof are outside this proposal's milestone scope; the partition theorem remains a full milestone. Solvers may contribute the omitted geometric and tree-decomposition infrastructure when proving it.
The Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the cutoff-80 mission already covers every , the new work is the range from 70 to 80.
The cutoff came down from 90 to 80 in under two days, through moona3k's proofs at 89, 88, 87, 85, 84 and 80. The step to 89 sharpened the estimates of the cutoff-90 argument, and the step to 85 added a new idea, a weighted pair-curvature and confinement estimate. How far these methods reach is not known; 70 asks for ten more units. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 70 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryIn a prophet inequality, a decision maker observes random rewards one at a time and must choose without seeing future realizations. The benchmark is a prophet who sees all rewards and selects their maximum. A nonadaptive threshold rule chooses a threshold for each reward before observations begin, then accepts the first arriving reward that crosses its threshold. This model captures a simple class of stopping rules and, through the prophet inequality connection, informs posted price mechanisms in which prices are set before buyers arrive. Correa et al. (2021) prove that under uniformly random arrival order some such rule earns at least a fraction of the prophet's expected reward. The question here is whether that guarantee improves when the reward distributions are identical.
Fix an integer and draw independent rewards from the same three point law. A reward is with probability , is with probability , and is otherwise. The three probabilities are nonnegative and sum to one for . Thus a typical sample contains roughly unit rewards, while a high reward is rare enough that its presence among all draws has probability on the order of . Its magnitude is on the order of , so it still makes a nonvanishing contribution to the prophet's expected reward.
Give each coordinate a predetermined threshold . A uniformly random order reveals the sampled rewards, and the rule accepts the first . Conditional on a sample, let . Each accepted coordinate is equally likely to arrive first among , so the conditional expected reward is
Write for the rule's reward and for the prophet's reward. These are expectations of nonnegative random variables. The thresholds may be infinite, allowing a coordinate to be discarded in advance.
The goal is the paper's i.i.d. tightness claim: for every , sufficiently large members of this explicit family satisfy
The universal quantifier includes every nonadaptive threshold vector, including asymmetric thresholds and coordinates that are never accepted. The proof in Appendix B supports the displayed statement for every sufficiently large , which strengthens the existence of one hard instance stated in Section 3.1. Together with the paper's lower bound, this shows that the factor cannot be raised for this rule class even under identical distributions.
The milestones cover the prophet limit , reduction of arbitrary thresholds to two-level rules, the three contributions to a two-level rule's expected reward according to the number of high observations, Proposition A.3's scalar maximization, and the resulting uniform asymptotic bound on all two-level rules. The first coordinates of a two-level rule accept both and ; the remaining coordinates accept only . These targets correspond to Section 3.1, Proposition A.3, and Appendix B of Correa et al..
The explicit i.i.d. family locates a limit of nonadaptive thresholds under random arrivals. Identical distributions remove heterogeneity as an explanation for the loss against a prophet: the obstruction remains even when every reward has the same law. Consequently, an improved guarantee requires a richer rule class or additional assumptions on the distribution. The paper studies an adaptive threshold rule separately and obtains a stronger i.i.d. guarantee; this mission isolates the upper bound for the nonadaptive class.
Formalizing this result supplies a reusable model for random-order threshold selection on a finite i.i.d. product space, including its conditional reward formula and extended nonnegative expectations. The paper proves the tightness result; the Lean declarations in this proposal state it and its supporting results as proof obligations. The published i.i.d. product-measure model from the Samuel-Cahn development already has machine-checked definitions and is reused here. The proposed upper-bound theorems have not yet been proved in Lean.
Bounding each coordinate's expected contribution in isolation loses the interaction between unit rewards and the rare high reward. When a high reward occurs, accepting many unit rewards can dilute its share of the random-order reward; rejecting unit rewards sacrifices ordinary samples. The reduction to two-level rules must apply to every threshold vector before the count of unit-accepting coordinates can be optimized. Appendix B then controls the cases of zero, one, and at least two high observations uniformly in that count. The one-high-value case contains a printed final inequality that drops a positive term; the formal target uses the preceding, valid bound, whose extra term vanishes in the limit.
Lean represents a sample as Fin (n ^ 2) → ℝ and its law as a finite product measure. The index set is 0-based: the paper's are coordinates . The law is used only for , where it is a probability measure. Thresholds have type , and crossing is strict, matching Theorem 1's indicator . The page describes its two-level rule with weak threshold language; under strict crossing the same acceptance sets use thresholds and . The reward uses the paper's convention. Expectations are lintegrals with values in $[0,\infty]`, avoiding a zero default for nonintegrable real integrals. The goal quantifies over all threshold vectors and uses the actual prophet expectation of the same law; no restricted rule class or surrogate benchmark can replace either one.
The general i.i.d. law, sample maximum, and expected maximum come from SamuelCahnProphet.IID.Setting. The paper's three point law, random-order reward, canonical two-level rule, and high-value count are local definitions. Useful contributions include exact finite-law calculations, dominance of two-level rules, uniform estimates in , and the scalar exponential inequality of Proposition A.3. These parts can also support formal work on other finite-support prophet inequalities.
Boundary control of a transport equation acts at the edge of a spatial interval, while the state evolves throughout the interval. A backstepping transformation connects the original state to a simpler target state by integrating against kernels on a triangular region. The transformation is useful only when those kernels exist with the regularity and uniqueness needed to define a single feedback law. Coron, Vazquez, Krstic and Bastin use this construction for a two-component quasilinear hyperbolic system. Their Appendix A isolates a four-component linear kernel system and proves its well-posedness independently of the later stability arguments (Coron et al., Appendix A).
This mission concerns that appendix result. The paper states a generic system broad enough to include the kernel equations arising from its controller design. Its goal is a unique continuous solution on the closed triangle, assuming continuous coefficients and strictly positive transport speeds. The result supplies the existence and uniqueness premise for the paper's later linear and quasilinear stabilization results. It is a proved result in the source preprint; the work here is to state its analytic content precisely in Lean and leave its proof as a formalization target.
Let . There are four unknown real functions on . Two positive, continuous functions describe the characteristic speeds. Four functions supply forcing, and sixteen functions couple the unknown components. The functions and are continuous on . Boundary functions are continuous on . The paper's equations (A.1)–(A.4) have first-order directional derivatives of on the left and on the right (Coron et al., p. 18).
The boundary data have two forms. Components and are prescribed on the diagonal : and . Components and are prescribed on the lower edge with linear dependence on and . For example, . The fourth component uses in the same way. Those edge couplings are part of the problem, rather than optional side conditions.
For merely continuous , a classical partial derivative need not exist. Accordingly, the mission uses the paper's characteristic integral equations (A.23) as the meaning of solution. The travel-time coordinates are for , with . Each characteristic starts on the prescribed part of the boundary and ends at . The value of equals its starting boundary value plus the forcing and coupling integrals along that characteristic. A continuously differentiable solution of the differential equations and the boundary conditions satisfies this integral form (Coron et al., pp. 19–20).
The goal is Theorem A.1: for every set of data with the continuity and positivity assumptions above, there is a continuous characteristic solution on , and any two such solutions agree at every point of :
Four source results mark the path to that goal. Lemma A.3 keeps every characteristic in and records its continuity and coordinate inequalities. Lemma A.4 bounds the integral of the th power of its first coordinate by . Lemma A.5 bounds one application of the linear integral operator to an increment satisfying a factorial estimate. Proposition A.6 bounds the resulting infinite series by (Coron et al., pp. 19, 21–23). These are the mission's four milestones.
Theorem A.1 fixes a genuine mathematical issue behind the feedback construction: a kernel cannot be treated as an arbitrary coefficient of a controller when its defining boundary problem has not been solved. Existence gives a kernel for the transformation; uniqueness makes that kernel determined by the coefficient data. The theorem is stated for a generic coupled system, so the same result can support several kernels rather than just one equation in the control design (Coron et al., Appendix A).
Formalizing this known proof would add a reusable interface for characteristic coordinates, bounded coefficient functions on a triangle, and coupled Volterra-type integral operators. The present proposal contains statements, not completed proofs. The local prior-art search found no published Goursat kernel item with the same four-component system and boundary conventions. The broader paper's linear and quasilinear stability results are separate missions; this one records their analytic kernel prerequisite without importing their controller definitions.
The mixed boundaries make the usual one-direction transport picture insufficient. Two characteristic families enter from , while two enter from the diagonal. Moreover, the lower-edge values of and depend on the other components at that edge. Thus a bound for one component cannot ignore the other three or assume all boundary values are given independently. A candidate continuous solution must also be shown to agree with the same integral equations at the corner and along both boundary segments. The explicit characteristics involve the inverse of , whose argument and range must be checked throughout (Coron et al., pp. 19–23).
The Lean data bundle contains globally defined real functions, with continuity and positivity imposed only on or . Such functions represent continuous data on those closed domains by extension; values outside the domains do not enter the statements. The four components use Fin 4, indexed in Lean for the paper's . The two lower-edge couplings and the two diagonal values are all included in IsCharSolution. Equality in the uniqueness clause is restricted to , because the extensions outside it are unconstrained.
The coordinate inverses are Function.invFunOn on ; only arguments in their ranges have mathematical meaning here. Lemma A.3 includes the domain facts that keep the characteristics in range. Integrals are over finite characteristic intervals with continuous integrands, and the maxima in (A.35) are suprema of continuous images of compact sets, not suprema over all real inputs. Proposition A.6 asserts summability before using an infinite sum. Lemmas A.4 and A.5 include , a valid base case needed by the source's induction. Lemma A.5 makes the continuity of the increment explicit so its integrals retain their intended values. Existence and uniqueness both remain in the goal; retaining only one would change Theorem A.1. Two formalizations would trivialize or falsify the goal and are ruled out: dropping the boundary conditions (A.5)–(A.7) from the solution notion makes uniqueness false, and reading the PDEs (A.1)–(A.4) classically for a merely continuous would make existence false; the solution notion is the paper's characteristic integral form with all boundary conditions. Contributions to the characteristic and operator estimates, continuity of the constructed limit, and the uniqueness argument are within scope.
Least-squares regression, for a tall matrix with , is among the most frequently solved problems in numerical computation. Direct methods (QR or SVD) cost time, which is prohibitive when is in the millions. Sketching replaces the problem by a much smaller one: choose a matrix with , form and , and solve instead. The question is when the solution of the small problem is nearly optimal for the original one.
Clarkson and Woodruff, Low Rank Approximation and Regression in Input Sparsity Time (STOC 2013; JACM 2017), showed that a very sparse random sketch (one non-zero per column, the CountSketch matrix) can be applied in time proportional to the number of non-zero entries of and still yields -approximate regression and low-rank approximation. §7 of that paper isolates the deterministic part of the argument: two conditions on a fixed sketch that guarantee a near-optimal solution, whatever distribution produced .
Timeline. Sarlós (FOCS 2006) introduced sketch-and-solve regression with fast Johnson–Lindenstrauss transforms. Drineas, Mahoney, Muthukrishnan and Sarlós (Numer. Math. 2011) stated the structural conditions for single-response regression (their Lemma 1); Theorem 36 of Clarkson–Woodruff generalizes it to multiple responses. Clarkson and Woodruff then supplied the sparse sketches meeting the conditions in input-sparsity time.
All matrices are real. For a vector let ; for a matrix let . Fix of rank at most , a right-hand side and a sketch . Let be the column space and a matrix with orthonormal columns () spanning .
If is a subspace embedding for with and satisfies the event of Lemma 32 for with error parameter , then every sketched minimizer satisfies
This is the explicit form the paper's proof establishes; the printed bound on norms follows after rescaling .
Theorem 36 separates the algorithm design for sketched regression from its correctness proof: any random construction (CountSketch, subsampled randomized Hadamard transforms, leverage-score sampling, Gaussian matrices) yields a -approximate regression solver once it is shown to satisfy the two conditions with constant probability. Clarkson and Woodruff use it for their input-sparsity-time regression algorithm (Theorem 38) and, through Theorem 39 and affine embeddings, for low-rank approximation. The same conditions recur throughout the randomized numerical linear algebra literature (see Woodruff's survey Sketching as a Tool for Numerical Linear Algebra, 2014).
The results are proved in the paper (§7.3, §7.5 and Appendix A, p. 37). To our knowledge none has a machine-checked proof. Formalizing them produces a reusable, distribution-free layer of sketching theory: the probabilistic statements about specific sketches can then be proved separately and composed with it.
The obvious argument applies the subspace embedding to the residual , but that vector does not lie in , so an embedding of alone says nothing about it; embedding augmented with the columns of instead costs a sketch dimension that grows with . The hypotheses of Theorem 36 control the optimal residual only through the approximate-product condition, which is far weaker than norm preservation, and the difficulty is to transfer that control to the sketched solution (Lemma 37) with the constants and . A second obstacle is the passage from a general of rank at most to an orthonormal basis of : it changes , which is why the approximate-product condition is stated for .
Matrices are Matrix (Fin m) (Fin n) ℝ; squared norms are explicit sums sqNorm and frobSq; the column space is the range of Matrix.mulVecLin; rank is Matrix.rank. Everything is deterministic: is an arbitrary fixed matrix and no probability space appears. The committed conventions are:
A trivializing formalization is ruled out: is never defined as , the approximate-product hypothesis is an inequality and not the exact identity , is non-negative, and the goal is stated for general of rank at most , not only for orthonormal . The hypotheses are jointly satisfiable (for instance ).
A complete development needs the Frobenius inner product and its Pythagorean identity, the normal equations for matrix least squares, the existence of the Moore–Penrose inverse, and the spectral-norm bound for a symmetric matrix from its quadratic form; all are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Theorem 36, are welcome.
An intermediary such as a ride platform must attract buyers and sellers who arrive at different times. A buyer may wait for a seller; a seller may wait for a buyer. Both sides can choose when to request a match, so an ask price and a bid price affect participation as well as the intermediary's margin. Chen and Hu study whether a simple posted-price policy remains profitable despite this waiting and the uncertainty of arrivals. Their submitted manuscript proves a finite-market guarantee and an asymptotic rate for the policy used here. The proof appears in its Supplemental Note, while the model and theorem are in the main text.
Buyers arrive during a horizon as a Poisson process of rate , and sellers arrive independently at rate . A buyer's valuation has density on and a seller's cost has density on . Marks are independent of arrival times. A buyer and a seller each trade at most one unit. If they wait after arrival, they incur costs and per unit time, respectively. The paper assumes regularity: the buyer's virtual value and the seller's virtual cost are weakly increasing on their supports. Here .
A clairvoyant assignment knows all arrivals through . For each possible buyer–seller pair it assigns virtual surplus less the waiting cost determined by their arrival order. It chooses a partial matching with greatest total value, denoted . A separate fluid program chooses a measurable, nonnegative pair of price trajectories that clears demand and supply at every time. Its optimal value is . These are different objects: is random and uses indivisible agents, whereas is a deterministic continuous-flow optimum. Lemma 2 of the manuscript compares their values in expectation.
Let be the greatest volume in with nonnegative marginal virtual surplus. The buyer and seller prices are inverse-distribution prices at that volume. Proposition 1 states that these constant prices attain the fluid optimum and .
The greedy matching policy pairs requests first come, first served. Under the waiting-adjusted fixed-price policy, a buyer's posted ask is minus times a conditional expected wait per match probability; the seller's posted bid is plus the corresponding term. The buyer adjustment is conditioned on the observed pre-arrival inventory signal. Agents request immediately exactly when their valuation or cost crosses the base-price threshold. The policy's expected profit is computed from posted prices paid by successfully matched agents.
The first target is the paper's finite-market bound:
When , the benchmark comparison also gives . For scaled systems with arrival rates and , where both exponents are positive, the second target is a constant independent of such that
The milestone list follows the source's Proposition 1, Lagrangian relaxation, Lemma 2, Poisson request counts, policy profit identity, Gallego–van Ryzin moment bound, and Lemma S.5 on arrival-rate monotonicity. The last three supply the finite bound and its scaling statement in the Supplemental Note.
The finite bound quantifies the cost of using fixed base prices and greedy matching instead of the fluid ideal. Its two terms separate the loss from random mismatch and the extra waiting adjustment. The scaled bound says that, as both sides' arrival rates grow, the fraction of the fluid value lost by this policy vanishes at a rate governed by the slower-growing side. This offers a concrete reason to use a simple policy when the market is large, while keeping the smaller-market correction visible.
The paper already proves these claims. This mission asks for machine-checked proofs of their precise statements. The fluid optimizer, the clairvoyant matching problem, the marked Poisson arrival model, and the policy-profit identity are reusable mathematical objects beyond this theorem. The positive-part moment bound is an already published theorem and is referenced rather than posed again.
The obvious comparison between posted-price profit and fluid revenue misses the cost of requests that wait or never match. The price corrections themselves are conditional expectations divided by conditional match probabilities; their effect cannot be captured by simply subtracting a constant waiting charge. The proof must connect those corrections to the time integral of the queue imbalance, then control the imbalance of two Poisson request streams. A second difficulty is that the fluid optimum and the expected clairvoyant optimum are defined through different feasible sets, so their comparison needs a separate relaxation argument. These obstacles are visible in the source's proof of Lemma 2 and Theorem 2.
The density and virtual-value environment is the published bilateral-trade definition, imported through a local name alias required by the frozen shared market module. Lean represents arrivals by independent Poisson counts and independent identically distributed time-and-value marks. This is equal in law to the paper's homogeneous marked Poisson processes on . Arrival time marks are uniform probability laws, and valuation and cost marks use the source densities. Simultaneous requests are ordered by index; such ties have probability zero. The deterministic program ranges over measurable, nonnegative, market-clearing paths with interval-integrable objective terms. Its value is the supremum of their objectives, not a formula involving and ; Proposition 1 must establish that formula. The clairvoyant value uses the published partial-assignment-game worth, so negative-weight pairs may remain unmatched.
The density functions are continuous on their supports, an explicit addition needed for the inverse prices and maximum volume used by Proposition 1. The lower support endpoints are nonnegative so the constant prices belong to the nonnegative fluid price domain; this fills an implicit domain convention in the manuscript. For Theorem 2 the overlap condition is strict, , ensuring positive and . The printed chain comparing and is stated under : when the numerator is negative, the claimed direction fails. Both expectations used as finite numbers are accompanied by integrability conclusions. Division by a zero match probability at the terminal time uses a zero convention on a set of arrival times with probability zero.
The policy model builds in the myopic request behavior that Theorem 1 identifies as an equilibrium; its strategic proof is outside this mission. The policy profit is the expectation of actual posted-price payments, and the waiting compensations are literal tagged-arrival conditional ratios. Contributions that prove the inverse-distribution properties, Poisson thinning, queue profit identity, fluid optimization, or final moment estimate all address parts of the stated target.
An associahedron of dimension is a simple polytope whose nonempty faces correspond, reversing inclusion, to the sets of pairwise non-crossing diagonals of a convex -gon: its vertices are the triangulations of the polygon and its facets are the diagonals. Associahedra appear in the combinatorics of parenthesizations (Tamari, Stasheff), in the theory of cluster algebras of type , where the Chapoton–Fomin–Zelevinsky construction realizes the cluster complex as the normal fan of a polytope, and in the study of secondary polytopes (Gelfand–Kapranov–Zelevinsky).
Many different polytopes realize the associahedron. Ceballos, Santos and Ziegler (arXiv:1109.5544v2) compare them up to normal isomorphism, a linear isomorphism of normal fans. One of the families they study, the "type II" family, is a construction of Santos presented at a conference in 2004 and first published in that paper (§5, pp. 18–23). It produces one associahedron for every triangulation of the -gon, the seed triangulation, and contains the Chapoton–Fomin–Zelevinsky associahedron as the case of the snake seed. This mission formalizes the statement that the construction works for every seed: Theorems 5.1 and 5.2 of the paper.
Let and , and number the vertices of a convex -gon counterclockwise. A diagonal joins two non-adjacent vertices; two diagonals cross when their endpoints are distinct and alternate around the boundary; a triangulation is a maximal set of pairwise non-crossing diagonals, and has elements. Two triangulations differ by a flip when and .
Fix a triangulation and let , with basis vectors , . Santos' vectors (p. 19) are
For a set of diagonals, is the cone spanned by the vectors , . The fan is the collection of the cones for all non-crossing sets , the empty set giving .
The cones of the triangulations form a complete simplicial fan when the vectors of each triangulation are linearly independent, every vector of lies in one of these cones, and any two of them meet in the cone of their common diagonals.
For a polytope and , the exterior normal cone is , where . The normal fan of is the set of all , , one cone for each nonempty face (p. 5).
For every triangulation of the -gon,
A polytope with normal fan is an -dimensional associahedron. The goal fixes no weights and no right-hand sides: it asserts only that some polytope has this normal fan.
Theorems 5.1 and 5.2 are what make Santos' family a family of associahedra at all. Every later statement of the paper about type II, including the classification up to normal isomorphism (Corollary 5.7: seeds agreeing up to rotation and reflection) and the identification of the Chapoton–Fomin–Zelevinsky associahedron as the only realization of both types (Theorem 6.1), compares the fans , and the word "associahedron" in them rests on these two theorems. The construction yields Catalan-many fans with facet normals in -coordinates, and modulo rotations and reflections they are pairwise non-isomorphic.
The theorems are proved in the paper; to the best of a search of the Prove2Me catalogue, nothing about normal fans of polytopes, complete simplicial fans or associahedra has been formalized there, and Mathlib at the pinned revision has no notion of fan. The formalization would provide a machine-checked polytopality criterion for complete simplicial fans (Lemma 5.4), an explicit flip analysis of Santos' vectors (Lemma 5.3), and a polytopal realization of the associahedron for every seed.
Theorem 5.1 is not a direct computation. Linear independence of each triangulation and a sign condition for each flip do not by themselves make a fan; the paper combines them with assertion (1), a region covered by exactly one cone, and appeals to a covering criterion for vector configurations (De Loera–Rambau–Santos, Triangulations, Cor. 4.5.20, properties (ICoP) and (IPP)). A solver will likely need to formalize that criterion, or an equivalent argument that a pseudo-manifold of simplicial cones with these properties covers the space exactly once.
Lemma 5.3 requires a case analysis of how the seed triangulation meets the quadrilateral of a flip; the paper distinguishes four configurations, each with its own dependence (equations (4)–(7), p. 21), and showing that the four are exhaustive is itself a combinatorial statement about triangulations. Lemma 5.4 requires constructing a polytope from weights and identifying all of its normal cones, including the lower-dimensional ones, with the cones of the fan. Finally, the uniform constant has to work for all flips at once; for the dependence (4) the unperturbed weights ( on , elsewhere) give exactly zero, so a perturbation is unavoidable and must not spoil the other cases.
Vertices of the polygon are Fin (n + 3), chords are Sym2 (Fin (n + 3)), and diagonals, crossing and triangulations are reused from the published definition ChvatalArtGallery.FanPartition.Triangulation. The space is {d // d ∈ T₀} → ℝ, coordinate being the coefficient of . Cones are nonnegative hulls (PointedCone.hull ℝ). The fan contains every face, including .
"Normal fan of a polytope" is encoded as: is the convex hull of a finite set, and the set of cones equals with exterior normal cones, functionals identified with vectors by the coordinate pairing. Because is a cone of , the polytope must be full-dimensional; a point, a lower-dimensional polytope, or "some polytope whose facet normals are the rays" does not satisfy the goal. The inner-normal convention would give the fan , which is a different statement. The polytope is specified only through its normal fan, as in the paper.
Lemma 5.4 is stated for fans whose rays are indexed by the diagonals and whose maximal cones are the triangulations, the case in which the paper uses it; adjacent maximal cones are flip pairs. Lemma 5.3 requires the two coefficients to be strictly positive, as assertion (2) does, so the zero dependence is excluded. The ε of milestone 6 is quantified as . The weight is computed on 0-based positions as for , which equals the paper's 1-based .
A complete development needs basic fan theory (simplicial cones, a covering criterion), the polar construction behind Lemma 5.4, and the flip case analysis. The first two are reusable beyond this mission, for any polytopality argument on simplicial fans. Contributions of general lemmas on simplicial cones and on normal cones of polytopes are welcome.
An associahedron is a polytope whose faces encode ways to dissect a convex polygon without crossing diagonals. Its vertices represent triangulations. Associahedra occur in geometric combinatorics because the same combinatorial object admits many geometric realizations. Ceballos, Santos and Ziegler ask when two such realizations have the same normal fan up to a linear change of coordinates. This question distinguishes geometric constructions that have identical face lattices but different arrangements of facet normals. Their Santos family is indexed by seed triangulations, so its classification asks exactly how much of a seed can be recovered from its fan. Ceballos, Santos and Ziegler, §5.3.
Santos' construction was presented at a conference in 2004 and first appeared in print in this paper. The paper proves that the number of normal-isomorphism classes in this family is the number of polygon triangulations modulo rotations and reflections. It also explains a useful limit of the result: the set of normal vectors alone determines only the abstract dual tree of the seed triangulation, while the fan retains the further information needed for classification. Ceballos, Santos and Ziegler, §5 and Proposition 5.8.
Take a convex polygon with vertices in cyclic order and label its positions . A diagonal joins two nonadjacent vertices. A triangulation is a maximal collection of diagonals with no crossings. Each triangulation has diagonals. A flip removes one diagonal shared by two triangles and inserts the other diagonal of their quadrilateral.
Choose a seed triangulation . Let , with a coordinate for each seed diagonal . Santos assigns a vector to every polygon diagonal :
For each noncrossing set of diagonals, take the cone spanned by the vectors , , with nonnegative real coefficients. The collection of these cones is the fan . The paper proves that it is complete and is the normal fan of an associahedron. This mission uses that explicit fan as the meaning of , following the paper's own convention in §5.3. Ceballos, Santos and Ziegler, pp. 19, 23, Theorems 5.1–5.2.
Two fans are normally isomorphic here when an invertible real linear map sends every cone of the first to a cone of the second. A dihedral symmetry is a rotation or a reflection of the cyclically ordered polygon. It acts on a triangulation by relabelling both endpoints of each diagonal. Write when such a symmetry sends to .
For every and triangulations of the -gon, the goal is Corollary 5.7:
The left side compares all cones of the two fans through a linear isomorphism. The right side permits only the rotations and reflections of the polygon. It makes no choice of an ordering for the diagonals within either seed.
The milestone list follows the paper's argument: the polygon symmetry theorem for the associahedron's face lattice (Lemma 2.2); the induced crossing and parallelism preserving bijection of diagonals; the description and count of parallel facet pairs for Santos fans (Proposition 5.5); the injectivity of , where contains a seed and all single-flip insertions (Lemma 5.6); and invariance under rotations and reflections. Ceballos, Santos and Ziegler, pp. 6, 23–24.
The classification says precisely which apparent choices of seed triangulation are redundant. In particular, different dihedral orbits produce different normal-fan geometries even though all the resulting polytopes have the associahedron's face lattice. Parallel facet pairs supply an intrinsic geometric trace of the seed: they correspond to each seed diagonal and its flip. Lemma 5.6 then separates distinct seeds from their collections of these pairs. Ceballos, Santos and Ziegler, Proposition 5.5, Lemma 5.6 and Corollary 5.7.
The result is proved in the paper. The formalization work is to give a machine-checked account of its fan model and classification, including the polygon combinatorics and the linear-algebraic implications of a fan isomorphism. The supplied statements are proof targets, with sorry at theorem bodies; a complete Lean proof of the classification is not yet claimed. The explicit diagonal and crossing representation and the seed-indexed vector construction can also be reused to formalize the paper's fan and polytopality theorems.
A face-lattice isomorphism alone does not identify the seed: every associahedron in the family has the same face lattice. A first attempt to compare only the vectors also loses information. Proposition 5.8 shows that two different seed triangulations with isomorphic dual trees can yield linearly equivalent vector sets. The full fan records which vectors span cones together. The central task is to recover a crossing-preserving map of diagonals from a linear map of fans, then use the opposite directions of facet normals to recover . Ceballos, Santos and Ziegler, pp. 23–24, Propositions 5.5 and 5.8.
Lean represents polygon positions by Fin (n + 3) and unordered diagonals by Sym2; crossings and triangulations come from the published Chvátal triangulation definition. The ambient real vector space for a seed is the function space on the subtype of its actual diagonals. This makes the basis intrinsic to . A cone is the nonnegative real hull of the Santos vectors attached to a noncrossing diagonal set. NormallyIsomorphic demands a real linear equivalence of these ambient spaces. The classifying symmetry is explicitly or modulo .
No premise asserts the classification, and the fan is built from the paper's vectors rather than from a chosen list of abstract cones. Arbitrary permutations of diagonals, nonlinear maps, and an abstractly isomorphic dual tree do not satisfy the target's symmetry condition. The goal and the diagonal-action clause of Lemma 2.2 cover every ; the separate group-order clause in Lemma 2.2 applies for . Lemma 5.6 carries the printed bound . The triangular and quadrilateral cases are included in the goal and require their own boundary treatment in a proof. Contributions on crossing preservation, ray distinctness, linear independence of maximal cones, single-flip combinatorics, and dihedral equivariance are welcome.
Many matrix algorithms spend most of their time reading their input. A matrix with few nonzero entries should admit routines whose cost scales with that number, rather than with the product of its dimensions. Clarkson and Woodruff study random maps that compress a matrix before a regression or low rank approximation calculation while retaining the geometric information those calculations need. Their sparse embedding has one nonzero entry per input coordinate, so applying it to a sparse matrix can be charged to the matrix's nonzero entries. The probability guarantee for its geometry is Theorem 11 of the preprint, the target of this mission.
The paper proves further results for faster regression and low rank approximation after sketching. Those applications use the subspace guarantee as an input. This mission concentrates on that guarantee and the statements in §3 that support it. The source is the 5 April 2013 arXiv version; theorem and page labels below refer to that version.
Fix a real matrix of rank . Its column space is . A map is a subspace embedding for when it approximately preserves the length of every vector in simultaneously. The dimension , rather than the number of rows , controls the size required of the compressed space.
Here is the sparse embedding matrix . Each input coordinate independently chooses one bucket uniformly. The binary matrix has a at and zero elsewhere in column . Independently, is diagonal with a fair sign or at each coordinate. Thus the output in bucket is the signed sum of input coordinates assigned to . The probability in this mission is over the joint, uniform choice of all bucket assignments and signs, with fixed in advance. This is the construction in §2, p. 7.
For an orthonormal basis matrix of , the leverage score of row is . A threshold separates light coordinates, with , from heavy coordinates, with . The paper describes this split after sorting rows by leverage; the threshold description selects the same coordinates and keeps the input's original order. The bucket event bounds the sum of light leverage scores assigned to each bucket. The heavy event says that distinct heavy coordinates receive distinct buckets. These are properties of alone; the later concentration statements take probability over the independent signs after fixing a suitable .
There is an absolute constant such that for every of rank , every , and every integer ,
The event contains the universal quantifier over : one draw must work for the whole column space. The squared-norm estimate implies the norm formulation printed in Theorem 11, p. 11 on this range of . The paper gives its proof in §3, pp. 7–11.
The milestone list follows the paper's statements: a coordinate bound from §3.1; the weighted bucket estimate of Lemma 2; light-coordinate concentration in Lemma 3; the collision and exact-preservation statement of Lemma 5; the heavy-light cross-term estimate in Lemma 6; fixed-vector preservation in Lemma 7; and the passage to the whole subspace in Lemma 8. Their distinct probability spaces matter. Lemmas 2 and 5 concern bucket assignments, Lemmas 3, 6, and 7 concern signs for a fixed suitable assignment, and Lemma 8 is a general statement about a random linear map.
Theorem 11 gives a single compact random matrix that retains the Euclidean geometry of every vector in a specified rank- column space with probability at least . It supports sketch-and-solve algorithms: a computation performed on can use a much smaller row dimension while reasoning about the original column space. The construction also has exactly one nonzero per column, the structural fact behind its input-sparsity running time. The running-time bound is stated in the paper, but this mission's Lean target concerns the mathematical norm guarantee.
The paper already proves the theorem; the open work here is a machine-checked development of its statement and proof. The finite probability model, explicit squared norms, leverage scores, and bucket events can support later formalizations of other sparse sketching results. No machine-checked proof of Theorem 11 is claimed by this proposal. A complete development may reuse proved concentration inequalities from Mathlib or the platform, but the cited inequalities need their hypotheses checked against the finite-sign and weighted-bucket models used here.
A fixed-vector estimate does not itself imply that one random sketch works for all vectors of an uncountable subspace: the quantifier cannot simply be moved through the probability. Collisions also have different effects on high- and low-leverage coordinates. Heavy coordinates need a no-collision event; light coordinates can share buckets only while their total bucket weight remains controlled. The paper's statements keep these events and probability spaces separate. The final whole-subspace claim requires a uniform estimate whose failure probability accounts for the dimension .
Vectors are functions Fin n → ℝ, matrices are finite real matrices, and and are explicit sums of coordinate squares. The sample space is the product of all bucket maps and all Boolean sign assignments, with counting probability. Every theorem with a freely chosen bucket count assumes ; otherwise a Fin 0 sample space could make division by its cardinality meaningless. The theorem's size threshold forces this automatically when and . Matrix rank is Mathlib's matrix rank.
The formalization fixes in Theorem 11. The upper bound prevents the logarithmic size expression from degenerating near , and keeps its logarithm and division meaningful. Positive and are explicit where needed; Lemma 6 restricts . The heavy/light split uses leverage thresholds rather than a row permutation, and constants described as absolute are quantified before every dimension, matrix, error, and failure parameter. In particular, Theorem 11's event quantifies over all inside the probability, while Lemma 7 fixes before sampling signs. These choices exclude degenerate distributions, vacuous error ranges, and a fixed-vector claim masquerading as the goal.
The refined clause at the end of Theorem 11 is left out: its printed conflicts with the proof's collision requirement , and its threshold parameter is not fixed in the claim. Lemma 1 and the cited Hanson–Wright moment result, Theorem 4, are proof tools outside this proposal's milestone set. Contributions that formalize those tools faithfully, prove the bucket and sign estimates, or connect the finite model to existing probability libraries are useful for the goal.
An associahedron is a polytope whose vertices represent triangulations of a convex polygon and whose edges represent flips between triangulations. The same combinatorial polytope can be realized in different vector spaces with different facet directions. This matters when a construction uses the geometry of the realization, rather than only its face lattice: a linear change of coordinates can preserve its normal fan, while a general combinatorial relabelling need not. Ceballos, Santos and Ziegler compare three constructions and use parallel facets to distinguish them.
Two of those constructions form large families. Hohlweg–Lange choose a word of signs; Santos chooses a triangulation as a seed. Both yield associahedra, and both include the Chapoton–Fomin–Zelevinsky (CFZ) realization. The paper proves that CFZ is their only shared normal-isomorphism class. Its Theorem 6.1 is the target here; the result was announced as Theorem 1.1 in the introduction. Source, pp. 4 and 28.
Fix and a convex polygon with cyclically ordered vertices. A diagonal joins two nonadjacent vertices. Two diagonals cross when their endpoints alternate around the boundary. A triangulation is a maximal collection of pairwise noncrossing diagonals. Every triangulation has diagonals, and replacing one diagonal with the other diagonal of the quadrilateral it borders is a flip. The faces of an associahedron correspond to noncrossing sets of diagonals, while its vertices correspond to triangulations. Source, pp. 5 and 18–19.
A normal fan records the outward normal directions of all faces of a polytope and the cones they span. Two complete fans are linearly isomorphic when a real linear equivalence sends every cone of the first to a cone of the second. Polytopes are normally isomorphic when their normal fans are linearly isomorphic. This is Definition 2.1 of the paper; the comparison is geometric because it requires a linear map. Source, p. 5.
For the Hohlweg–Lange family, choose a sign word and extend it to on the labels . The negative labels, in increasing order, form one boundary chain; the positive labels, in decreasing order, form the other. For a diagonal with endpoint labels , let contain the labels strictly below it. Form by replacing with and with if those labels occur in . The characteristic vector of , considered modulo the all-ones vector, gives its facet normal. Source, pp. 14–16, Definition 4.1.
For the Santos family, choose a seed triangulation and use one basis vector for each seed diagonal . The normal assigned to a diagonal is when . Otherwise it is the sum of over seed diagonals crossing . The cones spanned by compatible diagonal vectors give the fan. The distinguished snake seed joins alternating polygon positions ; this seed gives the CFZ fan. Source, pp. 13 and 18–19.
Let and be the two normal fans, and let be the fixed snake. If is a triangulation, the target says
and it also asserts that . Together these are the uniqueness and existence parts of Theorem 6.1. The result covers dimensions zero and one as well as higher dimensions; Lemma 2.2 uses only for its second sentence, the uniqueness of the inducing symmetry. Source, pp. 6, 16 and 28–29.
The milestone list follows the paper's stated intermediate results: polygon symmetries of the associahedron, the parallel-facet pairs in each family, and the three properties of triangles in the seed that force the snake. Proposition 4.4 supplies the alternating-sign realization used for existence. The parallel-pair targets retain the source's exact count of pairs, through their characterization by the seed flips or the labelled quadrilaterals. Source, pp. 6, 16–17, 23 and 28–29.
Theorem 6.1 gives a complete answer to a comparison question that face-lattice data alone cannot settle: every member of either family has the same associahedral combinatorics, but almost no cross-family pair has linearly equivalent normal fans. It identifies the exceptional class without fixing coordinates for either construction. The characterization of parallel facets also gives a concrete invariant for later comparisons among associahedron realizations. Source, pp. 23 and 27–28.
The paper proves the result mathematically. A complete Lean development would add machine-checked definitions of the two ray systems and a proof of the classification, including the geometric step that a linear fan isomorphism induces a compatible correspondence of facet rays. The polygon triangulation and crossing definitions are already available as a published reusable component; proofs about fans and the two constructions are the remaining work.
An isomorphism of abstract face lattices gives too little information: it exists between all associahedra of the same dimension. The useful comparison must control a linear map on the actual normal vectors. The first obstacle is proving that such a map preserves the rays and therefore preserves which facets are parallel. Then the two explicit descriptions of parallel pairs must be reconciled, and the resulting sign restriction on a triangulation must force alternating turns of its dual path. Showing only that the dual tree is a path is insufficient; path triangulations can make consecutive turns on the same side. Source, pp. 17, 23 and 28–29.
Vertices are Fin (n+3) in counterclockwise positions, with zero-based indexing; Hohlweg–Lange signs apply to labels carried by those positions. Diagonals are unordered pairs. The imported Chvátal triangulation definition gives boundary edges, crossings, maximal noncrossing sets, and their triangles. A cone is the nonnegative span of the vectors assigned to a noncrossing set. The type I vectors are represented in using quotient coordinates ; type II vectors are functions on the seed diagonals. Hohlweg–Lange Proposition 4.3, cited in the paper, identifies the maximal cones of the type I normal fan with triangulations. Source, pp. 15–16.
Normal isomorphism uses a real linear equivalence, dihedral symmetry uses only rotations and reflections of the polygon, and the snake is the explicit alternating triangulation. The cones use the actual facet vectors. These commitments exclude a mere bijection of index sets, an arbitrary permutation of vertices, and a path triangulation with nonalternating turns. The condition appears only where the page has it, in the second sentence of Lemma 2.2 (uniqueness of the inducing symmetry); facet-normal comparisons quantify only over diagonals, exactly the facets represented in the paper. Reusable contributions include combinatorial flip lemmas, linear independence of triangulation rays, and general results about linear maps of simplicial fans.
Two-sided intermediaries charge buyers and pay sellers while trying to match the two groups. A larger arrival stream on one side changes both the number of possible matches and the prices that clear the market. Chen and Hu study this in a model of buyers and sellers who arrive over time and may wait before requesting a match. Their market-size theorem concerns the deterministic fluid benchmark used to choose fixed prices for the dynamic system. This mission formalizes that theorem from the submitted manuscript, main text §6, rather than the performance of the waiting-adjusted policy itself.
The fluid benchmark matters because it supplies an interpretable price and quantity for each pair of arrival rates. When buyers become more numerous, the model predicts that both the buyer price and the seller payment rise. When sellers become more numerous, both prices fall. In either direction, more arrivals raise the maximum matching quantity and the fluid profit. These claims concern the same valuation and cost distributions as the rates vary, so they isolate the effect of market size.
Buyer valuations lie in , with density and distribution function . Seller costs lie in , with density and distribution function . Write . Buyer and seller arrival rates are and , and the horizon has length . A buyer accepts a fixed ask price when the valuation is at least ; a seller accepts a fixed bid price when the cost is at most . Thus and are the corresponding acceptance rates.
The buyer virtual value is , and the seller virtual cost is . Assumptions 1 and 2 of the manuscript say these functions are weakly increasing on their respective supports. The supports overlap in the sense . The density assumptions ensure that the survival and cost distribution functions have inverse quantiles on . For a candidate volume , the virtual surplus is
The optimal fluid matching quantity is the largest in for which . The corresponding fixed prices are and .
The fluid program (D) permits any measurable nonnegative ask and bid price path on that clears the market at every time: . Its value is the supremum of buyer revenue minus seller payments, integrated over the horizon. Proposition 1 states that the constant path attains this value and that .
The goal is Theorem 3, the eight weak comparisons of prices, volume, and fluid profit. For with fixed, it asserts
For with fixed, the two price inequalities reverse while the volume and profit inequalities retain their directions. The goal leaves the rates and the two distributions as variables, so it states the market-size result across all systems meeting the paper's assumptions.
The milestones follow the source's dependency structure: Proposition 1 identifies the fluid optimizer; the proof of Lemma S.5 notes that decreases in ; Lemma S.5 establishes the volume and profit comparisons; and the two parts of the proof of Theorem 3 compare the fractions and served on the growing side. The paper's proofs are in the Supplemental Note, with related proofs in the Online Appendix.
The theorem gives directional predictions without differentiating optimal prices with respect to arrival rates. A platform comparing two otherwise identical markets can infer which way its fluid ask and bid prices move, whether it matches more units, and whether the benchmark profit increases. Proposition 1 also connects the optimization over time-varying paths to a fixed price pair, so the static claims apply to the entire feasible fluid program.
The result is proved in the manuscript; this mission asks for a machine-checked proof of the same statement. The formal development would make the inverse-quantile construction, attainment of the optimal volume, and the nonempty bounded fluid optimization problem explicit. Those objects can be reused in other two-sided pricing or matching models. This mission does not claim that the corresponding stochastic system has identical comparative statics; the manuscript itself focuses on the fluid regime in §6.
Increasing one arrival rate expands the feasible number of matches, but the two optimal prices do not follow from that fact alone. The buyer price depends on the fraction of buyers served, and the seller price depends on the fraction of sellers served. A growing side can have a larger matched volume yet a smaller matched fraction. The proof must control both quantities under the appropriate inverse distribution function. Profit also needs a comparison of two separate fluid optimization problems, rather than only a comparison of their candidate fixed-price formulas.
The Lean model reuses the published bilateral-trade environment for the two positive densities, interval supports, cumulative distributions, and virtual values. The new definitions clamp both cumulative distributions to their supports so a price outside the support still has the correct acceptance probability. Inverse quantiles are supported level-set infima, used only at arguments in . All rates and the horizon are positive; both densities are continuous on their supports; the virtual functions satisfy the paper's regularity assumptions; and . Density continuity is a disclosed addition needed for the asserted inverse-quantile and maximum properties.
The claims involving the value of (D) assume a nonnegative seller cost support. This disclosed domain correction puts the fixed seller price in (D), whose price paths take values in ; the imported bilateral-trade environment itself permits negative supports. The virtual-surplus and served-fraction inequalities hold without this condition. Every feasible path is measurable, nonnegative on , clears the market at every point of that interval, and has integrable buyer and seller revenue terms. The fluid value is defined as the supremum over those paths. It is never defined by Proposition 1's fixed-price identity, which would erase the optimization claim. The volume set is restricted to , so its supremum has the source's intended domain. The source uses “increasing” and “decreasing” in the weak sense.
Useful contributions include lemmas showing the clamped distributions are monotone, their supported inverses have the stated identities, the candidate volume set has a greatest member, the fluid feasible set is nonempty and bounded above, and the two fraction comparisons. These are substantive mathematical obligations: no arbitrary inverse, empty feasible set, non-integrable path, or preassigned fluid value should satisfy the goal by a default value.
Many procedures in high-dimensional statistics reduce to computing the probability that a normalized sum of independent random vectors falls into a set: simultaneous confidence intervals for many means, max-type tests, multiple testing with family-wise error control, and inference after model selection. When the dimension is comparable to or much larger than the sample size , these probabilities are approximated by those of a Gaussian vector with the same covariance, the high-dimensional central limit theorem. That Gaussian law is not available in practice, because its covariance matrix is unknown. The Gaussian multiplier bootstrap replaces it by a Gaussian vector built from the data, whose covariance is the sample covariance, and simulates from it.
Chernozhukov, Chetverikov and Kato, Central limit theorems and bootstrap in high dimensions (Ann. Probab. 45 (2017)), prove that this bootstrap is valid uniformly over hyperrectangles and over simple convex sets (sets sandwiched between a polytope with polynomially many facets and its small enlargement), with error depending on only through . This mission formalizes their abstract multiplier bootstrap theorem, Theorem 4.1.
Timeline:
Let and . Let be independent random vectors in with coordinates , centred () with . Let be independent Gaussian vectors with and set
The multiplier bootstrap: let be i.i.d. , independent of the data , let , and
Given the data, is Gaussian with covariance , while has covariance .
A hyperrectangle is a set with . For a finite set of unit vectors and thresholds , the polyhedron has the enlargement . For constants , a Borel set satisfies condition (C) if for some such polyhedron with facets; denotes this polyhedron and its normals. Condition (M.1′) with constant asks for every . Finally,
Let be a class of sets satisfying (C) and (M.1′). There is depending only on such that for every , on the event ,
The theorem is deterministic in the data: it holds at every realization on the event, and turning it into a rate requires only a bound on .
In the order of the proof (App. E.2, p. 2342):
Theorem 4.1 is the abstract step behind the paper's explicit multiplier bootstrap rates: Proposition 4.1 combines it with maximal inequalities that bound with high probability, and obtains, with probability at least , the rate for simple convex sets with sparse facet normals. In applications it justifies bootstrap critical values for max-type statistics and simultaneous confidence regions when . Remark 4.1, the hyperrectangle case, is the version most used in practice.
The results are proved on paper; none is formalized on the platform. A formal development produces machine-checked versions of the smooth-max sandwich, a Gaussian anti-concentration bound (Nazarov's inequality), a quantitative Gaussian comparison inequality and the bootstrap theorem itself. The comparison display and Lemma A.1 are proved in the paper only by citation ([20] and Klivans–O'Donnell–Servedio, Thm. 20), so formal proofs of them are new work rather than transcriptions.
The obvious route compares and through the Kolmogorov distance of their laws or through a total-variation bound between two Gaussians. Both depend polynomially on and fail when . The proof instead compares smooth functionals of the coordinatewise maximum, where the error depends on only through , and then converts back to probabilities of orthants with an anti-concentration inequality whose constant grows like . Both conversions must hold uniformly in the threshold , and the final bound for simple convex sets requires passing to the -dimensional vectors with , which is why appears. The comparison inequality for is the step with the least existing infrastructure: it is a Slepian–Stein interpolation between two Gaussian laws with explicit control of second derivatives of .
EuclideanSpace ℝ (Fin p); is Mathlib's multivariateGaussian 0 Σ. Independence is iIndepFun; 's law is fixed by P.map (Y i) = multivariateGaussian 0 (covMat P (X i)), and square integrability of each makes covMat positive semidefinite, so this is the genuine Gaussian law.mbLaw x is the push-forward of under , and the bound is asserted at every on the event, for the data . Since is independent of the data, this is a version of the conditional law; no conditional expectation appears.Infrastructure needed: multivariate Gaussian laws and their linear images, Gaussian integration by parts or Slepian interpolation, Nazarov's inequality, and properties of log-sum-exp. Lemma A.1, display (21) and the comparison display are reusable beyond this mission, for the high-dimensional CLT of the companion mission and for any max-type Gaussian approximation. Proofs of any milestone are welcome, as are proofs of the conditional Gaussianity identity from Mathlib's Gaussian API.
Many statistical procedures look at a large number of averages at once: simultaneous confidence intervals for means, multiple testing of hypotheses, the maximum of -statistics. Their calibration needs the joint law of a -dimensional normalized sum, and in modern applications is comparable to, or much larger than, the sample size . Classical multivariate central limit theorems with explicit error, such as Bentkus's bound over convex sets (Bentkus 2003), require to grow slowly with (roughly ), which rules out these applications.
Chernozhukov, Chetverikov and Kato showed that when the class of sets is restricted to hyperrectangles, the Gaussian approximation error depends on the dimension only through (Ann. Probab. 45 (2017)).
Timeline. In 2013 the same authors proved a Gaussian approximation for the maximum of a sum (sets of the form ) with rate (Ann. Statist. 41 (2013)). The 2017 paper extends this to all hyperrectangles, improves the rate to , and adds bootstrap results.
Let and . Let be independent random vectors in with coordinates , each centred () with . Let be independent centred Gaussian vectors with , the same covariance as . The normalized sums are
A hyperrectangle is a set with ; is the class of all of them. The quantity to bound is
The error is measured through the third-moment parameter and the truncated maximal moments
the same with , and . Here is the natural logarithm.
If for all , there are constants depending only on such that for every ,
The constants are left existential, as on the page: the goal asserts the shape of the bound, not particular values.
Under the moment conditions (M.1)–(M.2) and either an exponential (E.1) or a polynomial (E.2) moment bound with parameter ,
The result. Under the exponential moment condition (E.1), Proposition 2.1 makes the Gaussian approximation error tend to zero when , allowing much larger than . Under the polynomial moment condition (E.2), its second error term must also tend to zero. Theorem 2.1 is the probabilistic basis of the paper's multiplier and empirical bootstrap results for simultaneous inference (Chernozhukov, Chetverikov and Kato 2017).
Formalizing it. The result is proved on paper; no machine-checked version of this theorem was found in the platform catalog during this mission's prior-art search. A formal proof needs interpolation between and , Gaussian anti-concentration (Nazarov's inequality), and third-order Taylor estimates of smooth approximations of indicator functions. Nazarov's inequality is used in the paper by citation, so its formal proof is a separate milestone.
The obvious route, a Lindeberg replacement of each by after smoothing the indicator of a hyperrectangle coordinate by coordinate, loses a polynomial factor in : the derivatives of a product of smoothed one-dimensional indicators add up over coordinates, so the error grows like a power of rather than of . Any smoothing must also be paid for by the probability that the Gaussian vector falls in a thin neighbourhood of the boundary of a hyperrectangle, and a dimension-free bound on that probability is not available for general hyperrectangles; the anti-concentration bound is the best one can use. Finally, a direct comparison yields an inequality in which the quantity to be bounded appears on both sides, and the rate is obtained only after that inequality is solved; a one-shot estimate gives a worse power of . The truncation in handles coordinates too large for a third-order Taylor expansion, since no moment condition beyond third moments is assumed.
Vectors live in EuclideanSpace ℝ (Fin p) and the coordinate is X i ω j. The Gaussian comparison vectors satisfy P.map (Y i) = multivariateGaussian 0 (covMat P (X i)) with covMat P Z = (E[Z_j Z_k])_{j,k}, which is positive semidefinite, so this is the genuine ; the are independent. Hyperrectangle endpoints are extended reals used only in comparisons. Every theorem carries the standing assumptions , , independence, centring and finite second moments. Items that involve or add ; when a third moment is infinite the paper's bounds are vacuous, so this loses nothing. is defined by its formula for every real , because Theorem 2.1 evaluates it at , which may be below . Lemma 5.1 and Corollary 5.1 assume the 's independent of the 's, as the definition of does; Theorem 2.1 and Proposition 2.1 do not. A bound on a supremum is stated set by set.
Constants that the paper says depend only on (or on and ) are quantified after and before , , the probability space and every random vector; a constant chosen after , or the law would trivialize every statement. Upper bounds on expectations in hypotheses ((M.2), (E.1), (E.2)) and in Lemma C.1's conclusion are lower Lebesgue integrals, so a non-integrable function cannot make a hypothesis hold with a junk value of . Dropping the independence of the or using a wrong covariance would make the goal false.
A complete development needs: a multivariate Stein or Slepian interpolation, third-order Taylor expansion with remainder for functions on , Gaussian integration by parts, and Nazarov's inequality. The anti-concentration and smooth-max lemmas are reusable for any max-type Gaussian approximation, including the bootstrap results of the second mission of this series. Proofs of individual milestones, of Nazarov's inequality in particular, are welcome on their own.
Many constrained optimization problems in operations research have objective and constraint functions that are continuous but not differentiable: maxima of finitely many smooth functions, value functions of inner optimization problems, piecewise-linear costs. For such problems the classical Karush–Kuhn–Tucker theory does not apply directly, and algorithms need a nonsmooth replacement for the condition "the gradient of the Lagrangian vanishes". R. Mifflin's report Semismooth and semiconvex functions in constrained optimization (IIASA RR-76-21, 1976; SIAM J. Control Optim. 15(6), 1977) supplies one. It introduces a point-to-set map built from Clarke's generalized gradients and shows, in §5, that is necessary for optimality of locally Lipschitz problems and, for a class of semiconvex functions, also sufficient as soon as a strictly feasible point exists. The map goes back to Merrill's fixed-point work on differentiable and convex problems; Mifflin's own algorithm for semismooth problems converges to points satisfying , so the sufficiency result says when such points are actual minimizers.
This mission is the third of three on the report. Mission I treats pointwise maxima of compact families of smooth functions, mission II the chain rule for semismooth compositions.
Write for Euclidean space with inner product . For , a point and a direction , the generalized directional derivative is
and the generalized gradient is the set . When exists it is the directional derivative ; is quasidifferentiable at if exists and equals for every .
Let . is semiconvex at with respect to (Definition 2) if (a) is Lipschitz on a ball about , (b) is quasidifferentiable at , and (c) and imply . It is semiconvex on if this holds at every point of . Convex functions and differentiable pseudoconvex functions are semiconvex.
The problem of §5 is to minimize subject to , where . A point is feasible if and strictly feasible if ; is optimal if it is feasible and for every feasible . The map is
and is stationary if and . In Lean these are genGrad, HasDirDeriv, QuasidiffAt, SemiconvexAt/SemiconvexOn, IsFeasible, IsOptimal, Mmap and IsStationary in the namespace MifflinSemismooth.Optimality; is the published ClarkeGradients.Shared.genDirDeriv.
Suppose and are semiconvex on and . Then
The first alternative says the problem is infeasible, the last that it has no strictly feasible point. The theorem carries no constants and holds for any constraint function , not only a finite maximum.
The proof uses, in order: a point with minimizes a semiconvex over (p. 20); on the boundary , the condition yields , , with (p. 20); Proposition 1(b), (p. 3); Theorem 8, for semiconvex on a convex , implies (p. 19); and, if , for every feasible (p. 21).
Theorem 7 (p. 18): for locally Lipschitz , an optimal point is stationary. Theorem 6 (p. 17): for locally Lipschitz , is locally Lipschitz with , where ; semismoothness, semiconvexity and quasidifferentiability on pass from the to , and in the last two cases the inclusion is an equality at points of .
Theorems 7 and 9 together give a nonsmooth Karush–Kuhn–Tucker theory: for semiconvex problem functions with a strictly feasible point, stationarity in the sense of is equivalent to global optimality. For differentiable functions this recovers the sufficiency of the Fritz John conditions for pseudoconvex objectives and constraints (Mangasarian, Nonlinear Programming, Theorem 10.1.1); for convex functions it recovers the saddle-point characterization. Since Mifflin's algorithm produces stationary points, Theorem 9 is the certificate that turns its output into a global minimizer. Theorem 6 lets the constraint stand for a finite system .
The results are proved in the report. None of them, and neither the notion of semiconvexity nor the map , has a machine-checked proof on Prove2Me or in Mathlib as far as the platform search shows; Mathlib has no Clarke generalized gradient. The work is to formalize the known proofs, which also produces reusable facts about (nonemptiness, compactness, the max formula) and about semiconvex functions on convex sets.
The case analysis of Theorem 9 is short; the weight sits in its ingredients. Theorem 8 is the delicate step. Semiconvexity constrains only along directions where , so it says nothing directly about a direction along which does not increase; and a mean value inequality along the segment from to ignores quasidifferentiability and does not determine the sign of . Proposition 1(b) is an attainment statement for a sublinear function whose finiteness rests on the Lipschitz hypothesis, and it fails for the real-valued limsup without that hypothesis. The convex-combination step depends on and being nonempty and convex: the convex hull of a union of two sets need not consist of two-point combinations otherwise. Theorem 7 needs to be closed, which in the boundary case is a statement about the convex hull of two compact sets.
is EuclideanSpace ℝ (Fin n). is a real limsup and equals when the difference quotient is unbounded; every statement therefore has a Lipschitz hypothesis at the points where or is used, and semiconvexity includes "Lipschitz on a ball". is the paper's support-set definition, not the hull of gradient limits. is a relation (HasDirDeriv), never a function with a default value, so Definition 2(c) cannot hold vacuously. "Semiconvex on " means with respect to . "max" is IsGreatest, which asserts attainment. Lipschitz constants are nonnegative reals, which is equivalent to the page's positive constants.
The goal, Theorems 7, 8 and 9 are stated for an arbitrary constraint function ; the paper's is the special case maxConstraint hs with , and Theorem 6 is the bridge. Theorem 9's hypothesis is alone, without feasibility. Theorem 6(c) as printed asserts "for each "; that is false when (, , , ), so it is stated for . A formalization with the hull-of-limits , a junk-valued , a feasibility hypothesis added to Theorem 9, or semiconvexity with respect to a smaller set would prove a different and weaker theorem, and is ruled out.
A complete development needs the basic theory of the generalized gradient (Proposition 1(a), (b)), a Lebourg-type mean value theorem for case analysis along segments, and the finite-max rule. These are reusable beyond this mission, by missions I and II of the series in particular. Proofs of the milestones in any order are welcome, as are proofs of Proposition 1(a) as an auxiliary lemma.
Optimization models often build an objective from several intermediate quantities: constraints, penalties, and transformed measurements are evaluated first, then combined by an outer function. These intermediate and outer functions can be Lipschitz without being differentiable at the point of interest. Ordinary differentiation supplies no chain rule there. The generalized-gradient framework gives a set of possible first-order slopes, while semismoothness provides stronger directional behavior along sequences approaching the point. Mifflin's IIASA report asks whether this behavior survives such compositions and how the generalized gradient of the result relates to those of its ingredients.
The report first establishes basic properties of the generalized gradient in §2, including almost-everywhere differentiability and a nonsmooth mean value theorem. Section 4 then states a chain-rule inclusion as Theorem 4 and the semismooth composition result as Theorem 5. The report is dated December 1976; a journal version appeared in 1977. The mission cites theorem numbers and pages from the report version throughout. No claim about differences between the report and journal texts is needed here.
Work in finite-dimensional Euclidean spaces. Let , for , be component functions, and let be an outer function. Define the component map and the composite by
The functions are locally Lipschitz in the report's precise sense: on each bounded subset of their Euclidean domain they have a finite Lipschitz constant. For a scalar function , a point , and a direction , the generalized directional derivative is the joint upper limit of as and . Its associated generalized gradient is the support set
This is the definition used in Mifflin's report, not an identification assumed in advance with a hull of ordinary gradient limits. Proposition 1(c) supplies that identification under the paper's Lipschitz assumption. The ordinary one-sided directional derivative is the limit of for , when that limit exists.
Mifflin calls semismooth at if it is Lipschitz on a ball about and the scalar sequence has exactly one accumulation point whenever tends to zero, , and . The quantification is over every direction and every such sequence. This pointwise condition is Definition 1 of the report, and its link to one-sided directional derivatives is Lemma 2.
To state the chain rule, form the set
The same is used across all components. The sum is the action of the report's matrix on .
Theorem 4 asserts that is locally Lipschitz and that, at every point,
This is an inclusion, not a general equality. The report gives an example immediately after Theorem 4 in which the inclusion is strict: two identical absolute-value components cancel under an outer difference, while remains larger than .
The goal, Theorem 5, assumes the setting of Theorem 4. If each is semismooth at a selected and is semismooth at , then
The conclusion is pointwise. It does not assert semismoothness throughout from hypotheses at one point. The milestone list contains the chain rule and the source's stated support results: Proposition 2, Lemma 1, Proposition 1(c) and (d), Lemma 2, and the claims (4.2) and (4.11)–(4.12) from the proofs.
Theorem 5 permits composite nonsmooth objectives to be treated within the same semismooth class as their components. Theorem 4 gives a concrete set built from component generalized gradients that contains the composite's generalized gradient. Together, they let later statements about a composite use first-order information from its stated ingredients, subject to the inclusion's possible strictness. These are results proved in Mifflin's report, not open mathematical conjectures.
This mission drafts machine-checkable statements of those known results and their definition layer. The local Lean modules compile with proof placeholders; this staging does not supply machine-checked proofs of the theorems. A complete development would formalize the known arguments or another proof of the same statements. The reusable output would include the support-set generalized gradient, sequence-based semismoothness, the nonsmooth mean value result, and the chain-rule inclusion, all with their source assumptions exposed.
At a point where is differentiable, the component functions need not be differentiable, and the outer function need not be differentiable at . The ordinary smooth chain rule therefore cannot simply multiply ordinary gradients. The candidate is a convex set of combinations of generalized gradients; a single chosen combination does not in general describe all nearby limiting slopes. The report's strict-inclusion example also shows why replacing Theorem 4 by equality would be false. For semismoothness, the condition concerns every admissible sequence of generalized gradients near the point, so checking just one path or one gradient selection does not establish Theorem 5.
The Lean domain is EuclideanSpace ℝ (Fin n) and the outer domain is EuclideanSpace ℝ (Fin m). The report's norm is the Euclidean norm and its pairing is the real inner product. An index of type Fin m represents the components; is admitted, in which case the component space is a point and the composite is constant. A finite sum represents the column-matrix product. The generalized gradient is defined by all directional support inequalities, so Proposition 1(c) remains a theorem rather than becoming true by definition.
The generalized directional derivative is imported from the published definition matching the report's joint limit. Lean's real limsup has a default value for an unbounded quotient; Lipschitz hypotheses are carried wherever that operation is used. “Locally Lipschitz” is imported as Lipschitzness on every bounded subset, and the explicit constants of §2 use nonnegative reals, equivalent to the report's positive constants by enlarging them. The directional derivative is a relation asserting a limit, so no value is assigned when the limit fails. “Exactly one accumulation point” remains an existence-and-uniqueness assertion about cluster points. The report's means positive convergence to zero, as its proof of Lemma 2 says explicitly. These choices exclude a vacuous formulation that only asks about one convenient sequence or gives a default directional value.
The scope includes the two local definition files and the cited theorem statements, including both conclusions of Theorem 4 and Lemma 2. Proof contributions would need finite-dimensional Lipschitz and differentiability infrastructure, limiting-gradient compactness, convex hull and separation facts, and sequence convergence facts. Results about the alternative Qi–Sun vector-valued semismoothness notion are outside this mission's definition layer.
Carbon accounting assigns emissions from a shared supply-chain process to firms that can reduce them. If more than one firm can change the same emissions, charging each firm only a share may leave each with too little incentive to abate. Caro, Corbett, Tan and Zuidwijk study the conflict between avoiding double counting in an emissions ledger and inducing the effort a social planner would choose. Their working paper, published in Manufacturing & Service Operations Management in 2013, states an impossibility result for differentiable, increasing carbon-payment rules. It covers multiple firms, processes, and abatement actions, where a process can be influenced by several firms.
The question matters when a carbon footprint is used as a payment base rather than only as a report. A payment rule changes a firm's private incentive to exert costly effort. The rule may also include transfers between firms, so its incentive effect cannot be judged by looking at a single firm's allocated emissions alone. The paper asks what aggregate marginal payment is necessary if decentralized choices are to reproduce the social first best.
Timeline. Holmström (1982) showed for a team with one joint output and one-dimensional efforts that no budget-balanced sharing rule supports the efficient efforts as a Nash equilibrium (stated in the paper as Proposition 1, p. 11). Charging every team member the full social cost ("charging everything to everyone") is known to restore efficiency, as the paper recalls on p. 12. Caro, Corbett, Tan and Zuidwijk (2012 working paper, 2013 journal version) extend the impossibility to many processes, many abatement actions per firm and an explicit influence structure between firms and processes. They also characterize the linear rules that achieve the first best.
Let be a finite set of firms and a finite set of emission-producing processes. Firm chooses a vector of abatement efforts in , with . The full profile is . Firm 's profit before carbon payments is , concave and componentwise decreasing in its effort. Process 's footprint is , convex and componentwise decreasing in the collective effort, and nonnegative on the feasible box. The functions are differentiable, as assumed in the paper's model.
The influence matrix has entries in . An entry is one when the sum of the partial derivatives of with respect to firm 's actions is negative. The paper treats this matrix as independent of the effort profile. Joint carbon production means that a process has at least two influencing firms: for some , .
The societal cost per unit of footprint is . The social first best maximizes
over the effort box. The paper assumes that this solution is unique and that the effort bound is large enough for the relevant optimum to be interior. The first-best footprint is .
A carbon-based payment rule charges firm as a function of the observed footprint vector , rather than the unobserved effort profile. In the social-planner setting of equation (5), , where is its footprint allocation and the transfers balance: for . A Nash equilibrium is a feasible effort profile where no firm improves by changing its own entire effort vector while the other firms hold theirs fixed. At a footprint vector , the rule double-counts process when .
The goal is Proposition 2, evaluated at the first-best footprint:
The paper defines double counting existentially over footprint levels. Its Appendix A.1 proves the stronger assertion at , which is the target here. The rule remains of the form (5), with balanced internal transfers on the nonnegative footprint domain.
Two source statements form the milestone list. The necessary part of Lemma 7 gives equation (14): at an interior first best that is also a Nash equilibrium, the sum over processes of each footprint derivative times the gap between the firm's marginal payment and is zero, both with and without the influence indicator . Equation (18) says that if aggregate marginal payments do not exceed at , every individual process contribution to that sum is zero. The mission also drafts the sufficient part of Lemma 7 and Proposition 3, which characterizes the linear rules with : they implement precisely when .
Proposition 2 identifies a limit on footprint-based incentives under joint production. With more than one firm able to lower a process's emissions, a differentiable increasing rule that implements the first best cannot keep every aggregate marginal charge at or below the social carbon price. Balanced transfers among firms do not remove that requirement. Proposition 3 supplies a complementary characterization for linear payments, identifying which firms must bear the full marginal charge for the processes they influence. These are results proved in the paper, not open conjectures.
The formalization contributes a precise, reusable model of finite effort profiles, process footprints, unilateral deviations, and coordinate marginal payments. It also separates a global Nash best-response condition from first-order identities, so the necessary condition in Lemma 7 has mathematical content. The listed Lean theorems are draft statements with proof holes; they do not yet have machine-checked proofs. Completing them would formally verify the paper's stated claims under the declared model conventions.
The obstacle is the interaction between a shared footprint and unilateral decisions. A firm's payment derivative with respect to a process footprint is multiplied by that firm's own effect on the process, while the social objective prices the total footprint at . A condition on the sum of marginal payments alone does not specify the charge faced by each influential firm. With several actions and processes, the necessary condition is a sum over process contributions, so it cannot simply be read as a coordinatewise equality without further assumptions. These issues occur even though all effort and process index sets are finite.
Lean represents firms, each firm's action indices, and processes by finite types. Efforts and footprints are real-valued functions. The firm and collective effort boxes are closed coordinatewise intervals, with ; optimality and Nash equilibrium quantify over all feasible profiles or unilateral deviations. Coordinate partial derivatives use one-variable derivatives after replacing the corresponding coordinate. Payment rules are functions on real footprint vectors and “increasing” means componentwise nondecreasing.
The source's sign test for does not name an effort profile. The formalization pins it to every profile in the effort box, matching the paper's use of a fixed influence matrix. Interiority is required only of the named first best. The paper's “without loss of generality” nonempty row and column sums for are omitted because the results do not use them; the strict part of its cost monotonicity is likewise unused. Its participation condition (3) is outside the decentralized game (4) and is not added to Nash equilibrium. Equation (5) and transfer balance are imposed only for nonnegative footprint vectors, as printed. The effort bound and Proposition 3's matrix have distinct names.
The first best is a feasible global maximum, not a default-valued real supremum; Nash equilibrium tests full unilateral deviations, not stationarity. These choices rule out a vacuous first-best target and a first-order surrogate for the game. The supporting definitions of finite effort boxes, coordinate derivatives, social value, and Nash best response are useful beyond the final impossibility statement. Contributions that prove the source's necessary and sufficient conditions, the linear characterization, or the goal against these definitions are within scope.