结果族 082：Annular variation and dyadic absolute bounds for the triangular Hilbert transform · 学科：Real and complex analysis · 验证状态：主结果已 Lean 形式化
体检量血压，不管护士几点来量、袖带松紧如何，读数都不该爆表。数学里的”极大算子”就是这样的极限压力测试：它要求同一个控制函数，在每个点上同时压住所有可能截断选择下的读数。这篇论文证明三角 Hilbert 变换通过了这项测试，而且主结果已被计算机（Lean）逐行验证。
关键词卡片
@@M@@\int_{\varepsilon<|t|<R}F(x{+}t,y)G(x,y{+}t)\frac{dt}{t}@@，两个输入沿两个坐标方向平移后纠缠@@M@@B_*=\sup_{0<\varepsilon<R}|B_{\varepsilon,R}|@@，所有截断读数的上包络@@M@@\varepsilon@@、@@M@@R@@ 都是生硬边界，上确界同时遍历两者且可逐点选取@@M@@L^3\times L^3\to L^{3/2}@@ 的最平衡位置，正是 Thiele 问题 13 所问看个具体例子
数字版定理：@@M@@\|B_*(F,G)\|_{L^{3/2}(\mathbb R^2)}\le C\|F\|_3\|G\|_3@@，对一切复 @@M@@L^3@@ 输入成立。它远强于”每个固定截断各自有界”；由此立刻得到联合主值 @@M@@B=\lim_{\varepsilon\downarrow0,R\uparrow\infty}B_{\varepsilon,R}@@ 几乎处处且在 @@M@@L^{3/2}@@ 中存在，并解决 Thiele 问题 13 的对称点情形。
为什么值得关心
三角 Hilbert 变换是”平坦平移”情形下最缺内禀抵消机制的样本，此前三十年只算得出随尺度增长的界；本文把它压成一致常数。主定理（含截断积分与极大输出的可测性）已由 Lean 形式化，是同族三篇中率先通过机器验证者。
已 Lean 形式化
第一级台阶
导读的类比是”极限血压测试”：对象是平面上两个函数；仪器每选定一对截断端点（避开奇点的积分范围），就在每个点给出一个读数。护士几点来量、袖带松紧如何，对应端点在逐点各自挑选——极大算子把一切读数的上包络一并接管。定理说：存在一个只依赖输入大小的控制函数，在任何时候、任何松紧下都不爆表。
第二级台阶
写清对象与指标：三角 Hilbert 变换 @@M@@B_{\varepsilon,R}(F,G)(x,y)=\int_{\varepsilon<|t|<R}F(x+t,y)\,G(x,y+t)\,\frac{dt}{t}@@，两个输入沿两个坐标方向平移后与 @@M@@1/t@@ 核纠缠；极大算子 @@M@@B_*=\sup_{0<\varepsilon<R}|B_{\varepsilon,R}|@@，上确界同时遍历两个硬截断端点且可在每个点独立选取。指标 @@M@@L^3\times L^3\to L^{3/2}@@ 落在 Hölder 关系 @@M@@1/3+1/3=2/3@@ 的平衡位置，与第三个 @@M@@L^3@@ 输入配对即得对称点 @@M@@1/3+1/3+1/3=1@@。
第三级台阶
主定理陈述：存在绝对常数 @@M@@C@@，对一切复 @@M@@F,G\in L^3(\mathbb R^2)@@ 有 @@M@@\|B_*(F,G)\|_{L^{3/2}}\le C\|F\|_3\|G\|_3@@。语境是”平坦平移”——无曲率、无方向平均可借力，三十年最好结果只是随尺度范围增长的 @@M@@\sqrt{\log(R/\varepsilon)}@@ 界，且三角圈非二部、Bellman 框架明确受阻；假设里”复值、逐点自选双端点”排除了任何结构性限制。结论一手给出联合主值 @@M@@B=\lim_{\varepsilon\downarrow0,R\uparrow\infty}B_{\varepsilon,R}@@ 几乎处处与 @@M@@L^{3/2}@@ 收敛，另一手经行列式为一的变量代换给出平的与单纯形两种标量形式的一致界及最优常数相等，正面解决 Thiele 问题 13 的对称点情形。主定理（含可测性）已 Lean 形式化。
证明了三角 Hilbert 变换的逐点极大算子满足 @@M@@\|B_*(F,G)\|_{L^{3/2}}\le C\|F\|_3\|G\|_3@@，上确界取遍两个硬截断端点且可逐点选取；由此得到联合几乎处处与 @@M@@L^{3/2}@@ 主值收敛，并肯定地解决 Thiele 问题 13 的对称点情形。主结果已 Lean 形式化。
三角 Hilbert 变换 @@M@@B_{\varepsilon,R}(F,G)(x,y)=\int_{\varepsilon<|t|<R}F(x+t,y)G(x,y+t)\,\frac{\mathrm dt}{t}@@ 将两个输入沿两个坐标方向平移，是平坦平移（无曲率、无方向平均）情形下最缺少内蕴抵消机制的例子；与第三个输入配对得到的标量单纯形形式是纠缠奇异积分（entangled singular integral）的基本样本。对称点 @@M@@L^3\times L^3\times L^3@@ 估计是 Thiele 问题 13。此前 Durcik–Kovač–Thiele（2019）的幂次型抵消经循环置换与插值只给出 @@M@@\sqrt{\log(R/\varepsilon)}@@ 型、随尺度范围增长的界；带曲率或方向平均的变体依赖三角情形不具备的额外抵消。方法上的障碍同样古老：Kovač 的 Bellman 函数框架只适用于二部图，三角圈被明确列为障碍。
主定理：存在绝对常数 @@M@@C@@，对一切复 @@M@@F,G\in L^3(\mathbb R^2)@@，
@@M@@D\|B_*(F,G)\|_{L^{3/2}(\mathbb R^2)}\le C\|F\|_{L^3}\|G\|_{L^3},\qquad B_*=\sup_{0<\varepsilon<R<\infty}|B_{\varepsilon,R}(F,G)|,@@
上确界同时取遍两个有限硬截断端点。这比”每个截断各自范数有界”强得多：同一个 @@M@@L^{3/2}@@ 控制函数必须在每个点同时控制两端点的一切选取。由极大估计得联合主值 @@M@@B(F,G)=\lim_{\varepsilon\downarrow0,R\uparrow\infty}B_{\varepsilon,R}(F,G)@@ 几乎处处且在 @@M@@L^{3/2}@@ 中存在，且尾部极大振荡 @@M@@\|\sup_{\varepsilon<1/n,\,R>n}|B_{\varepsilon,R}-B|\|_{3/2}\to0@@。配对第三个 @@M@@L^3@@ 输入得标量平形式（flat form）的端点一致界 @@M@@\sup_{\varepsilon,R}|\mathcal L_{\varepsilon,R}|\le C_M\prod_v\|F_v\|_3@@；经行列式为一的变量代换，单纯形形式（simplex form）@@M@@\Lambda_{\varepsilon,R}@@ 有同样的界与联合标量主值，且两形式的最优常数相等——这肯定地解决了 Thiele 问题 13 的对称点情形。
先经变量代换 @@M@@x=-a,\ y=-b,\ t=a+b+c@@ 化到单纯形坐标，把两个输入与一个对偶输入采样到有限网格上；乘以高斯权后得到三个有限维矩阵 @@M@@W_v:H_{v+1}\to H_v@@，三个顶点空间对应采样的 @@M@@a,b,c@@ 坐标，对偶数组的两个指标恰好记录输出位置。矩阵部分建立维数无关的混合迹不等式（mixed trace inequality），把循环迹 @@M@@\tr(D_0W_0D_1W_1D_2W_2)@@ 控制为能量 @@M@@\tr((R_v^*R_v)^{3/2})@@（@@M@@R_v=[\,W_v\ \ W_{v-1}^*\,]@@ 为行星）的 Hessian 二次代价。热流部分把三个能量沿中心满足 @@M@@p_0+p_1+p_2=0@@ 的高斯中心平面积分，能量随方差增大的下降恰好控制估计带三个奇高斯窗的循环迹所需的全部代价。真正的新困难在逐点不同的截断：对偶数组的每个元素只在自己的两个尺度之间存在，于是能量在相邻开关尺度之间下降、在开关尺度处可能跳。关键估计控制跳跃绝对值之和：矩阵能量对元素的导数满足 @@M@@|(R\sqrt{R^*R})_{ij}|\le\|\mathrm{row}_iR\|_2\|\mathrm{col}_jR\|_2@@（该公式在秩改变时仍成立），高斯积分后行、列范数的乘积被一维 Hardy–Littlewood 极大函数沿切片控制，界与开关尺度的个数无关——”每个元素至多开关两次”是这里的杠杆。把跳跃与热流不等式沿尺度望远镜求和，即得允许任意输出相关掩模的耗散估计。最后，用有限菜单线性化光滑截断的有限极大值，经网格极限与有理端点穷举得光滑极大算子；其核与硬 Hilbert 核的逐点比较把估计过渡到紧支撑光滑输入的硬极大；再由密度与尾振荡消失论证推广到一切复 @@M@@L^3@@ 输入，并建立联合主值与标量推论。
主定理（含截断积分定义其上的公共满测集与极大输出的可测性）已 Lean 形式化（见合集 lean/docs/082.md 及 TriangularHilbert.lean）。族内另两篇为姊妹成果：dyadic 绝对界一文直接复用本文第二、三节的矩阵引理，环形变差一文把同一能量方法推进到全变差并重新导出本文的极大结论。按 OpenAI 官方声明，未经形式化的结果可能有问题；本文中形式化覆盖的是极大估计本身，主值收敛与标量等价等推论仍属未经形式化部分。
问 1：证明中最关键的新估计是什么？
（答：jumps 一节对能量跳变的控制。逐点自选截断意味着对偶数组每个元素只在属于自己的两个尺度之间存在，能量在相邻开关尺度之间下降、在开关尺度处可能跳。矩阵事实 @@M@@|(R\sqrt{R^*R})_{ij}|\le\|\mathrm{row}_iR\|_2\|\mathrm{col}_jR\|_2@@（在秩改变时仍成立）给出对元素的导数界，高斯积分后行、列范数之积被一维 Hardy–Littlewood 极大函数沿切片控制，界与开关尺度个数无关——”每个元素至多开关两次”是全部杠杆。没有它，逐点极大必带尺度数因子。）
问 2：混合迹不等式与热流在整台机器里各干什么？
（答：变量代换 @@M@@x=-a,y=-b,t=a+b+c@@ 化到单纯形坐标并采样成三个矩阵 @@M@@W_v@@ 后，维数无关的混合迹不等式把循环迹 @@M@@\tr(D_0W_0D_1W_1D_2W_2)@@ 控制为能量 @@M@@\tr((R_v^*R_v)^{3/2})@@（行星 @@M@@R_v=[W_v\ W_{v-1}^*]@@）的 Hessian 二次代价；热流一节把能量和沿中心满足 @@M@@p_0+p_1+p_2=0@@ 的高斯平面积分，其随方差增大的下降恰好支付带三个奇高斯窗的循环迹。跳变估计再叠加其上，沿尺度望远镜求和。）
问 3：为什么平坦情形三十年啃不动？
（答：带曲率的平移（Christ–Durcik–Roos 的 @@M@@(t,t^2)@@、Hsu–Lin 的曲线族）自带额外抵消，而他们的几何假设恰恰排除平坦曲线 @@M@@(t,t)@@；方向平均（Durcik–Roos、Lin–Slavíková）也依赖三角情形没有的机制。方法侧的老障碍是 Kovač 的 Bellman 函数框架只适用于二部图，三角圈在原文 6.2 节被点名。Durcik–Kovač–Thiele 的幂次型抵消经置换插值到对称点只剩 @@M@@\sqrt{\log(R/\varepsilon)}@@，仍随尺度范围增长。）
问 4：Lean 形式化覆盖到哪条线为止？
（答：主定理本身——含有限截断积分定义其上的公共满测集与极大输出的可测性（Lemma~finite-truncations）——已形式化（TriangularHilbert.lean）。但推论层不在覆盖内：联合主值收敛、尾部极大振荡消失、标量平/单纯形形式的等价与最优常数相等（Proposition~flat-equivalence）仍属未经形式化部分，引用时应加核验标注。）
问 5：AI 生成证明最可能出错的模式？
（答：三层极限过渡的衔接。先”有限菜单”线性化光滑截断的有限极大，再经网格极限与有理端点穷举得光滑极大算子，再与硬 Hilbert 核逐点比较过渡到紧支撑光滑输入，最后密度加尾振荡消失推广到一切复 @@M@@L^3@@。每一层的穷举是否真正覆盖”逐点自选端点”、核比较的逐点不等式在端点奇异处是否成立，是机器易含糊处；好在矩阵—热流核心已被 Lean 管住，敞口集中在推论层。）
问 6：与族内姊妹篇会不会共享同一暗伤？
（答：会共享基因：dyadic 一文直接复用本文第二、三节的矩阵引理，环形变差一文重推同一能量方法并重导极大结论。若混合迹不等式或能量跳变估计有错，三篇同时倒。本文是唯一主定理经形式化者，恰可充当公共节点的对照物——复核姊妹篇时应先对照本文的形式化陈述。）
问 7：谁会用到它？
（答：联合几乎处处与 @@M@@L^{3/2}@@ 主值直接可用于多线性奇异积分的收敛性问题；标量形式的一致界与最优常数相等回答了 Thiele 问题 13 的对称点（Grafakos 等文集第 9 节）。做纠缠奇异积分、Walsh 模型、Carleson 型算子与多线性 Hilbert 变换的时间—频率分析社群是直接用户。）
总评
族内率先通过机器验证的核心定理，把三十年只有对数增长的界压成一致常数，分量与可信度双高；剩余敞口集中在未形式化的推论层，以及三篇共用的能量机制在姊妹篇中的独立复核。