💻 computer science

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

Cet article présente une formalisation de la transformée de Laplace et de son inversion via un théorème de type Bromwich en Lean 4, démontrant son application à l'oscillateur harmonique tout en abordant les principaux défis analytiques et de formalisation.

Auteurs originaux : Daniel Goldberg, Antoine Vinciguerra

Publié 2026-08-10

📖 8 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Daniel Goldberg, Antoine Vinciguerra

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez un monde où le mouvement désordonné et chaotique des choses qui changent au fil du temps — comme un pendule oscillant, une corde de guitare vibrant ou un signal voyageant à travers un fil — pourrait être instantanément traduit en un problème d'algèbre propre et statique. C'est la magie de la transformée de Laplace, un outil mathématique utilisé par les ingénieurs et les scientifiques depuis plus d'un siècle. Voyez cela comme un traducteur universel qui convertit un récit écrit dans la langue du « temps » (où les choses bougent, accélèrent et ralentissent) en un récit écrit dans la langue des « nombres complexes » (où ces mêmes mouvements deviennent de simples multiplications et divisions).

Pourquoi est-ce important ? Parce que résoudre des équations sur la façon dont les choses changent est souvent incroyablement difficile, comme essayer de démêler un nœud pendant qu'il est tiré. Mais si vous pouvez traduire ce nœud dans une langue différente où il ressemble simplement à une ligne droite, vous pouvez le résoudre facilement, puis retraduire la réponse. Ce document traite de la construction d'un « vérificateur de preuve » pour ce traducteur. Les auteurs n'ont pas seulement énoncé les règles ; ils ont utilisé un programme informatique appelé Lean 4 pour prouver mathématiquement, étape par étape, que le traducteur fonctionne exactement comme promis, même pour les parties les plus complexes du processus. Ils voulaient s'assurer que lorsque nous utilisons ces outils puissants pour concevoir des ponts, des circuits ou des systèmes de contrôle, les mathématiques sous-jacentes sont d'une solidité absolue et exemptes d'erreurs cachées.

Le vérificateur de preuves numérique

Imaginez que vous avez un ami robot très strict, très littéral, qui adore les mathématiques mais déteste deviner. Vous lui dites : « Voici une formule qui transforme une ligne ondulée en une courbe lisse », et il demande : « En êtes-vous sûr ? Et si la ligne ondule trop ? Et si elle continue indéfiniment ? » Ce document est le résultat de deux chercheurs, Daniel et Antoine, enseignant à ce compagnon robot tout ce dont il a besoin de savoir sur la transformée de Laplace.

Ils n'ont pas seulement écrit un manuel ; ils ont construit une bibliothèque complète, vérifiée par ordinateur, dans Lean 4. Il s'agit d'un langage de programmation conçu spécifiquement pour écrire des preuves mathématiques qu'un ordinateur peut vérifier pour détecter des erreurs. Leur objectif était de prendre la transformée de Laplace — une méthode qui transforme les fonctions du temps en fonctions de nombres complexes — et de prouver que chaque règle fonctionne, des définitions de base au processus complexe d'« inversion » qui ramène la réponse vers le temps.

Le traducteur et le miroir magique

La transformée de Laplace est comme un miroir magique. Vous placez une fonction $f(t)$ (qui décrit quelque chose se produisant au cours du temps) dans le miroir, et il vous renvoie une nouvelle fonction $(Lf)(s)$ (qui décrit la même chose dans un monde de « fréquence »).

Le voyage aller : Le document prouve que si vous avez une fonction qui se comporte bien (elle n'explose pas vers l'infini trop vite), le miroir fonctionne. Ils ont prouvé les règles de traduction pour des choses simples comme les constantes, les puissances du temps et même les ondes sinusoïdales. Par exemple, ils ont montré que le miroir transforme la dérivée (le taux de variation) en une simple multiplication par un nombre $s$ , moins une valeur initiale. C'est la « recette secrète » qui rend la résolution des équations différentielles si facile.
Le voyage de retour (Inversion) : Le véritable défi est de récupérer la réponse. Comment regarder le reflet et savoir exactement quel était l'objet original ? C'est ce qu'on appelle la transformée de Laplace inverse. Le document prouve une méthode spécifique pour faire cela, connue sous le nom de formule de Bromwich.

