{"id":"palomar/PALOMAR-2026-09-09-000003","url":"https://github.com/DiarHaidary/Rerandomized-Subsampled-Trigonometric-Transforms/tree/929653a019eb4910fc6efb9cb34cc3c3c2f949d4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-09-000003-v1.json","repo":"https://github.com/DiarHaidary/Rerandomized-Subsampled-Trigonometric-Transforms","tags":["math.NA","cs.DS","msc:60B20","msc:68W20","randomized-linear-algebra","dimensionality-reduction","lean","probability"],"score":0,"title":"Rerandomized Subsampled Trigonometric Transforms","trust":"high","domain":"math.NA","source":"palomar","authors":["Diar Heidary"],"reviews":0,"subject":"math.NA","summary":"A Lean formalization of a two-round real Walsh subsampled randomized Hadamard embedding. For every fixed d-dimensional real subspace of a Walsh space of dimension n, independent unbiased diagonal signs and a uniform sample of M distinct rows preserve every squared Euclidean norm within factors 1-epsilon and 1+epsilon with probability at least 1-delta. The prescribed M is at most n and at most [8192(1+432/delta)+1]d/epsilon^2. Thus, at any fixed failure probability, the embedding dimension is O(d/epsilon^2), the scaling asked for in Problem 5.6 of arXiv:2602.05394v3 for its Walsh model. The…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-09","reactions":{},"formalized":true,"formalizes":[{"title":"Two-round Walsh SRHT: a self-contained moment and embedding proof","identifier":"","relationship":"formalizes"}]}