All missions

Motivation

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 $n$, not with the amount of distinct content. The number $r$ 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 $O(r)$ words. Until the work of Gagie, Navarro and Prezza, however, locating those occurrences, i.e. reporting their text positions, required space proportional to $n/s$ for a sampling step $s$, which defeats the purpose on repetitive data.

Timeline.

• 1994: Burrows and Wheeler introduce the transform (DEC SRC Research Report 124).
• 2000–2005: Ferragina and Manzini build the FM-index, with backward search and the LF mapping (J. ACM 52(4), 2005).
• 2005: Mäkinen and Navarro give the run-length FM-index, which counts occurrences in $O(r)$ words (Nordic J. Computing 12(1), 2005).
• 2016–2018: Prezza (PhD thesis, Udine, 2016) and Policriti and Prezza (Algorithmica 80(7), 2018) keep one known suffix-array cell, a "toehold", during backward search.
• 2017–2020: Gagie, Navarro and Prezza show that $O(r)$ words suffice to locate every occurrence (arXiv:1705.10382; arXiv:1809.02792; J. ACM 67(1), 2020). This mission formalizes the combinatorial core of that result.

Setting

A text $T[1..n]$ is a sequence over the alphabet $[1..\sigma]$ whose last symbol T[n]=\=1$is the smallest symbol and occurs nowhere else. The **suffix array**$SA[1..n]$is the permutation of$[1..n]$that lists the suffixes$T[SA[p]..n]$in strictly increasing lexicographic order, and the **inverse suffix array** satisfies$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 $T[0]$ is read as $T[n]$. The LF mapping is the counting formula $LF(p)=C[BWT[p]]+\operatorname{rank}[p]$, where $C[c]$ counts BWT symbols smaller than $c$ and $\operatorname{rank}[p]$ counts copies of $BWT[p]$ in $BWT[1..p]$.

A run is a maximal block of equal consecutive BWT symbols, and $r$ 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 $2r$ positions are sampled. Definition 3 cuts $T$ into phrases that begin exactly at the sampled positions. For a text position $k$, the phrase head $i$ of $T[k]$ is the greatest sampled position $\le k$. The permutation $\phi(i)=SA[ISA[i]-1]$ (Definition 2) returns the text position in the preceding suffix-array cell, and the differential arrays are $DSA[p]=SA[p]-SA[p-1]$ and $DISA[i]=ISA[i]-ISA[i-1]$. A text position starts a phrase of $ISA$ when $ISA[i]$ is the first position of a run.

Formalization targets

Goal: the identity in the proof of Lemma 3

Let $SA[p]=k+1$, let $i$ be the phrase head of $T[k]$, let $q=ISA[i+1]$, and let $N[i]=\langle x,y\rangle=\langle SA[q-1],SA[q+1]\rangle$ be the sample stored at $i$. Then

$$SA[p-1]=x+k-i\quad(p\ge 2),\qquad SA[p+1]=y+k-i\quad(p<n),$$

and $q\ge 2$, $q<n$ respectively, so that $N[i]$ is defined.

Milestones

1. §2.4, p. 9. $SA[LF(p)]=SA[p]-1$ for $SA[p]>1$, with $LF(p)\in[1..n]$.
2. Lemma 12, p. 20. If $BWT[p-1]=BWT[p]$, then $LF(p-1)=LF(p)-1$ and $DSA[LF(p)]=DSA[p]$.
3. Run-free claim, proof of Lemma 3, pp. 12–13. For $0\le t<k-i$, the cells $LF^t(p-1),LF^t(p),LF^t(p+1)$ are contiguous and lie in one BWT run.
4. Lemma 14, p. 23. If $i$ does not start a phrase of $ISA$, then $\phi(i-1)=\phi(i)-1$ and $DISA[i]=DISA[\phi(i)]$.

A companion item, from the proof of Lemma 2 (p. 12), states that a BWT interval holding both $c$ and a non-$c$ symbol contains an occurrence of $c$ at the first or last position of a run.

Significance

The goal says that the $O(r)$ numbers $N[i]$, 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 $SA[sp..ep]$ of a pattern, it lets an index list all occurrences in $O(r)$ space. This is the locating half of Theorem 1 of the paper. The same mechanism reappears throughout the paper: Lemma 4 generalises it to $s$ neighbours, Lemma 5 to the LCP array, and Lemmas 12 and 14 drive the access structures for $SA$ and $ISA$ 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 $r$-index. The handling of the wrap-around phrase (see below) is a case the paper's proof leaves implicit.

Difficulty

The obvious argument follows the three cells $p-1,p,p+1$ backwards under LF for $k-i$ steps. It rests on two facts that are easy to state and not routine to prove. First, $SA[LF(p)]=SA[p]-1$ must be derived from the counting formula $C[c]+\operatorname{rank}[p]$: 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]$back to$T[i+1]$. This is where the choice of$i$as the *greatest* sampled position$\le k$matters, and also where the case of no sampled position in$[1..k]$needs care. Finally, one more LF step from$T[i+1]$to$T[i]$produces the cell$q$, and the shift by$k-i$ must be tracked through natural-number arithmetic.

Formalization scope

Positions are 1-based natural numbers, as in the paper. $T$ and $SA$ are functions $\mathbb N\to\mathbb N$ read only on $[1..n]$. $SA$ is a hypothesis, IsSuffixArray: it maps $[1..n]$ injectively into $[1..n]$ and sorts the suffixes strictly in Lean's lexicographic order on lists. Since \=1$is unique and smallest, this order agrees with the paper's. BWT and LF are defined by the formulas of p. 8, never by the properties the milestones assert.$ISA[i]$is$0$if no cell holds$i$. Sampled positions follow the first sentence of Definition 1 (first or last in its run); the paper's "That is" clause omits the last character of the final run.$DSA$and$DISA$ are integer-valued.

Pins and guards:

• Wrap-around phrase. If no sampled position lies in $[1..k]$, the phrase containing $T[k]$ began at T[n]=\$$, which is always sampled. Its head is encoded as 0$($T[0]\equiv T[n]$), so that$q=ISA[1]$is the cell holding$$$. The goal covers this case; it does not assume a sampled position$\le k$.
• Neighbours. Each half of the goal and of the run-free claim is guarded by the existence of the neighbour ($p\ge 2$, $p<n$).
• SA[LF(p)]. The identity is stated for $SA[p]>1$; for $SA[p]=1$ it holds only cyclically.
• Lemma 14. "$[i-1..i]$ within a phrase of $ISA$" means that $i$ does not start a phrase of $ISA$, which begin only at run-first cells. Definition 3's phrases begin at run-first and run-last cells; the two parses are kept apart.

