$L^2$-Stability for STFT phase retrieval
泛函分析
2026-05-21 v1 经典分析与常微分方程
摘要
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.
引用
@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}
}
备注
24 pages, accpmpaining Lean source code in https://github.com/susannabertolini/PhaseRetrieval