Fock空间中平方限制稳定相位检索的复分析证明
A complex-analytic proof of square-restricted stable phase retrieval in Fock space
浏览论文内容
中文总结 AI 辅助
该研究通过复分析方法，结合加权导数范数、分部积分等技术，在Lean中借助大语言模型完成验证，证明了一维Fock空间中高斯点处平方限制形式的局部稳定相位检索的强制性不等式。
中文摘要 AI 辅助
我们给出一维Fock空间中高斯点处平方限制形式的局部稳定相位检索的简短复分析证明。主要估计是映射 $F\mapsto F^2$ 的强制性不等式：$\\|F^2-F(0)^2\\|_{\mathcal{F}^2(\mathbb{C})} \lesssim \inf_{c\in\mathbb{R}}\\||F|^2-c\\|_{L^2(d\gamma)}$。证明使用加权导数范数、两次分部积分和加权柯西不等式，且已借助大语言模型在Lean中完成完全验证。
英文摘要
We give a short complex-analytic proof of a square-restricted form of local stable phase retrieval at the Gaussian in one-dimensional Fock space. The main estimate is a coercivity inequality for the map $F\mapsto F^2$: \[ \|F^2-F(0)^2|_{\mathcal{F}^2(\mathbb{C})} \lesssim \inf_{c\in\mathbb{R}}\||F|^2-c\|_{L^2(d γ)}. \] The proof uses a weighted derivative norm, two integrations by parts, and a weighted Cauchy inequality. The proof has been completely verified in Lean with the aid of Large Language Models.
