💻 computer science

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

Este artículo presenta una formalización en Lean 4 de la transformada de Laplace y su inversión mediante un teorema de tipo Bromwich, demostrando su aplicación al oscilador armónico al tiempo que aborda desafíos analíticos y de formalización clave.

Autores originales: Daniel Goldberg, Antoine Vinciguerra

Publicado 2026-08-10

📖 7 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Daniel Goldberg, Antoine Vinciguerra

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina un mundo donde el movimiento desordenado y caótico de las cosas que cambian con el tiempo —como un péndulo oscilante, la cuerda vibrante de una guitarra o una señal viajando a través de un cable— pudiera traducirse instantáneamente en un problema de álgebra limpio y estático. Esta es la magia de la transformada de Laplace, una herramienta matemática utilizada por ingenieros y científicos durante más de un siglo. Piensa en ella como un traductor universal que convierte una historia escrita en el lenguaje del "tiempo" (donde las cosas se mueven, aceleran y desaceleran) en una historia escrita en el lenguaje de los "números complejos" (donde esos mismos movimientos se convierten en simples multiplicaciones y divisiones).

¿Por qué es esto importante? Porque resolver ecuaciones sobre cómo cambian las cosas suele ser increíblemente difícil, como intentar desenredar un nudo mientras este es tirado. Pero si puedes traducir ese nudo a un lenguaje diferente donde simplemente parece una línea recta, puedes resolverlo fácilmente y luego traducir la respuesta de vuelta. Este artículo trata sobre la construcción de un "verificador de pruebas" para este traductor. Los autores no se limitaron a escribir las reglas; utilizaron un programa informático llamado Lean 4 para demostrar matemáticamente, paso a paso, que el traductor funciona exactamente como promete, incluso en las partes más complicadas del proceso. Querían asegurarse de que cuando usamos estas poderosas herramientas para diseñar puentes, circuitos o sistemas de control, la matemática subyacente sea sólida como una roca y esté libre de errores ocultos.

El Verificador de Pruebas Digital

Imagina que tienes un amigo robot muy estricto y muy literal que ama las matemáticas pero odia adivinar. Le dices: "Aquí hay una fórmula que convierte una línea ondulada en una curva suave", y él pregunta: "¿Estás seguro? ¿Qué pasa si la línea ondula demasiado? ¿Qué pasa si continúa para siempre?". Este artículo es el resultado de dos investigadores, Daniel y Antoine, enseñando a ese amigo robot todo lo que necesita saber sobre la transformada de Laplace.

No se limitaron a escribir un libro de texto; construyeron una biblioteca completa verificada por computadora en Lean 4. Este es un lenguaje de programación diseñado específicamente para escribir demostraciones matemáticas que una computadora pueda verificar en busca de errores. Su objetivo fue tomar la transformada de Laplace —un método que convierte funciones del tiempo en funciones de números complejos— y demostrar que cada una de sus reglas funciona, desde las definiciones básicas hasta el complejo proceso de "inversión" que devuelve la respuesta al tiempo.

El Traductor y el Espejo Mágico

La transformada de Laplace es como un espejo mágico. Introduces una función $f(t)$ (que describe algo que sucede a lo largo del tiempo) en el espejo, y este te devuelve una nueva función $(Lf)(s)$ (que describe lo mismo en un mundo de "frecuencia").

El Viaje de Ida: El artículo demuestra que si tienes una función que se comporta bien (no explota hacia el infinito demasiado rápido), el espejo funciona. Demostraron las reglas de cómo traducir cosas simples como constantes, potencias del tiempo e incluso ondas sinusoidales. Por ejemplo, demostraron que el espejo convierte la derivada (la tasa de cambio) en una simple multiplicación por un número $s$ , menos un valor inicial. Esta es la "fórmula secreta" que hace que resolver ecuaciones diferenciales sea tan fácil.
El Viaje de Regreso (Inversión): El verdadero desafío es recuperar la respuesta. ¿Cómo miras el reflejo y sabes exactamente qué era el objeto original? Esto se llama la transformada de Laplace inversa. El artículo demuestra un método específico para hacer esto, conocido como la fórmula de Bromwich.

Por qué no tomaron el camino "fácil"

Normalmente, los matemáticos demuestran la fórmula de inversión utilizando una técnica llamada integración de contorno complejo. Imagina dibujar un bucle alrededor de una forma en un mapa y usar un teorema especial (el Teorema de los Residuos) para contar los "tesoros" dentro. Es una herramienta poderosa, pero los autores descubrieron que la biblioteca de la computadora aún no tenía suficientes de estas herramientas de "dibujo de mapas" integradas.

Así que tomaron un camino diferente, más a nivel del suelo. En lugar de dibujar bucles en el plano complejo, trataron el problema como una integración del mundo real sobre una línea recta. Descompusieron el problema en piezas más pequeñas y manejables:

