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

기술 요약: 디리클레 적분에서 로바쳅스키 공식까지

문제 정의
본 논문은 디리클레 적분, $\lim_{T \to +\infty} \int_0^T \frac{\sin t}{t} dt = \frac{\pi}{2}$를 Mathlib 라이브러리를 사용하여 Lean 4 증명 보조기 내에서 정형화하는 문제를 다룬다. 주요 과제는 피적분 함수인 $\text{sinc}$ 함수($\sin t / t$)의 성질에 있다. 이 함수는 양의 반직선 상에서 절대 적분 가능하지 않기 때문에 르베그 적분 가능하지 않다. 표준적인 수학적 관행에서는 $\int_0^{+\infty} \text{sinc}(t) dt$라는 표기법을 느슨하게 사용하지만, Mathlib과 같은 정형 시스템에서 비적분 가능 함수의 보흐너 적분(Bochner integral)은 0으로 정의된다. 결과적으로, 적분값 자체를 직접 정형화하는 것은 불가능하며, 대신 문제를 절단된 적분(truncated integrals)의 수렴 문제로 재구성해야 한다. 또한, "파인만 기법"(지수 인자 $e^{-at}$를 도입하고 $a \to 0^+$로 극한을 취함)에 의존하는 고전적인 증명들은 정형화 과정에서 난관에 봉착한다. 극한의 교환을 정당화하기 위해서는 조건부 수렴의 정형화된 프레임워크 내에서 조율하기 까다로운 균등 꼬리 추정치(uniform tail estimates)가 필요하기 때문이다.

방법론
저자들은 절대 적분 가능한 $\text{sont}^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)$에 대한 폐쇄형 표현(closed-form expression)을 도출하고, $\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$로 갈 때 경계항(boundary term)이 소멸하므로, $\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$가 헤비사이드 함수로 수렴함을 도출한다. 구체적으로, $\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$$
  증명은 가법 원(additive circle) $\mathbb{R}/\pi\mathbb{Z}$ 상의 연속 함수 공간에서 코사인 다항식의 밀도(Mathlib의 푸리에 해석에 존재하는 결과)를 활용한다. 저자들은 먼저 개별 코사인 모드에 대해 항등식을 검증한 후, 균등 근사와 귀류법을 통해 일반적인 연속 함수로 이를 확장한다.

의의 및 주장
저자들은 본 연구가 로바쳅스키 적분 공식을 증명 보조기에서 정형화한 첫 사례라고 주장한다. 디리클레 적분은 이전에 Isabelle/HOL(Avigad 등)에서 푸리에 정리와 $1/x$의 적분 표현을 사용하는 다른 접근 방식으로 정형화된 바 있으나, 본 논문의 기여는 $\text{sinc}^2$를 경유하는 특정한 경로와 로바쳅스키 공식으로의 적용에 있다.

본 연구의 의의는 두 가지 측면에서 두드다:

1. 방법론적: 비적분 가능 함수의 직접적인 르베그 적분 시 발생하는 함정을 피하기 위해, 조건부 수렴하는 적분을 절대 수렴하는 대응물로부터 분리함으로써 정형 시스템에서 조건부 수렴하는 적분을 다루는 견고한 전략을 보여준다.
2. 이론적: Mathlib의 푸리어 해석 인프라(특히 가법 원 상의 밀도 결과)를 적용하여, 이전에 기계적으로 검증되지 않았던 고전적 적분 항등식을 증명함으로써 고전적 실해석학과 현대적 정형 라이브러리를 연결한다.

논문은 개발된 인프라가 $\text{sinc}$ 함수의 더 높은 짝수 차수에 대한 로바쳅스키 유형의 공식 및 라플라스 변환 이론에 대한 응용을 지원할 수 있음을 언급하며 마무리되나, 이는 완료된 작업이라기보다 향후 연구 방향으로 제시되었다.