Theoretical Computer Science

Motivation

Retailers that carry a limited range of products often know something about a customer before choosing which of those products to display. The customized assortment problem asks which products to carry when the displayed assortment may be tailored to the arriving customer's type. This separates the first-stage capacity decision from the later offer decision. El Housni and Topaloglu study the problem under a mixture of multinomial logit choice models and develop an approximation framework for it in their SSRN paper. This mission isolates their structural guarantee for Augmented Greedy, Theorem 4.2 of the PDF version dated 7 December 2021. The theorem identifies the revenue recovered from customer types whose optimal personalized offers agree with a chosen product subset.

The paper contrasts this setting with ordinary assortment optimization, where every type sees the same products. Its later approximation results use the structural guarantee here as a component. The classical comparison is the cardinality-constrained greedy bound for monotone submodular functions, associated with Nemhauser, Wolsey and Fisher (1978). The paper's Appendix B gives an instance in which the customized revenue function lacks global submodularity, so that classical result does not apply directly. El Housni and Topaloglu, §§4 and App. B.

Setting

Let $N=\{1,\ldots,n\}$ be a finite product set. Product $i$ has positive revenue $r_i$, and products are indexed with $r_1\ge\cdots\ge r_n>0$. Let $M=\{1,\ldots,m\}$ be customer types. A type-$j$ customer arrives with probability $\theta_j\ge0$, with $\sum_{j\in M}\theta_j=1$, and assigns each product $i$ a nonnegative preference weight $v_{ij}$. The no-purchase option has weight one. Offering an assortment $T\subseteq N$ to that customer gives MNL expected revenue

If the retailer initially carries only $S\subseteq N$, it can still choose the best offer to each customer type. Thus $f_j(S)=\max_{T\subseteq S}\operatorname{Rev}_j(T)$. For $C\subseteq M$, write $f^C(S)=\sum_{j\in C}\theta_j f_j(S)$, and abbreviate $f=f^M$. The first-stage capacity is $K$; an optimal solution $S^*$ of CAP maximizes $f(S)$ among sets with at most $K$ products. These definitions and the standing data assumptions are stated in §2 and §4 of the paper.

For each product $i$, the prefix $V_i=\{1,\ldots,i\}$ contains products at least as early in the revenue ordering. Greedy starts at the empty set, repeatedly adds an available product that maximizes the new objective value, and stops at cardinality $k$ or when the prefix is exhausted. Augmented Greedy runs Greedy on $V_i$ for each $i$, using $S\mapsto\sum_{j\in C}\theta_j\min(f_j(S),r_i)$, and returns whichever candidate has the greatest $f^C$ value. Both stages may break ties arbitrarily. El Housni and Topaloglu, §4.1.

For type $j$, use the optimal personalized assortment $S_j^*=\{i\in S^*:r_i\ge f_j(S^*)\}$, characterized by Lemma E.1. A type $j\in C$ is complete with respect to $P\subseteq N$ when $P\cap S_j^*=P\cap S^*$; let $C_P$ collect these types. The threshold choice matters because zero-weight products can be present in other optimal offers without helping a customer. El Housni and Topaloglu, Definition 4.1 and App. E.

Formalization targets

Theorem 4.2: complete-type revenue

For every $C\subseteq M$, $P\subseteq N$, $k$ with $|P\cap S^*|\le k$, and every output $\Delta$ of Augmented Greedy on $C,k$,

This is the mission goal, the structural performance statement of Theorem 4.2, p. 11. It does not assert a constant-factor approximation to all of CAP: it identifies the contribution from complete customer types.

Supporting targets

The milestone list follows the results used with this bound: monotonicity of $f_j$ from Appendix C; the MNL threshold assortment of Lemma E.1; submodularity of $S\mapsto\min(f_j(S),r_i)$ on $V_i$ from Lemma 4.3; and the cited $1-1/e$ Greedy guarantee for a nonnegative monotone submodular objective. The greedy milestone compares its output against every feasible set of cardinality at most $k$.

Significance

