Convexity of the expected error of volume-sampled column subsets
For positive reals $\lambda_1, \dots, \lambda_n$ let $e_j(\lambda)$ be their $j$-th elementary symmetric polynomial, with $e_0 = 1$ and $e_{n+1} = 0$, and let $$f(j) = \frac{(j + 1)\, e_{j+1}(\lambda)}{e_j(\lambda)}, \qquad 1 \le j \le n.$$ If $\lambda_1, \dots, \lambda_n$ are the eigenvalues of $A^{\mathsf T}A$ and a set $S$ of $j$ columns of $A$ is drawn with probability proportional to $\det(A_S^{\mathsf T}A_S)$ (volume sampling), then $f(j)$ is the expected squared Frobenius error $\mathbb{E}\|A - P_S A\|_F^2$, where $P_S$ is the orthogonal projector onto the span of the chosen columns (Deshpande, Rademacher, Vempala and Wang).
Problem. Is $f$ discretely convex, that is, is $$f(j - 1) - 2f(j) + f(j + 1) \ge 0 \qquad (2 \le j \le n - 1)$$ for every $n \ge 3$ and all positive reals $\lambda_1, \dots, \lambda_n$?
Source: Dereziński, Khanna and Mahoney (2020), Conjecture 1.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- CO, PR
- Keywords
- column subset selection, elementary symmetric polynomials, OpenProblemsInNLA, volume sampling
References
@inproceedings{derezinski2020,
author = {Derezi{\'n}ski, Micha{\l} and Khanna, Rajiv and Mahoney, Michael W.},
title = {Improved guarantees and a multiple-descent curve for Column Subset Selection and the {N}ystr{\"o}m method},
booktitle = {Advances in Neural Information Processing Systems 33 (NeurIPS 2020)},
publisher = {Curran Associates, Inc.},
year = {2020},
pages = {4953--4964},
eprint = {2002.09073},
archivePrefix = {arXiv},
}
@article{deshpande2006,
author = {Deshpande, Amit and Rademacher, Luis and Vempala, Santosh S. and Wang, Grant},
title = {Matrix approximation and projective clustering via volume sampling},
journal = {Theory Comput.},
volume = {2},
number = {12},
year = {2006},
pages = {225--247},
doi = {10.4086/toc.2006.v002a012},
}
@misc{openproblemsinnla-ra07,
author = {Townsend, Alex},
title = {{RA-07}: Convexity of the expected error of volume-sampled column subsets},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/randomized-and-low-rank-approximation/RA-07/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00117.
namespace RegistryProblems.OP_00117
noncomputable section
open scoped BigOperators Polynomial
/-- The actual canonical sum over all subsets of the indicated cardinality. -/
def elementarySymmetric {n : ℕ} (lam : Fin n → ℝ) (j : ℕ) : ℝ :=
((Finset.univ : Finset (Fin n)).powersetCard j).sum fun S => S.prod lam
/-- The exact sequence in RA-07, defined using ordinary real division. -/
def errorSequence {n : ℕ} (lam : Fin n → ℝ) (j : ℕ) : ℝ :=
((j + 1 : ℕ) : ℝ) * elementarySymmetric lam (j + 1) / elementarySymmetric lam j
/-- OP-00117: Convexity of the expected error of volume-sampled column subsets -/
def _root_.RegistryProblems.Problem_OP_00117 : Prop :=
∀ n : ℕ, 3 ≤ n → ∀ lam : Fin n → ℝ, (∀ i, 0 < lam i) →
∀ j : ℕ, 2 ≤ j → j ≤ n - 1 →
0 ≤ errorSequence lam (j - 1) - 2 * errorSequence lam j + errorSequence lam (j + 1)
end
end RegistryProblems.OP_00117
Formalised by George Stepaniants (Apache-2.0); reviewed by clemens-admin.
Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.
Resolving this problem in Lean
Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.
In lakefile.toml:
[[require]] name = "RegistryProblems" git = "https://github.com/cthalhammer/registry-problems" rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"
In your proof:
import RegistryProblems.OP_00117 theorem resolution : RegistryProblems.Problem_OP_00117 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00117" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00117 := by sorry
You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.
Resolution claims
Proves the complete canonical discrete-convexity assertion for (j+1)e_(j+1)/e_j over every positive real spectrum. Actual subset sums, polynomial derivatives, full root multiplicities and an exact nonnegative pair certificate connect the proof to the original ratios.
For positive numbers $\lambda_1,\ldots,\lambda_n$, let $e_j$ be their elementary symmetric polynomials, with $e_0=1$ and $e_{n+1}=0$. We prove that $(j+1)e_{j+1}/e_j$ is a decreasing convex sequence on $\{0,\ldots,n\}$. The proof reduces each second difference to the nonnegative quantity $s_1s_3-s_2^2$ for the reciprocal roots of a derivative of the generating polynomial. This proves Conjecture 1 of Dereziński, Khanna, and Mahoney. We give a …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, RA-07/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00117, "Convexity of the expected error of volume-sampled column subsets", clopen.solutions.