Sensitivity-dependent row sampling for ℓₚ embeddings when p exceeds two
Fix $p > 2$. For a full-column-rank $A \in \mathbb{R}^{n \times d}$ with rows $a_1^{\mathsf T}, \dots, a_n^{\mathsf T}$, the $\ell_p$ sensitivities and the total sensitivity are $$s_i = \sup_{x \ne 0} \frac{|a_i^{\mathsf T}x|^p}{\|Ax\|_p^p}, \qquad \mathcal S = \sum_{i=1}^n s_i.$$ For $\alpha > 0$, sensitivity sampling keeps row $i$ independently with probability $q_i = \min\{1, 1/n + s_i/\alpha\}$ and scales each kept row by $q_i^{-1/p}$; let $\widetilde A$ be the resulting matrix, whose expected number of rows is $\sum_i q_i$. Woodruff and Yasuda proved that for some $\alpha$, with probability at least $1 - 1/\operatorname{poly}(n)$, $\widetilde A$ has at most $\varepsilon^{-2}\mathcal S^{2-2/p}\operatorname{polylog} n$ rows and satisfies the two-sided bound below for all $x$. For $1 \le p \le 2$, Munteanu and Omlor obtained $\widetilde O(\varepsilon^{-2}(\mathcal S + d))$ rows by sampling with the $\ell_p$ sensitivities augmented by $\ell_2$ sensitivities.
Problem. Are there constants $C_p, c_p > 0$ such that for every such $A$ and all $0 < \varepsilon, \delta < 1/2$ one can choose $\alpha$ with $$\sum_{i=1}^n q_i \le C_p\varepsilon^{-2}(\mathcal S + d)\log^{c_p}\!\left(\frac{2nd}{\varepsilon\delta}\right)$$ while, with probability at least $1 - \delta$, $$(1 - \varepsilon)\|Ax\|_p^p \le \|\widetilde Ax\|_p^p \le (1 + \varepsilon)\|Ax\|_p^p \qquad \text{for all } x \in \mathbb{R}^d?$$
Source: Woodruff and Yasuda (2023), §3, who conjecture that sensitivity sampling achieves Õ(ε⁻²(S + d)) samples for ℓp subspace embeddings; stated by OpenProblemsInNLA for p > 2, with the sampling probabilities of their Theorem 1.5, the expected number of rows, failure probability δ and a factor polylogarithmic in nd/(εδ).
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- PR
- Keywords
- OpenProblemsInNLA, row sampling, sensitivity sampling, subspace embeddings
- Literature checked
- Oct. 8, 2026 by clemens-admin
References
@inproceedings{woodruff2023,
author = {Woodruff, David P. and Yasuda, Taisuke},
title = {Sharper Bounds for $\ell_p$ Sensitivity Sampling},
booktitle = {Proceedings of the 40th International Conference on Machine Learning (ICML 2023)},
series = {Proc. Mach. Learn. Res.},
volume = {202},
publisher = {PMLR},
year = {2023},
pages = {37238--37272},
eprint = {2306.00732},
archivePrefix = {arXiv},
}
@inproceedings{munteanu2024,
author = {Munteanu, Alexander and Omlor, Simon},
title = {Optimal bounds for $\ell_p$ sensitivity sampling via $\ell_2$ augmentation},
booktitle = {Proceedings of the 41st International Conference on Machine Learning (ICML 2024)},
series = {Proc. Mach. Learn. Res.},
volume = {235},
publisher = {PMLR},
year = {2024},
pages = {36769--36796},
eprint = {2406.00328},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-ra06,
author = {Townsend, Alex},
title = {{RA-06}: Sensitivity-dependent row sampling for $\ell_p$ embeddings when p exceeds two},
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-06/README.md},
note = {Read at commit eb7c9d6, 2026-10-07},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00239.
namespace RegistryProblems.OP_00239
noncomputable section
open scoped BigOperators
/-- The exact real row action of a rectangular matrix. -/
def RowValue {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ)
(i : Fin n) (x : Fin d → ℝ) : ℝ :=
∑ j, A i j * x j
/-- The original full-column-rank promise, expressed as injectivity. -/
def FullColumnRank {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ) : Prop :=
∀ x : Fin d → ℝ, (∀ i, RowValue A i x = 0) → ∀ j, x j = 0
/-- The exact pth power of the ℓ_p norm of `A x`, for a real exponent. -/
noncomputable def InputEnergy {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ)
(p : ℝ) (x : Fin d → ℝ) : ℝ :=
∑ i, Real.rpow |RowValue A i x| p
/-- Ordinary row sensitivity. The denominator is positive for nonzero `x`
when the quantified matrix has full column rank. No augmented score occurs. -/
noncomputable def Sensitivity {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ)
(p : ℝ) (i : Fin n) : ℝ :=
sSup {y : ℝ | ∃ x : Fin d → ℝ,
(∃ j, x j ≠ 0) ∧
y = Real.rpow |RowValue A i x| p / InputEnergy A p x}
noncomputable def TotalSensitivity {n d : ℕ}
(A : Matrix (Fin n) (Fin d) ℝ) (p : ℝ) : ℝ :=
∑ i, Sensitivity A p i
/-- The exact floor and saturation rule from RA-06. -/
noncomputable def RetentionProbability {n d : ℕ}
(A : Matrix (Fin n) (Fin d) ℝ) (p α : ℝ) (i : Fin n) : ℝ :=
min 1 ((1 : ℝ) / (n : ℝ) + Sensitivity A p i / α)
/-- Probability of one Boolean retention vector under independent Bernoulli
draws with the prescribed possibly unequal probabilities. -/
noncomputable def OutcomeWeight {n d : ℕ}
(A : Matrix (Fin n) (Fin d) ℝ) (p α : ℝ)
(kept : Fin n → Bool) : ℝ :=
∏ i : Fin n,
if kept i = true then RetentionProbability A p α i
else 1 - RetentionProbability A p α i
/-- Exactly the ℓ_p norm power after retained row `i` is rescaled by
`q_i^(-1/p)`; for admissible inputs `q_i>0`, so its pth-power weight is `1/q_i`. -/
noncomputable def SampledEnergy {n d : ℕ}
(A : Matrix (Fin n) (Fin d) ℝ) (p α : ℝ)
(kept : Fin n → Bool) (x : Fin d → ℝ) : ℝ :=
∑ i : Fin n,
if kept i = true then
Real.rpow |RowValue A i x| p / RetentionProbability A p α i
else 0
/-- One sampled matrix preserves both norm-power bounds simultaneously for
every real test vector. -/
def Embedding {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ)
(p α ε : ℝ) (kept : Fin n → Bool) : Prop :=
∀ x : Fin d → ℝ,
(1 - ε) * InputEnergy A p x ≤ SampledEnergy A p α kept x ∧
SampledEnergy A p α kept x ≤ (1 + ε) * InputEnergy A p x
/-- Exact finite probability of the simultaneous all-vector event. -/
noncomputable def SuccessProbability {n d : ℕ}
(A : Matrix (Fin n) (Fin d) ℝ) (p α ε : ℝ) : ℝ := by
classical
exact ∑ kept : Fin n → Bool,
if Embedding A p α ε kept then OutcomeWeight A p α kept else 0
/-- The expected number of retained rows is the sum of the marginals. -/
noncomputable def ExpectedSize {n d : ℕ}
(A : Matrix (Fin n) (Fin d) ℝ) (p α : ℝ) : ℝ :=
∑ i, RetentionProbability A p α i
/-- One pair of constants depending only on the fixed real exponent `p`
must work for every full-rank matrix, both tolerances, and one shared `α`.
The logarithmic exponent is an arbitrary positive real constant. -/
def OriginalPositiveClaim (p : ℝ) : Prop :=
∃ C c : ℝ, 0 < C ∧ 0 < c ∧
∀ (n d : ℕ), 0 < n → 0 < d →
∀ A : Matrix (Fin n) (Fin d) ℝ, FullColumnRank A →
∀ ε δ : ℝ, 0 < ε → ε < 1 / 2 → 0 < δ → δ < 1 / 2 →
∃ α : ℝ, 0 < α ∧
ExpectedSize A p α ≤
C * Real.rpow ε (-2) * (TotalSensitivity A p + (d : ℝ)) *
Real.rpow (Real.log (2 * (n : ℝ) * (d : ℝ) / (ε * δ))) c ∧
1 - δ ≤ SuccessProbability A p α ε
/-- OP-00239: Sensitivity-dependent row sampling for ℓₚ embeddings when p exceeds two -/
def _root_.RegistryProblems.Problem_OP_00239 : Prop :=
∀ p : ℝ, 2 < p → OriginalPositiveClaim p
end
end RegistryProblems.OP_00239
Formalised by OpenAI Codex AI (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_00239 theorem resolution : RegistryProblems.Problem_OP_00239 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00239" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00239 := 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
A complete negative theorem for every real p>2, retaining the original independent Bernoulli sampling rule, expected-size budget, and simultaneous norm-power embedding assertion.
For every fixed real $p > 2$, the manuscript constructs full-column-rank matrices with total $\ell_p$ sensitivity $\mathcal S = \Theta_p(d)$ for which every nonnegative reweighted row subset preserving all $\|Ax\|_p^p$ within $1 \pm \varepsilon$ needs $\Omega_p((\mathcal S + d)\varepsilon^{-p})$ rows, in an explicit large-dimension regime. The matrices are grounded incidence matrices of complete graphs, all of whose rows have the …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-20 | Solution claimed → Lean verified | The registry's curators | RA-06: failure of the ordinary-sensitivity row-sampling guarantee v1 recorded from OpenProblemsInNLA @ 5487945, RA-06/lean/. |
| 2026-10-08 | Needs verification → Solution claimed | clemens-admin | Listed with the record of its solution, unreviewed. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00239, "Sensitivity-dependent row sampling for ℓₚ embeddings when p exceeds two", clopen.solutions.