结果族 360：Weak MTW curvature gives convexity and regular optimal transport · 学科：Differential geometry · 验证状态：主结果已 Lean 形式化
把一堆沙以最省代价搬到指定位置（最优运输），搬运方案是否连续规矩，取决于地形几何。论文证明：名为”弱 MTW”的曲率条件自动保证每个点的”可行出发方向盘”是凸的——不许有月牙形缺口——而且方案里每个点都被一座”整山”从下方稳稳托住。
关键词卡片
看个具体例子
定理一：弱 MTW ⇒ 每点的切单射域 @@M@@I(x)@@ 及闭极小域 @@M@@G_x@@ 都是凸集：
定理二：每个次梯度 @@M@@p\in\partial u(x)@@ 都是极小速度，满足全局支撑不等式 @@M@@u(x')\ge u(x)+c(x,\exp_x p)-c(x',\exp_x p)@@；且全程不假设非聚焦、允许共轭割点、不用任何密度假设。
为什么值得关心
它在无聚焦假设下解决 Villani 猜想，补上”弱 MTW ⇒ 凸单射域 ⇒ 一致正则输运”这条链条中缺失的一环。
已 Lean 形式化
第一级台阶
导读里”搬运方案是否规矩”指把一个概率分布搬到另一个的最优映射是否连续；”可行出发方向盘”是从某点出发、沿测地线走过单位时间后仍保持最短路的那些初速度；”凸”是说任意两个可行方向的中间方向仍可行，不许有月牙形缺口；”整山托住”则是势函数图像的每一点都被一张全局切平面从下方稳稳撑住。论文宣布：一个只管”横向”的曲率条件，就足以同时买到这两样。
第二级台阶
用本科术语精确化：设 @@M@@(M,g)@@ 为紧致无边界的光滑黎曼流形，代价取平方测地距离 @@M@@c(x,y)=d(x,y)^2/2@@。切单射域 @@M@@I(x)=\{v:\exists a>1,\ d(x,\exp_x(av))=a|v|\}@@，闭极小域 @@M@@G_x=\{p:d(x,\exp_xp)=|p|\}@@。弱 MTW 条件（A3w）只要求：当方向 @@M@@\xi\perp\eta@@ 时，代价的四阶交叉导数 @@M@@\mathfrak S_{(x,v)}(\xi,\eta)\ge0@@ 对一切 @@M@@v\in I(x)@@ 成立——对非正交方向、严格正性一概不问。势函数 @@M@@u(x)=\max_y\{-c(x,y)-v(y)\}@@ 是最优输运的对偶对象，@@M@@\partial u(x)@@ 是其普通次梯度。
第三级台阶
两个定理的语境：@@M@@n\ge2@@、@@M@@M@@ 紧致连通无边界、满足弱 MTW。定理一说每个 @@M@@I(x)@@ 与 @@M@@G_x@@ 都是凸集——普通线性凸，共轭割点照单全收，这解决了 Villani 的猜想；定理二说每个次梯度 @@M@@p\in\partial u(x)@@ 都是极小速度且满足全局支撑不等式 @@M@@u(x')\ge u(x)+c(x,\exp_xp)-c(x',\exp_xp)@@，中间时刻 @@M@@F_t(x,p)=\exp_x(tp)@@（@@M@@0<t<1@@）是次梯度图到 @@M@@M@@ 的同胚。”紧致”挡住向无穷的逃逸；”只控垂直方向”的弱假设与”允许共轭割点”的组合正是此前 Loeper–Villani、Figalli–Gallouët–Rifford 需要非聚焦才能绕过的两道墙；全文不用任何密度假设。
在紧致无边的连通黎曼流形上，弱 MTW 曲率条件本身就迫使每点的切单射域凸，从而在不假设非聚焦的前提下解决 Villani 猜想；同时证明任意势函数的次梯度都自带全局支撑山峰，为一致正则输运奠定几何基础。
最优输运（optimal transport）研究如何以最小代价把一个概率分布搬运到另一个。当代价取紧黎曼流形上的平方测地距离 @@M@@c(x,y)=d(x,y)^2/2@@ 时，输运映射的连续性严重依赖代价几何：距离函数在割迹（cut locus）处失去光滑。Ma–Trudinger–Wang 曲率条件正是为控制这种几何而生，其退化形式”弱 MTW”（又称 A3w）只要求代价在正交方向上的四阶交叉导数非负。Villani 猜想：弱 MTW 应蕴含每个切单射域（tangent injectivity domain）@@M@@I(x)@@ 的凸性——这是支撑山峰方法成立的关键前提。此前 Loeper–Villani 在强 MTW 加非聚焦（nonfocality）下、Figalli–Gallouët–Rifford 在一般非聚焦下证明了该蕴含；共轭割点（conjugate cut point）情形始终是障碍：那里代价可能不光滑，而弱 MTW 只控制垂直于速度线段的方向，两个困难都无法靠在定义域之外延拓光滑凹性来绕过。
论文证明两个定理。定理一（单射域凸性）：设 @@M@@(M,g)@@ 为维数 @@M@@n\geq2@@ 的光滑连通紧致无边界黎曼流形且满足弱 MTW，则对每点 @@M@@x@@，切单射域 @@M@@I(x)@@——测地线越过时刻 1 仍保持极小的初速度构成的开集——是凸的；闭极小域 @@M@@G_x@@ 同样凸。结论是普通线性凸性，不需要非聚焦、严格 MTW、非正交方向的曲率条件或先验凸性，共轭割点被允许。定理二（全局支撑与中间几何）：对任意由连续数据定义的势函数（potential）@@M@@u(x)=\max_y\{-c(x,y)-v(y)\}@@，每个普通次梯度（subdifferential）@@M@@p\in\partial u(x)@@ 都是极小速度，即 @@M@@p\in G_x@@，且满足全局支撑不等式 @@M@@u(x')\geq u(x)+c(x,\exp_xp)-c(x',\exp_xp)@@；对每个 @@M@@0<t<1@@，投影 @@M@@F_t(x,p)=\exp_x(tp)@@ 是次梯度图到 @@M@@M@@ 的同胚（homeomorphism）；提升间隙截面 @@M@@\mathcal S_x(r)@@ 紧且凸，直径平方不超过 @@M@@8(r+\operatorname{osc}v)@@；中间势 @@M@@Q_tu=-Q_{1-t}v@@ 具有只依赖流形与时刻 @@M@@t@@ 的 @@M@@C^{1,1}@@ 界与极点 Lipschitz 控制。全部结论不使用任何密度假设。
证明把”支撑山峰”（supporting mountain）原则推过割迹，分三步。第一步建立无聚焦假设下的工具箱：在非共轭速度处定义光滑测地分支的分支 Hessian（branch Hessian）@@M@@A_x(w)@@，证明径向恒等式 @@M@@A_x(w)w=w@@、严格径向比较 @@M@@A_x(sa)>\frac{s}{s'}A_x(s'a)@@，并把弱 MTW 转化为横向凹性——沿速度线段 @@M@@b_t@@，当 @@M@@\xi@@ 垂直于线段方向时 @@M@@A_x(b_t)(\xi,\xi)@@ 是凹函数。第二步排除共轭性：设 @@M@@[b_0,b_1]\subset G_x@@ 两端非共轭而内点 @@M@@z@@ 共轭，先用指数映射的核向量构造两端为零的 Jacobi 场（Jacobi field），平行输运成试验场族，得 @@M@@A_x(a)(\xi,\xi)\leq C_0-c_0/P(a)@@，其中指标型（index form）@@M@@P(a)@@ 在 @@M@@a\to z@@ 时趋于零，Hessian 随之崩向 @@M@@-\infty@@；横向凹性迫使共轭核落入线段方向 @@M@@e@@，径向恒等式又给出方向 @@M@@e@@ 上的下界 @@M@@A_x(r(z+te))(e,e)\geq 1-C_2/t@@，与径向收缩 @@M@@r=1-t^2@@ 时的上界 @@M@@C_1-c_1/(t^2+1-r)@@ 在 @@M@@t\downarrow0@@ 时不相容。第三步是延拓论证：把次梯度图随时间 @@M@@t@@ 放大，取首次触割时刻 @@M@@t_*@@；极小凸包经取极限仍极小，第二步的推论使其整体非共轭；局部单射引理再排除两个图点撞到同一像的情形——一阶不等式把正权积极小速度逼入垂直于碰撞方向的仿射超平面，线性项在除以碰撞距离平方之前于有限阶段被精确抵消，弱 MTW 与径向严格比较联立给出正二次间隙而矛盾；随后由区域不变性（invariance of domain）与”和短时同胚同伦的覆叠映射必单叶”的拓扑事实，把局部单射升级为整体同胚，再由”捕获每个极小对数”引理逼出与首次失败矛盾，故任何图向量在时间 1 之前都碰不到割。最后令 @@M@@t\uparrow1@@ 取闭包极限得全局支撑；把它应用于两座山峰的极大值即得 @@M@@G_x@@ 凸，进而 @@M@@I(x)=\operatorname{int}G_x@@ 凸；截面凸性、直径界与 @@M@@C^{1,1}@@ 中间正则性由分裂支撑、逆向测地流与双侧支架给出。
论文声明主结果已有 Lean 形式化证明。本文是结果族 360 的几何基石：姊妹篇《Uniform Bi-Hölder Transport from Weak MTW》把本文的全部密度无关结论作为输入，两文合成”弱 MTW @@M@@\Rightarrow@@ 凸单射域 @@M@@\Rightarrow@@ 一致正则输运”的完整链条，补上了 Figalli–Rifford–Villani 当年需额外假设凸单射域才能得到的全局支撑原则。按 OpenAI 官方声明，未经形式化的结果可能有问题；本文主结果已形式化，附录中的度数理论替代论证是可选路线，不影响主证明。
问 1：证明中最关键、最脆弱的一步是什么？
答：排除共轭性（sec:conjugacy）。设线段 @@M@@[b_0,b_1]\subset G_x@@ 两端非共轭而内点共轭：用指数映射核向量构造两端为零的 Jacobi 试验场，得分支 Hessian 上界 @@M@@A_x(a)(\xi,\xi)\le C_0-c_0/P(a)@@，指标型 @@M@@P(a)@@ 趋零时 Hessian 崩向 @@M@@-\infty@@；横向凹性迫使共轭核躲进线段方向 @@M@@e@@，而径向恒等式在该方向给下界 @@M@@1-C_2/t@@，与径向收缩后的上界在 @@M@@t\downarrow0@@ 时不相容。上下界都只在极限处分胜负，余量极薄。
问 2：为什么此前的非聚焦假设不能只是”方便”？
答：Figalli–Gallouët–Rifford 的证明靠非聚焦保证割点严格先于第一共轭点，代价在关键区域保持光滑。本文允许共轭割点后，代价沿速度线段可能失去光滑，而弱 MTW 又只控制垂直于线段的方向——introduction 明说这两个困难都无法靠把光滑凹性延拓到定义域之外来绕过，必须整个换掉技术框架。
问 3：与已有工作相比真正的新意是什么？
答：Loeper–Villani 在强 MTW 加非聚焦下得凸性；FGR2014 在一般非聚焦下得蕴含；FRV2011 则是把”凸单射域”当假设推出全局支撑。本文从弱 MTW 单独推出凸性本身，再自行重建全局支撑，且共轭割点、密度假设一概豁免——Villani 猜想在此设定下被完整解决。
问 4：为什么中间时刻的同胚结论到不了时刻 1？
答：introduction 给出反例：@@M@@u(x)=-c(x,y_0)@@ 有多个极点共享同一终点，@@M@@F_1@@ 无法单射。只有”支撑与极小速度”两条断言经闭包通过到时刻 1，@@M@@C^{1,1}@@ 中间正则性与同胚只对 @@M@@0<t<1@@ 成立——边界处的退化是本质的。
问 5：AI 生成的证明最可能在哪里出错？
答：两处顺序敏感的操作：其一是排除图投影碰撞时，一阶不等式把正权积极小速度逼入垂直于碰撞方向的仿射超平面后，线性项必须在除以碰撞距离平方之前”于有限阶段被精确抵消”，次序颠倒则极限不闭合；其二是局部单射经”与短时同胚同伦的覆叠映射必单叶”升级为整体同胚的拓扑论证，覆叠层数的归纳若漏情形即断链。缓解因素：主结果已 Lean 形式化。
问 6：谁会用到它？
答：最优输运正则性理论的研究者：姊妹篇《Uniform Bi-Hölder Transport from Weak MTW》把本文全部密度无关结论当输入，合成”弱 MTW @@M@@\Rightarrow@@ 凸单射域 @@M@@\Rightarrow@@ 一致正则输运”的完整链条；Monge 问题、代价为平方距离的正则性研究都直接受益。
总评
这是 Villani 猜想在最弱假设下的解决，也是整条正则输运链条缺失地基的浇筑，且带形式化背书；最大残余风险在排除共轭性与碰撞抵消两处极限论证的常数细节——恰是 Lean 语句最难逐字覆盖的部分。