$L^2$-Stability for STFT phase retrieval

TL;DR

This paper proves $L^2$-local stability for phase retrieval using the STFT with Gaussian windows and extends the result to Hermite windows via formalization in Lean 4.

Contribution

It establishes $L^2$-local stability for phase retrieval with Gaussian windows and formalizes an extension to Hermite windows in Lean 4.

Findings

Proves $L^2$-local stable phase retrieval for Gaussian window.

Extends the result to Hermite windows through formalization.

Demonstrates interplay between mathematicians and LLMs in proof development.

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.