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

技術要約：ディリクレ積分からロバチェフスキーの公式へ

問題提起
本論文は、Mathlibライブラリを用いたLean 4証明助手による、ディリクレ積分 $\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のような形式体系において、非可積分関数のボホナー積分はゼロと定義される。したがって、積分値の直接的な形式化は不可能であり、代わりに、切断された積分の収束として問題を構成する必要がある。さらに、「ファインマンのトリック」（指数因子 $e^{-at}$ を導入し、$a \to 0^+$ の極限を取る手法）に依拠した古典的な証明は、極限の入れ替えを正当化するために、条件収束の形式的枠組みの中で調整が困難な一様テール推定を必要とするという、形式的な障害に直面する。

手法
著者らは、$\text{sinc}^2(t)$ という絶対可積分な二乗sinc関数の経路を経由することで、条件収束の困難を回避する証明戦略を採用している。

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)$ の閉形式の表現を導出し、$\text{sinc}^2$ は絶対可積分であるため、優収束定理（DCT）を用いて $x \to 0^+$ の極限を取る。
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 フィルタを使用して表現される。

主要な貢献と結果
本論文は、実解析における3つの相互に関連する一連の結果の形式化を提示している：

• ディリクレ積分： 著者らは、$\text{sinc}(t)$ の切断された積分の極限が $\pi/2$ に収束するという、機械的に検証された証明を提供する。これは、非可積分な関数自体にルベーグ積分を適用することなく達成される。
• ディリクレ・カットオフとヘヴィサイド極限： 正規化された原始関数 $D(x) = \frac{1}{2} + \frac{1}{\pi}\int_0^x \text{sinc}(t) dt$ がヘヴィサイド関数に収束することを導出する。具体的には、$\lim_{R \to \infty} D(Rx) = H(x)$ が各点収束することを証明する。この結果は積分カットオフ公式へと拡張され、$D(R(a-t))$ が可積分関数に対する近似単位としてどのように機能するかを示す。
• 三角積分恒等式： $\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$（$f(x+\pi)=f(x)$ かつ $f(\pi-x)=f(x)$ を満たす）に対するロバチェフスキーの公式を形式化する。定理は以下の通りである：
  $$\int_0^\infty \text{sinc}^2(x)f(x) dx = \int_0^{\pi/2} f(x) dx$$
  証明には、加法的な円 $\mathbb{R}/\pi\mathbb{Z}$ 上の連続関数の空間における余弦多項式の稠密性（Mathlibのフーリエ解析にある結果）を利用する。著者らはまず、個々の余弦モードに対して恒等式を検証し、次に一様近似と背理法を用いて、これを一般的な連続関数へと拡張する。

意義と主張
著者らは、本研究が証明助手におけるロバチェフスキーの積分公式の最初の形式化であることを主張している。ディリクレ積分自体は、フービニの定理と $1/x$ の積分表示を用いた異なるアプローチによって、以前にIsabelle/HOL（Avigadらによる）で形式化されているが、本論文の貢献は、$\text{sinc}^2$ を経由するという特定の経路と、ロバチェフスキーの公式への適用にある。

本研究の意義は二重である：

1. 方法論的： 条件収束する積分を、絶対収束する対応物から分離することで、非可積分関数の直接的なルベーグ積分に伴う陥穽を回避するという、形式的体系における堅牢な戦略を示している。
2. 理論的： 実解析と現代的な形式ライブラリを橋渡しし、Mathlibのフーリエ解析のインフラストラクチャ（特に加法的な円上の稠密性の結果）を適用して、これまで機械的に検証されていなかった古典的な積分恒等式を証明している。

論文の結びとして、開発されたインフラストラクチャは、$\text{sinc}$ 関数の高次の偶数乗に関するロバチェフスキー型の公式や、ラプラス変換論への応用といった潜在的な拡張をサポートしていることが述べられているが、これらは完了した作業ではなく、将来の方向性として提示されている。