Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

Resumen Técnico: Formalización de la Desigualdad Isoperimétrica Clásica en el Caso Bidimensional

1. El Problema

El artículo aborda la desigualdad isoperimétrica en el plano euclidiano ($\mathbb{R}^2$), un resultado fundamental de la geometría y el análisis que establece una relación entre el perímetro ($L$) y el área ($A$) de una curva cerrada simple.

• Enunciado: Para cualquier curva cerrada simple de perímetro $L$ que encierra un área $A$, se cumple que:
  $$L^2 \geq 4\pi A$$
  La igualdad se alcanza si y solo si la curva es un círculo.
• Desafío: Aunque la desigualdad es conocida desde la antigüedad y existen múltiples demostraciones (Steiner, Weierstrass, etc.), las pruebas clásicas a menudo omiten detalles técnicos rigurosos, como la justificación de la conmutación de sumas infinitas e integrales, la diferenciación término a término de series de Fourier y las condiciones exactas de regularidad de la curva. El objetivo es verificar esta prueba de manera exhaustiva mediante un asistente de pruebas.

2. Metodología

El autor utiliza el asistente de pruebas Lean 4 y su biblioteca matemática Mathlib para formalizar la demostración analítica propuesta por Adolf Hurwitz en 1902. Esta aproximación es elegida por su elegancia y por reducir el problema geométrico a una desigualdad puramente analítica mediante series de Fourier.

El proceso de formalización se divide en dos fases principales:

Fase 1: Fundamentos Analíticos (Teoría de Series de Fourier)
Antes de abordar la desigualdad, se formalizan las herramientas necesarias:

• Relaciones de Ortogonalidad: Se prueban las relaciones de ortogonalidad para funciones trigonométricas ($\sin, \cos$) en el intervalo $[-\pi, \pi]$.
• Convergencia Uniforme: Se utiliza el Criterio M de Weierstrass para establecer la convergencia uniforme de las series de Fourier bajo condiciones de sumabilidad de los coeficientes ($\sum (|a_n| + |b_n|) < \infty$).
• Diferenciación Término a Término: Se formaliza la condición bajo la cual la derivada de una serie de Fourier es la serie de las derivadas de sus términos, requiriendo la convergencia uniforme de la serie derivada.
• Teorema de Parseval: Se verifica la identidad que relaciona la norma $L^2$ de la función con la norma $\ell^2$ de sus coeficientes de Fourier.
• Desigualdad de Wirtinger: Se demuestra esta desigualdad funcional (un caso especial de la desigualdad de Poincaré) utilizando el Teorema de Parseval. Establece que para una función periódica de media cero, la norma $L^2$ de la función es menor o igual a la norma $L^2$ de su derivada.

Fase 2: La Prueba de Hurwitz
Se aplica la teoría anterior a curvas cerradas simples $C^1$:

1. Parametrización: Se considera una curva $\gamma$ parametrizada por longitud de arco $L$ y se reparametriza sobre el intervalo $[0, 2\pi]$ mediante funciones $f(\theta)$ y $g(\theta)$.
2. Fórmula del Área: Se expresa el área $A$ utilizando la fórmula de la "cordillera" (shoelace formula) y el teorema de Green, transformándola en una integral de $f(\theta)g'(\theta)$.
3. Integración por Partes: Se aplica integración por partes para simplificar la expresión del área, aprovechando la periodicidad de la curva para que los términos de frontera se anulen.
4. Desigualdad AM-GM: Se utiliza la desigualdad entre la media aritmética y la media geométrica ($2uv \leq u^2 + v^2$) para acotar el área.
5. Aplicación de Wirtinger: Se asume (mediante traslación) que la media de $f$ es cero y se aplica la desigualdad de Wirtinger para acotar $\int f^2$ por $\int (f')^2$.
6. Restricción de Longitud de Arco: Se utiliza la condición de parametrización por longitud de arco ($\| \gamma' \| = 1$), lo que implica $(f')^2 + (g')^2 = (L/2\pi)^2$.
7. Conclusión: Sustituyendo estos valores, se deriva finalmente $A \leq L^2 / (4\pi)$.

3. Contribuciones Clave y Desafíos de Formalización

El artículo destaca varios desafíos técnicos superados durante la implementación en Lean 4:

• Intercambio de Sumas e Integrales: A diferencia de las pruebas de libro de texto que a menudo son vagas, Lean exige invocar explícitamente el Teorema de Convergencia Dominada (Dominated Convergence Theorem) para justificar el intercambio de la integral y la suma infinita en el Teorema de Parseval.
• Diferenciación Término a Término: Se requirió manejar cuidadosamente la convergencia uniforme de la serie de derivadas y ajustar los índices de las sumas (diferencia entre índices naturales $\mathbb{N}$ y naturales positivos $\mathbb{N}^+$) para que coincidan con las lemas de Mathlib.
• Espacios Euclídeos y Proyecciones: La representación de curvas en $\mathbb{R}^2$ se realizó utilizando EuclideanSpace R (Fin 2). Un desafío fue conectar las derivadas de las funciones de coordenadas ($x(t), y(t)$) con la derivada del vector de la curva $\gamma(t)$, utilizando propiedades de proyecciones lineales continuas (PiLp.proj).
• Convenciones de Indexación: La necesidad de convertir entre sumas indexadas por $\mathbb{N}$ (común en Mathlib) y $\mathbb{N}^+$ (natural para series de Fourier sin término constante) requirió el uso de equivalencias explícitas y reindexación de sumas.
• Estructura de la Prueba: Se definió una estructura SimpleClosedC1Curve que encapsula todas las propiedades necesarias (continuidad, derivabilidad, periodicidad, simplicidad y parametrización por longitud de arco).

4. Resultados Principales

El trabajo presenta la primera formalización completa de la prueba de Hurwitz en Lean 4. Los resultados verificados incluyen:

1. Lemas de Ortogonalidad Trigonométrica: Pruebas rigurosas de las integrales de productos de senos y cosenos.
2. Teorema de Parseval Formalizado: Validado bajo hipótesis explícitas de integrabilidad y sumabilidad.
3. Desigualdad de Wirtinger: Derivada y verificada mediante la comparación de las sumas de Parseval.
4. Teorema Principal: La desigualdad isoperimétrica $A \leq L^2/(4\pi)$ para curvas cerradas simples $C^1$ con derivada continua.

El código completo está disponible en el repositorio de GitHub del autor (https://github.com/mirajcs/IsoperimetricInequality).

5. Significado e Impacto

• Certidumbre Matemática: Proporciona una verificación máquina de un teorema clásico, eliminando cualquier ambigüedad sobre los pasos analíticos sutiles (como la diferenciación de series infinitas) que a menudo se dan por sentados en la literatura.
• Avance en Análisis Formal: Demuestra la madurez de Mathlib para manejar análisis clásico de nivel de posgrado, incluyendo teoría de Fourier, integración de Lebesgue y cálculo de variaciones.
• Estudio de Caso: Sirve como un modelo para futuras formalizaciones de resultados analíticos complejos, documentando las decisiones de diseño y los obstáculos comunes (como la gestión de índices y la convergencia).
• Futuro Trabajo: El artículo identifica áreas para futuras extensiones, como la formalización del caso de igualdad (caracterización del círculo), la generalización a curvas de menor regularidad (variación acotada) y la extensión a dimensiones superiores ($\mathbb{R}^n$).

En resumen, este trabajo no solo verifica un resultado geométrico fundamental, sino que también expande las fronteras de lo que es posible formalizar en el ecosistema Lean 4, sirviendo como un puente entre el análisis clásico y la verificación formal moderna.