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?
Large data sets make clustering and subspace fitting expensive because a candidate solution must be evaluated against every input point. A dimensionality reduction replaces the data by a lower-rank matrix whose costs approximate those of the original input for an entire class of candidate solutions. Feldman, Schmidt, and Sohler study reductions that retain enough information for -means, principal component analysis, and projective clustering. Their journal paper identifies a rank truncation and one residual scalar that preserve the fitting cost of every shape lying in a low-dimensional linear subspace Feldman, Schmidt, and Sohler (2020), Theorem 22.
The published article also records that some coreset sizes in its 2013 conference version were incorrect. This mission uses the 2020 journal statement and its page numbering throughout. The authors cite earlier SVD-based approximations to -means on p. 613, while their Theorem 22 gives a uniform cost guarantee for arbitrary nonempty shapes contained in a -dimensional subspace Feldman, Schmidt, and Sohler (2020), pp. 603, 613, 620.
The input is a real matrix . Its rows are points in . For a nonempty set of candidate locations or shapes , let be the infimum of Euclidean distances from row to points of . The shape cost is
The set need not be closed and need not be a subspace. For example, it can be a finite set of cluster centers. The restriction is that all of its points lie in some linear subspace of dimension . This matches the paper's shape class in §5; the affine case is treated separately Feldman, Schmidt, and Sohler (2020), pp. 619–620.
Fix a singular value decomposition , where and are orthogonal and the diagonal entries of the rectangular matrix are nonnegative and nonincreasing. The entry is indexed from one. The rank- truncation keeps the first diagonal entries and sets the rest to zero. Its squared Frobenius residual is . The corrected cost of is Feldman, Schmidt, and Sohler (2020), Definition 1 and §2.
The milestones first record the matrix Pythagorean identity, the projection and residual bounds, and the lower bound on the cost of a linear -subspace. They then state the residual-corrected approximation in Corollary 16:
Here has orthonormal columns spanning the complement of the candidate subspace. Corollary 20, Corollary 21, and display (9) connect these linear estimates to costs of general sets Feldman, Schmidt, and Sohler (2020), pp. 604, 613–615, 619–620.
The goal is Theorem 22. For , , and , every nonempty contained in a linear -dimensional subspace satisfies
The quantifier over makes this a guarantee for every admissible candidate on the same reduced data, rather than a statement about one selected optimum Feldman, Schmidt, and Sohler (2020), Theorem 22, p. 620.
The theorem preserves objective values after replacing by a rank- matrix and one number. For a fixed and accuracy parameter, the rank threshold depends on and , with no direct dependence on the number of points or ambient dimension except the upper bound on feasible . In the paper, the result leads to a guarantee for -means candidates, since centers span a linear subspace of dimension at most Feldman, Schmidt, and Sohler (2020), Corollary 23, p. 621.
The result is proved in the paper, but this mission's Lean theorems are posed with sorry; they do not yet have machine-checked proofs. A completed development would connect a reusable rectangular SVD model, matrix projection identities, infimum distances to arbitrary nonempty sets, and a uniform cost inequality. The SVD definition is already published in the platform library; the row-cost and singular-value conventions here supply the interface needed for this paper Feldman, Schmidt, and Sohler (2020), §§2, 3, 5.
The linear subspace bound compares a projection cost with a tail sum of squared singular values. The paper recalls that fact in §3 without proving it, so the formal development needs a suitable singular-value inequality or a derivation from existing matrix approximation results. For general shapes , a bound on the cost of one linear subspace does not by itself control the distance from each projected point to every point of . The remaining milestones state the projection error, the squared-distance perturbation bound, and the Pythagorean cost split that address that gap Feldman, Schmidt, and Sohler (2020), pp. 613, 619–621.
The proof printed after Theorem 22 invokes earlier corollaries under a stronger rank threshold than the theorem states. The mission keeps the printed theorem threshold, whose claim remains valid; a formal proof must bridge that discrepancy Feldman, Schmidt, and Sohler (2020), pp. 620–621.
Matrices are Matrix (Fin n) (Fin d) ℝ, and rows are points of EuclideanSpace ℝ (Fin d). Squared Frobenius norm is an explicit finite sum of squared entries. Shape cost sums squared Metric.infDist values over rows. Since Mathlib assigns a real default value to distance from the empty set while the paper assigns infinity, every theorem about a general shape requires C.Nonempty. This is the page's own requirement for Theorem 22 and Corollary 21, and is also needed for display (9).
The SVD and its truncation use the published ProjLikeRetr.FixedRank.IsSVD and truncSVD. Every SVD statement quantifies over an arbitrary valid triple ; tied singular values do not fix a unique truncation. The local is one-based, while truncSVD m keeps zero-based diagonal positions below . Orthonormal columns of satisfy , their orthogonal complement has columns, and projection in ambient coordinates is . Theorem 22 quantifies over arbitrary nonempty contained in a linear -subspace; it does not restrict to subspaces or replace linear containment by affine containment.
The integer inequalities in Lean use additive forms such as to avoid truncated natural-number subtraction. The theorem retains the printed threshold, including the proof gap described above. Running-time clauses are outside the mission's mathematical statements. Contributions are welcome toward the singular-value lower bound, the projection and infimum-distance identities, and the final uniform inequality; the matrix and distance definitions are reusable in the companion affine-subspace mission.
Many problems in quantum information theory ask for the maximum of a linear functional over pairs of quantum states, one on each of two systems, subject to linear constraints on each state. The best success probability of an approximate quantum error-correcting code of given size is of this form: the encoder and the decoder are quantum channels, their Choi matrices are states with fixed marginals, and the objective is bilinear in the two (Berta, Borderi, Fawzi & Scholz, arXiv:1810.12197, §4). Such constrained bilinear programs are nonconvex. Seesaw methods give lower bounds that often converge in practice, but they offer no guarantee of global optimality. What is needed is a hierarchy of efficiently computable outer bounds that converges to the optimum, with an explicit rate.
For the unconstrained problem, the optimisation over separable states, such a hierarchy is classical: the Doherty–Parrilo–Spedalieri hierarchy of -extendible states, whose convergence follows from finite quantum de Finetti theorems (Christandl, König, Mitchison & Renner 2007; Brandão & Harrow 2013). The standard de Finetti approximant is, however, a mixture of product states that need not satisfy the linear constraints, so it says nothing about the constrained problem. The paper proves a de Finetti theorem with linear constraints (Theorem 2.3) and derives from it a semidefinite hierarchy for constrained bilinear programs with a convergence guarantee (Theorem 3.1).
A -dimensional quantum system has operator space ; a state is a positive semidefinite with . Let and be systems of dimensions and . The data are an objective , arbitrary linear maps and , and matrices , . The constrained bilinear program is
For let be copies of . A state on is symmetric with respect to if it is invariant under every permutation of the copies , . Write , and . The level- program is
It is a semidefinite program of size polynomial in and .
The rate involves the trace norm , the Schatten -norm (largest singular value), and the minimal distortion with side information of ,
the infimum over measurements on and the supremum over all finite-dimensional ; is the analogue with product measurements . Throughout, is base 2.
The page states with . The goal makes explicit the rate the proof gives.
Theorem 3.1 turns a nonconvex problem into a sequence of semidefinite programs whose values decrease to the optimum at rate , with a constant that depends polynomially on and logarithmically on . Every level is a certified upper bound; together with any feasible point it brackets . The same argument applied to channel fidelities gives converging outer bounds on the success probability of approximate quantum error correction (§4 of the paper), and the constrained de Finetti theorem is the key step there as well. Theorem 2.3 is of independent interest: it is the first finite de Finetti theorem in which the approximating separable state inherits linear constraints of the extension.
The results are proved in the paper; none of them has been machine-checked. A complete formalization requires the quantum relative entropy and mutual information with their chain rule, the quantum Pinsker inequality, state two-designs and their existence, and a weighted Hölder inequality for Schatten norms; most of this is absent from Mathlib, and each piece is reusable beyond this mission.
The obvious route measures every copy with a fixed informationally complete measurement and uses the resulting classical de Finetti statement. This approximates by a mixture of product states, but the states in the mixture need not satisfy , and projecting them onto the constraint set destroys the error bound. The paper instead conditions on the outcomes of only copies and keeps quantum; the constraint on then transfers to the conditional state of by symmetry. Making this rigorous needs the chain rule of conditional mutual information with classical conditioning, and the distortion of the measurement must be bounded independently of the side system , which is what Lemma D.1 provides. The Schatten-norm estimate there is elementary but requires a weighted Hölder inequality and a careful choice of weight.
Systems are finite index types: is indexed by Fin dA × (Fin N → Fin dB), is Mathlib's Kronecker product, and the permutation action permutes the word in Fin N → Fin dB. States, trace norm and partial traces are the published definitions WildeQIT_IsDensityOperator, WildeQIT_traceNorm and WildeQIT_partialTrace. The linear maps , are arbitrary -linear maps (not assumed positive or trace preserving), applied blockwise to one tensor factor. The objective is the real part of , equal to for Hermitian . Each "max" is the supremum of the set of objective values over the feasible set, never over all matrices. Wherever the page has copies of , the Lean has n + 1: SDPval … n is the page's , and the bounds have denominator . The distortions and take values in ; the standalone bound on assumes .
No feasibility hypothesis is added to the goal. The feasible sets of and of every level are empty or nonempty together, and the empty case reads . The goal mentions only , , , , and ; a formalization in which or were free real numbers, or in which the de Finetti mixture was not required to satisfy the constraints, would be a different and much weaker statement.
Contributions are welcome at every milestone, and especially in the reusable infrastructure: quantum relative entropy and mutual information on matrices, the quantum Pinsker inequality, unitary and state designs, and Hölder inequalities for Schatten norms.
Online sellers of loans, insurance, travel and retail goods observe data about each arriving customer before quoting a price. Using that data to price individually is attractive only if the seller can learn, from its own sales, how demand responds to price for customers with given characteristics. Two features make this hard in practice. The number of recorded characteristics is often large, possibly larger than the selling horizon , while only a few of them matter. And price sensitivity is itself heterogeneous: different customers respond to the same price change differently.
Ban and Keskin (Management Science 67(9), 2021) model both features and ask how fast the revenue lost to learning can grow. Their answer is that a seller who learns with lasso-regularized quasi-likelihood estimation and occasional price experiments loses revenue of order up to logarithmic factors, where is the number of relevant characteristics, and that no policy can do better than order . This mission formalizes the upper bound for the general (nonlinear-link) model with unknown sparsity, Theorem 3 of the paper.
In each period a customer arrives with a raw feature vector . The are i.i.d., take values in a compact set inside a ball of radius , have mean zero and positive definite covariance . The seller sees the augmented vector , charges a price with , and observes the demand
Here is an unknown parameter in a compact rectangle , the link is known, differentiable and increasing with on the relevant domain, and the demand shocks form a sub-Gaussian martingale difference sequence. The term is the customer's own price sensitivity. With the argument of is .
The sparsity of is , . The seller does not know .
The expected revenue of price is , and the clairvoyant price maximizes it; it is assumed to lie in the interior of for , . The regret of a policy over periods is
The policy ILQX charges the experimental price in periods and in periods , and otherwise charges , where maximizes the lasso-penalized quasi-likelihood
over the experimental periods (), and is the projection onto . The regularization level is for a constant .
There is a finite constant such that
is fixed with the model and is uniform over ; since varies over , the factor carries content.
Theorem 3 says that a seller facing many potentially relevant customer characteristics, without knowing which matter and under a nonlinear demand link such as logit, loses revenue at a rate governed by the number of relevant characteristics and only logarithmically by the total number . Combined with the paper's lower bound (Theorem 1, for the linear model), it makes ILQX first-order optimal up to logarithmic factors. An unregularized policy would pay order , which is linear in when exceeds .
The paper's proofs are in its electronic companion, which this mission does not reproduce; no machine-checked version of the result exists. A complete formalization would also produce a reusable high-probability error bound for lasso-regularized quasi-likelihood estimation under adaptively collected data (Lemma 3), and a machine-checked model of feature-based dynamic pricing on which related policies can be stated.
The estimation error must be controlled on data collected by the policy itself. The design vectors use only two prices, so the information about the price sensitivity accrues only from the experimental periods. Standard lasso error bounds assume a fixed or i.i.d. design and a restricted-eigenvalue condition on it; here a restricted-eigenvalue-type property of the random Kronecker design must be derived from and , and the noise enters through a martingale whose conditional law may depend on past prices. The quasi-likelihood is not a least-squares objective, so the curvature comes from the bounds , which hold only on the bounded domain and not at an unconstrained estimate. Finally, the regret bound has to turn a squared-error bound holding with probability into an expected revenue loss, which requires the revenue loss to be second order in the parameter error at an interior optimum.
Fin (d+1) → ℝ with the intercept at index 0; is Fin 2 × Fin (d+1) → ℝ with , . Periods are 1-based. .Contributions welcome: existence of a measurable maximizer of the objective, the counting lemma, and supporting lemmas for Lemma 3 and the regret bound.
An online player repeatedly chooses a subset of coordinates and pays the sum of their losses. In many applications the player sees only that sum, not the losses of the selected coordinates. This bandit feedback makes it harder to identify which coordinate within each chosen subset is responsible for a favorable or unfavorable outcome. Audibert, Bubeck and Lugosi studied how this information limit changes regret in online combinatorial optimization. Their Theorem 5 establishes a lower bound that scales linearly with the number of selected coordinates and with the square root of the ambient dimension and horizon. Audibert, Bubeck and Lugosi, 2013, pp. 13–14
The result is part of a comparison among full-information, semi-bandit and bandit feedback in the same action model. Under full information the player sees the complete loss vector after each round; under semi-bandit feedback the player sees losses at selected coordinates; under bandit feedback the player sees only one scalar. The paper proves upper bounds for semi-bandit play and a bandit lower bound. The latter is the target of this mission. Audibert, Bubeck and Lugosi, 2013, pp. 2–3, 14
Fix a dimension , a horizon , and a finite nonempty set . Each action has exactly entries equal to one. At round , the player selects a probability distribution on , draws an action , and simultaneously an adversary selects a loss vector . The player pays the scalar . In the bandit protocol, that scalar is the only new information made available for the next round. A player strategy can use every previous action and observed scalar loss, and can randomize at every round. Audibert, Bubeck and Lugosi, 2013, pp. 2–3
The paper measures performance by pseudo-regret against the best fixed action in expectation:
The expectation covers the player's randomization and, when present, the adversary's randomization. This benchmark chooses one action for the whole horizon after comparing expected cumulative losses. It is the sole notion of regret used in the paper. Audibert, Bubeck and Lugosi, 2013, p. 2 and footnote 1
For the lower bound, the appendix arranges the coordinates as parallel games with choices per game. An action selects one coordinate from each game. The adversary can associate a favoured choice with each game and assign independent Bernoulli losses whose means are at the favoured coordinates and elsewhere. The player still sees only the sum of the selected losses. These are the -adversaries that underlie the milestone statements. Audibert, Bubeck and Lugosi, 2013, pp. 16–17
The goal is Theorem 5 with the divisibility condition used by its appendix construction. For and , there is an action set such that every bandit strategy faces some bounded loss law with
The order of the choices is part of the claim: the action set is fixed first; then each player strategy may face its own adversary. The lower bound retains the paper's explicit constant . Audibert, Bubeck and Lugosi, 2013, p. 14, Theorem 5; p. 16
The milestones follow the appendix's stated results: Lemma 5 bounds a logarithm; Lemma 4 and its corrected second case bound the divergence between sums of independent Bernoulli variables; the one-round observation bound and the horizon bound control information revealed by bandit feedback. Equations (9), (10), and (11) connect that information to expected regret and symmetry. The final averaged bound on the chance of selecting a favoured choice closes the path to the goal. The milestones are stated for deterministic players, as in the first three steps of the appendix; the passage to randomized players (the appendix's fourth step) is part of the goal's proof and is not a separate milestone. Audibert, Bubeck and Lugosi, 2013, pp. 17–18, 20–21
The theorem prevents a uniform regret guarantee of smaller order than for this bandit action model. It shows that aggregating selected losses into a single observation imposes a cost beyond what a player can avoid by choosing a different randomized strategy. In particular, the quantifier over every strategy makes the claim about the feedback model, rather than about one named algorithm. The paper proves the result in Appendix B, with the Bernoulli-sum estimate in Appendix C. Audibert, Bubeck and Lugosi, 2013, pp. 14, 16–18, 20–21
The formalization work is to prove the existing paper result in Lean from a finite protocol that represents all behavioural player strategies, together with the finite laws of the appendix's adversaries. The resulting definitions of action paths, scalar observations, finite probability laws, and divergence estimates can support other finite-horizon bandit lower bounds. These statements are drafted as open Lean theorems; compilation checks their types, while proofs remain for solvers. The paper's mathematical proof does not itself constitute a machine-checked proof.
A scalar bandit observation sums losses from several games. The player cannot separate the contribution of the favoured coordinate in one game from the other selected losses by inspecting that observation. A bound for the divergence of a single Bernoulli variable therefore does not directly bound the information available to the player. The appendix's central estimate concerns sums of independent Bernoulli variables, followed by the law of the whole sequence of scalar observations. Audibert, Bubeck and Lugosi, 2013, pp. 16, 18, 20
There is also a correction to make explicit. Lemma 4 is false for some parameters allowed by its printed statement: taking , , and violates the displayed bound. The error is in the second case of its proof, which applies Lemma 5 outside its range when . The mission states Lemma 4 with the additional condition , which holds whenever , and states the corrected second case separately: for , . Through the corrected case, the one-round bound used by the goal holds for the full range , so Theorem 5 and its constant are unaffected. Audibert, Bubeck and Lugosi, 2013, pp. 20–21, Lemmas 4–5
Actions are functions constrained to zero or one, with coordinate sum . Coordinates and rounds are indexed from zero. A behavioural strategy maps every history of chosen actions and real-valued observed losses to a probability distribution on the finite action set. Its domain includes every real history, even though the appendix's particular Bernoulli adversaries generate integer observations. The strategy may randomize; restricting the goal to deterministic players or allowing it to inspect an unobserved loss vector would change the game.
The goal's exhibited adversary is an oblivious, finitely supported probability law on loss sequences in . It belongs to the broader adversary class of the paper, so this existential formulation is stronger. All expectations are finite sums. The regret comparator is a minimum over the nonempty action set, not a default value assigned to an empty set. The action set has binary entries and equal coordinate sums, and every loss lies in the unit interval; these clauses rule out trivial lower bounds from malformed actions or unbounded losses.
The hypothesis is added to the printed theorem because Appendix B assumes it to partition coordinates into equally sized games. When , it forces and the claimed lower bound is zero. The milestone model uses functions with , deterministic players, finite Bernoulli product laws, and a finite real KL sum. Its log ratios are meaningful on the common support ensured by the stated parameter bounds. Reusable contributions include the finite bandit protocol and observation laws, as well as proofs of the KL and averaging milestones.
A partially observable Markov decision process (POMDP) models a controller that cannot see the state of the system it steers, only noisy observations of it. Inventory control with unrecorded demand, machine maintenance with imperfect inspection, and target tracking from sensor readings all have this form. The standard way to solve a POMDP is to replace it by its belief MDP, also called the completely observable MDP (COMDP): the state becomes the posterior distribution of the hidden state given everything observed so far. The belief MDP is fully observed, so the theory of Markov decision processes applies to it, but only if the belief MDP satisfies that theory's hypotheses. For MDPs with Borel state and action spaces, unbounded costs and possibly noncompact action sets, the hypothesis that yields optimality equations, convergence of value iterations and stationary optimal policies is Assumption (W*) of Feinberg, Kasyanov and Zadoianchuk (Math. Oper. Res. 2012): the cost is -inf-compact and the transition probability is weakly continuous.
Before Feinberg, Kasyanov and Zgurovsky (arXiv:1401.2168v2, published in Math. Oper. Res. 41(2), 2016), sufficient conditions for the belief MDP to be weakly continuous required a weakly continuous filter (Hernández-Lerma, 1989, as recalled on p. 11 of arXiv:1401.2168v2), a condition that fails in many natural models. The paper replaces it by a condition on the primitive data of the POMDP.
Let (states), (observations) and (actions) be Borel subsets of Polish spaces. Let be the transition kernel on given , the observation kernel on given , and a Borel one-step cost bounded below. is the set of probability measures on with the topology of weak convergence ( for bounded continuous ). A sequence converges setwise if for every Borel , and in the total variation if over Borel with values in . A kernel is weakly (setwise, total-variation) continuous if implies the corresponding convergence of the measures.
For a belief and an action , let be the joint law of the next state and observation (3.1), and its observation marginal (3.2). A filter is a kernel with (3.3): is the posterior after observing . The belief MDP has state space , action set , cost (3.8), and transition , the law of when (3.5). A cost is -inf-compact on if its restriction to has compact level sets for every compact .
If either Assumption (D) () or Assumption (P) ( and ) holds, is bounded below and -inf-compact on , is weakly continuous and is continuous in the total variation, then the belief MDP satisfies Assumption (W*):
Theorem 3.6 supplies the hypothesis under which the cited general MDP theory gives stationary optimal policies, optimality equations and convergence of value iterations for total-cost POMDPs in terms of , and alone, without compactness of the action set, boundedness of the cost or continuity of the filter. It covers, for example, observation kernels with densities continuous in , and the paper applies it to inventory control with incomplete records and to the Kalman filter. Example 4.1 of the same paper shows that total-variation continuity of cannot be weakened to setwise continuity.
The result is proved in the paper; this proposal poses its formal statement and the supporting results as proof targets. Completing them would provide a checked bridge from POMDPs to the general MDP theory under weak continuity, together with reusable facts about weak, setwise and total-variation convergence: equicontinuity of integrals against weakly continuous kernels (Theorem 5.2), the convergence-in-probability criterion (Theorem 5.5), and the generalized Fatou lemmas.
The posterior is defined only for -almost every and has no continuous version in general, so weak continuity of cannot be read off from continuity of . The tempting argument, that continuous and make the Bayes posterior move continuously, fails: need not be countable and need not have densities. What has to be controlled is the joint law on sets uniformly in the observation set ; convergence for each fixed is not enough. Turning this uniform control into almost-sure convergence of posteriors along a subsequence requires a diagonal argument over a countable base of . On the cost side, the difficulty is that may take the value and is not continuous; -inf-compactness has to be transported through integration against a weakly converging sequence of measures.
All definitions live in FeinbergPOMDP.WStar.Model. are separable metrizable spaces with their Borel σ-algebras (PolishSpace is not assumed, since Borel subsets of Polish spaces need not be Polish); is additionally nonempty and standard Borel in Theorems 3.6 and 3.7, where a filter must exist. is Mathlib's ProbabilityMeasure with the weak topology. All continuity notions are the paper's sequential ones; total variation is the supremum over Borel functions with values in , written in – form, while the set-indexed suprema of (5.15) and (5.17) keep their set form. The cost is written with and taking values in , so , exact even when on a set of positive measure. -inf-compactness is the published FeinbergLiang.ACOE.KInfCompact. A filter is a map that satisfies (3.3) and is jointly Borel measurable in , as the paper's stochastic kernel is; is the image of under for the Borel σ-algebra of the weak topology on .
Since does not depend on the choice of filter, every statement about is made for every filter satisfying (3.3). A fixed filter that ignores the observation, such as , would make a point mass and the weak continuity trivial; it satisfies (3.3) only when observations carry no information, and is excluded by quantifying over all filters.
The goal states the Assumption (W*) conclusion of Theorem 3.6. Its tail, "statements (i)–(vi) of Theorem 3.1 hold", invokes Theorem 2.1 of Feinberg et al. (2012) applied to the belief MDP; it is cited rather than proved in this paper. Generalized Fatou's lemmas 5.1(i) and 5.1(ii) are referenced from the published Schäl (1993) items. A complete development needs weak and setwise convergence on ProbabilityMeasure, portmanteau-type arguments, disintegration (Measure.condKernel) and the identification of the Borel and Giry σ-algebras on ; the last is missing from Mathlib and is a welcome contribution in its own right. Proofs of any milestone, and alternative arguments for Theorem 3.7, are welcome.
Wasserstein distributionally robust optimization (DRO) replaces the empirical risk of a loss by its worst case over all distributions within Wasserstein distance of the empirical law . Gao, Chen and Kleywegt (arXiv:1712.06050; Operations Research, 2024, doi:10.1287/opre.2022.2383) show that, for small radii, this worst-case risk is the empirical risk plus times a variation of the loss (a norm of its gradient or local slope), up to a remainder. This links DRO to gradient-norm regularization, as used in adversarial training and in data-driven newsvendor and pricing models.
For smooth losses the remainder is of order . Many losses used in practice are only piecewise smooth: hinge, ReLU networks, newsvendor costs, . Near the set where the pieces meet, the first-order expansion fails, and the paper's Theorem 1(I)–(II) carries an extra boundary term . Theorem 1(III) shows that this term is small with high probability, uniformly over the loss class, provided the data distribution does not concentrate near the non-smooth points. This mission formalizes that probabilistic bound.
Let be a metric space with its Borel -algebra, a probability measure on , and an i.i.d. sample from , with empirical law . The sampling law is the product on , and is its expectation. The formal statements also assume the metric space is second countable.
Let be a set of losses , and for each let be its non-smooth set: for a piecewise smooth with pieces , the union of the pairwise intersections of their closures (Assumption 1). The paper assumes is -null. The distance to a set is , with .
The objects of the mission are:
In Lean the boundary gap is the shared WassVarReg.PInf.boundaryGap; nearIndicator, indicatorClass, empRademacher, rademacher and Assumption3 are in WassVarReg.Boundary. The sample law is the published MinimaxWass.DataDep.sampleLaw.
Under Assumption 3 there exist such that for all , and , with probability at least , for every ,
The constants and are left unspecified; they depend only on Assumption 3.
The result. With and a class of bounded complexity, the right side of the goal is . Combined with Theorem 1(I)–(II), it gives the paper's conclusion that -Wasserstein DRO with is asymptotically equivalent to empirical variation regularization, , for non-smooth losses, uniformly over the class. Without it, the boundary term is only bounded by , and the expansion has no better accuracy than first order. Assumption 3 is the condition under which the non-smooth set does not matter statistically.
Formalizing it. The result is proved in the paper; it has no machine-checked proof. Its proof composes a uniform deviation bound (McDiarmid's inequality plus symmetrization) with a bounded-density estimate. The mission produces a general Rademacher deviation bound for bounded classes on an arbitrary metric space with a measurability guard, reusable by any statistical-learning mission, and fixes the printed constant of Lemma EC.5 ( on the page, from its proof).
The deterministic parts are short. The difficulty is in Lemma EC.5. McDiarmid's inequality must be applied to the uniform deviation over an arbitrary, possibly uncountable, class. Symmetrization must then be carried out with Bochner integrals over and a finite sign space. Neither tool is in Mathlib in this form. A tempting shortcut, bounding each fixed by Hoeffding's inequality and taking a union bound, fails: the class is infinite, and the bound must hold simultaneously for all inside a single event. A second point is Assumption 3: it controls only the shell , so the mass of has to come from the null closure of .
[MeasurableSpace Z] [BorelSpace Z] [SecondCountableTopology Z] in the goal-level statements. Second countability is an added technical hypothesis used throughout this paper's mission series. A sample is ω : Fin n → Z with , and its law is Measure.pi. Empirical means are .Metric.infEDist, which is on . A loss with thus has boundary gap and is excluded from , as on the page. The real-valued Metric.infDist (which is on ) would give such a loss gap and is not used.D : (Z → ℝ) → Set Z. The goal-level statements assume each is closed and -null, the standing consequence of its construction in Assumption 1. The details of the piecewise smooth loss model are not needed for this probability estimate.Contributions welcome: a general McDiarmid inequality for product measures, a symmetrization lemma for measurable classes, and proofs of the milestones in any order.
A seller learning a demand curve normally adjusts prices as new observations arrive. A price-change limit prevents that continual adjustment: a price may have to be chosen before the seller knows which demand curve it faces, then held through a block of sales. This matters when repricing is operationally costly, constrained by contracts, or visible to customers. Chen, Chao and Wang study pricing jointly with inventory replenishment under censored demand. Their Theorem 2 asks how much regret is unavoidable when the seller can change price at most times, regardless of the learning policy it uses (SSRN revision, pp. 10–11, 35–42).
The lower bound is paired with their Theorem 1: in the well-separated setting an algorithm attains regret proportional to for large horizons, while Theorem 2 asserts the same exponent cannot be improved uniformly over admissible policies (SSRN revision, p. 10). The paper appeared as an Operations Research technical note in 2020 (DOI 10.1287/opre.2020.1993); this mission cites the authors' SSRN revision dated 2020-02-10, whose page and result numbers are used throughout.
The horizon has periods. At each period the seller posts a price and replenishes inventory to one unit. Demand is either zero or one, so all demand can be served and the observed sale equals demand. The unknown scalar parameter belongs to . Conditional on the posted price, the probability of one unit of demand is
Holding and shortage costs are zero. Hence expected one-period revenue is . The clairvoyant benchmark is : it is attained by the feasible price . The local Lean sanity check proves this maximum property, so the benchmark does not rely on a default value of a supremum. The model is the explicit Bernoulli construction in the proof of Theorem 2 (SSRN revision, p. 35).
An admissible randomized policy may draw random bits and use past posted prices and observed sales when choosing its next price. Its action cannot depend on future demand or on the unknown parameter. Every realized seed and demand path must satisfy the price-change constraint
The regret is the expected sum of under the policy and the demand law at parameter . The paper's admissibility and change constraint are stated on pp. 5–6; its randomized policy factorization is displayed in (49) on p. 35 (SSRN revision).
The goal is the minimax reading of Theorem 2. For each fixed , there is a positive constant and a horizon threshold , independent of the policy and the horizon, such that
The parameter is selected after the policy. The proof's objective (56) is a worst-case parameter choice for each policy (SSRN revision, p. 37). The printed theorem sentence can also be read as one fixed instance defeating every algorithm; that order is false because a policy supplied with that instance's can post in every period.
Five milestones expose the source's quantitative ingredients. The hierarchy (50) constructs parameters from signs and scales . Its parameters lie in for large . Different signs are separated at scale . Lemma 1 bounds one-period regret by the squared error in a nearest-instance selection. The pointwise inequality underlying (57) gives a cost of at least for a wrong sign. A corrected Lemma 2 supplies a quadratic Bernoulli relative-entropy bound under an explicit interior condition (SSRN revision, pp. 36–37).
The exponent quantifies the cost of the change budget: fixing leaves a polynomial regret floor even though the Bernoulli demand law is one-dimensional and observed without censoring. Since the constructed instance fixes inventory at a level that serves every demand, a lower bound here also applies to policies in the joint pricing and inventory setting whenever that instance is admitted. It identifies the information loss caused by limited repricing, independently of lost sales and censoring.
The paper states the lower bound and gives a proof, but its printed Lemma 2 is false at prices where . The subsequent Lemma 3 applies that unrestricted bound. Therefore the source proof does not, as printed, establish the minimax claim for every admissible price policy. The Lean goal is an open target; the four elementary milestones and corrected information bound are also open Lean statements. Formalizing this mission requires an argument that handles prices at the zero-demand kink, or a different route to the lower bound. No machine-checked proof of this specific result is claimed here.
The natural comparison of two nearby parameters uses the relative entropy between their observed demand laws. Away from the kink, this information is quadratic in the parameter difference. At a price that makes demand impossible under one parameter but possible under the other, the divergence in the printed direction can be linear in that difference. The unrestricted bound of Lemma 2 therefore fails at exactly the prices an arbitrary policy may choose. Restricting the policy's prices would change the target. A faithful proof must retain those prices while still controlling the policy's information and regret (SSRN revision, Lemmas 2–3, pp. 36–40).
Lean represents the horizon by Fin T; its index zero is period one in the paper. Bernoulli demand paths have type Fin T → Bool. A policy's price at a period depends on a random seed and only the earlier demand bits; with inventory level one, these bits are exactly the observed sales. A probability measure on the seed models adaptive randomization, including a pre-sampled stream of random choices. Prices are measurable functions of the seed for each finite history. The budget holds on every seed and path, not only on average.
Path probabilities are finite products of conditional Bernoulli probabilities. Regret is a finite sum of nonnegative gaps integrated over the seed with lintegral, so it cannot become zero through non-integrability of a real-valued expectation. The exponent of and the scales use real division. The arg-min in (51) is any genuine nearest-instance selection; a local proof checks that one exists. The hierarchy's validity and separation statements require a large-horizon threshold, which the unqualified printed prose omits. The corrected Lemma 2 adds to keep the Bernoulli probabilities in the interior. Its verbatim milestone retains the printed statement, and its formal statement and note disclose the correction. Lemma 3 is not stated because its printed proof relies on Lemma 2 outside that interior region.
The named Bernoulli family strengthens the theorem's existential instance wording, while also exposing a limitation: at it violates the positive-mean and identifiability conditions stated earlier in the paper. That discrepancy is recorded rather than hidden in an assumption. Definitions for randomized adapted policies, finite path laws, the parameter hierarchy, and Bernoulli relative entropy are reusable; contributions that establish the open goal or repair the information comparison are in scope.
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.
Maximizing a homogeneous polynomial over the unit sphere, , covers the largest stable set of a graph (degree three), the norm of a matrix (degree four) and the best separable state problem of quantum information. For quadratic it is an eigenvalue problem; for degree at least three it is NP-hard. The sum-of-squares hierarchy of Parrilo and Lasserre replaces " on the sphere" by " is a sum of squares of polynomials of degree at most on the sphere", giving upper bounds that are computable by a semidefinite program of size and decrease to . How fast they converge decides how large has to be for a given accuracy. Fang–Fawzi, §1–1.1
Timeline:
Write , , and . A matrix polynomial has a real polynomial in each entry, and is the real matrix of values. means that the symmetric matrix is positive semidefinite. A matrix polynomial is -sos on if there are finitely many matrix polynomials , each entry of total degree at most , with
For a scalar polynomial , is the least such that (a matrix) is -sos on , and is the minimum of on . The level value is when no such exists.
The milestones use three further objects. A harmonic decomposition of a homogeneous of degree is with homogeneous of degree and . is the least constant with for all such in all dimensions. The Gegenbauer coefficients of a univariate polynomial are its coefficients against the orthogonal polynomials for the weight on , equation (9). For of degree at most , the kernel error is
For every there are constants depending only on such that, for all and every matrix polynomial , homogeneous of degree with , symmetric at every , with on :
The goal fixes only the shape and the regime , and leaves the constants open.
They follow the paper's proof, in attack order:
Theorem 2 says how the level must grow with the dimension: suffices for relative error , where Reznick's analysis needs . Theorem 10 of the paper shows that, for , the kernel error of this technique really is of order . Independence of the matrix size gives certificates for polynomials that are bihomogeneous of degree on . The paper's Theorem 15 uses this, together with the DPS duality of the companion mission, to bound the convergence of the DPS hierarchy for separability. Fang–Fawzi, pp. 3, 10, 14
The theorem is proved in the 2019 preprint and was published in Mathematical Programming in 2021. No machine-checked proof of it or of its ingredients is known. Proving it formally takes reusable infrastructure: degree-bounded matrix SOS on the sphere, harmonic decomposition of homogeneous polynomials, Gegenbauer polynomials with their coefficients and the Funk–Hecke formula, and spectra of Jacobi matrices of orthogonal polynomials. The milestones also correct the printed text, as listed under Formalization scope.
Positive semidefiniteness of at each point of the sphere does not give a factorization with factors of prescribed degree, and Reznick's kernel only reaches error . Two estimates must be uniform at once. First, harmonic projection of a degree- form must be bounded in sup norm independently of ; the bound is easy, and the sup-norm bound is the content of Proposition 5. Second, the kernel error must be bounded throughout the regime , which comes down to the location of the largest zero of a Gegenbauer polynomial. The printed bounds on that zero and on in Proposition 7 are false in small dimensions, so the paper's explicit constants cannot be relied on.
Fin d → ℝ (0-based coordinates), and is the equation , not the sup-norm sphere. Matrix polynomials are matrices over MvPolynomial (Fin d) ℝ, evaluated entrywise, and homogeneity is entrywise.Measure.toSphere.Proofs of any milestone are welcome. So are reusable developments of Gegenbauer polynomials, spherical harmonics, the Funk–Hecke formula, Jacobi matrices, and Carathéodory-type finite quadratures that turn an integral of squares into a finite sum of squares.
A newsvendor chooses an order quantity before seeing demand. Unsold units have no salvage value, while demand above the order quantity cannot be filled. If the demand law is unknown but a few moments are known, the decision maker may minimize cost against the worst distribution consistent with those moments. Das, Dhara and Natarajan study this distributionally robust problem when the known moments are the first and an arbitrary real moment of order Das, Dhara and Natarajan, 2019. The high-demand tail matters especially when the cost ratio favors large orders. The mission asks what tail behavior is implicitly selected by the robust objective, even though each admissible distribution has a finite th moment.
The two-moment case goes back to Scarf's newsvendor bound. The paper extends the model to noninteger and gives lower and upper shortage bounds before proving its tail result. Its preprint is the pinned source for every statement here; the proof of each numbered result follows that result in the paper Das, Dhara and Natarajan, 2019, §§1, 3–4.
Let be the order quantity and let be random demand. The expected shortage under a demand law is , where . Fix , a positive mean , and a moment . The moment ambiguity set contains all probability laws supported on whose first moment is and whose finite th moment is . Its worst-case expected shortage is
For a critical ratio , the robust newsvendor minimizes over . This mission centers on ; the optimal-order threshold is treated in the companion mission. The ambiguity set and objective are the paper's (3.1)–(3.3) Das, Dhara and Natarajan, 2019, pp. 10–11.
A positive function is regularly varying with index if as for every . The notation is . For a probability law , its survival tail is ; means a tail parameter Das, Dhara and Natarajan, 2019, §4.1, p. 26.
The first target is Theorem 4.3(a):
It covers every , including . Scarf's piecewise formula (1.3), Proposition 3.3, and both parts of Proposition 3.4 supply the paper's cited bounds. Each upper bound retains its strict quantity threshold and its printed denominator Das, Dhara and Natarajan, 2019, pp. 3, 15, 19, 28.
The full goal, Theorem 4.3, also states that a nonnegative probability law exists outside with
Every moment of of order is finite, while every moment of order is infinite. The milestone list includes the properties of stated in §2.1 (non-increasing, convex, for , ), the single-law representation (2.1) and the two stated Karamata results used to characterize the tail Das, Dhara and Natarajan, 2019, pp. 6, 27–30.
A companion milestone is Proposition 4.1. For let be a robust optimal order quantity and the optimal robust cost. Then is optimal for the standard newsvendor with demand law , and
Das, Dhara and Natarajan, 2019, p. 30, (4.9). It is a consequence of the goal, not a step toward it.
The theorem connects a decision made against an entire moment class to a single effective law. That law matches the robust expected shortage for every admissible order quantity but has an infinite th moment, so it does not belong to the class being optimized over. This distinction explains why large robust orders behave as though demand were heavy tailed. The paper also uses the result to relate the robust optimal order quantity to the optimal cost at high service levels in Proposition 4.1 Das, Dhara and Natarajan, 2019, pp. 30–31.
The mathematical theorem was proved in the cited paper. This mission asks for a Lean proof of its exact statement and reusable formal results for moment-constrained probability laws, stop-loss transforms, and regular variation. No machine-checked proof of these particular statements is part of the present draft. The cited bounds and analytic results are posed as separate milestones so their hypotheses and constants remain inspectable.
Pointwise optimization over demand laws does not automatically give one law that attains the worst-case shortage for every . For a fixed , an extremal law may depend on , as Scarf's formula illustrates Das, Dhara and Natarajan, 2019, p. 3. The theorem asks for a single and then a precise tail index and a sharp moment cutoff. A generic upper bound on shortages would establish neither the representative law nor its infinite th moment. The regimes , , and have different cited upper-bound statements, yet the final theorem has no regime restriction.
Lean represents a demand law by a Borel measure on with probability mass one and zero mass below zero. Membership in requires both real moments to be integrable; this makes the moment equalities genuine rather than default values of a nonintegrable Bochner integral. Under and , the paper's two-point law (3.6) makes the ambiguity set nonempty. Its shortage values are bounded above by , so the real supremum defining is finite and meaningful. The strict thresholds in Propositions 3.3–3.4 keep their power denominators positive Das, Dhara and Natarajan, 2019, pp. 12, 15, 19.
Regular variation includes eventual positivity, excluding a zero-over-zero ratio from passing as a tail law. Infinite moments of are lower Lebesgue integrals in extended nonnegative reals. The existence of is asserted rather than built into a definition. Theorem 4.2(b)'s displayed limit has a negative sign in the preprint, although its nonnegative numerator and denominator require the positive value ; the formal statement uses the corrected sign. Its regularly varying tail integral is eventually positive, which ensures genuine finite tail integrals for large lower limits. Theorem 4.1 explicitly requires local integrability. Two encodings would trivialize the goal and are excluded: defining inside the statement (it is existential), and a regular-variation predicate satisfied by the zero function. The properties of and the representation (2.1) are stated for , the instance the paper uses, rather than for a general finite-mean ambiguity set. In Proposition 4.1 the optimal cost is the cost at the chosen optimizer, the statement holds for every selection of optimizers, and means that the ratio of the two sides tends to as . These analytic conventions and the probability and measure infrastructure can be reused beyond this mission. Contributions to any of the ten source milestones, including the difficult root assertion in Proposition 3.4(b), are welcome.
In 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.
A prophet inequality compares a gambler who sees nonnegative random rewards one at a time, and must accept or reject each on arrival, with a prophet who knows all values in advance and simply takes . For independent and identically distributed (i.i.d.) rewards the question is the best constant such that some online rule always earns at least . The question matters in operations research and mechanism design because a seller who posts take-it-or-leave-it prices to arriving customers faces exactly this stopping problem on the customers' virtual values; prophet inequalities translate into revenue guarantees for posted price mechanisms relative to Myerson's optimal auction (Chawla, Hartline, Malec and Sivan 2010).
Timeline (as recounted in §1 of the paper):
Let be i.i.d. nonnegative random variables with distribution function . A threshold rule fixes real numbers and stops at
receiving . Because the thresholds may change with the step , the rule is adaptive; for i.i.d. variables the number of variables already seen is all the history the rule needs.
The analysis works with quantiles. The generalized inverse is , and is the threshold that accepts with probability (with a coin toss to break ties at an atom). The function
is the expected reward from a variable accepted with probability . The quantile stopping rule of Algorithm 2 partitions into intervals , draws an acceptance probability with density proportional to , and stops at step with probability ; its value is . The analysis then passes through the normalizations and , the recursion (8)–(9) on , and the differential equation
Let be the unique solution of
For every and every law of nonnegative i.i.d. there are thresholds with
In order: the quantile sandwich ; the representation (7) ; the identity "expected reward of the quantile rule at equals "; Lemma 4 (); Lemma 5 ( when all agree); the equivalence of equal with the recursion (8) and ; the closed form (9)–(10); Lemma 6 on (ODE); Proposition D.1; Lemma 7 (); uniqueness of in (2); optimality of the dynamic-programming thresholds; domination of the randomized rule by them; and .
A companion statement records the numerical guarantee .
The result. Theorem 2 gives the optimal constant of the i.i.d. prophet inequality and, through , shows for every , which settles the problem posed by Hill and Kertz in 1982. Since (Kertz 1986), no rule of any kind achieves a better constant uniformly in . Through the virtual-value connection it implies that, for customers with i.i.d. valuations, an adaptive posted price mechanism earns at least a fraction of the optimal auction's revenue (Corollary 2 of the paper).
Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of any of its lemmas is known. The proof combines a measure-theoretic part (quantile functions, randomized tie-breaking at atoms, Tonelli and integration by parts), a combinatorial recursion, and real analysis of an autonomous ODE with a third-derivative Taylor argument. Formal versions of these parts are reusable: the quantile representation of , the expected reward of a quantile rule, and the optimality of dynamic-programming thresholds are standard tools across prophet inequalities and optimal stopping.
The obvious attempt, computing the optimal dynamic-programming thresholds and bounding their value against , does not lead to a closed-form constant: the optimal values satisfy a nonlinear recursion that depends on the whole distribution. The paper avoids it by analysing a randomized rule whose value is exactly a -weighted average of , which reduces the problem to a distribution-free recursion. Two steps then carry the weight. First, randomizing correctly at atoms of so that every step accepts with probability exactly ; without this, is not the step reward. Second, comparing the discrete recursion (9) with the continuous (ODE): the comparison needs strict convexity and , and the latter holds only because , a standing assumption validated at at the end. The existence of the partition with all equal (a solution of (8) with , , ) is taken from Hill and Kertz and is not proved in the paper.
Lean conventions:
SamuelCahnProphet.IID.iidLaw μ n (the published i.i.d. setting), and is its Emax. Coordinates are 0-based; the partition , , and the recursion keep the paper's 1-based index.A degenerate cannot trivialize the goal: is pinned by (2) and , and the goal is stated for every and every nonnegative law, including laws with infinite mean.
A complete development needs the quantile function of a law on , Tonelli's theorem on product measures, uniqueness for ODEs with locally Lipschitz right-hand side (ODE_solution_unique), and Taylor's theorem; the existence of the Hill–Kertz partition is a further proof obligation. Contributions to any milestone, and reusable lemmas on quantile functions and finite-horizon optimal stopping, are welcome.
A quantum algorithm for a system of linear equations must turn operations it can implement into an approximation of the inverse of the system matrix. For a Hermitian matrix, time evolution is such an operation. Childs, Kothari and Somma use a Fourier expansion of the scalar reciprocal to express an approximation to as a finite linear combination of these evolutions. Their paper reports an exponential improvement in the dependence on the requested precision over earlier linear-systems methods. The scalar approximation in Lemma 11 is the mathematical input to their Fourier algorithm and to the query and gate analyses in Theorem 3. This mission isolates that approximation and the Gaussian estimates stated around it. Theorem 3's complexity claims themselves are outside the present formalization. Childs, Kothari and Somma, §3, pp. 10–14.
Fix a condition number . The scalar spectral domain is
It contains the real eigenvalues permitted after the paper's normalization and excludes zero, where the reciprocal is undefined. For an accuracy , two functions are -close on when their difference has magnitude at most at every point of that domain. A complex-valued approximant is compared with as a complex number. The paper gives this domain and closeness convention before the Fourier construction. Childs, Kothari and Somma, pp. 9–10.
The intermediate function is a truncated Gaussian Fourier integral. It integrates over and then over , multiplying by . The finite approximant is a Gaussian Fourier double sum with the same normalization and phase. Its samples are for and for ; each term carries both mesh widths. Thus count the retained samples, while control their spacing. The sign in the phase and the factor are part of the definitions. Childs, Kothari and Somma, (18), p. 10, and (21), p. 11.
Lemma 12 says that for cutoffs of scale
the function is -close to on . The proposal includes the paper's explicit error bound (27) and its Gaussian tail bound (28), as well as the Gaussian Poisson-summation identity of Lemma 13. These are separate reusable targets, not replacements for the approximation theorem. Childs, Kothari and Somma, Lemmas 12–13 and (27)–(28), pp. 11–12.
The goal is Lemma 11:
where
The statements impose upper and lower bounds with absolute constants, uniformly across and . The requested approximation error is exactly , matching the lemma's claim. The four scales specify both the size of the finite expansion and its mesh. Childs, Kothari and Somma, Lemma 11, p. 10.
The finite sum provides the paper's Fourier route from scalar reciprocal approximation to a linear combination of time-evolution operators. Its sample counts and spacings are the quantities that enter the algorithm's implementation costs. A result that only asserted approximation after arbitrarily many samples would not express the bound used there. The truncated integral and Poisson identity also remain useful for other Gaussian quadrature and Fourier-sampling arguments. Childs, Kothari and Somma, §§3.1–3.2, pp. 11–14.
The paper proves these claims on paper. This proposal asks for machine-checked Lean proofs of the scalar statements, including the complex normalization, the finite and infinite sum conventions, and the uniform scale bounds. It does not assert that the quantum algorithm, its Hamiltonian simulation subroutines, or its query and gate complexity theorems have been formalized.
The infinite Gaussian Fourier representation alone does not specify a finite implementable expansion. Restricting both integrals introduces two truncation errors, while replacing them by samples adds discretization and periodic-aliasing effects. These errors have to be controlled simultaneously with , , , and at the scales stated in Lemma 11. Merely taking the mesh arbitrarily fine gives approximation without the theorem's finite-size bounds. The proof also uses a complex Fourier phase although its target is real, and its infinite sums must have their ordinary convergent meaning. Childs, Kothari and Somma, proof of Lemma 11, pp. 13–14.
The Lean development uses for and the cutoff and mesh parameters, for and , and the complex norm for closeness. Finite sums use exactly and ; the integral for is iterated and has nonnegative upper cutoffs. The optional identity (20) is also an iterated integral, with the integral evaluated before the integral. Infinite sums in Lemma 13 are over . The Gaussian integrals and series in the statements are convergent, so Lean's totalized integral and sum conventions do not supply artificial zero values.
The paper's condition-number convention is recorded as and Corollary 10's operating range as . Those conditions keep nonempty and positive. The unnumbered reciprocal-exponential bound from p. 13 has explicitly, because the printed fractions have no value at zero. The bounds quantify their constants before the problem parameters. In particular, choices with unbounded sample counts or vanishing mesh widths cannot satisfy the goal solely by brute-force approximation.
A complete development needs reusable Gaussian integration and tail estimates, complex exponential identities, summability of Gaussian integer series, and Poisson summation in Mathlib's analytic setting. Contributions that establish these general facts, the stated milestones, or Lemma 11 with its original bounds all fit this scope. This mission uses the reviewed shared definition of . Childs, Kothari and Somma, pp. 9–14.
When indivisible goods are shared among people, comparing each person's bundle with another person's bundle is only one way to judge fairness. A second test asks whether a group could repartition the goods it collectively received so that one of its members would reliably obtain more. Groupwise maximin share (GMMS) makes this test for every subgroup. It strengthens the ordinary maximin-share benchmark, which tests only the grand coalition and all goods. Chaudhury, Kavitha, Mehlhorn and Sgouritsa use this distinction to study a complete allocation obtained from their almost envy-free allocation: goods initially left unassigned are given to one unenvied agent. Their Theorem 16 proves that the resulting allocation gives every agent at least four sevenths of her groupwise maximin share under additive valuations. Chaudhury et al., pp. 4–5, 15–16.
The paper first constructs a partial EFX allocation whose unallocated goods have bounded value to every agent. Its Section 3 then assumes additive valuations and derives maximin-share and GMMS guarantees. This mission addresses the GMMS consequence of that construction. The existence of the starting allocation is the subject of the first mission in this series; the present theorem specifies what happens when its pool is donated. Chaudhury et al., Theorems 8 and 16.
Let be a finite set of agents and a finite set of indivisible goods. Each agent has a valuation for a bundle . Here valuations are nonnegative and additive: is the sum of the values of the individual goods in . A partial allocation gives pairwise disjoint bundles to the agents. The remaining goods form its pool, . An allocation is complete when its pool is empty. These are the paper's allocation conventions. Chaudhury et al., pp. 3–4.
An allocation is envy-free up to any good (EFX) if, after any single good is removed from agent 's bundle, agent values that remainder no more than her own bundle: for all and . The envy graph has a directed edge when values 's bundle more than her own. A source is a vertex with no incoming edge, so nobody envies that agent. Chaudhury et al., pp. 3, 8.
For a set and a positive number of parts, is the largest worst-part value agent can secure by partitioning into bundles. A complete allocation is -GMMS when each agent meets an fraction of this benchmark for every subgroup containing her:
The benchmark uses only goods allocated to that subgroup. The paper states it both as a complete-allocation property in its introduction and in Definition 15. Chaudhury et al., pp. 5, 15.
Assume is partial and EFX, every agent satisfies , and is a source of its envy graph. Define and for . The goal states that is complete, that donation does not lower any agent's own value, and that
This is the GMMS bullet of Theorem 16 applied to the particular allocation the authors define immediately before it. The paper obtains a suitable from Lemma 12, which has the relevant properties of Theorem 8. Chaudhury et al., pp. 11–12, 14–16.
The milestones are Proposition 13, the reduction step in Theorem 16's proof, and all three parts of Lemma 17. Proposition 13 compares maximin shares after deleting agents and at most as many goods. Lemma 17 bounds the value of each bad good, the donated bundle, and the other good bundles. They retain the constants and used in the paper. Chaudhury et al., pp. 14, 16–17.
The result turns an almost envy-free partial allocation into a complete allocation with a guarantee for every coalition. A plain maximin-share statement would only compare each agent with a partition of all goods among all agents; here every subgroup and its allocated goods count. The distinction matters even when an ordinary maximin-share bound is easy to meet because there are fewer goods than agents. Chaudhury et al., p. 5.
The paper proves Theorem 16 mathematically. The remaining work for this mission is a machine-checked proof of its stated GMMS consequence and its supporting results. Its definitions of partial allocation, pool, finite maximin share and groupwise guarantee can also serve later formalizations of fair division. The Nash-social-welfare half-guarantee in the printed theorem depends on the starting allocation from Lemma 12; this mission records only the value preservation under donation. Chaudhury et al., pp. 14, 16.
Giving all leftover goods to one agent makes the allocation complete, but it can change how another agent values that enlarged bundle and how a subgroup's benchmark is calculated. EFX alone compares bundles after deleting one good; GMMS compares an agent with every repartition of a subgroup's goods. The difficulty is to control those repartitions while keeping the exact constant. Merely applying an ordinary maximin-share bound to the grand coalition does not establish the required subgroup inequalities. Chaudhury et al., pp. 15–17.
Agents and goods are represented by Fin n and Fin m; Lean numbers agents from zero, and the paper's “agent 1” is an explicit source . Bundles are finite sets. Valuations are real-valued but include nonnegativity alongside additivity, representing the paper's codomain . The pool is computed from , and the donated allocation is a function of and . No independent pool or arbitrary completed allocation is allowed. Completeness is a conclusion. The maximin share is a finite maximum of finite minima over labelled partitions, which may have empty parts. Every use has a positive part count; in the GMMS definition this follows from . Cardinality is converted to real numbers before fractions are formed. These choices exclude zero-part maximin shares and integer division. Chaudhury et al., pp. 3–5, 15–16.
The theorem is conditional on the EFX and pool-value properties of the source allocation, rather than repeating its existence proof. It states the conclusion for every such allocation and every source. The paper's half-optimal-Nash-social-welfare bullet is outside this mission because it invokes the separate black-box starting allocation of Lemma 12. Contributions toward finite-partition comparisons, EFX value bounds, and the groupwise estimate are welcome. Chaudhury et al., pp. 14–17.
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.
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.
Mobile devices can divide work between local execution, a nearby shared cloudlet, and a remote cloud. A cloudlet has limited capacity, so one user's choice changes the delay faced by the others. Cardellini and coauthors model this as a generalized Nash equilibrium problem, in which each user's feasible choices depend on the aggregate cloudlet load. The shared utilization cap makes a direct distributed solution awkward: a user must know how much capacity all other users consume before choosing a feasible deviation. The paper therefore introduces an additional player who sets a cloudlet price. This mission formalizes the relationship between the original coupled game and that extended, ordinary Nash game Cardellini et al., accepted manuscript, pp. 10–16.
There are users and cloudlet servers. User chooses fractions , , and for local, cloudlet, and remote-cloud execution. These fractions are nonnegative and sum to one. At most a fraction can be offloaded, and a user-specific linear power constraint applies. The set contains these private feasible choices. The cloudlet load and the shared feasible set are
Each user's cost is the response-time expression on p. 10, with coefficients . The VI map is the stack of the user's partial gradients, written in closed form on p. 11. A variational solution belongs to and satisfies for every . The pairing sums all three coordinates for each user. Section 5 assumes and for every user; the model also has and Cardellini et al., pp. 7, 9–11.
The extended game replaces the joint cap in each user's feasible set by a price. User minimizes over . A cloudlet manager chooses to maximize . The manager's choice is part of the Nash equilibrium condition, not a preimposed complementary-slackness equation. The extended game's VI set is and its map is Cardellini et al., p. 15.
The goal is the two-part assertion of Theorem 2. Under the standing assumptions and a strict load bound on the full product of private feasible sets, its equilibrium characterization is
The same goal states that monotonicity of on implies monotonicity of on . The three milestones follow the paper's path: the extended Nash game is equivalent to its VI; the shared affine constraint has a scalar multiplier at a VI solution; and the price-load coupling cancels in the monotonicity pairing. The source states the first as a classical result and gives the last two in its proof Cardellini et al., pp. 15–16.
The characterization lets a variational solution of a game with coupled feasible sets be found as an equilibrium of a game whose users have separate feasible sets. The additional scalar has a concrete interpretation: it is the multiplier of the shared cloudlet-utilization cap. The monotonicity assertion connects the paper's analysis of the original VI to methods for the extended one. The paper uses this relationship as the entry point for its distributed algorithms in the next section Cardellini et al., pp. 16–17.
The result is proved in the paper but is not yet machine checked in this mission. A complete development would give reusable Lean interfaces for a finite-dimensional VI on an intersection of a product polytope and one affine half-space, a multiplier characterization for that intersection, and an equilibrium-to-VI conversion for separable player constraints. Those components could support other capacity-sharing games. The theorem drafts remain proof obligations; the definitions compile locally.
A Nash equilibrium requires each user to be optimal against every privately feasible deviation, including deviations that violate the original shared cap. Consequently, the user's cloudlet cost must remain well defined throughout for the equivalence to hold. A load bound only on does not cover those deviations. The multiplier comparison must also account for the manager's maximization condition and the sign of the load term in . For monotonicity, evaluates on the whole product , a larger domain than . These domain distinctions explain why the statement needs two explicit repairs to the printed theorem Cardellini et al., pp. 15–16.
Lean represents the users as Fin N and the three processing locations as a finite tier type. Indices therefore start at zero. The costs, the map , the private sets, , and are separate definitions. The Euclidean pairing is written as a finite sum; no Pi-type sup norm is used. The extended Nash predicate quantifies over user deviations in and over every nonnegative manager price. The VI predicates are in their own module so the game is not built into their meaning. The theorem's statement remains meaningful at ; no positive-user hypothesis is added to Section 5's assumptions.
The first repair requires at every . The paper's Theorem 1 condition (18) implies this bound, but is stronger than needed. Without the bound, a private deviation can cross the pole of ; Lean's total division then assigns a value at a zero denominator even though the paper's cost has none. In a two-user instance with , and , the pole can lie within one user's private feasible interval. The second repair reads “the original game is monotone” on , because that is precisely the -domain of . Monotonicity on alone is insufficient. Both repairs are disclosed in the item notes, and the source wording remains visible in the milestone quotations.
An empty would make a solution statement vacuous; the formal development should retain concrete feasible parameter instances. The map is the paper's displayed formula, rather than a derivative chosen to make a milestone tautological. The VI uses all user coordinates, and the extended game does not silently reinstate the shared constraint in user deviations. Contributions toward the stated multiplier theorem, Nash-to-VI equivalence, and the cancellation identity are welcome, along with reusable finite-dimensional convex-analysis lemmas.
Allocating indivisible goods fairly is difficult because a single good can change how an agent compares two bundles. Exact envy-freeness can be impossible (one good, two agents), so the field works with relaxations. Envy-freeness up to any good (EFX) requires each agent to prefer her own bundle to every other agent's bundle after any one good of that other bundle is removed. Whether EFX allocations of all goods always exist is open; the question motivates weakening the requirement that every good be assigned, and asking how little must be left over. Chaudhury, Kavitha, Mehlhorn and Sgouritsa show that leaving a small, unenvied set of goods unallocated (donated to "charity") suffices for every normalized monotone valuation profile (arXiv:1907.04596v3, Theorem 8, pp. 11–12).
Timeline (as recounted on pp. 2–3 of the source):
The two bounds matter separately. The empty allocation is EFX and donates everything; a cardinality bound alone still lets the donated goods carry most of an agent's value; the value bound alone allows almost all goods to be donated. The paper's later maximin-share and groupwise-maximin-share guarantees (Theorems 14 and 16, treated in the next missions of this series) are derived from exactly the allocation produced here.
There are agents, indexed by in the paper, and a finite set of indivisible goods. Agent has a valuation . It is normalized if and monotone if implies . No additivity, submodularity or substitutes condition is assumed. These are the general valuations of §1.1.1, p. 3, and §2 of the source.
A partial allocation consists of pairwise disjoint bundles . Its pool is the goods not assigned to anyone,
The allocation is EFX when
The paper calls allocations partial by default (p. 3, footnote 5). The envy graph has the agents as vertices and an edge when . A source is a vertex with no incoming edge. Its reachability component includes itself. The social welfare of is . These notions are introduced on pp. 8–9 of the source.
For a set of goods, an envied set is one some agent values more than her own bundle. An inclusion-wise minimal envied subset is envied, but no strict subset of is envied by anyone. An agent who envies such a is a most envious agent of ; the paper allows ties. The three update rules U0, U1 and U2 use these sets to change an allocation while maintaining EFX (Definition 3 and Algorithm 2, p. 9).
The goal is the allocation guarantee of Theorem 8:
Both the stronger source-count bound and its consequence are stated. The theorem asserts existence for every normalized, monotone valuation profile, including nonadditive profiles. It does not require the returned envy graph to be acyclic; acyclicity is an invariant used during construction, rather than an additional advertised property of the final allocation.
The attack path consists of the paper's numbered Lemmas 2, 4, 5, 6 and 7. Lemma 2 concerns removal of envy cycles; its Lean form keeps the page's conditional "if is EFX then is EFX" and the unconditional strict welfare increase. Lemma 4 records what U0 does and what its failure implies. Lemma 5 records U1's welfare and EFX guarantees. Lemma 6 supplies the finite source, good and agent data required for U2. Lemma 7 states U2's welfare and EFX guarantees. Their source wording and page locations appear in the milestone list; the Lean statements include the exact allocation updates where those lemmas rely on them.
The theorem guarantees a partial EFX allocation even for general monotone valuations, while limiting the unallocated pool more tightly than the number of agents: its size is below the number of unenvied agents. Every agent also values that entire pool no more than her own bundle. These two bounds distinguish the allocation from a merely EFX partial allocation. They provide the starting point for the paper's later statements on approximate maximin shares under additive valuations (Theorems 14 and 16).
The mathematical result is proved in the paper. The mission asks for a machine-checked proof of its allocation guarantee and of the supporting lemmas, with a reusable Lean account of finite partial allocations, the unallocated pool, envy graphs, minimal envied subsets and the update rules. Such definitions are useful for other fair-division questions involving unallocated indivisible goods.
EFX must hold after the allocation is changed, for every agent pair and for removal of every good from the other agent's new bundle. Simply giving a pool good to an agent may violate that condition, even though it makes the pool smaller. Conversely, replacing a bundle with an envied subset can improve welfare while returning goods to the pool. The source-count bound depends on controlling both kinds of progress. Rule U2 adds a further complication: its bundle moves follow envy paths, so an overlap between selected paths would make the new allocation ambiguous. These are the points at which the straightforward approach of distributing the remaining goods one at a time stops working.
Lean represents agents by Fin n, goods by Fin m, bundles by finite sets of goods, and valuations by real-valued functions on bundles. The paper's one-based subscripts become zero-based Lean indices. Nonnegative values need no separate hypothesis: normalization and monotonicity imply them. The hypothesis is explicit because the paper presumes agents and the strict bound is false when . The pool is computed as the complement of the union of pairwise disjoint assigned bundles. It is never a free set. EFX ranges over every pair , including , and every good of .
The minimal-envied-subset definition checks every strict subset against every agent. The most envious agent is a relation, allowing the paper's arbitrary tie choice. Reachability includes a path of length zero. U2's new allocation is calculated from its paths and chosen subsets. Lemma 6 includes Algorithm 1's acyclic-graph invariant and the ordering property established in its proof. It replaces the printed threshold with , the exact number of fresh goods its construction needs and the threshold used by the goal. Lemma 7 takes that ordering property to make path assignments unambiguous.
The printed U2 pool expression in Algorithm 2, line 13, is malformed; the formal statement uses the pool of the constructed allocation and the corrected union of leftover goods. Theorem 8's final sentence also asserts an iteration bound. This mission poses the allocation conclusions, while a future run-level formalization would be needed to state and check the iteration count. The paper's preceding count of U1/U2 steps and successive U0 steps does not by itself imply the printed number. Definitions and the numbered lemma statements are welcome contributions; a purported proof that uses a free empty pool, overlapping bundles, zero agents or an arbitrary replacement allocation would not establish this target.
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 scheduling decisions are not owned by a single decision maker. A machine shared by two departments, a production line serving two customers, or a computing resource shared by two users must process the jobs of two agents, each of which judges a schedule by its own criterion. Agnetis, Mirchandani, Pacciarelli and Pacifici introduced this model in Scheduling Problems with Two Competing Agents (Operations Research, 2004, doi:10.1287/opre.1030.0092), and it became the starting point of the literature on multi-agent scheduling (surveyed in Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal, Multiagent Scheduling, Springer, 2014, doi:10.1007/978-3-642-41880-8).
When neither agent can impose its criterion on the other, the natural object to compute is the set of compromises that cannot be improved for one agent without hurting the other: the Pareto frontier. Section 11 of the paper asks how large that frontier can be for each pair of criteria it studies, because the size of the frontier decides whether it can be listed in polynomial time. This mission formalizes the answer for one agent minimizing its total completion time against the other agent's maximum cost.
Agent owns jobs and agent owns jobs , with . Every job has a positive processing time , is available at time , and is processed without interruption on a single machine that handles one job at a time. Since both criteria below are nondecreasing in completion times, a schedule is a sequence of all jobs processed in that order from time without idle time, and denotes the completion time of .
A schedule is nondominated if no schedule has and with at least one inequality strict. Its nondominated pair is . The constrained problem asks for a schedule with for every -job that minimizes among such schedules; such a schedule is optimal for the bound .
The -jobs of a schedule follow the SPT order when they appear by nondecreasing processing time, equal lengths in index order. A -job overtakes an -job when it moves from after it to before it.
The paper prints the bound . That bound is false: with one job per agent, unit processing times and , the schedules and give the two nondominated pairs and . The corrected bound is the one the printed argument supports.
A frontier of size at most means that the scheme the paper calls PP, which solves the constrained problem for a decreasing sequence of bounds, lists every nondominated pair with polynomially many calls to a polynomial algorithm (Theorem 5.5 of the paper). The contrast with the other criteria of §11 is the point: for two total-completion-time agents the paper exhibits an exponential frontier (Example 11.7). The bound therefore separates criteria whose compromises can be negotiated over an explicit list from those where they cannot.
Formalizing it adds three things. First, the printed statements need corrections: the bound is off by one, and Lemmas 11.4 and 11.5 are false when identical -jobs may be ordered differently in the two schedules. A machine-checked version fixes the exact hypotheses. Second, the monotonicity of overtakes (Lemma 11.5) is a reusable structural fact about parametric scheduling under a tightening constraint. Third, no part of this paper or of two-agent scheduling has been machine-checked before, to our knowledge; the published sequence model the mission builds on comes from the formalization of Moore's 1968 algorithm.
The obvious argument counts overtakes: as the bound decreases, each -job overtakes each -job at most once, so consecutive frontier points differ by at least one new overtake. The step that does not go through as printed is "at most once". Optimal schedules for a given bound are not unique, and two optimal schedules can disagree on the order of identical -jobs and on the position of a -job between them. Then an "overtake" can be undone between two bounds without any change in the objectives. The counting is valid only for a consistently chosen family of schedules, and turning the comparison of optimal schedules for two different bounds into a strict improvement needs an exchange argument with careful bookkeeping of which jobs shift. A second, smaller gap is the base case: the first schedule of the chain carries no overtake and must be counted separately.
Jobs are Fin nA ⊕ Fin nB, 0-based, and a schedule is a duplicate-free list of all jobs; completion times come from the published definition MooreLateJobs.Shared.completionTime (Moore 1968 series), referenced rather than redefined. Processing times are real and strictly positive, the paper's standing convention, which the exchange arguments use. The bound is real; the paper's integer is a special case. Feasibility for the bound is stated job by job. The maximum cost is a finite maximum and requires .
Explicit readings of the paper's phrases:
Set.encard of a set of real pairs, so the goal asserts finiteness as well as the bound; it is not a Set.ncard, which would be on an infinite set.Nothing in the statements is trivial by construction. The goal is about every instance with positive data, its hypotheses are satisfiable, and the counterexample to the printed bound is checked in Lean. The milestones' SPT hypotheses are met by some optimal schedule of every feasible instance, so they are not vacuous. Running times, including the polynomiality of PP and the choice of the decrement in Figure 4, are not formalized.
A complete development needs exchange lemmas for single-machine sequences (moving a job, swapping two adjacent jobs, and their effect on completion times), the existence of SPT-ordered optimal schedules, and a chain-counting argument for nested sets of overtakes. The exchange lemmas are reusable for any single-machine sequencing mission. Contributions of any of these, and of a proof of the corrected bound that avoids the scheme PP, are welcome.
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.