{"id":"palomar/PALOMAR-2026-10-14-000002","url":"https://github.com/mario-ullrich/Lean-Discretization/tree/209d4bf72bec56fa7b181a24dacb8570b10a6986","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-14-000002-v1.json","repo":"https://github.com/mario-ullrich/Lean-Discretization","tags":["math.FA","cs.DS","msc:42C15","msc:15A45","msc:65F55","msc:05C50","spectral-sparsification","linear-algebra","lean"],"score":0,"title":"The sparsification theorem of Batson, Spielman and Srivastava","trust":"high","domain":"math.FA","source":"palomar","authors":["Mario Ullrich"],"reviews":0,"subject":"math.FA","summary":"Let (Ω, μ) be a measure space and a = (a_k) a family of m square-integrable functions whose Gram matrix ∫ a a* dμ is the identity. Then for every n ≥ m there are points x₁, …, xₙ ∈ Ω and weights w₁, …, wₙ > 0 with (1 − √((m−1)/n))² I ≼ ∑ᵢ wᵢ a(xᵢ) a(xᵢ)* ≼ (1 + √((m−1)/n))² I in the Loewner order. For the counting measure on a finite set Ω this is the theorem for finitely many vectors: if v_k ∈ ℂᵐ, k ∈ Ω, satisfy ∑_k v_k v_k* = I, then for every n ≥ m there are weights s_k ≥ 0, at most n of them nonzero, with (1 − √((m−1)/n))² I ≼ ∑_k s_k v_k v_k* ≼ (1 + √((m−1)/n))² I, so a reweighted…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-14","reactions":{},"formalized":true,"formalizes":[{"title":"Twice-Ramanujan sparsifiers","identifier":"arXiv:0808.0163","relationship":"formalizes"},{"title":"Constructive discretization and approximation in reproducing kernel Hilbert spaces","identifier":"arXiv:2602.18719","relationship":"formalizes"}]}