The space and time claims of Lemmas 2–3 and Theorem 1 ($O(r)$ words, $O(\log\log_w(n/r))$ 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 $SA[p]-1$", 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 $\le k$.

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 $\phi$ for the left half of the goal.

Selected references

• T. Gagie, G. Navarro, N. Prezza, Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space, arXiv:1809.02792v2, 2019. https://arxiv.org/abs/1809.02792
• T. Gagie, G. Navarro, N. Prezza, Fully Functional Suffix Trees and Optimal Text Searching in BWT-Runs Bounded Space, J. ACM 67(1), 2020. https://doi.org/10.1145/3375890
• T. Gagie, G. Navarro, N. Prezza, Optimal-Time Text Indexing in BWT-runs Bounded Space, arXiv:1705.10382, 2017 (SODA 2018). https://arxiv.org/abs/1705.10382
• P. Ferragina, G. Manzini, Indexing Compressed Text, J. ACM 52(4):552–581, 2005. https://doi.org/10.1145/1082036.1082039
• A. Policriti, N. Prezza, LZ77 Computation Based on the Run-Length Encoded BWT, Algorithmica 80(7):1986–2011, 2018. https://doi.org/10.1007/s00453-017-0327-z
• V. Mäkinen, G. Navarro, Succinct Suffix Arrays Based on Run-Length Encoding, Nordic Journal of Computing 12(1):40–66, 2005 (no DOI).
• M. Burrows, D. J. Wheeler, A Block Sorting Lossless Data Compression Algorithm, Technical Report 124, Digital Equipment Corporation, 1994 (no DOI).

Motivation

Large network games can be described by a graphon, a measurable kernel that assigns an interaction weight to each pair of players in a continuum. This representation is useful when a finite network is viewed as an approximation to a limiting network. A basic question is whether a small change in interaction weights can cause a large change in equilibrium behavior. Carmona, Cooney, Graves, and Laurière answer this question for a static game with real actions, noisy player states, and costs coupled through an aggregate state. Their static graphon games paper establishes existence and uniqueness under different hypotheses, and Theorem 3.20 gives an explicit stability estimate under its contraction condition.

The mission isolates that stability estimate and the results on which it depends. It belongs to the same development as the paper's existence theorem, but has a narrower question: how sensitively does the equilibrium respond when one graphon is replaced by another? The paper later studies finite-player approximations, for which understanding the limiting graphon game's equilibrium is useful. Those later approximation theorems are outside this mission.

Setting

The player set is $I=[0,1]$ with Lebesgue probability measure. Every player chooses a real action. A strategy profile $\alpha$ assigns an action $\alpha(x)$ to almost every player and belongs to $L^2(I)$. Profiles that differ only on a null set represent the same strategy.

A graphon is a symmetric, real-valued, measurable, square-integrable function $w$ on $I\times I$. It defines an integral operator $W$ on $L^2(I)$ by

$$[Wg](x)=\int_I w(x,y)g(y)\,dy.$$

Its norm $\|W\|$ is the $L^2$-to-$L^2$ operator norm. In particular, interaction weights are allowed to be negative and are not restricted to $[0,1]$. A second graphon $w'$ has operator $W'$, and $\|W-W'\|$ is the operator norm of their difference.

A player's state is $X_{a,z,\xi}=b(a,z)+\xi$, where $a$ is the player's action, $z$ is an aggregate state, and $\xi$ has a common centered probability law $\mu_0$ with finite second moment. Assumption 1 bounds squared changes in $b$ by $c_\alpha$ times the squared action change plus $c_z$ times the squared aggregate change. For a profile $\alpha$, its aggregate $Z\alpha$ is the $L^2$ solution of

$$[Z\alpha](x)=\int_I w(x,y)b(\alpha(y),[Z\alpha](y))\,dy \quad\text{for almost every }x\in I.$$

Proposition 3.1 states that this aggregate exists and is unique when $\sqrt{c_z}\|W\|<1$. This equation is the deterministic aggregate obtained from the paper's continuum model.

The expected cost of action $a$ at aggregate $z$ is $J(a,z)=\int f(b(a,z)+\xi,a,z)\,\mu_0(d\xi)$. Assumption 4 says that $J(\cdot,z)$ is continuously differentiable and uniformly $\ell_c$-strongly convex, and its action derivative changes at most $\ell_J|z-z'|$ when the aggregate changes. The best response $Bz$ minimizes this cost pointwise. A Nash equilibrium is an $L^2$ profile $\alpha$ whose action minimizes $J(\cdot,[Z\alpha](x))$ for almost every player. Assumption 5 adds the uniform bound $|b(a,z)|\leq c_0$.

Formalization targets

The first targets are the unique aggregate of Proposition 3.1, the best-response bound of Lemma 3.7, and the $L^2$ aggregate bound (15) of Lemma 3.16. Together these support the uniqueness condition in Proposition 3.17:

$$\frac{\ell_J}{\ell_c} \frac{\sqrt{c_\alpha}\|W\|}{1-\sqrt{c_z}\|W\|}<1. \tag{17}$$

Lemma 3.19 then bounds the change of aggregate when the same profile is placed in two graphons. The goal, Theorem 3.20, concerns an equilibrium $\alpha$ for $w$ and any equilibrium $\alpha'$ for $w'$:

$$\|\alpha-\alpha'\|_{L^2(I)}\leq\kappa\|W-W'\|, \qquad \kappa=\frac{c_0\ell_J(1-\sqrt{c_z}\|W\|)} {(1-\sqrt{c_z}\|W\|) [\ell_c(1-\sqrt{c_z}\|W\|)-\ell_J\sqrt{c_\alpha}\|W\|]}.$$

Here $w$ satisfies both $\sqrt{c_z}\|W\|<1$ and (17), while $w'$ is required only to satisfy $\sqrt{c_z}\|W'\|<1$. The displayed coefficient is the paper's expression, including its common factor.

Significance

The theorem gives a quantitative guarantee: as long as the original game's contraction condition holds, the distance between equilibria is controlled by the operator distance between graphons. The bound identifies how state sensitivity $c_\alpha,c_z$, cost sensitivity $\ell_J$, strong convexity $\ell_c$, and the state bound $c_0$ enter that guarantee. The result also separates two questions: whether an equilibrium exists for a changed graphon, and how far any such equilibrium can lie from the original one.

The mathematical theorem is proved in the paper; the Lean goal is open. A complete formal development would establish the $L^2$ integral-operator estimates, the aggregate and best-response regularity results, the unique equilibrium under (17), and finally the stability inequality. The definitions of real-valued graphons, aggregates, and their extended-valued operator norm can support later work on graphon games beyond this particular estimate. The paper's §4 finite-player results, including Theorems 4.3, 4.7, and 4.9, are not posed here.

Difficulty

An equilibrium is a fixed point of a response to an aggregate, so changing the graphon changes both the aggregate and the equilibrium profile. A direct comparison of costs at two equilibria does not by itself separate these effects or yield the printed constant. The aggregate is defined only as an $L^2$ equivalence class, while its equation and pointwise best responses use representatives. The formalization must keep those almost-everywhere statements aligned with the operator norm estimate. It must also retain the paper's asymmetric hypotheses: (17) is assumed for the original graphon, while the second graphon is allowed to have any Nash equilibrium under its own aggregate condition.

Formalization scope

Lean uses unitInterval with its volume measure for $I$, real actions, functions with MemLp for $L^2$ profiles, and almost-everywhere equality for profiles and aggregates. IsGraphon includes measurability, symmetry, and square integrability. IsAggregate records equation (6) and membership in $L^2$. The integral cost is computed from $b$, $f$, and $\mu_0$ rather than supplied as an unrelated function. Assumptions 1, 4, and 5 are explicit; the centered noise law is part of the standing model. Lemma 3.7 is stated for an arbitrary cost satisfying Assumption 4, as on the page.

The paper defines equilibrium through a best-response map on a rich Fubini extension. Proposition 3.6 identifies that with the almost-everywhere pointwise minimization condition under Assumption 4. The mission uses that equivalent condition as its equilibrium predicate. This is a disclosed model choice because the Fubini extension itself is not formalized. A best response is selected by classical choice; Assumption 4 gives the minimizer that makes the selection meaningful.

Norm inequalities use extended nonnegative reals. For a square-integrable graphon, its operator norm is finite, and real hypotheses use that finite value. The operator norm is never a real supremum with a default value for unbounded inputs; an equilibrium always includes an aggregate; and an infinite left-side norm is never converted to zero. These choices prevent the stability claim from becoming empty at a bad input. Contributions to the integral-operator infrastructure, the existence and uniqueness of aggregates, and the five named milestones are all within scope.

Selected references

• René Carmona, Daniel B. Cooney, Christy V. Graves, and Mathieu Laurière, Stochastic Graphon Games: I. The Static Case, arXiv:1911.10664v1, 2019; published in Mathematics of Operations Research, 2022. arXiv

Motivation

First order primal–dual algorithms are used when a linear program is too large for a direct factorization or when matrix operations are cheaper than solving a sequence of linear systems. Their basic guarantees often bound an averaged duality gap by a quantity proportional to $1/t$ after $t$ steps. A restart discards the current inner iteration history and begins again from an averaged output. For problems with a suitable error bound, restarts can turn sublinear progress into geometric decrease in distance to the solution set. Applegate, Hinder, Lu and Lubin analyze this mechanism for a class that includes proximal point, extragradient, primal–dual hybrid gradient and ADMM methods, with constants listed in their Table 1. Their adaptive rule is useful when the sharpness constant is unavailable to the algorithm designer. Applegate et al., arXiv:2105.12715v4, §§2–4

Setting

Let $X\subseteq\mathbb R^n$ and $Y\subseteq\mathbb R^m$ be closed convex sets. The primal–dual problem is $\min_{x\in X}\max_{y\in Y}L(x,y)$, where $L$ is differentiable, convex in $x$ and concave in $y$. A point $z=(x,y)$ is feasible when $z\in Z=X\times Y$. Its saddle-point set $Z^\star$ contains the feasible pairs satisfying $L(x,y')\le L(x,y)\le L(x',y)$ for every $x'\in X$ and $y'\in Y$. Distances and balls use a chosen seminorm $\|\cdot\|_p$; this matters for methods whose natural geometry is degenerate. Applegate et al., arXiv:2105.12715v4, pp. 2–3

For $r>0$, put $W_r(z)=\{\hat z\in Z:\|z-\hat z\|_p\le r\}$. The normalized duality gap is $\rho_r(z)=\sup_{\hat z\in W_r(z)}[L(x,\hat y)-L(\hat x,y)]/r$. At $r=0$ it is the upper limit as positive radii decrease to zero. The gap can be infinite under a seminorm, so its values are extended real. A problem is $\alpha$-sharp on $S\subseteq Z$ when $\alpha\operatorname{dist}_p(z,Z^\star)\le\rho_r(z)$ for every $z\in S$ and every $0<r\le\operatorname{diam}_p(S)$. This condition connects a computable local gap to the distance of interest. Applegate et al., arXiv:2105.12715v4, pp. 3, 11, (4), Definition 1

The base algorithm begins at $z^0\in Z$ and supplies averaged outputs $\bar z^t$ for positive inner times $t$. Property 3 requires constants $q,C>0$, uniform over every feasible start and output run, for which $\bar z^t\in Z$, $\rho_{\|\bar z^t-z^0\|_p}(\bar z^t)\le2C\|\bar z^t-z^0\|_p/t$, and $\|\bar z^t-z^0\|_p\le(q+2)\operatorname{dist}_p(z^0,Z^\star)$. An outer run starts at $z^{k,0}$, runs its inner algorithm for $\tau^k$ steps, and sets $z^{k+1,0}=\bar z^{k,\tau^k}$. Its first length $\tau^0\ge1$ is selected by the user. At later outer indices, it restarts at the first positive time when the normalized gap has fallen below $\beta$ times the gap at the previous outer transition, with $0<\beta<1$. Applegate et al., arXiv:2105.12715v4, pp. 9–10, 15–16, Property 3, Algorithm 1, (30)

Formalization targets

The goal is both parts of Theorem 2. Assume all outer starts lie in one set $S$ on which the problem is $\alpha$-sharp, with $\alpha>0$. Define the ceiling time $t^\star=\left\lceil2C(q+2)/(\alpha\beta)\right\rceil$. For every $k\ge1$ the target is

$$\tau^k\le t^\star, \qquad \operatorname{dist}_p(z^{k,0},Z^\star) \le\beta^k\frac{t^\star}{\tau^0}\operatorname{dist}_p(z^{0,0},Z^\star).$$

The milestones are Proposition 8's treatment of zero displacement, the displayed restart comparison in the proof of (33), the bound (33) itself, and the repeated normalized-gap inequality in the proof of part (ii). Each is tied to the arXiv version's printed page and label. The assertion begins at $k=1$: the first interval is free and need not be at most $t^\star$. Applegate et al., arXiv:2105.12715v4, pp. 17–18

Significance

The first conclusion gives a uniform bound on the inner work of every subsequent adaptive interval. The second translates the gap-based restart rule into a geometric distance guarantee while retaining the user-selected first interval as a visible factor. Together, they explain why an algorithm that does not know $\alpha$ can have the same characteristic restart scale as one using a fixed frequency chosen from $\alpha$. The paper proves this theorem and gives linear-programming settings in which its sharpness premise holds; this mission asks for a machine-checked statement and, eventually, a machine-checked proof of that known result. Applegate et al., arXiv:2105.12715v4, Theorems 1–2 and Lemma 5

Formalizing the result also produces reusable interfaces for saddle sets, seminorm distances, localized duality gaps, uniform algorithm properties, and first-trigger restart runs. Those interfaces can support other primal–dual analyses without committing to a particular inner update map. A complete proof can later connect Property 3 to the paper's individual algorithms, while this mission preserves the abstract theorem that they share. Applegate et al., arXiv:2105.12715v4, Proposition 4 and §4

Difficulty

The restart test uses a gap evaluated at the moving radius $\|\bar z^{k,t}-z^{k,0}\|_p$, whereas sharpness relates a gap at the radius of the previous outer transition to distance from $Z^\star$. This mismatch must be reconciled while preserving the exact ceiling constant. A zero seminorm displacement is a separate boundary case: sharpness only speaks about positive radii, but the algorithm can still encounter radius zero. The theorem also needs the first qualifying time; knowing merely that a later time satisfies the test gives no upper bound on the interval length. Applegate et al., arXiv:2105.12715v4, pp. 16–18

Formalization scope

Lean represents $x$ and $y$ by finite-dimensional Euclidean spaces and $z$ by their product, allowing either dimension to be zero. The geometry on that product is an explicit Seminorm, never the product type's default norm. $Z^\star$ is the set of saddle pairs. The standing problem predicate includes closed convex feasible sets, separate convexity and concavity, and differentiability on the whole ambient product space. It also requires $Z^\star\ne\varnothing$, a disclosed strengthening of the paper's standing feasibility and finite-optimum assumptions so the real-valued distance to $Z^\star$ cannot collapse to an empty-infimum default. The infimum defining distance is over saddle points only; the supremum defining the gap is over feasible pairs only. The normalized gap and diameter use extended reals so an unbounded seminorm ball does not silently acquire value zero. Applegate et al., arXiv:2105.12715v4, pp. 2–4

The base method is a relation from a start to possible averaged-output sequences. Property 3 fixes $q,C$ before quantifying over starts, runs and positive times. The theorem assumes initial feasibility; Property 3 then makes restarted outer points feasible. An adaptive run records the positive first interval and the first qualifying positive time for each later interval. The ceiling is Nat.ceil; the factor $t^\star/\tau^0$ is division in the reals. A formalization with arbitrarily chosen qualifying restart times, sharpness only along one chosen trajectory, a real-valued supremum over an unbounded ball, or a vacuous solution set would change the result. Contributions to the gap and seminorm infrastructure and to either half of Theorem 2 are useful; the individual algorithm implementations are outside this mission's core. Applegate et al., arXiv:2105.12715v4, pp. 9–10, 16–18

Selected references

• D. Applegate, O. Hinder, H. Lu and M. Lubin, Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness, Mathematical Programming, 2022; mission citation basis: arXiv:2105.12715v4.

Motivation

Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571, ICLR 2018) train classifiers against adversarial perturbations by solving a Lagrangian relaxation of a Wasserstein distributionally robust problem. The inner problem, $\sup_z \{\ell(\theta;z)-\gamma\, c(z,z_0)\}$, is strongly concave, and hence solvable by gradient ascent with the paper's certificates, exactly when the penalty $\gamma$ exceeds the input-smoothness constant $L_{zz}$ of the loss: the Lipschitz constant of $z\mapsto\nabla_z\ell(\theta;z)$. For a deep network this constant is not given; §4 of the paper ("Bounds on smoothness of neural networks") supplies an explicit upper bound in terms of the weights' spectral norms and per-layer constants of the activations. The bound tells a practitioner how large $\gamma$ must be for the robustness guarantees to apply, and it is of the same type as the spectral-norm Lipschitz bounds used for adversarial robustness and generalization of deep networks (Szegedy et al. 2014; Bartlett, Foster, Telgarsky 2017), but at the level of the derivative rather than the function.

