结果族 072：Brennan’s conjecture and the integral-means spectrum · 学科：Real and complex analysis · 验证状态：主结果已 Lean 形式化
想象一张圆形橡皮膜，被无重叠地拉伸成任意形状。越靠近边缘，变形可以越疯狂。这篇论文精确回答：把”压缩程度”沿靠近边缘的薄圈平均之后，最多能以多快的速度增长？结论：严格慢于 @@M@@(1-r)^{-1/4}@@ 这条公认分界线，从而推翻了一个流行近三十年的谱公式。
关键词卡片
@@M@@|f'|^p@@ 沿半径 @@M@@r@@ 的圆周取平均，度量变形在边缘附近的集中速度。@@M@@B(p)@@；本文主角是 @@M@@p=-1@@ 处的 @@M@@B_b(-1)@@。@@M@@B_b(p)=p^2/4@@，在 @@M@@p=-1@@ 处预言恰为 @@M@@1/4@@。看个具体例子
把猜测的谱画成图：Kraetzer 认为它是抛物线 @@M@@p^2/4@@，于是 @@M@@p=-1@@ 处的高度恰为 @@M@@1/4@@（空心点）；本文证明真实高度严格更低（实心点）。
数字版定理：取 @@M@@r=1-10^{-8}@@。此前最佳上界的指数是 @@M@@0.388@@，允许均值涨到约 @@M@@10^{3.1}@@ 倍；新定理保证增长因子的指数严格小于 @@M@@1/4@@，即不超过 @@M@@10^{2}@@ 倍（不计常数）。
为什么值得关心
这是 Brennan 猜想家族的关键进展：首次把 @@M@@p=-1@@ 处的指数严格压到 @@M@@1/4@@ 之下，宣布 Kraetzer 谱公式不真，而这类指数与单叶函数泰勒系数的经典难题直接相关。
已 Lean 形式化
第一级台阶
导读里的”橡皮膜”其实是三样东西：一张膜（单位圆盘）、一种不许折叠的拉伸（一一保形映射）、以及边缘附近的薄圈（靠近边界的圆周）。”压缩程度”就是拉伸在某点的剧烈程度，把它沿一个薄圈平均，得到一个数；当薄圈不断逼近边缘，这个数最多以多快的速度变大，就是全部问题。
第二级台阶
| 用本科复分析的语汇：单位圆盘上的单叶函数指单射全纯映射（导数处处非零），记标准化条件为原点映到原点、导数在一处为 1。对实数指数 p 与半径 r，积分均值 M_pf’ 定义为 | f’ | ^p 沿圆周 | z | =r 的平均；每个映射有自己的增长指数（limsup 型），而对有界 image 的单叶类取上确界，得到普适积分均值谱 B_b(p)。 |
第三级台阶
定理在无界 image 也不加边界正则性的最一般单叶类上陈述：存在与映射无关的常数，使逆一次幂均值 M_{-1}f’ 被 (1-r) 的 -1/4+ε 次幂一致控制，其中 ε 是某个严格正的间隙（证明不给数值）。假设”单叶”挡住了折叠带来的高阶奇性，而”归一化”只起定标作用、不影响指数。结论取极限指数后即 B_b(-1)<1/4，与 Kraetzer 1996 年基于数值实验提出的谱公式 B_b(p)=p²/4 在 p=-1 处的预测值 1/4 相冲突——猜测的恒等式被证伪，且此前的严格上界 0.388 均停在 1/4 之上。
第一级台阶
导读里的”橡皮膜”其实是三样东西：一张膜（单位圆盘）、一种不许折叠的拉伸（一一保形映射）、以及边缘附近的薄圈（靠近边界的圆周）。”压缩程度”就是拉伸在某点的剧烈程度，把它沿一个薄圈平均，得到一个数；当薄圈不断逼近边缘，这个数最多以多快的速度变大，就是全部问题。
第二级台阶
| 用本科复分析的语汇：单位圆盘上的单叶函数指单射全纯映射（导数处处非零），记标准化条件为原点映到原点、导数在一处为 1。对实数指数 p 与半径 r，积分均值 M_pf’ 定义为 | f’ | ^p 沿圆周 | z | =r 的平均；每个映射有自己的增长指数（limsup 型），而对有界 image 的单叶类取上确界，得到普适积分均值谱 B_b(p)。 |
第三级台阶
定理在无界 image 也不加边界正则性的最一般单叶类上陈述：存在与映射无关的常数，使逆一次幂均值 M_{-1}f’ 被 (1-r) 的 -1/4+ε 次幂一致控制，其中 ε 是某个严格正的间隙（证明不给数值）。假设”单叶”挡住了折叠带来的高阶奇性，而”归一化”只起定标作用、不影响指数。结论取极限指数后即 B_b(-1)<1/4，与 Kraetzer 1996 年基于数值实验提出的谱公式 B_b(p)=p²/4 在 p=-1 处的预测值 1/4 相冲突——猜测的恒等式被证伪，且此前的严格上界 0.388 均停在 1/4 之上。
证明对所有标准化单叶函数一致成立的估计 @@M@@M_{-1}[f'](r)\le C(1-r)^{-1/4+\varepsilon}@@，从而有界单叶类的普适积分均值谱满足 @@M@@B_b(-1)<1/4@@，推翻了 Kraetzer 谱猜想在 @@M@@p=-1@@ 处的预测值。
单叶（univalent，即单射全纯）函数的导数即使在图像有界时也能在边界附近剧烈集中，积分均值谱（universal integral-means spectrum）记录这种集中速率在整类映射上的最大可能指数。对图像有界的子类 @@M@@\mathcal S_b@@，Kraetzer 在 1996 年论文与学位论文中依据数值实验猜测 @@M@@B_b(p)=p^2/4@@（@@M@@|p|\le2@@）、@@M@@B_b(p)=|p|-1@@（@@M@@|p|\ge2@@），在 @@M@@p=-1@@ 处给出预测值 @@M@@1/4@@。此前最好的严格上界来自 Hedenmalm–Shimorin 的加权 Bergman 空间方法（对无界标准盘类得 @@M@@0.403@@）与 Sola 的改进（@@M@@0.388@@），都停在 @@M@@1/4@@ 之上；Beliaev–Smirnov 的随机共形雪花路线给出的是数值近似而非严格误差控制。该问题与 Carleson–Jones 系数问题相联系，且由 Makarov 比较定理，无界谱是有界谱与 Koebe 贡献 @@M@@3p-1@@ 的最大值，故两谱在正指数处本质不同。本文首次把 @@M@@p=-1@@ 处的上界严格压到 @@M@@1/4@@ 之下。
定理：存在常数 @@M@@0<\varepsilon<1/4@@ 与 @@M@@C<\infty@@，使得对每个标准化单叶函数 @@M@@f\in\mathcal S@@ 与每个 @@M@@1/2\le r<1@@，逆一次幂积分均值满足 @@M@@M_{-1}[f'](r)\le C(1-r)^{-1/4+\varepsilon}@@；常数与映射无关，连图像大小也无关，且不要求图像有界。取极限指数即得 @@M@@B_b(-1)<1/4@@，故 Kraetzer 猜想的谱恒等式不真。需要说明：证明只给出正间隙的存在性，不给出 @@M@@\varepsilon@@ 的数值；结论也不解决 @@M@@p=1@@ 处的猜测值。
骨架与姊妹篇（Brennan 猜想一文）同构，但权重处处由平方改为一次幂，并新增”严格性”机制。先在上半平面紧类 @@M@@\mathcal K@@（@@M@@F(i)=0@@、@@M@@F'(i)=1@@ 的单叶映射，由 Montel 与 Hurwitz 定理紧致）上定义正算子 @@M@@A_z\Phi(F)=|Q_F(z)|\Phi(T_zF)@@（@@M@@Q_F=1/F'@@），其增长率 @@M@@\rho=2^\beta@@（@@M@@0\le\beta\le1@@）通过二进网格比较控制全部盘均值：@@M@@M_{-1}[f'](r)\le C_0\|L^n\|@@，故 @@M@@B_b(-1)\le\beta@@。反设 @@M@@\beta\ge1/4@@。第一步与姊妹篇平行：由特征测度加水平平移与对数尺度平均，构造精确参数的仿射律 @@M@@\mathbb E[|Q_F(x+iy)|\Phi(T_zF)]=y^{-\beta}\mathbb E\Phi(F)@@，对常数测试求导得矩 @@M@@\mathbb Ea_F(i)=-\beta@@、@@M@@\mathbb E|q_F(i)|^2=\beta(\beta+1)@@（一次幂权重使矩的数值与姊妹篇不同）。第二步取 @@M@@k=(\beta+2)/3@@ 与位势 @@M@@V_\xi^F=y^k/|F-\xi|@@，其临界点由临界映射 @@M@@G_F=F-\frac{iy}{k}F'@@ 的原像给出；规范化符号 Jacobi 的期望为 @@M@@k^2\mathbb EJ_F(i)=(4\beta-1)(\beta+2)/9@@，当 @@M@@\beta>1/4@@ 时严格为正，当 @@M@@\beta=1/4@@ 时恰好为零——这个临界归零是本文独有的分岔。第三步是严格配对：好目标除要求正超水平集紧（对几乎一切映射与目标成立）与正则值（Sard 定理）外，还要求不同临界点的 @@M@@V@@ 值互不相同；无并列这一性质由 @@M@@F@@ 的单射性经隐函数论证排除并列临界值的零测集而得。于是按 @@M@@V@@ 值降序的同秩配对把每个鞍点送到 @@M@@V@@ 值严格更大的极大点。第四步是严格输运：定义比值 @@M@@c_F(z)=(V(R_F(z))/V(z))^3>1@@，配对在每个目标纤维上的单射性给出加权不等式，取期望得 @@M@@\mathbb EJ_{F,+}c_F\le\mathbb EJ_{F,-}@@，进而 @@M@@\mathbb EJ_F(i)\le0@@；若取等，则非负量 @@M@@J_{F,+}(c_F-1)@@ 期望为零，迫使 @@M@@J_F(i)=0@@ 几乎必然——不同点对之间的增益可以任意小，无需一致 Gap。与矩公式比较：@@M@@\beta>1/4@@ 立即矛盾；只剩 @@M@@\beta=1/4@@ 且 @@M@@J_F\equiv0@@ 几乎必然的刚性情形。最后用调和屏障排除它：@@M@@k=3/4@@ 时 @@M@@J_F\equiv0@@ 等价于 @@M@@|q_F+1/4|^2=1/4@@，从而前 Schwarz 量满足 @@M@@|F''/F'|\ge1/(4y)@@，其对数 @@M@@u@@ 调和且 @@M@@\ge-\log4-\log y@@；在矩形 @@M@@[-1,1]\times[\varepsilon,1]@@ 上构造在 @@M@@i/2@@ 处随 @@M@@\log(1/\varepsilon)@@ 增长趋于无穷的调和下屏障，与 @@M@@u(i/2)@@ 有限矛盾。故 @@M@@\beta<1/4@@，取 @@M@@b\in(\beta,1/4)@@ 用根极限与盘比较即得一致估计。
主结果已 Lean 形式化：族内 StrictMeans.lean 覆盖一致估计与 @@M@@B_b(-1)<1/4@@ 的推论。本文与姊妹篇《Brennan’s conjecture and sharp inverse-square integral means》共享”紧模型—二进采样—鞍点/极大点配对—输运矛盾”框架并互相印证；文中明确声明全部一次幂估计与输运输断均自证，不引用姊妹篇的逆平方端点定理。按 OpenAI 官方声明，未经形式化的结果可能存在问题；本篇主结果已形式化，但 @@M@@\varepsilon@@ 的具体数值未给出，读者应以社区核验为准。
问 1：证明里最脆弱的一环在哪里？
（答：引言明确指出”严格性”是本文独有的障碍——非严格的鞍点/极大点比较只能排除 β>1/4，不能排除恰好等于 1/4。为此第 4-5 节要求”不同临界点的位势值互不相同”（无并列），再由严格配对把等号情形逼到 Jacobi 几乎必然为零。无并列依赖 F 的单射性加隐函数论证排除零测集，这一步没有经典文献可循，是全文最依赖自创测度论细节的地方。）
问 2：去掉”单叶”假设会怎样？
| （答：立刻崩塌。单射性在证明中至少承担两职：保证 1/F’ 处处有定义（导数无零点，任意实幂可取）；并在第 4 节用于排除临界值并列的零测集。若允许临界点， | f’ | 的奇性可以任意坏，积分均值谱问题本身就不再有 1/4 量级的参照系。） |
问 3：与 Hedenmalem–Shimorin/Sola 的 Bergman 空间方法相比，真正的新意是什么？
| （答：不是数值改进而是方法换代：此前最好上界 0.388 停在 1/4 之上，路线是加权 Bergman 空间；本文改用上半平面紧类上的正算子 L（在两个仿射子尺度采样 1/ | F’ | ），其增长率 2^β 直接控制一切盘均值，再用仿射律、矩恒等式与鞍点-极大点输运矛盾导出 β<1/4。框架与姊妹篇（Brennan 猜想一文）同构但一次幂权重处处不同，文中声明全部输运输断自证、不引用姊妹篇端点定理。） |
问 4：既然主结果已 Lean 形式化，AI 生成证明的典型风险还剩什么？
（答：形式化覆盖 StrictMeans.lean 中的一致估计与 B_b(-1)<1/4 推论，这是最强的可信度背书。但论文正文与形式化脚本之间仍可能有措辞级偏差（如”对几乎一切映射与目标成立”的例外集处理），且 ε 无数值、p=1 处的猜测值未解决——引用结论时应只引用已形式化的部分。）
问 5：等号情形为什么需要调和屏障这最后一步？
| （答：严格配对把矛盾逼到”β=1/4 且 J_F 几乎必然为零”的刚性情形，输运不等式到此取等、无法继续。第 6 节证明此时 k=3/4 下 J_F≡0 等价于 | q_F+1/4 | ²=1/4，即前 Schwarz 量满足一个下调和型不等式，其在固定点的值随屏障区域 ε→0 而被迫无界，与 u(i/2) 有限矛盾。没有这一步，定理只能得到 β≤1/4。） |
问 6：谁会用这个结果？
（答：直接用户是单叶函数与共形映射社区：B_b 谱的任何一点定位都反馈到 Carleson–Jones 系数问题；由 Makarov 比较定理，无界谱 = max(有界谱, 3p-1)，本文在有界谱负指数端给出的严格间隙也修正了数值工作者对整条谱曲线的预期——Kraetzer 抛物线不再是可引用的猜测。）
总评
这是把一个悬置近三十年的数值猜测第一次钉进严格数学的工作，且经 Lean 形式化，分量扎实；最大风险在于严格配对与输运环节的测度论细节虽逻辑自洽但极精密，未经独立人类证明复现之前，引用范围应守住已形式化的主定理本身。
问 1：证明里最脆弱的一环在哪里？
（答：引言明确指出”严格性”是本文独有的障碍——非严格的鞍点/极大点比较只能排除 β>1/4，不能排除恰好等于 1/4。为此第 4-5 节要求”不同临界点的位势值互不相同”（无并列），再由严格配对把等号情形逼到 Jacobi 几乎必然为零。无并列依赖 F 的单射性加隐函数论证排除零测集，这一步没有经典文献可循，是全文最依赖自创测度论细节的地方。）
问 2：去掉”单叶”假设会怎样？
| （答：立刻崩塌。单射性在证明中至少承担两职：保证 1/F’ 处处有定义（导数无零点，任意实幂可取）；并在第 4 节用于排除临界值并列的零测集。若允许临界点， | f’ | 的奇性可以任意坏，积分均值谱问题本身就不再有 1/4 量级的参照系。） |
问 3：与 Hedenmalem–Shimorin/Sola 的 Bergman 空间方法相比，真正的新意是什么？
| （答：不是数值改进而是方法换代：此前最好上界 0.388 停在 1/4 之上，路线是加权 Bergman 空间；本文改用上半平面紧类上的正算子 L（在两个仿射子尺度采样 1/ | F’ | ），其增长率 2^β 直接控制一切盘均值，再用仿射律、矩恒等式与鞍点-极大点输运矛盾导出 β<1/4。框架与姊妹篇（Brennan 猜想一文）同构但一次幂权重处处不同，文中声明全部输运输断自证、不引用姊妹篇端点定理。） |
问 4：既然主结果已 Lean 形式化，AI 生成证明的典型风险还剩什么？
（答：形式化覆盖 StrictMeans.lean 中的一致估计与 B_b(-1)<1/4 推论，这是最强的可信度背书。但论文正文与形式化脚本之间仍可能有措辞级偏差（如”对几乎一切映射与目标成立”的例外集处理），且 ε 无数值、p=1 处的猜测值未解决——引用结论时应只引用已形式化的部分。）
问 5：等号情形为什么需要调和屏障这最后一步？
| （答：严格配对把矛盾逼到”β=1/4 且 J_F 几乎必然为零”的刚性情形，输运不等式到此取等、无法继续。第 6 节证明此时 k=3/4 下 J_F≡0 等价于 | q_F+1/4 | ²=1/4，即前 Schwarz 量满足一个下调和型不等式，其在固定点的值随屏障区域 ε→0 而被迫无界，与 u(i/2) 有限矛盾。没有这一步，定理只能得到 β≤1/4。） |
问 6：谁会用这个结果？
（答：直接用户是单叶函数与共形映射社区：B_b 谱的任何一点定位都反馈到 Carleson–Jones 系数问题；由 Makarov 比较定理，无界谱 = max(有界谱, 3p-1)，本文在有界谱负指数端给出的严格间隙也修正了数值工作者对整条谱曲线的预期——Kraetzer 抛物线不再是可引用的猜测。）
总评
这是把一个悬置近三十年的数值猜测第一次钉进严格数学的工作，且经 Lean 形式化，分量扎实；最大风险在于严格配对与输运环节的测度论细节虽逻辑自洽但极精密，未经独立人类证明复现之前，引用范围应守住已形式化的主定理本身。