Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

제시된 논문 "Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case"는 Lean 4 증명 보조 도구와 그 수학 라이브러리인 Mathlib를 사용하여 2 차원 평면에서의 고전적인 **등주 부등식 (Isoperimetric Inequality)**을 Adolf Hurwitz 의 해석학적 접근법을 통해 완전히 형식화 (Formalization) 한 연구입니다.

이 논문의 주요 내용을 문제 정의, 방법론, 핵심 기여, 결과, 그리고 의의로 나누어 상세히 요약하면 다음과 같습니다.

1. 문제 정의 (The Problem)

• 등주 문제: 주어진 둘레 (Perimeter, $L$) 를 가진 평면 도형 중 어떤 도형이 가장 큰 넓이 (Area, $A$) 를 가지는가?
• 등주 부등식: 임의의 단순 닫힌 곡선 $C$에 대해 $L^2 \ge 4\pi A$가 성립하며, 등호는 $C$가 원일 때만 성립한다.
• 형식화의 필요성: 기존 교과서의 증명은 무한급수와 적분의 교환, 항별 미분, 곡선의 정밀한 규칙성 (Regularity) 조건 등 기술적인 세부 사항을 간과하거나 직관적으로 넘기는 경우가 많습니다. 이 논문은 이러한 모든 논리적 단계를 기계가 검증할 수 있는 명확한 논리 언어로 재구성하여 증명의 정확성을 보장하고자 합니다.

2. 방법론 (Methodology)

논문의 형식화는 크게 두 단계로 진행되었습니다.

1 단계: 푸리에 해석학의 기초 확립

Hurwitz 의 증명을 위해 필요한 해석학적 도구들을 Mathlib 에 구축했습니다.

