$L^2$-Stability for STFT phase retrieval

Abstract

We prove that the short-time Fourier transform with Gaussian window performs $L^2$-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 $L^2$-local stable phase retrieval for all Hermite windows and all elements in the finite span of the canonical basis vectors is also presented.

24 pages, accpmpaining Lean source code in https://github.com/susannabertolini/PhaseRetrieval