Pourquoi ils n'ont pas pris la voie « facile »

Habituellement, les mathématiciens prouvent la formule d'inversion en utilisant une technique appelée intégration de contour complexe. Imaginez dessiner une boucle autour d'une forme sur une carte et utiliser un théorème spécial (le théorème des résidus) pour compter les « trésors » à l'intérieur. C'est un outil puissant, mais les auteurs ont constaté que la bibliothèque de l'ordinateur ne possédait pas encore assez de ces outils de « dessin de cartes » intégrés.

Ils ont donc emprunté un chemin différent, plus proche du terrain. Au lieu de dessiner des boucles dans le plan complexe, ils ont traité le problème comme une intégration dans le monde réel sur une ligne droite. Ils ont décomposé le problème en morceaux plus petits et gérables :

Troncation : Ils ont fait comme si la ligne infinie n'était qu'un segment court et fini de $-T$ à $T$ .
La fonction Sinc : À mesure qu'ils rallongeaient ce segment, un motif spécifique émergeait impliquant une fonction appelée sinc (qui ressemble à une onde qui devient de plus en plus petite).
L'intégrale de Dirichlet : Ils se sont appuyés sur un fait célèbre, déjà prouvé, concernant l'aire sous cette onde sinc (l'intégrale de Dirichlet) pour montrer qu'à mesure que le segment devient infiniment long, le résultat reconstruit parfaitement la fonction originale.

Cette approche était plus difficile à mettre en place mais plus sûre pour la vérification par ordinateur car elle reposait sur le calcul des nombres réels, domaine dans lequel l'ordinateur est déjà très performant.

Le test du pendule oscillant

Pour prouver que leur système fonctionne réellement, ils n'ont pas seulement vérifié des mathématiques abstraites ; ils ont résolu un problème de physique classique : l'oscillateur harmonique. C'est la mathématique derrière un pendule oscillant ou un ressort qui rebondit de haut en bas.

La configuration : Ils ont défini un ressort qui part au repos mais reçoit une poussée rapide, décrite par l'équation $y''(t) + \omega^2 y(t) = 0$ .
La traduction : Ils ont injecté cette équation dans leur traducteur de Laplace vérifié par ordinateur.
Le résultat : L'ordinateur a réussi à convertir cette équation différentielle complexe en une simple équation algébrique : $(s^2 + \omega^2)Y(s) = \omega$ .
La solution : Résoudre pour $Y(s)$ leur a donné $\frac{\omega}{s^2 + \omega^2}$ .
La vérification : L'ordinateur a ensuite vérifié sa propre bibliothèque et a confirmé que ce résultat spécifique est exactement la transformée de Laplace de $\sin(\omega t)$ .

Ce fut un immense succès. Cela signifiait que l'ordinateur n'a pas seulement calculé la réponse ; il a prouvé que la réponse est bien une onde sinusoïdale, correspondant à ce que les physiciens humains savent depuis des siècles, mais avec un niveau de certitude qui ne laisse aucune place à l'erreur humaine.

Les règles strictes du jeu

Le document est également une leçon sur la prudence nécessaire lorsque l'on cesse de deviner pour commencer à prouver. Les auteurs mettent en lumière plusieurs « pièges » qui sont souvent balayés sous le tapis dans les manuels :

L'infini est délicat : On ne peut pas simplement supposer qu'une intégrale tend vers l'infini. La preuve a dû stipuler explicitement que la fonction doit décroître assez vite pour que la « queue » de l'intégrale disparaisse.
Les cas limites : Lors des calculs, il existe des points spécifiques (comme $t=0$ ) où les règles changent. L'ordinateur les a forcés à être précis sur l'endroit exact où la fonction est définie et continue.
L'inversion de l'ordre : Dans la preuve de l'inversion, ils ont dû inverser l'ordre de deux intégrales. En mathématiques informelles, on pourrait simplement faire cela. Dans leur preuve formelle, ils ont dû prouver rigoureusement que l'« aire » sous la surface combinée était finie avant de pouvoir changer l'ordre.

L'essentiel à retenir

Ce document est un jalon de la vérification formelle. Il ne découvre pas une nouvelle loi de la physique ou invente un nouveau type d'onde. Au lieu de cela, il construit un fort de certitude autour d'un outil déjà largement utilisé. En traduisant la transformée de Laplace et son inversion dans un langage qu'un ordinateur peut vérifier, les auteurs ont créé un standard de référence.

Ils ont prouvé que le « miroir magique » fonctionne, à condition de suivre les règles strictes sur le comportement de la fonction à l'infini et au départ. Ils ont montré que le chemin vers la réponse implique une logique prudente, étape par étape, plutôt que des raccourcis. Pour quiconque construit la prochaine génération de logiciels reposant sur ces outils mathématiques, ce travail garantit que la fondation n'est pas seulement solide, mais incassable. L'exemple de l'oscillateur harmonique sert de sceau d'approbation final : l'ordinateur est d'accord avec l'humain, et pour la première fois, l'ordinateur a validé la preuve.

Résumé Technique : Une Formalisation de la Transformée de Laplace et de son Inversion dans Lean 4

Énoncé du Problème
L'article traite de la formalisation de la transformée de Laplace et de son inversion au sein du prouveur de théorèmes Lean 4, en exploitant spécifiquement la bibliothèque mathlib. Bien que la transformée de Laplace soit un outil standard en mathématiques appliquées pour convertir des équations différentielles linéaires en équations algébriques, sa formalisation rigoureuse présente des défis importants. Ceux-ci incluent la gestion de fonctions à valeurs complexes, la gestion des intégrales impropres (limites d'intégrales tronquées par rapport aux intégrales de Lebesgue) et la preuve du théorème d'inversion sans dépendre de l'intégration de contours complexes et des théorèmes des résidus, qui ne sont pas encore suffisamment développés dans la bibliothèque actuelle de Lean 4.

