结果族 325：The complete Crouzeix conjecture · 学科：Functional analysis · 验证状态：主结果已 Lean 形式化
把矩阵多项式想成一个”代入机器”：把数字 z 换成矩阵 A，输出的”大小”能不能事先圈住？数值域 W(A) 是复平面上圈出的一块凸地盘，Crouzeix 猜想说：代入后的范数不超过多项式在这块地盘上最大值的 2 倍，而且 2 不能再小。本文对所有矩阵、所有矩阵系数多项式直接证明了它。
关键词卡片
@@M@@u^*Au@@（u 取单位向量）在复平面上扫出的紧凸集，总包含特征值。@@M@@\|P[A]\|\le 2\cdot\max_{z\in W(A)}\|P(z)\|@@。看个具体例子
论文用来说明常数 2 不可改进的最小例子：@@M@@2\times 2@@ 幂零矩阵配上一次多项式。
@@M@@A=\begin{pmatrix}0&2\\0&0\end{pmatrix},\ P(z)=z:\qquad W(A)=\{z:\lvert z\rvert\le 1\},\qquad \|P[A]\|=\|A\|=2=2\cdot\max_{z\in W(A)}\lvert z\rvert.@@
注意特征值只有 0——若用地盘只圈特征值的谱估计，界会是 0，毫无用处；数值域这块更大的地盘恰好圈住全部非正规性，常数 2 被精确吃到。
为什么值得关心
2007 年以来最好的一般常数是 @@M@@1+\sqrt2\approx 2.414@@，本文推进到理论极限 2，完整版 Crouzeix 猜想收官。
已 Lean 形式化
第一级台阶
导读把矩阵多项式比作”代入机器”、数值域比作”圈出的凸地盘”。换成半数学的话：研究对象是把矩阵代入多项式后得到的输出；控制集是数值域——由矩阵扫出的那块紧凸地盘；问题问：输出的”大小”能否被多项式在地盘上的最大值乘一个普适常数圈住，以及这个常数最小是多少。导读的例子提醒：只用特征值圈不住非正规矩阵（幂零矩阵特征值全零、范数可达 2），数值域恰好补上非正规性信息。
第二级台阶
用本科术语精确化。矩阵 @@M@@A@@ 的数值域是 @@M@@W(A)=\{u^*Au:u^*u=1\}@@，由 Toeplitz–Hausdorff 定理它是含谱的紧凸集。矩阵系数多项式 @@M@@P(z)=\sum_k B_kz^k@@（@@M@@B_k@@ 是不必交换的矩阵）在 @@M@@A@@ 处的取值定义为 @@M@@P[A]=\sum_k A^k\otimes B_k@@；范数取算子范数。所谓”完整”（complete）指不等式对系数维数一致成立——这恰是 @@M@@W(A)@@ 构成完全 @@M@@2@@-谱集的断言，比标量版本强得多。
第三级台阶
定理的语境是：基维数 @@M@@n@@、系数维数 @@M@@m@@、次数 @@M@@d@@ 三者任意且互相独立——此前标量证明的交换性论证经不起矩阵放大（系数矩阵不必交换），而 @@M@@2\times2@@ 基矩阵、基维数至多 @@M@@3@@ 等完整结果都带维数限制，一般完整常数停在 @@M@@1+\sqrt2@@。主定理断言：对上述一切 @@M@@A@@ 与 @@M@@P@@，@@M@@\|P[A]\|\le2\max_{z\in W(A)}\|P(z)\|@@；数值域退化为点或线段的矩阵同样覆盖。常数 2 最优：@@M@@A=\begin{pmatrix}0&2\\0&0\end{pmatrix}@@ 配 @@M@@P(z)=z@@ 时数值域是单位圆盘、@@M@@\|A\|=2@@，恰好取等。
本文直接证明：对任意复方阵 @@M@@A@@ 与任意矩阵系数多项式 @@M@@P@@，恒有 @@M@@\|P[A]\|\le 2\max_{z\in W(A)}\|P(z)\|@@，其中 @@M@@W(A)@@ 为数值域；常数 2 达到最优，且与基维数、系数维数、次数全部无关——完整版 Crouzeix 猜想的矩阵形式就此解决。
矩阵的数值域（numerical range）@@M@@W(A)=\{u^*Au:\ u^*u=1\}@@ 是由 Toeplitz–Hausdorff 定理刻画的紧凸集，总包含谱。正规矩阵靠谱定理就能控制多项式取值，非正规矩阵却不行：非零幂零矩阵的谱是 @@M@@\{0\}@@，范数却可达 2。数值域保留了足够的非正规性信息，因而成为给出普适界的自然控制集。Crouzeix 于 2004 年提出以 @@M@@W(A)@@ 为控制集、常数取 2 的猜想，2007 年先证得普适界 11.08；Delyon–Delyon 的正边界表示与 Crouzeix–Palencia 的正双层位势（double-layer potential）方法把完整界推进到 @@M@@1+\sqrt2@@，Badea–Crouzeix–Delyon 又对 @@M@@2\times 2@@ 基矩阵得到完整的常数 2。2026 年 Jin、Lorist–Schwenninger、Luo 相继给出标量证明，Åhag–Czyż–Virtanen 证明了基维数至多 3 的完整情形。长期卡点在于：标量证明里的交换性论证经不起矩阵系数的放大（amplification），因为系数矩阵不必交换。
定理 1.1：对任意正整数 @@M@@n,m@@、任意 @@M@@A\in M_n(\mathbb C)@@、任意次数 @@M@@d@@ 及任意 @@M@@P(z)=\sum_{k=0}^d B_kz^k@@（@@M@@B_k\in M_m(\mathbb C)@@），记 @@M@@P[A]=\sum_{k=0}^d A^k\otimes B_k@@，则 @@M@@\|P[A]\|\le 2\max_{z\in W(A)}\|P(z)\|@@。常数 2 在所有 @@M@@n,m,d@@ 上不能一致改进；数值域退化为点或线段的矩阵同样被覆盖。”完整”（complete）指该界对系数维数 @@M@@m@@ 一致成立——这恰是 @@M@@W(A)@@ 构成完全 2-谱集（complete 2-spectral set）的断言，比标量版本强得多。
先把 @@M@@W(A)@@ 严格放入一个边界为正则实解析 Jordan 曲线的有界凸域 @@M@@\Omega@@，用外部共形映射（exterior conformal map）@@M@@h@@ 将 @@M@@\partial\Omega@@ 参数化为单位圆，并把 Cauchy 核在无穷远处展开，得到 Faber 多项式（Faber polynomials）@@M@@b_k@@。第一步建立系数定理：边界值 @@M@@b_k\circ h@@ 等于 @@M@@\mu^k@@ 加上纯负频率修正，混合系数恰为微分化的 Grunsky 系数（Grunsky coefficients）；由它们合成的核 @@M@@K=1+s+\bar s@@ 非负，且对每个变量的圆周积分均为 1。这两条边缘恒等式使”正频率到负频率”的映射成为 @@M@@L^2@@ 压缩，从而夹住系数范数：@@M@@\sum_k\|C_k\|_{HS}^2\le\int_{\mathbb T}\|G\circ h\|_{HS}^2\,d\tau\le\|C_0\|_{HS}^2+2\sum_{k\ge1}\|C_k\|_{HS}^2@@。这一不等式把”边界上函数有多大”翻译成”系数有多大”，非零次系数所带的权重 2 正是最终常数 2 的来源。
随后对目标多项式 @@M@@F@@（设边界算子范数至多 1）取 @@M@@F[A]@@ 的一对单位顶部奇异向量（top singular vectors）@@M@@x,y@@，用预解式（resolvent）@@M@@R(\lambda)=\lambda h'(\lambda)(h(\lambda)I-A)^{-1}=\sum_k b_k(A)\lambda^{-k}@@ 生成系数泛函；数值域条件经支撑半平面不等式导出 @@M@@R+R^*\succeq 0@@，即 Delyon–Delyon 与 Crouzeix–Palencia 一脉相承的正双层位势。本文的关键新招是保序检验：既然系数矩阵不必交换，就把检验多项式 @@M@@G@@ 分别放在 @@M@@F@@ 的左侧与右侧，得 @@M@@y^*(FG)[A]x=\gamma\,x^*G[A]x@@ 与 @@M@@y^*(GF)[A]x=\gamma\,y^*G[A]y@@，两条链各自使用相应乘法顺序的 Hilbert–Schmidt 乘法界；再对偶地选取检验系数，得到两个对角泛函的加权范数上界，其权重与对角压缩场的 Fourier 平方范数恰好互为倒数配对。最后把 @@M@@R+R^*@@ 压缩成 @@M@@2\times 2@@ 正块 @@M@@\Delta\succeq 0@@，正性蕴含交叉场范数受对角场控制，与 Parseval 计算合并得 @@M@@2a^2\le 8a^2/\gamma^2@@，即 @@M@@\gamma\le 2@@。收尾时用指数型支撑函数构造的解析凸邻域序列收缩到任意紧凸数值域，并附 Toeplitz–Hausdorff 凸性的简短证明；@@M@@A=\begin{pmatrix}0&2\\0&0\end{pmatrix}@@ 与 @@M@@P(z)=z@@ 表明常数 2 不可再小。
本文主结果已 Lean 形式化。同族姊妹篇《The complete Crouzeix theorem》以”最优相似＋公共正边界表示”的结构路线另证同一不等式：两文共享外部核与预解式正性这套解析内核，但证明路径各自独立完整，互为印证。按 OpenAI 官方声明，未经形式化的结果可能存在问题；本文主结果已通过形式化验证，可信度相应更高。
问 1：证明里最关键的一步是什么？
（答：保序双检验加权重配对。取 @@M@@F[A]@@ 的单位顶部奇异向量对 @@M@@x,y@@，把检验多项式 @@M@@G@@ 分别放在 @@M@@F@@ 的左、右两侧得 @@M@@y^*(FG)[A]x=\gamma x^*G[A]x@@ 与 @@M@@y^*(GF)[A]x=\gamma y^*G[A]y@@，两条链各用相应乘法顺序的 Hilbert–Schmidt 界；对偶选取检验系数后，两个对角泛函的加权平方范数（常数项权 1、其余权 @@M@@1/2@@）恰与对角压缩场的 Fourier 平方范数倒数配对，再用 @@M@@R+R^*\succeq0@@ 压成的 @@M@@2\times2@@ 正块比较交叉场与对角场，得 @@M@@2a^2\le8a^2/\gamma^2@@ 即 @@M@@\gamma\le2@@。）
问 2：这一步哪里最脆？
（答：配对的源头——定理 lem:faber 的系数机制：核 @@M@@K=1+s+\bar s@@（@@M@@s@@ 为微分化 Grunsky 系数）非负、且对每个变量圆周积分为 1，由此”正频到负频”才是 @@M@@L^2@@ 压缩、命题 prop:coefficients 的双侧夹 @@M@@\sum\|C_k\|_{HS}^2\le\int\|G\circ h\|_{HS}^2\le\|C_0\|_{HS}^2+2\sum_{k\ge1}\|C_k\|_{HS}^2@@ 才成立。非零次系数的权重 2 正是最终常数 2 的来源；支撑半平面不等式给的非负性若在某退化边界失效，全链断裂。）
问 3：为什么标量证明不能自动升级，维数假设为什么省不掉？
（答：放大后系数矩阵不必交换，标量证明里交换顺序的论证失效——Lorist–Schwenninger 自己在 Section 3(iv) 指出这一点。本文的对策是不交换、而是保序：@@M@@FG@@ 与 @@M@@GF@@ 分开用。基维数限制（@@M@@2\times2@@ 的 BCD、@@M@@\le3@@ 的 Åhag–Czyż–Virtanen）则源于其相似化归技巧不跨维数，本文不再依赖相似。）
问 4：与 @@M@@1+\sqrt2@@ 及姊妹篇相比，真正的新意是什么？
（答：把 Crouzeix–Palencia 2017 的完整界从 @@M@@1+\sqrt2@@ 推到最优 2，且三个维数参数全部自由。姊妹篇《The complete Crouzeix theorem》用”最优相似＋公共正边界表示”的结构路线另证同一不等式，两文共享预解式正性这套解析内核但路径独立，互为印证。）
问 5：AI 生成证明的风险在这里如何？
（答：高危点本是共形几何细节：外部的 @@M@@h@@ 在 @@M@@|\lambda|>r@@ 单叶、Grunsky 型系数的指数衰减估计、以及最后把解析凸邻域序列收缩到任意紧凸数值域（点、线段退化情形全靠这一步）。据任务元信息主定理已通过 Lean 形式化，主链已被机器核验吸收；附录的外领圈构造与退化情形叙述仍以文本核验为宜。）
问 6：常数 2 为什么恰好不可再小？
（答：@@M@@2\times2@@ 幂零矩阵 @@M@@A@@ 的数值域是单位圆盘，@@M@@\|A\|=2=2\cdot\max_{W(A)}|z|@@——非正规性被数值域如数圈住、常数被精确吃满。任何小于 2 的普适常数都会在此翻车，所以 2 是理论极限而非艺术选择。）
问 7：谁会用到它？
（答：完全谱集与矩阵值泛函演算理论的人——@@M@@W(A)@@ 是完全 2-谱集自此是定理；依赖数值域做多项式界控制的数值线性代数（Krylov 子空间、矩阵函数逼近的误差估计）直接拿到最优常数。注意无穷维算子或一般有界凸域上的完整版论文未断言，仍属后续。）
总评
完整版 Crouzeix 猜想在矩阵形式上以一条直接估计收官，把十九年之久的 @@M@@1+\sqrt2@@ 缺口填到理论极限 2，且有 Lean 形式化与姊妹篇双保险；残余风险只在退化数值域的收缩极限叙述与共形附录，属边角可局部核验。