The theorem says that one algorithmic output captures a fixed fraction of the benchmark supplied by complete types, despite the absence of global submodularity of $f$. It connects the local behavior of truncated type revenues to the full customized assortment objective. The paper uses this result in the development of later algorithms; without it, the standard submodular greedy theorem gives no immediate conclusion for CAP. El Housni and Topaloglu, §§4–5.

The mathematical results are proved in the 2021 paper. The formalization work here is to give machine-checkable statements for the objective, the algorithm with all its legal tie choices, and the four supporting targets, then supply proofs. The MNL revenue formula is already available as a published platform definition; the local CAP and algorithm definitions specify the extra model needed by this theorem. A completed development could also support later CAP missions that use the same threshold and submodularity properties.

Difficulty

The tempting argument applies the classical greedy guarantee directly to $f$, since $f$ increases when more products are carried. Appendix B of the paper shows that this fails: even for one customer type, $f$ need not be submodular. Restricting the ground set to a revenue prefix and truncating each $f_j$ at that prefix's revenue level changes the submodularity question, but the final guarantee must still concern the untruncated $f^C$ objective. The threshold condition in the definition of $C_P$ is what makes that comparison meaningful. El Housni and Topaloglu, App. B, Lemma 4.3 and Theorem 4.2.

Formalization scope

Products and types are Fin n and Fin m; their zero-based Lean indices correspond to the paper's indices plus one. Assortments and type groups are finite sets. The model assumes $r_i>0$, $v_{ij}\ge0$, $\theta_j\ge0$, $\sum_j\theta_j=1$, and decreasing revenue order. The no-purchase weight is exactly one. CAP and personalized revenue use maxima over nonempty finite powersets, so empty input sets have their intended value rather than an arbitrary real supremum. The theorem keeps the source's optimality assumption on $S^*$, even though its particular inequality uses less.

The Greedy predicate describes each successive maximizer and the exact stopping rule. Augmented Greedy requires a Greedy output at every prefix and an $f^C$-maximizing choice among them. Thus the output is constrained by the printed algorithm, and the statement covers every tie-break. The type-$j$ assortment is defined from $S^*$ by the Lemma E.1 threshold, rather than supplied as a free set. These choices rule out a size-only output condition, an arbitrarily chosen $S_j^*$, a vacuous run predicate, and real supremum defaults. The target includes the corner cases $k=0$, $C=\varnothing$, and $P\cap S^*=\varnothing$, where its right side is zero. Arrival probabilities summing to one force $m\ge1$; Augmented Greedy has an output only when at least one product exists.

The reusable parts are the MNL threshold characterization, finite-set submodularity and the general Greedy bound. Contributions toward those lemmas, the paper's case analysis for Lemma 4.3, and the final structural theorem are in scope. Runtime claims, the paper's later logarithmic approximation theorems and its computational experiments are outside this mission.

Selected references

• Omar El Housni and Huseyin Topaloglu, Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models: Value of Personalized Assortments, SSRN 3830082, version of 7 December 2021; published as Operations Research 71(4), 2023. SSRN preprint. The mission's numbering and page citations use the pinned 2021 PDF.
• George L. Nemhauser, Laurence A. Wolsey and Marshall L. Fisher, An Analysis of Approximations for Maximizing Submodular Set Functions—I, Mathematical Programming 14, 265–294, 1978. DOI.

Motivation

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-$s$ substring is called an $s$-mer. The number of different $s$-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.

Setting

Let $T[1..n]$ be a text over the ordered alphabet $[1..\sigma]$. Its final symbol is a unique terminator \=1$, smaller than every other symbol in the text. For each$i\in[1..n]$, the **suffix**$T[i..n]$starts at$i$and ends at the terminator. The **suffix array**$SA[1..n]$is the permutation of$[1..n]$that lists these suffixes in increasing lexicographic order. Thus$SA[p]$is the starting position of the$p$th suffix. This is the setup of §2 of the source preprint, pp. 7–9.

The BWT symbol at position $p$ is the character just before the suffix at $SA[p]$. 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; r$denotes their number. The first and last BWT positions in each run correspond to **sampled text positions**. A text substring$T[i..j]$ is primary when its interval contains a sampled text position, as in Definition 5, p. 16.

For $1\le s\le n$, let $\mathcal S_s(T)$ be the set of length-$s$ strings occurring in $T$:

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.