Setting

A layered network of depth $L$ has widths $d_{l,I}$ (pre-activation of layer $l$) and $d_{l,O}$ (output of layer $l$), with $d_{0,O}=p$ the input dimension and $d_{L,O}=K$ the number of classes. Its parameters are weight matrices $\theta_l:\mathbb R^{d_{l-1,O}}\to\mathbb R^{d_{l,I}}$, and each linear layer is followed by a nonlinear operation $\sigma_l:\mathbb R^{d_{l,I}}\to\mathbb R^{d_{l,O}}$ (an activation, possibly combined with pooling). The output of the first $l$ layers is

$$F_0(\theta;x)=x,\qquad F_l(\theta;x)=\sigma_l\big(\theta_l\cdot F_{l-1}(\theta;x)\big),$$

and its Jacobian in $x$ is $J_xF_l(\theta;x)$. All spaces carry the Euclidean norm $\|\cdot\|_2$, and $\|\cdot\|_{\mathrm{op}}$ is the $\ell_2$-operator (spectral) norm.

Assumption E. For $l=1,\dots,L$, the map $\sigma_l$ is $L^0_l$-Lipschitz for $\|\cdot\|_2$, its Jacobian $J\sigma_l$ is $L^1_l$-Lipschitz from $\|\cdot\|_2$ to $\|\cdot\|_{\mathrm{op}}$, and $L^0_l>0$. From these constants define

