PaperlayerView exact revision on arXiv

Source-linked AI summary

SparseStack Is an Optimal Oblivious Subspace Embedding

Diar Heidary

arXiv:2609.02978v2cs.DScs.NAmath.NA

TL;DR

SparseStack was conjectured to achieve optimal oblivious subspace embedding parameters with sparse columns. This paper proves those parameters for the fully independent construction using coupling and finite-dimensional operator bounds, with an additive estimate for shared-factor contributions.

  • Problem

    Whether fully independent SparseStack attains the conjectured oblivious subspace embedding row and sparsity parameters remained an open question.

    Source: §1.2 · p. 4

  • Method

    The proof couples signed one-hot selectors to independent-entry variables and bounds their moments through finite-dimensional operator estimates.

    Source: §1.4 · p. 5

  • Results

    m = O((d + log(d/δ))/ε^2) rows and s = O(log(d/δ)/ε) nonzeros per column suffice for fully independent SparseStack.

    Source: §1.2 · p. 4

  • Takeaways & Limitations

    The shared-factor estimate is additive, bounding ℓ occupied sites by d + ℓ - 1 rather than dℓ.

    Source: §4 · p. 14

    The result covers fully independent SparseStack and fixed U (or U independent of Π), not limited independence, other sparse distributions, or adaptive U.

    Source: §8 · pp. 22–23

Abstract

from arXiv · show

We prove that fully independent SparseStack achieves the oblivious subspace embedding parameters conjectured by Nelson and Nguyen (FOCS 2013): $m=O((d+\log(1/\delta))/\varepsilon^2)$ rows and $s=O(\log(d/\delta)/\varepsilon)$ nonzero entries per column for distortion $\varepsilon$ and failure probability $\delta$ on any fixed $d$-dimensional subspace, with explicit constants. The proof turns random-matrix concentration into a problem in finite-dimensional linear algebra. A coupling first reduces the moment estimates to a model with independent finite-valued entries. We represent these variables by multiplication operators, so their matrix moments become exact matrix elements of a deterministic operator on a finite tensor product. The central estimate bounds the contribution of $\ell\ge1$ occupied sites sharing the external factor $\mathbb{R}^d$ by $d+\ell-1$ rather than $d\ell$, yielding additive dependence on the dimension and the moment order. This approach controls both spectral edges without Gaussian comparison. The main theorem has been formally verified in Lean 4.

1 Introduction

The paper proves that fully independent SparseStack achieves the conjectured oblivious subspace embedding parameters for fixed subspaces. Its proof reduces moment bounds to finite-dimensional operator estimates, including a shared-factor bound additive in dimension and moment order.

1.1 Sparse subspace embeddings

  • An oblivious subspace embedding preserves the norms of vectors in each fixed d-dimensional subspace within distortion ε, with failure probability δ.The Gram error controls both spectral edges of the sketch restricted to the subspace.Source: §1.1 · p. 3
  • SparseStack stacks s independent CountSketch blocks, giving each column exactly s nonzero entries, each equal to ±s^-1/2; the result assumes full independence.The result does not cover limited-independence implementations.Source: §1.1 · p. 3

1.2 Main result

  • m = O((d + log(1/δ))/ε^2) rows and s = O(log(d/δ)/ε) nonzeros per column suffice for fully independent SparseStack, with explicit constants.The constants are not optimized.Source: §1.1 · p. 3, §1.2 · p. 4
  • For a fixed U, the theorem's guarantee also holds when U is random and independent of Π, but not when U depends on Π.Source: §1.2 · pp. 3–4

1.3 Related work

  • The result attains the conjectured row and sparsity parameters for fully independent SparseStack, without Gaussian comparison, but does not cover other OSNAP distributions or limited independence.Source: §1.3 · p. 4

1.4 Overview of the proof

  • The proof bounds even moments of the Gram error, couples signed one-hot selectors to an independent-entry model, and represents its moments as matrix elements of a deterministic finite-tensor operator.The operator acts on a space graded by total level and splits into bands that raise, preserve, or lower grade.Source: §1.4 · p. 5
  • The band estimates use the shared-factor bound d + ℓ - 1 for ℓ light sites, then control moments and apply Markov's inequality to obtain the failure bound.The moment expansion uses words that stay below grade 2q; q is chosen from d and δ.Source: §1.4 · pp. 5–6
  • The main theorem has also been formally verified in Lean 4.Source: §1.4 · p. 6

