💻 computer science

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

Cet article présente une formalisation dans Lean 4 de l'intégrale de Dirichlet et de ses applications, y compris la formule de Lobatchevski, en employant une stratégie qui utilise la fonction sinus cardinal au carré absolument intégrable et la densité des polynômes en cosinus pour traiter rigoureusement la convergence conditionnelle et dériver diverses identités d'intégrales trigonométriques.

Auteurs originaux : Daniel Goldberg, Antoine Vinciguerra

Publié 2026-08-27

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

Dans le vaste paysage des mathématiques, il existe un coin tranquille dédié à l'étude de la manière dont les choses s'additionnent au fil du temps, particulièrement lorsque celles-ci oscillent d'avant en arrière. C'est le domaine de l'analyse réelle, où les mathématiciens examinent le comportement de fonctions qui changent continûment. L'une des énigmes les plus célèbres de ce domaine concerne une courbe spécifique qui monte et descend comme une vague, devenant de plus en plus petite à mesure qu'elle s'étire vers l'infini. La question est simple à énoncer mais difficile à résoudre : si l'on additionne l'aire sous cette courbe oscillante, du tout début jusqu'au point le plus lointain que l'on puisse imaginer, quel total obtient-on ? Pendant plus d'un siècle, les mathématiciens ont connu la réponse, mais prouver cela rigoureusement sans faire de suppositions cachées a toujours été une tâche délicate. Cela s'explique par le fait que la courbe ne se stabilise pas assez rapidement pour que les règles standards d'addition puissent s'appliquer directement ; elle repose sur une annulation précise des aires positives et négatives pour atteindre une somme finie. Comprendre ce comportement est crucial non seulement pour les mathématiques pures, mais aussi pour la technologie qui sous-tend les communications modernes, car ces mêmes motifs oscillants sont utilisés pour reconstruire des signaux et des images à partir de données brutes.

Récemment, deux chercheurs, Daniel Goldberg et Antoine Vinciguerra, ont décidé de s'attaquer à ce problème classique à l'aide d'un programme informatique conçu pour vérifier des preuves mathématiques avec une certitude absolue. Ils n'ont pas seulement écrit la solution ; ils ont construit un argument logique complet, étape par étape, à l'intérieur d'un système logiciel appelé Lean 4, qui agit comme un auditeur infatigable refusant d'accepter la moindre étape à moins qu'elle ne soit justifiée par les règles de la logique. Leur objectif était de formaliser l'intégrale de Dirichlet, le nom donné au calcul de cette aire oscillante spécifique, et de montrer comment elle se connecte à un ensemble plus large de règles pour l'intégration de fonctions périodiques. Le défi auquel ils ont été confrontés est que la manière standard dont les ordinateurs traitent les calculs d'aire, connue sous le nom d'intégrale de Lebesgue, ne peut pas traiter directement cette courbe particulière car la taille totale de ses oscillations est infinie, bien que l'aire nette soit finie. Pour contourner cela, les chercheurs ont dû trouver un détour astucieux qui évite le problème de l'infini tout en menant à la bonne réponse.

Au lieu d'essayer de forcer l'ordinateur à accepter directement la courbe oscillante originale, l'équipe a d'abord examiné une version modifiée de celle-ci où la courbe était élevée au carré. Cette version au carré se comporte beaucoup mieux ; son aire totale est finie et bien élevée, ce qui permet à l'ordinateur de la calculer en utilisant des méthodes standards. Les chercheurs ont ensuite prouvé une relation spécifique entre l'aire sous la courbe oscillante originale et l'aire sous cette version au carré. En calculant d'abord l'aire de la courbe au carré, ils pouvaient mathématiquement transférer ce résultat vers le problème original. Cette approche leur a permis de contourner les difficultés de la convergence conditionnelle, où l'ordre de l'addition importe, et d'arriver au résultat célèbre selon lequel l'aire totale est exactement la moitié du nombre pi. Il ne s'agissait pas d'une supposition ou d'une simulation ; c'était une preuve rigoureuse que la limite de l'aire, à mesure que la frontière s'éloigne de plus en plus, converge vers cette valeur spécifique.