Méthodologie
Les auteurs adoptent une approche de théorie de la mesure fondée sur le cadre de l'intégrale de Bochner disponible dans mathlib. Le développement procède à travers plusieurs choix méthodologiques clés :

Construction de Noyau Abstrait : La transformée est d'abord définie dans un cadre général sur une algèbre normée complète $E$ en utilisant un noyau $e^{-L(e,p)}$ . Cette couche abstraite isole les propriétés algébriques du noyau exponentiel des choix de mesure spécifiques.
Spécialisation aux Fonctions à Valeurs Réelles : La construction est spécialisée pour les fonctions à valeurs complexes sur la droite réelle. Les auteurs utilisent deux représentations :
- Une approche par mesure image, poussant en avant la mesure de Lebesgue sur $[0, \infty)$ vers l'axe réel dans $\mathbb{C}$ , utilisée principalement pour le théorème d'inversion.
- Une approche par intégrale d'ensemble directe sur $(0, \infty)$ , utilisée pour les règles opérationnelles et l'exemple de l'oscillateur harmonique.
Gestion des Intégrales Impropres : La formalisation traite explicitement la transformée de Laplace comme une limite d'intégrales tronquées (sur $(0, T]$ ) plutôt que comme une notation directe d'intégrale impropre. Cette distinction est cruciale pour appliquer correctement le théorème de la convergence dominée au sein du cadre Lean.
Inversion sur Variable Réelle : Au lieu d'utiliser la preuve standard d'analyse complexe impliquant la déformation de contour et le théorème des résidus, les auteurs prouvent le théorème d'inversion en utilisant l'intégration de variable réelle. En paramétrant le contour de Bromwich par $s = \gamma + ir$ $s = γ + i r$ , l'intégrale de ligne verticale est convertie en une intégrale sur $r \in \mathbb{R}$ $r \in R$ . La preuve repose ensuite sur :
- Le théorème de Fubini pour échanger l'ordre d'intégration.
- L'intégrale de Dirichlet (formalisée dans un module séparé [9]) pour gérer le noyau oscillatoire $\frac{\sin(T(t-a))}{t-a}$ .
- L'intégration par parties et les propriétés de la primitive de l'intégrale de Dirichlet pour montrer la convergence ponctuelle vers la fonction originale.