2 Reduction to independent entries

Because unit-norm sketch columns make the Gram error a hollow sum over distinct columns, a signed-selector coupling can transfer its moment bound to an independent-entry model. Conditional Jensen then transfers the Schatten-moment bound back to the original model.

2.1 The hollow Gram error

  • The Gram error is a hollow sum over distinct columns, and the absence of diagonal terms makes the coupling applicable.Source: §2.1 · p. 6

2.2 A coupling with an independent-entry vector

  • The coupling replaces each signed one-hot selector with an independent-entry vector in {0, ±1}, with the selector recovered as a conditional expectation up to a constant factor.The conditional selector law is uniform over signed basis vectors and independent of the proxy vector's support size.Source: §2.2 · p. 7

2.3 Convex-order transfer

  • Conditional Jensen transfers the even Schatten-moment bound from the original hollow Gram error to its independent-entry counterpart; diagonal terms are excluded because they incur an extra factor.The comparison uses a convex Schatten-norm power and a conditional barycenter.Source: §2.3 · pp. 7–8

3 A finite tensor-product model for the moments

The section converts moments of independent finite-valued entries into matrix elements of a deterministic operator on a finite tensor product. Its grading and row-operator identities organize the operator into pieces that can be bounded later.

3.1 Independent three-point entries

  • The independent-entry model uses a three-point variable with mean zero, variance one, and fourth moment b.Source: §3.1 · p. 8

3.2 Multiplication by one entry

  • Multiplication by one entry is represented in a three-dimensional orthonormal basis by a Jacobi matrix decomposed into raising and lowering legs.The heavy-leg coefficient b −1 is the only place sparsity enters the local model.Source: §3.2 · pp. 8–9

3.3 Sites, patterns, and the product space

  • Tensoring the local spaces over all mn sites gives an orthonormal pattern basis, with the all-zero pattern as the vacuum.Under the isometry to the array’s function space, the vacuum represents the constant function and each lifted J acts as multiplication by its entry.Source: §3.3 · pp. 9–10

3.4 The moment identity

  • For every integer k ≥ 0, the expected trace moment is represented by a vacuum matrix element of the deterministic operator’s k-th power.The identity follows by identifying the tensor-product operator with multiplication by the random matrix-valued function.Source: §3.4 · p. 10

3.5 Grading and the three bands

  • Grading the pattern space by total level makes the operator split into three bands that shift grade by +2, 0, or −2.The band decomposition follows because each local leg changes a site’s level by one.Source: §3.5 · p. 11

3.6 Band inventory

  • Each band term acts on two sites in one row, contracting and re-emitting the external vector through that row’s frame vectors.The expansion sorts terms by grade shift and assigns coefficients according to their number of heavy legs.Source: §3.6 · p. 12

3.7 Row operators and a factorization identity

  • Row operators factor sums over distinct sites into Gram operators plus diagonal terms, yielding identities such as L0 = (bG − D1) + H′.The Y+ and Y0 families are instead bounded directly because factorization is unsuitable for them.Source: §3.7 · p. 13

4 The shared-factor light-sector inequality

The shared-factor light-sector inequality bounds the operator contribution from occupied light sites additively in the dimension and their number. A labelled tensor-product estimate is compressed to configurations with distinct sites to obtain the bound for the light sector.

4 The shared-factor light-sector inequality

  • On grade κ, the light Gram operator is positive semidefinite and bounded above by (d + κ − 1)I, hence also by (d + κ)I.Blocks with no light sites contribute zero; on the others ℓ ≤ κ.Source: §4 · pp. 14–15
  • For ℓ light sites, the relevant operator norm is at most d + ℓ − 1, rather than the dℓ bound from treating sites separately.All light sites share one external factor; their rank-one contributions overlap across sites only through an operator of norm one.Source: §4 · p. 14
  • The lemma proves the bound by estimating ℓ copies of a one-particle operator on labelled tensor slots, then compressing to the distinct-site block.The labelled model permits repetitions; the hard-core block is indexed by sets of ℓ distinct light sites.Source: §4 · pp. 14–15
  • The labelled shared-factor bound is attained before compression, while compression preserves the upper bound but need not preserve equality.For n > d, decomposing column slots into im(U) and its orthogonal complement leaves the same bound with the number of active slots.Source: §4 · p. 16

5 Row-local hop estimates

