Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

Resumo Técnico: Formalização da Desigualdade Isoperimétrica Clássica no Caso Bidimensional

1. O Problema e o Objetivo
O artigo aborda a formalização completa da Desigualdade Isoperimétrica no plano euclidiano bidimensional utilizando o assistente de prova Lean 4 e sua biblioteca matemática Mathlib.
O teorema central estabelece que, para qualquer curva fechada simples $C$ no plano com perímetro $L$ e área encerrada $A$, vale a desigualdade:
$$L^2 \ge 4\pi A$$
A igualdade ocorre se e somente se a curva for um círculo. O objetivo do trabalho é verificar mecanicamente a prova analítica elegante desenvolvida por Adolf Hurwitz em 1902, garantindo que cada passo lógico seja rigorosamente verificado por máquina, eliminando lacunas comuns em provas informais (como a troca de limites, integrais e derivadas).

2. Metodologia e Estratégia de Prova
A formalização segue a abordagem analítica de Hurwitz, que reduz o problema geométrico a uma comparação de somas de coeficientes de Fourier. O processo foi dividido em duas fases principais:

• Fase 1: Fundamentos Analíticos e de Séries de Fourier
  Antes de atacar a desigualdade, os autores formalizaram as ferramentas necessárias para a prova de Hurwitz:

  • Relações de Ortogonalidade: Formalização das integrais de produtos de funções trigonométricas ($\sin$ e $\cos$) no intervalo $[-\pi, \pi]$.
  • Convergência Uniforme: Uso do Teste M de Weierstrass para garantir a convergência uniforme das somas parciais das séries de Fourier sob condições de somabilidade dos coeficientes.
  • Diferenciação Termo a Termo: Estabelecimento das condições sob as quais a derivada de uma série de Fourier pode ser calculada derivando termo a termo (requerendo a convergência uniforme da série das derivadas).
  • Teorema de Parseval: Formalização da identidade que relaciona a norma $L^2$ de uma função com a soma dos quadrados de seus coeficientes de Fourier.
  • Desigualdade de Wirtinger: Prova de que, para funções periódicas com média zero, a norma $L^2$ da função é limitada pela norma $L^2$ de sua derivada.

• Fase 2: A Prova de Hurwitz
  A prova da desigualdade isoperimétrica propriamente dita foi construída sobre os fundamentos acima:

  1. Parametrização: Considera-se uma curva fechada simples $C^1$ parametrizada por comprimento de arco. A curva é reparametrizada para o intervalo $[0, 2\pi]$.
  2. Fórmula da Área (Fórmula do Sapateiro): A área $A$ é expressa como uma integral envolvendo as coordenadas reparametrizadas $f(\theta)$ e $g(\theta)$.
  3. Integração por Partes: Simplifica a expressão da área, explorando a periodicidade da curva para eliminar termos de fronteira.
  4. Desigualdade AM-GM: Aplica-se a desigualdade aritmético-geométrica para limitar o produto $f g'$ por uma soma de quadrados.
  5. Aplicação de Wirtinger: Utiliza-se a desigualdade de Wirtinger (aplicada à coordenada $f$, assumindo média zero via translação) para substituir o termo $\int f^2$ por $\int (f')^2$.
  6. Restrição de Comprimento de Arco: A condição de parametrização por comprimento de arco implica que $(f')^2 + (g')^2$ é constante e igual a $(L/2\pi)^2$.
  7. Conclusão: A integração final resulta em $A \le L^2/(4\pi)$.

3. Contribuições Chave e Desafios de Formalização
O trabalho destaca vários desafios técnicos específicos ao traduzir a análise clássica para a teoria de tipos dependentes do Lean 4:

• Intercâmbio de Somas e Integrais: Em provas informais, a troca de soma e integral é frequentemente assumida. No Lean, foi necessário invocar explicitamente o Teorema da Convergência Dominada (Dominated Convergence Theorem) e verificar as hipóteses de somabilidade $L^1$ dos termos da série.
• Diferenciação Termo a Termo: A formalização exigiu a construção cuidadosa de lemas que conectam a convergência uniforme da série de derivadas à diferenciabilidade da função limite, lidando com deslocamentos de índices (entre índices naturais $\mathbb{N}$ e inteiros positivos $\mathbb{N}^+$).
• Espaços Euclidianos e Projeções: O uso da estrutura EuclideanSpace do Mathlib para $\mathbb{R}^n$ exigiu cuidado ao lidar com projeções de coordenadas e a relação entre derivadas de Fréchet (do vetor) e derivadas das funções escalares de coordenada.
• Convenções de Indexação: A reconciliação entre as convenções de indexação de séries de Fourier (que começam em $n=1$ para termos oscilatórios) e as ferramentas padrão do Mathlib (que frequentemente usam $\mathbb{N}$) foi um ponto de atenção constante.
• Estrutura de Dados: Definição de uma estrutura SimpleClosedC1Curve que encapsula a parametrização, a periodicidade, a simplicidade (sem auto-interseção) e a condição de derivada contínua.

4. Resultados Principais
O artigo apresenta a prova formalizada dos seguintes teoremas e lemas no Lean 4:

• Teorema de Parseval: Formalizado para séries de Fourier clássicas com hipóteses explícitas de somabilidade.
• Desigualdade de Wirtinger: Provada via Parseval, estabelecendo a relação entre a energia da função e a de sua derivada.
• Teorema Principal (Desigualdade Isoperimétrica): A prova completa de que $A \le L^2/(4\pi)$ para curvas $C^1$ fechadas simples com parametrização por comprimento de arco.
• Código Disponível: Toda a formalização está disponível publicamente no repositório GitHub do autor, servindo como um exemplo de uso avançado do Mathlib para análise real.

5. Significado e Impacto

• Rigor Matemático: O trabalho fornece um registro definitivo de que a prova de Hurwitz é logicamente correta, forçando a explicitação de todas as condições de regularidade e hipóteses analíticas que textos de livros didáticos muitas vezes omitem.
• Avanço no Mathlib: Demonstra a capacidade do ecossistema Lean 4 de lidar com análise clássica de nível de pós-graduação, incluindo teoria de Fourier, integração de Lebesgue e cálculo vetorial.
• Estudo de Caso: Serve como um guia valioso para outros pesquisadores que desejam formalizar teoremas de análise, documentando padrões de design e soluções para problemas comuns (como a troca de limites e a manipulação de somas infinitas).
• Limitações e Futuro: O trabalho atual assume a identidade de Parseval e Wirtinger como hipóteses para a função reparametrizada específica. O próximo passo natural seria derivar essas identidades diretamente da definição da curva, e futuramente generalizar para curvas com menor regularidade (variação limitada) ou para dimensões superiores.

Em suma, este artigo representa um marco na formalização de resultados clássicos da geometria e análise, validando uma prova elegante de mais de um século de antiguidade com o rigor absoluto da verificação formal.