Improve the randomized LU squared-error factor to 2^k
Randomly pivoted LU, applied in exact arithmetic to $A \in \mathbb{C}^{m \times n}$, produces residuals $S_0 = A, S_1, S_2, \dots$: given $S_t \ne 0$, it picks a pivot $(i, j)$ with probability $|(S_t)_{ij}|^2/\|S_t\|_F^2$ and sets $$S_{t+1} = S_t - \frac{S_t(:,j)\,S_t(i,:)}{(S_t)_{ij}},$$ and once a residual is zero all later ones are zero. Let $\sigma_1(A) \ge \sigma_2(A) \ge \cdots$ be the singular values of $A$. Gilles and Wilber proved $\mathbb{E}\|S_k\|_F^2 \le 4^k \sum_{j > k} \sigma_j(A)^2$.
Problem. Is $$\mathbb{E}\|S_k\|_F^2 \le 2^k \sum_{j > k} \sigma_j(A)^2$$ for every $m, n \ge 1$, every $A \in \mathbb{C}^{m \times n}$ and every $1 \le k \le \min(m, n)$?
Source: Gilles and Wilber (2026), the conjecture following their Theorem 3.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- PR
- Keywords
- low-rank approximations, OpenProblemsInNLA, pivoted LU factorizations
References
@misc{gilles2026,
author = {Gilles, Marc Aur{\`e}le and Wilber, Heather},
title = {Low-Rank Approximation by Randomly Pivoted {LU}},
year = {2026},
eprint = {2601.22344},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-ra03,
author = {Townsend, Alex},
title = {{RA-03}: Improve the randomized LU squared-error factor to $2^k$},
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-03/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00116.
namespace RegistryProblems.OP_00116
noncomputable section
open scoped BigOperators Classical
/-- The squared Frobenius norm, written as the exact sum of squared complex moduli. -/
def frobeniusSq {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℂ) : ℝ :=
∑ i, ∑ j, Complex.normSq (A i j)
/-- `none` is the absorbing label used only after the residual is zero.
Each `some (i,j)` selects a row and a column together. -/
abbrev Pivot (m n : ℕ) := Option (Fin m × Fin n)
/-- The exact conditional pivot probabilities. The zero residual assigns
probability one to `none`; otherwise only entry labels have nonzero mass. -/
def pivotMass {m n : ℕ} (S : Matrix (Fin m) (Fin n) ℂ) : Pivot m n → ℝ
| none => if S = 0 then 1 else 0
| some ij => if S = 0 then 0 else Complex.normSq (S ij.1 ij.2) / frobeniusSq S
/-- The canonical rank-one cross update. A zero entry is given an identity
update solely to totalize the function; its selection probability is zero. -/
def pivotResidual {m n : ℕ} (S : Matrix (Fin m) (Fin n) ℂ)
(ij : Fin m × Fin n) : Matrix (Fin m) (Fin n) ℂ :=
if S ij.1 ij.2 = 0 then S
else fun a b => S a b - S a ij.2 * S ij.1 b / S ij.1 ij.2
/-- The next residual for a transition label. The `none` transition has
positive mass exactly at the zero matrix, where it keeps the residual zero. -/
def nextResidual {m n : ℕ} (S : Matrix (Fin m) (Fin n) ℂ) :
Pivot m n → Matrix (Fin m) (Fin n) ℂ
| none => 0
| some ij => pivotResidual S ij
/-- The terminal residual along an ordered history of `k` transitions. -/
def historyResidual {m n : ℕ} (S : Matrix (Fin m) (Fin n) ℂ) :
{k : ℕ} → (Fin k → Pivot m n) → Matrix (Fin m) (Fin n) ℂ
| 0, _ => S
| k + 1, h => historyResidual (nextResidual S (h 0)) (fun i : Fin k => h i.succ)
/-- The joint probability of a history is the product of the conditional
probabilities along its actual residuals. No independence of row and column
choices, or of successive pivot choices, is assumed. -/
def historyMass {m n : ℕ} (S : Matrix (Fin m) (Fin n) ℂ) :
{k : ℕ} → (Fin k → Pivot m n) → ℝ
| 0, _ => 1
| k + 1, h => pivotMass S (h 0) *
historyMass (nextResidual S (h 0)) (fun i : Fin k => h i.succ)
/-- The actual finite expectation after exactly `k` transitions. Absorption
implements the canonical instruction to keep all later residuals zero. -/
def expectedError {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℂ) (k : ℕ) : ℝ :=
∑ h : Fin k → Pivot m n, historyMass A h * frobeniusSq (historyResidual A h)
/-- The decreasing singular values of the matrix acting on complex Euclidean
spaces, using mathlib's zero-based sequence with its actual spectral definition. -/
def singularValue {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℂ) (j : ℕ) : ℝ :=
(Matrix.toEuclideanLin A).singularValues j
/-- The canonical squared singular-value tail after rank `k`.
Paper indices `j > k` become zero-based indices in `[k, min m n)`. -/
def singularTailSq {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℂ) (k : ℕ) : ℝ :=
∑ j ∈ Finset.Ico k (min m n), singularValue A j ^ 2
/-- OP-00116: Improve the randomized LU squared-error factor to 2^k -/
def _root_.RegistryProblems.Problem_OP_00116 : Prop :=
∀ m n : ℕ, 1 ≤ m → 1 ≤ n → ∀ A : Matrix (Fin m) (Fin n) ℂ,
∀ k : ℕ, 1 ≤ k → k ≤ min m n →
expectedError A k ≤ (2 : ℝ) ^ k * singularTailSq A k
end
end RegistryProblems.OP_00116
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_00116 theorem resolution : RegistryProblems.Problem_OP_00116 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00116" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00116 := 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 genuine finite randomized LU process and its normalized history law, derives the actual singular-value tail and expected squared Frobenius error at an exact matrix witness, and refutes the full original universal bound.
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-03/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00116, "Improve the randomized LU squared-error factor to 2^k", clopen.solutions.