Ayant résolu l'énigme principale, l'équipe a utilisé ses nouveaux outils pour explorer ce qui pourrait en être dérivé. Ils ont montré comment cette intégrale agit comme un filtre capable de transformer une onde lisse et continue en un saut brusque de type échelon, un comportement fondamental dans le traitement des signaux numériques. Ils ont également découvert et prouvé une collection d'autres identités impliquant des produits de ces fonctions oscillantes, montrant comment différentes fréquences interagissent lorsqu'elles sont multipliées. Ces résultats ne sont pas de simples curiosités abstraites ; ils fournissent le fondement mathématique de la compréhension de la manière dont les signaux peuvent être reconstruits à partir d'échantillons, un concept central du théorème d'échantillonnage de Shannon utilisé dans le traitement du son et des images numériques. Les chercheurs ont démontré qu'en comprenant le comportement de ces intégrales spécifiques, on peut dériver des formules précises pour la façon dont les différents motifs d'ondes se combinent et s'annulent les uns les autres.

La réalisation finale et peut-être la plus surprenante de leur travail fut la formalisation d'une formule découverte par Nikolaï Lobatchevski, un mathématicien principalement connu pour ses travaux sur la géométrie non euclidienne. Lobatchevski avait trouvé une règle permettant de calculer l'aire sous une courbe oscillante multipliée par un motif répétitif en examinant simplement une petite tranche de ce motif. Les chercheurs ont prouvé que cette règle est vraie pour toute fonction continue et répétitive possédant un certain type de symétrie, en utilisant l'ordinateur pour vérifier que la somme infinie des oscillations peut être réduite à un calcul simple sur un intervalle court. Ils y sont parvenus en montrant que toute fonction répétitive de ce type peut être approximée de près par une somme de simples ondes cosusoïdales, et puisque la règle fonctionne pour chaque onde individuelle, elle doit fonctionner pour l'ensemble de la fonction. Cela fournit une preuve vérifiée par machine d'une identité générale qui n'avait été comprise jusqu'alors que par l'intuition humaine et les méthodes traditionnelles de papier et de crayon.

Le travail de Goldberg et Vinciguerra démontre que même les vérités mathématiques séculaires peuvent bénéficier de la précision de la vérification informatique moderne. En décomposant le problème en morceaux gérables et en contournant les obstacles qui troublent les méthodes d'intégration standards, ils ont créé un fondement solide pour la recherche future en traitement du signal et en analyse harmonique. Leur formalisation confirme que l'intégrale de Dirichlet est bien la limite des aires sur des intervalles bornés, et elle établit un cadre fiable pour la formule de Lobatchevski. Cette réussite suggère que des approches rigoureuses similaires pourraient être appliquées à des versions plus complexes de ces intégrales, menant potentiellement à de nouvelles perspectives sur la façon dont nous comprenons les structures mathématiques qui régissent le monde physique. Leur article témoigne de la puissance de la combinaison d'une profonde intuition mathématique et de la logique implacable de la vérification informatique, transformant un casse-tête classique en un fait vérifié.

Résumé technique : De l'intégrale de Dirichlet à la formule de Lobatchevski

