💻 computer science

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

Este artigo apresenta uma formalização em Lean 4 da integral de Dirichlet e suas aplicações, incluindo a fórmula de Lobachevsky, empregando uma estratégia que utiliza a função sinc ao quadrado absolutamente integrável e a densidade de polinômios de cosseno para lidar rigorosamente com a convergência condicional e derivar diversas identidades de integrais trigonométricas.

Autores originais: Daniel Goldberg, Antoine Vinciguerra

Publicado 2026-08-27

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Daniel Goldberg, Antoine Vinciguerra

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

No vasto cenário da matemática, existe um canto silencioso dedicado ao estudo de como as coisas se somam ao longo do tempo, particularmente quando essas coisas oscilam para frente e para trás. Este é o domínio da análise real, onde matemáticos examinam o comportamento de funções que mudam continuamente. Um dos enigmas mais famosos neste campo envolve uma curva específica que sobe e desce como uma onda, diminuindo cada vez mais à medida que se estende em direção ao infinito. A questão é simples de enunciar, mas difícil de resolver: se você somar a área sob esta curva oscilante desde o início até o ponto mais distante que você possa imaginar, qual o total que você obtém? Por mais de um século, os matemáticos souberam a resposta, mas prová-la rigorosamente sem fazer suposições ocultas sempre foi uma tarefa delicada. Isso ocorre porque a curva não se estabiliza rápido o suficiente para que as regras padrão de adição se apliquem diretamente; ela depende de um cancelamento preciso de áreas positivas e negativas para atingir uma soma finita. Compreender esse comportamento é crucial não apenas para a matemática pura, mas também para a tecnologia que sustenta a comunicação moderna, pois esses mesmos padrões oscilantes são usados para reconstruir sinais e imagens a partir de dados brutos.

Recentemente, dois pesquisadores, Daniel Goldberg e Antoine Vinciguerra, decidiram enfrentar este problema clássico usando um programa de computador projetado para verificar provas matemáticas com certeza absoluta. Eles não apenas escreveram a solução; eles construíram um argumento lógico completo, passo a passo, dentro de um sistema de software chamado Lean 4, que atua como um auditor incansável que se recusa a aceitar um único passo, a menos que este seja justificado pelas regras da lógica. O objetivo deles era formalizar a integral de Dirichlet, o nome dado ao cálculo dessa área oscilante específica, e mostrar como ela se conecta a um conjunto mais amplo de regras para integrar funções periódicas. O desafio enfrentado foi que a maneira padrão como os computadores lidam com cálculos de área, conhecida como integral de Lebesgue, não pode processar diretamente esta curva em particular porque o tamanho total de suas oscilações é infinito, embora a área líquida seja finita. Para contornar isso, os pesquisadores tiveram que encontrar um desvio inteligente que evitasse o problema do infinito, mas ainda assim levasse à resposta correta.

Em vez de tentar forçar o computador a aceitar a curva oscilante original diretamente, a equipe primeiro olhou para uma versão modificada dela, onde a curva era elevada ao quadrado. Esta versão ao quadrado comporta-se muito melhor; sua área total é finita e bem comportada, permitindo que o computador a calcule usando métodos padrão. Os pesquisadores então provaram uma relação específica entre a área sob a curva oscilante original e a área sob esta versão ao quadrado. Ao calcular a área da curva ao quadrado primeiro, eles puderam matematicamente transferir esse resultado de volta para o problema original. Essa abordagem permitiu-lhes contornar as dificuldades da convergência condicional, onde a ordem da adição importa, e chegar ao famoso resultado de que a área total é exatamente metade do número pi. Isso não foi um palpite ou uma simulação; foi uma prova rigorosa de que o limite da área, conforme o limite se desloca cada vez mais para longe, converge para este valor específico.

Tendo resolvido o enigma principal, a equipe usou suas novas ferramentas para explorar o que mais poderia ser derivado dele. Eles mostraram como esta integral atua como um filtro que pode transformar uma onda suave e contínua em um salto abrupto, semelhante a um degrau, um comportamento fundamental para a forma como os sinais digitais são processados. Eles também descobriram e provaram uma coleção de outras identidades envolvendo produtos dessas funções oscilantes, mostrando como diferentes frequências interagem quando multiplicadas. Esses resultados não são apenas curiosidades abstratas; eles fornecem a base matemática para entender como os sinais podem ser reconstruídos a partir de amostras, um conceito central ao teorema de amostragem de Shannon usado no processamento de áudio e imagem digitais. Os pesquisadores demonstraram que, ao compreender o comportamento dessas integrais específicas, é possível derivar fórmulas precisas para como diferentes padrões de ondas se combinam e se cancelam mutuamente.

