AI 中文总结
在 Lean 4 中形式化狄利克雷积分及其经典应用，通过绝对可积函数 \\(\operatorname{sinc}^2\\) 规避条件收敛积分的指数因子处理难题，推导相关积分恒等式并形式化罗巴切夫斯基积分公式。
AI 中文摘要
我们在 Lean 4 证明助手内形式化了狄利克雷积分及其若干经典应用。由于 sinc 函数在正半轴上不是勒贝格可积的，狄利克雷积分必须表示为有界区间上积分的极限。为了避免从条件收敛积分中去除指数因子的困难，我们转而使用绝对可积函数 \\(\operatorname{sinc}^2\\)。我们通过积分号下求导和控制收敛定理计算其积分，再从截断积分之间的恒等式恢复狄利克雷积分。利用这些结果，我们形式化了狄利克雷截断函数到赫维赛德函数的收敛性，并推导了若干二次和双线性三角积分恒等式。最后，我们利用 Mathlib 关于加法圆的傅里叶分析得到的余弦多项式的稠密性，形式化了满足反射对称性的连续周期函数的罗巴切夫斯基积分公式。
英文摘要
We formalize the Dirichlet integral and several of its classical applications in the Lean~4 proof assistant. Since the sinc function is not Lebesgue integrable on the positive half-line, the Dirichlet integral must be represented as the limit of integrals over bounded intervals. To avoid the difficulty of removing an exponential factor from a conditionally convergent integral, we instead pass through the absolutely integrable function \(\operatorname{sinc}^2\). We evaluate its integral by differentiation under the integral sign and dominated convergence, and then recover the Dirichlet integral from an identity between truncated integrals. Using these results, we formalize the convergence of the Dirichlet cutoff to the Heaviside function and derive several quadratic and bilinear trigonometric integral identities. Finally, we formalize Lobachevsky's integral formula for continuous periodic functions satisfying a reflection symmetry, using the density of cosine polynomials obtained from Mathlib's Fourier analysis on the additive circle.
