贝塞尔序列的格罗滕迪克定理
Grothendieck's theorem for Bessel sequences
浏览论文内容
中文总结 AI 辅助
本文建立贝塞尔序列的精确格罗滕迪克定理，将其应用于肯定回答Olevskii的延拓问题，且附带Lean 4对主要结果的形式化验证。
中文摘要 AI 辅助
我们建立了贝塞尔序列的格罗滕迪克定理的一个精确版本。具体而言，给定希尔伯特空间中具有贝塞尔界1的贝塞尔序列$\boldsymbol{\{ x_j \}_{j\in\mathbb{N}}}$，我们证明存在属于$L^\infty([0,1])$单位球的函数$\boldsymbol{\{ f_j \}_{j\in\mathbb{N}}}$，使得对所有$j,k \in \mathbb{N}$，有$\boldsymbol{\langle x_j,x_k\rangle = \int_0^1 f_j(x)\overline{f_k(x)}\\,dx}$。作为应用，我们对Olevskii的一个延拓问题给出了肯定回答：若$E \subset [0,1]$是勒贝格可测集且$[0,1]\setminus E$具有正测度，则$L^2(E)$中每个具有贝塞尔界1的贝塞尔序列，都可延拓为$L^2([0,1])$中的正交系，且在$[0,1]\setminus E$上以最优常数$\boldsymbol{\lambda([0,1]\setminus E)^{-1/2}}$为界。本文附带了用Lean 4对主要结果的形式化验证。
英文摘要
We establish a sharp version of Grothendieck's theorem for Bessel sequences. Precisely, given a Bessel sequence $\{ x_j \}_{j\in\mathbb{N}}$ with Bessel bound $1$ in a Hilbert space, we show that there exists functions $\{ f_j \}_{j\in\mathbb{N}}$ belonging to the unit ball of $L^\infty([0,1])$ such that for all $j,k \in \mathbb{N}$ one has $$ \langle x_j,x_k\rangle = \int_0^1 f_j(x)\overline{f_k(x)}\,dx.$$ As an application, we give an affirmative answer to an extension problem of Olevskii: if $E \subset [0,1]$ is a Lebesgue measurable set such that $[0,1]\setminus E$ has positive measure, then every Bessel sequence in $L^2(E)$ with Bessel bound $1$ extends to an orthonormal system in $L^2([0,1])$ that is bounded by the (optimal) constant $λ([0,1]\setminus E)^{-1/2}$ on $[0,1]\setminus E$. A formalization of our main result in Lean 4 accompanies the paper.