The row-local hop estimates bound operators that change site levels within one sketch row, using counts of sites at specified levels. Their applications cover grade-changing and grade-preserving terms, as well as heavy-leg Gram operators.

5 Row-local hop estimates

  • The row-local hop estimate bounds one-site and two-site row operators using the maximum input and output counts of sites at specified levels.For two-site hops, the estimate reindexes inputs by output patterns and applies row analysis and synthesis inequalities.Source: §5 · pp. 16–17
  • The applications bound Y+, Y0, and H′ using light-site counts, with the Y0 estimate also using the input heavy-site count.L+ is treated separately because applying the same estimate would count free input sites, of order mn.Source: §5 · p. 17
  • The heavy Gram operators for R and R† are bounded by the row-occupation operator Nr.The two bounds apply to Sr(R)Sr(R)† and Sr(R†)Sr(R†)†, respectively.Source: §5 · pp. 16–17
  • Table 1 groups three applications on Kν by their output grades and two applications on row-grade strata by their shifts; the latter vanish when ℓ = 0.For the two row-stratum applications, the stated count satisfies N ≤ ℓ when ℓ ≥ 1.Source: Table 1 · p. 18

6 Band estimates

The band estimates combine block Cauchy–Schwarz with four Gram budgets to control heavy, light, and mixed contributions. A uniform envelope collects these bounds across grades, with the light–light estimate sharp at grade zero.

6.1 A block Cauchy–Schwarz inequality

  • The block Cauchy–Schwarz lemma bounds a sum of projected compositions using the product of two operator norms, enabling estimates through Gram operators.The application uses grade-homogeneous operators and preserves Loewner bounds under compression to a grade sector.Source: §6.1 · pp. 18–19

6.2 The four Gram budgets

  • Four Gram budgets bound G(P†), G(P), G(R), and G(R†) by bG, (d + κ)I, κI, and κI, respectively.The diagonal operators D0, D1, and DH are bounded by mI, κI, and κI on their stated spaces.Source: §6.2 · p. 19

6.3 Heavy–heavy terms

  • The heavy–heavy estimates give ∥H+|Kν∥ ≤ ν + 1 and ∥H0|Kν∥ ≤ 2ν.These follow from the heavy Gram bounds and the diagonal-operator estimate.Source: §6.3 · p. 19

6.4 Light–light terms

  • At ν = 0, the light–light bound satisfies ∥m−1L+|K0∥² ≤ (d + 1)/m and is attained in the limit of frames with maxi ∥ui∥ → 0.For each row and unordered pair {i, j}, the corresponding coefficient is (Uij + Uji)x.Source: §6.4 · p. 20

6.5 Mixed terms

  • The mixed-term estimates combine the X and Y components, and the stated bound holds without restricting the relative sizes of ν and m.The first term in the bound could be halved, but the authors retain the stated form for the uniform table.Source: §6.5 · p. 20, §6.6 · p. 20

6.6 The uniform band envelope

  • The uniform band envelope collects bounds for all three components of B+, B0, and B− across grades ν, with the last-row entries vanishing for ν < 2.For ν ≥ 2, each last-row entry is the corresponding +2 bound at grade ν − 2.Source: §6.6 · p. 20, Table 2 · p. 21

7 Proof of the main theorem

The proof bounds high moments by expanding the operator into grade-changing components, then converts those estimates into a probability guarantee. Integer rounding yields the stated parameters and explicit constants.

7.1 The moment bound

  • For M2q, a nonvanishing word has k≤q upward and k downward steps, keeping every grade between 0 and 2q; summing over words and α∈[d] gives the first bound in (83).Source: §7.1 · p. 21

7.2 From moments to probability

  • The moment bound and Markov’s inequality establish the probability guarantee once the chosen parameters satisfy the stated inequalities.The proof uses 2^-q ≤ δ/d to conclude (8).Source: §7.2 · pp. 21–22

7.3 Integer rounding and explicit constants

  • Rounding s and m proves the explicit parameter bounds and completes Theorem 1.1.The proof uses s = ⌈λ⌉ and m = sb, with m < 2M0.Source: §7.3 · p. 22

8 Scope and limitations

The proof combines coupling, moment transfer, operator bounds, and rounding to establish the theorem. Its stated restrictions include full independence, a fixed or independently chosen subspace, and the SparseStack distribution.

