From the Dirichlet Integral to Lobachevsky's Formula: A Formalization in Lean 4

技术摘要：从狄利克雷积分到罗巴切夫斯基公式

问题陈述
本文旨在利用 Mathlib 库在 Lean 4 证明辅助器中对狄利克雷积分（Dirichlet integral）进行形式化，即 $\lim_{T \to +\infty} \int_0^T \frac{\sin t}{t} dt = \frac{\pi}{2}$。主要的挑战在于被积函数 $\text{sinc}$ 函数（$\sin t / t$）的性质：它在正半轴上不是勒贝格可积的，因为它不是绝对可积的。在标准数学实践中，人们常随意使用符号 $\int_0^{+\infty} \text{sinc}(t) dt$，但在像 Mathlib 这样的形式化系统中，非可积函数的 Bochner 积分被定义为零。因此，直接形式化该积分的值是不可能的；相反，问题必须被构造成截断积分的收敛性问题。此外，依赖于“费曼技巧”（引入指数因子 $e^{-at}$ 并取极限 $a \to 0^+$）的经典证明面临着形式化障碍：为了证明极限交换的合理性，需要一致尾部估计（uniform tail estimates），这在处理条件收敛的形式化框架时难以协调。

方法论
作者采用了一种绕过条件收敛困难性的证明策略，通过转向绝对可积的 $\text{sinc}^2(t)$ 函数来进行路径转换。

1. 评估 $\text{sinc}^2$： 形式化过程首先确立了 $\text{sinc}^2(t)$ 在 $(0, \infty)$ 上是勒贝格可积的。作者通过引入辅助函数 $I(x) = \int_0^\infty e^{-xt} \text{sinc}^2(t) dt$ 来计算积分 $\int_0^\infty \text{sinc}^2(t) dt$。通过对积分进行两次微分，作者推导出了 $I(x)$ 的闭式表达式，并利用控制收敛定理（DCT）取 $x \to 0^+$ 的极限，由于 $\text{sinc}^2$ 是绝对可积的，此处使用 DCT 是有效的。
2. 恢复狄利克雷积分： 通过一个联系 $\text{sinc}$ 和 $\text{sinc}^2$ 截断积分的恒等式来恢复狄利克雷积分的值。利用分部积分法，作者证明了对于任何 $T > 0$：
   $$\int_0^T \text{sinc}(t) dt = \int_0^{T/2} \text{sinc}^2(t) dt + \frac{T}{2}\text{sinc}^2\left(\frac{T}{2}\right)$$
   当 $T \to \infty$ 时，边界项趋于零，从而允许将 $\text{sinc}$ 积分的极限与 $\text{sinc}^2$ 积分的极限等同起来。
3. 形式化结构： 该形式化严格区分了勒贝格积分（用于 $\text{sinc}^2$）与截断积分的极限（用于 $\text{sinc}$）的概念。收敛性通过 Lean 的 Tendsto 和 atTop 过滤器进行表达。

核心贡献与结果
本文呈现了实分析中三个相互关联的结论族的形式化：

• 狄利克雷积分： 作者提供了一个经过机器检查的证明，证明了 $\text{sinc}(t)$ 的截断积分之极限收敛于 $\pi/2$。这是在没有直接调用非可积函数本身的勒贝格积分的情况下实现的。
• 狄利克雷截断与阶跃函数极限： 形式化推导了归一化原函数 $D(x) = \frac{1}{2} + \frac{1}{\pi}\int_0^x \text{sinc}(t) dt$ 向阶跃函数（Heaviside function）的收敛性。具体而言，它证明了 $\lim_{R \to \infty} D(Rx) = H(x)$ 点收敛。该结果被扩展到一个积分截断公式，展示了 $D(R(a-t))$ 如何作为可积函数的近似单位（approximate identity）。
• 三角积分恒等式： 利用对 $\text{sinc}^2$ 积分的评估，作者形式化了若干二次和双线性恒等式，包括：
  • $\int_0^\infty \left(\frac{\sin(at)}{t}\right)^2 dt = \frac{\pi |a|}{2}$
  • $\int_0^\infty \frac{1-\cos(at)}{t^2} dt = \frac{\pi |a|}{2}$
  • $\int_0^\infty \text{sinc}(at)\text{sinc}(bt) dt = \frac{\pi}{2 \max(a,b)}$
• 罗巴切夫斯基积分公式： 本文形式化了适用于满足 $f(x+\pi)=f(x)$ 且 $f(\pi-x)=f(x)$ 的连续周期函数 $f$ 的罗巴切夫斯基积分公式。该定理指出：
  $$\int_0^\infty \text{sinc}^2(x)f(x) dx = \int_0^{\pi/2} f(x) dx$$
  证明过程利用了余弦多项式在加法圆 $\mathbb{R}/\pi\mathbb{Z}$ 上的连续函数空间中的稠密性（这是 Mathlib 中傅里叶分析的一个结果）。作者首先验证了单个余弦模的恒等式，然后通过一致逼近和矛盾论证将其推广到一般的连续函数。

意义与主张
作者声称这项工作是第一个在证明辅助器中对罗巴切夫斯基积分公式进行形式化的工作。虽然狄利克雷积分此前已在 Isabelle/HOL 中被形式化（由 Avigad 等人完成，采用了涉及 Fubini 定理和 $1/x$ 积分表示的不同方法），但本文的贡献在于其通过 $\text{sinc}^2$ 进行路径转换的具体方法，以及其在罗巴切夫斯基公式上的应用。

这项工作的意义是双重的：

1. 方法论层面： 它展示了一种在形式化系统中处理条件收敛积分的稳健策略，即通过将它们与绝对收敛的对应物分离，从而避免直接处理非可积函数的勒贝格积分所带来的陷阱。
2. 理论层面： 它通过将 Mathlib 的傅里叶分析基础设施（特别是关于加法圆的稠密性结果）应用于证明一个此前未经过机器检查的经典积分恒等式，架起了经典实分析与现代形式化库之间的桥梁。

文章最后指出，所开发的基础设施支持潜在的扩展，例如形式化针对 $\text{sinc}$ 函数更高偶次幂的罗巴切夫斯基型公式以及在拉普拉斯变换理论中的应用，尽管这些目前被视为未来的研究方向而非已完成的工作。