Énoncé du problème
L'article traite de la formalisation de l'intégrale de Dirichlet, $\lim_{T \to +\infty} \int_0^T \frac{\sin t}{t} dt = \frac{\pi}{2}$ , dans l'assistant de preuve Lean 4 en utilisant la bibliothèque Mathlib. Le défi principal réside dans la nature de l'intégrande, la fonction $\text{sinc}$ ( $\sin t / t$ ), qui n'est pas intégrable au sens de Lebesgue sur la demi-droite positive car elle n'est pas absolument intégrable. Dans la pratique mathématique standard, la notation $\int_0^{+\infty} \text{sinc}(t) dt$ est utilisée de manière informelle, mais dans les systèmes formels comme Mathlib, l'intégrale de Bochner d'une fonction non intégrable est définie comme étant nulle. Par conséquent, une formalisation directe de la valeur de l'intégrale est impossible ; le problème doit être formulé comme la convergence des intégrales tronquées. De plus, les preuves classiques reposant sur l'astuce de Feynman (introduction d'un facteur exponentiel $e^{-at}$ et passage à la limite quand $a \to 0^+$ ) font face à des obstacles de formalisation : justifier l'interversion des limites nécessite des estimations de queue uniformes qui sont difficiles à coordonner dans le cadre formel de la convergence conditionnelle.

Méthodologie
Les auteurs adoptent une stratégie de preuve qui contourne les difficultés de la convergence conditionnelle en passant par la fonction $\text{sinc}^2(t)$ , qui est absolument intégrable.

Évaluation de $\text{sinc}^2$ : La formalisation établit d'abord que $\text{sinc}^2(t)$ est intégrable au sens de Lebesgue sur $(0, \infty)$ . Elle évalue l'intégrale $\int_0^\infty \text{sinc}^2(t) dt$ en introduisant une fonction auxiliaire $I(x) = \int_0^\infty e^{-xt} \text{sinc}^2(t) dt$ . En dérivant deux fois sous le signe intégral, les auteurs dérivent une expression de forme fermée pour $I(x)$ et prennent la limite quand $x \to 0^+$ en utilisant le théorème de la convergence dominée (DCT), ce qui est valide ici car $\text{sinc}^2$ est absolument intégrable.
Récupération de l'intégrale de Dirichlet : La valeur de l'intégrale de Dirichlet est récupérée via une identité reliant les intégrales tronquées de $\text{sinc}$ et de $\text{sinc}^2$ . En utilisant l'intégration par parties, les auteurs prouvent que pour tout $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)$
Lorsque $T \to \infty$ , le terme de bord s'annule, permettant d'équilibrer la limite de l'intégrale de $\text{sinc}$ avec la limite de l'intégrale de $\text{sinc}^2$ .
Structure formelle : La formalisation sépare strictement les concepts d'intégration de Lebesgue (utilisée pour $\text{sinc}^2$ ) et de limite des intégrales tronquées (utilisée pour $\text{sinc}$ ). La convergence est exprimée en utilisant les filtres Tendsto et atTop de Lean.

Contributions clés et résultats
Le papier présente la formalisation de trois familles interconnectées de résultats en analyse réelle :

L'intégrale de Dirichlet : Les auteurs fournissent une preuve vérifiée par machine que la limite des intégrales tronquées de $\text{sinc}(t)$ converge vers $\pi/2$ . Ceci est réalisé sans invoquer l'intégrale de Lebesgue de la fonction non intégrable elle-même.
La coupure de Dirichlet et la limite de Heaviside : La formalisation dérive la convergence de la primitive normalisée $D(x) = \frac{1}{2} + \frac{1}{\pi}\int_0^x \text{sinc}(t) dt$ vers la fonction de Heaviside. Plus précisément, elle prouve que $\lim_{R \to \infty} D(Rx) = H(x)$ ponctuellement. Ce résultat est étendu à une formule de coupure intégrale, montrant comment $D(R(a-t))$ agit comme une identité approchée pour les fonctions intégrables.
Identités d'intégrales trigonométriques : En utilisant l'évaluation de l'intégrale de $\text{sinc}^2$ $sinc^{2}$ , les auteurs formalisent plusieurs identités quadratiques et bilinéaires, incluant :
- $\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)}$
La formule intégrale de Lobatchevski : Le papier formalise la formule de Lobatchevski pour les fonctions périodiques continues $f$ satisfaisant $f(x+\pi)=f(x)$ et $f(\pi-x)=f(x)$ . Le théorème stipule :
$\int_0^\infty \text{sinc}^2(x)f(x) dx = \int_0^{\pi/2} f(x) dx$
La preuve utilise la densité des polynômes en cosinus dans l'espace des fonctions continues sur le cercle additif $\mathbb{R}/\pi\mathbb{Z}$ (un résultat disponible dans l'analyse de Fourier de Mathlib). Les auteurs vérifient d'abord l'identité pour les modes de cosinus individuels, puis l'étendent aux fonctions continues générales via l'approximation uniforme et un argument de contradiction.

Signification et affirmations
Les auteurs affirment que ce travail constitue la première formalisation de la formule intégrale de Lobatchevski dans un assistant de preuve. Bien que l'intégrale de Dirichlet ait été formalisée précédemment dans Isabelle/HOL (par Avigad et al.) en utilisant une approche différente impliquant le théorème de Fubini et la représentation de $1/x$ comme une intégrale, la contribution de ce papier réside dans son passage spécifique par $\text{sinc}^2$ et son application à la formule de Lobatchevski.

La signification du travail est double :

Méthodologique : Il démontre une stratégie robuste pour traiter les intégrales à convergence conditionnelle dans les systèmes formels en les séparant de leurs contreparties à convergence absolue, évitant ainsi les pièges de l'intégration de Lebesgue directe pour les fonctions non intégrables.
Théorique : Il jette un pont entre l'analyse réelle classique et les bibliothèques formelles modernes en appliquant l'infrastructure d'analyse de Fourier de Mathlib (spécifiquement les résultats de densité sur le cercle additif) pour prouver une identité d'intégrale classique qui n'avait pas été vérifiée par machine auparavant.

Le papier conclut en notant que l'infrastructure développée permet des extensions potentielles, telles que la formalisation de formules de type Lobatchevski pour des puissures paires supérieures de la fonction sinc et des applications à la théorie de la transformée de Laplace, bien que celles-ci soient présentées comme des directions futures plutôt que comme des travaux achevés.

Articles similaires