• 직교성 (Orthogonality): $[-\pi, \pi]$ 구간에서 삼각함수 ($\sin, \cos$) 의 직교 관계를 증명했습니다.
• 파세발의 정리 (Parseval's Theorem): 함수의 $L^2$ 노름과 푸리에 계수의 $\ell^2$ 노름 사이의 등식을 증명했습니다. 이를 위해 급수와 적분의 교환 (Dominated Convergence Theorem 활용) 을 엄격하게 정당화했습니다.
• 균등 수렴 및 미분: Weierstrass M-테스트를 사용하여 푸리에 급수의 부분합이 균등 수렴함을 보였고, 이를 바탕으로 **항별 미분 (Term-by-term Differentiation)**이 가능함을 증명했습니다.
• Wirtinger 부등식: 평균이 0 인 주기 함수에 대해 $\int f^2 \le \int (f')^2$가 성립함을 파세발의 정리를 통해 유도했습니다.

2 단계: Hurwitz 의 증명 수행

형식화된 도구를 사용하여 등주 부등식을 유도했습니다.

1. 곡선 재매개변수화: 길이 $L$인 단순 닫힌 $C^1$ 곡선을 호의 길이 매개변수 (Arc-length parametrization) 로 정의한 후, $[0, 2\pi]$ 구간으로 재매개변수화하여 $f(\theta), g(\theta)$를 정의했습니다.
2. 넓이 공식 유도: 그린 정리 (Shoelace formula) 를 적용하고 부분적분 (Integration by Parts) 을 사용하여 넓이 $A = \int_0^{2\pi} f(\theta)g'(\theta) d\theta$로 변환했습니다.
3. 부등식 적용:
   • AM-GM 부등식: $2fg' \le f^2 + (g')^2$를 적용하여 $A \le \frac{1}{2} \int (f^2 + (g')^2)$를 얻었습니다.
   • Wirtinger 부등식: $f$의 평균이 0 이 되도록 좌표 평행이동을 가정하고, $\int f^2 \le \int (f')^2$를 적용하여 $A \le \frac{1}{2} \int ((f')^2 + (g')^2)$로 강화했습니다.
   • 호의 길이 제약 조건: 곡선이 호의 길이 매개변수화되었으므로 $(f')^2 + (g')^2 = (L/2\pi)^2$가 성립함을 이용했습니다.
4. 최종 결론: 위 식들을 종합하여 $A \le \frac{L^2}{4\pi}$를 유도했습니다.

3. 주요 기여 및 기술적 도전 과제 (Key Contributions & Challenges)

이 논문은 단순히 정리를 증명하는 것을 넘어, Lean 4 에서 고전 해석학을 형식화하는 과정에서 발생한 여러 기술적 난제를 해결했습니다.

• 급수와 적분의 교환: 교과서에서는 간략히 넘기는 무한급수와 적분의 교환을 Mathlib 의 MeasureTheory.integral_tsum_of_summable_integral_norm (우세 수렴 정리의 일종) 을 사용하여 엄격하게 정당화했습니다.
• 항별 미분의 엄밀한 처리: 푸리에 급수의 항별 미분은 급수의 균등 수렴과 미분계수의 균등 수렴이 모두 필요하며, Lean 의 hasDerivAt_of_tendstoUniformly 정리를 적용하기 위해 인덱스 (N 과 N+) 를 맞추는 등의 세심한 조정이 필요했습니다.
• EuclideanSpace 와 좌표 투영: Mathlib 의 EuclideanSpace 구조를 사용하여 2 차원 곡선을 모델링하고, 좌표 함수의 도함수를 곡선의 도함수와 연결하는 과정에서 PiLp 투영과 체인 룰 (Chain Rule) 을 정교하게 조합했습니다.
• 인덱스 관례의 통합: 푸리에 계수는 자연수 ($N^+$) 로 인덱싱되지만, Mathlib 의 많은 정리는 자연수 ($N$) 를 기반으로 합니다. 이 불일치를 해결하기 위해 Equiv.pnatEquivNat 등을 활용한 인덱스 변환을 수행했습니다.
• 완전한 증명 구조: 등주 부등식의 증명을 5 단계로 나누어 각 단계 (넓이 공식, 부분적분, AM-GM, Wirtinger 부등식, 호의 길이 제약) 를 모듈화하여 재사용 가능한 형태로 구성했습니다.

4. 결과 (Results)

• 완전한 형식화 증명: Lean 4 환경에서 Hurwitz 의 증명을 포함한 등주 부등식 ($L^2 \ge 4\pi A$) 이 기계적으로 검증되었습니다.
• 보조 정리들의 확립: 등주 부등식 증명에 필수적인 직교성, 파세발 정리, Wirtinger 부등식, 항별 미분 정리 등이 Mathlib 스타일로 재구현 및 증명되었습니다.
• 코드 공개: 전체 형식화 코드는 GitHub (https://github.com/mirajcs/IsoperimetricInequality) 에서 공개되어 향후 연구의 기초 자료로 활용 가능합니다.

5. 의의 및 의의 (Significance)

• 수학적 확실성 (Certainty): 등주 부등식과 같은 고전적인 정리의 증명이 가진 기술적 누락 (Gap) 을 제거하고, 모든 논리적 단계를 기계가 검증함으로써 수학의 확실성을 높였습니다.
• Lean 4/Mathlib 의 능력 입증: 고등학교 및 대학원 수준의 해석학 (Fourier 급수, 적분, 미분) 을 Lean 4 로 형식화할 수 있음을 보여주었습니다. 특히 복잡한 무한급수와 적분의 상호작용을 다룰 수 있는 라이브러리의 성숙도를 입증했습니다.
• 향후 연구의 발판:
  • 현재는 $C^1$ 곡선에 국한되어 있으나, 향후 $W^{1,2}$ 공간이나 더 낮은 규칙성을 가진 곡선으로 확장 가능합니다.
  • 등호 조건 (곡선이 원일 때) 에 대한 증명과 고차원 ($R^n$) 등주 부등식으로의 일반화를 위한 기초를 마련했습니다.
  • 푸리에 계수와 실제 함수 간의 연결 (현재는 가설로 가정됨) 을 완성하여 더 자동화된 증명 체계를 구축할 수 있는 방향을 제시했습니다.

결론적으로, 이 논문은 기하학적 직관을 해석학적 도구로 변환하고, 이를 컴퓨터가 검증 가능한 논리로 재구성한 성공적인 사례로, 형식적 수학 (Formal Mathematics) 의 발전에 중요한 기여를 했습니다.