Truncamiento: Fingieron que la línea infinita era solo un segmento corto y finito de $-T$ a $T$ .
La Función Sinc: A medida que hacían este segmento cada vez más largo, surgía un patrón específico que involucraba una función llamada sinc (que parece una onda que se hace cada vez más pequeña).
La Integral de Dirichlet: Se apoyaron en un hecho famoso, ya demostrado, sobre el área bajo esta onda sinc (la integral de Dirichlet) para mostrar que, a medida que el segmento se vuelve infinitamente largo, el resultado reconstruye perfectamente la función original.

Este enfoque fue más difícil de configurar pero más seguro para la verificación de la computadora porque dependía del cálculo de números reales, en el cual la computadora ya era muy buena.

La Prueba del Péndulo Oscilante

Para demostrar que su sistema realmente funciona, no solo verificaron matemáticas abstractas; resolvieron un problema clásico de física: el oscilador armónico. Esta es la matemática detrás de un péndulo oscilante o un resorte rebotando arriba y abajo.

La Configuración: Definieron un resorte que parte del reposo pero recibe un empujón rápido, descrito por la ecuación $y''(t) + \omega^2 y(t) = 0$ .
La Traducción: Introdujeron esta ecuación en su traductor de Laplace verificado por computadora.
El Resultado: La computadora convirtió con éxito esta desordenada ecuación diferencial en una simple ecuación algebraica: $(s^2 + \omega^2)Y(s) = \omega$ .
La Solución: Resolver para $Y(s)$ les dio $\frac{\omega}{s^2 + \omega^2}$ .
La Verificación: La computadora luego revisó su propia biblioteca y confirmó que este resultado específico es exactamente la transformada de Laplace de $\sin(\omega t)$ .

Esto fue un gran éxito. Significó que la computadora no solo calculó la respuesta, sino que demostró que la respuesta es, de hecho, una onda senoidal, coincidiendo con lo que los físicos humanos han sabido durante siglos, pero con un nivel de certeza que no deja lugar a dudas.

Las Reglas Estrictas del Juego

El artículo es también una lección sobre lo cuidadoso que hay que ser cuando dejas de adivinar y empiezas a demostrar. Los autores destacan varios "errores comunes" que a menudo se pasan por alto en los libros de texto:

El Infinito es Complicado: No puedes simplemente asumir que una integral tiende al infinito. La demostración tuvo que establecer explícitamente que la función debe decaer lo suficientemente rápido para que la "cola" de la integral desaparezca.
Los Casos Límite: Al realizar las matemáticas, existen puntos específicos (como el tiempo $t=0$ ) donde las reglas cambian. La computadora los obligó a ser precisos sobre exactamente dónde la función está definida y es continua.
Cambiar el Orden: En la demostración de la inversión, tuvieron que cambiar el orden de dos integrales. En las matemáticas casuales, podrías simplemente hacer esto. En su demostración formal, tuvieron que demostrar rigurosamente que el "área" bajo la superficie combinada era finita antes de que se les permitiera cambiar el orden.

La Conclusión Final

Este artículo es un hito en la verificación formal. No descubre una nueva ley de la física ni inventa un nuevo tipo de onda. En su lugar, construye una fortaleza de certeza alrededor de una herramienta que ya es ampliamente utilizada. Al traducir la transformada de Laplace y su inversión a un lenguaje que una computadora pueda verificar, los autores han creado un estándar de referencia.

Demostraron que el "espejo mágico" funciona, siempre y cuando se sigan las reglas estrictas sobre cómo se comporta la función en el infinito y al inicio. Mostraron que el camino hacia la respuesta implica una lógica cuidadosa, paso a paso, en lugar de atajos. Para cualquiera que construya la próxima generación de software que dependa de estas herramientas matemáticas, este trabajo asegura que la base no es solo fuerte, sino inquebrantable. El ejemplo del oscilador armónico sirve como el sello de aprobación final: la computadora está de acuerdo con el humano y, por primera vez, la computadora ha firmado la prueba.

Resumen Técnico: Una Formalización de la Transformada de Laplace y su Inversión en Lean 4

Planteamiento del Problema
El artículo aborda la formalización de la transformada de Laplace y su inversión dentro del demostrador de teoremas Lean 4, aprovechando específicamente la biblioteca mathlib. Si bien la transformada de Laplace es una herramienta estándar en la matemática aplicada para convertir ecuaciones diferenciales lineales en algebraicas, su formalización rigurosa presenta desafíos significativos. Estos incluyen el manejo de funciones con valores complejos, la gestión de integrales impropias (límites de integrales truncadas frente a la integral de Lebesgue) y la demostración del teorema de inversión sin depender de la integración de contornos complejos y los teoremas de los residuos, los cuales aún no están suficientemente desarrollados en la actual biblioteca de Lean 4.

Metodología
Los autores adoptan un enfoque de teoría de la medida fundamentado en el marco de la integral de Bochner disponible en mathlib. El desarrollo procede a través de varias elecciones metodológicas clave:

Construcción de Núcleo Abstracto: La transformada se define primero en un entorno general sobre un álgebra normada completa $E$ utilizando un núcleo $e^{-L(e,p)}$ . Esta capa abstracta aísla las propiedades algebraicas del núcleo exponencial de las elecciones de medida específicas.
Especialización a Funciones de Valores Reales: La construcción se especializa para funciones con valores complejos en la recta real. Los autores utilizan dos representaciones:
- Un enfoque de medida mapeada, que proyecta la medida de Lebesgue en $[0, \infty)$ hacia el eje real dentro de $\mathbb{C}$ , utilizado principalmente para el teorema de inversión.
- Un enfoque de integral de conjunto directo sobre $(0, \infty)$ , utilizado para las reglas operacionales y el ejemplo del oscilador armónico.
Manejo de Integrales Impropias: La formalización trata explícitamente la transformada de Laplace como un límite de integrales truncadas (sobre $(0, T]$ ) en lugar de una notación directa de integral impropia. Esta distinción es crucial para aplicar correctamente el Teorema de la Convergencia Dominada dentro del marco de Lean.
Inversión de Variable Real: En lugar de utilizar la demostración estándar de análisis complejo que involucra la deformación de contornos y el Teorema de los Residuos, los autores demuestran el teorema de inversión utilizando la integración de variable real. Al parametrizar el contorno de Bromwich como $s = \gamma + ir$ $s = γ + i r$ , la integral de la línea vertical se convierte en una integral sobre $r \in \mathbb{R}$ $r \in R$ . La demostración depende de:
- El Teorema de Fubini para intercambiar el orden de integración.
- La integral de Dirichlet (formalizada en un módulo separado [9]) para manejar el núcleo oscilatorio $\frac{\sin(T(t-a))}{t-a}$ .
- Integración por partes y las propiedades de la primitiva de la integral de Dirichlet para mostrar la convergencia puntual al la función original.

Contribuciones Clave
El artículo presenta cuatro contribcciones principales a la comunidad de matemáticas formales:

Formalización de la Transformada Generalizada: Una definición del núcleo y la transformada de Laplace en un álgebra normada completa, incluyendo demostraciones de las leyes escalar y aditiva.
Reglas Operacionales y Convergencia: Una formalización de la transformada como una integral de Bochner sobre la semirrecta positiva. Los autores demuestran la convergencia de las transformadas truncadas y establecen fórmulas de forma cerrada para constantes, potencias, exponenciales, derivadas (incluyendo derivadas iteradas), funciones trigonométricas (seno y coseno) y escalamiento. Estas demostraciones se realizan bajo supuestos explícitos de integrabilidad y decaimiento.
Teorema de Inversión de Tipo Bromwich: Una demostración formal de que la transformada inversa recupera una función diferenciable $f(t)$ en cada punto de un conjunto prescrito $S \subset (0, \infty)$ . Esta demostración utiliza la integral de Dirichlet formalizada y evita la integración de contornos complejos, basándose en integrales de parámetros reales y convergencia dominada.
Aplicación del Oscilador Armónico: Una derivación formal completa de la solución en el dominio de Laplace para la ecuación del oscilador armónico $y''(t) + \omega^2 y(t) = 0$ con condiciones iniciales $y(0)=0, y'(0)=\omega$ . El teorema identifica la transformada de la solución con $\frac{\omega}{s^2 + \omega^2}$ , verificando explícitamente todas las hipótesis analíticas (regularidad, integrabilidad, decaimiento) que suelen suprimirse en las derivaciones de los libros de texto.

Resultados
El desarrollo formal consta de aproximadamente 2,900 líneas de código en Lean distribuidas en cuatro archivos fuente. Los resultados clave incluyen:

Teorema RealLaplaceTransformIs: Descompone la construcción abstracta en la forma de integral familiar.
Teorema IsInverseLaplace: Establece la convergencia puntual de la transformada inversa a la función original $f(t)$ bajo condiciones de continuidad, diferenciabilidad e integrabilidad de $f(t)e^{-\gamma t}$ y su derivada.
Teorema harmonic_oscillator_laplace_eq: Prueba que la transformada de Laplace de una función que satisface la ecuación del oscilador armónico es igual a la transformada de $\sin(\omega t)$ .

Significancia y Alcance
Los autores posicionan este trabajo como un paso fundacional en la formalización del análisis aplicado. La significancia radica en:

Cerrar la Brecha: Proporcionar un teorema de inversión funcional en Lean 4 sin esperar al desarrollo de una teoría completa de residuos complejos.
Hipótesis Explícitas: La formalización expone las condiciones analíticas (como el decaimiento en el límite y la integrabilidad de las derivadas pesadas) que a menudo son implícitas en los tratamientos clásicos, asegurando la corrección rigurosa.
Arquitectura Modular: La separación del núcleo abstracto, la especialización en el eje real y los ejemplos de aplicación crea una estructura reutilizable para futuros desarrollos.

El artículo concluye señalando que, si bien la convolución y otras reglas operacionales son pasos naturales a seguir, requieren un tratamiento cuidadoso y no están cubiertas en este manuscrito. El trabajo se presenta como una formalización específica de la transformada directa, el teorema de inversión y una aplicación canónica, en lugar de una biblioteca exhaustiva de todas las propiedades de la transformada de Laplace.