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?
Which cycle lengths a graph must contain is a classical question of extremal graph theory. A graph on vertices is pancyclic if it has cycles of every length from to ; Bondy's meta-conjecture (Bondy 1971) and a long line of results ask which density or expansion conditions force pancyclicity or, more modestly, force the set of cycle lengths to contain a long interval. For sparse graphs, expansion is the natural hypothesis: random graphs and explicit expanders are sparse, yet very well connected.
Friedman and Krivelevich, Cycle lengths in expanding graphs (arXiv:1912.11011v2; Combinatorica 41, 2021), study two expansion conditions. For the usual vertex expanders they show that cycle lengths are numerous and well spread, but they also note that an expander need not contain any interval of cycle lengths of non-trivial length. Section 4 of the paper therefore introduces a different, two-set expansion condition, the β-graph, and shows that it does force a complete interval of cycle lengths of length linear in . This mission formalizes that result, Theorem 3.
Timeline.
All graphs are finite and simple. For a graph and a vertex set , the external neighborhood of is
Let have vertices and let . is a β-graph if every two disjoint vertex sets with are joined by an edge. For , the complete graph is a β-graph for every ; when , only the complete graph is. No graph on zero vertices is a β-graph.
The set of cycle lengths of is . A cycle of length has distinct vertices.
The proof works with the tree : two complete -ary trees of depth (every internal vertex has children, every leaf is at distance from the root) whose roots are joined by a path of length . A graph contains a copy of a tree if there is an injective map from the vertices of to those of sending edges to edges.
Logarithms are to base .
For every there exist positive constants and such that every β-graph on vertices satisfies
The goal fixes the shape of the bound, not its constants: the proof's choice is , and is a multiple of . As the interval widens towards . The upper end is tight up to the constant: the disjoint union of with isolated vertices is a β-graph.
In the order of the proof (pp. 15–18):
The result. Theorem 3 proves the conjecture of Hefetz, Krivelevich and Szabó in a stronger form: β may be any constant below instead of tending to zero with , and the lower end is of optimal order. Since spectral expanders satisfy the β-graph condition (by the expander mixing lemma an -graph with is a β-graph), the theorem gives long intervals of cycle lengths in pseudo-random graphs. The method, embedding two large trees joined by a path and closing the cycle across their leaf sets, is a template for producing cycles of prescribed length in expanding graphs.
Formalizing it. The result is proved on paper. As far as the platform's records show, none of it is formalized: Mathlib has trees, walks, cycles and graph copies, but no tree-embedding theorem for expanders and no result on cycle lengths of this kind. The main piece of new infrastructure is Haxell's theorem (milestone 3), which the paper cites without proof. Its proof (in Haxell's paper and in Balogh–Csaba–Pei–Samotij) is a few pages of inductive embedding with a Hall-type invariant. A formal proof of Theorem 4.1 would be reusable for any embedding argument for bounded-degree trees, for example in Ramsey and size-Ramsey problems for trees and paths. The printed proof also has a rounding gap (below), so the formal proof will have to settle a slightly different argument from the printed one.
The β-graph condition only speaks about pairs of large sets, while cycles are built edge by edge, so short and long cycles both need a mechanism. The obvious approach, finding a long path and then shortcutting it, does not control which lengths occur. The proof instead needs a robust embedding theorem for trees with about leaves inside a subgraph with good expansion of small sets, and that is Theorem 4.1, a deep result.
A second difficulty is quantitative. In the printed verification of claims (1) and (2) on p. 17, a complete -ary tree of depth is counted as having about vertices, as if exactly. In fact can be almost , and for claim (2) the honest count only covers rather than . For the gap is larger. Theorem 3 is unaffected, because its constants are only and pruning the trees to leaves repairs the count. But a solver following the printed proof will need to repair that step. The two claims are therefore not posed as milestones.
Graphs on vertices are SimpleGraph (Fin n). Vertex sets are Set with Set.ncard, and every inequality involving β, a logarithm or is stated in ℝ after casting. Logarithms are Real.logb 2. Cycles are Mathlib's Walk.IsCycle, so every cycle length is at least . "Contains a copy" is SimpleGraph.IsContained (injective and edge-preserving, not induced). The subgraph of Lemma 4.1 is the induced subgraph on a set , with . The tree is defined on words of length at most over (two tagged copies) plus path vertices.
Conventions of the goal:
Infrastructure needed: Haxell's theorem (reusable well beyond this mission), counting leaves and vertices of complete -ary trees, and turning an embedded plus one edge into a Walk.IsCycle. Contributions to any milestone are welcome, in particular a proof of Theorem 4.1 and a repaired version of claims (1) and (2) with pruned trees.
In a structured bandit problem a learner repeatedly chooses a decision from a set and observes a noisy reward whose mean is an unknown function from a known class . Classical analyses of such problems measure the complexity of by the eluder dimension (Russo and Van Roy, 2013; 2014) or the star number, and prove regret bounds for posterior sampling (Thompson sampling) or optimistic algorithms in terms of these quantities.
Foster, Kakade, Qian and Rakhlin (2021) introduced the Decision-Estimation Coefficient (DEC), a single complexity measure that yields both upper and lower bounds on the minimax regret of interactive decision making. Section 6.2 of that paper connects the DEC to the older parameters: it shows that the square-loss DEC is bounded by the disagreement coefficient of the class, a quantity introduced in Foster, Rakhlin, Simchi-Levi and Xu (2020) and itself bounded by the star number and the eluder dimension. The bound is certified by posterior sampling, so it also explains why posterior sampling works for these classes.
Let be a set of decisions. A model assigns to each decision a reward distribution; here a model enters only through its mean-reward function and an optimal decision . The class collects the mean-reward functions of a model class . A reference model , not necessarily in , has mean reward .
A prior is a finitely supported distribution over . The posterior sampling strategy plays , the law of when .
The prior-dependent square-loss DEC (display (70) of the paper) is
the best trade-off between regret and squared estimation error that a decision distribution can achieve against a model drawn from the prior.
For a class of functions and a distribution on , the disagreement coefficient (Definition 6.3) is
where is drawn independently of . It measures how much mass puts on decisions where some function of the class is large although it is small in . The shifted class consists of the differences , .
For every , posterior sampling certifies
In the formal statement, the objective of (70) evaluated at is bounded by for every and every upper bound of the disagreement coefficients of the shifted classes.
Theorem 6.2 bounds the DEC of any structured bandit class by its disagreement coefficient. With the bounds of the disagreement coefficient by the star number and the eluder dimension (Lemma 6.1 of the paper, from Foster et al. 2020) and the minimax theorem, it yields Theorem 6.1, which recovers the regret bound of Russo and Van Roy for posterior sampling as a special case, and gives a bound in terms of the star number. The decoupling lemma (Lemma E.2) is a general tool: it controls a coupled quantity by a decoupled second moment, and applies wherever an algorithm's decision and the function evaluated there are drawn from the same distribution.
The results are proved in the paper. None of them has a machine-checked proof; this mission produces the first formal statement of the disagreement coefficient and of the decoupling lemma, on which formal versions of eluder-dimension and star-number bounds can build.
The obvious argument fails at the decoupling step. The quantity evaluates each function at its own decision, while the estimation error controls only , with independent indices. For a finite set of decisions, Cauchy–Schwarz bridges the two at the price of a factor ; for an infinite decision space this gives nothing. The disagreement coefficient replaces the cardinality, but it controls disagreement only at one pair of scales at a time (the size of and the norm of ), while the coupled quantity involves all scales at once; obtaining only a loss from this is the technical core of Lemma E.2.
The goal is not trivialized by a junk value: the disagreement coefficient is a genuine supremum under the stated hypotheses (a sorry-free check accompanies the definitions), rules out negative logarithms, the class is the whole class rather than the prior's support, and the reference model is not assumed to lie in the class.
Contributions welcome: proofs of the milestones in attack order; a general layer-cake lemma for finite sums; a formal disagreement coefficient bound by the star number or the eluder dimension (Lemma 6.1), which would lead to Theorem 6.1.
Interactive decision making covers bandits, contextual bandits and reinforcement learning: a learner repeatedly chooses a decision, observes a reward and an observation drawn from an unknown model, and tries to accumulate nearly as much reward as the best decision for that model. Foster, Kakade, Qian and Rakhlin (arXiv:2112.13487) introduced the Decision-Estimation Coefficient (DEC), a single quantity that gives lower bounds on the regret of every algorithm and, through the Estimation-to-Decisions (E2D) meta-algorithm, matching upper bounds. This mission formalizes the upper-bound side in its strongest form: E2D run with Hellinger confidence sets (Option II of Algorithm 1) has regret controlled by the localized DEC, the same quantity that appears in the paper's lower bounds (Theorems 3.1 and 3.2).
The basic E2D guarantee (33) in terms of the global DEC is already posed on Prove2Me as an open goal (FoundationsRL.GeneralDM.e2d_general_regret_bound_v2, the restatement in Foster and Rakhlin's lecture notes, arXiv:2312.16730, Proposition 26). It is not posed again here.
A decision space is a finite set. An outcome consists of a reward and an observation and ranges over a finite set , and is its reward. A model assigns to every decision a probability distribution on . Its mean reward is , and is a decision maximizing . The learner knows a model class that contains the true model . At round it plays a distribution on , and its regret is
Write for the squared Hellinger distance. For a reference model and the DEC is
The localized class keeps only the models whose optimal value exceeds that of by at most .
E2D with Option II receives at each round an estimate from an online estimation oracle. It keeps the confidence set of models whose accumulated Hellinger error against past estimates, , is at most . It plays a minimizer of the DEC problem over at . Assumption D.1 asks that, with probability , the oracle's Hellinger error on the rounds where is at most a known bound . It also asks that .
With , rewards in and , with probability at least ,
The bound is the paper's most general upper bound. Together with the lower bounds of §3, it shows that the localized DEC characterizes the regret of interactive decision making up to the estimation term. With an aggregating estimator satisfying (App. A.3), it recovers the finite-class guarantee of Theorem 3.3. The companions extend E2D to general divergences, randomized estimators and adversarially chosen contexts. That last setting contains SquareCB for contextual bandits.
All results of this mission are proved in the paper. None was machine-checked before. Formalizing them produces a checked reduction from decision making to estimation for finite decision and outcome spaces, stated against the published DEC and localized-class definitions, so that later bounds on the DEC of specific classes (bandits, tabular RL) can be combined with it.
The non-localized bound follows from the per-round step (138) by summation. The localized bound does not: the per-round DEC is taken over the confidence set , and replacing it by a localized class requires that every model surviving in have optimal value close to that of the current estimate . The confidence set constrains Hellinger errors against past estimates, not optimal values, and the estimate itself is in general not a member of the class. Bridging these is the content of Lemma D.2 and the containment. The first round is a boundary case: there the confidence set is the whole class, so the containment holds only if the radius is at least the full range of the rewards.
Fintype), a finite outcome set , and models m : S → Y → ℝ with every m π a probability vector. Expectations are finite sums. Contexts in Theorem 8.1 range over an arbitrary type.decGf, and dec for the supremum over ) and the localized class are the published FoundationsRL.GeneralDM definitions, referenced and not redefined.IsOptionIIRun (lines 7 and 8 and ). "With probability at least " becomes the hypothesis EventD1, the event of Assumption D.1. Line 8's arg min is relaxed to "certifies the minimax value from above", as Remark 4.1 permits. Rounds are 0-based, and is evaluated at the paper's index.IsOptionIIRun. The open bound (33) is not restated.decGf in the class are reusable beyond this mission.Retailers observe demand signals (point-of-sale data, local forecasts) that their suppliers do not. Whether a retailer should pass such a signal upstream is a central question of the supply chain information-sharing literature. In a single chain, sharing helps the manufacturer plan, but the retailer may lose from it. Competition between chains adds a second effect: sharing in one chain changes how the rival chain responds to its own signal.
Ha, Tian and Tong (MSOM 2017) study this question when the manufacturer's planning decision is production cost reduction: a manufacturer that knows more about demand can invest in lowering its unit cost more efficiently. They find that the equilibrium of the information-sharing game between two competing chains depends on a single efficiency parameter in a three-regime pattern. This mission formalizes that pattern for quantity (Cournot) competition.
Earlier work on information sharing in competing chains (for example Ha, Tong and Zhang, Management Science 2011, on production diseconomies of scale) found related threshold structures under different upstream technologies. The present paper replaces the production cost with a cost-reduction investment.
There are two identical supply chains , each with one manufacturer and one retailer. Retailer faces the inverse demand
where is a demand shock with mean and variance , and is the competition intensity. Manufacturer has unit production cost and lowers it by at effort cost ; a small means efficient cost reduction. Retailer observes a signal with accuracy ; under the linear information structure, .
In stage one, each chain fixes its arrangement : the retailer shares its signal with the manufacturer () or not (). Then the manufacturer sets a wholesale price and a cost reduction, and the retailer a quantity. For each arrangement profile the quantity stage has a linear equilibrium with explicit response coefficients (Lemma 2(a)). These give closed-form ex-ante profits , and for the retailer, the manufacturer and the chain.
The value of information sharing to chain is . In stage one, manufacturer offers retailer the smallest side payment that makes sharing acceptable to the retailer, and chooses or . The result is a symmetric game between the two manufacturers (Table 1). Manufacturer 's payoff is for and for . The standing assumptions are , and .
For fixed , and there are thresholds
such that the set of pure-strategy equilibria of the stage-one game is
In the middle regime, both manufacturers are strictly better off at than at .
A companion item states the Cournot half of Proposition 7(c): for no side payment is needed and is the unique equilibrium.
Proposition 7(a) separates three regimes of cost-reduction efficiency. When cost reduction is efficient (), sharing is dominant. At intermediate efficiency the stage-one game is a coordination game: both chains sharing is Pareto-better for the manufacturers, but both not sharing is also an equilibrium. When cost reduction is inefficient, no chain shares. Competition matters through the gap : a chain whose rival shares tolerates a less efficient cost reduction before it stops sharing, and the thresholds fall as signals become more accurate or competition more intense.
The paper proves these facts by hand-checked algebra, often stated as "we can verify". The formalization turns each such step into a checked statement: the fixed-point identities behind Lemma 2(a), the closed forms of Lemma 3, the reduction of the sign of to the polynomials and , and the monotonicity and location of their roots. None of these results has a machine-checked proof yet. The definitions (response coefficients, profits, side payment, stage-one game) are reusable for the Bertrand half of the paper and for other two-chain information-sharing models.
The obvious approach expands and as rational functions of and tries to read off their signs. That does not finish by itself. After cancelling positive factors, the signs are those of and , which are quadratics in with coefficients polynomial in . The thresholds are defined implicitly by a root of each quadratic crossing . Showing that and are initial intervals of needs the relevant root to be strictly decreasing in , to exceed below and to change sign at . The strict ordering needs a comparison of two roots involving and on . The equilibrium analysis then needs the retailer comparison, to know when the side payment is positive. Table 1's payoff entries are valid only in that case.
Everything is over , in the namespace CompetingChains.Cournot. A general definition TwoPlayerGame gives pure-strategy Nash equilibria of a two-player normal-form game. The definition Setting records the paper's reduced form: the standing assumptions, the response coefficients of Lemma 2(a), the best responses (7) and (9), the ex-ante profit functions of p. 17, the equilibrium profits , , , the stage-one payoff and its set of pure equilibria. The Bayesian stages enter only through these closed forms. The arrangements are an inductive type {S, N}. Manufacturer 2's payoff at is manufacturer 1's payoff at . The chain profit is defined as retailer plus manufacturer profit. The stage-one payoff uses as printed on p. 21, and agrees with Table 1 whenever the side payment is positive.
Conventions and added hypotheses, each disclosed in the items:
The coefficients, profits, and payoffs are definitions, never free parameters. A statement with free coefficients, a goal whose thresholds lack , or one that only asserts membership of would be trivial or weaker, and is not what is posed. No published platform definition states this model, so none is referenced.
Not in scope: Lemma 2's uniqueness (delegated by the paper to earlier work), the wholesale-price and cost-reduction lines of Lemma 2(a), the Bertrand half (Propositions 6(b), 7(b)), the single-chain analysis of §4, Proposition 8 and the numerical study. Proofs of any item are welcome. The polynomial root analysis behind Proposition 6(a) is the main open piece of work.
In random-feature models, also called extreme learning machines or random neural networks, the inner weights of a one-hidden-layer network are drawn at random and only the linear readout is trained. Training is then a least-squares problem, which is why such models, and their dynamic counterparts reservoir computing and echo state networks, are used in practice. The question is how well such a network can approximate a target when it is not allowed to choose its inner weights. Gonon, Grigoryeva and Ortega (Ann. Appl. Probab. 33 (2023) 28–69) answer it with explicit, non-asymptotic bounds. Their first result, Theorem 1, covers static ReLU networks on an arbitrary separable Hilbert space. The later results of the paper, on finite-dimensional inputs and on echo state networks, are built on it.
Timeline:
is a separable real Hilbert space with inner product , and is the rectifier. The inner weights , , are i.i.d. with law . For a readout matrix the random ReLU network is
The target is assumed to have a Fourier representation on the ball of radius : for , with complex measures whose total variations have finite second moments (condition (15)). The sampling law has the product form . Two further quantities enter: , and the density , where . The input is an -valued random variable with law and , independent of the inner weights.
If , condition (i) or (ii) on holds, and the integrals (16) of and are finite, then there is a readout , a measurable function of , with
and for every , with probability at least , . Here and
Milestones 2–6 are stated for a single output component (), to which the proof reduces.
Theorem 1 says that only the readout has to be trained. With inner weights drawn from an essentially arbitrary product law satisfying (i) or (ii), a least-squares readout achieves error with a constant computable from the Fourier data of and the sampling law (Remark 3, p. 38). The finite-dimensional rates of Section 4.2 (Proposition 3, Corollary 1) follow from it, and so do, through the reservoir functional's Fourier representation, the echo state network bounds of Sections 5–6.
The result is proved on paper but has no machine-checked proof. A formal proof needs integral representations of Fourier-type functions by ReLU units, Radon–Nikodym arguments for signed measures on product spaces, and the variance identity for i.i.d. averages. A side product of formalizing it is a correction: the printed constant is false for small and has to be replaced by , which agrees with it for .
There is an obvious argument: sample features from and use Maurey's empirical method. It does not apply, because the features here are ReLU ridge functions of a real-valued bias drawn from , not complex exponentials. The proof must first rewrite the oscillatory representation as an integral of rectifiers, (18)–(20). That step uses the realness of , which is not given and follows only from being real near . The signed measure obtained this way must then be absolutely continuous with respect to the sampling law , with a density whose second moment is controlled by (16). In case (ii), may vanish outside a bounded interval, and the support of has to be matched to it.
A complete development needs the following:
The variance identity (25) and the bound (26) are independent of the Fourier setting and reusable. Contributions to any milestone are welcome, and so are alternative proofs of (19) and (20).
An echo state network with output feedback is a recurrent model whose previous output is fed back into its next hidden-state update. In reservoir computing only the linear output weights are trained, while the internal weights are fixed, typically after being drawn at random. This raises a quantitative question: if the internal rows are sampled from a fixed law, can a network with blocks of random rows and a suitable linear readout approximate a given input–output rule, and at what rate in ? Gonon, Grigoryeva and Ortega answer this for targets generated by contracting reservoir systems. Their Theorem 4 (p. 63) gives, with explicit constants, a probability bound and an excess-risk bound of order , plus a term decaying geometrically in the length of the observation window. The input set is not required to be bounded: the bound depends on the input process only through over the window.
Inputs are vectors in a set and an input history is , with . A target reservoir is a map , with the closed Euclidean ball of radius , such that is an -contraction for every , with . Its reservoir functional is , where for all . The output dimension is .
The approximating network has blocks of rows. Each row is a vector , and the rows of are i.i.d. with law . With an activation and a readout matrix , the system is
with and ; its functional is . For each and a signed measure defines the integral map
The constant measures the size of these densities, and is the approximation error of . The input process is independent of , is an integrable target, and the loss is Lipschitz with constant . The echo state event of (87) is the event that for all and , where .
The milestones are the displayed estimates of the proof, in attack order:
There is a readout , a function of alone, such that for every and every , with probability at least , the event holds and
where is evaluated at fixed network weights.
The bound separates three sources of error: sampling blocks of random rows (rate ), the approximation of by the integral map (), and the finite initialization of the feedback recursion (). Only the readout depends on the target; the internal weights are generated without it. The theorem also bounds the probability that the random feedback map leaves the state ball on which the recursion is controlled, which is the form in which the echo state property enters. Via Theorem 3 (p. 62), which specializes the densities through the paper's Proposition 2, it gives approximation rates for ReLU output-feedback networks.
The paper proves the result on pp. 63–68. No part of it is formalized. A complete development would give machine-checked Rademacher symmetrization and contraction estimates for random features, uniform-over-a-ball bounds for sampled integral maps, and a treatment of finite feedback recursions on product probability spaces, all reusable outside reservoir computing.
A pointwise approximation of by the sampled map does not control the feedback system, because the next feedback value is itself the random output of the previous update. The comparison must hold uniformly over the state ball and over the whole input window, and the event that the recursion leaves the ball must be charged to an explicit probability. The uniform bound requires symmetrization and the Ledoux–Talagrand contraction principle for a supremum over a continuum of states, with per-index contractions; Lipschitz continuity of alone does not supply the vanishing at zero that principle needs. The input is unbounded, so the input dependence must be tracked through and integrated at the end.
States, inputs, outputs and rows are Euclidean spaces (EuclideanSpace); a row is indexed by and the rows by . Time is the index ; the equation (78) is the published ReservoirESN.IsSolution. The rows have law on their own space and lives on a separate probability space; the probability is under the product law, which encodes the independence of §6.1. Signed measures are their Radon–Nikodym densities with respect to , with integrability and first-moment hypotheses. , and are extended nonnegative integrals and suprema, converted to reals only under their finiteness hypotheses; the risk integrals are finite under the loss Lipschitz bound, integrable target and input-moment assumption; the supremum in (87) is unfolded. is assumed jointly measurable, the standing convention that makes and random variables; the standing assumptions and (p. 30) and (§6.1) are hypotheses.
Trivialization ruled out. The readout is a measurable function of the rows only and is chosen before and . A readout allowed to look at the input would make the claim a different and much weaker statement.
Correction of the print. The goal and milestones (91), (93), (96) assume : the contraction principle cited at (91) needs contractions vanishing at zero, while the printed theorem states only that is Lipschitz. ReLU, the paper's application, satisfies it. The goal retains the printed full risk difference. Its proof passes through (88), where an indicator depending on is moved inside a risk integral; this step needs further justification. The milestone quotations keep the printed text.
Contributions are welcome on each milestone, on general Rademacher symmetrization and contraction lemmas for suprema over compact parameter sets, on measurability of suprema of continuous random fields, and on the printed form of the risk bound.
Which cycle lengths a graph must contain is a long-standing theme of extremal graph theory, studied for graphs of given minimum degree, chromatic number or density. A natural class in which to ask it is that of expanders: graphs in which every not-too-large vertex set has many neighbours outside it (Hoory, Linial and Wigderson). It is known that an -expander on vertices has a cycle of length and a cycle of length (Krivelevich's survey, Corollary 3.2 and Theorem 7.4, arXiv:1812.11562); the question is what happens between these extremes.
One cannot hope for a full interval of cycle lengths: the complete bipartite graph is an -expander without odd cycles, and subdividing every edge of a bounded-degree expander times gives an -expander all of whose cycle lengths are divisible by . L. Friedman and M. Krivelevich (Cycle lengths in expanding graphs, Combinatorica 41 (2021); arXiv:1912.11011v2) show that this is the only obstruction: the cycle lengths of an -expander are well spread, in the sense that every window of consecutive integers between logarithmic and linear length contains one. This mission formalizes that theorem (Theorem 1 of the paper) together with the lemmas of its §2.
Let be a finite simple graph on vertices. For , the external neighbourhood is .
All logarithms are base . In Lean these objects are extNbhd, IsKAlphaExpander, IsAlphaExpander, cycleLengths, ball, contract, level and levelSet, in the namespace CycleLengthsExp.WellSpread.
For every there are positive constants , and such that for all large , every -expander on vertices satisfies
The goal fixes only the shape of the dependence on , not the constants, so an improvement of the constants does not invalidate it.
The result. Theorem 1 says that, up to an additive error of order , an -expander contains every cycle length from up to a constant fraction of . The additive error is optimal in its dependence on by the subdivision example, and the logarithmic lower end is necessary because expanders can have logarithmic girth. It implies that is linear in for every -expander; the companion mission of this series (Theorem 2 of the paper) improves the dependence on in that count. The lemmas of §2, especially the robust sub-expander lemmas 2.2 and 2.6, the disjoint-paths lemma 2.3 and the depth-first-search lemma 2.5, are general-purpose statements about vertex expanders that do not depend on the cycle-length question.
Formalizing it. The theorem is proved on paper; none of it is machine-checked. Mathlib has walks, paths, cycles, distances and induced subgraphs, but no vertex expansion, no Menger theorem, no depth-first-search path lemma and no breadth-first-tree construction. This mission produces formal statements of all of these at the level of generality the paper uses, and a complete development would supply reusable lemmas about vertex expanders on finite simple graphs.
The obvious argument fails at the step of hitting a prescribed length. Expansion easily gives long paths and long cycles, but controlling the length of a cycle to within an additive requires a structure with many cycles whose lengths differ by small, controlled amounts. The paper builds it from two breadth-first trees joined by many short disjoint paths, a long path routed through bounded-size subtrees, and a pigeonhole selection that avoids spoiling too many subtrees; the explicit constants of Lemma 2.7 then have to be propagated through Theorem 1. Lemma 2.3 additionally needs Menger's theorem, which is not in Mathlib, and Lemma 2.5 is a depth-first-search argument whose formal invariant is not short.
SimpleGraph (Fin n); the ball-growth milestone uses any finite vertex type. Sizes are Set.ncard; inequalities involving , , or logarithms are stated in ℝ. is (n + 1) / 2. Logarithms are Real.logb 2.G.induce U, the edges of , never the edges of a tree.G.dist u v for in one component. The first inequality of the lemma is false as printed (the path with ) and is not posed. Lemma 2.7, item 4, is posed with as printed, although its proof gives .Walk.IsCycle, never closed walks; Lemma 2.1 never uses G.diam, which is for a disconnected graph; and no statement divides by .Collections of genomes, versioned documents and source-code histories are highly repetitive: most of each new item is a copy of something already stored. Full-text indexes such as the suffix array and the FM-index answer pattern queries on such collections, but their size grows with the text length , not with the amount of distinct content. The number of runs in the Burrows–Wheeler transform (BWT) of the text is a standard measure of repetitiveness, and the run-length FM-index of Mäkinen and Navarro counts the occurrences of a pattern in words. Until the work of Gagie, Navarro and Prezza, however, locating those occurrences, i.e. reporting their text positions, required space proportional to for a sampling step , which defeats the purpose on repetitive data.
Timeline.
A text is a sequence over the alphabet whose last symbol T[n]=\=1SA[1..n][1..n]T[SA[p]..n]SA[ISA[i]]=i. The BWT records the character preceding each sorted suffix, $$BWT[p]=T[SA[p]-1]\ (SA[p]>1),\qquad BWT[p]=T[n]=\\ (SA[p]=1),$$ so that is read as . The LF mapping is the counting formula , where counts BWT symbols smaller than and counts copies of in .
A run is a maximal block of equal consecutive BWT symbols, and is their number. A text position is sampled when its character is the first or last BWT character in its run (Definition 1); at most positions are sampled. Definition 3 cuts into phrases that begin exactly at the sampled positions. For a text position , the phrase head of is the greatest sampled position . The permutation (Definition 2) returns the text position in the preceding suffix-array cell, and the differential arrays are and . A text position starts a phrase of when is the first position of a run.
Let , let be the phrase head of , let , and let be the sample stored at . Then
and , respectively, so that is defined.
A companion item, from the proof of Lemma 2 (p. 12), states that a BWT interval holding both and a non- symbol contains an occurrence of at the first or last position of a run.
The goal says that the numbers , one pair per sampled position, determine the neighbours of every suffix-array cell, after one predecessor search over the sampled positions. Combined with the toehold of Lemma 2, which provides one known cell inside the interval of a pattern, it lets an index list all occurrences in space. This is the locating half of Theorem 1 of the paper. The same mechanism reappears throughout the paper: Lemma 4 generalises it to neighbours, Lemma 5 to the LCP array, and Lemmas 12 and 14 drive the access structures for and in §5.
The results are proved in the paper; none of them has a machine-checked proof. The mission contributes a formal model of suffix arrays, BWT, LF and runs that is independent of any data-structure encoding, a checked proof of the LF identity from the counting formula, and the exact correctness statement behind the -index. The handling of the wrap-around phrase (see below) is a case the paper's proof leaves implicit.
The obvious argument follows the three cells backwards under LF for steps. It rests on two facts that are easy to state and not routine to prove. First, must be derived from the counting formula : this is a stable-sorting argument about suffixes that begin with the same symbol, and it uses the uniqueness of \$$. Second, LF must map adjacent cells of a run to adjacent cells, and one must check that the neighbouring cells never leave the run while the middle cell walks from T[k]T[i+1]i\le k[1..k]T[i+1]T[i]qk-i$ must be tracked through natural-number arithmetic.
Positions are 1-based natural numbers, as in the paper. and are functions read only on . is a hypothesis, IsSuffixArray: it maps injectively into and sorts the suffixes strictly in Lean's lexicographic order on lists. Since \=1ISA[i]0iDSADISA$ are integer-valued.
Pins and guards:
The space and time claims of Lemmas 2–3 and Theorem 1 ( words, time on a word RAM) are out of scope; the goal is their explicit combinatorial content. Two trivializing formalizations are ruled out: defining LF as "the cell holding ", which would make milestone 1 a tautology; and defining the phrase head by iterating LF, which would build the proof into the definition. The phrase head is the maximum of the sampled positions .
A full development needs elementary facts about lexicographic order on lists, counting over finite intervals, and iterates of LF. The suffix-array and BWT layer is reusable beyond this mission; two parallel missions on the same paper share the same core definitions. Proofs of the milestones in any order are welcome, as are alternative routes, e.g. through Lemma 14 and for the left half of the goal.
In interactive decision making, an algorithm chooses actions while learning which model governs its observations. A low-regret guarantee for one algorithm does not by itself say whether every algorithm could do better. The Decision-Estimation Coefficient (DEC) was introduced to express the cost of choosing useful decisions while distinguishing plausible models. Foster, Kakade, Qian and Rakhlin's Theorem 3.2 gives the corresponding lower bound: when a localized model class has large DEC, an adaptive algorithm must incur expected regret under at least one model in the class. This mission formalizes that result for finite decision and outcome alphabets.
The paper's protocol covers bandits, partial monitoring, and reinforcement-learning examples through a common model that maps each decision to a distribution over rewards and observations. Its lower bound concerns the protocol itself, rather than any one algorithm or application. The theorem therefore gives a common test for the limits of learning in several interactive settings. The finite-alphabet representation here retains adaptive decision kernels, which are central to the theorem.
Let be the set of decisions, the set of joint reward–observation outcomes, and the reward map. A model assigns a probability distribution on to each . Its mean reward is , and is a maximizing decision. The gap function is .
At round , an adaptive algorithm assigns a distribution on decisions using the full preceding history. It samples a decision from that distribution and receives an outcome drawn from . The joint law of the length- history is . Following equation (1) of the paper, regret sums the gaps averaged under the algorithm's chosen distribution at each round. Thus its expectation is over the history law, while the inner gap is averaged under . This formulation retains the algorithm's dependence on earlier outcomes.
For probability distributions on , write for squared Hellinger distance. For a reference model and , the DEC of a class is
The uniformly localized class contains those for which for every decision. The density-ratio bound is the supremum of event likelihood ratios over both models, decisions and events, with a lower cutoff of . It may be infinite. These conventions are equations (2), (5), and (12), and the definition immediately before Theorem 3.1 in the source.
Suppose is nonempty, every model is a probability kernel, and for every and . For , set and . The goal is the following supremum form of Theorem 3.2, equation (13):
The paper writes the result with a maximum over and a supremum over , and says that one model attains the resulting bound. Its proof explicitly permits a limit sequence when the inner supremum is not attained. The displayed statement records exactly the resulting bound on the supremum of expected regret. It implies an arbitrarily close model-specific bound for each fixed and .
The milestones follow the statements the paper's proof (App. C.1.3, pp. 90–91) uses, in attack order: the multiplicative Hellinger comparison of Lemma A.11; the difference comparison of Lemma A.12; the Hellinger bound on adaptive history laws, with ; the DEC comparison at the reference model's average play , (129); the localized gap comparison (132); and the final inequality for . Their source wording and page citations are preserved in the milestone list.
The theorem supplies a quantitative obstruction to uniformly small expected regret. It uses the same coefficient that appears in the paper's upper-bound framework, so a model class with matching upper and lower DEC estimates can have its regret scale characterized through one object. In particular, the coefficient is sensitive to the model neighborhood relevant at horizon ; replacing it by a global coefficient would lose the theorem's stated localization. The paper applies this framework to bandit and reinforcement-learning classes.
The goal and milestone declarations here are open Lean statements with checked syntax and types. A complete formalization would supply proofs of the Hellinger comparisons, the history-law inequality, and the lower bound itself. The history and density-ratio definitions are reusable for other adaptive finite-alphabet lower bounds; the published FoundationsRL mean reward, Hellinger distance and DEC definitions are reused directly.
A fixed sequence of decision distributions does not describe the theorem's algorithms: later decisions depend on outcomes produced by the unknown model. The comparison must therefore use two different laws on entire histories generated by the same adaptive kernels under two models. A bound on a single round's divergence cannot simply be multiplied by without accounting for the dependence of future decision distributions on past observations. The DEC itself involves a minimum over decision distributions and a supremum over models, which need not be attained.
The Lean representation uses finite and ; probability laws and expectations are finite vectors and sums. This is a finite-alphabet specialization of the paper's measurable-space setting. Histories are functions from round indices to decision–outcome pairs. The algorithm is a family of kernels from every possible past history to a decision distribution. Its law is the product of its decision probabilities and the model's outcome probabilities. Rounds are indexed from zero in Lean, corresponding to the paper's rounds .
Every model in and every algorithm kernel is normalized and nonnegative. The mean reward range , nonempty model class, maximizing selector, and positive horizon are explicit hypotheses. They keep the real-valued supremum and infimum in the published DEC from taking Lean's default values on empty or unbounded sets. An event with positive numerator and zero denominator has infinite likelihood ratio; remains allowed because the theorem uses . Its logarithm therefore has a finite, positive argument for . The goal uses the exact constants and . The proof's constant is printed on p. 90 as ; the formalization uses , the hypothesis of Lemma A.13 (98) from which is derived. Without it the history bound fails for two nearly equal models, and with it still holds, so the goal is unaffected. The intermediate results that select a model approaching a supremum carry an arbitrary slack , the paper's "limit sequence".
Contributions should preserve the adaptive history law and equation (1)'s decision-distribution regret. A statement restricted to predetermined decisions would leave out the central quantifier of Theorem 3.2. The published FoundationsRL definitions of , and provide the shared finite model interface; the new history and density-ratio layer can support further lower bounds in this series.
Online selection problems ask an algorithm to accept or reject elements as they arrive, while keeping the accepted set feasible. The decisions are irrevocable, and the arrival order can be chosen after the random activity of the elements is known. A guarantee for one constraint is therefore useful only if it remains meaningful when several constraints apply at once. In Feldman, Svensson and Zenklusen's paper, the constraints include matroid independence, matching, and knapsack capacity. A set satisfying two such requirements lies in the intersection of their feasible families. Theorem 1.9 establishes how their online guarantees combine: the two selectability factors multiply.
The result belongs to a sequence of statements in the paper. The authors first define greedy online contention resolution schemes and their selectability guarantee in Definitions 1.3–1.5. They then state the combination theorem in the introduction and identify the intersection construction in Definition 2.10. Lemma 2.11 supplies the precise selectability assertion for that construction. This mission isolates those claims so that later formalizations of specific constraints can reuse them without repeating the probability argument.
Let be a finite ground set and a family of feasible sets. A fractional point determines a random active set : each belongs to independently with probability . Thus a particular set has weight
A greedy online contention resolution scheme, or greedy OCRS, chooses a down-closed family . As active elements arrive, it accepts an element when adding that element to those already accepted remains in . In a randomized scheme, the choice of is random and independent of . The family contains the empty set, as the procedure begins with no accepted elements.
An element is selectable for a realized active set and family if every with still permits : . This condition covers every possible set that might have been accepted before arrives. A greedy OCRS is -selectable for a relaxation when the probability of this event is at least for every and every . The probability includes both draws when the family is randomized. Here and .
For two feasible families , the combination of their greedy OCRSs independently draws and , then uses . This is a family of sets satisfying both constraints. The proof also uses , the indicator that for every lying in . For selectability itself, .
For , let the first scheme be -selectable and the second -selectable. The mission asks for a greedy OCRS on the intersection with
The target records existence of the combined scheme, independent of a particular proof of its selectability. The paper also claims preservation of polynomial-time efficiency; the finite mathematical model here does not assign a complexity measure to a family sampler or membership oracle, so that clause is outside this target.
The lemma names the combined scheme: independently draw both greedy families and use their intersection. It asserts the same bound for that specific scheme. The earlier milestones record the two order properties of and the finite product-measure correlation inequality appearing in the lemma's proof. Their statements keep the original quantifiers over active sets and families visible.
The theorem turns guarantees for individual constraints into a guarantee for simultaneous constraints. If a matroid scheme and a matching scheme meet the same scale parameter , their intersection is governed by the product of their selectability factors. The factor loss is explicit, which lets subsequent algorithmic results track it without redefining the combined scheme. The lemma additionally fixes the actual distribution over intersected families, avoiding ambiguity about how two randomized procedures are coupled.
Mathlib already provides a general finite FKG inequality, but it does not state the paper's OCRS objects, the selectable event, or the intersection theorem. This mission adds those interfaces and the specialized correlation statement. The source results are proved in the cited paper; the local theorem files in this proposal are statements for later machine-checked proofs. A complete formalization would connect the finite active-set weights to Mathlib's lattice correlation theorem and then establish the randomized family bookkeeping. The finite probability definitions can also serve other OCRS results in the same paper.
The obvious argument would multiply the two probabilities that is selectable for the separate families. Both events depend on the same active set , so they are not independent even when the families are drawn independently. Moreover, selectability for the intersection checks only sets belonging to both families, whereas the original bounds check each family separately. The formal statements must keep these two dependencies distinct. The paper's two monotonicity claims and its FKG display identify the needed intermediate assertions, but their use with an arbitrary random choice of families still requires careful finite-sum reasoning.
The ground set is a finite Lean type and subsets are Finsets. Feasibility is a predicate on those finite sets. Fractional points are real-valued functions, and each input relaxation is represented as a set of such functions with an explicit coordinate bound . The scale and selectability parameters belong to . The point ranges over , not over an independently chosen intersection of scaled sets, so the case retains the paper's meaning. The finite products define the law of ; no measure-theoretic integral is used.
A randomized scheme is a probability weight on possible greedy families for every input point. The combined weight is the product of the two original weights summed over pairs with the required intersection, expressing independent draws. The family distribution is independent of the active-set draw. This sampling convention is necessary for the stated product guarantee and is made explicit here although Definition 2.10 does not spell it out. Each greedy family contains and lies in its own feasible family. These requirements exclude the empty-family and unconstrained-family encodings that would make selectability trivial. The unit-cube bounds prevent negative active-set weights.
The Lean declarations focus on the finite selectability guarantee. They abstract a polytope by its set of fractional points and use the paper's unit-cube condition; they do not formalize a polyhedral representation or test that its binary points equal the feasible sets. A full development of the paper's algorithmic setting would additionally represent online arrival orders, family sampling algorithms, membership oracles, and polynomial running time. Contributions establishing the finite probability lemmas, the specialized FKG statement, and Lemma 2.11 are directly useful here. The general active-set and selectability definitions are reusable across the paper's other missions.
Hypergraph Turán problems ask how many edges a -uniform hypergraph on vertices can have without containing a fixed sub-hypergraph. For graphs () the theory is well developed; for exact answers are rare and are known mostly for small, dense configurations such as the Fano plane or expanded triangles. Paths are the natural sparse test case. For graphs, Erdős and Gallai (1959) showed that a graph on vertices without a path of length has at most edges. For hypergraphs there are several notions of path: Berge paths (Győri, Katona and Lemons, 2010), loose paths (Mubayi and Verstraëte, 2007, asymptotic bounds) and the most restrictive notion, linear paths. The case of two edges was solved by Frankl (1977), and the case asymptotically by Frankl and Füredi (1987).
Füredi, Jiang and Seiver (arXiv:1108.1247v1, published in Combinatorica 34 (2014), doi:10.1007/s00493-014-2838-4) determined the Turán number of every -uniform linear path exactly, for and large, together with the unique extremal families. It is one of the few exact hypergraph Turán results for an infinite family of forbidden hypergraphs.
The vertex set is . A family is a set of subsets of ; it is -uniform if , the set of all -element subsets.
A linear path of length is a sequence of distinct sets such that
The -uniform linear path of length is written ; a family contains it if some of its members form a linear path. The Turán number is the maximum size of a -uniform family on that does not contain .
Two counting functions describe the answer:
For a set of elements, is the number of -sets meeting (the star family of ), and adds the -sets of that contain two fixed vertices (the even family).
The proof is phrased in the language of the delta-system method: -stars (sets pairwise meeting in a common kernel), the kernel degree (the largest for which an -star with kernel exists), -homogeneous families (k-partite families whose intersections follow a single intersection-closed pattern of subsets of , each intersection being the kernel of an -star), the rank of , the kernel graph of , and the -blowup of a graph .
For every and there is such that for all :
and in each case a -uniform, path-free family of that size is exactly the star family of some -set (odd case), respectively the even family of some -set and two distinct vertices (even case).
In the order the proof uses them:
The theorem gives the exact extremal number and the unique extremal configuration for every linear path when , and its proof yields a stability statement (Theorem 5.1 of the paper): a path-free family of nearly extremal size is close to a star family. The method is the standard template for exact results on sparse hypergraphs: delta-system decomposition, an asymptotic bound from a graph theorem applied to a kernel graph, then stability and cleaning.
The result is proved in the paper. As far as the platform's catalog shows, none of it is formalized: Mathlib has the intersecting Erdős–Ko–Rado theorem () but not the -intersecting version with uniqueness for large , not Erdős' matching theorem, not the Erdős–Gallai circumference theorem, and no delta-system machinery. A formalization would produce reusable libraries for each of these, and the first machine-checked exact hypergraph Turán number for an infinite family.
The obvious argument — bound the number of members through each vertex and sum — gives only with a wrong leading constant, because a path-free family can have vertices of almost full degree. Exactness needs three layers that do not reduce to one another. First, the intersection semilattice lemma (Lemma 3.1) is a deep structural theorem with a doubly exponential constant; it is cited, not proved, in the paper. Second, the asymptotic bound passes through the Erdős–Gallai circumference theorem, itself a nontrivial graph result. Third, the exact value requires a stability argument with several error terms (, ) that must be balanced, followed by Erdős' matching theorem and the 2-intersecting Erdős–Ko–Rado theorem for large , both with uniqueness. The structural lemmas of §§3–4 are elementary but involve greedy embeddings in which disjointness of the new vertices has to be maintained carefully.
Vertices are Fin n; families are Finset (Finset (Fin n)); -uniformity is 𝓕 ⊆ univ.powersetCard k. A linear path is an injective map Fin ℓ → Finset (Fin n) into the family with consecutive members meeting in exactly one vertex and non-consecutive members disjoint. The Turán number is a Finset.sup of cardinalities over all path-free -uniform subfamilies, a finite attained maximum for ; at the feasible set is empty and Lean returns zero, which no theorem here uses. Partitions into parts are part maps Fin n → Fin k; stars are finsets of distinct petals; the rank is a minimum computed with sInf, exact because intersection patterns consist of proper subsets of . "Sufficiently large " and every are explicit existential constants chosen before and the family.
Hypotheses added relative to the page: Theorem 3.8 assumes the homogeneous family is nonempty (the empty family is homogeneous for every pattern, and the proof starts from a member). Lemma 4.2 states , implicit in the paper's definition of a blowup using new vertices; it excludes a false zero-threshold case at . Lemma 4.3 is stated for an arbitrary choice of a vertex in each member, a generalization of the printed lemma, whose proof uses only . Bound (1) is posed for . Claims 2–3 are stated stand-alone with the -set existentially quantified.
Trivializing formalizations are ruled out: the goal asserts the value and the uniqueness of the extremal family, the Turán number is a true maximum rather than a junk supremum, the linear path requires intersections of size exactly one and disjointness of non-consecutive members, and all constants are quantified before .
Needed infrastructure: the delta-system method (Lemma 3.1), Erdős–Gallai for circumference, Erdős' matching theorem and -intersecting Erdős–Ko–Rado for large . Each is reusable well beyond this mission, and contributions of any of them are welcome.
Quantum information often describes a system through a state shared among many small registers. One would like to replace the state on a few registers by a product of their individual states, because product states are easier to estimate and optimize over. The usual finite quantum de Finetti theorems obtain such approximations from permutation symmetry. A physical preparation, however, need not be symmetric. Berta, Borderi, Fawzi and Scholz give a quantitative statement that instead selects the retained registers at random and conditions on measurements of other registers. Their Theorem 2.5 is the target here.
The authors place this result alongside their hierarchy for constrained bilinear optimization, but the theorem without symmetry is independent of the hierarchy. In §2.6 they compare its polynomial dependence on the local dimension and the number of retained registers with the earlier no-symmetry approximation discussed in their reference [12]. The result identifies exactly what random selection and measurement can supply when a global permutation-invariance hypothesis is unavailable.
Let be a quantum system of dimension , and let be an arbitrary density operator on copies of . Choose a uniformly random permutation of these copies. Its first positions form an ordered tuple of systems to retain; the remaining positions form an ordered tuple available for measurement. There is no symmetry condition on .
A measurement on has finitely many outcomes and positive operators whose sum is the identity. Measure the first systems , where , and condition the retained state on the observed outcomes. Write for that conditional state and for its marginal on the th retained system. The trace norm measures the error between and . The expectation is over the uniform permutation and the measurement outcomes, with their Born-rule probabilities.
The distortion with side information of a fixed measurement is the largest ratio between an input trace norm and the norm left after measuring only its factor. The input ranges over Hermitian operators on , over every finite-dimensional side system , with zero partial trace on both and . The paper's is the infimum of this distortion over all measurements on equation (10). A state two-design is a finite family of rank-one projectors whose average second tensor power is the projector onto the symmetric subspace with the normalization in Lemma D.1. The projectors give an explicit measurement with distortion at most .
The principal target is the explicit form of Theorem 2.5. For , put . With the two-design measurement, some satisfies
Here the in the expectation is the outcome string for the first members of . The same is chosen before taking that expectation. This rate is stated with its constants and its two consecutive inequalities; an existence assertion without the error bound would lose the theorem's content.
The milestone path also states the telescoping trace-norm inequality of equation (12), the measurement estimate of Lemma D.1, and the final averaged inequality on p. 11. A companion milestone treats any fixed POVM with its own distortion. That formulation captures the proof's arbitrary-measurement step without treating the infimum as if every measurement attained it.
For an arbitrary multipartite state, random ordering and conditioning give one measured prefix length at which the selected registers have small expected distance from a product. The explicit rate is polynomial in and and decays as . It therefore gives a quantitative approximation guarantee under a selection rule that can be applied without first establishing exchangeability Berta et al., §2.6.
The theorem is proved in the paper; the work here is to express its state, measurement, conditional distribution, and norm bound in Lean and to connect the estimate to reusable finite-dimensional quantum-information definitions. The local statements are currently proof obligations, not machine-checked proofs. The published density-operator, trace-norm, and partial-trace definitions are reused. Once proved, the statements can serve as a precise interface for subsequent formal work on randomized subsystem selection and information-theoretic decoupling.
Randomly choosing systems does not turn the original state into a product state. A direct bound on the distance to a product can be large even when each one-system marginal is simple, because correlations among the retained systems remain. Equation (12) breaks the total error into successive correlation terms; the paper controls their average by measuring other systems and using information-theoretic estimates. A second difficulty is that a measurement can erase distinctions between different input operators. The two-design estimate supplies a dimension-dependent bound on that loss, uniformly over the size of a side system.
The printed theorem leaves the measurement unspecified while using the minimum distortion over all measurements. A trivial measurement cannot satisfy that reading. The proof explicitly permits the measurement built from a state two-design, with replacing ; that is the measurement used in the goal proof of Theorem 2.5, p. 10.
The system has basis Fin dB; copies have basis Fin n → Fin dB. The formalization writes , assumes , and ranges over . A state is a positive semidefinite complex matrix with trace one. Permutations act on the copy coordinates, and their finite uniform average models the paper's random ordered tuples. Measurement outcomes are finite words; the conditional state divides the unnormalized post-measurement state by its probability. A zero-probability outcome uses Lean's zero inverse and contributes zero to the weighted expectation. The existence of a state and of a nonempty two-design rules out zero-dimensional and empty-outcome instances in the goal.
The fixed-measurement distortion and take values in extended nonnegative reals, so a measurement that destroys a nonzero operator has infinite distortion. The logarithm is base two except for . The definitions use the paper's unnormalized trace norm, with no factor . No mutual-information estimate or Pinsker inequality is assumed in the goal: both belong to possible proofs. Contributions proving the stated milestones, the positivity and normalization of the conditional states, or reusable trace-norm facts for finite tensor products all advance the target.
Large network games can be described by a graphon, a measurable kernel that assigns an interaction weight to each pair of players in a continuum. This representation is useful when a finite network is viewed as an approximation to a limiting network. A basic question is whether a small change in interaction weights can cause a large change in equilibrium behavior. Carmona, Cooney, Graves, and Laurière answer this question for a static game with real actions, noisy player states, and costs coupled through an aggregate state. Their static graphon games paper establishes existence and uniqueness under different hypotheses, and Theorem 3.20 gives an explicit stability estimate under its contraction condition.
The mission isolates that stability estimate and the results on which it depends. It belongs to the same development as the paper's existence theorem, but has a narrower question: how sensitively does the equilibrium respond when one graphon is replaced by another? The paper later studies finite-player approximations, for which understanding the limiting graphon game's equilibrium is useful. Those later approximation theorems are outside this mission.
The player set is with Lebesgue probability measure. Every player chooses a real action. A strategy profile assigns an action to almost every player and belongs to . Profiles that differ only on a null set represent the same strategy.
A graphon is a symmetric, real-valued, measurable, square-integrable function on . It defines an integral operator on by
Its norm is the -to- operator norm. In particular, interaction weights are allowed to be negative and are not restricted to . A second graphon has operator , and is the operator norm of their difference.
A player's state is , where is the player's action, is an aggregate state, and has a common centered probability law with finite second moment. Assumption 1 bounds squared changes in by times the squared action change plus times the squared aggregate change. For a profile , its aggregate is the solution of
Proposition 3.1 states that this aggregate exists and is unique when . This equation is the deterministic aggregate obtained from the paper's continuum model.
The expected cost of action at aggregate is . Assumption 4 says that is continuously differentiable and uniformly -strongly convex, and its action derivative changes at most when the aggregate changes. The best response minimizes this cost pointwise. A Nash equilibrium is an profile whose action minimizes for almost every player. Assumption 5 adds the uniform bound .
The first targets are the unique aggregate of Proposition 3.1, the best-response bound of Lemma 3.7, and the aggregate bound (15) of Lemma 3.16. Together these support the uniqueness condition in Proposition 3.17:
Lemma 3.19 then bounds the change of aggregate when the same profile is placed in two graphons. The goal, Theorem 3.20, concerns an equilibrium for and any equilibrium for :
Here satisfies both and (17), while is required only to satisfy . The displayed coefficient is the paper's expression, including its common factor.
The theorem gives a quantitative guarantee: as long as the original game's contraction condition holds, the distance between equilibria is controlled by the operator distance between graphons. The bound identifies how state sensitivity , cost sensitivity , strong convexity , and the state bound enter that guarantee. The result also separates two questions: whether an equilibrium exists for a changed graphon, and how far any such equilibrium can lie from the original one.
The mathematical theorem is proved in the paper; the Lean goal is open. A complete formal development would establish the integral-operator estimates, the aggregate and best-response regularity results, the unique equilibrium under (17), and finally the stability inequality. The definitions of real-valued graphons, aggregates, and their extended-valued operator norm can support later work on graphon games beyond this particular estimate. The paper's §4 finite-player results, including Theorems 4.3, 4.7, and 4.9, are not posed here.
An equilibrium is a fixed point of a response to an aggregate, so changing the graphon changes both the aggregate and the equilibrium profile. A direct comparison of costs at two equilibria does not by itself separate these effects or yield the printed constant. The aggregate is defined only as an equivalence class, while its equation and pointwise best responses use representatives. The formalization must keep those almost-everywhere statements aligned with the operator norm estimate. It must also retain the paper's asymmetric hypotheses: (17) is assumed for the original graphon, while the second graphon is allowed to have any Nash equilibrium under its own aggregate condition.
Lean uses unitInterval with its volume measure for , real actions, functions with MemLp for profiles, and almost-everywhere equality for profiles and aggregates. IsGraphon includes measurability, symmetry, and square integrability. IsAggregate records equation (6) and membership in . The integral cost is computed from , , and rather than supplied as an unrelated function. Assumptions 1, 4, and 5 are explicit; the centered noise law is part of the standing model. Lemma 3.7 is stated for an arbitrary cost satisfying Assumption 4, as on the page.
The paper defines equilibrium through a best-response map on a rich Fubini extension. Proposition 3.6 identifies that with the almost-everywhere pointwise minimization condition under Assumption 4. The mission uses that equivalent condition as its equilibrium predicate. This is a disclosed model choice because the Fubini extension itself is not formalized. A best response is selected by classical choice; Assumption 4 gives the minimizer that makes the selection meaningful.
Norm inequalities use extended nonnegative reals. For a square-integrable graphon, its operator norm is finite, and real hypotheses use that finite value. The operator norm is never a real supremum with a default value for unbounded inputs; an equilibrium always includes an aggregate; and an infinite left-side norm is never converted to zero. These choices prevent the stability claim from becoming empty at a bad input. Contributions to the integral-operator infrastructure, the existence and uniqueness of aggregates, and the five named milestones are all within scope.
First order primal–dual algorithms are used when a linear program is too large for a direct factorization or when matrix operations are cheaper than solving a sequence of linear systems. Their basic guarantees often bound an averaged duality gap by a quantity proportional to after steps. A restart discards the current inner iteration history and begins again from an averaged output. For problems with a suitable error bound, restarts can turn sublinear progress into geometric decrease in distance to the solution set. Applegate, Hinder, Lu and Lubin analyze this mechanism for a class that includes proximal point, extragradient, primal–dual hybrid gradient and ADMM methods, with constants listed in their Table 1. Their adaptive rule is useful when the sharpness constant is unavailable to the algorithm designer. Applegate et al., arXiv:2105.12715v4, §§2–4
Let and be closed convex sets. The primal–dual problem is , where is differentiable, convex in and concave in . A point is feasible when . Its saddle-point set contains the feasible pairs satisfying for every and . Distances and balls use a chosen seminorm ; this matters for methods whose natural geometry is degenerate. Applegate et al., arXiv:2105.12715v4, pp. 2–3
For , put . The normalized duality gap is . At it is the upper limit as positive radii decrease to zero. The gap can be infinite under a seminorm, so its values are extended real. A problem is -sharp on when for every and every . This condition connects a computable local gap to the distance of interest. Applegate et al., arXiv:2105.12715v4, pp. 3, 11, (4), Definition 1
The base algorithm begins at and supplies averaged outputs for positive inner times . Property 3 requires constants , uniform over every feasible start and output run, for which , , and . An outer run starts at , runs its inner algorithm for steps, and sets . Its first length is selected by the user. At later outer indices, it restarts at the first positive time when the normalized gap has fallen below times the gap at the previous outer transition, with . Applegate et al., arXiv:2105.12715v4, pp. 9–10, 15–16, Property 3, Algorithm 1, (30)
The goal is both parts of Theorem 2. Assume all outer starts lie in one set on which the problem is -sharp, with . Define the ceiling time . For every the target is
The milestones are Proposition 8's treatment of zero displacement, the displayed restart comparison in the proof of (33), the bound (33) itself, and the repeated normalized-gap inequality in the proof of part (ii). Each is tied to the arXiv version's printed page and label. The assertion begins at : the first interval is free and need not be at most . Applegate et al., arXiv:2105.12715v4, pp. 17–18
The first conclusion gives a uniform bound on the inner work of every subsequent adaptive interval. The second translates the gap-based restart rule into a geometric distance guarantee while retaining the user-selected first interval as a visible factor. Together, they explain why an algorithm that does not know can have the same characteristic restart scale as one using a fixed frequency chosen from . The paper proves this theorem and gives linear-programming settings in which its sharpness premise holds; this mission asks for a machine-checked statement and, eventually, a machine-checked proof of that known result. Applegate et al., arXiv:2105.12715v4, Theorems 1–2 and Lemma 5
Formalizing the result also produces reusable interfaces for saddle sets, seminorm distances, localized duality gaps, uniform algorithm properties, and first-trigger restart runs. Those interfaces can support other primal–dual analyses without committing to a particular inner update map. A complete proof can later connect Property 3 to the paper's individual algorithms, while this mission preserves the abstract theorem that they share. Applegate et al., arXiv:2105.12715v4, Proposition 4 and §4
The restart test uses a gap evaluated at the moving radius , whereas sharpness relates a gap at the radius of the previous outer transition to distance from . This mismatch must be reconciled while preserving the exact ceiling constant. A zero seminorm displacement is a separate boundary case: sharpness only speaks about positive radii, but the algorithm can still encounter radius zero. The theorem also needs the first qualifying time; knowing merely that a later time satisfies the test gives no upper bound on the interval length. Applegate et al., arXiv:2105.12715v4, pp. 16–18
Lean represents and by finite-dimensional Euclidean spaces and by their product, allowing either dimension to be zero. The geometry on that product is an explicit Seminorm, never the product type's default norm. is the set of saddle pairs. The standing problem predicate includes closed convex feasible sets, separate convexity and concavity, and differentiability on the whole ambient product space. It also requires , a disclosed strengthening of the paper's standing feasibility and finite-optimum assumptions so the real-valued distance to cannot collapse to an empty-infimum default. The infimum defining distance is over saddle points only; the supremum defining the gap is over feasible pairs only. The normalized gap and diameter use extended reals so an unbounded seminorm ball does not silently acquire value zero. Applegate et al., arXiv:2105.12715v4, pp. 2–4
The base method is a relation from a start to possible averaged-output sequences. Property 3 fixes before quantifying over starts, runs and positive times. The theorem assumes initial feasibility; Property 3 then makes restarted outer points feasible. An adaptive run records the positive first interval and the first qualifying positive time for each later interval. The ceiling is Nat.ceil; the factor is division in the reals. A formalization with arbitrarily chosen qualifying restart times, sharpness only along one chosen trajectory, a real-valued supremum over an unbounded ball, or a vacuous solution set would change the result. Contributions to the gap and seminorm infrastructure and to either half of Theorem 2 are useful; the individual algorithm implementations are outside this mission's core. Applegate et al., arXiv:2105.12715v4, pp. 9–10, 16–18
Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571, ICLR 2018) train classifiers against adversarial perturbations by solving a Lagrangian relaxation of a Wasserstein distributionally robust problem. The inner problem, , is strongly concave, and hence solvable by gradient ascent with the paper's certificates, exactly when the penalty exceeds the input-smoothness constant of the loss: the Lipschitz constant of . For a deep network this constant is not given; §4 of the paper ("Bounds on smoothness of neural networks") supplies an explicit upper bound in terms of the weights' spectral norms and per-layer constants of the activations. The bound tells a practitioner how large must be for the robustness guarantees to apply, and it is of the same type as the spectral-norm Lipschitz bounds used for adversarial robustness and generalization of deep networks (Szegedy et al. 2014; Bartlett, Foster, Telgarsky 2017), but at the level of the derivative rather than the function.
A layered network of depth has widths (pre-activation of layer ) and (output of layer ), with the input dimension and the number of classes. Its parameters are weight matrices , and each linear layer is followed by a nonlinear operation (an activation, possibly combined with pooling). The output of the first layers is
and its Jacobian in is . All spaces carry the Euclidean norm , and is the -operator (spectral) norm.
Assumption E. For , the map is -Lipschitz for , its Jacobian is -Lipschitz from to , and . From these constants define
The classification loss is the softmax loss with , for a class .
Under Assumption E, for every class and all inputs ,
Under Assumption E, for ,
In the order the paper's proof uses them: Lemma 6 (the chain rule for , recursively and as a product); Proposition 5, first part; the telescoping representation (34) of ; Proposition 5, second part; the softmax constants of §B.9 (gradient , Lipschitz constant , smoothness constant ); and the recursion of §B.9 for with its instance for a softmax output layer.
Corollary 4 converts the abstract hypothesis of the paper's convergence and certification results (missions 1 and 2 of this series) into a checkable condition on a trained network: , computable from spectral norms of the weights and from constants of standard activations (the paper lists average pooling, sigmoid and ELU). Proposition 5 is a reusable statement about any composition of smooth maps with linear layers, independent of the softmax and of robust optimization.
The results are proved in the paper (§B.8–§B.9). No machine-checked proof of them is known to exist. This mission produces a formal development of the input Jacobian of a layered network with varying widths, the telescoping estimate for its variation, and the smoothness constants of the softmax loss, all with the paper's explicit constants.
The function-level bound (first part of Proposition 5) is a direct induction. The derivative-level bound is not: the obvious induction on needs both a bound on , which comes from the Lipschitz half and the differentiability of every layer, and a bound on the variation of the Jacobian of the previous layers, and the two must be combined so that the constant comes out as exactly of (21), whose definition uses quotients by . For the corollary, the softmax loss must be shown to have Lipschitz constant (a supremum that is not attained) and a -Lipschitz derivative; the paper's eigenvalue argument for the latter is loose and its displayed initial condition for the recursion of the constants is misprinted, so the printed text cannot be transcribed line by line. In Lean, the widths change from layer to layer, so the network is a family of maps between different Euclidean spaces, and every product of Jacobians is a dependently typed composition.
EuclideanSpace ℝ (Fin n); weights are continuous linear maps, so ‖θ l‖ is the spectral norm; Jacobians are Fréchet derivatives with the operator norm. A Frobenius or entrywise norm would state a different theorem and is not used.l is the paper's layer (θ l, σ l, L0 l, L1 l); F l, α L0 l, β L0 L1 l carry the paper's index . Widths vary with the layer; they are not collapsed to a single dimension.Fin K; the goal uses Mathlib's gradient, whose norm equals the operator norm of the derivative.A complete development needs the chain rule for the network map, the mean value inequality for the softmax loss, and the algebra of (21). The definitions of the layered network and of the softmax loss are independent of robust optimization and are reusable for other Lipschitz and smoothness bounds of deep networks. Proofs of any milestone, and alternative arguments with sharper constants stated as separate theorems, are welcome.
An inventory policy chooses how much stock to order before demand is observed. Its quality is assessed by the holding and backlogging costs it incurs on future demand. A policy chosen to perform well on historical demand can overfit those observations. A useful statistical guarantee therefore controls the difference between historical and future costs simultaneously over the policies that the procedure may select. Xie, Ma and Xin establish such guarantees for stationary base-stock, , and nonstationary base-stock policy classes.
This formalization covers the principal bound families in that paper. Its first goal is the expected generalization and estimation bound for nonstationary base-stock policies with no fixed ordering cost, Corollary 4.10. Its supporting targets include Theorem 4.9 and the constructive product-sample partition in Lemma 4.12. The other principal bounds remain in the explicit scope below and await their own full Lean declarations. The companion inventory-information project needs these results as proved dependencies; merely citing the paper does not close that project's formal proof obligations.
There are periods, a deterministic lead time , and demand bounded by . The first order arrives in period . Average loss means the sum of holding and backlogging costs in periods , divided by the positive horizon . The initial pipeline is empty, and initial inventory is nonpositive for the base-stock models. Holding and backlogging cost coefficients are . Nonstationary base-stock policies in the first goal have no fixed ordering cost and use levels .
The Lean model indexes the first period by zero. It uses the source's explicit finite-maximum formula for post-replenishment inventory, with the demand interval summed up to, but excluding, the observation period. In mathematical notation the inventory in period is . Cost is evaluated after subtracting the current demand . This is a backlog model; applications to lost sales require a separate equivalence argument.
Data comprise IID demand trajectories from a probability measure on the bounded trajectory space. Different periods of the same trajectory can be dependent. Generalization error is the one-sided supremum , where is expected average loss and is empirical average loss. Estimation error is , for an empirical minimizer and a best-in-class population policy. It is not the error relative to every history-dependent inventory policy. These conventions follow Sections 3 and 4.
The first goal, Corollary 4.10, asserts the existence of one absolute constant such that
The constant is quantified before the horizon, lead time, support, costs, demand distribution, sample size, and policy selections. The first inequality explicitly refers to actual minimizers, with an integrable selected risk. The GE conclusion holds independently of whether a particular selector has been supplied.
Its principal complexity target is Theorem 4.9: for each relevant period and , the normalized inventory class has fat-shattering dimension at most . The Lean statement says directly that every -shattered indexed sample has cardinality at most that number. It uses the source convention of a strict upper label and non-strict lower label.
Lemma 4.12 partitions all product indices into groups of indices. Every coordinate of every group traverses the original row indices exactly once. The formal statement uses a bijection between anchor-offset pairs and complete index tuples, together with a coordinate-permutation assertion. The dimension is positive, and and are included.
The full scope also retains Theorem 4.1 and Corollary 4.2 (stationary policies), Theorem 4.4 and Corollary 4.5 ( upper bounds), Theorem 4.7 and Corollary 4.8 ( fat-shattering and GE lower bounds), and the expected Product ERM comparison in equation (4.7). They are catalogued with their assumptions but are not yet all encoded. The GE lower bound is not asserted to be a minimax policy-regret lower bound.
The nonstationary policy vector grows with the horizon, while the expected average-loss bound has no horizon factor. A verified version supplies a reusable statistical ingredient for finite-horizon inventory learning. Total-cost bounds require multiplication by the horizon. Absolute uniform deviation, period-dependent costs, high-probability statements, initial-state reductions, and censoring require further bridge theorems. They are not attributed to Corollary 4.10 without those proofs.
The cyclic partition has a complete locally checked Lean proof with axiom dependencies only propext and Quot.sound. The two statistical targets remain open. Neither a drafted declaration nor a local proof is described as a server-verified contribution.
Ordinary pseudodimension can grow with the horizon for the nonstationary class, so it does not by itself give the desired horizon-free rate. A full proof needs scale-sensitive complexity, probability, and integration infrastructure. For Product ERM, coordinate independence must be explicit: the groups in the partition need not be independent of each other. The expected comparison transfers upper bounds; it cannot reverse direction to transfer a GE lower bound.
The shared environment is Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Demand and policy coordinates are bounded real subtypes with their usual measurable structures. Probability is over IID whole trajectories. Finite maximum indices are nonempty. Positive prevent zero denominators in the targets. General definitions remain total, and their behavior outside these hypotheses is exposed in the independent read-backs.
Complete proofs must establish the boundedness and measurability needed for the real suprema and integrals to have their usual meaning. They may not assume the convergence bound, replace arbitrary probability measures by finite-support distributions, or silently restrict the policy class. The branch additionally needs explicit unbounded-domain conventions when holding or backlogging costs vanish. Reusable contributions include shattering, symmetrization, entropy bounds, selection and integrability facts, and finite-product sampling.
Large data sets make clustering and subspace fitting expensive because a candidate solution must be evaluated against every input point. A dimensionality reduction replaces the data by a lower-rank matrix whose costs approximate those of the original input for an entire class of candidate solutions. Feldman, Schmidt, and Sohler study reductions that retain enough information for -means, principal component analysis, and projective clustering. Their journal paper identifies a rank truncation and one residual scalar that preserve the fitting cost of every shape lying in a low-dimensional linear subspace Feldman, Schmidt, and Sohler (2020), Theorem 22.
The published article also records that some coreset sizes in its 2013 conference version were incorrect. This mission uses the 2020 journal statement and its page numbering throughout. The authors cite earlier SVD-based approximations to -means on p. 613, while their Theorem 22 gives a uniform cost guarantee for arbitrary nonempty shapes contained in a -dimensional subspace Feldman, Schmidt, and Sohler (2020), pp. 603, 613, 620.
The input is a real matrix . Its rows are points in . For a nonempty set of candidate locations or shapes , let be the infimum of Euclidean distances from row to points of . The shape cost is
The set need not be closed and need not be a subspace. For example, it can be a finite set of cluster centers. The restriction is that all of its points lie in some linear subspace of dimension . This matches the paper's shape class in §5; the affine case is treated separately Feldman, Schmidt, and Sohler (2020), pp. 619–620.
Fix a singular value decomposition , where and are orthogonal and the diagonal entries of the rectangular matrix are nonnegative and nonincreasing. The entry is indexed from one. The rank- truncation keeps the first diagonal entries and sets the rest to zero. Its squared Frobenius residual is . The corrected cost of is Feldman, Schmidt, and Sohler (2020), Definition 1 and §2.
The milestones first record the matrix Pythagorean identity, the projection and residual bounds, and the lower bound on the cost of a linear -subspace. They then state the residual-corrected approximation in Corollary 16:
Here has orthonormal columns spanning the complement of the candidate subspace. Corollary 20, Corollary 21, and display (9) connect these linear estimates to costs of general sets Feldman, Schmidt, and Sohler (2020), pp. 604, 613–615, 619–620.
The goal is Theorem 22. For , , and , every nonempty contained in a linear -dimensional subspace satisfies
The quantifier over makes this a guarantee for every admissible candidate on the same reduced data, rather than a statement about one selected optimum Feldman, Schmidt, and Sohler (2020), Theorem 22, p. 620.
The theorem preserves objective values after replacing by a rank- matrix and one number. For a fixed and accuracy parameter, the rank threshold depends on and , with no direct dependence on the number of points or ambient dimension except the upper bound on feasible . In the paper, the result leads to a guarantee for -means candidates, since centers span a linear subspace of dimension at most Feldman, Schmidt, and Sohler (2020), Corollary 23, p. 621.
The result is proved in the paper, but this mission's Lean theorems are posed with sorry; they do not yet have machine-checked proofs. A completed development would connect a reusable rectangular SVD model, matrix projection identities, infimum distances to arbitrary nonempty sets, and a uniform cost inequality. The SVD definition is already published in the platform library; the row-cost and singular-value conventions here supply the interface needed for this paper Feldman, Schmidt, and Sohler (2020), §§2, 3, 5.
The linear subspace bound compares a projection cost with a tail sum of squared singular values. The paper recalls that fact in §3 without proving it, so the formal development needs a suitable singular-value inequality or a derivation from existing matrix approximation results. For general shapes , a bound on the cost of one linear subspace does not by itself control the distance from each projected point to every point of . The remaining milestones state the projection error, the squared-distance perturbation bound, and the Pythagorean cost split that address that gap Feldman, Schmidt, and Sohler (2020), pp. 613, 619–621.
The proof printed after Theorem 22 invokes earlier corollaries under a stronger rank threshold than the theorem states. The mission keeps the printed theorem threshold, whose claim remains valid; a formal proof must bridge that discrepancy Feldman, Schmidt, and Sohler (2020), pp. 620–621.
Matrices are Matrix (Fin n) (Fin d) ℝ, and rows are points of EuclideanSpace ℝ (Fin d). Squared Frobenius norm is an explicit finite sum of squared entries. Shape cost sums squared Metric.infDist values over rows. Since Mathlib assigns a real default value to distance from the empty set while the paper assigns infinity, every theorem about a general shape requires C.Nonempty. This is the page's own requirement for Theorem 22 and Corollary 21, and is also needed for display (9).
The SVD and its truncation use the published ProjLikeRetr.FixedRank.IsSVD and truncSVD. Every SVD statement quantifies over an arbitrary valid triple ; tied singular values do not fix a unique truncation. The local is one-based, while truncSVD m keeps zero-based diagonal positions below . Orthonormal columns of satisfy , their orthogonal complement has columns, and projection in ambient coordinates is . Theorem 22 quantifies over arbitrary nonempty contained in a linear -subspace; it does not restrict to subspaces or replace linear containment by affine containment.
The integer inequalities in Lean use additive forms such as to avoid truncated natural-number subtraction. The theorem retains the printed threshold, including the proof gap described above. Running-time clauses are outside the mission's mathematical statements. Contributions are welcome toward the singular-value lower bound, the projection and infimum-distance identities, and the final uniform inequality; the matrix and distance definitions are reusable in the companion affine-subspace mission.
Many problems in quantum information theory ask for the maximum of a linear functional over pairs of quantum states, one on each of two systems, subject to linear constraints on each state. The best success probability of an approximate quantum error-correcting code of given size is of this form: the encoder and the decoder are quantum channels, their Choi matrices are states with fixed marginals, and the objective is bilinear in the two (Berta, Borderi, Fawzi & Scholz, arXiv:1810.12197, §4). Such constrained bilinear programs are nonconvex. Seesaw methods give lower bounds that often converge in practice, but they offer no guarantee of global optimality. What is needed is a hierarchy of efficiently computable outer bounds that converges to the optimum, with an explicit rate.
For the unconstrained problem, the optimisation over separable states, such a hierarchy is classical: the Doherty–Parrilo–Spedalieri hierarchy of -extendible states, whose convergence follows from finite quantum de Finetti theorems (Christandl, König, Mitchison & Renner 2007; Brandão & Harrow 2013). The standard de Finetti approximant is, however, a mixture of product states that need not satisfy the linear constraints, so it says nothing about the constrained problem. The paper proves a de Finetti theorem with linear constraints (Theorem 2.3) and derives from it a semidefinite hierarchy for constrained bilinear programs with a convergence guarantee (Theorem 3.1).
A -dimensional quantum system has operator space ; a state is a positive semidefinite with . Let and be systems of dimensions and . The data are an objective , arbitrary linear maps and , and matrices , . The constrained bilinear program is
For let be copies of . A state on is symmetric with respect to if it is invariant under every permutation of the copies , . Write , and . The level- program is
It is a semidefinite program of size polynomial in and .
The rate involves the trace norm , the Schatten -norm (largest singular value), and the minimal distortion with side information of ,
the infimum over measurements on and the supremum over all finite-dimensional ; is the analogue with product measurements . Throughout, is base 2.
The page states with . The goal makes explicit the rate the proof gives.
Theorem 3.1 turns a nonconvex problem into a sequence of semidefinite programs whose values decrease to the optimum at rate , with a constant that depends polynomially on and logarithmically on . Every level is a certified upper bound; together with any feasible point it brackets . The same argument applied to channel fidelities gives converging outer bounds on the success probability of approximate quantum error correction (§4 of the paper), and the constrained de Finetti theorem is the key step there as well. Theorem 2.3 is of independent interest: it is the first finite de Finetti theorem in which the approximating separable state inherits linear constraints of the extension.
The results are proved in the paper; none of them has been machine-checked. A complete formalization requires the quantum relative entropy and mutual information with their chain rule, the quantum Pinsker inequality, state two-designs and their existence, and a weighted Hölder inequality for Schatten norms; most of this is absent from Mathlib, and each piece is reusable beyond this mission.
The obvious route measures every copy with a fixed informationally complete measurement and uses the resulting classical de Finetti statement. This approximates by a mixture of product states, but the states in the mixture need not satisfy , and projecting them onto the constraint set destroys the error bound. The paper instead conditions on the outcomes of only copies and keeps quantum; the constraint on then transfers to the conditional state of by symmetry. Making this rigorous needs the chain rule of conditional mutual information with classical conditioning, and the distortion of the measurement must be bounded independently of the side system , which is what Lemma D.1 provides. The Schatten-norm estimate there is elementary but requires a weighted Hölder inequality and a careful choice of weight.
Systems are finite index types: is indexed by Fin dA × (Fin N → Fin dB), is Mathlib's Kronecker product, and the permutation action permutes the word in Fin N → Fin dB. States, trace norm and partial traces are the published definitions WildeQIT_IsDensityOperator, WildeQIT_traceNorm and WildeQIT_partialTrace. The linear maps , are arbitrary -linear maps (not assumed positive or trace preserving), applied blockwise to one tensor factor. The objective is the real part of , equal to for Hermitian . Each "max" is the supremum of the set of objective values over the feasible set, never over all matrices. Wherever the page has copies of , the Lean has n + 1: SDPval … n is the page's , and the bounds have denominator . The distortions and take values in ; the standalone bound on assumes .
No feasibility hypothesis is added to the goal. The feasible sets of and of every level are empty or nonempty together, and the empty case reads . The goal mentions only , , , , and ; a formalization in which or were free real numbers, or in which the de Finetti mixture was not required to satisfy the constraints, would be a different and much weaker statement.
Contributions are welcome at every milestone, and especially in the reusable infrastructure: quantum relative entropy and mutual information on matrices, the quantum Pinsker inequality, unitary and state designs, and Hölder inequalities for Schatten norms.
Online sellers of loans, insurance, travel and retail goods observe data about each arriving customer before quoting a price. Using that data to price individually is attractive only if the seller can learn, from its own sales, how demand responds to price for customers with given characteristics. Two features make this hard in practice. The number of recorded characteristics is often large, possibly larger than the selling horizon , while only a few of them matter. And price sensitivity is itself heterogeneous: different customers respond to the same price change differently.
Ban and Keskin (Management Science 67(9), 2021) model both features and ask how fast the revenue lost to learning can grow. Their answer is that a seller who learns with lasso-regularized quasi-likelihood estimation and occasional price experiments loses revenue of order up to logarithmic factors, where is the number of relevant characteristics, and that no policy can do better than order . This mission formalizes the upper bound for the general (nonlinear-link) model with unknown sparsity, Theorem 3 of the paper.
In each period a customer arrives with a raw feature vector . The are i.i.d., take values in a compact set inside a ball of radius , have mean zero and positive definite covariance . The seller sees the augmented vector , charges a price with , and observes the demand
Here is an unknown parameter in a compact rectangle , the link is known, differentiable and increasing with on the relevant domain, and the demand shocks form a sub-Gaussian martingale difference sequence. The term is the customer's own price sensitivity. With the argument of is .
The sparsity of is , . The seller does not know .
The expected revenue of price is , and the clairvoyant price maximizes it; it is assumed to lie in the interior of for , . The regret of a policy over periods is
The policy ILQX charges the experimental price in periods and in periods , and otherwise charges , where maximizes the lasso-penalized quasi-likelihood
over the experimental periods (), and is the projection onto . The regularization level is for a constant .
There is a finite constant such that
is fixed with the model and is uniform over ; since varies over , the factor carries content.
Theorem 3 says that a seller facing many potentially relevant customer characteristics, without knowing which matter and under a nonlinear demand link such as logit, loses revenue at a rate governed by the number of relevant characteristics and only logarithmically by the total number . Combined with the paper's lower bound (Theorem 1, for the linear model), it makes ILQX first-order optimal up to logarithmic factors. An unregularized policy would pay order , which is linear in when exceeds .
The paper's proofs are in its electronic companion, which this mission does not reproduce; no machine-checked version of the result exists. A complete formalization would also produce a reusable high-probability error bound for lasso-regularized quasi-likelihood estimation under adaptively collected data (Lemma 3), and a machine-checked model of feature-based dynamic pricing on which related policies can be stated.
The estimation error must be controlled on data collected by the policy itself. The design vectors use only two prices, so the information about the price sensitivity accrues only from the experimental periods. Standard lasso error bounds assume a fixed or i.i.d. design and a restricted-eigenvalue condition on it; here a restricted-eigenvalue-type property of the random Kronecker design must be derived from and , and the noise enters through a martingale whose conditional law may depend on past prices. The quasi-likelihood is not a least-squares objective, so the curvature comes from the bounds , which hold only on the bounded domain and not at an unconstrained estimate. Finally, the regret bound has to turn a squared-error bound holding with probability into an expected revenue loss, which requires the revenue loss to be second order in the parameter error at an interior optimum.
Fin (d+1) → ℝ with the intercept at index 0; is Fin 2 × Fin (d+1) → ℝ with , . Periods are 1-based. .Contributions welcome: existence of a measurable maximizer of the objective, the counting lemma, and supporting lemmas for Lemma 3 and the regret bound.
Linear programs at very large scale are increasingly solved by first-order primal-dual methods, which use only matrix-vector products instead of matrix factorizations. Such methods parallelize well and have a small memory footprint, but on their own they are slow to reach moderate or high accuracy. Applegate, Hinder, Lu and Lubin (arXiv:2105.12715, Math. Program. 2022) showed that periodically restarting a primal-dual method from the average of its iterates turns its sublinear ergodic rate into a linear rate on sharp problems, a class that contains every linear program. The analysis underlies PDLP, a restarted PDHG solver studied computationally by Applegate et al. (arXiv:2106.04756) and shipped in Google OR-Tools.
This mission formalizes the paper's first convergence theorem: with restarts at a fixed frequency, the distance from the restart points to the solution set shrinks by a factor per restart.
Let and be closed convex sets and let be differentiable, convex in and concave in . Problem (1) is
with feasible region and primal-dual points . Its solution set is the set of saddle points : for all , . Throughout, .
Distances are measured in a semi-norm , which the paper allows in order to cover ADMM. Write , , and . The primal-dual gap (3) at is , and the normalized duality gap (4a)–(4b) is
By Definition 1, problem (1) is -sharp on if for all and all .
The base method is abstract. From a start it outputs averaged points , . It has Property 3 with constants if, for every start and every , and
i. ,
ii. .
Algorithm 1 with fixed-frequency restarts (29) runs the base method from for
steps, sets , and repeats, with .
If the base method has Property 3 and (1) is -sharp on with , then for every
Proposition 2 (p. 8) and Proposition 4 (p. 10) show where Property 3 comes from. A generic algorithm (6) with iterates and targets has Property 1 with if for every (12). It has Property 2 with if or .
Fact 1 (p. 11), that is non-decreasing in , is included as well.
Theorem 1 converts any primal-dual method with an ergodic rate on the normalized duality gap into a linearly convergent method on sharp problems. The rate is iterations to reach (Remark 3). Through Proposition 4 it applies to PPM, EGM, PDHG and ADMM. Combined with the paper's Lemma 5, which shows that linear programs are sharp with the inverse of a Hoffman constant, it yields linear convergence of restarted PDHG for LP. The paper also shows that this rate matches a lower bound for a general class of primal-dual methods.
The result is proved in the paper. As far as is known, no part of it, and no normalized duality gap or primal-dual sharpness notion, has a machine-checked proof. The mission adds a checked version of the restart argument, with every degenerate case resolved: zero displacements, unbounded balls, and semi-norms that are not norms.
Each proof is short, but the statements are delicate in ways the paper passes over.
A direct contraction argument that applies sharpness at an arbitrary radius, or on all of , does not prove the theorem as stated.
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). and are allowed.Seminorm ℝ on their product, never the product's built-in norm.EReal, so unbounded sets give and not a junk . is a real infimum over the nonempty set .Standing assumptions and added hypotheses:
Departures from the page:
The goal is not trivialized by its hypotheses. A companion check file exhibits on , with the sup norm and an oracle base method, on which every hypothesis of Theorem 1 holds and . Sharpness is assumed only where Definition 1 and the theorem assume it: replacing by , or the radius range by all , would weaken the theorem.
A complete development needs elementary facts about suprema in EReal, Jensen's inequality for convex-concave functions on averages, and geometric sums. The definitions of , sharpness and Property 3 are reusable for the adaptive-restart theorem of the same paper (Theorem 2, a separate mission) and for other restart analyses. Proofs of any milestone or companion are welcome.
Posted prices turn an offline allocation problem into a sequential choice process: each agent sees a menu of outcomes and prices, then chooses an outcome without revealing its full valuation. The balanced prices framework of Dütting, Feldman, Kesselheim, and Lucier gives welfare guarantees by comparing the revenue collected from an allocation with the welfare that remains feasible after it. Its appeal is that the comparison can be checked in a deterministic full-information setting before any probability distribution over valuations enters the analysis. Dütting et al., 2020
One valuation class at a time would make that framework difficult to reuse. Combinatorial auction valuations are often built by taking pointwise maxima of simpler valuations or by adding values from separate markets. Section 5 of the paper asks whether a price construction balanced for the simple class remains balanced after these operations. Theorem 5.3 gives the maximum closure result; Theorem 5.4 gives addition across markets. Appendix B extends both to the weaker balancing condition used elsewhere in the paper. Dütting et al., 2020, §5 and Appendix B
There are agents in a fixed order. Agent receives an outcome from a space containing a null outcome. A profile is feasible when it lies in . The model assumes downward closure: removing the outcomes of any group of agents from a feasible profile keeps it feasible. For a set of agents , write for the profile retaining on and assigning the null outcome elsewhere. The prefix retains only the agents before . Dütting et al., 2020, §2
A valuation profile assigns each agent a function . The welfare of is . Every base valuation takes values in , the normalization stated in §2. For any set of profiles, denotes the best welfare achievable in . An allocation rule ALG chooses a feasible profile from a valuation profile. A pricing rule assigns a nonnegative, possibly infinite price to outcome when the partial profile is ; an infeasible extension has infinite price. Dütting et al., 2020, pp. 547–548
An exchange-compatible family specifies a set of comparison profiles for each profile . It is exchange compatible when replacing any one coordinate of by the corresponding coordinate of any gives a feasible profile. This property is required for every in the full outcome space. A rule is -balanced for valuation , ALG, and that family, for constants and (Definition 3.1), when both inequalities hold for every feasible and every :
The maximum extension of a base valuation space consists of nonempty finite pointwise maxima of elements of . A base profile supports an extended profile at if at every outcome and for every agent. ALG is consistent when whenever supports at . The optimal allocation rule has this property by Lemma 5.2. Dütting et al., 2020, p. 554
The goal is Theorem 5.3. Given one exchange-compatible family and a collection balanced for every base profile, consistency of ALG preserves the same constants for every extended profile and every corresponding supporting base profile:
The milestone list records the welfare supremum comparison and the two price inequalities in the paper's proof. The family remains the same for all base and extended profiles. Dütting et al., 2020, Theorem 5.3 and proof
Theorem 5.4 treats separate allocation problems. The joint outcome and feasible set are products; values and prices add across components; ALG applies each component's rule. It asserts balancedness with the same and . Appendix B changes the second balancedness bound to and requires strong consistency for maximum closure. Theorems B.2 and B.3 preserve under maxima and addition, respectively. Dütting et al., 2020, Theorems 5.4, B.2, B.3
The maximum closure theorem lets a balanced-price construction for a simple valuation class cover finite maxima of that class without worsening its balancing constants. The addition theorem lets separately priced markets be combined by summing prices. Together these two operations account for the XOS composition discussed immediately after Theorem 5.4; the paper uses the results to connect its general framework to combinatorial auctions and multidimensional matroid settings. Dütting et al., 2020, p. 555
These results have paper proofs. The work here is to state their exact deterministic content in Lean so later formalizations of the price constructions can import the closure theorems. The definitions of supporting valuations, exchange-compatible families, and extended-real prices are reusable beyond this mission. The companion statements keep the product-market and weak-balancedness variants alongside the central theorem, while their proofs remain to be formalized.
For maximum closure, the prices are indexed by a base profile but must be balanced for a different profile that is pointwise larger. A supporting profile agrees with only at ALG's outcome , while condition (a) refers to , an outcome ALG chooses for a different input, and both conditions refer to optimal welfare over , where and can differ. Balancedness of for therefore says nothing about on its own; without a hypothesis tying ALG's choices for and together the statement is false, which is why consistency (Definition 5.1) is part of the theorem. The formal statement must keep the real-valued optimum meaningful for maxima of base valuations, so the normalization of §2 is carried through to . Dütting et al., 2020, Definition 5.1 and Theorem 5.3
For addition, a direct product of the component comparison families has an edge case: a component family can be empty while another is nonempty. The paper's displayed product family then makes the lower balancedness inequality too strong. The theorem statements ask for an exchange-compatible family to exist, as the printed theorems do; they do not require that failing product family. This discrepancy is recorded for review. Dütting et al., 2020, proof of Theorem 5.4
Agents and markets use zero-based finite indices; the paper writes agent indices from one. A profile's prefix contains exactly the agents with smaller indices. Valuations are functions to with base values in . The maximum extension uses a nonempty finite set of base functions, so its maximum is defined at every outcome. Optimal welfare is a real supremum; bounded valuations keep it finite, and the empty set has value zero. Prices are extended nonnegative reals so is retained. The lower balancedness inequality embeds its real right side using ofReal, which handles a negative lower bound consistently with nonnegative prices. The upper inequality keeps the price sum in extended reals.
The maximum theorem quantifies over every extended profile and every supporting base profile, including genuinely new maxima. It keeps one exchange-compatible family for all valuations. The maximum-closure theorems require every base price to satisfy the pricing-rule condition and conclude it for the supporting price. ALG feasibility is assumed on , which contains the base profiles. The product theorems construct joint outcomes, additive values, componentwise ALG, and summed prices from the component data; they do not admit an unrelated joint allocation rule. Downward closure and a zero price for the null outcome at feasible partial allocations are included for the product statements. The latter is a disclosed assumption satisfied by the paper's pricing examples and needed to handle empty component families. No distribution or posted-price run is part of this deterministic mission. Lemma 5.2 and the strong-consistency companion take an optimal rule to be one that attains the welfare supremum over on every profile in , the profiles to which Definitions 5.1 and B.1 apply it; the product companions additionally conclude that the summed prices form a pricing rule (infinite off ). Their ALG feasibility premise concerns the component profiles supplied in the theorem.
The development needs finite dependent products and sums, finite maxima, real suprema of bounded sets, and extended nonnegative arithmetic. Contributions proving the three maximum-closure milestones, the goal, or the product-market companions are all within scope. A proof that specializes the supporting profile to would lose the intended maximum extension and does not satisfy the goal's universal quantification.
An online player repeatedly chooses a subset of coordinates and pays the sum of their losses. In many applications the player sees only that sum, not the losses of the selected coordinates. This bandit feedback makes it harder to identify which coordinate within each chosen subset is responsible for a favorable or unfavorable outcome. Audibert, Bubeck and Lugosi studied how this information limit changes regret in online combinatorial optimization. Their Theorem 5 establishes a lower bound that scales linearly with the number of selected coordinates and with the square root of the ambient dimension and horizon. Audibert, Bubeck and Lugosi, 2013, pp. 13–14
The result is part of a comparison among full-information, semi-bandit and bandit feedback in the same action model. Under full information the player sees the complete loss vector after each round; under semi-bandit feedback the player sees losses at selected coordinates; under bandit feedback the player sees only one scalar. The paper proves upper bounds for semi-bandit play and a bandit lower bound. The latter is the target of this mission. Audibert, Bubeck and Lugosi, 2013, pp. 2–3, 14
Fix a dimension , a horizon , and a finite nonempty set . Each action has exactly entries equal to one. At round , the player selects a probability distribution on , draws an action , and simultaneously an adversary selects a loss vector . The player pays the scalar . In the bandit protocol, that scalar is the only new information made available for the next round. A player strategy can use every previous action and observed scalar loss, and can randomize at every round. Audibert, Bubeck and Lugosi, 2013, pp. 2–3
The paper measures performance by pseudo-regret against the best fixed action in expectation:
The expectation covers the player's randomization and, when present, the adversary's randomization. This benchmark chooses one action for the whole horizon after comparing expected cumulative losses. It is the sole notion of regret used in the paper. Audibert, Bubeck and Lugosi, 2013, p. 2 and footnote 1
For the lower bound, the appendix arranges the coordinates as parallel games with choices per game. An action selects one coordinate from each game. The adversary can associate a favoured choice with each game and assign independent Bernoulli losses whose means are at the favoured coordinates and elsewhere. The player still sees only the sum of the selected losses. These are the -adversaries that underlie the milestone statements. Audibert, Bubeck and Lugosi, 2013, pp. 16–17
The goal is Theorem 5 with the divisibility condition used by its appendix construction. For and , there is an action set such that every bandit strategy faces some bounded loss law with
The order of the choices is part of the claim: the action set is fixed first; then each player strategy may face its own adversary. The lower bound retains the paper's explicit constant . Audibert, Bubeck and Lugosi, 2013, p. 14, Theorem 5; p. 16
The milestones follow the appendix's stated results: Lemma 5 bounds a logarithm; Lemma 4 and its corrected second case bound the divergence between sums of independent Bernoulli variables; the one-round observation bound and the horizon bound control information revealed by bandit feedback. Equations (9), (10), and (11) connect that information to expected regret and symmetry. The final averaged bound on the chance of selecting a favoured choice closes the path to the goal. The milestones are stated for deterministic players, as in the first three steps of the appendix; the passage to randomized players (the appendix's fourth step) is part of the goal's proof and is not a separate milestone. Audibert, Bubeck and Lugosi, 2013, pp. 17–18, 20–21
The theorem prevents a uniform regret guarantee of smaller order than for this bandit action model. It shows that aggregating selected losses into a single observation imposes a cost beyond what a player can avoid by choosing a different randomized strategy. In particular, the quantifier over every strategy makes the claim about the feedback model, rather than about one named algorithm. The paper proves the result in Appendix B, with the Bernoulli-sum estimate in Appendix C. Audibert, Bubeck and Lugosi, 2013, pp. 14, 16–18, 20–21
The formalization work is to prove the existing paper result in Lean from a finite protocol that represents all behavioural player strategies, together with the finite laws of the appendix's adversaries. The resulting definitions of action paths, scalar observations, finite probability laws, and divergence estimates can support other finite-horizon bandit lower bounds. These statements are drafted as open Lean theorems; compilation checks their types, while proofs remain for solvers. The paper's mathematical proof does not itself constitute a machine-checked proof.
A scalar bandit observation sums losses from several games. The player cannot separate the contribution of the favoured coordinate in one game from the other selected losses by inspecting that observation. A bound for the divergence of a single Bernoulli variable therefore does not directly bound the information available to the player. The appendix's central estimate concerns sums of independent Bernoulli variables, followed by the law of the whole sequence of scalar observations. Audibert, Bubeck and Lugosi, 2013, pp. 16, 18, 20
There is also a correction to make explicit. Lemma 4 is false for some parameters allowed by its printed statement: taking , , and violates the displayed bound. The error is in the second case of its proof, which applies Lemma 5 outside its range when . The mission states Lemma 4 with the additional condition , which holds whenever , and states the corrected second case separately: for , . Through the corrected case, the one-round bound used by the goal holds for the full range , so Theorem 5 and its constant are unaffected. Audibert, Bubeck and Lugosi, 2013, pp. 20–21, Lemmas 4–5
Actions are functions constrained to zero or one, with coordinate sum . Coordinates and rounds are indexed from zero. A behavioural strategy maps every history of chosen actions and real-valued observed losses to a probability distribution on the finite action set. Its domain includes every real history, even though the appendix's particular Bernoulli adversaries generate integer observations. The strategy may randomize; restricting the goal to deterministic players or allowing it to inspect an unobserved loss vector would change the game.
The goal's exhibited adversary is an oblivious, finitely supported probability law on loss sequences in . It belongs to the broader adversary class of the paper, so this existential formulation is stronger. All expectations are finite sums. The regret comparator is a minimum over the nonempty action set, not a default value assigned to an empty set. The action set has binary entries and equal coordinate sums, and every loss lies in the unit interval; these clauses rule out trivial lower bounds from malformed actions or unbounded losses.
The hypothesis is added to the printed theorem because Appendix B assumes it to partition coordinates into equally sized games. When , it forces and the claimed lower bound is zero. The milestone model uses functions with , deterministic players, finite Bernoulli product laws, and a finite real KL sum. Its log ratios are meaningful on the common support ensured by the stated parameter bounds. Reusable contributions include the finite bandit protocol and observation laws, as well as proofs of the KL and averaging milestones.
A partially observable Markov decision process describes a controlled system whose state is hidden but whose observations are available to a decision maker. The distribution of the hidden state conditional on the observations is the belief state. Replacing the hidden state by this distribution turns the model into a fully observed decision process, provided the resulting belief transition has the regularity needed by the usual existence and dynamic programming results. Feinberg, Kasyanov, and Zgurovsky give sufficient conditions for that regularity in their study of total-cost POMDPs, Theorems 3.6 and 3.7.
Their observation-kernel condition is continuity in total variation. Example 4.1 of the same paper tests its sharpness: the authors construct a two-state model with setwise-continuous observations for which the belief transition fails to be weakly continuous. This matters when selecting assumptions for a POMDP theorem. Setwise convergence already requires convergence of the probabilities of every fixed observation event, so it can look adequate for belief updates. The example shows that it is still too weak for the stated conclusion.
The hidden state space is and the observation space is with Lebesgue probability measure . The action space is , equipped with the topology inherited from . The state does not move: its transition law is the point mass at for every action. Its continuity in total variation is immediate from this fixed-state behavior.
At hidden state 1 the observation law is always . At hidden state 2, action zero also produces . Under action , state 2 produces a law . The density equals zero on the open left half of each cell in the -part dyadic partition and equals two elsewhere, including the cell endpoints. Equation (4.1) gives the exact intervals. These laws oscillate more rapidly as grows, and the paper establishes for every fixed Borel set . Thus the observation kernel is setwise continuous even at the accumulation action zero. Example 4.1, pp. 13–14.
A belief assigns a probability to each hidden state. For a current belief and an action , the joint law covers the next state and its observation, and is the observation marginal. A filter is a conditional law of the next state given observation : it satisfies the disintegration identity (3.3). The belief transition is the law of the random posterior when has law . These objects are defined in (3.1)–(3.5) of the paper. Different versions of agree only almost everywhere for each current belief and action, yet they yield the same belief transition.
At the uniform belief , action zero reveals nothing, while every positive-index action produces the same two-point posterior law:
The mission's goal asserts that is total-variation continuous, is a setwise-continuous probability kernel, a valid filter exists, and the positive-index laws fail to converge weakly to the zero-action law as . It states the failure for every filter satisfying (3.3), so it is a property of the POMDP rather than of a selected version of its conditional distribution. The milestone list follows the paper's assertions: setwise convergence of the dyadic laws, setwise continuity of , the two posterior values almost everywhere, and the explicit laws of .
The example identifies a precise boundary of the sufficient condition in Theorems 3.6 and 3.7. Those theorems use total-variation continuity of the observation law to obtain a weakly continuous belief transition; replacing that premise by setwise continuity makes their continuity conclusion false in this model. The explicit law also shows the size of the discrepancy: the positive-index belief transition has two fixed atoms, while the zero-action transition is concentrated at the original belief. Example 4.1, pp. 13–14.
A machine-checked development would add reusable definitions of sequential kernel continuity, the joint state-observation law, conditional filters, and the belief transition on the Borel space of probability measures. It would also formalize a concrete setwise-convergent sequence of densities whose induced posterior laws do not converge weakly. The paper proves the example; the Lean statements in this proposal are open proof targets, with no completed machine-checked proof claimed here.
Setwise continuity controls for each fixed Borel set . A posterior is a probability measure determined by the observation, and the belief transition tests the distribution of those posterior measures. The observation regions distinguishing the states change with , so convergence on fixed observation sets does not imply convergence of their posterior distributions. This is the gap in the immediate argument that tries to pass from setwise convergence of to weak convergence of .
The conditional filter adds a second precision issue. Equation (3.3) determines its values only almost surely under the observation marginal, and different versions may disagree on null observations. Any claim about a posterior value at every would exceed the source; the posterior milestone therefore has an almost-everywhere qualifier, while the goal quantifies over every valid version of .
Lean represents by Fin 2, with 0 for the paper's state 1 and 1 for state 2; by unitInterval; and by the specified subtype of . Positive integers are a subtype of , so the density and the action are never evaluated at . The measure is volume on unitInterval, which has total mass one. The density follows (4.1) literally, with open zero intervals and density two at their endpoints. The general transition and observation law use Mathlib kernels; the example instantiates them directly. The goal includes the probability-kernel property of the concrete and existence of a valid , guarding the universal filter clause against vacuity.
Weak, setwise, and total-variation convergence are sequential, as on page 4. The weak test class consists of bounded continuous real functions; the setwise test class consists of all Borel sets. The target space of carries the Borel σ-algebra of the weak topology on , stated explicitly because Mathlib's default measurable structure on that type is the Giry σ-algebra. The filter predicate requires measurability in for fixed in both structures. Joint measurability in is described in the paper but is not encoded in this local predicate; only the fixed-parameter property is used by (3.3) and (3.5). This choice and its quantifier effect are recorded in the moderation notes.
No cost, initial observation kernel, initial prior, or discount factor enters Example 4.1. Contributions on the dyadic law, kernel continuity, conditional posterior values, and the resulting belief-law identity are all within scope. A filter hard-coded to return the prior belief, a discrete topology on , or a claim for only one version of would change the counterexample and is excluded by the definitions and goal.
A partially observable Markov decision process (POMDP) models a controller that cannot see the state of the system it steers, only noisy observations of it. Inventory control with unrecorded demand, machine maintenance with imperfect inspection, and target tracking from sensor readings all have this form. The standard way to solve a POMDP is to replace it by its belief MDP, also called the completely observable MDP (COMDP): the state becomes the posterior distribution of the hidden state given everything observed so far. The belief MDP is fully observed, so the theory of Markov decision processes applies to it, but only if the belief MDP satisfies that theory's hypotheses. For MDPs with Borel state and action spaces, unbounded costs and possibly noncompact action sets, the hypothesis that yields optimality equations, convergence of value iterations and stationary optimal policies is Assumption (W*) of Feinberg, Kasyanov and Zadoianchuk (Math. Oper. Res. 2012): the cost is -inf-compact and the transition probability is weakly continuous.
Before Feinberg, Kasyanov and Zgurovsky (arXiv:1401.2168v2, published in Math. Oper. Res. 41(2), 2016), sufficient conditions for the belief MDP to be weakly continuous required a weakly continuous filter (Hernández-Lerma, 1989, as recalled on p. 11 of arXiv:1401.2168v2), a condition that fails in many natural models. The paper replaces it by a condition on the primitive data of the POMDP.
Let (states), (observations) and (actions) be Borel subsets of Polish spaces. Let be the transition kernel on given , the observation kernel on given , and a Borel one-step cost bounded below. is the set of probability measures on with the topology of weak convergence ( for bounded continuous ). A sequence converges setwise if for every Borel , and in the total variation if over Borel with values in . A kernel is weakly (setwise, total-variation) continuous if implies the corresponding convergence of the measures.
For a belief and an action , let be the joint law of the next state and observation (3.1), and its observation marginal (3.2). A filter is a kernel with (3.3): is the posterior after observing . The belief MDP has state space , action set , cost (3.8), and transition , the law of when (3.5). A cost is -inf-compact on if its restriction to has compact level sets for every compact .
If either Assumption (D) () or Assumption (P) ( and ) holds, is bounded below and -inf-compact on , is weakly continuous and is continuous in the total variation, then the belief MDP satisfies Assumption (W*):
Theorem 3.6 supplies the hypothesis under which the cited general MDP theory gives stationary optimal policies, optimality equations and convergence of value iterations for total-cost POMDPs in terms of , and alone, without compactness of the action set, boundedness of the cost or continuity of the filter. It covers, for example, observation kernels with densities continuous in , and the paper applies it to inventory control with incomplete records and to the Kalman filter. Example 4.1 of the same paper shows that total-variation continuity of cannot be weakened to setwise continuity.
The result is proved in the paper; this proposal poses its formal statement and the supporting results as proof targets. Completing them would provide a checked bridge from POMDPs to the general MDP theory under weak continuity, together with reusable facts about weak, setwise and total-variation convergence: equicontinuity of integrals against weakly continuous kernels (Theorem 5.2), the convergence-in-probability criterion (Theorem 5.5), and the generalized Fatou lemmas.
The posterior is defined only for -almost every and has no continuous version in general, so weak continuity of cannot be read off from continuity of . The tempting argument, that continuous and make the Bayes posterior move continuously, fails: need not be countable and need not have densities. What has to be controlled is the joint law on sets uniformly in the observation set ; convergence for each fixed is not enough. Turning this uniform control into almost-sure convergence of posteriors along a subsequence requires a diagonal argument over a countable base of . On the cost side, the difficulty is that may take the value and is not continuous; -inf-compactness has to be transported through integration against a weakly converging sequence of measures.
All definitions live in FeinbergPOMDP.WStar.Model. are separable metrizable spaces with their Borel σ-algebras (PolishSpace is not assumed, since Borel subsets of Polish spaces need not be Polish); is additionally nonempty and standard Borel in Theorems 3.6 and 3.7, where a filter must exist. is Mathlib's ProbabilityMeasure with the weak topology. All continuity notions are the paper's sequential ones; total variation is the supremum over Borel functions with values in , written in – form, while the set-indexed suprema of (5.15) and (5.17) keep their set form. The cost is written with and taking values in , so , exact even when on a set of positive measure. -inf-compactness is the published FeinbergLiang.ACOE.KInfCompact. A filter is a map that satisfies (3.3) and is jointly Borel measurable in , as the paper's stochastic kernel is; is the image of under for the Borel σ-algebra of the weak topology on .
Since does not depend on the choice of filter, every statement about is made for every filter satisfying (3.3). A fixed filter that ignores the observation, such as , would make a point mass and the weak continuity trivial; it satisfies (3.3) only when observations carry no information, and is excluded by quantifying over all filters.
The goal states the Assumption (W*) conclusion of Theorem 3.6. Its tail, "statements (i)–(vi) of Theorem 3.1 hold", invokes Theorem 2.1 of Feinberg et al. (2012) applied to the belief MDP; it is cited rather than proved in this paper. Generalized Fatou's lemmas 5.1(i) and 5.1(ii) are referenced from the published Schäl (1993) items. A complete development needs weak and setwise convergence on ProbabilityMeasure, portmanteau-type arguments, disintegration (Measure.condKernel) and the identification of the Borel and Giry σ-algebras on ; the last is missing from Mathlib and is a welcome contribution in its own right. Proofs of any milestone, and alternative arguments for Theorem 3.7, are welcome.
Wasserstein distributionally robust optimization (DRO) replaces the empirical risk of a loss by its worst case over all distributions within Wasserstein distance of the empirical law . Gao, Chen and Kleywegt (arXiv:1712.06050; Operations Research, 2024, doi:10.1287/opre.2022.2383) show that, for small radii, this worst-case risk is the empirical risk plus times a variation of the loss (a norm of its gradient or local slope), up to a remainder. This links DRO to gradient-norm regularization, as used in adversarial training and in data-driven newsvendor and pricing models.
For smooth losses the remainder is of order . Many losses used in practice are only piecewise smooth: hinge, ReLU networks, newsvendor costs, . Near the set where the pieces meet, the first-order expansion fails, and the paper's Theorem 1(I)–(II) carries an extra boundary term . Theorem 1(III) shows that this term is small with high probability, uniformly over the loss class, provided the data distribution does not concentrate near the non-smooth points. This mission formalizes that probabilistic bound.
Let be a metric space with its Borel -algebra, a probability measure on , and an i.i.d. sample from , with empirical law . The sampling law is the product on , and is its expectation. The formal statements also assume the metric space is second countable.
Let be a set of losses , and for each let be its non-smooth set: for a piecewise smooth with pieces , the union of the pairwise intersections of their closures (Assumption 1). The paper assumes is -null. The distance to a set is , with .
The objects of the mission are:
In Lean the boundary gap is the shared WassVarReg.PInf.boundaryGap; nearIndicator, indicatorClass, empRademacher, rademacher and Assumption3 are in WassVarReg.Boundary. The sample law is the published MinimaxWass.DataDep.sampleLaw.
Under Assumption 3 there exist such that for all , and , with probability at least , for every ,
The constants and are left unspecified; they depend only on Assumption 3.
The result. With and a class of bounded complexity, the right side of the goal is . Combined with Theorem 1(I)–(II), it gives the paper's conclusion that -Wasserstein DRO with is asymptotically equivalent to empirical variation regularization, , for non-smooth losses, uniformly over the class. Without it, the boundary term is only bounded by , and the expansion has no better accuracy than first order. Assumption 3 is the condition under which the non-smooth set does not matter statistically.
Formalizing it. The result is proved in the paper; it has no machine-checked proof. Its proof composes a uniform deviation bound (McDiarmid's inequality plus symmetrization) with a bounded-density estimate. The mission produces a general Rademacher deviation bound for bounded classes on an arbitrary metric space with a measurability guard, reusable by any statistical-learning mission, and fixes the printed constant of Lemma EC.5 ( on the page, from its proof).
The deterministic parts are short. The difficulty is in Lemma EC.5. McDiarmid's inequality must be applied to the uniform deviation over an arbitrary, possibly uncountable, class. Symmetrization must then be carried out with Bochner integrals over and a finite sign space. Neither tool is in Mathlib in this form. A tempting shortcut, bounding each fixed by Hoeffding's inequality and taking a union bound, fails: the class is infinite, and the bound must hold simultaneously for all inside a single event. A second point is Assumption 3: it controls only the shell , so the mass of has to come from the null closure of .
[MeasurableSpace Z] [BorelSpace Z] [SecondCountableTopology Z] in the goal-level statements. Second countability is an added technical hypothesis used throughout this paper's mission series. A sample is ω : Fin n → Z with , and its law is Measure.pi. Empirical means are .Metric.infEDist, which is on . A loss with thus has boundary gap and is excluded from , as on the page. The real-valued Metric.infDist (which is on ) would give such a loss gap and is not used.D : (Z → ℝ) → Set Z. The goal-level statements assume each is closed and -null, the standing consequence of its construction in Assumption 1. The details of the piecewise smooth loss model are not needed for this probability estimate.Contributions welcome: a general McDiarmid inequality for product measures, a symmetrization lemma for measurable classes, and proofs of the milestones in any order.