Contributions Clés
Le papier présente quatre contributions principales à la communauté des mathématiques formelles :

Formalisation de la Transformée Généralisée : Une définition du noyau et de la transformée de Laplace sur une algèbre normée complète, incluant des preuves des lois scalaires et additives.
Règles Opérationnelles et Convergence : Une formalisation de la transformée comme une intégrale de Bochner sur la demi-droite positive. Les auteurs prouvent la convergence des transformées tronquées et établissent des formules de forme fermée pour les constantes, les puissances, les exponentielles, les dérivées (y compris les dérivées itérées), les fonctions trigonométriques (sinus et cosinus) et le changement d'échelle. Ces preuves sont conduites sous des hypothèses explicites d'intégrabilité et de décroissance.
Théorème d'Inversion de Type Bromwich : Une preuve formelle que la transformée de Laplace inverse récupère une fonction dérivable $f(t)$ en chaque point d'un ensemble prescrit $S \subset (0, \infty)$ . Cette preuve utilise l'intégrale de Dirichlet formalisée et évite l'intégration de contour complexe, s'appuyant plutôt sur des intégrales de paramètres réels et la convergence dominée.
Application de l'Oscillateur Harmonique : Une dérivation formelle complète de la solution dans le domaine de Laplace pour l'équation de l'oscillateur harmonique $y''(t) + \omega^2 y(t) = 0$ avec les conditions initiales $y(0)=0, y'(0)=\omega$ . Le théorème identifie la transformée de la solution avec $\frac{\omega}{s^2 + \omega^2}$ , vérifiant explicitement toutes les hypothèses analytiques (régularité, intégrabilité, décroissance) habituellement supprimées dans les dérivations des manuels.

Résultats
Le développement formel consiste en environ 2 900 lignes de code Lean réparties sur quatre fichiers sources. Les résultats clés incluent :

Théorème RealLaplaceTransformIs : Déploie la construction abstraite vers la forme intégrale familière.
Théorème IsInverseLaplace : Établit la convergence ponctuelle de la transformée inverse vers la fonction originale $f(t)$ sous des conditions de continuité, de dérivabilité et d'intégrabilité de $f(t)e^{-\gamma t}$ et de sa dérivée.
Théorème harmonic_oscillator_laplace_eq : Prouve que la transformée de Laplace d'une fonction satisfaisant l'équation de l'oscillateur harmonique est égale à la transformée de $\sin(\omega t)$ .

Signification et Portée
Les auteurs positionnent ce travail comme une étape fondamentale dans la formalisation de l'analyse appliquée. La signification réside dans :

Combler le fossé : Fournir un théorème d'inversion fonctionnel dans Lean 4 sans attendre le développement d'une théorie complète des résidus complexes.
Hypothèses Explicites : La formalisation expose les conditions analytiques (telles que la décroissance aux limites et l'intégrabilité des dérivées pondérées) qui sont souvent implicites dans les traitements classiques, garantissant une correction rigoureuse.
Architecture Modulaire : La séparation du noyau abstrait, de la spécialisation sur l'axe réel et des exemples d'application crée une structure réutilisable pour des développements futurs.

Le papier conclut en notant que bien que la convolution et d'autres règles opérationnelles soient des étapes naturelles suivantes, elles nécessitent un traitement prudent et ne sont pas couvertes dans ce manuscrit. Le travail est présenté comme une formalisation spécifique de la transformée directe, du théorème d'inversion et d'une application canonique, plutôt que comme une bibliothèque exhaustive de toutes les propriétés de la transformée de Laplace.