Exponential smoothed tail bounds for partial pivoting
For a nonsingular $A \in \mathbb{R}^{n \times n}$ let $\rho_{\mathrm{PP}}(A)$ be the growth factor of Gaussian elimination with partial pivoting in exact arithmetic: the largest entry modulus of the successive active Schur complements $S_1 = A, S_2, \dots, S_n$, divided by the largest entry modulus of $A$. Let $G \in \mathbb{R}^{n \times n}$ have independent standard normal entries. For every $\bar A$ and $\sigma > 0$, the matrix $\bar A + \sigma G$ is almost surely nonsingular, with no ties in the choice of pivots. Huang and Tikhomirov showed that for $\bar A = 0$ and $\sigma = 1$ the growth factor is at most polynomial in $n$ with probability close to one.
Problem. Are there constants $c_1, c_2 > 0$ such that $$\Pr\bigl\{\rho_{\mathrm{PP}}(\bar A + \sigma G) > x\,(n/\sigma)^{c_1}\bigr\} \le 2^{-c_2 x}$$ for every $n \ge 1$, every $\bar A \in \mathbb{R}^{n \times n}$ with $\|\bar A\|_2 \le 1$, every $0 < \sigma \le 1$ and every $x \ge 1$?
Source: Spielman and Teng (2006), Conjecture 16; in another form (‖U‖max/‖A‖max, absolute constants, σ ≤ 1), Sankar, Spielman and Teng (2006), Conjecture 3. Constants independent of n, Ā, σ and x, with x ≥ 1, as stated by OpenProblemsInNLA.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- PR
- Keywords
- Gaussian elimination, growth factors, OpenProblemsInNLA, smoothed analysis
References
@incollection{spielman2006,
author = {Spielman, Daniel A. and Teng, Shang-Hua},
title = {Smoothed analysis of algorithms and heuristics: progress and open questions},
booktitle = {Foundations of Computational Mathematics, Santander 2005},
editor = {Pardo, Luis M. and Pinkus, Allan and S{\"u}li, Endre and Todd, Michael J.},
series = {London Math. Soc. Lecture Note Ser.},
volume = {331},
publisher = {Cambridge University Press},
address = {Cambridge},
year = {2006},
pages = {274--342},
doi = {10.1017/CBO9780511721571.010},
}
@article{sankar2006,
author = {Sankar, Arvind and Spielman, Daniel A. and Teng, Shang-Hua},
title = {Smoothed analysis of the condition numbers and growth factors of matrices},
journal = {SIAM J. Matrix Anal. Appl.},
volume = {28},
number = {2},
year = {2006},
pages = {446--476},
doi = {10.1137/S0895479803436202},
eprint = {cs/0310022},
archivePrefix = {arXiv},
}
@article{huang2024,
author = {Huang, Han and Tikhomirov, Konstantin},
title = {Average-case analysis of the {G}aussian elimination with partial pivoting},
journal = {Probab. Theory Related Fields},
volume = {189},
number = {1-2},
year = {2024},
pages = {501--567},
doi = {10.1007/s00440-024-01276-2},
eprint = {2206.01726},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-ie04,
author = {Townsend, Alex},
title = {{IE-04}: Exponential smoothed tail bounds for partial pivoting},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/linear-systems-and-elimination/IE-04/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00078.
namespace RegistryProblems.OP_00078
noncomputable section
open scoped BigOperators NNReal Matrix.Norms.L2Operator
open MeasureTheory ProbabilityTheory
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℝ
abbrev PivotPath (n : ℕ) := Fin n → Fin n
/-- The standard nested product measurable space on the actual n² real entries.
Matrix is a type synonym for the double function space; making this instance
explicit does not change its measurable sets or the Gaussian product law. -/
instance measurableSpaceMat (n : ℕ) : MeasurableSpace (Mat n) :=
(inferInstance : MeasurableSpace (Fin n → Fin n → ℝ))
/-- The actual induced Euclidean matrix norm, fixed by L2Operator scope. -/
def spectralNorm {n : ℕ} (A : Mat n) : ℝ := ‖A‖
/-- Swap current row positions; partial pivoting never exchanges columns. -/
def rowSwap {n : ℕ} (S : Mat n) (k p : Fin n) : Mat n :=
fun i j => S (Equiv.swap k p i) j
/-- Actual Schur update, padded with zero outside the new active block.
Lean's total division is used only to make this a total function; admissible
paths separately require nonzero pivots. -/
def schurStep {n : ℕ} (S : Mat n) (k p : Fin n) : Mat n :=
let B := rowSwap S k p
fun i j => if k < i ∧ k < j then
B i j - (B i k / B k k) * B k j else 0
def trajectory {n : ℕ} (A : Mat n) (path : PivotPath n) : ℕ → Mat n
| 0 => A
| k + 1 => if h : k < n then
schurStep (trajectory A path k) ⟨k, h⟩ (path ⟨k, h⟩) else 0
def AdmissiblePivot {n : ℕ} (S : Mat n) (k p : Fin n) : Prop :=
k ≤ p ∧ S p k ≠ 0 ∧ ∀ i, k ≤ i → |S i k| ≤ |S p k|
def AdmissiblePath {n : ℕ} (A : Mat n) (path : PivotPath n) : Prop :=
∀ k, AdmissiblePivot (trajectory A path k.val) k (path k)
/-- The true maximum of absolute input entries, as a finite NNReal supremum. -/
def entryMaxNN {n : ℕ} (A : Mat n) : ℝ≥0 :=
Finset.univ.sup (fun ij : Fin n × Fin n => ‖A ij.1 ij.2‖₊)
def entryMax {n : ℕ} (A : Mat n) : ℝ := entryMaxNN A
def activeMaxNN {n : ℕ} (S : Mat n) (k : ℕ) : ℝ≥0 :=
Finset.univ.sup (fun ij : Fin n × Fin n =>
if k ≤ ij.1.val ∧ k ≤ ij.2.val then ‖S ij.1 ij.2‖₊ else 0)
/-- The exact n active stages are counted, divided by the original entry max. -/
def growth {n : ℕ} (A : Mat n) (path : PivotPath n) : ℝ :=
((Finset.univ.sup (fun k : Fin n =>
activeMaxNN (trajectory A path k.val) k.val) : ℝ≥0) : ℝ) / entryMax A
/-- A deterministic measurable GEPP tie rule, valid on every nonsingular input.
The frozen Challenge separately proves that firstPath supplies such a rule;
the quantified class cannot silently be empty. -/
def AdmissibleRule {n : ℕ} (rule : Mat n → PivotPath n) : Prop :=
(∀ A, A.det ≠ 0 → AdmissiblePath A (rule A)) ∧
Measurable (fun A => growth A (rule A))
/-- n² mutually independent standard real Gaussians, specified by their actual
finite product measure, not by a premise about unspecified random variables. -/
def gaussianMatrix (n : ℕ) : Measure (Mat n) :=
Measure.pi (fun _ : Fin n => Measure.pi (fun _ : Fin n => gaussianReal 0 1))
def smoothedInput {n : ℕ} (center : Mat n) (σ : ℝ) (G : Mat n) : Mat n :=
center + σ • G
/-- An actual algorithmic tail event on the nonsingular input domain.
Its measurability is a separate exported obligation. Intersecting with this
domain only decreases any total-extension tail event, so a violation here also
violates any such extension without requiring a singular-set nullity premise. -/
def exceedanceEvent {n : ℕ} (center : Mat n) (σ threshold : ℝ)
(rule : Mat n → PivotPath n) : Set (Mat n) :=
{G | let A := smoothedInput center σ G
A.det ≠ 0 ∧ threshold < growth A (rule A)}
/-- OP-00078: Exponential smoothed tail bounds for partial pivoting -/
def _root_.RegistryProblems.Problem_OP_00078 : Prop :=
∃ c₁ c₂ : ℝ, 0 < c₁ ∧ 0 < c₂ ∧
∀ n : ℕ, 1 ≤ n → ∀ center : Mat n, spectralNorm center ≤ 1 →
∀ σ : ℝ, 0 < σ → σ ≤ 1 → ∀ x : ℝ, 1 ≤ x →
∀ rule : Mat n → PivotPath n, AdmissibleRule rule →
gaussianMatrix n (exceedanceEvent center σ
(x * ((n : ℝ) / σ) ^ c₁) rule) ≤
ENNReal.ofReal ((2 : ℝ) ^ (-c₂ * x))
end
end RegistryProblems.OP_00078
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_00078 theorem resolution : RegistryProblems.Problem_OP_00078 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00078" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00078 := 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 formally checked negative resolution of the uniform exponential Gaussian-smoothed GEPP tail, with all 21 frozen obligations, genuine product Gaussian measures, the full nonsingular perturbation box and arbitrary positive real proposed constants.
For every $n\ge2$ and $C\in\{0,I_n\}$, a matrix $G$ with independent standard normal entries satisfies $\Pr\{\rho_{\rm PP}(C+G)>\tfrac12(3/2)^{n-1}\}\ge2^{-n^2(n^2+n+5)}$, where $\rho_{\rm PP}$ is the growth factor of Gaussian elimination with partial pivoting in exact arithmetic. Consequently no positive constants $c_1,c_2$ give $\Pr\{\rho_{\rm PP}(\bar A+\sigma G)>x(n/\sigma)^{c_1}\}\le2^{-c_2x}$ for all $n$, all $\|\bar A\|_2\le1$, $0<\sigma\le1$ and $x\ge1$; the center $\bar A=I_n$ with $\sigma=1$ already violates it. …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, IE-04/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00078, "Exponential smoothed tail bounds for partial pivoting", clopen.solutions.