$$\alpha_l(\theta)=\prod_{j=1}^{l}L^0_j\,\|\theta_j\|_{\mathrm{op}},\qquad \beta_l(\theta)=\alpha_l(\theta)\sum_{j=1}^{l}\frac{L^1_j}{(L^0_j)^2}\,\alpha_j(\theta).$$

The classification loss is the softmax loss $\ell(\theta;(x,y))=-\log p_y(\theta;x)$ with $p_y(\theta;x)=\exp(F_{L,y}(\theta;x))/\sum_{k=1}^K\exp(F_{L,k}(\theta;x))$, for a class $y\in\{1,\dots,K\}$.

Formalization targets

Goal: Corollary 4

Under Assumption E, for every class $y$ and all inputs $x,x'$,

$$\big\|\nabla_x\ell(\theta;(x,y))-\nabla_x\ell(\theta;(x',y))\big\|_2\le\big(\sqrt2\,\beta_L(\theta)+\alpha_L(\theta)^2\big)\,\|x-x'\|_2 .$$

Proposition 5

Under Assumption E, for $l=1,\dots,L$,

$$\|F_l(\theta;x)-F_l(\theta;x')\|_2\le\alpha_l(\theta)\|x-x'\|_2,\qquad \|J_xF_l(\theta;x)-J_xF_l(\theta;x')\|_{\mathrm{op}}\le\beta_l(\theta)\|x-x'\|_2 .$$

Milestones

In the order the paper's proof uses them: Lemma 6 (the chain rule for $J_xF_l$, recursively and as a product); Proposition 5, first part; the telescoping representation (34) of $J_xF_l(\theta;x)-J_xF_l(\theta;x')$; Proposition 5, second part; the softmax constants of §B.9 (gradient $p(v)-e_y$, Lipschitz constant $\sqrt2$, smoothness constant $1$); and the recursion of §B.9 for $\alpha_l,\beta_l$ with its instance $\beta_{L+1}=\sqrt2\,\beta_L+\alpha_L^2$ for a softmax output layer.

Significance

Corollary 4 converts the abstract hypothesis $\gamma>L_{zz}$ of the paper's convergence and certification results (missions 1 and 2 of this series) into a checkable condition on a trained network: $L_{zz}\le\sqrt2\,\beta_L(\theta)+\alpha_L(\theta)^2$, computable from spectral norms of the weights and from constants of standard activations (the paper lists average pooling, sigmoid and ELU). Proposition 5 is a reusable statement about any composition of smooth maps with linear layers, independent of the softmax and of robust optimization.

The results are proved in the paper (§B.8–§B.9). No machine-checked proof of them is known to exist. This mission produces a formal development of the input Jacobian of a layered network with varying widths, the telescoping estimate for its variation, and the smoothness constants of the softmax loss, all with the paper's explicit constants.

Difficulty

The function-level bound (first part of Proposition 5) is a direct induction. The derivative-level bound is not: the obvious induction on $J_xF_{l+1}=J\sigma_{l+1}\cdot\theta_{l+1}\cdot J_xF_l$ needs both a bound on $\|J_xF_l\|_{\mathrm{op}}$, which comes from the Lipschitz half and the differentiability of every layer, and a bound on the variation of the Jacobian of the previous layers, and the two must be combined so that the constant comes out as exactly $\beta_l(\theta)$ of (21), whose definition uses quotients by $(L^0_j)^2$. For the corollary, the softmax loss must be shown to have Lipschitz constant $\sqrt2$ (a supremum that is not attained) and a $1$-Lipschitz derivative; the paper's eigenvalue argument for the latter is loose and its displayed initial condition for the recursion of the constants is misprinted, so the printed text cannot be transcribed line by line. In Lean, the widths change from layer to layer, so the network is a family of maps between different Euclidean spaces, and every product of Jacobians is a dependently typed composition.

Formalization scope

• Inputs, pre-activations and outputs are EuclideanSpace ℝ (Fin n); weights are continuous linear maps, so ‖θ l‖ is the spectral norm; Jacobians are Fréchet derivatives with the operator norm. A Frobenius or entrywise norm would state a different theorem and is not used.
• Layers are indexed from $0$ in Lean: Lean layer l is the paper's layer $l+1$ (θ l, σ l, L0 l, L1 l); F l, α L0 l, β L0 L1 l carry the paper's index $l$. Widths vary with the layer; they are not collapsed to a single dimension.
• Assumption E is stated for the first $L$ layers and includes two hypotheses implicit on the page: each $\sigma_l$ is differentiable (the assumption speaks of its Jacobian) and $L^1_l\ge0$. The paper's $L^0_l>0$ is kept.
• $\alpha_l$ and $\beta_l$ are the explicit product and sum of (21); they are definitions, not free parameters. Consequently $\alpha_0=1$ and $\beta_0=0$; the paper's "$\beta_0(\theta)=\alpha_0(\theta)=1$" in §B.9 is a misprint and is not followed. The recursion $\beta_{l+1}=(\alpha_{l+1}/\alpha_l)\beta_l+\dots$ is stated in the division-free form $\beta_{l+1}=L^0_{l+1}\|\theta_{l+1}\|_{\mathrm{op}}\beta_l+\dots$, and in the paper's form when $\alpha_l\ne0$.
• In (34) the first displayed line (a "product of differences") is a misprint; only the telescoped sum is formalized.
• The softmax loss is real-valued on $\mathbb R^K$ with $K=d_{L,O}$ and a class $y$ in Fin K; the goal uses Mathlib's gradient, whose norm equals the operator norm of the derivative.
• The goal is not trivialized by free constants: a version with $\alpha,\beta$ as arbitrary parameters, or with the loss not tied to $F_L$, would not be Corollary 4 and is not what is posed.
• Not formalized: the Hessian formula $\nabla^2\sigma_y=\operatorname{diag}p-pp^T$ and the eigenvalue argument (only their conclusion $L^1=1$ is stated); attainment of $\sup_x\|p(x)-e_y\|_2=\sqrt2$ (the value of the supremum, for $K\ge2$, is stated; it is not attained); Examples 1–3 (constants of pooling, sigmoid and ELU).

A complete development needs the chain rule for the network map, the mean value inequality for the softmax loss, and the algebra of (21). The definitions of the layered network and of the softmax loss are independent of robust optimization and are reusable for other Lipschitz and smoothness bounds of deep networks. Proofs of any milestone, and alternative arguments with sharper constants stated as separate theorems, are welcome.

Selected references

• A. Sinha, H. Namkoong, R. Volpi, J. Duchi, Certifying Some Distributional Robustness with Principled Adversarial Training, ICLR 2018; arXiv:1710.10571v5, 2020. https://arxiv.org/abs/1710.10571
• C. Szegedy et al., Intriguing properties of neural networks, ICLR 2014. https://arxiv.org/abs/1312.6199
• P. Bartlett, D. Foster, M. Telgarsky, Spectrally-normalized margin bounds for neural networks, NeurIPS 2017. https://arxiv.org/abs/1706.08498

Motivation

Linear programs at very large scale are increasingly solved by first-order primal-dual methods, which use only matrix-vector products instead of matrix factorizations. Such methods parallelize well and have a small memory footprint, but on their own they are slow to reach moderate or high accuracy. Applegate, Hinder, Lu and Lubin (arXiv:2105.12715, Math. Program. 2022) showed that periodically restarting a primal-dual method from the average of its iterates turns its sublinear ergodic rate into a linear rate on sharp problems, a class that contains every linear program. The analysis underlies PDLP, a restarted PDHG solver studied computationally by Applegate et al. (arXiv:2106.04756) and shipped in Google OR-Tools.

This mission formalizes the paper's first convergence theorem: with restarts at a fixed frequency, the distance from the restart points to the solution set shrinks by a factor $\beta$ per restart.

Setting

Let $X \subseteq \mathbb R^n$ and $Y \subseteq \mathbb R^m$ be closed convex sets and let $L(x, y)$ be differentiable, convex in $x$ and concave in $y$. Problem (1) is

$$\min_{x \in X} \max_{y \in Y} L(x, y),$$

with feasible region $Z = X \times Y$ and primal-dual points $z = (x, y)$. Its solution set $Z^\star$ is the set of saddle points $z^\star \in Z$: $L(x^\star, y') \le L(x^\star, y^\star) \le L(x', y^\star)$ for all $x' \in X$, $y' \in Y$. Throughout, $Z^\star \neq \emptyset$.

Distances are measured in a semi-norm $\|\cdot\|$, which the paper allows in order to cover ADMM. Write $\operatorname{dist}(z, Z^\star) = \inf_{z^\star \in Z^\star}\|z - z^\star\|$, $\operatorname{diam}(S) = \sup_{s, s' \in S}\|s - s'\|$, and $W_r(z) = \{\hat z \in Z : \|z - \hat z\| \le r\}$. The primal-dual gap (3) at $z$ is $\sup_{\hat z \in Z}\{L(x, \hat y) - L(\hat x, y)\}$, and the normalized duality gap (4a)–(4b) is

$$\rho_r(z) = \frac{1}{r}\sup_{\hat z \in W_r(z)}\{L(x, \hat y) - L(\hat x, y)\} \quad (r > 0), \qquad \rho_0(z) = \limsup_{r \to 0^+}\rho_r(z).$$

By Definition 1, problem (1) is $\alpha$-sharp on $S \subseteq Z$ if $\alpha\operatorname{dist}(z, Z^\star) \le \rho_r(z)$ for all $z \in S$ and all $r \in (0, \operatorname{diam}(S)]$.

The base method is abstract. From a start $z^0$ it outputs averaged points $\bar z^t$, $t \ge 1$. It has Property 3 with constants $q, C > 0$ if, for every start $z^0 \in Z$ and every $t \ge 1$, $\bar z^t \in Z$ and

i. $\rho_{\|\bar z^t - z^0\|}(\bar z^t) \le 2C\|\bar z^t - z^0\|/t$,

ii. $\|\bar z^t - z^0\| \le (q + 2)\operatorname{dist}(z^0, Z^\star)$.

Algorithm 1 with fixed-frequency restarts (29) runs the base method from $z^{n,0}$ for

$$t^\star = \left\lceil \frac{2C(q+2)}{\alpha\beta}\right\rceil$$

steps, sets $z^{n+1,0} = \bar z^{n,t^\star}$, and repeats, with $\beta \in (0, 1)$.

Formalization targets

Goal: Theorem 1 (p. 17)

If the base method has Property 3 and (1) is $\alpha$-sharp on $W_R(z^{0,0})$ with $R = \frac{q+2}{1-\beta}\operatorname{dist}(z^{0,0}, Z^\star)$, then for every $n \ge 0$

$$\operatorname{dist}(z^{n,0}, Z^\star) \le \beta^n \operatorname{dist}(z^{0,0}, Z^\star). \tag{31}$$

Milestones

1. Proposition 5 (p. 11): for $z \in Z$, $\rho_r(z)$ is non-increasing in $r \in [0, \infty)$.
2. Proposition 6 (p. 11): for $z \in Z$ and $r \ge 0$, the primal-dual gap at $z$ is zero if and only if $\rho_r(z) = 0$.
3. Proposition 8 (p. 17): under Property 3, $\|\bar z^t - z^0\| = 0$ implies $\bar z^t \in Z^\star$.
4. First display of the proof of Theorem 1 (p. 17): if (31) holds for all $n \le N$, then $\|z^{N+1,0} - z^{0,0}\| \le R$, so $z^{N+1,0} \in W_R(z^{0,0})$.
5. Display (32) (p. 17): if $z^{N,0}, z^{N+1,0} \in W_R(z^{0,0})$, then

$$\operatorname{dist}(z^{N+1,0}, Z^\star) \le \beta\operatorname{dist}(z^{N,0}, Z^\star).$$

Companion statements

Proposition 2 (p. 8) and Proposition 4 (p. 10) show where Property 3 comes from. A generic algorithm (6) with iterates $z^t$ and targets $\hat z^t$ has Property 1 with $C$ if $L(\hat x^{t+1}, y) - L(x, \hat y^{t+1}) \le \frac C2\|z - z^t\|^2 - \frac C2\|z - z^{t+1}\|^2$ for every $z \in Z$ (12). It has Property 2 with $q$ if $\|\hat z^t - z^t\| \le q\operatorname{dist}(z^t, Z^\star)$ or $\|\hat z^t - z^{t-1}\| \le q\operatorname{dist}(z^t, Z^\star)$.

• Proposition 2: Property 1 gives non-expansiveness $\|z^{t+1} - z^\star\| \le \|z^t - z^\star\|$ and the ergodic rate $L(\bar x^t, y) - L(x, \bar y^t) \le C\|z - z^0\|^2/(2t)$.
• Proposition 4: Properties 1 and 2 give Property 3 for the averages $\bar z^t = \frac1t\sum_{i=1}^t \hat z^i$, with the same $q$ and $C$.

Fact 1 (p. 11), that $r\rho_r(z)$ is non-decreasing in $r$, is included as well.

Significance

Theorem 1 converts any primal-dual method with an $O(1/t)$ ergodic rate on the normalized duality gap into a linearly convergent method on sharp problems. The rate is $O\big(\frac{C}{\alpha}\log\frac1\epsilon\big)$ iterations to reach $\operatorname{dist}(z, Z^\star) \le \epsilon$ (Remark 3). Through Proposition 4 it applies to PPM, EGM, PDHG and ADMM. Combined with the paper's Lemma 5, which shows that linear programs are sharp with $\alpha$ the inverse of a Hoffman constant, it yields linear convergence of restarted PDHG for LP. The paper also shows that this rate matches a lower bound for a general class of primal-dual methods.

The result is proved in the paper. As far as is known, no part of it, and no normalized duality gap or primal-dual sharpness notion, has a machine-checked proof. The mission adds a checked version of the restart argument, with every degenerate case resolved: zero displacements, unbounded balls, and semi-norms that are not norms.

Difficulty

Each proof is short, but the statements are delicate in ways the paper passes over.

• The paper's argmax over $W_r(z)$ need not exist under a semi-norm, and $\rho_r(z)$ may be $+\infty$. Proposition 5 therefore has to be proved with suprema, through the convex-combination scaling $z + \frac{r_1}{r_2}(\hat z - z)$, not with a maximizer.
• Sharpness is only available at radii in $(0, \operatorname{diam}(W_R(z^{0,0}))]$ and only at points of $W_R(z^{0,0})$. So the induction in Theorem 1 must carry two facts together: the contraction (31), and the fact that every restart point stays in $W_R(z^{0,0})$.
• The step size $r = \|z^{N+1,0} - z^{N,0}\|$ may be zero, which is why Proposition 8, and through it Propositions 5 and 6 at $r = 0$, is needed.

A direct contraction argument that applies sharpness at an arbitrary radius, or on all of $Z$, does not prove the theorem as stated.

Formalization scope

• $\mathbb R^n$ and $\mathbb R^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). $n = 0$ and $m = 0$ are allowed.
• The semi-norm is an arbitrary Seminorm ℝ on their product, never the product's built-in norm.
• The primal-dual gap, $\rho_r$ and $\operatorname{diam}$ are suprema in EReal, so unbounded sets give $+\infty$ and not a junk $0$. $\operatorname{dist}(\cdot, Z^\star)$ is a real infimum over the nonempty set $Z^\star$.
• The base method is a map from starts to sets of admissible output sequences, because a primal-dual step can be an argmin and need not be single-valued. Property 3 quantifies over every start in $Z$ and every run, with $q$ and $C$ fixed first.
• The restart length is the natural number $\lceil 2C(q+2)/(\alpha\beta)\rceil$, and every inner loop has exactly this length.

Standing assumptions and added hypotheses:

• $X$ and $Y$ are closed and convex, and $L$ is convex-concave and differentiable on the whole space.
• $Z^\star \neq \emptyset$ replaces the page's "non-empty feasible region and bounded optimal value".
• $\alpha > 0$ is assumed.
• Property 1 is required for every $t \ge 0$, although the paper's $\mathbb N$ starts at one: the proof of Proposition 2 telescopes from $z^0$.
• The iterates of a generic algorithm stay in $Z$, which the page leaves implicit.

Departures from the page:

• Proposition 8 asserts only $\bar z^t \in Z^\star$. The page's "$\bar z^{n,t} = z^{n,0}$" does not follow under a semi-norm.
• Milestones that do not use a standing assumption drop it.

The goal is not trivialized by its hypotheses. A companion check file exhibits $L(x, y) = xy$ on $\mathbb R \times \mathbb R$, with the sup norm and an oracle base method, on which every hypothesis of Theorem 1 holds and $\operatorname{dist}(z^{0,0}, Z^\star) = 1$. Sharpness is assumed only where Definition 1 and the theorem assume it: replacing $W_R(z^{0,0})$ by $Z$, or the radius range by all $r > 0$, would weaken the theorem.

A complete development needs elementary facts about suprema in EReal, Jensen's inequality for convex-concave functions on averages, and geometric sums. The definitions of $\rho_r$, sharpness and Property 3 are reusable for the adaptive-restart theorem of the same paper (Theorem 2, a separate mission) and for other restart analyses. Proofs of any milestone or companion are welcome.

Selected references

• D. Applegate, O. Hinder, H. Lu, M. Lubin, Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness, Math. Program. (2022); arXiv:2105.12715v4. https://arxiv.org/abs/2105.12715 · https://doi.org/10.1007/s10107-022-01901-9
• D. Applegate, M. Díaz, O. Hinder, H. Lu, M. Lubin, B. O'Donoghue, W. Schudy, Practical Large-Scale Linear Programming using Primal-Dual Hybrid Gradient, NeurIPS 2021. https://arxiv.org/abs/2106.04756
• A. Chambolle, T. Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, J. Math. Imaging Vision 40 (2011). https://doi.org/10.1007/s10851-010-0251-1
• A. Nemirovski, Prox-Method with Rate of Convergence O(1/t) for Variational Inequalities with Lipschitz Continuous Monotone Operators and Smooth Convex-Concave Saddle Point Problems, SIAM J. Optim. 15 (2004). https://doi.org/10.1137/S1052623403425629

Motivation

Posted prices turn an offline allocation problem into a sequential choice process: each agent sees a menu of outcomes and prices, then chooses an outcome without revealing its full valuation. The balanced prices framework of Dütting, Feldman, Kesselheim, and Lucier gives welfare guarantees by comparing the revenue collected from an allocation with the welfare that remains feasible after it. Its appeal is that the comparison can be checked in a deterministic full-information setting before any probability distribution over valuations enters the analysis. Dütting et al., 2020

One valuation class at a time would make that framework difficult to reuse. Combinatorial auction valuations are often built by taking pointwise maxima of simpler valuations or by adding values from separate markets. Section 5 of the paper asks whether a price construction balanced for the simple class remains balanced after these operations. Theorem 5.3 gives the maximum closure result; Theorem 5.4 gives addition across markets. Appendix B extends both to the weaker balancing condition used elsewhere in the paper. Dütting et al., 2020, §5 and Appendix B

Setting

There are $n$ agents in a fixed order. Agent $i$ receives an outcome $x_i$ from a space $X_i$ containing a null outcome. A profile $x=(x_i)_i$ is feasible when it lies in $\mathcal F$. The model assumes downward closure: removing the outcomes of any group of agents from a feasible profile keeps it feasible. For a set of agents $S$, write $x_S$ for the profile retaining $x_i$ on $S$ and assigning the null outcome elsewhere. The prefix $x_{[i-1]}$ retains only the agents before $i$. Dütting et al., 2020, §2

A valuation profile $v$ assigns each agent a function $v_i:X_i\to\mathbb R$. The welfare of $x$ is $v(x)=\sum_i v_i(x_i)$. Every base valuation takes values in $[0,1]$, the normalization stated in §2. For any set $S$ of profiles, $v(\operatorname{OPT}(v,S))$ denotes the best welfare achievable in $S$. An allocation rule ALG chooses a feasible profile from a valuation profile. A pricing rule assigns a nonnegative, possibly infinite price $p_i(x_i\mid y)$ to outcome $x_i$ when the partial profile is $y$; an infeasible extension has infinite price. Dütting et al., 2020, pp. 547–548

An exchange-compatible family $(\mathcal F_x)_{x\in X}$ specifies a set of comparison profiles for each profile $x$. It is exchange compatible when replacing any one coordinate of $x$ by the corresponding coordinate of any $y\in\mathcal F_x$ gives a feasible profile. This property is required for every $x$ in the full outcome space. A rule $p^v$ is $(\alpha,\beta)$-balanced for valuation $v$, ALG, and that family, for constants $\alpha>0$ and $\beta\ge0$ (Definition 3.1), when both inequalities hold for every feasible $x$ and every $x'\in\mathcal F_x$:

$$\frac{v(\operatorname{ALG}(v))-v(\operatorname{OPT}(v,\mathcal F_x))}{\alpha} \le \sum_i p_i^v(x_i\mid x_{[i-1]}), \qquad \sum_i p_i^v(x'_i\mid x_{[i-1]}) \le \beta v(\operatorname{OPT}(v,\mathcal F_x)).$$

The maximum extension $V_i^{\max}$ of a base valuation space $V_i$ consists of nonempty finite pointwise maxima of elements of $V_i$. A base profile $\tilde v$ supports an extended profile $v$ at $x$ if $\tilde v_i\le v_i$ at every outcome and $\tilde v_i(x_i)=v_i(x_i)$ for every agent. ALG is consistent when $\tilde v(\operatorname{ALG}(\tilde v))\ge\tilde v(\operatorname{ALG}(v))$ whenever $\tilde v$ supports $v$ at $\operatorname{ALG}(v)$. The optimal allocation rule has this property by Lemma 5.2. Dütting et al., 2020, p. 554

Formalization targets

Closure under maxima

The goal is Theorem 5.3. Given one exchange-compatible family and a collection $(p^w)_{w\in V}$ balanced for every base profile, consistency of ALG preserves the same constants for every extended profile and every corresponding supporting base profile:

$$v\in V^{\max},\quad \tilde v\in V\text{ supports }v\text{ at }\operatorname{ALG}(v) \quad\Longrightarrow\quad p^{\tilde v}\text{ is }(\alpha,\beta)\text{-balanced for }v.$$

The milestone list records the welfare supremum comparison and the two price inequalities in the paper's proof. The family $\mathcal F_x$ remains the same for all base and extended profiles. Dütting et al., 2020, Theorem 5.3 and proof

Closure under addition and weak balancedness

Theorem 5.4 treats $m$ separate allocation problems. The joint outcome and feasible set are products; values and prices add across components; ALG applies each component's rule. It asserts balancedness with the same $\alpha$ and $\beta$. Appendix B changes the second balancedness bound to $\beta_1v(\operatorname{OPT}(v,\mathcal F_x))+\beta_2v(\operatorname{ALG}(v))$ and requires strong consistency for maximum closure. Theorems B.2 and B.3 preserve $\alpha,\beta_1,\beta_2$ under maxima and addition, respectively. Dütting et al., 2020, Theorems 5.4, B.2, B.3

Significance

The maximum closure theorem lets a balanced-price construction for a simple valuation class cover finite maxima of that class without worsening its balancing constants. The addition theorem lets separately priced markets be combined by summing prices. Together these two operations account for the XOS composition discussed immediately after Theorem 5.4; the paper uses the results to connect its general framework to combinatorial auctions and multidimensional matroid settings. Dütting et al., 2020, p. 555

These results have paper proofs. The work here is to state their exact deterministic content in Lean so later formalizations of the price constructions can import the closure theorems. The definitions of supporting valuations, exchange-compatible families, and extended-real prices are reusable beyond this mission. The companion statements keep the product-market and weak-balancedness variants alongside the central theorem, while their proofs remain to be formalized.

Difficulty

For maximum closure, the prices are indexed by a base profile $\tilde v$ but must be balanced for a different profile $v$ that is pointwise larger. A supporting profile agrees with $v$ only at ALG's outcome $\operatorname{ALG}(v)$, while condition (a) refers to $\operatorname{ALG}(\tilde v)$, an outcome ALG chooses for a different input, and both conditions refer to optimal welfare over $\mathcal F_x$, where $\tilde v$ and $v$ can differ. Balancedness of $p^{\tilde v}$ for $\tilde v$ therefore says nothing about $v$ on its own; without a hypothesis tying ALG's choices for $v$ and $\tilde v$ together the statement is false, which is why consistency (Definition 5.1) is part of the theorem. The formal statement must keep the real-valued optimum meaningful for maxima of base valuations, so the $[0,1]$ normalization of §2 is carried through to $V^{\max}$. Dütting et al., 2020, Definition 5.1 and Theorem 5.3

For addition, a direct product of the component comparison families has an edge case: a component family can be empty while another is nonempty. The paper's displayed product family then makes the lower balancedness inequality too strong. The theorem statements ask for an exchange-compatible family to exist, as the printed theorems do; they do not require that failing product family. This discrepancy is recorded for review. Dütting et al., 2020, proof of Theorem 5.4

Formalization scope

Agents and markets use zero-based finite indices; the paper writes agent indices from one. A profile's prefix contains exactly the agents with smaller indices. Valuations are functions to $\mathbb R$ with base values in $[0,1]$. The maximum extension uses a nonempty finite set of base functions, so its maximum is defined at every outcome. Optimal welfare is a real supremum; bounded valuations keep it finite, and the empty set has value zero. Prices are extended nonnegative reals so $+\infty$ is retained. The lower balancedness inequality embeds its real right side using ofReal, which handles a negative lower bound consistently with nonnegative prices. The upper inequality keeps the price sum in extended reals.

The maximum theorem quantifies over every extended profile and every supporting base profile, including genuinely new maxima. It keeps one exchange-compatible family for all valuations. The maximum-closure theorems require every base price to satisfy the pricing-rule condition and conclude it for the supporting price. ALG feasibility is assumed on $V^{\max}$, which contains the base profiles. The product theorems construct joint outcomes, additive values, componentwise ALG, and summed prices from the component data; they do not admit an unrelated joint allocation rule. Downward closure and a zero price for the null outcome at feasible partial allocations are included for the product statements. The latter is a disclosed assumption satisfied by the paper's pricing examples and needed to handle empty component families. No distribution or posted-price run is part of this deterministic mission. Lemma 5.2 and the strong-consistency companion take an optimal rule to be one that attains the welfare supremum over $\mathcal F$ on every profile in $V^{\max}$, the profiles to which Definitions 5.1 and B.1 apply it; the product companions additionally conclude that the summed prices form a pricing rule (infinite off $\mathcal F$). Their ALG feasibility premise concerns the component profiles supplied in the theorem.

The development needs finite dependent products and sums, finite maxima, real suprema of bounded sets, and extended nonnegative arithmetic. Contributions proving the three maximum-closure milestones, the goal, or the product-market companions are all within scope. A proof that specializes the supporting profile to $\tilde v=v$ would lose the intended maximum extension and does not satisfy the goal's universal quantification.

Selected references

• P. Dütting, M. Feldman, T. Kesselheim, and B. Lucier, Prophet Inequalities Made Easy: Stochastic Optimization by Pricing Nonstochastic Inputs, SIAM Journal on Computing 49(3):540–582, 2020. DOI: 10.1137/20M1323850.