Formalization targets

Primary occurrences

Lemma 8, p. 17 states that every nonempty substring of $T$ has an occurrence with the same contents that is primary. With $\operatorname{Sampled}(T)$ 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 $|\operatorname{Sampled}(T)|\le 2r$ stated in the proof of Lemma 9. These give precise intermediate claims in the paper's route to the count.

Distinct $s$-mers

The main goal is Lemma 9, p. 17:

Here $r$ is calculated from the BWT of the text's suffix array. Both inequalities on $s$ are part of the source statement. The bound concerns distinct strings of a fixed length, not the number $n-s+1$ of substring windows.

Significance

The theorem gives an explicit upper bound on the number of different length-$s$ 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-$s$ 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.

Difficulty

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: $n$ may be large even when $r$ 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.

Formalization scope

The Lean representation uses $\mathbb N$ for symbols and 1-based positions. The functions $T$ and $SA$ are read only on $[1..n]$. An IsText hypothesis enforces $n\ge1$, membership in $[1..\sigma]$, and the unique final terminator \=1$. An `IsSuffixArray` hypothesis says that$SA$maps$[1..n]$injectively into itself and orders its suffixes strictly; it does not presuppose any claim about BWT samples. Because that finite domain has$n$elements, these conditions describe a permutation. The BWT is computed from$T$and$SA$, with the predecessor of position 1 read as position$n$. 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 $s$-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 $O(\cdot)$ 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.

Selected references

• Travis Gagie, Gonzalo Navarro, and Nicola Prezza, Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space, arXiv:1809.02792v2, 2019. Preprint.
• Travis Gagie, Gonzalo Navarro, and Nicola Prezza, Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space, Journal of the ACM 67(1), 2020. DOI:10.1145/3375890. The mission follows the preprint's numbering and wording.

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$:

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:

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.

Motivation

Least-squares regression, $\min_X\|AX-B\|_F$ for a tall matrix $A\in\mathbb R^{n\times d}$ with $n\gg d$, is among the most frequently solved problems in numerical computation. Direct methods (QR or SVD) cost $O(nd^2)$ time, which is prohibitive when $n$ is in the millions. Sketching replaces the problem by a much smaller one: choose a matrix $S\in\mathbb R^{t\times n}$ with $t\ll n$, form $SA$ and $SB$, and solve $\min_X\|S(AX-B)\|_F$ instead. The question is when the solution of the small problem is nearly optimal for the original one.

Clarkson and Woodruff, Low Rank Approximation and Regression in Input Sparsity Time (STOC 2013; JACM 2017), showed that a very sparse random sketch (one non-zero per column, the CountSketch matrix) can be applied in time proportional to the number of non-zero entries of $A$ and still yields $(1+\varepsilon)$-approximate regression and low-rank approximation. §7 of that paper isolates the deterministic part of the argument: two conditions on a fixed sketch $S$ that guarantee a near-optimal solution, whatever distribution produced $S$.

Timeline. Sarlós (FOCS 2006) introduced sketch-and-solve regression with fast Johnson–Lindenstrauss transforms. Drineas, Mahoney, Muthukrishnan and Sarlós (Numer. Math. 2011) stated the structural conditions for single-response regression (their Lemma 1); Theorem 36 of Clarkson–Woodruff generalizes it to multiple responses. Clarkson and Woodruff then supplied the sparse sketches meeting the conditions in input-sparsity time.

Setting

