结果族 088：Sharp projection-body inequalities and a counterexample to simplex maximization · 学科：Convex and metric geometry（凸几何与度量几何） · 验证状态：主结果已 Lean 形式化
手影游戏：一个立体在灯光下朝各个方向投出影子，方向不同，影子的大小也不同。数学家把”每个方向的影子大小”整体打包，造成一个新的立体——投影体。Petty 1971 年猜：体积相同的立体中，椭球（球的均匀拉伸版）的投影体最小。这篇论文证明：在四维及以上的所有维度，椭球、且只有椭球，投影体最”瘦”。
关键词卡片
@@M@@\Pi K@@，其各方向的”半径”等于 @@M@@K@@ 在该方向投影的 @@M@@(n-1)@@ 维体积——一本影子档案册。@@M@@h_K(u)=\max_{x\in K}\langle x,u\rangle@@，凸体在方向 @@M@@u@@ 上伸出去的距离。@@M@@R_n(K)=|\Pi K|/|K|^{n-1}@@ 就是。看个具体例子
球朝任何方向投去，影子都是低一维的球。于是对单位球 @@M@@B@@（记 @@M@@\kappa_d@@ 为 @@M@@d@@ 维单位球体积），每个方向的影子一样大：@@M@@\Pi B=\kappa_{n-1}B@@。数字版定理：
@@M@@\frac{|\Pi K|}{|K|^{n-1}}\ \ge\ \frac{|\Pi B|}{|B|^{n-1}}=\kappa_{n-1}^{\,n}\,\kappa_n^{\,2-n}\qquad(n\ge4)@@
代入 @@M@@n=4@@ 读一读：任何四维凸体的”影子总分”都不低于球的值，取等的只有椭球。
一般凸体的影子随方向忽大忽小，打包出的投影体更胖；定理断言同体积下椭球最省，其余一律严格更胖。
为什么值得关心
与三维的已有结果合并，1971 年提出的 Petty 投影体积猜想在全部 @@M@@n\ge3@@ 维成立；论文还推出新的仿射 Sobolev 不等式与赋范空间等周不等式。
已 Lean 形式化
第一级台阶
手影游戏里有两个对象：一个立体，和它在墙上随方向变化的影子。导读做的事是把”整本影子档案”再打包成一个抽象立体：每个方向上伸出多远，就代表朝那个方向投影的影子有多大。问题变成：固定立体的体积，谁的影子档案最”省”——朝任何方向都不多占地方。球是当然的候选：它各方向影子一样大；均匀拉伸后的球（椭球）继承这一资格。
第二级台阶
| 用本科术语精确化：凸体 K 的支撑函数 h_K(u)=max_{x∈K}⟨x,u⟩ 记录各方向的伸展距离。投影体 ΠK 定义为支撑函数等于 K 向垂直于 u 的超平面正交投影之 (n−1) 维体积的对称凸体。比值 R_n(K)= | ΠK | / | K | ^{n−1} 在平移与可逆线性变换下不变——这由反变恒等式 Π(TK)= | det T | ·T^{−t}ΠK 保证——因而是仿射不变量；椭球即球经可逆线性映射的像。 |
第三级台阶
| 定理在 n≥4 陈述：对每个凸体——不要求对称、不要求边界正则——都有 R_n(K)≥κ_{n−1}^n·κ_n^{2−n}（κ_m 为 m 维单位球体积），等号当且仅当 K 是椭球，且等号断言是全局的、不附带”接近椭球”条件。无假设性排除了一切靠光滑化或局部刚性归约的旧路线；三维情形由外部结果补齐，本文证明不依赖它。证明把凸体化成测度：体积的第一变分产生一个概率测度，目标不等式归约为两个测度关于核 | x·y | 的双线性配对的下界，再用球面调和的谱间隙控制高次分量、用仿射坐标选择消去二次分量后收口。 |
证明 Petty 投影体积猜想在所有 @@M@@n\ge 4@@ 维成立：体积固定的凸体中，椭球、且仅有椭球，使其投影体的体积最小。与陈等人此前证得的三维结果合并，这个 1971 年提出的仿射等周型猜想在全部 @@M@@n\ge 3@@ 维度获得解决。
凸体 @@M@@K\subset\mathbb{R}^n@@ 的投影体（projection body）@@M@@\Pi K@@ 把各方向的”影子”打包成一个新凸体：其支撑函数 @@M@@h_{\Pi K}(u)@@ 定义为 @@M@@K@@ 向超平面 @@M@@u^\perp@@ 正交投影的 @@M@@(n-1)@@ 维体积。泛函 @@M@@R_n(K)=|\Pi K|/|K|^{n-1}@@ 在平移与可逆线性变换下不变，属于仿射等周问题（affine isoperimetric problem）；注意它与经典 Petty 投影不等式不同——后者度量的是 @@M@@\Pi K@@ 的极体的体积。Petty 在 1971 年猜想：当 @@M@@n\ge3@@ 时 @@M@@R_n@@ 恰被椭球最小化，由 @@M@@\Pi B_2^n=\kappa_{n-1}B_2^n@@ 可知最小值就是球的值。此前最好的结果都带限制：Saroglou–Zvavitch 与 Ivaki 的定理只在线性换坐标后”接近球”的范围内局部成立；Mielke–Sulz 只处理旋转体；陈-冯-李-席-徐证明了无附加假设的三维情形。难点在于一般凸体既不对称也无边界正则性，且等号条件必须是全局的。
主定理：对每个 @@M@@n\ge4@@ 与每个凸体 @@M@@K\subset\mathbb{R}^n@@，
@@M@@D\frac{|\Pi K|}{|K|^{n-1}}\ \ge\ \kappa_{n-1}^{\,n}\,\kappa_n^{\,2-n},@@
等号成立当且仅当 @@M@@K=a+TB_2^n@@，即 @@M@@K@@ 是椭球。定理对任意凸体成立，等号断言是全局的、不要求接近椭球。结合陈等人的三维定理，猜想对一切 @@M@@n\ge3@@ 成立（三维是外部结果，本文证明并不依赖它）。论文第七节还从主定理推出三组新不等式：Lutwak–Petty 低次投影体不等式——对 @@M@@1\le i\le n-1@@，@@M@@V_{i+1}(\Pi_i K)/V_{i+1}(K)^i@@ 达到球的下界，其中 @@M@@2\le i\le n-2@@ 是新确立的范围；非负紧支光滑函数的混合行列式梯度积分 @@M@@\mathcal D_n(f_1,\dots,f_n)@@ 的最优仿射 @@M@@L^1@@ Sobolev 不等式，其对角形式强于 Zhang 的仿射 Sobolev 不等式；以及赋范空间中 Holmes–Thompson 体积的等周不等式，等号当且仅当范数球是椭球且体与之位似。
证明走”化体为测度”的路线，核心是一个与投影体无关的双线性不等式。
第一步，把凸体换成测度。将 @@M@@K@@ 平移并归一化到 @@M@@|K|=\kappa_n@@ 后，体积的第一变分产生 @@M@@\mathbb{R}^n@@ 上的概率测度 @@M@@\eta_K@@：支撑有界、张成全空间，且对每个对称凸体 @@M@@M@@ 满足 @@M@@\int h_M\,d\eta_K\ge(|M|/\kappa_n)^{1/n}@@；同时 @@M@@h_{\Pi K}(y)@@ 等于 @@M@@\int|x\cdot y|\,d\eta_K(x)@@ 的固定倍数。于是目标下界化归为：任何两个满足该支撑函数条件的测度 @@M@@\eta,\zeta@@ 都有 @@M@@\iint|x\cdot y|\,d\eta(x)d\zeta(y)\ge b_n@@（@@M@@b_n=\E|u_1|@@）。
第二步，为测度配备变分最优的范数。在 @@M@@\tau_A(L)=1@@ 约束下最小化目标 @@M@@J(g)@@（@@M@@n=4@@ 取对数型 @@M@@\E\log g@@，@@M@@n\ge5@@ 取线性型 @@M@@\E g@@），存在唯一极小体，其规范函数（gauge）@@M@@g@@ 满足变分表示：测度的支撑泛函可用梯度场 @@M@@X_{g^k}=g^{k-1}\nabla g@@ 的球面平均表出。该构造属于对偶 Minkowski 问题（dual Minkowski problem）框架，但论文直接自证了表示公式、唯一性，以及随矩阵秩退化所需的连续性——测度可以带原子，极小体也不必光滑。
第三步，两块球面调和估计。符号检验用 @@M@@|a|\ge\operatorname{sgn}(u\cdot v)\,a@@ 把配对下方控制为含 cosine 变换（cosine transform）与 Funk 变换（Funk transform）的双线性形式，谱间隙 @@M@@\lambda_2=2n<\lambda_4=4(n+2)@@ 把常数部分与 4 次及以上调和部分分开；严格的范数估计则断言对任何范数 @@M@@g@@（不要求光滑）有 @@M@@c_{n,k}\|Q(g^k)\|_2^2\le(\E g^k)^2-(\E g^{k-1})^2@@，除非 @@M@@g\equiv1@@（欧氏情形）否则严格——证明先用范数凸性给出的曲率不等式 @@M@@\Delta_S g+(n-1)g\ge0@@ 分部积分，再化为逐点标量不等式，最后用光滑化逼近过渡到一般范数。
第四步，消去二次调和分量。它不是符号检验算子的零特征空间，只能靠选仿射坐标去除：把变分极小化解连续延拓到半正定矩阵锥的边界（此时规范函数退化为半范数），在退化核方向显式计算出一个指向锥内的矩阵场，Brouwer 不动点定理给出 @@M@@\det A=1@@ 的正定矩阵 @@M@@A@@，使 @@M@@g_A^k@@ 的二次分量为零。只需对一个测度做此规范化，另一个测度用逆步变换 @@M@@A^{-1}@@ 处理，配对 @@M@@\iint|x\cdot y|@@ 在 @@M@@(Ax)\cdot(A^{-1}y)=x\cdot y@@ 下不变。
最后合成：对 @@M@@\eta_K@@ 与体积归一的投影体的测度应用双线性不等式，得 @@M@@|\Pi K|\ge\kappa_n\kappa_{n-1}^{\,n}@@，解除归一化即为主定理。等号情形被逐步逼紧：先得 @@M@@g\equiv1@@，即支撑条件在某个中心椭球上取等，再由第一变分的等号断言推出 @@M@@K@@ 是该椭球的平移相似像。
论文标注主结果已有 Lean 形式化证明。族内姊妹篇《A product counterexample to the simplex maximum for projection-body volume》处理同一泛函的另一端：本文确定极小值侧（椭球唯一最小化），姊妹篇推翻极大值侧的 Brannen 单形猜想，两篇合看才构成 @@M@@R_n@@ 极值行为的完整图景。第七节推论引用了 Lutwak 与 Haddad 的条件性蕴含等外部文献，属”主定理＋引用”的组合。按 OpenAI 官方声明，未经形式化的结果可能有问题；本文主结果已形式化，是族内可信度最高的一环。
问 1：证明里最关键也最脆弱的一步在哪？
答：仿射规范化命题。二次调和分量不是符号检验算子的零特征空间，调和分析消不掉，只能选坐标消去。论文把变分极小化解连续延拓到半正定矩阵锥的边界——此时规范函数退化为半范数——在退化方向显式算出一个指向锥内的矩阵场，Brouwer 不动点给出 det A=1 且二次分量为零的位置。延拓要穿越矩阵秩的变化，其连续性（测度可带原子、极小体可不光滑）是全文最软也最险的一环。
问 2：为什么只证 n≥4，三维怎么办？
答：变分目标的形状随维度分岔：n=4 取对数型 E log g，n≥5 取线性型 E g，对数端点需要单独处理。三维情形由 Chen–冯–李–席–徐的外部定理补齐，合并后猜想在一切 n≥3 成立；引言明言本文对 n≥4 的证明不使用那个外部结果。
问 3：与已有工作相比真正的新意是什么？
答：此前结果全带限制：Saroglou–Zvavitch 与 Ivaki 只在”线性换坐标后接近球”的局部成立，Mielke–Sulz 只处理旋转体，Chen 等只做三维。本文对任意凸体给出不等式加全局等号分类。方法上的新部件有二：对任意（不必光滑）范数的高次调和严格估计，以及极小化测度穿越矩阵秩的连续选择——后者使全局仿射坐标成为可能。
问 4：哪个技术环节最值得复核？
答：严格范数估计的逼近层。它先对光滑范数用曲率不等式 Δ_S g+(n−1)g≥0 分部积分、化为逐点标量不等式，再经光滑化逼近过渡到一般范数。逼近步要保证严格性在极限中不丢失（否则等号分类会多出极限体）。主结果已 Lean 形式化，这一风险已大幅压低。
问 5：与姊妹篇是什么关系？
答：同一泛函 R_n 的两端。本文定极小值侧（椭球唯一最小化）；姊妹篇用两个十维单纯形的乘积推翻 Brannen 的单纯形极大值猜想。两篇合看才构成 R_n 极值行为的完整图景——这正说明”极小侧已完美解决”不蕴含极大侧任何信息。
问 6：谁会用这个结果？
答：第七节的三组推论直接服务不同社区：Lutwak–Petty 低次投影体不等式（2≤i≤n−2 为新确立范围）给凸几何；最优仿射 L¹ Sobolev 不等式（对角形式强于 Zhang 的）给分析；赋范空间 Holmes–Thompson 等周不等式给有限维几何。这些推论属”主定理＋引用外部蕴含”的组合，引用部分未形式化。
总评
这是把 1971 年仿射等周猜想收官到全维度的硬结果，Lean 背书加全局等号分类使其成为族内最可靠的一环；残余风险集中在穿越秩退化的连续性论证与未形式化的推论链。