$L^2$-Stability for STFT phase retrieval
Functional Analysis
2026-05-21 v1 Classical Analysis and ODEs
Abstract
We prove that the short-time Fourier transform with Gaussian window performs -local stable phase retrieval at the constant function. The proof involved significant interplay between mathematicians and LLMs. An autoformalization in Lean 4 of an extension of our result to -local stable phase retrieval for all Hermite windows and all elements in the finite span of the canonical basis vectors is also presented.
Cite
@article{arxiv.2605.20527,
title = {$L^2$-Stability for STFT phase retrieval},
author = {Susanna Bertolini and Jaume de Dios Pont and Ben Pineau and Mitchell A. Taylor and João P. G. Ramos},
journal= {arXiv preprint arXiv:2605.20527},
year = {2026}
}
Comments
24 pages, accpmpaining Lean source code in https://github.com/susannabertolini/PhaseRetrieval