A conquista final e talvez a mais surpreendente do trabalho deles foi a formalização de uma fórmula descoberta por Nikolai Lobachevsky, um matemático mais conhecido pelo seu trabalho em geometria não euclidiana. Lobachevsky havia encontrado uma regra que permite que a área sob uma curva oscilante multiplicada por um padrão repetitivo seja calculada observando apenas uma pequena fatia desse padrão. Os pesquisadores provaram que essa regra é verdadeira para qualquer função contínua e repetitiva que possua um tipo específico de simetria, usando o computador para verificar que a soma infinita das oscilações pode ser reduzida a um cálculo simples sobre um intervalo curto. Eles alcançaram isso ao mostrar que qualquer função repetitiva desse tipo pode ser aproximada de perto por uma soma de ondas de cosseno simples e, como a regra funciona para cada onda individual, deve funcionar para toda a função. Isso fornece uma prova verificada por máquina de uma identidade geral que anteriormente só era compreendida através da intuição humana e de métodos tradicionais de papel e lápis.

O trabalho de Goldberg e Vinciguerra demonstra que mesmo verdades matemáticas centenárias podem beneficiar-se da precisão da verificação por computador moderna. Ao decompor o problema em partes gerenciáveis e navegar pelos obstáculos que confundem os métodos de integração padrão, eles criaram uma base sólida para pesquisas futuras em processamento de sinais e análise harmônica. A formalização deles confirma que a integral de Dirichlet é, de fato, o limite das áreas sobre intervalos limitados, e estabelece um arcabouço confiável para a fórmula de Lobachevsky. Esta conquista sugere que abordagens rigorosas semelhantes poderiam ser aplicadas a versões mais complexas destas integrais, potencialmente levando a novos insights sobre como entendemos as estruturas matemáticas que governam o mundo físico. O artigo é um testemunho do poder de combinar o profundo insight matemático com a lógica implacável da verificação por computador, transformando um enigma clássico em um fato verificado.

Resumo Técnico: Do Integral de Dirichlet à Fórmula de Lobachevsky

Enunciado do Problema
O artigo aborda a formalização do integral de Dirichlet, $\lim_{T \to +\infty} \int_0^T \frac{\sin t}{t} dt = \frac{\pi}{2}$ , dentro do assistente de prova Lean 4, utilizando a biblioteca Mathlib. O desafio primordial reside na natureza da função integrando, a função $\text{sinc}$ ( $\sin t / t$ ), que não é integrável no sentido de Lebesgue no semirreto positivo porque não é absolutamente integrável. Na prática matemática padrão, a notação $\int_0^{+\infty} \text{sinc}(t) dt$ é utilizada de forma imprecisa, mas em sistemas formais como o Mathlib, o integral de Bochner de uma função não integrável é definido como zero. Consequentemente, uma formalização direta do valor do integral é impossível; em vez disso, o problema deve ser formulado como a convergência de integrais truncadas. Além disso, provas clássicas que dependem do "truque de Feynman" (introduzir um fator exponencial $e^{-at}$ e tomar o limite $a \to 0^+$ ) enfrentam obstruções formais: justificar a troca de limites exige estimativas de cauda uniformes que são difíceis de coordenar dentro do arcabouço formal de convergência condicional.

Metodologia
Os autores adotam uma estratégia de prova que contorna as dificuldades da convergência condicional ao rotear o processo através da função $\text{sinc}^2$ , que é absolutamente integrável.

