结果族 331：Reflexive midpoint convexity and diamond distortion · 学科：Functional analysis · 验证状态：主结果已 Lean 形式化
给球的”渐近圆度”画体检曲线：一种指标是中点版——两边对称地迈步，看范数平均涨多少；另一种是单侧版——只往一边迈，看涨多少。这篇论文在 @@M@@L^1@@（可积函数空间）的一个特殊子空间里，把两条曲线精确地算了出来：中点曲线在小步长时是 @@M@@t/2@@ 的线性上升，而单侧曲线直到步长 @@M@@2@@ 之前纹丝不动是零。两条曲线一分开，”中点圆度换不出单侧圆度”就不再是印象，而是精确事实。
关键词卡片
@@M@@T@@ 都有 @@M@@\|I+T\|=1+\|T\|@@；球面处处存在几乎正对的点，极端”圆”。@@M@@t@@ 时范数平均增益的最坏情形——中点圆度的曲线。@@M@@t@@ 的增益曲线——单侧圆度。看个具体例子
定理算出的两条曲线：@@M@@H_E(x,t)=\max\{t/2,\ t-1\}@@，@@M@@D_E(x,t)=\max\{0,\ t-2\}@@。代入步长 @@M@@t=1@@：
@@M@@DH_E(x,1)=\max\{0.5,\ 0\}=0.5,\qquad D_E(x,1)=\max\{0,\ -1\}=0@@
中点版涨一半，单侧版原地踏步；直到 @@M@@t=2@@ 单侧曲线才开始抬头。这张”体检单”同时证明：继承范数非 AUC，且任何等价范数都不可能 AUC。
为什么值得关心
它把”AMUC 不蕴含 AUC 可再赋范”从定性分离推进到精确模曲线，并给出 Kadets–Werner 构造的完整定量实现。
主结果已 Lean 形式化
第一级台阶
导读把两条渐近圆度曲线比作体检单：中点版对称迈步看平均涨多少，单侧版只往一边迈看涨多少。拧紧一点：对象是 L¹（概率空间上可积函数全体）的一个特殊子空间，长度尺子就是继承的 L¹ 范数；操作是先扔掉任意有限多个方向（选一个余维有限的子空间），再在剩下的方向里迈步，看范数增益的”最坏情形最好成绩”。两条曲线的差距，就是两种圆度的差距。
第二级台阶
| 用本科术语说：对范数 N、单位向量 x 与 t>0，平均中点模 H_N(x,t) 是 sup_F inf_{y∈F,N(y)≥1}[(N(x+ty)+N(x−ty))/2−1]，F 取遍余维有限子空间；单侧模 D_N(x,t) 把平均换成 N(x+ty)−1。N 渐近一致凸（AUC）指单侧模对一切 t>0 为正。Daugavet 性质指对每个秩一算子 T 有 ‖I+T‖=1+‖T‖；测度预紧指单位球在 d(f,g)=inf{a:P( | f−g | >a)<a} 下完全有界。 |
第三级台阶
定理 1.1 的语境：E 是 L¹ 的无限维闭子空间，仅两条几何假设——单位球测度预紧（它让截断把球变成范数紧集，供有限网与符号泛函取 F）与继承范数具 Daugavet 性质（它保证单位向量的每个弱邻域内都有近直径点）。结论在每个单位中心精确算出两条曲线：H_E(x,t)=max{t/2, t−1}，D_E(x,t)=max{0, t−2}——平均模在零附近线性增长而单侧模直到 t=2 恒为零；且任何等价范数都非 AUC。配套的构造节把 Kadets–Werner 扩张定量化，保证这样的空间确实存在。
对单位球在测度下完全有界且具 Daugavet 性质的 @@M@@L^1@@ 子空间，本文把平均渐近中点模与单侧渐近模精确算出为 @@M@@\max\{t/2,t-1\}@@ 与 @@M@@\max\{0,t-2\}@@，并证明任何等价范数都不渐近一致凸，把 Baudier 对”中点凸 ≠ 可再赋范一致凸”的分离做到了精确定量。
渐近一致凸（asymptotically uniformly convex，AUC）与渐近中点一致凸（asymptotic midpoint uniform convexity，AMUC）是 Banach 空间几何中刻画单位球”渐近圆度”的两种强弱不同的性质：前者要求沿余维有限子空间的方向单侧移动时范数有增益，后者只要求两个对称端点的平均值有增益。Dilworth、Kutzarova、Randrianarivony、Revalski 与 Zhivkov（2016）定义了 AMUC 并提出问题：AMUC 与 AUC 是否在再赋范（renorming）意义下等价？Baudier（2026）给出否定回答：他证明单位球在测度下相对紧的 @@M@@L^1@@ 子空间自动具有 AMUC，并套用 Kadets–Werner 的 Daugavet 例子。卡在哪里的是定量精度：此前只知道模的某个线性下界，两条模曲线的确切形状、以及”排除一切等价 AUC 范数”的完整论证，都未完成。
设 @@M@@E@@ 是概率空间上 @@M@@L^1@@ 的无限维闭实子空间，满足两条几何假设：单位球依测度度量 @@M@@d(f,g)=\inf\{a>0:\mathbb P(|f-g|>a)<a\}@@ 完全有界；继承的 @@M@@L^1@@ 范数具 Daugavet 性质（Daugavet property，即对每个秩一算子 @@M@@T@@ 有 @@M@@\|I+T\|=1+\|T\|@@）。对单位向量 @@M@@x@@ 与 @@M@@t>0@@，定义平均中点模 @@M@@H_E(x,t)@@ 为先取余维有限子空间 @@M@@F@@、再取 @@M@@F@@ 中范数 @@M@@\ge1@@ 的方向 @@M@@y@@ 时 @@M@@\frac{\|x+ty\|_1+\|x-ty\|_1}{2}-1@@ 的下确界的上确界，单侧模 @@M@@D_E(x,t)@@ 类似。定理证明：在每个单位中心处 @@M@@H_E(x,t)=\max\{t/2,t-1\}@@，@@M@@D_E(x,t)=\max\{0,t-2\}@@。于是平均模在原点附近有线性增长 @@M@@t/2@@，而单侧模直到 @@M@@t=2@@ 都恒为零——继承范数不仅自身非 AUC，且任何等价范数都不可能是 AUC。论文还给出 Kadets–Werner 构造的完整定量实现，保证满足两假设的空间确实存在，使整篇论证自足。
下界的核心是”截断＋符号泛函”。由恒等式 @@M@@(|a+b|+|a-b|)/2=\max\{|a|,|b|\}@@，平均增量恰等于 @@M@@\int(t|y|-|x|)_+\,d\mathbb P@@，因此只需控制 @@M@@y@@ 与 @@M@@x@@ 的重叠。把每个单位向量在高度 @@M@@|x|/t@@ 处逐点截断，截断算子逐点 1-Lipschitz，把测度预紧的单位球变成 @@M@@L^1@@ 紧集；取其有限 @@M@@\varepsilon@@-网，用网元的符号泛函的公共核作 @@M@@F@@，则 @@M@@F@@ 中任何单位向量的截断至多保留一半质量，即至少一半质量落在截断高度之外，直接给出 @@M@@t/2@@ 的增益；三角不等式给出 @@M@@t-1@@ 支。上界走完全相反的路线：先用 Kadets–Shvidkoy–Sirotkin–Werner 的切片刻画与 Bourgain 的”切片凸组合”引理，得到 Daugavet 性质等价于”单位向量的每个相对弱开邻域内都有几乎距离为 2 的点”；再对任意余维有限子空间 @@M@@F@@ 取核为 @@M@@F@@ 的有限秩投影 @@M@@P@@，在弱邻域 @@M@@\{v:\|P(v-x)\|<\varepsilon\}@@ 中选出几乎直径点 @@M@@v_\varepsilon@@，其差在 @@M@@F@@ 中的分量长度趋于 2，用凸组合恒等式把 @@M@@\|x+t y_\varepsilon\|@@ 压到 @@M@@1+(t-2)_+@@，两条上界曲线一次得到。排除再赋范的论证最巧：设 @@M@@N@@ 为等价 AUC 范数，取 @@M@@N@@ 在球上的近似极大点 @@M@@x_0@@，AUC 性质给出子空间 @@M@@F@@ 使大位移必带来 @@M@@(1+\gamma)@@ 倍增益，而商坐标意义下 @@M@@x_0@@ 的弱邻域内的点若想逃出增益区就必须与 @@M@@x_0@@ 的 @@M@@N@@-距离很小，进而 @@M@@\|\cdot\|@@-距离小于 @@M@@1/2@@——与弱邻域内必有近直径点矛盾。最后的构造部分将 Kadets–Werner 的有限维扩张定量化：用均值 1、高度集中在 0 附近的重尾乘子 @@M@@f=sV^{-1/p}@@ 乘旧单位向量生成新向量，借助常数 10、54、108 的尾概率与下界估计同时控制新球在测度度量下贴近旧球，用大数定律以平均恢复旧向量，再以可和误差 @@M@@h_b=2^{-b}@@ 迭代取闭包，极限空间同时保有测度预紧性与 Daugavet 切片性质。
论文声明其主结果已有 Lean 形式化证明，属结果族 331；姊妹篇（树位势模型与独立乘积模型）在同一框架下从三个不同角度印证”AMUC 不蕴含 AUC 可再赋范”，本文提供其中最精确的模曲线。按 OpenAI 官方声明，未经形式化的结果可能有问题；本篇主结果已形式化，可信度较高，但 Kadets–Werner 构造的定量常数等细节仍以论文原文与社区核验为准。
问 1：证明中最关键、最脆弱的一步是什么？
| （答：下界的”截断＋符号泛函”组合：由恒等式 ( | a+b | + | a−b | )/2=max{ | a | , | b | }，平均增益恰为 ∫(t | y | − | x | )_+dP，于是只需逼 y 与 x 的重叠。把单位向量在高度 | x | /t 处逐点截断（1-Lipschitz，把测度预紧球变范数紧），取有限 ε-网符号泛函的公共核作 F，则 F 中单位方向的截断至多留一半质量，得 t/2 增益。脆弱点在”测度预紧翻成范数紧”的换算与”一半质量”的出处——下界曲线的常数来源。） |
问 2：两条假设各自挡住什么？能去掉一条吗？
（答：分工明确：测度预紧只服务下界（造紧集与有限网），Daugavet 只服务上界与排重赋范（弱邻域近直径点，经 Shvydkoy 弱开刻画与 KSSW 切片刻画）。去掉测度预紧，Baudier 的 AMUC 定理本身就失效；去掉 Daugavet，max{0,t−2} 的上界无从谈起。论文未讨论单假设情形，但结构上两条各管一半、缺一即塌。）
问 3：与 Baudier 2026 相比真正的新意是什么？
（答：Baudier 只证了 AMUC（某个线性下界）并套用 Kadets–Werner 例子得定性否定；本文把两条模曲线在一切单位中心精确算死（H=max{t/2,t−1}、D=max{0,t−2}），并补全两块：对一切等价范数排除 AUC 的论证，与 Kadets–Werner 构造的定量实现；技术上用有限网截断取代 Brézis–Lieb 分裂路线，下界更可数化。）
问 4：单侧模为什么恰好死到 t=2？这个 2 有几何含义吗？
（答：t=2 正是单位球直径：上界走”取核为 F 的有限秩投影 P，在弱邻域 {‖P(v−x)‖<ε} 内选几乎直径点 v_ε”，其差在 F 中分量长度趋于 2，凸组合恒等式把 ‖x+ty‖ 压到 1+(t−2)_+。几何上，弱邻域里总有几乎对径点，前 2 步被直径余量吸收，t>2 才有净增益——折点即直径。）
问 5：排除一切等价 AUC 范数的论证为何最巧、风险何在？
（答：它要在陌生范数 N 下工作：取 N 的近似极大点 x₀，AUC 给出子空间 F 使大位移必有 (1+γ) 倍增益；而商坐标下 x₀ 的弱邻域内的点若逃不出增益区，就必须与 x₀ 的 N-距离很小、进而 ‖·‖-距离 <1/2——与”弱邻域内必有近直径点”矛盾。风险在 N-距离与 ‖·‖-距离的换算依赖等价常数，双范数桥接最易藏错。）
问 6：这类 AI 证明最可能的出错模式？
（答：最典型的是”先选子空间再选方向”的量词顺序：H、D 的定义是 sup_F inf_y，若证明中不小心换成 inf 后 sup，模会被系统性高估或低估；其次是构造节常数 10、54、108 与可和误差 2^{-b} 的账本。主定理已 Lean 形式化，模曲线有机器背书；构造节的定量常数与 Shvydkoy 引理的引用形式仍属人工核验范围。）
问 7：谁会用到精确模曲线？
（答：渐近几何与重赋范理论：AMUC/AUC 分离从此有了定量标尺，研究透镜非紧性、渐近凸性与度量嵌入失真换算的人可把”模≳t^p ⇒ 失真≳k^{1/p}”类传递规则用在精确曲线上；Daugavet 空间理论也多了把范数恒等式翻译成模公式的样例——”处处近对径”与”单侧模死到 t=2”是同一件事的两种说法。）
总评
把 DKRRZ 之问的否定回答从定性推到精确曲线，并自足补齐存在性构造，是结果族 331 中定量最强的收官篇，主定理有 Lean 背书；最大风险在双范数换算的重赋范排除段与构造节的常数账本，好在均非结论主干。