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?
Strategic open pit mine planning decides which parts of an ore body are excavated, in which period, and where each block of material is sent: to a processing plant, a stockpile or a waste dump. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research 68(5), 2020) state the problem as a mixed-integer program, the precedence-constrained production scheduling problem with clusters (PCPSP-C), which extends the formulation of Bienstock and Zuckerberg (IPCO 2010) to clusters of blocks that are extracted together. The integer versions of this program have large integrality gaps on production scheduling instances (§5, p. 1432), so the authors derive problem-specific cutting planes. This mission concerns the variable-right-hand-side (VRHS) production cuts of §5.2. They combine the precedence order of the clusters with the capacity of a single destination: if a solution sends many blocks to a capacitated destination, the predecessors of those blocks must be fully extracted.
The VRHS cuts are introduced first on a one-period, two-destination set, the mode-knapsack set MK (§5.2.1), and then generalised to the full multi-period clustered model (§5.2.2). Disaggregated formulations with destination choices go back to Boland et al. (Comput. Oper. Res. 2009); cutting planes for the precedence-constrained knapsack structure of open pit scheduling were studied by Bley et al. (Comput. Oper. Res. 2010).
All page references are journal pages of the published Operations Research article.
An instance has finite sets of blocks, of destinations and of clusters, the latter a partition of , and periods . Block lies in cluster and has weight . A precedence relation on blocks induces one on clusters ( if some block of precedes some block of ), assumed to be a strict partial order. The arc set is its transitive reduction: when is an immediate predecessor of . The reverse closure of a cluster is , the cluster and everything that requires it; for a set of clusters, .
Variables give the fraction of cluster extracted in period , and the fraction of block sent to destination in period . The constraints (2)–(7) of p. 1427 are
together with an integrality condition: full integrality (10), , defines the PCPSP-F, and partial integrality (11), " implies for ", defines the PCPSP-P. The general rows include the destination capacity rows (9), . The cuts use the cumulative variables (17).
The mode-knapsack set MK (p. 1433) fixes a DAG , weights and a capacity , and consists of the vectors with
Fix , and clusters with . Let , for , and , . For constants (), the inequality
is valid for the PCPSP-F, and, when (33), for the PCPSP-P. The goal is the conjunction of the two validity claims.
A valid inequality removes fractional points of the linear relaxation while keeping every feasible schedule. The VRHS cuts are among the production cuts that the paper evaluates in its computational study (§8), alongside the extraction cuts and the hourglass cuts. Their right-hand side is not a constant but a combination of extraction variables along a chain, which is what lets them couple the destination capacity with the precedence order; the paper's Theorem 5 shows the mechanism on MK, Theorem 7 in the full model. The partial integrality regime, under which the second half of Theorem 7 holds, is the one used by commercial mine planning software (p. 1427).
The results are proved in the paper by case analysis on the first index with . None of them has a machine-checked proof. Formalizing them makes explicit which rows of the formulation each cut uses (the destination capacity (9) and the integrality condition), and what role the coefficient condition (33) plays in the partially integral case.
The proof uses that partition and are disjoint from , which requires along the chain. It uses that for every , and that forces all strict successors of to be unextracted; both chain the constraints (4) and (11) along covering arcs of a finite strict order, since the formulation constrains only the arcs of , not all of . A natural first attempt, arguing directly from , therefore does not apply. The counting step needs , which is not a constraint of the formulation but follows from , and the nonemptiness of clusters. In the partial integrality case a fractional is possible, and the bound on the term must come from (33) rather than from integrality.
Blocks, destinations and clusters are finite types; periods are Fin T, index standing for period . An instance carries the block-to-cluster map, the block precedence, values, discount rate, weights, capacities and side rows . Cluster precedence is derived from block precedence; is its covering relation, and constraints (4) and (11) range over only. The chain is a function on read at with , and condition 1 of Theorem 7 is stated for consecutive pairs. In (32), is taken at the single period and is cumulative.
The standing assumptions of §2.1 are hypotheses of every PCPSP-C statement: clusters cover (so each is nonempty), is a strict partial order on clusters, , and . A cut "valid for the PCPSP-F (PCPSP-P)" is stated as: at every point feasible for the formulation with full (partial) integrality whose destination capacity rows (9) hold, the inequality holds. The capacity rows enter as an explicit hypothesis because the paper assumes they are among the rows of ; without them the cut is false. Validity is never asserted for the LP relaxation, where (29) and (32) fail, so the integrality condition cannot be dropped. Conditions 2 and 3 of Theorem 7 are kept as on the page, although the proof does not use condition 3. In MK, the DAG property, and are hypotheses; an arc means that extracting forces , and collects and the blocks from which is reachable.
The development needs only finite sums, finite sets and orders from Mathlib. Contributions are welcome on the chaining lemma for covering relations of finite strict orders, on the nonnegativity and monotonicity of , and on the partition of , which the goal and the milestones share.
Many problems in convex optimization, variational inequalities and saddle-point computation can be written as a monotone inclusion: find in a real Hilbert space with
where is a set-valued maximally monotone operator (a subdifferential, a normal cone, a constraint) and is a single-valued monotone operator (a gradient, or the skew operator of a saddle-point problem). Splitting methods solve such problems using and separately: a backward step evaluates the resolvent , and a forward step evaluates .
The classical forward-backward method converges when is cocoercive, but can fail when is merely monotone and Lipschitz, which is the case for saddle-point operators such as . Tseng's forward-backward-forward method (Tseng 2000) removes the cocoercivity assumption at the price of two evaluations of per iteration. Malitsky and Tam (arXiv:1808.04162; SIAM J. Optim. 30(2), 2020) propose the forward-reflected-backward method, which needs one evaluation of and one resolvent of per iteration, reusing the previous value of .
Timeline of the relevant results:
is a real Hilbert space with inner product . A set-valued operator is monotone if whenever , , and maximally monotone if its graph is not properly contained in the graph of another monotone operator. Its resolvent is, for and maximally monotone, an everywhere defined single-valued map, characterised by . A map is -Lipschitz if , and monotone if .
The zero set is . Given initial points and step sizes , the forward-reflected-backward method is
A sequence converges weakly to if for every ; a sequential weak cluster point is the weak limit of a subsequence.
If is maximally monotone, is monotone and -Lipschitz, , and for some , then every sequence generated by (13) satisfies
In attack order:
Corollary 2.6, the constant-step case , is included as a companion theorem.
Theorem 2.5 shows that monotone inclusions with a Lipschitz, non-cocoercive single-valued part can be solved by a splitting method with the per-iteration cost of forward-backward splitting: one forward and one backward evaluation. For saddle-point problems, where each evaluation of is a pair of matrix–vector products, this halves the operator cost of Tseng's method. The method contains the projected reflected gradient method and, for , Popov's method and the optimistic gradient method used in training generative adversarial networks (Remark 2.1). The analysis of this section is reused for the linear rate, the linesearch, the inertial variant and the three-operator variant of later sections (missions 2–5 of this series).
The theorem is proved in the paper. Formalizing it requires a machine-checked Opial-type lemma and a machine-checked demiclosedness argument for maximally monotone operators perturbed by a continuous monotone map, both reusable well beyond this mission. To our knowledge no machine-checked proof of convergence of the forward-reflected-backward method exists.
The energy inequality of Lemma 2.4 is algebra plus monotonicity and the Lipschitz estimate, and it yields boundedness and . The difficulty lies in passing from these facts to weak convergence of the whole sequence. Norm convergence is false in general, so a Cauchy-sequence argument is unavailable. The energy is not Fejér monotone in alone, because of the cross term , so the standard Fejér/Opial lemma does not apply directly. Identifying weak cluster points as zeros requires the weak-strong closedness of the graph of , which in turn rests on maximal monotonicity of the sum: this is not a consequence of monotonicity of the two parts, and the inclusion (25) can be passed to the limit only because the step sizes stay above .
The Lean development uses a real inner product space H (InnerProductSpace ℝ H), complete wherever the page needs it, and the published operator vocabulary ThreeOpSplitting.Accel.MonotoneOperators (monotone and maximally monotone set-valued operators, monotone and Lipschitz single-valued maps, resolvents). Conventions:
x j is and lam j is ; the initial points are arbitrary.Three formalizations would trivialize the goal and are excluded:
A complete development needs the Opial-type Lemma 2.2, which in turn needs weak sequential compactness of bounded sets in Hilbert space, and maximal monotonicity of for continuous monotone (Bauschke–Combettes, Corollaries 20.25 and 24.4(i)) with its demiclosedness (Proposition 20.33). These are general results of monotone operator theory, and contributions of them as separate theorems are welcome.
The spectral radius of a graph, the largest eigenvalue of its adjacency matrix, measures how densely and how unevenly the edges of the graph are distributed. Asking which graph in a class maximizes it is a spectral analogue of the extremal question "which graph in the class has the most edges". For planar graphs the question has a long history in spectral graph theory, going back at least to Schwenk and Wilson. It also arose in geography, where the spectral radius serves as a measure of the connectivity of planar networks. To compare real networks with a theoretical upper bound, geographers wanted the planar graph of maximum spectral radius (arXiv:1606.01916v2, p. 3).
Timeline, as recorded by Tait and Tobin (pp. 1–3):
All graphs are finite and simple. A graph on vertices has vertex set . Its adjacency matrix is the real matrix with entry in position when and otherwise. Its eigenvalues are real, and the largest is the spectral radius .
A graph is planar if it can be drawn in the plane with vertices as distinct points and edges as simple arcs joining their ends, such that an arc meets no vertex other than its ends and two arcs meet only at common ends.
For graphs and on disjoint vertex sets, the join is the graph on the union of the two vertex sets that keeps every edge of and of and adds every edge between a vertex of and a vertex of . Write for a single edge, for the path on vertices, and for their join: two adjacent vertices, both joined to every vertex of a path on the remaining vertices. The paper also writes it .
A planar graph on vertices is a planar spectral maximizer if for every planar graph on the same vertices.
The milestones refer to a leading eigenvector of a maximizer, scaled so that every entry is positive and the largest entry is , and to a vertex with . For a parameter they use the sets and , the edge counts (edges inside ) and (edges between and ), and a second vertex with that is adjacent to all but vertices of .
The threshold is not fixed. The paper proves the statement only for beyond an unspecified bound, and the conjecture's bound remains open. The equivalence encodes "the unique maximizer is ": every maximizer is isomorphic to it, and it is itself a maximizer.
The result. Theorem 15 settles the Boots–Royle / Cao–Vince conjecture for all large . It identifies the planar graph of maximum spectral radius exactly, so the theoretical upper bound that the geographic application asks for is . Along the way, Lemmas 8–14 describe the eigenvector of the extremal graph: two vertices carry almost all of the eigenvector weight, and every other entry is below . The same method proves the outerplanar analogue (Theorem 7, the companion mission of this series).
Formalizing it. The theorem is proved on paper and has no machine-checked proof. Formalizing it needs several pieces that are absent from Mathlib or the platform and are reusable: the edge bound and the bipartite bound for topologically planar graphs, the non-planarity of and and of their subdivisions, Rayleigh-quotient comparison of spectral radii, and the face structure of maximal planar graphs. Each milestone is a self-contained target.
Counting edges does not separate the candidates. A maximizer can be taken to be a maximal planar graph, so it has exactly edges. Every maximal planar graph on vertices has the same number of edges, and the standard lower bound is the same for all of them. The extremal graph is pinned down only through its eigenvector. One has to show that the weight concentrates on two vertices, which are then forced to be adjacent to each other (Lemma 13) and to every other vertex (Lemma 14). Lemma 13 is the step specific to planarity. It uses the triangular faces of a maximal planar graph to find an edge switch that keeps the graph planar. In the formal setting, planarity is topological, so every planarity fact of the argument (the edge counts, the and obstructions, the faces of a triangulation) has to be derived from the drawing.
SimpleGraph (Fin n). " is " is a graph isomorphism G ≃g bookPath n, where bookPath n lives on Fin 2 ⊕ Fin (n - 2). It is not an equality on a fixed labelling.WangKangXue.SpectralTuran.specRad, the largest eigenvalue of the real adjacency matrix.RobertsonSeymour1986.GM5.IsPlanar: a drawing by simple arcs. It is not replaced by /-minor-freeness or by an edge count, either of which would change the class the maximum ranges over.IsSpecMax IsPlanar G: is planar and for every planar on Fin n. Every milestone from Lemma 8 to Lemma 14 assumes it. These lemmas are false for an arbitrary planar graph, so a statement that drops the hypothesis, or replaces it by a property implying the conclusion, is not acceptable.IsSecondHub), with the constants and .Bibliographic data as given in the bibliography of Tait and Tobin (pp. 21–23).
The spectral radius of a graph , the largest eigenvalue of its adjacency matrix, is a standard measure of how densely and how centrally a graph is connected. A classical theme of spectral graph theory asks, for a natural family of graphs, which member of the family on vertices maximizes . For planar graphs this question was raised by geographers comparing road and transport networks, and for outerplanar graphs it was posed by Cvetković and Rowlinson in their 1990 survey of the largest eigenvalue of a graph, where they relate it to the study of subfamilies of Hamiltonian graphs.
Conjecture (Cvetković–Rowlinson, 1990). The outerplanar graph on vertices of maximum spectral radius is .
Timeline:
This mission formalizes Section 2 of Tait and Tobin.
All graphs are finite and simple. An -vertex graph has vertex set , adjacency matrix , and spectral radius , the largest eigenvalue of the real symmetric matrix . Write for the degree of a vertex and for its neighbourhood.
A plane drawing of places the vertices at distinct points of and each edge as a simple arc between its ends; an arc passes through no other vertex, and two arcs meet only at a common end. The union of the vertex points and arcs is a compact set, so its complement has exactly one unbounded connected component, the outer face. A graph is outerplanar if it has a plane drawing in which every vertex lies on the boundary of the outer face.
The join of two graphs is their disjoint union together with all edges between them. The fan is a single vertex joined to every vertex of a path on vertices; it is outerplanar and has edges.
An outerplanar graph on vertices is a spectral maximizer if for every outerplanar graph on the same vertices.
Several milestones refer to a Perron vector: an eigenvector of for with all entries positive, normalized so that its maximum entry is , together with a vertex with . For a connected graph such a vector exists by the Perron–Frobenius theorem.
There is such that for every and every graph on vertices,
The forward direction is the paper's Theorem 7; the converse says that the fan is the maximizer, as the conjecture reads. The threshold is left unspecified, as in the paper.
The milestones follow the proof in Section 2, in order:
The theorem settles, for all large , a conjecture that had been open since 1990 and had resisted several partial attacks. The same paper settles, in the same framework, the planar analogue (the Boots–Royle and Cao–Vince conjecture, ) and a conjecture on spectral irregularity. The outerplanar case is the shortest of the three.
On the formal side, the result is proved on paper but has no machine-checked proof. Completing the mission produces a formal theory of outerplanar plane drawings (edge bound, -freeness, outerplanarity of the fan), eigenvector estimates for extremal graphs, and the full extremal theorem. The edge bound and the exclusion are reusable for any later work on outerplanar or series–parallel graphs. Determining the exact threshold , or proving the statement for every , would be a strengthening beyond the paper.
There are two separate difficulties. The first is topological: the facts about outerplanar graphs that the spectral argument uses (at most edges, no subgraph, no cycle in when dominates, outerplanarity of the fan) are folklore on paper but require a Jordan-curve-type argument about plane drawings, of which Mathlib currently contains very little. The second is spectral: the edge-switching step that proves compares of two graphs through the Rayleigh quotient, and needs a positive Perron vector and the variational characterization of the largest eigenvalue for symmetric matrices. A purely combinatorial edge-maximization argument does not work: the fan is not the only outerplanar graph with edges, so maximizing the number of edges does not identify the spectral maximizer.
SimpleGraph (Fin n); is the published WangKangXue.SpectralTuran.specRad, the largest eigenvalue of G.adjMatrix ℝ.RobertsonSeymour1986.GM5.PlaneDrawing with every vertex point in the closure of the unbounded component of the complement of the drawing. It is not replaced by a forbidden-minor characterization; such characterizations are theorems about outerplanarity, and would change which graphs compete in the maximization.IsSpecMax IsOuterplanar G: is outerplanar and no outerplanar graph on the same vertex set has larger . It is never weakened to a comparison with the fan.G ≃g fan n, with the fan on Fin 1 ⊕ Fin (n - 1).∃ N, ∀ n ≥ N.A complete development needs the Perron–Frobenius theorem for symmetric nonnegative matrices and the Rayleigh quotient characterization of , both of general use; the theory of outerplanar drawings; and the counting arguments of the lemmas. Contributions to any of these layers are welcome, as are independent proofs of the outerplanar facts from the drawing definition.
Unit commitment (UC) is the day-ahead decision of an electricity system operator: which generators to switch on in each hour of the next day, and how much each of them should produce. System operators solve UC problems every day, and their cost and reliability are first-order concerns of power-system operations. With a large share of wind and solar generation, the net load (demand minus renewable output) at each node is uncertain at commitment time, and robust optimization is one of the standard ways to commit units that remain operable for every load trajectory in an uncertainty set.
The robust UC literature first adopted the two-stage model (Jiang et al. 2012; Zhao and Zeng 2012; Bertsimas et al. 2013): commitments are chosen first, then the dispatch is chosen after the whole day's net loads are revealed. In reality the operator learns the loads hour by hour, so the dispatch at hour may only use what has been observed up to . Lorca, Sun, Litvinov and Zheng (2016) introduced the multistage robust UC model that imposes this non-anticipativity, and asked when the extra realism matters. Their answer is this mission's goal: it matters only through the ramping constraints.
There are generators , net-load nodes , lines and hours .
The two-stage robust UC (2) minimizes over
where the dispatch is chosen knowing the whole trajectory . The multistage robust UC (5) minimizes over
over policies that depend only on and satisfy the dispatch constraints for every .
With the ramping constraints deleted from both models,
and consequently the two problems have the same optimal value over .
Both sides are compared with problem (1P), whose objective is
On a two-bus, two-hour system with line limit and ramp rates equal to , the two-stage model is feasible (Proposition 1), yet under its commitment no causal dispatch policy is feasible (Proposition 2). These show that the hypothesis "without ramping constraints" cannot be dropped.
The theorem locates exactly where multistage robust UC differs from the two-stage model: in the inter-temporal coupling created by ramping. Without ramping, the hourly dispatch problems decouple and so does the uncertainty set, so seeing the future gives the dispatch no advantage. With ramping, Example 1 shows the two-stage model can certify a commitment that fails in real-time operation. The practical message drawn in the paper is that the multistage model is useful precisely when ramping capability is a scarce resource, which is the situation of systems with high renewable penetration.
The result is proved in the paper. As far as is known it has not been machine-checked. This mission produces a formal model of robust UC (commitment logic, network-constrained dispatch, budget uncertainty, non-anticipative policies) together with a checked proof of the equivalence and of the counterexample. The model is a reusable base for later formal work on robust and multistage power-system models, such as the affine-policy results of the same paper.
The two separability steps are short on paper but must be carried out in the extended reals, where infeasible dispatch problems have value and sums of extended reals are not well behaved in general; the argument has to show that no arises. The main gap is the multistage side. The paper passes from the policy formulation (5) to the nested max-min formulation (6) by a remark, without proof. Formally, the value of an optimization over non-anticipative policies, which are functions on the whole uncertainty set, has to be identified with a backward max-min recursion over the per-hour sets, in both directions and without any attainment of the minima. A tempting shortcut, defining the multistage model as the nested formula, would prove nothing about policies and is excluded.
Fin T, 0-based: Lean period is the paper's . Generators, nodes, buses and lines are Fin Ng, Fin Nd, Fin Nb, Fin Nl.EReal; an infimum over an empty set is , the paper's convention for infeasibility.Contributions welcome: proofs of the milestones and the goal, and lemmas on infima and suprema of sums over product sets in EReal, which are reusable beyond this mission.
First-order methods such as the gradient method, Nesterov's accelerated method and the Heavy-ball method are usually analysed one at a time, each with its own hand-built potential function. Lessard, Recht and Packard (SIAM J. Optim. 26(1), 2016; read here in arXiv:1408.3595v7) observed that such a method is a linear dynamical system in feedback with the gradient map, and that tools from robust control, the integral quadratic constraints (IQCs) of Megretski and Rantzer (IEEE TAC 42(6), 1997), turn the question "does this method converge linearly, and at what rate?" into the feasibility of a small semidefinite program. The size of that program depends on the algorithm, not on the dimension of the optimization problem.
The paper's main result, Theorem 4, is the certificate behind this approach. It has been the starting point of a line of work on automated and computer-aided analysis of optimization algorithms, including the design of new methods with provably optimal rates.
An iterative algorithm is a linear system with state , driven by an input and producing an output :
The loop is closed by a map from sequences to sequences, . For the gradient method, , , and .
Instead of itself, one uses a constraint that is known to satisfy. A filter is a second linear system with state , inputs and output :
Given a reference point , the pair is the fixed point of the filter: and . Assume (all eigenvalues of have modulus less than one) and let be a symmetric matrix. The map satisfies the -hard IQC defined by if, for every input sequence , with and ,
It satisfies the pointwise IQC if each term is nonnegative.
Eliminating , the systems and combine into one linear system with state :
The condition number of a symmetric positive definite is , and is the Euclidean norm.
Let be a fixed point of and (, , and the filter equations above), let , and suppose satisfies the -hard IQC defined by . If there are and with
then every trajectory of the interconnection, , satisfies
The milestones follow the paper's proof: the elimination (3.6) of ; the one-step inequality (3.10) obtained from the LMI at a fixed point of (3.7); its weighted telescoped sum; the decay in the -weighted norm; and the passage to the Euclidean norm with the factor . Two companion statements are included: a pointwise IQC implies the -hard IQC for every (the remark after Theorem 4), and Proposition 2 (for ), the Lyapunov characterisation .
Theorem 4 reduces a statement about all functions in a class, for instance all strongly convex functions with Lipschitz gradients in every dimension, to a semidefinite feasibility problem with a handful of variables. The paper uses it to recover the known rates of the gradient method and to compute numerically certified rates for Nesterov's method, and the same template underlies later rate certificates for proximal, operator-splitting and distributed methods. The pointwise remark is what lets the sector IQC of gradients be plugged in directly.
The theorem is proved in the paper; nothing about it is open. To our knowledge neither the IQC framework nor Theorem 4 has a machine-checked proof. A formal development gives the first verified version of the certificate, and with it a route by which a numerically found LMI solution, once checked exactly, yields a verified convergence rate for a concrete algorithm.
The argument is short; the difficulty is in the bookkeeping. The IQC is a statement about every input sequence, while the conclusion concerns one trajectory of the closed loop, so the proof has to instantiate the IQC at the trajectory's own output and match the filter state it produces with the -component of the combined state. The weights must line up with the telescoping of the one-step inequality, and the final step needs the eigenvalue bounds together with the fact that removes the filter state from the initial error. Block matrices indexed by sums of index types make each of these steps heavier in Lean than on paper.
Vectors are Fin n → ℝ, matrices are Matrix (Fin a) (Fin b) ℝ, and sequences are ℕ → Fin n → ℝ indexed from . The norm is written out as , because Mathlib's norm on Fin n → ℝ is the sup norm, under which the constant would be wrong. The combined state lives on Fin nξ ⊕ Fin nζ and the LMI on (Fin nξ ⊕ Fin nζ) ⊕ Fin d, assembled with Matrix.fromBlocks, fromRows and fromCols; "" is positive semidefiniteness of the negated matrix. is the largest over the smallest eigenvalue of the Hermitian matrix , and is stated over the complex spectrum.
The page allows ; since the weights are undefined at , every statement that uses them assumes . Proposition 2 is printed without a sign condition and is false for ; it is stated for . The IQC hypothesis quantifies over every input sequence and every , with the filter started at ; replacing it by the IQC along the single closed-loop trajectory, starting the filter at , or reading as the sup norm would each change the theorem, and none is the formalization. The trajectory in the goal is universally quantified ("for any "); its existence is not assumed. The hypotheses and are kept as on the page although the proof does not use them. A sanity instance outside the proposal (the scalar gradient method with the sector IQC, , , ) checks in Lean that all hypotheses of the goal can hold at once.
The development needs only Mathlib's linear algebra: block matrices, PosDef/PosSemidef, the spectral theorem for Hermitian matrices, and finite sums. The Euclidean-norm lemma (decay in a -norm implies decay in the Euclidean norm with factor ) and Proposition 2 are reusable beyond this mission. Proofs of any milestone, and of Proposition 2 in either direction, are welcome.
For a finite graph, the Cheeger constant measures how hard it is to cut the vertex set into two pieces, and the spectral gap of the graph Laplacian measures how fast random walks mix. The two Cheeger inequalities (Dodziuk 1984; Alon and Milman 1985; Alon 1986) bound each quantity by a function of the other, and they underlie the theory of expander graphs, with uses in derandomization, error-correcting codes and the analysis of Markov chains.
High-dimensional expanders extend this theory from graphs to simplicial complexes. Linial and Meshulam (2006) and Gromov (2010) introduced combinatorial and topological notions of expansion for complexes; the spectral side is Eckmann's discrete Hodge theory (1944), in which each dimension carries its own Laplacian. Parzanchevski, Rosenthal and Tessler (arXiv:1207.0638, Combinatorica 2015) defined a -dimensional Cheeger constant through partitions of the vertices into blocks and proved the analogue of the upper Cheeger inequality, , for complexes with a complete skeleton. This mission formalizes that theorem.
Let and . A finite -complex with a complete skeleton on consists of all subsets of with at most elements together with a set of -element subsets, the -cells. A set of vertices is a -cell; is therefore the set of all -element subsets.
Each cell is oriented by the increasing order of its vertices, with . The space of -forms consists of the real functions on -cells, with inner product
The co-boundary and the boundaries , are
where means that and is a cell, and equals times the increasingly oriented cell when has smaller vertices in . The upper Laplacian is on , and is the space of -cycles.
The spectral gap is the least eigenvalue of on the cycles (Definition 2.1):
For sets , let be the set of -cells with exactly one vertex in each . The Cheeger constant is (Definition 1.1)
the minimum over partitions of into nonempty sets . For , is the space of functions summing to zero, is the graph Laplacian, and is the usual Cheeger constant .
for every finite -complex with a complete skeleton on vertices.
Milestones 2 and 5–7 hold for every partition, not only a minimizing one.
The result. Theorem 1.2 shows that a large spectral gap forces every partition of the vertices into blocks to be crossed by many -cells, so spectral information certifies combinatorial expansion of a complex. The paper uses it with the spectral analysis of Gundert and Wagner to show that Linial–Meshulam random complexes have Cheeger constant of order for large (Corollary 1.3). The paper also shows that the converse direction fails: a triangulation of the Möbius strip has but , so no lower bound of the form holds.
Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked proof exists. A formal proof requires a signed simplicial chain complex with explicit orientations, the adjoint relation between boundary and co-boundary, and a Rayleigh-quotient bound for a symmetric operator on an invariant subspace. These are the basic tools for any further formal work on spectral high-dimensional expansion, including the Mixing Lemma of the same paper (the companion mission of this series).
The graph proof plugs a two-valued test function into the Rayleigh quotient. In dimension the test vector must be a -cycle, and an indicator of a block is not one. The paper's form (4.1) assigns to a -cell whose vertices meet distinct blocks the size of the missing block, with the sign of a permutation of the blocks. Showing that this form is a cycle and that its co-boundary has absolute value exactly on and elsewhere is a case analysis over how the vertices of a cell fall into blocks, and every case depends on the orientation signs. A convention error in any of the operators or in the form makes one of these identities fail. A second, smaller difficulty is that is a minimum over the spectrum on a subspace, so the Rayleigh bound must be proved for restricted to , which it preserves.
Fin n; a complex is a structure holding its -cells as Finset (Finset (Fin n)), each of size ; the complete skeleton is built into the type. Complexes without -cells are allowed.EuclideanSpace ℝ over the subtype of -element vertex sets, so no form is supported on sets of the wrong size. is modelled on all -element sets; vanishes off and ignores values there.Fin n; the sign of vertex in cell is . Boundary and co-boundary are both defined by their formulas; their adjointness is milestone 3.sInf. The goal states that some eigenvalue of on (a nonzero cycle with ) is at most the Cheeger ratio of every partition, which is equivalent to . A partition is a family A : Fin (d+1) → Finset (Fin n) of nonempty, pairwise disjoint sets covering the vertices.sInf (empty sets give ), unsigned boundaries (for which ), cocycles in place of cycles (on which is zero), and arbitrary disjoint families in place of partitions (empty blocks give ratio ).LinearMap.IsSymmetric), and counting cells by blocks of a partition. The chain-complex and adjointness lemmas are reusable in any formal development of simplicial Hodge theory; contributions there are welcome.Tensor decompositions express a multiway array as a sum of simple terms. The canonical polyadic decomposition (CPD) writes an -th order tensor as a sum of outer products of vectors; block term decompositions replace each rank-one term by a term of higher multilinear rank. These models are used in signal processing, blind source separation and telecommunications, and are computed numerically by minimizing a least-squares misfit.
Sorber, Van Barel and De Lathauwer (SIAM J. Optim. 23(2), 2013) introduce the (rank- rank-1) block term decomposition (BTD), which contains both the CPD and the rank- BTD as special cases, and develop optimization algorithms for it: nonlinear conjugate gradient and quasi-Newton methods built on the complex gradient, and Gauss–Newton and Levenberg–Marquardt methods built on the Jacobian. For the second family the central object is the Gramian of the Jacobian of the residual. Theorem 4.5 of the paper gives its exact block structure, and that structure is what lets the methods run without ever forming .
Fix modes with dimensions , a number of terms , and block sizes ; put . The BTD approximates by
where the inner sum runs over the columns of block . Here and .
The paper reads this as a structured CPD in rank-one terms. The first factor matrices are the , and the last are
where copies column of into the columns of block . The residual tensor is
and the unknowns are . The Jacobian is the complex (holomorphic) derivative: is a polynomial in , not in .
Three auxiliary matrices enter the answer. The first is , the Hadamard product of the Gramians of the factor matrices outside a mode set , with entries . The second is , which satisfies (Proposition 4.1). The third is the block diagonal .
For every tensor and every ,
The goal has two parts, and both are required. The first is that the Gramian of the CPD Jacobian equals the explicit block matrix. The second is the factorization through .
With Theorem 4.5, is determined by the factor matrices and the small Gramians . For a hypercubical CPD this takes extra memory instead of the of a dense Gramian. Theorem 4.6 of the paper then turns the same structure into a matrix–vector product in operations, which is what inexact Gauss–Newton and Levenberg–Marquardt steps solved by preconditioned conjugate gradients require. The block-diagonal part also gives the block Jacobi preconditioner of the paper's §4.2. For the CPD, expressions for the Gramian were already studied in chemometrics (the paper cites G. Tomasi's 2006 thesis for this); Theorem 4.5 states the block structure in closed form and extends it to the structured BTD through .
The result is proved in the paper. As far as a search of Prove2Me and Mathlib shows, nothing about CPD or BTD Jacobians has been formalized. This mission produces a machine-checked proof of the block structure, starting from an explicit model of the decomposition and an honest complex derivative. That model (outer products, the structured CPD, , , the Hadamard-Gramian products) can be reused for the paper's cogradient theorem and for other tensor algorithms.
The identity is finite-dimensional, but no single step reduces it to a known lemma. First, is a genuine derivative of a multilinear polynomial map in complex variables, so each entry has to be computed from the derivative of a sum of products. Second, is a sum over all multi-indices. Turning it into the product of Gramians in means exchanging a sum of products with a product of sums while one or two modes are held fixed, with the conjugates landing on crossed column indices (, ). Third, the structured factor matrices are not unknowns. The derivative with respect to has to go through the chain rule and the vec–Kronecker identity, and 's rows and columns are indexed by different sets.
All objects are defined in TensorBTD.Gramian.Setting, with the following conventions.
Fin P ⊕ Fin Q (mode is Sum.inl (p-1) and mode is Sum.inr (q-1)), so all indices are 0-based. The columns are Σ r : Fin R, Fin (L r) in lexicographic order, which is the order of (3.5).Matrix.vec. This is the paper's Definition 2.5 with its misprint corrected to . Kronecker products are Mathlib's ⊗ₖ.deriv of at . It is not defined by its closed form, and it is not a real derivative.There are no hypotheses. The paper's assumptions that and its qualifiers "nonzero" and "rank-" are not used in Section 4, so they are dropped. This is a generalization: gives the plain CPD in terms.
A goal that took the closed form of as the definition, or that defined entrywise by the outer-product formula of milestone 1, would only state a sum identity. Both are ruled out: is a derivative, and the goal asserts that the Gramian of the CPD Jacobian equals the closed form. A misprint in the proof's closing paragraph, for the block, is corrected in Lean to .
Useful Mathlib infrastructure includes Matrix.vec, Matrix.kroneckerMap, Matrix.blockDiagonal', Finset.prod_univ_sum and the derivative rules for finite products (HasDerivAt.finset_prod). General lemmas welcome as contributions: derivatives of multilinear maps along coordinate directions, the sum–product exchange over Fintype.piFinset, and the chain rule for a Jacobian composed with a linear map.
Distance covariance was introduced by Székely, Rizzo and Bakirov (2007) as a measure of dependence between random vectors in Euclidean spaces: it is zero exactly when the vectors are independent, and its empirical version gives a consistent test of independence that needs no moment beyond the first. Lyons (2013) asked for which metric spaces the same holds. His Theorem 3.11 shows that it holds whenever both spaces have strong negative type. This mission formalizes the complementary result, Proposition 3.15 of the same paper: the hypothesis on the space cannot be removed. Without negative type, distance covariance can even be negative; without strong negative type, it can vanish on a law that is not a product. Together with Theorem 3.11, the proposition locates the boundary of metric spaces on which distance covariance is a valid test of independence.
Timeline. 2007: Székely, Rizzo and Bakirov define distance covariance on and prove the independence characterization there. 2013: Lyons extends the theory to metric spaces of negative type, characterizes the spaces where it remains a test of independence as those of strong negative type, and proves Proposition 3.15. 2018 and 2021: two errata by the author correct several statements of the paper; the first of them adds the standing assumption that all metric spaces are separable. Proposition 3.15 is not affected by the corrections.
Let and be separable metric spaces, each with its Borel -field. A finite Borel measure on has a finite first moment if for some point . For such put
and define the doubly centred distance . For two probability measures with finite first moments, is the energy of their difference,
Let be a Borel probability measure on whose marginals on and on have finite first moments. Its distance covariance is
is a product measure if .
has negative type if for every , all points and all reals with ,
On such a space for all probability measures with finite first moments, and has strong negative type if moreover equality holds only when . Write for the point mass at .
Let have at least two points.
The space is arbitrary apart from having two points, so the statement fixes nothing about it.
The result. Theorem 3.11 of the paper shows that strong negative type of both spaces suffices for to characterize independence. Proposition 3.15 shows the hypothesis on each factor is necessary: a single failure of (3.1) already produces a law with negative distance covariance, so is not even a nonnegative quantity there, and a single pair of distinct laws with produces a dependent law that the test cannot detect. Consequently, any use of distance covariance on general metric data (graphs, spaces with , spaces of distributions under Wasserstein metrics) has to verify strong negative type first. Since the two-point space is arbitrary, the failure is a property of alone.
Formalizing it. The proposition is proved in the paper; no machine-checked proof of it, or of any result about distance covariance, is known to exist. The mission produces a formal definition of distance covariance on separable metric spaces, of negative and strong negative type in the paper's measure-theoretic form, and the computation of on two-point mixtures. These are the same objects as in the sibling mission on Theorem 3.11, so the two together give a formal account of when distance covariance characterizes independence.
The step the paper calls "a little algebra" is the bulk of the work: is a four-fold integral of a product of doubly centred distances, each of which is itself built from integrals against a marginal of , and every manipulation of it happens inside Bochner integrals over product measures whose integrability has to be derived from first moments alone. In a formal setting nothing about these integrals is automatic. The passage from a violation of the finite-sum condition (3.1) to two probability measures with is left implicit in the paper. The non-product claim also uses a fact the page does not state: that , which follows from and is false without it.
All metric spaces carry their Borel -field and are assumed second countable, which for metric spaces is separability; this is the author's own correction, Errata (i), which makes measurable on the product. Measures are Mathlib measures with values in ; mixture weights such as , and enter as extended nonnegative reals, and is always restricted to . Because Mathlib's Bochner integral does not integrate against signed measures, is defined as the bilinear energy expansion displayed above. "Not a product measure" means differs from the product of its own marginals, never from some other product.
Several formalizations of this statement would be trivially true and are excluded. A Bochner integral of a non-integrable function is in Lean, so every statement either assumes or concludes the finite first moments that make and genuine integrals. Negative type is the finite-sum condition (3.1) and strong negative type the measure condition of p. 11, never an embedding property. The product condition is tested against 's own marginals, not against free factors. is quantified before is chosen, and part 2's hypothesis is the full negation of strong negative type, which includes spaces of negative type.
A complete development needs integrability of under from first moments (Lemma 2.1 of the paper), linearity of the energy in each measure, push-forwards of mixtures of product measures, and the intermediate value theorem. The integrability and energy-bilinearity lemmas are reusable for any work on energy distance or distance covariance. Contributions of these general lemmas, as well as of proofs of the individual milestones, are welcome.
Distance covariance is a statistic for testing whether two random variables are independent. Székely, Rizzo and Bakirov introduced it for Euclidean spaces (Ann. Statist. 2007): the population distance covariance of a joint law is exactly when is a product measure, so a consistent test of independence follows. Lyons (arXiv:1106.5758) extended the statistic to arbitrary metric spaces and showed that the characterization of independence holds on a pair of metric spaces precisely when both have strong negative type (his Theorem 3.11 and Proposition 3.15). That makes strong negative type the property a statistician has to check before using distance covariance on a given space. Functional data, the main case in practice, live in Hilbert spaces.
This mission formalizes Lyons's Theorem 3.16: every separable Hilbert space is of strong negative type. Kosorok (2009, cited by Lyons) had asked whether the characterization of independence extends to Hilbert spaces.
Timeline.
Let be a separable metric space with its Borel -field. A Borel probability measure has a finite first moment if for some . For two such measures write and
the integral of against the square of the signed measure .
The space has negative type if, for all , all and all real with ,
By approximation, negative type gives for all probability measures with finite first moments. The space has strong negative type if it has negative type and only when . Strict negative type is the same condition restricted to finitely supported measures.
The proof works on and uses the following objects. is the law on of an IID standard normal sequence ; is Lebesgue measure on ; . For put . The Gaussian Crofton embedding sends to the function
on . For probability measures on , its barycenter at is the function .
The goal has no constants. Each milestone states a claim of the paper in the paper's strength.
The result. With Theorem 3.11, Theorem 3.16 shows that for random elements of separable Hilbert spaces, zero distance covariance is equivalent to independence. Distance-covariance tests are therefore consistent for curves, images and other functional data. It also yields Corollary 3.18: if is a separable metric space of negative type, then has strong negative type, so a test of independence is available on every separable space of negative type after a change of metric. Remark 3.17 shows that separability cannot simply be dropped: a non-separable Hilbert space is of strong negative type exactly when its dimension is a cardinal of measure zero.
The formalization. The theorem is proved, and to our knowledge no proof of it, or of negative type of Hilbert spaces, is machine-checked. A complete development needs four things:
Measure.infinitePi and gaussianReal;Each of these is reusable outside distance covariance: the first in Gaussian measure theory, the last whenever laws on sequence spaces are compared.
The first idea is to approximate. Euclidean spaces have strict negative type, finite-dimensional projections of a Hilbert space are Euclidean, and probability measures are limits of finitely supported ones. Approximation preserves the inequality , but it does not preserve the equality case. A limit of strictly negative quantities may be even though . Remark 3.3 of the paper exhibits a space of strict but not strong negative type, so this gap is real.
The second idea is to transport the finite-dimensional Crofton embedding, in which is the measure of half-spaces separating and . It fails because has no rotation-invariant Lebesgue measure on its half-spaces. The Gaussian measure replaces it. But is defined only -almost surely, and its exceptional set depends on . As a result, " almost everywhere" does not immediately give information for every direction and level . That passage from almost every to every is the step the 2018 Errata had to justify.
Lean conventions, all disclosed in the items:
InnerProductSpace ℝ H with CompleteSpace H, as Errata (viii) prescribes; a complex space has the distances of its realification. Separability is SecondCountableTopology, which matches the standing separability of Errata (i). is lp (fun _ : ℕ => ℝ) 2 with the Borel -field, declared in the Setting file because Mathlib supplies none.Trivializing encodings are ruled out:
Contributions are welcome on any milestone. The reduction of a general separable to (by an isometry onto a closed subspace) is not posed separately and belongs to the goal's proof. Mathlib's Measure.ext_of_charFun, for finite measures on complete second-countable real inner product spaces, is a natural tool for milestone 5. Separability of lp is not yet an instance in Mathlib.
Testing whether two random quantities are independent is one of the basic tasks of statistics. Classical correlation only detects linear dependence. Distance covariance, introduced by Székely, Rizzo and Bakirov (Ann. Statist. 2007) for random vectors in Euclidean spaces, is a dependence measure that vanishes exactly under independence. It only needs the distances between sample points, and its empirical version is a simple V-statistic. These properties made it a standard tool for nonparametric independence testing.
Lyons (Ann. Probab. 41 (2013), arXiv:1106.5758) asked in which metric spaces this characterization of independence survives. The answer is the class of metric spaces of strong negative type, which includes all separable Hilbert spaces. On such spaces, distance covariance gives a test of independence that is consistent against every alternative. This mission formalizes that result, Theorem 3.11 of the paper, together with the chain of results its proof rests on.
Timeline. Schoenberg (1937, 1938) characterized metric spaces of negative type by isometric embeddings of into Hilbert space. Székely, Rizzo and Bakirov (2007) defined distance covariance on and proved that it vanishes only under independence. Lyons (2013) extended the theory to general metric spaces and identified strong negative type as the exact condition. The Errata (Ann. Probab. 46 (2018), 2400–2405; included in arXiv:1106.5758, pp. 24–29) added a standing separability assumption and repaired a gap in Lemma 3.8. The Second Errata appeared in Ann. Probab. 49 (2021).
Let and be separable metric spaces with their Borel -fields. A finite measure on has a finite first moment if for some (equivalently every) . For such define
For a probability measure on whose marginals and have finite first moments, the distance covariance is
is a product measure if .
has negative type if for all , all points and all real weights with . For finite measures with finite first moments, is the integral of against . On spaces of negative type for probability measures . The space has strong negative type if, in addition, only when .
An embedding is a map into a real Hilbert space with . Its barycenter map is . The tensor embedding takes values in the Hilbert tensor product . denotes the finite signed measures whose variation has finite first moment. denotes those on the product whose variation has marginals of finite first moment.
If and have strong negative type and the marginals of the probability measure have finite first moments, then
The converse, that a product measure has (p. 5), is included as a companion statement.
The result. Theorem 3.11 makes the empirical distance covariance a consistent test of independence against all alternatives on any pair of separable metric spaces of strong negative type. Examples are separable Hilbert spaces and their subsets, and every space of negative type after replacing by , . Its companion, Proposition 3.15 (a separate mission of this series), shows that strong negative type is exactly the right hypothesis. Proposition 3.7 also identifies distance covariance with Brownian covariance and with the original Euclidean definition, through specific choices of embedding.
Formalizing it. The result is proved, with the gap in Lemma 3.8 closed by the Errata (2018). No part of it has a machine-checked proof that we know of. A formalization needs barycenters of Hilbert-space-valued maps against measures, the Hilbert tensor product of two real Hilbert spaces, and Schoenberg's embedding theorem. None of these is in Mathlib in this form, and all are reusable well beyond distance covariance.
The obvious route reads as "the barycenters of and of coincide in " and concludes by injectivity. Strong negative type only gives injectivity of on probability measures, while is a signed measure on a product space. Getting from injectivity on single factors to injectivity on of the product is where the original proof had a gap: an auxiliary signed measure built from was not shown to have a finite first moment. The errata version changes the embeddings so that this can be done. Two smaller obstacles are integrability (the definition of is meaningful only by Lemma 2.1) and the construction of the Hilbert space in Schoenberg's theorem.
All spaces are Lean metric spaces with their Borel -fields and SecondCountableTopology. This is the separability the author adds in Errata (i), which makes measurable on the product. Measures are Mathlib Measures. A probability on has marginals θ.map Prod.fst and θ.map Prod.snd. "Product measure" means equals the product of these marginals. Hilbert spaces are real (Errata (viii)). Existential embeddings land in , which suffices for separable spaces. The Hilbert tensor product is the completion of the algebraic tensor product with its inner product. is defined by its bilinear expansion. Injectivity on and is stated for pairs of finite measures, which is equivalent to injectivity on signed measures via the Jordan decomposition.
Every integral here is a Bochner integral, which is for a non-integrable integrand. Each statement therefore carries the finite-first-moment hypotheses of the paper, and integrability itself is a milestone. Negative type and strong negative type are defined by (3.1) and by the condition on , not through an embedding or a barycenter map, so Schoenberg's theorem and Proposition 3.1 are not definitional. A statement with a "product measure" whose factors are free, or with dcov defined without the moment hypotheses, would be a different and trivializable theorem.
Welcome contributions: barycenter calculus for Hilbert-valued integrals, tensor-product integrals, Schoenberg's theorem, and proofs of any milestone.
A retailer that personalizes the set of products it shows to each customer needs to know who its customers are. In the low-rank multinomial-logit model of Kallus and Udell, Dynamic Assortment Personalization in High Dimensions (arXiv:1610.05604), every arriving customer belongs to one of customer types, and the type of each arrival is drawn independently from an unknown type distribution . Planning a non-personalized assortment, or weighting the per-type preference estimates, requires an estimate of from the observed types. When is large (types may be fine-grained customer profiles), the question is how many observations are needed before that estimate is reliable, and in which norm.
Theorem 4 of the paper answers this for the simplest estimator, the empirical frequencies, with an explicit, non-asymptotic bound in every norm, . The bound has two regimes: one that is good when the sample size is only slightly larger than , and one that is good when is large compared with .
Customer types are labelled . The type distribution is a vector in the probability simplex
The observation model (Sec. 3.2, p. 13) consists of records , : the type of the -th customer, the item the customer chose, and the assortment offered. The types are independent and identically distributed with . The items and assortments play no role for the type distribution.
The empirical type frequencies (Sec. 3.2.1, p. 14) are
For and the norm is , and ; the convention at is used throughout.
The proof works with the empirical Rademacher complexity of the sample: with the indicator vector of the -th type,
For every and , with probability at least ,
The goal keeps the paper's constants and its single statement over all , including .
The first term of the minimum shows that is consistent in every norm as soon as grows faster than , and gives -consistency in , i.e. in total variation. A coordinatewise argument alone cannot give this: for it yields a bound that does not vanish unless grows faster than . The second term is the sharper one in the regime , for instance in , where it gives the familiar rate. In the paper the estimate of enters non-personalized assortment planning, where the expected revenue of an assortment is averaged over types.
On the formalization side, the result is proved in the paper; nothing about it is open. As far as a search of the Prove2Me catalog shows, no machine-checked version of this statement, or of an concentration bound for empirical frequencies with these constants, exists. A complete development would also supply, in finite and elementary form, a coordinatewise Hoeffding bound for binomial proportions and an deviation bound for categorical samples, both reusable well beyond this mission.
The second term is a union bound and a binomial tail bound. The first term is where the work is. The obvious route, bounding each coordinate separately and summing, costs a factor in the norm and gives a useless rate when is comparable to . The proof instead treats as the supremum of an empirical process over the unit ball, controls its mean through the Rademacher complexity (where the absolute value of a sum of random signs must be bounded by ), and then needs concentration of the supremum around its mean with constants good enough to produce the stated and . The paper's p. 44 citation of a symmetrization result states it with the empirical rather than the expected complexity, so that step has to be redone with care rather than transcribed.
2b0104810fa9d656f2b79f8a44f791b2a3da388f3f6707564f4619da2050216a. Its printed page numbers equal the PDF page numbers.Fin m and draws Fin N, both 0-based. A sample is a map x : Fin N → Fin m.stdSimplex), which forces , and , added because is undefined for an empty sample. The milestones' tail bounds assume , which the paper leaves implicit. For the events are certain and the printed bounds can be smaller than .PiLp norm on for , with an extended nonnegative real; and use an exponent defined as at and otherwise. is the natural logarithm.Distributionally robust optimization handles an uncertain parameter whose distribution is only partly known. A decision must satisfy an expectation constraint for every distribution in an ambiguity set, the set of distributions consistent with the available information. Wiesemann, Kuhn and Sim (Optimization Online preprint 3757, 2013; Operations Research 62(6), 2014, doi:10.1287/opre.2014.1314) introduce a standardized ambiguity set. Its members are joint distributions of and auxiliary random vectors , constrained by expectation conditions and by probability bounds on conic confidence sets. Worst-case expectation constraints over such a set have tractable conic reformulations. The practical question is which kinds of distributional information this format can express. A set over describes information about through its -marginals, so the precise claim is that some set of distributions of equals the projection of a standardized set.
Section 3 of the paper settles this question for several common descriptors of dispersion. One of them is the absolute mean spread, the gap between the mean of a random variable above a threshold and its mean below it. Levi, Perakis and Uichanco used it to describe demand uncertainty in data-driven newsvendor models (Oper. Res. 63(6), 2015). The paper notes that, unlike variance or coefficient-of-variation bounds, spread information "can no longer be constructed via straightforward application of Theorem 5", its general lifting result for conic-representable moment bounds. Proposition 2 provides a dedicated lifting instead.
Fix , a threshold , a spread budget and a probability level . For a probability distribution on under which has a finite mean, write
The absolute mean spread of at is . The target set (spreadSet) consists of the with whose spread is at most .
The lifted ambiguity set (liftedSpreadSet) consists of the probability distributions of on with and , satisfying almost surely
The marginal is the law of under , and .
For the companion result, the Huber loss (8) is if and otherwise, for .
The page states the conclusion as for a given in the right-hand set. The set identity is the content, and it is the goal.
The milestones follow the two inclusions of the proof (pp. 40–41).
Combining them gives
and hence is contained in the target set. 2. For in the target set, and satisfy
Consequently equals the spread, and the target set is contained in . 3. A companion, Proposition 3, assertion 3 (p. 21): for and , the distributions with are exactly the -marginals of a lifted set on with auxiliary variables .
The proposition places absolute mean spread information inside the paper's standardized framework. Every result proved there for standardized sets therefore applies to spread-constrained ambiguity sets. The lifted set of Proposition 2 violates the paper's nesting condition (N), so Theorem 1's exact reformulation does not apply. Instead, Theorem 3 and Observation 1 give conservative approximations, which here are linear programs (p. 18). The Huber companion does the same for an expected Huber loss bound, a robust alternative to a variance bound.
Both results are proved in the paper. Neither has a machine-checked proof that this mission is aware of. A formalization adds three things: a checked equality of the two sets, with every integrability and positivity side condition made explicit; reusable lemmas on elementary conditional means of a scalar projection; and a check of the companion. The companion's printed proof contains an incorrect intermediate identity (see Difficulty), although the proposition itself holds.
The obvious reading of the inclusion target is "the constraint on bounds the spread pointwise". That reading fails, because the spread is a ratio of expectations over two complementary events, and and are not determined by . Only their difference is fixed, almost surely. The bound must hold for every coupling of with that respects the constraints. The reverse inclusion needs an explicit lift of an arbitrary . The lift has to meet the moment condition exactly, not just as an inequality. The paper leaves that step implicit.
In Lean the main friction is measure-theoretic bookkeeping: integrability of the auxiliary coordinates (which is derived, not assumed), set integrals over the two half-spaces, and push-forwards along the first projection. In the Huber companion, the identity the proof states for the minimized integrand is false in general: with and the left side is and the right side is . The inclusion needs a different pointwise inequality.
Fin nP → ℝ, with written f ⬝ᵥ z. The lifted outcome space is (Fin nP → ℝ) × (ℝ × ℝ × ℝ), and are the projections uOf, vOf, wOf. The Huber lift uses Fin 5 → ℝ with components .μ.map Prod.fst. Both theorems are stated as set identities between Set (Measure _).condMeanGe, condMeanLt). σ-algebra conditioning is not used. Both events have probability or , both positive because , so no division by zero occurs.Prod.fst are reusable beyond this mission. Proofs of the individual milestones are welcome, as are reusable lemmas on lifts of the form .A Markov decision process (MDP) is evaluated with a transition kernel that, in practice, is estimated from data. The expected total reward of a policy can be very sensitive to small errors in that estimate (Mannor, Simester, Sun and Tsitsiklis, 2007). Robust MDPs address this by letting the kernel range over an ambiguity set and optimizing the worst-case expected reward. Iyengar (2005) and Nilim and El Ghaoui (2005) showed that when the ambiguity set is (s, a)-rectangular (the transition law of each state–action pair varies independently of all others), the robust problem is solved by a robust Bellman recursion and a deterministic stationary policy is optimal.
Wiesemann, Kuhn and Rustem (Robust Markov Decision Processes, Mathematics of Operations Research 38(1), 2013) widen this to s-rectangular ambiguity sets, in which the transition laws of different actions in the same state may be coupled. Their Theorem 4.1 shows that robust policy improvement over such sets is still solved by a robust Bellman fixed point, but the optimal stationary policy may need to randomize. This mission formalizes that theorem and the chain of results its proof uses.
Timeline:
States form a finite set , actions a finite set . Choosing action in state and moving to pays a reward ; rewards are discounted by and the initial state has a known law in the probability simplex .
The uncertain parameter lies in
with symmetric negative semidefinite, bounded and containing a Slater point. Transition probabilities are affine in the parameter, for . The ambiguity set is the set of kernels , . It is s-rectangular if , where collects the blocks of members of : the parameter may be chosen separately in each state.
A stationary randomized policy assigns to each state a distribution over actions. It induces the Markov reward process
and the reward to-go . The worst-case expected total reward of is .
Two robust Bellman maps on carry the results:
In Lean these are phiEval and phiImprove, in the namespace WiesemannRMDP.SRect.
For an s-rectangular , has a unique fixed point , per-state maximizers exist, and the glued policy together with the constant function attains
Theorem 4.1 reduces robust policy improvement over s-rectangular sets to computing the fixed point of one map on , each evaluation of which is a finite convex program; the paper derives a polynomial-time method from it (Corollary 4.2). It also shows that the optimal policy is stationary but generally randomized, which separates s-rectangular from (s, a)-rectangular robust MDPs. Theorem 3.2 is the evaluation counterpart and is used again when the paper compares s-rectangular and general ambiguity sets (Proposition 3.10).
The results are proved in the paper; none is formalized. On the platform, the (s, a)-rectangular analogue with deterministic policies and costs (Nilim and El Ghaoui) and a related robust linear-programming characterization in another model (Derman, Geist and Mannor) exist, but neither covers coupled actions, randomized policies or rewards depending on the next state. A complete development would give machine-checked robust value iteration for s-rectangular sets and reusable facts on the reward to-go of a finite Markov reward process.
The obvious argument copies the nominal proof: the optimum of the constant- restriction is the fixed point , so the constant function is optimal. That only solves the restriction to constant ; the problems optimize over all continuous reward to-go functions , and showing that no non-constant does better is where s-rectangularity enters. Without it the claim is false: the paper's Example 3.11 gives a non-rectangular set where the constant bound is strictly below the worst-case reward. A second subtlety is that depends on only through the row , which is what lets per-state maximizers be assembled into a single policy; the maximizers are in general not deterministic.
States and actions are finite nonempty types; policies are functions satisfying the published IsPolicy, and the simplex condition on is the published IsTransitionKernel. and are built from the published InducedTransition and InducedReward. The model is a structure Model with the standing assumptions in Model.Standing. The reward to-go is defined by the series , not as the solution of the evaluation equation, so Proposition 3.1 (b) is not definitional. The minimum over and the maximum over are infima and suprema over subtypes, attained under the standing assumptions; the objective is used only for continuous on , and where arbitrary appear (the middle line of (10)) the infimum is taken in the extended reals. Inequalities on are componentwise; contractions are with respect to the sup norm. The paper's in (3b) carries the index , as elsewhere in the paper.
A statement that compares the fixed point only with constant reward to-go functions, or that takes and as hypotheses satisfying the conclusion, is not Theorem 4.1; the goal asserts existence and uniqueness of , existence of the maximizers, and optimality against every policy and every continuous feasible .
Useful infrastructure: Neumann series for times a row-stochastic matrix, continuity of infima over compact parameter sets, and contraction properties of min/max Bellman operators. Proofs of the milestones, and of nonvacuity of richer instances, are welcome.
The price of anarchy (POA) of a game measures how much selfish behaviour costs: it is the ratio between the largest cost of an equilibrium and the cost of an optimal outcome, for a nonnegative objective such as the sum of the players' costs. Since Koutsoupias and Papadimitriou (1999) and Roughgarden and Tardos (2002), POA bounds have been proved for routing, scheduling, facility location, auctions and many other models, mostly for pure Nash equilibria.
Pure Nash equilibria need not exist, are hard to compute in general, and are not what players running learning algorithms converge to. A bound that holds only at pure Nash equilibria therefore says little about realized play. Roughgarden's paper (J. ACM 62(5), 2015; conference version STOC 2009) observes that most known POA proofs follow one template, the smoothness argument, and proves that any bound obtained this way extends automatically to much broader equilibrium concepts. This mission formalizes the static half of that result: the extension to coarse correlated equilibria (Theorem 3.2) and to their approximate versions (Theorem 4.1).
Timeline:
A cost-minimization game has finitely many players . Player chooses a strategy from an arbitrary set ; an outcome is a vector , and player pays a real cost . Write for the outcome in which player switches to and the others stay put. The joint cost is , assumed nonnegative.
An outcome is a pure Nash equilibrium if for every and . For it is an -Nash equilibrium if .
A coarse correlated equilibrium is a probability distribution over outcomes with
and an -coarse correlated equilibrium satisfies the same with a factor on the right. Every pure Nash, mixed Nash and correlated equilibrium is a coarse correlated equilibrium, and coarse correlated equilibria are exactly the limits of play in which every player has vanishing external regret.
The game is -smooth if for every two outcomes
The robust price of anarchy is .
For every game with robust POA , every coarse correlated equilibrium and every outcome ,
Theorem 3.2 says that the robust POA of a game bounds the expected cost of every coarse correlated equilibrium, which contains every other equilibrium concept in the hierarchy. Combined with the companion result for no-regret sequences (Theorem 3.3, mission II of this series), it makes POA bounds meaningful for learning dynamics: whenever players use no-regret algorithms, their average cost is within the robust POA of optimal. For linear congestion games, which are -smooth, it yields the bound for all coarse correlated equilibria at once. Theorem 4.1 shows that the bounds degrade gracefully when the equilibrium condition holds only approximately, which covers equilibria computed to finite accuracy.
The results are proved in the paper; their proofs are short. No machine-checked version is known to exist. The mission's value is a reusable, platform-wide definition layer for cost-minimization games, smoothness, the robust POA and the equilibrium hierarchy, on which later results can be stated: the bicriteria bounds of §4.2, the tightness theorem for congestion games (mission III), and smoothness bounds for specific models such as auctions, routing and scheduling.
The mathematics is linear: it uses only linearity of expectation and one rearrangement. The difficulty lies in the encoding. The robust POA is an infimum over a set that may be empty (then on the page) and need not be attained. Passing from the fixed-pair bound to the infimum uses . Theorem 4.1's printed side condition is meaningless when and reverses its meaning when . Each of these must be handled so that the formal statement is neither false nor vacuous.
Players form a finite type with decidable equality, and strategy sets are arbitrary types with no finiteness assumed. Outcomes are dependent functions, and the deviation is Function.update s i s'ᵢ. Costs are real-valued, and are unconstrained reals except . Probability distributions are finitely supported weight functions that are nonnegative with total mass . Expectations are therefore finite sums with no integrability side conditions. This covers all finite games and all mixed and correlated equilibria of finite games, but not distributions with infinite support.
The robust POA is an extended-real (EReal) infimum over the smoothness pairs with , so it is when no such pair exists, and the goal compares the expected cost with in EReal. The goal carries two explicit hypotheses:
Without the second, a game with no smoothness pair and would be claimed to have expected cost at most (EReal sets ), which the page does not assert. A formalization in which the distribution may have total mass , or in which is an infimum over all pairs rather than over the smoothness pairs with , trivializes or falsifies the goal, and is ruled out by the definitions.
In Theorem 4.1 and the -Nash bound:
The -coarse correlated equilibrium is the extension of (15) that the paper says is "defined in the same way" as -Nash equilibria (p. 15). Remark 4.4 writes out the payoff analogue.
Claim (3)–(5) and the -Nash bound keep the paper's hypotheses and optimality of , although the inequalities hold without them. Example 4.2 is not posed: its printed bound should read .
Contributions welcome:
In online convex optimization, a learner makes a prediction before seeing the next loss. A standard regret guarantee often depends on a learning rate chosen using the size of the comparator that will be assessed later. That comparator is unknown during play. Chapter 13 of Orabona's textbook uses coin betting to obtain a bound that adapts to every comparator while the algorithm uses only its initial wealth and a bound on the observed subgradients. The coordinate-wise form allows the guarantee to reflect a comparator whose important coordinates differ greatly in size.
The motivating task is deterministic. An adversary may choose convex losses over successive rounds, and the performance measure compares the learner's cumulative loss with the loss of a single fixed vector. The algorithm is allowed to know the coordinate bound and its initial wealth parameter ; it does not know the final comparator or a suitable learning rate for it. The capstone is Theorem 13.9, p. 215, the chapter's coordinate-wise Krichevsky–Trofimov result.
There are rounds, numbered , in a space . In round the learner outputs , pays , and then receives a subgradient of the loss at . A subgradient supports the loss everywhere: for every . Each coordinate obeys . For a fixed comparator , regret is
The underlying KT bettor begins with wealth . Given coin outcomes , it wagers a fraction of its wealth before outcome arrives. Its signed wager is , and . The denominator is , including the first round, when the past sum and the wager are zero. Algorithm 13.1, p. 208 defines this update.
For optimization, Algorithm 13.3, p. 215 applies a separate KT update to every coordinate. With , the prediction is fixed by past gradients and past predictions:
This is the algorithm studied in the target theorem. A run includes the update and an admissible subgradient at each round; it is not an arbitrary sequence of predictions satisfying a bound after the fact.
The main target records both inequalities in Theorem 13.9. For every comparator ,
The milestone path consists of three statements drawn directly from the chapter: the gamma-potential one-step inequality (13.1), the continuous-coin wealth guarantee of Theorem 13.4, and the one-dimensional KT regret display in §13.2.1. The first controls the change in the betting potential, the second relates that potential to final wealth, and the third is the scalar guarantee used by the coordinate-wise theorem. All three retain the printed constants and the source's one-based indexing.
The first inequality charges each comparator coordinate according to its own magnitude. The second expresses the result using familiar and norms. Both apply to the same run without choosing a new algorithm for a new . At , the bound is , showing directly the cost of the initial-wealth choice. For a sparse or uneven comparator, the coordinate sum can be more informative than a bound that uses only the largest coordinate.
The mathematical results are proved in the cited textbook. This mission supplies Lean statements for those results; the theorem files are proof targets and do not yet contain machine-checked proofs. A completed development would connect the betting potential, the one-dimensional optimization reduction, and the coordinate aggregation through reusable lemmas. Its definition layer can also serve later formalizations of coin-betting algorithms with other wealth potentials.
The prediction uses a changing wager fraction determined by the previous outcomes. A direct fixed-fraction calculation does not describe that sequence of wagers. The chapter instead identifies a gamma-function potential that can be compared with the changing wealth at every round. For continuous coin outcomes, the potential must satisfy an inequality for every real , including interior values rather than only the binary endpoints.
The optimization guarantee adds another boundary: a lower bound on betting wealth must become an upper bound on regret for every real comparator. The desired expression has a logarithm, a square root, and the exact factor inside it. The coordinate-wise result must preserve the scalar constant in every coordinate and then justify the second inequality involving . These are the places where a weaker or altered constant would change the target.
Lean represents as functions Fin d → ℝ; its function norm is the sup norm, while the quantity is the explicit sum . The theorem assumes , , , and . These make the finite-dimensional setting nonempty and the printed quotients and logarithms operate on their intended domains. Time index zero is unused. All sums over rounds use .
Losses are real-valued and subdifferentiable on the whole space, as in Algorithm 13.3. The run records full-space subgradients selected at the learner's predictions and their coordinate bounds. This selected-gradient condition is sufficient for the printed regret inequalities; global boundedness of every possible subgradient is a stronger convention used in the one-dimensional prose. The gamma potential is a separate definition with Real.Gamma; its arguments are positive on the domains used by the wealth theorem. The bettor's wealth is a finite product of its exact per-round returns.
The formalization must keep the explicit update in the run predicate. Allowing to depend on the current , or replacing the update by a generic betting rule, would no longer state Algorithm 13.3's guarantee. Contributions are welcome on the gamma-potential inequality, the wealth bound, the one-dimensional regret bound, and the final coordinate aggregation. The supporting results should retain the chapter's constants and handle the first round and zero-valued coin outcomes.
Helly's theorem says that a finite family of convex sets in has a common point whenever every of its members do. Two of its best-known strengthenings weaken the hypothesis in different directions. The colorful Helly theorem, due to Lovász and first published by Bárány (1982), distributes the sets into color classes and only asks that every colorful choice of one set per class intersects. The fractional Helly theorem of Katchalski and Liu (1979) only asks that a positive fraction of the -tuples intersect, and concludes that a positive fraction of the whole family has a common point. Bárány, Fodor, Montejano, Oliveros and Pór (2014) combined the two into a colorful fractional Helly theorem, which they used to prove colorful and fractional -theorems.
Timeline:
Work in with . A color class is a finite indexed family of convex subsets of ; repetitions are allowed. Given color classes , a colorful choice is a tuple with , selecting the sets . There are colorful choices.
For : if at least colorful choices satisfy , then for some color there is with
If every colorful choice satisfies , then for some color .
Colorful Helly specializes to Helly's theorem by taking all color classes equal, and the colorful fractional theorem specializes to the fractional Helly theorem in the same way. Both are standard inputs in the theory of intersection patterns: colorful and fractional -theorems, Helly-type results for families with extra structure, and bounds on transversal numbers. Mathlib contains Helly's theorem and Carathéodory's theorem but neither colorful statement; this mission adds both as reusable, machine-checked results.
Helly's theorem alone does not suffice: the hypothesis only controls colorful tuples, so subfamilies with two sets of the same color are never assumed to intersect. The arguments need an extremal object attached to each colorful intersection (classically a lexicographic minimum or a lowest point) and a Helly-type reduction showing that this object is determined by at most of the chosen sets. The sets are not assumed closed or bounded, so a reduction to compact sets is also required.
is EuclideanSpace ℝ (Fin d); the color classes are a dependent family indexed by Fin (d+1) and Fin (N i), and a colorful choice is a dependent function (i : Fin (d+1)) → Fin (N i). The number of intersecting colorful choices is the cardinality (Set.ncard) of a set of such functions. Empty color classes are allowed; they make the statements trivially true, since an intersection over an empty index set is the whole space. The fraction is explicit rather than existentially quantified. Proofs of the optimal fraction would be welcome as a stronger follow-up.
A stochastic reaction network tracks the counts of chemical species as reactions occur. Different species and reaction rates may grow at different powers of a large system-size parameter. Kang and Kurtz's model-reduction paper uses these powers to identify candidate time scales and combinations of species that can remain bounded. Before a reduced model can be justified, the dominant reactions that increase a combination must be compared with those that decrease it. Condition 3.2 makes that comparison.
Checking the condition for every nonnegative linear combination is a large task even for a finite network: the weights range over a continuum, and changing a weight can change which reactions increase or decrease the combination. The paper's Lemma 3.4 relates this task to the directed graph of species. It says that combinations supported on different strongly connected components can be checked component by component. This mission formalizes that result and the claims in its proof that carry the reduction.
There are finitely many species and finitely many indexed reactions . Reaction consumes molecules of species and produces molecules of that species. The stoichiometric change is . Species has a nonnegative scaling exponent , and reaction has a real exponent . The effective reaction exponent is .
For a vector of nonnegative weights , the scalar is the change in its linear combination when reaction occurs. Write for reactions with positive change and for reactions with negative change. The balance equation equates the largest on these two sets. If that equation fails, the time-scale inequality permits a chosen exponent only when it is no larger than , the largest on the support of minus the largest on . Condition 3.2 is the disjunction of these two alternatives.
The species graph has an edge when one reaction consumes and produces . Its strongly connected components are the maximal sets of species that can reach one another by directed paths. A single species is a component when it shares no larger mutual-reachability class. A nonnegative vector supported in one such component is a component-level test vector.
The goal is Lemma 3.4, p. 15. Suppose , each is nonnegative and supported within one maximal strongly connected component, and distinct pieces belong to distinct components. For fixed , the lemma asserts all three implications:
The companion consequence on the same page quantifies over all nonnegative vectors: if any one of these properties holds for every vector supported in a strongly connected subgraph, then it holds for every vector. The milestones mirror the paper's proof: a chain of component pieces cannot revisit a piece; under Condition 3.2 the maximal positive exponent either satisfies the time-scale bound or is bounded by the maximal negative exponent; and the two uniform cases yield their respective alternatives.
Lemma 3.4 replaces a global family of tests with tests inside individual strongly connected components. In the paper this narrows the balance checks needed before the authors study separated time scales and reduced stochastic models. The uniform balance and uniform time-scale clauses matter separately: the first preserves equality of dominant positive and negative exponents, while the second preserves the same admissible across a sum of pieces. The general Condition 3.2 clause allows different pieces to satisfy different alternatives.
The mathematical result was proved in the 2010 arXiv preprint and published in 2013; it is not an open conjecture. This proposal supplies Lean statements and a reusable finite reaction-network vocabulary, with proofs left for solvers. The local sanity file checks the empty-maximum and zero-vector behavior without using sorry. The draft theorem files compile as statements, but their six proofs are not yet machine checked.
The obvious inequality for a sum says that a reaction increasing increases at least one piece. It does not say that the piece's dominant increasing reaction also increases the sum: contributions from other pieces can cancel it. Consequently, taking a maximum separately on each piece does not directly give the balance equation for the sum. The graph restriction is decisive because a sequence of compensating reactions would otherwise be able to cycle among pieces. The milestones isolate that no-repetition property and the two inequalities the paper obtains from it.
Species, reactions, and pieces are represented by Fin s, Fin r, and Fin m; these are zero-based versions of the paper's one-based indices. The stoichiometric coefficients are natural numbers, the changes and all scaling exponents are real, and . Following the standing restriction on p. 5, each reaction consumes at most two molecules. The paper's is computed from , , and , not supplied independently.
For a reaction set , uses WithBot ℝ, so the maximum of an empty set is , as the paper explicitly uses on p. 17. The support maximum in is an ordinary real maximum when relevant. The value is represented in EReal: when is empty, it is and the time-scale inequality holds for every real . Subtraction is performed in the reals before conversion to EReal. Thus zero vectors do not acquire a spurious bound from a default-valued maximum or extended-real subtraction.
An edge uses positive consumption and positive production in the same indexed reaction, matching the wording on pp. 4 and 15. Mutual reachability defines a component. Each piece is required to lie in one component, and different pieces in different components. These conditions prevent splitting a single component into separately balanced pieces, which would make the goal false. An empty family of pieces is permitted; its sum is zero. The definition file is useful for the other balance results in the paper, while the graph and component lemmas can support later work on reaction-network decomposition.
In a welfare sharing game, several players choose resources and receive shares of each resource's welfare. A rule for splitting welfare is useful only if the resulting players' incentives admit stable choices. The paper by Gopalakrishnan, Marden, and Wierman characterizes the distribution rules that guarantee a pure Nash equilibrium for every game formed from a specified class of local welfare functions. Its Appendix C supplies a complementary structural result: generalized weighted Shapley rules give the game a vector-valued potential. That structure provides a way to analyze equilibrium existence and dynamics without enumerating all possible unilateral deviations individually.
The scalar weighted-potential case was known for weighted Shapley values in the work of Hart and Mas-Colell, as Appendix C recounts. The 2014 paper extends the setting to an ordered system of priority blocks. A single scalar component cannot generally express the priority structure, so Appendix C uses a finite vector whose components are compared in order. This mission isolates that explicit potential theorem from the paper's separate characterization theorem.
Let be the players and the resources, with . Player chooses an action , possibly containing several resources. For a profile , let be the users of resource . Each resource has a local welfare function and a distribution rule , giving player 's share when the resource is used by coalition . The game's utilities are separable:
A weight system specifies positive weights and an ordered partition of the players. For a nonempty coalition , let be its members in the earliest block meeting . The Möbius coefficient of a welfare function is
The generalized weighted Shapley value distributes the contribution of among players in in proportion to their weights. The generalized weighted marginal contribution rule instead evaluates the difference in a welfare function when a player is removed from the part of a coalition in that player's block and later blocks. These are the two formulas in Tables 1–2 of the source paper. The ground welfare functions used by the two rules, and , may differ. Their coefficients are related by (12): for every nonempty .
A generalized weighted potential is a vector with a fixed component assigned to each player. For any unilateral change by that player, all earlier components stay equal, and the player's utility change equals a positive multiple of the change in the assigned component. This is the precise potential identity used in this mission.
The local target is equation (83): local resource potentials whose changes agree with each player's utility share combine into a game-level potential. The coefficient target is the equality between the Table 1 marginal-contribution rule and its Table 2 Möbius-basis expansion. The closed-form target identifies exactly which vector component each player can change.
The goal is Theorem 3, using its closed form (85). Write . If each is simultaneously the generalized weighted Shapley rule for and the generalized weighted marginal contribution rule for , with their coefficients related by (12), then
is a generalized weighted potential with player weights . The goal specifies this potential itself, rather than merely asserting that some potential exists.
The theorem gives an explicit structural certificate for all games built from these sharing rules. A maximum of a vector potential in lexicographic order is stable against improving deviations, so the identity supports the equilibrium guarantee in the main characterization result. Its formula also gives a concrete object for studying changes in allocations or comparing priority systems; these are uses of the result, not additional claims of this mission. The closed form is particularly useful because each component is an evaluation of a ground welfare function on a specified suffix of the priority partition, as the paper explains on p. 11.
The mathematical result was proved in 2014. The remaining formalization work is to construct a machine-checked proof of the exact vector identity, including the coalition basis calculation and the passage from local resource changes to whole-game utility changes. The local platform index contains related scalar and ordinal potential theorems, but no declaration with this paper's priority-block model and closed-form vector potential.
The obvious scalar-potential analogy does not by itself track ordered priority classes. Adding a player in one class can leave some vector components unchanged while affecting a later component. The proof obligation therefore includes the exact component order and a player-specific change identity, uniformly over coalitions and actions. A second difficulty is reconciling two descriptions of the same distribution rule: Table 1 uses a welfare difference, while Table 2 expands welfare in Möbius coefficients over coalitions. The equality must hold even when the welfare at the empty coalition is arbitrary.
There is also a printed inconsistency. Definition 1 and (83) call the assigned component the “first nonzero” component, but the proof only establishes that earlier components are unchanged. The assigned component can also be unchanged on a particular deviation, while a later one changes. Formula (84) disagrees with the closed form (85) in a two-block example. The mission follows the fixed per-player component supported by the proof and states (85); the precise counterexample is in the moderation notes.
Players and resources are represented by Fin n and Fin m, coalitions and actions by Finset, and real-valued welfare and utility functions by functions into . The standing model has and strictly positive player weights. The potential predicate requires , matching Definition 1's positive vector dimension. The ordered partition is a map from players into blocks; empty blocks are allowed, and Fin K provides zero-based indices. A vector component is indexed in reverse block order, so component 1 sees only the final block and component sees the whole coalition. For a nonempty , is its earliest occupied block; its empty-case value is empty and is never used in (12).
Rules are compared only for players belonging to the coalition in which they are evaluated. The named Shapley and marginal rules return zero off that coalition; arbitrary input rules may have other unused values there. No budget-balance or hypothesis is added; the empty-coalition value cancels in marginal differences. Action sets may be empty because this mission proves a potential identity for feasible deviations, without asserting that a feasible profile or equilibrium exists. The formalization does not replace the goal by a vacuous existence claim: it fixes the potential to the explicit closed form (85) and requires the full change identity at every feasible unilateral deviation.
The development needs finite-set sums, powersets, ordered finite indices, real arithmetic, and the paper-specific welfare rules. The local-to-global separability statement and finite coalition-basis calculation can be reused in related sharing games. Contributions proving the stated milestones, or strengthening the result under correctly stated extra assumptions, are in scope.
A suffix tree of a text answers pattern-matching and string-analysis queries (longest repeats, maximal repeats, matching statistics) in time close to optimal, but it occupies machine words. For highly repetitive collections, such as many genomes of one species or the versions of a document, this is far more than the information the text contains. A standard measure of that information is , the number of runs (maximal blocks of one repeated symbol) of the Burrows–Wheeler transform of . On repetitive collections is orders of magnitude smaller than , and indexes using words are of direct practical interest in bioinformatics and in versioned document stores.
Gagie, Navarro and Prezza (arXiv:1809.02792v2, 2019) build a compressed suffix tree in words (their Theorem 9, p. 28). A compressed suffix tree in the style of Abeliuk, Cánovas and Navarro (Algorithms 2013) needs the longest common prefix array in compressed form, and stores it differentially, as . The paper's route to compressing is one exact combinatorial fact: has a bidirectional macro scheme of size at most (p. 28). A cited conversion of macro schemes into run-length grammars (Lemma 18, from Gagie, Navarro and Prezza, LATIN 2018) then gives the grammar. This mission formalizes that combinatorial fact and the lemmas it rests on.
A text , , is a string over the alphabet whose last symbol T[n]=\=1T[i..]T[i]T[i+1]\cdots T[n]SA[1..n][1..n]$ listing the starting positions of the suffixes in increasing lexicographic order.
The Burrows–Wheeler transform is if and if : the symbol preceding the -th smallest suffix, read cyclically. The LF mapping is
where counts the symbols of smaller than and counts the occurrences of in . A position starts a run if or ; is the number of run starts, written .
Let be the length of the longest common prefix of two strings. Then
The differential suffix array is , .
A bidirectional macro scheme (BMS) of size on a sequence of any symbol type (Definition 6, p. 28, after Storer and Szymanski) is a partition into consecutive blocks, each either an explicit symbol (a block of length 1) or a pointer to another occurrence of the same content. The source map sends a position at offset inside a pointer block to . The scheme is correct if, from every position , some iterate , , is an explicit symbol.
This is the sentence following Lemma 16 on p. 28, proved by Lemma 17. It fixes no constant beyond the paper's own count, and it is the exact input Lemma 18 needs.
The result. The bound ties the compressibility of the array, a structure of size that does not obviously inherit the repetitiveness of the BWT, to the number of BWT runs. Through Lemma 18 it yields a run-length grammar of size for (Lemma 19, p. 29), and the paper's compressed suffix tree supports its navigation primitives on that grammar. The same pattern, runs of the BWT inducing copies in a differential array, drives the paper's -word access to and (§5), of which Lemma 12 is the first step.
Formalizing it. The result is proved in the paper; to our knowledge none of it, nor the basic theory of suffix arrays and the Burrows–Wheeler transform, has a machine-checked proof on this platform. The mission produces a self-contained Lean development of the BWT and LF mapping from their counting definitions, of the and arrays, and of macro schemes with their correctness condition. The single-cycle property of and the identity are folklore results that underlie every FM-index; they are formalized here from the counting formula, not assumed.
The obvious proof of the goal counts blocks: at most explicit symbols and at most regions. The counting is easy; the content lies in the two properties the count presupposes. First, the copies must be correct: a whole region must coincide with the stretch starting at , which needs to map a run onto consecutive positions and differences to be preserved, and it needs three consecutive equal BWT symbols, not two, because involves the suffixes in cells , and . Second, the scheme must be correct as a whole: following pointers must never cycle. A scheme in which two regions point at each other satisfies every local condition and still fails. Ruling this out requires the global fact that is one cycle through all of , which in turn rests on the lexicographic order of suffixes and the uniqueness of the terminator \$$. Connecting the counting definition of LFSA[LF(p)]=SA[p]-1$ is itself a nontrivial argument about ranks of symbols among sorted suffixes.
Positions are 1-based natural numbers, as in the paper. The text and the suffix array are functions read only on , symbols are natural numbers, and \=1[1..n]BWTLFT[0]T[n]LCP\operatorname{lcp}DLCPDSAij\ne i[1..n]fp_i+k\le np_0=-2p_1=1LFLFSA[LF(p)]=SA[p]-1SA[p]>1SA[p]=1$ it holds only cyclically.
The paper's space and time claims (Theorem 9, Lemma 19) and the cited grammar conversion (Lemma 18) are out of scope; the goal is their explicit combinatorial content.
Every sequence has a macro scheme of size (all symbols explicit), and a set of pointers that only point at each other satisfies every local condition, so a formalization that bounds the size of an arbitrary partition, or that drops the condition that every chain of copies reaches an explicit symbol, would be empty or false; both are excluded by the definition used. , and are not defined through the properties the milestones assert.
Contributions welcome: proofs of the milestones, and reusable lemmas about the LF mapping and lexicographic order of suffixes, which the paper's other missions (locating with sampled phrases, counting distinct substrings) also use.
A text index answers questions about occurrences of a pattern without scanning the whole text. One reason to compress such an index is that many stored texts are repetitive: multiple versions of a document or genome often share long passages. The Burrows–Wheeler transform (BWT) rearranges a text's symbols in a way that groups related contexts. A small number of equal-symbol runs in the BWT is therefore a useful measure of repetition. Gagie, Navarro, and Prezza use the number of runs to state space bounds for text searching and suffix-tree operations in Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space.
This mission isolates one exact counting result underneath those data-structure bounds. A length- substring is called an -mer. The number of different -mers measures how many local patterns the text contains; repeated occurrences of the same string count once. Lemma 9 of the 2019 preprint bounds this number directly in terms of BWT runs. The result makes a relation between two notions of text repetition precise: clustering in the BWT and diversity of fixed-length substrings.
Let be a text over the ordered alphabet . Its final symbol is a unique terminator \=1i\in[1..n]T[i..n]iSA[1..n][1..n]SA[p]p$th suffix. This is the setup of §2 of the source preprint, pp. 7–9.
The BWT symbol at position is the character just before the suffix at . When that suffix is the whole text and has no preceding character, its predecessor is read cyclically as T[n]=\$$. The BWT partitions into maximal runs of equal symbols; rT[i..j]$ is primary when its interval contains a sampled text position, as in Definition 5, p. 16.
For , let be the set of length- strings occurring in :
The braces matter: two windows with identical contents give one element. The final allowed window includes the terminator. The text is not padded in this definition.
Lemma 8, p. 17 states that every nonempty substring of has an occurrence with the same contents that is primary. With denoting sampled text positions, the assertion is
The mission's milestones also capture the suffix-array interval of a pattern, the sampled occurrence of each individual character, and the bound stated in the proof of Lemma 9. These give precise intermediate claims in the paper's route to the count.
The main goal is Lemma 9, p. 17:
Here is calculated from the BWT of the text's suffix array. Both inequalities on are part of the source statement. The bound concerns distinct strings of a fixed length, not the number of substring windows.
The theorem gives an explicit upper bound on the number of different length- strings that can appear when the BWT has few runs. In §4.2 the authors use it to bound the text area holding all distinct length- substrings; that area supports the alphabet-mapping component of their compressed index. This exact combinatorial assertion remains meaningful independently of a machine model or a choice of data structure. Its role in the broader construction is described around Lemmas 8 and 9, pp. 16–17.
The result is proved in the paper. The work here is to give its objects and claims machine-checkable statements and then close their proofs in Lean. The mission has not already supplied a machine-checked proof of these claims. A completed development would also provide reusable definitions of suffix arrays, BWT run boundaries, and finite sets of distinct substrings for later formalizations of compressed text indexes.
The count is immediate only after every substring can be represented by an occurrence containing a sampled position. A direct count of all starting positions cannot yield the claimed bound: may be large even when is small. The difficult step is therefore the primary-occurrence claim of Lemma 8. Its statement has to preserve both parts of “occurrence”: the replacement interval must have the same length and symbols, and it must stay inside the text. The suffix-array range used there depends on lexicographic order, while sampled positions are defined through changes between adjacent BWT symbols. Connecting those two views of the text is the central obstacle.
The Lean representation uses for symbols and 1-based positions. The functions and are read only on . An IsText hypothesis enforces , membership in , and the unique final terminator \=1SA[1..n]nTSAn$. Runs are counted by their starting cells; samples are the corresponding text positions from both ends of every run. The model follows the first sentence of Definition 1, including the last character of the final run. The source's following explanatory clause omits that endpoint.
The set of -mers is a finite set of lists formed from every valid window. It is not restricted to primary windows, which would make the goal a different and easier statement. A primary substring carries valid endpoints and a sampled position inside them. The formal statements do not assume that the desired primary occurrence exists; that is precisely the content of Lemma 8. The paper's space and time results are outside this mission: the goal is their explicit substring-counting content.
A complete proof needs elementary facts about list prefixes and lexicographic order, finite interval images, the BWT's run partition, and cardinalities of substring windows near samples. The definitions and interval lemmas can be reused by other missions on suffix arrays and compressed strings. Contributions proving any of the listed milestones or strengthening the surrounding reusable string infrastructure are within scope.
In a structured bandit problem a learner repeatedly chooses a decision from a set and observes a noisy reward whose mean is an unknown function from a known class . Classical analyses of such problems measure the complexity of by the eluder dimension (Russo and Van Roy, 2013; 2014) or the star number, and prove regret bounds for posterior sampling (Thompson sampling) or optimistic algorithms in terms of these quantities.
Foster, Kakade, Qian and Rakhlin (2021) introduced the Decision-Estimation Coefficient (DEC), a single complexity measure that yields both upper and lower bounds on the minimax regret of interactive decision making. Section 6.2 of that paper connects the DEC to the older parameters: it shows that the square-loss DEC is bounded by the disagreement coefficient of the class, a quantity introduced in Foster, Rakhlin, Simchi-Levi and Xu (2020) and itself bounded by the star number and the eluder dimension. The bound is certified by posterior sampling, so it also explains why posterior sampling works for these classes.
Let be a set of decisions. A model assigns to each decision a reward distribution; here a model enters only through its mean-reward function and an optimal decision . The class collects the mean-reward functions of a model class . A reference model , not necessarily in , has mean reward .
A prior is a finitely supported distribution over . The posterior sampling strategy plays , the law of when .
The prior-dependent square-loss DEC (display (70) of the paper) is
the best trade-off between regret and squared estimation error that a decision distribution can achieve against a model drawn from the prior.
For a class of functions and a distribution on , the disagreement coefficient (Definition 6.3) is
where is drawn independently of . It measures how much mass puts on decisions where some function of the class is large although it is small in . The shifted class consists of the differences , .
For every , posterior sampling certifies
In the formal statement, the objective of (70) evaluated at is bounded by for every and every upper bound of the disagreement coefficients of the shifted classes.
Theorem 6.2 bounds the DEC of any structured bandit class by its disagreement coefficient. With the bounds of the disagreement coefficient by the star number and the eluder dimension (Lemma 6.1 of the paper, from Foster et al. 2020) and the minimax theorem, it yields Theorem 6.1, which recovers the regret bound of Russo and Van Roy for posterior sampling as a special case, and gives a bound in terms of the star number. The decoupling lemma (Lemma E.2) is a general tool: it controls a coupled quantity by a decoupled second moment, and applies wherever an algorithm's decision and the function evaluated there are drawn from the same distribution.
The results are proved in the paper. None of them has a machine-checked proof; this mission produces the first formal statement of the disagreement coefficient and of the decoupling lemma, on which formal versions of eluder-dimension and star-number bounds can build.
The obvious argument fails at the decoupling step. The quantity evaluates each function at its own decision, while the estimation error controls only , with independent indices. For a finite set of decisions, Cauchy–Schwarz bridges the two at the price of a factor ; for an infinite decision space this gives nothing. The disagreement coefficient replaces the cardinality, but it controls disagreement only at one pair of scales at a time (the size of and the norm of ), while the coupled quantity involves all scales at once; obtaining only a loss from this is the technical core of Lemma E.2.
The goal is not trivialized by a junk value: the disagreement coefficient is a genuine supremum under the stated hypotheses (a sorry-free check accompanies the definitions), rules out negative logarithms, the class is the whole class rather than the prior's support, and the reference model is not assumed to lie in the class.
Contributions welcome: proofs of the milestones in attack order; a general layer-cake lemma for finite sums; a formal disagreement coefficient bound by the star number or the eluder dimension (Lemma 6.1), which would lead to Theorem 6.1.
Retailers observe demand signals (point-of-sale data, local forecasts) that their suppliers do not. Whether a retailer should pass such a signal upstream is a central question of the supply chain information-sharing literature. In a single chain, sharing helps the manufacturer plan, but the retailer may lose from it. Competition between chains adds a second effect: sharing in one chain changes how the rival chain responds to its own signal.
Ha, Tian and Tong (MSOM 2017) study this question when the manufacturer's planning decision is production cost reduction: a manufacturer that knows more about demand can invest in lowering its unit cost more efficiently. They find that the equilibrium of the information-sharing game between two competing chains depends on a single efficiency parameter in a three-regime pattern. This mission formalizes that pattern for quantity (Cournot) competition.
Earlier work on information sharing in competing chains (for example Ha, Tong and Zhang, Management Science 2011, on production diseconomies of scale) found related threshold structures under different upstream technologies. The present paper replaces the production cost with a cost-reduction investment.
There are two identical supply chains , each with one manufacturer and one retailer. Retailer faces the inverse demand
where is a demand shock with mean and variance , and is the competition intensity. Manufacturer has unit production cost and lowers it by at effort cost ; a small means efficient cost reduction. Retailer observes a signal with accuracy ; under the linear information structure, .
In stage one, each chain fixes its arrangement : the retailer shares its signal with the manufacturer () or not (). Then the manufacturer sets a wholesale price and a cost reduction, and the retailer a quantity. For each arrangement profile the quantity stage has a linear equilibrium with explicit response coefficients (Lemma 2(a)). These give closed-form ex-ante profits , and for the retailer, the manufacturer and the chain.
The value of information sharing to chain is . In stage one, manufacturer offers retailer the smallest side payment that makes sharing acceptable to the retailer, and chooses or . The result is a symmetric game between the two manufacturers (Table 1). Manufacturer 's payoff is for and for . The standing assumptions are , and .
For fixed , and there are thresholds
such that the set of pure-strategy equilibria of the stage-one game is
In the middle regime, both manufacturers are strictly better off at than at .
A companion item states the Cournot half of Proposition 7(c): for no side payment is needed and is the unique equilibrium.
Proposition 7(a) separates three regimes of cost-reduction efficiency. When cost reduction is efficient (), sharing is dominant. At intermediate efficiency the stage-one game is a coordination game: both chains sharing is Pareto-better for the manufacturers, but both not sharing is also an equilibrium. When cost reduction is inefficient, no chain shares. Competition matters through the gap : a chain whose rival shares tolerates a less efficient cost reduction before it stops sharing, and the thresholds fall as signals become more accurate or competition more intense.
The paper proves these facts by hand-checked algebra, often stated as "we can verify". The formalization turns each such step into a checked statement: the fixed-point identities behind Lemma 2(a), the closed forms of Lemma 3, the reduction of the sign of to the polynomials and , and the monotonicity and location of their roots. None of these results has a machine-checked proof yet. The definitions (response coefficients, profits, side payment, stage-one game) are reusable for the Bertrand half of the paper and for other two-chain information-sharing models.
The obvious approach expands and as rational functions of and tries to read off their signs. That does not finish by itself. After cancelling positive factors, the signs are those of and , which are quadratics in with coefficients polynomial in . The thresholds are defined implicitly by a root of each quadratic crossing . Showing that and are initial intervals of needs the relevant root to be strictly decreasing in , to exceed below and to change sign at . The strict ordering needs a comparison of two roots involving and on . The equilibrium analysis then needs the retailer comparison, to know when the side payment is positive. Table 1's payoff entries are valid only in that case.
Everything is over , in the namespace CompetingChains.Cournot. A general definition TwoPlayerGame gives pure-strategy Nash equilibria of a two-player normal-form game. The definition Setting records the paper's reduced form: the standing assumptions, the response coefficients of Lemma 2(a), the best responses (7) and (9), the ex-ante profit functions of p. 17, the equilibrium profits , , , the stage-one payoff and its set of pure equilibria. The Bayesian stages enter only through these closed forms. The arrangements are an inductive type {S, N}. Manufacturer 2's payoff at is manufacturer 1's payoff at . The chain profit is defined as retailer plus manufacturer profit. The stage-one payoff uses as printed on p. 21, and agrees with Table 1 whenever the side payment is positive.
Conventions and added hypotheses, each disclosed in the items:
The coefficients, profits, and payoffs are definitions, never free parameters. A statement with free coefficients, a goal whose thresholds lack , or one that only asserts membership of would be trivial or weaker, and is not what is posed. No published platform definition states this model, so none is referenced.
Not in scope: Lemma 2's uniqueness (delegated by the paper to earlier work), the wholesale-price and cost-reduction lines of Lemma 2(a), the Bertrand half (Propositions 6(b), 7(b)), the single-chain analysis of §4, Proposition 8 and the numerical study. Proofs of any item are welcome. The polynomial root analysis behind Proposition 6(a) is the main open piece of work.
Collections of genomes, versioned documents and source-code histories are highly repetitive: most of each new item is a copy of something already stored. Full-text indexes such as the suffix array and the FM-index answer pattern queries on such collections, but their size grows with the text length , not with the amount of distinct content. The number of runs in the Burrows–Wheeler transform (BWT) of the text is a standard measure of repetitiveness, and the run-length FM-index of Mäkinen and Navarro counts the occurrences of a pattern in words. Until the work of Gagie, Navarro and Prezza, however, locating those occurrences, i.e. reporting their text positions, required space proportional to for a sampling step , which defeats the purpose on repetitive data.
Timeline.
A text is a sequence over the alphabet whose last symbol T[n]=\=1SA[1..n][1..n]T[SA[p]..n]SA[ISA[i]]=i. The BWT records the character preceding each sorted suffix, $$BWT[p]=T[SA[p]-1]\ (SA[p]>1),\qquad BWT[p]=T[n]=\\ (SA[p]=1),$$ so that is read as . The LF mapping is the counting formula , where counts BWT symbols smaller than and counts copies of in .
A run is a maximal block of equal consecutive BWT symbols, and is their number. A text position is sampled when its character is the first or last BWT character in its run (Definition 1); at most positions are sampled. Definition 3 cuts into phrases that begin exactly at the sampled positions. For a text position , the phrase head of is the greatest sampled position . The permutation (Definition 2) returns the text position in the preceding suffix-array cell, and the differential arrays are and . A text position starts a phrase of when is the first position of a run.
Let , let be the phrase head of , let , and let be the sample stored at . Then
and , respectively, so that is defined.
A companion item, from the proof of Lemma 2 (p. 12), states that a BWT interval holding both and a non- symbol contains an occurrence of at the first or last position of a run.
The goal says that the numbers , one pair per sampled position, determine the neighbours of every suffix-array cell, after one predecessor search over the sampled positions. Combined with the toehold of Lemma 2, which provides one known cell inside the interval of a pattern, it lets an index list all occurrences in space. This is the locating half of Theorem 1 of the paper. The same mechanism reappears throughout the paper: Lemma 4 generalises it to neighbours, Lemma 5 to the LCP array, and Lemmas 12 and 14 drive the access structures for and in §5.
The results are proved in the paper; none of them has a machine-checked proof. The mission contributes a formal model of suffix arrays, BWT, LF and runs that is independent of any data-structure encoding, a checked proof of the LF identity from the counting formula, and the exact correctness statement behind the -index. The handling of the wrap-around phrase (see below) is a case the paper's proof leaves implicit.
The obvious argument follows the three cells backwards under LF for steps. It rests on two facts that are easy to state and not routine to prove. First, must be derived from the counting formula : this is a stable-sorting argument about suffixes that begin with the same symbol, and it uses the uniqueness of \$$. Second, LF must map adjacent cells of a run to adjacent cells, and one must check that the neighbouring cells never leave the run while the middle cell walks from T[k]T[i+1]i\le k[1..k]T[i+1]T[i]qk-i$ must be tracked through natural-number arithmetic.
Positions are 1-based natural numbers, as in the paper. and are functions read only on . is a hypothesis, IsSuffixArray: it maps injectively into and sorts the suffixes strictly in Lean's lexicographic order on lists. Since \=1ISA[i]0iDSADISA$ are integer-valued.
Pins and guards:
The space and time claims of Lemmas 2–3 and Theorem 1 ( words, time on a word RAM) are out of scope; the goal is their explicit combinatorial content. Two trivializing formalizations are ruled out: defining LF as "the cell holding ", which would make milestone 1 a tautology; and defining the phrase head by iterating LF, which would build the proof into the definition. The phrase head is the maximum of the sampled positions .
A full development needs elementary facts about lexicographic order on lists, counting over finite intervals, and iterates of LF. The suffix-array and BWT layer is reusable beyond this mission; two parallel missions on the same paper share the same core definitions. Proofs of the milestones in any order are welcome, as are alternative routes, e.g. through Lemma 14 and for the left half of the goal.
Online selection problems ask an algorithm to accept or reject elements as they arrive, while keeping the accepted set feasible. The decisions are irrevocable, and the arrival order can be chosen after the random activity of the elements is known. A guarantee for one constraint is therefore useful only if it remains meaningful when several constraints apply at once. In Feldman, Svensson and Zenklusen's paper, the constraints include matroid independence, matching, and knapsack capacity. A set satisfying two such requirements lies in the intersection of their feasible families. Theorem 1.9 establishes how their online guarantees combine: the two selectability factors multiply.
The result belongs to a sequence of statements in the paper. The authors first define greedy online contention resolution schemes and their selectability guarantee in Definitions 1.3–1.5. They then state the combination theorem in the introduction and identify the intersection construction in Definition 2.10. Lemma 2.11 supplies the precise selectability assertion for that construction. This mission isolates those claims so that later formalizations of specific constraints can reuse them without repeating the probability argument.
Let be a finite ground set and a family of feasible sets. A fractional point determines a random active set : each belongs to independently with probability . Thus a particular set has weight
A greedy online contention resolution scheme, or greedy OCRS, chooses a down-closed family . As active elements arrive, it accepts an element when adding that element to those already accepted remains in . In a randomized scheme, the choice of is random and independent of . The family contains the empty set, as the procedure begins with no accepted elements.
An element is selectable for a realized active set and family if every with still permits : . This condition covers every possible set that might have been accepted before arrives. A greedy OCRS is -selectable for a relaxation when the probability of this event is at least for every and every . The probability includes both draws when the family is randomized. Here and .
For two feasible families , the combination of their greedy OCRSs independently draws and , then uses . This is a family of sets satisfying both constraints. The proof also uses , the indicator that for every lying in . For selectability itself, .
For , let the first scheme be -selectable and the second -selectable. The mission asks for a greedy OCRS on the intersection with
The target records existence of the combined scheme, independent of a particular proof of its selectability. The paper also claims preservation of polynomial-time efficiency; the finite mathematical model here does not assign a complexity measure to a family sampler or membership oracle, so that clause is outside this target.
The lemma names the combined scheme: independently draw both greedy families and use their intersection. It asserts the same bound for that specific scheme. The earlier milestones record the two order properties of and the finite product-measure correlation inequality appearing in the lemma's proof. Their statements keep the original quantifiers over active sets and families visible.
The theorem turns guarantees for individual constraints into a guarantee for simultaneous constraints. If a matroid scheme and a matching scheme meet the same scale parameter , their intersection is governed by the product of their selectability factors. The factor loss is explicit, which lets subsequent algorithmic results track it without redefining the combined scheme. The lemma additionally fixes the actual distribution over intersected families, avoiding ambiguity about how two randomized procedures are coupled.
Mathlib already provides a general finite FKG inequality, but it does not state the paper's OCRS objects, the selectable event, or the intersection theorem. This mission adds those interfaces and the specialized correlation statement. The source results are proved in the cited paper; the local theorem files in this proposal are statements for later machine-checked proofs. A complete formalization would connect the finite active-set weights to Mathlib's lattice correlation theorem and then establish the randomized family bookkeeping. The finite probability definitions can also serve other OCRS results in the same paper.
The obvious argument would multiply the two probabilities that is selectable for the separate families. Both events depend on the same active set , so they are not independent even when the families are drawn independently. Moreover, selectability for the intersection checks only sets belonging to both families, whereas the original bounds check each family separately. The formal statements must keep these two dependencies distinct. The paper's two monotonicity claims and its FKG display identify the needed intermediate assertions, but their use with an arbitrary random choice of families still requires careful finite-sum reasoning.
The ground set is a finite Lean type and subsets are Finsets. Feasibility is a predicate on those finite sets. Fractional points are real-valued functions, and each input relaxation is represented as a set of such functions with an explicit coordinate bound . The scale and selectability parameters belong to . The point ranges over , not over an independently chosen intersection of scaled sets, so the case retains the paper's meaning. The finite products define the law of ; no measure-theoretic integral is used.
A randomized scheme is a probability weight on possible greedy families for every input point. The combined weight is the product of the two original weights summed over pairs with the required intersection, expressing independent draws. The family distribution is independent of the active-set draw. This sampling convention is necessary for the stated product guarantee and is made explicit here although Definition 2.10 does not spell it out. Each greedy family contains and lies in its own feasible family. These requirements exclude the empty-family and unconstrained-family encodings that would make selectability trivial. The unit-cube bounds prevent negative active-set weights.
The Lean declarations focus on the finite selectability guarantee. They abstract a polytope by its set of fractional points and use the paper's unit-cube condition; they do not formalize a polyhedral representation or test that its binary points equal the feasible sets. A full development of the paper's algorithmic setting would additionally represent online arrival orders, family sampling algorithms, membership oracles, and polynomial running time. Contributions establishing the finite probability lemmas, the specialized FKG statement, and Lemma 2.11 are directly useful here. The general active-set and selectability definitions are reusable across the paper's other missions.