Avaliação de $\text{sinc}^2$ : A formalização estabelece primeiro que $\text{sinc}^2(t)$ é integrável no sentido de Lebesgue em $(0, \infty)$ . Ela avalia o integral $\int_0^\infty \text{sinc}^2(t) dt$ introduzindo uma função auxiliar $I(x) = \int_0^\infty e^{-xt} \text{sinc}^2(t) dt$ . Ao derivar sob o sinal do integral duas vezes, os autores derivam uma expressão de forma fechada para $I(x)$ e tomam o limite conforme $x \to 0^+$ usando o Teorema da Convergência Dominada (TCD), que é válido aqui porque $\text{sinc}^2$ é absolutamente integrável.
Recuperação do Integral de Dirichlet: O valor do integral de Dirichlet é recuperado via uma identidade que relaciona os integrais truncados de $\text{sinc}$ e $\text{sinc}^2$ . Usando integração por partes, os autores provam que para qualquer $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)$
Conforme $T \to \infty$ , o termo de fronteira desaparece, permitindo que o limite do integral de $\text{sinc}$ seja igualado ao limite do integral de $\text{sinc}^2$ .
Estrutura Formal: A formalização separa estritamente os conceitos de integração de Lebesgue (usada para $\text{sinc}^2$ ) e o limite de integrais truncadas (usado para $\text{sinc}$ ). A convergência é expressa usando os filtros Tendsto e atTop do Lean.

Contribuições e Resultados Principais
O artigo apresenta a formalização de três famílias interconectadas de resultados em análise real:

O Integral de Dirichlet: Os autores fornecem uma prova verificada por máquina de que o limite dos integrais truncados de $\text{sinc}(t)$ converge para $\pi/2$ . Isso é alcançado sem invocar o integral de Lebesgue da própria função não integrável.
O Corte de Dirichlet e o Limite de Heaviside: A formalização deriva a convergência da primitiva normalizada $D(x) = \frac{1}{2} + \frac{1}{\pi}\int_0^x \text{sinc}(t) dt$ para a função de Heaviside. Especificamente, prova-se que $\lim_{R \to \infty} D(Rx) = H(x)$ pontualmente. Este resultado é estendido para uma fórmula de corte integral, mostrando como $D(R(a-t))$ atua como uma identidade aproximada para funções integráveis.
Identidades de Integrais Trigonométricos: Utilizando a avaliação do integral de $\text{sinc}^2$ $sinc^{2}$ , os autores formalizam diversas identidades quadráticas e bilineares, incluindo:
- $\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órmula Integral de Lobachevsky: O artigo formaliza a fórmula de Lobachevsky para funções periódicas contínuas $f$ que satisfazem $f(x+\pi)=f(x)$ e $f(\pi-x)=f(x)$ . O teorema afirma:
$\int_0^\infty \text{sinc}^2(x)f(x) dx = \int_0^{\pi/2} f(x) dx$
A prova utiliza a densidade de polinômios de cosseno no espaço de funções contínuas no círculo aditivo $\mathbb{R}/\pi\mathbb{Z}$ (um resultado disponível na análise de Fourier do Mathlib). Os autores primeiro verificam a identidade para modos de cosseno individuais e depois a estendem para funções contínuas gerais via aproximação uniforme e um argumento de contradição.

Significância e Alegações
Os autores afirmam que este trabalho fornece a primeira formalização da fórmula integral de Lobachevsky em um assistente de prova. Embora o integral de Dirichlet tenha sido formalizado anteriormente no Isabelle/HOL (por Avigad et al.) utilizando uma abordagem diferente envolvendo o teorema de Fubini e a representação de $1/x$ como um integral, este artigo reside em sua rota específica através de $\text{sinc}^2$ e sua aplicação à fórmula de Lobachevsky.

A significância do trabalho é dupla:

Metodológica: Demonstra uma estratégia robusta para lidar com integrais condicionalmente convergentes em sistemas formais, separando-os de seus equivalentes absolutamente convergentes, evitando as armadilhas da integração direta de Lebesgue para funções não integráveis.
Teórica: Faz a ponte entre a análise real clássica e as bibliotecas formais modernas, aplicando a infraestrutura de análise de Fourier do Mathlib (especificamente resultados de densidade no círculo aditivo) para provar uma identidade integral clássica que não havia sido verificada por máquina anteriormente.

O artigo conclui observando que a infraestrutura desenvolvida suporta extensões potenciais, como a formalização de fórmulas do tipo Lobachevsky para potências pares superiores da função sinc e aplicações à teoria da transformada de Laplace, embora estas sejam apresentadas como direções futuras e não como trabalho concluído.

Mais como este