Polynomial trace-error factor after exactly the target rank of pivots
Let $A \in \mathbb{C}^{n \times n}$ be Hermitian positive semidefinite, with eigenvalues $\lambda_1(A) \ge \cdots \ge \lambda_n(A) \ge 0$, and let $\tau_r(A) = \sum_{j > r} \lambda_j(A)$. Randomly pivoted Cholesky (RPCholesky), in exact arithmetic, produces residuals $R_0 = A, R_1, R_2, \dots$: given $R_t \ne 0$, it picks an index $j$ with probability $(R_t)_{jj}/\operatorname{tr}(R_t)$ and sets $$R_{t+1} = R_t - \frac{R_t(:,j)\,R_t(j,:)}{(R_t)_{jj}},$$ and once a residual is zero all later ones are zero. Chen, Epperly, Tropp and Webber proved $\mathbb{E}\operatorname{tr}(R_r) \le 2^r \tau_r(A)$.
Problem. Are there constants $C > 0$ and $p \ge 0$ such that $$\mathbb{E}\operatorname{tr}(R_r) \le C r^p \tau_r(A)$$ for every $n \ge 1$, every Hermitian positive semidefinite $A \in \mathbb{C}^{n \times n}$ and every integer $1 \le r \le n$?
Source: Epperly (2025), PhD thesis, Conjecture 11.2.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- PR
- Keywords
- low-rank approximations, OpenProblemsInNLA, pivoted Cholesky factorizations
References
@phdthesis{epperly2025,
author = {Epperly, Ethan N.},
title = {Make the Most of What You Have: Resource-Efficient Randomized Algorithms for Matrix Computations},
school = {California Institute of Technology},
year = {2025},
doi = {10.7907/pef3-mg80},
}
@article{chen2025,
author = {Chen, Yifan and Epperly, Ethan N. and Tropp, Joel A. and Webber, Robert J.},
title = {Randomly pivoted {C}holesky: Practical approximation of a kernel matrix with few entry evaluations},
journal = {Comm. Pure Appl. Math.},
volume = {78},
number = {5},
year = {2025},
pages = {995--1041},
doi = {10.1002/cpa.22234},
eprint = {2207.06503},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-ra02,
author = {Townsend, Alex},
title = {{RA-02}: Polynomial trace-error factor after exactly the target rank of pivots},
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-02/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00115.
namespace RegistryProblems.OP_00115
noncomputable section
open scoped BigOperators ComplexOrder Matrix
abbrev Square (n : ℕ) := Matrix (Fin n) (Fin n) ℂ
abbrev History (n k : ℕ) := Fin k → Fin n
def realTrace {n : ℕ} (A : Square n) : ℝ := A.trace.re
/-- Zero-diagonal choices are harmless totalization. Their probability is zero
for a nonzero PSD residual. The nonzero case is the original complex update. -/
def choleskyStep {n : ℕ} (A : Square n) (j : Fin n) : Square n :=
if A j j = 0 then A else fun a b => A a b - A a j * A j b / A j j
/-- On a zero PSD residual use uniform dummy labels; all residuals stay zero.
The n=0 value is only totalization: normalization is asserted for n>=1. -/
def pivotMass {n : ℕ} (A : Square n) (j : Fin n) : ℝ :=
if realTrace A = 0 then 1 / (n : ℝ) else (A j j).re / realTrace A
/-- Chronological residual, including all zero-probability paths. -/
def pathResidual {n : ℕ} (A : Square n) : List (Fin n) → Square n
| [] => A
| j :: w => pathResidual (choleskyStep A j) w
/-- Product of actual conditional masses; no independence assumption. -/
def pathWeight {n : ℕ} (A : Square n) : List (Fin n) → ℝ
| [] => 1
| j :: w => pivotMass A j * pathWeight (choleskyStep A j) w
def pathContribution {n : ℕ} (A : Square n) (w : List (Fin n)) : ℝ :=
pathWeight A w * realTrace (pathResidual A w)
/-- Full finite expectation. Every ordered label sequence is included. -/
def expectedTrace {n : ℕ} (A : Square n) (k : ℕ) : ℝ :=
∑ f : History n k, pathContribution A (List.ofFn f)
/-- Mathlib's genuinely decreasing eigenvalues. The finite-index transport
uses only card(Fin n)=n; the separately reindexed eigenvalues is not used. -/
def orderedEigenvalues {n : ℕ} (A : Square n) (hA : A.IsHermitian) : Fin n → ℝ :=
fun i => hA.eigenvalues₀ (Fin.cast (Fintype.card_fin n).symm i)
/-- Zero-based i>=r is the original one-based j>r tail. -/
def rankTail {n : ℕ} (A : Square n) (hA : A.IsHermitian) (r : ℕ) : ℝ :=
∑ i ∈ (Finset.univ.filter fun i : Fin n => r ≤ i.val), orderedEigenvalues A hA i
/-- OP-00115: Polynomial trace-error factor after exactly the target rank of pivots -/
def _root_.RegistryProblems.Problem_OP_00115 : Prop :=
∃ C : ℝ, 0 < C ∧ ∃ p : ℝ, 0 ≤ p ∧
∀ n : ℕ, 1 ≤ n → ∀ A : Square n, ∀ hA : A.PosSemidef,
∀ r : ℕ, 1 ≤ r → r ≤ n →
expectedTrace A r ≤ C * Real.rpow (r : ℝ) p * rankTail A hA.isHermitian r
end
end RegistryProblems.OP_00115
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_00115 theorem resolution : RegistryProblems.Problem_OP_00115 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00115" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00115 := 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
Complete negative answer to the original RPCholesky polynomial trace-factor question. For every real C>0 and p>=0, a complex positive-definite matrix of order r+1 strictly violates the proposed bound after exactly r pivots. All normalized process and genuine ordered eigenvalue-tail semantics are proved.
For every positive integer $r$, an explicit one-parameter family of real, entrywise-positive, positive-definite matrices of order $r+1$ makes the expected trace error of $r$ randomly pivoted Cholesky steps approach $2^r$ times the optimal rank-$r$ trace error. The same family makes the expected squared Frobenius error of $r$ randomly pivoted LU steps approach $4^r$ times the optimal rank-$r$ squared Frobenius error. …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, RA-02/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00115, "Polynomial trace-error factor after exactly the target rank of pivots", clopen.solutions.