Scope and limitations

  • All hash values and signs must be independent; a limited-independence version would require a separate joint-moment computation for its chosen encoding.The 2q-th Gram-error moment can involve up to 4q column selectors, so 2q-wise independence of primitive variables does not itself provide the needed moment matching.Source: §8 · p. 22
  • The theorem covers a fixed U or one independent of Π, but not a U chosen dependently on Π.For independent random U with orthonormal columns, conditioning on U preserves the guarantee.Source: §8 · p. 22
  • The result is for the SparseStack distribution, not every sparse embedding with s nonzeros per column.Source: §8 · p. 23
  • The constants are not optimized; identified losses include factors from the number of bands and terms in the envelope.Source: §8 · p. 23

A Verification status

The fixed-matrix theorem and its load-bearing estimates are kernel-checked in Lean 4, while matching the formal declarations to the manuscript remains a human comparison.

Version history

  • Versions through 1.6.1 used an earlier title; Version 1.8 reorganized and expanded exposition, and Version 2.0 revised the abstract and related-work attributions without changing results or proofs.The main theorem, parameter choices, final band envelope, and numerical constants remained unchanged.Source: A Verification status · p. 23

Artifact and availability

  • The artifact uses Lean 4.33.0 and a specified mathlib commit; its canonical manuscript, formal source, and audit record are in the project repository.The repository build command is cd formal && lake build.Source: A Verification status · p. 23

Main statement

  • The main matrix declaration assumes d ≥ 1, 0 < ε ≤ 1, 0 < δ ≤ 1, a real U, and UᵀU = Id, with no further hypotheses.Its conclusion packages the SparseStack law, failure and two-sided event bounds, exact column sparsity, parameter bounds, b ≥ 2, and m = sb.Source: A Verification status · p. 23

Axiom audit

  • The axiom audit reports only propext, Classical.choice, and Quot.sound, and the source sweep found none of the listed escape hatches.The sweep covered sorry, admit, project-defined axioms, unsafe, partial, opaque, implemented_by, and native_decide.Source: A Verification status · p. 23

Correspondence with the paper

  • The Lean theorem matches Version 2.0's real fully independent signed-hash SparseStack law, normalization, constants, failure event, two-sided OSE event, and sparsity bounds.The comparison also confirms the same definitions of q, Dq, s, M0, b, and m, with n ≥ 1 following from d ≥ 1 and UTU = Id.Source: A Verification status · p. 23
  • Kernel checks cover the concrete heavy, light, and mixed band modules, final band envelope, moment expansion, Markov step, Gram/OSE equivalence, and integer rounding.The three directional uses and two heavy-leg uses of the merged row-local hop lemma are checked separately.Source: A Verification status · pp. 23–24

What is not verified

  • Lean accepted the stated declarations after elaboration; it does not check the paper's prose or certify that the formal statement captures the intended external problem.The theorem-level correspondence is a human comparison.Source: A Verification status · pp. 23–24

B Notation index

The notation index groups the model and parameters, tensor-product construction, grade and block operators, and row-operator and envelope notation used in the paper.

Model and parameters

  • The model uses n for ambient dimension, d for subspace dimension, U for a fixed orthonormal-column matrix, and ε and δ for distortion and failure probability.It defines q = max{1, ⌈log2(d/δ)⌉}, Dq = d + 2q + 1, and M0 = Λ²Dq/ε².Source: B Notation index · p. 25
  • The sparsity parameters are s nonzeros per column, b rows per block, m = sb total rows, and h = b − 1.The index also names the CountSketch blocks, hash rows, signs, and SparseStack matrix.Source: B Notation index · p. 25

Tensor-product model

  • The tensor-product model uses sites in [m] × [n], product space (R³)⊗mn, a vacuum and local basis, plus a Jacobi matrix and its four legs.Patterns, basis vectors, grades, level-j sites, row grades, and grade-sector projections are also defined.Source: B Notation index · p. 25

Blocks and grade sectors

  • The block notation identifies a heavy set T with ℓ light sites, its basis vectors, and the complementary columns I \ T.The grade-ν sector is Hν, with Kν = Rᵈ ⊗ Hν and associated orthogonal projections.Source: B Notation index · p. 25

Operators and envelopes

  • The operator index names the band families, row operator Sr(Z), Gram operator G(Z), diagonal operators, and envelope scales and ladder constant.It also defines G(P†) and the transpose light hop.Source: B Notation index · p. 25
Loading 2609.02978v2…