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?
The European Union's General Data Protection Regulation (GDPR, in force since 2018) requires a firm to obtain a consumer's explicit opt-in consent before it collects her personal data. Most of the economic literature reads such consent rules as a cost to data-driven firms. Choe, Matsushima and Shekhar (ISER Discussion Paper No. 1246, Osaka University, June 2024; published in Management Science, 2025, doi:10.1287/mnsc.2024.06653) ask what happens to the price of a digital service when consumers gain the right to buy it without sharing data. Their model is a monopoly with two-dimensional consumer heterogeneity, simple enough to be solved in closed form, and it lets the answer be stated for every value of the firm's opt-in benefit and every mix of usage-based and data-based revenue.
This mission formalizes the paper's general price comparison, Proposition A1: the equilibrium price is higher after the GDPR.
A monopolist sells an online service at zero marginal cost and price . A consumer has a type , where is her valuation for the service and her privacy cost of sharing data; types are independent and uniform on , so the mass of a set of consumers is its area. A consumer who shares data receives an opt-in benefit , and the firm earns an exogenous data revenue per unit of shared data.
The utilities of opt-in purchase (buy and share) and opt-out purchase (buy without sharing) are
The firm chooses the price first and consumers respond, so the equilibrium price in each regime is a maximizer over of the corresponding profit: for and for . The paper's appendix expresses them through the thresholds
and the radicals , .
For every and , both profits attain a global maximum on , and every pair of maximizers satisfies
The result. Proposition A1 says the price rise is robust: it holds for every opt-in benefit and every revenue model, from a firm that earns nothing from data () to one whose data revenue dominates. The paper's welfare results (on demand, profit and consumer surplus) are comparisons of the same two equilibria, and the price comparison is the one among them that holds uniformly; the others change sign with and are established in the paper only numerically. The main text's Proposition 1 is the instance .
Formalizing it. The paper's proof is a chain of closed-form computations spread over the appendix and online appendix: areas of polygons, the maximization of piecewise cubic profits over all of , and a sign argument with nested square roots. Several steps are stated as "one can verify", and the online appendix contains printed slips (a derivative written with respect to the wrong variable in §D, a pair of cases listed incorrectly on p. 14). A machine-checked proof turns the chain into a verified one. The milestones isolate the parts that are reusable on their own: the demand formulas (4)–(6) and the closed-form equilibria, on which the paper's companion profit comparison (Proposition A3) also rests. None of these results has been formalized before.
The obvious route, solving the first-order condition on each demand piece, gives candidates, not maximizers. The profits are only piecewise smooth, the pieces meet at and , and the price ranges over all of , including negative prices before the GDPR. Showing that the candidate is the unique global maximizer requires comparing values across pieces and controlling the profit outside the paper's displayed price ranges. The comparison step is the second difficulty: in the middle region the gap mixes a polynomial with a square root, and its positivity is not a one-line estimate. The gap tends to as , so no uniform margin is available.
q : ℝ × ℝ with q.1 = v, q.2 = c; the type square is Set.Icc 0 1 ×ˢ Set.Icc 0 1, and every demand is (volume S).toReal for the Lebesgue measure on ℝ × ℝ.ℝ → ℝ of the price, and an equilibrium price is IsMaxOn profit Set.univ p. The price is never restricted to the paper's case ranges, and is a consequence, not an assumption.α in Lean.A formalization that compares the two closed-form prices instead of maximizers of the modelled profits, that asserts a property of "every maximizer" without proving one exists, or that restricts prices to a bounded interval, would not state Proposition A1; the goal and the milestones rule all three out. Results of the paper established only numerically (Propositions 2–4, A2, the second and third bullets of A3, A4) are not posed, and neither are the comparative statics of Lemmas A1–A2.
A complete development needs areas of polygons under the Lebesgue measure on (via MeasureTheory.volume_regionBetween or Fubini), elementary calculus on piecewise polynomials, and inequalities with square roots. The demand computations and the global-maximization arguments are reusable for the companion mission on the paper's profit comparison. Contributions of any milestone, or of further intermediate lemmas such as the continuity of the demands in the price, are welcome.
Online advertising lets a firm aim its messages at the consumers most likely to want its product, but the data behind that aim is noisy: a platform's prediction of who belongs to a demographic or interest segment is right only with some probability. A natural expectation is that sharper targeting raises firms' profits, since fewer messages are wasted. Karle and Reisinger (SSRN 4626076, March 2024; published in Management Science, doi:10.1287/mnsc.2023.03632) show that this can fail: when both firms chase the same valuable consumers, better targeting also increases the number of consumers who see both firms' advertisements, which intensifies price competition.
The model combines a targeting stage with the clearinghouse price-competition model of Varian (1980) and Narasimhan (1988), in which some consumers are informed about one firm only (loyal consumers) and others about both (shoppers), and equilibrium prices are dispersed. This mission formalizes the paper's result for costless advertising: industry profit first falls as targeting improves, then jumps up when firms switch to segmenting the market, then stays flat.
There are two consumer groups and , each of mass one. Group- consumers value the product at , group- consumers at , with . Two firms produce at zero cost. For every consumer each firm receives a signal of the consumer's group that is correct with probability , independently across firms. Only consumers of the group a firm targets are interested in its product.
Stage 1. Each firm chooses a target group and a message scope: expected (message only the consumers its signal places in group , which reaches a mass of group ) or all (message every consumer, which reaches all of group ). Messages cost each; in this mission .
Stage 2. Having observed stage 1, firms set prices. For a stage-1 profile , if both firms target the same group, the shoppers are the targeted consumers reached by both, where is firm 's reach; firm 's loyal mass is . If they target different groups, and . A consumer buys if the price does not exceed her valuation; shoppers buy from the cheaper firm and split equally on ties. Firm 's profit at prices is , or according as , or , and if exceeds the valuation.
Firms may randomize prices: a price strategy is a probability measure on , and is firm 's expected profit. A subgame perfect Nash equilibrium (SPNE) is a pure stage-1 profile and a continuation that assigns to each of the sixteen stage-1 profiles a Nash equilibrium of its pricing subgame, such that no firm gains at stage 1 by changing its action. The sum of expected profits is .
Two cumulative distribution functions appear, on :
both below and from on, so has an atom at . The thresholds are and .
For : ; for every there is an SPNE with
which is strictly decreasing in ; for every there is an SPNE with sum ; and (the upward jump).
The proposition shows that the non-monotonicity of industry profit in targeting precision, which the paper first derives for high advertising costs, does not rely on advertising being costly. With free messages a firm could inform every consumer, which is equivalent to perfect targeting; the equilibrium instead has one firm refrain from doing so, because the resulting asymmetry keeps prices high. For regulation of consumer data and for platforms selling targeting precision, the result says that better targeting technology can lower sellers' profits over a range of precisions and raise them discontinuously elsewhere.
The result is proved in the paper (main text and Online Appendix A). It has not been machine-checked. Formalizing it means verifying mixed-strategy equilibria of a pricing game with a continuum of prices, including an atom at the valuation, in all sixteen subgames of a two-stage game, a pattern that recurs throughout the clearinghouse and price-dispersion literature.
The stage-1 comparison is arithmetic once the stage-2 payoffs are known; the work is in the pricing subgames. Each mixed equilibrium must be verified against every real price deviation, which needs the expected profit at price against a distribution with an atom, where the tie-splitting rule matters exactly at the atom. Subgame perfection requires a pricing equilibrium in every off-path subgame too, including those where both firms target group (the group- equilibria rescaled by ) and the Bertrand subgames. The obvious shortcut, assigning each subgame its textbook profit as a number, is not available: the stage-1 values are defined as integrals against the equilibrium strategies.
Lean 4 with Mathlib. The pricing game is a separate definition (a general clearinghouse duopoly with valuations , loyal masses and shopper mass ); the targeting game builds on it. Committed conventions:
ProbabilityTheory.cdf; statements about all measures with cdf also assert that such a measure exists;The goal is Proposition 2 in existence form: it asserts an SPNE with the stated total. The paper exhibits that equilibrium; uniqueness of equilibrium payoffs is not claimed. Propositions 1 and 3 (high and general costs) are not posed. Trivializing encodings are excluded by construction: stage-1 values are integrals of the continuation strategies, not a table; the equilibrium condition quantifies over all sixteen subgames, not just the path; strategies are probability measures on , so no integral takes a junk value; and statements quantifying over measures with a given cdf include the existence of one.
Contributions welcome: integration of the tie-split profit against cdfs with atoms, a reusable lemma that a clearinghouse with given loyal and shopper masses has an equilibrium, and the rescaling of equilibria by the valuation.
This mission develops Chapter 4 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let take values of bit width , i.e. for all , and let evaluate in binary. Algorithm 2 with budget starts from a uniformly random incumbent and repeatedly runs Algorithm 1 (search with an unknown number of marked items) with the marking unitary , replacing by the returned index whenever ; a call of Algorithm 1 that would exceed the budget is interrupted at the -th application of , and the algorithm then returns . Each application of counts as one application of and is charged additional gates; each round of Algorithm 1 with qubits of precision is charged further gates (Hadamards and the inverse QFT).
There are absolute constants such that for every , , every such and every the following holds. Run Algorithm 2 independently times with budget and output an -minimal one of the returned indices. Then:
and the number of additional gates is at most .
This is the quadratic quantum speedup for unstructured minimization, the basis of the optimization applications of Grover search.
Formalization Note The source's gate bound is stated with the suppressed polylogarithmic factors and explicit, the interruption rule for the budget is made explicit, and , are the choices of the source's proof. Algorithm 1 is the shared formalization of the earlier corollary; the outcome law is a weight on (returned index, applications of , gates).
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
The class number formula connects the analytic behaviour of the Dedekind zeta function of a number field at with the basic arithmetic invariants of : its class number, regulator, number of roots of unity and discriminant. It is the main tool for computing and bounding class numbers analytically, and its quadratic case, Dirichlet's class number formula, came out of Dirichlet's proof of his theorem on primes in arithmetic progressions.
Timeline.
Let be a number field of degree , where is the number of real embeddings and the number of complex embeddings of . Write for the class number (the order of the ideal class group), for the regulator, for the number of roots of unity in , and for the discriminant of . The Dedekind zeta function is the Dirichlet series
For the quadratic case, let be a fundamental discriminant, let be the number of proper () equivalence classes of binary quadratic forms of discriminant (positive definite ones if ), and let be the Kronecker symbol, a Dirichlet character modulo with -function . For let according as , , . For let solve with minimal, and put .
with the supporting facts that is a Dirichlet character, that for a quadratic field, that the Pell equation is solvable, and that is a fundamental unit or its square. 5. Finite forms of for prime conductor :
The result. The formula makes computable from -values. In the quadratic case it gives closed formulas for class numbers, and it implies that for real characters, which is the hardest step in Dirichlet's theorem on primes in arithmetic progressions. Its refinements for cyclotomic fields relate class numbers to cyclotomic units and lead into Iwasawa theory.
Formalizing it. The result is classical. Mathlib already proves the residue as a one-sided real limit, as , and that statement is available on the platform as a proved theorem. What is not formalized is the meromorphic continuation of to all of with a single simple pole, which is what the goal requires. Dirichlet's formula in terms of binary quadratic forms, its supporting facts, and the finite forms of are not formalized either.
The residue formula follows from counting ideals of bounded norm, but that only controls for real . Continuing to all of needs a separate analytic input, such as theta functions or Hecke's integral representation with a functional equation, or a decomposition into Hecke -functions. Mathlib has such continuations for the Riemann zeta function and Dirichlet -functions, but not for in general. For Dirichlet's formula, the hard part is connecting classes of binary quadratic forms (proper equivalence, positive definiteness for ) with ideal classes of the quadratic order, keeping track of the unit and automorph conventions that decide the constants and .
NumberField.dedekindZeta (the Dirichlet series, meaningful for ) together with nrRealPlaces, nrComplexPlaces, regulator, classNumber, torsionOrder and discr. The continuation is stated as an entire function with on and equal to the residue. Since the residue is positive, this rules out the trivial reading where is continued with no pole.DirichletCharacter.LFunction, the analytic continuation, so is its value at and not the (conditionally convergent) series. The character is a hypothesis agreeing with the Kronecker symbol, and a separate milestone shows that such a character exists.The Fourier coefficients of modular forms are among the most studied arithmetic functions in number theory. In 1916 Srinivasa Ramanujan studied the coefficients of the discriminant modular form and conjectured three properties: multiplicativity, a three-term recursion on prime powers, and the bound for primes (Ramanujan 1916). Hans Petersson extended the size bound to the coefficients of holomorphic cusp forms for congruence subgroups (Petersson 1930). The resulting Ramanujan–Petersson conjecture for holomorphic cusp forms is now a theorem of Deligne (weight ) and Deligne–Serre (weight ). Its analogues for Maass forms and for general automorphic representations remain open.
Timeline (as recorded in the source article, Wikipedia: Ramanujan–Petersson conjecture):
Let and . The Dedekind eta function is . The discriminant modular form is
It is a holomorphic cusp form of weight and level . Ramanujan's tau function is defined by the Fourier expansion
Its Ramanujan -function is the Dirichlet series .
More generally, let be a congruence subgroup, meaning that contains the principal congruence subgroup for some . A holomorphic cusp form of weight for is a holomorphic function with for every , which vanishes at every cusp. Such an is periodic with some least period , and it has a Fourier expansion with . When contains (for example , , or itself), and .
For every congruence subgroup , every weight , every cusp form of weight for with coefficients , and every ,
The goal splits by weight into Deligne's theorem () and the Deligne–Serre theorem (), both listed as milestones.
The bound says that the roots of have equal absolute value , an analogue of the Riemann hypothesis for the local factors of . The bounds for general cusp forms are used throughout analytic number theory to control sums of Fourier coefficients. They are also used in the explicit construction of Ramanujan graphs by Lubotzky, Phillips and Sarnak, which are optimal expander graphs. The generalized conjecture for implies Selberg's conjecture on Laplace eigenvalues.
All targets in this mission are proved theorems in the literature. At the pinned Mathlib revision, none of them is formalized except the identity . Mathlib does contain the definitions they need: , as a cusp form of weight 12 and level 1, -expansions, congruence subgroups, and the -function of a cusp form. Mathlib also proves the analytic continuation of that -function. The remaining work is to formalize Hecke theory for , the elementary consequences of Deligne's bound, the -function statements, and ultimately Deligne's and Deligne–Serre's theorems.
The algebraic statements about (multiplicativity, the recursion, the Euler product) and the functional equation are classical, but formalizing them needs infrastructure that Mathlib does not yet have, such as Hecke operators on cusp forms. The size bounds are of a different kind. Estimates from the Petersson inner product or from Hecke's method give only the exponent (Hecke's bound). That exponent is attainable by complex analysis alone, but the improvement to is not. In the literature it depends on arithmetic geometry: Deligne's proof of the Weil conjectures for , and Galois representations for . The analytically similar statement for Maass forms is still open.
ModularForm.discriminant with period , as a complex number. The source's description of is taken as the definition, and integrality is not assumed.atTop on , with the constant allowed to depend on .Subgroup.strictWidthInfty). This equals whenever lies in . A congruence subgroup is CongruenceSubgroup.IsCongruenceSubgroup.In the AdS/CFT correspondence a quantum theory of gravity in an asymptotically anti-de Sitter spacetime is equivalent to a conformal field theory on its boundary. A central question is how local bulk physics is encoded in the boundary theory, and in particular which bulk region is described by a given boundary subregion . Harlow's TASI 2017 lectures (arXiv:1802.01040) review the answer that emerged from quantum error correction: the boundary Hilbert space is a code, bulk effective field theory lives in a code subspace, and the boundary subregion can reconstruct every bulk operator in its entanglement wedge. The lectures state as their main technical target the theorem that this entanglement wedge reconstruction, the quantum Ryu–Takayanagi (RT) formula with a central area operator, and the JLMS formula (equality of boundary and bulk relative entropies) are mathematically equivalent. All of these statements are finite-dimensional linear algebra, which makes them formalizable now.
Timeline. Almheiri, Dong and Harlow proposed the quantum-error-correction interpretation of AdS/CFT in 2014 (arXiv:1411.7041). Jafferis, Lewkowycz, Maldacena and Suh derived the JLMS relation in 2015 (arXiv:1512.06431), and Dong, Harlow and Wall established the implications between JLMS and reconstruction for factors in 2016 (arXiv:1601.05416). Harlow proved the general three-way equivalence for arbitrary finite-dimensional von Neumann algebras in 2016 (arXiv:1607.03901, Comm. Math. Phys. 2017). The TASI lectures (2017, published 2018) present this theorem as Theorem 5.2.
All Hilbert spaces are finite-dimensional. The boundary space factorizes as . A code subspace is described by an isometry whose columns are an orthonormal basis of . An operator on represents a logical operator if and for every code state.
A von Neumann algebra on is a set of operators closed under sums, products and adjoints and containing all multiples of the identity; is its commutant and its center. Every such is block diagonal, with . For a state with diagonal blocks , the algebraic entropy is , and the algebraic relative entropy is defined analogously (eqs. (5.16), (5.18)).
For and a von Neumann algebra on , the following are equivalent:
Theorem 5.2 turns three separately motivated features of holography into a single mathematical statement. Since the RT formula is independently derived from the gravitational path integral, the theorem implies subregion duality in the entanglement wedge; it also shows that a non-trivial area operator requires an algebra with non-trivial center. Theorem 4.1 is the subsystem-code special case, and Theorem 5.1 is the structure result that gives the algebraic entropies their meaning.
The results are proved in the literature (Harlow 2017 for Theorem 5.2; Theorems 4.1 and 5.1 are standard), but the lectures state Theorem 5.2 without proof, and none of these statements has a machine-checked proof that this mission is aware of. The mission produces formal statements and, eventually, formal proofs of the finite-dimensional structure theory of operator-algebra quantum error correction.
The three conditions live at different levels: (1) is a statement about operators, (2) about von Neumann entropies of single states, and (3) about relative entropies of pairs of states. Passing between them requires control of the full block structure of relative to the bipartition , not only of a single factor, and the classical term of (5.18) couples different blocks, so the general case does not reduce to the factor case treated earlier in the literature. Relative entropies can be infinite (when supports are not nested), so the equalities in (3) are equalities of extended reals and every argument must remain valid at .
Hilbert spaces are coordinate spaces for finite index types, operators are complex matrices, tensor products are Kronecker products, and is the image of an isometry (an operator acts on code states as applied to ). States are density matrices (positive semidefinite, trace one). Von Neumann entropy and relative entropy are defined from eigen-decompositions; relative entropy takes values in the extended reals. A von Neumann algebra is a -subalgebra of matrices; the algebraic entropies are computed in a block decomposition of , which every statement takes as an arbitrary decomposition realizing (the value does not depend on the choice). The RT identity is stated as an equality of complex numbers. Theorem 4.1 assumes a nonzero code subspace; the Singleton bound assumes and ; both conditions are implicit in the lectures and are needed for the statements to be true.
A trivializing reading is excluded: the hypotheses of every statement are satisfiable, and the goal is a full equivalence of three non-trivial conditions rather than any single implication.
Useful reusable infrastructure: partial traces and their interaction with Kronecker products, entropies of block-diagonal states, relative entropy (Klein's inequality and its equality case), and the structure theory of finite-dimensional -algebras of matrices. Contributions of proofs of the individual implications (1)⇒(2), (2)⇒(3), (3)⇒(1) as sketches are welcome.
A switch network is a set of queues served by servers. In every time slot each server can serve at most one queue, so a scheduler must pick a matching of queues to servers. Such systems model input-queued packet switches, crowdsourcing platforms that route job types to worker types, and wireless links with unknown channel quality. When the success probability of each queue–server link is unknown, the scheduler has to learn it from the services it observes while the queues are building up. This makes switch scheduling a multi-armed bandit problem in which the cost is not cumulative reward but queue length.
Krishnasamy, Sen, Johari and Shakkottai (arXiv:1604.06377, Operations Research 2021) measure a scheduler by its queue-regret: the expected difference between its queue lengths and those of a genie that knows the best matching. They show that the queue-regret has two regimes. In the late stage, once the queues regularly empty, it decays like (their Theorem 3, the subject of a sibling mission). In the early stage it grows like , as the regret of a classical bandit does, and the system is then effectively unstable. This mission is about the early stage, made precise in the paper's Theorem 8: in heavy traffic, where the arrival rates are close to the best service rates, every reasonable policy pays logarithmic queue-regret for a long time.
The lower-bound technique descends from Lai and Robbins (1985): a policy that does well on every instance must explore each sub-optimal link about times, a count obtained by a change of measure and the Bretagnolle–Huber inequality.
Queues are indexed by and servers by . In every slot , queue receives an arrival , and link offers a service . All of these are independent and i.i.d. over slots. Notation:
Assumption 1 asks that every queue have a unique best server and that the best servers of distinct queues be distinct. Assumption 2 is for every . Assumption 3 draws the initial queue vector from the stationary law of the genie queues.
A scheduler picks a matching , so queue is served by server . Its decision may use the past schedules, the services observed on the scheduled links, and private randomness. The queues evolve as . The genie always schedules and has queues . The queue-regret is . The schedule counts are .
A policy is -consistent () if on every instance for all and all , with a constant that may depend on the instance. The key constant is
where is the Bernoulli Kullback–Leibler divergence.
Fix , an -consistent policy and . There exist constants and , the same for every arrival vector , such that, with and :
Theorem 8 complements the late-stage lower bound. Together they show that queue-regret goes through a phase transition. Up to time of order , the queue-regret of any consistent policy grows like . Since the left end of the window does not move as while the right end grows like , the heavily loaded regime is exactly where learning costs are visible in queue lengths. The theorem also explains why algorithms designed for the late stage (Q-UCB, Q-ThS in the same paper) cannot avoid this early cost.
The formalization adds a machine-checked statement of a lower bound whose constants are pinned down precisely. In particular it states which quantities and may depend on (see below). Along the way it builds a reusable model of a learning switch scheduler: randomized, history-dependent policies, the coupled genie system and the stationary initial law. It also provides a Lai–Robbins-type count bound (Lemma 19) for matching bandits. The results are proved on paper in the held preprint (§9.2). To the best of the platform's records none of them has been formalized.
The obvious route to Theorem 8 is to bound the queue-regret below by the regret of the corresponding bandit. That fails, because queue-regret is not cumulative: an empty queue forgives past mistakes. The proof therefore needs the stationary start (Assumption 3), so that and the sub-optimal schedules show up as a drift (Lemma 22). This holds only up to a load term , which limits the window.
The count bound (Lemma 19) requires a change of measure between two instances that swap the best servers of two queues. It needs a chain rule for the KL divergence of adaptively collected observations, where the policy's own randomness must cancel. Neither the swapped instances nor the trajectory law are standard Mathlib objects.
Fin U and servers are Fin K, with and . is trivial, and for it is an empty minimum.Fin U ↪ Fin K.The source is the arXiv v4 preprint; the paper's proofs are in its §§8–9. Welcome contributions include the KL chain rule for adaptively scheduled Bernoulli observations, stationarity of the geometric law for the genie chain, and measurability of the trajectory.
An agent whose preferences change over time cannot simply optimize. Under non-exponential discounting, for instance hyperbolic or pseudo-exponential discount functions, a plan that is optimal today stops being optimal tomorrow, and a later self deviates from it. Strotz (1955) proposed that a sophisticated agent treat future selves as players in a game and look for a subgame-perfect equilibrium strategy instead. In discrete time this notion is unambiguous. In continuous time, Ekeland and Lazrak (2006) gave the first rigorous definition, through a first-order (derivative-type) condition, and nearly all later work on time-inconsistent stochastic control in continuous time uses it.
Huang and Zhou (2021) point out that this standard notion, here called a weak equilibrium, can admit strategies that the agent strictly wants to abandon over arbitrarily short intervals. They introduce a strong equilibrium, which rules out every profitable short deviation. For a controlled finite-state Markov chain they characterize both notions and prove that both exist under compactness. This mission formalizes that existence theorem together with the expansions and characterizations it rests on.
Let . A continuous-time Markov chain on is controlled through its generator , with -th row . A row must lie in
and an admissible set is fixed for each state. The control space is .
A payoff rate is paid at time difference when the chain is in state and uses row . The standing assumptions are that is continuous on and that, for every , is integrable in . The expected payoff is
For , the concatenation follows on and afterwards.
The first-order gain of a row in state is .
Suppose every is nonempty, convex and compact, is continuous on , and is concave. Then
If moreover is strictly concave and satisfies the and remainder conditions of Lemma 3.2, then
Theorem 3.3 is the general existence result of the paper. Theorem 3.1 and Proposition 3.2 give a way to find equilibria in a given model, but they do not say whether one exists. Remark 3.4 shows that without compactness of the , no equilibrium need exist. The strong half shows that the stricter concept is not empty in general: under strict concavity a strong equilibrium exists. Example 4.3 of the paper shows that weak equilibria need not be strong, so the two halves are different results.
The paper gives a proof, and none of it has been formalized. A formalization produces a checked equilibrium-existence theorem for a controlled continuous-time Markov chain. It also produces reusable small-time expansions of matrix-exponential payoffs. These expansions are shared by the paper's other results: the two-state example and the convergence of discrete-time equilibria.
The fixed-point step itself is routine once its hypotheses are in place. The work lies in the analysis that feeds it. First, the continuity of needs a limit passage under an infinite-horizon integral, which requires a uniform integrable bound on along a converging sequence of generators. Second, the step from a fixed point to a weak equilibrium goes through Theorem 3.1, whose hypothesis (3.3) is not among those of Theorem 3.3. Showing that without (3.3) is not one of the paper's numbered statements. Third, the strong half needs Proposition 3.2. Its proof treats deviations that agree with in the current state, which are felt only at second or higher order in , through the first order at which the chain can reach a state where the deviation differs. The obvious argument, comparing first-order terms only, says nothing in that case.
States are Fin N, so state of the paper is index . Rows are Fin N → ℝ and generators are Matrix (Fin N) (Fin N) ℝ with the entrywise topology. Expectations are not built from a Markov process. Under the law of given is the -th row of , so . Under the transition matrix is for and afterwards. Integrals are Bochner integrals over . The norm in (2.3) is the sup norm, which is equivalent because (2.3) quantifies over every . The liminf in the weak-equilibrium definition is encoded as "for every , eventually ". "Increasing" in (3.4) and (3.15) means nondecreasing.
Two hypotheses are added to the printed Theorem 3.3:
The shift bound (3.3) is deliberately not assumed in the weak half. No statement assumes integrability of a payoff; it follows from (2.3) because is a stochastic matrix. The time derivative in Lemma 3.2 is tied to by a derivative condition, and is meaningless otherwise. These choices rule out formalizations that are trivially true because an integral is junk or an admissible set is empty. Every hypothesis on ranges over only.
A complete development needs:
The matrix-exponential facts about generators are reusable beyond this mission. Contributions to any milestone are welcome, and so are lemmas on generators and .
Data-driven control asks for a controller computed directly from measured trajectories of an unknown system, without first identifying a model. When the measurements are corrupted by unknown process noise, many systems explain the same data, and a controller designed from the data alone is only trustworthy if it stabilizes every one of them. Van Waarde, Camlibel, Eising and Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) show that this robust design problem is an implication between two quadratic matrix inequalities (QMIs), and they develop matrix versions of Yakubovich's S-lemma and of Finsler's lemma to decide such implications by a linear matrix inequality (LMI).
Timeline:
All matrices are real. is the set of symmetric matrices; () means is symmetric positive semidefinite (definite), and means .
QMI solution sets. For partitioned with , ,
with and defined by "" and "". The generalized Schur complement is , with the Moore–Penrose pseudo-inverse, and is the class of with , and .
Data. The unknown system is with , . The measured data are and ; and are the first and last columns of . The unknown noise satisfies for a given . The systems compatible with the data form
and . The data are informative for quadratic stabilization (Definition 2.1) if some and satisfy for all .
Let be the -square matrix
For and data generated by the system:
(a) the data are informative if and only if with (5.5);
(b) if moreover and , the data are informative if and only if with (5.6);
(c) whenever (5.5) or (5.6) holds, satisfies the Lyapunov inequality with that and makes Schur stable for every .
The vector S-lemma, strict S-lemma and Finsler's lemma (Lemmas 4.1–4.3); the completion and lifting lemmas 4.4–4.5; the reduction of matrix inclusions to vector implications (Theorem 4.6); the matrix S-lemmas
(Theorems 4.7, 4.10–4.12, Corollary 4.13); and the three claims of §5.1 that put Theorem 5.1 in the form of Corollary 4.13: , the Lyapunov inequality is , and , .
Theorem 5.1(a) is an exact test, with no rank condition on the data and no Slater condition on the noise model, for the existence of one state-feedback gain with a common quadratic Lyapunov function that stabilizes every system consistent with noisy data. The test is a semidefinite feasibility problem in and returns the controller . It covers energy bounds, per-sample bounds, sample-covariance bounds, noise in a known subspace and exact data within one statement, and its matrix S-lemmas are the tools reused in the paper's further results (the reduced LMI and explicit gain of §5.2, Petersen's lemma in §4.5).
None of these results has a machine-checked proof. Mathlib has the Loewner order, positive (semi)definiteness and spectral theory of symmetric matrices, but no S-lemma, no Finsler lemma, no Moore–Penrose pseudo-inverse for matrices and no theory of QMI solution sets. A formalization would supply these as reusable linear-algebra results and would certify the design rule .
The "if" directions are direct computations: multiply out a Schur complement. The difficulty is in the "only if" directions. The S-lemma's converse relies on the hidden convexity of the joint range of two quadratic forms (Dines' theorem), which is not a consequence of finite-dimensional convex duality alone. Passing from matrices to vectors requires Lemma 4.5, which builds a full matrix solution of the QMI from one vector; it uses the pseudo-inverse factorization of and fails without . In Theorem 4.11 the existence of the margin comes from a compactness argument on an unbounded solution set, after splitting off the kernel of . The obvious approach, applying the strict matrix S-lemma (Theorem 4.10) directly, does not work because is only semidefinite in the noise models of interest.
Matrices are Matrix ι ι ℝ over finite index types; a matrix in is indexed by ι ⊕ κ, and block matrices are Matrix.fromBlocks / Matrix.fromRows. and are Mathlib's PosSemidef and PosDef, which include symmetry, as the paper's §1.1 convention does. The pseudo-inverse is defined as the unique matrix satisfying the four Penrose conditions, not Matrix.inv, which returns on singular matrices. "Stabilizing gain for all of " is stated as the Lyapunov inequality with the LMI's together with .
The following are added or made explicit:
The goal adds no hypothesis . A formalization in which may be empty, or in which the pseudo-inverse is a junk value, would be trivial or false, and the definitions rule both out.
Contributions are welcome for the pseudo-inverse API (existence, uniqueness, identities), the S-lemma and Finsler's lemma (reusable beyond this mission), and the Schur-complement factorizations (3.2)–(3.4). Platform items ConvexOptimization.s_procedure (inhomogeneous S-procedure) and ConvexOptimization.field_of_values_psd_witness (Dines) are natural proof tools for Lemma 4.1.
In a repeated game, players who do not know the payoff structure can still learn by reinforcement: each player keeps a running score for every action, the cumulative payoff that action would have earned, and plays a mixed strategy that favours actions with high scores. Turning scores into mixed strategies through a regularized best response (maximize score minus a convex penalty) gives a family of dynamics that includes exponential weights and the replicator dynamics (entropic penalty), and also the projection dynamics (quadratic penalty). The same scheme is the continuous-time counterpart of online mirror descent and dual averaging in online optimization.
For the replicator dynamics, the standard folk results of evolutionary game theory say that Nash equilibria are stationary, that limits of interior orbits are Nash equilibria, that Lyapunov stable states are Nash equilibria, and that strict equilibria are asymptotically stable (Weibull 1995; Hofbauer–Sigmund 1998). Mertikopoulos and Sandholm (arXiv:1407.6267v2, Math. Oper. Res. 41(4), 2016) show that all four results survive for the whole family. For steep, decomposable penalties several of them were known (Coucheney–Gaujal–Mertikopoulos 2015). The new part is the nonsteep case, where mixed strategies can hit the boundary of the simplex and the induced dynamics on strategies are no longer well defined.
A finite game has a finite set of players. Player has a finite nonempty set of pure strategies and a payoff function . A mixed profile is , and is player 's expected payoff when the players randomize independently. The payoff vector is , the payoff of pure strategy against .
A penalty function on a simplex (Definition 2.1) is a function that is continuous, smooth on the relative interior of every face, and -strongly convex:
Steepness (gradients blowing up at the boundary) is not required. Its choice map is . Every player has a penalty function with constant .
The reinforcement learning dynamics (RL) are
and an orbit is a pair , , satisfying them. A Nash equilibrium is a profile with for every and every mixed . It is strict if the inequality is strict for every .
Because (RL) lives in the space of scores and is neither injective nor surjective, stability is defined on the trajectories of play (Definition 5.1):
for every finite game and every choice of penalty functions , steep or not.
Theorem 5.2, Parts I–III (stationary Nash and in ; limits of orbits and Lyapunov stable states are Nash), Proposition 5.3, Proposition 3.1 (global existence and uniqueness of orbits) and Proposition A.1(i)–(ii).
Theorem 5.2 says that, as far as the qualitative long-run behaviour is concerned, the whole class of regularized reinforcement dynamics behaves like the replicator dynamics. Part IV is the positive half: strict equilibria are robust attractors of learning. This is used to justify equilibrium selection by learning, and Proposition 5.4 (not part of this mission) builds the rates of convergence, including convergence in finite time for nonsteep penalties, on top of it.
The result is proved in the paper; none of it is formalized. A Lean development would provide a reusable layer of game-theoretic learning dynamics: penalty functions without steepness, choice maps as regularized argmax, the Fenchel coupling and the one-sided Bregman divergence on the simplex. Two companion missions on the same paper use the same layer, for the extinction of dominated strategies and for time averages in zero-sum games. As far as is known, the stability theory of Section 5 has no machine-checked proof even for the replicator dynamics.
The obvious argument would be a Lyapunov argument for the induced dynamics on , as for the replicator equation. For nonsteep penalties these dynamics are not well defined: orbits reach the boundary and is not invertible there. The proof works in the dual space instead, where the natural Lyapunov candidate is the Fenchel coupling . The coupling is not differentiable along the orbit in the usual sense, and its sublevel sets in score space must be related to genuine neighbourhoods of in . That needs the Bregman divergence with one-sided derivatives at boundary points and its continuity across faces of different dimension (Proposition C.2(iii)). A second obstacle is that the coupling does not strictly decrease when the maximizer sits at the vertex. The page states a strict inequality there, which fails for nonsteep penalties, so the argument has to be run with the weak inequality and a first-exit-time argument.
agt_games vocabulary: AGT.IsLottery, AGT.IsMixedProfile, AGT.expectedPayoff, and AGT.IsMixedNash for (5.1). Players form a Fintype ι, and actions are A k with Fintype and DecidableEq.IsPenalty h K, Definition 2.1 with the Euclidean norm in (2.5) and smoothness along curves inside the relative interiors of faces. There is no steepness.IsChoice h y x, never a chosen argmax.IsRLOrbit u h y x, the differential form (3.1) with one-sided derivatives at . Statements quantify over orbits and never construct one.Trivializing encodings are excluded. Q is not a chosen maximizer that could be chosen badly. Orbit hypotheses are not vacuous: a verification file exhibits an orbit and a strict equilibrium together with a penalty function. Steepness is not added to the hypotheses. The conclusion is genuine convergence together with Lyapunov stability, not a or a stability-only statement. Proofs of any milestone are welcome. The conjugate and Bregman layer (Appendix C), the regularized-argmax lemmas (Appendix A) and the well-posedness of (RL) (Proposition 3.1) are reusable beyond this mission.
Two-stage stochastic linear programs model decisions taken in two steps: a first-stage decision is fixed before an uncertain parameter is observed, and a second-stage (recourse) decision adapts to afterwards. They underlie capacity planning, inventory and network design. In practice the distribution of is known only through samples . Distributionally robust optimization replaces the unknown distribution by the worst case over an ambiguity set; a popular choice is a Wasserstein ball around the empirical distribution, because it contains the true distribution with high probability and yields out-of-sample guarantees (Mohajerin Esfahani and Kuhn, 2018).
Hanasusanto and Kuhn (arXiv:1609.07505, Operations Research 66(3), 2018) study when the resulting two-stage problem can be solved exactly. Section 3 of their paper gives a copositive reformulation for the 2-Wasserstein ball (the subject of a companion mission). Section 4, the subject of this mission, shows that when the uncertainty enters only the constraints of the recourse problem and the ball is a 1-Wasserstein ball with a polyhedral reference distance, the whole problem is a linear program.
Let and be the first-stage cost and feasible set, the second-stage cost, the recourse matrix, and , affine functions of . The recourse value at is
The uncertainty affects only the constraints (in the paper's notation, ), and there is no support constraint: . The problem has sufficiently expensive recourse if some satisfies .
For scaling parameters the reference distance is with
Moving a unit of mass in the positive direction of coordinate costs , in the negative direction . The 1-Wasserstein ball consists of the probability measures on whose optimal transport cost to under is at most . The worst-case expectation and the two-stage problem (1) are
The dual norm of (31) is .
For and every , equals the optimal value of the linear program
and consequently problem (1) has the optimal value of (32) minimized jointly over and the other variables with added to the objective.
Theorem 6 shows that the two-stage distributionally robust linear program over a 1-Wasserstein ball, which is a priori an optimization over infinitely many distributions, has a linear-programming reformulation with blocks of variables and constraints. It covers distributionally robust least-absolute-deviation regression (Example 2 of the paper), where the reformulation becomes the empirical loss plus a dual-norm regularizer, and it contrasts with the paper's Theorem 7, which shows that for -norm reference distances with the same problem is NP-hard.
The result is proved in the paper; there is no machine-checked proof. A formalization adds a verified chain from the measure-theoretic worst-case expectation to a finite linear program, including the conventions the paper leaves implicit: the extended-real values ( may be , and (32) may then be infeasible), the restriction , and the first-stage cost in the objective.
Each step of the proof is classical, but the chain crosses several regimes. Theorem 1 is a Wasserstein strong duality result, and here it is applied to a loss that is convex, possibly on part of , and not upper semicontinuous, with a cost that is not symmetric; the standard published duality theorems assume an upper semicontinuous real-valued loss or a metric. The passage to (33) interchanges a supremum over with an infimum over the dual-norm ball and must handle the case where the dual recourse polyhedron is unbounded. Finally, every equivalence must hold in the extended reals: an argument that tacitly assumes finiteness proves a statement that fails exactly when the dual polyhedron has a recession direction.
Vectors are Fin n → ℝ, samples are ξhat : Fin I → (Fin K → ℝ) with , and carries its product (Borel) σ-algebra. and are affine maps. The transport cost is the platform definition RWPI.SqrtLasso.transportCost (couplings with first marginal , second ), the empirical distribution is WassersteinDRO.Duality.empiricalDistribution, and expectations of the extended-real recourse value use WassersteinDRO.Duality.erealExpectation (value whenever the positive part has infinite integral). Every optimal value is an extended-real infimum or supremum over its feasible set; no Bochner integral and no real-valued sInf/sSup is used.
Conventions made explicit, with reasons:
A formalization in which is defined by (6), (33) or (32), in which the gauge is secretly symmetric, or in which expectations are Bochner integrals (zero for non-integrable functions) would make the goal trivial or different; the definitions here exclude each of these.
A complete development needs Wasserstein strong duality for a lower semicontinuous loss and cost (with a disintegration of couplings to pass to the moment problem (5)), LP strong duality and Farkas' lemma in the extended-real form, and a minimax interchange over a compact dual-norm ball. Wasserstein duality for general costs and extended-real LP duality are reusable well beyond this mission; contributions of either are welcome.
Linear-quadratic (LQ) control is the setting in which stochastic optimal control has a closed-form answer: the optimal control is a linear feedback of the state, and the feedback gain comes from a Riccati differential equation. In the mean-field version, the expectation of the state and of the control appear in the dynamics and in the cost. Mean-field SDEs go back to Kac (1956) and McKean (1966) as models of interacting particle systems. A cost containing can penalize the variance of the state, which is what is wanted when the optimal state should not be too sensitive to the noise (mean–variance portfolio selection is the standard example). With such a cost the problem is no longer a classical LQ problem: the weights on may be negative definite, and the cost is not an expectation of a function of the state path, so the classical Riccati theory does not apply as it stands.
J. Yong (SIAM J. Control Optim. 51(4), 2013, pp. 2809–2838) solved the problem with deterministic coefficients. He derives the optimality system, a linear mean-field forward–backward SDE, and decouples it with two Riccati equations. One governs the deviation , the other the mean . The optimal control is then an explicit state feedback.
Timeline:
Let be a complete probability space carrying a one-dimensional standard Brownian motion , and let be the natural filtration of augmented by the -null sets. Fix a horizon . An admissible control is an -progressively measurable with ; the set of them is . For the state solves
with deterministic matrix-valued coefficients. The cost is
Problem (MF-LQ): minimize over . The assumptions are:
The weights themselves need not be semidefinite.
With and , the two Riccati equations are
with . Write and .
Under (H1)–(H2), (4.8) and (4.9) have unique solutions and on . The closed-loop system obtained by substituting
into the state equation has a unique solution . With and the explicit , the 4-tuple solves the optimality system, and is optimal. Moreover
The Woodbury identity used on p. 2826 is already proved on the platform (FamousTheorems.woodbury_identity) and is referenced.
The result. Theorem 4.1 reduces a mean-field stochastic control problem, whose state law enters the dynamics, to two matrix ODEs. The optimal control is computable offline: integrate and backward, then feed back the state and its mean. The value is explicit, so cost comparisons between the mean-field problem and its classical counterpart become comparisons between Riccati solutions; §5 of the paper does exactly this for variance-penalized costs. When all barred coefficients vanish, and the classical stochastic LQ feedback is recovered.
Formalizing it. The result is proved, not open; this mission formalizes the known proof. No continuous-time stochastic LQ theorem exists on the platform. The mission builds on the published stochastic calculus of Peng1990.SMP.Stochastic (Itô integrals, SDE and BSDE solutions, ) and adds a reusable mean-field LQ setting, matrix Riccati equations in integral form, and a verification theorem. None of the statements has a machine-checked proof yet.
The Riccati equations are nonlinear matrix ODEs with only coefficients. Local existence is routine, but global existence on needs an a priori bound, which a local fixed-point argument does not give. The bound comes from the control interpretation of the equation, and it requires semidefiniteness of . The second equation contains , and its quadratic term is only controlled when , which in turn needs . Its "state weight" is semidefinite only through the identity of milestone 7, even though itself may be negative definite. On the stochastic side, the verification step (milestone 9) and the duality arguments of Theorems 3.1–3.2 apply Itô's product rule to and to for processes driven by the same Brownian motion, with an absolutely continuous (not differentiable) . Itô's formula is not yet available on the platform: it is the open goal EthierKurtz.ito_formula. Existence in Proposition 2.8 needs a minimizer of a coercive continuous quadratic functional on the Hilbert space .
States are Fin n → ℝ, controls Fin m → ℝ, time is ℝ≥0, and the horizon satisfies . The probability space is complete. is Peng1990.SMP.IsStdBrownian with one coordinate, and is ReflectedBSDE.Existence.augmentedFiltration. is the Bochner integral of the solution itself. Every mean-field term is a closure over the process being solved for, never a free deterministic input. Solutions of the forward and backward equations are the published SolvesSDE/SolvesBSDE notions: progressive, square-integrable, with the integral identity at each almost surely. Controls and -components are identified up to -null sets.
Other conventions:
Matrix.inv is a true inverse. For (4.9), follows from (H2) once .A formalization in which the mean is an independent input, or in which a Riccati "solution" may use the junk value of a singular inverse, would trivialize the problem. Both are ruled out by the definitions above. A sorry-free sanity file shows that (H1)–(H2) hold for data with negative definite, and that the Riccati class is non-empty.
Contributions are welcome on all of the following:
Matrix approximation replaces a large or complicated matrix with a random matrix that is easier to store or compute. Averaging independent realizations improves accuracy while retaining the structure of each realization. Examples in Tropp's monograph include sparse approximations and randomized matrix products. The practical question is how the number of samples, the size of one sample, and its second moment control the spectral norm error. Tropp, §6.2
The book proves a matrix Bernstein inequality in Theorem 6.1.1, then applies it to an empirical matrix average in Corollary 6.2.1. Theorem 6.1.1 is already posed as TroppMatrixConcentration.matrix_bernstein on Prove2Me and is currently Open. This mission records the application with its own hypotheses and constants. The capstone concerns the estimator that a reader would construct, rather than a sum of abstract centered summands. Tropp, §§6.1–6.2
Let be a fixed complex matrix. A sample matrix has the same size, has expectation , and has spectral norm at most almost surely. The equality makes one sample an unbiased estimate of . The almost-sure bound limits the size of every sample except on a probability-zero set. The dimensions are positive integers, and is a positive sample count.
Take independent copies with the distribution of . Their matrix sampling estimator is
For any rectangular matrix , denotes its conjugate transpose and its spectral norm. The per-sample second moment is
Both terms matter for a rectangular matrix: and act on different coordinate spaces. All expectations of matrices are entrywise expectations, represented by Bochner integrals in Lean. The almost-sure norm bound guarantees the moments used here are finite. Tropp, equations (6.2.4)–(6.2.6)
Corollary 6.2.1 gives an expectation estimate and a tail estimate for the same estimator. For every real ,
The goal includes both bounds. The expectation estimate controls average error; the tail estimate controls the chance of an error above a chosen threshold. The dimension enters only through in the expectation bound and the factor in the tail bound. These are the book's constants, including the factors and in the linear terms. Tropp, Corollary 6.2.1, p. 81
The milestone list follows Corollary 6.1.2 for uncentered summands, the bound , and the variance estimate . Equation (6.2.7) is a companion: a stated lower bound on implies for . Tropp, pp. 77, 82
The result turns a bound on one random matrix into a quantitative guarantee for an empirical approximation. It lets a user choose a sample count for a target error and evaluate both average error and failure probability. The same framework is instantiated later in the monograph for matrix sparsification and multiplication; those applications depend on controlling and for their particular sampling laws. Tropp, §§6.2–6.4
This is a known mathematical result proved in the book. Its Lean statement is an open formalization target. The mission adds a reusable empirical-mean definition and application statements built on the already published matrix spectral norm and rectangular second-moment definitions. A proof of the general matrix Bernstein theorem remains separate; the mission can draw on it when that platform theorem is proved.
The estimator error is a centered sum, but the sampling assumptions are given for an uncentered random matrix . Bounding the centered summands changes the uniform bound from to . The variance parameter must be related to the second moment of one uncentered sample, with the correct scaling. Dropping the common-distribution condition would leave no relation between the samples' second moments and . Applying scalar concentration to entries would not directly give the stated spectral norm bound or its dimension dependence. Tropp, proof of Corollary 6.2.1, p. 82
Matrices are Matrix (Fin d₁) (Fin d₂) ℂ. The spectral norm and rectSecondMoment are imported from tc's published TroppMatrixConcentration definitions. An arbitrary probability space carries a measurable reference matrix and a finite family ; iIndepFun expresses independence and IdentDistrib expresses equality in law with . The estimator is the finite sum scaled by . No particular sampling scheme or deterministic choice of is fixed: the formal goal requires only the source's unbiasedness and boundedness conditions.
The Lean statements explicitly require , , measurability, and the almost-sure form of . These make the logarithm and inverse sample count meaningful and make the random matrix laws well behaved. For the uncentered Bernstein corollary, integrability of each is explicit because a bounded deviation from an unspecified mean alone does not establish that the mean exists. The goal also asserts integrability of its error norm, preventing a Bochner integral from silently taking Lean's default value for a nonintegrable function. The bound on supplies that integrability. When the denominator in a tail formula is zero, the displayed total real division gives a loose bound at the degenerate case; the source's probabilistic claim remains valid.
Contributions that formalize the centered-summand calculation, the variance estimate, or the transfer from the general matrix Bernstein theorem are within scope. The imported matrix and probability definitions are reusable in other matrix concentration missions. The local empirical-mean definition is reusable whenever a matrix estimator averages finitely many random samples.
A firm selling a fixed stock of a perishable product over a finite season must set prices without knowing how demand responds to them. Online retail and travel platforms often see a customer's segment before quoting a price, so they can price-discriminate across consumer types. Learning a separate demand curve for each type, however, seems to cost more exploration as the number of types grows. Chen and Gallego (arXiv:1812.09234v3, 2021; Mathematics of Operations Research, 2022) give a learning algorithm whose regret does not depend on the number of types. Their key step is to learn a single scalar first: the shadow price of inventory.
Earlier work on the single-type problem frames the question. Besbes and Zeevi (Operations Research, 2009) defined the regret against the fluid benchmark and showed that no policy can achieve regret decaying faster than . Wang, Deng and Ye (Operations Research, 2014) gave a single-product algorithm whose regret matches this rate up to logarithmic factors. Chen and Gallego extend the rate to types with one inventory constraint.
There are consumer types, a season and an inventory . When the firm charges price to type , type- consumers arrive at rate . Prices range over , where is a choke price with . Assumption 1 asks that each be strictly decreasing, bounded and Lipschitz, and that the revenue rate be Lipschitz and twice differentiable, with .
The fluid problem (2) maximizes subject to . Its optimal value is . Its dual is one-dimensional. With
the dual optimum is , and the optimal fluid prices are the constants .
In the -th system demand and inventory scale together: type arrives as a Poisson process with rate , and the inventory is . The firm does not know . It knows , , , the constants of Assumption 1 and, by Assumption 2, intervals and that contain every and . A policy has expected revenue , and its regret is
Algorithm 1, the primal-dual learning algorithm, runs phases of shrinking lengths . In each learning phase it tests a price grid inside the current interval estimators of every . It then minimizes an empirical dual function on a grid of and re-centres the interval estimators of and . In the last phase it either charges a marked-up price (sufficient capacity), or tests two prices and interpolates between them so that total sales end close to (insufficient capacity). Its tuning depends on a constant .
For every one can choose and a constant , independent of , such that
Theorem 1 states that personalized pricing for types under a shared inventory constraint is learnable at the single-type rate , up to logarithms, with a constant independent of . Combined with the Besbes–Zeevi lower bound, the algorithm is rate-optimal. Learning the scalar shadow price , instead of the joint optimum of an -dimensional problem, is what avoids the curse of dimensionality.
The result is proved in the paper; no machine-checked version exists. A formalization would add to the platform a multi-type Poisson pricing model with stock-outs, the one-dimensional Lagrangian dual of the fluid revenue-management problem, an exactly specified multi-phase learning algorithm, and reusable Poisson deviation lemmas. Lemmas 1, 2, 9 and 10 and Proposition 1 can be proved independently of the probabilistic analysis.
The obvious argument estimates every directly and charges the estimate. With interval estimators of width this loses revenue of order per unit time when the inventory constraint binds (), because is then not the unconstrained maximizer of . The paper's (11) and (19) show the loss. The bound requires steering the total sales to within of the inventory, which is Lemma 8, and a second-order expansion of the revenue around that uses the first-order condition .
Formally, a further difficulty is the closed loop: the prices of a phase depend on the counts of earlier phases, and the counts are Poisson only conditionally, through the random time change .
All declarations live in the namespace PrimalDualPricing.Regret. Printed page numbers equal PDF page numbers in the cited preprint.
Fin M. Each satisfies Assumption 1 on and is otherwise any extension with ; the last-phase prices and can leave . encodes the choke price. and are fields carrying their optimality properties.IsPoissonProcess) with right-continuous, jointly measurable paths. The inventory of the -th system is units, and nothing is sold after the stock-out. Lemmas 6–8 use the uncapped sales of the paper's modified system (§4).A formalization that lets the policy read the true demand, measures regret against anything other than , ignores the stock-out in , or assumes the high-probability events of Lemma 5 would trivialize the goal; none of these is done here.
Contributions to the reusable parts are welcome: Poisson tails, the envelope theorem for , and the time-change construction of policy-driven Poisson sales.
In online learning with bandit feedback, the learner chooses one action and sees only that action's loss. This is the information pattern of sequential trials in which testing one option does not reveal the outcomes of the others. The learner must keep its cumulative loss close to that of a good fixed action while learning which actions are good. A full-information method can update from every arm's loss each round; here the unseen losses have to be handled through the observations the learner actually receives. Chapter 9 of Orabona's text develops this distinction for multi-armed bandits.
Two environments are treated in the chapter. With an oblivious adversary, all losses are fixed before play, although the learner does not know them. With a stochastic environment, each arm has a fixed loss distribution and new losses are drawn across rounds. An algorithm with a guarantee in both environments does not need to be told which generated its data. Theorem 9.17 gives such a pair of guarantees for the FTRL version of Tsallis-INF, using the precise constants stated in the pinned version of the book.
There are arms and rounds, numbered . In round , the learner forms a probability vector on the simplex , draws an arm with probability of choosing , and observes only . The loss of an unchosen arm is not revealed. For an oblivious adversary, the entire table is deterministic and the expectation is over the learner's draws.
Algorithm 9.6 uses the importance-weighted estimate if , and otherwise. Its Tsallis-INF FTRL prediction minimizes, over ,
The minimizer has positive coordinates. Thus each denominator used by the estimator is positive. In the stochastic environment, arm has mean ; if is a best arm, its gap is . The pull count is the number of rounds through in which arm is selected. Stochastic pseudo-regret compares the learner's expected loss with , the expected loss of always playing the best arm.
The mission's main theorem is the adversarial claim of Theorem 9.17, p. 165. For every fixed comparator arm and losses in ,
Taking to be the best arm in the fixed loss table yields the stated adversarial regret bound. The companion item formalizes the second claim of the same theorem: if the losses are stochastic with a unique best arm and , then
The milestone list contains the chapter's pseudo-regret decomposition (Lemma 9.10), its sub-Gaussian sample-mean bound (Corollary 9.9, reused from an existing formal statement), and the probability-sensitive Tsallis-INF inequality (9.8). These are distinct mathematical claims rather than alternate names for the final bound.
The adversarial bound grows like and remains valid for any fixed bounded loss table. The stochastic bound instead measures the difficulty of distinguishing arms through the positive gaps and grows logarithmically with the horizon for fixed gaps. Both refer to the same FTRL update and the same importance-weighted estimator. The finite-horizon constants and are part of the target, not unspecified factors hidden in asymptotic notation.
Both claims are proved in the book. The work here is to give their hypotheses, random experiment, and algorithm a machine-checkable Lean interface, then formalize the known arguments. At this drafting stage the theorem bodies are open Lean problems; a successful build checks that their statements are well formed, not that the regret bounds have been proved. The resulting finite-history bandit protocol and stochastic pseudo-regret definitions can also support other loss-based bandit algorithms. The existing formalized sub-Gaussian tail bound can be reused for concentration results elsewhere in the chapter.
The learner observes only one coordinate, while regret is measured against losses across all arms. The importance-weighted estimate corrects the missing observations in expectation, but its size can grow when a selected arm has small probability. Consequently, a bound based only on a uniform estimate of its magnitude loses the probability dependence needed for the theorem's constants. The stochastic claim adds another difficulty: the learner's choices depend on past observed losses, so a current loss must be related to a random pull count without letting the choice depend on that current loss.
There are two tempting but invalid shortcuts. Permitting to inspect would change the bandit protocol, and taking an expectation under an arbitrary path measure would no longer describe the arm draws of Algorithm 9.6. The formal statements tie each prediction to its FTRL objective and each path probability to the predictions made along that history.
Arms are Fin d; the main theorem permits , where both its regret and bound are zero. Rounds retain the book's indexing. A finite path has a dummy coordinate zero, fixed to an arbitrary anchor arm; this coordinate is never played or scored. The adversarial losses are a fixed table, selected before any draw. A path has probability equal to the product of the algorithm's conditional arm probabilities, and regret against a fixed arm is a finite weighted sum over paths. The FTRL run predicate requires simplex membership, strict positivity, minimization against every simplex point, and dependence only on past arm choices. The last two properties specify the intended update on every possible history.
The stochastic model first samples a loss table from a probability measure and then draws an arm path conditionally using the same Algorithm 9.6. Current-round loss vectors are independent across rounds, while coordinates within one round need not be independent. Each arm has the same mean in every round. The policy is a measurable function of the observed history (past arms and their losses); its expected loss is explicitly integrable. Loss bounds are imposed on every outcome in the chosen sample space, which can be taken as the support of bounded distributions. The stochastic statement adds to make the logarithmic formula's domain explicit, and the unique-best-arm assumption ensures every denominator in the displayed sum is positive. Lemma 9.10 also spells out the integrability of its means and pull counts.
The development needs finite probability laws, real integrals, simplex geometry, and properties of the square-root regularizer. The independent tail bound for sample means is already available as a referenced theorem. Contributions that establish existence and interiority of the FTRL minimizer, the normalization of the path law, or the stated regret inequalities fit this scope. A choice rule that sees the current loss, a path law unrelated to , or a zero integrability default does not satisfy the intended bandit model.
In stochastic programming the objective is an expectation that cannot be evaluated, and an algorithm sees only noisy gradients drawn from a stochastic first-order oracle. Stochastic gradient descent and its relatives are the standard methods. For convex the optimal rate is known: Lan's accelerated stochastic approximation method (Lan, Math. Program. 2012) reaches an expected optimality gap of order after oracle calls. For smooth nonconvex , Ghadimi and Lan's randomized stochastic gradient (RSG) method (arXiv:1309.5549, SIAM J. Optim. 2013) bounds the expected squared gradient norm at a randomly chosen iterate, but it is only nearly optimal when happens to be convex.
Saeed Ghadimi and Guanghui Lan (arXiv:1310.3787v1, 2013; Mathematical Programming 156, 2016) combined the two lines: the randomized stochastic accelerated gradient (RSAG) method has a guarantee for nonconvex problems, and with suitable step sizes it attains the optimal rate on convex ones. This mission formalizes that result, Theorem 3 of the paper, together with the steps of its proof in §3.1.
Let be differentiable with Lipschitz gradient: for all , with . Gradients are available only through a stochastic oracle: at its -th call, with input , it returns , where are random variables on a probability space and is jointly measurable.
Algorithm 3 (RSAG). The inputs are , step sizes , for , , , an iteration limit , and a probability mass function . A termination index with is drawn first, independently of the noise. With , for ,
and the method stops at and outputs . The oracle error is .
Assumption 1 asks that the oracle be unbiased, , with variance . The paper does not require the to be independent.
The weights are , , and for a horizon
Fix . The expectations are taken over and .
a) If is bounded below with , for , and (3.4), then
b) If is convex with a minimizer , is nonincreasing (2.10), and (3.6), and (3.7), then
The goal keeps every printed constant and leaves the step sizes free. Corollary 3 specializes them; it is not part of this mission.
Part a): the quadratic bound (2.1) (already proved on the platform); a pathwise one-step inequality for (p. 16); a stochastic version of (2.17) bounding ; the summed inequality with martingale terms (pp. 16–17); its expectation (p. 17); the identity expressing as a -weighted average (p. 17); Theorem 3 a). Part b): Lemma 1 (p. 4); the convexity bound (2.21); (3.10) with a sign corrected; the stochastic version of (2.22); (3.11); its two consequences at (p. 18); the weighting identity for (p. 18); Theorem 3 b).
The result. Theorem 3 gives one stochastic first-order method with two guarantees. On a nonconvex problem it finds an approximate stationary point with an explicit bound on . On a convex problem its optimality gap matches the lower bound for stochastic convex optimization, which the RSG method does not. The method does not need to know which case it is in; only the step-size policy changes. Later work on accelerated and variance-reduced methods for nonconvex stochastic problems builds on the same analysis, and Theorem 4 of the paper extends it to composite problems with mini-batches.
Formalizing it. The result is proved in the paper and, as far as we know, has not been machine-checked. A formal proof would check the bookkeeping that a reader usually takes on trust: the nested sums in and , the conditional-expectation arguments that make a martingale difference sequence, and the passage from fixed horizons to the random output . The printed proof has small errors (see Formalization scope), so the formal statements record the corrected forms.
The deterministic analysis of the AG method (Theorem 1) bounds along a single trajectory. In the stochastic case the same chain produces cross terms and . These cross terms do not vanish pathwise, and the variance terms come with coefficients involving that grow backwards in time. The obvious argument would take expectations termwise. It fails unless one shows that each cross-term coefficient is measurable with respect to the past, so that its product with has zero mean under conditional unbiasedness. This also requires square-integrability of every iterate, which the hypotheses do not state and which has to be established by induction. A second difficulty is the random output: the bound is on , an integral over and the noise jointly, so the independence of from the noise has to be used explicitly.
EuclideanSpace ℝ (Fin n) (the published GhadimiLan.RSG.E n). is the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth Ψ g LΨ, with , and .GhadimiLan.RSG.AssumptionA1 applied to the middle points: for a filtration to which the noise is adapted, a.s. and . This conditional form is what the paper's martingale-difference step uses. It holds when the are independent, and it allows dependent noise, as the paper does.The following versions would make the goal trivial and are excluded: a deterministic oracle ( hard-wired), fixed to , an oracle not tied to , and an unconditional unbiasedness hypothesis too weak to support the martingale step.
A complete development needs conditional expectations of vector-valued random variables, square-integrability of the iterates, and the independence calculus for the random index. These parts are reusable for the companion RSG and mini-batch RSAG missions. Contributions are welcome on any milestone. The pathwise milestones (one-step bound, (2.17), (2.21), (2.22), (3.10)) need no probability theory.
The simplex method for linear programming moves from vertex to vertex along the edges of a polyhedron. A lower bound on the number of pivots of any edge-following method is the graph diameter of the feasible polyhedron: the largest number of edges needed to connect two of its vertices. Whether this diameter is bounded by a polynomial in the dimension and the number of facets is the polynomial Hirsch conjecture, open since the 1950s. The original Hirsch conjecture, , was refuted for unbounded polyhedra by Klee and Walkup (1967) and for bounded ones by Santos (2012) (doi:10.4007/annals.2012.176.1.7).
Timeline.
A polyhedron is the set of solutions of finitely many linear inequalities,
It need not be bounded. A vertex of is a point for which some half-space satisfies , equivalently an extreme point of . Two vertices are adjacent when for some half-space ; the segment is then an edge. A path of length is a sequence of vertices with consecutive vertices adjacent, is the least such , and the diameter is over pairs of vertices. A -polyhedron is a -dimensional polyhedron with facets, and
the maximum taken over bounded and unbounded polyhedra alike. All logarithms are to base 2.
The goal fixes no constant beyond the paper's own exponent and leaves no case of , or boundedness open.
The result. The bound is never larger than the Kalai–Kleitman bound. It equals the true value in dimensions 1 and 2, and it depends on only through the Hirsch quantity . Since , it is also symmetric under linear-programming duality, which exchanges the roles of and . For fixed it is polynomial in . It applies to the unbounded feasible regions that arise in practice in linear programming.
Formalizing it. The theorem has been proved since 2014. The platform has a proof of the bounded case only: Hirsch.todd_bound assumes , a nonempty interior and Bornology.IsBounded. This mission's goal extends it to all polyhedra, bounded or not, and to . That is the statement the paper proves, and the one an analysis of the simplex method on unbounded feasible regions needs. The unbounded form of Lemma 1 and the common-facet bound are open on the platform as items of the Kalai–Kleitman series and are reused here. Klee's unbounded three-dimensional bound has no formal proof on the platform: the published Hirsch.klee_three_dimensional_bound and Hirsch.dimension_three_bound cover bounded polyhedra only. The bounded recursion Hirsch.kalai_kleitman_recursion and the bounded facet reduction Hirsch.facet_reduction are proved and may serve as models.
Two steps are hard. The first is the unbounded case. Statements proved for polytopes do not transfer directly, because an unbounded polyhedron may have no vertices or a single one, unbounded edges (rays) that are not edges of the graph, and redundant or implicit-equality rows. Each geometric milestone must hold for these. The second is Klee's three-dimensional bound, which the paper cites without proof. Assuming boundedness to apply the published polytope versions is ruled out: Klee and Walkup showed that unbounded and bounded diameters differ from dimension four on, so the unbounded case carries content of its own. The arithmetic milestones are elementary but sensitive to edge values of and the real power.
All statements use the published definitions Hirsch.Hpoly, Hirsch.Adj and Hirsch.DiamLE (Hirsch_model). Vertices are Set.extremePoints ℝ. DiamLE P B says that any two extreme points are joined by a walk of exactly steps, each step staying put or crossing an edge. So the bound includes connectivity of the vertex–edge graph.
DiamLE (Hpoly a b) B. This ranges over all polyhedra given by inequalities in , including lower-dimensional, empty and redundant ones. It is equivalent to the paper's statement: a lower-dimensional polyhedron of dimension with facets has .Real.logb 2 and the power is Real.rpow. A distance is at most exactly when it is at most the floor , abbreviated toddBound d n in the milestone on the ten cases. The clause is a separate conjunct, because in Real.rpow.Trivializing encodings are excluded: no Bornology.IsBounded hypothesis; no definition of by sSup over , which would be on unbounded families; no use of Hirsch.gdist, which is when no walk exists; and no dropping of the clause.
Contributions are welcome on every milestone. A complete development needs facial structure of unbounded polyhedra (facets as polyhedra one dimension lower, tight rows at vertices), the relaxation argument of Lemma 1, Klee's three-dimensional argument, and real-power and logarithm estimates. The facet machinery and Klee's bound are reusable for any diameter result on unbounded polyhedra.
Many graph-colouring questions ask whether a proper colouring can be produced indirectly, from local data, instead of being assigned vertex by vertex. In the 1-2-3 Conjecture, the colours are produced by weighting the edges of a graph and colouring each vertex with the sum of the weights at it. Karoński, Łuczak and Thomason asked in 2004 whether weights from always suffice (J. Combin. Theory Ser. B 91 (2004)). The question started as a local version of the irregularity strength problem, where all vertices, not only adjacent ones, must receive different sums. It became one of the most studied problems on graph labellings. Surveys: Seamone (arXiv:1211.5122) and Grytczuk (DOI 10.1016/j.ejc.2020.103213).
Timeline.
Let be a finite simple graph and write for the neighbourhood of a vertex . A -edge-weighting is a function . The weighted degree of is
Two adjacent vertices have a coloring conflict if . The weighting is vertex-coloring if no edge is a coloring conflict, that is, if is a proper vertex colouring of .
If has a connected component consisting of a single edge (a component isomorphic to ), then for every , so no weighting is vertex-coloring. This is the only obstruction.
The proof uses a few further objects:
The Lean names are wdeg G ω v for , IsWeighting G k ω, IsVertexColoring G ω, NoK2Component G and IsGoodPartition G U R B.
If no connected component of is isomorphic to , then there is with
Every finite connected graph with has a vertex-coloring -edge-weighting. This is the statement the case analysis of the proof establishes. Theorem 1 follows by treating each component separately.
In the order the proof uses them:
The result. Theorem 1 settles a conjecture that was open for nineteen years. The constant is optimal: the triangle has no vertex-coloring -weighting (two of its three edges get the same weight, and then two vertices tie), and deciding whether a vertex-coloring -weighting exists is NP-complete (Dudek and Wajc, 2011). Theorem 1 also closes the sequence of upper bounds on the number of weights needed. Variants remain open: total weightings with vertex weights and edge weights (the 1-2 Conjecture), and list versions.
Formalizing it. The theorem is proved, in a 16-page paper. As far as is known it has no machine-checked proof. A formal proof would verify the case analysis at the end of the paper (pp. 11–14, about fifteen sub-cases with three auxiliary graphs), which is where errors in such arguments usually hide. The flow lemma is quoted from the 2023 paper and not reproved here. Formalizing it means proving an integral max-flow statement for a specific unit-capacity network, and the result can be reused for other flow-based weighting arguments.
The obvious approach is to fix the weights greedily, edge by edge or vertex by vertex. This fails because changing one edge weight changes two weighted degrees at once, so a repair at one vertex can create a conflict at a neighbour. With only three weights there is no room to absorb this. Every earlier bound above used the extra weight as slack.
The difficulty in the paper is parity. The construction needs the set of blue vertices to have even cardinality, and cannot always be made even. The proof therefore removes one or two vertices, applies one of three base lemmas, and re-inserts the vertices. That re-insertion may need one more round of weight changes along a path. Each sub-case has to keep track of parities, of exact weighted degrees on , and of the connectivity of simultaneously.
Representation.
SimpleGraph V on a finite vertex type V with decidable adjacency. The paper's "graph" is a finite simple graph: weighted degrees are finite sums, and the proof uses a maximum cut and vertex orderings.ω : Sym2 V → ℕ on unordered pairs. IsWeighting G k ω requires for every edge of ; values on non-edges are unconstrained and never used.G.neighborFinset v. Since in Sym2, the single sum equals both sides of Theorem 1's displayed inequality.G.between R B, induced on wherever that vertex set is not all of .Conventions that differ from the page. There are two, both disclosed in the item statements:
Lemma 5's condition is stated in , and Lemma 3's is computed in .
Ruled out. None of the following formalizations is faithful:
Infrastructure. A complete development needs:
The flow and cut definitions are stated for arbitrary finite graphs and can be reused. Contributions are welcome at every level: proofs of individual lemmas, general flow-decomposition results, and the final case analysis.
In a stochastic multi-armed bandit, a player repeatedly chooses one of arms and receives a random reward drawn from the chosen arm's unknown distribution. The classical lower bounds of Lai and Robbins (1985) and Burnetas and Katehakis (1996) describe the regret of good strategies when the horizon tends to infinity: it grows like , with a constant determined by Kullback–Leibler divergences. They say nothing about small horizons.
Garivier, Ménard and Stoltz (Math. Oper. Res., 2019; arXiv:1602.07182v3) show that the regret has a definite shape over the whole range of : it is almost linear at first ("explore first"), and only afterwards logarithmic ("exploit next"). Their §3 gives three non-asymptotic lower bounds for the initial phase, each for a natural class of strategies. This mission is the third of them, Theorem 4 (p. 13): a collective lower bound on the total number of pulls of all suboptimal arms. It is the bound that remains informative when many arms are suboptimal, and it is the one illustrated for large in the paper's §3.4.
A bandit problem is a family of probability distributions on , each with an expectation . A model is a set of such distributions, and is in when every . Put .
At each round a strategy chooses an arm from the past rewards (possibly with auxiliary randomization) and observes a reward . The number of pulls of arm up to round is , and is the expectation when interacts with .
The set of optimal arms is , of cardinality , and the set of worst arms is , the arms of smallest mean. The paper defines a partial order: when for every optimal arm of and for every other arm. Two classes of strategies enter the theorem.
With the Kullback–Leibler divergence, the constant of the theorem is
The Bernoulli divergence is , (5).
For every model , every strategy pairwise symmetric for optimal arms and monotonic on , every bandit problem in and every ,
Theorem 4 bounds the regret from below through , (13). While is small compared with , the right-hand side of the theorem is of order , so the regret is linear: a reasonable strategy cannot avoid spending a constant fraction of the first rounds on the suboptimal arms. Unlike the per-arm bounds of Theorems 2 and 3, the bound concerns all suboptimal arms at once and does not degrade as grows; §3.4 of the paper shows numerically that it gives the stronger regret bound for many arms.
The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. A formal proof would exercise the published canonical bandit model of the platform (StochasticBandit, BanditPolicy, banditMeasure) on a genuine lower-bound argument with two auxiliary bandit problems, together with a local Pinsker inequality for Bernoulli divergences in that is reusable in other bandit lower bounds.
The obvious attempt applies the fundamental inequality (6) to and an alternative in which one suboptimal arm becomes optimal, as in Theorem 2. That gives a bound arm by arm, which deteriorates with and does not see the number of optimal arms; it also needs a hypothesis of the type "smarter than uniform", which is not assumed here. Nothing is known about how a general behaves on itself, so the two hypotheses on must carry all the information, and both are weak: Definition 3 only constrains pairs of optimal arms with equal laws, and only through the joint distribution of their pull counts under the canonical bandit measure; Definition 4 only compares problems ordered by . On the analytic side, the classical Pinsker inequality loses the factor and gives a weaker theorem, so a local refinement is required, and every divergence is valued in .
Arms are indexed by Fin K (the paper's arm is index ), with assumed in the goal. A bandit problem is the published BanditAlgorithm.StochasticBandit K, a strategy is a published BanditPolicy K (a family of Markov kernels from histories to arms; every strategy of the paper with auxiliary uniform randomization induces one with the same law of arms and rewards), and is the integral of the pull count against banditMeasure. A model is a Set (Measure ℝ) whose members are probability measures with an integrable identity, the standing assumption of §1.1–§1.2. Definitions 3 and 4 leave implicit and are read "for all "; in Definition 3 equality of distributions is equality of the image measures of the pair of counts, not of their expectations. , and take values in ; the goal assumes , since otherwise the printed bound is and a real-valued conversion would silently replace by . The Bernoulli divergence is defined as the divergence between two Bernoulli laws on , so it is where (5) is, rather than a finite junk value. The auxiliary problems of the proof are not constructed; the milestones quantify over them with their defining properties.
The paper's "In particular" clause, for , is not stated: it follows from the main display only when (at the main bound is negative), and whether it holds in general is not known here.
A formalization that weakens the strategy classes (full permutation symmetry, or equality of expected counts in Definition 3), drops the requirement that the problems lie in the model, or uses a real Bernoulli divergence with finite values at does not count.
A complete development needs the fundamental inequality (6) on the canonical bandit model (the subject of mission I of this series; the chain rule for the divergence of bandit measures is already proved on the platform), the symmetry argument on the canonical measure, Lemma 6 and Lemma 2. Contributions of any of these, and of the identity integrated against banditMeasure, are welcome; Lemma 6 and the symmetry lemma are reusable beyond this mission.
A stochastic multi-armed bandit learner repeatedly selects one of finitely many arms and sees only the reward from the selected arm. The learner must gather information about uncertain rewards while trying to select high-mean arms. Expected regret summarizes the lost reward relative to always selecting an optimal arm, but regret alone does not explain how much sampling each particular arm must receive. Garivier, Ménard, and Stoltz study this allocation question directly in Explore First, Exploit Next: The True Shape of Regret in Bandit Problems. Their Section 3 gives lower bounds for small horizons, before the longer-run logarithmic behavior becomes dominant.
The paper's first small-horizon result concerns strategies that allocate at least a uniform share to every optimal arm, on every problem in a specified model. This requirement excludes a strategy that always selects one fixed label and succeeds only when that label happens to be best. Such a requirement still permits many adaptive policies; it constrains their performance on optimal arms rather than prescribing their decisions round by round. The result establishes a compulsory initial allocation to every arm, including one whose mean is below the best mean. It is Theorem 2 on page 10 of the pinned arXiv:1602.07182v3.
A bandit problem consists of probability laws on . At each round, a strategy chooses an arm using the observed past and randomization, then receives an independent reward drawn from that arm's law. The mean reward of arm is . Write , and call an arm optimal when . The count is the number of times arm is chosen during the first rounds. These objects and the information available to a strategy are specified in Section 1.1, pages 2–3.
A model is a collection of possible arm laws, each a probability measure with an expectation. The notation means that every arm law belongs to . A strategy is smarter than uniform on when, for every bandit problem in the model, every optimal arm , and every integer , it satisfies
This is Definition 2 on page 10. It imposes a lower bound on each optimal arm, even when several arms tie. The requirement is evaluated across the whole model, so a strategy cannot be declared smarter based only on its behavior on the one problem used in the theorem.
For a law , a real threshold , and the model , the information number is the infimum of over those whose mean exceeds . The infimum is if there is no such . This is the definition on page 4. It measures how close an arm law is, in Kullback–Leibler divergence, to another admissible law that would give it a mean above the present optimum.
The main target is Theorem 2. For a model , a strategy smarter than uniform on it, a bandit problem , every arm , and every integer , the finite- case states
The theorem includes optimal and suboptimal arms. Its printed companion says that when , the arm receives at least expected selections. In the formal statement this threshold is , which also expresses the intended case . Both claims come from Theorem 2, page 10.
The milestone list follows the source's intermediate claims. Lemma 6, page 20 bounds Bernoulli relative entropy using the maximum of over an interval. The proof of Theorem 2 on page 11 states that Bernoulli relative entropy increases in its second argument on the interval starting at its first argument. The same page applies the paper's fundamental inequality (6) to the fraction of rounds spent on one arm, then states a lower bound against a single alternative arm law. These are the four curated milestones for the main theorem.
The theorem turns a model-relative performance condition into a numerical constraint on early sampling. If an arm's law is close in divergence to a law that would make it best, then the bound keeps its expected pull count near the uniform allocation until the horizon is large enough for the term under the square root to matter. It identifies the divergence scale at which this particular guarantee becomes weak. The paper contrasts this absolute bound with later relative and collective bounds that capture different dependencies on the number of arms in Section 3, pages 10–14.
The mathematical result is proved in the paper. The remaining work in this mission is a machine-checked development of the statement and its source-backed intermediate inequalities in the canonical stochastic-bandit model. The published bandit structure, policy kernels, and information number provide reusable foundations. Shared definitions supply the Bernoulli divergence, model predicate, and expected pull counts; the local strategy class makes the hypothesis of this particular theorem explicit. The Bernoulli inequalities and the pull-count change-of-measure statement can be reused in other lower-bound results.
A performance condition about optimal arms does not directly constrain an arm that is suboptimal in the problem of interest. The small-horizon bound must remain valid even though the strategy may adapt to observed rewards, and the relevant alternative arm laws can have divergences approaching an infimum without attaining it. The paper's lower bound is therefore sensitive to the exact orientation of the two bandit problems, the expected count multiplying their divergence, and the boundary conventions for Bernoulli relative entropy. Replacing the infimum with a chosen alternative or changing a divergence to an ordinary real with an arbitrary boundary value would alter the statement.
Lean uses arms Fin K, indexed from zero; the paper indexes them from one. The horizon is a natural number, and counts are integrated against the probability measure on -round histories generated by a stochastic kernel policy. Such kernels represent the arm-and-reward histories induced by the paper's strategies with auxiliary randomization. The model is a set of probability measures on whose identity function is integrable. The published StochasticBandit, BanditPolicy, and ConsistentBanditPolicy definitions supply the basic problem, history measure, pull count, means, and .
Bernoulli divergence and take values in . The real square-root formula assumes : when it is infinite, the paper's right-hand side is , while converting infinity directly to Lean's real value would produce a false numerical bound. The starting bandit problem is explicitly in , a condition needed for the proof's use of Definition 2 on a one-arm modification, although the printed quantifier on page 10 omits it. The arm parameter guarantees ; every target assumes , so its real divisions by and have the stated meaning.
A faithful development must retain Definition 2's quantification over all model problems and each optimal arm, rather than only over the bandit problem used in the conclusion. It must use the full Bernoulli relative entropy, including infinite endpoint values, and the infimum over precisely those model laws with mean greater than . The local instance of (6) also assumes integrable arm rewards in both bandit problems, as Section 1.1 requires. Contributions that establish the four milestones, the companion threshold claim, or reusable count-integrability and divergence facts are in scope.
In a stochastic multi-armed bandit, a decision maker repeatedly chooses one of several unknown reward sources. Sampling an arm reveals its reward but uses a round that could have been spent on a better arm. A good strategy must therefore reduce sampling of inferior arms, yet it cannot stop sampling them too early: it must still distinguish the current problem from a nearby one in which an apparently inferior arm is best. This tension produces the logarithmic lower bounds that benchmark bandit algorithms.
Garivier, Ménard and Stoltz revisit that benchmark in Explore First, Exploit Next. Their Theorem 5 gives a finite-horizon lower bound with explicit terms beyond the leading logarithm. It concerns every uniformly super-fast convergent strategy on a well-behaved model, not a particular algorithm. The distinction matters when comparing an algorithm's upper bound to what any strategy with that uniform performance guarantee must pay. The theorem is proved in the paper; this mission asks for a machine-checked statement and proof of that established result.
There are arms. Arm has an unknown probability distribution over real rewards, with finite mean . The vector is a bandit problem. Its best mean is , and the gap of arm is . An arm with is suboptimal. A strategy selects an arm each round using the previous arms and rewards, possibly with randomization. Write for the number of times it selects arm by round , and for the expected count under the problem .
A model specifies the probability distributions that an arm may have. All its laws have a finite first moment, and a bandit problem is in when every arm law belongs to it. For a law and a target mean , the paper's minimal information cost is
where an empty infimum is . This measures how much the law of an arm must change to make its mean exceed . The Bernoulli divergence used in the intermediate change-of-measure bound keeps its infinite values at the boundary.
Let be the interior of the set of expectations of laws in . A model is well behaved when positive functions and satisfy, whenever , , , and ,
A strategy is uniformly super-fast convergent with constant when for every problem in , every suboptimal arm, and every . The same constant applies throughout. Finally, records the inverse-squared gaps of all suboptimal arms.
For each suboptimal arm let . The goal is Theorem 5, with and
For every satisfying , , , and , the target is
The milestones follow the paper's displayed bounds: the one-alternative inequality (15), the optimized inequality (17), the inverse-information-cost bound after (17), and the product inequality quoted immediately before Theorem 5. They preserve the same constants and the same .
The leading term is the familiar distribution-dependent sampling barrier. The explicit , , and quantify the correction at a finite horizon; the paper observes that their combined contribution has order under its conditions. This makes the result useful when an algorithm's upper bound includes a second-order term and one wants to know the scale that a lower bound permits. It also identifies precisely which model regularity and uniform strategy guarantee support that comparison.
Formalizing Theorem 5 would add a reusable finite-horizon lower bound to the bandit library. The published definitions of stochastic bandits, policies, pull counts, and supply the base model; this mission adds the paper's well-behavedness and super-fast convergence predicates and states the intermediate inequalities as separate targets. The paper's proof is established mathematically, while these mission statements remain open Lean theorems until solvers supply machine-checked proofs.
The information cost is an infimum over alternative reward laws, so the finite-horizon bound must remain meaningful when the feasible set is empty or its divergence is infinite. The displayed formulas also divide by that information cost and use logarithms of quantities involving the strategy's uniform constant. For Theorem 5, the explicit correction factors must all lie in the range where the paper's final product inequality applies. A purely asymptotic statement would discard exactly the constants and horizon conditions that distinguish this theorem.
Arms are Fin K, so the paper's arm has Lean index . A strategy is represented by Markov kernels on observed arm-reward histories; its expected pull count is an integral of a bounded count. The model consists of probability measures on with integrable identity. The information cost and Bernoulli divergence live in ; a finite positive cost is converted to a real number only where a displayed reciprocal requires it. The goal contains a suboptimal arm, which rules out the empty-arm and single-arm cases. The model's witness functions are total in Lean, with requirements only on their paper-defined domains.
The theorem explicitly assumes and , which are implicit in the paper's use of and . It also assumes : the printed proof invokes a product inequality requiring that sign, although the theorem prints only . The version of (17) in the milestone list assumes in the case of a negative logarithm. These conditions and the model's integrability prevent vacuous or totalized-value readings of the lower bound. Contributions toward the four displayed milestones, the required measure-theoretic change of measure, and the finite-horizon arithmetic are in scope.
A seller with several goods can sell them one at a time or offer a mechanism that links allocation and payment across goods. Separate selling asks the seller to solve a one-good pricing problem for each item. A general mechanism can offer lotteries and menus whose outcomes depend on the buyer's whole valuation vector. The difference matters because the buyer's private information covers several values at once, and an optimal multidimensional mechanism need not resemble an ordinary posted price. Hart and Nisan ask how much revenue is guaranteed by simple selling rules when the joint valuation distribution is unrestricted apart from the stated independence assumptions (Hart and Nisan, arXiv:1204.1846v3).
This mission isolates their two-good, identically distributed result, Theorem B. The paper first gives a one-half guarantee for two independent goods with potentially different distributions, then improves the guarantee to when their distributions agree. The improvement is a claim about every probability law on nonnegative values. It assumes neither a density nor a regularity condition on the tail of that law. The paper proves the result in Appendix A.1 after stating it in the introduction (Hart and Nisan, pp. 6 and 31–35).
There is one risk-neutral buyer and one seller. For two goods, the buyer's private valuation is a vector with . Values are additive: receiving both goods is worth . The seller knows the distribution of the vector but not the realized values. In this mission, and are independent and have the same arbitrary probability law on . A law, rather than a named pair of random variables on a probability space, carries all the data needed by the revenue quantities.
A direct mechanism takes a reported pair and returns an allocation probability for each good and a real payment to the seller. The buyer's payoff from reporting truthfully is . The mechanism is incentive compatible (IC) if truthful reporting is at least as good as any other report for every possible valuation, and individually rational (IR) if truthful payoff is nonnegative everywhere. These requirements hold on the whole nonnegative orthant, as in Section 2.1 of the paper (Hart and Nisan, pp. 11–14).
Write for the expected payment under a valuation law and for the supremum of over feasible, IC, IR mechanisms. For one good, write . The separate-selling revenue for two identically distributed goods is . Equation (1) of the paper identifies the one-good value with the supremum of posted-price revenue ; the supremum formulation covers laws for which no maximizing price exists (Hart and Nisan, p. 12; Myerson, 1981).
The goal is the exact upper bound written at the start of the paper's proof:
Equivalently, separate selling guarantees at least of optimal revenue whenever the ratio has an ordinary meaning. The inequality itself is the stable formulation at zero and infinite revenues. The formal goal uses the exact constant , not the rounded percentage in the theorem's prose (Hart and Nisan, Theorem B, p. 6; proof, p. 31).
The milestones include the one-good posted-price identity, the fact that nonnegative payments suffice when optimizing, symmetrization for identical independent goods, Lemma 19's lower-valuation revenue bound, equation (12), and the two expectation estimates and final numerical bound used after it. Proposition 5's IC characterization is also a draft theorem, though it is not a milestone. Each statement retains its source's domain and the constant . The final inequality for the right side of (12) is stated for every nondecreasing allocation function into , as required by the paper's argument on pp. 33–35.
Theorem B gives a distribution-free quantitative guarantee for an easy-to-describe selling rule in a setting where the optimal rule may depend on the buyer's entire two-dimensional private type. Its guarantee is stronger than the one-half guarantee for merely independent goods stated as Theorem A. The conclusion concerns the best revenue available from all feasible IC and IR mechanisms, so the benchmark includes randomized allocations and payments depending on both reported values (Hart and Nisan, pp. 6 and 11–13).
The formalization target is a machine-checked version of a proved result, not a new conjecture. The proposal currently contains compiled Lean statements with unproved theorem bodies. A completed development would prove the stated inequality and its selected supporting results. It would also supply reusable definitions for direct mechanisms with additive nonnegative values, extended-real revenue, optimal revenue as a supremum, and symmetry of two-good mechanisms. No machine-checked proof of these proposed Hart–Nisan statements is claimed here.
The one-good posted-price formula does not directly control an arbitrary two-good mechanism: allocation of either good and the payment can depend on both reported values. Applying a one-good bound separately to the two coordinates therefore leaves terms that depend on the other coordinate. In particular, a direct comparison between each marginal posted-price optimum and the total payment loses the improved constant. The proof has to control the dependence created by a joint mechanism while retaining the exact numerical estimate. A second formal difficulty is that an admissible mechanism can have a negative expected payment even though optimal revenue is nonnegative, while an unrestricted law can give infinite optimal revenue. Replacing every expectation by an ordinary real integral or clipping each mechanism's revenue would change Lemma 19 and the intermediate inequalities (Hart and Nisan, pp. 31–35).
Valuations are finite vectors ; the main theorem fixes . The two-good law is the product of the same one-good probability measure in both coordinates, so independence and identical distribution are built into the data. The model represents allocation probabilities as real numbers with explicit bounds . It requires IC and IR pointwise on all reports. No positive transfer (NPT) means and is imposed only on supporting statements where the paper uses it. Following the paper's footnote 12, admissibility also requires the payment function to be measurable.
An individual expected payment is an extended real difference of positive and negative Lebesgue integrals. For IC mechanisms, the negative part is finite because the payment is bounded below by its value at zero. Optimal revenue is the supremum of the nonnegative clips of admissible mechanisms' expected payments; the zero mechanism makes this the same supremum as in the paper. Lemma 19 and equation (12) keep individual revenue in the extended reals. Supporting inequalities that write as a real number explicitly assume ; Theorem B does not. Integrals of bounded threshold functions use ordinary real expectation, while the nonnegative term uses a nonnegative Lebesgue integral. The goal cannot be satisfied by a correlated joint law, a bounded-support special case, a vacuous assumption on , or a rounded constant.
The reusable work includes one-good posted-price revenue for arbitrary laws, a nonnegative-transfer reduction, a faithful single-mechanism revenue type, and probability identities for two independent coordinates. Theorem A, Theorem 7, Theorem 16, and a full formalization of the paper's other selling rules are outside this mission.
The Decision-Estimation Coefficient (DEC) of Foster, Kakade, Qian and Rakhlin (arXiv:2112.13487) is a single complexity measure that bounds the minimax regret of interactive decision making (bandits, reinforcement learning, and their structured variants) from above and from below. Its lower bound (Theorem 3.2 of the paper) states that every algorithm suffers expected regret at least a constant times , so concrete lower bounds on regret follow from concrete lower bounds on the DEC of localized model classes.
The multi-armed bandit is the first test of this program. Its minimax regret is classical (Auer et al., 2002; Audibert and Bubeck, 2010). Section 5.1 of the paper recovers it through the DEC: posterior sampling (Proposition 5.1) and inverse gap weighting (Proposition 5.2) bound the DEC by from above, and Proposition 5.3 bounds it by from below. The lower bound is proved through a hard family of models (Definition 5.1, Lemma 5.1), the device that the paper reuses for linear, ReLU and gap-dependent lower bounds in §§6–7.
A decision space is a finite set; here , the arms. A model assigns to every arm a distribution over rewards in (observations are trivial). Its mean reward is , and is an optimal arm. The squared Hellinger distance between distributions on a finite set is (no factor , the paper's (5)).
For a class of models, a reference model and , the DEC (2) is
With , the -localized class (12) is .
A reference model and models , , form an -family (Definition 5.1) if there are with , , and . is the Bernoulli distribution with mean .
For arms, and every , with ,
The mission also states monotonicity of the DEC in the class (the step from the family to the localized class), Proposition 5.1 (posterior sampling bounds the dual square-loss DEC by ), and Proposition 6.7, the gap-dependent variant: for bandits with gap exactly , some in the class has . Proposition 5.2 (inverse gap weighting) and the decoupling step of Proposition 5.1 are already proved on the platform and are included as references.
Proposition 5.3 is the DEC half of the minimax lower bound for multi-armed bandits: combined with Theorem 3.2 and , it shows that the general DEC theory loses nothing in rate on the most basic interactive problem, and that the upper bounds of Propositions 5.1 and 5.2 are tight up to constants. Lemma 5.1 is reusable: any lower bound on the DEC of a class can be obtained by exhibiting a hard family, and the paper uses it for linear bandits (Proposition 6.2), ReLU bandits (Proposition 6.6) and gap-dependent bounds (Propositions 6.7, 6.8).
The results are proved in the paper. As far as is known, none of them is machine-checked. A formal development provides a verified Bernoulli Hellinger bound, a reusable hard-family lemma for the DEC as published on the platform, and the first verified DEC lower bound for a concrete class.
The DEC is an inf-sup, so a lower bound must hold against every exploration distribution . A natural first attempt picks a single alternative model and compares; this fails because can concentrate on the arm where that alternative differs and then the Hellinger penalty cancels the regret. The family must be spread so that no single is good for all of its members at once, and the constants must balance the regret term against the information term at the chosen . In Lean, an additional difficulty is that the DEC is written with real sInf/sSup, which are on empty or unbounded sets: every lower bound requires showing that the relevant sets are nonempty and bounded, and passing from the family to the localized class needs monotonicity of the DEC, which the paper uses without comment.
m : S → Y → ℝ with every m π a probability vector; expectations are finite sums. The DEC is the published FoundationsRL.GeneralDM.decGf, the Hellinger distance hellingerSq, the mean reward fM.Y = Bool, reward on true), a subclass of the paper's all-distributions-on- class. The DEC is monotone in the class and the localized class shrinks with the class, so the Bernoulli lower bounds imply the paper's.piStar with the hypothesis that it picks a maximizer of ; every statement holds for every such selector, so for whichever maximizer the paper meant (the reference has every arm optimal).decGf evaluate to the junk value ; the goal is stated over a class containing with bounded rewards, so the inequality is the genuine one, and its right side is strictly positive.Contributions welcome: proofs of the milestones in attack order, sorry-free lemmas on nonemptiness and boundedness of the DEC's inner sets (reusable for every DEC lower bound in this series), and a proof of the gap-dependent companion.
Generalized Turán problems ask for the maximum number of copies of a fixed graph in an -vertex graph that avoids a family of forbidden subgraphs. The ordinary Turán number counts edges (); Alon and Shikhelman (arXiv:1506.03397) started the systematic study of the general function , building on earlier results of Erdős on cliques, Bollobás and Győri on pentagons in triangle-free graphs, and Győri and Li on triangles in graphs without a long odd or even cycle. Counting cycles in graphs with forbidden cycles is closely tied to extremal problems for Berge hypergraphs, and the constructions used are sparse hypergraphs of large girth.
Gerbner, Győri, Methuku and Vizer, Generalized Turán problems for even cycles (arXiv:1712.07079, J. Combin. Theory Ser. B, 2020), determine or bound for many cycle families. This mission covers one of their results in §6.2: the number of odd cycles in a graph in which every shorter cycle is forbidden and, in addition, one longer odd cycle is forbidden. Its companion (Theorem 17, a separate mission of this series) forbids a longer even cycle instead, and there the paper obtains a sub-quadratic upper bound; with an odd extra cycle only a quadratic upper bound is proved.
All graphs are finite and simple. For an integer , is the cycle of length . For a set of integers , write ; a graph is -free if it contains no with as a (not necessarily induced) subgraph. The family consists of all cycles .
For graphs and , is the number of copies of in : subgraphs of isomorphic to , counted without labelling. The generalized Turán number is
For a vertex of , is the set of vertices at distance exactly from .
A hypergraph is a finite set of hyperedges (vertex sets); it is -uniform if each hyperedge has vertices. A Berge cycle of length is a sequence of distinct vertices and distinct hyperedges with and . The girth of a hypergraph is the length of its shortest Berge cycle; "girth at least " means there is no Berge cycle of length .
For all integers , as ,
Both the lower and the upper bound are part of the goal; the implied constants may depend on and only.
The supporting published theorem erdos_gallai_path_conjecture (the Erdős–Gallai path theorem: a graph on vertices with no path of edges has at most edges) is included as a reference item; the paper's proof of Claim 19 invokes it.
Theorem 18 shows that forbidding all cycles up to length together with one odd cycle still permits polynomially more than copies of , at least , and at most . Compared with Theorem 17, where an even cycle is forbidden and the count is , it isolates the role of the parity of the extra forbidden cycle. The authors conjecture that the true order is sub-quadratic (Conjecture 34, §8 of the paper), so the gap between the two exponents in Theorem 18 is a stated open question; a formal development of the known bounds is the base on which any improvement would be checked.
The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces: a reusable encoding of generalized Turán numbers for cycle families on top of Mathlib's copyCount; Berge cycles and the girth of uniform hypergraphs; distance layers ; and a formal statement of the Nešetřil–Rödl existence theorem, which is used as a black box by many extremal constructions.
The upper bound requires careful bookkeeping of distance layers around a vertex in a graph without short cycles. The obvious estimate, bounding the copies of through by the number of pairs of vertices of , gives only per vertex and hence nothing better than the trivial bound overall; the content of Claim 19 is that forbidding the single cycle makes the edge count inside linear, and the parity of is used essentially.
The lower bound rests on Theorem 29, a cited result that is not proved in the paper, and for which Mathlib has no supporting theory of uniform hypergraphs or Berge cycles. For the construction itself, the paper only asserts that the cycle-replacement graph has no short cycle other than the inserted 's; a cycle of the graph may wander through many hyperedges, and relating it to the girth of the hypergraph is the step a formal proof has to supply.
Fin n; graphs are SimpleGraph (Fin n). Cycles are Mathlib's SimpleGraph.cycleGraph, and is Mathlib's unlabelled copyCount.Set.Icc 3 (2 * l) ∪ {2 * k + 1}: every length , not only .edist, so vertices of other components lie in no layer.Finset (Finset V); "girth at least " is a predicate (no Berge cycle of length ), not an infimum, so a hypergraph without Berge cycles has every girth.Asymptotics.IsBigO along atTop, with real exponents; both directions of the goal are stated.A formalization that states only the upper bound, uses labelled copies, lets a constant depend on the graph, omits the short cycles from the forbidden family, or defines by a supremum that can take a junk value, does not prove this theorem.
Contributions welcome: proofs of the milestones, a proof of Theorem 29, and general lemmas on breadth-first layers in graphs of large girth, which are reusable by the companion missions of this series.
Neural networks trained by empirical risk minimization are sensitive to small adversarial perturbations of their inputs. Distributionally robust optimization addresses this by training against the worst distribution in a neighbourhood of the data distribution. Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571v5, ICLR 2018) take the neighbourhood to be a Wasserstein ball and relax the hard constraint to a Lagrangian penalty with multiplier . For large the inner maximization becomes strongly concave and is solved per data point by a transportation map , which turns each training example into its worst-case perturbation.
The average transport cost is the amount of robustness the trained model actually certifies on the sample: by the paper's duality result, the empirical worst-case loss at level is computable, and it is the certificate of robustness that the paper advertises. A certificate measured on the training sample is only useful if it transfers to the population. This mission formalizes the result that it does: concentrates around its population counterpart, uniformly over the parameter set.
Parameters range over a set and data over a set , both with the Euclidean norm. A transportation cost satisfies and Assumption A: is continuous and is -strongly convex for each . A loss satisfies Assumption B: its partial gradients , are Lipschitz in each variable, with constants .
For the problem is -strongly concave on , and the transportation map is its maximizer,
Given i.i.d. samples with and empirical distribution , the empirical robustness level and its population counterpart are
The complexity of enters through its covering number , the least number of points such that every is within of some ( if there is no finite such family).
Two alternative regularity conditions close the setting, with a constant : (i) is -Lipschitz on in each argument; or (ii) and is -Lipschitz. Put in case (i) and in case (ii).
For every ,
In case (i), and this is exactly the last display of the proof of Theorem 4 (p. 44); case (ii) is the "identical reasoning" the paper invokes with . is an arbitrary subset of : no compactness is assumed, and an infinite covering number makes the bound vacuous rather than false.
In the order the proof uses them:
The tail bound gives a -type generalization rate for the gap between the robustness certified on the sample and the robustness achieved on the population: with for bounded , the deviation is of order . It also implies, as the paper notes, that the certified level stays positive for large whenever the loss is not invariant to the data.
The paper states the result as Theorem 4, display (17), in "with probability " form with the constant . That form does not follow from the proved tail bound as printed: inverting the tail bound gives a deviation with a covering radius that depends on the deviation rather than on , whereas (17) uses in both places and drops and . The mission therefore poses what the proof establishes, the tail bound above, and does not claim (17). None of this paper's results has a machine-checked proof; Hoeffding's inequality and covering numbers are in Mathlib, the argmax stability and the cover argument are not.
Concentration at a single fixed is Hoeffding's inequality and carries no information about the trained model, whose parameter depends on the sample. The supremum over an arbitrary, possibly uncountable is the content. A union bound needs a finite family, and transferring control from a finite family to all of needs the deviation to be Lipschitz in . The deviation is built from the transportation map, which is an argmax and has no closed form; its regularity in comes only from strong concavity, which holds only for . In case (ii) the cost itself has no Lipschitz assumption, and the Lipschitz property of has to be extracted from the optimality of at two different parameters. Finally, the supremum event is not obviously measurable.
Spaces are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m); the paper's general norm is specialised to , in Assumptions A and B, in cases (i) and (ii), and in the covering number. The cost is real valued and constrained on only; the loss is typed on , but Assumption B and the argmax property of the transportation map are required only for and , matching the paper's . The transportation map is a function together with its argmax property. Samples are the coordinates of the product measure ; of the supremum event is its outer measure, so no measurability of the event is assumed. The supremum is a real supremum of quantities bounded by . The covering number is Mathlib's Metric.coveringNumber (closed balls, centres in , values in ). The definition on p. 9 does not say where the centres lie; the proof applies Hoeffding's inequality "for any fixed " at the centres, and the loss is only defined on , so the centres are taken in .
Hypotheses made explicit that the page leaves implicit:
Case (ii) is assumed for only, as printed in Theorem 4.
A bound for one fixed , a supremum taken outside the probability, a covering radius not tied to , or a covering number of a set other than would be a different and much weaker statement; the goal has the supremum over inside the event and the radius .
A complete development needs the stability of maximizers of strongly concave functions under Lipschitz perturbation of the gradient, a finite-cover union bound for outer measures, and Hoeffding's inequality for bounded i.i.d. coordinates of a product measure. The first two are reusable well beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for the goal.