💻 computer science

A Formalization of the Laplace Transform and Its Inversion in Lean 4

Este artigo apresenta uma formalização em Lean 4 da transformada de Laplace e de sua inversão via um teorema do tipo Bromwich, demonstrando sua aplicação ao oscilador harmônico ao mesmo tempo em que aborda desafios analíticos e de formalização fundamentais.

Autores originais: Daniel Goldberg, Antoine Vinciguerra

Publicado 2026-08-10

📖 7 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

Imagine um mundo onde o movimento desordenado e caótico das coisas mudando ao longo do tempo — como um pêndulo oscilando, uma corda de violão vibrando ou um sinal viajando através de um fio — pudesse ser instantaneamente traduzido em um problema de álgebra limpo e estático. Esta é a magia da transformada de Laplace, uma ferramenta matemática usada por engenheiros e cientistas há mais de um século. Pense nisso como um tradutor universal que converte uma história escrita na linguagem do "tempo" (onde as coisas se movem, aceleram e desaceleram) em uma história escrita na linguagem dos "números complexos" (onde esses mesmos movimentos se tornam simples multiplicação e divisão).

Por que isso importa? Porque resolver equações sobre como as coisas mudam é frequentemente incrivelmente difícil, como tentar desatar um nó enquanto ele está sendo puxado. Mas, se você puder traduzir esse nó para uma linguagem diferente onde ele pareça apenas uma linha reta, você pode resolvê-lo facilmente e depois traduzir a resposta de volta. Este artigo é sobre a construção de um "verificador de provas" para este tradutor. Os autores não apenas escreveram as regras; eles usaram um programa de computador chamado Lean 4 para provar matematicamente, passo a passo, que o tradutor funciona exatamente como prometido, mesmo para as partes mais complicadas do processo. Eles queriam garantir que, quando usarmos essas ferramentas poderosas para projetar pontes, circuitos ou sistemas de controle, a matemática subjacente seja sólida como uma rocha e livre de erros ocultos.

O Verificador de Provas Digital

Imagine que você tem um amigo robô muito rigoroso e muito literal, que ama matemática, mas odeia adivinhações. Você diz a ele: "Aqui está uma fórmula que transforma uma linha ondulada em uma curva suave", e ele pergunta: "Tem certeza? E se a linha ondular demais? E se ela continuar para sempre?". Este artigo é o resultado de dois pesquisadores, Daniel e Antoine, ensinando a esse amigo robô tudo o que ele precisa saber sobre a transformada de Laplace.

Eles não escreveram apenas um livro didático; eles construíram uma biblioteca completa, verificada por computador, em Lean 4. Esta é uma linguagem de programação projetada especificamente para escrever provas matemáticas que um computador possa verificar quanto a erros. O objetivo deles foi pegar a transformada de Laplace — um método que transforma funções do tempo em funções de números complexos — e provar que cada regra funciona, desde as definições básicas até o complexo processo de "inversão" que transforma a resposta de volta em tempo.

O Tradutor e o Espelho Mágico

A transformada de Laplace é como um espelho mágico. Você coloca uma função $f(t)$ (que descreve algo acontecendo ao longo do tempo) no espelho, e ele reflete de volta uma nova função $(Lf)(s)$ (que descreve a mesma coisa em um mundo de "frequência").

A Viagem de Ida: O artigo prova que, se você tiver uma função que se comporta bem (não explode para o infinito rápido demais), o espelho funciona. Eles provaram as regras de como traduzir coisas simples como constantes, potências de tempo e até ondas senoidais. Por exemplo, mostraram que o espelho transforma a derivada (a taxa de variação) em uma simples multiplicação por um número $s$ , menos um valor inicial. Este é o "ingrediente secreto" que torna a resolução de equações diferenciais tão fácil.
A Viagem de Volta (Inversão): O verdadeiro desafio é trazer a resposta de volta. Como você olha para o reflexo e sabe exatamente qual era o objeto original? Isso é chamado de transformada de Laplace inversa. O artigo prova um método específico para fazer isso, conhecido como fórmula de Bromwich.

Por que Eles Não Seguiram o Caminho "Fácil"

Normalmente, matemáticos provam a fórmula de inversão usando uma técnica chamada integração de contorno complexo. Imagine desenhar um laço ao redor de uma forma em um mapa e usar um teorema especial (o Teorema do Resíduo) para contar os "tesouros" dentro dele. É uma ferramenta poderosa, mas os autores descobriram que a biblioteca do computador ainda não tinha construído suficientes dessas ferramentas de "desenhar laços no mapa".

Então, eles seguiram um caminho diferente, mais próximo do nível do solo. Em vez de desenhar laços no plano complexo, eles trataram o problema como uma integração do mundo real sobre uma linha reta. Eles dividiram o problema em partes menores e gerenciáveis:

Truncamento: Eles fingiram que a linha infinita era apenas um segmento curto e finito de $-T$ a $T$ .
A Função Sinc: À medida que tornavam esse segmento cada vez mais longo, um padrão específico emergia envolvendo uma função chamada sinc (que se parece com uma onda que vai diminuindo cada vez mais).
A Integral de Dirichlet: Eles confiaram em um fato famoso e já provado sobre a área sob esta onda sinc (a integral de Dirichlet) para mostrar que, conforme o segmento se torna infinitamente longo, o resultado reconstrói perfeitamente a função original.

Essa abordagem foi mais difícil de configurar, mas mais segura para o computador verificar, porque dependia do cálculo de números reais, do qual o computador já era muito bom.

O Teste do Pêndulo Oscilante

Para provar que seu sistema realmente funciona, eles não apenas checaram matemática abstrata; eles resolveram um problema clássico de física: o oscilador harmônico. Esta é a matemática por trás de um pêndulo oscilante ou de uma mola saltitando para cima e para baixo.

A Configuração: Eles definiram uma mola que começa em repouso, mas recebe um empurrão rápido, descrita pela equação $y''(t) + \omega^2 y(t) = 0$ .
A Tradução: Eles alimentaram essa equação no seu tradutor de Laplace verificado por computador.
O Resultado: O computador converteu com sucesso a equação diferencial bagunçada em uma simples equação algébrica: $(s^2 + \omega^2)Y(s) = \omega$ .
A Solução: Resolver para $Y(s)$ deu a eles $\frac{\omega}{s^2 + \omega^2}$ .
A Verificação: O computador então checou sua própria biblioteca e confirmou que este resultado específico é exatamente a transformada de Laplace de $\sin(\omega t)$ .

Isso foi um grande sucesso. Significou que o computador não apenas calculou a resposta; ele provou que a resposta é, de fato, uma onda senoidal, coincidindo com o que físicos humanos sabem há séculos, mas com um nível de certeza que não deixa margem para erro humano.

As Regras Estritas do Jogo

O artigo é também uma lição sobre o quão cuidadoso você precisa ser quando para de adivinhar e começa a provar. Os autores destacam vários "detalhes traiçoeiros" que frequentemente são varridos para debaixo do tapete nos livros didáticos:

O Infinito é Complicado: Você não pode simplesmente assumir que uma integral vai ao infinito. A prova teve que declarar explicitamente que a função deve decair rápido o suficiente para que a "cauda" da integral desapareça.
Os Casos Limítrofes: Ao fazer a matemática, existem pontos específicos (como $t=0$ ) onde as regras mudam. O computador os forçou a serem precisos sobre exatamente onde a função é definida e contínos.
Troca de Ordem: Na prova de inversão, eles tiveram que trocar a ordem de duas integrais. Na matemática casual, você poderia apenas fazer isso. Em sua prova formal, eles tiveram que provar rigorosamente que a "área" sob a superfície combinada era finita antes de terem permissão para trocar a ordem.

A Conclusão

Este artigo é um marco na verificação formal. Ele não descobre uma nova lei da física ou inventa um novo tipo de onda. Em vez disso, constrói uma fortaleza de certeza em torno de uma ferramenta que já é amplamente utilizada. Ao traduzir a transformada de Laplace e sua inversão para uma linguagem que um computador pode verificar, os autores criaram um padrão de referência.

Eles provaram que o "espelho mágico" funciona, desde que você siga as regras estritas sobre como a função se comporta no infinito e no início. Eles mostraram que o caminho para a resposta envolve uma lógica cuidadosa, passo a passo, em vez de atalhos. Para qualquer pessoa que esteja construindo a próxima geração de softwares que dependem dessas ferramentas matemáticas, este trabalho garante que a base não seja apenas forte, mas inquebrável. O exemplo do oscilador harmônico serve como o selo final de aprovação: o computador concorda com o humano e, pela primeira vez, o computador assinou a prova.

Resumo Técnico: Uma Formalização da Transformada de Laplace e Sua Inversão em Lean 4

Enunciado do Problema
O artigo aborda a formalização da transformada de Laplace e sua inversão dentro do provador de teoremas Lean 4, utilizando especificamente a biblioteca mathlib. Embora a transformada de Laplace seja uma ferramenta padrão na matemática aplicada para converter equações diferenciais lineares em equações algébricas, sua formalização rigorosa apresenta desafios significativos. Estes incluem o tratamento de funções de valores complexos, o gerenciamento de integrais impróprias (limites de integrais truncadas versus integrais de Lebesgue) e a prova do teorema de inversão sem depender da integração de contorno complexo e dos teoremas de resíduos, que ainda não estão suficientemente desenvolvidos na atual biblioteca Lean 4.

Metodologia
Os autores adotam uma abordagem de teoria da medida fundamentada no arcabouço da integral de Bochner disponível no mathlib. O desenvolvimento procede através de várias escolhas metodológicas fundamentais:

Construção de Núcleo Abstrato: A transformada é primeiro definida em um cenário geral sobre uma álgebra de norma completa $E$ usando um núcleo $e^{-L(e,p)}$ . Esta camada abstrata isola as propriedades algébricas do núcleo exponencial das escolhas de medida específicas.
Especialização para Funções de Valores Reais: A construção é especializada para funções de valores complexos na reta real. Os autores utilizam duas representações:
- Uma abordagem de medida mapeada, projetando a medida de Lebesgue em $[0, \infty)$ para o eixo real dentro de $\mathbb{C}$ , usada primariamente para o teorema de inversão.
- Uma abordagem de integral de conjunto direto sobre $(0, \infty)$ , usada para regras operacionais e o exemplo do oscilador harmônico.
Tratamento de Integrais Impróprias: A formalização trata explicitamente a transformada de Laplace como um limite de integrais truncadas (sobre $(0, T]$ ) em vez de uma notação direta de integral imprópria. Esta distinção é crucial para aplicar corretamente o Teorema da Convergência Dominada dentro do arcabouço do Lean.
Inversão de Variável Real: Em vez de utilizar a prova padrão de análise complexa envolvendo deformação de contorno e o Teorema de Resíduos, os autores provam o teorema de inversão utilizando integração de variável real. Ao parametrizar o contorno de Bromwich como $s = \gamma + ir$ $s = γ + i r$ , a integral de linha vertical é convertida em uma integral sobre $r \in \mathbb{R}$ $r \in R$ . A prova então baseia-se em:
- O Teorema de Fubini para trocar a ordem de integração.
- A integral de Dirichlet (formalizada em um módulo separado [9]) para lidar com o núcleo oscilatório $\frac{\sin(T(t-a))}{t-a}$ .
- Integração por partes e propriedades da primitiva da integral de Dirichlet para mostrar a convergência pontual para a função original.

Principais Contribuições
O artigo apresenta quatro contribuições principais para a comunidade de matemática formal:

Formalização de Transformada Generalizada: Uma definição do núcleo e da transformada de Laplace em uma álgebra de norma completa, incluindo provas de leis escalares e aditivas.
Regras Operacionais e Convergência: Uma formalização da transformada como uma integral de Bochner sobre o semieixo positivo. Os autores provam a convergência de transformadas truncadas e estabelecem fórmulas de forma fechada para constantes, potências, exponenciais, derivadas (incluindo derivadas iteradas), funções trigonométricas (seno e cosseno) e escala. Estas provas são conduzidas sob suposições explícitas de integrabilidade e decaimento.
Teorema de Inversão do Tipo Bromwich: Uma prova formal de que a transformada inversa recupera uma função diferenciável $f(t)$ em cada ponto de um conjunto prescrito $S \subset (0, \infty)$ . Esta prova utiliza a integral de Dirichlet formalizada e evita a integração de contorno complexo, baseando-se em integrais de parâmetros reais e convergência dominada.
Aplicação do Oscilador Harmônico: Uma derivação formal completa da solução no domínio de Laplace para a equação do oscilador harmônico $y''(t) + \omega^2 y(t) = 0$ com condições iniciais $y(0)=0, y'(0)=\omega$ . O teorema identifica a transformada da solução com $\frac{\omega}{s^2 + \omega^2}$ , verificando explicitamente todas as hipóteses analíticas (regularidade, integrabilidade, decaimento) usualmente suprimidas em derivações de livros didáticos.

Resultados
O desenvolvimento formal consiste em aproximadamente 2.900 linhas de código Lean distribuídas em quatro arquivos fonte. Resultados principais incluem:

Teorema RealLaplaceTransformIs: Desdobra a construção abstrata na forma integral familiar.
Teorema IsInverseLaplace: Estabelece a convergência pontual da transformada inversa para a função original $f(t)$ sob condições de continuidade, diferenciabilidade e integrabilidade de $f(t)e^{-\gamma t}$ e de sua derivada.
Teorema harmonic_oscillator_laplace_eq: Prova que a transformada de Laplace de uma função que satisfaz a equação do oscilador harmônico é igual à transformada de $\sin(\omega t)$ .

Significância e Escopo
Os autores posicionam este trabalho como um passo fundamental na formalização da análise aplicada. A significância reside em:

Preenchimento da Lacuna: Fornecer um teorema de inversão funcional em Lean 4 sem esperar pelo desenvolvimento de uma teoria completa de resíduos complexos.
Hipóteses Explícitas: A formalização expõe condições analíticas (como decaimento de fronteira e integrabilidade de derivadas ponderadas) que são frequentemente implícitas em tratamentos clássicos, garantindo a correção rigorosa.
Arquitetura Modular: A separação do núcleo abstrato, a especialização para o eixo real e os exemplos de aplicação cria uma estrutura reutilizável para desenvolvimentos futuros.

O artigo conclui observando que, embora a convolução e outras regras operacionais sejam os próximos passos naturais, elas requerem um tratamento cuidadoso e não são cobertas neste manuscrito. O trabalho é apresentado como uma formalização específica da transformada direta, do teorema de inversão e de uma aplicação canônica, em vez de uma biblioteca abrangente de todas as propriedades da transformada de Laplace.