Subspace embeddings with the rerandomized SRHT
A Lean 4 formalization of a rerandomized SRHT subspace embedding theorem. For every ambient Walsh dimension n = 2^m, rank 1 <= r <= n, and 0 < epsilon < 1, one deterministic width k <= min(n, ceil(C r / epsilon^2)) can be chosen independently of the orthonormal frame. For each fixed frame, the transform with two independent uniform sign layers and an independent uniform k-subset has spectral failure probability at most 1/100, and preserves all squared norms in that subspace within 1 +/- epsilon with probability at least 99/100. C is an explicit universal constant, with no sharp numerical…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-07-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-07-000001/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-07-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'