All matrices are real. For a vector $v$ let $\|v\|_2^2=\sum_iv_i^2$; for a matrix $M$ let $\|M\|_F^2=\sum_{i,j}M_{ij}^2$. Fix $A\in\mathbb R^{n\times d}$ of rank at most $r$, a right-hand side $B\in\mathbb R^{n\times d'}$ and a sketch $S\in\mathbb R^{t\times n}$. Let $C(A)=\{Ax\}$ be the column space and $U\in\mathbb R^{n\times k}$ a matrix with orthonormal columns ($U^\top U=I$) spanning $C(A)$.

• $Y^*$ is a least-squares minimizer: it minimizes $\|AY-B\|_F^2$ (problem (8)).
• $\tilde Y$ is a sketched minimizer: it minimizes $\|S(AY-B)\|_F^2$ (problem (7)).
• $S$ is a subspace embedding for $A$ with parameter $\eta$ if $\bigl|\|SAx\|_2^2-\|Ax\|_2^2\bigr|\le\eta\|Ax\|_2^2$ for every $x$.
• $S$ satisfies the approximate matrix multiplication event (Lemma 32) for a pair $(U,W)$ with error parameter $e$ if $\|U^\top S^\top SW-U^\top W\|_F^2\le e^2\|U\|_F^2\|W\|_F^2$.

Formalization targets

Goal: Theorem 36 (p. 24)

If $S$ is a subspace embedding for $A$ with $0\le\eta\le1/2$ and satisfies the event of Lemma 32 for $(U,B-AY^*)$ with error parameter $\sqrt{\varepsilon/r}$, then every sketched minimizer satisfies

This is the explicit form the paper's proof establishes; the printed $(1+\epsilon)$ bound on norms follows after rescaling $\varepsilon$.

Milestones

• Fact 34 (Pythagorean theorem): $C^\top D=0\Rightarrow\|C+D\|_F^2=\|C\|_F^2+\|D\|_F^2$.
• Fact 35 (normal equations): $C^-D$ is a minimizer; every minimizer $X^*$ satisfies $C^\top(CX^*-D)=0$ and $\|CX-D\|_F^2=\|C(X-X^*)\|_F^2+\|CX^*-D\|_F^2$.
• Lemma 37: for $A$ with orthonormal columns, $\|A(\tilde Y-Y^*)\|_F\le2\sqrt\varepsilon\|B-AY^*\|_F$.
• Theorem 39 (affine embeddings, an independent companion result of §7.5): under an embedding with parameter $\varepsilon\le1/2$ and the event of Lemma 32 with parameter $\varepsilon/\sqrt r$, $\|S(AX-B)\|_F^2-\|S\tilde B\|_F^2$ equals $\|AX-B\|_F^2-\|\tilde B\|_F^2$ up to $\pm2\varepsilon\|AX-B\|_F^2$ for all $X$, and $\|S(AX-B)\|_F^2=(1\pm3\varepsilon)\|AX-B\|_F^2$ if $S$ also preserves $\|\tilde B\|_F^2$ to $1\pm\varepsilon$.

Significance

Theorem 36 separates the algorithm design for sketched regression from its correctness proof: any random construction (CountSketch, subsampled randomized Hadamard transforms, leverage-score sampling, Gaussian matrices) yields a $(1+O(\varepsilon))$-approximate regression solver once it is shown to satisfy the two conditions with constant probability. Clarkson and Woodruff use it for their input-sparsity-time regression algorithm (Theorem 38) and, through Theorem 39 and affine embeddings, for low-rank approximation. The same conditions recur throughout the randomized numerical linear algebra literature (see Woodruff's survey Sketching as a Tool for Numerical Linear Algebra, 2014).

The results are proved in the paper (§7.3, §7.5 and Appendix A, p. 37). To our knowledge none has a machine-checked proof. Formalizing them produces a reusable, distribution-free layer of sketching theory: the probabilistic statements about specific sketches can then be proved separately and composed with it.

Difficulty

The obvious argument applies the subspace embedding to the residual $A\tilde Y-B$, but that vector does not lie in $C(A)$, so an embedding of $C(A)$ alone says nothing about it; embedding $C(A)$ augmented with the columns of $B$ instead costs a sketch dimension that grows with $d'$. The hypotheses of Theorem 36 control the optimal residual $B-AY^*$ only through the approximate-product condition, which is far weaker than norm preservation, and the difficulty is to transfer that control to the sketched solution (Lemma 37) with the constants $2\sqrt\varepsilon$ and $1+4\varepsilon$. A second obstacle is the passage from a general $A$ of rank at most $r$ to an orthonormal basis $U$ of $C(A)$: it changes $\|A\|_F$, which is why the approximate-product condition is stated for $U$.

Formalization scope

Matrices are Matrix (Fin m) (Fin n) ℝ; squared norms are explicit sums sqNorm and frobSq; the column space is the range of Matrix.mulVecLin; rank is Matrix.rank. Everything is deterministic: $S$ is an arbitrary fixed matrix and no probability space appears. The committed conventions are:

1. The subspace embedding is in squared form. In Theorem 36 and Lemma 37 its parameter $\eta$ plays the paper's $\epsilon_0^2$ (so $\epsilon_0\le1/\sqrt2$ becomes $\eta\le1/2$), which is how the proof of Lemma 37 (p. 37) uses it; in Theorem 39 the parameter is $\varepsilon$ itself, as that proof uses it.
2. "$S$ satisfies Lemma 32" is the event inside the probability, for the pair $(U,B-AY^*)$ (resp. $(U,\tilde B)$) that the proofs use, with $\le$ in place of the printed $<$ (a weaker hypothesis).
3. $\tilde Y$, $Y^*$, $X^*$ are arbitrary minimizers; "the solution" need not be unique. The Moore–Penrose inverse is specified by the four Penrose equations.
4. $r\ge1$ guards $\varepsilon/r$ and $\varepsilon/\sqrt r$; "$n>d$" (§7) concerns running times and is not assumed.

A trivializing formalization is ruled out: $\tilde Y$ is never defined as $Y^*$, the approximate-product hypothesis is an inequality and not the exact identity $U^\top S^\top S(B-AY^*)=0$, $\eta$ is non-negative, and the goal is stated for general $A$ of rank at most $r$, not only for orthonormal $A$. The hypotheses are jointly satisfiable (for instance $S=I$).

A complete development needs the Frobenius inner product and its Pythagorean identity, the normal equations for matrix least squares, the existence of the Moore–Penrose inverse, and the spectral-norm bound for a symmetric matrix from its quadratic form; all are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Theorem 36, are welcome.

Selected references

• K. L. Clarkson and D. P. Woodruff, Low Rank Approximation and Regression in Input Sparsity Time, arXiv:1207.6365v4, 2013; J. ACM 64(6), 2017. https://arxiv.org/abs/1207.6365
• P. Drineas, M. W. Mahoney, S. Muthukrishnan and T. Sarlós, Faster Least Squares Approximation, Numerische Mathematik 117(2), 2011. https://arxiv.org/abs/0710.1435
• T. Sarlós, Improved Approximation Algorithms for Large Matrices via Random Projections, FOCS 2006. https://doi.org/10.1109/FOCS.2006.37
• D. P. Woodruff, Sketching as a Tool for Numerical Linear Algebra, Foundations and Trends in Theoretical Computer Science 10(1–2), 2014. https://arxiv.org/abs/1411.4357

Motivation

The paper of Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (2016) has an algorithmic headline. This mission concerns one of its finite graph lemmas, Lemma 2.9. The lemma translates a condition phrased separately for every connected component into a condition on three vertex sets. A reader of graph decompositions encounters both forms: components express what remains connected after deleting vertices, while a small fixed number of parts gives a compact way to state constraints on a partition. Lemma 2.9 identifies exactly when the two forms agree for the half-balance threshold. The same result appears again in the paper as Lemma 6.2, where the authors use it in a later section.

The result does not require a tree decomposition or a treewidth hypothesis. It holds for every finite graph. That generality makes it a useful standalone target: the definitions of deletion, connected components, and the weighted three-partition can be reused wherever graph separators are studied. The mission follows the published SIAM article, with printed page 328 for the main lemma and pages 363–364 for its restatement and the supporting combinatorial observation.

Setting

Let $G$ be a finite simple graph with vertex set $V(G)$. Let $S$ and $X$ be subsets of its vertices. The deleted graph $G\setminus X$ retains precisely the vertices outside $X$ and the edges joining them. Two remaining vertices are in the same connected component when a walk joins them without passing through any vertex of $X$. Write $C_X(u)$ for the vertex set of the component containing $u\notin X$. This interpretation follows the paper's notation on page 320.

A balanced $S$-separator is a set $X$ for which each component of $G\setminus X$ contains at most half the vertices of $S$:

The paper introduces this phrase on page 321. Here balance is a property of $X$ relative to $S$; it imposes no bound on the size of $X$. The denominator counts all vertices of $S$, including any that lie in $X$.

A three-part partition of $V(G)\setminus X$ is a triple $(M_1,M_2,M_3)$ of pairwise disjoint sets whose union is $V(G)\setminus X$. A part may be empty. Two parts have no edge between them if no edge of $G$ joins a vertex of one to a vertex of the other. Since the graph is undirected, checking the three unordered pairs of distinct parts covers the requirement for every $i\ne j$.

Formalization targets

Lemma 2.9: balanced separators and three parts

The goal is the equivalence stated on page 328, also restated as Lemma 6.2 on page 363:

The equivalence is the target, including both directions. It applies even when $S$ or $V(G)\setminus X$ is empty. It does not include a bound on $|X|$.

Lemma 6.3: three bounded sums

The main supporting result on page 363 says that nonnegative integers $a_1,\ldots,a_p$ with total $q$ and $a_i\le q/2$ can be divided into three classes, each with sum at most $q/2$. The milestone list also records the paper's merge inequality and its assertion that a component cannot cross between parts having no edge between them. These are the specific claims used in the published discussion of Lemma 2.9.

Significance

Lemma 2.9 lets a componentwise balance condition be represented by three sets whose coverage, disjointness, edge separation, and cardinalities can be inspected directly. It gives an exact equivalence, so the three-part formulation loses no balanced separators and introduces none that fail the original definition. That is the mathematical content needed when a later argument represents a separator by a bounded number of regions rather than by a list of all its components. The result is already proved in the 2016 paper; the open work in this mission is a machine-checked formalization of that known result and its cited supporting claims.

Formalizing the equivalence also establishes reusable interfaces for vertex deletion and component membership in a finite simple graph. A future development can state a separator condition using IsBalancedSSep, or use the three-part conclusion without redefining what a component of $G\setminus X$ means. The independent integer-partition lemma has uses whenever indivisible nonnegative weights, each no larger than half the total, must be grouped into three bounded classes. Nothing in that statement depends on graphs.

Difficulty

There may be arbitrarily many components of $G\setminus X$, although the conclusion permits only three parts. Simply assigning all components to one part can violate the half bound, while splitting a component between different parts may create forbidden edges. A component's weight is the number of its vertices in $S$, and those weights can be uneven or zero. The theorem has to accommodate all such patterns without changing the threshold $|S|/2$. In the converse direction, the absence of edges between the three parts must control entire walks, not only their first edge; ordinary connectivity in $G$ would allow a walk through $X$ and would describe the wrong components.

Formalization scope

The Lean development uses SimpleGraph V with V : Type, [Fintype V], and [DecidableEq V]. Vertex sets are Finset V. The shared walk-based AvoidReach G X u v requires every vertex on a walk to lie outside $X$, including both endpoints; avoidComp G X u collects the vertices reachable in this way. It is used only for $u\notin X$ when quantifying over components. This shared definition matches the paper's $G\setminus X$. The graph itself need not have decidable adjacency, since the statements concern propositions rather than computations.

Half bounds are written as $2c\le |S|$ or $2c\le q$ in natural-number arithmetic. This is equivalent to the paper's rational half bound and avoids any interpretation of natural-number division. The three parts may be empty, so $X=V(G)$ is a genuine boundary case. The set $S$ may meet $X$; the right-hand denominator remains $|S|$. The graph may have no vertices. There is no treewidth parameter or size condition on $X$: adding one would change Lemma 2.9 and can make its reverse implication false. Nor may components be computed using connectivity in the original graph, where paths through deleted vertices could merge them.

The required infrastructure is finite graph walks, finite sets, cardinalities, sums over finite index types, and the three original claims in the milestone list. The graph-component definitions and the integer grouping theorem are reusable beyond this mission. Contributions that prove any milestone or the full equivalence under exactly these conventions are in scope.

Selected references

• H. L. Bodlaender, P. G. Drange, M. S. Dregi, F. V. Fomin, D. Lokshtanov and M. Pilipczuk, A c^k n 5-approximation algorithm for treewidth, SIAM Journal on Computing 45(2):317–378, 2016. DOI: 10.1137/130947374.